Skip to content

Commit

Permalink
Merge branch 'master' into fix-5969-sync-for-rust
Browse files Browse the repository at this point in the history
  • Loading branch information
@MikaelMayer
MikaelMayer authored Jan 11, 2025
2 parents fb43df6 + 0a33545 commit 1c6bb02
Show file tree
Hide file tree
Showing 15 changed files with 136 additions and 61 deletions.
48 changes: 35 additions & 13 deletions Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -265,15 +265,27 @@ protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw, string a
return wr.NewBlock($"public static void _StaticMain(Dafny.ISequence<Dafny.ISequence<{CharTypeName}>> {argsParameterName})");
}

/// <summary>
/// Compute the name of the class to use to translate a data-type or a class
/// </summary>
private string protectedTypeName(TopLevelDecl dt) {
var protectedName = IdName(dt);
if (dt.EnclosingModuleDefinition is { Name: var moduleName } && moduleName == protectedName) {
return $"_{protectedName}";
}
return protectedName;
}

string IdProtectModule(string moduleName) {
Contract.Requires(moduleName != null);
return string.Join(".", moduleName.Split(".").Select(IdProtect));
}

protected override ConcreteSyntaxTree CreateModule(ModuleDefinition module, string moduleName, bool isDefault,
ModuleDefinition externModule,
string libraryName /*?*/, Attributes moduleAttributes, ConcreteSyntaxTree wr) {
moduleName = IdProtectModule(moduleName);
return wr.NewBlock($"namespace {moduleName}", " // end of " + $"namespace {moduleName}");
var protectedModuleName = IdProtectModule(moduleName);
return wr.NewBlock($"namespace {protectedModuleName}", " // end of " + $"namespace {protectedModuleName}");
}

protected override string GetHelperModuleName() => DafnyHelpersClass;
Expand Down Expand Up @@ -305,8 +317,9 @@ string PrintVariance(TypeParameter.TPVariance variance) {
return $"<{targs.Comma(PrintTypeParameter)}>";
}

protected override IClassWriter CreateClass(string moduleName, string name, bool isExtern, string /*?*/ fullPrintName,
protected override IClassWriter CreateClass(string moduleName, bool isExtern, string /*?*/ fullPrintName,
List<TypeParameter> typeParameters, TopLevelDecl cls, List<Type>/*?*/ superClasses, IOrigin tok, ConcreteSyntaxTree wr) {
var name = protectedTypeName(cls);
var wBody = WriteTypeHeader("partial class", name, typeParameters, superClasses, tok, wr);

ConcreteSyntaxTree/*?*/ wCtorBody = null;
Expand Down Expand Up @@ -442,7 +455,7 @@ protected override ConcreteSyntaxTree CreateIterator(IteratorDecl iter, Concrete
// }
// }

var cw = (ClassWriter)CreateClass(IdProtect(iter.EnclosingModuleDefinition.GetCompileName(Options)), IdName(iter), iter, wr);
var cw = (ClassWriter)CreateClass(IdProtect(iter.EnclosingModuleDefinition.GetCompileName(Options)), iter, wr);
var w = cw.InstanceMemberWriter;
// here come the fields

Expand Down Expand Up @@ -559,7 +572,7 @@ IClassWriter CompileDatatypeBase(DatatypeDecl dt, ConcreteSyntaxTree wr) {
// }
var nonGhostTypeArgs = SelectNonGhost(dt, dt.TypeArgs);
var DtT_TypeArgs = TypeParameters(nonGhostTypeArgs);
var DtT_protected = IdName(dt) + DtT_TypeArgs;
var DtT_protected = protectedTypeName(dt) + DtT_TypeArgs;
var simplifiedType = DatatypeWrapperEraser.SimplifyType(Options, UserDefinedType.FromTopLevelDecl(dt.Origin, dt));
var simplifiedTypeName = TypeName(simplifiedType, wr, dt.Origin);

Expand All @@ -581,7 +594,7 @@ IClassWriter CompileDatatypeBase(DatatypeDecl dt, ConcreteSyntaxTree wr) {
} else {
EmitTypeDescriptorsForClass(dt.TypeArgs, dt, out var wTypeFields, out var wCtorParams, out _, out var wCtorBody);
wr.Append(wTypeFields);
wr.Format($"public {IdName(dt)}({wCtorParams})").NewBlock().Append(wCtorBody);
wr.Format($"public {protectedTypeName(dt)}({wCtorParams})").NewBlock().Append(wCtorBody);
}

var wDefault = new ConcreteSyntaxTree();
Expand Down Expand Up @@ -995,7 +1008,7 @@ private void CompileDatatypeConstructors(DatatypeDecl dt, ConcreteSyntaxTree wrx
// public override _IDt<T> _Get() { if (c != null) { d = c(); c = null; } return d; }
// public override string ToString() { return _Get().ToString(); }
// }
var w = wrx.NewNamedBlock($"public class {dt.GetCompileName(Options)}__Lazy{typeParams} : {IdName(dt)}{typeParams}");
var w = wrx.NewNamedBlock($"public class {dt.GetCompileName(Options)}__Lazy{typeParams} : {protectedTypeName(dt)}{typeParams}");
w.WriteLine($"public {NeedsNew(dt, "Computer")}delegate {DtTypeName(dt)} Computer();");
w.WriteLine($"{NeedsNew(dt, "c")}Computer c;");
w.WriteLine($"{NeedsNew(dt, "d")}{DtTypeName(dt)} d;");
Expand All @@ -1017,7 +1030,7 @@ private void CompileDatatypeConstructors(DatatypeDecl dt, ConcreteSyntaxTree wrx
int constructorIndex = 0; // used to give each constructor a different name
foreach (var ctor in dt.Ctors.Where(ctor => !ctor.IsGhost)) {
var wr = wrx.NewNamedBlock(
$"public class {DtCtorDeclarationName(ctor)}{TypeParameters(nonGhostTypeArgs)} : {IdName(dt)}{typeParams}");
$"public class {DtCtorDeclarationName(ctor)}{TypeParameters(nonGhostTypeArgs)} : {protectedTypeName(dt)}{typeParams}");
DatatypeFieldsAndConstructor(ctor, constructorIndex, wr);
constructorIndex++;
}
Expand Down Expand Up @@ -1191,7 +1204,7 @@ string DtCtorDeclarationName(DatatypeCtor ctor) {
Contract.Ensures(Contract.Result<string>() != null);

var dt = ctor.EnclosingDatatype;
return dt.IsRecordType ? IdName(dt) : dt.GetCompileName(Options) + "_" + ctor.GetCompileName(Options);
return dt.IsRecordType ? protectedTypeName(dt) : dt.GetCompileName(Options) + "_" + ctor.GetCompileName(Options);
}

/// <summary>
Expand All @@ -1217,7 +1230,7 @@ string DtCtorName(DatatypeCtor ctor) {
Contract.Ensures(Contract.Result<string>() != null);

var dt = ctor.EnclosingDatatype;
var dtName = IdName(dt);
var dtName = protectedTypeName(dt);
if (!dt.EnclosingModuleDefinition.TryToAvoidName) {
dtName = IdProtectModule(dt.EnclosingModuleDefinition.GetCompileName(Options)) + "." + dtName;
}
Expand All @@ -1235,7 +1248,7 @@ string DtCreateName(DatatypeCtor ctor) {
}

protected override IClassWriter DeclareNewtype(NewtypeDecl nt, ConcreteSyntaxTree wr) {
var cw = (ClassWriter)CreateClass(IdProtect(nt.EnclosingModuleDefinition.GetCompileName(Options)), IdName(nt), nt, wr);
var cw = (ClassWriter)CreateClass(IdProtect(nt.EnclosingModuleDefinition.GetCompileName(Options)), nt, wr);
var w = cw.StaticMemberWriter;
if (nt.NativeType != null) {
var wEnum = w.NewBlock($"public static System.Collections.Generic.IEnumerable<{GetNativeTypeName(nt.NativeType)}> IntegerRange(BigInteger lo, BigInteger hi)");
Expand Down Expand Up @@ -1304,7 +1317,7 @@ void DeclareBoxedNewtype(NewtypeDecl nt, ConcreteSyntaxTree wr) {
}

protected override void DeclareSubsetType(SubsetTypeDecl sst, ConcreteSyntaxTree wr) {
var cw = (ClassWriter)CreateClass(IdProtect(sst.EnclosingModuleDefinition.GetCompileName(Options)), IdName(sst), sst, wr);
var cw = (ClassWriter)CreateClass(IdProtect(sst.EnclosingModuleDefinition.GetCompileName(Options)), sst, wr);
if (sst.WitnessKind == SubsetTypeDecl.WKind.Compiled) {
var sw = new ConcreteSyntaxTree(cw.InstanceMemberWriter.RelativeIndentLevel);
var wStmts = cw.InstanceMemberWriter.Fork();
Expand Down Expand Up @@ -2507,13 +2520,22 @@ private string FullTypeName(UserDefinedType udt, MemberDecl/*?*/ member = null,
return (cl.EnclosingModuleDefinition.TryToAvoidName ? "" : IdProtectModule(cl.EnclosingModuleDefinition.GetCompileName(Options)) + ".") + DtTypeName(cl, false);
}

if (cl is DatatypeDecl) {
return (cl.EnclosingModuleDefinition.TryToAvoidName ? "" : IdProtectModule(cl.EnclosingModuleDefinition.GetCompileName(Options)) + ".") + protectedTypeName(cl as DatatypeDecl);
}

if (cl.EnclosingModuleDefinition.TryToAvoidName) {
return IdProtect(cl.GetCompileName(Options));
}

if (cl.IsExtern(Options, out _, out _)) {
return cl.EnclosingModuleDefinition.GetCompileName(Options) + "." + cl.GetCompileName(Options);
}

if (cl is ClassDecl) {
return (cl.EnclosingModuleDefinition.TryToAvoidName ? "" : IdProtectModule(cl.EnclosingModuleDefinition.GetCompileName(Options)) + ".") + protectedTypeName(cl as ClassDecl);
}

return IdProtectModule(cl.EnclosingModuleDefinition.GetCompileName(Options)) + "." + IdProtect(cl.GetCompileName(Options));
}

Expand All @@ -2528,7 +2550,7 @@ protected override void EmitThis(ConcreteSyntaxTree wr, bool callToInheritedMemb

protected override void EmitDatatypeValue(DatatypeValue dtv, string typeDescriptorArguments, string arguments, ConcreteSyntaxTree wr) {
var dt = dtv.Ctor.EnclosingDatatype;
var dtName = IdProtectModule(dt.EnclosingModuleDefinition.GetCompileName(Options)) + "." + IdName(dt);
var dtName = IdProtectModule(dt.EnclosingModuleDefinition.GetCompileName(Options)) + "." + protectedTypeName(dt);

var nonGhostInferredTypeArgs = SelectNonGhost(dt, dtv.InferredTypeArgs);
var typeParams = nonGhostInferredTypeArgs.Count == 0 ? "" : $"<{TypeNames(nonGhostInferredTypeArgs, wr, dtv.Origin)}>";
Expand Down
41 changes: 25 additions & 16 deletions Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -149,7 +149,7 @@ protected override void EmitFooter(Program program, ConcreteSyntaxTree wr) {
public override void EmitCallToMain(Method mainMethod, string baseName, ConcreteSyntaxTree wr) {
var w = wr.NewBlock("int main(int argc, char *argv[])");
var tryWr = w.NewBlock("try");
tryWr.WriteLine(string.Format("{0}::{1}::{2}(dafny_get_args(argc, argv));", mainMethod.EnclosingClass.EnclosingModuleDefinition.GetCompileName(Options), mainMethod.EnclosingClass.GetCompileName(Options), mainMethod.Name));
tryWr.WriteLine(string.Format("{0}::{1}::{2}(dafny_get_args(argc, argv));", mainMethod.EnclosingClass.EnclosingModuleDefinition.GetCompileName(Options), clName(mainMethod.EnclosingClass), mainMethod.Name));
var catchWr = w.NewBlock("catch (DafnyHaltException & e)");
catchWr.WriteLine("std::cout << \"Program halted: \" << e.what() << std::endl;");
}
Expand Down Expand Up @@ -226,9 +226,18 @@ private string InstantiateTemplate(List<Type> typeArgs) {

protected override string GetHelperModuleName() => "_dafny";

protected override IClassWriter CreateClass(string moduleName, string name, bool isExtern, string/*?*/ fullPrintName, List<TypeParameter>/*?*/ typeParameters, TopLevelDecl cls, List<Type>/*?*/ superClasses, IOrigin tok, ConcreteSyntaxTree wr) {
private string clName(TopLevelDecl cl) {
var className = IdName(cl);
if (cl is ClassDecl || cl is DefaultClassDecl) {
return className;
}
return "class_" + className;
}

protected override IClassWriter CreateClass(string moduleName, bool isExtern, string/*?*/ fullPrintName, List<TypeParameter>/*?*/ typeParameters, TopLevelDecl cls, List<Type>/*?*/ superClasses, IOrigin tok, ConcreteSyntaxTree wr) {
var className = clName(cls);
if (isExtern) {
throw new UnsupportedFeatureException(tok, Feature.ExternalClasses, String.Format("extern in class {0}", name));
throw new UnsupportedFeatureException(tok, Feature.ExternalClasses, String.Format("extern in class {0}", className));
}
if (superClasses != null && superClasses.Any(trait => !trait.IsObject)) {
throw new UnsupportedFeatureException(tok, Feature.Traits);
Expand All @@ -242,17 +251,17 @@ protected override IClassWriter CreateClass(string moduleName, string name, bool
classDefWriter.WriteLine(DeclareTemplate(typeParameters));
}

var methodDeclWriter = classDefWriter.NewBlock(string.Format("class {0}", name), ";");
var methodDeclWriter = classDefWriter.NewBlock(string.Format("class {0}", className), ";");
var methodDefWriter = wr;

classDeclWriter.WriteLine("class {0};", name);
classDeclWriter.WriteLine("class {0};", className);

methodDeclWriter.Write("public:\n");
methodDeclWriter.WriteLine("// Default constructor");
methodDeclWriter.WriteLine("{0}() {{}}", name);
methodDeclWriter.WriteLine("{0}() {{}}", className);

// Create the code for the specialization of get_default
var fullName = moduleName + "::" + name;
var fullName = moduleName + "::" + className;
var getDefaultStr = String.Format("template <{0}>\nstruct get_default<std::shared_ptr<{1}{2} > > {{\n",
TypeParameters(typeParameters),
fullName,
Expand All @@ -266,7 +275,7 @@ protected override IClassWriter CreateClass(string moduleName, string name, bool

var fieldWriter = methodDeclWriter;

return new ClassWriter(name, this, methodDeclWriter, methodDefWriter, fieldWriter, wr);
return new ClassWriter(className, this, methodDeclWriter, methodDefWriter, fieldWriter, wr);
}

protected override bool SupportsProperties { get => false; }
Expand Down Expand Up @@ -615,8 +624,8 @@ protected override IClassWriter DeclareNewtype(NewtypeDecl nt, ConcreteSyntaxTre
} else {
throw new UnsupportedFeatureException(nt.Origin, Feature.NonNativeNewtypes);
}
var className = "class_" + IdName(nt);
var cw = CreateClass(nt.EnclosingModuleDefinition.GetCompileName(Options), className, nt, wr) as ClassWriter;
var cw = CreateClass(nt.EnclosingModuleDefinition.GetCompileName(Options), nt, wr) as ClassWriter;
var className = clName(nt);
var w = cw.MethodDeclWriter;
if (nt.WitnessKind == SubsetTypeDecl.WKind.Compiled) {
var witness = new ConcreteSyntaxTree(w.RelativeIndentLevel);
Expand Down Expand Up @@ -653,8 +662,8 @@ protected override void DeclareSubsetType(SubsetTypeDecl sst, ConcreteSyntaxTree

this.modDeclWr.WriteLine("{0} using {1} = {2};", templateDecl, IdName(sst), TypeName(sst.Var.Type, wr, sst.Origin));

var className = "class_" + IdName(sst);
var cw = CreateClass(sst.EnclosingModuleDefinition.GetCompileName(Options), className, sst, wr) as ClassWriter;
var cw = CreateClass(sst.EnclosingModuleDefinition.GetCompileName(Options), sst, wr) as ClassWriter;
var className = clName(sst);
var w = cw.MethodDeclWriter;

if (sst.WitnessKind == SubsetTypeDecl.WKind.Compiled) {
Expand Down Expand Up @@ -785,7 +794,7 @@ public void Finish() { }

wr.Write("{0} {1}{2}::{3}",
targetReturnTypeReplacement ?? "void",
m.EnclosingClass.GetCompileName(Options),
clName(m.EnclosingClass),
InstantiateTemplate(m.EnclosingClass.TypeArgs),
IdName(m));

Expand Down Expand Up @@ -1043,7 +1052,7 @@ protected override string TypeInitializationValue(Type type, ConcreteSyntaxTree
} else if (cl is NewtypeDecl) {
var td = (NewtypeDecl)cl;
if (td.Witness != null) {
return td.EnclosingModuleDefinition.GetCompileName(Options) + "::class_" + td.GetCompileName(Options) + "::Witness";
return td.EnclosingModuleDefinition.GetCompileName(Options) + "::" + clName(td) + "::Witness";
} else if (td.NativeType != null) {
return "0";
} else {
Expand All @@ -1052,7 +1061,7 @@ protected override string TypeInitializationValue(Type type, ConcreteSyntaxTree
} else if (cl is SubsetTypeDecl) {
var td = (SubsetTypeDecl)cl;
if (td.WitnessKind == SubsetTypeDecl.WKind.Compiled) {
return td.EnclosingModuleDefinition.GetCompileName(Options) + "::class_" + td.GetCompileName(Options) + "::Witness";
return td.EnclosingModuleDefinition.GetCompileName(Options) + "::" + clName(td) + "::Witness";
} else if (td.WitnessKind == SubsetTypeDecl.WKind.Special) {
// WKind.Special is only used with -->, ->, and non-null types:
Contract.Assert(ArrowType.IsPartialArrowTypeName(td.Name) || ArrowType.IsTotalArrowTypeName(td.Name) || td is NonNullTypeDecl);
Expand Down Expand Up @@ -1762,7 +1771,7 @@ protected override ILvalue EmitMemberSelect(Action<ConcreteSyntaxTree> obj, Type
// This used to work, but now obj comes in wanting to use TypeName on the class, which results in (std::shared_ptr<_module::MyClass>)::c;
//return SuffixLvalue(obj, "::{0}", member.CompileName);
return SimpleLvalue(wr => {
wr.Write("{0}::{1}::{2}", IdProtect(member.EnclosingClass.EnclosingModuleDefinition.GetCompileName(Options)), IdProtect(member.EnclosingClass.GetCompileName(Options)), IdProtect(member.GetCompileName(Options)));
wr.Write("{0}::{1}::{2}", IdProtect(member.EnclosingClass.EnclosingModuleDefinition.GetCompileName(Options)), IdProtect(clName(member.EnclosingClass)), IdProtect(member.GetCompileName(Options)));
});
} else if (member is DatatypeDestructor dtor && dtor.EnclosingClass is TupleTypeDecl) {
return SuffixLvalue(obj, ".get<{0}>()", dtor.Name);
Expand Down
4 changes: 2 additions & 2 deletions Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -193,13 +193,13 @@ protected override ConcreteSyntaxTree EmitCoercionIfNecessary(Type from, Type to
}
}

protected override IClassWriter CreateClass(string moduleName, string name, bool isExtern, string fullPrintName,
protected override IClassWriter CreateClass(string moduleName, bool isExtern, string fullPrintName,
List<TypeParameter> typeParameters, TopLevelDecl cls, List<Type> superClasses, IOrigin tok, ConcreteSyntaxTree wr) {
if (currentBuilder is ClassContainer builder) {
List<DAST.TypeArgDecl> typeParams = typeParameters.Select(tp => GenTypeArgDecl(tp)).ToList();

return new ClassWriter(this, typeParams.Count > 0, builder.Class(
name, moduleName, typeParams, superClasses.Select(t => GenType(t)).ToList(),
IdName(cls), moduleName, typeParams, superClasses.Select(t => GenType(t)).ToList(),
ParseAttributes(cls.Attributes), GetDocString(cls))
);
} else {
Expand Down
Loading

0 comments on commit 1c6bb02

Please sign in to comment.