Tried to reduce frame-axiom instantiations by saying the earlier heap must be a "heap anchor".

Currently, a heap is an anchor if it produced by a havoc (but not a direct update).

4 files changed, 30 insertions, 14 deletions

diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index ef6106e0..dbf9b76c 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -398,7 +398,8 @@ function {:inline true} read<alpha>(H:Heap, r:ref, f:Field alpha): alpha { H[r,
 function {:inline true} update<alpha>(H:Heap, r:ref, f:Field alpha, v:alpha): Heap { H[r,f := v] }

 

 function $IsGoodHeap(Heap): bool;

-var $Heap: Heap where $IsGoodHeap($Heap);

+function $IsHeapAnchor(Heap): bool;

+var $Heap: Heap where $IsGoodHeap($Heap) && $IsHeapAnchor($Heap);

 

 function $HeapSucc(Heap, Heap): bool;

 axiom (forall<alpha> h: Heap, r: ref, f: Field alpha, x: alpha :: { update(h, r, f, x) }

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 90d0b11c..4324b2b8 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -1761,7 +1761,7 @@ namespace Microsoft.Dafny {
       var oih = new Bpl.IdentifierExpr(iter.tok, "$_OldIterHeap", predef.HeapType);

       Bpl.Expr wh = BplAnd(

         FunctionCall(iter.tok, BuiltinFunction.IsGoodHeap, null, oih),

-        FunctionCall(iter.tok, BuiltinFunction.HeapSucc, null, oih, etran.HeapExpr));

+        HeapSucc(oih, etran.HeapExpr));

       localVariables.Add(new Bpl.LocalVariable(iter.tok, new Bpl.TypedIdent(iter.tok, "$_OldIterHeap", predef.HeapType, wh)));

 

       // do an initial YieldHavoc

@@ -3692,9 +3692,9 @@ namespace Microsoft.Dafny {
     /// <summary>

     /// Generates:

     ///   axiom (forall s, h0: HeapType, h1: HeapType, formals... ::

-    ///        { HeapSucc(h0,h1), F(s,h1,formals) }

+    ///        { IsHeapAnchor(h0), HeapSucc(h0,h1), F(s,h1,formals) }

     ///        heaps are well-formed and formals are allocated AND

-    ///        HeapSucc(h0,h1)

+    ///        IsHeapAnchor(h0) AND HeapSucc(h0,h1)

     ///        AND

     ///        (forall(alpha) o: ref, f: Field alpha ::

     ///            o != null AND h0[o,alloc] AND h1[o,alloc] AND

@@ -3813,7 +3813,8 @@ namespace Microsoft.Dafny {
         Bpl.Expr oNotNullAlloced = Bpl.Expr.And(oNotNull, Bpl.Expr.And(etran0.IsAlloced(f.tok, o), etran1.IsAlloced(f.tok, o)));

         Bpl.Expr unchanged = Bpl.Expr.Eq(ReadHeap(f.tok, h0, o, field), ReadHeap(f.tok, h1, o, field));

 

-        Bpl.Expr heapSucc = FunctionCall(f.tok, BuiltinFunction.HeapSucc, null, h0, h1);

+        Bpl.Expr h0IsHeapAnchor = FunctionCall(h0.tok, BuiltinFunction.IsHeapAnchor, null, h0);

+        Bpl.Expr heapSucc = HeapSucc(h0, h1);

         Bpl.Expr r0 = InRWClause(f.tok, o, field, f.Reads, etran0, null, null);

         Bpl.Expr q0 = new Bpl.ForallExpr(f.tok, new List<TypeVariable> { alpha }, new List<Variable> { oVar, fieldVar },

           Bpl.Expr.Imp(Bpl.Expr.And(oNotNullAlloced, r0), unchanged));

@@ -3873,11 +3874,11 @@ namespace Microsoft.Dafny {
         var F0 = new Bpl.NAryExpr(f.tok, fn, f0args);

         var F1 = new Bpl.NAryExpr(f.tok, fn, f1args);

         var eq = Bpl.Expr.Eq(F0, F1);

-        var tr = new Bpl.Trigger(f.tok, true, new List<Bpl.Expr> { heapSucc, F1 });

+        var tr = new Bpl.Trigger(f.tok, true, new List<Bpl.Expr> { h0IsHeapAnchor, heapSucc, F1 });

 

         var typeParams = TrTypeParamDecls(f.TypeArgs);

         var ax = new Bpl.ForallExpr(f.tok, typeParams, bvars, null, tr,

-          Bpl.Expr.Imp(Bpl.Expr.And(wellFormed, heapSucc),

+          Bpl.Expr.Imp(Bpl.Expr.And(wellFormed, Bpl.Expr.And(h0IsHeapAnchor, heapSucc)),

           Bpl.Expr.Imp(q0, eq)));

         sink.AddTopLevelDeclaration(new Bpl.Axiom(f.tok, ax, comment));

 #endif

@@ -5829,7 +5830,7 @@ namespace Microsoft.Dafny {
 

           var h0 = BplBoundVar("h0", predef.HeapType, bvars);

           var h1 = BplBoundVar("h1", predef.HeapType, bvars);

-          var heapSucc = FunctionCall(tok, BuiltinFunction.HeapSucc, null, h0, h1);

+          var heapSucc = HeapSucc(h0, h1);

           var goodHeaps = BplAnd(

             FunctionCall(tok, BuiltinFunction.IsGoodHeap, null, h0),

             FunctionCall(tok, BuiltinFunction.IsGoodHeap, null, h1));

@@ -6683,7 +6684,7 @@ namespace Microsoft.Dafny {
         // the frame condition, which is free since it is checked with every heap update and call

         boilerplate.Add(new BoilerplateTriple(tok, true, FrameCondition(tok, modifiesClause, isGhostContext, etranPre, etran, etranMod), null, "frame condition"));

         // HeapSucc(S1, S2) or HeapSuccGhost(S1, S2)

-        Bpl.Expr heapSucc = FunctionCall(tok, isGhostContext ? BuiltinFunction.HeapSuccGhost : BuiltinFunction.HeapSucc, null, etranPre.HeapExpr, etran.HeapExpr);

+        Bpl.Expr heapSucc = HeapSucc(etranPre.HeapExpr, etran.HeapExpr, isGhostContext);

         boilerplate.Add(new BoilerplateTriple(tok, true, heapSucc, null, "boilerplate"));

       }

       return boilerplate;

@@ -7316,7 +7317,7 @@ namespace Microsoft.Dafny {
           // havoc $Heap;

           builder.Add(new Bpl.HavocCmd(s.Tok, new List<Bpl.IdentifierExpr> { (Bpl.IdentifierExpr/*TODO: this cast is rather dubious*/)etran.HeapExpr }));

           // assume $HeapSucc(preModifyHeap, $Heap);   OR $HeapSuccGhost

-          builder.Add(new Bpl.AssumeCmd(s.Tok, FunctionCall(s.Tok, s.IsGhost ? BuiltinFunction.HeapSuccGhost : BuiltinFunction.HeapSucc, null, preModifyHeap, etran.HeapExpr)));

+          builder.Add(new Bpl.AssumeCmd(s.Tok, HeapSucc(preModifyHeap, etran.HeapExpr, s.IsGhost)));

           // assume nothing outside the frame was changed

           var etranPreLoop = new ExpressionTranslator(this, predef, preModifyHeap);

           var updatedFrameEtran = new ExpressionTranslator(etran, modifyFrameName);

@@ -7867,7 +7868,7 @@ namespace Microsoft.Dafny {
       var prevEtran = new ExpressionTranslator(this, predef, prevHeap);

       updater.Add(Bpl.Cmd.SimpleAssign(s.Tok, prevHeap, etran.HeapExpr));

       updater.Add(new Bpl.HavocCmd(s.Tok, new List<Bpl.IdentifierExpr> { (Bpl.IdentifierExpr/*TODO: this cast is rather dubious*/)etran.HeapExpr }));

-      updater.Add(new Bpl.AssumeCmd(s.Tok, FunctionCall(s.Tok, BuiltinFunction.HeapSucc, null, prevHeap, etran.HeapExpr)));

+      updater.Add(new Bpl.AssumeCmd(s.Tok, HeapSucc(prevHeap, etran.HeapExpr)));

 

       // Here comes:

       //   assume (forall<alpha> o: ref, f: Field alpha ::

@@ -11913,6 +11914,7 @@ namespace Microsoft.Dafny {
       IntToReal,

 

       IsGoodHeap,

+      IsHeapAnchor,

       HeapSucc,

       HeapSuccGhost,

 

@@ -12293,6 +12295,10 @@ namespace Microsoft.Dafny {
           Contract.Assert(args.Length == 1);

           Contract.Assert(typeInstantiation == null);

           return FunctionCall(tok, "$IsGoodHeap", Bpl.Type.Bool, args);

+        case BuiltinFunction.IsHeapAnchor:

+          Contract.Assert(args.Length == 1);

+          Contract.Assert(typeInstantiation == null);

+          return FunctionCall(tok, "$IsHeapAnchor", Bpl.Type.Bool, args);

         case BuiltinFunction.HeapSucc:

           Contract.Assert(args.Length == 2);

           Contract.Assert(typeInstantiation == null);

@@ -14131,6 +14137,9 @@ namespace Microsoft.Dafny {
         Bpl.Expr.Eq(oldHeap, newHeap),

         FunctionCall(newHeap.tok, BuiltinFunction.HeapSucc, null, oldHeap, newHeap));

     }

+    Bpl.Expr HeapSucc(Bpl.Expr oldHeap, Bpl.Expr newHeap, bool useGhostHeapSucc = false) {

+      return FunctionCall(newHeap.tok, useGhostHeapSucc ? BuiltinFunction.HeapSuccGhost : BuiltinFunction.HeapSucc, null, oldHeap, newHeap);

+    }

 

     // Bpl-making-utilities

 

diff --git a/Test/VSI-Benchmarks/b3.dfy b/Test/VSI-Benchmarks/b3.dfy
index f59b0c3e..d47c4d4d 100644
--- a/Test/VSI-Benchmarks/b3.dfy
+++ b/Test/VSI-Benchmarks/b3.dfy
@@ -96,7 +96,7 @@ class Benchmark3 {
       if x < m { k := j; m := x; }

       j := j+1;

     }

-    

+

     j := 0;

     while j < k

       invariant j <= k;

@@ -108,10 +108,16 @@ class Benchmark3 {
       RotationLemma(old(q.contents), j, qc0, q.contents);

       j := j+1;

     }

-  

+

     assert j == k;  

     assert q.contents == old(q.contents)[k..] + old(q.contents)[..k];

+    ghost var qq := q.contents;

     m := q.Dequeue();

+    assert q.contents == qq[1..] && m == qq[0];

+    assert [m] + q.contents == qq;

+    assert |old(q.contents)| == |q.contents| + 1;

+

+    assert q.contents == old(q.contents)[k+1..] + old(q.contents)[..k];  

   }

 

   lemma RotationLemma(O: seq, j: nat, A: seq, C: seq)

diff --git a/Test/VerifyThis2015/Problem3.dfy b/Test/VerifyThis2015/Problem3.dfy
index 4205035d..10ad2d3a 100644
--- a/Test/VerifyThis2015/Problem3.dfy
+++ b/Test/VerifyThis2015/Problem3.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" /vcsMaxKeepGoingSplits:5 "%s" > "%t"

+// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

 // RUN: %diff "%s.expect" "%t"

 

 // Rustan Leino