From 5bde019be1cb76c4e910668ad540db83079eddf1 Mon Sep 17 00:00:00 2001 From: Olivier Bouissou Date: Fri, 3 Jan 2025 15:57:54 -0500 Subject: [PATCH 01/45] Update test to run on all back-ends --- .../TestFiles/LitTests/LitTest/git-issues/git-issue-6014.dfy | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-6014.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-6014.dfy index 38f582328f..5965e1212f 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-6014.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-6014.dfy @@ -1,6 +1,4 @@ -// NONUNIFORM: Test still fails on CS (https://github.com/dafny-lang/dafny/issues/5746) -// RUN: %run --target java "%s" > "%t" -// RUN: %diff "%s.expect" "%t" +// RUN: %testDafnyForEachCompiler --refresh-exit-code=0 "%s" module State { From 32e1456fb87833651dc201d06e6a7597e8218177 Mon Sep 17 00:00:00 2001 From: Olivier Bouissou Date: Mon, 6 Jan 2025 15:48:36 -0500 Subject: [PATCH 02/45] Change name of namespace if there is a name clash with a data type --- .../Backends/CSharp/CsharpCodeGenerator.cs | 25 +++++++++++++++++-- 1 file changed, 23 insertions(+), 2 deletions(-) diff --git a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs index cccbd96d39..0dd3205af2 100644 --- a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs +++ b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs @@ -265,15 +265,36 @@ protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw, string a return wr.NewBlock($"public static void _StaticMain(Dafny.ISequence> {argsParameterName})"); } + private IDictionary moduleNameMapping = new Dictionary(); + string IdProtectModule(string moduleName) { + Contract.Requires(moduleName != null); + if (moduleNameMapping.ContainsKey(moduleName)) { + return moduleNameMapping[moduleName]; + } 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); + var hasNameClash = false; + // If the module has a type decl with the same name, change the name of the generated nameclass + // to _N+moduleName to avoid name clashes. + if (module != null) { + foreach (var d in module.TopLevelDecls) { + if (d is DatatypeDecl) { + if (d.Name == module.Name) { + hasNameClash = true; + break; + } + } + } + } + protectedModuleName = hasNameClash ? "_N" + protectedModuleName : protectedModuleName; + moduleNameMapping.Add(moduleName, protectedModuleName); + return wr.NewBlock($"namespace {protectedModuleName}", " // end of " + $"namespace _N{moduleName}"); } protected override string GetHelperModuleName() => DafnyHelpersClass; From f8333da04b63ac65100c1e5d6cafec5299f2d441 Mon Sep 17 00:00:00 2001 From: Olivier Bouissou Date: Mon, 6 Jan 2025 16:00:44 -0500 Subject: [PATCH 03/45] Adding fix files --- docs/news/fix.5746 | 1 + docs/news/fix.6014 | 1 + 2 files changed, 2 insertions(+) create mode 100644 docs/news/fix.5746 create mode 100644 docs/news/fix.6014 diff --git a/docs/news/fix.5746 b/docs/news/fix.5746 new file mode 100644 index 0000000000..19e1b00b37 --- /dev/null +++ b/docs/news/fix.5746 @@ -0,0 +1 @@ +Fix C# generated code when a module contains a type with the same name diff --git a/docs/news/fix.6014 b/docs/news/fix.6014 new file mode 100644 index 0000000000..614d71f332 --- /dev/null +++ b/docs/news/fix.6014 @@ -0,0 +1 @@ +Fix Java generated code when a module contains a type with the same name From 218384330ca8e30be6ca5eaba7d9c54241462d31 Mon Sep 17 00:00:00 2001 From: Olivier Bouissou Date: Mon, 6 Jan 2025 16:13:01 -0500 Subject: [PATCH 04/45] Avoid issue when translating multiple times a module named Dafny --- .../Backends/CSharp/CsharpCodeGenerator.cs | 26 +++++++++++-------- 1 file changed, 15 insertions(+), 11 deletions(-) diff --git a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs index 0dd3205af2..9249291481 100644 --- a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs +++ b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs @@ -279,21 +279,25 @@ protected override ConcreteSyntaxTree CreateModule(ModuleDefinition module, stri ModuleDefinition externModule, string libraryName /*?*/, Attributes moduleAttributes, ConcreteSyntaxTree wr) { var protectedModuleName = IdProtectModule(moduleName); - var hasNameClash = false; - // If the module has a type decl with the same name, change the name of the generated nameclass - // to _N+moduleName to avoid name clashes. - if (module != null) { - foreach (var d in module.TopLevelDecls) { - if (d is DatatypeDecl) { - if (d.Name == module.Name) { - hasNameClash = true; - break; + if (moduleNameMapping.ContainsKey(moduleName)) { + protectedModuleName = moduleNameMapping[moduleName]; + } else { + var hasNameClash = false; + // If the module has a type decl with the same name, change the name of the generated nameclass + // to _N+moduleName to avoid name clashes. + if (module != null) { + foreach (var d in module.TopLevelDecls) { + if (d is DatatypeDecl) { + if (d.Name == module.Name) { + hasNameClash = true; + break; + } } } } + protectedModuleName = hasNameClash ? "_N" + protectedModuleName : protectedModuleName; + moduleNameMapping.Add(moduleName, protectedModuleName); } - protectedModuleName = hasNameClash ? "_N" + protectedModuleName : protectedModuleName; - moduleNameMapping.Add(moduleName, protectedModuleName); return wr.NewBlock($"namespace {protectedModuleName}", " // end of " + $"namespace _N{moduleName}"); } From 38af5324c1473fd5ade50d3e2796fa82d197012c Mon Sep 17 00:00:00 2001 From: Olivier Bouissou Date: Mon, 6 Jan 2025 17:59:36 -0500 Subject: [PATCH 05/45] Updating .expect file --- .../LitTests/LitTest/git-issues/git-issue-6014.dfy.expect | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-6014.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-6014.dfy.expect index 3b538928db..05a682bd4e 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-6014.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-6014.dfy.expect @@ -1,3 +1 @@ - -Dafny program verifier finished with 0 verified, 0 errors -Hello! +Hello! \ No newline at end of file From 0000eb210181ad798e4226da5eb790646f0b299e Mon Sep 17 00:00:00 2001 From: Olivier Bouissou Date: Mon, 6 Jan 2025 22:39:27 -0500 Subject: [PATCH 06/45] Addind newline --- .../LitTests/LitTest/git-issues/git-issue-6014.dfy.expect | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-6014.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-6014.dfy.expect index 05a682bd4e..10ddd6d257 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-6014.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-6014.dfy.expect @@ -1 +1 @@ -Hello! \ No newline at end of file +Hello! From 8758fa64ef5cd807da31a66a341abcc013865ee9 Mon Sep 17 00:00:00 2001 From: Olivier Bouissou Date: Tue, 7 Jan 2025 10:45:13 -0500 Subject: [PATCH 07/45] Fixing comment at the end of the namespace definition --- Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs index 9249291481..c3cbcf20b0 100644 --- a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs +++ b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs @@ -298,7 +298,7 @@ protected override ConcreteSyntaxTree CreateModule(ModuleDefinition module, stri protectedModuleName = hasNameClash ? "_N" + protectedModuleName : protectedModuleName; moduleNameMapping.Add(moduleName, protectedModuleName); } - return wr.NewBlock($"namespace {protectedModuleName}", " // end of " + $"namespace _N{moduleName}"); + return wr.NewBlock($"namespace {protectedModuleName}", " // end of " + $"namespace {protectedModuleName}"); } protected override string GetHelperModuleName() => DafnyHelpersClass; From 63cf4043cf32ce1be887607f534e6a513a40974d Mon Sep 17 00:00:00 2001 From: Olivier Bouissou Date: Tue, 7 Jan 2025 11:05:20 -0500 Subject: [PATCH 08/45] Adding comments --- Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs | 2 ++ 1 file changed, 2 insertions(+) diff --git a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs index c3cbcf20b0..630e908d0b 100644 --- a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs +++ b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs @@ -265,6 +265,8 @@ protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw, string a return wr.NewBlock($"public static void _StaticMain(Dafny.ISequence> {argsParameterName})"); } + // Mapping of Dafny module name to C# module names. The C# module names could be changed to + // avoid name clash between a namespace and a datatype declared within it. private IDictionary moduleNameMapping = new Dictionary(); string IdProtectModule(string moduleName) { From ffd7b41b39b0c97678662e0e85240f430beb7973 Mon Sep 17 00:00:00 2001 From: Olivier Bouissou Date: Tue, 7 Jan 2025 13:49:54 -0500 Subject: [PATCH 09/45] Change logic to update name of class rather than name of namespace. Makes the solution more robust. --- .../Backends/CSharp/CsharpCodeGenerator.cs | 58 +++++++++---------- 1 file changed, 26 insertions(+), 32 deletions(-) diff --git a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs index 630e908d0b..eb74bcf06c 100644 --- a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs +++ b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs @@ -265,15 +265,24 @@ protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw, string a return wr.NewBlock($"public static void _StaticMain(Dafny.ISequence> {argsParameterName})"); } - // Mapping of Dafny module name to C# module names. The C# module names could be changed to - // avoid name clash between a namespace and a datatype declared within it. - private IDictionary moduleNameMapping = new Dictionary(); + /// + /// Compute the name of the class to use to translate a data-type + /// + private string dataTypeName(DatatypeDecl dt) { + var protectedName = IdProtect(dt.Name); + if (dt.EnclosingModuleDefinition is not null) { + var moduleName = IdProtectModule(dt.EnclosingModuleDefinition.Name); + if (moduleName == protectedName) { + return $"_{protectedName}"; + } else { + return $"{moduleName}_{protectedName}"; + } + } + return protectedName; + } string IdProtectModule(string moduleName) { Contract.Requires(moduleName != null); - if (moduleNameMapping.ContainsKey(moduleName)) { - return moduleNameMapping[moduleName]; - } return string.Join(".", moduleName.Split(".").Select(IdProtect)); } @@ -281,25 +290,6 @@ protected override ConcreteSyntaxTree CreateModule(ModuleDefinition module, stri ModuleDefinition externModule, string libraryName /*?*/, Attributes moduleAttributes, ConcreteSyntaxTree wr) { var protectedModuleName = IdProtectModule(moduleName); - if (moduleNameMapping.ContainsKey(moduleName)) { - protectedModuleName = moduleNameMapping[moduleName]; - } else { - var hasNameClash = false; - // If the module has a type decl with the same name, change the name of the generated nameclass - // to _N+moduleName to avoid name clashes. - if (module != null) { - foreach (var d in module.TopLevelDecls) { - if (d is DatatypeDecl) { - if (d.Name == module.Name) { - hasNameClash = true; - break; - } - } - } - } - protectedModuleName = hasNameClash ? "_N" + protectedModuleName : protectedModuleName; - moduleNameMapping.Add(moduleName, protectedModuleName); - } return wr.NewBlock($"namespace {protectedModuleName}", " // end of " + $"namespace {protectedModuleName}"); } @@ -586,7 +576,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 = dataTypeName(dt) + DtT_TypeArgs; var simplifiedType = DatatypeWrapperEraser.SimplifyType(Options, UserDefinedType.FromTopLevelDecl(dt.Origin, dt)); var simplifiedTypeName = TypeName(simplifiedType, wr, dt.Origin); @@ -608,7 +598,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 {dataTypeName(dt)}({wCtorParams})").NewBlock().Append(wCtorBody); } var wDefault = new ConcreteSyntaxTree(); @@ -1022,7 +1012,7 @@ private void CompileDatatypeConstructors(DatatypeDecl dt, ConcreteSyntaxTree wrx // public override _IDt _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} : {dataTypeName(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;"); @@ -1044,7 +1034,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)} : {dataTypeName(dt)}{typeParams}"); DatatypeFieldsAndConstructor(ctor, constructorIndex, wr); constructorIndex++; } @@ -1218,7 +1208,7 @@ string DtCtorDeclarationName(DatatypeCtor ctor) { Contract.Ensures(Contract.Result() != null); var dt = ctor.EnclosingDatatype; - return dt.IsRecordType ? IdName(dt) : dt.GetCompileName(Options) + "_" + ctor.GetCompileName(Options); + return dt.IsRecordType ? dataTypeName(dt) : dt.GetCompileName(Options) + "_" + ctor.GetCompileName(Options); } /// @@ -1244,7 +1234,7 @@ string DtCtorName(DatatypeCtor ctor) { Contract.Ensures(Contract.Result() != null); var dt = ctor.EnclosingDatatype; - var dtName = IdName(dt); + var dtName = dataTypeName(dt); if (!dt.EnclosingModuleDefinition.TryToAvoidName) { dtName = IdProtectModule(dt.EnclosingModuleDefinition.GetCompileName(Options)) + "." + dtName; } @@ -2534,6 +2524,10 @@ 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)) + ".") + dataTypeName(cl as DatatypeDecl); + } + if (cl.EnclosingModuleDefinition.TryToAvoidName) { return IdProtect(cl.GetCompileName(Options)); } @@ -2555,7 +2549,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)) + "." + dataTypeName(dt); var nonGhostInferredTypeArgs = SelectNonGhost(dt, dtv.InferredTypeArgs); var typeParams = nonGhostInferredTypeArgs.Count == 0 ? "" : $"<{TypeNames(nonGhostInferredTypeArgs, wr, dtv.Origin)}>"; From c217fb5a2e7a8dc19c6ead8f24501b49a0a00b13 Mon Sep 17 00:00:00 2001 From: Olivier Bouissou Date: Tue, 7 Jan 2025 16:02:01 -0500 Subject: [PATCH 10/45] Remove debug code --- Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs | 2 -- 1 file changed, 2 deletions(-) diff --git a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs index eb74bcf06c..b9df5f79c1 100644 --- a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs +++ b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs @@ -274,8 +274,6 @@ private string dataTypeName(DatatypeDecl dt) { var moduleName = IdProtectModule(dt.EnclosingModuleDefinition.Name); if (moduleName == protectedName) { return $"_{protectedName}"; - } else { - return $"{moduleName}_{protectedName}"; } } return protectedName; From 8b8382dfeb680bc388fb237fc5e4440ef24c25ab Mon Sep 17 00:00:00 2001 From: Olivier Bouissou Date: Tue, 7 Jan 2025 16:26:07 -0500 Subject: [PATCH 11/45] Fix issue --- Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs index b9df5f79c1..efc6ef120c 100644 --- a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs +++ b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs @@ -269,7 +269,7 @@ protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw, string a /// Compute the name of the class to use to translate a data-type /// private string dataTypeName(DatatypeDecl dt) { - var protectedName = IdProtect(dt.Name); + var protectedName = IdName(dt); if (dt.EnclosingModuleDefinition is not null) { var moduleName = IdProtectModule(dt.EnclosingModuleDefinition.Name); if (moduleName == protectedName) { From 33aae8f4d2fea7bd6d5ed5d064d41e8188466871 Mon Sep 17 00:00:00 2001 From: Olivier Bouissou Date: Tue, 7 Jan 2025 17:28:11 -0500 Subject: [PATCH 12/45] Extension to classes within modules --- .../Backends/CSharp/CsharpCodeGenerator.cs | 24 ++++++++-- .../Backends/Cplusplus/CppCodeGenerator.cs | 19 ++++---- .../Backends/Dafny/DafnyCodeGenerator.cs | 4 +- .../Backends/GoLang/GoCodeGenerator.cs | 14 +++--- .../Backends/Java/JavaCodeGenerator.cs | 7 +-- .../JavaScript/JavaScriptCodeGenerator.cs | 9 ++-- .../Backends/Python/PythonCodeGenerator.cs | 7 +-- .../SinglePassCodeGenerator.cs | 10 ++--- .../LitTest/git-issues/git-issue-6014.dfy | 45 ++++++++++++++++++- 9 files changed, 101 insertions(+), 38 deletions(-) diff --git a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs index efc6ef120c..c945b8e100 100644 --- a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs +++ b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs @@ -279,6 +279,17 @@ private string dataTypeName(DatatypeDecl dt) { return protectedName; } + private string className(TopLevelDecl dt) { + var protectedName = IdName(dt); + if (dt.EnclosingModuleDefinition is not null) { + var moduleName = IdProtectModule(dt.EnclosingModuleDefinition.Name); + if (moduleName == protectedName) { + return $"_{protectedName}"; + } + } + return protectedName; + } + string IdProtectModule(string moduleName) { Contract.Requires(moduleName != null); return string.Join(".", moduleName.Split(".").Select(IdProtect)); @@ -320,8 +331,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, TopLevelDecl tl, bool isExtern, string /*?*/ fullPrintName, List typeParameters, TopLevelDecl cls, List/*?*/ superClasses, IOrigin tok, ConcreteSyntaxTree wr) { + var name = className(tl); var wBody = WriteTypeHeader("partial class", name, typeParameters, superClasses, tok, wr); ConcreteSyntaxTree/*?*/ wCtorBody = null; @@ -457,7 +469,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, iter, wr); var w = cw.InstanceMemberWriter; // here come the fields @@ -1250,7 +1262,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, 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)"); @@ -1319,7 +1331,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, sst, wr); if (sst.WitnessKind == SubsetTypeDecl.WKind.Compiled) { var sw = new ConcreteSyntaxTree(cw.InstanceMemberWriter.RelativeIndentLevel); var wStmts = cw.InstanceMemberWriter.Fork(); @@ -2526,6 +2538,10 @@ private string FullTypeName(UserDefinedType udt, MemberDecl/*?*/ member = null, return (cl.EnclosingModuleDefinition.TryToAvoidName ? "" : IdProtectModule(cl.EnclosingModuleDefinition.GetCompileName(Options)) + ".") + dataTypeName(cl as DatatypeDecl); } + if (cl is ClassDecl) { + return (cl.EnclosingModuleDefinition.TryToAvoidName ? "" : IdProtectModule(cl.EnclosingModuleDefinition.GetCompileName(Options)) + ".") + className(cl as ClassDecl); + } + if (cl.EnclosingModuleDefinition.TryToAvoidName) { return IdProtect(cl.GetCompileName(Options)); } diff --git a/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs b/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs index 04f08c8794..a6d2ba003c 100644 --- a/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs +++ b/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs @@ -226,9 +226,10 @@ private string InstantiateTemplate(List typeArgs) { protected override string GetHelperModuleName() => "_dafny"; - protected override IClassWriter CreateClass(string moduleName, string name, bool isExtern, string/*?*/ fullPrintName, List/*?*/ typeParameters, TopLevelDecl cls, List/*?*/ superClasses, IOrigin tok, ConcreteSyntaxTree wr) { + protected override IClassWriter CreateClass(string moduleName, TopLevelDecl cl, bool isExtern, string/*?*/ fullPrintName, List/*?*/ typeParameters, TopLevelDecl cls, List/*?*/ superClasses, IOrigin tok, ConcreteSyntaxTree wr) { + var className = "class_" + IdName(cl); 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); @@ -242,17 +243,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 > {{\n", TypeParameters(typeParameters), fullName, @@ -266,7 +267,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; } @@ -615,8 +616,8 @@ protected override IClassWriter DeclareNewtype(NewtypeDecl nt, ConcreteSyntaxTre } else { throw new UnsupportedFeatureException(nt.Origin, Feature.NonNativeNewtypes); } + var cw = CreateClass(nt.EnclosingModuleDefinition.GetCompileName(Options), nt, nt, wr) as ClassWriter; var className = "class_" + IdName(nt); - var cw = CreateClass(nt.EnclosingModuleDefinition.GetCompileName(Options), className, nt, wr) as ClassWriter; var w = cw.MethodDeclWriter; if (nt.WitnessKind == SubsetTypeDecl.WKind.Compiled) { var witness = new ConcreteSyntaxTree(w.RelativeIndentLevel); @@ -653,8 +654,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 cw = CreateClass(sst.EnclosingModuleDefinition.GetCompileName(Options), sst, sst, wr) as ClassWriter; var className = "class_" + IdName(sst); - var cw = CreateClass(sst.EnclosingModuleDefinition.GetCompileName(Options), className, sst, wr) as ClassWriter; var w = cw.MethodDeclWriter; if (sst.WitnessKind == SubsetTypeDecl.WKind.Compiled) { diff --git a/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs b/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs index 05b0ba6a85..80b8b9e45f 100644 --- a/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs +++ b/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs @@ -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, TopLevelDecl cl, bool isExtern, string fullPrintName, List typeParameters, TopLevelDecl cls, List superClasses, IOrigin tok, ConcreteSyntaxTree wr) { if (currentBuilder is ClassContainer builder) { List 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(cl), moduleName, typeParams, superClasses.Select(t => GenType(t)).ToList(), ParseAttributes(cls.Attributes), GetDocString(cls)) ); } else { diff --git a/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs b/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs index edbeb76c7c..0f854146b7 100644 --- a/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs +++ b/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs @@ -329,16 +329,16 @@ private void EmitImport(Import import, ConcreteSyntaxTree importWriter, Concrete private string HelperModulePrefix => ModuleName == "dafny" ? "" : $"{GetHelperModuleName()}."; - protected override IClassWriter CreateClass(string moduleName, string name, bool isExtern, string/*?*/ fullPrintName, + protected override IClassWriter CreateClass(string moduleName, TopLevelDecl cl, bool isExtern, string/*?*/ fullPrintName, List typeParameters, TopLevelDecl cls, List/*?*/ superClasses, IOrigin tok, ConcreteSyntaxTree wr) { var isDefaultClass = cls is DefaultClassDecl; bool isSequence = superClasses.Any(superClass => superClass is UserDefinedType udt && IsDafnySequence(udt.ResolvedClass)); - return CreateClass(cls, name, isExtern, fullPrintName, typeParameters, superClasses, tok, wr, includeRtd: !isDefaultClass, includeEquals: !isSequence, includeString: !isSequence); + return CreateClass(cls, cl, isExtern, fullPrintName, typeParameters, superClasses, tok, wr, includeRtd: !isDefaultClass, includeEquals: !isSequence, includeString: !isSequence); } // TODO Consider splitting this into two functions; most things seem to be passing includeRtd: false, includeEquals: false and includeString: true. - private GoCodeGenerator.ClassWriter CreateClass(TopLevelDecl classContext, string name, bool isExtern, string/*?*/ fullPrintName, List/*?*/ typeParameters, List/*?*/ superClasses, IOrigin tok, ConcreteSyntaxTree wr, bool includeRtd, bool includeEquals, bool includeString) { + private GoCodeGenerator.ClassWriter CreateClass(TopLevelDecl classContext, TopLevelDecl cl, bool isExtern, string/*?*/ fullPrintName, List/*?*/ typeParameters, List/*?*/ superClasses, IOrigin tok, ConcreteSyntaxTree wr, bool includeRtd, bool includeEquals, bool includeString) { // See docs/Compilation/ReferenceTypes.md for a description of how instance members of classes and traits are compiled into Go. // // func New_Class_(Type0 _dafny.TypeDescriptor, Type1 _dafny.TypeDescriptor) *Class { @@ -382,7 +382,7 @@ private GoCodeGenerator.ClassWriter CreateClass(TopLevelDecl classContext, strin // return "module.Class" // } // - name = Capitalize(name); + var name = Capitalize(IdName(cl)); var w = CreateDescribedSection("class {0}", wr, name); @@ -586,7 +586,7 @@ protected override ConcreteSyntaxTree CreateIterator(IteratorDecl iter, Concrete // // break becomes: // return // }() - var cw = CreateClass(iter, IdName(iter), false, null, iter.TypeArgs, null, null, wr, includeRtd: false, includeEquals: false, includeString: true); + var cw = CreateClass(iter, iter, false, null, iter.TypeArgs, null, null, wr, includeRtd: false, includeEquals: false, includeString: true); cw.InstanceFieldWriter.WriteLine("cont chan<- struct{}"); cw.InstanceFieldWriter.WriteLine("yielded <-chan struct{}"); @@ -1084,7 +1084,7 @@ string StructOfCtor(DatatypeCtor ctor) { } protected override IClassWriter DeclareNewtype(NewtypeDecl nt, ConcreteSyntaxTree wr) { - var cw = CreateClass(nt, IdName(nt), false, null, nt.TypeArgs, + var cw = CreateClass(nt, nt, false, null, nt.TypeArgs, nt.ParentTypeInformation.UniqueParentTraits(), null, wr, includeRtd: false, includeEquals: false, includeString: true); var w = cw.ConcreteMethodWriter; var nativeType = nt.NativeType != null ? GetNativeTypeName(nt.NativeType) : null; @@ -1130,7 +1130,7 @@ protected override IClassWriter DeclareNewtype(NewtypeDecl nt, ConcreteSyntaxTre } protected override void DeclareSubsetType(SubsetTypeDecl sst, ConcreteSyntaxTree wr) { - var cw = CreateClass(sst, IdName(sst), false, null, sst.TypeArgs, null, null, wr, includeRtd: false, includeEquals: false, includeString: true); + var cw = CreateClass(sst, sst, false, null, sst.TypeArgs, null, null, wr, includeRtd: false, includeEquals: false, includeString: true); var w = cw.ConcreteMethodWriter; if (sst.WitnessKind == SubsetTypeDecl.WKind.Compiled) { var witness = new ConcreteSyntaxTree(w.RelativeIndentLevel); diff --git a/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs b/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs index 868393dc65..e71ef393c2 100644 --- a/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs +++ b/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs @@ -373,7 +373,7 @@ protected override void FinishModule() { } 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, sst, wr); if (sst.WitnessKind == SubsetTypeDecl.WKind.Compiled) { var sw = new ConcreteSyntaxTree(cw.InstanceMemberWriter.RelativeIndentLevel); var wStmts = cw.InstanceMemberWriter.Fork(); @@ -870,8 +870,9 @@ protected override string TypeName_UDT(string fullCompileName, List typeParameters, TopLevelDecl cls, List /*?*/ superClasses, IOrigin tok, ConcreteSyntaxTree wr) { + var name = IdName(cl); var javaName = isExtern ? FormatExternBaseClassName(name) : name; var filename = $"{ModulePath}/{javaName}.java"; var w = wr.NewFile(filename); @@ -3601,7 +3602,7 @@ protected override void EmitHalt(IOrigin tok, Expression messageExpr, ConcreteSy } 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, nt, wr); var w = cw.StaticMemberWriter; if (nt.NativeType != null) { var nativeType = GetBoxedNativeTypeName(nt.NativeType); diff --git a/Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs b/Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs index 5593c74501..56b7cde5de 100644 --- a/Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs +++ b/Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs @@ -90,8 +90,9 @@ protected override ConcreteSyntaxTree CreateModule(ModuleDefinition module, stri protected override string GetHelperModuleName() => "_dafny"; - protected override IClassWriter CreateClass(string moduleName, string name, bool isExtern, string/*?*/ fullPrintName, + protected override IClassWriter CreateClass(string moduleName, TopLevelDecl cl, bool isExtern, string/*?*/ fullPrintName, List typeParameters, TopLevelDecl cls, List/*?*/ superClasses, IOrigin tok, ConcreteSyntaxTree wr) { + var name = IdName(cl); var w = wr.NewBlock(string.Format("$module.{0} = class {0}" + (isExtern ? " extends $module.{0}" : ""), name), ";"); w.Write("constructor ("); var sep = ""; @@ -160,7 +161,7 @@ protected override ConcreteSyntaxTree CreateIterator(IteratorDecl iter, Concrete // } // } - var cw = CreateClass(IdProtect(iter.EnclosingModuleDefinition.GetCompileName(Options)), IdName(iter), iter, wr) as JavaScriptCodeGenerator.ClassWriter; + var cw = CreateClass(IdProtect(iter.EnclosingModuleDefinition.GetCompileName(Options)), iter, iter, wr) as JavaScriptCodeGenerator.ClassWriter; var w = cw.MethodWriter; var instanceFieldsWriter = cw.FieldWriter; // here come the fields @@ -575,7 +576,7 @@ protected override ConcreteSyntaxTree CreateIterator(IteratorDecl iter, Concrete } 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, nt, wr); var w = cw.MethodWriter; if (nt.NativeType != null) { var wIntegerRangeBody = w.NewBlock("static *IntegerRange(lo, hi)"); @@ -638,7 +639,7 @@ void GenerateIsMethod(RedirectingTypeDecl declWithConstraints, ConcreteSyntaxTre } 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, sst, wr); var w = cw.MethodWriter; var udt = UserDefinedType.FromTopLevelDecl(sst.Origin, sst); string d; diff --git a/Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs b/Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs index 7654c96ec0..f322c10823 100644 --- a/Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs +++ b/Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs @@ -231,12 +231,13 @@ private static string MangleName(string name) { return name; } - protected override IClassWriter CreateClass(string moduleName, string name, bool isExtern, string/*?*/ fullPrintName, + protected override IClassWriter CreateClass(string moduleName, TopLevelDecl cl, bool isExtern, string/*?*/ fullPrintName, List typeParameters, TopLevelDecl cls, List superClasses, IOrigin tok, ConcreteSyntaxTree wr) { var realSuperClasses = superClasses?.Where(trait => !trait.IsObject).ToList() ?? new List(); var baseClasses = realSuperClasses.Any() ? $"({realSuperClasses.Comma(trait => TypeName(trait, wr, tok))})" : ""; + var name = IdName(cl); var methodWriter = wr.NewBlockPy(header: $"class {IdProtect(name)}{baseClasses}:"); var relevantTypeParameters = typeParameters.Where(NeedsTypeDescriptor).ToList(); @@ -276,7 +277,7 @@ protected override IClassWriter CreateTrait(string name, bool isExtern, List true; protected virtual bool TraitRepeatsInheritedDeclarations => false; protected virtual bool InstanceMethodsAllowedToCallTraitMethods => true; - protected IClassWriter CreateClass(string moduleName, string name, TopLevelDecl cls, ConcreteSyntaxTree wr) { - return CreateClass(moduleName, name, false, null, cls.TypeArgs, + protected IClassWriter CreateClass(string moduleName, TopLevelDecl cl, TopLevelDecl cls, ConcreteSyntaxTree wr) { + return CreateClass(moduleName, cl, false, null, cls.TypeArgs, cls, (cls as TopLevelDeclWithMembers)?.ParentTypeInformation.UniqueParentTraits(), null, wr); } /// /// "tok" can be "null" if "superClasses" is. /// - protected abstract IClassWriter CreateClass(string moduleName, string name, bool isExtern, string/*?*/ fullPrintName, + protected abstract IClassWriter CreateClass(string moduleName, TopLevelDecl cl, bool isExtern, string/*?*/ fullPrintName, List typeParameters, TopLevelDecl cls, List/*?*/ superClasses, IOrigin tok, ConcreteSyntaxTree wr); /// @@ -1685,7 +1685,7 @@ private void EmitModule(Program program, ConcreteSyntaxTree programNode, ModuleD if (include) { var cw = CreateClass(IdProtect(d.EnclosingModuleDefinition.GetCompileName(Options)), - IdName(defaultClassDecl), + defaultClassDecl, classIsExtern, defaultClassDecl.FullName, defaultClassDecl.TypeArgs, defaultClassDecl, defaultClassDecl.ParentTypeInformation.UniqueParentTraits(), defaultClassDecl.Origin, wr); @@ -1700,7 +1700,7 @@ private void EmitModule(Program program, ConcreteSyntaxTree programNode, ModuleD var (classIsExtern, include) = GetIsExternAndIncluded(cl); if (include) { - var cw = CreateClass(IdProtect(d.EnclosingModuleDefinition.GetCompileName(Options)), IdName(cl), + var cw = CreateClass(IdProtect(d.EnclosingModuleDefinition.GetCompileName(Options)), cl, classIsExtern, cl.FullName, cl.TypeArgs, cl, cl.ParentTypeInformation.UniqueParentTraits(), cl.Origin, wr); CompileClassMembers(program, cl, cw); diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-6014.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-6014.dfy index 5965e1212f..a01c94e4c3 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-6014.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-6014.dfy @@ -15,4 +15,47 @@ module Foo { method Main() { print "Hello!\n"; } -} \ No newline at end of file +} + +module Enclosing { + + module A { + datatype A = Whatever + } + +} + +module UsingEnclosing { + + import opened Enclosing + + const bar: A.A + + method Main2() { + print "Hello!\n"; + } +} + +module A { + + trait T { + var a: X + } + + class A extends T { + var x : int + constructor() {x := 0;} + } + +} + +module UsingA { + + import opened A + + method Main() { + var b := new A(); + + print "Hello!\n"; + } +} From f7e149270ad2dd0d382aeaecc3b83cb4cdce3c29 Mon Sep 17 00:00:00 2001 From: Olivier Bouissou Date: Tue, 7 Jan 2025 17:28:55 -0500 Subject: [PATCH 13/45] Whitespace formatting --- Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs b/Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs index 56b7cde5de..2ce752f965 100644 --- a/Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs +++ b/Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs @@ -92,7 +92,7 @@ protected override ConcreteSyntaxTree CreateModule(ModuleDefinition module, stri protected override IClassWriter CreateClass(string moduleName, TopLevelDecl cl, bool isExtern, string/*?*/ fullPrintName, List typeParameters, TopLevelDecl cls, List/*?*/ superClasses, IOrigin tok, ConcreteSyntaxTree wr) { - var name = IdName(cl); + var name = IdName(cl); var w = wr.NewBlock(string.Format("$module.{0} = class {0}" + (isExtern ? " extends $module.{0}" : ""), name), ";"); w.Write("constructor ("); var sep = ""; From 057771aad03bc492f3fd6df8c2320a341ec556f4 Mon Sep 17 00:00:00 2001 From: Olivier Bouissou Date: Wed, 8 Jan 2025 09:18:21 -0500 Subject: [PATCH 14/45] Fix cpp code generation and test --- .../Backends/Cplusplus/CppCodeGenerator.cs | 24 +++++++++++-------- .../LitTest/git-issues/git-issue-6014.dfy | 2 +- 2 files changed, 15 insertions(+), 11 deletions(-) diff --git a/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs b/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs index a6d2ba003c..d9381c1649 100644 --- a/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs +++ b/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs @@ -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;"); } @@ -226,8 +226,12 @@ private string InstantiateTemplate(List typeArgs) { protected override string GetHelperModuleName() => "_dafny"; + private string clName(TopLevelDecl cl) { + return "class_" + IdName(cl); + } + protected override IClassWriter CreateClass(string moduleName, TopLevelDecl cl, bool isExtern, string/*?*/ fullPrintName, List/*?*/ typeParameters, TopLevelDecl cls, List/*?*/ superClasses, IOrigin tok, ConcreteSyntaxTree wr) { - var className = "class_" + IdName(cl); + var className = clName(cl); if (isExtern) { throw new UnsupportedFeatureException(tok, Feature.ExternalClasses, String.Format("extern in class {0}", className)); } @@ -444,7 +448,7 @@ protected override IClassWriter DeclareDatatype(DatatypeDecl dt, ConcreteSyntaxT // Overload the not-comparison operator wstruct.WriteLine("friend bool operator!=(const {0} &left, const {0} &right) {{ return !(left == right); }} ", structName); - // Define a custom hasher + // Define a custom hasherGetCompileName hashWr.WriteLine("template <{0}>", TypeParameters(dt.TypeArgs)); var fullName = dt.EnclosingModuleDefinition.GetCompileName(Options) + "::" + structName + InstantiateTemplate(dt.TypeArgs); var hwr = hashWr.NewBlock(string.Format("struct std::hash<{0}>", fullName), ";"); @@ -617,7 +621,7 @@ protected override IClassWriter DeclareNewtype(NewtypeDecl nt, ConcreteSyntaxTre throw new UnsupportedFeatureException(nt.Origin, Feature.NonNativeNewtypes); } var cw = CreateClass(nt.EnclosingModuleDefinition.GetCompileName(Options), nt, nt, wr) as ClassWriter; - var className = "class_" + IdName(nt); + var className = clName(nt); var w = cw.MethodDeclWriter; if (nt.WitnessKind == SubsetTypeDecl.WKind.Compiled) { var witness = new ConcreteSyntaxTree(w.RelativeIndentLevel); @@ -655,7 +659,7 @@ 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 cw = CreateClass(sst.EnclosingModuleDefinition.GetCompileName(Options), sst, sst, wr) as ClassWriter; - var className = "class_" + IdName(sst); + var className = clName(sst); var w = cw.MethodDeclWriter; if (sst.WitnessKind == SubsetTypeDecl.WKind.Compiled) { @@ -786,7 +790,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)); @@ -1044,7 +1048,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 { @@ -1053,7 +1057,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); @@ -1763,14 +1767,14 @@ protected override ILvalue EmitMemberSelect(Action 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); } else if (member is SpecialField sf2 && sf2.SpecialId == SpecialField.ID.UseIdParam && sf2.IdParam is string fieldName && fieldName.StartsWith("is_")) { // Ugly hack of a check to figure out if this is a datatype query: f.Constructor? - return SuffixLvalue(obj, ".is_{0}_{1}()", IdProtect(sf2.EnclosingClass.GetCompileName(Options)), fieldName.Substring(3)); + return SuffixLvalue(obj, ".is_{0}_{1}()", IdProtect(clName(sf2.EnclosingClass)), fieldName.Substring(3)); } else if (member is SpecialField sf) { GetSpecialFieldInfo(sf.SpecialId, sf.IdParam, objType, out var compiledName, out var preStr, out var postStr); if (sf.SpecialId == SpecialField.ID.Keys || sf.SpecialId == SpecialField.ID.Values) { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-6014.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-6014.dfy index a01c94e4c3..b43e78bfeb 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-6014.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-6014.dfy @@ -53,7 +53,7 @@ module UsingA { import opened A - method Main() { + method Main3() { var b := new A(); print "Hello!\n"; From 72d4da6b38ab235973b3f1481c21068d067985f4 Mon Sep 17 00:00:00 2001 From: Olivier Bouissou Date: Wed, 8 Jan 2025 11:47:29 -0500 Subject: [PATCH 15/45] Test for CPP compiler --- Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs b/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs index d9381c1649..dbf8d2c275 100644 --- a/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs +++ b/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs @@ -227,7 +227,11 @@ private string InstantiateTemplate(List typeArgs) { protected override string GetHelperModuleName() => "_dafny"; private string clName(TopLevelDecl cl) { - return "class_" + IdName(cl); + var className = IdName(cl); + if (className == "__default" || true) { + return className; + } + return "class_" + className; } protected override IClassWriter CreateClass(string moduleName, TopLevelDecl cl, bool isExtern, string/*?*/ fullPrintName, List/*?*/ typeParameters, TopLevelDecl cls, List/*?*/ superClasses, IOrigin tok, ConcreteSyntaxTree wr) { From 9244f8266fe313e5be165f18c3683ea2292f4cf7 Mon Sep 17 00:00:00 2001 From: Olivier Bouissou Date: Wed, 8 Jan 2025 13:22:18 -0500 Subject: [PATCH 16/45] Simplification to remove duplicate argument to CreateClass --- .../Backends/CSharp/CsharpCodeGenerator.cs | 10 +++++----- .../Backends/Cplusplus/CppCodeGenerator.cs | 10 +++++----- .../DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs | 4 ++-- .../DafnyCore/Backends/GoLang/GoCodeGenerator.cs | 14 +++++++------- .../DafnyCore/Backends/Java/JavaCodeGenerator.cs | 8 ++++---- .../Backends/JavaScript/JavaScriptCodeGenerator.cs | 10 +++++----- .../Backends/Python/PythonCodeGenerator.cs | 8 ++++---- .../SinglePassCodeGenerator.cs | 11 ++++++----- 8 files changed, 38 insertions(+), 37 deletions(-) diff --git a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs index c945b8e100..1afe19c97c 100644 --- a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs +++ b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs @@ -331,9 +331,9 @@ string PrintVariance(TypeParameter.TPVariance variance) { return $"<{targs.Comma(PrintTypeParameter)}>"; } - protected override IClassWriter CreateClass(string moduleName, TopLevelDecl tl, bool isExtern, string /*?*/ fullPrintName, + protected override IClassWriter CreateClass(string moduleName, bool isExtern, string /*?*/ fullPrintName, List typeParameters, TopLevelDecl cls, List/*?*/ superClasses, IOrigin tok, ConcreteSyntaxTree wr) { - var name = className(tl); + var name = className(cls); var wBody = WriteTypeHeader("partial class", name, typeParameters, superClasses, tok, wr); ConcreteSyntaxTree/*?*/ wCtorBody = null; @@ -469,7 +469,7 @@ protected override ConcreteSyntaxTree CreateIterator(IteratorDecl iter, Concrete // } // } - var cw = (ClassWriter)CreateClass(IdProtect(iter.EnclosingModuleDefinition.GetCompileName(Options)), iter, iter, wr); + var cw = (ClassWriter)CreateClass(IdProtect(iter.EnclosingModuleDefinition.GetCompileName(Options)), iter, wr); var w = cw.InstanceMemberWriter; // here come the fields @@ -1262,7 +1262,7 @@ string DtCreateName(DatatypeCtor ctor) { } protected override IClassWriter DeclareNewtype(NewtypeDecl nt, ConcreteSyntaxTree wr) { - var cw = (ClassWriter)CreateClass(IdProtect(nt.EnclosingModuleDefinition.GetCompileName(Options)), 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)"); @@ -1331,7 +1331,7 @@ void DeclareBoxedNewtype(NewtypeDecl nt, ConcreteSyntaxTree wr) { } protected override void DeclareSubsetType(SubsetTypeDecl sst, ConcreteSyntaxTree wr) { - var cw = (ClassWriter)CreateClass(IdProtect(sst.EnclosingModuleDefinition.GetCompileName(Options)), 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(); diff --git a/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs b/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs index dbf8d2c275..80f74a2071 100644 --- a/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs +++ b/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs @@ -228,14 +228,14 @@ private string InstantiateTemplate(List typeArgs) { private string clName(TopLevelDecl cl) { var className = IdName(cl); - if (className == "__default" || true) { + if (cl is ClassDecl || cl is DefaultClassDecl) { return className; } return "class_" + className; } - protected override IClassWriter CreateClass(string moduleName, TopLevelDecl cl, bool isExtern, string/*?*/ fullPrintName, List/*?*/ typeParameters, TopLevelDecl cls, List/*?*/ superClasses, IOrigin tok, ConcreteSyntaxTree wr) { - var className = clName(cl); + protected override IClassWriter CreateClass(string moduleName, bool isExtern, string/*?*/ fullPrintName, List/*?*/ typeParameters, TopLevelDecl cls, List/*?*/ superClasses, IOrigin tok, ConcreteSyntaxTree wr) { + var className = clName(cls); if (isExtern) { throw new UnsupportedFeatureException(tok, Feature.ExternalClasses, String.Format("extern in class {0}", className)); } @@ -624,7 +624,7 @@ protected override IClassWriter DeclareNewtype(NewtypeDecl nt, ConcreteSyntaxTre } else { throw new UnsupportedFeatureException(nt.Origin, Feature.NonNativeNewtypes); } - var cw = CreateClass(nt.EnclosingModuleDefinition.GetCompileName(Options), nt, 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) { @@ -662,7 +662,7 @@ 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 cw = CreateClass(sst.EnclosingModuleDefinition.GetCompileName(Options), sst, sst, wr) as ClassWriter; + var cw = CreateClass(sst.EnclosingModuleDefinition.GetCompileName(Options), sst, wr) as ClassWriter; var className = clName(sst); var w = cw.MethodDeclWriter; diff --git a/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs b/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs index 80b8b9e45f..ba17c4a4d1 100644 --- a/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs +++ b/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs @@ -193,13 +193,13 @@ protected override ConcreteSyntaxTree EmitCoercionIfNecessary(Type from, Type to } } - protected override IClassWriter CreateClass(string moduleName, TopLevelDecl cl, bool isExtern, string fullPrintName, + protected override IClassWriter CreateClass(string moduleName, bool isExtern, string fullPrintName, List typeParameters, TopLevelDecl cls, List superClasses, IOrigin tok, ConcreteSyntaxTree wr) { if (currentBuilder is ClassContainer builder) { List typeParams = typeParameters.Select(tp => GenTypeArgDecl(tp)).ToList(); return new ClassWriter(this, typeParams.Count > 0, builder.Class( - IdName(cl), moduleName, typeParams, superClasses.Select(t => GenType(t)).ToList(), + IdName(cls), moduleName, typeParams, superClasses.Select(t => GenType(t)).ToList(), ParseAttributes(cls.Attributes), GetDocString(cls)) ); } else { diff --git a/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs b/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs index 0f854146b7..953f7d4347 100644 --- a/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs +++ b/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs @@ -329,16 +329,16 @@ private void EmitImport(Import import, ConcreteSyntaxTree importWriter, Concrete private string HelperModulePrefix => ModuleName == "dafny" ? "" : $"{GetHelperModuleName()}."; - protected override IClassWriter CreateClass(string moduleName, TopLevelDecl cl, bool isExtern, string/*?*/ fullPrintName, + protected override IClassWriter CreateClass(string moduleName, bool isExtern, string/*?*/ fullPrintName, List typeParameters, TopLevelDecl cls, List/*?*/ superClasses, IOrigin tok, ConcreteSyntaxTree wr) { var isDefaultClass = cls is DefaultClassDecl; bool isSequence = superClasses.Any(superClass => superClass is UserDefinedType udt && IsDafnySequence(udt.ResolvedClass)); - return CreateClass(cls, cl, isExtern, fullPrintName, typeParameters, superClasses, tok, wr, includeRtd: !isDefaultClass, includeEquals: !isSequence, includeString: !isSequence); + return CreateClass(cls, isExtern, fullPrintName, typeParameters, superClasses, tok, wr, includeRtd: !isDefaultClass, includeEquals: !isSequence, includeString: !isSequence); } // TODO Consider splitting this into two functions; most things seem to be passing includeRtd: false, includeEquals: false and includeString: true. - private GoCodeGenerator.ClassWriter CreateClass(TopLevelDecl classContext, TopLevelDecl cl, bool isExtern, string/*?*/ fullPrintName, List/*?*/ typeParameters, List/*?*/ superClasses, IOrigin tok, ConcreteSyntaxTree wr, bool includeRtd, bool includeEquals, bool includeString) { + private GoCodeGenerator.ClassWriter CreateClass(TopLevelDecl classContext, bool isExtern, string/*?*/ fullPrintName, List/*?*/ typeParameters, List/*?*/ superClasses, IOrigin tok, ConcreteSyntaxTree wr, bool includeRtd, bool includeEquals, bool includeString) { // See docs/Compilation/ReferenceTypes.md for a description of how instance members of classes and traits are compiled into Go. // // func New_Class_(Type0 _dafny.TypeDescriptor, Type1 _dafny.TypeDescriptor) *Class { @@ -382,7 +382,7 @@ private GoCodeGenerator.ClassWriter CreateClass(TopLevelDecl classContext, TopLe // return "module.Class" // } // - var name = Capitalize(IdName(cl)); + var name = Capitalize(IdName(classContext)); var w = CreateDescribedSection("class {0}", wr, name); @@ -586,7 +586,7 @@ protected override ConcreteSyntaxTree CreateIterator(IteratorDecl iter, Concrete // // break becomes: // return // }() - var cw = CreateClass(iter, iter, false, null, iter.TypeArgs, null, null, wr, includeRtd: false, includeEquals: false, includeString: true); + var cw = CreateClass(iter, false, null, iter.TypeArgs, null, null, wr, includeRtd: false, includeEquals: false, includeString: true); cw.InstanceFieldWriter.WriteLine("cont chan<- struct{}"); cw.InstanceFieldWriter.WriteLine("yielded <-chan struct{}"); @@ -1084,7 +1084,7 @@ string StructOfCtor(DatatypeCtor ctor) { } protected override IClassWriter DeclareNewtype(NewtypeDecl nt, ConcreteSyntaxTree wr) { - var cw = CreateClass(nt, nt, false, null, nt.TypeArgs, + var cw = CreateClass(nt, false, null, nt.TypeArgs, nt.ParentTypeInformation.UniqueParentTraits(), null, wr, includeRtd: false, includeEquals: false, includeString: true); var w = cw.ConcreteMethodWriter; var nativeType = nt.NativeType != null ? GetNativeTypeName(nt.NativeType) : null; @@ -1130,7 +1130,7 @@ protected override IClassWriter DeclareNewtype(NewtypeDecl nt, ConcreteSyntaxTre } protected override void DeclareSubsetType(SubsetTypeDecl sst, ConcreteSyntaxTree wr) { - var cw = CreateClass(sst, sst, false, null, sst.TypeArgs, null, null, wr, includeRtd: false, includeEquals: false, includeString: true); + var cw = CreateClass(sst, false, null, sst.TypeArgs, null, null, wr, includeRtd: false, includeEquals: false, includeString: true); var w = cw.ConcreteMethodWriter; if (sst.WitnessKind == SubsetTypeDecl.WKind.Compiled) { var witness = new ConcreteSyntaxTree(w.RelativeIndentLevel); diff --git a/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs b/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs index e71ef393c2..88a80e524e 100644 --- a/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs +++ b/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs @@ -373,7 +373,7 @@ protected override void FinishModule() { } protected override void DeclareSubsetType(SubsetTypeDecl sst, ConcreteSyntaxTree wr) { - var cw = (ClassWriter)CreateClass(IdProtect(sst.EnclosingModuleDefinition.GetCompileName(Options)), 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(); @@ -870,9 +870,9 @@ protected override string TypeName_UDT(string fullCompileName, List typeParameters, TopLevelDecl cls, List /*?*/ superClasses, IOrigin tok, ConcreteSyntaxTree wr) { - var name = IdName(cl); + var name = IdName(cls); var javaName = isExtern ? FormatExternBaseClassName(name) : name; var filename = $"{ModulePath}/{javaName}.java"; var w = wr.NewFile(filename); @@ -3602,7 +3602,7 @@ protected override void EmitHalt(IOrigin tok, Expression messageExpr, ConcreteSy } protected override IClassWriter DeclareNewtype(NewtypeDecl nt, ConcreteSyntaxTree wr) { - var cw = (ClassWriter)CreateClass(IdProtect(nt.EnclosingModuleDefinition.GetCompileName(Options)), nt, nt, wr); + var cw = (ClassWriter)CreateClass(IdProtect(nt.EnclosingModuleDefinition.GetCompileName(Options)), nt, wr); var w = cw.StaticMemberWriter; if (nt.NativeType != null) { var nativeType = GetBoxedNativeTypeName(nt.NativeType); diff --git a/Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs b/Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs index 2ce752f965..a75fd312f4 100644 --- a/Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs +++ b/Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs @@ -90,9 +90,9 @@ protected override ConcreteSyntaxTree CreateModule(ModuleDefinition module, stri protected override string GetHelperModuleName() => "_dafny"; - protected override IClassWriter CreateClass(string moduleName, TopLevelDecl cl, bool isExtern, string/*?*/ fullPrintName, + protected override IClassWriter CreateClass(string moduleName, bool isExtern, string/*?*/ fullPrintName, List typeParameters, TopLevelDecl cls, List/*?*/ superClasses, IOrigin tok, ConcreteSyntaxTree wr) { - var name = IdName(cl); + var name = IdName(cls); var w = wr.NewBlock(string.Format("$module.{0} = class {0}" + (isExtern ? " extends $module.{0}" : ""), name), ";"); w.Write("constructor ("); var sep = ""; @@ -161,7 +161,7 @@ protected override ConcreteSyntaxTree CreateIterator(IteratorDecl iter, Concrete // } // } - var cw = CreateClass(IdProtect(iter.EnclosingModuleDefinition.GetCompileName(Options)), iter, iter, wr) as JavaScriptCodeGenerator.ClassWriter; + var cw = CreateClass(IdProtect(iter.EnclosingModuleDefinition.GetCompileName(Options)), iter, wr) as JavaScriptCodeGenerator.ClassWriter; var w = cw.MethodWriter; var instanceFieldsWriter = cw.FieldWriter; // here come the fields @@ -576,7 +576,7 @@ protected override ConcreteSyntaxTree CreateIterator(IteratorDecl iter, Concrete } protected override IClassWriter DeclareNewtype(NewtypeDecl nt, ConcreteSyntaxTree wr) { - var cw = (ClassWriter)CreateClass(IdProtect(nt.EnclosingModuleDefinition.GetCompileName(Options)), nt, nt, wr); + var cw = (ClassWriter)CreateClass(IdProtect(nt.EnclosingModuleDefinition.GetCompileName(Options)), nt, wr); var w = cw.MethodWriter; if (nt.NativeType != null) { var wIntegerRangeBody = w.NewBlock("static *IntegerRange(lo, hi)"); @@ -639,7 +639,7 @@ void GenerateIsMethod(RedirectingTypeDecl declWithConstraints, ConcreteSyntaxTre } protected override void DeclareSubsetType(SubsetTypeDecl sst, ConcreteSyntaxTree wr) { - var cw = (ClassWriter)CreateClass(IdProtect(sst.EnclosingModuleDefinition.GetCompileName(Options)), sst, sst, wr); + var cw = (ClassWriter)CreateClass(IdProtect(sst.EnclosingModuleDefinition.GetCompileName(Options)), sst, wr); var w = cw.MethodWriter; var udt = UserDefinedType.FromTopLevelDecl(sst.Origin, sst); string d; diff --git a/Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs b/Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs index f322c10823..e95837a998 100644 --- a/Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs +++ b/Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs @@ -231,13 +231,13 @@ private static string MangleName(string name) { return name; } - protected override IClassWriter CreateClass(string moduleName, TopLevelDecl cl, bool isExtern, string/*?*/ fullPrintName, + protected override IClassWriter CreateClass(string moduleName, bool isExtern, string/*?*/ fullPrintName, List typeParameters, TopLevelDecl cls, List superClasses, IOrigin tok, ConcreteSyntaxTree wr) { var realSuperClasses = superClasses?.Where(trait => !trait.IsObject).ToList() ?? new List(); var baseClasses = realSuperClasses.Any() ? $"({realSuperClasses.Comma(trait => TypeName(trait, wr, tok))})" : ""; - var name = IdName(cl); + var name = IdName(cls); var methodWriter = wr.NewBlockPy(header: $"class {IdProtect(name)}{baseClasses}:"); var relevantTypeParameters = typeParameters.Where(NeedsTypeDescriptor).ToList(); @@ -277,7 +277,7 @@ protected override IClassWriter CreateTrait(string name, bool isExtern, List true; protected virtual bool TraitRepeatsInheritedDeclarations => false; protected virtual bool InstanceMethodsAllowedToCallTraitMethods => true; - protected IClassWriter CreateClass(string moduleName, TopLevelDecl cl, TopLevelDecl cls, ConcreteSyntaxTree wr) { - return CreateClass(moduleName, cl, false, null, cls.TypeArgs, + protected IClassWriter CreateClass(string moduleName, TopLevelDecl cls, ConcreteSyntaxTree wr) { + return CreateClass(moduleName, false, null, cls.TypeArgs, cls, (cls as TopLevelDeclWithMembers)?.ParentTypeInformation.UniqueParentTraits(), null, wr); } /// /// "tok" can be "null" if "superClasses" is. /// - protected abstract IClassWriter CreateClass(string moduleName, TopLevelDecl cl, bool isExtern, string/*?*/ fullPrintName, + protected abstract IClassWriter CreateClass(string moduleName, bool isExtern, string/*?*/ fullPrintName, List typeParameters, TopLevelDecl cls, List/*?*/ superClasses, IOrigin tok, ConcreteSyntaxTree wr); /// @@ -1684,8 +1684,8 @@ private void EmitModule(Program program, ConcreteSyntaxTree programNode, ModuleD var (classIsExtern, include) = GetIsExternAndIncluded(defaultClassDecl); if (include) { + // HERE: was using IdName(defaultClassDecl) as name, now using clName(defaultClassDecl) var cw = CreateClass(IdProtect(d.EnclosingModuleDefinition.GetCompileName(Options)), - defaultClassDecl, classIsExtern, defaultClassDecl.FullName, defaultClassDecl.TypeArgs, defaultClassDecl, defaultClassDecl.ParentTypeInformation.UniqueParentTraits(), defaultClassDecl.Origin, wr); @@ -1700,7 +1700,8 @@ private void EmitModule(Program program, ConcreteSyntaxTree programNode, ModuleD var (classIsExtern, include) = GetIsExternAndIncluded(cl); if (include) { - var cw = CreateClass(IdProtect(d.EnclosingModuleDefinition.GetCompileName(Options)), cl, + // HERE: was using IdName(cl) as name, now using clName(cl) + var cw = CreateClass(IdProtect(d.EnclosingModuleDefinition.GetCompileName(Options)), classIsExtern, cl.FullName, cl.TypeArgs, cl, cl.ParentTypeInformation.UniqueParentTraits(), cl.Origin, wr); CompileClassMembers(program, cl, cw); From 96a80135ad5727eafe692d15d0f35cfb6506078d Mon Sep 17 00:00:00 2001 From: Olivier Bouissou Date: Wed, 8 Jan 2025 14:32:09 -0500 Subject: [PATCH 17/45] Fix tests --- Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs | 9 +++++---- Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs | 2 +- 2 files changed, 6 insertions(+), 5 deletions(-) diff --git a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs index 1afe19c97c..0471384ae3 100644 --- a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs +++ b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs @@ -2538,10 +2538,6 @@ private string FullTypeName(UserDefinedType udt, MemberDecl/*?*/ member = null, return (cl.EnclosingModuleDefinition.TryToAvoidName ? "" : IdProtectModule(cl.EnclosingModuleDefinition.GetCompileName(Options)) + ".") + dataTypeName(cl as DatatypeDecl); } - if (cl is ClassDecl) { - return (cl.EnclosingModuleDefinition.TryToAvoidName ? "" : IdProtectModule(cl.EnclosingModuleDefinition.GetCompileName(Options)) + ".") + className(cl as ClassDecl); - } - if (cl.EnclosingModuleDefinition.TryToAvoidName) { return IdProtect(cl.GetCompileName(Options)); } @@ -2549,6 +2545,11 @@ private string FullTypeName(UserDefinedType udt, MemberDecl/*?*/ member = null, 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)) + ".") + className(cl as ClassDecl); + } + return IdProtectModule(cl.EnclosingModuleDefinition.GetCompileName(Options)) + "." + IdProtect(cl.GetCompileName(Options)); } diff --git a/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs b/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs index 80f74a2071..34a24125ca 100644 --- a/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs +++ b/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs @@ -1778,7 +1778,7 @@ protected override ILvalue EmitMemberSelect(Action obj, Type } else if (member is SpecialField sf2 && sf2.SpecialId == SpecialField.ID.UseIdParam && sf2.IdParam is string fieldName && fieldName.StartsWith("is_")) { // Ugly hack of a check to figure out if this is a datatype query: f.Constructor? - return SuffixLvalue(obj, ".is_{0}_{1}()", IdProtect(clName(sf2.EnclosingClass)), fieldName.Substring(3)); + return SuffixLvalue(obj, ".is_{0}_{1}()", IdProtect(sf2.EnclosingClass.GetCompileName(Options)), fieldName.Substring(3)); } else if (member is SpecialField sf) { GetSpecialFieldInfo(sf.SpecialId, sf.IdParam, objType, out var compiledName, out var preStr, out var postStr); if (sf.SpecialId == SpecialField.ID.Keys || sf.SpecialId == SpecialField.ID.Values) { From 7ce21043e7196d58d8f6a950e1bffcff0780428d Mon Sep 17 00:00:00 2001 From: Olivier Bouissou Date: Wed, 8 Jan 2025 14:34:12 -0500 Subject: [PATCH 18/45] Fixing expect file --- .../LitTests/LitTest/git-issues/git-issue-4449.dfy.expect | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4449.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4449.dfy.expect index 93a73046bc..dcab703fd3 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4449.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4449.dfy.expect @@ -1,3 +1,3 @@ AnyName.B -AnyName.AnyName +AnyName._AnyName done From 2a839d28c1c42cd4d65d5e10a675655f4d3477d0 Mon Sep 17 00:00:00 2001 From: Olivier Bouissou Date: Wed, 8 Jan 2025 16:14:35 -0500 Subject: [PATCH 19/45] Fix test 4449 --- .../LitTests/LitTest/git-issues/git-issue-4449.dfy.cs.check | 1 - .../LitTests/LitTest/git-issues/git-issue-4449.dfy.cs.expect | 3 +++ .../LitTests/LitTest/git-issues/git-issue-4449.dfy.java.check | 1 - 3 files changed, 3 insertions(+), 2 deletions(-) delete mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4449.dfy.cs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4449.dfy.cs.expect delete mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4449.dfy.java.check diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4449.dfy.cs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4449.dfy.cs.check deleted file mode 100644 index a8dfdf5ec1..0000000000 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4449.dfy.cs.check +++ /dev/null @@ -1 +0,0 @@ -CHECK: Failed to compile C# source code .* \ No newline at end of file diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4449.dfy.cs.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4449.dfy.cs.expect new file mode 100644 index 0000000000..dcab703fd3 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4449.dfy.cs.expect @@ -0,0 +1,3 @@ +AnyName.B +AnyName._AnyName +done diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4449.dfy.java.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4449.dfy.java.check deleted file mode 100644 index 6d927bd791..0000000000 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4449.dfy.java.check +++ /dev/null @@ -1 +0,0 @@ -CHECK: error: cannot find symbol \ No newline at end of file From 49cb0909f0e06f857da346e00d730c0a3c667023 Mon Sep 17 00:00:00 2001 From: Olivier Bouissou Date: Wed, 8 Jan 2025 16:14:51 -0500 Subject: [PATCH 20/45] Really fix test 4440 --- .../LitTests/LitTest/git-issues/git-issue-4449.dfy.expect | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4449.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4449.dfy.expect index dcab703fd3..93a73046bc 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4449.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4449.dfy.expect @@ -1,3 +1,3 @@ AnyName.B -AnyName._AnyName +AnyName.AnyName done From 389726692f5e22e47bf90b8971f898cc2517e7a9 Mon Sep 17 00:00:00 2001 From: olivier-aws Date: Thu, 9 Jan 2025 08:00:07 -0500 Subject: [PATCH 21/45] Update Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Mikaël Mayer --- Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs index 0471384ae3..c56cd1bbcb 100644 --- a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs +++ b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs @@ -270,7 +270,7 @@ protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw, string a /// private string dataTypeName(DatatypeDecl dt) { var protectedName = IdName(dt); - if (dt.EnclosingModuleDefinition is not null) { + if (dt.EnclosingModuleDefinition is { Name: var moduleName } && moduleName == protectedName) { var moduleName = IdProtectModule(dt.EnclosingModuleDefinition.Name); if (moduleName == protectedName) { return $"_{protectedName}"; From d311c332a9210cf03d125474a3b05aa8bb9d3894 Mon Sep 17 00:00:00 2001 From: Olivier Bouissou Date: Thu, 9 Jan 2025 08:01:37 -0500 Subject: [PATCH 22/45] Adding Default as a protected name --- Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs | 1 + 1 file changed, 1 insertion(+) diff --git a/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs b/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs index 868393dc65..8f5533399e 100644 --- a/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs +++ b/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs @@ -2439,6 +2439,7 @@ private static string PublicIdProtectAux(string name) { case "toString": case "equals": case "hashCode": + case "Default": return name + "_"; // TODO: figure out what to do here (C# uses @, Go uses _, JS uses _$$_) default: return name; // Package name is not a keyword, so it can be used From b000601930ca7265f18801308d39696e17edf35c Mon Sep 17 00:00:00 2001 From: Olivier Bouissou Date: Thu, 9 Jan 2025 08:12:35 -0500 Subject: [PATCH 23/45] Apply CR suggestions --- .../Backends/CSharp/CsharpCodeGenerator.cs | 39 +++++++------------ .../SinglePassCodeGenerator.cs | 2 - 2 files changed, 13 insertions(+), 28 deletions(-) diff --git a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs index c56cd1bbcb..16d30a6253 100644 --- a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs +++ b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs @@ -266,27 +266,14 @@ protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw, string a } /// - /// Compute the name of the class to use to translate a data-type + /// Compute the name of the class to use to translate a data-type or a class /// - private string dataTypeName(DatatypeDecl dt) { + private string protectedTypeName(TopLevelDecl dt) { var protectedName = IdName(dt); - if (dt.EnclosingModuleDefinition is { Name: var moduleName } && moduleName == protectedName) { - var moduleName = IdProtectModule(dt.EnclosingModuleDefinition.Name); + if (dt.EnclosingModuleDefinition is { Name: var moduleName } && moduleName == protectedName) if (moduleName == protectedName) { return $"_{protectedName}"; } - } - return protectedName; - } - - private string className(TopLevelDecl dt) { - var protectedName = IdName(dt); - if (dt.EnclosingModuleDefinition is not null) { - var moduleName = IdProtectModule(dt.EnclosingModuleDefinition.Name); - if (moduleName == protectedName) { - return $"_{protectedName}"; - } - } return protectedName; } @@ -333,7 +320,7 @@ string PrintVariance(TypeParameter.TPVariance variance) { protected override IClassWriter CreateClass(string moduleName, bool isExtern, string /*?*/ fullPrintName, List typeParameters, TopLevelDecl cls, List/*?*/ superClasses, IOrigin tok, ConcreteSyntaxTree wr) { - var name = className(cls); + var name = protectedTypeName(cls); var wBody = WriteTypeHeader("partial class", name, typeParameters, superClasses, tok, wr); ConcreteSyntaxTree/*?*/ wCtorBody = null; @@ -586,7 +573,7 @@ IClassWriter CompileDatatypeBase(DatatypeDecl dt, ConcreteSyntaxTree wr) { // } var nonGhostTypeArgs = SelectNonGhost(dt, dt.TypeArgs); var DtT_TypeArgs = TypeParameters(nonGhostTypeArgs); - var DtT_protected = dataTypeName(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); @@ -608,7 +595,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 {dataTypeName(dt)}({wCtorParams})").NewBlock().Append(wCtorBody); + wr.Format($"public {protectedTypeName(dt)}({wCtorParams})").NewBlock().Append(wCtorBody); } var wDefault = new ConcreteSyntaxTree(); @@ -1022,7 +1009,7 @@ private void CompileDatatypeConstructors(DatatypeDecl dt, ConcreteSyntaxTree wrx // public override _IDt _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} : {dataTypeName(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;"); @@ -1044,7 +1031,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)} : {dataTypeName(dt)}{typeParams}"); + $"public class {DtCtorDeclarationName(ctor)}{TypeParameters(nonGhostTypeArgs)} : {protectedTypeName(dt)}{typeParams}"); DatatypeFieldsAndConstructor(ctor, constructorIndex, wr); constructorIndex++; } @@ -1218,7 +1205,7 @@ string DtCtorDeclarationName(DatatypeCtor ctor) { Contract.Ensures(Contract.Result() != null); var dt = ctor.EnclosingDatatype; - return dt.IsRecordType ? dataTypeName(dt) : dt.GetCompileName(Options) + "_" + ctor.GetCompileName(Options); + return dt.IsRecordType ? protectedTypeName(dt) : dt.GetCompileName(Options) + "_" + ctor.GetCompileName(Options); } /// @@ -1244,7 +1231,7 @@ string DtCtorName(DatatypeCtor ctor) { Contract.Ensures(Contract.Result() != null); var dt = ctor.EnclosingDatatype; - var dtName = dataTypeName(dt); + var dtName = protectedTypeName(dt); if (!dt.EnclosingModuleDefinition.TryToAvoidName) { dtName = IdProtectModule(dt.EnclosingModuleDefinition.GetCompileName(Options)) + "." + dtName; } @@ -2535,7 +2522,7 @@ private string FullTypeName(UserDefinedType udt, MemberDecl/*?*/ member = null, } if (cl is DatatypeDecl) { - return (cl.EnclosingModuleDefinition.TryToAvoidName ? "" : IdProtectModule(cl.EnclosingModuleDefinition.GetCompileName(Options)) + ".") + dataTypeName(cl as DatatypeDecl); + return (cl.EnclosingModuleDefinition.TryToAvoidName ? "" : IdProtectModule(cl.EnclosingModuleDefinition.GetCompileName(Options)) + ".") + protectedTypeName(cl as DatatypeDecl); } if (cl.EnclosingModuleDefinition.TryToAvoidName) { @@ -2547,7 +2534,7 @@ private string FullTypeName(UserDefinedType udt, MemberDecl/*?*/ member = null, } if (cl is ClassDecl) { - return (cl.EnclosingModuleDefinition.TryToAvoidName ? "" : IdProtectModule(cl.EnclosingModuleDefinition.GetCompileName(Options)) + ".") + className(cl as ClassDecl); + return (cl.EnclosingModuleDefinition.TryToAvoidName ? "" : IdProtectModule(cl.EnclosingModuleDefinition.GetCompileName(Options)) + ".") + protectedTypeName(cl as ClassDecl); } return IdProtectModule(cl.EnclosingModuleDefinition.GetCompileName(Options)) + "." + IdProtect(cl.GetCompileName(Options)); @@ -2564,7 +2551,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)) + "." + dataTypeName(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)}>"; diff --git a/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs index 73344cf161..0d3c5a7b5f 100644 --- a/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs +++ b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs @@ -1684,7 +1684,6 @@ private void EmitModule(Program program, ConcreteSyntaxTree programNode, ModuleD var (classIsExtern, include) = GetIsExternAndIncluded(defaultClassDecl); if (include) { - // HERE: was using IdName(defaultClassDecl) as name, now using clName(defaultClassDecl) var cw = CreateClass(IdProtect(d.EnclosingModuleDefinition.GetCompileName(Options)), classIsExtern, defaultClassDecl.FullName, defaultClassDecl.TypeArgs, defaultClassDecl, @@ -1700,7 +1699,6 @@ private void EmitModule(Program program, ConcreteSyntaxTree programNode, ModuleD var (classIsExtern, include) = GetIsExternAndIncluded(cl); if (include) { - // HERE: was using IdName(cl) as name, now using clName(cl) var cw = CreateClass(IdProtect(d.EnclosingModuleDefinition.GetCompileName(Options)), classIsExtern, cl.FullName, cl.TypeArgs, cl, cl.ParentTypeInformation.UniqueParentTraits(), cl.Origin, wr); From 0927bfe5dea41ab516d8181306eaef9d9f864e21 Mon Sep 17 00:00:00 2001 From: Olivier Bouissou Date: Thu, 9 Jan 2025 08:20:23 -0500 Subject: [PATCH 24/45] Removing useless if-then-else --- Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs index 16d30a6253..444c6e372a 100644 --- a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs +++ b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs @@ -270,10 +270,9 @@ protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw, string a /// private string protectedTypeName(TopLevelDecl dt) { var protectedName = IdName(dt); - if (dt.EnclosingModuleDefinition is { Name: var moduleName } && moduleName == protectedName) - if (moduleName == protectedName) { - return $"_{protectedName}"; - } + if (dt.EnclosingModuleDefinition is { Name: var moduleName } && moduleName == protectedName) { + return $"_{protectedName}"; + } return protectedName; } From 6c73672944a684c4290fb32026efbac03eabef20 Mon Sep 17 00:00:00 2001 From: Olivier Bouissou Date: Thu, 9 Jan 2025 08:26:12 -0500 Subject: [PATCH 25/45] Adding test files --- .../LitTests/LitTest/git-issues/git-issu-3809.dfy | 14 ++++++++++++++ .../LitTest/git-issues/git-issu-3809.dfy.expect | 1 + 2 files changed, 15 insertions(+) create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issu-3809.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issu-3809.dfy.expect diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issu-3809.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issu-3809.dfy new file mode 100644 index 0000000000..d2ad39e2d0 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issu-3809.dfy @@ -0,0 +1,14 @@ +// RUN: %testDafnyForEachCompiler --refresh-exit-code=0 "%s" + +module m { + datatype D = A + | B + | C { + static const Default: D := A + } + + method Main() { + print "Hello!\n"; + } + +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issu-3809.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issu-3809.dfy.expect new file mode 100644 index 0000000000..10ddd6d257 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issu-3809.dfy.expect @@ -0,0 +1 @@ +Hello! From 06ece5a0253afc81c85af188818b214b0319e5ef Mon Sep 17 00:00:00 2001 From: Olivier Bouissou Date: Thu, 9 Jan 2025 08:31:13 -0500 Subject: [PATCH 26/45] Default protected name in CS also --- Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs | 1 + 1 file changed, 1 insertion(+) diff --git a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs index cccbd96d39..7dd26ad424 100644 --- a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs +++ b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs @@ -2477,6 +2477,7 @@ public override string PublicIdProtect(string name) { case "ToString": case "GetHashCode": case "Main": + case "Default": return "_" + name; default: return name; From 87d818ea927062a6f24f184ec6acfb7416de6325 Mon Sep 17 00:00:00 2001 From: Olivier Bouissou Date: Thu, 9 Jan 2025 08:36:01 -0500 Subject: [PATCH 27/45] Renaming files --- .../LitTest/git-issues/{git-issu-3809.dfy => git-issue-3809.dfy} | 0 .../{git-issu-3809.dfy.expect => git-issue-3809.dfy.expect} | 0 2 files changed, 0 insertions(+), 0 deletions(-) rename Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/{git-issu-3809.dfy => git-issue-3809.dfy} (100%) rename Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/{git-issu-3809.dfy.expect => git-issue-3809.dfy.expect} (100%) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issu-3809.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3809.dfy similarity index 100% rename from Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issu-3809.dfy rename to Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3809.dfy diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issu-3809.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3809.dfy.expect similarity index 100% rename from Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issu-3809.dfy.expect rename to Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3809.dfy.expect From 80d2341b814c18b2e8491ecf8d40199e34b2e9e6 Mon Sep 17 00:00:00 2001 From: Olivier Bouissou Date: Thu, 9 Jan 2025 09:47:53 -0500 Subject: [PATCH 28/45] Better test to check that Default is correct --- .../LitTests/LitTest/git-issues/git-issue-3809.dfy | 8 +++++++- .../LitTests/LitTest/git-issues/git-issue-3809.dfy.expect | 1 + 2 files changed, 8 insertions(+), 1 deletion(-) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3809.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3809.dfy index d2ad39e2d0..b07924f067 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3809.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3809.dfy @@ -4,10 +4,16 @@ module m { datatype D = A | B | C { - static const Default: D := A + static const Default: D := B } method Main() { + var x := D.Default; + match x { + case A => print "A!\n"; + case B => print "B!\n"; + case C => print "C!\n"; + } print "Hello!\n"; } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3809.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3809.dfy.expect index 10ddd6d257..cd144ee6b0 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3809.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3809.dfy.expect @@ -1 +1,2 @@ +B! Hello! From 22fe2cd382820ad6cfca6012fa79fee9f884e7f2 Mon Sep 17 00:00:00 2001 From: Olivier Bouissou Date: Thu, 9 Jan 2025 09:48:01 -0500 Subject: [PATCH 29/45] Fix Go case also --- Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs | 1 + 1 file changed, 1 insertion(+) diff --git a/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs b/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs index edbeb76c7c..8fca2b3458 100644 --- a/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs +++ b/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs @@ -2579,6 +2579,7 @@ public override string PublicIdProtect(string name) { case "String": case "Equals": case "EqualsGeneric": + case "Default": // Built-in types (can also be used as functions) case "bool": From eb8a522f9c227d409ef6638fd41840281584fe75 Mon Sep 17 00:00:00 2001 From: Olivier Bouissou Date: Thu, 9 Jan 2025 09:49:44 -0500 Subject: [PATCH 30/45] Remove extra comment --- Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs b/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs index 34a24125ca..dc8d871516 100644 --- a/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs +++ b/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs @@ -452,7 +452,7 @@ protected override IClassWriter DeclareDatatype(DatatypeDecl dt, ConcreteSyntaxT // Overload the not-comparison operator wstruct.WriteLine("friend bool operator!=(const {0} &left, const {0} &right) {{ return !(left == right); }} ", structName); - // Define a custom hasherGetCompileName + // Define a custom hasher hashWr.WriteLine("template <{0}>", TypeParameters(dt.TypeArgs)); var fullName = dt.EnclosingModuleDefinition.GetCompileName(Options) + "::" + structName + InstantiateTemplate(dt.TypeArgs); var hwr = hashWr.NewBlock(string.Format("struct std::hash<{0}>", fullName), ";"); From eccab32dcf9688a5f55455c3869064e9eeb5546f Mon Sep 17 00:00:00 2001 From: Olivier Bouissou Date: Thu, 9 Jan 2025 08:01:37 -0500 Subject: [PATCH 31/45] Adding Default as a protected name --- Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs | 1 + 1 file changed, 1 insertion(+) diff --git a/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs b/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs index 88a80e524e..89c86b482a 100644 --- a/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs +++ b/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs @@ -2440,6 +2440,7 @@ private static string PublicIdProtectAux(string name) { case "toString": case "equals": case "hashCode": + case "Default": return name + "_"; // TODO: figure out what to do here (C# uses @, Go uses _, JS uses _$$_) default: return name; // Package name is not a keyword, so it can be used From 68b41b44dd5647f23083cb9f7f58b336438196bf Mon Sep 17 00:00:00 2001 From: Olivier Bouissou Date: Thu, 9 Jan 2025 08:26:12 -0500 Subject: [PATCH 32/45] Adding test files --- .../LitTests/LitTest/git-issues/git-issu-3809.dfy | 14 ++++++++++++++ .../LitTest/git-issues/git-issu-3809.dfy.expect | 1 + 2 files changed, 15 insertions(+) create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issu-3809.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issu-3809.dfy.expect diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issu-3809.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issu-3809.dfy new file mode 100644 index 0000000000..d2ad39e2d0 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issu-3809.dfy @@ -0,0 +1,14 @@ +// RUN: %testDafnyForEachCompiler --refresh-exit-code=0 "%s" + +module m { + datatype D = A + | B + | C { + static const Default: D := A + } + + method Main() { + print "Hello!\n"; + } + +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issu-3809.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issu-3809.dfy.expect new file mode 100644 index 0000000000..10ddd6d257 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issu-3809.dfy.expect @@ -0,0 +1 @@ +Hello! From 86c6209d041dc5148dfe142c69ee4d9d32943da8 Mon Sep 17 00:00:00 2001 From: Olivier Bouissou Date: Thu, 9 Jan 2025 08:31:13 -0500 Subject: [PATCH 33/45] Default protected name in CS also --- Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs | 1 + 1 file changed, 1 insertion(+) diff --git a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs index 444c6e372a..330dd155ed 100644 --- a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs +++ b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs @@ -2490,6 +2490,7 @@ public override string PublicIdProtect(string name) { case "ToString": case "GetHashCode": case "Main": + case "Default": return "_" + name; default: return name; From 137798e982cfb0e6b1b30ff80bf1192517d891ce Mon Sep 17 00:00:00 2001 From: Olivier Bouissou Date: Thu, 9 Jan 2025 08:36:01 -0500 Subject: [PATCH 34/45] Renaming files --- .../LitTest/git-issues/{git-issu-3809.dfy => git-issue-3809.dfy} | 0 .../{git-issu-3809.dfy.expect => git-issue-3809.dfy.expect} | 0 2 files changed, 0 insertions(+), 0 deletions(-) rename Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/{git-issu-3809.dfy => git-issue-3809.dfy} (100%) rename Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/{git-issu-3809.dfy.expect => git-issue-3809.dfy.expect} (100%) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issu-3809.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3809.dfy similarity index 100% rename from Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issu-3809.dfy rename to Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3809.dfy diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issu-3809.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3809.dfy.expect similarity index 100% rename from Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issu-3809.dfy.expect rename to Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3809.dfy.expect From 8f990c8a88a2ca53bbf8558980dc922d9576b47c Mon Sep 17 00:00:00 2001 From: Olivier Bouissou Date: Thu, 9 Jan 2025 09:47:53 -0500 Subject: [PATCH 35/45] Better test to check that Default is correct --- .../LitTests/LitTest/git-issues/git-issue-3809.dfy | 8 +++++++- .../LitTests/LitTest/git-issues/git-issue-3809.dfy.expect | 1 + 2 files changed, 8 insertions(+), 1 deletion(-) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3809.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3809.dfy index d2ad39e2d0..b07924f067 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3809.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3809.dfy @@ -4,10 +4,16 @@ module m { datatype D = A | B | C { - static const Default: D := A + static const Default: D := B } method Main() { + var x := D.Default; + match x { + case A => print "A!\n"; + case B => print "B!\n"; + case C => print "C!\n"; + } print "Hello!\n"; } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3809.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3809.dfy.expect index 10ddd6d257..cd144ee6b0 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3809.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3809.dfy.expect @@ -1 +1,2 @@ +B! Hello! From 10b5a1ce8bb5e35a1e46c92ecc0eb5a841f70d56 Mon Sep 17 00:00:00 2001 From: Olivier Bouissou Date: Thu, 9 Jan 2025 09:48:01 -0500 Subject: [PATCH 36/45] Fix Go case also --- Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs | 1 + 1 file changed, 1 insertion(+) diff --git a/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs b/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs index 953f7d4347..1401c5b107 100644 --- a/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs +++ b/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs @@ -2579,6 +2579,7 @@ public override string PublicIdProtect(string name) { case "String": case "Equals": case "EqualsGeneric": + case "Default": // Built-in types (can also be used as functions) case "bool": From 968536362fd4708a247c0856008040685c018661 Mon Sep 17 00:00:00 2001 From: Olivier Bouissou Date: Thu, 9 Jan 2025 10:42:22 -0500 Subject: [PATCH 37/45] Improved test --- .../LitTests/LitTest/git-issues/git-issue-3809.dfy | 8 +++++++- .../LitTests/LitTest/git-issues/git-issue-3809.dfy.expect | 1 + 2 files changed, 8 insertions(+), 1 deletion(-) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3809.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3809.dfy index b07924f067..6669ff2d29 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3809.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3809.dfy @@ -4,11 +4,17 @@ module m { datatype D = A | B | C { - static const Default: D := B + static const Default: D := B // This one will be translated as Default_ + method Default_() { // Just to be sure there is no clash: this is translated as Default__ + print "Default_ Method\n"; + } } + + method Main() { var x := D.Default; + x.Default_(); match x { case A => print "A!\n"; case B => print "B!\n"; diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3809.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3809.dfy.expect index cd144ee6b0..9ba695c450 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3809.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3809.dfy.expect @@ -1,2 +1,3 @@ +Default_ Method B! Hello! From 7dee024a60b546fb21a875d71771f5d93a386fc1 Mon Sep 17 00:00:00 2001 From: Olivier Bouissou Date: Thu, 9 Jan 2025 17:14:14 -0500 Subject: [PATCH 38/45] Really fix Go case --- Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs b/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs index 1401c5b107..12dfa815b0 100644 --- a/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs +++ b/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs @@ -2515,7 +2515,7 @@ private string IdName(Declaration decl) { // Don't use Go_ because Capitalize might use it and we know there's a conflict return "Go__" + decl.GetCompileName(Options); } else { - return Capitalize(decl.GetCompileName(Options)); + return IdProtect(Capitalize(decl.GetCompileName(Options))); } } From 40435ca10c74c61f21413d38ffa6f9ac589ea0fc Mon Sep 17 00:00:00 2001 From: Olivier Bouissou Date: Thu, 9 Jan 2025 08:26:12 -0500 Subject: [PATCH 39/45] Adding test files --- .../LitTests/LitTest/git-issues/git-issu-3809.dfy | 14 ++++++++++++++ .../LitTest/git-issues/git-issu-3809.dfy.expect | 1 + 2 files changed, 15 insertions(+) create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issu-3809.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issu-3809.dfy.expect diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issu-3809.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issu-3809.dfy new file mode 100644 index 0000000000..d2ad39e2d0 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issu-3809.dfy @@ -0,0 +1,14 @@ +// RUN: %testDafnyForEachCompiler --refresh-exit-code=0 "%s" + +module m { + datatype D = A + | B + | C { + static const Default: D := A + } + + method Main() { + print "Hello!\n"; + } + +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issu-3809.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issu-3809.dfy.expect new file mode 100644 index 0000000000..10ddd6d257 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issu-3809.dfy.expect @@ -0,0 +1 @@ +Hello! From 2bb5d3c324c842b0b34b8c50a54817e51d1d874c Mon Sep 17 00:00:00 2001 From: Olivier Bouissou Date: Thu, 9 Jan 2025 08:36:01 -0500 Subject: [PATCH 40/45] Renaming files --- .../LitTests/LitTest/git-issues/git-issu-3809.dfy | 14 -------------- .../LitTest/git-issues/git-issu-3809.dfy.expect | 1 - .../LitTests/LitTest/git-issues/git-issue-3809.dfy | 2 +- 3 files changed, 1 insertion(+), 16 deletions(-) delete mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issu-3809.dfy delete mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issu-3809.dfy.expect diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issu-3809.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issu-3809.dfy deleted file mode 100644 index d2ad39e2d0..0000000000 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issu-3809.dfy +++ /dev/null @@ -1,14 +0,0 @@ -// RUN: %testDafnyForEachCompiler --refresh-exit-code=0 "%s" - -module m { - datatype D = A - | B - | C { - static const Default: D := A - } - - method Main() { - print "Hello!\n"; - } - -} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issu-3809.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issu-3809.dfy.expect deleted file mode 100644 index 10ddd6d257..0000000000 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issu-3809.dfy.expect +++ /dev/null @@ -1 +0,0 @@ -Hello! diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3809.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3809.dfy index 6669ff2d29..be8e13ec89 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3809.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3809.dfy @@ -20,7 +20,7 @@ module m { case B => print "B!\n"; case C => print "C!\n"; } - print "Hello!\n"; + print "Hello!\n"; } } From ca639a91dee72bb71085f0afed82c79adcfde671 Mon Sep 17 00:00:00 2001 From: Olivier Bouissou Date: Thu, 9 Jan 2025 09:47:53 -0500 Subject: [PATCH 41/45] Better test to check that Default is correct --- .../LitTests/LitTest/git-issues/git-issue-3809.dfy.expect | 3 +++ 1 file changed, 3 insertions(+) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3809.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3809.dfy.expect index 9ba695c450..976779f917 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3809.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3809.dfy.expect @@ -1,3 +1,6 @@ +<<<<<<< HEAD Default_ Method +======= +>>>>>>> 80d2341b8 (Better test to check that Default is correct) B! Hello! From fa418985e8d4a20bfd16399e112b6d65a82b8bef Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Wed, 8 Jan 2025 09:24:45 -0800 Subject: [PATCH 42/45] Update to .NET 8 (#5322) ### Description - Use .NET 8.0 instead of 6.0 throughout the project - Make the ordering of diagnostics deterministic even when multiple diagnostics differ only in their related locations ### How has this been tested? - Updated existing tests to match well-defined ordering By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt). --------- Co-authored-by: Remy Willems --- .github/workflows/doc-tests.yml | 6 -- .../workflows/integration-tests-reusable.yml | 2 +- .github/workflows/msbuild.yml | 2 +- .../workflows/publish-release-reusable.yml | 2 +- .github/workflows/publish-release.yml | 2 +- .github/workflows/refman.yml | 2 +- .github/workflows/release-downloads-nuget.yml | 2 +- .github/workflows/runtime-tests.yml | 6 -- .github/workflows/xunit-tests-reusable.yml | 2 +- CONTRIBUTING.md | 2 +- Scripts/use-local-boogie.sh | 2 +- Source/AutoExtern.Test/AutoExtern.Test.csproj | 1 - Source/AutoExtern.Test/Minimal/Library.csproj | 2 +- .../Tutorial/ClientApp/ClientApp.csproj | 4 +- .../Tutorial/Library/Library.csproj | 2 +- Source/AutoExtern/AutoExtern.csproj | 2 +- Source/Dafny/Dafny.csproj | 3 +- .../DafnyBenchmarkingPlugin.csproj | 1 - Source/DafnyCore.Test/DafnyCore.Test.csproj | 1 - .../DafnyToRustCompilerCoverage.cs | 2 +- .../GeneratedFromDafny/DefsCoverage.cs | 2 +- .../FactorPathsOptimizationTest.cs | 2 +- .../GeneratedFromDafny/RASTCoverage.cs | 2 +- Source/DafnyCore/AST/SystemModuleManager.cs | 2 +- .../Backends/CSharp/CsharpBackend.cs | 2 +- .../Backends/CSharp/CsharpCodeGenerator.cs | 2 +- Source/DafnyCore/DafnyCore.csproj | 7 +- Source/DafnyCore/DafnyGeneratedFromDafny.sh | 2 +- .../GeneratedFromDafny/D2DPrettyPrinter.cs | 2 +- Source/DafnyCore/GeneratedFromDafny/DAST.cs | 2 +- .../GeneratedFromDafny/DAST_Format.cs | 2 +- Source/DafnyCore/GeneratedFromDafny/DCOMP.cs | 2 +- .../DafnyCompilerRustUtils.cs | 2 +- Source/DafnyCore/GeneratedFromDafny/Defs.cs | 2 +- .../ExpressionOptimization.cs | 2 +- .../FactorPathsOptimization.cs | 2 +- .../GeneratedFromDafny/Formatting.cs | 2 +- .../GeneratedFromDafny/FuncExtensions.cs | 2 +- Source/DafnyCore/GeneratedFromDafny/RAST.cs | 2 +- .../ResolvedDesugaredExecutableDafnyPlugin.cs | 2 +- .../Std_Arithmetic_DivInternals.cs | 2 +- .../Std_Arithmetic_DivInternalsNonlinear.cs | 2 +- .../Std_Arithmetic_DivMod.cs | 2 +- .../Std_Arithmetic_GeneralInternals.cs | 2 +- .../Std_Arithmetic_Logarithm.cs | 2 +- .../Std_Arithmetic_ModInternals.cs | 2 +- .../Std_Arithmetic_ModInternalsNonlinear.cs | 2 +- .../GeneratedFromDafny/Std_Arithmetic_Mul.cs | 2 +- .../Std_Arithmetic_MulInternals.cs | 2 +- .../Std_Arithmetic_MulInternalsNonlinear.cs | 2 +- .../Std_Arithmetic_Power.cs | 2 +- .../Std_Arithmetic_Power2.cs | 2 +- .../GeneratedFromDafny/Std_Collections_Seq.cs | 2 +- .../DafnyCore/GeneratedFromDafny/Std_Math.cs | 2 +- .../GeneratedFromDafny/Std_Strings.cs | 2 +- .../Std_Strings_CharStrEscaping.cs | 2 +- .../Std_Strings_DecimalConversion.cs | 2 +- .../Std_Strings_HexConversion.cs | 2 +- .../GeneratedFromDafny/Std_Wrappers.cs | 2 +- Source/DafnyCore/Generic/DafnyDiagnostic.cs | 59 ++++++++++++++++ Source/DafnyCore/Generic/Reporting.cs | 3 - .../DafnyDriver.Test/DafnyDriver.Test.csproj | 1 - .../LanguageServerProcessTest.cs | 4 +- Source/DafnyDriver/Commands/VerifyCommand.cs | 4 +- Source/DafnyDriver/DafnyDriver.csproj | 5 +- .../DafnyLanguageServer.Test.csproj | 1 - .../Performance/LargeFilesTest.cs | 4 +- .../DafnyLanguageServer.csproj | 5 +- .../Language/CachingParser.cs | 4 +- .../Language/CachingResolver.cs | 4 +- .../DafnyPipeline.Test.csproj | 1 - .../DafnyPipeline.Test/ProverLogStability.cs | 2 +- Source/DafnyPipeline/DafnyPipeline.csproj | 5 +- .../DafnyRuntime.Tests.csproj | 1 - Source/DafnyRuntime/DafnyRuntime.csproj | 1 + .../DafnyRuntime/DafnyRuntimeSystemModule.cs | 2 +- Source/DafnyServer/DafnyServer.csproj | 5 +- Source/DafnyServer/SuperLegacySymbolTable.cs | 12 +--- .../DafnyTestGeneration.Test.csproj | 1 - .../DafnyTestGeneration.csproj | 3 +- Source/Directory.Build.props | 1 + .../IntegrationTests/IntegrationTests.csproj | 1 - Source/IntegrationTests/LitTests.cs | 2 +- .../DafnyTests/RunAllTests/RunAllTests.csproj | 2 +- .../TestAttribute/TestAttribute.csproj | 2 +- .../comp/manualcompile/ManualCompile.csproj | 2 +- .../comp/manualcompile/ManualCompile.dfy | 2 +- .../consumer/Consumer.csproj | 2 +- .../LitTest/dafny0/AutoReq.dfy.expect | 6 +- .../dafny0/{Fuel.legacy.dfy => Fuel.dfy} | 2 +- .../LitTests/LitTest/dafny0/Fuel.dfy.expect | 67 +++++++++++++++++++ .../LitTest/dafny0/Fuel.legacy.dfy.expect | 67 ------------------- .../LitTest/dafny0/Input/IncludesTuples.dfy | 2 +- ...message-per-failed-precondition.dfy.expect | 8 +-- .../LitTest/examples/Simple_compiler/Makefile | 2 +- .../csharp/SimpleCompiler.csproj | 4 +- .../git-issues/git-issue-2299.dfy.expect | 6 +- .../git-issues/git-issue-3549a.dfy.expect | 2 +- .../InductionWithoutTriggers.dfy.expect | 6 +- ...nductionWithoutTriggers.dfy.refresh.expect | 6 +- Source/TestDafny/TestDafny.csproj | 2 +- Source/XUnitExtensions/Lit/DiffCommand.cs | 2 +- Source/XUnitExtensions/XUnitExtensions.csproj | 2 +- customBoogie.patch | 2 +- docs/DafnyRef/Plugins.md | 2 +- docs/DafnyRef/UserGuide.md | 2 +- docs/Installation.md | 22 +++--- docs/OnlineTutorial/guide.10.expect | 8 +-- 108 files changed, 259 insertions(+), 233 deletions(-) create mode 100644 Source/DafnyCore/Generic/DafnyDiagnostic.cs rename Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/{Fuel.legacy.dfy => Fuel.dfy} (99%) create mode 100755 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Fuel.dfy.expect delete mode 100755 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Fuel.legacy.dfy.expect diff --git a/.github/workflows/doc-tests.yml b/.github/workflows/doc-tests.yml index 919b1aeece..99dc121ca7 100644 --- a/.github/workflows/doc-tests.yml +++ b/.github/workflows/doc-tests.yml @@ -32,12 +32,6 @@ jobs: uses: actions/setup-dotnet@v4 with: dotnet-version: 8.0.x - # If we do not also install .NET 6 as well, then our doc-tests fail for an unknown reason - # Failing run: https://github.com/dafny-lang/dafny/actions/runs/12276984671/job/34255376460 - - name: Setup dotnet - uses: actions/setup-dotnet@v4 - with: - dotnet-version: 6.0.x - name: Checkout Dafny uses: actions/checkout@v4 with: diff --git a/.github/workflows/integration-tests-reusable.yml b/.github/workflows/integration-tests-reusable.yml index ed6ee6687f..3109c167cc 100644 --- a/.github/workflows/integration-tests-reusable.yml +++ b/.github/workflows/integration-tests-reusable.yml @@ -19,7 +19,7 @@ on: default: "" env: - dotnet-version: 6.0.x # SDK Version for building Dafny + dotnet-version: 8.0.x # SDK Version for building Dafny jobs: # This job is used to dynamically calculate the matrix dimensions. diff --git a/.github/workflows/msbuild.yml b/.github/workflows/msbuild.yml index c8c8e173e0..5e779c576a 100644 --- a/.github/workflows/msbuild.yml +++ b/.github/workflows/msbuild.yml @@ -12,7 +12,7 @@ concurrency: env: - dotnet-version: 6.0.x # SDK Version for building Dafny + dotnet-version: 8.0.x # SDK Version for building Dafny jobs: check-deep-tests: diff --git a/.github/workflows/publish-release-reusable.yml b/.github/workflows/publish-release-reusable.yml index d288548bf8..adee22747d 100644 --- a/.github/workflows/publish-release-reusable.yml +++ b/.github/workflows/publish-release-reusable.yml @@ -30,7 +30,7 @@ on: required: false env: - dotnet-version: 6.0.x # SDK Version for building Dafny + dotnet-version: 8.0.x # SDK Version for building Dafny jobs: diff --git a/.github/workflows/publish-release.yml b/.github/workflows/publish-release.yml index 7600affd73..7b3ee73a7e 100644 --- a/.github/workflows/publish-release.yml +++ b/.github/workflows/publish-release.yml @@ -7,7 +7,7 @@ on: - 'v*' env: - dotnet-version: 6.0.x # SDK Version for building Dafny + dotnet-version: 8.0.x # SDK Version for building Dafny jobs: deep-integration-tests: diff --git a/.github/workflows/refman.yml b/.github/workflows/refman.yml index 72caa203bf..93a65d4470 100644 --- a/.github/workflows/refman.yml +++ b/.github/workflows/refman.yml @@ -28,7 +28,7 @@ jobs: - name: Setup dotnet uses: actions/setup-dotnet@v4 with: - dotnet-version: 6.0.x + dotnet-version: 8.0.x - name: Checkout Dafny uses: actions/checkout@v4 with: diff --git a/.github/workflows/release-downloads-nuget.yml b/.github/workflows/release-downloads-nuget.yml index 09c25932a1..1d08a00ba4 100644 --- a/.github/workflows/release-downloads-nuget.yml +++ b/.github/workflows/release-downloads-nuget.yml @@ -17,7 +17,7 @@ on: workflow_dispatch: env: - dotnet-version: 6.0.x # SDK Version for running Dafny (TODO: should this be an older version?) + dotnet-version: 8.0.x # SDK Version for running Dafny (TODO: should this be an older version?) z3BaseUri: https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02 concurrency: diff --git a/.github/workflows/runtime-tests.yml b/.github/workflows/runtime-tests.yml index 8a5719110b..0d5888a133 100644 --- a/.github/workflows/runtime-tests.yml +++ b/.github/workflows/runtime-tests.yml @@ -31,12 +31,6 @@ jobs: uses: actions/setup-dotnet@v4 with: dotnet-version: 8.0.x - # If we do not also install .NET 6 as well, then our doc-tests fail for an unknown reason - # Failing run: https://github.com/dafny-lang/dafny/actions/runs/12276984671/job/34255376460 - - name: Setup dotnet - uses: actions/setup-dotnet@v4 - with: - dotnet-version: 6.0.x - name: Set up JDK 18 uses: actions/setup-java@v4 with: diff --git a/.github/workflows/xunit-tests-reusable.yml b/.github/workflows/xunit-tests-reusable.yml index 68576f2315..d6b768e6f3 100644 --- a/.github/workflows/xunit-tests-reusable.yml +++ b/.github/workflows/xunit-tests-reusable.yml @@ -73,7 +73,7 @@ jobs: - name: Setup .NET uses: actions/setup-dotnet@v4 with: - dotnet-version: 6.0.x + dotnet-version: 8.0.x - name: Install dependencies run: | dotnet restore ${{env.solutionPath}} diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index b181dac5d1..ddaf054181 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -85,7 +85,7 @@ Subsequent CI runs should pick up the successful `deep-tests` run and make the ` ### How can I write portions of Dafny in Dafny itself? Since https://github.com/dafny-lang/dafny/pull/2399, it is possible to add \*.dfy files next to other source files. -The plugin `dafny-msbuild` takes all the dafny files and compiles them into a single file `Source/DafnyCore/obj/Debug/net6.0/GeneratedFromDafny.cs` +The plugin `dafny-msbuild` takes all the dafny files and compiles them into a single file `Source/DafnyCore/obj/Debug/net8.0/GeneratedFromDafny.cs` that is automatically included in the build process. This file contains also the Dafny run-time in C#. One example of such file is `Source/DafnyCore/AST/Formatting.dfy`, and you can use it as a starting point. diff --git a/Scripts/use-local-boogie.sh b/Scripts/use-local-boogie.sh index e3e23d2c0b..49f1f45613 100755 --- a/Scripts/use-local-boogie.sh +++ b/Scripts/use-local-boogie.sh @@ -2,5 +2,5 @@ BOOGIE_PATH="boogie/" allDlls=("Boogie.AbstractInterpretation.dll" "Boogie.BaseTypes.dll" "Boogie.CodeContractsExtender.dll" "Boogie.Concurrency.dll" "Boogie.Core.dll" "Boogie.ExecutionEngine.dll" "Boogie.Graph.dll" "Boogie.Houdini.dll" "Boogie.Model.dll" "Boogie.Predication.dll" "Boogie.Provers.SMTLib.dll" "Boogie.VCExpr.dll" "Boogie.VCGeneration.dll" "BoogieDriver.dll" "System.Configuration.ConfigurationManager.dll" "System.Runtime.Caching.dll" "System.Security.Cryptography.ProtectedData.dll" "System.Security.Permissions.dll") for t in "${allDlls[@]}" do - cp "${BOOGIE_PATH}Source/BoogieDriver/bin/Release/net6.0/${t}" Binaries/ + cp "${BOOGIE_PATH}Source/BoogieDriver/bin/Release/net8.0/${t}" Binaries/ done diff --git a/Source/AutoExtern.Test/AutoExtern.Test.csproj b/Source/AutoExtern.Test/AutoExtern.Test.csproj index 0c4e1dc0b5..08593d7dba 100644 --- a/Source/AutoExtern.Test/AutoExtern.Test.csproj +++ b/Source/AutoExtern.Test/AutoExtern.Test.csproj @@ -2,7 +2,6 @@ Exe - net6.0 enable enable false diff --git a/Source/AutoExtern.Test/Minimal/Library.csproj b/Source/AutoExtern.Test/Minimal/Library.csproj index 132c02c59c..30402ac0e7 100644 --- a/Source/AutoExtern.Test/Minimal/Library.csproj +++ b/Source/AutoExtern.Test/Minimal/Library.csproj @@ -1,7 +1,7 @@ - net6.0 + net8.0 enable enable diff --git a/Source/AutoExtern.Test/Tutorial/ClientApp/ClientApp.csproj b/Source/AutoExtern.Test/Tutorial/ClientApp/ClientApp.csproj index 86b01ff865..7ba274e8ce 100644 --- a/Source/AutoExtern.Test/Tutorial/ClientApp/ClientApp.csproj +++ b/Source/AutoExtern.Test/Tutorial/ClientApp/ClientApp.csproj @@ -2,9 +2,9 @@ Exe - net6.0 + net8.0 enable - CS3021; CS0162 + CS8981; CS3021; CS0162 diff --git a/Source/AutoExtern.Test/Tutorial/Library/Library.csproj b/Source/AutoExtern.Test/Tutorial/Library/Library.csproj index 132c02c59c..30402ac0e7 100644 --- a/Source/AutoExtern.Test/Tutorial/Library/Library.csproj +++ b/Source/AutoExtern.Test/Tutorial/Library/Library.csproj @@ -1,7 +1,7 @@ - net6.0 + net8.0 enable enable diff --git a/Source/AutoExtern/AutoExtern.csproj b/Source/AutoExtern/AutoExtern.csproj index 0c00890cff..f44de5524b 100644 --- a/Source/AutoExtern/AutoExtern.csproj +++ b/Source/AutoExtern/AutoExtern.csproj @@ -2,7 +2,7 @@ Exe - net6.0 + net8.0 enable enable false diff --git a/Source/Dafny/Dafny.csproj b/Source/Dafny/Dafny.csproj index ff383440c3..7c639eb2b7 100644 --- a/Source/Dafny/Dafny.csproj +++ b/Source/Dafny/Dafny.csproj @@ -5,7 +5,6 @@ Dafny true TRACE - net6.0 Major ..\..\Binaries\ false @@ -16,7 +15,7 @@ README.md - + false false diff --git a/Source/DafnyBenchmarkingPlugin/DafnyBenchmarkingPlugin.csproj b/Source/DafnyBenchmarkingPlugin/DafnyBenchmarkingPlugin.csproj index 9cf987817b..85823c27a9 100644 --- a/Source/DafnyBenchmarkingPlugin/DafnyBenchmarkingPlugin.csproj +++ b/Source/DafnyBenchmarkingPlugin/DafnyBenchmarkingPlugin.csproj @@ -1,7 +1,6 @@ - net6.0 Major enable enable diff --git a/Source/DafnyCore.Test/DafnyCore.Test.csproj b/Source/DafnyCore.Test/DafnyCore.Test.csproj index 8e9d3e8aeb..e585e29faf 100644 --- a/Source/DafnyCore.Test/DafnyCore.Test.csproj +++ b/Source/DafnyCore.Test/DafnyCore.Test.csproj @@ -1,7 +1,6 @@ - net6.0 enable enable diff --git a/Source/DafnyCore.Test/GeneratedFromDafny/DafnyToRustCompilerCoverage.cs b/Source/DafnyCore.Test/GeneratedFromDafny/DafnyToRustCompilerCoverage.cs index fc783dccf8..699aeffaaf 100644 --- a/Source/DafnyCore.Test/GeneratedFromDafny/DafnyToRustCompilerCoverage.cs +++ b/Source/DafnyCore.Test/GeneratedFromDafny/DafnyToRustCompilerCoverage.cs @@ -1,7 +1,7 @@ // Dafny program the_program compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyCore.Test/GeneratedFromDafny/DefsCoverage.cs b/Source/DafnyCore.Test/GeneratedFromDafny/DefsCoverage.cs index 9ea4308a4f..c31e0447b0 100644 --- a/Source/DafnyCore.Test/GeneratedFromDafny/DefsCoverage.cs +++ b/Source/DafnyCore.Test/GeneratedFromDafny/DefsCoverage.cs @@ -1,7 +1,7 @@ // Dafny program the_program compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyCore.Test/GeneratedFromDafny/FactorPathsOptimizationTest.cs b/Source/DafnyCore.Test/GeneratedFromDafny/FactorPathsOptimizationTest.cs index 7b3f936730..04573118e9 100644 --- a/Source/DafnyCore.Test/GeneratedFromDafny/FactorPathsOptimizationTest.cs +++ b/Source/DafnyCore.Test/GeneratedFromDafny/FactorPathsOptimizationTest.cs @@ -1,7 +1,7 @@ // Dafny program the_program compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyCore.Test/GeneratedFromDafny/RASTCoverage.cs b/Source/DafnyCore.Test/GeneratedFromDafny/RASTCoverage.cs index 8b8833e5ad..bebebfe276 100644 --- a/Source/DafnyCore.Test/GeneratedFromDafny/RASTCoverage.cs +++ b/Source/DafnyCore.Test/GeneratedFromDafny/RASTCoverage.cs @@ -1,7 +1,7 @@ // Dafny program the_program compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyCore/AST/SystemModuleManager.cs b/Source/DafnyCore/AST/SystemModuleManager.cs index e153c76bfe..2c8c02fa49 100644 --- a/Source/DafnyCore/AST/SystemModuleManager.cs +++ b/Source/DafnyCore/AST/SystemModuleManager.cs @@ -62,7 +62,7 @@ public byte[] MyHash { Concat(TotalArrowTypeDecls.Keys.OrderBy(x => x)). Concat(tupleInts.OrderBy(x => x)); var bytes = ints.SelectMany(BitConverter.GetBytes).ToArray(); - hash = HashAlgorithm.Create("SHA256")!.ComputeHash(bytes); + hash = SHA256.Create()!.ComputeHash(bytes); } return hash; diff --git a/Source/DafnyCore/Backends/CSharp/CsharpBackend.cs b/Source/DafnyCore/Backends/CSharp/CsharpBackend.cs index 82e8606a0f..50c293c1f0 100644 --- a/Source/DafnyCore/Backends/CSharp/CsharpBackend.cs +++ b/Source/DafnyCore/Backends/CSharp/CsharpBackend.cs @@ -92,7 +92,7 @@ public override string GetCompileName(bool isDefaultModule, string moduleName, s {outputType} - net6.0 + net8.0 enable false CS8600;CS8603;CS8604;CS8605;CS8625;CS8629;CS8714;CS8765;CS8769;CS8981 diff --git a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs index 330dd155ed..d8092b8467 100644 --- a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs +++ b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs @@ -67,7 +67,7 @@ protected override void EmitHeader(Program program, ConcreteSyntaxTree wr) { wr.WriteLine("// Dafny program {0} compiled into C#", program.Name); wr.WriteLine("// To recompile, you will need the libraries"); wr.WriteLine("// System.Runtime.Numerics.dll System.Collections.Immutable.dll"); - wr.WriteLine("// but the 'dotnet' tool in net6.0 should pick those up automatically."); + wr.WriteLine("// but the 'dotnet' tool in .NET should pick those up automatically."); wr.WriteLine("// Optionally, you may want to include compiler switches like"); wr.WriteLine("// /debug /nowarn:162,164,168,183,219,436,1717,1718"); wr.WriteLine(); diff --git a/Source/DafnyCore/DafnyCore.csproj b/Source/DafnyCore/DafnyCore.csproj index 3ac2ed66bb..56f845c656 100644 --- a/Source/DafnyCore/DafnyCore.csproj +++ b/Source/DafnyCore/DafnyCore.csproj @@ -17,11 +17,12 @@ true ..\..\Binaries\ TRACE - net6.0 Major MIT - $(NoWarn);NU5104 + $(NoWarn);NU5104;CS8981 + + true @@ -35,7 +36,7 @@ - + diff --git a/Source/DafnyCore/DafnyGeneratedFromDafny.sh b/Source/DafnyCore/DafnyGeneratedFromDafny.sh index 2ae61370ed..44210dad64 100755 --- a/Source/DafnyCore/DafnyGeneratedFromDafny.sh +++ b/Source/DafnyCore/DafnyGeneratedFromDafny.sh @@ -4,7 +4,7 @@ # 1. Delete the file GeneratedFromDafny.cs # 2. Add a dependency to # -# That's it! The same file will now be automatically generated as obj/Debug/net6.0/GeneratedFromDafny.cs +# That's it! The same file will now be automatically generated as obj/Debug/net8.0/GeneratedFromDafny.cs # 3. Remove the following dependencies that are being taken care by dafny-msbuild # # diff --git a/Source/DafnyCore/GeneratedFromDafny/D2DPrettyPrinter.cs b/Source/DafnyCore/GeneratedFromDafny/D2DPrettyPrinter.cs index eaf1d9b97e..9216519c02 100644 --- a/Source/DafnyCore/GeneratedFromDafny/D2DPrettyPrinter.cs +++ b/Source/DafnyCore/GeneratedFromDafny/D2DPrettyPrinter.cs @@ -1,7 +1,7 @@ // Dafny program the_program compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyCore/GeneratedFromDafny/DAST.cs b/Source/DafnyCore/GeneratedFromDafny/DAST.cs index 17306167c6..b6152f6d38 100644 --- a/Source/DafnyCore/GeneratedFromDafny/DAST.cs +++ b/Source/DafnyCore/GeneratedFromDafny/DAST.cs @@ -1,7 +1,7 @@ // Dafny program the_program compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyCore/GeneratedFromDafny/DAST_Format.cs b/Source/DafnyCore/GeneratedFromDafny/DAST_Format.cs index 1efc61a86e..b7550c51a9 100644 --- a/Source/DafnyCore/GeneratedFromDafny/DAST_Format.cs +++ b/Source/DafnyCore/GeneratedFromDafny/DAST_Format.cs @@ -1,7 +1,7 @@ // Dafny program the_program compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs b/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs index 01c84f6080..154c7d9a08 100644 --- a/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs +++ b/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs @@ -1,7 +1,7 @@ // Dafny program the_program compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyCore/GeneratedFromDafny/DafnyCompilerRustUtils.cs b/Source/DafnyCore/GeneratedFromDafny/DafnyCompilerRustUtils.cs index 061db1db0d..e83a87fbeb 100644 --- a/Source/DafnyCore/GeneratedFromDafny/DafnyCompilerRustUtils.cs +++ b/Source/DafnyCore/GeneratedFromDafny/DafnyCompilerRustUtils.cs @@ -1,7 +1,7 @@ // Dafny program the_program compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyCore/GeneratedFromDafny/Defs.cs b/Source/DafnyCore/GeneratedFromDafny/Defs.cs index cd86606bcf..e8e90c99a8 100644 --- a/Source/DafnyCore/GeneratedFromDafny/Defs.cs +++ b/Source/DafnyCore/GeneratedFromDafny/Defs.cs @@ -1,7 +1,7 @@ // Dafny program the_program compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyCore/GeneratedFromDafny/ExpressionOptimization.cs b/Source/DafnyCore/GeneratedFromDafny/ExpressionOptimization.cs index 2b9201f0b8..2ffd8bd898 100644 --- a/Source/DafnyCore/GeneratedFromDafny/ExpressionOptimization.cs +++ b/Source/DafnyCore/GeneratedFromDafny/ExpressionOptimization.cs @@ -1,7 +1,7 @@ // Dafny program the_program compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyCore/GeneratedFromDafny/FactorPathsOptimization.cs b/Source/DafnyCore/GeneratedFromDafny/FactorPathsOptimization.cs index 2308d3c767..6d755a587c 100644 --- a/Source/DafnyCore/GeneratedFromDafny/FactorPathsOptimization.cs +++ b/Source/DafnyCore/GeneratedFromDafny/FactorPathsOptimization.cs @@ -1,7 +1,7 @@ // Dafny program the_program compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyCore/GeneratedFromDafny/Formatting.cs b/Source/DafnyCore/GeneratedFromDafny/Formatting.cs index 07d403c955..f8026126c1 100644 --- a/Source/DafnyCore/GeneratedFromDafny/Formatting.cs +++ b/Source/DafnyCore/GeneratedFromDafny/Formatting.cs @@ -1,7 +1,7 @@ // Dafny program the_program compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyCore/GeneratedFromDafny/FuncExtensions.cs b/Source/DafnyCore/GeneratedFromDafny/FuncExtensions.cs index 39894fcdf0..af326244b5 100644 --- a/Source/DafnyCore/GeneratedFromDafny/FuncExtensions.cs +++ b/Source/DafnyCore/GeneratedFromDafny/FuncExtensions.cs @@ -1,7 +1,7 @@ // Dafny program the_program compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyCore/GeneratedFromDafny/RAST.cs b/Source/DafnyCore/GeneratedFromDafny/RAST.cs index 8c0c742cf2..eeceeaf7c4 100644 --- a/Source/DafnyCore/GeneratedFromDafny/RAST.cs +++ b/Source/DafnyCore/GeneratedFromDafny/RAST.cs @@ -1,7 +1,7 @@ // Dafny program the_program compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyCore/GeneratedFromDafny/ResolvedDesugaredExecutableDafnyPlugin.cs b/Source/DafnyCore/GeneratedFromDafny/ResolvedDesugaredExecutableDafnyPlugin.cs index b545bb2a8e..b6eb208ee5 100644 --- a/Source/DafnyCore/GeneratedFromDafny/ResolvedDesugaredExecutableDafnyPlugin.cs +++ b/Source/DafnyCore/GeneratedFromDafny/ResolvedDesugaredExecutableDafnyPlugin.cs @@ -1,7 +1,7 @@ // Dafny program the_program compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_DivInternals.cs b/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_DivInternals.cs index 997d1b461c..cf1aa8ccbe 100644 --- a/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_DivInternals.cs +++ b/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_DivInternals.cs @@ -1,7 +1,7 @@ // Dafny program the_program compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_DivInternalsNonlinear.cs b/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_DivInternalsNonlinear.cs index 42ee76c580..317eb9149b 100644 --- a/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_DivInternalsNonlinear.cs +++ b/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_DivInternalsNonlinear.cs @@ -1,7 +1,7 @@ // Dafny program the_program compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_DivMod.cs b/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_DivMod.cs index 0cacb4aa84..75a36f1e97 100644 --- a/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_DivMod.cs +++ b/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_DivMod.cs @@ -1,7 +1,7 @@ // Dafny program the_program compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_GeneralInternals.cs b/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_GeneralInternals.cs index bfbf27c915..189d7f348b 100644 --- a/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_GeneralInternals.cs +++ b/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_GeneralInternals.cs @@ -1,7 +1,7 @@ // Dafny program the_program compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_Logarithm.cs b/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_Logarithm.cs index de30d84aca..081f1d7848 100644 --- a/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_Logarithm.cs +++ b/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_Logarithm.cs @@ -1,7 +1,7 @@ // Dafny program the_program compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_ModInternals.cs b/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_ModInternals.cs index 956c44501c..5b8f886515 100644 --- a/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_ModInternals.cs +++ b/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_ModInternals.cs @@ -1,7 +1,7 @@ // Dafny program the_program compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_ModInternalsNonlinear.cs b/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_ModInternalsNonlinear.cs index 30cf7f2c8e..7643658879 100644 --- a/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_ModInternalsNonlinear.cs +++ b/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_ModInternalsNonlinear.cs @@ -1,7 +1,7 @@ // Dafny program the_program compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_Mul.cs b/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_Mul.cs index 9def4d585f..fe0b79e122 100644 --- a/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_Mul.cs +++ b/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_Mul.cs @@ -1,7 +1,7 @@ // Dafny program the_program compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_MulInternals.cs b/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_MulInternals.cs index dbbe944372..9d4cccdf0c 100644 --- a/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_MulInternals.cs +++ b/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_MulInternals.cs @@ -1,7 +1,7 @@ // Dafny program the_program compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_MulInternalsNonlinear.cs b/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_MulInternalsNonlinear.cs index 28123ed8dd..58e0b3e074 100644 --- a/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_MulInternalsNonlinear.cs +++ b/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_MulInternalsNonlinear.cs @@ -1,7 +1,7 @@ // Dafny program the_program compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_Power.cs b/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_Power.cs index 5d473618d6..f5cfdce6f4 100644 --- a/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_Power.cs +++ b/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_Power.cs @@ -1,7 +1,7 @@ // Dafny program the_program compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_Power2.cs b/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_Power2.cs index 8251fce257..3022cf4802 100644 --- a/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_Power2.cs +++ b/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_Power2.cs @@ -1,7 +1,7 @@ // Dafny program the_program compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyCore/GeneratedFromDafny/Std_Collections_Seq.cs b/Source/DafnyCore/GeneratedFromDafny/Std_Collections_Seq.cs index d17cdc366b..32faed2a00 100644 --- a/Source/DafnyCore/GeneratedFromDafny/Std_Collections_Seq.cs +++ b/Source/DafnyCore/GeneratedFromDafny/Std_Collections_Seq.cs @@ -1,7 +1,7 @@ // Dafny program the_program compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyCore/GeneratedFromDafny/Std_Math.cs b/Source/DafnyCore/GeneratedFromDafny/Std_Math.cs index 8e22eb1689..19b0810262 100644 --- a/Source/DafnyCore/GeneratedFromDafny/Std_Math.cs +++ b/Source/DafnyCore/GeneratedFromDafny/Std_Math.cs @@ -1,7 +1,7 @@ // Dafny program the_program compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyCore/GeneratedFromDafny/Std_Strings.cs b/Source/DafnyCore/GeneratedFromDafny/Std_Strings.cs index dbda9bad3d..0b2540af5a 100644 --- a/Source/DafnyCore/GeneratedFromDafny/Std_Strings.cs +++ b/Source/DafnyCore/GeneratedFromDafny/Std_Strings.cs @@ -1,7 +1,7 @@ // Dafny program the_program compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyCore/GeneratedFromDafny/Std_Strings_CharStrEscaping.cs b/Source/DafnyCore/GeneratedFromDafny/Std_Strings_CharStrEscaping.cs index c7bcf7b8e0..54dbb0c05d 100644 --- a/Source/DafnyCore/GeneratedFromDafny/Std_Strings_CharStrEscaping.cs +++ b/Source/DafnyCore/GeneratedFromDafny/Std_Strings_CharStrEscaping.cs @@ -1,7 +1,7 @@ // Dafny program the_program compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyCore/GeneratedFromDafny/Std_Strings_DecimalConversion.cs b/Source/DafnyCore/GeneratedFromDafny/Std_Strings_DecimalConversion.cs index a408b17251..3d3cb3c89d 100644 --- a/Source/DafnyCore/GeneratedFromDafny/Std_Strings_DecimalConversion.cs +++ b/Source/DafnyCore/GeneratedFromDafny/Std_Strings_DecimalConversion.cs @@ -1,7 +1,7 @@ // Dafny program the_program compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyCore/GeneratedFromDafny/Std_Strings_HexConversion.cs b/Source/DafnyCore/GeneratedFromDafny/Std_Strings_HexConversion.cs index 57a20d539c..0217a2ac0c 100644 --- a/Source/DafnyCore/GeneratedFromDafny/Std_Strings_HexConversion.cs +++ b/Source/DafnyCore/GeneratedFromDafny/Std_Strings_HexConversion.cs @@ -1,7 +1,7 @@ // Dafny program the_program compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyCore/GeneratedFromDafny/Std_Wrappers.cs b/Source/DafnyCore/GeneratedFromDafny/Std_Wrappers.cs index bd2a8af634..6d224dc262 100644 --- a/Source/DafnyCore/GeneratedFromDafny/Std_Wrappers.cs +++ b/Source/DafnyCore/GeneratedFromDafny/Std_Wrappers.cs @@ -1,7 +1,7 @@ // Dafny program the_program compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyCore/Generic/DafnyDiagnostic.cs b/Source/DafnyCore/Generic/DafnyDiagnostic.cs new file mode 100644 index 0000000000..71f016ede9 --- /dev/null +++ b/Source/DafnyCore/Generic/DafnyDiagnostic.cs @@ -0,0 +1,59 @@ +#nullable enable +using System; +using System.Collections.Generic; + +namespace Microsoft.Dafny; + +public record DafnyDiagnostic(MessageSource Source, string ErrorId, IOrigin Token, string Message, ErrorLevel Level, + IReadOnlyList RelatedInformation) : IComparable { + public int CompareTo(DafnyDiagnostic? other) { + if (other == null) { + return 1; + } + var r0 = OriginCenterComparer.Instance.Compare(Token, other.Token); + if (r0 != 0) { + return r0; + } + + for (var index = 0; index < RelatedInformation.Count; index++) { + if (other.RelatedInformation.Count > index) { + var r1 = RelatedInformation[index].Token.Center.CompareTo(other.RelatedInformation[index].Token.Center); + if (r1 != 0) { + return r1; + } + } else { + return 1; + } + } + + if (other.RelatedInformation.Count > RelatedInformation.Count) { + return -1; + } + + return 0; + } +} + +class OriginCenterComparer : IComparer { + public static readonly OriginCenterComparer Instance = new(); + + public int Compare(IOrigin? x, IOrigin? y) { + if (x == null) { + return -1; + } + + if (y == null) { + return 1; + } + + if (x is NestedOrigin nestedX && y is NestedOrigin nestedY) { + var outer = Compare(nestedX.Outer, nestedY.Outer); + if (outer != 0) { + return outer; + } + + return Compare(nestedX.Inner, nestedY.Inner); + } + return x.Center.CompareTo(y.Center); + } +} \ No newline at end of file diff --git a/Source/DafnyCore/Generic/Reporting.cs b/Source/DafnyCore/Generic/Reporting.cs index def369b167..de600c10c7 100644 --- a/Source/DafnyCore/Generic/Reporting.cs +++ b/Source/DafnyCore/Generic/Reporting.cs @@ -1,7 +1,6 @@ // Copyright by the contributors to the Dafny Project // SPDX-License-Identifier: MIT #nullable enable -using System.Collections.Generic; using System.CommandLine; using System.Linq; @@ -16,8 +15,6 @@ public enum MessageSource { } public record DafnyRelatedInformation(IOrigin Token, string Message); - public record DafnyDiagnostic(MessageSource Source, string ErrorId, IOrigin Token, string Message, ErrorLevel Level, - IReadOnlyList RelatedInformation); public class ErrorReporterSink : ErrorReporter { public ErrorReporterSink(DafnyOptions options) : base(options) { } diff --git a/Source/DafnyDriver.Test/DafnyDriver.Test.csproj b/Source/DafnyDriver.Test/DafnyDriver.Test.csproj index b1681b47cb..670c6f2ec6 100644 --- a/Source/DafnyDriver.Test/DafnyDriver.Test.csproj +++ b/Source/DafnyDriver.Test/DafnyDriver.Test.csproj @@ -1,7 +1,6 @@ - net6.0 enable enable diff --git a/Source/DafnyDriver.Test/LanguageServerProcessTest.cs b/Source/DafnyDriver.Test/LanguageServerProcessTest.cs index d42c8f4d26..a180c2401a 100644 --- a/Source/DafnyDriver.Test/LanguageServerProcessTest.cs +++ b/Source/DafnyDriver.Test/LanguageServerProcessTest.cs @@ -204,10 +204,10 @@ public static async Task Main(string[] args) {{ var configuration = JsonSerializer.Serialize( new { runtimeOptions = new { - tfm = "net6.0", + tfm = "net8.0", framework = new { name = "Microsoft.NETCore.App", - version = "6.0.0", + version = "8.0.0", rollForward = "LatestMinor" } } diff --git a/Source/DafnyDriver/Commands/VerifyCommand.cs b/Source/DafnyDriver/Commands/VerifyCommand.cs index ff8ca57160..789db4ee4b 100644 --- a/Source/DafnyDriver/Commands/VerifyCommand.cs +++ b/Source/DafnyDriver/Commands/VerifyCommand.cs @@ -193,13 +193,13 @@ public static void ReportVerificationDiagnostics(CliCompilation compilation, IOb completed.Result, batchReporter); } - foreach (var diagnostic in batchReporter.AllMessages.OrderBy(m => m.Token.Center)) { + foreach (var diagnostic in batchReporter.AllMessages.Order()) { compilation.Compilation.Reporter.Message(diagnostic.Source, diagnostic.Level, diagnostic.ErrorId, diagnostic.Token, diagnostic.Message); } }); - } + } public static async Task LogVerificationResults(CliCompilation cliCompilation, ResolutionResult resolution, IObservable verificationResults) { diff --git a/Source/DafnyDriver/DafnyDriver.csproj b/Source/DafnyDriver/DafnyDriver.csproj index d7655e6767..f928e3f504 100644 --- a/Source/DafnyDriver/DafnyDriver.csproj +++ b/Source/DafnyDriver/DafnyDriver.csproj @@ -5,8 +5,7 @@ DafnyDriver false TRACE - net6.0 -Major + Major ..\..\Binaries\ false @@ -15,7 +14,7 @@ true - + false false diff --git a/Source/DafnyLanguageServer.Test/DafnyLanguageServer.Test.csproj b/Source/DafnyLanguageServer.Test/DafnyLanguageServer.Test.csproj index e25f0c91a9..16d4a63d5f 100644 --- a/Source/DafnyLanguageServer.Test/DafnyLanguageServer.Test.csproj +++ b/Source/DafnyLanguageServer.Test/DafnyLanguageServer.Test.csproj @@ -1,7 +1,6 @@  - net6.0 false Microsoft.Dafny.LanguageServer.IntegrationTest diff --git a/Source/DafnyLanguageServer.Test/Performance/LargeFilesTest.cs b/Source/DafnyLanguageServer.Test/Performance/LargeFilesTest.cs index 359ab1ee16..62c857c220 100644 --- a/Source/DafnyLanguageServer.Test/Performance/LargeFilesTest.cs +++ b/Source/DafnyLanguageServer.Test/Performance/LargeFilesTest.cs @@ -68,7 +68,7 @@ public async Task QuickEditsInLargeFile() { var afterChange = DateTime.Now; var changeMilliseconds = (afterChange - afterOpen).TotalMilliseconds; await AssertNoDiagnosticsAreComing(CancellationTokenWithHighTimeout); - threadPoolSchedulingCancellationToken.Cancel(); + await threadPoolSchedulingCancellationToken.CancelAsync(); var averageTimeToSchedule = await threadPoolSchedulingTimeTask; var division = changeMilliseconds / openMilliseconds; @@ -124,4 +124,4 @@ await Task.Run(() => { public LargeFilesTest(ITestOutputHelper output) : base(output) { } -} \ No newline at end of file +} diff --git a/Source/DafnyLanguageServer/DafnyLanguageServer.csproj b/Source/DafnyLanguageServer/DafnyLanguageServer.csproj index 756bb1eb5a..67513425d4 100644 --- a/Source/DafnyLanguageServer/DafnyLanguageServer.csproj +++ b/Source/DafnyLanguageServer/DafnyLanguageServer.csproj @@ -1,8 +1,7 @@  - net6.0 -Major + Major true enable Microsoft.Dafny.LanguageServer @@ -13,7 +12,7 @@ README.md - + false false diff --git a/Source/DafnyLanguageServer/Language/CachingParser.cs b/Source/DafnyLanguageServer/Language/CachingParser.cs index 5a2ec13606..9973bea587 100644 --- a/Source/DafnyLanguageServer/Language/CachingParser.cs +++ b/Source/DafnyLanguageServer/Language/CachingParser.cs @@ -36,7 +36,7 @@ protected override DfyParseFileResult ParseFile(DafnyOptions options, FileSnapsh // Add NUL delimiter to avoid collisions (otherwise hash("A" + "BC") == hash("AB" + "C")) var uriBytes = Encoding.UTF8.GetBytes(uri + "\0"); - var (newReader, hash) = ComputeHashFromReader(uriBytes, reader, HashAlgorithm.Create("SHA256")!); + var (newReader, hash) = ComputeHashFromReader(uriBytes, reader, SHA256.Create()!); if (!parseCache.TryGet(hash, out var result)) { logger.LogDebug($"Parse cache miss for {uri}"); result = base.ParseFile(options, fileSnapshot with { Reader = newReader }, uri, cancellationToken); @@ -84,4 +84,4 @@ private static (TextReader reader, byte[] hash) ComputeHashFromReader(byte[] sta result.Add(chunk); } } -} \ No newline at end of file +} diff --git a/Source/DafnyLanguageServer/Language/CachingResolver.cs b/Source/DafnyLanguageServer/Language/CachingResolver.cs index 1bfc902126..1418549d18 100644 --- a/Source/DafnyLanguageServer/Language/CachingResolver.cs +++ b/Source/DafnyLanguageServer/Language/CachingResolver.cs @@ -75,7 +75,7 @@ protected override ModuleResolutionResult ResolveModuleDeclaration(CompilationDa private byte[] GetHash(ModuleDecl moduleDeclaration) { if (!hashes.TryGetValue(moduleDeclaration, out var result)) { var moduleVertex = dependencies.FindVertex(moduleDeclaration); - var hashAlgorithm = HashAlgorithm.Create("SHA256")!; + var hashAlgorithm = SHA256.Create()!; hashAlgorithm.Initialize(); // We don't want the order of Successors to influence the hash, so we order by the content hash, for which CloneId is currently a proxy var orderedSuccessors = moduleVertex.Successors.OrderBy(s => s.N.CloneId); @@ -98,4 +98,4 @@ private byte[] GetHash(ModuleDecl moduleDeclaration) { return result; } -} \ No newline at end of file +} diff --git a/Source/DafnyPipeline.Test/DafnyPipeline.Test.csproj b/Source/DafnyPipeline.Test/DafnyPipeline.Test.csproj index a98109beba..34ec4c877a 100644 --- a/Source/DafnyPipeline.Test/DafnyPipeline.Test.csproj +++ b/Source/DafnyPipeline.Test/DafnyPipeline.Test.csproj @@ -1,7 +1,6 @@ - net6.0 false diff --git a/Source/DafnyPipeline.Test/ProverLogStability.cs b/Source/DafnyPipeline.Test/ProverLogStability.cs index 7931d8118e..18b4e529a7 100644 --- a/Source/DafnyPipeline.Test/ProverLogStability.cs +++ b/Source/DafnyPipeline.Test/ProverLogStability.cs @@ -119,7 +119,7 @@ public async Task ProverLogRegression() { var regularProverLog = await GetProverLogForProgramAsync(options, await GetBoogie(options, originalProgram)); regularProverLog = regularProverLog.Replace("\r", ""); if (updateProverLog) { - var path = Path.GetFullPath(filePath).Replace("bin" + Path.DirectorySeparatorChar + "Debug" + Path.DirectorySeparatorChar + "net6.0" + Path.DirectorySeparatorChar, ""); + var path = Path.GetFullPath(filePath).Replace("bin" + Path.DirectorySeparatorChar + "Debug" + Path.DirectorySeparatorChar + "net8.0" + Path.DirectorySeparatorChar, ""); await File.WriteAllTextAsync(path, regularProverLog); await Console.Out.WriteLineAsync("Updated prover log file at " + path); } else { diff --git a/Source/DafnyPipeline/DafnyPipeline.csproj b/Source/DafnyPipeline/DafnyPipeline.csproj index 759c23f348..559c7781cb 100644 --- a/Source/DafnyPipeline/DafnyPipeline.csproj +++ b/Source/DafnyPipeline/DafnyPipeline.csproj @@ -7,12 +7,11 @@ false ..\..\Binaries\ TRACE - net6.0 -Major + Major MIT - + false false diff --git a/Source/DafnyRuntime.Tests/DafnyRuntime.Tests.csproj b/Source/DafnyRuntime.Tests/DafnyRuntime.Tests.csproj index f90c85ef0b..bc05a98a47 100644 --- a/Source/DafnyRuntime.Tests/DafnyRuntime.Tests.csproj +++ b/Source/DafnyRuntime.Tests/DafnyRuntime.Tests.csproj @@ -1,7 +1,6 @@ - net6.0 enable false diff --git a/Source/DafnyRuntime/DafnyRuntime.csproj b/Source/DafnyRuntime/DafnyRuntime.csproj index 3943da7ce0..8cfbf6fab4 100644 --- a/Source/DafnyRuntime/DafnyRuntime.csproj +++ b/Source/DafnyRuntime/DafnyRuntime.csproj @@ -6,6 +6,7 @@ true false TRACE;ISDAFNYRUNTIMELIB + netstandard2.0;net452 ..\..\Binaries\ 7.3 diff --git a/Source/DafnyRuntime/DafnyRuntimeSystemModule.cs b/Source/DafnyRuntime/DafnyRuntimeSystemModule.cs index b5b6988b13..d0e8ea5dea 100644 --- a/Source/DafnyRuntime/DafnyRuntimeSystemModule.cs +++ b/Source/DafnyRuntime/DafnyRuntimeSystemModule.cs @@ -1,7 +1,7 @@ // Dafny program systemModulePopulator.dfy compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyServer/DafnyServer.csproj b/Source/DafnyServer/DafnyServer.csproj index 38ee3311f2..d736ee1074 100644 --- a/Source/DafnyServer/DafnyServer.csproj +++ b/Source/DafnyServer/DafnyServer.csproj @@ -5,13 +5,12 @@ DafnyServer false TRACE - net6.0 -Major + Major ..\..\Binaries\ MIT - + false false diff --git a/Source/DafnyServer/SuperLegacySymbolTable.cs b/Source/DafnyServer/SuperLegacySymbolTable.cs index f394a28b07..acec53486a 100644 --- a/Source/DafnyServer/SuperLegacySymbolTable.cs +++ b/Source/DafnyServer/SuperLegacySymbolTable.cs @@ -227,9 +227,7 @@ private static void ParseUpdateStatement(Statement statement, List(); - var rightSideDots = rightSide.OfType(); - var allExprDotNames = leftSideDots.Concat(rightSideDots); + var allExprDotNames = leftSide.OfType(); foreach (var exprDotName in allExprDotNames) { if (!(exprDotName.Lhs.Type is UserDefinedType)) { continue; @@ -304,12 +302,8 @@ private static IEnumerable ParseBodyForFieldReferences(IEn var updateStmt = (AssignStatement)statement; var leftSide = updateStmt.Lhss; var rightSide = updateStmt.Rhss; - var leftSideDots = leftSide.OfType(); - var rightSideDots = rightSide.OfType(); - var exprDotNames = leftSideDots.Concat(rightSideDots); - var leftSideNameSegments = leftSide.OfType(); - var rightSideNameSegments = rightSide.OfType(); - var nameSegments = leftSideNameSegments.Concat(rightSideNameSegments); + var exprDotNames = leftSide.OfType(); + var nameSegments = leftSide.OfType(); var allRightSideExpressions = rightSide.SelectMany(e => e.SubExpressions.SelectMany(GetAllSubExpressions)); var allLeftSideExpressions = leftSide.SelectMany(e => e.SubExpressions.SelectMany(GetAllSubExpressions)); diff --git a/Source/DafnyTestGeneration.Test/DafnyTestGeneration.Test.csproj b/Source/DafnyTestGeneration.Test/DafnyTestGeneration.Test.csproj index b4920e5881..1ec68cb84b 100644 --- a/Source/DafnyTestGeneration.Test/DafnyTestGeneration.Test.csproj +++ b/Source/DafnyTestGeneration.Test/DafnyTestGeneration.Test.csproj @@ -1,7 +1,6 @@ - net6.0 false diff --git a/Source/DafnyTestGeneration/DafnyTestGeneration.csproj b/Source/DafnyTestGeneration/DafnyTestGeneration.csproj index 6631561a0e..016cf01c49 100644 --- a/Source/DafnyTestGeneration/DafnyTestGeneration.csproj +++ b/Source/DafnyTestGeneration/DafnyTestGeneration.csproj @@ -8,8 +8,7 @@ ..\..\Binaries\ true TRACE - net6.0 -Major + Major enable false MIT diff --git a/Source/Directory.Build.props b/Source/Directory.Build.props index f7bb029a0e..3c096675bb 100644 --- a/Source/Directory.Build.props +++ b/Source/Directory.Build.props @@ -1,6 +1,7 @@ + net8.0 4.9.2 1701;1702;VSTHRD200 diff --git a/Source/IntegrationTests/IntegrationTests.csproj b/Source/IntegrationTests/IntegrationTests.csproj index 5370699a47..cfb699f062 100644 --- a/Source/IntegrationTests/IntegrationTests.csproj +++ b/Source/IntegrationTests/IntegrationTests.csproj @@ -1,7 +1,6 @@ - net6.0 true false enable diff --git a/Source/IntegrationTests/LitTests.cs b/Source/IntegrationTests/LitTests.cs index b91a4b5fa4..11e8f226ed 100644 --- a/Source/IntegrationTests/LitTests.cs +++ b/Source/IntegrationTests/LitTests.cs @@ -25,7 +25,7 @@ public class LitTests { private static readonly Assembly TestDafnyAssembly = typeof(MultiBackendTest).Assembly; private static readonly Assembly DafnyServerAssembly = typeof(Server).Assembly; - private static readonly string RepositoryRoot = Path.GetFullPath("../../../../../"); // Up from Source/IntegrationTests/bin/Debug/net6.0/ + private static readonly string RepositoryRoot = Path.GetFullPath("../../../../../"); // Up from Source/IntegrationTests/bin/Debug/net8.0/ private static readonly string[] DefaultBoogieArguments = new[] { "/infer:j", diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/DafnyTests/RunAllTests/RunAllTests.csproj b/Source/IntegrationTests/TestFiles/LitTests/LitTest/DafnyTests/RunAllTests/RunAllTests.csproj index d8b5e8b41a..eefc01ebbe 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/DafnyTests/RunAllTests/RunAllTests.csproj +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/DafnyTests/RunAllTests/RunAllTests.csproj @@ -2,7 +2,7 @@ Exe - net6.0 + net8.0 false diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/DafnyTests/TestAttribute/TestAttribute.csproj b/Source/IntegrationTests/TestFiles/LitTests/LitTest/DafnyTests/TestAttribute/TestAttribute.csproj index 768e4f6f82..58a723cd45 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/DafnyTests/TestAttribute/TestAttribute.csproj +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/DafnyTests/TestAttribute/TestAttribute.csproj @@ -1,7 +1,7 @@  - net6.0 + net8.0 diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/manualcompile/ManualCompile.csproj b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/manualcompile/ManualCompile.csproj index 41f1d5ad4b..a269962b55 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/manualcompile/ManualCompile.csproj +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/manualcompile/ManualCompile.csproj @@ -2,7 +2,7 @@ Exe - net6.0 + net8.0 diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/manualcompile/ManualCompile.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/manualcompile/ManualCompile.dfy index b521245c0d..7adf33da4c 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/manualcompile/ManualCompile.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/manualcompile/ManualCompile.dfy @@ -2,7 +2,7 @@ // RUN: %translate cs --verbose --include-runtime "%s" > "%t" // RUN: dotnet build %S/ManualCompile.csproj -// RUN: dotnet %S/bin/Debug/net6.0/ManualCompile.dll >> "%t" +// RUN: dotnet %S/bin/Debug/net8.0/ManualCompile.dll >> "%t" // RUN: %translate js --verbose --include-runtime "%s" >> "%t" // RUN: node %S/ManualCompile.js >> "%t" diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/consumer/Consumer.csproj b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/consumer/Consumer.csproj index e6bb653223..b32966d460 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/consumer/Consumer.csproj +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/consumer/Consumer.csproj @@ -2,7 +2,7 @@ - net6.0 + net8.0 Exe diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/AutoReq.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/AutoReq.dfy.expect index a1ede7a970..f149c64f7b 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/AutoReq.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/AutoReq.dfy.expect @@ -2,16 +2,16 @@ AutoReq.dfy(13,2): Error: function precondition could not be proved AutoReq.dfy(5,13): Related location: this proposition could not be proved AutoReq.dfy(25,2): Error: function precondition could not be proved AutoReq.dfy(5,13): Related location: this proposition could not be proved +AutoReq.dfy(38,11): Error: function precondition could not be proved +AutoReq.dfy(5,13): Related location: this proposition could not be proved AutoReq.dfy(38,11): Error: assertion might not hold AutoReq.dfy(31,12): Related location: this proposition could not be proved AutoReq.dfy(7,4): Related location: this proposition could not be proved -AutoReq.dfy(38,11): Error: function precondition could not be proved +AutoReq.dfy(40,11): Error: function precondition could not be proved AutoReq.dfy(5,13): Related location: this proposition could not be proved AutoReq.dfy(40,11): Error: assertion might not hold AutoReq.dfy(31,26): Related location: this proposition could not be proved AutoReq.dfy(7,4): Related location: this proposition could not be proved -AutoReq.dfy(40,11): Error: function precondition could not be proved -AutoReq.dfy(5,13): Related location: this proposition could not be proved AutoReq.dfy(45,11): Error: assertion might not hold AutoReq.dfy(31,12): Related location: this proposition could not be proved AutoReq.dfy(7,4): Related location: this proposition could not be proved diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Fuel.legacy.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Fuel.dfy similarity index 99% rename from Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Fuel.legacy.dfy rename to Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Fuel.dfy index 91e3ea6426..ce78a8795b 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Fuel.legacy.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Fuel.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 4 %dafny /compile:0 /deprecation:0 /autoTriggers:0 /optimizeResolution:0 /errorLimit:0 "%s" > "%t" +// RUN: %exits-with 4 %verify --allow-deprecation --manual-triggers --error-limit 0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" module TestModule1 { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Fuel.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Fuel.dfy.expect new file mode 100755 index 0000000000..9263a74096 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Fuel.dfy.expect @@ -0,0 +1,67 @@ +Fuel.dfy(17,22): Error: assertion might not hold +Fuel.dfy(66,27): Error: assertion might not hold +Fuel.dfy(71,27): Error: assertion might not hold +Fuel.dfy(92,22): Error: assertion might not hold +Fuel.dfy(93,23): Error: assertion might not hold +Fuel.dfy(94,22): Error: assertion might not hold +Fuel.dfy(129,8): Error: Fuel can only increase within a given scope. +Fuel.dfy(120,22): Error: assertion might not hold +Fuel.dfy(121,23): Error: assertion might not hold +Fuel.dfy(122,22): Error: assertion might not hold +Fuel.dfy(132,26): Error: assertion might not hold +Fuel.dfy(133,26): Error: assertion might not hold +Fuel.dfy(157,22): Error: assertion might not hold +Fuel.dfy(200,55): Error: assertion might not hold +Fuel.dfy(245,22): Error: assertion might not hold +Fuel.dfy(247,22): Error: assertion might not hold +Fuel.dfy(280,26): Error: assertion might not hold +Fuel.dfy(335,26): Error: function precondition could not be proved +Fuel.dfy(324,21): Related location: this proposition could not be proved +Fuel.dfy(312,43): Related location: this proposition could not be proved +Fuel.dfy(335,26): Error: function precondition could not be proved +Fuel.dfy(324,21): Related location: this proposition could not be proved +Fuel.dfy(312,58): Related location: this proposition could not be proved +Fuel.dfy(335,26): Error: function precondition could not be proved +Fuel.dfy(324,21): Related location: this proposition could not be proved +Fuel.dfy(313,41): Related location: this proposition could not be proved +Fuel.dfy(335,26): Error: function precondition could not be proved +Fuel.dfy(324,21): Related location: this proposition could not be proved +Fuel.dfy(314,46): Related location: this proposition could not be proved +Fuel.dfy(335,26): Error: function precondition could not be proved +Fuel.dfy(324,21): Related location: this proposition could not be proved +Fuel.dfy(314,72): Related location: this proposition could not be proved +Fuel.dfy(335,26): Error: function precondition could not be proved +Fuel.dfy(324,21): Related location: this proposition could not be proved +Fuel.dfy(314,93): Related location: this proposition could not be proved +Fuel.dfy(335,49): Error: destructor 't' can only be applied to datatype values constructed by 'VTuple' +Fuel.dfy(335,50): Error: index out of range +Fuel.dfy(336,38): Error: index out of range +Fuel.dfy(336,42): Error: destructor 'u' can only be applied to datatype values constructed by 'VUint64' +Fuel.dfy(336,45): Error: function precondition could not be proved +Fuel.dfy(329,21): Related location: this proposition could not be proved +Fuel.dfy(311,43): Related location: this proposition could not be proved +Fuel.dfy(336,45): Error: function precondition could not be proved +Fuel.dfy(329,21): Related location: this proposition could not be proved +Fuel.dfy(312,43): Related location: this proposition could not be proved +Fuel.dfy(336,45): Error: function precondition could not be proved +Fuel.dfy(329,21): Related location: this proposition could not be proved +Fuel.dfy(312,58): Related location: this proposition could not be proved +Fuel.dfy(336,45): Error: function precondition could not be proved +Fuel.dfy(329,21): Related location: this proposition could not be proved +Fuel.dfy(313,41): Related location: this proposition could not be proved +Fuel.dfy(336,45): Error: function precondition could not be proved +Fuel.dfy(329,21): Related location: this proposition could not be proved +Fuel.dfy(314,72): Related location: this proposition could not be proved +Fuel.dfy(336,45): Error: function precondition could not be proved +Fuel.dfy(329,21): Related location: this proposition could not be proved +Fuel.dfy(314,93): Related location: this proposition could not be proved +Fuel.dfy(336,71): Error: index out of range +Fuel.dfy(407,8): Error: Fuel can only increase within a given scope. +Fuel.dfy(397,22): Error: assertion might not hold +Fuel.dfy(398,22): Error: assertion might not hold +Fuel.dfy(399,23): Error: assertion might not hold +Fuel.dfy(435,22): Error: assertion might not hold +Fuel.dfy(436,22): Error: assertion might not hold +Fuel.dfy(437,23): Error: assertion might not hold + +Dafny program verifier finished with 31 verified, 39 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Fuel.legacy.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Fuel.legacy.dfy.expect deleted file mode 100755 index c5a06552f2..0000000000 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Fuel.legacy.dfy.expect +++ /dev/null @@ -1,67 +0,0 @@ -Fuel.legacy.dfy(129,8): Error: Fuel can only increase within a given scope. -Fuel.legacy.dfy(407,8): Error: Fuel can only increase within a given scope. -Fuel.legacy.dfy(17,22): Error: assertion might not hold -Fuel.legacy.dfy(66,27): Error: assertion might not hold -Fuel.legacy.dfy(71,27): Error: assertion might not hold -Fuel.legacy.dfy(92,22): Error: assertion might not hold -Fuel.legacy.dfy(93,23): Error: assertion might not hold -Fuel.legacy.dfy(94,22): Error: assertion might not hold -Fuel.legacy.dfy(120,22): Error: assertion might not hold -Fuel.legacy.dfy(121,23): Error: assertion might not hold -Fuel.legacy.dfy(122,22): Error: assertion might not hold -Fuel.legacy.dfy(132,26): Error: assertion might not hold -Fuel.legacy.dfy(133,26): Error: assertion might not hold -Fuel.legacy.dfy(157,22): Error: assertion might not hold -Fuel.legacy.dfy(200,55): Error: assertion might not hold -Fuel.legacy.dfy(245,22): Error: assertion might not hold -Fuel.legacy.dfy(247,22): Error: assertion might not hold -Fuel.legacy.dfy(280,26): Error: assertion might not hold -Fuel.legacy.dfy(335,26): Error: function precondition could not be proved -Fuel.legacy.dfy(324,21): Related location -Fuel.legacy.dfy(313,41): Related location -Fuel.legacy.dfy(335,26): Error: function precondition could not be proved -Fuel.legacy.dfy(324,21): Related location -Fuel.legacy.dfy(314,72): Related location -Fuel.legacy.dfy(335,26): Error: function precondition could not be proved -Fuel.legacy.dfy(324,21): Related location -Fuel.legacy.dfy(314,93): Related location -Fuel.legacy.dfy(335,26): Error: function precondition could not be proved -Fuel.legacy.dfy(324,21): Related location -Fuel.legacy.dfy(314,46): Related location -Fuel.legacy.dfy(335,26): Error: function precondition could not be proved -Fuel.legacy.dfy(324,21): Related location -Fuel.legacy.dfy(312,43): Related location -Fuel.legacy.dfy(335,26): Error: function precondition could not be proved -Fuel.legacy.dfy(324,21): Related location -Fuel.legacy.dfy(312,58): Related location -Fuel.legacy.dfy(335,49): Error: destructor 't' can only be applied to datatype values constructed by 'VTuple' -Fuel.legacy.dfy(335,50): Error: index out of range -Fuel.legacy.dfy(336,38): Error: index out of range -Fuel.legacy.dfy(336,42): Error: destructor 'u' can only be applied to datatype values constructed by 'VUint64' -Fuel.legacy.dfy(336,45): Error: function precondition could not be proved -Fuel.legacy.dfy(329,21): Related location -Fuel.legacy.dfy(311,43): Related location -Fuel.legacy.dfy(336,45): Error: function precondition could not be proved -Fuel.legacy.dfy(329,21): Related location -Fuel.legacy.dfy(314,93): Related location -Fuel.legacy.dfy(336,45): Error: function precondition could not be proved -Fuel.legacy.dfy(329,21): Related location -Fuel.legacy.dfy(312,58): Related location -Fuel.legacy.dfy(336,45): Error: function precondition could not be proved -Fuel.legacy.dfy(329,21): Related location -Fuel.legacy.dfy(313,41): Related location -Fuel.legacy.dfy(336,45): Error: function precondition could not be proved -Fuel.legacy.dfy(329,21): Related location -Fuel.legacy.dfy(314,72): Related location -Fuel.legacy.dfy(336,45): Error: function precondition could not be proved -Fuel.legacy.dfy(329,21): Related location -Fuel.legacy.dfy(312,43): Related location -Fuel.legacy.dfy(336,71): Error: index out of range -Fuel.legacy.dfy(397,22): Error: assertion might not hold -Fuel.legacy.dfy(398,22): Error: assertion might not hold -Fuel.legacy.dfy(399,23): Error: assertion might not hold -Fuel.legacy.dfy(435,22): Error: assertion might not hold -Fuel.legacy.dfy(436,22): Error: assertion might not hold -Fuel.legacy.dfy(437,23): Error: assertion might not hold - -Dafny program verifier finished with 31 verified, 39 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Input/IncludesTuples.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Input/IncludesTuples.dfy index 480f19bf3c..daf58aae43 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Input/IncludesTuples.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Input/IncludesTuples.dfy @@ -1,6 +1,6 @@ // RUN: echo Input for Stdin.dfy // Note that the current directory for .NET tests is always the output directory // for the IntegrationTests project. -// i.e. something like IntegrationTests/bin/Debug/net6.0 +// i.e. something like IntegrationTests/bin/Debug/net8.0 include "TestFiles/LitTests/LitTest/dafny0/Tuples.dfy" \ No newline at end of file diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/one-message-per-failed-precondition.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/one-message-per-failed-precondition.dfy.expect index 730a9d00e3..5391422767 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/one-message-per-failed-precondition.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/one-message-per-failed-precondition.dfy.expect @@ -1,10 +1,10 @@ one-message-per-failed-precondition.dfy(13,3): Error: a precondition for this call could not be proved -one-message-per-failed-precondition.dfy(9,13): Related location: this is the precondition that could not be proved -one-message-per-failed-precondition.dfy(13,3): Error: a precondition for this call could not be proved one-message-per-failed-precondition.dfy(8,13): Related location: this is the precondition that could not be proved -one-message-per-failed-precondition.dfy(20,33): Error: function precondition could not be proved -one-message-per-failed-precondition.dfy(18,13): Related location: this proposition could not be proved +one-message-per-failed-precondition.dfy(13,3): Error: a precondition for this call could not be proved +one-message-per-failed-precondition.dfy(9,13): Related location: this is the precondition that could not be proved one-message-per-failed-precondition.dfy(20,33): Error: function precondition could not be proved one-message-per-failed-precondition.dfy(17,13): Related location: this proposition could not be proved +one-message-per-failed-precondition.dfy(20,33): Error: function precondition could not be proved +one-message-per-failed-precondition.dfy(18,13): Related location: this proposition could not be proved Dafny program verifier finished with 0 verified, 4 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/examples/Simple_compiler/Makefile b/Source/IntegrationTests/TestFiles/LitTests/LitTest/examples/Simple_compiler/Makefile index 9b695cffd4..662f746a70 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/examples/Simple_compiler/Makefile +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/examples/Simple_compiler/Makefile @@ -21,7 +21,7 @@ $(dafny_csharp_dir)/%.cs: %.dfy | $(dafny_csharp_dir) # Step 3: compile resulting C# project csproj := SimpleCompiler.csproj -csharp_dll := $(csharp_dir)/bin/Debug/net6.0/SimpleCompiler.dll +csharp_dll := $(csharp_dir)/bin/Debug/net8.0/SimpleCompiler.dll csharp_files := $(wildcard $(csharp_dir)/*) csharp_shared_deps := $(patsubst %,$(csharp_dir)/%,$(shared_deps)) csharp_dafny_deps := $(patsubst %.dfy,$(dafny_csharp_dir)/%.cs,$(dafny_files)) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/examples/Simple_compiler/csharp/SimpleCompiler.csproj b/Source/IntegrationTests/TestFiles/LitTests/LitTest/examples/Simple_compiler/csharp/SimpleCompiler.csproj index c3a9eccf93..bb542208d5 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/examples/Simple_compiler/csharp/SimpleCompiler.csproj +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/examples/Simple_compiler/csharp/SimpleCompiler.csproj @@ -2,9 +2,9 @@ Exe - net6.0 + net8.0 enable - CS3021; CS0162; CS0164 + CS8981; CS3021; CS0162; CS0164 diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2299.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2299.dfy.expect index 101c6a5a39..2bb07b70a7 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2299.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2299.dfy.expect @@ -7,13 +7,13 @@ git-issue-2299.dfy(21,4): Related location: this proposition could not be proved git-issue-2299.dfy(67,13): Error: assertion might not hold git-issue-2299.dfy(21,4): Related location: this proposition could not be proved git-issue-2299.dfy(81,11): Error: assertion might not hold +git-issue-2299.dfy(27,4): Related location: this proposition could not be proved +git-issue-2299.dfy(10,11): Related location: this proposition could not be proved +git-issue-2299.dfy(81,11): Error: assertion might not hold git-issue-2299.dfy(27,18): Related location: this proposition could not be proved git-issue-2299.dfy(16,4): Related location: this proposition could not be proved git-issue-2299.dfy(81,11): Error: assertion might not hold git-issue-2299.dfy(27,32): Related location: this proposition could not be proved git-issue-2299.dfy(21,4): Related location: this proposition could not be proved -git-issue-2299.dfy(81,11): Error: assertion might not hold -git-issue-2299.dfy(27,4): Related location: this proposition could not be proved -git-issue-2299.dfy(10,11): Related location: this proposition could not be proved Dafny program verifier finished with 7 verified, 7 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3549a.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3549a.dfy.expect index 32d93e22db..3ccac32363 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3549a.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3549a.dfy.expect @@ -1 +1 @@ -Invalid filename: The path is empty. (Parameter 'path') +Invalid filename: The value cannot be an empty string. (Parameter 'path') diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/InductionWithoutTriggers.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/InductionWithoutTriggers.dfy.expect index f049bcc234..4f6393dcb3 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/InductionWithoutTriggers.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/InductionWithoutTriggers.dfy.expect @@ -19,10 +19,10 @@ InductionWithoutTriggers.dfy(100,0): Error: a postcondition could not be proved InductionWithoutTriggers.dfy(99,10): Related location: this is the postcondition that could not be proved InductionWithoutTriggers.dfy(31,27): Related location: this proposition could not be proved InductionWithoutTriggers.dfy(124,0): Error: a postcondition could not be proved on this return path -InductionWithoutTriggers.dfy(123,18): Related location: this is the postcondition that could not be proved -InductionWithoutTriggers.dfy(35,27): Related location: this proposition could not be proved -InductionWithoutTriggers.dfy(124,0): Error: a postcondition could not be proved on this return path InductionWithoutTriggers.dfy(123,10): Related location: this is the postcondition that could not be proved InductionWithoutTriggers.dfy(31,27): Related location: this proposition could not be proved +InductionWithoutTriggers.dfy(124,0): Error: a postcondition could not be proved on this return path +InductionWithoutTriggers.dfy(123,18): Related location: this is the postcondition that could not be proved +InductionWithoutTriggers.dfy(35,27): Related location: this proposition could not be proved Dafny program verifier finished with 17 verified, 8 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/InductionWithoutTriggers.dfy.refresh.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/InductionWithoutTriggers.dfy.refresh.expect index 963b7041fd..566c53271f 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/InductionWithoutTriggers.dfy.refresh.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/InductionWithoutTriggers.dfy.refresh.expect @@ -19,10 +19,10 @@ InductionWithoutTriggers.dfy(100,0): Error: a postcondition could not be proved InductionWithoutTriggers.dfy(99,10): Related location: this is the postcondition that could not be proved InductionWithoutTriggers.dfy(31,27): Related location: this proposition could not be proved InductionWithoutTriggers.dfy(124,0): Error: a postcondition could not be proved on this return path -InductionWithoutTriggers.dfy(123,18): Related location: this is the postcondition that could not be proved -InductionWithoutTriggers.dfy(35,27): Related location: this proposition could not be proved -InductionWithoutTriggers.dfy(124,0): Error: a postcondition could not be proved on this return path InductionWithoutTriggers.dfy(123,10): Related location: this is the postcondition that could not be proved InductionWithoutTriggers.dfy(31,27): Related location: this proposition could not be proved +InductionWithoutTriggers.dfy(124,0): Error: a postcondition could not be proved on this return path +InductionWithoutTriggers.dfy(123,18): Related location: this is the postcondition that could not be proved +InductionWithoutTriggers.dfy(35,27): Related location: this proposition could not be proved Dafny program verifier finished with 12 verified, 8 errors diff --git a/Source/TestDafny/TestDafny.csproj b/Source/TestDafny/TestDafny.csproj index 83f292e792..4865653669 100644 --- a/Source/TestDafny/TestDafny.csproj +++ b/Source/TestDafny/TestDafny.csproj @@ -2,7 +2,7 @@ Exe - net6.0 + net8.0 enable enable false diff --git a/Source/XUnitExtensions/Lit/DiffCommand.cs b/Source/XUnitExtensions/Lit/DiffCommand.cs index ad79003bfe..f4060abbfb 100644 --- a/Source/XUnitExtensions/Lit/DiffCommand.cs +++ b/Source/XUnitExtensions/Lit/DiffCommand.cs @@ -35,7 +35,7 @@ public static ILitCommand Parse(string[] args) { if (Path.GetExtension(expectedOutputFile) == ".tmp") { return "With DAFNY_INTEGRATION_TESTS_UPDATE_EXPECT_FILE=true, first argument of %diff cannot be a *.tmp file, it should be an *.expect file"; } - var path = Path.GetFullPath(expectedOutputFile).Replace("bin" + Path.DirectorySeparatorChar + "Debug" + Path.DirectorySeparatorChar + "net6.0" + Path.DirectorySeparatorChar, ""); + var path = Path.GetFullPath(expectedOutputFile).Replace("bin" + Path.DirectorySeparatorChar + "Debug" + Path.DirectorySeparatorChar + "net8.0" + Path.DirectorySeparatorChar, ""); File.WriteAllText(path, actualOutput); return null; } diff --git a/Source/XUnitExtensions/XUnitExtensions.csproj b/Source/XUnitExtensions/XUnitExtensions.csproj index 3ff901352c..3ee91d23d0 100644 --- a/Source/XUnitExtensions/XUnitExtensions.csproj +++ b/Source/XUnitExtensions/XUnitExtensions.csproj @@ -1,7 +1,7 @@ - net6.0 + net8.0 false enable diff --git a/customBoogie.patch b/customBoogie.patch index 911dc435a4..9887a91122 100644 --- a/customBoogie.patch +++ b/customBoogie.patch @@ -73,6 +73,6 @@ index 4a8b2f89b..a308be9bf 100644 + + + - + diff --git a/docs/DafnyRef/Plugins.md b/docs/DafnyRef/Plugins.md index 6cb7c29f1d..c044914d6a 100644 --- a/docs/DafnyRef/Plugins.md +++ b/docs/DafnyRef/Plugins.md @@ -230,6 +230,6 @@ That's it! Now, build your library while inside your folder: > dotnet build ``` -This will create the file `PluginTutorial/bin/Debug/net6.0/PluginTutorial.dll`. +This will create the file `PluginTutorial/bin/Debug/net8.0/PluginTutorial.dll`. Now, open VSCode, open Dafny settings, and enter the absolute path to this DLL in the plugins section. Restart VSCode, and it should work! diff --git a/docs/DafnyRef/UserGuide.md b/docs/DafnyRef/UserGuide.md index 156cb2b049..578b63c692 100644 --- a/docs/DafnyRef/UserGuide.md +++ b/docs/DafnyRef/UserGuide.md @@ -2732,7 +2732,7 @@ If you have Boogie installed locally, you can run the printed Boogie file with t DOTNET=$(which dotnet) BOOGIE_ROOT="path/to/boogie/Source" -BOOGIE="$BOOGIE_ROOT/BoogieDriver/bin/Debug/net6.0/BoogieDriver.dll" +BOOGIE="$BOOGIE_ROOT/BoogieDriver/bin/Debug/net8.0/BoogieDriver.dll" if [[ ! -x "$DOTNET" ]]; then echo "Error: Dafny requires .NET Core to run on non-Windows systems." diff --git a/docs/Installation.md b/docs/Installation.md index edecd0f392..991e4b06b4 100644 --- a/docs/Installation.md +++ b/docs/Installation.md @@ -15,7 +15,7 @@ are in the [Dafny project wiki](https://github.com/dafny-lang/dafny/wiki/INSTALL System Requirements =================== -The `dafny tool` is a .NET 6.0 artifact, but it compiles to native executables on supported platforms. +The `dafny tool` is a .NET 8.0 artifact, but it compiles to native executables on supported platforms. That and the Z3 tool are all that is needed to use dafny for verification; additional tools are need for compilation, as described below. @@ -41,7 +41,7 @@ In addition, the Dafny toolkit supplies runtime libraries, either in source form ### C# - Dafny targeting C# produces C#10-compatible source code. -- Only the .NET 6.0 set of tools (which includes the C# compiler) is needed to compile and run the generated C# code. +- Only the .NET 8.0 set of tools (which includes the C# compiler) is needed to compile and run the generated C# code. - The Dafny runtime library is included as C# source along with the generated C# code, so the user can compile those sources and any user code in one project. @@ -86,9 +86,9 @@ For most users, we recommend using Dafny with VS Code, which has an easy install ## Visual Studio Code {#Visual-Studio-Code} 0. Install [Visual Studio Code](https://code.visualstudio.com/) -1. If you are on a Mac or Linux, install .NET 6.0, as described under those platforms below. +1. If you are on a Mac or Linux, install .NET 8.0, as described under those platforms below. 2. In Visual Studio Code, press `Ctrl+P` (or `⌘P` on a Mac), and enter `ext install dafny-lang.ide-vscode`. -3. If you open a `.dfy` file, Dafny VSCode will offer to download and install the latest Dafny. You can also browse extensions: +3. If you open a `.dfy` file, Dafny VSCode will offer to download and install the latest Dafny. You can also browse extensions: ![vs-code-dafny-2 0 1-install](https://user-images.githubusercontent.com/3601079/141353551-5cb5e23b-5536-47be-ba17-e5af494b775c.gif) ## Emacs {#Emacs} @@ -118,7 +118,7 @@ install the correct dependencies for the desired language. To install Dafny on your own machine, -* Install (if not already present) .NET Core 6.0: `https://dotnet.microsoft.com/download/dotnet/6.0` +* Install (if not already present) .NET Core 8.0: `https://dotnet.microsoft.com/download/dotnet/8.0` * Download the windows zip file from the [releases page](https://github.com/dafny-lang/dafny/releases/latest) and **save** it to your disk. * Then, **before you open or unzip it**, right-click on it and select Properties; at the bottom of the dialog, click the **Unblock** button and then the OK button. * Now, open the zip file and copy its contents into a directory on your machine. (You can now delete the zip file.) @@ -130,7 +130,7 @@ Then: ## Linux (Binary) {#linux-binary} To install a binary installation of dafny on Linux (e.g., Ubuntu), do the following: -* Install .NET 6.0. See: `https://docs.microsoft.com/dotnet/core/install/linux` or `sudo apt install dotnet-sdk-6.0` +* Install .NET 8.0. See: `https://docs.microsoft.com/dotnet/core/install/linux` or `sudo apt install dotnet-sdk-8.0` * Install the Linux binary version of Dafny, from `https://github.com/dafny-lang/dafny/releases/latest` * Unzip the downloaded file in a (empty) location of your choice @@ -165,7 +165,7 @@ After the compiler dependencies are installed, you can run a quick test of the i The .NET [NuGet](https://www.nuget.org/) repository collects .NET libraries and tools for easy installation. Dafny is available on NuGet, and can be installed as follows: -* Install .NET 6.0 as described for your platform in one of the subsections above. +* Install .NET 8.0 as described for your platform in one of the subsections above. * Install a binary version of Z3 4.12.1 for your platform from its [GitHub releases page](https://github.com/Z3Prover/z3/releases/tag/Z3-4.12.1) and put the `z3` executable in your `PATH`. * Install Dafny using `dotnet tool install --global dafny` (or leave out the `--global` to use with `dotnet tool run` from the source directory of a .NET project). @@ -181,10 +181,10 @@ Additional instructions are found in the [Dafny User Guide](DafnyRef/DafnyRef#se ### C# (.Net) -Install .NET 6.0: -* Windows) `https://dotnet.microsoft.com/download/dotnet/6.0` -* Linux) Install .NET 6.0. See: `https://docs.microsoft.com/dotnet/core/install/linux` or `sudo apt install dotnet-sdk-6.0` -* Mac) Install .NET 6.0: `brew install dotnet-sdk` or from `https://docs.microsoft.com/dotnet/core/install/macos` +Install .NET 8.0: +* Windows) `https://dotnet.microsoft.com/download/dotnet/8.0` +* Linux) Install .NET 8.0. See: `https://docs.microsoft.com/dotnet/core/install/linux` or `sudo apt install dotnet-sdk-8.0` +* Mac) Install .NET 8.0: `brew install dotnet-sdk` or from `https://docs.microsoft.com/dotnet/core/install/macos` To separately compile and run your program for .NET: diff --git a/docs/OnlineTutorial/guide.10.expect b/docs/OnlineTutorial/guide.10.expect index e714f865f0..6a7d67a897 100644 --- a/docs/OnlineTutorial/guide.10.expect +++ b/docs/OnlineTutorial/guide.10.expect @@ -1,14 +1,14 @@ text.dfy(7,0): Error: a postcondition could not be proved on this return path +text.dfy(4,12): Related location: this is the postcondition that could not be proved +text.dfy(7,0): Error: a postcondition could not be proved on this return path text.dfy(5,23): Related location: this is the postcondition that could not be proved text.dfy(7,0): Error: a postcondition could not be proved on this return path text.dfy(6,22): Related location: this is the postcondition that could not be proved -text.dfy(7,0): Error: a postcondition could not be proved on this return path -text.dfy(4,12): Related location: this is the postcondition that could not be proved +text.dfy(16,0): Error: a postcondition could not be proved on this return path +text.dfy(13,12): Related location: this is the postcondition that could not be proved text.dfy(16,0): Error: a postcondition could not be proved on this return path text.dfy(14,23): Related location: this is the postcondition that could not be proved text.dfy(16,0): Error: a postcondition could not be proved on this return path text.dfy(15,22): Related location: this is the postcondition that could not be proved -text.dfy(16,0): Error: a postcondition could not be proved on this return path -text.dfy(13,12): Related location: this is the postcondition that could not be proved Dafny program verifier finished with 0 verified, 6 errors From e1affea425782e9ec506a384bee2fae2a1a043c5 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 9 Jan 2025 20:24:57 +0100 Subject: [PATCH 43/45] Set a default verification time limit (#6028) Fixes https://github.com/dafny-lang/ide-vscode/issues/514 ### What was changed? Set a default verification time limit ### How has this been tested? Added a CLI test that checks there is a default time-out By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt). --- Source/DafnyCore/Options/BoogieOptionBag.cs | 4 +- Source/DafnyCore/Pipeline/Compilation.cs | 96 +++++++++++++++++-- .../LitTests/LitTest/cli/defaultTimeLimit.dfy | 17 ++++ .../LitTest/cli/defaultTimeLimit.dfy.expect | 7 ++ .../git-issues/git-issue-3855.dfy.expect | 2 +- docs/DafnyRef/UserGuide.md | 2 +- docs/news/{fix.6006 => 6006.fix} | 0 docs/news/6028.feat | 1 + 8 files changed, 117 insertions(+), 12 deletions(-) create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/defaultTimeLimit.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/defaultTimeLimit.dfy.expect rename docs/news/{fix.6006 => 6006.fix} (100%) create mode 100644 docs/news/6028.feat diff --git a/Source/DafnyCore/Options/BoogieOptionBag.cs b/Source/DafnyCore/Options/BoogieOptionBag.cs index 2983c3dbf3..59ffe8bfcb 100644 --- a/Source/DafnyCore/Options/BoogieOptionBag.cs +++ b/Source/DafnyCore/Options/BoogieOptionBag.cs @@ -51,8 +51,8 @@ public static class BoogieOptionBag { IsHidden = true }; - public static readonly Option VerificationTimeLimit = new("--verification-time-limit", - "Limit the number of seconds spent trying to verify each procedure") { + public static readonly Option VerificationTimeLimit = new("--verification-time-limit", () => 30, + "Limit the number of seconds spent trying to verify each assertion batch. A value of 0 indicates no limit") { ArgumentHelpName = "seconds", }; diff --git a/Source/DafnyCore/Pipeline/Compilation.cs b/Source/DafnyCore/Pipeline/Compilation.cs index d89a6b973f..0ecaadeae7 100644 --- a/Source/DafnyCore/Pipeline/Compilation.cs +++ b/Source/DafnyCore/Pipeline/Compilation.cs @@ -4,6 +4,7 @@ using System.Collections.Concurrent; using System.Collections.Generic; using System.CommandLine; +using System.CommandLine.Help; using System.IO; using System.Linq; using System.Reactive; @@ -560,17 +561,96 @@ public static void ReportDiagnosticsInResult(DafnyOptions options, string name, errorReporter.ReportBoogieError(errorInformation, dafnyCounterExampleModel); } - // This reports problems that are not captured by counter-examples, like a time-out - // The Boogie API forces us to create a temporary engine here to report the outcome, even though it only uses the options. - var boogieEngine = new ExecutionEngine(options, new EmptyVerificationResultCache(), - CustomStackSizePoolTaskScheduler.Create(0, 0)); - boogieEngine.ReportOutcome(null, outcome, outcomeError => errorReporter.ReportBoogieError(outcomeError, null, false), - name, token, null, TextWriter.Null, - timeLimit, result.CounterExamples); + var outcomeError = ReportOutcome(options, outcome, name, token, timeLimit, result.CounterExamples); + if (outcomeError != null) { + errorReporter.ReportBoogieError(outcomeError, null, false); + } + } + + private static ErrorInformation? ReportOutcome(DafnyOptions options, + VcOutcome vcOutcome, string name, + IToken token, uint timeLimit, List errors) { + ErrorInformation? errorInfo = null; + + switch (vcOutcome) { + case VcOutcome.Correct: + break; + case VcOutcome.Errors: + case VcOutcome.TimedOut: { + if (vcOutcome != VcOutcome.TimedOut && + (!errors.Any(e => e.IsAuxiliaryCexForDiagnosingTimeouts))) { + break; + } + + string msg = string.Format("Verification of '{1}' timed out after {0} seconds. (the limit can be increased using --verification-time-limit)", timeLimit, name); + errorInfo = ErrorInformation.Create(token, msg); + + // Report timed out assertions as auxiliary info. + var comparer = new CounterexampleComparer(); + var timedOutAssertions = errors.Where(e => e.IsAuxiliaryCexForDiagnosingTimeouts).Distinct(comparer) + .OrderBy(x => x, comparer).ToList(); + if (0 < timedOutAssertions.Count) { + errorInfo!.Msg += $" with {timedOutAssertions.Count} check(s) that timed out individually"; + } + + foreach (Counterexample error in timedOutAssertions) { + IToken tok; + string auxMsg = null!; + switch (error) { + case CallCounterexample callCounterexample: + tok = callCounterexample.FailingCall.tok; + auxMsg = callCounterexample.FailingCall.Description.FailureDescription; + break; + case ReturnCounterexample returnCounterexample: + tok = returnCounterexample.FailingReturn.tok; + auxMsg = returnCounterexample.FailingReturn.Description.FailureDescription; + break; + case AssertCounterexample assertError: { + tok = assertError.FailingAssert.tok; + if (!(assertError.FailingAssert.ErrorMessage == null || + ((ExecutionEngineOptions)options).ForceBplErrors)) { + auxMsg = assertError.FailingAssert.ErrorMessage; + } + + auxMsg ??= assertError.FailingAssert.Description.FailureDescription; + break; + } + default: throw new Exception(); + } + + errorInfo.AddAuxInfo(tok, auxMsg, "Unverified check due to timeout"); + } + + break; + } + case VcOutcome.OutOfResource: { + string msg = "Verification out of resource (" + name + ")"; + errorInfo = ErrorInformation.Create(token, msg); + } + break; + case VcOutcome.OutOfMemory: { + string msg = "Verification out of memory (" + name + ")"; + errorInfo = ErrorInformation.Create(token, msg); + } + break; + case VcOutcome.SolverException: { + string msg = "Verification encountered solver exception (" + name + ")"; + errorInfo = ErrorInformation.Create(token, msg); + } + break; + + case VcOutcome.Inconclusive: { + string msg = "Verification inconclusive (" + name + ")"; + errorInfo = ErrorInformation.Create(token, msg); + } + break; + } + + return errorInfo; } private static void AddAssertedExprToCounterExampleErrorInfo( - DafnyOptions options, Counterexample counterExample, ErrorInformation errorInformation) { + DafnyOptions options, Counterexample counterExample, ErrorInformation errorInformation) { Boogie.ProofObligationDescription? boogieProofObligationDesc = null; switch (errorInformation.Kind) { case ErrorKind.Assertion: diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/defaultTimeLimit.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/defaultTimeLimit.dfy new file mode 100644 index 0000000000..e91e3331f3 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/defaultTimeLimit.dfy @@ -0,0 +1,17 @@ +// RUN: ! %baredafny verify --use-basename-for-filename "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +method Foo() { + // Assert something that takes a long time to verify + assert Ack(4, 2) == 1; +} + +function Ack(m: nat, n: nat): nat +{ + if m == 0 then + n + 1 + else if n == 0 then + Ack(m - 1, 1) + else + Ack(m - 1, Ack(m, n - 1)) +} \ No newline at end of file diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/defaultTimeLimit.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/defaultTimeLimit.dfy.expect new file mode 100644 index 0000000000..b7677c3985 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/defaultTimeLimit.dfy.expect @@ -0,0 +1,7 @@ +defaultTimeLimit.dfy(4,7): Error: Verification of 'Foo' timed out after 30 seconds. (the limit can be increased using --verification-time-limit) + | +4 | method Foo() { + | ^^^ + + +Dafny program verifier finished with 1 verified, 0 errors, 1 time out diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3855.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3855.dfy.expect index e7965e5641..2c2bc4bc24 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3855.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3855.dfy.expect @@ -1,5 +1,5 @@ git-issue-3855.dfy(799,0): Warning: attribute :ignore is deprecated -git-issue-3855.dfy(799,11): Error: Verification of 'Memory.dynMove' timed out after seconds +git-issue-3855.dfy(799,11): Error: Verification of 'Memory.dynMove' timed out after seconds. (the limit can be increased using --verification-time-limit) git-issue-3855.dfy(942,17): Error: a precondition for this call could not be proved git-issue-3855.dfy(430,29): Related location: this is the precondition that could not be proved git-issue-3855.dfy(942,17): Error: a precondition for this call could not be proved diff --git a/docs/DafnyRef/UserGuide.md b/docs/DafnyRef/UserGuide.md index 578b63c692..8fd4ce1c5d 100644 --- a/docs/DafnyRef/UserGuide.md +++ b/docs/DafnyRef/UserGuide.md @@ -2769,7 +2769,7 @@ The following options are also commonly used: but a large positive number reports more errors per run * `--verification-time-limit:` (was `-timeLimit:`) - limits - the number of seconds spent trying to verify each procedure. + the number of seconds spent trying to verify each assertion batch. ### 13.9.11. Controlling test generation {#sec-controlling-test-gen} diff --git a/docs/news/fix.6006 b/docs/news/6006.fix similarity index 100% rename from docs/news/fix.6006 rename to docs/news/6006.fix diff --git a/docs/news/6028.feat b/docs/news/6028.feat new file mode 100644 index 0000000000..2bfb795746 --- /dev/null +++ b/docs/news/6028.feat @@ -0,0 +1 @@ +Change the default value for --verification-time-limit to 30 seconds instead of 0 (no limit) \ No newline at end of file From ca63bcfbfa654fda3f4b84a0f58e174b87c6bf19 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 10 Jan 2025 15:20:59 +0100 Subject: [PATCH 44/45] Attempt at fixing nightly. (#6035) ### What was changed? - Remove the `$(RUNTIME_IDENTIFIER)` property from csproj files that was needed as a workaround but may break things in .NET 8 according to SO - Remove references from DafnyDriver to DafnyServer, that prevented publishing correctly with .NET 8 - Stop publishing DafnyLanguageServer since it's not used directly. ### How has this been tested? Tested by existing tests By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt). --- .github/workflows/integration-tests-reusable.yml | 5 +++++ Scripts/package.py | 1 - Source/DafnyDriver/Commands/ServerCommand.cs | 2 -- Source/DafnyDriver/DafnyDriver.csproj | 12 +----------- .../Legacy/LegacyJsonVerificationLogger.cs | 1 - .../DafnyLanguageServer/DafnyLanguageServer.csproj | 1 - Source/DafnyServer/DafnyServer.csproj | 10 ---------- .../DafnyTestGeneration/DafnyTestGeneration.csproj | 1 - 8 files changed, 6 insertions(+), 27 deletions(-) diff --git a/.github/workflows/integration-tests-reusable.yml b/.github/workflows/integration-tests-reusable.yml index 3109c167cc..79d72f30dc 100644 --- a/.github/workflows/integration-tests-reusable.yml +++ b/.github/workflows/integration-tests-reusable.yml @@ -72,6 +72,11 @@ jobs: uses: actions/setup-dotnet@v4 with: dotnet-version: ${{ env.dotnet-version }} + # Setup dotnet 6.0 for running Boogie. Alternatively we could try running Boogie with a roll forward policy, or updating Boogie. + - name: Setup dotnet + uses: actions/setup-dotnet@v4 + with: + dotnet-version: 6.0.x - name: C++ for ubuntu 20.04 if: matrix.os == 'ubuntu-20.04' run: | diff --git a/Scripts/package.py b/Scripts/package.py index f543d37715..aaffbfe4e2 100755 --- a/Scripts/package.py +++ b/Scripts/package.py @@ -161,7 +161,6 @@ def build(self): if path.exists(self.buildDirectory): shutil.rmtree(self.buildDirectory) run(["make", "--quiet", "clean"]) - self.run_publish("DafnyLanguageServer") self.run_publish("DafnyServer") self.run_publish("DafnyRuntime", "netstandard2.0") self.run_publish("DafnyRuntime", "net452") diff --git a/Source/DafnyDriver/Commands/ServerCommand.cs b/Source/DafnyDriver/Commands/ServerCommand.cs index a4cdf8c92b..51381672ef 100644 --- a/Source/DafnyDriver/Commands/ServerCommand.cs +++ b/Source/DafnyDriver/Commands/ServerCommand.cs @@ -1,6 +1,4 @@ -using System.Collections.Generic; using System.CommandLine; -using DafnyCore; using Microsoft.Dafny.LanguageServer.Language; using Microsoft.Dafny.LanguageServer.Language.Symbols; using Microsoft.Dafny.LanguageServer.Workspace; diff --git a/Source/DafnyDriver/DafnyDriver.csproj b/Source/DafnyDriver/DafnyDriver.csproj index f928e3f504..0236f2ce5f 100644 --- a/Source/DafnyDriver/DafnyDriver.csproj +++ b/Source/DafnyDriver/DafnyDriver.csproj @@ -13,16 +13,6 @@ true - - - false - false - - - - - $(RUNTIME_IDENTIFIER) - @@ -42,8 +32,8 @@ + - diff --git a/Source/DafnyDriver/Legacy/LegacyJsonVerificationLogger.cs b/Source/DafnyDriver/Legacy/LegacyJsonVerificationLogger.cs index 93087fe8e5..e6e27c8b15 100644 --- a/Source/DafnyDriver/Legacy/LegacyJsonVerificationLogger.cs +++ b/Source/DafnyDriver/Legacy/LegacyJsonVerificationLogger.cs @@ -4,7 +4,6 @@ using System.Linq; using System.Text.Json.Nodes; using DafnyCore.Verifier; -using DafnyServer; using Microsoft.Boogie; using VC; diff --git a/Source/DafnyLanguageServer/DafnyLanguageServer.csproj b/Source/DafnyLanguageServer/DafnyLanguageServer.csproj index 67513425d4..92f1fad7df 100644 --- a/Source/DafnyLanguageServer/DafnyLanguageServer.csproj +++ b/Source/DafnyLanguageServer/DafnyLanguageServer.csproj @@ -6,7 +6,6 @@ enable Microsoft.Dafny.LanguageServer ..\..\Binaries\ - true false MIT README.md diff --git a/Source/DafnyServer/DafnyServer.csproj b/Source/DafnyServer/DafnyServer.csproj index d736ee1074..f9cd46eb53 100644 --- a/Source/DafnyServer/DafnyServer.csproj +++ b/Source/DafnyServer/DafnyServer.csproj @@ -10,16 +10,6 @@ MIT - - false - false - - - - - $(RUNTIME_IDENTIFIER) - - diff --git a/Source/DafnyTestGeneration/DafnyTestGeneration.csproj b/Source/DafnyTestGeneration/DafnyTestGeneration.csproj index 016cf01c49..f4f2f78ffd 100644 --- a/Source/DafnyTestGeneration/DafnyTestGeneration.csproj +++ b/Source/DafnyTestGeneration/DafnyTestGeneration.csproj @@ -15,7 +15,6 @@ - From 8946261959d65fd58690a232f516f8e76ebaf3ea Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 10 Jan 2025 21:14:55 +0100 Subject: [PATCH 45/45] Delete test for legacy CLI that tests broken behavior (#6037) ### What was changed? The Dafny legacy CLI shows part of a .NET error message as part of it UI. This can not be tested well since the specific error message is not defined as part of .NET, and can be different across .NET versions and platforms. On Windows it returns: `Invalid filename: The value cannot be an empty string. (Parameter 'path')` On other platforms it is: `Invalid filename: The path is empty. (Parameter 'path')` Instead of fixing the legacy CLI to remove the ambiguity, I'm removing the test for that ambiguous behavior since the old CLI is deprecated. ### How has this been tested? Removed a test By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt). --- .../TestFiles/LitTests/LitTest/git-issues/git-issue-3549a.dfy | 2 -- .../LitTests/LitTest/git-issues/git-issue-3549a.dfy.expect | 1 - 2 files changed, 3 deletions(-) delete mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3549a.dfy delete mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3549a.dfy.expect diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3549a.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3549a.dfy deleted file mode 100644 index 9ce07b0f26..0000000000 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3549a.dfy +++ /dev/null @@ -1,2 +0,0 @@ -// RUN: %exits-with 1 %baredafny "" 2> "%t" -// RUN: %diff "%s.expect" "%t" diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3549a.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3549a.dfy.expect deleted file mode 100644 index 3ccac32363..0000000000 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3549a.dfy.expect +++ /dev/null @@ -1 +0,0 @@ -Invalid filename: The value cannot be an empty string. (Parameter 'path')