Report

Model Checking Software, Solving Horn Clauses Part I Nikolaj Bjørner Microsoft Research VTSA, Luxembourg, October 30-31, 2014 Takeaways Symbolic Software Model Checking = SMT for Horn Clauses Simplification and pre-processing A Solver using clues from IC3 An Algorithmic Overview (separate slides) Horn Clauses mc(x) = x-10 mc(x) = mc(mc(x+11)) if x > 100 if x 100 assert (x ≤ →mc(x) = 91) ∀. > mc(, − ) ∀, , . ≤ mc( + , ) mc(, ) mc(, ) ∀, . mc(, ) ∧ ≤ → = Solver finds solution for mc [Hoder, B. SAT 2012] Transition System • • • • V init(V) step(V, V’) safe(V) - program variables - initial states - transition relation - safe states Safe Transition System ∃. • ∀V . init(V) → (V) • ∀V, V’ . V ∧ step(V, V’) → (V′) • ∀V . (V) →safe(V) – [Rybalchenko et.al. PLDI 2012, POPL 2014] Termination and reactivity are also handled in framework of solving systems of logical formulas. Recursive Procedures Formulate as Horn clauses: ∀. > mc(, − ) ∀, , . ≤ mc( + , ) mc(, ) mc(, ) ∀, . mc(, ) ∧ ≥ = Solve for mc Recursive Procedures Formulate as Predicate Transformer: F (mc)(,) = > 100 ∧ = − 10 ∨ ≤ 100 ∧ ∃. mc + 11, ∧ mc(, ) Check: μF mc , ∧ ≥ 101 → = 91 Recursive Procedures Instead of computing μF mc , , then checking μF mc , ∧ ≤ 101 → = 91 Suffices to find post-fixed point mc satisfying: ∀, . F mc , → mc , ∀, . mc , ∧ ≤ 101 → = 91 Program Verification as SMT - aka A Crusade for Hornish Satisfaction Program Verification (Safety) as Solving fixed-points as Satisfiability of Horn clauses [Bjørner, McMillan, Rybalchenko, SMT workshop 2012] Hilbert Sausage Factory: [Grebenshchikov, Lopes, Popeea, Rybalchenko, PLDI 2012] Procedures Horn Formulas Summary as commands Verifying procedure calls Modular Concurrency Horn Clauses − − , , ′ , ′ − , − , ′ − ′ ⇒ , , ∧ , , ′ , ′ ⇒ ′ , ′ , ∧ , ′ ⇒ , ′ , ∧ , , ′ , ′ ⇒ , ′ 1 1 ∧ ⋯ ∧ ⇒ ≠ [Predicate Abstraction and Refinement for Verifying Multi-Threaded Programs Gupta, Popeea, Rybalchenko, POPL 2011] Horn Clauses Γ ⊢ : ()} → : (, ) } ≺ : ′()} → : ′(, ) } Extract sufficient Horn Conditions Γ ∧ ′ ⇒ Γ ∧ ′ ∧ , ⇒ ′ , Generalized Horn Formulas Handling background axioms: ∀, . , ⇒ ∃ ∀ ∧ ∧ , , ⇒ Remark: Abductive Logic Programming amounts to symbolic simulation: - + ⊨ ∃ . () - + is consistent eg. solve for negation of above formula: ∃. ∧ (∀ . , → ∃ . (, , )) Simplifying Horn Clauses A model checking Example Abstraction as Boolean Program b := count == old_count [SLAM, BLAST, Graf & Saidi, Uribe, ..] (Predicate) Abstraction/Refinement • SMT solver used to synthesize (strongest) abstract transition relation F: , ′ ⇒ (1 … , , 1 ′ … , ′ ) Control as Horn Clauses (set-logic HORN) (declare-fun Loop (Int Int Bool) Bool) (declare-fun WhileTest (Int Int Bool) Bool) ; Loop is entered in arbitrary values of count, old_count (assert (forall ((count Int) (old_count Int)) (Loop count old_count false))) Loop ; Loop without if test (assert (forall ((count Int) (old_count Int) (lock_state Bool)) (=> (Loop count old_count lock_state) (WhileTest count count true)))) ; Loop with if-test (assert (forall ((count Int) (old_count Int) (lock_state Bool)) (=> (Loop count old_count lock_state) (WhileTest (+ 1 count ) count false)))) (assert (forall ((count Int) (old_count Int) (lock_state Bool)) (=> (and (not (= old_count count )) (WhileTest count old_count lock_state)) (Loop count old_count lock_state)))) While Test (assert (forall ((count Int) (old_count Int) (lock_state Bool)) (=> (and (= old_count count ) (WhileTest count old_count lock_state)) (= lock_state true)))) (assert (forall ((count Int) (old_count Int) (lock_state Bool)) (=> (Loop count old_count lock_state) (= lock_state false)))) (check-sat) (get-model) Solving Horn Clauses Pre-processing → ′ Search – Find model M such that ⊨ Or – Find refutation proof : ⊢ ⊥ Pre-processing • • • • • • Cone of Influence Simplification Subsumption Inlining Slicing Unfolding Cone of Influence – top down ∧ → P → T → ∧>→ ∧<→ = → Q ∧≤→ S is not used S ≔ Cone of Influence – bottom up ∧ , 0 → ∧>→ ∧<→ = → There is no “rule to produce Q(x,1)” , ≔ = 1 Q , ∧ ≤ → , Inlining (set-logic HORN) (declare-fun Loop (Int Int Bool) Bool) (declare-fun WhileTest (Int Int Bool) Bool) ; Loop is entered in arbitrary values of count, old_count (assert (forall ((count Int) (old_count Int)) (Loop count old_count false))) ; Loop without if test (assert (forall ((count Int) (old_count Int) (lock_state Bool)) (=> (Loop count old_count lock_state) (WhileTest count count true)))) (set-logic HORN) (declare-fun Loop (Int Int Bool) Bool) (declare-fun WhileTest (Int Int Bool) Bool) ; Loop is entered in arbitrary values of count, old_count (assert (forall ((count Int) (old_count Int)) (Loop count old_count false))) ; Loop without if test + repeat loop (assert (forall ((count Int) (old_count Int) (lock_state Bool)) (=> (and (Loop count old_count lock_state) (not (= count count))) (Loop count count true))) ; Loop without if test + loop exit (assert (forall ((count Int) (old_count Int) (lock_state Bool)) ; Loop with if-test (=> (and (Loop count old_count lock_state) (= count count)) (assert (forall ((count Int) (old_count Int) (lock_state Bool)) (= true true))) (=> (Loop count old_count lock_state) (WhileTest (+ 1 count ) count false)))) (assert (forall ((count Int) (old_count Int) (lock_state Bool)) (=> (and (not (= old_count count )) (WhileTest count old_count lock_state)) (Loop count old_count lock_state)))) (assert (forall ((count Int) (old_count Int) (lock_state Bool)) (=> (and (= old_count count ) (WhileTest count old_count lock_state)) (= lock_state true)))) (assert (forall ((count Int) (old_count Int) (lock_state Bool)) (=> (Loop count old_count lock_state) (= lock_state false)))) (check-sat) (get-model) ; Loop with if-test + repeat loop (assert (forall ((count Int) (old_count Int) (lock_state Bool)) (=> (and (Loop count old_count lock_state) (not (= (+ 1 count ) count )) (Loop (+ 1 count) count false))) ; Loop with if-test + loop exit (assert (forall ((count Int) (old_count Int) (lock_state Bool)) (=> (and (Loop count old_count lock_state) (= (+ 1 count ) count ) (= false true))) (assert (forall ((count Int) (old_count Int) (lock_state Bool)) (=> (Loop count old_count lock_state) (= lock_state false)))) (check-sat) (get-model) (set-logic HORN) (declare-fun Loop (Int Int Bool) Bool) (declare-fun WhileTest (Int Int Bool) Bool) Simplification ; Loop is entered in arbitrary values of count, old_count (assert (forall ((count Int) (old_count Int)) (Loop count old_count false))) ; Loop without if test + repeat loop (assert (forall ((count Int) (old_count Int) (lock_state Bool)) (=> (and (Loop count old_count lock_state) (not (= count count))) (Loop count count true))) ; Loop without if test + loop exit (assert (forall ((count Int) (old_count Int) (lock_state Bool)) (=> (and (Loop count old_count lock_state) (= count count)) (= truetrue))) (set-logic HORN) (declare-fun Loop (Int Int Bool) Bool) (declare-fun WhileTest (Int Int Bool) Bool) ; Loop is entered in arbitrary values of count, old_count (assert (forall ((count Int) (old_count Int)) (Loop count old_count false))) ; Loop without if test + repeat loop ; Loop without if test + loop exit (assert (forall ((count Int) (old_count Int) (lock_state Bool)) (=> (Loop count old_count lock_state) (= true true))) ; Loop with if-test + repeat loop (assert (forall ((count Int) (old_count Int) (lock_state Bool)) (=> (and (Loop count old_count lock_state) (not (= (+ 1 count ) count )) ; Loop with if-test + repeat loop (Loop (+ 1 count) count false))) (assert (forall ((count Int) (old_count Int) (lock_state Bool)) (=> (Loop count old_count lock_state) ; Loop with if-test + loop exit (Loop (+ 1 count) count false))) (assert (forall ((count Int) (old_count Int) (lock_state Bool)) (=> (and (Loop count old_count lock_state) (= (+ 1 count ) count ) (= false true))) ; Loop with if-test + loop exit (assert (forall ((count Int) (old_count Int) (lock_state Bool)) (=> (Loop count old_count lock_state) (= lock_state false)))) (assert (forall ((count Int) (old_count Int) (lock_state Bool)) (=> (Loop count old_count lock_state) (= lock_state false)))) (check-sat) (get-model) (check-sat) (get-model) (set-logic HORN) (declare-fun Loop (Int Int Bool) Bool) (declare-fun WhileTest (Int Int Bool) Bool) Simplification ; Loop is entered in arbitrary values of count, old_count (assert (forall ((count Int) (old_count Int)) (Loop count old_count false))) ; Loop without if test + repeat loop (assert (forall ((count Int) (old_count Int) (lock_state Bool)) (=> (and (Loop count old_count lock_state) (not (= count count))) (Loop count count true))) ; Loop without if test + loop exit (assert (forall ((count Int) (old_count Int) (lock_state Bool)) (=> (and (Loop count old_count lock_state) (= count count)) (= truetrue))) (set-logic HORN) (declare-fun Loop (Int Int Bool) Bool) (declare-fun WhileTest (Int Int Bool) Bool) ; Loop is entered in arbitrary values of count, old_count (assert (forall ((count Int) (old_count Int)) (Loop count old_count false))) ; Loop without if test + repeat loop ; Loop without if test + loop exit ; Loop with if-test + repeat loop (assert (forall ((count Int) (old_count Int) (lock_state Bool)) (=> (and (Loop count old_count lock_state) (not (= (+ 1 count ) count )) ; Loop with if-test + repeat loop (Loop (+ 1 count) count false))) (assert (forall ((count Int) (old_count Int) (lock_state Bool)) (=> (Loop count old_count lock_state) ; Loop with if-test + loop exit (Loop (+ 1 count) count false))) (assert (forall ((count Int) (old_count Int) (lock_state Bool)) (=> (and (Loop count old_count lock_state) (= (+ 1 count ) count ) (= false true))) ; Loop with if-test + loop exit (assert (forall ((count Int) (old_count Int) (lock_state Bool)) (=> (Loop count old_count lock_state) (= lock_state false)))) (assert (forall ((count Int) (old_count Int) (lock_state Bool)) (=> (Loop count old_count true) false))) (check-sat) (get-model) (check-sat) (get-model) Cone of Influence (set-logic HORN) (declare-fun Loop (Int Int Bool) Bool) (declare-fun WhileTest (Int Int Bool) Bool) ; Loop is entered in arbitrary values of count, old_count (assert (forall ((count Int) (old_count Int)) (Loop count old_count false))) ; Loop without if test + repeat loop (assert (forall ((count Int) (old_count Int) (lock_state Bool)) (=> (and (Loop count old_count lock_state) (not (= count count))) (Loop count count true))) ; Loop without if test + loop exit (assert (forall ((count Int) (old_count Int) (lock_state Bool)) (=> (and (Loop count old_count lock_state) (= count count)) (= truetrue))) (set-logic HORN) (declare-fun Loop (Int Int Bool) Bool) (declare-fun WhileTest (Int Int Bool) Bool) ; Loop is entered in arbitrary values of count, old_count (assert (forall ((count Int) (old_count Int)) (Loop count old_count false))) ; Loop without if test + repeat loop ; Loop without if test + loop exit ; Loop with if-test + repeat loop (assert (forall ((count Int) (old_count Int) (lock_state Bool)) (=> (and (Loop count old_count lock_state) (not (= (+ 1 count ) count )) ; Loop with if-test + repeat loop (Loop (+ 1 count) count false))) (assert (forall ((count Int) (old_count Int) (lock_state Bool)) (=> (Loop count old_count lock_state) ; Loop with if-test + loop exit (Loop (+ 1 count) count false))) (assert (forall ((count Int) (old_count Int) (lock_state Bool)) (=> (and (Loop count old_count lock_state) (= (+ 1 count ) count ) (= false true))) ; Loop with if-test + loop exit (assert (forall ((count Int) (old_count Int) (lock_state Bool)) (=> (Loop count old_count lock_state) (= lock_state false)))) (assert (forall ((count Int) (old_count Int) (lock_state Bool)) (=> (Loop count old_count true) false))) (check-sat) (get-model) (check-sat) (get-model) (set-logic HORN) (declare-fun Loop (Int Int Bool) Bool) (declare-fun WhileTest (Int Int Bool) Bool) Result ; Loop is entered in arbitrary values of count, old_count (assert (forall ((count Int) (old_count Int)) (Loop count old_count false))) ; Loop without if test + repeat loop (assert (forall ((count Int) (old_count Int) (lock_state Bool)) (=> (and (Loop count old_count lock_state) (not (= count count))) (Loop count count true))) ; Loop without if test + loop exit (assert (forall ((count Int) (old_count Int) (lock_state Bool)) (=> (and (Loop count old_count lock_state) (= count count)) (= truetrue))) (set-logic HORN) (declare-fun Loop (Int Int Bool) Bool) (declare-fun WhileTest (Int Int Bool) Bool) ; Loop is entered in arbitrary values of count, old_count ; Loop without if test + repeat loop ; Loop without if test + loop exit ; Loop with if-test + repeat loop (assert (forall ((count Int) (old_count Int) (lock_state Bool)) (=> (and (Loop count old_count lock_state) (not (= (+ 1 count ) count )) ; Loop with if-test + repeat loop (Loop (+ 1 count) count false))) ; Loop with if-test + loop exit (assert (forall ((count Int) (old_count Int) (lock_state Bool)) (=> (and (Loop count old_count lock_state) (= (+ 1 count ) count ) (= false true))) (assert (forall ((count Int) (old_count Int) (lock_state Bool)) (=> (Loop count old_count lock_state) (= lock_state false)))) (check-sat) (get-model) ; Loop with if-test + loop exit (check-sat) (get-model) Slicing • Remove variables that have no effect Unfolding • = more aggressive in-lining • Also applied to predicates that are not eliminated A Horn Clause Solver Algorithm Objective is to solve for R such that F → , → , ∀ Key elements of PDR algorithm: Over-approximate reachable states ≔ F , → → ⋯ → ≔ Propagate back from ¬ Resolve conflicts Strengthen/propagate using induction Algorithm Objective is to solve for R such that F → , Initialize: → , ∀ ↖ ↗ ≔ ≔ F F Main invariant: ↖ ↖ ↗ + ↖ F Algorithm Main invariant: F → + → → + Search: Mile-high perspective Modern SMT solver Decisions: Conflict Conflict Clauses Assignments Resolution Fixedpoint solver → WP → Conflict ← SP ← Resolution Conflict resolution with arithmetic R(0,0,0,0). Initial states T(L,M,Y1,Y2,L’,M’,Y1’,Y2’)R(L,M,Y1,Y2) R(L’,M’,Y1’,Y2’) Reachable states R(2,2,Y1,Y2) false Is unsafe state reachable? Step(L,L’,Y1,Y2,Y1’) T(L,M,Y1,Y2,L’,M,Y1’,Y2) Step(M,M’,Y2,Y1,Y2’) T(L,M,Y1,Y2,L,M’,Y1,Y2’) Step(0,1,Y1,Y2,Y2+1). (Y1 ≤ Y2 ∨ Y2 = 0) Step(1,2,Y1,Y2,Y1). Step(2,3,Y1,Y2,Y1). Step(3,0,Y1,Y2,0). P1 takes a step P2 takes a step ℓ : ≔ + ; ℓ ℓ : = ∨ ≤ ; ℓ ℓ : ; ℓ ℓ : ≔ ; ℓ Search: Mile-high perspective F () F 2 () B2 ¬ B ¬ ¬ Conflict Propagation Conflict Propagation Conflict Resolution Interpolating Conflicts = = = = = = = = = = = = = = = = Conflict Resolution ≥ + ∧ ≥ Conflict ∧ ≤ 0 ≥ ∧ ≤ 0∧ Resolution Get Generalization from Farkas Lemma Eg., resolve away blue internal variables Interpolating Conflicts = = = == = → ≥ = → ≥ = = Conflict Resolution Conflict Propagation Conflict Propagation = = = = = == →=≥ = = Generalization from T-lemmas Can we satisfy? (, , , ). Initial states , , , , ’, ’, ’, ’ , , , , ’, ’, ’, ’ Reachable states , , , ¬ = ∧ = . Unsafe state is unreachable = ∧ = ∧ = ∧ F M E.g., there is unsat core of: is unsatisfiable ≤ ≤ ∧ F M Unsat proof uses T-lemmas > ∨ < ∨ − > ∨ − > ¬ ¬M Generalization from T-lemmas Can we satisfy? (, , , ). Initial states , , , , ’, ’, ’, ’ , , , , ’, ’, ’, ’ Reachable states , , , ¬ = ∧ = . Unsafe state is unreachable Unsat proof uses T-lemmas > ∨ < ∨ − > ∨ − > ¬ ¬M ⋅ − ≤ − ≤ ⋅ ( − ≤ ) − ≤ − ≤ − ≤ − ≤ − ≤ −−−−− − ≤ − − ≤