Commit e1cb6b38 authored by Clément Fumex's avatar Clément Fumex
Browse files

new example: bitwalker (in progress)

parent ffa04f83
module Bitwalker
use import int.Int
use import int.EuclideanDivision
use import array.Array
use import ref.Ref
use import bv.BV32
use bv.BV8
use bv.BV64
use bv.BVConverter_32_64 as C32_64
use bv.BVConverter_8_32 as C8_32
function nth64_inv (value : BV64.t) (i : BV32.t) : bool =
BV64.nth_bv value (C32_64.toBig (sub (of_int 63) i))
function nth8_inv (value : BV8.t) (i : BV8.t) : bool =
BV8.nth_bv value (BV8.sub (BV8.of_int 7) i)
function nth8_inv_stream (stream : array BV8.t) (pos : BV32.t) : bool =
nth8_inv (stream[ to_uint (udiv pos (of_int 8)) ]) (C8_32.toSmall (urem pos (of_int 8)))
let poke_64bit (value : BV64.t) (left : BV32.t) (flag : BV32.t) =
requires{ ult left (of_int 64) }
ensures{ forall i. ult i (of_int 64) /\ i <> left ->
nth64_inv result i = nth64_inv value i }
ensures{ flag <> zero <-> nth64_inv result left }
let mask = BV64.lsl_bv (BV64.of_int 1) (C32_64.toBig (sub (of_int 63) left)) in
if( flag = zero )
then
BV64.bw_and value (BV64.bw_not mask)
else
BV64.bw_or value mask
let peek_8bit (byte : BV8.t) (left : BV32.t) =
requires{ ult left (of_int 8) }
ensures{ result <> BV8.zero <-> nth8_inv byte (C8_32.toSmall left) }
let mask = BV8.lsl_bv (BV8.of_int 1) (C8_32.toSmall (sub (of_int 7) left)) in
let flag = BV8.bw_and byte mask in
flag
let peek_8bit_array (addr : array BV8.t) (left : BV32.t) =
requires{ 8 * (length addr) < two_power_size }
requires{ to_uint left < 8 * length addr }
ensures{ result <> BV8.zero <-> nth8_inv_stream addr left }
peek_8bit (addr[ to_uint (udiv left (of_int 8)) ]) (urem left (of_int 8))
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{ 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)) }
if (to_uint (add start len) > ( 8 *length addr ))
then
BV64.zero
else
let retval = ref BV64.zero in
let i = ref zero in
assert { ult start (sub ones len)};
while ult !i len do
variant{ !i with ugt }
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}
assert {ult (add start !i) (add start len)};
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)};
i := add !i (of_int 1)
done;
!retval
end
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