Attention une mise à jour du serveur va être effectuée le lundi 17 mai entre 13h et 13h30. Cette mise à jour va générer une interruption du service de quelques minutes.

Commit b7787a01 authored by MARCHE Claude's avatar MARCHE Claude

fix examples using bitvectors

parent 9ec870c8
......@@ -7,14 +7,17 @@ module Test_proofinuse
(* Shift is div example ------------------- *)
let shift_is_div ( x : t ) ( y : t ) : t =
requires{ 0 <= t'int y < 32 }
let shift_is_div ( x : t ) ( y : t ) : t
requires { 0 <= t'int y < 32 }
=
let res = lsr_bv x one in
assert{ res = ( udiv x (2:t) ) };
assert{ t'int res = div (t'int x) 2 };
let res = lsr_bv res (2:t) in
assert{ res = ( udiv x (8:t) ) };
assert{ t'int res = div (t'int x) 8 };
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 --------------------- *)
......@@ -29,7 +32,7 @@ module Test_proofinuse
type bitvec64 = BV64.t
let mask ( x : t ) =
ensures{ BV8.eq result BV8.one }
ensures { result = BV8.one }
(* ensures{ not ( BV8.eq result (BV8.of_int 1) ) } *)
let res = C8_32.toSmall(
bw_and
......
......@@ -55,8 +55,8 @@ module Bitwalker
ensures { flag = BV64.nth_bv result
(C32_64.toBig (BV32.sub (BV32.of_int 63) left)) }
let mask =
BV64.lsl_bv (BV64.int_check 1)
(C32_64.toBig (BV32.sub_check (BV32.int_check 63) left))
BV64.lsl_bv (1:BV64.t)
(C32_64.toBig (BV32.sub_check (63:BV32.t) left))
in
match flag with
| True -> BV64.bw_or value mask
......@@ -83,7 +83,7 @@ module Bitwalker
BV64.nth_bv result i = BV64.nth_bv value i }
ensures { flag = BV64.nth_bv result (BV64.sub (BV64.of_int 63) left_bv) }
let mask =
BV64.lsl_bv (BV64.int_check 1) (BV64.of_int (63 - left))
BV64.lsl_bv (1:BV64.t) (BV64.of_int (63 - left))
in
match flag with
| True -> BV64.bw_or value mask
......@@ -105,7 +105,7 @@ module Bitwalker
result = BV8.nth_bv
byte (BV8.sub (BV8.of_int 7) (C8_32.toSmall left))}
let mask =
BV32.lsl_bv (BV32.int_check 1) (BV32.sub_check (BV32.int_check 7) left)
BV32.lsl_bv (1:BV32.t) (BV32.sub_check (7:BV32.t) left)
in
not (BV32.eq (BV32.bw_and (C8_32.toBig byte) mask) BV32.zeros)
end
......@@ -116,7 +116,7 @@ module Bitwalker
requires { BV32.t'int left < 8 * length addr }
ensures { result = nth8_stream addr (BV32.t'int left) }
=
peek_8bit_bv (addr[ BV32.t'int (BV32.udiv_check left (BV32.int_check 8)) ]) (BV32.urem_check left (BV32.int_check 8))
peek_8bit_bv (addr[ BV32.to_uint (BV32.udiv_check left (8:BV32.t)) ]) (BV32.urem_check 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] *)
......@@ -133,7 +133,7 @@ module Bitwalker
/\
(forall i:int. BV32.t'int len <= i < 64 -> BV64.nth result i = False) }
=
if (BV32.t'int (BV32.add_check start len) > ( 8 *length addr ))
if (BV32.to_uint (BV32.add_check start len) > ( 8 *length addr ))
then
BV64.zeros
else
......@@ -157,7 +157,7 @@ module Bitwalker
let flag = peek_8bit_array addr (BV32.add_check start !i) in
retval := poke_64bit_bv !retval (BV32.add_check lstart !i) flag;
i := BV32.add_check !i (BV32.int_check 1);
i := BV32.add_check !i (1:BV32.t);
done;
......@@ -171,8 +171,8 @@ module Bitwalker
begin
ensures {result = BV64.nth_bv value
(BV64.sub (BV64.of_int 63) (C32_64.toBig left))}
let mask = BV64.lsl_bv (BV64.int_check 1)
(C32_64.toBig (BV32.sub_check (BV32.int_check 63) left)) in
let mask = BV64.lsl_bv (1:BV64.t)
(C32_64.toBig (BV32.sub_check (63:BV32.t) left)) in
not (BV64.eq (BV64.bw_and value mask) BV64.zeros)
end
......@@ -200,7 +200,7 @@ module Bitwalker
= BV8.nth_bv byte (C8_32.toSmall i) }
ensures { BV8.nth_bv result (BV8.sub (BV8.of_int 7) (C8_32.toSmall left))
= flag }
let mask = BV8.lsl_bv (BV8.int_check 1) (BV8.sub_check (BV8.int_check 7) (C8_32.toSmall left)) in
let mask = BV8.lsl_bv (1:BV8.t) (BV8.sub_check (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)
......@@ -208,16 +208,16 @@ module Bitwalker
end
let poke_8bit_array (addr : array BV8.t) (left : BV32.t) (flag : bool)
writes {addr}
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.udiv_check left (BV32.int_check 8) in
let k = BV32.urem_check left (BV32.int_check 8) in
addr[BV32.t'int i] <- poke_8bit addr[BV32.t'int i] k flag
let i = BV32.udiv_check left (8:BV32.t) in
let k = BV32.urem_check 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)
writes { addr }
......@@ -241,7 +241,7 @@ module Bitwalker
nth8_stream addr i
= nth8_stream (old addr) i) }
=
if BV32.t'int (BV32.add_check start len) > 8 * length addr
if BV32.to_uint (BV32.add_check start len) > 8 * length addr
then
-1 (*error: invalid_bit_sequence*)
else
......@@ -279,7 +279,7 @@ module Bitwalker
nth8_stream addr k
= BV64.nth value (BV32.t'int start + BV32.t'int len - k - 1)};
i := BV32.add_check !i (BV32.int_check 1);
i := BV32.add_check !i (1:BV32.t);
done;
0
......
......@@ -40,7 +40,7 @@ module Fenwick
(* Get the i-th elements of the model. *)
function get (f:fenwick) (i:int) : int = f.t[i+f.leaves-1]
(* Get the sum of elements over range [a;b[ *)
function rget (f:fenwick) (a b:int) : int = sum a b (get f)
function rget (f:fenwick) (a b:int) : int = sum (get f) a b
(* Create a Fenwick tree initialized at 0 *)
let make (lv:int) : fenwick
......@@ -62,14 +62,14 @@ module Fenwick
f.t[!lc] <- f.t[!lc] + x;
(* Update node summaries for all elements on the path
from the updated leaf to the root. *)
'I:
label I in
while !lc <> 0 do
invariant { 0 <= !lc < f.t.length }
invariant { forall i. 0 <= i /\ i < f.leaves - 1 ->
f.t[i] = f.t[2*i+1] + f.t[2*i+2] -
if 2*i+1 <= !lc <= 2*i+2 then x else 0 }
invariant { forall i. f.leaves - 1 <= i < f.t.length ->
f.t[i] = (at f 'I).t[i] }
f.t[i] = (f at I).t[i] }
variant { !lc }
lc := div (!lc - 1) 2;
f.t[!lc] <- f.t[!lc] + x
......@@ -79,7 +79,7 @@ module Fenwick
let rec ghost sum_dec (a b c:int) : unit
requires { a <= b }
ensures { forall f g. (forall i. a <= i < b -> f i = g (i+c)) ->
sum a b f = sum (a+c) (b+c) g }
sum f a b = sum g (a+c) (b+c) }
variant { b - a }
= if a < b then sum_dec (a+1) b c
......@@ -89,7 +89,7 @@ module Fenwick
are exactly the childs of elements of range [a;b[. *)
let rec ghost fen_compact (f:fenwick) (a b:int) : unit
requires { 0 <= a <= b /\ 2 * b < f.t.length /\ valid f }
ensures { sum a b (A.get f.t) = sum (2*a+1) (2*b+1) (A.get f.t) }
ensures { sum (A.([]) f.t) a b = sum (A.([]) f.t) (2*a+1) (2*b+1) }
variant { b - a }
= if a < b then fen_compact f (a+1) b
......@@ -106,7 +106,7 @@ module Fenwick
and use compaction lemma to halve interval size. *)
while !ra <> !rb do
invariant { 0 <= !ra <= !rb <= f.t.length }
invariant { !acc + sum !ra !rb (A.get f.t) = rget f a b }
invariant { !acc + sum (A.([]) f.t) !ra !rb = rget f a b }
variant { !rb - !ra }
if mod !ra 2 = 0 then acc := !acc + f.t[!ra];
ra := div !ra 2;
......
......@@ -10,9 +10,9 @@ theory Utils
use import bv.BV32
let constant one : t = (1:bool)
let constant one : t = (1:t)
let constant two : t = (2:t)
let constant lastbit : t = sub size_bv one
let constant lastbit : t = (31:t)
function max (x y : t) : t = (if ult x y then y else x)
function min (x y : t) : t = (if ult x y then x else y)
......
......@@ -30,11 +30,6 @@ module BVCheck_Gen
predicate uge t t
predicate ugt t t
val int_check (a:int) : t
requires { 0 <= a < two_power_size }
ensures { to_uint result = a }
ensures { result = of_int a }
val add_check (a b:t) : t
requires { 0 <= to_uint a + to_uint b < two_power_size }
ensures { to_uint result = to_uint a + to_uint b }
......
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