Merge branch 'mppa-work' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work

7 files changed, 372 insertions, 144 deletions

diff --git a/backend/Duplicateaux.ml b/backend/Duplicateaux.ml
index d0b7129e..636a8d8e 100644
--- a/backend/Duplicateaux.ml
+++ b/backend/Duplicateaux.ml
@@ -95,52 +95,6 @@ let print_intset s =
     Printf.printf "}"
   end
 
-(* FIXME - dominators not working well because the order of dataflow update isn't right *)
-  (*
-let get_dominators code entrypoint =
-  let bfs_order = bfs code entrypoint
-  and predecessors = get_predecessors_rtl code
-  in let doms = ref (PTree.map (fun n i -> PSet.of_list bfs_order) code)
-  in begin
-    Printf.printf "BFS: ";
-    print_intlist bfs_order;
-    Printf.printf "\n";
-    List.iter (fun n ->
-      let preds = get_some @@ PTree.get n predecessors
-      and single = PSet.singleton n
-      in match preds with
-      | [] -> doms := PTree.set n single !doms
-      | p::lp ->
-          let set_p = get_some @@ PTree.get p !doms
-          and set_lp = List.map (fun p -> get_some @@ PTree.get p !doms) lp
-          in let inter = List.fold_left PSet.inter set_p set_lp
-          in let union = PSet.union inter single
-          in begin
-            Printf.printf "----------------------------------------\n";
-            Printf.printf "n = %d\n" (P.to_int n);
-            Printf.printf "set_p = "; print_intset set_p; Printf.printf "\n";
-            Printf.printf "set_lp = ["; List.iter (fun s -> print_intset s; Printf.printf ", ") set_lp; Printf.printf "]\n";
-            Printf.printf "=> inter = "; print_intset inter; Printf.printf "\n";
-            Printf.printf "=> union = "; print_intset union; Printf.printf "\n";
-            doms := PTree.set n union !doms
-          end
-    ) bfs_order;
-    !doms
-  end
-*)
-
-let print_dominators dominators =
-  let domlist = PTree.elements dominators
-  in begin
-    Printf.printf "{\n";
-    List.iter (fun (n, doms) ->
-      Printf.printf "\t";
-      Printf.printf "%d:" (P.to_int n);
-      print_intset doms;
-      Printf.printf "\n"
-    ) domlist
-  end
-
 type vstate = Unvisited | Processed | Visited
 
 (** Getting loop branches with a DFS visit :
@@ -206,78 +160,62 @@ let rec look_ahead code node is_loop_header predicate =
         else look_ahead code n is_loop_header predicate
       )
 
-exception HeuristicSucceeded
-
-let do_call_heuristic code ifso ifnot is_loop_header preferred =
+let do_call_heuristic code cond ifso ifnot is_loop_header =
   let predicate n = (function
   | Icall _ -> true
   | _ -> false) @@ get_some @@ PTree.get n code
-  in if (look_ahead code ifso is_loop_header predicate) then
-    (preferred := false; raise HeuristicSucceeded)
-  else if (look_ahead code ifnot is_loop_header predicate) then
-    (preferred := true; raise HeuristicSucceeded)
-  else ()
+  in if (look_ahead code ifso is_loop_header predicate) then Some false
+  else if (look_ahead code ifnot is_loop_header predicate) then Some true
+  else None
 
-let do_opcode_heuristic code cond ifso ifnot preferred = DuplicateOpcodeHeuristic.opcode_heuristic code cond ifso ifnot preferred
+let do_opcode_heuristic code cond ifso ifnot is_loop_header = DuplicateOpcodeHeuristic.opcode_heuristic code cond ifso ifnot is_loop_header
 
-let do_return_heuristic code ifso ifnot is_loop_header preferred =
+let do_return_heuristic code cond ifso ifnot is_loop_header =
   let predicate n = (function
   | Ireturn _ -> true
   | _ -> false) @@ get_some @@ PTree.get n code
-  in if (look_ahead code ifso is_loop_header predicate) then
-    (preferred := false; raise HeuristicSucceeded)
-  else if (look_ahead code ifnot is_loop_header predicate) then
-    (preferred := true; raise HeuristicSucceeded)
-  else ()
+  in if (look_ahead code ifso is_loop_header predicate) then Some false
+  else if (look_ahead code ifnot is_loop_header predicate) then Some true
+  else None
 
-let do_store_heuristic code ifso ifnot is_loop_header preferred =
+let do_store_heuristic code cond ifso ifnot is_loop_header =
   let predicate n = (function
   | Istore _ -> true
   | _ -> false) @@ get_some @@ PTree.get n code
-  in if (look_ahead code ifso is_loop_header predicate) then
-    (preferred := false; raise HeuristicSucceeded)
-  else if (look_ahead code ifnot is_loop_header predicate) then
-    (preferred := true; raise HeuristicSucceeded)
-  else ()
+  in if (look_ahead code ifso is_loop_header predicate) then Some false
+  else if (look_ahead code ifnot is_loop_header predicate) then Some true
+  else None
 
-let do_loop_heuristic code ifso ifnot is_loop_header preferred =
+let do_loop_heuristic code cond ifso ifnot is_loop_header =
   let predicate n = get_some @@ PTree.get n is_loop_header
-  in if (look_ahead code ifso is_loop_header predicate) then
-    (preferred := true; raise HeuristicSucceeded)
-  else if (look_ahead code ifnot is_loop_header predicate) then
-    (preferred := false; raise HeuristicSucceeded)
-  else ()
+  in if (look_ahead code ifso is_loop_header predicate) then Some true
+  else if (look_ahead code ifnot is_loop_header predicate) then Some false
+  else None
 
 let get_directions code entrypoint =
   let bfs_order = bfs code entrypoint
   and is_loop_header = get_loop_headers code entrypoint
   and directions = ref (PTree.map (fun n i -> false) code) (* false <=> fallthru *)
   in begin
-    Printf.printf "Loop headers: ";
-    ptree_printbool is_loop_header;
-    Printf.printf "\n";
+    (* Printf.printf "Loop headers: "; *)
+    (* ptree_printbool is_loop_header; *)
+    (* Printf.printf "\n"; *)
     List.iter (fun n ->
       match (get_some @@ PTree.get n code) with
       | Icond (cond, lr, ifso, ifnot) ->
-          Printf.printf "Analyzing %d.." (P.to_int n);
-          let preferred = ref false
-          in (try
-            Printf.printf " call..";
-            do_call_heuristic code ifso ifnot is_loop_header preferred;
-            Printf.printf " opcode..";
-            do_opcode_heuristic code cond ifso ifnot preferred;
-            Printf.printf " return..";
-            do_return_heuristic code ifso ifnot is_loop_header preferred;
-            Printf.printf " store..";
-            do_store_heuristic code ifso ifnot is_loop_header preferred;
-            Printf.printf " loop..";
-            do_loop_heuristic code ifso ifnot is_loop_header preferred;
-            Printf.printf "Random choice for %d\n" (P.to_int n);
-            preferred := Random.bool ()
-            with HeuristicSucceeded | DuplicateOpcodeHeuristic.HeuristicSucceeded
-              -> Printf.printf " %s\n" (match !preferred with true -> "BRANCH"
-                                        | false -> "FALLTHROUGH")
-          ); directions := PTree.set n !preferred !directions
+          (* Printf.printf "Analyzing %d.." (P.to_int n); *)
+          let heuristics = [ do_call_heuristic; do_opcode_heuristic;
+            do_return_heuristic; do_store_heuristic; do_loop_heuristic ] in
+          let preferred = ref None in
+          begin
+            List.iter (fun do_heur ->
+              match !preferred with
+              | None -> preferred := do_heur code cond ifso ifnot is_loop_header
+              | Some _ -> ()
+            ) heuristics;
+            match !preferred with None -> preferred := Some (Random.bool ()) | Some _ -> ();
+            directions := PTree.set n (get_some !preferred) !directions
+          end
       | _ -> ()
     ) bfs_order;
     !directions
@@ -306,9 +244,9 @@ let rec to_ttl_code_rec directions = function
 let to_ttl_code code entrypoint =
   let directions = get_directions code entrypoint
   in begin
-    Printf.printf "Ifso directions: ";
+    (* Printf.printf "Ifso directions: ";
     ptree_printbool directions;
-    Printf.printf "\n";
+    Printf.printf "\n"; *)
     Random.init(0); (* using same seed to make it deterministic *)
     to_ttl_code_rec directions (PTree.elements code)
   end
@@ -423,7 +361,7 @@ let select_traces code entrypoint =
         end
       end
     done;
-    Printf.printf "DFS: \t"; print_intlist order; Printf.printf "\n";
+    (* Printf.printf "DFS: \t"; print_intlist order; Printf.printf "\n"; *)
     !traces
   end
 
@@ -471,7 +409,7 @@ let rec change_pointers code n n' = function
  * n': the integer which should contain the duplicate of n
  * returns: new code, new ptree *)
 let duplicate code ptree parent n preds n' =
-  Printf.printf "Duplicating node %d into %d..\n" (P.to_int n) (P.to_int n');
+  (* Printf.printf "Duplicating node %d into %d..\n" (P.to_int n) (P.to_int n'); *)
   match PTree.get n' code with
   | Some _ -> failwith "The PTree already has a node n'"
   | None ->
@@ -529,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)
@@ -548,7 +486,7 @@ let rec invert_iconds_trace code = function
         | Icond (c, lr, ifso, ifnot) ->
             assert (n' == ifso || n' == ifnot);
             if (n' == ifso) then (
-              Printf.printf "Reversing ifso/ifnot for node %d\n" (P.to_int n);
+              (* Printf.printf "Reversing ifso/ifnot for node %d\n" (P.to_int n); *)
               PTree.set n (Icond (Op.negate_condition c, lr, ifnot, ifso)) code )
             else code
         | _ -> code
@@ -561,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/backend/Linearizeaux.ml b/backend/Linearizeaux.ml
index a6964233..a813ac96 100644
--- a/backend/Linearizeaux.ml
+++ b/backend/Linearizeaux.ml
@@ -122,7 +122,11 @@ let enumerate_aux_flat f reach =
  * rather than a branch (ifso).
  *
  * The enumeration below takes advantage of this - preferring to layout nodes
- * following the fallthroughs of the Lcond branches
+ * following the fallthroughs of the Lcond branches.
+ *
+ * It is slightly adapted from the work of Petris and Hansen 90 on intraprocedural
+ * code positioning - only we do it on a broader grain, since we don't have the exact
+ * frequencies (we only know which branch is the preferred one)
  *)
 
 let get_some = function
@@ -136,29 +140,320 @@ let rec last_element = function
   | e :: [] -> e
   | e' :: e :: l -> last_element (e::l)
 
-let dfs code entrypoint =
+let print_plist l =
+  let rec f = function
+  | [] -> ()
+  | n :: l -> Printf.printf "%d, " (P.to_int n); f l
+  in begin
+    Printf.printf "[";
+    f l;
+    Printf.printf "]"
+  end
+
+let forward_sequences code entry =
   let visited = ref (PTree.map (fun n i -> false) code) in
-  let rec dfs_list code = function
+  (* returns the list of traversed nodes, and a list of nodes to start traversing next *)
+  let rec traverse_fallthrough code node =
+    (* Printf.printf "Traversing %d..\n" (P.to_int node); *)
+    if not (get_some @@ PTree.get node !visited) then begin
+      visited := PTree.set node true !visited;
+      match PTree.get node code with
+      | None -> failwith "No such node"
+      | Some bb ->
+          let ln, rem = match (last_element bb) with
+          | Lop _ | Lload _ | Lgetstack _ | Lsetstack _ | Lstore _ | Lcall _
+          | Lbuiltin _ -> assert false
+          | Ltailcall _ | Lreturn -> ([], [])
+          | Lbranch n -> let ln, rem = traverse_fallthrough code n in (ln, rem)
+          | Lcond (_, _, ifso, ifnot) -> let ln, rem = traverse_fallthrough code ifnot in (ln, [ifso] @ rem)
+          | Ljumptable(_, ln) -> match ln with
+              | [] -> ([], [])
+              | n :: ln -> let lln, rem = traverse_fallthrough code n in (lln, ln @ rem)
+          in ([node] @ ln, rem)
+      end
+    else ([], [])
+  in let rec f code = function
   | [] -> []
   | node :: ln ->
-      let node_dfs =
-        if not (get_some @@ PTree.get node !visited) then begin
-          visited := PTree.set node true !visited;
-          match PTree.get node code with
-          | None -> failwith "No such node"
-          | Some bb -> [node] @ match (last_element bb) with
-            | Lop _ | Lload _ | Lgetstack _ | Lsetstack _ | Lstore _ | Lcall _
-            | Lbuiltin _ -> assert false
-            | Ltailcall _ | Lreturn -> []
-            | Lbranch n -> dfs_list code [n]
-            | Lcond (_, _, ifso, ifnot) -> dfs_list code [ifnot; ifso]
-            | Ljumptable(_, ln) -> dfs_list code ln
-          end
-        else []
-      in node_dfs @ (dfs_list code ln)
-  in dfs_list code [entrypoint]
-
-let enumerate_aux_trace f reach = dfs f.fn_code f.fn_entrypoint
+      let fs, rem_from_node = traverse_fallthrough code node
+      in [fs] @ ((f code rem_from_node) @ (f code ln))
+  in (f code [entry])
+
+module PInt = struct
+  type t = P.t
+  let compare x y = compare (P.to_int x) (P.to_int y)
+end
+
+module PSet = Set.Make(PInt)
+
+module LPInt = struct
+  type t = P.t list
+  let rec compare x y =
+    match x with
+    | [] -> ( match y with
+      | [] -> 0
+      | _ -> 1 )
+    | e :: l -> match y with
+      | [] -> -1
+      | e' :: l' ->
+          let e_cmp = PInt.compare e e' in
+          if e_cmp == 0 then compare l l' else e_cmp
+end
+
+module LPSet = Set.Make(LPInt)
+
+let iter_lpset f s = Seq.iter f (LPSet.to_seq s)
+
+let first_of = function
+  | [] -> None
+  | e :: l -> Some e
+
+let rec last_of = function
+  | [] -> None
+  | e :: l -> (match l with [] -> Some e | e :: l -> last_of l)
+
+let can_be_merged code s s' =
+  let last_s = get_some @@ last_of s in
+  let first_s' = get_some @@ first_of s' in
+  match get_some @@ PTree.get last_s code with
+  | Lop _ | Lload _ | Lgetstack _ | Lsetstack _ | Lstore _ | Lcall _
+  | Lbuiltin _ | Ltailcall _ | Lreturn -> false
+  | Lbranch n -> n == first_s'
+  | Lcond (_, _, ifso, ifnot) -> ifnot == first_s'
+  | Ljumptable (_, ln) ->
+      match ln with
+      | [] -> false
+      | n :: ln -> n == first_s'
+
+let merge s s' = Some s
+
+let try_merge code (fs: (BinNums.positive list) list) =
+  let seqs = ref (LPSet.of_list fs) in
+  let oldLength = ref (LPSet.cardinal !seqs) in
+  let continue = ref true in
+  let found = ref false in
+  while !continue do
+    begin
+      found := false;
+      iter_lpset (fun s ->
+        if !found then ()
+        else iter_lpset (fun s' ->
+          if (!found || s == s') then ()
+          else if (can_be_merged code s s') then
+            begin
+              seqs := LPSet.remove s !seqs;
+              seqs := LPSet.remove s' !seqs;
+              seqs := LPSet.add (get_some (merge s s')) !seqs;
+              found := true;
+            end
+          else ()
+        ) !seqs
+      ) !seqs;
+      if !oldLength == LPSet.cardinal !seqs then
+        continue := false
+      else
+        oldLength := LPSet.cardinal !seqs
+    end
+  done;
+  !seqs
+
+(** Code adapted from Duplicateaux.get_loop_headers
+  *
+  * Getting loop branches with a DFS visit :
+  * Each node is either Unvisited, Visited, or Processed
+  * pre-order: node becomes Processed
+  * post-order: node becomes Visited
+  *
+  * If we come accross an edge to a Processed node, it's a loop!
+  *)
+type pos = BinNums.positive
+
+module PP = struct
+  type t = pos * pos
+  let compare a b =
+    let ax, ay = a in
+    let bx, by = b in
+    let dx = compare ax bx in
+    if (dx == 0) then compare ay by
+    else dx
+end
+
+module PPMap = Map.Make(PP)
+
+type vstate = Unvisited | Processed | Visited
+
+let get_loop_edges code entry =
+  let visited = ref (PTree.map (fun n i -> Unvisited) code) in
+  let is_loop_edge = ref PPMap.empty
+  in let rec dfs_visit code from = function
+  | [] -> ()
+  | node :: ln ->
+      match (get_some @@ PTree.get node !visited) with
+      | Visited -> ()
+      | Processed -> begin
+          let from_node = get_some from in
+          is_loop_edge := PPMap.add (from_node, node) true !is_loop_edge;
+          visited := PTree.set node Visited !visited
+        end
+      | Unvisited -> begin
+          visited := PTree.set node Processed !visited;
+          let bb = get_some @@ PTree.get node code in
+          let next_visits = (match (last_element bb) with
+          | Lop _ | Lload _ | Lgetstack _ | Lsetstack _ | Lstore _ | Lcall _
+          | Lbuiltin _ -> assert false
+          | Ltailcall _ | Lreturn -> []
+          | Lbranch n -> [n]
+          | Lcond (_, _, ifso, ifnot) -> [ifso; ifnot]
+          | Ljumptable(_, ln) -> ln
+          ) in dfs_visit code (Some node) next_visits;
+          visited := PTree.set node Visited !visited;
+          dfs_visit code from ln
+        end
+  in begin
+    dfs_visit code None [entry];
+    !is_loop_edge
+  end
+
+let ppmap_is_true pp ppmap = PPMap.mem pp ppmap && PPMap.find pp ppmap
+
+module Int = struct
+  type t = int
+  let compare x y = compare x y
+end
+
+module ISet = Set.Make(Int)
+
+let print_iset s = begin
+  Printf.printf "{";
+  ISet.iter (fun e -> Printf.printf "%d, " e) s;
+  Printf.printf "}"
+end
+
+let print_depmap dm = begin
+  Printf.printf "[|";
+  Array.iter (fun s -> print_iset s; Printf.printf ", ") dm;
+  Printf.printf "|]\n"
+end
+
+let construct_depmap code entry fs =
+  let is_loop_edge = get_loop_edges code entry in
+  let visited = ref (PTree.map (fun n i -> false) code) in
+  let depmap = Array.map (fun e -> ISet.empty) fs in
+  let find_index_of_node n =
+    let index = ref 0 in
+    begin
+      Array.iteri (fun i s ->
+        match List.find_opt (fun e -> e == n) s with
+        | Some _ -> index := i
+        | None -> ()
+      ) fs;
+      !index
+    end
+  in let check_and_update_depmap from target =
+    (* Printf.printf "From %d to %d\n" (P.to_int from) (P.to_int target); *)
+    if not (ppmap_is_true (from, target) is_loop_edge) then
+      let in_index_fs = find_index_of_node from in
+      let out_index_fs = find_index_of_node target in
+      if out_index_fs != in_index_fs then
+        depmap.(out_index_fs) <- ISet.add in_index_fs depmap.(out_index_fs)
+      else ()
+    else ()
+  in let rec dfs_visit code = function
+  | [] -> ()
+  | node :: ln ->
+      begin
+        match (get_some @@ PTree.get node !visited) with
+        | true -> ()
+        | false -> begin
+            visited := PTree.set node true !visited;
+            let bb = get_some @@ PTree.get node code in
+            let next_visits =
+              match (last_element bb) with
+              | Ltailcall _ | Lreturn -> []
+              | Lbranch n -> (check_and_update_depmap node n; [n])
+              | Lcond (_, _, ifso, ifnot) -> begin
+                  check_and_update_depmap node ifso;
+                  check_and_update_depmap node ifnot;
+                  [ifso; ifnot]
+                end
+              | Ljumptable(_, ln) -> begin
+                  List.iter (fun n -> check_and_update_depmap node n) ln;
+                  ln
+                end
+              (* end of bblocks should not be another value than one of the above *)
+              | _ -> failwith "last_element gave an invalid output"
+            in dfs_visit code next_visits
+          end;
+        dfs_visit code ln
+      end
+  in begin
+    dfs_visit code [entry];
+    depmap
+  end
+
+let print_sequence s =
+  Printf.printf "[";
+  List.iter (fun n -> Printf.printf "%d, " (P.to_int n)) s;
+  Printf.printf "]\n"
+
+let print_ssequence ofs =
+  Printf.printf "[";
+  List.iter (fun s -> print_sequence s) ofs;
+  Printf.printf "]\n"
+
+let order_sequences code entry fs =
+  let fs_a = Array.of_list fs in
+  let depmap = construct_depmap code entry fs_a in
+  let fs_evaluated = Array.map (fun e -> false) fs_a in
+  let ordered_fs = ref [] in
+  let evaluate s_id =
+    begin
+      assert (not fs_evaluated.(s_id));
+      ordered_fs := fs_a.(s_id) :: !ordered_fs;
+      fs_evaluated.(s_id) <- true;
+      Array.iteri (fun i deps ->
+        depmap.(i) <- ISet.remove s_id deps
+      ) depmap
+    end
+  in let select_next () =
+    let selected_id = ref None in
+    begin
+      Array.iteri (fun i deps ->
+        begin
+          (* Printf.printf "Deps: "; print_iset deps; Printf.printf "\n"; *)
+          match !selected_id with
+          | None -> if (deps == ISet.empty && not fs_evaluated.(i)) then selected_id := Some i
+          | Some id -> ()
+        end
+      ) depmap;
+      match !selected_id with
+      | Some id -> id
+      | None -> begin
+          Array.iteri (fun i deps ->
+            match !selected_id with
+            | None -> if not fs_evaluated.(i) then selected_id := Some i
+            | Some id -> ()
+          ) depmap;
+          get_some !selected_id
+        end
+    end
+  in begin
+    (* Printf.printf "depmap: "; print_depmap depmap; *)
+    (* Printf.printf "forward sequences identified: "; print_ssequence fs; *)
+    while List.length !ordered_fs != List.length fs do
+      let next_id = select_next () in
+      evaluate next_id
+    done;
+    (* Printf.printf "forward sequences ordered: "; print_ssequence (List.rev (!ordered_fs)); *)
+    List.rev (!ordered_fs)
+  end
+
+let enumerate_aux_trace f reach =
+  let code = f.fn_code in
+  let entry = f.fn_entrypoint in
+  let fs = forward_sequences code entry in
+  let ofs = order_sequences code entry fs in
+  List.flatten ofs
 
 let enumerate_aux f reach =
   if !Clflags.option_ftracelinearize then enumerate_aux_trace f reach
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..43aedf50 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
@@ -318,7 +318,7 @@ let cmdline_actions =
  [
   Exact "-O0", Unit (unset_all optimization_options);
   Exact "-O", Unit (set_all optimization_options);
-  _Regexp "-O1", Self (fun _ -> set_all optimization_options (); option_fpostpass := false; option_fduplicate := false);
+  _Regexp "-O1", Self (fun _ -> set_all optimization_options (); option_fpostpass := false);
   _Regexp "-O[123]$", Unit (set_all optimization_options);
   Exact "-Os", Set option_Osize;
   Exact "-Obranchless", Set option_Obranchless;
@@ -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 =>
diff --git a/mppa_k1c/DuplicateOpcodeHeuristic.ml b/mppa_k1c/DuplicateOpcodeHeuristic.ml
index 690553ce..2ec314c1 100644
--- a/mppa_k1c/DuplicateOpcodeHeuristic.ml
+++ b/mppa_k1c/DuplicateOpcodeHeuristic.ml
@@ -2,10 +2,8 @@
 open Op
 open Integers
 
-exception HeuristicSucceeded
-
-let opcode_heuristic code cond ifso ifnot preferred =
-  let decision = match cond with
+let opcode_heuristic code cond ifso ifnot is_loop_header =
+  match cond with
   | Ccompimm (c, n) | Ccompuimm (c, n) -> if n == Integers.Int.zero then (match c with
       | Clt | Cle -> Some false
       | Cgt | Cge -> Some true
@@ -27,6 +25,3 @@ let opcode_heuristic code cond ifso ifnot preferred =
       | _ -> None
       )
   | _ -> None
-  in match decision with
-  | Some b -> (preferred := b; raise HeuristicSucceeded)
-  | None -> ()