From 72f35c3e93d97eba797031eb1845e8c8d965327d Mon Sep 17 00:00:00 2001
From: Cyril SIX <cyril.six@kalray.eu>
Date: Wed, 9 Dec 2020 13:04:01 +0100
Subject: Fixing exponential blowup on get_loop_info.mark_path.explore

---
 backend/Duplicateaux.ml | 77 ++++++++++++++++++++++++++++---------------------
 1 file changed, 44 insertions(+), 33 deletions(-)

(limited to 'backend/Duplicateaux.ml')

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 *)
-- 
cgit