diff options
author | Yann Herklotz <git@yannherklotz.com> | 2020-08-31 22:37:44 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2020-08-31 22:37:44 +0100 |
commit | b431bdeb59e69df41cd98fadea49968d224493ee (patch) | |
tree | 2432959ca65908e7c5573d1c87a43be2e8d2d4b4 /src/hls/PrintRTLBlock.ml | |
parent | 6cb38f39f5609651691419c6a299b09695a4623c (diff) | |
download | vericert-b431bdeb59e69df41cd98fadea49968d224493ee.tar.gz vericert-b431bdeb59e69df41cd98fadea49968d224493ee.zip |
Add working partitioning algorithm
Diffstat (limited to 'src/hls/PrintRTLBlock.ml')
-rw-r--r-- | src/hls/PrintRTLBlock.ml | 119 |
1 files changed, 119 insertions, 0 deletions
diff --git a/src/hls/PrintRTLBlock.ml b/src/hls/PrintRTLBlock.ml index e69de29..45bd253 100644 --- a/src/hls/PrintRTLBlock.ml +++ b/src/hls/PrintRTLBlock.ml @@ -0,0 +1,119 @@ +(* *********************************************************************) +(* *) +(* 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 Printf +open Camlcoq +open Datatypes +open Maps +open AST +open RTLBlock +open PrintAST + +(* Printing of RTL code *) + +let reg pp r = + fprintf pp "x%d" (P.to_int 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_bblock_body pp i = + fprintf pp "\t\t"; + match i with + | RBnop -> fprintf pp "nop\n" + | RBop(op, ls, dst) -> + fprintf pp "%a = %a\n" + reg dst (PrintOp.print_operation reg) (op, ls) + | RBload(chunk, addr, args, dst) -> + fprintf pp "%a = %s[%a]\n" + reg dst (name_of_chunk chunk) + (PrintOp.print_addressing reg) (addr, args) + | RBstore(chunk, addr, args, src) -> + fprintf pp "%s[%a] = %a\n" + (name_of_chunk chunk) + (PrintOp.print_addressing reg) (addr, args) + reg src + +let print_bblock_exit pp i = + fprintf pp "\t\t"; + match i with + | Some(RBcall(_, fn, args, res, _)) -> + fprintf pp "%a = %a(%a)\n" + reg res ros fn regs args; + | Some(RBtailcall(_, fn, args)) -> + fprintf pp "tailcall %a(%a)\n" + ros fn regs args + | Some(RBbuiltin(ef, args, res, _)) -> + fprintf pp "%a = %s(%a)\n" + (print_builtin_res reg) res + (name_of_external ef) + (print_builtin_args reg) args + | Some(RBcond(cond, args, s1, s2)) -> + fprintf pp "if (%a) goto %d else goto %d\n" + (PrintOp.print_condition reg) (cond, args) + (P.to_int s1) (P.to_int s2) + | Some(RBjumptable(arg, tbl)) -> + let tbl = Array.of_list tbl in + fprintf pp "jumptable (%a)\n" reg arg; + for i = 0 to Array.length tbl - 1 do + fprintf pp "\tcase %d: goto %d\n" i (P.to_int tbl.(i)) + done + | Some(RBreturn None) -> + fprintf pp "return\n" + | Some(RBreturn (Some arg)) -> + fprintf pp "return %a\n" reg arg + | Some(RBgoto n) -> + fprintf pp "goto %d\n" (P.to_int n) + | None -> fprintf pp "\n" + +let print_bblock pp (pc, i) = + fprintf pp "%5d:{\n" pc; + List.iter (print_bblock_body pp) i.bb_body; + print_bblock_exit pp i.bb_exit; + fprintf pp "\t}\n\n" + +let print_function pp id f = + fprintf pp "%s(%a) {\n" (extern_atom id) regs f.fn_params; + let instrs = + List.sort + (fun (pc1, _) (pc2, _) -> compare pc2 pc1) + (List.rev_map + (fun (pc, i) -> (P.to_int pc, i)) + (PTree.elements f.fn_code)) in + List.iter (print_bblock pp) instrs; + fprintf pp "}\n\n" + +let print_globdef pp (id, gd) = + match gd with + | Gfun(Internal f) -> print_function pp id f + | _ -> () + +let print_program pp (prog: program) = + List.iter (print_globdef pp) prog.prog_defs + +let destination : string option ref = ref None + +let print_if prog = + match !destination with + | None -> () + | Some f -> + let oc = open_out f in + print_program oc prog; + close_out oc |