From 91fa6b7d576a111f39cde20de5d8e612b4d712b5 Mon Sep 17 00:00:00 2001 From: leino Date: Thu, 25 Jun 2015 18:12:53 -0700 Subject: 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). --- Binaries/DafnyPrelude.bpl | 3 ++- Source/Dafny/Translator.cs | 29 +++++++++++++++++++---------- Test/VSI-Benchmarks/b3.dfy | 10 ++++++++-- Test/VerifyThis2015/Problem3.dfy | 2 +- 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(H:Heap, r:ref, f:Field alpha): alpha { H[r, function {:inline true} update(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 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 { /// /// 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 { alpha }, new List { 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 { heapSucc, F1 }); + var tr = new Bpl.Trigger(f.tok, true, new List { 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/*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/*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 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 -- cgit v1.2.3