diff options
author | Yann Herklotz <git@yannherklotz.com> | 2021-02-22 18:41:33 +0000 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2021-02-22 18:41:33 +0000 |
commit | 91b62a7100ccb1f8910422bc4566bc57ade8f7e7 (patch) | |
tree | 5987436a23f446a42672061b7d8740b3a2775403 /src | |
parent | a5ae227155f09822207c49d75fdbb6e4b7652936 (diff) | |
download | vericert-91b62a7100ccb1f8910422bc4566bc57ade8f7e7.tar.gz vericert-91b62a7100ccb1f8910422bc4566bc57ade8f7e7.zip |
Add RTLPar printing
Diffstat (limited to 'src')
-rw-r--r-- | src/Compiler.v | 1 | ||||
-rw-r--r-- | src/VericertClflags.ml | 1 | ||||
-rw-r--r-- | src/extraction/Extraction.v | 1 | ||||
-rw-r--r-- | src/hls/printRTLPar.ml | 74 |
4 files changed, 77 insertions, 0 deletions
diff --git a/src/Compiler.v b/src/Compiler.v index d99ce56..e837e9d 100644 --- a/src/Compiler.v +++ b/src/Compiler.v @@ -82,6 +82,7 @@ We then need to declare the external OCaml functions used to print out intermedi Parameter print_RTL: Z -> RTL.program -> unit. Parameter print_HTL: HTL.program -> unit. Parameter print_RTLBlock: Z -> RTLBlock.program -> unit. +Parameter print_RTLPar: Z -> RTLPar.program -> unit. Definition print {A: Type} (printer: A -> unit) (prog: A) : A := let unused := printer prog in prog. diff --git a/src/VericertClflags.ml b/src/VericertClflags.ml index 534962b..930b613 100644 --- a/src/VericertClflags.ml +++ b/src/VericertClflags.ml @@ -5,5 +5,6 @@ let option_debug_hls = ref false let option_initial = ref false let option_dhtl = ref false let option_drtlblock = ref false +let option_drtlpar = ref false let option_hls_schedule = ref false let option_fif_conv = ref false diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v index 8aec96e..5c1dac5 100644 --- a/src/extraction/Extraction.v +++ b/src/extraction/Extraction.v @@ -141,6 +141,7 @@ Extract Constant Compiler.print_Cminor => "PrintCminor.print_if". Extract Constant driver.Compiler.print_RTL => "PrintRTL.print_if". Extract Constant Compiler.print_RTL => "PrintRTL.print_if". Extract Constant Compiler.print_RTLBlock => "PrintRTLBlock.print_if". +Extract Constant Compiler.print_RTLPar => "PrintRTLPar.print_if". Extract Constant Compiler.print_HTL => "PrintHTL.print_if". Extract Constant Compiler.print_LTL => "PrintLTL.print_if". Extract Constant Compiler.print_Mach => "PrintMach.print_if". diff --git a/src/hls/printRTLPar.ml b/src/hls/printRTLPar.ml new file mode 100644 index 0000000..7fac0de --- /dev/null +++ b/src/hls/printRTLPar.ml @@ -0,0 +1,74 @@ +(* *********************************************************************) +(* *) +(* 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 RTLBlockInstr +open RTLPar +open PrintAST +open PrintRTLBlockInstr + +(* 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 pp (pc, i) = + fprintf pp "%5d:{\n" pc; + List.iter (fun x -> fprintf pp "["; + List.iter (fun x' -> fprintf pp "["; List.iter (print_bblock_body pp) x'; fprintf pp "]\n") x; + fprintf pp "]\n") 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 passno prog = + match !destination with + | None -> () + | Some f -> + let oc = open_out (f ^ "." ^ Z.to_string passno) in + print_program oc prog; + close_out oc |