Add support for assumption variables.

7 files changed, 240 insertions, 60 deletions

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 7b88d0bb..77e49352 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -2221,6 +2221,7 @@ namespace Microsoft.Dafny {
     public BlockStmt Body;  // Body is readonly after construction, except for any kind of rewrite that may take place around the time of resolution

     public bool IsRecursive;  // filled in during resolution

     public bool IsTailRecursive;  // filled in during resolution

+    public readonly ISet<IVariable> AssignedAssumptionVariables = new HashSet<IVariable>();

 

     [ContractInvariantMethod]

     void ObjectInvariant() {

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index d2fc74aa..c842239c 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -2607,6 +2607,7 @@ namespace Microsoft.Dafny
     }

 

     ClassDecl currentClass;

+    Method currentMethod;

     readonly Scope<TypeParameter>/*!*/ allTypeParameters = new Scope<TypeParameter>();

     readonly Scope<IVariable>/*!*/ scope = new Scope<IVariable>();

     Scope<Statement>/*!*/ labeledStatements = new Scope<Statement>();

@@ -3133,77 +3134,86 @@ namespace Microsoft.Dafny
     void ResolveMethod(Method m) {

       Contract.Requires(m != null);

 

-      // Add in-parameters to the scope, but don't care about any duplication errors, since they have already been reported

-      scope.PushMarker();

-      if (m.IsStatic) {

-        scope.AllowInstance = false;

-      }

-      foreach (Formal p in m.Ins) {

-        scope.Push(p.Name, p);

-      }

+      try

+      {

+        currentMethod = m;

 

-      // Start resolving specification...

-      foreach (MaybeFreeExpression e in m.Req) {

-        ResolveExpression(e.E, false, m);

-        Contract.Assert(e.E.Type != null);  // follows from postcondition of ResolveExpression

-        if (!UnifyTypes(e.E.Type, Type.Bool)) {

-          Error(e.E, "Precondition must be a boolean (got {0})", e.E.Type);

+        // Add in-parameters to the scope, but don't care about any duplication errors, since they have already been reported

+        scope.PushMarker();

+        if (m.IsStatic) {

+          scope.AllowInstance = false;

         }

-      }

-      foreach (FrameExpression fe in m.Mod.Expressions) {

-        ResolveFrameExpression(fe, "modifies", m.IsGhost, m);

-        if (m is Lemma) {

-          Error(fe.tok, "lemmas are not allowed to have modifies clauses");

-        } else if (m is CoLemma) {

-          Error(fe.tok, "colemmas are not allowed to have modifies clauses");

+        foreach (Formal p in m.Ins) {

+          scope.Push(p.Name, p);

         }

-      }

-      foreach (Expression e in m.Decreases.Expressions) {

-        ResolveExpression(e, false, m);

-        // any type is fine

-        if (m.IsGhost && e is WildcardExpr) {

-          Error(e, "'decreases *' is not allowed on ghost methods");

+

+        // Start resolving specification...

+        foreach (MaybeFreeExpression e in m.Req) {

+          ResolveExpression(e.E, false, m);

+          Contract.Assert(e.E.Type != null);  // follows from postcondition of ResolveExpression

+          if (!UnifyTypes(e.E.Type, Type.Bool)) {

+            Error(e.E, "Precondition must be a boolean (got {0})", e.E.Type);

+          }

+        }

+        foreach (FrameExpression fe in m.Mod.Expressions) {

+          ResolveFrameExpression(fe, "modifies", m.IsGhost, m);

+          if (m is Lemma) {

+            Error(fe.tok, "lemmas are not allowed to have modifies clauses");

+          } else if (m is CoLemma) {

+            Error(fe.tok, "colemmas are not allowed to have modifies clauses");

+          }

+        }

+        foreach (Expression e in m.Decreases.Expressions) {

+          ResolveExpression(e, false, m);

+          // any type is fine

+          if (m.IsGhost && e is WildcardExpr) {

+            Error(e, "'decreases *' is not allowed on ghost methods");

+          }

         }

-      }

 

-      // Add out-parameters to a new scope that will also include the outermost-level locals of the body

-      // Don't care about any duplication errors among the out-parameters, since they have already been reported

-      scope.PushMarker();

-      if (m is CoLemma && m.Outs.Count != 0) {

-        Error(m.Outs[0].tok, "colemmas are not allowed to have out-parameters");

-      } else {

-        foreach (Formal p in m.Outs) {

-          scope.Push(p.Name, p);

+        // Add out-parameters to a new scope that will also include the outermost-level locals of the body

+        // Don't care about any duplication errors among the out-parameters, since they have already been reported

+        scope.PushMarker();

+        if (m is CoLemma && m.Outs.Count != 0) {

+          Error(m.Outs[0].tok, "colemmas are not allowed to have out-parameters");

+        } else {

+          foreach (Formal p in m.Outs) {

+            scope.Push(p.Name, p);

+          }

         }

-      }

 

-      // ... continue resolving specification

-      foreach (MaybeFreeExpression e in m.Ens) {

-        ResolveExpression(e.E, true, m);

-        Contract.Assert(e.E.Type != null);  // follows from postcondition of ResolveExpression

-        if (!UnifyTypes(e.E.Type, Type.Bool)) {

-          Error(e.E, "Postcondition must be a boolean (got {0})", e.E.Type);

+        // ... continue resolving specification

+        foreach (MaybeFreeExpression e in m.Ens) {

+          ResolveExpression(e.E, true, m);

+          Contract.Assert(e.E.Type != null);  // follows from postcondition of ResolveExpression

+          if (!UnifyTypes(e.E.Type, Type.Bool)) {

+            Error(e.E, "Postcondition must be a boolean (got {0})", e.E.Type);

+          }

         }

-      }

 

-      // Resolve body

-      if (m.Body != null) {

-        var com = m as CoLemma;

-        if (com != null && com.PrefixLemma != null) {

-          // The body may mentioned the implicitly declared parameter _k.  Throw it into the

-          // scope before resolving the body.

-          var k = com.PrefixLemma.Ins[0];

-          scope.Push(k.Name, k);  // we expect no name conflict for _k

+        // Resolve body

+        if (m.Body != null) {

+          var com = m as CoLemma;

+          if (com != null && com.PrefixLemma != null) {

+            // The body may mentioned the implicitly declared parameter _k.  Throw it into the

+            // scope before resolving the body.

+            var k = com.PrefixLemma.Ins[0];

+            scope.Push(k.Name, k);  // we expect no name conflict for _k

+          }

+          var codeContext = m;

+          ResolveBlockStatement(m.Body, m.IsGhost, codeContext);

         }

-        var codeContext = m;

-        ResolveBlockStatement(m.Body, m.IsGhost, codeContext);

-      }

 

-      // attributes are allowed to mention both in- and out-parameters (including the implicit _k, for colemmas)

-      ResolveAttributes(m.Attributes, false, m);

+        // attributes are allowed to mention both in- and out-parameters (including the implicit _k, for colemmas)

+        ResolveAttributes(m.Attributes, false, m);

 

-      scope.PopMarker();  // for the out-parameters and outermost-level locals

-      scope.PopMarker();  // for the in-parameters

+        scope.PopMarker();  // for the out-parameters and outermost-level locals

+        scope.PopMarker();  // for the in-parameters

+      }

+      finally

+      {

+        currentMethod = null;

+      }

     }

 

     void ResolveCtorSignature(DatatypeCtor ctor, List<TypeParameter> dtTypeArguments) {

@@ -4176,6 +4186,24 @@ namespace Microsoft.Dafny
         if (!s.IsGhost) {

           s.IsGhost = (s.Update == null || s.Update.IsGhost) && s.Locals.All(v => v.IsGhost);

         }

+        foreach (var local in s.Locals)

+        {

+          if (Attributes.Contains(local.Attributes, "assumption"))

+          {

+            if (currentMethod == null)

+            {

+              Error(local.Tok, "assumption variable can only be declared in a method");

+            }

+            if (!local.IsGhost)

+            {

+              Error(local.Tok, "assumption variable must be ghost");

+            }

+            if (!(local.Type is BoolType))

+            {

+              Error(s, "assumption variable must be of type 'bool'");

+            }

+          }

+        }

 

       } else if (stmt is AssignStmt) {

         AssignStmt s = (AssignStmt)stmt;

@@ -4196,6 +4224,26 @@ namespace Microsoft.Dafny
             if (!lvalueIsGhost && specContextOnly) {

               Error(stmt, "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)");

             }

+

+            var localVar = var as LocalVariable;

+            if (localVar != null && currentMethod != null && Attributes.Contains(localVar.Attributes, "assumption"))

+            {

+              var rhs = s.Rhs as ExprRhs;

+              var expr = (rhs != null ? rhs.Expr : null);

+              var binaryExpr = expr as BinaryExpr;

+              if (binaryExpr != null

+                  && (binaryExpr.Op == BinaryExpr.Opcode.And)

+                  && (binaryExpr.E0.Resolved is IdentifierExpr)

+                  && ((IdentifierExpr)(binaryExpr.E0.Resolved)).Var == localVar

+                  && !currentMethod.AssignedAssumptionVariables.Contains(localVar))

+              {

+                currentMethod.AssignedAssumptionVariables.Add(localVar);

+              }

+              else

+              {

+                Error(stmt, string.Format("there may be at most one assignment to an assumption variable, the RHS of which must match the expression \"{0} && <boolean expression>\"", localVar.Name));

+              }

+            }

           }

         } else if (lhs is FieldSelectExpr) {

           var fse = (FieldSelectExpr)lhs;

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index b622b792..b1622efd 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -5468,6 +5468,10 @@ namespace Microsoft.Dafny {
           Bpl.LocalVariable var = new Bpl.LocalVariable(local.Tok, new Bpl.TypedIdent(local.Tok, local.AssignUniqueName(currentDeclaration), varType, wh));

           var.Attributes = etran.TrAttributes(local.Attributes, null); ;

           locals.Add(var);

+          if (Attributes.Contains(local.Attributes, "assumption"))

+          {

+            builder.Add(new AssumeCmd(local.Tok, new Bpl.IdentifierExpr(local.Tok, local.AssignUniqueName(currentDeclaration), varType), new QKeyValue(local.Tok, "assumption_variable_initialization", new List<object>(), null)));

+          }

         }

         if (s.Update != null) {

           TrStmt(s.Update, builder, locals, etran);

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 34c51d58..8987b169 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -2267,6 +2267,26 @@ Execution trace:
 

 Dafny program verifier finished with 24 verified, 4 errors

 

+-------------------- AssumptionVariables0.dfy --------------------

+AssumptionVariables0.dfy(3,29): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && <boolean expression>"

+AssumptionVariables0.dfy(4,33): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a2 && <boolean expression>"

+AssumptionVariables0.dfy(6,20): Error: assumption variable must be ghost

+AssumptionVariables0.dfy(6,2): Error: assumption variable must be of type 'bool'

+AssumptionVariables0.dfy(12,5): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a3 && <boolean expression>"

+AssumptionVariables0.dfy(14,5): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a3 && <boolean expression>"

+AssumptionVariables0.dfy(24,5): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && <boolean expression>"

+AssumptionVariables0.dfy(28,5): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && <boolean expression>"

+AssumptionVariables0.dfy(50,9): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && <boolean expression>"

+AssumptionVariables0.dfy(54,26): Error: assumption variable must be ghost

+AssumptionVariables0.dfy(58,37): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && <boolean expression>"

+AssumptionVariables0.dfy(58,10): Error: assumption variable must be of type 'bool'

+AssumptionVariables0.dfy(66,15): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && <boolean expression>"

+13 resolution/type errors detected in AssumptionVariables0.dfy

+

+-------------------- AssumptionVariables1.dfy --------------------

+

+Dafny program verifier finished with 4 verified, 0 errors

+

 -------------------- Superposition.dfy --------------------

 

 Verifying CheckWellformed$$_0_M0.C.M ...

diff --git a/Test/dafny0/AssumptionVariables0.dfy b/Test/dafny0/AssumptionVariables0.dfy
new file mode 100644
index 00000000..2087b402
--- /dev/null
+++ b/Test/dafny0/AssumptionVariables0.dfy
@@ -0,0 +1,72 @@
+method test0(x: int)

+{

+  ghost var {:assumption} a0 := false;  // error

+  ghost var a1, {:assumption} a2 := true, false;  // error

+  ghost var {:assumption} a3: bool;

+  var {:assumption} a4;  // 2 errors

+

+  a0 := a0 && (0 < x);

+

+  a1 := a1 && true;

+

+  a3 := true;  // error

+

+  a3 := a2 && true;  // error

+

+  a3 := a3 && true;

+}

+

+

+method test1()

+{

+  ghost var {:assumption} a0: bool;

+

+  a0 := true;  // error

+

+  a0 := a0 && true;

+

+  a0 := a0 && true;  // error

+}

+

+

+method test2()

+{

+  ghost var {:assumption} a0: bool;

+

+  a0 := a0 && true;

+

+  if (false)

+  {

+    var a0 := 1;

+

+    a0 := 2;

+

+    a0 := 3;

+

+    if (false)

+    {

+      ghost var {:assumption} a0: bool;

+

+      a0 := a0;  // error

+

+      if (false)

+      {

+        var {:assumption} a0: bool;  // error

+

+        if (false)

+        {

+          ghost var {:assumption} a0 := 1;  // 2 errors

+

+          if (false)

+          {

+            ghost var {:assumption} a0: bool;

+

+            a0 := a0 && true;

+

+            a0 := a0 && true;  // error

+          }

+        }

+      }

+    }

+  }

+}

diff --git a/Test/dafny0/AssumptionVariables1.dfy b/Test/dafny0/AssumptionVariables1.dfy
new file mode 100644
index 00000000..135c2699
--- /dev/null
+++ b/Test/dafny0/AssumptionVariables1.dfy
@@ -0,0 +1,34 @@
+method test0(x: int)

+{

+  ghost var {:assumption} a0: bool;

+  ghost var {:assumption} a1: bool, a2: bool, {:assumption} a3: bool;

+

+  assert a0 && a1 && a3;

+

+  a0 := a0 && (0 < x);

+

+  a1 := a1 && true;

+}

+

+

+method test1(x: int)

+{

+  ghost var {:assumption} a0: bool;

+

+  assert a0;

+

+  a0 := a0 && (0 < x);

+

+  var y := x;

+

+  while (y < 0)

+  {

+    ghost var {:assumption} a0: bool;

+

+    assert a0;

+

+    a0 := a0 && (0 < y);

+

+    y := y + 1;

+  }

+}

diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index 38e37d5d..fe3a29e1 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -30,7 +30,8 @@ for %%f in (TypeTests.dfy NatTypes.dfy RealTypes.dfy Definedness.dfy
             RankPos.dfy RankNeg.dfy

             Computations.dfy ComputationsNeg.dfy

             Include.dfy Includee.dfy AutoReq.dfy DatatypeUpdate.dfy ModifyStmt.dfy SeqSlice.dfy

-            RealCompare.dfy) do (

+            RealCompare.dfy

+            AssumptionVariables0.dfy AssumptionVariables1.dfy) do (

   echo.

   echo -------------------- %%f --------------------

   %DAFNY_EXE% /compile:0 /print:out.bpl.tmp /dprint:out.dfy.tmp %* %%f