From f8cc4843efa275189fa84dc8c735a80adb7421a3 Mon Sep 17 00:00:00 2001 From: manud99 <19774382+manud99@users.noreply.github.com> Date: Wed, 12 Jun 2024 15:26:11 +0200 Subject: [PATCH] Use a Map from Snap to Snap to represent a magic wand snapshot. (#836) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * Use a Map from Snap to Snap to represent a magic wand snapshot. * Fix failing test cases. * Fix broken links in comments. * First optimization: Create sort MagicWandSnapFunction (MWSF) with its own function definitions to replace wand maps. * Second optimization: When there is no applying expression use the original approach using MagicWandSnapSingleton. * Revert "Second optimization: When there is no applying expression use the original approach using MagicWandSnapSingleton." This reverts commit fd87482c7f9af2d31f32add3ba77c221917640b7. * Apply suggested changes from code review. * Fix test cases with quasihavoc statements. * Update submodule to use branch with both testcase changes * Remove abstractLhs and rhsSnapshot from MagicWandSnapshot. * Reduce diff * Simplify havoc * Simplify production of a MWSF. * Rename variable in Producer. * Update silver branch magic-wand-fixes. --------- Co-authored-by: Jonáš Fiala --- silver | 2 +- ...agic_wand_snap_functions_declarations.smt2 | 1 + src/main/scala/Utils.scala | 1 + .../decider/TermToSMTLib2Converter.scala | 7 +- .../scala/decider/TermToZ3APIConverter.scala | 2 + src/main/scala/rules/HavocSupporter.scala | 15 +- src/main/scala/rules/MagicWandSupporter.scala | 333 +++++++++++------- .../rules/MoreCompleteExhaleSupporter.scala | 2 +- src/main/scala/rules/Producer.scala | 2 +- .../scala/rules/QuantifiedChunkSupport.scala | 1 - src/main/scala/state/Chunks.scala | 7 +- src/main/scala/state/Terms.scala | 108 +++--- src/main/scala/state/Utils.scala | 5 +- .../BuiltinDomainsContributor.scala | 95 +++-- .../MagicWandSnapFunctionsContributor.scala | 92 +++++ ...icateAndWandSnapFunctionsContributor.scala | 4 +- .../scala/verifier/DefaultMainVerifier.scala | 7 + 17 files changed, 442 insertions(+), 242 deletions(-) create mode 100644 src/main/resources/magic_wand_snap_functions_declarations.smt2 create mode 100644 src/main/scala/supporters/MagicWandSnapFunctionsContributor.scala diff --git a/silver b/silver index e51a7aad2..d29ac2738 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit e51a7aad25c1e8278913b777e7cd4d619a801bd6 +Subproject commit d29ac2738d27232edaeb3d3a24952928f4006299 diff --git a/src/main/resources/magic_wand_snap_functions_declarations.smt2 b/src/main/resources/magic_wand_snap_functions_declarations.smt2 new file mode 100644 index 000000000..988585407 --- /dev/null +++ b/src/main/resources/magic_wand_snap_functions_declarations.smt2 @@ -0,0 +1 @@ +(declare-fun MWSF_apply ($MWSF $Snap) $Snap) diff --git a/src/main/scala/Utils.scala b/src/main/scala/Utils.scala index 56a773538..f7f817f2d 100644 --- a/src/main/scala/Utils.scala +++ b/src/main/scala/Utils.scala @@ -222,6 +222,7 @@ package object utils { case class ViperEmbedding(embeddedSort: Sort) extends silver.ast.ExtensionType { def substitute(typVarsMap: Predef.Map[silver.ast.TypeVar, silver.ast.Type]): silver.ast.Type = this def isConcrete: Boolean = true + override def toString: String = s"ViperEmbedding(sorts.$embeddedSort)" } } diff --git a/src/main/scala/decider/TermToSMTLib2Converter.scala b/src/main/scala/decider/TermToSMTLib2Converter.scala index b8f6c0f89..d876d1db7 100644 --- a/src/main/scala/decider/TermToSMTLib2Converter.scala +++ b/src/main/scala/decider/TermToSMTLib2Converter.scala @@ -61,6 +61,8 @@ class TermToSMTLib2Converter case sorts.FieldPermFunction() => text("$FPM") case sorts.PredicatePermFunction() => text("$PPM") + + case sorts.MagicWandSnapFunction => text("$MWSF") } def convert(d: Decl): String = { @@ -263,7 +265,7 @@ class TermToSMTLib2Converter case Lookup(field, fvf, at) => //fvf.sort match { // case _: sorts.PartialFieldValueFunction => - parens(text("$FVF.lookup_") <> field <+> render(fvf) <+> render(at)) + parens(text("$FVF.lookup_") <> field <+> render(fvf) <+> render(at)) // case _: sorts.TotalFieldValueFunction => // render(Apply(fvf, Seq(at))) // parens("$FVF.lookup_" <> field <+> render(fvf) <+> render(at)) @@ -313,6 +315,9 @@ class TermToSMTLib2Converter val docBindings = ssep((bindings.toSeq map (p => parens(render(p._1) <+> render(p._2)))).to(collection.immutable.Seq), space) parens(text("let") <+> parens(docBindings) <+> render(body)) + case MagicWandSnapshot(mwsf) => render(mwsf) + case MWSFLookup(mwsf, snap) => renderApp("MWSF_apply", Seq(mwsf, snap), sorts.Snap) + case _: MagicWandChunkTerm | _: Quantification => sys.error(s"Unexpected term $term cannot be translated to SMTLib code") diff --git a/src/main/scala/decider/TermToZ3APIConverter.scala b/src/main/scala/decider/TermToZ3APIConverter.scala index 3766ee49f..152bf1d64 100644 --- a/src/main/scala/decider/TermToZ3APIConverter.scala +++ b/src/main/scala/decider/TermToZ3APIConverter.scala @@ -445,6 +445,8 @@ class TermToZ3APIConverter case Let(bindings, body) => convert(body.replace(bindings)) + case MWSFLookup(mwsf, snap) => createApp("MWSF_apply", Seq(mwsf, snap), sorts.Snap) + case _: MagicWandChunkTerm | _: Quantification => sys.error(s"Unexpected term $term cannot be translated to SMTLib code") diff --git a/src/main/scala/rules/HavocSupporter.scala b/src/main/scala/rules/HavocSupporter.scala index e23472e23..d146c72ee 100644 --- a/src/main/scala/rules/HavocSupporter.scala +++ b/src/main/scala/rules/HavocSupporter.scala @@ -181,10 +181,17 @@ object havocSupporter extends SymbolicExecutionRules { val id = ChunkIdentifier(resource, s.program) val (relevantChunks, otherChunks) = chunkSupporter.splitHeap[NonQuantifiedChunk](s.h, id) - val newChunks = relevantChunks.map { ch => - val havockedSnap = freshSnap(ch.snap.sort, v) - val cond = replacementCond(lhs, ch.args, condInfo) - ch.withSnap(Ite(cond, havockedSnap, ch.snap)) + val newChunks = relevantChunks.map { + case ch: MagicWandChunk => + val havockedSnap = v.decider.fresh("mwsf", sorts.MagicWandSnapFunction) + val cond = replacementCond(lhs, ch.args, condInfo) + val magicWandSnapshot = MagicWandSnapshot(Ite(cond, havockedSnap, ch.snap.mwsf)) + ch.withSnap(magicWandSnapshot) + + case ch => + val havockedSnap = freshSnap(ch.snap.sort, v) + val cond = replacementCond(lhs, ch.args, condInfo) + ch.withSnap(Ite(cond, havockedSnap, ch.snap)) } otherChunks ++ newChunks } diff --git a/src/main/scala/rules/MagicWandSupporter.scala b/src/main/scala/rules/MagicWandSupporter.scala index 844f67a74..98ade45ff 100644 --- a/src/main/scala/rules/MagicWandSupporter.scala +++ b/src/main/scala/rules/MagicWandSupporter.scala @@ -79,25 +79,9 @@ object magicWandSupporter extends SymbolicExecutionRules { // result // } - //TODO: needs to calculate a snapshot that preserves values from the lhs - def createChunk(s: State, - wand: ast.MagicWand, - pve: PartialVerificationError, - v: Verifier) - (Q: (State, MagicWandChunk, Verifier) => VerificationResult) - : VerificationResult = - createChunk(s, wand, MagicWandSnapshot(freshSnap(sorts.Snap, v), freshSnap(sorts.Snap, v)), pve, v)(Q) - - def createChunk(s: State, - wand: ast.MagicWand, - abstractLhs: Term, - rhsSnapshot: Term, - pve: PartialVerificationError, - v: Verifier) - (Q: (State, MagicWandChunk, Verifier) => VerificationResult) - : VerificationResult = - createChunk(s, wand, MagicWandSnapshot(abstractLhs, rhsSnapshot), pve, v)(Q) - + /** + * Evaluate the wand's arguments and create a [[viper.silicon.state.MagicWandChunk]] out of it. + */ def createChunk(s: State, wand: ast.MagicWand, snap: MagicWandSnapshot, @@ -110,6 +94,37 @@ object magicWandSupporter extends SymbolicExecutionRules { ) } + /** + * Create a new [[viper.silicon.state.terms.MagicWandSnapshot]] + * and add the corresponding [[viper.silicon.state.terms.sorts.MagicWandSnapFunction]] definition to the state. + * + * It defines that when we apply the MagicWandSnapFunction to a snapshot `snap` + * we will get back `rhsSnapshot` that includes the values from that snapshot `snap`. + * + * @param abstractLhs The term that represent the snapshot of the consumed left-hand side of the magic wand. + * It is used as a bound variable in a forall quantifier. + * @param rhsSnapshot The term that integrates the left-hand side in the snapshot that is produced after applying the magic wand. + * @param v Verifier instance + * @return Fresh instance of [[viper.silicon.state.terms.MagicWandSnapshot]] + */ + def createMagicWandSnapshot(abstractLhs: Var, rhsSnapshot: Term, v: Verifier): MagicWandSnapshot = { + val mwsf = v.decider.fresh("mwsf", sorts.MagicWandSnapFunction) + val magicWandSnapshot = MagicWandSnapshot(mwsf) + v.decider.assumeDefinition(Forall( + abstractLhs, + MWSFLookup(mwsf, abstractLhs) === rhsSnapshot, + Trigger(MWSFLookup(mwsf, abstractLhs)) + )) + magicWandSnapshot + } + + /** + * Evaluate all expressions inside the given magic wand instance in the current state. + * + * @param s State in which to expressions are evaluated. + * @param wand Magic Wand instance. + * @param Q Method whose second argument is used to return the evaluated terms of all expressions. + */ def evaluateWandArguments(s: State, wand: ast.MagicWand, pve: PartialVerificationError, @@ -147,7 +162,7 @@ object magicWandSupporter extends SymbolicExecutionRules { val initial = (initialConsumptionResult, s, Stack.empty[Heap], Stack.empty[Option[CH]]) val (result, s1, heaps, consumedChunks) = hs.foldLeft[(ConsumptionResult, State, Stack[Heap], Stack[Option[CH]])](initial)((partialResult, heap) => - partialResult match { + partialResult match { case (r: Complete, sIn, hps, cchs) => (r, sIn, heap +: hps, None +: cchs) case (Incomplete(permsNeeded), sIn, hps, cchs) => val (success, sOut, h, cch) = consumeFunction(sIn, heap, permsNeeded, v) @@ -191,9 +206,25 @@ object magicWandSupporter extends SymbolicExecutionRules { } } -// private var cnt = 0L -// private val packageLogger = LoggerFactory.getLogger("package") - + /** + * Package a magic wand into a chunk. It performs the computation of the wand's footprint + * and captures all values associated to these locations inside the wand's snapshot. + * + * {{{ + * package A --* B { } + * }}} + * + * For reference see Chapter 3 and 5 of [[http://malte.schwerhoff.de/docs/phd_thesis.pdf Malte Schwerhoff's PhD thesis]] + * and [[https://ethz.ch/content/dam/ethz/special-interest/infk/chair-program-method/pm/documents/Education/Theses/Nils_Becker_BA_report.pdf Nils Becker's Bachelor report]] + * + * @param state Current state. + * @param wand AST representation of the magic wand. + * @param proofScript AST of the proof script. The proof script contains instructions how we can construct the RHS given the LHS. + * @param pve Partial Verification Error that is used to report errors. + * @param v Verifier instance. + * @param Q Continuation-style function that is called with the resulting state and the chunk that was created. + * @return Result of the overall verification process. + */ def packageWand(state: State, wand: ast.MagicWand, proofScript: ast.Seqn, @@ -202,42 +233,16 @@ object magicWandSupporter extends SymbolicExecutionRules { (Q: (State, Chunk, Verifier) => VerificationResult) : VerificationResult = { - /* TODO: Logging code is very similar to that in HeuristicsSupporter. Unify. */ - -// val myId = cnt; cnt += 1 -// val baseIdent = " " -// var printedHeader = false - -// def lnsay(msg: String, ident: Int = 1) { -// val prefix = "\n" + (if (ident == 0) "" else baseIdent) -// dosay(prefix, msg, ident - 1) -// } -// -// def say(msg: String, ident: Int = 1) { -// val prefix = if (ident == 0) "" else baseIdent -// dosay(prefix, msg, ident - 1) -// } -// -// def dosay(prefix: String, msg: String, ident: Int) { -// if (!printedHeader) { -// packageLogger.debug(s"\n[packageWand $myId]") -// printedHeader = true -// } -// -// val messagePrefix = baseIdent * ident -// packageLogger.debug(s"$prefix$messagePrefix $msg") -// } -// -// say(s"wand = $wand") -// say("c.reserveHeaps:") -// s.reserveHeaps.map(v.stateFormatter.format).foreach(str => say(str, 2)) - val s = if (state.exhaleExt) state else state.copy(reserveHeaps = Heap() :: state.h :: Nil) + // v.logger.debug(s"wand = $wand") + // v.logger.debug("c.reserveHeaps:") + // s.reserveHeaps.map(v.stateFormatter.format).foreach(str => v.logger.debug(str, 2)) + val stackSize = 3 + s.reserveHeaps.tail.size - /* IMPORTANT: Size matches structure of reserveHeaps at [State RHS] below */ - var results: Seq[(State, Stack[Term], Stack[Option[Exp]], Vector[RecordedPathConditions], Chunk)] = Nil + // IMPORTANT: Size matches structure of reserveHeaps at [State RHS] below + var recordedBranches: Seq[(State, Stack[Term], Stack[Option[Exp]], Vector[Term], Chunk)] = Nil /* TODO: When parallelising branches, some of the runtime assertions in the code below crash * during some executions - since such crashes are hard to debug, branch parallelisation @@ -250,67 +255,84 @@ object magicWandSupporter extends SymbolicExecutionRules { recordPcs = true, parallelizeBranches = false) - def createWandChunkAndRecordResults(s4: State, - freshSnapRoot: Var, - snap: Term, - v3: Verifier) - : VerificationResult = { + def appendToResults(s5: State, ch: Chunk, pcs: RecordedPathConditions, conservedPcs: Vector[Term], v4: Verifier): Unit = { + assert(s5.conservedPcs.nonEmpty, s"Unexpected structure of s5.conservedPcs: ${s5.conservedPcs}") - def appendToResults(s5: State, ch: Chunk, pcs: RecordedPathConditions, v4: Verifier): Unit = { - assert(s5.conservedPcs.nonEmpty, s"Unexpected structure of s5.conservedPcs: ${s5.conservedPcs}") + var conservedPcsStack: Stack[Vector[RecordedPathConditions]] = s5.conservedPcs - var conservedPcs: Vector[RecordedPathConditions] = Vector.empty - var conservedPcsStack: Stack[Vector[RecordedPathConditions]] = s5.conservedPcs + // Producing a wand's LHS and executing the packaging proof code can introduce definitional path conditions, e.g. + // new permission and snapshot maps, which are in general necessary to proceed after the + // package statement, e.g. to know which permissions have been consumed. + // Here, we want to keep *only* the definitions, but no other path conditions. - // Producing a wand's LHS and executing the packaging proof code can introduce definitional path conditions, e.g. - // new permission and snapshot maps, which are in general necessary to proceed after the - // package statement, e.g. to know which permissions have been consumed. - // Here, we want to keep *only* the definitions, but no other path conditions. + conservedPcsStack = + s5.conservedPcs.tail match { + case empty @ Seq() => empty + case head +: tail => (head ++ (s5.conservedPcs.head :+ pcs.definitionsOnly)) +: tail + } - conservedPcs = s5.conservedPcs.head :+ pcs.definitionsOnly + val s6 = s5.copy(conservedPcs = conservedPcsStack, recordPcs = s.recordPcs) - conservedPcsStack = - s5.conservedPcs.tail match { - case empty @ Seq() => empty - case head +: tail => (head ++ conservedPcs) +: tail - } + recordedBranches :+= (s6, v4.decider.pcs.branchConditions, v4.decider.pcs.branchConditionExps, conservedPcs, ch) + } - val s6 = s5.copy(conservedPcs = conservedPcsStack, recordPcs = s.recordPcs) + def createWandChunkAndRecordResults(s4: State, + freshSnapRoot: Var, + snapRhs: Term, + v3: Verifier) + : VerificationResult = { + val preMark = v3.decider.setPathConditionMark() - results :+= (s6, v4.decider.pcs.branchConditions, v4.decider.pcs.branchConditionExps, conservedPcs, ch) - } + v3.decider.prover.comment(s"Create MagicWandSnapFunction for wand $wand") + val wandSnapshot = this.createMagicWandSnapshot(freshSnapRoot, snapRhs, v3) - val preMark = v3.decider.setPathConditionMark() + // If the wand is used as a quantified resource anywhere in the program if (s4.qpMagicWands.contains(MagicWandIdentifier(wand, s.program))) { val bodyVars = wand.subexpressionsToEvaluate(s.program) val formalVars = bodyVars.indices.toList.map(i => Var(Identifier(s"x$i"), v.symbolConverter.toSort(bodyVars(i).typ), false)) + evals(s4, bodyVars, _ => pve, v3)((s5, args, v4) => { - val (sm, smValueDef) = - quantifiedChunkSupporter.singletonSnapshotMap(s5, wand, args, MagicWandSnapshot(freshSnapRoot, snap), v4) + val snapshotTerm = Combine(freshSnapRoot, snapRhs) + val (sm, smValueDef) = quantifiedChunkSupporter.singletonSnapshotMap(s5, wand, args, snapshotTerm, v4) v4.decider.prover.comment("Definitional axioms for singleton-SM's value") v4.decider.assumeDefinition(smValueDef) val ch = quantifiedChunkSupporter.createSingletonQuantifiedChunk(formalVars, wand, args, FullPerm, sm, s.program) - appendToResults(s5, ch, v4.decider.pcs.after(preMark), v4) + val conservedPcs = (s5.conservedPcs.head :+ v4.decider.pcs.after(preMark).definitionsOnly).flatMap(_.conditionalized) + appendToResults(s5, ch, v4.decider.pcs.after(preMark), conservedPcs, v4) Success() }) } else { - magicWandSupporter.createChunk(s4, wand, freshSnapRoot, snap, pve, v3)((s5, ch, v4) => { -// say(s"done: create wand chunk: $ch") - appendToResults(s5, ch, v4.decider.pcs.after(preMark), v4) + this.createChunk(s4, wand, wandSnapshot, pve, v3)((s5, ch, v4) => { + val conservedPcs = s5.conservedPcs.head :+ v4.decider.pcs.after(preMark).definitionsOnly + // Partition path conditions into a set which include the freshSnapRoot and those which do not + val (pcsWithFreshSnapRoot, pcsWithoutFreshSnapRoot) = conservedPcs.flatMap(_.conditionalized).partition(pcs => pcs.contains(freshSnapRoot)) + // For all path conditions which include the freshSnapRoot, add those as part of the definition of the MWSF in the same forall quantifier + val pcsQuantified = Forall( + freshSnapRoot, + And(pcsWithFreshSnapRoot.map { + // Remove forall quantifiers with the same quantified variable + case Quantification(Forall, v :: Nil, body: Term, _, _, _, _) if v == freshSnapRoot => body + case p => p + }), + Trigger(MWSFLookup(wandSnapshot.mwsf, freshSnapRoot)), + ) + + appendToResults(s5, ch, v4.decider.pcs.after(preMark), pcsQuantified +: pcsWithoutFreshSnapRoot, v4) Success() }) } } - val r = executionFlowController.locally(sEmp, v)((s1, v1) => { - /* Using conservingSnapshotGeneration a snapshot (binary tree) will be - * constructed using First/Second datatypes, that preserves the original root. - * The leafs of this tree will later appear in the snapshot of the rhs at the - * appropriate places. Thus equating freshSnapRoot with the snapshot received - * from consuming the lhs when applying the wand preserves values from the lhs - * into the rhs. + val tempResult = executionFlowController.locally(sEmp, v)((s1, v1) => { + /* A snapshot (binary tree) will be constructed using First/Second datatypes, + * that preserves the original root. The leafs of this tree will later appear + * in the snapshot of the RHS at the appropriate places. Thus equating + * `freshSnapRoot` with the snapshot received from consuming the LHS when + * applying the wand preserves values from the LHS into the RHS. */ val freshSnapRoot = freshSnap(sorts.Snap, v1) + + // Produce the wand's LHS. produce(s1.copy(conservingSnapshotGeneration = true), toSf(freshSnapRoot), wand.left, pve, v1)((sLhs, v2) => { val proofScriptCfg = proofScript.toCfg() @@ -331,26 +353,31 @@ object magicWandSupporter extends SymbolicExecutionRules { * empty, and where the dots represent the heaps belonging to surrounding package/packaging * operations. hOps will be populated while processing the RHS of the wand to package. * More precisely, each ghost operation (folding, applying, etc.) that is executed - * populates hUsed (by transferring permissions from heaps lower in the stack, and by - * adding new chunks, e.g. a folded predicate) during its execution, and afterwards - * merges hUsed and hOps, the result of which replaces hOps, and hUsed is replaced by a - * new empty heap (see also the final state updates in, e.g. method `applyingWand` - * or `unfoldingPredicate` below). + * populates hUsed during its execution. This is done by transferring permissions + * from heaps lower in the stack, and by adding new chunks, e.g. a folded predicate. + * Afterwards, it merges hUsed and hOps, which replaces hOps. hUsed is replaced by a + * new empty heap. See also the final state updates in, e.g. method `applyingWand` + * or `unfoldingPredicate` below. */ assert(stackSize == s2.reserveHeaps.length) -// say(s"done: produced LHS ${wand.left}") -// say(s"next: consume RHS ${wand.right}") + // Execute proof script, i.e. the part written after the magic wand wrapped by curly braces. + // The proof script should transform the current state such that we can consume the wand's RHS. executor.exec(s2, proofScriptCfg, v2)((proofScriptState, proofScriptVerifier) => { - consume(proofScriptState.copy(oldHeaps = s2.oldHeaps, reserveCfgs = proofScriptState.reserveCfgs.tail), wand.right, pve, proofScriptVerifier)((s3, snap, v3) => { -// say(s"done: consumed RHS ${wand.right}") - val s4 = s3.copy(//h = s.h, /* Temporarily */ - exhaleExt = false, - oldHeaps = s.oldHeaps) -// say(s"next: create wand chunk") - createWandChunkAndRecordResults(s4, freshSnapRoot, snap, v3)})})})}) - - if (results.isEmpty) { + // Consume the wand's RHS and produce a snapshot which records all the values of variables on the RHS. + // This part indirectly calls the methods `this.transfer` and `this.consumeFromMultipleHeaps`. + consume( + proofScriptState.copy(oldHeaps = s2.oldHeaps, reserveCfgs = proofScriptState.reserveCfgs.tail), + wand.right, pve, proofScriptVerifier + )((s3, snapRhs, v3) => { + + createWandChunkAndRecordResults(s3.copy(exhaleExt = false, oldHeaps = s.oldHeaps), freshSnapRoot, snapRhs, v3) + }) + }) + }) + }) + + if (recordedBranches.isEmpty) { // No results mean that packaging the wand resulted in inconsistent states on all paths, // and thus, that no wand chunk was created. In order to continue, we create one now. // Moreover, we need to set reserveHeaps to structurally match [State RHS] below. @@ -358,41 +385,83 @@ object magicWandSupporter extends SymbolicExecutionRules { createWandChunkAndRecordResults(s1, freshSnap(sorts.Snap, v), freshSnap(sorts.Snap, v), v) } - results.foldLeft(r)((res, packageOut) => { - res && { - val state = packageOut._1 - val branchConditions = packageOut._2 - val branchConditionsExp = packageOut._3 - val conservedPcs = packageOut._4 - val magicWandChunk = packageOut._5 - val s1 = state.copy(reserveHeaps = state.reserveHeaps.drop(3), + recordedBranches.foldLeft(tempResult)((prevRes, recordedState) => { + prevRes && { + val (state, branchConditions, branchConditionsExp, conservedPcs, magicWandChunk) = recordedState + val s1 = state.copy( + reserveHeaps = state.reserveHeaps.drop(3), parallelizeBranches = s.parallelizeBranches /* See comment above */ - /*branchConditions = c.branchConditions*/) + ) + + // We execute the continuation Q in a new scope with all branch conditions and all conserved path conditions. executionFlowController.locally(s1, v)((s2, v1) => { + // Set the branch conditions v1.decider.setCurrentBranchCondition(And(branchConditions), Some(viper.silicon.utils.ast.BigAnd(branchConditionsExp.flatten))) - conservedPcs.foreach(pcs => v1.decider.assume(pcs.conditionalized)) - Q(s2, magicWandChunk, v1)})}}) + + // Recreate all path conditions in the Z3 proof script that we recorded for that branch + conservedPcs.foreach(pcs => v1.decider.assume(pcs)) + + // Execute the continuation Q + Q(s2, magicWandChunk, v1) + }) + } + }) } + /** + * Apply a magic wand to the current state. This consumes the magic wand itself and the LHS of the wand, and then produces the RHS. + * + * @param s Current state. + * @param wand The AST instance of the magic wand to apply. + * @param pve Partial Verification Error that is used to report errors. + * @param v Verifier instance. + * @param Q Continuation-style function that is called with the resulting state and the verification result. + * @return Result of the overall verification process. + */ def applyWand(s: State, wand: ast.MagicWand, pve: PartialVerificationError, v: Verifier) (Q: (State, Verifier) => VerificationResult) : VerificationResult = { - consume(s, wand, pve, v)((s1, snap, v1) => { - val wandSnap = MagicWandSnapshot(snap) - consume(s1, wand.left, pve, v1)((s2, snap, v2) => { - /* It is assumed that snap and wandSnap.abstractLhs are structurally the same. - * Since a wand can only be applied once, equating the two snapshots is sound. - */ - assert(snap.sort == sorts.Snap, s"expected snapshot but found: $snap") - v2.decider.assume(snap === wandSnap.abstractLhs) - val s3 = s2.copy(oldHeaps = s1.oldHeaps + (Verifier.MAGIC_WAND_LHS_STATE_LABEL -> magicWandSupporter.getEvalHeap(s1))) - produce(s3.copy(conservingSnapshotGeneration = true), toSf(wandSnap.rhsSnapshot), wand.right, pve, v2)((s4, v3) => { - val s5 = s4.copy(g = s1.g, conservingSnapshotGeneration = s3.conservingSnapshotGeneration) - val s6 = v3.stateConsolidator(s5).consolidate(s5, v3).copy(oldHeaps = s1.oldHeaps) - Q(s6, v3)})})})} + // Consume the magic wand instance "A --* B". + consume(s, wand, pve, v)((s1, snapWand, v1) => { + // Consume the wand's LHS "A". + consume(s1, wand.left, pve, v1)((s2, snapLhs, v2) => { + /* It is assumed that snap and MagicWandSnapshot.abstractLhs are structurally the same. + * Equating the two snapshots is sound iff a wand is applied only once. + * The old solution in this case did use this assumption: + * v2.decider.assume(snap === snapWand.abstractLhs) + */ + assert(snapLhs.sort == sorts.Snap, s"expected snapshot but found: $snapLhs") + + // Create copy of the state with a new labelled heap (i.e. `oldHeaps`) called "lhs". + val s3 = s2.copy(oldHeaps = s1.oldHeaps + (Verifier.MAGIC_WAND_LHS_STATE_LABEL -> this.getEvalHeap(s1))) + + // If the snapWand is a (wrapped) MagicWandSnapshot then lookup the snapshot of the right-hand side by applying snapLhs. + val magicWandSnapshotLookup = snapWand match { + case snapshot: MagicWandSnapshot => snapshot.applyToMWSF(snapLhs) + case SortWrapper(snapshot: MagicWandSnapshot, _) => snapshot.applyToMWSF(snapLhs) + // Fallback solution for quantified magic wands + case predicateLookup: PredicateLookup => + v2.decider.assume(snapLhs === First(snapWand)) + Second(predicateLookup) + case _ => snapWand + } + + // Produce the wand's RHS. + produce(s3.copy(conservingSnapshotGeneration = true), toSf(magicWandSnapshotLookup), wand.right, pve, v2)((s4, v3) => { + // Recreate old state without the magic wand, and the state with the oldHeap called lhs. + val s5 = s4.copy(g = s1.g, conservingSnapshotGeneration = s3.conservingSnapshotGeneration) + + // Consolidate the state and remove labelled old heap "lhs". + val s6 = v3.stateConsolidator(s5).consolidate(s5, v3).copy(oldHeaps = s1.oldHeaps) + + Q(s6, v3) + }) + }) + }) + } def transfer[CH <: Chunk] (s: State, @@ -416,7 +485,7 @@ object magicWandSupporter extends SymbolicExecutionRules { */ val preMark = v.decider.setPathConditionMark() executionFlowController.tryOrFail2[Stack[Heap], Stack[Option[CH]]](s, v)((s1, v1, QS) => - magicWandSupporter.consumeFromMultipleHeaps(s1, s1.reserveHeaps.tail, perms, failure, qvars, v1)(consumeFunction)(QS) + this.consumeFromMultipleHeaps(s1, s1.reserveHeaps.tail, perms, failure, qvars, v1)(consumeFunction)(QS) )((s2, hs2, chs2, v2) => { val conservedPcs = s2.conservedPcs.head :+ v2.decider.pcs.after(preMark) val s3 = s2.copy(conservedPcs = conservedPcs +: s2.conservedPcs.tail, reserveHeaps = s.reserveHeaps.head +: hs2) diff --git a/src/main/scala/rules/MoreCompleteExhaleSupporter.scala b/src/main/scala/rules/MoreCompleteExhaleSupporter.scala index 5c7173c8a..8e983f573 100644 --- a/src/main/scala/rules/MoreCompleteExhaleSupporter.scala +++ b/src/main/scala/rules/MoreCompleteExhaleSupporter.scala @@ -55,7 +55,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { resource match { case f: ast.Field => v.symbolConverter.toSort(f.typ) case _: ast.Predicate => sorts.Snap - case _: ast.MagicWand => sorts.Snap + case _: ast.MagicWand => sorts.MagicWandSnapFunction } val `?s` = Var(Identifier("?s"), sort, false) diff --git a/src/main/scala/rules/Producer.scala b/src/main/scala/rules/Producer.scala index 33d8a1126..f3976c827 100644 --- a/src/main/scala/rules/Producer.scala +++ b/src/main/scala/rules/Producer.scala @@ -397,7 +397,7 @@ object producer extends ProductionRules { Q(s2, v1)}) case wand: ast.MagicWand => - val snap = sf(sorts.Snap, v) + val snap = sf(sorts.MagicWandSnapFunction, v) magicWandSupporter.createChunk(s, wand, MagicWandSnapshot(snap), pve, v)((s1, chWand, v1) => chunkSupporter.produce(s1, s1.h, chWand, v1)((s2, h2, v2) => Q(s2.copy(h = h2), v2))) diff --git a/src/main/scala/rules/QuantifiedChunkSupport.scala b/src/main/scala/rules/QuantifiedChunkSupport.scala index ae427d057..4f8902dbc 100644 --- a/src/main/scala/rules/QuantifiedChunkSupport.scala +++ b/src/main/scala/rules/QuantifiedChunkSupport.scala @@ -637,7 +637,6 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { /* Snapshots */ - /** @inheritdoc */ def singletonSnapshotMap(s: State, resource: ast.Resource, arguments: Seq[Term], diff --git a/src/main/scala/state/Chunks.scala b/src/main/scala/state/Chunks.scala index 2385d7935..44b907031 100644 --- a/src/main/scala/state/Chunks.scala +++ b/src/main/scala/state/Chunks.scala @@ -176,13 +176,16 @@ case class MagicWandChunk(id: MagicWandIdentifier, override val resourceID = MagicWandID override def withPerm(newPerm: Term) = MagicWandChunk(id, bindings, args, snap, newPerm) - override def withSnap(newSnap: Term) = MagicWandChunk(id, bindings, args, MagicWandSnapshot(newSnap), perm) + override def withSnap(newSnap: Term) = newSnap match { + case s: MagicWandSnapshot => MagicWandChunk(id, bindings, args, s, perm) + case _ => sys.error(s"MagicWand snapshot has to be of type MagicWandSnapshot but found ${newSnap.getClass}") + } override lazy val toString = { val pos = id.ghostFreeWand.pos match { case rp: viper.silver.ast.HasLineColumn => s"${rp.line}:${rp.column}" case other => other.toString } - s"wand@$pos[$snap; ${args.mkString(",")}]" + s"wand@$pos[$snap; ${args.mkString(", ")}]" } } diff --git a/src/main/scala/state/Terms.scala b/src/main/scala/state/Terms.scala index ed00e5541..e08f4854b 100644 --- a/src/main/scala/state/Terms.scala +++ b/src/main/scala/state/Terms.scala @@ -76,6 +76,11 @@ object sorts { override lazy val toString = id.toString } + object MagicWandSnapFunction extends Sort { + val id: Identifier = Identifier("MWSF") + override lazy val toString: String = id.toString + } + case class FieldPermFunction() extends Sort { val id = Identifier("FPM") override lazy val toString = id.toString @@ -321,39 +326,39 @@ sealed trait Term extends Node { lazy val subterms: Seq[Term] = state.utils.subterms(this) - /** @see [[ast.utility.Visitor.visit()]] */ + /** @see [[ast.utility.Visitor.visit]] */ def visit(f: PartialFunction[Term, Any]): Unit = ast.utility.Visitor.visit(this, state.utils.subterms)(f) - /** @see [[ast.utility.Visitor.visitOpt()]] */ + /** @see [[ast.utility.Visitor.visitOpt]] */ def visitOpt(f: Term => Boolean): Unit = ast.utility.Visitor.visitOpt(this, state.utils.subterms)(f) - /** @see [[ast.utility.Visitor.reduceTree()]] */ + /** @see [[ast.utility.Visitor.reduceTree]] */ def reduceTree[R](f: (Term, Seq[R]) => R): R = ast.utility.Visitor.reduceTree(this, state.utils.subterms)(f) - /** @see [[ast.utility.Visitor.existsDefined()]] */ + /** @see [[ast.utility.Visitor.existsDefined]] */ def existsDefined(f: PartialFunction[Term, Any]): Boolean = ast.utility.Visitor.existsDefined(this, state.utils.subterms)(f) - /** @see [[ast.utility.Visitor.hasSubnode()]] */ + /** @see [[ast.utility.Visitor.hasSubnode]] */ def hasSubterm(subterm: Term): Boolean = ast.utility.Visitor.hasSubnode(this, subterm, state.utils.subterms) - /** @see [[ast.utility.Visitor.deepCollect()]] */ + /** @see [[ast.utility.Visitor.deepCollect]] */ def deepCollect[R](f: PartialFunction[Term, R]) : Seq[R] = ast.utility.Visitor.deepCollect(Seq(this), state.utils.subterms)(f) - /** @see [[ast.utility.Visitor.shallowCollect()]] */ + /** @see [[ast.utility.Visitor.shallowCollect]] */ def shallowCollect[R](f: PartialFunction[Term, R]): Seq[R] = ast.utility.Visitor.shallowCollect(Seq(this), state.utils.subterms)(f) - /** @see [[ast.utility.Visitor.find()]] */ + /** @see [[ast.utility.Visitor.find]] */ def find[R](f: PartialFunction[Term, R]): Option[R] = ast.utility.Visitor.find(this, state.utils.subterms)(f) - /** @see [[state.utils.transform()]] */ + /** @see [[state.utils.transform]] */ def transform(pre: PartialFunction[Term, Term] = PartialFunction.empty) (recursive: Term => Boolean = !pre.isDefinedAt(_), post: PartialFunction[Term, Term] = PartialFunction.empty) @@ -2295,48 +2300,63 @@ object PredicateTrigger extends PreciseCondFlyweightFactory[(String, Term, Seq[T /* Magic wands */ -class MagicWandSnapshot(val abstractLhs: Term, val rhsSnapshot: Term) extends Combine(abstractLhs, rhsSnapshot) { - utils.assertSort(abstractLhs, "abstract lhs", sorts.Snap) - utils.assertSort(rhsSnapshot, "rhs", sorts.Snap) +/** + * Represents a snapshot of a magic wand, which is a function from `Snap` to `Snap`. + * + * @param mwsf The function that represents the snapshot of the magic wand. It is a variable of sort [[sorts.MagicWandSnapFunction]]. + * In the symbolic execution when we apply a magic wand, it consumes the left-hand side + * and uses this function and the resulting snapshot to look up which right-hand side to produce. + */ +class MagicWandSnapshot(val mwsf: Term) extends Term with ConditionalFlyweight[Term, MagicWandSnapshot] { + utils.assertSort(mwsf, "magic wand snap function", sorts.MagicWandSnapFunction) - override lazy val toString = s"wandSnap(lhs = $abstractLhs, rhs = $rhsSnapshot)" + override val sort: Sort = sorts.MagicWandSnapFunction - def merge(other: MagicWandSnapshot, branchConditions: Stack[Term]): MagicWandSnapshot = { - assert(this.abstractLhs == other.abstractLhs) - val condition = And(branchConditions) - MagicWandSnapshot(this.abstractLhs, if (this.rhsSnapshot == other.rhsSnapshot) - this.rhsSnapshot - else - Ite(condition, other.rhsSnapshot, this.rhsSnapshot)) - } + override lazy val toString = s"wandSnap($mwsf)" + + override val equalityDefiningMembers: Term = mwsf + + /** + * Apply the given snapshot of the left-hand side to the magic wand map to get the snapshot of the right-hand side + * which includes the values of the left-hand side. + * + * @param snapLhs The snapshot of the left-hand side that should be applied to the magic wand map. + * @return The snapshot of the right-hand side that preserves the values of the left-hand side. + */ + def applyToMWSF(snapLhs: Term): Term = MWSFLookup(mwsf, snapLhs) } -object MagicWandSnapshot { - def apply(snapshot: Term): MagicWandSnapshot = { - assert(snapshot.sort == sorts.Snap) - snapshot match { - case snap: MagicWandSnapshot => snap - case _ => - MagicWandSnapshot(First(snapshot), Second(snapshot)) - } - } +object MagicWandSnapshot extends PreciseCondFlyweightFactory[Term, MagicWandSnapshot] { + /** Create an instance of [[viper.silicon.state.terms.MagicWandSnapshot]]. */ + override def actualCreate(arg: Term): MagicWandSnapshot = + new MagicWandSnapshot(arg) +} - // Since MagicWandSnapshot subclasses Combine, we apparently cannot inherit the normal subclass, so we - // have to copy paste the code here. - var pool = new TrieMap[(Term, Term), MagicWandSnapshot]() +/** + * Term that applies a [[sorts.MagicWandSnapFunction]] to a snapshot. + * It returns a snapshot for the RHS of a magic wand that includes that values of the given snapshot. + * + * @param mwsf Term of sort [[sorts.MagicWandSnapFunction]]. Function from `Snap` to `Snap`. + * @param snap Term of sort [[sorts.Snap]] to which the MWSF is applied to. It represents the values of the wand's LHS. + */ +class MWSFLookup(val mwsf: Term, val snap: Term) extends Term with ConditionalFlyweightBinaryOp[MWSFLookup] { + val sort: Sort = sorts.Snap + override def p0: Term = mwsf + override def p1: Term = snap + override lazy val toString = s"$mwsf[$snap]" +} - def createIfNonExistent(args: (Term, Term)): MagicWandSnapshot = { - if (Verifier.config.useFlyweight) { - pool.getOrElseUpdate(args, actualCreate(args)) - } else { - actualCreate(args) - } +object MWSFLookup extends PreciseCondFlyweightFactory[(Term, Term), MWSFLookup] { + override def apply(pair: (Term, Term)): MWSFLookup = { + val (mwsf, snap) = pair + utils.assertSort(mwsf, "mwsf", sorts.MagicWandSnapFunction) + utils.assertSort(snap, "snap", sorts.Snap) + createIfNonExistent(pair) } - def actualCreate(tuple: (Term, Term)) = new MagicWandSnapshot(tuple._1, tuple._2) - def apply(fst: Term, snd: Term): MagicWandSnapshot = createIfNonExistent((fst, snd)) - - def unapply(mws: MagicWandSnapshot) = Some((mws.abstractLhs, mws.rhsSnapshot)) + /** Create an instance of [[viper.silicon.state.terms.MWSFLookup]]. */ + override def actualCreate(args: (Term, Term)): MWSFLookup = + new MWSFLookup(args._1, args._2) } class MagicWandChunkTerm(val chunk: MagicWandChunk) extends Term with ConditionalFlyweight[MagicWandChunk, MagicWandChunkTerm] { @@ -2461,7 +2481,7 @@ object PsfTop extends (String => Identifier) { */ /* Note: Sort wrappers should probably not be used as (outermost) triggers - * because they are optimised away if wrappee `t` already has sort `to`. + * because they are optimised away if wrapped `t` already has sort `to`. */ class SortWrapper(val t: Term, val to: Sort) extends Term diff --git a/src/main/scala/state/Utils.scala b/src/main/scala/state/Utils.scala index 38a1abbff..d2667e8cd 100644 --- a/src/main/scala/state/Utils.scala +++ b/src/main/scala/state/Utils.scala @@ -94,7 +94,7 @@ package object utils { } - /** @see [[viper.silver.ast.utility.Transformer.simplify()]] */ + /** @see [[viper.silver.ast.utility.Simplifier.simplify]] */ def transform[T <: Term](term: T, pre: PartialFunction[Term, Term] = PartialFunction.empty) (recursive: Term => Boolean = !pre.isDefinedAt(_), @@ -196,7 +196,8 @@ package object utils { case MapUpdate(t0, t1, t2) => MapUpdate(go(t0), go(t1), go(t2)) case MapDomain(t) => MapDomain(go(t)) case MapRange(t) => MapRange(go(t)) - case MagicWandSnapshot(lhs, rhs) => MagicWandSnapshot(go(lhs), go(rhs)) + case MagicWandSnapshot(t) => MagicWandSnapshot(go(t)) + case MWSFLookup(t0, t1) => MWSFLookup(go(t0), go(t1)) case Combine(t0, t1) => Combine(go(t0), go(t1)) case First(t) => First(go(t)) case Second(t) => Second(go(t)) diff --git a/src/main/scala/supporters/BuiltinDomainsContributor.scala b/src/main/scala/supporters/BuiltinDomainsContributor.scala index f181a298a..bb01d2fd0 100644 --- a/src/main/scala/supporters/BuiltinDomainsContributor.scala +++ b/src/main/scala/supporters/BuiltinDomainsContributor.scala @@ -8,7 +8,6 @@ package viper.silicon.supporters import java.io.File import java.net.URL - import scala.annotation.unused import scala.reflect.ClassTag import viper.silver.ast @@ -57,38 +56,20 @@ abstract class BuiltinDomainsContributor extends PreambleContributor[Sort, Domai def analyze(program: ast.Program): Unit = { val builtinDomainTypeInstances = computeGroundTypeInstances(program) - val sourceProgram = utils.loadProgramFromUrl(sourceUrl) + val sourceProgram = loadProgramFromUrl(sourceUrl) val sourceDomain = transformSourceDomain(sourceProgram.findDomain(sourceDomainName)) + // List of all domains found in the program with their instantiations, i.e. the types they are used with val sourceDomainTypeInstances = builtinDomainTypeInstances map (builtinTypeInstance => { - val instantiation : Map[viper.silver.ast.TypeVar,viper.silver.ast.Type] = sourceDomain.typVars.zip(builtinTypeInstance.typeArguments).toMap - //(instantiation, ast.DomainType(sourceDomain, instantiation)) + val instantiation: Map[viper.silver.ast.TypeVar, viper.silver.ast.Type] = sourceDomain.typVars.zip(builtinTypeInstance.typeArguments).toMap ast.DomainType(sourceDomain, instantiation) }) - /* For each necessary domain type, instantiate the corresponding domain */ - val sourceDomainInstantiationsWithType = - sourceDomainTypeInstances map (mdt => { - /* TODO: Copied from DomainInstances.getInstanceMembers. - * Cannot directly use that because it filters according to which domain instances - * are used in the program from which the source domain was loaded, whereas the - * instances should be filtered according to which are used in the program under - * verification. - */ - val functions = sourceDomain.functions.map(ast.utility.DomainInstances.substitute(_, mdt.typVarsMap, sourceProgram)).distinct - val axioms = sourceDomain.axioms.map(ast.utility.DomainInstances.substitute(_, mdt.typVarsMap, sourceProgram)).distinct - - val instance = - sourceDomain.copy(functions = functions, axioms = axioms)(sourceDomain.pos, sourceDomain.info, sourceDomain.errT) - - (mdt, transformSourceDomainInstance(instance, mdt)) - }) - - val sourceDomainInstantiations = sourceDomainInstantiationsWithType.map(x => x._2) + val sourceDomainInstantiationsWithType = instantiateWithDomain(sourceProgram, sourceDomain, sourceDomainTypeInstances) collectSorts(sourceDomainTypeInstances) - collectFunctions(sourceDomainInstantiations, program) + collectFunctions(sourceDomainInstantiationsWithType, program) collectAxioms(sourceDomainInstantiationsWithType) } @@ -97,6 +78,26 @@ abstract class BuiltinDomainsContributor extends PreambleContributor[Sort, Domai case builtinDomainTypeTag(s) => s }) + /** + * For each necessary domain type, instantiate the corresponding domain + */ + private def instantiateWithDomain(sourceProgram: ast.Program, sourceDomain: ast.Domain, sourceDomainTypeInstances: InsertionOrderedSet[ast.DomainType]): Set[(ast.DomainType, ast.Domain)] = { + sourceDomainTypeInstances map (domainType => { + /* TODO: Copied from DomainInstances.getInstanceMembers. + * Cannot directly use that because it filters according to which domain instances + * are used in the program from which the source domain was loaded, whereas the + * instances should be filtered according to which are used in the program under + * verification. + */ + val functions = sourceDomain.functions.map(ast.utility.DomainInstances.substitute(_, domainType.typVarsMap, sourceProgram)).distinct + val axioms = sourceDomain.axioms.map(ast.utility.DomainInstances.substitute(_, domainType.typVarsMap, sourceProgram)).distinct + + val instance = sourceDomain.copy(functions = functions, axioms = axioms)(sourceDomain.pos, sourceDomain.info, sourceDomain.errT) + + (domainType, transformSourceDomainInstance(instance, domainType)) + }) + } + protected def transformSourceDomain(sourceDomain: ast.Domain): ast.Domain = sourceDomain protected def transformSourceDomainInstance(sourceDomain: ast.Domain, @unused typ: ast.DomainType): ast.Domain = sourceDomain @@ -110,9 +111,9 @@ abstract class BuiltinDomainsContributor extends PreambleContributor[Sort, Domai }) } - protected def collectFunctions(domains: Set[ast.Domain], program: ast.Program): Unit = { - domains foreach ( - _.functions foreach (df => + protected def collectFunctions(domains: Set[(ast.DomainType, ast.Domain)], program: ast.Program): Unit = { + domains foreach (d => + d._2.functions foreach (df => if (df.interpretation.isEmpty) collectedFunctions += symbolConverter.toFunction(df, program).asInstanceOf[DomainFun])) } @@ -129,7 +130,7 @@ abstract class BuiltinDomainsContributor extends PreambleContributor[Sort, Domai * are preserved. */ val domainName = f"${d.domainName}[${d.typVarsMap.values.map(t => symbolConverter.toSort(t)).mkString(",")}]" - domainTranslator.translateAxiom(ax, symbolConverter.toSort, true).transform { + domainTranslator.translateAxiom(ax, symbolConverter.toSort, builtin = true).transform { case q@Quantification(_,_,_,_,name,_,_) if name != "" => q.copy(name = f"${domainName}_${name}") case Equals(t1, t2) => BuiltinEquals(t1, t2) @@ -146,37 +147,19 @@ abstract class BuiltinDomainsContributor extends PreambleContributor[Sort, Domai collectedFunctions def declareSymbolsAfterAnalysis(sink: ProverLike): Unit = { - collectedFunctions foreach (f => sink.declare(FunctionDecl(f))) + symbolsAfterAnalysis foreach (f => sink.declare(FunctionDecl(f))) } def axiomsAfterAnalysis: Iterable[Term] = collectedAxioms def emitAxiomsAfterAnalysis(sink: ProverLike): Unit = { - collectedAxioms foreach (ax => sink.assume(ax)) - } - - def updateGlobalStateAfterAnalysis(): Unit = { /* Nothing to contribute*/ } -} - -class BuiltinDomainAwareSymbolConverter(sourceDomainName: String, - targetSortFactory: Iterable[Sort] => Sort) - extends DefaultSymbolConverter { - - override def toSort(typ: ast.Type): Sort = typ match { - case dt: ast.DomainType if dt.domainName == sourceDomainName => - targetSortFactory(dt.typVarsMap.values map toSort) - case other => - super.toSort(other) + axiomsAfterAnalysis foreach (ax => sink.assume(ax)) } -} -private object utils { - def loadProgramFromResource(resource: String): ast.Program = { - loadProgramFromUrl(getClass.getResource(resource)) - } + /* Utility */ // TODO: Check that Silver's parser doesn't already provide suitable functionality. - def loadProgramFromUrl(url: URL): ast.Program = { + private def loadProgramFromUrl(url: URL): ast.Program = { assert(url != null, s"Unexpectedly found sourceUrl == null") val fromPath = viper.silver.utility.Paths.pathFromResource(url) @@ -204,3 +187,15 @@ private object utils { program } } + +class BuiltinDomainAwareSymbolConverter(sourceDomainName: String, + targetSortFactory: Iterable[Sort] => Sort) + extends DefaultSymbolConverter { + + override def toSort(typ: ast.Type): Sort = typ match { + case dt: ast.DomainType if dt.domainName == sourceDomainName => + targetSortFactory(dt.typVarsMap.values map toSort) + case other => + super.toSort(other) + } +} diff --git a/src/main/scala/supporters/MagicWandSnapFunctionsContributor.scala b/src/main/scala/supporters/MagicWandSnapFunctionsContributor.scala new file mode 100644 index 000000000..c2b925c6a --- /dev/null +++ b/src/main/scala/supporters/MagicWandSnapFunctionsContributor.scala @@ -0,0 +1,92 @@ +// This Source Code Form is subject to the terms of the Mozilla Public +// License, v. 2.0. If a copy of the MPL was not distributed with this +// file, You can obtain one at http://mozilla.org/MPL/2.0/. +// +// Copyright (c) 2011-2024 ETH Zurich. + +package viper.silicon.supporters + +import viper.silicon.common.collections.immutable.InsertionOrderedSet +import viper.silicon.interfaces.{PreambleContributor, PreambleReader} +import viper.silicon.interfaces.decider.ProverLike +import viper.silicon.state.terms.{Sort, SortDecl, sorts} +import viper.silver.ast +import viper.silver.ast.Program + +/** + * Add function declarations when the proof makes use of MagicWandSnapFunctions (MWSF). + * Those are used to preserve values across multiple applications of a magic wand, e.g. by using an applying expression. + * + * @param preambleReader Reader that returns the content of some given SMT2 files. + */ +class MagicWandSnapFunctionsContributor(preambleReader: PreambleReader[String, String]) + extends PreambleContributor[Sort, String, String] { + + /** File which contains all function declarations in the SMT2 syntax. */ + private val FILE_DECLARATIONS = "/magic_wand_snap_functions_declarations.smt2" + + /** Set for the sort [[viper.silicon.state.terms.sorts.MagicWandSnapFunction]] */ + private var collectedSorts: InsertionOrderedSet[Sort] = InsertionOrderedSet.empty + + /** Set for all function declaration related to [[viper.silicon.state.terms.sorts.MagicWandSnapFunction]] */ + private var collectedFunctionDecls: Iterable[String] = Seq.empty + + /* Functionality */ + + /** + * Add all function declarations when a program contains magic wands. + * + * @param program AST of the program to prove. + */ + override def analyze(program: Program): Unit = { + // If there are not magic wands, do not add any definitions or axioms + if (!program.existsDefined { case ast.MagicWand(_, _) => true }) return + + collectedSorts = InsertionOrderedSet(sorts.MagicWandSnapFunction) + collectedFunctionDecls = preambleReader.readPreamble(FILE_DECLARATIONS) + } + + /** Sorts to add to the preamble of the SMT proof script. */ + override def sortsAfterAnalysis: Iterable[Sort] = collectedSorts + + /** Add all sorts needed to the preamble using `sink`. */ + override def declareSortsAfterAnalysis(sink: ProverLike): Unit = { + sortsAfterAnalysis foreach (s => sink.declare(SortDecl(s))) + } + + /** Symbols to add to the preamble of the SMT proof script. */ + override def symbolsAfterAnalysis: Iterable[String] = + extractPreambleLines(collectedFunctionDecls) + + /** Add all symbols needed to the preamble using `sink`. */ + override def declareSymbolsAfterAnalysis(sink: ProverLike): Unit = + emitPreambleLines(sink, collectedFunctionDecls) + + /** Axioms to add to the preamble of the SMT proof script. Currently, there are none. */ + override def axiomsAfterAnalysis: Iterable[String] = Seq.empty + + /** Add all axioms needed to the preamble using `sink`. Currently, there are none. */ + override def emitAxiomsAfterAnalysis(sink: ProverLike): Unit = {} + + /** Helper function to transform the lines returned by the `PreambleReader`. */ + private def extractPreambleLines(lines: Iterable[String]*): Iterable[String] = + lines.flatten + + /** Helper function to emit all lines using `sink`. */ + private def emitPreambleLines(sink: ProverLike, lines: Iterable[String]*): Unit = { + lines foreach { declaration => + sink.emit(declaration) + } + } + + /* Lifetime */ + + def reset(): Unit = { + collectedSorts = InsertionOrderedSet.empty + collectedFunctionDecls = Seq.empty + } + + def stop(): Unit = {} + + def start(): Unit = {} +} diff --git a/src/main/scala/supporters/qps/PredicateAndWandSnapFunctionsContributor.scala b/src/main/scala/supporters/qps/PredicateAndWandSnapFunctionsContributor.scala index 920405ec6..3da5802d1 100644 --- a/src/main/scala/supporters/qps/PredicateAndWandSnapFunctionsContributor.scala +++ b/src/main/scala/supporters/qps/PredicateAndWandSnapFunctionsContributor.scala @@ -21,7 +21,6 @@ import viper.silicon.state.terms.{Sort, SortDecl, sorts} import viper.silver.ast.PredicateAccess trait PredicateSnapFunctionsContributor[SO, SY, AX] extends PreambleContributor[SO, SY, AX] -trait MagicWandSnapFunctionsContributor[SO, SY, AX] extends PreambleContributor[SO, SY, AX] /** Creates background definitions for n-tuples of predicate and wand arguments. Currently, * snapshot trees are used to built n-tuples. @@ -45,8 +44,7 @@ class DefaultPredicateAndWandSnapFunctionsContributor(preambleReader: PreambleRe termConverter: TermConverter[String, String, String], predicateSnapGenerator: PredicateSnapGenerator, config: Config) - extends PredicateSnapFunctionsContributor[Sort, String, String] - with MagicWandSnapFunctionsContributor[Sort, String, String] { + extends PredicateSnapFunctionsContributor[Sort, String, String] { /* PreambleBlock = Comment x Lines */ private type PreambleBlock = (String, Iterable[String]) diff --git a/src/main/scala/verifier/DefaultMainVerifier.scala b/src/main/scala/verifier/DefaultMainVerifier.scala index 61c4e31f5..a7d69656d 100644 --- a/src/main/scala/verifier/DefaultMainVerifier.scala +++ b/src/main/scala/verifier/DefaultMainVerifier.scala @@ -73,6 +73,7 @@ class DefaultMainVerifier(config: Config, protected val fieldValueFunctionsContributor = new DefaultFieldValueFunctionsContributor(preambleReader, symbolConverter, termConverter, config) protected val predSnapGenerator = new PredicateSnapGenerator(symbolConverter, snapshotSupporter) protected val predicateAndWandSnapFunctionsContributor = new DefaultPredicateAndWandSnapFunctionsContributor(preambleReader, termConverter, predSnapGenerator, config) + protected val magicWandSnapFunctionsContributor = new MagicWandSnapFunctionsContributor(preambleReader) private val _verificationPoolManager: VerificationPoolManager = new VerificationPoolManager(this) def verificationPoolManager: VerificationPoolManager = _verificationPoolManager @@ -82,6 +83,7 @@ class DefaultMainVerifier(config: Config, sequencesContributor, setsContributor, multisetsContributor, mapsContributor, domainsContributor, fieldValueFunctionsContributor, predSnapGenerator, predicateAndWandSnapFunctionsContributor, + magicWandSnapFunctionsContributor, functionsSupporter, predicateSupporter, _verificationPoolManager, MultiRunRecorders /* In lieu of a better place, include MultiRunRecorders singleton here */ @@ -459,6 +461,7 @@ class DefaultMainVerifier(config: Config, domainsContributor, fieldValueFunctionsContributor, predicateAndWandSnapFunctionsContributor, + magicWandSnapFunctionsContributor, functionsSupporter, predicateSupporter ) @@ -471,6 +474,7 @@ class DefaultMainVerifier(config: Config, domainsContributor, fieldValueFunctionsContributor, predicateAndWandSnapFunctionsContributor, + magicWandSnapFunctionsContributor, functionsSupporter, predicateSupporter ) @@ -483,6 +487,7 @@ class DefaultMainVerifier(config: Config, domainsContributor, fieldValueFunctionsContributor, predicateAndWandSnapFunctionsContributor, + magicWandSnapFunctionsContributor, functionsSupporter, predicateSupporter ) @@ -500,6 +505,7 @@ class DefaultMainVerifier(config: Config, domainsContributor, fieldValueFunctionsContributor, predicateAndWandSnapFunctionsContributor, + magicWandSnapFunctionsContributor, functionsSupporter, predicateSupporter ) @@ -512,6 +518,7 @@ class DefaultMainVerifier(config: Config, domainsContributor, fieldValueFunctionsContributor, predicateAndWandSnapFunctionsContributor, + magicWandSnapFunctionsContributor, functionsSupporter, predicateSupporter )