Merge pull request #860 from superaxander/qp-consolidation

Consolidating quantified field and predicate chunks

Author: marcoeilers

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
 }

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

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

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)