Commit dfd0187f authored by Clément Fumex's avatar Clément Fumex

progress on bitwalker example

parent e7a6c4dc
......@@ -47,14 +47,15 @@ module Bitwalker
let peek (start : BV32.t) (len : BV32.t) (addr : array BV8.t) =
(* requires \valid_read(addr + (0..size-1)); *) (* ?? *)
requires{ ule len (of_int 64) }
requires{ to_uint( start ) + to_uint( len ) < two_power_size }
requires{ to_uint start + to_uint len < two_power_size }
requires{ 8 * length addr < two_power_size }
ensures{ to_uint (add start len) > (8 * length addr) -> result = BV64.zero }
ensures{ to_uint (add start len) <= (8 * length addr) -> forall i. ult i len ->
nth8_inv_stream addr (add start i) <-> nth64_inv result (add (sub (of_int 64) len) i) }
ensures{ to_uint (add start len) <= (8 * length addr) -> forall i. ult i (sub (of_int 64) len) ->
nth64_inv result i = False }
ensures{ to_uint (add start len) <= (8 * length addr) -> BV64.ult result (BV64.lsl_bv (BV64.of_int 1) (C32_64.toBig len)) }
nth64_inv result i = False }
(* ensures{ to_uint (add start len) <= (8 * length addr) -> *)
(* BV64.ult result (BV64.lsl_bv (BV64.of_int 1) (C32_64.toBig len)) } *)
if (to_uint (add start len) > ( 8 *length addr ))
then
......@@ -64,6 +65,8 @@ module Bitwalker
let retval = ref BV64.zero in
let i = ref zero in
let lstart = sub (of_int 64) len in
assert { ult start (sub ones len)};
while ult !i len do
......@@ -71,15 +74,29 @@ module Bitwalker
invariant {ugt !i zero ->
nth8_inv_stream addr (add start (sub !i (of_int 1)))
<-> nth64_inv !retval (add (sub (of_int 64) len) (sub !i (of_int 1)))}
invariant {forall j. ult j !i -> nth8_inv_stream addr (add start j) <-> nth64_inv !retval (add (sub (of_int 64) len) j)}
invariant {forall j. ult j (sub (of_int 64) len) -> nth64_inv !retval j = False}
<-> nth64_inv !retval (add lstart (sub !i (of_int 1)))}
invariant {forall j. ult j !i->
nth8_inv_stream addr (add start j) <-> nth64_inv !retval (add lstart j)}
invariant {forall j. ult j lstart -> nth64_inv !retval j = False}
assert {ult (add start !i) (add start len)};
assert {ult (add lstart !i) (of_int 64)};
assert {forall j. ult j !i -> (add lstart j) <> (add lstart !i) };
let flag = peek_8bit_array addr (add start !i) in
retval := poke_64bit !retval (add (sub (of_int 64) len) !i) (C8_32.toBig flag);
assert {nth8_inv_stream addr (add start !i) <-> nth64_inv !retval (add (sub (of_int 64) len) !i)};
let temp = poke_64bit !retval (add lstart !i) (C8_32.toBig flag) in
assert {forall j. ult j !i -> ult (add lstart j) (of_int 64)};
assert {forall j. ult j !i -> nth64_inv !retval (add lstart j) <-> nth64_inv temp (add lstart j)};
retval := temp;
assert {forall j. ult j !i -> nth8_inv_stream addr (add start j) <-> nth64_inv !retval (add lstart j)};
assert {nth8_inv_stream addr (add start !i) <-> nth64_inv !retval (add lstart !i)};
assert {forall j. ult j (add !i (of_int 1)) -> ult j !i \/ j = !i};
i := add !i (of_int 1)
done;
!retval
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment