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,
