Add debug option to dump blocker graph
Created by: gsps
Adds a debug section blocker-graph
that dumps the (non-strict) implication graph among all blocking literals. The current graph is dumped at the end of checkAssumptions
and saved in blocker-graphs/*file*-*n*.dot
.
Nodes that correspond to defBlocker
s also contain the corresponding function name and the call site's position. The positional information is unreliable, since we only store the call site position when the callee's FunctionTemplate
is first cached (the cache key being the TypedFunDef
).
As an example, the following program requires multiple unfolding steps to prove the assertion in testUnfoldMe
:
object MustUnfoldThriceExample {
def unfoldMe(xs: List[BigInt]): BigInt = {
require(xs.forall(_ >= 0))
xs match {
case Nil() => BigInt(0)
case Cons(x, xs0) => x + unfoldMe(xs0)
}
} ensuring (_ >= 0)
def testUnfoldMe(xs: List[BigInt]): Unit = {
require(xs.size >= 3 && xs.forall(_ >= 0))
val sum = unfoldMe(xs)
assert(sum >= xs(0) + xs(1) + xs(2))
}
}
Running with --debug=blocker-graph
yields multiple .dot
files, one of which corresponds to the assertion's VC:
must-unfold-thrice.pdf
@samarion Any preference on where to move the dot-graph-dumping code that new lives in checkAssumptions
?