Skip to content

Commit

Permalink
summariseHeapAndAssertReadAccess() optionally returns a snapshot
Browse files Browse the repository at this point in the history
  • Loading branch information
@mlimbeck
mlimbeck committed Nov 26, 2024
1 parent e0b1373 commit 8033a59
Showing 1 changed file with 44 additions and 50 deletions.
94 changes: 44 additions & 50 deletions src/main/scala/rules/MoreCompleteExhaleSupporter.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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,
Expand All @@ -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(_)()))
})
Expand All @@ -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)
}
}

Expand All @@ -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)
Expand All @@ -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(_)()))
})
Expand Down Expand Up @@ -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)))
}
}
}
})
}
}
}
Expand Down Expand Up @@ -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()())()))
Expand Down

0 comments on commit 8033a59

Please sign in to comment.