aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--backend/Duplicateaux.ml2
-rw-r--r--backend/LICMaux.ml5
-rw-r--r--common/AuxTools.ml49
-rw-r--r--common/DebugPrint.ml6
-rw-r--r--scheduling/PrintBTL.ml16
-rw-r--r--scheduling/RTLpathLivegenaux.ml49
-rw-r--r--scheduling/RTLpathScheduleraux.ml1
-rw-r--r--scheduling/RTLtoBTLaux.ml68
8 files changed, 79 insertions, 117 deletions
diff --git a/backend/Duplicateaux.ml b/backend/Duplicateaux.ml
index d55da64a..e8e60a4f 100644
--- a/backend/Duplicateaux.ml
+++ b/backend/Duplicateaux.ml
@@ -23,6 +23,7 @@ open RTL
open Maps
open Camlcoq
open DebugPrint
+open AuxTools
let stats_oc = ref None
@@ -95,7 +96,6 @@ let write_stats_oc () =
end
let get_loop_headers = LICMaux.get_loop_headers
-let get_some = LICMaux.get_some
let rtl_successors = LICMaux.rtl_successors
(* Get list of nodes following a BFS of the code *)
diff --git a/backend/LICMaux.ml b/backend/LICMaux.ml
index b88dbc2d..df609505 100644
--- a/backend/LICMaux.ml
+++ b/backend/LICMaux.ml
@@ -17,16 +17,13 @@ open Kildall;;
open HashedSet;;
open Inject;;
open DebugPrint;;
+open AuxTools;;
type reg = P.t;;
(** get_loop_headers moved from Duplicateaux.ml to LICMaux.ml to prevent cycle dependencies *)
type vstate = Unvisited | Processed | Visited
-let get_some = function
-| None -> failwith "Did not get some"
-| Some thing -> thing
-
let rtl_successors = function
| Itailcall _ | Ireturn _ -> []
| Icall(_,_,_,_,n) | Ibuiltin(_,_,_,n) | Inop n | Iop (_,_,_,n)
diff --git a/common/AuxTools.ml b/common/AuxTools.ml
new file mode 100644
index 00000000..a667044f
--- /dev/null
+++ b/common/AuxTools.ml
@@ -0,0 +1,49 @@
+open RTL
+open Maps
+
+let get_some = function
+ | 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 _ -> []
+
+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
+
+let non_predicted_successors i = function
+ | None -> successors_inst i
+ | Some ps -> List.filter (fun s -> s != ps) (successors_inst i)
+
+(* adapted from Linearizeaux.get_join_points *)
+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 not (get_some @@ PTree.get pc !reached_twice) then
+ reached_twice := PTree.set pc true !reached_twice
+ end else begin
+ reached := PTree.set pc true !reached;
+ traverse_succs (successors_inst @@ get_some @@ PTree.get pc code)
+ end
+ and traverse_succs = function
+ | [] -> ()
+ | [pc] -> traverse pc
+ | pc :: l -> traverse pc; traverse_succs l
+ in traverse entry; !reached_twice
diff --git a/common/DebugPrint.ml b/common/DebugPrint.ml
index 6f8449ee..021ea5c0 100644
--- a/common/DebugPrint.ml
+++ b/common/DebugPrint.ml
@@ -1,6 +1,7 @@
open Maps
open Camlcoq
open Registers
+open AuxTools
let debug_flag = ref false
@@ -128,10 +129,7 @@ end
let print_instructions insts code =
- let get_some = function
- | None -> failwith "Did not get some"
- | Some thing -> thing
- in if (!debug_flag) then begin
+ if (!debug_flag) then begin
debug "[ ";
List.iter (
fun n -> (PrintRTL.print_instruction stdout (P.to_int n, get_some @@ PTree.get n code))
diff --git a/scheduling/PrintBTL.ml b/scheduling/PrintBTL.ml
index 781dcaf3..b461e3f1 100644
--- a/scheduling/PrintBTL.ml
+++ b/scheduling/PrintBTL.ml
@@ -23,38 +23,48 @@ let ros pp = function
let print_succ pp s =
fprintf pp "\tsucc %d\n" (P.to_int s)
+let print_pref pp pref =
+ fprintf pp "%s" pref
+
let rec print_iblock pp is_rec pref ib =
- fprintf pp "%s" pref;
match ib with
| Bnop ->
+ print_pref pp pref;
fprintf pp "Bnop\n"
| Bop(op, args, res) ->
+ print_pref pp pref;
fprintf pp "Bop: %a = %a\n"
reg res (PrintOp.print_operation reg) (op, args)
| Bload(trap, chunk, addr, args, dst) ->
+ print_pref pp pref;
fprintf pp "Bload: %a = %s[%a]%a\n"
reg dst (name_of_chunk chunk)
(PrintOp.print_addressing reg) (addr, args)
print_trapping_mode trap
| Bstore(chunk, addr, args, src) ->
+ print_pref pp pref;
fprintf pp "Bstore: %s[%a] = %a\n"
(name_of_chunk chunk)
(PrintOp.print_addressing reg) (addr, args)
reg src
| BF (Bcall(sg, fn, args, res, s)) ->
+ print_pref pp pref;
fprintf pp "Bcall: %a = %a(%a)\n"
reg res ros fn regs args;
print_succ pp s
| BF (Btailcall(sg, fn, args)) ->
+ print_pref pp pref;
fprintf pp "Btailcall: %a(%a)\n"
ros fn regs args
| BF (Bbuiltin(ef, args, res, s)) ->
+ print_pref pp pref;
fprintf pp "Bbuiltin: %a = %s(%a)\n"
(print_builtin_res reg) res
(name_of_external ef)
(print_builtin_args reg) args;
print_succ pp s
| Bcond(cond, args, ib1, ib2, info) ->
+ print_pref pp pref;
fprintf pp "Bcond: (%a) (prediction: %s)\n"
(PrintOp.print_condition reg) (cond, args)
(match info with None -> "none" | Some true -> "branch" | Some false -> "fallthrough");
@@ -67,15 +77,19 @@ let rec print_iblock pp is_rec pref ib =
fprintf pp "%s]\n" pref
| BF (Bjumptable(arg, tbl)) ->
let tbl = Array.of_list tbl in
+ print_pref pp pref;
fprintf pp "Bjumptable: (%a)\n" reg arg;
for i = 0 to Array.length tbl - 1 do
fprintf pp "\t\tcase %d: goto %d\n" i (P.to_int tbl.(i))
done
| BF (Breturn None) ->
+ print_pref pp pref;
fprintf pp "Breturn\n"
| BF (Breturn (Some arg)) ->
+ print_pref pp pref;
fprintf pp "Breturn: %a\n" reg arg
| BF (Bgoto s) ->
+ print_pref pp pref;
fprintf pp "Bgoto: %d\n" (P.to_int s)
| Bseq (ib1, ib2) ->
if is_rec then (
diff --git a/scheduling/RTLpathLivegenaux.ml b/scheduling/RTLpathLivegenaux.ml
index 2a20a15d..c9bb94d3 100644
--- a/scheduling/RTLpathLivegenaux.ml
+++ b/scheduling/RTLpathLivegenaux.ml
@@ -7,31 +7,7 @@ open Datatypes
open Kildall
open Lattice
open DebugPrint
-
-let get_some = function
-| 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 _ -> []
-
-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
-
-let non_predicted_successors i =
- match predicted_successor i with
- | None -> successors_inst i
- | Some n -> List.filter (fun n' -> n != n') (successors_inst i)
+open AuxTools
let rec list_to_regset = function
| [] -> Regset.empty
@@ -59,24 +35,6 @@ let get_output_reg i =
| Iop (_, _, r, _) | Iload (_, _, _, _, r, _) | Icall (_, _, _, r, _) -> Some r
| Ibuiltin (_, _, brr, _) -> (match brr with AST.BR r -> Some r | _ -> None)
-(* adapted from Linearizeaux.get_join_points *)
-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 not (get_some @@ PTree.get pc !reached_twice) then
- reached_twice := PTree.set pc true !reached_twice
- end else begin
- reached := PTree.set pc true !reached;
- traverse_succs (successors_inst @@ get_some @@ PTree.get pc code)
- end
- and traverse_succs = function
- | [] -> ()
- | [pc] -> traverse pc
- | pc :: l -> traverse pc; traverse_succs l
- in traverse entry; !reached_twice
-
(* Does not set the input_regs and liveouts field *)
let get_path_map code entry join_points =
let visited = ref (PTree.map (fun n i -> false) code) in
@@ -92,12 +50,13 @@ let get_path_map code entry join_points =
let inst = get_some @@ PTree.get n code in
begin
psize := !psize + 1;
- let successor = match predicted_successor inst with
+ let psucc = predicted_successor inst in
+ let successor = match psucc with
| None -> None
| Some n' -> if get_some @@ PTree.get n' join_points then None else Some n'
in match successor with
| Some n' -> begin
- path_successors := !path_successors @ non_predicted_successors inst;
+ path_successors := !path_successors @ non_predicted_successors inst psucc;
dig_path_rec n'
end
| None -> Some ({ psize = (Camlcoq.Nat.of_int !psize);
diff --git a/scheduling/RTLpathScheduleraux.ml b/scheduling/RTLpathScheduleraux.ml
index aeed39df..70a0c507 100644
--- a/scheduling/RTLpathScheduleraux.ml
+++ b/scheduling/RTLpathScheduleraux.ml
@@ -7,6 +7,7 @@ open RTL
open Maps
open Registers
open ExpansionOracle
+open AuxTools
let config = Machine.config
diff --git a/scheduling/RTLtoBTLaux.ml b/scheduling/RTLtoBTLaux.ml
index 9a61f55e..e14e0ab3 100644
--- a/scheduling/RTLtoBTLaux.ml
+++ b/scheduling/RTLtoBTLaux.ml
@@ -3,62 +3,9 @@ open RTL
open BTL
open Registers
open DebugPrint
-open PrintRTL
open PrintBTL
open Camlcoq
-
-(* 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
-
-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 _ -> []
-
-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
-
-(* TODO gourdinl Adapted from RTLpathLivegenaux to avoid redundant computations ... *)
-let non_predicted_successors i = function
- | None -> successors_inst i
- | Some ps -> List.filter (fun s -> s != ps) (successors_inst i)
-
-(* adapted from Linearizeaux.get_join_points *)
-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 (
- if not (get_some @@ PTree.get pc !reached_twice) then
- 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))
- and traverse_succs = function
- | [] -> ()
- | [ pc ] -> traverse pc
- | pc :: l ->
- traverse pc;
- traverse_succs l
- in
- traverse entry;
- !reached_twice
+open AuxTools
let encaps_final inst osucc =
match inst with
@@ -94,7 +41,7 @@ let translate_inst inst is_final =
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!! *)
+ (* TODO gourdinl SEPARATE IN A BETTER WAY!! *)
let rec build_btl_tree e =
if get_some @@ PTree.get e !reached then ()
else (
@@ -102,9 +49,6 @@ let translate_function code entry join_points =
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
@@ -148,7 +92,7 @@ let print_dm dm =
(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
@@ -157,12 +101,12 @@ let rtl2btl (f : RTL.coq_function) =
debug "Entry %d\n" (P.to_int entry);
debug "RTL Code: ";
print_code code;
+ debug_flag := false;
debug "BTL Code: ";
print_btl_code stderr btl true;
- debug "BTL Dupmap:\n";
- print_dm dm;
+ debug "Dupmap:\n";
+ print_ptree print_pint dm;
debug "Join points: ";
print_true_nodes join_points;
debug "\n";
- debug_flag := false;
((btl, entry), dm)
generated by cgit (git 2.34.1) at 2024-05-19 23:08:04 +0000