diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-05-08 08:39:30 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-05-08 08:39:30 +0000 |
commit | fb202a70ccc2872aa3849854c09810a6bee268e5 (patch) | |
tree | 1b2fa2f5fa1c7f84ff7589f778985a0db306d845 /backend/PrintMach.ml | |
parent | c45fc2431ea70e0cb5a80e65d0ac99f91e94693e (diff) |
powerpc/PrintAsm.ml arm/PrintAsm.ml: updated (no label elimination).
Added -dmach option and corresponding printer for Mach code.
CleanupLabelsproof.v: fixed for ARM
Driver.ml: -E sends output to stdout; support for .s and .S source files.
cparser/Elab.ml: spurious comment deleted.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1648 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend/PrintMach.ml')
-rw-r--r-- | backend/PrintMach.ml | 126 |
1 files changed, 126 insertions, 0 deletions
diff --git a/backend/PrintMach.ml b/backend/PrintMach.ml new file mode 100644 index 0000000..5b4887e --- /dev/null +++ b/backend/PrintMach.ml @@ -0,0 +1,126 @@ +(* *********************************************************************) +(* *) +(* 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-printer for Mach code *) + +open Format +open Camlcoq +open Datatypes +open Maps +open AST +open Integers +open Locations +open Machregsaux +open Mach +open PrintOp + +let name_of_chunk = function + | Mint8signed -> "int8signed" + | Mint8unsigned -> "int8unsigned" + | Mint16signed -> "int16signed" + | Mint16unsigned -> "int16unsigned" + | Mint32 -> "int32" + | Mfloat32 -> "float32" + | Mfloat64 -> "float64" + +let name_of_type = function + | Tint -> "int" + | Tfloat -> "float" + +let reg pp r = + match name_of_register r with + | Some s -> fprintf pp "%s" s + | None -> fprintf pp "<unknown reg>" + +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_instruction pp i = + match i with + | Mgetstack(ofs, ty, res) -> + fprintf pp "%a = stack(%ld, %s)@ " + reg res (camlint_of_coqint ofs) (name_of_type ty) + | Msetstack(arg, ofs, ty) -> + fprintf pp "stack(%ld, %s) = %a@ " + (camlint_of_coqint ofs) (name_of_type ty) reg arg + | Mgetparam(ofs, ty, res) -> + fprintf pp "%a = param(%ld, %s)@ " + reg res (camlint_of_coqint ofs) (name_of_type ty) + | Mop(op, args, res) -> + fprintf pp "%a = %a@ " + reg res (PrintOp.print_operation reg) (op, args) + | Mload(chunk, addr, args, dst) -> + fprintf pp "%a = %s[%a]@ " + reg dst (name_of_chunk chunk) + (PrintOp.print_addressing reg) (addr, args) + | Mstore(chunk, addr, args, src) -> + fprintf pp "%s[%a] = %a@ " + (name_of_chunk chunk) + (PrintOp.print_addressing reg) (addr, args) + reg src + | Mcall(sg, fn) -> + fprintf pp "call %a@ " ros fn + | Mtailcall(sg, fn) -> + fprintf pp "tailcall %a@ " ros fn + | Mbuiltin(ef, args, res) -> + fprintf pp "%a = builtin \"%s\"(%a)@ " + reg res (extern_atom ef.ef_id) regs args + | Mlabel lbl -> + fprintf pp "%ld:@ " (camlint_of_positive lbl) + | Mgoto lbl -> + fprintf pp "goto %ld@ " (camlint_of_positive lbl) + | Mcond(cond, args, lbl) -> + fprintf pp "if (%a) goto %ld@ " + (PrintOp.print_condition reg) (cond, args) + (camlint_of_positive lbl) + | Mjumptable(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 "@]@ " + | Mreturn -> + fprintf pp "return@ " + +let print_function pp f = + fprintf pp "@[<v 2>f() {@ "; + List.iter (print_instruction pp) f.fn_code; + fprintf pp "@;<0 -2>}@]@." + +let print_fundef pp fd = + match fd with + | Internal f -> print_function pp f + | External _ -> () + +let destination : string option ref = ref None +let currpp : formatter option ref = ref None + +let print_if fd = + match !destination with + | None -> () + | Some f -> + let pp = + match !currpp with + | Some pp -> pp + | None -> + let oc = open_out f in + let pp = formatter_of_out_channel oc in + currpp := Some pp; + pp + in print_fundef pp fd |