aboutsummaryrefslogtreecommitdiffstats
path: root/riscV/ExpansionOracle.ml
diff options
context:
space:
mode:
authorLéo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>2021-03-06 12:36:11 +0100
committerLéo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>2021-03-06 12:36:11 +0100
commitc19ecc9326d0278989d7651bf8c8cf0d1c387235 (patch)
tree479bd06ca0ed2e2d14900a78c93914537e4a7d91 /riscV/ExpansionOracle.ml
parent3e953ef41f736ed5b7db699b1adf21d46cb5b8db (diff)
downloadcompcert-kvx-c19ecc9326d0278989d7651bf8c8cf0d1c387235.tar.gz
compcert-kvx-c19ecc9326d0278989d7651bf8c8cf0d1c387235.zip
Adding a mini CSE pass in the expansion oracle
Diffstat (limited to 'riscV/ExpansionOracle.ml')
-rw-r--r--riscV/ExpansionOracle.ml238
1 files changed, 159 insertions, 79 deletions
diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml
index 95a300c5..44049ecf 100644
--- a/riscV/ExpansionOracle.ml
+++ b/riscV/ExpansionOracle.ml
@@ -20,14 +20,21 @@ open Asmgen
open DebugPrint
open RTLpath
open! Integers
+open Camlcoq
+
+type sop = Sop of operation * P.t list
+
+type sval = Si of RTL.instruction | Sr of P.t
let reg = ref 1
let node = ref 1
-let r2p () = Camlcoq.P.of_int !reg
+let p2i r = P.to_int r
+
+let r2p () = P.of_int !reg
-let n2p () = Camlcoq.P.of_int !node
+let n2p () = P.of_int !node
let r2pi () =
reg := !reg + 1;
@@ -39,30 +46,72 @@ let n2pi () =
type immt = Xoriw | Xoril | Sltiw | Sltiuw | Sltil | Sltiul
-let load_hilo32 a1 dest hi lo succ is_long k =
- if Int.eq lo Int.zero then Iop (OEluiw (hi, is_long), [ a1 ], dest, succ) :: k
+let debug_was_cse = ref false
+
+let find_or_addnmove op args rd succ sargs map_consts =
+ let sop = Sop (op, sargs) in
+ match Hashtbl.find_opt map_consts sop with
+ | Some r ->
+ debug_was_cse := true;
+ Sr (P.of_int r)
+ | None ->
+ Hashtbl.add map_consts sop (p2i rd);
+ Si (Iop (op, args, rd, succ))
+
+let build_head_tuple head sv =
+ match sv with Si i -> (head @ [ i ], None) | Sr r -> (head, Some r)
+
+let load_hilo32 dest hi lo succ map_consts =
+ let op1 = OEluiw hi in
+ if Int.eq lo Int.zero then
+ let sv = find_or_addnmove op1 [] dest succ [] map_consts in
+ build_head_tuple [] sv
else
let r = r2pi () in
- Iop (OEluiw (hi, is_long), [ a1 ], r, n2pi ())
- :: Iop (Oaddimm lo, [ r ], dest, succ) :: k
-
-let load_hilo64 a1 dest hi lo succ k =
- if Int64.eq lo Int64.zero then Iop (OEluil hi, [ a1 ], dest, succ) :: k
+ let op2 = Oaddimm lo in
+ match find_or_addnmove op1 [] r (n2pi ()) [] map_consts with
+ | Si i ->
+ let sv = find_or_addnmove op2 [ r ] dest succ [ r ] map_consts in
+ build_head_tuple [ i ] sv
+ | Sr r' ->
+ let sv = find_or_addnmove op2 [ r' ] dest succ [ r' ] map_consts in
+ build_head_tuple [] sv
+
+let load_hilo64 dest hi lo succ map_consts =
+ let op1 = OEluil hi in
+ if Int64.eq lo Int64.zero then
+ let sv = find_or_addnmove op1 [] dest succ [] map_consts in
+ build_head_tuple [] sv
else
let r = r2pi () in
- Iop (OEluil hi, [ a1 ], r, n2pi ())
- :: Iop (Oaddlimm lo, [ r ], dest, succ) :: k
-
-let loadimm32 a1 dest n succ is_long k =
+ let op2 = Oaddlimm lo in
+ match find_or_addnmove op1 [] r (n2pi ()) [] map_consts with
+ | Si i ->
+ let sv = find_or_addnmove op2 [ r ] dest succ [ r ] map_consts in
+ build_head_tuple [ i ] sv
+ | Sr r' ->
+ let sv = find_or_addnmove op2 [ r' ] dest succ [ r' ] map_consts in
+ build_head_tuple [] sv
+
+let loadimm32 dest n succ map_consts =
match make_immed32 n with
- | Imm32_single imm -> Iop (OEaddiwr0 (imm, is_long), [ a1 ], dest, succ) :: k
- | Imm32_pair (hi, lo) -> load_hilo32 a1 dest hi lo succ is_long k
+ | Imm32_single imm ->
+ let op1 = OEaddiwr0 imm in
+ let sv = find_or_addnmove op1 [] dest succ [] map_consts in
+ build_head_tuple [] sv
+ | Imm32_pair (hi, lo) -> load_hilo32 dest hi lo succ map_consts
-let loadimm64 a1 dest n succ k =
+let loadimm64 dest n succ map_consts =
match make_immed64 n with
- | Imm64_single imm -> Iop (OEaddilr0 imm, [ a1 ], dest, succ) :: k
- | Imm64_pair (hi, lo) -> load_hilo64 a1 dest hi lo succ k
- | Imm64_large imm -> Iop (OEloadli imm, [], dest, succ) :: k
+ | Imm64_single imm ->
+ let op1 = OEaddilr0 imm in
+ let sv = find_or_addnmove op1 [] dest succ [] map_consts in
+ build_head_tuple [] sv
+ | Imm64_pair (hi, lo) -> load_hilo64 dest hi lo succ map_consts
+ | Imm64_large imm ->
+ let op1 = OEloadli imm in
+ let sv = find_or_addnmove op1 [] dest succ [] map_consts in
+ build_head_tuple [] sv
let get_opimm imm = function
| Xoriw -> OExoriw imm
@@ -72,32 +121,42 @@ let get_opimm imm = function
| Sltil -> OEsltil imm
| Sltiul -> OEsltiul imm
-let opimm32 a1 dest n succ is_long k op opimm =
+let unzip_head_tuple ht r = match ht with l, Some r' -> r' | l, None -> r
+
+let opimm32 a1 dest n succ k op opimm map_consts =
match make_immed32 n with
| Imm32_single imm -> Iop (get_opimm imm opimm, [ a1 ], dest, succ) :: k
| Imm32_pair (hi, lo) ->
let r = r2pi () in
- load_hilo32 a1 r hi lo (n2pi ()) is_long
- (Iop (op, [ a1; r ], dest, succ) :: k)
+ let ht = load_hilo32 r hi lo (n2pi ()) map_consts in
+ let r' = unzip_head_tuple ht r in
+ fst ht @ Iop (op, [ a1; r' ], dest, succ) :: k
-let opimm64 a1 dest n succ k op opimm =
+let opimm64 a1 dest n succ k op opimm map_consts =
match make_immed64 n with
| Imm64_single imm -> Iop (get_opimm imm opimm, [ a1 ], dest, succ) :: k
| Imm64_pair (hi, lo) ->
let r = r2pi () in
- load_hilo64 a1 r hi lo (n2pi ()) (Iop (op, [ a1; r ], dest, succ) :: k)
+ let ht = load_hilo64 r hi lo (n2pi ()) map_consts in
+ let r' = unzip_head_tuple ht r in
+ fst ht @ Iop (op, [ a1; r' ], dest, succ) :: k
| Imm64_large imm ->
let r = r2pi () in
- Iop (OEloadli imm, [], r, n2pi ()) :: Iop (op, [ a1; r ], dest, succ) :: k
+ let op1 = OEloadli imm in
+ let inode = n2pi () in
+ let sv = find_or_addnmove op1 [] r inode [] map_consts in
+ let ht = build_head_tuple [] sv in
+ let r' = unzip_head_tuple ht r in
+ fst ht @ Iop (op, [ a1; r' ], dest, succ) :: k
-let xorimm32 a1 dest n succ is_long k =
- opimm32 a1 dest n succ is_long k Oxor Xoriw
+let xorimm32 a1 dest n succ k map_consts =
+ opimm32 a1 dest n succ k Oxor Xoriw map_consts
-let sltimm32 a1 dest n succ is_long k =
- opimm32 a1 dest n succ is_long k (OEsltw None) Sltiw
+let sltimm32 a1 dest n succ k map_consts =
+ opimm32 a1 dest n succ k (OEsltw None) Sltiw map_consts
-let sltuimm32 a1 dest n succ is_long k =
- opimm32 a1 dest n succ is_long k (OEsltuw None) Sltiuw
+let sltuimm32 a1 dest n succ k map_consts =
+ opimm32 a1 dest n succ k (OEsltuw None) Sltiuw map_consts
let xorimm64 a1 dest n succ k = opimm64 a1 dest n succ k Oxorl Xoril
@@ -233,85 +292,101 @@ let cond_single cmp f1 f2 dest succ =
| Cgt -> Iop (OEflts, [ f2; f1 ], dest, succ)
| Cge -> Iop (OEfles, [ f2; f1 ], dest, succ)
-let expanse_cbranchimm_int32s cmp a1 n info succ1 succ2 k =
+let expanse_cbranchimm_int32s cmp a1 n info succ1 succ2 k map_consts =
if Int.eq n Int.zero then cbranch_int32s true cmp a1 a1 info succ1 succ2 k
else
let r = r2pi () in
- loadimm32 a1 r n (n2pi ()) false
- (cbranch_int32s false cmp a1 r info succ1 succ2 k)
+ let ht = loadimm32 r n (n2pi ()) map_consts in
+ let r' = unzip_head_tuple ht r in
+ fst ht @ cbranch_int32s false cmp a1 r' info succ1 succ2 k
-let expanse_cbranchimm_int32u cmp a1 n info succ1 succ2 k =
+let expanse_cbranchimm_int32u cmp a1 n info succ1 succ2 k map_consts =
if Int.eq n Int.zero then cbranch_int32u true cmp a1 a1 info succ1 succ2 k
else
let r = r2pi () in
- loadimm32 a1 r n (n2pi ()) false
- (cbranch_int32u false cmp a1 r info succ1 succ2 k)
+ let ht = loadimm32 r n (n2pi ()) map_consts in
+ let r' = unzip_head_tuple ht r in
+ fst ht @ cbranch_int32u false cmp a1 r' info succ1 succ2 k
-let expanse_cbranchimm_int64s cmp a1 n info succ1 succ2 k =
+let expanse_cbranchimm_int64s cmp a1 n info succ1 succ2 k map_consts =
if Int64.eq n Int64.zero then cbranch_int64s true cmp a1 a1 info succ1 succ2 k
else
let r = r2pi () in
- loadimm64 a1 r n (n2pi ())
- (cbranch_int64s false cmp a1 r info succ1 succ2 k)
+ let ht = loadimm64 r n (n2pi ()) map_consts in
+ let r' = unzip_head_tuple ht r in
+ fst ht @ cbranch_int64s false cmp a1 r' info succ1 succ2 k
-let expanse_cbranchimm_int64u cmp a1 n info succ1 succ2 k =
+let expanse_cbranchimm_int64u cmp a1 n info succ1 succ2 k map_consts =
if Int64.eq n Int64.zero then cbranch_int64u true cmp a1 a1 info succ1 succ2 k
else
let r = r2pi () in
- loadimm64 a1 r n (n2pi ())
- (cbranch_int64u false cmp a1 r info succ1 succ2 k)
+ let ht = loadimm64 r n (n2pi ()) map_consts in
+ let r' = unzip_head_tuple ht r in
+ fst ht @ cbranch_int64u false cmp a1 r' info succ1 succ2 k
-let expanse_condimm_int32s cmp a1 n dest succ k =
+let expanse_condimm_int32s cmp a1 n dest succ k map_consts =
if Int.eq n Int.zero then cond_int32s true cmp a1 a1 dest succ k
else
match cmp with
| Ceq | Cne ->
let r = r2pi () in
- xorimm32 a1 r n (n2pi ()) false (cond_int32s true cmp r r dest succ k)
- | Clt -> sltimm32 a1 dest n succ false k
+ xorimm32 a1 r n (n2pi ())
+ (cond_int32s true cmp r r dest succ k)
+ map_consts
+ | Clt -> sltimm32 a1 dest n succ k map_consts
| Cle ->
if Int.eq n (Int.repr Int.max_signed) then
- loadimm32 a1 dest Int.one succ false k
- else sltimm32 a1 dest (Int.add n Int.one) succ false k
+ let ht = loadimm32 dest Int.one succ map_consts in
+ fst ht @ k
+ else sltimm32 a1 dest (Int.add n Int.one) succ k map_consts
| _ ->
let r = r2pi () in
- loadimm32 a1 r n (n2pi ()) false
- (cond_int32s false cmp a1 r dest succ k)
+ let ht = loadimm32 r n (n2pi ()) map_consts in
+ let r' = unzip_head_tuple ht r in
+ fst ht @ cond_int32s false cmp a1 r' dest succ k
-let expanse_condimm_int32u cmp a1 n dest succ k =
+let expanse_condimm_int32u cmp a1 n dest succ k map_consts =
if Int.eq n Int.zero then cond_int32u true cmp a1 a1 dest succ k
else
match cmp with
- | Clt -> sltuimm32 a1 dest n succ false k
+ | Clt -> sltuimm32 a1 dest n succ k map_consts
| _ ->
let r = r2pi () in
- loadimm32 a1 r n (n2pi ()) false
- (cond_int32u false cmp a1 r dest succ k)
+ let ht = loadimm32 r n (n2pi ()) map_consts in
+ let r' = unzip_head_tuple ht r in
+ fst ht @ cond_int32u false cmp a1 r' dest succ k
-let expanse_condimm_int64s cmp a1 n dest succ k =
+let expanse_condimm_int64s cmp a1 n dest succ k map_consts =
if Int64.eq n Int64.zero then cond_int64s true cmp a1 a1 dest succ k
else
match cmp with
| Ceq | Cne ->
let r = r2pi () in
- xorimm64 a1 r n (n2pi ()) (cond_int64s true cmp r r dest succ k)
- | Clt -> sltimm64 a1 dest n succ k
+ xorimm64 a1 r n (n2pi ())
+ (cond_int64s true cmp r r dest succ k)
+ map_consts
+ | Clt -> sltimm64 a1 dest n succ k map_consts
| Cle ->
if Int64.eq n (Int64.repr Int64.max_signed) then
- loadimm32 a1 dest Int.one succ true k
- else sltimm64 a1 dest (Int64.add n Int64.one) succ k
+ let ht = loadimm32 dest Int.one succ map_consts in
+ fst ht @ k
+ else sltimm64 a1 dest (Int64.add n Int64.one) succ k map_consts
| _ ->
let r = r2pi () in
- loadimm64 a1 r n (n2pi ()) (cond_int64s false cmp a1 r dest succ k)
+ let ht = loadimm64 r n (n2pi ()) map_consts in
+ let r' = unzip_head_tuple ht r in
+ fst ht @ cond_int64s false cmp a1 r' dest succ k
-let expanse_condimm_int64u cmp a1 n dest succ k =
+let expanse_condimm_int64u cmp a1 n dest succ k map_consts =
if Int64.eq n Int64.zero then cond_int64u true cmp a1 a1 dest succ k
else
match cmp with
- | Clt -> sltuimm64 a1 dest n succ k
+ | Clt -> sltuimm64 a1 dest n succ k map_consts
| _ ->
let r = r2pi () in
- loadimm64 a1 r n (n2pi ()) (cond_int64u false cmp a1 r dest succ k)
+ let ht = loadimm64 r n (n2pi ()) map_consts in
+ let r' = unzip_head_tuple ht r in
+ fst ht @ cond_int64u false cmp a1 r' dest succ k
let expanse_cond_fp cnot fn_cond cmp f1 f2 dest succ k =
let normal = is_normal_cmp cmp in
@@ -368,12 +443,12 @@ let write_pathmap initial esize 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;
+ code' := PTree.set (P.of_int current) inst !code';
+ new_order := P.of_int current :: !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;
+ code' := PTree.set (P.of_int current) inst !code';
+ new_order := P.of_int current :: !new_order;
write_tree k (current - 1) code' new_order
| [] -> ()
| _ -> failwith "ExpansionOracle.write_tree: inconsistent instruction."
@@ -387,11 +462,13 @@ let expanse (sb : superblock) code pm =
let was_exp = ref false in
let code' = ref code in
let pm' = ref pm in
+ let map_consts = Hashtbl.create 100 in
Array.iter
(fun n ->
was_branch := false;
was_exp := false;
let inst = get_some @@ PTree.get n code in
+ (*print_instruction stderr (0, inst);*)
(match inst with
| Iop (Ocmp (Ccomp c), a1 :: a2 :: nil, dest, succ) ->
debug "Iop/Ccomp\n";
@@ -403,11 +480,11 @@ let expanse (sb : superblock) code pm =
was_exp := true
| Iop (Ocmp (Ccompimm (c, imm)), a1 :: nil, dest, succ) ->
debug "Iop/Ccompimm\n";
- exp := expanse_condimm_int32s c a1 imm dest succ [];
+ exp := expanse_condimm_int32s c a1 imm dest succ [] map_consts;
was_exp := true
| Iop (Ocmp (Ccompuimm (c, imm)), a1 :: nil, dest, succ) ->
debug "Iop/Ccompuimm\n";
- exp := expanse_condimm_int32u c a1 imm dest succ [];
+ exp := expanse_condimm_int32u c a1 imm dest succ [] map_consts;
was_exp := true
| Iop (Ocmp (Ccompl c), a1 :: a2 :: nil, dest, succ) ->
debug "Iop/Ccompl\n";
@@ -419,11 +496,11 @@ let expanse (sb : superblock) code pm =
was_exp := true
| Iop (Ocmp (Ccomplimm (c, imm)), a1 :: nil, dest, succ) ->
debug "Iop/Ccomplimm\n";
- exp := expanse_condimm_int64s c a1 imm dest succ [];
+ exp := expanse_condimm_int64s c a1 imm dest succ [] map_consts;
was_exp := true
| Iop (Ocmp (Ccompluimm (c, imm)), a1 :: nil, dest, succ) ->
debug "Iop/Ccompluimm\n";
- exp := expanse_condimm_int64u c a1 imm dest succ [];
+ exp := expanse_condimm_int64u c a1 imm dest succ [] map_consts;
was_exp := true
| Iop (Ocmp (Ccompf c), f1 :: f2 :: nil, dest, succ) ->
debug "Iop/Ccompf\n";
@@ -453,12 +530,14 @@ let expanse (sb : superblock) code pm =
was_exp := true
| Icond (Ccompimm (c, imm), a1 :: nil, succ1, succ2, info) ->
debug "Icond/Ccompimm\n";
- exp := expanse_cbranchimm_int32s c a1 imm info succ1 succ2 [];
+ exp :=
+ expanse_cbranchimm_int32s c a1 imm info succ1 succ2 [] map_consts;
was_branch := true;
was_exp := true
| Icond (Ccompuimm (c, imm), a1 :: nil, succ1, succ2, info) ->
debug "Icond/Ccompuimm\n";
- exp := expanse_cbranchimm_int32u c a1 imm info succ1 succ2 [];
+ exp :=
+ expanse_cbranchimm_int32u c a1 imm info succ1 succ2 [] map_consts;
was_branch := true;
was_exp := true
| Icond (Ccompl c, a1 :: a2 :: nil, succ1, succ2, info) ->
@@ -473,12 +552,14 @@ let expanse (sb : superblock) code pm =
was_exp := true
| Icond (Ccomplimm (c, imm), a1 :: nil, succ1, succ2, info) ->
debug "Icond/Ccomplimm\n";
- exp := expanse_cbranchimm_int64s c a1 imm info succ1 succ2 [];
+ exp :=
+ expanse_cbranchimm_int64s c a1 imm info succ1 succ2 [] map_consts;
was_branch := true;
was_exp := true
| Icond (Ccompluimm (c, imm), a1 :: nil, succ1, succ2, info) ->
debug "Icond/Ccompluimm\n";
- exp := expanse_cbranchimm_int64u c a1 imm info succ1 succ2 [];
+ exp :=
+ expanse_cbranchimm_int64u c a1 imm info succ1 succ2 [] map_consts;
was_branch := true;
was_exp := true
| Icond (Ccompf c, f1 :: f2 :: nil, succ1, succ2, info) ->
@@ -509,9 +590,7 @@ let expanse (sb : superblock) code pm =
let lives = PTree.get n !liveins in
match lives with
| Some lives ->
- let new_branch_pc =
- Camlcoq.P.of_int (!node - (List.length !exp - 1))
- in
+ let new_branch_pc = P.of_int (!node - (List.length !exp - 1)) in
liveins := PTree.set new_branch_pc lives !liveins;
liveins := PTree.remove n !liveins
| _ -> ());
@@ -521,6 +600,7 @@ let expanse (sb : superblock) code pm =
sb.instructions;
sb.instructions <- Array.of_list (List.rev !new_order);
sb.liveins <- !liveins;
+ (*print_arrayp sb.instructions;*)
(*debug_flag := false;*)
(!code', !pm')
@@ -530,7 +610,7 @@ let rec find_last_node_reg = function
let rec traverse_list var = function
| [] -> ()
| e :: t ->
- let e' = Camlcoq.P.to_int e in
+ let e' = p2i e in
if e' > !var then var := e';
traverse_list var t
in