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 Utils.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 = sig
|
20
|
val pp_predicates: dep_t list -> formatter -> machine_t list -> unit
|
21
|
val pp_reset_spec: formatter -> ident -> machine_t -> unit
|
22
|
val pp_step_spec: formatter -> ident -> machine_t -> unit
|
23
|
val pp_step_instr_spec: machine_t -> ident -> formatter -> (int * instr_t) -> unit
|
24
|
end
|
25
|
|
26
|
module EmptyMod = struct
|
27
|
let pp_predicates _ _ _ = ()
|
28
|
let pp_reset_spec _ _ _ = ()
|
29
|
let pp_step_spec _ _ _ = ()
|
30
|
let pp_step_instr_spec _ _ _ _ = ()
|
31
|
end
|
32
|
|
33
|
module Main = functor (Mod: MODIFIERS_SRC) -> struct
|
34
|
|
35
|
(********************************************************************************************)
|
36
|
(* Instruction Printing functions *)
|
37
|
(********************************************************************************************)
|
38
|
|
39
|
|
40
|
(* Computes the depth to which multi-dimension array assignments should be expanded.
|
41
|
It equals the maximum number of nested static array constructions accessible from root [v].
|
42
|
*)
|
43
|
let rec expansion_depth v =
|
44
|
match v.value_desc with
|
45
|
| Cst cst -> expansion_depth_cst cst
|
46
|
| Var _ -> 0
|
47
|
| Fun (_, vl) -> List.fold_right (fun v -> max (expansion_depth v)) vl 0
|
48
|
| Array vl -> 1 + List.fold_right (fun v -> max (expansion_depth v)) vl 0
|
49
|
| Access (v, _) -> max 0 (expansion_depth v - 1)
|
50
|
| Power _ -> 0 (*1 + expansion_depth v*)
|
51
|
and expansion_depth_cst c =
|
52
|
match c with
|
53
|
| Const_array cl ->
|
54
|
1 + List.fold_right (fun c -> max (expansion_depth_cst c)) cl 0
|
55
|
| _ -> 0
|
56
|
|
57
|
let rec merge_static_loop_profiles lp1 lp2 =
|
58
|
match lp1, lp2 with
|
59
|
| [] , _ -> lp2
|
60
|
| _ , [] -> lp1
|
61
|
| p1 :: q1, p2 :: q2 -> (p1 || p2) :: merge_static_loop_profiles q1 q2
|
62
|
|
63
|
(* Returns a list of bool values, indicating whether the indices must be static or not *)
|
64
|
let rec static_loop_profile v =
|
65
|
match v.value_desc with
|
66
|
| Cst cst -> static_loop_profile_cst cst
|
67
|
| Var _ -> []
|
68
|
| Fun (_, vl) ->
|
69
|
List.fold_right
|
70
|
(fun v lp -> merge_static_loop_profiles lp (static_loop_profile v)) vl []
|
71
|
| Array vl ->
|
72
|
true :: List.fold_right
|
73
|
(fun v lp -> merge_static_loop_profiles lp (static_loop_profile v)) vl []
|
74
|
| Access (v, _) ->
|
75
|
begin match static_loop_profile v with [] -> [] | _ :: q -> q end
|
76
|
| Power (v, _) -> false :: static_loop_profile v
|
77
|
and static_loop_profile_cst cst =
|
78
|
match cst with
|
79
|
Const_array cl ->
|
80
|
List.fold_right
|
81
|
(fun c lp -> merge_static_loop_profiles lp (static_loop_profile_cst c))
|
82
|
cl []
|
83
|
| _ -> []
|
84
|
|
85
|
let rec is_const_index v =
|
86
|
match v.value_desc with
|
87
|
| Cst (Const_int _) -> true
|
88
|
| Fun (_, vl) -> List.for_all is_const_index vl
|
89
|
| _ -> false
|
90
|
|
91
|
type loop_index = LVar of ident | LInt of int ref | LAcc of value_t
|
92
|
(*
|
93
|
let rec value_offsets v offsets =
|
94
|
match v, offsets with
|
95
|
| _ , [] -> v
|
96
|
| Power (v, n) , _ :: q -> value_offsets v q
|
97
|
| Array vl , LInt r :: q -> value_offsets (List.nth vl !r) q
|
98
|
| Cst (Const_array cl) , LInt r :: q -> value_offsets (Cst (List.nth cl !r)) q
|
99
|
| Fun (f, vl) , _ -> Fun (f, List.map (fun v -> value_offsets v offsets) vl)
|
100
|
| _ , LInt r :: q -> value_offsets (Access (v, Cst (Const_int !r))) q
|
101
|
| _ , LVar i :: q -> value_offsets (Access (v, Var i)) q
|
102
|
*)
|
103
|
(* Computes the list of nested loop variables together with their dimension bounds.
|
104
|
- LInt r stands for loop expansion (no loop variable, but int loop index)
|
105
|
- LVar v stands for loop variable v
|
106
|
*)
|
107
|
let rec mk_loop_variables m ty depth =
|
108
|
match (Types.repr ty).Types.tdesc, depth with
|
109
|
| Types.Tarray (d, ty'), 0 ->
|
110
|
let v = mk_loop_var m () in
|
111
|
(d, LVar v) :: mk_loop_variables m ty' 0
|
112
|
| Types.Tarray (d, ty'), _ ->
|
113
|
let r = ref (-1) in
|
114
|
(d, LInt r) :: mk_loop_variables m ty' (depth - 1)
|
115
|
| _, 0 -> []
|
116
|
| _ -> assert false
|
117
|
|
118
|
let reorder_loop_variables loop_vars =
|
119
|
let (int_loops, var_loops) =
|
120
|
List.partition (function (_, LInt _) -> true | _ -> false) loop_vars
|
121
|
in
|
122
|
var_loops @ int_loops
|
123
|
|
124
|
(* Prints a one loop variable suffix for arrays *)
|
125
|
let pp_loop_var pp_val fmt lv =
|
126
|
match snd lv with
|
127
|
| LVar v -> fprintf fmt "[%s]" v
|
128
|
| LInt r -> fprintf fmt "[%d]" !r
|
129
|
| LAcc i -> fprintf fmt "[%a]" pp_val i
|
130
|
|
131
|
(* Prints a suffix of loop variables for arrays *)
|
132
|
let pp_suffix pp_val =
|
133
|
pp_print_list ~pp_sep:pp_print_nothing (pp_loop_var pp_val)
|
134
|
|
135
|
(* Prints a value expression [v], with internal function calls only.
|
136
|
[pp_var] is a printer for variables (typically [pp_c_var_read]),
|
137
|
but an offset suffix may be added for array variables
|
138
|
*)
|
139
|
(* Prints a constant value before a suffix (needs casting) *)
|
140
|
let rec pp_c_const_suffix var_type fmt c =
|
141
|
match c with
|
142
|
| Const_int i ->
|
143
|
pp_print_int fmt i
|
144
|
| Const_real r ->
|
145
|
Real.pp fmt r
|
146
|
| Const_tag t ->
|
147
|
pp_c_tag fmt t
|
148
|
| Const_array ca ->
|
149
|
let var_type = Types.array_element_type var_type in
|
150
|
fprintf fmt "(%a[])%a"
|
151
|
(pp_c_type "") var_type
|
152
|
(pp_print_braced (pp_c_const_suffix var_type)) ca
|
153
|
| Const_struct fl ->
|
154
|
pp_print_braced
|
155
|
(fun fmt (f, c) ->
|
156
|
(pp_c_const_suffix (Types.struct_field_type var_type f)) fmt c)
|
157
|
fmt fl
|
158
|
| Const_string _
|
159
|
| Const_modeid _ -> assert false (* string occurs in annotations not in C *)
|
160
|
|
161
|
(* Prints a [value] of type [var_type] indexed by the suffix list [loop_vars] *)
|
162
|
let rec pp_value_suffix m self var_type loop_vars pp_var fmt value =
|
163
|
(*eprintf "pp_value_suffix: %a %a %a@." Types.print_ty var_type Machine_code.pp_val value pp_suffix loop_vars;*)
|
164
|
let pp_suffix = pp_suffix (pp_value_suffix m self var_type [] pp_var) in
|
165
|
match loop_vars, value.value_desc with
|
166
|
| (x, LAcc i) :: q, _ when is_const_index i ->
|
167
|
let r = ref (Dimension.size_const_dimension (dimension_of_value i)) in
|
168
|
pp_value_suffix m self var_type ((x, LInt r)::q) pp_var fmt value
|
169
|
| (_, LInt r) :: q, Cst (Const_array cl) ->
|
170
|
let var_type = Types.array_element_type var_type in
|
171
|
pp_value_suffix m self var_type q pp_var fmt
|
172
|
(mk_val (Cst (List.nth cl !r)) Type_predef.type_int)
|
173
|
| (_, LInt r) :: q, Array vl ->
|
174
|
let var_type = Types.array_element_type var_type in
|
175
|
pp_value_suffix m self var_type q pp_var fmt (List.nth vl !r)
|
176
|
| loop_var :: q, Array vl ->
|
177
|
let var_type = Types.array_element_type var_type in
|
178
|
fprintf fmt "(%a[])%a%a"
|
179
|
(pp_c_type "") var_type
|
180
|
(pp_print_braced (pp_value_suffix m self var_type q pp_var)) vl
|
181
|
pp_suffix [loop_var]
|
182
|
| [], Array vl ->
|
183
|
let var_type = Types.array_element_type var_type in
|
184
|
fprintf fmt "(%a[])%a"
|
185
|
(pp_c_type "") var_type
|
186
|
(pp_print_braced (pp_value_suffix m self var_type [] pp_var)) vl
|
187
|
| _ :: q, Power (v, _) ->
|
188
|
pp_value_suffix m self var_type q pp_var fmt v
|
189
|
| _, Fun (n, vl) ->
|
190
|
pp_basic_lib_fun (Types.is_int_type value.value_type) n
|
191
|
(pp_value_suffix m self var_type loop_vars pp_var) fmt vl
|
192
|
| _, Access (v, i) ->
|
193
|
let var_type = Type_predef.type_array (Dimension.mkdim_var ()) var_type in
|
194
|
pp_value_suffix m self var_type
|
195
|
((Dimension.mkdim_var (), LAcc i) :: loop_vars) pp_var fmt v
|
196
|
| _, Var v ->
|
197
|
if is_memory m v then
|
198
|
(* array memory vars are represented by an indirection to a local var with the right type,
|
199
|
in order to avoid casting everywhere. *)
|
200
|
if Types.is_array_type v.var_type
|
201
|
then fprintf fmt "%a%a" pp_var v pp_suffix loop_vars
|
202
|
else fprintf fmt "%s->_reg.%a%a" self pp_var v pp_suffix loop_vars
|
203
|
else
|
204
|
fprintf fmt "%a%a" pp_var v pp_suffix loop_vars
|
205
|
| _, Cst cst ->
|
206
|
pp_c_const_suffix var_type fmt cst
|
207
|
| _, _ ->
|
208
|
eprintf "internal error: C_backend_src.pp_value_suffix %a %a %a@."
|
209
|
Types.print_ty var_type (pp_val m) value pp_suffix loop_vars;
|
210
|
assert false
|
211
|
|
212
|
(* Subsumes C_backend_common.pp_c_val to cope with aggressive substitution
|
213
|
which may yield constant arrays in expressions.
|
214
|
Type is needed to correctly print constant arrays.
|
215
|
*)
|
216
|
let pp_c_val m self pp_var fmt v =
|
217
|
pp_value_suffix m self v.value_type [] pp_var fmt v
|
218
|
|
219
|
let pp_basic_assign pp_var fmt typ var_name value =
|
220
|
if Types.is_real_type typ && !Options.mpfr
|
221
|
then
|
222
|
Mpfr.pp_inject_assign pp_var fmt (var_name, value)
|
223
|
else
|
224
|
fprintf fmt "%a = %a;"
|
225
|
pp_var var_name
|
226
|
pp_var value
|
227
|
|
228
|
(* type_directed assignment: array vs. statically sized type
|
229
|
- [var_type]: type of variable to be assigned
|
230
|
- [var_name]: name of variable to be assigned
|
231
|
- [value]: assigned value
|
232
|
- [pp_var]: printer for variables
|
233
|
*)
|
234
|
let pp_assign m self pp_var fmt var_type var_name value =
|
235
|
let depth = expansion_depth value in
|
236
|
(*eprintf "pp_assign %a %a %a %d@." Types.print_ty var_type pp_val var_name pp_val value depth;*)
|
237
|
let loop_vars = mk_loop_variables m var_type depth in
|
238
|
let reordered_loop_vars = reorder_loop_variables loop_vars in
|
239
|
let rec aux typ fmt vars =
|
240
|
match vars with
|
241
|
| [] ->
|
242
|
pp_basic_assign (pp_value_suffix m self var_type loop_vars pp_var)
|
243
|
fmt typ var_name value
|
244
|
| (d, LVar i) :: q ->
|
245
|
let typ' = Types.array_element_type typ in
|
246
|
(*eprintf "pp_aux %a %s@." Dimension.pp_dimension d i;*)
|
247
|
fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}"
|
248
|
i i i pp_c_dimension d i
|
249
|
(aux typ') q
|
250
|
| (d, LInt r) :: q ->
|
251
|
(*eprintf "pp_aux %a %d@." Dimension.pp_dimension d (!r);*)
|
252
|
let typ' = Types.array_element_type typ in
|
253
|
let szl = Utils.enumerate (Dimension.size_const_dimension d) in
|
254
|
fprintf fmt "@[<v 2>{@,%a@]@,}"
|
255
|
(pp_print_list (fun fmt i -> r := i; aux typ' fmt q)) szl
|
256
|
| _ -> assert false
|
257
|
in
|
258
|
begin
|
259
|
reset_loop_counter ();
|
260
|
(*reset_addr_counter ();*)
|
261
|
aux var_type fmt reordered_loop_vars;
|
262
|
(*eprintf "end pp_assign@.";*)
|
263
|
end
|
264
|
|
265
|
let pp_machine_ pp_machine_name fn_name m self fmt inst =
|
266
|
let (node, static) = try List.assoc inst m.minstances with Not_found ->
|
267
|
eprintf "internal error: %s %s %s %s:@." fn_name m.mname.node_id self inst;
|
268
|
raise Not_found
|
269
|
in
|
270
|
fprintf fmt "%a(%a%s->%s);"
|
271
|
pp_machine_name (node_name node)
|
272
|
(pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma
|
273
|
Dimension.pp_dimension) static
|
274
|
self inst
|
275
|
|
276
|
let pp_machine_reset =
|
277
|
pp_machine_ pp_machine_reset_name "pp_machine_reset"
|
278
|
|
279
|
let pp_machine_init =
|
280
|
pp_machine_ pp_machine_init_name "pp_machine_init"
|
281
|
|
282
|
let pp_machine_clear =
|
283
|
pp_machine_ pp_machine_clear_name "pp_machine_clear"
|
284
|
|
285
|
let pp_call m self pp_read pp_write fmt i
|
286
|
(inputs: Machine_code_types.value_t list) (outputs: var_decl list) =
|
287
|
try (* stateful node instance *)
|
288
|
let n, _ = List.assoc i m.minstances in
|
289
|
fprintf fmt "%a (%a%a%s->%s);"
|
290
|
pp_machine_step_name (node_name n)
|
291
|
(pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma
|
292
|
(pp_c_val m self pp_read)) inputs
|
293
|
(pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma
|
294
|
pp_write) outputs
|
295
|
self
|
296
|
i
|
297
|
with Not_found -> (* stateless node instance *)
|
298
|
let n, _ = List.assoc i m.mcalls in
|
299
|
fprintf fmt "%a (%a%a);"
|
300
|
pp_machine_step_name (node_name n)
|
301
|
(pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma
|
302
|
(pp_c_val m self pp_read)) inputs
|
303
|
(pp_print_list ~pp_sep:pp_print_comma pp_write) outputs
|
304
|
|
305
|
let pp_basic_instance_call m self =
|
306
|
pp_call m self (pp_c_var_read m) (pp_c_var_write m)
|
307
|
|
308
|
let pp_instance_call m self fmt i (inputs: Machine_code_types.value_t list) (outputs: var_decl list) =
|
309
|
let pp_offset pp_var indices fmt var =
|
310
|
fprintf fmt "%a%a"
|
311
|
pp_var var
|
312
|
(pp_print_list ~pp_sep:pp_print_nothing (fun fmt -> fprintf fmt "[%s]"))
|
313
|
indices
|
314
|
in
|
315
|
let rec aux indices fmt typ =
|
316
|
if Types.is_array_type typ
|
317
|
then
|
318
|
let dim = Types.array_type_dimension typ in
|
319
|
let idx = mk_loop_var m () in
|
320
|
fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}"
|
321
|
idx idx idx pp_c_dimension dim idx
|
322
|
(aux (idx::indices)) (Types.array_element_type typ)
|
323
|
else
|
324
|
let pp_read = pp_offset (pp_c_var_read m) indices in
|
325
|
let pp_write = pp_offset (pp_c_var_write m) indices in
|
326
|
pp_call m self pp_read pp_write fmt i inputs outputs
|
327
|
in
|
328
|
reset_loop_counter ();
|
329
|
aux [] fmt (List.hd inputs).Machine_code_types.value_type
|
330
|
|
331
|
let rec pp_conditional dependencies (m: machine_t) self fmt c tl el =
|
332
|
fprintf fmt "@[<v 2>if (%a) {%a@]@,@[<v 2>} else {%a@]@,}"
|
333
|
(pp_c_val m self (pp_c_var_read m)) c
|
334
|
(pp_print_list ~pp_prologue:pp_print_cut
|
335
|
(pp_machine_instr dependencies m self)) tl
|
336
|
(pp_print_list ~pp_prologue:pp_print_cut
|
337
|
(pp_machine_instr dependencies m self)) el
|
338
|
|
339
|
and pp_machine_instr dependencies (m: machine_t) self fmt instr =
|
340
|
match get_instr_desc instr with
|
341
|
| MNoReset _ -> ()
|
342
|
| MReset i ->
|
343
|
pp_machine_reset m self fmt i
|
344
|
| MLocalAssign (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
|
| MStateAssign (i,v) ->
|
349
|
pp_assign
|
350
|
m self (pp_c_var_read m) fmt
|
351
|
i.var_type (mk_val (Var i) i.var_type) v
|
352
|
| MStep ([i0], i, vl) when Basic_library.is_value_internal_fun (mk_val (Fun (i, vl)) i0.var_type) ->
|
353
|
pp_machine_instr dependencies m self fmt
|
354
|
(update_instr_desc instr (MLocalAssign (i0, mk_val (Fun (i, vl)) i0.var_type)))
|
355
|
| MStep (il, i, vl) when !Options.mpfr && Mpfr.is_homomorphic_fun i ->
|
356
|
pp_instance_call m self fmt i vl il
|
357
|
| MStep ([i0], i, vl) when has_c_prototype i dependencies ->
|
358
|
fprintf fmt "%a = %s%a;"
|
359
|
(pp_c_val m self (pp_c_var_read m)) (mk_val (Var i0) i0.var_type)
|
360
|
i
|
361
|
(pp_print_parenthesized (pp_c_val m self (pp_c_var_read m))) vl
|
362
|
| MStep (il, i, vl) ->
|
363
|
pp_basic_instance_call m self fmt i vl il
|
364
|
| MBranch (_, []) ->
|
365
|
eprintf "internal error: C_backend_src.pp_machine_instr %a@."
|
366
|
(pp_instr m) instr;
|
367
|
assert false
|
368
|
| MBranch (g, hl) ->
|
369
|
if let t = fst (List.hd hl) in t = tag_true || t = tag_false
|
370
|
then (* boolean case, needs special treatment in C because truth value is not unique *)
|
371
|
(* may disappear if we optimize code by replacing last branch test with default *)
|
372
|
let tl = try List.assoc tag_true hl with Not_found -> [] in
|
373
|
let el = try List.assoc tag_false hl with Not_found -> [] in
|
374
|
pp_conditional dependencies m self fmt g tl el
|
375
|
else (* enum type case *)
|
376
|
(*let g_typ = Typing.type_const Location.dummy_loc (Const_tag (fst (List.hd hl))) in*)
|
377
|
fprintf fmt "@[<v 2>switch(%a) {@,%a@,}@]"
|
378
|
(pp_c_val m self (pp_c_var_read m)) g
|
379
|
(pp_print_list ~pp_open_box:pp_open_vbox0
|
380
|
(pp_machine_branch dependencies m self)) hl
|
381
|
| MSpec s ->
|
382
|
fprintf fmt "@[/*@@ %s */@]@ " s
|
383
|
| MComment s ->
|
384
|
fprintf fmt "/*%s*/@ " s
|
385
|
|
386
|
and pp_machine_branch dependencies m self fmt (t, h) =
|
387
|
fprintf fmt "@[<v 2>case %a:@,%a@,break;@]"
|
388
|
pp_c_tag t
|
389
|
(pp_print_list ~pp_open_box:pp_open_vbox0
|
390
|
(pp_machine_instr dependencies m self)) h
|
391
|
|
392
|
let pp_machine_nospec_instr dependencies m self fmt _i instr =
|
393
|
pp_machine_instr dependencies m self fmt instr
|
394
|
|
395
|
let pp_machine_step_instr dependencies m self fmt i instr =
|
396
|
fprintf fmt "%a%a%a"
|
397
|
(if i = 0 then
|
398
|
(fun fmt () -> Mod.pp_step_instr_spec m self fmt (i-1, instr))
|
399
|
else
|
400
|
pp_print_nothing) ()
|
401
|
(pp_machine_instr dependencies m self) instr
|
402
|
(Mod.pp_step_instr_spec m self) (i, instr)
|
403
|
|
404
|
(********************************************************************************************)
|
405
|
(* C file Printing functions *)
|
406
|
(********************************************************************************************)
|
407
|
|
408
|
let print_const_def fmt tdecl =
|
409
|
let cdecl = const_of_top tdecl in
|
410
|
if !Options.mpfr && Types.(is_real_type (array_base_type cdecl.const_type))
|
411
|
then
|
412
|
fprintf fmt "%a;"
|
413
|
(pp_c_type cdecl.const_id) (Types.dynamic_type cdecl.const_type)
|
414
|
else
|
415
|
fprintf fmt "%a = %a;"
|
416
|
(pp_c_type cdecl.const_id) cdecl.const_type
|
417
|
pp_c_const cdecl.const_value
|
418
|
|
419
|
let print_alloc_instance fmt (i, (m, static)) =
|
420
|
fprintf fmt "_alloc->%s = %a %a;"
|
421
|
i
|
422
|
pp_machine_alloc_name (node_name m)
|
423
|
(pp_print_parenthesized Dimension.pp_dimension) static
|
424
|
|
425
|
let print_dealloc_instance fmt (i, (m, _)) =
|
426
|
fprintf fmt "%a (_alloc->%s);"
|
427
|
pp_machine_dealloc_name (node_name m)
|
428
|
i
|
429
|
|
430
|
let const_locals m =
|
431
|
List.filter (fun vdecl -> vdecl.var_dec_const) m.mstep.step_locals
|
432
|
|
433
|
let pp_c_decl_array_mem self fmt id =
|
434
|
fprintf fmt "%a = (%a) (%s->_reg.%s)"
|
435
|
(pp_c_type (sprintf "(*%s)" id.var_id)) id.var_type
|
436
|
(pp_c_type "(*)") id.var_type
|
437
|
self
|
438
|
id.var_id
|
439
|
|
440
|
let print_alloc_const fmt m =
|
441
|
pp_print_list
|
442
|
~pp_sep:(pp_print_endcut ";") ~pp_eol:(pp_print_endcut ";")
|
443
|
(pp_c_decl_local_var m) fmt (const_locals m)
|
444
|
|
445
|
let print_alloc_array fmt vdecl =
|
446
|
let base_type = Types.array_base_type vdecl.var_type in
|
447
|
let size_types = Types.array_type_multi_dimension vdecl.var_type in
|
448
|
let size_type = Dimension.multi_dimension_product vdecl.var_loc size_types in
|
449
|
fprintf fmt
|
450
|
"_alloc->_reg.%s = (%a*) malloc((%a)*sizeof(%a));@,\
|
451
|
assert(_alloc->%s);"
|
452
|
vdecl.var_id
|
453
|
(pp_c_type "") base_type
|
454
|
Dimension.pp_dimension size_type
|
455
|
(pp_c_type "") base_type
|
456
|
vdecl.var_id
|
457
|
|
458
|
let print_dealloc_array fmt vdecl =
|
459
|
fprintf fmt "free (_alloc->_reg.%s);"
|
460
|
vdecl.var_id
|
461
|
|
462
|
let array_mems m =
|
463
|
List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory
|
464
|
|
465
|
let print_alloc_code fmt m =
|
466
|
fprintf fmt
|
467
|
"%a *_alloc;@,\
|
468
|
_alloc = (%a *) malloc(sizeof(%a));@,\
|
469
|
assert(_alloc);@,\
|
470
|
%a%areturn _alloc;"
|
471
|
(pp_machine_memtype_name ~ghost:false) m.mname.node_id
|
472
|
(pp_machine_memtype_name ~ghost:false) m.mname.node_id
|
473
|
(pp_machine_memtype_name ~ghost:false) m.mname.node_id
|
474
|
(pp_print_list ~pp_sep:pp_print_nothing print_alloc_array) (array_mems m)
|
475
|
(pp_print_list ~pp_sep:pp_print_nothing print_alloc_instance) m.minstances
|
476
|
|
477
|
let print_dealloc_code fmt m =
|
478
|
fprintf fmt
|
479
|
"%a%afree (_alloc);@,\
|
480
|
return;"
|
481
|
(pp_print_list ~pp_sep:pp_print_nothing print_dealloc_array) (array_mems m)
|
482
|
(pp_print_list ~pp_sep:pp_print_nothing print_dealloc_instance) m.minstances
|
483
|
|
484
|
(* let print_stateless_init_code fmt m self =
|
485
|
* let minit = List.map (fun i -> match get_instr_desc i with MReset i -> i | _ -> assert false) m.minit in
|
486
|
* let array_mems = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in
|
487
|
* fprintf fmt "@[<v 2>%a {@,%a%t%a%t%a%treturn;@]@,}@.@."
|
488
|
* (print_init_prototype self) (m.mname.node_id, m.mstatic)
|
489
|
* (\* array mems *\)
|
490
|
* (Utils.fprintf_list ~sep:";@," (pp_c_decl_array_mem self)) array_mems
|
491
|
* (Utils.pp_final_char_if_non_empty ";@," array_mems)
|
492
|
* (\* memory initialization *\)
|
493
|
* (Utils.fprintf_list ~sep:"@," (pp_initialize m self (pp_c_var_read m))) m.mmemory
|
494
|
* (Utils.pp_newline_if_non_empty m.mmemory)
|
495
|
* (\* sub-machines initialization *\)
|
496
|
* (Utils.fprintf_list ~sep:"@," (pp_machine_init m self)) minit
|
497
|
* (Utils.pp_newline_if_non_empty m.minit)
|
498
|
*
|
499
|
* let print_stateless_clear_code fmt m self =
|
500
|
* let minit = List.map (fun i -> match get_instr_desc i with MReset i -> i | _ -> assert false) m.minit in
|
501
|
* let array_mems = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in
|
502
|
* fprintf fmt "@[<v 2>%a {@,%a%t%a%t%a%treturn;@]@,}@.@."
|
503
|
* (print_clear_prototype self) (m.mname.node_id, m.mstatic)
|
504
|
* (\* array mems *\)
|
505
|
* (Utils.fprintf_list ~sep:";@," (pp_c_decl_array_mem self)) array_mems
|
506
|
* (Utils.pp_final_char_if_non_empty ";@," array_mems)
|
507
|
* (\* memory clear *\)
|
508
|
* (Utils.fprintf_list ~sep:"@," (pp_clear m self (pp_c_var_read m))) m.mmemory
|
509
|
* (Utils.pp_newline_if_non_empty m.mmemory)
|
510
|
* (\* sub-machines clear*\)
|
511
|
* (Utils.fprintf_list ~sep:"@," (pp_machine_clear m self)) minit
|
512
|
* (Utils.pp_newline_if_non_empty m.minit) *)
|
513
|
|
514
|
let pp_c_check m self fmt (loc, check) =
|
515
|
fprintf fmt "@[<v>%a@,assert (%a);@]"
|
516
|
Location.pp_c_loc loc
|
517
|
(pp_c_val m self (pp_c_var_read m)) check
|
518
|
|
519
|
let pp_print_function
|
520
|
~pp_prototype ~prototype
|
521
|
?(pp_spec=pp_print_nothing)
|
522
|
?(pp_local=pp_print_nothing) ?(base_locals=[])
|
523
|
?(pp_array_mem=pp_print_nothing) ?(array_mems=[])
|
524
|
?(pp_init_mpfr_local=pp_print_nothing)
|
525
|
?(pp_clear_mpfr_local=pp_print_nothing)
|
526
|
?(mpfr_locals=[])
|
527
|
?(pp_check=pp_print_nothing) ?(checks=[])
|
528
|
?(pp_extra=pp_print_nothing)
|
529
|
?(pp_instr=fun fmt _ _ -> pp_print_nothing fmt ()) ?(instrs=[])
|
530
|
fmt =
|
531
|
fprintf fmt
|
532
|
"%a@[<v 2>%a {@,\
|
533
|
%a%a\
|
534
|
%a%a%a%a%areturn;@]@,\
|
535
|
}"
|
536
|
pp_spec ()
|
537
|
pp_prototype prototype
|
538
|
(* locals *)
|
539
|
(pp_print_list
|
540
|
~pp_open_box:pp_open_vbox0
|
541
|
~pp_sep:pp_print_semicolon
|
542
|
~pp_eol:pp_print_semicolon
|
543
|
pp_local)
|
544
|
base_locals
|
545
|
(* array mems *)
|
546
|
(pp_print_list
|
547
|
~pp_open_box:pp_open_vbox0
|
548
|
~pp_sep:pp_print_semicolon
|
549
|
~pp_eol:pp_print_semicolon
|
550
|
pp_array_mem)
|
551
|
array_mems
|
552
|
(* locals initialization *)
|
553
|
(pp_print_list
|
554
|
~pp_epilogue:pp_print_cut
|
555
|
pp_init_mpfr_local) (mpfr_vars mpfr_locals)
|
556
|
(* check assertions *)
|
557
|
(pp_print_list pp_check) checks
|
558
|
(* instrs *)
|
559
|
(pp_print_list_i
|
560
|
~pp_open_box:pp_open_vbox0
|
561
|
~pp_epilogue:pp_print_cut
|
562
|
pp_instr) instrs
|
563
|
(* locals clear *)
|
564
|
(pp_print_list
|
565
|
~pp_epilogue:pp_print_cut
|
566
|
pp_clear_mpfr_local) (mpfr_vars mpfr_locals)
|
567
|
(* extra *)
|
568
|
pp_extra ()
|
569
|
|
570
|
let node_of_machine m = {
|
571
|
top_decl_desc = Node m.mname;
|
572
|
top_decl_loc = Location.dummy_loc;
|
573
|
top_decl_owner = "";
|
574
|
top_decl_itf = false
|
575
|
}
|
576
|
|
577
|
let print_stateless_code dependencies fmt m =
|
578
|
let self = "__ERROR__" in
|
579
|
if not (!Options.ansi && is_generic_node (node_of_machine m))
|
580
|
then
|
581
|
(* C99 code *)
|
582
|
pp_print_function
|
583
|
~pp_prototype:print_stateless_prototype
|
584
|
~prototype:(m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs)
|
585
|
~pp_local:(pp_c_decl_local_var m)
|
586
|
~base_locals:m.mstep.step_locals
|
587
|
~pp_init_mpfr_local:(pp_initialize m self (pp_c_var_read m))
|
588
|
~pp_clear_mpfr_local:(pp_clear m self (pp_c_var_read m))
|
589
|
~mpfr_locals:m.mstep.step_locals
|
590
|
~pp_check:(pp_c_check m self)
|
591
|
~checks:m.mstep.step_checks
|
592
|
~pp_instr:(pp_machine_nospec_instr dependencies m self)
|
593
|
~instrs:m.mstep.step_instrs
|
594
|
fmt
|
595
|
else
|
596
|
(* C90 code *)
|
597
|
let gen_locals, base_locals = List.partition (fun v ->
|
598
|
Types.is_generic_type v.var_type) m.mstep.step_locals in
|
599
|
let gen_calls = List.map (fun e ->
|
600
|
let (id, _, _) = call_of_expr e
|
601
|
in mk_call_var_decl e.expr_loc id) m.mname.node_gencalls in
|
602
|
pp_print_function
|
603
|
~pp_prototype:print_stateless_prototype
|
604
|
~prototype:(m.mname.node_id,
|
605
|
m.mstep.step_inputs @ gen_locals @ gen_calls,
|
606
|
m.mstep.step_outputs)
|
607
|
~pp_local:(pp_c_decl_local_var m)
|
608
|
~base_locals
|
609
|
~pp_init_mpfr_local:(pp_initialize m self (pp_c_var_read m))
|
610
|
~pp_clear_mpfr_local:(pp_clear m self (pp_c_var_read m))
|
611
|
~mpfr_locals:m.mstep.step_locals
|
612
|
~pp_check:(pp_c_check m self)
|
613
|
~checks:m.mstep.step_checks
|
614
|
~pp_instr:(pp_machine_nospec_instr dependencies m self)
|
615
|
~instrs:m.mstep.step_instrs
|
616
|
fmt
|
617
|
|
618
|
let print_reset_code dependencies self fmt m =
|
619
|
pp_print_function
|
620
|
~pp_spec:(fun fmt () -> Mod.pp_reset_spec fmt self m)
|
621
|
~pp_prototype:(print_reset_prototype self)
|
622
|
~prototype:(m.mname.node_id, m.mstatic)
|
623
|
~pp_local:(pp_c_decl_local_var m)
|
624
|
~base_locals:(const_locals m)
|
625
|
~pp_instr:(pp_machine_nospec_instr dependencies m self)
|
626
|
~instrs:m.minit
|
627
|
fmt
|
628
|
|
629
|
let print_init_code self fmt m =
|
630
|
let minit = List.map (fun i ->
|
631
|
match get_instr_desc i with MReset i -> i | _ -> assert false) m.minit in
|
632
|
pp_print_function
|
633
|
~pp_prototype:(print_init_prototype self)
|
634
|
~prototype:(m.mname.node_id, m.mstatic)
|
635
|
~pp_array_mem:(pp_c_decl_array_mem self)
|
636
|
~array_mems:(array_mems m)
|
637
|
~pp_init_mpfr_local:(pp_initialize m self (pp_c_var_read m))
|
638
|
~mpfr_locals:m.mmemory
|
639
|
~pp_extra:(fun fmt () ->
|
640
|
pp_print_list
|
641
|
~pp_open_box:pp_open_vbox0
|
642
|
~pp_epilogue:pp_print_cut
|
643
|
(pp_machine_init m self)
|
644
|
fmt minit)
|
645
|
fmt
|
646
|
|
647
|
let print_clear_code self fmt m =
|
648
|
let minit = List.map (fun i ->
|
649
|
match get_instr_desc i with MReset i -> i | _ -> assert false) m.minit in
|
650
|
pp_print_function
|
651
|
~pp_prototype:(print_clear_prototype self)
|
652
|
~prototype:(m.mname.node_id, m.mstatic)
|
653
|
~pp_array_mem:(pp_c_decl_array_mem self)
|
654
|
~array_mems:(array_mems m)
|
655
|
~pp_clear_mpfr_local:(pp_clear m self (pp_c_var_read m))
|
656
|
~mpfr_locals:m.mmemory
|
657
|
~pp_extra:(fun fmt () ->
|
658
|
pp_print_list
|
659
|
~pp_open_box:pp_open_vbox0
|
660
|
~pp_epilogue:pp_print_cut
|
661
|
(pp_machine_clear m self)
|
662
|
fmt minit)
|
663
|
fmt
|
664
|
|
665
|
let print_step_code dependencies self fmt m =
|
666
|
if not (!Options.ansi && is_generic_node (node_of_machine m))
|
667
|
then
|
668
|
(* C99 code *)
|
669
|
pp_print_function
|
670
|
~pp_spec:(fun fmt () -> Mod.pp_step_spec fmt self m)
|
671
|
~pp_prototype:(print_step_prototype self)
|
672
|
~prototype:(m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs)
|
673
|
~pp_local:(pp_c_decl_local_var m)
|
674
|
~base_locals:m.mstep.step_locals
|
675
|
~pp_array_mem:(pp_c_decl_array_mem self)
|
676
|
~array_mems:(array_mems m)
|
677
|
~pp_init_mpfr_local:(pp_initialize m self (pp_c_var_read m))
|
678
|
~pp_clear_mpfr_local:(pp_clear m self (pp_c_var_read m))
|
679
|
~mpfr_locals:m.mstep.step_locals
|
680
|
~pp_check:(pp_c_check m self)
|
681
|
~checks:m.mstep.step_checks
|
682
|
~pp_instr:(pp_machine_step_instr dependencies m self)
|
683
|
~instrs:m.mstep.step_instrs
|
684
|
fmt
|
685
|
else
|
686
|
(* C90 code *)
|
687
|
let gen_locals, base_locals = List.partition (fun v ->
|
688
|
Types.is_generic_type v.var_type) m.mstep.step_locals in
|
689
|
let gen_calls = List.map (fun e ->
|
690
|
let id, _, _ = call_of_expr e in
|
691
|
mk_call_var_decl e.expr_loc id) m.mname.node_gencalls in
|
692
|
pp_print_function
|
693
|
~pp_spec:(fun fmt () -> Mod.pp_step_spec fmt self m)
|
694
|
~pp_prototype:(print_step_prototype self)
|
695
|
~prototype:(m.mname.node_id,
|
696
|
m.mstep.step_inputs @ gen_locals @ gen_calls,
|
697
|
m.mstep.step_outputs)
|
698
|
~pp_local:(pp_c_decl_local_var m)
|
699
|
~base_locals
|
700
|
~pp_init_mpfr_local:(pp_initialize m self (pp_c_var_read m))
|
701
|
~pp_clear_mpfr_local:(pp_clear m self (pp_c_var_read m))
|
702
|
~mpfr_locals:m.mstep.step_locals
|
703
|
~pp_check:(pp_c_check m self)
|
704
|
~checks:m.mstep.step_checks
|
705
|
~pp_instr:(pp_machine_step_instr dependencies m self)
|
706
|
~instrs:m.mstep.step_instrs
|
707
|
fmt
|
708
|
|
709
|
(********************************************************************************************)
|
710
|
(* MAIN C file Printing functions *)
|
711
|
(********************************************************************************************)
|
712
|
|
713
|
let pp_const_initialize m pp_var fmt const =
|
714
|
let var = Machine_code_common.mk_val
|
715
|
(Var (Corelang.var_decl_of_const const)) const.const_type in
|
716
|
let rec aux indices value fmt typ =
|
717
|
if Types.is_array_type typ
|
718
|
then
|
719
|
let dim = Types.array_type_dimension typ in
|
720
|
let szl = Utils.enumerate (Dimension.size_const_dimension dim) in
|
721
|
let typ' = Types.array_element_type typ in
|
722
|
let value = match value with
|
723
|
| Const_array ca -> List.nth ca
|
724
|
| _ -> assert false in
|
725
|
pp_print_list
|
726
|
(fun fmt i -> aux (string_of_int i :: indices) (value i) fmt typ') fmt szl
|
727
|
else
|
728
|
let indices = List.rev indices in
|
729
|
let pp_var_suffix fmt var =
|
730
|
fprintf fmt "%a%a" (pp_c_val m "" pp_var) var pp_array_suffix indices in
|
731
|
fprintf fmt "%a@,%a"
|
732
|
(Mpfr.pp_inject_init pp_var_suffix) var
|
733
|
(Mpfr.pp_inject_real pp_var_suffix pp_c_const) (var, value)
|
734
|
in
|
735
|
reset_loop_counter ();
|
736
|
aux [] const.const_value fmt const.const_type
|
737
|
|
738
|
let pp_const_clear pp_var fmt const =
|
739
|
let m = Machine_code_common.empty_machine in
|
740
|
let var = Corelang.var_decl_of_const const in
|
741
|
let rec aux indices fmt typ =
|
742
|
if Types.is_array_type typ
|
743
|
then
|
744
|
let dim = Types.array_type_dimension typ in
|
745
|
let idx = mk_loop_var m () in
|
746
|
fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}"
|
747
|
idx idx idx pp_c_dimension dim idx
|
748
|
(aux (idx::indices)) (Types.array_element_type typ)
|
749
|
else
|
750
|
let indices = List.rev indices in
|
751
|
let pp_var_suffix fmt var =
|
752
|
fprintf fmt "%a%a" (pp_c_var m "" pp_var) var pp_array_suffix indices in
|
753
|
Mpfr.pp_inject_clear pp_var_suffix fmt var
|
754
|
in
|
755
|
reset_loop_counter ();
|
756
|
aux [] fmt var.var_type
|
757
|
|
758
|
let print_import_init fmt dep =
|
759
|
let baseNAME = file_to_module_name dep.name in
|
760
|
fprintf fmt "%a();" pp_global_init_name baseNAME
|
761
|
|
762
|
let print_import_clear fmt dep =
|
763
|
let baseNAME = file_to_module_name dep.name in
|
764
|
fprintf fmt "%a();" pp_global_clear_name baseNAME
|
765
|
|
766
|
let print_global_init_code fmt (basename, prog, dependencies) =
|
767
|
let baseNAME = file_to_module_name basename in
|
768
|
let constants = List.map const_of_top (get_consts prog) in
|
769
|
fprintf fmt
|
770
|
"@[<v 2>%a {@,\
|
771
|
static %s init = 0;@,\
|
772
|
@[<v 2>if (!init) { @,\
|
773
|
init = 1;%a%a@]@,\
|
774
|
}@,\
|
775
|
return;@]@,\
|
776
|
}"
|
777
|
print_global_init_prototype baseNAME
|
778
|
(pp_c_basic_type_desc Type_predef.type_bool)
|
779
|
(* constants *)
|
780
|
(pp_print_list
|
781
|
~pp_prologue:pp_print_cut
|
782
|
(pp_const_initialize empty_machine (pp_c_var_read empty_machine)))
|
783
|
(mpfr_consts constants)
|
784
|
(* dependencies initialization *)
|
785
|
(pp_print_list
|
786
|
~pp_prologue:pp_print_cut
|
787
|
print_import_init) (List.filter (fun dep -> dep.local) dependencies)
|
788
|
|
789
|
let print_global_clear_code fmt (basename, prog, dependencies) =
|
790
|
let baseNAME = file_to_module_name basename in
|
791
|
let constants = List.map const_of_top (get_consts prog) in
|
792
|
fprintf fmt
|
793
|
"@[<v 2>%a {@,\
|
794
|
static %s clear = 0;@,\
|
795
|
@[<v 2>if (!clear) { @,\
|
796
|
clear = 1;%a%a@]@,\
|
797
|
}@,\
|
798
|
return;@]@,\
|
799
|
}"
|
800
|
print_global_clear_prototype baseNAME
|
801
|
(pp_c_basic_type_desc Type_predef.type_bool)
|
802
|
(* constants *)
|
803
|
(pp_print_list
|
804
|
~pp_prologue:pp_print_cut
|
805
|
(pp_const_clear (pp_c_var_read empty_machine))) (mpfr_consts constants)
|
806
|
(* dependencies initialization *)
|
807
|
(pp_print_list
|
808
|
~pp_prologue:pp_print_cut
|
809
|
print_import_clear) (List.filter (fun dep -> dep.local) dependencies)
|
810
|
|
811
|
let print_alloc_function fmt m =
|
812
|
if (not !Options.static_mem) then
|
813
|
(* Alloc functions, only if non static mode *)
|
814
|
fprintf fmt
|
815
|
"@[<v 2>%a {@,\
|
816
|
%a%a@]@,\
|
817
|
}@,\
|
818
|
@[<v 2>%a {@,\
|
819
|
%a%a@]@,\
|
820
|
@,"
|
821
|
print_alloc_prototype (m.mname.node_id, m.mstatic)
|
822
|
print_alloc_const m
|
823
|
print_alloc_code m
|
824
|
print_dealloc_prototype m.mname.node_id
|
825
|
print_alloc_const m
|
826
|
print_dealloc_code m
|
827
|
|
828
|
let print_mpfr_code self fmt m =
|
829
|
if !Options.mpfr then
|
830
|
fprintf fmt "@,@[<v>%a@,%a@]"
|
831
|
(* Init function *)
|
832
|
(print_init_code self) m
|
833
|
(* Clear function *)
|
834
|
(print_clear_code self) m
|
835
|
|
836
|
(* TODO: ACSL
|
837
|
- a contract machine shall not be directly printed in the C source
|
838
|
- but a regular machine associated to a contract machine shall integrate
|
839
|
the associated statements, updating its memories, at the end of the
|
840
|
function body.
|
841
|
- last one may print intermediate comment/acsl if/when they are present in
|
842
|
the sequence of instruction
|
843
|
*)
|
844
|
let print_machine dependencies fmt m =
|
845
|
if fst (get_stateless_status m) then
|
846
|
(* Step function *)
|
847
|
print_stateless_code dependencies fmt m
|
848
|
else
|
849
|
let self = mk_self m in
|
850
|
fprintf fmt "@[<v>%a%a@,@,%a%a@]"
|
851
|
print_alloc_function m
|
852
|
(* Reset function *)
|
853
|
(print_reset_code dependencies self) m
|
854
|
(* Step function *)
|
855
|
(print_step_code dependencies self) m
|
856
|
(print_mpfr_code self) m
|
857
|
|
858
|
let print_import_standard source_fmt () =
|
859
|
fprintf source_fmt
|
860
|
"@[<v>#include <assert.h>@,%a%a%a@]"
|
861
|
(if Machine_types.has_machine_type ()
|
862
|
then pp_print_endcut "#include <stdint.h>"
|
863
|
else pp_print_nothing) ()
|
864
|
(if not !Options.static_mem
|
865
|
then pp_print_endcut "#include <stdlib.h>"
|
866
|
else pp_print_nothing) ()
|
867
|
(if !Options.mpfr
|
868
|
then pp_print_endcut "#include <mpfr.h>"
|
869
|
else pp_print_nothing) ()
|
870
|
|
871
|
let print_extern_alloc_prototype fmt ind =
|
872
|
let static = List.filter (fun v -> v.var_dec_const) ind.nodei_inputs in
|
873
|
fprintf fmt "extern %a;@,extern %a;"
|
874
|
print_alloc_prototype (ind.nodei_id, static)
|
875
|
print_dealloc_prototype ind.nodei_id
|
876
|
|
877
|
let print_lib_c source_fmt basename prog machines dependencies =
|
878
|
fprintf source_fmt
|
879
|
"@[<v>\
|
880
|
%a\
|
881
|
%a@,\
|
882
|
@,\
|
883
|
%a@,\
|
884
|
%a\
|
885
|
%a\
|
886
|
%a\
|
887
|
%a\
|
888
|
%a\
|
889
|
%a\
|
890
|
%a\
|
891
|
@]@."
|
892
|
print_import_standard ()
|
893
|
print_import_prototype
|
894
|
{
|
895
|
local = true;
|
896
|
name = basename;
|
897
|
content = [];
|
898
|
is_stateful=true (* assuming it is stateful *);
|
899
|
}
|
900
|
|
901
|
(* Print the svn version number and the supported C standard (C90 or C99) *)
|
902
|
pp_print_version ()
|
903
|
|
904
|
(* Print dependencies *)
|
905
|
(pp_print_list
|
906
|
~pp_open_box:pp_open_vbox0
|
907
|
~pp_prologue:(pp_print_endcut "/* Import dependencies */")
|
908
|
print_import_prototype
|
909
|
~pp_epilogue:pp_print_cutcut) dependencies
|
910
|
|
911
|
(* Print consts *)
|
912
|
(pp_print_list
|
913
|
~pp_open_box:pp_open_vbox0
|
914
|
~pp_prologue:(pp_print_endcut "/* Global constants (definitions) */")
|
915
|
print_const_def
|
916
|
~pp_epilogue:pp_print_cutcut) (get_consts prog)
|
917
|
|
918
|
(* MPFR *)
|
919
|
(if !Options.mpfr then
|
920
|
fun fmt () ->
|
921
|
fprintf fmt
|
922
|
"@[<v>/* Global constants initialization */@,\
|
923
|
%a@,\
|
924
|
@,\
|
925
|
/* Global constants clearing */@,\
|
926
|
%a@]@,@,"
|
927
|
print_global_init_code (basename, prog, dependencies)
|
928
|
print_global_clear_code (basename, prog, dependencies)
|
929
|
else pp_print_nothing) ()
|
930
|
|
931
|
(if not !Options.static_mem then
|
932
|
fun fmt () ->
|
933
|
fprintf fmt
|
934
|
"@[<v>%a%a@]@,@,"
|
935
|
(pp_print_list
|
936
|
~pp_open_box:pp_open_vbox0
|
937
|
~pp_epilogue:pp_print_cut
|
938
|
~pp_prologue:(pp_print_endcut
|
939
|
"/* External allocation function prototypes */")
|
940
|
(fun fmt dep ->
|
941
|
pp_print_list
|
942
|
~pp_open_box:pp_open_vbox0
|
943
|
~pp_epilogue:pp_print_cut
|
944
|
print_extern_alloc_prototype
|
945
|
fmt
|
946
|
(List.filter_map (fun decl -> match decl.top_decl_desc with
|
947
|
| ImportedNode ind when not ind.nodei_stateless ->
|
948
|
Some ind
|
949
|
| _ -> None) dep.content))) dependencies
|
950
|
(pp_print_list
|
951
|
~pp_open_box:pp_open_vbox0
|
952
|
~pp_prologue:(pp_print_endcut
|
953
|
"/* Node allocation function prototypes */")
|
954
|
~pp_sep:pp_print_cutcut
|
955
|
(fun fmt m ->
|
956
|
fprintf fmt "%a;@,%a;"
|
957
|
print_alloc_prototype (m.mname.node_id, m.mstatic)
|
958
|
print_dealloc_prototype m.mname.node_id)) machines
|
959
|
else pp_print_nothing) ()
|
960
|
|
961
|
(* Print the struct definitions of all machines. *)
|
962
|
(pp_print_list
|
963
|
~pp_open_box:pp_open_vbox0
|
964
|
~pp_prologue:(pp_print_endcut "/* Struct definitions */")
|
965
|
~pp_sep:pp_print_cutcut
|
966
|
print_machine_struct
|
967
|
~pp_epilogue:pp_print_cutcut) machines
|
968
|
|
969
|
(* Print the spec predicates *)
|
970
|
(Mod.pp_predicates dependencies) machines
|
971
|
|
972
|
(* Print nodes one by one (in the previous order) *)
|
973
|
(pp_print_list
|
974
|
~pp_open_box:pp_open_vbox0
|
975
|
~pp_sep:pp_print_cutcut
|
976
|
(print_machine dependencies)) machines
|
977
|
|
978
|
end
|
979
|
|
980
|
(* Local Variables: *)
|
981
|
(* compile-command:"make -C ../../.." *)
|
982
|
(* End: *)
|