Attention une mise à jour du serveur va être effectuée le vendredi 16 avril entre 12h et 12h30. Cette mise à jour va générer une interruption du service de quelques minutes.

Commit 041f82dc authored by Raphael Rieu-Helft's avatar Raphael Rieu-Helft

C extraction: simplify some for loops

parent c05154d9
...@@ -459,7 +459,7 @@ module Powm ...@@ -459,7 +459,7 @@ module Powm
inv inv
(* TODO rewrite this with array literal once they exist *) (* TODO rewrite this with array literal once they exist *)
let win_size [@extraction:c_inline] (eb:int32) : int32 let win_size [@extraction:c_static_inline] (eb:int32) : int32
ensures { 0 <= result <= 10 } ensures { 0 <= result <= 10 }
ensures { eb > 0 -> result > 0 } ensures { eb > 0 -> result > 0 }
= if eb = 0 then 0 = if eb = 0 then 0
...@@ -474,7 +474,7 @@ module Powm ...@@ -474,7 +474,7 @@ module Powm
else if eb <= 28161 then 9 else if eb <= 28161 then 9
else 10 else 10
let redcify [@extraction:inline] (rp up: t) (un: int32) (mp: t) (n: int32) let redcify [@extraction:c_static_inline] (rp up: t) (un: int32) (mp: t) (n: int32)
requires { valid rp n /\ valid up un /\ valid mp n } requires { valid rp n /\ valid up un /\ valid mp n }
requires { 1 <= n /\ 1 <= un } requires { 1 <= n /\ 1 <= un }
requires { un + n < max_int32 } requires { un + n < max_int32 }
...@@ -535,7 +535,7 @@ module Powm ...@@ -535,7 +535,7 @@ module Powm
= power 2 (64 * i + (nbits - 64 * i)) = power 2 (64 * i + (nbits - 64 * i))
= power 2 nbits } = power 2 nbits }
let getbit [@extraction:inline] (p:t) (ghost pn:int32) (bi:int32) : limb let getbit [@extraction:c_static_inline] (p:t) (ghost pn:int32) (bi:int32) : limb
requires { valid p pn } requires { valid p pn }
requires { 1 <= bi } requires { 1 <= bi }
requires { pn >= (div (bi + 63) 64) } requires { pn >= (div (bi + 63) 64) }
...@@ -644,7 +644,7 @@ module Powm ...@@ -644,7 +644,7 @@ module Powm
= mod (2 * d + res) 2 = mod res 2 = res }; = mod (2 * d + res) 2 = mod res 2 = res };
lps % 2 lps % 2
let getbits [@extraction:c_inline] (p: t) (ghost pn: int32) (bi:int32) let getbits [@extraction:c_static_inline] (p: t) (ghost pn: int32) (bi:int32)
(nbits:int32) : limb (nbits:int32) : limb
requires { 1 <= nbits < 64 } requires { 1 <= nbits < 64 }
requires { 0 <= bi } requires { 0 <= bi }
......
...@@ -145,9 +145,9 @@ module C = struct ...@@ -145,9 +145,9 @@ module C = struct
Sseq(s1,s'), e Sseq(s1,s'), e
| Sseq (s1,_) -> get_last_expr s1 | Sseq (s1,_) -> get_last_expr s1
| Sif (c,Sexpr t,Sexpr e) -> Snop, Equestion(c,t,e) | Sif (c,Sexpr t,Sexpr e) -> Snop, Equestion(c,t,e)
| Sif _ -> raise (Unsupported "while (complex if)") | Sif _ -> raise (Unsupported "for/while (complex if)")
| Swhile (_c,_s) -> raise (Unsupported "while (while) {}") | Swhile (_c,_s) -> raise (Unsupported "for/while (while) {}")
| Sfor _ -> raise (Unsupported "while (for)") | Sfor _ -> raise (Unsupported "for/while (for)")
| Sbreak -> raise NotAValue | Sbreak -> raise NotAValue
| Sreturn _ -> raise NotAValue | Sreturn _ -> raise NotAValue
...@@ -489,7 +489,7 @@ module Print = struct ...@@ -489,7 +489,7 @@ module Print = struct
let local_printer = create_ident_printer c_keywords ~sanitizer let local_printer = create_ident_printer c_keywords ~sanitizer
let global_printer = create_ident_printer c_keywords ~sanitizer let global_printer = create_ident_printer c_keywords ~sanitizer
let c_inline = create_attribute "extraction:c_inline" let c_static_inline = create_attribute "extraction:c_static_inline"
(* prints the c inline keyword *) (* prints the c inline keyword *)
let print_local_ident fmt id = fprintf fmt "%s" (id_unique local_printer id) let print_local_ident fmt id = fprintf fmt "%s" (id_unique local_printer id)
...@@ -663,7 +663,7 @@ module Print = struct ...@@ -663,7 +663,7 @@ module Print = struct
| Swhile (e,b) -> fprintf fmt "@[<hov 2>while (%a) {@\n@[<hov>%a@]@]@\n}" | Swhile (e,b) -> fprintf fmt "@[<hov 2>while (%a) {@\n@[<hov>%a@]@]@\n}"
print_expr_no_paren e (print_stmt ~braces:false) b print_expr_no_paren e (print_stmt ~braces:false) b
| Sfor (einit, etest, eincr, s) -> | Sfor (einit, etest, eincr, s) ->
fprintf fmt "@[<hov 2>for (%a; %a; %a) {@\n@[<hov>%a@]@\n}@]" fprintf fmt "@[<hov 2>for (%a; %a; %a) {@\n@[<hov>%a@]@]@\n}"
print_expr_no_paren einit print_expr_no_paren einit
print_expr_no_paren etest print_expr_no_paren etest
print_expr_no_paren eincr print_expr_no_paren eincr
...@@ -674,8 +674,8 @@ module Print = struct ...@@ -674,8 +674,8 @@ module Print = struct
and print_def fmt def = and print_def fmt def =
let print_inline fmt id = let print_inline fmt id =
if Sattr.mem c_inline id.id_attrs if Sattr.mem c_static_inline id.id_attrs
then fprintf fmt "inline " then fprintf fmt "static inline "
else fprintf fmt "" in else fprintf fmt "" in
try match def with try match def with
| Dfun (id,(rt,args),body) -> | Dfun (id,(rt,args),body) ->
...@@ -1170,6 +1170,75 @@ module MLToC = struct ...@@ -1170,6 +1170,75 @@ module MLToC = struct
| Eraise (xs, None) when Sid.mem xs.xs_name env.returns -> | Eraise (xs, None) when Sid.mem xs.xs_name env.returns ->
assert false (* nothing to pass to return *) assert false (* nothing to pass to return *)
| Eraise _ -> raise (Unsupported "non break/return exception raised") | Eraise _ -> raise (Unsupported "non break/return exception raised")
| Elet (Lvar(eb, ee),
{ e_node = Elet(Lvar (sb, se),
{ e_node = Efor (i, sb', dir, eb', body) })})
when pv_equal sb sb' && pv_equal eb eb' ->
Debug.dprintf debug_c_extraction "LETFOR@.";
let open Number in
begin match i.pv_vs.vs_ty.ty_node with
| Tyapp ({ ts_def = Range { ir_lower = lb; ir_upper = ub }},_) ->
let init_test_ok =
match se.e_node, ee.e_node with
| Mltree.Econst sc, Mltree.Econst ec ->
let cmp = compare_const (ConstInt sc) (ConstInt ec) in
if dir = To then cmp <= 0 else cmp >= 0
| Mltree.Econst sc, _ ->
(* for i = 0 to n, on unsigned types *)
if dir = To
then BigInt.eq sc.il_int lb
else BigInt.eq sc.il_int ub
| _, Mltree.Econst ec ->
(* for i = n downto 0 *)
if dir = To
then BigInt.eq ec.il_int ub
else BigInt.eq ec.il_int lb
| _ -> false
in
let end_test_ok =
match ee.e_node with
| Mltree.Econst ec ->
if dir = To
then BigInt.lt ec.il_int ub
else BigInt.lt lb ec.il_int
| _ -> false
in
let ty = ty_of_ty info i.pv_vs.vs_ty in
let di = C.Ddecl(ty, [i.pv_vs.vs_name, Enothing]) in
let ei = C.Evar (i.pv_vs.vs_name) in
let env_f = { env with computes_return_value = false } in
let ds, is = expr info env_f se in
let is, se = get_last_expr is in
let init_e = C.Ebinop (Bassign, ei, se) in
let de, es = expr info env_f ee in
let es, ee = get_last_expr es in
let d = di :: ds @ de in
let incr_op = match dir with To -> Upreincr | DownTo -> Upredecr in
let incr_e = C.Eunop (incr_op, ei) in
let env' = { env with computes_return_value = false;
in_unguarded_loop = true;
breaks =
if env.in_unguarded_loop
then Sid.empty else env.breaks } in
let bd, bs = expr info env' body in
let test_op = match dir with | To -> C.Ble | DownTo -> C.Bge in
let sloop =
if end_test_ok
then C.Sfor(init_e, C.Ebinop (test_op, ei, ee),
incr_e, C.Sblock(bd, bs))
else
let end_test = C.Sif (C.Ebinop (C.Beq, ei, ee),
Sbreak, Snop) in
let bs = C.Sseq (bs, end_test) in
C.Sfor(init_e, Enothing, incr_e, C.Sblock(bd,bs)) in
let ise = C.Sseq (is, es) in
let s = if init_test_ok
then sloop
else C.(Sif (Ebinop (test_op, se, ee), sloop, Snop)) in
d, C.Sseq (ise, s)
| _ ->
raise (Unsupported "for loops where loop index is not a range type")
end
| Efor (i, sb, dir, eb, body) -> | Efor (i, sb, dir, eb, body) ->
Debug.dprintf debug_c_extraction "FOR@."; Debug.dprintf debug_c_extraction "FOR@.";
begin match i.pv_vs.vs_ty.ty_node with begin match i.pv_vs.vs_ty.ty_node with
...@@ -1178,7 +1247,7 @@ module MLToC = struct ...@@ -1178,7 +1247,7 @@ module MLToC = struct
let di = C.Ddecl(ty, [i.pv_vs.vs_name, Enothing]) in let di = C.Ddecl(ty, [i.pv_vs.vs_name, Enothing]) in
let ei = C.Evar (i.pv_vs.vs_name) in let ei = C.Evar (i.pv_vs.vs_name) in
let init_e = C.Ebinop (Bassign, ei, C.Evar (sb.pv_vs.vs_name)) in let init_e = C.Ebinop (Bassign, ei, C.Evar (sb.pv_vs.vs_name)) in
let incr_op = match dir with To -> C.Upreincr | DownTo -> C.Upredecr in let incr_op = match dir with To -> Upreincr | DownTo -> Upredecr in
let incr_e = C.Eunop (incr_op, ei) in let incr_e = C.Eunop (incr_op, ei) in
let end_test = C.Sif (C.Ebinop (C.Beq, ei, C.Evar eb.pv_vs.vs_name), let end_test = C.Sif (C.Ebinop (C.Beq, ei, C.Evar eb.pv_vs.vs_name),
Sbreak, Snop) in Sbreak, Snop) in
...@@ -1195,7 +1264,8 @@ module MLToC = struct ...@@ -1195,7 +1264,8 @@ module MLToC = struct
C.Evar (sb.pv_vs.vs_name)), C.Evar (sb.pv_vs.vs_name)),
C.Sfor(init_e, Enothing, incr_e, C.Sblock(bd,bs)), C.Sfor(init_e, Enothing, incr_e, C.Sblock(bd,bs)),
Snop) Snop)
| _ -> raise (Unsupported "for loops") | _ ->
raise (Unsupported "for loops where loop index is not a range type")
end end
| Ematch (({e_node = Eapp(rs,_)} as e1), [Ptuple rets,e2], []) | Ematch (({e_node = Eapp(rs,_)} as e1), [Ptuple rets,e2], [])
when List.for_all when List.for_all
...@@ -1455,7 +1525,9 @@ module MLToC = struct ...@@ -1455,7 +1525,9 @@ module MLToC = struct
Debug.dprintf debug_c_extraction "Unsupported : %s@." s; [] Debug.dprintf debug_c_extraction "Unsupported : %s@." s; []
let translate_decl (info:info) (d:Mltree.decl) ~header : C.definition list = let translate_decl (info:info) (d:Mltree.decl) ~header : C.definition list =
let decide_print id = query_syntax info.syntax id = None in let decide_print id =
(not (header && (Sattr.mem Print.c_static_inline id.id_attrs)))
&& query_syntax info.syntax id = None in
let names = Mltree.get_decl_name d in let names = Mltree.get_decl_name d in
match List.filter decide_print names with match List.filter decide_print names with
| [] -> [] | [] -> []
......
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