Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- ; 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)
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement