Fix Rust backend crashes due to match cases and static consts (#4458)

Fix Rust backend crashes due to match cases and static consts <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> --- Stack created with [Sapling](https://sapling-scm.com). Best reviewed with [ReviewStack](https://reviewstack.dev/dafny-lang/dafny/pull/4458). * #4518 * #4468 * #4459 * __->__ #4458
dafny-lang · Sep 6, 2023 · 0bf02c4 · 0bf02c4
1 parent 8d8bc5f
commit 0bf02c4
Show file tree

Hide file tree

Showing 4 changed files with 2,078 additions and 971 deletions.
diff --git a/Source/DafnyCore/Compilers/Dafny/Compiler-dafny.cs b/Source/DafnyCore/Compilers/Dafny/Compiler-dafny.cs
@@ -1058,7 +1058,13 @@ protected override void EmitLiteralExpr(ConcreteSyntaxTree wr, LiteralExpr e) {
             ));
             break;
           case StaticReceiverExpr:
-            throw new NotImplementedException();
+            if (e.Type.NormalizeExpandKeepConstraints() is UserDefinedType udt && udt.ResolvedClass is DatatypeDecl dt &&
+                DatatypeWrapperEraser.IsErasableDatatypeWrapper(Options, dt, out _)) {
+              baseExpr = (DAST.Expression)DAST.Expression.create_Companion(PathFromTopLevel(udt.ResolvedClass));
+            } else {
+              baseExpr = (DAST.Expression)DAST.Expression.create_Companion(PathFromTopLevel(e.Type.AsTopLevelTypeWithMembers));
+            }
+            break;
           default:
             DAST.Type baseType;
             if (e.Type.AsNewtype != null) {
@@ -1540,6 +1546,20 @@ protected override ConcreteSyntaxTree CreateLambda(List<Type> inTypes, IToken to
       }
     }
 
+    protected override void EmitLambdaApply(ConcreteSyntaxTree wr, out ConcreteSyntaxTree wLambda, out ConcreteSyntaxTree wArg) {
+      if (wr is BuilderSyntaxTree<StatementContainer> builder) {
+        var lambda = builder.Builder.Call();
+        wLambda = new BuilderSyntaxTree<ExprContainer>(lambda);
+        wArg = new BuilderSyntaxTree<ExprContainer>(lambda);
+      } else if (wr is BuilderSyntaxTree<ExprContainer> exprBuilder) {
+        var lambda = exprBuilder.Builder.Call();
+        wLambda = new BuilderSyntaxTree<ExprContainer>(lambda);
+        wArg = new BuilderSyntaxTree<ExprContainer>(lambda);
+      } else {
+        throw new InvalidOperationException();
+      }
+    }
+
     protected override void CreateIIFE(string bvName, Type bvType, IToken bvTok, Type bodyType, IToken bodyTok,
       ConcreteSyntaxTree wr, ref ConcreteSyntaxTree wStmts, out ConcreteSyntaxTree wrRhs, out ConcreteSyntaxTree wrBody) {
       if (wr is BuilderSyntaxTree<ExprContainer> builder) {

diff --git a/Source/DafnyCore/Compilers/Rust/Dafny-compiler-rust.dfy b/Source/DafnyCore/Compilers/Rust/Dafny-compiler-rust.dfy
@@ -1501,6 +1501,15 @@ module {:extern "DCOMP"} DCOMP {
           isErased := true;
           readIdents := recIdents;
         }
+        case Select(Companion(c), field, isConstant, isDatatype) => {
+          var onString, onOwned, onErased, recIdents := GenExpr(Companion(c), selfIdent, params, false);
+
+          s := onString + "::r#" + field + "()";
+
+          isOwned := true;
+          isErased := false;
+          readIdents := recIdents;
+        }
         case Select(on, field, isConstant, isDatatype) => {
           var onString, onOwned, onErased, recIdents := GenExpr(on, selfIdent, params, false);
           if !onErased {

diff --git a/Source/DafnyCore/Compilers/SinglePassCompiler.cs b/Source/DafnyCore/Compilers/SinglePassCompiler.cs
@@ -5253,9 +5253,11 @@ void EmitExpr(Expression e2, ConcreteSyntaxTree wr2, bool inLetExpr, ConcreteSyn
         //   }
         // }))(src)
 
+        EmitLambdaApply(wr, out var wLambda, out var wArg);
+
         string source = ProtectedFreshId("_source");
         ConcreteSyntaxTree w;
-        w = CreateLambda(new List<Type>() { e.Source.Type }, e.tok, new List<string>() { source }, e.Type, wr, wStmts);
+        w = CreateLambda(new List<Type>() { e.Source.Type }, e.tok, new List<string>() { source }, e.Type, wLambda, wStmts);
 
         if (e.Cases.Count == 0) {
           // the verifier would have proved we never get here; still, we need some code that will compile
@@ -5270,8 +5272,7 @@ void EmitExpr(Expression e2, ConcreteSyntaxTree wr2, bool inLetExpr, ConcreteSyn
           }
         }
         // We end with applying the source expression to the delegate we just built
-        wr.Write(LambdaExecute);
-        TrParenExpr(e.Source, wr, inLetExprBody, wStmts);
+        EmitExpr(e.Source, inLetExprBody, wArg, wStmts);
 
       } else if (expr is QuantifierExpr) {
         var e = (QuantifierExpr)expr;
@@ -5435,6 +5436,12 @@ void EmitExpr(Expression e2, ConcreteSyntaxTree wr2, bool inLetExpr, ConcreteSyn
       }
     }
 
+    protected virtual void EmitLambdaApply(ConcreteSyntaxTree wr, out ConcreteSyntaxTree wLambda, out ConcreteSyntaxTree wArg) {
+      wLambda = wr.Fork();
+      wr.Write(LambdaExecute);
+      wArg = wr.ForkInParens();
+    }
+
     protected void WriteTypeDescriptors(TopLevelDecl decl, List<Type> typeArguments, ConcreteSyntaxTree wrArgumentList, ref string sep) {
       Contract.Requires(decl.TypeArgs.Count == typeArguments.Count);
       var typeParameters = decl.TypeArgs;