Merging heaps early, fixing optional consumed heaps returned, fixing …

…some problems where we had too much permission on the heap
viperproject · Oct 17, 2024 · ff2f900 · ff2f900
1 parent 4e6ac3b
commit ff2f900
Show file tree

Hide file tree

Showing 5 changed files with 72 additions and 13 deletions.
diff --git a/src/main/scala/rules/Consumer.scala b/src/main/scala/rules/Consumer.scala
@@ -125,8 +125,8 @@ object consumer extends ConsumptionRules {
       else
         wrappedConsumeTlc(s, h, a, pve, v)((s1, h1, cHeap, snap1, v1) =>
           consumeTlcs(s1, h1, tlcs.tail, pves.tail, v1)((s2, h2, cHeap2, snap2, v2) => {
-            val combined = cHeap + cHeap2
-            Q(s2, h2, combined, Combine(snap1, snap2), v2)}))
+            val (fr3, combined) = v2.stateConsolidator(s2).merge(s2.functionRecorder, cHeap, cHeap2, v2)
+            Q(s2.copy(functionRecorder = fr3), h2, combined, Combine(snap1, snap2), v2)}))
     }
   }
 

diff --git a/src/main/scala/rules/QuantifiedChunkSupport.scala b/src/main/scala/rules/QuantifiedChunkSupport.scala
@@ -1320,7 +1320,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
         magicWandSupporter.consumeFromMultipleHeaps(s, heaps, permissions, failure, Seq(), v)(
           consumeSingleFromOneOfMultipleHeaps(identifier, codomainQVars, arguments, resource, chunkOrderHeuristics)
         )((s1, hs1, cHeap1, optChunks, v1) => {
-          val newTopHeap = hs1.head + cHeap1
+          //val newTopHeap = hs1.head + cHeap1
           val totalConsumedAmount = cHeap1.values.foldLeft(NoPerm: Term)((q, ch) => PermPlus(q, ch.asInstanceOf[GeneralChunk].perm))
           val totalConsumedFromFirst = if (optChunks.length > 0 && optChunks.head.nonEmpty) {
             PermMin(optChunks.head.get.asInstanceOf[QuantifiedBasicChunk].perm, totalConsumedAmount)
@@ -1332,9 +1332,12 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
 
           val nonEmptyChunks = optChunks.filter(_.isDefined)
           val cHeap2 = if (nonEmptyChunks.isEmpty) Heap() else Heap(Seq(nonEmptyChunks.head.get.asInstanceOf[QuantifiedBasicChunk].withPerm(totalConsumedFromAllButFirst)))
-          val newTopHeap2 = if (nonEmptyChunks.isEmpty) s.h else s.h + cHeap2
+          val (fr2, newTopHeap2) = if (nonEmptyChunks.isEmpty)
+            (s1.functionRecorder, s.h)
+          else
+            v1.stateConsolidator(s1).merge(s1.functionRecorder, s.h, cHeap2, v1)
 
-          val s1p = s1.copy(loopHeapStack = hs1.tail, h = newTopHeap2)
+          val s1p = s1.copy(loopHeapStack = hs1.tail, h = newTopHeap2, functionRecorder = fr2)
           if (nonEmptyChunks.isEmpty) {
             assert(v1.decider.checkSmoke(true))
             Success()

diff --git a/src/main/scala/rules/chunks/MoreCompleteExhaleSupporter.scala b/src/main/scala/rules/chunks/MoreCompleteExhaleSupporter.scala
@@ -242,8 +242,9 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
         }
 
         magicWandSupporter.consumeFromMultipleHeaps(s, heaps, perms, failure, Seq(), v)(consumeSingle)((s1, hs1, cHeap1, optChunks, v1) => {
-          val newTopHeap = hs1.head + cHeap1
-          val totalConsumedAmount = cHeap1.values.foldLeft(NoPerm: Term)((q, ch) => PermPlus(q, ch.asInstanceOf[GeneralChunk].perm))
+          //val (fr1, newTopHeap) = v1.stateConsolidator(s1).merge(s1.functionRecorder, s1.h, cHeap1, v1)
+          //val (fr1, newTopHeap) = (s1.functionRecorder, s1.h + cHeap1)
+          val totalConsumedAmount = perms
           val totalConsumedFromFirst = if (optChunks.length > 0 && optChunks.head.nonEmpty) {
             PermMin(optChunks.head.get.asInstanceOf[NonQuantifiedChunk].perm, totalConsumedAmount)
           } else {
@@ -253,10 +254,16 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
 
 
           val nonEmptyChunks = optChunks.filter(_.isDefined)
-          val cHeap2 = if (nonEmptyChunks.isEmpty) Heap() else Heap(Seq(nonEmptyChunks.head.get.asInstanceOf[NonQuantifiedChunk].withPerm(totalConsumedFromAllButFirst)))
-          val newTopHeap2 = if (nonEmptyChunks.isEmpty) s.h else s.h + cHeap2
-
-          val s1p = s1.copy(loopHeapStack = hs1.tail, h = newTopHeap2)
+          val cHeap2 = if (nonEmptyChunks.isEmpty)
+            Heap()
+          else
+            Heap(Seq(nonEmptyChunks.head.get.asInstanceOf[NonQuantifiedChunk].withPerm(totalConsumedFromAllButFirst)))
+          val (fr1, newTopHeap2) = if (nonEmptyChunks.isEmpty)
+            (s1.functionRecorder, s1.h)
+          else
+            v1.stateConsolidator(s1).merge(s1.functionRecorder,s1.h, cHeap2, v1)
+
+          val s1p = s1.copy(loopHeapStack = hs1.tail, h = newTopHeap2, functionRecorder = fr1)
           if (nonEmptyChunks.isEmpty){
             assert(v1.decider.checkSmoke(true))
             Success()
@@ -288,7 +295,8 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
         val snap = v.decider.fresh(snapSort)
         val ch = BasicChunk(FieldID, identifier, args, snap, gain)
         chunkSupporter.produce(s, h, ch, v)((s2, h2, v2) => {
-          doActualConsumeComplete(s2.copy(h = s2.h + ch), h2, resource, args, perms, ve, v2)(Q)
+          val (fr3, s3h) = v2.stateConsolidator(s2).merge(s2.functionRecorder, s2.h, ch, v2)
+          doActualConsumeComplete(s2.copy(h = s3h, functionRecorder = fr3), h2, resource, args, perms, ve, v2)(Q)
         })
       }
     } else {
@@ -426,7 +434,8 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
                 //Q(s1, newHeap, consumedHeap, Some(condSnap), v1)
                 Success()
               case false =>
-                result = (Incomplete(pNeeded), s1, newHeap, consumedHeap, None)
+                val consumedChunk = if (consumedChunks.isEmpty) None else Some(consumedChunks.head.withSnap(condSnap).withPerm(PermMinus(perms, pNeeded)))
+                result = (Incomplete(pNeeded), s1, newHeap, consumedHeap, consumedChunk)
                 //Q(s1, newHeap, consumedHeap, Some(condSnap), v1)
                 Success()
             }

diff --git a/src/test/resources/kinduct/basic.vpr b/src/test/resources/kinduct/basic.vpr
@@ -233,6 +233,29 @@ method mFrame4(r: Ref)
 
 }
 
+method mFrame4af(r: Ref)
+    requires acc(r.f) && acc(r.g)
+{
+    var b: Bool
+    b := havocBool()
+    r.f := 1
+    while (b)
+        invariant r.f == 1
+    {
+        assert acc(r.f)
+        //:: ExpectedOutput(assert.failed:assertion.false)
+        assert false
+        var tmp: Bool
+        tmp := havocBool()
+        if (tmp)
+        {
+            r.g := r.g
+        }
+        b := havocBool()
+    }
+
+}
+
 method mFrame5(r: Ref)
     requires acc(r.f) && acc(r.g)
 {

diff --git a/src/test/resources/kinduct/forceQP/basic.vpr b/src/test/resources/kinduct/forceQP/basic.vpr
@@ -254,6 +254,30 @@ method mFrame4(r: Ref)
 
 }
 
+method mFrame4af(r: Ref)
+    requires acc(r.f) && acc(r.g)
+{
+    forceQPs()
+    var b: Bool
+    b := havocBool()
+    r.f := 1
+    while (b)
+        invariant r.f == 1
+    {
+        assert acc(r.f)
+        //:: ExpectedOutput(assert.failed:assertion.false)
+        assert false
+        var tmp: Bool
+        tmp := havocBool()
+        if (tmp)
+        {
+            r.g := r.g
+        }
+        b := havocBool()
+    }
+
+}
+
 method mFrame5(r: Ref)
     requires acc(r.f) && acc(r.g)
 {