Dafny: fixed unsoundness having to do with a function depending on the allocation state

3 files changed, 77 insertions, 3 deletions

diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs
index 233f5415..daeef80c 100644
--- a/Dafny/Resolver.cs
+++ b/Dafny/Resolver.cs
@@ -2934,7 +2934,21 @@ namespace Microsoft.Dafny {
           var missingBounds = new List<BoundVar>();

           e.Bounds = DiscoverBounds(e.tok, e.BoundVars, e.LogicalBody(), e is ExistsExpr, missingBounds);

           if (missingBounds.Count != 0) {

-            e.MissingBounds = missingBounds;

+            // Report errors here about quantifications that depend on the allocation state.

+            var mb = missingBounds;

+            if (currentFunction != null) {

+              mb = new List<BoundVar>();  // (who cares if we allocate another array; this happens only in the case of a resolution error anyhow)

+              foreach (var bv in missingBounds) {

+                if (bv.Type.IsRefType) {

+                  Error(expr, "a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of '{0}'", bv.Name);

+                } else {

+                  mb.Add(bv);

+                }

+              }

+            }

+            if (mb.Count != 0) {

+              e.MissingBounds = mb;

+            }

           }

         }

 

@@ -3501,7 +3515,7 @@ namespace Microsoft.Dafny {
           // easy

           bounds.Add(new QuantifierExpr.BoolBoundedPool());

         } else {

-          // Go through the conjuncts of the range expression look for bounds.

+          // Go through the conjuncts of the range expression to look for bounds.

           Expression lowerBound = bv.Type is NatType ? new LiteralExpr(bv.tok, new BigInteger(0)) : null;

           Expression upperBound = null;

           foreach (var conjunct in NormalizedConjuncts(expr, polarity)) {

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 762bdea8..384adab5 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -670,6 +670,15 @@ Execution trace:
 Dafny program verifier finished with 8 verified, 2 errors

 

 -------------------- NonGhostQuantifiers.dfy --------------------

+NonGhostQuantifiers.dfy(146,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'

+NonGhostQuantifiers.dfy(150,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'

+NonGhostQuantifiers.dfy(155,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'

+NonGhostQuantifiers.dfy(160,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'

+NonGhostQuantifiers.dfy(164,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'

+NonGhostQuantifiers.dfy(168,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'

+NonGhostQuantifiers.dfy(173,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'

+NonGhostQuantifiers.dfy(178,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'

+NonGhostQuantifiers.dfy(183,13): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'c'

 NonGhostQuantifiers.dfy(13,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'n'

 NonGhostQuantifiers.dfy(42,4): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'n'

 NonGhostQuantifiers.dfy(46,4): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'd'

@@ -681,7 +690,7 @@ NonGhostQuantifiers.dfy(103,5): Error: quantifiers in non-ghost contexts must be
 NonGhostQuantifiers.dfy(111,10): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'y'

 NonGhostQuantifiers.dfy(120,8): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'x'

 NonGhostQuantifiers.dfy(137,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)

-11 resolution/type errors detected in NonGhostQuantifiers.dfy

+20 resolution/type errors detected in NonGhostQuantifiers.dfy

 

 -------------------- AdvancedLHS.dfy --------------------

 AdvancedLHS.dfy(32,23): Error: target object may be null

diff --git a/Test/dafny0/NonGhostQuantifiers.dfy b/Test/dafny0/NonGhostQuantifiers.dfy
index 58e64827..dc938496 100644
--- a/Test/dafny0/NonGhostQuantifiers.dfy
+++ b/Test/dafny0/NonGhostQuantifiers.dfy
@@ -138,3 +138,54 @@ class MyClass<T> {
     }

   }

 }

+

+// The following functions test what was once a soundness problem

+module DependencyOnAllAllocatedObjects {

+  function AllObjects0(): bool

+  {

+    forall c: SomeClass :: c != null ==> c.f == 0  // error: not allowed to dependend on which objects are allocated

+  }

+  function AllObjects1(): bool

+  {

+    forall c: SomeClass :: true  // error: not allowed to dependend on which objects are allocated

+  }

+  function AllObjects10(): bool

+    reads *;

+  {

+    forall c: SomeClass :: c != null ==> c.f == 0  // error: not allowed to dependend on which objects are allocated

+  }

+  function AllObjects11(): bool

+    reads *;

+  {

+    forall c: SomeClass :: true  // error: not allowed to dependend on which objects are allocated

+  }

+  function method AllObjects20(): bool

+  {

+    forall c: SomeClass :: c != null ==> c.f == 0  // error: not allowed to dependend on which objects are allocated

+  }

+  function method AllObjects21(): bool

+  {

+    forall c: SomeClass :: true  // error: not allowed to dependend on which objects are allocated

+  }

+  function method AllObjects30(): bool

+    reads *;

+  {

+    forall c: SomeClass :: c != null ==> c.f == 0  // error: not allowed to dependend on which objects are allocated

+  }

+  function method AllObjects31(): bool

+    reads *;

+  {

+    forall c: SomeClass :: true  // error: not allowed to dependend on which objects are allocated

+  }

+

+  method M()

+  {

+    var b := forall c: SomeClass :: c != null ==> c.f == 0;  // error: non-ghost code requires bounds

+    ghost var g := forall c: SomeClass :: c != null ==> c.f == 0;  // cool (this is in a ghost context

+                                                                   // outside a function)

+  }

+

+  class SomeClass {

+    var f: int;

+  }

+}