From ab520acd80f7d39aa14fdda6932accbb2a787ebf Mon Sep 17 00:00:00 2001
From: Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>
Date: Wed, 19 May 2021 12:47:22 +0200
Subject: Grouping common RTL functions, printer improvement

---
 common/AuxTools.ml   | 49 +++++++++++++++++++++++++++++++++++++++++++++++++
 common/DebugPrint.ml |  6 ++----
 2 files changed, 51 insertions(+), 4 deletions(-)
 create mode 100644 common/AuxTools.ml

(limited to 'common')

diff --git a/common/AuxTools.ml b/common/AuxTools.ml
new file mode 100644
index 00000000..a667044f
--- /dev/null
+++ b/common/AuxTools.ml
@@ -0,0 +1,49 @@
+open RTL
+open Maps
+
+let get_some = function
+  | None -> failwith "Got None instead of Some _"
+  | Some thing -> thing
+
+let successors_inst = function
+  | Inop n
+  | Iop (_, _, _, n)
+  | Iload (_, _, _, _, _, n)
+  | Istore (_, _, _, _, n)
+  | Icall (_, _, _, _, n)
+  | Ibuiltin (_, _, _, n) ->
+      [ n ]
+  | Icond (_, _, n1, n2, _) -> [ n1; n2 ]
+  | Ijumptable (_, l) -> l
+  | Itailcall _ | Ireturn _ -> []
+
+let predicted_successor = function
+  | Inop n | Iop (_, _, _, n) | Iload (_, _, _, _, _, n) | Istore (_, _, _, _, n)
+    ->
+      Some n
+  | Icall (_, _, _, _, n) | Ibuiltin (_, _, _, n) -> None
+  | Icond (_, _, n1, n2, p) -> (
+      match p with Some true -> Some n1 | Some false -> Some n2 | None -> None)
+  | Ijumptable _ | Itailcall _ | Ireturn _ -> None
+
+let non_predicted_successors i = function
+  | None -> successors_inst i
+  | Some ps -> List.filter (fun s -> s != ps) (successors_inst i)
+
+(* adapted from Linearizeaux.get_join_points *)
+let get_join_points code entry =
+  let reached = ref (PTree.map (fun n i -> false) code) in
+  let reached_twice = ref (PTree.map (fun n i -> false) code) in
+  let rec traverse pc =
+    if get_some @@ PTree.get pc !reached then begin
+      if not (get_some @@ PTree.get pc !reached_twice) then
+        reached_twice := PTree.set pc true !reached_twice
+    end else begin
+      reached := PTree.set pc true !reached;
+      traverse_succs (successors_inst @@ get_some @@ PTree.get pc code)
+    end
+  and traverse_succs = function
+    | [] -> ()
+    | [pc] -> traverse pc
+    | pc :: l -> traverse pc; traverse_succs l
+  in traverse entry; !reached_twice
diff --git a/common/DebugPrint.ml b/common/DebugPrint.ml
index 6f8449ee..021ea5c0 100644
--- a/common/DebugPrint.ml
+++ b/common/DebugPrint.ml
@@ -1,6 +1,7 @@
 open Maps
 open Camlcoq
 open Registers
+open AuxTools
 
 let debug_flag = ref false
 
@@ -128,10 +129,7 @@ end
 
 
 let print_instructions insts code =
-  let get_some = function
-  | None -> failwith "Did not get some"
-  | Some thing -> thing
-  in if (!debug_flag) then begin
+  if (!debug_flag) then begin
     debug "[ ";
     List.iter (
       fun n -> (PrintRTL.print_instruction stdout (P.to_int n, get_some @@ PTree.get n code))
-- 
cgit