working oracles (no renumber for now)

5 files changed, 144 insertions, 79 deletions

diff --git a/scheduling/BTLaux.ml b/scheduling/BTLaux.ml
index e8e355b1..863afdf0 100644
--- a/scheduling/BTLaux.ml
+++ b/scheduling/BTLaux.ml
@@ -1,3 +1,3 @@
 type inst_info = { mutable inumb : int; mutable pcond : bool option }
 
-type block_info = { mutable bnumb : int }
+type block_info = { mutable bnumb : int; mutable visited: bool }
diff --git a/scheduling/BTLrenumber.ml b/scheduling/BTLrenumber.ml
new file mode 100644
index 00000000..dd6baa89
--- /dev/null
+++ b/scheduling/BTLrenumber.ml
@@ -0,0 +1,50 @@
+(* XXX uncomment
+open !BTL
+open DebugPrint
+open AuxTools
+open Maps*)
+
+(** A quick note on the BTL renumber algorithm
+    This is a simple first version where we try to reuse the entry numbering from RTL.
+    In the futur, it would be great to implement a strongly connected components partitionning.
+    The numbering is done by a postorder traversal.
+    TODO gourdinl : note perso
+    - faire un comptage global du nombre d'instructions rtl à générer
+    - utiliser la structure d'info créée lors de la génération pour tenter de préserver au max
+    la relation d'ordre, avec une heuristique genre (1 + max des succs) pour l'insertion
+    - quand il y a un branchement conditionnel, privilégier le parcour du fils gauche en premier
+    (afin d'avoir de plus petits numéros à gauche)
+*)
+(*
+let rec get_max_rtl_ninsts code entry =
+let rec postorder_blk ib =
+*)
+
+(* XXX uncomment
+let postorder code entry =
+  let renumbered_code = ref PTree.empty in
+  let rec renum_ibf e =
+    let ibf = get_some @@ PTree.get e code in
+    if ibf.binfo.visited then ()
+    else (
+      ibf.binfo.visited <- true;
+      let next_nodes = ref [] in
+      let ib = ibf.entry in
+      let rec renum_iblock ib =
+        match ib with
+      in
+      let rib = renum_iblock ib in
+      ibf.entry <- rib;
+      renumbered_code := PTree.set e ibf !renumbered_code;
+      let succs = !next_nodes in
+      List.iter renum_ibf succs)
+  in
+  renum_ibf entry
+
+let renumber (f: BTL.coq_function) =
+  debug_flag := true;
+  let code = f.fn_code in
+  let entry = f.fn_entrypoint in
+  let renumbered_code = postorder code entry in
+  debug_flag := false;
+  renumbered_code*)
diff --git a/scheduling/BTLtoRTLaux.ml b/scheduling/BTLtoRTLaux.ml
index dd7ba4c7..b4833b2c 100644
--- a/scheduling/BTLtoRTLaux.ml
+++ b/scheduling/BTLtoRTLaux.ml
@@ -4,50 +4,56 @@ open RTL
 open Camlcoq
 open AuxTools
 open DebugPrint
-open PrintBTL
+open BTLaux
 
 let is_atom = function
-  | Bseq (_, _) | Bcond (_, _, _, _, _, _) -> false
+  | Bseq (_, _) | Bcond (_, _, _, _, _) -> false
   | _ -> true
 
-let rec get_nn = function
-  | Bnop ni
-  | Bop (_, _, _, ni)
-  | Bload (_, _, _, _, _, ni)
-  | Bstore (_, _, _, _, ni)
-  | Bcond (_, _, _, _, _, ni)
-  | BF (Breturn (_, ni))
-  | BF (Bcall (_, _, _, _, _, ni))
-  | BF (Btailcall (_, _, _, ni))
-  | BF (Bbuiltin (_, _, _, _, ni))
-  | BF (Bjumptable (_, _, ni)) ->
-      ni
-  | BF (Bgoto s) -> s
-  | Bseq (ib1, _) -> get_nn ib1
+let get_inumb iinfo = P.of_int iinfo.inumb
+
+let rec get_ib_num = function
+  | BF (Bgoto s, _) -> s
+  | Bnop iinfo
+  | Bop (_, _, _, iinfo)
+  | Bload (_, _, _, _, _, iinfo)
+  | Bstore (_, _, _, _, iinfo)
+  | Bcond (_, _, _, _, iinfo)
+  | BF (_, iinfo) ->
+      get_inumb iinfo
+  | Bseq (ib1, _) -> get_ib_num ib1
 
 let translate_function code entry =
-  let reached = ref (PTree.map (fun n i -> false) code) in
   let rtl_code = ref PTree.empty in
+  let code =
+    PTree.map
+      (fun n ibf ->
+        ibf.binfo.visited <- false;
+        ibf)
+      code
+  in
   let rec build_rtl_tree e =
-    if get_some @@ PTree.get e !reached then ()
+    let ibf = get_some @@ PTree.get e code in
+    if ibf.binfo.visited then ()
     else (
-      reached := PTree.set e true !reached;
+      ibf.binfo.visited <- true;
+      let ib = ibf.entry in
       let next_nodes = ref [] in
-      let ib = (get_some @@ PTree.get e code).entry in
       let rec translate_btl_block ib k =
-        print_btl_inst stderr ib;
         let rtli =
           match ib with
-          | Bcond (cond, lr, BF (Bgoto s1), BF (Bgoto s2), info, ni) ->
+          | Bcond (cond, lr, BF (Bgoto s1, _), BF (Bgoto s2, _), iinfo) ->
               next_nodes := s1 :: s2 :: !next_nodes;
-              Some (Icond (cond, lr, s1, s2, info), ni)
-          | Bcond (cond, lr, BF (Bgoto s1), ib2, info, ni) ->
-              assert (info = Some false);
+              Some (Icond (cond, lr, s1, s2, iinfo.pcond), get_inumb iinfo)
+          | Bcond (cond, lr, BF (Bgoto s1, _), ib2, iinfo) ->
+              assert (iinfo.pcond = Some false);
               next_nodes := s1 :: !next_nodes;
               translate_btl_block ib2 None;
-              Some (Icond (cond, lr, s1, get_nn ib2, info), ni)
+              Some
+                ( Icond (cond, lr, s1, get_ib_num ib2, iinfo.pcond),
+                  get_inumb iinfo )
           (* TODO gourdinl remove dynamic check *)
-          | Bcond (_, _, _, _, _, _) ->
+          | Bcond (_, _, _, _, _) ->
               failwith "translate_function: invalid Bcond"
           | Bseq (ib1, ib2) ->
               (* TODO gourdinl remove dynamic check *)
@@ -55,29 +61,35 @@ let translate_function code entry =
               translate_btl_block ib1 (Some ib2);
               translate_btl_block ib2 None;
               None
-          | Bnop ni -> Some (Inop (get_nn (get_some k)), ni)
-          | Bop (op, lr, rd, ni) ->
-              Some (Iop (op, lr, rd, get_nn (get_some k)), ni)
-          | Bload (trap, chk, addr, lr, rd, ni) ->
-              Some (Iload (trap, chk, addr, lr, rd, get_nn (get_some k)), ni)
-          | Bstore (chk, addr, lr, rd, ni) ->
-              Some (Istore (chk, addr, lr, rd, get_nn (get_some k)), ni)
-          | BF (Bcall (sign, fn, lr, rd, s, ni)) ->
+          | Bnop iinfo -> Some (Inop (get_ib_num (get_some k)), get_inumb iinfo)
+          | Bop (op, lr, rd, iinfo) ->
+              Some (Iop (op, lr, rd, get_ib_num (get_some k)), get_inumb iinfo)
+          | Bload (trap, chk, addr, lr, rd, iinfo) ->
+              Some
+                ( Iload (trap, chk, addr, lr, rd, get_ib_num (get_some k)),
+                  get_inumb iinfo )
+          | Bstore (chk, addr, lr, rd, iinfo) ->
+              Some
+                ( Istore (chk, addr, lr, rd, get_ib_num (get_some k)),
+                  get_inumb iinfo )
+          | BF (Bcall (sign, fn, lr, rd, s), iinfo) ->
               next_nodes := s :: !next_nodes;
-              Some (Icall (sign, fn, lr, rd, s), ni)
-          | BF (Btailcall (sign, fn, lr, ni)) ->
-              Some (Itailcall (sign, fn, lr), ni)
-          | BF (Bbuiltin (ef, lr, rd, s, ni)) ->
+              Some (Icall (sign, fn, lr, rd, s), get_inumb iinfo)
+          | BF (Btailcall (sign, fn, lr), iinfo) ->
+              Some (Itailcall (sign, fn, lr), get_inumb iinfo)
+          | BF (Bbuiltin (ef, lr, rd, s), iinfo) ->
               next_nodes := s :: !next_nodes;
-              Some (Ibuiltin (ef, lr, rd, s), ni)
-          | BF (Bjumptable (arg, tbl, ni)) -> Some (Ijumptable (arg, tbl), ni)
-          | BF (Breturn (oreg, ni)) -> Some (Ireturn oreg, ni)
-          | BF (Bgoto s) ->
+              Some (Ibuiltin (ef, lr, rd, s), get_inumb iinfo)
+          | BF (Bjumptable (arg, tbl), iinfo) ->
+              next_nodes := !next_nodes @ tbl;
+              Some (Ijumptable (arg, tbl), get_inumb iinfo)
+          | BF (Breturn oreg, iinfo) -> Some (Ireturn oreg, get_inumb iinfo)
+          | BF (Bgoto s, iinfo) ->
               next_nodes := s :: !next_nodes;
               None
         in
         match rtli with
-        | Some (inst, ni) -> rtl_code := PTree.set ni inst !rtl_code
+        | Some (inst, inumb) -> rtl_code := PTree.set inumb inst !rtl_code
         | None -> ()
       in
       translate_btl_block ib None;
@@ -88,16 +100,16 @@ let translate_function code entry =
   !rtl_code
 
 let btl2rtl (f : BTL.coq_function) =
-  debug_flag := true;
+  (*debug_flag := true;*)
   let code = f.fn_code in
   let entry = f.fn_entrypoint in
   let rtl = translate_function code entry in
   let dm = PTree.map (fun n i -> n) code in
-  debug "Entry %d\n" (P.to_int entry);
+  debug "Entry %d\n" (p2i entry);
   debug "RTL Code: ";
-  print_code rtl;
+  (*print_code rtl;*)
   debug "Dupmap:\n";
   print_ptree print_pint dm;
   debug "\n";
-  debug_flag := false;
+  (*debug_flag := false;*)
   ((rtl, entry), dm)
diff --git a/scheduling/PrintBTL.ml b/scheduling/PrintBTL.ml
index 23ad91f6..0ed3981d 100644
--- a/scheduling/PrintBTL.ml
+++ b/scheduling/PrintBTL.ml
@@ -2,10 +2,10 @@ open Printf
 open Camlcoq
 open Datatypes
 open Maps
-open AST
 open BTL
 open PrintAST
 open BTLaux
+open DebugPrint
 
 (* Printing of BTL code *)
 
@@ -97,15 +97,18 @@ let rec print_iblock pp is_rec pref 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);
-  fprintf pp "\n"
+  if !debug_flag then (
+    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")
+  else ()
 
+(* TODO gourdinl remove or adapt this?
 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
@@ -116,4 +119,4 @@ 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
+  List.iter (print_globdef pp) prog.prog_defs*)
diff --git a/scheduling/RTLtoBTLaux.ml b/scheduling/RTLtoBTLaux.ml
index d4fd2643..43556150 100644
--- a/scheduling/RTLtoBTLaux.ml
+++ b/scheduling/RTLtoBTLaux.ml
@@ -4,15 +4,16 @@ open BTL
 open Registers
 open DebugPrint
 open PrintBTL
-open Camlcoq
 open AuxTools
 open BTLaux
 
 let undef_node = -1
+
 let mk_iinfo _inumb _pcond = { inumb = _inumb; pcond = _pcond }
+
 let def_iinfo = { inumb = undef_node; pcond = None }
 
-let mk_binfo _bnumb = { bnumb = _bnumb }
+let mk_binfo _bnumb = { bnumb = _bnumb; visited = false }
 
 let encaps_final inst osucc =
   match inst with
@@ -40,16 +41,20 @@ let translate_inst iinfo inst is_final =
     | Ibuiltin (ef, lr, rd, s) -> BF (Bbuiltin (ef, lr, rd, s), iinfo)
     | Icond (cond, lr, ifso, ifnot, info) ->
         iinfo.pcond <- info;
-        Bcond (cond, lr, BF (Bgoto ifso, def_iinfo), BF (Bgoto ifnot, def_iinfo), iinfo)
+        Bcond
+          ( cond,
+            lr,
+            BF (Bgoto ifso, def_iinfo),
+            BF (Bgoto ifnot, def_iinfo),
+            iinfo )
     | Ijumptable (arg, tbl) -> BF (Bjumptable (arg, tbl), iinfo)
-    | Ireturn oreg -> BF (Breturn (oreg), iinfo)
+    | Ireturn oreg -> BF (Breturn oreg, iinfo)
   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
-  (* TODO gourdinl SEPARATE IN A BETTER WAY!! *)
   let rec build_btl_tree e =
     if get_some @@ PTree.get e !reached then ()
     else (
@@ -63,21 +68,24 @@ let translate_function code entry join_points =
           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 -> (
-            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;
                 iinfo.pcond <- info;
-                Bcond (cond, lr, BF (Bgoto ifso, def_iinfo), build_btl_block s, iinfo)
+                Bcond
+                  ( cond,
+                    lr,
+                    BF (Bgoto ifso, def_iinfo),
+                    build_btl_block s,
+                    iinfo )
             | _ -> Bseq (translate_inst iinfo inst false, build_btl_block s))
         | None ->
             debug "BLOCK END.\n";
@@ -94,25 +102,16 @@ let translate_function code entry join_points =
   build_btl_tree entry;
   !btl_code
 
-let print_dm dm =
-  List.iter
-    (fun (n, n') ->
-      debug "%d -> %d" (P.to_int n) (P.to_int n');
-      (*print_btl_inst stderr ib.entry;*)
-      debug "\n")
-    (PTree.elements dm)
-
 let rtl2btl (f : RTL.coq_function) =
-  debug_flag := true;
+  (*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
   let dm = PTree.map (fun n i -> n) btl in
-  debug "Entry %d\n" (P.to_int entry);
+  debug "Entry %d\n" (p2i entry);
   debug "RTL Code: ";
-  print_code code;
-  debug_flag := false;
+  (*print_code code;*)
   debug "BTL Code: ";
   print_btl_code stderr btl true;
   debug "Dupmap:\n";
@@ -120,4 +119,5 @@ let rtl2btl (f : RTL.coq_function) =
   debug "Join points: ";
   print_true_nodes join_points;
   debug "\n";
+  (*debug_flag := false;*)
   ((btl, entry), dm)