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

Finish tuple functions, module N now compiles

parent e0a39273
......@@ -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
......
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
......@@ -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;
......
......@@ -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
......
......@@ -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
......
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