Skip to content

Commit

Permalink
bug fixes in exhaleExt
Browse files Browse the repository at this point in the history
  • Loading branch information
@mlimbeck
mlimbeck committed Nov 20, 2024
1 parent 5f9ea43 commit e0b1373
Show file tree
Hide file tree
Showing 6 changed files with 75 additions and 45 deletions.
15 changes: 10 additions & 5 deletions src/main/scala/rules/ChunkSupporter.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.
*
Expand All @@ -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)
})
}

Expand All @@ -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) =>
Expand Down
26 changes: 12 additions & 14 deletions src/main/scala/rules/Consumer.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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))}")
})
})
}
Expand Down Expand Up @@ -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 =>
Expand Down Expand Up @@ -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) =>
Expand Down Expand Up @@ -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) =>
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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)
})
}

Expand Down Expand Up @@ -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)
Expand All @@ -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
Expand Down Expand Up @@ -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)
})
}
}
2 changes: 1 addition & 1 deletion src/main/scala/rules/Evaluator.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)
})
Expand Down
2 changes: 1 addition & 1 deletion src/main/scala/rules/Executor.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
59 changes: 41 additions & 18 deletions src/main/scala/rules/MoreCompleteExhaleSupporter.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down Expand Up @@ -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)
Expand All @@ -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
Expand Down Expand Up @@ -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)))
}
}})
}
}
}
}
}
Expand All @@ -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)
Expand Down Expand Up @@ -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()())()))
Expand Down
16 changes: 10 additions & 6 deletions src/main/scala/rules/QuantifiedChunkSupport.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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 {
Expand Down Expand Up @@ -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 {
Expand Down

0 comments on commit e0b1373

Please sign in to comment.