Second optimization: When there is no applying expression use the original approach using MagicWandSnapSingleton.

Author: manud99

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

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)

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 }
 }

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) =>

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)

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))