From 13507742ce19df91f98f0e7ea797dba704d05477 Mon Sep 17 00:00:00 2001
From: ploc <ploc@garoche.net>
Date: Wed, 12 Jul 2017 12:06:55 -0700
Subject: [PATCH] Refactored some code: optimization of machine
---
src/backends/backends.ml | 26 ++++++++-----
src/corelang.ml | 5 ---
src/corelang.mli | 1 -
src/machine_code.ml | 2 +-
src/main_lustre_compiler.ml | 69 +--------------------------------
src/optimize_machine.ml | 76 +++++++++++++++++++++++++++++++++++++
src/options_management.ml | 2 +-
7 files changed, 95 insertions(+), 86 deletions(-)
diff --git a/src/backends/backends.ml b/src/backends/backends.ml
index b4be7a02..1803b417 100644
--- a/src/backends/backends.ml
+++ b/src/backends/backends.ml
@@ -1,18 +1,24 @@
(* Backend-specific options *)
let join_guards = ref true
-let setup s =
- match s with
- | "emf" ->
- join_guards := true; (* guards should not be joined, in order to have only
- if c then x = e1 else x = e2 to ease
- reconstruction of flows. *)
- Options.optimization := 0; (* Optimization=0 prevents expression
- elimination. This simplifies largely the
- association of lustre expression to
- instructions *)
+let setup () =
+ match !Options.output with
+ (* | "emf" -> *)
+ (* join_guards := true; (\* guards should not be joined, in order to have only *)
+ (* if c then x = e1 else x = e2 to ease *)
+ (* reconstruction of flows. *\) *)
+ (* Options.optimization := 0; (\* Optimization=0 prevents expression *)
+ (* elimination. This simplifies largely the *)
+ (* association of lustre expression to *)
+ (* instructions *\) *)
| _ -> ()
+let is_functional () =
+ match !Options.output with
+ | "horn" | "lustre" | "acsl" | "emf" -> true
+ | _ -> false
+
+
(* Local Variables: *)
(* compile-command: "make -k -C .." *)
(* End: *)
diff --git a/src/corelang.ml b/src/corelang.ml
index 4b08dba8..00cd8f48 100755
--- a/src/corelang.ml
+++ b/src/corelang.ml
@@ -1065,11 +1065,6 @@ let copy_top top =
let copy_prog top_list =
List.map copy_top top_list
-let functional_backend () =
- match !Options.output with
- | "horn" | "lustre" | "acsl" -> true
- | _ -> false
-
(* Local Variables: *)
(* compile-command:"make -C .." *)
(* End: *)
diff --git a/src/corelang.mli b/src/corelang.mli
index eb8b7a48..73bef972 100755
--- a/src/corelang.mli
+++ b/src/corelang.mli
@@ -144,7 +144,6 @@ val extend_eexpr: (quantifier_type * var_decl list) list -> eexpr -> eexpr
val update_expr_annot: ident -> expr -> expr_annot -> expr
(* val mkpredef_call: Location.t -> ident -> eexpr list -> eexpr*)
-val functional_backend: unit -> bool
(* Local Variables: *)
(* compile-command:"make -C .." *)
(* End: *)
diff --git a/src/machine_code.ml b/src/machine_code.ml
index 85440e73..0e8a5305 100644
--- a/src/machine_code.ml
+++ b/src/machine_code.ml
@@ -602,7 +602,7 @@ let translate_decl nd sch =
to be declared for each assert *)
let new_locals, assert_instrs, nd_node_asserts =
let exprl = List.map (fun assert_ -> assert_.assert_expr ) nd.node_asserts in
- if Corelang.functional_backend () then
+ if Backends.is_functional () then
[], [], exprl
else (* Each assert(e) is associated to a fresh variable v and declared as
v=e; assert (v); *)
diff --git a/src/main_lustre_compiler.ml b/src/main_lustre_compiler.ml
index de44cabe..f9176183 100644
--- a/src/main_lustre_compiler.ml
+++ b/src/main_lustre_compiler.ml
@@ -262,74 +262,7 @@ let stage2 prog =
Log.report ~level:3 (fun fmt -> fprintf fmt ".. generated machines (unoptimized):@ %a@ "Machine_code.pp_machines machine_code);
(* Optimize machine code *)
- let machine_code =
- if !Options.optimization >= 4 (* && !Options.output <> "horn" *) then
- begin
- Log.report ~level:1
- (fun fmt -> fprintf fmt ".. machines optimization: sub-expression elimination@,");
- let machine_code = Optimize_machine.machines_cse machine_code in
- Log.report ~level:3 (fun fmt -> fprintf fmt ".. generated machines (sub-expr elim):@ %a@ "Machine_code.pp_machines machine_code);
- machine_code
- end
- else
- machine_code
- in
- (* Optimize machine code *)
- let machine_code, removed_table =
- if !Options.optimization >= 2 (*&& !Options.output <> "horn"*) then
- begin
- Log.report ~level:1 (fun fmt -> fprintf fmt
- ".. machines optimization: const. inlining (partial eval. with const)@,");
- let machine_code, removed_table = Optimize_machine.machines_unfold (Corelang.get_consts prog) node_schs machine_code in
- Log.report ~level:3 (fun fmt -> fprintf fmt "\t@[Eliminated constants: @[%a@]@]@ "
- (pp_imap Optimize_machine.pp_elim) removed_table);
- Log.report ~level:3 (fun fmt -> fprintf fmt ".. generated machines (const inlining):@ %a@ "Machine_code.pp_machines machine_code);
- machine_code, removed_table
- end
- else
- machine_code, IMap.empty
- in
- (* Optimize machine code *)
- let machine_code =
- if !Options.optimization >= 3 && not (Corelang.functional_backend ()) then
- begin
- Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines optimization: minimize stack usage by reusing variables@,");
- let node_schs = Scheduling.remove_prog_inlined_locals removed_table node_schs in
- let reuse_tables = Scheduling.compute_prog_reuse_table node_schs in
- Optimize_machine.machines_fusion (Optimize_machine.machines_reuse_variables machine_code reuse_tables)
- end
- else
- machine_code
- in
-
- (* Salsa optimize machine code *)
- (*
- let machine_code =
- if !Options.salsa_enabled then
- begin
- check_main ();
- Log.report ~level:1 (fun fmt -> fprintf fmt ".. salsa machines optimization: optimizing floating-point accuracy with Salsa@,");
- (* Selecting float constants for Salsa *)
- let constEnv = List.fold_left (
- fun accu c_topdecl ->
- match c_topdecl.top_decl_desc with
- | Const c when Types.is_real_type c.const_type ->
- (c.const_id, c.const_value) :: accu
- | _ -> accu
- ) [] (Corelang.get_consts prog)
- in
- List.map
- (Machine_salsa_opt.machine_t2machine_t_optimized_by_salsa constEnv)
- machine_code
- end
- else
- machine_code
- in
- Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@ "
- (Utils.fprintf_list ~sep:"@ " Machine_code.pp_machine)
- machine_code);
- *)
- machine_code
+ Optimize_machine.optimize prog node_schs machine_code
(* printing code *)
diff --git a/src/optimize_machine.ml b/src/optimize_machine.ml
index 9cd8c082..71a668c8 100644
--- a/src/optimize_machine.ml
+++ b/src/optimize_machine.ml
@@ -567,6 +567,82 @@ let rec machine_fusion m =
let machines_fusion prog =
List.map machine_fusion prog
+
+(*** Main function ***)
+
+let optimize prog node_schs machine_code =
+ let machine_code =
+ if !Options.optimization >= 4 (* && !Options.output <> "horn" *) then
+ begin
+ Log.report ~level:1
+ (fun fmt -> Format.fprintf fmt ".. machines optimization: sub-expression elimination@,");
+ let machine_code = machines_cse machine_code in
+ Log.report ~level:3 (fun fmt -> Format.fprintf fmt ".. generated machines (sub-expr elim):@ %a@ "Machine_code.pp_machines machine_code);
+ machine_code
+ end
+ else
+ machine_code
+ in
+ (* Optimize machine code *)
+ let machine_code, removed_table =
+ if !Options.optimization >= 2 && !Options.output <> "emf" (*&& !Options.output <> "horn"*) then
+ begin
+ Log.report ~level:1 (fun fmt -> Format.fprintf fmt
+ ".. machines optimization: const. inlining (partial eval. with const)@,");
+ let machine_code, removed_table = machines_unfold (Corelang.get_consts prog) node_schs machine_code in
+ Log.report ~level:3 (fun fmt -> Format.fprintf fmt "\t@[Eliminated constants: @[%a@]@]@ "
+ (pp_imap pp_elim) removed_table);
+ Log.report ~level:3 (fun fmt -> Format.fprintf fmt ".. generated machines (const inlining):@ %a@ "Machine_code.pp_machines machine_code);
+ machine_code, removed_table
+ end
+ else
+ machine_code, IMap.empty
+ in
+ (* Optimize machine code *)
+ let machine_code =
+ if !Options.optimization >= 3 && not (Backends.is_functional ()) then
+ begin
+ Log.report ~level:1 (fun fmt -> Format.fprintf fmt ".. machines optimization: minimize stack usage by reusing variables@,");
+ let node_schs = Scheduling.remove_prog_inlined_locals removed_table node_schs in
+ let reuse_tables = Scheduling.compute_prog_reuse_table node_schs in
+ machines_fusion (machines_reuse_variables machine_code reuse_tables)
+ end
+ else
+ machine_code
+ in
+
+ (* Salsa optimize machine code *)
+ (*
+ let machine_code =
+ if !Options.salsa_enabled then
+ begin
+ check_main ();
+ Log.report ~level:1 (fun fmt -> fprintf fmt ".. salsa machines optimization: optimizing floating-point accuracy with Salsa@,");
+ (* Selecting float constants for Salsa *)
+ let constEnv = List.fold_left (
+ fun accu c_topdecl ->
+ match c_topdecl.top_decl_desc with
+ | Const c when Types.is_real_type c.const_type ->
+ (c.const_id, c.const_value) :: accu
+ | _ -> accu
+ ) [] (Corelang.get_consts prog)
+ in
+ List.map
+ (Machine_salsa_opt.machine_t2machine_t_optimized_by_salsa constEnv)
+ machine_code
+ end
+ else
+ machine_code
+ in
+ Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@ "
+ (Utils.fprintf_list ~sep:"@ " Machine_code.pp_machine)
+ machine_code);
+ *)
+
+
+ machine_code
+
+
(* Local Variables: *)
(* compile-command:"make -C .." *)
(* End: *)
diff --git a/src/options_management.ml b/src/options_management.ml
index b8e7c123..33d74b8a 100644
--- a/src/options_management.ml
+++ b/src/options_management.ml
@@ -73,7 +73,7 @@ let set_mpfr prec =
let set_backend s =
output := s;
- Backends.setup s
+ Backends.setup ()
let common_options =
[ "-d", Arg.Set_string dest_dir, "uses the specified \x1b[4mdirectory\x1b[0m as root for generated/imported object and C files <default: .>";
--
GitLab