Merge branch 'kvx-work' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into kvx-work

1 files changed, 118 insertions, 0 deletions

diff --git a/common/DebugPrint.ml b/common/DebugPrint.ml
new file mode 100644
index 00000000..64efe727
--- /dev/null
+++ b/common/DebugPrint.ml
@@ -0,0 +1,118 @@
+open Maps
+open Camlcoq
+open Registers
+
+let debug_flag = ref false
+
+let debug fmt =
+  if !debug_flag then (flush stderr; Printf.eprintf fmt)
+  else Printf.ifprintf stderr fmt
+
+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
+
+(* Adapted from backend/PrintRTL.ml: print_function *)
+let print_code code = let open PrintRTL in let open Printf in
+  if (!debug_flag) then begin
+    fprintf stdout "{\n";
+    let instrs =
+      List.sort
+        (fun (pc1, _) (pc2, _) -> compare pc2 pc1)
+        (List.rev_map
+          (fun (pc, i) -> (P.to_int pc, i))
+          (PTree.elements code)) in
+    List.iter (print_instruction stdout) instrs;
+    fprintf stdout "}"
+  end
+
+let ptree_printbool pt =
+  let elements = PTree.elements pt
+  in begin
+    if !debug_flag then begin
+      Printf.printf "[";
+      List.iter (fun (n, b) ->
+        if b then Printf.printf "%d, " (P.to_int n) else ()
+      ) elements;
+      Printf.printf "]"
+    end
+  end
+
+let print_ptree printer pt =
+  let elements = PTree.elements pt in
+  begin
+    debug "[\n";
+    List.iter (fun (n, elt) ->
+      debug "\t%d: %a\n" (P.to_int n) printer elt
+    ) elements;
+    debug "]\n"
+  end
+
+let print_option_pint oc o =
+  if !debug_flag then
+    match o with
+    | None -> Printf.fprintf oc "None"
+    | Some n -> Printf.fprintf oc "Some %d" (P.to_int n)
+
+let print_pint oc i = if !debug_flag then Printf.fprintf oc "%d" (P.to_int i) else ()
+
+let print_regset rs = begin
+  debug "[";
+  List.iter (fun n -> debug "%d " (P.to_int n)) (Regset.elements rs);
+  debug "]"
+end
+
+let print_ptree_regset pt = begin
+  debug "[";
+  List.iter (fun (n, rs) ->
+    debug "\n\t";
+    debug "%d: " (P.to_int n);
+    print_regset rs
+  ) (PTree.elements pt);
+  debug "]"
+end
+
+let print_true_nodes booltree = begin
+  debug "[";
+  List.iter (fun (n,b) ->
+    if b then debug "%d " (P.to_int n)
+  ) (PTree.elements booltree);
+  debug "]";
+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
+    debug "[ ";
+    List.iter (
+      fun n -> (PrintRTL.print_instruction stdout (P.to_int n, get_some @@ PTree.get n code))
+    ) insts; debug "]"
+  end
+
+let print_arrayp arr = begin
+  debug "[| ";
+  Array.iter (fun n -> debug "%d, " (P.to_int n)) arr;
+  debug "|]"
+end
+