Improve autoReq's interactions with opaque

5 files changed, 129 insertions, 21 deletions

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 4d67dbe9..be968cfa 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -4078,8 +4078,8 @@ namespace Microsoft.Dafny {
       Contract.Ensures(Contract.Result<MatchCaseExpr>() != null);

 

       ResolvedCloner cloner = new ResolvedCloner();

-      var newVars = old_case.Arguments.ConvertAll(cloner.CloneBoundVar);

-      new_body = VarSubstituter(old_case.Arguments, newVars, new_body);

+      var newVars = old_case.Arguments.ConvertAll(cloner.CloneBoundVar);   

+      new_body = VarSubstituter(old_case.Arguments.ConvertAll<NonglobalVariable>(x=>(NonglobalVariable)x), newVars, new_body);

 

       var new_case = new MatchCaseExpr(old_case.tok, old_case.Id, newVars, new_body);

 

@@ -4113,7 +4113,7 @@ namespace Microsoft.Dafny {
       LHSs.Iter(p => oldVars.AddRange(p.Vars));

       var newVars = new List<BoundVar>();

       newLHSs.Iter(p => newVars.AddRange(p.Vars));

-      body = VarSubstituter(oldVars, newVars, body);

+      body = VarSubstituter(oldVars.ConvertAll<NonglobalVariable>(x => (NonglobalVariable)x), newVars, body);

 

       var let = new LetExpr(tok, newLHSs, RHSs, body, exact);

       let.Type = body.Type;  // resolve here

@@ -4135,7 +4135,7 @@ namespace Microsoft.Dafny {
         body = expr.Term;

       }

 

-      body = VarSubstituter(expr.BoundVars, newVars, body);

+      body = VarSubstituter(expr.BoundVars.ConvertAll<NonglobalVariable>(x=>(NonglobalVariable)x), newVars, body);

       

       QuantifierExpr q;

       if (forall) {

@@ -4148,7 +4148,7 @@ namespace Microsoft.Dafny {
       return q;           

     }

 

-    private static Expression VarSubstituter(List<BoundVar> oldVars, List<BoundVar> newVars, Expression e) {

+    public static Expression VarSubstituter(List<NonglobalVariable> oldVars, List<BoundVar> newVars, Expression e) {

       Contract.Requires(oldVars != null && newVars != null);

       Contract.Requires(oldVars.Count == newVars.Count);

       

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index b8c561b3..e9463e09 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -191,8 +191,9 @@ namespace Microsoft.Dafny
       var refinementTransformer = new RefinementTransformer(this, prog);

       rewriters.Add(refinementTransformer);

       rewriters.Add(new AutoContractsRewriter());

-      rewriters.Add(new OpaqueFunctionRewriter());

-      rewriters.Add(new AutoReqFunctionRewriter(this));

+      var opaqueRewriter = new OpaqueFunctionRewriter();      

+      rewriters.Add(new AutoReqFunctionRewriter(this, opaqueRewriter));

+      rewriters.Add(opaqueRewriter);

 

       systemNameInfo = RegisterTopLevelDecls(prog.BuiltIns.SystemModule, false);

       foreach (var decl in sortedDecls) {

diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs
index 5d0eab47..7b7ad5c9 100644
--- a/Source/Dafny/Rewriter.cs
+++ b/Source/Dafny/Rewriter.cs
@@ -372,12 +372,14 @@ namespace Microsoft.Dafny
   /// specifically asks to see it via the reveal_foo() lemma

   /// </summary>

   public class OpaqueFunctionRewriter : IRewriter {

-    //protected Dictionary<Function, Function> fullVersion;

-    protected Dictionary<Function, Function> original;

+    protected Dictionary<Function, Function> fullVersion; // Given an opaque function, retrieve the full

+    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) {

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

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

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

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

 

       foreach (var d in m.TopLevelDecls) {

         if (d is ClassDecl) {

@@ -397,14 +399,40 @@ namespace Microsoft.Dafny
           foreach (Expression ens in fn.Ens) {

             visitor.Visit(ens, context);

           }

+        } 

+      }

+

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

+        if (decl is Lemma) {

+          var lem = (Lemma)decl;

+          if (revealOriginal.ContainsKey(lem)) {

+            fixupRevealLemma(lem, revealOriginal[lem]);

+          }

         }

       }

     }

-

+  

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

-    protected bool isFullVersion(Function f) {

+    public bool isFullVersion(Function f) {

       return original.ContainsKey(f);

     }

+    

+    // In case we change how opacity is denoted

+    public bool isOpaque(Function f) {

+      return fullVersion.ContainsKey(f);

+    }

+

+    public Function OpaqueVersion(Function f) {

+      Function ret;

+      original.TryGetValue(f, out ret);

+      return ret;

+    }

+

+    public Function FullVersion(Function f) {

+      Function ret;

+      fullVersion.TryGetValue(f, out ret);

+      return ret;

+    }

 

     // Trims the body from the original function and then adds an internal,

     // full version, along with a lemma connecting the two

@@ -420,7 +448,7 @@ namespace Microsoft.Dafny
             var cloner = new Cloner();

             var fWithBody = cloner.CloneFunction(f, "#" + f.Name + "_FULL");  

             newDecls.Add(fWithBody);

-            //fullVersion.Add(f, fWithBody);

+            fullVersion.Add(f, fWithBody);

             original.Add(fWithBody, f);

 

             var newToken = new Boogie.Token(f.tok.line, f.tok.col);

@@ -489,6 +517,7 @@ namespace Microsoft.Dafny
                                     new Specification<FrameExpression>(new List<FrameExpression>(), null), newEnsuresList,

                                     new Specification<Expression>(new List<Expression>(), null), null, lemma_attrs, false);

             newDecls.Add(reveal);

+            revealOriginal[reveal] = f;

 

             // Update f's body to simply call the full version, so we preserve recursion checks, decreases clauses, etc.

             f.Body = func_builder(fWithBody);

@@ -496,8 +525,7 @@ namespace Microsoft.Dafny
         }

       }

       c.Members.AddRange(newDecls);

-    }

-

+    }    

 

     protected class OpaqueFunctionContext {

       public Function original;   // The original declaration of the opaque function

@@ -522,6 +550,33 @@ namespace Microsoft.Dafny
         return true;

       }

     }

+

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

+      if (fn.Req.Count == 0) {

+        return;

+      }

+

+      // Consolidate the requirements

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

+      foreach (var expr in fn.Req) {

+        reqs = Expression.CreateAnd(reqs, expr);

+      }

+

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

+      var origImpl = (BinaryExpr)origForall.Term;

+

+      // Substitute the forall's variables for those of the fn

+      var formals = fn.Formals.ConvertAll<NonglobalVariable>(x => (NonglobalVariable)x);

+      reqs = Expression.VarSubstituter(formals, origForall.BoundVars, reqs);

+

+      var newImpl = Expression.CreateImplies(reqs, origImpl.E1);

+      //var newForall = Expression.CreateQuantifier(origForall, true, newImpl);

+      var newForall = new ForallExpr(origForall.tok, origForall.BoundVars, origForall.Range, newImpl, origForall.Attributes);

+      newForall.Type = Type.Bool;

+

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

+    }

+

   }

 

 

@@ -532,10 +587,12 @@ namespace Microsoft.Dafny
   public class AutoReqFunctionRewriter : IRewriter {

     Function parentFunction;

     Resolver resolver;

+    OpaqueFunctionRewriter opaqueInfo;

     bool containsMatch; // TODO: Track this per-requirement, rather than per-function

 

-    public AutoReqFunctionRewriter(Resolver r) {

+    public AutoReqFunctionRewriter(Resolver r, OpaqueFunctionRewriter o) {

       this.resolver = r;

+      this.opaqueInfo = o;

     }

 

     public void PreResolve(ModuleDefinition m) { 

@@ -561,16 +618,52 @@ namespace Microsoft.Dafny
             addAutoReqToolTipInfo("pre", fn, auto_reqs);

 

             // Then the body itself, if any

-            if (fn.Body != null) {

-              auto_reqs = generateAutoReqs(fn.Body);

+            var body = fn.Body;

+            if (opaqueInfo.isOpaque(fn)) {  // Opaque functions don't have a body at this point, so use the original body

+              body = opaqueInfo.FullVersion(fn).Body;

+            }

+

+            if (body != null) {

+              auto_reqs = generateAutoReqs(body);

+

+              if (opaqueInfo.isOpaque(fn)) {  // We need to swap fn's variables in for fn_FULL's               

+                List<Expression> fnVars = new List<Expression>();

+                foreach (var formal in fn.Formals) {

+                  var id = new IdentifierExpr(formal.tok, formal.Name);

+                  id.Var = formal;  // resolve here

+                  fnVars.Add(id);

+                }

+

+                var body_reqs = new List<Expression>();

+                foreach (var req in auto_reqs) {

+                  body_reqs.Add(subVars(opaqueInfo.FullVersion(fn).Formals, fnVars, req, null));

+                }

+                auto_reqs = body_reqs;

+              }

+

               fn.Req.AddRange(auto_reqs);

               addAutoReqToolTipInfo("post", fn, auto_reqs);

-            }            

+            }          

           }

         } 

       }

     }

-  

+

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

+      Contract.Assert(formals != null);

+      Contract.Assert(values != null);

+      Contract.Assert(formals.Count == values.Count);

+      Dictionary<IVariable, Expression/*!*/> substMap = new Dictionary<IVariable, Expression>();

+      Dictionary<TypeParameter, Type> typeMap = new Dictionary<TypeParameter, Type>();

+

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

+        substMap.Add(formals[i], values[i]);

+      }

+

+      Translator.Substituter sub = new Translator.Substituter(f_this, substMap, typeMap, null);

+      return sub.Substitute(e);

+    }

+

     public void addAutoReqToolTipInfo(string label, Function f, List<Expression> reqs) {

       string prefix = "auto requires " + label + " ";

       string tip = "";

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 41cd8b02..81c15b1f 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -2083,7 +2083,7 @@ Execution trace:
     (0,0): anon0

     (0,0): anon11_Then

 

-Dafny program verifier finished with 49 verified, 8 errors

+Dafny program verifier finished with 52 verified, 8 errors

 

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

 

diff --git a/Test/dafny0/AutoReq.dfy b/Test/dafny0/AutoReq.dfy
index 0936176f..08acfc50 100644
--- a/Test/dafny0/AutoReq.dfy
+++ b/Test/dafny0/AutoReq.dfy
@@ -297,3 +297,17 @@ module StaticTest {
         EvenDoubler(y)

     }

 }

+

+module OpaqueTest {

+    static function bar(x:int) : int

+           requires x>7;

+    {

+           x-2

+    }

+

+    static function {:autoReq} {:opaque} foo(x:int) : int

+    {

+           bar(x)

+    }

+

+}