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 two_power_size_minus_one_val
  53   remove prop max_int_val
  54
  55   (* function to_int  - solver specific *)
  56   (* function to_uint - solver specific *)
  57   (* function of_int  - solver specific *)
  58
  59   remove prop to_uint_extensionality
  60   remove prop to_int_extensionality
  61
  62   remove prop to_uint_bounds
  63   (*remove prop to_uint_of_int*)
  64   remove prop to_uint_size_bv
  65   remove prop to_uint_zeros
  66   remove prop to_uint_ones
  67   remove prop to_uint_one
  68
  69   (* comparison operators *)
  70
  71   syntax predicate ult "(bvult %1 %2)"
  72   syntax predicate ule "(bvule %1 %2)"
  73   syntax predicate ugt "(bvugt %1 %2)"
  74   syntax predicate uge "(bvuge %1 %2)"
  75   syntax predicate slt "(bvslt %1 %2)"
  76   syntax predicate sle "(bvsle %1 %2)"
  77   syntax predicate sgt "(bvsgt %1 %2)"
  78   syntax predicate sge "(bvsge %1 %2)"
  79
  80   (** Arithmetic operators *)
  81
  82   syntax function add "(bvadd %1 %2)"
  83   remove prop to_uint_add
  84   remove prop to_uint_add_bounded
  85   remove prop to_uint_add_overflow
  86
  87   syntax function sub "(bvsub %1 %2)"
  88   remove prop to_uint_sub
  89   remove prop to_uint_sub_bounded
  90   remove prop to_uint_sub_overflow
  91
  92   syntax function neg "(bvneg %1)"
  93   remove prop to_uint_neg
  94   remove prop to_uint_neg_no_mod
  95
  96   syntax function mul "(bvmul %1 %2)"
  97   remove prop to_uint_mul
  98   remove prop to_uint_mul_bounded
  99
 100   syntax function udiv "(bvudiv %1 %2)"
 101   remove prop to_uint_udiv
 102
 103   syntax function urem "(bvurem %1 %2)"
 104   remove prop to_uint_urem
 105
 106   syntax function sdiv "(bvsdiv %1 %2)"
 107   (*remove prop to_int_sdiv*)
 108
 109   syntax function srem "(bvsrem %1 %2)"
 110   (*remove prop to_int_srem*)
 111
 112   (** Bitvector alternatives for shifts, rotations and nth *)
 113
 114   syntax function lsr_bv "(bvlshr %1 %2)"
 115   (* remove prop lsr_bv_is_lsr *)
 116   remove prop to_uint_lsr
 117
 118   syntax function asr_bv "(bvashr %1 %2)"
 119   (* remove prop asr_bv_is_asr *)
 120
 121   syntax function lsl_bv "(bvshl %1 %2)"
 122   (* remove prop lsl_bv_is_lsl *)
 123
 124   remove prop to_uint_lsl
 125
 126   (** rotations *)
 127   (* remove prop rotate_left_bv_is_rotate_left *)
 128   (* remove prop rotate_right_bv_is_rotate_right *)
 129
 130   (** nth_bv *)
 131
 132   (* remove prop nth_bv_def *)
 133   (* remove prop Nth_bv_is_nth *)
 134   (* remove prop Nth_bv_is_nth2 *)
 135
 136   remove prop Extensionality
 137 end
 138
 139 theory bv.BV256
 140
 141   syntax literal t "#x%64x"
 142   syntax type t "(_ BitVec 256)"
 143
 144   syntax function zeros "#x0000000000000000000000000000000000000000000000000000000000000000"
 145   syntax function one   "#x0000000000000000000000000000000000000000000000000000000000000001"
 146   syntax function ones  "#xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF"
 147   syntax function size_bv "(_ bv256 256)"
 148
 149   syntax predicate is_signed_positive "(bvsge %1 (_ bv0 256))"
 150
 151   syntax function rotate_left_bv "(bvor (bvshl %1 (bvurem %2 (_ bv256 256))) (bvlshr %1 (bvsub (_ bv256 256) (bvurem %2 (_ bv256 256)))))"
 152   syntax function rotate_right_bv "(bvor (bvlshr %1 (bvurem %2 (_ bv256 256))) (bvshl %1 (bvsub (_ bv256 256) (bvurem %2 (_ bv256 256)))))"
 153 end
 154
 155 theory bv.BV128
 156
 157   syntax literal t "#x%32x"
 158   syntax type t "(_ BitVec 128)"
 159
 160   syntax function zeros "#x00000000000000000000000000000000"
 161   syntax function one   "#x00000000000000000000000000000001"
 162   syntax function ones  "#xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF"
 163   syntax function size_bv "(_ bv128 128)"
 164
 165   syntax predicate is_signed_positive "(bvsge %1 (_ bv0 128))"
 166
 167   syntax function rotate_left_bv "(bvor (bvshl %1 (bvurem %2 (_ bv128 128))) (bvlshr %1 (bvsub (_ bv128 128) (bvurem %2 (_ bv128 128)))))"
 168   syntax function rotate_right_bv "(bvor (bvlshr %1 (bvurem %2 (_ bv128 128))) (bvshl %1 (bvsub (_ bv128 128) (bvurem %2 (_ bv128 128)))))"
 169 end
 170
 171 theory bv.BV64
 172
 173   syntax literal t "#x%16x"
 174   syntax type t "(_ BitVec 64)"
 175
 176   syntax function zeros "#x0000000000000000"
 177   syntax function one   "#x0000000000000001"
 178   syntax function ones  "#xFFFFFFFFFFFFFFFF"
 179   syntax function size_bv "(_ bv64 64)"
 180
 181   syntax predicate is_signed_positive "(bvsge %1 (_ bv0 64))"
 182
 183   syntax function rotate_left_bv "(bvor (bvshl %1 (bvurem %2 (_ bv64 64))) (bvlshr %1 (bvsub (_ bv64 64) (bvurem %2 (_ bv64 64)))))"
 184   syntax function rotate_right_bv "(bvor (bvlshr %1 (bvurem %2 (_ bv64 64))) (bvshl %1 (bvsub (_ bv64 64) (bvurem %2 (_ bv64 64)))))"
 185 end
 186
 187 theory bv.BV32
 188
 189   syntax literal t "#x%8x"
 190   syntax type t "(_ BitVec 32)"
 191
 192   syntax function zeros "#x00000000"
 193   syntax function one   "#x00000001"
 194   syntax function ones  "#xFFFFFFFF"
 195   syntax function size_bv "(_ bv32 32)"
 196
 197   syntax predicate is_signed_positive "(bvsge %1 (_ bv0 32))"
 198
 199   syntax function rotate_left_bv "(bvor (bvshl %1 (bvurem %2 (_ bv32 32))) (bvlshr %1 (bvsub (_ bv32 32) (bvurem %2 (_ bv32 32)))))"
 200   syntax function rotate_right_bv "(bvor (bvlshr %1 (bvurem %2 (_ bv32 32))) (bvshl %1 (bvsub (_ bv32 32) (bvurem %2 (_ bv32 32)))))"
 201 end
 202
 203 theory bv.BV16
 204
 205   syntax literal t "#x%4x"
 206   syntax type t "(_ BitVec 16)"
 207
 208   syntax function zeros "#x0000"
 209   syntax function one   "#x0001"
 210   syntax function ones  "#xFFFF"
 211   syntax function size_bv "(_ bv16 16)"
 212
 213   syntax predicate is_signed_positive "(bvsge %1 (_ bv0 16))"
 214
 215   syntax function rotate_left_bv "(bvor (bvshl %1 (bvurem %2 (_ bv16 16))) (bvlshr %1 (bvsub (_ bv16 16) (bvurem %2 (_ bv16 16)))))"
 216   syntax function rotate_right_bv "(bvor (bvlshr %1 (bvurem %2 (_ bv16 16))) (bvshl %1 (bvsub (_ bv16 16) (bvurem %2 (_ bv16 16)))))"
 217 end
 218
 219 theory bv.BV8
 220
 221   syntax literal t (* "#b%8b"  *) "#x%2x"
 222   syntax type t "(_ BitVec 8)"
 223
 224   syntax function zeros "#x00"
 225   syntax function one   "#x01"
 226   syntax function ones  "#xFF"
 227   syntax function size_bv "(_ bv8 8)"
 228
 229   syntax predicate is_signed_positive "(bvsge %1 (_ bv0 8))"
 230
 231   syntax function rotate_left_bv "(bvor (bvshl %1 (bvurem %2 (_ bv8 8))) (bvlshr %1 (bvsub (_ bv8 8) (bvurem %2 (_ bv8 8)))))"
 232   syntax function rotate_right_bv "(bvor (bvlshr %1 (bvurem %2 (_ bv8 8))) (bvshl %1 (bvsub (_ bv8 8) (bvurem %2 (_ bv8 8)))))"
 233 end
 234
 235 theory bv.BVConverter_Gen
 236   remove allprops
 237 end
 238
 239 theory bv.BVConverter_128_256
 240   syntax function toBig "((_ zero_extend 128) %1)"
 241   syntax function stoBig "((_ sign_extend 128) %1)"
 242   syntax function toSmall "((_ extract 127 0) %1)"
 243 end
 244
 245 theory bv.BVConverter_64_256
 246   syntax function toBig "((_ zero_extend 192) %1)"
 247   syntax function stoBig "((_ sign_extend 192) %1)"
 248   syntax function toSmall "((_ extract 63 0) %1)"
 249 end
 250
 251 theory bv.BVConverter_32_256
 252   syntax function toBig "((_ zero_extend 224) %1)"
 253   syntax function stoBig "((_ sign_extend 224) %1)"
 254   syntax function toSmall "((_ extract 31 0) %1)"
 255 end
 256
 257 theory bv.BVConverter_16_256
 258   syntax function toBig "((_ zero_extend 240) %1)"
 259   syntax function stoBig "((_ sign_extend 240) %1)"
 260   syntax function toSmall "((_ extract 15 0) %1)"
 261 end
 262
 263 theory bv.BVConverter_8_256
 264   syntax function toBig "((_ zero_extend 248) %1)"
 265   syntax function stoBig "((_ sign_extend 248) %1)"
 266   syntax function toSmall "((_ extract 7 0) %1)"
 267 end
 268
 269 theory bv.BVConverter_64_128
 270   syntax function toBig "((_ zero_extend 64) %1)"
 271   syntax function stoBig "((_ sign_extend 64) %1)"
 272   syntax function toSmall "((_ extract 63 0) %1)"
 273 end
 274
 275 theory bv.BVConverter_32_128
 276   syntax function toBig "((_ zero_extend 96) %1)"
 277   syntax function stoBig "((_ sign_extend 96) %1)"
 278   syntax function toSmall "((_ extract 31 0) %1)"
 279 end
 280
 281 theory bv.BVConverter_16_128
 282   syntax function toBig "((_ zero_extend 112) %1)"
 283   syntax function stoBig "((_ sign_extend 112) %1)"
 284   syntax function toSmall "((_ extract 15 0) %1)"
 285 end
 286
 287 theory bv.BVConverter_8_128
 288   syntax function toBig "((_ zero_extend 120) %1)"
 289   syntax function stoBig "((_ sign_extend 120) %1)"
 290   syntax function toSmall "((_ extract 7 0) %1)"
 291 end
 292
 293 theory bv.BVConverter_32_64
 294   syntax function toBig "((_ zero_extend 32) %1)"
 295   syntax function stoBig "((_ sign_extend 32) %1)"
 296   syntax function toSmall "((_ extract 31 0) %1)"
 297 end
 298
 299 theory bv.BVConverter_16_64
 300   syntax function toBig "((_ zero_extend 48) %1)"
 301   syntax function stoBig "((_ sign_extend 48) %1)"
 302   syntax function toSmall "((_ extract 15 0) %1)"
 303 end
 304
 305 theory bv.BVConverter_8_64
 306   syntax function toBig "((_ zero_extend 56) %1)"
 307   syntax function stoBig "((_ sign_extend 56) %1)"
 308   syntax function toSmall "((_ extract 7 0) %1)"
 309 end
 310
 311 theory bv.BVConverter_16_32
 312   syntax function toBig "((_ zero_extend 16) %1)"
 313   syntax function stoBig "((_ sign_extend 16) %1)"
 314   syntax function toSmall "((_ extract 15 0) %1)"
 315 end
 316
 317 theory bv.BVConverter_8_32
 318   syntax function toBig "((_ zero_extend 24) %1)"
 319   syntax function stoBig "((_ sign_extend 24) %1)"
 320   syntax function toSmall "((_ extract 7 0) %1)"
 321 end
 322
 323 theory bv.BVConverter_8_16
 324   syntax function toBig "((_ zero_extend 8) %1)"
 325   syntax function stoBig "((_ sign_extend 8) %1)"
 326   syntax function toSmall "((_ extract 7 0) %1)"
 327 end