Add printers for expressions and RTLPar

2 files changed, 114 insertions, 0 deletions

diff --git a/src/hls/PrintExpression.ml b/src/hls/PrintExpression.ml
new file mode 100644
index 0000000..cfe6750
--- /dev/null
+++ b/src/hls/PrintExpression.ml
@@ -0,0 +1,40 @@
+(*open Printf
+open Camlcoq
+open Datatypes
+open Maps
+open PrintAST
+open RTLPargen
+
+let reg pp r =
+  fprintf pp "x%d" (P.to_int r)
+
+let pred pp r =
+  fprintf pp "p%d" (P.to_int r)
+
+let print_resource pp = function
+  | Reg r -> reg pp r
+  | Pred r -> pred pp r
+  | Mem -> fprintf pp "M"
+
+let rec to_expr_list = function
+  | Enil -> []
+  | Econs (e, elist) -> e :: to_expr_list elist
+
+let rec print_expression pp = function
+  | Ebase r -> print_resource pp r
+  | Eop (op, elist, e) ->
+    PrintOp.print_operation print_expression pp (op, to_expr_list elist);
+    Printf.printf "; ";
+    print_expression pp e
+  | Eload (chunk, addr, elist, e) ->
+    fprintf pp "%s[%a]; " (name_of_chunk chunk) (PrintOp.print_addressing print_expression) (addr, to_expr_list elist);
+    print_expression pp e
+  | Estore (e, chunk, addr, elist, e') ->
+    fprintf pp "%s[%a] = %a; " (name_of_chunk chunk)
+      (PrintOp.print_addressing print_expression) (addr, to_expr_list elist)
+      print_expression e;
+    print_expression pp e
+  | Esetpred (p, cond, elist, e) ->
+    fprintf pp "%a = %a; " pred p (PrintOp.print_condition print_expression) (cond, to_expr_list elist);
+    print_expression pp e
+*)
diff --git a/src/hls/PrintRTLPar.ml b/src/hls/PrintRTLPar.ml
new file mode 100644
index 0000000..ab93fa5
--- /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 "{\n";
+              List.iter (fun x -> fprintf pp "( "; List.iter (print_bblock_body pp) x; fprintf pp " )") 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