Revision 13507742
Added by Pierre-Loïc Garoche about 6 years ago
| src/backends/backends.ml | ||
|---|---|---|
| 1 | 1 |
(* Backend-specific options *) |
| 2 | 2 |
let join_guards = ref true |
| 3 | 3 |
|
| 4 |
let setup s =
|
|
| 5 |
match s with
|
|
| 6 |
| "emf" ->
|
|
| 7 |
join_guards := true; (* guards should not be joined, in order to have only
|
|
| 8 |
if c then x = e1 else x = e2 to ease
|
|
| 9 |
reconstruction of flows. *)
|
|
| 10 |
Options.optimization := 0; (* Optimization=0 prevents expression
|
|
| 11 |
elimination. This simplifies largely the
|
|
| 12 |
association of lustre expression to
|
|
| 13 |
instructions *)
|
|
| 4 |
let setup () =
|
|
| 5 |
match !Options.output with
|
|
| 6 |
(* | "emf" -> *)
|
|
| 7 |
(* join_guards := true; (\* guards should not be joined, in order to have only *)
|
|
| 8 |
(* if c then x = e1 else x = e2 to ease *)
|
|
| 9 |
(* reconstruction of flows. *\) *)
|
|
| 10 |
(* Options.optimization := 0; (\* Optimization=0 prevents expression *)
|
|
| 11 |
(* elimination. This simplifies largely the *)
|
|
| 12 |
(* association of lustre expression to *)
|
|
| 13 |
(* instructions *\) *)
|
|
| 14 | 14 |
| _ -> () |
| 15 | 15 |
|
| 16 |
let is_functional () = |
|
| 17 |
match !Options.output with |
|
| 18 |
| "horn" | "lustre" | "acsl" | "emf" -> true |
|
| 19 |
| _ -> false |
|
| 20 |
|
|
| 21 |
|
|
| 16 | 22 |
(* Local Variables: *) |
| 17 | 23 |
(* compile-command: "make -k -C .." *) |
| 18 | 24 |
(* End: *) |
| src/corelang.ml | ||
|---|---|---|
| 1065 | 1065 |
let copy_prog top_list = |
| 1066 | 1066 |
List.map copy_top top_list |
| 1067 | 1067 |
|
| 1068 |
let functional_backend () = |
|
| 1069 |
match !Options.output with |
|
| 1070 |
| "horn" | "lustre" | "acsl" -> true |
|
| 1071 |
| _ -> false |
|
| 1072 |
|
|
| 1073 | 1068 |
(* Local Variables: *) |
| 1074 | 1069 |
(* compile-command:"make -C .." *) |
| 1075 | 1070 |
(* End: *) |
| src/corelang.mli | ||
|---|---|---|
| 144 | 144 |
val update_expr_annot: ident -> expr -> expr_annot -> expr |
| 145 | 145 |
(* val mkpredef_call: Location.t -> ident -> eexpr list -> eexpr*) |
| 146 | 146 |
|
| 147 |
val functional_backend: unit -> bool |
|
| 148 | 147 |
(* Local Variables: *) |
| 149 | 148 |
(* compile-command:"make -C .." *) |
| 150 | 149 |
(* End: *) |
| src/machine_code.ml | ||
|---|---|---|
| 602 | 602 |
to be declared for each assert *) |
| 603 | 603 |
let new_locals, assert_instrs, nd_node_asserts = |
| 604 | 604 |
let exprl = List.map (fun assert_ -> assert_.assert_expr ) nd.node_asserts in |
| 605 |
if Corelang.functional_backend () then
|
|
| 605 |
if Backends.is_functional () then
|
|
| 606 | 606 |
[], [], exprl |
| 607 | 607 |
else (* Each assert(e) is associated to a fresh variable v and declared as |
| 608 | 608 |
v=e; assert (v); *) |
| src/main_lustre_compiler.ml | ||
|---|---|---|
| 262 | 262 |
Log.report ~level:3 (fun fmt -> fprintf fmt ".. generated machines (unoptimized):@ %a@ "Machine_code.pp_machines machine_code); |
| 263 | 263 |
|
| 264 | 264 |
(* Optimize machine code *) |
| 265 |
let machine_code = |
|
| 266 |
if !Options.optimization >= 4 (* && !Options.output <> "horn" *) then |
|
| 267 |
begin |
|
| 268 |
Log.report ~level:1 |
|
| 269 |
(fun fmt -> fprintf fmt ".. machines optimization: sub-expression elimination@,"); |
|
| 270 |
let machine_code = Optimize_machine.machines_cse machine_code in |
|
| 271 |
Log.report ~level:3 (fun fmt -> fprintf fmt ".. generated machines (sub-expr elim):@ %a@ "Machine_code.pp_machines machine_code); |
|
| 272 |
machine_code |
|
| 273 |
end |
|
| 274 |
else |
|
| 275 |
machine_code |
|
| 276 |
in |
|
| 277 |
(* Optimize machine code *) |
|
| 278 |
let machine_code, removed_table = |
|
| 279 |
if !Options.optimization >= 2 (*&& !Options.output <> "horn"*) then |
|
| 280 |
begin |
|
| 281 |
Log.report ~level:1 (fun fmt -> fprintf fmt |
|
| 282 |
".. machines optimization: const. inlining (partial eval. with const)@,"); |
|
| 283 |
let machine_code, removed_table = Optimize_machine.machines_unfold (Corelang.get_consts prog) node_schs machine_code in |
|
| 284 |
Log.report ~level:3 (fun fmt -> fprintf fmt "\t@[Eliminated constants: @[%a@]@]@ " |
|
| 285 |
(pp_imap Optimize_machine.pp_elim) removed_table); |
|
| 286 |
Log.report ~level:3 (fun fmt -> fprintf fmt ".. generated machines (const inlining):@ %a@ "Machine_code.pp_machines machine_code); |
|
| 287 |
machine_code, removed_table |
|
| 288 |
end |
|
| 289 |
else |
|
| 290 |
machine_code, IMap.empty |
|
| 291 |
in |
|
| 292 |
(* Optimize machine code *) |
|
| 293 |
let machine_code = |
|
| 294 |
if !Options.optimization >= 3 && not (Corelang.functional_backend ()) then |
|
| 295 |
begin |
|
| 296 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines optimization: minimize stack usage by reusing variables@,"); |
|
| 297 |
let node_schs = Scheduling.remove_prog_inlined_locals removed_table node_schs in |
|
| 298 |
let reuse_tables = Scheduling.compute_prog_reuse_table node_schs in |
|
| 299 |
Optimize_machine.machines_fusion (Optimize_machine.machines_reuse_variables machine_code reuse_tables) |
|
| 300 |
end |
|
| 301 |
else |
|
| 302 |
machine_code |
|
| 303 |
in |
|
| 304 |
|
|
| 305 |
(* Salsa optimize machine code *) |
|
| 306 |
(* |
|
| 307 |
let machine_code = |
|
| 308 |
if !Options.salsa_enabled then |
|
| 309 |
begin |
|
| 310 |
check_main (); |
|
| 311 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. salsa machines optimization: optimizing floating-point accuracy with Salsa@,"); |
|
| 312 |
(* Selecting float constants for Salsa *) |
|
| 313 |
let constEnv = List.fold_left ( |
|
| 314 |
fun accu c_topdecl -> |
|
| 315 |
match c_topdecl.top_decl_desc with |
|
| 316 |
| Const c when Types.is_real_type c.const_type -> |
|
| 317 |
(c.const_id, c.const_value) :: accu |
|
| 318 |
| _ -> accu |
|
| 319 |
) [] (Corelang.get_consts prog) |
|
| 320 |
in |
|
| 321 |
List.map |
|
| 322 |
(Machine_salsa_opt.machine_t2machine_t_optimized_by_salsa constEnv) |
|
| 323 |
machine_code |
|
| 324 |
end |
|
| 325 |
else |
|
| 326 |
machine_code |
|
| 327 |
in |
|
| 328 |
Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@ " |
|
| 329 |
(Utils.fprintf_list ~sep:"@ " Machine_code.pp_machine) |
|
| 330 |
machine_code); |
|
| 331 |
*) |
|
| 332 |
machine_code |
|
| 265 |
Optimize_machine.optimize prog node_schs machine_code |
|
| 333 | 266 |
|
| 334 | 267 |
|
| 335 | 268 |
(* printing code *) |
| src/optimize_machine.ml | ||
|---|---|---|
| 567 | 567 |
let machines_fusion prog = |
| 568 | 568 |
List.map machine_fusion prog |
| 569 | 569 |
|
| 570 |
|
|
| 571 |
(*** Main function ***) |
|
| 572 |
|
|
| 573 |
let optimize prog node_schs machine_code = |
|
| 574 |
let machine_code = |
|
| 575 |
if !Options.optimization >= 4 (* && !Options.output <> "horn" *) then |
|
| 576 |
begin |
|
| 577 |
Log.report ~level:1 |
|
| 578 |
(fun fmt -> Format.fprintf fmt ".. machines optimization: sub-expression elimination@,"); |
|
| 579 |
let machine_code = machines_cse machine_code in |
|
| 580 |
Log.report ~level:3 (fun fmt -> Format.fprintf fmt ".. generated machines (sub-expr elim):@ %a@ "Machine_code.pp_machines machine_code); |
|
| 581 |
machine_code |
|
| 582 |
end |
|
| 583 |
else |
|
| 584 |
machine_code |
|
| 585 |
in |
|
| 586 |
(* Optimize machine code *) |
|
| 587 |
let machine_code, removed_table = |
|
| 588 |
if !Options.optimization >= 2 && !Options.output <> "emf" (*&& !Options.output <> "horn"*) then |
|
| 589 |
begin |
|
| 590 |
Log.report ~level:1 (fun fmt -> Format.fprintf fmt |
|
| 591 |
".. machines optimization: const. inlining (partial eval. with const)@,"); |
|
| 592 |
let machine_code, removed_table = machines_unfold (Corelang.get_consts prog) node_schs machine_code in |
|
| 593 |
Log.report ~level:3 (fun fmt -> Format.fprintf fmt "\t@[Eliminated constants: @[%a@]@]@ " |
|
| 594 |
(pp_imap pp_elim) removed_table); |
|
| 595 |
Log.report ~level:3 (fun fmt -> Format.fprintf fmt ".. generated machines (const inlining):@ %a@ "Machine_code.pp_machines machine_code); |
|
| 596 |
machine_code, removed_table |
|
| 597 |
end |
|
| 598 |
else |
|
| 599 |
machine_code, IMap.empty |
|
| 600 |
in |
|
| 601 |
(* Optimize machine code *) |
|
| 602 |
let machine_code = |
|
| 603 |
if !Options.optimization >= 3 && not (Backends.is_functional ()) then |
|
| 604 |
begin |
|
| 605 |
Log.report ~level:1 (fun fmt -> Format.fprintf fmt ".. machines optimization: minimize stack usage by reusing variables@,"); |
|
| 606 |
let node_schs = Scheduling.remove_prog_inlined_locals removed_table node_schs in |
|
| 607 |
let reuse_tables = Scheduling.compute_prog_reuse_table node_schs in |
|
| 608 |
machines_fusion (machines_reuse_variables machine_code reuse_tables) |
|
| 609 |
end |
|
| 610 |
else |
|
| 611 |
machine_code |
|
| 612 |
in |
|
| 613 |
|
|
| 614 |
(* Salsa optimize machine code *) |
|
| 615 |
(* |
|
| 616 |
let machine_code = |
|
| 617 |
if !Options.salsa_enabled then |
|
| 618 |
begin |
|
| 619 |
check_main (); |
|
| 620 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. salsa machines optimization: optimizing floating-point accuracy with Salsa@,"); |
|
| 621 |
(* Selecting float constants for Salsa *) |
|
| 622 |
let constEnv = List.fold_left ( |
|
| 623 |
fun accu c_topdecl -> |
|
| 624 |
match c_topdecl.top_decl_desc with |
|
| 625 |
| Const c when Types.is_real_type c.const_type -> |
|
| 626 |
(c.const_id, c.const_value) :: accu |
|
| 627 |
| _ -> accu |
|
| 628 |
) [] (Corelang.get_consts prog) |
|
| 629 |
in |
|
| 630 |
List.map |
|
| 631 |
(Machine_salsa_opt.machine_t2machine_t_optimized_by_salsa constEnv) |
|
| 632 |
machine_code |
|
| 633 |
end |
|
| 634 |
else |
|
| 635 |
machine_code |
|
| 636 |
in |
|
| 637 |
Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@ " |
|
| 638 |
(Utils.fprintf_list ~sep:"@ " Machine_code.pp_machine) |
|
| 639 |
machine_code); |
|
| 640 |
*) |
|
| 641 |
|
|
| 642 |
|
|
| 643 |
machine_code |
|
| 644 |
|
|
| 645 |
|
|
| 570 | 646 |
(* Local Variables: *) |
| 571 | 647 |
(* compile-command:"make -C .." *) |
| 572 | 648 |
(* End: *) |
| src/options_management.ml | ||
|---|---|---|
| 73 | 73 |
|
| 74 | 74 |
let set_backend s = |
| 75 | 75 |
output := s; |
| 76 |
Backends.setup s
|
|
| 76 |
Backends.setup ()
|
|
| 77 | 77 |
|
| 78 | 78 |
let common_options = |
| 79 | 79 |
[ "-d", Arg.Set_string dest_dir, "uses the specified \x1b[4mdirectory\x1b[0m as root for generated/imported object and C files <default: .>"; |
Also available in: Unified diff
Refactored some code: optimization of machine