mirror of
https://github.com/Z3Prover/z3
synced 2025-10-31 19:52:29 +00:00
three smt2 examples added and one python example updated (#5690)
This commit is contained in:
Matteo Nicoli
GitHub
parent
71cbb160d2
commit
cbdd7b0696
4 changed files with 445 additions and 23 deletions
168
examples/SMT-LIB2/bounded model checking/bubble_sort.smt2
Normal file
168
examples/SMT-LIB2/bounded model checking/bubble_sort.smt2
Normal file
|
|
@ -0,0 +1,168 @@
|
|||
; File name: bubble_sort.smt2
|
||||
;
|
||||
; BUBBLESORT - Copyright (c) March, 2021 - Matteo Nicoli
|
||||
;
|
||||
; An example of bounded model checking of the classic bubble sort algorithm.
|
||||
; we will copy the array values into a list in order to check whether the
|
||||
; array is ordered or not. That's because:
|
||||
; - it's easier to walk recursively through a list
|
||||
; - it gives an example of how list and sequences work in Z3
|
||||
;
|
||||
|
||||
|
||||
; size of the array
|
||||
(declare-const dim Int)
|
||||
|
||||
; arrays declaration
|
||||
(declare-const A0 (Array Int Int))
|
||||
(declare-const A1 (Array Int Int))
|
||||
(declare-const A2 (Array Int Int))
|
||||
(declare-const A3 (Array Int Int))
|
||||
|
||||
; indexes declaration
|
||||
(declare-const i0 Int)
|
||||
(declare-const i1 Int)
|
||||
(declare-const i2 Int)
|
||||
(declare-const i3 Int)
|
||||
|
||||
(declare-const j0 Int)
|
||||
(declare-const j1 Int)
|
||||
(declare-const j2 Int)
|
||||
(declare-const j3 Int)
|
||||
|
||||
(declare-const tmp0 Int)
|
||||
(declare-const tmp1 Int)
|
||||
(declare-const tmp2 Int)
|
||||
|
||||
; lists declaration (for post condition)
|
||||
(declare-const l0 (List Int))
|
||||
(declare-const l1 (List Int))
|
||||
(declare-const l2 (List Int))
|
||||
(declare-const l3 (List Int))
|
||||
(declare-const l4 (List Int))
|
||||
|
||||
(define-fun init_indexes ((_i Int) (_j Int)) Bool
|
||||
(and
|
||||
(= _i 0)
|
||||
(= _j 0)
|
||||
)
|
||||
)
|
||||
|
||||
(define-fun inner_loop
|
||||
(
|
||||
(_A0 (Array Int Int))
|
||||
(_A1 (Array Int Int))
|
||||
(tmp Int)
|
||||
(_i0 Int)
|
||||
(_dim Int)
|
||||
) Bool
|
||||
(ite
|
||||
(> (select _A0 _i0) (select _A0 (+ _i0 1)))
|
||||
(and
|
||||
(= tmp (select _A0 _i0))
|
||||
(= _A1 (store _A0 _i0 (select _A0 (+ _i0 1))))
|
||||
(= _A1 (store _A0 (+ _i0 1) tmp))
|
||||
)
|
||||
(= _A1 _A0)
|
||||
)
|
||||
)
|
||||
|
||||
; the body of the bubblesort algorithm
|
||||
(define-fun bsort_step
|
||||
(
|
||||
(_A0 (Array Int Int))
|
||||
(_A1 (Array Int Int))
|
||||
(tmp Int)
|
||||
(_i0 Int)
|
||||
(_j0 Int)
|
||||
(_i1 Int)
|
||||
(_j1 Int)
|
||||
(_dim Int)
|
||||
) Bool
|
||||
(ite
|
||||
(< _j0 (- _dim 1))
|
||||
(and
|
||||
(ite
|
||||
(< _i0 (- _dim 1))
|
||||
(and
|
||||
(inner_loop _A0 _A1 tmp _i0 _dim)
|
||||
(= _i1 (+ _i0 1))
|
||||
)
|
||||
(= _j1 (+ _j0 1))
|
||||
)
|
||||
(= _j1 (+ _j0 1))
|
||||
)
|
||||
(and
|
||||
(= _j1 (+ _j0 1))
|
||||
(= _A1 _A0)
|
||||
)
|
||||
)
|
||||
)
|
||||
|
||||
; the function by which we check whether the list is ordered
|
||||
(define-fun-rec check ((_l (List Int))) Bool
|
||||
(ite
|
||||
(= _l nil)
|
||||
true
|
||||
(ite
|
||||
(not (= (tail _l) nil))
|
||||
(and
|
||||
(>= (head _l) (head (tail _l)))
|
||||
(check (tail _l))
|
||||
)
|
||||
true
|
||||
)
|
||||
)
|
||||
)
|
||||
|
||||
; sets the size of the array
|
||||
(assert (= dim 4))
|
||||
|
||||
; initialization of the counters
|
||||
(assert (init_indexes i0 j0))
|
||||
|
||||
; the first step of the sorting algorithm
|
||||
(assert (bsort_step A0 A1 tmp0 i0 j0 i1 j1 dim))
|
||||
(assert (bsort_step A1 A2 tmp1 i1 j1 i2 j2 dim))
|
||||
(assert (bsort_step A2 A3 tmp2 i2 j2 i3 j3 dim))
|
||||
|
||||
; filling the list for test
|
||||
(assert
|
||||
(and
|
||||
(= l0 nil)
|
||||
(= l1 (insert (select A3 0) l0))
|
||||
(= l2 (insert (select A3 1) l1))
|
||||
(= l3 (insert (select A3 2) l2))
|
||||
(= l4 (insert (select A3 3) l3))
|
||||
)
|
||||
)
|
||||
|
||||
(echo "BUBBLE SORT")
|
||||
|
||||
(push)
|
||||
|
||||
; (negated) post-condition
|
||||
(assert (not (check l4)))
|
||||
|
||||
(echo "Testing the validity of the algorithm; `unsat` expected: ")
|
||||
|
||||
; `unsat` expected
|
||||
(check-sat)
|
||||
|
||||
(echo "---------------------")
|
||||
|
||||
(pop)
|
||||
|
||||
; post-condition
|
||||
(assert (check l4))
|
||||
|
||||
(echo "Getting a model; `sat` expected: ")
|
||||
|
||||
; `sat` expected
|
||||
(check-sat)
|
||||
|
||||
(echo "---------------------")
|
||||
|
||||
(echo "Model: ")
|
||||
(get-value (A3))
|
||||
(exit)
|
||||
114
examples/SMT-LIB2/bounded model checking/loop_unrolling.smt2
Normal file
114
examples/SMT-LIB2/bounded model checking/loop_unrolling.smt2
Normal file
|
|
@ -0,0 +1,114 @@
|
|||
; File name: loop_unrolling.smt2
|
||||
;
|
||||
; Copyright (c) March, 2021 - Matteo Nicoli
|
||||
;
|
||||
;
|
||||
; Let's start considering a simple C program involving an iteration:
|
||||
;
|
||||
; #define DIM 2
|
||||
;
|
||||
; /* uninterpreted functions */
|
||||
; long get_number();
|
||||
; void fill_array(long *A);
|
||||
;
|
||||
; int main()
|
||||
; {
|
||||
; long x = get_number();
|
||||
; long A[DIM];
|
||||
; long i = 0;
|
||||
; long found = 0;
|
||||
;
|
||||
; fill_array(A);
|
||||
;
|
||||
; while(i < DIM) {
|
||||
; if(x == A[i])
|
||||
; found = 1;
|
||||
; i++;
|
||||
; }
|
||||
; }
|
||||
;
|
||||
; Below, we can see its SSA representation in SMT-LIB2.
|
||||
; Our goal is to verify that, at the end of the program, the variable `found`
|
||||
; is equal to 1 if, and only if, `x` is an element of the array.
|
||||
|
||||
|
||||
(declare-const x Int)
|
||||
(declare-const A (Array Int Int))
|
||||
(declare-const i_0 Int)
|
||||
(declare-const found_0 Int)
|
||||
|
||||
(declare-const found_1 Int)
|
||||
(declare-const found_2 Int)
|
||||
(declare-const i_1 Int)
|
||||
(declare-const i_2 Int)
|
||||
|
||||
; Pre-condition: variables initialization
|
||||
(assert
|
||||
(and
|
||||
(= i_0 0)
|
||||
(= found_0 0)
|
||||
)
|
||||
)
|
||||
|
||||
; Transition funcion
|
||||
(define-fun body ((f_0 Int) (f Int) (i_0 Int) (i_1 Int)(_A (Array Int Int)) (_x Int)) Bool
|
||||
(and
|
||||
(= f (ite (= _x (select _A i_0)) 1 f_0))
|
||||
(= i_1 (+ i_0 1))
|
||||
)
|
||||
)
|
||||
|
||||
; Post-condition function
|
||||
(define-fun post ((_f Int) (_i Int) (_x Int) (_A (Array Int Int))) Bool
|
||||
(=
|
||||
(= _f 1)
|
||||
(= _x (select _A _i))
|
||||
)
|
||||
)
|
||||
|
||||
; Transition function is called DIM times:
|
||||
; for practical reasons, we are considering here DIM = 2
|
||||
(assert (body found_0 found_1 i_0 i_1 A x))
|
||||
(assert (body found_1 found_2 i_1 i_2 A x))
|
||||
|
||||
(push)
|
||||
|
||||
(echo "Bounded model checking with loop unrolling")
|
||||
|
||||
(echo "------------------------------------------")
|
||||
|
||||
; Post-condition (negated) is called DIM times
|
||||
(assert
|
||||
(not
|
||||
(or
|
||||
(post found_2 i_0 x A)
|
||||
(post found_2 i_1 x A)
|
||||
)
|
||||
)
|
||||
)
|
||||
|
||||
(echo "Testing the validity of the post-condition: `unsat expected`")
|
||||
|
||||
; `unsat` expected
|
||||
(check-sat)
|
||||
|
||||
(pop)
|
||||
|
||||
; Post-condition (called DIM times)
|
||||
(assert
|
||||
(or
|
||||
(post found_2 i_0 x A)
|
||||
(post found_2 i_1 x A)
|
||||
)
|
||||
)
|
||||
|
||||
(echo "Getting a model; `sat` expected: ")
|
||||
|
||||
; `sat` expected
|
||||
(check-sat)
|
||||
|
||||
(echo "------------------------------------------")
|
||||
|
||||
(echo "Model: ")
|
||||
(get-value (x A found_2))
|
||||
(exit)
|
||||
|
|
@ -0,0 +1,116 @@
|
|||
; File name: loop_unrolling_bitvec.smt2
|
||||
;
|
||||
; Copyright (c) March, 2021 - Matteo Nicoli
|
||||
;
|
||||
;
|
||||
; Let's start considering a simple C program involving an iteration:
|
||||
;
|
||||
; #define DIM 2
|
||||
;
|
||||
; /* uninterpreted functions */
|
||||
; long get_number();
|
||||
; void fill_array(long *A);
|
||||
;
|
||||
; int main()
|
||||
; {
|
||||
; long x = get_number();
|
||||
; long A[DIM];
|
||||
; long i = 0;
|
||||
; long found = 0;
|
||||
;
|
||||
; fill_array(A);
|
||||
;
|
||||
; while(i < DIM) {
|
||||
; if(x == A[i])
|
||||
; found = 1;
|
||||
; i++;
|
||||
; }
|
||||
; }
|
||||
;
|
||||
; Below, we can see its SSA representation in SMT-LIB2.
|
||||
; Our goal is to verify that, at the end of the program, the variable `found`
|
||||
; is equal to 1 if, and only if, `x` is an element of the array.
|
||||
; We define our custom sort `IntValue` that represents a 32-bit integer value.
|
||||
|
||||
|
||||
(define-sort IntValue () (_ BitVec 32))
|
||||
(declare-const x IntValue)
|
||||
(declare-const A (Array IntValue IntValue))
|
||||
(declare-const i_0 IntValue)
|
||||
(declare-const found_0 IntValue)
|
||||
|
||||
(declare-const found_1 IntValue)
|
||||
(declare-const found_2 IntValue)
|
||||
(declare-const i_1 IntValue)
|
||||
(declare-const i_2 IntValue)
|
||||
|
||||
; Pre-condition: variables initialization
|
||||
(assert
|
||||
(and
|
||||
(= i_0 #x00000000)
|
||||
(= found_0 #x00000000)
|
||||
)
|
||||
)
|
||||
|
||||
; Transition funcion
|
||||
(define-fun body ((f_0 IntValue) (f IntValue) (i_0 IntValue) (i_1 IntValue)(_A (Array IntValue IntValue)) (_x IntValue)) Bool
|
||||
(and
|
||||
(= f (ite (= _x (select _A i_0)) #x00000001 f_0))
|
||||
(= i_1 (bvadd i_0 #x00000001))
|
||||
)
|
||||
)
|
||||
|
||||
; Post-condition function
|
||||
(define-fun post ((_f IntValue) (_i IntValue) (_x IntValue) (_A (Array IntValue IntValue))) Bool
|
||||
(=
|
||||
(= _f #x00000001)
|
||||
(= _x (select _A _i))
|
||||
)
|
||||
)
|
||||
|
||||
; Transition function is called DIM times:
|
||||
; for practical reasons, we are considering here DIM = 2
|
||||
(assert (body found_0 found_1 i_0 i_1 A x))
|
||||
(assert (body found_1 found_2 i_1 i_2 A x))
|
||||
|
||||
(push)
|
||||
|
||||
(echo "Bounded model checking with loop unrolling")
|
||||
|
||||
(echo "------------------------------------------")
|
||||
|
||||
; Post-condition (negated) is called DIM times
|
||||
(assert
|
||||
(not
|
||||
(or
|
||||
(post found_2 i_0 x A)
|
||||
(post found_2 i_1 x A)
|
||||
)
|
||||
)
|
||||
)
|
||||
|
||||
(echo "Testing the validity of the post-condition: `unsat expected`")
|
||||
|
||||
; `unsat` expected
|
||||
(check-sat)
|
||||
|
||||
(pop)
|
||||
|
||||
; Post-condition (called DIM times)
|
||||
(assert
|
||||
(or
|
||||
(post found_2 i_0 x A)
|
||||
(post found_2 i_1 x A)
|
||||
)
|
||||
)
|
||||
|
||||
(echo "Getting a model; `sat` expected: ")
|
||||
|
||||
; `sat` expected
|
||||
(check-sat)
|
||||
|
||||
(echo "------------------------------------------")
|
||||
|
||||
(echo "Model: ")
|
||||
(get-value (x A found_2))
|
||||
(exit)
|
||||
|
|
@ -1,3 +1,5 @@
|
|||
# File name: bubble_sort.py
|
||||
#
|
||||
# BUBBLESORT - Copyright (c) June, 2020 - Matteo Nicoli
|
||||
|
||||
from z3 import Solver, Int, Array, IntSort, And, Not, If, Select, Store, sat
|
||||
|
|
@ -36,11 +38,11 @@ def check(variables, Ar, dim) :
|
|||
yield variables[e] == Select(Ar,e)
|
||||
|
||||
def mk_post_condition(values) :
|
||||
condition = []
|
||||
for v1,v2 in zip(values,values[1:]) :
|
||||
condition.append(v1 <= v2)
|
||||
condition = [v1 <= v2 for v1,v2 in zip(values,values[1:])]
|
||||
return And(*condition)
|
||||
|
||||
|
||||
def main() :
|
||||
dim = int(input("size of the array: "))
|
||||
|
||||
i = [Int(f"i_{x}") for x in range(dim + 1)]
|
||||
|
|
@ -61,9 +63,31 @@ init_check_condition = check(values,A[-1],dim)
|
|||
s.add(And(*init_check_condition))
|
||||
|
||||
post_condition = mk_post_condition(values)
|
||||
|
||||
print("Bubble sort")
|
||||
print("---------------------")
|
||||
|
||||
s.push()
|
||||
s.add(Not(post_condition))
|
||||
|
||||
print("Testing the validity of the algorithm; `valid expected`:")
|
||||
|
||||
if s.check() == sat :
|
||||
print(f"counterexample:\n{s.model()}")
|
||||
else :
|
||||
print("valid")
|
||||
|
||||
print("---------------------")
|
||||
|
||||
s.pop()
|
||||
|
||||
s.add(post_condition)
|
||||
print("Getting a model...")
|
||||
print("Model:")
|
||||
|
||||
if s.check() == sat :
|
||||
print(s.model())
|
||||
|
||||
|
||||
if __name__ == "__main__" :
|
||||
main()
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue