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