Revision ca7ff3f7
Added by Lélio Brun over 1 year ago
src/backends/C/c_backend_header.ml | ||
---|---|---|
17 | 17 |
open C_backend_common |
18 | 18 |
|
19 | 19 |
(********************************************************************************************) |
20 |
(* Header Printing functions *)
|
|
20 |
(* Header Printing functions *)
|
|
21 | 21 |
(********************************************************************************************) |
22 | 22 |
|
23 |
|
|
24 | 23 |
module type MODIFIERS_HDR = sig |
25 |
module GhostProto: MODIFIERS_GHOST_PROTO |
|
26 |
val print_machine_decl_prefix: Format.formatter -> machine_t -> unit |
|
27 |
val pp_import_arrow: formatter -> unit -> unit |
|
24 |
module GhostProto : MODIFIERS_GHOST_PROTO |
|
25 |
|
|
26 |
val print_machine_decl_prefix : Format.formatter -> machine_t -> unit |
|
27 |
|
|
28 |
val pp_import_arrow : formatter -> unit -> unit |
|
28 | 29 |
end |
29 | 30 |
|
30 | 31 |
module EmptyMod = struct |
31 | 32 |
module GhostProto = EmptyGhostProto |
32 |
let print_machine_decl_prefix = fun _ _ -> () |
|
33 |
|
|
34 |
let print_machine_decl_prefix _ _ = () |
|
35 |
|
|
33 | 36 |
let pp_import_arrow fmt () = |
34 | 37 |
fprintf fmt "#include \"%s/arrow.h%s\"" |
35 | 38 |
(Arrow.arrow_top_decl ()).top_decl_owner |
36 | 39 |
(if !Options.cpp then "pp" else "") |
37 | 40 |
end |
38 | 41 |
|
39 |
module Main = functor (Mod: MODIFIERS_HDR) -> struct |
|
40 |
|
|
41 |
module Protos = Protos(Mod.GhostProto) |
|
42 |
|
|
43 |
let print_import_standard fmt () = |
|
44 |
(* if Machine_types.has_machine_type () then *) |
|
45 |
fprintf fmt |
|
46 |
"#include <stdint.h>@,\ |
|
47 |
%a\ |
|
48 |
%a" |
|
49 |
(if !Options.mpfr then |
|
50 |
pp_print_endcut "#include <mpfr.h>" |
|
51 |
else pp_print_nothing) () |
|
52 |
Mod.pp_import_arrow () |
|
53 |
|
|
54 |
let rec print_static_val pp_var fmt v = |
|
55 |
match v.value_desc with |
|
56 |
| Cst c -> |
|
57 |
pp_c_const fmt c |
|
58 |
| Var v -> |
|
59 |
pp_var fmt v |
|
60 |
| Fun (n, vl) -> |
|
61 |
pp_basic_lib_fun (Types.is_int_type v.value_type) n |
|
62 |
(print_static_val pp_var) fmt vl |
|
63 |
| _ -> |
|
64 |
(* TODO: raise proper error *) |
|
65 |
eprintf "Internal error: C_backend_header.print_static_val"; |
|
66 |
assert false |
|
67 |
|
|
68 |
let print_constant_decl (m, attr, inst) pp_var fmt v = |
|
69 |
fprintf fmt "%s %a = %a" |
|
70 |
attr |
|
71 |
(pp_c_type (sprintf "%s ## %s" inst v.var_id)) v.var_type |
|
72 |
(print_static_val pp_var) (get_const_assign m v) |
|
73 |
|
|
74 |
let pp_var inst const_locals fmt v = |
|
75 |
if List.mem v const_locals then |
|
76 |
fprintf fmt "%s ## %s" inst v.var_id |
|
77 |
else fprintf fmt "%s" v.var_id |
|
78 |
|
|
79 |
let print_static_constant_decl (_, _, inst as macro) fmt const_locals = |
|
80 |
pp_print_list ~pp_open_box:pp_open_vbox0 |
|
81 |
~pp_sep:(pp_print_endcut ";\\") ~pp_eol:(pp_print_endcut ";\\") |
|
82 |
(print_constant_decl macro (pp_var inst const_locals)) |
|
83 |
fmt |
|
84 |
const_locals |
|
85 |
|
|
86 |
let print_static_declare_instance |
|
87 |
(m, attr, inst) const_locals fmt (i, (n, static)) = |
|
88 |
let values = List.map (value_of_dimension m) static in |
|
89 |
fprintf fmt "%a(%s, %a%s)" |
|
90 |
pp_machine_static_declare_name (node_name n) |
|
91 |
attr |
|
92 |
(pp_print_list ~pp_open_box:pp_open_hbox ~pp_sep:pp_print_comma |
|
93 |
~pp_eol:pp_print_comma (print_static_val (pp_var inst const_locals))) |
|
94 |
values |
|
95 |
i |
|
96 |
|
|
97 |
let print_static_declare_macro fmt (m, attr, inst as macro) = |
|
98 |
let const_locals = |
|
99 |
List.filter (fun vdecl -> vdecl.var_dec_const) m.mstep.step_locals in |
|
100 |
let array_mem = |
|
101 |
List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in |
|
102 |
fprintf fmt |
|
103 |
"@[<v 2>\ |
|
104 |
#define %a(%s, %a%s)\\@,\ |
|
105 |
%a%s %a %s;\\@,\ |
|
106 |
%a%a;\ |
|
107 |
@]" |
|
108 |
pp_machine_static_declare_name m.mname.node_id |
|
109 |
attr |
|
110 |
(pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma |
|
111 |
(pp_c_var_read m)) m.mstatic |
|
112 |
inst |
|
113 |
(* constants *) |
|
114 |
(print_static_constant_decl macro) const_locals |
|
115 |
attr |
|
116 |
(pp_machine_memtype_name ~ghost:false) m.mname.node_id |
|
117 |
inst |
|
118 |
(pp_print_list ~pp_open_box:pp_open_vbox0 |
|
119 |
~pp_sep:(pp_print_endcut ";\\") ~pp_eol:(pp_print_endcut ";\\") |
|
120 |
(pp_c_decl_local_var m)) array_mem |
|
121 |
(pp_print_list ~pp_open_box:pp_open_vbox0 |
|
122 |
~pp_sep:(pp_print_endcut ";\\") |
|
123 |
(fun fmt (i', m') -> |
|
124 |
let path = sprintf "%s ## _%s" inst i' in |
|
125 |
fprintf fmt "%a" |
|
126 |
(print_static_declare_instance macro const_locals) |
|
127 |
(path, m'))) m.minstances |
|
128 |
|
|
129 |
let print_static_link_instance fmt (i, (m, _)) = |
|
130 |
fprintf fmt "%a(%s)" pp_machine_static_link_name (node_name m) i |
|
131 |
|
|
132 |
(* Allocation of a node struct: |
|
133 |
- if node memory is an array/matrix/etc, we cast it to a pointer (see pp_registers_struct) |
|
134 |
*) |
|
135 |
let print_static_link_macro fmt (m, _, inst) = |
|
136 |
let array_mem = List.filter (fun v -> Types.is_array_type v.var_type) |
|
137 |
m.mmemory in |
|
138 |
fprintf fmt |
|
139 |
"@[<v>@[<v 2>\ |
|
140 |
#define %a(%s) do {\\@,\ |
|
141 |
%a%a;\\@]@,\ |
|
142 |
} while (0)\ |
|
143 |
@]" |
|
144 |
pp_machine_static_link_name m.mname.node_id |
|
145 |
inst |
|
146 |
(pp_print_list ~pp_open_box:pp_open_vbox0 |
|
147 |
~pp_sep:(pp_print_endcut ";\\") ~pp_eol:(pp_print_endcut ";\\") |
|
148 |
(fun fmt v -> |
|
149 |
fprintf fmt "%s._reg.%s = (%a*) &%s" |
|
150 |
inst |
|
151 |
v.var_id |
|
152 |
(fun fmt v -> pp_c_type "" fmt (Types.array_base_type v.var_type)) v |
|
153 |
v.var_id)) array_mem |
|
154 |
(pp_print_list ~pp_open_box:pp_open_vbox0 |
|
155 |
~pp_sep:(pp_print_endcut ";\\") |
|
156 |
(fun fmt (i',m') -> |
|
157 |
let path = sprintf "%s ## _%s" inst i' in |
|
158 |
fprintf fmt "%a;\\@,%s.%s = &%s" |
|
159 |
print_static_link_instance (path,m') |
|
160 |
inst |
|
161 |
i' |
|
162 |
path)) m.minstances |
|
163 |
|
|
164 |
let print_static_alloc_macro fmt (m, attr, inst) = |
|
165 |
fprintf fmt |
|
166 |
"@[<v>@[<v 2>\ |
|
167 |
#define %a(%s, %a%s)\\@,\ |
|
168 |
%a(%s, %a%s);\\@,\ |
|
169 |
%a(%s);\ |
|
170 |
@]@]" |
|
171 |
pp_machine_static_alloc_name m.mname.node_id |
|
172 |
attr |
|
173 |
(pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma |
|
174 |
(pp_c_var_read m)) m.mstatic |
|
175 |
inst |
|
176 |
pp_machine_static_declare_name m.mname.node_id |
|
177 |
attr |
|
178 |
(pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma |
|
179 |
(pp_c_var_read m)) m.mstatic |
|
180 |
inst |
|
181 |
pp_machine_static_link_name m.mname.node_id |
|
182 |
inst |
|
183 |
|
|
184 |
(* TODO: ACSL |
|
185 |
we do multiple things: |
|
186 |
- provide the semantics of the node as a predicate: function step and reset are associated to ACSL predicate |
|
187 |
- the node is associated to a refinement contract, wrt its ACSL sem |
|
188 |
- if the node is a regular node associated to a contract, print the contract as function contract. |
|
189 |
- do not print anything if this is a contract node |
|
190 |
*) |
|
191 |
let print_machine_alloc_decl fmt m = |
|
192 |
Mod.print_machine_decl_prefix fmt m; |
|
193 |
if not (fst (get_stateless_status m)) then |
|
194 |
if !Options.static_mem then |
|
195 |
(* Static allocation *) |
|
196 |
let macro = (m, mk_attribute m, mk_instance m) in |
|
197 |
fprintf fmt "%a@,%a@,%a" |
|
198 |
print_static_declare_macro macro |
|
199 |
print_static_link_macro macro |
|
200 |
print_static_alloc_macro macro |
|
201 |
else |
|
202 |
(* Dynamic allocation *) |
|
203 |
fprintf fmt "extern %a;@,extern %a" |
|
204 |
print_alloc_prototype (m.mname.node_id, m.mstatic) |
|
205 |
print_dealloc_prototype m.mname.node_id |
|
206 |
|
|
207 |
let print_machine_struct_top_decl_from_header fmt tdecl = |
|
208 |
let inode = imported_node_of_top tdecl in |
|
209 |
if not inode.nodei_stateless then |
|
210 |
(* Declare struct *) |
|
211 |
fprintf fmt "%a;" |
|
212 |
(pp_machine_memtype_name ~ghost:false) inode.nodei_id |
|
213 |
|
|
214 |
let print_stateless_C_prototype fmt (name, inputs, outputs) = |
|
215 |
let output = |
|
216 |
match outputs with |
|
217 |
| [hd] -> hd |
|
218 |
| _ -> assert false |
|
219 |
in |
|
220 |
fprintf fmt "%a %s %a" |
|
221 |
(pp_basic_c_type ~pp_c_basic_type_desc ~var_opt:None) output.var_type |
|
222 |
name |
|
223 |
(pp_print_parenthesized pp_c_decl_input_var) inputs |
|
224 |
|
|
225 |
let print_machine_decl_top_decl_from_header fmt tdecl = |
|
226 |
let inode = imported_node_of_top tdecl in |
|
227 |
(*Mod.print_machine_decl_prefix fmt m;*) |
|
228 |
let prototype = (inode.nodei_id, inode.nodei_inputs, inode.nodei_outputs) in |
|
229 |
if inode.nodei_prototype = Some "C" then |
|
230 |
if inode.nodei_stateless then |
|
231 |
fprintf fmt "extern %a;" print_stateless_C_prototype prototype |
|
232 |
else begin |
|
42 |
module Main = |
|
43 |
functor |
|
44 |
(Mod : MODIFIERS_HDR) |
|
45 |
-> |
|
46 |
struct |
|
47 |
module Protos = Protos (Mod.GhostProto) |
|
48 |
|
|
49 |
let print_import_standard fmt () = |
|
50 |
(* if Machine_types.has_machine_type () then *) |
|
51 |
fprintf fmt "#include <stdint.h>@,%a%a" |
|
52 |
(if !Options.mpfr then pp_print_endcut "#include <mpfr.h>" |
|
53 |
else pp_print_nothing) |
|
54 |
() Mod.pp_import_arrow () |
|
55 |
|
|
56 |
let rec print_static_val pp_var fmt v = |
|
57 |
match v.value_desc with |
|
58 |
| Cst c -> |
|
59 |
pp_c_const fmt c |
|
60 |
| Var v -> |
|
61 |
pp_var fmt v |
|
62 |
| Fun (n, vl) -> |
|
63 |
pp_basic_lib_fun |
|
64 |
(Types.is_int_type v.value_type) |
|
65 |
n (print_static_val pp_var) fmt vl |
|
66 |
| _ -> |
|
233 | 67 |
(* TODO: raise proper error *) |
234 |
Format.eprintf "internal error: print_machine_decl_top_decl_from_header";
|
|
68 |
eprintf "Internal error: C_backend_header.print_static_val";
|
|
235 | 69 |
assert false |
236 |
end |
|
237 |
else if inode.nodei_stateless then |
|
238 |
fprintf fmt "extern %a;" Protos.print_stateless_prototype prototype |
|
239 |
else |
|
240 |
let static_inputs = List.filter (fun v -> v.var_dec_const) |
|
241 |
inode.nodei_inputs in |
|
242 |
let used name = |
|
243 |
List.exists (fun v -> v.var_id = name) |
|
244 |
(inode.nodei_inputs @ inode.nodei_outputs) in |
|
245 |
let self = mk_new_name used "self" in |
|
246 |
let mem = mk_new_name used "mem" in |
|
247 |
let static_prototype = (inode.nodei_id, static_inputs) in |
|
248 |
fprintf fmt |
|
249 |
"extern %a;@,\ |
|
250 |
extern %a;@,\ |
|
251 |
extern %a;@,\ |
|
252 |
extern %a;@,\ |
|
253 |
extern %a;" |
|
254 |
(Protos.print_set_reset_prototype self mem) static_prototype |
|
255 |
(Protos.print_clear_reset_prototype self mem) static_prototype |
|
256 |
(Protos.print_init_prototype self) static_prototype |
|
257 |
(Protos.print_clear_prototype self) static_prototype |
|
258 |
(Protos.print_step_prototype self mem) prototype |
|
259 |
|
|
260 |
let print_const_top_decl fmt tdecl = |
|
261 |
let cdecl = const_of_top tdecl in |
|
262 |
fprintf fmt "extern %a;" |
|
263 |
(pp_c_type cdecl.const_id) |
|
264 |
(if !Options.mpfr && Types.(is_real_type (array_base_type cdecl.const_type)) |
|
265 |
then Types.dynamic_type cdecl.const_type |
|
266 |
else cdecl.const_type) |
|
267 |
|
|
268 |
let rec pp_c_type_decl filename cpt var fmt tdecl = |
|
269 |
match tdecl with |
|
270 |
| Tydec_any -> |
|
271 |
assert false |
|
272 |
| Tydec_int -> |
|
273 |
fprintf fmt "int %s" var |
|
274 |
| Tydec_real when !Options.mpfr -> |
|
275 |
fprintf fmt "%s %s" Mpfr.mpfr_t var |
|
276 |
| Tydec_real -> |
|
277 |
fprintf fmt "double %s" var |
|
278 |
(* | Tydec_float -> fprintf fmt "float %s" var *) |
|
279 |
| Tydec_bool -> |
|
280 |
fprintf fmt "_Bool %s" var |
|
281 |
| Tydec_clock ty -> |
|
282 |
pp_c_type_decl filename cpt var fmt ty |
|
283 |
| Tydec_const c -> |
|
284 |
fprintf fmt "%s %s" c var |
|
285 |
| Tydec_array (d, ty) -> |
|
286 |
fprintf fmt "%a[%a]" (pp_c_type_decl filename cpt var) ty pp_c_dimension d |
|
287 |
| Tydec_enum tl -> |
|
288 |
incr cpt; |
|
289 |
fprintf fmt "enum _enum_%s_%d %a %s" (protect_filename filename) !cpt |
|
290 |
(pp_print_braced pp_print_string) tl var |
|
291 |
| Tydec_struct fl -> |
|
292 |
incr cpt; |
|
293 |
fprintf fmt "struct _struct_%s_%d %a %s" (protect_filename filename) !cpt |
|
294 |
(pp_print_braced ~pp_sep:pp_print_semicolon |
|
295 |
(fun fmt (label, tdesc) -> pp_c_type_decl filename cpt label fmt tdesc)) |
|
296 |
fl var |
|
297 | 70 |
|
298 |
(* let print_type_definitions fmt filename = |
|
299 |
* let cpt_type = ref 0 in |
|
300 |
* Hashtbl.iter (fun typ decl -> |
|
301 |
* match typ with |
|
302 |
* | Tydec_const var -> |
|
303 |
* begin match decl.top_decl_desc with |
|
304 |
* | TypeDef tdef -> |
|
305 |
* fprintf fmt "typedef %a;@.@." |
|
306 |
* (pp_c_type_decl filename cpt_type var) tdef.tydef_desc |
|
307 |
* | _ -> assert false |
|
308 |
* end |
|
309 |
* | _ -> ()) type_table *) |
|
310 |
|
|
311 |
let reset_type_definitions, print_type_definition_top_decl_from_header = |
|
312 |
let cpt_type = ref 0 in |
|
313 |
(fun () -> cpt_type := 0), |
|
314 |
(fun filename fmt tdecl -> |
|
315 |
let typ = typedef_of_top tdecl in |
|
316 |
fprintf fmt "typedef %a;" |
|
317 |
(pp_c_type_decl filename cpt_type typ.tydef_id) typ.tydef_desc) |
|
318 |
|
|
319 |
(********************************************************************************************) |
|
320 |
(* MAIN Header Printing functions *) |
|
321 |
(********************************************************************************************) |
|
322 |
|
|
323 |
let print_alloc_header header_fmt basename _prog machines dependencies spec = |
|
324 |
(* Include once: start *) |
|
325 |
let baseNAME = file_to_module_name basename in |
|
326 |
fprintf header_fmt |
|
327 |
"@[<v>\ |
|
328 |
%a@,\ |
|
329 |
#ifndef _%s_alloc@,\ |
|
330 |
#define _%s_alloc@,\ |
|
331 |
@,\ |
|
332 |
/* Import header from %s */@,\ |
|
333 |
%a@,\ |
|
334 |
@,\ |
|
335 |
%a\ |
|
336 |
%a\ |
|
337 |
%a\ |
|
338 |
#endif\ |
|
339 |
@]" |
|
340 |
|
|
341 |
(* Print the svn version number and the supported C standard (C90 or C99) *) |
|
342 |
pp_print_version () |
|
343 |
|
|
344 |
baseNAME baseNAME |
|
345 |
|
|
346 |
(* Import the header *) |
|
347 |
basename |
|
348 |
print_import_prototype |
|
349 |
{ |
|
350 |
local = true; |
|
351 |
name = basename; |
|
352 |
content = []; |
|
353 |
is_stateful = true (* assuming it is staful *); |
|
354 |
} |
|
355 |
|
|
356 |
(* Print dependencies *) |
|
357 |
(pp_print_list |
|
358 |
~pp_open_box:pp_open_vbox0 |
|
359 |
~pp_prologue:(pp_print_endcut "/* Import dependencies */") |
|
360 |
print_import_alloc_prototype |
|
361 |
~pp_epilogue:pp_print_cutcut) dependencies |
|
362 |
|
|
363 |
(* Print the struct definitions of all machines. *) |
|
364 |
(pp_print_list |
|
365 |
~pp_open_box:pp_open_vbox0 |
|
366 |
~pp_prologue:(pp_print_endcut "/* Struct definitions */") |
|
367 |
~pp_sep:pp_print_cutcut |
|
368 |
print_machine_struct |
|
369 |
~pp_epilogue:pp_print_cutcut) machines |
|
370 |
|
|
371 |
(* Print the prototypes of all machines *) |
|
372 |
(pp_print_list |
|
373 |
~pp_open_box:pp_open_vbox0 |
|
374 |
~pp_prologue:(pp_print_endcut |
|
375 |
"/* Node allocation function/macro prototypes */") |
|
376 |
~pp_sep:pp_print_cutcut |
|
377 |
print_machine_alloc_decl |
|
378 |
~pp_epilogue:pp_print_cutcut) machines |
|
379 |
(* Include once: end *) |
|
380 |
|
|
381 |
(* Function called when compiling a lusi file and generating the associated C |
|
382 |
header. *) |
|
383 |
let print_header_from_header header_fmt basename header = |
|
384 |
(* Include once: start *) |
|
385 |
let baseNAME = file_to_module_name basename in |
|
386 |
let types = get_typedefs header in |
|
387 |
let consts = get_consts header in |
|
388 |
let nodes = get_imported_nodes header in |
|
389 |
let dependencies = get_dependencies header in |
|
390 |
reset_type_definitions (); |
|
391 |
fprintf header_fmt |
|
392 |
"@[<v>\ |
|
393 |
%a@,\ |
|
394 |
#ifndef _%s@,\ |
|
395 |
#define _%s@,\ |
|
396 |
@,\ |
|
397 |
/* Import standard library */@,\ |
|
398 |
%a@,\ |
|
399 |
@,\ |
|
400 |
%a\ |
|
401 |
%a\ |
|
402 |
%a\ |
|
403 |
%a\ |
|
404 |
%a\ |
|
405 |
%a\ |
|
406 |
#endif\ |
|
407 |
@]@." |
|
408 |
|
|
409 |
(* Print the version number and the supported C standard (C90 or C99) *) |
|
410 |
pp_print_version () |
|
411 |
|
|
412 |
baseNAME baseNAME |
|
413 |
|
|
414 |
(* imports standard library definitions (arrow) *) |
|
415 |
print_import_standard () |
|
416 |
|
|
417 |
(* imports dependencies *) |
|
418 |
(pp_print_list |
|
419 |
~pp_open_box:pp_open_vbox0 |
|
420 |
~pp_prologue:(pp_print_endcut "/* Import dependencies */") |
|
421 |
(fun fmt dep -> |
|
422 |
let local, name = dependency_of_top dep in |
|
423 |
print_import_prototype fmt |
|
424 |
{ |
|
425 |
local; |
|
426 |
name; |
|
427 |
content = []; |
|
428 |
is_stateful = true (* assuming it is stateful *) |
|
429 |
}) |
|
430 |
~pp_epilogue:pp_print_cutcut) |
|
431 |
dependencies |
|
432 |
|
|
433 |
(* Print the type definitions from the type table *) |
|
434 |
(pp_print_list |
|
435 |
~pp_open_box:pp_open_vbox0 |
|
436 |
~pp_prologue:(pp_print_endcut "/* Types definitions */") |
|
437 |
(print_type_definition_top_decl_from_header basename) |
|
438 |
~pp_epilogue:pp_print_cutcut) |
|
439 |
types |
|
440 |
|
|
441 |
(* Print the global constant declarations. *) |
|
442 |
(pp_print_list |
|
443 |
~pp_open_box:pp_open_vbox0 |
|
444 |
~pp_prologue: |
|
445 |
(pp_print_endcut |
|
446 |
"/* Global constants (declarations, definitions are in C file) */") |
|
447 |
print_const_top_decl |
|
448 |
~pp_epilogue:pp_print_cutcut) |
|
449 |
consts |
|
450 |
|
|
451 |
(* MPFR *) |
|
452 |
(if !Options.mpfr then |
|
453 |
fun fmt () -> fprintf fmt |
|
454 |
"/* Global initialization declaration */@,\ |
|
455 |
extern %a;@,@,\ |
|
456 |
/* Global clear declaration */@,\ |
|
457 |
extern %a;@,@," |
|
458 |
print_global_init_prototype baseNAME |
|
459 |
print_global_clear_prototype baseNAME |
|
460 |
else pp_print_nothing) () |
|
461 |
|
|
462 |
(* Print the struct declarations of all machines. *) |
|
463 |
(pp_print_list |
|
464 |
~pp_open_box:pp_open_vbox0 |
|
465 |
~pp_prologue:(pp_print_endcut "/* Struct declarations */") |
|
466 |
print_machine_struct_top_decl_from_header |
|
467 |
~pp_epilogue:pp_print_cutcut) |
|
468 |
nodes |
|
469 |
|
|
470 |
(* Print the prototypes of all machines *) |
|
471 |
(pp_print_list |
|
472 |
~pp_open_box:pp_open_vbox0 |
|
473 |
~pp_prologue:(pp_print_endcut "/* Nodes declarations */") |
|
474 |
~pp_sep:pp_print_cutcut |
|
475 |
print_machine_decl_top_decl_from_header |
|
476 |
~pp_epilogue:pp_print_cutcut) |
|
477 |
nodes |
|
478 |
|
|
479 |
end |
|
71 |
let print_constant_decl (m, attr, inst) pp_var fmt v = |
|
72 |
fprintf fmt "%s %a = %a" attr |
|
73 |
(pp_c_type (sprintf "%s ## %s" inst v.var_id)) |
|
74 |
v.var_type (print_static_val pp_var) (get_const_assign m v) |
|
75 |
|
|
76 |
let pp_var inst const_locals fmt v = |
|
77 |
if List.mem v const_locals then fprintf fmt "%s ## %s" inst v.var_id |
|
78 |
else fprintf fmt "%s" v.var_id |
|
79 |
|
|
80 |
let print_static_constant_decl ((_, _, inst) as macro) fmt const_locals = |
|
81 |
pp_print_list ~pp_open_box:pp_open_vbox0 ~pp_sep:(pp_print_endcut ";\\") |
|
82 |
~pp_eol:(pp_print_endcut ";\\") |
|
83 |
(print_constant_decl macro (pp_var inst const_locals)) |
|
84 |
fmt const_locals |
|
85 |
|
|
86 |
let print_static_declare_instance (m, attr, inst) const_locals fmt |
|
87 |
(i, (n, static)) = |
|
88 |
let values = List.map (value_of_dimension m) static in |
|
89 |
fprintf fmt "%a(%s, %a%s)" pp_machine_static_declare_name (node_name n) |
|
90 |
attr |
|
91 |
(pp_print_list ~pp_open_box:pp_open_hbox ~pp_sep:pp_print_comma |
|
92 |
~pp_eol:pp_print_comma |
|
93 |
(print_static_val (pp_var inst const_locals))) |
|
94 |
values i |
|
95 |
|
|
96 |
let print_static_declare_macro fmt ((m, attr, inst) as macro) = |
|
97 |
let const_locals = |
|
98 |
List.filter (fun vdecl -> vdecl.var_dec_const) m.mstep.step_locals |
|
99 |
in |
|
100 |
let array_mem = |
|
101 |
List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory |
|
102 |
in |
|
103 |
fprintf fmt "@[<v 2>#define %a(%s, %a%s)\\@,%a%s %a %s;\\@,%a%a;@]" |
|
104 |
pp_machine_static_declare_name m.mname.node_id attr |
|
105 |
(pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma |
|
106 |
(pp_c_var_read m)) |
|
107 |
m.mstatic inst |
|
108 |
(* constants *) |
|
109 |
(print_static_constant_decl macro) |
|
110 |
const_locals attr |
|
111 |
(pp_machine_memtype_name ~ghost:false) |
|
112 |
m.mname.node_id inst |
|
113 |
(pp_print_list ~pp_open_box:pp_open_vbox0 |
|
114 |
~pp_sep:(pp_print_endcut ";\\") ~pp_eol:(pp_print_endcut ";\\") |
|
115 |
(pp_c_decl_local_var m)) |
|
116 |
array_mem |
|
117 |
(pp_print_list ~pp_open_box:pp_open_vbox0 |
|
118 |
~pp_sep:(pp_print_endcut ";\\") (fun fmt (i', m') -> |
|
119 |
let path = sprintf "%s ## _%s" inst i' in |
|
120 |
fprintf fmt "%a" |
|
121 |
(print_static_declare_instance macro const_locals) |
|
122 |
(path, m'))) |
|
123 |
m.minstances |
|
124 |
|
|
125 |
let print_static_link_instance fmt (i, (m, _)) = |
|
126 |
fprintf fmt "%a(%s)" pp_machine_static_link_name (node_name m) i |
|
127 |
|
|
128 |
(* Allocation of a node struct: - if node memory is an array/matrix/etc, we |
|
129 |
cast it to a pointer (see pp_registers_struct) *) |
|
130 |
let print_static_link_macro fmt (m, _, inst) = |
|
131 |
let array_mem = |
|
132 |
List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory |
|
133 |
in |
|
134 |
fprintf fmt "@[<v>@[<v 2>#define %a(%s) do {\\@,%a%a;\\@]@,} while (0)@]" |
|
135 |
pp_machine_static_link_name m.mname.node_id inst |
|
136 |
(pp_print_list ~pp_open_box:pp_open_vbox0 |
|
137 |
~pp_sep:(pp_print_endcut ";\\") ~pp_eol:(pp_print_endcut ";\\") |
|
138 |
(fun fmt v -> |
|
139 |
fprintf fmt "%s._reg.%s = (%a*) &%s" inst v.var_id |
|
140 |
(fun fmt v -> |
|
141 |
pp_c_type "" fmt (Types.array_base_type v.var_type)) |
|
142 |
v v.var_id)) |
|
143 |
array_mem |
|
144 |
(pp_print_list ~pp_open_box:pp_open_vbox0 |
|
145 |
~pp_sep:(pp_print_endcut ";\\") (fun fmt (i', m') -> |
|
146 |
let path = sprintf "%s ## _%s" inst i' in |
|
147 |
fprintf fmt "%a;\\@,%s.%s = &%s" print_static_link_instance |
|
148 |
(path, m') inst i' path)) |
|
149 |
m.minstances |
|
150 |
|
|
151 |
let print_static_alloc_macro fmt (m, attr, inst) = |
|
152 |
fprintf fmt |
|
153 |
"@[<v>@[<v 2>#define %a(%s, %a%s)\\@,%a(%s, %a%s);\\@,%a(%s);@]@]" |
|
154 |
pp_machine_static_alloc_name m.mname.node_id attr |
|
155 |
(pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma |
|
156 |
(pp_c_var_read m)) |
|
157 |
m.mstatic inst pp_machine_static_declare_name m.mname.node_id attr |
|
158 |
(pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma |
|
159 |
(pp_c_var_read m)) |
|
160 |
m.mstatic inst pp_machine_static_link_name m.mname.node_id inst |
|
161 |
|
|
162 |
(* TODO: ACSL we do multiple things: - provide the semantics of the node as |
|
163 |
a predicate: function step and reset are associated to ACSL predicate - |
|
164 |
the node is associated to a refinement contract, wrt its ACSL sem - if |
|
165 |
the node is a regular node associated to a contract, print the contract |
|
166 |
as function contract. - do not print anything if this is a contract node *) |
|
167 |
let print_machine_alloc_decl fmt m = |
|
168 |
Mod.print_machine_decl_prefix fmt m; |
|
169 |
if not (fst (get_stateless_status m)) then |
|
170 |
if !Options.static_mem then |
|
171 |
(* Static allocation *) |
|
172 |
let macro = m, mk_attribute m, mk_instance m in |
|
173 |
fprintf fmt "%a@,%a@,%a" print_static_declare_macro macro |
|
174 |
print_static_link_macro macro print_static_alloc_macro macro |
|
175 |
else |
|
176 |
(* Dynamic allocation *) |
|
177 |
fprintf fmt "extern %a;@,extern %a" print_alloc_prototype |
|
178 |
(m.mname.node_id, m.mstatic) |
|
179 |
print_dealloc_prototype m.mname.node_id |
|
180 |
|
|
181 |
let print_machine_struct_top_decl_from_header fmt tdecl = |
|
182 |
let inode = imported_node_of_top tdecl in |
|
183 |
if not inode.nodei_stateless then |
|
184 |
(* Declare struct *) |
|
185 |
fprintf fmt "%a;" (pp_machine_memtype_name ~ghost:false) inode.nodei_id |
|
186 |
|
|
187 |
let print_stateless_C_prototype fmt (name, inputs, outputs) = |
|
188 |
let output = match outputs with [ hd ] -> hd | _ -> assert false in |
|
189 |
fprintf fmt "%a %s %a" |
|
190 |
(pp_basic_c_type ~pp_c_basic_type_desc ~var_opt:None) |
|
191 |
output.var_type name |
|
192 |
(pp_print_parenthesized pp_c_decl_input_var) |
|
193 |
inputs |
|
194 |
|
|
195 |
let print_machine_decl_top_decl_from_header fmt tdecl = |
|
196 |
let inode = imported_node_of_top tdecl in |
|
197 |
(*Mod.print_machine_decl_prefix fmt m;*) |
|
198 |
let prototype = inode.nodei_id, inode.nodei_inputs, inode.nodei_outputs in |
|
199 |
if inode.nodei_prototype = Some "C" then |
|
200 |
if inode.nodei_stateless then |
|
201 |
fprintf fmt "extern %a;" print_stateless_C_prototype prototype |
|
202 |
else ( |
|
203 |
(* TODO: raise proper error *) |
|
204 |
Format.eprintf |
|
205 |
"internal error: print_machine_decl_top_decl_from_header"; |
|
206 |
assert false) |
|
207 |
else if inode.nodei_stateless then |
|
208 |
fprintf fmt "extern %a;" Protos.print_stateless_prototype prototype |
|
209 |
else |
|
210 |
let static_inputs = |
|
211 |
List.filter (fun v -> v.var_dec_const) inode.nodei_inputs |
|
212 |
in |
|
213 |
let used name = |
|
214 |
List.exists |
|
215 |
(fun v -> v.var_id = name) |
|
216 |
(inode.nodei_inputs @ inode.nodei_outputs) |
|
217 |
in |
|
218 |
let self = mk_new_name used "self" in |
|
219 |
let mem = mk_new_name used "mem" in |
|
220 |
let static_prototype = inode.nodei_id, static_inputs in |
|
221 |
fprintf fmt "extern %a;@,extern %a;@,extern %a;@,extern %a;@,extern %a;" |
|
222 |
(Protos.print_set_reset_prototype self mem) |
|
223 |
static_prototype |
|
224 |
(Protos.print_clear_reset_prototype self mem) |
|
225 |
static_prototype |
|
226 |
(Protos.print_init_prototype self) |
|
227 |
static_prototype |
|
228 |
(Protos.print_clear_prototype self) |
|
229 |
static_prototype |
|
230 |
(Protos.print_step_prototype self mem) |
|
231 |
prototype |
|
232 |
|
|
233 |
let print_const_top_decl fmt tdecl = |
|
234 |
let cdecl = const_of_top tdecl in |
|
235 |
fprintf fmt "extern %a;" (pp_c_type cdecl.const_id) |
|
236 |
(if |
|
237 |
!Options.mpfr |
|
238 |
&& Types.(is_real_type (array_base_type cdecl.const_type)) |
|
239 |
then Types.dynamic_type cdecl.const_type |
|
240 |
else cdecl.const_type) |
|
241 |
|
|
242 |
let rec pp_c_type_decl filename cpt var fmt tdecl = |
|
243 |
match tdecl with |
|
244 |
| Tydec_any -> |
|
245 |
assert false |
|
246 |
| Tydec_int -> |
|
247 |
fprintf fmt "int %s" var |
|
248 |
| Tydec_real when !Options.mpfr -> |
|
249 |
fprintf fmt "%s %s" Mpfr.mpfr_t var |
|
250 |
| Tydec_real -> |
|
251 |
fprintf fmt "double %s" var |
|
252 |
(* | Tydec_float -> fprintf fmt "float %s" var *) |
|
253 |
| Tydec_bool -> |
|
254 |
fprintf fmt "_Bool %s" var |
|
255 |
| Tydec_clock ty -> |
|
256 |
pp_c_type_decl filename cpt var fmt ty |
|
257 |
| Tydec_const c -> |
|
258 |
fprintf fmt "%s %s" c var |
|
259 |
| Tydec_array (d, ty) -> |
|
260 |
fprintf fmt "%a[%a]" |
|
261 |
(pp_c_type_decl filename cpt var) |
|
262 |
ty pp_c_dimension d |
|
263 |
| Tydec_enum tl -> |
|
264 |
incr cpt; |
|
265 |
fprintf fmt "enum _enum_%s_%d %a %s" |
|
266 |
(protect_filename filename) |
|
267 |
!cpt |
|
268 |
(pp_print_braced pp_print_string) |
|
269 |
tl var |
|
270 |
| Tydec_struct fl -> |
|
271 |
incr cpt; |
|
272 |
fprintf fmt "struct _struct_%s_%d %a %s" |
|
273 |
(protect_filename filename) |
|
274 |
!cpt |
|
275 |
(pp_print_braced ~pp_sep:pp_print_semicolon (fun fmt (label, tdesc) -> |
|
276 |
pp_c_type_decl filename cpt label fmt tdesc)) |
|
277 |
fl var |
|
278 |
|
|
279 |
(* let print_type_definitions fmt filename = |
|
280 |
* let cpt_type = ref 0 in |
|
281 |
* Hashtbl.iter (fun typ decl -> |
|
282 |
* match typ with |
|
283 |
* | Tydec_const var -> |
|
284 |
* begin match decl.top_decl_desc with |
|
285 |
* | TypeDef tdef -> |
|
286 |
* fprintf fmt "typedef %a;@.@." |
|
287 |
* (pp_c_type_decl filename cpt_type var) tdef.tydef_desc |
|
288 |
* | _ -> assert false |
|
289 |
* end |
|
290 |
* | _ -> ()) type_table *) |
|
291 |
|
|
292 |
let reset_type_definitions, print_type_definition_top_decl_from_header = |
|
293 |
let cpt_type = ref 0 in |
|
294 |
( (fun () -> cpt_type := 0), |
|
295 |
fun filename fmt tdecl -> |
|
296 |
let typ = typedef_of_top tdecl in |
|
297 |
fprintf fmt "typedef %a;" |
|
298 |
(pp_c_type_decl filename cpt_type typ.tydef_id) |
|
299 |
typ.tydef_desc ) |
|
300 |
|
|
301 |
(********************************************************************************************) |
|
302 |
(* MAIN Header Printing functions *) |
|
303 |
(********************************************************************************************) |
|
304 |
|
|
305 |
let print_alloc_header header_fmt basename _prog machines dependencies spec |
|
306 |
= |
|
307 |
(* Include once: start *) |
|
308 |
let baseNAME = file_to_module_name basename in |
|
309 |
fprintf header_fmt |
|
310 |
"@[<v>%a@,\ |
|
311 |
#ifndef _%s_alloc@,\ |
|
312 |
#define _%s_alloc@,\ |
|
313 |
@,\ |
|
314 |
/* Import header from %s */@,\ |
|
315 |
%a@,\ |
|
316 |
@,\ |
|
317 |
%a%a%a#endif@]" |
|
318 |
(* Print the svn version number and the supported C standard (C90 or |
|
319 |
C99) *) |
|
320 |
pp_print_version () baseNAME baseNAME (* Import the header *) basename |
|
321 |
print_import_prototype |
|
322 |
{ |
|
323 |
local = true; |
|
324 |
name = basename; |
|
325 |
content = []; |
|
326 |
is_stateful = true (* assuming it is staful *); |
|
327 |
} |
|
328 |
(* Print dependencies *) |
|
329 |
(pp_print_list ~pp_open_box:pp_open_vbox0 |
|
330 |
~pp_prologue:(pp_print_endcut "/* Import dependencies */") |
|
331 |
print_import_alloc_prototype ~pp_epilogue:pp_print_cutcut) |
|
332 |
dependencies |
|
333 |
(* Print the struct definitions of all machines. *) |
|
334 |
(pp_print_list ~pp_open_box:pp_open_vbox0 |
|
335 |
~pp_prologue:(pp_print_endcut "/* Struct definitions */") |
|
336 |
~pp_sep:pp_print_cutcut print_machine_struct |
|
337 |
~pp_epilogue:pp_print_cutcut) |
|
338 |
machines |
|
339 |
(* Print the prototypes of all machines *) |
|
340 |
(pp_print_list ~pp_open_box:pp_open_vbox0 |
|
341 |
~pp_prologue: |
|
342 |
(pp_print_endcut "/* Node allocation function/macro prototypes */") |
|
343 |
~pp_sep:pp_print_cutcut print_machine_alloc_decl |
|
344 |
~pp_epilogue:pp_print_cutcut) |
|
345 |
machines |
|
346 |
(* Include once: end *) |
|
347 |
|
|
348 |
(* Function called when compiling a lusi file and generating the associated |
|
349 |
C header. *) |
|
350 |
let print_header_from_header header_fmt basename header = |
|
351 |
(* Include once: start *) |
|
352 |
let baseNAME = file_to_module_name basename in |
|
353 |
let types = get_typedefs header in |
|
354 |
let consts = get_consts header in |
|
355 |
let nodes = get_imported_nodes header in |
|
356 |
let dependencies = get_dependencies header in |
|
357 |
reset_type_definitions (); |
|
358 |
fprintf header_fmt |
|
359 |
"@[<v>%a@,\ |
|
360 |
#ifndef _%s@,\ |
|
361 |
#define _%s@,\ |
|
362 |
@,\ |
|
363 |
/* Import standard library */@,\ |
|
364 |
%a@,\ |
|
365 |
@,\ |
|
366 |
%a%a%a%a%a%a#endif@]@." |
|
367 |
(* Print the version number and the supported C standard (C90 or C99) *) |
|
368 |
pp_print_version () baseNAME baseNAME |
|
369 |
(* imports standard library definitions (arrow) *) |
|
370 |
print_import_standard () |
|
371 |
(* imports dependencies *) |
|
372 |
(pp_print_list ~pp_open_box:pp_open_vbox0 |
|
373 |
~pp_prologue:(pp_print_endcut "/* Import dependencies */") |
|
374 |
(fun fmt dep -> |
|
375 |
let local, name = dependency_of_top dep in |
|
376 |
print_import_prototype fmt |
|
377 |
{ |
|
378 |
local; |
|
379 |
name; |
|
380 |
content = []; |
|
381 |
is_stateful = true (* assuming it is stateful *); |
|
382 |
}) |
|
383 |
~pp_epilogue:pp_print_cutcut) |
|
384 |
dependencies |
|
385 |
(* Print the type definitions from the type table *) |
|
386 |
(pp_print_list ~pp_open_box:pp_open_vbox0 |
|
387 |
~pp_prologue:(pp_print_endcut "/* Types definitions */") |
|
388 |
(print_type_definition_top_decl_from_header basename) |
|
389 |
~pp_epilogue:pp_print_cutcut) |
|
390 |
types |
|
391 |
(* Print the global constant declarations. *) |
|
392 |
(pp_print_list ~pp_open_box:pp_open_vbox0 |
|
393 |
~pp_prologue: |
|
394 |
(pp_print_endcut |
|
395 |
"/* Global constants (declarations, definitions are in C file) \ |
|
396 |
*/") |
|
397 |
print_const_top_decl ~pp_epilogue:pp_print_cutcut) |
|
398 |
consts |
|
399 |
(* MPFR *) |
|
400 |
(if !Options.mpfr then fun fmt () -> |
|
401 |
fprintf fmt |
|
402 |
"/* Global initialization declaration */@,\ |
|
403 |
extern %a;@,\ |
|
404 |
@,\ |
|
405 |
/* Global clear declaration */@,\ |
|
406 |
extern %a;@,\ |
|
407 |
@," |
|
408 |
print_global_init_prototype baseNAME print_global_clear_prototype |
|
409 |
baseNAME |
|
410 |
else pp_print_nothing) |
|
411 |
() |
|
412 |
(* Print the struct declarations of all machines. *) |
|
413 |
(pp_print_list ~pp_open_box:pp_open_vbox0 |
|
414 |
~pp_prologue:(pp_print_endcut "/* Struct declarations */") |
|
415 |
print_machine_struct_top_decl_from_header |
|
416 |
~pp_epilogue:pp_print_cutcut) |
|
417 |
nodes |
|
418 |
(* Print the prototypes of all machines *) |
|
419 |
(pp_print_list ~pp_open_box:pp_open_vbox0 |
|
420 |
~pp_prologue:(pp_print_endcut "/* Nodes declarations */") |
|
421 |
~pp_sep:pp_print_cutcut print_machine_decl_top_decl_from_header |
|
422 |
~pp_epilogue:pp_print_cutcut) |
|
423 |
nodes |
|
424 |
end |
|
480 | 425 |
(* Local Variables: *) |
481 | 426 |
(* compile-command:"make -C ../../.." *) |
482 | 427 |
(* End: *) |
Also available in: Unified diff
reformatting