From ff2f900bee074610048d82aa1c7d0fd394a5f46e Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Thu, 17 Oct 2024 22:49:44 +0200 Subject: [PATCH] Merging heaps early, fixing optional consumed heaps returned, fixing some problems where we had too much permission on the heap --- src/main/scala/rules/Consumer.scala | 4 +-- .../scala/rules/QuantifiedChunkSupport.scala | 9 ++++--- .../chunks/MoreCompleteExhaleSupporter.scala | 25 +++++++++++++------ src/test/resources/kinduct/basic.vpr | 23 +++++++++++++++++ src/test/resources/kinduct/forceQP/basic.vpr | 24 ++++++++++++++++++ 5 files changed, 72 insertions(+), 13 deletions(-) diff --git a/src/main/scala/rules/Consumer.scala b/src/main/scala/rules/Consumer.scala index 5255db5d..3f81501d 100644 --- a/src/main/scala/rules/Consumer.scala +++ b/src/main/scala/rules/Consumer.scala @@ -125,8 +125,8 @@ object consumer extends ConsumptionRules { else wrappedConsumeTlc(s, h, a, pve, v)((s1, h1, cHeap, snap1, v1) => consumeTlcs(s1, h1, tlcs.tail, pves.tail, v1)((s2, h2, cHeap2, snap2, v2) => { - val combined = cHeap + cHeap2 - Q(s2, h2, combined, Combine(snap1, snap2), v2)})) + val (fr3, combined) = v2.stateConsolidator(s2).merge(s2.functionRecorder, cHeap, cHeap2, v2) + Q(s2.copy(functionRecorder = fr3), h2, combined, Combine(snap1, snap2), v2)})) } } diff --git a/src/main/scala/rules/QuantifiedChunkSupport.scala b/src/main/scala/rules/QuantifiedChunkSupport.scala index 1c9f6098..f87812d2 100644 --- a/src/main/scala/rules/QuantifiedChunkSupport.scala +++ b/src/main/scala/rules/QuantifiedChunkSupport.scala @@ -1320,7 +1320,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { magicWandSupporter.consumeFromMultipleHeaps(s, heaps, permissions, failure, Seq(), v)( consumeSingleFromOneOfMultipleHeaps(identifier, codomainQVars, arguments, resource, chunkOrderHeuristics) )((s1, hs1, cHeap1, optChunks, v1) => { - val newTopHeap = hs1.head + cHeap1 + //val newTopHeap = hs1.head + cHeap1 val totalConsumedAmount = cHeap1.values.foldLeft(NoPerm: Term)((q, ch) => PermPlus(q, ch.asInstanceOf[GeneralChunk].perm)) val totalConsumedFromFirst = if (optChunks.length > 0 && optChunks.head.nonEmpty) { PermMin(optChunks.head.get.asInstanceOf[QuantifiedBasicChunk].perm, totalConsumedAmount) @@ -1332,9 +1332,12 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { val nonEmptyChunks = optChunks.filter(_.isDefined) val cHeap2 = if (nonEmptyChunks.isEmpty) Heap() else Heap(Seq(nonEmptyChunks.head.get.asInstanceOf[QuantifiedBasicChunk].withPerm(totalConsumedFromAllButFirst))) - val newTopHeap2 = if (nonEmptyChunks.isEmpty) s.h else s.h + cHeap2 + val (fr2, newTopHeap2) = if (nonEmptyChunks.isEmpty) + (s1.functionRecorder, s.h) + else + v1.stateConsolidator(s1).merge(s1.functionRecorder, s.h, cHeap2, v1) - val s1p = s1.copy(loopHeapStack = hs1.tail, h = newTopHeap2) + val s1p = s1.copy(loopHeapStack = hs1.tail, h = newTopHeap2, functionRecorder = fr2) if (nonEmptyChunks.isEmpty) { assert(v1.decider.checkSmoke(true)) Success() diff --git a/src/main/scala/rules/chunks/MoreCompleteExhaleSupporter.scala b/src/main/scala/rules/chunks/MoreCompleteExhaleSupporter.scala index 09dfaaae..31fd36d7 100644 --- a/src/main/scala/rules/chunks/MoreCompleteExhaleSupporter.scala +++ b/src/main/scala/rules/chunks/MoreCompleteExhaleSupporter.scala @@ -242,8 +242,9 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { } magicWandSupporter.consumeFromMultipleHeaps(s, heaps, perms, failure, Seq(), v)(consumeSingle)((s1, hs1, cHeap1, optChunks, v1) => { - val newTopHeap = hs1.head + cHeap1 - val totalConsumedAmount = cHeap1.values.foldLeft(NoPerm: Term)((q, ch) => PermPlus(q, ch.asInstanceOf[GeneralChunk].perm)) + //val (fr1, newTopHeap) = v1.stateConsolidator(s1).merge(s1.functionRecorder, s1.h, cHeap1, v1) + //val (fr1, newTopHeap) = (s1.functionRecorder, s1.h + cHeap1) + val totalConsumedAmount = perms val totalConsumedFromFirst = if (optChunks.length > 0 && optChunks.head.nonEmpty) { PermMin(optChunks.head.get.asInstanceOf[NonQuantifiedChunk].perm, totalConsumedAmount) } else { @@ -253,10 +254,16 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { val nonEmptyChunks = optChunks.filter(_.isDefined) - val cHeap2 = if (nonEmptyChunks.isEmpty) Heap() else Heap(Seq(nonEmptyChunks.head.get.asInstanceOf[NonQuantifiedChunk].withPerm(totalConsumedFromAllButFirst))) - val newTopHeap2 = if (nonEmptyChunks.isEmpty) s.h else s.h + cHeap2 - - val s1p = s1.copy(loopHeapStack = hs1.tail, h = newTopHeap2) + val cHeap2 = if (nonEmptyChunks.isEmpty) + Heap() + else + Heap(Seq(nonEmptyChunks.head.get.asInstanceOf[NonQuantifiedChunk].withPerm(totalConsumedFromAllButFirst))) + val (fr1, newTopHeap2) = if (nonEmptyChunks.isEmpty) + (s1.functionRecorder, s1.h) + else + v1.stateConsolidator(s1).merge(s1.functionRecorder,s1.h, cHeap2, v1) + + val s1p = s1.copy(loopHeapStack = hs1.tail, h = newTopHeap2, functionRecorder = fr1) if (nonEmptyChunks.isEmpty){ assert(v1.decider.checkSmoke(true)) Success() @@ -288,7 +295,8 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { val snap = v.decider.fresh(snapSort) val ch = BasicChunk(FieldID, identifier, args, snap, gain) chunkSupporter.produce(s, h, ch, v)((s2, h2, v2) => { - doActualConsumeComplete(s2.copy(h = s2.h + ch), h2, resource, args, perms, ve, v2)(Q) + val (fr3, s3h) = v2.stateConsolidator(s2).merge(s2.functionRecorder, s2.h, ch, v2) + doActualConsumeComplete(s2.copy(h = s3h, functionRecorder = fr3), h2, resource, args, perms, ve, v2)(Q) }) } } else { @@ -426,7 +434,8 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { //Q(s1, newHeap, consumedHeap, Some(condSnap), v1) Success() case false => - result = (Incomplete(pNeeded), s1, newHeap, consumedHeap, None) + val consumedChunk = if (consumedChunks.isEmpty) None else Some(consumedChunks.head.withSnap(condSnap).withPerm(PermMinus(perms, pNeeded))) + result = (Incomplete(pNeeded), s1, newHeap, consumedHeap, consumedChunk) //Q(s1, newHeap, consumedHeap, Some(condSnap), v1) Success() } diff --git a/src/test/resources/kinduct/basic.vpr b/src/test/resources/kinduct/basic.vpr index 13a7ad93..9f15a982 100644 --- a/src/test/resources/kinduct/basic.vpr +++ b/src/test/resources/kinduct/basic.vpr @@ -233,6 +233,29 @@ method mFrame4(r: Ref) } +method mFrame4af(r: Ref) + requires acc(r.f) && acc(r.g) +{ + var b: Bool + b := havocBool() + r.f := 1 + while (b) + invariant r.f == 1 + { + assert acc(r.f) + //:: ExpectedOutput(assert.failed:assertion.false) + assert false + var tmp: Bool + tmp := havocBool() + if (tmp) + { + r.g := r.g + } + b := havocBool() + } + +} + method mFrame5(r: Ref) requires acc(r.f) && acc(r.g) { diff --git a/src/test/resources/kinduct/forceQP/basic.vpr b/src/test/resources/kinduct/forceQP/basic.vpr index 9c9db6ee..8f188653 100644 --- a/src/test/resources/kinduct/forceQP/basic.vpr +++ b/src/test/resources/kinduct/forceQP/basic.vpr @@ -254,6 +254,30 @@ method mFrame4(r: Ref) } +method mFrame4af(r: Ref) + requires acc(r.f) && acc(r.g) +{ + forceQPs() + var b: Bool + b := havocBool() + r.f := 1 + while (b) + invariant r.f == 1 + { + assert acc(r.f) + //:: ExpectedOutput(assert.failed:assertion.false) + assert false + var tmp: Bool + tmp := havocBool() + if (tmp) + { + r.g := r.g + } + b := havocBool() + } + +} + method mFrame5(r: Ref) requires acc(r.f) && acc(r.g) {