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 be8d929a authored by Léo Gourdin's avatar Léo Gourdin
Browse files

Adding both RV expansion methods in kvx-work

parent a6545d8f
......@@ -105,6 +105,8 @@ let option_fmadd = ref true
let option_div_i32 = ref "stsud"
let option_div_i64 = ref "stsud"
let option_fcoalesce_mem = ref true
let option_fexpanse_rtlcond = ref false
let option_fexpanse_others = ref false
let option_fforward_moves = ref false
let option_fmove_loop_invariants = ref false
let option_fnontrap_loads = ref true
......
......@@ -444,6 +444,8 @@ let cmdline_actions =
@ f_opt "madd" option_fmadd
@ f_opt "nontrap-loads" option_fnontrap_loads
@ f_opt "coalesce-mem" option_fcoalesce_mem
@ f_opt "expanse-rtlcond" option_fexpanse_rtlcond
@ f_opt "expanse-others" option_fexpanse_others
@ f_opt "all-loads-nontrap" option_all_loads_nontrap
@ f_opt "forward-moves" option_fforward_moves
(* Code generation options *)
......
......@@ -23,7 +23,6 @@ open Asm
open Asmexpandaux
open AST
open Camlcoq
open Asmgen
open! Integers
exception Error of string
......@@ -45,13 +44,11 @@ let align n a = (n + a - 1) land (-a)
(* Emit instruction sequences that set or offset a register by a constant. *)
let expand_loadimm32 dst n =
match make_immed32 n with
| Imm32_single imm -> emit (Paddiw (dst, X0, imm))
| Imm32_pair (hi, lo) -> List.iter emit (load_hilo32 dst hi lo [])
List.iter emit (Asmgen.loadimm32 dst n [])
let expand_addptrofs dst src n =
List.iter emit (addptrofs dst src n [])
List.iter emit (Asmgen.addptrofs dst src n [])
let expand_storeind_ptr src base ofs =
List.iter emit (storeind_ptr src base ofs [])
List.iter emit (Asmgen.storeind_ptr src base ofs [])
(* Built-ins. They come in two flavors:
- annotation statements: take their arguments in registers or stack
......
......@@ -86,6 +86,12 @@ Definition make_immed64 (val: int64) :=
Definition load_hilo32 (r: ireg) (hi lo: int) k :=
if Int.eq lo Int.zero then Pluiw r hi :: k
else Pluiw r hi :: Paddiw r r lo :: k.
Definition loadimm32 (r: ireg) (n: int) (k: code) :=
match make_immed32 n with
| Imm32_single imm => Paddiw r X0 imm :: k
| Imm32_pair hi lo => load_hilo32 r hi lo k
end.
Definition opimm32 (op: ireg -> ireg0 -> ireg0 -> instruction)
(opimm: ireg -> ireg0 -> int -> instruction)
......@@ -96,11 +102,23 @@ Definition opimm32 (op: ireg -> ireg0 -> ireg0 -> instruction)
end.
Definition addimm32 := opimm32 Paddw Paddiw.
Definition andimm32 := opimm32 Pandw Pandiw.
Definition orimm32 := opimm32 Porw Poriw.
Definition xorimm32 := opimm32 Pxorw Pxoriw.
Definition sltimm32 := opimm32 Psltw Psltiw.
Definition sltuimm32 := opimm32 Psltuw Psltiuw.
Definition load_hilo64 (r: ireg) (hi lo: int64) k :=
if Int64.eq lo Int64.zero then Pluil r hi :: k
else Pluil r hi :: Paddil r r lo :: k.
Definition loadimm64 (r: ireg) (n: int64) (k: code) :=
match make_immed64 n with
| Imm64_single imm => Paddil r X0 imm :: k
| Imm64_pair hi lo => load_hilo64 r hi lo k
| Imm64_large imm => Ploadli r imm :: k
end.
Definition opimm64 (op: ireg -> ireg0 -> ireg0 -> instruction)
(opimm: ireg -> ireg0 -> int64 -> instruction)
(rd rs: ireg) (n: int64) (k: code) :=
......@@ -111,6 +129,11 @@ Definition opimm64 (op: ireg -> ireg0 -> ireg0 -> instruction)
end.
Definition addimm64 := opimm64 Paddl Paddil.
Definition andimm64 := opimm64 Pandl Pandil.
Definition orimm64 := opimm64 Porl Poril.
Definition xorimm64 := opimm64 Pxorl Pxoril.
Definition sltimm64 := opimm64 Psltl Psltil.
Definition sltuimm64 := opimm64 Psltul Psltiul.
Definition addptrofs (rd rs: ireg) (n: ptrofs) (k: code) :=
if Ptrofs.eq_dec n Ptrofs.zero then
......@@ -120,6 +143,68 @@ Definition addptrofs (rd rs: ireg) (n: ptrofs) (k: code) :=
then addimm64 rd rs (Ptrofs.to_int64 n) k
else addimm32 rd rs (Ptrofs.to_int n) k.
(** Translation of conditional branches. *)
Definition transl_cbranch_int32s (cmp: comparison) (r1 r2: ireg0) (lbl: label) :=
match cmp with
| Ceq => Pbeqw r1 r2 lbl
| Cne => Pbnew r1 r2 lbl
| Clt => Pbltw r1 r2 lbl
| Cle => Pbgew r2 r1 lbl
| Cgt => Pbltw r2 r1 lbl
| Cge => Pbgew r1 r2 lbl
end.
Definition transl_cbranch_int32u (cmp: comparison) (r1 r2: ireg0) (lbl: label) :=
match cmp with
| Ceq => Pbeqw r1 r2 lbl
| Cne => Pbnew r1 r2 lbl
| Clt => Pbltuw r1 r2 lbl
| Cle => Pbgeuw r2 r1 lbl
| Cgt => Pbltuw r2 r1 lbl
| Cge => Pbgeuw r1 r2 lbl
end.
Definition transl_cbranch_int64s (cmp: comparison) (r1 r2: ireg0) (lbl: label) :=
match cmp with
| Ceq => Pbeql r1 r2 lbl
| Cne => Pbnel r1 r2 lbl
| Clt => Pbltl r1 r2 lbl
| Cle => Pbgel r2 r1 lbl
| Cgt => Pbltl r2 r1 lbl
| Cge => Pbgel r1 r2 lbl
end.
Definition transl_cbranch_int64u (cmp: comparison) (r1 r2: ireg0) (lbl: label) :=
match cmp with
| Ceq => Pbeql r1 r2 lbl
| Cne => Pbnel r1 r2 lbl
| Clt => Pbltul r1 r2 lbl
| Cle => Pbgeul r2 r1 lbl
| Cgt => Pbltul r2 r1 lbl
| Cge => Pbgeul r1 r2 lbl
end.
Definition transl_cond_float (cmp: comparison) (rd: ireg) (fs1 fs2: freg) :=
match cmp with
| Ceq => (Pfeqd rd fs1 fs2, true)
| Cne => (Pfeqd rd fs1 fs2, false)
| Clt => (Pfltd rd fs1 fs2, true)
| Cle => (Pfled rd fs1 fs2, true)
| Cgt => (Pfltd rd fs2 fs1, true)
| Cge => (Pfled rd fs2 fs1, true)
end.
Definition transl_cond_single (cmp: comparison) (rd: ireg) (fs1 fs2: freg) :=
match cmp with
| Ceq => (Pfeqs rd fs1 fs2, true)
| Cne => (Pfeqs rd fs1 fs2, false)
| Clt => (Pflts rd fs1 fs2, true)
| Cle => (Pfles rd fs1 fs2, true)
| Cgt => (Pflts rd fs2 fs1, true)
| Cge => (Pfles rd fs2 fs1, true)
end.
(** Functions to select a special register according to the op "oreg" argument from RTL *)
Definition apply_bin_oreg_ireg0 (optR: option oreg) (r1 r2: ireg0): (ireg0 * ireg0) :=
......@@ -138,6 +223,59 @@ Definition get_oreg (optR: option oreg) (r: ireg0) :=
Definition transl_cbranch
(cond: condition) (args: list mreg) (lbl: label) (k: code) :=
match cond, args with
| Ccomp c, a1 :: a2 :: nil =>
do r1 <- ireg_of a1; do r2 <- ireg_of a2;
OK (transl_cbranch_int32s c r1 r2 lbl :: k)
| Ccompu c, a1 :: a2 :: nil =>
do r1 <- ireg_of a1; do r2 <- ireg_of a2;
OK (transl_cbranch_int32u c r1 r2 lbl :: k)
| Ccompimm c n, a1 :: nil =>
do r1 <- ireg_of a1;
OK (if Int.eq n Int.zero then
transl_cbranch_int32s c r1 X0 lbl :: k
else
loadimm32 X31 n (transl_cbranch_int32s c r1 X31 lbl :: k))
| Ccompuimm c n, a1 :: nil =>
do r1 <- ireg_of a1;
OK (if Int.eq n Int.zero then
transl_cbranch_int32u c r1 X0 lbl :: k
else
loadimm32 X31 n (transl_cbranch_int32u c r1 X31 lbl :: k))
| Ccompl c, a1 :: a2 :: nil =>
do r1 <- ireg_of a1; do r2 <- ireg_of a2;
OK (transl_cbranch_int64s c r1 r2 lbl :: k)
| Ccomplu c, a1 :: a2 :: nil =>
do r1 <- ireg_of a1; do r2 <- ireg_of a2;
OK (transl_cbranch_int64u c r1 r2 lbl :: k)
| Ccomplimm c n, a1 :: nil =>
do r1 <- ireg_of a1;
OK (if Int64.eq n Int64.zero then
transl_cbranch_int64s c r1 X0 lbl :: k
else
loadimm64 X31 n (transl_cbranch_int64s c r1 X31 lbl :: k))
| Ccompluimm c n, a1 :: nil =>
do r1 <- ireg_of a1;
OK (if Int64.eq n Int64.zero then
transl_cbranch_int64u c r1 X0 lbl :: k
else
loadimm64 X31 n (transl_cbranch_int64u c r1 X31 lbl :: k))
| Ccompf c, f1 :: f2 :: nil =>
do r1 <- freg_of f1; do r2 <- freg_of f2;
let (insn, normal) := transl_cond_float c X31 r1 r2 in
OK (insn :: (if normal then Pbnew X31 X0 lbl else Pbeqw X31 X0 lbl) :: k)
| Cnotcompf c, f1 :: f2 :: nil =>
do r1 <- freg_of f1; do r2 <- freg_of f2;
let (insn, normal) := transl_cond_float c X31 r1 r2 in
OK (insn :: (if normal then Pbeqw X31 X0 lbl else Pbnew X31 X0 lbl) :: k)
| Ccompfs c, f1 :: f2 :: nil =>
do r1 <- freg_of f1; do r2 <- freg_of f2;
let (insn, normal) := transl_cond_single c X31 r1 r2 in
OK (insn :: (if normal then Pbnew X31 X0 lbl else Pbeqw X31 X0 lbl) :: k)
| Cnotcompfs c, f1 :: f2 :: nil =>
do r1 <- freg_of f1; do r2 <- freg_of f2;
let (insn, normal) := transl_cond_single c X31 r1 r2 in
OK (insn :: (if normal then Pbeqw X31 X0 lbl else Pbnew X31 X0 lbl) :: k)
| CEbeqw optR, a1 :: a2 :: nil =>
do r1 <- ireg_of a1; do r2 <- ireg_of a2;
let (r1', r2') := apply_bin_oreg_ireg0 optR r1 r2 in
......@@ -206,6 +344,133 @@ Definition transl_cbranch
Error(msg "Asmgen.transl_cond_branch")
end.
(** Translation of a condition operator. The generated code sets the
[rd] target register to 0 or 1 depending on the truth value of the
condition. *)
Definition transl_cond_int32s (cmp: comparison) (rd: ireg) (r1 r2: ireg0) (k: code) :=
match cmp with
| Ceq => Pseqw rd r1 r2 :: k
| Cne => Psnew rd r1 r2 :: k
| Clt => Psltw rd r1 r2 :: k
| Cle => Psltw rd r2 r1 :: Pxoriw rd rd Int.one :: k
| Cgt => Psltw rd r2 r1 :: k
| Cge => Psltw rd r1 r2 :: Pxoriw rd rd Int.one :: k
end.
Definition transl_cond_int32u (cmp: comparison) (rd: ireg) (r1 r2: ireg0) (k: code) :=
match cmp with
| Ceq => Pseqw rd r1 r2 :: k
| Cne => Psnew rd r1 r2 :: k
| Clt => Psltuw rd r1 r2 :: k
| Cle => Psltuw rd r2 r1 :: Pxoriw rd rd Int.one :: k
| Cgt => Psltuw rd r2 r1 :: k
| Cge => Psltuw rd r1 r2 :: Pxoriw rd rd Int.one :: k
end.
Definition transl_cond_int64s (cmp: comparison) (rd: ireg) (r1 r2: ireg0) (k: code) :=
match cmp with
| Ceq => Pseql rd r1 r2 :: k
| Cne => Psnel rd r1 r2 :: k
| Clt => Psltl rd r1 r2 :: k
| Cle => Psltl rd r2 r1 :: Pxoriw rd rd Int.one :: k
| Cgt => Psltl rd r2 r1 :: k
| Cge => Psltl rd r1 r2 :: Pxoriw rd rd Int.one :: k
end.
Definition transl_cond_int64u (cmp: comparison) (rd: ireg) (r1 r2: ireg0) (k: code) :=
match cmp with
| Ceq => Pseql rd r1 r2 :: k
| Cne => Psnel rd r1 r2 :: k
| Clt => Psltul rd r1 r2 :: k
| Cle => Psltul rd r2 r1 :: Pxoriw rd rd Int.one :: k
| Cgt => Psltul rd r2 r1 :: k
| Cge => Psltul rd r1 r2 :: Pxoriw rd rd Int.one :: k
end.
Definition transl_condimm_int32s (cmp: comparison) (rd: ireg) (r1: ireg) (n: int) (k: code) :=
if Int.eq n Int.zero then transl_cond_int32s cmp rd r1 X0 k else
match cmp with
| Ceq | Cne => xorimm32 rd r1 n (transl_cond_int32s cmp rd rd X0 k)
| Clt => sltimm32 rd r1 n k
| Cle => if Int.eq n (Int.repr Int.max_signed)
then loadimm32 rd Int.one k
else sltimm32 rd r1 (Int.add n Int.one) k
| _ => loadimm32 X31 n (transl_cond_int32s cmp rd r1 X31 k)
end.
Definition transl_condimm_int32u (cmp: comparison) (rd: ireg) (r1: ireg) (n: int) (k: code) :=
if Int.eq n Int.zero then transl_cond_int32u cmp rd r1 X0 k else
match cmp with
| Clt => sltuimm32 rd r1 n k
| _ => loadimm32 X31 n (transl_cond_int32u cmp rd r1 X31 k)
end.
Definition transl_condimm_int64s (cmp: comparison) (rd: ireg) (r1: ireg) (n: int64) (k: code) :=
if Int64.eq n Int64.zero then transl_cond_int64s cmp rd r1 X0 k else
match cmp with
| Ceq | Cne => xorimm64 rd r1 n (transl_cond_int64s cmp rd rd X0 k)
| Clt => sltimm64 rd r1 n k
| Cle => if Int64.eq n (Int64.repr Int64.max_signed)
then loadimm32 rd Int.one k
else sltimm64 rd r1 (Int64.add n Int64.one) k
| _ => loadimm64 X31 n (transl_cond_int64s cmp rd r1 X31 k)
end.
Definition transl_condimm_int64u (cmp: comparison) (rd: ireg) (r1: ireg) (n: int64) (k: code) :=
if Int64.eq n Int64.zero then transl_cond_int64u cmp rd r1 X0 k else
match cmp with
| Clt => sltuimm64 rd r1 n k
| _ => loadimm64 X31 n (transl_cond_int64u cmp rd r1 X31 k)
end.
Definition transl_cond_op
(cond: condition) (rd: ireg) (args: list mreg) (k: code) :=
match cond, args with
| Ccomp c, a1 :: a2 :: nil =>
do r1 <- ireg_of a1; do r2 <- ireg_of a2;
OK (transl_cond_int32s c rd r1 r2 k)
| Ccompu c, a1 :: a2 :: nil =>
do r1 <- ireg_of a1; do r2 <- ireg_of a2;
OK (transl_cond_int32u c rd r1 r2 k)
| Ccompimm c n, a1 :: nil =>
do r1 <- ireg_of a1;
OK (transl_condimm_int32s c rd r1 n k)
| Ccompuimm c n, a1 :: nil =>
do r1 <- ireg_of a1;
OK (transl_condimm_int32u c rd r1 n k)
| Ccompl c, a1 :: a2 :: nil =>
do r1 <- ireg_of a1; do r2 <- ireg_of a2;
OK (transl_cond_int64s c rd r1 r2 k)
| Ccomplu c, a1 :: a2 :: nil =>
do r1 <- ireg_of a1; do r2 <- ireg_of a2;
OK (transl_cond_int64u c rd r1 r2 k)
| Ccomplimm c n, a1 :: nil =>
do r1 <- ireg_of a1;
OK (transl_condimm_int64s c rd r1 n k)
| Ccompluimm c n, a1 :: nil =>
do r1 <- ireg_of a1;
OK (transl_condimm_int64u c rd r1 n k)
| Ccompf c, f1 :: f2 :: nil =>
do r1 <- freg_of f1; do r2 <- freg_of f2;
let (insn, normal) := transl_cond_float c rd r1 r2 in
OK (insn :: if normal then k else Pxoriw rd rd Int.one :: k)
| Cnotcompf c, f1 :: f2 :: nil =>
do r1 <- freg_of f1; do r2 <- freg_of f2;
let (insn, normal) := transl_cond_float c rd r1 r2 in
OK (insn :: if normal then Pxoriw rd rd Int.one :: k else k)
| Ccompfs c, f1 :: f2 :: nil =>
do r1 <- freg_of f1; do r2 <- freg_of f2;
let (insn, normal) := transl_cond_single c rd r1 r2 in
OK (insn :: if normal then k else Pxoriw rd rd Int.one :: k)
| Cnotcompfs c, f1 :: f2 :: nil =>
do r1 <- freg_of f1; do r2 <- freg_of f2;
let (insn, normal) := transl_cond_single c rd r1 r2 in
OK (insn :: if normal then Pxoriw rd rd Int.one :: k else k)
| _, _ =>
Error(msg "Asmgen.transl_cond_op")
end.
(** Translation of the arithmetic operation [r <- op(args)].
The corresponding instructions are prepended to [k]. *)
......@@ -218,6 +483,22 @@ Definition transl_op
| FR r, FR a => OK (Pfmv r a :: k)
| _ , _ => Error(msg "Asmgen.Omove")
end
| Ointconst n, nil =>
do rd <- ireg_of res;
OK (loadimm32 rd n k)
| Olongconst n, nil =>
do rd <- ireg_of res;
OK (loadimm64 rd n k)
| Ofloatconst f, nil =>
do rd <- freg_of res;
OK (if Float.eq_dec f Float.zero
then Pfcvtdw rd X0 :: k
else Ploadfi rd f :: k)
| Osingleconst f, nil =>
do rd <- freg_of res;
OK (if Float32.eq_dec f Float32.zero
then Pfcvtsw rd X0 :: k
else Ploadsi rd f :: k)
| Oaddrsymbol s ofs, nil =>
do rd <- ireg_of res;
OK (if Archi.pic_code tt && negb (Ptrofs.eq ofs Ptrofs.zero)
......@@ -227,9 +508,18 @@ Definition transl_op
do rd <- ireg_of res;
OK (addptrofs rd SP n k)
| Ocast8signed, a1 :: nil =>
do rd <- ireg_of res; do rs <- ireg_of a1;
OK (Pslliw rd rs (Int.repr 24) :: Psraiw rd rd (Int.repr 24) :: k)
| Ocast16signed, a1 :: nil =>
do rd <- ireg_of res; do rs <- ireg_of a1;
OK (Pslliw rd rs (Int.repr 16) :: Psraiw rd rd (Int.repr 16) :: k)
| Oadd, a1 :: a2 :: nil =>
do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
OK (Paddw rd rs1 rs2 :: k)
| Oaddimm n, a1 :: nil =>
do rd <- ireg_of res; do rs <- ireg_of a1;
OK (addimm32 rd rs n k)
| Oneg, a1 :: nil =>
do rd <- ireg_of res; do rs <- ireg_of a1;
OK (Psubw rd X0 rs :: k)
......@@ -260,12 +550,21 @@ Definition transl_op
| Oand, a1 :: a2 :: nil =>
do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
OK (Pandw rd rs1 rs2 :: k)
| Oandimm n, a1 :: nil =>
do rd <- ireg_of res; do rs <- ireg_of a1;
OK (andimm32 rd rs n k)
| Oor, a1 :: a2 :: nil =>
do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
OK (Porw rd rs1 rs2 :: k)
| Oorimm n, a1 :: nil =>
do rd <- ireg_of res; do rs <- ireg_of a1;
OK (orimm32 rd rs n k)
| Oxor, a1 :: a2 :: nil =>
do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
OK (Pxorw rd rs1 rs2 :: k)
| Oxorimm n, a1 :: nil =>
do rd <- ireg_of res; do rs <- ireg_of a1;
OK (xorimm32 rd rs n k)
| Oshl, a1 :: a2 :: nil =>
do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
OK (Psllw rd rs1 rs2 :: k)
......@@ -284,6 +583,19 @@ Definition transl_op
| Oshruimm n, a1 :: nil =>
do rd <- ireg_of res; do rs <- ireg_of a1;
OK (Psrliw rd rs n :: k)
| Oshrximm n, a1 :: nil =>
do rd <- ireg_of res; do rs <- ireg_of a1;
OK (if Int.eq n Int.zero
then Pmv rd rs :: k
else if Int.eq n Int.one
then Psrliw X31 rs (Int.repr 31) ::
Paddw X31 rs X31 ::
Psraiw rd X31 Int.one :: k
else Psraiw X31 rs (Int.repr 31) ::
Psrliw X31 X31 (Int.sub Int.iwordsize n) ::
Paddw X31 rs X31 ::
Psraiw rd X31 n :: k)
(* [Omakelong], [Ohighlong] should not occur *)
| Olowlong, a1 :: nil =>
do rd <- ireg_of res; do rs <- ireg_of a1;
......@@ -292,9 +604,16 @@ Definition transl_op
do rd <- ireg_of res; do rs <- ireg_of a1;
assertion (ireg_eq rd rs);
OK (Pcvtw2l rd :: k)
| Ocast32unsigned, a1 :: nil =>
do rd <- ireg_of res; do rs <- ireg_of a1;
assertion (ireg_eq rd rs);
OK (Pcvtw2l rd :: Psllil rd rd (Int.repr 32) :: Psrlil rd rd (Int.repr 32) :: k)
| Oaddl, a1 :: a2 :: nil =>
do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
OK (Paddl rd rs1 rs2 :: k)
| Oaddlimm n, a1 :: nil =>
do rd <- ireg_of res; do rs <- ireg_of a1;
OK (addimm64 rd rs n k)
| Onegl, a1 :: nil =>
do rd <- ireg_of res; do rs <- ireg_of a1;
OK (Psubl rd X0 rs :: k)
......@@ -325,12 +644,21 @@ Definition transl_op
| Oandl, a1 :: a2 :: nil =>
do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
OK (Pandl rd rs1 rs2 :: k)
| Oandlimm n, a1 :: nil =>
do rd <- ireg_of res; do rs <- ireg_of a1;
OK (andimm64 rd rs n k)
| Oorl, a1 :: a2 :: nil =>
do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
OK (Porl rd rs1 rs2 :: k)
| Oorlimm n, a1 :: nil =>
do rd <- ireg_of res; do rs <- ireg_of a1;
OK (orimm64 rd rs n k)
| Oxorl, a1 :: a2 :: nil =>
do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
OK (Pxorl rd rs1 rs2 :: k)
| Oxorlimm n, a1 :: nil =>
do rd <- ireg_of res; do rs <- ireg_of a1;
OK (xorimm64 rd rs n k)
| Oshll, a1 :: a2 :: nil =>
do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
OK (Pslll rd rs1 rs2 :: k)
......@@ -349,6 +677,19 @@ Definition transl_op
| Oshrluimm n, a1 :: nil =>
do rd <- ireg_of res; do rs <- ireg_of a1;
OK (Psrlil rd rs n :: k)
| Oshrxlimm n, a1 :: nil =>
do rd <- ireg_of res; do rs <- ireg_of a1;
OK (if Int.eq n Int.zero
then Pmv rd rs :: k
else if Int.eq n Int.one
then Psrlil X31 rs (Int.repr 63) ::
Paddl X31 rs X31 ::
Psrail rd X31 Int.one :: k
else Psrail X31 rs (Int.repr 63) ::
Psrlil X31 X31 (Int.sub Int64.iwordsize' n) ::
Paddl X31 rs X31 ::
Psrail rd X31 n :: k)
| Onegf, a1 :: nil =>
do rd <- freg_of res; do rs <- freg_of a1;
OK (Pfnegd rd rs :: k)
......@@ -443,6 +784,9 @@ Definition transl_op
| Osingleoflongu, a1 :: nil =>
do rd <- freg_of res; do rs <- ireg_of a1;
OK (Pfcvtslu rd rs :: k)
| Ocmp cmp, _ =>
do rd <- ireg_of res;
transl_cond_op cmp rd args k
(* Instructions expanded in RTL *)
| OEseqw optR, a1 :: a2 :: nil =>
......
......@@ -115,6 +115,14 @@ Qed.
Section TRANSL_LABEL.
Remark loadimm32_label:
forall r n k, tail_nolabel k (loadimm32 r n k).
Proof.
intros; unfold loadimm32. destruct (make_immed32 n); TailNoLabel.
unfold load_hilo32. destruct (Int.eq lo Int.zero); TailNoLabel.
Qed.
Hint Resolve loadimm32_label: labels.
Remark opimm32_label:
forall op opimm r1 r2 n k,
(forall r1 r2 r3, nolabel (op r1 r2 r3)) ->
......@@ -126,6 +134,14 @@ Proof.
Qed.
Hint Resolve opimm32_label: labels.
Remark loadimm64_label:
forall r n k, tail_nolabel k (loadimm64 r n k).
Proof.
intros; unfold loadimm64. destruct (make_immed64 n); TailNoLabel.
unfold load_hilo64. destruct (Int64.eq lo Int64.zero); TailNoLabel.
Qed.
Hint Resolve loadimm64_label: labels.
Remark opimm64_label:
forall op opimm r1 r2 n k,
(forall r1 r2 r3, nolabel (op r1 r2 r3)) ->
......@@ -145,25 +161,165 @@ Proof.
Qed.
Hint Resolve addptrofs_label: labels.
Remark transl_cond_float_nolabel:
forall c r1 r2 r3 insn normal,
transl_cond_float c r1 r2 r3 = (insn, normal) -> nolabel insn.
Proof.
unfold transl_cond_float; intros. destruct c; inv H; exact I.
Qed.
Remark transl_cond_single_nolabel:
forall c r1 r2 r3 insn normal,
transl_cond_single c r1 r2 r3 = (insn, normal) -> nolabel insn.
Proof.
unfold transl_cond_single; intros. destruct c; inv H; exact I.
Qed.
Remark transl_cbranch_label:
forall cond args lbl k c,
transl_cbranch cond args lbl k = OK c -> tail_nolabel k c.
Proof.
intros. unfold transl_cbranch in H; destruct cond; TailNoLabel.
all: destruct optR as [[]|]; simpl in *; TailNoLabel.
- destruct c0; simpl; TailNoLabel.
- destruct c0; simpl; TailNoLabel.
- destruct (Int.eq n Int.zero).
destruct c0; simpl; TailNoLabel.
apply tail_nolabel_trans with (transl_cbranch_int32s c0 x X31 lbl :: k).
auto with labels. destruct c0; simpl; TailNoLabel.
- destruct (Int.eq n Int.zero).
destruct c0; simpl; TailNoLabel.
apply tail_nolabel_trans with (transl_cbranch_int32u c0 x X31 lbl :: k).
auto with labels. destruct c0; simpl; TailNoLabel.
- destruct c0; simpl; TailNoLabel.
- destruct c0; simpl; TailNoLabel.
- destruct (Int64.eq n Int64.zero).
destruct c0; simpl; TailNoLabel.
apply tail_nolabel_trans with (transl_cbranch_int64s c0 x X31 lbl :: k).
auto with labels. destruct c0; simpl; TailNoLabel.
- destruct (Int64.eq n Int64.zero).
destruct c0; simpl; TailNoLabel.
apply tail_nolabel_trans with (transl_cbranch_int64u c0 x X31 lbl :: k).
auto with labels. destruct c0; simpl; TailNoLabel.
- destruct (transl_cond_float c0 X31 x x0) as [insn normal] eqn:F; inv EQ2.
apply tail_nolabel_cons. eapply transl_cond_float_nolabel; eauto.
destruct normal; TailNoLabel.
- destruct (transl_cond_float c0 X31 x x0) as [insn normal] eqn:F; inv EQ2.
apply tail_nolabel_cons. eapply transl_cond_float_nolabel; eauto.
destruct normal; TailNoLabel.
- destruct (transl_cond_single c0 X31 x x0) as <