Removed specContextOnly parameter from ResolveStatement.

Moved all bounds discovery to resolution pass 1.

7 files changed, 94 insertions, 41 deletions

diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index 49e6efa0..e935c83d 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -586,16 +586,16 @@ method LetSuchThat(ghost z: int, n: nat)
 module NonInferredType {

   predicate P<T>(x: T)

 

-  method NonInferredType0(x: int)

+  method InferredType(x: int)

   {

     var t;

-    assume forall z :: P(z) && z == t;  // It would be nice to allow the following example, but the implementation calls DiscoverBounds before CheckInference for quantifiers.

+    assume forall z :: P(z) && z == t;

     assume t == x;  // this statement determines the type of t and z

   }

 

-  method NonInferredType1(x: int)

+  method NonInferredType(x: int)

   {

-    var t;

+    var t;  // error: the type of t is not determined

     assume forall z :: P(z) && z == t;  // error: the type of z is not determined

   }

 }

@@ -1126,15 +1126,15 @@ method TraitSynonym()
 // ----- set comprehensions where the term type is finite -----

 

 module ObjectSetComprehensions {

-  // allowed in non-ghost context:

-  function A() : set<object> { set o : object | true :: o }

+  // the following set comprehensions are known to be finite

+  function A() : set<object> { set o : object | true :: o }  // error: a function is not allowed to depend on the allocated state

 

-  lemma B() { var x := set o : object | true :: o; }

+  function method B() : set<object> { set o : object | true :: o }  // error: a function is not allowed to depend on the allocated state

 

-  // not allowed in non-ghost context:

-  function method C() : set<object> { set o : object | true :: o }

+  // outside functions, the comprehension is permitted, but it cannot be compiled

+  lemma C() { var x := set o : object | true :: o; }

 

-  method D() { var x := set o : object | true :: o; }

+  method D() { var x := set o : object | true :: o; }  // error: not (easily) compilable

 }

 

 // ------ regression test for type checking of integer division -----

@@ -1228,9 +1228,9 @@ module NonInferredTypeVariables {
   method BadClient(n: nat)

   {

     var p := P(n);  // error: cannot infer the type argument for P

-    ghost var q := Q(n);  // error: cannot infer the type argument for Q

+    ghost var q := Q(n);  // error: cannot infer the type argument for Q (and thus q's type cannot be determined either)

     M(n);  // error: cannot infer the type argument for M

-    var x := N(n);  // error: cannot infer the type argument for N

+    var x := N(n);  // error: cannot infer the type argument for N (and thus x's type cannot be determined either)

     var a := new array;  // error: cannot infer the type argument for 'array'

     var c := new C;  // error: cannot infer the type argument for 'C'

     var s: set;  // type argument for 'set' 

@@ -1248,7 +1248,7 @@ module NonInferredTypeVariables {
     ghost var d0 := forall s :: s == {7} ==> s != {};

     var d1 := forall s: set :: s in S ==> s == {};

     var ggcc0: C;

-    var ggcc1: C;

+    var ggcc1: C;  // error: full type cannot be determined

     ghost var d2 := forall c: C :: c != null ==> c.f == 10;

     ghost var d2' := forall c :: c == ggcc0 && c != null ==> c.f == 10;

     ghost var d2'' := forall c :: c == ggcc1 && c != null ==> c.f == c.f; // error: here, type of c is not determined

diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect
index edf61b33..be19eeac 100644
--- a/Test/dafny0/ResolutionErrors.dfy.expect
+++ b/Test/dafny0/ResolutionErrors.dfy.expect
@@ -20,10 +20,9 @@ ResolutionErrors.dfy(535,7): Error: RHS (of type List<A>) not assignable to LHS
 ResolutionErrors.dfy(540,7): Error: RHS (of type List<A>) not assignable to LHS (of type List<B>)

 ResolutionErrors.dfy(554,23): Error: type of case bodies do not agree (found Tree<_T1,_T0>, previous types Tree<_T0,_T1>)

 ResolutionErrors.dfy(566,24): Error: Wrong number of type arguments (0 instead of 2) passed to datatype: Tree

-ResolutionErrors.dfy(592,25): Error: the type of this variable is underspecified

-ResolutionErrors.dfy(592,23): Error: type variable 'T' in the function call to 'P' could not be determined

-ResolutionErrors.dfy(599,25): Error: the type of this variable is underspecified

+ResolutionErrors.dfy(598,8): Error: the type of this local variable is underspecified

 ResolutionErrors.dfy(599,23): Error: type variable 'T' in the function call to 'P' could not be determined

+ResolutionErrors.dfy(599,18): Error: type of bound variable 'z' could not be determined; please specify the type explicitly

 ResolutionErrors.dfy(612,13): Error: 'new' is not allowed in ghost contexts

 ResolutionErrors.dfy(613,9): Error: 'new' is not allowed in ghost contexts

 ResolutionErrors.dfy(622,23): Error: 'new' is not allowed in ghost contexts

@@ -81,12 +80,28 @@ ResolutionErrors.dfy(1105,6): Error: RHS (of type P<int>) not assignable to LHS
 ResolutionErrors.dfy(1110,13): Error: arguments must have the same type (got P<int> and P<X>)

 ResolutionErrors.dfy(1111,13): Error: arguments must have the same type (got P<bool> and P<X>)

 ResolutionErrors.dfy(1112,13): Error: arguments must have the same type (got P<int> and P<bool>)

-ResolutionErrors.dfy(1135,38): Error: set comprehensions in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'o'

+ResolutionErrors.dfy(1130,31): Error: a set comprehension 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 'o'

+ResolutionErrors.dfy(1132,38): Error: a set comprehension 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 'o'

 ResolutionErrors.dfy(1137,24): Error: set comprehensions in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'o'

+ResolutionErrors.dfy(1230,13): Error: type variable 'PT' in the function call to 'P' could not be determined

+ResolutionErrors.dfy(1231,14): Error: the type of this variable is underspecified

+ResolutionErrors.dfy(1231,19): Error: type variable 'QT' in the function call to 'Q' could not be determined

+ResolutionErrors.dfy(1232,4): Error: type '?' to the method 'M' is not determined

+ResolutionErrors.dfy(1233,8): Error: the type of this variable is underspecified

+ResolutionErrors.dfy(1233,13): Error: type '?' to the method 'N' is not determined

+ResolutionErrors.dfy(1234,8): Error: the type of this variable is underspecified

+ResolutionErrors.dfy(1235,8): Error: the type of this variable is underspecified

+ResolutionErrors.dfy(1236,8): Error: the type of this local variable is underspecified

+ResolutionErrors.dfy(1237,8): Error: the type of this variable is underspecified

+ResolutionErrors.dfy(1238,8): Error: the type of this local variable is underspecified

 ResolutionErrors.dfy(1242,26): Error: the type of this variable is underspecified

+ResolutionErrors.dfy(1242,21): Error: type of bound variable 's' could not be determined; please specify the type explicitly

 ResolutionErrors.dfy(1243,31): Error: the type of this variable is underspecified

+ResolutionErrors.dfy(1243,21): Error: type of bound variable 's' could not be determined; please specify the type explicitly

 ResolutionErrors.dfy(1244,29): Error: the type of this variable is underspecified

-ResolutionErrors.dfy(1254,34): Error: the type of this variable is underspecified

+ResolutionErrors.dfy(1244,21): Error: type of bound variable 'c' could not be determined; please specify the type explicitly

+ResolutionErrors.dfy(1251,8): Error: the type of this local variable is underspecified

+ResolutionErrors.dfy(1254,29): Error: type of bound variable 'c' could not be determined; please specify the type explicitly

 ResolutionErrors.dfy(1270,21): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name or declare a module import 'opened?')

 ResolutionErrors.dfy(1271,24): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name or declare a module import 'opened?')

 ResolutionErrors.dfy(1308,16): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (y)

@@ -209,4 +224,4 @@ ResolutionErrors.dfy(1123,8): Error: new cannot be applied to a trait
 ResolutionErrors.dfy(1144,13): Error: first argument to / must be of numeric type (instead got set<bool>)

 ResolutionErrors.dfy(1151,18): Error: a call to a possibly non-terminating method is allowed only if the calling method is also declared (with 'decreases *') to be possibly non-terminating

 ResolutionErrors.dfy(1166,14): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating

-211 resolution/type errors detected in ResolutionErrors.dfy

+226 resolution/type errors detected in ResolutionErrors.dfy

diff --git a/Test/dafny4/Regression0.dfy b/Test/dafny4/Regression0.dfy
index be092261..666d9575 100644
--- a/Test/dafny4/Regression0.dfy
+++ b/Test/dafny4/Regression0.dfy
@@ -4,10 +4,10 @@
 // This once crashed Dafny

 

 method M() {

-  var s := [1, "2"];

+  var s := [1, "2"];  // error: all elements must have the same type

   if * {

-    assert exists n :: n in s && n != 1;

+    assert exists n :: n in s && n != 1;  // the type of n is inferred to be int

   } else {

-    assert "2" in s;

+    assert "2" in s;  // error: since the type of s wasn't determined

   }

 }

diff --git a/Test/dafny4/Regression0.dfy.expect b/Test/dafny4/Regression0.dfy.expect
index 9d1e3019..566b3e3f 100644
--- a/Test/dafny4/Regression0.dfy.expect
+++ b/Test/dafny4/Regression0.dfy.expect
@@ -1,4 +1,3 @@
 Regression0.dfy(7,15): Error: All elements of display must be of the same type (got string, but type of previous elements is int)

-Regression0.dfy(9,28): Error: the type of this variable is underspecified

 Regression0.dfy(11,15): Error: second argument to "in" must be a set, multiset, or sequence with elements of type string, or a map with domain string (instead got ?)

-3 resolution/type errors detected in Regression0.dfy

+2 resolution/type errors detected in Regression0.dfy

diff --git a/Test/dafny4/set-compr.dfy b/Test/dafny4/set-compr.dfy
index 71a07f3d..d093a924 100644
--- a/Test/dafny4/set-compr.dfy
+++ b/Test/dafny4/set-compr.dfy
@@ -22,7 +22,7 @@ method O() returns (ghost p: set<object>)
 

 method P() returns (p: set<object>)

 {

-  p := set o: object | true;  // not allowed -- not in a ghost context

+  p := set o: object | true;  // error: not (easily) compilable

 }

 

 ghost method Q() returns (p: set<object>)

@@ -30,26 +30,54 @@ ghost method Q() returns (p: set<object>)
   p := set o: object | true;  // allowed, since the whole method is ghost

 }

 

-function F(): int

+function F(p: object): int

+  requires p in set o: object | true  // error: function is not allowed to depend on allocation state

+  ensures p in set o: object | true  // error: ditto (although one could argue that this would be okay)

+  reads set o: object | true  // error: same as for 'requires'

+  decreases set o: object | true  // error: same as for 'ensures'

+{

+  if p in set o: object | true then  // error: function is not allowed to depend on allocation state

+    F(p)

+  else

+    0

+}

+

+function method G(p: object): int

+  requires p in set o: object | true  // error (see F)

+  ensures p in set o: object | true  // error (see F)

+  reads set o: object | true  // error (see F)

+  decreases set o: object | true  // error (see F)

+{

+  if p in set o: object | true then  // error (see F)

+    G(p)

+  else

+    0

+}

+

+method M0() returns (ghost r: int, s: int)

   requires null in set o: object | true  // allowed

   ensures null in set o: object | true  // allowed

-  reads set o: object | true  // allowed

+  modifies set o: object | true  // allowed

   decreases set o: object | true  // allowed

 {

-  if null in set o: object | true then  // allowed -- in a ghost context

-    F()

-  else

-    0

+  if null in set o: object | true {  // this makes the "if" a ghost

+    r := G(null);

+    s := G(null);  // error: assignment of non-ghost not allowed inside ghost "if"

+  } else {

+    r := 0;

+  }

 }

 

-function method G(): int

+method M1() returns (ghost r: int, s: int)

   requires null in set o: object | true  // (X) allowed

   ensures null in set o: object | true  // (X) allowed

-  reads set o: object | true  // allowed

+  modifies set o: object | true  // allowed

   decreases set o: object | true  // (X) allowed

 {

-  if null in set o: object | true then  // not allowed, since this is not a ghost context

-    G()

-  else

-    0

+  if null in set o: object | true {  // this makes the "if" a ghost

+    r := G(null);

+    s := G(null);  // error: assignment of non-ghost not allowed inside ghost "if"

+  } else {

+    r := 0;

+  }

 }

diff --git a/Test/dafny4/set-compr.dfy.expect b/Test/dafny4/set-compr.dfy.expect
index 615ee2bc..b0490a11 100644
--- a/Test/dafny4/set-compr.dfy.expect
+++ b/Test/dafny4/set-compr.dfy.expect
@@ -1,3 +1,14 @@
 set-compr.dfy(25,7): Error: set comprehensions in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'o'

-set-compr.dfy(51,13): Error: set comprehensions in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'o'

-2 resolution/type errors detected in set-compr.dfy

+set-compr.dfy(34,16): Error: a set comprehension 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 'o'

+set-compr.dfy(35,15): Error: a set comprehension 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 'o'

+set-compr.dfy(36,8): Error: a set comprehension 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 'o'

+set-compr.dfy(37,12): Error: a set comprehension 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 'o'

+set-compr.dfy(39,10): Error: a set comprehension 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 'o'

+set-compr.dfy(46,16): Error: a set comprehension 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 'o'

+set-compr.dfy(47,15): Error: a set comprehension 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 'o'

+set-compr.dfy(48,8): Error: a set comprehension 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 'o'

+set-compr.dfy(49,12): Error: a set comprehension 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 'o'

+set-compr.dfy(51,10): Error: a set comprehension 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 'o'

+set-compr.dfy(65,6): 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)

+set-compr.dfy(79,6): 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)

+13 resolution/type errors detected in set-compr.dfy

diff --git a/Test/hofs/ReadsReads.dfy b/Test/hofs/ReadsReads.dfy
index a6f8d922..60ac35f5 100644
--- a/Test/hofs/ReadsReads.dfy
+++ b/Test/hofs/ReadsReads.dfy
@@ -105,14 +105,14 @@ module WhatWeKnowAboutReads {
 
 module ReadsAll {
   function A(f: int -> int) : int
-    reads set o,x | o in f.reads(x) :: o
+    reads set x,o | o in f.reads(x) :: o  // note, with "set o,x ..." instead, Dafny complains (this is perhaps less than ideal)
     requires forall x :: f.requires(x)
   {
     f(0) + f(1) + f(2)
   }
 
   function method B(f: int -> int) : int
-    reads set o,x | o in f.reads(x) :: o
+    reads set x,o | o in f.reads(x) :: o  // note, with "set o,x ..." instead, Dafny complains (this is perhaps less than ideal)
     requires forall x :: f.requires(x)
   {
     f(0) + f(1) + f(2)