[BROKEN] Replacing the boolean -fduplicate option by an integer

To control the threshold for duplication

5 files changed, 15 insertions, 15 deletions

diff --git a/backend/Duplicateaux.ml b/backend/Duplicateaux.ml
index 05b8ddb8..636a8d8e 100644
--- a/backend/Duplicateaux.ml
+++ b/backend/Duplicateaux.ml
@@ -467,7 +467,7 @@ let tail_duplicate code preds ptree trace =
   in (new_code, new_ptree, !nb_duplicated)
 
 let superblockify_traces code preds traces =
-  let max_nb_duplicated = 1 (* FIXME - should be architecture dependent *)
+  let max_nb_duplicated = !Clflags.option_fduplicate (* FIXME - should be architecture dependent *)
   in let ptree = make_identity_ptree code
   in let rec f code ptree = function
     | [] -> (code, ptree, 0)
@@ -499,12 +499,14 @@ let rec invert_iconds code = function
                   else code
       in invert_iconds code' ts
 
-(* For now, identity function *)
 let duplicate_aux f =
   let entrypoint = f.fn_entrypoint in
   let code = f.fn_code in
   let traces = select_traces (to_ttl_code code entrypoint) entrypoint in
   let icond_code = invert_iconds code traces in
   let preds = get_predecessors_rtl icond_code in
-  let (new_code, pTreeId) = ((* print_traces traces; *) superblockify_traces icond_code preds traces) in
-  ((new_code, f.fn_entrypoint), pTreeId)
+  if !Clflags.option_fduplicate >= 1 then
+    let (new_code, pTreeId) = ((* print_traces traces; *) superblockify_traces icond_code preds traces) in
+    ((new_code, f.fn_entrypoint), pTreeId)
+  else
+    ((icond_code, entrypoint), make_identity_ptree code)
diff --git a/driver/Clflags.ml b/driver/Clflags.ml
index 6d6f1df4..79c0bce0 100644
--- a/driver/Clflags.ml
+++ b/driver/Clflags.ml
@@ -28,8 +28,8 @@ let option_fconstprop = ref true
 let option_fcse = ref true
 let option_fcse2 = ref true
 let option_fredundancy = ref true
-let option_fduplicate = ref false
-let option_finvertcond = ref true (* only active if option_fduplicate is also true *)
+let option_fduplicate = ref 0
+let option_finvertcond = ref true
 let option_ftracelinearize = ref false
 let option_fpostpass = ref true
 let option_fpostpass_sched = ref "list"
diff --git a/driver/Compiler.v b/driver/Compiler.v
index 499feff2..da19a0b9 100644
--- a/driver/Compiler.v
+++ b/driver/Compiler.v
@@ -134,7 +134,7 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program :=
    @@ print (print_RTL 2)
    @@ time "Renumbering" Renumber.transf_program
    @@ print (print_RTL 3)
-  @@@ partial_if Compopts.optim_duplicate (time "Tail-duplicating" Duplicate.transf_program)
+  @@@ time "Tail-duplicating" Duplicate.transf_program
    @@ print (print_RTL 4)
    @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program)
    @@ print (print_RTL 5)
@@ -254,7 +254,7 @@ Definition CompCert's_passes :=
   ::: mkpass (match_if Compopts.optim_tailcalls Tailcallproof.match_prog)
   ::: mkpass Inliningproof.match_prog
   ::: mkpass Renumberproof.match_prog
-  ::: mkpass (match_if Compopts.optim_duplicate Duplicateproof.match_prog)
+  ::: mkpass Duplicateproof.match_prog
   ::: mkpass (match_if Compopts.optim_constprop Constpropproof.match_prog)
   ::: mkpass (match_if Compopts.optim_constprop Renumberproof.match_prog)
   ::: mkpass (match_if Compopts.optim_CSE CSEproof.match_prog)
@@ -301,7 +301,7 @@ Proof.
   set (p7 := total_if optim_tailcalls Tailcall.transf_program p6) in *.
   destruct (Inlining.transf_program p7) as [p8|e] eqn:P8; simpl in T; try discriminate.
   set (p9 := Renumber.transf_program p8) in *.
-  destruct (partial_if optim_duplicate Duplicate.transf_program p9) as [p10|e] eqn:P10; simpl in T; try discriminate.
+  destruct (Duplicate.transf_program p9) as [p10|e] eqn:P10; simpl in T; try discriminate.
   set (p11 := total_if optim_constprop Constprop.transf_program p10) in *.
   set (p12 := total_if optim_constprop Renumber.transf_program p11) in *.
   destruct (partial_if optim_CSE CSE.transf_program p12) as [p13|e] eqn:P13; simpl in T; try discriminate.
@@ -326,7 +326,7 @@ Proof.
   exists p7; split. apply total_if_match. apply Tailcallproof.transf_program_match.
   exists p8; split. apply Inliningproof.transf_program_match; auto.
   exists p9; split. apply Renumberproof.transf_program_match; auto.
-  exists p10; split. eapply partial_if_match; eauto. apply Duplicateproof.transf_program_match; auto.
+  exists p10; split. apply Duplicateproof.transf_program_match; auto.
   exists p11; split. apply total_if_match. apply Constpropproof.transf_program_match.
   exists p12; split. apply total_if_match. apply Renumberproof.transf_program_match.
   exists p13; split. eapply partial_if_match; eauto. apply CSEproof.transf_program_match.
@@ -412,7 +412,7 @@ Ltac DestructM :=
     eapply Inliningproof.transf_program_correct; eassumption.
   eapply compose_forward_simulations. eapply Renumberproof.transf_program_correct; eassumption.
   eapply compose_forward_simulations.
-    eapply match_if_simulation. eassumption. exact Duplicateproof.transf_program_correct.
+    eapply Duplicateproof.transf_program_correct; eassumption.
   eapply compose_forward_simulations.
     eapply match_if_simulation. eassumption. exact Constpropproof.transf_program_correct.
   eapply compose_forward_simulations.
diff --git a/driver/Driver.ml b/driver/Driver.ml
index db71aef9..dd357423 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -204,7 +204,7 @@ Processing options:
     -finvertcond    Invert conditions based on predicted paths (to prefer fallthrough).
                     Requires -fduplicate to be also activated [on]
     -ftracelinearize Linearizes based on the traces identified by duplicate phase
-                    It is recommended to also activate -fduplicate with this pass [off]
+                    It is heavily recommended to activate -finvertcond with this pass [off]
   -fforward-moves   Forward moves after CSE
   -finline       Perform inlining of functions [on]
   -finline-functions-called-once Integrate functions only required by their
@@ -393,7 +393,7 @@ let cmdline_actions =
   @ f_opt "cse2" option_fcse2
   @ f_opt "redundancy" option_fredundancy
   @ f_opt "postpass" option_fpostpass
-  @ f_opt "duplicate" option_fduplicate
+  @ [ Exact "-fduplicate", Integer (fun n -> option_fduplicate := n) ]
   @ f_opt "invertcond" option_finvertcond
   @ f_opt "tracelinearize" option_ftracelinearize
   @ f_opt_str "postpass" option_fpostpass option_fpostpass_sched
diff --git a/extraction/extraction.v b/extraction/extraction.v
index 929c21e0..ba6b080b 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -105,8 +105,6 @@ Extract Constant Compopts.generate_float_constants =>
   "fun _ -> !Clflags.option_ffloatconstprop >= 2".
 Extract Constant Compopts.optim_tailcalls =>
   "fun _ -> !Clflags.option_ftailcalls".
-Extract Constant Compopts.optim_duplicate =>
-  "fun _ -> !Clflags.option_fduplicate".
 Extract Constant Compopts.optim_constprop =>
   "fun _ -> !Clflags.option_fconstprop".
 Extract Constant Compopts.optim_CSE =>