Make reveal axioms from opaque functions quantify over layers

10 files changed, 192 insertions, 61 deletions

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index af40173a..2077fe7e 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -214,6 +214,7 @@ namespace Microsoft.Dafny {
     /// - if the attribute is {:nm false}, then value==false

     /// - if the attribute is anything else, then value returns as whatever it was passed in as.

     /// </summary>

+    [Pure]

     public static bool ContainsBool(Attributes attrs, string nm, ref bool value) {

       Contract.Requires(nm != null);

       for (; attrs != null; attrs = attrs.Prev) {

@@ -5544,11 +5545,19 @@ namespace Microsoft.Dafny {
         return "q$" + quantUnique;

       }

     }

+    public String Refresh(String s) {

+      return s + "#" + typeRefreshCount++ + FullName; 

+    }

     public TypeParameter Refresh(TypeParameter p) {

       TypeParameter cp = new TypeParameter(p.tok, typeRefreshCount++ + "#" + p.Name, p.EqualitySupport);

       cp.Parent = this;

       return cp;

     }

+    [ContractInvariantMethod]

+    void ObjectInvariant() {

+      var _scratch = true;

+      Contract.Invariant(Attributes.ContainsBool(Attributes, "typeQuantifier", ref _scratch) || TypeArgs.Count == 0);

+    }

     public QuantifierExpr(IToken tok, List<TypeParameter> tvars, List<BoundVar> bvars, Expression range, Expression term, Attributes attrs)

       : base(tok, bvars, range, term, attrs) {

       Contract.Requires(tok != null);

diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs
index 1500e37f..70fdae85 100644
--- a/Source/Dafny/RefinementTransformer.cs
+++ b/Source/Dafny/RefinementTransformer.cs
@@ -492,6 +492,8 @@ namespace Microsoft.Dafny
       }

       moduleUnderConstruction = null;

     }

+    public void PostCyclicityResolve(ModuleDefinition m) { 

+    }

     Function CloneFunction(IToken tok, Function f, bool isGhost, List<Expression> moreEnsures, Expression moreBody, Expression replacementBody, bool checkPrevPostconditions, Attributes moreAttributes) {

       Contract.Requires(tok != null);

       Contract.Requires(moreBody == null || f is Predicate);

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 19d3025f..f3e3ce93 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -308,6 +308,9 @@ namespace Microsoft.Dafny
             }

           }

         }

+        foreach (var r in rewriters) {

+          r.PostCyclicityResolve(module);

+        }

       }

       // fill in default decreases clauses:  for functions and methods, and for loops

       FillInDefaultDecreasesClauses(prog);

diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs
index dbfcae01..ca3c105d 100644
--- a/Source/Dafny/Rewriter.cs
+++ b/Source/Dafny/Rewriter.cs
@@ -10,6 +10,8 @@ namespace Microsoft.Dafny
   {

     void PreResolve(ModuleDefinition m);

     void PostResolve(ModuleDefinition m);

+    // After SCC/Cyclicity/Recursivity analysis:

+    void PostCyclicityResolve(ModuleDefinition m);

   }

   [ContractClassFor(typeof(IRewriter))]

   abstract class IRewriterContracts : IRewriter

@@ -20,6 +22,9 @@ namespace Microsoft.Dafny
     public void PostResolve(ModuleDefinition m) {

       Contract.Requires(m != null);

     }

+    public void PostCyclicityResolve(ModuleDefinition m) {

+      Contract.Requires(m != null);

+    }

   }

 

   public class AutoGeneratedToken : TokenWrapper

@@ -136,6 +141,9 @@ namespace Microsoft.Dafny
       }

     }

 

+    public void PostCyclicityResolve(ModuleDefinition m) { 

+    }

+

     void ProcessClassPostResolve(ClassDecl cl) {

       // Find all fields of a reference type, and make a note of whether or not the reference type has a Repr field.

       // Also, find the Repr field and the function Valid in class "cl"

@@ -382,11 +390,13 @@ namespace Microsoft.Dafny
     protected Dictionary<Function, Function> original;    // Given a full version of an opaque function, find the original opaque version

     protected Dictionary<Lemma, Function> revealOriginal; // Map reveal_* lemmas back to their original functions

 

-    public void PreResolve(ModuleDefinition m) {

+    public OpaqueFunctionRewriter() : base() {

       fullVersion = new Dictionary<Function, Function>();

       original = new Dictionary<Function, Function>();

       revealOriginal = new Dictionary<Lemma, Function>();

+    }

 

+    public void PreResolve(ModuleDefinition m) {

       foreach (var d in m.TopLevelDecls) {

         if (d is ClassDecl) {

           DuplicateOpaqueClassFunctions((ClassDecl)d);

@@ -418,6 +428,18 @@ namespace Microsoft.Dafny
         }

       }

     }

+

+    public void PostCyclicityResolve(ModuleDefinition m) {

+      // Add layer quantifier if the function is recursive 

+      foreach (var decl in ModuleDefinition.AllCallables(m.TopLevelDecls)) {

+        if (decl is Lemma) {

+          var lem = (Lemma)decl;

+          if (revealOriginal.ContainsKey(lem)) {

+            needsLayerQuantifier(lem, revealOriginal[lem]);

+          }

+        }

+      }

+    }

   

     // Is f the full version of an opaque function?

     public bool isFullVersion(Function f) {

@@ -567,6 +589,24 @@ namespace Microsoft.Dafny
       }

     }

 

+    // If the function is recursive, make the reveal lemma quantifier a layerQuantifier

+    protected void needsLayerQuantifier(Lemma lem, Function fn) {

+      var origForall = lem.Ens[0].E as ForallExpr;

+      if (origForall != null && fn.IsRecursive) {

+        var newAttrib = new Attributes("layerQuantifier", new List<Attributes.Argument>(), origForall.Attributes);

+        var newForall = new ForallExpr(origForall.tok, origForall.TypeArgs, origForall.BoundVars, origForall.Range, origForall.Term, newAttrib);

+        newForall.Type = Type.Bool;

+        lem.Ens[0] = new MaybeFreeExpression(newForall);

+      }

+    }

+

+    // This is for the reveal_F function. The ensures clause looks like this:

+    // 

+    //     ensures forall<A,B> x : T<A,B> :: F(x) == F_FULL(x)

+    //

+    // But the type argument substitutions for F and F_FULL are way off, so 

+    // we use this function to make a substitution to the type variables the

+    // forall quantifier binds.

     protected void fixupTypeArguments(Lemma lem, Function fn) {

       var origForall = lem.Ens[0].E as ForallExpr;

       if (origForall != null) {

@@ -593,6 +633,8 @@ namespace Microsoft.Dafny
         return;

       }

 

+      // DR: Note: I don't know of any example that actually gets to these lines below: 

+

       // Consolidate the requirements

       Expression reqs = Expression.CreateBoolLiteral(fn.tok, true);

       foreach (var expr in fn.Req) {

@@ -687,6 +729,9 @@ namespace Microsoft.Dafny
       }

     }

 

+    public void PostCyclicityResolve(ModuleDefinition m) { 

+    }

+

     Expression subVars(List<Formal> formals, List<Expression> values, Expression e, Expression f_this) {

       Contract.Assert(formals != null);

       Contract.Assert(values != null);

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 65a4ee53..a77590b4 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -922,8 +922,15 @@ namespace Microsoft.Dafny {
       }

     }

 

-    Bpl.Expr LayerSucc(Bpl.Expr e) {

-      return FunctionCall(e.tok, BuiltinFunction.LayerSucc, null, e);

+    Bpl.Expr LayerSucc(Bpl.Expr e, int amt = 1) {

+      if (amt == 0) {

+        return e;

+      } else if (amt > 0) {

+        return FunctionCall(e.tok, BuiltinFunction.LayerSucc, null, LayerSucc(e, amt-1));

+      } else {

+        Contract.Assert(false);

+        return null;

+      }

     }

 

     // Makes a call to equality, if k is null, or otherwise prefix equality. For codatatypes.

@@ -8257,7 +8264,7 @@ namespace Microsoft.Dafny {
       public readonly string This;

       public readonly string modifiesFrame; // the name of the context's frame variable.

       readonly Function applyLimited_CurrentFunction;

-      public readonly int layerInterCluster = 1;

+      public readonly Bpl.Expr layerInterCluster;     

       public readonly Bpl.Expr layerIntraCluster = null;  // a value of null says to do the same as for inter-cluster calls

       public int Statistics_CustomLayerFunctionCount = 0;

       public readonly bool ProducingCoCertificates = false;

@@ -8270,13 +8277,12 @@ namespace Microsoft.Dafny {
         Contract.Invariant(translator != null);

         Contract.Invariant(This != null);

         Contract.Invariant(modifiesFrame != null);

-        Contract.Invariant(0 <= layerInterCluster);

+        Contract.Invariant(layerInterCluster != null);

         Contract.Invariant(0 <= Statistics_CustomLayerFunctionCount);

       }

 

       /// <summary>

-      /// This is the most general constructor.  It is private and takes all the parameters.  Whenever

-      /// one ExpressionTranslator is constructed from another, unchanged parameters are just copied in.

+      /// This is a general constructor, but takes the layerInterCluster as an int.

       /// </summary>

       ExpressionTranslator(Translator translator, PredefinedDecls predef, Bpl.Expr heap, string thisVar,

         Function applyLimited_CurrentFunction, int layerInterCluster, Bpl.Expr layerIntraCluster, string modifiesFrame) {

@@ -8293,6 +8299,30 @@ namespace Microsoft.Dafny {
         this.HeapExpr = heap;

         this.This = thisVar;

         this.applyLimited_CurrentFunction = applyLimited_CurrentFunction;

+        this.layerInterCluster = LayerN(layerInterCluster);

+        this.layerIntraCluster = layerIntraCluster;

+        this.modifiesFrame = modifiesFrame;

+      }

+

+      /// <summary>

+      /// This is the most general constructor.  It is private and takes all the parameters.  Whenever

+      /// one ExpressionTranslator is constructed from another, unchanged parameters are just copied in.

+      /// </summary>

+      ExpressionTranslator(Translator translator, PredefinedDecls predef, Bpl.Expr heap, string thisVar,

+        Function applyLimited_CurrentFunction, Bpl.Expr layerInterCluster, Bpl.Expr layerIntraCluster, string modifiesFrame) {

+

+        Contract.Requires(translator != null);

+        Contract.Requires(predef != null);

+        Contract.Requires(heap != null);

+        Contract.Requires(thisVar != null);

+        Contract.Requires(layerInterCluster != null);

+        Contract.Requires(modifiesFrame != null);

+

+        this.translator = translator;

+        this.predef = predef;

+        this.HeapExpr = heap;

+        this.This = thisVar;

+        this.applyLimited_CurrentFunction = applyLimited_CurrentFunction;

         this.layerInterCluster = layerInterCluster;

         this.layerIntraCluster = layerIntraCluster;

         this.modifiesFrame = modifiesFrame;

@@ -8369,9 +8399,9 @@ namespace Microsoft.Dafny {
         Contract.Requires(0 <= offset);

         Contract.Ensures(Contract.Result<ExpressionTranslator>() != null);

 

-        var et = new ExpressionTranslator(translator, predef, HeapExpr, This, applyLimited_CurrentFunction, layerInterCluster + offset, layerIntraCluster, modifiesFrame);

+        var et = new ExpressionTranslator(translator, predef, HeapExpr, This, applyLimited_CurrentFunction, translator.LayerSucc(layerInterCluster, offset), layerIntraCluster, modifiesFrame);

         if (this.oldEtran != null) {

-          var etOld = new ExpressionTranslator(translator, predef, Old.HeapExpr, This, applyLimited_CurrentFunction, layerInterCluster + offset, layerIntraCluster, modifiesFrame);

+          var etOld = new ExpressionTranslator(translator, predef, Old.HeapExpr, This, applyLimited_CurrentFunction, translator.LayerSucc(layerInterCluster, offset), layerIntraCluster, modifiesFrame);

           etOld.oldEtran = etOld;

           et.oldEtran = etOld;

         }

@@ -8414,14 +8444,11 @@ namespace Microsoft.Dafny {
         Contract.Ensures(Contract.Result<Bpl.Expr>() != null);

         return new Bpl.IdentifierExpr(Token.NoToken, "$LZ", predef.LayerType);

       }

+

       public Bpl.Expr LayerN(int n) {

         Contract.Requires(0 <= n);

         Contract.Ensures(Contract.Result<Bpl.Expr>() != null);

-        var s = LayerZero();

-        for (; n != 0; n--) {

-          s = translator.FunctionCall(Token.NoToken, BuiltinFunction.LayerSucc, null, s);

-        }

-        return s;

+        return translator.LayerSucc(LayerZero(), n);

       }

 

       public Bpl.IdentifierExpr ModuleContextHeight() {

@@ -8695,7 +8722,7 @@ namespace Microsoft.Dafny {
               ModuleDefinition.InSameSCC(e.Function, applyLimited_CurrentFunction)) {

               layerArgument = this.layerIntraCluster;

             } else {

-              layerArgument = LayerN(layerInterCluster);

+              layerArgument = this.layerInterCluster;

             }

           } else {

             layerArgument = null;

@@ -9054,6 +9081,15 @@ namespace Microsoft.Dafny {
           Bpl.Expr typeAntecedent = TrBoundVariables(e.BoundVars, bvars);

           Bpl.QKeyValue kv = TrAttributes(e.Attributes, "trigger");

           Bpl.Trigger tr = null;

+          ExpressionTranslator bodyEtran = this;

+          bool _scratch = true;

+          if (Attributes.ContainsBool(e.Attributes, "layerQuantifier", ref _scratch)) {

+            // If this is a layer quantifier, quantify over layers here, and use $LS(ly) layers in the translation of the body

+            Bpl.Expr ly; var lyVar = BplBoundVar(e.Refresh("$ly"), predef.LayerType, out ly);

+            bvars.Add(lyVar);

+            Expr layer = translator.LayerSucc(ly); 

+            bodyEtran = new ExpressionTranslator(translator, predef, HeapExpr, This, applyLimited_CurrentFunction, layer, layer, modifiesFrame);

+          }

           for (Attributes aa = e.Attributes; aa != null; aa = aa.Prev) {

             if (aa.Name == "trigger") {

               List<Bpl.Expr> tt = new List<Bpl.Expr>();

@@ -9061,17 +9097,17 @@ namespace Microsoft.Dafny {
                 if (arg.E == null) {

                   Console.WriteLine("Warning: string argument to 'trigger' attribute ignored");

                 } else {

-                  tt.Add(TrExpr(arg.E));

+                  tt.Add(bodyEtran.TrExpr(arg.E));

                 }

               }

               tr = new Bpl.Trigger(expr.tok, true, tt, tr);

-            }

+            } 

           }

           var antecedent = typeAntecedent;

           if (e.Range != null) {

-            antecedent = Bpl.Expr.And(antecedent, TrExpr(e.Range));

+            antecedent = Bpl.Expr.And(antecedent, bodyEtran.TrExpr(e.Range));

           }

-          Bpl.Expr body = TrExpr(e.Term);

+          Bpl.Expr body = bodyEtran.TrExpr(e.Term);

 

           if (e is ForallExpr) {

             return new Bpl.ForallExpr(expr.tok, new List<TypeVariable>(), Concat(tyvars,bvars), kv, tr, Bpl.Expr.Imp(antecedent, body));

@@ -10127,7 +10163,7 @@ namespace Microsoft.Dafny {
           var B2 = etran2.TrExpr(e.E2);

           var needsTokenAdjust = TrSplitNeedsTokenAdjustment(expr);

           // Dan: dafny4/Circ.dfy needs this one to be 2+, rather than 1+ 

-          Bpl.Expr layer = etran.LayerN(2 + etran.layerInterCluster); 

+          Bpl.Expr layer = LayerSucc(etran.layerInterCluster, 2); 

           foreach (var c in CoPrefixEquality(needsTokenAdjust ? new ForceCheckToken(expr.tok) : expr.tok, codecl, e.E1.Type.TypeArgs, e.E2.Type.TypeArgs, kMinusOne, layer, A2, B2, true)) {

             var p = Bpl.Expr.Binary(c.tok, BinaryOperator.Opcode.Or, prefixEqK, Bpl.Expr.Imp(kPos, c));

             splits.Add(new SplitExprInfo(SplitExprInfo.K.Checked, p));

diff --git a/Test/dafny0/FunctionSpecifications.dfy b/Test/dafny0/FunctionSpecifications.dfy
index caf8a681..1b7c8bfc 100644
--- a/Test/dafny0/FunctionSpecifications.dfy
+++ b/Test/dafny0/FunctionSpecifications.dfy
@@ -146,13 +146,6 @@ function {:opaque} f(i:int):int
   f(i) + 1

 }

 

-method m()

-  ensures false;

-{

-  reveal_f();

-  assert f(0) == f(0) + 1;

-}

-

 // Try a sneakier (nested) version of the test above

 function {:opaque} g(i:int):int

   decreases i;

@@ -165,13 +158,6 @@ function h(i:int):int
   g(i)

 }

 

-method n()

-  ensures false;

-{

-  reveal_g();

-  assert g(0) == g(0) + 1;

-}

-

 // Check that using the reveal_ lemma to prove the well-definedness of a function

 // in a lower SCC does not cause a soundness problem

 

@@ -188,14 +174,3 @@ function {:opaque} B(): int
   A()

 }

 

-method m_noreveal()

-  ensures false;

-{

-  assert f(0) == f(0) + 1;

-}

-

-method n_noreveal()

-  ensures false;

-{

-  assert g(0) == g(0) + 1;

-}

diff --git a/Test/dafny0/FunctionSpecifications.dfy.expect b/Test/dafny0/FunctionSpecifications.dfy.expect
index 618372d8..e7df68f7 100644
--- a/Test/dafny0/FunctionSpecifications.dfy.expect
+++ b/Test/dafny0/FunctionSpecifications.dfy.expect
@@ -37,20 +37,14 @@ FunctionSpecifications.dfy(130,27): Error: assertion violation
 Execution trace:

     (0,0): anon0

     (0,0): anon3_Else

-FunctionSpecifications.dfy(165,3): Error: cannot prove termination; try supplying a decreases clause

+FunctionSpecifications.dfy(158,3): Error: cannot prove termination; try supplying a decreases clause

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Else

-FunctionSpecifications.dfy(181,3): Error: cannot prove termination; try supplying a decreases clause

+FunctionSpecifications.dfy(167,3): Error: cannot prove termination; try supplying a decreases clause

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Else

-FunctionSpecifications.dfy(194,15): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-FunctionSpecifications.dfy(200,15): Error: assertion violation

-Execution trace:

-    (0,0): anon0

 FunctionSpecifications.dfy(135,20): Error BP5003: A postcondition might not hold on this return path.

 FunctionSpecifications.dfy(137,29): Related location: This is the postcondition that might not hold.

 Execution trace:

@@ -62,16 +56,16 @@ FunctionSpecifications.dfy(146,3): Error: failure to decrease termination measur
 Execution trace:

     (0,0): anon0

     (0,0): anon3_Else

-FunctionSpecifications.dfy(160,3): Error: failure to decrease termination measure

+FunctionSpecifications.dfy(153,3): Error: failure to decrease termination measure

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Else

-FunctionSpecifications.dfy(188,3): Error: cannot prove termination; try supplying a decreases clause

+FunctionSpecifications.dfy(174,3): Error: cannot prove termination; try supplying a decreases clause

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Else

-FunctionSpecifications.dfy(185,20): Error: cannot prove termination; try supplying a decreases clause

+FunctionSpecifications.dfy(171,20): Error: cannot prove termination; try supplying a decreases clause

 Execution trace:

     (0,0): anon0

 

-Dafny program verifier finished with 23 verified, 17 errors

+Dafny program verifier finished with 17 verified, 15 errors

diff --git a/Test/dafny0/OpaqueFunctions.dfy b/Test/dafny0/OpaqueFunctions.dfy
index 3b591ef2..d00e1246 100644
--- a/Test/dafny0/OpaqueFunctions.dfy
+++ b/Test/dafny0/OpaqueFunctions.dfy
@@ -159,7 +159,62 @@ module M1 refines M0 {
 

 function{:opaque} id<A>(x : A):A { x }

 

+method id_ok()

+{

+  reveal_id();

+  assert id(1) == 1;

+}

+

+method id_fail()

+{

+  assert id(1) == 1;

+}

+

 datatype Box<A> = Bx(A)

 

 function{:opaque} id_box(x : Box):Box { x }

 

+method box_ok()

+{

+  reveal_id();

+  assert id(Bx(1)) == Bx(1);

+}

+

+method box_fail()

+{

+  assert id(Bx(1)) == Bx(1);

+}

+

+// ------------------------- opaque and layer quantifiers

+

+module LayerQuantifiers

+{

+  function{:opaque} f(x:nat) : bool { if x == 0 then true else f(x-1) }

+

+  method rec_should_ok()

+  {

+    reveal_f();

+    assert f(1);

+  }

+

+  method rec_should_fail()

+  {

+    assert f(1);

+  }

+

+  method rec_should_unroll_ok(one : int)

+    requires one == 1;

+  {

+    reveal_f();

+    // this one should have enough fuel

+    assert f(one + one);

+  }

+

+  method rec_should_unroll_fail(one : int)

+    requires one == 1;

+  {

+    reveal_f();

+    // this one does not have enough fuel

+    assert f(one + one + one);

+  }

+}

diff --git a/Test/dafny0/OpaqueFunctions.dfy.expect b/Test/dafny0/OpaqueFunctions.dfy.expect
index 9d4497dc..df076f60 100644
--- a/Test/dafny0/OpaqueFunctions.dfy.expect
+++ b/Test/dafny0/OpaqueFunctions.dfy.expect
@@ -71,5 +71,17 @@ Execution trace:
 OpaqueFunctions.dfy(138,12): Error: assertion violation

 Execution trace:

     (0,0): anon0

+OpaqueFunctions.dfy(202,12): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+OpaqueFunctions.dfy(218,12): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+OpaqueFunctions.dfy(170,16): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+OpaqueFunctions.dfy(185,20): Error: assertion violation

+Execution trace:

+    (0,0): anon0

 

-Dafny program verifier finished with 45 verified, 19 errors

+Dafny program verifier finished with 59 verified, 23 errors

diff --git a/Test/dafny0/OpaqueFunctionsFail.dfy b/Test/dafny0/OpaqueFunctionsFail.dfy
index ae7f81f6..3895ed3c 100644
--- a/Test/dafny0/OpaqueFunctionsFail.dfy
+++ b/Test/dafny0/OpaqueFunctionsFail.dfy
@@ -1,9 +1,9 @@
-
-// ---------------------------------- opaque and generics
-
 // RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
+
+// ---------------------------------- opaque and generics
+
 // This function cannot normally be called, so the
 // generated opaquity code contains such a bad call.
 function{:opaque} zero<A>():int { 0 }