From 122881f506d155892bdc37e41a3e14a8d8fa4498 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Tue, 5 Sep 2023 20:47:36 +0200 Subject: [PATCH] K-induction without heaps might work --- src/main/scala/Config.scala | 6 ++ src/main/scala/decider/Decider.scala | 9 +- src/main/scala/rules/Consumer.scala | 4 +- src/main/scala/rules/Evaluator.scala | 23 ++--- src/main/scala/rules/Executor.scala | 83 +++++++++++++++++++ src/main/scala/rules/HavocSupporter.scala | 5 +- .../scala/rules/PermissionSupporter.scala | 2 +- src/main/scala/rules/PredicateSupporter.scala | 1 + src/main/scala/rules/Producer.scala | 2 + .../scala/rules/QuantifiedChunkSupport.scala | 8 +- src/main/scala/rules/StateConsolidator.scala | 2 + .../rules/{ => chunks}/ChunkSupporter.scala | 21 ++--- .../MoreCompleteExhaleSupporter.scala | 21 +++-- src/main/scala/state/State.scala | 16 +++- src/main/scala/state/package.scala | 2 +- 15 files changed, 159 insertions(+), 46 deletions(-) rename src/main/scala/rules/{ => chunks}/ChunkSupporter.scala (97%) rename src/main/scala/rules/{ => chunks}/MoreCompleteExhaleSupporter.scala (97%) diff --git a/src/main/scala/Config.scala b/src/main/scala/Config.scala index 068bcc03e..f197e2bd7 100644 --- a/src/main/scala/Config.scala +++ b/src/main/scala/Config.scala @@ -647,6 +647,12 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") { case _ => opt } + val kinduction: ScallopOption[Int] = opt[Int]("enableKInduction", + descr = "Enable k-induction with the given k (default: 0, i.e., disabled).", + default = None, + noshort = true + ) + // DEPRECATED and replaced by exhaleMode. val moreCompleteExhale: ScallopOption[Boolean] = opt[Boolean]("enableMoreCompleteExhale", descr = "Warning: This option is deprecated. " diff --git a/src/main/scala/decider/Decider.scala b/src/main/scala/decider/Decider.scala index 145fcceb0..b9d26cd73 100644 --- a/src/main/scala/decider/Decider.scala +++ b/src/main/scala/decider/Decider.scala @@ -49,7 +49,7 @@ 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 assert(t: Term, s: State, 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 @@ -238,14 +238,19 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier => def checkSmoke(isAssert: Boolean = false): Boolean = { val timeout = if (isAssert) Verifier.config.assertTimeout.toOption else Verifier.config.checkTimeout.toOption + prover.check(timeout) == Unsat } def check(t: Term, timeout: Int): Boolean = deciderAssert(t, Some(timeout)) - def assert(t: Term, timeout: Option[Int] = Verifier.config.assertTimeout.toOption) + def assert(t: Term, s: State, timeout: Option[Int] = Verifier.config.assertTimeout.toOption) (Q: Boolean => VerificationResult) : VerificationResult = { + if (s.loopPhaseStack.nonEmpty && s.loopPhaseStack.head._1 == LoopPhases.Assuming) { + assume(t) + return Q(true) + } val success = deciderAssert(t, timeout) diff --git a/src/main/scala/rules/Consumer.scala b/src/main/scala/rules/Consumer.scala index ac1a95edc..b96525b99 100644 --- a/src/main/scala/rules/Consumer.scala +++ b/src/main/scala/rules/Consumer.scala @@ -6,6 +6,8 @@ package viper.silicon.rules +import viper.silicon.rules.chunks.chunkSupporter + import scala.collection.mutable import viper.silver.ast import viper.silver.ast.utility.QuantifiedPermissions.QuantifiedPermissionAssertion @@ -480,7 +482,7 @@ object consumer extends ConsumptionRules { Quantification(q, vars, Implies(transformed, body), trgs, name, isGlob, weight) case _ => t } - v2.decider.assert(termToAssert) { + v2.decider.assert(termToAssert, s3) { 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 610cc514e..97c95290a 100644 --- a/src/main/scala/rules/Evaluator.scala +++ b/src/main/scala/rules/Evaluator.scala @@ -6,6 +6,7 @@ package viper.silicon.rules +import viper.silicon.rules.chunks.chunkSupporter import viper.silver.ast import viper.silver.verifier.{CounterexampleTransformer, PartialVerificationError, VerifierWarning} import viper.silver.verifier.errors.{ErrorWrapperWithExampleTransformer, PreconditionInAppFalse} @@ -213,7 +214,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.assert(IsPositive(totalPermissions.replace(`?r`, tRcvr)), s1) { case false => createFailure(pve dueTo InsufficientPermission(fa), v1, s1) case true => @@ -247,7 +248,7 @@ object evaluator extends EvaluationRules { val totalPermissions = PermLookup(fa.field.name, pmDef1.pm, tRcvr) IsPositive(totalPermissions) } - v1.decider.assert(permCheck) { + v1.decider.assert(permCheck, s1) { case false => createFailure(pve dueTo InsufficientPermission(fa), v1, s1) case true => @@ -791,7 +792,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.assert(IsNonNegative(tPerm), s2) { // TODO: Replace with permissionSupporter.assertNotNegative case true => joiner.join[Term, Term](s2, v2)((s3, v3, QB) => { val s4 = s3.incCycleCounter(predicate) @@ -854,9 +855,9 @@ object evaluator extends EvaluationRules { if (s1.triggerExp) { Q(s1, SeqAt(t0, t1), v1) } else { - v1.decider.assert(AtLeast(t1, IntLiteral(0))) { + v1.decider.assert(AtLeast(t1, IntLiteral(0)), s1) { case true => - v1.decider.assert(Less(t1, SeqLength(t0))) { + v1.decider.assert(Less(t1, SeqLength(t0)), s1) { case true => Q(s1, SeqAt(t0, t1), v1) case false => @@ -869,7 +870,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.assert(Less(t1, SeqLength(t0)), s1) { case true => failure1 combine Q(s1, SeqAt(t0, t1), v1) case false => @@ -892,9 +893,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.assert(AtLeast(t1, IntLiteral(0)), s1) { case true => - v1.decider.assert(Less(t1, SeqLength(t0))) { + v1.decider.assert(Less(t1, SeqLength(t0)), s1) { case true => Q(s1, SeqUpdate(t0, t1, t2), v1) case false => @@ -907,7 +908,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.assert(Less(t1, SeqLength(t0)), s1) { case true => failure1 combine Q(s1, SeqUpdate(t0, t1, t2), v1) case false => @@ -1003,7 +1004,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.assert(SetIn(keyT, MapDomain(baseT)), s1) { case true => Q(s1, MapLookup(baseT, keyT), v1) case false => v1.decider.assume(SetIn(keyT, MapDomain(baseT))) @@ -1214,7 +1215,7 @@ object evaluator extends EvaluationRules { (Q: (State, Term, Verifier) => VerificationResult) : VerificationResult = { - v.decider.assert(tDivisor !== tZero){ + v.decider.assert(tDivisor !== tZero, s){ 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 d15793a22..b5ea4ad49 100644 --- a/src/main/scala/rules/Executor.scala +++ b/src/main/scala/rules/Executor.scala @@ -6,6 +6,8 @@ package viper.silicon.rules +import viper.silicon.rules.chunks.chunkSupporter + import scala.annotation.unused import viper.silver.cfg.silver.SilverCfg import viper.silver.cfg.silver.SilverCfg.{SilverBlock, SilverEdge} @@ -77,6 +79,29 @@ object executor extends ExecutionRules { def handleOutEdge(s: State, edge: SilverEdge, v: Verifier): State = { edge.kind match { + case cfg.Kind.Out if Verifier.config.kinduction.isSupplied => + val (phase, kRemaining, loopHeap) = s.loopPhaseStack.head + val sPop = s.copy(loopPhaseStack = s.loopPhaseStack.tail) + val sNew = phase match { + case LoopPhases.Transferring => + // just merge back + val (fr1, h1) = v.stateConsolidator.merge(s.functionRecorder, s.h, s.loopHeapStack.head, v) + val s1 = s.copy(functionRecorder = fr1, h = h1, + loopHeapStack = s.loopHeapStack.tail, loopReadVarStack = s.loopReadVarStack.tail) + s1 + case LoopPhases.Assuming => + v.decider.assume(False) + // assume false + val s1 = s.copy(loopHeapStack = s.loopHeapStack.tail, loopReadVarStack = s.loopReadVarStack.tail) + s1 + case LoopPhases.Checking => + // just merge back + val (fr1, h1) = v.stateConsolidator.merge(s.functionRecorder, s.h, s.loopHeapStack.head, v) + val s1 = s.copy(functionRecorder = fr1, h = h1, + loopHeapStack = s.loopHeapStack.tail, loopReadVarStack = s.loopReadVarStack.tail) + s1 + } + sNew case cfg.Kind.Out => val (fr1, h1) = v.stateConsolidator.merge(s.functionRecorder, s.h, s.invariantContexts.head, v) val s1 = s.copy(functionRecorder = fr1, h = h1, @@ -166,6 +191,19 @@ object executor extends ExecutionRules { case block @ cfg.LoopHeadBlock(invs, stmts, _) => incomingEdgeKind match { + case cfg.Kind.In if Verifier.config.kinduction.isSupplied => + val readPerm = v.decider.fresh(sorts.Perm) + v.decider.assume(PermLess(NoPerm, readPerm)) + val sFirstPhase = s.copy(loopPhaseStack = s.loopPhaseStack.prepended((LoopPhases.Transferring, Verifier.config.kinduction(), block)), + loopHeapStack = s.loopHeapStack.prepended(s.h), + h = Heap(), + loopReadVarStack = s.loopReadVarStack.prepended(readPerm)) + val edges = s.methodCfg.outEdges(block) + + execs(sFirstPhase, stmts, v)((s4, v3) => { + v3.decider.prover.comment("Loop head block: Follow loop-internal edges") + follows(s4, edges, WhileFailed, v3)(Q) + }) case cfg.Kind.In => /* We've reached a loop head block via an in-edge. Steps to perform: * - Check loop invariant for self-framingness @@ -223,10 +261,55 @@ object executor extends ExecutionRules { if (v2.decider.checkSmoke()) Success() else { + //if (stmts.nonEmpty) + // throw new Exception() execs(s3, stmts, v2)((s4, v3) => { v3.decider.prover.comment("Loop head block: Follow loop-internal edges") follows(s4, sortedEdges, WhileFailed, v3)(Q)})}})}})})) + case _ if Verifier.config.kinduction.isSupplied => + val (phase, kRemaining, loopHeap) = s.loopPhaseStack.head + val edges = s.methodCfg.outEdges(block) + consumes(s, invs, e => LoopInvariantNotPreserved(e), v)((_, _, v) => + phase match { + case LoopPhases.Transferring => + if (kRemaining > 1) { + val sNew = s.copy(loopPhaseStack = (LoopPhases.Transferring, kRemaining - 1, loopHeap) +: s.loopPhaseStack.tail) + execs(sNew, stmts, v)((s4, v3) => { + follows(s4, edges, WhileFailed, v3)(Q) + }) + } else { + /* Havoc local variables that are assigned to in the loop body */ + val wvs = s.methodCfg.writtenVars(block) + /* TODO: BUG: Variables declared by LetWand show up in this list, but shouldn't! */ + + val gBody = Store(wvs.foldLeft(s.g.values)((map, x) => map.updated(x, v.decider.fresh(x)))) + val sNew = s.copy(g = gBody, h = Heap(), + loopPhaseStack = (LoopPhases.Assuming, Verifier.config.kinduction(), loopHeap) +: s.loopPhaseStack.tail) + execs(sNew, stmts, v)((s4, v3) => { + follows(s4, edges, WhileFailed, v3)(Q) + }) + } + case LoopPhases.Assuming => + if (kRemaining > 1) { + val sNew = s.copy(loopPhaseStack = (LoopPhases.Assuming, kRemaining - 1, loopHeap) +: s.loopPhaseStack.tail) + execs(sNew, stmts, v)((s4, v3) => { + follows(s4, edges, WhileFailed, v3)(Q) + }) + } else { + val sNew = s.copy(loopPhaseStack = (LoopPhases.Checking, 1, loopHeap) +: s.loopPhaseStack.tail) + execs(sNew, stmts, v)((s4, v3) => { + follows(s4, edges, WhileFailed, v3)(Q) + }) + } + case LoopPhases.Checking => + val outEdges = edges filter(_.kind == cfg.Kind.Out) + execs(s, stmts, v)((s4, v3) => { + follows(s4, outEdges, WhileFailed, v3)(Q) + }) + } + ) + case _ => /* We've reached a loop head block via an edge other than an in-edge: a normal edge or * and out-edge. We consider this edge to be a back-edge and we break the cycle by diff --git a/src/main/scala/rules/HavocSupporter.scala b/src/main/scala/rules/HavocSupporter.scala index ec2ea7cfe..b73a4e224 100644 --- a/src/main/scala/rules/HavocSupporter.scala +++ b/src/main/scala/rules/HavocSupporter.scala @@ -6,6 +6,7 @@ package viper.silicon.rules +import viper.silicon.rules.chunks.chunkSupporter import viper.silicon.interfaces.VerificationResult import viper.silicon.interfaces.state.{Chunk, NonQuantifiedChunk} import viper.silicon.Map @@ -17,7 +18,7 @@ import viper.silicon.state.terms.predef.{`?r`, `?s`} import viper.silicon.utils.freshSnap import viper.silicon.verifier.Verifier import viper.silver.ast -import viper.silver.verifier.errors.{QuasihavocFailed, HavocallFailed} +import viper.silver.verifier.errors.{HavocallFailed, QuasihavocFailed} import viper.silver.verifier.reasons.QuasihavocallNotInjective object havocSupporter extends SymbolicExecutionRules { @@ -125,7 +126,7 @@ object havocSupporter extends SymbolicExecutionRules { v.decider.prover.comment("Check havocall receiver injectivity") val notInjectiveReason = QuasihavocallNotInjective(havocall) - v.decider.assert(receiverInjectivityCheck) { + v.decider.assert(receiverInjectivityCheck, s1) { case false => createFailure(pve dueTo notInjectiveReason, v, s1) case true => // Generate the inverse axioms diff --git a/src/main/scala/rules/PermissionSupporter.scala b/src/main/scala/rules/PermissionSupporter.scala index 63cd54194..a7f4d0ba5 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.assert(perms.IsNonNegative(tPerm), s) { 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..284d05c45 100644 --- a/src/main/scala/rules/PredicateSupporter.scala +++ b/src/main/scala/rules/PredicateSupporter.scala @@ -6,6 +6,7 @@ package viper.silicon.rules +import viper.silicon.rules.chunks.chunkSupporter import viper.silver.ast import viper.silver.verifier.PartialVerificationError import viper.silver.verifier.reasons.InsufficientPermission diff --git a/src/main/scala/rules/Producer.scala b/src/main/scala/rules/Producer.scala index a29672f59..43e5b7fb1 100644 --- a/src/main/scala/rules/Producer.scala +++ b/src/main/scala/rules/Producer.scala @@ -6,6 +6,8 @@ package viper.silicon.rules +import viper.silicon.rules.chunks.chunkSupporter + import scala.collection.mutable import viper.silver.ast import viper.silver.ast.utility.QuantifiedPermissions.QuantifiedPermissionAssertion diff --git a/src/main/scala/rules/QuantifiedChunkSupport.scala b/src/main/scala/rules/QuantifiedChunkSupport.scala index c1a03b2d4..8093d511e 100644 --- a/src/main/scala/rules/QuantifiedChunkSupport.scala +++ b/src/main/scala/rules/QuantifiedChunkSupport.scala @@ -862,7 +862,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.assert(nonNegTerm, s) { case true => /* TODO: Can we omit/simplify the injectivity check in certain situations? */ @@ -882,7 +882,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.assert(receiverInjectivityCheck, s) { case true => val ax = inverseFunctions.axiomInversesOfInvertibles val inv = inverseFunctions.copy(axiomInversesOfInvertibles = Forall(ax.vars, ax.body, effectiveTriggers)) @@ -1067,7 +1067,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.assert(nonNegTerm, s) { case true => val hints = quantifiedChunkSupporter.extractHints(Some(tCond), tArgs) val chunkOrderHeuristics = @@ -1100,7 +1100,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { qidPrefix = qid, program = s.program) v.decider.prover.comment("Check receiver injectivity") - v.decider.assert(receiverInjectivityCheck) { + v.decider.assert(receiverInjectivityCheck, s) { case true => val qvarsToInvOfLoc = inverseFunctions.qvarsToInversesOf(formalQVars) val condOfInvOfLoc = tCond.replace(qvarsToInvOfLoc) diff --git a/src/main/scala/rules/StateConsolidator.scala b/src/main/scala/rules/StateConsolidator.scala index ba207cefe..08c6f8bc9 100644 --- a/src/main/scala/rules/StateConsolidator.scala +++ b/src/main/scala/rules/StateConsolidator.scala @@ -6,6 +6,8 @@ package viper.silicon.rules +import viper.silicon.rules.chunks.{chunkSupporter, moreCompleteExhaleSupporter} + import scala.annotation.unused import viper.silicon.Config import viper.silicon.common.collections.immutable.InsertionOrderedSet diff --git a/src/main/scala/rules/ChunkSupporter.scala b/src/main/scala/rules/chunks/ChunkSupporter.scala similarity index 97% rename from src/main/scala/rules/ChunkSupporter.scala rename to src/main/scala/rules/chunks/ChunkSupporter.scala index fe88e765b..4c7542b27 100644 --- a/src/main/scala/rules/ChunkSupporter.scala +++ b/src/main/scala/rules/chunks/ChunkSupporter.scala @@ -4,18 +4,20 @@ // // Copyright (c) 2011-2019 ETH Zurich. -package viper.silicon.rules +package viper.silicon.rules.chunks -import scala.reflect.ClassTag -import viper.silver.ast -import viper.silver.verifier.VerificationError import viper.silicon.interfaces.state._ import viper.silicon.interfaces.{Success, VerificationResult} import viper.silicon.resources.{NonQuantifiedPropertyInterpreter, Resources} +import viper.silicon.rules._ import viper.silicon.state._ import viper.silicon.state.terms._ import viper.silicon.state.terms.perms.IsPositive import viper.silicon.verifier.Verifier +import viper.silver.ast +import viper.silver.verifier.VerificationError + +import scala.reflect.ClassTag trait ChunkSupportRules extends SymbolicExecutionRules { def consume(s: State, @@ -42,13 +44,6 @@ trait ChunkSupportRules extends SymbolicExecutionRules { (Q: (State, Heap, Term, Verifier) => VerificationResult) : VerificationResult - def findChunk[CH <: NonQuantifiedChunk: ClassTag] - (chunks: Iterable[Chunk], - id: ChunkIdentifer, - args: Iterable[Term], - v: Verifier) - : Option[CH] - def findMatchingChunk[CH <: NonQuantifiedChunk: ClassTag] (chunks: Iterable[Chunk], chunk: CH, @@ -221,6 +216,8 @@ object chunkSupporter extends ChunkSupportRules { v: Verifier) (Q: (State, Term, Verifier) => VerificationResult) : VerificationResult = { + if (s.loopPhaseStack.nonEmpty) + throw new Exception() val id = ChunkIdentifier(resource, s.program) @@ -234,7 +231,7 @@ object chunkSupporter extends ChunkSupportRules { } } - def findChunk[CH <: NonQuantifiedChunk: ClassTag] + private[chunks] def findChunk[CH <: NonQuantifiedChunk: ClassTag] (chunks: Iterable[Chunk], id: ChunkIdentifer, args: Iterable[Term], diff --git a/src/main/scala/rules/MoreCompleteExhaleSupporter.scala b/src/main/scala/rules/chunks/MoreCompleteExhaleSupporter.scala similarity index 97% rename from src/main/scala/rules/MoreCompleteExhaleSupporter.scala rename to src/main/scala/rules/chunks/MoreCompleteExhaleSupporter.scala index 6abf20ff3..9bb863833 100644 --- a/src/main/scala/rules/MoreCompleteExhaleSupporter.scala +++ b/src/main/scala/rules/chunks/MoreCompleteExhaleSupporter.scala @@ -4,22 +4,24 @@ // // Copyright (c) 2011-2019 ETH Zurich. -package viper.silicon.rules +package viper.silicon.rules.chunks -import scala.collection.mutable.ListBuffer -import viper.silicon.{MList, MMap} +import viper.silicon.rules.chunks.chunkSupporter.findChunksWithID import viper.silicon.interfaces.state._ import viper.silicon.interfaces.{Success, VerificationResult} import viper.silicon.resources.{FieldID, NonQuantifiedPropertyInterpreter, Resources} -import viper.silicon.rules.chunkSupporter.findChunksWithID +import viper.silicon.rules.{SnapshotMapDefinition, SymbolicExecutionRules} import viper.silicon.state._ import viper.silicon.state.terms._ import viper.silicon.state.terms.perms.{IsNonPositive, IsPositive} import viper.silicon.supporters.functions.NoopFunctionRecorder import viper.silicon.verifier.Verifier +import viper.silicon.{MList, MMap} import viper.silver.ast import viper.silver.verifier.VerificationError +import scala.collection.mutable.ListBuffer + object moreCompleteExhaleSupporter extends SymbolicExecutionRules { sealed trait TaggedSummarisingSnapshot { def snapshot: Term @@ -140,6 +142,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { (Q: (State, Term, Verifier) => VerificationResult) : VerificationResult = { + val id = ChunkIdentifier(resource, s.program) val relevantChunks = findChunksWithID[NonQuantifiedChunk](h.values, id).toSeq @@ -151,7 +154,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { } } else { summarise(s, relevantChunks, resource, args, v)((s1, snap, _, permSum, v1) => - v.decider.assert(IsPositive(permSum)) { + v.decider.assert(IsPositive(permSum), s1) { case true => Q(s1, snap, v1) case false => @@ -189,7 +192,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.assert(IsPositive(permSum), s1) { case true => Q(s1, h, Some(snap), v1) case false => @@ -217,7 +220,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { if (relevantChunks.isEmpty) { // if no permission is exhaled, return none - v.decider.assert(perms === NoPerm) { + v.decider.assert(perms === NoPerm, s) { case true => Q(s, h, None, v) case false => createFailure(ve, v, s) } @@ -300,7 +303,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { if (!moreNeeded) { Q(s1, newHeap, Some(condSnap), v1) } else { - v1.decider.assert(pNeeded === NoPerm) { + v1.decider.assert(pNeeded === NoPerm, s1) { case true => Q(s1, newHeap, Some(condSnap), v1) case false => @@ -353,7 +356,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { val s1 = s.copy(functionRecorder = newFr) - v.decider.assert(totalPermTaken !== NoPerm) { + v.decider.assert(totalPermTaken !== NoPerm, s1) { case true => v.decider.assume(perms === totalPermTaken) summarise(s1, relevantChunks.toSeq, resource, args, v)((s2, snap, _, _, v1) => diff --git a/src/main/scala/state/State.scala b/src/main/scala/state/State.scala index b56238772..c72516f69 100644 --- a/src/main/scala/state/State.scala +++ b/src/main/scala/state/State.scala @@ -11,11 +11,18 @@ import viper.silver.cfg.silver.SilverCfg import viper.silicon.common.Mergeable import viper.silicon.common.collections.immutable.InsertionOrderedSet import viper.silicon.decider.RecordedPathConditions +import viper.silicon.state.LoopPhases.LoopPhase import viper.silicon.state.State.OldHeaps import viper.silicon.state.terms.{Term, Var} import viper.silicon.supporters.PredicateData import viper.silicon.supporters.functions.{FunctionData, FunctionRecorder, NoopFunctionRecorder} import viper.silicon.{Map, Stack} +import viper.silver.cfg.silver.SilverCfg.SilverLoopHeadBlock + +object LoopPhases extends Enumeration { + type LoopPhase = Value + val Transferring, Assuming, Checking = Value +} final case class State(g: Store = Store(), h: Heap = Heap(), @@ -68,7 +75,10 @@ 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, + loopPhaseStack: Stack[(LoopPhase, Int, SilverLoopHeadBlock)] = Stack(), + loopHeapStack: Stack[Heap] = Stack(), + loopReadVarStack: Stack[Var] = Stack()) extends Mergeable[State] { val isMethodVerification: Boolean = { @@ -156,7 +166,7 @@ object State { ssCache1, hackIssue387DisablePermissionConsumption1, qpFields1, qpPredicates1, qpMagicWands1, smCache1, pmCache1, smDomainNeeded1, predicateSnapMap1, predicateFormalVarMap1, retryLevel, useHeapTriggers, - moreCompleteExhale) => + moreCompleteExhale, loopPhase, loopHeaps, loopReadVars) => /* Decompose state s2: most values must match those of s1 */ s2 match { @@ -181,7 +191,7 @@ object State { ssCache2, `hackIssue387DisablePermissionConsumption1`, `qpFields1`, `qpPredicates1`, `qpMagicWands1`, smCache2, pmCache2, `smDomainNeeded1`, `predicateSnapMap1`, `predicateFormalVarMap1`, `retryLevel`, `useHeapTriggers`, - moreCompleteExhale2) => + moreCompleteExhale2, `loopPhase`, loopHeaps2, loopReadVars2) => val functionRecorder3 = functionRecorder1.merge(functionRecorder2) val triggerExp3 = triggerExp1 && triggerExp2 diff --git a/src/main/scala/state/package.scala b/src/main/scala/state/package.scala index a6381ac76..354463694 100644 --- a/src/main/scala/state/package.scala +++ b/src/main/scala/state/package.scala @@ -9,7 +9,7 @@ package viper.silicon import viper.silicon.interfaces.state.NonQuantifiedChunk import viper.silver.ast import viper.silicon.rules.PermMapDefinition -import viper.silicon.rules.moreCompleteExhaleSupporter.TaggedSummarisingSnapshot +import viper.silicon.rules.chunks.moreCompleteExhaleSupporter.TaggedSummarisingSnapshot import viper.silicon.state.terms.Term package object state {