Commit dbcf4f61 authored by Raphaël Rieu-Helft's avatar Raphaël Rieu-Helft

Add n by 1 division when divisor is normalized

parent fd8fccb5
......@@ -111,7 +111,11 @@ void lsld(uint32_t * low, uint32_t * high, uint32_t x, uint32_t cnt)
syntax val sub_mod "%1 - %2"
syntax val mul_mod "%1 * %2"
syntax val div2by1 "(uint32_t)(((uint64_t)%1 | ((uint64_t)%2 << 32))/(uint64_t)%3)"
syntax val div2by1
"(uint32_t)(((uint64_t)%1 | ((uint64_t)%2 << 32))/(uint64_t)%3)"
syntax val lsl "%1 << %2"
syntax val rsl "%1 >> %2"
end
......
......@@ -1584,15 +1584,6 @@ module N
};
(r,d)
val lsl (x cnt:limb) : limb
requires { 0 < l2i cnt < 32 }
ensures { l2i result =
(l2i x) * (mod (power 2 (l2i cnt)) radix) }
val lsr (x cnt:limb) : limb
requires { 0 < l2i cnt < 32 }
ensures { l2i result = div (l2i x) (power 2 (l2i cnt)) }
(** [lshift r x sz cnt] shifts [(x,sz)] [cnt] bits to the left and
writes the result in [(r, sz)]. Returns the [cnt] most significant
bits of [(x, sz)]. Corresponds to [mpn_lshift]. *)
......@@ -1637,7 +1628,7 @@ module N
let l,h = lsld_ext !low cnt in
assert { l2i !high + l2i h < radix };
let ghost v = Limb.(+) !high h in
value_sub_update_no_change (pelts r) (!rp).offset (r.offset + 1+ p2i !i)
value_sub_update_no_change (pelts r) (!rp).offset (r.offset + 1 + p2i !i)
(r.offset + p2i sz) v;
C.set !rp (Limb.(+) !high h);
rp := C.incr !rp minus_one;
......@@ -2145,31 +2136,122 @@ module N
assert { 0 <= l2i !r < l2i d };
assert { l2i !qh * l2i d + l2i !r = l2i ul + radix * l2i uh };
(!qh,!r)
(*
let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
let divmod_1_norm (q x:t) (y:limb) (sz:int32) : limb
requires { valid_ptr_itv x (p2i sz) }
requires { valid_ptr_itv r (p2i sz) }
requires { valid_ptr_itv q (p2i sz) }
requires { 0 < p2i sz }
ensures { value_sub_shift r sz
= div (value_sub_shift y sz) (l2i y) + l2i result }
requires { l2i y >= div radix 2 }
ensures { value_sub_shift x (p2i sz)
= value_sub_shift q (p2i sz) * l2i y + l2i result }
=
let v = invert_limb y in
let limb_zero = Limb.of_int 0 in
let zero = Int32.of_int 0 in
let one = Int32.of_int 1 in
let msb = Int32.(-) sz one in
let minus_one = Int32.(-_) (Int32.of_int 1) in
let lx = ref limb_zero in
let xp = ref (C.incr x msb) in
let qp = ref (C.incr q msb) in
let i = ref msb in
let r = ref limb_zero in
while (Int32.(>=) !i zero) do
variant { p2i !i }
xp := C.incr !xp minus_one;
qp := C.incr !qp minus_one;
let (q,rem) = div2by1_inv !r (C.get !xp) y v in
invariant { -1 <= p2i !i <= p2i msb }
invariant { (!qp).offset = q.offset + p2i !i }
invariant { (!xp).offset = x.offset + p2i !i }
invariant { plength !qp = plength q }
invariant { plength !xp = plength x }
invariant { pelts !qp = pelts q }
invariant { pelts !xp = pelts x }
invariant { l2i !r < l2i y }
invariant { value_sub (pelts x) (x.offset + p2i !i + 1) (x.offset + p2i sz)
= value_sub (pelts q) (q.offset + p2i !i + 1)
(q.offset + p2i sz)
* l2i y
+ l2i !r }
assert { p2i !i >= 0 };
label StartLoop in
let ghost k = p2i !i in
lx := C.get !xp;
let (qu,rem) = div2by1_inv !r !lx y v in
r:=rem;
C.set !qp q;
value_sub_update_no_change (pelts q) (!qp).offset (q.offset + 1 + p2i !i)
(q.offset + p2i sz) qu;
C.set !qp qu;
xp := C.incr !xp minus_one;
qp := C.incr !qp minus_one;
i := Int32.(-) !i one;
value_sub_head (pelts x) (x.offset + k) (x.offset + p2i sz);
value_sub_head (pelts q) (q.offset + k) (q.offset + p2i sz);
assert { value_sub (pelts x) (x.offset + p2i !i + 1) (x.offset + p2i sz)
= value_sub (pelts q) (q.offset + p2i !i + 1)
(q.offset + p2i sz)
* l2i y
+ l2i !r
by
l2i (pelts q)[q.offset + k] = l2i qu
so
l2i (pelts x)[x.offset + k] = l2i !lx
so
value_sub (pelts x) (x.offset + p2i !i + 1) (x.offset + p2i sz)
= value_sub (pelts x) (x.offset + k) (x.offset + p2i sz)
= l2i (pelts x)[x.offset + k]
+ radix * value_sub (pelts x) (x.offset + k + 1)
(x.offset + p2i sz)
= l2i !lx + radix * value_sub (pelts x) (x.offset + k + 1)
(x.offset + p2i sz)
= l2i !lx + radix *
(value_sub (pelts q) (q.offset + k + 1)
(q.offset + p2i sz)
* l2i y
+ l2i (!r at StartLoop))
= l2i !lx + radix * l2i (!r at StartLoop)
+ radix * (value_sub (pelts q) (q.offset + k + 1)
(q.offset + p2i sz)
* l2i y)
= l2i qu * l2i y + l2i !r
+ radix * value_sub (pelts q) (q.offset + k + 1)
(q.offset + p2i sz)
* l2i y
= l2i (pelts q)[q.offset + k] * l2i y + l2i !r
+ radix * value_sub (pelts q) (q.offset + k + 1)
(q.offset + p2i sz)
* l2i y
= l2i y * (l2i (pelts q)[q.offset + k]
+ radix * value_sub (pelts q) (q.offset + k + 1)
(q.offset + p2i sz))
+ l2i !r
= l2i y * value_sub (pelts q) (q.offset + p2i !i + 1)
(q.offset + p2i sz)
+ l2i !r
}
done;
!r
(*TODO normalize within main loop by counting leading zeros in a preceding loop*)
(*
let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
requires { valid_ptr_itv x (p2i sz) }
requires { valid_ptr_itv q (p2i sz) }
requires { 0 < p2i sz }
ensures { value_sub_shift x (p2i sz)
= value_sub_shift q (p2i sz) * l2i y + l2i result }
{
if is_msb_set y
then divmod_1_norm q x y sz
else
let uone = UInt32.of_int 1 in
let clz = ref (UInt32.of_int 0) in
let ry = ref y in
while (not (is_msb_set !ry)) do
ry := lsl !ry uone;
clz := UInt32.(+) !clz uone;
done;
let xn =
}
*)
(** Tests *)
......
......@@ -224,6 +224,16 @@ module UInt32
returns { (r,d) -> to_int r + (max_uint32+1) * to_int d =
(power 2 (to_int cnt)) * to_int x }
val lsl (x cnt:uint32) : uint32
requires { 0 < to_int cnt < 32 }
requires { (power 2 (to_int cnt)) * to_int x <= max_uint32 }
ensures { to_int result = (power 2 (to_int cnt)) * to_int x }
val rsl (x cnt:uint32) : uint32
requires { 0 < to_int cnt < 32 }
requires { to_int x >= power 2 (to_int cnt) || to_int x = 0 }
ensures { to_int x = (power 2 (to_int cnt)) * to_int result }
val div2by1 (l h d:uint32) : uint32
requires { to_int h < to_int d }
(* this pre implies d > 0 and also
......@@ -237,6 +247,10 @@ module UInt32
ensures { to_int result
= div (to_int l + (max_uint32+1) * to_int h) (to_int d) }
val is_msb_set (x:uint32) : bool
ensures { result <-> 2 * to_int x > max_uint32 }
(* use bv.BV32
val to_bv (x: uint32) : BV32.t
......
......@@ -656,6 +656,9 @@ module Translate = struct
| PDlet (LDsym (rs, ce)) ->
let fname = rs.rs_name in
Format.printf "PDlet rsymbol %s@." fname.id_string;
if rs_ghost rs
then begin Format.printf "is ghost@."; [] end
else
begin try
if Mid.mem fname info.syntax
then (Format.printf "has syntax@."; [])
......@@ -677,14 +680,18 @@ module Translate = struct
let is_simple_tuple ity =
let arity_zero = function
| Ityapp(_,a,r) -> a = [] && r = []
| Ityreg { reg_args = a; reg_regs = r } -> a = [] && r = []
| Ityreg { reg_args = a; reg_regs = r } ->
a = [] && r = []
| Ityvar _ -> true
in
(match ity.ity_node with
| Ityapp ({its_ts = s},_,_) | Ityreg { reg_its = {its_ts = s}; }
-> is_ts_tuple s
| Ityapp ({its_ts = s},_,_)
| Ityreg { reg_its = {its_ts = s}; }
-> is_ts_tuple s
| _ -> false)
&& (ity_fold (fun acc ity -> acc && arity_zero ity.ity_node) true ity)
&& (ity_fold
(fun acc ity ->
acc && arity_zero ity.ity_node) true ity)
in
(* FIXME is it necessary to have arity 0 in regions ?*)
let rtype =
......
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