From ba4537a9c8c6208031629e376f4053eb632b6822 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Sun, 2 Feb 2025 12:30:24 +0100 Subject: [PATCH] Fixing wildcards that are marked as constrainable for too long (#893) --- silver | 2 +- src/main/scala/rules/Consumer.scala | 8 ++++---- src/main/scala/rules/Evaluator.scala | 5 +++-- src/main/scala/rules/Executor.scala | 2 ++ src/main/scala/rules/Producer.scala | 16 ++++++++++------ 5 files changed, 20 insertions(+), 13 deletions(-) diff --git a/silver b/silver index 16a00271..2c71dc1a 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 16a00271533d28f32af19875b62085302bec0149 +Subproject commit 2c71dc1ae81eb6710e3f4feaf3d393afe1da4b60 diff --git a/src/main/scala/rules/Consumer.scala b/src/main/scala/rules/Consumer.scala index fd3e34b9..d15f1b88 100644 --- a/src/main/scala/rules/Consumer.scala +++ b/src/main/scala/rules/Consumer.scala @@ -277,7 +277,7 @@ object consumer extends ConsumptionRules { negativePermissionReason = NegativePermission(acc.perm), notInjectiveReason = QPAssertionNotInjective(acc.loc), insufficientPermissionReason = InsufficientPermission(acc.loc), - v1)(Q) + v1)((s2, h2, snap, v2) => Q(s2.copy(constrainableARPs = s.constrainableARPs), h2, snap, v2)) case (s1, _, _, _, _, None, v1) => Q(s1, h, if (returnSnap) Some(Unit) else None, v1) } @@ -323,7 +323,7 @@ object consumer extends ConsumptionRules { negativePermissionReason = NegativePermission(acc.perm), notInjectiveReason = QPAssertionNotInjective(acc.loc), insufficientPermissionReason = InsufficientPermission(acc.loc), - v1)(Q) + v1)((s2, h2, snap, v2) => Q(s2.copy(constrainableARPs = s.constrainableARPs), h2, snap, v2)) case (s1, _, _, _, _, None, v1) => Q(s1, h, if (returnSnap) Some(Unit) else None, v1) } @@ -365,8 +365,8 @@ object consumer extends ConsumptionRules { negativePermissionReason = NegativePermission(ePerm), 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) + v1)((s2, h2, snap, v2) => Q(s2.copy(constrainableARPs = s.constrainableARPs), h2, snap, v2)) + case (s1, _, _, _, _, None, v1) => Q(s1.copy(constrainableARPs = s.constrainableARPs), h, if (returnSnap) Some(Unit) else None, v1) } case accPred@ast.AccessPredicate(loc @ ast.FieldAccess(eRcvr, field), ePerm) diff --git a/src/main/scala/rules/Evaluator.scala b/src/main/scala/rules/Evaluator.scala index c0623d9d..ee67ccf4 100644 --- a/src/main/scala/rules/Evaluator.scala +++ b/src/main/scala/rules/Evaluator.scala @@ -1006,13 +1006,14 @@ object evaluator extends EvaluationRules { 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) + val s7a = s7.copy(g = insg).setConstrainable(s7.constrainableARPs, false) 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, permissionScalingFactor = s6.permissionScalingFactor, - permissionScalingFactorExp = s6.permissionScalingFactorExp) + permissionScalingFactorExp = s6.permissionScalingFactorExp, + constrainableARPs = s1.constrainableARPs) .decCycleCounter(predicate) val s10 = v5.stateConsolidator(s9).consolidateOptionally(s9, v5) eval(s10, eIn, pve, v5)((s9, t9, e9, v9) => QB(s9, (t9, e9), v9))})}) diff --git a/src/main/scala/rules/Executor.scala b/src/main/scala/rules/Executor.scala index 99461b5d..5edef113 100644 --- a/src/main/scala/rules/Executor.scala +++ b/src/main/scala/rules/Executor.scala @@ -602,6 +602,7 @@ object executor extends ExecutionRules { Q(s6, v3)})})}) case fold @ ast.Fold(pap @ ast.PredicateAccessPredicate(predAcc @ ast.PredicateAccess(eArgs, predicateName), _)) => + assert(s.constrainableARPs.isEmpty) v.decider.startDebugSubExp() val ePerm = pap.perm val predicate = s.program.findPredicate(predicateName) @@ -617,6 +618,7 @@ object executor extends ExecutionRules { )}))) case unfold @ ast.Unfold(pap @ ast.PredicateAccessPredicate(pa @ ast.PredicateAccess(eArgs, predicateName), _)) => + assert(s.constrainableARPs.isEmpty) v.decider.startDebugSubExp() val ePerm = pap.perm val predicate = s.program.findPredicate(predicateName) diff --git a/src/main/scala/rules/Producer.scala b/src/main/scala/rules/Producer.scala index 605fd30d..6b613ba9 100644 --- a/src/main/scala/rules/Producer.scala +++ b/src/main/scala/rules/Producer.scala @@ -321,7 +321,8 @@ object producer extends ProductionRules { val perm = accPred.perm eval(s, eRcvr, pve, v)((s1, tRcvr, eRcvrNew, v1) => eval(s1, perm, pve, v1)((s2, tPerm, ePermNew, v2) => - permissionSupporter.assertNotNegative(s2, tPerm, perm, ePermNew, pve, v2)((s3, v3) => { + permissionSupporter.assertNotNegative(s2, tPerm, perm, ePermNew, pve, v2)((s2a, v3) => { + val s3 = s2a.copy(constrainableARPs = s.constrainableARPs) val snap = sf(v3.symbolConverter.toSort(field.typ), v3) val gain = if (!Verifier.config.unsafeWildcardOptimization() || s2.permLocations.contains(field)) PermTimes(tPerm, s3.permissionScalingFactor) @@ -347,7 +348,8 @@ object producer extends ProductionRules { val perm = accPred.perm evals(s, eArgs, _ => pve, v)((s1, tArgs, eArgsNew, v1) => eval(s1, perm, pve, v1)((s1a, tPerm, ePermNew, v1a) => - permissionSupporter.assertNotNegative(s1a, tPerm, perm, ePermNew, pve, v1a)((s2, v2) => { + permissionSupporter.assertNotNegative(s1a, tPerm, perm, ePermNew, pve, v1a)((s1b, v2) => { + val s2 = s1b.copy(constrainableARPs = s.constrainableARPs) val snap = sf( predicate.body.map(v2.snapshotSupporter.optimalSnapshotSort(_, s.program)._1) .getOrElse(sorts.Snap), v2) @@ -430,8 +432,9 @@ object producer extends ProductionRules { evalQuantified(s, Forall, forall.variables, Seq(cond), Seq(acc.loc.rcv, acc.perm), optTrigger, qid, pve, v) { case (s1, qvars, qvarExps, Seq(tCond), eCondNew, Some((Seq(tRcvr, tPerm), rcvrPerm, tTriggers, (auxGlobals, auxNonGlobals), auxExps)), v1) => val tSnap = sf(sorts.FieldValueFunction(v1.symbolConverter.toSort(acc.loc.field.typ), acc.loc.field.name), v1) + val s1a = s1.copy(constrainableARPs = s.constrainableARPs) quantifiedChunkSupporter.produce( - s1, + s1a, forall, acc.loc.field, qvars, qvarExps, Seq(`?r`), @@ -454,7 +457,7 @@ object producer extends ProductionRules { QPAssertionNotInjective(acc.loc), v1 )(Q) - case (s1, _, _, _, _, None, v1) => Q(s1, v1) + case (s1, _, _, _, _, None, v1) => Q(s1.copy(constrainableARPs = s.constrainableARPs), v1) } case QuantifiedPermissionAssertion(forall, cond, acc: ast.PredicateAccessPredicate) => @@ -468,8 +471,9 @@ object producer extends ProductionRules { evalQuantified(s, Forall, forall.variables, Seq(cond), acc.perm +: acc.loc.args, optTrigger, qid, pve, v) { case (s1, qvars, qvarExps, Seq(tCond), eCondNew, Some((Seq(tPerm, tArgs @ _*), permArgs, tTriggers, (auxGlobals, auxNonGlobals), auxExps)), v1) => val tSnap = sf(sorts.PredicateSnapFunction(s1.predicateSnapMap(predicate), predicate.name), v1) + val s1a = s1.copy(constrainableARPs = s.constrainableARPs) quantifiedChunkSupporter.produce( - s1, + s1a, forall, predicate, qvars, @@ -495,7 +499,7 @@ object producer extends ProductionRules { QPAssertionNotInjective(acc.loc), v1 )(Q) - case (s1, _, _, _, _, None, v1) => Q(s1, v1) + case (s1, _, _, _, _, None, v1) => Q(s1.copy(constrainableARPs = s.constrainableARPs), v1) } case QuantifiedPermissionAssertion(forall, cond, wand: ast.MagicWand) =>