Commit 3104e551 authored by Léo Gourdin's avatar Léo Gourdin
Browse files

Adding pathmap psize modification during expansion oracle

parent 7ae5c396
......@@ -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
| [] -> ()
......
......@@ -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
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment