diff --git a/drivers/c.drv b/drivers/c.drv
index 9a4598a7e47d6f3ce6d2c931c19959d51abed04a..9617410814d787cb658a756db987adbcf9c29fcd 100644
--- a/drivers/c.drv
+++ b/drivers/c.drv
@@ -47,6 +47,47 @@ end
module mach.int.UInt32
+ prelude
+
+"
+#define LOW_MASK 0x00000000FFFFFFFFULL
+
+void add_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)
+{
+ 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)
+{
+ 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)
+{
+ 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)
+{
+ uint64_t r = (uint64_t)x << cnt;
+ *low = (uint32_t)(r & LOW_MASK);
+ *high = (uint32_t)(r >> 32);
+}
+"
+
syntax val of_int "%1"
syntax converter of_int "%1"
@@ -64,6 +105,10 @@ module mach.int.UInt32
syntax val (<) "%1 < %2"
syntax val (>=) "%1 >= %2"
syntax val (>) "%1 > %2"
+
+ syntax val add_mod "%1 + %2"
+ syntax val sub_mod "%1 - %2"
+ syntax val mul_mod "%1 * %2"
end
diff --git a/examples/in_progress/multiprecision/Makefile b/examples/in_progress/multiprecision/Makefile
index 39f706e750cfc9a9c40ab044e92bb8d032e0849d..e2a1f2b124aa55e5288dcec6137936230c0a6db0 100644
--- a/examples/in_progress/multiprecision/Makefile
+++ b/examples/in_progress/multiprecision/Makefile
@@ -1,2 +1,5 @@
+all: why3 extract
+why3:
+ make -C ../../..
extract:
- why3 extract -D c -o build mp2.mlw -T Main
+ why3 extract -D c -o build mp2.mlw -T N
diff --git a/examples/in_progress/multiprecision/mp2.mlw b/examples/in_progress/multiprecision/mp2.mlw
index 6e659ebf7d8fa10a7fb160133dc038dabac5af44..1470283790e440af201f7fe966a599401dc59367 100644
--- a/examples/in_progress/multiprecision/mp2.mlw
+++ b/examples/in_progress/multiprecision/mp2.mlw
@@ -1518,11 +1518,6 @@ module N
=
()
- val lsld (x cnt:limb) : (limb,limb)
- requires { 0 < l2i cnt < 32 }
- returns { (r,d) -> l2i r + radix * l2i d =
- (power 2 (l2i cnt)) * l2i x }
-
let lemma pow2_32 ()
ensures { power 2 32 = radix }
=
@@ -2110,30 +2105,21 @@ module N
assert { l2i !qh * l2i d + l2i !r = l2i ul + radix * l2i uh };
(!qh,!r)
-end
-
-module Main
-
- use import mach.c.C
- use import N
- use import mach.int.Int32
- use import int.Int
- use import ref.Ref
-
+ (** Tests *)
let print (p:t) (m n:int32) : unit
requires { 0 <= p.offset + p2i m
<= p.offset + p2i n
<= plength p }
=
let i = ref m in
- let q = ref (incr p m) in
+ let q = ref (C.incr p m) in
let one = Int32.of_int 1 in
while (Int32.(<) !i n) do
invariant { p2i m <= p2i !i <= p2i n }
invariant { (!q).offset = p.offset + p2i !i }
invariant { plength !q = plength p }
variant { p2i n - p2i !i }
- print_uint32 (get !q);
+ print_uint32 (C.get !q);
print_space ();
q := C.incr !q one;
i := Int32.(+) !i one;
@@ -2159,7 +2145,7 @@ module Main
if not (is_null p)
then begin
C.set p l1;
- C.set (incr p (Int32.of_int 1)) l2
+ C.set (C.incr p (Int32.of_int 1)) l2
end;
p
@@ -2167,7 +2153,7 @@ module Main
let p = from_limb (Limb.of_int 42) in
if not (is_null p)
then begin
- print_uint32 (get p);
+ print_uint32 (C.get p);
print_newline ();
end;
free p;
diff --git a/modules/mach/int.mlw b/modules/mach/int.mlw
index 8db904c8efda281538ab77dc0b0e5217ee4e51d4..edb865d997f604d210a7b4e7bd35476a4eb006e4 100644
--- a/modules/mach/int.mlw
+++ b/modules/mach/int.mlw
@@ -113,6 +113,7 @@ module Unsigned
use import int.Int
use import int.EuclideanDivision
+ use import int.Power
let constant min_unsigned : int = 0
@@ -157,6 +158,11 @@ module Unsigned
to_int r + (max+1) * to_int d =
to_int x * to_int y }
+ val lsld (x cnt:t) : (t,t)
+ requires { 0 < to_int cnt < 32 }
+ returns { (r,d) -> to_int r + (max+1) * to_int d =
+ (power 2 (to_int cnt)) * to_int x }
+
end
module Int31
diff --git a/src/mlw/cprinter.ml b/src/mlw/cprinter.ml
index 4ff2eee3e6a980ef99d064eed88dc51f6e69c4ca..4d3e1ae362ab161d9aeec1dfa80766ceba62ba45 100644
--- a/src/mlw/cprinter.ml
+++ b/src/mlw/cprinter.ml
@@ -220,6 +220,15 @@ module C = struct
d, Sfor(e1,e2,e3,s')
| s -> d,s
+ let rec elim_empty_blocks = function
+ | Sblock ([], s) -> elim_empty_blocks s
+ | Sblock (d,s) -> Sblock (d, elim_empty_blocks s)
+ | Sseq (s1,s2) -> Sseq (elim_empty_blocks s1, elim_empty_blocks s2)
+ | Sif (c,t,e) -> Sif(c, elim_empty_blocks t, elim_empty_blocks e)
+ | Swhile (c,s) -> Swhile(c, elim_empty_blocks s)
+ | Sfor(e1,e2,e3,s) -> Sfor(e1,e2,e3,elim_empty_blocks s)
+ | s -> s
+
let rec elim_nop = function
| Sseq (s1,s2) ->
let s1 = elim_nop s1 in
@@ -286,9 +295,9 @@ module Print = struct
| Tvoid -> fprintf fmt "void"
| Tsyntax (s, tl) ->
syntax_arguments
- (if paren then ("("^s^")") else s)
+ s
(print_ty ~paren:false) fmt tl
- | Tptr ty -> fprintf fmt "(%a)*" (print_ty ~paren:true) ty
+ | Tptr ty -> fprintf fmt "%a *" (print_ty ~paren:true) ty
| Tarray (ty, expr) ->
fprintf fmt (protect_on paren "%a[%a]")
(print_ty ~paren:true) ty (print_expr ~paren:false) expr
@@ -366,6 +375,7 @@ module Print = struct
(print_expr ~paren:false) e (print_stmt ~braces:true) (Sblock([],b))
| Sfor _ -> raise (Unprinted "for loops")
| Sbreak -> fprintf fmt "break;"
+ | Sreturn Enothing -> fprintf fmt "return;"
| Sreturn e -> fprintf fmt "return %a;" (print_expr ~paren:true) e
and print_def fmt def =
@@ -442,6 +452,7 @@ module Translate = struct
type syntax_env = { in_unguarded_loop : bool;
computes_return_value : bool;
+ returns_tuple: bool * ident list;
breaks : Sid.t;
returns : Sid.t; }
@@ -463,32 +474,50 @@ module Translate = struct
begin match ce.c_node with
| Cfun e -> expr info env e
| Capp (rs, pvsl) ->
- let e = match query_syntax info.syntax rs.rs_name with
- | 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 ->
- let args = List.filter
- (fun pv -> not (pv.pv_ghost
- || ity_equal pv.pv_ity ity_unit))
- pvsl in
- C.(Ecall(Evar(rs.rs_name),
- List.map (fun pv -> Evar(pv_name pv)) args))
- in
- C.([],
- if env.computes_return_value
- && not (ity_equal rs.rs_cty.cty_result ity_unit)
- then Sreturn e
- else Sexpr e)
+ if is_rs_tuple rs && env.computes_return_value
+ then begin
+ match env.returns_tuple with
+ | true, rl ->
+ let args = List.filter (fun pv -> not (pv.pv_ghost
+ || ity_equal pv.pv_ity ity_unit))
+ pvsl in
+ assert (List.length rl = List.length args);
+ C.([],
+ List.fold_right2 (fun res arg acc ->
+ Sseq(Sexpr(Ebinop(Bassign,
+ Eunop(Ustar,Evar(res)),
+ Evar(pv_name arg))),
+ acc))
+ rl args (Sreturn(Enothing)))
+ | _ -> assert false
+ end
+ else
+ let e = match query_syntax info.syntax rs.rs_name with
+ | 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 ->
+ let args = List.filter
+ (fun pv -> not (pv.pv_ghost
+ || ity_equal pv.pv_ity ity_unit))
+ pvsl in
+ C.(Ecall(Evar(rs.rs_name),
+ List.map (fun pv -> Evar(pv_name pv)) args))
+ in
+ C.([],
+ if env.computes_return_value
+ && not (ity_equal rs.rs_cty.cty_result ity_unit)
+ then Sreturn e
+ else Sexpr e)
| _ -> raise (Unsupported "Cpur/Cany") (*TODO clarify*)
end
| Eassign _ -> raise (Unsupported "mutable field assign")
@@ -556,6 +585,7 @@ module Translate = struct
let cd, cs = C.flatten_defs cd cs in
let env' = { computes_return_value = false;
in_unguarded_loop = true;
+ returns_tuple = env.returns_tuple;
returns = env.returns;
breaks =
if env.in_unguarded_loop
@@ -583,6 +613,7 @@ module Translate = struct
in
let env' = { computes_return_value = env.computes_return_value;
in_unguarded_loop = false;
+ returns_tuple = env.returns_tuple;
breaks = breaks;
returns = returns;
} in
@@ -603,14 +634,15 @@ module Translate = struct
match p.pat_node with Pvar _ -> true |_-> false)
rets
->
- let rets = List.map
- (fun p -> match p.pat_node with
- | Pvar vs -> C.(Eunop(Uaddr,Evar(vs.vs_name)))
+ let rets, defs = List.fold_right
+ (fun p (r, d)-> match p.pat_node with
+ | Pvar vs -> (C.(Eunop(Uaddr,Evar(vs.vs_name)))::r,
+ C.Ddecl(ty_of_ty info vs.vs_ty, [vs.vs_name, C.Enothing])::d)
| _ -> assert false )
- rets in
+ rets ([], []) in
let d,s = expr info {env with computes_return_value = false} e1 in
let b = expr info env e2 in
- d, C.(Sseq(add_to_last_call rets s, Sblock b))
+ d@defs, C.(Sseq(add_to_last_call rets s, Sblock b))
| Ecase _ -> raise (Unsupported "pattern matching")
| Eghost _ | Epure _ | Eabsurd -> assert false
@@ -630,20 +662,58 @@ module Translate = struct
&& not (ity_equal pv.pv_ity ity_unit))
rs.rs_cty.cty_args) in
begin match ce.c_node with
- | Cfun e ->
- let rity = rs.rs_cty.cty_result in
- let rtype =
- if ity_equal rity ity_unit
- then C.Tvoid
- else ty_of_ty info (ty_of_ity rity) in
- let env = { computes_return_value = true;
- in_unguarded_loop = false;
- returns = Sid.empty;
- breaks = Sid.empty; } in
- let d,s = expr info env e in
- let d,s = C.flatten_defs d s in
- let s = C.elim_nop s in
- [C.Dfun (fname, (rtype,params), (d,s))]
+ | Cfun e ->
+ let env = { computes_return_value = true;
+ in_unguarded_loop = false;
+ returns_tuple = false, [];
+ returns = Sid.empty;
+ breaks = Sid.empty; } in
+ let rity = rs.rs_cty.cty_result in
+ let is_simple_tuple ity =
+ let arity_zero = function
+ | Ityapp(_,a,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
+ | _ -> false)
+ && (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 =
+ if ity_equal rity ity_unit
+ then C.Tvoid
+ else ty_of_ty info (ty_of_ity rity) in
+ let env, rtype, params = match rtype with
+ | C.Tnosyntax when is_simple_tuple rity ->
+ (* instead of returning a tuple, return
+ void and assign the result to addresses
+ passed as parameters *)
+ let returns =
+ let f ity b acc =
+ if b
+ then (C.Tptr(ty_of_ty info (ty_of_ity ity)),
+ id_register (id_fresh "result"))::acc
+ else acc
+ in
+ match rity.ity_node with
+ | Ityapp(s, tl,_)
+ | Ityreg { reg_its = s; reg_args = tl } ->
+ List.fold_right2 f tl s.its_arg_vis []
+ | Ityvar _ -> assert false
+ in
+ {env with returns_tuple = true, List.map snd returns},
+ C.Tvoid,
+ returns@params
+ | _ -> env, rtype, params
+ in
+ let d,s = expr info env e in
+ (* let d,s = C.flatten_defs d s in *)
+ let s = C.elim_nop s in
+ let s = C.elim_empty_blocks s in
+ [C.Dfun (fname, (rtype,params), (d,s))]
| _ -> raise (Unsupported
"Non-function with no syntax in toplevel let")
end