aboutsummaryrefslogtreecommitdiffstats
path: root/scheduling/PrintBTL.ml
diff options
context:
space:
mode:
authorLéo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>2021-05-27 16:55:18 +0200
committerLéo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>2021-05-27 16:55:18 +0200
commit1a78c940f46273b7146d2111b1e2da309434f021 (patch)
treeefa4c885cabc1a54d223193e754a21c5a3360010 /scheduling/PrintBTL.ml
parenta6006df63f0d03cc223d13834e81a71651513fbe (diff)
downloadcompcert-kvx-1a78c940f46273b7146d2111b1e2da309434f021.tar.gz
compcert-kvx-1a78c940f46273b7146d2111b1e2da309434f021.zip
[disabled checker] BTL Scheduling and Renumbering OK!
Diffstat (limited to 'scheduling/PrintBTL.ml')
-rw-r--r--scheduling/PrintBTL.ml67
1 files changed, 37 insertions, 30 deletions
diff --git a/scheduling/PrintBTL.ml b/scheduling/PrintBTL.ml
index 502565c2..52178064 100644
--- a/scheduling/PrintBTL.ml
+++ b/scheduling/PrintBTL.ml
@@ -4,8 +4,8 @@ open Datatypes
open Maps
open BTL
open PrintAST
-open BTLaux
open DebugPrint
+open BTLtypes
(* Printing of BTL code *)
@@ -26,39 +26,44 @@ let print_pref pp pref = fprintf pp "%s" pref
let rec print_iblock pp is_rec pref ib =
match ib with
- | Bnop _ ->
+ | Bnop None ->
print_pref pp pref;
- fprintf pp "Bnop\n"
- | Bop (op, args, res, _) ->
+ fprintf pp "??: Bnop None\n"
+ | Bnop (Some iinfo) ->
print_pref pp pref;
- fprintf pp "Bop: %a = %a\n" reg res
+ fprintf pp "%d: Bnop\n" iinfo.inumb
+ | Bop (op, args, res, iinfo) ->
+ print_pref pp pref;
+ fprintf pp "%d: Bop: %a = %a\n" iinfo.inumb reg res
(PrintOp.print_operation reg)
(op, args)
- | Bload (trap, chunk, addr, args, dst, _) ->
+ | Bload (trap, chunk, addr, args, dst, iinfo) ->
print_pref pp pref;
- fprintf pp "Bload: %a = %s[%a]%a\n" reg dst (name_of_chunk chunk)
+ fprintf pp "%d: Bload: %a = %s[%a]%a\n" iinfo.inumb reg dst
+ (name_of_chunk chunk)
(PrintOp.print_addressing reg)
(addr, args) print_trapping_mode trap
- | Bstore (chunk, addr, args, src, _) ->
+ | Bstore (chunk, addr, args, src, iinfo) ->
print_pref pp pref;
- fprintf pp "Bstore: %s[%a] = %a\n" (name_of_chunk chunk)
+ fprintf pp "%d: Bstore: %s[%a] = %a\n" iinfo.inumb (name_of_chunk chunk)
(PrintOp.print_addressing reg)
(addr, args) reg src
- | BF (Bcall (sg, fn, args, res, s), _) ->
+ | BF (Bcall (sg, fn, args, res, s), iinfo) ->
print_pref pp pref;
- fprintf pp "Bcall: %a = %a(%a)\n" reg res ros fn regs args;
+ fprintf pp "%d: Bcall: %a = %a(%a)\n" iinfo.inumb reg res ros fn regs args;
print_succ pp s
- | BF (Btailcall (sg, fn, args), _) ->
+ | BF (Btailcall (sg, fn, args), iinfo) ->
print_pref pp pref;
- fprintf pp "Btailcall: %a(%a)\n" ros fn regs args
- | BF (Bbuiltin (ef, args, res, s), _) ->
+ fprintf pp "%d: Btailcall: %a(%a)\n" iinfo.inumb ros fn regs args
+ | BF (Bbuiltin (ef, args, res, s), iinfo) ->
print_pref pp pref;
- fprintf pp "Bbuiltin: %a = %s(%a)\n" (print_builtin_res reg) res
- (name_of_external ef) (print_builtin_args reg) args;
+ fprintf pp "%d: Bbuiltin: %a = %s(%a)\n" iinfo.inumb
+ (print_builtin_res reg) res (name_of_external ef)
+ (print_builtin_args reg) args;
print_succ pp s
| Bcond (cond, args, ib1, ib2, iinfo) ->
print_pref pp pref;
- fprintf pp "Bcond: (%a) (prediction: %s)\n"
+ fprintf pp "%d: Bcond: (%a) (prediction: %s)\n" iinfo.inumb
(PrintOp.print_condition reg)
(cond, args)
(match iinfo.pcond with
@@ -72,39 +77,41 @@ let rec print_iblock pp is_rec pref ib =
fprintf pp "%sifnot = [\n" pref;
if is_rec then print_iblock pp is_rec pref' ib2 else fprintf pp "...\n";
fprintf pp "%s]\n" pref
- | BF (Bjumptable (arg, tbl), _) ->
+ | BF (Bjumptable (arg, tbl), iinfo) ->
let tbl = Array.of_list tbl in
print_pref pp pref;
- fprintf pp "Bjumptable: (%a)\n" reg arg;
+ fprintf pp "%d: Bjumptable: (%a)\n" iinfo.inumb reg arg;
for i = 0 to Array.length tbl - 1 do
fprintf pp "\t\tcase %d: goto %d\n" i (P.to_int tbl.(i))
done
- | BF (Breturn None, _) ->
+ | BF (Breturn None, iinfo) ->
print_pref pp pref;
- fprintf pp "Breturn\n"
- | BF (Breturn (Some arg), _) ->
+ fprintf pp "%d: Breturn\n" iinfo.inumb
+ | BF (Breturn (Some arg), iinfo) ->
print_pref pp pref;
- fprintf pp "Breturn: %a\n" reg arg
- | BF (Bgoto s, _) ->
+ fprintf pp "%d: Breturn: %a\n" iinfo.inumb reg arg
+ | BF (Bgoto s, iinfo) ->
print_pref pp pref;
- fprintf pp "Bgoto: %d\n" (P.to_int s)
+ fprintf pp "%d: Bgoto: %d\n" iinfo.inumb (P.to_int s)
| Bseq (ib1, ib2) ->
if is_rec then (
print_iblock pp is_rec pref ib1;
print_iblock pp is_rec pref ib2)
else fprintf pp "Bseq...\n"
-let print_btl_inst pp ib = print_iblock pp false " " ib
+let print_btl_inst pp ib =
+ if !debug_flag then print_iblock pp false " " ib else ()
-let print_btl_code pp btl is_rec =
+let print_btl_code pp btl =
if !debug_flag then (
fprintf pp "\n";
List.iter
(fun (n, ibf) ->
- fprintf pp "[BTL Liveness]\n";
+ fprintf pp "[BTL Liveness] ";
print_regset ibf.input_regs;
- fprintf pp "[BTL block %d]\n" (P.to_int n);
- print_iblock pp is_rec " " ibf.entry;
+ fprintf pp "\n";
+ fprintf pp "[BTL block %d with inumb %d]\n" (P.to_int n) ibf.binfo.bnumb;
+ print_iblock pp true " " ibf.entry;
fprintf pp "\n")
(PTree.elements btl);
fprintf pp "\n")