From fd87482c7f9af2d31f32add3ba77c221917640b7 Mon Sep 17 00:00:00 2001 From: Manuel Dublanc <19774382+manud99@users.noreply.github.com> Date: Mon, 6 May 2024 11:48:12 +0200 Subject: [PATCH] Second optimization: When there is no applying expression use the original approach using MagicWandSnapSingleton. --- .../decider/TermToSMTLib2Converter.scala | 3 +- .../scala/decider/TermToZ3APIConverter.scala | 2 + src/main/scala/rules/MagicWandSupporter.scala | 57 ++++++++----- src/main/scala/rules/Producer.scala | 31 ++++--- src/main/scala/state/Terms.scala | 84 ++++++++++++++++--- src/main/scala/state/Utils.scala | 3 +- 6 files changed, 136 insertions(+), 44 deletions(-) diff --git a/src/main/scala/decider/TermToSMTLib2Converter.scala b/src/main/scala/decider/TermToSMTLib2Converter.scala index c2c90f497..96c4e961b 100644 --- a/src/main/scala/decider/TermToSMTLib2Converter.scala +++ b/src/main/scala/decider/TermToSMTLib2Converter.scala @@ -316,7 +316,8 @@ 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(_, _, wandMap) => render(wandMap) + case snap: MagicWandSnapSingleton => renderBinaryOp("$Snap.combine", snap) + case MagicWandSnapFunction(_, _, wandMap) => render(wandMap) case MWSFLookup(mwsf, snap) => renderApp("MWSF_apply", Seq(mwsf, snap), sorts.Snap) case _: MagicWandChunkTerm diff --git a/src/main/scala/decider/TermToZ3APIConverter.scala b/src/main/scala/decider/TermToZ3APIConverter.scala index 3766ee49f..821784ab4 100644 --- a/src/main/scala/decider/TermToZ3APIConverter.scala +++ b/src/main/scala/decider/TermToZ3APIConverter.scala @@ -435,6 +435,8 @@ class TermToZ3APIConverter case bop: Combine => ctx.mkApp(combineConstructor, convertTerm(bop.p0), convertTerm(bop.p1)) + case MagicWandSnapSingleton(abstractLhs, rhsSnapshot) => + ctx.mkApp(combineConstructor, convertTerm(abstractLhs), convertTerm(rhsSnapshot)) case SortWrapper(t, to) => createApp(convertId(SortWrapperId(t.sort, to)), Seq(t), to) diff --git a/src/main/scala/rules/MagicWandSupporter.scala b/src/main/scala/rules/MagicWandSupporter.scala index 70ed60efc..3dc88ca5e 100644 --- a/src/main/scala/rules/MagicWandSupporter.scala +++ b/src/main/scala/rules/MagicWandSupporter.scala @@ -7,7 +7,7 @@ package viper.silicon.rules import viper.silver.ast -import viper.silver.ast.{Exp, Stmt} +import viper.silver.ast.{Applying, Exp, Program, Stmt} import viper.silver.cfg.Edge import viper.silver.cfg.silver.SilverCfg.SilverBlock import viper.silver.verifier.PartialVerificationError @@ -16,7 +16,7 @@ import viper.silicon.decider.RecordedPathConditions import viper.silicon.interfaces._ import viper.silicon.interfaces.state._ import viper.silicon.state._ -import viper.silicon.state.terms.{MagicWandSnapshot, _} +import viper.silicon.state.terms.{MagicWandSnapshot, MagicWandSnapSingleton, MagicWandSnapFunction, _} import viper.silicon.utils.{freshSnap, toSf} import viper.silicon.verifier.Verifier @@ -212,10 +212,6 @@ object magicWandSupporter extends SymbolicExecutionRules { 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 recordedBranches: Seq[(State, Stack[Term], Stack[Option[Exp]], Vector[Term], Chunk)] = Nil @@ -260,8 +256,13 @@ object magicWandSupporter extends SymbolicExecutionRules { val preMark = v3.decider.setPathConditionMark() v3.decider.prover.comment(s"Create WandMap for wand $wand") - val wandSnapshot = MagicWandSnapshot(freshSnapRoot, snapRhs, v3.decider.fresh("mwsf", sorts.MagicWandSnapFunction)) - v3.decider.assumeDefinition(wandSnapshot.definition) + val wandSnapshot: MagicWandSnapshot = if (useMWSF(s4.program)) { + val fct = MagicWandSnapFunction(freshSnapRoot, snapRhs, v3.decider.fresh("mwsf", sorts.MagicWandSnapFunction)) + v3.decider.assumeDefinition(fct.definition) + fct + } else { + MagicWandSnapSingleton(freshSnapRoot, snapRhs) + } // If the wand is part of a quantified expression if (s4.qpMagicWands.contains(MagicWandIdentifier(wand, s.program))) { @@ -285,16 +286,18 @@ object magicWandSupporter extends SymbolicExecutionRules { // Partition path conditions into a set which include the abstractLhs and those which do not val (pcsWithAbstractLhs, pcsWithoutAbstractLhs) = conservedPcs.flatMap(_.conditionalized).partition(pcs => pcs.contains(wandSnapshot.abstractLhs)) // For all path conditions which include the abstractLhs, add those as part of the definition of the wandMap in the same forall quantifier - val pcsQuantified = Forall( - wandSnapshot.abstractLhs, - And(pcsWithAbstractLhs.map { - // Remove redundant forall quantifiers with the same quantified variable - case Quantification(Forall, wandSnapshot.abstractLhs :: Nil, body: Term, _, _, _, _) => body - case p => p - }), - Trigger(MWSFLookup(wandSnapshot.wandMap, wandSnapshot.abstractLhs)), - ) - + val pcsQuantified = wandSnapshot match { + case _: MagicWandSnapSingleton => And(pcsWithAbstractLhs) + case wandSnapshot: MagicWandSnapFunction => Forall( + wandSnapshot.abstractLhs, + And(pcsWithAbstractLhs.map { + // Remove redundant forall quantifiers with the same quantified variable + case Quantification(Forall, wandSnapshot.abstractLhs :: Nil, body: Term, _, _, _, _) => body + case p => p + }), + Trigger(MWSFLookup(wandSnapshot.wandMap, wandSnapshot.abstractLhs)), + ) + } appendToResults(s5, ch, v4.decider.pcs.after(preMark), pcsQuantified +: pcsWithoutAbstractLhs, v4) Success() }) @@ -418,8 +421,11 @@ object magicWandSupporter extends SymbolicExecutionRules { // 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.applyToWandMap(snapLhs) - case SortWrapper(snapshot: MagicWandSnapshot, _) => snapshot.applyToWandMap(snapLhs) + case snapshot: MagicWandSnapSingleton => + v2.decider.assume(snapLhs === snapshot.abstractLhs) + snapshot.rhsSnapshot + case snapshot: MagicWandSnapFunction => snapshot.applyToWandMap(snapLhs) + case SortWrapper(snapshot: MagicWandSnapFunction, _) => snapshot.applyToWandMap(snapLhs) // Fallback solution for quantified magic wands case predicateLookup: PredicateLookup => v2.decider.assume(snapLhs === First(snapWand)) @@ -524,4 +530,15 @@ object magicWandSupporter extends SymbolicExecutionRules { s.reserveCfgs.head.outEdges(b) else s.methodCfg.outEdges(b) + + /** + * Determine, whether to use MWSF or MagicWandSnapshot. + * MWSF have the advantage over MagicWandSnapshot that they can be applied multiple times. + * However, they are slower than MagicWandSnapshots. + * + * @param program AST program which is verified. + * @return Boolean indicating whether to use MWSF instead of MagicWandSnapshot. + */ + def useMWSF(program: Program): Boolean = + program.existsDefined { case Applying(_, _) => true } } diff --git a/src/main/scala/rules/Producer.scala b/src/main/scala/rules/Producer.scala index 16cef52aa..9acca8877 100644 --- a/src/main/scala/rules/Producer.scala +++ b/src/main/scala/rules/Producer.scala @@ -397,18 +397,25 @@ object producer extends ProductionRules { Q(s2, v1)}) case wand: ast.MagicWand => - val snapRhs = sf(sorts.MagicWandSnapFunction, v) - - // Create Map that takes a snapshot, which represent the values of the consumed LHS of the wand, - // and relates it to the snapshot of the RHS. We use this to preserve values of the LHS in the RHS snapshot. - v.decider.prover.comment(s"Produce new magic wand snapshot map for wand $wand") - val abstractLhs = v.decider.fresh(sorts.Snap) - val wandMap = v.decider.fresh("$mwsf", sorts.MagicWandSnapFunction) - val magicWandSnapshot = MagicWandSnapshot(abstractLhs, MWSFLookup(snapRhs, abstractLhs), wandMap) - - // We assume that the wandMap that we get from `snapRhs`, which potentially is nested in a binary tree, - // is the same as our newly created wandMap. - v.decider.assumeDefinition(magicWandSnapshot.definition) + val magicWandSnapshot: MagicWandSnapshot = if (magicWandSupporter.useMWSF(s.program)) { + val snapRhs = sf(sorts.MagicWandSnapFunction, v) + + // Create Map that takes a snapshot, which represent the values of the consumed LHS of the wand, + // and relates it to the snapshot of the RHS. We use this to preserve values of the LHS in the RHS snapshot. + v.decider.prover.comment(s"Produce new magic wand snapshot map for wand $wand") + val abstractLhs = v.decider.fresh(sorts.Snap) + val wandMap = v.decider.fresh("$mwsf", sorts.MagicWandSnapFunction) + val snapFunction = MagicWandSnapFunction(abstractLhs, MWSFLookup(snapRhs, abstractLhs), wandMap) + + // We assume that the wandMap that we get from `snapRhs`, which potentially is nested in a binary tree, + // is the same as our newly created wandMap. + v.decider.assumeDefinition(snapFunction.definition) + snapFunction + + } else { + val snap = sf(sorts.Snap, v) + MagicWandSnapSingleton(snap) + } magicWandSupporter.createChunk(s, wand, magicWandSnapshot, pve, v)((s1, chWand, v1) => chunkSupporter.produce(s1, s1.h, chWand, v1)((s2, h2, v2) => diff --git a/src/main/scala/state/Terms.scala b/src/main/scala/state/Terms.scala index 3d858a711..811fa4b46 100644 --- a/src/main/scala/state/Terms.scala +++ b/src/main/scala/state/Terms.scala @@ -2300,6 +2300,68 @@ object PredicateTrigger extends PreciseCondFlyweightFactory[(String, Term, Seq[T /* Magic wands */ +abstract class MagicWandSnapshot(val abstractLhs: Term, val rhsSnapshot: Term) extends Term { + utils.assertSort(abstractLhs, "abstract lhs", sorts.Snap) + utils.assertSort(rhsSnapshot, "rhs snapshot", sorts.Snap) +} + +/** + * Snapshot for a magic wand. It represents a function which can be used only once + * by equating a snapshot from consuming the wand's LHS with `abstractLhs`. + * + * For a snapshot which can be applied multiple times see [[MagicWandSnapFunction]]. + * + * @param abstractLhs The abstract snapshot which acts as a placeholder in the + * `rhsSnapshot` for the values when applying the magic wand. + * @param rhsSnapshot Snapshot which can be used when producing the wand's RHS. + */ +class MagicWandSnapSingleton(override val abstractLhs: Term, override val rhsSnapshot: Term) + extends MagicWandSnapshot(abstractLhs, rhsSnapshot) + with ConditionalFlyweightBinaryOp[MagicWandSnapSingleton] { + + override lazy val toString: String = s"wandSnap(lhs = $abstractLhs, rhs = $rhsSnapshot)" + + /* ConditionalFlyweightBinaryOp members */ + + override def sort: Sort = sorts.Snap + + override def p0: Term = abstractLhs + + override def p1: Term = rhsSnapshot +} + +object MagicWandSnapSingleton { + var pool = new TrieMap[(Term, Term), MagicWandSnapSingleton]() + + /** Craete a new [[MagicWandSnapSingleton]] from a single snapshot term. */ + def apply(snapshot: Term): MagicWandSnapshot = { + assert(snapshot.sort == sorts.Snap, s"MagicWandSnapshot.apply expects sorts Snap but got ${snapshot.sort}") + + snapshot match { + case snap: MagicWandSnapSingleton => snap + case _ => MagicWandSnapSingleton(First(snapshot), Second(snapshot)) + } + } + + /** Create a new [[MagicWandSnapSingleton]] from two snapshot terms. */ + def apply(abstractLhs: Term, rhsSnapshot: Term): MagicWandSnapSingleton = + createIfNonExistent((abstractLhs, rhsSnapshot)) + + /** Destruct a [[MagicWandSnapSingleton]] instance. Used in [[viper.silicon.state.utils.transform]] */ + def unapply(mws: MagicWandSnapSingleton): Some[(Term, Term)] = + Some((mws.abstractLhs, mws.rhsSnapshot)) + + private def createIfNonExistent(args: (Term, Term)): MagicWandSnapSingleton = { + if (Verifier.config.useFlyweight) { + pool.getOrElseUpdate(args, actualCreate(args)) + } else { + actualCreate(args) + } + } + + private def actualCreate(tuple: (Term, Term)) = new MagicWandSnapSingleton(tuple._1, tuple._2) +} + /** * Represents a snapshot of a magic wand, which is a map from Snap to Snap. * @@ -2310,7 +2372,10 @@ object PredicateTrigger extends PreciseCondFlyweightFactory[(String, Term, Seq[T * In the symbolic execution this represents a function that when we apply a magic wand * it consumes the left-hand side and uses the resulting snapshot to look up which right-hand side should be produced. */ -class MagicWandSnapshot(val abstractLhs: Var, val rhsSnapshot: Term, val wandMap: Term) extends Term with ConditionalFlyweight[Term, MagicWandSnapshot] { +class MagicWandSnapFunction(override val abstractLhs: Var, override val rhsSnapshot: Term, val wandMap: Term) + extends MagicWandSnapshot(abstractLhs, rhsSnapshot) + with ConditionalFlyweight[Term, MagicWandSnapFunction] { + utils.assertSort(abstractLhs, "abstract lhs", sorts.Snap) utils.assertSort(rhsSnapshot, "rhs snapshot", sorts.Snap) utils.assertSort(wandMap, "wand map", sorts.MagicWandSnapFunction) @@ -2342,15 +2407,14 @@ class MagicWandSnapshot(val abstractLhs: Var, val rhsSnapshot: Term, val wandMap def applyToWandMap(snapLhs: Term): Term = MWSFLookup(wandMap, snapLhs) } -object MagicWandSnapshot { - /** - * Create a new instance of `MagicWandSnapshot`. - * - * @see [[viper.silicon.state.terms.MagicWandSnapshot]] - */ - def apply(abstractLhs: Var, rhsSnapshot: Term, wandMap: Term): MagicWandSnapshot = new MagicWandSnapshot(abstractLhs, rhsSnapshot, wandMap) +object MagicWandSnapFunction { + /** Create a new instance of [[viper.silicon.state.terms.MagicWandSnapFunction]]. */ + def apply(abstractLhs: Var, rhsSnapshot: Term, wandMap: Term): MagicWandSnapFunction = + new MagicWandSnapFunction(abstractLhs, rhsSnapshot, wandMap) - def unapply(snap: MagicWandSnapshot): Option[(Var, Term, Term)] = Some(snap.abstractLhs, snap.rhsSnapshot, snap.wandMap) + /** Destructs an instance of [[viper.silicon.state.terms.MagicWandSnapFunction]]. */ + def unapply(snap: MagicWandSnapFunction): Option[(Var, Term, Term)] = + Some(snap.abstractLhs, snap.rhsSnapshot, snap.wandMap) } class MWSFLookup(val mwsf: Term, val snap: Term) extends Term with ConditionalFlyweightBinaryOp[MWSFLookup] { @@ -2361,7 +2425,7 @@ class MWSFLookup(val mwsf: Term, val snap: Term) extends Term with ConditionalFl } object MWSFLookup extends PreciseCondFlyweightFactory[(Term, Term), MWSFLookup] { - override def apply(pair: (Term, Term)) = { + override def apply(pair: (Term, Term)): MWSFLookup = { val (mwsf, snap) = pair utils.assertSort(mwsf, "mwsf", sorts.MagicWandSnapFunction) utils.assertSort(snap, "snap", sorts.Snap) diff --git a/src/main/scala/state/Utils.scala b/src/main/scala/state/Utils.scala index e37aea1fd..5f01ec793 100644 --- a/src/main/scala/state/Utils.scala +++ b/src/main/scala/state/Utils.scala @@ -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(t0, t1, t2) => MagicWandSnapshot(go(t0), go(t1), go(t2)) + case MagicWandSnapSingleton(t0, t1) => MagicWandSnapSingleton(go(t0), go(t1)) + case MagicWandSnapFunction(t0, t1, t2) => MagicWandSnapFunction(go(t0), go(t1), go(t2)) case MWSFLookup(t0, t1) => MWSFLookup(go(t0), go(t1)) case Combine(t0, t1) => Combine(go(t0), go(t1)) case First(t) => First(go(t))