Efficient Decision Procedure for Bounded Integer Non-linear Operations using SMT(LIA) Oct 28, 2008 Malay Ganai System Analysis & Verification Group NEC Labs America Princeton, U. S. A. Outline Motivation Existing Approaches Our Approach Experiments Conclusions 2 Motivation Theory of non-linear operations: un-decidable, in general – imprecise formulation and/or incomplete reasoning adopted Non-linear integer operations on program variables occur sparingly in application programs – multiplication, divide, left and right shifts, mod, bitwise Overflow and Underflow are not used as a programming feature typically – signed over/under flow not defined (C99/C++98 standard) – programmers avoid them due to portability reasons • more interested in detection: knowing if overflow/underflow occurs • less interested in casualties: knowing how overflow/underflow affects – exploited by most static analysis methods (abstract interpretation) • soundness results depend on un-boundedness of variables 3 Existing Approaches (1/2) Encoding: Bit-blasting, Solver: Boolean SAT – – – – Both operands bounded Bit-blasting linear integer arithmetic can lead to large formula Arithmetic semantics is “lost” in such encoding For eg: CBMC Encoding: Bit-vector Arithmetic, Solver: SMT(BV) – – – – Preprocessor followed by a Boolean SAT overflow/underflow handled specific to machines architecture precision/scalability trade-off? For eg: Calysto (Program Analysis) using Spear Abstractions/Refinement – Iterative steps • SAT solver on (under-approx) bounded data paths, • an abstraction on UNSAT core, followed by • a refinement guided by Presburger/SAT solver – No incremental formulation • each problem solved and generated separately – For eg: ASAP, DP for bit-vector using abstraction 4 Existing Approaches (2/2) Encoding: Booleanization, Solver: SMT(LIA) – Naïve encoding for non-linear multiplications, bit-wise operations – Booleanization followed by Linearization Given integer x ∈ [0,2N) Introduce integer-vars xk = [0,1] for 0 ≤ k ≤ N-1 N −1 Linear Constraint x = ∑ 2k ∗c x k k =0 Boolean Constraint ∏ k Bitwise Relational Decomposition (BRD) B = ( x k == 1) k Boolean vector: BN-1 … Bk … B0 representing x – No guidance to SMT(LIA) • Solver has to guess Bk’s as it is not explicitly related to x – For eg: MathSat 5 Our Approach: Highlights Better Encoding (over BRD) – Bit-wise structural decomposition (BSD) • Structural relationship between a variable and its decomposition provides better guidance to solver – Linearize multiplier, divide, mod, shifts – Linearization criteria • rules to select non-linear operand for BSD. Lazy Bound Refinement (LBR) algorithm – Incremental formulation using under and over-approximations • Successive refined problems are solved incrementally – Refinement step • tighten bounds for un-decomposed variables (X variables) • relax bounds for decomposed variables (Y variables) – Exploits SMT(LIA) solvers’ incremental solving capability • assertion/retraction of bound constraints are typically supported 6 Our Approach: Overview Linear Arithmetic Constraints SMT(NLIA) Boolean combination of Non-Linear + Linear Integer Arithmetic on bounded integers LBR DP: Encoding + LBR SMT(LIA) Solver “Linearize” Integer Non-linear Operations ( ∗, /, %, <<, >>, &, ||, ⊗) 7 Linearization (multiplier) MULT: z = u ∗ v, with u,v unsigned integer (u ≥0, v>0 ) Select u for Boolean decomposition, UN-1 …U0 Initialize Partial Sum Final result Linearized Multiplier: r0 = 0 k r k +1 = r k + ITE (U k , 2 ∗C v,0) 0 ≤ k ≤ N −1 z = rN z = u ∗ v = u ∗L v if (u < 2 N ) z = x ∗ y, with x,y signed integer u = ITE ( x < 0,− x, x) v = ITE ( y < 0,− y, y ) w = u ∗L v z = ITE ( y < 0 ⊗ x < 0,− w, w) 8 Linearization (divide, mod) DIV: d = u/v, with u≥0,v>0 (general case similar to multiplier) MOD: r=u%v, with u≥0,v>0 (general case similar to multiplier) Bounding Constraint DIV MOD u − v + 1 ≤ t ∗L v ≤ u t is integer-var d = ITE (u < v,0, ITE (u == v,1, ITE (v == 1, u , t ))) r = ITE (u < v, u , ITE (u == v,0, ITE (v == 1,0, u − t ))) 9 Linearization (bit-wise operation) z = u bop v, with u,v unsigned integer, bop ∈ {&,||, ⊗} UN-1 …U0 and VN-1 …V0 are bit decomposition of U and V, resp. Initialize Partial Sum Final result r0 = 0 k r k +1 = r k + ITE (U k bop V k , 2 ,0) 0 ≤ k ≤ N − 1 z = rN 10 Lazy Bounding and Refinement (LBR): Overview Input – Formula: SMT(LIA) φL(linearized formula) – Partition term sets: • X = {x1. …xn} terms not bit-decomposed • Y = {y1. …ym} terms bit-decomposed – Bounding constraints: -2N ≤ xi,yj < 2N Incremental Formulation – Do not re-encode the linearized formula φL – Use assert/retract procedures of the SMT(LIA) solver to tighten/relax bounding constraints Start yj variables with small bound, relax as needed – -b(yj) ≤ yj < b(yj), with b(yj) = 2β , 0<β≤N – predicates Bk (kth bit of yj) gets simplified to false for k≥β – increase β as required Start xi variables with no bounds, tighten as needed – add constraints -2N ≤ xi < 2N as needed 11 LBR Algorithm (flow) SMT_Init(φL) Linearized SMT(LIA) : φL Partition term-sets: X,Y ∀ y∈Y b( y ) = 1 X b = Φ ;Y b = Y Relax Bound SMT_Assert(φXb) SMT_Assert(φYb) Tighten Bound Xb←Xb’ ∀ y∈Y b b( y ) ← 2 ∗ b( y ) ϕ Y b = ∧ y∈Y b (−b( y ) ≤ y < b( y )) ϕ X b = ∧ x∈X b (− 2 N ≤ x < 2 N ) N ϕ Y b = ∧ y∈Y (−b( y ) ≤ y < b( y )) b Y Xb’=Xb? Xb’ := Xb ∪ {x | -2N > α(x) or 2N ≤ α(x)} SAT UNSAT Y N SAT? α: sat assgn N Y SMT_Check Yb =∅? Relax Bound Tighten Bound SMT_Retract(φYb) Yb := {y | -b(y) ≤ y or b(y) < y) cause for UNSAT with b(y) < 2N} 12 LBR: Termination and Correctness Theorem 1: LBR always terminates It requires O(n+N.m) iterations where – n is the number of X variables, – m is the number of Y variables – [-2N,2N) is the system bound Theorem 2: LBR decides correctly Let φall be φL with -2N ≤ xi,yj < 2N Let φi be the formula at ith iteration when LBR terminates – Claim: φall satisfiable iff φi is satisfiable. 13 Linearization Criteria (LC) Given z = u ∗ v, prefer u over v as per following rules R1: u is an input operand to more MULT – to reduce number of operands considered for bit decomposition R2: u has a fewer MULT in its transitive input – to reduce bound relaxing refinements R3: u has lower bound size – to reduce bound relaxing refinements Candidate-sets for decomposition Example w2=u1∗ w1 ∗ w3=u2* u3 w1=u2* u2 ∗ ∗ u1 u2 u2 u3 Apply LC Y a = {u1 , u 2} Y b = {w1 , u 2} Y c = {u1 , u 2 , u 3} Y d = {w1 , u 2 , u 3} 14 Linearization Criteria (LC) Given z = u ∗ v, prefer u over v as per following rules R1: u is an input operand to more MULT – to reduce number of operands considered for bit decomposition R2: u has a fewer MULT in its transitive input – to reduce bound relaxing refinements R3: u has lower bound size – to reduce bound relaxing refinements Candidate-sets for decomposition Example w2=u1∗ w1 ∗ w3=u2* u3 w1=u2* u2 ∗ ∗ u1 u2 u2 u3 Apply LC Y a = {u1 , u 2} Y b = {w1 , u 2} Y c = {u1 , u 2 , u 3} Y d = {w1 , u 2 , u 3} 15 Linearization Criteria (LC) Given z = u ∗ v, prefer u over v as per following rules R1: u is an input operand to more MULT – to reduce number of operands considered for bit decomposition R2: u has a fewer MULT in its transitive input – to reduce bound relaxing refinements R3: u has lower bound size – to reduce bound relaxing refinements Candidate-sets for decomposition Example w2=u1∗ w1 ∗ w3=u2* u3 w1=u2* u2 ∗ ∗ u1 u2 u2 u3 Apply LC Y a = {u1 , u 2} Y b = {w1 , u 2} Y c = {u1 , u 2 , u 3} Y d = {w1 , u 2 , u 3} 16 Linearization Criteria (LC) Given z = u ∗ v, prefer u over v as per following rules R1: u is an input operand to more MULT – to reduce number of operands considered for bit decomposition R2: u has a fewer MULT in its transitive input – to reduce bound relaxing refinements R3: u has lower bound size – to reduce bound relaxing refinements Candidate-sets for decomposition Example w2=u1∗ w1 ∗ w3=u2* u3 w1=u2* u2 ∗ ∗ u1 u2 u2 u3 Apply LC Y a = {u1 , u 2} Y b = {w1 , u 2} Y c = {u1 , u 2 , u 3} Y d = {w1 , u 2 , u 3} 17 Linearization Criteria (LC) Given z = u ∗ v, prefer u over v as per following rules R1: u is an input operand to more MULT – to reduce number of operands considered for bit decomposition R2: u has a fewer MULT in its transitive input – to reduce bound relaxing refinements R3: u has lower bound size – to reduce bound relaxing refinements Candidate-sets for decomposition Example w2=u1∗ w1 ∗ w3=u2* u3 w1=u2* u2 ∗ ∗ u1 u2 u2 u3 Apply LC Y a = {u1 , u 2} Y b = {w1 , u 2} Y c = {u1 , u 2 , u 3} Y d = {w1 , u 2 , u 3} 18 Linearization Criteria (LC) Given z = u ∗ v, prefer u over v as per following rules R1: u is an input operand to more MULT – to reduce number of operands considered for bit decomposition R2: u has a fewer MULT in its transitive input – to reduce bound relaxing refinements R3: u has lower bound size – to reduce bound relaxing refinements Candidate-sets for decomposition Example w2=u1∗ w1 ∗ w3=u2* u3 w1=u2* u2 ∗ ∗ u1 u2 u2 u3 Y a = {u1 , u 2} Y b = {w1 , u 2} Y c = {u1 , u 2 , u 3} Y d = {w1 , u 2 , u 3} Apply LC R1 : Y c , Y d p Y a , Y b 19 Linearization Criteria (LC) Given z = u ∗ v, prefer u over v as per following rules R1: u is an input operand to more MULT – to reduce number of operands considered for bit decomposition R2: u has a fewer MULT in its transitive input – to reduce bound relaxing refinements R3: u has lower bound size – to reduce bound relaxing refinements Candidate-sets for decomposition Example w2=u1∗ w1 ∗ w3=u2* u3 w1=u2* u2 ∗ ∗ u1 u2 u2 u3 Y a = {u1 , u 2} Y b = {w1 , u 2} Y c = {u1 , u 2 , u 3} Y d = {w1 , u 2 , u 3} Apply LC R1 : Y c , Y d p Y a , Y b R2 : Y b p Y a 20 BSD: Bitwise Structural Decomposition Input: Bounded unsigned integer u ∈ [0, 2N) Output: Boolean decomposition, BN-1 …Bk … B0 Boolean Constraint tN = u k = ≥ ( Bk t k 2 ) Linear Constraint k t k −1 = ITE( B k , t k − 2 , t k ) N − 1 ≥ k ≥ 0 N −1 ≥ k ≥ 0 Compared to BRD approach No new integer variables, but – Additional N-1 linear constraints are introduced – Structural relationship between Boolean and intermediate terms is captured explicitly (pre-computed learning ) Note, y=ITE(S,a,b) is encoded using 2 CNF clauses 21 BSD Unfolded (example) t 3 = u = 13; 3 3 = ( 13 ≥ ) = 1 ; = 13 − t2 B3 2 2 =5 2 2 = ( 5 ≥ ) = 1 ; = 5 − t1 B2 2 2 =1 1 = ( 1 ≥ B1 2 ) = 0; t 0 = t1 = 1 0 = ( 1 ≥ B0 2 ) =1 B3 B 2 B1 B0 ≡ 1101 22 Encoding from φ to φL : Summary Input φ: SMT(NLIA), System bound: [-2N,2N) Ouput φL: SMT(LIA) (linearized formula) Partition terms into X and Y set using LC – X = {x1. …xn} variables that will not be decomposed – Y = {y1. …ym} variables that will be decomposed Decompose Y variables using BSD – Add Boolean constraints for ITE, predicates – Add intermediate term linear equation Linearize non-linear operations – Add Boolean constraints for ITE, predicates – Add linear constraints (partial sum) 23 Application: Software verification 0 1:1: int intfoo foo(int (intx)x){ { 2:2: int intss==x+2; x+2; 3:3: int t = s-3; int t = s-3; 4:4: ifif( (t>6 t>6) ) 5:5: t t==t t* *x;x; 6:6: else else 7:7: t t==t-1; t-1; 8:8: ss+= t; += t; 9:9: return returns;s; 10: 10: } } CFG Gen t>6 t = t * x; s = x+2; t = x-1; ! (t > 6) CFG t=t-1; 1 2 s += t; 3 Model Gen F-Soft B2 SMT problem with Linear + Non-Linear Integer Arithmetic on bounded integers t LBR DP: Encoding + LBR “Linearize” Integer Non-linear Operations ( ∗, /, %, <<, >>, &, ||, ⊗) B1 t Linear Arithmetic Constraints SMT (LIA) Solver 1 BMC B0 t x ∗ x 1 t’ - 24 Experiments (Comparisons) Solvers – LBR + SMT(LIA) solver yices (1.0.11) – SMT(BV) solver Z3 (ver 1.1) Linearization Criteria (for BSD) – LC (with linearization criteria R1-R3) – NLC (does not follow R1-R3) Encoding – BRD (bitwise relation decomposition) – BSD (bitwise structural decomposition) Decision procedures (uses BSD) – LBR-LE (Lazy bounds on X, Eager bounds on Y) – LBR-EL (Eager bounds on X, Lazy bounds on Y) – LBR-LL (Lazy bounds on X, Lazy Bounds on Y) 25 Experiment-1 (Controlled) Time Limit: 600s (1000s for Z3) Platform: 3.4GHz Linux (windows for Z3) DP S:f2,f3 S:f1,f2 S:f1,f3 S:f2 S:f1 D:f2,f3 D:f1,f4,f5 D:f4,f6(c1) D:f4,f6(c2) D:f4,f6(c3) D:f4,f6(c4) D:f4,f6(c4) D:f4,f6(c5) With linearization criteria (LC) No LC LBR-LE LBR-EL LBR-LL BRD-LL NLC-LL nx ny #R X:L nx ny #R X:L X:E X:L X:L 50 38 49 19 20 50 59 34 34 34 34 34 34 2 2 2 2 3 2 1 2 2 2 4 2 5 4 2 8 2 10 2 6 2 4 2 6 2 4 Y:E TO TO TO TO TO TO TO TO TO TO TO TO TO Y:L 4.1 2.1 10.9 0.7 3.1 16.0 104.3 19.2 86.3 10.1 3.3 10.7 3.3 Y:L 3.8 1.4 10.8 0.5 3.7 32.9 121.8 43.3 118.4 13.9 3.6 14.3 3.6 Y:L 58.4 54.5 286.2 1.6 9.5 58.2 560.8 47.5 154.0 21.4 9.2 13.2 8.0 46 37 47 18 20 48 58 33 33 33 33 33 33 6 3 5 2 2 6 6 3 3 3 3 3 3 4 4 4 4 2 7 8 10 7 7 7 7 Y:L 528.1 10.1 123.0 3.6 0.8 TO 297.1 68.9 169.0 50.9 61.9 60.6 60.3 Z3 1 175 38 195 1 TO 328 TO TO TO TO TO TO 26 Experiment-1 Time Limit: 600s (1000s for Z3) Platform: 3.4GHz Linux (windows for Z3) DP S:f2,f3 S:f1,f2 S:f1,f3 S:f2 S:f1 D:f2,f3 D:f1,f4,f5 D:f4,f6(c1) D:f4,f6(c2) D:f4,f6(c3) D:f4,f6(c4) D:f4,f6(c5) D:f4,f6(c6) With linearization criteria (LC) No LC LBR-LE LBR-EL LBR-LL BRD-LL NLC-LL f 1 ( x, y ) = x 2 y + 11 x 2 + 13 xy + 143 xy + 30 y + 330 nx ny #I nx ny #I X:L X:E X:L X:L X:L Z3 ( x) = x3Y:L 27 x + 27Y:L + 9 x 2 + Y:L f 2Y:E 50 38 49 19 20 50 59 34 34 34 34 34 34 2 2 3 1 2 4 5 2 2 2 2 2 2 Y:L 2 f TO 4.1 3.8 58.4 46 6 4 528.1 1 3 ( x, y ) = 12 xyz + 8 xz + 36 yz + 24 z + 6 xy + 4 x + 18 y + 12 2 TO 2.1 1.4 54.5 37 3 4 10.1 175 3 2 2 f TO 10.9 10.8 286.2 47 5 4 123.0 38 4 ( y ) = y + 27 y + 243 y + 729 2 TO 0.7 0.5 1.6 18 2 4 3.6 195 2 ( x) = x 3.1 − 3 x + 23.7 2 f 5TO 9.5 20 2 2 0.8 1 2 58.2 48 6 TO TO ( x, y, c)16.0 = xy − c32.9 (c: products f 6TO of primes) 4 TO 104.3 121.8 560.8 58 6 7 297.1 328 8 TO 19.2 43.3 47.5 33 3 8 68.9 TO f118.4 f3(x,y)=0 2,f3 ≡ Solve: 2(x)=0 ∧154.0 10 S:fTO 86.3 33 3 10 169.0 TO 6 D:fTO 10.1 21.4 33 3 7 50.9 TO f213.9 (x1)=0 ∧ f3(x2,y)=0 2,f3 ≡ Solve: 4 TO 3.3 3.6 9.2 33 3 7 61.9 TO 6 TO 10.7 14.3 13.2 33 3 7 60.6 TO 4 TO 3.3 3.6 8.0 33 3 7 60.3 TO 27 Experiment-1 Time Limit: 600s (1000s for Z3) Platform: 3.4GHz Linux (windows for Z3) DP S:f2,f3 S:f1,f2 S:f1,f3 S:f2 S:f1 D:f2,f3 D:f1,f4,f5 D:f4,f6(c1) D:f4,f6(c2) D:f4,f6(c3) D:f4,f6(c4) D:f4,f6(c4) D:f4,f6(c5) nx ny 50 38 49 19 20 50 59 34 34 34 34 34 34 With linearization criteria (LC) No LC LBR-LE LBR-EL LBR-LL BRD-LL NLC-LL #I nx ny #I X:L X:E X:L X:L X:L 2 2 2 2 3 2 1 2 2 2 4 2 5 4 2 8 2 10 2 6 2 4 2 6 2 4 Y:E TO TO TO TO TO TO TO TO TO TO TO TO TO Y:L 4.1 2.1 10.9 0.7 3.1 16.0 104.3 19.2 86.3 10.1 3.3 10.7 3.3 Y:L 3.8 1.4 10.8 0.5 3.7 32.9 121.8 43.3 118.4 13.9 3.6 14.3 3.6 Y:L 58.4 54.5 286.2 1.6 9.5 58.2 560.8 47.5 154.0 21.4 9.2 13.2 8.0 46 37 47 18 20 48 58 33 33 33 33 33 33 6 3 5 2 2 6 6 3 3 3 3 3 3 4 4 4 4 2 7 8 10 7 7 7 7 Y:L 528.1 10.1 123.0 3.6 0.8 TO 297.1 68.9 169.0 50.9 61.9 60.6 60.3 Z3 1 175 38 195 1 TO 328 TO TO TO TO TO TO Number of Y variables 28 Experiment-1 Time Limit: 600s (1000s for Z3) Platform: 3.4GHz Linux (windows for Z3) DP S:f2,f3 S:f1,f2 S:f1,f3 S:f2 S:f1 D:f2,f3 D:f1,f4,f5 D:f4,f6(c1) D:f4,f6(c2) D:f4,f6(c3) D:f4,f6(c4) D:f4,f6(c4) D:f4,f6(c5) nx ny 50 38 49 19 20 50 59 34 34 34 34 34 34 With linearization criteria (LC) No LC LBR-LE LBR-EL LBR-LL BRD-LL NLC-LL #I nx ny #I X:L X:E X:L X:L X:L 2 2 2 2 3 2 1 2 2 2 4 2 5 4 2 8 2 10 2 6 2 4 2 6 2 4 Y:E TO TO TO TO TO TO TO TO TO TO TO TO TO Y:L 4.1 2.1 10.9 0.7 3.1 16.0 104.3 19.2 86.3 10.1 3.3 10.7 3.3 Y:L 3.8 1.4 10.8 0.5 3.7 32.9 121.8 43.3 118.4 13.9 3.6 14.3 3.6 Y:L 58.4 54.5 286.2 1.6 9.5 58.2 560.8 47.5 154.0 21.4 9.2 13.2 8.0 46 37 47 18 20 48 58 33 33 33 33 33 33 6 3 5 2 2 6 6 3 3 3 3 3 3 4 4 4 4 2 7 8 10 7 7 7 7 Y:L 528.1 10.1 123.0 3.6 0.8 TO 297.1 68.9 169.0 50.9 61.9 60.6 60.3 Z3 1 175 38 195 1 TO 328 TO TO TO TO TO TO Number of Relaxations 29 Experiment-1 Time Limit: 600s (1000s for Z3) Platform: 3.4GHz Linux (windows for Z3) DP S:f2,f3 S:f1,f2 S:f1,f3 S:f2 S:f1 D:f2,f3 D:f1,f4,f5 D:f4,f6(c1) D:f4,f6(c2) D:f4,f6(c3) D:f4,f6(c4) D:f4,f6(c4) D:f4,f6(c5) With linearization criteria (LC) No LC LBR-LE LBR-EL LBR-LL BRD-LL NLC-LL nx ny #I nx ny #I X:L X:E X:L X:L X:L 50 38 49 19 20 50 59 34 34 34 34 34 34 2 2 2 2 3 2 1 2 2 2 4 2 5 4 2 8 2 10 2 6 2 4 2 6 2 4 Y:E TO TO TO TO TO TO TO TO TO TO TO TO TO Y:L 4.1 2.1 10.9 0.7 3.1 16.0 104.3 19.2 86.3 10.1 3.3 10.7 3.3 Y:L 3.8 1.4 10.8 0.5 3.7 32.9 121.8 43.3 118.4 13.9 3.6 14.3 3.6 Y:L 58.4 54.5 286.2 1.6 9.5 58.2 560.8 47.5 154.0 21.4 9.2 13.2 8.0 46 37 47 18 20 48 58 33 33 33 33 33 33 6 3 5 2 2 6 6 3 3 3 3 3 3 4 4 4 4 2 7 8 10 7 7 7 7 Y:L 528.1 10.1 123.0 3.6 0.8 TO 297.1 68.9 169.0 50.9 61.9 60.6 60.3 Z3 1 175 38 195 1 TO 328 TO TO TO TO TO TO Solve Time 30 Experiment-1 Time Limit: 600s (1000s for Z3) Platform: 3.4GHz Linux (windows for Z3) DP S:f2,f3 S:f1,f2 S:f1,f3 S:f2 S:f1 D:f2,f3 D:f1,f4,f5 D:f4,f6(c1) D:f4,f6(c2) D:f4,f6(c3) D:f4,f6(c4) D:f4,f6(c4) D:f4,f6(c5) With linearization criteria (LC) No LC NLC-LL LBR-LE LBR-EL LBR-LL BRD-LL nx ny #I nx ny #I X:L X:E X:L X:L X:L 50 38 49 19 20 50 59 34 34 34 34 34 34 2 2 2 2 3 2 1 2 2 2 4 2 5 4 2 8 2 10 2 6 2 4 2 6 2 4 Y:E TO TO TO TO TO TO TO TO TO TO TO TO TO Y:L 4.1 2.1 10.9 0.7 3.1 16.0 104.3 19.2 86.3 10.1 3.3 10.7 3.3 Y:L 3.8 1.4 10.8 0.5 3.7 32.9 121.8 43.3 118.4 13.9 3.6 14.3 3.6 Y:L 58.4 54.5 286.2 1.6 9.5 58.2 560.8 47.5 154.0 21.4 9.2 13.2 8.0 46 37 47 18 20 48 58 33 33 33 33 33 33 6 3 5 2 2 6 6 3 3 3 3 3 3 4 4 4 4 2 7 8 10 7 7 7 7 Y:L 528.1 10.1 123.0 3.6 0.8 TO 297.1 68.9 169.0 50.9 61.9 60.6 60.3 Z3 1 175 38 195 1 TO 328 TO TO TO TO TO TO Solve Time 31 Experiment-1 Time Limit: 600s (1000s for Z3) Platform: 3.4GHz Linux (windows for Z3) DP S:f2,f3 S:f1,f2 S:f1,f3 S:f2 S:f1 D:f2,f3 D:f1,f4,f5 D:f4,f6(c1) D:f4,f6(c2) D:f4,f6(c3) D:f4,f6(c4) D:f4,f6(c4) D:f4,f6(c5) With linearization criteria (LC) No LC NLC-LL LBR-LE LBR-EL LBR-LL BRD-LL nx ny #I nx ny #I X:L X:E X:L X:L X:L 50 38 49 19 20 50 59 34 34 34 34 34 34 2 2 2 2 3 2 1 2 2 2 4 2 5 4 2 8 2 10 2 6 2 4 2 6 2 4 Y:E TO TO TO TO TO TO TO TO TO TO TO TO TO Y:L 4.1 2.1 10.9 0.7 3.1 16.0 104.3 19.2 86.3 10.1 3.3 10.7 3.3 Y:L 3.8 1.4 10.8 0.5 3.7 32.9 121.8 43.3 118.4 13.9 3.6 14.3 3.6 Y:L 58.4 54.5 286.2 1.6 9.5 58.2 560.8 47.5 154.0 21.4 9.2 13.2 8.0 46 37 47 18 20 48 58 33 33 33 33 33 33 6 3 5 2 2 6 6 3 3 3 3 3 3 4 4 4 4 2 7 8 10 7 7 7 7 Y:L 528.1 10.1 123.0 3.6 0.8 TO 297.1 68.9 169.0 50.9 61.9 60.6 60.3 Z3 1 175 38 195 1 TO 328 TO TO TO TO TO TO Solve Time 32 Experiment-1 Time Limit: 600s (1000s for Z3) Platform: 3.4GHz Linux (windows for Z3) DP S:f2,f3 S:f1,f2 S:f1,f3 S:f2 S:f1 D:f2,f3 D:f1,f4,f5 D:f4,f6(c1) D:f4,f6(c2) D:f4,f6(c3) D:f4,f6(c4) D:f4,f6(c4) D:f4,f6(c5) With linearization criteria (LC) No LC LBR-LE LBR-EL LBR-LL BRD-LL NLC-LL nx ny #I nx ny #I X:L X:E X:L X:L X:L 50 38 49 19 20 50 59 34 34 34 34 34 34 2 2 2 2 3 2 1 2 2 2 4 2 5 4 2 8 2 10 2 6 2 4 2 6 2 4 Y:E TO TO TO TO TO TO TO TO TO TO TO TO TO Y:L 4.1 2.1 10.9 0.7 3.1 16.0 104.3 19.2 86.3 10.1 3.3 10.7 3.3 Y:L 3.8 1.4 10.8 0.5 3.7 32.9 121.8 43.3 118.4 13.9 3.6 14.3 3.6 Y:L 58.4 54.5 286.2 1.6 9.5 58.2 560.8 47.5 154.0 21.4 9.2 13.2 8.0 46 37 47 18 20 48 58 33 33 33 33 33 33 6 3 5 2 2 6 6 3 3 3 3 3 3 4 4 4 4 2 7 8 10 7 7 7 7 Y:L 528.1 10.1 123.0 3.6 0.8 TO 297.1 68.9 169.0 50.9 61.9 60.6 60.3 Z3 1 175 38 195 1 TO 328 TO TO TO TO TO TO Solve Time 33 Experiment-2 (SMT-based BMC) Time Limit: 600s (1000s for Z3) Platform: 3.4GHz Linux (windows for Z3) LBR-LE LBR-EL LBR-LL BRD-LL Ex #R G-1891-61 G-21-3 G-273-13 G-7747-127 G-91-13 L-1891-1830 L-21-14 L-273-260 L-91-78 2 2 2 2 2 2 4 8 10 X:L Y:E 27.9 1.1 5.1 54.6 2.6 123.9 15.4 70.6 20.4 X:E Y:L 11.4 1.4 3.0 19.6 3.4 51.0 7.7 35.6 13.8 X:L Y:L 12.1 0.8 2.4 3.6 2.9 137.7 10.5 37.5 21.0 X:L Y:L 4.6 2.4 2.9 9.1 2.8 333.8 9.8 56.2 27.1 Z3 497 7 26 77 20 TO TO TO TO 34 Experiment-2 Ex #R G-1891-61 G-21-3 G-273-13 G-7747-127 G-91-13 L-1891-1830 L-21-14 L-273-260 L-91-78 2 2 2 2 2 2 4 8 10 Time Limit: 600s (1000s for Z3) /* Parameters p1-p2*/ Platform: Linux (windows for Z3) void gcd-p1-p2(int x, 3.4GHz int y) { LBR-LE LBR-EL LBR-LL BRD-LL Z3 int g; int count=1; X:L X:E X:L X:L g = gcd(x,y); Y:E Y:L Y:L Y:L if (x + y == p1 && g == p2) 27.9 11.4 12.1 4.6 497 count -= 1; 1.1 1.4count); 0.8 2.4 7 assert( 3.0 2.4 2.9 26 }5.1 54.6 gcd(a,b) 19.6 3.6 9.1 77 int 3.4 2.9 2.8 20 {2.6 123.9 333.8 TO while 51.0 (b!=0) 137.7 { 15.4 int t 7.7= b; 10.5 9.8 TO a % b; 37.5 70.6 b = 35.6 56.2 TO t; 20.4 a = 13.8 21.0 27.1 TO } return a; } 35 Experiment-2 Ex #R G-1891-61 G-21-3 G-273-13 G-7747-127 G-91-13 L-1891-1830 L-21-14 L-273-260 L-91-78 2 2 2 2 2 2 4 8 10 /* Parameters p3-p4*/ void lcm-p3-p4(int x, (1000s int y) Time Limit: 600s for Z3) Platform: 3.4GHz Linux (windows for Z3) { int g,l; int count=1; LBR-LE LBR-EL LBR-LL BRD-LL Z3 g = gcd(x,y); X:L X:E X:L X:L l = (x * y)/g; //LCM Y:E Y:L p3 &&Y:Ll == p4) ifY:L (x+y == 27.9 11.4 12.11; 4.6 497 count -= 1.1 1.4 0.8 2.4 7 assert( count); 5.1 } 3.0 2.4 2.9 26 54.6 int 19.6 3.6 9.1 77 gcd(a,b) 2.6 { 3.4 2.9 2.8 20 123.9 while 51.0 (b!=0) 137.7 { 333.8 TO int t = b; 15.4 7.7 10.5 9.8 TO b = a % b; 70.6 35.6 37.5 56.2 TO a = t; 21.0 20.4 13.8 27.1 TO } return a; } 36 Experiment-2 Time Limit: 600s (1000s for Z3) Platform: 3.4GHz Linux (windows for Z3) LBR-LE LBR-EL LBR-LL BRD-LL Ex #R G-1891-61 G-21-3 G-273-13 G-7747-127 G-91-13 L-1891-1830 L-21-14 L-273-260 L-91-78 2 2 2 2 2 2 4 8 10 X:L Y:E 27.9 1.1 5.1 54.6 2.6 123.9 15.4 70.6 20.4 X:E Y:L 11.4 1.4 3.0 19.6 3.4 51.0 7.7 35.6 13.8 X:L Y:L 12.1 0.8 2.4 3.6 2.9 137.7 10.5 37.5 21.0 X:L Y:L 4.6 2.4 2.9 9.1 2.8 333.8 9.8 56.2 27.1 Z3 497 7 26 77 20 TO TO TO TO Solve Time 37 Experiment-2 Time Limit: 600s (1000s for Z3) Platform: 3.4GHz Linux (windows for Z3) LBR-LE LBR-EL LBR-LL BRD-LL Ex #R G-1891-61 G-21-3 G-273-13 G-7747-127 G-91-13 L-1891-1830 L-21-14 L-273-260 L-91-78 2 2 2 2 2 2 4 8 10 X:L Y:E 27.9 1.1 5.1 54.6 2.6 123.9 15.4 70.6 20.4 X:E Y:L 11.4 1.4 3.0 19.6 3.4 51.0 7.7 35.6 13.8 X:L Y:L 12.1 0.8 2.4 3.6 2.9 137.7 10.5 37.5 21.0 X:L Y:L 4.6 2.4 2.9 9.1 2.8 333.8 9.8 56.2 27.1 Z3 497 7 26 77 20 TO TO TO TO Solve Time 38 Experiment-2 Time Limit: 600s (1000s for Z3) Platform: 3.4GHz Linux (windows for Z3) LBR-LE LBR-EL LBR-LL BRD-LL Ex #R G-1891-61 G-21-3 G-273-13 G-7747-127 G-91-13 L-1891-1830 L-21-14 L-273-260 L-91-78 2 2 2 2 2 2 4 8 10 X:L Y:E 27.9 1.1 5.1 54.6 2.6 123.9 15.4 70.6 20.4 X:E Y:L 11.4 1.4 3.0 19.6 3.4 51.0 7.7 35.6 13.8 X:L Y:L 12.1 0.8 2.4 3.6 2.9 137.7 10.5 37.5 21.0 X:L Y:L 4.6 2.4 2.9 9.1 2.8 333.8 9.8 56.2 27.1 Z3 497 7 26 77 20 TO TO TO TO Solve Time 39 Experiment-3 (SMT-based BMC) Time Limit: 1000s Platform: 3.4GHz Linux Ex(#prp) B1(88) B2(12) B3(33) B4(14) B5(57) B6(5) B7(1) LBR-LE X:L, Y:E TLW DTO #W 69.0 143.6 67.3 831.1 184.1 138 24 12 8 29 119 161 40 2 1 0 0 2 1 LBR-EL X:E, Y:L TLW DTO #W 69.8 5.1 962.1 51.8 878.9 31.5 4.2 138 303 232 363 181 467 161 40 7 22 10 17 3 1 LBR-LL X:L, Y:L TLW DTO #W 30.3 7.2 821.6 26.1 946.6 5.7 1.2 241 436 261 530 184 590 161 40 7 23 10 18 3 1 TLW 30.3 6.6 772.2 45.7 981.2 24.5 1.6 BRD X:L, Y:L #W DTO 241 399 234 386 173 532 161 40 7 22 10 15 3 1 40 Experiment-3 Time Limit: 1000s Platform: 3.4GHz Linux Ex(#prp) B1(88) B2(12) B3(33) B4(14) B5(57) B6(5) B7(1) LBR-LE X:L, Y:E • TLW DTO #W 69.0 143.6 67.3 831.1 184.1 138 24 12 8 29 119 161 LBR-EL LBR-LL BRD X:E, Y:L X:L, Y:L X:L, Y:L C programs (industry+public domain) TLW DTO #W TLW DTO #W TLW DTO #W - linux drivers, network app, embed soft. 40 69.8 138 40 30.3 241 40 30.3 241 - predominately linear operators with 303 7 2 5.1sporadic 6.6 399 7.2 operators: 436 7 /,%,& non-linear 232 22 821.6 261 23 772.2 234 1• 962.1 Properties 363 10 26.1 530assertions 0 51.8 10 45.7 386 - array-bound-violations, 0 2 1 878.9 181 31.5 467 4.2 161 17 3 1 946.6 184 5.7 590 1.2 161 18 3 1 981.2 24.5 1.6 173 532 161 40 7 22 10 15 3 1 41 Experiment-3 Time Limit: 1000s Platform: 3.4GHz Linux Ex(#prp) B1(88) B2(12) B3(33) B4(14) B5(57) B6(5) B7(1) LBR-LE X:L, Y:E TLW DTO #W 69.0 143.6 67.3 831.1 184.1 138 24 12 8 29 119 161 40 2 1 0 0 2 1 LBR-EL X:E, Y:L TLW DTO #W 69.8 5.1 962.1 51.8 878.9 31.5 4.2 138 303 232 363 181 467 161 40 7 22 10 17 3 1 LBR-LL X:L, Y:L TLW DTO #W 30.3 7.2 821.6 26.1 946.6 5.7 1.2 241 436 261 530 184 590 161 40 7 23 10 18 3 1 TLW 30.3 6.6 772.2 45.7 981.2 24.5 1.6 BRD X:L, Y:L DTO #W 241 399 234 386 173 532 161 40 7 22 10 15 3 1 Number of witnesses found 42 Experiment-3 Time Limit: 1000s Platform: 3.4GHz Linux Ex(#prp) B1(88) B2(12) B3(33) B4(14) B5(57) B6(5) B7(1) LBR-LE X:L, Y:E TLW DTO #W 69.0 143.6 67.3 831.1 184.1 138 24 12 8 29 119 161 40 2 1 0 0 2 1 LBR-EL X:E, Y:L TLW DTO #W 69.8 5.1 962.1 51.8 878.9 31.5 4.2 138 303 232 363 181 467 161 40 7 22 10 17 3 1 LBR-LL X:L, Y:L TLW DTO #W 30.3 7.2 821.6 26.1 946.6 5.7 1.2 241 436 261 530 184 590 161 40 7 23 10 18 3 1 TLW 30.3 6.6 772.2 45.7 981.2 24.5 1.6 BRD X:L, Y:L DTO #W 241 399 234 386 173 532 161 40 7 22 10 15 3 1 Time to find last witness 43 Summary/Conclusions Efficient decision procedure for non-linear theory for bounded integers – Improved bit-wise decomposition • pre-computed learning providing guidance to SMT solver • compared BSD v/s BRD – Improved linearization • linearization criteria: reduces number of refinement steps • compared LC v/s NLC – Lazy-bounding and refinement algorithm • Incremental formulation, exploits incremental capability of SMT(LIA) solvers • Avoids re-encoding, thereby, improves performances overall • compared LBR-LL, LBR-LE, LBR-EL, Z3 Effective for verification of application programs – Overflow and underflow not used as programming feature – Non-linear terms used sporadically, Boolean and linear terms mostly – SMT(BV) solver may be overkill for such applications 44 Questions 45