Enable the option enforce determinism for the verify command

.github/workflows/msbuild.yml

@@ -161,7 +161,7 @@ jobs:
           output: both
           # Fail if less than 86% total coverage, measured across all packages combined.
           # Report "yellow" status if less than 90% total coverage.
-          thresholds: '86 90'
+          thresholds: '85 90'
 
       - name: Code coverage report (LSP)
         uses: irongut/[email protected]

Source/DafnyCore/AST/Statements/Assignment/AssignSuchThatStmt.cs

@@ -77,6 +77,10 @@ public override void GenResolve(INewOrOldResolver resolver, ResolutionContext re
     Contract.Requires(this != null);
     Contract.Requires(resolutionContext != null);
 
+    if (!resolutionContext.IsGhost && resolver.Options.ForbidNondeterminism) {
+      resolver.Reporter.Error(MessageSource.Resolver, GeneratorErrors.ErrorId.c_assign_such_that_forbidden,
+        Tok, "assign-such-that statement forbidden by the --enforce-determinism option");
+    }
     base.GenResolve(resolver, resolutionContext);
 
     if (AssumeToken != null) {

Source/DafnyCore/AST/Statements/Assignment/HavocRhs.cs

@@ -16,4 +16,10 @@ private HavocRhs(Cloner cloner, HavocRhs havocRhs) : base(cloner, havocRhs) {
   public override bool CanAffectPreviouslyKnownExpressions { get { return false; } }
   public override IEnumerable<INode> Children => Enumerable.Empty<Node>();
   public override IEnumerable<INode> PreResolveChildren => Enumerable.Empty<Node>();
+
+  public void Resolve(INewOrOldResolver resolver, ResolutionContext resolutionContext) {
+    if (!resolutionContext.IsGhost && resolver.Options.ForbidNondeterminism) {
+      resolver.Reporter.Error(MessageSource.Resolver, GeneratorErrors.ErrorId.c_nondeterminism_forbidden, Tok, "nondeterministic assignment forbidden by the --enforce-determinism option");
+    }
+  }
 }

Source/DafnyCore/AST/Statements/ControlFlow/AlternativeStmt.cs

@@ -57,4 +57,49 @@ public bool SetIndent(int indentBefore, TokenNewIndentCollector formatter) {
       formatter.VisitAlternatives(Alternatives, indentBefore);
     });
   }
+
+  public void Resolve(INewOrOldResolver resolver, ResolutionContext resolutionContext) {
+    if (!resolutionContext.IsGhost && resolver.Options.ForbidNondeterminism && 2 <= Alternatives.Count) {
+      resolver.Reporter.Error(MessageSource.Resolver, GeneratorErrors.ErrorId.c_case_based_if_forbidden, Tok,
+        "case-based if statement forbidden by the --enforce-determinism option");
+    }
+    ResolveAlternatives(resolver, Alternatives, null, resolutionContext);
+  }
+
+  public static void ResolveAlternatives(INewOrOldResolver resolver, List<GuardedAlternative> alternatives,
+    AlternativeLoopStmt loopToCatchBreaks, ResolutionContext resolutionContext) {
+    Contract.Requires(alternatives != null);
+    Contract.Requires(resolutionContext != null);
+
+    // first, resolve the guards
+    foreach (var alternative in alternatives) {
+      int prevErrorCount = resolver.Reporter.Count(ErrorLevel.Error);
+      resolver.ResolveExpression(alternative.Guard, resolutionContext);  // follows from postcondition of ResolveExpression
+      bool successfullyResolved = resolver.Reporter.Count(ErrorLevel.Error) == prevErrorCount;
+      resolver.ConstrainTypeExprBool(alternative.Guard, "condition is expected to be of type bool, but is {0}");
+    }
+
+    if (loopToCatchBreaks != null) {
+      resolver.LoopStack.Add(loopToCatchBreaks);  // push
+    }
+    foreach (var alternative in alternatives) {
+      resolver.Scope.PushMarker();
+      resolver.DominatingStatementLabels.PushMarker();
+      if (alternative.IsBindingGuard) {
+        var exists = (ExistsExpr)alternative.Guard;
+        foreach (var v in exists.BoundVars) {
+          resolver.ScopePushAndReport(resolver.Scope, v, "bound-variable");
+        }
+      }
+      resolver.ResolveAttributes(alternative, resolutionContext);
+      foreach (Statement ss in alternative.Body) {
+        resolver.ResolveStatementWithLabels(ss, resolutionContext);
+      }
+      resolver.DominatingStatementLabels.PopMarker();
+      resolver.Scope.PopMarker();
+    }
+    if (loopToCatchBreaks != null) {
+      resolver.LoopStack.RemoveAt(resolver.LoopStack.Count - 1);  // pop
+    }
+  }
 }

Source/DafnyCore/AST/Statements/ControlFlow/IfStmt.cs

@@ -86,4 +86,36 @@ public bool SetIndent(int indentBefore, TokenNewIndentCollector formatter) {
     }
     return false;
   }
+
+  public void Resolve(INewOrOldResolver resolver, ResolutionContext resolutionContext) {
+    if (Guard != null) {
+      if (!resolutionContext.IsGhost && IsBindingGuard && resolver.Options.ForbidNondeterminism) {
+        resolver.Reporter.Error(MessageSource.Resolver, GeneratorErrors.ErrorId.c_binding_if_forbidden, Tok, "binding if statement forbidden by the --enforce-determinism option");
+      }
+      resolver.ResolveExpression(Guard, resolutionContext);
+      resolver.ConstrainTypeExprBool(Guard, "condition is expected to be of type bool, but is {0}");
+    } else {
+      if (!resolutionContext.IsGhost && resolver.Options.ForbidNondeterminism) {
+        resolver.Reporter.Error(MessageSource.Resolver, GeneratorErrors.ErrorId.c_nondeterministic_if_forbidden, Tok, "nondeterministic if statement forbidden by the --enforce-determinism option");
+      }
+    }
+
+    resolver.Scope.PushMarker();
+    if (IsBindingGuard) {
+      var exists = (ExistsExpr)Guard;
+      foreach (var v in exists.BoundVars) {
+        resolver.ScopePushAndReport(resolver.Scope, v.Name, v, v.Tok, "bound-variable");
+      }
+    }
+    resolver.DominatingStatementLabels.PushMarker();
+    resolver.ResolveBlockStatement(Thn, resolutionContext);
+    resolver.DominatingStatementLabels.PopMarker();
+    resolver.Scope.PopMarker();
+
+    if (Els != null) {
+      resolver.DominatingStatementLabels.PushMarker();
+      resolver.ResolveStatement(Els, resolutionContext);
+      resolver.DominatingStatementLabels.PopMarker();
+    }
+  }
 }

Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Statement.cs

@@ -98,11 +98,7 @@ protected void TrStmt(Statement stmt, ConcreteSyntaxTree wr, ConcreteSyntaxTree
               var rhsTypes = new List<Type>();
               foreach (var assignStmt in assignStmts) {
                 var rhs = assignStmt.Rhs;
-                if (rhs is HavocRhs) {
-                  if (Options.ForbidNondeterminism) {
-                    Error(ErrorId.c_nondeterminism_forbidden, rhs.Tok, "nondeterministic assignment forbidden by the --enforce-determinism option", wr);
-                  }
-                } else {
+                if (rhs is not HavocRhs) {
                   var lhs = assignStmt.Lhs;
                   rhss.Add(rhs);
                   lhss.Add(lhs);
@@ -129,9 +125,6 @@ protected void TrStmt(Statement stmt, ConcreteSyntaxTree wr, ConcreteSyntaxTree
             var s = assignStmt;
             Contract.Assert(s.Lhs is not SeqSelectExpr expr || expr.SelectOne);  // multi-element array assignments are not allowed
             if (s.Rhs is HavocRhs) {
-              if (Options.ForbidNondeterminism) {
-                Error(ErrorId.c_nondeterminism_forbidden, s.Rhs.Tok, "nondeterministic assignment forbidden by the --enforce-determinism option", wr);
-              }
             } else if (s.Rhs is TypeRhs typeRhs) {
               var lvalue = CreateLvalue(s.Lhs, wr, wStmts);
               wStmts = wr.Fork();
@@ -157,9 +150,6 @@ protected void TrStmt(Statement stmt, ConcreteSyntaxTree wr, ConcreteSyntaxTree
           }
         case AssignSuchThatStmt thatStmt: {
             var s = thatStmt;
-            if (Options.ForbidNondeterminism) {
-              Error(ErrorId.c_assign_such_that_forbidden, s.Tok, "assign-such-that statement forbidden by the --enforce-determinism option", wr);
-            }
             var lhss = s.Lhss.ConvertAll(lhs => ((IdentifierExpr)lhs.Resolved).Var);  // the resolver allows only IdentifierExpr left-hand sides
             var missingBounds = BoundedPool.MissingBounds(lhss, s.Bounds, BoundedPool.PoolVirtues.Enumerable);
             if (missingBounds.Count != 0) {
@@ -216,9 +206,6 @@ protected void TrStmt(Statement stmt, ConcreteSyntaxTree wr, ConcreteSyntaxTree
         case IfStmt ifStmt: {
             IfStmt s = ifStmt;
             if (s.Guard == null) {
-              if (Options.ForbidNondeterminism) {
-                Error(ErrorId.c_nondeterministic_if_forbidden, s.Tok, "nondeterministic if statement forbidden by the --enforce-determinism option", wr);
-              }
               // we can compile the branch of our choice
               ConcreteSyntaxTree guardWriter;
               if (s.Els == null) {
@@ -241,10 +228,6 @@ protected void TrStmt(Statement stmt, ConcreteSyntaxTree wr, ConcreteSyntaxTree
                 Coverage.UnusedInstrumentationPoint(s.Els.Tok, "else branch");
               }
             } else {
-              if (s.IsBindingGuard && Options.ForbidNondeterminism) {
-                Error(ErrorId.c_binding_if_forbidden, s.Tok, "binding if statement forbidden by the --enforce-determinism option", wr);
-              }
-
               var coverageForElse = Coverage.IsRecording && !(s.Els is IfStmt);
               var thenWriter = EmitIf(out var guardWriter, s.Els != null || coverageForElse, wr);
               EmitExpr(s.IsBindingGuard ? ((ExistsExpr)s.Guard).AlphaRename("eg_d") : s.Guard, false, guardWriter, wStmts);
@@ -272,9 +255,6 @@ protected void TrStmt(Statement stmt, ConcreteSyntaxTree wr, ConcreteSyntaxTree
           }
         case AlternativeStmt alternativeStmt: {
             var s = alternativeStmt;
-            if (Options.ForbidNondeterminism && 2 <= s.Alternatives.Count) {
-              Error(ErrorId.c_case_based_if_forbidden, s.Tok, "case-based if statement forbidden by the --enforce-determinism option", wr);
-            }
             foreach (var alternative in s.Alternatives) {
               var thn = EmitIf(out var guardWriter, true, wr);
               EmitExpr(alternative.IsBindingGuard ? ((ExistsExpr)alternative.Guard).AlphaRename("eg_d") : alternative.Guard, false, guardWriter, wStmts);
@@ -294,9 +274,6 @@ protected void TrStmt(Statement stmt, ConcreteSyntaxTree wr, ConcreteSyntaxTree
               return;
             }
             if (s.Guard == null) {
-              if (Options.ForbidNondeterminism) {
-                Error(ErrorId.c_non_deterministic_loop_forbidden, s.Tok, "nondeterministic loop forbidden by the --enforce-determinism option", wr);
-              }
               // This loop is allowed to stop iterating at any time. We choose to never iterate, but we still
               // emit a loop structure. The structure "while (false) { }" comes to mind, but that results in
               // an "unreachable code" error from Java, so we instead use "while (true) { break; }".
@@ -312,9 +289,6 @@ protected void TrStmt(Statement stmt, ConcreteSyntaxTree wr, ConcreteSyntaxTree
             break;
           }
         case AlternativeLoopStmt loopStmt: {
-            if (Options.ForbidNondeterminism) {
-              Error(ErrorId.c_case_based_loop_forbidden, loopStmt.Tok, "case-based loop forbidden by the --enforce-determinism option", wr);
-            }
             if (loopStmt.Alternatives.Count != 0) {
               var w = CreateWhileLoop(out var whileGuardWriter, wr);
               EmitExpr(Expression.CreateBoolLiteral(loopStmt.tok, true), false, whileGuardWriter, wStmts);
@@ -361,9 +335,6 @@ protected void TrStmt(Statement stmt, ConcreteSyntaxTree wr, ConcreteSyntaxTree
             }
             var s0 = (AssignStmt)s.S0;
             if (s0.Rhs is HavocRhs) {
-              if (Options.ForbidNondeterminism) {
-                Error(ErrorId.c_nondeterminism_forbidden, s0.Rhs.Tok, "nondeterministic assignment forbidden by --enforce-determinism", wr);
-              }
               // The forall statement says to havoc a bunch of things.  This can be efficiently compiled
               // into doing nothing.
               return;
@@ -527,8 +498,6 @@ protected void TrStmt(Statement stmt, ConcreteSyntaxTree wr, ConcreteSyntaxTree
             var s = modifyStmt;
             if (s.Body != null) {
               TrStmt(s.Body, wr);
-            } else if (Options.ForbidNondeterminism) {
-              Error(ErrorId.c_bodyless_modify_statement_forbidden, s.Tok, "modify statement without a body forbidden by the --enforce-determinism option", wr);
             }
 
             break;

Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs

@@ -1611,11 +1611,6 @@ private void EmitModule(Program program, ConcreteSyntaxTree programNode, ModuleD
           }
         } else if (d is IteratorDecl) {
           var iter = (IteratorDecl)d;
-          if (Options.ForbidNondeterminism && iter.Outs.Count > 0) {
-            Error(ErrorId.c_iterators_are_not_deterministic, iter.tok,
-              "since yield parameters are initialized arbitrarily, iterators are forbidden by the --enforce-determinism option",
-              wr);
-          }
 
           var wIter = CreateIterator(iter, wr);
           if (iter.Body == null) {
@@ -1669,15 +1664,6 @@ private void EmitModule(Program program, ConcreteSyntaxTree programNode, ModuleD
             }
           }
 
-          if (Options.ForbidNondeterminism &&
-              !classIsExtern &&
-              !cl.Members.Exists(member => member is Constructor) &&
-              cl.Members.Exists(member => member is Field && !(member is ConstantField { Rhs: not null }))) {
-            Error(ErrorId.c_constructorless_class_forbidden, cl.tok,
-              "since fields are initialized arbitrarily, constructor-less classes are forbidden by the --enforce-determinism option",
-              wr);
-          }
-
           if (include) {
             var cw = CreateClass(IdProtect(d.EnclosingModuleDefinition.GetCompileName(Options)), IdName(cl),
               classIsExtern, cl.FullName,

Source/DafnyCore/DafnyOptions.cs

@@ -353,7 +353,8 @@ public enum ContractTestingMode {
     public bool WarnShadowing = false;
     public FunctionSyntaxOptions FunctionSyntax = FunctionSyntaxOptions.Version4;
     public QuantifierSyntaxOptions QuantifierSyntax = QuantifierSyntaxOptions.Version4;
-    public int DefiniteAssignmentLevel = 1; // [0..5] 2 and 3 have the same effect, 4 turns off an array initialisation check and field initialization check, unless --enforce-determinism is used.
+
+    public int DefiniteAssignmentLevel { get; set; } = 1;
     public HashSet<string> LibraryFiles { get; set; } = new();
     public ContractTestingMode TestContracts = ContractTestingMode.None;
 

Source/DafnyCore/Options/CommonOptionBag.cs

@@ -537,7 +537,9 @@ void ParsePrintMode(Option<PrintModes> option, Boogie.CommandLineParseState ps,
 
     DafnyOptions.RegisterLegacyBinding(EnforceDeterminism, (options, value) => {
       options.ForbidNondeterminism = value;
-      options.DefiniteAssignmentLevel = 4;
+      if (!options.Get(RelaxDefiniteAssignment)) {
+        options.DefiniteAssignmentLevel = 4;
+      }
     });
     RelaxDefiniteAssignment.AddValidator(optionResult => {
       var enforceDeterminismResult = optionResult.FindResultFor(EnforceDeterminism);

Source/DafnyCore/Options/DafnyCommands.cs

@@ -51,7 +51,6 @@ static DafnyCommands() {
   public static readonly IReadOnlyList<Option> TranslationOptions = new Option[] {
     BoogieOptionBag.NoVerify,
     BoogieOptionBag.HiddenNoVerify,
-    CommonOptionBag.EnforceDeterminism,
     CommonOptionBag.OptimizeErasableDatatypeWrapper,
     CommonOptionBag.TestAssumptions,
     DeveloperOptionBag.Bootstrapping,
@@ -110,6 +109,7 @@ static DafnyCommands() {
     CommonOptionBag.WarnMissingConstructorParenthesis,
     PrintStmt.TrackPrintEffectsOption,
     CommonOptionBag.AllowAxioms,
+    CommonOptionBag.EnforceDeterminism,
     MethodOrFunction.AllowExternalContracts,
     DafnyProject.FindProjectOption
   }).Concat(ParserOptions).ToList();

Source/DafnyCore/Resolver/ModuleResolver.cs

@@ -1478,6 +1478,22 @@ public void ResolveTopLevelDecls_Core(List<TopLevelDecl> declarations,
       // Further checks
       // ----------------------------------------------------------------------------
 
+      foreach (TopLevelDecl d in declarations) {
+        if (d is ClassLikeDecl classLikeDecl) {
+          var classIsExtern = !Options.DisallowExterns && Attributes.Contains(classLikeDecl.Attributes, "extern");
+          if (Options.ForbidNondeterminism &&
+              !classIsExtern &&
+              !classLikeDecl.Members.Exists(member => member is Constructor) &&
+              classLikeDecl.Members.Exists(member => member is Field && !(member is ConstantField { Rhs: not null }))) {
+            // This check should be moved to the resolver once we have a language construct to indicate the type is imported
+            // Instead of the extern attribute
+            Reporter.Error(MessageSource.Resolver, GeneratorErrors.ErrorId.c_constructorless_class_forbidden,
+              classLikeDecl.tok,
+              "since fields are initialized arbitrarily, constructor-less classes are forbidden by the --enforce-determinism option");
+          }
+        }
+      }
+
       if (reporter.Count(ErrorLevel.Error) == prevErrorCount) {
         // Check that type-parameter variance is respected in type definitions
         foreach (TopLevelDecl d in declarations) {
@@ -2966,7 +2982,7 @@ public void ScopePushAndReport(Scope<IVariable> scope, IVariable v, string kind)
       ScopePushAndReport(scope, v.Name, v, v.Tok, kind);
     }
 
-    void ScopePushAndReport<Thing>(Scope<Thing> scope, string name, Thing thing, IToken tok, string kind) where Thing : class {
+    public Scope<Thing>.PushResult ScopePushAndReport<Thing>(Scope<Thing> scope, string name, Thing thing, IToken tok, string kind) where Thing : class {
       Contract.Requires(scope != null);
       Contract.Requires(name != null);
       Contract.Requires(thing != null);
@@ -2983,6 +2999,8 @@ void ScopePushAndReport<Thing>(Scope<Thing> scope, string name, Thing thing, ITo
           reporter.Warning(MessageSource.Resolver, ResolutionErrors.ErrorId.none, tok, "Shadowed {0} name: {1}", kind, name);
           break;
       }
+
+      return r;
     }
 
     /// <summary>