diff options
Diffstat (limited to 'riscV')
| -rw-r--r-- | riscV/Asmexpand.ml | 9 | ||||
| -rw-r--r-- | riscV/Asmgen.v | 344 | ||||
| -rw-r--r-- | riscV/Asmgenproof.v | 162 | ||||
| -rw-r--r-- | riscV/Asmgenproof1.v | 919 | ||||
| -rw-r--r-- | riscV/ExpansionOracle.ml | 140 | ||||
| -rw-r--r-- | riscV/RTLpathSE_simplify.v | 10 |
6 files changed, 111 insertions, 1473 deletions
diff --git a/riscV/Asmexpand.ml b/riscV/Asmexpand.ml index c5cd6817..3f9d3359 100644 --- a/riscV/Asmexpand.ml +++ b/riscV/Asmexpand.ml @@ -23,6 +23,7 @@ open Asm open Asmexpandaux open AST open Camlcoq +open Asmgen open! Integers exception Error of string @@ -44,11 +45,13 @@ 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 = - List.iter emit (Asmgen.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 []) let expand_addptrofs dst src n = - List.iter emit (Asmgen.addptrofs dst src n []) + List.iter emit (addptrofs dst src n []) let expand_storeind_ptr src base ofs = - List.iter emit (Asmgen.storeind_ptr src base ofs []) + List.iter emit (storeind_ptr src base ofs []) (* Built-ins. They come in two flavors: - annotation statements: take their arguments in registers or stack diff --git a/riscV/Asmgen.v b/riscV/Asmgen.v index 3e84e950..da6c0101 100644 --- a/riscV/Asmgen.v +++ b/riscV/Asmgen.v @@ -86,12 +86,6 @@ 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) @@ -102,23 +96,11 @@ 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) := @@ -129,11 +111,6 @@ 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 @@ -143,68 +120,6 @@ 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) := @@ -223,59 +138,6 @@ 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 @@ -344,133 +206,6 @@ 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]. *) @@ -483,22 +218,6 @@ 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) @@ -508,18 +227,9 @@ 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) @@ -550,21 +260,12 @@ 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) @@ -583,19 +284,6 @@ 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; @@ -604,16 +292,9 @@ 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) @@ -644,21 +325,12 @@ 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) @@ -677,19 +349,6 @@ 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) @@ -784,9 +443,6 @@ 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 => diff --git a/riscV/Asmgenproof.v b/riscV/Asmgenproof.v index 509eac94..4af8352c 100644 --- a/riscV/Asmgenproof.v +++ b/riscV/Asmgenproof.v @@ -115,14 +115,6 @@ 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)) -> @@ -134,14 +126,6 @@ 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)) -> @@ -161,165 +145,25 @@ 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. -- 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 [insn normal] eqn:F; inv EQ2. - apply tail_nolabel_cons. eapply transl_cond_single_nolabel; eauto. - destruct normal; TailNoLabel. -- destruct (transl_cond_single c0 X31 x x0) as [insn normal] eqn:F; inv EQ2. - apply tail_nolabel_cons. eapply transl_cond_single_nolabel; eauto. - destruct normal; TailNoLabel. -- destruct optR as [[]|]; simpl in *; TailNoLabel. -- destruct optR as [[]|]; simpl in *; TailNoLabel. -- destruct optR as [[]|]; simpl in *; TailNoLabel. -- destruct optR as [[]|]; simpl in *; TailNoLabel. -- destruct optR as [[]|]; simpl in *; TailNoLabel. -- destruct optR as [[]|]; simpl in *; TailNoLabel. -- destruct optR as [[]|]; simpl in *; TailNoLabel. -- destruct optR as [[]|]; simpl in *; TailNoLabel. -- destruct optR as [[]|]; simpl in *; TailNoLabel. -- destruct optR as [[]|]; simpl in *; TailNoLabel. -- destruct optR as [[]|]; simpl in *; TailNoLabel. -- destruct optR as [[]|]; simpl in *; TailNoLabel. -- destruct optR as [[]|]; simpl in *; TailNoLabel. -- destruct optR as [[]|]; simpl in *; TailNoLabel. -- destruct optR as [[]|]; simpl in *; TailNoLabel. -- destruct optR as [[]|]; simpl in *; TailNoLabel. + all: destruct optR as [[]|]; simpl in *; TailNoLabel. Qed. -Remark transl_cond_op_label: - forall cond args r k c, - transl_cond_op cond r args k = OK c -> tail_nolabel k c. -Proof. - intros. unfold transl_cond_op in H; destruct cond; TailNoLabel. -- destruct c0; simpl; TailNoLabel. -- destruct c0; simpl; TailNoLabel. -- unfold transl_condimm_int32s. - destruct (Int.eq n Int.zero). -+ destruct c0; simpl; TailNoLabel. -+ destruct c0; simpl. -* eapply tail_nolabel_trans; [apply opimm32_label; intros; exact I | TailNoLabel]. -* eapply tail_nolabel_trans; [apply opimm32_label; intros; exact I | TailNoLabel]. -* apply opimm32_label; intros; exact I. -* destruct (Int.eq n (Int.repr Int.max_signed)). apply loadimm32_label. apply opimm32_label; intros; exact I. -* eapply tail_nolabel_trans. apply loadimm32_label. TailNoLabel. -* eapply tail_nolabel_trans. apply loadimm32_label. TailNoLabel. -- unfold transl_condimm_int32u. - destruct (Int.eq n Int.zero). -+ destruct c0; simpl; TailNoLabel. -+ destruct c0; simpl; - try (eapply tail_nolabel_trans; [apply loadimm32_label | TailNoLabel]). - apply opimm32_label; intros; exact I. -- destruct c0; simpl; TailNoLabel. - - destruct c0; simpl; TailNoLabel. -- unfold transl_condimm_int64s. - destruct (Int64.eq n Int64.zero). -+ destruct c0; simpl; TailNoLabel. -+ destruct c0; simpl. -* eapply tail_nolabel_trans; [apply opimm64_label; intros; exact I | TailNoLabel]. -* eapply tail_nolabel_trans; [apply opimm64_label; intros; exact I | TailNoLabel]. -* apply opimm64_label; intros; exact I. -* destruct (Int64.eq n (Int64.repr Int64.max_signed)). apply loadimm32_label. apply opimm64_label; intros; exact I. -* eapply tail_nolabel_trans. apply loadimm64_label. TailNoLabel. -* eapply tail_nolabel_trans. apply loadimm64_label. TailNoLabel. -- unfold transl_condimm_int64u. - destruct (Int64.eq n Int64.zero). -+ destruct c0; simpl; TailNoLabel. -+ destruct c0; simpl; - try (eapply tail_nolabel_trans; [apply loadimm64_label | TailNoLabel]). - apply opimm64_label; intros; exact I. -- destruct (transl_cond_float c0 r 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 r 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 r x x0) as [insn normal] eqn:F; inv EQ2. - apply tail_nolabel_cons. eapply transl_cond_single_nolabel; eauto. - destruct normal; TailNoLabel. -- destruct (transl_cond_single c0 r x x0) as [insn normal] eqn:F; inv EQ2. - apply tail_nolabel_cons. eapply transl_cond_single_nolabel; eauto. - destruct normal; TailNoLabel. - Qed. - Remark transl_op_label: forall op args r k c, transl_op op args r k = OK c -> tail_nolabel k c. Proof. Opaque Int.eq. - unfold transl_op; intros; destruct op; TailNoLabel. + unfold transl_op; intros; destruct op; TailNoLabel; + try (destruct optR as [[]|]; simpl in *; TailNoLabel). - destruct (preg_of r); try discriminate; destruct (preg_of m); inv H; TailNoLabel. -- destruct (Float.eq_dec n Float.zero); TailNoLabel. -- destruct (Float32.eq_dec n Float32.zero); TailNoLabel. - destruct (Archi.pic_code tt && negb (Ptrofs.eq ofs Ptrofs.zero)). + eapply tail_nolabel_trans; [|apply addptrofs_label]. TailNoLabel. + TailNoLabel. -- apply opimm32_label; intros; exact I. -- apply opimm32_label; intros; exact I. -- apply opimm32_label; intros; exact I. -- apply opimm32_label; intros; exact I. -- destruct (Int.eq n Int.zero); try destruct (Int.eq n Int.one); TailNoLabel. -- apply opimm64_label; intros; exact I. -- apply opimm64_label; intros; exact I. -- apply opimm64_label; intros; exact I. -- apply opimm64_label; intros; exact I. -- destruct (Int.eq n Int.zero); try destruct (Int.eq n Int.one); TailNoLabel. -- eapply transl_cond_op_label; eauto. -- destruct optR as [[]|]; simpl in *; TailNoLabel. -- destruct optR as [[]|]; simpl in *; TailNoLabel. -- destruct optR as [[]|]; simpl in *; TailNoLabel. -- destruct optR as [[]|]; simpl in *; TailNoLabel. -- destruct optR as [[]|]; simpl in *; TailNoLabel. -- destruct optR as [[]|]; simpl in *; TailNoLabel. -- destruct optR as [[]|]; simpl in *; TailNoLabel. -- destruct optR as [[]|]; simpl in *; TailNoLabel. -- destruct optR as [[]|]; simpl in *; TailNoLabel. -- destruct optR as [[]|]; simpl in *; TailNoLabel. -- destruct optR as [[]|]; simpl in *; TailNoLabel. -- destruct optR as [[]|]; simpl in *; TailNoLabel. Qed. Remark indexed_memory_access_label: diff --git a/riscV/Asmgenproof1.v b/riscV/Asmgenproof1.v index 2293e001..faa066b0 100644 --- a/riscV/Asmgenproof1.v +++ b/riscV/Asmgenproof1.v @@ -129,22 +129,6 @@ Proof. intros; Simpl. Qed. -Lemma loadimm32_correct: - forall rd n k rs m, - exists rs', - exec_straight ge fn (loadimm32 rd n k) rs m k rs' m - /\ rs'#rd = Vint n - /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. -Proof. - unfold loadimm32; intros. generalize (make_immed32_sound n); intros E. - destruct (make_immed32 n). -- subst imm. econstructor; split. - apply exec_straight_one. simpl; eauto. auto. - split. rewrite Int.add_zero_l; Simpl. - intros; Simpl. -- rewrite E. apply load_hilo32_correct. -Qed. - Lemma opimm32_correct: forall (op: ireg -> ireg0 -> ireg0 -> instruction) (opi: ireg -> ireg0 -> int -> instruction) @@ -195,27 +179,6 @@ Proof. intros; Simpl. Qed. -Lemma loadimm64_correct: - forall rd n k rs m, - exists rs', - exec_straight ge fn (loadimm64 rd n k) rs m k rs' m - /\ rs'#rd = Vlong n - /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r. -Proof. - unfold loadimm64; intros. generalize (make_immed64_sound n); intros E. - destruct (make_immed64 n). -- subst imm. econstructor; split. - apply exec_straight_one. simpl; eauto. auto. - split. rewrite Int64.add_zero_l; Simpl. - intros; Simpl. -- exploit load_hilo64_correct; eauto. intros (rs' & A & B & C). - rewrite E. exists rs'; eauto. -- subst imm. econstructor; split. - apply exec_straight_one. simpl; eauto. auto. - split. Simpl. - intros; Simpl. -Qed. - Lemma opimm64_correct: forall (op: ireg -> ireg0 -> ireg0 -> instruction) (opi: ireg -> ireg0 -> int64 -> instruction) @@ -290,102 +253,6 @@ Proof. rewrite H0 in B. inv B. auto. Qed. -(** Translation of conditional branches *) - -Lemma transl_cbranch_int32s_correct: - forall cmp r1 r2 lbl (rs: regset) m b, - Val.cmp_bool cmp rs##r1 rs##r2 = Some b -> - exec_instr ge fn (transl_cbranch_int32s cmp r1 r2 lbl) rs m = - eval_branch fn lbl rs m (Some b). -Proof. - intros. destruct cmp; simpl; rewrite ? H. -- destruct rs##r1; simpl in H; try discriminate. destruct rs##r2; inv H. - simpl; auto. -- destruct rs##r1; simpl in H; try discriminate. destruct rs##r2; inv H. - simpl; auto. -- auto. -- rewrite <- Val.swap_cmp_bool. simpl. rewrite H; auto. -- rewrite <- Val.swap_cmp_bool. simpl. rewrite H; auto. -- auto. -Qed. - -Lemma transl_cbranch_int32u_correct: - forall cmp r1 r2 lbl (rs: regset) m b, - Val.cmpu_bool (Mem.valid_pointer m) cmp rs##r1 rs##r2 = Some b -> - exec_instr ge fn (transl_cbranch_int32u cmp r1 r2 lbl) rs m = - eval_branch fn lbl rs m (Some b). -Proof. - intros. destruct cmp; simpl; rewrite ? H; auto. -- rewrite <- Val.swap_cmpu_bool. simpl. rewrite H; auto. -- rewrite <- Val.swap_cmpu_bool. simpl. rewrite H; auto. -Qed. - -Lemma transl_cbranch_int64s_correct: - forall cmp r1 r2 lbl (rs: regset) m b, - Val.cmpl_bool cmp rs###r1 rs###r2 = Some b -> - exec_instr ge fn (transl_cbranch_int64s cmp r1 r2 lbl) rs m = - eval_branch fn lbl rs m (Some b). -Proof. - intros. destruct cmp; simpl; rewrite ? H. -- destruct rs###r1; simpl in H; try discriminate. destruct rs###r2; inv H. - simpl; auto. -- destruct rs###r1; simpl in H; try discriminate. destruct rs###r2; inv H. - simpl; auto. -- auto. -- rewrite <- Val.swap_cmpl_bool. simpl. rewrite H; auto. -- rewrite <- Val.swap_cmpl_bool. simpl. rewrite H; auto. -- auto. -Qed. - -Lemma transl_cbranch_int64u_correct: - forall cmp r1 r2 lbl (rs: regset) m b, - Val.cmplu_bool (Mem.valid_pointer m) cmp rs###r1 rs###r2 = Some b -> - exec_instr ge fn (transl_cbranch_int64u cmp r1 r2 lbl) rs m = - eval_branch fn lbl rs m (Some b). -Proof. - intros. destruct cmp; simpl; rewrite ? H; auto. -- rewrite <- Val.swap_cmplu_bool. simpl. rewrite H; auto. -- rewrite <- Val.swap_cmplu_bool. simpl. rewrite H; auto. -Qed. - -Lemma transl_cond_float_correct: - forall (rs: regset) m cmp rd r1 r2 insn normal v, - transl_cond_float cmp rd r1 r2 = (insn, normal) -> - v = (if normal then Val.cmpf cmp rs#r1 rs#r2 else Val.notbool (Val.cmpf cmp rs#r1 rs#r2)) -> - exec_instr ge fn insn rs m = Next (nextinstr (rs#rd <- v)) m. -Proof. - intros. destruct cmp; simpl in H; inv H; auto. -- rewrite Val.negate_cmpf_eq. auto. -- simpl. f_equal. f_equal. f_equal. destruct (rs r2), (rs r1); auto. unfold Val.cmpf, Val.cmpf_bool. - rewrite <- Float.cmp_swap. auto. -- simpl. f_equal. f_equal. f_equal. destruct (rs r2), (rs r1); auto. unfold Val.cmpf, Val.cmpf_bool. - rewrite <- Float.cmp_swap. auto. -Qed. - -Lemma transl_cond_single_correct: - forall (rs: regset) m cmp rd r1 r2 insn normal v, - transl_cond_single cmp rd r1 r2 = (insn, normal) -> - v = (if normal then Val.cmpfs cmp rs#r1 rs#r2 else Val.notbool (Val.cmpfs cmp rs#r1 rs#r2)) -> - exec_instr ge fn insn rs m = Next (nextinstr (rs#rd <- v)) m. -Proof. - intros. destruct cmp; simpl in H; inv H; auto. -- simpl. f_equal. f_equal. f_equal. destruct (rs r2), (rs r1); auto. unfold Val.cmpfs, Val.cmpfs_bool. - rewrite Float32.cmp_ne_eq. destruct (Float32.cmp Ceq f0 f); auto. -- simpl. f_equal. f_equal. f_equal. destruct (rs r2), (rs r1); auto. unfold Val.cmpfs, Val.cmpfs_bool. - rewrite <- Float32.cmp_swap. auto. -- simpl. f_equal. f_equal. f_equal. destruct (rs r2), (rs r1); auto. unfold Val.cmpfs, Val.cmpfs_bool. - rewrite <- Float32.cmp_swap. auto. - Qed. - -(* TODO gourdinl UNUSUED ? Remark branch_on_X31: - forall normal lbl (rs: regset) m b, - rs#X31 = Val.of_bool (eqb normal b) -> - exec_instr ge fn (if normal then Pbnew X31 X0 lbl else Pbeqw X31 X0 lbl) rs m = - eval_branch fn lbl rs m (Some b). -Proof. - intros. destruct normal; simpl; rewrite H; simpl; destruct b; reflexivity. - Qed.*) - Ltac ArgsInv := repeat (match goal with | [ H: Error _ = OK _ |- _ ] => discriminate @@ -417,219 +284,46 @@ Proof. { apply eval_condition_lessdef with (map ms args) m; auto. eapply preg_vals; eauto. } clear EVAL MEXT AG. destruct cond; simpl in TRANSL; ArgsInv. - - exists rs, (transl_cbranch_int32s c0 x x0 lbl). - intuition auto. constructor. apply transl_cbranch_int32s_correct; auto. -- exists rs, (transl_cbranch_int32u c0 x x0 lbl). - intuition auto. constructor. apply transl_cbranch_int32u_correct; auto. -- predSpec Int.eq Int.eq_spec n Int.zero. -+ subst n. exists rs, (transl_cbranch_int32s c0 x X0 lbl). - intuition auto. constructor. apply transl_cbranch_int32s_correct; auto. -+ exploit (loadimm32_correct X31 n); eauto. intros (rs' & A & B & C). - exists rs', (transl_cbranch_int32s c0 x X31 lbl). - split. constructor; eexact A. split; auto. - apply transl_cbranch_int32s_correct; auto. - simpl; rewrite B, C; eauto with asmgen. -- predSpec Int.eq Int.eq_spec n Int.zero. -+ subst n. exists rs, (transl_cbranch_int32u c0 x X0 lbl). - intuition auto. constructor. apply transl_cbranch_int32u_correct; auto. -+ exploit (loadimm32_correct X31 n); eauto. intros (rs' & A & B & C). - exists rs', (transl_cbranch_int32u c0 x X31 lbl). - split. constructor; eexact A. split; auto. - apply transl_cbranch_int32u_correct; auto. - simpl; rewrite B, C; eauto with asmgen. -- exists rs, (transl_cbranch_int64s c0 x x0 lbl). - intuition auto. constructor. apply transl_cbranch_int64s_correct; auto. -- exists rs, (transl_cbranch_int64u c0 x x0 lbl). - intuition auto. constructor. apply transl_cbranch_int64u_correct; auto. -- predSpec Int64.eq Int64.eq_spec n Int64.zero. -+ subst n. exists rs, (transl_cbranch_int64s c0 x X0 lbl). - intuition auto. constructor. apply transl_cbranch_int64s_correct; auto. -+ exploit (loadimm64_correct X31 n); eauto. intros (rs' & A & B & C). - exists rs', (transl_cbranch_int64s c0 x X31 lbl). - split. constructor; eexact A. split; auto. - apply transl_cbranch_int64s_correct; auto. - simpl; rewrite B, C; eauto with asmgen. -- predSpec Int64.eq Int64.eq_spec n Int64.zero. -+ subst n. exists rs, (transl_cbranch_int64u c0 x X0 lbl). - intuition auto. constructor. apply transl_cbranch_int64u_correct; auto. -+ exploit (loadimm64_correct X31 n); eauto. intros (rs' & A & B & C). - exists rs', (transl_cbranch_int64u c0 x X31 lbl). - split. constructor; eexact A. split; auto. - apply transl_cbranch_int64u_correct; auto. - simpl; rewrite B, C; eauto with asmgen. -- destruct (transl_cond_float c0 X31 x x0) as [insn normal] eqn:TC; inv EQ2. - set (v := if normal then Val.cmpf c0 rs#x rs#x0 else Val.notbool (Val.cmpf c0 rs#x rs#x0)). - assert (V: v = Val.of_bool (eqb normal b)). - { unfold v, Val.cmpf. rewrite EVAL'. destruct normal, b; reflexivity. } - econstructor; econstructor. - split. constructor. apply exec_straight_one. eapply transl_cond_float_correct with (v := v); eauto. auto. - split. rewrite V; destruct normal, b; reflexivity. - intros; Simpl. -- destruct (transl_cond_float c0 X31 x x0) as [insn normal] eqn:TC; inv EQ2. - assert (EVAL'': Val.cmpf_bool c0 (rs x) (rs x0) = Some (negb b)). - { destruct (Val.cmpf_bool c0 (rs x) (rs x0)) as [[]|]; inv EVAL'; auto. } - set (v := if normal then Val.cmpf c0 rs#x rs#x0 else Val.notbool (Val.cmpf c0 rs#x rs#x0)). - assert (V: v = Val.of_bool (xorb normal b)). - { unfold v, Val.cmpf. rewrite EVAL''. destruct normal, b; reflexivity. } - econstructor; econstructor. - split. constructor. apply exec_straight_one. eapply transl_cond_float_correct with (v := v); eauto. auto. - split. rewrite V; destruct normal, b; reflexivity. - intros; Simpl. -- destruct (transl_cond_single c0 X31 x x0) as [insn normal] eqn:TC; inv EQ2. - set (v := if normal then Val.cmpfs c0 rs#x rs#x0 else Val.notbool (Val.cmpfs c0 rs#x rs#x0)). - assert (V: v = Val.of_bool (eqb normal b)). - { unfold v, Val.cmpfs. rewrite EVAL'. destruct normal, b; reflexivity. } - econstructor; econstructor. - split. constructor. apply exec_straight_one. eapply transl_cond_single_correct with (v := v); eauto. auto. - split. rewrite V; destruct normal, b; reflexivity. - intros; Simpl. -- destruct (transl_cond_single c0 X31 x x0) as [insn normal] eqn:TC; inv EQ2. - assert (EVAL'': Val.cmpfs_bool c0 (rs x) (rs x0) = Some (negb b)). - { destruct (Val.cmpfs_bool c0 (rs x) (rs x0)) as [[]|]; inv EVAL'; auto. } - set (v := if normal then Val.cmpfs c0 rs#x rs#x0 else Val.notbool (Val.cmpfs c0 rs#x rs#x0)). - assert (V: v = Val.of_bool (xorb normal b)). - { unfold v, Val.cmpfs. rewrite EVAL''. destruct normal, b; reflexivity. } - econstructor; econstructor. - split. constructor. apply exec_straight_one. eapply transl_cond_single_correct with (v := v); eauto. auto. - split. rewrite V; destruct normal, b; reflexivity. - intros; Simpl. - -- destruct optR as [[]|]; - unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; - unfold zero32, Op.zero32 in *; - destruct (rs x) eqn:EQRS; simpl in *; try congruence; - inv EQ2; eexists; eexists; eauto; split; constructor; auto; - simpl in *. - + rewrite EQRS; - assert (HB: (Int.eq Int.zero i) = b) by congruence. + all: + destruct optR as [[]|]; + unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; + unfold zero32, Op.zero32 in *; + unfold zero64, Op.zero64 in *; inv EQ2; + try (destruct (rs x); simpl in EVAL'; discriminate; fail); + try (eexists; eexists; eauto; split; constructor; + simpl in *; try rewrite EVAL'; auto; fail). + all: + destruct (rs x) eqn:EQRS; simpl in *; try congruence; + eexists; eexists; eauto; split; constructor; auto; + simpl in *; rewrite EQRS. + - assert (HB: (Int.eq Int.zero i) = b) by congruence; rewrite HB; destruct b; simpl; auto. - + rewrite EQRS; - assert (HB: (Int.eq i Int.zero) = b) by congruence. + - assert (HB: (Int.eq i Int.zero) = b) by congruence. rewrite <- HB; destruct b; simpl; auto. - + rewrite EQRS; - destruct (rs x0); try congruence. + - destruct (rs x0); try congruence. assert (HB: (Int.eq i i0) = b) by congruence. rewrite <- HB; destruct b; simpl; auto. -- destruct optR as [[]|]; - unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; - unfold zero32, Op.zero32 in *; - destruct (rs x) eqn:EQRS; simpl in *; try congruence; - inv EQ2; eexists; eexists; eauto; split; constructor; auto; - simpl in *. - + rewrite EQRS; - assert (HB: negb (Int.eq Int.zero i) = b) by congruence. + - assert (HB: negb (Int.eq Int.zero i) = b) by congruence. rewrite HB; destruct b; simpl; auto. - + rewrite EQRS; - assert (HB: negb (Int.eq i Int.zero) = b) by congruence. + - assert (HB: negb (Int.eq i Int.zero) = b) by congruence. rewrite <- HB; destruct b; simpl; auto. - + rewrite EQRS; - destruct (rs x0); try congruence. + - destruct (rs x0); try congruence. assert (HB: negb (Int.eq i i0) = b) by congruence. rewrite <- HB; destruct b; simpl; auto. -- destruct optR as [[]|]; - unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; - unfold zero32, Op.zero32 in *; inv EQ2; - try (destruct (rs x); simpl in EVAL'; discriminate; fail); - eexists; eexists; eauto; split; constructor; - simpl in *; try rewrite EVAL'; auto. -- destruct optR as [[]|]; - unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; - unfold zero32, Op.zero32 in *; inv EQ2; - try (destruct (rs x); simpl in EVAL'; discriminate; fail); - eexists; eexists; eauto; split; constructor; - simpl in *; try rewrite EVAL'; auto. -- destruct optR as [[]|]; - unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; - unfold zero32, Op.zero32 in *; inv EQ2; - try (destruct (rs x); simpl in EVAL'; discriminate; fail); - eexists; eexists; eauto; split; constructor; - simpl in *; try rewrite EVAL'; auto. -- destruct optR as [[]|]; - unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; - unfold zero32, Op.zero32 in *; inv EQ2; - try (destruct (rs x); simpl in EVAL'; discriminate; fail); - eexists; eexists; eauto; split; constructor; - simpl in *; try rewrite EVAL'; auto. -- destruct optR as [[]|]; - unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; - unfold zero32, Op.zero32 in *; inv EQ2; - try (destruct (rs x); simpl in EVAL'; discriminate; fail); - eexists; eexists; eauto; split; constructor; - simpl in *; try rewrite EVAL'; auto. -- destruct optR as [[]|]; - unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; - unfold zero32, Op.zero32 in *; inv EQ2; - try (destruct (rs x); simpl in EVAL'; discriminate; fail); - eexists; eexists; eauto; split; constructor; - simpl in *; try rewrite EVAL'; auto. -- destruct optR as [[]|]; - unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; - unfold zero32, Op.zero32 in *; inv EQ2; - destruct (rs x) eqn:EQRS; simpl in *; try congruence; - eexists; eexists; eauto; split; constructor; - simpl in *; auto. - + rewrite EQRS; - assert (HB: (Int64.eq Int64.zero i) = b) by congruence. + - assert (HB: (Int64.eq Int64.zero i) = b) by congruence. rewrite HB; destruct b; simpl; auto. - + rewrite EQRS; - assert (HB: (Int64.eq i Int64.zero) = b) by congruence. + - assert (HB: (Int64.eq i Int64.zero) = b) by congruence. rewrite <- HB; destruct b; simpl; auto. - + rewrite EQRS; - destruct (rs x0); try congruence. + - destruct (rs x0); try congruence. assert (HB: (Int64.eq i i0) = b) by congruence. rewrite <- HB; destruct b; simpl; auto. -- destruct optR as [[]|]; - unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; - unfold zero32, Op.zero32 in *; inv EQ2; - destruct (rs x) eqn:EQRS; simpl in *; try congruence; - eexists; eexists; eauto; split; constructor; - simpl in *; auto. - + rewrite EQRS; - assert (HB: negb (Int64.eq Int64.zero i) = b) by congruence. + - assert (HB: negb (Int64.eq Int64.zero i) = b) by congruence. rewrite HB; destruct b; simpl; auto. - + rewrite EQRS; - assert (HB: negb (Int64.eq i Int64.zero) = b) by congruence. + - assert (HB: negb (Int64.eq i Int64.zero) = b) by congruence. rewrite <- HB; destruct b; simpl; auto. - + rewrite EQRS; - destruct (rs x0); try congruence. + - destruct (rs x0); try congruence. assert (HB: negb (Int64.eq i i0) = b) by congruence. rewrite <- HB; destruct b; simpl; auto. -- destruct optR as [[]|]; - unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; - unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2; - try (destruct (rs x); simpl in EVAL'; discriminate; fail); - eexists; eexists; eauto; split; constructor; - simpl in *; try rewrite EVAL'; auto. -- destruct optR as [[]|]; - unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; - unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2; - try (destruct (rs x); simpl in EVAL'; discriminate; fail); - eexists; eexists; eauto; split; constructor; - simpl in *; try rewrite EVAL'; auto. -- destruct optR as [[]|]; - unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; - unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2; - try (destruct (rs x); simpl in EVAL'; discriminate; fail); - eexists; eexists; eauto; split; constructor; - simpl in *; try rewrite EVAL'; auto. -- destruct optR as [[]|]; - unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; - unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2; - try (destruct (rs x); simpl in EVAL'; discriminate; fail); - eexists; eexists; eauto; split; constructor; - simpl in *; try rewrite EVAL'; auto. -- destruct optR as [[]|]; - unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; - unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2; - try (destruct (rs x); simpl in EVAL'; discriminate; fail); - eexists; eexists; eauto; split; constructor; - simpl in *; try rewrite EVAL'; auto. -- destruct optR as [[]|]; - unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; - unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2; - try (destruct (rs x); simpl in EVAL'; discriminate; fail); - eexists; eexists; eauto; split; constructor; - simpl in *; try rewrite EVAL'; auto. Qed. Lemma transl_cbranch_correct_true: @@ -663,417 +357,6 @@ Proof. intros; Simpl. Qed. -(** Translation of condition operators *) - -Lemma transl_cond_int32s_correct: - forall cmp rd r1 r2 k rs m, - exists rs', - exec_straight ge fn (transl_cond_int32s cmp rd r1 r2 k) rs m k rs' m - /\ Val.lessdef (Val.cmp cmp rs##r1 rs##r2) rs'#rd - /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. -Proof. - intros. destruct cmp; simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. - split; intros; Simpl. destruct (rs##r1); auto. destruct (rs##r2); auto. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. - split; intros; Simpl. destruct (rs##r1); auto. destruct (rs##r2); auto. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. - split; intros; Simpl. -- econstructor; split. - eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. - split; intros; Simpl. unfold Val.cmp. rewrite <- Val.swap_cmp_bool. - simpl. rewrite (Val.negate_cmp_bool Clt). - destruct (Val.cmp_bool Clt rs##r2 rs##r1) as [[]|]; auto. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. - split; intros; Simpl. unfold Val.cmp. rewrite <- Val.swap_cmp_bool. auto. -- econstructor; split. - eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. - split; intros; Simpl. unfold Val.cmp. rewrite (Val.negate_cmp_bool Clt). - destruct (Val.cmp_bool Clt rs##r1 rs##r2) as [[]|]; auto. -Qed. - -Lemma transl_cond_int32u_correct: - forall cmp rd r1 r2 k rs m, - exists rs', - exec_straight ge fn (transl_cond_int32u cmp rd r1 r2 k) rs m k rs' m - /\ rs'#rd = Val.cmpu (Mem.valid_pointer m) cmp rs##r1 rs##r2 - /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. -Proof. - intros. destruct cmp; simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. - split; intros; Simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. - split; intros; Simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. - split; intros; Simpl. -- econstructor; split. - eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. - split; intros; Simpl. unfold Val.cmpu. rewrite <- Val.swap_cmpu_bool. - simpl. rewrite (Val.negate_cmpu_bool (Mem.valid_pointer m) Cle). - destruct (Val.cmpu_bool (Mem.valid_pointer m) Cle rs##r1 rs##r2) as [[]|]; auto. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. - split; intros; Simpl. unfold Val.cmpu. rewrite <- Val.swap_cmpu_bool. auto. -- econstructor; split. - eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. - split; intros; Simpl. unfold Val.cmpu. rewrite (Val.negate_cmpu_bool (Mem.valid_pointer m) Clt). - destruct (Val.cmpu_bool (Mem.valid_pointer m) Clt rs##r1 rs##r2) as [[]|]; auto. -Qed. - -Lemma transl_cond_int64s_correct: - forall cmp rd r1 r2 k rs m, - exists rs', - exec_straight ge fn (transl_cond_int64s cmp rd r1 r2 k) rs m k rs' m - /\ Val.lessdef (Val.maketotal (Val.cmpl cmp rs###r1 rs###r2)) rs'#rd - /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. -Proof. - intros. destruct cmp; simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. - split; intros; Simpl. destruct (rs###r1); auto. destruct (rs###r2); auto. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. - split; intros; Simpl. destruct (rs###r1); auto. destruct (rs###r2); auto. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. - split; intros; Simpl. -- econstructor; split. - eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. - split; intros; Simpl. unfold Val.cmpl. rewrite <- Val.swap_cmpl_bool. - simpl. rewrite (Val.negate_cmpl_bool Clt). - destruct (Val.cmpl_bool Clt rs###r2 rs###r1) as [[]|]; auto. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. - split; intros; Simpl. unfold Val.cmpl. rewrite <- Val.swap_cmpl_bool. auto. -- econstructor; split. - eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. - split; intros; Simpl. unfold Val.cmpl. rewrite (Val.negate_cmpl_bool Clt). - destruct (Val.cmpl_bool Clt rs###r1 rs###r2) as [[]|]; auto. -Qed. - -Lemma transl_cond_int64u_correct: - forall cmp rd r1 r2 k rs m, - exists rs', - exec_straight ge fn (transl_cond_int64u cmp rd r1 r2 k) rs m k rs' m - /\ rs'#rd = Val.maketotal (Val.cmplu (Mem.valid_pointer m) cmp rs###r1 rs###r2) - /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. -Proof. - intros. destruct cmp; simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. - split; intros; Simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. - split; intros; Simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. - split; intros; Simpl. -- econstructor; split. - eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. - split; intros; Simpl. unfold Val.cmplu. rewrite <- Val.swap_cmplu_bool. - simpl. rewrite (Val.negate_cmplu_bool (Mem.valid_pointer m) Cle). - destruct (Val.cmplu_bool (Mem.valid_pointer m) Cle rs###r1 rs###r2) as [[]|]; auto. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. - split; intros; Simpl. unfold Val.cmplu. rewrite <- Val.swap_cmplu_bool. auto. -- econstructor; split. - eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. - split; intros; Simpl. unfold Val.cmplu. rewrite (Val.negate_cmplu_bool (Mem.valid_pointer m) Clt). - destruct (Val.cmplu_bool (Mem.valid_pointer m) Clt rs###r1 rs###r2) as [[]|]; auto. -Qed. - -Lemma transl_condimm_int32s_correct: - forall cmp rd r1 n k rs m, - r1 <> X31 -> - exists rs', - exec_straight ge fn (transl_condimm_int32s cmp rd r1 n k) rs m k rs' m - /\ Val.lessdef (Val.cmp cmp rs#r1 (Vint n)) rs'#rd - /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r. -Proof. - intros. unfold transl_condimm_int32s. - predSpec Int.eq Int.eq_spec n Int.zero. -- subst n. exploit transl_cond_int32s_correct. intros (rs' & A & B & C). - exists rs'; eauto. -- assert (DFL: - exists rs', - exec_straight ge fn (loadimm32 X31 n (transl_cond_int32s cmp rd r1 X31 k)) rs m k rs' m - /\ Val.lessdef (Val.cmp cmp rs#r1 (Vint n)) rs'#rd - /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r). - { exploit loadimm32_correct; eauto. intros (rs1 & A1 & B1 & C1). - exploit transl_cond_int32s_correct; eauto. intros (rs2 & A2 & B2 & C2). - exists rs2; split. - eapply exec_straight_trans. eexact A1. eexact A2. - split. simpl in B2. rewrite B1, C1 in B2 by auto with asmgen. auto. - intros; transitivity (rs1 r); auto. } - destruct cmp. -+ unfold xorimm32. - exploit (opimm32_correct Pxorw Pxoriw Val.xor); eauto. intros (rs1 & A1 & B1 & C1). - exploit transl_cond_int32s_correct; eauto. intros (rs2 & A2 & B2 & C2). - exists rs2; split. - eapply exec_straight_trans. eexact A1. eexact A2. - split. simpl in B2; rewrite B1 in B2; simpl in B2. destruct (rs#r1); auto. - unfold Val.cmp in B2; simpl in B2; rewrite Int.xor_is_zero in B2. exact B2. - intros; transitivity (rs1 r); auto. -+ unfold xorimm32. - exploit (opimm32_correct Pxorw Pxoriw Val.xor); eauto. intros (rs1 & A1 & B1 & C1). - exploit transl_cond_int32s_correct; eauto. intros (rs2 & A2 & B2 & C2). - exists rs2; split. - eapply exec_straight_trans. eexact A1. eexact A2. - split. simpl in B2; rewrite B1 in B2; simpl in B2. destruct (rs#r1); auto. - unfold Val.cmp in B2; simpl in B2; rewrite Int.xor_is_zero in B2. exact B2. - intros; transitivity (rs1 r); auto. -+ exploit (opimm32_correct Psltw Psltiw (Val.cmp Clt)); eauto. intros (rs1 & A1 & B1 & C1). - exists rs1; split. eexact A1. split; auto. rewrite B1; auto. -+ predSpec Int.eq Int.eq_spec n (Int.repr Int.max_signed). -* subst n. exploit loadimm32_correct; eauto. intros (rs1 & A1 & B1 & C1). - exists rs1; split. eexact A1. split; auto. - unfold Val.cmp; destruct (rs#r1); simpl; auto. rewrite B1. - unfold Int.lt. rewrite zlt_false. auto. - change (Int.signed (Int.repr Int.max_signed)) with Int.max_signed. - generalize (Int.signed_range i); omega. -* exploit (opimm32_correct Psltw Psltiw (Val.cmp Clt)); eauto. intros (rs1 & A1 & B1 & C1). - exists rs1; split. eexact A1. split; auto. - rewrite B1. unfold Val.cmp; simpl; destruct (rs#r1); simpl; auto. - unfold Int.lt. replace (Int.signed (Int.add n Int.one)) with (Int.signed n + 1). - destruct (zlt (Int.signed n) (Int.signed i)). - rewrite zlt_false by omega. auto. - rewrite zlt_true by omega. auto. - rewrite Int.add_signed. symmetry; apply Int.signed_repr. - assert (Int.signed n <> Int.max_signed). - { red; intros E. elim H1. rewrite <- (Int.repr_signed n). rewrite E. auto. } - generalize (Int.signed_range n); omega. -+ apply DFL. -+ apply DFL. -Qed. - -Lemma transl_condimm_int32u_correct: - forall cmp rd r1 n k rs m, - r1 <> X31 -> - exists rs', - exec_straight ge fn (transl_condimm_int32u cmp rd r1 n k) rs m k rs' m - /\ Val.lessdef (Val.cmpu (Mem.valid_pointer m) cmp rs#r1 (Vint n)) rs'#rd - /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r. -Proof. - intros. unfold transl_condimm_int32u. - predSpec Int.eq Int.eq_spec n Int.zero. -- subst n. exploit transl_cond_int32u_correct. intros (rs' & A & B & C). - exists rs'; split. eexact A. split; auto. rewrite B; auto. -- assert (DFL: - exists rs', - exec_straight ge fn (loadimm32 X31 n (transl_cond_int32u cmp rd r1 X31 k)) rs m k rs' m - /\ Val.lessdef (Val.cmpu (Mem.valid_pointer m) cmp rs#r1 (Vint n)) rs'#rd - /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r). - { exploit loadimm32_correct; eauto. intros (rs1 & A1 & B1 & C1). - exploit transl_cond_int32u_correct; eauto. intros (rs2 & A2 & B2 & C2). - exists rs2; split. - eapply exec_straight_trans. eexact A1. eexact A2. - split. simpl in B2. rewrite B1, C1 in B2 by auto with asmgen. rewrite B2; auto. - intros; transitivity (rs1 r); auto. } - destruct cmp. -+ apply DFL. -+ apply DFL. -+ exploit (opimm32_correct Psltuw Psltiuw (Val.cmpu (Mem.valid_pointer m) Clt) m); eauto. - intros (rs1 & A1 & B1 & C1). - exists rs1; split. eexact A1. split; auto. rewrite B1; auto. -+ apply DFL. -+ apply DFL. -+ apply DFL. -Qed. - -Lemma transl_condimm_int64s_correct: - forall cmp rd r1 n k rs m, - r1 <> X31 -> - exists rs', - exec_straight ge fn (transl_condimm_int64s cmp rd r1 n k) rs m k rs' m - /\ Val.lessdef (Val.maketotal (Val.cmpl cmp rs#r1 (Vlong n))) rs'#rd - /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r. -Proof. - intros. unfold transl_condimm_int64s. - predSpec Int64.eq Int64.eq_spec n Int64.zero. -- subst n. exploit transl_cond_int64s_correct. intros (rs' & A & B & C). - exists rs'; eauto. -- assert (DFL: - exists rs', - exec_straight ge fn (loadimm64 X31 n (transl_cond_int64s cmp rd r1 X31 k)) rs m k rs' m - /\ Val.lessdef (Val.maketotal (Val.cmpl cmp rs#r1 (Vlong n))) rs'#rd - /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r). - { exploit loadimm64_correct; eauto. intros (rs1 & A1 & B1 & C1). - exploit transl_cond_int64s_correct; eauto. intros (rs2 & A2 & B2 & C2). - exists rs2; split. - eapply exec_straight_trans. eexact A1. eexact A2. - split. simpl in B2. rewrite B1, C1 in B2 by auto with asmgen. auto. - intros; transitivity (rs1 r); auto. } - destruct cmp. -+ unfold xorimm64. - exploit (opimm64_correct Pxorl Pxoril Val.xorl); eauto. intros (rs1 & A1 & B1 & C1). - exploit transl_cond_int64s_correct; eauto. intros (rs2 & A2 & B2 & C2). - exists rs2; split. - eapply exec_straight_trans. eexact A1. eexact A2. - split. simpl in B2; rewrite B1 in B2; simpl in B2. destruct (rs#r1); auto. - unfold Val.cmpl in B2; simpl in B2; rewrite Int64.xor_is_zero in B2. exact B2. - intros; transitivity (rs1 r); auto. -+ unfold xorimm64. - exploit (opimm64_correct Pxorl Pxoril Val.xorl); eauto. intros (rs1 & A1 & B1 & C1). - exploit transl_cond_int64s_correct; eauto. intros (rs2 & A2 & B2 & C2). - exists rs2; split. - eapply exec_straight_trans. eexact A1. eexact A2. - split. simpl in B2; rewrite B1 in B2; simpl in B2. destruct (rs#r1); auto. - unfold Val.cmpl in B2; simpl in B2; rewrite Int64.xor_is_zero in B2. exact B2. - intros; transitivity (rs1 r); auto. -+ exploit (opimm64_correct Psltl Psltil (fun v1 v2 => Val.maketotal (Val.cmpl Clt v1 v2))); eauto. intros (rs1 & A1 & B1 & C1). - exists rs1; split. eexact A1. split; auto. rewrite B1; auto. -+ predSpec Int64.eq Int64.eq_spec n (Int64.repr Int64.max_signed). -* subst n. exploit loadimm32_correct; eauto. intros (rs1 & A1 & B1 & C1). - exists rs1; split. eexact A1. split; auto. - unfold Val.cmpl; destruct (rs#r1); simpl; auto. rewrite B1. - unfold Int64.lt. rewrite zlt_false. auto. - change (Int64.signed (Int64.repr Int64.max_signed)) with Int64.max_signed. - generalize (Int64.signed_range i); omega. -* exploit (opimm64_correct Psltl Psltil (fun v1 v2 => Val.maketotal (Val.cmpl Clt v1 v2))); eauto. intros (rs1 & A1 & B1 & C1). - exists rs1; split. eexact A1. split; auto. - rewrite B1. unfold Val.cmpl; simpl; destruct (rs#r1); simpl; auto. - unfold Int64.lt. replace (Int64.signed (Int64.add n Int64.one)) with (Int64.signed n + 1). - destruct (zlt (Int64.signed n) (Int64.signed i)). - rewrite zlt_false by omega. auto. - rewrite zlt_true by omega. auto. - rewrite Int64.add_signed. symmetry; apply Int64.signed_repr. - assert (Int64.signed n <> Int64.max_signed). - { red; intros E. elim H1. rewrite <- (Int64.repr_signed n). rewrite E. auto. } - generalize (Int64.signed_range n); omega. -+ apply DFL. -+ apply DFL. -Qed. - -Lemma transl_condimm_int64u_correct: - forall cmp rd r1 n k rs m, - r1 <> X31 -> - exists rs', - exec_straight ge fn (transl_condimm_int64u cmp rd r1 n k) rs m k rs' m - /\ Val.lessdef (Val.maketotal (Val.cmplu (Mem.valid_pointer m) cmp rs#r1 (Vlong n))) rs'#rd - /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r. -Proof. - intros. unfold transl_condimm_int64u. - predSpec Int64.eq Int64.eq_spec n Int64.zero. -- subst n. exploit transl_cond_int64u_correct. intros (rs' & A & B & C). - exists rs'; split. eexact A. split; auto. rewrite B; auto. -- assert (DFL: - exists rs', - exec_straight ge fn (loadimm64 X31 n (transl_cond_int64u cmp rd r1 X31 k)) rs m k rs' m - /\ Val.lessdef (Val.maketotal (Val.cmplu (Mem.valid_pointer m) cmp rs#r1 (Vlong n))) rs'#rd - /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r). - { exploit loadimm64_correct; eauto. intros (rs1 & A1 & B1 & C1). - exploit transl_cond_int64u_correct; eauto. intros (rs2 & A2 & B2 & C2). - exists rs2; split. - eapply exec_straight_trans. eexact A1. eexact A2. - split. simpl in B2. rewrite B1, C1 in B2 by auto with asmgen. rewrite B2; auto. - intros; transitivity (rs1 r); auto. } - destruct cmp. -+ apply DFL. -+ apply DFL. -+ exploit (opimm64_correct Psltul Psltiul (fun v1 v2 => Val.maketotal (Val.cmplu (Mem.valid_pointer m) Clt v1 v2)) m); eauto. - intros (rs1 & A1 & B1 & C1). - exists rs1; split. eexact A1. split; auto. rewrite B1; auto. -+ apply DFL. -+ apply DFL. -+ apply DFL. - Qed. - -Lemma transl_cond_op_correct: - forall cond rd args k c rs m, - transl_cond_op cond rd args k = OK c -> - exists rs', - exec_straight ge fn c rs m k rs' m - /\ Val.lessdef (Val.of_optbool (eval_condition cond (map rs (map preg_of args)) m)) rs'#rd - /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r. -Proof. - assert (MKTOT: forall ob, Val.of_optbool ob = Val.maketotal (option_map Val.of_bool ob)). - { destruct ob as [[]|]; reflexivity. } - intros until m; intros TR. - destruct cond; simpl in TR; ArgsInv. -+ (* cmp *) - exploit transl_cond_int32s_correct; eauto. intros (rs' & A & B & C). exists rs'; eauto. -+ (* cmpu *) - exploit transl_cond_int32u_correct; eauto. intros (rs' & A & B & C). - exists rs'; repeat split; eauto. rewrite B; auto. -+ (* cmpimm *) - apply transl_condimm_int32s_correct; eauto with asmgen. -+ (* cmpuimm *) - apply transl_condimm_int32u_correct; eauto with asmgen. -+ (* cmpl *) - exploit transl_cond_int64s_correct; eauto. intros (rs' & A & B & C). - exists rs'; repeat split; eauto. rewrite MKTOT; eauto. -+ (* cmplu *) - exploit transl_cond_int64u_correct; eauto. intros (rs' & A & B & C). - exists rs'; repeat split; eauto. rewrite B, MKTOT; eauto. -+ (* cmplimm *) - exploit transl_condimm_int64s_correct; eauto. instantiate (1 := x); eauto with asmgen. - intros (rs' & A & B & C). - exists rs'; repeat split; eauto. rewrite MKTOT; eauto. -+ (* cmpluimm *) - exploit transl_condimm_int64u_correct; eauto. instantiate (1 := x); eauto with asmgen. - intros (rs' & A & B & C). - exists rs'; repeat split; eauto. rewrite MKTOT; eauto. -+ (* cmpf *) - destruct (transl_cond_float c0 rd x x0) as [insn normal] eqn:TR. - fold (Val.cmpf c0 (rs x) (rs x0)). - set (v := Val.cmpf c0 (rs x) (rs x0)). - destruct normal; inv EQ2. -* econstructor; split. - apply exec_straight_one. eapply transl_cond_float_correct with (v := v); eauto. auto. - split; intros; Simpl. -* econstructor; split. - eapply exec_straight_two. - eapply transl_cond_float_correct with (v := Val.notbool v); eauto. - simpl; reflexivity. - auto. auto. - split; intros; Simpl. unfold v, Val.cmpf. destruct (Val.cmpf_bool c0 (rs x) (rs x0)) as [[]|]; auto. -+ (* notcmpf *) - destruct (transl_cond_float c0 rd x x0) as [insn normal] eqn:TR. - rewrite Val.notbool_negb_3. fold (Val.cmpf c0 (rs x) (rs x0)). - set (v := Val.cmpf c0 (rs x) (rs x0)). - destruct normal; inv EQ2. -* econstructor; split. - eapply exec_straight_two. - eapply transl_cond_float_correct with (v := v); eauto. - simpl; reflexivity. - auto. auto. - split; intros; Simpl. unfold v, Val.cmpf. destruct (Val.cmpf_bool c0 (rs x) (rs x0)) as [[]|]; auto. -* econstructor; split. - apply exec_straight_one. eapply transl_cond_float_correct with (v := Val.notbool v); eauto. auto. - split; intros; Simpl. -+ (* cmpfs *) - destruct (transl_cond_single c0 rd x x0) as [insn normal] eqn:TR. - fold (Val.cmpfs c0 (rs x) (rs x0)). - set (v := Val.cmpfs c0 (rs x) (rs x0)). - destruct normal; inv EQ2. -* econstructor; split. - apply exec_straight_one. eapply transl_cond_single_correct with (v := v); eauto. auto. - split; intros; Simpl. -* econstructor; split. - eapply exec_straight_two. - eapply transl_cond_single_correct with (v := Val.notbool v); eauto. - simpl; reflexivity. - auto. auto. - split; intros; Simpl. unfold v, Val.cmpfs. destruct (Val.cmpfs_bool c0 (rs x) (rs x0)) as [[]|]; auto. -+ (* notcmpfs *) - destruct (transl_cond_single c0 rd x x0) as [insn normal] eqn:TR. - rewrite Val.notbool_negb_3. fold (Val.cmpfs c0 (rs x) (rs x0)). - set (v := Val.cmpfs c0 (rs x) (rs x0)). - destruct normal; inv EQ2. -* econstructor; split. - eapply exec_straight_two. - eapply transl_cond_single_correct with (v := v); eauto. - simpl; reflexivity. - auto. auto. - split; intros; Simpl. unfold v, Val.cmpfs. destruct (Val.cmpfs_bool c0 (rs x) (rs x0)) as [[]|]; auto. -* econstructor; split. - apply exec_straight_one. eapply transl_cond_single_correct with (v := Val.notbool v); eauto. auto. - split; intros; Simpl. - Qed. - -(** Some arithmetic properties. *) - -Remark cast32unsigned_from_cast32signed: - forall i, Int64.repr (Int.unsigned i) = Int64.zero_ext 32 (Int64.repr (Int.signed i)). -Proof. - intros. apply Int64.same_bits_eq; intros. - rewrite Int64.bits_zero_ext, !Int64.testbit_repr by tauto. - rewrite Int.bits_signed by tauto. fold (Int.testbit i i0). - change Int.zwordsize with 32. - destruct (zlt i0 32). auto. apply Int.bits_above. auto. -Qed. - (* Translation of arithmetic operations *) Ltac SimplEval H := @@ -1103,28 +386,6 @@ Opaque Int.eq. unfold transl_op in TR; destruct op; ArgsInv; simpl in EV; SimplEval EV; try TranslOpSimpl. (* move *) { destruct (preg_of res), (preg_of m0); inv TR; TranslOpSimpl. } - (* intconst *) - { exploit loadimm32_correct; eauto. intros (rs' & A & B & C). - exists rs'; split; eauto. rewrite B; auto with asmgen. } - (* longconst *) - { exploit loadimm64_correct; eauto. intros (rs' & A & B & C). - exists rs'; split; eauto. rewrite B; auto with asmgen. } - (* floatconst *) - { destruct (Float.eq_dec n Float.zero). - + subst n. econstructor; split. - apply exec_straight_one. simpl; eauto. auto. - split; intros; Simpl. - + econstructor; split. - apply exec_straight_one. simpl; eauto. auto. - split; intros; Simpl. } - (* singleconst *) - { destruct (Float32.eq_dec n Float32.zero). - + subst n. econstructor; split. - apply exec_straight_one. simpl; eauto. auto. - split; intros; Simpl. - + econstructor; split. - apply exec_straight_one. simpl; eauto. auto. - split; intros; Simpl. } (* addrsymbol *) { destruct (Archi.pic_code tt && negb (Ptrofs.eq ofs Ptrofs.zero)). + set (rs1 := nextinstr (rs#x <- (Genv.symbol_address ge id Ptrofs.zero))). @@ -1141,138 +402,6 @@ Opaque Int.eq. (* stackoffset *) { exploit addptrofs_correct. instantiate (1 := X2); auto with asmgen. intros (rs' & A & B & C). exists rs'; split; eauto. auto with asmgen. } - (* cast8signed *) - { econstructor; split. - eapply exec_straight_two. simpl;eauto. simpl;eauto. auto. auto. - split; intros; Simpl. - assert (A: Int.ltu (Int.repr 24) Int.iwordsize = true) by auto. - destruct (rs x0); auto; simpl. rewrite A; simpl. rewrite A. - apply Val.lessdef_same. f_equal. apply Int.sign_ext_shr_shl. split; reflexivity. } - (* cast16signed *) - { econstructor; split. - eapply exec_straight_two. simpl;eauto. simpl;eauto. auto. auto. - split; intros; Simpl. - assert (A: Int.ltu (Int.repr 16) Int.iwordsize = true) by auto. - destruct (rs x0); auto; simpl. rewrite A; simpl. rewrite A. - apply Val.lessdef_same. f_equal. apply Int.sign_ext_shr_shl. split; reflexivity. } - (* addimm *) - { exploit (opimm32_correct Paddw Paddiw Val.add); auto. instantiate (1 := x0); eauto with asmgen. - intros (rs' & A & B & C). - exists rs'; split; eauto. rewrite B; auto with asmgen. } - (* andimm *) - { exploit (opimm32_correct Pandw Pandiw Val.and); auto. instantiate (1 := x0); eauto with asmgen. - intros (rs' & A & B & C). - exists rs'; split; eauto. rewrite B; auto with asmgen. } - (* orimm *) - exploit (opimm32_correct Porw Poriw Val.or); auto. instantiate (1 := x0); eauto with asmgen. - { intros (rs' & A & B & C). - exists rs'; split; eauto. rewrite B; auto with asmgen. } - (* xorimm *) - { exploit (opimm32_correct Pxorw Pxoriw Val.xor); auto. instantiate (1 := x0); eauto with asmgen. - intros (rs' & A & B & C). - exists rs'; split; eauto. rewrite B; auto with asmgen. } - (* shrximm *) - { destruct (Val.shrx (rs x0) (Vint n)) eqn:TOTAL; cbn. - { - exploit Val.shrx_shr_3; eauto. intros E; subst v. - destruct (Int.eq n Int.zero). - + econstructor; split. apply exec_straight_one. simpl; eauto. auto. - split; intros; Simpl. - + destruct (Int.eq n Int.one). - * econstructor; split. - eapply exec_straight_step. simpl; reflexivity. auto. - eapply exec_straight_step. simpl; reflexivity. auto. - apply exec_straight_one. simpl; reflexivity. auto. - split; intros; Simpl. - * change (Int.repr 32) with Int.iwordsize. set (n' := Int.sub Int.iwordsize n). - econstructor; split. - eapply exec_straight_step. simpl; reflexivity. auto. - eapply exec_straight_step. simpl; reflexivity. auto. - eapply exec_straight_step. simpl; reflexivity. auto. - apply exec_straight_one. simpl; reflexivity. auto. - split; intros; Simpl. - } - destruct (Int.eq n Int.zero). - + econstructor; split. apply exec_straight_one. simpl; eauto. auto. - split; intros; Simpl. - + destruct (Int.eq n Int.one). - * econstructor; split. - eapply exec_straight_step. simpl; reflexivity. auto. - eapply exec_straight_step. simpl; reflexivity. auto. - apply exec_straight_one. simpl; reflexivity. auto. - split; intros; Simpl. - * change (Int.repr 32) with Int.iwordsize. set (n' := Int.sub Int.iwordsize n). - econstructor; split. - eapply exec_straight_step. simpl; reflexivity. auto. - eapply exec_straight_step. simpl; reflexivity. auto. - eapply exec_straight_step. simpl; reflexivity. auto. - apply exec_straight_one. simpl; reflexivity. auto. - split; intros; Simpl. } - (* longofintu *) - { econstructor; split. - eapply exec_straight_three. simpl; eauto. simpl; eauto. simpl; eauto. auto. auto. auto. - split; intros; Simpl. destruct (rs x0); auto. simpl. - assert (A: Int.ltu (Int.repr 32) Int64.iwordsize' = true) by auto. - rewrite A; simpl. rewrite A. apply Val.lessdef_same. f_equal. - rewrite cast32unsigned_from_cast32signed. apply Int64.zero_ext_shru_shl. compute; auto. } - (* addlimm *) - { exploit (opimm64_correct Paddl Paddil Val.addl); auto. instantiate (1 := x0); eauto with asmgen. - intros (rs' & A & B & C). - exists rs'; split; eauto. rewrite B; auto with asmgen. } - (* andimm *) - { exploit (opimm64_correct Pandl Pandil Val.andl); auto. instantiate (1 := x0); eauto with asmgen. - intros (rs' & A & B & C). - exists rs'; split; eauto. rewrite B; auto with asmgen. } - (* orimm *) - { exploit (opimm64_correct Porl Poril Val.orl); auto. instantiate (1 := x0); eauto with asmgen. - intros (rs' & A & B & C). - exists rs'; split; eauto. rewrite B; auto with asmgen. } - (* xorimm *) - { exploit (opimm64_correct Pxorl Pxoril Val.xorl); auto. instantiate (1 := x0); eauto with asmgen. - intros (rs' & A & B & C). - exists rs'; split; eauto. rewrite B; auto with asmgen. } - (* shrxlimm *) - { destruct (Val.shrxl (rs x0) (Vint n)) eqn:TOTAL. - { - exploit Val.shrxl_shrl_3; eauto. intros E; subst v. - destruct (Int.eq n Int.zero). - + econstructor; split. apply exec_straight_one. simpl; eauto. auto. - split; intros; Simpl. - + destruct (Int.eq n Int.one). - * econstructor; split. - eapply exec_straight_step. simpl; reflexivity. auto. - eapply exec_straight_step. simpl; reflexivity. auto. - apply exec_straight_one. simpl; reflexivity. auto. - split; intros; Simpl. - - * change (Int.repr 64) with Int64.iwordsize'. set (n' := Int.sub Int64.iwordsize' n). - econstructor; split. - eapply exec_straight_step. simpl; reflexivity. auto. - eapply exec_straight_step. simpl; reflexivity. auto. - eapply exec_straight_step. simpl; reflexivity. auto. - apply exec_straight_one. simpl; reflexivity. auto. - split; intros; Simpl. - } - destruct (Int.eq n Int.zero). - + econstructor; split. apply exec_straight_one. simpl; eauto. auto. - split; intros; Simpl. - + destruct (Int.eq n Int.one). - * econstructor; split. - eapply exec_straight_step. simpl; reflexivity. auto. - eapply exec_straight_step. simpl; reflexivity. auto. - apply exec_straight_one. simpl; reflexivity. auto. - split; intros; Simpl. - - * change (Int.repr 64) with Int64.iwordsize'. set (n' := Int.sub Int64.iwordsize' n). - econstructor; split. - eapply exec_straight_step. simpl; reflexivity. auto. - eapply exec_straight_step. simpl; reflexivity. auto. - eapply exec_straight_step. simpl; reflexivity. auto. - apply exec_straight_one. simpl; reflexivity. auto. - split; intros; Simpl. } - (* cond *) - { exploit transl_cond_op_correct; eauto. intros (rs' & A & B & C). - exists rs'; split. eexact A. eauto with asmgen. } (* Expanded instructions from RTL *) 9,10,19,20: econstructor; split; try apply exec_straight_one; simpl; eauto; diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml index def90a6a..5d739375 100644 --- a/riscV/ExpansionOracle.ml +++ b/riscV/ExpansionOracle.ml @@ -22,13 +22,11 @@ open! Integers open Camlcoq open Option open AST -open Printf +open DebugPrint (** Mini CSE (a dynamic numbering is applied during expansion. The CSE algorithm is inspired by the "static" one used in backend/CSE.v *) -let exp_debug = false - (** Managing virtual registers and node index *) let reg = ref 1 @@ -80,9 +78,9 @@ type numb = { } let print_list_pos l = - if exp_debug then eprintf "["; - List.iter (fun i -> if exp_debug then eprintf "%d;" (p2i i)) l; - if exp_debug then eprintf "]\n" + debug "["; + List.iter (fun i -> debug "%d;" (p2i i)) l; + debug "]\n" let empty_numbering () = { nnext = 1; seqs = []; nreg = Hashtbl.create 100; nval = Hashtbl.create 100 } @@ -93,11 +91,11 @@ let rec get_nvalues vn = function let v = match Hashtbl.find_opt !vn.nreg r with | Some v -> - if exp_debug then eprintf "getnval r=%d |-> v=%d\n" (p2i r) v; + debug "getnval r=%d |-> v=%d\n" (p2i r) v; v | None -> let n = !vn.nnext in - if exp_debug then eprintf "getnval r=%d |-> v=%d\n" (p2i r) n; + debug "getnval r=%d |-> v=%d\n" (p2i r) n; !vn.nnext <- !vn.nnext + 1; Hashtbl.replace !vn.nreg r n; Hashtbl.replace !vn.nval n [ r ]; @@ -112,17 +110,17 @@ let get_nval_ornil vn v = let forget_reg vn rd = match Hashtbl.find_opt !vn.nreg rd with | Some v -> - if exp_debug then eprintf "forget_reg: r=%d |-> v=%d\n" (p2i rd) v; + debug "forget_reg: r=%d |-> v=%d\n" (p2i rd) v; let old_regs = get_nval_ornil vn v in - if exp_debug then eprintf "forget_reg: old_regs are:\n"; + debug "forget_reg: old_regs are:\n"; print_list_pos old_regs; Hashtbl.replace !vn.nval v (List.filter (fun n -> not (P.eq n rd)) old_regs) | None -> - if exp_debug then eprintf "forget_reg: no mapping for r=%d\n" (p2i rd) + debug "forget_reg: no mapping for r=%d\n" (p2i rd) let update_reg vn rd v = - if exp_debug then eprintf "update_reg: update v=%d with r=%d\n" v (p2i rd); + debug "update_reg: update v=%d with r=%d\n" v (p2i rd); forget_reg vn rd; let old_regs = get_nval_ornil vn v in Hashtbl.replace !vn.nval v (rd :: old_regs) @@ -132,7 +130,7 @@ let rec find_valnum_rhs rh = function | Seq (v, rh') :: tl -> if rh = rh' then Some v else find_valnum_rhs rh tl let set_unknown vn rd = - if exp_debug then eprintf "set_unknown: rd=%d\n" (p2i rd); + debug "set_unknown: rd=%d\n" (p2i rd); forget_reg vn rd; Hashtbl.remove !vn.nreg rd @@ -141,19 +139,19 @@ let set_res_unknown vn res = match res with BR r -> set_unknown vn r | _ -> () let addrhs vn rd rh = match find_valnum_rhs rh !vn.seqs with | Some vres -> - if exp_debug then eprintf "addrhs: Some v=%d\n" vres; + debug "addrhs: Some v=%d\n" vres; Hashtbl.replace !vn.nreg rd vres; update_reg vn rd vres | None -> let n = !vn.nnext in - if exp_debug then eprintf "addrhs: None v=%d\n" n; + debug "addrhs: None v=%d\n" n; !vn.nnext <- !vn.nnext + 1; !vn.seqs <- Seq (n, rh) :: !vn.seqs; update_reg vn rd n; Hashtbl.replace !vn.nreg rd n let addsop vn v op rd = - if exp_debug then eprintf "addsop\n"; + debug "addsop\n"; if op = Omove then ( update_reg vn rd (List.hd v); Hashtbl.replace !vn.nreg rd (List.hd v)) @@ -167,11 +165,11 @@ let rec kill_mem_operations = function | eq :: tl -> eq :: kill_mem_operations tl let reg_valnum vn v = - if exp_debug then eprintf "reg_valnum: trying to find a mapping for v=%d\n" v; + debug "reg_valnum: trying to find a mapping for v=%d\n" v; match Hashtbl.find !vn.nval v with | [] -> None | r :: rs -> - if exp_debug then eprintf "reg_valnum: found a mapping r=%d\n" (p2i r); + debug "reg_valnum: found a mapping r=%d\n" (p2i r); Some r let rec reg_valnums vn = function @@ -216,7 +214,7 @@ let addinst vn op args rd = let rh = Sop (op, v) in match find_rhs vn rh with | Some r -> - if exp_debug then eprintf "addinst: rhs found with r=%d\n" (p2i r); + debug "addinst: rhs found with r=%d\n" (p2i r); Sr r | None -> addsop vn v op rd; @@ -627,8 +625,7 @@ let get_regs_inst = function (** Modify pathmap according to the size of the expansion list *) let write_pathmap initial esize pm' = - if exp_debug then - eprintf "write_pathmap: initial=%d, esize=%d\n" (p2i initial) esize; + debug "write_pathmap: initial=%d, esize=%d\n" (p2i initial) esize; 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' = @@ -655,7 +652,7 @@ let get_arguments vn vals args = (** Update the code tree with the expansion list *) let rec write_tree vn exp initial current code' new_order fturn = - if exp_debug then eprintf "wt: node is %d\n" !node; + debug "wt: node is %d\n" !node; let target_node, next_node = if fturn then (P.to_int initial, current) else (current, current - 1) in @@ -685,7 +682,7 @@ let rec write_tree vn exp initial current code' new_order fturn = (** Main expansion function - TODO gourdinl to split? *) let expanse (sb : superblock) code pm = - if exp_debug then eprintf "#### New superblock for expansion oracle\n"; + debug "#### New superblock for expansion oracle\n"; let new_order = ref [] in let liveins = ref sb.liveins in let exp = ref [] in @@ -699,139 +696,138 @@ let expanse (sb : superblock) code pm = was_branch := false; was_exp := false; let inst = get_some @@ PTree.get n code in - if exp_debug then eprintf "We are checking node %d\n" (p2i n); - (if !Clflags.option_fexpanse_rtlcond then - match inst with + debug "We are checking node %d\n" (p2i n); + (match inst with (* Expansion of conditions - Ocmp *) | Iop (Ocmp (Ccomp c), a1 :: a2 :: nil, dest, succ) -> - if exp_debug then eprintf "Iop/Ccomp\n"; + debug "Iop/Ccomp\n"; exp := cond_int32s vn false c a1 a2 dest; exp := extract_final vn !exp dest succ; was_exp := true | Iop (Ocmp (Ccompu c), a1 :: a2 :: nil, dest, succ) -> - if exp_debug then eprintf "Iop/Ccompu\n"; + debug "Iop/Ccompu\n"; exp := cond_int32u vn false c a1 a2 dest; exp := extract_final vn !exp dest succ; was_exp := true | Iop (Ocmp (Ccompimm (c, imm)), a1 :: nil, dest, succ) -> - if exp_debug then eprintf "Iop/Ccompimm\n"; + debug "Iop/Ccompimm\n"; exp := expanse_condimm_int32s vn c a1 imm dest; exp := extract_final vn !exp dest succ; was_exp := true | Iop (Ocmp (Ccompuimm (c, imm)), a1 :: nil, dest, succ) -> - if exp_debug then eprintf "Iop/Ccompuimm\n"; + debug "Iop/Ccompuimm\n"; exp := expanse_condimm_int32u vn c a1 imm dest; exp := extract_final vn !exp dest succ; was_exp := true | Iop (Ocmp (Ccompl c), a1 :: a2 :: nil, dest, succ) -> - if exp_debug then eprintf "Iop/Ccompl\n"; + debug "Iop/Ccompl\n"; exp := cond_int64s vn false c a1 a2 dest; exp := extract_final vn !exp dest succ; was_exp := true | Iop (Ocmp (Ccomplu c), a1 :: a2 :: nil, dest, succ) -> - if exp_debug then eprintf "Iop/Ccomplu\n"; + debug "Iop/Ccomplu\n"; exp := cond_int64u vn false c a1 a2 dest; exp := extract_final vn !exp dest succ; was_exp := true | Iop (Ocmp (Ccomplimm (c, imm)), a1 :: nil, dest, succ) -> - if exp_debug then eprintf "Iop/Ccomplimm\n"; + debug "Iop/Ccomplimm\n"; exp := expanse_condimm_int64s vn c a1 imm dest; exp := extract_final vn !exp dest succ; was_exp := true | Iop (Ocmp (Ccompluimm (c, imm)), a1 :: nil, dest, succ) -> - if exp_debug then eprintf "Iop/Ccompluimm\n"; + debug "Iop/Ccompluimm\n"; exp := expanse_condimm_int64u vn c a1 imm dest; exp := extract_final vn !exp dest succ; was_exp := true | Iop (Ocmp (Ccompf c), f1 :: f2 :: nil, dest, succ) -> - if exp_debug then eprintf "Iop/Ccompf\n"; + debug "Iop/Ccompf\n"; exp := expanse_cond_fp vn false cond_float c f1 f2 dest; exp := extract_final vn !exp dest succ; was_exp := true | Iop (Ocmp (Cnotcompf c), f1 :: f2 :: nil, dest, succ) -> - if exp_debug then eprintf "Iop/Cnotcompf\n"; + debug "Iop/Cnotcompf\n"; exp := expanse_cond_fp vn true cond_float c f1 f2 dest; exp := extract_final vn !exp dest succ; was_exp := true | Iop (Ocmp (Ccompfs c), f1 :: f2 :: nil, dest, succ) -> - if exp_debug then eprintf "Iop/Ccompfs\n"; + debug "Iop/Ccompfs\n"; exp := expanse_cond_fp vn false cond_single c f1 f2 dest; exp := extract_final vn !exp dest succ; was_exp := true | Iop (Ocmp (Cnotcompfs c), f1 :: f2 :: nil, dest, succ) -> - if exp_debug then eprintf "Iop/Cnotcompfs\n"; + debug "Iop/Cnotcompfs\n"; exp := expanse_cond_fp vn true cond_single c f1 f2 dest; exp := extract_final vn !exp dest succ; was_exp := true (* Expansion of branches - Ccomp *) | Icond (Ccomp c, a1 :: a2 :: nil, succ1, succ2, info) -> - if exp_debug then eprintf "Icond/Ccomp\n"; + debug "Icond/Ccomp\n"; exp := cbranch_int32s false c a1 a2 info succ1 succ2 []; was_branch := true; was_exp := true | Icond (Ccompu c, a1 :: a2 :: nil, succ1, succ2, info) -> - if exp_debug then eprintf "Icond/Ccompu\n"; + debug "Icond/Ccompu\n"; exp := cbranch_int32u false c a1 a2 info succ1 succ2 []; was_branch := true; was_exp := true | Icond (Ccompimm (c, imm), a1 :: nil, succ1, succ2, info) -> - if exp_debug then eprintf "Icond/Ccompimm\n"; + debug "Icond/Ccompimm\n"; exp := expanse_cbranchimm_int32s vn c a1 imm info succ1 succ2; was_branch := true; was_exp := true | Icond (Ccompuimm (c, imm), a1 :: nil, succ1, succ2, info) -> - if exp_debug then eprintf "Icond/Ccompuimm\n"; + debug "Icond/Ccompuimm\n"; exp := expanse_cbranchimm_int32u vn c a1 imm info succ1 succ2; was_branch := true; was_exp := true | Icond (Ccompl c, a1 :: a2 :: nil, succ1, succ2, info) -> - if exp_debug then eprintf "Icond/Ccompl\n"; + debug "Icond/Ccompl\n"; exp := cbranch_int64s false c a1 a2 info succ1 succ2 []; was_branch := true; was_exp := true | Icond (Ccomplu c, a1 :: a2 :: nil, succ1, succ2, info) -> - if exp_debug then eprintf "Icond/Ccomplu\n"; + debug "Icond/Ccomplu\n"; exp := cbranch_int64u false c a1 a2 info succ1 succ2 []; was_branch := true; was_exp := true | Icond (Ccomplimm (c, imm), a1 :: nil, succ1, succ2, info) -> - if exp_debug then eprintf "Icond/Ccomplimm\n"; + debug "Icond/Ccomplimm\n"; exp := expanse_cbranchimm_int64s vn c a1 imm info succ1 succ2; was_branch := true; was_exp := true | Icond (Ccompluimm (c, imm), a1 :: nil, succ1, succ2, info) -> - if exp_debug then eprintf "Icond/Ccompluimm\n"; + debug "Icond/Ccompluimm\n"; exp := expanse_cbranchimm_int64u vn c a1 imm info succ1 succ2; was_branch := true; was_exp := true | Icond (Ccompf c, f1 :: f2 :: nil, succ1, succ2, info) -> - if exp_debug then eprintf "Icond/Ccompf\n"; + debug "Icond/Ccompf\n"; exp := expanse_cbranch_fp vn false cond_float c f1 f2 info succ1 succ2; was_branch := true; was_exp := true | Icond (Cnotcompf c, f1 :: f2 :: nil, succ1, succ2, info) -> - if exp_debug then eprintf "Icond/Cnotcompf\n"; + debug "Icond/Cnotcompf\n"; exp := expanse_cbranch_fp vn true cond_float c f1 f2 info succ1 succ2; was_branch := true; was_exp := true | Icond (Ccompfs c, f1 :: f2 :: nil, succ1, succ2, info) -> - if exp_debug then eprintf "Icond/Ccompfs\n"; + debug "Icond/Ccompfs\n"; exp := expanse_cbranch_fp vn false cond_single c f1 f2 info succ1 succ2; was_branch := true; was_exp := true | Icond (Cnotcompfs c, f1 :: f2 :: nil, succ1, succ2, info) -> - if exp_debug then eprintf "Icond/Cnotcompfs\n"; + debug "Icond/Cnotcompfs\n"; exp := expanse_cbranch_fp vn true cond_single c f1 f2 info succ1 succ2; was_branch := true; was_exp := true | _ -> ()); - (if !Clflags.option_fexpanse_others && not !was_exp then + (if not !was_exp then match inst with | Iop (Ofloatconst f, nil, dest, succ) -> - if exp_debug then eprintf "Iop/Ofloatconst\n"; + debug "Iop/Ofloatconst\n"; let r = r2pi () in let l = loadimm64 vn r (Floats.Float.to_bits f) in let r', l' = extract_arg l in @@ -839,7 +835,7 @@ let expanse (sb : superblock) code pm = exp := extract_final vn !exp dest succ; was_exp := true | Iop (Osingleconst f, nil, dest, succ) -> - if exp_debug then eprintf "Iop/Osingleconst\n"; + debug "Iop/Osingleconst\n"; let r = r2pi () in let l = loadimm32 vn r (Floats.Float32.to_bits f) in let r', l' = extract_arg l in @@ -847,57 +843,57 @@ let expanse (sb : superblock) code pm = exp := extract_final vn !exp dest succ; was_exp := true | Iop (Ointconst n, nil, dest, succ) -> - if exp_debug then eprintf "Iop/Ointconst\n"; + debug "Iop/Ointconst\n"; exp := loadimm32 vn dest n; exp := extract_final vn !exp dest succ; was_exp := true | Iop (Olongconst n, nil, dest, succ) -> - if exp_debug then eprintf "Iop/Olongconst\n"; + debug "Iop/Olongconst\n"; exp := loadimm64 vn dest n; exp := extract_final vn !exp dest succ; was_exp := true | Iop (Oaddimm n, a1 :: nil, dest, succ) -> - if exp_debug then eprintf "Iop/Oaddimm\n"; + debug "Iop/Oaddimm\n"; exp := addimm32 vn a1 dest n None; exp := extract_final vn !exp dest succ; was_exp := true | Iop (Oaddlimm n, a1 :: nil, dest, succ) -> - if exp_debug then eprintf "Iop/Oaddlimm\n"; + debug "Iop/Oaddlimm\n"; exp := addimm64 vn a1 dest n None; exp := extract_final vn !exp dest succ; was_exp := true | Iop (Oandimm n, a1 :: nil, dest, succ) -> - if exp_debug then eprintf "Iop/Oandimm\n"; + debug "Iop/Oandimm\n"; exp := andimm32 vn a1 dest n; exp := extract_final vn !exp dest succ; was_exp := true | Iop (Oandlimm n, a1 :: nil, dest, succ) -> - if exp_debug then eprintf "Iop/Oandlimm\n"; + debug "Iop/Oandlimm\n"; exp := andimm64 vn a1 dest n; exp := extract_final vn !exp dest succ; was_exp := true | Iop (Oorimm n, a1 :: nil, dest, succ) -> - if exp_debug then eprintf "Iop/Oorimm\n"; + debug "Iop/Oorimm\n"; exp := orimm32 vn a1 dest n; exp := extract_final vn !exp dest succ; was_exp := true | Iop (Oorlimm n, a1 :: nil, dest, succ) -> - if exp_debug then eprintf "Iop/Oorlimm\n"; + debug "Iop/Oorlimm\n"; exp := orimm64 vn a1 dest n; exp := extract_final vn !exp dest succ; was_exp := true | Iop (Oxorimm n, a1 :: nil, dest, succ) -> - if exp_debug then eprintf "Iop/Oxorimm\n"; + debug "Iop/Oxorimm\n"; exp := xorimm32 vn a1 dest n; exp := extract_final vn !exp dest succ; was_exp := true | Iop (Oxorlimm n, a1 :: nil, dest, succ) -> - if exp_debug then eprintf "Iop/Oxorlimm\n"; + debug "Iop/Oxorlimm\n"; exp := xorimm64 vn a1 dest n; exp := extract_final vn !exp dest succ; was_exp := true | Iop (Ocast8signed, a1 :: nil, dest, succ) -> - if exp_debug then eprintf "Iop/cast8signed\n"; + debug "Iop/cast8signed\n"; let op = Oshlimm (Int.repr (Z.of_sint 24)) in let r = r2pi () in let i1 = addinst vn op [ a1 ] r in @@ -907,7 +903,7 @@ let expanse (sb : superblock) code pm = exp := extract_final vn !exp dest succ; was_exp := true | Iop (Ocast16signed, a1 :: nil, dest, succ) -> - if exp_debug then eprintf "Iop/cast16signed\n"; + debug "Iop/cast16signed\n"; let op = Oshlimm (Int.repr (Z.of_sint 16)) in let r = r2pi () in let i1 = addinst vn op [ a1 ] r in @@ -917,7 +913,7 @@ let expanse (sb : superblock) code pm = exp := extract_final vn !exp dest succ; was_exp := true | Iop (Ocast32unsigned, a1 :: nil, dest, succ) -> - if exp_debug then eprintf "Iop/Ocast32unsigned\n"; + debug "Iop/Ocast32unsigned\n"; let r1 = r2pi () in let r2 = r2pi () in let op1 = Ocast32signed in @@ -934,10 +930,10 @@ let expanse (sb : superblock) code pm = was_exp := true | Iop (Oshrximm n, a1 :: nil, dest, succ) -> if Int.eq n Int.zero then ( - if exp_debug then eprintf "Iop/Oshrximm1\n"; + debug "Iop/Oshrximm1\n"; exp := [ addinst vn (OEmayundef (MUshrx n)) [ a1; a1 ] dest ]) else if Int.eq n Int.one then ( - if exp_debug then eprintf "Iop/Oshrximm2\n"; + debug "Iop/Oshrximm2\n"; let r1 = r2pi () in let r2 = r2pi () in let op1 = Oshruimm (Int.repr (Z.of_sint 31)) in @@ -953,7 +949,7 @@ let expanse (sb : superblock) code pm = let r3, l3 = extract_arg (i3 :: l2) in exp := addinst vn (OEmayundef (MUshrx n)) [ r3; r3 ] dest :: l3) else ( - if exp_debug then eprintf "Iop/Oshrximm3\n"; + debug "Iop/Oshrximm3\n"; let r1 = r2pi () in let r2 = r2pi () in let r3 = r2pi () in @@ -977,10 +973,10 @@ let expanse (sb : superblock) code pm = was_exp := true | Iop (Oshrxlimm n, a1 :: nil, dest, succ) -> if Int.eq n Int.zero then ( - if exp_debug then eprintf "Iop/Oshrxlimm1\n"; + debug "Iop/Oshrxlimm1\n"; exp := [ addinst vn (OEmayundef (MUshrxl n)) [ a1; a1 ] dest ]) else if Int.eq n Int.one then ( - if exp_debug then eprintf "Iop/Oshrxlimm2\n"; + debug "Iop/Oshrxlimm2\n"; let r1 = r2pi () in let r2 = r2pi () in let op1 = Oshrluimm (Int.repr (Z.of_sint 63)) in @@ -996,7 +992,7 @@ let expanse (sb : superblock) code pm = let r3, l3 = extract_arg (i3 :: l2) in exp := addinst vn (OEmayundef (MUshrxl n)) [ r3; r3 ] dest :: l3) else ( - if exp_debug then eprintf "Iop/Oshrxlimm3\n"; + debug "Iop/Oshrxlimm3\n"; let r1 = r2pi () in let r2 = r2pi () in let r3 = r2pi () in diff --git a/riscV/RTLpathSE_simplify.v b/riscV/RTLpathSE_simplify.v index ca049962..7aca1772 100644 --- a/riscV/RTLpathSE_simplify.v +++ b/riscV/RTLpathSE_simplify.v @@ -853,6 +853,16 @@ Proof. destruct x; destruct y; simpl; auto. rewrite Float32.cmp_swap. auto. Qed. +Remark cast32unsigned_from_cast32signed: + forall i, Int64.repr (Int.unsigned i) = Int64.zero_ext 32 (Int64.repr (Int.signed i)). +Proof. + intros. apply Int64.same_bits_eq; intros. + rewrite Int64.bits_zero_ext, !Int64.testbit_repr by tauto. + rewrite Int.bits_signed by tauto. fold (Int.testbit i i0). + change Int.zwordsize with 32. + destruct (zlt i0 32). auto. apply Int.bits_above. auto. +Qed. + (** * Intermediates lemmas on each expanded instruction *) Lemma simplify_ccomp_correct ge sp hst st c r r0 rs0 m0 v v0: forall |