From a54023d3a712e213cb5615d74248ea3dfc590c00 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Sat, 19 Oct 2024 01:42:00 +0200 Subject: [PATCH] QP chunk merging (from master branch, thanks Alex), and immediately calling merge whenever adding chunks in more places --- src/main/scala/interfaces/state/Chunks.scala | 15 +- .../records/data/SingleMergeRecord.scala | 6 +- .../logger/writer/SymbExLogReportWriter.scala | 11 +- src/main/scala/rules/Executor.scala | 3 +- .../scala/rules/QuantifiedChunkSupport.scala | 196 +++++++++++++++--- src/main/scala/rules/StateConsolidator.scala | 71 ++++--- .../scala/rules/chunks/ChunkSupporter.scala | 13 +- src/main/scala/state/Chunks.scala | 59 ++++-- src/main/scala/state/State.scala | 2 +- src/test/resources/kinduct/basic_while.vpr | 64 ++++++ .../resources/kinduct/forceQP/basic_while.vpr | 68 ++++++ 11 files changed, 416 insertions(+), 92 deletions(-) diff --git a/src/main/scala/interfaces/state/Chunks.scala b/src/main/scala/interfaces/state/Chunks.scala index 201c76eeb..641188f15 100644 --- a/src/main/scala/interfaces/state/Chunks.scala +++ b/src/main/scala/interfaces/state/Chunks.scala @@ -17,13 +17,19 @@ trait GeneralChunk extends Chunk { val resourceID: ResourceID val id: ChunkIdentifer val perm: Term - def withPerm(perm: Term): GeneralChunk + def applyCondition(newCond: Term): GeneralChunk + def permMinus(perm: Term): GeneralChunk + def permPlus(perm: Term): GeneralChunk } trait NonQuantifiedChunk extends GeneralChunk { val args: Seq[Term] val snap: Term - override def withPerm(perm: Term): NonQuantifiedChunk + + override def applyCondition(newCond: Term): NonQuantifiedChunk + override def permMinus(perm: Term): NonQuantifiedChunk + override def permPlus(perm: Term): NonQuantifiedChunk + def withPerm(perm: Term): NonQuantifiedChunk def withSnap(snap: Term): NonQuantifiedChunk } @@ -31,6 +37,9 @@ trait QuantifiedChunk extends GeneralChunk { val quantifiedVars: Seq[Var] def snapshotMap: Term def valueAt(arguments: Seq[Term]): Term - override def withPerm(perm: Term): QuantifiedChunk + + override def applyCondition(newCond: Term): QuantifiedChunk + override def permMinus(perm: Term): QuantifiedChunk + override def permPlus(perm: Term): QuantifiedChunk def withSnapshotMap(snap: Term): QuantifiedChunk } \ No newline at end of file diff --git a/src/main/scala/logger/records/data/SingleMergeRecord.scala b/src/main/scala/logger/records/data/SingleMergeRecord.scala index 7137aff56..04dc530ad 100644 --- a/src/main/scala/logger/records/data/SingleMergeRecord.scala +++ b/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 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 diff --git a/src/main/scala/logger/writer/SymbExLogReportWriter.scala b/src/main/scala/logger/writer/SymbExLogReportWriter.scala index 8b3d9928f..bff6e301b 100644 --- a/src/main/scala/logger/writer/SymbExLogReportWriter.scala +++ b/src/main/scala/logger/writer/SymbExLogReportWriter.scala @@ -58,32 +58,32 @@ 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), @@ -91,7 +91,6 @@ object SymbExLogReportWriter { "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) ) diff --git a/src/main/scala/rules/Executor.scala b/src/main/scala/rules/Executor.scala index c01e72515..92be2f1c1 100644 --- a/src/main/scala/rules/Executor.scala +++ b/src/main/scala/rules/Executor.scala @@ -478,7 +478,8 @@ object executor extends ExecutionRules { val ch = quantifiedChunkSupporter.createSingletonQuantifiedChunk(Seq(`?r`), field, Seq(tRcvr), FullPerm, sm, s.program) if (s3.heapDependentTriggers.contains(field)) v3.decider.assume(FieldTrigger(field.name, sm, tRcvr)) - Q(s3.copy(h = h3 + ch), v3) + val (fr4, h4) = v3.stateConsolidator(s3).merge(s3.functionRecorder, h3, ch, v3) + Q(s3.copy(h = h4, functionRecorder = fr4), v3) } ) })) diff --git a/src/main/scala/rules/QuantifiedChunkSupport.scala b/src/main/scala/rules/QuantifiedChunkSupport.scala index f87812d2b..28d67cc3c 100644 --- a/src/main/scala/rules/QuantifiedChunkSupport.scala +++ b/src/main/scala/rules/QuantifiedChunkSupport.scala @@ -22,7 +22,7 @@ import viper.silicon.state.terms.perms.IsPositive import viper.silicon.state.terms.perms.BigPermSum import viper.silicon.state.terms.predef.`?r` import viper.silicon.state.terms.utils.consumeExactRead -import viper.silicon.supporters.functions.NoopFunctionRecorder +import viper.silicon.supporters.functions.{FunctionRecorder, NoopFunctionRecorder} import viper.silicon.utils.notNothing.NotNothing import viper.silicon.verifier.Verifier import viper.silver.reporter.InternalWarningMessage @@ -205,6 +205,35 @@ trait QuantifiedChunkSupport extends SymbolicExecutionRules { def hintBasedChunkOrderHeuristic(hints: Seq[Term]) : Seq[QuantifiedBasicChunk] => Seq[QuantifiedBasicChunk] + + def findChunk(chunks: Iterable[Chunk], chunk: QuantifiedChunk, v: Verifier): Option[QuantifiedChunk] + + /** Merge the snapshots of two quantified heap chunks that denote the same field locations + * + * @param fr The functionRecorder to use when new snapshot maps are generated. + * @param field The name of the field. + * @param t1 The first chunk's snapshot map. + * @param t2 The second chunk's snapshot map. + * @param p1 The first chunk's permission amount, should be constrained by the domain. + * @param p2 The second chunk's permission amount, should be constrained by the domain. + * @param v The verifier to use. + * @return A tuple (fr, sm, def) of functionRecorder, a snapshot map sm and a term def constraining sm. + */ + def combineFieldSnapshotMaps(fr: FunctionRecorder, field: String, t1: Term, t2: Term, p1: Term, p2: Term, v: Verifier): (FunctionRecorder, Term, Term) + + /** Merge the snapshots of two quantified heap chunks that denote the same predicate + * + * @param fr The functionRecorder to use when new snapshot maps are generated. + * @param predicate The name of the predicate. + * @param qVars The variables over which p1 and p2 are defined + * @param t1 The first chunk's snapshot map. + * @param t2 The second chunk's snapshot map. + * @param p1 The first chunk's permission amount, should be constrained by the domain. + * @param p2 The second chunk's permission amount, should be constrained by the domain. + * @param v The verifier to use. + * @return A tuple (fr, sm, def) of functionRecorder, a snapshot map sm and a term def constraining sm. + */ + def combinePredicateSnapshotMaps(fr: FunctionRecorder, predicate: String, qVars: Seq[Var], t1: Term, t2: Term, p1: Term, p2: Term, v: Verifier): (FunctionRecorder, Term, Term) } object quantifiedChunkSupporter extends QuantifiedChunkSupport { @@ -225,8 +254,6 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { .zip(arguments) .map { case (x, a) => x === a }) - val conditionalizedPermissions = - Ite(condition, permissions, NoPerm) val hints = extractHints(None, arguments) @@ -235,9 +262,9 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { resource, arguments, sm, - conditionalizedPermissions, + condition, + permissions, None, - Some(conditionalizedPermissions), Some(arguments), hints, program) @@ -271,11 +298,8 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { val qvarsToInversesOfCodomain = inverseFunctions.qvarsToInversesOf(codomainQVars) - val conditionalizedPermissions = - Ite( - And(And(imagesOfCodomain), condition.replace(qvarsToInversesOfCodomain)), - permissions.replace(qvarsToInversesOfCodomain), - NoPerm) + val cond = And(And(imagesOfCodomain), condition.replace(qvarsToInversesOfCodomain)) + val perms = permissions.replace(qvarsToInversesOfCodomain) val hints = extractHints(Some(condition), arguments) @@ -285,9 +309,9 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { resource, arguments, sm, - conditionalizedPermissions, + cond, + perms, Some(inverseFunctions), - Some(conditionalizedPermissions), None, hints, program) @@ -323,9 +347,9 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { resource: ast.Resource, arguments: Seq[Term], sm: Term, + condition: Term, permissions: Term, optInverseFunctions: Option[InverseFunctions], - optInitialCond: Option[Term], optSingletonArguments: Option[Seq[Term]], hints: Seq[Term], program: ast.Program) @@ -339,9 +363,9 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { QuantifiedFieldChunk( BasicChunkIdentifier(field.name), sm, + condition, permissions, optInverseFunctions, - optInitialCond, optSingletonArguments.map(_.head), hints) @@ -350,20 +374,20 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { BasicChunkIdentifier(predicate.name), codomainQVars, sm, + condition, permissions, optInverseFunctions, - optInitialCond, optSingletonArguments, hints) case wand: ast.MagicWand => + val conditionalizedPermissions = Ite(condition, permissions, NoPerm) QuantifiedMagicWandChunk( MagicWandIdentifier(wand, program), codomainQVars, sm, - permissions, + conditionalizedPermissions, optInverseFunctions, - optInitialCond, optSingletonArguments, hints) @@ -1055,8 +1079,8 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { val forall = ast.Forall(Seq(), Seq(), ast.TrueLit()())() // Just used to get the position for a potentioal warning. produce(s2, forall, resource, qvars, formalQVars, qid, optTrigger, tTriggers, auxGlobals, auxNonGlobals, tCond, tArgs, freshSnap, permissionToProduce, pve, negativePermissionReason, notInjectiveReason, v)( (s3, ch, v3) => { - val h3 = h + ch - doConsume(s3, h3, resource, qvars, formalQVars, qid, optTrigger, tTriggers, auxGlobals, auxNonGlobals, tCond, tArgs, tPerm, pve, negativePermissionReason, notInjectiveReason, insufficientPermissionReason, v3)(Q) + val (fr3, h3) = v3.stateConsolidator(s3).merge(s3.functionRecorder, h, ch, v3) + doConsume(s3.copy(functionRecorder = fr3), h3, resource, qvars, formalQVars, qid, optTrigger, tTriggers, auxGlobals, auxNonGlobals, tCond, tArgs, tPerm, pve, negativePermissionReason, notInjectiveReason, insufficientPermissionReason, v3)(Q) } ) } @@ -1323,7 +1347,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { //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) + PermMin(optChunks.head.get.perm, totalConsumedAmount) } else { NoPerm } @@ -1331,7 +1355,10 @@ 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 cHeap2 = if (nonEmptyChunks.isEmpty) + Heap() + else + Heap(Seq(nonEmptyChunks.head.get.withPerm(totalConsumedFromAllButFirst))) val (fr2, newTopHeap2) = if (nonEmptyChunks.isEmpty) (s1.functionRecorder, s.h) else @@ -1366,8 +1393,8 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { } val freshSnap = v.decider.fresh(snapSort) produceSingleLocation(s2, resource, codomainQVars, arguments, freshSnap, permissionToProduce, trigger, v)((s3, ch, v3) => { - val h3 = h + ch - doConsumeSingleLocation(s3, h3, codomainQVars, arguments, resourceAccess, permissions, optChunkOrderHeuristic, pve, v3)(Q) + val (fr4, h4) = v3.stateConsolidator(s3).merge(s3.functionRecorder, h, ch, v3) + doConsumeSingleLocation(s3.copy(functionRecorder = fr4), h4, codomainQVars, arguments, resourceAccess, permissions, optChunkOrderHeuristic, pve, v3)(Q) }) } } else { @@ -1627,7 +1654,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { v.decider.assume(permissionConstraint) remainingChunks = - remainingChunks :+ ithChunk.withPerm(PermMinus(ithChunk.perm, ithPTaken)) + remainingChunks :+ ithChunk.permMinus(ithPTaken) consumedChunks = consumedChunks :+ ithChunk.withPerm(ithPTaken) } else { v.decider.prover.comment(s"Chunk depleted?") @@ -1640,7 +1667,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { consumedChunks = consumedChunks :+ ithChunk.withPerm(ithPTaken) if (!chunkDepleted) { remainingChunks = - remainingChunks :+ ithChunk.withPerm(PermMinus(ithChunk.perm, ithPTaken)) + remainingChunks :+ ithChunk.permMinus(ithPTaken) } } } @@ -1963,6 +1990,125 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { matchingChunks ++ otherChunks } + override def findChunk(chunks: Iterable[Chunk], chunk: QuantifiedChunk, v: Verifier): Option[QuantifiedChunk] = { + val lr = chunk match { + case qfc: QuantifiedFieldChunk if qfc.invs.isDefined => + Left(qfc.invs.get.invertibles, qfc.quantifiedVars, qfc.condition) + case qfc: QuantifiedFieldChunk if qfc.singletonArguments.isDefined => + Right(qfc.singletonArguments.get) + case qpc: QuantifiedPredicateChunk if qpc.invs.isDefined => + Left(qpc.invs.get.invertibles, qpc.quantifiedVars, qpc.condition) + case qpc: QuantifiedPredicateChunk if qpc.singletonArguments.isDefined => + Right(qpc.singletonArguments.get) + case _ => return None + } + val relevantChunks: Iterable[QuantifiedBasicChunk] = chunks.flatMap { + case ch: QuantifiedBasicChunk if ch.id == chunk.id => Some(ch) + case _ => None + } + + val (receiverTerms, quantVars, cond) = lr match { + case Left(tuple) => tuple + case Right(singletonArguments) => + return relevantChunks.find { ch => + val chunkInfo = ch match { + case qfc: QuantifiedFieldChunk if qfc.singletonArguments.isDefined => + Some(qfc.singletonArguments.get) + case qpc: QuantifiedPredicateChunk if qpc.singletonArguments.isDefined => + Some(qpc.singletonArguments.get) + case _ => None + } + chunkInfo match { + case Some(cSingletonArguments) => + val equalityTerm = And(singletonArguments.zip(cSingletonArguments).map { case (a, b) => a === b }) + val result = v.decider.check(equalityTerm, Verifier.config.checkTimeout()) + if (result) { + // Learn the equality + v.decider.assume(equalityTerm) + } + result + case _ => false + } + } + } + relevantChunks.find { ch => + val chunkInfo = ch match { + case qfc: QuantifiedFieldChunk if qfc.invs.isDefined => + Some(qfc.invs.get.invertibles, qfc.quantifiedVars, qfc.condition) + case qpc: QuantifiedPredicateChunk if qpc.invs.isDefined => + Some(qpc.invs.get.invertibles, qpc.quantifiedVars, qpc.condition) + case _ => None + } + chunkInfo match { + case Some((cInvertibles, cQvars, cCond)) => + receiverTerms.zip(cInvertibles).forall(p => { + if (cQvars.length == quantVars.length && cQvars.zip(quantVars).forall(vars => vars._1.sort == vars._2.sort)) { + val condReplaced = cCond.replace(cQvars, quantVars) + val secondReplaced = p._2.replace(cQvars, quantVars) + val equalityTerm = SimplifyingForall(quantVars, And(Seq(p._1 === secondReplaced, cond === condReplaced)), Seq()) + val result = v.decider.check(equalityTerm, Verifier.config.checkTimeout()) + if (result) { + // Learn the equality + v.decider.assume(equalityTerm) + } + result + } else { + false + } + }) + case _ => false + } + } + } + + // Based on StateConsolidator#combineSnapshots + override def combineFieldSnapshotMaps(fr: FunctionRecorder, field: String, t1: Term, t2: Term, p1: Term, p2: Term, v: Verifier): (FunctionRecorder, Term, Term) = { + val lookupT1 = Lookup(field, t1, `?r`) + val lookupT2 = Lookup(field, t2, `?r`) + val (fr2, sm, smDef, triggers) = (IsPositive(p1), IsPositive(p2)) match { + // If we statically know that both permission values are positive we can forego the quantifier + case (True, True) => return (fr, t1, t1 === t2) + case (True, b2) => (fr, t1, Implies(b2, lookupT1 === lookupT2), Seq(Trigger(lookupT1), Trigger(lookupT2))) + case (b1, True) => (fr, t2, Implies(b1, lookupT2 === lookupT1), Seq(Trigger(lookupT2), Trigger(lookupT1))) + case (b1, b2) => + /* + * Since it is not definitely known whether p1 and p2 are positive, + * we have to introduce a fresh snapshot. Note that it is not sound + * to use t1 or t2 and constrain it. + */ + val t3 = v.decider.fresh(t1.sort) + val lookupT3 = Lookup(field, t3, `?r`) + (fr.recordConstrainedVar(t3, And(Implies(b1, lookupT3 === lookupT1), Implies(b2, lookupT3 === lookupT2))), t3, + And(Implies(b1, lookupT3 === lookupT1), Implies(b2, lookupT3 === lookupT2)), Seq(Trigger(lookupT1), Trigger(lookupT2), Trigger(lookupT3))) + } + + (fr2, sm, Forall(`?r`, smDef, triggers)) + } + + // Based on StateConsolidator#combineSnapshots + override def combinePredicateSnapshotMaps(fr: FunctionRecorder, predicate: String, qVars: Seq[Var], t1: Term, t2: Term, p1: Term, p2: Term, v: Verifier): (FunctionRecorder, Term, Term) = { + val lookupT1 = PredicateLookup(predicate, t1, qVars) + val lookupT2 = PredicateLookup(predicate, t2, qVars) + val (fr2, sm, smDef, triggers) = (IsPositive(p1), IsPositive(p2)) match { + // If we statically know that both permission values are positive we can forego the quantifier + case (True, True) => return (fr, t1, t1 === t2) + case (True, b2) => (fr, t1, Implies(b2, lookupT1 === lookupT2), Seq(Trigger(lookupT1), Trigger(lookupT2))) + case (b1, True) => (fr, t2, Implies(b1, lookupT2 === lookupT1), Seq(Trigger(lookupT2), Trigger(lookupT1))) + case (b1, b2) => + /* + * Since it is not definitely known whether p1 and p2 are positive, + * we have to introduce a fresh snapshot. Note that it is not sound + * to use t1 or t2 and constrain it. + */ + val t3 = v.decider.fresh(t1.sort) + val lookupT3 = PredicateLookup(predicate, t3, qVars) + (fr.recordConstrainedVar(t3, And(Implies(b1, lookupT3 === lookupT1), Implies(b2, lookupT3 === lookupT2))), t3, + And(Implies(b1, lookupT3 === lookupT1), Implies(b2, lookupT3 === lookupT2)), Seq(Trigger(lookupT1), Trigger(lookupT2), Trigger(lookupT3))) + } + + (fr2, sm, Forall(qVars, smDef, triggers)) + } + def qpAppChunkOrderHeuristics(receiverTerms: Seq[Term], quantVars: Seq[Var], hints: Seq[Term], v: Verifier) : Seq[QuantifiedBasicChunk] => Seq[QuantifiedBasicChunk] = { // Heuristics that looks for quantified chunks that have the same shape (as in, the same number and types of diff --git a/src/main/scala/rules/StateConsolidator.scala b/src/main/scala/rules/StateConsolidator.scala index 8219512f5..a383eaf4f 100644 --- a/src/main/scala/rules/StateConsolidator.scala +++ b/src/main/scala/rules/StateConsolidator.scala @@ -26,7 +26,7 @@ trait StateConsolidationRules extends SymbolicExecutionRules { def consolidate(s: State, v: Verifier): State def consolidateOptionally(s: State, v: Verifier): State def merge(fr: FunctionRecorder, h: Heap, newH: Heap, v: Verifier): (FunctionRecorder, Heap) - def merge(fr: FunctionRecorder, h: Heap, ch: NonQuantifiedChunk, v: Verifier): (FunctionRecorder, Heap) + def merge(fr: FunctionRecorder, h: Heap, ch: Chunk, v: Verifier): (FunctionRecorder, Heap) protected def assumeUpperPermissionBoundForQPFields(s: State, v: Verifier): State protected def assumeUpperPermissionBoundForQPFields(s: State, heaps: Seq[Heap], v: Verifier): State @@ -44,7 +44,7 @@ class MinimalStateConsolidator extends StateConsolidationRules { def merge(fr: FunctionRecorder, h: Heap, newH: Heap, v: Verifier): (FunctionRecorder, Heap) = (fr, Heap(h.values ++ newH.values)) - def merge(fr: FunctionRecorder, h: Heap, ch: NonQuantifiedChunk, v: Verifier): (FunctionRecorder, Heap) = + def merge(fr: FunctionRecorder, h: Heap, ch: Chunk, v: Verifier): (FunctionRecorder, Heap) = (fr, h + ch) protected def assumeUpperPermissionBoundForQPFields(s: State, @unused v: Verifier): State = s @@ -66,13 +66,11 @@ class DefaultStateConsolidator(protected val config: Config) extends StateConsol val (functionRecorderAfterHeapMerging, mergedHeaps) = initialHeaps.foldLeft((s.functionRecorder, Nil: List[Heap])) { case ((fr, hs), h) => - val (nonQuantifiedChunks, otherChunks) = partition(h) - var continue = false - var mergedChunks: Seq[NonQuantifiedChunk] = Nil - var destChunks: Seq[NonQuantifiedChunk] = Nil - var newChunks: Seq[NonQuantifiedChunk] = nonQuantifiedChunks + var mergedChunks: Seq[Chunk] = Nil + var destChunks: Seq[Chunk] = Nil + var newChunks: Seq[Chunk] = h.values.toSeq var functionRecorder: FunctionRecorder = fr var fixedPointRound: Int = 0 @@ -94,10 +92,9 @@ class DefaultStateConsolidator(protected val config: Config) extends StateConsol fixedPointRound = fixedPointRound + 1 } while (continue) - val allChunks = mergedChunks ++ otherChunks - val interpreter = new NonQuantifiedPropertyInterpreter(allChunks, v) + val interpreter = new NonQuantifiedPropertyInterpreter(mergedChunks, v) - mergedChunks foreach { ch => + mergedChunks.filter(_.isInstanceOf[BasicChunk]) foreach { case ch: BasicChunk => val resource = Resources.resourceDescriptions(ch.resourceID) v.decider.assume(interpreter.buildPathConditionsForChunk(ch, resource.instanceProperties)) } @@ -107,7 +104,7 @@ class DefaultStateConsolidator(protected val config: Config) extends StateConsol } v.symbExLog.closeScope(sepIdentifier) - (functionRecorder, hs :+ Heap(allChunks)) + (functionRecorder, hs :+ Heap(mergedChunks)) } val s1 = s.copy(functionRecorder = functionRecorderAfterHeapMerging, @@ -123,43 +120,41 @@ class DefaultStateConsolidator(protected val config: Config) extends StateConsol if (s.retrying) consolidate(s, v) else s - def merge(fr: FunctionRecorder, h: Heap, ch: NonQuantifiedChunk, v: Verifier): (FunctionRecorder, Heap) = { + def merge(fr: FunctionRecorder, h: Heap, ch: Chunk, v: Verifier): (FunctionRecorder, Heap) = { merge(fr, h, Heap(Seq(ch)), v) } def merge(fr1: FunctionRecorder, h: Heap, newH: Heap, v: Verifier): (FunctionRecorder, Heap) = { val mergeLog = new CommentRecord("Merge", null, v.decider.pcs) val sepIdentifier = v.symbExLog.openScope(mergeLog) - val (nonQuantifiedChunks, otherChunks) = partition(h) - val (newNonQuantifiedChunks, newOtherChunk) = partition(newH) - val (fr2, mergedChunks, newlyAddedChunks, snapEqs) = singleMerge(fr1, nonQuantifiedChunks, newNonQuantifiedChunks, v) + val (fr2, mergedChunks, newlyAddedChunks, snapEqs) = singleMerge(fr1, h.values.toSeq, newH.values.toSeq, v) v.decider.assume(snapEqs) val interpreter = new NonQuantifiedPropertyInterpreter(mergedChunks, v) - newlyAddedChunks foreach { ch => + newlyAddedChunks.filter(_.isInstanceOf[BasicChunk]) foreach { case ch: BasicChunk => val resource = Resources.resourceDescriptions(ch.resourceID) v.decider.assume(interpreter.buildPathConditionsForChunk(ch, resource.instanceProperties)) } v.symbExLog.closeScope(sepIdentifier) - (fr2, Heap(mergedChunks ++ otherChunks ++ newOtherChunk)) + (fr2, Heap(mergedChunks)) } private def singleMerge(fr: FunctionRecorder, - destChunks: Seq[NonQuantifiedChunk], - newChunks: Seq[NonQuantifiedChunk], + destChunks: Seq[Chunk], + newChunks: Seq[Chunk], v: Verifier) : (FunctionRecorder, - Seq[NonQuantifiedChunk], - Seq[NonQuantifiedChunk], + Seq[Chunk], + Seq[Chunk], InsertionOrderedSet[Term]) = { val mergeLog = new SingleMergeRecord(destChunks, newChunks, v.decider.pcs) val sepIdentifier = v.symbExLog.openScope(mergeLog) // bookkeeper.heapMergeIterations += 1 - val initial = (fr, destChunks, Seq[NonQuantifiedChunk](), InsertionOrderedSet[Term]()) + val initial = (fr, destChunks, Seq[Chunk](), InsertionOrderedSet[Term]()) val result = newChunks.foldLeft(initial) { case ((fr1, accMergedChunks, accNewChunks, accSnapEqs), nextChunk) => /* accMergedChunks: already merged chunks @@ -169,7 +164,7 @@ class DefaultStateConsolidator(protected val config: Config) extends StateConsol * sequence of destination chunks */ - chunkSupporter.findMatchingChunk(accMergedChunks, nextChunk, v) match { + findMatchingChunk(accMergedChunks, nextChunk, v) match { case Some(ch) => mergeChunks(fr1, ch, nextChunk, v) match { case Some((fr2, newChunk, snapEq)) => @@ -185,14 +180,38 @@ class DefaultStateConsolidator(protected val config: Config) extends StateConsol result } + private def findMatchingChunk(chunks: Iterable[Chunk], chunk: Chunk, v: Verifier): Option[Chunk] = { + chunk match { + case chunk: BasicChunk => + chunkSupporter.findChunk[BasicChunk](chunks, chunk.id, chunk.args, v) + case chunk: QuantifiedChunk => quantifiedChunkSupporter.findChunk(chunks, chunk, v) + case _ => None + } + } + // Merges two chunks that are aliases (i.e. that have the same id and the args are proven to be equal) // and returns the merged chunk or None, if the chunks could not be merged - private def mergeChunks(fr1: FunctionRecorder, chunk1: NonQuantifiedChunk, chunk2: NonQuantifiedChunk, v: Verifier) = (chunk1, chunk2) match { + private def mergeChunks(fr1: FunctionRecorder, chunk1: Chunk, chunk2: Chunk, v: Verifier) = (chunk1, chunk2) match { case (BasicChunk(rid1, id1, args1, snap1, perm1), BasicChunk(_, _, _, snap2, perm2)) => val (fr2, combinedSnap, snapEq) = combineSnapshots(fr1, snap1, snap2, perm1, perm2, v) Some(fr2, BasicChunk(rid1, id1, args1, combinedSnap, PermPlus(perm1, perm2)), snapEq) - case (_, _) => + case (l@QuantifiedFieldChunk(id1, fvf1, condition1, perm1, invs1, singletonRcvr1, hints1), + r@QuantifiedFieldChunk(_, fvf2, _, perm2, _, _, hints2)) => + assert(l.quantifiedVars == Seq(`?r`)) + assert(r.quantifiedVars == Seq(`?r`)) + // We need to use l.perm/r.perm here instead of perm1 and perm2 since the permission amount might be dependent on the condition/domain + val (fr2, combinedSnap, snapEq) = quantifiedChunkSupporter.combineFieldSnapshotMaps(fr1, id1.name, fvf1, fvf2, l.perm, r.perm, v) + val permSum = PermPlus(perm1, perm2) + val bestHints = if (hints1.nonEmpty) hints1 else hints2 + Some(fr2, QuantifiedFieldChunk(id1, combinedSnap, condition1, permSum, invs1, singletonRcvr1, bestHints), snapEq) + case (l@QuantifiedPredicateChunk(id1, qVars1, psf1, _, perm1, _, _, _), + r@QuantifiedPredicateChunk(_, qVars2, psf2, condition2, perm2, invs2, singletonArgs2, hints2)) => + val (fr2, combinedSnap, snapEq) = quantifiedChunkSupporter.combinePredicateSnapshotMaps(fr1, id1.name, qVars2, psf1, psf2, l.perm.replace(qVars1, qVars2), r.perm, v) + + val permSum = PermPlus(perm1.replace(qVars1, qVars2), perm2) + Some(fr2, QuantifiedPredicateChunk(id1, qVars2, combinedSnap, condition2, permSum, invs2, singletonArgs2, hints2), snapEq) + case _ => None } @@ -339,7 +358,7 @@ class MinimalRetryingStateConsolidator(config: Config) extends RetryingStateCons override def merge(fr: FunctionRecorder, h: Heap, newH: Heap, v: Verifier): (FunctionRecorder, Heap) = (fr, Heap(h.values ++ newH.values)) - override def merge(fr: FunctionRecorder, h: Heap, ch: NonQuantifiedChunk, v: Verifier): (FunctionRecorder, Heap) = + override def merge(fr: FunctionRecorder, h: Heap, ch: Chunk, v: Verifier): (FunctionRecorder, Heap) = (fr, h + ch) override protected def assumeUpperPermissionBoundForQPFields(s: State, @unused v: Verifier): State = s diff --git a/src/main/scala/rules/chunks/ChunkSupporter.scala b/src/main/scala/rules/chunks/ChunkSupporter.scala index 75d6d6e3a..4613c782e 100644 --- a/src/main/scala/rules/chunks/ChunkSupporter.scala +++ b/src/main/scala/rules/chunks/ChunkSupporter.scala @@ -44,12 +44,6 @@ trait ChunkSupportRules extends SymbolicExecutionRules { (Q: (State, Heap, Term, Verifier) => VerificationResult) : VerificationResult - def findMatchingChunk[CH <: NonQuantifiedChunk: ClassTag] - (chunks: Iterable[Chunk], - chunk: CH, - v: Verifier) - : Option[CH] - def findChunksWithID[CH <: NonQuantifiedChunk: ClassTag] (chunks: Iterable[Chunk], id: ChunkIdentifer) @@ -278,7 +272,7 @@ object chunkSupporter extends ChunkSupportRules { } } - private[chunks] def findChunk[CH <: NonQuantifiedChunk: ClassTag] + def findChunk[CH <: NonQuantifiedChunk: ClassTag] (chunks: Iterable[Chunk], id: ChunkIdentifer, args: Iterable[Term], @@ -288,11 +282,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) diff --git a/src/main/scala/state/Chunks.scala b/src/main/scala/state/Chunks.scala index 1e5d3ceec..6a3acce73 100644 --- a/src/main/scala/state/Chunks.scala +++ b/src/main/scala/state/Chunks.scala @@ -40,6 +40,9 @@ case class BasicChunk(resourceID: BaseID, //case PredicateID => require(snap.sort == sorts.Snap, s"A predicate chunk's snapshot ($snap) is expected to be of sort Snap, but found ${snap.sort}") //} + override def applyCondition(newCond: Term) = withPerm(Ite(newCond, perm, NoPerm)) + override def permMinus(newPerm: Term) = withPerm(PermMinus(perm, newPerm)) + override def permPlus(newPerm: Term) = withPerm(PermPlus(perm, newPerm)) override def withPerm(newPerm: Term) = BasicChunk(resourceID, id, args, snap, newPerm) override def withSnap(newSnap: Term) = BasicChunk(resourceID, id, args, newSnap, perm) @@ -51,7 +54,11 @@ case class BasicChunk(resourceID: BaseID, sealed trait QuantifiedBasicChunk extends QuantifiedChunk { override val id: ChunkIdentifer - override def withPerm(perm: Term): QuantifiedBasicChunk + + override def applyCondition(newCond: Term): QuantifiedBasicChunk + override def permMinus(perm: Term): QuantifiedBasicChunk + override def permPlus(perm: Term): QuantifiedBasicChunk + def withPerm(perm: Term): QuantifiedBasicChunk override def withSnapshotMap(snap: Term): QuantifiedBasicChunk def singletonArguments: Option[Seq[Term]] def hints: Seq[Term] @@ -64,19 +71,20 @@ sealed trait QuantifiedBasicChunk extends QuantifiedChunk { */ case class QuantifiedFieldChunk(id: BasicChunkIdentifier, fvf: Term, - perm: Term, + condition: Term, + permValue: Term, invs: Option[InverseFunctions], - initialCond: Option[Term], singletonRcvr: Option[Term], hints: Seq[Term] = Nil) extends QuantifiedBasicChunk { require(fvf.sort.isInstanceOf[terms.sorts.FieldValueFunction], s"Quantified chunk values must be of sort FieldValueFunction, but found value $fvf of sort ${fvf.sort}") - require(perm.sort == sorts.Perm, s"Permissions $perm must be of sort Perm, but found ${perm.sort}") + require(permValue.sort == sorts.Perm, s"Permissions $permValue must be of sort Perm, but found ${permValue.sort}") override val resourceID = FieldID override val quantifiedVars = Seq(`?r`) + override val perm = Ite(condition, permValue, NoPerm) override def snapshotMap: Term = fvf override def singletonArguments: Option[Seq[Term]] = singletonRcvr.map(Seq(_)) @@ -89,8 +97,15 @@ case class QuantifiedFieldChunk(id: BasicChunkIdentifier, Lookup(id.name, fvf, arguments.head) } - override def withPerm(newPerm: Term) = QuantifiedFieldChunk(id, fvf, newPerm, invs, initialCond, singletonRcvr, hints) - override def withSnapshotMap(newFvf: Term) = QuantifiedFieldChunk(id, newFvf, perm, invs, initialCond, singletonRcvr, hints) + override def applyCondition(newCond: Term) = QuantifiedFieldChunk(id, fvf, terms.And(newCond, condition), permValue, invs, singletonRcvr, hints) + override def permMinus(newPerm: Term) = QuantifiedFieldChunk(id, fvf, condition, PermMinus(permValue, newPerm), invs, singletonRcvr, hints) + override def permPlus(newPerm: Term) = QuantifiedFieldChunk(id, fvf, condition, PermPlus(permValue, newPerm), invs, singletonRcvr, hints) + override def withSnapshotMap(newFvf: Term) = QuantifiedFieldChunk(id, newFvf, condition, permValue, invs, singletonRcvr, hints) + override def withPerm(newPerm: Term) = { + // TODO: This implementation only replaces permValue, so if the caller assumes that it'll set the perm value period, it is + // only correct if newPerm is zero when condition is false. + QuantifiedFieldChunk(id, fvf, condition, newPerm, invs, singletonRcvr, hints) + } override lazy val toString = s"${terms.Forall} ${`?r`} :: ${`?r`}.$id -> $fvf # $perm" } @@ -98,26 +113,30 @@ case class QuantifiedFieldChunk(id: BasicChunkIdentifier, case class QuantifiedPredicateChunk(id: BasicChunkIdentifier, quantifiedVars: Seq[Var], psf: Term, - perm: Term, + condition: Term, + permValue: Term, invs: Option[InverseFunctions], - initialCond: Option[Term], singletonArgs: Option[Seq[Term]], hints: Seq[Term] = Nil) extends QuantifiedBasicChunk { require(psf.sort.isInstanceOf[terms.sorts.PredicateSnapFunction], s"Quantified predicate chunk values must be of sort PredicateSnapFunction ($psf), but found ${psf.sort}") - require(perm.sort == sorts.Perm, s"Permissions $perm must be of sort Perm, but found ${perm.sort}") + require(permValue.sort == sorts.Perm, s"Permissions $permValue must be of sort Perm, but found ${permValue.sort}") override val resourceID = PredicateID + override val perm = Ite(condition, permValue, NoPerm) override def snapshotMap: Term = psf override def singletonArguments: Option[Seq[Term]] = singletonArgs override def valueAt(args: Seq[Term]) = PredicateLookup(id.name, psf, args) - override def withPerm(newPerm: Term) = QuantifiedPredicateChunk(id, quantifiedVars, psf, newPerm, invs, initialCond, singletonArgs, hints) - override def withSnapshotMap(newPsf: Term) = QuantifiedPredicateChunk(id, quantifiedVars, newPsf, perm, invs, initialCond, singletonArgs, hints) + override def applyCondition(newCond: Term) = QuantifiedPredicateChunk(id, quantifiedVars, psf, terms.And(newCond, condition), permValue, invs, singletonArgs, hints) + override def permMinus(newPerm: Term) = QuantifiedPredicateChunk(id, quantifiedVars, psf, condition, PermMinus(permValue, newPerm), invs, singletonArgs, hints) + override def permPlus(newPerm: Term) = QuantifiedPredicateChunk(id, quantifiedVars, psf, condition, PermPlus(permValue, newPerm), invs, singletonArgs, hints) + override def withPerm(newPerm: Term) = QuantifiedPredicateChunk(id, quantifiedVars, psf, condition, newPerm, invs, singletonArgs, hints) + override def withSnapshotMap(newPsf: Term) = QuantifiedPredicateChunk(id, quantifiedVars, newPsf, condition, permValue, invs, singletonArgs, hints) override lazy val toString = s"${terms.Forall} ${quantifiedVars.mkString(",")} :: $id(${quantifiedVars.mkString(",")}) -> $psf # $perm" } @@ -126,7 +145,6 @@ case class QuantifiedMagicWandChunk(id: MagicWandIdentifier, wsf: Term, perm: Term, invs: Option[InverseFunctions], - initialCond: Option[Term], singletonArgs: Option[Seq[Term]], hints: Seq[Term] = Nil) extends QuantifiedBasicChunk { @@ -140,9 +158,11 @@ case class QuantifiedMagicWandChunk(id: MagicWandIdentifier, override def singletonArguments: Option[Seq[Term]] = singletonArgs override def valueAt(args: Seq[Term]) = PredicateLookup(id.toString, wsf, args) - - override def withPerm(newPerm: Term) = QuantifiedMagicWandChunk(id, quantifiedVars, wsf, newPerm, invs, initialCond, singletonArgs, hints) - override def withSnapshotMap(newWsf: Term) = QuantifiedMagicWandChunk(id, quantifiedVars, newWsf, perm, invs, initialCond, singletonArgs, hints) + override def applyCondition(newCond: Term) = withPerm(Ite(newCond, perm, NoPerm)) + override def permMinus(newPerm: Term) = withPerm(PermMinus(perm, newPerm)) + override def permPlus(newPerm: Term) = withPerm(PermPlus(perm, newPerm)) + def withPerm(newPerm: Term) = QuantifiedMagicWandChunk(id, quantifiedVars, wsf, newPerm, invs, singletonArgs, hints) + override def withSnapshotMap(newWsf: Term) = QuantifiedMagicWandChunk(id, quantifiedVars, newWsf, perm, invs, singletonArgs, hints) override lazy val toString = s"${terms.Forall} ${quantifiedVars.mkString(",")} :: $id(${quantifiedVars.mkString(",")}) -> $wsf # $perm" } @@ -175,6 +195,15 @@ case class MagicWandChunk(id: MagicWandIdentifier, override val resourceID = MagicWandID + override def applyCondition(newCond: Term) = + withPerm(Ite(newCond, perm, NoPerm)) + + override def permMinus(newPerm: Term) = + withPerm(PermMinus(perm, newPerm)) + + override def permPlus(newPerm: Term) = + withPerm(PermPlus(perm, newPerm)) + override def withPerm(newPerm: Term) = MagicWandChunk(id, bindings, args, snap, newPerm) override def withSnap(newSnap: Term) = newSnap match { case s: MagicWandSnapshot => MagicWandChunk(id, bindings, args, s, perm) diff --git a/src/main/scala/state/State.scala b/src/main/scala/state/State.scala index 8d6a6294b..348229b68 100644 --- a/src/main/scala/state/State.scala +++ b/src/main/scala/state/State.scala @@ -279,7 +279,7 @@ object State { h map (c => { c match { case c: GeneralChunk => - c.withPerm(Ite(cond, c.perm, NoPerm)) + c.applyCondition(cond) case _ => sys.error("Chunk type not conditionalizable.") } }) diff --git a/src/test/resources/kinduct/basic_while.vpr b/src/test/resources/kinduct/basic_while.vpr index 2ccd1befe..30aeaec3e 100644 --- a/src/test/resources/kinduct/basic_while.vpr +++ b/src/test/resources/kinduct/basic_while.vpr @@ -140,3 +140,67 @@ method t11(r: Ref) returns () j := j+1 } } + +method justChecking(r: Ref) returns () + requires acc(r.f, write) +{ + var j: Int := 2 + while (j < (r.f)) + invariant acc(r.f, 1/2) + { + j := j+1 + } + assert perm(r.f) == write + //:: ExpectedOutput(assert.failed:assertion.false) + assert false +} + +method justChecking2(r: Ref) returns () + requires acc(r.f, write) +{ + var j: Int := 2 + assume r.f == 32 + while (j < (r.f)) + invariant acc(r.f, 1/2) + { + assume r.f == 34 + j := j+1 + } + assert perm(r.f) == write + assert false +} + +method justChecking3(r: Ref) returns () + requires acc(r.f, write) +{ + var j: Int := 2 + assume r.f == 32 + while (j < (r.f)) + invariant acc(r.f, 1/2) + { + r.f := 34 + j := j+1 + } + assert perm(r.f) == write + assert r.f == 32 || r.f == 34 + assert r.f == 34 + //:: ExpectedOutput(assert.failed:assertion.false) + assert r.f == 32 +} + +method justChecking4(r: Ref) returns () + requires acc(r.f, write) +{ + var j: Int + assume r.f == 32 + while (j < (r.f)) + invariant acc(r.f, 1/2) + { + r.f := 34 + j := j+1 + } + assert perm(r.f) == write + assert r.f == 32 || r.f == 34 + //:: ExpectedOutput(assert.failed:assertion.false) + assert r.f == 34 +} \ No newline at end of file diff --git a/src/test/resources/kinduct/forceQP/basic_while.vpr b/src/test/resources/kinduct/forceQP/basic_while.vpr index c7410b11d..d1c4a67ce 100644 --- a/src/test/resources/kinduct/forceQP/basic_while.vpr +++ b/src/test/resources/kinduct/forceQP/basic_while.vpr @@ -156,3 +156,71 @@ method t11(r: Ref) returns () j := j+1 } } + +method justChecking(r: Ref) returns () + requires acc(r.f, write) +{ + var j: Int := 2 + forceQPs() + while (j < (r.f)) + invariant acc(r.f, 1/2) + { + j := j+1 + } + assert perm(r.f) == write + //:: ExpectedOutput(assert.failed:assertion.false) + assert false +} + +method justChecking2(r: Ref) returns () + requires acc(r.f, write) +{ + var j: Int := 2 + assume r.f == 32 + forceQPs() + while (j < (r.f)) + invariant acc(r.f, 1/2) + { + assume r.f == 34 + j := j+1 + } + assert perm(r.f) == write + assert false +} + +method justChecking3(r: Ref) returns () + requires acc(r.f, write) +{ + var j: Int := 2 + assume r.f == 32 + forceQPs() + while (j < (r.f)) + invariant acc(r.f, 1/2) + { + r.f := 34 + j := j+1 + } + assert perm(r.f) == write + assert r.f == 32 || r.f == 34 + assert r.f == 34 + //:: ExpectedOutput(assert.failed:assertion.false) + assert r.f == 32 +} + +method justChecking4(r: Ref) returns () + requires acc(r.f, write) +{ + var j: Int + assume r.f == 32 + forceQPs() + while (j < (r.f)) + invariant acc(r.f, 1/2) + { + r.f := 34 + j := j+1 + } + assert perm(r.f) == write + assert r.f == 32 || r.f == 34 + //:: ExpectedOutput(assert.failed:assertion.false) + assert r.f == 34 +} \ No newline at end of file