Support for detecting complete assignments in constructor and panic i…

…f unassigned

Source/DafnyCore/Backends/Rust/Dafny-compiler-rust-definitions.dfy

@@ -190,14 +190,24 @@ module {:extern "Defs"} DafnyToRustCompilerDefinitions {
     {
       Environment(names + [name], types[name := tpe], assignmentStatusKnown - {name})
     }
-    function merge(other: Environment): Environment
+    // Merges a current environment with a new one
+    function Merge(other: Environment): Environment
     {
       Environment(
         names + other.names,
         types + other.types,
         assignmentStatusKnown + other.assignmentStatusKnown
       )
     }
+    // When exiting If-then-else, we can remove variables that were unassigned in both branches
+    function Join(thenBranch: Environment, elseBranch: Environment): Environment {
+      var removed := types.Keys - (thenBranch.types.Keys + elseBranch.types.Keys);
+      Environment(
+        Std.Collections.Seq.Filter(name => name !in removed, names),
+        types - removed,
+        assignmentStatusKnown - removed
+      )
+    }
     // Used to removed from the environment the "_is_assigned" vars used to initialize fields
     function RemoveAssigned(name: string): Environment
       requires name in names
@@ -519,13 +529,18 @@ module {:extern "Defs"} DafnyToRustCompilerDefinitions {
     ensures BecomesLeftCallsRight(op) ==> !BecomesRightCallsLeft(op)
   {}
 
+  function Panic(optText: string := ""): R.Expr {
+    if optText == "" then
+      R.Identifier("panic!").Apply0()
+    else
+      R.Identifier("panic!").Apply1(R.LiteralString(optText, binary := false, verbatim := false))
+  }
+
   function UnreachablePanicIfVerified(pointerType: PointerType, optText: string := ""): R.Expr {
     if pointerType.Raw? then
       R.Unsafe(R.Block(R.std.MSel("hint").AsExpr().FSel("unreachable_unchecked").Apply0()))
-    else if optText == "" then
-      R.Identifier("panic!").Apply0()
     else
-      R.Identifier("panic!").Apply1(R.LiteralString(optText, binary := false, verbatim := false))
+      Panic(optText)
   }
 
   function DefaultDatatypeImpl(

Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy

@@ -2229,9 +2229,9 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
             var fieldName := escapeVar(field.formal.name);
             var fieldTyp := GenType(field.formal.typ, GenTypeContext.default());
             var isAssignedVar := AddAssignedPrefix(fieldName);
-            if isAssignedVar in newEnv.names {
-              assume {:axiom} InitializationValue(field.formal.typ) < stmt; // Needed for termination
-              var rhs, _, _ := GenExpr(InitializationValue(field.formal.typ), selfIdent, env, OwnershipOwned);
+            if isAssignedVar in newEnv.names { // We can't determine statically if the field was assigned
+              var panicked := "Field "+ fieldName +" is not initialized";
+              var rhs := UnreachablePanicIfVerified(pointerType, panicked);
               readIdents := readIdents + {isAssignedVar};
               var update_if_uninit :=
                 if field.isConstant then update_field_if_uninit_macro else update_field_mut_if_uninit_macro;
@@ -2307,7 +2307,9 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
           readIdents := readIdents + thnIdents;
           var els, elsIdents, elsEnv := GenStmts(elsDafny, selfIdent, env, isLast, earlyReturn);
           readIdents := readIdents + elsIdents;
-          newEnv := env;
+
+          // All variables that both thnEnv and elsEnv remove can be removed from the environment
+          newEnv := env.Join(thnEnv, elsEnv);
           generated := R.IfExpr(cond, thn, els);
         }
         case Labeled(lbl, body) => {
@@ -4162,7 +4164,7 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
             paramNames := paramNames + [name];
             paramTypesMap := paramTypesMap[name := params[i].tpe];
           }
-          var subEnv := env.ToOwned().merge(Environment(paramNames, paramTypesMap, {}));
+          var subEnv := env.ToOwned().Merge(Environment(paramNames, paramTypesMap, {}));
 
           var recursiveGen, recIdents, _ := GenStmts(body, if selfIdent != NoSelf then ThisTyped("_this", selfIdent.dafnyType) else NoSelf, subEnv, true, None);
           readIdents := {};

Source/DafnyCore/Backends/Rust/RustBackend.cs

@@ -48,6 +48,9 @@ public override string TargetBaseDir(string dafnyProgramName) =>
     $"{Path.GetFileNameWithoutExtension(dafnyProgramName)}-rust/src";
 
   protected override DafnyWrittenCodeGenerator CreateDafnyWrittenCompiler() {
+    if (Options.Get(CommonOptionBag.RelaxDefiniteAssignment)) {
+      throw new UnsupportedInvalidOperationException("The Rust compiler does not support `--relax-definite-assignment`");
+    }
     return new RustCodeGenerator(Options);
   }
 

Source/DafnyCore/GeneratedFromDafny/Defs.cs

@@ -491,14 +491,19 @@ public static bool BecomesRightCallsLeft(DAST._IBinOp op) {
         return false;
       }
     }
+    public static RAST._IExpr Panic(Dafny.ISequence<Dafny.Rune> optText) {
+      if ((optText).Equals(Dafny.Sequence<Dafny.Rune>.UnicodeFromString(""))) {
+        return (RAST.Expr.create_Identifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("panic!"))).Apply0();
+      } else {
+        return (RAST.Expr.create_Identifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("panic!"))).Apply1(RAST.Expr.create_LiteralString(optText, false, false));
+      }
+    }
     public static RAST._IExpr UnreachablePanicIfVerified(Defs._IPointerType pointerType, Dafny.ISequence<Dafny.Rune> optText)
     {
       if ((pointerType).is_Raw) {
         return RAST.__default.Unsafe(RAST.Expr.create_Block(((((RAST.__default.std).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("hint"))).AsExpr()).FSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("unreachable_unchecked"))).Apply0()));
-      } else if ((optText).Equals(Dafny.Sequence<Dafny.Rune>.UnicodeFromString(""))) {
-        return (RAST.Expr.create_Identifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("panic!"))).Apply0();
       } else {
-        return (RAST.Expr.create_Identifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("panic!"))).Apply1(RAST.Expr.create_LiteralString(optText, false, false));
+        return Defs.__default.Panic(optText);
       }
     }
     public static RAST._IModDecl DefaultDatatypeImpl(Dafny.ISequence<RAST._ITypeParamDecl> rTypeParamsDecls, RAST._IType datatypeType, RAST._IExpr datatypeName, Dafny.ISequence<RAST._IAssignIdentifier> structAssignments)
@@ -970,7 +975,8 @@ public interface _IEnvironment {
     bool NeedsAsRefForBorrow(Dafny.ISequence<Dafny.Rune> name);
     bool IsMaybePlacebo(Dafny.ISequence<Dafny.Rune> name);
     Defs._IEnvironment AddAssigned(Dafny.ISequence<Dafny.Rune> name, RAST._IType tpe);
-    Defs._IEnvironment merge(Defs._IEnvironment other);
+    Defs._IEnvironment Merge(Defs._IEnvironment other);
+    Defs._IEnvironment Join(Defs._IEnvironment thenBranch, Defs._IEnvironment elseBranch);
     Defs._IEnvironment RemoveAssigned(Dafny.ISequence<Dafny.Rune> name);
     Defs._IEnvironment AddAssignmentStatus(Dafny.ISequence<Dafny.Rune> name, Defs._IAssignmentStatus assignmentStatus);
     bool IsAssignmentStatusKnown(Dafny.ISequence<Dafny.Rune> name);
@@ -1090,9 +1096,16 @@ public Defs._IEnvironment AddAssigned(Dafny.ISequence<Dafny.Rune> name, RAST._IT
     {
       return Defs.Environment.create(Dafny.Sequence<Dafny.ISequence<Dafny.Rune>>.Concat((this).dtor_names, Dafny.Sequence<Dafny.ISequence<Dafny.Rune>>.FromElements(name)), Dafny.Map<Dafny.ISequence<Dafny.Rune>, RAST._IType>.Update((this).dtor_types, name, tpe), Dafny.Set<Dafny.ISequence<Dafny.Rune>>.Difference((this).dtor_assignmentStatusKnown, Dafny.Set<Dafny.ISequence<Dafny.Rune>>.FromElements(name)));
     }
-    public Defs._IEnvironment merge(Defs._IEnvironment other) {
+    public Defs._IEnvironment Merge(Defs._IEnvironment other) {
       return Defs.Environment.create(Dafny.Sequence<Dafny.ISequence<Dafny.Rune>>.Concat((this).dtor_names, (other).dtor_names), Dafny.Map<Dafny.ISequence<Dafny.Rune>, RAST._IType>.Merge((this).dtor_types, (other).dtor_types), Dafny.Set<Dafny.ISequence<Dafny.Rune>>.Union((this).dtor_assignmentStatusKnown, (other).dtor_assignmentStatusKnown));
     }
+    public Defs._IEnvironment Join(Defs._IEnvironment thenBranch, Defs._IEnvironment elseBranch)
+    {
+      Dafny.ISet<Dafny.ISequence<Dafny.Rune>> _0_removed = Dafny.Set<Dafny.ISequence<Dafny.Rune>>.Difference(((this).dtor_types).Keys, Dafny.Set<Dafny.ISequence<Dafny.Rune>>.Union(((thenBranch).dtor_types).Keys, ((elseBranch).dtor_types).Keys));
+      return Defs.Environment.create(Std.Collections.Seq.__default.Filter<Dafny.ISequence<Dafny.Rune>>(Dafny.Helpers.Id<Func<Dafny.ISet<Dafny.ISequence<Dafny.Rune>>, Func<Dafny.ISequence<Dafny.Rune>, bool>>>((_1_removed) => ((System.Func<Dafny.ISequence<Dafny.Rune>, bool>)((_2_name) => {
+  return !(_1_removed).Contains(_2_name);
+})))(_0_removed), (this).dtor_names), Dafny.Map<Dafny.ISequence<Dafny.Rune>, RAST._IType>.Subtract((this).dtor_types, _0_removed), Dafny.Set<Dafny.ISequence<Dafny.Rune>>.Difference((this).dtor_assignmentStatusKnown, _0_removed));
+    }
     public Defs._IEnvironment RemoveAssigned(Dafny.ISequence<Dafny.Rune> name) {
       BigInteger _0_indexInEnv = Std.Collections.Seq.__default.IndexOf<Dafny.ISequence<Dafny.Rune>>((this).dtor_names, name);
       return Defs.Environment.create(Dafny.Sequence<Dafny.ISequence<Dafny.Rune>>.Concat(((this).dtor_names).Subsequence(BigInteger.Zero, _0_indexInEnv), ((this).dtor_names).Drop((_0_indexInEnv) + (BigInteger.One))), Dafny.Map<Dafny.ISequence<Dafny.Rune>, RAST._IType>.Subtract((this).dtor_types, Dafny.Set<Dafny.ISequence<Dafny.Rune>>.FromElements(name)), Dafny.Set<Dafny.ISequence<Dafny.Rune>>.Difference((this).dtor_assignmentStatusKnown, Dafny.Set<Dafny.ISequence<Dafny.Rune>>.FromElements(name)));

Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/classes-relax.dfy

@@ -0,0 +1,36 @@
+// NONUNIFORM: Rust does not support relaxed definite assignment
+// RUN: %exits-with 3 %baredafny run --target=rs --relax-definite-assignment "%s" > "%t"
+// RUN: %diff "%s.wrong.expect" "%t"
+// RUN: %baredafny run --target=rs "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+datatype D = D(value: int)
+
+class Y {
+  var c: int
+  const d: D
+  constructor(c: int) ensures this.c == c && d.value == c {
+    this.c := c;
+    if c == 1 {
+      this.d := D(1);
+    } else {
+      this.d := D(c);
+    }
+  }
+
+  constructor Two(c: int, b: bool) ensures this.c == c && d.value == c
+    requires b
+  {
+    this.c := c; // d not assigned, compilation error.
+    if b {
+      this.d := D(c);
+    }
+    // This will emit a conditional panick but Dafny will prove it's unreachable
+  }
+}
+
+method Main() {
+  var y := new Y(1);
+  var y2 := new Y.Two(1, true);
+  print "Instantiation successful";
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/classes-relax.dfy.expect

@@ -0,0 +1,3 @@
+
+Dafny program verifier finished with 3 verified, 0 errors
+Instantiation successful

Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/classes-relax.dfy.wrong.expect

@@ -0,0 +1,3 @@
+
+Dafny program verifier finished with 3 verified, 0 errors
+(0,-1): Error: Microsoft.Dafny.UnsupportedInvalidOperationException: The Rust compiler does not support `--relax-definite-assignment`