From 8fd11b1b63854033bee1e7351492507343638b79 Mon Sep 17 00:00:00 2001 From: mlimbeck Date: Sat, 9 Nov 2024 21:24:06 +0100 Subject: [PATCH 1/6] remove snapshot creation in consume for some satements --- src/main/scala/rules/ChunkSupporter.scala | 13 ++- src/main/scala/rules/Consumer.scala | 102 ++++++++++-------- src/main/scala/rules/Evaluator.scala | 15 +-- src/main/scala/rules/Executor.scala | 16 +-- src/main/scala/rules/MagicWandSupporter.scala | 20 ++-- src/main/scala/rules/PredicateSupporter.scala | 19 ++-- .../scala/rules/QuantifiedChunkSupport.scala | 101 ++++++++++------- .../scala/supporters/MethodSupporter.scala | 2 +- .../functions/FunctionVerificationUnit.scala | 2 +- 9 files changed, 170 insertions(+), 120 deletions(-) diff --git a/src/main/scala/rules/ChunkSupporter.scala b/src/main/scala/rules/ChunkSupporter.scala index 311063b26..ab1ed8382 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], + SnapNeeded: 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,16 +72,17 @@ object chunkSupporter extends ChunkSupportRules { argsExp: Option[Seq[ast.Exp]], perms: Term, permsExp: Option[ast.Exp], + SnapNeeded: 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, SnapNeeded, ve, v)((s2, h2, optSnap, v2) => optSnap match { case Some(snap) => - Q(s2, h2, snap.convert(sorts.Snap), v2) + Q(s2, h2, Some(snap.convert(sorts.Snap)), v2) case None => /* 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,7 @@ 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) }) } @@ -102,6 +104,7 @@ object chunkSupporter extends ChunkSupportRules { argsExp: Option[Seq[ast.Exp]], perms: Term, permsExp: Option[ast.Exp], + SnapNeeded: Boolean, ve: VerificationError, v: Verifier) (Q: (State, Heap, Option[Term], Verifier) => VerificationResult) diff --git a/src/main/scala/rules/Consumer.scala b/src/main/scala/rules/Consumer.scala index 4041636ba..78e1517ca 100644 --- a/src/main/scala/rules/Consumer.scala +++ b/src/main/scala/rules/Consumer.scala @@ -36,8 +36,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, SnapNeeded: 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`. @@ -56,9 +56,10 @@ trait ConsumptionRules extends SymbolicExecutionRules { */ def consumes(s: State, as: Seq[ast.Exp], + SnapNeeded: Boolean, pvef: ast.Exp => PartialVerificationError, v: Verifier) - (Q: (State, Term, Verifier) => VerificationResult) + (Q: (State, Option[Term], Verifier) => VerificationResult) : VerificationResult } @@ -71,11 +72,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, SnapNeeded: 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, SnapNeeded, pve, v)((s1, h1, snap, v1) => { val s2 = s1.copy(h = h1, partiallyConsumedHeap = s.partiallyConsumedHeap) Q(s2, snap, v1)}) @@ -84,9 +85,10 @@ object consumer extends ConsumptionRules { /** @inheritdoc */ def consumes(s: State, as: Seq[ast.Exp], + SnapNeeded: 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 +102,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(), SnapNeeded, allPves.result(), v)((s1, h1, snap1, v1) => { val s2 = s1.copy(h = h1, partiallyConsumedHeap = s.partiallyConsumedHeap) Q(s2, snap1, v1) @@ -110,34 +112,42 @@ object consumer extends ConsumptionRules { private def consumeTlcs(s: State, h: Heap, tlcs: Seq[ast.Exp], + SnapNeeded: 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, Some(Unit), 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, SnapNeeded, 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, SnapNeeded, pve, v)((s1, h1, snap1, v1) => { + consumeTlcs(s1, h1, tlcs.tail, SnapNeeded, pves.tail, v1)((s2, h2, snap2, v2) => + + (snap1, snap2) match { + case (Some(sn1), Some(sn2)) => Q(s2, h2, Some(Combine(sn1, sn2)), v2) + case (Some(_), _) => Q(s2, h2, snap1, v2) + case (None, Some(_)) => Q(s2, h2, snap2, v2) + case (None, None) => Q(s2, h2, None, v2) + }) + }) } } - 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, SnapNeeded: 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, SnapNeeded, pves, v)(Q) } /** Wrapper/decorator for consume that injects the following operations: @@ -147,9 +157,10 @@ object consumer extends ConsumptionRules { protected def wrappedConsumeTlc(s: State, h: Heap, a: ast.Exp, + SnapNeeded: 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 +168,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, SnapNeeded, 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, SnapNeeded: 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 +201,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, SnapNeeded, pve, v)(Q) case imp @ ast.Implies(e0, a0) if !a.isPure => val impliesRecord = new ImpliesRecord(imp, s, v.decider.pcs, "consume") @@ -198,19 +209,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, SnapNeeded, 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, Some(Unit), 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, SnapNeeded, 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 +229,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, SnapNeeded, 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, SnapNeeded, pve, v2)((s3, h1, t1, v3) => { v3.symbExLog.closeScope(uidCondExp) Q(s3, h1, t1, v3) }))) @@ -260,12 +271,13 @@ object consumer extends ConsumptionRules { eArgs = permRcvrOpt.map(permRcvr => Seq(permRcvr(1))), tPerm = tPerm, ePerm = permRcvrOpt.map(_(0)), + SnapNeeded = SnapNeeded, 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, Some(True), v1) } case QuantifiedPermissionAssertion(forall, cond, acc: ast.PredicateAccessPredicate) => @@ -305,12 +317,13 @@ object consumer extends ConsumptionRules { eArgs = permArgsNew.map(_.tail), tPerm = tPerm, ePerm = permArgsNew.map(_.head), + SnapNeeded = SnapNeeded, 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, Some(True), v1) } case QuantifiedPermissionAssertion(forall, cond, wand: ast.MagicWand) => @@ -346,12 +359,13 @@ object consumer extends ConsumptionRules { eArgs = bodyVarsNew, tPerm = tPerm, ePerm = Option.when(withExp)(ePerm), + SnapNeeded = SnapNeeded, 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, Some(True), v1) } case accPred@ast.AccessPredicate(loc @ ast.FieldAccess(eRcvr, field), ePerm) @@ -387,6 +401,7 @@ object consumer extends ConsumptionRules { loc, loss, lossExp, + SnapNeeded, None, pve, v2 @@ -431,6 +446,7 @@ object consumer extends ConsumptionRules { loc, loss, lossExp, + SnapNeeded, None, pve, v2 @@ -442,7 +458,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, SnapNeeded, pve, v1)(Q)}) case ast.AccessPredicate(locacc: ast.LocationAccess, perm) => eval(s, perm, pve, v)((s1, tPerm, permNew, v1) => @@ -456,7 +472,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, SnapNeeded, ve, v3, description)((s4, h1, snap1, v4) => { val s5 = s4.copy(partiallyConsumedHeap = Some(h1), constrainableARPs = s.constrainableARPs) Q(s5, h1, snap1, v4)})}))) @@ -496,6 +512,7 @@ object consumer extends ConsumptionRules { wand, loss, lossExp, + SnapNeeded, None, pve, v1 @@ -508,12 +525,12 @@ 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)), SnapNeeded, ve, v1, description)(Q) }) case _ => evalAndAssert(s, a, pve, v)((s1, t, v1) => { - Q(s1, h, t, v1) + Q(s1, h, Some(t), v1) }) } @@ -521,26 +538,27 @@ object consumer extends ConsumptionRules { } private def consumeConditionalTlcMoreJoins(s: State, h: Heap, e0: ast.Exp, a1: ast.Exp, a2: Option[ast.Exp], scopeUid: Int, + SnapNeeded: 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, SnapNeeded, 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, SnapNeeded, 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, Some(Unit)), v2) }) })(entries => { val s2 = entries match { @@ -552,8 +570,8 @@ 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 + Some(Ite(And(entry1.pathConditions.branchConditions), entry1.data._2.get, entry2.data._2.get)) ) (entry1.pathConditionAwareMergeWithoutConsolidation(entry2, v1), mergedData) case _ => diff --git a/src/main/scala/rules/Evaluator.scala b/src/main/scala/rules/Evaluator.scala index 0570c926c..19a1dbe9e 100644 --- a/src/main/scala/rules/Evaluator.scala +++ b/src/main/scala/rules/Evaluator.scala @@ -220,7 +220,8 @@ object evaluator extends EvaluationRules { * quantifier in whose body field 'fa.field' was accessed) * which is protected by a trigger term that we currently don't have. */ - v1.decider.assume(And(fvfDef.valueDefinitions), Option.when(withExp)(DebugExp.createInstance("Value definitions", isInternal_ = true))) + v1.decider.prover.comment("reemit") + //v1.decider.assume(And(fvfDef.valueDefinitions), Option.when(withExp)(DebugExp.createInstance("Value definitions", isInternal_ = true))) if (s1.heapDependentTriggers.contains(fa.field)){ val trigger = FieldTrigger(fa.field.name, fvfDef.sm, tRcvr) val triggerExp = Option.when(withExp)(DebugExp.createInstance(s"FieldTrigger(${eRcvr.toString()}.${fa.field.name})")) @@ -919,8 +920,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 +978,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 +993,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, diff --git a/src/main/scala/rules/Executor.scala b/src/main/scala/rules/Executor.scala index a19e85d65..ca1073152 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)), true, 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, true, 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/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..8fab3118a 100644 --- a/src/main/scala/rules/QuantifiedChunkSupport.scala +++ b/src/main/scala/rules/QuantifiedChunkSupport.scala @@ -521,10 +521,18 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { smDomainDefinitionCondition, /* Alternatively: codomainQVarsInDomainOfSummarisingSm */ IsPositive(chunk.perm)) + val trigger = if (Verifier.config.disableISCTriggers()) { + Nil + } else if (s.heapDependentTriggers.contains(field)){ + Seq(Trigger(lookupSummary)) //, Trigger(lookupChunk)) + } else { + Seq(Trigger(lookupSummary)) + } + Forall( codomainQVar, Implies(effectiveCondition, BuiltinEquals(lookupSummary, lookupChunk)), - if (Verifier.config.disableISCTriggers()) Nil else Seq(Trigger(lookupSummary), Trigger(lookupChunk)), + trigger, s"qp.fvfValDef${v.counter(this).next()}", isGlobal = relevantQvars.isEmpty) }) @@ -594,6 +602,11 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { SetIn(qvar, PredicateDomain(MagicWandIdentifier(wand, s.program).toString, sm)) } + val resourceIdentifier = resource match { + case wand: ast.MagicWand => MagicWandIdentifier(wand, s.program) + case r => r + } + val valueDefinitions = relevantChunks map (chunk => { val lookupSummary = ResourceLookup(resource, sm, Seq(qvar), s.program) @@ -605,29 +618,34 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { if (codomainQVars.nonEmpty) qvar !== Unit else qvar === Unit // TODO: Consider if axioms can be simplified in case codomainQVars is empty - val effectiveCondition = + val effectiveCondition = { And( transformedOptSmDomainDefinitionCondition.getOrElse(True), /* Alternatively: qvarInDomainOfSummarisingSm */ IsPositive(chunk.perm).replace(snapToCodomainTermsSubstitution)) + } + + val trigger = if (Verifier.config.disableISCTriggers()) { + Nil + } else if (s.heapDependentTriggers.contains(resourceIdentifier)){ + Seq(Trigger(lookupSummary), Trigger(lookupChunk)) + } else { + Seq(Trigger(lookupSummary)) + } Forall( qvar, Implies(effectiveCondition, And(snapshotNotUnit, BuiltinEquals(lookupSummary, lookupChunk))), - if (Verifier.config.disableISCTriggers()) Nil else Seq(Trigger(lookupSummary), Trigger(lookupChunk)), + trigger, s"qp.psmValDef${v.counter(this).next()}", isGlobal = relevantQvars.isEmpty) }) - val resourceIdentifier = resource match { - case wand: ast.MagicWand => MagicWandIdentifier(wand, s.program) - case r => r - } val resourceAndValueDefinitions = if (s.heapDependentTriggers.contains(resourceIdentifier)){ val resourceTriggerDefinition = Forall( qvar, And(relevantChunks map (chunk => ResourceTriggerFunction(resource, chunk.snapshotMap, Seq(qvar), s.program))), - Trigger(ResourceLookup(resource, sm, Seq(qvar), s.program)), + Trigger(ResourceLookup(resource, sm, Seq(qvar), s.program)), // +: (relevantChunks map (chunk => Trigger(ResourceLookup(resource, chunk.snapshotMap, Seq(qvar), s.program)))), s"qp.psmResTrgDef${v.counter(this).next()}", isGlobal = relevantQvars.isEmpty) valueDefinitions :+ resourceTriggerDefinition @@ -810,7 +828,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { (smDef, s.smCache + (key, value)) } } - + v.decider.prover.comment("SummarizingSnapshots") emitSnapshotMapDefinition(s, smDef, v, optQVarsInstantiations) (smDef, smCache) @@ -1152,12 +1170,13 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { eArgs: Option[Seq[ast.Exp]], tPerm: Term, ePerm: Option[ast.Exp], + SnapNeeded: 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 +1367,8 @@ 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) => Q(s4, s4.h, Some(ch.snapshotMap.convert(sorts.Snap)), v3) + case _ => Q(s4, s4.h, Some(v3.decider.fresh(sorts.Snap, Option.when(withExp)(PUnknown()))), v3) } ) } else { @@ -1375,16 +1394,19 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { val optSmDomainDefinitionCondition2 = if (s2.smDomainNeeded) Some(And(condOfInvOfLoc, IsPositive(lossOfInvOfLoc), And(And(imagesOfFormalQVars)))) else None - val (smDef2, smCache2) = - quantifiedChunkSupporter.summarisingSnapshotMap( + if(SnapNeeded) { + 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 +1425,11 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { resourceAccess: ast.ResourceAccess, permissions: Term, /* p */ permissionsExp: Option[ast.Exp], + SnapNeeded: 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) @@ -1468,9 +1491,9 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { optCh match { case Some(ch) => val snap = ResourceLookup(resource, ch.snapshotMap, arguments, s4.program).convert(sorts.Snap) - Q(s4, s4.h, snap, v2) + Q(s4, s4.h, Some(snap), v2) case _ => - Q(s4, s4.h, v2.decider.fresh(sorts.Snap, Option.when(withExp)(PUnknown())), v2) + Q(s4, s4.h, Some(v2.decider.fresh(sorts.Snap, Option.when(withExp)(PUnknown()))), v2) } ) } else { @@ -1494,19 +1517,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 (SnapNeeded) { + 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/supporters/MethodSupporter.scala b/src/main/scala/supporters/MethodSupporter.scala index f132f638f..8f2cccb2c 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, true, 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..845689009 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, true, postconditionViolated, v)((s3, _, _) => { recorders :+= s3.functionRecorder Success()})})})} From 5f9ea439ee25169a130f9dd079fa04bd6546d88e Mon Sep 17 00:00:00 2001 From: mlimbeck Date: Tue, 19 Nov 2024 13:37:41 +0100 Subject: [PATCH 2/6] return Snap after consume only optionally --- src/main/scala/rules/ChunkSupporter.scala | 8 +- src/main/scala/rules/Consumer.scala | 77 ++++++++++--------- src/main/scala/rules/Evaluator.scala | 3 +- src/main/scala/rules/Executor.scala | 2 +- .../scala/rules/QuantifiedChunkSupport.scala | 35 +++------ .../scala/supporters/MethodSupporter.scala | 2 +- .../functions/FunctionVerificationUnit.scala | 2 +- 7 files changed, 59 insertions(+), 70 deletions(-) diff --git a/src/main/scala/rules/ChunkSupporter.scala b/src/main/scala/rules/ChunkSupporter.scala index ab1ed8382..5350131e1 100644 --- a/src/main/scala/rules/ChunkSupporter.scala +++ b/src/main/scala/rules/ChunkSupporter.scala @@ -29,7 +29,7 @@ trait ChunkSupportRules extends SymbolicExecutionRules { argsExp: Option[Seq[ast.Exp]], perms: Term, permsExp: Option[ast.Exp], - SnapNeeded: Boolean, + returnSnap: Boolean, ve: VerificationError, v: Verifier, description: String) @@ -72,14 +72,14 @@ object chunkSupporter extends ChunkSupportRules { argsExp: Option[Seq[ast.Exp]], perms: Term, permsExp: Option[ast.Exp], - SnapNeeded: Boolean, + returnSnap: Boolean, ve: VerificationError, v: Verifier, description: String) (Q: (State, Heap, Option[Term], Verifier) => VerificationResult) : VerificationResult = { - consume2(s, h, resource, args, argsExp, perms, permsExp, SnapNeeded, 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, Some(snap.convert(sorts.Snap)), v2) @@ -104,7 +104,7 @@ object chunkSupporter extends ChunkSupportRules { argsExp: Option[Seq[ast.Exp]], perms: Term, permsExp: Option[ast.Exp], - SnapNeeded: Boolean, + returnSnap: Boolean, ve: VerificationError, v: Verifier) (Q: (State, Heap, Option[Term], Verifier) => VerificationResult) diff --git a/src/main/scala/rules/Consumer.scala b/src/main/scala/rules/Consumer.scala index 78e1517ca..d00e17564 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,7 +37,7 @@ trait ConsumptionRules extends SymbolicExecutionRules { * consumed partial heap. * @return The result of the continuation. */ - def consume(s: State, a: ast.Exp, SnapNeeded: Boolean, pve: PartialVerificationError, v: Verifier) + def consume(s: State, a: ast.Exp, returnSnap: Boolean, pve: PartialVerificationError, v: Verifier) (Q: (State, Option[Term], Verifier) => VerificationResult) : VerificationResult @@ -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,7 +58,7 @@ trait ConsumptionRules extends SymbolicExecutionRules { */ def consumes(s: State, as: Seq[ast.Exp], - SnapNeeded: Boolean, + returnSnap: Boolean, pvef: ast.Exp => PartialVerificationError, v: Verifier) (Q: (State, Option[Term], Verifier) => VerificationResult) @@ -72,11 +74,11 @@ object consumer extends ConsumptionRules { */ /** @inheritdoc */ - def consume(s: State, a: ast.Exp, SnapNeeded: Boolean, pve: PartialVerificationError, v: Verifier) + 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, SnapNeeded, 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)}) @@ -85,7 +87,7 @@ object consumer extends ConsumptionRules { /** @inheritdoc */ def consumes(s: State, as: Seq[ast.Exp], - SnapNeeded: Boolean, + returnSnap: Boolean, pvef: ast.Exp => PartialVerificationError, v: Verifier) (Q: (State, Option[Term], Verifier) => VerificationResult) @@ -102,7 +104,7 @@ object consumer extends ConsumptionRules { allPves ++= pves }) - consumeTlcs(s, s.h, allTlcs.result(), SnapNeeded, 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) @@ -112,7 +114,7 @@ object consumer extends ConsumptionRules { private def consumeTlcs(s: State, h: Heap, tlcs: Seq[ast.Exp], - SnapNeeded: Boolean, + returnSnap: Boolean, pves: Seq[PartialVerificationError], v: Verifier) (Q: (State, Heap, Option[Term], Verifier) => VerificationResult) @@ -125,14 +127,14 @@ object consumer extends ConsumptionRules { val pve = pves.head if (tlcs.tail.isEmpty) - wrappedConsumeTlc(s, h, a, SnapNeeded, pve, v)(Q) + wrappedConsumeTlc(s, h, a, returnSnap, pve, v)(Q) else - wrappedConsumeTlc(s, h, a, SnapNeeded, pve, v)((s1, h1, snap1, v1) => { - consumeTlcs(s1, h1, tlcs.tail, SnapNeeded, pves.tail, v1)((s2, h2, 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)) => Q(s2, h2, Some(Combine(sn1, sn2)), v2) - case (Some(_), _) => Q(s2, h2, snap1, v2) + case (Some(_), _) => Q(s2, h2, snap1, v2) //This case and the next case should not be possible and would indicate a bug. case (None, Some(_)) => Q(s2, h2, snap2, v2) case (None, None) => Q(s2, h2, None, v2) }) @@ -140,14 +142,14 @@ object consumer extends ConsumptionRules { } } - private def consumeR(s: State, h: Heap, a: ast.Exp, SnapNeeded: Boolean, pve: PartialVerificationError, v: Verifier) + 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, SnapNeeded, pves, v)(Q) + consumeTlcs(s, h, tlcs, returnSnap, pves, v)(Q) } /** Wrapper/decorator for consume that injects the following operations: @@ -157,7 +159,7 @@ object consumer extends ConsumptionRules { protected def wrappedConsumeTlc(s: State, h: Heap, a: ast.Exp, - SnapNeeded: Boolean, + returnSnap: Boolean, pve: PartialVerificationError, v: Verifier) (Q: (State, Heap, Option[Term], Verifier) => VerificationResult) @@ -174,13 +176,13 @@ object consumer extends ConsumptionRules { val sepIdentifier = v1.symbExLog.openScope(new ConsumeRecord(a, s1, v.decider.pcs)) - consumeTlc(s1, h0, a, SnapNeeded, 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, SnapNeeded: Boolean, pve: PartialVerificationError, v: Verifier) + private def consumeTlc(s: State, h: Heap, a: ast.Exp, returnSnap: Boolean, pve: PartialVerificationError, v: Verifier) (Q: (State, Heap, Option[Term], Verifier) => VerificationResult) : VerificationResult = { @@ -201,7 +203,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, SnapNeeded, 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") @@ -209,7 +211,7 @@ 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, SnapNeeded, 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) }), @@ -221,7 +223,7 @@ object consumer extends ConsumptionRules { 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, SnapNeeded, 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") @@ -229,11 +231,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, SnapNeeded, 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, SnapNeeded, 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) }))) @@ -271,7 +273,7 @@ object consumer extends ConsumptionRules { eArgs = permRcvrOpt.map(permRcvr => Seq(permRcvr(1))), tPerm = tPerm, ePerm = permRcvrOpt.map(_(0)), - SnapNeeded = SnapNeeded, + returnSnap = returnSnap, pve = pve, negativePermissionReason = NegativePermission(acc.perm), notInjectiveReason = QPAssertionNotInjective(acc.loc), @@ -317,7 +319,7 @@ object consumer extends ConsumptionRules { eArgs = permArgsNew.map(_.tail), tPerm = tPerm, ePerm = permArgsNew.map(_.head), - SnapNeeded = SnapNeeded, + returnSnap = returnSnap, pve = pve, negativePermissionReason = NegativePermission(acc.perm), notInjectiveReason = QPAssertionNotInjective(acc.loc), @@ -359,7 +361,7 @@ object consumer extends ConsumptionRules { eArgs = bodyVarsNew, tPerm = tPerm, ePerm = Option.when(withExp)(ePerm), - SnapNeeded = SnapNeeded, + returnSnap = returnSnap, pve = pve, negativePermissionReason = NegativePermission(ePerm), notInjectiveReason = sys.error("Quantified wand not injective"), /*ReceiverNotInjective(...)*/ @@ -401,7 +403,7 @@ object consumer extends ConsumptionRules { loc, loss, lossExp, - SnapNeeded, + returnSnap, None, pve, v2 @@ -446,7 +448,7 @@ object consumer extends ConsumptionRules { loc, loss, lossExp, - SnapNeeded, + returnSnap, None, pve, v2 @@ -458,7 +460,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, SnapNeeded, 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) => @@ -472,7 +474,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, SnapNeeded, 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)})}))) @@ -512,7 +514,7 @@ object consumer extends ConsumptionRules { wand, loss, lossExp, - SnapNeeded, + returnSnap, None, pve, v1 @@ -525,7 +527,7 @@ 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)), SnapNeeded, 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 _ => @@ -538,7 +540,7 @@ object consumer extends ConsumptionRules { } private def consumeConditionalTlcMoreJoins(s: State, h: Heap, e0: ast.Exp, a1: ast.Exp, a2: Option[ast.Exp], scopeUid: Int, - SnapNeeded: Boolean, + returnSnap: Boolean, pve: PartialVerificationError, v: Verifier) (Q: (State, Heap, Option[Term], Verifier) => VerificationResult) : VerificationResult = { @@ -546,19 +548,19 @@ object consumer extends ConsumptionRules { 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, SnapNeeded, 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, SnapNeeded, 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, Some(Unit)), v2) + QB(s2.copy(parallelizeBranches = s1.parallelizeBranches), (h, if (returnSnap) Some(Unit) else None), v2) }) })(entries => { val s2 = entries match { @@ -571,7 +573,12 @@ object consumer extends ConsumptionRules { entry2.data._1, And(entry2.pathConditions.branchConditions), Option.when(withExp)(BigAnd(entry2.pathConditions.branchConditionExps.map(_._2.get))), ), // Assume that entry1.pcs is inverse of entry2.pcs - Some(Ite(And(entry1.pathConditions.branchConditions), entry1.data._2.get, entry2.data._2.get)) + (entry1.data._2, entry2.data._2) match { + case (Some(t1), Some(t2)) => Some(Ite(And(entry1.pathConditions.branchConditions), t1, t2)) + case (Some(t1), None) => Some(t1) //This case and the next case should not be possible and would indicate a bug. + case (None, Some(t2)) => Some(t2) + case (None, None) => None + } ) (entry1.pathConditionAwareMergeWithoutConsolidation(entry2, v1), mergedData) case _ => diff --git a/src/main/scala/rules/Evaluator.scala b/src/main/scala/rules/Evaluator.scala index e4cd925c6..c50cef694 100644 --- a/src/main/scala/rules/Evaluator.scala +++ b/src/main/scala/rules/Evaluator.scala @@ -220,8 +220,7 @@ object evaluator extends EvaluationRules { * quantifier in whose body field 'fa.field' was accessed) * which is protected by a trigger term that we currently don't have. */ - v1.decider.prover.comment("reemit") - //v1.decider.assume(And(fvfDef.valueDefinitions), Option.when(withExp)(DebugExp.createInstance("Value definitions", isInternal_ = true))) + v1.decider.assume(And(fvfDef.valueDefinitions), Option.when(withExp)(DebugExp.createInstance("Value definitions", isInternal_ = true))) if (s1.heapDependentTriggers.contains(fa.field)){ val trigger = FieldTrigger(fa.field.name, fvfDef.sm, tRcvr) val triggerExp = Option.when(withExp)(DebugExp.createInstance(s"FieldTrigger(${eRcvr.toString()}.${fa.field.name})")) diff --git a/src/main/scala/rules/Executor.scala b/src/main/scala/rules/Executor.scala index ca1073152..64baaffcb 100644 --- a/src/main/scala/rules/Executor.scala +++ b/src/main/scala/rules/Executor.scala @@ -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)), true, 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))) diff --git a/src/main/scala/rules/QuantifiedChunkSupport.scala b/src/main/scala/rules/QuantifiedChunkSupport.scala index 8fab3118a..ea5981545 100644 --- a/src/main/scala/rules/QuantifiedChunkSupport.scala +++ b/src/main/scala/rules/QuantifiedChunkSupport.scala @@ -521,18 +521,10 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { smDomainDefinitionCondition, /* Alternatively: codomainQVarsInDomainOfSummarisingSm */ IsPositive(chunk.perm)) - val trigger = if (Verifier.config.disableISCTriggers()) { - Nil - } else if (s.heapDependentTriggers.contains(field)){ - Seq(Trigger(lookupSummary)) //, Trigger(lookupChunk)) - } else { - Seq(Trigger(lookupSummary)) - } - Forall( codomainQVar, Implies(effectiveCondition, BuiltinEquals(lookupSummary, lookupChunk)), - trigger, + if (Verifier.config.disableISCTriggers()) Nil else Seq(Trigger(lookupSummary), Trigger(lookupChunk)), s"qp.fvfValDef${v.counter(this).next()}", isGlobal = relevantQvars.isEmpty) }) @@ -624,18 +616,10 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { IsPositive(chunk.perm).replace(snapToCodomainTermsSubstitution)) } - val trigger = if (Verifier.config.disableISCTriggers()) { - Nil - } else if (s.heapDependentTriggers.contains(resourceIdentifier)){ - Seq(Trigger(lookupSummary), Trigger(lookupChunk)) - } else { - Seq(Trigger(lookupSummary)) - } - Forall( qvar, Implies(effectiveCondition, And(snapshotNotUnit, BuiltinEquals(lookupSummary, lookupChunk))), - trigger, + if (Verifier.config.disableISCTriggers()) Nil else Seq(Trigger(lookupSummary), Trigger(lookupChunk)), s"qp.psmValDef${v.counter(this).next()}", isGlobal = relevantQvars.isEmpty) }) @@ -828,7 +812,6 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { (smDef, s.smCache + (key, value)) } } - v.decider.prover.comment("SummarizingSnapshots") emitSnapshotMapDefinition(s, smDef, v, optQVarsInstantiations) (smDef, smCache) @@ -1170,7 +1153,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { eArgs: Option[Seq[ast.Exp]], tPerm: Term, ePerm: Option[ast.Exp], - SnapNeeded: Boolean, + returnSnap: Boolean, pve: PartialVerificationError, negativePermissionReason: => ErrorReason, notInjectiveReason: => ErrorReason, @@ -1391,10 +1374,10 @@ 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 - if(SnapNeeded) { + 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) @@ -1425,7 +1408,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { resourceAccess: ast.ResourceAccess, permissions: Term, /* p */ permissionsExp: Option[ast.Exp], - SnapNeeded: Boolean, + returnSnap: Boolean, optChunkOrderHeuristic: Option[Seq[QuantifiedBasicChunk] => Seq[QuantifiedBasicChunk]], pve: PartialVerificationError, v: Verifier) @@ -1517,7 +1500,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { result match { case (Complete(), s1, remainingChunks) => val h1 = Heap(remainingChunks ++ otherChunks) - if (SnapNeeded) { + if (returnSnap) { val (smDef1, smCache1) = quantifiedChunkSupporter.summarisingSnapshotMap( s = s1, diff --git a/src/main/scala/supporters/MethodSupporter.scala b/src/main/scala/supporters/MethodSupporter.scala index 8f2cccb2c..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, true, 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 845689009..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, true, postconditionViolated, v)((s3, _, _) => { + consumes(s2, posts, false, postconditionViolated, v)((s3, _, _) => { recorders :+= s3.functionRecorder Success()})})})} From e0b1373226425d3b365fa1b486c6ca73cfede466 Mon Sep 17 00:00:00 2001 From: mlimbeck Date: Wed, 20 Nov 2024 01:05:30 +0100 Subject: [PATCH 3/6] bug fixes in exhaleExt --- src/main/scala/rules/ChunkSupporter.scala | 15 +++-- src/main/scala/rules/Consumer.scala | 26 ++++---- src/main/scala/rules/Evaluator.scala | 2 +- src/main/scala/rules/Executor.scala | 2 +- .../rules/MoreCompleteExhaleSupporter.scala | 59 +++++++++++++------ .../scala/rules/QuantifiedChunkSupport.scala | 16 +++-- 6 files changed, 75 insertions(+), 45 deletions(-) diff --git a/src/main/scala/rules/ChunkSupporter.scala b/src/main/scala/rules/ChunkSupporter.scala index 5350131e1..9ae93abfc 100644 --- a/src/main/scala/rules/ChunkSupporter.scala +++ b/src/main/scala/rules/ChunkSupporter.scala @@ -83,7 +83,7 @@ object chunkSupporter extends ChunkSupportRules { optSnap match { case Some(snap) => Q(s2, h2, Some(snap.convert(sorts.Snap)), v2) - case None => + 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. * @@ -94,6 +94,7 @@ 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, Some(fresh), v2) + case None => Q(s2, h2, None, v2) }) } @@ -114,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 d00e17564..4855dbf55 100644 --- a/src/main/scala/rules/Consumer.scala +++ b/src/main/scala/rules/Consumer.scala @@ -121,7 +121,7 @@ object consumer extends ConsumptionRules { : VerificationResult = { if (tlcs.isEmpty) - Q(s, h, Some(Unit), v) + Q(s, h, if (returnSnap) Some(Unit) else None, v) else { val a = tlcs.head val pve = pves.head @@ -134,9 +134,8 @@ object consumer extends ConsumptionRules { (snap1, snap2) match { case (Some(sn1), Some(sn2)) => Q(s2, h2, Some(Combine(sn1, sn2)), v2) - case (Some(_), _) => Q(s2, h2, snap1, v2) //This case and the next case should not be possible and would indicate a bug. - case (None, Some(_)) => Q(s2, h2, snap2, v2) case (None, None) => Q(s2, h2, None, v2) + case (_, _) => sys.error(s"Consume returned unexpected snapshot: ${(returnSnap, (snap1, snap2))}") }) }) } @@ -217,7 +216,7 @@ object consumer extends ConsumptionRules { }), (s2, v2) => { v2.symbExLog.closeScope(uidImplies) - Q(s2, h, Some(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 => @@ -279,7 +278,7 @@ object consumer extends ConsumptionRules { notInjectiveReason = QPAssertionNotInjective(acc.loc), insufficientPermissionReason = InsufficientPermission(acc.loc), v1)(Q) - case (s1, _, _, _, _, None, v1) => Q(s1, h, Some(True), v1) + case (s1, _, _, _, _, None, v1) => Q(s1, h, if(returnSnap) Some(Unit) else None, v1) } case QuantifiedPermissionAssertion(forall, cond, acc: ast.PredicateAccessPredicate) => @@ -325,7 +324,7 @@ object consumer extends ConsumptionRules { notInjectiveReason = QPAssertionNotInjective(acc.loc), insufficientPermissionReason = InsufficientPermission(acc.loc), v1)(Q) - case (s1, _, _, _, _, None, v1) => Q(s1, h, Some(True), v1) + case (s1, _, _, _, _, None, v1) => Q(s1, h, if(returnSnap) Some(Unit) else None, v1) } case QuantifiedPermissionAssertion(forall, cond, wand: ast.MagicWand) => @@ -367,7 +366,7 @@ object consumer extends ConsumptionRules { notInjectiveReason = sys.error("Quantified wand not injective"), /*ReceiverNotInjective(...)*/ insufficientPermissionReason = MagicWandChunkNotFound(wand), /*InsufficientPermission(...)*/ v1)(Q) - case (s1, _, _, _, _, None, v1) => Q(s1, h, Some(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) @@ -531,8 +530,8 @@ object consumer extends ConsumptionRules { }) case _ => - evalAndAssert(s, a, pve, v)((s1, t, v1) => { - Q(s1, h, Some(t), v1) + evalAndAssert(s, a, returnSnap, pve, v)((s1, t, v1) => { + Q(s1, h, t, v1) }) } @@ -575,9 +574,8 @@ object consumer extends ConsumptionRules { // Assume that entry1.pcs is inverse of entry2.pcs (entry1.data._2, entry2.data._2) match { case (Some(t1), Some(t2)) => Some(Ite(And(entry1.pathConditions.branchConditions), t1, t2)) - case (Some(t1), None) => Some(t1) //This case and the next case should not be possible and would indicate a bug. - case (None, Some(t2)) => Some(t2) case (None, None) => None + case (_, _) => sys.error(s"Unexpected join data entries: $entries") } ) (entry1.pathConditionAwareMergeWithoutConsolidation(entry2, v1), mergedData) @@ -592,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 @@ -633,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 c50cef694..09c0e0120 100644 --- a/src/main/scala/rules/Evaluator.scala +++ b/src/main/scala/rules/Evaluator.scala @@ -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 64baaffcb..5840a01c3 100644 --- a/src/main/scala/rules/Executor.scala +++ b/src/main/scala/rules/Executor.scala @@ -516,7 +516,7 @@ 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, true, pve, v)((s2, _, v1) => { + consume(s, a, false, pve, v)((s2, _, v1) => { Q(s2.copy(h = s2.reserveHeaps.head), v1) }) } else diff --git a/src/main/scala/rules/MoreCompleteExhaleSupporter.scala b/src/main/scala/rules/MoreCompleteExhaleSupporter.scala index 1739866e1..4ee0d512e 100644 --- a/src/main/scala/rules/MoreCompleteExhaleSupporter.scala +++ b/src/main/scala/rules/MoreCompleteExhaleSupporter.scala @@ -203,15 +203,18 @@ 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 + actualConsumeComplete(s, h, resource, args, argsExp, perms, permsExp, returnSnap, ve, v)(Q) + else { + //What are we doing here? Can we reach this point with returnSnap= false? summariseHeapAndAssertReadAccess(s, h, resource, args, argsExp, ve, v)(Q) + } } private def summariseHeapAndAssertReadAccess(s: State, @@ -243,6 +246,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 +268,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 @@ -342,23 +347,36 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { val newHeap = Heap(allChunks) 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 = 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) + } else { + v1.decider.assert(pNeeded === NoPerm) { + case true => + Q(s1, newHeap, Some(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(s1, newHeap, Some(condSnap), v1) + Q(s0, newHeap, None, v) } else { - v1.decider.assert(pNeeded === NoPerm) { + v.decider.assert(pNeeded === NoPerm) { case true => - Q(s1, newHeap, Some(condSnap), v1) + Q(s0, newHeap, None, v) case false => - createFailure(ve, v1, s1, 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))) } - }}) + } + } } } } @@ -370,6 +388,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,8 +452,12 @@ 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()())())) diff --git a/src/main/scala/rules/QuantifiedChunkSupport.scala b/src/main/scala/rules/QuantifiedChunkSupport.scala index ea5981545..4ab808efb 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 @@ -629,7 +630,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { Forall( qvar, And(relevantChunks map (chunk => ResourceTriggerFunction(resource, chunk.snapshotMap, Seq(qvar), s.program))), - Trigger(ResourceLookup(resource, sm, Seq(qvar), s.program)), // +: (relevantChunks map (chunk => Trigger(ResourceLookup(resource, chunk.snapshotMap, Seq(qvar), s.program)))), + Trigger(ResourceLookup(resource, sm, Seq(qvar), s.program)), s"qp.psmResTrgDef${v.counter(this).next()}", isGlobal = relevantQvars.isEmpty) valueDefinitions :+ resourceTriggerDefinition @@ -1350,8 +1351,10 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { (result, s4, h2, Some(consumedChunk)) })((s4, optCh, v3) => optCh match { - case Some(ch) => Q(s4, s4.h, Some(ch.snapshotMap.convert(sorts.Snap)), v3) - case _ => Q(s4, s4.h, Some(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) //Why do we not record this new snapshot? + case _ => Q(s4, s4.h, None, v3) } ) } else { @@ -1472,11 +1475,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, Some(snap), v2) - case _ => - Q(s4, s4.h, Some(v2.decider.fresh(sorts.Snap, Option.when(withExp)(PUnknown()))), v2) + case None if returnSnap => + Q(s4, s4.h, Some(freshSnap(sorts.Snap, v2)), v2) //Why do we not record this new snapshot? + case _ => Q(s4, s4.h, None, v2) } ) } else { From 8033a59da5014756b6534f9076077b6189406ce6 Mon Sep 17 00:00:00 2001 From: mlimbeck Date: Tue, 26 Nov 2024 15:58:08 +0100 Subject: [PATCH 4/6] summariseHeapAndAssertReadAccess() optionally returns a snapshot --- .../rules/MoreCompleteExhaleSupporter.scala | 94 +++++++++---------- 1 file changed, 44 insertions(+), 50 deletions(-) diff --git a/src/main/scala/rules/MoreCompleteExhaleSupporter.scala b/src/main/scala/rules/MoreCompleteExhaleSupporter.scala index 4ee0d512e..7378ee65e 100644 --- a/src/main/scala/rules/MoreCompleteExhaleSupporter.scala +++ b/src/main/scala/rules/MoreCompleteExhaleSupporter.scala @@ -132,8 +132,9 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { argsExp: Option[Seq[ast.Exp]], 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 + returnSnap: Boolean, v: Verifier) - (Q: (State, Term, Seq[Term], Term, Option[ast.Exp], Verifier) => VerificationResult) + (Q: (State, Option[Term], Seq[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,28 +143,33 @@ 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, if (returnSnap) Some(chunk.snap) else None, Seq(), chunk.perm, chunk.permExp, v) } else { - return Q(s, chunk.snap, Seq(), NoPerm, Option.when(withExp)(ast.NoPerm()()), v) + return Q(s, if (returnSnap) Some(chunk.snap) else None, Seq(), NoPerm, Option.when(withExp)(ast.NoPerm()()), 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 */ + if(returnSnap) { + v.decider.assumeDefinition(And(snapDefs), Option.when(withExp)(DebugExp.createInstance("Snapshot", true))) + // v.decider.assume(PermAtMost(permSum, FullPerm())) /* Done in StateConsolidator instead */ - val s2 = - taggedSnap match { - case _: FreshSummarisingSnapshot => - val smd = SnapshotMapDefinition(resource, taggedSnap.snapshot, snapDefs, Seq.empty) - val fr2 = s1.functionRecorder.recordFvfAndDomain(smd) + val s2 = + taggedSnap match { + case _: FreshSummarisingSnapshot => + val smd = SnapshotMapDefinition(resource, taggedSnap.snapshot, snapDefs, Seq.empty) + val fr2 = s1.functionRecorder.recordFvfAndDomain(smd) - s1.copy(functionRecorder = fr2) - case _ => - s1 - } + s1.copy(functionRecorder = fr2) + case _ => + s1 + } - Q(s2, taggedSnap.snapshot, snapDefs, permSum, permSumExp, v) + Q(s2, Some(taggedSnap.snapshot), snapDefs, permSum, permSumExp, v) + } else { + Q(s1,None, snapDefs, permSum, permSumExp, v) + } } def lookupComplete(s: State, @@ -186,10 +192,10 @@ 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, true, v)((s1, snap, _, permSum, permSumExp, v1) => v.decider.assert(IsPositive(permSum)) { case true => - Q(s1, snap, v1) + Q(s1, snap.get, v1) case false => createFailure(ve, v, s1, IsPositive(permSum), permSumExp.map(IsPositive(_)())) }) @@ -212,8 +218,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { if (!s.hackIssue387DisablePermissionConsumption) actualConsumeComplete(s, h, resource, args, argsExp, perms, permsExp, returnSnap, ve, v)(Q) else { - //What are we doing here? Can we reach this point with returnSnap= false? - summariseHeapAndAssertReadAccess(s, h, resource, args, argsExp, ve, v)(Q) + summariseHeapAndAssertReadAccess(s, h, resource, args, argsExp, returnSnap, ve, v)(Q) } } @@ -222,6 +227,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) @@ -230,10 +236,10 @@ 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) => + summarise(s, relevantChunks, resource, args, argsExp, None, returnSnap, v)((s1, snap, _, permSum, permSumExp, v1) => v.decider.assert(IsPositive(permSum)) { case true => - Q(s1, h, Some(snap), v1) + Q(s1, h, snap, v1) case false => createFailure(ve, v, s1, IsPositive(permSum), permSumExp.map(IsPositive(_)())) }) @@ -347,36 +353,28 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { val newHeap = Heap(allChunks) val s0 = s.copy(functionRecorder = currentFunctionRecorder) - if (returnSnap) { - 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 (!moreNeeded) { - Q(s1, newHeap, Some(condSnap), v1) + + summarise(s0, relevantChunks.toSeq, resource, args, argsExp, Some(definiteAlias.map(_.snap)), returnSnap, v)((s1, snap, _, _, _, v1) => { + val condSnap = if (returnSnap) { + Some(if (v1.decider.check(IsPositive(perms), Verifier.config.checkTimeout())) { + snap.get } else { - v1.decider.assert(pNeeded === NoPerm) { - case true => - Q(s1, newHeap, Some(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 { + Ite(IsPositive(perms), snap.get.convert(sorts.Snap), Unit) + }) + } else { + None + } if (!moreNeeded) { - Q(s0, newHeap, None, v) + Q(s1, newHeap, condSnap, v1) } else { - v.decider.assert(pNeeded === NoPerm) { + v1.decider.assert(pNeeded === NoPerm) { case true => - Q(s0, newHeap, None, v) + Q(s1, newHeap, condSnap, v1) case false => - createFailure(ve, v, s0, pNeeded === NoPerm, pNeededExp.map(pn => ast.EqCmp(pn, ast.NoPerm()())(pn.pos, pn.info, pn.errT))) + createFailure(ve, v1, s1, pNeeded === NoPerm, pNeededExp.map(pn => ast.EqCmp(pn, ast.NoPerm()())(pn.pos, pn.info, pn.errT))) } } - } + }) } } } @@ -452,12 +450,8 @@ 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))) - 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) - } + summarise(s1, relevantChunks.toSeq, resource, args, argsExp, None, returnSnap, v)((s2, snap, _, _, _, v1) => + Q(s2, updatedChunks, snap, v1)) 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()())())) From 12ed299d0c9369f34301afe04e7588aab2dd31fb Mon Sep 17 00:00:00 2001 From: mlimbeck Date: Tue, 26 Nov 2024 17:06:44 +0100 Subject: [PATCH 5/6] remove comments, revert unnecessary changes --- src/main/scala/rules/Consumer.scala | 2 +- .../scala/rules/QuantifiedChunkSupport.scala | 17 ++++++++--------- 2 files changed, 9 insertions(+), 10 deletions(-) diff --git a/src/main/scala/rules/Consumer.scala b/src/main/scala/rules/Consumer.scala index 4855dbf55..c5b4aed2f 100644 --- a/src/main/scala/rules/Consumer.scala +++ b/src/main/scala/rules/Consumer.scala @@ -127,7 +127,7 @@ object consumer extends ConsumptionRules { val pve = pves.head if (tlcs.tail.isEmpty) - wrappedConsumeTlc(s, h, a, returnSnap, pve, v)(Q) + wrappedConsumeTlc(s, h, a, returnSnap, pve, v)(Q) else wrappedConsumeTlc(s, h, a, returnSnap, pve, v)((s1, h1, snap1, v1) => { consumeTlcs(s1, h1, tlcs.tail, returnSnap, pves.tail, v1)((s2, h2, snap2, v2) => diff --git a/src/main/scala/rules/QuantifiedChunkSupport.scala b/src/main/scala/rules/QuantifiedChunkSupport.scala index 4ab808efb..353d36e69 100644 --- a/src/main/scala/rules/QuantifiedChunkSupport.scala +++ b/src/main/scala/rules/QuantifiedChunkSupport.scala @@ -595,11 +595,6 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { SetIn(qvar, PredicateDomain(MagicWandIdentifier(wand, s.program).toString, sm)) } - val resourceIdentifier = resource match { - case wand: ast.MagicWand => MagicWandIdentifier(wand, s.program) - case r => r - } - val valueDefinitions = relevantChunks map (chunk => { val lookupSummary = ResourceLookup(resource, sm, Seq(qvar), s.program) @@ -611,11 +606,10 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { if (codomainQVars.nonEmpty) qvar !== Unit else qvar === Unit // TODO: Consider if axioms can be simplified in case codomainQVars is empty - val effectiveCondition = { + val effectiveCondition = And( transformedOptSmDomainDefinitionCondition.getOrElse(True), /* Alternatively: qvarInDomainOfSummarisingSm */ IsPositive(chunk.perm).replace(snapToCodomainTermsSubstitution)) - } Forall( qvar, @@ -625,6 +619,10 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { isGlobal = relevantQvars.isEmpty) }) + val resourceIdentifier = resource match { + case wand: ast.MagicWand => MagicWandIdentifier(wand, s.program) + case r => r + } val resourceAndValueDefinitions = if (s.heapDependentTriggers.contains(resourceIdentifier)){ val resourceTriggerDefinition = Forall( @@ -813,6 +811,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { (smDef, s.smCache + (key, value)) } } + emitSnapshotMapDefinition(s, smDef, v, optQVarsInstantiations) (smDef, smCache) @@ -1353,7 +1352,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { optCh match { 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) //Why do we not record this new snapshot? + Q(s4, s4.h, Some(freshSnap(sorts.Snap, v3)), v3) case _ => Q(s4, s4.h, None, v3) } ) @@ -1479,7 +1478,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { val snap = ResourceLookup(resource, ch.snapshotMap, arguments, s4.program).convert(sorts.Snap) Q(s4, s4.h, Some(snap), v2) case None if returnSnap => - Q(s4, s4.h, Some(freshSnap(sorts.Snap, v2)), v2) //Why do we not record this new snapshot? + Q(s4, s4.h, Some(freshSnap(sorts.Snap, v2)), v2) case _ => Q(s4, s4.h, None, v2) } ) From 77366a87d99bf40c77bd3c1e16a997341413206c Mon Sep 17 00:00:00 2001 From: mlimbeck Date: Wed, 27 Nov 2024 15:44:19 +0100 Subject: [PATCH 6/6] minor improvements and feedback --- src/main/scala/rules/ChunkSupporter.scala | 2 +- src/main/scala/rules/Consumer.scala | 16 +- .../rules/MoreCompleteExhaleSupporter.scala | 145 ++++++++++++------ .../scala/rules/QuantifiedChunkSupport.scala | 2 +- src/main/scala/state/package.scala | 2 +- 5 files changed, 105 insertions(+), 62 deletions(-) diff --git a/src/main/scala/rules/ChunkSupporter.scala b/src/main/scala/rules/ChunkSupporter.scala index 9ae93abfc..35ff5eb60 100644 --- a/src/main/scala/rules/ChunkSupporter.scala +++ b/src/main/scala/rules/ChunkSupporter.scala @@ -115,7 +115,7 @@ 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) => - if(returnSnap){ + if (returnSnap){ Q(s1, h, optCh.flatMap(ch => Some(ch.snap)), v1) } else { Q(s1, h, None, v1) diff --git a/src/main/scala/rules/Consumer.scala b/src/main/scala/rules/Consumer.scala index c5b4aed2f..fd3e34b94 100644 --- a/src/main/scala/rules/Consumer.scala +++ b/src/main/scala/rules/Consumer.scala @@ -133,8 +133,8 @@ object consumer extends ConsumptionRules { consumeTlcs(s1, h1, tlcs.tail, returnSnap, pves.tail, v1)((s2, h2, snap2, v2) => (snap1, snap2) match { - case (Some(sn1), Some(sn2)) => Q(s2, h2, Some(Combine(sn1, sn2)), v2) - case (None, None) => Q(s2, h2, None, v2) + 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))}") }) }) @@ -278,7 +278,7 @@ object consumer extends ConsumptionRules { notInjectiveReason = QPAssertionNotInjective(acc.loc), insufficientPermissionReason = InsufficientPermission(acc.loc), v1)(Q) - case (s1, _, _, _, _, None, v1) => Q(s1, h, if(returnSnap) Some(Unit) else None, v1) + case (s1, _, _, _, _, None, v1) => Q(s1, h, if (returnSnap) Some(Unit) else None, v1) } case QuantifiedPermissionAssertion(forall, cond, acc: ast.PredicateAccessPredicate) => @@ -324,7 +324,7 @@ object consumer extends ConsumptionRules { notInjectiveReason = QPAssertionNotInjective(acc.loc), insufficientPermissionReason = InsufficientPermission(acc.loc), v1)(Q) - case (s1, _, _, _, _, None, v1) => Q(s1, h, if(returnSnap) Some(Unit) else None, v1) + case (s1, _, _, _, _, None, v1) => Q(s1, h, if (returnSnap) Some(Unit) else None, v1) } case QuantifiedPermissionAssertion(forall, cond, wand: ast.MagicWand) => @@ -366,7 +366,7 @@ object consumer extends ConsumptionRules { notInjectiveReason = sys.error("Quantified wand not injective"), /*ReceiverNotInjective(...)*/ insufficientPermissionReason = MagicWandChunkNotFound(wand), /*InsufficientPermission(...)*/ v1)(Q) - case (s1, _, _, _, _, None, v1) => Q(s1, h, if(returnSnap) Some(Unit) else None, 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) @@ -573,8 +573,8 @@ object consumer extends ConsumptionRules { ), // Assume that entry1.pcs is inverse of entry2.pcs (entry1.data._2, entry2.data._2) match { - case (Some(t1), Some(t2)) => Some(Ite(And(entry1.pathConditions.branchConditions), t1, t2)) - case (None, None) => None + 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") } ) @@ -631,7 +631,7 @@ object consumer extends ConsumptionRules { val s5 = s4.copy(h = s.h, reserveHeaps = s.reserveHeaps, exhaleExt = s.exhaleExt) - Q(s5, if(returnSnap) Some(Unit) else None, v4) + Q(s5, if (returnSnap) Some(Unit) else None, v4) }) } } diff --git a/src/main/scala/rules/MoreCompleteExhaleSupporter.scala b/src/main/scala/rules/MoreCompleteExhaleSupporter.scala index 7378ee65e..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) @@ -132,9 +159,8 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { argsExp: Option[Seq[ast.Exp]], 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 - returnSnap: Boolean, v: Verifier) - (Q: (State, Option[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 @@ -143,33 +169,28 @@ 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, if (returnSnap) Some(chunk.snap) else None, Seq(), chunk.perm, chunk.permExp, v) + return Q(s, chunk.snap, chunk.perm, chunk.permExp, v) } else { - return Q(s, if (returnSnap) Some(chunk.snap) else None, 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) + v.decider.assumeDefinition(And(snapDefs), Option.when(withExp)(DebugExp.createInstance("Snapshot", true))) + // v.decider.assume(PermAtMost(permSum, FullPerm())) /* Done in StateConsolidator instead */ + + val s2 = + taggedSnap match { + case _: FreshSummarisingSnapshot => + val smd = SnapshotMapDefinition(resource, taggedSnap.snapshot, snapDefs, Seq.empty) + val fr2 = s1.functionRecorder.recordFvfAndDomain(smd) + + s1.copy(functionRecorder = fr2) + case _ => + s1 + } - if(returnSnap) { - v.decider.assumeDefinition(And(snapDefs), Option.when(withExp)(DebugExp.createInstance("Snapshot", true))) - // v.decider.assume(PermAtMost(permSum, FullPerm())) /* Done in StateConsolidator instead */ - - val s2 = - taggedSnap match { - case _: FreshSummarisingSnapshot => - val smd = SnapshotMapDefinition(resource, taggedSnap.snapshot, snapDefs, Seq.empty) - val fr2 = s1.functionRecorder.recordFvfAndDomain(smd) - - s1.copy(functionRecorder = fr2) - case _ => - s1 - } - - Q(s2, Some(taggedSnap.snapshot), snapDefs, permSum, permSumExp, v) - } else { - Q(s1,None, snapDefs, permSum, permSumExp, v) - } + Q(s2, taggedSnap.snapshot, permSum, permSumExp, v) } def lookupComplete(s: State, @@ -192,10 +213,10 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { createFailure(ve, v, s, False, "branch is dead") } } else { - summarise(s, relevantChunks, resource, args, argsExp, None, true, 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.get, v1) + Q(s1, snap, v1) case false => createFailure(ve, v, s1, IsPositive(permSum), permSumExp.map(IsPositive(_)())) }) @@ -235,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, returnSnap, 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, snap, v1) + Q(s1, h, None, v) case false => createFailure(ve, v, s1, IsPositive(permSum), permSumExp.map(IsPositive(_)())) - }) + } + } } private def actualConsumeComplete(s: State, @@ -354,16 +384,15 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { val s0 = s.copy(functionRecorder = currentFunctionRecorder) - summarise(s0, relevantChunks.toSeq, resource, args, argsExp, Some(definiteAlias.map(_.snap)), returnSnap, v)((s1, snap, _, _, _, v1) => { - val condSnap = if (returnSnap) { - Some(if (v1.decider.check(IsPositive(perms), Verifier.config.checkTimeout())) { - snap.get + + + 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.get.convert(sorts.Snap), Unit) + Ite(IsPositive(perms), snap.convert(sorts.Snap), Unit) }) - } else { - None - } if (!moreNeeded) { Q(s1, newHeap, condSnap, v1) } else { @@ -375,6 +404,18 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { } } }) + } 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))) + } + } + } } } } @@ -450,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, returnSnap, v)((s2, snap, _, _, _, v1) => - Q(s2, updatedChunks, 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/QuantifiedChunkSupport.scala b/src/main/scala/rules/QuantifiedChunkSupport.scala index 353d36e69..a05e39aa4 100644 --- a/src/main/scala/rules/QuantifiedChunkSupport.scala +++ b/src/main/scala/rules/QuantifiedChunkSupport.scala @@ -1376,7 +1376,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { permissionRemovalResult match { case (Complete(), s2, remainingChunks) => val h3 = Heap(remainingChunks ++ otherChunks) - if(returnSnap) { + if (returnSnap) { val optSmDomainDefinitionCondition2 = if (s2.smDomainNeeded) Some(And(condOfInvOfLoc, IsPositive(lossOfInvOfLoc), And(And(imagesOfFormalQVars)))) else None 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])] }