Presentation

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