QP chunk merging (from master branch, thanks Alex), and immediately c…

…alling merge whenever adding chunks in more places
viperproject · Oct 18, 2024 · a54023d · a54023d
1 parent ff2f900
commit a54023d
Show file tree

Hide file tree

Showing 11 changed files with 416 additions and 92 deletions.
diff --git a/src/main/scala/interfaces/state/Chunks.scala b/src/main/scala/interfaces/state/Chunks.scala
@@ -17,20 +17,29 @@ trait GeneralChunk extends Chunk {
   val resourceID: ResourceID
   val id: ChunkIdentifer
   val perm: Term
-  def withPerm(perm: Term): GeneralChunk
+  def applyCondition(newCond: Term): GeneralChunk
+  def permMinus(perm: Term): GeneralChunk
+  def permPlus(perm: Term): GeneralChunk
 }
 
 trait NonQuantifiedChunk extends GeneralChunk {
   val args: Seq[Term]
   val snap: Term
-  override def withPerm(perm: Term): NonQuantifiedChunk
+
+  override def applyCondition(newCond: Term): NonQuantifiedChunk
+  override def permMinus(perm: Term): NonQuantifiedChunk
+  override def permPlus(perm: Term): NonQuantifiedChunk
+  def withPerm(perm: Term): NonQuantifiedChunk
   def withSnap(snap: Term): NonQuantifiedChunk
 }
 
 trait QuantifiedChunk extends GeneralChunk {
   val quantifiedVars: Seq[Var]
   def snapshotMap: Term
   def valueAt(arguments: Seq[Term]): Term
-  override def withPerm(perm: Term): QuantifiedChunk
+
+  override def applyCondition(newCond: Term): QuantifiedChunk
+  override def permMinus(perm: Term): QuantifiedChunk
+  override def permPlus(perm: Term): QuantifiedChunk
   def withSnapshotMap(snap: Term): QuantifiedChunk
 }
diff --git 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
 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
@@ -58,40 +58,39 @@ 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),
         "predicate" -> JsString(id.toString),
         "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/Executor.scala b/src/main/scala/rules/Executor.scala
@@ -478,7 +478,8 @@ object executor extends ExecutionRules {
                 val ch = quantifiedChunkSupporter.createSingletonQuantifiedChunk(Seq(`?r`), field, Seq(tRcvr), FullPerm, sm, s.program)
                 if (s3.heapDependentTriggers.contains(field))
                   v3.decider.assume(FieldTrigger(field.name, sm, tRcvr))
-                Q(s3.copy(h = h3 + ch), v3)
+                val (fr4, h4) = v3.stateConsolidator(s3).merge(s3.functionRecorder, h3, ch, v3)
+                Q(s3.copy(h = h4, functionRecorder = fr4), v3)
               }
             )
           }))