From 3104e551bf87abeab9a257c955cf9b180769dc64 Mon Sep 17 00:00:00 2001
From: Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>
Date: Mon, 8 Feb 2021 17:26:12 +0100
Subject: Adding pathmap psize modification during expansion oracle

---
 riscV/ExpansionOracle.ml          | 29 ++++++++++++++++++++---------
 scheduling/RTLpathScheduleraux.ml | 10 +++++-----
 2 files changed, 25 insertions(+), 14 deletions(-)

diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml
index af14811d..e267fd5a 100644
--- a/riscV/ExpansionOracle.ml
+++ b/riscV/ExpansionOracle.ml
@@ -18,6 +18,7 @@ open RTL
 open Op
 open Asmgen
 open DebugPrint
+open RTLpath
 open! Integers
 
 let reg = ref 1
@@ -345,29 +346,37 @@ let get_regs_inst = function
   | Ireturn (Some r) -> [ r ]
   | _ -> []
 
-let rec write_tree' exp current initial code' new_order =
-  if current = !node then (
-    code' := PTree.set initial (Inop (n2p ())) !code';
-    new_order := initial :: !new_order);
+let write_initial_node initial code' new_order =
+  code' := PTree.set initial (Inop (n2p ())) !code';
+  new_order := initial :: !new_order
+
+let write_pathmap initial esize pm' =
+  let path = get_some @@ PTree.get initial !pm' in
+  let npsize = Camlcoq.Nat.of_int (esize + (Camlcoq.Nat.to_int path.psize)) in
+  let path' = { psize = npsize; input_regs = path.input_regs; output_regs = path.output_regs } in
+  pm' := PTree.set initial path' !pm'
+
+let rec write_tree exp current code' new_order =
   match exp with
   | (Iop (_, _, _, succ) as inst) :: k ->
       code' := PTree.set (Camlcoq.P.of_int current) inst !code';
       new_order := Camlcoq.P.of_int current :: !new_order;
-      write_tree' k (current - 1) initial code' new_order
+      write_tree k (current - 1) code' new_order
   | (Icond (_, _, succ1, succ2, _) as inst) :: k ->
       code' := PTree.set (Camlcoq.P.of_int current) inst !code';
       new_order := Camlcoq.P.of_int current :: !new_order;
-      write_tree' k (current - 1) initial code' new_order
+      write_tree k (current - 1) code' new_order
   | [] -> ()
   | _ -> failwith "ExpansionOracle.write_tree: inconsistent instruction."
 
-let expanse (sb : superblock) code =
+let expanse (sb : superblock) code pm =
   let new_order = ref [] in
   let liveins = ref sb.liveins in
   let exp = ref [] in
   let was_branch = ref false in
   let was_exp = ref false in
   let code' = ref code in
+  let pm' = ref pm in
   Array.iter
     (fun n ->
       was_branch := false;
@@ -493,11 +502,13 @@ let expanse (sb : superblock) code =
              liveins := PTree.set (n2p ()) lives !liveins;
              liveins := PTree.remove n !liveins
          | _ -> ());
-        write_tree' !exp !node n code' new_order))
+        write_pathmap sb.instructions.(0) (List.length !exp) pm';
+        write_initial_node n code' new_order;
+        write_tree !exp !node code' new_order))
     sb.instructions;
   sb.instructions <- Array.of_list (List.rev !new_order);
   sb.liveins <- !liveins;
-  !code'
+  (!code', !pm')
 
 let rec find_last_node_reg = function
   | [] -> ()
diff --git a/scheduling/RTLpathScheduleraux.ml b/scheduling/RTLpathScheduleraux.ml
index cdee5a5b..19b05741 100644
--- a/scheduling/RTLpathScheduleraux.ml
+++ b/scheduling/RTLpathScheduleraux.ml
@@ -280,11 +280,11 @@ let turn_all_loads_nontrap sb code =
     !code'
   end
 
-let rec do_schedule code = function
-  | [] -> code
+let rec do_schedule code pm = function
+  | [] -> (code, pm)
   | sb :: lsb ->
       (*debug_flag := true;*)
-      let code_exp = expanse sb code in
+      let (code_exp, pm) = expanse sb code pm in
       (*debug_flag := false;*)
       (* Trick: instead of turning loads into non trap as needed..
        * First, we turn them all into non-trap.
@@ -302,7 +302,7 @@ let rec do_schedule code = function
         debug "\nNew Code: "; print_code new_code;
         debug "\n";
         (* debug_flag := false; *)
-        do_schedule new_code lsb
+        do_schedule new_code pm lsb
       end
 
 let get_ok r = match r with Errors.OK x -> x | _ -> failwith "Did not get OK"
@@ -323,6 +323,6 @@ let scheduler f =
     (*debug_flag := true; *)
     find_last_node_reg (PTree.elements code);
     (*print_code code;*)
-    let tc = do_schedule code lsb in
+    let (tc, pm) = do_schedule code pm lsb in
     (((tc, entry), pm), id_ptree)
   end
-- 
cgit