Skip to content

Commit

Permalink
Making sure verification continues after assuming potentially unsatis…
Browse files Browse the repository at this point in the history 
…fiable condition in evalQuantified
  • Loading branch information
@marcoeilers
marcoeilers committed May 6, 2024
1 parent 59f3acd commit 0510154
Show file tree
Hide file tree
Showing 5 changed files with 57 additions and 20 deletions.
2 changes: 1 addition & 1 deletion silver
Submodule silver updated 2 files
+20 −0 src/test/resources/all/issues/silicon/0842a.vpr
+2,620 −0 src/test/resources/all/issues/silicon/0842b.vpr
14 changes: 9 additions & 5 deletions src/main/scala/rules/Consumer.scala
View file
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
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)) // QB((s5, ts1, 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
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
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

0 comments on commit 0510154

Please sign in to comment.