aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--driver/Clflags.ml1
-rw-r--r--driver/Compopts.v3
-rw-r--r--driver/Driver.ml2
-rw-r--r--extraction/extraction.v4
-rw-r--r--mppa_k1c/PostpassSchedulingOracle.ml5
5 files changed, 12 insertions, 3 deletions
diff --git a/driver/Clflags.ml b/driver/Clflags.ml
index 77fae8ee..fe7aef10 100644
--- a/driver/Clflags.ml
+++ b/driver/Clflags.ml
@@ -28,6 +28,7 @@ let option_fconstprop = ref true
let option_fcse = ref true
let option_fredundancy = ref true
let option_fpostpass = ref true
+let option_pp_optimizer = ref 1
let option_falignfunctions = ref (None: int option)
let option_falignbranchtargets = ref 0
let option_faligncondbranchs = ref 0
diff --git a/driver/Compopts.v b/driver/Compopts.v
index e6eecc9b..16ad7c33 100644
--- a/driver/Compopts.v
+++ b/driver/Compopts.v
@@ -42,6 +42,9 @@ Parameter optim_redundancy: unit -> bool.
(** Flag -fpostpass. Postpass scheduling for K1 architecture *)
Parameter optim_postpass: unit -> bool.
+(** Flag -fpp_optimizer, to specify the postpass optimizer to use *)
+Parameter optim_pp_optimizer: unit -> nat.
+
(** Flag -fthumb. For the ARM back-end. *)
Parameter thumb: unit -> bool.
diff --git a/driver/Driver.ml b/driver/Driver.ml
index 467cf989..36d55913 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -194,6 +194,7 @@ Processing options:
-fcse Perform common subexpression elimination [on]
-fredundancy Perform redundancy elimination [on]
-fpostpass Perform postpass scheduling (only for K1 architecture) [on]
+ -pp-optimizer Select the postpass optimizer to use if -fpostpass is active [list_scheduler]
-finline Perform inlining of functions [on]
-finline-functions-called-once Integrate functions only required by their
single caller [on]
@@ -295,6 +296,7 @@ let cmdline_actions =
Exact "-O", Unit (set_all optimization_options);
_Regexp "-O[123]$", Unit (set_all optimization_options);
Exact "-Os", Set option_Osize;
+ Exact "-pp-optimizer", String(fun s -> option_pp_optimizer := if (s == "list_scheduler") then 1 else 0);
Exact "-fsmall-data", Integer(fun n -> option_small_data := n);
Exact "-fsmall-const", Integer(fun n -> option_small_const := n);
Exact "-ffloat-const-prop", Integer(fun n -> option_ffloatconstprop := n);
diff --git a/extraction/extraction.v b/extraction/extraction.v
index f58991aa..a7fe8f9f 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -113,6 +113,8 @@ Extract Constant Compopts.optim_redundancy =>
"fun _ -> !Clflags.option_fredundancy".
Extract Constant Compopts.optim_postpass =>
"fun _ -> !Clflags.option_fpostpass".
+Extract Constant Compopts.optim_pp_optimizer =>
+ "fun _ -> !Clflags.option_pp_optimizer".
Extract Constant Compopts.thumb =>
"fun _ -> !Clflags.option_mthumb".
Extract Constant Compopts.debug =>
@@ -191,4 +193,4 @@ Separate Extraction
Floats.Float32.from_parsed Floats.Float.from_parsed
Globalenvs.Senv.invert_symbol
Parser.translation_unit_file
- Compopts.optim_postpass.
+ Compopts.optim_postpass Compopts.optim_pp_optimizer.
diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml
index 7b632144..4d448df3 100644
--- a/mppa_k1c/PostpassSchedulingOracle.ml
+++ b/mppa_k1c/PostpassSchedulingOracle.ml
@@ -684,8 +684,9 @@ let print_bb oc bb =
in List.iter (print_inst oc) asm_instructions
let do_schedule bb =
- let problem = build_problem bb
- in let solution = validated_scheduler list_scheduler problem
+ let scheduler = match Compopts.optim_pp_optimizer () with 1 -> list_scheduler | _ -> failwith "No scheduler provided"
+ in let problem = build_problem bb
+ in let solution = validated_scheduler scheduler problem
in match solution with
| None -> failwith "Could not find a valid schedule"
| Some sol -> let bundles = bundlize_solution bb sol in