Vous avez reçu un message "Your GitLab account has been locked ..." ? Pas d'inquiétude : lisez cet article https://docs.gricad-pages.univ-grenoble-alpes.fr/help/unlock/

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

Try to save values in virtual registers during expansion

parent dae202e1
......@@ -29,6 +29,10 @@ let r2p () = Camlcoq.P.of_int !reg
let n2p () = Camlcoq.P.of_int !node
let r2pi () =
reg := !reg + 1;
r2p ()
let n2pi () =
node := !node + 1;
n2p ()
......@@ -36,27 +40,27 @@ 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
if Int.eq lo Int.zero then Iop (OEluiw (hi, is_long), [ a1 ], dest, succ) :: k
else
Iop (OEluiw (hi, is_long), [a1], dest, n2pi ())
:: Iop (Oaddimm lo, [ dest ], dest, succ)
:: k
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
if Int64.eq lo Int64.zero then Iop (OEluil hi, [ a1 ], dest, succ) :: k
else
Iop (OEluil hi, [a1], dest, n2pi ())
:: Iop (Oaddlimm lo, [ dest ], dest, succ)
:: k
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 =
match make_immed32 n with
| Imm32_single imm -> Iop (OEaddiwr0 (imm, is_long), [a1], dest, succ) :: k
| 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
let loadimm64 a1 dest n succ k =
match make_immed64 n with
| Imm64_single imm -> Iop (OEaddilr0 imm, [a1], dest, succ) :: k
| 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
......@@ -72,28 +76,28 @@ let opimm32 a1 dest n succ is_long k op opimm =
match make_immed32 n with
| Imm32_single imm -> Iop (get_opimm imm opimm, [ a1 ], dest, succ) :: k
| Imm32_pair (hi, lo) ->
reg := !reg + 1;
load_hilo32 a1 (r2p ()) hi lo (n2pi ()) is_long
(Iop (op, [ a1; r2p () ], dest, succ) :: k)
let r = r2pi () in
load_hilo32 a1 r hi lo (n2pi ()) is_long
(Iop (op, [ a1; r ], dest, succ) :: k)
let opimm64 a1 dest n succ k op opimm =
match make_immed64 n with
| Imm64_single imm -> Iop (get_opimm imm opimm, [ a1 ], dest, succ) :: k
| Imm64_pair (hi, lo) ->
reg := !reg + 1;
load_hilo64 a1 (r2p ()) hi lo (n2pi ())
(Iop (op, [ a1; r2p () ], dest, succ) :: k)
let r = r2pi () in
load_hilo64 a1 r hi lo (n2pi ()) (Iop (op, [ a1; r ], dest, succ) :: k)
| Imm64_large imm ->
reg := !reg + 1;
Iop (OEloadli imm, [], r2p (), n2pi ())
:: Iop (op, [ a1; r2p () ], dest, succ)
:: k
let r = r2pi () in
Iop (OEloadli imm, [], r, n2pi ()) :: 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 is_long k =
opimm32 a1 dest n succ is_long k Oxor Xoriw
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 is_long k =
opimm32 a1 dest n succ is_long k (OEsltw None) Sltiw
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 is_long k =
opimm32 a1 dest n succ is_long k (OEsltuw None) Sltiuw
let xorimm64 a1 dest n succ k = opimm64 a1 dest n succ k Oxorl Xoril
......@@ -152,14 +156,14 @@ let cond_int32s is_x0 cmp a1 a2 dest succ k =
| Cne -> Iop (OEsnew optR0, [ a1; a2 ], dest, succ) :: k
| Clt -> Iop (OEsltw optR0, [ a1; a2 ], dest, succ) :: k
| Cle ->
Iop (OEsltw optR0, [ a2; a1 ], dest, n2pi ())
:: Iop (OExoriw Int.one, [ dest ], dest, succ)
:: k
let r = r2pi () in
Iop (OEsltw optR0, [ a2; a1 ], r, n2pi ())
:: Iop (OExoriw Int.one, [ r ], dest, succ) :: k
| Cgt -> Iop (OEsltw optR0, [ a2; a1 ], dest, succ) :: k
| Cge ->
Iop (OEsltw optR0, [ a1; a2 ], dest, n2pi ())
:: Iop (OExoriw Int.one, [ dest ], dest, succ)
:: k
let r = r2pi () in
Iop (OEsltw optR0, [ a1; a2 ], r, n2pi ())
:: Iop (OExoriw Int.one, [ r ], dest, succ) :: k
let cond_int32u is_x0 cmp a1 a2 dest succ k =
let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in
......@@ -168,14 +172,14 @@ let cond_int32u is_x0 cmp a1 a2 dest succ k =
| Cne -> Iop (OEsneuw optR0, [ a1; a2 ], dest, succ) :: k
| Clt -> Iop (OEsltuw optR0, [ a1; a2 ], dest, succ) :: k
| Cle ->
Iop (OEsltuw optR0, [ a2; a1 ], dest, n2pi ())
:: Iop (OExoriw Int.one, [ dest ], dest, succ)
:: k
let r = r2pi () in
Iop (OEsltuw optR0, [ a2; a1 ], r, n2pi ())
:: Iop (OExoriw Int.one, [ r ], dest, succ) :: k
| Cgt -> Iop (OEsltuw optR0, [ a2; a1 ], dest, succ) :: k
| Cge ->
Iop (OEsltuw optR0, [ a1; a2 ], dest, n2pi ())
:: Iop (OExoriw Int.one, [ dest ], dest, succ)
:: k
let r = r2pi () in
Iop (OEsltuw optR0, [ a1; a2 ], r, n2pi ())
:: Iop (OExoriw Int.one, [ r ], dest, succ) :: k
let cond_int64s is_x0 cmp a1 a2 dest succ k =
let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in
......@@ -184,14 +188,14 @@ let cond_int64s is_x0 cmp a1 a2 dest succ k =
| Cne -> Iop (OEsnel optR0, [ a1; a2 ], dest, succ) :: k
| Clt -> Iop (OEsltl optR0, [ a1; a2 ], dest, succ) :: k
| Cle ->
Iop (OEsltl optR0, [ a2; a1 ], dest, n2pi ())
:: Iop (OExoriw Int.one, [ dest ], dest, succ)
:: k
let r = r2pi () in
Iop (OEsltl optR0, [ a2; a1 ], r, n2pi ())
:: Iop (OExoriw Int.one, [ r ], dest, succ) :: k
| Cgt -> Iop (OEsltl optR0, [ a2; a1 ], dest, succ) :: k
| Cge ->
Iop (OEsltl optR0, [ a1; a2 ], dest, n2pi ())
:: Iop (OExoriw Int.one, [ dest ], dest, succ)
:: k
let r = r2pi () in
Iop (OEsltl optR0, [ a1; a2 ], r, n2pi ())
:: Iop (OExoriw Int.one, [ r ], dest, succ) :: k
let cond_int64u is_x0 cmp a1 a2 dest succ k =
let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in
......@@ -200,14 +204,14 @@ let cond_int64u is_x0 cmp a1 a2 dest succ k =
| Cne -> Iop (OEsneul optR0, [ a1; a2 ], dest, succ) :: k
| Clt -> Iop (OEsltul optR0, [ a1; a2 ], dest, succ) :: k
| Cle ->
Iop (OEsltul optR0, [ a2; a1 ], dest, n2pi ())
:: Iop (OExoriw Int.one, [ dest ], dest, succ)
:: k
let r = r2pi () in
Iop (OEsltul optR0, [ a2; a1 ], r, n2pi ())
:: Iop (OExoriw Int.one, [ r ], dest, succ) :: k
| Cgt -> Iop (OEsltul optR0, [ a2; a1 ], dest, succ) :: k
| Cge ->
Iop (OEsltul optR0, [ a1; a2 ], dest, n2pi ())
:: Iop (OExoriw Int.one, [ dest ], dest, succ)
:: k
let r = r2pi () in
Iop (OEsltul optR0, [ a1; a2 ], r, n2pi ())
:: Iop (OExoriw Int.one, [ r ], dest, succ) :: k
let is_normal_cmp = function Cne -> false | _ -> true
......@@ -231,47 +235,48 @@ let cond_single cmp f1 f2 dest succ =
let expanse_cbranchimm_int32s cmp a1 n info succ1 succ2 k =
if Int.eq n Int.zero then cbranch_int32s true cmp a1 a1 info succ1 succ2 k
else (
reg := !reg + 1;
loadimm32 a1 (r2p ()) n (n2pi ()) false
(cbranch_int32s false cmp a1 (r2p ()) 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 expanse_cbranchimm_int32u cmp a1 n info succ1 succ2 k =
if Int.eq n Int.zero then cbranch_int32u true cmp a1 a1 info succ1 succ2 k
else (
reg := !reg + 1;
loadimm32 a1 (r2p ()) n (n2pi ()) false
(cbranch_int32u false cmp a1 (r2p ()) 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 expanse_cbranchimm_int64s cmp a1 n info succ1 succ2 k =
if Int64.eq n Int64.zero then cbranch_int64s true cmp a1 a1 info succ1 succ2 k
else (
reg := !reg + 1;
loadimm64 a1 (r2p ()) n (n2pi ())
(cbranch_int64s false cmp a1 (r2p ()) 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 expanse_cbranchimm_int64u cmp a1 n info succ1 succ2 k =
if Int64.eq n Int64.zero then cbranch_int64u true cmp a1 a1 info succ1 succ2 k
else (
reg := !reg + 1;
loadimm64 a1 (r2p ()) n (n2pi ())
(cbranch_int64u false cmp a1 (r2p ()) 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 expanse_condimm_int32s cmp a1 n dest succ k =
if Int.eq n Int.zero then cond_int32s true cmp a1 a1 dest succ k
else
match cmp with
| Ceq | Cne ->
xorimm32 a1 dest n (n2pi ()) false
(cond_int32s true cmp dest dest dest succ k)
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
| Cle ->
if Int.eq n (Int.repr Int.max_signed) then loadimm32 a1 dest Int.one succ false k
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
| _ ->
reg := !reg + 1;
loadimm32 a1 (r2p ()) n (n2pi ()) false
(cond_int32s false cmp a1 (r2p ()) dest succ k)
let r = r2pi () in
loadimm32 a1 r n (n2pi ()) false
(cond_int32s false cmp a1 r dest succ k)
let expanse_condimm_int32u cmp a1 n dest succ k =
if Int.eq n Int.zero then cond_int32u true cmp a1 a1 dest succ k
......@@ -279,27 +284,25 @@ let expanse_condimm_int32u cmp a1 n dest succ k =
match cmp with
| Clt -> sltuimm32 a1 dest n succ false k
| _ ->
reg := !reg + 1;
loadimm32 a1 (r2p ()) n (n2pi ()) false
(cond_int32u false cmp a1 (r2p ()) dest succ k)
let r = r2pi () in
loadimm32 a1 r n (n2pi ()) false
(cond_int32u false cmp a1 r dest succ k)
let expanse_condimm_int64s cmp a1 n dest succ k =
if Int64.eq n Int64.zero then cond_int64s true cmp a1 a1 dest succ k
else
match cmp with
| Ceq | Cne ->
reg := !reg + 1;
xorimm64 a1 (r2p ()) n (n2pi ())
(cond_int64s true cmp (r2p ()) (r2p ()) dest succ k)
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
| 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
| _ ->
reg := !reg + 1;
loadimm64 a1 (r2p ()) n (n2pi ())
(cond_int64s false cmp a1 (r2p ()) dest succ k)
let r = r2pi () in
loadimm64 a1 r n (n2pi ()) (cond_int64s false cmp a1 r dest succ k)
let expanse_condimm_int64u cmp a1 n dest succ k =
if Int64.eq n Int64.zero then cond_int64u true cmp a1 a1 dest succ k
......@@ -307,9 +310,8 @@ let expanse_condimm_int64u cmp a1 n dest succ k =
match cmp with
| Clt -> sltuimm64 a1 dest n succ k
| _ ->
reg := !reg + 1;
loadimm64 a1 (r2p ()) n (n2pi ())
(cond_int64u false cmp a1 (r2p ()) dest succ k)
let r = r2pi () in
loadimm64 a1 r n (n2pi ()) (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
......@@ -320,14 +322,14 @@ let expanse_cond_fp cnot fn_cond cmp f1 f2 dest succ k =
:: (if normal' then k else Iop (OExoriw Int.one, [ dest ], dest, succ) :: k)
let expanse_cbranch_fp cnot fn_cond cmp f1 f2 info succ1 succ2 k =
reg := !reg + 1;
let r = r2pi () in
let normal = is_normal_cmp cmp in
let normal' = if cnot then not normal else normal in
let insn = fn_cond cmp f1 f2 (r2p ()) (n2pi ()) in
let insn = fn_cond cmp f1 f2 r (n2pi ()) in
insn
:: (if normal' then
Icond (CEbnew (Some false), [ r2p (); r2p () ], succ1, succ2, info)
else Icond (CEbeqw (Some false), [ r2p (); r2p () ], succ1, succ2, info))
::
(if normal' then Icond (CEbnew (Some false), [ r; r ], succ1, succ2, info)
else Icond (CEbeqw (Some false), [ r; r ], succ1, succ2, info))
:: k
let get_regindent = function Coq_inr _ -> [] | Coq_inl r -> [ r ]
......@@ -352,8 +354,15 @@ let write_initial_node initial code' 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; pre_output_regs = path.pre_output_regs; output_regs = path.output_regs } in
let npsize = Camlcoq.Nat.of_int (esize + Camlcoq.Nat.to_int path.psize) in
let path' =
{
psize = npsize;
input_regs = path.input_regs;
pre_output_regs = path.pre_output_regs;
output_regs = path.output_regs;
}
in
pm' := PTree.set initial path' !pm'
let rec write_tree exp current code' new_order =
......@@ -500,7 +509,9 @@ 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 =
Camlcoq.P.of_int (!node - (List.length !exp - 1))
in
liveins := PTree.set new_branch_pc lives !liveins;
liveins := PTree.remove n !liveins
| _ -> ());
......
......@@ -64,6 +64,10 @@ let print_condition reg pp = function
fprintf pp "CEbeqw"; (get_optR0_s Ceq reg pp r1 r2 optR0)
| (CEbnew optR0, [r1;r2]) ->
fprintf pp "CEbnew"; (get_optR0_s Cne reg pp r1 r2 optR0)
| (CEbequw optR0, [r1;r2]) ->
fprintf pp "CEbequw"; (get_optR0_s Ceq reg pp r1 r2 optR0)
| (CEbneuw optR0, [r1;r2]) ->
fprintf pp "CEbneuw"; (get_optR0_s Cne reg pp r1 r2 optR0)
| (CEbltw optR0, [r1;r2]) ->
fprintf pp "CEbltw"; (get_optR0_s Clt reg pp r1 r2 optR0)
| (CEbltuw optR0, [r1;r2]) ->
......@@ -76,6 +80,10 @@ let print_condition reg pp = function
fprintf pp "CEbeql"; (get_optR0_s Ceq reg pp r1 r2 optR0)
| (CEbnel optR0, [r1;r2]) ->
fprintf pp "CEbnel"; (get_optR0_s Cne reg pp r1 r2 optR0)
| (CEbequl optR0, [r1;r2]) ->
fprintf pp "CEbequl"; (get_optR0_s Ceq reg pp r1 r2 optR0)
| (CEbneul optR0, [r1;r2]) ->
fprintf pp "CEbneul"; (get_optR0_s Cne reg pp r1 r2 optR0)
| (CEbltl optR0, [r1;r2]) ->
fprintf pp "CEbltl"; (get_optR0_s Clt reg pp r1 r2 optR0)
| (CEbltul optR0, [r1;r2]) ->
......@@ -187,23 +195,27 @@ let print_operation reg pp = function
| Ocmp c, args -> print_condition reg pp (c, args)
| OEseqw optR0, [r1;r2] -> fprintf pp "OEseqw"; (get_optR0_s Ceq reg pp r1 r2 optR0)
| OEsnew optR0, [r1;r2] -> fprintf pp "OEsnew"; (get_optR0_s Cne reg pp r1 r2 optR0)
| OEsequw optR0, [r1;r2] -> fprintf pp "OEsequw"; (get_optR0_s Ceq reg pp r1 r2 optR0)
| OEsneuw optR0, [r1;r2] -> fprintf pp "OEsneuw"; (get_optR0_s Cne reg pp r1 r2 optR0)
| OEsltw optR0, [r1;r2] -> fprintf pp "OEsltw"; (get_optR0_s Clt reg pp r1 r2 optR0)
| OEsltuw optR0, [r1;r2] -> fprintf pp "OEsltuw"; (get_optR0_s Clt reg pp r1 r2 optR0)
| OEsltiw n, [r1] -> fprintf pp "OEsltiw(%a,%ld)" reg r1 (camlint_of_coqint n)
| OEsltiuw n, [r1] -> fprintf pp "OEsltiuw(%a,%ld)" reg r1 (camlint_of_coqint n)
| OExoriw n, [r1] -> fprintf pp "OExoriw(%a,%ld)" reg r1 (camlint_of_coqint n)
| OEluiw (n, _), [] -> fprintf pp "OEluiw(%ld)" (camlint_of_coqint n)
| OEaddiwr0 (n, _), [] -> fprintf pp "OEaddiwr0(%ld,X0)" (camlint_of_coqint n)
| OEluiw (n, _), _ -> fprintf pp "OEluiw(%ld)" (camlint_of_coqint n)
| OEaddiwr0 (n, _), _ -> fprintf pp "OEaddiwr0(%ld,X0)" (camlint_of_coqint n)
| OEseql optR0, [r1;r2] -> fprintf pp "OEseql"; (get_optR0_s Ceq reg pp r1 r2 optR0)
| OEsnel optR0, [r1;r2] -> fprintf pp "OEsnel"; (get_optR0_s Cne reg pp r1 r2 optR0)
| OEsequl optR0, [r1;r2] -> fprintf pp "OEsequl"; (get_optR0_s Ceq reg pp r1 r2 optR0)
| OEsneul optR0, [r1;r2] -> fprintf pp "OEsneul"; (get_optR0_s Cne reg pp r1 r2 optR0)
| OEsltl optR0, [r1;r2] -> fprintf pp "OEsltl"; (get_optR0_s Clt reg pp r1 r2 optR0)
| OEsltul optR0, [r1;r2] -> fprintf pp "OEsltul"; (get_optR0_s Clt reg pp r1 r2 optR0)
| OEsltil n, [r1] -> fprintf pp "OEsltil(%a,%ld)" reg r1 (camlint_of_coqint n)
| OEsltiul n, [r1] -> fprintf pp "OEsltiul(%a,%ld)" reg r1 (camlint_of_coqint n)
| OExoril n, [r1] -> fprintf pp "OExoril(%a,%ld)" reg r1 (camlint_of_coqint n)
| OEluil n, [] -> fprintf pp "OEluil(%ld)" (camlint_of_coqint n)
| OEaddilr0 n, [] -> fprintf pp "OEaddilr0(%ld,X0)" (camlint_of_coqint n)
| OEloadli n, [] -> fprintf pp "OEloadli(%ld)" (camlint_of_coqint n)
| OEluil n, _ -> fprintf pp "OEluil(%ld)" (camlint_of_coqint n)
| OEaddilr0 n, _ -> fprintf pp "OEaddilr0(%ld,X0)" (camlint_of_coqint n)
| OEloadli n, _ -> fprintf pp "OEloadli(%ld)" (camlint_of_coqint n)
| OEfeqd, [r1;r2] -> fprintf pp "OEfeqd(%a,%s,%a)" reg r1 (comparison_name Ceq) reg r2
| OEfltd, [r1;r2] -> fprintf pp "OEfltd(%a,%s,%a)" reg r1 (comparison_name Clt) reg r2
| OEfled, [r1;r2] -> fprintf pp "OEfled(%a,%s,%a)" reg r1 (comparison_name Cle) reg r2
......
......@@ -303,7 +303,7 @@ let rec do_schedule code pm = function
debug "\nSchedule to apply: "; print_arrayp schedule;
debug "\nNew Code: "; print_code new_code;
debug "\n";
(* debug_flag := false; *)
(*debug_flag := false; *)
do_schedule new_code pm lsb
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