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 ++++++++++++++++++++---------
 1 file changed, 20 insertions(+), 9 deletions(-)

(limited to 'riscV/ExpansionOracle.ml')

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
   | [] -> ()
-- 
cgit