diff options
author | Cyril SIX <cyril.six@kalray.eu> | 2020-12-09 13:04:01 +0100 |
---|---|---|
committer | Cyril SIX <cyril.six@kalray.eu> | 2020-12-09 13:04:01 +0100 |
commit | 72f35c3e93d97eba797031eb1845e8c8d965327d (patch) | |
tree | b2f65fee1270aecd3fe0dd930e788228a68ecd6b /backend/Duplicateaux.ml | |
parent | fac788f255313517de24732370fc3a10dda1b247 (diff) | |
download | compcert-kvx-72f35c3e93d97eba797031eb1845e8c8d965327d.tar.gz compcert-kvx-72f35c3e93d97eba797031eb1845e8c8d965327d.zip |
Fixing exponential blowup on get_loop_info.mark_path.explore
Diffstat (limited to 'backend/Duplicateaux.ml')
-rw-r--r-- | backend/Duplicateaux.ml | 77 |
1 files changed, 44 insertions, 33 deletions
diff --git a/backend/Duplicateaux.ml b/backend/Duplicateaux.ml index 498cc2c5..a58ab2c2 100644 --- a/backend/Duplicateaux.ml +++ b/backend/Duplicateaux.ml @@ -210,39 +210,50 @@ let get_loop_info is_loop_header bfs_order code = 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 src == dest then true - else if (get_some @@ PTree.get src !visited) then false - else begin - let inst = get_some @@ PTree.get src code in - visited := PTree.set src true !visited; - match rtl_successors inst with - | [] -> false - | [s] -> explore s dest - | [s1; s2] -> let snapshot_visited = ref !visited in begin - (* Remembering that we tried the ifso node *) - cb_info := PTree.set src true !cb_info; - match explore s1 dest with - | true -> ( - visited := !snapshot_visited; - match explore s2 dest with - | true -> begin - (* Both paths lead to a loop: we cannot predict the CB - * (but the explore still succeeds) *) - cb_info := PTree.remove src !cb_info; - true - end - | false -> true (* nothing to do, the explore succeeded *) - ) - | false -> begin - cb_info := PTree.set src false !cb_info; - match explore s2 dest with - | true -> true - | false -> (cb_info := PTree.remove src !cb_info; false) - end - end - | _ -> false - end + let explore src dest = + (* Memoizing the results to avoid exponential blow-up *) + let memory = ref PTree.empty in + let rec explore_rec src = + if src == dest then true + else if (get_some @@ PTree.get src !visited) then false + else begin + let inst = get_some @@ PTree.get src code in + visited := PTree.set src true !visited; + match rtl_successors inst with + | [] -> false + | [s] -> explore_wrap s + | [s1; s2] -> let snapshot_visited = ref !visited in begin + debug "\t\tSplit at %d: either %d or %d\n" (P.to_int src) (P.to_int s1) (P.to_int s2); + (* Remembering that we tried the ifso node *) + cb_info := PTree.set src true !cb_info; + match explore_wrap s1 with + | true -> ( + visited := !snapshot_visited; + match explore_wrap s2 with + | true -> begin + (* Both paths lead to a loop: we cannot predict the CB + * (but the explore still succeeds) *) + cb_info := PTree.remove src !cb_info; + true + end + | false -> true (* nothing to do, the explore succeeded *) + ) + | false -> begin + cb_info := PTree.set src false !cb_info; + match explore_wrap s2 with + | true -> true + | false -> (cb_info := PTree.remove src !cb_info; false) + end + end + | _ -> false + end + and explore_wrap src = begin + match PTree.get src !memory with + | Some b -> b + | None -> + let result = explore_rec src in + (memory := PTree.set src result !memory; result) + end in explore_wrap src (* 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 *) |