From e96b2dd600239a44b5d857d23dfacd4733583fe4 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sun, 2 May 2010 07:46:23 +0000
Subject: 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 | 117 ++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 117 insertions(+)
 create mode 100644 backend/PrintLTL.ml

(limited to 'backend/PrintLTL.ml')

diff --git a/backend/PrintLTL.ml b/backend/PrintLTL.ml
new file mode 100644
index 00000000..cce00f63
--- /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
+
+
-- 
cgit