Skip to content

Commit

Permalink
WIP on function applications and partial invariants
Browse files Browse the repository at this point in the history
  • Loading branch information
@marcoeilers
marcoeilers committed Oct 24, 2023
1 parent d3a29fb commit ee0c8fa
Show file tree
Hide file tree
Showing 5 changed files with 350 additions and 18 deletions.
10 changes: 5 additions & 5 deletions src/main/scala/rules/Consumer.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
}
Expand Down Expand Up @@ -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 = {

Expand All @@ -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)
Expand Down Expand Up @@ -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)
})
}
Expand Down Expand Up @@ -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)
})
Expand Down
130 changes: 130 additions & 0 deletions src/main/scala/rules/Evaluator.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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) => {
Expand Down Expand Up @@ -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()
Expand Down
22 changes: 12 additions & 10 deletions src/main/scala/rules/Executor.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 _ =>
Expand Down
9 changes: 6 additions & 3 deletions src/main/scala/state/State.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down Expand Up @@ -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)
((_, _) => {
Expand Down
Loading

0 comments on commit ee0c8fa

Please sign in to comment.