oracle simplification, BTL printer, and error msg spec

1 files changed, 107 insertions, 0 deletions

diff --git a/scheduling/PrintBTL.ml b/scheduling/PrintBTL.ml
new file mode 100644
index 00000000..8f61380e
--- /dev/null
+++ b/scheduling/PrintBTL.ml
@@ -0,0 +1,107 @@
+open Printf
+open Camlcoq
+open Datatypes
+open Maps
+open AST
+open BTL
+open PrintAST
+
+(* Printing of BTL 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_succ pp s =
+  fprintf pp "\tsucc %d\n" (P.to_int s)
+
+let rec print_iblock pp is_rec pref ib =
+  fprintf pp "%s" pref;
+  match ib with
+  | Bnop ->
+      fprintf pp "Bnop\n"
+  | Bop(op, args, res) ->
+      fprintf pp "Bop: %a = %a\n"
+         reg res (PrintOp.print_operation reg) (op, args)
+  | Bload(trap, chunk, addr, args, dst) ->
+      fprintf pp "Bload: %a = %s[%a]%a\n"
+         reg dst (name_of_chunk chunk)
+         (PrintOp.print_addressing reg) (addr, args)
+         print_trapping_mode trap
+  | Bstore(chunk, addr, args, src) ->
+      fprintf pp "Bstore: %s[%a] = %a\n"
+         (name_of_chunk chunk)
+         (PrintOp.print_addressing reg) (addr, args)
+         reg src
+  | BF (Bcall(sg, fn, args, res, s)) ->
+      fprintf pp "Bcall: %a = %a(%a)\n"
+        reg res ros fn regs args;
+      print_succ pp s
+  | BF (Btailcall(sg, fn, args)) ->
+      fprintf pp "Btailcall: %a(%a)\n"
+        ros fn regs args
+  | BF (Bbuiltin(ef, args, res, s)) ->
+      fprintf pp "Bbuiltin: %a = %s(%a)\n"
+        (print_builtin_res reg) res
+        (name_of_external ef)
+        (print_builtin_args reg) args;
+      print_succ pp s
+  | Bcond(cond, args, ib1, ib2, info) ->
+      fprintf pp "Bcond: (%a) (prediction: %s)\n"
+        (PrintOp.print_condition reg) (cond, args)
+        (match info with None -> "none" | Some true -> "branch" | Some false -> "fallthrough");
+        let pref' = pref ^ "  " in
+        fprintf pp "%sifso = [\n" pref;
+        if is_rec then print_iblock pp is_rec pref' ib1 else fprintf pp "...\n";
+        fprintf pp "%s]\n" pref;
+        fprintf pp "%sifnot = [\n" pref;
+        if is_rec then print_iblock pp is_rec pref' ib2 else fprintf pp "...\n";
+        fprintf pp "%s]\n" pref
+  | BF (Bjumptable(arg, tbl)) ->
+      let tbl = Array.of_list tbl in
+      fprintf pp "Bjumptable: (%a)\n" reg arg;
+      for i = 0 to Array.length tbl - 1 do
+        fprintf pp "\t\tcase %d: goto %d\n" i (P.to_int tbl.(i))
+      done
+  | BF (Breturn None) ->
+      fprintf pp "Breturn\n"
+  | BF (Breturn (Some arg)) ->
+      fprintf pp "Breturn: %a\n" reg arg
+  | BF (Bgoto s) ->
+      fprintf pp "Bgoto: %d\n" (P.to_int s)
+  | Bseq (ib1, ib2) ->
+      if is_rec then (
+        print_iblock pp is_rec pref ib1;
+        print_iblock pp is_rec pref ib2)
+      else fprintf pp "Bseq...\n"
+
+let print_btl_code pp btl is_rec =
+  fprintf pp "\n";
+  List.iter (fun (n,ibf) ->
+    fprintf pp "[BTL block %d]\n" (P.to_int n);
+    print_iblock pp is_rec "  " ibf.entry;
+    fprintf pp "\n")
+  (PTree.elements btl);
+  fprintf pp "\n"
+
+let print_function pp id f =
+  fprintf pp "%s(%a) {\n" (extern_atom id) regs f.fn_params;
+  let instrs = List.map (fun (n,i) -> i.entry) (PTree.elements f.fn_code) in
+  List.iter (print_iblock pp true "") 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: BTL.program) =
+  List.iter (print_globdef pp) prog.prog_defs