diff options
author | Yann Herklotz <git@yannherklotz.com> | 2021-01-31 15:43:50 +0000 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2021-01-31 15:43:50 +0000 |
commit | 3b77ad9c0f3c52ba1cc02f954ee5bc2b63f51366 (patch) | |
tree | b142b028d1e8814e86db9f21f6ae8ddebe002f5f /src/hls/PrintRTLBlock.ml | |
parent | d2a3355b00ad5edfd4de4627df0cf45830114ac5 (diff) | |
download | vericert-3b77ad9c0f3c52ba1cc02f954ee5bc2b63f51366.tar.gz vericert-3b77ad9c0f3c52ba1cc02f954ee5bc2b63f51366.zip |
Fix OCaml files for compilation
Diffstat (limited to 'src/hls/PrintRTLBlock.ml')
-rw-r--r-- | src/hls/PrintRTLBlock.ml | 51 |
1 files changed, 2 insertions, 49 deletions
diff --git a/src/hls/PrintRTLBlock.ml b/src/hls/PrintRTLBlock.ml index 45bd253..caf64ff 100644 --- a/src/hls/PrintRTLBlock.ml +++ b/src/hls/PrintRTLBlock.ml @@ -17,8 +17,10 @@ open Camlcoq open Datatypes open Maps open AST +open RTLBlockInstr open RTLBlock open PrintAST +open PrintRTLBlockInstr (* Printing of RTL code *) @@ -34,55 +36,6 @@ 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; |