From a932f79bf7ec02c56509af5c02ae9b6d78a97c27 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Thu, 26 Sep 2024 21:01:15 +0200 Subject: [PATCH 1/9] asserting (a) in e --- src/main/scala/rules/Evaluator.scala | 5 +++++ .../functions/HeapAccessReplacingExpressionTranslator.scala | 1 + 2 files changed, 6 insertions(+) diff --git a/src/main/scala/rules/Evaluator.scala b/src/main/scala/rules/Evaluator.scala index 943002243..11046c651 100644 --- a/src/main/scala/rules/Evaluator.scala +++ b/src/main/scala/rules/Evaluator.scala @@ -1029,6 +1029,11 @@ object evaluator extends EvaluationRules { Option.when(withExp)(s.relevantQuantifiedVariables.map(_._2.get)), v))((s4, r4, v4) => Q(s4, r4._1, r4._2, v4)) + case ast.Asserting(eAss, eIn) => + consume(s, eAss, pve, v)((_, _, _) => { + eval(s, eIn, pve, v)(Q) + }) + /* Sequences */ case ast.SeqContains(e0, e1) => evalBinOp(s, e1, e0, SeqIn, pve, v)((s1, t, e1New, e0New, v1) => diff --git a/src/main/scala/supporters/functions/HeapAccessReplacingExpressionTranslator.scala b/src/main/scala/supporters/functions/HeapAccessReplacingExpressionTranslator.scala index 02dd6d9f0..4b70d2140 100644 --- a/src/main/scala/supporters/functions/HeapAccessReplacingExpressionTranslator.scala +++ b/src/main/scala/supporters/functions/HeapAccessReplacingExpressionTranslator.scala @@ -128,6 +128,7 @@ class HeapAccessReplacingExpressionTranslator(symbolConverter: SymbolConverter, case loc: ast.LocationAccess => getOrFail(data.locToSnap, loc, toSort(loc.typ), Option.when(Verifier.config.enableDebugging())(extractPTypeFromExp(loc))) case ast.Unfolding(_, eIn) => translate(toSort)(eIn) case ast.Applying(_, eIn) => translate(toSort)(eIn) + case ast.Asserting(_, eIn) => translate(toSort)(eIn) case eFApp: ast.FuncApp => val silverFunc = program.findFunction(eFApp.funcname) From 562b9fe3b90f5b55c5cd3da0ee3b540227cef52d Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Fri, 27 Sep 2024 10:55:12 +0200 Subject: [PATCH 2/9] Update silver --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index 10b1b26a2..f649c0baf 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 10b1b26a20957e5f000bf1bbcd4017145148afd7 +Subproject commit f649c0baf2fc133a5d99261dbb567b8a33732588 From 52f94d26e9d66693e28fa7489368b5ee350accec Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Fri, 4 Oct 2024 13:32:13 +0200 Subject: [PATCH 3/9] Resetting heap instead of throwing away entire state after checking assertion --- src/main/scala/rules/Evaluator.scala | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/main/scala/rules/Evaluator.scala b/src/main/scala/rules/Evaluator.scala index 11046c651..b0d116432 100644 --- a/src/main/scala/rules/Evaluator.scala +++ b/src/main/scala/rules/Evaluator.scala @@ -1030,8 +1030,9 @@ object evaluator extends EvaluationRules { => Q(s4, r4._1, r4._2, v4)) case ast.Asserting(eAss, eIn) => - consume(s, eAss, pve, v)((_, _, _) => { - eval(s, eIn, pve, v)(Q) + consume(s, eAss, pve, v)((s2, _, v2) => { + val s3 = s2.copy(g = s.g, h = s.h) + eval(s3, eIn, pve, v2)(Q) }) /* Sequences */ From c9832ebd495a1e17d6e249ad4ee43ec8b6f1a9a7 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Tue, 15 Oct 2024 15:55:16 +0200 Subject: [PATCH 4/9] Fixing issue #862 --- silver | 2 +- src/main/scala/rules/Evaluator.scala | 2 +- src/main/scala/state/State.scala | 10 ++++++++-- 3 files changed, 10 insertions(+), 4 deletions(-) diff --git a/silver b/silver index 10b1b26a2..f4a8d5a73 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 10b1b26a20957e5f000bf1bbcd4017145148afd7 +Subproject commit f4a8d5a73e9a823db4247d9d94004ec1133704d7 diff --git a/src/main/scala/rules/Evaluator.scala b/src/main/scala/rules/Evaluator.scala index 943002243..0570c926c 100644 --- a/src/main/scala/rules/Evaluator.scala +++ b/src/main/scala/rules/Evaluator.scala @@ -1678,7 +1678,7 @@ object evaluator extends EvaluationRules { Option.when(withExp)(ast.Implies(BigAnd(entry.pathConditions.branchConditionExps.map(bc => bc._2.get)), ast.EqCmp(joinExp.get, entry.data._2.get)())()))) - var sJoined = entries.tail.foldLeft(entries.head.s)((sAcc, entry) =>sAcc.merge(entry.s)) + var sJoined = entries.tail.foldLeft(entries.head.s)((sAcc, entry) => sAcc.merge(entry.s)) sJoined = sJoined.copy(functionRecorder = sJoined.functionRecorder.recordPathSymbol(joinSymbol)) joinDefEqs foreach { case (t, exp, expNew) => v.decider.assume(t, exp, expNew)} diff --git a/src/main/scala/state/State.scala b/src/main/scala/state/State.scala index 25f9e5fdd..141adc9ce 100644 --- a/src/main/scala/state/State.scala +++ b/src/main/scala/state/State.scala @@ -196,7 +196,7 @@ object State { triggerExp2, `partiallyConsumedHeap1`, `permissionScalingFactor1`, `permissionScalingFactorExp1`, `isEvalInOld`, - `reserveHeaps1`, `reserveCfgs1`, `conservedPcs1`, `recordPcs1`, `exhaleExt1`, + `reserveHeaps1`, `reserveCfgs1`, conservedPcs2, `recordPcs1`, `exhaleExt1`, ssCache2, `hackIssue387DisablePermissionConsumption1`, `qpFields1`, `qpPredicates1`, `qpMagicWands1`, `permResources1`, smCache2, pmCache2, `smDomainNeeded1`, `predicateSnapMap1`, `predicateFormalVarMap1`, `retryLevel`, `useHeapTriggers`, @@ -214,6 +214,11 @@ object State { val ssCache3 = ssCache1 ++ ssCache2 val moreCompleteExhale3 = moreCompleteExhale || moreCompleteExhale2 + assert(conservedPcs1.length == conservedPcs2.length) + val conservedPcs3 = conservedPcs1 + .zip(conservedPcs1) + .map({ case (pcs1, pcs2) => (pcs1 ++ pcs2).distinct }) + s1.copy(functionRecorder = functionRecorder3, possibleTriggers = possibleTriggers3, triggerExp = triggerExp3, @@ -222,7 +227,8 @@ object State { ssCache = ssCache3, smCache = smCache3, pmCache = pmCache3, - moreCompleteExhale = moreCompleteExhale3) + moreCompleteExhale = moreCompleteExhale3, + conservedPcs = conservedPcs3) case _ => val err = new StringBuilder() From e71774ce9f77c26e15ba5a26e79059b2b35d72c9 Mon Sep 17 00:00:00 2001 From: Dspil Date: Wed, 16 Oct 2024 06:02:51 +0000 Subject: [PATCH 5/9] Updates submodules --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index f4a8d5a73..10b1b26a2 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit f4a8d5a73e9a823db4247d9d94004ec1133704d7 +Subproject commit 10b1b26a20957e5f000bf1bbcd4017145148afd7 From 26091b7f6101827bb4235565daf6875aa1bc3f7f Mon Sep 17 00:00:00 2001 From: Silver Bot Date: Wed, 13 Nov 2024 15:52:29 +0000 Subject: [PATCH 6/9] Update silver submodule --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index 10b1b26a2..5611fcbd1 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 10b1b26a20957e5f000bf1bbcd4017145148afd7 +Subproject commit 5611fcbd13209be062344a26c0cbdbb3a728c92a From 2257d9c029d368629ed1f831c3c959713b1d1d10 Mon Sep 17 00:00:00 2001 From: Silver Bot Date: Wed, 13 Nov 2024 18:51:51 +0000 Subject: [PATCH 7/9] Update silver submodule --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index 5f5c02202..08c001b33 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 5f5c02202030b67c0cf90d8540d26ca3d71c9bd6 +Subproject commit 08c001b33decce0b16e698be862d7904c7282a99 From 761d4dd71f0a555b7d03e250d3eabd5536b01afb Mon Sep 17 00:00:00 2001 From: Markus Limbeck <92801626+mlimbeck@users.noreply.github.com> Date: Fri, 29 Nov 2024 16:35:46 +0100 Subject: [PATCH 8/9] Optional Snapshot Generation in Consume (#879) --- src/main/scala/rules/ChunkSupporter.scala | 28 ++-- src/main/scala/rules/Consumer.scala | 113 ++++++++------ src/main/scala/rules/Evaluator.scala | 14 +- src/main/scala/rules/Executor.scala | 16 +- src/main/scala/rules/MagicWandSupporter.scala | 20 +-- .../rules/MoreCompleteExhaleSupporter.scala | 138 +++++++++++++----- src/main/scala/rules/PredicateSupporter.scala | 19 +-- .../scala/rules/QuantifiedChunkSupport.scala | 79 +++++----- src/main/scala/state/package.scala | 2 +- .../scala/supporters/MethodSupporter.scala | 2 +- .../functions/FunctionVerificationUnit.scala | 2 +- 11 files changed, 269 insertions(+), 164 deletions(-) diff --git a/src/main/scala/rules/ChunkSupporter.scala b/src/main/scala/rules/ChunkSupporter.scala index 311063b26..35ff5eb60 100644 --- a/src/main/scala/rules/ChunkSupporter.scala +++ b/src/main/scala/rules/ChunkSupporter.scala @@ -29,10 +29,11 @@ trait ChunkSupportRules extends SymbolicExecutionRules { argsExp: Option[Seq[ast.Exp]], perms: Term, permsExp: Option[ast.Exp], + returnSnap: Boolean, ve: VerificationError, v: Verifier, description: String) - (Q: (State, Heap, Term, Verifier) => VerificationResult) + (Q: (State, Heap, Option[Term], Verifier) => VerificationResult) : VerificationResult def produce(s: State, h: Heap, ch: NonQuantifiedChunk, v: Verifier) @@ -71,17 +72,18 @@ object chunkSupporter extends ChunkSupportRules { argsExp: Option[Seq[ast.Exp]], perms: Term, permsExp: Option[ast.Exp], + returnSnap: Boolean, ve: VerificationError, v: Verifier, description: String) - (Q: (State, Heap, Term, Verifier) => VerificationResult) + (Q: (State, Heap, Option[Term], Verifier) => VerificationResult) : VerificationResult = { - consume2(s, h, resource, args, argsExp, perms, permsExp, ve, v)((s2, h2, optSnap, v2) => + consume2(s, h, resource, args, argsExp, perms, permsExp, returnSnap, ve, v)((s2, h2, optSnap, v2) => optSnap match { case Some(snap) => - Q(s2, h2, snap.convert(sorts.Snap), v2) - case None => + Q(s2, h2, Some(snap.convert(sorts.Snap)), v2) + case None if returnSnap => /* Not having consumed anything could mean that we are in an infeasible * branch, or that the permission amount to consume was zero. * @@ -91,7 +93,8 @@ object chunkSupporter extends ChunkSupportRules { */ val fresh = v2.decider.fresh(sorts.Snap, Option.when(withExp)(PUnknown())) val s3 = s2.copy(functionRecorder = s2.functionRecorder.recordFreshSnapshot(fresh.applicable)) - Q(s3, h2, fresh, v2) + Q(s3, h2, Some(fresh), v2) + case None => Q(s2, h2, None, v2) }) } @@ -102,6 +105,7 @@ object chunkSupporter extends ChunkSupportRules { argsExp: Option[Seq[ast.Exp]], perms: Term, permsExp: Option[ast.Exp], + returnSnap: Boolean, ve: VerificationError, v: Verifier) (Q: (State, Heap, Option[Term], Verifier) => VerificationResult) @@ -111,24 +115,28 @@ object chunkSupporter extends ChunkSupportRules { if (s.exhaleExt) { val failure = createFailure(ve, v, s, "chunk consume in package") magicWandSupporter.transfer(s, perms, permsExp, failure, Seq(), v)(consumeGreedy(_, _, id, args, _, _, _))((s1, optCh, v1) => - Q(s1, h, optCh.flatMap(ch => Some(ch.snap)), v1)) + if (returnSnap){ + Q(s1, h, optCh.flatMap(ch => Some(ch.snap)), v1) + } else { + Q(s1, h, None, v1) + }) } else { executionFlowController.tryOrFail2[Heap, Option[Term]](s.copy(h = h), v)((s1, v1, QS) => if (s1.moreCompleteExhale) { - moreCompleteExhaleSupporter.consumeComplete(s1, s1.h, resource, args, argsExp, perms, permsExp, ve, v1)((s2, h2, snap2, v2) => { + moreCompleteExhaleSupporter.consumeComplete(s1, s1.h, resource, args, argsExp, perms, permsExp, returnSnap, ve, v1)((s2, h2, snap2, v2) => { QS(s2.copy(h = s.h), h2, snap2, v2) }) } else { consumeGreedy(s1, s1.h, id, args, perms, permsExp, v1) match { case (Complete(), s2, h2, optCh2) => val snap = optCh2 match { - case None => None - case Some(ch) => + case Some(ch) if returnSnap => if (v1.decider.check(IsPositive(perms), Verifier.config.checkTimeout())) { Some(ch.snap) } else { Some(Ite(IsPositive(perms), ch.snap.convert(sorts.Snap), Unit)) } + case _ => None } QS(s2.copy(h = s.h), h2, snap, v1) case _ if v1.decider.checkSmoke(true) => diff --git a/src/main/scala/rules/Consumer.scala b/src/main/scala/rules/Consumer.scala index 4041636ba..fd3e34b94 100644 --- a/src/main/scala/rules/Consumer.scala +++ b/src/main/scala/rules/Consumer.scala @@ -28,6 +28,7 @@ trait ConsumptionRules extends SymbolicExecutionRules { * * @param s The state to consume the assertion from. * @param a The assertion to consume. + * @param returnSnap Whether a snapshot should be returned or not. * @param pve The error to report in case the consumption fails. * @param v The verifier to use. * @param Q The continuation to invoke if the consumption succeeded, with the following @@ -36,8 +37,8 @@ trait ConsumptionRules extends SymbolicExecutionRules { * consumed partial heap. * @return The result of the continuation. */ - def consume(s: State, a: ast.Exp, pve: PartialVerificationError, v: Verifier) - (Q: (State, Term, Verifier) => VerificationResult) + def consume(s: State, a: ast.Exp, returnSnap: Boolean, pve: PartialVerificationError, v: Verifier) + (Q: (State, Option[Term], Verifier) => VerificationResult) : VerificationResult /** Subsequently consumes the assertions `as` (from head to tail), starting in state `s`. @@ -48,6 +49,7 @@ trait ConsumptionRules extends SymbolicExecutionRules { * * @param s The state to consume the assertions from. * @param as The assertions to consume. + * @param returnSnap Whether a snapshot should be returned or not. * @param pvef The error to report in case a consumption fails. Given assertions `as`, an error * `pvef(as_i)` will be reported if consuming assertion `as_i` fails. * @param v @see [[consume]] @@ -56,9 +58,10 @@ trait ConsumptionRules extends SymbolicExecutionRules { */ def consumes(s: State, as: Seq[ast.Exp], + returnSnap: Boolean, pvef: ast.Exp => PartialVerificationError, v: Verifier) - (Q: (State, Term, Verifier) => VerificationResult) + (Q: (State, Option[Term], Verifier) => VerificationResult) : VerificationResult } @@ -71,11 +74,11 @@ object consumer extends ConsumptionRules { */ /** @inheritdoc */ - def consume(s: State, a: ast.Exp, pve: PartialVerificationError, v: Verifier) - (Q: (State, Term, Verifier) => VerificationResult) + def consume(s: State, a: ast.Exp, returnSnap: Boolean, pve: PartialVerificationError, v: Verifier) + (Q: (State, Option[Term], Verifier) => VerificationResult) : VerificationResult = { - consumeR(s, s.h, a.whenExhaling, pve, v)((s1, h1, snap, v1) => { + consumeR(s, s.h, a.whenExhaling, returnSnap, pve, v)((s1, h1, snap, v1) => { val s2 = s1.copy(h = h1, partiallyConsumedHeap = s.partiallyConsumedHeap) Q(s2, snap, v1)}) @@ -84,9 +87,10 @@ object consumer extends ConsumptionRules { /** @inheritdoc */ def consumes(s: State, as: Seq[ast.Exp], + returnSnap: Boolean, pvef: ast.Exp => PartialVerificationError, v: Verifier) - (Q: (State, Term, Verifier) => VerificationResult) + (Q: (State, Option[Term], Verifier) => VerificationResult) : VerificationResult = { val allTlcs = mutable.ListBuffer[ast.Exp]() @@ -100,7 +104,7 @@ object consumer extends ConsumptionRules { allPves ++= pves }) - consumeTlcs(s, s.h, allTlcs.result(), allPves.result(), v)((s1, h1, snap1, v1) => { + consumeTlcs(s, s.h, allTlcs.result(), returnSnap, allPves.result(), v)((s1, h1, snap1, v1) => { val s2 = s1.copy(h = h1, partiallyConsumedHeap = s.partiallyConsumedHeap) Q(s2, snap1, v1) @@ -110,34 +114,41 @@ object consumer extends ConsumptionRules { private def consumeTlcs(s: State, h: Heap, tlcs: Seq[ast.Exp], + returnSnap: Boolean, pves: Seq[PartialVerificationError], v: Verifier) - (Q: (State, Heap, Term, Verifier) => VerificationResult) + (Q: (State, Heap, Option[Term], Verifier) => VerificationResult) : VerificationResult = { if (tlcs.isEmpty) - Q(s, h, Unit, v) + Q(s, h, if (returnSnap) Some(Unit) else None, v) else { val a = tlcs.head val pve = pves.head if (tlcs.tail.isEmpty) - wrappedConsumeTlc(s, h, a, pve, v)(Q) + wrappedConsumeTlc(s, h, a, returnSnap, pve, v)(Q) else - wrappedConsumeTlc(s, h, a, pve, v)((s1, h1, snap1, v1) => { - consumeTlcs(s1, h1, tlcs.tail, pves.tail, v1)((s2, h2, snap2, v2) => - Q(s2, h2, Combine(snap1, snap2), v2))}) + wrappedConsumeTlc(s, h, a, returnSnap, pve, v)((s1, h1, snap1, v1) => { + consumeTlcs(s1, h1, tlcs.tail, returnSnap, pves.tail, v1)((s2, h2, snap2, v2) => + + (snap1, snap2) match { + case (Some(sn1), Some(sn2)) if returnSnap => Q(s2, h2, Some(Combine(sn1, sn2)), v2) + case (None, None) if !returnSnap => Q(s2, h2, None, v2) + case (_, _) => sys.error(s"Consume returned unexpected snapshot: ${(returnSnap, (snap1, snap2))}") + }) + }) } } - private def consumeR(s: State, h: Heap, a: ast.Exp, pve: PartialVerificationError, v: Verifier) - (Q: (State, Heap, Term, Verifier) => VerificationResult) + private def consumeR(s: State, h: Heap, a: ast.Exp, returnSnap: Boolean, pve: PartialVerificationError, v: Verifier) + (Q: (State, Heap, Option[Term], Verifier) => VerificationResult) : VerificationResult = { val tlcs = a.topLevelConjuncts val pves = Seq.fill(tlcs.length)(pve) - consumeTlcs(s, h, tlcs, pves, v)(Q) + consumeTlcs(s, h, tlcs, returnSnap, pves, v)(Q) } /** Wrapper/decorator for consume that injects the following operations: @@ -147,9 +158,10 @@ object consumer extends ConsumptionRules { protected def wrappedConsumeTlc(s: State, h: Heap, a: ast.Exp, + returnSnap: Boolean, pve: PartialVerificationError, v: Verifier) - (Q: (State, Heap, Term, Verifier) => VerificationResult) + (Q: (State, Heap, Option[Term], Verifier) => VerificationResult) : VerificationResult = { /* tryOrFail effects the "main" heap s.h, so we temporarily set the consume-heap h to be the @@ -157,20 +169,20 @@ object consumer extends ConsumptionRules { * consume. */ val sInit = s.copy(h = h) - executionFlowController.tryOrFail2[Heap, Term](sInit, v)((s0, v1, QS) => { + executionFlowController.tryOrFail2[Heap, Option[Term]](sInit, v)((s0, v1, QS) => { val h0 = s0.h /* h0 is h, but potentially consolidated */ val s1 = s0.copy(h = s.h) /* s1 is s, but the retrying flag might be set */ val sepIdentifier = v1.symbExLog.openScope(new ConsumeRecord(a, s1, v.decider.pcs)) - consumeTlc(s1, h0, a, pve, v1)((s2, h2, snap2, v2) => { + consumeTlc(s1, h0, a, returnSnap, pve, v1)((s2, h2, snap2, v2) => { v2.symbExLog.closeScope(sepIdentifier) QS(s2, h2, snap2, v2)}) })(Q) } - private def consumeTlc(s: State, h: Heap, a: ast.Exp, pve: PartialVerificationError, v: Verifier) - (Q: (State, Heap, Term, Verifier) => VerificationResult) + private def consumeTlc(s: State, h: Heap, a: ast.Exp, returnSnap: Boolean, pve: PartialVerificationError, v: Verifier) + (Q: (State, Heap, Option[Term], Verifier) => VerificationResult) : VerificationResult = { /* ATTENTION: Expressions such as `perm(...)` must be evaluated in-place, @@ -190,7 +202,7 @@ object consumer extends ConsumptionRules { case imp @ ast.Implies(e0, a0) if !a.isPure && s.moreJoins.id >= JoinMode.Impure.id => val impliesRecord = new ImpliesRecord(imp, s, v.decider.pcs, "consume") val uidImplies = v.symbExLog.openScope(impliesRecord) - consumeConditionalTlcMoreJoins(s, h, e0, a0, None, uidImplies, pve, v)(Q) + consumeConditionalTlcMoreJoins(s, h, e0, a0, None, uidImplies, returnSnap, pve, v)(Q) case imp @ ast.Implies(e0, a0) if !a.isPure => val impliesRecord = new ImpliesRecord(imp, s, v.decider.pcs, "consume") @@ -198,19 +210,19 @@ object consumer extends ConsumptionRules { evaluator.eval(s, e0, pve, v)((s1, t0, e0New, v1) => branch(s1, t0, (e0, e0New), v1)( - (s2, v2) => consumeR(s2, h, a0, pve, v2)((s3, h1, t1, v3) => { + (s2, v2) => consumeR(s2, h, a0, returnSnap, pve, v2)((s3, h1, t1, v3) => { v3.symbExLog.closeScope(uidImplies) Q(s3, h1, t1, v3) }), (s2, v2) => { v2.symbExLog.closeScope(uidImplies) - Q(s2, h, Unit, v2) + Q(s2, h, if (returnSnap) Some(Unit) else None, v2) })) case ite @ ast.CondExp(e0, a1, a2) if !a.isPure && s.moreJoins.id >= JoinMode.Impure.id => val condExpRecord = new CondExpRecord(ite, s, v.decider.pcs, "consume") val uidCondExp = v.symbExLog.openScope(condExpRecord) - consumeConditionalTlcMoreJoins(s, h, e0, a1, Some(a2), uidCondExp, pve, v)(Q) + consumeConditionalTlcMoreJoins(s, h, e0, a1, Some(a2), uidCondExp, returnSnap, pve, v)(Q) case ite @ ast.CondExp(e0, a1, a2) if !a.isPure => val condExpRecord = new CondExpRecord(ite, s, v.decider.pcs, "consume") @@ -218,11 +230,11 @@ object consumer extends ConsumptionRules { eval(s, e0, pve, v)((s1, t0, e0New, v1) => branch(s1, t0, (e0, e0New), v1)( - (s2, v2) => consumeR(s2, h, a1, pve, v2)((s3, h1, t1, v3) => { + (s2, v2) => consumeR(s2, h, a1, returnSnap, pve, v2)((s3, h1, t1, v3) => { v3.symbExLog.closeScope(uidCondExp) Q(s3, h1, t1, v3) }), - (s2, v2) => consumeR(s2, h, a2, pve, v2)((s3, h1, t1, v3) => { + (s2, v2) => consumeR(s2, h, a2, returnSnap, pve, v2)((s3, h1, t1, v3) => { v3.symbExLog.closeScope(uidCondExp) Q(s3, h1, t1, v3) }))) @@ -260,12 +272,13 @@ object consumer extends ConsumptionRules { eArgs = permRcvrOpt.map(permRcvr => Seq(permRcvr(1))), tPerm = tPerm, ePerm = permRcvrOpt.map(_(0)), + returnSnap = returnSnap, pve = pve, negativePermissionReason = NegativePermission(acc.perm), notInjectiveReason = QPAssertionNotInjective(acc.loc), insufficientPermissionReason = InsufficientPermission(acc.loc), v1)(Q) - case (s1, _, _, _, _, None, v1) => Q(s1, h, True, v1) + case (s1, _, _, _, _, None, v1) => Q(s1, h, if (returnSnap) Some(Unit) else None, v1) } case QuantifiedPermissionAssertion(forall, cond, acc: ast.PredicateAccessPredicate) => @@ -305,12 +318,13 @@ object consumer extends ConsumptionRules { eArgs = permArgsNew.map(_.tail), tPerm = tPerm, ePerm = permArgsNew.map(_.head), + returnSnap = returnSnap, pve = pve, negativePermissionReason = NegativePermission(acc.perm), notInjectiveReason = QPAssertionNotInjective(acc.loc), insufficientPermissionReason = InsufficientPermission(acc.loc), v1)(Q) - case (s1, _, _, _, _, None, v1) => Q(s1, h, True, v1) + case (s1, _, _, _, _, None, v1) => Q(s1, h, if (returnSnap) Some(Unit) else None, v1) } case QuantifiedPermissionAssertion(forall, cond, wand: ast.MagicWand) => @@ -346,12 +360,13 @@ object consumer extends ConsumptionRules { eArgs = bodyVarsNew, tPerm = tPerm, ePerm = Option.when(withExp)(ePerm), + returnSnap = returnSnap, pve = pve, negativePermissionReason = NegativePermission(ePerm), notInjectiveReason = sys.error("Quantified wand not injective"), /*ReceiverNotInjective(...)*/ insufficientPermissionReason = MagicWandChunkNotFound(wand), /*InsufficientPermission(...)*/ v1)(Q) - case (s1, _, _, _, _, None, v1) => Q(s1, h, True, v1) + case (s1, _, _, _, _, None, v1) => Q(s1, h, if (returnSnap) Some(Unit) else None, v1) } case accPred@ast.AccessPredicate(loc @ ast.FieldAccess(eRcvr, field), ePerm) @@ -387,6 +402,7 @@ object consumer extends ConsumptionRules { loc, loss, lossExp, + returnSnap, None, pve, v2 @@ -431,6 +447,7 @@ object consumer extends ConsumptionRules { loc, loss, lossExp, + returnSnap, None, pve, v2 @@ -442,7 +459,7 @@ object consumer extends ConsumptionRules { case let: ast.Let if !let.isPure => letSupporter.handle[ast.Exp](s, let, pve, v)((s1, g1, body, v1) => { val s2 = s1.copy(g = s1.g + g1) - consumeR(s2, h, body, pve, v1)(Q)}) + consumeR(s2, h, body, returnSnap, pve, v1)(Q)}) case ast.AccessPredicate(locacc: ast.LocationAccess, perm) => eval(s, perm, pve, v)((s1, tPerm, permNew, v1) => @@ -456,7 +473,7 @@ object consumer extends ConsumptionRules { val lossExp = permNew.map(p => ast.PermMul(p, s3.permissionScalingFactorExp.get)(p.pos, p.info, p.errT)) val ve = pve dueTo InsufficientPermission(locacc) val description = s"consume ${a.pos}: $a" - chunkSupporter.consume(s3, h, resource, tArgs, eArgs, loss, lossExp, ve, v3, description)((s4, h1, snap1, v4) => { + chunkSupporter.consume(s3, h, resource, tArgs, eArgs, loss, lossExp, returnSnap, ve, v3, description)((s4, h1, snap1, v4) => { val s5 = s4.copy(partiallyConsumedHeap = Some(h1), constrainableARPs = s.constrainableARPs) Q(s5, h1, snap1, v4)})}))) @@ -496,6 +513,7 @@ object consumer extends ConsumptionRules { wand, loss, lossExp, + returnSnap, None, pve, v1 @@ -508,11 +526,11 @@ object consumer extends ConsumptionRules { magicWandSupporter.evaluateWandArguments(s, wand, pve, v)((s1, tArgs, eArgs, v1) => { val ve = pve dueTo MagicWandChunkNotFound(wand) val description = s"consume wand $wand" - chunkSupporter.consume(s1, h, wand, tArgs, eArgs, FullPerm, Option.when(withExp)(ast.FullPerm()(wand.pos, wand.info, wand.errT)), ve, v1, description)(Q) + chunkSupporter.consume(s1, h, wand, tArgs, eArgs, FullPerm, Option.when(withExp)(ast.FullPerm()(wand.pos, wand.info, wand.errT)), returnSnap, ve, v1, description)(Q) }) case _ => - evalAndAssert(s, a, pve, v)((s1, t, v1) => { + evalAndAssert(s, a, returnSnap, pve, v)((s1, t, v1) => { Q(s1, h, t, v1) }) } @@ -521,26 +539,27 @@ object consumer extends ConsumptionRules { } private def consumeConditionalTlcMoreJoins(s: State, h: Heap, e0: ast.Exp, a1: ast.Exp, a2: Option[ast.Exp], scopeUid: Int, + returnSnap: Boolean, pve: PartialVerificationError, v: Verifier) - (Q: (State, Heap, Term, Verifier) => VerificationResult) + (Q: (State, Heap, Option[Term], Verifier) => VerificationResult) : VerificationResult = { eval(s, e0, pve, v)((s1, t0, e0New, v1) => - joiner.join[(Heap, Term), (Heap, Term)](s1, v1, resetState = false)((s1, v1, QB) => { + joiner.join[(Heap, Option[Term]), (Heap, Option[Term])](s1, v1, resetState = false)((s1, v1, QB) => { branch(s1.copy(parallelizeBranches = false), t0, (e0, e0New), v1)( (s2, v2) => - consumeR(s2.copy(parallelizeBranches = s1.parallelizeBranches), h, a1, pve, v2)((s3, h1, t1, v3) => { + consumeR(s2.copy(parallelizeBranches = s1.parallelizeBranches), h, a1, returnSnap, pve, v2)((s3, h1, t1, v3) => { v3.symbExLog.closeScope(scopeUid) QB(s3, (h1, t1), v3) }), (s2, v2) => a2 match { - case Some(a2) => consumeR(s2.copy(parallelizeBranches = s1.parallelizeBranches), h, a2, pve, v2)((s3, h1, t1, v3) => { + case Some(a2) => consumeR(s2.copy(parallelizeBranches = s1.parallelizeBranches), h, a2, returnSnap, pve, v2)((s3, h1, t1, v3) => { v3.symbExLog.closeScope(scopeUid) QB(s3, (h1, t1), v3) }) case None => v2.symbExLog.closeScope(scopeUid) - QB(s2.copy(parallelizeBranches = s1.parallelizeBranches), (h, Unit), v2) + QB(s2.copy(parallelizeBranches = s1.parallelizeBranches), (h, if (returnSnap) Some(Unit) else None), v2) }) })(entries => { val s2 = entries match { @@ -552,8 +571,12 @@ object consumer extends ConsumptionRules { entry1.data._1, And(entry1.pathConditions.branchConditions), Option.when(withExp)(BigAnd(entry1.pathConditions.branchConditionExps.map(_._2.get))), entry2.data._1, And(entry2.pathConditions.branchConditions), Option.when(withExp)(BigAnd(entry2.pathConditions.branchConditionExps.map(_._2.get))), ), - // Asume that entry1.pcs is inverse of entry2.pcs - Ite(And(entry1.pathConditions.branchConditions), entry1.data._2, entry2.data._2) + // Assume that entry1.pcs is inverse of entry2.pcs + (entry1.data._2, entry2.data._2) match { + case (Some(t1), Some(t2)) if returnSnap => Some(Ite(And(entry1.pathConditions.branchConditions), t1, t2)) + case (None, None) if !returnSnap => None + case (_, _) => sys.error(s"Unexpected join data entries: $entries") + } ) (entry1.pathConditionAwareMergeWithoutConsolidation(entry2, v1), mergedData) case _ => @@ -567,8 +590,8 @@ object consumer extends ConsumptionRules { } - private def evalAndAssert(s: State, e: ast.Exp, pve: PartialVerificationError, v: Verifier) - (Q: (State, Term, Verifier) => VerificationResult) + private def evalAndAssert(s: State, e: ast.Exp, returnSnap: Boolean, pve: PartialVerificationError, v: Verifier) + (Q: (State, Option[Term], Verifier) => VerificationResult) : VerificationResult = { /* It is expected that the partially consumed heap (h in the above implementation of @@ -608,7 +631,7 @@ object consumer extends ConsumptionRules { val s5 = s4.copy(h = s.h, reserveHeaps = s.reserveHeaps, exhaleExt = s.exhaleExt) - Q(s5, Unit, v4) + Q(s5, if (returnSnap) Some(Unit) else None, v4) }) } } diff --git a/src/main/scala/rules/Evaluator.scala b/src/main/scala/rules/Evaluator.scala index 1b3e82e63..09c0e0120 100644 --- a/src/main/scala/rules/Evaluator.scala +++ b/src/main/scala/rules/Evaluator.scala @@ -919,8 +919,8 @@ object evaluator extends EvaluationRules { */ smDomainNeeded = true, moreJoins = JoinMode.Off) - consumes(s3, pres, _ => pvePre, v2)((s4, snap, v3) => { - val snap1 = snap.convert(sorts.Snap) + consumes(s3, pres, true, _ => pvePre, v2)((s4, snap, v3) => { + val snap1 = snap.get.convert(sorts.Snap) val preFApp = App(functionSupporter.preconditionVersion(v3.symbolConverter.toFunction(func)), snap1 :: tArgs) val preExp = Option.when(withExp)({ DebugExp.createInstance(Some(s"precondition of ${func.name}(${eArgsNew.get.mkString(", ")}) holds"), None, None, InsertionOrderedSet.empty) @@ -977,9 +977,9 @@ object evaluator extends EvaluationRules { // val c4 = c3.decCycleCounter(predicate) // eval(σ1, eIn, pve, c4)((tIn, c5) => // QB(tIn, c5))}) - consume(s4, acc, pve, v3)((s5, snap, v4) => { + consume(s4, acc, true, pve, v3)((s5, snap, v4) => { val fr6 = - s5.functionRecorder.recordSnapshot(pa, v4.decider.pcs.branchConditions, snap) + s5.functionRecorder.recordSnapshot(pa, v4.decider.pcs.branchConditions, snap.get) .changeDepthBy(+1) val s6 = s5.copy(functionRecorder = fr6, constrainableARPs = s1.constrainableARPs) @@ -992,14 +992,14 @@ object evaluator extends EvaluationRules { if (!Verifier.config.disableFunctionUnfoldTrigger()) { val eArgsString = eArgsNew.mkString(", ") val debugExp = Option.when(withExp)(DebugExp.createInstance(s"PredicateTrigger(${predicate.name}($eArgsString))", isInternal_ = true)) - v4.decider.assume(App(s.predicateData(predicate).triggerFunction, snap.convert(terms.sorts.Snap) +: tArgs), debugExp) + v4.decider.assume(App(s.predicateData(predicate).triggerFunction, snap.get.convert(terms.sorts.Snap) +: tArgs), debugExp) } val body = predicate.body.get /* Only non-abstract predicates can be unfolded */ val s7 = s6.scalePermissionFactor(tPerm, ePermNew) val argsPairs: List[(Term, Option[ast.Exp])] = if (withExp) tArgs zip eArgsNew.get.map(Some(_)) else tArgs zip Seq.fill(tArgs.size)(None) val insg = s7.g + Store(predicate.formalArgs map (_.localVar) zip argsPairs) val s7a = s7.copy(g = insg) - produce(s7a, toSf(snap), body, pve, v4)((s8, v5) => { + produce(s7a, toSf(snap.get), body, pve, v4)((s8, v5) => { val s9 = s8.copy(g = s7.g, functionRecorder = s8.functionRecorder.changeDepthBy(-1), recordVisited = s3.recordVisited, @@ -1030,7 +1030,7 @@ object evaluator extends EvaluationRules { => Q(s4, r4._1, r4._2, v4)) case ast.Asserting(eAss, eIn) => - consume(s, eAss, pve, v)((s2, _, v2) => { + consume(s, eAss, false, pve, v)((s2, _, v2) => { val s3 = s2.copy(g = s.g, h = s.h) eval(s3, eIn, pve, v2)(Q) }) diff --git a/src/main/scala/rules/Executor.scala b/src/main/scala/rules/Executor.scala index a19e85d65..5840a01c3 100644 --- a/src/main/scala/rules/Executor.scala +++ b/src/main/scala/rules/Executor.scala @@ -268,7 +268,7 @@ object executor extends ExecutionRules { })}) combine executionFlowController.locally(s, v)((s0, v0) => { v0.decider.prover.comment("Loop head block: Establish invariant") - consumes(s0, invs, LoopInvariantNotEstablished, v0)((sLeftover, _, v1) => { + consumes(s0, invs, false, LoopInvariantNotEstablished, v0)((sLeftover, _, v1) => { v1.decider.prover.comment("Loop head block: Execute statements of loop head block (in invariant state)") phase1data.foldLeft(Success(): VerificationResult) { case (result, _) if !result.continueVerification => result @@ -302,7 +302,7 @@ object executor extends ExecutionRules { * attempting to re-establish the invariant. */ v.decider.prover.comment("Loop head block: Re-establish invariant") - consumes(s, invs, e => LoopInvariantNotPreserved(e), v)((_, _, _) => + consumes(s, invs, false, e => LoopInvariantNotPreserved(e), v)((_, _, _) => Success()) } } @@ -435,7 +435,7 @@ object executor extends ExecutionRules { val resource = fa.res(s.program) val ve = pve dueTo InsufficientPermission(fa) val description = s"consume ${ass.pos}: $ass" - chunkSupporter.consume(s2, s2.h, resource, Seq(tRcvr), eRcvrNew.map(Seq(_)), FullPerm, Option.when(withExp)(ast.FullPerm()(ass.pos, ass.info, ass.errT)), ve, v2, description)((s3, h3, _, v3) => { + chunkSupporter.consume(s2, s2.h, resource, Seq(tRcvr), eRcvrNew.map(Seq(_)), FullPerm, Option.when(withExp)(ast.FullPerm()(ass.pos, ass.info, ass.errT)), false, ve, v2, description)((s3, h3, _, v3) => { val (tSnap, _) = ssaifyRhs(tRhs, rhs, rhsNew, field.name, field.typ, v3, s3) val id = BasicChunkIdentifier(field.name) val newChunk = BasicChunk(FieldID, id, Seq(tRcvr), eRcvrNew.map(Seq(_)), tSnap, FullPerm, Option.when(withExp)(ast.FullPerm()(ass.pos, ass.info, ass.errT))) @@ -486,7 +486,7 @@ object executor extends ExecutionRules { case exhale @ ast.Exhale(a) => val pve = ExhaleFailed(exhale) - consume(s, a, pve, v)((s1, _, v1) => + consume(s, a, false, pve, v)((s1, _, v1) => Q(s1, v1)) case assert @ ast.Assert(a: ast.FalseLit) => @@ -500,7 +500,7 @@ object executor extends ExecutionRules { case assert @ ast.Assert(a) if Verifier.config.disableSubsumption() => val r = - consume(s, a, AssertFailed(assert), v)((_, _, _) => + consume(s, a, false, AssertFailed(assert), v)((_, _, _) => Success()) r combine Q(s, v) @@ -516,11 +516,11 @@ object executor extends ExecutionRules { * hUsed (reserveHeaps.head) instead of consuming them. hUsed is later discarded and replaced * by s.h. By copying hUsed to s.h the contained permissions remain available inside the wand. */ - consume(s, a, pve, v)((s2, _, v1) => { + consume(s, a, false, pve, v)((s2, _, v1) => { Q(s2.copy(h = s2.reserveHeaps.head), v1) }) } else - consume(s, a, pve, v)((s1, _, v1) => { + consume(s, a, false, pve, v)((s1, _, v1) => { val s2 = s1.copy(h = s.h, reserveHeaps = s.reserveHeaps) Q(s2, v1)}) @@ -578,7 +578,7 @@ object executor extends ExecutionRules { tArgs zip Seq.fill(tArgs.size)(None) val s2 = s1.copy(g = Store(fargs.zip(argsWithExp)), recordVisited = true) - consumes(s2, meth.pres, _ => pvePre, v1)((s3, _, v2) => { + consumes(s2, meth.pres, false, _ => pvePre, v1)((s3, _, v2) => { v2.symbExLog.closeScope(preCondId) val postCondLog = new CommentRecord("Postcondition", s3, v2.decider.pcs) val postCondId = v2.symbExLog.openScope(postCondLog) diff --git a/src/main/scala/rules/MagicWandSupporter.scala b/src/main/scala/rules/MagicWandSupporter.scala index 0cd0e4acb..53bbd71c5 100644 --- a/src/main/scala/rules/MagicWandSupporter.scala +++ b/src/main/scala/rules/MagicWandSupporter.scala @@ -398,10 +398,10 @@ object magicWandSupporter extends SymbolicExecutionRules { // This part indirectly calls the methods `this.transfer` and `this.consumeFromMultipleHeaps`. consume( proofScriptState.copy(oldHeaps = s2.oldHeaps, reserveCfgs = proofScriptState.reserveCfgs.tail), - wand.right, pve, proofScriptVerifier + wand.right, true, pve, proofScriptVerifier )((s3, snapRhs, v3) => { - createWandChunkAndRecordResults(s3.copy(exhaleExt = false, oldHeaps = s.oldHeaps), freshSnapRoot, snapRhs, v3) + createWandChunkAndRecordResults(s3.copy(exhaleExt = false, oldHeaps = s.oldHeaps), freshSnapRoot, snapRhs.get, v3) }) }) }) @@ -457,28 +457,28 @@ object magicWandSupporter extends SymbolicExecutionRules { (Q: (State, Verifier) => VerificationResult) : VerificationResult = { // Consume the magic wand instance "A --* B". - consume(s, wand, pve, v)((s1, snapWand, v1) => { + consume(s, wand, true, pve, v)((s1, snapWand, v1) => { // Consume the wand's LHS "A". - consume(s1, wand.left, pve, v1)((s2, snapLhs, v2) => { + consume(s1, wand.left, true, pve, v1)((s2, snapLhs, v2) => { /* It is assumed that snap and MagicWandSnapshot.abstractLhs are structurally the same. * Equating the two snapshots is sound iff a wand is applied only once. * The old solution in this case did use this assumption: * v2.decider.assume(snap === snapWand.abstractLhs) */ - assert(snapLhs.sort == sorts.Snap, s"expected snapshot but found: $snapLhs") + assert(snapLhs.get.sort == sorts.Snap, s"expected snapshot but found: $snapLhs") // Create copy of the state with a new labelled heap (i.e. `oldHeaps`) called "lhs". val s3 = s2.copy(oldHeaps = s1.oldHeaps + (Verifier.MAGIC_WAND_LHS_STATE_LABEL -> this.getEvalHeap(s1))) // If the snapWand is a (wrapped) MagicWandSnapshot then lookup the snapshot of the right-hand side by applying snapLhs. - val magicWandSnapshotLookup = snapWand match { - case snapshot: MagicWandSnapshot => snapshot.applyToMWSF(snapLhs) - case SortWrapper(snapshot: MagicWandSnapshot, _) => snapshot.applyToMWSF(snapLhs) + val magicWandSnapshotLookup = snapWand.get match { + case snapshot: MagicWandSnapshot => snapshot.applyToMWSF(snapLhs.get) + case SortWrapper(snapshot: MagicWandSnapshot, _) => snapshot.applyToMWSF(snapLhs.get) // Fallback solution for quantified magic wands case predicateLookup: PredicateLookup => - v2.decider.assume(snapLhs === First(snapWand), Option.when(withExp)(DebugExp.createInstance("Magic wand snapshot", true))) + v2.decider.assume(snapLhs.get === First(snapWand.get), Option.when(withExp)(DebugExp.createInstance("Magic wand snapshot", true))) Second(predicateLookup) - case _ => snapWand + case _ => snapWand.get } // Produce the wand's RHS. diff --git a/src/main/scala/rules/MoreCompleteExhaleSupporter.scala b/src/main/scala/rules/MoreCompleteExhaleSupporter.scala index 1739866e1..f908c28fd 100644 --- a/src/main/scala/rules/MoreCompleteExhaleSupporter.scala +++ b/src/main/scala/rules/MoreCompleteExhaleSupporter.scala @@ -32,6 +32,39 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { final case class FreshSummarisingSnapshot(snapshot: Term) extends TaggedSummarisingSnapshot final case class ReusedSummarisingSnapshot(snapshot: Term) extends TaggedSummarisingSnapshot + private def permSummariseOnly(s: State, + relevantChunks: Seq[NonQuantifiedChunk], + resource: ast.Resource, + args: Seq[Term], + argsExp: Option[Seq[ast.Exp]], + v: Verifier) + : (State, Term, Option[ast.Exp]) = { + Verifier.config.mapCache(s.ssCache.get((resource, relevantChunks, args))) match { + case Some((_, _ ,_permissionSum, _permissionSumExp)) => + return (s, _permissionSum, _permissionSumExp) + case _ => + /* Cache miss */ + } + var permissionSum: Term = NoPerm + var permissionSumExp: Option[ast.Exp] = Option.when(withExp)(ast.NoPerm()()) + relevantChunks.foreach(ch => { + val argumentEqualities = + And(ch.args.zip(args).map { case (t1, t2) => t1 === t2 }) + val argumentEqualitiesExp = + Option.when(withExp)(BigAnd(ch.argsExp.get.zip(argsExp.get).map { case (e1, e2) => ast.EqCmp(e1, e2)() })) + + permissionSum = + PermPlus(permissionSum, Ite(argumentEqualities, ch.perm, NoPerm)) + + permissionSumExp = permissionSumExp.map(pse => + ast.PermAdd(pse, ast.CondExp(argumentEqualitiesExp.get, ch.permExp.get, ast.NoPerm()())())()) + }) + val ssc1 = s.ssCache + ((resource, relevantChunks, args) -> (None, None, permissionSum, permissionSumExp)) + val s1 = s.copy(ssCache = ssc1) + + (s1, permissionSum, permissionSumExp) + } + private def summariseOnly(s: State, relevantChunks: Seq[NonQuantifiedChunk], resource: ast.Resource, @@ -50,7 +83,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { // could be cached, and ?a1 etc. would be replaced before returning the summary to the caller. Verifier.config.mapCache(s.ssCache.get((resource, relevantChunks, args))) match { - case Some((_taggedSummarisingSnapshot, _summarisingSnapshotDefinitions, _permissionSum, _permissionSumExp)) => + case Some((Some(_taggedSummarisingSnapshot), Some(_summarisingSnapshotDefinitions), _permissionSum, _permissionSumExp)) => return (s, _taggedSummarisingSnapshot, _summarisingSnapshotDefinitions, _permissionSum, _permissionSumExp) case _ => /* Cache miss */ @@ -65,8 +98,6 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { val `?s` = Var(Identifier("?s"), sort, false) var summarisingSnapshotDefinitions: Seq[Term] = Vector.empty - var permissionSum: Term = NoPerm - var permissionSumExp: Option[ast.Exp] = Option.when(withExp)(ast.NoPerm()()) relevantChunks.foreach(ch => { val argumentEqualities = @@ -76,12 +107,6 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { summarisingSnapshotDefinitions :+= Implies(And(argumentEqualities, IsPositive(ch.perm)), `?s` === ch.snap) - - permissionSum = - PermPlus(permissionSum, Ite(argumentEqualities, ch.perm, NoPerm)) - - permissionSumExp = permissionSumExp.map(pse => - ast.PermAdd(pse, ast.CondExp(argumentEqualitiesExp.get, ch.permExp.get, ast.NoPerm()())())()) }) val taggedSummarisingSnapshot = @@ -119,7 +144,9 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { summarisingSnapshotDefinitions = summarisingSnapshotDefinitions map (_.replace(`?s`, summarisingSnapshot)) - val ssc1 = s.ssCache + ((resource, relevantChunks, args) -> (taggedSummarisingSnapshot, summarisingSnapshotDefinitions, permissionSum, permissionSumExp)) + val (_, permissionSum, permissionSumExp) = permSummariseOnly(s, relevantChunks, resource, args, argsExp, v) + + val ssc1 = s.ssCache + ((resource, relevantChunks, args) -> (Some(taggedSummarisingSnapshot), Some(summarisingSnapshotDefinitions), permissionSum, permissionSumExp)) val s1 = s.copy(ssCache = ssc1) (s1, taggedSummarisingSnapshot, summarisingSnapshotDefinitions, permissionSum, permissionSumExp) @@ -133,7 +160,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { knownValue: Option[Option[Term]], // None if we have not yet checked for a definite alias, // Some(v) if we have checked and the result was v v: Verifier) - (Q: (State, Term, Seq[Term], Term, Option[ast.Exp], Verifier) => VerificationResult) + (Q: (State, Term, Term, Option[ast.Exp], Verifier) => VerificationResult) : VerificationResult = { // Don't use the shortcut if we want a counterexample; in that case, we need the decider to perform a single // query to check if the permission amount we have is sufficient to get the correct counterexample. If we perform @@ -142,15 +169,15 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { if (relevantChunks.size == 1 && !Verifier.config.counterexample.isDefined) { val chunk = relevantChunks.head if (v.decider.check(And(chunk.args.zip(args).map { case (t1, t2) => t1 === t2 }), Verifier.config.checkTimeout())) { - return Q(s, chunk.snap, Seq(), chunk.perm, chunk.permExp, v) + return Q(s, chunk.snap, chunk.perm, chunk.permExp, v) } else { - return Q(s, chunk.snap, Seq(), NoPerm, Option.when(withExp)(ast.NoPerm()()), v) + return Q(s, chunk.snap, NoPerm, Option.when(withExp)(ast.NoPerm()()), v) } } - val (s1, taggedSnap, snapDefs, permSum, permSumExp) = summariseOnly(s, relevantChunks, resource, args, argsExp, knownValue, v) + val (s1, taggedSnap, snapDefs, permSum, permSumExp) = summariseOnly(s, relevantChunks, resource, args, argsExp, knownValue, v) v.decider.assumeDefinition(And(snapDefs), Option.when(withExp)(DebugExp.createInstance("Snapshot", true))) -// v.decider.assume(PermAtMost(permSum, FullPerm())) /* Done in StateConsolidator instead */ + // v.decider.assume(PermAtMost(permSum, FullPerm())) /* Done in StateConsolidator instead */ val s2 = taggedSnap match { @@ -163,7 +190,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { s1 } - Q(s2, taggedSnap.snapshot, snapDefs, permSum, permSumExp, v) + Q(s2, taggedSnap.snapshot, permSum, permSumExp, v) } def lookupComplete(s: State, @@ -186,7 +213,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { createFailure(ve, v, s, False, "branch is dead") } } else { - summarise(s, relevantChunks, resource, args, argsExp, None, v)((s1, snap, _, permSum, permSumExp, v1) => + summarise(s, relevantChunks, resource, args, argsExp, None, v)((s1, snap, permSum, permSumExp, v1) => v.decider.assert(IsPositive(permSum)) { case true => Q(s1, snap, v1) @@ -203,15 +230,17 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { argsExp: Option[Seq[ast.Exp]], perms: Term, permsExp: Option[ast.Exp], + returnSnap: Boolean, ve: VerificationError, v: Verifier) (Q: (State, Heap, Option[Term], Verifier) => VerificationResult) : VerificationResult = { if (!s.hackIssue387DisablePermissionConsumption) - actualConsumeComplete(s, h, resource, args, argsExp, perms, permsExp, ve, v)(Q) - else - summariseHeapAndAssertReadAccess(s, h, resource, args, argsExp, ve, v)(Q) + actualConsumeComplete(s, h, resource, args, argsExp, perms, permsExp, returnSnap, ve, v)(Q) + else { + summariseHeapAndAssertReadAccess(s, h, resource, args, argsExp, returnSnap, ve, v)(Q) + } } private def summariseHeapAndAssertReadAccess(s: State, @@ -219,6 +248,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { resource: ast.Resource, args: Seq[Term], argsExp: Option[Seq[ast.Exp]], + returnSnap: Boolean, ve: VerificationError, v: Verifier) (Q: (State, Heap, Option[Term], Verifier) => VerificationResult) @@ -226,14 +256,23 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { val id = ChunkIdentifier(resource, s.program) val relevantChunks = findChunksWithID[NonQuantifiedChunk](h.values, id).toSeq - - summarise(s, relevantChunks, resource, args, argsExp, None, v)((s1, snap, _, permSum, permSumExp, v1) => + if (returnSnap) { + summarise(s, relevantChunks, resource, args, argsExp, None, v)((s1, snap, permSum, permSumExp, v1) => + v.decider.assert(IsPositive(permSum)) { + case true => + Q(s1, h, Some(snap), v1) + case false => + createFailure(ve, v, s1, IsPositive(permSum), permSumExp.map(IsPositive(_)())) + }) + } else { + val (s1, permSum, permSumExp) = permSummariseOnly(s, relevantChunks, resource, args, argsExp, v) v.decider.assert(IsPositive(permSum)) { case true => - Q(s1, h, Some(snap), v1) + Q(s1, h, None, v) case false => createFailure(ve, v, s1, IsPositive(permSum), permSumExp.map(IsPositive(_)())) - }) + } + } } private def actualConsumeComplete(s: State, @@ -243,6 +282,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { argsExp: Option[Seq[ast.Exp]], perms: Term, permsExp: Option[ast.Exp], + returnSnap: Boolean, ve: VerificationError, v: Verifier) (Q: (State, Heap, Option[Term], Verifier) => VerificationResult) @@ -264,8 +304,9 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { } } else { if (!terms.utils.consumeExactRead(perms, s.constrainableARPs)) { - actualConsumeCompleteConstrainable(s, relevantChunks, resource, args, argsExp, perms, permsExp, ve, v)((s1, updatedChunks, optSnap, v2) => { - Q(s1, Heap(updatedChunks ++ otherChunks), optSnap, v2)}) + actualConsumeCompleteConstrainable(s, relevantChunks, resource, args, argsExp, perms, permsExp, returnSnap, ve, v)((s1, updatedChunks, optSnap, v2) => { + Q(s1, Heap(updatedChunks ++ otherChunks), optSnap, v2) + }) } else { var pNeeded = perms var pNeededExp = permsExp @@ -343,22 +384,38 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { val s0 = s.copy(functionRecorder = currentFunctionRecorder) - summarise(s0, relevantChunks.toSeq, resource, args, argsExp, Some(definiteAlias.map(_.snap)), v)((s1, snap, _, _, _, v1) => { - val condSnap = if (v1.decider.check(IsPositive(perms), Verifier.config.checkTimeout())) { - snap - } else { - Ite(IsPositive(perms), snap.convert(sorts.Snap), Unit) - } + + + if (returnSnap) { + summarise(s0, relevantChunks.toSeq, resource, args, argsExp, Some(definiteAlias.map(_.snap)), v)((s1, snap, _, _, v1) => { + val condSnap = Some(if (v1.decider.check(IsPositive(perms), Verifier.config.checkTimeout())) { + snap + } else { + Ite(IsPositive(perms), snap.convert(sorts.Snap), Unit) + }) if (!moreNeeded) { - Q(s1, newHeap, Some(condSnap), v1) + Q(s1, newHeap, condSnap, v1) } else { v1.decider.assert(pNeeded === NoPerm) { case true => - Q(s1, newHeap, Some(condSnap), v1) + Q(s1, newHeap, condSnap, v1) case false => createFailure(ve, v1, s1, pNeeded === NoPerm, pNeededExp.map(pn => ast.EqCmp(pn, ast.NoPerm()())(pn.pos, pn.info, pn.errT))) } - }}) + } + }) + } else { + if (!moreNeeded) { + Q(s, newHeap, None, v) + } else { + v.decider.assert(pNeeded === NoPerm) { + case true => + Q(s, newHeap, None, v) + case false => + createFailure(ve, v, s, pNeeded === NoPerm, pNeededExp.map(pn => ast.EqCmp(pn, ast.NoPerm()())(pn.pos, pn.info, pn.errT))) + } + } + } } } } @@ -370,6 +427,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { argsExp: Option[Seq[ast.Exp]], perms: Term, // Expected to be constrainable. Will be assumed to equal the consumed permission amount. permsExp: Option[ast.Exp], + returnSnap: Boolean, ve: VerificationError, v: Verifier) (Q: (State, ListBuffer[NonQuantifiedChunk], Option[Term], Verifier) => VerificationResult) @@ -433,16 +491,18 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { case true => val constraintExp = permsExp.map(pe => ast.EqCmp(pe, totalPermTakenExp.get)()) v.decider.assume(perms === totalPermTaken, Option.when(withExp)(DebugExp.createInstance(constraintExp, constraintExp))) - summarise(s1, relevantChunks.toSeq, resource, args, argsExp, None, v)((s2, snap, _, _, _, v1) => - Q(s2, updatedChunks, Some(snap), v1)) + if (returnSnap) { + summarise(s1, relevantChunks.toSeq, resource, args, argsExp, None, v)((s2, snap, _, _, v1) => + Q(s2, updatedChunks, Some(snap), v1)) + } else { + Q(s1, updatedChunks, None, v) + } case false => v.decider.finishDebugSubExp(s"consume permissions for ${resource.toString()}") createFailure(ve, v, s, totalPermTaken !== NoPerm, totalPermTakenExp.map(tpt => ast.NeCmp(tpt, ast.NoPerm()())())) } - } - private val freeReceiver = Var(Identifier("?rcvr"), sorts.Ref, false) private val freeReceiverExp = ast.LocalVar("?rcvr", ast.Ref)() diff --git a/src/main/scala/rules/PredicateSupporter.scala b/src/main/scala/rules/PredicateSupporter.scala index ad26da21b..4f4cf6640 100644 --- a/src/main/scala/rules/PredicateSupporter.scala +++ b/src/main/scala/rules/PredicateSupporter.scala @@ -70,16 +70,16 @@ object predicateSupporter extends PredicateSupportRules { val s1 = s.copy(g = gIns, smDomainNeeded = true) .scalePermissionFactor(tPerm, ePerm) - consume(s1, body, pve, v)((s1a, snap, v1) => { + consume(s1, body, true, pve, v)((s1a, snap, v1) => { if (!Verifier.config.disableFunctionUnfoldTrigger()) { val predTrigger = App(s1a.predicateData(predicate).triggerFunction, - snap.convert(terms.sorts.Snap) +: tArgs) + snap.get.convert(terms.sorts.Snap) +: tArgs) val eArgsString = eArgs.mkString(", ") v1.decider.assume(predTrigger, Option.when(withExp)(DebugExp.createInstance(s"PredicateTrigger(${predicate.name}($eArgsString))"))) } val s2 = s1a.setConstrainable(constrainableWildcards, false) if (s2.qpPredicates.contains(predicate)) { - val predSnap = snap.convert(s2.predicateSnapMap(predicate)) + val predSnap = snap.get.convert(s2.predicateSnapMap(predicate)) val formalArgs = s2.predicateFormalVarMap(predicate) val (sm, smValueDef) = quantifiedChunkSupporter.singletonSnapshotMap(s2, predicate, tArgs, predSnap, v1) @@ -113,7 +113,7 @@ object predicateSupporter extends PredicateSupportRules { functionRecorder = s2.functionRecorder.recordFvfAndDomain(smDef)) Q(s3, v1) } else { - val ch = BasicChunk(PredicateID, BasicChunkIdentifier(predicate.name), tArgs, eArgs, snap.convert(sorts.Snap), tPerm, ePerm) + val ch = BasicChunk(PredicateID, BasicChunkIdentifier(predicate.name), tArgs, eArgs, snap.get.convert(sorts.Snap), tPerm, ePerm) val s3 = s2.copy(g = s.g, smDomainNeeded = s.smDomainNeeded, permissionScalingFactor = s.permissionScalingFactor, @@ -156,18 +156,19 @@ object predicateSupporter extends PredicateSupportRules { pa, tPerm, ePerm, + true, None, pve, v )((s2, h2, snap, v1) => { val s3 = s2.copy(g = gIns, h = h2) .setConstrainable(constrainableWildcards, false) - produce(s3, toSf(snap), body, pve, v1)((s4, v2) => { + produce(s3, toSf(snap.get), body, pve, v1)((s4, v2) => { v2.decider.prover.saturate(Verifier.config.proverSaturationTimeouts.afterUnfold) if (!Verifier.config.disableFunctionUnfoldTrigger()) { val predicateTrigger = App(s4.predicateData(predicate).triggerFunction, - snap.convert(terms.sorts.Snap) +: tArgs) + snap.get.convert(terms.sorts.Snap) +: tArgs) val eargs = eArgs.mkString(", ") v2.decider.assume(predicateTrigger, Option.when(withExp)(DebugExp.createInstance(s"PredicateTrigger(${predicate.name}($eargs))"))) } @@ -179,14 +180,14 @@ object predicateSupporter extends PredicateSupportRules { } else { val ve = pve dueTo InsufficientPermission(pa) val description = s"consume ${pa.pos}: $pa" - chunkSupporter.consume(s1, s1.h, predicate, tArgs, eArgs, s1.permissionScalingFactor, s1.permissionScalingFactorExp, ve, v, description)((s2, h1, snap, v1) => { + chunkSupporter.consume(s1, s1.h, predicate, tArgs, eArgs, s1.permissionScalingFactor, s1.permissionScalingFactorExp, true, ve, v, description)((s2, h1, snap, v1) => { val s3 = s2.copy(g = gIns, h = h1) .setConstrainable(constrainableWildcards, false) - produce(s3, toSf(snap), body, pve, v1)((s4, v2) => { + produce(s3, toSf(snap.get), body, pve, v1)((s4, v2) => { v2.decider.prover.saturate(Verifier.config.proverSaturationTimeouts.afterUnfold) if (!Verifier.config.disableFunctionUnfoldTrigger()) { val predicateTrigger = - App(s4.predicateData(predicate).triggerFunction, snap +: tArgs) + App(s4.predicateData(predicate).triggerFunction, snap.get +: tArgs) val eargs = eArgs.mkString(", ") v2.decider.assume(predicateTrigger, Option.when(withExp)(DebugExp.createInstance(s"PredicateTrigger(${pa.predicateName}($eargs))"))) } diff --git a/src/main/scala/rules/QuantifiedChunkSupport.scala b/src/main/scala/rules/QuantifiedChunkSupport.scala index 37a7a26b8..a05e39aa4 100644 --- a/src/main/scala/rules/QuantifiedChunkSupport.scala +++ b/src/main/scala/rules/QuantifiedChunkSupport.scala @@ -21,6 +21,7 @@ import viper.silicon.state.terms.utils.consumeExactRead import viper.silicon.supporters.functions.{FunctionRecorder, NoopFunctionRecorder} import viper.silicon.utils.ast.{BigAnd, buildMinExp} import viper.silicon.utils.notNothing.NotNothing +import viper.silicon.utils.freshSnap import viper.silicon.verifier.Verifier import viper.silver.ast import viper.silver.parser.PUnknown @@ -1152,12 +1153,13 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { eArgs: Option[Seq[ast.Exp]], tPerm: Term, ePerm: Option[ast.Exp], + returnSnap: Boolean, pve: PartialVerificationError, negativePermissionReason: => ErrorReason, notInjectiveReason: => ErrorReason, insufficientPermissionReason: => ErrorReason, v: Verifier) - (Q: (State, Heap, Term, Verifier) => VerificationResult) + (Q: (State, Heap, Option[Term], Verifier) => VerificationResult) : VerificationResult = { val (inverseFunctions, imagesOfFormalQVars) = @@ -1348,8 +1350,10 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { (result, s4, h2, Some(consumedChunk)) })((s4, optCh, v3) => optCh match { - case Some(ch) => Q(s4, s4.h, ch.snapshotMap.convert(sorts.Snap), v3) - case _ => Q(s4, s4.h, v3.decider.fresh(sorts.Snap, Option.when(withExp)(PUnknown())), v3) + case Some(ch) if returnSnap => Q(s4, s4.h, Some(ch.snapshotMap.convert(sorts.Snap)), v3) + case None if returnSnap => + Q(s4, s4.h, Some(freshSnap(sorts.Snap, v3)), v3) + case _ => Q(s4, s4.h, None, v3) } ) } else { @@ -1372,19 +1376,22 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { permissionRemovalResult match { case (Complete(), s2, remainingChunks) => val h3 = Heap(remainingChunks ++ otherChunks) - val optSmDomainDefinitionCondition2 = - if (s2.smDomainNeeded) Some(And(condOfInvOfLoc, IsPositive(lossOfInvOfLoc), And(And(imagesOfFormalQVars)))) - else None - val (smDef2, smCache2) = - quantifiedChunkSupporter.summarisingSnapshotMap( + if (returnSnap) { + val optSmDomainDefinitionCondition2 = + if (s2.smDomainNeeded) Some(And(condOfInvOfLoc, IsPositive(lossOfInvOfLoc), And(And(imagesOfFormalQVars)))) + else None + val (smDef2, smCache2) = quantifiedChunkSupporter.summarisingSnapshotMap( s2, resource, formalQVars, relevantChunks, v, optSmDomainDefinitionCondition2) - val fr3 = s2.functionRecorder.recordFvfAndDomain(smDef2) - .recordFieldInv(inverseFunctions) - val s3 = s2.copy(functionRecorder = fr3, - partiallyConsumedHeap = Some(h3), - constrainableARPs = s.constrainableARPs, - smCache = smCache2) - Q(s3, h3, smDef2.sm.convert(sorts.Snap), v) + val fr3 = s2.functionRecorder.recordFvfAndDomain(smDef2) + .recordFieldInv(inverseFunctions) + val s3 = s2.copy(functionRecorder = fr3, + partiallyConsumedHeap = Some(h3), + constrainableARPs = s.constrainableARPs, + smCache = smCache2) + Q(s3, h3, Some(smDef2.sm.convert(sorts.Snap)), v) + } else { + Q(s2, h3, None, v) + } case (Incomplete(_, _), s2, _) => createFailure(pve dueTo insufficientPermissionReason, v, s2, "QP consume")} } @@ -1403,10 +1410,11 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { resourceAccess: ast.ResourceAccess, permissions: Term, /* p */ permissionsExp: Option[ast.Exp], + returnSnap: Boolean, optChunkOrderHeuristic: Option[Seq[QuantifiedBasicChunk] => Seq[QuantifiedBasicChunk]], pve: PartialVerificationError, v: Verifier) - (Q: (State, Heap, Term, Verifier) => VerificationResult) + (Q: (State, Heap, Option[Term], Verifier) => VerificationResult) : VerificationResult = { val resource = resourceAccess.res(s.program) @@ -1466,11 +1474,12 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { (result, s3, h2, Some(consumedChunk)) })((s4, optCh, v2) => optCh match { - case Some(ch) => + case Some(ch) if returnSnap => val snap = ResourceLookup(resource, ch.snapshotMap, arguments, s4.program).convert(sorts.Snap) - Q(s4, s4.h, snap, v2) - case _ => - Q(s4, s4.h, v2.decider.fresh(sorts.Snap, Option.when(withExp)(PUnknown())), v2) + Q(s4, s4.h, Some(snap), v2) + case None if returnSnap => + Q(s4, s4.h, Some(freshSnap(sorts.Snap, v2)), v2) + case _ => Q(s4, s4.h, None, v2) } ) } else { @@ -1494,19 +1503,23 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { result match { case (Complete(), s1, remainingChunks) => val h1 = Heap(remainingChunks ++ otherChunks) - val (smDef1, smCache1) = - quantifiedChunkSupporter.summarisingSnapshotMap( - s = s1, - resource = resource, - codomainQVars = codomainQVars, - relevantChunks = relevantChunks, - optSmDomainDefinitionCondition = None, - optQVarsInstantiations = Some(arguments), - v = v) - val s2 = s1.copy(functionRecorder = s1.functionRecorder.recordFvfAndDomain(smDef1), - smCache = smCache1) - val snap = ResourceLookup(resource, smDef1.sm, arguments, s2.program).convert(sorts.Snap) - Q(s2, h1, snap, v) + if (returnSnap) { + val (smDef1, smCache1) = + quantifiedChunkSupporter.summarisingSnapshotMap( + s = s1, + resource = resource, + codomainQVars = codomainQVars, + relevantChunks = relevantChunks, + optSmDomainDefinitionCondition = None, + optQVarsInstantiations = Some(arguments), + v = v) + val s2 = s1.copy(functionRecorder = s1.functionRecorder.recordFvfAndDomain(smDef1), + smCache = smCache1) + val snap = ResourceLookup(resource, smDef1.sm, arguments, s2.program).convert(sorts.Snap) + Q(s2, h1, Some(snap), v) + } else { + Q(s1, h1, None, v) + } case (Incomplete(_, _), _, _) => resourceAccess match { case locAcc: ast.LocationAccess => createFailure(pve dueTo InsufficientPermission(locAcc), v, s, "single QP consume") diff --git a/src/main/scala/state/package.scala b/src/main/scala/state/package.scala index 11fb6fb1b..5cb59c877 100644 --- a/src/main/scala/state/package.scala +++ b/src/main/scala/state/package.scala @@ -21,5 +21,5 @@ package object state { type SsCache = Map[ (ast.Resource, Seq[NonQuantifiedChunk], Seq[Term]), - (TaggedSummarisingSnapshot, Seq[Term], Term, Option[ast.Exp])] + (Option[TaggedSummarisingSnapshot], Option[Seq[Term]], Term, Option[ast.Exp])] } diff --git a/src/main/scala/supporters/MethodSupporter.scala b/src/main/scala/supporters/MethodSupporter.scala index f132f638f..9b483ff4a 100644 --- a/src/main/scala/supporters/MethodSupporter.scala +++ b/src/main/scala/supporters/MethodSupporter.scala @@ -111,7 +111,7 @@ trait DefaultMethodVerificationUnitProvider extends VerifierComponent { v: Verif && { executionFlowController.locally(s2a, v2)((s3, v3) => { exec(s3, body, v3)((s4, v4) => - consumes(s4, posts, postViolated, v4)((_, _, _) => + consumes(s4, posts, false, postViolated, v4)((_, _, _) => Success()))}) } )})}) v.decider.resetProverOptions() diff --git a/src/main/scala/supporters/functions/FunctionVerificationUnit.scala b/src/main/scala/supporters/functions/FunctionVerificationUnit.scala index 7fe942e80..67d4d8a7b 100644 --- a/src/main/scala/supporters/functions/FunctionVerificationUnit.scala +++ b/src/main/scala/supporters/functions/FunctionVerificationUnit.scala @@ -264,7 +264,7 @@ trait DefaultFunctionVerificationUnitProvider extends VerifierComponent { v: Ver Some(DebugExp.createInstance(e, eNew)) } else { None } decider.assume(BuiltinEquals(data.formalResult, tBody), debugExp) - consumes(s2, posts, postconditionViolated, v)((s3, _, _) => { + consumes(s2, posts, false, postconditionViolated, v)((s3, _, _) => { recorders :+= s3.functionRecorder Success()})})})} From 448775ec40c6413811f6c3ac1095e22bd227f7e6 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Mon, 2 Dec 2024 15:18:34 +0100 Subject: [PATCH 9/9] Fixed incorrect merge where wrong state is forwarded (#881) --- src/main/scala/rules/MoreCompleteExhaleSupporter.scala | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/main/scala/rules/MoreCompleteExhaleSupporter.scala b/src/main/scala/rules/MoreCompleteExhaleSupporter.scala index f908c28fd..4472c0fb8 100644 --- a/src/main/scala/rules/MoreCompleteExhaleSupporter.scala +++ b/src/main/scala/rules/MoreCompleteExhaleSupporter.scala @@ -406,13 +406,13 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { }) } else { if (!moreNeeded) { - Q(s, newHeap, None, v) + Q(s0, newHeap, None, v) } else { v.decider.assert(pNeeded === NoPerm) { case true => - Q(s, newHeap, None, v) + Q(s0, newHeap, None, v) case false => - createFailure(ve, v, s, pNeeded === NoPerm, pNeededExp.map(pn => ast.EqCmp(pn, ast.NoPerm()())(pn.pos, pn.info, pn.errT))) + createFailure(ve, v, s0, pNeeded === NoPerm, pNeededExp.map(pn => ast.EqCmp(pn, ast.NoPerm()())(pn.pos, pn.info, pn.errT))) } } }