bitvector_examples.mlw 9.84 KB
Newer Older
1 2
module Test_proofinuse

3 4 5 6
  use int.Int
  use int.Power
  use int.EuclideanDivision
  use bv.BV32
7 8 9

  (* Shift is div example -------------------  *)

10 11 12
  let shift_is_div ( x : t ) ( y : t ) : t
    requires { 0 <= t'int y < 32 }
  =
Clément Fumex's avatar
Clément Fumex committed
13
    let res = lsr_bv x one in
14 15 16 17 18 19 20
    assert { res = udiv x (2:t) };
    assert { t'int res = div (t'int x) 2 };
    let res : t = lsr_bv res (2:t) in
(*
    assert { res = udiv x (8:t) };
    assert { t'int res = div (t'int x) 8 };
*)
21 22 23 24
    res

 (* Mask example --------------------- *)

25 26
  use bv.BV8 as BV8
  use bv.BV64 as BV64
27

28 29
  use bv.BVConverter_32_64 as C32_46
  use bv.BVConverter_8_32 as C8_32
30

31 32
  type bitvec8 = BV8.t
  type bitvec64 = BV64.t
33 34

  let mask ( x : t ) =
35
    ensures { result = BV8.one }
36
    (* ensures{ not ( BV8.eq result (BV8.of_int 1) ) } *)
37 38
    let res = C8_32.toSmall(
                bw_and
Clément Fumex's avatar
Clément Fumex committed
39 40 41 42
                  (bw_or
                    (bw_and x (0xFFFF_FF00:t))
                    one)
                  (0x0000_00FF:t))
43 44 45 46
    in res

  (* test invariant from frama-c ---------------- *)

47
  use ref.Ref
48 49 50

  let testVariant( n : t ) =
    let i = ref n in
Clément Fumex's avatar
Clément Fumex committed
51
    let two = 2:t in
52 53

    while uge !i two do
54
    variant{ t'int !i }
55
      i := lsr_bv !i two
56 57 58 59
    done

  (* testssss *)

Clément Fumex's avatar
Clément Fumex committed
60
  predicate in_range (n : t) = (ule (0:t) n) /\ (ule n (0x0000_00FF:t))
61 62 63 64 65 66 67 68 69

  predicate add_over (x y : t) = (uge (add x y) x) /\ (uge (add x y) y)

  lemma ttt: forall x y.  (add_over x y) -> (forall i. ult i x -> add_over i y)
end

(** {1 Examples from Hackers Delight} *)

theory Hackers_delight
70 71
  use int.Int
  use bv.BV32
72 73 74 75 76 77 78 79 80 81

  (** de morgan's laws *)

  goal DM1: forall x y.
    bw_not( bw_and x y ) = bw_or (bw_not x) (bw_not y)

  goal DM2: forall x y.
    bw_not( bw_or x y ) = bw_and (bw_not x) (bw_not y)

  goal DM3: forall x.
Clément Fumex's avatar
Clément Fumex committed
82
    bw_not (add x one) = sub (bw_not x) one
83 84

  goal DM4: forall x.
Clément Fumex's avatar
Clément Fumex committed
85
    bw_not (sub x one) = add (bw_not x) one
86 87

  goal DM5: forall x.
Clément Fumex's avatar
Clément Fumex committed
88
    bw_not (neg x) = sub x one
89 90 91 92 93 94 95 96 97 98 99

  goal DM6: forall x y.
    bw_not( bw_xor x y ) = bw_xor (bw_not x) y (* = eq x y *)

  goal DM7: forall x y.
    bw_not( add x y ) = sub (bw_not x) y

  goal DM8: forall x y.
    bw_not( sub x y ) = add (bw_not x) y

  goal DMtest: forall x.
Clément Fumex's avatar
Clément Fumex committed
100
    zeros = bw_not( bw_or x (neg( add x one)))
101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117

  (* inequality  *)

  goal IE1: forall x y.
    ule (bw_xor x y) (bw_or x y)

  goal IE2: forall x y.
    ule (bw_and x y) (bw_not( bw_xor x y ))

  goal IE3: forall x y.
    ( ule x (add x y) /\ ule y (add x y) ) -> ule (bw_or x y) (add x y)

  goal IE4: forall x y.
    not ( ule x (add x y) /\ ule y (add x y) ) -> ugt (bw_or x y) (add x y)

  (* shift right and arithmetic shift right *)

Clément Fumex's avatar
Clément Fumex committed
118 119
  goal SR1: forall x n. ( ule zeros n /\ ule n (31:t)) ->
    bw_or (lsr_bv x n) (lsl_bv (neg( lsr_bv x (31:t) )) (sub (31:t) n))
120
  = asr_bv x n
121 122 123 124

  (* rotate en shift *)

  goal RS_left: forall x.
Clément Fumex's avatar
Clément Fumex committed
125
    bw_or (lsl_bv x one) (lsr_bv x (31:t)) = rotate_left_bv x one
126 127

  goal RS_right: forall x.
Clément Fumex's avatar
Clément Fumex committed
128
    bw_or (lsr_bv x one) (lsl_bv x (31:t)) = rotate_right_bv x one
129 130 131 132 133 134

  (* bound propagation *)

  goal BP1: forall a b c d x y.
    ( ule a x /\ ule x b /\ ule c y /\ ule y d ) ->
    ( ule b (add b d) /\ ule d (add b d) ) -> (* no overflow in addition *)
135
      ule (bw_or x y) (add b d) /\ ule zeros (bw_and x y)
136 137 138 139

  goal BP2: forall a b c d x y.
    ( ule a x /\ ule x b /\ ule c y /\ ule y d ) ->
    ( ule b (add b d) /\ ule d (add b d) ) -> (* no overflow in addition *)
140
      ule zeros (bw_xor x y) /\ ule (bw_xor x y) (add b d)
141 142 143 144 145 146 147 148

  goal BP3: forall a b c d x y.
    ( ule a x /\ ule x b /\ ule c y /\ ule y d ) ->
      ule (bw_not b) (bw_not x) /\ ule (bw_not x) (bw_not a)

end

module Hackers_delight_mod
149 150
  use int.Int
  use bv.BV32
151 152 153 154 155 156 157 158 159 160 161 162

  (* de morgan's laws *)

  let dm1 (x : t) (y : t) =
    ensures{ result = bw_or (bw_not x) (bw_not y) }
    bw_not( bw_and x y )

  let dm2 (x : t) (y : t) =
    ensures{ result = bw_and (bw_not x) (bw_not y) }
    bw_not( bw_or x y )

  let dm3 (x : t) =
Clément Fumex's avatar
Clément Fumex committed
163 164
    ensures{ result = sub (bw_not x) one }
    bw_not( add x one )
165 166

  let dm4 (x : t) =
Clément Fumex's avatar
Clément Fumex committed
167 168
    ensures{ result = add (bw_not x) one }
    bw_not( sub x one )
169 170

  let dm5 (x : t) =
Clément Fumex's avatar
Clément Fumex committed
171
    ensures{ result = sub x one }
172 173 174 175 176 177 178 179 180 181 182 183 184 185 186
    bw_not( neg x )

  let dm6 (x : t) (y : t) =
    ensures{ result = bw_xor (bw_not x) y }
    bw_not( bw_xor x y )

  let dm7 (x : t) (y : t) =
    ensures{ result = sub (bw_not x) y }
    bw_not( add x y )

  let dm8 (x : t) (y : t) =
    ensures{ result = add (bw_not x) y }
    bw_not( sub x y )

  let dmtest (x : t) =
187
    ensures{ result = zeros }
Clément Fumex's avatar
Clément Fumex committed
188
    bw_not( bw_or x (neg( add x one)))
189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212

  (* inequality  *)

  let ie1 (x : t) (y : t) =
    ensures{ ule result (bw_or x y) }
    bw_xor x y

  let ie2 (x : t) (y : t) =
    ensures{ ule result (bw_not( bw_xor x y ))}
    bw_and x y

  let ie3 (x : t) (y : t) =
    requires{ ule x (add x y) /\ ule y (add x y) }
    ensures{ ule result (add x y) }
    bw_or x y

  let ie4 (x : t) (y : t) =
    requires{ not ( ule x (add x y) /\ ule y (add x y) ) }
    ensures{ ugt result (add x y) }
    bw_or x y

  (* shift right and arithmetic shift right *)

  let sr1 (x : t) (n : t) =
Clément Fumex's avatar
Clément Fumex committed
213
    requires{ ule zeros n /\ ule n (31:t) }
214
    ensures{ result = asr_bv x n }
Clément Fumex's avatar
Clément Fumex committed
215
    bw_or (lsr_bv x n) (lsl_bv (neg( lsr_bv x (31:t) )) (sub (31:t) n))
216 217 218 219

  (* rotate en shift *)

  let rs_left (x : t) =
Clément Fumex's avatar
Clément Fumex committed
220 221
  ensures{ result = rotate_left_bv x one }
    bw_or (lsl_bv x one) (lsr_bv x (31:t))
222 223

  let rs_right (x : t) =
Clément Fumex's avatar
Clément Fumex committed
224 225
  ensures{ result = rotate_right_bv x one }
    bw_or (lsr_bv x one) (lsl_bv x (31:t))
226 227 228 229 230 231 232 233 234 235 236 237 238 239

  (* bound propagation *)

  let bp1 (a b c d x y : t) =
  requires{ ule a x /\ ule x b }
  requires{ ule c y /\ ule y d }
  requires{ ule b (add b d) /\ ule d (add b d) } (* no overflow in addition *)
  ensures{ ule result (add b d) }
    bw_or x y

  let bp1' (a b c d x y : t) =
  requires{ ule a x /\ ule x b }
  requires{ ule c y /\ ule y d }
  requires{ ule b (add b d) /\ ule d (add b d) } (* no overflow in addition *)
240
  ensures{ ule zeros result }
241 242 243 244 245 246
    bw_and x y

  let bp2 (a b c d x y : t) =
  requires{ ule a x /\ ule x b }
  requires{ ule c y /\ ule y d }
  requires{ ule b (add b d) /\ ule d (add b d) } (* no overflow in addition *)
247
  ensures{ ule zeros result }
248 249 250 251 252 253 254 255 256 257 258 259 260 261
  ensures{ ule result (add b d) }
    bw_xor x y

  let bp3 (a b c d x y : t) =
  requires{ ule a x /\ ule x b }
  requires{ ule c y /\ ule y d }
  ensures{ ule (bw_not b) result }
  ensures{ ule result (bw_not a) }
    bw_not x

end

module Test_imperial_violet

262 263 264 265
  use int.Int
  use int.EuclideanDivision
  use bv.BV32
  use array.Array
266 267 268 269

  (* to_int and bounds *)

  lemma bv32_bounds_bv:
270
    forall b. ule zeros b /\ ule b ones
271 272

  lemma to_int_ule:
Clément Fumex's avatar
Clément Fumex committed
273
    forall b c. ule b c -> t'int b <= t'int c
274 275

  lemma to_int_ult:
Clément Fumex's avatar
Clément Fumex committed
276
    forall b c. ult b c -> t'int b < t'int c
277 278

  lemma bv32_bounds_0:
Clément Fumex's avatar
Clément Fumex committed
279
    forall b. 0 <= t'int b
280 281

  lemma bv32_bounds:
Clément Fumex's avatar
Clément Fumex committed
282
    forall b. 0 <= t'int b < 0x1_0000_0000
283 284 285 286 287 288

  (* bounded add of array of t *)

  let add (a : array t ) (b : array t) =
    requires{ length a = length b }
    requires{ forall i. 0 <= i < length a ->
Clément Fumex's avatar
Clément Fumex committed
289
                ult a[i] (0x8000_0000:t) }
290
    requires{ forall i. 0 <= i < length b ->
Clément Fumex's avatar
Clément Fumex committed
291
                ult b[i] (0x8000_0000:t) }
292
    ensures{ forall i. 0 <= i < length result ->
Clément Fumex's avatar
Clément Fumex committed
293
               t'int result[i] = t'int a[i] + t'int b[i] }
294
    let sum = make (length a) zeros in
295 296
    for i = 0 to length a - 1 do
      invariant{ forall j. 0 <= j < i -> sum[j] = add a[j] b[j] }
Clément Fumex's avatar
Clément Fumex committed
297
      invariant{ forall j. 0 <= j < i -> t'int sum[j] = t'int a[j] + t'int b[j] }
298 299 300 301 302 303 304 305
      sum[i] <- add a[i] b[i]
    done;
    sum

end

module Test_from_bitvector_example

306 307
  use int.Int
  use bv.BV32
308 309

  goal Test1:
Clément Fumex's avatar
Clément Fumex committed
310
    let b = bw_and zeros ones in nth_bv b one = False
311 312

  goal Test2:
Clément Fumex's avatar
Clément Fumex committed
313
    let b = lsr_bv ones (16:t) in nth_bv b (15:t) = True
314 315

  goal Test3:
Clément Fumex's avatar
Clément Fumex committed
316
    let b = lsr_bv ones (16:t) in nth_bv b (16:t) = False
317 318

  goal Test4:
Clément Fumex's avatar
Clément Fumex committed
319
    let b = asr_bv ones (16:t) in nth_bv b (15:t) = True
320 321

  goal Test5:
Clément Fumex's avatar
Clément Fumex committed
322
    let b = asr_bv ones (16:t) in nth_bv b (16:t) = True
323 324

  goal Test6:
Clément Fumex's avatar
Clément Fumex committed
325
    let b = asr_bv (lsr_bv ones one) (16:t) in nth_bv b (16:t) = False
326 327

  let lsr31 () =
Clément Fumex's avatar
Clément Fumex committed
328 329
    ensures{ result = one }
    lsr_bv ones (31:t)
330 331

  let lsr30 () =
Clément Fumex's avatar
Clément Fumex committed
332 333
    ensures{ result = (3:t) }
    lsr_bv ones (30:t)
334 335

  let lsr29 () =
Clément Fumex's avatar
Clément Fumex committed
336 337
    ensures{ t'int result = 7 }
    lsr_bv ones (29:t)
338 339

  let lsr28 () =
Clément Fumex's avatar
Clément Fumex committed
340 341
    ensures{ t'int result = 15 }
    lsr_bv ones (28:t)
342 343

  let lsr27 () =
Clément Fumex's avatar
Clément Fumex committed
344 345
    ensures{ t'int result = 31 }
    lsr_bv ones (27:t)
346 347

  let lsr26 () =
Clément Fumex's avatar
Clément Fumex committed
348 349
    ensures{ t'int result = 63 }
    lsr_bv ones (26:t)
350 351

  let lsr20 () =
Clément Fumex's avatar
Clément Fumex committed
352 353
    ensures{ t'int result = 4095 }
    lsr_bv ones (20:t)
354 355

  let lsr13 () =
Clément Fumex's avatar
Clément Fumex committed
356 357
    ensures{ t'int result = 524287 }
    lsr_bv ones (13:t)
358 359

  let lsr8 () =
Clément Fumex's avatar
Clément Fumex committed
360 361
    ensures{ t'int result = 16777215 }
    lsr_bv ones (8:t)
362 363

  goal to_int_0x00000001:
Clément Fumex's avatar
Clément Fumex committed
364
    t'int (lsr_bv ones (31:t)) = 1
365 366

  goal to_int_0x00000003:
Clément Fumex's avatar
Clément Fumex committed
367
    t'int (lsr_bv ones (30:t)) = 3
368 369

  goal to_int_0x00000007:
Clément Fumex's avatar
Clément Fumex committed
370
    t'int (lsr_bv ones (29:t)) = 7
371 372

  goal to_int_0x0000000F:
Clément Fumex's avatar
Clément Fumex committed
373
    t'int (lsr_bv ones (28:t)) = 15
374 375

  goal to_int_0x0000001F:
Clément Fumex's avatar
Clément Fumex committed
376
    t'int (lsr_bv ones (27:t)) = 31
377 378

  goal to_int_0x0000003F:
Clément Fumex's avatar
Clément Fumex committed
379
    t'int (lsr_bv ones (26:t)) = 63
380 381

  goal to_int_0x0000007F:
Clément Fumex's avatar
Clément Fumex committed
382
    t'int (lsr_bv ones (25:t)) = 127
383 384

  goal to_int_0x000000FF:
Clément Fumex's avatar
Clément Fumex committed
385
    t'int (lsr_bv ones (24:t)) = 255
386 387

  goal to_int_0x000001FF:
Clément Fumex's avatar
Clément Fumex committed
388
    t'int (lsr_bv ones (23:t)) = 511
389 390

  goal to_int_0x000003FF:
Clément Fumex's avatar
Clément Fumex committed
391
    t'int (lsr_bv ones (22:t)) = 1023
392 393

  goal to_int_0x000007FF:
Clément Fumex's avatar
Clément Fumex committed
394
    t'int (lsr_bv ones (21:t)) = 2047
395 396

  goal to_int_0x00000FFF:
Clément Fumex's avatar
Clément Fumex committed
397
    t'int (lsr_bv ones (20:t)) = 4095
398 399

  goal to_int_0x00001FFF:
Clément Fumex's avatar
Clément Fumex committed
400
    t'int (lsr_bv ones (19:t)) = 8191
401 402

  goal to_int_0x00003FFF:
Clément Fumex's avatar
Clément Fumex committed
403
    t'int (lsr_bv ones (18:t)) = 16383
404 405

  goal to_int_0x00007FFF:
Clément Fumex's avatar
Clément Fumex committed
406
    t'int (lsr_bv ones (17:t)) = 32767
407 408

  goal to_int_0x0000FFFF:
Clément Fumex's avatar
Clément Fumex committed
409
    t'int (lsr_bv ones (16:t)) = 65535
410 411

  goal to_int_0x0001FFFF:
Clément Fumex's avatar
Clément Fumex committed
412
    t'int (lsr_bv ones (15:t)) = 131071
413 414

  goal to_int_0x0003FFFF:
Clément Fumex's avatar
Clément Fumex committed
415
    t'int (lsr_bv ones (14:t)) = 262143
416 417

  goal to_int_0x0007FFFF:
Clément Fumex's avatar
Clément Fumex committed
418
    t'int (lsr_bv ones (13:t)) = 524287
419 420

  goal to_int_0x000FFFFF:
Clément Fumex's avatar
Clément Fumex committed
421
    t'int (lsr_bv ones (12:t)) = 1048575
422 423

  goal to_int_0x00FFFFFF:
Clément Fumex's avatar
Clément Fumex committed
424
    t'int (lsr_bv ones (8:t)) = 16777215
425 426

  goal to_int_0xFFFFFFFF:
Clément Fumex's avatar
Clément Fumex committed
427
    t'int ones = 4294967295
428 429

end