aboutsummaryrefslogtreecommitdiffstats
path: root/common
diff options
context:
space:
mode:
authorSylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr>2021-01-07 18:26:17 +0100
committerSylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr>2021-01-07 18:26:17 +0100
commit2d086fdfe0ee11204116f6bc442a35a00e77fe38 (patch)
tree9348a282409885a85a15cb55bbddc17421dc3e4d /common
parent10da6dfa77f155d9d1e36e28c8bb8552601355f9 (diff)
parent13b0e8f162f751a9bdbe9952ebe1f22eb77d0f87 (diff)
downloadcompcert-kvx-2d086fdfe0ee11204116f6bc442a35a00e77fe38.tar.gz
compcert-kvx-2d086fdfe0ee11204116f6bc442a35a00e77fe38.zip
Merge branch 'kvx-work' into aarch64-peephole
Diffstat (limited to 'common')
-rw-r--r--common/DebugPrint.ml118
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
+