Fixing lots of issues

src/main/scala/rules/Evaluator.scala

@@ -191,7 +191,7 @@ object evaluator extends EvaluationRules {
            .setConstrainable(Seq(tVar), true)
         Q(s1, tVar, v)
 
-      case fa: ast.FieldAccess if Verifier.config.maskHeapMode() =>
+      case fa: ast.FieldAccess if Verifier.config.maskHeapMode() && s.qpFields.contains(fa.field) =>
         eval(s, fa.rcv, pve, v)((s1, tRcvr, v1) => {
           val resChunk = s.h.values.find(c => c.asInstanceOf[MaskHeapChunk].resource == fa.field).get.asInstanceOf[BasicMaskHeapChunk]
           val ve = pve dueTo InsufficientPermission(fa)
@@ -207,7 +207,7 @@ object evaluator extends EvaluationRules {
           }
         })
 
-      case pa: ast.PredicateAccess if Verifier.config.maskHeapMode() =>
+      case pa: ast.PredicateAccess if Verifier.config.maskHeapMode() && s.qpPredicates.contains(pa.res(s.program).asInstanceOf[ast.Predicate]) =>
         val pvef: ast.Exp => PartialVerificationError = _ => pve
         evals(s, pa.args, pvef, v)((s1, tArgs, v1) => {
           val resChunk = s.h.values.find(c => c.asInstanceOf[MaskHeapChunk].resource == pa.res(s.program)).get.asInstanceOf[BasicMaskHeapChunk]
@@ -800,16 +800,16 @@ object evaluator extends EvaluationRules {
               val (snapArgs, snapToRecord) = if (Verifier.config.heapFunctionEncoding()) {
                 val resources = maskHeapSupporter.getResourceSeq(func.pres, s4.program)
                 val args = resources.map(r => {
-                  val existingHeap = maskHeapSupporter.findMaskHeapChunkOptionally(s4.h, r)
+                  val existingHeap = maskHeapSupporter.findMaskHeapChunkOptionally(s3.h, r)
                   if (existingHeap.isDefined) {
                     existingHeap.get.heap
                   } else {
                     val (identifier, rSort) = r match {
-                      case f: ast.Field => (BasicChunkIdentifier(f.name), v.symbolConverter.toSort(f.typ))
-                      case p: ast.Predicate => (BasicChunkIdentifier(p.name), sorts.Snap)
+                      case f: ast.Field => (BasicChunkIdentifier(f.name), sorts.HeapSort(v.symbolConverter.toSort(f.typ)))
+                      case p: ast.Predicate => (BasicChunkIdentifier(p.name), sorts.PredHeapSort)
                       case mwi => (mwi, sorts.Snap)
                     }
-                    val chunks: Seq[BasicChunk] = s4.h.values.filter{
+                    val chunks: Seq[BasicChunk] = s3.h.values.filter{
                       case bc: BasicChunk => bc.id == identifier
                       case _ => false
                     }.toSeq.asInstanceOf[Seq[BasicChunk]]

src/main/scala/rules/Executor.scala

@@ -187,8 +187,8 @@ object executor extends ExecutionRules {
             val gBody = Store(wvs.foldLeft(s.g.values)((map, x) => map.updated(x, v.decider.fresh(x))))
 
             val bodyHeap = if (Verifier.config.maskHeapMode()) {
-              val fieldChunks = s.program.fields.map(f => BasicMaskHeapChunk(FieldID, f, ZeroMask, v.decider.fresh("hInit", HeapSort(v.symbolConverter.toSort(f.typ)))))
-              val predChunks = s.program.predicates.map(p => BasicMaskHeapChunk(PredicateID, p, PredZeroMask, v.decider.fresh("hInit", PredHeapSort)))
+              val fieldChunks = s.program.fields.filter(f => s.qpFields.contains(f)).map(f => BasicMaskHeapChunk(FieldID, f, ZeroMask, v.decider.fresh("hInit", HeapSort(v.symbolConverter.toSort(f.typ)))))
+              val predChunks = s.program.predicates.filter(p => s.qpPredicates.contains(p)).map(p => BasicMaskHeapChunk(PredicateID, p, PredZeroMask, v.decider.fresh("hInit", PredHeapSort)))
               Heap(fieldChunks ++ predChunks)
             } else {
               Heap()
@@ -307,7 +307,7 @@ object executor extends ExecutionRules {
           val t = ssaifyRhs(tRhs, x.name, x.typ, v)
           Q(s1.copy(g = s1.g + (x, t)), v1)})
 
-      case ass @ ast.FieldAssign(fa @ ast.FieldAccess(eRcvr, field), rhs) if Verifier.config.maskHeapMode() =>
+      case ass @ ast.FieldAssign(fa @ ast.FieldAccess(eRcvr, field), rhs) if Verifier.config.maskHeapMode() && s.qpFields.contains(field) =>
         assert(!s.exhaleExt)
         val pve = AssignmentFailed(ass)
         eval(s, eRcvr, pve, v)((s1, tRcvr, v1) =>
@@ -398,16 +398,22 @@ object executor extends ExecutionRules {
         val tRcvr = v.decider.fresh(x)
         v.decider.assume(tRcvr !== Null)
         var heap = s.h
-        for (field <- fields) {
+        val (qpFields, otherFields) = fields.partition(f => s.qpFields.contains(f))
+        for (field <- qpFields) {
           // assume currently none
           val fieldChunk = maskHeapSupporter.findMaskHeapChunk(heap, field)
           v.decider.assume(HeapLookup(fieldChunk.mask, tRcvr) === NoPerm)
           // add one
           val newFieldChunk = fieldChunk.copy(mask = HeapUpdate(fieldChunk.mask, tRcvr, FullPerm))
           heap = heap - fieldChunk + newFieldChunk
         }
+        val newChunks = otherFields map (field => {
+          val p = FullPerm
+          val snap = v.decider.fresh(field.name, v.symbolConverter.toSort(field.typ))
+          BasicChunk(FieldID, BasicChunkIdentifier(field.name), Seq(tRcvr), snap, p)
+        })
         val ts = viper.silicon.state.utils.computeReferenceDisjointnesses(s, tRcvr)
-        val s1 = s.copy(g = s.g + (x, tRcvr), h = heap)
+        val s1 = s.copy(g = s.g + (x, tRcvr), h = heap + Heap(newChunks))
         v.decider.assume(ts)
         Q(s1, v)
 

src/main/scala/rules/MaskHeapSupport.scala

@@ -61,10 +61,10 @@ object maskHeapSupporter extends SymbolicExecutionRules {
 
   def findMaskHeapChunk(h: Heap, r: Any) = findMaskHeapChunkOptionally(h, r).get
 
-  def findMaskHeapChunkOptionally(h: Heap, r: Any) = h.values.find(c => c.asInstanceOf[MaskHeapChunk].resource == r).asInstanceOf[Option[BasicMaskHeapChunk]]
+  def findMaskHeapChunkOptionally(h: Heap, r: Any) = h.values.filter(_.isInstanceOf[MaskHeapChunk]).find(c => c.asInstanceOf[MaskHeapChunk].resource == r).asInstanceOf[Option[BasicMaskHeapChunk]]
 
   def findOrCreateMaskHeapChunk(h: Heap, mwi: MagicWandIdentifier, v: Verifier) = {
-    h.values.find(c => c.asInstanceOf[MaskHeapChunk].resource == mwi) match {
+    h.values.filter(_.isInstanceOf[MaskHeapChunk]).find(c => c.asInstanceOf[MaskHeapChunk].resource == mwi) match {
       case Some(c: BasicMaskHeapChunk) => (h, c)
       case None =>
         val newHeap = v.decider.fresh("mwHeap", PredHeapSort)

src/main/scala/rules/Producer.scala

@@ -140,7 +140,11 @@ object producer extends ProductionRules {
     if (Verifier.config.maskHeapMode()) {
       val givenSnap = sf(sorts.Snap, v)
       val fakeTerm = if (!givenSnap.isInstanceOf[FakeMaskMapTerm]) {
-        val otherSnap = sf(null, null)
+        val otherSnap = try {
+          sf(null, null)
+        } catch {
+          case _: NullPointerException => null
+        }
         if (otherSnap.isInstanceOf[FakeMaskMapTerm]) {
           val tlcSnaps = fromSnapTree(givenSnap, as.size).map(t => Some(t))
           FakeMaskMapTerm(otherSnap.asInstanceOf[FakeMaskMapTerm].masks, tlcSnaps)
@@ -205,7 +209,7 @@ object producer extends ProductionRules {
           if (s == null && v == null) {
             snapTerm
           } else {
-            snapTerm.tlcNonQpTerms(0).get
+            snapTerm.tlcNonQpTerms(0).get.convert(s)
           }
         }
         sfFirst

src/main/scala/rules/StateConsolidator.scala

@@ -50,12 +50,34 @@ class MinimalStateConsolidator extends StateConsolidationRules {
   protected def assumeUpperPermissionBoundForQPFields(s: State, @unused heaps: Seq[Heap], @unused v: Verifier): State = s
 }
 
-class MaskHeapStateConsolidator extends MinimalStateConsolidator {
-  override def merge(fr: FunctionRecorder, h: Heap, ch: NonQuantifiedChunk, v: Verifier): (FunctionRecorder, Heap) = ???
+class MaskHeapStateConsolidator(config: Config) extends DefaultStateConsolidator(config) {
+
+  def filterMHChunks(h: Heap): Heap = {
+    Heap(h.values.filterNot(_.isInstanceOf[MaskHeapChunk]))
+  }
+
+  def filterNormalChunks(h: Heap): Heap = {
+    Heap(h.values.filter(_.isInstanceOf[MaskHeapChunk]))
+  }
+
+  override def consolidate(s: State, v: Verifier): State = {
+    val oldH = filterNormalChunks(s.h)
+    val oldReserves = s.reserveHeaps.map(h => filterNormalChunks(h))
+    val consolidated = super.consolidate(s.copy(h = filterMHChunks(s.h), reserveHeaps = s.reserveHeaps.map(h => filterMHChunks(h))), v)
+    consolidated.copy(h = consolidated.h + oldH, reserveHeaps = consolidated.reserveHeaps.zip(oldReserves).map(hs => hs._1 + hs._2))
+  }
 
   override def merge(fr: FunctionRecorder, h: Heap, newH: Heap, v: Verifier): (FunctionRecorder, Heap) = {
-    (fr, maskHeapSupporter.mergeWandHeaps(h, newH, v))
+    val (hMH, hNormal) = h.values.partition(_.isInstanceOf[MaskHeapChunk])
+    val (nMH, nNormal) = newH.values.partition(_.isInstanceOf[MaskHeapChunk])
+    val (fr1, h1) = super.merge(fr, Heap(hNormal), Heap(nNormal), v)
+    val h2 = maskHeapSupporter.mergeWandHeaps(Heap(hMH), Heap(nMH), v)
+    (fr1, h1 + h2)
   }
+
+  override protected def assumeUpperPermissionBoundForQPFields(s: State, v: Verifier): State = s
+
+  override protected def assumeUpperPermissionBoundForQPFields(s: State, heaps: Seq[Heap], v: Verifier): State = s
 }
 
 /** Default implementation that merges as many known-alias chunks as possible, and deduces various

src/main/scala/supporters/MethodSupporter.scala

@@ -51,8 +51,8 @@ trait DefaultMethodVerificationUnitProvider extends VerifierComponent { v: Verif
       openSymbExLogger(method)
 
       val heap = if (Verifier.config.maskHeapMode()) {
-        val fieldChunks = sInit.program.fields.map(f => BasicMaskHeapChunk(FieldID, f, ZeroMask, decider.fresh("hInit", HeapSort(symbolConverter.toSort(f.typ)))))
-        val predChunks = sInit.program.predicates.map(p => BasicMaskHeapChunk(PredicateID, p, PredZeroMask, decider.fresh("hInit", PredHeapSort)))
+        val fieldChunks = sInit.program.fields.filter(f => sInit.qpFields.contains(f)).map(f => BasicMaskHeapChunk(FieldID, f, ZeroMask, decider.fresh("hInit", HeapSort(symbolConverter.toSort(f.typ)))))
+        val predChunks = sInit.program.predicates.filter(p => sInit.qpPredicates.contains(p)).map(p => BasicMaskHeapChunk(PredicateID, p, PredZeroMask, decider.fresh("hInit", PredHeapSort)))
         Heap(fieldChunks ++ predChunks)
       } else {
         sInit.h

src/main/scala/supporters/functions/FunctionData.scala

@@ -292,7 +292,7 @@ class FunctionData(val programFunction: ast.Function,
 
   def transformToHeapVersion(t: Term) = {
     val resources = maskHeapSupporter.getResourceSeq(programFunction.pres, program)
-    val resHeaps = fromSnapTree(`?s`, resources.size).zip(resources).map {
+    val resHeaps = fromSnapTree(Second(`?s`), resources.size).zip(resources).map {
       case (s, r) =>
         val srt = r match {
           case f: ast.Field => sorts.HeapSort(symbolConverter.toSort(f.typ))

src/main/scala/verifier/BaseVerifier.scala

@@ -61,7 +61,7 @@ abstract class BaseVerifier(val config: Config,
     import StateConsolidationMode._
 
     config.stateConsolidationMode() match {
-      case _ if config.maskHeapMode() => new MaskHeapStateConsolidator
+      case _ if config.maskHeapMode() => new MaskHeapStateConsolidator(config)
       case Minimal => new MinimalStateConsolidator
       case Default => new DefaultStateConsolidator(config)
       case Retrying => new RetryingStateConsolidator(config)

src/test/scala/SiliconTests.scala

@@ -56,5 +56,5 @@ class SiliconTests extends SilSuite {
   }
 
   val commandLineArguments: Seq[String] =
-    Seq("--timeout", "600" /* seconds */, "--maskHeapMode")
+    Seq("--timeout", "600" /* seconds */, "--maskHeapMode", "--enableMoreCompleteExhale")
 }