summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--backend/PrintLTL.ml117
-rw-r--r--backend/PrintRTL.ml111
-rw-r--r--powerpc/Machregsaux.ml6
-rw-r--r--powerpc/Machregsaux.mli1
4 files changed, 235 insertions, 0 deletions
diff --git a/backend/PrintLTL.ml b/backend/PrintLTL.ml
new file mode 100644
index 0000000..cce00f6
--- /dev/null
+++ b/backend/PrintLTL.ml
@@ -0,0 +1,117 @@
+(* *********************************************************************)
+(* *)
+(* The Compcert verified compiler *)
+(* *)
+(* Xavier Leroy, INRIA Paris-Rocquencourt *)
+(* *)
+(* Copyright Institut National de Recherche en Informatique et en *)
+(* Automatique. All rights reserved. This file is distributed *)
+(* under the terms of the INRIA Non-Commercial License Agreement. *)
+(* *)
+(* *********************************************************************)
+
+(** Pretty-printers for RTL code *)
+
+open Format
+open Camlcoq
+open Datatypes
+open Maps
+open AST
+open Integers
+open Locations
+open LTL
+open PrintOp
+open PrintRTL
+
+let name_of_typ = function Tint -> "int" | Tfloat -> "float"
+
+let loc pp l =
+ match l with
+ | R r ->
+ begin match Machregsaux.name_of_register r with
+ | Some s -> fprintf pp "%s" s
+ | None -> fprintf pp "<unknown machreg>"
+ end
+ | S(Local(ofs, ty)) ->
+ fprintf pp "local(%ld,%s)" (camlint_of_coqint ofs) (name_of_typ ty)
+ | S(Incoming(ofs, ty)) ->
+ fprintf pp "incoming(%ld,%s)" (camlint_of_coqint ofs) (name_of_typ ty)
+ | S(Outgoing(ofs, ty)) ->
+ fprintf pp "outgoing(%ld,%s)" (camlint_of_coqint ofs) (name_of_typ ty)
+
+let rec locs pp = function
+ | [] -> ()
+ | [r] -> loc pp r
+ | r1::rl -> fprintf pp "%a, %a" loc r1 locs rl
+
+let ros pp = function
+ | Coq_inl r -> loc pp r
+ | Coq_inr s -> fprintf pp "\"%s\"" (extern_atom s)
+
+let print_succ pp s dfl =
+ let s = camlint_of_positive s in
+ if s <> dfl then fprintf pp " goto %ld@ " s
+
+let print_instruction pp (pc, i) =
+ fprintf pp "%5ld: " pc;
+ match i with
+ | Lnop s ->
+ let s = camlint_of_positive s in
+ if s = Int32.pred pc
+ then fprintf pp "nop@ "
+ else fprintf pp "goto %ld@ " s
+ | Lop(op, args, res, s) ->
+ fprintf pp "%a = %a@ " loc res (print_operator loc) (op, args);
+ print_succ pp s (Int32.pred pc)
+ | Lload(chunk, addr, args, dst, s) ->
+ fprintf pp "%a = %s[%a]@ "
+ loc dst (name_of_chunk chunk) (print_addressing loc) (addr, args);
+ print_succ pp s (Int32.pred pc)
+ | Lstore(chunk, addr, args, src, s) ->
+ fprintf pp "%s[%a] = %a@ "
+ (name_of_chunk chunk) (print_addressing loc) (addr, args) loc src;
+ print_succ pp s (Int32.pred pc)
+ | Lcall(sg, fn, args, res, s) ->
+ fprintf pp "%a = %a(%a)@ "
+ loc res ros fn locs args;
+ print_succ pp s (Int32.pred pc)
+ | Ltailcall(sg, fn, args) ->
+ fprintf pp "tailcall %a(%a)@ "
+ ros fn locs args
+ | Lcond(cond, args, s1, s2) ->
+ fprintf pp "if (%a) goto %ld else goto %ld@ "
+ (print_condition loc) (cond, args)
+ (camlint_of_positive s1) (camlint_of_positive s2)
+ | Ljumptable(arg, tbl) ->
+ let tbl = Array.of_list tbl in
+ fprintf pp "@[<v 2>jumptable (%a)" loc arg;
+ for i = 0 to Array.length tbl - 1 do
+ fprintf pp "@ case %d: goto %ld" i (camlint_of_positive tbl.(i))
+ done;
+ fprintf pp "@]@ "
+ | Lreturn None ->
+ fprintf pp "return@ "
+ | Lreturn (Some arg) ->
+ fprintf pp "return %a@ " loc arg
+
+let print_function pp f =
+ fprintf pp "@[<v 2>f(%a) {@ " locs f.fn_params;
+ let instrs =
+ List.sort
+ (fun (pc1, _) (pc2, _) -> Pervasives.compare pc2 pc1)
+ (List.map
+ (fun (Coq_pair(pc, i)) -> (camlint_of_positive pc, i))
+ (PTree.elements f.fn_code)) in
+ print_succ pp f.fn_entrypoint
+ (match instrs with (pc1, _) :: _ -> pc1 | [] -> -1l);
+ List.iter (print_instruction pp) instrs;
+ fprintf pp "@;<0 -2>}@]@."
+
+let print_fundef fd =
+ begin match fd with
+ | Internal f -> print_function std_formatter f
+ | External _ -> ()
+ end;
+ fd
+
+
diff --git a/backend/PrintRTL.ml b/backend/PrintRTL.ml
new file mode 100644
index 0000000..6e8c578
--- /dev/null
+++ b/backend/PrintRTL.ml
@@ -0,0 +1,111 @@
+(* *********************************************************************)
+(* *)
+(* The Compcert verified compiler *)
+(* *)
+(* Xavier Leroy, INRIA Paris-Rocquencourt *)
+(* *)
+(* Copyright Institut National de Recherche en Informatique et en *)
+(* Automatique. All rights reserved. This file is distributed *)
+(* under the terms of the INRIA Non-Commercial License Agreement. *)
+(* *)
+(* *********************************************************************)
+
+(** Pretty-printers for RTL code *)
+
+open Format
+open Camlcoq
+open Datatypes
+open Maps
+open AST
+open Integers
+open RTL
+open PrintOp
+
+let name_of_chunk = function
+ | Mint8signed -> "int8signed"
+ | Mint8unsigned -> "int8unsigned"
+ | Mint16signed -> "int16signed"
+ | Mint16unsigned -> "int16unsigned"
+ | Mint32 -> "int32"
+ | Mfloat32 -> "float32"
+ | Mfloat64 -> "float64"
+
+let reg pp r =
+ fprintf pp "x%ld" (camlint_of_positive r)
+
+let rec regs pp = function
+ | [] -> ()
+ | [r] -> reg pp r
+ | r1::rl -> fprintf pp "%a, %a" reg r1 regs rl
+
+let ros pp = function
+ | Coq_inl r -> reg pp r
+ | Coq_inr s -> fprintf pp "\"%s\"" (extern_atom s)
+
+let print_succ pp s dfl =
+ let s = camlint_of_positive s in
+ if s <> dfl then fprintf pp " goto %ld@ " s
+
+let print_instruction pp (pc, i) =
+ fprintf pp "%5ld: " pc;
+ match i with
+ | Inop s ->
+ let s = camlint_of_positive s in
+ if s = Int32.pred pc
+ then fprintf pp "nop@ "
+ else fprintf pp "goto %ld@ " s
+ | Iop(op, args, res, s) ->
+ fprintf pp "%a = %a@ " reg res (print_operator reg) (op, args);
+ print_succ pp s (Int32.pred pc)
+ | Iload(chunk, addr, args, dst, s) ->
+ fprintf pp "%a = %s[%a]@ "
+ reg dst (name_of_chunk chunk) (print_addressing reg) (addr, args);
+ print_succ pp s (Int32.pred pc)
+ | Istore(chunk, addr, args, src, s) ->
+ fprintf pp "%s[%a] = %a@ "
+ (name_of_chunk chunk) (print_addressing reg) (addr, args) reg src;
+ print_succ pp s (Int32.pred pc)
+ | Icall(sg, fn, args, res, s) ->
+ fprintf pp "%a = %a(%a)@ "
+ reg res ros fn regs args;
+ print_succ pp s (Int32.pred pc)
+ | Itailcall(sg, fn, args) ->
+ fprintf pp "tailcall %a(%a)@ "
+ ros fn regs args
+ | Icond(cond, args, s1, s2) ->
+ fprintf pp "if (%a) goto %ld else goto %ld@ "
+ (print_condition reg) (cond, args)
+ (camlint_of_positive s1) (camlint_of_positive s2)
+ | Ijumptable(arg, tbl) ->
+ let tbl = Array.of_list tbl in
+ fprintf pp "@[<v 2>jumptable (%a)" reg arg;
+ for i = 0 to Array.length tbl - 1 do
+ fprintf pp "@ case %d: goto %ld" i (camlint_of_positive tbl.(i))
+ done;
+ fprintf pp "@]@ "
+ | Ireturn None ->
+ fprintf pp "return@ "
+ | Ireturn (Some arg) ->
+ fprintf pp "return %a@ " reg arg
+
+let print_function pp f =
+ fprintf pp "@[<v 2>f(%a) {@ " regs f.fn_params;
+ let instrs =
+ List.sort
+ (fun (pc1, _) (pc2, _) -> Pervasives.compare pc2 pc1)
+ (List.map
+ (fun (Coq_pair(pc, i)) -> (camlint_of_positive pc, i))
+ (PTree.elements f.fn_code)) in
+ print_succ pp f.fn_entrypoint
+ (match instrs with (pc1, _) :: _ -> pc1 | [] -> -1l);
+ List.iter (print_instruction pp) instrs;
+ fprintf pp "@;<0 -2>}@]@."
+
+let print_fundef fd =
+ begin match fd with
+ | Internal f -> print_function std_formatter f
+ | External _ -> ()
+ end;
+ fd
+
+
diff --git a/powerpc/Machregsaux.ml b/powerpc/Machregsaux.ml
index b729d10..2ff3cd9 100644
--- a/powerpc/Machregsaux.ml
+++ b/powerpc/Machregsaux.ml
@@ -33,6 +33,12 @@ let register_names = [
("F11", FT1); ("F12", FT2); ("F0", FT3)
]
+let name_of_register r =
+ let rec rev_assoc = function
+ | [] -> None
+ | (a, b) :: rem -> if b = r then Some a else rev_assoc rem
+ in rev_assoc register_names
+
let register_by_name s =
try
Some(List.assoc (String.uppercase s) register_names)
diff --git a/powerpc/Machregsaux.mli b/powerpc/Machregsaux.mli
index 6d81988..400c5ab 100644
--- a/powerpc/Machregsaux.mli
+++ b/powerpc/Machregsaux.mli
@@ -14,3 +14,4 @@
val register_by_name: string -> Machregs.mreg option
val can_reserve_register: Machregs.mreg -> bool
+val name_of_register: Machregs.mreg -> string option
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-12 01:10:59 +0000