From 8669bb6847d71583f4ba8c50074c3e06904d66bf Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Mon, 5 Aug 2024 23:39:38 -0500 Subject: [PATCH 1/9] Chore: Generated Id are now declaration-specific Previously, Id for the compilation of local variables were global, which caused issues to merge generated files. Fixes #5330 --- Source/DafnyCore/AST/CompilationData.cs | 2 +- .../AST/Expressions/Variables/Formal.cs | 12 ++++--- .../AST/Expressions/Variables/IVariable.cs | 11 ++----- .../Variables/IVariableContracts.cs | 18 +++++------ .../Variables/NonglobalVariable.cs | 14 ++++++--- Source/DafnyCore/AST/Members/ICodeContext.cs | 2 +- .../DafnyCore/AST/Modules/ModuleDefinition.cs | 3 +- .../Statements/Assignment/LocalVariable.cs | 13 +++++--- .../AST/TypeDeclarations/Declaration.cs | 7 ++++- .../AST/TypeDeclarations/IteratorDecl.cs | 5 +-- .../AST/TypeDeclarations/NewtypeDecl.cs | 2 +- .../TypeDeclarations/TypeSynonymDeclBase.cs | 2 +- .../Backends/CSharp/CsharpCodeGenerator.cs | 6 ++-- .../Backends/CSharp/CsharpSynthesizer.cs | 12 +++---- .../Backends/Cplusplus/CppCodeGenerator.cs | 16 +++++----- .../Backends/Dafny/DafnyCodeGenerator.cs | 12 +++---- .../Backends/GoLang/GoCodeGenerator.cs | 6 ++-- .../Backends/Java/JavaCodeGenerator.cs | 2 +- .../JavaScript/JavaScriptCodeGenerator.cs | 2 +- .../Backends/Python/PythonCodeGenerator.cs | 12 +++---- .../SinglePassCodeGenerator.Statement.cs | 2 +- .../SinglePassCodeGenerator.cs | 19 +++++++++--- .../Resolver/InferDecreasesClause.cs | 2 +- .../Rewriters/RunAllTestsMainMethod.cs | 2 +- Source/DafnyCore/Verifier/BoogieGenerator.cs | 6 ++-- Source/DafnyCore/Verifier/FreshIdGenerator.cs | 31 ++++++++++++++----- 26 files changed, 128 insertions(+), 93 deletions(-) diff --git a/Source/DafnyCore/AST/CompilationData.cs b/Source/DafnyCore/AST/CompilationData.cs index ce827a7c0d9..0193ad362ff 100644 --- a/Source/DafnyCore/AST/CompilationData.cs +++ b/Source/DafnyCore/AST/CompilationData.cs @@ -5,7 +5,7 @@ namespace Microsoft.Dafny; public class CompilationData { - public readonly FreshIdGenerator IdGenerator = new(); + public readonly FreshIdGenerator IdGenerator = new CompilationIdGenerator(); public CompilationData(ErrorReporter errorReporter, List includes, IList rootSourceUris, ISet alreadyVerifiedRoots, ISet alreadyCompiledRoots) { Includes = includes; diff --git a/Source/DafnyCore/AST/Expressions/Variables/Formal.cs b/Source/DafnyCore/AST/Expressions/Variables/Formal.cs index cdbff00e752..90697bebbc1 100644 --- a/Source/DafnyCore/AST/Expressions/Variables/Formal.cs +++ b/Source/DafnyCore/AST/Expressions/Variables/Formal.cs @@ -36,10 +36,14 @@ public Formal(IToken tok, string name, Type type, bool inParam, bool isGhost, Ex public bool HasName => !Name.StartsWith("#"); private string sanitizedName; - public override string SanitizedName => - sanitizedName ??= SanitizeName(Name); // No unique-ification - public override string CompileName => - compileName ??= SanitizeName(NameForCompilation); + + public override string SanitizedName(CompilationIdGenerator generator) { + return sanitizedName ??= SanitizeName(Name); // No unique-ification + } + + public override string CompileName(CompilationIdGenerator generator) { + return compileName ??= SanitizeName(NameForCompilation); + } public override IEnumerable Children => (DefaultValue != null ? new List { DefaultValue } : Enumerable.Empty()).Concat(base.Children); diff --git a/Source/DafnyCore/AST/Expressions/Variables/IVariable.cs b/Source/DafnyCore/AST/Expressions/Variables/IVariable.cs index b262ff36001..bd468f06677 100644 --- a/Source/DafnyCore/AST/Expressions/Variables/IVariable.cs +++ b/Source/DafnyCore/AST/Expressions/Variables/IVariable.cs @@ -19,18 +19,13 @@ string UniqueName { bool HasBeenAssignedUniqueName { // unique names are not assigned until the Translator; if you don't already know if that stage has run, this boolean method will tell you get; } - static FreshIdGenerator CompileNameIdGenerator = new FreshIdGenerator(); - string AssignUniqueName(FreshIdGenerator generator); - string SanitizedName { - get; - } + string AssignUniqueName(VerificationIdGenerator generator); + string SanitizedName(CompilationIdGenerator generator); string SanitizedNameShadowable { // A name suitable for compilation, but without the unique identifier. // Useful to generate readable identifiers in the generated source code. get; } - string CompileName { - get; - } + string CompileName(CompilationIdGenerator generator); PreType PreType { get; diff --git a/Source/DafnyCore/AST/Expressions/Variables/IVariableContracts.cs b/Source/DafnyCore/AST/Expressions/Variables/IVariableContracts.cs index 7a473d9ba98..c239f703d20 100644 --- a/Source/DafnyCore/AST/Expressions/Variables/IVariableContracts.cs +++ b/Source/DafnyCore/AST/Expressions/Variables/IVariableContracts.cs @@ -35,11 +35,9 @@ public bool HasBeenAssignedUniqueName { throw new NotImplementedException(); // this getter implementation is here only so that the Ensures contract can be given here } } - public string SanitizedName { - get { - Contract.Ensures(Contract.Result() != null); - throw new NotImplementedException(); // this getter implementation is here only so that the Ensures contract can be given here - } + public string SanitizedName(CompilationIdGenerator generator) { + Contract.Ensures(Contract.Result() != null); + throw new NotImplementedException(); // this getter implementation is here only so that the Ensures contract can be given here } public string SanitizedNameShadowable { @@ -48,11 +46,9 @@ public string SanitizedNameShadowable { throw new NotImplementedException(); // this getter implementation is here only so that the Ensures contract can be given here } } - public string CompileName { - get { - Contract.Ensures(Contract.Result() != null); - throw new NotImplementedException(); // this getter implementation is here only so that the Ensures contract can be given here - } + public string CompileName(CompilationIdGenerator generator) { + Contract.Ensures(Contract.Result() != null); + throw new NotImplementedException(); // this getter implementation is here only so that the Ensures contract can be given here } public Type Type { get { @@ -88,7 +84,7 @@ public bool IsGhost { public void MakeGhost() { throw new NotImplementedException(); } - public string AssignUniqueName(FreshIdGenerator generator) { + public string AssignUniqueName(VerificationIdGenerator generator) { Contract.Ensures(Contract.Result() != null); throw new NotImplementedException(); } diff --git a/Source/DafnyCore/AST/Expressions/Variables/NonglobalVariable.cs b/Source/DafnyCore/AST/Expressions/Variables/NonglobalVariable.cs index 88aa24aa10f..e7ac2755f92 100644 --- a/Source/DafnyCore/AST/Expressions/Variables/NonglobalVariable.cs +++ b/Source/DafnyCore/AST/Expressions/Variables/NonglobalVariable.cs @@ -38,7 +38,7 @@ public string Name { private string uniqueName; public string UniqueName => uniqueName; public bool HasBeenAssignedUniqueName => uniqueName != null; - public string AssignUniqueName(FreshIdGenerator generator) { + public string AssignUniqueName(VerificationIdGenerator generator) { return uniqueName ??= generator.FreshId(Name + "#"); } @@ -91,12 +91,16 @@ public static string SanitizeName(string nm) { sanitizedNameShadowable ??= SanitizeName(Name); private string sanitizedName; - public virtual string SanitizedName => - sanitizedName ??= $"_{IVariable.CompileNameIdGenerator.FreshNumericId()}_{SanitizedNameShadowable}"; + + public virtual string SanitizedName(CompilationIdGenerator generator) { + return sanitizedName ??= $"_{generator.FreshNumericId()}_{SanitizedNameShadowable}"; + } protected string compileName; - public virtual string CompileName => - compileName ??= SanitizedName; + + public virtual string CompileName(CompilationIdGenerator generator) { + return compileName ??= SanitizedName(generator); + } Type type; public bool IsTypeExplicit { get; set; } diff --git a/Source/DafnyCore/AST/Members/ICodeContext.cs b/Source/DafnyCore/AST/Members/ICodeContext.cs index 9dda622ab1e..580d84b2aa4 100644 --- a/Source/DafnyCore/AST/Members/ICodeContext.cs +++ b/Source/DafnyCore/AST/Members/ICodeContext.cs @@ -144,7 +144,7 @@ public interface RedirectingTypeDecl : ICallable { Expression/*?*/ Constraint { get; } SubsetTypeDecl.WKind WitnessKind { get; } Expression/*?*/ Witness { get; } // non-null iff WitnessKind is Compiled or Ghost - FreshIdGenerator IdGenerator { get; } + VerificationIdGenerator IdGenerator { get; } [FilledInDuringResolution] bool ConstraintIsCompilable { get; set; } } \ No newline at end of file diff --git a/Source/DafnyCore/AST/Modules/ModuleDefinition.cs b/Source/DafnyCore/AST/Modules/ModuleDefinition.cs index c7da3bee900..68c53b79c99 100644 --- a/Source/DafnyCore/AST/Modules/ModuleDefinition.cs +++ b/Source/DafnyCore/AST/Modules/ModuleDefinition.cs @@ -4,6 +4,7 @@ using System.Diagnostics.Contracts; using System.Linq; using Microsoft.Dafny.Auditor; +using Microsoft.Dafny.Compilers; using OmniSharp.Extensions.LanguageServer.Protocol.Models; namespace Microsoft.Dafny; @@ -871,7 +872,7 @@ public ModuleSignature RegisterTopLevelDecls(ModuleResolver resolver, bool useIm dtor.AddAnotherEnclosingCtor(ctor, formal); } else { // either the destructor has no explicit name, or this constructor declared another destructor with this name, or no previous destructor had this name - dtor = new DatatypeDestructor(formal.RangeToken, ctor, formal, new Name(formal.RangeToken, formal.Name), "dtor_" + formal.CompileName, + dtor = new DatatypeDestructor(formal.RangeToken, ctor, formal, new Name(formal.RangeToken, formal.Name), "dtor_" + formal.CompileName(SinglePassCodeGenerator.FormalIdGenerator), formal.IsGhost, formal.Type, null); dtor.InheritVisibility(dt); dtor.EnclosingClass = dt; // resolve here diff --git a/Source/DafnyCore/AST/Statements/Assignment/LocalVariable.cs b/Source/DafnyCore/AST/Statements/Assignment/LocalVariable.cs index e90f93964c2..63a03a1c218 100644 --- a/Source/DafnyCore/AST/Statements/Assignment/LocalVariable.cs +++ b/Source/DafnyCore/AST/Statements/Assignment/LocalVariable.cs @@ -65,7 +65,7 @@ public string DisplayName { private string uniqueName; public string UniqueName => uniqueName; public bool HasBeenAssignedUniqueName => uniqueName != null; - public string AssignUniqueName(FreshIdGenerator generator) { + public string AssignUniqueName(VerificationIdGenerator generator) { return uniqueName ??= generator.FreshId(Name + "#"); } @@ -76,12 +76,15 @@ public string AssignUniqueName(FreshIdGenerator generator) { private string sanitizedName; - public string SanitizedName => - sanitizedName ??= $"_{IVariable.CompileNameIdGenerator.FreshNumericId()}_{SanitizedNameShadowable}"; + public string SanitizedName(CompilationIdGenerator generator) { + return sanitizedName ??= $"_{generator}_{SanitizedNameShadowable}"; + } string compileName; - public string CompileName => - compileName ??= SanitizedName; + + public string CompileName(CompilationIdGenerator generator) { + return compileName ??= SanitizedName(generator); + } // TODO rename and update comment? Or make it nullable? public readonly Type SyntacticType; // this is the type mentioned in the declaration, if any diff --git a/Source/DafnyCore/AST/TypeDeclarations/Declaration.cs b/Source/DafnyCore/AST/TypeDeclarations/Declaration.cs index daa1077654e..0e33514f7b7 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/Declaration.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/Declaration.cs @@ -132,9 +132,14 @@ public override string ToString() { return Name; } - internal FreshIdGenerator IdGenerator = new(); + // For Boogie + internal VerificationIdGenerator IdGenerator = new(); public override IEnumerable Children => (Attributes != null ? new List { Attributes } : Enumerable.Empty()); public override IEnumerable PreResolveChildren => Children; public abstract SymbolKind? Kind { get; } public abstract string GetDescription(DafnyOptions options); + + + // For Compilation + internal CompilationIdGenerator CompilationIdGenerator = new(); } \ No newline at end of file diff --git a/Source/DafnyCore/AST/TypeDeclarations/IteratorDecl.cs b/Source/DafnyCore/AST/TypeDeclarations/IteratorDecl.cs index 36a2666c330..2dd460a6f7f 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/IteratorDecl.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/IteratorDecl.cs @@ -1,5 +1,6 @@ using System.Collections.Generic; using System.Diagnostics.Contracts; +using Microsoft.Dafny.Compilers; namespace Microsoft.Dafny; @@ -345,7 +346,7 @@ public void Resolve(ModuleResolver resolver) { resolver.reporter.Error(MessageSource.Resolver, p, "Name of in-parameter is used by another member of the iterator: {0}", p.Name); } else { - var field = new SpecialField(p.RangeToken, p.Name, SpecialField.ID.UseIdParam, p.CompileName, p.IsGhost, false, + var field = new SpecialField(p.RangeToken, p.Name, SpecialField.ID.UseIdParam, p.CompileName(SinglePassCodeGenerator.FormalIdGenerator), p.IsGhost, false, false, p.Type, null); field.EnclosingClass = this; // resolve here field.InheritVisibility(this); @@ -361,7 +362,7 @@ public void Resolve(ModuleResolver resolver) { "Name of yield-parameter is used by another member of the iterator: {0}", p.Name); } else { nonDuplicateOuts.Add(p); - var field = new SpecialField(p.RangeToken, p.Name, SpecialField.ID.UseIdParam, p.CompileName, p.IsGhost, true, + var field = new SpecialField(p.RangeToken, p.Name, SpecialField.ID.UseIdParam, p.CompileName(SinglePassCodeGenerator.FormalIdGenerator), p.IsGhost, true, true, p.Type, null); field.EnclosingClass = this; // resolve here field.InheritVisibility(this); diff --git a/Source/DafnyCore/AST/TypeDeclarations/NewtypeDecl.cs b/Source/DafnyCore/AST/TypeDeclarations/NewtypeDecl.cs index efd594d52f4..58c50791a74 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/NewtypeDecl.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/NewtypeDecl.cs @@ -116,7 +116,7 @@ public TypeParameter.EqualitySupportValue EqualitySupport { Expression RedirectingTypeDecl.Constraint { get { return Constraint; } } SubsetTypeDecl.WKind RedirectingTypeDecl.WitnessKind { get { return WitnessKind; } } Expression RedirectingTypeDecl.Witness { get { return Witness; } } - FreshIdGenerator RedirectingTypeDecl.IdGenerator { get { return IdGenerator; } } + VerificationIdGenerator RedirectingTypeDecl.IdGenerator { get { return IdGenerator; } } bool ICodeContext.IsGhost { get { throw new NotSupportedException(); } // if .IsGhost is needed, the object should always be wrapped in an CodeContextWrapper diff --git a/Source/DafnyCore/AST/TypeDeclarations/TypeSynonymDeclBase.cs b/Source/DafnyCore/AST/TypeDeclarations/TypeSynonymDeclBase.cs index a6daacab0d6..198b4f41851 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/TypeSynonymDeclBase.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/TypeSynonymDeclBase.cs @@ -73,7 +73,7 @@ bool RedirectingTypeDecl.ConstraintIsCompilable { SubsetTypeDecl.WKind RedirectingTypeDecl.WitnessKind { get { return SubsetTypeDecl.WKind.CompiledZero; } } Expression RedirectingTypeDecl.Witness { get { return null; } } - FreshIdGenerator RedirectingTypeDecl.IdGenerator { get { return IdGenerator; } } + VerificationIdGenerator RedirectingTypeDecl.IdGenerator { get { return IdGenerator; } } bool ICodeContext.IsGhost { get { throw new NotSupportedException(); } // if .IsGhost is needed, the object should always be wrapped in an CodeContextWrapper diff --git a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs index 076c247c6de..6ec5686ec7f 100644 --- a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs +++ b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs @@ -867,7 +867,7 @@ private void CompileDatatypeDestructorsAndAddToInterface(DatatypeDecl dt, Concre if (compiledConstructorCount != 0) { var arg = dtor.CorrespondingFormals[0]; if (!arg.IsGhost) { - var DtorM = arg.HasName ? InternalFieldPrefix + arg.CompileName : FieldName(arg, index); + var DtorM = arg.HasName ? InternalFieldPrefix + arg.CompileName(FormalIdGenerator) : FieldName(arg, index); // TN dtor_QDtorM { get; } interfaceTree.WriteLine($"{TypeName(arg.Type, wr, arg.tok)} {DestructorGetterName(arg, ctor, index)} {{ get; }}"); @@ -1178,7 +1178,7 @@ private string FieldName(Formal formal, int i) { Contract.Requires(formal != null); Contract.Ensures(Contract.Result() != null); - return IdProtect(InternalFieldPrefix + (formal.HasName ? formal.CompileName : "a" + i)); + return IdProtect(InternalFieldPrefix + (formal.HasName ? formal.CompileName(FormalIdGenerator) : "a" + i)); } /// @@ -2977,7 +2977,7 @@ protected override void EmitDestructor(Action source, Formal } private string DestructorGetterName(Formal dtor, DatatypeCtor ctor, int index) { - return $"dtor_{(dtor.HasName ? dtor.CompileName : ctor.GetCompileName(Options) + FieldName(dtor, index))}"; + return $"dtor_{(dtor.HasName ? dtor.CompileName(FormalIdGenerator) : ctor.GetCompileName(Options) + FieldName(dtor, index))}"; } protected override ConcreteSyntaxTree CreateLambda(List inTypes, IToken tok, List inNames, diff --git a/Source/DafnyCore/Backends/CSharp/CsharpSynthesizer.cs b/Source/DafnyCore/Backends/CSharp/CsharpSynthesizer.cs index 56a6f7b6f58..631e7d67e14 100644 --- a/Source/DafnyCore/Backends/CSharp/CsharpSynthesizer.cs +++ b/Source/DafnyCore/Backends/CSharp/CsharpSynthesizer.cs @@ -89,7 +89,7 @@ public ConcreteSyntaxTree SynthesizeMethod(Method method, // The solution is to rename the out parameters. var parameterString = parameters.ToString(); var objectToReturnName = method.Outs.ToDictionary(o => o, - o => codeGenerator.idGenerator.FreshId(o.CompileName + "Return")); + o => codeGenerator.idGenerator.FreshId(o.CompileName(SinglePassCodeGenerator.FormalIdGenerator) + "Return")); foreach (var (obj, returnName) in objectToReturnName) { parameterString = Regex.Replace(parameterString, $"(^|[^a-zA-Z0-9_]){obj.CompileName}([^a-zA-Z0-9_]|$)", @@ -99,7 +99,7 @@ public ConcreteSyntaxTree SynthesizeMethod(Method method, // Initialize the mocks objectToMockName = method.Outs.ToDictionary(o => (IVariable)o, - o => codeGenerator.idGenerator.FreshId(o.CompileName + "Mock")); + o => codeGenerator.idGenerator.FreshId(o.CompileName(SinglePassCodeGenerator.FormalIdGenerator) + "Mock")); foreach (var (obj, mockName) in objectToMockName) { var typeName = codeGenerator.TypeName(obj.Type, wr, obj.Tok); // Mocking a trait works only so long as no trait member is accessed @@ -110,7 +110,7 @@ public ConcreteSyntaxTree SynthesizeMethod(Method method, wr.FormatLine($"var {mockName} = new Mock<{typeName}>();"); wr.FormatLine($"{mockName}.CallBase = true;"); } - wr.FormatLine($"var {obj.CompileName} = {mockName}.Object;"); + wr.FormatLine($"var {obj.CompileName(method.CompilationIdGenerator)} = {mockName}.Object;"); } // Stub methods and fields according to the Dafny post-conditions: @@ -122,10 +122,10 @@ public ConcreteSyntaxTree SynthesizeMethod(Method method, // Return the mocked objects: if (returnType != "void") { - wr.FormatLine($"return {method.Outs[0].CompileName};"); + wr.FormatLine($"return {method.Outs[0].CompileName(SinglePassCodeGenerator.FormalIdGenerator)};"); } else { foreach (var o in method.Outs) { - wr.FormatLine($"{objectToReturnName[o]} = {o.CompileName};"); + wr.FormatLine($"{objectToReturnName[o]} = {o.CompileName(SinglePassCodeGenerator.FormalIdGenerator)};"); } } wr.WriteLine("}"); @@ -244,7 +244,7 @@ private void SynthesizeExpression(ConcreteSyntaxTree wr, BinaryExpr binaryExpr, var typeName = codeGenerator.TypeName(arg.Type, wr, arg.tok); var bound = GetBound(arg); if (bound != null) { - wr.Format($"{typeName} {bound.Item1.CompileName}"); + wr.Format($"{typeName} {bound.Item1.CompileName(codeGenerator.currentIdGenerator)}"); } else { // if the argument is not a bound variable, it is irrelevant to the // expression in the lambda diff --git a/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs b/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs index be83d5f912b..001993b6394 100644 --- a/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs +++ b/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs @@ -368,7 +368,7 @@ protected override IClassWriter DeclareDatatype(DatatypeDecl dt, ConcreteSyntaxT var wc = wdef.NewNamedBlock("{1}\n{0}{2}::{0}()", DtT_protected, DeclareTemplate(dt.TypeArgs), InstantiateTemplate(dt.TypeArgs)); foreach (var arg in ctor.Formals) { if (!arg.IsGhost) { - wc.WriteLine("{0} = {1};", arg.CompileName, DefaultValue(arg.Type, wc, arg.tok)); + wc.WriteLine("{0} = {1};", arg.CompileName(SinglePassCodeGenerator.FormalIdGenerator), DefaultValue(arg.Type, wc, arg.tok)); } } @@ -393,7 +393,7 @@ protected override IClassWriter DeclareDatatype(DatatypeDecl dt, ConcreteSyntaxT owr.WriteLine("size_t seed = 0;"); foreach (var arg in ctor.Formals) { if (!arg.IsGhost) { - owr.WriteLine("hash_combine<{0}>(seed, x.{1});", TypeName(arg.Type, owr, dt.tok), arg.CompileName); + owr.WriteLine("hash_combine<{0}>(seed, x.{1});", TypeName(arg.Type, owr, dt.tok), arg.CompileName(SinglePassCodeGenerator.FormalIdGenerator)); } } owr.WriteLine("return seed;"); @@ -453,9 +453,9 @@ protected override IClassWriter DeclareDatatype(DatatypeDecl dt, ConcreteSyntaxT if (!arg.IsGhost) { if (arg.Type is UserDefinedType udt && udt.ResolvedClass == dt) { // Recursive destructor needs to use a pointer - owr.WriteLine("hash_combine>(seed, x.{1});", TypeName(arg.Type, owr, dt.tok), arg.CompileName); + owr.WriteLine("hash_combine>(seed, x.{1});", TypeName(arg.Type, owr, dt.tok), arg.CompileName(SinglePassCodeGenerator.FormalIdGenerator)); } else { - owr.WriteLine("hash_combine<{0}>(seed, x.{1});", TypeName(arg.Type, owr, dt.tok), arg.CompileName); + owr.WriteLine("hash_combine<{0}>(seed, x.{1});", TypeName(arg.Type, owr, dt.tok), arg.CompileName(SinglePassCodeGenerator.FormalIdGenerator)); } argCount++; } @@ -482,10 +482,10 @@ protected override IClassWriter DeclareDatatype(DatatypeDecl dt, ConcreteSyntaxT if (!arg.IsGhost) { if (arg.Type is UserDefinedType udt && udt.ResolvedClass == dt) { // This is a recursive destuctor, so we need to allocate space and copy the input in - wc.WriteLine("COMPILER_result_subStruct.{0} = std::make_shared<{1}>({0});", arg.CompileName, + wc.WriteLine("COMPILER_result_subStruct.{0} = std::make_shared<{1}>({0});", arg.CompileName(SinglePassCodeGenerator.FormalIdGenerator), DtT_protected); } else { - wc.WriteLine("COMPILER_result_subStruct.{0} = {0};", arg.CompileName); + wc.WriteLine("COMPILER_result_subStruct.{0} = {0};", arg.CompileName(SinglePassCodeGenerator.FormalIdGenerator)); } } } @@ -501,7 +501,7 @@ protected override IClassWriter DeclareDatatype(DatatypeDecl dt, ConcreteSyntaxT wd.WriteLine("{0} COMPILER_result_subStruct;", DatatypeSubStructName(default_ctor, true)); foreach (Formal arg in default_ctor.Formals) { if (!arg.IsGhost) { - wd.WriteLine("COMPILER_result_subStruct.{0} = {1};", arg.CompileName, + wd.WriteLine("COMPILER_result_subStruct.{0} = {1};", arg.CompileName(SinglePassCodeGenerator.FormalIdGenerator), DefaultValue(arg.Type, wd, arg.tok)); } } @@ -550,7 +550,7 @@ protected override IClassWriter DeclareDatatype(DatatypeDecl dt, ConcreteSyntaxT } var wDtor = ws.NewNamedBlock("{0} dtor_{1}()", returnType, - arg.CompileName); + arg.CompileName(SinglePassCodeGenerator.FormalIdGenerator)); if (dt.IsRecordType) { wDtor.WriteLine("return this.{0};", IdName(arg)); } else { diff --git a/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs b/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs index 572bd8ad845..9216177a637 100644 --- a/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs +++ b/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs @@ -51,7 +51,7 @@ public DafnyCodeGenerator(DafnyOptions options, ErrorReporter reporter, string i } protected override string GetCompileNameNotProtected(IVariable v) { - return preventShadowing ? v.CompileName : v.SanitizedNameShadowable; + return preventShadowing ? v.CompileName(currentIdGenerator) : v.SanitizedNameShadowable; } public void AddUnsupported(string why) { @@ -437,7 +437,7 @@ protected override void GetNativeInfo(NativeType.Selection sel, out string name, foreach (var param in formals) { if (param is not ImplicitFormal && !param.IsGhost) { paramsList.Add((DAST.Formal)DAST.Formal.create_Formal( - Sequence.UnicodeFromString(IdProtect(param.CompileName)), GenType(param.Type), ParseAttributes(param.Attributes))); + Sequence.UnicodeFromString(IdProtect(param.CompileName(FormalIdGenerator))), GenType(param.Type), ParseAttributes(param.Attributes))); } } @@ -495,7 +495,7 @@ public ConcreteSyntaxTree CreateMethod(Method m, List List outTypes = new(); foreach (var outVar in m.Outs) { if (!outVar.IsGhost) { - outVars.Add(Sequence.UnicodeFromString(compiler.IdProtect(outVar.CompileName))); + outVars.Add(Sequence.UnicodeFromString(compiler.IdProtect(outVar.CompileName(m.CompilationIdGenerator)))); outTypes.Add(compiler.GenType(outVar.Type)); } } @@ -814,7 +814,7 @@ protected override void EmitNameAndActualTypeArgs(string protectedName, List)Option.create_Some(GenType(replacementReceiver.Type)) : (Option)Option.create_None(); if (receiverBeforeName) { - var name = replacementReceiver is IdentifierExpr { Var: { CompileName: var compileName } } + var name = replacementReceiver is IdentifierExpr { Var: var variable } && variable.CompileName(enclosingDeclaration.CompilationIdGenerator) is var compileName ? compileName : "receiver"; receiverArg = (Option<_IFormal>)Option.create_Some( @@ -1771,7 +1771,7 @@ protected override void EmitDatatypeValue(DatatypeValue dtv, string typeDescript } private static string GetDestructorFormalName(Formal formal) { - var defaultName = formal.CompileName; + var defaultName = formal.CompileName(FormalIdGenerator); object externVal = null; bool hasExternVal = Attributes.ContainsMatchingValue(formal.Attributes, "extern", ref externVal, new List { @@ -2180,7 +2180,7 @@ protected override void EmitDestructor(Action source, Formal int.Parse(dtor.NameForCompilation), GenType(dtor.Type) )); } else { - var compileName = GetExtractOverrideName(dtor.Attributes, dtor.CompileName); + var compileName = GetExtractOverrideName(dtor.Attributes, dtor.CompileName(currentIdGenerator)); builder.Builder.AddExpr((DAST.Expression)DAST.Expression.create_Select( sourceAST, Sequence.UnicodeFromString(compileName), diff --git a/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs b/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs index 856bd85ce5d..3c912a105d8 100644 --- a/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs +++ b/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs @@ -912,7 +912,7 @@ string StructOfCtor(DatatypeCtor ctor) { var arg = dtor.CorrespondingFormals[0]; if (!arg.IsGhost && arg.HasName) { wr.WriteLine(); - var wDtor = wr.NewNamedBlock("func (_this {0}) {1}() {2}", name, FormatDatatypeDestructorName(arg.CompileName), TypeName(arg.Type, wr, arg.tok)); + var wDtor = wr.NewNamedBlock("func (_this {0}) {1}() {2}", name, FormatDatatypeDestructorName(arg.CompileName(FormalIdGenerator)), TypeName(arg.Type, wr, arg.tok)); var n = dtor.EnclosingCtors.Count; if (n == 1) { wDtor.WriteLine("return _this.Get_().({0}).{1}", StructOfCtor(dtor.EnclosingCtors[0]), DatatypeFieldName(arg)); @@ -1845,12 +1845,12 @@ protected string UnqualifiedClassName(Type type, ConcreteSyntaxTree wr, IToken t protected string DatatypeFieldName(Formal formal, int formalNonGhostIndex) { // Don't rely on base.FormalName because it needlessly (for us) passes the // value through IdProtect when we're going to capitalize it - return formal.HasName ? Capitalize(formal.CompileName) : "A" + formalNonGhostIndex + "_"; + return formal.HasName ? Capitalize(formal.CompileName(FormalIdGenerator)) : "A" + formalNonGhostIndex + "_"; } protected string DatatypeFieldName(Formal formal) { Contract.Assert(formal.HasName); - return Capitalize(formal.CompileName); + return Capitalize(formal.CompileName(FormalIdGenerator)); } // ----- Declarations ------------------------------------------------------------- diff --git a/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs b/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs index d4ab8a5d3a0..c447c4b3a51 100644 --- a/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs +++ b/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs @@ -2326,7 +2326,7 @@ private string FieldName(Formal formal, int i) { Contract.Requires(formal != null); Contract.Ensures(Contract.Result() != null); - return IdProtect(InternalFieldPrefix + (formal.HasName ? formal.CompileName : "a" + i)); + return IdProtect(InternalFieldPrefix + (formal.HasName ? formal.CompileName(FormalIdGenerator) : "a" + i)); } protected override void EmitPrintStmt(ConcreteSyntaxTree wr, Expression arg) { diff --git a/Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs b/Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs index e2e71971cf2..66df643a0e3 100644 --- a/Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs +++ b/Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs @@ -435,7 +435,7 @@ protected override ConcreteSyntaxTree CreateIterator(IteratorDecl iter, Concrete if (!arg.IsGhost && arg.HasName) { // datatype: get dtor_Dtor0() { return this.Dtor0; } // codatatype: get dtor_Dtor0() { return this._D().Dtor0; } - wr.WriteLine("get dtor_{0}() {{ return this{2}.{1}; }}", arg.CompileName, IdName(arg), dt is CoDatatypeDecl ? "._D()" : ""); + wr.WriteLine("get dtor_{0}() {{ return this{2}.{1}; }}", arg.CompileName(FormalIdGenerator), IdName(arg), dt is CoDatatypeDecl ? "._D()" : ""); } } } diff --git a/Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs b/Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs index 81e3a5b7212..dff1600d05d 100644 --- a/Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs +++ b/Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs @@ -374,7 +374,7 @@ from dtor in ctor.Destructors where dtor.EnclosingCtors[0] == ctor select dtor.CorrespondingFormals[0] into arg where !arg.IsGhost - select IdProtect(arg.CompileName)) { + select IdProtect(arg.CompileName(dt.CompilationIdGenerator))) { w.WriteLine("@property"); w.NewBlockPy($"def {destructor}(self):") .WriteLine($"return self._get().{destructor}"); @@ -417,9 +417,9 @@ private void DatatypeFieldsAndConstructor(DatatypeCtor ctor, ConcreteSyntaxTree .Where(f => !f.IsGhost) .Select(f => { if (f.Type.IsStringType && UnicodeCharEnabled) { - return $"{{self.{IdProtect(f.CompileName)}.VerbatimString(True)}}"; + return $"{{self.{IdProtect(f.CompileName(FormalIdGenerator))}.VerbatimString(True)}}"; } else { - return $"{{{DafnyRuntimeModule}.string_of(self.{IdProtect(f.CompileName)})}}"; + return $"{{{DafnyRuntimeModule}.string_of(self.{IdProtect(f.CompileName(FormalIdGenerator))})}}"; } }) .Comma(); @@ -433,7 +433,7 @@ private void DatatypeFieldsAndConstructor(DatatypeCtor ctor, ConcreteSyntaxTree var argList = ctor.Formals .Where(f => !f.IsGhost) - .Select(f => $"self.{IdProtect(f.CompileName)} == __o.{IdProtect(f.CompileName)}"); + .Select(f => $"self.{IdProtect(f.CompileName(FormalIdGenerator))} == __o.{IdProtect(f.CompileName(FormalIdGenerator))}"); var suffix = args.Length > 0 ? $" and {string.Join(" and ", argList)}" : ""; wr.NewBlockPy("def __eq__(self, __o: object) -> bool:") @@ -1511,7 +1511,7 @@ protected override void EmitSeqConstructionExpr(SeqConstructionExpr expr, bool i wr.Write(DafnySeqMakerFunction); if (expr.Initializer is LambdaExpr lam) { valueExpression = Expr(lam.Body, inLetExprBody, wStmts); - var binder = IdProtect(lam.BoundVars[0].CompileName); + var binder = IdProtect(lam.BoundVars[0].CompileName(currentIdGenerator)); wr.Write($"([{valueExpression} for {binder} in {range}])"); } else { valueExpression = Expr(expr.Initializer, inLetExprBody, wStmts); @@ -1549,7 +1549,7 @@ protected override void EmitDestructor(Action source, Formal Contract.Assert(coreDtor.CorrespondingFormals.Count == 1); Contract.Assert(dtor == coreDtor.CorrespondingFormals[0]); // any other destructor is a ghost } else { - wr.Write(ctor.EnclosingDatatype is TupleTypeDecl ? $"[{dtor.NameForCompilation}]" : $".{IdProtect(dtor.CompileName)}"); + wr.Write(ctor.EnclosingDatatype is TupleTypeDecl ? $"[{dtor.NameForCompilation}]" : $".{IdProtect(dtor.CompileName(currentIdGenerator))}"); } } diff --git a/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Statement.cs b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Statement.cs index 2c6214ead56..9ddaafd692b 100644 --- a/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Statement.cs +++ b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Statement.cs @@ -733,7 +733,7 @@ private ConcreteSyntaxTree EmitNestedMatchStmtCaseConstructor(string sourceName, valueWriter.Append(destructor); } } else { - newSourceName = ProtectedFreshId(arg.CompileName); + newSourceName = ProtectedFreshId(arg.CompileName(currentIdGenerator)); var valueWriter = DeclareLocalVar(newSourceName, type, idPattern.Tok, result); valueWriter.Append(destructor); result = EmitNestedMatchCaseConditions(newSourceName, type, childPattern, result, lastCase); diff --git a/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs index 798ccae90ca..b4d9327898d 100644 --- a/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs +++ b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs @@ -67,11 +67,14 @@ public abstract partial class SinglePassCodeGenerator { protected ModuleDefinition enclosingModule; // non-null when a module body is being translated protected Method enclosingMethod; // non-null when a method body is being translated protected Function enclosingFunction; // non-null when a function body is being translated + protected Declaration enclosingDeclaration; // non-null when a declaration body is being translated - protected internal readonly FreshIdGenerator idGenerator = new FreshIdGenerator(); + protected internal readonly CompilationIdGenerator idGenerator = new CompilationIdGenerator(); - private protected string ProtectedFreshId(string prefix) => IdProtect(idGenerator.FreshId(prefix)); - private protected string ProtectedFreshNumericId(string prefix) => IdProtect(idGenerator.FreshNumericId(prefix)); + protected internal CompilationIdGenerator currentIdGenerator => enclosingDeclaration?.CompilationIdGenerator ?? idGenerator; + + private protected string ProtectedFreshId(string prefix) => IdProtect(currentIdGenerator.FreshId(prefix)); + private protected string ProtectedFreshNumericId(string prefix) => IdProtect(currentIdGenerator.FreshNumericId(prefix)); Dictionary uniqueAstNumbers = new Dictionary(); int GetUniqueAstNumber(Expression expr) { @@ -985,7 +988,7 @@ protected virtual string IdName(TypeParameter tp) { return IdProtect(tp.GetCompileName(Options)); } protected virtual string GetCompileNameNotProtected(IVariable v) { - return v.CompileName; + return v.CompileName(currentIdGenerator); } protected virtual string IdName(IVariable v) { Contract.Requires(v != null); @@ -1844,12 +1847,16 @@ protected int WriteFormals(string sep, List formals, ConcreteSyntaxTree } return n; // the number of formals written } + + // Placeholder because formals don't need an Id generator + + public static CompilationIdGenerator FormalIdGenerator = new UncallableIdGenerator(); protected string FormalName(Formal formal, int i) { Contract.Requires(formal != null); Contract.Ensures(Contract.Result() != null); - return IdProtect(formal.HasName ? formal.CompileName : "_a" + i); + return IdProtect(formal.HasName ? formal.CompileName(FormalIdGenerator) : "_a" + i); } public static bool HasMain(Program program, out Method mainMethod) { @@ -2129,6 +2136,7 @@ void CompileClassMembers(Program program, TopLevelDeclWithMembers c, IClassWrite if (c is not TraitDecl || TraitRepeatsInheritedDeclarations) { thisContext = c; foreach (var member in inheritedMembers.Select(memberx => (memberx as Function)?.ByMethodDecl ?? memberx)) { + enclosingDeclaration = member; Contract.Assert(!member.IsStatic); // only instance members should ever be added to .InheritedMembers if (member.IsGhost) { // skip @@ -2198,6 +2206,7 @@ void CompileClassMembers(Program program, TopLevelDeclWithMembers c, IClassWrite } foreach (MemberDecl memberx in c.Members) { + enclosingDeclaration = memberx; var member = (memberx as Function)?.ByMethodDecl ?? memberx; if (!member.IsStatic) { thisContext = c; diff --git a/Source/DafnyCore/Resolver/InferDecreasesClause.cs b/Source/DafnyCore/Resolver/InferDecreasesClause.cs index c2f9060aa71..0e3996c8520 100644 --- a/Source/DafnyCore/Resolver/InferDecreasesClause.cs +++ b/Source/DafnyCore/Resolver/InferDecreasesClause.cs @@ -147,7 +147,7 @@ public Expression FrameToObjectSet(List fexprs) { List sets = new List(); List singletons = null; - var idGen = new FreshIdGenerator(); + var idGen = new VerificationIdGenerator(); // drop wildcards altogether in the following iterations foreach (FrameExpression fe in fexprs.Where(fe => fe.E is not WildcardExpr)) { Contract.Assert(fe != null); diff --git a/Source/DafnyCore/Rewriters/RunAllTestsMainMethod.cs b/Source/DafnyCore/Rewriters/RunAllTestsMainMethod.cs index 24415062a93..4d6185bf404 100644 --- a/Source/DafnyCore/Rewriters/RunAllTestsMainMethod.cs +++ b/Source/DafnyCore/Rewriters/RunAllTestsMainMethod.cs @@ -95,7 +95,7 @@ internal override void PreResolve(Program program) { internal override void PostResolve(Program program) { var tok = program.GetStartOfFirstFileToken() ?? Token.NoToken; List mainMethodStatements = new(); - var idGenerator = new FreshIdGenerator(); + var idGenerator = new CompilationIdGenerator(); // var success := true; var successVarStmt = Statement.CreateLocalVariable(tok, "success", Expression.CreateBoolLiteral(tok, true)); diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.cs b/Source/DafnyCore/Verifier/BoogieGenerator.cs index 924d78212c4..e30bd6c6a5e 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.cs @@ -1753,9 +1753,9 @@ public enum StmtType { NONE, ASSERT, ASSUME }; public StmtType stmtContext = StmtType.NONE; // the Statement that is currently being translated public bool adjustFuelForExists = true; // fuel need to be adjusted for exists based on whether exists is in assert or assume stmt. - public readonly FreshIdGenerator defaultIdGenerator = new FreshIdGenerator(); + public readonly VerificationIdGenerator defaultIdGenerator = new VerificationIdGenerator(); - public FreshIdGenerator CurrentIdGenerator { + public VerificationIdGenerator CurrentIdGenerator { get { var decl = codeContext as Declaration; if (decl != null) { @@ -3654,7 +3654,7 @@ Bpl.Expr SetupVariableAsLocal(IVariable v, Dictionary sub Contract.Requires(builder != null); Contract.Requires(decreases != null); List oldBfs = new List(); - var idGen = new FreshIdGenerator(); + var idGen = new VerificationIdGenerator(); foreach (Expression e in decreases) { Contract.Assert(e != null); Bpl.LocalVariable bfVar = new Bpl.LocalVariable(e.tok, new Bpl.TypedIdent(e.tok, idGen.FreshId(varPrefix), TrType(cce.NonNull(e.Type)))); diff --git a/Source/DafnyCore/Verifier/FreshIdGenerator.cs b/Source/DafnyCore/Verifier/FreshIdGenerator.cs index 4196ea040c1..02d80e53f17 100644 --- a/Source/DafnyCore/Verifier/FreshIdGenerator.cs +++ b/Source/DafnyCore/Verifier/FreshIdGenerator.cs @@ -1,9 +1,10 @@ +using System; using System.Collections.Generic; using System.Diagnostics.Contracts; using System.Linq; namespace Microsoft.Dafny { - public class FreshIdGenerator { + public abstract class FreshIdGenerator { string tipString; // a string representation of Tip int tipChildrenCount = 0; readonly Stack> prefixToCountStack = new(); // invariant PrefixToCount_Stack.Count == Tip.Count @@ -35,7 +36,7 @@ public FreshIdGenerator() { prefixToCountStack.Push(new()); } - private FreshIdGenerator(string commonPrefix) : this() { + protected FreshIdGenerator(string commonPrefix) : this() { this.commonPrefix = commonPrefix; } @@ -50,11 +51,7 @@ public string FreshId(string prefix) { return commonPrefix + prefix + FreshNumericId(prefix); } - public FreshIdGenerator NestedFreshIdGenerator(string prefix) { - return new(FreshId(prefix)); - } - - public string FreshNumericId(string prefix = "") { + public virtual string FreshNumericId(string prefix = "") { var prefixToCount = prefixToCountStack.Peek(); lock (prefixToCount) { if (!prefixToCount.TryGetValue(prefix, out var old)) { @@ -65,4 +62,24 @@ public string FreshNumericId(string prefix = "") { } } } + + public class CompilationIdGenerator : FreshIdGenerator { + } + + public class VerificationIdGenerator : FreshIdGenerator { + public VerificationIdGenerator() { + } + public VerificationIdGenerator(string commonPrefix) : base(commonPrefix) { + } + public VerificationIdGenerator NestedFreshIdGenerator(string prefix) { + return new(FreshId(prefix)); + } + } + + // For formals + public class UncallableIdGenerator : CompilationIdGenerator { + public override string FreshNumericId(string prefix = "") { + throw new InvalidOperationException("Not supposed to call this method with this kind of Id generator"); + } + } } \ No newline at end of file From d9f1066bbac779479f519346957cbc94b4e80573 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Tue, 6 Aug 2024 10:56:43 -0500 Subject: [PATCH 2/9] Updated generated files --- ...afnyToRustCompilerCoverage_RASTCoverage.cs | 212 +- .../Statements/Assignment/LocalVariable.cs | 2 +- .../Backends/CSharp/CsharpCodeGenerator.cs | 12 +- .../Backends/CSharp/CsharpSynthesizer.cs | 4 +- .../Backends/Cplusplus/CppCodeGenerator.cs | 4 +- .../Backends/GoLang/GoCodeGenerator.cs | 20 +- .../Backends/Java/JavaCodeGenerator.cs | 26 +- .../JavaScript/JavaScriptCodeGenerator.cs | 18 +- .../DafnyCore/DafnyGeneratedFromDafnyPost.py | 2 +- Source/DafnyCore/GeneratedFromDafny/DAST.cs | 98 +- .../GeneratedFromDafny/DAST_Format.cs | 10 +- Source/DafnyCore/GeneratedFromDafny/DCOMP.cs | 8964 ++++++++--------- .../GeneratedFromDafny/Formatting.cs | 28 +- Source/DafnyCore/GeneratedFromDafny/RAST.cs | 1680 +-- .../ResolvedDesugaredExecutableDafnyPlugin.cs | 6 +- .../Std_Arithmetic_DivInternals.cs | 24 +- .../Std_Arithmetic_Logarithm.cs | 14 +- .../Std_Arithmetic_ModInternals.cs | 16 +- .../Std_Arithmetic_MulInternals.cs | 14 +- .../Std_Arithmetic_Power.cs | 14 +- .../GeneratedFromDafny/Std_Collections_Seq.cs | 302 +- .../Std_Strings_CharStrEscaping.cs | 52 +- .../Std_Strings_DecimalConversion.cs | 96 +- .../Std_Strings_HexConversion.cs | 96 +- .../GeneratedFromDafny/Std_Wrappers.cs | 82 +- .../DafnyCore/Triggers/TriggerExtensions.cs | 1 - Source/DafnyCore/Verifier/FreshIdGenerator.cs | 4 + 27 files changed, 5902 insertions(+), 5899 deletions(-) diff --git a/Source/DafnyCore.Test/GeneratedFromDafny/DafnyToRustCompilerCoverage_RASTCoverage.cs b/Source/DafnyCore.Test/GeneratedFromDafny/DafnyToRustCompilerCoverage_RASTCoverage.cs index db6a2b35422..5ff65b29a76 100644 --- a/Source/DafnyCore.Test/GeneratedFromDafny/DafnyToRustCompilerCoverage_RASTCoverage.cs +++ b/Source/DafnyCore.Test/GeneratedFromDafny/DafnyToRustCompilerCoverage_RASTCoverage.cs @@ -24,120 +24,120 @@ public static RAST._IExpr DafnyIntLiteral(Dafny.ISequence s) { } public static void TestOptimizeToString() { - RAST._IExpr _1095_x; - _1095_x = RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x")); - RAST._IExpr _1096_y; - _1096_y = RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("y")); - DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_UnaryOp(Dafny.Sequence.UnicodeFromString("&"), RAST.Expr.create_Call(RAST.Expr.create_Select(_1095_x, Dafny.Sequence.UnicodeFromString("clone")), Dafny.Sequence.FromElements()), DAST.Format.UnaryOpFormat.create_NoFormat())).Optimize(), RAST.Expr.create_UnaryOp(Dafny.Sequence.UnicodeFromString("&"), _1095_x, DAST.Format.UnaryOpFormat.create_NoFormat()))); - DafnyToRustCompilerCoverage.RASTCoverage.__default.TestNoOptimize(RAST.Expr.create_UnaryOp(Dafny.Sequence.UnicodeFromString("&"), RAST.Expr.create_Call(RAST.Expr.create_Select(_1095_x, Dafny.Sequence.UnicodeFromString("clone")), Dafny.Sequence.FromElements(_1096_y)), DAST.Format.UnaryOpFormat.create_NoFormat())); - DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_UnaryOp(Dafny.Sequence.UnicodeFromString("!"), RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("=="), _1095_x, _1096_y, DAST.Format.BinaryOpFormat.create_NoFormat()), DAST.Format.UnaryOpFormat.create_CombineFormat())).Optimize(), RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("!="), _1095_x, _1096_y, DAST.Format.BinaryOpFormat.create_NoFormat()))); - DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_UnaryOp(Dafny.Sequence.UnicodeFromString("!"), RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("<"), _1095_x, _1096_y, DAST.Format.BinaryOpFormat.create_NoFormat()), DAST.Format.UnaryOpFormat.create_CombineFormat())).Optimize(), RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString(">="), _1095_x, _1096_y, DAST.Format.BinaryOpFormat.create_NoFormat()))); - DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_UnaryOp(Dafny.Sequence.UnicodeFromString("!"), RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("<"), _1095_x, _1096_y, DAST.Format.BinaryOpFormat.create_ReverseFormat()), DAST.Format.UnaryOpFormat.create_CombineFormat())).Optimize(), RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("<="), _1096_y, _1095_x, DAST.Format.BinaryOpFormat.create_NoFormat()))); + RAST._IExpr _0_x; + _0_x = RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x")); + RAST._IExpr _1_y; + _1_y = RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("y")); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_UnaryOp(Dafny.Sequence.UnicodeFromString("&"), RAST.Expr.create_Call(RAST.Expr.create_Select(_0_x, Dafny.Sequence.UnicodeFromString("clone")), Dafny.Sequence.FromElements()), DAST.Format.UnaryOpFormat.create_NoFormat())).Optimize(), RAST.Expr.create_UnaryOp(Dafny.Sequence.UnicodeFromString("&"), _0_x, DAST.Format.UnaryOpFormat.create_NoFormat()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.TestNoOptimize(RAST.Expr.create_UnaryOp(Dafny.Sequence.UnicodeFromString("&"), RAST.Expr.create_Call(RAST.Expr.create_Select(_0_x, Dafny.Sequence.UnicodeFromString("clone")), Dafny.Sequence.FromElements(_1_y)), DAST.Format.UnaryOpFormat.create_NoFormat())); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_UnaryOp(Dafny.Sequence.UnicodeFromString("!"), RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("=="), _0_x, _1_y, DAST.Format.BinaryOpFormat.create_NoFormat()), DAST.Format.UnaryOpFormat.create_CombineFormat())).Optimize(), RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("!="), _0_x, _1_y, DAST.Format.BinaryOpFormat.create_NoFormat()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_UnaryOp(Dafny.Sequence.UnicodeFromString("!"), RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("<"), _0_x, _1_y, DAST.Format.BinaryOpFormat.create_NoFormat()), DAST.Format.UnaryOpFormat.create_CombineFormat())).Optimize(), RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString(">="), _0_x, _1_y, DAST.Format.BinaryOpFormat.create_NoFormat()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_UnaryOp(Dafny.Sequence.UnicodeFromString("!"), RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("<"), _0_x, _1_y, DAST.Format.BinaryOpFormat.create_ReverseFormat()), DAST.Format.UnaryOpFormat.create_CombineFormat())).Optimize(), RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("<="), _1_y, _0_x, DAST.Format.BinaryOpFormat.create_NoFormat()))); DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((DafnyToRustCompilerCoverage.RASTCoverage.__default.ConversionNum(RAST.Type.create_I128(), DafnyToRustCompilerCoverage.RASTCoverage.__default.DafnyIntLiteral(Dafny.Sequence.UnicodeFromString("1")))).Optimize(), RAST.Expr.create_LiteralInt(Dafny.Sequence.UnicodeFromString("1")))); - DafnyToRustCompilerCoverage.RASTCoverage.__default.TestNoOptimize(DafnyToRustCompilerCoverage.RASTCoverage.__default.ConversionNum(RAST.Type.create_I128(), _1095_x)); - DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_StmtExpr(RAST.Expr.create_DeclareVar(RAST.DeclareType.create_MUT(), Dafny.Sequence.UnicodeFromString("z"), Std.Wrappers.Option.create_Some(RAST.Type.create_I128()), Std.Wrappers.Option.create_None()), RAST.Expr.create_StmtExpr(RAST.__default.AssignVar(Dafny.Sequence.UnicodeFromString("z"), _1096_y), RAST.Expr.create_RawExpr(Dafny.Sequence.UnicodeFromString("return"))))).Optimize(), RAST.Expr.create_StmtExpr(RAST.Expr.create_DeclareVar(RAST.DeclareType.create_MUT(), Dafny.Sequence.UnicodeFromString("z"), Std.Wrappers.Option.create_Some(RAST.Type.create_I128()), Std.Wrappers.Option.create_Some(_1096_y)), RAST.Expr.create_RawExpr(Dafny.Sequence.UnicodeFromString("return"))))); - DafnyToRustCompilerCoverage.RASTCoverage.__default.TestNoOptimize(RAST.Expr.create_StmtExpr(RAST.Expr.create_DeclareVar(RAST.DeclareType.create_MUT(), Dafny.Sequence.UnicodeFromString("z"), Std.Wrappers.Option.create_Some(RAST.Type.create_I128()), Std.Wrappers.Option.create_None()), RAST.Expr.create_StmtExpr(RAST.__default.AssignVar(Dafny.Sequence.UnicodeFromString("w"), _1096_y), RAST.Expr.create_RawExpr(Dafny.Sequence.UnicodeFromString("return"))))); - DafnyToRustCompilerCoverage.RASTCoverage.__default.TestNoOptimize(_1095_x); - DafnyToRustCompilerCoverage.RASTCoverage.__default.TestNoOptimize(RAST.Expr.create_StmtExpr(_1095_x, _1095_x)); - DafnyToRustCompilerCoverage.RASTCoverage.__default.TestNoOptimize(RAST.Expr.create_StmtExpr(RAST.Expr.create_Match(_1095_x, Dafny.Sequence.FromElements()), _1095_x)); - DafnyToRustCompilerCoverage.RASTCoverage.__default.TestNoOptimize(RAST.Expr.create_StmtExpr(RAST.Expr.create_StructBuild(_1095_x, Dafny.Sequence.FromElements()), _1095_x)); - DafnyToRustCompilerCoverage.RASTCoverage.__default.TestNoOptimize(RAST.Expr.create_StmtExpr(RAST.Expr.create_Tuple(Dafny.Sequence.FromElements()), _1095_x)); - DafnyToRustCompilerCoverage.RASTCoverage.__default.TestNoOptimize(RAST.Expr.create_StmtExpr(RAST.Expr.create_UnaryOp(Dafny.Sequence.UnicodeFromString("&"), _1095_x, DAST.Format.UnaryOpFormat.create_NoFormat()), _1095_x)); - DafnyToRustCompilerCoverage.RASTCoverage.__default.TestNoOptimize(RAST.Expr.create_StmtExpr(RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("&&"), _1095_x, _1095_x, DAST.Format.BinaryOpFormat.create_NoFormat()), _1095_x)); - DafnyToRustCompilerCoverage.RASTCoverage.__default.TestNoOptimize(RAST.Expr.create_StmtExpr(RAST.Expr.create_TypeAscription(_1095_x, RAST.Type.create_I128()), _1095_x)); - DafnyToRustCompilerCoverage.RASTCoverage.__default.TestNoOptimize(RAST.Expr.create_StmtExpr(RAST.Expr.create_LiteralInt(Dafny.Sequence.UnicodeFromString("1")), _1095_x)); - DafnyToRustCompilerCoverage.RASTCoverage.__default.TestNoOptimize(RAST.Expr.create_StmtExpr(RAST.Expr.create_LiteralString(Dafny.Sequence.UnicodeFromString("2"), true, false), _1095_x)); - DafnyToRustCompilerCoverage.RASTCoverage.__default.TestNoOptimize(RAST.Expr.create_StmtExpr(RAST.Expr.create_LiteralString(Dafny.Sequence.UnicodeFromString("3"), false, true), _1095_x)); - DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_StmtExpr(RAST.Expr.create_DeclareVar(RAST.DeclareType.create_MUT(), Dafny.Sequence.UnicodeFromString("z"), Std.Wrappers.Option.create_Some(RAST.Type.create_I128()), Std.Wrappers.Option.create_None()), RAST.Expr.create_StmtExpr(RAST.__default.AssignVar(Dafny.Sequence.UnicodeFromString("z"), _1096_y), RAST.Expr.create_RawExpr(Dafny.Sequence.UnicodeFromString("return"))))).Optimize(), RAST.Expr.create_StmtExpr(RAST.Expr.create_DeclareVar(RAST.DeclareType.create_MUT(), Dafny.Sequence.UnicodeFromString("z"), Std.Wrappers.Option.create_Some(RAST.Type.create_I128()), Std.Wrappers.Option.create_Some(_1096_y)), RAST.Expr.create_RawExpr(Dafny.Sequence.UnicodeFromString("return"))))); - Dafny.ISequence _1097_coverageExpression; - _1097_coverageExpression = Dafny.Sequence.FromElements(RAST.Expr.create_RawExpr(Dafny.Sequence.UnicodeFromString("abc")), RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x")), RAST.Expr.create_Match(RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x")), Dafny.Sequence.FromElements(RAST.MatchCase.create(Dafny.Sequence.UnicodeFromString("abc"), RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x"))))), RAST.Expr.create_StmtExpr(RAST.Expr.create_RawExpr(Dafny.Sequence.UnicodeFromString("panic!()")), RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("a"))), RAST.Expr.create_Block(RAST.Expr.create_RawExpr(Dafny.Sequence.UnicodeFromString("abc"))), RAST.Expr.create_StructBuild(RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("dummy")), Dafny.Sequence.FromElements(RAST.AssignIdentifier.create(Dafny.Sequence.UnicodeFromString("foo"), RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("bar"))))), RAST.Expr.create_StructBuild(RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("dummy")), Dafny.Sequence.FromElements(RAST.AssignIdentifier.create(Dafny.Sequence.UnicodeFromString("foo"), RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("bar"))), RAST.AssignIdentifier.create(Dafny.Sequence.UnicodeFromString("foo2"), RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("bar"))))), RAST.Expr.create_Tuple(Dafny.Sequence.FromElements(RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x")))), RAST.Expr.create_UnaryOp(Dafny.Sequence.UnicodeFromString("-"), RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x")), DAST.Format.UnaryOpFormat.create_NoFormat()), RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("+"), RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x")), RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("y")), DAST.Format.BinaryOpFormat.create_NoFormat()), RAST.Expr.create_TypeAscription(RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x")), RAST.Type.create_I128()), RAST.Expr.create_LiteralInt(Dafny.Sequence.UnicodeFromString("322")), RAST.Expr.create_LiteralString(Dafny.Sequence.UnicodeFromString("abc"), true, false), RAST.Expr.create_LiteralString(Dafny.Sequence.UnicodeFromString("abc"), false, true), RAST.Expr.create_DeclareVar(RAST.DeclareType.create_MUT(), Dafny.Sequence.UnicodeFromString("abc"), Std.Wrappers.Option.create_Some(RAST.Type.create_I128()), Std.Wrappers.Option.create_None()), RAST.Expr.create_DeclareVar(RAST.DeclareType.create_CONST(), Dafny.Sequence.UnicodeFromString("abc"), Std.Wrappers.Option.create_None(), Std.Wrappers.Option.create_Some(RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x")))), RAST.__default.AssignVar(Dafny.Sequence.UnicodeFromString("abc"), RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x"))), RAST.Expr.create_IfExpr(RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x")), RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x")), RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x"))), RAST.Expr.create_Loop(Std.Wrappers.Option.create_Some(RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x"))), RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x"))), RAST.Expr.create_For(Dafny.Sequence.UnicodeFromString("abc"), RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x")), RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x"))), RAST.Expr.create_Labelled(Dafny.Sequence.UnicodeFromString("abc"), RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x"))), RAST.Expr.create_Break(Std.Wrappers.Option>.create_None()), RAST.Expr.create_Break(Std.Wrappers.Option>.create_Some(Dafny.Sequence.UnicodeFromString("l"))), RAST.Expr.create_Continue(Std.Wrappers.Option>.create_None()), RAST.Expr.create_Continue(Std.Wrappers.Option>.create_Some(Dafny.Sequence.UnicodeFromString("l"))), RAST.Expr.create_Return(Std.Wrappers.Option.create_None()), RAST.Expr.create_Return(Std.Wrappers.Option.create_Some(RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x")))), RAST.Expr.create_Call(RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x")), Dafny.Sequence.FromElements()), RAST.Expr.create_Call(RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x")), Dafny.Sequence.FromElements(RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x")), RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("y")))), RAST.Expr.create_CallType(RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x")), Dafny.Sequence.FromElements(RAST.Type.create_I128(), RAST.Type.create_U32())), RAST.Expr.create_Select(RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x")), Dafny.Sequence.UnicodeFromString("abc")), RAST.Expr.create_MemberSelect(RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x")), Dafny.Sequence.UnicodeFromString("abc"))); - BigInteger _hi4 = new BigInteger((_1097_coverageExpression).Count); - for (BigInteger _1098_i = BigInteger.Zero; _1098_i < _hi4; _1098_i++) { - RAST._IExpr _1099_c; - _1099_c = (_1097_coverageExpression).Select(_1098_i); - RAST._IPrintingInfo _1100___v0; - _1100___v0 = (_1099_c).printingInfo; - RAST._IExpr _1101___v1; - _1101___v1 = (_1099_c).Optimize(); - Dafny.IMap> _1102___v2; - _1102___v2 = Dafny.Map>.FromElements(new Dafny.Pair>(_1099_c, (_1099_c)._ToString(Dafny.Sequence.UnicodeFromString("")))); - RAST._IExpr _1103___v3; - _1103___v3 = (RAST.Expr.create_StmtExpr(RAST.Expr.create_DeclareVar(RAST.DeclareType.create_MUT(), Dafny.Sequence.UnicodeFromString("abc"), Std.Wrappers.Option.create_Some(RAST.Type.create_I128()), Std.Wrappers.Option.create_None()), _1099_c)).Optimize(); - RAST._IExpr _1104___v4; - _1104___v4 = (RAST.Expr.create_StmtExpr(RAST.Expr.create_DeclareVar(RAST.DeclareType.create_MUT(), Dafny.Sequence.UnicodeFromString("abc"), Std.Wrappers.Option.create_Some(RAST.Type.create_I128()), Std.Wrappers.Option.create_None()), RAST.Expr.create_StmtExpr(RAST.__default.AssignVar(Dafny.Sequence.UnicodeFromString("abc"), _1099_c), RAST.Expr.create_RawExpr(Dafny.Sequence.UnicodeFromString(""))))).Optimize(); - RAST._IExpr _1105___v5; - _1105___v5 = (RAST.Expr.create_UnaryOp(Dafny.Sequence.UnicodeFromString("&"), _1099_c, DAST.Format.UnaryOpFormat.create_NoFormat())).Optimize(); - RAST._IExpr _1106___v6; - _1106___v6 = (RAST.Expr.create_UnaryOp(Dafny.Sequence.UnicodeFromString("!"), _1099_c, DAST.Format.UnaryOpFormat.create_NoFormat())).Optimize(); - RAST._IExpr _1107___v7; - _1107___v7 = (DafnyToRustCompilerCoverage.RASTCoverage.__default.ConversionNum(RAST.Type.create_U8(), _1099_c)).Optimize(); - RAST._IExpr _1108___v8; - _1108___v8 = (DafnyToRustCompilerCoverage.RASTCoverage.__default.ConversionNum(RAST.Type.create_U8(), RAST.Expr.create_Call(_1099_c, Dafny.Sequence.FromElements()))).Optimize(); - RAST._IExpr _1109___v9; - _1109___v9 = (DafnyToRustCompilerCoverage.RASTCoverage.__default.ConversionNum(RAST.Type.create_U8(), RAST.Expr.create_Call(RAST.Expr.create_MemberSelect(_1099_c, Dafny.Sequence.UnicodeFromString("int!")), Dafny.Sequence.FromElements()))).Optimize(); - RAST._IExpr _1110___v10; - _1110___v10 = (DafnyToRustCompilerCoverage.RASTCoverage.__default.ConversionNum(RAST.Type.create_U8(), RAST.Expr.create_Call(RAST.Expr.create_MemberSelect(RAST.Expr.create_MemberSelect(_1099_c, Dafny.Sequence.UnicodeFromString("dafny_runtime")), Dafny.Sequence.UnicodeFromString("int!")), Dafny.Sequence.FromElements()))).Optimize(); - RAST._IExpr _1111___v11; - _1111___v11 = (DafnyToRustCompilerCoverage.RASTCoverage.__default.ConversionNum(RAST.Type.create_U8(), RAST.Expr.create_Call(RAST.Expr.create_MemberSelect(RAST.Expr.create_MemberSelect(RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("")), Dafny.Sequence.UnicodeFromString("dafny_runtime")), Dafny.Sequence.UnicodeFromString("int!")), Dafny.Sequence.FromElements(_1099_c)))).Optimize(); - Std.Wrappers._IOption> _1112___v12; - _1112___v12 = (_1099_c).RightMostIdentifier(); + DafnyToRustCompilerCoverage.RASTCoverage.__default.TestNoOptimize(DafnyToRustCompilerCoverage.RASTCoverage.__default.ConversionNum(RAST.Type.create_I128(), _0_x)); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_StmtExpr(RAST.Expr.create_DeclareVar(RAST.DeclareType.create_MUT(), Dafny.Sequence.UnicodeFromString("z"), Std.Wrappers.Option.create_Some(RAST.Type.create_I128()), Std.Wrappers.Option.create_None()), RAST.Expr.create_StmtExpr(RAST.__default.AssignVar(Dafny.Sequence.UnicodeFromString("z"), _1_y), RAST.Expr.create_RawExpr(Dafny.Sequence.UnicodeFromString("return"))))).Optimize(), RAST.Expr.create_StmtExpr(RAST.Expr.create_DeclareVar(RAST.DeclareType.create_MUT(), Dafny.Sequence.UnicodeFromString("z"), Std.Wrappers.Option.create_Some(RAST.Type.create_I128()), Std.Wrappers.Option.create_Some(_1_y)), RAST.Expr.create_RawExpr(Dafny.Sequence.UnicodeFromString("return"))))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.TestNoOptimize(RAST.Expr.create_StmtExpr(RAST.Expr.create_DeclareVar(RAST.DeclareType.create_MUT(), Dafny.Sequence.UnicodeFromString("z"), Std.Wrappers.Option.create_Some(RAST.Type.create_I128()), Std.Wrappers.Option.create_None()), RAST.Expr.create_StmtExpr(RAST.__default.AssignVar(Dafny.Sequence.UnicodeFromString("w"), _1_y), RAST.Expr.create_RawExpr(Dafny.Sequence.UnicodeFromString("return"))))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.TestNoOptimize(_0_x); + DafnyToRustCompilerCoverage.RASTCoverage.__default.TestNoOptimize(RAST.Expr.create_StmtExpr(_0_x, _0_x)); + DafnyToRustCompilerCoverage.RASTCoverage.__default.TestNoOptimize(RAST.Expr.create_StmtExpr(RAST.Expr.create_Match(_0_x, Dafny.Sequence.FromElements()), _0_x)); + DafnyToRustCompilerCoverage.RASTCoverage.__default.TestNoOptimize(RAST.Expr.create_StmtExpr(RAST.Expr.create_StructBuild(_0_x, Dafny.Sequence.FromElements()), _0_x)); + DafnyToRustCompilerCoverage.RASTCoverage.__default.TestNoOptimize(RAST.Expr.create_StmtExpr(RAST.Expr.create_Tuple(Dafny.Sequence.FromElements()), _0_x)); + DafnyToRustCompilerCoverage.RASTCoverage.__default.TestNoOptimize(RAST.Expr.create_StmtExpr(RAST.Expr.create_UnaryOp(Dafny.Sequence.UnicodeFromString("&"), _0_x, DAST.Format.UnaryOpFormat.create_NoFormat()), _0_x)); + DafnyToRustCompilerCoverage.RASTCoverage.__default.TestNoOptimize(RAST.Expr.create_StmtExpr(RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("&&"), _0_x, _0_x, DAST.Format.BinaryOpFormat.create_NoFormat()), _0_x)); + DafnyToRustCompilerCoverage.RASTCoverage.__default.TestNoOptimize(RAST.Expr.create_StmtExpr(RAST.Expr.create_TypeAscription(_0_x, RAST.Type.create_I128()), _0_x)); + DafnyToRustCompilerCoverage.RASTCoverage.__default.TestNoOptimize(RAST.Expr.create_StmtExpr(RAST.Expr.create_LiteralInt(Dafny.Sequence.UnicodeFromString("1")), _0_x)); + DafnyToRustCompilerCoverage.RASTCoverage.__default.TestNoOptimize(RAST.Expr.create_StmtExpr(RAST.Expr.create_LiteralString(Dafny.Sequence.UnicodeFromString("2"), true, false), _0_x)); + DafnyToRustCompilerCoverage.RASTCoverage.__default.TestNoOptimize(RAST.Expr.create_StmtExpr(RAST.Expr.create_LiteralString(Dafny.Sequence.UnicodeFromString("3"), false, true), _0_x)); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_StmtExpr(RAST.Expr.create_DeclareVar(RAST.DeclareType.create_MUT(), Dafny.Sequence.UnicodeFromString("z"), Std.Wrappers.Option.create_Some(RAST.Type.create_I128()), Std.Wrappers.Option.create_None()), RAST.Expr.create_StmtExpr(RAST.__default.AssignVar(Dafny.Sequence.UnicodeFromString("z"), _1_y), RAST.Expr.create_RawExpr(Dafny.Sequence.UnicodeFromString("return"))))).Optimize(), RAST.Expr.create_StmtExpr(RAST.Expr.create_DeclareVar(RAST.DeclareType.create_MUT(), Dafny.Sequence.UnicodeFromString("z"), Std.Wrappers.Option.create_Some(RAST.Type.create_I128()), Std.Wrappers.Option.create_Some(_1_y)), RAST.Expr.create_RawExpr(Dafny.Sequence.UnicodeFromString("return"))))); + Dafny.ISequence _2_coverageExpression; + _2_coverageExpression = Dafny.Sequence.FromElements(RAST.Expr.create_RawExpr(Dafny.Sequence.UnicodeFromString("abc")), RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x")), RAST.Expr.create_Match(RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x")), Dafny.Sequence.FromElements(RAST.MatchCase.create(Dafny.Sequence.UnicodeFromString("abc"), RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x"))))), RAST.Expr.create_StmtExpr(RAST.Expr.create_RawExpr(Dafny.Sequence.UnicodeFromString("panic!()")), RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("a"))), RAST.Expr.create_Block(RAST.Expr.create_RawExpr(Dafny.Sequence.UnicodeFromString("abc"))), RAST.Expr.create_StructBuild(RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("dummy")), Dafny.Sequence.FromElements(RAST.AssignIdentifier.create(Dafny.Sequence.UnicodeFromString("foo"), RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("bar"))))), RAST.Expr.create_StructBuild(RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("dummy")), Dafny.Sequence.FromElements(RAST.AssignIdentifier.create(Dafny.Sequence.UnicodeFromString("foo"), RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("bar"))), RAST.AssignIdentifier.create(Dafny.Sequence.UnicodeFromString("foo2"), RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("bar"))))), RAST.Expr.create_Tuple(Dafny.Sequence.FromElements(RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x")))), RAST.Expr.create_UnaryOp(Dafny.Sequence.UnicodeFromString("-"), RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x")), DAST.Format.UnaryOpFormat.create_NoFormat()), RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("+"), RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x")), RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("y")), DAST.Format.BinaryOpFormat.create_NoFormat()), RAST.Expr.create_TypeAscription(RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x")), RAST.Type.create_I128()), RAST.Expr.create_LiteralInt(Dafny.Sequence.UnicodeFromString("322")), RAST.Expr.create_LiteralString(Dafny.Sequence.UnicodeFromString("abc"), true, false), RAST.Expr.create_LiteralString(Dafny.Sequence.UnicodeFromString("abc"), false, true), RAST.Expr.create_DeclareVar(RAST.DeclareType.create_MUT(), Dafny.Sequence.UnicodeFromString("abc"), Std.Wrappers.Option.create_Some(RAST.Type.create_I128()), Std.Wrappers.Option.create_None()), RAST.Expr.create_DeclareVar(RAST.DeclareType.create_CONST(), Dafny.Sequence.UnicodeFromString("abc"), Std.Wrappers.Option.create_None(), Std.Wrappers.Option.create_Some(RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x")))), RAST.__default.AssignVar(Dafny.Sequence.UnicodeFromString("abc"), RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x"))), RAST.Expr.create_IfExpr(RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x")), RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x")), RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x"))), RAST.Expr.create_Loop(Std.Wrappers.Option.create_Some(RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x"))), RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x"))), RAST.Expr.create_For(Dafny.Sequence.UnicodeFromString("abc"), RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x")), RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x"))), RAST.Expr.create_Labelled(Dafny.Sequence.UnicodeFromString("abc"), RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x"))), RAST.Expr.create_Break(Std.Wrappers.Option>.create_None()), RAST.Expr.create_Break(Std.Wrappers.Option>.create_Some(Dafny.Sequence.UnicodeFromString("l"))), RAST.Expr.create_Continue(Std.Wrappers.Option>.create_None()), RAST.Expr.create_Continue(Std.Wrappers.Option>.create_Some(Dafny.Sequence.UnicodeFromString("l"))), RAST.Expr.create_Return(Std.Wrappers.Option.create_None()), RAST.Expr.create_Return(Std.Wrappers.Option.create_Some(RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x")))), RAST.Expr.create_Call(RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x")), Dafny.Sequence.FromElements()), RAST.Expr.create_Call(RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x")), Dafny.Sequence.FromElements(RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x")), RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("y")))), RAST.Expr.create_CallType(RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x")), Dafny.Sequence.FromElements(RAST.Type.create_I128(), RAST.Type.create_U32())), RAST.Expr.create_Select(RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x")), Dafny.Sequence.UnicodeFromString("abc")), RAST.Expr.create_MemberSelect(RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x")), Dafny.Sequence.UnicodeFromString("abc"))); + BigInteger _hi0 = new BigInteger((_2_coverageExpression).Count); + for (BigInteger _3_i = BigInteger.Zero; _3_i < _hi0; _3_i++) { + RAST._IExpr _4_c; + _4_c = (_2_coverageExpression).Select(_3_i); + RAST._IPrintingInfo _5___v0; + _5___v0 = (_4_c).printingInfo; + RAST._IExpr _6___v1; + _6___v1 = (_4_c).Optimize(); + Dafny.IMap> _7___v2; + _7___v2 = Dafny.Map>.FromElements(new Dafny.Pair>(_4_c, (_4_c)._ToString(Dafny.Sequence.UnicodeFromString("")))); + RAST._IExpr _8___v3; + _8___v3 = (RAST.Expr.create_StmtExpr(RAST.Expr.create_DeclareVar(RAST.DeclareType.create_MUT(), Dafny.Sequence.UnicodeFromString("abc"), Std.Wrappers.Option.create_Some(RAST.Type.create_I128()), Std.Wrappers.Option.create_None()), _4_c)).Optimize(); + RAST._IExpr _9___v4; + _9___v4 = (RAST.Expr.create_StmtExpr(RAST.Expr.create_DeclareVar(RAST.DeclareType.create_MUT(), Dafny.Sequence.UnicodeFromString("abc"), Std.Wrappers.Option.create_Some(RAST.Type.create_I128()), Std.Wrappers.Option.create_None()), RAST.Expr.create_StmtExpr(RAST.__default.AssignVar(Dafny.Sequence.UnicodeFromString("abc"), _4_c), RAST.Expr.create_RawExpr(Dafny.Sequence.UnicodeFromString(""))))).Optimize(); + RAST._IExpr _10___v5; + _10___v5 = (RAST.Expr.create_UnaryOp(Dafny.Sequence.UnicodeFromString("&"), _4_c, DAST.Format.UnaryOpFormat.create_NoFormat())).Optimize(); + RAST._IExpr _11___v6; + _11___v6 = (RAST.Expr.create_UnaryOp(Dafny.Sequence.UnicodeFromString("!"), _4_c, DAST.Format.UnaryOpFormat.create_NoFormat())).Optimize(); + RAST._IExpr _12___v7; + _12___v7 = (DafnyToRustCompilerCoverage.RASTCoverage.__default.ConversionNum(RAST.Type.create_U8(), _4_c)).Optimize(); + RAST._IExpr _13___v8; + _13___v8 = (DafnyToRustCompilerCoverage.RASTCoverage.__default.ConversionNum(RAST.Type.create_U8(), RAST.Expr.create_Call(_4_c, Dafny.Sequence.FromElements()))).Optimize(); + RAST._IExpr _14___v9; + _14___v9 = (DafnyToRustCompilerCoverage.RASTCoverage.__default.ConversionNum(RAST.Type.create_U8(), RAST.Expr.create_Call(RAST.Expr.create_MemberSelect(_4_c, Dafny.Sequence.UnicodeFromString("int!")), Dafny.Sequence.FromElements()))).Optimize(); + RAST._IExpr _15___v10; + _15___v10 = (DafnyToRustCompilerCoverage.RASTCoverage.__default.ConversionNum(RAST.Type.create_U8(), RAST.Expr.create_Call(RAST.Expr.create_MemberSelect(RAST.Expr.create_MemberSelect(_4_c, Dafny.Sequence.UnicodeFromString("dafny_runtime")), Dafny.Sequence.UnicodeFromString("int!")), Dafny.Sequence.FromElements()))).Optimize(); + RAST._IExpr _16___v11; + _16___v11 = (DafnyToRustCompilerCoverage.RASTCoverage.__default.ConversionNum(RAST.Type.create_U8(), RAST.Expr.create_Call(RAST.Expr.create_MemberSelect(RAST.Expr.create_MemberSelect(RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("")), Dafny.Sequence.UnicodeFromString("dafny_runtime")), Dafny.Sequence.UnicodeFromString("int!")), Dafny.Sequence.FromElements(_4_c)))).Optimize(); + Std.Wrappers._IOption> _17___v12; + _17___v12 = (_4_c).RightMostIdentifier(); } } public static void TestPrintingInfo() { - RAST._IExpr _1113_x; - _1113_x = RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x")); - RAST._IExpr _1114_y; - _1114_y = RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("y")); - DAST.Format._IBinaryOpFormat _1115_bnf; - _1115_bnf = DAST.Format.BinaryOpFormat.create_NoFormat(); + RAST._IExpr _0_x; + _0_x = RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x")); + RAST._IExpr _1_y; + _1_y = RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("y")); + DAST.Format._IBinaryOpFormat _2_bnf; + _2_bnf = DAST.Format.BinaryOpFormat.create_NoFormat(); DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(((RAST.Expr.create_RawExpr(Dafny.Sequence.UnicodeFromString("x"))).printingInfo).is_UnknownPrecedence); - DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((_1113_x).printingInfo, RAST.PrintingInfo.create_Precedence(BigInteger.One))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((_0_x).printingInfo, RAST.PrintingInfo.create_Precedence(BigInteger.One))); DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_LiteralInt(Dafny.Sequence.UnicodeFromString("3"))).printingInfo, RAST.PrintingInfo.create_Precedence(BigInteger.One))); DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_LiteralString(Dafny.Sequence.UnicodeFromString("abc"), true, false)).printingInfo, RAST.PrintingInfo.create_Precedence(BigInteger.One))); - DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_UnaryOp(Dafny.Sequence.UnicodeFromString("?"), _1113_x, DAST.Format.UnaryOpFormat.create_NoFormat())).printingInfo, RAST.PrintingInfo.create_SuffixPrecedence(new BigInteger(5)))); - DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_UnaryOp(Dafny.Sequence.UnicodeFromString("-"), _1113_x, DAST.Format.UnaryOpFormat.create_NoFormat())).printingInfo, RAST.PrintingInfo.create_Precedence(new BigInteger(6)))); - DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_UnaryOp(Dafny.Sequence.UnicodeFromString("*"), _1113_x, DAST.Format.UnaryOpFormat.create_NoFormat())).printingInfo, RAST.PrintingInfo.create_Precedence(new BigInteger(6)))); - DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_UnaryOp(Dafny.Sequence.UnicodeFromString("!"), _1113_x, DAST.Format.UnaryOpFormat.create_NoFormat())).printingInfo, RAST.PrintingInfo.create_Precedence(new BigInteger(6)))); - DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_UnaryOp(Dafny.Sequence.UnicodeFromString("&"), _1113_x, DAST.Format.UnaryOpFormat.create_NoFormat())).printingInfo, RAST.PrintingInfo.create_Precedence(new BigInteger(6)))); - DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_UnaryOp(Dafny.Sequence.UnicodeFromString("&mut"), _1113_x, DAST.Format.UnaryOpFormat.create_NoFormat())).printingInfo, RAST.PrintingInfo.create_Precedence(new BigInteger(6)))); - DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_UnaryOp(Dafny.Sequence.UnicodeFromString("!!"), _1113_x, DAST.Format.UnaryOpFormat.create_NoFormat())).printingInfo, RAST.PrintingInfo.create_UnknownPrecedence())); - DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_Select(_1113_x, Dafny.Sequence.UnicodeFromString("name"))).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(2), RAST.Associativity.create_LeftToRight()))); - DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_MemberSelect(_1113_x, Dafny.Sequence.UnicodeFromString("name"))).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(2), RAST.Associativity.create_LeftToRight()))); - DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_Call(_1113_x, Dafny.Sequence.FromElements())).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(2), RAST.Associativity.create_LeftToRight()))); - DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_TypeAscription(_1113_x, RAST.Type.create_I128())).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(10), RAST.Associativity.create_LeftToRight()))); - DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("*"), _1113_x, _1114_y, _1115_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(20), RAST.Associativity.create_LeftToRight()))); - DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("/"), _1113_x, _1114_y, _1115_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(20), RAST.Associativity.create_LeftToRight()))); - DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("%"), _1113_x, _1114_y, _1115_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(20), RAST.Associativity.create_LeftToRight()))); - DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("+"), _1113_x, _1114_y, _1115_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(30), RAST.Associativity.create_LeftToRight()))); - DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("-"), _1113_x, _1114_y, _1115_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(30), RAST.Associativity.create_LeftToRight()))); - DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("<<"), _1113_x, _1114_y, _1115_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(40), RAST.Associativity.create_LeftToRight()))); - DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString(">>"), _1113_x, _1114_y, _1115_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(40), RAST.Associativity.create_LeftToRight()))); - DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("&"), _1113_x, _1114_y, _1115_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(50), RAST.Associativity.create_LeftToRight()))); - DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("^"), _1113_x, _1114_y, _1115_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(60), RAST.Associativity.create_LeftToRight()))); - DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("|"), _1113_x, _1114_y, _1115_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(70), RAST.Associativity.create_LeftToRight()))); - DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("=="), _1113_x, _1114_y, _1115_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(80), RAST.Associativity.create_RequiresParentheses()))); - DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("!="), _1113_x, _1114_y, _1115_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(80), RAST.Associativity.create_RequiresParentheses()))); - DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("<"), _1113_x, _1114_y, _1115_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(80), RAST.Associativity.create_RequiresParentheses()))); - DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString(">"), _1113_x, _1114_y, _1115_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(80), RAST.Associativity.create_RequiresParentheses()))); - DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("<="), _1113_x, _1114_y, _1115_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(80), RAST.Associativity.create_RequiresParentheses()))); - DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString(">="), _1113_x, _1114_y, _1115_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(80), RAST.Associativity.create_RequiresParentheses()))); - DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("&&"), _1113_x, _1114_y, _1115_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(90), RAST.Associativity.create_LeftToRight()))); - DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("||"), _1113_x, _1114_y, _1115_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(100), RAST.Associativity.create_LeftToRight()))); - DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString(".."), _1113_x, _1114_y, _1115_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(110), RAST.Associativity.create_RequiresParentheses()))); - DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("..="), _1113_x, _1114_y, _1115_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(110), RAST.Associativity.create_RequiresParentheses()))); - DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("="), _1113_x, _1114_y, _1115_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(110), RAST.Associativity.create_RightToLeft()))); - DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("+="), _1113_x, _1114_y, _1115_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(110), RAST.Associativity.create_RightToLeft()))); - DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("-="), _1113_x, _1114_y, _1115_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(110), RAST.Associativity.create_RightToLeft()))); - DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("*="), _1113_x, _1114_y, _1115_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(110), RAST.Associativity.create_RightToLeft()))); - DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("/="), _1113_x, _1114_y, _1115_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(110), RAST.Associativity.create_RightToLeft()))); - DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("%="), _1113_x, _1114_y, _1115_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(110), RAST.Associativity.create_RightToLeft()))); - DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("&="), _1113_x, _1114_y, _1115_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(110), RAST.Associativity.create_RightToLeft()))); - DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("|="), _1113_x, _1114_y, _1115_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(110), RAST.Associativity.create_RightToLeft()))); - DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("^="), _1113_x, _1114_y, _1115_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(110), RAST.Associativity.create_RightToLeft()))); - DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("<<="), _1113_x, _1114_y, _1115_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(110), RAST.Associativity.create_RightToLeft()))); - DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString(">>="), _1113_x, _1114_y, _1115_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(110), RAST.Associativity.create_RightToLeft()))); - DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("?!?"), _1113_x, _1114_y, _1115_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(BigInteger.Zero, RAST.Associativity.create_RequiresParentheses()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_UnaryOp(Dafny.Sequence.UnicodeFromString("?"), _0_x, DAST.Format.UnaryOpFormat.create_NoFormat())).printingInfo, RAST.PrintingInfo.create_SuffixPrecedence(new BigInteger(5)))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_UnaryOp(Dafny.Sequence.UnicodeFromString("-"), _0_x, DAST.Format.UnaryOpFormat.create_NoFormat())).printingInfo, RAST.PrintingInfo.create_Precedence(new BigInteger(6)))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_UnaryOp(Dafny.Sequence.UnicodeFromString("*"), _0_x, DAST.Format.UnaryOpFormat.create_NoFormat())).printingInfo, RAST.PrintingInfo.create_Precedence(new BigInteger(6)))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_UnaryOp(Dafny.Sequence.UnicodeFromString("!"), _0_x, DAST.Format.UnaryOpFormat.create_NoFormat())).printingInfo, RAST.PrintingInfo.create_Precedence(new BigInteger(6)))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_UnaryOp(Dafny.Sequence.UnicodeFromString("&"), _0_x, DAST.Format.UnaryOpFormat.create_NoFormat())).printingInfo, RAST.PrintingInfo.create_Precedence(new BigInteger(6)))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_UnaryOp(Dafny.Sequence.UnicodeFromString("&mut"), _0_x, DAST.Format.UnaryOpFormat.create_NoFormat())).printingInfo, RAST.PrintingInfo.create_Precedence(new BigInteger(6)))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_UnaryOp(Dafny.Sequence.UnicodeFromString("!!"), _0_x, DAST.Format.UnaryOpFormat.create_NoFormat())).printingInfo, RAST.PrintingInfo.create_UnknownPrecedence())); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_Select(_0_x, Dafny.Sequence.UnicodeFromString("name"))).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(2), RAST.Associativity.create_LeftToRight()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_MemberSelect(_0_x, Dafny.Sequence.UnicodeFromString("name"))).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(2), RAST.Associativity.create_LeftToRight()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_Call(_0_x, Dafny.Sequence.FromElements())).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(2), RAST.Associativity.create_LeftToRight()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_TypeAscription(_0_x, RAST.Type.create_I128())).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(10), RAST.Associativity.create_LeftToRight()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("*"), _0_x, _1_y, _2_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(20), RAST.Associativity.create_LeftToRight()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("/"), _0_x, _1_y, _2_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(20), RAST.Associativity.create_LeftToRight()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("%"), _0_x, _1_y, _2_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(20), RAST.Associativity.create_LeftToRight()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("+"), _0_x, _1_y, _2_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(30), RAST.Associativity.create_LeftToRight()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("-"), _0_x, _1_y, _2_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(30), RAST.Associativity.create_LeftToRight()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("<<"), _0_x, _1_y, _2_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(40), RAST.Associativity.create_LeftToRight()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString(">>"), _0_x, _1_y, _2_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(40), RAST.Associativity.create_LeftToRight()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("&"), _0_x, _1_y, _2_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(50), RAST.Associativity.create_LeftToRight()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("^"), _0_x, _1_y, _2_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(60), RAST.Associativity.create_LeftToRight()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("|"), _0_x, _1_y, _2_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(70), RAST.Associativity.create_LeftToRight()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("=="), _0_x, _1_y, _2_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(80), RAST.Associativity.create_RequiresParentheses()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("!="), _0_x, _1_y, _2_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(80), RAST.Associativity.create_RequiresParentheses()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("<"), _0_x, _1_y, _2_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(80), RAST.Associativity.create_RequiresParentheses()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString(">"), _0_x, _1_y, _2_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(80), RAST.Associativity.create_RequiresParentheses()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("<="), _0_x, _1_y, _2_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(80), RAST.Associativity.create_RequiresParentheses()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString(">="), _0_x, _1_y, _2_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(80), RAST.Associativity.create_RequiresParentheses()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("&&"), _0_x, _1_y, _2_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(90), RAST.Associativity.create_LeftToRight()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("||"), _0_x, _1_y, _2_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(100), RAST.Associativity.create_LeftToRight()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString(".."), _0_x, _1_y, _2_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(110), RAST.Associativity.create_RequiresParentheses()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("..="), _0_x, _1_y, _2_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(110), RAST.Associativity.create_RequiresParentheses()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("="), _0_x, _1_y, _2_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(110), RAST.Associativity.create_RightToLeft()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("+="), _0_x, _1_y, _2_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(110), RAST.Associativity.create_RightToLeft()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("-="), _0_x, _1_y, _2_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(110), RAST.Associativity.create_RightToLeft()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("*="), _0_x, _1_y, _2_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(110), RAST.Associativity.create_RightToLeft()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("/="), _0_x, _1_y, _2_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(110), RAST.Associativity.create_RightToLeft()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("%="), _0_x, _1_y, _2_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(110), RAST.Associativity.create_RightToLeft()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("&="), _0_x, _1_y, _2_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(110), RAST.Associativity.create_RightToLeft()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("|="), _0_x, _1_y, _2_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(110), RAST.Associativity.create_RightToLeft()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("^="), _0_x, _1_y, _2_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(110), RAST.Associativity.create_RightToLeft()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("<<="), _0_x, _1_y, _2_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(110), RAST.Associativity.create_RightToLeft()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString(">>="), _0_x, _1_y, _2_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(110), RAST.Associativity.create_RightToLeft()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("?!?"), _0_x, _1_y, _2_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(BigInteger.Zero, RAST.Associativity.create_RequiresParentheses()))); DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_Break(Std.Wrappers.Option>.create_None())).printingInfo, RAST.PrintingInfo.create_UnknownPrecedence())); } public static void TestExpr() diff --git a/Source/DafnyCore/AST/Statements/Assignment/LocalVariable.cs b/Source/DafnyCore/AST/Statements/Assignment/LocalVariable.cs index 63a03a1c218..7d36fc0cd64 100644 --- a/Source/DafnyCore/AST/Statements/Assignment/LocalVariable.cs +++ b/Source/DafnyCore/AST/Statements/Assignment/LocalVariable.cs @@ -77,7 +77,7 @@ public string AssignUniqueName(VerificationIdGenerator generator) { private string sanitizedName; public string SanitizedName(CompilationIdGenerator generator) { - return sanitizedName ??= $"_{generator}_{SanitizedNameShadowable}"; + return sanitizedName ??= $"_{generator.FreshNumericId()}_{SanitizedNameShadowable}"; } string compileName; diff --git a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs index 6ec5686ec7f..c9b5a3e2903 100644 --- a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs +++ b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs @@ -899,7 +899,7 @@ private void CompileDatatypeDestructorsAndAddToInterface(DatatypeDecl dt, Concre var compiledConstructorsProcessed = 0; for (var i = 0; i < dtor.EnclosingCtors.Count; i++) { var ctor_i = dtor.EnclosingCtors[i]; - Contract.Assert(arg.CompileName == dtor.CorrespondingFormals[i].CompileName); + Contract.Assert(arg.CompileName(FormalIdGenerator) == dtor.CorrespondingFormals[i].CompileName(FormalIdGenerator)); if (ctor_i.IsGhost) { continue; } @@ -2046,18 +2046,18 @@ protected override void EmitHalt(IToken tok, Expression/*?*/ messageExpr, Concre protected override ConcreteSyntaxTree EmitForStmt(IToken tok, IVariable loopIndex, bool goingUp, string /*?*/ endVarName, List body, LList