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