Dafny: allow class names to be used when referring to static functions (and, soon, methods), and test cases for new name resolution rules

6 files changed, 171 insertions, 22 deletions

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index df49e8c7..f6d96bab 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -1850,6 +1850,25 @@ namespace Microsoft.Dafny {
     }

   }

 

+  /// <summary>

+  /// Instances of this class are introduced during resolution to indicate that a static method or function has

+  /// been invoked without specifying a receiver (that is, by just giving the name of the enclosing class).

+  /// </summary>

+  public class StaticReceiverExpr : LiteralExpr

+  {

+    public StaticReceiverExpr(IToken tok, ClassDecl cl)

+      : base(tok)  // constructs a LiteralExpr representing the 'null' literal

+    {

+      Contract.Requires(tok != null);

+      Contract.Requires(cl != null);

+      var typeArgs = new List<Type>();

+      foreach (var ta in cl.TypeArgs) {

+        typeArgs.Add(new InferredTypeProxy());

+      }

+      Type = new UserDefinedType(tok, cl.Name, cl, typeArgs);

+    }

+  }

+

   public class LiteralExpr : Expression {

     public readonly object Value;

 

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index b01ca509..d0b5ab60 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -1871,29 +1871,27 @@ namespace Microsoft.Dafny {
           r = ResolveSuffix(r, e, 1, twoState, specContext);

 

         } else if (classes.TryGetValue(id.val, out decl)) {

-          if (decl is ClassDecl) {

+          if (e.Tokens.Count == 1 && e.Arguments == null) {

+            Error(id, "name of type ('{0}') is used as a variable", id.val);

+          } else if (e.Tokens.Count == 1 && e.Arguments != null) {

+            Error(id, "name of type ('{0}') is used as a function", id.val);

+            // resolve the arguments nonetheless

+            foreach (var arg in e.Arguments) {

+              ResolveExpression(arg, twoState, specContext);

+            }

+          } else if (decl is ClassDecl) {

             // ----- root is a class

             var cd = (ClassDecl)decl;

-            Contract.Assert(false); // TODO

+            r = ResolveSuffix(new StaticReceiverExpr(id, cd), e, 1, twoState, specContext);

 

           } else {

             // ----- root is a datatype

             var dt = (DatatypeDecl)decl;  // otherwise, unexpected TopLevelDecl

-            if (e.Tokens.Count == 1 && e.Arguments == null) {

-              Error(id, "name of datatype ('{0}') is used as a variable", id.val);

-            } else if (e.Tokens.Count == 1 && e.Arguments != null) {

-              Error(id, "name of dataypte ('{0}') is used as a function", id.val);

-              // resolve the arguments nonetheless

-              foreach (var arg in e.Arguments) {

-                ResolveExpression(arg, twoState, specContext);

-              }

-            } else {

-              var args = (e.Tokens.Count == 2 ? e.Arguments : null) ?? new List<Expression>();

-              r = new DatatypeValue(id, id.val, e.Tokens[1].val, args);

-              ResolveExpression(r, twoState, specContext);

-              if (e.Tokens.Count != 2) {

-                r = ResolveSuffix(r, e, 2, twoState, specContext);

-              }

+            var args = (e.Tokens.Count == 2 ? e.Arguments : null) ?? new List<Expression>();

+            r = new DatatypeValue(id, id.val, e.Tokens[1].val, args);

+            ResolveExpression(r, twoState, specContext);

+            if (e.Tokens.Count != 2) {

+              r = ResolveSuffix(r, e, 2, twoState, specContext);

             }

           }

 

@@ -2035,6 +2033,9 @@ namespace Microsoft.Dafny {
         } else {

           Contract.Assert(ctype != null && ctype.ResolvedClass != null);  // follows from postcondition of ResolveMember

           e.Field = (Field)member;

+          if (e.Obj is StaticReceiverExpr) {

+            Error(expr, "a field must be selected via an object, not just a class name");

+          }

           // build the type substitution map

           Dictionary<TypeParameter,Type> subst = new Dictionary<TypeParameter,Type>();

           for (int i = 0; i < ctype.TypeArgs.Count; i++) {

@@ -2108,6 +2109,9 @@ namespace Microsoft.Dafny {
         } else {

           Function function = (Function)member;

           e.Function = function;

+          if (e.Receiver is StaticReceiverExpr && !function.IsStatic) {

+            Error(expr, "an instance function must be selected via an object, not just a class name");

+          }

           if (!specContext && function.IsGhost) {

             Error(expr, "function calls are allowed only in specification contexts (consider declaring the function a 'function method')");

           }

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index d9d3a572..289a597d 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -402,11 +402,25 @@ Execution trace:
 Dafny program verifier finished with 3 verified, 3 errors

 

 -------------------- ResolutionErrors.dfy --------------------

+ResolutionErrors.dfy(39,13): Error: 'this' is not allowed in a 'class' context

 ResolutionErrors.dfy(10,16): Error: 'decreases *' is not allowed on ghost loops

 ResolutionErrors.dfy(22,11): Error: array selection requires an array2 (got array3<T>)

 ResolutionErrors.dfy(23,12): Error: sequence/array selection requires a sequence or array (got array3<T>)

 ResolutionErrors.dfy(24,11): Error: array selection requires an array4 (got array<T>)

-4 resolution/type errors detected in ResolutionErrors.dfy

+ResolutionErrors.dfy(45,14): Error: a field must be selected via an object, not just a class name

+ResolutionErrors.dfy(46,7): Error: unresolved identifier: F

+ResolutionErrors.dfy(47,14): Error: an instance function must be selected via an object, not just a class name

+ResolutionErrors.dfy(48,7): Error: unresolved identifier: G

+ResolutionErrors.dfy(50,2): Error: member M does not exist in class _default

+ResolutionErrors.dfy(52,2): Error: member N does not exist in class _default

+ResolutionErrors.dfy(55,8): Error: non-function expression is called with parameters

+ResolutionErrors.dfy(56,14): Error: member z does not exist in class Global

+ResolutionErrors.dfy(75,12): Error: the name 'Benny' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.Benny')

+ResolutionErrors.dfy(80,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')

+ResolutionErrors.dfy(81,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')

+ResolutionErrors.dfy(83,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')

+ResolutionErrors.dfy(85,12): Error: wrong number of arguments to datatype constructor Abc (found 2, expected 1)

+18 resolution/type errors detected in ResolutionErrors.dfy

 

 -------------------- Array.dfy --------------------

 Array.dfy(10,12): Error: assignment may update an array element not in the enclosing method's modifies clause

@@ -540,6 +554,10 @@ Execution trace:
 

 Dafny program verifier finished with 6 verified, 1 error

 

+-------------------- Basics.dfy --------------------

+

+Dafny program verifier finished with 5 verified, 0 errors

+

 -------------------- ControlStructures.dfy --------------------

 ControlStructures.dfy(5,3): Error: missing case in case statement: Blue

 Execution trace:

diff --git a/Test/dafny0/Basics.dfy b/Test/dafny0/Basics.dfy
new file mode 100644
index 00000000..1eeb2d92
--- /dev/null
+++ b/Test/dafny0/Basics.dfy
@@ -0,0 +1,44 @@
+class Global {

+  static function G(x: int): int { x+x }

+  static method N(x: int) returns (ghost r: int)

+    ensures r == Global.G(x);

+  {

+    if {

+      case true =>  r := G(x+0);

+      case true =>

+        var g: Global;

+        r := g.G(x);

+      case true =>

+        var g: Global := null;

+        r := g.G(x);

+      case true =>

+        r := Global.G(x);

+    }

+  }

+}

+

+method TestCalls(k: nat) {

+  var g: Global, h: Global;

+  assume g != h;

+  ghost var r: int;

+  ghost var s := Global.G(k);

+

+//  call r := Global.N(k);

+//  assert r == s;

+

+  call r := g.N(k);

+  assert r == s;

+  call r := h.N(k);

+  assert r == s;

+

+  g := null;

+  call r := g.N(k);

+  assert r == s;

+

+//  call r := Global.N(r);

+  if (k == 0) {

+    assert r == s;

+  } else {

+//    assert r == s;  // error: G(k) and G(k+k) are different

+  }

+}

diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index 5ec0cc4c..b33d4d54 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -8,18 +8,82 @@ method GhostDivergentLoop()
    ghost var i := 0;

    while (i < 2)

       decreases *; // error: not allowed on a ghost loop

-	  invariant i <= 2;

-	  invariant (forall j :: 0 <= j && j < i ==> a[j] > 0);

+      invariant i <= 2;

+      invariant (forall j :: 0 <= j && j < i ==> a[j] > 0);

    {

      i := 0;

    }

    assert a[1] != a[1]; // ...for then this would incorrectly verify

 }

 

-method M<T>(a: array3<T>, b: array<T>, m: int, n: int)

+method ManyIndices<T>(a: array3<T>, b: array<T>, m: int, n: int)

 {

   // the following invalid expressions were once incorrectly resolved:

   var x := a[m, n];        // error

   var y := a[m];           // error

   var z := b[m, n, m, n];  // error

 }

+

+// -------- name resolution

+

+class Global {

+  var X: int;

+  function method F(x: int): int { x }

+  static function method G(x: int): int { x }

+  method M(x: int) returns (r: int)

+  {

+    r := x + X;

+  }

+  static method N(x: int) returns (r: int)

+  {

+    r := x + X;  // error: cannot access instance field X from static method

+  }

+}

+

+method TestNameResolution0() {

+  var z: int;

+  z := Global.X;  // error: X is an instance field

+  z := F(2);  // error: cannot resolve F

+  z := Global.F(2);  // error: invocation of instance function requires an instance

+  z := G(2);  // error: cannot resolve G

+  z := Global.G(2);

+  call z := M(2);  // error: cannot resolve M

+//  call z := Global.M(2);  // error: call to instance method requires an instance

+  call z := N(1);  // error: cannot resolve N

+//  call z := Global.N(1);

+

+  z := z(5);  // error: using local as if it were a function

+  z := Global.z;  // error: class Global does not have a member z

+

+  var Global: Global;  // a local variable with the name 'Global'

+  z := Global.X;  // this means the instance field X of the object stored in the local variable 'Global'

+  var gg: Global := null;

+  var y := gg.G(5);

+  call y := gg.N(5);

+}

+

+datatype Abc = Abel | Benny | Cecilia(y: int) | David(x: int) | Eleanor;

+datatype Xyz = Alberta | Benny | Constantine(y: int) | David(x: int);

+datatype Rst = David(x: int, y: int);

+

+function Tuv(arg0: Abc, arg1: bool): int { 10 }

+var Eleanor: bool;

+

+method TestNameResolution1() {

+  var a0 := Abel;

+  var a1 := Alberta;

+  var b0 := Benny;  // error: there's more than one constructor with the name Benny; needs qualification

+  var b1 := Abc.Benny;

+  var b2 := Xyz.Benny;

+  var Benny := 15;  // introduce a local variable with the name 'Benny'

+  var b3 := Benny;

+  var d0 := David(20);  // error: constructor name David is ambiguous

+  var d1 := David;  // error: constructor name David is ambiguous (never mind that the signature does

+                    // not match either of them)

+  var d2 := David(20, 40);  // error: constructor name Davis is ambiguous (never mind that the given

+                            // parameters match the signature of only one of those constructors)

+  var d3 := Abc.David(20, 40);  // error: wrong number of parameters

+  var d4 := Rst.David(20, 40);

+  var e := Eleanor;

+  assert Tuv(e, this.Eleanor) == 10;

+}

diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index 16bc0e2b..22221a15 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -15,7 +15,7 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy
             FunctionSpecifications.dfy ResolutionErrors.dfy

             Array.dfy MultiDimArray.dfy NonGhostQuantifiers.dfy AdvancedLHS.dfy

             Modules0.dfy Modules1.dfy BadFunction.dfy

-            Comprehensions.dfy ControlStructures.dfy

+            Comprehensions.dfy Basics.dfy ControlStructures.dfy

             Termination.dfy Use.dfy DTypes.dfy

             TypeParameters.dfy Datatypes.dfy TypeAntecedents.dfy SplitExpr.dfy

             Refinement.dfy RefinementErrors.dfy) do (