Commit d79732e4 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

Experiment with a variant of bitwalker example

parent 101b1f51
......@@ -55,6 +55,9 @@ theory bv.BV64
syntax function nth_bv
"(not (= (bvand (bvlshr %1 %2) (_ bv1 64)) (_ bv0 64)))"
(* possible alternative definition :
"(= ((_ extract 0 0) (bvlshr %1 %2)) (_ bv1 1))"
*)
syntax function rotate_left "(bvor (bvshl %1 (bvurem %2 (_ bv64 64))) (bvlshr %1 (bvsub (_ bv64 64) (bvurem %2 (_ bv64 64)))))"
syntax function rotate_right "(bvor (bvlshr %1 (bvurem %2 (_ bv64 64))) (bvshl %1 (bvsub (_ bv64 64) (bvurem %2 (_ bv64 64)))))"
......
module Bitwalker
use import int.Int
use import int.EuclideanDivision
use import array.Array
use import ref.Ref
use bv.BV32
use bv.BV8
use bv.BV64
use bv.BVConverter_32_64 as C32_64
use bv.BVConverter_8_32 as C8_32
val int8_check (a:int) : BV8.t
requires { 0 <= a < BV8.two_power_size }
ensures { BV8.to_uint result = a }
ensures { result = BV8.of_int a }
val int32_check (a:int) : BV32.t
requires { 0 <= a < BV32.two_power_size }
ensures { BV32.to_uint result = a }
ensures { result = BV32.of_int a }
val int64_check (a:int) : BV64.t
requires { 0 <= a < BV64.two_power_size }
ensures { BV64.to_uint result = a }
ensures { result = BV64.of_int a }
val add32_check (a b:BV32.t) : BV32.t
requires { 0 <= BV32.to_uint a + BV32.to_uint b < BV32.two_power_size }
ensures { BV32.to_uint result = BV32.to_uint a + BV32.to_uint b }
ensures { result = BV32.add a b }
val sub32_check (a b:BV32.t) : BV32.t
requires { 0 <= BV32.to_uint a - BV32.to_uint b < BV32.two_power_size }
ensures { BV32.to_uint result = BV32.to_uint a - BV32.to_uint b }
ensures { result = BV32.sub a b }
(*
predicate nth64_inv (value : BV64.t) (i : int) =
BV64.nth value (63 - i)
predicate nth8_inv (value : BV8.t) (i : int) =
BV8.nth value (7 - i)
*)
predicate nth8_stream (stream : array BV8.t) (pos : int) =
BV8.nth stream[div pos 8] (7 - mod pos 8)
(*
predicate nth64_inv_bv (value : BV64.t) (i : BV32.t) =
BV64.nth_bv value (BV64.sub (BV64.of_int 63) (C32_64.toBig i))
predicate nth8_inv_bv (value : BV8.t) (i : BV32.t) =
BV8.nth_bv value (BV8.sub (BV8.of_int 7) (C8_32.toSmall i))
*)
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 = nth8_inv_bv value (of_int i)
*)
(** 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)
requires { 0 <= BV32.to_uint left < 64 }
ensures { forall i. 0 <= i < 64 /\ i <> 63 - BV32.to_uint left ->
BV64.nth result i = BV64.nth value i }
ensures { flag = BV64.nth result (63 - BV32.to_uint left) }
=
abstract
ensures { forall i:BV32.t. i <> BV32.sub (BV32.of_int 63) 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 (BV32.of_int 63) left)) }
let mask =
BV64.lsl_bv (int64_check 1)
(C32_64.toBig (sub32_check (int32_check 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)
requires { 0 <= BV32.to_uint left < 8 }
ensures { result = BV8.nth byte (7 - BV32.to_uint left) }
=
abstract
ensures {
result = BV32.nth_bv
(C8_32.toBig byte) (BV32.sub (BV32.of_int 7) left)
}
let mask =
BV32.lsl_bv (int32_check 1) (sub32_check (int32_check 7) left)
in
BV32.bw_and (C8_32.toBig byte) mask <> BV32.zero
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)
requires{ 8 * (length addr) < two_power_size }
requires{ to_uint left < 8 * length addr }
ensures{ result = nth8_inv_stream addr (to_uint left) }
=
let ret = peek_8bit_bv (addr[ to_uint (udiv left (of_int 8)) ]) (urem left (of_int 8)) in
ret
(* 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{ 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:int. 0 <= i < 64 -> BV64.nth result i =
(if i < to_uint len then
nth8_inv_stream addr (to_uint start + to_uint len - i - 1)
else false)}
(* ensures{ to_uint (add start len) <= (8 * length addr) -> forall i. ult i len -> *)
(* nth8_inv_stream addr (to_uint (add start i)) *)
(* = nth64_inv result (to_uint (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) -> *)
(* len = (of_int 64) *)
(* \/ BV64.ult result (BV64.lsl_bv (BV64.of_int 1) (C32_64.toBig len)) } *)
=
if (to_uint (add_check start len) > ( 8 *length addr ))
then
BV64.zero
else
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 variant{ !i with ugt }
invariant {0 <= to_uint !i <= to_uint len}
invariant {forall j:int. to_uint len - to_uint !i <= j < to_uint len ->
BV64.nth !retval j
= nth8_inv_stream addr (to_uint start + to_uint len - j - 1)}
invariant {forall j:int. 0 <= j < to_uint len - to_uint !i ->
BV64.nth !retval j
= False}
invariant {forall j:int. to_uint len <= j < 64 ->
BV64.nth !retval j
= False}
(* invariant {forall j:int. 0 <= j < to_uint lstart -> *)
(* nth64_inv !retval j *)
(* = False} *)
(* 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 {to_uint start + to_uint !i < to_uint start + to_uint len}; *)
(* assert {to_uint (add start !i) = to_uint start + to_uint !i}; *)
(* assert {forall j. ult j !i -> (add lstart j) <> (add lstart !i)}; *)
assert {forall j:int. to_uint len <= j < 64 -> j <> to_uint lstart + to_uint !i};
let flag = peek_8bit_array addr (add_check start !i) in
retval := poke_64bit_bv !retval (add_check lstart !i) flag;
(* assert {nth8_inv_stream addr (to_uint start + to_uint !i) *)
(* = flag}; *)
(* assert {let j = to_uint len - to_uint !i - 1 in *)
(* BV64.nth !retval j *)
(* = nth8_inv_stream addr (to_uint start + to_uint !i)}; *)
(* assert {forall j:int. j < to_uint !i + 1 -> j < to_uint !i \/ j = to_uint !i}; *)
i := add_check !i (of_int 1);
(* assert {let j = to_uint len - to_uint !i in *)
(* BV64.nth !retval j *)
(* = nth8_inv_stream addr (to_uint start + to_uint len - j -1)}; *)
(* assert {forall j:int. to_uint len - to_uint !i < j < to_uint len -> *)
(* BV64.nth !retval j *)
(* = nth8_inv_stream addr (to_uint start + to_uint len - j - 1)} *)
done;
(* missing an axiom in the sens of the following in the theory ? *)
(* axiom nth_mask: forall l b j. ule l size -> ult j l -> *)
(* nth b (sub size j) = False -> *)
(* bw_and (lsl_bv ones (sub size l)) b = zero}; *)
(* or even ? *)
(* axiom nth_mask: forall i m n v. ule m n -> ule n size -> ule m i /\ ult i n *)
(* -> nth_bv v i = False *)
(* <-> bw_and (bw_and (lsl_bv ones m) (lsr_bv ones (sub size n))) v = zero}; *)
(* assert {forall j b. ult j lstart -> nth64_inv b j = False -> *)
(* BV64.bw_and (BV64.lsl_bv BV64.ones (C32_64.toBig len)) b = BV64.zero}; *)
(* assert {forall v i. ult i (of_int 64) -> *)
(* BV64.nth_bv v (BV64.sub (BV64.of_int 63) (C32_64.toBig i)) = nth64_inv v i }; *)
(* assert {forall j b. BV64.uge j (C32_64.toBig len) -> BV64.ult j (BV64.of_int 64)-> BV64.nth_bv b j = False}; *)
(* assert {BV64.bw_and (BV64.lsl_bv BV64.ones (C32_64.toBig len)) !retval = BV64.zero}; *)
!retval
let peek_64bit (value : BV64.t) (left : BV32.t)
requires {ult left (of_int 64)}
ensures {result = nth64_inv value left}
=
let mask = BV64.lsl_bv (BV64.of_int 1) (C32_64.toBig (sub (of_int 63) left)) in
let flag = (BV64.bw_and value mask <> BV64.zero) in
flag
let poke_8bit (byte : BV8.t) (left : BV32.t) (flag : bool)
requires { ult left (of_int 8) }
ensures { forall i. i <> left ->
nth8_inv result i = nth8_inv byte i }
ensures { nth8_inv result left = flag }
=
let mask = BV8.lsl_bv (BV8.of_int 1) (BV8.sub (BV8.of_int 7) (C8_32.toSmall left)) in
if flag
then
BV8.bw_or byte mask
else
BV8.bw_and byte (BV8.bw_not mask)
let poke_8bit_array (addr : array BV8.t) (left : BV32.t) (flag : bool)
writes {addr}
requires { 8 * (length addr) < max_int }
requires { to_uint left < 8 * length addr }
ensures { forall i. i <> left ->
nth8_inv_stream addr i = nth8_inv_stream (old addr) i}
ensures { forall i. 0 <= i < 8 * length addr /\ i <> to_uint left ->
nth8_inv_stream addr (of_int i) = nth8_inv_stream (old addr) (of_int i) }
ensures { nth8_inv_stream addr left = flag }
=
'Init:
let i = div (to_uint left) 8 in
let k = urem left (of_int 8) in
addr[i] <- poke_8bit addr[i] k flag;
assert {forall j. div (to_uint j) 8 <> i \/ urem j (of_int 8) <> k <-> j <> left};
assert { forall j l. j <> i \/ l <> k ->
nth8_inv addr[j] l
= nth8_inv (at addr 'Init)[j] l }
function maxvalue (len : BV32.t) : BV64.t = BV64.lsl_bv (BV64.of_int 1) (C32_64.toBig len)
let poke (start : BV32.t) (len : BV32.t) (addr : array BV8.t) (value : BV64.t)
writes { addr }
requires{ ult 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 = -1 }
ensures { BV64.ule (maxvalue len) value /\ to_uint (add start len) <= 8 * length addr ->
result = -2 }
ensures { BV64.ugt (maxvalue len) value /\ to_uint (add start len) <= 8 * length addr ->
result = 0 }
ensures { BV64.ugt (maxvalue len) value /\ to_uint (add start len) <= 8 * length addr ->
forall i. ult i start ->
nth8_inv_stream (old addr) i
= nth8_inv_stream addr i }
ensures { BV64.ugt (maxvalue len) value /\ to_uint (add start len) <= 8 * length addr ->
forall i. ult i len ->
nth8_inv_stream addr (add start i)
= nth64_inv value (add (sub (of_int 64) len) i) }
ensures { BV64.ugt (maxvalue len) value /\ to_uint (add start len) <= 8 * length addr ->
forall i. ule (add start len) i /\ to_uint i < 8 * length addr ->
nth8_inv_stream addr i
= nth8_inv_stream (old addr) i }
=
if to_uint (add start len) > 8 * length addr
then
-1 (*error: invalid_bit_sequence*)
else
if BV64.uge value (maxvalue len)
then
-2 (*error: value_too_big*)
else
let lstart = sub (of_int 64) len in
let i = ref zero in
assert { ult start (sub ones len) };
'Init:
while ult !i len do variant { !i with ugt }
invariant {ule start (add start !i)}
invariant {ule (add start !i) (add start len)}
invariant {forall k. ult k start ->
nth8_inv_stream addr k
= nth8_inv_stream (at addr 'Init) k}
invariant {forall k. ult k !i ->
nth8_inv_stream addr (add start k)
= nth64_inv value (add lstart k)}
invariant {forall k. ule (add start !i) k /\ to_uint k < 8 * length addr ->
nth8_inv_stream addr k
= nth8_inv_stream (at addr 'Init) k}
assert {forall j. ult j !i -> (add lstart j) <> (add lstart !i)};
let flag = peek_64bit value (add lstart !i) in
poke_8bit_array addr (add start !i) flag;
assert {nth8_inv_stream addr (add start !i)
= nth64_inv value (add lstart !i)};
assert { forall k. ult k !i ->
nth8_inv_stream addr (add start k)
= nth64_inv value (add lstart k)};
assert {forall j. ult j (add !i (of_int 1)) -> ult j !i \/ j = !i};
i := add !i (of_int 1);
done;
0
let peekthenpoke (start len : BV32.t) (addr : array BV8.t)
requires {8 * length addr < two_power_size}
requires {ult len (of_int 64)}
requires {to_uint start + to_uint len <= 8 * length addr}
ensures {result = 0}
ensures {forall i. to_uint i < 8 * length addr ->
nth8_inv_stream addr i = nth8_inv_stream (old addr) i}
=
assert {to_uint (add start len) <= 8 * length addr};
'Init:
let value = peek start len addr in
let res = poke start len addr value in
assert {forall i. ult i len ->
nth8_inv_stream addr (add start i)
= nth8_inv_stream (at addr 'Init) (add start i)};
assert {forall i. ule start i /\ ult i (add start len) ->
ult (sub i start) len};
assert {forall i. ule start i /\ ult i (add start len) /\
(i = (add start (sub i start))) ->
nth8_inv_stream addr i
= nth8_inv_stream (at addr 'Init) i};
res
let pokethenpeek (start len : BV32.t) (addr : array BV8.t) (value : BV64.t)
writes {addr}
requires {8 * length addr < two_power_size}
requires {ult len (of_int 64)}
requires {to_uint start + to_uint len <= 8 * length addr}
requires {BV64.ult value (maxvalue len)}
ensures {result = value}
=
assert {to_uint (add start len) <= 8 * length addr};
let ghost lstart = sub (of_int 64) len in
let poke_result = poke start len addr value in
assert {poke_result = 0};
let peek_result = peek start len addr in
assert {forall i. ult i len ->
nth64_inv peek_result (add lstart i)
= nth64_inv value (add lstart i)};
assert {forall i. ule (sub (of_int 64) len) i /\ ult i (of_int 64) ->
ult (add i lstart) len};
assert {forall i. ule (sub (of_int 64) len) i /\ ult i (of_int 64) /\
i = (add lstart (sub i lstart)) ->
nth64_inv peek_result i
= nth64_inv value i};
assert {forall i. ult i (of_int 64) ->
nth64_inv peek_result i
= nth64_inv value i};
assert {
forall v w.
forall m n. ule m n /\ ule n size ->
(forall i. ule m i /\ ult i n -> nth_bv v i = nth_bv w i) ->
bw_and v (bw_and (lsl_bv ones m) (lsr_bv ones (sub size n)))
= bw_and w (bw_and (lsl_bv ones m) (lsr_bv ones (sub size n)))
};
assert {forall a b.
(forall i. nth_bv a (sub (of_int 31) i)
= nth_bv b (sub (of_int 31) i))
<->
(forall i. nth_bv a i = nth_bv b i)
};
assert {forall i. ult i (of_int 64) -> i = sub (of_int 63) (sub (of_int 63) i)};
assert {forall v i. BV64.ult i BV64.size ->
BV64.nth_bv v i = nth64_inv v (sub (of_int 63) (C32_64.toSmall i)) };
assert {forall i. BV64.ult i BV64.size ->
BV64.nth_bv peek_result i
= BV64.nth_bv value i};
assert {BV64.eq peek_result value};
peek_result
*****)
end
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="2" name="Z3" version="4.3.2" timelimit="5" memlimit="1000"/>
<file name="../bitwalker_abstract2.mlw" expanded="true">
<theory name="Bitwalker" sum="b7a131dcea083d6baada14c70d159dd0" expanded="true">
<goal name="nth64" expanded="true">
</goal>
<goal name="WP_parameter poke_64bit_bv" expl="VC for poke_64bit_bv" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter poke_64bit_bv.1" expl="1. precondition">
<proof prover="0"><result status="valid" time="0.03" steps="79"/></proof>
<proof prover="1"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter poke_64bit_bv.2" expl="2. precondition">
<proof prover="0"><result status="valid" time="0.03" steps="82"/></proof>
<proof prover="1"><result status="valid" time="0.03"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter poke_64bit_bv.3" expl="3. precondition">
<proof prover="0"><result status="valid" time="0.03" steps="85"/></proof>
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter poke_64bit_bv.4" expl="4. VC for poke_64bit_bv" expanded="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter poke_64bit_bv.5" expl="5. VC for poke_64bit_bv" expanded="true">
<proof prover="0"><result status="timeout" time="5.00"/></proof>
<proof prover="1" edited="bitwalker_abstract2-Bitwalker-WP_parameter_poke_64bit_bv_2.smt2" obsolete="true"><undone/></proof>
<proof prover="2"><result status="timeout" time="4.99"/></proof>
</goal>
<goal name="WP_parameter poke_64bit_bv.6" expl="6. VC for poke_64bit_bv" expanded="true">
<proof prover="2"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="WP_parameter poke_64bit_bv.7" expl="7. VC for poke_64bit_bv" expanded="true">
<proof prover="1" edited="bitwalker_abstract2-Bitwalker-WP_parameter_poke_64bit_bv_1.smt2"><result status="valid" time="0.05"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter poke_64bit_bv.8" expl="8. postcondition">
<proof prover="0"><result status="valid" time="0.77" steps="258"/></proof>
<proof prover="2"><result status="timeout" time="4.99"/></proof>
</goal>
<goal name="WP_parameter poke_64bit_bv.9" expl="9. postcondition" expanded="true">
<proof prover="0"><result status="valid" time="1.46" steps="621"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter peek_8bit_bv" expl="VC for peek_8bit_bv" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter peek_8bit_bv.1" expl="1. precondition">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter peek_8bit_bv.2" expl="2. precondition">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter peek_8bit_bv.3" expl="3. precondition">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter peek_8bit_bv.4" expl="4. VC for peek_8bit_bv">
<proof prover="1"><result status="valid" time="0.09"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter peek_8bit_bv.5" expl="5. postcondition" expanded="true">
<proof prover="0"><result status="timeout" time="5.00"/></proof>
<proof prover="1"><result status="timeout" time="5.03"/></proof>
<proof prover="2"><result status="timeout" time="4.99"/></proof>
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
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