Skip to content

Fixing issue #842 #843

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
marcoeilers merged 3 commits into from
May 6, 2024
Merged

Fixing issue #842 #843

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
0510154
Making sure verification continues after assuming potentially unsatis…
marcoeilers May 6, 2024
bd9d821
Updated tests
marcoeilers May 6, 2024
efba03c
Cleanup
marcoeilers May 6, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion silver
Open in desktop
Submodule silver updated 1 files
+47 −0 src/test/resources/all/issues/silicon/0842.vpr
14 changes: 9 additions & 5 deletions src/main/scala/rules/Consumer.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -122,9 +122,9 @@ object consumer extends ConsumptionRules {
if (tlcs.tail.isEmpty)
wrappedConsumeTlc(s, h, a, pve, v)(Q)
else
wrappedConsumeTlc(s, h, a, pve, v)((s1, h1, snap1, v1) =>
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)))
Q(s2, h2, Combine(snap1, snap2), v2))})
}
}

Expand Down Expand Up @@ -234,8 +234,9 @@ object consumer extends ConsumptionRules {
val optTrigger =
if (forall.triggers.isEmpty) None
else Some(forall.triggers)

evalQuantified(s, Forall, forall.variables, Seq(cond), Seq(acc.perm, acc.loc.rcv), optTrigger, qid.name, pve, v) {
case (s1, qvars, Seq(tCond), Seq(tPerm, tRcvr), tTriggers, (auxGlobals, auxNonGlobals), v1) =>
case (s1, qvars, Seq(tCond), Some((Seq(tPerm, tRcvr), tTriggers, (auxGlobals, auxNonGlobals))), v1) =>
quantifiedChunkSupporter.consume(
s = s1,
h = h,
Expand All @@ -255,6 +256,7 @@ object consumer extends ConsumptionRules {
notInjectiveReason = QPAssertionNotInjective(acc.loc),
insufficientPermissionReason = InsufficientPermission(acc.loc),
v1)(Q)
case (s1, _, _, None, v1) => Q(s1, h, True, v1)
}

case QuantifiedPermissionAssertion(forall, cond, acc: ast.PredicateAccessPredicate) =>
Expand All @@ -272,7 +274,7 @@ object consumer extends ConsumptionRules {
if (forall.triggers.isEmpty) None
else Some(forall.triggers)
evalQuantified(s, Forall, forall.variables, Seq(cond), acc.perm +: acc.loc.args, optTrigger, qid.name, pve, v) {
case (s1, qvars, Seq(tCond), Seq(tPerm, tArgs @ _*), tTriggers, (auxGlobals, auxNonGlobals), v1) =>
case (s1, qvars, Seq(tCond), Some((Seq(tPerm, tArgs @ _*), tTriggers, (auxGlobals, auxNonGlobals))), v1) =>
quantifiedChunkSupporter.consume(
s = s1,
h = h,
Expand All @@ -292,6 +294,7 @@ object consumer extends ConsumptionRules {
notInjectiveReason = QPAssertionNotInjective(acc.loc),
insufficientPermissionReason = InsufficientPermission(acc.loc),
v1)(Q)
case (s1, _, _, None, v1) => Q(s1, h, True, v1)
}

case QuantifiedPermissionAssertion(forall, cond, wand: ast.MagicWand) =>
Expand All @@ -304,7 +307,7 @@ object consumer extends ConsumptionRules {
val ePerm = ast.FullPerm()()
val tPerm = FullPerm
evalQuantified(s, Forall, forall.variables, Seq(cond), bodyVars, optTrigger, qid, pve, v) {
case (s1, qvars, Seq(tCond), tArgs, tTriggers, (auxGlobals, auxNonGlobals), v1) =>
case (s1, qvars, Seq(tCond), Some((tArgs, tTriggers, (auxGlobals, auxNonGlobals))), v1) =>
quantifiedChunkSupporter.consume(
s = s1,
h = h,
Expand All @@ -324,6 +327,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, True, v1)
}

case ast.AccessPredicate(loc @ ast.FieldAccess(eRcvr, field), ePerm)
Expand Down
49 changes: 39 additions & 10 deletions src/main/scala/rules/Evaluator.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ package viper.silicon.rules
import viper.silicon.Config.JoinMode
import viper.silver.ast
import viper.silver.verifier.{CounterexampleTransformer, PartialVerificationError, VerifierWarning}
import viper.silver.verifier.errors.{ErrorWrapperWithExampleTransformer, PreconditionInAppFalse}
import viper.silver.verifier.errors.{ErrorWrapperWithExampleTransformer, Internal, PreconditionInAppFalse}
import viper.silver.verifier.reasons._
import viper.silicon.common.collections.immutable.InsertionOrderedSet
import viper.silicon.interfaces._
Expand Down Expand Up @@ -57,7 +57,7 @@ trait EvaluationRules extends SymbolicExecutionRules {
name: String,
pve: PartialVerificationError,
v: Verifier)
(Q: (State, Seq[Var], Seq[Term], Seq[Term], Seq[Trigger], (Seq[Term], Seq[Quantification]), Verifier) => VerificationResult)
(Q: (State, Seq[Var], Seq[Term], Option[(Seq[Term], Seq[Trigger], (Seq[Term], Seq[Quantification]))], Verifier) => VerificationResult)
: VerificationResult
}

Expand Down Expand Up @@ -722,7 +722,7 @@ object evaluator extends EvaluationRules {
}
val name = s"prog.$posString"
evalQuantified(s, qantOp, eQuant.variables, Nil, Seq(body), Some(eTriggers), name, pve, v){
case (s1, tVars, _, Seq(tBody), tTriggers, (tAuxGlobal, tAux), v1) =>
case (s1, tVars, _, Some((Seq(tBody), tTriggers, (tAuxGlobal, tAux))), v1) =>
val tAuxHeapIndep = tAux.flatMap(v.quantifierSupporter.makeTriggersHeapIndependent(_, v1.decider.fresh))

v1.decider.prover.comment("Nested auxiliary terms: globals (aux)")
Expand All @@ -742,6 +742,13 @@ object evaluator extends EvaluationRules {

val tQuant = Quantification(qantOp, tVars, tBody, tTriggers, name, quantWeight)
Q(s1, tQuant, v1)
case (s1, _, _, None, v1) =>
// This should not happen unless the current path is dead.
if (v1.decider.checkSmoke(true)) {
Unreachable()
} else {
createFailure(pve.dueTo(InternalReason(sourceQuant, "Quantifier evaluation failed.")), v1, s1)
}
}

case fapp @ ast.FuncApp(funcName, eArgs) =>
Expand Down Expand Up @@ -1114,7 +1121,15 @@ object evaluator extends EvaluationRules {
name: String,
pve: PartialVerificationError,
v: Verifier)
(Q: (State, Seq[Var], Seq[Term], Seq[Term], Seq[Trigger], (Seq[Term], Seq[Quantification]), Verifier) => VerificationResult)
(Q: (State,
Seq[Var], /* Variables from vars */
Seq[Term], /* Terms from es1 */
Option[( /* None if es2 or trigger evaluation did not result in a term because es1 is unsatisfiable */
Seq[Term], /* Terms from es2 */
Seq[Trigger], /* Triggers from optTriggers */
(Seq[Term], Seq[Quantification]) /* Global and non-global auxiliary assumptions */
)],
Verifier) => VerificationResult)
: VerificationResult = {

val localVars = vars map (_.localVar)
Expand All @@ -1125,23 +1140,37 @@ object evaluator extends EvaluationRules {
quantifiedVariables = tVars ++ s.quantifiedVariables,
recordPossibleTriggers = true,
possibleTriggers = Map.empty) // TODO: Why reset possibleTriggers if they are merged with s.possibleTriggers later anyway?
type R = (State, Seq[Term], Seq[Term], Seq[Trigger], (Seq[Term], Seq[Quantification]), Map[ast.Exp, Term])
type R = (State, Seq[Term], Option[(Seq[Term], Seq[Trigger], (Seq[Term], Seq[Quantification]), Map[ast.Exp, Term])])
executionFlowController.locallyWithResult[R](s1, v)((s2, v1, QB) => {
val preMark = v1.decider.setPathConditionMark()
evals(s2, es1, _ => pve, v1)((s3, ts1, v2) => {
val bc = And(ts1)
// ME: If bc is unsatisfiable, we are assuming false here. In that case, evaluating es2 and the triggers
// may not return any value (e.g. if es2 contains a field read for which we don't have permission, a smoke
// check succeeds, then the continuation for evals(es2) is never invoked). This caused issue #842.
// In this case, we return None.
v2.decider.setCurrentBranchCondition(bc, Some(viper.silicon.utils.ast.BigAnd(es1)))
evals(s3, es2, _ => pve, v2)((s4, ts2, v3) => {
var es2AndTriggerTerms: Option[(Seq[Term], Seq[Trigger], (Seq[Term], Seq[Quantification]), Map[ast.Exp, Term])] = None
var finalState = s3
val es2AndTriggerResult = evals(s3, es2, _ => pve, v2)((s4, ts2, v3) => {
evalTriggers(s4, optTriggers.getOrElse(Nil), pve, v3)((s5, tTriggers, _) => { // TODO: v4 isn't forward - problem?
val (auxGlobals, auxNonGlobalQuants) =
v3.decider.pcs.after(preMark).quantified(quant, tVars, tTriggers, s"$name-aux", isGlobal = false, bc)
val additionalPossibleTriggers: Map[ast.Exp, Term] =
if (s.recordPossibleTriggers) s5.possibleTriggers else Map()
QB((s5, ts1, ts2, tTriggers, (auxGlobals, auxNonGlobalQuants), additionalPossibleTriggers))})})})
}){case (s2, ts1, ts2, tTriggers, (tAuxGlobal, tAux), additionalPossibleTriggers) =>
val s3 = s.copy(possibleTriggers = s.possibleTriggers ++ additionalPossibleTriggers)
es2AndTriggerTerms = Some((ts2, tTriggers, (auxGlobals, auxNonGlobalQuants), additionalPossibleTriggers))
finalState = s5
Success()
})})
es2AndTriggerResult combine QB((finalState, ts1, es2AndTriggerTerms))
})
}){
case (s2, ts1, Some((ts2, tTriggers, (tAuxGlobal, tAux), additionalPossibleTriggers))) =>
val s3 = s.copy(possibleTriggers = s.possibleTriggers ++ additionalPossibleTriggers)
.preserveAfterLocalEvaluation(s2)
Q(s3, tVars, ts1, ts2, tTriggers, (tAuxGlobal, tAux), v)
Q(s3, tVars, ts1, Some((ts2, tTriggers, (tAuxGlobal, tAux))), v)
case (s2, ts1, None) =>
Q(s2, tVars, ts1, None, v)
}
}

Expand Down
3 changes: 2 additions & 1 deletion src/main/scala/rules/HavocSupporter.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -104,7 +104,7 @@ object havocSupporter extends SymbolicExecutionRules {
pve = pve,
v = v)
{
case (s1, tVars, Seq(tCond), tArgs, Seq(), _, v1) =>
case (s1, tVars, Seq(tCond), Some((tArgs, Seq(), _)), v1) =>
// Seq() represents an empty list of Triggers
// TODO: unnamed argument is (tAuxGlobal, tAux). How should these be handled?

Expand Down Expand Up @@ -154,6 +154,7 @@ object havocSupporter extends SymbolicExecutionRules {

Q(s1.copy(h = Heap(newChunks)), v1)
}
case (s1, _, _, None, v1) => Q(s1, v1)
}
}

Expand Down
9 changes: 6 additions & 3 deletions src/main/scala/rules/Producer.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -411,7 +411,7 @@ object producer extends ProductionRules {
if (forall.triggers.isEmpty) None
else Some(forall.triggers)
evalQuantified(s, Forall, forall.variables, Seq(cond), Seq(acc.loc.rcv, acc.perm), optTrigger, qid, pve, v) {
case (s1, qvars, Seq(tCond), Seq(tRcvr, tPerm), tTriggers, (auxGlobals, auxNonGlobals), v1) =>
case (s1, qvars, Seq(tCond), Some((Seq(tRcvr, tPerm), tTriggers, (auxGlobals, auxNonGlobals))), v1) =>
val tSnap = sf(sorts.FieldValueFunction(v1.symbolConverter.toSort(acc.loc.field.typ), acc.loc.field.name), v1)
// v.decider.assume(PermAtMost(tPerm, FullPerm()))
quantifiedChunkSupporter.produce(
Expand All @@ -432,6 +432,7 @@ object producer extends ProductionRules {
QPAssertionNotInjective(acc.loc),
v1
)(Q)
case (s1, _, _, None, v1) => Q(s1, v1)
}

case QuantifiedPermissionAssertion(forall, cond, acc: ast.PredicateAccessPredicate) =>
Expand All @@ -442,7 +443,7 @@ object producer extends ProductionRules {
if (forall.triggers.isEmpty) None
else Some(forall.triggers)
evalQuantified(s, Forall, forall.variables, Seq(cond), acc.perm +: acc.loc.args, optTrigger, qid, pve, v) {
case (s1, qvars, Seq(tCond), Seq(tPerm, tArgs @ _*), tTriggers, (auxGlobals, auxNonGlobals), v1) =>
case (s1, qvars, Seq(tCond), Some((Seq(tPerm, tArgs @ _*), tTriggers, (auxGlobals, auxNonGlobals))), v1) =>
val tSnap = sf(sorts.PredicateSnapFunction(s1.predicateSnapMap(predicate), predicate.name), v1)
quantifiedChunkSupporter.produce(
s1,
Expand All @@ -464,6 +465,7 @@ object producer extends ProductionRules {
QPAssertionNotInjective(acc.loc),
v1
)(Q)
case (s1, _, _, None, v1) => Q(s1, v1)
}

case QuantifiedPermissionAssertion(forall, cond, wand: ast.MagicWand) =>
Expand All @@ -474,7 +476,7 @@ object producer extends ProductionRules {
else Some(forall.triggers)
val qid = MagicWandIdentifier(wand, s.program).toString
evalQuantified(s, Forall, forall.variables, Seq(cond), bodyVars, optTrigger, qid, pve, v) {
case (s1, qvars, Seq(tCond), tArgs, tTriggers, (auxGlobals, auxNonGlobals), v1) =>
case (s1, qvars, Seq(tCond), Some((tArgs, tTriggers, (auxGlobals, auxNonGlobals))), v1) =>
val tSnap = sf(sorts.PredicateSnapFunction(sorts.Snap, qid), v1)
quantifiedChunkSupporter.produce(
s1,
Expand All @@ -496,6 +498,7 @@ object producer extends ProductionRules {
QPAssertionNotInjective(wand),
v1
)(Q)
case (s1, _, _, None, v1) => Q(s1, v1)
}

case _: ast.InhaleExhaleExp =>
Expand Down
⚡