Revision 71999483
Added by Pierre-Loïc Garoche about 4 years ago
| src/backends/C/c_backend.ml | ||
|---|---|---|
| 29 | 29 |
let gen_files funs basename prog machines dependencies = |
| 30 | 30 |
let destname = !Options.dest_dir ^ "/" ^ basename in |
| 31 | 31 |
|
| 32 |
let print_header, print_lib_c, print_main_c, print_makefile(* , print_cmake *) = funs in |
|
| 32 |
let print_header, print_lib_c, print_main_c, print_makefile, preprocess (* , print_cmake *) = funs in
|
|
| 33 | 33 |
|
| 34 |
let machines, spec = preprocess machines in |
|
| 35 |
|
|
| 34 | 36 |
(* Generating H file *) |
| 35 | 37 |
let alloc_header_file = destname ^ "_alloc.h" in (* Could be changed *) |
| 36 | 38 |
let header_out = open_out alloc_header_file in |
| 37 | 39 |
let header_fmt = formatter_of_out_channel header_out in |
| 38 |
print_header header_fmt basename prog machines dependencies; |
|
| 40 |
print_header header_fmt basename prog machines dependencies spec;
|
|
| 39 | 41 |
close_out header_out; |
| 40 | 42 |
|
| 41 | 43 |
(* Generating Lib C file *) |
| ... | ... | |
| 146 | 148 |
Header.print_alloc_header, |
| 147 | 149 |
Source.print_lib_c, |
| 148 | 150 |
SourceMain.print_main_c, |
| 149 |
Makefile.print_makefile(* , *) |
|
| 151 |
Makefile.print_makefile, |
|
| 152 |
(fun m -> m, []) |
|
| 150 | 153 |
(* CMakefile.print_makefile *) |
| 151 | 154 |
in |
| 152 | 155 |
gen_files funs basename prog machines dependencies |
| ... | ... | |
| 169 | 172 |
Header.print_alloc_header, |
| 170 | 173 |
Source.print_lib_c, |
| 171 | 174 |
SourceMain.print_main_c, |
| 172 |
Makefile.print_makefile(* , *) |
|
| 175 |
Makefile.print_makefile, |
|
| 176 |
C_backend_spec.preprocess_acsl |
|
| 173 | 177 |
(* CMakefile.print_makefile *) |
| 174 | 178 |
in |
| 175 | 179 |
gen_files funs basename prog machines dependencies |
| src/backends/C/c_backend_common.ml | ||
|---|---|---|
| 369 | 369 |
else |
| 370 | 370 |
() |
| 371 | 371 |
|
| 372 |
let print_machine_struct fmt m = |
|
| 372 |
let print_machine_struct machines fmt m =
|
|
| 373 | 373 |
if fst (get_stateless_status m) then |
| 374 | 374 |
begin |
| 375 | 375 |
end |
| src/backends/C/c_backend_header.ml | ||
|---|---|---|
| 159 | 159 |
pp_machine_static_link_name m.mname.node_id |
| 160 | 160 |
inst |
| 161 | 161 |
|
| 162 |
let print_machine_decl fmt m = |
|
| 163 |
begin |
|
| 164 |
Mod.print_machine_decl_prefix fmt m; |
|
| 165 |
if fst (get_stateless_status m) then |
|
| 166 |
begin |
|
| 167 |
fprintf fmt "extern %a;@.@." |
|
| 168 |
print_stateless_prototype |
|
| 169 |
(m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs) |
|
| 170 |
end |
|
| 171 |
else |
|
| 172 |
begin |
|
| 173 |
(* Static allocation *) |
|
| 174 |
if !Options.static_mem |
|
| 175 |
then |
|
| 176 |
begin |
|
| 177 |
let inst = mk_instance m in |
|
| 178 |
let attr = mk_attribute m in |
|
| 179 |
fprintf fmt "%a@.%a@.%a@." |
|
| 180 |
print_static_declare_macro (m, attr, inst) |
|
| 181 |
print_static_link_macro (m, attr, inst) |
|
| 182 |
print_static_alloc_macro (m, attr, inst) |
|
| 183 |
end |
|
| 184 |
else |
|
| 185 |
begin |
|
| 186 |
(* Dynamic allocation *) |
|
| 187 |
fprintf fmt "extern %a;@.@." |
|
| 188 |
print_alloc_prototype (m.mname.node_id, m.mstatic); |
|
| 189 |
|
|
| 190 |
fprintf fmt "extern %a;@.@." |
|
| 191 |
print_dealloc_prototype m.mname.node_id; |
|
| 192 |
end; |
|
| 193 |
let self = mk_self m in |
|
| 194 |
fprintf fmt "extern %a;@.@." |
|
| 195 |
(print_reset_prototype self) (m.mname.node_id, m.mstatic); |
|
| 196 |
|
|
| 197 |
fprintf fmt "extern %a;@.@." |
|
| 198 |
(print_step_prototype self) |
|
| 199 |
(m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs); |
|
| 200 |
|
|
| 201 |
if !Options.mpfr then |
|
| 202 |
begin |
|
| 203 |
fprintf fmt "extern %a;@.@." |
|
| 204 |
(print_init_prototype self) (m.mname.node_id, m.mstatic); |
|
| 205 |
|
|
| 206 |
fprintf fmt "extern %a;@.@." |
|
| 207 |
(print_clear_prototype self) (m.mname.node_id, m.mstatic); |
|
| 208 |
end |
|
| 209 |
end |
|
| 210 |
end |
|
| 211 |
|
|
| 212 |
let print_machine_alloc_decl fmt m = |
|
| 162 |
(* TODO: ACSL |
|
| 163 |
we do multiple things: |
|
| 164 |
- provide the semantics of the node as a predicate: function step and reset are associated to ACSL predicate |
|
| 165 |
- the node is associated to a refinement contract, wrt its ACSL sem |
|
| 166 |
- if the node is a regular node associated to a contract, print the contract as function contract. |
|
| 167 |
- do not print anything if this is a contract node |
|
| 168 |
*) |
|
| 169 |
let print_machine_alloc_decl machines fmt m = |
|
| 213 | 170 |
Mod.print_machine_decl_prefix fmt m; |
| 214 | 171 |
if fst (get_stateless_status m) then |
| 215 | 172 |
begin |
| ... | ... | |
| 332 | 289 |
(********************************************************************************************) |
| 333 | 290 |
(* MAIN Header Printing functions *) |
| 334 | 291 |
(********************************************************************************************) |
| 292 |
(* Seems not used |
|
| 293 |
|
|
| 335 | 294 |
let print_header header_fmt basename prog machines dependencies = |
| 336 | 295 |
(* Include once: start *) |
| 337 | 296 |
let baseNAME = file_to_module_name basename in |
| ... | ... | |
| 369 | 328 |
end; |
| 370 | 329 |
(* Print the struct declarations of all machines. *) |
| 371 | 330 |
fprintf header_fmt "/* Structs declarations */@."; |
| 372 |
List.iter (print_machine_struct header_fmt) machines; |
|
| 331 |
List.iter (print_machine_struct machines header_fmt) machines;
|
|
| 373 | 332 |
pp_print_newline header_fmt (); |
| 374 | 333 |
(* Print the prototypes of all machines *) |
| 375 | 334 |
fprintf header_fmt "/* Nodes declarations */@."; |
| ... | ... | |
| 379 | 338 |
fprintf header_fmt "#endif@."; |
| 380 | 339 |
pp_print_newline header_fmt () |
| 381 | 340 |
end |
| 382 |
|
|
| 383 |
let print_alloc_header header_fmt basename prog machines dependencies = |
|
| 341 |
*) |
|
| 342 |
let print_alloc_header header_fmt basename prog machines dependencies spec =
|
|
| 384 | 343 |
(* Include once: start *) |
| 385 | 344 |
let baseNAME = file_to_module_name basename in |
| 386 | 345 |
begin |
| ... | ... | |
| 399 | 358 |
fprintf header_fmt "@]@."; |
| 400 | 359 |
(* Print the struct definitions of all machines. *) |
| 401 | 360 |
fprintf header_fmt "/* Struct definitions */@."; |
| 402 |
List.iter (print_machine_struct header_fmt) machines; |
|
| 361 |
List.iter (print_machine_struct machines header_fmt) machines;
|
|
| 403 | 362 |
pp_print_newline header_fmt (); |
| 363 |
fprintf header_fmt "/* Specification */@.%a@." C_backend_spec.pp_acsl_preamble spec; |
|
| 404 | 364 |
(* Print the prototypes of all machines *) |
| 405 | 365 |
fprintf header_fmt "/* Node allocation function/macro prototypes */@."; |
| 406 |
List.iter (print_machine_alloc_decl header_fmt) machines; |
|
| 366 |
List.iter (print_machine_alloc_decl machines header_fmt) machines;
|
|
| 407 | 367 |
pp_print_newline header_fmt (); |
| 408 | 368 |
(* Include once: end *) |
| 409 | 369 |
fprintf header_fmt "#endif@."; |
| src/backends/C/c_backend_spec.ml | ||
|---|---|---|
| 129 | 129 |
|
| 130 | 130 |
*) |
| 131 | 131 |
|
| 132 |
(* TODO ACSL |
|
| 133 |
mspec are function body annotations, sush as loop invariants, acsl asserts ... *) |
|
| 134 |
let pp_mspec fmt s = () |
|
| 135 |
|
|
| 136 |
(* TODO ACSL |
|
| 137 |
Return updates machines (eg with local annotations) and acsl preamble *) |
|
| 138 |
let preprocess_acsl machines = machines, [] |
|
| 139 |
|
|
| 140 |
(* TODO: This preamble shall be a list of types, axiomatics, predicates, theorems *) |
|
| 141 |
let pp_acsl_preamble fmt preamble = |
|
| 142 |
Format.fprintf fmt ""; |
|
| 143 |
() |
|
| 132 | 144 |
(**************************************************************************) |
| 133 | 145 |
(* MAKEFILE *) |
| 134 | 146 |
(**************************************************************************) |
| src/backends/C/c_backend_src.ml | ||
|---|---|---|
| 370 | 370 |
fprintf fmt "@[<v 2>switch(%a) {@,%a@,}@]"
|
| 371 | 371 |
(pp_c_val m self (pp_c_var_read m)) g |
| 372 | 372 |
(Utils.fprintf_list ~sep:"@," (pp_machine_branch dependencies m self)) hl |
| 373 |
| MSpec s -> fprintf fmt "@[/*@@ %s */@]@ " s |
|
| 373 | 374 |
| MComment s -> |
| 374 | 375 |
fprintf fmt "/*%s*/@ " s |
| 375 | 376 |
|
| ... | ... | |
| 633 | 634 |
(* dependencies initialization *) |
| 634 | 635 |
(Utils.fprintf_list ~sep:"@," print_import_clear) dependencies |
| 635 | 636 |
|
| 637 |
(* TODO: ACSL |
|
| 638 |
- a contract machine shall not be directly printed in the C source |
|
| 639 |
- but a regular machine associated to a contract machine shall integrate the associated statements, updating its memories, at the end of the function body. |
|
| 640 |
- last one may print intermediate comment/acsl if/when they are present in the sequence of instruction |
|
| 641 |
*) |
|
| 636 | 642 |
let print_machine dependencies fmt m = |
| 637 | 643 |
if fst (get_stateless_status m) then |
| 638 | 644 |
begin |
| ... | ... | |
| 729 | 735 |
(* Print the struct definitions of all machines. *) |
| 730 | 736 |
fprintf source_fmt "/* Struct definitions */@."; |
| 731 | 737 |
fprintf source_fmt "@[<v>"; |
| 732 |
List.iter (print_machine_struct source_fmt) machines; |
|
| 738 |
List.iter (print_machine_struct machines source_fmt) machines;
|
|
| 733 | 739 |
fprintf source_fmt "@]@."; |
| 734 | 740 |
pp_print_newline source_fmt (); |
| 735 | 741 |
(* Print nodes one by one (in the previous order) *) |
Also available in: Unified diff
Cleaning C backend - removing unused functiions
Preparing for coming ACSL