oracle simplification, BTL printer, and error msg spec

1 files changed, 105 insertions, 56 deletions

diff --git a/scheduling/RTLtoBTLaux.ml b/scheduling/RTLtoBTLaux.ml
index 20aa01aa..3c9b7644 100644
--- a/scheduling/RTLtoBTLaux.ml
+++ b/scheduling/RTLtoBTLaux.ml
@@ -3,28 +3,35 @@ open RTL
 open BTL
 open Registers
 open DebugPrint
+open PrintRTL
+open PrintBTL
 
 (* TODO gourdinl duplicated parts from RTLpathLivegenaux.ml
         This should be accessible everywhere. *)
 let get_some = function
-| None -> failwith "Got None instead of Some _"
-| Some thing -> thing
+  | None -> failwith "Got None instead of Some _"
+  | Some thing -> thing
 
 let successors_inst = function
-| Inop n | Iop (_,_,_,n) | Iload (_,_,_,_,_,n) | Istore (_,_,_,_,n) | Icall (_,_,_,_,n) | Ibuiltin (_,_,_,n) -> [n]
-| Icond (_,_,n1,n2,_) -> [n1; n2]
-| Ijumptable (_,l) -> l
-| Itailcall _ | Ireturn _ -> []
+  | Inop n
+  | Iop (_, _, _, n)
+  | Iload (_, _, _, _, _, n)
+  | Istore (_, _, _, _, n)
+  | Icall (_, _, _, _, n)
+  | Ibuiltin (_, _, _, n) ->
+      [ n ]
+  | Icond (_, _, n1, n2, _) -> [ n1; n2 ]
+  | Ijumptable (_, l) -> l
+  | Itailcall _ | Ireturn _ -> []
 
 let predicted_successor = function
-| Inop n | Iop (_,_,_,n) | Iload (_,_,_,_,_,n) | Istore (_,_,_,_,n) -> Some n
-| Icall (_,_,_,_,n) | Ibuiltin (_,_,_,n) -> None
-| Icond (_,_,n1,n2,p) -> (
-    match p with
-    | Some true -> Some n1
-    | Some false -> Some n2
-    | None -> None )
-| Ijumptable _ | Itailcall _ | Ireturn _ -> None
+  | Inop n | Iop (_, _, _, n) | Iload (_, _, _, _, _, n) | Istore (_, _, _, _, n)
+    ->
+      Some n
+  | Icall (_, _, _, _, n) | Ibuiltin (_, _, _, n) -> None
+  | Icond (_, _, n1, n2, p) -> (
+      match p with Some true -> Some n1 | Some false -> Some n2 | None -> None)
+  | Ijumptable _ | Itailcall _ | Ireturn _ -> None
 
 (* TODO gourdinl Adapted from RTLpathLivegenaux to avoid redundant computations ... *)
 let non_predicted_successors i = function
@@ -36,83 +43,125 @@ let get_join_points code entry =
   let reached = ref (PTree.map (fun n i -> false) code) in
   let reached_twice = ref (PTree.map (fun n i -> false) code) in
   let rec traverse pc =
-    if get_some @@ PTree.get pc !reached then begin
+    if get_some @@ PTree.get pc !reached then (
       if not (get_some @@ PTree.get pc !reached_twice) then
-        reached_twice := PTree.set pc true !reached_twice
-    end else begin
+        reached_twice := PTree.set pc true !reached_twice)
+    else (
       reached := PTree.set pc true !reached;
-      traverse_succs (successors_inst @@ get_some @@ PTree.get pc code)
-    end
+      traverse_succs (successors_inst @@ get_some @@ PTree.get pc code))
   and traverse_succs = function
     | [] -> ()
-    | [pc] -> traverse pc
-    | pc :: l -> traverse pc; traverse_succs l
-  in traverse entry; !reached_twice
+    | [ pc ] -> traverse pc
+    | pc :: l ->
+        traverse pc;
+        traverse_succs l
+  in
+  traverse entry;
+  !reached_twice
+
+let encaps_final inst osucc =
+  match inst with
+  | BF _ | Bcond _ -> inst
+  | _ -> Bseq (inst, BF (Bgoto (get_some @@ osucc)))
 
-let translate_inst = function
-    | Inop (_) -> Bnop
-    | Iop (op,lr,rd,_) -> Bop (op,lr,rd)
-    | Iload (trap,chk,addr,lr,rd,_) -> Bload (trap,chk,addr,lr,rd)
-    | Istore (chk,addr,lr,rd,_) -> Bstore (chk,addr,lr,rd)
-    | Icall (sign,fn,lr,rd,s) -> BF (Bcall (sign,fn,lr,rd,s))
-    | Itailcall (sign,fn,lr) -> BF (Btailcall (sign,fn,lr))
-    | Ibuiltin (ef,lr,rd,s) -> BF (Bbuiltin (ef,lr,rd,s))
-    | Icond (cond,lr,ifso,ifnot,info) -> (
+let translate_inst inst is_final =
+  let osucc = ref None in
+  let btli =
+    match inst with
+    | Inop s ->
+        osucc := Some s;
+        Bnop
+    | Iop (op, lr, rd, s) ->
+        osucc := Some s;
+        Bop (op, lr, rd)
+    | Iload (trap, chk, addr, lr, rd, s) ->
+        osucc := Some s;
+        Bload (trap, chk, addr, lr, rd)
+    | Istore (chk, addr, lr, rd, s) ->
+        osucc := Some s;
+        Bstore (chk, addr, lr, rd)
+    | Icall (sign, fn, lr, rd, s) -> BF (Bcall (sign, fn, lr, rd, s))
+    | Itailcall (sign, fn, lr) -> BF (Btailcall (sign, fn, lr))
+    | Ibuiltin (ef, lr, rd, s) -> BF (Bbuiltin (ef, lr, rd, s))
+    | Icond (cond, lr, ifso, ifnot, info) ->
         (* TODO gourdinl remove this *)
         assert (info = None);
-        Bcond (cond,lr,BF (Bgoto(ifso)),BF (Bgoto(ifnot)),info))
-    | Ijumptable (arg, tbl) -> BF (Bjumptable (arg,tbl))
-    | Ireturn (oreg) -> BF (Breturn (oreg))
+        Bcond (cond, lr, BF (Bgoto ifso), BF (Bgoto ifnot), info)
+    | Ijumptable (arg, tbl) -> BF (Bjumptable (arg, tbl))
+    | Ireturn oreg -> BF (Breturn oreg)
+  in
+  if is_final then encaps_final btli !osucc else btli
 
 let translate_function code entry join_points =
   let reached = ref (PTree.map (fun n i -> false) code) in
   let btl_code = ref PTree.empty in
   (* SEPARATE IN A BETTER WAY!! *)
   let rec build_btl_tree e =
-    if (get_some @@ PTree.get e !reached) then ()
+    if get_some @@ PTree.get e !reached then ()
     else (
       reached := PTree.set e true !reached;
       let next_nodes = ref [] in
       let rec build_btl_block n =
         let inst = get_some @@ PTree.get n code in
+        debug "Inst is : ";
+        print_instruction stderr (0, inst);
+        debug "\n";
         let psucc = predicted_successor inst in
         let succ =
-        match psucc with
-        | Some ps -> if get_some @@ PTree.get ps join_points then None else Some ps
-        | None -> None
-        in match succ with
+          match psucc with
+          | Some ps ->
+              if get_some @@ PTree.get ps join_points then (
+                debug "IS JOIN PT\n";
+                None)
+              else Some ps
+          | None -> None
+        in
+        match succ with
         | Some s -> (
-          match inst with
-          | Icond (cond,lr,ifso,ifnot,info) -> (
-              (* TODO gourdinl remove this *)
-              assert (s = ifso || s = ifnot);
-              next_nodes := !next_nodes @ non_predicted_successors inst psucc;
-              if s = ifso then
-                Bcond (cond,lr,build_btl_block s,BF (Bgoto (ifnot)),info)
-              else
-                Bcond (cond,lr,BF (Bgoto (ifso)),build_btl_block s,info))
-          | _ -> Bseq (translate_inst inst, build_btl_block s))
-        | None -> (
+            debug "BLOCK CONTINUE\n";
+            match inst with
+            | Icond (cond, lr, ifso, ifnot, info) ->
+                (* TODO gourdinl remove this *)
+                assert (s = ifnot);
+                next_nodes := !next_nodes @ non_predicted_successors inst psucc;
+                Bcond (cond, lr, BF (Bgoto ifso), build_btl_block s, info)
+            | _ -> Bseq (translate_inst inst false, build_btl_block s))
+        | None ->
+            debug "BLOCK END.\n";
             next_nodes := !next_nodes @ successors_inst inst;
-            translate_inst inst)
+            translate_inst inst true
       in
       let ib = build_btl_block e in
       let succs = !next_nodes in
       let ibf = { entry = ib; input_regs = Regset.empty } in
       btl_code := PTree.set e ibf !btl_code;
       List.iter build_btl_tree succs)
-  in build_btl_tree entry; !btl_code
+  in
+  build_btl_tree entry;
+  !btl_code
+
+(*let print_dm dm =*)
+  (*List.iter (fun (n,ib) ->*)
+    (*debug "%d:" (P.to_int n);*)
+    (*print_iblock stderr false ib.entry)*)
+  (*(PTree.elements dm)*)
+
 
-let rtl2btl (f: RTL.coq_function) =
+
+let rtl2btl (f : RTL.coq_function) =
+  debug_flag := true;
   let code = f.fn_code in
   let entry = f.fn_entrypoint in
   let join_points = get_join_points code entry in
   let btl = translate_function code entry join_points in
-  debug_flag := true;
-  debug"Code: ";
+  let dm = PTree.map (fun n i -> n) btl in
+  debug "RTL Code: ";
   print_code code;
+  debug "BTL Code: ";
+  print_btl_code stderr btl true;
   debug "Join points: ";
   print_true_nodes join_points;
   debug "\n";
+  (*print_dm dm;*)
   debug_flag := false;
-  ((btl, entry), PTree.empty)
+  ((btl, entry), dm)