Add RTLPar printing

5 files changed, 84 insertions, 4 deletions

diff --git a/driver/VericertDriver.ml b/driver/VericertDriver.ml
index d2c301f..4c1e2f9 100644
--- a/driver/VericertDriver.ml
+++ b/driver/VericertDriver.ml
@@ -66,6 +66,7 @@ let compile_c_file sourcename ifile ofile =
   set_dest Vericert.PrintCminor.destination option_dcminor ".cm";
   set_dest Vericert.PrintRTL.destination option_drtl ".rtl";
   set_dest Vericert.PrintRTLBlock.destination option_drtlblock ".rtlblock";
+  set_dest Vericert.PrintRTLPar.destination option_drtlpar ".rtlpar";
   set_dest Vericert.PrintHTL.destination option_dhtl ".htl";
   set_dest Vericert.Regalloc.destination_alloctrace option_dalloctrace ".alloctrace";
   set_dest Vericert.PrintLTL.destination option_dltl ".ltl";
@@ -390,6 +391,7 @@ let cmdline_actions =
   Exact "-dcminor", Set option_dcminor;
   Exact "-drtl", Set option_drtl;
   Exact "-drtlblock", Set option_drtlblock;
+  Exact "-drtlpar", Set option_drtlpar;
   Exact "-dhtl", Set option_dhtl;
   Exact "-dltl", Set option_dltl;
   Exact "-dalloctrace", Set option_dalloctrace;
@@ -403,6 +405,7 @@ let cmdline_actions =
     option_dcminor := true;
     option_drtl := true;
     option_drtlblock := true;
+    option_drtlpar := true;
     option_dhtl := true;
     option_dltl := true;
     option_dalloctrace := true;
@@ -417,10 +420,10 @@ let cmdline_actions =
   warning_options @
 (* Vericert.Interpreter mode *)
  [ Exact "-interp", Set option_interp;
-  Exact "-quiet", Unit (fun () -> Vericert.Interp.trace := 0);
-  Exact "-trace", Unit (fun () -> Vericert.Interp.trace := 2);
-  Exact "-random", Unit (fun () -> Vericert.Interp.mode := Vericert.Interp.Random);
-  Exact "-all", Unit (fun () -> Vericert.Interp.mode := Vericert.Interp.All)
+   Exact "-quiet", Unit (fun () -> Vericert.Interp.trace := 0);
+   Exact "-trace", Unit (fun () -> Vericert.Interp.trace := 2);
+   Exact "-random", Unit (fun () -> Vericert.Interp.mode := Vericert.Interp.Random);
+   Exact "-all", Unit (fun () -> Vericert.Interp.mode := Vericert.Interp.All)
  ]
 (* Optimization options *)
 (* -f options: come in -f and -fno- variants *)
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