ada/why3
0
0
Fork 0
mirror of https://github.com/AdaCore/why3.git synced 2026-02-12 12:34:55 -08:00
Code Issues Packages Projects Releases Wiki Activity
Files
master
why3/examples/bitwalker.mlw
BONNOT Paul 58313caa48 Resolve "Give values to BV constants when cloning"
2023-06-16 08:44:32 +00:00

322 lines
12 KiB
Plaintext
Raw Permalink Blame History

module Bitwalker
use int.Int
use int.EuclideanDivision
use array.Array
use ref.Ref
(* use bv.BV32 *)
(* use bv.BV8 *)
(* use bv.BV64 *)
use mach.bv.BVCheck8 as BV8
use mach.bv.BVCheck32 as BV32
use mach.bv.BVCheck64 as BV64
use bv.BVConverter_32_64 as C32_64
use bv.BVConverter_8_32 as C8_32
(* file missing in repository
use mach.bv.BV
*)
function nth8_stream (stream : array BV8.t) (pos : int) : bool =
BV8.nth stream[div pos 8] (7 - mod pos 8)
lemma nth64:
forall value:BV64.t, i:int. 0 <= i < 64 ->
BV64.nth value i = BV64.nth_bv value (C32_64.toBig (BV32.of_int i))
lemma nth8:
forall value:BV8.t, i:int. 0 <= i < 8 ->
BV8.nth value i = BV8.nth_bv value (C8_32.toSmall (BV32.of_int i))
(* *)
let function maxvalue (len : BV32.t) : BV64.t =
BV64.lsl_bv (1:BV64.t) (C32_64.toBig len)
let lemma nth_ultpre0 (x:BV64.t) (len:BV32.t)
requires { BV32.t'int len < 64}
ensures { BV64.eq_sub x BV64.zeros (BV32.t'int len) (64 - BV32.t'int len)
<-> BV64.t'int x < BV64.t'int (maxvalue len) }
=
assert { BV32.ult len (64:BV32.t) };
assert { BV64.eq_sub_bv x BV64.zeros (C32_64.toBig len) (BV64.sub (64:BV64.t) (C32_64.toBig len))
<-> BV64.ult x (maxvalue len) }
(** return `value` with the bit of index `left` from the left set to `flag` *)
let poke_64bit_bv (value : BV64.t) (left : BV32.t) (flag : bool) : BV64.t
requires { BV32.t'int left < 64 }
ensures { forall i. 0 <= i < 64 /\ i <> 63 - BV32.t'int left ->
BV64.nth result i = BV64.nth value i }
ensures { flag = BV64.nth result (63 - BV32.t'int left) }
=
assert { BV32.ult left (64:BV32.t) };
begin
ensures { forall i:BV32.t. i <> BV32.sub (63:BV32.t) left ->
BV64.nth_bv result (C32_64.toBig i) =
BV64.nth_bv value (C32_64.toBig i) }
ensures { flag = BV64.nth_bv result
(C32_64.toBig (BV32.sub (63:BV32.t) left)) }
let mask =
BV64.lsl_bv (1:BV64.t)
(C32_64.toBig (BV32.u_sub (63:BV32.t) left))
in
match flag with
| True -> BV64.bw_or value mask
| False -> BV64.bw_and value (BV64.bw_not mask)
end
end
(** return `value` with the bit of index `left` from the left set to `flag` *)
(* version where `left` is an int and not a bitvector, which
is closer to the result of the SPARK translation from signed
integers *)
let poke_64bit (value : BV64.t) (left : int) (flag : bool) : BV64.t
requires { 0 <= left < 64 }
ensures { forall i. 0 <= i < 64 /\ i <> 63 - left ->
BV64.nth result i = BV64.nth value i }
ensures { flag = BV64.nth result (63 - left) }
=
let ghost left_bv = BV64.of_int left in
assert { BV64.ult left_bv (64:BV64.t) };
assert { (BV64.sub (63:BV64.t) left_bv) = BV64.of_int (63 - left) };
begin
ensures { forall i:BV64.t. BV64.ule i (63:BV64.t) ->
i <> BV64.sub (63:BV64.t) left_bv ->
BV64.nth_bv result i = BV64.nth_bv value i }
ensures { flag = BV64.nth_bv result (BV64.sub (63:BV64.t) left_bv) }
let mask =
BV64.lsl_bv (1:BV64.t) (BV64.of_int (63 - left))
in
match flag with
| True -> BV64.bw_or value mask
| False -> BV64.bw_and value (BV64.bw_not mask)
end
end
(* return the bit of `byte` at position `left` starting from the
left *)
let peek_8bit_bv (byte : BV8.t) (left : BV32.t) : bool
requires { 0 <= BV32.t'int left < 8 }
ensures { result = BV8.nth byte (7 - BV32.t'int left) }
=
assert {BV32.ult left (8:BV32.t)};
begin
ensures {
result = BV8.nth_bv
byte (BV8.sub (7:BV8.t) (C8_32.toSmall left))}
let mask =
BV32.lsl_bv (1:BV32.t) (BV32.u_sub (7:BV32.t) left)
in
not (BV32.eq (BV32.bw_and (C8_32.toBig byte) mask) 0x0)
end
(* return the bit of the `left`/8 element of `addr` at position mod `left` 8 starting from the left *)
let peek_8bit_array (addr : array BV8.t) (left : BV32.t) : bool
requires { 8 * (length addr) < BV32.two_power_size }
requires { BV32.t'int left < 8 * length addr }
ensures { result = nth8_stream addr (BV32.t'int left) }
=
peek_8bit_bv (addr[ BV32.to_uint (BV32.u_div left (8:BV32.t)) ]) (BV32.u_rem left (8:BV32.t))
(* return a bitvector of 64 bits with its `len` bits of the right
set to the bits between `start` and `start+len` of `addr` *)
let peek (start : BV32.t) (len : BV32.t) (addr : array BV8.t) : BV64.t
requires { BV32.t'int len <= 64 }
requires { BV32.t'int start + BV32.t'int len < BV32.two_power_size }
requires { 8 * length addr < BV32.two_power_size }
ensures { BV32.t'int start + BV32.t'int len > (8 * length addr) ->
result = BV64.zeros }
ensures { BV32.t'int start + BV32.t'int len <= (8 * length addr) ->
(forall i:int. 0 <= i < BV32.t'int len ->
BV64.nth result i
= nth8_stream addr (BV32.t'int start + BV32.t'int len - i - 1))
/\
(forall i:int. BV32.t'int len <= i < 64 -> BV64.nth result i = False) }
=
if (BV32.to_uint (BV32.u_add start len) > ( 8 *length addr ))
then
0x0
else
let retval = ref 0x0 in
let i = ref 0x0 in
let lstart = BV32.u_sub (64:BV32.t) len in
while BV32.ult !i len do variant{ BV32.t'int len - BV32.t'int !i }
invariant {0 <= BV32.t'int !i <= BV32.t'int len}
invariant {forall j:int. BV32.t'int len - BV32.t'int !i <= j < BV32.t'int len ->
BV64.nth !retval j
= nth8_stream addr (BV32.t'int start + BV32.t'int len - j - 1)}
invariant {forall j:int. 0 <= j < BV32.t'int len - BV32.t'int !i ->
BV64.nth !retval j
= False}
invariant {forall j:int. BV32.t'int len <= j < 64 ->
BV64.nth !retval j
= False}
let flag = peek_8bit_array addr (BV32.u_add start !i) in
retval := poke_64bit_bv !retval (BV32.u_add lstart !i) flag;
i := BV32.u_add !i (1:BV32.t);
done;
!retval
let peek_64bit (value : BV64.t) (left : BV32.t) : bool
requires {BV32.t'int left < 64}
ensures {result = BV64.nth value (63 - BV32.t'int left)}
=
assert {BV32.ult left (64:BV32.t)};
begin
ensures {result = BV64.nth_bv value
(BV64.sub (63:BV64.t) (C32_64.toBig left))}
let mask = BV64.lsl_bv (1:BV64.t)
(C32_64.toBig (BV32.u_sub (63:BV32.t) left)) in
not (BV64.eq (BV64.bw_and value mask) 0x0)
end
(*
static inline uint8_t PokeBit8(uint8_t byte, uint32_t left, int flag)
{
uint8_t mask = ((uint8_t) 1) << (7u - left);
return (flag == 0) ? (byte & ~mask) : (byte | mask);
}
*)
(* return `byte` with the bit at index `left` from the left set to `flag` *)
let poke_8bit (byte : BV8.t) (left : BV32.t) (flag : bool) : BV8.t
requires { BV32.t'int left < 8 }
ensures { forall i:int. 0 <= i < 8 -> i <> 7 - BV32.t'int left ->
BV8.nth result i = BV8.nth byte i }
ensures { BV8.nth result (7 - BV32.t'int left) = flag }
=
assert { BV32.ult left (8:BV32.t) };
begin
ensures { forall i:BV32.t. BV32.ult i (8:BV32.t) ->
i <> BV32.sub (7:BV32.t) left ->
BV8.nth_bv result (C8_32.toSmall i)
= BV8.nth_bv byte (C8_32.toSmall i) }
ensures { BV8.nth_bv result (BV8.sub (7:BV8.t) (C8_32.toSmall left))
= flag }
let mask = BV8.lsl_bv (1:BV8.t) (BV8.u_sub (7:BV8.t) (C8_32.toSmall left)) in
match flag with
| True -> BV8.bw_or byte mask
| False -> BV8.bw_and byte (BV8.bw_not mask)
end
end
let poke_8bit_array (addr : array BV8.t) (left : BV32.t) (flag : bool)
requires { 8 * (length addr) < BV32.two_power_size }
requires { BV32.t'int left < 8 * length addr }
writes { addr }
ensures { forall i:int. 0 <= i < 8 * length addr -> i <> BV32.t'int left ->
nth8_stream addr i = nth8_stream (old addr) i}
ensures { nth8_stream addr (BV32.t'int left) = flag }
=
let i = BV32.u_div left (8:BV32.t) in
let k = BV32.u_rem left (8:BV32.t) in
addr[BV32.to_uint i] <- poke_8bit addr[BV32.to_uint i] k flag
let poke (start : BV32.t) (len : BV32.t) (addr : array BV8.t) (value : BV64.t) : int
writes { addr }
requires{ BV32.t'int len < 64 } (* could be lower or equal if maxvalue and the condition to return -2 is corrected *)
requires{ BV32.t'int start + BV32.t'int len < BV32.two_power_size }
requires{ 8 * length addr < BV32.two_power_size }
ensures { -2 <= result <= 0 }
ensures { result = -1 <-> BV32.t'int start + BV32.t'int len > 8 * length addr }
ensures { result = -2 <-> BV64.t'int (maxvalue len) <= BV64.t'int value /\ BV32.t'int start + BV32.t'int len <= 8 * length addr }
ensures { result = 0 <-> BV64.t'int (maxvalue len) > BV64.t'int value /\ BV32.t'int start + BV32.t'int len <= 8 * length addr }
ensures { result = 0 ->
(forall i:int. 0 <= i < BV32.t'int start ->
nth8_stream (old addr) i
= nth8_stream addr i)
/\
(forall i:int. BV32.t'int start <= i < BV32.t'int start + BV32.t'int len ->
nth8_stream addr i
= BV64.nth value (BV32.t'int len - i - 1 + BV32.t'int start))
/\
(forall i:int. BV32.t'int start + BV32.t'int len <= i < 8 * length addr ->
nth8_stream addr i
= nth8_stream (old addr) i) }
=
if BV32.to_uint (BV32.u_add start len) > 8 * length addr
then
-1 (*error: invalid_bit_sequence*)
else
if BV64.uge value (maxvalue len) (* should be len <> 64 && _..._ *)
then
-2 (*error: value_too_big*)
else
let lstart = BV32.u_sub (64:BV32.t) len in
let i = ref 0x0 in
while BV32.ult !i len do variant { BV32.t'int len - BV32.t'int !i }
invariant {0 <= BV32.t'int !i <= BV32.t'int len}
invariant {forall j:int. 0 <= j < BV32.t'int start ->
nth8_stream (old addr) j
= nth8_stream addr j}
invariant {forall j:int. BV32.t'int start <= j < BV32.t'int start + BV32.t'int !i ->
nth8_stream addr j
= BV64.nth value (BV32.t'int len - j - 1 + BV32.t'int start) }
invariant {forall j:int. BV32.t'int start + BV32.t'int !i <= j < 8 * length addr ->
nth8_stream addr j
= nth8_stream (old addr) j }
let flag = peek_64bit value (BV32.u_add lstart !i) in
poke_8bit_array addr (BV32.u_add start !i) flag;
assert {nth8_stream addr (BV32.t'int start + BV32.t'int !i)
= BV64.nth value ((BV32.t'int len - BV32.t'int !i - 1))};
assert { forall k. BV32.t'int start <= k < BV32.t'int start + BV32.t'int !i ->
k <> BV32.t'int start + BV32.t'int !i &&
0 <= k < 8 * length addr &&
nth8_stream addr k
= BV64.nth value (BV32.t'int start + BV32.t'int len - k - 1)};
i := BV32.u_add !i (1:BV32.t);
done;
0
let peekthenpoke (start len : BV32.t) (addr : array BV8.t)
requires {8 * length addr < BV32.two_power_size}
requires {0 <= BV32.t'int len < 64}
requires {BV32.t'int start + BV32.t'int len <= 8 * length addr}
ensures {result = 0}
ensures {forall i. 0 <= i < 8 * length addr ->
nth8_stream addr i = nth8_stream (old addr) i}
=
let value = peek start len addr in
let res = poke start len addr value in
assert {res = 0};
assert {forall i. BV32.t'int start <= i < BV32.t'int start + BV32.t'int len ->
nth8_stream addr i
= nth8_stream (old addr) i};
res
let pokethenpeek (start len : BV32.t) (addr : array BV8.t) (value : BV64.t)
writes {addr}
requires {8 * length addr < BV32.two_power_size}
requires {0 <= BV32.t'int len < 64}
requires {BV32.t'int start + BV32.t'int len <= 8 * length addr}
requires {BV64.t'int value < BV64.t'int (maxvalue len)}
ensures {result = value}
=
assert { forall i:int. BV32.t'int len <= i < 64 ->
BV64.nth value i = False };
let poke_result = poke start len addr value in
assert { poke_result = 0 };
let peek_result = peek start len addr in
assert { BV64.(==) peek_result value };
peek_result
end
Reference in New Issue View Git Blame Copy Permalink