Dafny:

* added missing error checking for ghost-vs-physical contexts (e.g., use of the "old" keyword)
* check that arrays are not null when accessed
* added dafny1/FindZero.dfy test case

8 files changed, 72 insertions, 6 deletions

diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs
index 22a58a39..ba28d531 100644
--- a/Dafny/Resolver.cs
+++ b/Dafny/Resolver.cs
@@ -837,7 +837,11 @@ namespace Microsoft.Dafny {
       

 #if !NO_CHEAP_OBJECT_WORKAROUND

       if (a is ObjectType || b is ObjectType) {  // TODO: remove this temporary hack

-        // allow anything with object; this is BOGUS

+        var other = a is ObjectType ? b : a;

+        if (other is BoolType || other is IntType || other is SetType || other is SeqType || other.IsDatatype) {

+          return false;

+        }

+        // allow anything else with object; this is BOGUS

         return true;

       }

 #endif

@@ -2019,6 +2023,8 @@ namespace Microsoft.Dafny {
         OldExpr e = (OldExpr)expr;

         if (!twoState) {

           Error(expr, "old expressions are not allowed in this context");

+        } else if (!specContext) {

+          Error(expr, "old expressions are allowed only in specification and ghost contexts");

         }

         ResolveExpression(e.E, twoState, specContext);

         expr.Type = e.E.Type;

@@ -2027,6 +2033,8 @@ namespace Microsoft.Dafny {
         FreshExpr e = (FreshExpr)expr;

         if (!twoState) {

           Error(expr, "fresh expressions are not allowed in this context");

+        } else if (!specContext) {

+          Error(expr, "fresh expressions are allowed only in specification and ghost contexts");

         }

         ResolveExpression(e.E, twoState, specContext);

         // the type of e.E must be either an object or a collection of objects

@@ -2047,6 +2055,9 @@ namespace Microsoft.Dafny {
       } else if (expr is AllocatedExpr) {

         AllocatedExpr e = (AllocatedExpr)expr;

         ResolveExpression(e.E, twoState, specContext);

+        if (!specContext) {

+          Error(expr, "allocated expressions are allowed only in specification and ghost contexts");

+        }

         // e.E can be of any type

         expr.Type = Type.Bool;

 

diff --git a/Dafny/Translator.cs b/Dafny/Translator.cs
index 2bb5a51e..557fcaf0 100644
--- a/Dafny/Translator.cs
+++ b/Dafny/Translator.cs
@@ -1785,6 +1785,9 @@ namespace Microsoft.Dafny {
         bool isSequence = e.Seq.Type is SeqType;

         CheckWellformed(e.Seq, options, locals, builder, etran);

         Bpl.Expr seq = etran.TrExpr(e.Seq);

+        if (e.Seq.Type.IsArrayType) {

+          builder.Add(Assert(e.Seq.tok, Bpl.Expr.Neq(seq, predef.Null), "array may be null"));

+        }

         Bpl.Expr e0 = null;

         if (e.E0 != null) {

           e0 = etran.TrExpr(e.E0);

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 1ac8fc1c..afa88a47 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -483,9 +483,12 @@ Modules0.dfy(62,6): Error: inter-module calls must follow the module import rela
 Modules0.dfy(72,6): Error: inter-module calls must follow the module import relation (so module X0 must transitively import X1)

 Modules0.dfy(91,4): Error: inter-module calls must follow the module import relation (so module _default must transitively import YY)

 Modules0.dfy(116,16): Error: ghost variables are allowed only in specification contexts

-Modules0.dfy(133,10): Error: match source expression 'tree' has already been used as a match source expression in this context

-Modules0.dfy(172,12): Error: match source expression 'l' has already been used as a match source expression in this context

-10 resolution/type errors detected in Modules0.dfy

+Modules0.dfy(130,11): Error: old expressions are allowed only in specification and ghost contexts

+Modules0.dfy(131,11): Error: fresh expressions are allowed only in specification and ghost contexts

+Modules0.dfy(132,11): Error: allocated expressions are allowed only in specification and ghost contexts

+Modules0.dfy(148,10): Error: match source expression 'tree' has already been used as a match source expression in this context

+Modules0.dfy(187,12): Error: match source expression 'l' has already been used as a match source expression in this context

+13 resolution/type errors detected in Modules0.dfy

 

 -------------------- Modules1.dfy --------------------

 Modules1.dfy(55,3): Error: decreases expression must be bounded below by 0

diff --git a/Test/dafny0/Modules0.dfy b/Test/dafny0/Modules0.dfy
index adce71a8..59052ac2 100644
--- a/Test/dafny0/Modules0.dfy
+++ b/Test/dafny0/Modules0.dfy
@@ -121,6 +121,21 @@ class Ghosty {
   ghost method Theorem(a: int) { }

 }

 

+var SomeField: int;

+

+method SpecialFunctions()

+  modifies this;

+{

+  SomeField := SomeField + 4;

+  var a := old(SomeField);  // error: old can only be used in ghost contexts

+  var b := fresh(this);  // error: fresh can only be used in ghost contexts

+  var c := allocated(this);  // error: allocated can only be used in ghost contexts

+  if (fresh(this)) {  // this guard makes the if statement a ghost statement

+    ghost var x := old(SomeField);  // this is a ghost context, so it's okay

+    ghost var y := allocated(this);  // this is a ghost context, so it's okay

+  }

+}

+

 // ---------------------- illegal match expressions ---------------

 

 datatype Tree { Nil; Cons(int, Tree, Tree); }

diff --git a/Test/dafny0/NatTypes.dfy b/Test/dafny0/NatTypes.dfy
index 93bd4b65..6b7ce9b9 100644
--- a/Test/dafny0/NatTypes.dfy
+++ b/Test/dafny0/NatTypes.dfy
@@ -60,7 +60,7 @@ datatype List<T> {
   Cons(nat, T, List<T>);

 }

 

-method MatchIt(list: List<bool>) returns (k: nat)

+method MatchIt(list: List<object>) returns (k: nat)

 {

   match (list) {

     case Nil =>

diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer
index d96e12a5..d0eba7cb 100644
--- a/Test/dafny1/Answer
+++ b/Test/dafny1/Answer
@@ -59,6 +59,10 @@ Dafny program verifier finished with 2 verified, 0 errors
 

 Dafny program verifier finished with 17 verified, 0 errors

 

+-------------------- FindZero.dfy --------------------

+

+Dafny program verifier finished with 4 verified, 0 errors

+

 -------------------- TerminationDemos.dfy --------------------

 

 Dafny program verifier finished with 11 verified, 0 errors

diff --git a/Test/dafny1/FindZero.dfy b/Test/dafny1/FindZero.dfy
new file mode 100644
index 00000000..cff8b934
--- /dev/null
+++ b/Test/dafny1/FindZero.dfy
@@ -0,0 +1,30 @@
+method FindZero(a: array<int>) returns (r: int)

+  requires a != null && forall i :: 0 <= i && i < a.Length ==> 0 <= a[i];

+  requires forall i :: 0 <= i && i+1 < a.Length ==> a[i]-1 <= a[i+1];

+  ensures 0 <= r ==> r < a.Length && a[r] == 0;

+  ensures r < 0 ==> forall i :: 0 <= i && i < a.Length ==> a[i] != 0;

+{

+  var n := 0;

+  while (n < a.Length)

+    invariant forall i :: 0 <= i && i < n && i < a.Length ==> a[i] != 0;

+  {

+    if (a[n] == 0) { r := n; return; }

+    call Lemma(a, n, a[n]);

+    n := n + a[n];

+  }

+  r := -1;

+}

+

+ghost method Lemma(a: array<int>, k: int, m: int)

+  requires a != null && forall i :: 0 <= i && i < a.Length ==> 0 <= a[i];

+  requires forall i :: 0 <= i && i+1 < a.Length ==> a[i]-1 <= a[i+1];

+  requires 0 <= k;

+  requires k < a.Length ==> m <= a[k];

+  ensures forall i :: k <= i && i < k+m && i < a.Length ==> a[i] != 0;

+  decreases m;

+{

+  if (0 < m && k < a.Length) {

+    assert a[k] != 0;

+    call Lemma(a, k+1, m-1);

+  }

+}

diff --git a/Test/dafny1/runtest.bat b/Test/dafny1/runtest.bat
index b6fc7f62..cab18ddb 100644
--- a/Test/dafny1/runtest.bat
+++ b/Test/dafny1/runtest.bat
@@ -18,7 +18,7 @@ for %%f in (Queue.dfy PriorityQueue.dfy ExtensibleArray.dfy
             ListCopy.dfy ListReverse.dfy ListContents.dfy

             MatrixFun.dfy pow2.dfy

             SchorrWaite.dfy

-            Cubes.dfy SumOfCubes.dfy

+            Cubes.dfy SumOfCubes.dfy FindZero.dfy

             TerminationDemos.dfy Substitution.dfy TreeDatatype.dfy KatzManna.dfy

             Induction.dfy Rippling.dfy

             Celebrity.dfy