Make reveal axioms from opaque functions quantify over layers

5 files changed, 115 insertions, 20 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));