Revision ca7ff3f7
Added by Lélio Brun over 1 year ago
src/backends/C/c_backend_src.ml | ||
---|---|---|
17 | 17 |
open C_backend_common |
18 | 18 |
|
19 | 19 |
module type MODIFIERS_SRC = sig |
20 |
module GhostProto: MODIFIERS_GHOST_PROTO |
|
21 |
val pp_predicates: formatter -> machine_t list -> unit |
|
22 |
val pp_set_reset_spec: formatter -> ident -> ident -> machine_t -> unit |
|
23 |
val pp_clear_reset_spec: formatter -> ident -> ident -> machine_t -> unit |
|
24 |
val pp_step_spec: formatter -> machine_t list -> ident -> ident -> machine_t -> unit |
|
25 |
val pp_step_instr_spec: machine_t -> ident -> ident -> formatter -> instr_t -> unit |
|
26 |
val pp_ghost_parameter: ident -> formatter -> ident option -> unit |
|
20 |
module GhostProto : MODIFIERS_GHOST_PROTO |
|
21 |
|
|
22 |
val pp_predicates : formatter -> machine_t list -> unit |
|
23 |
|
|
24 |
val pp_set_reset_spec : formatter -> ident -> ident -> machine_t -> unit |
|
25 |
|
|
26 |
val pp_clear_reset_spec : formatter -> ident -> ident -> machine_t -> unit |
|
27 |
|
|
28 |
val pp_step_spec : |
|
29 |
formatter -> machine_t list -> ident -> ident -> machine_t -> unit |
|
30 |
|
|
31 |
val pp_step_instr_spec : |
|
32 |
machine_t -> ident -> ident -> formatter -> instr_t -> unit |
|
33 |
|
|
34 |
val pp_ghost_parameter : ident -> formatter -> ident option -> unit |
|
27 | 35 |
end |
28 | 36 |
|
29 | 37 |
module EmptyMod = struct |
30 | 38 |
module GhostProto = EmptyGhostProto |
39 |
|
|
31 | 40 |
let pp_predicates _ _ = () |
41 |
|
|
32 | 42 |
let pp_set_reset_spec _ _ _ _ = () |
43 |
|
|
33 | 44 |
let pp_clear_reset_spec _ _ _ _ = () |
45 |
|
|
34 | 46 |
let pp_step_spec _ _ _ _ _ = () |
47 |
|
|
35 | 48 |
let pp_step_instr_spec _ _ _ _ _ = () |
49 |
|
|
36 | 50 |
let pp_ghost_parameter _ _ _ = () |
37 | 51 |
end |
38 | 52 |
|
39 |
module Main = functor (Mod: MODIFIERS_SRC) -> struct |
|
40 |
|
|
41 |
module Protos = Protos(Mod.GhostProto) |
|
42 |
|
|
43 |
(********************************************************************************************) |
|
44 |
(* Instruction Printing functions *) |
|
45 |
(********************************************************************************************) |
|
46 |
|
|
47 |
|
|
48 |
let rec merge_static_loop_profiles lp1 lp2 = |
|
49 |
match lp1, lp2 with |
|
50 |
| [] , _ -> lp2 |
|
51 |
| _ , [] -> lp1 |
|
52 |
| p1 :: q1, p2 :: q2 -> (p1 || p2) :: merge_static_loop_profiles q1 q2 |
|
53 |
|
|
54 |
(* Returns a list of bool values, indicating whether the indices must be static or not *) |
|
55 |
let rec static_loop_profile v = |
|
56 |
match v.value_desc with |
|
57 |
| Cst cst -> static_loop_profile_cst cst |
|
58 |
| Var _ | ResetFlag -> [] |
|
59 |
| Fun (_, vl) -> |
|
60 |
List.fold_right |
|
61 |
(fun v lp -> merge_static_loop_profiles lp (static_loop_profile v)) vl [] |
|
62 |
| Array vl -> |
|
63 |
true :: List.fold_right |
|
64 |
(fun v lp -> merge_static_loop_profiles lp (static_loop_profile v)) vl [] |
|
65 |
| Access (v, _) -> |
|
66 |
begin match static_loop_profile v with [] -> [] | _ :: q -> q end |
|
67 |
| Power (v, _) -> false :: static_loop_profile v |
|
68 |
and static_loop_profile_cst cst = |
|
69 |
match cst with |
|
70 |
Const_array cl -> |
|
71 |
List.fold_right |
|
72 |
(fun c lp -> merge_static_loop_profiles lp (static_loop_profile_cst c)) |
|
73 |
cl [] |
|
74 |
| _ -> [] |
|
75 |
|
|
76 |
|
|
77 |
(* Subsumes C_backend_common.pp_c_val to cope with aggressive substitution |
|
78 |
which may yield constant arrays in expressions. |
|
79 |
Type is needed to correctly print constant arrays. |
|
80 |
*) |
|
81 |
let pp_c_val m self pp_var fmt v = |
|
82 |
pp_value_suffix m self v.value_type [] pp_var fmt v |
|
83 |
|
|
84 |
let pp_machine_ pp_machine_name fn_name m fmt ?inst self mem = |
|
85 |
let name, is_arrow, static = |
|
86 |
match inst with |
|
87 |
| Some inst -> |
|
88 |
let node, static = try List.assoc inst m.minstances with Not_found -> |
|
89 |
eprintf "internal error: %s %s %s %s:@." |
|
90 |
fn_name m.mname.node_id self inst; |
|
91 |
raise Not_found |
|
92 |
in |
|
93 |
node_name node, Arrow.td_is_arrow node, static |
|
94 |
| None -> |
|
95 |
m.mname.node_id, false, [] |
|
96 |
in |
|
97 |
let is_arrow_reset = is_arrow && fn_name = "pp_machine_set_reset" in |
|
98 |
fprintf fmt "%a(%a%s%a)%a;" |
|
99 |
(if is_arrow_reset then |
|
100 |
(fun fmt -> fprintf fmt "%s_reset") |
|
101 |
else |
|
102 |
pp_machine_name) name |
|
103 |
(pp_comma_list ~pp_eol:pp_print_comma Dimension.pp_dimension) static |
|
104 |
self |
|
105 |
(pp_print_option (fun fmt -> fprintf fmt "->%s")) inst |
|
106 |
(if is_arrow_reset then pp_print_nothing else Mod.pp_ghost_parameter mem) |
|
107 |
inst |
|
108 |
|
|
109 |
let pp_machine_set_reset m self mem fmt inst = |
|
110 |
pp_machine_ pp_machine_set_reset_name "pp_machine_set_reset" m fmt ~inst |
|
111 |
self mem |
|
112 |
|
|
113 |
let pp_machine_clear_reset m self mem fmt = |
|
114 |
pp_machine_ pp_machine_clear_reset_name "pp_machine_clear_reset" m fmt |
|
115 |
self mem |
|
116 |
|
|
117 |
let pp_machine_init m self mem fmt inst = |
|
118 |
pp_machine_ pp_machine_init_name "pp_machine_init" m fmt ~inst self mem |
|
119 |
|
|
120 |
let pp_machine_clear m self mem fmt inst = |
|
121 |
pp_machine_ pp_machine_clear_name "pp_machine_clear" m fmt ~inst self mem |
|
122 |
|
|
123 |
let pp_call m self mem pp_read pp_write fmt i inputs outputs = |
|
124 |
try (* stateful node instance *) |
|
125 |
let n, _ = List.assoc i m.minstances in |
|
126 |
fprintf fmt "%a(%a%a%s->%s)%a;" |
|
127 |
pp_machine_step_name (node_name n) |
|
128 |
(pp_comma_list ~pp_eol:pp_print_comma |
|
129 |
(pp_c_val m self pp_read)) inputs |
|
130 |
(pp_comma_list ~pp_eol:pp_print_comma |
|
131 |
pp_write) outputs |
|
132 |
self |
|
133 |
i |
|
134 |
(Mod.pp_ghost_parameter mem) (Some i) |
|
135 |
with Not_found -> (* stateless node instance *) |
|
136 |
let n, _ = List.assoc i m.mcalls in |
|
137 |
fprintf fmt "%a(%a%a);" |
|
138 |
pp_machine_step_name (node_name n) |
|
139 |
(pp_comma_list ~pp_eol:pp_print_comma |
|
140 |
(pp_c_val m self pp_read)) inputs |
|
141 |
(pp_comma_list pp_write) outputs |
|
142 |
|
|
143 |
let pp_basic_instance_call m self mem = |
|
144 |
pp_call m self mem (pp_c_var_read m) (pp_c_var_write m) |
|
145 |
|
|
146 |
let pp_arrow_call m self mem fmt i outputs = |
|
147 |
match outputs with |
|
148 |
| [x] -> |
|
149 |
fprintf fmt "%a = %a(%s->%s)%a;" |
|
150 |
(pp_c_var_read m) x |
|
151 |
pp_machine_step_name Arrow.arrow_id |
|
152 |
self |
|
153 |
i |
|
154 |
(Mod.pp_ghost_parameter mem) (Some i) |
|
155 |
| _ -> assert false |
|
156 |
|
|
157 |
let pp_instance_call m self mem fmt i inputs outputs = |
|
158 |
let pp_offset pp_var indices fmt var = |
|
159 |
fprintf fmt "%a%a" |
|
160 |
pp_var var |
|
161 |
(pp_print_list ~pp_sep:pp_print_nothing (fun fmt -> fprintf fmt "[%s]")) |
|
162 |
indices |
|
163 |
in |
|
164 |
let rec aux indices fmt typ = |
|
165 |
if Types.is_array_type typ |
|
53 |
module Main = |
|
54 |
functor |
|
55 |
(Mod : MODIFIERS_SRC) |
|
56 |
-> |
|
57 |
struct |
|
58 |
module Protos = Protos (Mod.GhostProto) |
|
59 |
|
|
60 |
(********************************************************************************************) |
|
61 |
(* Instruction Printing functions *) |
|
62 |
(********************************************************************************************) |
|
63 |
|
|
64 |
let rec merge_static_loop_profiles lp1 lp2 = |
|
65 |
match lp1, lp2 with |
|
66 |
| [], _ -> |
|
67 |
lp2 |
|
68 |
| _, [] -> |
|
69 |
lp1 |
|
70 |
| p1 :: q1, p2 :: q2 -> |
|
71 |
(p1 || p2) :: merge_static_loop_profiles q1 q2 |
|
72 |
|
|
73 |
(* Returns a list of bool values, indicating whether the indices must be |
|
74 |
static or not *) |
|
75 |
let rec static_loop_profile v = |
|
76 |
match v.value_desc with |
|
77 |
| Cst cst -> |
|
78 |
static_loop_profile_cst cst |
|
79 |
| Var _ | ResetFlag -> |
|
80 |
[] |
|
81 |
| Fun (_, vl) -> |
|
82 |
List.fold_right |
|
83 |
(fun v lp -> merge_static_loop_profiles lp (static_loop_profile v)) |
|
84 |
vl [] |
|
85 |
| Array vl -> |
|
86 |
true |
|
87 |
:: |
|
88 |
List.fold_right |
|
89 |
(fun v lp -> merge_static_loop_profiles lp (static_loop_profile v)) |
|
90 |
vl [] |
|
91 |
| Access (v, _) -> ( |
|
92 |
match static_loop_profile v with [] -> [] | _ :: q -> q) |
|
93 |
| Power (v, _) -> |
|
94 |
false :: static_loop_profile v |
|
95 |
|
|
96 |
and static_loop_profile_cst cst = |
|
97 |
match cst with |
|
98 |
| Const_array cl -> |
|
99 |
List.fold_right |
|
100 |
(fun c lp -> |
|
101 |
merge_static_loop_profiles lp (static_loop_profile_cst c)) |
|
102 |
cl [] |
|
103 |
| _ -> |
|
104 |
[] |
|
105 |
|
|
106 |
(* Subsumes C_backend_common.pp_c_val to cope with aggressive substitution |
|
107 |
which may yield constant arrays in expressions. Type is needed to |
|
108 |
correctly print constant arrays. *) |
|
109 |
let pp_c_val m self pp_var fmt v = |
|
110 |
pp_value_suffix m self v.value_type [] pp_var fmt v |
|
111 |
|
|
112 |
let pp_machine_ pp_machine_name fn_name m fmt ?inst self mem = |
|
113 |
let name, is_arrow, static = |
|
114 |
match inst with |
|
115 |
| Some inst -> |
|
116 |
let node, static = |
|
117 |
try List.assoc inst m.minstances |
|
118 |
with Not_found -> |
|
119 |
eprintf "internal error: %s %s %s %s:@." fn_name m.mname.node_id |
|
120 |
self inst; |
|
121 |
raise Not_found |
|
122 |
in |
|
123 |
node_name node, Arrow.td_is_arrow node, static |
|
124 |
| None -> |
|
125 |
m.mname.node_id, false, [] |
|
126 |
in |
|
127 |
let is_arrow_reset = is_arrow && fn_name = "pp_machine_set_reset" in |
|
128 |
fprintf fmt "%a(%a%s%a)%a;" |
|
129 |
(if is_arrow_reset then fun fmt -> fprintf fmt "%s_reset" |
|
130 |
else pp_machine_name) |
|
131 |
name |
|
132 |
(pp_comma_list ~pp_eol:pp_print_comma Dimension.pp_dimension) |
|
133 |
static self |
|
134 |
(pp_print_option (fun fmt -> fprintf fmt "->%s")) |
|
135 |
inst |
|
136 |
(if is_arrow_reset then pp_print_nothing |
|
137 |
else Mod.pp_ghost_parameter mem) |
|
138 |
inst |
|
139 |
|
|
140 |
let pp_machine_set_reset m self mem fmt inst = |
|
141 |
pp_machine_ pp_machine_set_reset_name "pp_machine_set_reset" m fmt ~inst |
|
142 |
self mem |
|
143 |
|
|
144 |
let pp_machine_clear_reset m self mem fmt = |
|
145 |
pp_machine_ pp_machine_clear_reset_name "pp_machine_clear_reset" m fmt |
|
146 |
self mem |
|
147 |
|
|
148 |
let pp_machine_init m self mem fmt inst = |
|
149 |
pp_machine_ pp_machine_init_name "pp_machine_init" m fmt ~inst self mem |
|
150 |
|
|
151 |
let pp_machine_clear m self mem fmt inst = |
|
152 |
pp_machine_ pp_machine_clear_name "pp_machine_clear" m fmt ~inst self mem |
|
153 |
|
|
154 |
let pp_call m self mem pp_read pp_write fmt i inputs outputs = |
|
155 |
try |
|
156 |
(* stateful node instance *) |
|
157 |
let n, _ = List.assoc i m.minstances in |
|
158 |
fprintf fmt "%a(%a%a%s->%s)%a;" pp_machine_step_name (node_name n) |
|
159 |
(pp_comma_list ~pp_eol:pp_print_comma (pp_c_val m self pp_read)) |
|
160 |
inputs |
|
161 |
(pp_comma_list ~pp_eol:pp_print_comma pp_write) |
|
162 |
outputs self i |
|
163 |
(Mod.pp_ghost_parameter mem) |
|
164 |
(Some i) |
|
165 |
with Not_found -> |
|
166 |
(* stateless node instance *) |
|
167 |
let n, _ = List.assoc i m.mcalls in |
|
168 |
fprintf fmt "%a(%a%a);" pp_machine_step_name (node_name n) |
|
169 |
(pp_comma_list ~pp_eol:pp_print_comma (pp_c_val m self pp_read)) |
|
170 |
inputs (pp_comma_list pp_write) outputs |
|
171 |
|
|
172 |
let pp_basic_instance_call m self mem = |
|
173 |
pp_call m self mem (pp_c_var_read m) (pp_c_var_write m) |
|
174 |
|
|
175 |
let pp_arrow_call m self mem fmt i outputs = |
|
176 |
match outputs with |
|
177 |
| [ x ] -> |
|
178 |
fprintf fmt "%a = %a(%s->%s)%a;" (pp_c_var_read m) x |
|
179 |
pp_machine_step_name Arrow.arrow_id self i |
|
180 |
(Mod.pp_ghost_parameter mem) |
|
181 |
(Some i) |
|
182 |
| _ -> |
|
183 |
assert false |
|
184 |
|
|
185 |
let pp_instance_call m self mem fmt i inputs outputs = |
|
186 |
let pp_offset pp_var indices fmt var = |
|
187 |
fprintf fmt "%a%a" pp_var var |
|
188 |
(pp_print_list ~pp_sep:pp_print_nothing (fun fmt -> |
|
189 |
fprintf fmt "[%s]")) |
|
190 |
indices |
|
191 |
in |
|
192 |
let rec aux indices fmt typ = |
|
193 |
if Types.is_array_type typ then |
|
194 |
let dim = Types.array_type_dimension typ in |
|
195 |
let idx = mk_loop_var m () in |
|
196 |
fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}" idx |
|
197 |
idx idx pp_c_dimension dim idx |
|
198 |
(aux (idx :: indices)) |
|
199 |
(Types.array_element_type typ) |
|
200 |
else |
|
201 |
let pp_read = pp_offset (pp_c_var_read m) indices in |
|
202 |
let pp_write = pp_offset (pp_c_var_write m) indices in |
|
203 |
pp_call m self mem pp_read pp_write fmt i inputs outputs |
|
204 |
in |
|
205 |
reset_loop_counter (); |
|
206 |
aux [] fmt (List.hd inputs).Machine_code_types.value_type |
|
207 |
|
|
208 |
let rec pp_conditional dependencies m self mem fmt c tl el = |
|
209 |
let pp_machine_instrs = |
|
210 |
pp_print_list ~pp_open_box:pp_open_vbox0 ~pp_prologue:pp_print_cut |
|
211 |
(pp_machine_instr dependencies m self mem) |
|
212 |
in |
|
213 |
let pp_cond = pp_c_val m self (pp_c_var_read m) in |
|
214 |
match tl, el with |
|
215 |
| [], _ :: _ -> |
|
216 |
fprintf fmt "@[<v 2>if (!%a) {%a@]@,}" pp_cond c pp_machine_instrs el |
|
217 |
| _, [] -> |
|
218 |
fprintf fmt "@[<v 2>if (%a) {%a@]@,}" pp_cond c pp_machine_instrs tl |
|
219 |
| _, _ -> |
|
220 |
fprintf fmt "@[<v 2>if (%a) {%a@]@,@[<v 2>} else {%a@]@,}" pp_cond c |
|
221 |
pp_machine_instrs tl pp_machine_instrs el |
|
222 |
|
|
223 |
and pp_machine_instr dependencies m self mem fmt instr = |
|
224 |
let pp_instr fmt instr = |
|
225 |
match get_instr_desc instr with |
|
226 |
| MNoReset _ -> |
|
227 |
() |
|
228 |
| MSetReset inst -> |
|
229 |
pp_machine_set_reset m self mem fmt inst |
|
230 |
| MClearReset -> |
|
231 |
fprintf fmt "%t@,%a" |
|
232 |
(pp_machine_clear_reset m self mem) |
|
233 |
pp_label reset_label |
|
234 |
| MResetAssign b -> |
|
235 |
pp_reset_assign self fmt b |
|
236 |
| MLocalAssign (i, v) -> |
|
237 |
pp_assign m self (pp_c_var_read m) fmt (i, v) |
|
238 |
| MStateAssign (i, v) -> |
|
239 |
pp_assign m self (pp_c_var_read m) fmt (i, v) |
|
240 |
| MStep ([ i0 ], i, vl) |
|
241 |
when Basic_library.is_value_internal_fun |
|
242 |
(mk_val (Fun (i, vl)) i0.var_type) -> |
|
243 |
pp_machine_instr dependencies m self mem fmt |
|
244 |
(update_instr_desc instr |
|
245 |
(MLocalAssign (i0, mk_val (Fun (i, vl)) i0.var_type))) |
|
246 |
| MStep (il, i, vl) when !Options.mpfr && Mpfr.is_homomorphic_fun i -> |
|
247 |
pp_instance_call m self mem fmt i vl il |
|
248 |
| MStep ([ i0 ], i, vl) when has_c_prototype i dependencies -> |
|
249 |
fprintf fmt "%a = %s%a;" |
|
250 |
(pp_c_val m self (pp_c_var_read m)) |
|
251 |
(mk_val (Var i0) i0.var_type) |
|
252 |
i |
|
253 |
(pp_print_parenthesized (pp_c_val m self (pp_c_var_read m))) |
|
254 |
vl |
|
255 |
| MStep (il, i, vl) -> |
|
256 |
let td, _ = List.assoc i m.minstances in |
|
257 |
if Arrow.td_is_arrow td then pp_arrow_call m self mem fmt i il |
|
258 |
else pp_basic_instance_call m self mem fmt i vl il |
|
259 |
| MBranch (_, []) -> |
|
260 |
eprintf "internal error: C_backend_src.pp_machine_instr %a@." |
|
261 |
(pp_instr m) instr; |
|
262 |
assert false |
|
263 |
| MBranch (g, hl) -> |
|
264 |
if |
|
265 |
let t = fst (List.hd hl) in |
|
266 |
t = tag_true || t = tag_false |
|
267 |
then |
|
268 |
(* boolean case, needs special treatment in C because truth value is |
|
269 |
not unique *) |
|
270 |
(* may disappear if we optimize code by replacing last branch test |
|
271 |
with default *) |
|
272 |
let tl = try List.assoc tag_true hl with Not_found -> [] in |
|
273 |
let el = try List.assoc tag_false hl with Not_found -> [] in |
|
274 |
let no_noreset = |
|
275 |
List.filter (fun i -> |
|
276 |
match i.instr_desc with MNoReset _ -> false | _ -> true) |
|
277 |
in |
|
278 |
pp_conditional dependencies m self mem fmt g (no_noreset tl) |
|
279 |
(no_noreset el) |
|
280 |
else |
|
281 |
(* enum type case *) |
|
282 |
(*let g_typ = Typing.type_const Location.dummy_loc (Const_tag (fst |
|
283 |
(List.hd hl))) in*) |
|
284 |
fprintf fmt "@[<v 2>switch(%a) {@,%a@,}@]" |
|
285 |
(pp_c_val m self (pp_c_var_read m)) |
|
286 |
g |
|
287 |
(pp_print_list ~pp_open_box:pp_open_vbox0 |
|
288 |
(pp_machine_branch dependencies m self mem)) |
|
289 |
hl |
|
290 |
| MSpec s -> |
|
291 |
fprintf fmt "@[/*@@ %s */@]@ " s |
|
292 |
| MComment s -> |
|
293 |
fprintf fmt "/*%s*/@ " s |
|
294 |
in |
|
295 |
fprintf fmt "%a%a" pp_instr instr |
|
296 |
(Mod.pp_step_instr_spec m self mem) |
|
297 |
instr |
|
298 |
|
|
299 |
and pp_machine_branch dependencies m self mem fmt (t, h) = |
|
300 |
fprintf fmt "@[<v 2>case %a:@,%a@,break;@]" pp_c_tag t |
|
301 |
(pp_print_list ~pp_open_box:pp_open_vbox0 |
|
302 |
(pp_machine_instr dependencies m self mem)) |
|
303 |
h |
|
304 |
|
|
305 |
(* let pp_machine_nospec_instr dependencies m self fmt instr = |
|
306 |
* pp_machine_instr dependencies m self fmt instr |
|
307 |
* |
|
308 |
* let pp_machine_step_instr dependencies m self mem fmt instr = |
|
309 |
* fprintf fmt "%a%a" |
|
310 |
* (pp_machine_instr dependencies m self) instr |
|
311 |
* (Mod.pp_step_instr_spec m self mem) instr *) |
|
312 |
|
|
313 |
(********************************************************************************************) |
|
314 |
(* C file Printing functions *) |
|
315 |
(********************************************************************************************) |
|
316 |
|
|
317 |
let print_const_def fmt tdecl = |
|
318 |
let cdecl = const_of_top tdecl in |
|
319 |
if |
|
320 |
!Options.mpfr && Types.(is_real_type (array_base_type cdecl.const_type)) |
|
166 | 321 |
then |
167 |
let dim = Types.array_type_dimension typ in |
|
168 |
let idx = mk_loop_var m () in |
|
169 |
fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}" |
|
170 |
idx idx idx pp_c_dimension dim idx |
|
171 |
(aux (idx::indices)) (Types.array_element_type typ) |
|
322 |
fprintf fmt "%a;" (pp_c_type cdecl.const_id) |
|
323 |
(Types.dynamic_type cdecl.const_type) |
|
172 | 324 |
else |
173 |
let pp_read = pp_offset (pp_c_var_read m) indices in |
|
174 |
let pp_write = pp_offset (pp_c_var_write m) indices in |
|
175 |
pp_call m self mem pp_read pp_write fmt i inputs outputs |
|
176 |
in |
|
177 |
reset_loop_counter (); |
|
178 |
aux [] fmt (List.hd inputs).Machine_code_types.value_type |
|
179 |
|
|
180 |
let rec pp_conditional dependencies m self mem fmt c tl el = |
|
181 |
let pp_machine_instrs = |
|
182 |
pp_print_list ~pp_open_box:pp_open_vbox0 ~pp_prologue:pp_print_cut |
|
183 |
(pp_machine_instr dependencies m self mem) in |
|
184 |
let pp_cond = pp_c_val m self (pp_c_var_read m) in |
|
185 |
match tl, el with |
|
186 |
| [], _ :: _ -> |
|
187 |
fprintf fmt "@[<v 2>if (!%a) {%a@]@,}" |
|
188 |
pp_cond c |
|
189 |
pp_machine_instrs el |
|
190 |
| _, [] -> |
|
191 |
fprintf fmt "@[<v 2>if (%a) {%a@]@,}" |
|
192 |
pp_cond c |
|
193 |
pp_machine_instrs tl |
|
194 |
| _, _ -> |
|
195 |
fprintf fmt "@[<v 2>if (%a) {%a@]@,@[<v 2>} else {%a@]@,}" |
|
196 |
pp_cond c |
|
197 |
pp_machine_instrs tl |
|
198 |
pp_machine_instrs el |
|
199 |
|
|
200 |
and pp_machine_instr dependencies m self mem fmt instr = |
|
201 |
let pp_instr fmt instr = match get_instr_desc instr with |
|
202 |
| MNoReset _ -> () |
|
203 |
| MSetReset inst -> |
|
204 |
pp_machine_set_reset m self mem fmt inst |
|
205 |
| MClearReset -> |
|
206 |
fprintf fmt "%t@,%a" |
|
207 |
(pp_machine_clear_reset m self mem) pp_label reset_label |
|
208 |
| MResetAssign b -> |
|
209 |
pp_reset_assign self fmt b |
|
210 |
| MLocalAssign (i, v) -> |
|
211 |
pp_assign m self (pp_c_var_read m) fmt (i, v) |
|
212 |
| MStateAssign (i, v) -> |
|
213 |
pp_assign m self (pp_c_var_read m) fmt (i, v) |
|
214 |
| MStep ([i0], i, vl) when Basic_library.is_value_internal_fun (mk_val (Fun (i, vl)) i0.var_type) -> |
|
215 |
pp_machine_instr dependencies m self mem fmt |
|
216 |
(update_instr_desc instr (MLocalAssign (i0, mk_val (Fun (i, vl)) i0.var_type))) |
|
217 |
| MStep (il, i, vl) when !Options.mpfr && Mpfr.is_homomorphic_fun i -> |
|
218 |
pp_instance_call m self mem fmt i vl il |
|
219 |
| MStep ([i0], i, vl) when has_c_prototype i dependencies -> |
|
220 |
fprintf fmt "%a = %s%a;" |
|
221 |
(pp_c_val m self (pp_c_var_read m)) (mk_val (Var i0) i0.var_type) |
|
222 |
i |
|
223 |
(pp_print_parenthesized (pp_c_val m self (pp_c_var_read m))) vl |
|
224 |
| MStep (il, i, vl) -> |
|
225 |
let td, _ = List.assoc i m.minstances in |
|
226 |
if Arrow.td_is_arrow td then |
|
227 |
pp_arrow_call m self mem fmt i il |
|
228 |
else |
|
229 |
pp_basic_instance_call m self mem fmt i vl il |
|
230 |
| MBranch (_, []) -> |
|
231 |
eprintf "internal error: C_backend_src.pp_machine_instr %a@." |
|
232 |
(pp_instr m) instr; |
|
233 |
assert false |
|
234 |
| MBranch (g, hl) -> |
|
235 |
if let t = fst (List.hd hl) in t = tag_true || t = tag_false |
|
236 |
then (* boolean case, needs special treatment in C because truth value is not unique *) |
|
237 |
(* may disappear if we optimize code by replacing last branch test with default *) |
|
238 |
let tl = try List.assoc tag_true hl with Not_found -> [] in |
|
239 |
let el = try List.assoc tag_false hl with Not_found -> [] in |
|
240 |
let no_noreset = List.filter (fun i -> match i.instr_desc with |
|
241 |
| MNoReset _ -> false |
|
242 |
| _ -> true) |
|
243 |
in |
|
244 |
pp_conditional dependencies m self mem fmt g |
|
245 |
(no_noreset tl) (no_noreset el) |
|
246 |
else (* enum type case *) |
|
247 |
(*let g_typ = Typing.type_const Location.dummy_loc (Const_tag (fst (List.hd hl))) in*) |
|
248 |
fprintf fmt "@[<v 2>switch(%a) {@,%a@,}@]" |
|
249 |
(pp_c_val m self (pp_c_var_read m)) g |
|
250 |
(pp_print_list ~pp_open_box:pp_open_vbox0 |
|
251 |
(pp_machine_branch dependencies m self mem)) hl |
|
252 |
| MSpec s -> |
|
253 |
fprintf fmt "@[/*@@ %s */@]@ " s |
|
254 |
| MComment s -> |
|
255 |
fprintf fmt "/*%s*/@ " s |
|
256 |
in |
|
257 |
fprintf fmt "%a%a" pp_instr instr (Mod.pp_step_instr_spec m self mem) instr |
|
258 |
|
|
259 |
and pp_machine_branch dependencies m self mem fmt (t, h) = |
|
260 |
fprintf fmt "@[<v 2>case %a:@,%a@,break;@]" |
|
261 |
pp_c_tag t |
|
262 |
(pp_print_list ~pp_open_box:pp_open_vbox0 |
|
263 |
(pp_machine_instr dependencies m self mem)) h |
|
264 |
|
|
265 |
(* let pp_machine_nospec_instr dependencies m self fmt instr = |
|
266 |
* pp_machine_instr dependencies m self fmt instr |
|
267 |
* |
|
268 |
* let pp_machine_step_instr dependencies m self mem fmt instr = |
|
269 |
* fprintf fmt "%a%a" |
|
270 |
* (pp_machine_instr dependencies m self) instr |
|
271 |
* (Mod.pp_step_instr_spec m self mem) instr *) |
|
272 |
|
|
273 |
(********************************************************************************************) |
|
274 |
(* C file Printing functions *) |
|
275 |
(********************************************************************************************) |
|
276 |
|
|
277 |
let print_const_def fmt tdecl = |
|
278 |
let cdecl = const_of_top tdecl in |
|
279 |
if !Options.mpfr && Types.(is_real_type (array_base_type cdecl.const_type)) |
|
280 |
then |
|
281 |
fprintf fmt "%a;" |
|
282 |
(pp_c_type cdecl.const_id) (Types.dynamic_type cdecl.const_type) |
|
283 |
else |
|
284 |
fprintf fmt "%a = %a;" |
|
285 |
(pp_c_type cdecl.const_id) cdecl.const_type |
|
286 |
pp_c_const cdecl.const_value |
|
287 |
|
|
288 |
let print_alloc_instance fmt (i, (m, static)) = |
|
289 |
fprintf fmt "_alloc->%s = %a %a;" |
|
290 |
i |
|
291 |
pp_machine_alloc_name (node_name m) |
|
292 |
(pp_print_parenthesized Dimension.pp_dimension) static |
|
293 |
|
|
294 |
let print_dealloc_instance fmt (i, (m, _)) = |
|
295 |
fprintf fmt "%a (_alloc->%s);" |
|
296 |
pp_machine_dealloc_name (node_name m) |
|
297 |
i |
|
298 |
|
|
299 |
let const_locals m = |
|
300 |
List.filter (fun vdecl -> vdecl.var_dec_const) m.mstep.step_locals |
|
301 |
|
|
302 |
let pp_c_decl_array_mem self fmt id = |
|
303 |
fprintf fmt "%a = (%a) (%s->_reg.%s)" |
|
304 |
(pp_c_type (sprintf "(*%s)" id.var_id)) id.var_type |
|
305 |
(pp_c_type "(*)") id.var_type |
|
306 |
self |
|
307 |
id.var_id |
|
308 |
|
|
309 |
let print_alloc_const fmt m = |
|
310 |
pp_print_list |
|
311 |
~pp_sep:(pp_print_endcut ";") ~pp_eol:(pp_print_endcut ";") |
|
312 |
(pp_c_decl_local_var m) fmt (const_locals m) |
|
313 |
|
|
314 |
let print_alloc_array fmt vdecl = |
|
315 |
let base_type = Types.array_base_type vdecl.var_type in |
|
316 |
let size_types = Types.array_type_multi_dimension vdecl.var_type in |
|
317 |
let size_type = Dimension.multi_dimension_product vdecl.var_loc size_types in |
|
318 |
fprintf fmt |
|
319 |
"_alloc->_reg.%s = (%a*) malloc((%a)*sizeof(%a));@,\ |
|
320 |
assert(_alloc->%s);" |
|
321 |
vdecl.var_id |
|
322 |
(pp_c_type "") base_type |
|
323 |
Dimension.pp_dimension size_type |
|
324 |
(pp_c_type "") base_type |
|
325 |
vdecl.var_id |
|
326 |
|
|
327 |
let print_dealloc_array fmt vdecl = |
|
328 |
fprintf fmt "free (_alloc->_reg.%s);" |
|
329 |
vdecl.var_id |
|
330 |
|
|
331 |
let array_mems m = |
|
332 |
List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory |
|
333 |
|
|
334 |
let print_alloc_code fmt m = |
|
335 |
fprintf fmt |
|
336 |
"%a *_alloc;@,\ |
|
337 |
_alloc = (%a *) malloc(sizeof(%a));@,\ |
|
338 |
assert(_alloc);@,\ |
|
339 |
%a%areturn _alloc;" |
|
340 |
(pp_machine_memtype_name ~ghost:false) m.mname.node_id |
|
341 |
(pp_machine_memtype_name ~ghost:false) m.mname.node_id |
|
342 |
(pp_machine_memtype_name ~ghost:false) m.mname.node_id |
|
343 |
(pp_print_list ~pp_sep:pp_print_nothing print_alloc_array) (array_mems m) |
|
344 |
(pp_print_list ~pp_sep:pp_print_nothing print_alloc_instance) m.minstances |
|
345 |
|
|
346 |
let print_dealloc_code fmt m = |
|
347 |
fprintf fmt |
|
348 |
"%a%afree (_alloc);@,\ |
|
349 |
return;" |
|
350 |
(pp_print_list ~pp_sep:pp_print_nothing print_dealloc_array) (array_mems m) |
|
351 |
(pp_print_list ~pp_sep:pp_print_nothing print_dealloc_instance) m.minstances |
|
352 |
|
|
353 |
(* let print_stateless_init_code fmt m self = |
|
354 |
* let minit = List.map (fun i -> match get_instr_desc i with MReset i -> i | _ -> assert false) m.minit in |
|
355 |
* let array_mems = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in |
|
356 |
* fprintf fmt "@[<v 2>%a {@,%a%t%a%t%a%treturn;@]@,}@.@." |
|
357 |
* (print_init_prototype self) (m.mname.node_id, m.mstatic) |
|
358 |
* (\* array mems *\) |
|
359 |
* (Utils.fprintf_list ~sep:";@," (pp_c_decl_array_mem self)) array_mems |
|
360 |
* (Utils.pp_final_char_if_non_empty ";@," array_mems) |
|
361 |
* (\* memory initialization *\) |
|
362 |
* (Utils.fprintf_list ~sep:"@," (pp_initialize m self (pp_c_var_read m))) m.mmemory |
|
363 |
* (Utils.pp_newline_if_non_empty m.mmemory) |
|
364 |
* (\* sub-machines initialization *\) |
|
365 |
* (Utils.fprintf_list ~sep:"@," (pp_machine_init m self)) minit |
|
366 |
* (Utils.pp_newline_if_non_empty m.minit) |
|
367 |
* |
|
368 |
* let print_stateless_clear_code fmt m self = |
|
369 |
* let minit = List.map (fun i -> match get_instr_desc i with MReset i -> i | _ -> assert false) m.minit in |
|
370 |
* let array_mems = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in |
|
371 |
* fprintf fmt "@[<v 2>%a {@,%a%t%a%t%a%treturn;@]@,}@.@." |
|
372 |
* (print_clear_prototype self) (m.mname.node_id, m.mstatic) |
|
373 |
* (\* array mems *\) |
|
374 |
* (Utils.fprintf_list ~sep:";@," (pp_c_decl_array_mem self)) array_mems |
|
375 |
* (Utils.pp_final_char_if_non_empty ";@," array_mems) |
|
376 |
* (\* memory clear *\) |
|
377 |
* (Utils.fprintf_list ~sep:"@," (pp_clear m self (pp_c_var_read m))) m.mmemory |
|
378 |
* (Utils.pp_newline_if_non_empty m.mmemory) |
|
379 |
* (\* sub-machines clear*\) |
|
380 |
* (Utils.fprintf_list ~sep:"@," (pp_machine_clear m self)) minit |
|
381 |
* (Utils.pp_newline_if_non_empty m.minit) *) |
|
382 |
|
|
383 |
let pp_c_check m self fmt (loc, check) = |
|
384 |
fprintf fmt "@[<v>%a@,assert (%a);@]" |
|
385 |
Location.pp_c_loc loc |
|
386 |
(pp_c_val m self (pp_c_var_read m)) check |
|
387 |
|
|
388 |
let pp_print_function |
|
389 |
~pp_prototype ~prototype |
|
390 |
?(pp_spec=pp_print_nothing) |
|
391 |
?(pp_local=pp_print_nothing) ?(base_locals=[]) |
|
392 |
?(pp_array_mem=pp_print_nothing) ?(array_mems=[]) |
|
393 |
?(pp_init_mpfr_local=pp_print_nothing) |
|
394 |
?(pp_clear_mpfr_local=pp_print_nothing) |
|
395 |
?(mpfr_locals=[]) |
|
396 |
?(pp_check=pp_print_nothing) ?(checks=[]) |
|
397 |
?(pp_extra=pp_print_nothing) |
|
398 |
?(pp_instr=fun fmt _ -> pp_print_nothing fmt ()) ?(instrs=[]) |
|
399 |
fmt = |
|
400 |
fprintf fmt |
|
401 |
"%a@[<v 2>%a {@,\ |
|
402 |
%a%a\ |
|
403 |
%a%a%a%a%areturn;@]@,\ |
|
404 |
}" |
|
405 |
pp_spec () |
|
406 |
pp_prototype prototype |
|
407 |
(* locals *) |
|
408 |
(pp_print_list |
|
409 |
~pp_open_box:pp_open_vbox0 |
|
410 |
~pp_sep:pp_print_semicolon |
|
411 |
~pp_eol:pp_print_semicolon |
|
412 |
pp_local) |
|
413 |
base_locals |
|
414 |
(* array mems *) |
|
415 |
(pp_print_list |
|
416 |
~pp_open_box:pp_open_vbox0 |
|
417 |
~pp_sep:pp_print_semicolon |
|
418 |
~pp_eol:pp_print_semicolon |
|
419 |
pp_array_mem) |
|
420 |
array_mems |
|
421 |
(* locals initialization *) |
|
422 |
(pp_print_list |
|
423 |
~pp_epilogue:pp_print_cut |
|
424 |
pp_init_mpfr_local) (mpfr_vars mpfr_locals) |
|
425 |
(* check assertions *) |
|
426 |
(pp_print_list pp_check) checks |
|
427 |
(* instrs *) |
|
428 |
(pp_print_list |
|
429 |
~pp_open_box:pp_open_vbox0 |
|
430 |
~pp_epilogue:pp_print_cut |
|
431 |
pp_instr) instrs |
|
432 |
(* locals clear *) |
|
433 |
(pp_print_list |
|
434 |
~pp_epilogue:pp_print_cut |
|
435 |
pp_clear_mpfr_local) (mpfr_vars mpfr_locals) |
|
436 |
(* extra *) |
|
437 |
pp_extra () |
|
438 |
|
|
439 |
let node_of_machine m = { |
|
440 |
top_decl_desc = Node m.mname; |
|
441 |
top_decl_loc = Location.dummy_loc; |
|
442 |
top_decl_owner = ""; |
|
443 |
top_decl_itf = false |
|
444 |
} |
|
445 |
|
|
446 |
let print_stateless_code machines dependencies fmt m = |
|
447 |
let self = "__ERROR__" in |
|
448 |
if not (!Options.ansi && is_generic_node (node_of_machine m)) |
|
449 |
then |
|
450 |
(* C99 code *) |
|
325 |
fprintf fmt "%a = %a;" (pp_c_type cdecl.const_id) cdecl.const_type |
|
326 |
pp_c_const cdecl.const_value |
|
327 |
|
|
328 |
let print_alloc_instance fmt (i, (m, static)) = |
|
329 |
fprintf fmt "_alloc->%s = %a %a;" i pp_machine_alloc_name (node_name m) |
|
330 |
(pp_print_parenthesized Dimension.pp_dimension) |
|
331 |
static |
|
332 |
|
|
333 |
let print_dealloc_instance fmt (i, (m, _)) = |
|
334 |
fprintf fmt "%a (_alloc->%s);" pp_machine_dealloc_name (node_name m) i |
|
335 |
|
|
336 |
let const_locals m = |
|
337 |
List.filter (fun vdecl -> vdecl.var_dec_const) m.mstep.step_locals |
|
338 |
|
|
339 |
let pp_c_decl_array_mem self fmt id = |
|
340 |
fprintf fmt "%a = (%a) (%s->_reg.%s)" |
|
341 |
(pp_c_type (sprintf "(*%s)" id.var_id)) |
|
342 |
id.var_type (pp_c_type "(*)") id.var_type self id.var_id |
|
343 |
|
|
344 |
let print_alloc_const fmt m = |
|
345 |
pp_print_list ~pp_sep:(pp_print_endcut ";") ~pp_eol:(pp_print_endcut ";") |
|
346 |
(pp_c_decl_local_var m) fmt (const_locals m) |
|
347 |
|
|
348 |
let print_alloc_array fmt vdecl = |
|
349 |
let base_type = Types.array_base_type vdecl.var_type in |
|
350 |
let size_types = Types.array_type_multi_dimension vdecl.var_type in |
|
351 |
let size_type = |
|
352 |
Dimension.multi_dimension_product vdecl.var_loc size_types |
|
353 |
in |
|
354 |
fprintf fmt |
|
355 |
"_alloc->_reg.%s = (%a*) malloc((%a)*sizeof(%a));@,assert(_alloc->%s);" |
|
356 |
vdecl.var_id (pp_c_type "") base_type Dimension.pp_dimension size_type |
|
357 |
(pp_c_type "") base_type vdecl.var_id |
|
358 |
|
|
359 |
let print_dealloc_array fmt vdecl = |
|
360 |
fprintf fmt "free (_alloc->_reg.%s);" vdecl.var_id |
|
361 |
|
|
362 |
let array_mems m = |
|
363 |
List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory |
|
364 |
|
|
365 |
let print_alloc_code fmt m = |
|
366 |
fprintf fmt |
|
367 |
"%a *_alloc;@,\ |
|
368 |
_alloc = (%a *) malloc(sizeof(%a));@,\ |
|
369 |
assert(_alloc);@,\ |
|
370 |
%a%areturn _alloc;" |
|
371 |
(pp_machine_memtype_name ~ghost:false) |
|
372 |
m.mname.node_id |
|
373 |
(pp_machine_memtype_name ~ghost:false) |
|
374 |
m.mname.node_id |
|
375 |
(pp_machine_memtype_name ~ghost:false) |
|
376 |
m.mname.node_id |
|
377 |
(pp_print_list ~pp_sep:pp_print_nothing print_alloc_array) |
|
378 |
(array_mems m) |
|
379 |
(pp_print_list ~pp_sep:pp_print_nothing print_alloc_instance) |
|
380 |
m.minstances |
|
381 |
|
|
382 |
let print_dealloc_code fmt m = |
|
383 |
fprintf fmt "%a%afree (_alloc);@,return;" |
|
384 |
(pp_print_list ~pp_sep:pp_print_nothing print_dealloc_array) |
|
385 |
(array_mems m) |
|
386 |
(pp_print_list ~pp_sep:pp_print_nothing print_dealloc_instance) |
|
387 |
m.minstances |
|
388 |
|
|
389 |
(* let print_stateless_init_code fmt m self = |
|
390 |
* let minit = List.map (fun i -> match get_instr_desc i with MReset i -> i | _ -> assert false) m.minit in |
|
391 |
* let array_mems = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in |
|
392 |
* fprintf fmt "@[<v 2>%a {@,%a%t%a%t%a%treturn;@]@,}@.@." |
|
393 |
* (print_init_prototype self) (m.mname.node_id, m.mstatic) |
|
394 |
* (\* array mems *\) |
|
395 |
* (Utils.fprintf_list ~sep:";@," (pp_c_decl_array_mem self)) array_mems |
|
396 |
* (Utils.pp_final_char_if_non_empty ";@," array_mems) |
|
397 |
* (\* memory initialization *\) |
|
398 |
* (Utils.fprintf_list ~sep:"@," (pp_initialize m self (pp_c_var_read m))) m.mmemory |
|
399 |
* (Utils.pp_newline_if_non_empty m.mmemory) |
|
400 |
* (\* sub-machines initialization *\) |
|
401 |
* (Utils.fprintf_list ~sep:"@," (pp_machine_init m self)) minit |
|
402 |
* (Utils.pp_newline_if_non_empty m.minit) |
|
403 |
* |
|
404 |
* let print_stateless_clear_code fmt m self = |
|
405 |
* let minit = List.map (fun i -> match get_instr_desc i with MReset i -> i | _ -> assert false) m.minit in |
|
406 |
* let array_mems = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in |
|
407 |
* fprintf fmt "@[<v 2>%a {@,%a%t%a%t%a%treturn;@]@,}@.@." |
|
408 |
* (print_clear_prototype self) (m.mname.node_id, m.mstatic) |
|
409 |
* (\* array mems *\) |
|
410 |
* (Utils.fprintf_list ~sep:";@," (pp_c_decl_array_mem self)) array_mems |
|
411 |
* (Utils.pp_final_char_if_non_empty ";@," array_mems) |
|
412 |
* (\* memory clear *\) |
|
413 |
* (Utils.fprintf_list ~sep:"@," (pp_clear m self (pp_c_var_read m))) m.mmemory |
|
414 |
* (Utils.pp_newline_if_non_empty m.mmemory) |
|
415 |
* (\* sub-machines clear*\) |
|
416 |
* (Utils.fprintf_list ~sep:"@," (pp_machine_clear m self)) minit |
|
417 |
* (Utils.pp_newline_if_non_empty m.minit) *) |
|
418 |
|
|
419 |
let pp_c_check m self fmt (loc, check) = |
|
420 |
fprintf fmt "@[<v>%a@,assert (%a);@]" Location.pp_c_loc loc |
|
421 |
(pp_c_val m self (pp_c_var_read m)) |
|
422 |
check |
|
423 |
|
|
424 |
let pp_print_function ~pp_prototype ~prototype ?(pp_spec = pp_print_nothing) |
|
425 |
?(pp_local = pp_print_nothing) ?(base_locals = []) |
|
426 |
?(pp_array_mem = pp_print_nothing) ?(array_mems = []) |
|
427 |
?(pp_init_mpfr_local = pp_print_nothing) |
|
428 |
?(pp_clear_mpfr_local = pp_print_nothing) ?(mpfr_locals = []) |
|
429 |
?(pp_check = pp_print_nothing) ?(checks = []) |
|
430 |
?(pp_extra = pp_print_nothing) |
|
431 |
?(pp_instr = fun fmt _ -> pp_print_nothing fmt ()) ?(instrs = []) fmt = |
|
432 |
fprintf fmt "%a@[<v 2>%a {@,%a%a%a%a%a%a%areturn;@]@,}" pp_spec () |
|
433 |
pp_prototype prototype |
|
434 |
(* locals *) |
|
435 |
(pp_print_list ~pp_open_box:pp_open_vbox0 ~pp_sep:pp_print_semicolon |
|
436 |
~pp_eol:pp_print_semicolon pp_local) |
|
437 |
base_locals |
|
438 |
(* array mems *) |
|
439 |
(pp_print_list ~pp_open_box:pp_open_vbox0 ~pp_sep:pp_print_semicolon |
|
440 |
~pp_eol:pp_print_semicolon pp_array_mem) |
|
441 |
array_mems |
|
442 |
(* locals initialization *) |
|
443 |
(pp_print_list ~pp_epilogue:pp_print_cut pp_init_mpfr_local) |
|
444 |
(mpfr_vars mpfr_locals) |
|
445 |
(* check assertions *) |
|
446 |
(pp_print_list pp_check) |
|
447 |
checks |
|
448 |
(* instrs *) |
|
449 |
(pp_print_list ~pp_open_box:pp_open_vbox0 ~pp_epilogue:pp_print_cut |
|
450 |
pp_instr) |
|
451 |
instrs |
|
452 |
(* locals clear *) |
|
453 |
(pp_print_list ~pp_epilogue:pp_print_cut pp_clear_mpfr_local) |
|
454 |
(mpfr_vars mpfr_locals) (* extra *) |
|
455 |
pp_extra () |
|
456 |
|
|
457 |
let node_of_machine m = |
|
458 |
{ |
|
459 |
top_decl_desc = Node m.mname; |
|
460 |
top_decl_loc = Location.dummy_loc; |
|
461 |
top_decl_owner = ""; |
|
462 |
top_decl_itf = false; |
|
463 |
} |
|
464 |
|
|
465 |
let print_stateless_code machines dependencies fmt m = |
|
466 |
let self = "__ERROR__" in |
|
467 |
if not (!Options.ansi && is_generic_node (node_of_machine m)) then |
|
468 |
(* C99 code *) |
|
469 |
pp_print_function |
|
470 |
~pp_spec:(fun fmt () -> Mod.pp_step_spec fmt machines self self m) |
|
471 |
~pp_prototype:Protos.print_stateless_prototype |
|
472 |
~prototype:(m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs) |
|
473 |
~pp_local:(pp_c_decl_local_var m) ~base_locals:m.mstep.step_locals |
|
474 |
~pp_init_mpfr_local:(pp_initialize m self (pp_c_var_read m)) |
|
475 |
~pp_clear_mpfr_local:(pp_clear m self (pp_c_var_read m)) |
|
476 |
~mpfr_locals:m.mstep.step_locals ~pp_check:(pp_c_check m self) |
|
477 |
~checks:m.mstep.step_checks |
|
478 |
~pp_instr:(pp_machine_instr dependencies m self self) |
|
479 |
~instrs:m.mstep.step_instrs fmt |
|
480 |
else |
|
481 |
(* C90 code *) |
|
482 |
let gen_locals, base_locals = |
|
483 |
List.partition |
|
484 |
(fun v -> Types.is_generic_type v.var_type) |
|
485 |
m.mstep.step_locals |
|
486 |
in |
|
487 |
let gen_calls = |
|
488 |
List.map |
|
489 |
(fun e -> |
|
490 |
let id, _, _ = call_of_expr e in |
|
491 |
mk_call_var_decl e.expr_loc id) |
|
492 |
m.mname.node_gencalls |
|
493 |
in |
|
494 |
pp_print_function ~pp_prototype:Protos.print_stateless_prototype |
|
495 |
~prototype: |
|
496 |
( m.mname.node_id, |
|
497 |
m.mstep.step_inputs @ gen_locals @ gen_calls, |
|
498 |
m.mstep.step_outputs ) |
|
499 |
~pp_local:(pp_c_decl_local_var m) ~base_locals |
|
500 |
~pp_init_mpfr_local:(pp_initialize m self (pp_c_var_read m)) |
|
501 |
~pp_clear_mpfr_local:(pp_clear m self (pp_c_var_read m)) |
|
502 |
~mpfr_locals:m.mstep.step_locals ~pp_check:(pp_c_check m self) |
|
503 |
~checks:m.mstep.step_checks |
|
504 |
~pp_instr:(pp_machine_instr dependencies m self self) |
|
505 |
~instrs:m.mstep.step_instrs fmt |
|
506 |
|
|
507 |
let print_clear_reset_code dependencies self mem fmt m = |
|
451 | 508 |
pp_print_function |
452 |
~pp_spec:(fun fmt () -> Mod.pp_step_spec fmt machines self self m) |
|
453 |
~pp_prototype:Protos.print_stateless_prototype |
|
454 |
~prototype:(m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs) |
|
455 |
~pp_local:(pp_c_decl_local_var m) |
|
456 |
~base_locals:m.mstep.step_locals |
|
457 |
~pp_init_mpfr_local:(pp_initialize m self (pp_c_var_read m)) |
|
458 |
~pp_clear_mpfr_local:(pp_clear m self (pp_c_var_read m)) |
|
459 |
~mpfr_locals:m.mstep.step_locals |
|
460 |
~pp_check:(pp_c_check m self) |
|
461 |
~checks:m.mstep.step_checks |
|
462 |
~pp_instr:(pp_machine_instr dependencies m self self) |
|
463 |
~instrs:m.mstep.step_instrs |
|
509 |
~pp_spec:(fun fmt () -> Mod.pp_clear_reset_spec fmt self mem m) |
|
510 |
~pp_prototype:(Protos.print_clear_reset_prototype self mem) |
|
511 |
~prototype:(m.mname.node_id, m.mstatic) |
|
512 |
~pp_local:(pp_c_decl_local_var m) ~base_locals:(const_locals m) |
|
513 |
~pp_instr:(pp_machine_instr dependencies m self mem) |
|
514 |
~instrs: |
|
515 |
[ |
|
516 |
mk_branch |
|
517 |
(mk_val ResetFlag Type_predef.type_bool) |
|
518 |
[ "true", mkinstr (MResetAssign false) :: m.minit ]; |
|
519 |
] |
|
464 | 520 |
fmt |
465 |
else |
|
466 |
(* C90 code *) |
|
467 |
let gen_locals, base_locals = List.partition (fun v -> |
|
468 |
Types.is_generic_type v.var_type) m.mstep.step_locals in |
|
469 |
let gen_calls = List.map (fun e -> |
|
470 |
let (id, _, _) = call_of_expr e |
|
471 |
in mk_call_var_decl e.expr_loc id) m.mname.node_gencalls in |
|
521 |
|
|
522 |
let print_set_reset_code dependencies self mem fmt m = |
|
472 | 523 |
pp_print_function |
473 |
~pp_prototype:Protos.print_stateless_prototype |
|
474 |
~prototype:(m.mname.node_id, |
|
475 |
m.mstep.step_inputs @ gen_locals @ gen_calls, |
|
476 |
m.mstep.step_outputs) |
|
477 |
~pp_local:(pp_c_decl_local_var m) |
|
478 |
~base_locals |
|
479 |
~pp_init_mpfr_local:(pp_initialize m self (pp_c_var_read m)) |
|
480 |
~pp_clear_mpfr_local:(pp_clear m self (pp_c_var_read m)) |
|
481 |
~mpfr_locals:m.mstep.step_locals |
|
482 |
~pp_check:(pp_c_check m self) |
|
483 |
~checks:m.mstep.step_checks |
|
484 |
~pp_instr:(pp_machine_instr dependencies m self self) |
|
485 |
~instrs:m.mstep.step_instrs |
|
524 |
~pp_spec:(fun fmt () -> Mod.pp_set_reset_spec fmt self mem m) |
|
525 |
~pp_prototype:(Protos.print_set_reset_prototype self mem) |
|
526 |
~prototype:(m.mname.node_id, m.mstatic) |
|
527 |
~pp_instr:(pp_machine_instr dependencies m self mem) |
|
528 |
~instrs:[ mkinstr (MResetAssign true) ] |
|
486 | 529 |
fmt |
487 | 530 |
|
488 |
let print_clear_reset_code dependencies self mem fmt m = |
|
489 |
pp_print_function |
|
490 |
~pp_spec:(fun fmt () -> Mod.pp_clear_reset_spec fmt self mem m) |
|
491 |
~pp_prototype:(Protos.print_clear_reset_prototype self mem) |
|
492 |
~prototype:(m.mname.node_id, m.mstatic) |
|
493 |
~pp_local:(pp_c_decl_local_var m) |
|
494 |
~base_locals:(const_locals m) |
|
495 |
~pp_instr:(pp_machine_instr dependencies m self mem) |
|
496 |
~instrs:[mk_branch |
|
497 |
(mk_val ResetFlag Type_predef.type_bool) |
|
498 |
["true", mkinstr (MResetAssign false) :: m.minit]] |
|
499 |
fmt |
|
500 |
|
|
501 |
let print_set_reset_code dependencies self mem fmt m = |
|
502 |
pp_print_function |
|
503 |
~pp_spec:(fun fmt () -> Mod.pp_set_reset_spec fmt self mem m) |
|
504 |
~pp_prototype:(Protos.print_set_reset_prototype self mem) |
|
505 |
~prototype:(m.mname.node_id, m.mstatic) |
|
506 |
~pp_instr:(pp_machine_instr dependencies m self mem) |
|
507 |
~instrs:[mkinstr (MResetAssign true)] |
|
508 |
fmt |
|
509 |
|
|
510 |
let print_init_code self fmt m = |
|
511 |
let minit = List.map (fun i -> |
|
512 |
match get_instr_desc i with |
|
513 |
| MSetReset i -> i |
|
514 |
| _ -> assert false) |
|
515 |
m.minit in |
|
516 |
pp_print_function |
|
517 |
~pp_prototype:(Protos.print_init_prototype self) |
|
518 |
~prototype:(m.mname.node_id, m.mstatic) |
|
519 |
~pp_array_mem:(pp_c_decl_array_mem self) |
|
520 |
~array_mems:(array_mems m) |
|
521 |
~pp_init_mpfr_local:(pp_initialize m self (pp_c_var_read m)) |
|
522 |
~mpfr_locals:m.mmemory |
|
523 |
~pp_extra:(fun fmt () -> |
|
524 |
pp_print_list |
|
525 |
~pp_open_box:pp_open_vbox0 |
|
526 |
~pp_epilogue:pp_print_cut |
|
527 |
(pp_machine_init m self self) |
|
528 |
fmt minit) |
|
529 |
fmt |
|
530 |
|
|
531 |
let print_clear_code self fmt m = |
|
532 |
let minit = List.map (fun i -> |
|
533 |
match get_instr_desc i with |
|
534 |
| MSetReset i -> i |
|
535 |
| _ -> assert false) m.minit in |
|
536 |
pp_print_function |
|
537 |
~pp_prototype:(Protos.print_clear_prototype self) |
|
538 |
~prototype:(m.mname.node_id, m.mstatic) |
|
539 |
~pp_array_mem:(pp_c_decl_array_mem self) |
|
540 |
~array_mems:(array_mems m) |
|
541 |
~pp_clear_mpfr_local:(pp_clear m self (pp_c_var_read m)) |
|
542 |
~mpfr_locals:m.mmemory |
|
543 |
~pp_extra:(fun fmt () -> |
|
544 |
pp_print_list |
|
545 |
~pp_open_box:pp_open_vbox0 |
|
546 |
~pp_epilogue:pp_print_cut |
|
547 |
(pp_machine_clear m self self) |
|
548 |
fmt minit) |
|
549 |
fmt |
|
550 |
|
|
551 |
let print_step_code machines dependencies self mem fmt m = |
|
552 |
if not (!Options.ansi && is_generic_node (node_of_machine m)) |
|
553 |
then |
|
554 |
(* C99 code *) |
|
531 |
let print_init_code self fmt m = |
|
532 |
let minit = |
|
533 |
List.map |
|
534 |
(fun i -> |
|
535 |
match get_instr_desc i with MSetReset i -> i | _ -> assert false) |
|
536 |
m.minit |
|
537 |
in |
|
555 | 538 |
pp_print_function |
556 |
~pp_spec:(fun fmt () -> Mod.pp_step_spec fmt machines self mem m) |
|
557 |
~pp_prototype:(Protos.print_step_prototype self mem) |
|
558 |
~prototype:(m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs) |
|
559 |
~pp_local:(pp_c_decl_local_var m) |
|
560 |
~base_locals:m.mstep.step_locals |
|
561 |
~pp_array_mem:(pp_c_decl_array_mem self) |
|
562 |
~array_mems:(array_mems m) |
|
539 |
~pp_prototype:(Protos.print_init_prototype self) |
|
540 |
~prototype:(m.mname.node_id, m.mstatic) |
|
541 |
~pp_array_mem:(pp_c_decl_array_mem self) ~array_mems:(array_mems m) |
|
563 | 542 |
~pp_init_mpfr_local:(pp_initialize m self (pp_c_var_read m)) |
564 |
~pp_clear_mpfr_local:(pp_clear m self (pp_c_var_read m)) |
|
565 |
~mpfr_locals:m.mstep.step_locals |
|
566 |
~pp_check:(pp_c_check m self) |
|
567 |
~checks:m.mstep.step_checks |
|
568 |
~pp_instr:(pp_machine_instr dependencies m self mem) |
|
569 |
~instrs:m.mstep.step_instrs |
|
543 |
~mpfr_locals:m.mmemory |
|
544 |
~pp_extra:(fun fmt () -> |
|
545 |
pp_print_list ~pp_open_box:pp_open_vbox0 ~pp_epilogue:pp_print_cut |
|
546 |
(pp_machine_init m self self) |
|
547 |
fmt minit) |
|
570 | 548 |
fmt |
571 |
else |
|
572 |
(* C90 code *) |
|
573 |
let gen_locals, base_locals = List.partition (fun v -> |
|
574 |
Types.is_generic_type v.var_type) m.mstep.step_locals in |
|
575 |
let gen_calls = List.map (fun e -> |
|
576 |
let id, _, _ = call_of_expr e in |
|
577 |
mk_call_var_decl e.expr_loc id) m.mname.node_gencalls in |
|
549 |
|
|
550 |
let print_clear_code self fmt m = |
|
551 |
let minit = |
|
552 |
List.map |
|
553 |
(fun i -> |
|
554 |
match get_instr_desc i with MSetReset i -> i | _ -> assert false) |
|
555 |
m.minit |
|
556 |
in |
|
578 | 557 |
pp_print_function |
579 |
~pp_spec:(fun fmt () -> Mod.pp_step_spec fmt machines self mem m) |
|
580 |
~pp_prototype:(Protos.print_step_prototype self mem) |
|
581 |
~prototype:(m.mname.node_id, |
|
582 |
m.mstep.step_inputs @ gen_locals @ gen_calls, |
|
583 |
m.mstep.step_outputs) |
|
584 |
~pp_local:(pp_c_decl_local_var m) |
|
585 |
~base_locals |
|
586 |
~pp_init_mpfr_local:(pp_initialize m self (pp_c_var_read m)) |
|
558 |
~pp_prototype:(Protos.print_clear_prototype self) |
|
559 |
~prototype:(m.mname.node_id, m.mstatic) |
|
560 |
~pp_array_mem:(pp_c_decl_array_mem self) ~array_mems:(array_mems m) |
|
587 | 561 |
~pp_clear_mpfr_local:(pp_clear m self (pp_c_var_read m)) |
588 |
~mpfr_locals:m.mstep.step_locals
|
|
589 |
~pp_check:(pp_c_check m self)
|
|
590 |
~checks:m.mstep.step_checks
|
|
591 |
~pp_instr:(pp_machine_instr dependencies m self mem)
|
|
592 |
~instrs:m.mstep.step_instrs
|
|
562 |
~mpfr_locals:m.mmemory
|
|
563 |
~pp_extra:(fun fmt () ->
|
|
564 |
pp_print_list ~pp_open_box:pp_open_vbox0 ~pp_epilogue:pp_print_cut
|
|
565 |
(pp_machine_clear m self self)
|
|
566 |
fmt minit)
|
|
593 | 567 |
fmt |
594 | 568 |
|
595 |
(********************************************************************************************) |
|
596 |
(* MAIN C file Printing functions *) |
|
597 |
(********************************************************************************************) |
|
598 |
|
|
599 |
let pp_const_initialize m pp_var fmt const = |
|
600 |
let var = Machine_code_common.mk_val |
|
601 |
(Var (Corelang.var_decl_of_const const)) const.const_type in |
|
602 |
let rec aux indices value fmt typ = |
|
603 |
if Types.is_array_type typ |
|
604 |
then |
|
605 |
let dim = Types.array_type_dimension typ in |
|
606 |
let szl = Utils.enumerate (Dimension.size_const_dimension dim) in |
|
607 |
let typ' = Types.array_element_type typ in |
|
608 |
let value = match value with |
|
609 |
| Const_array ca -> List.nth ca |
|
610 |
| _ -> assert false in |
|
611 |
pp_print_list |
|
612 |
(fun fmt i -> aux (string_of_int i :: indices) (value i) fmt typ') fmt szl |
|
569 |
let print_step_code machines dependencies self mem fmt m = |
|
570 |
if not (!Options.ansi && is_generic_node (node_of_machine m)) then |
|
571 |
(* C99 code *) |
|
572 |
pp_print_function |
|
573 |
~pp_spec:(fun fmt () -> Mod.pp_step_spec fmt machines self mem m) |
|
574 |
~pp_prototype:(Protos.print_step_prototype self mem) |
|
575 |
~prototype:(m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs) |
|
576 |
~pp_local:(pp_c_decl_local_var m) ~base_locals:m.mstep.step_locals |
|
577 |
~pp_array_mem:(pp_c_decl_array_mem self) ~array_mems:(array_mems m) |
|
578 |
~pp_init_mpfr_local:(pp_initialize m self (pp_c_var_read m)) |
|
579 |
~pp_clear_mpfr_local:(pp_clear m self (pp_c_var_read m)) |
|
580 |
~mpfr_locals:m.mstep.step_locals ~pp_check:(pp_c_check m self) |
|
581 |
~checks:m.mstep.step_checks |
|
582 |
~pp_instr:(pp_machine_instr dependencies m self mem) |
|
583 |
~instrs:m.mstep.step_instrs fmt |
|
613 | 584 |
else |
614 |
let indices = List.rev indices in |
|
615 |
let pp_var_suffix fmt var = |
|
616 |
fprintf fmt "%a%a" (pp_c_val m "" pp_var) var pp_array_suffix indices in |
|
617 |
fprintf fmt "%a@,%a" |
|
618 |
(Mpfr.pp_inject_init pp_var_suffix) var |
|
619 |
(Mpfr.pp_inject_real pp_var_suffix pp_c_const) (var, value) |
|
620 |
in |
|
621 |
reset_loop_counter (); |
|
622 |
aux [] const.const_value fmt const.const_type |
|
623 |
|
|
624 |
let pp_const_clear pp_var fmt const = |
|
625 |
let m = Machine_code_common.empty_machine in |
|
626 |
let var = Corelang.var_decl_of_const const in |
|
627 |
let rec aux indices fmt typ = |
|
628 |
if Types.is_array_type typ |
|
629 |
then |
|
630 |
let dim = Types.array_type_dimension typ in |
|
631 |
let idx = mk_loop_var m () in |
|
632 |
fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}" |
|
633 |
idx idx idx pp_c_dimension dim idx |
|
634 |
(aux (idx::indices)) (Types.array_element_type typ) |
|
635 |
else |
|
636 |
let indices = List.rev indices in |
|
637 |
let pp_var_suffix fmt var = |
|
638 |
fprintf fmt "%a%a" (pp_c_var m "" pp_var) var pp_array_suffix indices in |
|
639 |
Mpfr.pp_inject_clear pp_var_suffix fmt var |
|
640 |
in |
|
641 |
reset_loop_counter (); |
|
642 |
aux [] fmt var.var_type |
|
643 |
|
|
644 |
let print_import_init fmt dep = |
|
645 |
let baseNAME = file_to_module_name dep.name in |
|
646 |
fprintf fmt "%a();" pp_global_init_name baseNAME |
|
647 |
|
|
648 |
let print_import_clear fmt dep = |
|
649 |
let baseNAME = file_to_module_name dep.name in |
|
650 |
fprintf fmt "%a();" pp_global_clear_name baseNAME |
|
651 |
|
|
652 |
let print_global_init_code fmt (basename, prog, dependencies) = |
|
653 |
let baseNAME = file_to_module_name basename in |
|
654 |
let constants = List.map const_of_top (get_consts prog) in |
|
655 |
fprintf fmt |
|
656 |
"@[<v 2>%a {@,\ |
|
657 |
static %s init = 0;@,\ |
|
658 |
@[<v 2>if (!init) { @,\ |
|
659 |
init = 1;%a%a@]@,\ |
|
660 |
}@,\ |
|
661 |
return;@]@,\ |
|
662 |
}" |
|
663 |
print_global_init_prototype baseNAME |
|
664 |
(pp_c_basic_type_desc Type_predef.type_bool) |
|
665 |
(* constants *) |
|
666 |
(pp_print_list |
|
667 |
~pp_prologue:pp_print_cut |
|
668 |
(pp_const_initialize empty_machine (pp_c_var_read empty_machine))) |
|
669 |
(mpfr_consts constants) |
|
670 |
(* dependencies initialization *) |
|
671 |
(pp_print_list |
|
672 |
~pp_prologue:pp_print_cut |
|
673 |
print_import_init) (List.filter (fun dep -> dep.local) dependencies) |
|
674 |
|
|
675 |
let print_global_clear_code fmt (basename, prog, dependencies) = |
|
676 |
let baseNAME = file_to_module_name basename in |
|
677 |
let constants = List.map const_of_top (get_consts prog) in |
|
678 |
fprintf fmt |
|
679 |
"@[<v 2>%a {@,\ |
|
680 |
static %s clear = 0;@,\ |
|
681 |
@[<v 2>if (!clear) { @,\ |
|
682 |
clear = 1;%a%a@]@,\ |
|
683 |
}@,\ |
|
684 |
return;@]@,\ |
|
685 |
}" |
|
686 |
print_global_clear_prototype baseNAME |
|
687 |
(pp_c_basic_type_desc Type_predef.type_bool) |
|
688 |
(* constants *) |
|
689 |
(pp_print_list |
|
690 |
~pp_prologue:pp_print_cut |
|
691 |
(pp_const_clear (pp_c_var_read empty_machine))) (mpfr_consts constants) |
|
692 |
(* dependencies initialization *) |
|
693 |
(pp_print_list |
|
694 |
~pp_prologue:pp_print_cut |
|
695 |
print_import_clear) (List.filter (fun dep -> dep.local) dependencies) |
|
696 |
|
|
697 |
let print_alloc_function fmt m = |
|
698 |
if (not !Options.static_mem) then |
|
699 |
(* Alloc functions, only if non static mode *) |
|
585 |
(* C90 code *) |
|
586 |
let gen_locals, base_locals = |
|
587 |
List.partition |
|
588 |
(fun v -> Types.is_generic_type v.var_type) |
|
589 |
m.mstep.step_locals |
|
590 |
in |
|
591 |
let gen_calls = |
|
592 |
List.map |
|
593 |
(fun e -> |
|
594 |
let id, _, _ = call_of_expr e in |
|
595 |
mk_call_var_decl e.expr_loc id) |
|
596 |
m.mname.node_gencalls |
|
597 |
in |
|
598 |
pp_print_function |
|
599 |
~pp_spec:(fun fmt () -> Mod.pp_step_spec fmt machines self mem m) |
|
600 |
~pp_prototype:(Protos.print_step_prototype self mem) |
|
601 |
~prototype: |
|
602 |
( m.mname.node_id, |
|
603 |
m.mstep.step_inputs @ gen_locals @ gen_calls, |
|
604 |
m.mstep.step_outputs ) |
|
605 |
~pp_local:(pp_c_decl_local_var m) ~base_locals |
|
606 |
~pp_init_mpfr_local:(pp_initialize m self (pp_c_var_read m)) |
|
607 |
~pp_clear_mpfr_local:(pp_clear m self (pp_c_var_read m)) |
|
608 |
~mpfr_locals:m.mstep.step_locals ~pp_check:(pp_c_check m self) |
|
609 |
~checks:m.mstep.step_checks |
|
610 |
~pp_instr:(pp_machine_instr dependencies m self mem) |
|
611 |
~instrs:m.mstep.step_instrs fmt |
|
612 |
|
|
613 |
(********************************************************************************************) |
|
614 |
(* MAIN C file Printing functions *) |
|
615 |
(********************************************************************************************) |
|
616 |
|
|
617 |
let pp_const_initialize m pp_var fmt const = |
|
618 |
let var = |
|
619 |
Machine_code_common.mk_val |
|
620 |
(Var (Corelang.var_decl_of_const const)) |
|
621 |
const.const_type |
|
622 |
in |
|
623 |
let rec aux indices value fmt typ = |
|
624 |
if Types.is_array_type typ then |
|
625 |
let dim = Types.array_type_dimension typ in |
|
626 |
let szl = Utils.enumerate (Dimension.size_const_dimension dim) in |
|
627 |
let typ' = Types.array_element_type typ in |
|
628 |
let value = |
|
629 |
match value with Const_array ca -> List.nth ca | _ -> assert false |
|
630 |
in |
|
631 |
pp_print_list |
|
632 |
(fun fmt i -> aux (string_of_int i :: indices) (value i) fmt typ') |
|
633 |
fmt szl |
|
634 |
else |
|
635 |
let indices = List.rev indices in |
|
636 |
let pp_var_suffix fmt var = |
|
637 |
fprintf fmt "%a%a" (pp_c_val m "" pp_var) var pp_array_suffix |
|
638 |
indices |
|
639 |
in |
|
640 |
fprintf fmt "%a@,%a" |
|
641 |
(Mpfr.pp_inject_init pp_var_suffix) |
|
642 |
var |
|
643 |
(Mpfr.pp_inject_real pp_var_suffix pp_c_const) |
|
644 |
(var, value) |
|
645 |
in |
|
646 |
reset_loop_counter (); |
|
647 |
aux [] const.const_value fmt const.const_type |
|
648 |
|
|
649 |
let pp_const_clear pp_var fmt const = |
|
650 |
let m = Machine_code_common.empty_machine in |
|
651 |
let var = Corelang.var_decl_of_const const in |
|
652 |
let rec aux indices fmt typ = |
|
653 |
if Types.is_array_type typ then |
|
654 |
let dim = Types.array_type_dimension typ in |
|
655 |
let idx = mk_loop_var m () in |
|
656 |
fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}" idx |
|
657 |
idx idx pp_c_dimension dim idx |
|
658 |
(aux (idx :: indices)) |
|
659 |
(Types.array_element_type typ) |
|
660 |
else |
|
661 |
let indices = List.rev indices in |
|
662 |
let pp_var_suffix fmt var = |
|
663 |
fprintf fmt "%a%a" (pp_c_var m "" pp_var) var pp_array_suffix |
|
664 |
indices |
|
665 |
in |
|
666 |
Mpfr.pp_inject_clear pp_var_suffix fmt var |
|
667 |
in |
|
668 |
reset_loop_counter (); |
|
669 |
aux [] fmt var.var_type |
|
670 |
|
|
671 |
let print_import_init fmt dep = |
|
672 |
let baseNAME = file_to_module_name dep.name in |
|
673 |
fprintf fmt "%a();" pp_global_init_name baseNAME |
|
674 |
|
|
675 |
let print_import_clear fmt dep = |
|
676 |
let baseNAME = file_to_module_name dep.name in |
|
677 |
fprintf fmt "%a();" pp_global_clear_name baseNAME |
|
678 |
|
|
679 |
let print_global_init_code fmt (basename, prog, dependencies) = |
|
680 |
let baseNAME = file_to_module_name basename in |
|
681 |
let constants = List.map const_of_top (get_consts prog) in |
|
700 | 682 |
fprintf fmt |
701 | 683 |
"@[<v 2>%a {@,\ |
702 |
%a%a@]@,\ |
|
684 |
static %s init = 0;@,\ |
|
685 |
@[<v 2>if (!init) { @,\ |
|
686 |
init = 1;%a%a@]@,\ |
|
703 | 687 |
}@,\ |
704 |
@[<v 2>%a {@,\ |
|
705 |
%a%a@]@,\ |
|
706 |
@," |
|
707 |
print_alloc_prototype (m.mname.node_id, m.mstatic) |
|
708 |
print_alloc_const m |
|
709 |
print_alloc_code m |
|
710 |
print_dealloc_prototype m.mname.node_id |
|
711 |
print_alloc_const m |
|
712 |
print_dealloc_code m |
|
713 |
|
|
714 |
let print_mpfr_code self fmt m = |
|
715 |
if !Options.mpfr then |
|
716 |
fprintf fmt "@,@[<v>%a@,%a@]" |
|
717 |
(* Init function *) |
|
718 |
(print_init_code self) m |
|
719 |
(* Clear function *) |
|
720 |
(print_clear_code self) m |
|
721 |
|
|
722 |
(* TODO: ACSL |
|
723 |
- a contract machine shall not be directly printed in the C source |
|
724 |
- but a regular machine associated to a contract machine shall integrate |
|
725 |
the associated statements, updating its memories, at the end of the |
|
726 |
function body. |
|
727 |
- last one may print intermediate comment/acsl if/when they are present in |
|
728 |
the sequence of instruction |
|
729 |
*) |
|
730 |
let print_machine machines dependencies fmt m = |
|
731 |
if fst (get_stateless_status m) then |
|
732 |
(* Step function *) |
|
733 |
print_stateless_code machines dependencies fmt m |
|
734 |
else |
|
735 |
let self = mk_self m in |
|
736 |
let mem = mk_mem m in |
|
737 |
fprintf fmt "@[<v>%a%a@,@,%a@,@,%a%a@]" |
|
738 |
print_alloc_function m |
|
739 |
(* Reset functions *) |
|
740 |
(print_clear_reset_code dependencies self mem) m |
|
741 |
(print_set_reset_code dependencies self mem) m |
|
688 |
return;@]@,\ |
|
689 |
}" |
|
690 |
print_global_init_prototype baseNAME |
|
691 |
(pp_c_basic_type_desc Type_predef.type_bool) |
|
692 |
(* constants *) |
|
693 |
(pp_print_list ~pp_prologue:pp_print_cut |
|
694 |
(pp_const_initialize empty_machine (pp_c_var_read empty_machine))) |
|
695 |
(mpfr_consts constants) |
|
696 |
(* dependencies initialization *) |
|
697 |
(pp_print_list ~pp_prologue:pp_print_cut print_import_init) |
|
698 |
(List.filter (fun dep -> dep.local) dependencies) |
|
699 |
|
|
700 |
let print_global_clear_code fmt (basename, prog, dependencies) = |
|
701 |
let baseNAME = file_to_module_name basename in |
|
702 |
let constants = List.map const_of_top (get_consts prog) in |
|
703 |
fprintf fmt |
|
704 |
"@[<v 2>%a {@,\ |
|
705 |
static %s clear = 0;@,\ |
|
706 |
@[<v 2>if (!clear) { @,\ |
|
707 |
clear = 1;%a%a@]@,\ |
|
708 |
}@,\ |
|
709 |
return;@]@,\ |
|
710 |
}" |
|
711 |
print_global_clear_prototype baseNAME |
|
712 |
(pp_c_basic_type_desc Type_predef.type_bool) |
|
713 |
(* constants *) |
|
714 |
(pp_print_list ~pp_prologue:pp_print_cut |
|
715 |
(pp_const_clear (pp_c_var_read empty_machine))) |
|
716 |
(mpfr_consts constants) |
|
717 |
(* dependencies initialization *) |
|
718 |
(pp_print_list ~pp_prologue:pp_print_cut print_import_clear) |
|
719 |
(List.filter (fun dep -> dep.local) dependencies) |
|
720 |
|
|
721 |
let print_alloc_function fmt m = |
|
722 |
if not !Options.static_mem then |
|
723 |
(* Alloc functions, only if non static mode *) |
|
724 |
fprintf fmt "@[<v 2>%a {@,%a%a@]@,}@,@[<v 2>%a {@,%a%a@]@,@," |
|
725 |
print_alloc_prototype |
|
726 |
(m.mname.node_id, m.mstatic) |
|
727 |
print_alloc_const m print_alloc_code m print_dealloc_prototype |
|
728 |
m.mname.node_id print_alloc_const m print_dealloc_code m |
|
729 |
|
|
730 |
let print_mpfr_code self fmt m = |
|
731 |
if !Options.mpfr then |
|
732 |
fprintf fmt "@,@[<v>%a@,%a@]" |
|
733 |
(* Init function *) |
|
734 |
(print_init_code self) |
|
735 |
m |
|
736 |
(* Clear function *) |
|
737 |
(print_clear_code self) |
|
738 |
m |
|
739 |
|
|
740 |
(* TODO: ACSL - a contract machine shall not be directly printed in the C |
|
741 |
source - but a regular machine associated to a contract machine shall |
|
742 |
integrate the associated statements, updating its memories, at the end of |
|
743 |
the function body. - last one may print intermediate comment/acsl if/when |
|
744 |
they are present in the sequence of instruction *) |
|
745 |
let print_machine machines dependencies fmt m = |
|
746 |
if fst (get_stateless_status m) then |
|
742 | 747 |
(* Step function *) |
743 |
(print_step_code machines dependencies self mem) m |
|
744 |
(print_mpfr_code self) m |
|
745 |
|
|
746 |
let print_import_standard source_fmt () = |
|
747 |
fprintf source_fmt |
|
748 |
"@[<v>#include <assert.h>@,%a%a%a@]" |
|
749 |
(if Machine_types.has_machine_type () |
|
750 |
then pp_print_endcut "#include <stdint.h>" |
|
751 |
else pp_print_nothing) () |
|
752 |
(if not !Options.static_mem |
|
753 |
then pp_print_endcut "#include <stdlib.h>" |
|
754 |
else pp_print_nothing) () |
|
755 |
(if !Options.mpfr |
|
756 |
then pp_print_endcut "#include <mpfr.h>" |
|
757 |
else pp_print_nothing) () |
|
758 |
|
|
759 |
let print_extern_alloc_prototype fmt ind = |
|
760 |
let static = List.filter (fun v -> v.var_dec_const) ind.nodei_inputs in |
|
761 |
fprintf fmt "extern %a;@,extern %a;" |
|
762 |
print_alloc_prototype (ind.nodei_id, static) |
|
763 |
print_dealloc_prototype ind.nodei_id |
|
764 |
|
|
765 |
let print_lib_c source_fmt basename prog machines dependencies = |
|
766 |
fprintf source_fmt |
|
767 |
"@[<v>\ |
|
768 |
%a\ |
|
769 |
%a@,\ |
|
770 |
@,\ |
|
771 |
%a@,\ |
|
772 |
%a\ |
|
773 |
%a\ |
|
774 |
%a\ |
|
775 |
%a\ |
|
776 |
%a\ |
|
777 |
%a\ |
|
778 |
%a\ |
|
779 |
@]@." |
|
780 |
print_import_standard () |
|
781 |
print_import_prototype |
|
782 |
{ |
|
783 |
local = true; |
|
784 |
name = basename; |
|
785 |
content = []; |
|
786 |
is_stateful=true (* assuming it is stateful *); |
|
787 |
} |
|
788 |
|
|
789 |
(* Print the svn version number and the supported C standard (C90 or C99) *) |
|
790 |
pp_print_version () |
|
791 |
|
|
792 |
(* Print dependencies *) |
|
793 |
(pp_print_list |
|
794 |
~pp_open_box:pp_open_vbox0 |
|
795 |
~pp_prologue:(pp_print_endcut "/* Import dependencies */") |
|
796 |
print_import_prototype |
|
797 |
~pp_epilogue:pp_print_cutcut) dependencies |
|
798 |
|
|
799 |
(* Print consts *) |
|
800 |
(pp_print_list |
|
801 |
~pp_open_box:pp_open_vbox0 |
|
802 |
~pp_prologue:(pp_print_endcut "/* Global constants (definitions) */") |
|
803 |
print_const_def |
|
804 |
~pp_epilogue:pp_print_cutcut) (get_consts prog) |
|
805 |
|
|
806 |
(* MPFR *) |
|
807 |
(if !Options.mpfr then |
|
808 |
fun fmt () -> |
|
809 |
fprintf fmt |
Also available in: Unified diff
reformatting