advertisement

Predicate Abstraction of ANSI-C Programs Using SAT By Edmund Clarke, Daniel Kroening, Natalia Sharygina, Karen Yorav Presented by Yunho Kim Provable Software Lab, KAIST Contents • Introduction • Preparation of C code • Abstraction using SAT • Model checking • Conclusion Predicate Abstraction of ANSI-C Programs Using SAT, Yunho Kim, Provable Software Lab, KAIST 2/23 Introduction(1/3) • A simple C code has too many states for exhaustive analysis Example(unsigned int x) L1: while(x>1) { L2: if (x%2 == 1) L3: x = 3*x+1; else L4: x = x/2; } L5: assert(x != 0); Final L5 Program L4 Counter L3 … L2 L1 Initial 0 1 2 … Value of x • However, what we really need is ‘x is 0 or not’, not the concrete value of x Predicate Abstraction of ANSI-C Programs Using SAT, Yunho Kim, Provable Software Lab, KAIST 3/23 Introduction(2/3) • Predicate is a function which returns a Boolean value – A function π: X→ {true, false} is a predicate on X • States satisfying same predicates are equivalent π=true L5 Program Counter L3 π = true L4 … L2 L1 0 1 2 Value of x … Predicate Abstraction π = false π = false π ⇔ (x = 0) Predicate Abstraction of ANSI-C Programs Using SAT, Yunho Kim, Provable Software Lab, KAIST 4/23 Introduction(3/3) • Overview of predicate abstraction process C program Spec φ Predicate Abstraction Predicate Refinement Boolean Program φ Model Checking Spurious? Spurious Counterexample φ true φ false + counterexample Today’s focus: How to make a Boolean program effectively and efficiently from a given C program and a set of predicates Predicate Abstraction of ANSI-C Programs Using SAT, Yunho Kim, Provable Software Lab, KAIST 5/23 Contents • Introduction • Preparation of C code • Abstraction using SAT • Model checking • Conclusion Predicate Abstraction of ANSI-C Programs Using SAT, Yunho Kim, Provable Software Lab, KAIST 6/23 Preparation of C code(1/3) Concrete state Concrete transition (basic block) Abstraction function (predicates) Abstract state Concrete next state Abstraction function (predicates) Abstract transition Abstract next state Predicate Abstraction of ANSI-C Programs Using SAT, Yunho Kim, Provable Software Lab, KAIST 7/23 Preparation of C code(2/3) • Transform C program into goto-program – Function inlining • Recursion is not supported – Loop is rewritten using if and goto statements – Side-effects are removed • x = 5+(++i); i = i+1; x = 5+i; Predicate Abstraction of ANSI-C Programs Using SAT, Yunho Kim, Provable Software Lab, KAIST 8/23 Preparation of C code(3/3) • goto-program example C program 1. int global; 2. int func(){ 3. global = 1; 4. } 5. 6. int main(){ 7. int x, i; 8. func(); 9. if ((x = 5+(++i))){ 10. global = 2; 11. } 12. else{ 13. global = 3; 14. } 15. } goto-program 1. int global; 2. int x, i; 3. global = 1; 4. i = i+1; 5. x = 5+i; 6. if (!x) goto L1; 7. global = 2; 8. goto L2; 9. L1: global = 3; 10. L2: Predicate Abstraction of ANSI-C Programs Using SAT, Yunho Kim, Provable Software Lab, KAIST 9/23 Contents • Introduction • Preparation of C code • Abstraction using SAT • Model checking • Conclusion Predicate Abstraction of ANSI-C Programs Using SAT, Yunho Kim, Provable Software Lab, KAIST 10/23 Abstraction using SAT(1/9) • Definition – v is the vector of all concrete program variables v • v is a state of a concrete program • Program counter is considered as a variable – b denotes the vector of all Boolean variables b • b is a state of a Boolean program • Each predicate πi is associated with a Boolean variable bi – π denotes the vector of predicates πi • π(v) is called the abstraction function, π(v) = b Predicate Abstraction of ANSI-C Programs Using SAT, Yunho Kim, Provable Software Lab, KAIST 11/23 Abstraction using SAT(2/9) • Definition (con’t) – T is a concrete transition relation which maps a concrete state v into a concrete next state v’ – B is an abstract transition relation which maps an abstract state b into an abstract next state b’ Predicate Abstraction of ANSI-C Programs Using SAT, Yunho Kim, Provable Software Lab, KAIST 12/23 Abstraction using SAT(3/9) Concrete transition (basic block) Concrete state Concrete next state PC=L4, x = 3 PC’=L1, x’ = 1 Abstraction function (predicates) π ⇔ (x = 0) Abstraction function (predicates) b = false π ⇔ (x = 0) b = false Example(unsigned int x) Abstract L1: while(x>1) { state L2: if (x%2 == 1) L3: L4: else Abstract transition Abstract next state x = 3*x+1; x = x/2; } L5: assert(x != 0); Predicate Abstraction of ANSI-C Programs Using SAT, Yunho Kim, Provable Software Lab, KAIST 13/23 Abstraction using SAT(4/9) • First defines the concrete transition relation of a basic block • Each basic block consists of a sequence of assignments – Therefore do not consider control statements here • T denotes the CNF formula representing the concrete transition relation Predicate Abstraction of ANSI-C Programs Using SAT, Yunho Kim, Provable Software Lab, KAIST 14/23 Abstraction using SAT(5/9) • Translates a basic block into its Static Single Assignment(SSA) form Basic block x = z * x; y = x + 1; x = x + y; SSA form v[x:=x0, y:=y0, z:=z0] x1 = z0 * x0; CNF y1 = x1 + 1; formula x2 = x1 + y1; v’[x’:=x2, y’:=y1, z’:=z0] T(v, v’) • Each v’ in v’ is the largest numbered SSA variable Predicate Abstraction of ANSI-C Programs Using SAT, Yunho Kim, Provable Software Lab, KAIST 15/23 Abstraction using SAT(6/9) • Assignments and arithmetic operations are translated into CNF formula • Assume that x,y,z are three bits positive integers represented by propositions x0x1x2, y0y1y2, z0z1z2 • C z=x+y (z0(x0⊕y0)⊕( (x1∧y1) ∨ ((x1⊕y1)∧(x2∧y2))) ∧ (z1(x1⊕y1)⊕(x2∧y2)) ∧ (z2(x2⊕y2)) Predicate Abstraction of ANSI-C Programs Using SAT, Yunho Kim, Provable Software Lab, KAIST 16/23 Abstraction using SAT(7/9) • The abstract transition relation B(b, b’) is defined using π as follows: • Predicate Abstraction of ANSI-C Programs Using SAT, Yunho Kim, Provable Software Lab, KAIST 17/23 Abstraction using SAT(8/9) • Example SAT formula Basic block SSA form d = e; e = e+1; v[d:=d0, e:=e0] d1 = e0 e1 = e0+1 v’[d’:=d1, e’:=e1] All satisfying assignments obtained using SAT solver (b1(e0≥0))∧(b2(e0≤100))∧ d1=e0 ∧ e1=e0+1 ∧ (b1’=(e1≥0))∧(b2’=(e1≤100)) b1 b2 b1’ b2’ 0 1 0 1 0 1 1 1 1 0 0 1 1 0 1 0 1 1 1 0 1 1 1 1 Predicates: π1 = e ≥ 0 π2 = e ≤ 100 Predicate Abstraction of ANSI-C Programs Using SAT, Yunho Kim, Provable Software Lab, KAIST 18/23 Abstraction using SAT(9/9) • The condition in if statement can be a predicate SAT formula Control statement x = 0; if (x<2) x = x+1; b1x0<2 ∧ x1=0 ∧ b1’ x1<2 ∧ b1’x1<2 ∧ x2=x1+1 ∧ b1’’ x2<2 ∨ Predicate: π1 = x < 0 ┐(b1’x1<2)∧ x2=x1∧ b1’’=b1’ Predicate Abstraction of ANSI-C Programs Using SAT, Yunho Kim, Provable Software Lab, KAIST 19/23 Contents • Introduction • Preparation of C code • Abstraction using SAT • Model checking • Conclusion Predicate Abstraction of ANSI-C Programs Using SAT, Yunho Kim, Provable Software Lab, KAIST 20/23 Model checking(1/1) • Model checker tries to find a counterexample of the generated Boolean program model. • If no counterexample is found, the concrete program satisfies given requirements. • If a counterexample is found, check its feasibility – If the counterexample is infeasible, refine predicates and rerun predicate abstraction process Predicate Abstraction of ANSI-C Programs Using SAT, Yunho Kim, Provable Software Lab, KAIST 21/23 Conclusion(1/1) • Predicate abstraction using SAT performs better than theorem provers • It can use sound abstraction with the power of SAT solver Predicate Abstraction of ANSI-C Programs Using SAT, Yunho Kim, Provable Software Lab, KAIST 22/23 References(1/1) • Predicate abstraction of ANSI-C Programs Using SAT by Edmund Clarke, Daniel Kroening, Natasha Sharygina and Karen Yorav in Formal Methods in System Design, Vol. 25, pp. 105-127, 2004 Predicate Abstraction of ANSI-C Programs Using SAT, Yunho Kim, Provable Software Lab, KAIST 23/23