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

Fix extraction bug and clz builtin for 64bit

parent ad7cd706
......@@ -52,35 +52,35 @@ module mach.int.UInt32
"
#define LOW_MASK 0x00000000FFFFFFFFULL
void add_with_carry(uint32_t * res, uint32_t * carry, uint32_t x, uint32_t y, uint32_t c)
void add32_with_carry(uint32_t * res, uint32_t * carry, uint32_t x, uint32_t y, uint32_t c)
{
uint64_t r = (uint64_t)x + (uint64_t)y + (uint64_t) c;
*res = (uint32_t)(r & LOW_MASK);
*carry = (uint32_t)(r >> 32);
}
void sub_with_borrow(uint32_t * res, uint32_t * borrow, uint32_t x, uint32_t y, uint32_t b)
void sub32_with_borrow(uint32_t * res, uint32_t * borrow, uint32_t x, uint32_t y, uint32_t b)
{
uint64_t r = (uint64_t)x - (uint64_t)y - (uint64_t) b;
*res = (uint32_t)(r & LOW_MASK);
*borrow = (uint32_t)(r >> 63);
}
void mul_double(uint32_t * low, uint32_t * high, uint32_t x, uint32_t y)
void mul32_double(uint32_t * low, uint32_t * high, uint32_t x, uint32_t y)
{
uint64_t r = (uint64_t)x * (uint64_t)y;
*low = (uint32_t)(r & LOW_MASK);
*high = (uint32_t)(r >> 32);
}
void add3(uint32_t * low, uint32_t * high, uint32_t x, uint32_t y, uint32_t z)
void add32_3(uint32_t * low, uint32_t * high, uint32_t x, uint32_t y, uint32_t z)
{
uint64_t r = (uint64_t)x + (uint64_t)y + (uint64_t) z;
*low = (uint32_t)(r & LOW_MASK);
*high = (uint32_t)(r >> 32);
}
void lsld(uint32_t * low, uint32_t * high, uint32_t x, uint32_t cnt)
void lsld32(uint32_t * low, uint32_t * high, uint32_t x, uint32_t cnt)
{
uint64_t r = (uint64_t)x << cnt;
*low = (uint32_t)(r & LOW_MASK);
......@@ -93,6 +93,13 @@ void lsld(uint32_t * low, uint32_t * high, uint32_t x, uint32_t cnt)
syntax type uint32 "uint32_t"
syntax converter max_uint32 "0xffffffff"
syntax converter length "32"
syntax val add_with_carry "add32_with_carry"
syntax val sub_with_borrow "sub32_with_borrow"
syntax val mul_double "mul32_double"
syntax val add3 "add32_3"
syntax val lsld "lsld32"
syntax val (+) "%1 + %2"
syntax val (-) "%1 - %2"
......@@ -121,6 +128,9 @@ void lsld(uint32_t * low, uint32_t * high, uint32_t x, uint32_t cnt)
syntax val count_leading_zeros "__builtin_clz(%1)"
syntax val of_int32 "(uint32_t)%1"
end
module mach.int.UInt64
......@@ -128,7 +138,7 @@ module mach.int.UInt64
prelude
"
void add_with_carry(uint64_t * res, uint64_t * carry, uint64_t x, uint64_t y, uint64_t c)
void add64_with_carry(uint64_t * res, uint64_t * carry, uint64_t x, uint64_t y, uint64_t c)
{
uint64_t r = x + y + c;
*res = r;
......@@ -136,7 +146,7 @@ void add_with_carry(uint64_t * res, uint64_t * carry, uint64_t x, uint64_t y, ui
else *carry = ((r == x) && c);
}
void sub_with_borrow(uint64_t * res, uint64_t * borrow, uint64_t x, uint64_t y, uint64_t b)
void sub64_with_borrow(uint64_t * res, uint64_t * borrow, uint64_t x, uint64_t y, uint64_t b)
{
uint64_t r = x - y - b;
*res = r;
......@@ -144,24 +154,31 @@ void sub_with_borrow(uint64_t * res, uint64_t * borrow, uint64_t x, uint64_t y,
else *borrow = ((r == x) && b);
}
void mul_double(uint64_t * low, uint64_t * high, uint64_t x, uint64_t y)
void mul64_double(uint64_t * low, uint64_t * high, uint64_t x, uint64_t y)
{
uint64_t h, l;
asm(\"mulq %3\" : \"=a\"(l),\"=d\"(h) : \"a\"(x), \"g\"(y));
asm(\"mulq %3\" : \"=a\"(l),\"=d\"(h) : \"a\"(x), \"rm\"(y));
*high = h;
*low = l;
}
void add3(uint64_t * low, uint64_t * high, uint64_t x, uint64_t y, uint64_t z)
uint64_t div64_2by1(uint64_t ul, uint64_t uh, uint64_t d)
{
uint64_t q,r;
asm(\"divq %4\" : \"=a\"(q),\"=d\"(r) : \"a\"(ul), \"d\"(uh), \"rm\"(d));
return q;
}
void add64_3(uint64_t * low, uint64_t * high, uint64_t x, uint64_t y, uint64_t z)
{
uint64_t r, c1, c2;
add_with_carry(&r, &c1, x, y, 0);
add_with_carry(&r, &c2, r, z, 0);
add64_with_carry(&r, &c1, x, y, 0);
add64_with_carry(&r, &c2, r, z, 0);
*high = c1 + c2;
*low = r;
}
void lsld(uint64_t * low, uint64_t * high, uint64_t x, uint64_t cnt)
void lsld64(uint64_t * low, uint64_t * high, uint64_t x, uint64_t cnt)
{
*high = x >> (64 - cnt);
*low = x << cnt;
......@@ -173,6 +190,14 @@ void lsld(uint64_t * low, uint64_t * high, uint64_t x, uint64_t cnt)
syntax type uint64 "uint64_t"
syntax converter max_uint64 "0xffffffffffffffff"
syntax converter length "64"
syntax val add_with_carry "add64_with_carry"
syntax val sub_with_borrow "sub64_with_borrow"
syntax val mul_double "mul64_double"
syntax val div2by1 "div64_2by1"
syntax val add3 "add64_3"
syntax val lsld "lsld64"
syntax val (+) "%1 + %2"
syntax val (-) "%1 - %2"
......@@ -191,15 +216,14 @@ void lsld(uint64_t * low, uint64_t * high, uint64_t x, uint64_t cnt)
syntax val sub_mod "%1 - %2"
syntax val mul_mod "%1 * %2"
syntax val div2by1
"0"
syntax val lsl "%1 << %2"
syntax val lsr "%1 >> %2"
syntax val is_msb_set "%1 & 0x8000000000000000ULL"
syntax val count_leading_zeros "__builtin_clz(%1)"
syntax val count_leading_zeros "__builtin_clzll(%1)"
syntax val of_int32 "(uint64_t)%1"
end
......
......@@ -3077,7 +3077,8 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
(* [(x,sz)] is normalized if its most significant bit is set. *)
predicate normalized (x:t) (sz:int32) =
valid_ptr_itv x (p2i sz) /\ l2i (pelts x)[p2i sz - 1] >= div radix 2
valid_ptr_itv x (p2i sz)
/\ l2i (pelts x)[x.offset + p2i sz - 1] >= div radix 2
let div_sb_qr (q x y:t) (sx sy:int32) : unit
requires { 2 <= p2i sy <= p2i sx }
......@@ -3102,39 +3103,47 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
let x1 = ref (C.get_ofs !xp one) in
let i = ref (Int32.(-) sx sy) in
let mdn = Int32.(-) two sy in
let q = ref limb_zero in
let ql = ref limb_zero in
while (Int32.(>) !i zero) do
variant { p2i !i }
invariant { 0 <= p2i !i <= p2i sx - p2i sy }
invariant { (!qp).offset = q.offset + p2i !i }
invariant { (!xp).offset = x.offset + p2i sy + p2i !i - 2 }
invariant { plength !qp = plength q }
invariant { plength !xp = plength x }
invariant { pelts !qp = pelts q }
invariant { pelts !xp = pelts x }
xp := C.incr !xp minus_one;
if (Limb.(=) !x1 dh && Limb.(=) (C.get_ofs !xp one) dl) (* unlikely *)
then begin
q := Limb.of_int Limb.max_uint64;
let _ = submul_limb (C.incr !xp mdn) y !q sy in
ql := Limb.of_int Limb.max_uint64;
let _ = submul_limb (C.incr !xp mdn) y !ql sy in
x1 := C.get_ofs !xp one
end
else begin
let qu, rh, rl =
div3by2_inv !x1 (C.get_ofs !xp one) (C.get !xp) dh dl v in
q := qu;
ql := qu;
x1 := rh;
x0 := rl;
(* TODO use sy-2 and use the existing x0 and x1 for the last two steps*)
let cy = submul_limb (C.incr !xp mdn) y !q sy in
let cy = submul_limb (C.incr !xp mdn) y !ql sy in
(* let cy1 = if (Limb.(<) !x0 cy) then uone else uzero in
x0 := sub_mod !x0 cy;
let cy2 = if (Limb.(<) !x1 cy1) then uone else uzero in
x1 := sub_mod !x1 cy2;
C.set !xp !x0;*)
x1 := sub_mod !x1 cy2;*)
C.set !xp !x0;
if Limb.ne cy limb_zero (*unlikely*)
then begin
(* TODO should be a simple add in place *)
let c = addmul_limb (C.incr !xp mdn) y uone sy in
x1 := Limb.(+) !x1 (Limb.(+) dh c);
q := Limb.(-) !q uone;
ql := Limb.(-) !ql uone;
end;
end;
qp := C.incr !qp minus_one;
C.set !qp !q
C.set !qp !ql;
i := Int32.(-) !i one;
done;
C.set_ofs !xp one !x1
......@@ -3172,7 +3181,7 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
else begin
let nx = malloc (UInt32.of_int32 (Int32.(+) sx one)) in
let ny = malloc (UInt32.of_int32 sy) in
let _ = lshift ny y sy (Limb.of_int32 clz) in
let _c = lshift ny y sy (Limb.of_int32 clz) in
let h = lshift nx x sx (Limb.of_int32 clz) in
C.set_ofs nx sx h;
(* TODO don't add 1 when not needed, cf "adjust" in GMP algo *)
......
#include <gmp.h>
#include <stdint.h>
#include <stdio.h>
#include <stdlib.h>
uint64_t add(uint64_t * r3, uint64_t * x4, uint64_t * y3, int32_t sx, int32_t
sy);
void mul(uint64_t * r10, uint64_t * x11, uint64_t * y10, int32_t sx2, int32_t
sy2);
void div_qr(uint64_t * q, uint64_t * r, uint64_t * x, uint64_t * y, int32_t sx, int32_t sy);
#define TMP_ALLOC_LIMBS(n) malloc((n) * 8)
void mpn_dump(mp_ptr ap, mp_size_t an) {
for (mp_size_t i = 0; i != an; ++i)
printf("%016lx ", ap[i]);
printf("\n");
}
#if defined(TEST_GMP) || defined(TEST_WHY3)
#define BENCH
#else
#define COMPARE
#define TEST_GMP
#define TEST_WHY3
#endif
int main () {
mp_ptr ap, bp, rp, refp, rq, rr, refq, refr;
mp_size_t max_n, an, bn, rn;
//gmp_randstate_t rands;
//TMP_DECL;
//TMP_MARK;
//tests_start ();
//TESTS_REPS (reps, argv, argc);
//gmp_randinit_default(rands);
//gmp_randseed_ui(rands, 42);
/* Re-interpret reps argument as a size argument. */
max_n = 20;
ap = TMP_ALLOC_LIMBS (max_n + 1);
bp = TMP_ALLOC_LIMBS (max_n + 1);
rp = TMP_ALLOC_LIMBS (2 * max_n);
refp = TMP_ALLOC_LIMBS (2 * max_n);
rq = TMP_ALLOC_LIMBS (max_n + 1);
rr = TMP_ALLOC_LIMBS (max_n + 1);
refq = TMP_ALLOC_LIMBS (max_n + 1);
refr = TMP_ALLOC_LIMBS (max_n + 1);
for (an = 1; an <= max_n; an += 1)
{
for (bn = 1; bn <= an; bn += 1)
{
mpn_random2 (ap, an + 1);
mpn_random2 (bp, bn + 1);
#ifdef BENCH
for (int iter = 0; iter != 10000; ++iter) {
#endif
#ifdef TEST_GMP
mpn_mul (refp, ap, an, bp, bn);
mpn_tdiv_qr (refq, refr, 0, ap, an, bp, bn);
#endif
#ifdef TEST_WHY3
mul (rp, ap, bp, an, bn);
div_qr(rq, rr, ap, bp, an, bn);
#endif
#ifdef BENCH
}
#endif
#ifdef COMPARE
rn = an + bn;
if (mpn_cmp (refp, rp, rn))
{
printf ("ERROR, an = %d, bn = %d, rn = %d\n",
(int) an, (int) bn, (int) rn);
printf ("a: "); mpn_dump (ap, an);
printf ("b: "); mpn_dump (bp, bn);
printf ("r: "); mpn_dump (rp, rn);
printf ("ref: "); mpn_dump (refp, rn);
abort();
}
rn = bn;
if (mpn_cmp (refr, rr, rn))
{
printf ("ERROR, an = %d, bn = %d, rn = %d\n",
(int) an, (int) bn, (int) rn);
printf ("a: "); mpn_dump (ap, an);
printf ("b: "); mpn_dump (bp, bn);
printf ("r: "); mpn_dump (rr, rn);
printf ("ref: "); mpn_dump (refr, rn);
abort();
}
rn = an - bn + 1;
if (mpn_cmp (refq, rq, rn))
{
printf ("ERROR, an = %d, bn = %d, rn = %d\n",
(int) an, (int) bn, (int) rn);
printf ("a: "); mpn_dump (ap, an);
printf ("b: "); mpn_dump (bp, bn);
printf ("r: "); mpn_dump (rr, rn);
printf ("ref: "); mpn_dump (refr, rn);
abort();
}
#endif
}
}
//TMP_FREE;
//tests_end ();
return 0;
}
......@@ -499,23 +499,38 @@ module Translate = struct
match
(query_syntax info.syntax rs.rs_name,
query_syntax info.converter rs.rs_name) with
| _, Some s
| Some s, _ ->
let params =
List.map (fun pv -> (C.Evar(pv_name pv),
ty_of_ty info (ty_of_ity pv.pv_ity)))
pvsl in
let rty = ty_of_ity e.e_ity in
let rtyargs = match rty.ty_node with
| Tyvar _ -> [||]
| Tyapp (_,args) ->
Array.of_list (List.map (ty_of_ty info) args)
in
C.Esyntax(s,ty_of_ty info rty, rtyargs, params,
Mid.mem rs.rs_name info.converter)
| None, None ->
let args = List.filter
begin
try
let _ = Str.search_forward
(Str.regexp "[%]\\([tv]?\\)[0-9]+") s 0 in
let params =
List.map (fun pv -> (C.Evar(pv_name pv),
ty_of_ty info (ty_of_ity pv.pv_ity)))
pvsl in
let rty = ty_of_ity e.e_ity in
let rtyargs = match rty.ty_node with
| Tyvar _ -> [||]
| Tyapp (_,args) ->
Array.of_list (List.map (ty_of_ty info) args)
in
C.Esyntax(s,ty_of_ty info rty, rtyargs, params,
Mid.mem rs.rs_name info.converter)
with Not_found ->
let args = List.filter
(fun pv -> not (pv.pv_ghost
|| ity_equal pv.pv_ity ity_unit))
pvsl in
if pvsl=[]
then C.(Esyntax(s, Tnosyntax, [||], [], true)) (*constant*)
else
(*function defined in the prelude *)
C.(Ecall(Esyntax(s, Tnosyntax, [||], [], true),
List.map (fun pv -> Evar(pv_name pv)) args))
end
| _ ->
let args = List.filter
(fun pv -> not (pv.pv_ghost
|| ity_equal pv.pv_ity ity_unit))
pvsl in
......@@ -536,8 +551,11 @@ module Translate = struct
begin match ld with
| LDvar (pv,le) ->
Format.printf "let %s@." pv.pv_vs.vs_name.id_string;
if pv.pv_ghost then expr info env e
if pv.pv_ghost
(*TODO check it's actually unused *)
then expr info env e
else if ity_equal pv.pv_ity ity_unit
|| pv.pv_vs.vs_name.id_string.[0] = '_'
then let env' = {env with computes_return_value = false} in
([], C.Sseq (C.Sblock(expr info env' le),
C.Sblock(expr info env e)))
......@@ -657,8 +675,9 @@ module Translate = struct
| _ -> assert false )
rets ([], []) in
let d,s = expr info {env with computes_return_value = false} e1 in
let s' = C.add_to_last_call rets s in
let b = expr info env e2 in
d@defs, C.(Sseq(add_to_last_call rets s, Sblock b))
d@defs, C.(Sseq(s', Sblock b))
| Ecase _ -> raise (Unsupported "pattern matching")
| Eghost _ | Epure _ | Eabsurd -> assert false
......
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