Transcript slides - SAS 2011

Satisfiability Modulo Recursive Programs
Philippe Suter, Ali Sinan Köksal, Viktor Kuncak
École Polytechnique Fédérale de Lausanne, Switzerland
Leon(Online)
• A verifier for Scala programs.
• The programming and specification languages
are the same purely functional subset.
def content(t: Tree) = t match {
case Leaf ⇒ Set.empty
case Node(l, v, r) ⇒
(content(l) ++ content(r)) + e
}
def insert(e: Int, t: Tree) = t match {
case Leaf ⇒ Node(Leaf, e, Leaf)
case Node(l, v, r) if e < v ⇒
Node(insert(e, l), v, r)
case Node(l, v, r) if e > v ⇒
Node(l, v, insert(e, r))
case _ ⇒ t
} ensuring(
res ⇒ content(res) == content(t) + e)
~$ ./demo
…of quantifier-free formulas
in a decidable base theory…
Satisfiability Modulo
Recursive Programs
…pure, total, deterministic, firstorder and terminating on all inputs…
Satisfiability Modulo Recursive Programs
• Semi-decidable problem of great interest:
– applications in verification, testing, theorem
proving, constraint logic programming, …
• Our algorithm always finds counter-examples
when they exist, and will also find
assume/guarantee style proofs.
• It is a decision procedure for infinitely and
sufficiently surjective abstraction functions.
• We implemented it as a part of a verification
system for a purely functional subset of Scala.
Proving/Disproving Modulo
Recursive Programs
Proving by Inlining
def size(lst: List) = lst match {
case Nil ⇒ 0
case Cons(_, _) ⇒ 1
} ensuring(res ⇒ res ≥ 0)
Convert pattern-matching,
negate.
(if(lst = Nil) 0 else 1) < 0
Unsatisfiable.
Proving by Inlining
def size(lst: List) = lst match {
case Nil ⇒ 0
case Cons(x, xs) ⇒ 1 + size(xs)
} ensuring(res ⇒ res ≥ 0)
Convert pattern-matching,
negate,
treat functions as uninterpreted.
(if(lst = Nil) 0 else 1 + size(lst.tail)) < 0
Satisfiable.
(e.g. for size(Nil) = -2)
Inline post-condition.
(if(lst = Nil) 0 else 1 + size(lst.tail)) < 0 ∧
size(lst.tail) ≥ 0
Unsatisfiable.
Disproving by Inlining
def prop(lst: List) = {
size(lst) ≥ 0
} ensuring(res ⇒ res)
def size(lst: List) = lst match {
case Nil ⇒ -1
case Cons(x, xs) ⇒ 1 + size(xs)
}
Negate,
treat functions as uninterpreted.
size(lst) < 0
Satisfiable.
(e.g. lst = [0], size([0]) = -1)
Inline definition of size(lst).
size(lst) < 0 ∧
size(lst) = (if(lst = Nil) -1 else 1 + size(lst.tail))
Satisfiable.
(e.g. lst = [0,1], size([1]) = -2)
Disproving with Inlining
size(lst)
?
size(lst.tail)
?
size(lst.tail.tail)
?
…
There are always unknown branches in the evaluation tree.
We can never be sure that there exists no smaller solution.
Branch Rewriting
size(lst) = if(lst = Nil) {
-1
} else {
1 + size(lst.tail)
}
size(lst) = ite1
∧ p1 ⇔ lst = Nil
∧ p1 ⇒ ite1 = -1
∧ ¬p1 ⇒ ite1 = 1 + size(lst.tail)
…
∧ p1
size(lst)
?
p1
¬p1
• Satisfiable assignments do not
depend on unknown values.
• Unsatisfiable answers have two
possible meanings.
Algorithm
(φ, B) = unroll(φ, _)
while(true) {
solve(φ ∧ B) match {
case “SAT” ⇒ return “SAT”
Some literals in B may be
implied by φ : no need to
unroll what they guard.
case “UNSAT” ⇒ solve(φ) match {
case “UNSAT” ⇒ return “UNSAT”
case “SAT” ⇒ (φ, B) = unroll(φ, B)
}
Inlining must be fair
}
}
“I’m feeling lucky”
Inlines some postconditions and bodies of function
applications that were guarded by a literal in B,
returns the new formula and new set of guards B.
Completeness for Counter-Examples
• Let a1,… an be the free variables of φ, and c1,…,cn
be a counter-example to φ.
• Let T be the evaluation tree of φ[a1→c1, …,
an→cn].
?
T:
?
?
?
• Eventually, the algorithm will reach a point where
T is covered.
Pattern-Matching Exhaustiveness
• We generate a formula that expresses that no
case matches, and prove it unsatisfiable.
def zip(l1: List, l2: List) : PairList = {
require(size(l1) == size(l2))
l1 match {
case Nil ⇒ PNil
case Cons(x, xs) ⇒ l2 match {
case Cons(y, ys) ⇒
PCons(P(x, y), zip(xs, ys))
}
}
}
size(l1) == size(l2)
∧ l1 ≠ Nil
∧ l2 == Nil
Unsatisfiable.
Termination for Sufficiently
Surjective Abstraction Functions
Sufficiently Surjective Abstractions
• The algorithm terminates, and is thus a
decision procedure for the case of infinitely
and
sufficiently
surjective
abstraction
functions.
def α(tree: Tree) : C = tree match {
case Leaf() ⇒ empty
case Node(l, v, r) ⇒ combine(α(l), v, α(r))
}
[
]
P. Suter, M. Dotta, V. Kuncak, Decision Procedures for Algebraic
Data Types with Abstractions, POPL 2010
«
»
many trees for which this
«There are only finitely
»
does not hold.
If one tree is mapped by α into an element, then
many other trees are mapped to the same one.
content
∅
5
5
5
1
1
1
1
5
content
…
{ 1, 5 }
def content(tree: Tree) : Set[Int] = tree match {
case Leaf() ⇒ Set.empty
case Node(l, v, r) ⇒ (content(l) ++ content(r)) + v
}
def allEven(list: List) : Boolean = list match {
case Nil() ⇒ true
case Cons(x, xs) ⇒ (x % 2 == 0) && allEven(list)
}
def max(tree: Tree) : Option[Int]= tree match {
case Leaf() ⇒ None
case Node(l, v, r) ⇒ Some(max(l), max(r)) match {
case (None, None) ⇒ Some(v)
case (Some(lm), None) ⇒ max(lm, v)
case (None, Some(rm)) ⇒ max(rm, v)
case (Some(lm), Some(rm)) ⇒ (max(lm, rm), v)
})}
Sufficiently Surjective Abstractions in the Wild
«
In the context of a project to reason about a
domain specific language called Guardol for
XML message processing applications […the]
procedure has allowed us to prove a number of
interesting things […], so I'm extremely grateful
for it.
»
Mike Whalen
(University of Minnesota & Rockwell Collins)
A Tale of Two Techniques
φ ≡ … α(t) …
t≡
t≡
t≡
t≡
t≡
∨ ψ(α(t))
• For catamorphisms, unrolling α
corresponds to enumerating
potential counter-examples by the
size of their tree.
• When all required trees have
been considered, a formula at
least as strong as ψ(α(t)) is
derived by the solver.
Verification System
Leon(Online)
www
.scala
compiler
-
prunes out
rewrites functions
generate VCs
solve VCs
(generate testcases)
final report
Leon(Online)
• Proves that all match expressions are exhaustive.
• For each function, proves that the pre-condition
implies the post-condition.
• Proves that all function invocations satisfy the
preconditions.
(
Bonus features:
)
• Can generate test-cases satisfying complex preconditions
• Outputs to Isabelle format for manual proofs
(Some) Experimental Results
Benchmark
LoC
#Funs.
#VCs.
Time (s)
ListOperations
107
15
27
0.76
AssociativeList
50
5
11
0.23
InsertionSort
99
6
15
0.42
RedBlackTrees
117
11
24
3.73
PropositionalLogic
86
9
23
2.36
AmortizedQueue
124
14
32
3.37
94
11
23
0.79
677
71
155
11.66
VSComp
Functional correctness properties of data structures: red-black trees implement a set
and maintain height invariants, associative list has read-over-write property, insertion
sort returns a sorted list of identical content, amortized queue implements a balanced
queue, etc.
Related Work
• SMT Solvers + axioms
– can be very efficient for well-formed axioms
– in general, no guarantee than instantiations are fair
– cannot in general conclude satisfiability (changing…)
• Interactive verification systems (ACL2, Isabelle, Coq)
– very good at building inductive proofs
– could benefit greatly from counter-example
generation (as feedback to the user but also to
prune out branches in the search)
• Sinha’s Inertial Refinement technique
– similar use of “blocked paths”
– no guarantee to find counter-examples
Related Work, continued
• DSolve (aka. “Liquid Types”)
– because the proofs are based on type inference
rules, cannot immediately be used to prove
assertions relating different functions
• Bounded Model Checking
– offer similar guarantees on the discovery of
counter-examples
– reduces to SAT rather than SMT
– unclear when it is complete for proofs
• Finite Model Finding (Alloy, Paradox)
– lack of theory reasoning, no proofs
Satisfiability Modulo Recursive Programs
• Semi-decidable problem of great interest:
– applications in verification, testing, theorem
proving, constraint logic programming, …
• Our algorithm always finds counter-examples
when they exist, and will also find
assume/guarantee style proofs.
• It is a decision procedure for infinitely and
sufficiently surjective abstraction functions.
• We implemented it as a part of a verification
system for a purely functional subset of Scala.
Try it online http://lara.epfl.ch/leon/
Thank you.