More debug

1 files changed, 21 insertions, 6 deletions

diff --git a/backend/Duplicateaux.ml b/backend/Duplicateaux.ml
index b43a1585..f70666e4 100644
--- a/backend/Duplicateaux.ml
+++ b/backend/Duplicateaux.ml
@@ -202,9 +202,13 @@ let do_loop2_heuristic loop_info n code cond ifso ifnot is_loop_header =
 (* Returns a PTree of either None or Some b where b determines the node following the loop, for a cb instruction *)
 (* It uses the fact that loops in CompCert are done by a branch (backedge) instruction followed by a cb *)
 let get_loop_info is_loop_header bfs_order code =
+  debug "GET LOOP INFO\n";
+  debug "==================================\n";
   let loop_info = ref (PTree.map (fun n i -> None) code) in
   let mark_path s n =
     let visited = ref (PTree.map (fun n i -> false) code) in
+    (* Returns true if there is a path from src to dest (not involving jumptables) *)
+    (* Mark nodes as visited along the way *)
     let rec explore src dest =
       if (get_some @@ PTree.get src !visited) then false
       else if src == dest then true
@@ -216,6 +220,9 @@ let get_loop_info is_loop_header bfs_order code =
         | [s1; s2] -> (explore s1 dest) || (explore s2 dest)
         | _ -> false
       end
+    (* Goes forward until a CB is encountered
+     * Returns None if no CB was found, or Some the_cb_node
+     * Marks nodes as visited along the way *)
     in let rec advance_to_cb src =
       if (get_some @@ PTree.get src !visited) then None
       else begin
@@ -234,14 +241,21 @@ let get_loop_info is_loop_header bfs_order code =
           match get_some @@ PTree.get s !loop_info with
           | None | Some _ -> begin
               match get_some @@ PTree.get s code with
-              | Icond (_, _, n1, n2, _) ->
+              | Icond (_, _, n1, n2, _) -> (
                   let b1 = explore n1 n in
                   let b2 = explore n2 n in
-                  if (b1 && b2) then (debug "both true\n")
-                  else if b1 then (debug "true privileged\n"; loop_info := PTree.set s (Some true) !loop_info)
-                  else if b2 then (debug "false privileged\n"; loop_info := PTree.set s (Some false) !loop_info)
-                  else (debug "none true\n")
-              | _ -> ( debug "not an icond\n" )
+                  if (b1 && b2) then 
+                    debug "\tBoth paths lead back to the head: NONE\n"
+                  else if b1 then begin 
+                    debug "\tTrue path leads to the head: TRUE\n"; 
+                    loop_info := PTree.set s (Some true) !loop_info
+                  end else if b2 then begin
+                    debug "\tFalse path leads to the head: FALSE\n";
+                    loop_info := PTree.set s (Some false) !loop_info
+                  end else
+                    debug "\tNo path leads back to the head: NONE\n"
+                )
+              | _ -> failwith "\tNot an Icond\n"
             end
           (* | Some _ -> ( debug "already loop info there\n" ) FIXME - we don't know yet whether a branch to a loop head is a backedge or not *)
         )
@@ -256,6 +270,7 @@ let get_loop_info is_loop_header bfs_order code =
       | Ijumptable _ -> ()
       | Itailcall _ | Ireturn _ -> ()
     ) bfs_order;
+    debug "==================================\n";
     !loop_info
   end