aboutsummaryrefslogtreecommitdiffstats
path: root/backend/LICMaux.ml
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-11-05 09:50:15 +0100
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-11-05 09:50:15 +0100
commit39d14caa044364ea93da7dbc49a699008e505311 (patch)
tree7be8c998cc2289767fa996dc61cd092305bd1002 /backend/LICMaux.ml
parent0fe569d24b99a34fb3b9ad6c0cb86876cc86a31d (diff)
parent160c4ae21cdc86e26850ed0bdec8d95ca23c57db (diff)
downloadcompcert-kvx-39d14caa044364ea93da7dbc49a699008e505311.tar.gz
compcert-kvx-39d14caa044364ea93da7dbc49a699008e505311.zip
Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass
Diffstat (limited to 'backend/LICMaux.ml')
-rw-r--r--backend/LICMaux.ml41
1 files changed, 37 insertions, 4 deletions
diff --git a/backend/LICMaux.ml b/backend/LICMaux.ml
index 3d344123..f166e9e4 100644
--- a/backend/LICMaux.ml
+++ b/backend/LICMaux.ml
@@ -39,6 +39,28 @@ let rtl_successors = function
| Icond (_,_,n1,n2,_) -> [n1; n2]
| Ijumptable (_,ln) -> ln
+let print_ptree_bool oc pt =
+ if !debug_flag then
+ let elements = PTree.elements pt in
+ begin
+ Printf.fprintf oc "[";
+ List.iter (fun (n, b) ->
+ if b then Printf.fprintf oc "%d, " (P.to_int n)
+ ) elements;
+ Printf.fprintf oc "]\n"
+ end
+ else ()
+
+let print_intlist oc l =
+ let rec f oc = function
+ | [] -> ()
+ | n::ln -> (Printf.fprintf oc "%d %a" (P.to_int n) f ln)
+ in begin
+ if !debug_flag then begin
+ Printf.fprintf oc "[%a]" f l
+ end
+ end
+
(** Getting loop branches with a DFS visit :
* Each node is either Unvisited, Visited, or Processed
* pre-order: node becomes Processed
@@ -53,23 +75,34 @@ let get_loop_headers code entrypoint = begin
in let rec dfs_visit code = function
| [] -> ()
| node :: ln ->
+ debug "ENTERING node %d, REM are %a\n" (P.to_int node) print_intlist ln;
match (get_some @@ PTree.get node !visited) with
- | Visited -> ()
+ | Visited -> begin
+ debug "\tNode %d is already Visited, skipping\n" (P.to_int node);
+ dfs_visit code ln
+ end
| Processed -> begin
debug "Node %d is a loop header\n" (P.to_int node);
is_loop_header := PTree.set node true !is_loop_header;
- visited := PTree.set node Visited !visited
+ visited := PTree.set node Visited !visited;
+ dfs_visit code ln
end
| Unvisited -> begin
visited := PTree.set node Processed !visited;
- match PTree.get node code with
+ debug "Node %d is Processed\n" (P.to_int node);
+ (match PTree.get node code with
| None -> failwith "No such node"
- | Some i -> let next_visits = rtl_successors i in dfs_visit code next_visits;
+ | Some i -> let next_visits = rtl_successors i in begin
+ debug "About to visit: %a\n" print_intlist next_visits;
+ dfs_visit code next_visits
+ end);
+ debug "Node %d is Visited!\n" (P.to_int node);
visited := PTree.set node Visited !visited;
dfs_visit code ln
end
in begin
dfs_visit code [entrypoint];
+ debug "LOOP HEADERS: %a\n" print_ptree_bool !is_loop_header;
!is_loop_header
end
end