drivers/smt-libv2-bv.gen

   1 (* Why3 driver for SMT-LIB2, common part of bit-vector theories *)
   2
   3 prelude ";;; SMT-LIB2 driver: bit-vectors, common part"
   4
   5 theory bv.BV_Gen
   6   remove prop size_pos
   7   remove prop nth_out_of_bound
   8   remove prop Nth_zeros
   9   remove prop Nth_ones
  10
  11   (** this meta seems somehow placed too early since we cannot give a
  12      syntax rule for the literals yet, it is only possible in the
  13      clones. Yet, this will prevent users who clone this module to
  14      forget to add such a syntax rule in their driver. See also issue
  15      https://gitlab.inria.fr/why3/why3/-/issues/759 *)
  16   meta "literal:keep" type t
  17
  18   (* Note: the syntax rules given in this module are somehow given too
  19      early, since they are only valid in each clones. Yet, it is
  20      convenient to share those declarations once and for all. See also issue
  21      https://gitlab.inria.fr/why3/why3/-/issues/759 *)
  22
  23   syntax function bw_and "(bvand %1 %2)"
  24   syntax function bw_or "(bvor %1 %2)"
  25   syntax function bw_xor "(bvxor %1 %2)"
  26   syntax function bw_not "(bvnot %1)"
  27
  28   (* Warning: we should NOT remove all the axioms using "allprops" *)
  29
  30   remove prop Nth_bw_and
  31   remove prop Nth_bw_or
  32   remove prop Nth_bw_xor
  33   remove prop Nth_bw_not
  34
  35   (** Shift operators *)
  36
  37   remove prop Lsr_nth_low
  38   remove prop Lsr_nth_high
  39   remove prop lsr_zeros
  40   remove prop Asr_nth_low
  41   remove prop Asr_nth_high
  42   remove prop asr_zeros
  43   remove prop Lsl_nth_low
  44   remove prop Lsl_nth_high
  45   remove prop lsl_zeros
  46   remove prop Nth_rotate_left
  47   remove prop Nth_rotate_right
  48
  49   (* Conversions from/to integers *)
  50
  51   remove prop two_power_size_val
  52   remove prop max_int_val
  53
  54   (* function to_int  - solver specific *)
  55   (* function to_uint - solver specific *)
  56   (* function of_int  - solver specific *)
  57
  58   remove prop to_uint_extensionality
  59   remove prop to_int_extensionality
  60
  61   remove prop to_uint_bounds
  62   (*remove prop to_uint_of_int*)
  63   remove prop to_uint_size_bv
  64   remove prop to_uint_zeros
  65   remove prop to_uint_ones
  66   remove prop to_uint_one
  67
  68   (* comparison operators *)
  69
  70   syntax predicate ult "(bvult %1 %2)"
  71   syntax predicate ule "(bvule %1 %2)"
  72   syntax predicate ugt "(bvugt %1 %2)"
  73   syntax predicate uge "(bvuge %1 %2)"
  74   syntax predicate slt "(bvslt %1 %2)"
  75   syntax predicate sle "(bvsle %1 %2)"
  76   syntax predicate sgt "(bvsgt %1 %2)"
  77   syntax predicate sge "(bvsge %1 %2)"
  78
  79   (** Arithmetic operators *)
  80
  81   syntax function add "(bvadd %1 %2)"
  82   remove prop to_uint_add
  83   remove prop to_uint_add_bounded
  84   remove prop to_uint_add_overflow
  85
  86   syntax function sub "(bvsub %1 %2)"
  87   remove prop to_uint_sub
  88   remove prop to_uint_sub_bounded
  89   remove prop to_uint_sub_overflow
  90
  91   syntax function neg "(bvneg %1)"
  92   remove prop to_uint_neg
  93   remove prop to_uint_neg_no_mod
  94
  95   syntax function mul "(bvmul %1 %2)"
  96   remove prop to_uint_mul
  97   remove prop to_uint_mul_bounded
  98
  99   syntax function udiv "(bvudiv %1 %2)"
 100   remove prop to_uint_udiv
 101
 102   syntax function urem "(bvurem %1 %2)"
 103   remove prop to_uint_urem
 104
 105   syntax function sdiv "(bvsdiv %1 %2)"
 106   (*remove prop to_int_sdiv*)
 107
 108   syntax function srem "(bvsrem %1 %2)"
 109   (*remove prop to_int_srem*)
 110
 111   (** Bitvector alternatives for shifts, rotations and nth *)
 112
 113   syntax function lsr_bv "(bvlshr %1 %2)"
 114   (* remove prop lsr_bv_is_lsr *)
 115   remove prop to_uint_lsr
 116
 117   syntax function asr_bv "(bvashr %1 %2)"
 118   (* remove prop asr_bv_is_asr *)
 119
 120   syntax function lsl_bv "(bvshl %1 %2)"
 121   (* remove prop lsl_bv_is_lsl *)
 122
 123   remove prop to_uint_lsl
 124
 125   (** rotations *)
 126   (* remove prop rotate_left_bv_is_rotate_left *)
 127   (* remove prop rotate_right_bv_is_rotate_right *)
 128
 129   (** nth_bv *)
 130
 131   (* remove prop nth_bv_def *)
 132   (* remove prop Nth_bv_is_nth *)
 133   (* remove prop Nth_bv_is_nth2 *)
 134
 135   remove prop Extensionality
 136 end
 137
 138 theory bv.BV256
 139
 140   syntax literal t "#x%64x"
 141   syntax type t "(_ BitVec 256)"
 142
 143   syntax function zeros "#x0000000000000000000000000000000000000000000000000000000000000000"
 144   syntax function one   "#x0000000000000000000000000000000000000000000000000000000000000001"
 145   syntax function ones  "#xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF"
 146   syntax function size_bv "(_ bv256 256)"
 147
 148   syntax predicate is_signed_positive "(bvsge %1 (_ bv0 256))"
 149
 150   syntax function rotate_left_bv "(bvor (bvshl %1 (bvurem %2 (_ bv256 256))) (bvlshr %1 (bvsub (_ bv256 256) (bvurem %2 (_ bv256 256)))))"
 151   syntax function rotate_right_bv "(bvor (bvlshr %1 (bvurem %2 (_ bv256 256))) (bvshl %1 (bvsub (_ bv256 256) (bvurem %2 (_ bv256 256)))))"
 152 end
 153
 154 theory bv.BV128
 155
 156   syntax literal t "#x%32x"
 157   syntax type t "(_ BitVec 128)"
 158
 159   syntax function zeros "#x00000000000000000000000000000000"
 160   syntax function one   "#x00000000000000000000000000000001"
 161   syntax function ones  "#xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF"
 162   syntax function size_bv "(_ bv128 128)"
 163
 164   syntax predicate is_signed_positive "(bvsge %1 (_ bv0 128))"
 165
 166   syntax function rotate_left_bv "(bvor (bvshl %1 (bvurem %2 (_ bv128 128))) (bvlshr %1 (bvsub (_ bv128 128) (bvurem %2 (_ bv128 128)))))"
 167   syntax function rotate_right_bv "(bvor (bvlshr %1 (bvurem %2 (_ bv128 128))) (bvshl %1 (bvsub (_ bv128 128) (bvurem %2 (_ bv128 128)))))"
 168 end
 169
 170 theory bv.BV64
 171
 172   syntax literal t "#x%16x"
 173   syntax type t "(_ BitVec 64)"
 174
 175   syntax function zeros "#x0000000000000000"
 176   syntax function one   "#x0000000000000001"
 177   syntax function ones  "#xFFFFFFFFFFFFFFFF"
 178   syntax function size_bv "(_ bv64 64)"
 179
 180   syntax predicate is_signed_positive "(bvsge %1 (_ bv0 64))"
 181
 182   syntax function rotate_left_bv "(bvor (bvshl %1 (bvurem %2 (_ bv64 64))) (bvlshr %1 (bvsub (_ bv64 64) (bvurem %2 (_ bv64 64)))))"
 183   syntax function rotate_right_bv "(bvor (bvlshr %1 (bvurem %2 (_ bv64 64))) (bvshl %1 (bvsub (_ bv64 64) (bvurem %2 (_ bv64 64)))))"
 184 end
 185
 186 theory bv.BV32
 187
 188   syntax literal t "#x%8x"
 189   syntax type t "(_ BitVec 32)"
 190
 191   syntax function zeros "#x00000000"
 192   syntax function one   "#x00000001"
 193   syntax function ones  "#xFFFFFFFF"
 194   syntax function size_bv "(_ bv32 32)"
 195
 196   syntax predicate is_signed_positive "(bvsge %1 (_ bv0 32))"
 197
 198   syntax function rotate_left_bv "(bvor (bvshl %1 (bvurem %2 (_ bv32 32))) (bvlshr %1 (bvsub (_ bv32 32) (bvurem %2 (_ bv32 32)))))"
 199   syntax function rotate_right_bv "(bvor (bvlshr %1 (bvurem %2 (_ bv32 32))) (bvshl %1 (bvsub (_ bv32 32) (bvurem %2 (_ bv32 32)))))"
 200 end
 201
 202 theory bv.BV16
 203
 204   syntax literal t "#x%4x"
 205   syntax type t "(_ BitVec 16)"
 206
 207   syntax function zeros "#x0000"
 208   syntax function one   "#x0001"
 209   syntax function ones  "#xFFFF"
 210   syntax function size_bv "(_ bv16 16)"
 211
 212   syntax predicate is_signed_positive "(bvsge %1 (_ bv0 16))"
 213
 214   syntax function rotate_left_bv "(bvor (bvshl %1 (bvurem %2 (_ bv16 16))) (bvlshr %1 (bvsub (_ bv16 16) (bvurem %2 (_ bv16 16)))))"
 215   syntax function rotate_right_bv "(bvor (bvlshr %1 (bvurem %2 (_ bv16 16))) (bvshl %1 (bvsub (_ bv16 16) (bvurem %2 (_ bv16 16)))))"
 216 end
 217
 218 theory bv.BV8
 219
 220   syntax literal t (* "#b%8b"  *) "#x%2x"
 221   syntax type t "(_ BitVec 8)"
 222
 223   syntax function zeros "#x00"
 224   syntax function one   "#x01"
 225   syntax function ones  "#xFF"
 226   syntax function size_bv "(_ bv8 8)"
 227
 228   syntax predicate is_signed_positive "(bvsge %1 (_ bv0 8))"
 229
 230   syntax function rotate_left_bv "(bvor (bvshl %1 (bvurem %2 (_ bv8 8))) (bvlshr %1 (bvsub (_ bv8 8) (bvurem %2 (_ bv8 8)))))"
 231   syntax function rotate_right_bv "(bvor (bvlshr %1 (bvurem %2 (_ bv8 8))) (bvshl %1 (bvsub (_ bv8 8) (bvurem %2 (_ bv8 8)))))"
 232 end
 233
 234 theory bv.BVConverter_Gen
 235   remove allprops
 236 end
 237
 238 theory bv.BVConverter_128_256
 239   syntax function toBig "((_ zero_extend 128) %1)"
 240   syntax function stoBig "((_ sign_extend 128) %1)"
 241   syntax function toSmall "((_ extract 127 0) %1)"
 242 end
 243
 244 theory bv.BVConverter_64_128
 245   syntax function toBig "((_ zero_extend 64) %1)"
 246   syntax function stoBig "((_ sign_extend 64) %1)"
 247   syntax function toSmall "((_ extract 63 0) %1)"
 248 end
 249
 250 theory bv.BVConverter_32_128
 251   syntax function toBig "((_ zero_extend 96) %1)"
 252   syntax function stoBig "((_ sign_extend 96) %1)"
 253   syntax function toSmall "((_ extract 31 0) %1)"
 254 end
 255
 256 theory bv.BVConverter_16_128
 257   syntax function toBig "((_ zero_extend 112) %1)"
 258   syntax function stoBig "((_ sign_extend 112) %1)"
 259   syntax function toSmall "((_ extract 15 0) %1)"
 260 end
 261
 262 theory bv.BVConverter_8_128
 263   syntax function toBig "((_ zero_extend 120) %1)"
 264   syntax function stoBig "((_ sign_extend 120) %1)"
 265   syntax function toSmall "((_ extract 7 0) %1)"
 266 end
 267
 268 theory bv.BVConverter_32_64
 269   syntax function toBig "((_ zero_extend 32) %1)"
 270   syntax function stoBig "((_ sign_extend 32) %1)"
 271   syntax function toSmall "((_ extract 31 0) %1)"
 272 end
 273
 274 theory bv.BVConverter_16_64
 275   syntax function toBig "((_ zero_extend 48) %1)"
 276   syntax function stoBig "((_ sign_extend 48) %1)"
 277   syntax function toSmall "((_ extract 15 0) %1)"
 278 end
 279
 280 theory bv.BVConverter_8_64
 281   syntax function toBig "((_ zero_extend 56) %1)"
 282   syntax function stoBig "((_ sign_extend 56) %1)"
 283   syntax function toSmall "((_ extract 7 0) %1)"
 284 end
 285
 286 theory bv.BVConverter_16_32
 287   syntax function toBig "((_ zero_extend 16) %1)"
 288   syntax function stoBig "((_ sign_extend 16) %1)"
 289   syntax function toSmall "((_ extract 15 0) %1)"
 290 end
 291
 292 theory bv.BVConverter_8_32
 293   syntax function toBig "((_ zero_extend 24) %1)"
 294   syntax function stoBig "((_ sign_extend 24) %1)"
 295   syntax function toSmall "((_ extract 7 0) %1)"
 296 end
 297
 298 theory bv.BVConverter_8_16
 299   syntax function toBig "((_ zero_extend 8) %1)"
 300   syntax function stoBig "((_ sign_extend 8) %1)"
 301   syntax function toSmall "((_ extract 7 0) %1)"
 302 end
 303
 304 theory bv.Pow2int
 305   remove allprops
 306 end