diff --git a/src/main/scala/Config.scala b/src/main/scala/Config.scala index 6acf1ed71..f2a5d236f 100644 --- a/src/main/scala/Config.scala +++ b/src/main/scala/Config.scala @@ -160,6 +160,12 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") { noshort = true ) + val avoidReverifyingWelldefinedness: ScallopOption[Boolean] = opt[Boolean]("avoidReverifyingWelldefinedness", + descr = "Do not re-verify well-definedness of contracts or predicates when using them", + default = Some(false), + noshort = true + ) + val includeMethods: ScallopOption[String] = opt[String]("includeMethods", descr = "Include methods in verification (default: '*'). Wildcard characters are '?' and '*'. ", default = Some(".*"), diff --git a/src/main/scala/decider/Decider.scala b/src/main/scala/decider/Decider.scala index 9c27fc4e9..fd54e2ff5 100644 --- a/src/main/scala/decider/Decider.scala +++ b/src/main/scala/decider/Decider.scala @@ -49,7 +49,10 @@ trait Decider { * 1. It passes State and Operations to the continuation * 2. The implementation reacts to a failing assertion by e.g. a state consolidation */ - def assert(t: Term, timeout: Option[Int] = None)(Q: Boolean => VerificationResult): VerificationResult + def assertRaw(t: Term, timeout: Option[Int] = None)(Q: Boolean => VerificationResult): VerificationResult + + def assertWD(t: Term, s: State, v: Verifier, timeout: Option[Int] = None)(Q: Boolean => VerificationResult): VerificationResult + def assertC(t: Term, s: State, v: Verifier, timeout: Option[Int] = None)(Q: Boolean => VerificationResult): VerificationResult def fresh(id: String, sort: Sort): Var def fresh(id: String, argSorts: Seq[Sort], resultSort: Sort): Function @@ -243,9 +246,30 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier => def check(t: Term, timeout: Int): Boolean = deciderAssert(t, Some(timeout)) - def assert(t: Term, timeout: Option[Int] = Verifier.config.assertTimeout.toOption) - (Q: Boolean => VerificationResult) - : VerificationResult = { + def assertC(t: Term, s: State, v: Verifier, timeout: Option[Int] = Verifier.config.assertTimeout.toOption) + (Q: Boolean => VerificationResult) + : VerificationResult = { + if (s.isKnownCorrect) { + Q(true) + } else { + assertRaw(t, timeout)(Q) + } + } + + def assertWD(t: Term, s: State, v: Verifier, timeout: Option[Int] = Verifier.config.assertTimeout.toOption) + (Q: Boolean => VerificationResult) + : VerificationResult = { + if ((Verifier.config.avoidReverifyingWelldefinedness() && s.isKnownWelldefined) || s.isKnownCorrect) { + // TODO: ME: We could assume(t) here, should we? + Q(true) + } else { + assertRaw(t, timeout)(Q) + } + } + + def assertRaw(t: Term, timeout: Option[Int] = Verifier.config.assertTimeout.toOption) + (Q: Boolean => VerificationResult) + : VerificationResult = { val success = deciderAssert(t, timeout) diff --git a/src/main/scala/rules/Consumer.scala b/src/main/scala/rules/Consumer.scala index d337f572c..10f607cca 100644 --- a/src/main/scala/rules/Consumer.scala +++ b/src/main/scala/rules/Consumer.scala @@ -480,7 +480,7 @@ object consumer extends ConsumptionRules { Quantification(q, vars, Implies(transformed, body), trgs, name, isGlob, weight) case _ => t } - v2.decider.assert(termToAssert) { + v2.decider.assertC(termToAssert, s2, v2) { case true => v2.decider.assume(t) QS(s3, v2) diff --git a/src/main/scala/rules/Evaluator.scala b/src/main/scala/rules/Evaluator.scala index 64aae33e2..7486b6824 100644 --- a/src/main/scala/rules/Evaluator.scala +++ b/src/main/scala/rules/Evaluator.scala @@ -213,7 +213,7 @@ object evaluator extends EvaluationRules { val s2 = s1.copy(functionRecorder = fr1) Q(s2, fvfLookup, v1) } else { - v1.decider.assert(IsPositive(totalPermissions.replace(`?r`, tRcvr))) { + v1.decider.assertWD(IsPositive(totalPermissions.replace(`?r`, tRcvr)), s1, v1) { case false => createFailure(pve dueTo InsufficientPermission(fa), v1, s1) case true => @@ -247,7 +247,7 @@ object evaluator extends EvaluationRules { val totalPermissions = PermLookup(fa.field.name, pmDef1.pm, tRcvr) IsPositive(totalPermissions) } - v1.decider.assert(permCheck) { + v1.decider.assertWD(permCheck, s1, v1) { case false => createFailure(pve dueTo InsufficientPermission(fa), v1, s1) case true => @@ -719,6 +719,7 @@ object evaluator extends EvaluationRules { reasonOffendingNode.replace(formalsToActuals)), exampleTrafo) val s3 = s2.copy(g = Store(fargs.zip(tArgs)), recordVisited = true, + isKnownWelldefined= true, functionRecorder = s2.functionRecorder.changeDepthBy(+1), /* Temporarily disable the recorder: when recording (to later on * translate a particular function fun) and a function application @@ -756,6 +757,7 @@ object evaluator extends EvaluationRules { recordVisited = s2.recordVisited, functionRecorder = fr5, smDomainNeeded = s2.smDomainNeeded, + isKnownWelldefined = s2.isKnownWelldefined, hackIssue387DisablePermissionConsumption = s.hackIssue387DisablePermissionConsumption) QB(s5, tFApp, v3)}) /* TODO: The join-function is heap-independent, and it is not obvious how a @@ -771,7 +773,7 @@ object evaluator extends EvaluationRules { if (s.cycles(predicate) < Verifier.config.recursivePredicateUnfoldings()) { evals(s, eArgs, _ => pve, v)((s1, tArgs, v1) => eval(s1, ePerm, pve, v1)((s2, tPerm, v2) => - v2.decider.assert(IsNonNegative(tPerm)) { // TODO: Replace with permissionSupporter.assertNotNegative + v2.decider.assertWD(IsNonNegative(tPerm), s2, v2) { // TODO: Replace with permissionSupporter.assertNotNegative case true => joiner.join[Term, Term](s2, v2)((s3, v3, QB) => { val s4 = s3.incCycleCounter(predicate) @@ -801,11 +803,12 @@ object evaluator extends EvaluationRules { val body = predicate.body.get /* Only non-abstract predicates can be unfolded */ val s7 = s6.scalePermissionFactor(tPerm) val insg = s7.g + Store(predicate.formalArgs map (_.localVar) zip tArgs) - val s7a = s7.copy(g = insg) + val s7a = s7.copy(g = insg, isKnownWelldefined = true) produce(s7a, toSf(snap), body, pve, v4)((s8, v5) => { val s9 = s8.copy(g = s7.g, functionRecorder = s8.functionRecorder.changeDepthBy(-1), recordVisited = s3.recordVisited, + isKnownWelldefined = s7.isKnownWelldefined, permissionScalingFactor = s6.permissionScalingFactor) .decCycleCounter(predicate) val s10 = v5.stateConsolidator.consolidateIfRetrying(s9, v5) @@ -834,9 +837,9 @@ object evaluator extends EvaluationRules { if (s1.triggerExp) { Q(s1, SeqAt(t0, t1), v1) } else { - v1.decider.assert(AtLeast(t1, IntLiteral(0))) { + v1.decider.assertWD(AtLeast(t1, IntLiteral(0)), s1, v1) { case true => - v1.decider.assert(Less(t1, SeqLength(t0))) { + v1.decider.assertWD(Less(t1, SeqLength(t0)), s1, v1) { case true => Q(s1, SeqAt(t0, t1), v1) case false => @@ -849,7 +852,7 @@ object evaluator extends EvaluationRules { val failure1 = createFailure(pve dueTo SeqIndexNegative(e0, e1), v1, s1) if (s1.retryLevel == 0) { v1.decider.assume(AtLeast(t1, IntLiteral(0))) - v1.decider.assert(Less(t1, SeqLength(t0))) { + v1.decider.assertWD(Less(t1, SeqLength(t0)), s1, v1) { case true => failure1 combine Q(s1, SeqAt(t0, t1), v1) case false => @@ -872,9 +875,9 @@ object evaluator extends EvaluationRules { if (s1.triggerExp) { Q(s1, SeqUpdate(t0, t1, t2), v1) } else { - v1.decider.assert(AtLeast(t1, IntLiteral(0))) { + v1.decider.assertWD(AtLeast(t1, IntLiteral(0)), s1, v1) { case true => - v1.decider.assert(Less(t1, SeqLength(t0))) { + v1.decider.assertWD(Less(t1, SeqLength(t0)), s1, v1) { case true => Q(s1, SeqUpdate(t0, t1, t2), v1) case false => @@ -887,7 +890,7 @@ object evaluator extends EvaluationRules { val failure1 = createFailure(pve dueTo SeqIndexNegative(e0, e1), v1, s1) if (s1.retryLevel == 0) { v1.decider.assume(AtLeast(t1, IntLiteral(0))) - v1.decider.assert(Less(t1, SeqLength(t0))) { + v1.decider.assertWD(Less(t1, SeqLength(t0)), s1, v1) { case true => failure1 combine Q(s1, SeqUpdate(t0, t1, t2), v1) case false => @@ -983,7 +986,7 @@ object evaluator extends EvaluationRules { case ast.MapLookup(base, key) => evals2(s, Seq(base, key), Nil, _ => pve, v)({ case (s1, Seq(baseT, keyT), v1) if s1.triggerExp => Q(s1, MapLookup(baseT, keyT), v1) - case (s1, Seq(baseT, keyT), v1) => v1.decider.assert(SetIn(keyT, MapDomain(baseT))) { + case (s1, Seq(baseT, keyT), v1) => v1.decider.assertWD(SetIn(keyT, MapDomain(baseT)), s1, v1) { case true => Q(s1, MapLookup(baseT, keyT), v1) case false => v1.decider.assume(SetIn(keyT, MapDomain(baseT))) @@ -1159,7 +1162,7 @@ object evaluator extends EvaluationRules { (Q: (State, Term, Verifier) => VerificationResult) : VerificationResult = { - v.decider.assert(tDivisor !== tZero){ + v.decider.assertWD(tDivisor !== tZero, s, v){ case true => Q(s, t, v) case false => val failure = createFailure(pve dueTo DivisionByZero(eDivisor), v, s) diff --git a/src/main/scala/rules/Executor.scala b/src/main/scala/rules/Executor.scala index 407611f44..836d02b1f 100644 --- a/src/main/scala/rules/Executor.scala +++ b/src/main/scala/rules/Executor.scala @@ -483,7 +483,7 @@ object executor extends ExecutionRules { val preCondLog = new CommentRecord("Precondition", s1, v1.decider.pcs) val preCondId = v1.symbExLog.openScope(preCondLog) val s2 = s1.copy(g = Store(fargs.zip(tArgs)), - recordVisited = true) + recordVisited = true, isKnownWelldefined = true) consumes(s2, meth.pres, _ => pvePre, v1)((s3, _, v2) => { v2.symbExLog.closeScope(preCondId) val postCondLog = new CommentRecord("Postcondition", s3, v2.decider.pcs) @@ -498,7 +498,8 @@ object executor extends ExecutionRules { .map(p => (p._1, s5.g(p._2))).toMap) val s6 = s5.copy(g = s1.g + gLhs, oldHeaps = s1.oldHeaps, - recordVisited = s1.recordVisited) + recordVisited = s1.recordVisited, + isKnownWelldefined = s1.isKnownWelldefined) v3.symbExLog.closeScope(sepIdentifier) Q(s6, v3)})})}) diff --git a/src/main/scala/rules/HavocSupporter.scala b/src/main/scala/rules/HavocSupporter.scala index 63520ae22..527a49e75 100644 --- a/src/main/scala/rules/HavocSupporter.scala +++ b/src/main/scala/rules/HavocSupporter.scala @@ -125,7 +125,7 @@ object havocSupporter extends SymbolicExecutionRules { v.decider.prover.comment("Check havocall receiver injectivity") val notInjectiveReason = QuasihavocallNotInjective(havocall) - v.decider.assert(receiverInjectivityCheck) { + v.decider.assertWD(receiverInjectivityCheck, s1, v) { case false => createFailure(pve dueTo notInjectiveReason, v, s1) case true => // Generate the inverse axioms diff --git a/src/main/scala/rules/MoreCompleteExhaleSupporter.scala b/src/main/scala/rules/MoreCompleteExhaleSupporter.scala index 9cdf7528a..43d368f24 100644 --- a/src/main/scala/rules/MoreCompleteExhaleSupporter.scala +++ b/src/main/scala/rules/MoreCompleteExhaleSupporter.scala @@ -151,7 +151,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { } } else { summarise(s, relevantChunks, resource, args, v)((s1, snap, _, permSum, v1) => - v.decider.assert(IsPositive(permSum)) { + v.decider.assertWD(IsPositive(permSum), s1, v) { case true => Q(s1, snap, v1) case false => @@ -189,7 +189,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { val relevantChunks = findChunksWithID[NonQuantifiedChunk](h.values, id).toSeq summarise(s, relevantChunks, resource, args, v)((s1, snap, _, permSum, v1) => - v.decider.assert(IsPositive(permSum)) { + v.decider.assertWD(IsPositive(permSum), s1, v) { case true => Q(s1, h, Some(snap), v1) case false => @@ -217,7 +217,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { if (relevantChunks.isEmpty) { // if no permission is exhaled, return none - v.decider.assert(perms === NoPerm()){ + v.decider.assertC(perms === NoPerm(), s, v){ case true => Q(s, h, None, v) case false => createFailure(ve, v, s) } @@ -289,7 +289,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { if (!moreNeeded) { Q(s1, newHeap, Some(condSnap), v1) } else { - v1.decider.assert(pNeeded === NoPerm()) { + v1.decider.assertC(pNeeded === NoPerm(), s1, v1) { case true => Q(s1, newHeap, Some(condSnap), v1) case false => @@ -342,7 +342,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { val s1 = s.copy(functionRecorder = newFr) - v.decider.assert(totalPermTaken !== NoPerm()) { + v.decider.assertC(totalPermTaken !== NoPerm(), s1, v) { case true => v.decider.assume(perms === totalPermTaken) summarise(s1, relevantChunks.toSeq, resource, args, v)((s2, snap, _, _, v1) => diff --git a/src/main/scala/rules/PermissionSupporter.scala b/src/main/scala/rules/PermissionSupporter.scala index 63cd54194..626916c9e 100644 --- a/src/main/scala/rules/PermissionSupporter.scala +++ b/src/main/scala/rules/PermissionSupporter.scala @@ -23,7 +23,7 @@ object permissionSupporter extends SymbolicExecutionRules { case k: Var if s.constrainableARPs.contains(k) => Q(s, v) case _ => - v.decider.assert(perms.IsNonNegative(tPerm)) { + v.decider.assertWD(perms.IsNonNegative(tPerm), s, v) { case true => Q(s, v) case false => createFailure(pve dueTo NegativePermission(ePerm), v, s) } diff --git a/src/main/scala/rules/PredicateSupporter.scala b/src/main/scala/rules/PredicateSupporter.scala index da0661fe8..6fae0a929 100644 --- a/src/main/scala/rules/PredicateSupporter.scala +++ b/src/main/scala/rules/PredicateSupporter.scala @@ -57,7 +57,7 @@ object predicateSupporter extends PredicateSupportRules { val body = predicate.body.get /* Only non-abstract predicates can be unfolded */ val gIns = s.g + Store(predicate.formalArgs map (_.localVar) zip tArgs) val s1 = s.copy(g = gIns, - smDomainNeeded = true) + smDomainNeeded = true, isKnownWelldefined = true) .scalePermissionFactor(tPerm) consume(s1, body, pve, v)((s1a, snap, v1) => { if (!Verifier.config.disableFunctionUnfoldTrigger()) { @@ -65,7 +65,7 @@ object predicateSupporter extends PredicateSupportRules { snap.convert(terms.sorts.Snap) +: tArgs) v1.decider.assume(predTrigger) } - val s2 = s1a.setConstrainable(constrainableWildcards, false) + val s2 = s1a.copy(isKnownWelldefined = s.isKnownWelldefined).setConstrainable(constrainableWildcards, false) if (s2.qpPredicates.contains(predicate)) { val predSnap = snap.convert(s2.predicateSnapMap(predicate)) val formalArgs = s2.predicateFormalVarMap(predicate) @@ -134,7 +134,7 @@ object predicateSupporter extends PredicateSupportRules { pve, v )((s2, h2, snap, v1) => { - val s3 = s2.copy(g = gIns, h = h2) + val s3 = s2.copy(g = gIns, h = h2, isKnownWelldefined = true) .setConstrainable(constrainableWildcards, false) produce(s3, toSf(snap), body, pve, v1)((s4, v2) => { v2.decider.prover.saturate(Verifier.config.proverSaturationTimeouts.afterUnfold) @@ -145,14 +145,15 @@ object predicateSupporter extends PredicateSupportRules { v2.decider.assume(predicateTrigger) } Q(s4.copy(g = s.g, - permissionScalingFactor = s.permissionScalingFactor), + permissionScalingFactor = s.permissionScalingFactor, + isKnownWelldefined = s.isKnownWelldefined), v2)}) }) } else { val ve = pve dueTo InsufficientPermission(pa) val description = s"consume ${pa.pos}: $pa" chunkSupporter.consume(s1, s1.h, predicate, tArgs, s1.permissionScalingFactor, ve, v, description)((s2, h1, snap, v1) => { - val s3 = s2.copy(g = gIns, h = h1) + val s3 = s2.copy(g = gIns, h = h1, isKnownWelldefined = true) .setConstrainable(constrainableWildcards, false) produce(s3, toSf(snap), body, pve, v1)((s4, v2) => { v2.decider.prover.saturate(Verifier.config.proverSaturationTimeouts.afterUnfold) @@ -162,7 +163,8 @@ object predicateSupporter extends PredicateSupportRules { v2.decider.assume(predicateTrigger) } val s5 = s4.copy(g = s.g, - permissionScalingFactor = s.permissionScalingFactor) + permissionScalingFactor = s.permissionScalingFactor, + isKnownWelldefined = s.isKnownWelldefined) Q(s5, v2)})}) } } diff --git a/src/main/scala/rules/QuantifiedChunkSupport.scala b/src/main/scala/rules/QuantifiedChunkSupport.scala index 5d94239dd..bd166a11c 100644 --- a/src/main/scala/rules/QuantifiedChunkSupport.scala +++ b/src/main/scala/rules/QuantifiedChunkSupport.scala @@ -861,7 +861,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { val nonNegImplication = Implies(tCond, perms.IsNonNegative(tPerm)) val nonNegTerm = Forall(qvars, Implies(FunctionPreconditionTransformer.transform(nonNegImplication, s.program), nonNegImplication), Nil) // TODO: Replace by QP-analogue of permissionSupporter.assertNotNegative - v.decider.assert(nonNegTerm) { + v.decider.assertWD(nonNegTerm, s, v) { case true => /* TODO: Can we omit/simplify the injectivity check in certain situations? */ @@ -881,7 +881,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { } v.decider.prover.comment("Check receiver injectivity") v.decider.assume(FunctionPreconditionTransformer.transform(receiverInjectivityCheck, s.program)) - v.decider.assert(receiverInjectivityCheck) { + v.decider.assertWD(receiverInjectivityCheck, s, v) { case true => val ax = inverseFunctions.axiomInversesOfInvertibles val inv = inverseFunctions.copy(axiomInversesOfInvertibles = Forall(ax.vars, ax.body, effectiveTriggers)) @@ -1066,7 +1066,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { val nonNegImplication = Implies(tCond, perms.IsNonNegative(tPerm)) val nonNegTerm = Forall(qvars, Implies(FunctionPreconditionTransformer.transform(nonNegImplication, s.program), nonNegImplication), Nil) // TODO: Replace by QP-analogue of permissionSupporter.assertNotNegative - v.decider.assert(nonNegTerm) { + v.decider.assertWD(nonNegTerm, s, v) { case true => val hints = quantifiedChunkSupporter.extractHints(Some(tCond), tArgs) val chunkOrderHeuristics = @@ -1099,7 +1099,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { qidPrefix = qid, program = s.program) v.decider.prover.comment("Check receiver injectivity") - v.decider.assert(receiverInjectivityCheck) { + v.decider.assertWD(receiverInjectivityCheck, s, v) { case true => val qvarsToInvOfLoc = inverseFunctions.qvarsToInversesOf(formalQVars) val condOfInvOfLoc = tCond.replace(qvarsToInvOfLoc) diff --git a/src/main/scala/state/State.scala b/src/main/scala/state/State.scala index fc8c28fce..6f73c4346 100644 --- a/src/main/scala/state/State.scala +++ b/src/main/scala/state/State.scala @@ -68,7 +68,9 @@ final case class State(g: Store = Store(), retryLevel: Int = 0, /* ast.Field, ast.Predicate, or MagicWandIdentifier */ heapDependentTriggers: InsertionOrderedSet[Any] = InsertionOrderedSet.empty, - moreCompleteExhale: Boolean = false) + moreCompleteExhale: Boolean = false, + isKnownWelldefined: Boolean = false, + isKnownCorrect: Boolean = false) extends Mergeable[State] { def incCycleCounter(m: ast.Predicate) = @@ -149,7 +151,7 @@ object State { ssCache1, hackIssue387DisablePermissionConsumption1, qpFields1, qpPredicates1, qpMagicWands1, smCache1, pmCache1, smDomainNeeded1, predicateSnapMap1, predicateFormalVarMap1, hack, retryLevel, useHeapTriggers, - moreCompleteExhale) => + moreCompleteExhale, isKnownWelldefined, isKnownCorrect) => /* Decompose state s2: most values must match those of s1 */ s2 match { @@ -174,7 +176,7 @@ object State { ssCache2, `hackIssue387DisablePermissionConsumption1`, `qpFields1`, `qpPredicates1`, `qpMagicWands1`, smCache2, pmCache2, `smDomainNeeded1`, `predicateSnapMap1`, `predicateFormalVarMap1`, `hack`, `retryLevel`, `useHeapTriggers`, - moreCompleteExhale2) => + moreCompleteExhale2, isKnownWelldefined2, isKnownCorrect2) => val functionRecorder3 = functionRecorder1.merge(functionRecorder2) val triggerExp3 = triggerExp1 && triggerExp2 @@ -186,6 +188,8 @@ object State { val ssCache3 = ssCache1 ++ ssCache2 val moreCompleteExhale3 = moreCompleteExhale || moreCompleteExhale2 + val isKnownWelldefined3 = isKnownWelldefined && isKnownWelldefined2 + val isKnownCorrect3 = isKnownCorrect && isKnownCorrect2 s1.copy(functionRecorder = functionRecorder3, possibleTriggers = possibleTriggers3, @@ -194,7 +198,9 @@ object State { ssCache = ssCache3, smCache = smCache3, pmCache = pmCache3, - moreCompleteExhale = moreCompleteExhale3) + moreCompleteExhale = moreCompleteExhale3, + isKnownWelldefined = isKnownWelldefined3, + isKnownCorrect = isKnownCorrect3) case _ => val err = new StringBuilder()