Pretty-printers for RTL and LTL. Not yet well integrated.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1332 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

backend/PrintLTL.ml

+(* *********************************************************************)
+(*                                                                     *)
+(*              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
+
+

backend/PrintRTL.ml

+(* *********************************************************************)
+(*                                                                     *)
+(*              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
+
+

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)

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