Fix default values

Source/DafnyCore/Verifier/Translator.ClassMembers.cs

@@ -673,33 +673,32 @@ private void AddMethodImpl(Method m, Boogie.Procedure proc, bool wellformednessP
         Contract.Assert(definiteAssignmentTrackers.Count == 0);
       } else {
         // check well-formedness of any default-value expressions (before assuming preconditions)
-        // TODO: modify WithDelayedReadsChecks so we can use it here too
-        var wfo = new WFOptions(null, true, true, true);
-        foreach (var formal in m.Ins.Where(formal => formal.DefaultValue != null)) {
-          var e = formal.DefaultValue;
-          CheckWellformed(e, wfo, localVariables, builder, etran);
-          builder.Add(new Boogie.AssumeCmd(e.tok, CanCallAssumption(e, etran)));
-          CheckSubrange(e.tok, etran.TrExpr(e), e.Type, formal.Type, builder);
-
-          if (formal.IsOld) {
-            Boogie.Expr wh = GetWhereClause(e.tok, etran.TrExpr(e), e.Type, etran.Old, ISALLOC, true);
-            if (wh != null) {
-              var desc = new PODesc.IsAllocated("default value", "in the two-state lemma's previous state");
-              builder.Add(Assert(e.tok, wh, desc));
+        WithDelayedReadsChecks(etran, localVariables, builderInitializationArea, builder, true, wfo => {
+          foreach (var formal in m.Ins.Where(formal => formal.DefaultValue != null)) {
+            var e = formal.DefaultValue;
+            CheckWellformed(e, wfo, localVariables, builder, etran);
+            builder.Add(new Boogie.AssumeCmd(e.tok, CanCallAssumption(e, etran)));
+            CheckSubrange(e.tok, etran.TrExpr(e), e.Type, formal.Type, builder);
+
+            if (formal.IsOld) {
+              Boogie.Expr wh = GetWhereClause(e.tok, etran.TrExpr(e), e.Type, etran.Old, ISALLOC, true);
+              if (wh != null) {
+                var desc = new PODesc.IsAllocated("default value", "in the two-state lemma's previous state");
+                builder.Add(Assert(e.tok, wh, desc));
+              }
             }
           }
-        }
-        wfo.ProcessSavedReadsChecks(localVariables, builderInitializationArea, builder);
+        });
 
         // check well-formedness of the preconditions, and then assume each one of them
-        WithDelayedReadsChecks(etran, localVariables, builderInitializationArea, builder, wfo => {
+        WithDelayedReadsChecks(etran, localVariables, builderInitializationArea, builder, false, wfo => {
           foreach (AttributedExpression p in m.Req) {
             CheckWellformedAndAssume(p.E, wfo, localVariables, builder, etran);
           }
         });
 
         // check well-formedness of the reads clauses
-        WithDelayedReadsChecks(etran, localVariables, builderInitializationArea, builder, wfo => {
+        WithDelayedReadsChecks(etran, localVariables, builderInitializationArea, builder, false, wfo => {
           CheckFrameWellFormed(wfo, m.Reads, localVariables, builder, etran);
           if (etran.readsFrame != null && Attributes.Contains(m.Attributes, "concurrent")) {
             var desc = new PODesc.ConcurrentFrameEmpty("reads clause");
@@ -708,7 +707,7 @@ private void AddMethodImpl(Method m, Boogie.Procedure proc, bool wellformednessP
         });
 
         // check well-formedness of the modifies clauses
-        WithDelayedReadsChecks(etran, localVariables, builderInitializationArea, builder, wfo => {
+        WithDelayedReadsChecks(etran, localVariables, builderInitializationArea, builder, false, wfo => {
           CheckFrameWellFormed(wfo, m.Mod.Expressions, localVariables, builder, etran);
           if (Attributes.Contains(m.Attributes, "concurrent")) {
             var desc = new PODesc.ConcurrentFrameEmpty("modifies clause");

Source/DafnyCore/Verifier/Translator.ExpressionWellformed.cs

@@ -224,11 +224,13 @@ void CheckWellformedAndAssume(Expression expr, WFOptions wfOptions, List<Variabl
       builder.Add(TrAssumeCmd(expr.tok, etran.TrExpr(expr)));
     }
 
-    void WithDelayedReadsChecks(ExpressionTranslator etran, List<Variable> localVariables,
+    void WithDelayedReadsChecks(ExpressionTranslator etran,
+      List<Variable> localVariables,
       BoogieStmtListBuilder builderInitializationArea, BoogieStmtListBuilder builder,
+      bool doOnlyCoarseGrainedTerminationChecks,
       Action<WFOptions> action) {
       var doReadsChecks = etran.readsFrame != null;
-      var options = new WFOptions(null, doReadsChecks, doReadsChecks);
+      var options = new WFOptions(null, doReadsChecks, doReadsChecks, doOnlyCoarseGrainedTerminationChecks);
       action(options);
       if (doReadsChecks) {
         options.ProcessSavedReadsChecks(localVariables, builderInitializationArea, builder);

Test/git-issues/github-issue-reads-on-methods.dfy

@@ -95,7 +95,6 @@ method BadMetaBox(b: Box<Box<int>>)
 }
 
 method GoodMetaBox(b: Box<Box<int>>)
-  // Crashing...
   modifies b.x
 {
   b.x.x := 42;
@@ -108,14 +107,14 @@ function Foo(b: Box<Box<int>>): int
 }
 
 trait T {
-  method M(b: Box<int>)
+  method M(b: Box<int>) returns (r: int)
 }
 
 class C extends T {
-  method M(b: Box<int>) 
-    modifies b
+  method M(b: Box<int>) returns (r: int) 
+    reads b // BUG
   {
-    b.x := 42;
+    return 42;
   }
 }
 
@@ -187,7 +186,6 @@ method DefaultValueReads(b: Box<int>, x: int := b.x)
 // * Explicitly test against ghost state too
 //   * ghost methods/lemmas as well
 // * {:concurrent} (probably separate test file)
-// * Review reads checks for AST elements missed because they don't occur in expressions
 // * Optimize checking for `reads {}`? Can be checked with a simple AST pass, much cheaper
 //   * At least some cases might be handled by existing IsAlwaysTrue
 // * Double-check if it's correct that function default values don't assume preconditions

Test/git-issues/github-issue-reads-on-methods.dfy.expect

@@ -1,4 +1,11 @@
-github-issue-reads-on-methods.dfy(36,9): Error: insufficient reads clause to read field
-github-issue-reads-on-methods.dfy(79,23): Error: insufficient reads clause to read field
+github-issue-reads-on-methods.dfy(38,9): Error: insufficient reads clause to read field
+github-issue-reads-on-methods.dfy(85,23): Error: insufficient reads clause to read field
+github-issue-reads-on-methods.dfy(92,13): Error: insufficient reads clause to read field
+github-issue-reads-on-methods.dfy(94,4): Error: insufficient reads clause to read field
+github-issue-reads-on-methods.dfy(167,13): Error: insufficient reads clause to read field
+github-issue-reads-on-methods.dfy(174,50): Error: insufficient reads clause to read field
+github-issue-reads-on-methods.dfy(127,25): Error: reads clause might not be empty ({:concurrent} restriction)
+github-issue-reads-on-methods.dfy(142,23): Error: reads clause might not be empty ({:concurrent} restriction)
+github-issue-reads-on-methods.dfy(153,23): Error: modifies clause might not be empty ({:concurrent} restriction)
 
-Dafny program verifier finished with 8 verified, 2 errors
+Dafny program verifier finished with 20 verified, 9 errors