Satisfiability Modulo Theory (SMT)
Dr. September 12, 2022
Why Satisfiability Modulo Theory (SMT) Explicit model checking suffers from state space explosion
Explicit model checking not very well suited for proof of equivalence between different programs, e.g, specification and optimised programs.
Copyright By PowCoder代写 加微信 powcoder
SMT is well suited for any verification and constraint problems.
– Solving sudoku and other games.
– Used in package managers for dependence analysis – Used for checking program security see here
– Used for verifying device drivers see here
SMT good for any optimisation problem, see here
Our very first problem in SMT solver
• Consider the linear system of inequalities in Equation 1:
x + y ≥ 10
x − y ≥ 20 (1)
• What are some integer values of x and y that satisfy the inequalities?
• Multiple ways of doing this, e.g., Gaussian elimination, by substituting, etc. • I will show manual solving:
x + y ≥ 10 ∴ x ≥ 10 − y ∴ 10 − y − y ≥ 20 ∴−2y≥10 =⇒ y≤−5
∴x≥10−(−5) =⇒ x≥15 (2) • We use SMT solver called Z3 from Microsoft as shown in Listing 1
1 #!/usr/bin/env python3 2
3 # Using the z3 SMT solver with python3 bindings
4 from z3 import IntSort, Solver, sat, And, Consts
5 # Importing the datatype Int, the Solver class, and the ‘sat’ variable.
6 # Finally, the And (logical And class)
8 def main():
9 # Declaring and defining the two variables.
10 x, y = Consts(‘x y’, IntSort()) # IntSort just stands for Int (type) 11
12 s = Solver() # Initialising the solver
14 # Adding the equations into the solver
15 s.add(And(x + y >= 10, x – y >= 20))
17 # Show the state of the solver
18 print(‘Solver state: %s’ % s)
20 # Solving for all free variables: x and y
21 ret = s.check()
23 # Check if there is some assignment for x and y
24 # that satisfy the equations
25 if ret == sat:
26 print(‘Result:’)
27 print(‘x: %s’ % s.model()[x])
28 print(‘y: %s’ % s.model()[y])
31 # Calling the main function in python
32 if __name__ == ‘__main__’:
# Just for debugging
Figure 1: Example 1
1 Solver state: [And(x + y >= 10, x – y >= 20)]
• See Z3 documentation • See Z3 API
Figure 2: Results for Example 1
3 Hardware circuit equivalence
3.1 Consider a 1-bit adder circuit described by a designer.
• We have three inputs Cin, A, and B.
• We have two outputs, Sum and Carry.
• There are a number of gates that compute the Sum and the Carry.
3.2 Consider another 1-bit adder
• Again we have the same number of inputs and outputs. 3
• The second implementation is a whole lot better than the first one.
• The second implementation has fewer number of gates and hence is optimised.
3.3 We want to prove that the two implementations are equivalent
• The first implementation can be encoded in binary logic as shown in Equations 3 and 4.
((¬A) ∧ (¬B) ∧ C)∨
((¬A) ∧ B ∧ (¬C))∨
(A ∧ (¬B) ∧ (¬C))∨
(A ∧ B ∧ C) (3)
Carryf ⇔(B∧C)∨(A∧C)∨(A∧B) (4) • The logical operators mean the following:
1. ⇔ is logical equivalence.
2. ¬ is logical negation (or not).
3. ∧ is logical conjunction (or and).
4. ∨ is logical disjunction (or operator). 5. ⊕ is logical XOR.
• The logic can be encoded into Z3 solver as follows:
1 # Note the captialisation of Boolean operators.
2 from z3 import And, Not, Or, solver
functional(Sumf, Carryf, A, B, C, s):
# Note <=> is converted into ==
s.add(Sumf == Or(And(Not(A), Not(B), C),
And(Not(A), B, Not(C)),
And(A, Not(B), Not(C)),
And(A, B, C)))
s.add(Carryf == Or(And(B, C), And(A, C), And(A, B)))
• The second implementation can be encoded into binary logic as shown in Equation 5
u⇔A⊕B v ⇔ (u ∧ C) w ⇔ (A ∧ B)
Si ⇔ u ⊕ C
Ci ⇔ (w ∨ v) (5)
1 from z3 import And, Not, Xor, BoolSort, Or, sat
2 from z3 import Solver, Consts
implementation(Si, Ci, A, B, C, s):
u, v, w = Consts(‘u, v, w’, BoolSort())
s.add(u == Xor(A, B))
s.add(v == And(u, C))
s.add(w == And(A, B))
s.add(Si == Xor(u, C))
s.add(Ci == Or(w, v))
functional(sumf, carryf, a, b, c, s):
s.add(sumf == Or(And(Not(a), Not(b), c),
And(Not(a), b, Not(c)),
And(a, Not(b), Not(c)),
And(a, b, c)))
s.add(carryf == Or(And(b, c), And(a, c), And(a, b)))
implementation(Si, Ci, A, B, C, s):
u, v, w = Consts(‘u, v, w’, BoolSort())
s.add(u == Xor(A, B))
s.add(v == And(u, C))
s.add(w == And(A, B))
s.add(Si == Xor(u, C))
s.add(Ci == Or(w, v))
A, B, Cin = Consts(‘A, B, Cin’, BoolSort())
Sf, Cf = Consts(‘Sf, Cf’, BoolSort())
s = Solver()
functional(Sf, Cf, A, B, Cin, s)
Si, Ci = Consts(‘Si, Ci’, BoolSort())
implementation(Si, Ci, A, B, Cin, s)
• The two implementations are equivalent ⇔, if and only if
– For all inputs Sumf ⇔ Si ∧ Carryf ⇔ Ci
– Equivalently, there exists no input values for A, B, C, such that, (Sumf ⊕ Si) ∨ (Carrf ⊕ Ci) is satisfied.
– The above is called a ”mitre” circuit.
– The SMT encoding is shown in Listing 3
1 #!/usr/bin/env python3 2
3 from z3 import And, Not, Xor, BoolSort, Or, sat
4 from z3 import Solver, Consts
27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43
44 if __name__ == ‘__main__’:
# Now the “mitre” circuit
s.add(Or(Xor(Sf, Si), Xor(Cf, Ci)))
# Check if the circuits are equivalent
if s.check() == sat:
print(‘Circuits not equivalent’)
print(s.model()) # print the values of A, B, C, etc.
print(‘Circuits are equivalent’)
1 Circuits are equivalent
Figure 3: Hardware Equivalence Encoding
Figure 4: Results for Hardware Equivalence in Listing 3 5
10 11 12 13 14
/* Optimised by the compiler */
int power3_impl(int i){
4 Software program code equivalence
4.1 Equivalence of two C++ programs Example 1
• Consider the two pieces of C++ programs in Listing 5
• Function power3_func is written by the programmer
• Function power3_impl is the optimised code translated by the compiler
• We want to show that for all input values i, the output is the same for both programs • Logically we want to show that ∀i ∈ Z, outl == outr
• Equivalently, we want to show that: ¬(∃i ∈ Z, outl ̸= outr)
• We want to do this at compile time, without running the program.
• This is called proving compiler correctness.
/* Written by the programmer */
int power3_func(int i){
for (int ii = 0; ii < 2; ++ii) {
8 return outl; 9}
outl *= i;
int outr = ((i * i) * i);
return outr;
8 return outl; 9}
10 11 12 13 14 15 16
/* SSA form */
int power3_func_ssa(int i){
int o1 = i;
/* Loop unrolled */
int o2 = o1 * i;
outl *= i;
Figure 5: Hand written and optimised programs
4.1.1 Step-1 change programs into single static assignment (SSA) format
• Every variable is assigned only once
• Requires unrolling the loop
• One assignment for each loop iteration • See Listing 6
/* Original form */
int power3_func(int i){
for (int ii = 0; ii < 2; ++ii) {
/* iteration 1 */
17 outl = o2 * i; /* iteration 2 */
18 return outl;
Figure 6: SSA representation of the program
4.1.2 Step-2 model the SSA form of the program into logic
• We have the logic from power3_func_ssa program as shown in Equation 6
(o1 == i)∧(o2 == o1∗i)∧(outl == o2∗i) (6)
• The logic from power3_impl is shown in Equation 7
(outr == ((i∗i)∗i) (7)
4.1.3 Step-3 encoding the logical formulas in SMT (Z3)
• The SMT encoding is shown in Listing 7
1 #!/usr/bin/env python3
2 # The standard imports
3 from z3 import Solver, sat, And, Consts
# Importing the type Int
from z3 import IntSort
s = Solver()
# Declaring the variables we need
i, o1, o2, outl, outr = Consts('i o1 o2 outl outr', IntSort())
# Encode outl
s.add(And(o1 == i, o2 == (o1 * i), outl == (o2 * i)))
10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28
29 if __name__ == '__main__':
# Encode outr
s.add(outr == (i * (i * i)))
if s.check() == sat:
print('Codes not equivalent, example:')
print(s.model())
print('Codes are equivalent')
# IntSort is typedef for Int type
# Importing the solver
# Encode the condition that there exists no i, such that outl !=
s.add(outl != outr)
1 Codes are equivalent
Figure 7: SMT encoding of the software program equivalence, Example 1
Figure 8: Results for Listing 7 7
4.2 Equivalence of two C++ programs Example 2
• Similar to Example 1, see Listing 9
– Using addition instead of multiplication
– Using float type instead of int type
– We want to prove that add3_func and add3_impl outputs are the same for every input i.
/* Written by the programmer */
float add3_func(float i){
8 return outl; 9}
float outl;
for (int ii = 0; ii < 2; ++ii) {
outl += i;
10 /* Optimised by the compiler */
11 float add3_impl(float i){
12 float outr = ((i + i) + i);
13 return outr;
Figure 9: Hand written and optimised programs
4.2.1 Encoding the equivalence logical formulas in SMT (Z3)
• Same as before, with minor changes, see Listing 10
1 #!/usr/bin/env python3
2 from z3 import Solver, sat, And, Consts
# Importing the Real type, to simulate floats
from z3 import RealSort
s = Solver()
# Declaring variables as Reals
i, o1, o2, outl, outr = Consts('i o1 o2 outl outr', RealSort())
# Make add3_func_ssa format
s.add(And(o1 == i, o2 == (o1 + i), outl == (o2 + i)))
10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27
28 if __name__ == '__main__':
# Make outr
s.add(outr == (i + (i + i)))
# Add the equivalence statement
s.add(outl != outr)
if s.check() == sat:
print('Codes not equivalent, example:')
print(s.model())
print('Codes are equivalent')
Figure 10: SMT encoding for software program equivalence, Example 2 8
Codes are equivalent
10 11 12 13 14 15
template
/* Optimised by the compiler */
T add3_impl(T i){
T outr = ((i + i) + i);
return outr;
Figure 12: Generic types in C++ • The type signature of add3_func is: T add3_func(T)
• The type signature of add3_impl is: T add3_impl(T)
• The type signature of operator+ is: T operator+ (T, T)
• The type signature of operator+= is: T operator+= (T, T)
• The type signature of operator= is: T operator= (T, T)
• The return type is T
• The inputs are also of type T
• SMT steals this idea of C++ templates to implement generic types • All variables are now declared with type T
• The partial encoding is given in Listing 13 with type T
Figure 11: Results for Listing 10 • There are some challenges and questions:
1. For every function *, +, etc, we need to encode it into SMT and prove its correctness.
2. For every type int, float, double, etc we need to encode it into SMT and prove its correctness.
3. Can we do better?
4. Can we make a general statement about correctness of the above program irrespective of types and operators?
4.3 Generic software program equivalence
• Have a general type, int, float, unsigned char, etc. • Have a general function, *, +, etc.
4.3.1 Generalising the types via Sorts
• Consider the generic C++ program for add3_func and add3_impl in Listing 12
for (int ii = 0; ii < 2; ++ii) {
template
T add3_func(T i){
8 return outl; 9}
outl += i;
• We are missing the logic of the SMT program in Listing 13
1 #!/usr/bin/env python3
2 from z3 import Solver, sat, And, Consts
general():
from z3 import DeclareSort
# Declare the new type T
T = DeclareSort(‘T’)
10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27
28 if __name__ == ‘__main__’:
29 general()
s = Solver()
# Declare the variables of type T
i, o1, o2, outl, outr = Consts(‘i o1 o2 outl outr’, T)
# FIXME: Here we need to fill in the logic
# Same as before, checking if for some i, outl and outr are
# different.
s.add(outl != outr)
if s.check() == sat:
print(‘Codes not equivalent, example:’)
print(s.model())
print(‘Codes are equivalent’)
Figure 13: SMT encoding with generic sort (type)
4.3.2 Generalising the operators via uninterpreted functions
• We want a generic function f, which captures properties of all *, +, etc operators. • We simply replace the operator with some random function ”f”
• See the C++ code in Listing 14
2 template
3 // We will not define the function f.
4 // We will let SMT define the function for us!
5 Tf(T,T);
7 template
9 10 11 12 13 14
add3_func(T i){
for (int ii = 0; ii < 2; ++ii) {
outl = f(outl, i);
return outl;
// Replaced the operator with f
17 template
18 /* Optimised by the compiler */
19 T add3_impl(T i){
20 T outr = f(f(i, i), i); // Replaced the operator with f
21 return outr;
Figure 14: Generic function and types in C++
• Just like defining a generic function in C++, we define a generic function f in SMT.
• Moreover, we replace all uses of +, *, etc, with just f as we have done in the C++ code. • This function f is called an uninterpreted function in SMT
• Function ”f” has no definition, and hence, no semantics.
• The logic with the generic function f is shown in Equation 8
(o1 == i) ∧ (o2 == f(o1, i)) ∧ (outl == f(o2, i))
(outr == f (f (i, i), i) (8)
4.3.3 Encoding the generic equivalence formula in SMT (Z3)
• The generic encoding in SMT is shown in Listing 15
1 #!/usr/bin/env python3
2 from z3 import Solver, sat, And, Consts
10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36
s = Solver()
general():
from z3 import Function, ForAll, DeclareSort
# Declaring the new type T
T = DeclareSort(‘T’)
# A new Type “T”
# Declaring the variables we need for type T
i, o1, o2, outl, outr = Consts(‘i o1 o2 outl outr’, T)
# Declaring the new function “f” of type signature: (T, T) -> T
f = Function(‘f’, T, T, T)
# Make outl, replacing the operator with f everywhere
s.add(And(o1 == i, o2 == f(o1, i), outl == f(o2, i)))
# Make outr, replacing the operators with f everywhere
s.add(outr == f(i, f(i, i)))
s.add(outl != outr)
# Print what is in the solver
print(‘Solver state: %s’ % s)
print(‘\n’)
if s.check() == sat:
# Print the model if something is wrong
print(‘Codes not equivalent, example trace:’)
print(s.model())
# Else everything is A OK!
37 38 39 40 41 42 43 44 45 46
1 2 3 4 5 6 7 8 9
10 11 12 13 14
print(‘Codes are equivalent’)
def main():
if __name__ == ‘__main__’:
Figure 15: First generic encoding in SMT
Solver state: [And(o1 == i, o2 == f(o1, i), outl == f(o2, i)),
outr == f(i, f(i, i)),
outl != outr]
Codes not equivalent, example trace:
[i = T!val!0,
outr = T!val!3,
outl = T!val!2,
o2 = T!val!1,
o1 = T!val!0,
f = [(T!val!1, T!val!0) -> T!val!2,
(T!val!0, T!val!1) -> T!val!3,
else -> T!val!1]]
Figure 16: Results for Listing 15
1. The encoding does not work
• The trace states the following: – Giveni=0,outl=2
– Giveni=0,outr=3
– The problem is the function f
– The function f defined by SMT in C++ is given in Listing 17
if (a == 1 && b == 0)
else if (a == 0 && b == 1)
else return 1;
Figure 17: SMT defined function f in C++ 2. What is incorrect about function f?
• It is not commutative.
– Returned values from cases if(a==0 && b==1) and (a==1 && b==0) should be the same!
– Note that +, *, etc are all commutative.
– Example:2*3==6==3*2,2+3==5==3+2. • We can enforce this property using the following logic:
template
T f (T a, T b) {
s = Solver()
– ∀x,y ∈ T,f(x,y) == f(y,x)
• The correct SMT encoding is shown in Listing 18
1 #!/usr/bin/env python3
2 from z3 import Solver, sat, And, Consts
general():
from z3 import Function, ForAll, DeclareSort
# Declaring the new type T
T = DeclareSort(‘T’)
# A new Type “T”
# Declaring the variables we need for type T
i, o1, o2, outl, outr = Consts(‘i o1 o2 outl outr’, T)
# Declaring the new function “f” of type signature: (T, T) -> T
f = Function(‘f’, T, T, T)
# Adding the commutativity constraint
x, y = Consts(‘x y’, T)
s.add(ForAll([x, y], f(x, y) == f(y, x)))
# Make outl, replacing the operator with f everywhere
s.add(And(o1 == i, o2 == f(o1, i), outl == f(o2, i)))
# Make outr, replacing the operators with f everywhere
s.add(outr == f(i, f(i, i)))
s.add(outl != outr)
# Print what is in the solver
print(‘Solver state: %s’ % s)
print(‘\n’)
if s.check() == sat:
# Print the model if something is wrong
print(‘Codes not equivalent, example trace:’)
print(s.model())
# Else everything is A OK!
print(‘Codes are equivalent’)
48 if __name__ == ‘__main__’:
Figure 18: Second and correct SMT generic functional equivalence encoding
1 Solver state: [ForAll([x, y], f(x, y) == f(y, x)),
2 And(o1 == i, o2 == f(o1, i), outl == f(o2, i)),
3 outr == f(i, f(i, i)),
4 outl != outr]
7 Codes are equivalent
Figure 19: Results for Listing 18
3. Hence, the functional and optimised code are equivalent for all commutative operators and of any type.
4.3.4 Relaxing the commutativity constraint
• Consider the program with matrices in python – in Listing 20 • Are the specification and implementation equivalent?
1 import numpy as np
np.array([[1, 2], [3, 4]]) a;
i in range(2):
Figure 20: Specification and (optimised) implementation, Example 3
9 # are they equal?
(a*a*a); 10 print(c == b)
1 [[ True True]
2 [ True True]]
Figure 21: Results for Listing 20 • However, matrix multiplication is not a commutative operator.
– A∗B̸=B∗A
• Hence, our previous proof does not apply to the matrix multiplication operator.
• So can we do better?
• What is the common property shared between addition, and multiplication for int and matrix?
– It is associativity, i.e., ∀x, y, z ∈ T, f(f(x, y), z) == f(x, f(y, z))
– We need to replace the commutativity constraint with the associativity constraint in the SMT en-
• Using associativity makes it more general.
• The proof applies to more operations of any type.
• The associative SMT encoding is given in Listing 22
1 #!/usr/bin/env python3
2 from z3 import Solver, sat, And, Consts
general():
from z3 import Function, ForAll, DeclareSort
# Declaring the new type T
T = DeclareSort(‘T’) # A new Type “T”
10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49
1 2 3 4 5 6 7
s = Solver()
# Declaring the variables we need for type T
i, o1, o2, outl, outr = Consts(‘i o1 o2 outl outr’, T)
# Declaring the new function “f” of type signature: (T, T) -> T
f = Function(‘f’, T, T, T)
# Adding the associativity constraint x,y,z=Consts(‘xyz’,T)
s.add(ForAll([x, y, z], f(f(x, y), z) == f(x, f(y, z))))
# Make outl, replacing the operator with f everywhere
s.add(And(o1 == i, o2 == f(o1, i), outl == f(o2, i)))
# Make outr, replacing the operators with f everywhere
s.add(outr == f(i, f(i, i)))
s.add(outl != outr)
# Print what is in the solver
print(‘Solver state: %s’ % s)
print(‘\n’)
if s.check() == sat:
# Print the model if something is wrong
print(‘Codes not equivalent, example trace:’)
print(s.model())
# Else everything is A OK!
print(‘Codes are equivalent’)
if __name__ == ‘__main__’:
Figure 22: SMT encoding of software program equivalence with associativity
Solver state: [ForAll([x, y, z], f(f(x, y), z) == f(x, f(y, z))),
And(o1 == i, o2 == f(o1, i), outl == f(o2, i)),
outr == f(i, f(i, i)),
outl != outr]
Codes are equivalent
Figure 23: Result of Listing 22
5 Modelling the task allocation problem
• In this section we solve an optimisation problem using SMT. • Consider Figure 24
P1 P2 … Pp ALU ALU ALU
Figure 24: The processor arch
程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com