1 files changed, 78 insertions, 3 deletions

diff --git a/backend/Linearizeaux.ml b/backend/Linearizeaux.ml
index 902724e0..5914f6a3 100644
--- a/backend/Linearizeaux.ml
+++ b/backend/Linearizeaux.ml
@@ -12,7 +12,12 @@
 
 open LTL
 open Maps
-open Camlcoq
+
+let debug_flag = ref false
+
+let debug fmt =
+  if !debug_flag then Printf.eprintf fmt
+  else Printf.ifprintf stderr fmt
 
 (* Trivial enumeration, in decreasing order of PC *)
 
@@ -29,6 +34,8 @@ let enumerate_aux f reach =
 
 (* More clever enumeration that flattens basic blocks *)
 
+open Camlcoq
+
 module IntSet = Set.Make(struct type t = int let compare = compare end)
 
 (* Determine join points: reachable nodes that have > 1 predecessor *)
@@ -80,7 +87,7 @@ let basic_blocks f joins =
        | [] -> assert false
        | Lbranch s :: _ -> next_in_block blk minpc s
        | Ltailcall (sig0, ros) :: _ -> end_block blk minpc
-       | Lcond (cond, args, ifso, ifnot) :: _ ->
+       | Lcond (cond, args, ifso, ifnot, _) :: _ ->
              end_block blk minpc; start_block ifso; start_block ifnot
        | Ljumptable(arg, tbl) :: _ ->
              end_block blk minpc; List.iter start_block tbl
@@ -110,5 +117,73 @@ let flatten_blocks blks =
 
 (* Build the enumeration *)
 
-let enumerate_aux f reach =
+let enumerate_aux_flat f reach =
   flatten_blocks (basic_blocks f (join_points f))
+
+(**
+ * Alternate enumeration based on traces as identified by Duplicate.v 
+ *
+ * This is a slight alteration to the above heuristic, ensuring that any
+ * superblock will be contiguous in memory, while still following the original
+ * heuristic
+ *
+ * Slight change: instead of taking the minimum pc of the superblock, we just take
+ * the pc of the first block.
+ * (experimentally this leads to slightly better performance..)
+ *)
+
+let super_blocks f joins =
+  let blocks = ref [] in
+  let visited = ref IntSet.empty in
+  (* start_block:
+       pc is the function entry point
+          or a join point
+          or the successor of a conditional test *)
+  let rec start_block pc =
+    let npc = P.to_int pc in
+    if not (IntSet.mem npc !visited) then begin
+      visited := IntSet.add npc !visited;
+      in_block [] npc pc
+    end
+  (* in_block: add pc to block and check successors *)
+  and in_block blk minpc pc =
+    let blk = pc :: blk in
+    match PTree.get pc f.fn_code with
+    | None -> assert false
+    | Some b ->
+       let rec do_instr_list = function
+       | [] -> assert false
+       | Lbranch s :: _ -> next_in_block blk minpc s
+       | Ltailcall (sig0, ros) :: _ -> end_block blk minpc
+       | Lcond (cond, args, ifso, ifnot, pred) :: _ -> begin
+            match pred with
+            | None -> (end_block blk minpc; start_block ifso; start_block ifnot)
+            | Some true -> (next_in_block blk minpc ifso; start_block ifnot)
+            | Some false -> (next_in_block blk minpc ifnot; start_block ifso)
+          end
+       | Ljumptable(arg, tbl) :: _ ->
+             end_block blk minpc; List.iter start_block tbl
+       | Lreturn :: _ -> end_block blk minpc
+       | instr :: b' -> do_instr_list b' in
+       do_instr_list b
+  (* next_in_block: check if join point and either extend block
+     or start block *)
+  and next_in_block blk minpc pc =
+    let npc = P.to_int pc in
+    if IntSet.mem npc joins
+    then (end_block blk minpc; start_block pc)
+    else in_block blk minpc pc
+  (* end_block: record block that we just discovered *)
+  and end_block blk minpc =
+    blocks := (minpc, List.rev blk) :: !blocks
+  in
+    start_block f.fn_entrypoint; !blocks
+
+(* Build the enumeration *)
+
+let enumerate_aux_sb f reach =
+  flatten_blocks (super_blocks f (join_points f))
+
+let enumerate_aux f reach =
+  if !Clflags.option_ftracelinearize then enumerate_aux_sb f reach
+  else enumerate_aux_flat f reach