Introduction to Satisfiability Modulo Theories(SMT).ppt

《Introduction to Satisfiability Modulo Theories(SMT).ppt》由会员分享，可在线阅读，更多相关《Introduction to Satisfiability Modulo Theories(SMT).ppt（65页珍藏版）》请在麦多课文档分享上搜索。

1、Introduction to Satisfiability Modulo Theories (SMT),Clark Barrett, NYU Sanjit A. Seshia, UC Berkeley,ICCAD TutorialNovember 2, 2009,C. Barrett & S. A. Seshia,ICCAD 2009 Tutorial,2,Boolean Satisfiability (SAT),:,. . .,p2,p1,pn,Is there an assignment to the p1, p2, , pn variables such that evaluates

2、to 1?,C. Barrett & S. A. Seshia,ICCAD 2009 Tutorial,3,Satisfiability Modulo Theories,:,. . .,p2,p1,pn,Is there an assignment to the x,y,z,w variables s.t. evaluates to 1?,x + 2 z 1,x % 26 = v,w & 0xFFFF = x,x = y,C. Barrett & S. A. Seshia,ICCAD 2009 Tutorial,4,Satisfiability Modulo Theories,Given a

3、formula in first-order logic, with associated background theories, is the formula satisfiable? Yes: return a satisfying solution No generate a proof of unsatisfiability,C. Barrett & S. A. Seshia,ICCAD 2009 Tutorial,5,Applications of SMT,Hardware verification at higher levels of abstraction (RTL and

4、above) Verification of analog/mixed-signal circuits Verification of hybrid systems Software model checking Software testing Security: Finding vulnerabilities, verifying electronic voting machines, Program synthesis ,C. Barrett & S. A. Seshia,ICCAD 2009 Tutorial,6,References,Satisfiability Modulo The

5、ories Clark Barrett, Roberto Sebastiani, Sanjit A. Seshia, and Cesare Tinelli. Chapter 8 in the Handbook of Satisfiability, Armin Biere, Hans van Maaren, and Toby Walsh, editors, IOS Press, 2009. (available from our webpages)SMTLIB: A repository for SMT formulas (common format) and tools SMTCOMP: An

6、 annual competition of SMT solvers,C. Barrett & S. A. Seshia,ICCAD 2009 Tutorial,7,Roadmap for this Tutorial,Background and Notation Survey of Theories Theory Solvers Approaches to SMT Solving Lazy Encoding to SAT Eager Encoding to SAT Conclusion,C. Barrett & S. A. Seshia,ICCAD 2009 Tutorial,8,Roadm

7、ap for this Tutorial,Background and Notation Survey of Theories Theory Solvers Approaches to SMT Solving Lazy Encoding to SAT Eager Encoding to SAT Conclusion,C. Barrett & S. A. Seshia,ICCAD 2009 Tutorial,9,First-Order Logic,A formal notation for mathematics, with expressions involving Propositional

8、 symbols Predicates Functions and constant symbols Quantifiers In contrast, propositional (Boolean) logic only involves propositional symbols and operators,C. Barrett & S. A. Seshia,ICCAD 2009 Tutorial,10,First-Order Logic: Syntax,As with propositional logic, expressions in first-order logic are mad

9、e up of sequences of symbols. Symbols are divided into logical symbols and non-logical symbols or parameters. Example:(x = y) (y = z) (f(z) f(x)+1),C. Barrett & S. A. Seshia,ICCAD 2009 Tutorial,11,First-Order Logic: Syntax,Logical Symbols Propositional connectives: , , :, !, $ Variables: v1, v2, . .

10、 . Quantifiers: 8, 9 Non-logical symbols/Parameters Equality: = Functions: +, -, %, bit-wise &, f(), concat, Predicates: , is_substring, Constant symbols: 0, 1.0, null, ,C. Barrett & S. A. Seshia,ICCAD 2009 Tutorial,12,Quantifier-free Subset,We will largely restrict ourselves to formulas without qua

11、ntifiers (8, 9) This is called the quantifier-free subset/fragment of first-order logic with the relevant theory,C. Barrett & S. A. Seshia,ICCAD 2009 Tutorial,13,Logical Theory,Defines a set of parameters (non-logical symbols) and their meanings This definition is called a signature. Example of a si

12、gnature:Theory of linear arithmetic over integersSignature is (0,1,+,-,) interpreted over Z,C. Barrett & S. A. Seshia,ICCAD 2009 Tutorial,14,Roadmap for this Tutorial,Background and Notation Survey of Theories Theory Solvers Two Approaches to SMT Solving Lazy Encoding to SAT Eager Encoding to SAT Co

13、nclusion,C. Barrett & S. A. Seshia,ICCAD 2009 Tutorial,15,Some Useful Theories,Equality (with uninterpreted functions) Linear arithmetic (over Q or Z) Difference logic (over Q or Z) Finite-precision bit-vectors integer or floating-point Arrays / memories Misc.: Non-linear arithmetic, strings, induct

14、ive datatypes (e.g. lists), sets, ,C. Barrett & S. A. Seshia,ICCAD 2009 Tutorial,16,Theory of Equality and Uninterpreted Functions (EUF),Also called the “free theory” Because function symbols can take any meaning Only property required is congruence: that these symbols map identical arguments to ide

15、ntical values i.e., x = y ) f(x) = f(y) SMTLIB name: QF_UF,C. Barrett & S. A. Seshia,ICCAD 2009 Tutorial,17,Data and Function Abstraction with EUF,Common Operations,10,x,y,p,ITE(p, x, y),If-then-else,x,y,x = y,=,Test for equality,C. Barrett & S. A. Seshia,ICCAD 2009 Tutorial,18,Hardware Abstraction

16、with EUF,For any Block that Transforms or Evaluates Data: Replace with generic, unspecified function Also view instruction memory as function,F2,F1,F3,C. Barrett & S. A. Seshia,ICCAD 2009 Tutorial,19,Example QF_UF (EUF) Formula,(x = y) (y = z) (f(x) f(z)Transitivity: (x = y) (y = z) ) (x = z)Congrue

17、nce:(x = z) ) (f(x) = f(z),C. Barrett & S. A. Seshia,ICCAD 2009 Tutorial,20,Equivalence Checking of Program Fragments,int fun1(int y) int x, z;z = y;y = x;x = z;return x*x; ,int fun2(int y) return y*y; ,What if we use SAT to check equivalence?,SMT formula Satisfiable iff programs non-equivalent( z =

18、 y y1 = x x1 = z ret1 = x1*x1) ( ret2 = y*y ) ( ret1 ret2 ),C. Barrett & S. A. Seshia,ICCAD 2009 Tutorial,21,Equivalence Checking of Program Fragments,int fun1(int y) int x, z;z = y;y = x;x = z;return x*x; ,int fun2(int y) return y*y; ,SMT formula Satisfiable iff programs non-equivalent( z = y y1 =

19、x x1 = z ret1 = x1*x1) ( ret2 = y*y ) ( ret1 ret2 ),Using SAT to check equivalence (w/ Minisat)32 bits for y: Did not finish in over 5 hours16 bits for y: 37 sec.8 bits for y: 0.5 sec.,C. Barrett & S. A. Seshia,ICCAD 2009 Tutorial,22,Equivalence Checking of Program Fragments,int fun1(int y) int x, z

20、;z = y;y = x;x = z;return x*x; ,int fun2(int y) return y*y; ,SMT formula ( z = y y1 = x x1 = z ret1 = sq(x1) ) ( ret2 = sq(y) ) ( ret1 ret2 ),Using EUF solver: 0.01 sec,C. Barrett & S. A. Seshia,ICCAD 2009 Tutorial,23,Equivalence Checking of Program Fragments,int fun1(int y) int x;x = x y;y = x y;x

21、= x y;return x*x; ,int fun2(int y) return y*y; ,Does EUF still work?,No! Must reason about bit-wise XOR.Need a solver for bit-vector arithmetic.Solvable in less than a sec. with a current bit-vector solver.,C. Barrett & S. A. Seshia,ICCAD 2009 Tutorial,24,Finite-Precision Bit-Vector Arithmetic (QF_B

22、V),Fixed width data words Can model int, short, long, etc. Arithmetic operations E.g., add/subtract/multiply/divide & comparisons Twos complement and unsigned operations Bit-wise logical operations E.g., and/or/xor, shift/extract and equality Boolean connectives,C. Barrett & S. A. Seshia,ICCAD 2009

23、Tutorial,25,Linear Arithmetic (QF_LRA, QF_LIA),Boolean combination of linear constraints of the form(a1 x1 + a2 x2 + + an xn b) xis could be in Q or Z , 2 ,=Many applications, including: Verification of analog circuits Software verification, e.g., of array bounds,C. Barrett & S. A. Seshia,ICCAD 2009

24、 Tutorial,26,Difference Logic (QF_IDL, QF_RDL),Boolean combination of linear constraints of the formxi - xj cij or xi ci 2 ,=, xis in Q or Z Applications: Software verification (most linear constraints are of this form) Processor datapath verification Job shop scheduling / real-time systems Timing v

25、erification for circuits,C. Barrett & S. A. Seshia,ICCAD 2009 Tutorial,27,Arrays/Memories,SMT solvers can also be very effective in modeling data structures in software and hardware Arrays in programs Memories in hardware designs: e.g. instruction and data memories, CAMs, etc.,C. Barrett & S. A. Ses

26、hia,ICCAD 2009 Tutorial,28,Theory of Arrays (QF_AX) Select and Store,Two interpreted functions: select and store select(A,i) Read from A at index i store(A,i,d) Write d to A at index i Two main axioms: select(store(A,i,d), i) = d select(store(A,i,d), j) = select(A,j) for i j One other axiom: (8 i. s

27、elect(A,i) = select(B,i) ) A = B,C. Barrett & S. A. Seshia,ICCAD 2009 Tutorial,29,Equivalence Checking of Program Fragments,int fun1(int y) int x2;x0 = y;y = x1;x1 = x0;return x1*x1; ,int fun2(int y) return y*y; ,SMT formula x1 = store(x,0,y) y1 = select(x1,1) x2 = store(x1,1,select(x1,0) ret1 = sq(

28、select(x2,1) ( ret2 = sq(y) ) ( ret1 ret2 ),C. Barrett & S. A. Seshia,ICCAD 2009 Tutorial,30,Roadmap for this Tutorial,Background and Notation Survey of Theories Theory Solvers Two Approaches to SMT Solving Lazy Encoding to SAT Eager Encoding to SAT Conclusion,C. Barrett & S. A. Seshia,ICCAD 2009 Tu

29、torial,31,Over to Clark,C. Barrett & S. A. Seshia,ICCAD 2009 Tutorial,32,Roadmap for this Tutorial,Background and Notation Survey of Theories Theory Solvers Approaches to SMT Solving Lazy Encoding to SAT Eager Encoding to SAT Conclusion,C. Barrett & S. A. Seshia,ICCAD 2009 Tutorial,33,Eager Approach

30、 to SMT,Key Ideas: Small-domain encoding Constrain model search Rewrite rules Abstraction-based methods (eager + lazy)Example Solvers: UCLID, STP, Spear, Boolector, Beaver, ,SAT Solver involved in Theory Reasoning,C. Barrett & S. A. Seshia,ICCAD 2009 Tutorial,34,Theories,Eager Encoding Methods have

31、been demonstrated for the following Theories: Equality & Uninterpreted Functions Integer Linear Arithmetic Restricted Lambda expressions Arrays, memories, etc. Finite-precision Bit-Vector Arithmetic Strings,C. Barrett & S. A. Seshia,ICCAD 2009 Tutorial,35,UCLID Operation,Operation Series of transfor

32、mations leading to Boolean formula Each step is validity (satisfiability) preserving Each step performs optimizations,Lambda Expansion for Arrays,Encoding Arithmetic,Boolean Satisfiability,Input Formula,-free Formula,Linear/ Bitvector ArithmeticFormula,Boolean Formula,Function & Predicate Eliminatio

33、n,http:/uclid.eecs.berkeley.edu,C. Barrett & S. A. Seshia,ICCAD 2009 Tutorial,36,Rewrites: Eliminating Function Applications,Two applications of an uninterpreted function f in a formula f(x1) and f(x2),C. Barrett & S. A. Seshia,ICCAD 2009 Tutorial,37,Small-Domain Encoding,Consider an SMT formula (x1

34、, x2, , xn) where xi 2 Di Small-domain encoding/Finite instantiation: Derive finite set Si Di s.t. |Si| |Di| In some cases, Si is finite where Di is infinite Encode each xi to take values only in Si Could be done by encoding to SAT Example: Integer Linear Arithmetic (QF_LIA),C. Barrett & S. A. Seshi

35、a,ICCAD 2009 Tutorial,38,Solving QF_LIA is NP-complete,In NP: If a satisfying solution exists, then one exists within a bound d log d is polynomial in input size Expression for d Papadimitriou, 82(n+m) (bmax +1) ( m amax ) 2m+3 Input size: m # constraints n # variables bmax largest constant (absolut

36、e value) amax largest coefficient (absolute value),C. Barrett & S. A. Seshia,ICCAD 2009 Tutorial,39,Small-domain encoding / Finite Instantiation: Nave approach,Steps Calculate the solution bound d Encode each integer variable with d log d e bits & translate to Boolean formula Run SAT solver Problem:

37、 For QF_LIA, d is W( m m ) W( m log m ) bits per variable Solution: Exploit special-cases and domain-specific structure,C. Barrett & S. A. Seshia,ICCAD 2009 Tutorial,40,Special Case 1: Equality Logic,Linear constraints are equalities xi = xj Result: d = n,x1 x2 x2 x3 x1 x33-valued domain is needed:

38、1, 2, 3,C. Barrett & S. A. Seshia,ICCAD 2009 Tutorial,41,Special Case 2: Difference Logic,Boolean combination of difference-bound constraintsxi xj + b, xi b Result: d = n (bmax + 1) Bryant, Lahiri, Seshia, CAV02 Proof sketch: satisfying solution corresponds to shortest path in constraint graph Longe

39、st such path has length n (bmax + 1) Tighter formula-specific bounds possible,C. Barrett & S. A. Seshia,ICCAD 2009 Tutorial,42,Special Case 3: Generalized 2SAT,Generalized 2SAT constraintsxi + xj b, - xi - xj b, xi - xj b, xi bd = 2 n (bmax + 1) Seshia, Subramani, Bryant,04,C. Barrett & S. A. Seshia

40、,ICCAD 2009 Tutorial,43,Full Integer Linear Arithmetic,Can we avoid the mm blow-up? In fact, yes. The idea is to derive a new parameterized solution bound d Formalize parameters that the bound really depends on Parameters characterize sparse structure Occurs especially in software verification; also

41、 in many high-level hardware models Seshia & Bryant, LICS04, LMCS05,C. Barrett & S. A. Seshia,ICCAD 2009 Tutorial,44,Structure of Linear Constraints in Software Verification,Characteristics of studied benchmarks Mostly difference constraints Only 3% of constraints were NOT difference constraints Non

42、-difference constraints are sparse At most 6 variables per constraint (total number of variables in 1000s) Some similar observations: Pratt77, ESC/Java-Simplify-TR03,C. Barrett & S. A. Seshia,ICCAD 2009 Tutorial,45,Parameterized Solution Bound,New parameters: k non-difference constraints, w variable

43、s per constraint (width),C. Barrett & S. A. Seshia,ICCAD 2009 Tutorial,46,Example,C. Barrett & S. A. Seshia,ICCAD 2009 Tutorial,47,Summary of d Values,C. Barrett & S. A. Seshia,ICCAD 2009 Tutorial,48,Abstraction-Based Methods,For some logics, one cannot easily compute a closed-form expression for th

44、e small domain Example: Bit-Vector Arithmetic In such cases, an abstraction-refinement approach can be used to compute formula-specific small domains,C. Barrett & S. A. Seshia,ICCAD 2009 Tutorial,49,Bit-Vector Arithmetic: Some History,B.C. (Before Chaff) String operations (concatenate, field extract

45、ion) Linear arithmetic with bounds checking Modular arithmetic SAT-Based “Bit Blasting” Generate Boolean circuit based on bit-level behavior of operations Handles arbitrary operations Check with best available SAT solver Effective in many applications CBMC Clarke, Kroening, Lerda, TACAS 04 Microsoft

46、 Cogent + SLAM Cook, Kroening, Sharygina, CAV 05,C. Barrett & S. A. Seshia,ICCAD 2009 Tutorial,50,Research Challenge,Is there a better way than bit blasting? Requirements Provide same functionality as with bit blasting Must support all bit-vector operators Exploit word-level structure Improve on per

47、formance of bit blasting Current Approaches based on two core ideas: Simplification: Simplify input formula using word-level rewrite rules and solvers Abstraction: Can use automatic abstraction-refinement to solve simplified formula,C. Barrett & S. A. Seshia,ICCAD 2009 Tutorial,51,Bit-Vector SMT Sol

48、vers, circa Spr.2009,Current Techniques with Sample Tools Proof-based abstraction-refinement UCLID Bryant et al., TACAS 07 Solver for linear modular arithmetic to simplify the formula STP Ganesh & Dill, CAV07 Automatic parameter tuning for SAT Spear Hutter et al., FMCAD 07 Rewrites, underapproximati

49、on, efficient SAT engine Boolector Brummayer & Biere, TACAS09 Equality/constant propagation, logic optimization, special rules for non-linear ops - Beaver Jha et al., CAV09 DPLL(T) framework: Layered approach, rewriting CVC3 Barrett et al., MathSAT Bruttomesso et al, Yices Dutertre et al., Z3 de Moura et al,