smt-libv2-bv.gen 4.46 KB
Newer Older
1 2 3 4
(* Why3 driver for SMT-LIB2, common part of bit-vector theories *)

prelude ";;; SMT-LIB2 driver: bit-vectors, common part"

5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22
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)"
  syntax predicate eq "(= %1 %2)"

23 24
  (* Warning: we should NOT remove all the axioms using "allprops" *)

25
  remove prop size_pos
26
  remove prop nth_out_of_bound
27
  remove prop Nth_zeros
28 29 30 31 32 33 34
  remove prop Nth_ones
  remove prop two_power_size_val
  remove prop max_int_val
  remove prop Nth_bw_or
  remove prop Nth_bw_and
  remove prop Nth_bw_xor
  remove prop Nth_bw_not
35 36
  remove prop Lsr_nth_low
  remove prop Lsr_nth_high
37
  remove prop lsr_zeros
38 39
  remove prop Asr_nth_low
  remove prop Asr_nth_high
40
  remove prop asr_zeros
41 42
  remove prop Lsl_nth_low
  remove prop Lsl_nth_high
43
  remove prop lsl_zeros
44 45 46 47 48 49 50
  remove prop Nth_rotate_left
  remove prop Nth_rotate_right

  remove prop to_uint_extensionality
  remove prop to_uint_bounds
  remove prop to_int_extensionality

51
  remove prop Of_int_zeros
52 53
  remove prop Of_int_ones

54 55 56 57 58 59 60 61 62 63 64
  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
  remove prop to_uint_lsr
  remove prop to_uint_lsl
65

66
  remove prop Extensionality
67 68 69 70 71 72 73 74 75 76 77 78 79 80

  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)"
end

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

81
  syntax function zeros "#x0000000000000000"
82 83
  syntax function ones "#xFFFFFFFFFFFFFFFF"

84 85
  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)))))"
86 87 88 89 90
end

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

91
  syntax function zeros "#x00000000"
92 93
  syntax function ones "#xFFFFFFFF"

94 95
  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)))))"
96 97 98 99 100
end

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

101
  syntax function zeros "#x0000"
102 103
  syntax function ones "#xFFFF"

104 105
  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)))))"
106 107 108 109 110
end

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

111
  syntax function zeros "#x00"
112 113
  syntax function ones "#xFF"

114 115
  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)))))"
116 117
end

118
theory bv.BVConverter_Gen
119
   remove allprops
120 121
end

122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151
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

152
theory bv.Pow2int
153
  remove allprops
154
end