From c41fd00f42833452f351a562c288d171658a6299 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Sun, 22 Oct 2023 16:54:25 +0200 Subject: [PATCH] Read permissions work, more tests --- src/main/scala/rules/MagicWandSupporter.scala | 1 - .../scala/rules/chunks/ChunkSupporter.scala | 48 ++++-- src/test/resources/kinduct/basic.vpr | 162 ++++++++++++++++++ 3 files changed, 199 insertions(+), 12 deletions(-) diff --git a/src/main/scala/rules/MagicWandSupporter.scala b/src/main/scala/rules/MagicWandSupporter.scala index 13f801e8d..2092ddc94 100644 --- 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 index d2cbec664..8bb72f59f 100644 --- 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 index 9673fdd4a..7a973b252 100644 --- 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