diff --git a/src/main/scala/interfaces/state/Chunks.scala b/src/main/scala/interfaces/state/Chunks.scala index e556b4a4..32975024 100644 --- a/src/main/scala/interfaces/state/Chunks.scala +++ b/src/main/scala/interfaces/state/Chunks.scala @@ -18,16 +18,21 @@ trait GeneralChunk extends Chunk { val resourceID: ResourceID val id: ChunkIdentifer val perm: Term - val permExp: Option[ast.Exp] + def applyCondition(newCond: Term, newCondExp: Option[ast.Exp]): GeneralChunk + def permMinus(perm: Term, permExp: Option[ast.Exp]): GeneralChunk + def permPlus(perm: Term, permExp: Option[ast.Exp]): GeneralChunk - def withPerm(perm: Term, permExp: Option[ast.Exp]): GeneralChunk + val permExp: Option[ast.Exp] } trait NonQuantifiedChunk extends GeneralChunk { val args: Seq[Term] val argsExp: Option[Seq[ast.Exp]] val snap: Term - override def withPerm(perm: Term, permExp: Option[ast.Exp]): NonQuantifiedChunk + override def applyCondition(newCond: Term, newCondExp: Option[ast.Exp]): NonQuantifiedChunk + override def permMinus(perm: Term, permExp: Option[ast.Exp]): NonQuantifiedChunk + override def permPlus(perm: Term, permExp: Option[ast.Exp]): NonQuantifiedChunk + def withPerm(perm: Term, permExp: Option[ast.Exp]): NonQuantifiedChunk def withSnap(snap: Term): NonQuantifiedChunk } @@ -37,6 +42,8 @@ trait QuantifiedChunk extends GeneralChunk { def snapshotMap: Term def valueAt(arguments: Seq[Term]): Term - override def withPerm(perm: Term, permExp: Option[ast.Exp]): QuantifiedChunk + override def applyCondition(newCond: Term, newCondExp: Option[ast.Exp]): QuantifiedChunk + override def permMinus(perm: Term, permExp: Option[ast.Exp]): QuantifiedChunk + override def permPlus(perm: Term, permExp: Option[ast.Exp]): QuantifiedChunk def withSnapshotMap(snap: Term): QuantifiedChunk } \ No newline at end of file diff --git a/src/main/scala/logger/records/data/SingleMergeRecord.scala b/src/main/scala/logger/records/data/SingleMergeRecord.scala index 7137aff5..aa8467dc 100644 --- a/src/main/scala/logger/records/data/SingleMergeRecord.scala +++ b/src/main/scala/logger/records/data/SingleMergeRecord.scala @@ -8,13 +8,13 @@ package viper.silicon.logger.records.data import viper.silicon.common.collections.immutable.InsertionOrderedSet import viper.silicon.decider.PathConditionStack -import viper.silicon.interfaces.state.NonQuantifiedChunk +import viper.silicon.interfaces.state.{Chunk, NonQuantifiedChunk} import viper.silicon.state._ import viper.silicon.state.terms.Term import viper.silver.ast -class SingleMergeRecord(val destChunks: Seq[NonQuantifiedChunk], - val newChunks: Seq[NonQuantifiedChunk], +class SingleMergeRecord(val destChunks: Seq[Chunk], + val newChunks: Seq[Chunk], p: PathConditionStack) extends DataRecord { val value: ast.Node = null val state: State = null diff --git a/src/main/scala/logger/writer/SymbExLogReportWriter.scala b/src/main/scala/logger/writer/SymbExLogReportWriter.scala index 8047dd45..4cae25a8 100644 --- a/src/main/scala/logger/writer/SymbExLogReportWriter.scala +++ b/src/main/scala/logger/writer/SymbExLogReportWriter.scala @@ -58,32 +58,32 @@ object SymbExLogReportWriter { "perm" -> TermWriter.toJSON(perm) ) - case QuantifiedFieldChunk(id, fvf, perm, _, invs, cond, receiver, _, hints) => + case QuantifiedFieldChunk(id, fvf, condition, _, perm, _, invs, receiver, _, hints) => JsObject( "type" -> JsString("quantified_field_chunk"), "field" -> JsString(id.toString), "field_value_function" -> TermWriter.toJSON(fvf), + "condition" -> TermWriter.toJSON(condition), "perm" -> TermWriter.toJSON(perm), "invs" -> invs.map(inverseFunctionsToJSON).getOrElse(JsNull), - "cond" -> cond.map(TermWriter.toJSON).getOrElse(JsNull), "receiver" -> receiver.map(TermWriter.toJSON).getOrElse(JsNull), "hints" -> (if (hints.nonEmpty) JsArray(hints.map(TermWriter.toJSON).toVector) else JsNull) ) - case QuantifiedPredicateChunk(id, vars, _, psf, perm, _, invs, cond, singletonArgs, _, hints) => + case QuantifiedPredicateChunk(id, vars, _, psf, condition, _, perm, _, invs, singletonArgs, _, hints) => JsObject( "type" -> JsString("quantified_predicate_chunk"), "vars" -> JsArray(vars.map(TermWriter.toJSON).toVector), "predicate" -> JsString(id.toString), "predicate_snap_function" -> TermWriter.toJSON(psf), + "condition" -> TermWriter.toJSON(condition), "perm" -> TermWriter.toJSON(perm), "invs" -> invs.map(inverseFunctionsToJSON).getOrElse(JsNull), - "cond" -> cond.map(TermWriter.toJSON).getOrElse(JsNull), "singleton_args" -> singletonArgs.map(as => JsArray(as.map(TermWriter.toJSON).toVector)).getOrElse(JsNull), "hints" -> (if (hints.nonEmpty) JsArray(hints.map(TermWriter.toJSON).toVector) else JsNull) ) - case QuantifiedMagicWandChunk(id, vars, _, wsf, perm, _, invs, cond, singletonArgs, _, hints) => + case QuantifiedMagicWandChunk(id, vars, _, wsf, perm, _, invs, singletonArgs, _, hints) => JsObject( "type" -> JsString("quantified_magic_wand_chunk"), "vars" -> JsArray(vars.map(TermWriter.toJSON).toVector), @@ -91,7 +91,6 @@ object SymbExLogReportWriter { "wand_snap_function" -> TermWriter.toJSON(wsf), "perm" -> TermWriter.toJSON(perm), "invs" -> invs.map(inverseFunctionsToJSON).getOrElse(JsNull), - "cond" -> cond.map(TermWriter.toJSON).getOrElse(JsNull), "singleton_args" -> singletonArgs.map(as => JsArray(as.map(TermWriter.toJSON).toVector)).getOrElse(JsNull), "hints" -> (if (hints.nonEmpty) JsArray(hints.map(TermWriter.toJSON).toVector) else JsNull) ) diff --git a/src/main/scala/rules/ChunkSupporter.scala b/src/main/scala/rules/ChunkSupporter.scala index 0af1205c..311063b2 100644 --- a/src/main/scala/rules/ChunkSupporter.scala +++ b/src/main/scala/rules/ChunkSupporter.scala @@ -56,12 +56,6 @@ trait ChunkSupportRules extends SymbolicExecutionRules { v: Verifier) : Option[CH] - def findMatchingChunk[CH <: NonQuantifiedChunk: ClassTag] - (chunks: Iterable[Chunk], - chunk: CH, - v: Verifier) - : Option[CH] - def findChunksWithID[CH <: NonQuantifiedChunk: ClassTag] (chunks: Iterable[Chunk], id: ChunkIdentifer) @@ -264,11 +258,6 @@ object chunkSupporter extends ChunkSupportRules { findChunkLiterally(relevantChunks, args) orElse findChunkWithProver(relevantChunks, args, v) } - def findMatchingChunk[CH <: NonQuantifiedChunk: ClassTag] - (chunks: Iterable[Chunk], chunk: CH, v: Verifier): Option[CH] = { - findChunk[CH](chunks, chunk.id, chunk.args, v) - } - def findChunksWithID[CH <: NonQuantifiedChunk: ClassTag](chunks: Iterable[Chunk], id: ChunkIdentifer): Iterable[CH] = { chunks.flatMap { case c: CH if id == c.id => Some(c) diff --git a/src/main/scala/rules/QuantifiedChunkSupport.scala b/src/main/scala/rules/QuantifiedChunkSupport.scala index ec7687c2..37a7a26b 100644 --- a/src/main/scala/rules/QuantifiedChunkSupport.scala +++ b/src/main/scala/rules/QuantifiedChunkSupport.scala @@ -18,7 +18,7 @@ import viper.silicon.state.terms._ import viper.silicon.state.terms.perms.{BigPermSum, IsPositive} import viper.silicon.state.terms.predef.`?r` import viper.silicon.state.terms.utils.consumeExactRead -import viper.silicon.supporters.functions.NoopFunctionRecorder +import viper.silicon.supporters.functions.{FunctionRecorder, NoopFunctionRecorder} import viper.silicon.utils.ast.{BigAnd, buildMinExp} import viper.silicon.utils.notNothing.NotNothing import viper.silicon.verifier.Verifier @@ -224,6 +224,35 @@ trait QuantifiedChunkSupport extends SymbolicExecutionRules { def hintBasedChunkOrderHeuristic(hints: Seq[Term]) : Seq[QuantifiedBasicChunk] => Seq[QuantifiedBasicChunk] + + def findChunk(chunks: Iterable[Chunk], chunk: QuantifiedChunk, v: Verifier): Option[QuantifiedChunk] + + /** Merge the snapshots of two quantified heap chunks that denote the same field locations + * + * @param fr The functionRecorder to use when new snapshot maps are generated. + * @param field The name of the field. + * @param t1 The first chunk's snapshot map. + * @param t2 The second chunk's snapshot map. + * @param p1 The first chunk's permission amount, should be constrained by the domain. + * @param p2 The second chunk's permission amount, should be constrained by the domain. + * @param v The verifier to use. + * @return A tuple (fr, sm, def) of functionRecorder, a snapshot map sm and a term def constraining sm. + */ + def combineFieldSnapshotMaps(fr: FunctionRecorder, field: String, t1: Term, t2: Term, p1: Term, p2: Term, v: Verifier): (FunctionRecorder, Term, Term) + + /** Merge the snapshots of two quantified heap chunks that denote the same predicate + * + * @param fr The functionRecorder to use when new snapshot maps are generated. + * @param predicate The name of the predicate. + * @param qVars The variables over which p1 and p2 are defined + * @param t1 The first chunk's snapshot map. + * @param t2 The second chunk's snapshot map. + * @param p1 The first chunk's permission amount, should be constrained by the domain. + * @param p2 The second chunk's permission amount, should be constrained by the domain. + * @param v The verifier to use. + * @return A tuple (fr, sm, def) of functionRecorder, a snapshot map sm and a term def constraining sm. + */ + def combinePredicateSnapshotMaps(fr: FunctionRecorder, predicate: String, qVars: Seq[Var], t1: Term, t2: Term, p1: Term, p2: Term, v: Verifier): (FunctionRecorder, Term, Term) } object quantifiedChunkSupporter extends QuantifiedChunkSupport { @@ -247,12 +276,8 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { .zip(arguments) .map { case (x, a) => x === a }) - val conditionExp = codomainQVarsExp.map(vars => BigAnd(vars.zip(argumentsExp.get).map { case (x, a) => ast.EqCmp(x.localVar, a)() } )) - - val conditionalizedPermissions = - Ite(condition, permissions, NoPerm) - val conditionalizedPermissionsExp = permissionsExp.map(pe => ast.CondExp(conditionExp.get, pe, ast.NoPerm()())(pe.pos, pe.info, pe.errT)) + val conditionExp = codomainQVarsExp.map(vars => BigAnd(vars.zip(argumentsExp.get).map { case (x, a) => ast.EqCmp(x.localVar, a)() } )) val hints = extractHints(None, arguments) @@ -262,10 +287,11 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { resource, arguments, sm, - conditionalizedPermissions, - conditionalizedPermissionsExp, + condition, + conditionExp, + permissions, + permissionsExp, None, - Some(conditionalizedPermissions), Some(arguments), argumentsExp, hints, @@ -310,17 +336,8 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { val qvarsToInversesOfCodomain = inverseFunctions.qvarsToInversesOf(codomainQVars) - val conditionalizedPermissions = - Ite( - And(And(imagesOfCodomain), condition.replace(qvarsToInversesOfCodomain)), - permissions.replace(qvarsToInversesOfCodomain), - NoPerm) - - val conditionalizedPermissionsExp = - Option.when(withExp)(ast.CondExp( - conditionExp.get, - permissionExps.get, - ast.NoPerm()())()) + val cond = And(And(imagesOfCodomain), condition.replace(qvarsToInversesOfCodomain)) + val perms = permissions.replace(qvarsToInversesOfCodomain) val hints = extractHints(Some(condition), arguments) @@ -331,10 +348,11 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { resource, arguments, sm, - conditionalizedPermissions, - conditionalizedPermissionsExp, + cond, + conditionExp, + perms, + permissionExps, Some(inverseFunctions), - Some(conditionalizedPermissions), None, None, hints, @@ -372,10 +390,11 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { resource: ast.Resource, arguments: Seq[Term], sm: Term, + condition: Term, + conditionExp: Option[ast.Exp], permissions: Term, permissionsExp: Option[ast.Exp], optInverseFunctions: Option[InverseFunctions], - optInitialCond: Option[Term], optSingletonArguments: Option[Seq[Term]], optSingletonArgumentsExp: Option[Seq[ast.Exp]], hints: Seq[Term], @@ -391,10 +410,11 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { QuantifiedFieldChunk( BasicChunkIdentifier(field.name), sm, + condition, + conditionExp, permissions, permissionsExp, optInverseFunctions, - optInitialCond, optSingletonArguments.map(_.head), optSingletonArgumentsExp.map(_.head), hints) @@ -405,24 +425,26 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { codomainQVars, codomainQVarExps, sm, + condition, + conditionExp, permissions, permissionsExp, optInverseFunctions, - optInitialCond, optSingletonArguments, optSingletonArgumentsExp, hints) case wand: ast.MagicWand => + val conditionalizedPermissions = Ite(condition, permissions, NoPerm) + val conditionalizedPermissionsExp = conditionExp.map(ce => ast.CondExp(ce, permissionsExp.get, ast.NoPerm()())(ce.pos, ce.info, ce.errT)) QuantifiedMagicWandChunk( MagicWandIdentifier(wand, program), codomainQVars, codomainQVarExps, sm, - permissions, - permissionsExp, + conditionalizedPermissions, + conditionalizedPermissionsExp, optInverseFunctions, - optInitialCond, optSingletonArguments, optSingletonArgumentsExp, hints) @@ -1588,12 +1610,10 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { v.decider.assume(permissionConstraint, permissionConstraintExp, permissionConstraintExp) remainingChunks = - remainingChunks :+ ithChunk.withPerm(PermMinus(ithChunk.perm, ithPTaken), - ithPTakenExp.map(ipt => ast.PermSub(ithChunk.permExp.get, ipt)(ipt.pos, ipt.info, ipt.errT))) + remainingChunks :+ ithChunk.permMinus(ithPTaken, ithPTakenExp) } else { v.decider.prover.comment(s"Chunk depleted?") val chunkDepleted = v.decider.check(depletedCheck, Verifier.config.splitTimeout()) - if (!chunkDepleted) { val unusedCheck = Forall(codomainQVars, ithPTaken === NoPerm, Nil) val chunkUnused = v.decider.check(unusedCheck, Verifier.config.checkTimeout()) @@ -1601,8 +1621,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { remainingChunks = remainingChunks :+ ithChunk } else { remainingChunks = - remainingChunks :+ ithChunk.withPerm(PermMinus(ithChunk.perm, ithPTaken), - ithPTakenExp.map(ipt => ast.PermSub(ithChunk.permExp.get, ipt)(ipt.pos, ipt.info, ipt.errT))) + remainingChunks :+ ithChunk.permMinus(ithPTaken, ithPTakenExp) } } } @@ -1944,6 +1963,127 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { matchingChunks ++ otherChunks } + override def findChunk(chunks: Iterable[Chunk], chunk: QuantifiedChunk, v: Verifier): Option[QuantifiedChunk] = { + val lr = chunk match { + case qfc: QuantifiedFieldChunk if qfc.invs.isDefined => + Left(qfc.invs.get.invertibles, qfc.quantifiedVars, qfc.condition) + case qfc: QuantifiedFieldChunk if qfc.singletonArguments.isDefined => + Right(qfc.singletonArguments.get) + case qpc: QuantifiedPredicateChunk if qpc.invs.isDefined => + Left(qpc.invs.get.invertibles, qpc.quantifiedVars, qpc.condition) + case qpc: QuantifiedPredicateChunk if qpc.singletonArguments.isDefined => + Right(qpc.singletonArguments.get) + case _ => return None + } + val relevantChunks: Iterable[QuantifiedBasicChunk] = chunks.flatMap { + case ch: QuantifiedBasicChunk if ch.id == chunk.id => Some(ch) + case _ => None + } + + val (receiverTerms, quantVars, cond) = lr match { + case Left(tuple) => tuple + case Right(singletonArguments) => + return relevantChunks.find { ch => + val chunkInfo = ch match { + case qfc: QuantifiedFieldChunk if qfc.singletonArguments.isDefined => + Some(qfc.singletonArguments.get) + case qpc: QuantifiedPredicateChunk if qpc.singletonArguments.isDefined => + Some(qpc.singletonArguments.get) + case _ => None + } + chunkInfo match { + case Some(cSingletonArguments) => + val equalityTerm = And(singletonArguments.zip(cSingletonArguments).map { case (a, b) => a === b }) + val result = v.decider.check(equalityTerm, Verifier.config.checkTimeout()) + if (result) { + // Learn the equality + val debugExp = Option.when(withExp)(DebugExp.createInstance("Chunks alias", true)) + v.decider.assume(equalityTerm, debugExp) + } + result + case _ => false + } + } + } + relevantChunks.find { ch => + val chunkInfo = ch match { + case qfc: QuantifiedFieldChunk if qfc.invs.isDefined => + Some(qfc.invs.get.invertibles, qfc.quantifiedVars, qfc.condition) + case qpc: QuantifiedPredicateChunk if qpc.invs.isDefined => + Some(qpc.invs.get.invertibles, qpc.quantifiedVars, qpc.condition) + case _ => None + } + chunkInfo match { + case Some((cInvertibles, cQvars, cCond)) => + receiverTerms.zip(cInvertibles).forall(p => { + if (cQvars.length == quantVars.length && cQvars.zip(quantVars).forall(vars => vars._1.sort == vars._2.sort)) { + val condReplaced = cCond.replace(cQvars, quantVars) + val secondReplaced = p._2.replace(cQvars, quantVars) + val equalityTerm = SimplifyingForall(quantVars, And(Seq(p._1 === secondReplaced, cond === condReplaced)), Seq()) + val result = v.decider.check(equalityTerm, Verifier.config.checkTimeout()) + if (result) { + // Learn the equality + val debugExp = Option.when(withExp)(DebugExp.createInstance("Chunks alias", true)) + v.decider.assume(equalityTerm, debugExp) + } + result + } else { + false + } + }) + case _ => false + } + } + } + + // Based on StateConsolidator#combineSnapshots + override def combineFieldSnapshotMaps(fr: FunctionRecorder, field: String, t1: Term, t2: Term, p1: Term, p2: Term, v: Verifier): (FunctionRecorder, Term, Term) = { + val lookupT1 = Lookup(field, t1, `?r`) + val lookupT2 = Lookup(field, t2, `?r`) + val (fr2, sm, smDef, triggers) = (IsPositive(p1), IsPositive(p2)) match { + // If we statically know that both permission values are positive we can forego the quantifier + case (True, True) => return (fr, t1, t1 === t2) + case (True, b2) => (fr, t1, Implies(b2, lookupT1 === lookupT2), Seq(Trigger(lookupT1), Trigger(lookupT2))) + case (b1, True) => (fr, t2, Implies(b1, lookupT2 === lookupT1), Seq(Trigger(lookupT2), Trigger(lookupT1))) + case (b1, b2) => + /* + * Since it is not definitely known whether p1 and p2 are positive, + * we have to introduce a fresh snapshot. Note that it is not sound + * to use t1 or t2 and constrain it. + */ + val t3 = v.decider.fresh(t1.sort, Option.when(withExp)(PUnknown())) + val lookupT3 = Lookup(field, t3, `?r`) + (fr.recordConstrainedVar(t3, And(Implies(b1, lookupT3 === lookupT1), Implies(b2, lookupT3 === lookupT2))), t3, + And(Implies(b1, lookupT3 === lookupT1), Implies(b2, lookupT3 === lookupT2)), Seq(Trigger(lookupT1), Trigger(lookupT2), Trigger(lookupT3))) + } + + (fr2, sm, Forall(`?r`, smDef, triggers)) + } + + // Based on StateConsolidator#combineSnapshots + override def combinePredicateSnapshotMaps(fr: FunctionRecorder, predicate: String, qVars: Seq[Var], t1: Term, t2: Term, p1: Term, p2: Term, v: Verifier): (FunctionRecorder, Term, Term) = { + val lookupT1 = PredicateLookup(predicate, t1, qVars) + val lookupT2 = PredicateLookup(predicate, t2, qVars) + val (fr2, sm, smDef, triggers) = (IsPositive(p1), IsPositive(p2)) match { + // If we statically know that both permission values are positive we can forego the quantifier + case (True, True) => return (fr, t1, t1 === t2) + case (True, b2) => (fr, t1, Implies(b2, lookupT1 === lookupT2), Seq(Trigger(lookupT1), Trigger(lookupT2))) + case (b1, True) => (fr, t2, Implies(b1, lookupT2 === lookupT1), Seq(Trigger(lookupT2), Trigger(lookupT1))) + case (b1, b2) => + /* + * Since it is not definitely known whether p1 and p2 are positive, + * we have to introduce a fresh snapshot. Note that it is not sound + * to use t1 or t2 and constrain it. + */ + val t3 = v.decider.fresh(t1.sort, Option.when(withExp)(PUnknown())) + val lookupT3 = PredicateLookup(predicate, t3, qVars) + (fr.recordConstrainedVar(t3, And(Implies(b1, lookupT3 === lookupT1), Implies(b2, lookupT3 === lookupT2))), t3, + And(Implies(b1, lookupT3 === lookupT1), Implies(b2, lookupT3 === lookupT2)), Seq(Trigger(lookupT1), Trigger(lookupT2), Trigger(lookupT3))) + } + + (fr2, sm, Forall(qVars, smDef, triggers)) + } + def qpAppChunkOrderHeuristics(receiverTerms: Seq[Term], quantVars: Seq[Var], hints: Seq[Term], v: Verifier) : Seq[QuantifiedBasicChunk] => Seq[QuantifiedBasicChunk] = { // Heuristics that looks for quantified chunks that have the same shape (as in, the same number and types of diff --git a/src/main/scala/rules/StateConsolidator.scala b/src/main/scala/rules/StateConsolidator.scala index 2d08658f..a8e29210 100644 --- a/src/main/scala/rules/StateConsolidator.scala +++ b/src/main/scala/rules/StateConsolidator.scala @@ -67,13 +67,11 @@ class DefaultStateConsolidator(protected val config: Config) extends StateConsol val (functionRecorderAfterHeapMerging, mergedHeaps) = initialHeaps.foldLeft((s.functionRecorder, Nil: List[Heap])) { case ((fr, hs), h) => - val (nonQuantifiedChunks, otherChunks) = partition(h) - var continue = false - var mergedChunks: Seq[NonQuantifiedChunk] = Nil - var destChunks: Seq[NonQuantifiedChunk] = Nil - var newChunks: Seq[NonQuantifiedChunk] = nonQuantifiedChunks + var mergedChunks: Seq[Chunk] = Nil + var destChunks: Seq[Chunk] = Nil + var newChunks: Seq[Chunk] = h.values.toSeq var functionRecorder: FunctionRecorder = fr var fixedPointRound: Int = 0 @@ -95,10 +93,10 @@ class DefaultStateConsolidator(protected val config: Config) extends StateConsol fixedPointRound = fixedPointRound + 1 } while (continue) - val allChunks = mergedChunks ++ otherChunks - val interpreter = new NonQuantifiedPropertyInterpreter(allChunks, v) - mergedChunks foreach { ch => + val interpreter = new NonQuantifiedPropertyInterpreter(mergedChunks, v) + + mergedChunks.filter(_.isInstanceOf[BasicChunk]) foreach { case ch: BasicChunk => val resource = Resources.resourceDescriptions(ch.resourceID) val pathCond = interpreter.buildPathConditionsForChunk(ch, resource.instanceProperties) pathCond.foreach(p => v.decider.assume(p._1, Option.when(withExp)(DebugExp.createInstance(p._2, p._2)))) @@ -110,7 +108,7 @@ class DefaultStateConsolidator(protected val config: Config) extends StateConsol } v.symbExLog.closeScope(sepIdentifier) - (functionRecorder, hs :+ Heap(allChunks)) + (functionRecorder, hs :+ Heap(mergedChunks)) } val s1 = s.copy(functionRecorder = functionRecorderAfterHeapMerging, @@ -133,37 +131,35 @@ class DefaultStateConsolidator(protected val config: Config) extends StateConsol def merge(fr1: FunctionRecorder, s: State, h: Heap, newH: Heap, v: Verifier): (FunctionRecorder, Heap) = { val mergeLog = new CommentRecord("Merge", null, v.decider.pcs) val sepIdentifier = v.symbExLog.openScope(mergeLog) - val (nonQuantifiedChunks, otherChunks) = partition(h) - val (newNonQuantifiedChunks, newOtherChunk) = partition(newH) - val (fr2, mergedChunks, newlyAddedChunks, snapEqs) = singleMerge(fr1, nonQuantifiedChunks, newNonQuantifiedChunks, v) + val (fr2, mergedChunks, newlyAddedChunks, snapEqs) = singleMerge(fr1, h.values.toSeq, newH.values.toSeq, v) v.decider.assume(snapEqs, Option.when(withExp)(DebugExp.createInstance("Snapshot", isInternal_ = true)), enforceAssumption = false) val interpreter = new NonQuantifiedPropertyInterpreter(mergedChunks, v) - newlyAddedChunks foreach { ch => + newlyAddedChunks.filter(_.isInstanceOf[BasicChunk]) foreach { case ch: BasicChunk => val resource = Resources.resourceDescriptions(ch.resourceID) val pathCond = interpreter.buildPathConditionsForChunk(ch, resource.instanceProperties) pathCond.foreach(p => v.decider.assume(p._1, Option.when(withExp)(DebugExp.createInstance(p._2, p._2)))) } v.symbExLog.closeScope(sepIdentifier) - (fr2, Heap(mergedChunks ++ otherChunks ++ newOtherChunk)) + (fr2, Heap(mergedChunks)) } private def singleMerge(fr: FunctionRecorder, - destChunks: Seq[NonQuantifiedChunk], - newChunks: Seq[NonQuantifiedChunk], + destChunks: Seq[Chunk], + newChunks: Seq[Chunk], v: Verifier) : (FunctionRecorder, - Seq[NonQuantifiedChunk], - Seq[NonQuantifiedChunk], + Seq[Chunk], + Seq[Chunk], InsertionOrderedSet[Term]) = { val mergeLog = new SingleMergeRecord(destChunks, newChunks, v.decider.pcs) val sepIdentifier = v.symbExLog.openScope(mergeLog) // bookkeeper.heapMergeIterations += 1 - val initial = (fr, destChunks, Seq[NonQuantifiedChunk](), InsertionOrderedSet[Term]()) + val initial = (fr, destChunks, Seq[Chunk](), InsertionOrderedSet[Term]()) val result = newChunks.foldLeft(initial) { case ((fr1, accMergedChunks, accNewChunks, accSnapEqs), nextChunk) => /* accMergedChunks: already merged chunks @@ -173,7 +169,7 @@ class DefaultStateConsolidator(protected val config: Config) extends StateConsol * sequence of destination chunks */ - chunkSupporter.findMatchingChunk(accMergedChunks, nextChunk, v) match { + findMatchingChunk(accMergedChunks, nextChunk, v) match { case Some(ch) => mergeChunks(fr1, ch, nextChunk, v) match { case Some((fr2, newChunk, snapEq)) => @@ -189,14 +185,40 @@ class DefaultStateConsolidator(protected val config: Config) extends StateConsol result } + private def findMatchingChunk(chunks: Iterable[Chunk], chunk: Chunk, v: Verifier): Option[Chunk] = { + chunk match { + case chunk: BasicChunk => + chunkSupporter.findChunk[BasicChunk](chunks, chunk.id, chunk.args, v) + case chunk: QuantifiedChunk => quantifiedChunkSupporter.findChunk(chunks, chunk, v) + case _ => None + } + } + // Merges two chunks that are aliases (i.e. that have the same id and the args are proven to be equal) // and returns the merged chunk or None, if the chunks could not be merged - private def mergeChunks(fr1: FunctionRecorder, chunk1: NonQuantifiedChunk, chunk2: NonQuantifiedChunk, v: Verifier) = (chunk1, chunk2) match { + private def mergeChunks(fr1: FunctionRecorder, chunk1: Chunk, chunk2: Chunk, v: Verifier): Option[(FunctionRecorder, Chunk, Term)] = (chunk1, chunk2) match { case (BasicChunk(rid1, id1, args1, args1Exp, snap1, perm1, perm1Exp), BasicChunk(_, _, _, _, snap2, perm2, perm2Exp)) => val (fr2, combinedSnap, snapEq) = combineSnapshots(fr1, snap1, snap2, perm1, perm2, v) Some(fr2, BasicChunk(rid1, id1, args1, args1Exp, combinedSnap, PermPlus(perm1, perm2), perm1Exp.map(p1 => ast.PermAdd(p1, perm2Exp.get)())), snapEq) - case (_, _) => + case (l@QuantifiedFieldChunk(id1, fvf1, condition1, condition1Exp, perm1, perm1Exp, invs1, singletonRcvr1, singletonRcvr1Exp, hints1), + r@QuantifiedFieldChunk(_, fvf2, _, _, perm2, perm2Exp, _, _, _, hints2)) => + assert(l.quantifiedVars == Seq(`?r`)) + assert(r.quantifiedVars == Seq(`?r`)) + // We need to use l.perm/r.perm here instead of perm1 and perm2 since the permission amount might be dependent on the condition/domain + val (fr2, combinedSnap, snapEq) = quantifiedChunkSupporter.combineFieldSnapshotMaps(fr1, id1.name, fvf1, fvf2, l.perm, r.perm, v) + val permSum = PermPlus(perm1, perm2) + val permSumExp = perm1Exp.map(p1 => ast.PermAdd(p1, perm2Exp.get)()) + val bestHints = if (hints1.nonEmpty) hints1 else hints2 + Some(fr2, QuantifiedFieldChunk(id1, combinedSnap, condition1, condition1Exp, permSum, permSumExp, invs1, singletonRcvr1, singletonRcvr1Exp, bestHints), snapEq) + case (l@QuantifiedPredicateChunk(id1, qVars1, qVars1Exp, psf1, _, _, perm1, perm1Exp, _, _, _, _), + r@QuantifiedPredicateChunk(_, qVars2, qVars2Exp, psf2, condition2, condition2Exp, perm2, perm2Exp, invs2, singletonArgs2, singletonArgs2Exp, hints2)) => + val (fr2, combinedSnap, snapEq) = quantifiedChunkSupporter.combinePredicateSnapshotMaps(fr1, id1.name, qVars2, psf1, psf2, l.perm.replace(qVars1, qVars2), r.perm, v) + + val permSum = PermPlus(perm1.replace(qVars1, qVars2), perm2) + val permSumExp = perm1Exp.map(p1 => ast.PermAdd(p1.replace(qVars1Exp.get.zip(qVars2Exp.get).toMap), perm2Exp.get)()) + Some(fr2, QuantifiedPredicateChunk(id1, qVars2, qVars2Exp, combinedSnap, condition2, condition2Exp, permSum, permSumExp, invs2, singletonArgs2, singletonArgs2Exp, hints2), snapEq) + case _ => None } diff --git a/src/main/scala/state/Chunks.scala b/src/main/scala/state/Chunks.scala index 0292727c..e986fade 100644 --- a/src/main/scala/state/Chunks.scala +++ b/src/main/scala/state/Chunks.scala @@ -43,6 +43,12 @@ case class BasicChunk(resourceID: BaseID, case PredicateID => require(snap.sort == sorts.Snap, s"A predicate chunk's snapshot ($snap) is expected to be of sort Snap, but found ${snap.sort}") } + override def applyCondition(newCond: Term, newCondExp: Option[ast.Exp]) = + withPerm(Ite(newCond, perm, NoPerm), newCondExp.map(nce => ast.CondExp(nce, permExp.get, ast.NoPerm()())())) + override def permMinus(newPerm: Term, newPermExp: Option[ast.Exp]) = + withPerm(PermMinus(perm, newPerm), newPermExp.map(npe => ast.PermSub(permExp.get, npe)())) + override def permPlus(newPerm: Term, newPermExp: Option[ast.Exp]) = + withPerm(PermPlus(perm, newPerm), newPermExp.map(npe => ast.PermAdd(permExp.get, npe)())) override def withPerm(newPerm: Term, newPermExp: Option[ast.Exp]) = BasicChunk(resourceID, id, args, argsExp, snap, newPerm, newPermExp) override def withSnap(newSnap: Term) = BasicChunk(resourceID, id, args, argsExp, newSnap, perm, permExp) @@ -54,7 +60,9 @@ case class BasicChunk(resourceID: BaseID, sealed trait QuantifiedBasicChunk extends QuantifiedChunk { override val id: ChunkIdentifer - override def withPerm(perm: Term, permExp: Option[ast.Exp]): QuantifiedBasicChunk + override def applyCondition(newCond: Term, newCondExp: Option[ast.Exp]): QuantifiedBasicChunk + override def permMinus(perm: Term, permExp: Option[ast.Exp]): QuantifiedBasicChunk + override def permPlus(perm: Term, permExp: Option[ast.Exp]): QuantifiedBasicChunk override def withSnapshotMap(snap: Term): QuantifiedBasicChunk def singletonArguments: Option[Seq[Term]] def singletonArgumentExps: Option[Seq[ast.Exp]] @@ -68,10 +76,11 @@ sealed trait QuantifiedBasicChunk extends QuantifiedChunk { */ case class QuantifiedFieldChunk(id: BasicChunkIdentifier, fvf: Term, - perm: Term, - permExp: Option[ast.Exp], + condition: Term, + conditionExp: Option[ast.Exp], + permValue: Term, + permValueExp: Option[ast.Exp], invs: Option[InverseFunctions], - initialCond: Option[Term], singletonRcvr: Option[Term], singletonRcvrExp: Option[ast.Exp], hints: Seq[Term] = Nil) @@ -79,13 +88,14 @@ case class QuantifiedFieldChunk(id: BasicChunkIdentifier, require(fvf.sort.isInstanceOf[terms.sorts.FieldValueFunction], s"Quantified chunk values must be of sort FieldValueFunction, but found value $fvf of sort ${fvf.sort}") - require(perm.sort == sorts.Perm, s"Permissions $perm must be of sort Perm, but found ${perm.sort}") + require(permValue.sort == sorts.Perm, s"Permissions $permValue must be of sort Perm, but found ${permValue.sort}") override val resourceID = FieldID override val quantifiedVars = Seq(`?r`) + override val perm = Ite(condition, permValue, NoPerm) + override val permExp: Option[ast.Exp] = conditionExp.map(c => ast.CondExp(c, permValueExp.get, ast.NoPerm()())()) override val quantifiedVarExps = if (Verifier.config.enableDebugging()) Some(Seq(ast.LocalVarDecl(`?r`.id.name, ast.Ref)())) else None - override def snapshotMap: Term = fvf override def singletonArguments: Option[Seq[Term]] = singletonRcvr.map(Seq(_)) @@ -99,8 +109,16 @@ case class QuantifiedFieldChunk(id: BasicChunkIdentifier, Lookup(id.name, fvf, arguments.head) } - override def withPerm(newPerm: Term, newPermExp: Option[ast.Exp]) = QuantifiedFieldChunk(id, fvf, newPerm, newPermExp, invs, initialCond, singletonRcvr, singletonRcvrExp, hints) - override def withSnapshotMap(newFvf: Term) = QuantifiedFieldChunk(id, newFvf, perm, permExp, invs, initialCond, singletonRcvr, singletonRcvrExp, hints) + def withPerm(newPerm: Term, newPermExp: Option[ast.Exp]) = + QuantifiedFieldChunk(id, fvf, condition, conditionExp, newPerm, newPermExp, invs, singletonRcvr, singletonRcvrExp, hints) + override def applyCondition(newCond: Term, newCondExp: Option[ast.Exp]) = + QuantifiedFieldChunk(id, fvf, terms.And(newCond, condition), newCondExp.map(nce => ast.And(nce, conditionExp.get)()), permValue, permValueExp, invs, singletonRcvr, singletonRcvrExp, hints) + override def permMinus(newPerm: Term, newPermExp: Option[ast.Exp]) = + withPerm(PermMinus(permValue, newPerm), newPermExp.map(npe => ast.PermSub(permValueExp.get, npe)())) + override def permPlus(newPerm: Term, newPermExp: Option[ast.Exp]) = + withPerm(PermPlus(permValue, newPerm), newPermExp.map(npe => ast.PermAdd(permValueExp.get, npe)())) + override def withSnapshotMap(newFvf: Term) = + QuantifiedFieldChunk(id, newFvf, condition, conditionExp, permValue, permValueExp, invs, singletonRcvr, singletonRcvrExp, hints) override lazy val toString = s"${terms.Forall} ${`?r`} :: ${`?r`}.$id -> $fvf # $perm" } @@ -109,19 +127,22 @@ case class QuantifiedPredicateChunk(id: BasicChunkIdentifier, quantifiedVars: Seq[Var], quantifiedVarExps: Option[Seq[ast.LocalVarDecl]], psf: Term, - perm: Term, - permExp: Option[ast.Exp], + condition: Term, + conditionExp: Option[ast.Exp], + permValue: Term, + permValueExp: Option[ast.Exp], invs: Option[InverseFunctions], - initialCond: Option[Term], singletonArgs: Option[Seq[Term]], singletonArgExps: Option[Seq[ast.Exp]], hints: Seq[Term] = Nil) extends QuantifiedBasicChunk { require(psf.sort.isInstanceOf[terms.sorts.PredicateSnapFunction], s"Quantified predicate chunk values must be of sort PredicateSnapFunction ($psf), but found ${psf.sort}") - require(perm.sort == sorts.Perm, s"Permissions $perm must be of sort Perm, but found ${perm.sort}") + require(permValue.sort == sorts.Perm, s"Permissions $permValue must be of sort Perm, but found ${permValue.sort}") override val resourceID = PredicateID + override val perm = Ite(condition, permValue, NoPerm) + override val permExp = conditionExp.map(c => ast.CondExp(c, permValueExp.get, ast.NoPerm()())()) override def snapshotMap: Term = psf override def singletonArguments: Option[Seq[Term]] = singletonArgs @@ -129,8 +150,16 @@ case class QuantifiedPredicateChunk(id: BasicChunkIdentifier, override def valueAt(args: Seq[Term]) = PredicateLookup(id.name, psf, args) - override def withPerm(newPerm: Term, newPermExp: Option[ast.Exp]) = QuantifiedPredicateChunk(id, quantifiedVars, quantifiedVarExps, psf, newPerm, newPermExp, invs, initialCond, singletonArgs, singletonArgExps, hints) - override def withSnapshotMap(newPsf: Term) = QuantifiedPredicateChunk(id, quantifiedVars, quantifiedVarExps, newPsf, perm, permExp, invs, initialCond, singletonArgs, singletonArgExps, hints) + def withPerm(newPerm: Term, newPermExp: Option[ast.Exp]) = + QuantifiedPredicateChunk(id, quantifiedVars, quantifiedVarExps, psf, condition, conditionExp, newPerm, newPermExp, invs, singletonArgs, singletonArgExps, hints) + override def applyCondition(newCond: Term, newCondExp: Option[ast.Exp]) = + QuantifiedPredicateChunk(id, quantifiedVars, quantifiedVarExps, psf, terms.And(newCond, condition), newCondExp.map(nce => ast.And(nce, conditionExp.get)()), permValue, permValueExp, invs, singletonArgs, singletonArgExps, hints) + override def permMinus(newPerm: Term, newPermExp: Option[ast.Exp]) = + withPerm(PermMinus(permValue, newPerm), newPermExp.map(npe => ast.PermSub(permValueExp.get, npe)())) + override def permPlus(newPerm: Term, newPermExp: Option[ast.Exp]) = + withPerm(PermPlus(permValue, newPerm), newPermExp.map(npe => ast.PermAdd(permValueExp.get, npe)())) + override def withSnapshotMap(newPsf: Term) = + QuantifiedPredicateChunk(id, quantifiedVars, quantifiedVarExps, newPsf, condition, conditionExp, permValue, permValueExp, invs, singletonArgs, singletonArgExps, hints) override lazy val toString = s"${terms.Forall} ${quantifiedVars.mkString(",")} :: $id(${quantifiedVars.mkString(",")}) -> $psf # $perm" } @@ -142,7 +171,6 @@ case class QuantifiedMagicWandChunk(id: MagicWandIdentifier, perm: Term, permExp: Option[ast.Exp], invs: Option[InverseFunctions], - initialCond: Option[Term], singletonArgs: Option[Seq[Term]], singletonArgExps: Option[Seq[ast.Exp]], hints: Seq[Term] = Nil) @@ -159,8 +187,16 @@ case class QuantifiedMagicWandChunk(id: MagicWandIdentifier, override def valueAt(args: Seq[Term]) = PredicateLookup(id.toString, wsf, args) - override def withPerm(newPerm: Term, newPermExp: Option[ast.Exp]) = QuantifiedMagicWandChunk(id, quantifiedVars, quantifiedVarExps, wsf, newPerm, newPermExp, invs, initialCond, singletonArgs, singletonArgExps, hints) - override def withSnapshotMap(newWsf: Term) = QuantifiedMagicWandChunk(id, quantifiedVars, quantifiedVarExps, newWsf, perm, permExp, invs, initialCond, singletonArgs, singletonArgExps, hints) + override def applyCondition(newCond: Term, newCondExp: Option[ast.Exp]) = + withPerm(Ite(newCond, perm, NoPerm), newCondExp.map(nce => ast.CondExp(nce, permExp.get, ast.NoPerm()())())) + override def permMinus(newPerm: Term, newPermExp: Option[ast.Exp]) = + withPerm(PermMinus(perm, newPerm), newPermExp.map(npe => ast.PermSub(permExp.get, npe)())) + override def permPlus(newPerm: Term, newPermExp: Option[ast.Exp]) = + withPerm(PermPlus(perm, newPerm), newPermExp.map(npe => ast.PermAdd(permExp.get, npe)())) + def withPerm(newPerm: Term, newPermExp: Option[ast.Exp]) = + QuantifiedMagicWandChunk(id, quantifiedVars, quantifiedVarExps, wsf, newPerm, newPermExp, invs, singletonArgs, singletonArgExps, hints) + override def withSnapshotMap(newWsf: Term) = + QuantifiedMagicWandChunk(id, quantifiedVars, quantifiedVarExps, newWsf, perm, permExp, invs, singletonArgs, singletonArgExps, hints) override lazy val toString = s"${terms.Forall} ${quantifiedVars.mkString(",")} :: $id(${quantifiedVars.mkString(",")}) -> $wsf # $perm" } @@ -195,7 +231,14 @@ case class MagicWandChunk(id: MagicWandIdentifier, override val resourceID = MagicWandID + override def applyCondition(newCond: Term, newCondExp: Option[ast.Exp]) = + withPerm(Ite(newCond, perm, NoPerm), newCondExp.map(nce => ast.CondExp(nce, permExp.get, ast.NoPerm()())())) + override def permMinus(newPerm: Term, newPermExp: Option[ast.Exp]) = + withPerm(PermMinus(perm, newPerm), newPermExp.map(npe => ast.PermSub(permExp.get, npe)())) + override def permPlus(newPerm: Term, newPermExp: Option[ast.Exp]) = + withPerm(PermPlus(perm, newPerm), newPermExp.map(npe => ast.PermAdd(permExp.get, npe)())) override def withPerm(newPerm: Term, newPermExp: Option[ast.Exp]) = MagicWandChunk(id, bindings, args, argsExp, snap, newPerm, newPermExp) + override def withSnap(newSnap: Term) = newSnap match { case s: MagicWandSnapshot => MagicWandChunk(id, bindings, args, argsExp, s, perm, permExp) case _ => sys.error(s"MagicWand snapshot has to be of type MagicWandSnapshot but found ${newSnap.getClass}") diff --git a/src/main/scala/state/State.scala b/src/main/scala/state/State.scala index 314edc6f..25f9e5fd 100644 --- a/src/main/scala/state/State.scala +++ b/src/main/scala/state/State.scala @@ -280,7 +280,7 @@ object State { h map (c => { c match { case c: GeneralChunk => - c.withPerm(Ite(cond, c.perm, NoPerm), condExp.map(ce => ast.CondExp(ce, c.permExp.get, ast.NoPerm()())())) + c.applyCondition(cond, condExp) case _ => sys.error("Chunk type not conditionalizable.") } })