smt-libv2-bv-realization.gen 5.3 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18
(* Why3 driver checking compatibility of BV theories with SMT-LIB2 *)

theory bv.BV_Gen
  syntax function bw_and "(bvand %1 %2)"
  syntax function bw_or "(bvor %1 %2)"
  syntax function bw_xor "(bvxor %1 %2)"
  syntax function bw_not "(bvnot %1)"

  syntax function add "(bvadd %1 %2)"
  syntax function sub "(bvsub %1 %2)"
  syntax function neg "(bvneg %1)"
  syntax function mul "(bvmul %1 %2)"
  syntax function udiv "(bvudiv %1 %2)"
  syntax function urem "(bvurem %1 %2)"

  syntax function lsr_bv "(bvlshr %1 %2)"
  syntax function lsl_bv "(bvshl %1 %2)"
  syntax function asr_bv "(bvashr %1 %2)"
19
  syntax predicate (==) "(= %1 %2)"
20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35

  syntax predicate ult "(bvult %1 %2)"
  syntax predicate ule "(bvule %1 %2)"
  syntax predicate ugt "(bvugt %1 %2)"
  syntax predicate uge "(bvuge %1 %2)"
  syntax predicate slt "(bvslt %1 %2)"
  syntax predicate sle "(bvsle %1 %2)"
  syntax predicate sgt "(bvsgt %1 %2)"
  syntax predicate sge "(bvsge %1 %2)"

  (** Removing the axioms that should be proved instead
    the one that are commented out are instead kept
  *)

  remove prop size_pos
  remove prop nth_out_of_bound
36
  remove prop Nth_zeros
37 38 39 40 41 42 43
  remove prop Nth_ones
  remove prop Nth_bw_and
  remove prop Nth_bw_or
  remove prop Nth_bw_xor
  remove prop Nth_bw_not
  remove prop Lsr_nth_low
  remove prop Lsr_nth_high
44
  remove prop lsr_zeros
45 46
  remove prop Asr_nth_low
  remove prop Asr_nth_high
47
  remove prop asr_zeros
48 49
  remove prop Lsl_nth_high
  remove prop Lsl_nth_low
50
  remove prop lsl_zeros
51 52 53 54 55 56 57 58 59 60 61 62 63 64
  remove prop Nth_rotate_right
  remove prop Nth_rotate_left

(* Conversions from/to integers *)

  remove prop two_power_size_val
  remove prop max_int_val

  remove prop to_uint_extensionality
  remove prop to_int_extensionality

  remove prop to_uint_bounds
  remove prop to_uint_of_int

Clément Fumex's avatar
Clément Fumex committed
65 66 67 68
  remove prop to_uint_size_bv
  remove prop to_uint_zeros
  remove prop to_uint_ones
  remove prop to_uint_one
69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109

  (** Arithmetic operators *)

  remove prop to_uint_add
  remove prop to_uint_add_bounded

  remove prop to_uint_sub
  remove prop to_uint_sub_bounded

  remove prop to_uint_neg

  remove prop to_uint_mul
  remove prop to_uint_mul_bounded

  remove prop to_uint_udiv
  remove prop to_uint_urem

  (* kept: Nth_bv_is_nth *)
  (* kept: Nth_bv_is_nth2 *)
  (* kept: lsr_bv_is_lsr *)

  remove prop to_uint_lsr

  (* kept: asr_bv_is_asr *)
  (* kept: lsl_bv_is_lsl *)

  remove prop to_uint_lsl

  (* kept: rotate_left_bv_is_rotate_left *)
  (* kept: rotate_right_bv_is_rotate_right *)

  remove prop eq_sub_equiv
  remove prop Extensionality


end


theory bv.BV64
  syntax type t "(_ BitVec 64)"

110
  syntax function zeros "#x0000000000000000"
111 112 113 114 115 116 117 118 119 120 121 122 123 124 125
  syntax function ones "#xFFFFFFFFFFFFFFFF"

  syntax function nth_bv
    "(not (= (bvand (bvlshr %1 %2) (_ bv1 64)) (_ bv0 64)))"
(* possible alternative definition :
    "(= ((_ extract 0 0) (bvlshr %1 %2)) (_ bv1 1))"
*)

  syntax function rotate_left_bv "(bvor (bvshl %1 (bvurem %2 (_ bv64 64))) (bvlshr %1 (bvsub (_ bv64 64) (bvurem %2 (_ bv64 64)))))"
  syntax function rotate_right_bv "(bvor (bvlshr %1 (bvurem %2 (_ bv64 64))) (bvshl %1 (bvsub (_ bv64 64) (bvurem %2 (_ bv64 64)))))"
end

theory bv.BV32
  syntax type t "(_ BitVec 32)"

126
  syntax function zeros "#x00000000"
127 128 129 130 131 132 133 134 135 136 137 138
  syntax function ones "#xFFFFFFFF"

  syntax function nth_bv
    "(not (= (bvand (bvlshr %1 %2) (_ bv1 32)) (_ bv0 32)))"

  syntax function rotate_left_bv "(bvor (bvshl %1 (bvurem %2 (_ bv32 32))) (bvlshr %1 (bvsub (_ bv32 32) (bvurem %2 (_ bv32 32)))))"
  syntax function rotate_right_bv "(bvor (bvlshr %1 (bvurem %2 (_ bv32 32))) (bvshl %1 (bvsub (_ bv32 32) (bvurem %2 (_ bv32 32)))))"
end

theory bv.BV16
  syntax type t "(_ BitVec 16)"

139
  syntax function zeros "#x0000"
140 141 142 143 144 145 146 147 148 149 150 151
  syntax function ones "#xFFFF"

  syntax function nth_bv
    "(not (= (bvand (bvlshr %1 %2) (_ bv1 16)) (_ bv0 16)))"

  syntax function rotate_left_bv "(bvor (bvshl %1 (bvurem %2 (_ bv16 16))) (bvlshr %1 (bvsub (_ bv16 16) (bvurem %2 (_ bv16 16)))))"
  syntax function rotate_right_bv "(bvor (bvlshr %1 (bvurem %2 (_ bv16 16))) (bvshl %1 (bvsub (_ bv16 16) (bvurem %2 (_ bv16 16)))))"
end

theory bv.BV8
  syntax type t "(_ BitVec 8)"

152
  syntax function zeros "#x00"
153 154 155 156 157 158 159 160 161 162
  syntax function ones "#xFF"

  syntax function nth_bv
    "(not (= (bvand (bvlshr %1 %2) (_ bv1 8)) (_ bv0 8)))"

  syntax function rotate_left_bv "(bvor (bvshl %1 (bvurem %2 (_ bv8 8))) (bvlshr %1 (bvsub (_ bv8 8) (bvurem %2 (_ bv8 8)))))"
  syntax function rotate_right_bv "(bvor (bvlshr %1 (bvurem %2 (_ bv8 8))) (bvshl %1 (bvsub (_ bv8 8) (bvurem %2 (_ bv8 8)))))"
end

theory bv.BVConverter_Gen
163
  remove allprops
164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198
end

theory bv.BVConverter_32_64
  syntax function toBig "((_ zero_extend 32) %1)"
  syntax function toSmall "((_ extract 31 0) %1)"
end

theory bv.BVConverter_16_64
  syntax function toBig "((_ zero_extend 48) %1)"
  syntax function toSmall "((_ extract 15 0) %1)"
end

theory bv.BVConverter_8_64
  syntax function toBig "((_ zero_extend 56) %1)"
  syntax function toSmall "((_ extract 7 0) %1)"
end

theory bv.BVConverter_16_32
  syntax function toBig "((_ zero_extend 16) %1)"
  syntax function toSmall "((_ extract 15 0) %1)"
end

theory bv.BVConverter_8_32
  syntax function toBig "((_ zero_extend 24) %1)"
  syntax function toSmall "((_ extract 7 0) %1)"
end

theory bv.BVConverter_8_16
  syntax function toBig "((_ zero_extend 8) %1)"
  syntax function toSmall "((_ extract 7 0) %1)"
end

theory bv.Pow2int
  remove allprops
end