Revision 45f0f48d src/main_lustre_compiler.ml
src/main_lustre_compiler.ml | ||
---|---|---|
88 | 88 |
end |
89 | 89 |
|
90 | 90 |
|
91 |
let functional_backend () = |
|
92 |
match !Options.output with |
|
93 |
| "horn" | "lustre" | "acsl" -> true |
|
94 |
| _ -> false |
|
95 |
|
|
91 | 96 |
(* From prog to prog *) |
92 | 97 |
let stage1 prog dirname basename = |
93 | 98 |
(* Removing automata *) |
... | ... | |
122 | 127 |
|
123 | 128 |
(* Typing *) |
124 | 129 |
let computed_types_env = type_decls type_env prog in |
125 |
|
|
130 |
|
|
126 | 131 |
(* Clock calculus *) |
127 | 132 |
let computed_clocks_env = clock_decls clock_env prog in |
128 | 133 |
|
... | ... | |
148 | 153 |
in |
149 | 154 |
*) |
150 | 155 |
(* Delay calculus *) |
151 |
(* |
|
156 |
(* TO BE DONE LATER (Xavier)
|
|
152 | 157 |
if(!Options.delay_calculus) |
153 | 158 |
then |
154 | 159 |
begin |
... | ... | |
213 | 218 |
end |
214 | 219 |
else |
215 | 220 |
begin |
216 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. keeping FP numbers@,");
|
|
221 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. keeping floating-point numbers@,");
|
|
217 | 222 |
prog |
218 | 223 |
end in |
219 | 224 |
Log.report ~level:2 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog); |
... | ... | |
221 | 226 |
(* Checking array accesses *) |
222 | 227 |
if !Options.check then |
223 | 228 |
begin |
224 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. array access checks@,");
|
|
229 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. checking array accesses@,");
|
|
225 | 230 |
Access.check_prog prog; |
226 | 231 |
end; |
227 | 232 |
|
... | ... | |
257 | 262 |
let machine_code = |
258 | 263 |
if !Options.optimization >= 4 && !Options.output <> "horn" then |
259 | 264 |
begin |
260 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines optimization (phase 3)@,");
|
|
265 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines optimization: common sub-expression elimination@,");
|
|
261 | 266 |
Optimize_machine.machines_cse machine_code |
262 | 267 |
end |
263 | 268 |
else |
... | ... | |
267 | 272 |
let machine_code, removed_table = |
268 | 273 |
if !Options.optimization >= 2 && !Options.output <> "horn" then |
269 | 274 |
begin |
270 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines optimization (phase 1)@ ");
|
|
275 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines optimization: constants inlining@,");
|
|
271 | 276 |
Optimize_machine.machines_unfold (Corelang.get_consts prog) node_schs machine_code |
272 | 277 |
end |
273 | 278 |
else |
... | ... | |
277 | 282 |
let machine_code = |
278 | 283 |
if !Options.optimization >= 3 && !Options.output <> "horn" then |
279 | 284 |
begin |
280 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines optimization (phase 2)@ ");
|
|
285 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines optimization: minimize stack usage by reusing variables@,");
|
|
281 | 286 |
let node_schs = Scheduling.remove_prog_inlined_locals removed_table node_schs in |
282 | 287 |
let reuse_tables = Scheduling.compute_prog_reuse_table node_schs in |
283 | 288 |
Optimize_machine.machines_fusion (Optimize_machine.machines_reuse_variables machine_code reuse_tables) |
... | ... | |
292 | 297 |
if !Options.salsa_enabled then |
293 | 298 |
begin |
294 | 299 |
check_main (); |
295 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. salsa machines optimization (phase 3)@ ");
|
|
300 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. salsa machines optimization: optimizing floating-point accuracy with Salsa@,");
|
|
296 | 301 |
(* Selecting float constants for Salsa *) |
297 | 302 |
let constEnv = List.fold_left ( |
298 | 303 |
fun accu c_topdecl -> |
... | ... | |
348 | 353 |
let source_out = open_out source_file in |
349 | 354 |
let fmt = formatter_of_out_channel source_out in |
350 | 355 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. hornification@,"); |
351 |
Horn_backend.translate fmt basename prog machine_code;
|
|
356 |
Horn_backend.translate fmt basename prog (Machine_code.arrow_machine::machine_code);
|
|
352 | 357 |
(* Tracability file if option is activated *) |
353 | 358 |
if !Options.traces then ( |
354 |
let traces_file = destname ^ ".traces" in (* Could be changed *) |
|
359 |
let traces_file = destname ^ ".traces.xml" in (* Could be changed *)
|
|
355 | 360 |
let traces_out = open_out traces_file in |
356 | 361 |
let fmt = formatter_of_out_channel traces_out in |
357 | 362 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. tracing info@,"); |
358 |
Horn_backend.traces_file fmt basename prog machine_code; |
|
363 |
Horn_backend_traces.traces_file fmt basename prog machine_code;
|
|
359 | 364 |
) |
360 | 365 |
end |
361 | 366 |
| "lustre" -> |
Also available in: Unified diff