diff --git a/src/main/scala/rules/Consumer.scala b/src/main/scala/rules/Consumer.scala index d5285f8bc..c34a36312 100644 --- a/src/main/scala/rules/Consumer.scala +++ b/src/main/scala/rules/Consumer.scala @@ -55,7 +55,7 @@ trait ConsumptionRules extends SymbolicExecutionRules { def consumes(s: State, as: Seq[ast.Exp], pvef: ast.Exp => PartialVerificationError, - v: Verifier) + v: Verifier, isAssert: Boolean = false) (Q: (State, Term, Verifier) => VerificationResult) : VerificationResult } @@ -84,7 +84,7 @@ object consumer extends ConsumptionRules { def consumes(s: State, as: Seq[ast.Exp], pvef: ast.Exp => PartialVerificationError, - v: Verifier) + v: Verifier, isAssert: Boolean = false) (Q: (State, Term, Verifier) => VerificationResult) : VerificationResult = { @@ -100,7 +100,7 @@ object consumer extends ConsumptionRules { }) consumeTlcs(s, s.h, allTlcs.result(), allPves.result(), v)((s1, h1, cHeap, snap1, v1) => { - val s2 = s1.copy(h = h1, + val s2 = s1.copy(h = if (isAssert) h1 + cHeap else h1, partiallyConsumedHeap = s.partiallyConsumedHeap, consumedHeapParts = Some(cHeap)) Q(s2, snap1, v1) @@ -467,6 +467,7 @@ object consumer extends ConsumptionRules { case _ => evalAndAssert(s, a, pve, v)((s1, t, v1) => { + val old = s.consumedHeapParts Q(s1, h, Heap(), t, v1) }) } @@ -560,8 +561,7 @@ object consumer extends ConsumptionRules { failure combine QS(s3, v2) } else failure}}) })((s4, v4) => { - val s5 = s4.copy(h = s.h, - reserveHeaps = s.reserveHeaps, + val s5 = s4.copy(reserveHeaps = s.reserveHeaps, exhaleExt = s.exhaleExt) Q(s5, Unit, v4) }) diff --git a/src/main/scala/rules/Evaluator.scala b/src/main/scala/rules/Evaluator.scala index d15518c5f..4584a495c 100644 --- a/src/main/scala/rules/Evaluator.scala +++ b/src/main/scala/rules/Evaluator.scala @@ -694,6 +694,99 @@ object evaluator extends EvaluationRules { Q(s1, tQuant, v1) } + case fapp@ast.FuncApp(funcName, eArgs) if s.loopPhaseStack.nonEmpty && s.loopPhaseStack.head._1 != LoopPhases.Checking => + val func = s.program.findFunction(funcName) + evals2(s, eArgs, Nil, _ => pve, v)((s1, tArgs, v1) => { + // bookkeeper.functionApplications += 1 + val joinFunctionArgs = tArgs //++ c2a.quantifiedVariables.filterNot(tArgs.contains) + /* TODO: Does it matter that the above filterNot does not filter out quantified + * variables that are not "raw" function arguments, but instead are used + * in an expression that is used as a function argument? + * E.g., in + * forall i: Int :: fun(i*i) + * the above filterNot will not remove i from the list of already + * used quantified variables because i does not match i*i. + * Hence, the joinedFApp will take two arguments, namely, i*i and i, + * although the latter is not necessary. + */ + joiner.join[Term, Term](s1, v1, false)((s2, v2, QB) => { + val pres = func.pres.map(_.transform { + /* [Malte 2018-08-20] Two examples of the test suite, one of which is the regression + * for Carbon issue #210, fail if the subsequent code that strips out triggers from + * exhaled function preconditions, is commented. The code was originally a work-around + * for Silicon issue #276. Removing triggers from function preconditions is OK-ish + * because they are consumed (exhaled), i.e. asserted. However, the triggers are + * also used to internally generated quantifiers, e.g. related to QPs. My hope is that + * this hack is no longer needed once heap-dependent triggers are supported. + */ + case q: ast.Forall => q.copy(triggers = Nil)(q.pos, q.info, q.errT) + }) + /* Formal function arguments are instantiated with the corresponding actual arguments + * by adding the corresponding bindings to the store. To avoid formals in error messages + * and to report actuals instead, we have two choices: the first is two attach a reason + * transformer to the partial verification error, as done below; the second is to attach + * a node transformer to every formal, as illustrated by NodeBacktranslationTests.scala. + * The first approach is slightly simpler and suffices here, though. + */ + val fargs = func.formalArgs.map(_.localVar) + val formalsToActuals: Map[ast.LocalVar, ast.Exp] = fargs.zip(eArgs).to(Map) + val exampleTrafo = CounterexampleTransformer({ + case ce: SiliconCounterexample => ce.withStore(s2.g) + case ce => ce + }) + val pvePre = + ErrorWrapperWithExampleTransformer(PreconditionInAppFalse(fapp).withReasonNodeTransformed(reasonOffendingNode => + reasonOffendingNode.replace(formalsToActuals)), exampleTrafo) + val s3 = s2.copy(g = Store(fargs.zip(tArgs)), + recordVisited = true, + functionRecorder = s2.functionRecorder.changeDepthBy(+1), + /* Temporarily disable the recorder: when recording (to later on + * translate a particular function fun) and a function application + * fapp is hit, then there is no need to record any information + * about assertions from fapp's precondition since the latter is not + * translated as part of the translation of fun. + * Recording such information is even potentially harmful if formals + * are not syntactically replaced by actuals but rather bound to + * them via the store. Consider the following function: + * function fun(x: Ref) + * requires foo(x) // foo is another function + * ... + * { ... fun(x.next) ...} + * For fun(x)'s precondition, a mapping from foo(x) to a snapshot is + * recorded. When fun(x.next) is hit, its precondition is consumed, + * but without substituting actuals for formals, continuing to + * record mappings would add another mapping from foo(x) (which is + * actually foo(x.next)) to some potentially different snapshot. + * When translating fun(x) to an axiom, the snapshot of foo(x) from + * fun(x)'s precondition will be the branch-condition-dependent join + * of the recorded snapshots - which is wrong (probably only + * incomplete). + */ + smDomainNeeded = true, + moreJoins = false) + consumes(s3, pres, _ => pvePre, v2, true)((s4, snap, v3) => { + val snap1 = snap.convert(sorts.Snap) + val preFApp = App(functionSupporter.preconditionVersion(v3.symbolConverter.toFunction(func)), snap1 :: tArgs) + v3.decider.assume(preFApp) + val tFApp = App(v3.symbolConverter.toFunction(func), snap1 :: tArgs) + val fr5 = + s4.functionRecorder.changeDepthBy(-1) + .recordSnapshot(fapp, v3.decider.pcs.branchConditions, snap1) + val s5 = s4.copy( + g = s2.g, + recordVisited = s2.recordVisited, + functionRecorder = fr5, + smDomainNeeded = s2.smDomainNeeded, + hackIssue387DisablePermissionConsumption = s.hackIssue387DisablePermissionConsumption, + moreJoins = s2.moreJoins) + QB(s5, tFApp, v3) + }) + /* TODO: The join-function is heap-independent, and it is not obvious how a + * joined snapshot could be defined and represented + */ + })(joinKInd(v1.symbolConverter.toSort(func.typ), s"joined_${func.name}", joinFunctionArgs, v1))(Q) + }) + case fapp @ ast.FuncApp(funcName, eArgs) => val func = s.program.findFunction(funcName) evals2(s, eArgs, Nil, _ => pve, v)((s1, tArgs, v1) => { @@ -1405,6 +1498,43 @@ object evaluator extends EvaluationRules { } } + private def joinKInd(joinSort: Sort, + joinFunctionName: String, + joinFunctionArgs: Seq[Term], + v: Verifier) + (entries: Seq[JoinDataEntry[Term]]) + : (State, Term) = { + + assert(entries.nonEmpty, "Expected at least one join data entry") + + entries match { + case Seq(entry) => + /* If there is only one entry, i.e. one branch to join, it is assumed that the other + * branch was infeasible, and the branch conditions are therefore ignored. + */ + (entry.s, entry.data) + case _ => + val quantifiedVarsSorts = joinFunctionArgs.map(_.sort) + val joinSymbol = v.decider.fresh(joinFunctionName, quantifiedVarsSorts, joinSort) + val joinTerm = App(joinSymbol, joinFunctionArgs) + + val joinDefEqs = entries map (entry => + Implies(And(entry.pathConditions.branchConditions), joinTerm === entry.data)) + + var sJoined = if (entries.length == 2) { + State.merge(entries(0).s, entries(0).pathConditions, entries(1).s, entries(1).pathConditions) + }else { + val start = State.merge(entries(0).s, entries(0).pathConditions, entries(1).s, entries(1).pathConditions) + entries.tail.tail.foldLeft(start)((sAcc, entry) => State.merge(entry.s, And(entry.pathConditions.branchConditions), sAcc, True)) + } + sJoined = sJoined.copy(functionRecorder = sJoined.functionRecorder.recordPathSymbol(joinSymbol)) + + v.decider.assume(joinDefEqs) + + (sJoined, joinTerm) + } + } + private def evalHeapTrigger(s: State, exps: Seq[ast.Exp], pve: PartialVerificationError, v: Verifier) (Q: (State, Seq[Term], Verifier) => VerificationResult) : VerificationResult = { var triggers: Seq[Term] = Seq() diff --git a/src/main/scala/rules/Executor.scala b/src/main/scala/rules/Executor.scala index fe64719e6..b71a5b953 100644 --- a/src/main/scala/rules/Executor.scala +++ b/src/main/scala/rules/Executor.scala @@ -321,44 +321,46 @@ object executor extends ExecutionRules { case _ if Verifier.config.kinduction.isSupplied => val (phase, kRemaining, loopHeap) = s.loopPhaseStack.head val edges = s.methodCfg.outEdges(block) - consumes(s, invs, e => LoopInvariantNotPreserved(e), v)((_, _, v) => + consumes(s, invs, e => LoopInvariantNotPreserved(e), v, true)((sp, _, v) => { + val shuh = s + println("??") phase match { case LoopPhases.Transferring => if (kRemaining > 1) { - val sNew = s.copy(loopPhaseStack = (LoopPhases.Transferring, kRemaining - 1, loopHeap) +: s.loopPhaseStack.tail) + val sNew = sp.copy(loopPhaseStack = (LoopPhases.Transferring, kRemaining - 1, loopHeap) +: sp.loopPhaseStack.tail) execs(sNew, stmts, v)((s4, v3) => { follows(s4, edges, WhileFailed, v3, None)(Q) }) } else { /* Havoc local variables that are assigned to in the loop body */ - val wvs = s.methodCfg.writtenVars(block) + val wvs = sp.methodCfg.writtenVars(block) /* TODO: BUG: Variables declared by LetWand show up in this list, but shouldn't! */ - val gBody = Store(wvs.foldLeft(s.g.values)((map, x) => map.updated(x, v.decider.fresh(x)))) - val sNew = s.copy(g = gBody, h = Heap(), - loopPhaseStack = (LoopPhases.Assuming, Verifier.config.kinduction(), loopHeap) +: s.loopPhaseStack.tail) + val gBody = Store(wvs.foldLeft(sp.g.values)((map, x) => map.updated(x, v.decider.fresh(x)))) + val sNew = sp.copy(g = gBody, h = Heap(), + loopPhaseStack = (LoopPhases.Assuming, Verifier.config.kinduction(), loopHeap) +: sp.loopPhaseStack.tail) execs(sNew, stmts, v)((s4, v3) => { follows(s4, edges, WhileFailed, v3, None)(Q) }) } case LoopPhases.Assuming => if (kRemaining > 1) { - val sNew = s.copy(loopPhaseStack = (LoopPhases.Assuming, kRemaining - 1, loopHeap) +: s.loopPhaseStack.tail) + val sNew = sp.copy(loopPhaseStack = (LoopPhases.Assuming, kRemaining - 1, loopHeap) +: sp.loopPhaseStack.tail) execs(sNew, stmts, v)((s4, v3) => { follows(s4, edges, WhileFailed, v3, None)(Q) }) } else { - val sNew = s.copy(loopPhaseStack = (LoopPhases.Checking, 1, loopHeap) +: s.loopPhaseStack.tail) + val sNew = sp.copy(loopPhaseStack = (LoopPhases.Checking, 1, loopHeap) +: sp.loopPhaseStack.tail) execs(sNew, stmts, v)((s4, v3) => { follows(s4, edges, WhileFailed, v3, None)(Q) }) } case LoopPhases.Checking => val outEdges = edges filter(_.kind == cfg.Kind.Out) - execs(s, stmts, v)((s4, v3) => { + execs(sp, stmts, v)((s4, v3) => { follows(s4, outEdges, WhileFailed, v3, None)(Q) }) - } + }} ) case _ => diff --git a/src/main/scala/state/State.scala b/src/main/scala/state/State.scala index 18cf78564..3bb590268 100644 --- a/src/main/scala/state/State.scala +++ b/src/main/scala/state/State.scala @@ -301,6 +301,12 @@ object State { } def merge(s1: State, pc1: RecordedPathConditions, s2: State, pc2: RecordedPathConditions): State = { + val conditions1 = And(pc1.branchConditions) + val conditions2 = And(pc2.branchConditions) + merge(s1, conditions1, s2, conditions2) + } + + def merge(s1: State, conditions1: Term, s2: State, conditions2: Term): State = { s1 match { /* Decompose state s1 */ case State(g1, h1, program, member, @@ -358,9 +364,6 @@ object State { val smDomainNeeded3 = smDomainNeeded1 || smDomainNeeded2 - val conditions1 = And(pc1.branchConditions) - val conditions2 = And(pc2.branchConditions) - val mergeStore = (g1: Store, g2: Store) => { Store(mergeMaps(g1.values, conditions1, g2.values, conditions2) ((_, _) => { diff --git a/src/test/resources/kinduct/funcAndPartial.vpr b/src/test/resources/kinduct/funcAndPartial.vpr new file mode 100644 index 000000000..6fc15bdee --- /dev/null +++ b/src/test/resources/kinduct/funcAndPartial.vpr @@ -0,0 +1,197 @@ + + + + +field f: Int +field g: Ref + +function getF(r: Ref): Int + requires acc(r.f, 1/2) +{ + r.f +} + +function getFFull(r: Ref): Int + requires acc(r.f, 1/1) +{ + r.f +} + +method mFuncFrame(r1: Ref, r2: Ref, r3: Ref, b: Bool) + requires acc(r1.f) && acc(r2.f, 1/2) && acc(r3.f, 1/2) + requires acc(r2.g) +{ + var bp: Bool := b + r1.f := 0 + + while (bp) + { + var tmp: Int + tmp := getF(r1) + bp := havocBool() + } + assert r1.f == 0 + //:: ExpectedOutput(assert.failed:assertion.false) + assert false +} + +method mFuncFrame2(r1: Ref, r2: Ref, r3: Ref, b: Bool) + requires acc(r1.f) && acc(r2.f, 1/2) && acc(r3.f, 1/2) + requires acc(r2.g) +{ + var bp: Bool := b + r1.f := 0 + + while (bp) + { + var tmp: Int + tmp := getFFull(r1) + bp := havocBool() + } + //:: ExpectedOutput(assert.failed:assertion.false) + assert r1.f == 0 +} + +method mFldInv(r1: Ref, r2: Ref, r3: Ref, b: Bool) + requires acc(r1.f) && acc(r2.f, 1/2) && acc(r3.f, 1/2) + requires acc(r2.g) +{ + var bp: Bool := b + r1.f := 0 + + while (bp) + invariant r1.f >= 0 + { + var tmp: Int + bp := havocBool() + } + assert r1.f == 0 + //:: ExpectedOutput(assert.failed:assertion.false) + assert false +} + +method mFldInvFail(r1: Ref, r2: Ref, r3: Ref, b: Bool) + requires acc(r1.f) && acc(r2.f, 1/2) && acc(r3.f, 1/2) + requires acc(r2.g) +{ + var bp: Bool := b + r1.f := 0 + + while (bp) + //:: ExpectedOutput(invariant.not.preserved:assertion.false) + invariant r1.f >= 0 + { + var tmp: Int + if (r1.f == 0) { + r1.f := r1.f + 1 + } else { + r1.f := r1.f - 3 + } + bp := havocBool() + } +} + +method mFldInv2(r1: Ref, r2: Ref, r3: Ref, b: Bool) + requires acc(r1.f) && acc(r2.f, 1/2) && acc(r3.f, 1/2) + requires acc(r2.g) +{ + var bp: Bool := b + r1.f := 0 + + while (bp) + invariant acc(r1.f) && r1.f >= 0 + { + var tmp: Int + bp := havocBool() + } + var after: Int + after := r1.f + r1.f := 17 + assert after >= 0 + //:: ExpectedOutput(assert.failed:assertion.false) + assert after == 0 +} + +method mFuncInv2(r1: Ref, r2: Ref, r3: Ref, b: Bool) + requires acc(r1.f) && acc(r2.f, 1/2) && acc(r3.f, 1/2) + requires acc(r2.g) +{ + var bp: Bool := b + r1.f := 0 + + while (bp) + invariant acc(r1.f) && getF(r1) >= 0 + { + var tmp: Int + bp := havocBool() + } + var after: Int + after := r1.f + r1.f := 17 + assert after >= 0 + //:: ExpectedOutput(assert.failed:assertion.false) + assert after == 0 +} + +method mFldInvFail2(r1: Ref, r2: Ref, r3: Ref, b: Bool) + requires acc(r1.f) && acc(r2.f, 1/2) && acc(r3.f, 1/2) + requires acc(r2.g) +{ + var bp: Bool := b + r1.f := 0 + + while (bp) + //:: ExpectedOutput(invariant.not.preserved:assertion.false) + invariant acc(r1.f) && r1.f >= 0 + { + var tmp: Int + if (r1.f == 0) { + r1.f := r1.f + 1 + } else { + r1.f := r1.f - 3 + } + bp := havocBool() + } +} + +method mFuncInv(r1: Ref, r2: Ref, r3: Ref, b: Bool) + requires acc(r1.f) && acc(r2.f, 1/2) && acc(r3.f, 1/2) + requires acc(r2.g) +{ + var bp: Bool := b + r1.f := 0 + + while (bp) + invariant getF(r1) >= 0 + { + var tmp: Int + bp := havocBool() + } + assert r1.f == 0 + //:: ExpectedOutput(assert.failed:assertion.false) + assert false +} + +method mFuncInvFail(r1: Ref, r2: Ref, r3: Ref, b: Bool) + requires acc(r1.f) && acc(r2.f, 1/2) && acc(r3.f, 1/2) + requires acc(r2.g) +{ + var bp: Bool := b + r1.f := 0 + + while (bp) + //:: ExpectedOutput(invariant.not.preserved:assertion.false) + invariant getF(r1) >= 0 + { + var tmp: Int + if (r1.f == 0) { + r1.f := r1.f + 1 + } else { + r1.f := r1.f - 3 + } + bp := havocBool() + } +} + +method havocBool() returns (r: Bool) +function detBool(): Bool \ No newline at end of file