Exercise Chapter 12 Practical Binary Analysis Z3

; Z3 script solver to do the next exercises
; 2. Proving Reachability
;   Use Z3 to figure out which of the calls to foo, bar, and baz are reachable
;   in the listing from the previous exercise. Model the relevant operations and branches
;   using bitvectors
; 3. Finding Opaque Predicates
;   Use Z3 to check whether any of the conditionals in the previous
;   listing are opaque predicates. If so, are they opaque true or false?
;   which code is unreachable and therefore safe to eliminate from the listing
;
; For the next code
;
;   x = int(argv[0])
;   y = int(argv[1])
;
;   z = x*x
;   w = y*y
;
;   if(z <= 1)
;       if( ((z + w) % 7 == 0) && (x % 7 != 0) )
;           foo(z, w
;
;   else
;       if((2**z - 1) % z != 0)
;           bar(x, y, z)
;
;       else
;           z = z + w
;           baz(z, y, x)
;
;   z = z*z
;   qux(x, y, z)


(declare-const x (_ BitVec 32))
(declare-const y (_ BitVec 32))
(declare-const z (_ BitVec 32))
(declare-const w (_ BitVec 32))
(assert (= z (bvmul x x)))
(assert (= w (bvmul y y)))

(push)
; Solver to call the function foo
(assert (bvsle z (_ bv1 32)))

(push)
(assert (and (= (bvsmod (bvadd z w) (_ bv7 32)) (_ bv0 32)) (not (= (bvsmod x (_ bv7 32)) (_ bv0 32)))))
(check-sat)
(get-model)
(pop)

(push)
; check if the sentence "if" after "if z <= 1" is opaque predicate
(assert (not (and (= (bvsmod (bvadd z w) (_ bv7 32)) (_ bv0 32)) (not (= (bvsmod x (_ bv7 32)) (_ bv0 32))))))
(check-sat)
(get-model)
(pop)

(pop)


(push)
(assert (bvsgt z (_ bv1 32)))

(push)
; Solver to call the function bar after else if
(assert (not (= (bvsmod (bvsub (ite (= z (_ bv0 32)) (_ bv1 32) (bvshl (_ bv2 32) z)) (_ bv1 32)) z) (_ bv0 32))))
(check-sat)
(get-model)
(pop)

(push)
; Solver to call the function baz after the else else
(assert (= (bvsmod (bvsub (ite (= z (_ bv0 32)) (_ bv1 32) (bvshl (_ bv2 32) z)) (_ bv1 32)) z) (_ bv0 32)))
(assert (= z (bvadd z w)))
(check-sat)
(get-model)
(pop)

(pop)