• API
• FAQ
• Tools
• Archive
SHARE
TWEET

Untitled

a guest Feb 16th, 2019 72 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
1. ;;
2. ;; Prove that
3. ;; (x -y) >> 3 != ((x >> 3)  - (y >> 3))
4. ;;
5. ;; if x >= y
6. ;;
7. ;;
8. (declare-fun x () (_ BitVec 32))
9. (declare-fun y () (_ BitVec 32))
10. (declare-fun shift () (_ BitVec 32))
11. (assert
12.   (=
13.     shift
14.     (_ bv3 32)
15.   )
16. )
17. (assert (bvuge x y))
18. (assert
19.   (not
20.     (=
21.       (bvlshr
22.         (bvsub x y)
23.         shift
24.       )
25.       (bvsub
26.         (bvlshr x shift)
27.         (bvlshr y shift)
28.       )
29.     )
30.   )
31. )
32. ;; Z3 responds SAT
33. ;; meaning that there is a counter example
34. ;; to our proposed equality.
35. (check-sat)
36. (get-model)
37. (exit)
38.
39. ;;
40. ;; Prove that
41. ;; (x -y) >> shift == ((x >> shift)  - (y >> shift))
42. ;;
43. ;; if x >= y and y is a multiple of (1 << shift).
44. ;;
46. ;; the equality hold.
47. ;;
48. (declare-fun x () (_ BitVec 32))
49. (declare-fun y () (_ BitVec 32))
50. (declare-fun shift () (_ BitVec 32))
51. (assert
52.   (=
53.     shift
54.     (_ bv3 32)
55.   )
56. )
57. (assert
58.   (=
59.     (_ bv0 32)
60.     (bvurem
61.       y
62.       (bvshl
63.         (_ bv1 32)
64.         shift
65.       )
66.     )
67.   )
68. )
69. (assert (bvuge x y))
70. (assert
71.   (not
72.     (=
73.       (bvlshr
74.         (bvsub x y)
75.         shift
76.       )
77.       (bvsub
78.         (bvlshr x shift)
79.         (bvlshr y shift)
80.       )
81.     )
82.   )
83. )
84. ;; Z3 responds UNSAT
85. ;; meaning that there isn't a counter example
86. ;; to our proposed equality.
87. (check-sat)
RAW Paste Data
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy.

Top