Correcting a few bugs in trace selection and expansion

2 files changed, 20 insertions, 15 deletions

diff --git a/backend/Duplicateaux.ml b/backend/Duplicateaux.ml
index cabcf1fd..37647714 100644
--- a/backend/Duplicateaux.ml
+++ b/backend/Duplicateaux.ml
@@ -198,9 +198,8 @@ let do_loop_heuristic code cond ifso ifnot is_loop_header =
 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 *)
+  and directions = ref (PTree.map (fun n i -> None) code) (* None <=> no predicted direction *)
   in begin
-    (* Printf.printf "Loop headers: "; *)
     (* ptree_printbool is_loop_header; *)
     (* Printf.printf "\n"; *)
     List.iter (fun n ->
@@ -217,11 +216,10 @@ let get_directions code entrypoint =
               | None -> preferred := do_heur code cond ifso ifnot is_loop_header
               | Some _ -> ()
             ) heuristics;
-            (match !preferred with None -> (Printf.printf "\tRANDOM\n"; preferred := Some (Random.bool ())) | Some _ -> ());
-            directions := PTree.set n (get_some !preferred) !directions;
+            directions := PTree.set n !preferred !directions;
             (match !preferred with | Some false -> Printf.printf "\tFALLTHROUGH\n"
-                                  | Some true -> Printf.printf "\tBRANCH\n"
-                                  | None -> ());
+                                   | Some true -> Printf.printf "\tBRANCH\n"
+                                   | None -> Printf.printf "\tUNSURE\n");
             Printf.printf "---------------------------------------\n"
           end
       | _ -> ()
@@ -230,7 +228,7 @@ let get_directions code entrypoint =
   end
 
 let update_direction direction = function
-| Icond (cond, lr, n, n', _) -> Icond (cond, lr, n, n', Some direction)
+| Icond (cond, lr, n, n', _) -> Icond (cond, lr, n, n', direction)
 | i -> i
 
 let rec update_direction_rec directions = function
@@ -239,6 +237,7 @@ let rec update_direction_rec directions = function
     in let direction = get_some @@ PTree.get n directions
     in PTree.set n (update_direction direction i) (update_direction_rec directions lm)
 
+(* Uses branch prediction to write prediction annotations in Icond *)
 let update_directions code entrypoint =
   let directions = get_directions code entrypoint
   in begin
@@ -510,7 +509,7 @@ let rec invert_iconds code = function
 
 let duplicate_aux f =
   let entrypoint = f.fn_entrypoint in
-  let code = f.fn_code in
+  let code = update_directions (f.fn_code) entrypoint in
   let traces = select_traces code entrypoint in
   let icond_code = invert_iconds code traces in
   let preds = get_predecessors_rtl icond_code in
diff --git a/backend/Linearizeaux.ml b/backend/Linearizeaux.ml
index c9a5d620..5b3384f2 100644
--- a/backend/Linearizeaux.ml
+++ b/backend/Linearizeaux.ml
@@ -154,7 +154,7 @@ let forward_sequences code entry =
   let visited = ref (PTree.map (fun n i -> false) code) in
   (* 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); *)
+    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
@@ -163,12 +163,13 @@ let forward_sequences code entry =
           let ln, rem = match (last_element bb) with
           | Lop _ | Lload _ | Lgetstack _ | Lsetstack _ | Lstore _ | Lcall _
           | Lbuiltin _ -> assert false
-          | Ltailcall _ | Lreturn -> ([], [])
+          | Ltailcall _ | Lreturn -> begin Printf.printf "STOP tailcall/return\n"; ([], []) end
           | 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)
+          | Lcond (_, _, ifso, ifnot, info) -> (match info with
+            | None -> begin Printf.printf "STOP Lcond None\n"; ([], [ifso; ifnot]) end
+            | Some false -> let ln, rem = traverse_fallthrough code ifnot in (ln, [ifso] @ rem)
+            | Some true -> failwith "Inconsistency detected: ifnot is not the preferred branch")
+          | Ljumptable(_, ln) -> begin Printf.printf "STOP Ljumptable\n"; ([], ln) end
           in ([node] @ ln, rem)
       end
     else ([], [])
@@ -179,6 +180,7 @@ let forward_sequences code entry =
       in [fs] @ ((f code rem_from_node) @ (f code ln))
   in (f code [entry])
 
+(** Unused code
 module PInt = struct
   type t = P.t
   let compare x y = compare (P.to_int x) (P.to_int y)
@@ -219,7 +221,10 @@ let can_be_merged code s s' =
   | Lop _ | Lload _ | Lgetstack _ | Lsetstack _ | Lstore _ | Lcall _
   | Lbuiltin _ | Ltailcall _ | Lreturn -> false
   | Lbranch n -> n == first_s'
-  | Lcond (_, _, ifso, ifnot, _) -> ifnot == first_s'
+  | Lcond (_, _, ifso, ifnot, info) -> (match info with
+    | None -> false
+    | Some false -> ifnot == first_s'
+    | Some true -> failwith "Inconsistency detected - ifnot is not the preferred branch")
   | Ljumptable (_, ln) ->
       match ln with
       | [] -> false
@@ -256,6 +261,7 @@ let try_merge code (fs: (BinNums.positive list) list) =
     end
   done;
   !seqs
+*)
 
 (** Code adapted from Duplicateaux.get_loop_headers
   *