Read permissions work, more tests

viperproject · Oct 22, 2023 · c41fd00 · c41fd00
1 parent 3517f38
commit c41fd00
Show file tree

Hide file tree

Showing 3 changed files with 199 additions and 12 deletions.
diff --git a/src/main/scala/rules/MagicWandSupporter.scala b/src/main/scala/rules/MagicWandSupporter.scala
@@ -153,7 +153,6 @@ object magicWandSupporter extends SymbolicExecutionRules {
             val sInP = if (hps.nonEmpty) sIn else sIn.copy(loopReadVarStack = sIn.loopReadVarStack.tail.prepended((sIn.loopReadVarStack.head._1, false)))
             val (success, sOutP, h, cHeap, cch) = consumeFunction(sInP, heap, permsNeeded, v)
             val sOut = sOutP.copy(loopReadVarStack = sIn.loopReadVarStack)
-            println("===")
             val tEq = (cchs.flatten.lastOption, cch) match {
               /* Equating wand snapshots would indirectly equate the actual left hand sides when they are applied
                * and thus be unsound. Since fractional wands do not exist it is not necessary to equate their

diff --git a/src/main/scala/rules/chunks/ChunkSupporter.scala b/src/main/scala/rules/chunks/ChunkSupporter.scala
@@ -201,22 +201,48 @@ object chunkSupporter extends ChunkSupportRules {
             : VerificationResult = {
 
     executionFlowController.tryOrFail2[Heap, Term](s.copy(h = h), v)((s1, v1, QS) => {
-      val lookupFunction = {
+      {
         if (s1.loopPhaseStack.nonEmpty && (s1.loopPhaseStack.head._1 == LoopPhases.Transferring || s1.loopPhaseStack.head._1 == LoopPhases.Assuming)) {
           assert(s1.moreCompleteExhale)
-          val perms = FractionPermLiteral(Rational(1, 100))// s1.loopReadVarStack.head._1
-          def fn(s: State, h: Heap, resource: ast.Resource, args: Seq[Term], ve: VerificationError, v: Verifier)(QP: (State, Term, Verifier) => VerificationResult): VerificationResult = {
-            moreCompleteExhaleSupporter.consumeComplete(s, h, resource, args, perms, ve, v)((s2, h2, hConsumed, snap2, v2) => {
-              QP(s2, snap2.get, v2)
+
+          val identifier = resource match {
+            case f: ast.Field => BasicChunkIdentifier(f.name)
+            case p: ast.Predicate => BasicChunkIdentifier(p.name)
+            case mw: ast.MagicWand => ??? // MagicWandIdentifier(mw, s.program)
+          }
+          val chs = chunkSupporter.findChunksWithID[NonQuantifiedChunk](h.values, identifier)
+          val currentPermAmount =
+            chs.foldLeft(NoPerm: Term)((q, ch) => {
+              val argsPairWiseEqual = And(args.zip(ch.args).map { case (a1, a2) => a1 === a2 })
+              PermPlus(q, Ite(argsPairWiseEqual, ch.perm, NoPerm))
             })
+          val havePerm = IsPositive(currentPermAmount)
+          brancher.branch(s1, havePerm, None, v1)((s2, v2) => {
+            moreCompleteExhaleSupporter.lookupComplete(s2, h, resource, args, ve, v2)((s3, tSnap, v3) =>
+              QS(s3, s3.h, tSnap, v3))
+          },
+            (s2, v2) => {
+              val perms = s2.loopReadVarStack.head._1 // FractionPermLiteral(Rational(1, 100))
+
+              def fn(s: State, h: Heap, resource: ast.Resource, args: Seq[Term], ve: VerificationError, v: Verifier)(QP: (State, Term, Verifier) => VerificationResult): VerificationResult = {
+                moreCompleteExhaleSupporter.consumeComplete(s, h, resource, args, perms, ve, v)((s2, h2, hConsumed, snap2, v2) => {
+                  QP(s2, snap2.get, v2)
+                })
+              }
+
+              fn(s2, s2.h, resource, args, ve, v2)((s3, tSnap, v3) =>
+                QS(s3, s3.h, tSnap, v3))
+            })
+        } else {
+          if (s1.moreCompleteExhale) {
+            moreCompleteExhaleSupporter.lookupComplete(s1, s1.h, resource, args, ve, v1)((s2, tSnap, v2) =>
+              QS(s2, s2.h, tSnap, v2))
+          } else {
+            lookupGreedy(s1, s1.h, resource, args, ve, v1)((s2, tSnap, v2) =>
+              QS(s2, s2.h, tSnap, v2))
           }
-          fn _
-        } else
-        if (s1.moreCompleteExhale) moreCompleteExhaleSupporter.lookupComplete _
-        else lookupGreedy _
+        }
       }
-      lookupFunction(s1, s1.h, resource, args, ve, v1)((s2, tSnap, v2) =>
-        QS(s2, s2.h, tSnap, v2))
     })(Q)
   }
 

diff --git a/src/test/resources/kinduct/basic.vpr b/src/test/resources/kinduct/basic.vpr
@@ -4,6 +4,7 @@ field g: Ref
 predicate P(x: Ref) { acc(x.f) && acc(x.g, 1/2) }
 
 method havocBool() returns (b: Bool)
+function detBool(): Bool
 
 method m(r1: Ref, r2: Ref, r3: Ref, b: Bool)
     requires acc(r1.f) && acc(r2.f, 1/2) && acc(r3.f, 1/2)
@@ -144,6 +145,167 @@ method div(n0: Int, n: Int) returns (r: Int)
   requires n > 0 && n0 >= n
   ensures r >= 0
 
+method mFrame(r: Ref)
+    requires acc(r.f)
+{
+    var b: Bool
+    b := havocBool()
+    r.f := 1
+    while (b)
+    {
+        b := havocBool()
+    }
+    assert r.f == 1
+}
+
+method mFrame2(r: Ref)
+    requires acc(r.f)
+{
+    var b: Bool
+    b := havocBool()
+    r.f := 1
+    while (b)
+    {
+        assert acc(r.f)
+        b := havocBool()
+    }
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert r.f == 1
+}
+
+method mFrame3(r: Ref)
+    requires acc(r.f)
+{
+    var b: Bool
+    b := havocBool()
+    r.f := 1
+    while (b)
+        invariant r.f == 1
+    {
+        assert acc(r.f)
+        b := havocBool()
+    }
+    assert r.f == 1
+}
+
+method mFrame4(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)
+        var tmp: Bool
+        tmp := havocBool()
+        if (tmp)
+        {
+            //:: ExpectedOutput(assignment.failed:insufficient.permission)
+            r.g := r.g
+        }
+        b := havocBool()
+    }
+
+}
+
+method mFrame5(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)
+        var tmp: Bool
+        tmp := detBool()
+        if (tmp)
+        {
+            r.g := r.g
+        }
+        b := havocBool()
+    }
+
+}
+
+method mRead(r: Ref, p: Perm)
+    requires p > none
+    requires acc(r.f, p)
+{
+    var b: Bool
+    b := havocBool()
+    var tmp: Int
+    tmp := 0
+    while (b)
+    {
+        tmp := tmp + r.f
+        tmp := tmp + r.f
+        b := havocBool()
+    }
+}
+
+method mRead2(r: Ref, p: Perm)
+    requires p >= none
+    requires acc(r.f, p)
+{
+    var b: Bool
+    b := havocBool()
+    var tmp: Int
+    tmp := 0
+    while (b)
+    {
+        //:: ExpectedOutput(assignment.failed:insufficient.permission)
+        tmp := tmp + r.f
+        tmp := tmp + r.f
+        b := havocBool()
+    }
+}
+
+method mRead3(r: Ref, p: Perm)
+    requires p > none
+    requires acc(r.f, p)
+{
+    var b: Bool
+    b := havocBool()
+    var tmp: Int
+    tmp := 0
+    var before: Int
+    before := r.f
+    while (b)
+    {
+        tmp := tmp + r.f
+        tmp := tmp + r.f
+        b := havocBool()
+    }
+    assert before == r.f
+    assert perm(r.f) == p
+}
+
+method mRead4(r: Ref, p: Perm)
+    requires p > none
+    requires acc(r.f, p)
+{
+    var b: Bool
+    b := havocBool()
+    var tmp: Int
+    tmp := 0
+    var before: Int
+    before := r.f
+    while (b)
+    {
+        tmp := tmp + r.f
+        tmp := tmp + r.f
+        b := havocBool()
+    }
+    assert before == r.f
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert perm(r.f) > p
+}
+
+
 // assert
 // exhale
 // read