lustrec / src / c_backend.ml @ fa090c4e
History | View | Annotate | Download (40.2 KB)
1 |
(* ---------------------------------------------------------------------------- |
---|---|
2 |
* SchedMCore - A MultiCore Scheduling Framework |
3 |
* Copyright (C) 2009-2013, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE |
4 |
* Copyright (C) 2012-2013, INPT, Toulouse, FRANCE |
5 |
* |
6 |
* This file is part of Prelude |
7 |
* |
8 |
* Prelude is free software; you can redistribute it and/or |
9 |
* modify it under the terms of the GNU Lesser General Public License |
10 |
* as published by the Free Software Foundation ; either version 2 of |
11 |
* the License, or (at your option) any later version. |
12 |
* |
13 |
* Prelude is distributed in the hope that it will be useful, but |
14 |
* WITHOUT ANY WARRANTY ; without even the implied warranty of |
15 |
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU |
16 |
* Lesser General Public License for more details. |
17 |
* |
18 |
* You should have received a copy of the GNU Lesser General Public |
19 |
* License along with this program ; if not, write to the Free Software |
20 |
* Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 |
21 |
* USA |
22 |
*---------------------------------------------------------------------------- *) |
23 |
|
24 |
(* This module is used for the lustre to C compiler *) |
25 |
|
26 |
open Format |
27 |
open LustreSpec |
28 |
open Corelang |
29 |
open Machine_code |
30 |
|
31 |
(********************************************************************************************) |
32 |
(* Basic Printing functions *) |
33 |
(********************************************************************************************) |
34 |
|
35 |
let print_version fmt = |
36 |
Format.fprintf fmt "/* @[<v>C code generated by %s@,SVN version number %s@,Code is %s compliant */@,@]@." |
37 |
(Filename.basename Sys.executable_name) Version.number (if !Options.ansi then "ANSI C90" else "C99") |
38 |
|
39 |
(* Generation of a non-clashing name for the self memory variable (for step and reset functions) *) |
40 |
let mk_self m = |
41 |
mk_new_name (m.mstep.step_inputs@m.mstep.step_outputs@m.mstep.step_locals@m.mmemory) "self" |
42 |
|
43 |
(* Generation of a non-clashing name for the instance variable of static allocation macro *) |
44 |
let mk_instance m = |
45 |
mk_new_name (m.mstep.step_inputs@m.mmemory) "inst" |
46 |
|
47 |
(* Generation of a non-clashing name for the attribute variable of static allocation macro *) |
48 |
let mk_attribute m = |
49 |
mk_new_name (m.mstep.step_inputs@m.mmemory) "attr" |
50 |
|
51 |
let mk_call_var_decl loc id = |
52 |
{ var_id = id; |
53 |
var_dec_type = mktyp Location.dummy_loc Tydec_any; |
54 |
var_dec_clock = mkclock Location.dummy_loc Ckdec_any; |
55 |
var_dec_const = false; |
56 |
var_type = Type_predef.type_arrow (Types.new_var ()) (Types.new_var ()); |
57 |
var_clock = Clocks.new_var true; |
58 |
var_loc = loc } |
59 |
|
60 |
(* counter for loop variable creation *) |
61 |
let loop_cpt = ref (-1) |
62 |
|
63 |
let reset_loop_counter () = |
64 |
loop_cpt := -1 |
65 |
|
66 |
let mk_loop_var m () = |
67 |
let vars = m.mstep.step_inputs@m.mstep.step_outputs@m.mstep.step_locals@m.mmemory in |
68 |
let rec aux () = |
69 |
incr loop_cpt; |
70 |
let s = Printf.sprintf "__%s_%d" "i" !loop_cpt in |
71 |
if List.exists (fun v -> v.var_id = s) vars then aux () else s |
72 |
in aux () |
73 |
(* |
74 |
let addr_cpt = ref (-1) |
75 |
|
76 |
let reset_addr_counter () = |
77 |
addr_cpt := -1 |
78 |
|
79 |
let mk_addr_var m var = |
80 |
let vars = m.mmemory in |
81 |
let rec aux () = |
82 |
incr addr_cpt; |
83 |
let s = Printf.sprintf "%s_%s_%d" var "addr" !addr_cpt in |
84 |
if List.exists (fun v -> v.var_id = s) vars then aux () else s |
85 |
in aux () |
86 |
*) |
87 |
let pp_machine_memtype_name fmt id = fprintf fmt "struct %s_mem" id |
88 |
let pp_machine_regtype_name fmt id = fprintf fmt "struct %s_reg" id |
89 |
let pp_machine_alloc_name fmt id = fprintf fmt "%s_alloc" id |
90 |
let pp_machine_static_declare_name fmt id = fprintf fmt "%s_DECLARE" id |
91 |
let pp_machine_static_link_name fmt id = fprintf fmt "%s_LINK" id |
92 |
let pp_machine_static_alloc_name fmt id = fprintf fmt "%s_ALLOC" id |
93 |
let pp_machine_reset_name fmt id = fprintf fmt "%s_reset" id |
94 |
let pp_machine_step_name fmt id = fprintf fmt "%s_step" id |
95 |
|
96 |
let pp_c_dimension fmt d = |
97 |
fprintf fmt "%a" Dimension.pp_dimension d |
98 |
|
99 |
let pp_c_type var fmt t = |
100 |
let rec aux t pp_suffix = |
101 |
match (Types.repr t).Types.tdesc with |
102 |
| Types.Tclock t' -> aux t' pp_suffix |
103 |
| Types.Tbool -> fprintf fmt "_Bool %s%a" var pp_suffix () |
104 |
| Types.Treal -> fprintf fmt "double %s%a" var pp_suffix () |
105 |
| Types.Tint -> fprintf fmt "int %s%a" var pp_suffix () |
106 |
| Types.Tarray (d, t') -> |
107 |
let pp_suffix' fmt () = fprintf fmt "%a[%a]" pp_suffix () pp_c_dimension d in |
108 |
aux t' pp_suffix' |
109 |
| Types.Tstatic (_, t') -> fprintf fmt "const "; aux t' pp_suffix |
110 |
| Types.Tconst ty -> fprintf fmt "%s %s" ty var |
111 |
| Types.Tarrow (_, _) -> fprintf fmt "void (*%s)()" var |
112 |
| _ -> eprintf "internal error: pp_c_type %a@." Types.print_ty t; assert false |
113 |
in aux t (fun fmt () -> ()) |
114 |
|
115 |
let rec pp_c_initialize fmt t = |
116 |
match (Types.repr t).Types.tdesc with |
117 |
| Types.Tint -> pp_print_string fmt "0" |
118 |
| Types.Tclock t' -> pp_c_initialize fmt t' |
119 |
| Types.Tbool -> pp_print_string fmt "0" |
120 |
| Types.Treal -> pp_print_string fmt "0." |
121 |
| Types.Tarray (d, t') when Dimension.is_dimension_const d -> |
122 |
fprintf fmt "{%a}" |
123 |
(Utils.fprintf_list ~sep:"," (fun fmt _ -> pp_c_initialize fmt t')) |
124 |
(Utils.duplicate 0 (Dimension.size_const_dimension d)) |
125 |
| _ -> assert false |
126 |
|
127 |
(* Declaration of an input variable: |
128 |
- if its type is array/matrix/etc, then declare it as a mere pointer, |
129 |
in order to cope with unknown/parametric array dimensions, |
130 |
as it is the case for generics |
131 |
*) |
132 |
let pp_c_decl_input_var fmt id = |
133 |
if !Options.ansi && Types.is_array_type id.var_type |
134 |
then pp_c_type (sprintf "(*%s)" id.var_id) fmt (Types.array_base_type id.var_type) |
135 |
else pp_c_type id.var_id fmt id.var_type |
136 |
|
137 |
(* Declaration of an output variable: |
138 |
- if its type is scalar, then pass its address |
139 |
- if its type is array/matrix/etc, then declare it as a mere pointer, |
140 |
in order to cope with unknown/parametric array dimensions, |
141 |
as it is the case for generics |
142 |
*) |
143 |
let pp_c_decl_output_var fmt id = |
144 |
if (not !Options.ansi) && Types.is_array_type id.var_type |
145 |
then pp_c_type id.var_id fmt id.var_type |
146 |
else pp_c_type (sprintf "(*%s)" id.var_id) fmt (Types.array_base_type id.var_type) |
147 |
|
148 |
(* Declaration of a local/mem variable: |
149 |
- if it's an array/matrix/etc, its size(s) should be |
150 |
known in order to statically allocate memory, |
151 |
so we print the full type |
152 |
*) |
153 |
let pp_c_decl_local_var fmt id = |
154 |
pp_c_type id.var_id fmt id.var_type |
155 |
|
156 |
let pp_c_decl_array_mem self fmt id = |
157 |
fprintf fmt "%a = (%a) (%s->_reg.%s)" |
158 |
(pp_c_type (sprintf "(*%s)" id.var_id)) id.var_type |
159 |
(pp_c_type "(*)") id.var_type |
160 |
self |
161 |
id.var_id |
162 |
|
163 |
(* Declaration of a struct variable: |
164 |
- if it's an array/matrix/etc, we declare it as a pointer |
165 |
*) |
166 |
let pp_c_decl_struct_var fmt id = |
167 |
if Types.is_array_type id.var_type |
168 |
then pp_c_type (sprintf "(*%s)" id.var_id) fmt (Types.array_base_type id.var_type) |
169 |
else pp_c_type id.var_id fmt id.var_type |
170 |
|
171 |
(* Access to the value of a variable: |
172 |
- if it's not a scalar output, then its name is enough |
173 |
- otherwise, dereference it (it has been declared as a pointer, |
174 |
despite its scalar Lustre type) |
175 |
- moreover, cast arrays variables into their original array type. |
176 |
*) |
177 |
let pp_c_var_read m fmt id = |
178 |
if Types.is_array_type id.var_type |
179 |
then |
180 |
fprintf fmt "%s" id.var_id |
181 |
else |
182 |
if List.exists (fun o -> o.var_id = id.var_id) m.mstep.step_outputs (* id is output *) |
183 |
then fprintf fmt "*%s" id.var_id |
184 |
else fprintf fmt "%s" id.var_id |
185 |
|
186 |
(* Addressable value of a variable, the one that is passed around in calls: |
187 |
- if it's not a scalar non-output, then its name is enough |
188 |
- otherwise, reference it (it must be passed as a pointer, |
189 |
despite its scalar Lustre type) |
190 |
*) |
191 |
let pp_c_var_write m fmt id = |
192 |
if Types.is_array_type id.var_type |
193 |
then |
194 |
fprintf fmt "%s" id.var_id |
195 |
else |
196 |
if List.exists (fun o -> o.var_id = id.var_id) m.mstep.step_outputs (* id is output *) |
197 |
then |
198 |
fprintf fmt "%s" id.var_id |
199 |
else |
200 |
fprintf fmt "&%s" id.var_id |
201 |
|
202 |
let pp_c_decl_instance_var fmt (name, (node, static)) = |
203 |
fprintf fmt "%a *%s" pp_machine_memtype_name (node_name node) name |
204 |
|
205 |
let pp_c_tag fmt t = |
206 |
pp_print_string fmt (if t = tag_true then "1" else if t = tag_false then "0" else t) |
207 |
|
208 |
(* Prints a constant value *) |
209 |
let rec pp_c_const fmt c = |
210 |
match c with |
211 |
| Const_int i -> pp_print_int fmt i |
212 |
| Const_real r -> pp_print_string fmt r |
213 |
| Const_float r -> pp_print_float fmt r |
214 |
| Const_tag t -> pp_c_tag fmt t |
215 |
| Const_array ca -> fprintf fmt "{%a}" (Utils.fprintf_list ~sep:"," pp_c_const) ca |
216 |
|
217 |
(* Prints a value expression [v], with internal function calls only. |
218 |
[pp_var] is a printer for variables (typically [pp_c_var_read]), |
219 |
but an offset suffix may be added for array variables |
220 |
*) |
221 |
let rec pp_c_val self pp_var fmt v = |
222 |
match v with |
223 |
| Cst c -> pp_c_const fmt c |
224 |
| Array vl -> fprintf fmt "{%a}" (Utils.fprintf_list ~sep:", " (pp_c_val self pp_var)) vl |
225 |
| Access (t, i) -> fprintf fmt "%a[%a]" (pp_c_val self pp_var) t (pp_c_val self pp_var) i |
226 |
| Power (v, n) -> assert false |
227 |
| LocalVar v -> pp_var fmt v |
228 |
| StateVar v -> |
229 |
if Types.is_array_type v.var_type |
230 |
then fprintf fmt "*%a" pp_var v |
231 |
else fprintf fmt "%s->_reg.%a" self pp_var v |
232 |
| Fun (n, vl) -> Basic_library.pp_c n (pp_c_val self pp_var) fmt vl |
233 |
|
234 |
let pp_c_checks self fmt m = |
235 |
Utils.fprintf_list ~sep:"" (fun fmt (loc, check) -> fprintf fmt "@[<v>%a@,assert (%a);@]@," Location.pp_c_loc loc (pp_c_val self (pp_c_var_read m)) check) fmt m.mstep.step_checks |
236 |
|
237 |
|
238 |
(********************************************************************************************) |
239 |
(* Instruction Printing functions *) |
240 |
(********************************************************************************************) |
241 |
|
242 |
(* Computes the depth to which multi-dimension array assignments should be expanded. |
243 |
It equals the maximum number of nested static array constructions accessible from root [v]. |
244 |
*) |
245 |
let rec expansion_depth v = |
246 |
match v with |
247 |
| Cst (Const_array cl) -> 1 + List.fold_right (fun c -> max (expansion_depth (Cst c))) cl 0 |
248 |
| Cst _ |
249 |
| LocalVar _ |
250 |
| StateVar _ -> 0 |
251 |
| Fun (_, vl) -> List.fold_right (fun v -> max (expansion_depth v)) vl 0 |
252 |
| Array vl -> 1 + List.fold_right (fun v -> max (expansion_depth v)) vl 0 |
253 |
| Access (v, i) -> max 0 (expansion_depth v - 1) |
254 |
| Power (v, n) -> 0 (*1 + expansion_depth v*) |
255 |
|
256 |
type loop_index = LVar of ident | LInt of int ref |
257 |
|
258 |
(* Computes the list of nested loop variables together with their dimension bounds. |
259 |
- LInt r stands for loop expansion (no loop variable, but int loop index) |
260 |
- LVar v stands for loop variable v |
261 |
*) |
262 |
let rec mk_loop_variables m ty depth = |
263 |
match (Types.repr ty).Types.tdesc, depth with |
264 |
| Types.Tarray (d, ty'), 0 -> |
265 |
let v = mk_loop_var m () in |
266 |
(d, LVar v) :: mk_loop_variables m ty' 0 |
267 |
| Types.Tarray (d, ty'), _ -> |
268 |
let r = ref (-1) in |
269 |
(d, LInt r) :: mk_loop_variables m ty' (depth - 1) |
270 |
| _ , 0 -> [] |
271 |
| _ -> assert false |
272 |
|
273 |
let reorder_loop_variables loop_vars = |
274 |
let (int_loops, var_loops) = List.partition (function (d, LInt _) -> true | _ -> false) loop_vars in |
275 |
var_loops @ int_loops |
276 |
|
277 |
(* Prints a one loop variable suffix for arrays *) |
278 |
let pp_loop_var fmt lv = |
279 |
match snd lv with |
280 |
| LVar v -> fprintf fmt "[%s]" v |
281 |
| LInt r -> fprintf fmt "[%d]" !r |
282 |
|
283 |
(* Prints a suffix of loop variables for arrays *) |
284 |
let pp_suffix fmt loop_vars = |
285 |
Utils.fprintf_list ~sep:"" pp_loop_var fmt loop_vars |
286 |
|
287 |
(* Prints a [value] indexed by the suffix list [loop_vars] *) |
288 |
let rec pp_value_suffix self loop_vars pp_value fmt value = |
289 |
match loop_vars, value with |
290 |
| (_, LInt r) :: q, Array vl -> |
291 |
pp_value_suffix self q pp_value fmt (List.nth vl !r) |
292 |
| _ :: q, Power (v, n) -> |
293 |
pp_value_suffix self loop_vars pp_value fmt v |
294 |
| _ , Fun (n, vl) -> |
295 |
Basic_library.pp_c n (pp_value_suffix self loop_vars pp_value) fmt vl |
296 |
| _ , _ -> |
297 |
let pp_var_suffix fmt v = fprintf fmt "%a%a" pp_value v pp_suffix loop_vars in |
298 |
pp_c_val self pp_var_suffix fmt value |
299 |
|
300 |
(* type_directed assignment: array vs. statically sized type |
301 |
- [var_type]: type of variable to be assigned |
302 |
- [var_name]: name of variable to be assigned |
303 |
- [value]: assigned value |
304 |
- [pp_var]: printer for variables |
305 |
*) |
306 |
let pp_assign m self pp_var fmt var_type var_name value = |
307 |
let depth = expansion_depth value in |
308 |
(*eprintf "pp_assign %a %a %d@." Types.print_ty var_type pp_val value depth;*) |
309 |
let loop_vars = mk_loop_variables m var_type depth in |
310 |
let reordered_loop_vars = reorder_loop_variables loop_vars in |
311 |
let rec aux fmt vars = |
312 |
match vars with |
313 |
| [] -> |
314 |
fprintf fmt "%a = %a;" (pp_value_suffix self loop_vars pp_var) var_name (pp_value_suffix self loop_vars pp_var) value |
315 |
| (d, LVar i) :: q -> |
316 |
(*eprintf "pp_aux %a %s@." Dimension.pp_dimension d i;*) |
317 |
fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}" |
318 |
i i i Dimension.pp_dimension d i |
319 |
aux q |
320 |
| (d, LInt r) :: q -> |
321 |
(*eprintf "pp_aux %a %d@." Dimension.pp_dimension d (!r);*) |
322 |
let szl = Utils.enumerate (Dimension.size_const_dimension d) in |
323 |
fprintf fmt "@[<v 2>{@,%a@]@,}" |
324 |
(Utils.fprintf_list ~sep:"@," (fun fmt i -> r := i; aux fmt q)) szl |
325 |
in |
326 |
begin |
327 |
reset_loop_counter (); |
328 |
(*reset_addr_counter ();*) |
329 |
aux fmt reordered_loop_vars |
330 |
end |
331 |
|
332 |
let pp_instance_call m self fmt i (inputs: value_t list) (outputs: var_decl list) = |
333 |
try (* stateful node instance *) |
334 |
let (n,_) = List.assoc i m.minstances in |
335 |
fprintf fmt "%s_step (%a%t%a%t%s->%s);" |
336 |
(node_name n) |
337 |
(Utils.fprintf_list ~sep:", " (pp_c_val self (pp_c_var_read m))) inputs |
338 |
(Utils.pp_final_char_if_non_empty ", " inputs) |
339 |
(Utils.fprintf_list ~sep:", " (pp_c_var_write m)) outputs |
340 |
(Utils.pp_final_char_if_non_empty ", " outputs) |
341 |
self |
342 |
i |
343 |
with Not_found -> (* stateless node instance *) |
344 |
let (n,_) = List.assoc i m.mcalls in |
345 |
fprintf fmt "%s (%a%t%a);" |
346 |
(node_name n) |
347 |
(Utils.fprintf_list ~sep:", " (pp_c_val self (pp_c_var_read m))) inputs |
348 |
(Utils.pp_final_char_if_non_empty ", " inputs) |
349 |
(Utils.fprintf_list ~sep:", " (pp_c_var_write m)) outputs |
350 |
|
351 |
let pp_machine_reset (m: machine_t) self fmt inst = |
352 |
let (node, static) = List.assoc inst m.minstances in |
353 |
fprintf fmt "%a(%a%t%s->%s);" |
354 |
pp_machine_reset_name (node_name node) |
355 |
(Utils.fprintf_list ~sep:", " Dimension.pp_dimension) static |
356 |
(Utils.pp_final_char_if_non_empty ", " static) |
357 |
self inst |
358 |
|
359 |
let rec pp_conditional (m: machine_t) self fmt c tl el = |
360 |
fprintf fmt "@[<v 2>if (%a) {%t%a@]@,@[<v 2>} else {%t%a@]@,}" |
361 |
(pp_c_val self (pp_c_var_read m)) c |
362 |
(Utils.pp_newline_if_non_empty tl) |
363 |
(Utils.fprintf_list ~sep:"@," (pp_machine_instr m self)) tl |
364 |
(Utils.pp_newline_if_non_empty el) |
365 |
(Utils.fprintf_list ~sep:"@," (pp_machine_instr m self)) el |
366 |
|
367 |
and pp_machine_instr (m: machine_t) self fmt instr = |
368 |
match instr with |
369 |
| MReset i -> |
370 |
pp_machine_reset m self fmt i |
371 |
| MLocalAssign (i,v) -> |
372 |
pp_assign |
373 |
m self (pp_c_var_read m) fmt |
374 |
i.var_type (LocalVar i) v |
375 |
| MStateAssign (i,v) -> |
376 |
pp_assign |
377 |
m self (pp_c_var_read m) fmt |
378 |
i.var_type (StateVar i) v |
379 |
| MStep ([i0], i, vl) when Basic_library.is_internal_fun i -> |
380 |
pp_machine_instr m self fmt (MLocalAssign (i0, Fun (i, vl))) |
381 |
| MStep (il, i, vl) -> |
382 |
pp_instance_call m self fmt i vl il |
383 |
| MBranch (g,hl) -> |
384 |
if hl <> [] && let t = fst (List.hd hl) in t = tag_true || t = tag_false |
385 |
then (* boolean case, needs special treatment in C because truth value is not unique *) |
386 |
(* may disappear if we optimize code by replacing last branch test with default *) |
387 |
let tl = try List.assoc tag_true hl with Not_found -> [] in |
388 |
let el = try List.assoc tag_false hl with Not_found -> [] in |
389 |
pp_conditional m self fmt g tl el |
390 |
else (* enum type case *) |
391 |
fprintf fmt "@[<v 2>switch(%a) {@,%a@,}@]" |
392 |
(pp_c_val self (pp_c_var_read m)) g |
393 |
(Utils.fprintf_list ~sep:"@," (pp_machine_branch m self)) hl |
394 |
|
395 |
and pp_machine_branch m self fmt (t, h) = |
396 |
fprintf fmt "@[<v 2>case %a:@,%a@,break;@]" pp_c_tag t (Utils.fprintf_list ~sep:"@," (pp_machine_instr m self)) h |
397 |
|
398 |
|
399 |
(**************************************************************************) |
400 |
(* Printing spec for c *) |
401 |
|
402 |
(**************************************************************************) |
403 |
|
404 |
|
405 |
let pp_econst fmt c = |
406 |
match c with |
407 |
| EConst_int i -> pp_print_int fmt i |
408 |
| EConst_real r -> pp_print_string fmt r |
409 |
| EConst_float r -> pp_print_float fmt r |
410 |
| EConst_bool b -> pp_print_bool fmt b |
411 |
| EConst_string s -> pp_print_string fmt ("\"" ^ s ^ "\"") |
412 |
|
413 |
let rec pp_eexpr is_output fmt eexpr = |
414 |
let pp_eexpr = pp_eexpr is_output in |
415 |
match eexpr.eexpr_desc with |
416 |
| EExpr_const c -> pp_econst fmt c |
417 |
| EExpr_ident id -> |
418 |
if is_output id then pp_print_string fmt ("*" ^ id) else pp_print_string fmt id |
419 |
| EExpr_tuple el -> Utils.fprintf_list ~sep:"," pp_eexpr fmt el |
420 |
| EExpr_arrow (e1, e2) -> fprintf fmt "%a -> %a" pp_eexpr e1 pp_eexpr e2 |
421 |
| EExpr_fby (e1, e2) -> fprintf fmt "%a fby %a" pp_eexpr e1 pp_eexpr e2 |
422 |
(* | EExpr_concat (e1, e2) -> fprintf fmt "%a::%a" pp_eexpr e1 pp_eexpr e2 *) |
423 |
(* | EExpr_tail e -> fprintf fmt "tail %a" pp_eexpr e *) |
424 |
| EExpr_pre e -> fprintf fmt "pre %a" pp_eexpr e |
425 |
| EExpr_when (e, id) -> fprintf fmt "%a when %s" pp_eexpr e id |
426 |
| EExpr_merge (id, e1, e2) -> |
427 |
fprintf fmt "merge (%s, %a, %a)" id pp_eexpr e1 pp_eexpr e2 |
428 |
| EExpr_appl (id, e, r) -> pp_eapp is_output fmt id e r |
429 |
| EExpr_forall (vars, e) -> fprintf fmt "forall %a; %a" Printers.pp_node_args vars pp_eexpr e |
430 |
| EExpr_exists (vars, e) -> fprintf fmt "exists %a; %a" Printers.pp_node_args vars pp_eexpr e |
431 |
|
432 |
|
433 |
(* | EExpr_whennot _ *) |
434 |
(* | EExpr_uclock _ *) |
435 |
(* | EExpr_dclock _ *) |
436 |
(* | EExpr_phclock _ -> assert false *) |
437 |
and pp_eapp is_output fmt id e r = |
438 |
let pp_eexpr = pp_eexpr is_output in |
439 |
match r with |
440 |
| None -> |
441 |
(match id, e.eexpr_desc with |
442 |
| "+", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a + %a)" pp_eexpr e1 pp_eexpr e2 |
443 |
| "uminus", _ -> fprintf fmt "(- %a)" pp_eexpr e |
444 |
| "-", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a - %a)" pp_eexpr e1 pp_eexpr e2 |
445 |
| "*", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a * %a)" pp_eexpr e1 pp_eexpr e2 |
446 |
| "/", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a / %a)" pp_eexpr e1 pp_eexpr e2 |
447 |
| "mod", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a mod %a)" pp_eexpr e1 pp_eexpr e2 |
448 |
| "&&", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a && %a)" pp_eexpr e1 pp_eexpr e2 |
449 |
| "||", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a || %a)" pp_eexpr e1 pp_eexpr e2 |
450 |
| "xor", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a ^^ %a)" pp_eexpr e1 pp_eexpr e2 |
451 |
| "impl", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a ==> %a)" pp_eexpr e1 pp_eexpr e2 |
452 |
| "<", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a < %a)" pp_eexpr e1 pp_eexpr e2 |
453 |
| "<=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a <= %a)" pp_eexpr e1 pp_eexpr e2 |
454 |
| ">", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a > %a)" pp_eexpr e1 pp_eexpr e2 |
455 |
| ">=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a >= %a)" pp_eexpr e1 pp_eexpr e2 |
456 |
| "!=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a != %a)" pp_eexpr e1 pp_eexpr e2 |
457 |
| "=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a == %a)" pp_eexpr e1 pp_eexpr e2 |
458 |
| "not", _ -> fprintf fmt "(! %a)" pp_eexpr e |
459 |
| "ite", EExpr_tuple([e1;e2;e3]) -> fprintf fmt "(if %a then %a else %a)" pp_eexpr e1 pp_eexpr e2 pp_eexpr e3 |
460 |
| _ -> fprintf fmt "%s (%a)" id pp_eexpr e) |
461 |
| Some x -> fprintf fmt "%s (%a) every %s" id pp_eexpr e x |
462 |
|
463 |
let pp_ensures is_output fmt e = |
464 |
match e with |
465 |
| EnsuresExpr e -> fprintf fmt "ensures %a;@ " (pp_eexpr is_output) e |
466 |
| SpecObserverNode (name, args) -> fprintf fmt "observer %s (%a);@ " name (Utils.fprintf_list ~sep:", " (pp_eexpr is_output)) args |
467 |
|
468 |
let pp_acsl_spec outputs fmt spec = |
469 |
let is_output = fun oid -> List.exists (fun v -> v.var_id = oid) outputs in |
470 |
let pp_eexpr = pp_eexpr is_output in |
471 |
fprintf fmt "@[<v 2>/*@@ "; |
472 |
Utils.fprintf_list ~sep:"" (fun fmt r -> fprintf fmt "requires %a;@ " pp_eexpr r) fmt spec.requires; |
473 |
Utils.fprintf_list ~sep:"" (pp_ensures is_output) fmt spec.ensures; |
474 |
fprintf fmt "@ "; |
475 |
(* fprintf fmt "assigns *self%t%a;@ " *) |
476 |
(* (fun fmt -> if List.length outputs > 0 then fprintf fmt ", ") *) |
477 |
(* (fprintf_list ~sep:"," (fun fmt v -> fprintf fmt "*%s" v.var_id)) outputs; *) |
478 |
Utils.fprintf_list ~sep:"@ " (fun fmt (name, assumes, requires) -> |
479 |
fprintf fmt "behavior %s:@[@ %a@ %a@]" |
480 |
name |
481 |
(Utils.fprintf_list ~sep:"@ " (fun fmt r -> fprintf fmt "assumes %a;" pp_eexpr r)) assumes |
482 |
(Utils.fprintf_list ~sep:"@ " (pp_ensures is_output)) requires |
483 |
) fmt spec.behaviors; |
484 |
fprintf fmt "@]@ */@."; |
485 |
() |
486 |
|
487 |
(********************************************************************************************) |
488 |
(* Prototype Printing functions *) |
489 |
(********************************************************************************************) |
490 |
|
491 |
let print_alloc_prototype fmt (name, static) = |
492 |
fprintf fmt "%a * %a (%a)" |
493 |
pp_machine_memtype_name name |
494 |
pp_machine_alloc_name name |
495 |
(Utils.fprintf_list ~sep:",@ " pp_c_decl_input_var) static |
496 |
|
497 |
let print_reset_prototype self fmt (name, static) = |
498 |
fprintf fmt "void %a (@[<v>%a%t%a *%s@])" |
499 |
pp_machine_reset_name name |
500 |
(Utils.fprintf_list ~sep:",@ " pp_c_decl_input_var) static |
501 |
(Utils.pp_final_char_if_non_empty ",@," static) |
502 |
pp_machine_memtype_name name |
503 |
self |
504 |
|
505 |
let print_stateless_prototype fmt (name, inputs, outputs) = |
506 |
match outputs with |
507 |
(* DOESN'T WORK FOR ARRAYS |
508 |
| [o] -> fprintf fmt "%a (@[<v>%a@])" |
509 |
(pp_c_type name) o.var_type |
510 |
(Utils.fprintf_list ~sep:",@ " pp_c_var) inputs |
511 |
*) |
512 |
| _ -> fprintf fmt "void %s (@[<v>@[%a%t@]@,@[%a@]@,@])" |
513 |
name |
514 |
(Utils.fprintf_list ~sep:",@ " pp_c_decl_input_var) inputs |
515 |
(Utils.pp_final_char_if_non_empty ",@ " inputs) |
516 |
(Utils.fprintf_list ~sep:",@ " pp_c_decl_output_var) outputs |
517 |
|
518 |
let print_step_prototype self fmt (name, inputs, outputs) = |
519 |
fprintf fmt "void %a (@[<v>@[%a%t@]@,@[%a@]%t@[%a *%s@]@])" |
520 |
pp_machine_step_name name |
521 |
(Utils.fprintf_list ~sep:",@ " pp_c_decl_input_var) inputs |
522 |
(Utils.pp_final_char_if_non_empty ",@ " inputs) |
523 |
(Utils.fprintf_list ~sep:",@ " pp_c_decl_output_var) outputs |
524 |
(Utils.pp_final_char_if_non_empty ",@," outputs) |
525 |
pp_machine_memtype_name name |
526 |
self |
527 |
|
528 |
(********************************************************************************************) |
529 |
(* Header Printing functions *) |
530 |
(********************************************************************************************) |
531 |
|
532 |
(* Removed because of "open" constructs. No more extern functions *) |
533 |
(* |
534 |
let print_prototype fmt decl = |
535 |
match decl.top_decl_desc with |
536 |
| ImportedFun m -> ( |
537 |
fprintf fmt "extern %a;@," |
538 |
print_stateless_prototype |
539 |
(m.fun_id, m.fun_inputs, m.fun_outputs) |
540 |
) |
541 |
| ImportedNode m -> ( |
542 |
if m.nodei_stateless then (* It's a function not a node *) |
543 |
fprintf fmt "extern %a;@," |
544 |
print_stateless_prototype |
545 |
(m.nodei_id, m.nodei_inputs, m.nodei_outputs) |
546 |
else ( |
547 |
let static = List.filter (fun v -> v.var_dec_const) m.nodei_inputs in |
548 |
fprintf fmt "extern %a;@," |
549 |
print_alloc_prototype (m.nodei_id, static); |
550 |
fprintf fmt "extern %a;@," |
551 |
(print_reset_prototype "self") (m.nodei_id, static); |
552 |
fprintf fmt "extern %a;@," |
553 |
(print_step_prototype "self") (m.nodei_id, m.nodei_inputs, m.nodei_outputs); |
554 |
) |
555 |
) |
556 |
| _ -> () (* We don't do anything here *) |
557 |
*) |
558 |
|
559 |
let print_import_standard fmt = |
560 |
fprintf fmt "#include \"%s/include/lustrec/arrow.h\"@.@." Version.prefix |
561 |
|
562 |
let print_prototype fmt decl = |
563 |
match decl.top_decl_desc with |
564 |
| Open m -> fprintf fmt "#include \"%s.h\"@," m |
565 |
| _ -> () (* We don't do anything here *) |
566 |
|
567 |
let pp_registers_struct fmt m = |
568 |
if m.mmemory <> [] |
569 |
then |
570 |
fprintf fmt "@[%a {@[%a; @]}@] _reg; " |
571 |
pp_machine_regtype_name m.mname.node_id |
572 |
(Utils.fprintf_list ~sep:"; " pp_c_decl_struct_var) m.mmemory |
573 |
else |
574 |
() |
575 |
|
576 |
let print_machine_struct fmt m = |
577 |
if m.mname.node_id != arrow_id |
578 |
then ( |
579 |
(* We don't print arrow function *) |
580 |
(* Define struct *) |
581 |
fprintf fmt "@[%a {@[%a%a%t@]};@]@." |
582 |
pp_machine_memtype_name m.mname.node_id |
583 |
pp_registers_struct m |
584 |
(Utils.fprintf_list ~sep:"; " pp_c_decl_instance_var) m.minstances |
585 |
(Utils.pp_final_char_if_non_empty "; " m.minstances) |
586 |
) |
587 |
|
588 |
(* |
589 |
let pp_static_array_instance fmt m (v, m) = |
590 |
fprintf fmt "%s" (mk_addr_var m v) |
591 |
*) |
592 |
let print_static_declare_instance attr fmt (i, (m, static)) = |
593 |
fprintf fmt "%a(%s, %a%t%s)" |
594 |
pp_machine_static_declare_name (node_name m) |
595 |
attr |
596 |
(Utils.fprintf_list ~sep:", " Dimension.pp_dimension) static |
597 |
(Utils.pp_final_char_if_non_empty ", " static) |
598 |
i |
599 |
|
600 |
let print_static_declare_macro fmt m = |
601 |
let array_mem = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in |
602 |
let inst = mk_instance m in |
603 |
let attr = mk_attribute m in |
604 |
fprintf fmt "@[<v 2>#define %a(%s, %a%tinst)\\@,%s %a inst;\\@,%a%t%a;@,@]" |
605 |
pp_machine_static_declare_name m.mname.node_id |
606 |
attr |
607 |
(Utils.fprintf_list ~sep:", " (pp_c_var_read m)) m.mstatic |
608 |
(Utils.pp_final_char_if_non_empty ", " m.mstatic) |
609 |
attr |
610 |
pp_machine_memtype_name m.mname.node_id |
611 |
(Utils.fprintf_list ~sep:";\\@," pp_c_decl_local_var) array_mem |
612 |
(Utils.pp_final_char_if_non_empty ";\\@," array_mem) |
613 |
(Utils.fprintf_list ~sep:";\\@," |
614 |
(fun fmt (i',m') -> |
615 |
let path = sprintf "inst ## _%s" i' in |
616 |
fprintf fmt "%a" |
617 |
(print_static_declare_instance attr) (path,m') |
618 |
)) m.minstances |
619 |
|
620 |
|
621 |
let print_static_link_instance fmt (i, (m, _)) = |
622 |
fprintf fmt "%a(%s)" pp_machine_static_link_name (node_name m) i |
623 |
|
624 |
let print_static_link_macro fmt m = |
625 |
let array_mem = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in |
626 |
fprintf fmt "@[<v>@[<v 2>#define %a(inst) do {\\@,%a%t%a;\\@]@,} while (0)@.@]" |
627 |
pp_machine_static_link_name m.mname.node_id |
628 |
(Utils.fprintf_list ~sep:";\\@," |
629 |
(fun fmt v -> |
630 |
fprintf fmt "inst.%s = &%s" |
631 |
v.var_id |
632 |
v.var_id |
633 |
)) array_mem |
634 |
(Utils.pp_final_char_if_non_empty ";\\@," array_mem) |
635 |
(Utils.fprintf_list ~sep:";\\@," |
636 |
(fun fmt (i',m') -> |
637 |
let path = sprintf "inst ## _%s" i' in |
638 |
fprintf fmt "%a;\\@,inst.%s = &%s" |
639 |
print_static_link_instance (path,m') |
640 |
i' |
641 |
path |
642 |
)) m.minstances |
643 |
|
644 |
let print_static_alloc_macro fmt m = |
645 |
fprintf fmt "@[<v>@[<v 2>#define %a(attr,%a%tinst)\\@,%a(attr,%a%tinst);\\@,%a(inst);@]@,@]@." |
646 |
pp_machine_static_alloc_name m.mname.node_id |
647 |
(Utils.fprintf_list ~sep:", " (pp_c_var_read m)) m.mstatic |
648 |
(Utils.pp_final_char_if_non_empty ", " m.mstatic) |
649 |
pp_machine_static_declare_name m.mname.node_id |
650 |
(Utils.fprintf_list ~sep:", " (pp_c_var_read m)) m.mstatic |
651 |
(Utils.pp_final_char_if_non_empty ", " m.mstatic) |
652 |
pp_machine_static_link_name m.mname.node_id |
653 |
|
654 |
let print_machine_decl fmt m = |
655 |
if m.mname.node_id <> arrow_id |
656 |
then ( |
657 |
(* We don't print arrow function *) |
658 |
(* Static allocation *) |
659 |
if !Options.static_mem |
660 |
then ( |
661 |
fprintf fmt "%a@.%a@.%a@." |
662 |
print_static_declare_macro m |
663 |
print_static_link_macro m |
664 |
print_static_alloc_macro m |
665 |
) |
666 |
else ( |
667 |
(* Dynamic allocation *) |
668 |
fprintf fmt "extern %a;@.@." |
669 |
print_alloc_prototype (m.mname.node_id, m.mstatic) |
670 |
); |
671 |
let self = mk_self m in |
672 |
fprintf fmt "extern %a;@.@." |
673 |
(print_reset_prototype self) (m.mname.node_id, m.mstatic); |
674 |
(* Print specification if any *) |
675 |
(match m.mspec with |
676 |
| None -> () |
677 |
| Some spec -> |
678 |
pp_acsl_spec m.mstep.step_outputs fmt spec |
679 |
); |
680 |
fprintf fmt "extern %a;@.@." |
681 |
(print_step_prototype self) |
682 |
(m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs) |
683 |
) |
684 |
|
685 |
|
686 |
(********************************************************************************************) |
687 |
(* C file Printing functions *) |
688 |
(********************************************************************************************) |
689 |
|
690 |
let print_const_def fmt cdecl = |
691 |
fprintf fmt "%a = %a;@." (pp_c_type cdecl.const_id) cdecl.const_type pp_c_const cdecl.const_value |
692 |
|
693 |
let print_const_decl fmt cdecl = |
694 |
fprintf fmt "extern %a;@." (pp_c_type cdecl.const_id) cdecl.const_type |
695 |
|
696 |
let print_alloc_instance fmt (i, (m, static)) = |
697 |
fprintf fmt "_alloc->%s = %a (%a);@," |
698 |
i |
699 |
pp_machine_alloc_name (node_name m) |
700 |
(Utils.fprintf_list ~sep:", " Dimension.pp_dimension) static |
701 |
|
702 |
let print_alloc_array fmt vdecl = |
703 |
let base_type = Types.array_base_type vdecl.var_type in |
704 |
let size_types = Types.array_type_multi_dimension vdecl.var_type in |
705 |
let size_type = Dimension.multi_dimension_product vdecl.var_loc size_types in |
706 |
fprintf fmt "_alloc->%s = (%a*) malloc((%a)*sizeof(%a));@,assert(_alloc->%s);@," |
707 |
vdecl.var_id |
708 |
(pp_c_type "") base_type |
709 |
Dimension.pp_dimension size_type |
710 |
(pp_c_type "") base_type |
711 |
vdecl.var_id |
712 |
|
713 |
let print_alloc_code fmt m = |
714 |
let array_mem = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in |
715 |
fprintf fmt "%a *_alloc;@,_alloc = (%a *) malloc(sizeof(%a));@,assert(_alloc);@,%a%areturn _alloc;" |
716 |
pp_machine_memtype_name m.mname.node_id |
717 |
pp_machine_memtype_name m.mname.node_id |
718 |
pp_machine_memtype_name m.mname.node_id |
719 |
(Utils.fprintf_list ~sep:"" print_alloc_array) array_mem |
720 |
(Utils.fprintf_list ~sep:"" print_alloc_instance) m.minstances |
721 |
|
722 |
let print_step_code fmt m self = |
723 |
if not (!Options.ansi && is_generic_node { top_decl_desc = Node m.mname; top_decl_loc = Location.dummy_loc }) |
724 |
then |
725 |
(* C99 code *) |
726 |
let array_mems = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in |
727 |
fprintf fmt "@[<v 2>%a {@,%a%t%a%t@,%a%a%t%t@]@,}@.@." |
728 |
(print_step_prototype self) (m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs) |
729 |
(* locals *) |
730 |
(Utils.fprintf_list ~sep:";@," pp_c_decl_local_var) m.mstep.step_locals |
731 |
(Utils.pp_final_char_if_non_empty ";@," m.mstep.step_locals) |
732 |
(* array mems *) |
733 |
(Utils.fprintf_list ~sep:";@," (pp_c_decl_array_mem self)) array_mems |
734 |
(Utils.pp_final_char_if_non_empty ";@," array_mems) |
735 |
(* check assertions *) |
736 |
(pp_c_checks self) m |
737 |
(* instrs *) |
738 |
(Utils.fprintf_list ~sep:"@," (pp_machine_instr m self)) m.mstep.step_instrs |
739 |
(Utils.pp_newline_if_non_empty m.mstep.step_instrs) |
740 |
(fun fmt -> fprintf fmt "return;") |
741 |
else |
742 |
(* C90 code *) |
743 |
let (gen_locals, base_locals) = List.partition (fun v -> Types.is_generic_type v.var_type) m.mstep.step_locals in |
744 |
let gen_calls = List.map (fun e -> let (id, _, _) = call_of_expr e in mk_call_var_decl e.expr_loc id) m.mname.node_gencalls in |
745 |
fprintf fmt "@[<v 2>%a {@,%a%t@,%a%a%t%t@]@,}@.@." |
746 |
(print_step_prototype self) (m.mname.node_id, (m.mstep.step_inputs@gen_locals@gen_calls), m.mstep.step_outputs) |
747 |
(* locals *) |
748 |
(Utils.fprintf_list ~sep:";@," pp_c_decl_local_var) base_locals |
749 |
(Utils.pp_final_char_if_non_empty ";" base_locals) |
750 |
(* check assertions *) |
751 |
(pp_c_checks self) m |
752 |
(* instrs *) |
753 |
(Utils.fprintf_list ~sep:"@," (pp_machine_instr m self)) m.mstep.step_instrs |
754 |
(Utils.pp_newline_if_non_empty m.mstep.step_instrs) |
755 |
(fun fmt -> fprintf fmt "return;") |
756 |
|
757 |
let print_machine fmt m = |
758 |
if m.mname.node_id <> arrow_id |
759 |
then ( |
760 |
(* We don't print arrow function *) |
761 |
(* Alloc function, only if non static mode *) |
762 |
if (not !Options.static_mem) then |
763 |
( |
764 |
fprintf fmt "@[<v 2>%a {@,%a@]@,}@.@." |
765 |
print_alloc_prototype (m.mname.node_id, m.mstatic) |
766 |
print_alloc_code m; |
767 |
); |
768 |
let self = mk_self m in |
769 |
(* Reset function *) |
770 |
fprintf fmt "@[<v 2>%a {@,%a%treturn;@]@,}@.@." |
771 |
(print_reset_prototype self) (m.mname.node_id, m.mstatic) |
772 |
(Utils.fprintf_list ~sep:"@," (pp_machine_instr m self)) m.minit |
773 |
(Utils.pp_newline_if_non_empty m.minit); |
774 |
(* Step function *) |
775 |
print_step_code fmt m self |
776 |
) |
777 |
|
778 |
(********************************************************************************************) |
779 |
(* Main related functions *) |
780 |
(********************************************************************************************) |
781 |
|
782 |
let print_get_input fmt v = |
783 |
match v.var_type.Types.tdesc with |
784 |
| Types.Tint -> fprintf fmt "_get_int(\"%s\")" v.var_id |
785 |
| Types.Tbool -> fprintf fmt "_get_bool(\"%s\")" v.var_id |
786 |
| Types.Treal -> fprintf fmt "_get_double(\"%s\")" v.var_id |
787 |
| _ -> assert false |
788 |
|
789 |
let print_put_outputs fmt ol = |
790 |
let po fmt o = |
791 |
match o.var_type.Types.tdesc with |
792 |
| Types.Tint -> fprintf fmt "_put_int(\"%s\", %s)" o.var_id o.var_id |
793 |
| Types.Tbool -> fprintf fmt "_put_bool(\"%s\", %s)" o.var_id o.var_id |
794 |
| Types.Treal -> fprintf fmt "_put_double(\"%s\", %s)" o.var_id o.var_id |
795 |
| _ -> assert false |
796 |
in |
797 |
List.iter (fprintf fmt "@ %a;" po) ol |
798 |
|
799 |
let print_main_fun machines m fmt = |
800 |
let mname = m.mname.node_id in |
801 |
let main_mem = |
802 |
if (!Options.static_mem && !Options.main_node <> "") |
803 |
then "&main_mem" |
804 |
else "main_mem" in |
805 |
fprintf fmt "@[<v 2>int main (int argc, char *argv[]) {@ "; |
806 |
fprintf fmt "/* Declaration of inputs/outputs variables */@ "; |
807 |
List.iter |
808 |
(fun v -> fprintf fmt "%a = %a;@ " (pp_c_type v.var_id) v.var_type pp_c_initialize v.var_type |
809 |
) m.mstep.step_inputs; |
810 |
List.iter |
811 |
(fun v -> fprintf fmt "%a = %a;@ " (pp_c_type v.var_id) v.var_type pp_c_initialize v.var_type |
812 |
) m.mstep.step_outputs; |
813 |
fprintf fmt "@ /* Main memory allocation */@ "; |
814 |
if (!Options.static_mem && !Options.main_node <> "") |
815 |
then (fprintf fmt "%a(static,main_mem);@ " pp_machine_static_alloc_name mname) |
816 |
else (fprintf fmt "%a *main_mem = %a();@ " pp_machine_memtype_name mname pp_machine_alloc_name mname); |
817 |
fprintf fmt "@ /* Initialize the main memory */@ "; |
818 |
fprintf fmt "%a(%s);@ " pp_machine_reset_name mname main_mem; |
819 |
fprintf fmt "@ ISATTY = isatty(0);@ "; |
820 |
fprintf fmt "@ /* Infinite loop */@ "; |
821 |
fprintf fmt "@[<v 2>while(1){@ "; |
822 |
fprintf fmt "fflush(stdout);@ "; |
823 |
List.iter |
824 |
(fun v -> fprintf fmt "%s = %a;@ " |
825 |
v.var_id |
826 |
print_get_input v |
827 |
) m.mstep.step_inputs; |
828 |
(match m.mstep.step_outputs with |
829 |
(* | [] -> ( *) |
830 |
(* fprintf fmt "%a(%a%t%s);@ " *) |
831 |
(* pp_machine_step_name mname *) |
832 |
(* (Utils.fprintf_list ~sep:", " (fun fmt v -> pp_print_string fmt v.var_id)) m.mstep.step_inputs *) |
833 |
(* (pp_final_char_if_non_empty ", " m.mstep.step_inputs) *) |
834 |
(* main_mem *) |
835 |
(* ) *) |
836 |
(* | [o] -> ( *) |
837 |
(* fprintf fmt "%s = %a(%a%t%a, %s);%a" *) |
838 |
(* o.var_id *) |
839 |
(* pp_machine_step_name mname *) |
840 |
(* (Utils.fprintf_list ~sep:", " (fun fmt v -> pp_print_string fmt v.var_id)) m.mstep.step_inputs *) |
841 |
(* (pp_final_char_if_non_empty ", " m.mstep.step_inputs) *) |
842 |
(* (Utils.fprintf_list ~sep:", " (fun fmt v -> fprintf fmt "&%s" v.var_id)) m.mstep.step_outputs *) |
843 |
(* main_mem *) |
844 |
(* print_put_outputs [o]) *) |
845 |
| _ -> ( |
846 |
fprintf fmt "%a(%a%t%a, %s);%a" |
847 |
pp_machine_step_name mname |
848 |
(Utils.fprintf_list ~sep:", " (fun fmt v -> pp_print_string fmt v.var_id)) m.mstep.step_inputs |
849 |
(Utils.pp_final_char_if_non_empty ", " m.mstep.step_inputs) |
850 |
(Utils.fprintf_list ~sep:", " (fun fmt v -> fprintf fmt "&%s" v.var_id)) m.mstep.step_outputs |
851 |
main_mem |
852 |
print_put_outputs m.mstep.step_outputs) |
853 |
); |
854 |
fprintf fmt "@]@ }@ "; |
855 |
fprintf fmt "return 1;"; |
856 |
fprintf fmt "@]@ }@." |
857 |
|
858 |
let print_main_header fmt = |
859 |
fprintf fmt "#include <stdio.h>@.#include <unistd.h>@.#include \"%s/include/lustrec/io_frontend.h\"@." Version.prefix |
860 |
|
861 |
let rec pp_c_type_decl filename cpt var fmt tdecl = |
862 |
match tdecl with |
863 |
| Tydec_any -> assert false |
864 |
| Tydec_int -> fprintf fmt "int %s" var |
865 |
| Tydec_real -> fprintf fmt "double %s" var |
866 |
| Tydec_float -> fprintf fmt "float %s" var |
867 |
| Tydec_bool -> fprintf fmt "_Bool %s" var |
868 |
| Tydec_clock ty -> pp_c_type_decl filename cpt var fmt ty |
869 |
| Tydec_const c -> fprintf fmt "%s %s" c var |
870 |
| Tydec_array (d, ty) -> fprintf fmt "%a[%a]" (pp_c_type_decl filename cpt var) ty pp_c_dimension d |
871 |
| Tydec_enum tl -> |
872 |
begin |
873 |
incr cpt; |
874 |
fprintf fmt "enum _enum_%s_%d { %a } %s" filename !cpt (Utils.fprintf_list ~sep:", " pp_print_string) tl var |
875 |
end |
876 |
|
877 |
let print_type_definitions fmt filename = |
878 |
let cpt_type = ref 0 in |
879 |
Hashtbl.iter (fun typ def -> |
880 |
match typ with |
881 |
| Tydec_const var -> |
882 |
fprintf fmt "typedef %a;@.@." |
883 |
(pp_c_type_decl filename cpt_type var) def |
884 |
| _ -> ()) type_table |
885 |
|
886 |
let print_makefile basename nodename dependencies fmt = |
887 |
fprintf fmt "GCC=gcc@."; |
888 |
fprintf fmt "LUSTREC=%s@." Sys.executable_name; |
889 |
fprintf fmt "LUSTREC_BASE=%s@." (Filename.dirname (Filename.dirname Sys.executable_name)); |
890 |
fprintf fmt "INC=${LUSTREC_BASE}/include/lustrec@."; |
891 |
fprintf fmt "@."; |
892 |
fprintf fmt "%s_%s:@." basename nodename; |
893 |
fprintf fmt "\t${GCC} -I${INC} -I. -c %s.c@." basename; |
894 |
List.iter (fun s -> (* Format.eprintf "Adding dependency: %s@." s; *) |
895 |
fprintf fmt "\t${GCC} -I${INC} -c %s@." s) |
896 |
(("${INC}/io_frontend.c")::(List.map (fun s -> s ^ ".c") dependencies)); |
897 |
(* fprintf fmt "\t${GCC} -I${INC} -c ${INC}/StdLibrary.c@."; *) |
898 |
(* fprintf fmt "\t${GCC} -o %s_%s io_frontend.o StdLibrary.o -lm %s.o@." basename nodename basename*) |
899 |
fprintf fmt "\t${GCC} -o %s_%s io_frontend.o %a -lm %s.o@." basename nodename |
900 |
(Utils.fprintf_list ~sep:" " (fun fmt s -> Format.fprintf fmt "%s.o" s)) dependencies basename; |
901 |
fprintf fmt "@."; |
902 |
fprintf fmt "clean:@."; |
903 |
fprintf fmt "\t\\rm -f *.o %s_%s@." basename nodename |
904 |
|
905 |
|
906 |
|
907 |
|
908 |
(********************************************************************************************) |
909 |
(* Translation function *) |
910 |
(********************************************************************************************) |
911 |
|
912 |
let translate_to_c header_fmt source_fmt makefile_fmt spec_fmt_opt basename prog machines dependencies = |
913 |
(* Generating H file *) |
914 |
|
915 |
(* Include once: start *) |
916 |
let baseNAME = String.uppercase basename in |
917 |
let baseNAME = Str.global_replace (Str.regexp "\\.\\|\\ ") "_" baseNAME in |
918 |
(* Print the svn version number and the supported C standard (C90 or C99) *) |
919 |
print_version header_fmt; |
920 |
fprintf header_fmt "#ifndef _%s@.#define _%s@." baseNAME baseNAME; |
921 |
pp_print_newline header_fmt (); |
922 |
fprintf header_fmt "/* Imports standard library */@."; |
923 |
(* imports standard library definitions (arrow) *) |
924 |
print_import_standard header_fmt; |
925 |
pp_print_newline header_fmt (); |
926 |
fprintf header_fmt "/* Types definitions */@."; |
927 |
(* Print the type definitions from the type table *) |
928 |
print_type_definitions header_fmt basename; |
929 |
pp_print_newline header_fmt (); |
930 |
(* Print the global constant declarations. *) |
931 |
fprintf header_fmt "/* Global constant (declarations, definitions are in C file) */@."; |
932 |
List.iter (fun c -> print_const_decl header_fmt c) (get_consts prog); |
933 |
pp_print_newline header_fmt (); |
934 |
(* Print the struct declarations of all machines. *) |
935 |
fprintf header_fmt "/* Struct declarations */@."; |
936 |
List.iter (print_machine_struct header_fmt) machines; |
937 |
pp_print_newline header_fmt (); |
938 |
(* Print the prototypes of all machines *) |
939 |
fprintf header_fmt "/* Nodes declarations */@."; |
940 |
List.iter (print_machine_decl header_fmt) machines; |
941 |
pp_print_newline header_fmt (); |
942 |
(* Include once: end *) |
943 |
fprintf header_fmt "#endif@."; |
944 |
pp_print_newline header_fmt (); |
945 |
|
946 |
(* Generating C file *) |
947 |
|
948 |
(* If a main node is identified, generate a main function for it *) |
949 |
let main_include, main_print, main_makefile = |
950 |
match !Options.main_node with |
951 |
| "" -> (fun _ -> ()), (fun _ -> ()), (fun _ -> ()) |
952 |
| main_node -> ( |
953 |
match Machine_code.get_machine_opt main_node machines with |
954 |
| None -> eprintf "Unable to find a main node named %s@.@?" main_node; (fun _ -> ()), (fun _ -> ()), (fun _ -> ()) |
955 |
| Some m -> print_main_header, print_main_fun machines m, print_makefile basename !Options.main_node dependencies |
956 |
) |
957 |
in |
958 |
main_include source_fmt; |
959 |
fprintf source_fmt "#include <stdlib.h>@.#include <assert.h>@.#include \"%s\"@.@." (basename^".h"); |
960 |
(* Print the svn version number and the supported C standard (C90 or C99) *) |
961 |
print_version source_fmt; |
962 |
(* Print the prototype of imported nodes *) |
963 |
fprintf source_fmt "/* Imported nodes declarations */@."; |
964 |
fprintf source_fmt "@[<v>"; |
965 |
List.iter (print_prototype source_fmt) prog; |
966 |
fprintf source_fmt "@]@."; |
967 |
(* Print consts *) |
968 |
fprintf source_fmt "/* Global constants (definitions) */@."; |
969 |
List.iter (fun c -> print_const_def source_fmt c) (get_consts prog); |
970 |
pp_print_newline source_fmt (); |
971 |
(* Print nodes one by one (in the previous order) *) |
972 |
List.iter (print_machine source_fmt) machines; |
973 |
main_print source_fmt; |
974 |
|
975 |
(* Generating Makefile *) |
976 |
main_makefile makefile_fmt |
977 |
|
978 |
(* Local Variables: *) |
979 |
(* compile-command:"make -C .." *) |
980 |
(* End: *) |