1
|
(********************************************************************)
|
2
|
(* *)
|
3
|
(* The LustreC compiler toolset / The LustreC Development Team *)
|
4
|
(* Copyright 2012 - -- ONERA - CNRS - INPT *)
|
5
|
(* *)
|
6
|
(* LustreC is free software, distributed WITHOUT ANY WARRANTY *)
|
7
|
(* under the terms of the GNU Lesser General Public License *)
|
8
|
(* version 2.1. *)
|
9
|
(* *)
|
10
|
(********************************************************************)
|
11
|
|
12
|
open Format
|
13
|
open Lustre_types
|
14
|
open Machine_code_types
|
15
|
open Corelang
|
16
|
open Machine_code_common
|
17
|
open C_backend_common
|
18
|
|
19
|
module type MODIFIERS_SRC =
|
20
|
sig
|
21
|
end
|
22
|
|
23
|
module EmptyMod =
|
24
|
struct
|
25
|
end
|
26
|
|
27
|
module Main = functor (Mod: MODIFIERS_SRC) ->
|
28
|
struct
|
29
|
|
30
|
(********************************************************************************************)
|
31
|
(* Instruction Printing functions *)
|
32
|
(********************************************************************************************)
|
33
|
|
34
|
|
35
|
(* Computes the depth to which multi-dimension array assignments should be expanded.
|
36
|
It equals the maximum number of nested static array constructions accessible from root [v].
|
37
|
*)
|
38
|
let rec expansion_depth v =
|
39
|
match v.value_desc with
|
40
|
| Cst cst -> expansion_depth_cst cst
|
41
|
| Var _ -> 0
|
42
|
| Fun (_, vl) -> List.fold_right (fun v -> max (expansion_depth v)) vl 0
|
43
|
| Array vl -> 1 + List.fold_right (fun v -> max (expansion_depth v)) vl 0
|
44
|
| Access (v, i) -> max 0 (expansion_depth v - 1)
|
45
|
| Power (v, n) -> 0 (*1 + expansion_depth v*)
|
46
|
and expansion_depth_cst c =
|
47
|
match c with
|
48
|
Const_array cl -> 1 + List.fold_right (fun c -> max (expansion_depth_cst c)) cl 0
|
49
|
| _ -> 0
|
50
|
|
51
|
let rec merge_static_loop_profiles lp1 lp2 =
|
52
|
match lp1, lp2 with
|
53
|
| [] , _ -> lp2
|
54
|
| _ , [] -> lp1
|
55
|
| p1 :: q1, p2 :: q2 -> (p1 || p2) :: merge_static_loop_profiles q1 q2
|
56
|
|
57
|
(* Returns a list of bool values, indicating whether the indices must be static or not *)
|
58
|
let rec static_loop_profile v =
|
59
|
match v.value_desc with
|
60
|
| Cst cst -> static_loop_profile_cst cst
|
61
|
| Var _ -> []
|
62
|
| Fun (_, vl) -> List.fold_right (fun v lp -> merge_static_loop_profiles lp (static_loop_profile v)) vl []
|
63
|
| Array vl -> true :: List.fold_right (fun v lp -> merge_static_loop_profiles lp (static_loop_profile v)) vl []
|
64
|
| Access (v, i) -> (match (static_loop_profile v) with [] -> [] | _ :: q -> q)
|
65
|
| Power (v, n) -> false :: static_loop_profile v
|
66
|
and static_loop_profile_cst cst =
|
67
|
match cst with
|
68
|
Const_array cl -> List.fold_right
|
69
|
(fun c lp -> merge_static_loop_profiles lp (static_loop_profile_cst c))
|
70
|
cl
|
71
|
[]
|
72
|
| _ -> []
|
73
|
|
74
|
|
75
|
let rec is_const_index v =
|
76
|
match v.value_desc with
|
77
|
| Cst (Const_int _) -> true
|
78
|
| Fun (_, vl) -> List.for_all is_const_index vl
|
79
|
| _ -> false
|
80
|
|
81
|
type loop_index = LVar of ident | LInt of int ref | LAcc of value_t
|
82
|
(*
|
83
|
let rec value_offsets v offsets =
|
84
|
match v, offsets with
|
85
|
| _ , [] -> v
|
86
|
| Power (v, n) , _ :: q -> value_offsets v q
|
87
|
| Array vl , LInt r :: q -> value_offsets (List.nth vl !r) q
|
88
|
| Cst (Const_array cl) , LInt r :: q -> value_offsets (Cst (List.nth cl !r)) q
|
89
|
| Fun (f, vl) , _ -> Fun (f, List.map (fun v -> value_offsets v offsets) vl)
|
90
|
| _ , LInt r :: q -> value_offsets (Access (v, Cst (Const_int !r))) q
|
91
|
| _ , LVar i :: q -> value_offsets (Access (v, Var i)) q
|
92
|
*)
|
93
|
(* Computes the list of nested loop variables together with their dimension bounds.
|
94
|
- LInt r stands for loop expansion (no loop variable, but int loop index)
|
95
|
- LVar v stands for loop variable v
|
96
|
*)
|
97
|
let rec mk_loop_variables m ty depth =
|
98
|
match (Types.repr ty).Types.tdesc, depth with
|
99
|
| Types.Tarray (d, ty'), 0 ->
|
100
|
let v = mk_loop_var m () in
|
101
|
(d, LVar v) :: mk_loop_variables m ty' 0
|
102
|
| Types.Tarray (d, ty'), _ ->
|
103
|
let r = ref (-1) in
|
104
|
(d, LInt r) :: mk_loop_variables m ty' (depth - 1)
|
105
|
| _ , 0 -> []
|
106
|
| _ -> assert false
|
107
|
|
108
|
let reorder_loop_variables loop_vars =
|
109
|
let (int_loops, var_loops) =
|
110
|
List.partition (function (d, LInt _) -> true | _ -> false) loop_vars
|
111
|
in
|
112
|
var_loops @ int_loops
|
113
|
|
114
|
(* Prints a one loop variable suffix for arrays *)
|
115
|
let pp_loop_var m pp_val fmt lv =
|
116
|
match snd lv with
|
117
|
| LVar v -> fprintf fmt "[%s]" v
|
118
|
| LInt r -> fprintf fmt "[%d]" !r
|
119
|
| LAcc i -> fprintf fmt "[%a]" pp_val i
|
120
|
|
121
|
(* Prints a suffix of loop variables for arrays *)
|
122
|
let pp_suffix m pp_val fmt loop_vars =
|
123
|
Utils.fprintf_list ~sep:"" (pp_loop_var m pp_val) fmt loop_vars
|
124
|
|
125
|
(* Prints a value expression [v], with internal function calls only.
|
126
|
[pp_var] is a printer for variables (typically [pp_c_var_read]),
|
127
|
but an offset suffix may be added for array variables
|
128
|
*)
|
129
|
(* Prints a constant value before a suffix (needs casting) *)
|
130
|
let rec pp_c_const_suffix var_type fmt c =
|
131
|
match c with
|
132
|
| Const_int i -> pp_print_int fmt i
|
133
|
| Const_real r -> Real.pp fmt r
|
134
|
| Const_tag t -> pp_c_tag fmt t
|
135
|
| Const_array ca -> let var_type = Types.array_element_type var_type in
|
136
|
fprintf fmt "(%a[]){%a }" (pp_c_type "") var_type (Utils.fprintf_list ~sep:", " (pp_c_const_suffix var_type)) ca
|
137
|
| Const_struct fl -> fprintf fmt "{%a }" (Utils.fprintf_list ~sep:", " (fun fmt (f, c) -> (pp_c_const_suffix (Types.struct_field_type var_type f)) fmt c)) fl
|
138
|
| Const_string _
|
139
|
| Const_modeid _ -> assert false (* string occurs in annotations not in C *)
|
140
|
|
141
|
|
142
|
(* Prints a [value] of type [var_type] indexed by the suffix list [loop_vars] *)
|
143
|
let rec pp_value_suffix m self var_type loop_vars pp_var fmt value =
|
144
|
(*Format.eprintf "pp_value_suffix: %a %a %a@." Types.print_ty var_type Machine_code.pp_val value pp_suffix loop_vars;*)
|
145
|
let pp_suffix = pp_suffix m (pp_value_suffix m self var_type [] pp_var) in
|
146
|
(
|
147
|
match loop_vars, value.value_desc with
|
148
|
| (x, LAcc i) :: q, _ when is_const_index i ->
|
149
|
let r = ref (Dimension.size_const_dimension (dimension_of_value i)) in
|
150
|
pp_value_suffix m self var_type ((x, LInt r)::q) pp_var fmt value
|
151
|
| (_, LInt r) :: q, Cst (Const_array cl) ->
|
152
|
let var_type = Types.array_element_type var_type in
|
153
|
pp_value_suffix m self var_type q pp_var fmt (mk_val (Cst (List.nth cl !r)) Type_predef.type_int)
|
154
|
| (_, LInt r) :: q, Array vl ->
|
155
|
let var_type = Types.array_element_type var_type in
|
156
|
pp_value_suffix m self var_type q pp_var fmt (List.nth vl !r)
|
157
|
| loop_var :: q, Array vl ->
|
158
|
let var_type = Types.array_element_type var_type in
|
159
|
Format.fprintf fmt "(%a[]){%a }%a" (pp_c_type "") var_type (Utils.fprintf_list ~sep:", " (pp_value_suffix m self var_type q pp_var)) vl pp_suffix [loop_var]
|
160
|
| [] , Array vl ->
|
161
|
let var_type = Types.array_element_type var_type in
|
162
|
Format.fprintf fmt "(%a[]){%a }" (pp_c_type "") var_type (Utils.fprintf_list ~sep:", " (pp_value_suffix m self var_type [] pp_var)) vl
|
163
|
| _ :: q, Power (v, n) ->
|
164
|
pp_value_suffix m self var_type q pp_var fmt v
|
165
|
| _ , Fun (n, vl) ->
|
166
|
pp_basic_lib_fun (Types.is_int_type value.value_type) n (pp_value_suffix m self var_type loop_vars pp_var) fmt vl
|
167
|
| _ , Access (v, i) ->
|
168
|
let var_type = Type_predef.type_array (Dimension.mkdim_var ()) var_type in
|
169
|
pp_value_suffix m self var_type ((Dimension.mkdim_var (), LAcc i) :: loop_vars) pp_var fmt v
|
170
|
| _ , Var v ->
|
171
|
if is_memory m v then (
|
172
|
(* array memory vars are represented by an indirection to a local var with the right type,
|
173
|
in order to avoid casting everywhere. *)
|
174
|
if Types.is_array_type v.var_type
|
175
|
then Format.fprintf fmt "%a%a" pp_var v pp_suffix loop_vars
|
176
|
else Format.fprintf fmt "%s->_reg.%a%a" self pp_var v pp_suffix loop_vars
|
177
|
)
|
178
|
else (
|
179
|
Format.fprintf fmt "%a%a" pp_var v pp_suffix loop_vars
|
180
|
)
|
181
|
| _ , Cst cst -> pp_c_const_suffix var_type fmt cst
|
182
|
| _ , _ -> (Format.eprintf "internal error: C_backend_src.pp_value_suffix %a %a %a@." Types.print_ty var_type (pp_val m) value pp_suffix loop_vars; assert false)
|
183
|
)
|
184
|
|
185
|
(* Subsumes C_backend_common.pp_c_val to cope with aggressive substitution
|
186
|
which may yield constant arrays in expressions.
|
187
|
Type is needed to correctly print constant arrays.
|
188
|
*)
|
189
|
let pp_c_val m self pp_var fmt v =
|
190
|
pp_value_suffix m self v.value_type [] pp_var fmt v
|
191
|
|
192
|
let pp_basic_assign pp_var fmt typ var_name value =
|
193
|
if Types.is_real_type typ && !Options.mpfr
|
194
|
then
|
195
|
Mpfr.pp_inject_assign pp_var fmt var_name value
|
196
|
else
|
197
|
fprintf fmt "%a = %a;"
|
198
|
pp_var var_name
|
199
|
pp_var value
|
200
|
|
201
|
(* type_directed assignment: array vs. statically sized type
|
202
|
- [var_type]: type of variable to be assigned
|
203
|
- [var_name]: name of variable to be assigned
|
204
|
- [value]: assigned value
|
205
|
- [pp_var]: printer for variables
|
206
|
*)
|
207
|
let pp_assign m self pp_var fmt var_type var_name value =
|
208
|
let depth = expansion_depth value in
|
209
|
(*Format.eprintf "pp_assign %a %a %a %d@." Types.print_ty var_type pp_val var_name pp_val value depth;*)
|
210
|
let loop_vars = mk_loop_variables m var_type depth in
|
211
|
let reordered_loop_vars = reorder_loop_variables loop_vars in
|
212
|
let rec aux typ fmt vars =
|
213
|
match vars with
|
214
|
| [] ->
|
215
|
pp_basic_assign (pp_value_suffix m self var_type loop_vars pp_var) fmt typ var_name value
|
216
|
| (d, LVar i) :: q ->
|
217
|
let typ' = Types.array_element_type typ in
|
218
|
(*eprintf "pp_aux %a %s@." Dimension.pp_dimension d i;*)
|
219
|
fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}"
|
220
|
i i i pp_c_dimension d i
|
221
|
(aux typ') q
|
222
|
| (d, LInt r) :: q ->
|
223
|
(*eprintf "pp_aux %a %d@." Dimension.pp_dimension d (!r);*)
|
224
|
let typ' = Types.array_element_type typ in
|
225
|
let szl = Utils.enumerate (Dimension.size_const_dimension d) in
|
226
|
fprintf fmt "@[<v 2>{@,%a@]@,}"
|
227
|
(Utils.fprintf_list ~sep:"@," (fun fmt i -> r := i; aux typ' fmt q)) szl
|
228
|
| _ -> assert false
|
229
|
in
|
230
|
begin
|
231
|
reset_loop_counter ();
|
232
|
(*reset_addr_counter ();*)
|
233
|
aux var_type fmt reordered_loop_vars;
|
234
|
(*Format.eprintf "end pp_assign@.";*)
|
235
|
end
|
236
|
|
237
|
let pp_machine_reset (m: machine_t) self fmt inst =
|
238
|
let (node, static) =
|
239
|
try
|
240
|
List.assoc inst m.minstances
|
241
|
with Not_found -> (Format.eprintf "internal error: pp_machine_reset %s %s %s:@." m.mname.node_id self inst; raise Not_found) in
|
242
|
fprintf fmt "%a(%a%t%s->%s);"
|
243
|
pp_machine_reset_name (node_name node)
|
244
|
(Utils.fprintf_list ~sep:", " Dimension.pp_dimension) static
|
245
|
(Utils.pp_final_char_if_non_empty ", " static)
|
246
|
self inst
|
247
|
|
248
|
let pp_machine_init (m: machine_t) self fmt inst =
|
249
|
let (node, static) =
|
250
|
try
|
251
|
List.assoc inst m.minstances
|
252
|
with Not_found -> (Format.eprintf "internal error: pp_machine_init %s %s %s@." m.mname.node_id self inst; raise Not_found) in
|
253
|
fprintf fmt "%a(%a%t%s->%s);"
|
254
|
pp_machine_init_name (node_name node)
|
255
|
(Utils.fprintf_list ~sep:", " Dimension.pp_dimension) static
|
256
|
(Utils.pp_final_char_if_non_empty ", " static)
|
257
|
self inst
|
258
|
|
259
|
let pp_machine_clear (m: machine_t) self fmt inst =
|
260
|
let (node, static) =
|
261
|
try
|
262
|
List.assoc inst m.minstances
|
263
|
with Not_found -> (Format.eprintf "internal error: pp_machine_clear %s %s %s@." m.mname.node_id self inst; raise Not_found) in
|
264
|
fprintf fmt "%a(%a%t%s->%s);"
|
265
|
pp_machine_clear_name (node_name node)
|
266
|
(Utils.fprintf_list ~sep:", " Dimension.pp_dimension) static
|
267
|
(Utils.pp_final_char_if_non_empty ", " static)
|
268
|
self inst
|
269
|
|
270
|
let has_c_prototype funname dependencies =
|
271
|
let imported_node_opt = (* We select the last imported node with the name funname.
|
272
|
The order of evaluation of dependencies should be
|
273
|
compatible with overloading. (Not checked yet) *)
|
274
|
List.fold_left
|
275
|
(fun res dep ->
|
276
|
match res with
|
277
|
| Some _ -> res
|
278
|
| None ->
|
279
|
let decls = dep.content in
|
280
|
let matched = fun t -> match t.top_decl_desc with
|
281
|
| ImportedNode nd -> nd.nodei_id = funname
|
282
|
| _ -> false
|
283
|
in
|
284
|
if List.exists matched decls then (
|
285
|
match (List.find matched decls).top_decl_desc with
|
286
|
| ImportedNode nd -> Some nd
|
287
|
| _ -> assert false
|
288
|
)
|
289
|
else
|
290
|
None
|
291
|
) None dependencies in
|
292
|
match imported_node_opt with
|
293
|
| None -> false
|
294
|
| Some nd -> (match nd.nodei_prototype with Some "C" -> true | _ -> false)
|
295
|
(*
|
296
|
let pp_instance_call dependencies m self fmt i (inputs: value_t list) (outputs: var_decl list) =
|
297
|
try (* stateful node instance *)
|
298
|
let (n,_) = List.assoc i m.minstances in
|
299
|
let (input_types, _) = Typing.get_type_of_call n in
|
300
|
let inputs = List.combine input_types inputs in
|
301
|
fprintf fmt "%a (%a%t%a%t%s->%s);"
|
302
|
pp_machine_step_name (node_name n)
|
303
|
(Utils.fprintf_list ~sep:", " (pp_c_val self (pp_c_var_read m))) inputs
|
304
|
(Utils.pp_final_char_if_non_empty ", " inputs)
|
305
|
(Utils.fprintf_list ~sep:", " (pp_c_var_write m)) outputs
|
306
|
(Utils.pp_final_char_if_non_empty ", " outputs)
|
307
|
self
|
308
|
i
|
309
|
with Not_found -> (* stateless node instance *)
|
310
|
let (n,_) = List.assoc i m.mcalls in
|
311
|
let (input_types, output_types) = Typing.get_type_of_call n in
|
312
|
let inputs = List.combine input_types inputs in
|
313
|
if has_c_prototype i dependencies
|
314
|
then (* external C function *)
|
315
|
let outputs = List.map2 (fun t v -> t, Var v) output_types outputs in
|
316
|
fprintf fmt "%a = %s(%a);"
|
317
|
(Utils.fprintf_list ~sep:", " (pp_c_val self (pp_c_var_read m))) outputs
|
318
|
i
|
319
|
(Utils.fprintf_list ~sep:", " (pp_c_val self (pp_c_var_read m))) inputs
|
320
|
else
|
321
|
fprintf fmt "%a (%a%t%a);"
|
322
|
pp_machine_step_name (node_name n)
|
323
|
(Utils.fprintf_list ~sep:", " (pp_c_val self (pp_c_var_read m))) inputs
|
324
|
(Utils.pp_final_char_if_non_empty ", " inputs)
|
325
|
(Utils.fprintf_list ~sep:", " (pp_c_var_write m)) outputs
|
326
|
*)
|
327
|
let rec pp_conditional dependencies (m: machine_t) self fmt c tl el =
|
328
|
fprintf fmt "@[<v 2>if (%a) {%t%a@]@,@[<v 2>} else {%t%a@]@,}"
|
329
|
(pp_c_val m self (pp_c_var_read m)) c
|
330
|
(Utils.pp_newline_if_non_empty tl)
|
331
|
(Utils.fprintf_list ~sep:"@," (pp_machine_instr dependencies m self)) tl
|
332
|
(Utils.pp_newline_if_non_empty el)
|
333
|
(Utils.fprintf_list ~sep:"@," (pp_machine_instr dependencies m self)) el
|
334
|
|
335
|
and pp_machine_instr dependencies (m: machine_t) self fmt instr =
|
336
|
match get_instr_desc instr with
|
337
|
| MNoReset _ -> ()
|
338
|
| MReset i ->
|
339
|
pp_machine_reset m self fmt i
|
340
|
| MLocalAssign (i,v) ->
|
341
|
pp_assign
|
342
|
m self (pp_c_var_read m) fmt
|
343
|
i.var_type (mk_val (Var i) i.var_type) v
|
344
|
| MStateAssign (i,v) ->
|
345
|
pp_assign
|
346
|
m self (pp_c_var_read m) fmt
|
347
|
i.var_type (mk_val (Var i) i.var_type) v
|
348
|
| MStep ([i0], i, vl) when Basic_library.is_value_internal_fun (mk_val (Fun (i, vl)) i0.var_type) ->
|
349
|
pp_machine_instr dependencies m self fmt
|
350
|
(update_instr_desc instr (MLocalAssign (i0, mk_val (Fun (i, vl)) i0.var_type)))
|
351
|
| MStep (il, i, vl) when !Options.mpfr && Mpfr.is_homomorphic_fun i ->
|
352
|
pp_instance_call m self fmt i vl il
|
353
|
| MStep ([i0], i, vl) when has_c_prototype i dependencies ->
|
354
|
fprintf fmt "%a = %s(%a);"
|
355
|
(pp_c_val m self (pp_c_var_read m)) (mk_val (Var i0) i0.var_type)
|
356
|
i
|
357
|
(Utils.fprintf_list ~sep:", " (pp_c_val m self (pp_c_var_read m))) vl
|
358
|
| MStep (il, i, vl) ->
|
359
|
pp_basic_instance_call m self fmt i vl il
|
360
|
| MBranch (_, []) -> (Format.eprintf "internal error: C_backend_src.pp_machine_instr %a@." (pp_instr m) instr; assert false)
|
361
|
| MBranch (g, hl) ->
|
362
|
if let t = fst (List.hd hl) in t = tag_true || t = tag_false
|
363
|
then (* boolean case, needs special treatment in C because truth value is not unique *)
|
364
|
(* may disappear if we optimize code by replacing last branch test with default *)
|
365
|
let tl = try List.assoc tag_true hl with Not_found -> [] in
|
366
|
let el = try List.assoc tag_false hl with Not_found -> [] in
|
367
|
pp_conditional dependencies m self fmt g tl el
|
368
|
else (* enum type case *)
|
369
|
(*let g_typ = Typing.type_const Location.dummy_loc (Const_tag (fst (List.hd hl))) in*)
|
370
|
fprintf fmt "@[<v 2>switch(%a) {@,%a@,}@]"
|
371
|
(pp_c_val m self (pp_c_var_read m)) g
|
372
|
(Utils.fprintf_list ~sep:"@," (pp_machine_branch dependencies m self)) hl
|
373
|
| MSpec s -> fprintf fmt "@[/*@@ %s */@]@ " s
|
374
|
| MComment s ->
|
375
|
fprintf fmt "/*%s*/@ " s
|
376
|
|
377
|
|
378
|
and pp_machine_branch dependencies m self fmt (t, h) =
|
379
|
fprintf fmt "@[<v 2>case %a:@,%a@,break;@]"
|
380
|
pp_c_tag t
|
381
|
(Utils.fprintf_list ~sep:"@," (pp_machine_instr dependencies m self)) h
|
382
|
|
383
|
|
384
|
(********************************************************************************************)
|
385
|
(* C file Printing functions *)
|
386
|
(********************************************************************************************)
|
387
|
|
388
|
let print_const_def fmt cdecl =
|
389
|
if !Options.mpfr && Types.is_real_type (Types.array_base_type cdecl.const_type)
|
390
|
then
|
391
|
fprintf fmt "%a;@."
|
392
|
(pp_c_type cdecl.const_id) (Types.dynamic_type cdecl.const_type)
|
393
|
else
|
394
|
fprintf fmt "%a = %a;@."
|
395
|
(pp_c_type cdecl.const_id) cdecl.const_type
|
396
|
pp_c_const cdecl.const_value
|
397
|
|
398
|
|
399
|
let print_alloc_instance fmt (i, (m, static)) =
|
400
|
fprintf fmt "_alloc->%s = %a (%a);@,"
|
401
|
i
|
402
|
pp_machine_alloc_name (node_name m)
|
403
|
(Utils.fprintf_list ~sep:", " Dimension.pp_dimension) static
|
404
|
|
405
|
let print_dealloc_instance fmt (i, (m, _)) =
|
406
|
fprintf fmt "%a (_alloc->%s);@,"
|
407
|
pp_machine_dealloc_name (node_name m)
|
408
|
i
|
409
|
|
410
|
let print_alloc_const fmt m =
|
411
|
let const_locals = List.filter (fun vdecl -> vdecl.var_dec_const) m.mstep.step_locals in
|
412
|
fprintf fmt "%a%t"
|
413
|
(Utils.fprintf_list ~sep:";@," (pp_c_decl_local_var m)) const_locals
|
414
|
(Utils.pp_final_char_if_non_empty ";@," const_locals)
|
415
|
|
416
|
let print_alloc_array fmt vdecl =
|
417
|
let base_type = Types.array_base_type vdecl.var_type in
|
418
|
let size_types = Types.array_type_multi_dimension vdecl.var_type in
|
419
|
let size_type = Dimension.multi_dimension_product vdecl.var_loc size_types in
|
420
|
fprintf fmt "_alloc->_reg.%s = (%a*) malloc((%a)*sizeof(%a));@,assert(_alloc->%s);@,"
|
421
|
vdecl.var_id
|
422
|
(pp_c_type "") base_type
|
423
|
Dimension.pp_dimension size_type
|
424
|
(pp_c_type "") base_type
|
425
|
vdecl.var_id
|
426
|
|
427
|
let print_dealloc_array fmt vdecl =
|
428
|
fprintf fmt "free (_alloc->_reg.%s);@,"
|
429
|
vdecl.var_id
|
430
|
|
431
|
let print_alloc_code fmt m =
|
432
|
let array_mem = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in
|
433
|
fprintf fmt "%a *_alloc;@,_alloc = (%a *) malloc(sizeof(%a));@,assert(_alloc);@,%a%areturn _alloc;"
|
434
|
pp_machine_memtype_name m.mname.node_id
|
435
|
pp_machine_memtype_name m.mname.node_id
|
436
|
pp_machine_memtype_name m.mname.node_id
|
437
|
(Utils.fprintf_list ~sep:"" print_alloc_array) array_mem
|
438
|
(Utils.fprintf_list ~sep:"" print_alloc_instance) m.minstances
|
439
|
|
440
|
let print_dealloc_code fmt m =
|
441
|
let array_mem = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in
|
442
|
fprintf fmt "%a%afree (_alloc);@,return;"
|
443
|
(Utils.fprintf_list ~sep:"" print_dealloc_array) array_mem
|
444
|
(Utils.fprintf_list ~sep:"" print_dealloc_instance) m.minstances
|
445
|
|
446
|
let print_stateless_init_code dependencies fmt m self =
|
447
|
let minit = List.map (fun i -> match get_instr_desc i with MReset i -> i | _ -> assert false) m.minit in
|
448
|
let array_mems = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in
|
449
|
fprintf fmt "@[<v 2>%a {@,%a%t%a%t%a%treturn;@]@,}@.@."
|
450
|
(print_init_prototype self) (m.mname.node_id, m.mstatic)
|
451
|
(* array mems *)
|
452
|
(Utils.fprintf_list ~sep:";@," (pp_c_decl_array_mem self)) array_mems
|
453
|
(Utils.pp_final_char_if_non_empty ";@," array_mems)
|
454
|
(* memory initialization *)
|
455
|
(Utils.fprintf_list ~sep:"@," (pp_initialize m self (pp_c_var_read m))) m.mmemory
|
456
|
(Utils.pp_newline_if_non_empty m.mmemory)
|
457
|
(* sub-machines initialization *)
|
458
|
(Utils.fprintf_list ~sep:"@," (pp_machine_init m self)) minit
|
459
|
(Utils.pp_newline_if_non_empty m.minit)
|
460
|
|
461
|
let print_stateless_clear_code dependencies fmt m self =
|
462
|
let minit = List.map (fun i -> match get_instr_desc i with MReset i -> i | _ -> assert false) m.minit in
|
463
|
let array_mems = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in
|
464
|
fprintf fmt "@[<v 2>%a {@,%a%t%a%t%a%treturn;@]@,}@.@."
|
465
|
(print_clear_prototype self) (m.mname.node_id, m.mstatic)
|
466
|
(* array mems *)
|
467
|
(Utils.fprintf_list ~sep:";@," (pp_c_decl_array_mem self)) array_mems
|
468
|
(Utils.pp_final_char_if_non_empty ";@," array_mems)
|
469
|
(* memory clear *)
|
470
|
(Utils.fprintf_list ~sep:"@," (pp_clear m self (pp_c_var_read m))) m.mmemory
|
471
|
(Utils.pp_newline_if_non_empty m.mmemory)
|
472
|
(* sub-machines clear*)
|
473
|
(Utils.fprintf_list ~sep:"@," (pp_machine_clear m self)) minit
|
474
|
(Utils.pp_newline_if_non_empty m.minit)
|
475
|
|
476
|
let print_stateless_code dependencies fmt m =
|
477
|
let self = "__ERROR__" in
|
478
|
if not (!Options.ansi && is_generic_node { top_decl_desc = Node m.mname; top_decl_loc = Location.dummy_loc; top_decl_owner = ""; top_decl_itf = false })
|
479
|
then
|
480
|
(* C99 code *)
|
481
|
fprintf fmt "@[<v 2>%a {@,%a%t%a%t@,%a%a%t%a%t%t@]@,}@.@."
|
482
|
print_stateless_prototype (m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs)
|
483
|
(* locals *)
|
484
|
(Utils.fprintf_list ~sep:";@," (pp_c_decl_local_var m)) m.mstep.step_locals
|
485
|
(Utils.pp_final_char_if_non_empty ";@," m.mstep.step_locals)
|
486
|
(* locals initialization *)
|
487
|
(Utils.fprintf_list ~sep:"@," (pp_initialize m self (pp_c_var_read m))) m.mstep.step_locals
|
488
|
(Utils.pp_newline_if_non_empty m.mstep.step_locals)
|
489
|
(* check assertions *)
|
490
|
(pp_c_checks self) m
|
491
|
(* instrs *)
|
492
|
(Utils.fprintf_list ~sep:"@," (pp_machine_instr dependencies m self)) m.mstep.step_instrs
|
493
|
(Utils.pp_newline_if_non_empty m.mstep.step_instrs)
|
494
|
(* locals clear *)
|
495
|
(Utils.fprintf_list ~sep:"@," (pp_clear m self (pp_c_var_read m))) m.mstep.step_locals
|
496
|
(Utils.pp_newline_if_non_empty m.mstep.step_locals)
|
497
|
(fun fmt -> fprintf fmt "return;")
|
498
|
else
|
499
|
(* C90 code *)
|
500
|
let (gen_locals, base_locals) = List.partition (fun v -> Types.is_generic_type v.var_type) m.mstep.step_locals in
|
501
|
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
|
502
|
fprintf fmt "@[<v 2>%a {@,%a%t%a%t@,%a%a%t%a%t%t@]@,}@.@."
|
503
|
print_stateless_prototype (m.mname.node_id, (m.mstep.step_inputs@gen_locals@gen_calls), m.mstep.step_outputs)
|
504
|
(* locals *)
|
505
|
(Utils.fprintf_list ~sep:";@," (pp_c_decl_local_var m)) base_locals
|
506
|
(Utils.pp_final_char_if_non_empty ";" base_locals)
|
507
|
(* locals initialization *)
|
508
|
(Utils.fprintf_list ~sep:"@," (pp_initialize m self (pp_c_var_read m))) m.mstep.step_locals
|
509
|
(Utils.pp_newline_if_non_empty m.mstep.step_locals)
|
510
|
(* check assertions *)
|
511
|
(pp_c_checks self) m
|
512
|
(* instrs *)
|
513
|
(Utils.fprintf_list ~sep:"@," (pp_machine_instr dependencies m self)) m.mstep.step_instrs
|
514
|
(Utils.pp_newline_if_non_empty m.mstep.step_instrs)
|
515
|
(* locals clear *)
|
516
|
(Utils.fprintf_list ~sep:"@," (pp_clear m self (pp_c_var_read m))) m.mstep.step_locals
|
517
|
(Utils.pp_newline_if_non_empty m.mstep.step_locals)
|
518
|
(fun fmt -> fprintf fmt "return;")
|
519
|
|
520
|
let print_reset_code dependencies fmt m self =
|
521
|
let const_locals = List.filter (fun vdecl -> vdecl.var_dec_const) m.mstep.step_locals in
|
522
|
fprintf fmt "@[<v 2>%a {@,%a%t@,%a%treturn;@]@,}@.@."
|
523
|
(print_reset_prototype self) (m.mname.node_id, m.mstatic)
|
524
|
(* constant locals decl *)
|
525
|
(Utils.fprintf_list ~sep:";@," (pp_c_decl_local_var m)) const_locals
|
526
|
(Utils.pp_final_char_if_non_empty ";" const_locals)
|
527
|
(* instrs *)
|
528
|
(Utils.fprintf_list ~sep:"@," (pp_machine_instr dependencies m self)) m.minit
|
529
|
(Utils.pp_newline_if_non_empty m.minit)
|
530
|
|
531
|
let print_init_code dependencies fmt m self =
|
532
|
let minit = List.map (fun i -> match get_instr_desc i with MReset i -> i | _ -> assert false) m.minit in
|
533
|
let array_mems = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in
|
534
|
fprintf fmt "@[<v 2>%a {@,%a%t%a%t%a%treturn;@]@,}@.@."
|
535
|
(print_init_prototype self) (m.mname.node_id, m.mstatic)
|
536
|
(* array mems *)
|
537
|
(Utils.fprintf_list ~sep:";@," (pp_c_decl_array_mem self)) array_mems
|
538
|
(Utils.pp_final_char_if_non_empty ";@," array_mems)
|
539
|
(* memory initialization *)
|
540
|
(Utils.fprintf_list ~sep:"@," (pp_initialize m self (pp_c_var_read m))) m.mmemory
|
541
|
(Utils.pp_newline_if_non_empty m.mmemory)
|
542
|
(* sub-machines initialization *)
|
543
|
(Utils.fprintf_list ~sep:"@," (pp_machine_init m self)) minit
|
544
|
(Utils.pp_newline_if_non_empty m.minit)
|
545
|
|
546
|
let print_clear_code dependencies fmt m self =
|
547
|
let minit = List.map (fun i -> match get_instr_desc i with MReset i -> i | _ -> assert false) m.minit in
|
548
|
let array_mems = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in
|
549
|
fprintf fmt "@[<v 2>%a {@,%a%t%a%t%a%treturn;@]@,}@.@."
|
550
|
(print_clear_prototype self) (m.mname.node_id, m.mstatic)
|
551
|
(* array mems *)
|
552
|
(Utils.fprintf_list ~sep:";@," (pp_c_decl_array_mem self)) array_mems
|
553
|
(Utils.pp_final_char_if_non_empty ";@," array_mems)
|
554
|
(* memory clear *)
|
555
|
(Utils.fprintf_list ~sep:"@," (pp_clear m self (pp_c_var_read m))) m.mmemory
|
556
|
(Utils.pp_newline_if_non_empty m.mmemory)
|
557
|
(* sub-machines clear*)
|
558
|
(Utils.fprintf_list ~sep:"@," (pp_machine_clear m self)) minit
|
559
|
(Utils.pp_newline_if_non_empty m.minit)
|
560
|
|
561
|
let print_step_code dependencies fmt m self =
|
562
|
if not (!Options.ansi && is_generic_node { top_decl_desc = Node m.mname; top_decl_loc = Location.dummy_loc; top_decl_owner = ""; top_decl_itf = false })
|
563
|
then
|
564
|
(* C99 code *)
|
565
|
let array_mems = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in
|
566
|
fprintf fmt "@[<v 2>%a {@,%a%t%a%t%a%t@,%a%a%t%a%t%t@]@,}@.@."
|
567
|
(print_step_prototype self) (m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs)
|
568
|
(* locals *)
|
569
|
(Utils.fprintf_list ~sep:";@," (pp_c_decl_local_var m)) m.mstep.step_locals
|
570
|
(Utils.pp_final_char_if_non_empty ";@," m.mstep.step_locals)
|
571
|
(* array mems *)
|
572
|
(Utils.fprintf_list ~sep:";@," (pp_c_decl_array_mem self)) array_mems
|
573
|
(Utils.pp_final_char_if_non_empty ";@," array_mems)
|
574
|
(* locals initialization *)
|
575
|
(Utils.fprintf_list ~sep:"@," (pp_initialize m self (pp_c_var_read m))) m.mstep.step_locals
|
576
|
(Utils.pp_newline_if_non_empty m.mstep.step_locals)
|
577
|
(* check assertions *)
|
578
|
(pp_c_checks self) m
|
579
|
(* instrs *)
|
580
|
(Utils.fprintf_list ~sep:"@," (pp_machine_instr dependencies m self)) m.mstep.step_instrs
|
581
|
(Utils.pp_newline_if_non_empty m.mstep.step_instrs)
|
582
|
(* locals clear *)
|
583
|
(Utils.fprintf_list ~sep:"@," (pp_clear m self (pp_c_var_read m))) m.mstep.step_locals
|
584
|
(Utils.pp_newline_if_non_empty m.mstep.step_locals)
|
585
|
(fun fmt -> fprintf fmt "return;")
|
586
|
else
|
587
|
(* C90 code *)
|
588
|
let (gen_locals, base_locals) = List.partition (fun v -> Types.is_generic_type v.var_type) m.mstep.step_locals in
|
589
|
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
|
590
|
fprintf fmt "@[<v 2>%a {@,%a%t%a%t@,%a%a%t%a%t%t@]@,}@.@."
|
591
|
(print_step_prototype self) (m.mname.node_id, (m.mstep.step_inputs@gen_locals@gen_calls), m.mstep.step_outputs)
|
592
|
(* locals *)
|
593
|
(Utils.fprintf_list ~sep:";@," (pp_c_decl_local_var m)) base_locals
|
594
|
(Utils.pp_final_char_if_non_empty ";" base_locals)
|
595
|
(* locals initialization *)
|
596
|
(Utils.fprintf_list ~sep:"@," (pp_initialize m self (pp_c_var_read m))) m.mstep.step_locals
|
597
|
(Utils.pp_newline_if_non_empty m.mstep.step_locals)
|
598
|
(* check assertions *)
|
599
|
(pp_c_checks self) m
|
600
|
(* instrs *)
|
601
|
(Utils.fprintf_list ~sep:"@," (pp_machine_instr dependencies m self)) m.mstep.step_instrs
|
602
|
(Utils.pp_newline_if_non_empty m.mstep.step_instrs)
|
603
|
(* locals clear *)
|
604
|
(Utils.fprintf_list ~sep:"@," (pp_clear m self (pp_c_var_read m))) m.mstep.step_locals
|
605
|
(Utils.pp_newline_if_non_empty m.mstep.step_locals)
|
606
|
(fun fmt -> fprintf fmt "return;")
|
607
|
|
608
|
|
609
|
(********************************************************************************************)
|
610
|
(* MAIN C file Printing functions *)
|
611
|
(********************************************************************************************)
|
612
|
|
613
|
let print_global_init_code fmt basename prog dependencies =
|
614
|
let baseNAME = file_to_module_name basename in
|
615
|
let constants = List.map const_of_top (get_consts prog) in
|
616
|
fprintf fmt "@[<v 2>%a {@,static %s init = 0;@,@[<v 2>if (!init) { @,init = 1;@,%a%t%a@]@,}@,return;@]@,}@.@."
|
617
|
print_global_init_prototype baseNAME
|
618
|
(pp_c_basic_type_desc Type_predef.type_bool)
|
619
|
(* constants *)
|
620
|
(Utils.fprintf_list ~sep:"@," (pp_const_initialize empty_machine (pp_c_var_read empty_machine))) constants
|
621
|
(Utils.pp_final_char_if_non_empty "@," dependencies)
|
622
|
(* dependencies initialization *)
|
623
|
(Utils.fprintf_list ~sep:"@," print_import_init) dependencies
|
624
|
|
625
|
let print_global_clear_code fmt basename prog dependencies =
|
626
|
let baseNAME = file_to_module_name basename in
|
627
|
let constants = List.map const_of_top (get_consts prog) in
|
628
|
fprintf fmt "@[<v 2>%a {@,static %s clear = 0;@,@[<v 2>if (!clear) { @,clear = 1;@,%a%t%a@]@,}@,return;@]@,}@.@."
|
629
|
print_global_clear_prototype baseNAME
|
630
|
(pp_c_basic_type_desc Type_predef.type_bool)
|
631
|
(* constants *)
|
632
|
(Utils.fprintf_list ~sep:"@," (pp_const_clear (pp_c_var_read empty_machine))) constants
|
633
|
(Utils.pp_final_char_if_non_empty "@," dependencies)
|
634
|
(* dependencies initialization *)
|
635
|
(Utils.fprintf_list ~sep:"@," print_import_clear) dependencies
|
636
|
|
637
|
(* TODO: ACSL
|
638
|
- a contract machine shall not be directly printed in the C source
|
639
|
- but a regular machine associated to a contract machine shall integrate the associated statements, updating its memories, at the end of the function body.
|
640
|
- last one may print intermediate comment/acsl if/when they are present in the sequence of instruction
|
641
|
*)
|
642
|
let print_machine dependencies fmt m =
|
643
|
if fst (get_stateless_status m) then
|
644
|
begin
|
645
|
(* Step function *)
|
646
|
print_stateless_code dependencies fmt m
|
647
|
end
|
648
|
else
|
649
|
begin
|
650
|
(* Alloc functions, only if non static mode *)
|
651
|
if (not !Options.static_mem) then
|
652
|
begin
|
653
|
fprintf fmt "@[<v 2>%a {@,%a%a@]@,}@.@."
|
654
|
print_alloc_prototype (m.mname.node_id, m.mstatic)
|
655
|
print_alloc_const m
|
656
|
print_alloc_code m;
|
657
|
|
658
|
fprintf fmt "@[<v 2>%a {@,%a%a@]@,}@.@."
|
659
|
print_dealloc_prototype m.mname.node_id
|
660
|
print_alloc_const m
|
661
|
print_dealloc_code m;
|
662
|
end;
|
663
|
let self = mk_self m in
|
664
|
(* Reset function *)
|
665
|
print_reset_code dependencies fmt m self;
|
666
|
(* Step function *)
|
667
|
print_step_code dependencies fmt m self;
|
668
|
|
669
|
if !Options.mpfr then
|
670
|
begin
|
671
|
(* Init function *)
|
672
|
print_init_code dependencies fmt m self;
|
673
|
(* Clear function *)
|
674
|
print_clear_code dependencies fmt m self;
|
675
|
end
|
676
|
end
|
677
|
|
678
|
let print_import_standard source_fmt =
|
679
|
begin
|
680
|
fprintf source_fmt "#include <assert.h>@.";
|
681
|
if Machine_types.has_machine_type () then
|
682
|
begin
|
683
|
fprintf source_fmt "#include <stdint.h>@."
|
684
|
end;
|
685
|
if not !Options.static_mem then
|
686
|
begin
|
687
|
fprintf source_fmt "#include <stdlib.h>@.";
|
688
|
end;
|
689
|
if !Options.mpfr then
|
690
|
begin
|
691
|
fprintf source_fmt "#include <mpfr.h>@.";
|
692
|
end
|
693
|
end
|
694
|
|
695
|
let print_lib_c source_fmt basename prog machines dependencies =
|
696
|
print_import_standard source_fmt;
|
697
|
print_import_prototype source_fmt {local=true; name=basename; content=[]; is_stateful=true} (* assuming it is stateful *);
|
698
|
pp_print_newline source_fmt ();
|
699
|
(* Print the svn version number and the supported C standard (C90 or C99) *)
|
700
|
print_version source_fmt;
|
701
|
(* Print the prototype of imported nodes *)
|
702
|
fprintf source_fmt "/* Import dependencies */@.";
|
703
|
fprintf source_fmt "@[<v>";
|
704
|
List.iter (print_import_prototype source_fmt) dependencies;
|
705
|
fprintf source_fmt "@]@.";
|
706
|
(* Print consts *)
|
707
|
fprintf source_fmt "/* Global constants (definitions) */@.";
|
708
|
fprintf source_fmt "@[<v>";
|
709
|
List.iter (fun c -> print_const_def source_fmt (const_of_top c)) (get_consts prog);
|
710
|
fprintf source_fmt "@]@.";
|
711
|
if !Options.mpfr then
|
712
|
begin
|
713
|
fprintf source_fmt "/* Global constants initialization */@.";
|
714
|
print_global_init_code source_fmt basename prog dependencies;
|
715
|
fprintf source_fmt "/* Global constants clearing */@.";
|
716
|
print_global_clear_code source_fmt basename prog dependencies;
|
717
|
end;
|
718
|
if not !Options.static_mem then
|
719
|
begin
|
720
|
fprintf source_fmt "/* External allocation function prototypes */@.";
|
721
|
fprintf source_fmt "@[<v>";
|
722
|
List.iter (print_extern_alloc_prototypes source_fmt) dependencies;
|
723
|
fprintf source_fmt "@]@.";
|
724
|
fprintf source_fmt "/* Node allocation function prototypes */@.";
|
725
|
fprintf source_fmt "@[<v>";
|
726
|
List.iter
|
727
|
(fun m -> fprintf source_fmt "%a;@.@.%a;@.@."
|
728
|
print_alloc_prototype (m.mname.node_id, m.mstatic)
|
729
|
print_dealloc_prototype m.mname.node_id
|
730
|
)
|
731
|
machines;
|
732
|
fprintf source_fmt "@]@.";
|
733
|
end;
|
734
|
|
735
|
(* Print the struct definitions of all machines. *)
|
736
|
fprintf source_fmt "/* Struct definitions */@.";
|
737
|
fprintf source_fmt "@[<v>";
|
738
|
List.iter (print_machine_struct machines source_fmt) machines;
|
739
|
fprintf source_fmt "@]@.";
|
740
|
pp_print_newline source_fmt ();
|
741
|
(* Print nodes one by one (in the previous order) *)
|
742
|
List.iter (print_machine dependencies source_fmt) machines;
|
743
|
end
|
744
|
|
745
|
(* Local Variables: *)
|
746
|
(* compile-command:"make -C ../../.." *)
|
747
|
(* End: *)
|