bv.why 16.9 KB
Newer Older
1
theory CheckBV64
2
  use import bv.BV64
3 4
  use int.Int

5 6 7 8 9 10 11
  constant one   : t                                         = of_int 1
  constant two   : t                                         = of_int 2
  constant sz    : int                                       = 64
  constant mx    : int                                       =        0xFFFF_FFFF_FFFF_FFFF
  constant md    : int                                       =      0x1_0000_0000_0000_0000
  constant lastb : t                                         = of_int 0x8000_0000_0000_0000

12
  goal ok_zero   : zeros                                     = (of_int 0)
13
  goal ok_ones   : ones                                      = (of_int mx)
14
  goal ok_zero2  : to_uint zeros                             = 0
15 16 17 18 19
  goal ok_ones2  : to_uint ones                              = mx
  goal ok_size   : size                                      = sz
  goal ok_max    : max_int                                   = mx
  goal ok_tpsize : two_power_size                            = md

20 21
  goal ok1       : add ones one                              = zeros
  goal ok2       : sub zeros one                             = ones
22 23 24
  goal ok3       : neg ones                                  = one
  goal ok5       : mul one two                               = two
  goal ok6       : mul ones ones                             = one
25
  goal ok7       : udiv one two                              = zeros
26 27 28
  goal ok8       : urem one two                              = one
  goal ok9       : lsl_bv one one                            = two
  goal ok10      : lsl_bv ones one                           = sub ones one
29
  goal ok12      : lsr_bv one two                            = zeros
30
  goal ok13      : lsr_bv ones (sub (of_int sz) one)         = one
31
  goal ok14      : asr_bv one two                            = zeros
32 33 34 35
  goal ok15      : asr_bv ones two                           = ones
  goal ok16      : bw_and ones one                           = one
  goal ok17      : bw_or  ones one                           = ones
  goal ok18      : bw_xor ones one                           = sub ones one
36
  goal ok19      : bw_not ones                               = zeros
37 38 39 40
  goal ok20      : rotate_right_bv one one                   = lastb
  goal ok21      : rotate_right_bv ones two                  = ones
  goal ok22      : rotate_left_bv lastb one                  = one
  goal ok23      : rotate_left_bv ones two                   = ones
41 42
  goal ok24      : lsl_bv one (add (of_int sz) one)          = zeros
  goal ok25      : lsr_bv lastb (add (of_int sz) one)        = zeros
43 44 45 46
  goal ok26      : asr_bv lastb (add (of_int sz) one)        = ones
  goal ok27      : rotate_right_bv one (add (of_int sz) one) = lastb
  goal ok28      : rotate_left_bv one (add (of_int sz) one)  = two

47
  goal trap      : of_int md                                 = zeros
48

49 50 51
  goal smoke1    : neg lastb                                 = zeros
  goal smoke2    : udiv one zeros                            = zeros
  goal smoke3    : urem one zeros                            = zeros
52
  goal smoke4    : lsl_bv ones one                           = ones
53 54
  goal smoke5    : ugt (lsr_bv ones one) lastb
  goal smoke6    : ule (asr_bv lastb one) lastb
55 56
  goal smoke7    : rotate_right_bv one one                   = zeros
  goal smoke8    : rotate_left_bv lastb one                  = zeros
57 58 59

  (* from example/logic/bitvectors.why *)

60 61 62 63 64 65 66 67 68
  constant b0000  : t                                        = of_int 0b0000
  constant b0001  : t                                        = of_int 0b0001
  constant b0010  : t                                        = of_int 0b0010
  constant b0011  : t                                        = of_int 0b0011
  constant b0110  : t                                        = of_int 0b0110
  constant b0101  : t                                        = of_int 0b0101
  constant b0111  : t                                        = of_int 0b0111
  constant b1100  : t                                        = of_int 0b1100
  constant b11100 : t                                        = of_int 0b11100
69

70
  constant size_sub_one : int                                = Int.(-) size 1
71

72 73
  goal g1 : bw_and b0011 b0110                               = b0010
  goal f1 : bw_and b0011 b0110                               = b0011
74

75 76
  goal g2 :  bw_or b0011 b0110                               = b0111
  goal f2 :  bw_or b0011 b0110                               = b0110
77

78 79
  goal g3 :  bw_xor b0011 b0110                              = b0101
  goal g4 :  bw_not b0011                                    = (of_int 0xFFFFFFFFFFFFFFFC)
80

81 82 83
  goal g3a : lsr_bv b0111 (of_int 2)                         = b0001
  goal g3b : lsr_bv ones (of_int size_sub_one)               = b0001
  goal f3  : lsr_bv ones (of_int 0x100000001)                = (of_int 0x7FFFFFFF)
84

85 86
  goal g4a : lsl_bv b0111 (of_int 2)                         = b11100
  goal g4b : lsl_bv b0001 (of_int 31)                        = (of_int 0x80000000)
87

88 89
  goal g5a : asr_bv b0111 (of_int 2)                         = b0001
  goal g5b : asr_bv ones (of_int (Int.(-) size 1))           = ones
90

91 92
  goal g7 : to_uint b11100                                   = 28
  goal f7 : to_uint ones                                     = Int.(-_) 1
93

94 95
  goal g8a : nth_bv b0110 (of_int 2)                         = True
  goal g8b : nth_bv b0110 (of_int 3)                         = False
96

97
  goal Nth_Bv_bw_and:
98
    forall v1 v2 n. ult n size_bv ->
99
      nth_bv (bw_and v1 v2) n                                = andb (nth_bv v1 n) (nth_bv v2 n)
100

101
  goal Nth_Bv_bw_or:
102
    forall v1 v2 n. ult n size_bv ->
103
      nth_bv (bw_or v1 v2) n                                 = orb (nth_bv v1 n) (nth_bv v2 n)
104

105
  goal Nth_Bv_bw_xor:
106
    forall v1 v2 n. ult n size_bv ->
107
      nth_bv (bw_xor v1 v2) n                                = xorb (nth_bv v1 n) (nth_bv v2 n)
108

109
  goal Nth_Bv_bw_not:
110
    forall v n. ult n size_bv ->
111
      nth_bv (bw_not v) n                                    = notb (nth_bv v n)
112

113
  goal not_not : forall v:t. bw_not (bw_not v)               = v
114 115

  goal not_and : forall v1 v2:t.
116
    bw_not (bw_and v1 v2)                                    = bw_or (bw_not v1) (bw_not v2)
117

118
  goal Lsr_Bv_nth_bv_low: forall b n s.
119
    ult s size_bv -> ult n size_bv -> ult (add n s) size_bv ->
120
      nth_bv (lsr_bv b s) n                                  = nth_bv b (add n s)
121

122
  goal Lsr_Bv_nth_bv_high: forall b n s.
123
    ult s size_bv -> ult n size_bv -> uge (add n s) size_bv ->
124
      nth_bv (lsr_bv b s) n                                  = False
125

126
  goal Asr_Bv_nth_bv_low: forall b n s.
127
    ult s size_bv -> ult n size_bv -> ult (add n s) size_bv ->
128
       nth_bv (asr_bv b s) n                                 = nth_bv b (add n s)
129

130
  goal Asr_Bv_nth_bv_high: forall b n s.
131
    ult s size_bv -> ult n size_bv -> uge (add n s) size_bv ->
132
      nth_bv (asr_bv b s) n                                  = nth_bv b (sub size_bv one)
133

134
  goal Lsl_Bv_nth_bv_high: forall b n s.
135
    ult s size_bv -> ult n size_bv -> ult (sub n s) size_bv ->
136
      nth_bv (lsl_bv b s) n                                  = nth_bv b (sub n s)
137

138
  goal Lsl_Bv_nth_bv_low: forall b n s.
139
    ult s size_bv -> ult n size_bv -> uge (sub n s) size_bv ->
140
      nth_bv (lsl_bv b s) n                                  = False
141 142 143 144

end

theory CheckBV32
145
  use import bv.BV32
146 147
  use int.Int

148 149 150 151 152 153 154
  constant one   : t                                         = of_int 1
  constant two   : t                                         = of_int 2
  constant sz    : int                                       = 32
  constant mx    : int                                       = 0xFFFFFFFF
  constant md    : int                                       = 0x100000000
  constant lastb : t                                         = of_int 0x80000000

155
  goal ok_zero   : zeros                                     = (of_int 0)
156
  goal ok_ones   : ones                                      = (of_int mx)
157
  goal ok_zero2  : to_uint zeros                             = 0
158 159 160 161 162
  goal ok_ones2  : to_uint ones                              = mx
  goal ok_size   : size                                      = sz
  goal ok_max    : max_int                                   = mx
  goal ok_tpsize : two_power_size                            = md

163 164
  goal ok1       : add ones one                              = zeros
  goal ok2       : sub zeros one                             = ones
165 166 167
  goal ok3       : neg ones                                  = one
  goal ok5       : mul one two                               = two
  goal ok6       : mul ones ones                             = one
168
  goal ok7       : udiv one two                              = zeros
169 170 171
  goal ok8       : urem one two                              = one
  goal ok9       : lsl_bv one one                            = two
  goal ok10      : lsl_bv ones one                           = sub ones one
172
  goal ok12      : lsr_bv one two                            = zeros
173
  goal ok13      : lsr_bv ones (sub (of_int sz) one)         = one
174
  goal ok14      : asr_bv one two                            = zeros
175 176 177 178
  goal ok15      : asr_bv ones two                           = ones
  goal ok16      : bw_and ones one                           = one
  goal ok17      : bw_or  ones one                           = ones
  goal ok18      : bw_xor ones one                           = sub ones one
179
  goal ok19      : bw_not ones                               = zeros
180 181 182 183
  goal ok20      : rotate_right_bv one one                   = lastb
  goal ok21      : rotate_right_bv ones two                  = ones
  goal ok22      : rotate_left_bv lastb one                  = one
  goal ok23      : rotate_left_bv ones two                   = ones
184 185
  goal ok24      : lsl_bv one (add (of_int sz) one)          = zeros
  goal ok25      : lsr_bv lastb (add (of_int sz) one)        = zeros
186 187 188 189
  goal ok26      : asr_bv lastb (add (of_int sz) one)        = ones
  goal ok27      : rotate_right_bv one (add (of_int sz) one) = lastb
  goal ok28      : rotate_left_bv one (add (of_int sz) one)  = two

190
  goal trap      : of_int md                                 = zeros
191

192 193 194
  goal smoke1    : neg lastb                                 = zeros
  goal smoke2    : udiv one zeros                            = zeros
  goal smoke3    : urem one zeros                            = zeros
195
  goal smoke4    : lsl_bv ones one                           = ones
196 197
  goal smoke5    : ugt (lsr_bv ones one) lastb
  goal smoke6    : ule (asr_bv lastb one) lastb
198 199
  goal smoke7    : rotate_right_bv one one                   = zeros
  goal smoke8    : rotate_left_bv lastb one                  = zeros
200 201 202
end

theory CheckBV16
203
  use import bv.BV16
204 205
  use int.Int

206 207 208 209 210 211 212
  constant one   : t                                         = of_int 1
  constant two   : t                                         = of_int 2
  constant sz    : int                                       = 16
  constant mx    : int                                       = 65535
  constant md    : int                                       = 65536
  constant lastb : t                                         = of_int 32768

213
  goal ok_zero   : zeros                                     = (of_int 0)
214
  goal ok_ones   : ones                                      = (of_int mx)
215
  goal ok_zero2  : to_uint zeros                             = 0
216 217 218 219 220
  goal ok_ones2  : to_uint ones                              = mx
  goal ok_size   : size                                      = sz
  goal ok_max    : max_int                                   = mx
  goal ok_tpsize : two_power_size                            = md

221 222
  goal ok1       : add ones one                              = zeros
  goal ok2       : sub zeros one                             = ones
223 224 225
  goal ok3       : neg ones                                  = one
  goal ok5       : mul one two                               = two
  goal ok6       : mul ones ones                             = one
226
  goal ok7       : udiv one two                              = zeros
227 228 229
  goal ok8       : urem one two                              = one
  goal ok9       : lsl_bv one one                            = two
  goal ok10      : lsl_bv ones one                           = sub ones one
230
  goal ok12      : lsr_bv one two                            = zeros
231
  goal ok13      : lsr_bv ones (sub (of_int sz) one)         = one
232
  goal ok14      : asr_bv one two                            = zeros
233 234 235 236
  goal ok15      : asr_bv ones two                           = ones
  goal ok16      : bw_and ones one                           = one
  goal ok17      : bw_or  ones one                           = ones
  goal ok18      : bw_xor ones one                           = sub ones one
237
  goal ok19      : bw_not ones                               = zeros
238 239 240 241
  goal ok20      : rotate_right_bv one one                   = lastb
  goal ok21      : rotate_right_bv ones two                  = ones
  goal ok22      : rotate_left_bv lastb one                  = one
  goal ok23      : rotate_left_bv ones two                   = ones
242 243
  goal ok24      : lsl_bv one (add (of_int sz) one)          = zeros
  goal ok25      : lsr_bv lastb (add (of_int sz) one)        = zeros
244 245 246 247
  goal ok26      : asr_bv lastb (add (of_int sz) one)        = ones
  goal ok27      : rotate_right_bv one (add (of_int sz) one) = lastb
  goal ok28      : rotate_left_bv one (add (of_int sz) one)  = two

248
  goal trap      : of_int md                                 = zeros
249

250 251 252
  goal smoke1    : neg lastb                                 = zeros
  goal smoke2    : udiv one zeros                            = zeros
  goal smoke3    : urem one zeros                            = zeros
253
  goal smoke4    : lsl_bv ones one                           = ones
254 255
  goal smoke5    : ugt (lsr_bv ones one) lastb
  goal smoke6    : ule (asr_bv lastb one) lastb
256 257
  goal smoke7    : rotate_right_bv one one                   = zeros
  goal smoke8    : rotate_left_bv lastb one                  = zeros
258 259 260
end

theory CheckBV8
261
  use import bv.BV8
262 263
  use int.Int

264 265 266 267 268 269 270
  constant one   : t                                         = of_int 1
  constant two   : t                                         = of_int 2
  constant sz    : int                                       = 8
  constant mx    : int                                       = 255
  constant md    : int                                       = 256
  constant lastb : t                                         = of_int 128

271
  goal ok_zero   : zeros                                     = (of_int 0)
272
  goal ok_ones   : ones                                      = (of_int mx)
273
  goal ok_zero2  : to_uint zeros                             = 0
274 275 276 277 278
  goal ok_ones2  : to_uint ones                              = mx
  goal ok_size   : size                                      = sz
  goal ok_max    : max_int                                   = mx
  goal ok_tpsize : two_power_size                            = md

279 280
  goal ok1       : add ones one                              = zeros
  goal ok2       : sub zeros one                             = ones
281 282 283
  goal ok3       : neg ones                                  = one
  goal ok5       : mul one two                               = two
  goal ok6       : mul ones ones                             = one
284
  goal ok7       : udiv one two                              = zeros
285 286 287
  goal ok8       : urem one two                              = one
  goal ok9       : lsl_bv one one                            = two
  goal ok10      : lsl_bv ones one                           = sub ones one
288
  goal ok12      : lsr_bv one two                            = zeros
289
  goal ok13      : lsr_bv ones (sub (of_int sz) one)         = one
290
  goal ok14      : asr_bv one two                            = zeros
291 292 293 294
  goal ok15      : asr_bv ones two                           = ones
  goal ok16      : bw_and ones one                           = one
  goal ok17      : bw_or  ones one                           = ones
  goal ok18      : bw_xor ones one                           = sub ones one
295
  goal ok19      : bw_not ones                               = zeros
296 297 298 299
  goal ok20      : rotate_right_bv one one                   = lastb
  goal ok21      : rotate_right_bv ones two                  = ones
  goal ok22      : rotate_left_bv lastb one                  = one
  goal ok23      : rotate_left_bv ones two                   = ones
300 301
  goal ok24      : lsl_bv one (add (of_int sz) one)          = zeros
  goal ok25      : lsr_bv lastb (add (of_int sz) one)        = zeros
302 303 304 305
  goal ok26      : asr_bv lastb (add (of_int sz) one)        = ones
  goal ok27      : rotate_right_bv one (add (of_int sz) one) = lastb
  goal ok28      : rotate_left_bv one (add (of_int sz) one)  = two

306
  goal trap      : of_int md                                 = zeros
307

308 309 310
  goal smoke1    : neg lastb                                 = zeros
  goal smoke2    : udiv one zeros                            = zeros
  goal smoke3    : urem one zeros                            = zeros
311
  goal smoke4    : lsl_bv ones one                           = ones
312 313
  goal smoke5    : ugt (lsr_bv ones one) lastb
  goal smoke6    : ule (asr_bv lastb one) lastb
314 315
  goal smoke7    : rotate_right_bv one one                   = zeros
  goal smoke8    : rotate_left_bv lastb one                  = zeros
316
end