From 255cee09b71255051c2b40eae0c88bffce1f6f32 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 20 Apr 2013 07:54:52 +0000 Subject: Big merge of the newregalloc-int64 branch. Lots of changes in two directions: 1- new register allocator (+ live range splitting, spilling&reloading, etc) based on a posteriori validation using the Rideau-Leroy algorithm 2- support for 64-bit integer arithmetic (type "long long"). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2200 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/PrintXTL.ml | 147 ++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 147 insertions(+) create mode 100644 backend/PrintXTL.ml (limited to 'backend/PrintXTL.ml') diff --git a/backend/PrintXTL.ml b/backend/PrintXTL.ml new file mode 100644 index 00000000..756fc58c --- /dev/null +++ b/backend/PrintXTL.ml @@ -0,0 +1,147 @@ +(* *********************************************************************) +(* *) +(* 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 XTL *) + +open Format +open Camlcoq +open Datatypes +open Maps +open AST +open Registers +open Op +open Locations +open PrintAST +open PrintOp +open XTL + +let mreg pp r = + match Machregsaux.name_of_register r with + | Some s -> fprintf pp "%s" s + | None -> fprintf pp "" + +let short_name_of_type = function Tint -> 'i' | Tfloat -> 'f' | Tlong -> 'l' + +let loc pp = function + | R r -> mreg pp r + | S(Local, ofs, ty) -> + fprintf pp "L%c%ld" (short_name_of_type ty) (camlint_of_coqint ofs) + | S(Incoming, ofs, ty) -> + fprintf pp "I%c%ld" (short_name_of_type ty) (camlint_of_coqint ofs) + | S(Outgoing, ofs, ty) -> + fprintf pp "O%c%ld" (short_name_of_type ty) (camlint_of_coqint ofs) + +let current_alloc = ref (None: (var -> loc) option) +let current_liveness = ref (None: VSet.t PMap.t option) + +let reg pp r ty = + match !current_alloc with + | None -> fprintf pp "x%ld" (P.to_int32 r) + | Some alloc -> fprintf pp "x%ld{%a}" (P.to_int32 r) loc (alloc (V(r, ty))) + +let var pp = function + | V(r, ty) -> reg pp r ty + | L l -> loc pp l + +let rec vars pp = function + | [] -> () + | [r] -> var pp r + | r1::rl -> fprintf pp "%a, %a" var r1 vars rl + +let ros pp = function + | Coq_inl r -> var pp r + | Coq_inr s -> fprintf pp "\"%s\"" (extern_atom s) + +let liveset pp lv = + fprintf pp "@[{"; + VSet.iter (function V(r, ty) -> fprintf pp "@ x%ld" (P.to_int32 r) + | L l -> ()) + lv; + fprintf pp " }@]" + +let print_succ pp s dfl = + let s = P.to_int32 s in + if s <> dfl then fprintf pp "goto %ld" s + +let print_instruction pp succ = function + | Xmove(src, dst) -> + fprintf pp "%a = %a;" var dst var src + | Xreload(src, dst) -> + fprintf pp "%a =r %a;" var dst var src + | Xspill(src, dst) -> + fprintf pp "%a =s %a;" var dst var src + | Xparmove(srcs, dsts, t1, t2) -> + fprintf pp "(%a) = (%a) using %a, %a;" vars dsts vars srcs var t1 var t2 + | Xop(op, args, res) -> + fprintf pp "%a = %a;" var res (print_operation var) (op, args) + | Xload(chunk, addr, args, dst) -> + fprintf pp "%a = %s[%a];" + var dst (name_of_chunk chunk) (print_addressing var) (addr, args) + | Xstore(chunk, addr, args, src) -> + fprintf pp "%s[%a] = %a;" + (name_of_chunk chunk) (print_addressing var) (addr, args) var src + | Xcall(sg, fn, args, res) -> + fprintf pp "%a = call %a(%a);" vars res ros fn vars args + | Xtailcall(sg, fn, args) -> + fprintf pp "tailcall %a(%a);" ros fn vars args + | Xbuiltin(ef, args, res) -> + fprintf pp "%a = builtin %s(%a);" + vars res (name_of_external ef) vars args + | Xbranch s -> + print_succ pp s succ + | Xcond(cond, args, s1, s2) -> + fprintf pp "if (%a) goto %ld else goto %ld" + (print_condition var) (cond, args) + (P.to_int32 s1) (P.to_int32 s2) + | Xjumptable(arg, tbl) -> + let tbl = Array.of_list tbl in + fprintf pp "@[jumptable (%a)" var arg; + for i = 0 to Array.length tbl - 1 do + fprintf pp "@ case %d: goto %ld" i (P.to_int32 tbl.(i)) + done; + fprintf pp "@]" + | Xreturn args -> + fprintf pp "return %a" vars args + +let rec print_instructions pp succ = function + | [] -> () + | [i] -> print_instruction pp succ i + | i :: il -> + print_instruction pp succ i; + fprintf pp "@ "; + print_instructions pp succ il + +let print_block pp (pc, blk) = + fprintf pp "%5ld: @[" pc; + print_instructions pp (Int32.pred pc) blk; + fprintf pp "@]@ "; + match !current_liveness with + | None -> () + | Some liveness -> fprintf pp "%a@ " liveset (PMap.get (P.of_int32 pc) liveness) + +let print_function pp ?alloc ?live f = + current_alloc := alloc; + current_liveness := live; + fprintf pp "@[f() {@ "; + let instrs = + List.sort + (fun (pc1, _) (pc2, _) -> Pervasives.compare pc2 pc1) + (List.map + (fun (pc, i) -> (P.to_int32 pc, i)) + (PTree.elements f.fn_code)) in + print_succ pp f.fn_entrypoint + (match instrs with (pc1, _) :: _ -> pc1 | [] -> -1l); + List.iter (print_block pp) instrs; + fprintf pp "@;<0 -2>}@]@."; + current_alloc := None; + current_liveness := None + -- cgit