Fix a variety of bugs in Rust backend based on ESDK testing (#4538)

Fix a variety of bugs in Rust backend based on ESDK testing














<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT

license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

Source/DafnyCore/AST/Expressions/DefaultValueExpression.cs

@@ -73,6 +73,8 @@ public void FillIn(ModuleResolver resolver, Dictionary<DefaultValueExpression, W
     var s = new DefaultValueSubstituter(resolver, visited, this.receiver, this.substMap, typeMap);
     this.ResolvedExpression = s.Substitute(this.formal.DefaultValue);
     visited[this] = WorkProgress.Done;
+
+    this.ResolvedExpression.Type = this.Type;
   }
 
   class DefaultValueSubstituter : Substituter {

Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs

@@ -1988,8 +1988,11 @@ protected override ConcreteSyntaxTree EmitForStmt(IToken tok, IVariable loopInde
       return startWr;
     }
 
-    protected override ConcreteSyntaxTree CreateForLoop(string indexVar, string bound, ConcreteSyntaxTree wr, string start = null) {
+    protected override ConcreteSyntaxTree CreateForLoop(string indexVar, Action<ConcreteSyntaxTree> boundAction, ConcreteSyntaxTree wr, string start = null) {
       start = start ?? "0";
+      var boundWriter = new ConcreteSyntaxTree();
+      boundAction(boundWriter);
+      var bound = boundWriter.ToString();
       return wr.NewNamedBlock("for (var {0} = {2}; {0} < {1}; {0}++)", indexVar, bound, start);
     }
 

Source/DafnyCore/Compilers/Cplusplus/Compiler-cpp.cs

@@ -1326,8 +1326,11 @@ protected override ConcreteSyntaxTree EmitForStmt(IToken tok, IVariable loopInde
       throw new UnsupportedFeatureException(tok, Feature.ForLoops, "for loops have not yet been implemented");
     }
 
-    protected override ConcreteSyntaxTree CreateForLoop(string indexVar, string bound, ConcreteSyntaxTree wr, string start = null) {
+    protected override ConcreteSyntaxTree CreateForLoop(string indexVar, Action<ConcreteSyntaxTree> boundAction, ConcreteSyntaxTree wr, string start = null) {
       start = start ?? "0";
+      var boundWriter = new ConcreteSyntaxTree();
+      boundAction(boundWriter);
+      var bound = boundWriter.ToString();
       return wr.NewNamedBlock("for (auto {0} = {2}; {0} < {1}; {0}++)", indexVar, bound, start);
     }
 

Source/DafnyCore/Compilers/Dafny/AST.dfy

@@ -1,5 +1,5 @@
 module {:extern "DAST"} DAST {
-  datatype Module = Module(name: string, body: seq<ModuleItem>)
+  datatype Module = Module(name: string, isExtern: bool, body: seq<ModuleItem>)
 
   datatype ModuleItem = Module(Module) | Class(Class) | Trait(Trait) | Newtype(Newtype) | Datatype(Datatype)
 
@@ -65,23 +65,35 @@ module {:extern "DAST"} DAST {
 
   datatype CollKind = Seq | Array | Map
 
+  datatype BinOp =
+    Eq(referential: bool, nullable: bool) |
+    Neq(referential: bool, nullable: bool) |
+    Div() | EuclidianDiv() |
+    Mod() | EuclidianMod() |
+    Implies() |
+    In() |
+    NotIn() |
+    SetDifference() |
+    Concat() |
+    Passthrough(string)
+
   datatype Expression =
     Literal(Literal) |
     Ident(string) |
     Companion(seq<Ident>) |
     Tuple(seq<Expression>) |
-    New(path: seq<Ident>, args: seq<Expression>) |
-    NewArray(dims: seq<Expression>) |
-    DatatypeValue(path: seq<Ident>, variant: string, isCo: bool, contents: seq<(string, Expression)>) |
+    New(path: seq<Ident>, typeArgs: seq<Type>, args: seq<Expression>) |
+    NewArray(dims: seq<Expression>, typ: Type) |
+    DatatypeValue(path: seq<Ident>, typeArgs: seq<Type>, variant: string, isCo: bool, contents: seq<(string, Expression)>) |
     Convert(value: Expression, from: Type, typ: Type) |
     SeqConstruct(length: Expression, elem: Expression) |
-    SeqValue(elements: seq<Expression>) |
+    SeqValue(elements: seq<Expression>, typ: Type) |
     SetValue(elements: seq<Expression>) |
     MapValue(mapElems: seq<(Expression, Expression)>) |
     This() |
     Ite(cond: Expression, thn: Expression, els: Expression) |
     UnOp(unOp: UnaryOp, expr: Expression) |
-    BinOp(op: string, left: Expression, right: Expression) |
+    BinOp(op: BinOp, left: Expression, right: Expression) |
     ArrayLen(expr: Expression, dim: nat) |
     Select(expr: Expression, field: string, isConstant: bool, onDatatype: bool) |
     SelectFn(expr: Expression, field: string, onDatatype: bool, isStatic: bool, arity: nat) |
@@ -96,9 +108,11 @@ module {:extern "DAST"} DAST {
     TypeTest(on: Expression, dType: seq<Ident>, variant: string) |
     InitializationValue(typ: Type) |
     BoolBoundedPool() |
+    SetBoundedPool(of: Expression) |
+    SeqBoundedPool(of: Expression, includeDuplicates: bool) |
     IntRange(lo: Expression, hi: Expression)
 
   datatype UnaryOp = Not | BitwiseNot | Cardinality
 
-  datatype Literal = BoolLiteral(bool) | IntLiteral(string, Type) | DecLiteral(string, string, Type) | StringLiteral(string) | CharLiteral(char) | Null
+  datatype Literal = BoolLiteral(bool) | IntLiteral(string, Type) | DecLiteral(string, string, Type) | StringLiteral(string) | CharLiteral(char) | Null(Type)
 }

Source/DafnyCore/Compilers/Dafny/ASTBuilder.cs

@@ -21,19 +21,21 @@ public List<Module> Finish() {
   interface ModuleContainer {
     void AddModule(Module item);
 
-    public ModuleBuilder Module(string name) {
-      return new ModuleBuilder(this, name);
+    public ModuleBuilder Module(string name, bool isExtern) {
+      return new ModuleBuilder(this, name, isExtern);
     }
   }
 
   class ModuleBuilder : ClassContainer, TraitContainer, NewtypeContainer, DatatypeContainer {
     readonly ModuleContainer parent;
     readonly string name;
+    readonly bool isExtern;
     readonly List<ModuleItem> body = new();
 
-    public ModuleBuilder(ModuleContainer parent, string name) {
+    public ModuleBuilder(ModuleContainer parent, string name, bool isExtern) {
       this.parent = parent;
       this.name = name;
+      this.isExtern = isExtern;
     }
 
     public void AddModule(Module item) {
@@ -57,7 +59,11 @@ public void AddDatatype(Datatype item) {
     }
 
     public object Finish() {
-      parent.AddModule((Module)Module.create(Sequence<Rune>.UnicodeFromString(this.name), Sequence<ModuleItem>.FromArray(body.ToArray())));
+      parent.AddModule((Module)Module.create(
+        Sequence<Rune>.UnicodeFromString(this.name),
+        this.isExtern,
+        Sequence<ModuleItem>.FromArray(body.ToArray())
+      ));
       return parent;
     }
   }
@@ -960,7 +966,7 @@ interface ExprContainer {
 
     void AddBuildable(BuildableExpr item);
 
-    BinOpBuilder BinOp(string op) {
+    BinOpBuilder BinOp(DAST.BinOp op) {
       var ret = new BinOpBuilder(op);
       AddBuildable(ret);
       return ret;
@@ -1050,6 +1056,7 @@ interface BuildableLhs {
   class ArrayLhs : BuildableLhs, ExprContainer {
     readonly List<DAST.Expression> indices;
     object arrayExpr = null;
+    readonly System.Diagnostics.StackTrace stackTrace = new(true);
 
     public ArrayLhs(List<DAST.Expression> indices) {
       this.indices = indices;
@@ -1072,6 +1079,9 @@ public void AddBuildable(BuildableExpr item) {
     }
 
     public DAST.AssignLhs Build() {
+      if (arrayExpr == null) {
+        Console.WriteLine(stackTrace);
+      }
       var builtArrayExpr = new List<DAST.Expression>();
       ExprContainer.RecursivelyBuild(new List<object> { arrayExpr }, builtArrayExpr);
 
@@ -1084,10 +1094,10 @@ interface BuildableExpr {
   }
 
   class BinOpBuilder : ExprContainer, BuildableExpr {
-    readonly string op;
+    readonly DAST.BinOp op;
     readonly List<object> operands = new();
 
-    public BinOpBuilder(string op) {
+    public BinOpBuilder(DAST.BinOp op) {
       this.op = op;
     }
 
@@ -1106,7 +1116,7 @@ public DAST.Expression Build() {
 
       var builtOperands = new List<DAST.Expression>();
       ExprContainer.RecursivelyBuild(operands, builtOperands);
-      return (DAST.Expression)DAST.Expression.create_BinOp(Sequence<Rune>.UnicodeFromString(op), builtOperands[0], builtOperands[1]);
+      return (DAST.Expression)DAST.Expression.create_BinOp(op, builtOperands[0], builtOperands[1]);
     }
   }