From a54e1a5b176e52a94840cbabc02d02611fcdb673 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Tue, 8 Dec 2020 13:42:59 +0100 Subject: More debug --- backend/Duplicateaux.ml | 27 +++++++++++++++++++++------ 1 file changed, 21 insertions(+), 6 deletions(-) (limited to 'backend/Duplicateaux.ml') 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 -- cgit