diff --git a/silver b/silver index 42fa22f0c..40a00dd9a 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 42fa22f0c31923b0f304039805328288c45979d3 +Subproject commit 40a00dd9a3b622527a40b8c960dd7743b6dee535 diff --git a/src/main/scala/rules/Brancher.scala b/src/main/scala/rules/Brancher.scala index 3c1cf3240..0f4fe4b85 100644 --- a/src/main/scala/rules/Brancher.scala +++ b/src/main/scala/rules/Brancher.scala @@ -50,10 +50,11 @@ object brancher extends BranchingRules { * (1) the branching is due to the short-circuiting evaluation of a conjunction * (2) the branch condition contains a quantified variable */ + val allQuantifiedVariables = s.quantifiedVariables ++ s.packagingWandSnapshots val skipPathFeasibilityCheck = ( fromShortCircuitingAnd - || ( s.quantifiedVariables.nonEmpty - && s.quantifiedVariables.map(_._1).exists(condition.freeVariables.contains)) + || ( allQuantifiedVariables.nonEmpty + && allQuantifiedVariables.map(_._1).exists(condition.freeVariables.contains)) ) /* True if the then-branch is to be explored */ diff --git a/src/main/scala/rules/Executor.scala b/src/main/scala/rules/Executor.scala index 763ac1afa..57714bfec 100644 --- a/src/main/scala/rules/Executor.scala +++ b/src/main/scala/rules/Executor.scala @@ -597,11 +597,7 @@ object executor extends ExecutionRules { } assert(s2.reserveHeaps.length == s.reserveHeaps.length) - val s3 = chWand match { - case ch: QuantifiedMagicWandChunk => - v1.heapSupporter.triggerResourceIfNeeded(s2, wand, ch.singletonArgs.get, ch.singletonArgExps, v1) - case _ => s2 - } + val s3 = v1.heapSupporter.triggerWandIfNeeded(s2, wand, chWand, v1) continuation(s3.copy(isInPackage = s.isInPackage), v1) }) diff --git a/src/main/scala/rules/HeapSupporter.scala b/src/main/scala/rules/HeapSupporter.scala index 649c1c629..7888d755d 100644 --- a/src/main/scala/rules/HeapSupporter.scala +++ b/src/main/scala/rules/HeapSupporter.scala @@ -10,7 +10,7 @@ import viper.silicon import viper.silicon.common.collections.immutable.InsertionOrderedSet import viper.silicon.debugger.DebugExp import viper.silicon.interfaces.VerificationResult -import viper.silicon.interfaces.state.{ChunkIdentifer, NonQuantifiedChunk} +import viper.silicon.interfaces.state.{Chunk, ChunkIdentifer, NonQuantifiedChunk} import viper.silicon.resources.{FieldID, PredicateID} import viper.silicon.rules.havocSupporter.{HavocHelperData, HavocOneData, HavocallData} import viper.silicon.rules.quantifiedChunkSupporter.freshSnapshotMap @@ -67,6 +67,18 @@ trait HeapSupportRules extends SymbolicExecutionRules { eArgs: Option[Seq[ast.Exp]], v: Verifier): State + /** Creates the chunk for a (quantified or non-quantified) magic wand with the given snapshot, + * returning the chunk plus any ground definitions that should be conserved separately. */ + def createWandChunk(s: State, + wand: ast.MagicWand, + tArgs: Seq[Term], + eArgs: Option[Seq[ast.Exp]], + snapshot: MagicWandSnapshot, + v: Verifier): (Chunk, Seq[Term], Option[Seq[DebugExp]]) + + /** Triggers the wand resource if the produced chunk is a quantified one; a no-op otherwise. */ + def triggerWandIfNeeded(s: State, wand: ast.MagicWand, chWand: Chunk, v: Verifier): State + def consumeSingle(s: State, h: Heap, resAcc: ast.ResourceAccess, @@ -438,6 +450,37 @@ class DefaultHeapSupportRules extends HeapSupportRules { } } + def createWandChunk(s: State, + wand: ast.MagicWand, + tArgs: Seq[Term], + eArgs: Option[Seq[ast.Exp]], + snapshot: MagicWandSnapshot, + v: Verifier): (Chunk, Seq[Term], Option[Seq[DebugExp]]) = { + if (s.isQuantifiedResource(wand)) { + val formalVars = s.getFormalArgVars(wand, v) + val formalVarExps = Option.when(withExp)(s.getFormalArgDecls(wand)) + // The singleton snapshot map maps the wand's arguments to its magic wand snap function. + val (sm, smValueDef) = quantifiedChunkSupporter.singletonSnapshotMap(s, wand, tArgs, snapshot.mwsf, v) + v.decider.prover.comment("Definitional axioms for singleton-SM's value") + val debugExp = Option.when(withExp)(DebugExp.createInstance("Definitional axioms for singleton-SM's value", true)) + v.decider.assumeDefinition(smValueDef, debugExp) + val chunk = quantifiedChunkSupporter.createSingletonQuantifiedChunk(formalVars, formalVarExps, wand, tArgs, + eArgs, FullPerm, Option.when(withExp)(ast.FullPerm()()), sm, s.program) + (chunk, Seq(smValueDef), Option.when(withExp)(Seq(debugExp.get))) + } else { + val chunk = MagicWandChunk(MagicWandIdentifier(wand, s.program), s.g.values, tArgs, eArgs, snapshot, FullPerm, + Option.when(withExp)(ast.FullPerm()(wand.pos, wand.info, wand.errT))) + (chunk, Seq.empty[Term], Option.when(withExp)(Seq.empty[DebugExp])) + } + } + + def triggerWandIfNeeded(s: State, wand: ast.MagicWand, chWand: Chunk, v: Verifier): State = + chWand match { + case ch: QuantifiedMagicWandChunk => + triggerResourceIfNeeded(s, wand, ch.singletonArgs.get, ch.singletonArgExps, v) + case _ => s + } + def produceSingle(s: State, resource: ast.Resource, tArgs: Seq[Term], @@ -545,7 +588,7 @@ class DefaultHeapSupportRules extends HeapSupportRules { case p: ast.Predicate => sf(sorts.PredicateSnapFunction(s.predicateSnapMap(p.name), p.name), v) case _: ast.MagicWand => - sf(sorts.PredicateSnapFunction(sorts.Snap, qid), v) + sf(sorts.PredicateSnapFunction(sorts.MagicWandSnapFunction, qid), v) } quantifiedChunkSupporter.produce( diff --git a/src/main/scala/rules/MagicWandSupporter.scala b/src/main/scala/rules/MagicWandSupporter.scala index c5fc50dbd..a1930c4fe 100644 --- a/src/main/scala/rules/MagicWandSupporter.scala +++ b/src/main/scala/rules/MagicWandSupporter.scala @@ -176,7 +176,7 @@ object magicWandSupporter extends SymbolicExecutionRules { * and thus be unsound. Since fractional wands do not exist it is not necessary to equate their * snapshots. Also have a look at the comments in the packageWand and applyWand methods. */ - case (Some(_: MagicWandChunk), Some(_: MagicWandChunk)) => True + case (Some(_: MagicWandChunk | _: QuantifiedMagicWandChunk), Some(_: MagicWandChunk | _: QuantifiedMagicWandChunk)) => True case (Some(ch1: NonQuantifiedChunk), Some(ch2: NonQuantifiedChunk)) => ch1.snap === ch2.snap case (Some(ch1: QuantifiedBasicChunk), Some(ch2: QuantifiedBasicChunk)) => ch1.snapshotMap === ch2.snapshotMap case _ => True @@ -314,41 +314,30 @@ object magicWandSupporter extends SymbolicExecutionRules { val bodyVars = wand.subexpressionsToEvaluate(s.program) evals(s, bodyVars, _ => pve, v)((s2, tArgs, eArgsNew, v2) => { - // Currently, the snapshot of a wand differs depending on whether it is a quantified magic wand or not. - // Therefore, we have to keep the case distinction here and cannot leave everything but the chunk creation - // to the HeapSupporter. - val (s3, ch, tPcs, ePcs, v3 ) = if (s2.qpMagicWands.contains(MagicWandIdentifier(wand, s2.program))) { - val formalVars = bodyVars.indices.toList.map(i => Var(Identifier(s"x$i"), v.symbolConverter.toSort(bodyVars(i).typ), false)) - val formalVarExps = Option.when(withExp)(bodyVars.indices.toList.map(i => ast.LocalVarDecl(s"x$i", bodyVars(i).typ)())) - val snapshotTerm = Combine(freshSnapRoot, snapRhs) - val (sm, smValueDef) = quantifiedChunkSupporter.singletonSnapshotMap(s2, wand, tArgs, snapshotTerm, v2) - v2.decider.prover.comment("Definitional axioms for singleton-SM's value") - val debugExp = Option.when(withExp)(DebugExp.createInstance("Definitional axioms for singleton-SM's value", true)) - v2.decider.assumeDefinition(smValueDef, debugExp) - val ch = quantifiedChunkSupporter.createSingletonQuantifiedChunk(formalVars, formalVarExps, wand, tArgs, - eArgsNew, FullPerm, Option.when(withExp)(ast.FullPerm()()), sm, s.program) - val conservedPcs = s2.conservedPcs.head :+ v2.decider.pcs.after(preMark).definitionsOnly - (s2, ch, conservedPcs.flatMap(_.conditionalized), Option.when(withExp)(conservedPcs.flatMap(_.conditionalizedExp)), v2) - } else { - val ch = MagicWandChunk(MagicWandIdentifier(wand, s.program), s2.g.values, tArgs, eArgsNew, wandSnapshot, FullPerm, - Option.when(withExp)(ast.FullPerm()(wand.pos, wand.info, wand.errT))) - val conservedPcs = s2.conservedPcs.head :+ v2.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(pcs => pcs.conditionalized).partition(_.contains(freshSnapRoot)) - val pcsWithoutExp = Option.when(withExp)(filterDebugExpsWithoutSnapshot(conservedPcs.flatMap(pcs => pcs.conditionalizedExp), 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)), - ) - (s2, ch, pcsQuantified +: pcsWithoutFreshSnapRoot, Option.when(withExp)(DebugExp.createInstance("MWSF definition path conditions", pcsQuantified, true) +: pcsWithoutExp.get), v2) - } - appendToResults(s3, ch, v3.decider.pcs.after(preMark), (tPcs, ePcs), v3) + // Partition the conserved PCs here, before any definitions about the new wand chunks are assumed below, so that + // the ground value def is not bundled into (and trapped inside) the freshSnapRoot quantifier. + val conservedPcs = s2.conservedPcs.head :+ v2.decider.pcs.after(preMark).definitionsOnly + + val (pcsWithFreshSnapRoot, pcsWithoutFreshSnapRoot) = conservedPcs.flatMap(pcs => pcs.conditionalized).partition(_.contains(freshSnapRoot)) + val pcsWithoutExp = Option.when(withExp)(filterDebugExpsWithoutSnapshot(conservedPcs.flatMap(pcs => pcs.conditionalizedExp), 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)), + ) + + val (ch, groundPcs, groundPcsExp) = v2.heapSupporter.createWandChunk(s2, wand, tArgs, eArgsNew, wandSnapshot, v2) + + val tPcs = (pcsQuantified +: pcsWithoutFreshSnapRoot) ++ groundPcs + val ePcs = Option.when(withExp)(DebugExp.createInstance("MWSF definition path conditions", pcsQuantified, true) +: (pcsWithoutExp.get ++ groundPcsExp.get)) + + val s3 = s2.copy(packagingWandSnapshots = s2.packagingWandSnapshots.filterNot(_._1 == freshSnapRoot)) + appendToResults(s3, ch, v2.decider.pcs.after(preMark), (tPcs, ePcs), v2) Success() }) } @@ -362,8 +351,13 @@ object magicWandSupporter extends SymbolicExecutionRules { */ val freshSnapRoot = freshSnap(sorts.Snap, v1) + // Record the abstract LHS snapshot so that new declarations created while packaging are parameterized by it + // (see State.packagingWandSnapshots); each apply of the resulting wand then gets its own LHS snapshot. + val freshSnapshotRootVar = Option.when(withExp)(ast.LocalVar("LHS", ast.InternalType)()) + val s1WithSnapRoot = s1.copy(packagingWandSnapshots = (freshSnapRoot, freshSnapshotRootVar) +: s1.packagingWandSnapshots) + // Produce the wand's LHS. - produce(s1.copy(conservingSnapshotGeneration = true), toSf(freshSnapRoot), wand.left, pve, v1)((sLhs, v2) => { + produce(s1WithSnapRoot.copy(conservingSnapshotGeneration = true), toSf(freshSnapRoot), wand.left, pve, v1)((sLhs, v2) => { val proofScriptCfg = proofScript.toCfg() val emptyHeap = v2.heapSupporter.getEmptyHeap(sLhs.program) @@ -472,14 +466,12 @@ object magicWandSupporter extends SymbolicExecutionRules { // 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. + // Look up the RHS snapshot by applying snapLhs to the wand's MWSF (a (wrapped) + // MagicWandSnapshot for an individual wand, or an MWSF-sorted lookup for a quantified one). val magicWandSnapshotLookup = snapWand.get match { case snapshot: MagicWandSnapshot => snapshot.applyToMWSF(snapLhs.get) case SortWrapper(snapshot: MagicWandSnapshot, _) => snapshot.applyToMWSF(snapLhs.get) - // Fallback solution for quantified magic wands - case predicateLookup: PredicateLookup => - v2.decider.assume(snapLhs.get === First(snapWand.get), Option.when(withExp)(DebugExp.createInstance("Magic wand snapshot", true))) - Second(predicateLookup) + case t if t.sort == sorts.MagicWandSnapFunction => MWSFLookup(t, snapLhs.get) case _ => snapWand.get } diff --git a/src/main/scala/rules/MoreCompleteExhaleSupporter.scala b/src/main/scala/rules/MoreCompleteExhaleSupporter.scala index 1aa582efd..a31a3f6f3 100644 --- a/src/main/scala/rules/MoreCompleteExhaleSupporter.scala +++ b/src/main/scala/rules/MoreCompleteExhaleSupporter.scala @@ -130,7 +130,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { case Some(v) => ReusedSummarisingSnapshot(v) case None => - val ss = v.decider.appliedFresh("ss", sort, s.functionRecorderQuantifiedVariables().map(_._1) ++ s.quantifiedVariables.map(_._1)) + val ss = v.decider.appliedFresh("ss", sort, s.functionRecorderQuantifiedVariables().map(_._1) ++ s.packagingWandSnapshots.map(_._1) ++ s.quantifiedVariables.map(_._1)) FreshSummarisingSnapshot(ss) } } @@ -327,7 +327,8 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { definiteAlias.contains(ch1) || !definiteAlias.contains(ch2) && ch1.args == args } - val additionalArgs = s.relevantQuantifiedVariables.map(_._1) + // Permission maps deliberately exclude packagingWandSnapshots (would break permission matching after a package). + val additionalArgs = (s.functionRecorderQuantifiedVariables() ++ s.quantifiedVariables).map(_._1) var currentFunctionRecorder = s.functionRecorder relevantChunks.sortWith(sortFunction) foreach { ch => diff --git a/src/main/scala/rules/QuantifiedChunkSupport.scala b/src/main/scala/rules/QuantifiedChunkSupport.scala index b1a12e07e..6d20c6909 100644 --- a/src/main/scala/rules/QuantifiedChunkSupport.scala +++ b/src/main/scala/rules/QuantifiedChunkSupport.scala @@ -501,7 +501,8 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { // TODO: Consider if axioms can be simplified in case codomainQVars is empty val snapshotMaps = relevantChunks.map(_.snapshotMap) - val relevantQvars = s.quantifiedVariables.map(_._1).filter(qvar => + // packagingWandSnapshots are always relevant; regular quantified variables only if they occur. + val relevantQvars = s.packagingWandSnapshots.map(_._1) ++ s.quantifiedVariables.map(_._1).filter(qvar => snapshotMaps.exists(sm => sm.contains(qvar)) || optSmDomainDefinitionCondition.exists(_.contains(qvar))) val additionalFvfArgs = s.functionRecorderQuantifiedVariables().map(_._1) ++ relevantQvars val sm = freshSnapshotMap(s, resource, additionalFvfArgs, v) @@ -668,7 +669,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { v: Verifier) : (Term, Term) = { - val additionalSmArgs = s.relevantQuantifiedVariables(arguments).map(_._1) + val additionalSmArgs = s.packagingWandSnapshots.map(_._1) ++ s.relevantQuantifiedVariables(arguments).map(_._1) val sm = freshSnapshotMap(s, resource, additionalSmArgs, v) val smValueDef = BuiltinEquals(ResourceLookup(resource, sm, arguments, s.program), value) @@ -1421,7 +1422,9 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { })((s4, optCh, v2) => optCh match { case Some(ch) if returnSnap => - val snap = ResourceLookup(resource, ch.snapshotMap, arguments, s4.program).convert(sorts.Snap) + val lookup = ResourceLookup(resource, ch.snapshotMap, arguments, s4.program) + // For magic wands the lookup is already the MWSF (applied directly by applyWand). + val snap = if (resource.isInstanceOf[ast.MagicWand]) lookup else lookup.convert(sorts.Snap) Q(s4, s4.h, Some(snap), v2) case None if returnSnap => Q(s4, s4.h, Some(freshSnap(sorts.Snap, v2)), v2) @@ -1461,7 +1464,9 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { v = v) val s2 = s1.copy(functionRecorder = s1.functionRecorder.recordFvfAndDomain(smDef1), smCache = smCache1) - val snap = ResourceLookup(resource, smDef1.sm, arguments, s2.program).convert(sorts.Snap) + val lookup = ResourceLookup(resource, smDef1.sm, arguments, s2.program) + // For magic wands the lookup is already the MWSF (applied directly by applyWand). + val snap = if (resource.isInstanceOf[ast.MagicWand]) lookup else lookup.convert(sorts.Snap) Q(s2, h1, Some(snap), v) } else { Q(s1, h1, None, v) @@ -1551,7 +1556,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { v.decider.prover.comment("Precomputing data for removing quantified permissions") - val additionalArgs = s.relevantQuantifiedVariables.map(_._1) + val additionalArgs = (s.packagingWandSnapshots ++ s.functionRecorderQuantifiedVariables() ++ s.quantifiedVariables).map(_._1) var currentFunctionRecorder = s.functionRecorder val precomputedData = candidates map { ch => @@ -1743,7 +1748,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { // TODO: Reconsider use of and general design behind s.predicateSnapMap sorts.PredicateSnapFunction(s.predicateSnapMap(predicate.name), predicate.name) case w: ast.MagicWand => - sorts.PredicateSnapFunction(sorts.Snap, MagicWandIdentifier(w, s.program).toString) + sorts.PredicateSnapFunction(sorts.MagicWandSnapFunction, MagicWandIdentifier(w, s.program).toString) case _ => sys.error(s"Found yet unsupported resource $resource (${resource.getClass.getSimpleName})") } diff --git a/src/main/scala/state/Chunks.scala b/src/main/scala/state/Chunks.scala index a4942f237..0738e7693 100644 --- a/src/main/scala/state/Chunks.scala +++ b/src/main/scala/state/Chunks.scala @@ -199,7 +199,7 @@ case class QuantifiedMagicWandChunk(id: MagicWandIdentifier, hints: Seq[Term] = Nil) extends QuantifiedBasicChunk { - require(wsf.sort.isInstanceOf[terms.sorts.PredicateSnapFunction] && wsf.sort.asInstanceOf[terms.sorts.PredicateSnapFunction].codomainSort == sorts.Snap, s"Quantified magic wand chunk values must be of sort MagicWandSnapFunction ($wsf), but found ${wsf.sort}") + require(wsf.sort.isInstanceOf[terms.sorts.PredicateSnapFunction] && wsf.sort.asInstanceOf[terms.sorts.PredicateSnapFunction].codomainSort == sorts.MagicWandSnapFunction, s"Quantified magic wand chunk values must be a PredicateSnapFunction with codomain MagicWandSnapFunction ($wsf), but found ${wsf.sort}") require(perm.sort == sorts.Perm, s"Permissions $perm must be of sort Perm, but found ${perm.sort}") override val resourceID = MagicWandID diff --git a/src/main/scala/state/State.scala b/src/main/scala/state/State.scala index 22043c79a..a22619e53 100644 --- a/src/main/scala/state/State.scala +++ b/src/main/scala/state/State.scala @@ -44,6 +44,7 @@ final case class State(g: Store = Store(), constrainableARPs: InsertionOrderedSet[Var] = InsertionOrderedSet.empty, quantifiedVariables: Stack[(Var, Option[ast.AbstractLocalVar])] = Nil, + packagingWandSnapshots: Stack[(Var, Option[ast.AbstractLocalVar])] = Nil, retrying: Boolean = false, underJoin: Boolean = false, functionRecorder: FunctionRecorder = NoopFunctionRecorder, @@ -170,7 +171,7 @@ final case class State(g: Store = Store(), functionRecorder.arguments.fold(Seq.empty[(Var, Option[ast.AbstractLocalVar])])(d => d) def relevantQuantifiedVariables(filterPredicate: Var => Boolean): Seq[(Var, Option[ast.AbstractLocalVar])] = ( - functionRecorderQuantifiedVariables() + functionRecorderQuantifiedVariables() ++ packagingWandSnapshots.filter(x => filterPredicate(x._1)) ++ quantifiedVariables.filter(x => filterPredicate(x._1)) ) @@ -183,8 +184,9 @@ final case class State(g: Store = Store(), Sanitizer.replaceFreeVariablesInExpression(e, varMapping.map(vm => vm._1 -> vm._2.get), Set()) } + // Unlike the filtered overload (used for inverse functions), this also includes packagingWandSnapshots. lazy val relevantQuantifiedVariables: Seq[(Var, Option[ast.AbstractLocalVar])] = - relevantQuantifiedVariables(_ => true) + functionRecorderQuantifiedVariables() ++ packagingWandSnapshots ++ quantifiedVariables override val toString = s"${this.getClass.getSimpleName}(...)" } @@ -205,6 +207,7 @@ object State { methodCfg1, invariantContexts1, constrainableARPs1, quantifiedVariables1, + packagingWandSnapshots1, retrying1, underJoin1, functionRecorder1, @@ -230,6 +233,7 @@ object State { `methodCfg1`, `invariantContexts1`, constrainableARPs2, quantifiedVariables2, + packagingWandSnapshots2, `retrying1`, `underJoin1`, functionRecorder2, @@ -250,6 +254,7 @@ object State { val possibleTriggers3 = possibleTriggers1 ++ possibleTriggers2 val constrainableARPs3 = constrainableARPs1 ++ constrainableARPs2 val quantifiedVariables3 = (quantifiedVariables1 ++ quantifiedVariables2).distinct + val packagingWandSnapshots3 = (packagingWandSnapshots1 ++ packagingWandSnapshots2).distinct val smCache3 = smCache1.union(smCache2) val pmCache3 = pmCache1 ++ pmCache2 @@ -268,6 +273,7 @@ object State { triggerExp = triggerExp3, constrainableARPs = constrainableARPs3, quantifiedVariables = quantifiedVariables3, + packagingWandSnapshots = packagingWandSnapshots3, ssCache = ssCache3, smCache = smCache3, pmCache = pmCache3, @@ -363,6 +369,7 @@ object State { methodCfg1, invariantContexts1, constrainableARPs1, quantifiedVariables1, + packagingWandSnapshots1, retrying1, underJoin1, functionRecorder1, @@ -387,6 +394,7 @@ object State { `methodCfg1`, invariantContexts2, constrainableARPs2, `quantifiedVariables1`, + `packagingWandSnapshots1`, `retrying1`, `underJoin1`, functionRecorder2, diff --git a/src/main/scala/supporters/SnapshotSupporter.scala b/src/main/scala/supporters/SnapshotSupporter.scala index 8f3f6efa8..931340dd9 100644 --- a/src/main/scala/supporters/SnapshotSupporter.scala +++ b/src/main/scala/supporters/SnapshotSupporter.scala @@ -8,7 +8,7 @@ package viper.silicon.supporters import viper.silicon.debugger.DebugExp import viper.silicon.state.terms.{Combine, First, Second, Sort, Term, Unit, sorts} -import viper.silicon.state.{MagicWandIdentifier, State, SymbolConverter} +import viper.silicon.state.{State, SymbolConverter} import viper.silicon.utils.toSf import viper.silicon.verifier.Verifier import viper.silver.ast @@ -40,8 +40,6 @@ class DefaultSnapshotSupporter(symbolConverter: SymbolConverter) extends Snapsho case p: ast.Predicate => p.body.map(v.snapshotSupporter.optimalSnapshotSort(_, s.program)._1) .getOrElse(sorts.Snap) - case mw: ast.MagicWand if s.qpMagicWands.contains(MagicWandIdentifier(mw, s.program)) => - sorts.Snap case _: ast.MagicWand => sorts.MagicWandSnapFunction } diff --git a/src/main/scala/supporters/qps/PredicateAndWandSnapFunctionsContributor.scala b/src/main/scala/supporters/qps/PredicateAndWandSnapFunctionsContributor.scala index 3da5802d1..4761fb988 100644 --- a/src/main/scala/supporters/qps/PredicateAndWandSnapFunctionsContributor.scala +++ b/src/main/scala/supporters/qps/PredicateAndWandSnapFunctionsContributor.scala @@ -97,7 +97,7 @@ class DefaultPredicateAndWandSnapFunctionsContributor(preambleReader: PreambleRe // WARNING: DefaultSetsContributor contributes a sort that is due to QPs over predicates and wands collectedSorts = collectedPredicates.map(predicate => - sorts.PredicateSnapFunction(predicateSnapGenerator.getSnap(predicate)._1, predicate.name)) ++ collectedWandIdentifiers.map(identifier => sorts.PredicateSnapFunction(sorts.Snap, identifier.toString)) + sorts.PredicateSnapFunction(predicateSnapGenerator.getSnap(predicate)._1, predicate.name)) ++ collectedWandIdentifiers.map(identifier => sorts.PredicateSnapFunction(sorts.MagicWandSnapFunction, identifier.toString)) collectedFunctionDecls = generateFunctionDecls @@ -129,7 +129,7 @@ class DefaultPredicateAndWandSnapFunctionsContributor(preambleReader: PreambleRe val wandsPreamble = collectedWandIdentifiers map (wandIdentifier => { - val snapSort = sorts.Snap + val snapSort = sorts.MagicWandSnapFunction val id = wandIdentifier.toString val substitutions = Map("$PRD$" -> id, "$S$" -> termConverter.convert(snapSort)) val declarations = preambleReader.readParametricPreamble(snapsTemplateFile, substitutions) @@ -157,7 +157,7 @@ class DefaultPredicateAndWandSnapFunctionsContributor(preambleReader: PreambleRe val wandsPreamble = collectedWandIdentifiers map (wandIdentifier => { - val sort = sorts.Snap // predicateSnapGenerator.getSnap(wandIdentifier)._1 + val sort = sorts.MagicWandSnapFunction // predicateSnapGenerator.getSnap(wandIdentifier)._1 val id = wandIdentifier.toString val substitutions = Map("$PRD$" -> id, "$S$" -> termConverter.convert(sort)) val declarations = preambleReader.readParametricPreamble(templateFile, substitutions)