Adding a BTL record to help oracles

1 files changed, 52 insertions, 58 deletions

diff --git a/scheduling/PrintBTL.ml b/scheduling/PrintBTL.ml
index b461e3f1..4b14d28e 100644
--- a/scheduling/PrintBTL.ml
+++ b/scheduling/PrintBTL.ml
@@ -8,84 +8,80 @@ open PrintAST
 
 (* Printing of BTL code *)
 
-let reg pp r =
-  fprintf pp "x%d" (P.to_int r)
+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
+  | [ 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 print_succ pp s = fprintf pp "\tsucc %d\n" (P.to_int s)
 
-let print_pref pp pref =
-  fprintf pp "%s" pref
+let print_pref pp pref = fprintf pp "%s" pref
 
 let rec print_iblock pp is_rec pref ib =
   match ib with
-  | Bnop ->
+  | Bnop _ ->
       print_pref pp pref;
       fprintf pp "Bnop\n"
-  | Bop(op, args, res) ->
+  | Bop (op, args, res, _) ->
       print_pref pp pref;
-      fprintf pp "Bop: %a = %a\n"
-         reg res (PrintOp.print_operation reg) (op, args)
-  | Bload(trap, chunk, addr, args, dst) ->
+      fprintf pp "Bop: %a = %a\n" reg res
+        (PrintOp.print_operation reg)
+        (op, args)
+  | Bload (trap, chunk, addr, args, dst, _) ->
       print_pref pp pref;
-      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 "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, _) ->
       print_pref pp pref;
-      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 "Bstore: %s[%a] = %a\n" (name_of_chunk chunk)
+        (PrintOp.print_addressing reg)
+        (addr, args) reg src
+  | BF (Bcall (sg, fn, args, res, s, _)) ->
       print_pref pp pref;
-      fprintf pp "Bcall: %a = %a(%a)\n"
-        reg res ros fn regs args;
+      fprintf pp "Bcall: %a = %a(%a)\n" reg res ros fn regs args;
       print_succ pp s
-  | BF (Btailcall(sg, fn, args)) ->
+  | BF (Btailcall (sg, fn, args, _)) ->
       print_pref pp pref;
-      fprintf pp "Btailcall: %a(%a)\n"
-        ros fn regs args
-  | BF (Bbuiltin(ef, args, res, s)) ->
+      fprintf pp "Btailcall: %a(%a)\n" ros fn regs args
+  | BF (Bbuiltin (ef, args, res, s, _)) ->
       print_pref pp pref;
-      fprintf pp "Bbuiltin: %a = %s(%a)\n"
-        (print_builtin_res reg) res
-        (name_of_external ef)
-        (print_builtin_args reg) args;
+      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) ->
+  | Bcond (cond, args, ib1, ib2, info, _) ->
       print_pref pp pref;
       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)) ->
+        (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
       print_pref pp pref;
       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) ->
+  | BF (Breturn (None, _)) ->
       print_pref pp pref;
       fprintf pp "Breturn\n"
-  | BF (Breturn (Some arg)) ->
+  | BF (Breturn (Some arg, _)) ->
       print_pref pp pref;
       fprintf pp "Breturn: %a\n" reg arg
   | BF (Bgoto s) ->
@@ -97,28 +93,26 @@ let rec print_iblock pp is_rec pref ib =
         print_iblock pp is_rec pref ib2)
       else fprintf pp "Bseq...\n"
 
-let print_btl_inst pp ib =
-  print_iblock pp false "  " ib
+let print_btl_inst pp ib = print_iblock pp false "  " ib
 
 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);
+  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
+  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
-  | _ -> ()
+  match gd with Gfun (Internal f) -> print_function pp id f | _ -> ()
 
-let print_program pp (prog: BTL.program) =
+let print_program pp (prog : BTL.program) =
   List.iter (print_globdef pp) prog.prog_defs