From 3c9f4184e332bb6cee7dba12461bab9bb2d007e9 Mon Sep 17 00:00:00 2001 From: Alexander Stekelenburg Date: Fri, 12 Jul 2024 11:32:18 +0200 Subject: [PATCH 1/5] Implement merging/state consolidation for quantified field and predicate chunks --- src/main/scala/interfaces/state/Chunks.scala | 9 + .../records/data/SingleMergeRecord.scala | 6 +- .../logger/writer/SymbExLogReportWriter.scala | 6 +- src/main/scala/rules/ChunkSupporter.scala | 11 -- .../scala/rules/QuantifiedChunkSupport.scala | 186 ++++++++++++++++-- src/main/scala/rules/StateConsolidator.scala | 61 +++--- src/main/scala/state/Chunks.scala | 38 +++- src/main/scala/state/State.scala | 2 +- 8 files changed, 251 insertions(+), 68 deletions(-) diff --git a/src/main/scala/interfaces/state/Chunks.scala b/src/main/scala/interfaces/state/Chunks.scala index 201c76eeb..521ed7aca 100644 --- a/src/main/scala/interfaces/state/Chunks.scala +++ b/src/main/scala/interfaces/state/Chunks.scala @@ -17,12 +17,18 @@ trait GeneralChunk extends Chunk { val resourceID: ResourceID val id: ChunkIdentifer val perm: Term + def applyCondition(newCond: Term): GeneralChunk + def permMinus(perm: Term): GeneralChunk + def permPlus(perm: Term): GeneralChunk def withPerm(perm: Term): GeneralChunk } trait NonQuantifiedChunk extends GeneralChunk { val args: Seq[Term] val snap: Term + override def applyCondition(newCond: Term): NonQuantifiedChunk + override def permMinus(perm: Term): NonQuantifiedChunk + override def permPlus(perm: Term): NonQuantifiedChunk override def withPerm(perm: Term): NonQuantifiedChunk def withSnap(snap: Term): NonQuantifiedChunk } @@ -31,6 +37,9 @@ trait QuantifiedChunk extends GeneralChunk { val quantifiedVars: Seq[Var] def snapshotMap: Term def valueAt(arguments: Seq[Term]): Term + override def applyCondition(newCond: Term): QuantifiedChunk + override def permMinus(perm: Term): QuantifiedChunk + override def permPlus(perm: Term): QuantifiedChunk override def withPerm(perm: Term): 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 7137aff56..aa8467dc4 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 8b3d9928f..1b22e9af3 100644 --- a/src/main/scala/logger/writer/SymbExLogReportWriter.scala +++ b/src/main/scala/logger/writer/SymbExLogReportWriter.scala @@ -58,11 +58,12 @@ object SymbExLogReportWriter { "perm" -> TermWriter.toJSON(perm) ) - case QuantifiedFieldChunk(id, fvf, perm, invs, cond, receiver, hints) => + case QuantifiedFieldChunk(id, fvf, condition, perm, invs, cond, 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), @@ -70,12 +71,13 @@ object SymbExLogReportWriter { "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, cond, 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), diff --git a/src/main/scala/rules/ChunkSupporter.scala b/src/main/scala/rules/ChunkSupporter.scala index deb756d8c..609d39bd1 100644 --- a/src/main/scala/rules/ChunkSupporter.scala +++ b/src/main/scala/rules/ChunkSupporter.scala @@ -49,12 +49,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) @@ -243,11 +237,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 4f8902dbc..6d781db9a 100644 --- a/src/main/scala/rules/QuantifiedChunkSupport.scala +++ b/src/main/scala/rules/QuantifiedChunkSupport.scala @@ -22,7 +22,7 @@ import viper.silicon.state.terms.perms.IsPositive import viper.silicon.state.terms.perms.BigPermSum 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.notNothing.NotNothing import viper.silicon.verifier.Verifier import viper.silver.reporter.InternalWarningMessage @@ -205,6 +205,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 { @@ -225,9 +254,6 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { .zip(arguments) .map { case (x, a) => x === a }) - val conditionalizedPermissions = - Ite(condition, permissions, NoPerm) - val hints = extractHints(None, arguments) genericQuantifiedChunk( @@ -235,9 +261,9 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { resource, arguments, sm, - conditionalizedPermissions, + condition, + permissions, None, - Some(conditionalizedPermissions), Some(arguments), hints, program) @@ -271,11 +297,8 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { val qvarsToInversesOfCodomain = inverseFunctions.qvarsToInversesOf(codomainQVars) - val conditionalizedPermissions = - Ite( - And(And(imagesOfCodomain), condition.replace(qvarsToInversesOfCodomain)), - permissions.replace(qvarsToInversesOfCodomain), - NoPerm) + val cond = And(And(imagesOfCodomain), condition.replace(qvarsToInversesOfCodomain)) + val perms = permissions.replace(qvarsToInversesOfCodomain) val hints = extractHints(Some(condition), arguments) @@ -285,9 +308,9 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { resource, arguments, sm, - conditionalizedPermissions, + cond, + perms, Some(inverseFunctions), - Some(conditionalizedPermissions), None, hints, program) @@ -323,14 +346,15 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { resource: ast.Resource, arguments: Seq[Term], sm: Term, + condition: Term, permissions: Term, optInverseFunctions: Option[InverseFunctions], - optInitialCond: Option[Term], optSingletonArguments: Option[Seq[Term]], hints: Seq[Term], program: ast.Program) : QuantifiedBasicChunk = { + val conditionalizedPermissions = Ite(condition, permissions, NoPerm) resource match { case field: ast.Field => assert(arguments.length == 1) @@ -339,9 +363,10 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { QuantifiedFieldChunk( BasicChunkIdentifier(field.name), sm, + condition, permissions, optInverseFunctions, - optInitialCond, + Some(conditionalizedPermissions), optSingletonArguments.map(_.head), hints) @@ -350,9 +375,10 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { BasicChunkIdentifier(predicate.name), codomainQVars, sm, + condition, permissions, optInverseFunctions, - optInitialCond, + Some(conditionalizedPermissions), optSingletonArguments, hints) @@ -361,9 +387,9 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { MagicWandIdentifier(wand, program), codomainQVars, sm, - permissions, + conditionalizedPermissions, optInverseFunctions, - optInitialCond, + Some(conditionalizedPermissions), optSingletonArguments, hints) @@ -1434,11 +1460,10 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { v.decider.assume(permissionConstraint) remainingChunks = - remainingChunks :+ ithChunk.withPerm(PermMinus(ithChunk.perm, ithPTaken)) + remainingChunks :+ ithChunk.permMinus(ithPTaken) } 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()) @@ -1446,7 +1471,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { remainingChunks = remainingChunks :+ ithChunk } else { remainingChunks = - remainingChunks :+ ithChunk.withPerm(PermMinus(ithChunk.perm, ithPTaken)) + remainingChunks :+ ithChunk.permMinus(ithPTaken) } } } @@ -1769,6 +1794,125 @@ 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.invs.get.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.invs.get.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 + v.decider.assume(equalityTerm) + } + 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.invs.get.condition) + case qpc: QuantifiedPredicateChunk if qpc.invs.isDefined => + Some(qpc.invs.get.invertibles, qpc.quantifiedVars, qpc.invs.get.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 + v.decider.assume(equalityTerm) + } + 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) + 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) + 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 49e22100c..6467ecf4d 100644 --- a/src/main/scala/rules/StateConsolidator.scala +++ b/src/main/scala/rules/StateConsolidator.scala @@ -64,13 +64,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 @@ -92,10 +90,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) v.decider.assume(interpreter.buildPathConditionsForChunk(ch, resource.instanceProperties)) } @@ -105,7 +103,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, @@ -128,36 +126,34 @@ class DefaultStateConsolidator(protected val config: Config) extends StateConsol def merge(fr1: FunctionRecorder, 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) val interpreter = new NonQuantifiedPropertyInterpreter(mergedChunks, v) - newlyAddedChunks foreach { ch => + newlyAddedChunks.filter(_.isInstanceOf[BasicChunk]) foreach { case ch: BasicChunk => val resource = Resources.resourceDescriptions(ch.resourceID) v.decider.assume(interpreter.buildPathConditionsForChunk(ch, resource.instanceProperties)) } 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 @@ -167,7 +163,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)) => @@ -183,14 +179,35 @@ 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) = (chunk1, chunk2) match { case (BasicChunk(rid1, id1, args1, snap1, perm1), BasicChunk(_, _, _, snap2, perm2)) => val (fr2, combinedSnap, snapEq) = combineSnapshots(fr1, snap1, snap2, perm1, perm2, v) Some(fr2, BasicChunk(rid1, id1, args1, combinedSnap, PermPlus(perm1, perm2)), snapEq) - case (_, _) => + case (l@QuantifiedFieldChunk(id1, fvf1, condition1, perm1, invs1, initialCond1, _, hints1), r@QuantifiedFieldChunk(_, fvf2, _, perm2, _, _, singletonRcvr2, 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) + // TODO: Deal with hints + // TODO: Store multiple known singleton receivers for better heuristics? + Some(fr2, QuantifiedFieldChunk(id1, combinedSnap, condition1, PermPlus(perm1, perm2), invs1, initialCond1, singletonRcvr2, hints1), snapEq) + case (l@QuantifiedPredicateChunk(id1, qVars1, psf1, _, perm1, _, _, _, hints1), r@QuantifiedPredicateChunk(_, qVars2, psf2, condition2, perm2, initialCond2, invs2, singletonArgs2, hints2)) => + val (fr2, combinedSnap, snapEq) = quantifiedChunkSupporter.combinePredicateSnapshotMaps(fr1, id1.name, qVars2, psf1, psf2, l.perm.replace(qVars1, qVars2), r.perm, v) + + Some(fr2, QuantifiedPredicateChunk(id1, qVars2, combinedSnap, condition2, PermPlus(perm1.replace(qVars1, qVars2), perm2), initialCond2, invs2, singletonArgs2, hints2), snapEq) + case (l, r) => None } diff --git a/src/main/scala/state/Chunks.scala b/src/main/scala/state/Chunks.scala index 44b907031..e890646ce 100644 --- a/src/main/scala/state/Chunks.scala +++ b/src/main/scala/state/Chunks.scala @@ -40,6 +40,9 @@ 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) = withPerm(Ite(newCond, perm, NoPerm)) + override def permMinus(newPerm: Term) = withPerm(PermMinus(perm, newPerm)) + override def permPlus(newPerm: Term) = withPerm(PermPlus(perm, newPerm)) override def withPerm(newPerm: Term) = BasicChunk(resourceID, id, args, snap, newPerm) override def withSnap(newSnap: Term) = BasicChunk(resourceID, id, args, newSnap, perm) @@ -51,6 +54,9 @@ case class BasicChunk(resourceID: BaseID, sealed trait QuantifiedBasicChunk extends QuantifiedChunk { override val id: ChunkIdentifer + override def applyCondition(newCond: Term): QuantifiedBasicChunk + override def permMinus(perm: Term): QuantifiedBasicChunk + override def permPlus(perm: Term): QuantifiedBasicChunk override def withPerm(perm: Term): QuantifiedBasicChunk override def withSnapshotMap(snap: Term): QuantifiedBasicChunk def singletonArguments: Option[Seq[Term]] @@ -64,7 +70,8 @@ sealed trait QuantifiedBasicChunk extends QuantifiedChunk { */ case class QuantifiedFieldChunk(id: BasicChunkIdentifier, fvf: Term, - perm: Term, + condition: Term, + permValue: Term, invs: Option[InverseFunctions], initialCond: Option[Term], singletonRcvr: Option[Term], @@ -73,10 +80,11 @@ 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 def snapshotMap: Term = fvf override def singletonArguments: Option[Seq[Term]] = singletonRcvr.map(Seq(_)) @@ -89,8 +97,11 @@ case class QuantifiedFieldChunk(id: BasicChunkIdentifier, Lookup(id.name, fvf, arguments.head) } - override def withPerm(newPerm: Term) = QuantifiedFieldChunk(id, fvf, newPerm, invs, initialCond, singletonRcvr, hints) - override def withSnapshotMap(newFvf: Term) = QuantifiedFieldChunk(id, newFvf, perm, invs, initialCond, singletonRcvr, hints) + override def applyCondition(newCond: Term) = QuantifiedFieldChunk(id, fvf, terms.And(newCond, condition), permValue, invs, initialCond, singletonRcvr, hints) + override def permMinus(newPerm: Term) = QuantifiedFieldChunk(id, fvf, condition, PermMinus(permValue, newPerm), invs, initialCond, singletonRcvr, hints) + override def permPlus(newPerm: Term) = QuantifiedFieldChunk(id, fvf, condition, PermPlus(permValue, newPerm), invs, initialCond, singletonRcvr, hints) + override def withPerm(newPerm: Term) = throw new RuntimeException("Should not be used with quantified field chunks") + override def withSnapshotMap(newFvf: Term) = QuantifiedFieldChunk(id, newFvf, condition, permValue, invs, initialCond, singletonRcvr, hints) override lazy val toString = s"${terms.Forall} ${`?r`} :: ${`?r`}.$id -> $fvf # $perm" } @@ -98,7 +109,8 @@ case class QuantifiedFieldChunk(id: BasicChunkIdentifier, case class QuantifiedPredicateChunk(id: BasicChunkIdentifier, quantifiedVars: Seq[Var], psf: Term, - perm: Term, + condition: Term, + permValue: Term, invs: Option[InverseFunctions], initialCond: Option[Term], singletonArgs: Option[Seq[Term]], @@ -106,17 +118,21 @@ case class QuantifiedPredicateChunk(id: BasicChunkIdentifier, 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 def snapshotMap: Term = psf override def singletonArguments: Option[Seq[Term]] = singletonArgs override def valueAt(args: Seq[Term]) = PredicateLookup(id.name, psf, args) - override def withPerm(newPerm: Term) = QuantifiedPredicateChunk(id, quantifiedVars, psf, newPerm, invs, initialCond, singletonArgs, hints) - override def withSnapshotMap(newPsf: Term) = QuantifiedPredicateChunk(id, quantifiedVars, newPsf, perm, invs, initialCond, singletonArgs, hints) + override def applyCondition(newCond: Term) = QuantifiedPredicateChunk(id, quantifiedVars, psf, terms.And(newCond, condition), permValue, invs, initialCond, singletonArgs, hints) + override def permMinus(newPerm: Term) = QuantifiedPredicateChunk(id, quantifiedVars, psf, condition, PermMinus(permValue, newPerm), invs, initialCond, singletonArgs, hints) + override def permPlus(newPerm: Term) = QuantifiedPredicateChunk(id, quantifiedVars, psf, condition, PermPlus(permValue, newPerm), invs, initialCond, singletonArgs, hints) + override def withPerm(newPerm: Term) = throw new RuntimeException("Should not be used with quantified predicate chunks") + override def withSnapshotMap(newPsf: Term) = QuantifiedPredicateChunk(id, quantifiedVars, newPsf, condition, permValue, invs, initialCond, singletonArgs, hints) override lazy val toString = s"${terms.Forall} ${quantifiedVars.mkString(",")} :: $id(${quantifiedVars.mkString(",")}) -> $psf # $perm" } @@ -141,6 +157,9 @@ case class QuantifiedMagicWandChunk(id: MagicWandIdentifier, override def valueAt(args: Seq[Term]) = PredicateLookup(id.toString, wsf, args) + override def applyCondition(newCond: Term) = withPerm(Ite(newCond, perm, NoPerm)) + override def permMinus(newPerm: Term) = withPerm(PermMinus(perm, newPerm)) + override def permPlus(newPerm: Term) = withPerm(PermPlus(perm, newPerm)) override def withPerm(newPerm: Term) = QuantifiedMagicWandChunk(id, quantifiedVars, wsf, newPerm, invs, initialCond, singletonArgs, hints) override def withSnapshotMap(newWsf: Term) = QuantifiedMagicWandChunk(id, quantifiedVars, newWsf, perm, invs, initialCond, singletonArgs, hints) @@ -175,6 +194,9 @@ case class MagicWandChunk(id: MagicWandIdentifier, override val resourceID = MagicWandID + override def applyCondition(newCond: Term) = withPerm(Ite(newCond, perm, NoPerm)) + override def permMinus(newPerm: Term) = withPerm(PermMinus(perm, newPerm)) + override def permPlus(newPerm: Term) = withPerm(PermPlus(perm, newPerm)) override def withPerm(newPerm: Term) = MagicWandChunk(id, bindings, args, snap, newPerm) override def withSnap(newSnap: Term) = newSnap match { case s: MagicWandSnapshot => MagicWandChunk(id, bindings, args, s, perm) diff --git a/src/main/scala/state/State.scala b/src/main/scala/state/State.scala index 03c596dca..a235caa50 100644 --- a/src/main/scala/state/State.scala +++ b/src/main/scala/state/State.scala @@ -267,7 +267,7 @@ object State { h map (c => { c match { case c: GeneralChunk => - c.withPerm(Ite(cond, c.perm, NoPerm)) + c.applyCondition(cond) case _ => sys.error("Chunk type not conditionalizable.") } }) From c63989f64eb759f33bde68c330ce07d6e34134fa Mon Sep 17 00:00:00 2001 From: Alexander Stekelenburg Date: Thu, 18 Jul 2024 09:57:26 +0200 Subject: [PATCH 2/5] Compare condition stored in chunk instead of its inverses since the condition may have been changed --- src/main/scala/rules/QuantifiedChunkSupport.scala | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/main/scala/rules/QuantifiedChunkSupport.scala b/src/main/scala/rules/QuantifiedChunkSupport.scala index 6d781db9a..d9e0641ee 100644 --- a/src/main/scala/rules/QuantifiedChunkSupport.scala +++ b/src/main/scala/rules/QuantifiedChunkSupport.scala @@ -1797,11 +1797,11 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { 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.invs.get.condition) + 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.invs.get.condition) + Left(qpc.invs.get.invertibles, qpc.quantifiedVars, qpc.condition) case qpc: QuantifiedPredicateChunk if qpc.singletonArguments.isDefined => Right(qpc.singletonArguments.get) case _ => return None @@ -1838,9 +1838,9 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { relevantChunks.find { ch => val chunkInfo = ch match { case qfc: QuantifiedFieldChunk if qfc.invs.isDefined => - Some(qfc.invs.get.invertibles, qfc.quantifiedVars, qfc.invs.get.condition) + Some(qfc.invs.get.invertibles, qfc.quantifiedVars, qfc.condition) case qpc: QuantifiedPredicateChunk if qpc.invs.isDefined => - Some(qpc.invs.get.invertibles, qpc.quantifiedVars, qpc.invs.get.condition) + Some(qpc.invs.get.invertibles, qpc.quantifiedVars, qpc.condition) case _ => None } chunkInfo match { From 4dbf41c8447135095eb365f5440719a93f24b365 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Thu, 12 Sep 2024 16:44:01 +0200 Subject: [PATCH 3/5] Pick non-empty hints --- src/main/scala/rules/StateConsolidator.scala | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/src/main/scala/rules/StateConsolidator.scala b/src/main/scala/rules/StateConsolidator.scala index 6467ecf4d..f583fb065 100644 --- a/src/main/scala/rules/StateConsolidator.scala +++ b/src/main/scala/rules/StateConsolidator.scala @@ -195,15 +195,13 @@ class DefaultStateConsolidator(protected val config: Config) extends StateConsol val (fr2, combinedSnap, snapEq) = combineSnapshots(fr1, snap1, snap2, perm1, perm2, v) Some(fr2, BasicChunk(rid1, id1, args1, combinedSnap, PermPlus(perm1, perm2)), snapEq) - case (l@QuantifiedFieldChunk(id1, fvf1, condition1, perm1, invs1, initialCond1, _, hints1), r@QuantifiedFieldChunk(_, fvf2, _, perm2, _, _, singletonRcvr2, hints2)) => + case (l@QuantifiedFieldChunk(id1, fvf1, condition1, perm1, invs1, initialCond1, singletonRcvr1, hints1), r@QuantifiedFieldChunk(_, fvf2, _, perm2, _, _, _, 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) - // TODO: Deal with hints - // TODO: Store multiple known singleton receivers for better heuristics? - Some(fr2, QuantifiedFieldChunk(id1, combinedSnap, condition1, PermPlus(perm1, perm2), invs1, initialCond1, singletonRcvr2, hints1), snapEq) - case (l@QuantifiedPredicateChunk(id1, qVars1, psf1, _, perm1, _, _, _, hints1), r@QuantifiedPredicateChunk(_, qVars2, psf2, condition2, perm2, initialCond2, invs2, singletonArgs2, hints2)) => + Some(fr2, QuantifiedFieldChunk(id1, combinedSnap, condition1, PermPlus(perm1, perm2), invs1, initialCond1, singletonRcvr1, if (hints1.nonEmpty) hints1 else hints2), snapEq) + case (l@QuantifiedPredicateChunk(id1, qVars1, psf1, _, perm1, _, _, singletonArgs1, hints1), r@QuantifiedPredicateChunk(_, qVars2, psf2, condition2, perm2, initialCond2, invs2, singletonArgs2, hints2)) => val (fr2, combinedSnap, snapEq) = quantifiedChunkSupporter.combinePredicateSnapshotMaps(fr1, id1.name, qVars2, psf1, psf2, l.perm.replace(qVars1, qVars2), r.perm, v) Some(fr2, QuantifiedPredicateChunk(id1, qVars2, combinedSnap, condition2, PermPlus(perm1.replace(qVars1, qVars2), perm2), initialCond2, invs2, singletonArgs2, hints2), snapEq) From 69cc8aaf075d12388f9236dca262189e322243b9 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Thu, 12 Sep 2024 16:53:16 +0200 Subject: [PATCH 4/5] Remove unused initialCond field --- .../logger/writer/SymbExLogReportWriter.scala | 9 +++----- .../scala/rules/QuantifiedChunkSupport.scala | 3 --- src/main/scala/rules/StateConsolidator.scala | 12 +++++----- src/main/scala/state/Chunks.scala | 23 ++++++++----------- 4 files changed, 19 insertions(+), 28 deletions(-) diff --git a/src/main/scala/logger/writer/SymbExLogReportWriter.scala b/src/main/scala/logger/writer/SymbExLogReportWriter.scala index 1b22e9af3..bff6e301b 100644 --- a/src/main/scala/logger/writer/SymbExLogReportWriter.scala +++ b/src/main/scala/logger/writer/SymbExLogReportWriter.scala @@ -58,7 +58,7 @@ object SymbExLogReportWriter { "perm" -> TermWriter.toJSON(perm) ) - case QuantifiedFieldChunk(id, fvf, condition, perm, invs, cond, receiver, hints) => + case QuantifiedFieldChunk(id, fvf, condition, perm, invs, receiver, hints) => JsObject( "type" -> JsString("quantified_field_chunk"), "field" -> JsString(id.toString), @@ -66,12 +66,11 @@ object SymbExLogReportWriter { "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, condition, 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), @@ -80,12 +79,11 @@ object SymbExLogReportWriter { "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), @@ -93,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/QuantifiedChunkSupport.scala b/src/main/scala/rules/QuantifiedChunkSupport.scala index d9e0641ee..3d3a403e2 100644 --- a/src/main/scala/rules/QuantifiedChunkSupport.scala +++ b/src/main/scala/rules/QuantifiedChunkSupport.scala @@ -366,7 +366,6 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { condition, permissions, optInverseFunctions, - Some(conditionalizedPermissions), optSingletonArguments.map(_.head), hints) @@ -378,7 +377,6 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { condition, permissions, optInverseFunctions, - Some(conditionalizedPermissions), optSingletonArguments, hints) @@ -389,7 +387,6 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { sm, conditionalizedPermissions, optInverseFunctions, - Some(conditionalizedPermissions), optSingletonArguments, hints) diff --git a/src/main/scala/rules/StateConsolidator.scala b/src/main/scala/rules/StateConsolidator.scala index f583fb065..6f1ba9e05 100644 --- a/src/main/scala/rules/StateConsolidator.scala +++ b/src/main/scala/rules/StateConsolidator.scala @@ -190,22 +190,22 @@ class DefaultStateConsolidator(protected val config: Config) extends StateConsol // 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: Chunk, chunk2: Chunk, 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, snap1, perm1), BasicChunk(_, _, _, snap2, perm2)) => val (fr2, combinedSnap, snapEq) = combineSnapshots(fr1, snap1, snap2, perm1, perm2, v) Some(fr2, BasicChunk(rid1, id1, args1, combinedSnap, PermPlus(perm1, perm2)), snapEq) - case (l@QuantifiedFieldChunk(id1, fvf1, condition1, perm1, invs1, initialCond1, singletonRcvr1, hints1), r@QuantifiedFieldChunk(_, fvf2, _, perm2, _, _, _, hints2)) => + case (l@QuantifiedFieldChunk(id1, fvf1, condition1, perm1, invs1, singletonRcvr1, hints1), r@QuantifiedFieldChunk(_, fvf2, _, perm2, _, _, 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) - Some(fr2, QuantifiedFieldChunk(id1, combinedSnap, condition1, PermPlus(perm1, perm2), invs1, initialCond1, singletonRcvr1, if (hints1.nonEmpty) hints1 else hints2), snapEq) - case (l@QuantifiedPredicateChunk(id1, qVars1, psf1, _, perm1, _, _, singletonArgs1, hints1), r@QuantifiedPredicateChunk(_, qVars2, psf2, condition2, perm2, initialCond2, invs2, singletonArgs2, hints2)) => + Some(fr2, QuantifiedFieldChunk(id1, combinedSnap, condition1, PermPlus(perm1, perm2), invs1, singletonRcvr1, if (hints1.nonEmpty) hints1 else hints2), snapEq) + case (l@QuantifiedPredicateChunk(id1, qVars1, psf1, _, perm1, _, _, _), r@QuantifiedPredicateChunk(_, qVars2, psf2, condition2, perm2, invs2, singletonArgs2, hints2)) => val (fr2, combinedSnap, snapEq) = quantifiedChunkSupporter.combinePredicateSnapshotMaps(fr1, id1.name, qVars2, psf1, psf2, l.perm.replace(qVars1, qVars2), r.perm, v) - Some(fr2, QuantifiedPredicateChunk(id1, qVars2, combinedSnap, condition2, PermPlus(perm1.replace(qVars1, qVars2), perm2), initialCond2, invs2, singletonArgs2, hints2), snapEq) - case (l, r) => + Some(fr2, QuantifiedPredicateChunk(id1, qVars2, combinedSnap, condition2, PermPlus(perm1.replace(qVars1, qVars2), perm2), invs2, singletonArgs2, hints2), snapEq) + case _ => None } diff --git a/src/main/scala/state/Chunks.scala b/src/main/scala/state/Chunks.scala index e890646ce..53a657352 100644 --- a/src/main/scala/state/Chunks.scala +++ b/src/main/scala/state/Chunks.scala @@ -73,7 +73,6 @@ case class QuantifiedFieldChunk(id: BasicChunkIdentifier, condition: Term, permValue: Term, invs: Option[InverseFunctions], - initialCond: Option[Term], singletonRcvr: Option[Term], hints: Seq[Term] = Nil) extends QuantifiedBasicChunk { @@ -97,11 +96,11 @@ case class QuantifiedFieldChunk(id: BasicChunkIdentifier, Lookup(id.name, fvf, arguments.head) } - override def applyCondition(newCond: Term) = QuantifiedFieldChunk(id, fvf, terms.And(newCond, condition), permValue, invs, initialCond, singletonRcvr, hints) - override def permMinus(newPerm: Term) = QuantifiedFieldChunk(id, fvf, condition, PermMinus(permValue, newPerm), invs, initialCond, singletonRcvr, hints) - override def permPlus(newPerm: Term) = QuantifiedFieldChunk(id, fvf, condition, PermPlus(permValue, newPerm), invs, initialCond, singletonRcvr, hints) + override def applyCondition(newCond: Term) = QuantifiedFieldChunk(id, fvf, terms.And(newCond, condition), permValue, invs, singletonRcvr, hints) + override def permMinus(newPerm: Term) = QuantifiedFieldChunk(id, fvf, condition, PermMinus(permValue, newPerm), invs, singletonRcvr, hints) + override def permPlus(newPerm: Term) = QuantifiedFieldChunk(id, fvf, condition, PermPlus(permValue, newPerm), invs, singletonRcvr, hints) override def withPerm(newPerm: Term) = throw new RuntimeException("Should not be used with quantified field chunks") - override def withSnapshotMap(newFvf: Term) = QuantifiedFieldChunk(id, newFvf, condition, permValue, invs, initialCond, singletonRcvr, hints) + override def withSnapshotMap(newFvf: Term) = QuantifiedFieldChunk(id, newFvf, condition, permValue, invs, singletonRcvr, hints) override lazy val toString = s"${terms.Forall} ${`?r`} :: ${`?r`}.$id -> $fvf # $perm" } @@ -112,7 +111,6 @@ case class QuantifiedPredicateChunk(id: BasicChunkIdentifier, condition: Term, permValue: Term, invs: Option[InverseFunctions], - initialCond: Option[Term], singletonArgs: Option[Seq[Term]], hints: Seq[Term] = Nil) extends QuantifiedBasicChunk { @@ -128,11 +126,11 @@ case class QuantifiedPredicateChunk(id: BasicChunkIdentifier, override def valueAt(args: Seq[Term]) = PredicateLookup(id.name, psf, args) - override def applyCondition(newCond: Term) = QuantifiedPredicateChunk(id, quantifiedVars, psf, terms.And(newCond, condition), permValue, invs, initialCond, singletonArgs, hints) - override def permMinus(newPerm: Term) = QuantifiedPredicateChunk(id, quantifiedVars, psf, condition, PermMinus(permValue, newPerm), invs, initialCond, singletonArgs, hints) - override def permPlus(newPerm: Term) = QuantifiedPredicateChunk(id, quantifiedVars, psf, condition, PermPlus(permValue, newPerm), invs, initialCond, singletonArgs, hints) + override def applyCondition(newCond: Term) = QuantifiedPredicateChunk(id, quantifiedVars, psf, terms.And(newCond, condition), permValue, invs, singletonArgs, hints) + override def permMinus(newPerm: Term) = QuantifiedPredicateChunk(id, quantifiedVars, psf, condition, PermMinus(permValue, newPerm), invs, singletonArgs, hints) + override def permPlus(newPerm: Term) = QuantifiedPredicateChunk(id, quantifiedVars, psf, condition, PermPlus(permValue, newPerm), invs, singletonArgs, hints) override def withPerm(newPerm: Term) = throw new RuntimeException("Should not be used with quantified predicate chunks") - override def withSnapshotMap(newPsf: Term) = QuantifiedPredicateChunk(id, quantifiedVars, newPsf, condition, permValue, invs, initialCond, singletonArgs, hints) + override def withSnapshotMap(newPsf: Term) = QuantifiedPredicateChunk(id, quantifiedVars, newPsf, condition, permValue, invs, singletonArgs, hints) override lazy val toString = s"${terms.Forall} ${quantifiedVars.mkString(",")} :: $id(${quantifiedVars.mkString(",")}) -> $psf # $perm" } @@ -142,7 +140,6 @@ case class QuantifiedMagicWandChunk(id: MagicWandIdentifier, wsf: Term, perm: Term, invs: Option[InverseFunctions], - initialCond: Option[Term], singletonArgs: Option[Seq[Term]], hints: Seq[Term] = Nil) extends QuantifiedBasicChunk { @@ -160,8 +157,8 @@ case class QuantifiedMagicWandChunk(id: MagicWandIdentifier, override def applyCondition(newCond: Term) = withPerm(Ite(newCond, perm, NoPerm)) override def permMinus(newPerm: Term) = withPerm(PermMinus(perm, newPerm)) override def permPlus(newPerm: Term) = withPerm(PermPlus(perm, newPerm)) - override def withPerm(newPerm: Term) = QuantifiedMagicWandChunk(id, quantifiedVars, wsf, newPerm, invs, initialCond, singletonArgs, hints) - override def withSnapshotMap(newWsf: Term) = QuantifiedMagicWandChunk(id, quantifiedVars, newWsf, perm, invs, initialCond, singletonArgs, hints) + override def withPerm(newPerm: Term) = QuantifiedMagicWandChunk(id, quantifiedVars, wsf, newPerm, invs, singletonArgs, hints) + override def withSnapshotMap(newWsf: Term) = QuantifiedMagicWandChunk(id, quantifiedVars, newWsf, perm, invs, singletonArgs, hints) override lazy val toString = s"${terms.Forall} ${quantifiedVars.mkString(",")} :: $id(${quantifiedVars.mkString(",")}) -> $wsf # $perm" } From 7468240773043d81ead16072c2386452d701a5bd Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Thu, 12 Sep 2024 16:56:12 +0200 Subject: [PATCH 5/5] Remove withPerm from interface of quantified chunks --- src/main/scala/interfaces/state/Chunks.scala | 4 +--- src/main/scala/state/Chunks.scala | 5 +---- 2 files changed, 2 insertions(+), 7 deletions(-) diff --git a/src/main/scala/interfaces/state/Chunks.scala b/src/main/scala/interfaces/state/Chunks.scala index 521ed7aca..6923efaaa 100644 --- a/src/main/scala/interfaces/state/Chunks.scala +++ b/src/main/scala/interfaces/state/Chunks.scala @@ -20,7 +20,6 @@ trait GeneralChunk extends Chunk { def applyCondition(newCond: Term): GeneralChunk def permMinus(perm: Term): GeneralChunk def permPlus(perm: Term): GeneralChunk - def withPerm(perm: Term): GeneralChunk } trait NonQuantifiedChunk extends GeneralChunk { @@ -29,7 +28,7 @@ trait NonQuantifiedChunk extends GeneralChunk { override def applyCondition(newCond: Term): NonQuantifiedChunk override def permMinus(perm: Term): NonQuantifiedChunk override def permPlus(perm: Term): NonQuantifiedChunk - override def withPerm(perm: Term): NonQuantifiedChunk + def withPerm(perm: Term): NonQuantifiedChunk def withSnap(snap: Term): NonQuantifiedChunk } @@ -40,6 +39,5 @@ trait QuantifiedChunk extends GeneralChunk { override def applyCondition(newCond: Term): QuantifiedChunk override def permMinus(perm: Term): QuantifiedChunk override def permPlus(perm: Term): QuantifiedChunk - override def withPerm(perm: Term): QuantifiedChunk def withSnapshotMap(snap: Term): QuantifiedChunk } \ No newline at end of file diff --git a/src/main/scala/state/Chunks.scala b/src/main/scala/state/Chunks.scala index 53a657352..94b044ab5 100644 --- a/src/main/scala/state/Chunks.scala +++ b/src/main/scala/state/Chunks.scala @@ -57,7 +57,6 @@ sealed trait QuantifiedBasicChunk extends QuantifiedChunk { override def applyCondition(newCond: Term): QuantifiedBasicChunk override def permMinus(perm: Term): QuantifiedBasicChunk override def permPlus(perm: Term): QuantifiedBasicChunk - override def withPerm(perm: Term): QuantifiedBasicChunk override def withSnapshotMap(snap: Term): QuantifiedBasicChunk def singletonArguments: Option[Seq[Term]] def hints: Seq[Term] @@ -99,7 +98,6 @@ case class QuantifiedFieldChunk(id: BasicChunkIdentifier, override def applyCondition(newCond: Term) = QuantifiedFieldChunk(id, fvf, terms.And(newCond, condition), permValue, invs, singletonRcvr, hints) override def permMinus(newPerm: Term) = QuantifiedFieldChunk(id, fvf, condition, PermMinus(permValue, newPerm), invs, singletonRcvr, hints) override def permPlus(newPerm: Term) = QuantifiedFieldChunk(id, fvf, condition, PermPlus(permValue, newPerm), invs, singletonRcvr, hints) - override def withPerm(newPerm: Term) = throw new RuntimeException("Should not be used with quantified field chunks") override def withSnapshotMap(newFvf: Term) = QuantifiedFieldChunk(id, newFvf, condition, permValue, invs, singletonRcvr, hints) override lazy val toString = s"${terms.Forall} ${`?r`} :: ${`?r`}.$id -> $fvf # $perm" @@ -129,7 +127,6 @@ case class QuantifiedPredicateChunk(id: BasicChunkIdentifier, override def applyCondition(newCond: Term) = QuantifiedPredicateChunk(id, quantifiedVars, psf, terms.And(newCond, condition), permValue, invs, singletonArgs, hints) override def permMinus(newPerm: Term) = QuantifiedPredicateChunk(id, quantifiedVars, psf, condition, PermMinus(permValue, newPerm), invs, singletonArgs, hints) override def permPlus(newPerm: Term) = QuantifiedPredicateChunk(id, quantifiedVars, psf, condition, PermPlus(permValue, newPerm), invs, singletonArgs, hints) - override def withPerm(newPerm: Term) = throw new RuntimeException("Should not be used with quantified predicate chunks") override def withSnapshotMap(newPsf: Term) = QuantifiedPredicateChunk(id, quantifiedVars, newPsf, condition, permValue, invs, singletonArgs, hints) override lazy val toString = s"${terms.Forall} ${quantifiedVars.mkString(",")} :: $id(${quantifiedVars.mkString(",")}) -> $psf # $perm" @@ -157,7 +154,7 @@ case class QuantifiedMagicWandChunk(id: MagicWandIdentifier, override def applyCondition(newCond: Term) = withPerm(Ite(newCond, perm, NoPerm)) override def permMinus(newPerm: Term) = withPerm(PermMinus(perm, newPerm)) override def permPlus(newPerm: Term) = withPerm(PermPlus(perm, newPerm)) - override def withPerm(newPerm: Term) = QuantifiedMagicWandChunk(id, quantifiedVars, wsf, newPerm, invs, singletonArgs, hints) + def withPerm(newPerm: Term) = QuantifiedMagicWandChunk(id, quantifiedVars, wsf, newPerm, invs, singletonArgs, hints) override def withSnapshotMap(newWsf: Term) = QuantifiedMagicWandChunk(id, quantifiedVars, newWsf, perm, invs, singletonArgs, hints) override lazy val toString = s"${terms.Forall} ${quantifiedVars.mkString(",")} :: $id(${quantifiedVars.mkString(",")}) -> $wsf # $perm"