mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
430 lines
9.9 KiB
Plaintext
430 lines
9.9 KiB
Plaintext
module Test_proofinuse
|
|
|
|
use int.Int
|
|
use int.Power
|
|
use int.EuclideanDivision
|
|
use bv.BV32
|
|
|
|
(* Shift is div example ------------------- *)
|
|
|
|
let shift_is_div ( x : t ) ( y : t ) : t
|
|
requires { 0 <= t'int y < 32 }
|
|
=
|
|
let res = lsr_bv x 0x1 in
|
|
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 };
|
|
*)
|
|
res
|
|
|
|
(* Mask example --------------------- *)
|
|
|
|
use bv.BV8 as BV8
|
|
use bv.BV64 as BV64
|
|
|
|
use bv.BVConverter_32_64 as C32_46
|
|
use bv.BVConverter_8_32 as C8_32
|
|
|
|
type bitvec8 = BV8.t
|
|
type bitvec64 = BV64.t
|
|
|
|
let mask ( x : t ) =
|
|
ensures { result = BV8.one }
|
|
(* ensures{ not ( BV8.eq result (BV8.of_int 1) ) } *)
|
|
let res = C8_32.toSmall(
|
|
bw_and
|
|
(bw_or
|
|
(bw_and x (0xFFFF_FF00:t))
|
|
0x1)
|
|
(0x0000_00FF:t))
|
|
in res
|
|
|
|
(* test invariant from frama-c ---------------- *)
|
|
|
|
use ref.Ref
|
|
|
|
let testVariant( n : t ) =
|
|
let i = ref n in
|
|
let two = 2:t in
|
|
|
|
while uge !i two do
|
|
variant{ t'int !i }
|
|
i := lsr_bv !i two
|
|
done
|
|
|
|
(* testssss *)
|
|
|
|
predicate in_range (n : t) = (ule (0:t) n) /\ (ule n (0x0000_00FF:t))
|
|
|
|
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
|
|
use int.Int
|
|
use bv.BV32
|
|
|
|
(** 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.
|
|
bw_not (add x one) = sub (bw_not x) one
|
|
|
|
goal DM4: forall x.
|
|
bw_not (sub x one) = add (bw_not x) one
|
|
|
|
goal DM5: forall x.
|
|
bw_not (neg x) = sub x one
|
|
|
|
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.
|
|
zeros = bw_not( bw_or x (neg( add x one)))
|
|
|
|
(* 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 *)
|
|
|
|
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))
|
|
= asr_bv x n
|
|
|
|
(* rotate en shift *)
|
|
|
|
goal RS_left: forall x.
|
|
bw_or (lsl_bv x one) (lsr_bv x (31:t)) = rotate_left_bv x one
|
|
|
|
goal RS_right: forall x.
|
|
bw_or (lsr_bv x one) (lsl_bv x (31:t)) = rotate_right_bv x one
|
|
|
|
(* 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 *)
|
|
ule (bw_or x y) (add b d) /\ ule zeros (bw_and x y)
|
|
|
|
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 *)
|
|
ule zeros (bw_xor x y) /\ ule (bw_xor x y) (add b d)
|
|
|
|
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
|
|
use int.Int
|
|
use bv.BV32
|
|
|
|
(* 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) =
|
|
ensures{ result = sub (bw_not x) one }
|
|
bw_not( add x 0x1 )
|
|
|
|
let dm4 (x : t) =
|
|
ensures{ result = add (bw_not x) one }
|
|
bw_not( sub x 0x1 )
|
|
|
|
let dm5 (x : t) =
|
|
ensures{ result = sub x one }
|
|
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) =
|
|
ensures{ result = zeros }
|
|
bw_not( bw_or x (neg( add x 0x1)))
|
|
|
|
(* 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) =
|
|
requires{ ule zeros n /\ ule n (31:t) }
|
|
ensures{ result = asr_bv x n }
|
|
bw_or (lsr_bv x n) (lsl_bv (neg( lsr_bv x (31:t) )) (sub (31:t) n))
|
|
|
|
(* rotate en shift *)
|
|
|
|
let rs_left (x : t) =
|
|
ensures{ result = rotate_left_bv x one }
|
|
bw_or (lsl_bv x 0x1) (lsr_bv x (31:t))
|
|
|
|
let rs_right (x : t) =
|
|
ensures{ result = rotate_right_bv x one }
|
|
bw_or (lsr_bv x 0x1) (lsl_bv x (31:t))
|
|
|
|
(* 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 *)
|
|
ensures{ ule zeros result }
|
|
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 *)
|
|
ensures{ ule zeros result }
|
|
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
|
|
|
|
use int.Int
|
|
use int.EuclideanDivision
|
|
use bv.BV32
|
|
use array.Array
|
|
|
|
(* to_int and bounds *)
|
|
|
|
lemma bv32_bounds_bv:
|
|
forall b. ule zeros b /\ ule b ones
|
|
|
|
lemma to_int_ule:
|
|
forall b c. ule b c -> t'int b <= t'int c
|
|
|
|
lemma to_int_ult:
|
|
forall b c. ult b c -> t'int b < t'int c
|
|
|
|
lemma bv32_bounds_0:
|
|
forall b. 0 <= t'int b
|
|
|
|
lemma bv32_bounds:
|
|
forall b. 0 <= t'int b < 0x1_0000_0000
|
|
|
|
(* 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 ->
|
|
ult a[i] (0x8000_0000:t) }
|
|
requires{ forall i. 0 <= i < length b ->
|
|
ult b[i] (0x8000_0000:t) }
|
|
ensures{ forall i. 0 <= i < length result ->
|
|
t'int result[i] = t'int a[i] + t'int b[i] }
|
|
let sum = make (length a) 0x0 in
|
|
for i = 0 to length a - 1 do
|
|
invariant{ forall j. 0 <= j < i -> sum[j] = add a[j] b[j] }
|
|
invariant{ forall j. 0 <= j < i -> t'int sum[j] = t'int a[j] + t'int b[j] }
|
|
sum[i] <- add a[i] b[i]
|
|
done;
|
|
sum
|
|
|
|
end
|
|
|
|
module Test_from_bitvector_example
|
|
|
|
use int.Int
|
|
use bv.BV32
|
|
|
|
goal Test1:
|
|
let b = bw_and zeros ones in nth_bv b one = False
|
|
|
|
goal Test2:
|
|
let b = lsr_bv ones (16:t) in nth_bv b (15:t) = True
|
|
|
|
goal Test3:
|
|
let b = lsr_bv ones (16:t) in nth_bv b (16:t) = False
|
|
|
|
goal Test4:
|
|
let b = asr_bv ones (16:t) in nth_bv b (15:t) = True
|
|
|
|
goal Test5:
|
|
let b = asr_bv ones (16:t) in nth_bv b (16:t) = True
|
|
|
|
goal Test6:
|
|
let b = asr_bv (lsr_bv ones one) (16:t) in nth_bv b (16:t) = False
|
|
|
|
let lsr31 () =
|
|
ensures{ result = one }
|
|
lsr_bv 0xFFFF_FFFF (31:t)
|
|
|
|
let lsr30 () =
|
|
ensures{ result = (3:t) }
|
|
lsr_bv 0xFFFF_FFFF (30:t)
|
|
|
|
let lsr29 () =
|
|
ensures{ t'int result = 7 }
|
|
lsr_bv 0xFFFF_FFFF (29:t)
|
|
|
|
let lsr28 () =
|
|
ensures{ t'int result = 15 }
|
|
lsr_bv 0xFFFF_FFFF (28:t)
|
|
|
|
let lsr27 () =
|
|
ensures{ t'int result = 31 }
|
|
lsr_bv 0xFFFF_FFFF (27:t)
|
|
|
|
let lsr26 () =
|
|
ensures{ t'int result = 63 }
|
|
lsr_bv 0xFFFF_FFFF (26:t)
|
|
|
|
let lsr20 () =
|
|
ensures{ t'int result = 4095 }
|
|
lsr_bv 0xFFFF_FFFF (20:t)
|
|
|
|
let lsr13 () =
|
|
ensures{ t'int result = 524287 }
|
|
lsr_bv 0xFFFF_FFFF (13:t)
|
|
|
|
let lsr8 () =
|
|
ensures{ t'int result = 16777215 }
|
|
lsr_bv 0xFFFF_FFFF (8:t)
|
|
|
|
goal to_int_0x00000001:
|
|
t'int (lsr_bv ones (31:t)) = 1
|
|
|
|
goal to_int_0x00000003:
|
|
t'int (lsr_bv ones (30:t)) = 3
|
|
|
|
goal to_int_0x00000007:
|
|
t'int (lsr_bv ones (29:t)) = 7
|
|
|
|
goal to_int_0x0000000F:
|
|
t'int (lsr_bv ones (28:t)) = 15
|
|
|
|
goal to_int_0x0000001F:
|
|
t'int (lsr_bv ones (27:t)) = 31
|
|
|
|
goal to_int_0x0000003F:
|
|
t'int (lsr_bv ones (26:t)) = 63
|
|
|
|
goal to_int_0x0000007F:
|
|
t'int (lsr_bv ones (25:t)) = 127
|
|
|
|
goal to_int_0x000000FF:
|
|
t'int (lsr_bv ones (24:t)) = 255
|
|
|
|
goal to_int_0x000001FF:
|
|
t'int (lsr_bv ones (23:t)) = 511
|
|
|
|
goal to_int_0x000003FF:
|
|
t'int (lsr_bv ones (22:t)) = 1023
|
|
|
|
goal to_int_0x000007FF:
|
|
t'int (lsr_bv ones (21:t)) = 2047
|
|
|
|
goal to_int_0x00000FFF:
|
|
t'int (lsr_bv ones (20:t)) = 4095
|
|
|
|
goal to_int_0x00001FFF:
|
|
t'int (lsr_bv ones (19:t)) = 8191
|
|
|
|
goal to_int_0x00003FFF:
|
|
t'int (lsr_bv ones (18:t)) = 16383
|
|
|
|
goal to_int_0x00007FFF:
|
|
t'int (lsr_bv ones (17:t)) = 32767
|
|
|
|
goal to_int_0x0000FFFF:
|
|
t'int (lsr_bv ones (16:t)) = 65535
|
|
|
|
goal to_int_0x0001FFFF:
|
|
t'int (lsr_bv ones (15:t)) = 131071
|
|
|
|
goal to_int_0x0003FFFF:
|
|
t'int (lsr_bv ones (14:t)) = 262143
|
|
|
|
goal to_int_0x0007FFFF:
|
|
t'int (lsr_bv ones (13:t)) = 524287
|
|
|
|
goal to_int_0x000FFFFF:
|
|
t'int (lsr_bv ones (12:t)) = 1048575
|
|
|
|
goal to_int_0x00FFFFFF:
|
|
t'int (lsr_bv ones (8:t)) = 16777215
|
|
|
|
goal to_int_0xFFFFFFFF:
|
|
t'int ones = 4294967295
|
|
|
|
end
|