daily pastebin goal
39%
SHARE
TWEET

Untitled

a guest Feb 16th, 2019 71 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. ;;
  45. ;; By adding the additional constraint on `y` it makes
  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. OK, I Understand
 
Top