Commit 95a80f16 authored by Raphael Rieu-Helft's avatar Raphael Rieu-Helft

Use the global ident table when extracting a function call

Fix wmpz extraction
parent 6b251218
......@@ -44,7 +44,7 @@ build/binverttab.h: binverttab.ml
extract: cfiles build/sqrtinit.h build/binverttab.h
CFILES = build/uint64gmp.c build/powm.c build/fxp.c build/sqrt.c build/sqrt1.c build/toom.c build/div.c build/logical.c build/mul.c build/sub.c build/add.c build/compare.c build/util.c build/int32.c
CFILES = build/uint64gmp.c build/alias.c build/z.c build/zadd.c build/zsub.c build/set.c build/powm.c build/fxp.c build/sqrt.c build/sqrt1.c build/toom.c build/div.c build/logical.c build/mul.c build/subold.c build/sub.c build/sub_1.c build/addold.c build/add.c build/add_1.c build/compare.c build/util.c build/int32.c
tests: extract
gcc $(CFLAGS) tests.c $(CFILES) -Irandom -lgmp -o build/tests
......
......@@ -188,7 +188,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 }
......@@ -230,7 +230,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 }
......@@ -259,7 +259,7 @@ module Add
= (pelts oy)[offset y + j] };
res
let add [@extraction:inline] (r x:ptr limb) (sx:int32)
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 }
......@@ -302,7 +302,7 @@ module Add
= (pelts oy)[offset y + j] };
res
let add_rx [@extraction:inline] (x:ptr limb) (sx:int32)
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 }
......@@ -333,7 +333,7 @@ module Add
= (pelts oy)[offset y + j] };
res
let add_ry [@extraction:inline] (x:ptr limb) (sx:int32)
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 }
......@@ -364,7 +364,7 @@ module Add
= (pelts ox)[offset x + j] };
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 }
......
......@@ -192,15 +192,7 @@ val release_writer (x: mpz_ptr) (p:ptr limb) : unit
ensures { mpz.readers[x] = 0 }
ensures { forall y. y <> x -> mpz.readers[y] = old mpz.readers[y] }
(* in C:
mpz_ptr x;
mpz_init(x);
extraction:
prelude defining _mpz_init as malloc + set fields
syntax val mpz_init "_mpz_init(%0)"
*)
val partial mpz_init () : mpz_ptr
val partial wmpz_init () : mpz_ptr
writes { mpz }
ensures { forall x. old mpz.alloc[result] > 0 -> result <> x }
(*result is fresh*)
......@@ -212,7 +204,7 @@ val partial mpz_init () : mpz_ptr
ensures { mpz.alloc[result] = 1 }
ensures { mpz.zones[result] <> null_zone }
val mpz_clear (x:mpz_ptr) : unit (* scrambles mpz._[x] *)
val wmpz_clear (x:mpz_ptr) : unit (* scrambles mpz._[x] *)
writes { mpz }
requires { mpz.readers[x] = 0 }
ensures { forall y. y <> x -> mpz_unchanged y mpz (old mpz) }
......
module Add
module Zadd
use int.Int
use int.Power
......
......@@ -9,7 +9,7 @@
<prover id="4" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="2000"/>
<file format="whyml" proved="true">
<path name=".."/><path name="mpz_add.mlw"/>
<theory name="Add" proved="true">
<theory name="Zadd" proved="true">
<goal name="wmpz_add&#39;vc" expl="VC for wmpz_add" proved="true">
<transf name="split_vc" proved="true" >
<goal name="wmpz_add&#39;vc.0" expl="precondition" proved="true">
......
module Sub
module Zsub
use int.Int
use int.Power
......
......@@ -9,7 +9,7 @@
<prover id="4" name="CVC4" version="1.6" timelimit="1" steplimit="0" memlimit="1000"/>
<file format="whyml" proved="true">
<path name=".."/><path name="mpz_sub.mlw"/>
<theory name="Sub" proved="true">
<theory name="Zsub" proved="true">
<goal name="wmpz_sub&#39;vc" expl="VC for wmpz_sub" proved="true">
<transf name="split_vc" proved="true" >
<goal name="wmpz_sub&#39;vc.0" expl="precondition" proved="true">
......
......@@ -182,7 +182,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 }
......@@ -224,7 +224,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 }
......@@ -253,7 +253,7 @@ module Sub
= (pelts oy)[offset y + j] };
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 }
......@@ -282,7 +282,7 @@ module Sub
= (pelts ox)[offset x + j] };
res
let sub [@extraction:inline] (r x:ptr limb) (sx:int32)
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 }
......@@ -325,7 +325,7 @@ module Sub
= (pelts oy)[offset y + j] };
res
let sub_rx [@extraction:inline] (x:ptr limb) (sx:int32)
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 }
......@@ -356,7 +356,7 @@ module Sub
= (pelts oy)[offset y + j] };
res
let sub_ry [@extraction:inline] (x:ptr limb) (sx:int32)
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 }
......
......@@ -143,10 +143,10 @@ int main () {
#endif
#if defined(TEST_GMP) || defined(TEST_MINIGMP)
c = mpn_add (refp, ap, an, bp, bn);
refc = mpn_add (refp, ap, an, bp, bn);
#endif
#ifdef TEST_WHY3
refc = wmpn_add (rp, ap, an, bp, bn);
c = wmpn_add1 (rp, ap, an, bp, bn);
#endif
#ifdef BENCH
......
......@@ -8,7 +8,7 @@ module Valuation
use number.Coprime
use export number.Parity
let rec function valuation (n p: int)
let rec ghost function valuation (n p: int)
requires { 1 < p }
requires { 1 <= n }
variant { n }
......
......@@ -131,7 +131,7 @@ struct __open_sep_result open_sep (uint64_t * r, uint64_t * x, int32_t sx,
struct __open_rx_result open_rx (uint64_t * x, int32_t sx,
uint64_t * y, int32_t sy)
{
struct __open_sep_result result;
struct __open_rx_result result;
result.__field_0 = x;
result.__field_1 = x;
result.__field_2 = y;
......@@ -141,7 +141,7 @@ struct __open_rx_result open_rx (uint64_t * x, int32_t sx,
struct __open_ry_result open_ry (uint64_t * x, int32_t sx,
uint64_t * y, int32_t sy)
{
struct __open_sep_result result;
struct __open_ry_result result;
result.__field_0 = y;
result.__field_1 = x;
result.__field_2 = y;
......@@ -150,7 +150,7 @@ struct __open_ry_result open_ry (uint64_t * x, int32_t sx,
struct __open_rxy_result open_rxy (uint64_t * x, int32_t sx)
{
struct __open_sep_result result;
struct __open_rxy_result result;
result.__field_0 = x;
result.__field_1 = x;
result.__field_2 = x;
......@@ -204,4 +204,68 @@ struct __open_rxy_result open_rxy (uint64_t * x, int32_t sx);
syntax val close_ry "IGNORE3(%1,%2,%4)" prec 1 15 15 15
syntax val close_rxy "IGNORE3(%1,%2,%4)" prec 1 15 15 15
end
module mpz.Z
prelude "
typedef struct
{
int _alloc;
int _size;
uint64_t * _ptr;
} __mpz_struct;
typedef __mpz_struct *mpz_ptr;
#define SIZ(x) ((x)->_size)
#define ALLOC(x) ((x)->_alloc)
#define PTR(x) ((x)->_ptr)
void wmpz_init (mpz_ptr x) {
ALLOC(x) = 1;
SIZ(x) = 0;
PTR(x) = malloc(1);
PTR(x)[0] = 0;
}
void wmpz_clear (mpz_ptr x)
{
free (PTR(x));
}
"
interface "
typedef struct
{
int _alloc;
int _size;
uint64_t * _ptr;
} __mpz_struct;
typedef __mpz_struct *mpz_ptr;
#define SIZ(x) ((x)->_size)
#define ALLOC(x) ((x)->_alloc)
#define PTR(x) ((x)->_ptr)
void wmpz_init (mpz_ptr x);
void wmpz_clear (mpz_ptr x);
"
syntax type mpz_ptr "mpz_ptr"
syntax val mpz_eq "%1 == %2" prec 7 15 14
syntax val size_of "SIZ(%1)" prec 1 15
syntax val set_size "SIZ(%1) = %2" prec 14 15 14
syntax val set_size_0 "SIZ(%1) = 0" prec 14 15
syntax val wmpz_minus "SIZ(%1) = -SIZ(%1)" prec 14 15 15
syntax val set_alloc "ALLOC(%1) = %2" prec 14 15 14
syntax val set_ptr "PTR(%1) = %2" prec 14 15 14
syntax val get_read_ptr "PTR(%1)" prec 1 15
syntax val get_write_ptr "PTR(%1)" prec 1 15
syntax val release_reader "(void)(%1)" prec 2 15
syntax val release_writer "(void)(%1)" prec 2 15
syntax val wmpz_init "wmpz_init(%0)" prec 2 15
syntax val wmpz_clear "wmpz_clear"
end
\ No newline at end of file
......@@ -4,7 +4,11 @@ module Wmpn
use export lemmas.Lemmas
use export util.Util
use export compare.Compare
use export add_1.Add_1
use add.AddOld
use export add.Add
use export sub_1.Sub_1
use sub.SubOld
use export sub.Sub
use export logical.Logical
use export mul.Mul
......@@ -13,5 +17,9 @@ module Wmpn
use export sqrt.Sqrt1
use export sqrtrem.Sqrt
use export powm.Powm
use export mpz.Z
use export mpz_getset.Set
use export mpz_add.Zadd
use export mpz_sub.Zsub
end
\ No newline at end of file
......@@ -438,8 +438,9 @@ module C = struct
| _ -> false
let left_assoc = function
| Band | Bor | Beq | Bne | Blt | Ble | Bgt | Bge -> true
| Beq | Bne | Blt | Ble | Bgt | Bge -> true
| Bassign -> false
| Band | Bor -> false (* avoids Wparentheses *)
let right_assoc = function
| Bassign -> true
......@@ -584,9 +585,13 @@ module Print = struct
(* call to function defined in the prelude *)
fprintf fmt (protect_on (prec < 1) "%s(%a)")
s (print_list comma (print_expr ~prec:15)) l
| Ecall (e,l) ->
| Ecall (Evar id, l) ->
fprintf fmt (protect_on (prec < 1) "%a(%a)")
print_global_ident id (print_list comma (print_expr ~prec:15)) l
| Ecall ((Esyntax _ as e),l) ->
fprintf fmt (protect_on (prec < 1) "%a(%a)")
(print_expr ~prec:1) e (print_list comma (print_expr ~prec:15)) l
| Ecall _ -> raise (Unsupported "complex function expression")
| Econst c -> print_const fmt c
| Evar id -> print_local_ident fmt id
| Elikely e -> fprintf fmt
......
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