Commit 2a35b574 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Merge branch 'whymp' into 'master'

Improvements to WhyMP

See merge request !381
parents 5f9ea672 064c6d90
......@@ -289,8 +289,8 @@ module mach.int.UInt64GMP
\n return result;\
\n}\
\n\
\nstruct __lsld64_result\
\n{ uint64_t __field_0;\
\nstruct __lsld64_result {\
\n uint64_t __field_0;\
\n uint64_t __field_1;\
\n};\
\n\
......
......@@ -12,10 +12,12 @@ else
endif
endif
ifdef GMP_DIR
CFLAGS = $(shell sed -n -e 's/^CFLAGS = \(.*\)/\1/p' $(GMP_DIR)/Makefile)
else
CFLAGS = -march=native -O2 -fomit-frame-pointer
ifndef CFLAGS
ifdef GMP_DIR
CFLAGS = $(shell sed -n -e 's/^CFLAGS = \(.*\)/\1/p' $(GMP_DIR)/Makefile)
else
CFLAGS = -march=native -O2 -fomit-frame-pointer
endif
endif
ifdef GMP_LIB
......@@ -73,25 +75,25 @@ no_INCLUDES =
INCLUDES = $($(OVERLAY)_INCLUDES)
build/libwmp.a: $(EXTRACTED)
cd build; gcc $(CFLAGS) $(INCLUDES:%=-include ../overlays/%) -c $(CFILES)
cd build; $(CC) $(CFLAGS) $(INCLUDES:%=-include ../overlays/%) -c $(CFILES)
ar rcs $@ $(addprefix build/,$(CFILES:.c=.o))
build/tests: tests.c build/libwmp.a
gcc $(CFLAGS) tests.c -Irandom -Lbuild -lm -lwmp -lgmp -o $@
$(CC) $(CFLAGS) tests.c -Irandom -Lbuild -lm -lwmp -lgmp -o $@
build/minitests: tests.c build/libwmp.a
gcc $(CFLAGS) -DCOMPARE_MINI tests.c -Irandom -Imini-gmp -Lbuild -lm -lwmp -o $@
$(CC) $(CFLAGS) -DCOMPARE_MINI tests.c -Irandom -Imini-gmp -Lbuild -lm -lwmp -o $@
UPPER = $(shell echo $* | tr [:lower:] [:upper:])
build/why3%bench: tests.c build/libwmp.a
gcc $(CFLAGS) -DTEST_WHY3 -DTEST_$(UPPER) tests.c -Iinclude -Irandom -Lbuild -lm -lwmp -lgmp -o $@
$(CC) $(CFLAGS) -DTEST_WHY3 -DTEST_$(UPPER) tests.c -Iinclude -Irandom -Lbuild -lm -lwmp -lgmp -o $@
build/gmp%bench: tests.c build/libwmp.a
gcc $(CFLAGS) $(GMPFLAGS) -DTEST_GMP -DTEST_$(UPPER) tests.c -Iinclude -Irandom -lm -lgmp -o $@
$(CC) $(CFLAGS) $(GMPFLAGS) -DTEST_GMP -DTEST_$(UPPER) tests.c -Iinclude -Irandom -lm -lgmp -o $@
build/minigmp%bench: tests.c build/libwmp.a
gcc $(CFLAGS) -DTEST_MINIGMP -DTEST_$(UPPER) tests.c -Iinclude -Imini-gmp -Irandom -lm -o $@
$(CC) $(CFLAGS) -DTEST_MINIGMP -DTEST_$(UPPER) tests.c -Iinclude -Imini-gmp -Irandom -lm -o $@
BENCHS = toomb sqrtrem millerrabin toomu add mul div powm toomm
......
......@@ -196,7 +196,7 @@ module Add
done;
c
let add_n (*[@extraction:inline]*) (r x y:ptr limb) (sz:int32) : limb
let add_n [@extraction:inline] (r x y:ptr limb) (sz:int32) : limb
requires { 0 <= sz }
requires { valid r sz /\ valid x sz /\ valid y sz }
requires { writable r }
......@@ -238,7 +238,7 @@ module Add
= (pelts oy)[offset y + j] };
res
let add_n_rx (*[@extraction:inline]*) (x y:ptr limb) (sz:int32) : limb
let add_n_rx [@extraction:inline] (x y:ptr limb) (sz:int32) : limb
requires { 0 <= sz }
requires { valid x sz /\ valid y sz }
requires { writable x }
......@@ -269,8 +269,7 @@ module Add
(int32'int sz);
res
let add (*[@extraction:inline]*) (r x:ptr limb) (sx:int32)
(y:ptr limb) (sy:int32) : limb
let add [@extraction:inline] (r x:ptr limb) (sx:int32) (y:ptr limb) (sy:int32) : limb
requires { 0 <= sy <= sx }
requires { valid r sx /\ valid x sx /\ valid y sy }
requires { writable r }
......@@ -312,8 +311,7 @@ module Add
= (pelts oy)[offset y + j] };
res
let add_rx (*[@extraction:inline]*) (x:ptr limb) (sx:int32)
(y:ptr limb) (sy:int32) : limb
let add_rx [@extraction:inline] (x:ptr limb) (sx:int32) (y:ptr limb) (sy:int32) : limb
requires { 0 <= sy <= sx }
requires { valid x sx /\ valid y sy }
requires { writable x }
......@@ -345,8 +343,7 @@ module Add
(offset y) (offset oy) (int32'int sy);
res
let add_ry (*[@extraction:inline]*) (x:ptr limb) (sx:int32)
(y:ptr limb) (sy:int32) : limb
let add_ry [@extraction:inline] (x:ptr limb) (sx:int32) (y:ptr limb) (sy:int32) : limb
requires { 0 <= sy <= sx }
requires { valid x sx /\ valid y sx }
requires { writable y }
......@@ -383,7 +380,7 @@ module Add
(offset x) (offset x) (int32'int sx);
res
let add_n_rxy (*[@extraction:inline]*) (x:ptr limb) (sx:int32) : limb
let add_n_rxy [@extraction:inline] (x:ptr limb) (sx:int32) : limb
requires { 0 <= sx }
requires { writable x }
requires { valid x sx }
......
#ifndef UINT64GMP_H_INCLUDED
#include <stdlib.h>
#include <stdint.h>
#include <stdio.h>
#include <assert.h>
#include <alloca.h>
typedef unsigned __int128 uint128_t;
struct __mul64_double_result
{ uint64_t __field_0;
uint64_t __field_1;
struct __mul64_double_result {
uint64_t __field_0;
uint64_t __field_1;
};
#define __builtin_expect(x,y) (x)
#define UWtype uint64_t
#define UHWtype uint32_t
......@@ -89,9 +84,9 @@ uint64_t __field_1;
static inline struct __mul64_double_result mul64_double(uint64_t x, uint64_t y)
{
struct __mul64_double_result result;
umul_ppmm (result.__field_1, result.__field_0, x, y);
return result;
struct __mul64_double_result result;
umul_ppmm (result.__field_1, result.__field_0, x, y);
return result;
}
static inline uint64_t div64_2by1(uint64_t ul, uint64_t uh, uint64_t d)
......@@ -99,72 +94,72 @@ static inline uint64_t div64_2by1(uint64_t ul, uint64_t uh, uint64_t d)
uint64_t q, r;
__udiv_qrnnd_c (q, r, uh, ul, d);
return q;
//return (((uint128_t)uh << 64) | ul) / d;
}
struct __add64_with_carry_result
{ uint64_t __field_0;
uint64_t __field_1;
struct __add64_with_carry_result {
uint64_t __field_0;
uint64_t __field_1;
};
static inline struct __add64_with_carry_result
add64_with_carry(uint64_t x, uint64_t y, uint64_t c)
{
struct __add64_with_carry_result result;
uint64_t r = x + y + c;
result.__field_0 = r;
if (r == x) result.__field_1 = c;
else result.__field_1 = (r < x);
return result;
struct __add64_with_carry_result result;
uint64_t r = x + y + c;
result.__field_0 = r;
if (r == x) result.__field_1 = c;
else result.__field_1 = (r < x);
return result;
}
struct __sub64_with_borrow_result
{ uint64_t __field_0;
uint64_t __field_1;
struct __sub64_with_borrow_result {
uint64_t __field_0;
uint64_t __field_1;
};
static inline struct __sub64_with_borrow_result
sub64_with_borrow(uint64_t x, uint64_t y, uint64_t b)
{
struct __sub64_with_borrow_result result;
uint64_t r = x - y - b;
result.__field_0 = r;
if (r > x) result.__field_1 = 1;
else if (r == x) result.__field_1 = b;
else result.__field_1 = 0;
return result;
struct __sub64_with_borrow_result result;
uint64_t r = x - y - b;
result.__field_0 = r;
if (r > x) result.__field_1 = 1;
else if (r == x) result.__field_1 = b;
else result.__field_1 = 0;
return result;
}
struct __add64_3_result
{ uint64_t __field_0;
uint64_t __field_1;
struct __add64_3_result {
uint64_t __field_0;
uint64_t __field_1;
};
static inline struct __add64_3_result add64_3(uint64_t x, uint64_t y, uint64_t z)
static inline struct __add64_3_result
add64_3(uint64_t x, uint64_t y, uint64_t z)
{
struct __add64_3_result result;
uint64_t r, c1, c2;
r = x + y;
c1 = r < y;
r += z;
c2 = r < z;
result.__field_1 = c1 + c2;
result.__field_0 = r;
return result;
struct __add64_3_result result;
uint64_t r, c1, c2;
r = x + y;
c1 = r < y;
r += z;
c2 = r < z;
result.__field_1 = c1 + c2;
result.__field_0 = r;
return result;
}
struct __lsld64_result
{ uint64_t __field_0;
uint64_t __field_1;
struct __lsld64_result {
uint64_t __field_0;
uint64_t __field_1;
};
static inline struct __lsld64_result lsld64(uint64_t x, uint64_t cnt)
static inline struct __lsld64_result
lsld64(uint64_t x, uint64_t cnt)
{
struct __lsld64_result result;
result.__field_1 = x >> (64 - cnt);
result.__field_0 = x << cnt;
return result;
struct __lsld64_result result;
result.__field_1 = x >> (64 - cnt);
result.__field_0 = x << cnt;
return result;
}
......
......@@ -19,7 +19,7 @@ module Alias
/\ min p1 = min p2 /\ max p1 = max p2 /\ zone p1 = zone p2
val open_sep (r x:ptr limb) (sx:int32) (y:ptr limb) (sy:int32) :
val open_sep (r x:ptr limb) (ghost sx:int32) (y:ptr limb) (ghost sy:int32) :
(nr:ptr limb, nx:ptr limb, ny:ptr limb, ghost m:mem)
requires { valid r sx /\ valid x sx /\ valid y sy }
requires { writable r }
......@@ -47,7 +47,7 @@ module Alias
alias { nr.data with ny.data }
alias { nx.data with ny.data }
val close_sep (r x:ptr limb) (sx:int32) (y:ptr limb) (sy:int32)
val close_sep (r x:ptr limb) (ghost sx:int32) (y:ptr limb) (ghost sy:int32)
(nr nx ny:ptr limb) (ghost m:mem) : unit
alias { nr.data with nx.data }
alias { nr.data with ny.data }
......@@ -78,7 +78,7 @@ module Alias
writes { nr, nx, ny, nr.data, nx.data, ny.data,
r.data, r.max, x.data, x.max, y.data, y.max, m.ok }
val open_rx (x:ptr limb) (sx:int32) (y:ptr limb) (sy:int32) :
val open_rx (x:ptr limb) (ghost sx:int32) (y:ptr limb) (ghost sy:int32) :
(nr:ptr limb, nx:ptr limb, ny:ptr limb, ghost m:mem)
requires { valid x sx /\ valid y sy }
requires { 0 <= sy <= sx }
......@@ -104,7 +104,7 @@ module Alias
alias { nr.data with ny.data }
alias { nx.data with ny.data }
val close_rx (x:ptr limb) (sx:int32) (y:ptr limb) (sy:int32)
val close_rx (x:ptr limb) (ghost sx:int32) (y:ptr limb) (ghost sy:int32)
(nr nx ny:ptr limb) (ghost m:mem) : unit
alias { nr.data with nx.data }
alias { nr.data with ny.data }
......@@ -131,7 +131,7 @@ module Alias
writes { nr, nx, ny, nr.data, nx.data, ny.data,
x.data, x.max, y.data, y.max, m.ok }
val open_shift_sep (r x:ptr limb) (sz:int32) :
val open_shift_sep (r x:ptr limb) (ghost sz:int32) :
(nr:ptr limb, nx:ptr limb, ghost m:mem)
requires { valid r sz /\ valid x sz }
requires { 0 <= sz }
......@@ -153,7 +153,7 @@ module Alias
writes { r, x }
alias { nr.data with nx.data }
val close_shift_sep (r x:ptr limb) (sz:int32) (nr nx:ptr limb) (ghost m:mem)
val close_shift_sep (r x:ptr limb) (ghost sz:int32) (nr nx:ptr limb) (ghost m:mem)
: unit
alias { nr.data with nx.data }
requires { writable r /\ writable nr }
......
......@@ -186,7 +186,7 @@ module Sub
done;
b
let sub_n (*[@extraction:inline]*) (r x y:ptr limb) (sz:int32) : limb
let sub_n [@extraction:inline] (r x y:ptr limb) (sz:int32) : limb
requires { 0 <= sz }
requires { valid r sz /\ valid x sz /\ valid y sz }
requires { writable r }
......@@ -228,7 +228,7 @@ module Sub
= (pelts oy)[offset y + j] };
res
let sub_n_rx (*[@extraction:inline]*) (x y:ptr limb) (sz:int32) : limb
let sub_n_rx [@extraction:inline] (x y:ptr limb) (sz:int32) : limb
requires { 0 <= sz }
requires { valid x sz /\ valid y sz }
requires { writable x }
......@@ -259,7 +259,7 @@ module Sub
(int32'int sz);
res
let sub_n_ry (*[@extraction:inline]*) (x y:ptr limb) (sz:int32) : limb
let sub_n_ry [@extraction:inline] (x y:ptr limb) (sz:int32) : limb
requires { 0 <= sz }
requires { valid x sz /\ valid y sz }
requires { writable y }
......@@ -290,8 +290,7 @@ module Sub
(offset x) (offset x) (int32'int sz);
res
let sub (*[@extraction:inline]*) (r x:ptr limb) (sx:int32)
(y:ptr limb) (sy:int32) : limb
let sub [@extraction:inline] (r x:ptr limb) (sx:int32) (y:ptr limb) (sy:int32) : limb
requires { 0 <= sy <= sx }
requires { valid r sx /\ valid x sx /\ valid y sy }
requires { writable r }
......@@ -333,8 +332,7 @@ module Sub
= (pelts oy)[offset y + j] };
res
let sub_rx (*[@extraction:inline]*) (x:ptr limb) (sx:int32)
(y:ptr limb) (sy:int32) : limb
let sub_rx [@extraction:inline] (x:ptr limb) (sx:int32) (y:ptr limb) (sy:int32) : limb
requires { 0 <= sy <= sx }
requires { valid x sx /\ valid y sy }
requires { writable x }
......@@ -366,8 +364,7 @@ module Sub
(offset y) (offset oy) (int32'int sy);
res
let sub_ry (*[@extraction:inline]*) (x:ptr limb) (sx:int32)
(y:ptr limb) (sy:int32) : limb
let sub_ry [@extraction:inline] (x:ptr limb) (sx:int32) (y:ptr limb) (sy:int32) : limb
requires { 0 <= sy <= sx }
requires { valid x sx /\ valid y sx }
requires { writable y }
......
......@@ -33,43 +33,28 @@ end
blacklist "binverttab"
module mach.int.UInt64GMP
interface
"\ntypedef unsigned __int128 uint128_t;\
\n\
\nstruct __mul64_double_result\
\n{ uint64_t __field_0;\
\n uint64_t __field_1;\
\n};\
\n\
\nstatic inline struct __mul64_double_result mul64_double(uint64_t x, uint64_t y)\
\n{\
\n uint128_t z = (uint128_t)x * (uint128_t)y;\
\n struct __mul64_double_result result = { z, z >> 64 };\
\n return result;\
\n}\
\n\
\nstatic inline uint64_t div64_2by1(uint64_t ul, uint64_t uh, uint64_t d)\
\n{\
\n return (((uint128_t)uh << 64) | ul) / d;\
\n}\
"
(* "
static struct __mul64_double_result mul64_double(uint64_t x, uint64_t y)
{
struct __mul64_double_result result;
umul_ppmm(result.__field_1,result.__field_0,x,y);
return result;
}
static uint64_t div64_2by1(uint64_t ul, uint64_t uh, uint64_t d)
{
uint64_t q;
uint64_t _dummy __attribute__((unused));
udiv_qrnnd(q,_dummy,uh,ul,d);
return q;
}
" *)
interface "\
\ntypedef unsigned __int128 uint128_t;\
\n\
\nstruct __mul64_double_result {\
\n uint64_t __field_0;\
\n uint64_t __field_1;\
\n};\
\n\
\nstatic inline struct __mul64_double_result\
\nmul64_double(uint64_t x, uint64_t y)\
\n{\
\n uint128_t z = (uint128_t)x * (uint128_t)y;\
\n struct __mul64_double_result result = { z, z >> 64 };\
\n return result;\
\n}\
\n\
\nstatic inline uint64_t\
\ndiv64_2by1(uint64_t ul, uint64_t uh, uint64_t d)\
\n{\
\n return (((uint128_t)uh << 64) | ul) / d;\
\n}\
"
syntax val mul_double "mul64_double"
syntax val div2by1 "div64_2by1"
......@@ -99,7 +84,7 @@ module ptralias.Alias
\n};\
\n\
\nstatic inline struct __open_sep_result\
\nopen_sep (uint64_t *r, uint64_t *x, int32_t sx, uint64_t *y, int32_t sy)\
\nopen_sep (uint64_t *r, uint64_t *x, uint64_t *y)\
\n{\
\n struct __open_sep_result result;\
\n result.__field_0 = r;\
......@@ -109,7 +94,7 @@ module ptralias.Alias
\n}\
\n\
\nstatic inline struct __open_rx_result\
\nopen_rx (uint64_t *x, int32_t sx, uint64_t *y, int32_t sy)\
\nopen_rx (uint64_t *x, uint64_t *y)\
\n{\
\n struct __open_rx_result result;\
\n result.__field_0 = x;\
......@@ -119,7 +104,7 @@ module ptralias.Alias
\n}\
\n\
\nstatic inline struct __open_shift_sep_result\
\nopen_shift_sep (uint64_t *r, uint64_t *x, int32_t sz)\
\nopen_shift_sep (uint64_t *r, uint64_t *x)\
\n{\
\n struct __open_shift_sep_result result;\
\n result.__field_0 = r;\
......@@ -131,9 +116,9 @@ module ptralias.Alias
syntax val open_sep "open_sep"
syntax val open_rx "open_rx"
syntax val open_shift_sep "open_shift_sep"
syntax val close_sep "IGNORE3(%1,%2,%4)" prec 1 15 15 15
syntax val close_rx "IGNORE3(%1,%2,%4)" prec 1 15 15 15
syntax val close_shift_sep "IGNORE2(%1,%2)" prec 1 15 15
syntax val close_sep "IGNORE3(%1, %2, %3)" prec 1 15 15 15
syntax val close_rx "IGNORE2(%1, %2)" prec 1 15 15
syntax val close_shift_sep "IGNORE2(%1, %2)" prec 1 15 15
end
......
......@@ -703,15 +703,26 @@ module RefreshLetBindings = struct
let id' = id_clone (pv_name pv) in
create_pvsymbol id' pv.pv_ity
let rec expr ((accv, accf) as acc) e =
let rec expr ((accv, accf, accx) as acc) e =
let acc,e = e_map_fold expr acc e in
let mk e_node = { e with e_node = e_node } in
match e.e_node with
(* collect let-bindings *)
(* collect bindings *)
| Elet (ld, e) ->
let acc, ld' = ldef acc ld in
let acc, e' = expr acc e in
acc, mk (Elet (ld', e'))
| Ematch (e, bl, el) ->
let acc, bl = Lists.map_fold_left match_pat acc bl in
let acc, el = Lists.map_fold_left match_exn acc el in
acc, mk (Ematch (e, bl, el))
| Eexn (xs, ty, e) ->
assert (not (Mid.mem xs.xs_name accx));
let id = id_clone xs.xs_name in
let xs = create_xsymbol id ~mask:xs.xs_mask xs.xs_ity in
let acc = accv, accf, Mid.add xs.xs_name xs accx in
let acc, e = expr acc e in
acc, mk (Eexn (xs, ty, e))
(* apply transformation under lambdas *)
| Efun (vl, e) ->
assert (List.for_all (fun (id,_,_) -> not (Mid.mem id accv)) vl);
......@@ -724,23 +735,24 @@ module RefreshLetBindings = struct
| Eapp (rs, el, p) ->
let rs' = Mrs.find_def rs rs accf in
acc, mk (Eapp (rs', el, p))
| _ -> acc, e
| Eraise (xs, e) ->
let xs = Mid.find_def xs xs.xs_name accx in
acc, mk (Eraise (xs, e))
| Econst _ | Eif _ | Eassign _ | Eblock _ | Ewhile _ | Efor _
| Eignore _ | Eabsurd -> acc, e
and pvs accv pv = Mid.find_def pv (pv_name pv) accv
and ldef ((accv, accf) as acc) ld =
and ldef ((accv, accf, accx) as acc) ld =
match ld with
| Lvar (pv, e) ->
let id = Translate.pv_name pv in
assert (not (Mid.mem id accv));
let pv' = clone_pv pv in
let acc = (Mid.add id pv' accv, accf) in
let acc', e' = expr acc e in
acc', Lvar (pv', e')
let (acc, pv) = refresh_pv acc pv in
let acc, e = expr acc e in
acc, Lvar (pv, e)
| Lsym (rs, tv, rty, vl, e) ->
assert (List.for_all (fun (id,_,_) -> not (Mid.mem id accv)) vl);
let rs' = clone_rs rs in
let acc = (accv, Mrs.add rs rs' accf) in
let acc = (accv, Mrs.add rs rs' accf, accx) in
let acc', e' = expr acc e in
acc', Lsym (rs, tv, rty, vl, e')
| Lany _ -> acc, ld
......@@ -752,6 +764,7 @@ module RefreshLetBindings = struct
let rs' = clone_rs rs in
Mrs.add rs rs' acc, { rd with rec_sym = rs' })
accf rl in
let acc = accv, accf, accx in
let acc, rl =
Lists.map_fold_left
(fun acc rd ->
......@@ -759,10 +772,49 @@ module RefreshLetBindings = struct
(fun (id,_,_) -> not (Mid.mem id accv))
rd.rec_args);
let acc, e = expr acc rd.rec_exp in
acc, { rd with rec_exp = e }) (accv, accf) rl in
acc, { rd with rec_exp = e }) acc rl in
acc, Lrec rl
let expr e = let _, e' = expr (Mid.empty, Mrs.empty) e in e'
and refresh_pv (accv, accf, accx) pv =
let id = Translate.pv_name pv in
assert (not (Mid.mem id accv));
let pv = clone_pv pv in
let acc = Mid.add id pv accv, accf, accx in
acc, pv
and match_pat acc (p, e) =
let rec aux acc = function
| Pwild ->
acc, Pwild
| Pvar vs ->
let pv = restore_pv vs in
let acc, pv = refresh_pv acc pv in
acc, Pvar pv.pv_vs
| Papp (ls, pl) ->
let acc, pl = Lists.map_fold_left aux acc pl in
acc, Papp (ls, pl)
| Ptuple pl ->
let acc, pl = Lists.map_fold_left aux acc pl in
acc, Ptuple pl
| Por (p1, p2) ->
let acc, p1 = aux acc p1 in
let acc, p2 = aux acc p2 in
acc, Por (p1, p2)
| Pas (pat, vs) ->
let pv = restore_pv vs in
let acc, pv = refresh_pv acc pv in
acc, Pas (pat, pv.pv_vs) in
let acc, p = aux acc p in
let acc, e = expr acc e in
acc, (p, e)
and match_exn ((_accv, _accf, accx) as acc) (xs, pl, e) =
let xs = Mid.find_def xs xs.xs_name accx in
let acc, pl = Lists.map_fold_left refresh_pv acc pl in
let acc, e = expr acc e in
acc, (xs, pl, e)
let expr e = let _, e' = expr (Mid.empty, Mrs.empty, Mid.empty) e in e'
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