diff options
Diffstat (limited to 'powerpc')
| -rw-r--r-- | powerpc/Archi.v | 12 | ||||
| -rw-r--r-- | powerpc/Asm.v | 177 | ||||
| -rw-r--r-- | powerpc/AsmToJSON.ml | 74 | ||||
| -rw-r--r-- | powerpc/Asmexpand.ml | 75 | ||||
| -rw-r--r-- | powerpc/Asmgen.v | 172 | ||||
| -rw-r--r-- | powerpc/Asmgenproof.v | 43 | ||||
| -rw-r--r-- | powerpc/Asmgenproof1.v | 405 | ||||
| -rw-r--r-- | powerpc/ConstpropOp.vp | 6 | ||||
| -rw-r--r-- | powerpc/ConstpropOpproof.v | 6 | ||||
| -rw-r--r-- | powerpc/Conventions1.v | 102 | ||||
| -rw-r--r-- | powerpc/Machregs.v | 23 | ||||
| -rw-r--r-- | powerpc/NeedOp.v | 5 | ||||
| -rw-r--r-- | powerpc/Op.v | 278 | ||||
| -rw-r--r-- | powerpc/PrintOp.ml | 26 | ||||
| -rw-r--r-- | powerpc/SelectLong.vp | 335 | ||||
| -rw-r--r-- | powerpc/SelectLongproof.v | 625 | ||||
| -rw-r--r-- | powerpc/SelectOp.vp | 19 | ||||
| -rw-r--r-- | powerpc/SelectOpproof.v | 9 | ||||
| -rw-r--r-- | powerpc/Stacklayout.v | 2 | ||||
| -rw-r--r-- | powerpc/TargetPrinter.ml | 138 | ||||
| -rw-r--r-- | powerpc/ValueAOp.v | 33 | ||||
| -rw-r--r-- | powerpc/extractionMachdep.v | 2 |
22 files changed, 2378 insertions, 189 deletions
diff --git a/powerpc/Archi.v b/powerpc/Archi.v index 10dc5534..5d11aad1 100644 --- a/powerpc/Archi.v +++ b/powerpc/Archi.v @@ -27,11 +27,14 @@ Definition big_endian := true. Definition align_int64 := 8%Z. Definition align_float64 := 8%Z. -Definition splitlong := true. +(** Can we use the 64-bit extensions to the PowerPC architecture? *) +Parameter ppc64 : bool. + +Definition splitlong := negb ppc64. Lemma splitlong_ptr32: splitlong = true -> ptr64 = false. Proof. - unfold splitlong, ptr64; congruence. + reflexivity. Qed. Program Definition default_pl_64 : bool * nan_pl 53 := @@ -51,7 +54,4 @@ Definition float_of_single_preserves_sNaN := true. Global Opaque ptr64 big_endian splitlong default_pl_64 choose_binop_pl_64 default_pl_32 choose_binop_pl_32 - float_of_single_preserves_sNaN. - -(** Can we use the 64-bit extensions to the PowerPC architecture? *) -Parameter ppc64: bool. + float_of_single_preserves_sNaN.
\ No newline at end of file diff --git a/powerpc/Asm.v b/powerpc/Asm.v index cc554eb1..746a610b 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -136,17 +136,24 @@ Definition label := positive. Inductive instruction : Type := | Padd: ireg -> ireg -> ireg -> instruction (**r integer addition *) + | Padd64: ireg -> ireg -> ireg -> instruction (**r integer addition (PPC64) *) | Paddc: ireg -> ireg -> ireg -> instruction (**r integer addition and set carry *) | Padde: ireg -> ireg -> ireg -> instruction (**r integer addition with carry *) | Paddi: ireg -> ireg -> constant -> instruction (**r add immediate *) + | Paddi64: ireg -> ireg -> int64 -> instruction (**r add immediate (PPC64) *) | Paddic: ireg -> ireg -> constant -> instruction (**r add immediate and set carry *) | Paddis: ireg -> ireg -> constant -> instruction (**r add immediate high *) + | Paddis64: ireg -> ireg -> int64 -> instruction (**r add immediate high (PPC64) *) | Paddze: ireg -> ireg -> instruction (**r add carry *) - | Pallocframe: Z -> ptrofs -> ptrofs -> instruction (**r allocate new stack frame (pseudo) *) + | Paddze64: ireg -> ireg -> instruction (**r add carry (PPC64) *) + | Pallocframe: Z -> ptrofs -> ptrofs -> instruction (**r allocate new stack frame (pseudo) *) | Pand_: ireg -> ireg -> ireg -> instruction (**r bitwise and *) + | Pand_64: ireg -> ireg -> ireg -> instruction (**r bitwise and (PPC64) *) | Pandc: ireg -> ireg -> ireg -> instruction (**r bitwise and-complement *) | Pandi_: ireg -> ireg -> constant -> instruction (**r and immediate and set conditions *) + | Pandi_64: ireg -> ireg -> int64 -> instruction (**r and immediate and set conditions (PPC64) *) | Pandis_: ireg -> ireg -> constant -> instruction (**r and immediate high and set conditions *) + | Pandis_64: ireg -> ireg -> int64 -> instruction (**r and immediate high and set conditions (PPC64) *) | Pb: label -> instruction (**r unconditional branch *) | Pbctr: signature -> instruction (**r branch to contents of register CTR *) | Pbctrl: signature -> instruction (**r branch to contents of CTR and link *) @@ -158,10 +165,15 @@ Inductive instruction : Type := | Pbt: crbit -> label -> instruction (**r branch if true *) | Pbtbl: ireg -> list label -> instruction (**r N-way branch through a jump table (pseudo) *) | Pcmpb: ireg -> ireg -> ireg -> instruction (**r compare bytes *) + | Pcmpld: ireg -> ireg -> instruction (**r unsigned integer comparison (PPC64) *) + | Pcmpldi: ireg -> int64 -> instruction (**r same, with immediate argument (PPC64) *) | Pcmplw: ireg -> ireg -> instruction (**r unsigned integer comparison *) | Pcmplwi: ireg -> constant -> instruction (**r same, with immediate argument *) + | Pcmpd: ireg -> ireg -> instruction (**r signed integer comparison (PPC64) *) + | Pcmpdi: ireg -> int64 -> instruction (**r same, with immediate argument (PPC64) *) | Pcmpw: ireg -> ireg -> instruction (**r signed integer comparison *) | Pcmpwi: ireg -> constant -> instruction (**r same, with immediate argument *) + | Pcntlzd: ireg -> ireg -> instruction (**r count leading zeros (PPC64) *) | Pcntlzw: ireg -> ireg -> instruction (**r count leading zeros *) | Pcreqv: crbit -> crbit -> crbit -> instruction (**r not-xor between condition bits *) | Pcror: crbit -> crbit -> crbit -> instruction (**r or between condition bits *) @@ -173,23 +185,28 @@ Inductive instruction : Type := | Pdcbtls: int -> ireg -> ireg -> instruction (**r data cache block touch and lock *) | Pdcbz: ireg -> ireg -> instruction (**r data cache block zero *) | Pdivw: ireg -> ireg -> ireg -> instruction (**r signed division *) + | Pdivd: ireg -> ireg -> ireg -> instruction (**r signed division (PPC64) *) | Pdivwu: ireg -> ireg -> ireg -> instruction (**r unsigned division *) + | Pdivdu: ireg -> ireg -> ireg -> instruction (**r unsigned division (PPC64) *) | Peieio: instruction (**r EIEIO barrier *) | Peqv: ireg -> ireg -> ireg -> instruction (**r bitwise not-xor *) | Pextsb: ireg -> ireg -> instruction (**r 8-bit sign extension *) | Pextsh: ireg -> ireg -> instruction (**r 16-bit sign extension *) | Pextsw: ireg -> ireg -> instruction (**r 64-bit sign extension (PPC64) *) - | Pfreeframe: Z -> ptrofs -> instruction (**r deallocate stack frame and restore previous frame (pseudo) *) + | Pextzw: ireg -> ireg -> instruction (**r 64-bit zero extension (pseudo, PPC64) *) + | Pfreeframe: Z -> ptrofs -> instruction (**r deallocate stack frame and restore previous frame (pseudo) *) | Pfabs: freg -> freg -> instruction (**r float absolute value *) | Pfabss: freg -> freg -> instruction (**r float absolute value *) | Pfadd: freg -> freg -> freg -> instruction (**r float addition *) | Pfadds: freg -> freg -> freg -> instruction (**r float addition *) | Pfcmpu: freg -> freg -> instruction (**r float comparison *) | Pfcfi: freg -> ireg -> instruction (**r signed-int-to-float conversion (pseudo, PPC64) *) + | Pfcfl: freg -> ireg -> instruction (**r signed-long-to-float conversion (pseudo, PPC64) *) | Pfcfiu: freg -> ireg -> instruction (**r unsigned-int-to-float conversion (pseudo, PPC64) *) | Pfcfid: freg -> freg -> instruction (**r signed-long-to-float conversion (PPC64) *) | Pfcti: ireg -> freg -> instruction (**r float-to-signed-int conversion, round towards 0 (pseudo) *) | Pfctiu: ireg -> freg -> instruction (**r float-to-unsigned-int conversion, round towards 0 (pseudo, PPC64) *) + | Pfctid: ireg -> freg -> instruction (**r float-to-signed-int conversion, round towards 0 (pseudo, PPC64) *) | Pfctidz: freg -> freg -> instruction (**r float-to-signed-long conversion, round towards 0 (PPC64) *) | Pfctiw: freg -> freg -> instruction (**r float-to-signed-int conversion, round by default *) | Pfctiwz: freg -> freg -> instruction (**r float-to-signed-int conversion, round towards 0 *) @@ -219,6 +236,10 @@ Inductive instruction : Type := | Picbtls: int -> ireg -> ireg -> instruction (**r instruction cache block touch and lock set *) | Plbz: ireg -> constant -> ireg -> instruction (**r load 8-bit unsigned int *) | Plbzx: ireg -> ireg -> ireg -> instruction (**r same, with 2 index regs *) + | Pld: ireg -> constant -> ireg -> instruction (**r load 64-bit int (PPC64) *) + | Pldx: ireg -> ireg -> ireg -> instruction (**r same, with 2 index regs *) + | Pld_a: ireg -> constant -> ireg -> instruction (**r load 64-bit quantity to int reg (PPC64) *) + | Pldx_a: ireg -> ireg -> ireg -> instruction (**r same, with 2 index regs *) | Plfd: freg -> constant -> ireg -> instruction (**r load 64-bit float *) | Plfdx: freg -> ireg -> ireg -> instruction (**r same, with 2 index regs *) | Plfd_a: freg -> constant -> ireg -> instruction (**r load 64-bit quantity to float reg *) @@ -230,6 +251,10 @@ Inductive instruction : Type := | Plhbrx: ireg -> ireg -> ireg -> instruction (**r load 16-bit int and reverse endianness *) | Plhz: ireg -> constant -> ireg -> instruction (**r load 16-bit unsigned int *) | Plhzx: ireg -> ireg -> ireg -> instruction (**r same, with 2 index regs *) + | Pldi: ireg -> int64 -> instruction (**r load 64-bit int constant (PPC64) *) + | Plmake: ireg -> ireg -> ireg -> instruction (**r build an int64 from 2 ints (pseudo, PPC64) *) + | Pllo: ireg -> instruction (**r extract low 32 bits of an int64 (pseudo, PPC64) *) + | Plhi: ireg -> ireg -> instruction (**r extract high 32 bits of an int64 (pseudo, PPC64) *) | Plfi: freg -> float -> instruction (**r load float constant *) | Plfis: freg -> float32 -> instruction (**r load float constant *) | Plwz: ireg -> constant -> ireg -> instruction (**r load 32-bit int *) @@ -250,25 +275,41 @@ Inductive instruction : Type := | Pmtspr: int -> ireg -> instruction (**r move to special register *) | Pmulli: ireg -> ireg -> constant -> instruction (**r integer multiply immediate *) | Pmullw: ireg -> ireg -> ireg -> instruction (**r integer multiply *) + | Pmulld: ireg -> ireg -> ireg -> instruction (**r integer multiply (PPC64) *) | Pmulhw: ireg -> ireg -> ireg -> instruction (**r multiply high signed *) | Pmulhwu: ireg -> ireg -> ireg -> instruction (**r multiply high signed *) + | Pmulhd: ireg -> ireg -> ireg -> instruction (**r multiply high double word signed (PPC64) *) + | Pmulhdu: ireg -> ireg -> ireg -> instruction (**r multiply high double word unsigned (PPC64) *) | Pnand: ireg -> ireg -> ireg -> instruction (**r bitwise not-and *) | Pnor: ireg -> ireg -> ireg -> instruction (**r bitwise not-or *) + | Pnor64: ireg -> ireg -> ireg -> instruction (**r bitwise not-or (PPC64) *) | Por: ireg -> ireg -> ireg -> instruction (**r bitwise or *) + | Por64: ireg -> ireg -> ireg -> instruction (**r bitwise or (PPC64) *) | Porc: ireg -> ireg -> ireg -> instruction (**r bitwise or-complement *) | Pori: ireg -> ireg -> constant -> instruction (**r or with immediate *) + | Pori64: ireg -> ireg -> int64 -> instruction (**r or with immediate (PPC64) *) | Poris: ireg -> ireg -> constant -> instruction (**r or with immediate high *) + | Poris64: ireg -> ireg -> int64 -> instruction (**r or with immediate high (PPC64) *) | Prldicl: ireg -> ireg -> int -> int -> instruction (**r rotate and mask left (PPC64) *) - | Prldicr: ireg -> ireg -> int -> int -> instruction (**r rotate and mask right (PPC64) *) + | Prldinm: ireg -> ireg -> int -> int64 -> instruction (**r rotate and mask (PPC64) *) + | Prldimi: ireg -> ireg -> int -> int64 -> instruction (**r rotate and insert (PPC64) *) | Prlwinm: ireg -> ireg -> int -> int -> instruction (**r rotate and mask *) | Prlwimi: ireg -> ireg -> int -> int -> instruction (**r rotate and insert *) + | Psld: ireg -> ireg -> ireg -> instruction (**r shift left 64 bits (PPC64) *) | Pslw: ireg -> ireg -> ireg -> instruction (**r shift left *) + | Psrad: ireg -> ireg -> ireg -> instruction (**r shift right signed 64 bits (PPC64) *) + | Psradi: ireg -> ireg -> int -> instruction (**r shift right signed immediate 64 bits (PPC64) *) | Psraw: ireg -> ireg -> ireg -> instruction (**r shift right signed *) | Psrawi: ireg -> ireg -> int -> instruction (**r shift right signed immediate *) + | Psrd: ireg -> ireg -> ireg -> instruction (**r shift right unsigned 64 bits (PPC64) *) | Psrw: ireg -> ireg -> ireg -> instruction (**r shift right unsigned *) | Pstb: ireg -> constant -> ireg -> instruction (**r store 8-bit int *) | Pstbx: ireg -> ireg -> ireg -> instruction (**r same, with 2 index regs *) + | Pstd: ireg -> constant -> ireg -> instruction (**r store 64-bit integer (PPC64) *) + | Pstdx: ireg -> ireg -> ireg -> instruction (**r same, with 2 index regs (PPC64) *) | Pstdu: ireg -> constant -> ireg -> instruction (**r store 64-bit integer with update (PPC64) *) + | Pstd_a: ireg -> constant -> ireg -> instruction (**r store 64-bit quantity from int reg (PPC64) *) + | Pstdx_a: ireg -> ireg -> ireg -> instruction (**r same, with 2 index regs (PPC64) *) | Pstfd: freg -> constant -> ireg -> instruction (**r store 64-bit float *) | Pstfdu: freg -> constant -> ireg -> instruction (**r store 64-bit float with update *) | Pstfdx: freg -> ireg -> ireg -> instruction (**r same, with 2 index regs *) @@ -288,15 +329,20 @@ Inductive instruction : Type := | Pstwbrx: ireg -> ireg -> ireg -> instruction (**r store 32-bit int with reverse endianness *) | Pstwcx_: ireg -> ireg -> ireg -> instruction (**r store conditional *) | Psubfc: ireg -> ireg -> ireg -> instruction (**r reversed integer subtraction *) + | Psubfc64: ireg -> ireg -> ireg -> instruction (**r reversed integer subtraction (PPC64) *) | Psubfe: ireg -> ireg -> ireg -> instruction (**r reversed integer subtraction with carry *) | Psubfze: ireg -> ireg -> instruction (**r integer opposite with carry *) | Psubfic: ireg -> ireg -> constant -> instruction (**r integer subtraction from immediate *) + | Psubfic64: ireg -> ireg -> int64 -> instruction (**r integer subtraction from immediate (PPC64) *) | Psync: instruction (**r SYNC barrier *) | Plwsync: instruction (**r LWSYNC barrier *) | Ptrap: instruction (**r unconditional trap *) | Pxor: ireg -> ireg -> ireg -> instruction (**r bitwise xor *) + | Pxor64: ireg -> ireg -> ireg -> instruction (**r bitwise xor (PPC64) *) | Pxori: ireg -> ireg -> constant -> instruction (**r bitwise xor with immediate *) + | Pxori64: ireg -> ireg -> int64 -> instruction (**r bitwise xor with immediate (PPC64) *) | Pxoris: ireg -> ireg -> constant -> instruction (**r bitwise xor with immediate high *) + | Pxoris64: ireg -> ireg -> int64 -> instruction (**r bitwise xor with immediate high (PPC64) *) | Plabel: label -> instruction (**r define a code label *) | Pbuiltin: external_function -> list (builtin_arg preg) -> builtin_res preg -> instruction (**r built-in function (pseudo) *) | Pcfi_adjust: int -> instruction (**r .cfi_adjust debug directive *) @@ -452,7 +498,10 @@ Fixpoint label_pos (lbl: label) (pos: Z) (c: code) {struct c} : option Z := when that register is used in argument position. *) Definition gpr_or_zero (rs: regset) (r: ireg) := - if ireg_eq r GPR0 then Vzero else rs#r. + if ireg_eq r GPR0 then Vint Int.zero else rs#r. + +Definition gpr_or_zero_l (rs: regset) (r: ireg) := + if ireg_eq r GPR0 then Vlong Int64.zero else rs#r. Variable ge: genv. @@ -597,6 +646,18 @@ Definition compare_uint (rs: regset) (m: mem) (v1 v2: val) := #CR0_2 <- (Val.cmpu (Mem.valid_pointer m) Ceq v1 v2) #CR0_3 <- Vundef. +Definition compare_slong (rs: regset) (v1 v2: val) := + rs#CR0_0 <- (Val.of_optbool (Val.cmpl_bool Clt v1 v2)) + #CR0_1 <- (Val.of_optbool (Val.cmpl_bool Cgt v1 v2)) + #CR0_2 <- (Val.of_optbool (Val.cmpl_bool Ceq v1 v2)) + #CR0_3 <- Vundef. + +Definition compare_ulong (rs: regset) (m: mem) (v1 v2: val) := + rs#CR0_0 <- (Val.of_optbool (Val.cmplu_bool (Mem.valid_pointer m) Clt v1 v2)) + #CR0_1 <- (Val.of_optbool (Val.cmplu_bool (Mem.valid_pointer m) Cgt v1 v2)) + #CR0_2 <- (Val.of_optbool (Val.cmplu_bool (Mem.valid_pointer m) Ceq v1 v2)) + #CR0_3 <- Vundef. + Definition compare_float (rs: regset) (v1 v2: val) := rs#CR0_0 <- (Val.cmpf Clt v1 v2) #CR0_1 <- (Val.cmpf Cgt v1 v2) @@ -619,6 +680,8 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out match i with | Padd rd r1 r2 => Next (nextinstr (rs#rd <- (Val.add rs#r1 rs#r2))) m + | Padd64 rd r1 r2 => + Next (nextinstr (rs#rd <- (Val.addl rs#r1 rs#r2))) m | Paddc rd r1 r2 => Next (nextinstr (rs#rd <- (Val.add rs#r1 rs#r2) #CARRY <- (Val.add_carry rs#r1 rs#r2 Vzero))) m @@ -627,14 +690,21 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out #CARRY <- (Val.add_carry rs#r1 rs#r2 rs#CARRY))) m | Paddi rd r1 cst => Next (nextinstr (rs#rd <- (Val.add (gpr_or_zero rs r1) (const_low cst)))) m + | Paddi64 rd r1 cst => + Next (nextinstr (rs#rd <- (Val.addl (gpr_or_zero_l rs r1) (Vlong cst)))) m | Paddic rd r1 cst => Next (nextinstr (rs#rd <- (Val.add (gpr_or_zero rs r1) (const_low cst)) #CARRY <- (Val.add_carry (gpr_or_zero rs r1) (const_low cst) Vzero))) m | Paddis rd r1 cst => Next (nextinstr (rs#rd <- (Val.add (gpr_or_zero rs r1) (const_high cst)))) m + | Paddis64 rd r1 cst => + Next (nextinstr (rs#rd <- (Val.addl (gpr_or_zero_l rs r1) (Vlong (Int64.shl cst (Int64.repr 16)))))) m | Paddze rd r1 => Next (nextinstr (rs#rd <- (Val.add rs#r1 rs#CARRY) #CARRY <- (Val.add_carry rs#r1 Vzero rs#CARRY))) m + | Paddze64 rd r1 => + Next (nextinstr (rs#rd <- (Val.addl rs#r1 rs#CARRY) + #CARRY <- (Val.addl_carry rs#r1 (Vlong Int64.zero) rs#CARRY))) m | Pallocframe sz ofs _ => let (m1, stk) := Mem.alloc m 0 sz in let sp := Vptr stk Ptrofs.zero in @@ -645,14 +715,23 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pand_ rd r1 r2 => let v := Val.and rs#r1 rs#r2 in Next (nextinstr (compare_sint (rs#rd <- v) v Vzero)) m + | Pand_64 rd r1 r2 => + let v := Val.andl rs#r1 rs#r2 in + Next (nextinstr (compare_slong (rs#rd <- v) v (Vlong Int64.zero))) m | Pandc rd r1 r2 => Next (nextinstr (rs#rd <- (Val.and rs#r1 (Val.notint rs#r2)))) m | Pandi_ rd r1 cst => let v := Val.and rs#r1 (const_low cst) in Next (nextinstr (compare_sint (rs#rd <- v) v Vzero)) m + | Pandi_64 rd r1 cst => + let v := Val.andl rs#r1 (Vlong cst) in + Next (nextinstr (compare_slong (rs#rd <- v) v (Vlong Int64.zero))) m | Pandis_ rd r1 cst => let v := Val.and rs#r1 (const_high cst) in Next (nextinstr (compare_sint (rs#rd <- v) v Vzero)) m + | Pandis_64 rd r1 cst => + let v := Val.andl rs#r1 (Vlong (Int64.shl cst (Int64.repr 16))) in + Next (nextinstr (compare_slong (rs#rd <- v) v (Vlong Int64.zero))) m | Pb lbl => goto_label f lbl rs m | Pbctr sg => @@ -684,10 +763,18 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out end | _ => Stuck end + | Pcmpld r1 r2 => + Next (nextinstr (compare_ulong rs m rs#r1 rs#r2)) m + | Pcmpldi r1 cst => + Next (nextinstr (compare_ulong rs m rs#r1 (Vlong cst))) m | Pcmplw r1 r2 => Next (nextinstr (compare_uint rs m rs#r1 rs#r2)) m | Pcmplwi r1 cst => Next (nextinstr (compare_uint rs m rs#r1 (const_low cst))) m + | Pcmpd r1 r2 => + Next (nextinstr (compare_slong rs rs#r1 rs#r2)) m + | Pcmpdi r1 cst => + Next (nextinstr (compare_slong rs rs#r1 (Vlong cst))) m | Pcmpw r1 r2 => Next (nextinstr (compare_sint rs rs#r1 rs#r2)) m | Pcmpwi r1 cst => @@ -696,14 +783,22 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out Next (nextinstr (rs#(reg_of_crbit bd) <- (Val.or rs#(reg_of_crbit b1) rs#(reg_of_crbit b2)))) m | Pdivw rd r1 r2 => Next (nextinstr (rs#rd <- (Val.maketotal (Val.divs rs#r1 rs#r2)))) m + | Pdivd rd r1 r2 => + Next (nextinstr (rs#rd <- (Val.maketotal (Val.divls rs#r1 rs#r2)))) m | Pdivwu rd r1 r2 => Next (nextinstr (rs#rd <- (Val.maketotal (Val.divu rs#r1 rs#r2)))) m + | Pdivdu rd r1 r2 => + Next (nextinstr (rs#rd <- (Val.maketotal (Val.divlu rs#r1 rs#r2)))) m | Peqv rd r1 r2 => Next (nextinstr (rs#rd <- (Val.notint (Val.xor rs#r1 rs#r2)))) m | Pextsb rd r1 => Next (nextinstr (rs#rd <- (Val.sign_ext 8 rs#r1))) m | Pextsh rd r1 => Next (nextinstr (rs#rd <- (Val.sign_ext 16 rs#r1))) m + | Pextsw rd r1 => + Next (nextinstr (rs#rd <- (Val.longofint rs#r1))) m + | Pextzw rd r1 => + Next (nextinstr (rs#rd <- (Val.longofintu rs#r1))) m | Pfreeframe sz ofs => match Mem.loadv Mint32 m (Val.offset_ptr rs#GPR1 ofs) with | None => Stuck @@ -729,12 +824,16 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out Next (nextinstr (compare_float rs rs#r1 rs#r2)) m | Pfcfi rd r1 => Next (nextinstr (rs#rd <- (Val.maketotal (Val.floatofint rs#r1)))) m + | Pfcfl rd r1 => + Next (nextinstr (rs#rd <- (Val.maketotal (Val.floatoflong rs#r1)))) m | Pfcfiu rd r1 => Next (nextinstr (rs#rd <- (Val.maketotal (Val.floatofintu rs#r1)))) m | Pfcti rd r1 => Next (nextinstr (rs#FPR13 <- Vundef #rd <- (Val.maketotal (Val.intoffloat rs#r1)))) m | Pfctiu rd r1 => Next (nextinstr (rs#FPR13 <- Vundef #rd <- (Val.maketotal (Val.intuoffloat rs#r1)))) m + | Pfctid rd r1 => + Next (nextinstr (rs#FPR13 <- Vundef #rd <- (Val.maketotal (Val.longoffloat rs#r1)))) m | Pfdiv rd r1 r2 => Next (nextinstr (rs#rd <- (Val.divf rs#r1 rs#r2))) m | Pfdivs rd r1 r2 => @@ -763,12 +862,20 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out load1 Mint8unsigned rd cst r1 rs m | Plbzx rd r1 r2 => load2 Mint8unsigned rd r1 r2 rs m + | Pld rd cst r1 => + load1 Mint64 rd cst r1 rs m + | Pldx rd r1 r2 => + load2 Mint64 rd r1 r2 rs m + | Pld_a rd cst r1 => + load1 Many64 rd cst r1 rs m + | Pldx_a rd r1 r2 => + load2 Many64 rd r1 r2 rs m | Plfd rd cst r1 => load1 Mfloat64 rd cst r1 rs m - | Plfdx rd r1 r2 => - load2 Mfloat64 rd r1 r2 rs m | Plfd_a rd cst r1 => load1 Many64 rd cst r1 rs m + | Plfdx rd r1 r2 => + load2 Mfloat64 rd r1 r2 rs m | Plfdx_a rd r1 r2 => load2 Many64 rd r1 r2 rs m | Plfs rd cst r1 => @@ -783,6 +890,14 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out load1 Mint16unsigned rd cst r1 rs m | Plhzx rd r1 r2 => load2 Mint16unsigned rd r1 r2 rs m + | Pldi rd i => + Next (nextinstr (rs #GPR12 <- Vundef #rd <- (Vlong i))) m + | Plmake rd r1 r2 => + Next (nextinstr (rs#rd <- (Val.longofwords rs#r1 rs#r2))) m + | Pllo rd => + Next (nextinstr (rs#rd <- (Val.loword rs#rd))) m + | Plhi rd r1 => + Next (nextinstr (rs#rd <- (Val.hiword rs#r1))) m | Plfi rd f => Next (nextinstr (rs #GPR12 <- Vundef #rd <- (Vfloat f))) m | Plfis rd f => @@ -809,39 +924,71 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out Next (nextinstr (rs#rd <- (Val.mul rs#r1 (const_low cst)))) m | Pmullw rd r1 r2 => Next (nextinstr (rs#rd <- (Val.mul rs#r1 rs#r2))) m + | Pmulld rd r1 r2 => + Next (nextinstr (rs#rd <- (Val.mull rs#r1 rs#r2))) m | Pmulhw rd r1 r2 => Next (nextinstr (rs#rd <- (Val.mulhs rs#r1 rs#r2))) m | Pmulhwu rd r1 r2 => Next (nextinstr (rs#rd <- (Val.mulhu rs#r1 rs#r2))) m + | Pmulhd rd r1 r2 => + Next (nextinstr (rs#rd <- (Val.mullhs rs#r1 rs#r2))) m + | Pmulhdu rd r1 r2 => + Next (nextinstr (rs#rd <- (Val.mullhu rs#r1 rs#r2))) m | Pnand rd r1 r2 => Next (nextinstr (rs#rd <- (Val.notint (Val.and rs#r1 rs#r2)))) m | Pnor rd r1 r2 => Next (nextinstr (rs#rd <- (Val.notint (Val.or rs#r1 rs#r2)))) m + | Pnor64 rd r1 r2 => + Next (nextinstr (rs#rd <- (Val.notl (Val.orl rs#r1 rs#r2)))) m | Por rd r1 r2 => Next (nextinstr (rs#rd <- (Val.or rs#r1 rs#r2))) m + | Por64 rd r1 r2 => + Next (nextinstr (rs#rd <- (Val.orl rs#r1 rs#r2))) m | Porc rd r1 r2 => Next (nextinstr (rs#rd <- (Val.or rs#r1 (Val.notint rs#r2)))) m | Pori rd r1 cst => Next (nextinstr (rs#rd <- (Val.or rs#r1 (const_low cst)))) m + | Pori64 rd r1 cst => + Next (nextinstr (rs#rd <- (Val.orl rs#r1 (Vlong cst)))) m | Poris rd r1 cst => Next (nextinstr (rs#rd <- (Val.or rs#r1 (const_high cst)))) m + | Poris64 rd r1 cst => + Next (nextinstr (rs#rd <- (Val.orl rs#r1 (Vlong (Int64.shl cst (Int64.repr 16)))))) m + | Prldinm rd r1 amount mask => + Next (nextinstr (rs#rd <- (Val.rolml rs#r1 amount mask))) m | Prlwinm rd r1 amount mask => Next (nextinstr (rs#rd <- (Val.rolm rs#r1 amount mask))) m | Prlwimi rd r1 amount mask => Next (nextinstr (rs#rd <- (Val.or (Val.and rs#rd (Vint (Int.not mask))) (Val.rolm rs#r1 amount mask)))) m + | Psld rd r1 r2 => + Next (nextinstr (rs#rd <- (Val.shll rs#r1 rs#r2))) m | Pslw rd r1 r2 => Next (nextinstr (rs#rd <- (Val.shl rs#r1 rs#r2))) m + | Psrad rd r1 r2 => + Next (nextinstr (rs#rd <- (Val.shrl rs#r1 rs#r2) #CARRY <- (Val.shrl_carry rs#r1 rs#r2))) m + | Psradi rd r1 n => + Next (nextinstr (rs#rd <- (Val.shrl rs#r1 (Vint n)) #CARRY <- (Val.shrl_carry rs#r1 (Vint n)))) m | Psraw rd r1 r2 => Next (nextinstr (rs#rd <- (Val.shr rs#r1 rs#r2) #CARRY <- (Val.shr_carry rs#r1 rs#r2))) m | Psrawi rd r1 n => Next (nextinstr (rs#rd <- (Val.shr rs#r1 (Vint n)) #CARRY <- (Val.shr_carry rs#r1 (Vint n)))) m + | Psrd rd r1 r2 => + Next (nextinstr (rs#rd <- (Val.shrlu rs#r1 rs#r2))) m | Psrw rd r1 r2 => Next (nextinstr (rs#rd <- (Val.shru rs#r1 rs#r2))) m | Pstb rd cst r1 => store1 Mint8unsigned rd cst r1 rs m | Pstbx rd r1 r2 => store2 Mint8unsigned rd r1 r2 rs m + | Pstd rd cst r1 => + store1 Mint64 rd cst r1 rs m + | Pstdx rd r1 r2 => + store2 Mint64 rd r1 r2 rs m + | Pstd_a rd cst r1 => + store1 Many64 rd cst r1 rs m + | Pstdx_a rd r1 r2 => + store2 Many64 rd r1 r2 rs m | Pstfd rd cst r1 => store1 Mfloat64 rd cst r1 rs m | Pstfdx rd r1 r2 => @@ -869,18 +1016,28 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Psubfc rd r1 r2 => Next (nextinstr (rs#rd <- (Val.sub rs#r2 rs#r1) #CARRY <- (Val.add_carry rs#r2 (Val.notint rs#r1) Vone))) m + | Psubfc64 rd r1 r2 => + Next (nextinstr (rs#rd <- (Val.subl rs#r2 rs#r1) #CARRY <- Vundef)) m | Psubfe rd r1 r2 => Next (nextinstr (rs#rd <- (Val.add (Val.add rs#r2 (Val.notint rs#r1)) rs#CARRY) #CARRY <- (Val.add_carry rs#r2 (Val.notint rs#r1) rs#CARRY))) m | Psubfic rd r1 cst => Next (nextinstr (rs#rd <- (Val.sub (const_low cst) rs#r1) #CARRY <- (Val.add_carry (const_low cst) (Val.notint rs#r1) Vone))) m + | Psubfic64 rd r1 cst => + Next (nextinstr (rs#rd <- (Val.subl (Vlong cst) rs#r1) #CARRY <- Vundef)) m | Pxor rd r1 r2 => Next (nextinstr (rs#rd <- (Val.xor rs#r1 rs#r2))) m + | Pxor64 rd r1 r2 => + Next (nextinstr (rs#rd <- (Val.xorl rs#r1 rs#r2))) m | Pxori rd r1 cst => Next (nextinstr (rs#rd <- (Val.xor rs#r1 (const_low cst)))) m + | Pxori64 rd r1 cst => + Next (nextinstr (rs#rd <- (Val.xorl rs#r1 (Vlong cst)))) m | Pxoris rd r1 cst => Next (nextinstr (rs#rd <- (Val.xor rs#r1 (const_high cst)))) m + | Pxoris64 rd r1 cst => + Next (nextinstr (rs#rd <- (Val.xorl rs#r1 (Vlong (Int64.shl cst (Int64.repr 16)))))) m | Plabel lbl => Next (nextinstr rs) m | Pcfi_rel_offset ofs => @@ -891,6 +1048,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out directly by [Asmgen], so we do not model them. *) | Pbdnz _ | Pcmpb _ _ _ + | Pcntlzd _ _ | Pcntlzw _ _ | Pcreqv _ _ _ | Pcrxor _ _ _ @@ -900,7 +1058,6 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pdcbtst _ _ _ | Pdcbtls _ _ _ | Pdcbz _ _ - | Pextsw _ _ | Peieio | Pfcfid _ _ | Pfctidz _ _ @@ -928,7 +1085,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pmfspr _ _ | Pmtspr _ _ | Prldicl _ _ _ _ - | Prldicr _ _ _ _ + | Prldimi _ _ _ _ | Pstdu _ _ _ | Pstwbrx _ _ _ | Pstwcx_ _ _ _ @@ -1067,7 +1224,7 @@ Proof. { intros. inv H; inv H0; congruence. } assert (B: forall p v1 v2, extcall_arg_pair rs m p v1 -> extcall_arg_pair rs m p v2 -> v1 = v2). - { intros. inv H; inv H0. + { intros. inv H; inv H0. eapply A; eauto. f_equal; eapply A; eauto. } assert (C: forall ll vl1, list_forall2 (extcall_arg_pair rs m) ll vl1 -> @@ -1107,7 +1264,7 @@ Ltac Equalities := (* initial states *) inv H; inv H0. f_equal. congruence. (* final no step *) - inv H. red; intros; red; intros. inv H; rewrite H0 in *; discriminate. + inv H. red; intros; red; intros. inv H; rewrite H0 in *; discriminate. (* final states *) inv H; inv H0. congruence. Qed. diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml index 1c8b9934..343d9b65 100644 --- a/powerpc/AsmToJSON.ml +++ b/powerpc/AsmToJSON.ml @@ -78,6 +78,7 @@ type instruction_arg = | Ireg of ireg | Freg of freg | Constant of constant + | Long of Integers.Int.int | Crbit of crbit | ALabel of positive | Float32 of Floats.float32 @@ -88,6 +89,7 @@ let p_arg oc = function | Ireg ir -> p_ireg oc ir | Freg fr -> p_freg oc fr | Constant c -> p_constant oc c + | Long i -> p_jsingle_object oc "Integer" p_int64 i | Crbit cr -> p_crbit oc cr | ALabel lbl -> p_label oc lbl | Float32 f -> p_float32_constant oc f @@ -101,18 +103,25 @@ let p_instruction oc ic = let sep oc = if !first then first := false else output_string oc ", " in let instruction n args = fprintf oc "\n%t{%a,%a}" sep inst_name n p_args args in let instruction = function - | Padd (ir1,ir2,ir3) -> instruction "Padd" [Ireg ir1; Ireg ir2; Ireg ir3] + | Padd (ir1,ir2,ir3) + | Padd64 (ir1,ir2,ir3) -> instruction "Padd" [Ireg ir1; Ireg ir2; Ireg ir3] | Paddc (ir1,ir2,ir3) -> instruction "Paddc" [Ireg ir1; Ireg ir2; Ireg ir3] | Padde (ir1,ir2,ir3) -> instruction "Padde" [Ireg ir1; Ireg ir2; Ireg ir3] | Paddi (ir1,ir2,c) -> instruction "Paddi" [Ireg ir1; Ireg ir2; Constant c] + | Paddi64 (ir1,ir2,n) -> instruction "Paddi" [Ireg ir1; Ireg ir2; Constant (Cint n)] (* FIXME, ugly, immediates are int64 but always fit into 16bits *) | Paddic (ir1,ir2,c) -> instruction "Paddic" [Ireg ir1; Ireg ir2; Constant c] | Paddis (ir1,ir2,c) -> instruction "Paddis" [Ireg ir1; Ireg ir2; Constant c] - | Paddze (ir1,ir2) -> instruction "Paddze" [Ireg ir1; Ireg ir2] + | Paddis64 (ir1,ir2,n) -> instruction "Paddis" [Ireg ir1; Ireg ir2; Constant (Cint n)] + | Paddze (ir1,ir2) + | Paddze64 (ir1,ir2) -> instruction "Paddze" [Ireg ir1; Ireg ir2] | Pallocframe _ -> assert false (* Should not occur *) - | Pand_ (ir1,ir2,ir3) -> instruction "Pand_" [Ireg ir1; Ireg ir2; Ireg ir3] + | Pand_ (ir1,ir2,ir3) + | Pand_64 (ir1,ir2,ir3) -> instruction "Pand_" [Ireg ir1; Ireg ir2; Ireg ir3] | Pandc (ir1,ir2,ir3) -> instruction "Pandc" [Ireg ir1; Ireg ir2; Ireg ir3] | Pandi_ (ir1,ir2,c) -> instruction "Pandi_" [Ireg ir1; Ireg ir2; Constant c] + | Pandi_64 (ir1,ir2,n) -> instruction "Pandi_" [Ireg ir1; Ireg ir2; Constant (Cint n)] | Pandis_ (ir1,ir2,c) -> instruction "Pandis_" [Ireg ir1; Ireg ir2; Constant c] + | Pandis_64 (ir1,ir2,n) -> instruction "Pandis_" [Ireg ir1; Ireg ir2; Constant (Cint n)] | Pb l -> instruction "Pb" [ALabel l] | Pbctr s -> instruction "Pbctr" [] | Pbctrl s -> instruction "Pbctrl" [] @@ -124,10 +133,15 @@ let p_instruction oc ic = | Pbt (cr,l) -> instruction "Pbt" [Crbit cr; ALabel l] | Pbtbl (i,lb) -> instruction "Pbtbl" ((Ireg i)::(List.map (fun a -> ALabel a) lb)) | Pcmpb (ir1,ir2,ir3) -> instruction "Pcmpb" [Ireg ir1; Ireg ir2; Ireg ir3] + | Pcmpld (ir1,ir2) -> instruction "Pcmpld" [Ireg ir1; Ireg ir2] + | Pcmpldi (ir,n) -> instruction "Pcmpldi" [Ireg ir; Constant (Cint n)] | Pcmplw (ir1,ir2) -> instruction "Pcmplw" [Ireg ir1; Ireg ir2] | Pcmplwi (ir,c) -> instruction "Pcmplwi" [Ireg ir; Constant c] + | Pcmpd (ir1,ir2) -> instruction "Pcmpd" [Ireg ir1; Ireg ir2] + | Pcmpdi (ir,n) -> instruction "Pcmpdi" [Ireg ir; Constant (Cint n)] | Pcmpw (ir1,ir2) -> instruction "Pcmpw" [Ireg ir1; Ireg ir2] | Pcmpwi (ir,c) -> instruction "Pcmpwi" [Ireg ir; Constant c] + | Pcntlzd (ir1,ir2) -> instruction "Pcntlzd" [Ireg ir1; Ireg ir2] | Pcntlzw (ir1,ir2) -> instruction "Pcntlzw" [Ireg ir1; Ireg ir2] | Pcreqv (cr1,cr2,cr3) -> instruction "Pcreqv" [Crbit cr1; Crbit cr2; Crbit cr3] | Pcror (cr1,cr2,cr3) -> instruction "Pcror" [Crbit cr1; Crbit cr2; Crbit cr3] @@ -139,23 +153,28 @@ let p_instruction oc ic = | Pdcbtls (n,ir1,ir2) -> instruction "Pdcbtls" [Constant (Cint n); Ireg ir1; Ireg ir2] | Pdcbz (ir1,ir2) -> instruction "Pdcbz" [Ireg ir1; Ireg ir2] | Pdivw (ir1,ir2,ir3) -> instruction "Pdivw" [Ireg ir1; Ireg ir2; Ireg ir3] + | Pdivd (ir1,ir2,ir3) -> instruction "Pdivd" [Ireg ir1; Ireg ir2; Ireg ir3] | Pdivwu (ir1,ir2,ir3) -> instruction "Pdivwu" [Ireg ir1; Ireg ir2; Ireg ir3] + | Pdivdu (ir1,ir2,ir3) -> instruction "Pdivdu" [Ireg ir1; Ireg ir2; Ireg ir3] | Peieio -> instruction "Peieio" [] | Peqv (ir1,ir2,ir3) -> instruction "Peqv" [Ireg ir1; Ireg ir2; Ireg ir3] | Pextsb (ir1,ir2) -> instruction "Pextsb" [Ireg ir1; Ireg ir2] | Pextsh (ir1,ir2) -> instruction "Pextsh" [Ireg ir1; Ireg ir2] | Pextsw (ir1,ir2) -> instruction "Pextsw" [Ireg ir1; Ireg ir2] - | Pfreeframe (c,i) -> assert false (* Should not occur *) + | Pextzw (ir1,ir2) -> assert false (* Should not occur *) + | Pfreeframe (c,i) -> () (* Should not occur *) | Pfabs (fr1,fr2) | Pfabss (fr1,fr2) -> instruction "Pfabs" [Freg fr1; Freg fr2] | Pfadd (fr1,fr2,fr3) -> instruction "Pfadd" [Freg fr1; Freg fr2; Freg fr3] | Pfadds (fr1,fr2,fr3) -> instruction "Pfadds" [Freg fr1; Freg fr2; Freg fr3] | Pfcmpu (fr1,fr2) -> instruction "Pfcmpu" [Freg fr1; Freg fr2] - | Pfcfi (ir,fr) -> assert false (* Should not occur *) + | Pfcfi (ir,fr) + | Pfcfl (ir,fr) -> assert false (* Should not occur *) | Pfcfid (fr1,fr2) -> instruction "Pfcfid" [Freg fr1; Freg fr2] | Pfcfiu _ (* Should not occur *) | Pfcti _ (* Should not occur *) - | Pfctiu _ -> assert false (* Should not occur *) + | Pfctiu _ (* Should not occur *) + | Pfctid _ -> assert false (* Should not occur *) | Pfctidz (fr1,fr2) -> instruction "Pfctidz" [Freg fr1; Freg fr2] | Pfctiw (fr1,fr2) -> instruction "Pfctiw" [Freg fr1; Freg fr2] | Pfctiwz (fr1,fr2) -> instruction "Pfctiwz" [Freg fr1; Freg fr2] @@ -186,6 +205,10 @@ let p_instruction oc ic = | Plwsync -> instruction "Plwsync" [] | Plbz (ir1,c,ir2) -> instruction "Plbz" [Ireg ir1; Constant c; Ireg ir2] | Plbzx (ir1,ir2,ir3) -> instruction "Plbzx" [Ireg ir1; Ireg ir2; Ireg ir3] + | Pld (ir1,c,ir2) + | Pld_a (ir1,c,ir2) -> instruction "Pld" [Ireg ir1; Constant c; Ireg ir2] + | Pldx (ir1,ir2,ir3) + | Pldx_a (ir1,ir2,ir3) -> instruction "Pldx" [Ireg ir1; Ireg ir2; Ireg ir3] | Plfd (fr,c,ir) | Plfd_a (fr,c,ir) -> instruction "Plfd" [Freg fr; Constant c; Ireg ir] | Plfdx (fr,ir1,ir2) @@ -197,6 +220,10 @@ let p_instruction oc ic = | Plhbrx (ir1,ir2,ir3) -> instruction "Plhbrx" [Ireg ir1; Ireg ir2; Ireg ir3] | Plhz (ir1,c,ir2) -> instruction "Plhz" [Ireg ir1; Constant c; Ireg ir2] | Plhzx (ir1,ir2,ir3) -> instruction "Plhzx" [Ireg ir1; Ireg ir2; Ireg ir3] + | Pldi (ir,c) -> instruction "Pldi" [Ireg ir; Long c] (* FIXME Cint is too small, we need Clong *) + | Plmake _ (* Should not occur *) + | Pllo _ (* Should not occur *) + | Plhi _ -> assert false (* Should not occur *) | Plfi (fr,fc) -> instruction "Plfi" [Freg fr; Float64 fc] | Plfis (fr,fc) -> instruction "Plfis" [Freg fr; Float32 fc] | Plwz (ir1,c,ir2) @@ -215,26 +242,42 @@ let p_instruction oc ic = | Pmtlr ir -> instruction "Pmtlr" [Ireg ir] | Pmfspr(ir, n) -> instruction "Pmfspr" [Ireg ir; Constant (Cint n)] | Pmtspr(n, ir) -> instruction "Pmtspr" [Constant (Cint n); Ireg ir] + | Pmulhd (ir1,ir2,ir3) -> instruction "Pmulhd" [Ireg ir1; Ireg ir2; Ireg ir3] + | Pmulhdu (ir1,ir2,ir3) -> instruction "Pmulhdu" [Ireg ir1; Ireg ir2; Ireg ir3] + | Pmulld (ir1,ir2,ir3) -> instruction "Pmulld" [Ireg ir1; Ireg ir2; Ireg ir3] | Pmulli (ir1,ir2,c) -> instruction "Pmulli" [Ireg ir1; Ireg ir2; Constant c] | Pmullw (ir1,ir2,ir3) -> instruction "Pmullw" [Ireg ir1; Ireg ir2; Ireg ir3] | Pmulhw (ir1,ir2,ir3) -> instruction "Pmulhw" [Ireg ir1; Ireg ir2; Ireg ir3] | Pmulhwu (ir1,ir2,ir3) -> instruction "Pmulhwu" [Ireg ir1; Ireg ir2; Ireg ir3] | Pnand (ir1,ir2,ir3) -> instruction "Pnand" [Ireg ir1; Ireg ir2; Ireg ir3] - | Pnor (ir1,ir2,ir3) -> instruction "Pnor" [Ireg ir1; Ireg ir2; Ireg ir3] - | Por (ir1,ir2,ir3) -> instruction "Por" [Ireg ir1; Ireg ir2; Ireg ir3] + | Pnor (ir1,ir2,ir3) + | Pnor64 (ir1,ir2,ir3) -> instruction "Pnor" [Ireg ir1; Ireg ir2; Ireg ir3] + | Por (ir1,ir2,ir3) + | Por64 (ir1,ir2,ir3) -> instruction "Por" [Ireg ir1; Ireg ir2; Ireg ir3] | Porc (ir1,ir2,ir3) -> instruction "Porc" [Ireg ir1; Ireg ir2; Ireg ir3] | Pori (ir1,ir2,c) -> instruction "Pori" [Ireg ir1; Ireg ir2; Constant c] + | Pori64 (ir1,ir2,n) -> instruction "Pori" [Ireg ir1; Ireg ir2; Constant (Cint n)] | Poris (ir1,ir2,c) -> instruction "Poris" [Ireg ir1; Ireg ir2; Constant c] + | Poris64 (ir1,ir2,n) -> instruction "Poris" [Ireg ir1; Ireg ir2; Constant (Cint n)] | Prldicl (ir1,ir2,ic1,ic2) -> instruction "Prldicl" [Ireg ir1; Ireg ir2; Constant (Cint ic1); Constant (Cint ic2)] - | Prldicr (ir1,ir2,ic1,ic2) -> instruction "Prldicr" [Ireg ir1; Ireg ir2; Constant (Cint ic1); Constant (Cint ic2)] + | Prldinm (ir1,ir2,ic1,ic2) -> instruction "Prldinm" [Ireg ir1; Ireg ir2; Constant (Cint ic1); Constant (Cint ic2)] + | Prldimi (ir1,ir2,ic1,ic2) ->instruction "Prldimi" [Ireg ir1; Ireg ir2; Constant (Cint ic1); Constant (Cint ic2)] | Prlwinm (ir1,ir2,ic1,ic2) -> instruction "Prlwinm" [Ireg ir1; Ireg ir2; Constant (Cint ic1); Constant (Cint ic2)] | Prlwimi (ir1,ir2,ic1,ic2) ->instruction "Prlwimi" [Ireg ir1; Ireg ir2; Constant (Cint ic1); Constant (Cint ic2)] + | Psld (ir1,ir2,ir3) -> instruction "Psld" [Ireg ir1; Ireg ir2; Ireg ir3] | Pslw (ir1,ir2,ir3) -> instruction "Pslw" [Ireg ir1; Ireg ir2; Ireg ir3] + | Psrad (ir1,ir2,ir3) -> instruction "Psrad" [Ireg ir1; Ireg ir2; Ireg ir3] + | Psradi (ir1,ir2,ic) -> instruction "Psradi" [Ireg ir1; Ireg ir2; Constant (Cint ic)] | Psraw (ir1,ir2,ir3) -> instruction "Psraw" [Ireg ir1; Ireg ir2; Ireg ir3] | Psrawi (ir1,ir2,ic) -> instruction "Psrawi" [Ireg ir1; Ireg ir2; Constant (Cint ic)] + | Psrd (ir1,ir2,ir3) -> instruction "Psrd" [Ireg ir1; Ireg ir2; Ireg ir3] | Psrw (ir1,ir2,ir3) -> instruction "Psrw" [Ireg ir1; Ireg ir2; Ireg ir3] | Pstb (ir1,c,ir2) -> instruction "Pstb" [Ireg ir1; Constant c; Ireg ir2] | Pstbx (ir1,ir2,ir3) -> instruction "Pstbx" [Ireg ir1; Ireg ir2; Ireg ir3] + | Pstd (ir1,c,ir2) + | Pstd_a (ir1,c,ir2) -> instruction "Pstd" [Ireg ir1; Constant c; Ireg ir2] + | Pstdx (ir1,ir2,ir3) + | Pstdx_a (ir1,ir2,ir3) -> instruction "Pstdx" [Ireg ir1; Ireg ir2; Ireg ir3] | Pstdu (ir1,c,ir2) -> instruction "Pstdu" [Ireg ir1; Constant c; Ireg ir2] | Pstfd (fr,c,ir) | Pstfd_a (fr,c,ir) -> instruction "Pstfd" [Freg fr; Constant c; Ireg ir] @@ -254,15 +297,20 @@ let p_instruction oc ic = | Pstwux (ir1,ir2,ir3) -> instruction "Pstwux" [Ireg ir1; Ireg ir2; Ireg ir3] | Pstwbrx (ir1,ir2,ir3) -> instruction "Pstwbrx" [Ireg ir1; Ireg ir2; Ireg ir3] | Pstwcx_ (ir1,ir2,ir3) -> instruction "Pstwcx_" [Ireg ir1; Ireg ir2; Ireg ir3] - | Psubfc (ir1,ir2,ir3) -> instruction "Psubfc" [Ireg ir1; Ireg ir2; Ireg ir3] + | Psubfc (ir1,ir2,ir3) + | Psubfc64 (ir1,ir2,ir3) -> instruction "Psubfc" [Ireg ir1; Ireg ir2; Ireg ir3] | Psubfe (ir1,ir2,ir3) -> instruction "Psubfe" [Ireg ir1; Ireg ir2; Ireg ir3] | Psubfze (ir1,ir2) -> instruction "Psubfze" [Ireg ir1; Ireg ir2] | Psubfic (ir1,ir2,c) -> instruction "Psubfic" [Ireg ir1; Ireg ir2; Constant c] + | Psubfic64 (ir1,ir2,n) -> instruction "Psubfic" [Ireg ir1; Ireg ir2; Constant (Cint n)] | Psync -> instruction "Psync" [] | Ptrap -> instruction "Ptrap" [] - | Pxor (ir1,ir2,ir3) -> instruction "Pxor" [Ireg ir1; Ireg ir2; Ireg ir3] - | Pxori (ir1,ir2,c) ->instruction "Pxori" [Ireg ir1; Ireg ir2; Constant c] + | Pxor (ir1,ir2,ir3) + | Pxor64 (ir1,ir2,ir3) -> instruction "Pxor" [Ireg ir1; Ireg ir2; Ireg ir3] + | Pxori (ir1,ir2,c) -> instruction "Pxori" [Ireg ir1; Ireg ir2; Constant c] + | Pxori64 (ir1,ir2,n) -> instruction "Pxori" [Ireg ir1; Ireg ir2; Constant (Cint n)] | Pxoris (ir1,ir2,c) -> instruction "Pxoris" [Ireg ir1; Ireg ir2; Constant c] + | Pxoris64 (ir1,ir2,n) -> instruction "Pxoris" [Ireg ir1; Ireg ir2; Constant (Cint n)] | Plabel l -> instruction "Plabel" [ALabel l] | Pbuiltin (ef,_,_) -> begin match ef with @@ -271,7 +319,7 @@ let p_instruction oc ic = | _ -> () end | Pcfi_adjust _ (* Only debug relevant *) - | Pcfi_rel_offset _ -> () (* Only debug relevant *) in + | Pcfi_rel_offset _ -> () in (* Only debug relevant *) List.iter instruction ic let p_storage oc static = diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index a27eeeb7..da229d0b 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -43,14 +43,19 @@ let _m1 = coqint_of_camlint (-1l) let _m4 = coqint_of_camlint (-4l) let _m8 = coqint_of_camlint (-8l) +let _0L = Integers.Int64.zero +let _32L = coqint_of_camlint64 32L +let _64L = coqint_of_camlint64 64L +let _m1L = coqint_of_camlint64 (-1L) +let upper32 = coqint_of_camlint64 0xFFFF_FFFF_0000_0000L +let lower32 = coqint_of_camlint64 0x0000_0000_FFFF_FFFFL + let emit_loadimm r n = List.iter emit (Asmgen.loadimm r n []) let emit_addimm rd rs n = List.iter emit (Asmgen.addimm rd rs n []) - - (* Handling of annotations *) let expand_annot_val txt targ args res = @@ -72,6 +77,8 @@ let expand_annot_val txt targ args res = So, use 64-bit accesses only if alignment >= 4. Note that lfd and stfd cannot trap on ill-formed floats. *) + + let offset_in_range ofs = Int.eq (Asmgen.high_s ofs) _0 @@ -184,6 +191,8 @@ let rec expand_builtin_vload_common chunk base offset res = emit (Plfs(res, offset, base)) | (Mfloat64 | Many64), BR(FR res) -> emit (Plfd(res, offset, base)) + | (Mint64 | Many64), BR(IR res) -> + emit (Pld(res, offset, base)) | Mint64, BR_splitlong(BR(IR hi), BR(IR lo)) -> begin match offset_constant offset _4 with | Some offset' -> @@ -243,6 +252,8 @@ let expand_builtin_vstore_common chunk base offset src = emit (Pstfs(src, offset, base)) | (Mfloat64 | Many64), BA(FR src) -> emit (Pstfd(src, offset, base)) + | (Mint64 | Many64), BA(IR src) -> + emit (Pstd(src, offset, base)) | Mint64, BA_splitlong(BA(IR hi), BA(IR lo)) -> begin match offset_constant offset _4 with | Some offset' -> @@ -361,6 +372,8 @@ let expand_builtin_inline name args res = emit (Pmulhwu(res, a1, a2)) | ("__builtin_clz" | "__builtin_clzl"), [BA(IR a1)], BR(IR res) -> emit (Pcntlzw(res, a1)) + | "__builtin_clzll", [BA(IR a1)], BR(IR res) -> + emit (Pcntlzd(res, a1)) | "__builtin_clzll", [BA_splitlong(BA(IR ah), BA(IR al))], BR(IR res) -> let lbl = new_label () in emit (Pcntlzw(GPR0, al)); @@ -376,6 +389,11 @@ let expand_builtin_inline name args res = emit (Pandc(res, GPR0, a1)); (* res := tmp & ~(x) *) emit (Pcntlzw(res, res)); (* res := #leading zeros *) emit (Psubfic(res, res, Cint _32)) (* res := 32 - #leading zeros *) + | "__builtin_ctzll", [BA(IR a1)], BR(IR res) -> + emit (Paddi64(GPR0, a1, _m1L)); (* tmp := x-1 *) + emit (Pandc(res, GPR0, a1)); (* res := tmp & ~(x) *) + emit (Pcntlzd(res, res)); (* res := #leading zeros *) + emit (Psubfic64(res, res, _64L)) (* res := 64 - #leading zeros *) | "__builtin_ctzll", [BA_splitlong(BA(IR ah), BA(IR al))], BR(IR res) -> let lbl1 = new_label () in let lbl2 = new_label () in @@ -530,22 +548,17 @@ let expand_builtin_inline name args res = | "__builtin_set_spr", _, _ -> raise (Error "the first argument of __builtin_set_spr must be a constant") (* Special registers in 32bit hybrid mode *) - | "__builtin_get_spr64", [BA_int n], BR_splitlong(BR(IR rh), BR(IR rl)) -> - if Archi.ppc64 then begin - emit (Pmfspr(rl, n)); - emit (Prldicl(rh, rl, _32, _32)); - emit (Prldicl(rl, rl, _0, _32)) - end else + | "__builtin_get_spr64", [BA_int n], BR(IR r) -> + if Archi.ppc64 then + emit (Pmfspr(r, n)) + else raise (Error "__builtin_get_spr64 is only supported for PPC64 targets") | "__builtin_get_spr64", _, _ -> raise (Error "the argument of __builtin_get_spr64 must be a constant") - | "__builtin_set_spr64", [BA_int n; BA_splitlong(BA(IR ah), BA(IR al))], _ -> - if Archi.ppc64 then begin - emit (Prldicr(GPR10, ah, _32, _31)); - emit (Prldicl(al, al, _0, _32)); - emit (Por(GPR10, GPR10, al)); - emit (Pmtspr(n, GPR10)) - end else + | "__builtin_set_spr64", [BA_int n; BA(IR a)], _ -> + if Archi.ppc64 then + emit (Pmtspr(n, a)) + else raise (Error "__builtin_set_spr64 is only supported for PPC64 targets") | "__builtin_set_spr64", _, _ -> raise (Error "the first argument of __builtin_set_spr64 must be a constant") @@ -692,6 +705,8 @@ let expand_instruction instr = | Pbctr sg | Pbctrl sg | Pbl(_, sg) | Pbs(_, sg) -> set_cr6 sg; emit instr + | Pextzw(r1, r2) -> + emit (Prldinm(r1, r2, _0L, lower32)) | Pfreeframe(sz, ofs) -> let variadic = is_current_function_variadic () in let sz = camlint_of_coqint sz in @@ -709,6 +724,14 @@ let expand_instruction instr = emit (Pfcfid(r1, r1)); emit (Paddi(GPR1, GPR1, Cint _8)); emit (Pcfi_adjust _m8) + | Pfcfl(r1, r2) -> + assert (Archi.ppc64); + emit (Pstdu(r2, Cint _m8, GPR1)); + emit (Pcfi_adjust _8); + emit (Plfd(r1, Cint _0, GPR1)); + emit (Pfcfid(r1, r1)); + emit (Paddi(GPR1, GPR1, Cint _8)); + emit (Pcfi_adjust _m8) | Pfcfiu(r1, r2) -> assert (Archi.ppc64); emit (Prldicl(GPR0, r2, _0, _32)); @@ -733,6 +756,14 @@ let expand_instruction instr = emit (Plwz(r1, Cint _4, GPR1)); emit (Paddi(GPR1, GPR1, Cint _8)); emit (Pcfi_adjust _m8) + | Pfctid(r1, r2) -> + assert (Archi.ppc64); + emit (Pfctidz(FPR13, r2)); + emit (Pstfdu(FPR13, Cint _m8, GPR1)); + emit (Pcfi_adjust _8); + emit (Pld(r1, Cint _0, GPR1)); + emit (Paddi(GPR1, GPR1, Cint _8)); + emit (Pcfi_adjust _m8) | Pfmake(rd, r1, r2) -> emit (Pstwu(r1, Cint _m8, GPR1)); emit (Pcfi_adjust _8); @@ -742,6 +773,20 @@ let expand_instruction instr = emit (Pcfi_adjust _m8); | Pfxdp(r1, r2) -> if r1 <> r2 then emit(Pfmr(r1, r2)) + | Plmake(r1, rhi, rlo) -> + if r1 = rlo then + emit (Prldimi(r1, rhi, _32L, upper32)) + else if r1 = rhi then begin + emit (Prldinm(r1, rhi, _32L, upper32)); + emit (Prldimi(r1, rlo, _0L, lower32)) + end else begin + emit (Pmr(r1, rlo)); + emit (Prldimi(r1, rhi, _32L, upper32)) + end + | Pllo r1 -> + () (* no computational content *) + | Plhi(r1, r2) -> + emit (Prldinm(r1, r2, _32L, lower32)) | Pmfcrbit(r1, bit) -> emit (Pmfcr r1); emit (Prlwinm(r1, r1, Z.of_uint (1 + num_crbit bit), _1)) diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v index 1c97c5b0..8c296f0a 100644 --- a/powerpc/Asmgen.v +++ b/powerpc/Asmgen.v @@ -120,6 +120,56 @@ Definition rolm (r1 r2: ireg) (amount mask: int) (k: code) := else Prlwinm r1 r2 amount Int.mone :: andimm_base r1 r1 mask k. +(** Smart constructors for 64-bit integer constants *) + +Definition low64_u (n: int64) := Int64.zero_ext 16 n. +Definition low64_s (n: int64) := Int64.sign_ext 16 n. + +Definition loadimm64 (r: ireg) (n: int64) (k: code) := + let lo_u := low64_u n in + let lo_s := low64_s n in + let hi_s := Int64.sign_ext 16 (Int64.shr n (Int64.repr 16)) in + if Int64.eq n lo_s then + Paddi64 r GPR0 n :: k + else if Int64.eq n (Int64.or (Int64.shl hi_s (Int64.repr 16)) lo_u) then + Paddis64 r GPR0 hi_s :: Pori64 r r lo_u :: k + else + Pldi r n :: k. + +Definition opimm64 (insn2: ireg -> ireg -> ireg -> instruction) + (insn1: ireg -> ireg -> int64 -> instruction) + (r1 r2: ireg) (n: int64) (ok: bool) (k: code) := + if ok then + insn1 r1 r2 n :: k + else if ireg_eq r2 GPR12 then + Pmr GPR0 GPR12 :: loadimm64 GPR12 n (insn2 r1 GPR0 GPR12 :: k) + else + loadimm64 GPR0 n (insn2 r1 r2 GPR0 :: k). + +Definition addimm64 (r1 r2: ireg) (n: int64) (k : code) := + opimm64 Padd64 Paddi64 r1 r2 n (Int64.eq n (low64_s n)) k. + +Definition orimm64 (r1 r2: ireg) (n: int64) (k : code) := + opimm64 Por64 Pori64 r1 r2 n (Int64.eq n (low64_u n)) k. + +Definition xorimm64 (r1 r2: ireg) (n: int64) (k : code) := + opimm64 Pxor64 Pxori64 r1 r2 n (Int64.eq n (low64_u n)) k. + +Definition andimm64_base (r1 r2: ireg) (n: int64) (k : code) := + opimm64 Pand_64 Pandi_64 r1 r2 n (Int64.eq n (low64_u n)) k. + +Definition andimm64 (r1 r2: ireg) (n: int64) (k : code) := + if is_rldl_mask n || is_rldr_mask n then + Prldinm r1 r2 Int.zero n :: k + else + andimm64_base r1 r2 n k. + +Definition rolm64 (r1 r2: ireg) (amount: int) (mask: int64) (k: code) := + if is_rldl_mask mask || is_rldr_mask mask || is_rldl_mask (Int64.shru' mask amount) then + Prldinm r1 r2 amount mask :: k + else + Prldinm r1 r2 amount Int64.mone :: andimm64_base r1 r1 mask k. + (** Accessing slots in the stack frame. *) Definition accessind {A: Type} @@ -136,7 +186,9 @@ Definition loadind (base: ireg) (ofs: ptrofs) (ty: typ) (dst: mreg) (k: code) := | Tint, IR r => OK(accessind Plwz Plwzx base ofs r k) | Tany32, IR r => OK(accessind Plwz_a Plwzx_a base ofs r k) | Tsingle, FR r => OK(accessind Plfs Plfsx base ofs r k) + | Tlong, IR r => OK(accessind Pld Pldx base ofs r k) | Tfloat, FR r => OK(accessind Plfd Plfdx base ofs r k) + | Tany64, IR r => OK(accessind Pld_a Pldx_a base ofs r k) | Tany64, FR r => OK(accessind Plfd_a Plfdx_a base ofs r k) | _, _ => Error (msg "Asmgen.loadind") end. @@ -146,7 +198,9 @@ Definition storeind (src: mreg) (base: ireg) (ofs: ptrofs) (ty: typ) (k: code) : | Tint, IR r => OK(accessind Pstw Pstwx base ofs r k) | Tany32, IR r => OK(accessind Pstw_a Pstwx_a base ofs r k) | Tsingle, FR r => OK(accessind Pstfs Pstfsx base ofs r k) + | Tlong, IR r => OK(accessind Pstd Pstdx base ofs r k) | Tfloat, FR r => OK(accessind Pstfd Pstfdx base ofs r k) + | Tany64, IR r => OK(accessind Pstd_a Pstdx_a base ofs r k) | Tany64, FR r => OK(accessind Pstfd_a Pstfdx_a base ofs r k) | _, _ => Error (msg "Asmgen.storeind") end. @@ -199,6 +253,26 @@ Definition transl_cond do r1 <- ireg_of a1; OK (andimm_base GPR0 r1 n k) | Cmasknotzero n, a1 :: nil => do r1 <- ireg_of a1; OK (andimm_base GPR0 r1 n k) + | Ccompl c, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; OK (Pcmpd r1 r2 :: k) + | Ccomplu c, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; OK (Pcmpld r1 r2 :: k) + | Ccomplimm c n, a1 :: nil => + do r1 <- ireg_of a1; + if Int64.eq n (low64_s n) then + OK (Pcmpdi r1 n :: k) + else if ireg_eq r1 GPR12 then + OK (Pmr GPR0 GPR12 :: loadimm64 GPR12 n (Pcmpd GPR0 GPR12 :: k)) + else + OK (loadimm64 GPR0 n (Pcmpd r1 GPR0 :: k)) + | Ccompluimm c n, a1 :: nil => + do r1 <- ireg_of a1; + if Int64.eq n (low64_u n) then + OK (Pcmpldi r1 n :: k) + else if ireg_eq r1 GPR12 then + OK (Pmr GPR0 GPR12 :: loadimm64 GPR12 n (Pcmpld GPR0 GPR12 :: k)) + else + OK (loadimm64 GPR0 n (Pcmpld r1 GPR0 :: k)) | _, _ => Error(msg "Asmgen.transl_cond") end. @@ -238,6 +312,10 @@ Definition crbit_for_cond (cond: condition) := | Cnotcompf cmp => let p := crbit_for_fcmp cmp in (fst p, negb (snd p)) | Cmaskzero n => (CRbit_2, true) | Cmasknotzero n => (CRbit_2, false) + | Ccompl cmp => crbit_for_icmp cmp + | Ccomplu cmp => crbit_for_icmp cmp + | Ccomplimm cmp n => crbit_for_icmp cmp + | Ccompluimm cmp n => crbit_for_icmp cmp end. (** Recognition of comparisons [>= 0] and [< 0]. *) @@ -509,8 +587,96 @@ Definition transl_op | Ofloatofwords, a1 :: a2 :: nil => do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- freg_of res; OK (Pfmake r r1 r2 :: k) + | Omakelong, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res; OK (Plmake r r1 r2 :: k) + | Olowlong, a1 :: nil => + assertion (mreg_eq a1 res); + do r <- ireg_of res; OK (Pllo r :: k) + | Ohighlong, a1 :: nil => + do r1 <- ireg_of a1; do r <- ireg_of res; OK (Plhi r r1 :: k) | Ocmp cmp, _ => transl_cond_op cmp args res k +(*c PPC64 operations *) + | Olongconst n, nil => + do r <- ireg_of res; OK (loadimm64 r n k) + | Ocast32signed, a1 :: nil => + do r1 <- ireg_of a1; do r <- ireg_of res; + OK (Pextsw r r1 :: k) + | Ocast32unsigned, a1 :: nil => + do r1 <- ireg_of a1; do r <- ireg_of res; + OK (Pextzw r r1 :: k) + | Oaddl, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res; + OK (Padd64 r r1 r2 :: k) + | Oaddlimm n, a1 :: nil => + do r1 <- ireg_of a1; do r <- ireg_of res; + OK (addimm64 r r1 n k) + | Osubl, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res; + OK (Psubfc64 r r2 r1 :: k) + | Onegl, a1 :: nil => + do r1 <- ireg_of a1; do r <- ireg_of res; + OK (Psubfic64 r r1 Int64.zero :: k) + | Omull, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res; + OK (Pmulld r r1 r2 :: k) + | Omullhs, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res; + OK (Pmulhd r r1 r2 :: k) + | Omullhu, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res; + OK (Pmulhdu r r1 r2 :: k) + | Odivl, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res; + OK (Pdivd r r1 r2 :: k) + | Odivlu, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res; + OK (Pdivdu r r1 r2 :: k) + | Oandl, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res; + OK (Pand_64 r r1 r2 :: k) + | Oandlimm n, a1 :: nil => + do r1 <- ireg_of a1; do r <- ireg_of res; + OK (andimm64 r r1 n k) + | Oorl, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res; + OK (Por64 r r1 r2 :: k) + | Oorlimm n, a1 :: nil => + do r1 <- ireg_of a1; do r <- ireg_of res; + OK (orimm64 r r1 n k) + | Oxorl, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res; + OK (Pxor64 r r1 r2 :: k) + | Oxorlimm n, a1 :: nil => + do r1 <- ireg_of a1; do r <- ireg_of res; + OK (xorimm64 r r1 n k) + | Onotl, a1 :: nil => + do r1 <- ireg_of a1; do r <- ireg_of res; + OK (Pnor64 r r1 r1 :: k) + | Oshll, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res; + OK (Psld r r1 r2 :: k) + | Oshrl, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res; + OK (Psrad r r1 r2 :: k) + | Oshrlimm n, a1 :: nil => + do r1 <- ireg_of a1; do r <- ireg_of res; + OK (Psradi r r1 n :: k) + | Oshrlu, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res; + OK (Psrd r r1 r2 :: k) + | Orolml amount mask, a1 :: nil => + do r1 <- ireg_of a1; do r <- ireg_of res; + OK (rolm64 r r1 amount mask k) + | Oshrxlimm n, a1 :: nil => + do r1 <- ireg_of a1; do r <- ireg_of res; + OK (Psradi r r1 n :: Paddze64 r r :: k) + | Olongoffloat, a1 :: nil => + do r1 <- freg_of a1; do r <- ireg_of res; + OK (Pfctid r r1 :: k) + | Ofloatoflong, a1 :: nil => + do r1 <- ireg_of a1; do r <- freg_of res; + OK (Pfcfl r r1 :: k) | _, _ => Error(msg "Asmgen.transl_op") end. @@ -588,6 +754,9 @@ Definition transl_load (chunk: memory_chunk) (addr: addressing) | Mint32 => do r <- ireg_of dst; transl_memory_access (Plwz r) (Plwzx r) addr args GPR12 k + | Mint64 => + do r <- ireg_of dst; + transl_memory_access (Pld r) (Pldx r) addr args GPR12 k | Mfloat32 => do r <- freg_of dst; transl_memory_access (Plfs r) (Plfsx r) addr args GPR12 k @@ -611,6 +780,9 @@ Definition transl_store (chunk: memory_chunk) (addr: addressing) | Mint32 => do r <- ireg_of src; transl_memory_access (Pstw r) (Pstwx r) addr args temp k + | Mint64 => + do r <- ireg_of src; + transl_memory_access (Pstd r) (Pstdx r) addr args temp k | Mfloat32 => do r <- freg_of src; transl_memory_access (Pstfs r) (Pstfsx r) addr args temp k diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v index 0610b242..bf75d2e0 100644 --- a/powerpc/Asmgenproof.v +++ b/powerpc/Asmgenproof.v @@ -179,6 +179,14 @@ Proof. Qed. Hint Resolve rolm_label: labels. +Remark loadimm64_label: + forall r n k, tail_nolabel k (loadimm64 r n k). +Proof. + unfold loadimm64; intros. + destruct Int64.eq. TailNoLabel. destruct Int64.eq; TailNoLabel. +Qed. +Hint Resolve loadimm64_label: labels. + Remark loadind_label: forall base ofs ty dst k c, loadind base ofs ty dst k = OK c -> tail_nolabel k c. @@ -232,12 +240,27 @@ Remark transl_op_label: Proof. Opaque Int.eq. unfold transl_op; intros; destruct op; TailNoLabel. - destruct (preg_of r); try discriminate; destruct (preg_of m); inv H; TailNoLabel. - destruct (symbol_is_small_data i i0). TailNoLabel. destruct (symbol_is_rel_data i i0); TailNoLabel. - destruct (symbol_is_small_data i i0). TailNoLabel. destruct (symbol_is_rel_data i i0); TailNoLabel. - destruct (Int.eq (high_s i) Int.zero); TailNoLabel; eapply tail_nolabel_trans; TailNoLabel. - destruct (Int.eq (high_s i) Int.zero); TailNoLabel; eapply tail_nolabel_trans; TailNoLabel. - eapply transl_cond_op_label; eauto. +- destruct (preg_of r); try discriminate; destruct (preg_of m); inv H; TailNoLabel. +- destruct (symbol_is_small_data i i0). TailNoLabel. destruct (symbol_is_rel_data i i0); TailNoLabel. +- destruct (symbol_is_small_data i i0). TailNoLabel. destruct (symbol_is_rel_data i i0); TailNoLabel. +- destruct (Int.eq (high_s i) Int.zero); TailNoLabel; eapply tail_nolabel_trans; TailNoLabel. +- destruct (Int.eq (high_s i) Int.zero); TailNoLabel; eapply tail_nolabel_trans; TailNoLabel. +- unfold addimm64, opimm64. destruct Int64.eq. TailNoLabel. + destruct ireg_eq; [apply tail_nolabel_cons; unfold nolabel;auto|]; eapply tail_nolabel_trans; TailNoLabel. +- unfold andimm64, andimm64_base, opimm64. + destruct (is_rldl_mask i || is_rldr_mask i). TailNoLabel. + destruct Int64.eq. TailNoLabel. + destruct ireg_eq; [apply tail_nolabel_cons; unfold nolabel;auto|]; eapply tail_nolabel_trans; TailNoLabel. +- unfold orimm64, opimm64. destruct Int64.eq. TailNoLabel. + destruct ireg_eq; [apply tail_nolabel_cons; unfold nolabel;auto|]; eapply tail_nolabel_trans; TailNoLabel. +- unfold xorimm64, opimm64. destruct Int64.eq. TailNoLabel. + destruct ireg_eq; [apply tail_nolabel_cons; unfold nolabel;auto|]; eapply tail_nolabel_trans; TailNoLabel. +- unfold rolm64, andimm64_base, opimm64. + destruct (is_rldl_mask i0 || is_rldr_mask i0 || is_rldl_mask (Int64.shru' i0 i)). TailNoLabel. + apply tail_nolabel_cons; unfold nolabel; auto. + destruct Int64.eq. TailNoLabel. + destruct ireg_eq; [apply tail_nolabel_cons; unfold nolabel;auto|]; eapply tail_nolabel_trans; TailNoLabel. +- eapply transl_cond_op_label; eauto. Qed. Remark transl_memory_access_label: @@ -760,12 +783,12 @@ Opaque loadind. destruct (snd (crbit_for_cond cond)). (* Pbt, taken *) econstructor; econstructor; econstructor; split. eexact A. - split. eapply agree_exten; eauto with asmgen. + split. eapply agree_undef_regs; eauto with asmgen. split. simpl. rewrite B. reflexivity. auto with asmgen. (* Pbf, taken *) econstructor; econstructor; econstructor; split. eexact A. - split. eapply agree_exten; eauto with asmgen. + split. eapply agree_undef_regs; eauto with asmgen. split. simpl. rewrite B. reflexivity. auto with asmgen. @@ -779,7 +802,7 @@ Opaque loadind. destruct (snd (crbit_for_cond cond)). apply exec_straight_one. simpl. rewrite B. reflexivity. auto. apply exec_straight_one. simpl. rewrite B. reflexivity. auto. - split. eapply agree_exten; eauto with asmgen. + split. eapply agree_undef_regs; eauto with asmgen. intros; Simpl. split. simpl. congruence. Simpl. @@ -865,7 +888,7 @@ Local Transparent destroyed_by_jumptable. apply exec_straight_two with rs4 m3'. simpl. unfold store1. rewrite gpr_or_zero_not_zero. change (rs3 GPR1) with sp. change (rs3 GPR0) with (rs0 LR). - simpl const_low. rewrite ATLR. erewrite storev_offset_ptr by eexact P. auto. congruence. + simpl const_low. rewrite ATLR. erewrite storev_offset_ptr by eexact P. auto. congruence. auto. auto. auto. left; exists (State rs5 m3'); split. eapply exec_straight_steps_1; eauto. omega. constructor. diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v index 9fee580c..e5736277 100644 --- a/powerpc/Asmgenproof1.v +++ b/powerpc/Asmgenproof1.v @@ -167,6 +167,18 @@ Proof. Qed. Hint Resolve gpr_or_zero_not_zero gpr_or_zero_zero: asmgen. +Lemma gpr_or_zero_l_not_zero: + forall rs r, r <> GPR0 -> gpr_or_zero_l rs r = rs#r. +Proof. + intros. unfold gpr_or_zero_l. case (ireg_eq r GPR0); tauto. +Qed. +Lemma gpr_or_zero_l_zero: + forall rs, gpr_or_zero_l rs GPR0 = Vlong Int64.zero. +Proof. + intros. reflexivity. +Qed. +Hint Resolve gpr_or_zero_l_not_zero gpr_or_zero_l_zero: asmgen. + Lemma ireg_of_not_GPR0: forall m r, ireg_of m = OK r -> IR r <> IR GPR0. Proof. @@ -280,6 +292,30 @@ Proof. intros. unfold compare_uint. Simpl. Qed. +Lemma compare_slong_spec: + forall rs v1 v2, + let rs1 := nextinstr (compare_slong rs v1 v2) in + rs1#CR0_0 = Val.of_optbool (Val.cmpl_bool Clt v1 v2) + /\ rs1#CR0_1 = Val.of_optbool (Val.cmpl_bool Cgt v1 v2) + /\ rs1#CR0_2 = Val.of_optbool (Val.cmpl_bool Ceq v1 v2) + /\ forall r', r' <> CR0_0 -> r' <> CR0_1 -> r' <> CR0_2 -> r' <> CR0_3 -> r' <> PC -> rs1#r' = rs#r'. +Proof. + intros. unfold rs1. split. reflexivity. split. reflexivity. split. reflexivity. + intros. unfold compare_slong. Simpl. +Qed. + +Lemma compare_ulong_spec: + forall rs m v1 v2, + let rs1 := nextinstr (compare_ulong rs m v1 v2) in + rs1#CR0_0 = Val.of_optbool (Val.cmplu_bool (Mem.valid_pointer m) Clt v1 v2) + /\ rs1#CR0_1 = Val.of_optbool (Val.cmplu_bool (Mem.valid_pointer m) Cgt v1 v2) + /\ rs1#CR0_2 = Val.of_optbool (Val.cmplu_bool (Mem.valid_pointer m) Ceq v1 v2) + /\ forall r', r' <> CR0_0 -> r' <> CR0_1 -> r' <> CR0_2 -> r' <> CR0_3 -> r' <> PC -> rs1#r' = rs#r'. +Proof. + intros. unfold rs1. split. reflexivity. split. reflexivity. split. reflexivity. + intros. unfold compare_ulong. Simpl. +Qed. + (** Loading a constant. *) Lemma loadimm_correct: @@ -493,6 +529,183 @@ Proof. intros. rewrite D; auto. unfold rs1; Simpl. Qed. +(** Load int64 constant. *) + +Lemma loadimm64_correct: + forall r n k rs m, + exists rs', + exec_straight ge fn (loadimm64 r n k) rs m k rs' m + /\ rs'#r = Vlong n + /\ forall r': preg, r' <> r -> r' <> GPR12 -> r' <> PC -> rs'#r' = rs#r'. +Proof. + intros. unfold loadimm64. + set (hi_s := Int64.sign_ext 16 (Int64.shr n (Int64.repr 16))). + set (hi' := Int64.shl hi_s (Int64.repr 16)). + destruct (Int64.eq n (low64_s n)). + (* addi *) + econstructor; split. apply exec_straight_one. simpl; eauto. auto. + rewrite Int64.add_zero_l. intuition Simpl. + (* addis + ori *) + predSpec Int64.eq Int64.eq_spec n (Int64.or hi' (low64_u n)). + econstructor; split. eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. + split. Simpl. rewrite Int64.add_zero_l. simpl; f_equal; auto. + intros. Simpl. + (* ldi *) + econstructor; split. apply exec_straight_one. simpl; eauto. auto. + intuition Simpl. +Qed. + +(** Add int64 immediate. *) + +Lemma addimm64_correct: + forall r1 r2 n k rs m, + r2 <> GPR0 -> + exists rs', + exec_straight ge fn (addimm64 r1 r2 n k) rs m k rs' m + /\ rs'#r1 = Val.addl rs#r2 (Vlong n) + /\ forall r': preg, r' <> r1 -> r' <> GPR0 -> r' <> GPR12 -> r' <> PC -> rs'#r' = rs#r'. +Proof. + intros. unfold addimm64, opimm64. destruct (Int64.eq n (low64_s n)); [|destruct (ireg_eq r2 GPR12)]. +- (* addi *) + econstructor; split. apply exec_straight_one. + simpl. rewrite gpr_or_zero_l_not_zero; eauto. + reflexivity. + intuition Simpl. +- (* move-loadimm-add *) + subst r2. + edestruct (loadimm64_correct GPR12 n) as (rs2 & A & B & C). + econstructor; split. eapply exec_straight_step. simpl; reflexivity. auto. + eapply exec_straight_trans. eexact A. apply exec_straight_one. simpl; reflexivity. auto. + split. rewrite B, C by eauto with asmgen. Simpl. + intros. Simpl. rewrite C by auto. Simpl. +- (* loadimm-add *) + edestruct (loadimm64_correct GPR0 n) as (rs2 & A & B & C). + econstructor; split. eapply exec_straight_trans. eexact A. apply exec_straight_one. simpl; reflexivity. auto. + split. rewrite B, C by eauto with asmgen. Simpl. + intros. Simpl. +Qed. + +(** Or int64 immediate. *) + +Lemma orimm64_correct: + forall r1 r2 n k rs m, + r2 <> GPR0 -> + exists rs', + exec_straight ge fn (orimm64 r1 r2 n k) rs m k rs' m + /\ rs'#r1 = Val.orl rs#r2 (Vlong n) + /\ forall r': preg, r' <> r1 -> r' <> GPR0 -> r' <> GPR12 -> r' <> PC -> rs'#r' = rs#r'. +Proof. + intros. unfold orimm64, opimm64. destruct (Int64.eq n (low64_u n)); [|destruct (ireg_eq r2 GPR12)]. +- (* ori *) + econstructor; split. apply exec_straight_one. simpl; eauto. reflexivity. + intuition Simpl. +- (* move-loadimm-or *) + subst r2. + edestruct (loadimm64_correct GPR12 n) as (rs2 & A & B & C). + econstructor; split. eapply exec_straight_step. simpl; reflexivity. auto. + eapply exec_straight_trans. eexact A. apply exec_straight_one. simpl; reflexivity. auto. + split. rewrite B, C by eauto with asmgen. Simpl. + intros. Simpl. rewrite C by auto. Simpl. +- (* loadimm-or *) + edestruct (loadimm64_correct GPR0 n) as (rs2 & A & B & C). + econstructor; split. eapply exec_straight_trans. eexact A. apply exec_straight_one. simpl; reflexivity. auto. + split. rewrite B, C by eauto with asmgen. Simpl. + intros. Simpl. +Qed. + +(** Xor int64 immediate. *) + +Lemma xorimm64_correct: + forall r1 r2 n k rs m, + r2 <> GPR0 -> + exists rs', + exec_straight ge fn (xorimm64 r1 r2 n k) rs m k rs' m + /\ rs'#r1 = Val.xorl rs#r2 (Vlong n) + /\ forall r': preg, r' <> r1 -> r' <> GPR0 -> r' <> GPR12 -> r' <> PC -> rs'#r' = rs#r'. +Proof. + intros. unfold xorimm64, opimm64. destruct (Int64.eq n (low64_u n)); [|destruct (ireg_eq r2 GPR12)]. +- (* xori *) + econstructor; split. apply exec_straight_one. simpl; eauto. reflexivity. + intuition Simpl. +- (* move-loadimm-xor *) + subst r2. + edestruct (loadimm64_correct GPR12 n) as (rs2 & A & B & C). + econstructor; split. eapply exec_straight_step. simpl; reflexivity. auto. + eapply exec_straight_trans. eexact A. apply exec_straight_one. simpl; reflexivity. auto. + split. rewrite B, C by eauto with asmgen. Simpl. + intros. Simpl. rewrite C by auto. Simpl. +- (* loadimm-xor *) + edestruct (loadimm64_correct GPR0 n) as (rs2 & A & B & C). + econstructor; split. eapply exec_straight_trans. eexact A. apply exec_straight_one. simpl; reflexivity. auto. + split. rewrite B, C by eauto with asmgen. Simpl. + intros. Simpl. +Qed. + +(** And int64 immediate. *) + +Lemma andimm64_base_correct: + forall r1 r2 n k rs m, + r2 <> GPR0 -> + exists rs', + exec_straight ge fn (andimm64_base r1 r2 n k) rs m k rs' m + /\ rs'#r1 = Val.andl rs#r2 (Vlong n) + /\ forall r': preg, r' <> r1 -> r' <> GPR12 -> important_preg r' = true -> rs'#r' = rs#r'. +Proof. + intros. unfold andimm64_base, opimm64. destruct (Int64.eq n (low64_u n)); [|destruct (ireg_eq r2 GPR12)]. +- (* andi *) + econstructor; split. apply exec_straight_one. simpl; eauto. reflexivity. + unfold compare_slong; intuition Simpl. +- (* move-loadimm-and *) + subst r2. + edestruct (loadimm64_correct GPR12 n) as (rs2 & A & B & C). + econstructor; split. eapply exec_straight_step. simpl; reflexivity. auto. + eapply exec_straight_trans. eexact A. apply exec_straight_one. simpl; reflexivity. auto. + split. rewrite B, C by eauto with asmgen. unfold compare_slong; Simpl. + intros. unfold compare_slong; Simpl. rewrite C by auto with asmgen. Simpl. +- (* loadimm-xor *) + edestruct (loadimm64_correct GPR0 n) as (rs2 & A & B & C). + econstructor; split. eapply exec_straight_trans. eexact A. apply exec_straight_one. simpl; reflexivity. auto. + split. rewrite B, C by eauto with asmgen. unfold compare_slong; Simpl. + intros. unfold compare_slong; Simpl. +Qed. + +Lemma andimm64_correct: + forall r1 r2 n k rs m, + r2 <> GPR0 -> + exists rs', + exec_straight ge fn (andimm64 r1 r2 n k) rs m k rs' m + /\ rs'#r1 = Val.andl rs#r2 (Vlong n) + /\ forall r': preg, r' <> r1 -> r' <> GPR12 -> important_preg r' = true -> rs'#r' = rs#r'. +Proof. + intros. unfold andimm64. destruct (is_rldl_mask n || is_rldr_mask n). +- econstructor; split. eapply exec_straight_one. simpl; reflexivity. reflexivity. + split. Simpl. destruct (rs r2); simpl; auto. rewrite Int64.rolm_zero. auto. + intros; Simpl. +- apply andimm64_base_correct; auto. +Qed. + +(** Rotate-and-mask for int64 *) + +Lemma rolm64_correct: + forall r1 r2 amount mask k rs m, + r1 <> GPR0 -> + exists rs', + exec_straight ge fn (rolm64 r1 r2 amount mask k) rs m k rs' m + /\ rs'#r1 = Val.rolml rs#r2 amount mask + /\ forall r': preg, r' <> r1 -> r' <> GPR12 -> important_preg r' = true -> rs'#r' = rs#r'. +Proof. + intros. unfold rolm64. + destruct (is_rldl_mask mask || is_rldr_mask mask || is_rldl_mask (Int64.shru' mask amount)). +- econstructor; split. eapply exec_straight_one. simpl; reflexivity. reflexivity. + intuition Simpl. +- edestruct (andimm64_base_correct r1 r1 mask k) as (rs2 & A & B & C); auto. + econstructor; split. + eapply exec_straight_step. simpl; reflexivity. reflexivity. eexact A. + split. rewrite B. Simpl. destruct (rs r2); simpl; auto. unfold Int64.rolm. + rewrite Int64.and_assoc, Int64.and_mone_l; auto. + intros; Simpl. rewrite C by auto. Simpl. +Qed. + (** Indexed memory loads. *) Lemma accessind_load_correct: @@ -541,8 +754,10 @@ Proof. unfold loadind; intros. destruct ty; try discriminate; destruct (preg_of dst); inv H; simpl in H0. apply accessind_load_correct with (inj := IR) (chunk := Mint32); auto with asmgen. apply accessind_load_correct with (inj := FR) (chunk := Mfloat64); auto with asmgen. + apply accessind_load_correct with (inj := IR) (chunk := Mint64); auto with asmgen. apply accessind_load_correct with (inj := FR) (chunk := Mfloat32); auto with asmgen. apply accessind_load_correct with (inj := IR) (chunk := Many32); auto with asmgen. + apply accessind_load_correct with (inj := IR) (chunk := Many64); auto with asmgen. apply accessind_load_correct with (inj := FR) (chunk := Many64); auto with asmgen. Qed. @@ -593,8 +808,10 @@ Proof. destruct ty; try discriminate; destruct (preg_of src) ; inv H; simpl in H0. apply accessind_store_correct with (inj := IR) (chunk := Mint32); auto with asmgen. apply accessind_store_correct with (inj := FR) (chunk := Mfloat64); auto with asmgen. + apply accessind_store_correct with (inj := IR) (chunk := Mint64); auto with asmgen. apply accessind_store_correct with (inj := FR) (chunk := Mfloat32); auto with asmgen. apply accessind_store_correct with (inj := IR) (chunk := Many32); auto with asmgen. + apply accessind_store_correct with (inj := IR) (chunk := Many64); auto with asmgen. apply accessind_store_correct with (inj := FR) (chunk := Many64); auto with asmgen. Qed. @@ -669,7 +886,7 @@ Lemma transl_cond_correct_1: (if snd (crbit_for_cond cond) then Val.of_optbool (eval_condition cond (map rs (map preg_of args)) m) else Val.notbool (Val.of_optbool (eval_condition cond (map rs (map preg_of args)) m))) - /\ forall r, important_preg r = true -> rs'#r = rs#r. + /\ forall r, important_preg r = true -> preg_notin r (destroyed_by_cond cond) -> rs'#r = rs#r. Proof. intros. Opaque Int.eq. @@ -755,6 +972,64 @@ Opaque Int.eq. fold (option_map negb (Some (Int.eq (Int.and i0 i) Int.zero))). rewrite Val.notbool_negb_3. rewrite Val.notbool_idem4. auto. auto with asmgen. +- (* Ccompl *) + destruct (compare_slong_spec rs (rs x) (rs x0)) as [A [B [C D]]]. + econstructor; split. + apply exec_straight_one. simpl; reflexivity. reflexivity. + rewrite <- Val.notbool_negb_3. rewrite <- Val.negate_cmpl_bool. + split. case c0; simpl; auto. + auto with asmgen. +- (* Ccomplu *) + destruct (compare_ulong_spec rs m (rs x) (rs x0)) as [A [B [C D]]]. + econstructor; split. + apply exec_straight_one. simpl; reflexivity. reflexivity. + rewrite <- Val.notbool_negb_3. rewrite <- Val.negate_cmplu_bool. + split. case c0; simpl; auto. + auto with asmgen. +- (* Ccomplimm *) + rewrite <- Val.notbool_negb_3. rewrite <- Val.negate_cmpl_bool. + destruct (Int64.eq i (low64_s i)); [|destruct (ireg_eq x GPR12)]; inv EQ0. ++ destruct (compare_slong_spec rs (rs x) (Vlong i)) as [A [B [C D]]]. + econstructor; split. + apply exec_straight_one. simpl; reflexivity. reflexivity. + split. case c0; simpl; auto. auto with asmgen. ++ destruct (loadimm64_correct GPR12 i (Pcmpd GPR0 GPR12 :: k) (nextinstr (rs#GPR0 <- (rs#GPR12))) m) as [rs1 [EX1 [RES1 OTH1]]]. + destruct (compare_slong_spec rs1 (rs GPR12) (Vlong i)) as [A [B [C D]]]. + assert (SAME: rs1 GPR0 = rs GPR12) by (apply OTH1; eauto with asmgen). + econstructor; split. + eapply exec_straight_step. simpl;reflexivity. reflexivity. + eapply exec_straight_trans. eexact EX1. eapply exec_straight_one. simpl;reflexivity. reflexivity. + split. rewrite RES1, SAME. destruct c0; simpl; auto. + simpl; intros. rewrite RES1, SAME. rewrite D by eauto with asmgen. rewrite OTH1 by eauto with asmgen. Simpl. ++ destruct (loadimm64_correct GPR0 i (Pcmpd x GPR0 :: k) rs m) as [rs1 [EX1 [RES1 OTH1]]]. + destruct (compare_slong_spec rs1 (rs x) (Vlong i)) as [A [B [C D]]]. + assert (SAME: rs1 x = rs x) by (apply OTH1; eauto with asmgen). + econstructor; split. + eapply exec_straight_trans. eexact EX1. eapply exec_straight_one. simpl;reflexivity. reflexivity. + split. rewrite RES1, SAME. destruct c0; simpl; auto. + simpl; intros. rewrite RES1, SAME. rewrite D; eauto with asmgen. +- (* Ccompluimm *) + rewrite <- Val.notbool_negb_3. rewrite <- Val.negate_cmplu_bool. + destruct (Int64.eq i (low64_u i)); [|destruct (ireg_eq x GPR12)]; inv EQ0. ++ destruct (compare_ulong_spec rs m (rs x) (Vlong i)) as [A [B [C D]]]. + econstructor; split. + apply exec_straight_one. simpl; reflexivity. reflexivity. + split. case c0; simpl; auto. auto with asmgen. ++ destruct (loadimm64_correct GPR12 i (Pcmpld GPR0 GPR12 :: k) (nextinstr (rs#GPR0 <- (rs#GPR12))) m) as [rs1 [EX1 [RES1 OTH1]]]. + destruct (compare_ulong_spec rs1 m (rs GPR12) (Vlong i)) as [A [B [C D]]]. + assert (SAME: rs1 GPR0 = rs GPR12) by (apply OTH1; eauto with asmgen). + econstructor; split. + eapply exec_straight_step. simpl;reflexivity. reflexivity. + eapply exec_straight_trans. eexact EX1. eapply exec_straight_one. simpl;reflexivity. reflexivity. + split. rewrite RES1, SAME. destruct c0; simpl; auto. + simpl; intros. rewrite RES1, SAME. rewrite D by eauto with asmgen. rewrite OTH1 by eauto with asmgen. Simpl. ++ destruct (loadimm64_correct GPR0 i (Pcmpld x GPR0 :: k) rs m) as [rs1 [EX1 [RES1 OTH1]]]. + destruct (compare_ulong_spec rs1 m (rs x) (Vlong i)) as [A [B [C D]]]. + assert (SAME: rs1 x = rs x) by (apply OTH1; eauto with asmgen). + econstructor; split. + eapply exec_straight_trans. eexact EX1. eapply exec_straight_one. simpl;reflexivity. reflexivity. + split. rewrite RES1, SAME. destruct c0; simpl; auto. + simpl; intros. rewrite RES1, SAME. rewrite D; eauto with asmgen. Qed. Lemma transl_cond_correct_2: @@ -767,7 +1042,7 @@ Lemma transl_cond_correct_2: (if snd (crbit_for_cond cond) then Val.of_bool b else Val.notbool (Val.of_bool b)) - /\ forall r, important_preg r = true -> rs'#r = rs#r. + /\ forall r, important_preg r = true -> preg_notin r (destroyed_by_cond cond) -> rs'#r = rs#r. Proof. intros. replace (Val.of_bool b) @@ -788,13 +1063,14 @@ Lemma transl_cond_correct_3: (if snd (crbit_for_cond cond) then Val.of_bool b else Val.notbool (Val.of_bool b)) - /\ agree ms sp rs'. + /\ agree (Mach.undef_regs (destroyed_by_cond cond) ms) sp rs'. Proof. intros. exploit transl_cond_correct_2. eauto. eapply eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. intros [rs' [A [B C]]]. - exists rs'; split. eauto. split. auto. apply agree_exten with rs; auto with asmgen. + exists rs'; split. eauto. split. auto. apply agree_undef_regs with rs; auto. intros r D. + apply C. apply important_data_preg_1; auto. Qed. (** Translation of condition operators *) @@ -851,7 +1127,7 @@ Lemma transl_cond_op_correct: exists rs', exec_straight ge fn c rs m k rs' m /\ rs'#(preg_of r) = Val.of_optbool (eval_condition cond (map rs (map preg_of args)) m) - /\ forall r', important_preg r' = true -> r' <> preg_of r -> rs'#r' = rs#r'. + /\ forall r', important_preg r' = true -> preg_notin r' (destroyed_by_cond cond) -> r' <> preg_of r -> rs'#r' = rs#r'. Proof. intros until args. unfold transl_cond_op. destruct (classify_condition cond args); intros; monadInv H; simpl; @@ -921,49 +1197,49 @@ Proof. assert (SAME: forall v1 v2, v1 = v2 -> Val.lessdef v2 v1). { intros; subst; auto. } Opaque Int.eq. intros. unfold transl_op in H; destruct op; ArgsInv; simpl in H0; try (inv H0); try TranslOpSimpl. - (* Omove *) +- (* Omove *) destruct (preg_of res) eqn:RES; destruct (preg_of m0) eqn:ARG; inv H. TranslOpSimpl. TranslOpSimpl. - (* Ointconst *) +- (* Ointconst *) destruct (loadimm_correct x i k rs m) as [rs' [A [B C]]]. exists rs'. rewrite B. auto with asmgen. - (* Oaddrsymbol *) +- (* Oaddrsymbol *) set (v' := Genv.symbol_address ge i i0). destruct (symbol_is_small_data i i0) eqn:SD; [ | destruct (symbol_is_rel_data i i0) ]. - (* small data *) ++ (* small data *) Opaque Val.add. econstructor; split. apply exec_straight_one; simpl; reflexivity. split. apply SAME. Simpl. rewrite small_data_area_addressing by auto. apply add_zero_symbol_address. intros; Simpl. - (* relative data *) ++ (* relative data *) econstructor; split. eapply exec_straight_two; simpl; reflexivity. split. apply SAME. Simpl. rewrite gpr_or_zero_not_zero by eauto with asmgen. Simpl. apply low_high_half_zero. intros; Simpl. - (* absolute data *) ++ (* absolute data *) econstructor; split. eapply exec_straight_two; simpl; reflexivity. split. apply SAME. Simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen. Simpl. apply low_high_half_zero. intros; Simpl. - (* Oaddrstack *) +- (* Oaddrstack *) destruct (addimm_correct x GPR1 (Ptrofs.to_int i) k rs m) as [rs' [EX [RES OTH]]]; eauto with asmgen. exists rs'; split. auto. split; auto with asmgen. - rewrite RES. destruct (rs GPR1); simpl; auto. + rewrite RES. destruct (rs GPR1); simpl; auto. Transparent Val.add. simpl. rewrite Ptrofs.of_int_to_int; auto. Opaque Val.add. - (* Oaddimm *) +- (* Oaddimm *) destruct (addimm_correct x0 x i k rs m) as [rs' [A [B C]]]; eauto with asmgen. exists rs'; auto with asmgen. - (* Oaddsymbol *) +- (* Oaddsymbol *) destruct (symbol_is_small_data i i0) eqn:SD; [ | destruct (symbol_is_rel_data i i0) ]. - (* small data *) ++ (* small data *) econstructor; split. eapply exec_straight_two; simpl; reflexivity. split. apply SAME. Simpl. rewrite (Val.add_commut (rs x)). f_equal. rewrite small_data_area_addressing by auto. apply add_zero_symbol_address. intros; Simpl. - (* relative data *) ++ (* relative data *) econstructor; split. eapply exec_straight_trans. eapply exec_straight_two; simpl; reflexivity. eapply exec_straight_two; simpl; reflexivity. @@ -971,12 +1247,12 @@ Opaque Val.add. Simpl. rewrite ! gpr_or_zero_zero. rewrite ! gpr_or_zero_not_zero by eauto with asmgen. Simpl. rewrite low_high_half_zero. auto. intros; Simpl. - (* absolute data *) ++ (* absolute data *) econstructor; split. eapply exec_straight_two; simpl; reflexivity. split. Simpl. rewrite ! gpr_or_zero_not_zero by (eauto with asmgen). Simpl. rewrite Val.add_assoc. rewrite (Val.add_commut (rs x)). rewrite low_high_half. auto. intros; Simpl. - (* Osubimm *) +- (* Osubimm *) case (Int.eq (high_s i) Int.zero). TranslOpSimpl. destruct (loadimm_correct GPR0 i (Psubfc x0 x GPR0 :: k) rs m) as [rs1 [EX [RES OTH]]]. @@ -984,7 +1260,7 @@ Opaque Val.add. eapply exec_straight_trans. eexact EX. apply exec_straight_one; simpl; reflexivity. split. Simpl. rewrite RES. rewrite OTH; eauto with asmgen. intros; Simpl. - (* Omulimm *) +- (* Omulimm *) case (Int.eq (high_s i) Int.zero). TranslOpSimpl. destruct (loadimm_correct GPR0 i (Pmullw x0 x GPR0 :: k) rs m) as [rs1 [EX [RES OTH]]]. @@ -992,61 +1268,111 @@ Opaque Val.add. eapply exec_straight_trans. eexact EX. apply exec_straight_one; simpl; reflexivity. split. Simpl. rewrite RES. rewrite OTH; eauto with asmgen. intros; Simpl. - (* Odivs *) +- (* Odivs *) replace v with (Val.maketotal (Val.divs (rs x) (rs x0))). TranslOpSimpl. rewrite H1; auto. - (* Odivu *) +- (* Odivu *) replace v with (Val.maketotal (Val.divu (rs x) (rs x0))). TranslOpSimpl. rewrite H1; auto. - (* Oand *) +- (* Oand *) set (v' := Val.and (rs x) (rs x0)) in *. pose (rs1 := rs#x1 <- v'). destruct (compare_sint_spec rs1 v' Vzero) as [A [B [C D]]]. econstructor; split. apply exec_straight_one; simpl; reflexivity. split. rewrite D; auto with asmgen. unfold rs1; Simpl. intros. rewrite D; auto with asmgen. unfold rs1; Simpl. - (* Oandimm *) +- (* Oandimm *) destruct (andimm_correct x0 x i k rs m) as [rs' [A [B C]]]. eauto with asmgen. exists rs'; auto with asmgen. - (* Oorimm *) +- (* Oorimm *) destruct (orimm_correct x0 x i k rs m) as [rs' [A [B C]]]. exists rs'; auto with asmgen. - (* Oxorimm *) +- (* Oxorimm *) destruct (xorimm_correct x0 x i k rs m) as [rs' [A [B C]]]. exists rs'; auto with asmgen. - (* Onor *) +- (* Onor *) replace (Val.notint (rs x)) with (Val.notint (Val.or (rs x) (rs x))). TranslOpSimpl. destruct (rs x); simpl; auto. rewrite Int.or_idem. auto. - (* Oshrximm *) +- (* Oshrximm *) econstructor; split. eapply exec_straight_two; simpl; reflexivity. split. Simpl. apply SAME. apply Val.shrx_carry. auto. intros; Simpl. - (* Orolm *) +- (* Orolm *) destruct (rolm_correct x0 x i i0 k rs m) as [rs' [A [B C]]]. eauto with asmgen. exists rs'; auto. +- (* Olongconst *) + destruct (loadimm64_correct x i k rs m) as [rs' [A [B C]]]. + exists rs'; auto with asmgen. +- (* Oaddlimm *) + destruct (addimm64_correct x0 x i k rs m) as [rs' [A [B C]]]. eauto with asmgen. + exists rs'; auto with asmgen. +- (* Odivl *) + replace v with (Val.maketotal (Val.divls (rs x) (rs x0))). + TranslOpSimpl. + rewrite H1; auto. +- (* Odivlu *) + replace v with (Val.maketotal (Val.divlu (rs x) (rs x0))). + TranslOpSimpl. + rewrite H1; auto. +- (* Oandl *) + set (v' := Val.andl (rs x) (rs x0)) in *. + pose (rs1 := rs#x1 <- v'). + destruct (compare_slong_spec rs1 v' (Vlong Int64.zero)) as [A [B [C D]]]. + econstructor; split. apply exec_straight_one; simpl; reflexivity. + split. rewrite D; auto with asmgen. unfold rs1; Simpl. + intros. rewrite D; auto with asmgen. unfold rs1; Simpl. +- (* Oandlimm *) + destruct (andimm64_correct x0 x i k rs m) as [rs' [A [B C]]]. eauto with asmgen. + exists rs'; auto with asmgen. +- (* Oorlimm *) + destruct (orimm64_correct x0 x i k rs m) as [rs' [A [B C]]]. eauto with asmgen. + exists rs'; auto with asmgen. +- (* Oxorlimm *) + destruct (xorimm64_correct x0 x i k rs m) as [rs' [A [B C]]]. eauto with asmgen. + exists rs'; auto with asmgen. +- (* Onotl *) + econstructor; split. eapply exec_straight_one; simpl; reflexivity. + split. Simpl. destruct (rs x); simpl; auto. rewrite Int64.or_idem; auto. + intros; Simpl. +- (* Oshrxlimm *) + econstructor; split. + eapply exec_straight_two; simpl; reflexivity. + split. Simpl. apply SAME. apply Val.shrxl_carry. auto. + intros; Simpl. +- (* Orolml *) + destruct (rolm64_correct x0 x i i0 k rs m) as [rs' [A [B C]]]. eauto with asmgen. + exists rs'; auto with asmgen. +- (* Olongoffloat *) + replace v with (Val.maketotal (Val.longoffloat (rs x))). + TranslOpSimpl. + rewrite H1; auto. +- (* Ofloatoflong *) + replace v with (Val.maketotal (Val.floatoflong (rs x))). + TranslOpSimpl. + rewrite H1; auto. (* Ointoffloat *) - replace v with (Val.maketotal (Val.intoffloat (rs x))). +- replace v with (Val.maketotal (Val.intoffloat (rs x))). TranslOpSimpl. rewrite H1; auto. (* Ointuoffloat *) - replace v with (Val.maketotal (Val.intuoffloat (rs x))). +- replace v with (Val.maketotal (Val.intuoffloat (rs x))). TranslOpSimpl. rewrite H1; auto. (* Ofloatofint *) - replace v with (Val.maketotal (Val.floatofint (rs x))). +- replace v with (Val.maketotal (Val.floatofint (rs x))). TranslOpSimpl. rewrite H1; auto. (* Ofloatofintu *) - replace v with (Val.maketotal (Val.floatofintu (rs x))). +- replace v with (Val.maketotal (Val.floatofintu (rs x))). TranslOpSimpl. rewrite H1; auto. (* Ocmp *) - destruct (transl_cond_op_correct c0 args res k rs m c) as [rs' [A [B C]]]; auto. +- destruct (transl_cond_op_correct c0 args res k rs m c) as [rs' [A [B C]]]; auto. exists rs'; auto with asmgen. Qed. @@ -1179,7 +1505,7 @@ Transparent Val.add. (* Ainstack *) set (ofs := Ptrofs.to_int i) in *. assert (L: Val.lessdef (Val.offset_ptr (rs GPR1) i) (Val.add (rs GPR1) (Vint ofs))). - { destruct (rs GPR1); simpl; auto. unfold ofs; rewrite Ptrofs.of_int_to_int; auto. } + { destruct (rs GPR1); simpl; auto. unfold ofs; rewrite Ptrofs.of_int_to_int; auto. } destruct (Int.eq (high_s ofs) Int.zero); inv TR. apply MK1. simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto. set (rs1 := nextinstr (rs#temp <- (Val.add rs#GPR1 (Vint (Int.shl (high_s ofs) (Int.repr 16)))))). @@ -1209,7 +1535,7 @@ Lemma transl_load_correct: Proof. intros. assert (LD: forall v, Val.lessdef a v -> v = a). - { intros. inv H2; auto. discriminate H1. } + { intros. inv H2; auto. discriminate H1. } assert (BASE: forall mk1 mk2 k' chunk' v', transl_memory_access mk1 mk2 addr args GPR12 k' = OK c -> Mem.loadv chunk' m a = Some v' -> @@ -1257,6 +1583,8 @@ Proof. eapply BASE; eauto; erewrite ireg_of_eq by eauto; auto. - (* Mint32 *) eapply BASE; eauto; erewrite ireg_of_eq by eauto; auto. +- (* Mint64 *) + eapply BASE; eauto; erewrite ireg_of_eq by eauto; auto. - (* Mfloat32 *) eapply BASE; eauto; erewrite freg_of_eq by eauto; auto. - (* Mfloat64 *) @@ -1277,7 +1605,7 @@ Proof. Local Transparent destroyed_by_store. intros. assert (LD: forall v, Val.lessdef a v -> v = a). - { intros. inv H2; auto. discriminate H1. } + { intros. inv H2; auto. discriminate H1. } assert (TEMP0: int_temp_for src = GPR11 \/ int_temp_for src = GPR12). unfold int_temp_for. destruct (mreg_eq src R12); auto. assert (TEMP1: int_temp_for src <> GPR0). @@ -1323,6 +1651,8 @@ Local Transparent destroyed_by_store. eapply BASE; eauto; erewrite ireg_of_eq by eauto; auto. - (* Mint32 *) eapply BASE; eauto; erewrite ireg_of_eq by eauto; auto. +- (* Mint64 *) + eapply BASE; eauto; erewrite ireg_of_eq by eauto; auto. - (* Mfloat32 *) eapply BASE; eauto; erewrite freg_of_eq by eauto; auto. - (* Mfloat64 *) @@ -1386,4 +1716,3 @@ Proof. Qed. End CONSTRUCTORS. - diff --git a/powerpc/ConstpropOp.vp b/powerpc/ConstpropOp.vp index 403a7a77..8946ae27 100644 --- a/powerpc/ConstpropOp.vp +++ b/powerpc/ConstpropOp.vp @@ -39,7 +39,7 @@ Definition const_for_result (a: aval) : option operation := Section STRENGTH_REDUCTION. -Nondetfunction cond_strength_reduction +Nondetfunction cond_strength_reduction (cond: condition) (args: list reg) (vl: list aval) := match cond, args, vl with | Ccomp c, r1 :: r2 :: nil, I n1 :: v2 :: nil => @@ -50,7 +50,7 @@ Nondetfunction cond_strength_reduction (Ccompuimm (swap_comparison c) n1, r2 :: nil) | Ccompu c, r1 :: r2 :: nil, v1 :: I n2 :: nil => (Ccompuimm c n2, r1 :: nil) - | _, _, _ => + | _, _, _ => (cond, args) end. @@ -158,7 +158,7 @@ Definition make_cast8signed (r: reg) (a: aval) := Definition make_cast16signed (r: reg) (a: aval) := if vincl a (Sgn Ptop 16) then (Omove, r :: nil) else (Ocast16signed, r :: nil). -Nondetfunction op_strength_reduction +Nondetfunction op_strength_reduction (op: operation) (args: list reg) (vl: list aval) := match op, args, vl with | Ocast8signed, r1 :: nil, v1 :: nil => make_cast8signed r1 v1 diff --git a/powerpc/ConstpropOpproof.v b/powerpc/ConstpropOpproof.v index bb0605ee..d2ebf52d 100644 --- a/powerpc/ConstpropOpproof.v +++ b/powerpc/ConstpropOpproof.v @@ -106,7 +106,7 @@ Proof. + (* global *) inv H2. exists (Genv.symbol_address ge id ofs); auto. + (* stack *) - inv H2. exists (Vptr sp ofs); split; auto. simpl. rewrite Ptrofs.add_zero_l; auto. + inv H2. exists (Vptr sp ofs); split; auto. simpl. rewrite Ptrofs.add_zero_l; auto. Qed. Lemma cond_strength_reduction_correct: @@ -478,7 +478,7 @@ Remark shift_symbol_address: Genv.symbol_address ge id (Ptrofs.add ofs (Ptrofs.of_int delta)) = Val.add (Genv.symbol_address ge id ofs) (Vint delta). Proof. intros. unfold Genv.symbol_address. destruct (Genv.find_symbol ge id); auto. -Qed. +Qed. Lemma addr_strength_reduction_correct: forall addr args vl res, @@ -491,7 +491,7 @@ Proof. destruct (addr_strength_reduction_match addr args vl); simpl; intros VL EA; InvApproxRegs; SimplVM; try (inv EA). - rewrite shift_symbol_address. econstructor; split; eauto. apply Val.add_lessdef; auto. -- econstructor; split; eauto. +- econstructor; split; eauto. change (Val.lessdef (Val.add (Vint n1) rs#r2) (Genv.symbol_address ge symb (Ptrofs.add (Ptrofs.of_int n1) n2))). rewrite Ptrofs.add_commut. rewrite shift_symbol_address. rewrite Val.add_commut. apply Val.add_lessdef; auto. diff --git a/powerpc/Conventions1.v b/powerpc/Conventions1.v index b83ab6da..2793fbfb 100644 --- a/powerpc/Conventions1.v +++ b/powerpc/Conventions1.v @@ -18,6 +18,7 @@ Require Import Decidableplus. Require Import AST. Require Import Events. Require Import Locations. +Require Archi. (** * Classification of machine registers *) @@ -41,6 +42,38 @@ Definition is_callee_save (r: mreg): bool := | F24 | F25 | F26 | F27 | F28 | F29 | F30 | F31 => true end. +Definition destroyed_at_call := + List.filter (fun r => negb (is_callee_save r)) all_mregs. + +(** The following definitions are used by the register allocator. *) + +(** When a PPC64 processor is used with the PPC32 ABI, the high 32 bits + of integer callee-save registers may not be preserved. So, + declare all integer registers as having size 32 bits for the purpose + of determining which variables can go in callee-save registers. *) + +Definition callee_save_type (r: mreg): typ := + match r with + | R3 | R4 | R5 | R6 | R7 | R8 | R9 | R10 | R11 | R12 + | R14 | R15 | R16 | R17 | R18 | R19 | R20 | R21 | R22 | R23 | R24 + | R25 | R26 | R27 | R28 | R29 | R30 | R31 => Tany32 + | F0 | F1 | F2 | F3 | F4 | F5 | F6 | F7 + | F8 | F9 | F10 | F11 | F12 | F13 | F14 | F15 + | F16 | F17 | F18 | F19 | F20 | F21 | F22 | F23 + | F24 | F25 | F26 | F27 | F28 | F29 | F30 | F31 => Tany64 + end. + +Definition is_float_reg (r: mreg): bool := + match r with + | R3 | R4 | R5 | R6 | R7 | R8 | R9 | R10 | R11 | R12 + | R14 | R15 | R16 | R17 | R18 | R19 | R20 | R21 | R22 | R23 | R24 + | R25 | R26 | R27 | R28 | R29 | R30 | R31 => false + | F0 | F1 | F2 | F3 | F4 | F5 | F6 | F7 + | F8 | F9 | F10 | F11 | F12 | F13 + | F14 | F15 | F16 | F17 | F18 | F19 | F20 | F21 | F22 | F23 + | F24 | F25 | F26 | F27 | F28 | F29 | F30 | F31 => true + end. + Definition int_caller_save_regs := R3 :: R4 :: R5 :: R6 :: R7 :: R8 :: R9 :: R10 :: R11 :: R12 :: nil. @@ -55,23 +88,9 @@ Definition float_callee_save_regs := F31 :: F30 :: F29 :: F28 :: F27 :: F26 :: F25 :: F24 :: F23 :: F22 :: F21 :: F20 :: F19 :: F18 :: F17 :: F16 :: F15 :: F14 :: nil. -Definition destroyed_at_call := - List.filter (fun r => negb (is_callee_save r)) all_mregs. - Definition dummy_int_reg := R3. (**r Used in [Coloring]. *) Definition dummy_float_reg := F0. (**r Used in [Coloring]. *) -Definition is_float_reg (r: mreg): bool := - match r with - | R3 | R4 | R5 | R6 | R7 | R8 | R9 | R10 | R11 | R12 - | R14 | R15 | R16 | R17 | R18 | R19 | R20 | R21 | R22 | R23 | R24 - | R25 | R26 | R27 | R28 | R29 | R30 | R31 => false - | F0 | F1 | F2 | F3 | F4 | F5 | F6 | F7 - | F8 | F9 | F10 | F11 | F12 | F13 - | F14 | F15 | F16 | F17 | F18 | F19 | F20 | F21 | F22 | F23 - | F24 | F25 | F26 | F27 | F28 | F29 | F30 | F31 => true - end. - (** * Function calling conventions *) (** The functions in this section determine the locations (machine registers @@ -97,7 +116,7 @@ Definition is_float_reg (r: mreg): bool := registers [R3] or [F1] or [R3, R4], depending on the type of the returned value. We treat a function without result as a function with one integer result. *) -Definition loc_result (s: signature) : rpair mreg := +Definition loc_result_32 (s: signature) : rpair mreg := match s.(sig_res) with | None => One R3 | Some (Tint | Tany32) => One R3 @@ -105,12 +124,24 @@ Definition loc_result (s: signature) : rpair mreg := | Some Tlong => Twolong R3 R4 end. +Definition loc_result_64 (s: signature) : rpair mreg := + match s.(sig_res) with + | None => One R3 + | Some (Tint | Tlong | Tany32 | Tany64) => One R3 + | Some (Tfloat | Tsingle) => One F1 + end. + +Definition loc_result := + if Archi.ptr64 then loc_result_64 else loc_result_32. + +(** The result registers have types compatible with that given in the signature. *) + Lemma loc_result_type: forall sig, subtype (proj_sig_res sig) (typ_rpair mreg_type (loc_result sig)) = true. Proof. - intros. unfold proj_sig_res, loc_result. - destruct (sig_res sig) as [[]|]; simpl; destruct Archi.ppc64; auto. + intros. unfold proj_sig_res, loc_result, loc_result_32, loc_result_64, mreg_type. + destruct Archi.ptr64 eqn:?; destruct (sig_res sig) as [[]|]; destruct Archi.ppc64; simpl; auto. Qed. (** The result locations are caller-save registers *) @@ -119,8 +150,8 @@ Lemma loc_result_caller_save: forall (s: signature), forall_rpair (fun r => is_callee_save r = false) (loc_result s). Proof. - intros. - unfold loc_result. destruct (sig_res s) as [[]|]; simpl; auto. + intros. unfold loc_result, loc_result_32, loc_result_64, is_callee_save; + destruct Archi.ptr64; destruct (sig_res s) as [[]|]; simpl; auto. Qed. (** If the result is in a pair of registers, those registers are distinct and have type [Tint] at least. *) @@ -132,11 +163,13 @@ Lemma loc_result_pair: | Twolong r1 r2 => r1 <> r2 /\ sg.(sig_res) = Some Tlong /\ subtype Tint (mreg_type r1) = true /\ subtype Tint (mreg_type r2) = true - /\ Archi.splitlong = true + /\ Archi.ptr64 = false end. Proof. - intros; unfold loc_result; destruct (sig_res sg) as [[]|]; auto. - simpl; intuition congruence. + intros; unfold loc_result, loc_result_32, loc_result_64, mreg_type; + destruct Archi.ptr64; destruct (sig_res sg) as [[]|]; destruct Archi.ppc64; simpl; auto. + split; auto. congruence. + split; auto. congruence. Qed. (** The location of the result depends only on the result part of the signature *) @@ -144,7 +177,8 @@ Qed. Lemma loc_result_exten: forall s1 s2, s1.(sig_res) = s2.(sig_res) -> loc_result s1 = loc_result s2. Proof. - intros. unfold loc_result. rewrite H; auto. + intros. unfold loc_result, loc_result_32, loc_result_64. + destruct Archi.ptr64; rewrite H; auto. Qed. (** ** Location of function arguments *) @@ -191,7 +225,10 @@ Fixpoint loc_arguments_rec Twolong (R r1) (R r2) :: loc_arguments_rec tys (ir + 2) fr ofs | _, _ => let ofs := align ofs 2 in - Twolong (S Outgoing ofs Tint) (S Outgoing (ofs + 1) Tint) :: loc_arguments_rec tys ir fr (ofs + 2) + (if Archi.ptr64 + then One (S Outgoing ofs Tlong) + else Twolong (S Outgoing ofs Tint) (S Outgoing (ofs + 1) Tint)) :: + loc_arguments_rec tys ir fr (ofs + 2) end end. @@ -279,10 +316,12 @@ Opaque list_nth_z. destruct H. subst; split; left; eapply list_nth_z_in; eauto. eapply IHtyl; eauto. destruct H. - subst. split; (split; [omega|apply Z.divide_1_l]). + subst. destruct Archi.ptr64; [split|split;split]; try omega. + apply align_divides; omega. apply Z.divide_1_l. apply Z.divide_1_l. eapply Y; eauto. omega. destruct H. - subst. split; (split; [omega|apply Z.divide_1_l]). + subst. destruct Archi.ptr64; [split|split;split]; try omega. + apply align_divides; omega. apply Z.divide_1_l. apply Z.divide_1_l. eapply Y; eauto. omega. - (* single *) assert (ofs <= align ofs 2) by (apply align_le; omega). @@ -386,12 +425,15 @@ Proof. set (ir' := align ir 2) in *. assert (DFL: In (S Outgoing ofs ty) (regs_of_rpairs - (Twolong (S Outgoing (align ofs0 2) Tint) - (S Outgoing (align ofs0 2 + 1) Tint) + ((if Archi.ptr64 + then One (S Outgoing (align ofs0 2) Tlong) + else Twolong (S Outgoing (align ofs0 2) Tint) + (S Outgoing (align ofs0 2 + 1) Tint)) :: loc_arguments_rec tyl ir' fr (align ofs0 2 + 2))) -> ofs + typesize ty <= size_arguments_rec tyl ir' fr (align ofs0 2 + 2)). - { intros IN. destruct IN. inv H1. - transitivity (align ofs0 2 + 2). simpl; omega. apply size_arguments_rec_above. + { destruct Archi.ptr64; intros IN. + - destruct IN. inv H1. apply size_arguments_rec_above. auto. + - destruct IN. inv H1. transitivity (align ofs0 2 + 2). simpl; omega. apply size_arguments_rec_above. destruct H1. inv H1. transitivity (align ofs0 2 + 2). simpl; omega. apply size_arguments_rec_above. auto. } destruct (list_nth_z int_param_regs ir'); auto. diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v index ce9c3542..6f2c6a03 100644 --- a/powerpc/Machregs.v +++ b/powerpc/Machregs.v @@ -86,7 +86,7 @@ Definition mreg_type (r: mreg): typ := match r with | R3 | R4 | R5 | R6 | R7 | R8 | R9 | R10 | R11 | R12 | R14 | R15 | R16 | R17 | R18 | R19 | R20 | R21 | R22 | R23 | R24 - | R25 | R26 | R27 | R28 | R29 | R30 | R31 => Tany32 + | R25 | R26 | R27 | R28 | R29 | R30 | R31 => if Archi.ppc64 then Tany64 else Tany32 | F0 | F1 | F2 | F3 | F4 | F5 | F6 | F7 | F8 | F9 | F10 | F11 | F12 | F13 | F14 | F15 | F16 | F17 | F18 | F19 | F20 | F21 | F22 | F23 @@ -159,11 +159,25 @@ Definition register_by_name (s: string) : option mreg := (** ** Destroyed registers, preferred registers *) +Definition destroyed_by_cond (cond: condition): list mreg := + match cond with + | Ccomplimm _ _ | Ccompluimm _ _ => R12 :: nil + | _ => nil + end. + Definition destroyed_by_op (op: operation): list mreg := match op with | Ofloatconst _ => R12 :: nil | Osingleconst _ => R12 :: nil + | Olongconst _ => R12 :: nil | Ointoffloat | Ointuoffloat => F13 :: nil + | Olongoffloat => F13 :: nil + | Oaddlimm _ => R12 :: nil + | Oandlimm _ => R12 :: nil + | Oorlimm _ => R12 :: nil + | Oxorlimm _ => R12 :: nil + | Orolml _ _ => R12 :: nil + | Ocmp c => destroyed_by_cond c | _ => nil end. @@ -173,9 +187,6 @@ Definition destroyed_by_load (chunk: memory_chunk) (addr: addressing): list mreg Definition destroyed_by_store (chunk: memory_chunk) (addr: addressing): list mreg := R11 :: R12 :: nil. -Definition destroyed_by_cond (cond: condition): list mreg := - nil. - Definition destroyed_by_jumptable: list mreg := R12 :: nil. @@ -239,11 +250,13 @@ Global Opaque (** Two-address operations. Return [true] if the first argument and the result must be in the same location *and* are unconstrained - by [mregs_for_operation]. There is only one: rotate-mask-insert. *) + by [mregs_for_operation]. *) Definition two_address_op (op: operation) : bool := match op with | Oroli _ _ => true + | Olowlong => true + | Ofloatofsingle => true | _ => false end. diff --git a/powerpc/NeedOp.v b/powerpc/NeedOp.v index 956b5d43..9a579cc5 100644 --- a/powerpc/NeedOp.v +++ b/powerpc/NeedOp.v @@ -51,6 +51,11 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | Oshrximm n => op1 (default nv) | Orolm amount mask => op1 (rolm nv amount mask) | Oroli amount mask => op1 (default nv) + | Olongconst n => nil + | Ocast32signed | Ocast32unsigned | Onegl | Onotl => op1 (default nv) + | Oaddl | Osubl | Omull | Omullhs | Omullhu | Odivl | Odivlu | Oandl | Oorl | Oxorl | Oshll | Oshrl | Oshrlu => op2 (default nv) + | Oaddlimm _ | Oandlimm _ | Oorlimm _ | Oxorlimm _ | Oshrlimm _ | Oshrxlimm _=> op1 (default nv) + | Orolml _ _ | Olongoffloat | Ofloatoflong => op1 (default nv) | Onegf | Oabsf => op1 (default nv) | Oaddf | Osubf | Omulf | Odivf => op2 (default nv) | Onegfs | Oabsfs => op1 (default nv) diff --git a/powerpc/Op.v b/powerpc/Op.v index e171c7d4..de4eee48 100644 --- a/powerpc/Op.v +++ b/powerpc/Op.v @@ -35,7 +35,6 @@ Require Import Globalenvs. Require Import Events. Set Implicit Arguments. -Local Transparent Archi.ptr64. (** Conditions (boolean-valued operators). *) @@ -43,11 +42,16 @@ Inductive condition : Type := | Ccomp: comparison -> condition (**r signed integer comparison *) | Ccompu: comparison -> condition (**r unsigned integer comparison *) | Ccompimm: comparison -> int -> condition (**r signed integer comparison with a constant *) - | Ccompuimm: comparison -> int -> condition (**r unsigned integer comparison with a constant *) + | Ccompuimm: comparison -> int -> condition (**r unsigned integer comparison with a constant *) | Ccompf: comparison -> condition (**r floating-point comparison *) | Cnotcompf: comparison -> condition (**r negation of a floating-point comparison *) | Cmaskzero: int -> condition (**r test [(arg & constant) == 0] *) - | Cmasknotzero: int -> condition. (**r test [(arg & constant) != 0] *) + | Cmasknotzero: int -> condition (**r test [(arg & constant) != 0] *) +(*c PPC64 specific conditions: *) + | Ccompl: comparison -> condition (**r signed int64 comparison *) + | Ccomplu: comparison -> condition (**r unsigned int64 comparison *) + | Ccomplimm: comparison -> int64 -> condition (**r signed int64 comparison with a constant *) + | Ccompluimm: comparison -> int64 -> condition. (**r unsigned int64 comparison with a constant *) (** Arithmetic and logical operations. In the descriptions, [rd] is the result of the operation and [r1], [r2], etc, are the arguments. *) @@ -58,7 +62,7 @@ Inductive operation : Type := | Ofloatconst: float -> operation (**r [rd] is set to the given float constant *) | Osingleconst: float32 -> operation (**r [rd] is set to the given float constant *) | Oaddrsymbol: ident -> ptrofs -> operation (**r [rd] is set to the the address of the symbol plus the offset *) - | Oaddrstack: ptrofs -> operation (**r [rd] is set to the stack pointer plus the given offset *) + | Oaddrstack: ptrofs -> operation (**r [rd] is set to the stack pointer plus the given offset *) (*c Integer arithmetic: *) | Ocast8signed: operation (**r [rd] is 8-bit sign extension of [r1] *) | Ocast16signed: operation (**r [rd] is 16-bit sign extension of [r1] *) @@ -92,6 +96,34 @@ Inductive operation : Type := | Oshru: operation (**r [rd = r1 >> r2] (unsigned) *) | Orolm: int -> int -> operation (**r rotate left and mask *) | Oroli: int -> int -> operation (**r rotate left and insert *) +(*c PPC64 64-bit integer arithmetic: *) + | Olongconst: int64 -> operation (**r [rd] is set to the given int64 constant *) + | Ocast32signed: operation (**r [rd] is 64-bit sign extension of [r1] *) + | Ocast32unsigned: operation (**r [rd] is 64-bit zero extension of [r1] *) + | Oaddl: operation (**r [rd = r1 + r2] *) + | Oaddlimm: int64 -> operation (**r [rd = r1 + n] *) + | Osubl: operation (**r [rd = r1 - r2] *) + | Onegl: operation (**r [rd = - r1] *) + | Omull: operation (**r [rd = r1 * r2] *) + | Omullhs: operation (**r [rd = high part of r1 * r2, signed] *) + | Omullhu: operation (**r [rd = high part of r1 * r2, unsigned] *) + | Odivl: operation (**r [rd = r1 / r2] (signed) *) + | Odivlu: operation (**r [rd = r1 / r2] (unsigned) *) + | Oandl: operation (**r [rd = r1 & r2] *) + | Oandlimm: int64 -> operation (**r [rd = r1 & n] *) + | Oorl: operation (**r [rd = r1 | r2] *) + | Oorlimm: int64 -> operation (**r [rd = r1 | n] *) + | Oxorl: operation (**r [rd = r1 ^ r2] *) + | Oxorlimm: int64 -> operation (**r [rd = r1 ^ n] *) + | Onotl: operation (**r [rd = ~r1] *) + | Oshll: operation (**r [rd = r1 << r2] *) + | Oshrl: operation (**r [rd = r1 >> r2] (signed) *) + | Oshrlimm: int -> operation (**r [rd = r1 >> n] (signed) *) + | Oshrxlimm: int -> operation (**r [rd = r1 / 2^n] (signed) *) + | Oshrlu: operation (**r [rd = r1 >> r2] (unsigned) *) + | Orolml: int -> int64 -> operation (**r rotate left and mask *) + | Olongoffloat: operation (**r [rd = signed_int64_of_float(r1)] *) + | Ofloatoflong: operation (**r [rd = float_of_signed_int64(r1)] *) (*c Floating-point arithmetic: *) | Onegf: operation (**r [rd = - r1] *) | Oabsf: operation (**r [rd = abs(r1)] *) @@ -120,27 +152,28 @@ Inductive operation : Type := (*c Boolean tests: *) | Ocmp: condition -> operation. (**r [rd = 1] if condition holds, [rd = 0] otherwise. *) + (** Addressing modes. [r1], [r2], etc, are the arguments to the addressing. *) Inductive addressing: Type := - | Aindexed: int -> addressing (**r Address is [r1 + offset] *) - | Aindexed2: addressing (**r Address is [r1 + r2] *) + | Aindexed: int -> addressing (**r Address is [r1 + offset] *) + | Aindexed2: addressing (**r Address is [r1 + r2] *) | Aglobal: ident -> ptrofs -> addressing (**r Address is [symbol + offset] *) - | Abased: ident -> ptrofs -> addressing (**r Address is [symbol + offset + r1] *) + | Abased: ident -> ptrofs -> addressing (**r Address is [symbol + offset + r1] *) | Ainstack: ptrofs -> addressing. (**r Address is [stack_pointer + offset] *) (** Comparison functions (used in module [CSE]). *) Definition eq_condition (x y: condition) : {x=y} + {x<>y}. Proof. - generalize Int.eq_dec; intro. + generalize Int.eq_dec Int64.eq_dec; intro. assert (forall (x y: comparison), {x=y}+{x<>y}). decide equality. decide equality. Defined. Definition beq_operation: forall (x y: operation), bool. - generalize Int.eq_dec Ptrofs.eq_dec ident_eq Float.eq_dec Float32.eq_dec eq_condition; boolean_equality. + generalize Int.eq_dec Int64.eq_dec Ptrofs.eq_dec ident_eq Float.eq_dec Float32.eq_dec eq_condition; boolean_equality. Defined. Definition eq_operation (x y: operation): {x=y} + {x<>y}. @@ -150,7 +183,7 @@ Defined. Definition eq_addressing (x y: addressing) : {x=y} + {x<>y}. Proof. - generalize Int.eq_dec Ptrofs.eq_dec ident_eq; intro. + generalize Int.eq_dec Int64.eq_dec Ptrofs.eq_dec ident_eq; intro. decide equality. Defined. @@ -173,6 +206,10 @@ Definition eval_condition (cond: condition) (vl: list val) (m: mem): option bool | Cnotcompf c, v1 :: v2 :: nil => option_map negb (Val.cmpf_bool c v1 v2) | Cmaskzero n, v1 :: nil => Val.maskzero_bool v1 n | Cmasknotzero n, v1 :: nil => option_map negb (Val.maskzero_bool v1 n) + | Ccompl c, v1 :: v2 :: nil => Val.cmpl_bool c v1 v2 + | Ccomplu c, v1 :: v2 :: nil => Val.cmplu_bool (Mem.valid_pointer m) c v1 v2 + | Ccomplimm c n, v1 :: nil => Val.cmpl_bool c v1 (Vlong n) + | Ccompluimm c n, v1 :: nil => Val.cmplu_bool (Mem.valid_pointer m) c v1 (Vlong n) | _, _ => None end. @@ -219,6 +256,33 @@ Definition eval_operation | Orolm amount mask, v1::nil => Some (Val.rolm v1 amount mask) | Oroli amount mask, v1::v2::nil => Some(Val.or (Val.and v1 (Vint (Int.not mask))) (Val.rolm v2 amount mask)) + | Olongconst n, nil => Some (Vlong n) + | Ocast32signed, v1::nil => Some (Val.longofint v1) + | Ocast32unsigned, v1::nil => Some (Val.longofintu v1) + | Oaddl, v1::v2::nil => Some (Val.addl v1 v2) + | Oaddlimm n, v1::nil => Some (Val.addl v1 (Vlong n)) + | Osubl, v1::v2::nil => Some (Val.subl v1 v2) + | Onegl, v1::nil => Some (Val.negl v1) + | Omull, v1::v2::nil => Some (Val.mull v1 v2) + | Omullhs, v1::v2::nil => Some (Val.mullhs v1 v2) + | Omullhu, v1::v2::nil => Some (Val.mullhu v1 v2) + | Odivl, v1::v2::nil => Val.divls v1 v2 + | Odivlu, v1::v2::nil => Val.divlu v1 v2 + | Oandl, v1::v2::nil => Some(Val.andl v1 v2) + | Oandlimm n, v1::nil => Some (Val.andl v1 (Vlong n)) + | Oorl, v1::v2::nil => Some(Val.orl v1 v2) + | Oorlimm n, v1::nil => Some (Val.orl v1 (Vlong n)) + | Oxorl, v1::v2::nil => Some(Val.xorl v1 v2) + | Oxorlimm n, v1::nil => Some (Val.xorl v1 (Vlong n)) + | Onotl, v1::nil => Some(Val.notl v1) + | Oshll, v1::v2::nil => Some (Val.shll v1 v2) + | Oshrl, v1::v2::nil => Some (Val.shrl v1 v2) + | Oshrlimm n, v1::nil => Some (Val.shrl v1 (Vint n)) + | Oshrxlimm n, v1::nil => Val.shrxl v1 (Vint n) + | Oshrlu, v1::v2::nil => Some (Val.shrlu v1 v2) + | Orolml amount mask, v1::nil => Some (Val.rolml v1 amount mask) + | Olongoffloat, v1::nil => Val.longoffloat v1 + | Ofloatoflong, v1::nil => Val.floatoflong v1 | Onegf, v1::nil => Some(Val.negf v1) | Oabsf, v1::nil => Some(Val.absf v1) | Oaddf, v1::v2::nil => Some(Val.addf v1 v2) @@ -295,6 +359,10 @@ Definition type_of_condition (c: condition) : list typ := | Cnotcompf _ => Tfloat :: Tfloat :: nil | Cmaskzero _ => Tint :: nil | Cmasknotzero _ => Tint :: nil + | Ccompl _ => Tlong :: Tlong :: nil + | Ccomplu _ => Tlong :: Tlong :: nil + | Ccomplimm _ _ => Tlong :: nil + | Ccompluimm _ _ => Tlong :: nil end. Definition type_of_operation (op: operation) : list typ * typ := @@ -337,6 +405,33 @@ Definition type_of_operation (op: operation) : list typ * typ := | Oshru => (Tint :: Tint :: nil, Tint) | Orolm _ _ => (Tint :: nil, Tint) | Oroli _ _ => (Tint :: Tint :: nil, Tint) + | Olongconst _ => (nil, Tlong) + | Ocast32signed => (Tint :: nil, Tlong) + | Ocast32unsigned => (Tint :: nil, Tlong) + | Oaddl => (Tlong :: Tlong :: nil, Tlong) + | Oaddlimm _ => (Tlong :: nil, Tlong) + | Osubl => (Tlong :: Tlong :: nil, Tlong) + | Onegl => (Tlong :: nil, Tlong) + | Omull => (Tlong :: Tlong :: nil, Tlong) + | Omullhs => (Tlong :: Tlong :: nil, Tlong) + | Omullhu => (Tlong :: Tlong :: nil, Tlong) + | Odivl => (Tlong :: Tlong :: nil, Tlong) + | Odivlu => (Tlong :: Tlong :: nil, Tlong) + | Oandl => (Tlong :: Tlong :: nil, Tlong) + | Oandlimm _ => (Tlong :: nil, Tlong) + | Oorl => (Tlong :: Tlong :: nil, Tlong) + | Oorlimm _ => (Tlong :: nil, Tlong) + | Oxorl => (Tlong :: Tlong :: nil, Tlong) + | Oxorlimm _ => (Tlong :: nil, Tlong) + | Onotl => (Tlong :: nil, Tlong) + | Oshll => (Tlong :: Tint :: nil, Tlong) + | Oshrl => (Tlong :: Tint :: nil, Tlong) + | Oshrlimm _ => (Tlong :: nil, Tlong) + | Oshrxlimm _ => (Tlong :: nil, Tlong) + | Oshrlu => (Tlong :: Tint :: nil, Tlong) + | Orolml _ _ => (Tlong :: nil, Tlong) + | Olongoffloat => (Tfloat :: nil, Tlong) + | Ofloatoflong => (Tlong :: nil, Tfloat) | Onegf => (Tfloat :: nil, Tfloat) | Oabsf => (Tfloat :: nil, Tfloat) | Oaddf => (Tfloat :: Tfloat :: nil, Tfloat) @@ -428,6 +523,35 @@ Proof with (try exact I; try reflexivity). destruct v0; destruct v1; simpl... destruct (Int.ltu i0 Int.iwordsize)... destruct v0... destruct v0; destruct v1... + exact I. + destruct v0... + destruct v0... + destruct v0; destruct v1... + destruct v0... + destruct v0; destruct v1... + destruct v0... + destruct v0; destruct v1... + destruct v0; destruct v1... + destruct v0; destruct v1... + destruct v0; destruct v1; simpl in *; inv H0. + destruct (Int64.eq i0 Int64.zero + || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq i0 Int64.mone); inv H2... + destruct v0; destruct v1; simpl in *; inv H0. destruct (Int64.eq i0 Int64.zero); inv H2... + destruct v0; destruct v1... + destruct v0... + destruct v0; destruct v1... + destruct v0... + destruct v0; destruct v1... + destruct v0... + destruct v0... + destruct v0; destruct v1; simpl... destruct (Int.ltu i0 Int64.iwordsize')... + destruct v0; destruct v1; simpl... destruct (Int.ltu i0 Int64.iwordsize')... + destruct v0; simpl... destruct (Int.ltu i Int64.iwordsize')... + destruct v0; simpl in *; inv H0. destruct (Int.ltu i (Int.repr 63)); inv H2... + destruct v0; destruct v1; simpl... destruct (Int.ltu i0 Int64.iwordsize')... + destruct v0... + destruct v0; simpl in H0; inv H0. destruct (Float.to_long f); inv H2... + destruct v0; simpl in H0; inv H0... destruct v0... destruct v0... destruct v0; destruct v1... @@ -491,6 +615,10 @@ Definition negate_condition (cond: condition): condition := | Cnotcompf c => Ccompf c | Cmaskzero n => Cmasknotzero n | Cmasknotzero n => Cmaskzero n + | Ccompl c => Ccompl(negate_comparison c) + | Ccomplu c => Ccomplu(negate_comparison c) + | Ccomplimm c n => Ccomplimm (negate_comparison c) n + | Ccompluimm c n => Ccompluimm (negate_comparison c) n end. Lemma eval_negate_condition: @@ -506,6 +634,10 @@ Proof. repeat (destruct vl; auto). destruct (Val.cmpf_bool c v v0); auto. destruct b; auto. repeat (destruct vl; auto). repeat (destruct vl; auto). destruct (Val.maskzero_bool v i) as [[]|]; auto. + repeat (destruct vl; auto). apply Val.negate_cmpl_bool. + repeat (destruct vl; auto). apply Val.negate_cmplu_bool. + repeat (destruct vl; auto). apply Val.negate_cmpl_bool. + repeat (destruct vl; auto). apply Val.negate_cmplu_bool. Qed. (** Shifting stack-relative references. This is used in [Stacking]. *) @@ -571,7 +703,7 @@ Lemma eval_offset_addressing: eval_addressing ge sp addr args = Some v -> eval_addressing ge sp addr' args = Some(Val.add v (Vint (Int.repr delta))). Proof. - intros. + intros. assert (D: Ptrofs.repr delta = Ptrofs.of_int (Int.repr delta)) by (symmetry; auto with ptrofs). destruct addr; simpl in H; inv H; simpl in *; FuncInv; subst. - rewrite Val.add_assoc; auto. @@ -599,6 +731,8 @@ Definition op_depends_on_memory (op: operation) : bool := match op with | Ocmp (Ccompu _) => true | Ocmp (Ccompuimm _ _) => true + | Ocmp (Ccomplu _) => Archi.ppc64 + | Ocmp (Ccompluimm _ _) => Archi.ppc64 | _ => false end. @@ -736,6 +870,10 @@ Proof. inv H3; inv H2; simpl in H0; inv H0; auto. inv H3; try discriminate; auto. inv H3; try discriminate; auto. + inv H3; inv H2; simpl in H0; inv H0; auto. + inv H3; inv H2; simpl in H0; inv H0; auto. + inv H3; try discriminate; auto. + inv H3; try discriminate; auto. Qed. Ltac TrivialExists := @@ -773,7 +911,7 @@ Proof. destruct (Int.eq i0 Int.zero || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H2. TrivialExists. inv H4; inv H3; simpl in H1; inv H1. simpl. - destruct (Int.eq i0 Int.zero); inv H2. TrivialExists. + destruct (Int.eq i0 Int.zero); inv H2. TrivialExists. inv H4; inv H2; simpl; auto. inv H4; simpl; auto. inv H4; inv H2; simpl; auto. @@ -796,6 +934,36 @@ Proof. inv H4; simpl; auto. inv H4; simpl; auto. inv H4; inv H2; simpl; auto. + inv H4; simpl; auto. + inv H4; inv H2; simpl; auto. + inv H4; simpl; auto. + inv H4; inv H2; simpl; auto. + inv H4; inv H2; simpl; auto. + inv H4; inv H2; simpl; auto. + inv H4; inv H3; simpl in H1; inv H1. simpl. + destruct (Int64.eq i0 Int64.zero + || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq i0 Int64.mone); inv H2. TrivialExists. + inv H4; inv H3; simpl in H1; inv H1. simpl. + destruct (Int64.eq i0 Int64.zero); inv H2. TrivialExists. + inv H4; inv H2; simpl; auto. + inv H4; simpl; auto. + inv H4; inv H2; simpl; auto. + inv H4; simpl; auto. + inv H4; inv H2; simpl; auto. + inv H4; simpl; auto. + inv H4; simpl; auto. + inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int64.iwordsize'); auto. + inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int64.iwordsize'); auto. + inv H4; simpl; auto. destruct (Int.ltu i Int64.iwordsize'); auto. + inv H4; simpl in *; inv H1. destruct (Int.ltu i (Int.repr 63)); inv H2. econstructor; eauto. + inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int64.iwordsize'); auto. + inv H4; simpl; auto. + inv H4; simpl in H1; inv H1. simpl. destruct (Float.to_long f0); simpl in H2; inv H2. + exists (Vlong i); auto. + inv H4; simpl in H1; inv H1; simpl. TrivialExists. + inv H4; simpl; auto. + inv H4; simpl; auto. + inv H4; inv H2; simpl; auto. inv H4; inv H2; simpl; auto. inv H4; inv H2; simpl; auto. inv H4; inv H2; simpl; auto. @@ -993,7 +1161,7 @@ Proof. rewrite eval_shift_stack_addressing. eapply eval_addressing_inj with (sp1 := Vptr sp1 Ptrofs.zero); eauto. intros. apply symbol_address_inject. - econstructor; eauto. rewrite Ptrofs.add_zero_l; auto. + econstructor; eauto. rewrite Ptrofs.add_zero_l; auto. Qed. Lemma eval_operation_inject: @@ -1013,7 +1181,7 @@ Proof. intros; eapply Mem.weak_valid_pointer_inject_no_overflow; eauto. intros; eapply Mem.different_pointers_inject; eauto. intros. apply symbol_address_inject. - econstructor; eauto. rewrite Ptrofs.add_zero_l; auto. + econstructor; eauto. rewrite Ptrofs.add_zero_l; auto. Qed. End EVAL_INJECT. @@ -1042,14 +1210,14 @@ End EVAL_INJECT. *) Inductive rlw_state: Type := - | RLW_S0 : rlw_state - | RLW_S1 : rlw_state - | RLW_S2 : rlw_state - | RLW_S3 : rlw_state - | RLW_S4 : rlw_state - | RLW_S5 : rlw_state - | RLW_S6 : rlw_state - | RLW_Sbad : rlw_state. + | RLW_S0 + | RLW_S1 + | RLW_S2 + | RLW_S3 + | RLW_S4 + | RLW_S5 + | RLW_S6 + | RLW_Sbad. Definition rlw_transition (s: rlw_state) (b: bool) : rlw_state := match s, b with @@ -1082,13 +1250,71 @@ Definition rlw_accepting (s: rlw_state) : bool := | RLW_Sbad => false end. -Fixpoint is_rlw_mask_rec (n: nat) (s: rlw_state) (x: Z) {struct n} : bool := +Fixpoint is_mask_rec {A: Type} (trans: A -> bool -> A) (accept: A -> bool) + (n: nat) (s: A) (x: Z) {struct n} : bool := match n with | O => - rlw_accepting s + accept s | S m => - is_rlw_mask_rec m (rlw_transition s (Z.odd x)) (Z.div2 x) + is_mask_rec trans accept m (trans s (Z.odd x)) (Z.div2 x) end. Definition is_rlw_mask (x: int) : bool := - is_rlw_mask_rec Int.wordsize RLW_S0 (Int.unsigned x). + is_mask_rec rlw_transition rlw_accepting Int.wordsize RLW_S0 (Int.unsigned x). + +(** For the 64-bit [rldicl] and [rldicr] instructions, the acceptable + masks are [1111100000] and [0000011111], that is, some ones in the + high bits and some zeroes in the low bits, or conversely. All ones + is OK, but not all zeroes. The corresponding automata are: +<< + 0 1 + / \ / \ + \ / \ / (accepting: [1]) + [0] --1--> [1] + + + 1 0 + / \ / \ + \ / \ / (accepting: [1], [2]) + [0] --1--> [1] --0--> [2] +>> +*) + +Inductive rll_state: Type := RLL_S0 | RLL_S1 | RLL_Sbad. + +Definition rll_transition (s: rll_state) (b: bool) : rll_state := + match s, b with + | RLL_S0, false => RLL_S0 + | RLL_S0, true => RLL_S1 + | RLL_S1, true => RLL_S1 + | _, _ => RLL_Sbad + end. + +Definition rll_accepting (s: rll_state) : bool := + match s with + | RLL_S1 => true + | _ => false + end. + +Inductive rlr_state: Type := RLR_S0 | RLR_S1 | RLR_S2 | RLR_Sbad. + +Definition rlr_transition (s: rlr_state) (b: bool) : rlr_state := + match s, b with + | RLR_S0, true => RLR_S1 + | RLR_S1, false => RLR_S2 + | RLR_S1, true => RLR_S1 + | RLR_S2, false => RLR_S2 + | _, _ => RLR_Sbad + end. + +Definition rlr_accepting (s: rlr_state) : bool := + match s with + | RLR_S1 | RLR_S2 => true + | _ => false + end. + +Definition is_rldl_mask (x: int64) : bool := (*r 0s in the high bits, 1s in the low bits *) + is_mask_rec rll_transition rll_accepting Int64.wordsize RLL_S0 (Int64.unsigned x). + +Definition is_rldr_mask (x: int64) : bool := (*r 1s in the high bits, 0s in the low bits *) + is_mask_rec rlr_transition rlr_accepting Int64.wordsize RLR_S0 (Int64.unsigned x). diff --git a/powerpc/PrintOp.ml b/powerpc/PrintOp.ml index a3fac2c3..cffaafdb 100644 --- a/powerpc/PrintOp.ml +++ b/powerpc/PrintOp.ml @@ -110,6 +110,32 @@ let print_operation reg pp = function | Olowlong, [r1] -> fprintf pp "lowlong(%a)" reg r1 | Ohighlong, [r1] -> fprintf pp "highlong(%a)" reg r1 | Ocmp c, args -> print_condition reg pp (c, args) + | Olongconst n, [] -> fprintf pp "%LdL" (camlint64_of_coqint n) + | Ocast32signed, [r1] -> fprintf pp "int32signed(%a)" reg r1 + | Ocast32unsigned, [r1] -> fprintf pp "int32unsigned(%a)" reg r1 + | Oaddl, [r1;r2] -> fprintf pp "%a +l %a" reg r1 reg r2 + | Oaddlimm n, [r1] -> fprintf pp "%a +l %Ld" reg r1 (camlint64_of_coqint n) + | Osubl, [r1;r2] -> fprintf pp "%a -l %a" reg r1 reg r2 + | Onegl, [r1] -> fprintf pp "-l %a" reg r1 + | Omull, [r1;r2] -> fprintf pp "%a *l %a" reg r1 reg r2 + | Odivl, [r1;r2] -> fprintf pp "%a /ls %a" reg r1 reg r2 + | Odivlu, [r1;r2] -> fprintf pp "%a /lu %a" reg r1 reg r2 + | Oandl, [r1;r2] -> fprintf pp "%a &l %a" reg r1 reg r2 + | Oandlimm n, [r1] -> fprintf pp "%a &l %Ld" reg r1 (camlint64_of_coqint n) + | Oorl, [r1;r2] -> fprintf pp "%a |l %a" reg r1 reg r2 + | Oorlimm n, [r1] -> fprintf pp "%a |l %Ld" reg r1 (camlint64_of_coqint n) + | Oxorl, [r1;r2] -> fprintf pp "%a ^l %a" reg r1 reg r2 + | Oxorlimm n, [r1] -> fprintf pp "%a ^l %Ld" reg r1 (camlint64_of_coqint n) + | Onotl, [r1] -> fprintf pp "~l %a" reg r1 + | Oshll, [r1;r2] -> fprintf pp "%a <<l %a" reg r1 reg r2 + | Oshrl, [r1;r2] -> fprintf pp "%a >>ls %a" reg r1 reg r2 + | Oshrlimm n, [r1] -> fprintf pp "%a >>ls %ld" reg r1 (camlint_of_coqint n) + | Oshrlu, [r1;r2] -> fprintf pp "%a >>lu %a" reg r1 reg r2 + | Orolml(n,m), [r1] -> + fprintf pp "(%a rol %Ld) &l 0x%Lx" + reg r1 (camlint64_of_coqint n) (camlint64_of_coqint m) + | Olongoffloat, [r1] -> fprintf pp "longoffloat(%a)" reg r1 + | Ofloatoflong, [r1] -> fprintf pp "floatoflong(%a)" reg r1 | _ -> fprintf pp "<bad operator>" let print_addressing reg pp = function diff --git a/powerpc/SelectLong.vp b/powerpc/SelectLong.vp index cc7a38f6..5f13774b 100644 --- a/powerpc/SelectLong.vp +++ b/powerpc/SelectLong.vp @@ -18,4 +18,337 @@ Require Import AST Integers Floats. Require Import Op CminorSel. Require Import SelectOp SplitLong. -(** This file is empty because we use the default implementation provided in [SplitLong]. *) +Local Open Scope cminorsel_scope. +Local Open Scope string_scope. + +Section SELECT. + +Context {hf: helper_functions}. + +Definition longconst (n: int64) : expr := + if Archi.splitlong then SplitLong.longconst n else Eop (Olongconst n) Enil. + +Definition is_longconst (e: expr) := + if Archi.splitlong then SplitLong.is_longconst e else + match e with + | Eop (Olongconst n) Enil => Some n + | _ => None + end. + +Definition intoflong (e: expr) := + if Archi.splitlong then SplitLong.intoflong e else + match is_longconst e with + | Some n => Eop (Ointconst (Int.repr (Int64.unsigned n))) Enil + | None => Eop Olowlong (e ::: Enil) + end. + +Definition longofint (e: expr) := + if Archi.splitlong then SplitLong.longofint e else + match is_intconst e with + | Some n => longconst (Int64.repr (Int.signed n)) + | None => Eop Ocast32signed (e ::: Enil) + end. + +Definition longofintu (e: expr) := + if Archi.splitlong then SplitLong.longofintu e else + match is_intconst e with + | Some n => longconst (Int64.repr (Int.unsigned n)) + | None => Eop Ocast32unsigned (e ::: Enil) + end. + +Nondetfunction notl (e: expr) := + if Archi.splitlong then SplitLong.notl e else + match e with + | Eop (Olongconst n) Enil => longconst (Int64.not n) + | Eop Onotl (t1:::Enil) => t1 + | _ => Eop Onotl (e:::Enil) + end. + +Nondetfunction andlimm (n1: int64) (e2: expr) := + if Int64.eq n1 Int64.zero then longconst Int64.zero else + if Int64.eq n1 Int64.mone then e2 else + match e2 with + | Eop (Olongconst n2) Enil => + longconst (Int64.and n1 n2) + | Eop (Oandlimm n2) (t2:::Enil) => + Eop (Oandlimm (Int64.and n1 n2)) (t2:::Enil) + | Eop (Orolml amount2 mask2) (t2:::Enil) => + Eop (Orolml amount2 (Int64.and n1 mask2)) (t2:::Enil) + | _ => + Eop (Oandlimm n1) (e2:::Enil) + end. + +Nondetfunction andl (e1: expr) (e2: expr) := + if Archi.splitlong then SplitLong.andl e1 e2 else + match e1, e2 with + | Eop (Olongconst n1) Enil, t2 => andlimm n1 t2 + | t1, Eop (Olongconst n2) Enil => andlimm n2 t1 + | _, _ => Eop Oandl (e1:::e2:::Enil) + end. + +Nondetfunction orlimm (n1: int64) (e2: expr) := + if Int64.eq n1 Int64.zero then e2 else + if Int64.eq n1 Int64.mone then longconst Int64.mone else + match e2 with + | Eop (Olongconst n2) Enil => longconst (Int64.or n1 n2) + | Eop (Oorlimm n2) (t2:::Enil) => Eop (Oorlimm (Int64.or n1 n2)) (t2:::Enil) + | _ => Eop (Oorlimm n1) (e2:::Enil) + end. + +Nondetfunction orl (e1: expr) (e2: expr) := + if Archi.splitlong then SplitLong.orl e1 e2 else + match e1, e2 with + | Eop (Orolml amount1 mask1) (t1:::Enil), Eop (Orolml amount2 mask2) (t2:::Enil) => + if Int.eq amount1 amount2 && same_expr_pure t1 t2 + then Eop (Orolml amount1 (Int64.or mask1 mask2)) (t1:::Enil) + else Eop Oorl (e1:::e2:::Enil) + | Eop (Olongconst n1) Enil, t2 => orlimm n1 t2 + | t1, Eop (Olongconst n2) Enil => orlimm n2 t1 + | _, _ => Eop Oorl (e1:::e2:::Enil) + end. + +Nondetfunction xorlimm (n1: int64) (e2: expr) := + if Int64.eq n1 Int64.zero then e2 else + if Int64.eq n1 Int64.mone then notl e2 else + match e2 with + | Eop (Olongconst n2) Enil => longconst (Int64.xor n1 n2) + | Eop (Oxorlimm n2) (t2:::Enil) => Eop (Oxorlimm (Int64.xor n1 n2)) (t2:::Enil) + | Eop Onotl (t2:::Enil) => Eop (Oxorlimm (Int64.not n1)) (t2:::Enil) + | _ => Eop (Oxorlimm n1) (e2:::Enil) + end. + +Nondetfunction xorl (e1: expr) (e2: expr) := + if Archi.splitlong then SplitLong.xorl e1 e2 else + match e1, e2 with + | Eop (Olongconst n1) Enil, t2 => xorlimm n1 t2 + | t1, Eop (Olongconst n2) Enil => xorlimm n2 t1 + | _, _ => Eop Oxorl (e1:::e2:::Enil) + end. + +Nondetfunction rolml (e1: expr) (amount2: int) (mask2: int64) := + if Int.eq amount2 Int.zero then andlimm mask2 e1 else + match e1 with + | Eop (Olongconst n1) Enil => + longconst (Int64.and (Int64.rol' n1 amount2) mask2) + | Eop (Orolml amount1 mask1) (t1:::Enil) => + Eop (Orolml (Int.modu (Int.add amount1 amount2) Int64.iwordsize') + (Int64.and (Int64.rol' mask1 amount2) mask2)) + (t1:::Enil) + | Eop (Oandlimm mask1) (t1:::Enil) => + Eop (Orolml amount2 + (Int64.and (Int64.rol' mask1 amount2) mask2)) + (t1:::Enil) + | _ => + Eop (Orolml amount2 mask2) (e1:::Enil) + end. + +Definition shllimm (e1: expr) (n: int) := + if Archi.splitlong then SplitLong.shllimm e1 n else + if Int.eq n Int.zero then e1 else + if negb (Int.ltu n Int64.iwordsize') then + Eop Oshll (e1:::Eop (Ointconst n) Enil:::Enil) + else + let n' := Int64.repr (Int.unsigned n) in + rolml e1 n (Int64.shl Int64.mone n'). + +Definition shrluimm (e1: expr) (n: int) := + if Archi.splitlong then SplitLong.shrluimm e1 n else + if Int.eq n Int.zero then e1 else + if negb (Int.ltu n Int64.iwordsize') then + Eop Oshrlu (e1:::Eop (Ointconst n) Enil:::Enil) + else + let n' := Int64.repr (Int.unsigned n) in + rolml e1 (Int.sub Int64.iwordsize' n) (Int64.shru Int64.mone n'). + +Nondetfunction shrlimm (e1: expr) (n: int) := + if Archi.splitlong then SplitLong.shrlimm e1 n else + if Int.eq n Int.zero then e1 else + if negb (Int.ltu n Int64.iwordsize') then + Eop Oshrl (e1:::Eop (Ointconst n) Enil:::Enil) + else + match e1 with + | Eop (Olongconst n1) Enil => + Eop (Olongconst(Int64.shr' n1 n)) Enil + | Eop (Oshrlimm n1) (t1:::Enil) => + if Int.ltu (Int.add n n1) Int64.iwordsize' + then Eop (Oshrlimm (Int.add n n1)) (t1:::Enil) + else Eop (Oshrlimm n) (e1:::Enil) + | _ => + Eop (Oshrlimm n) (e1:::Enil) + end. + +Definition shll (e1: expr) (e2: expr) := + if Archi.splitlong then SplitLong.shll e1 e2 else + match is_intconst e2 with + | Some n2 => shllimm e1 n2 + | None => Eop Oshll (e1:::e2:::Enil) + end. + +Definition shrl (e1: expr) (e2: expr) := + if Archi.splitlong then SplitLong.shrl e1 e2 else + match is_intconst e2 with + | Some n2 => shrlimm e1 n2 + | None => Eop Oshrl (e1:::e2:::Enil) + end. + +Definition shrlu (e1: expr) (e2: expr) := + if Archi.splitlong then SplitLong.shrlu e1 e2 else + match is_intconst e2 with + | Some n2 => shrluimm e1 n2 + | _ => Eop Oshrlu (e1:::e2:::Enil) + end. + +Nondetfunction addlimm (n: int64) (e: expr) := + if Int64.eq n Int64.zero then e else + match e with + | Eop (Olongconst m) Enil => longconst (Int64.add m n) + | Eop (Oaddlimm m) (t ::: Enil) => Eop (Oaddlimm(Int64.add m n)) (t ::: Enil) + | _ => Eop (Oaddlimm n) (e ::: Enil) + end. + +Nondetfunction addl (e1: expr) (e2: expr) := + if Archi.splitlong then SplitLong.addl e1 e2 else + match e1, e2 with + | Eop (Olongconst n1) Enil, t2 => addlimm n1 t2 + | t1, Eop (Olongconst n2) Enil => addlimm n2 t1 + | Eop (Oaddlimm n1) (t1:::Enil), Eop (Oaddlimm n2) (t2:::Enil) => + addlimm (Int64.add n1 n2) (Eop Oaddl (t1:::t2:::Enil)) + | Eop (Oaddlimm n1) (t1:::Enil), t2 => + addlimm n1 (Eop Oaddl (t1:::t2:::Enil)) + | t1, Eop (Oaddlimm n2) (t2:::Enil) => + addlimm n2 (Eop Oaddl (t1:::t2:::Enil)) + | _, _ => + Eop Oaddl (e1:::e2:::Enil) + end. + +Definition negl (e: expr) := + if Archi.splitlong then SplitLong.negl e else + match is_longconst e with + | Some n => longconst (Int64.neg n) + | None => Eop Onegl (e ::: Enil) + end. + +Nondetfunction subl (e1: expr) (e2: expr) := + if Archi.splitlong then SplitLong.subl e1 e2 else + match e1, e2 with + | t1, Eop (Olongconst n2) Enil => addlimm (Int64.neg n2) t1 + | _, _ => + Eop Osubl (e1:::e2:::Enil) + end. + +Definition mullimm_base (n1: int64) (e2: expr) := + match Int64.one_bits' n1 with + | i :: nil => + shllimm e2 i + | i :: j :: nil => + Elet e2 (addl (shllimm (Eletvar 0) i) (shllimm (Eletvar 0) j)) + | _ => + Eop Omull (e2:::longconst n1:::Enil) + end. + +Nondetfunction mullimm (n1: int64) (e2: expr) := + if Archi.splitlong then SplitLong.mullimm n1 e2 + else if Int64.eq n1 Int64.zero then longconst Int64.zero + else if Int64.eq n1 Int64.one then e2 + else match e2 with + | Eop (Olongconst n2) Enil => longconst (Int64.mul n1 n2) + | _ => mullimm_base n1 e2 + end. + +Nondetfunction mull (e1: expr) (e2: expr) := + if Archi.splitlong then SplitLong.mull e1 e2 else + match e1, e2 with + | Eop (Olongconst n1) Enil, t2 => mullimm n1 t2 + | t1, Eop (Olongconst n2) Enil => mullimm n2 t1 + | _, _ => Eop Omull (e1:::e2:::Enil) + end. + +Definition mullhu (e1: expr) (n2: int64) := + if Archi.splitlong then SplitLong.mullhu e1 n2 else + Eop Omullhu (e1 ::: longconst n2 ::: Enil). + +Definition mullhs (e1: expr) (n2: int64) := + if Archi.splitlong then SplitLong.mullhs e1 n2 else + Eop Omullhs (e1 ::: longconst n2 ::: Enil). + +Definition shrxlimm (e: expr) (n: int) := + if Archi.splitlong then SplitLong.shrxlimm e n else + if Int.eq n Int.zero then e else Eop (Oshrxlimm n) (e ::: Enil). + + +Definition modl_aux (divop: operation) (e1 e2: expr) := + Elet e1 + (Elet (lift e2) + (Eop Osubl (Eletvar 1 ::: + Eop Omull (Eop divop (Eletvar 1 ::: Eletvar 0 ::: Enil) ::: + Eletvar 0 ::: + Enil) ::: + Enil))). + +Definition divls_base (e1: expr) (e2: expr) := + if Archi.splitlong then SplitLong.divls_base e1 e2 else Eop Odivl (e1:::e2:::Enil). + +Definition divlu_base (e1: expr) (e2: expr) := + if Archi.splitlong then SplitLong.divlu_base e1 e2 else Eop Odivlu (e1:::e2:::Enil). + +Definition modls_base (e1: expr) (e2: expr) := + if Archi.splitlong then SplitLong.modls_base e1 e2 else + let default := modl_aux Odivl e1 e2 in + match is_longconst e1, is_longconst e2 with + | Some n1, Some n2 => + if Int64.eq Int64.zero n2 then default else + if Int64.eq n1 (Int64.repr Int64.min_signed) && Int64.eq n2 Int64.mone then default + else longconst (Int64.mods n1 n2) + | _, _ => default + end. + +Definition modlu_base (e1 e2: expr) := + if Archi.splitlong then SplitLong.modlu_base e1 e2 else + let default := modl_aux Odivlu e1 e2 in + match is_longconst e1, is_longconst e2 with + | Some n1, Some n2 => + if Int64.eq Int64.zero n2 + then default + else longconst (Int64.modu n1 n2) + | _, Some n2 => + match Int64.is_power2 n2 with + | Some _ => andlimm (Int64.sub n2 Int64.one) e1 + | _ => default + end + | _, _ => default + end. + +Definition cmplu (c: comparison) (e1 e2: expr) := + if Archi.splitlong then SplitLong.cmplu c e1 e2 else + match is_longconst e1, is_longconst e2 with + | Some n1, Some n2 => + Eop (Ointconst (if Int64.cmpu c n1 n2 then Int.one else Int.zero)) Enil + | Some n1, None => Eop (Ocmp (Ccompluimm (swap_comparison c) n1)) (e2:::Enil) + | None, Some n2 => Eop (Ocmp (Ccompluimm c n2)) (e1:::Enil) + | None, None => Eop (Ocmp (Ccomplu c)) (e1:::e2:::Enil) + end. + +Definition cmpl (c: comparison) (e1 e2: expr) := + if Archi.splitlong then SplitLong.cmpl c e1 e2 else + match is_longconst e1, is_longconst e2 with + | Some n1, Some n2 => + Eop (Ointconst (if Int64.cmp c n1 n2 then Int.one else Int.zero)) Enil + | Some n1, None => Eop (Ocmp (Ccomplimm (swap_comparison c) n1)) (e2:::Enil) + | None, Some n2 => Eop (Ocmp (Ccomplimm c n2)) (e1:::Enil) + | None, None => Eop (Ocmp (Ccompl c)) (e1:::e2:::Enil) + end. + +Definition longoffloat (e: expr) := + if Archi.splitlong + then SplitLong.longoffloat e + else Eop Olongoffloat (e:::Enil). + +Definition floatoflong (e: expr) := + if Archi.splitlong + then SplitLong.floatoflong e + else Eop Ofloatoflong (e:::Enil). + +Definition longofsingle (arg: expr) := + longoffloat (floatofsingle arg). + +End SELECT. diff --git a/powerpc/SelectLongproof.v b/powerpc/SelectLongproof.v index a82c082c..3e5e82d3 100644 --- a/powerpc/SelectLongproof.v +++ b/powerpc/SelectLongproof.v @@ -10,7 +10,7 @@ (* *) (* *********************************************************************) -(** Instruction selection for 64-bit integer operations *) +(** Correctness of instruction selection for 64-bit integer operations *) Require Import String Coqlib Maps Integers Floats Errors. Require Archi. @@ -19,4 +19,625 @@ Require Import Cminor Op CminorSel. Require Import SelectOp SelectOpproof SplitLong SplitLongproof. Require Import SelectLong. -(** This file is empty because we use the default implementation provided in [SplitLong]. *) +Local Open Scope cminorsel_scope. +Local Open Scope string_scope. + +(** * Correctness of the instruction selection functions for 64-bit operators *) + +Section CMCONSTR. + +Variable prog: program. +Variable hf: helper_functions. +Hypothesis HELPERS: helper_functions_declared prog hf. +Let ge := Genv.globalenv prog. +Variable sp: val. +Variable e: env. +Variable m: mem. + +Definition unary_constructor_sound (cstr: expr -> expr) (sem: val -> val) : Prop := + forall le a x, + eval_expr ge sp e m le a x -> + exists v, eval_expr ge sp e m le (cstr a) v /\ Val.lessdef (sem x) v. + +Definition binary_constructor_sound (cstr: expr -> expr -> expr) (sem: val -> val -> val) : Prop := + forall le a x b y, + eval_expr ge sp e m le a x -> + eval_expr ge sp e m le b y -> + exists v, eval_expr ge sp e m le (cstr a b) v /\ Val.lessdef (sem x y) v. + +Definition partial_unary_constructor_sound (cstr: expr -> expr) (sem: val -> option val) : Prop := + forall le a x y, + eval_expr ge sp e m le a x -> + sem x = Some y -> + exists v, eval_expr ge sp e m le (cstr a) v /\ Val.lessdef y v. + +Definition partial_binary_constructor_sound (cstr: expr -> expr -> expr) (sem: val -> val -> option val) : Prop := + forall le a x b y z, + eval_expr ge sp e m le a x -> + eval_expr ge sp e m le b y -> + sem x y = Some z -> + exists v, eval_expr ge sp e m le (cstr a b) v /\ Val.lessdef z v. + +Theorem eval_longconst: + forall le n, eval_expr ge sp e m le (longconst n) (Vlong n). +Proof. + unfold longconst; intros; destruct Archi.splitlong. + apply SplitLongproof.eval_longconst. + EvalOp. +Qed. + +Lemma is_longconst_sound: + forall v a n le, + is_longconst a = Some n -> eval_expr ge sp e m le a v -> v = Vlong n. +Proof with (try discriminate). + intros. unfold is_longconst in *. destruct Archi.splitlong. + eapply SplitLongproof.is_longconst_sound; eauto. + assert (a = Eop (Olongconst n) Enil). + { destruct a... destruct o... destruct e0... congruence. } + subst a. InvEval. auto. +Qed. + +Theorem eval_intoflong: unary_constructor_sound intoflong Val.loword. +Proof. + unfold intoflong; destruct Archi.splitlong. apply SplitLongproof.eval_intoflong. + red; intros. destruct (is_longconst a) as [n|] eqn:C. +- TrivialExists. simpl. erewrite (is_longconst_sound x) by eauto. auto. +- TrivialExists. +Qed. + +Theorem eval_longofintu: unary_constructor_sound longofintu Val.longofintu. +Proof. + unfold longofintu; destruct Archi.splitlong. apply SplitLongproof.eval_longofintu. + red; intros. destruct (is_intconst a) as [n|] eqn:C. +- econstructor; split. apply eval_longconst. + exploit is_intconst_sound; eauto. intros; subst x. auto. +- TrivialExists. +Qed. + +Theorem eval_longofint: unary_constructor_sound longofint Val.longofint. +Proof. + unfold longofint; destruct Archi.splitlong. apply SplitLongproof.eval_longofint. + red; intros. destruct (is_intconst a) as [n|] eqn:C. +- econstructor; split. apply eval_longconst. + exploit is_intconst_sound; eauto. intros; subst x. auto. +- TrivialExists. +Qed. + +Theorem eval_notl: unary_constructor_sound notl Val.notl. +Proof. + unfold notl; destruct Archi.splitlong. apply SplitLongproof.eval_notl. + red; intros. destruct (notl_match a). +- InvEval. econstructor; split. apply eval_longconst. auto. +- InvEval. subst. exists v1; split; auto. destruct v1; simpl; auto. rewrite Int64.not_involutive; auto. +- TrivialExists. +Qed. + +Theorem eval_andlimm: forall n, unary_constructor_sound (andlimm n) (fun v => Val.andl v (Vlong n)). +Proof. + unfold andlimm; intros; red; intros. + predSpec Int64.eq Int64.eq_spec n Int64.zero. + exists (Vlong Int64.zero); split. apply eval_longconst. + subst. destruct x; simpl; auto. rewrite Int64.and_zero; auto. + predSpec Int64.eq Int64.eq_spec n Int64.mone. + exists x; split. assumption. + subst. destruct x; simpl; auto. rewrite Int64.and_mone; auto. + destruct (andlimm_match a); InvEval; subst. +- econstructor; split. apply eval_longconst. simpl. rewrite Int64.and_commut; auto. +- TrivialExists. simpl. rewrite Val.andl_assoc. rewrite Int64.and_commut; auto. +- TrivialExists. simpl. destruct v1; simpl; auto. unfold Int64.rolm. rewrite Int64.and_assoc. + rewrite (Int64.and_commut mask2 n). reflexivity. +- TrivialExists. +Qed. + +Theorem eval_andl: binary_constructor_sound andl Val.andl. +Proof. + unfold andl; destruct Archi.splitlong. apply SplitLongproof.eval_andl. + red; intros. destruct (andl_match a b). +- InvEval. rewrite Val.andl_commut. apply eval_andlimm; auto. +- InvEval. apply eval_andlimm; auto. +- TrivialExists. +Qed. + +Theorem eval_orlimm: forall n, unary_constructor_sound (orlimm n) (fun v => Val.orl v (Vlong n)). +Proof. + unfold orlimm; intros; red; intros. + predSpec Int64.eq Int64.eq_spec n Int64.zero. + exists x; split; auto. subst. destruct x; simpl; auto. rewrite Int64.or_zero; auto. + predSpec Int64.eq Int64.eq_spec n Int64.mone. + econstructor; split. apply eval_longconst. subst. destruct x; simpl; auto. rewrite Int64.or_mone; auto. + destruct (orlimm_match a); InvEval; subst. +- econstructor; split. apply eval_longconst. simpl. rewrite Int64.or_commut; auto. +- TrivialExists. simpl. rewrite Val.orl_assoc. rewrite Int64.or_commut; auto. +- TrivialExists. +Qed. + +Theorem eval_orl: binary_constructor_sound orl Val.orl. +Proof. + unfold orl; destruct Archi.splitlong. apply SplitLongproof.eval_orl. + red; intros. + assert (DEFAULT: exists v, eval_expr ge sp e m le (Eop Oorl (a:::b:::Enil)) v /\ Val.lessdef (Val.orl x y) v) by TrivialExists. + assert (ROLM: forall v n1 n2 m1 m2, + n1 = n2 -> + Val.lessdef (Val.orl (Val.rolml v n1 m1) (Val.rolml v n2 m2)) + (Val.rolml v n1 (Int64.or m1 m2))). + { intros. destruct v; simpl; auto. unfold Int64.rolm. + rewrite Int64.and_or_distrib. rewrite H1. auto. } + destruct (orl_match a b). +- predSpec Int.eq Int.eq_spec amount1 amount2; simpl. + destruct (same_expr_pure t1 t2) eqn:?; auto. InvEval. + exploit eval_same_expr; eauto. intros [EQ1 EQ2]; subst. + exists (Val.rolml v0 amount2 (Int64.or mask1 mask2)); split. EvalOp. + apply ROLM; auto. auto. +- InvEval. rewrite Val.orl_commut. apply eval_orlimm; auto. +- InvEval. apply eval_orlimm; auto. +- apply DEFAULT. +Qed. + +Theorem eval_xorlimm: forall n, unary_constructor_sound (xorlimm n) (fun v => Val.xorl v (Vlong n)). +Proof. + unfold xorlimm; intros; red; intros. + predSpec Int64.eq Int64.eq_spec n Int64.zero. + exists x; split; auto. subst. destruct x; simpl; auto. rewrite Int64.xor_zero; auto. + predSpec Int64.eq Int64.eq_spec n Int64.mone. + replace (Val.xorl x (Vlong n)) with (Val.notl x). apply eval_notl; auto. + subst n. destruct x; simpl; auto. + destruct (xorlimm_match a); InvEval; subst. +- econstructor; split. apply eval_longconst. simpl. rewrite Int64.xor_commut; auto. +- TrivialExists. simpl. rewrite Val.xorl_assoc. rewrite Int64.xor_commut; auto. +- TrivialExists. simpl. destruct v1; simpl; auto. unfold Int64.not. + rewrite Int64.xor_assoc. apply f_equal. apply f_equal. apply f_equal. + apply Int64.xor_commut. +- TrivialExists. +Qed. + +Theorem eval_xorl: binary_constructor_sound xorl Val.xorl. +Proof. + unfold xorl; destruct Archi.splitlong. apply SplitLongproof.eval_xorl. + red; intros. destruct (xorl_match a b). +- InvEval. rewrite Val.xorl_commut. apply eval_xorlimm; auto. +- InvEval. apply eval_xorlimm; auto. +- TrivialExists. +Qed. + +Theorem eval_rolml: forall amount mask, unary_constructor_sound (fun v => rolml v amount mask) (fun v => Val.rolml v amount mask). +Proof. + unfold rolml. intros; red; intros. + predSpec Int.eq Int.eq_spec amount Int.zero. + rewrite H0. + exploit (eval_andlimm). eauto. intros (x0 & (H1 & H2)). + exists x0. split. apply H1. destruct x; auto. simpl. unfold Int64.rolm. + change (Int64.repr (Int.unsigned Int.zero)) with Int64.zero. rewrite Int64.rol_zero. + apply H2. + destruct (rolml_match a). +- econstructor; split. apply eval_longconst. simpl. InvEval. unfold Val.rolml. auto. +- InvEval. TrivialExists. simpl. rewrite <- H. + unfold Val.rolml; destruct v1; simpl; auto. + rewrite Int64.rolm_rolm by (exists (two_p (64-6)); auto). + f_equal. f_equal. f_equal. + unfold Int64.add. rewrite ! Int64.int_unsigned_repr. unfold Int.add. + set (a := Int.unsigned amount1 + Int.unsigned amount). + unfold Int.modu, Int64.modu. + change (Int.unsigned Int64.iwordsize') with 64. + change (Int64.unsigned Int64.iwordsize) with 64. + f_equal. + rewrite Int.unsigned_repr. + apply Int.eqmod_mod_eq. omega. + apply Int.eqmod_trans with a. + apply Int.eqmod_divides with Int.modulus. apply Int.eqm_sym. apply Int.eqm_unsigned_repr. + exists (two_p (32-6)); auto. + apply Int.eqmod_divides with Int64.modulus. apply Int64.eqm_unsigned_repr. + exists (two_p (64-6)); auto. + assert (0 <= Int.unsigned (Int.repr a) mod 64 < 64) by (apply Z_mod_lt; omega). + assert (64 < Int.max_unsigned) by (compute; auto). + omega. +- InvEval. TrivialExists. simpl. rewrite <- H. + unfold Val.rolml; destruct v1; simpl; auto. unfold Int64.rolm. + rewrite Int64.rol_and. rewrite Int64.and_assoc. auto. +- TrivialExists. +Qed. + +Theorem eval_shllimm: forall n, unary_constructor_sound (fun e => shllimm e n) (fun v => Val.shll v (Vint n)). +Proof. + intros; unfold shllimm. destruct Archi.splitlong eqn:SL. apply SplitLongproof.eval_shllimm; auto. + red; intros. + assert (ROLM: forall n1 v, + Int.ltu n1 Int64.iwordsize' = true -> + Val.shll v (Vint n1) = Val.rolml v n1 (Int64.shl Int64.mone (Int64.repr (Int.unsigned n1)))). + { intros. destruct v; auto. simpl. rewrite H0. rewrite <- Int64.shl_rolm. unfold Int64.shl. + rewrite Int64.int_unsigned_repr. constructor. unfold Int64.ltu. rewrite Int64.int_unsigned_repr. + apply H0. } + predSpec Int.eq Int.eq_spec n Int.zero. + exists x; split; auto. subst n; destruct x; simpl; auto. + destruct (Int.ltu Int.zero Int64.iwordsize'); auto. + change (Int64.shl' i Int.zero) with (Int64.shl i Int64.zero). rewrite Int64.shl_zero; auto. + destruct (Int.ltu n Int64.iwordsize') eqn:LT; simpl. +- rewrite ROLM by apply LT. apply eval_rolml. auto. +- TrivialExists. constructor; eauto. constructor. EvalOp. simpl; eauto. constructor. + constructor. +Qed. + +Theorem eval_shrluimm: forall n, unary_constructor_sound (fun e => shrluimm e n) (fun v => Val.shrlu v (Vint n)). +Proof. + unfold shrluimm; destruct Archi.splitlong. apply SplitLongproof.eval_shrluimm. auto. + red; intros. + assert (ROLM: forall n1 v, + Int.ltu n1 Int64.iwordsize' = true -> + Val.shrlu v (Vint n1) = Val.rolml v (Int.sub Int64.iwordsize' n1) (Int64.shru Int64.mone (Int64.repr (Int.unsigned n1)))). + { intros. destruct v; auto. simpl. rewrite H0. + rewrite Int64.int_sub_ltu by apply H0. rewrite Int64.repr_unsigned. rewrite <- Int64.shru_rolm. unfold Int64.shru'. unfold Int64.shru. + rewrite Int64.unsigned_repr. reflexivity. apply Int64.int_unsigned_range. + unfold Int64.ltu. rewrite Int64.int_unsigned_repr. auto. + } + predSpec Int.eq Int.eq_spec n Int.zero. + exists x. split. apply H. destruct x; simpl; auto. rewrite H0. rewrite Int64.shru'_zero. constructor. + destruct (Int.ltu n Int64.iwordsize') eqn:LT; simpl. +- rewrite ROLM by apply LT. apply eval_rolml. auto. +- TrivialExists. constructor; eauto. constructor. EvalOp. simpl; eauto. constructor. + constructor. +Qed. + +Theorem eval_shrlimm: forall n, unary_constructor_sound (fun e => shrlimm e n) (fun v => Val.shrl v (Vint n)). +Proof. + intros; unfold shrlimm. destruct Archi.splitlong eqn:SL. apply SplitLongproof.eval_shrlimm; auto. + red; intros. + predSpec Int.eq Int.eq_spec n Int.zero. + exists x; split; auto. subst n; destruct x; simpl; auto. + destruct (Int.ltu Int.zero Int64.iwordsize'); auto. + change (Int64.shr' i Int.zero) with (Int64.shr i Int64.zero). rewrite Int64.shr_zero; auto. + destruct (Int.ltu n Int64.iwordsize') eqn:LT; simpl. + assert (DEFAULT: exists v, eval_expr ge sp e m le (Eop (Oshrlimm n) (a:::Enil)) v + /\ Val.lessdef (Val.shrl x (Vint n)) v) by TrivialExists. + destruct (shrlimm_match a); InvEval. +- TrivialExists. simpl; rewrite LT; auto. +- destruct (Int.ltu (Int.add n n1) Int64.iwordsize') eqn:LT'; auto. + subst. econstructor; split. EvalOp. simpl; eauto. + destruct v1; simpl; auto. rewrite LT'. + destruct (Int.ltu n1 Int64.iwordsize') eqn:LT1; auto. + simpl; rewrite LT. rewrite Int.add_commut, Int64.shr'_shr'; auto. rewrite Int.add_commut; auto. +- apply DEFAULT. +- TrivialExists. constructor; eauto. constructor. EvalOp. simpl; eauto. constructor. auto. +Qed. + +Theorem eval_shll: binary_constructor_sound shll Val.shll. +Proof. + unfold shll. destruct Archi.splitlong eqn:SL. apply SplitLongproof.eval_shll; auto. + red; intros. destruct (is_intconst b) as [n2|] eqn:C. +- exploit is_intconst_sound; eauto. intros EQ; subst y. apply eval_shllimm; auto. +- TrivialExists. +Qed. + +Theorem eval_shrlu: binary_constructor_sound shrlu Val.shrlu. +Proof. + unfold shrlu. destruct Archi.splitlong eqn:SL. apply SplitLongproof.eval_shrlu; auto. + red; intros. destruct (is_intconst b) as [n2|] eqn:C. +- exploit is_intconst_sound; eauto. intros EQ; subst y. apply eval_shrluimm; auto. +- TrivialExists. +Qed. + +Theorem eval_shrl: binary_constructor_sound shrl Val.shrl. +Proof. + unfold shrl. destruct Archi.splitlong eqn:SL. apply SplitLongproof.eval_shrl; auto. + red; intros. destruct (is_intconst b) as [n2|] eqn:C. +- exploit is_intconst_sound; eauto. intros EQ; subst y. apply eval_shrlimm; auto. +- TrivialExists. +Qed. + +Theorem eval_negl: unary_constructor_sound negl Val.negl. +Proof. + unfold negl. destruct Archi.splitlong eqn:SL. apply SplitLongproof.eval_negl; auto. + red; intros. destruct (is_longconst a) as [n|] eqn:C. +- exploit is_longconst_sound; eauto. intros EQ; subst x. + econstructor; split. apply eval_longconst. auto. +- TrivialExists. +Qed. + +Theorem eval_addlimm: forall n, unary_constructor_sound (addlimm n) (fun v => Val.addl v (Vlong n)). +Proof. + unfold addlimm. + red; intros. predSpec Int64.eq Int64.eq_spec n Int64.zero. + exists x. split; auto. rewrite H0. destruct x; auto. simpl. rewrite Int64.add_zero. constructor. + destruct (addlimm_match a). +- econstructor; split. apply eval_longconst. simpl. InvEval. unfold Val.rolml. auto. +- InvEval. TrivialExists. simpl. rewrite <- H. rewrite Val.addl_assoc. reflexivity. +- InvEval. TrivialExists. +Qed. + + +Theorem eval_addl: binary_constructor_sound addl Val.addl. +Proof. + unfold addl. destruct Archi.splitlong eqn:SL. apply SplitLongproof.eval_addl; auto. + red; intros. destruct (addl_match a b); InvEval; subst. +- exploit (eval_addlimm n1); eauto. intros (n & (H1 & H2)). exists n. split; auto. + rewrite Val.addl_commut. exact H2. +- exploit (eval_addlimm n2). apply H. auto. +- rewrite Val.addl_permut_4. simpl. + apply eval_addlimm; EvalOp. +- rewrite Val.addl_assoc. rewrite Val.addl_permut. rewrite Val.addl_commut. + apply eval_addlimm; EvalOp. +- rewrite Val.addl_commut. rewrite Val.addl_assoc. rewrite Val.addl_permut. + rewrite Val.addl_commut. apply eval_addlimm; EvalOp. rewrite Val.addl_commut. + constructor. +- TrivialExists. +Qed. + +Theorem eval_subl: binary_constructor_sound subl Val.subl. +Proof. + unfold subl. destruct Archi.splitlong eqn:SL. + apply SplitLongproof.eval_subl. apply Archi.splitlong_ptr32; auto. + red; intros; destruct (subl_match a b); InvEval. +- rewrite Val.subl_addl_opp. apply eval_addlimm; auto. +- TrivialExists. +Qed. + +Theorem eval_mullimm_base: forall n, unary_constructor_sound (mullimm_base n) (fun v => Val.mull v (Vlong n)). +Proof. + intros; unfold mullimm_base. red. intros. + assert (DEFAULT: exists v : val, eval_expr ge sp e m le (Eop Omull (a ::: longconst n ::: Enil)) v + /\ Val.lessdef (Val.mull x (Vlong n)) v). + { TrivialExists. constructor. eauto. constructor. apply eval_longconst. constructor. auto. } + generalize (Int64.one_bits'_decomp n); intros D. + destruct (Int64.one_bits' n) as [ | i [ | j [ | ? ? ]]] eqn:B; auto. +- replace (Val.mull x (Vlong n)) with (Val.shll x (Vint i)). + apply eval_shllimm; auto. + simpl in D. rewrite D, Int64.add_zero. destruct x; simpl; auto. + rewrite (Int64.one_bits'_range n) by (rewrite B; auto with coqlib). + rewrite Int64.shl'_mul; auto. +- set (le' := x :: le). + assert (A0: eval_expr ge sp e m le' (Eletvar O) x) by (constructor; reflexivity). + exploit (eval_shllimm i). eexact A0. intros (v1 & A1 & B1). + exploit (eval_shllimm j). eexact A0. intros (v2 & A2 & B2). + exploit (eval_addl). eexact A1. eexact A2. intros (v3 & A3 & B3). + exists v3; split. econstructor; eauto. + rewrite D. simpl. rewrite Int64.add_zero. destruct x; auto. + simpl in *. + rewrite (Int64.one_bits'_range n) in B1 by (rewrite B; auto with coqlib). + rewrite (Int64.one_bits'_range n) in B2 by (rewrite B; auto with coqlib). + inv B1; inv B2. simpl in B3; inv B3. + rewrite Int64.mul_add_distr_r. rewrite <- ! Int64.shl'_mul. auto. +Qed. + +Theorem eval_mullimm: forall n, unary_constructor_sound (mullimm n) (fun v => Val.mull v (Vlong n)). +Proof. + unfold mullimm. intros. + destruct Archi.splitlong eqn:SL. + eapply SplitLongproof.eval_mullimm; eauto. + red; intros. predSpec Int64.eq Int64.eq_spec n Int64.zero. + exists (Vlong Int64.zero). + split. apply eval_longconst. destruct x; simpl; auto. + subst n; rewrite Int64.mul_zero; auto. + predSpec Int64.eq Int64.eq_spec n Int64.one. + exists x; split; auto. + destruct x; simpl; auto. subst n; rewrite Int64.mul_one; auto. + destruct (mullimm_match a); InvEval. +- econstructor; split. apply eval_longconst. rewrite Int64.mul_commut; auto. +- exploit (eval_mullimm_base n); eauto. +Qed. + +Theorem eval_mull: binary_constructor_sound mull Val.mull. +Proof. + unfold mull. destruct Archi.splitlong eqn:SL. + apply SplitLongproof.eval_mull; auto. + red; intros. destruct (mull_match a b). +- exploit (eval_mullimm n1); eauto. intros (n & (H1 & H2)). InvEval. exists n. split; auto. + rewrite Val.mull_commut. exact H2. +- exploit (eval_mullimm n2). apply H. InvEval. auto. +- TrivialExists. +Qed. + +Theorem eval_mullhu: + forall n, unary_constructor_sound (fun a => mullhu a n) (fun v => Val.mullhu v (Vlong n)). +Proof. + unfold mullhu; intros. destruct Archi.splitlong eqn:SL. apply SplitLongproof.eval_mullhu; auto. + red; intros. TrivialExists. constructor. eauto. constructor. apply eval_longconst. constructor. auto. +Qed. + +Theorem eval_mullhs: + forall n, unary_constructor_sound (fun a => mullhs a n) (fun v => Val.mullhs v (Vlong n)). +Proof. + unfold mullhs; intros. destruct Archi.splitlong eqn:SL. apply SplitLongproof.eval_mullhs; auto. + red; intros. TrivialExists. constructor. eauto. constructor. apply eval_longconst. constructor. auto. +Qed. + +Theorem eval_shrxlimm: + forall le a n x z, + eval_expr ge sp e m le a x -> + Val.shrxl x (Vint n) = Some z -> + exists v, eval_expr ge sp e m le (shrxlimm a n) v /\ Val.lessdef z v. +Proof. + unfold shrxlimm. intros. destruct Archi.splitlong eqn:SL. + eapply SplitLongproof.eval_shrxlimm; eauto. + predSpec Int.eq Int.eq_spec n Int.zero. +- subst n. destruct x; simpl in H0; inv H0. econstructor; split; eauto. + change (Int.ltu Int.zero (Int.repr 63)) with true. simpl. rewrite Int64.shrx'_zero; auto. +- TrivialExists. +Qed. + +Theorem eval_divls_base: partial_binary_constructor_sound divls_base Val.divls. +Proof. + unfold divls_base; red; intros. destruct Archi.splitlong eqn:SL. + eapply SplitLongproof.eval_divls_base; eauto. + TrivialExists. +Qed. + +Lemma eval_modl_aux: + forall divop semdivop, + (forall sp x y m, eval_operation ge sp divop (x :: y :: nil) m = semdivop x y) -> + forall le a b x y z, + eval_expr ge sp e m le a x -> + eval_expr ge sp e m le b y -> + semdivop x y = Some z -> + eval_expr ge sp e m le (modl_aux divop a b) (Val.subl x (Val.mull z y)). +Proof. + intros; unfold modl_aux. + eapply eval_Elet. eexact H0. eapply eval_Elet. + apply eval_lift. eexact H1. + eapply eval_Eop. eapply eval_Econs. + eapply eval_Eletvar. simpl; reflexivity. + eapply eval_Econs. eapply eval_Eop. + eapply eval_Econs. eapply eval_Eop. + eapply eval_Econs. apply eval_Eletvar. simpl; reflexivity. + eapply eval_Econs. apply eval_Eletvar. simpl; reflexivity. + apply eval_Enil. + rewrite H. eauto. + eapply eval_Econs. apply eval_Eletvar. simpl; reflexivity. + apply eval_Enil. + simpl; reflexivity. apply eval_Enil. + reflexivity. +Qed. + +Theorem eval_modls_base: partial_binary_constructor_sound modls_base Val.modls. +Proof. + unfold modls_base. red; intros. destruct Archi.splitlong eqn:SL. + eapply SplitLongproof.eval_modls_base; eauto. + assert (DEFAULT: exists v : val, eval_expr ge sp e m le (modl_aux Odivl a b) v /\ Val.lessdef z v). + exploit Val.modls_divls; eauto. intros [v [A B]]. + { subst. econstructor; split; eauto. + apply eval_modl_aux with (semdivop := Val.divls); auto. } + + destruct (is_longconst a) as [n1|] eqn:A. exploit is_longconst_sound. eauto. eauto. intros. + destruct (is_longconst b) as [n2|] eqn:B; auto. exploit is_longconst_sound. eauto. eauto. intros. + predSpec Int64.eq Int64.eq_spec Int64.zero n2; simpl. + (* n1 mod n2, n2 = 0 *) + auto. + predSpec Int64.eq Int64.eq_spec n1 (Int64.repr Int64.min_signed); predSpec Int64.eq Int64.eq_spec n2 Int64.mone; simpl; auto; subst. +- (* signed_min mod n2 | n2 != 0, n2 !- =1 *) + econstructor; split. apply eval_longconst. + unfold Val.modls in H1. + rewrite Int64.eq_false in H1; auto. + rewrite (Int64.eq_false n2 Int64.mone H6) in H1. + inversion H1. auto. +- (* n1 mod -1, n1 !- signed_min *) + econstructor; split. apply eval_longconst. + unfold Val.modls in H1. + rewrite Int64.eq_false in H1; auto. + rewrite Int64.eq_false in H1; auto. + inversion H1. auto. +- (* other valid cases *) + econstructor; split. apply eval_longconst. + unfold Val.modls in H1. + rewrite Int64.eq_false in H1; auto. + rewrite Int64.eq_false in H1; auto. + inversion H1. + auto. +- (* fallback *) + apply DEFAULT. +Qed. + + +Theorem eval_divlu_base: partial_binary_constructor_sound divlu_base Val.divlu. +Proof. + unfold divlu_base; red; intros. destruct Archi.splitlong eqn:SL. + eapply SplitLongproof.eval_divlu_base; eauto. + TrivialExists. +Qed. + +Theorem eval_modlu_base: partial_binary_constructor_sound modlu_base Val.modlu. +Proof. + unfold modlu_base; red; intros. destruct Archi.splitlong eqn:SL. + eapply SplitLongproof.eval_modlu_base; eauto. + assert (DEFAULT: exists v : val, eval_expr ge sp e m le (modl_aux Odivlu a b) v /\ Val.lessdef z v). + exploit Val.modlu_divlu; eauto. intros [v [A B]]. + subst. econstructor; split; eauto. + apply eval_modl_aux with (semdivop := Val.divlu); auto. + (* n1 and n2 are longconsts *) + destruct (is_longconst a) as [n1|] eqn:A. exploit is_longconst_sound; eauto. + destruct (is_longconst b) as [n2|] eqn:B; auto. exploit is_longconst_sound; eauto. intros. + predSpec Int64.eq Int64.eq_spec Int64.zero n2; simpl. + (* n2 = 0 *) +- auto. + (* n2 != 0 *) +- econstructor; split. apply eval_longconst. + rewrite H2 in H1. + rewrite H3 in H1. + unfold Val.modlu in H1. + rewrite Int64.eq_false in H1; auto. + inversion H1. auto. +- (* n1 no longconst, n2 is longconst *) + destruct (is_longconst b) as [n2|] eqn:B; auto. exploit is_longconst_sound; eauto. intros. + destruct (Int64.is_power2 n2) eqn:C; auto. + (* n2 is power of 2 *) + exploit eval_andlimm. apply H. intros. destruct H3. + exists x0. split. apply H3. + replace z with (Val.andl x (Vlong (Int64.sub n2 Int64.one))). apply H3. + apply (Val.modlu_pow2 x n2 i z); congruence. +Qed. + +Theorem eval_cmplu: + forall c le a x b y v, + eval_expr ge sp e m le a x -> + eval_expr ge sp e m le b y -> + Val.cmplu (Mem.valid_pointer m) c x y = Some v -> + eval_expr ge sp e m le (cmplu c a b) v. +Proof. + unfold cmplu; intros. destruct Archi.splitlong eqn:SL. + eapply SplitLongproof.eval_cmplu; eauto using Archi.splitlong_ptr32. + unfold Val.cmplu in H1. + destruct (Val.cmplu_bool (Mem.valid_pointer m) c x y) as [vb|] eqn:C; simpl in H1; inv H1. + destruct (is_longconst a) as [n1|] eqn:LC1; destruct (is_longconst b) as [n2|] eqn:LC2; + try (assert (x = Vlong n1) by (eapply is_longconst_sound; eauto)); + try (assert (y = Vlong n2) by (eapply is_longconst_sound; eauto)); + subst. +- simpl in C; inv C. EvalOp. destruct (Int64.cmpu c n1 n2); reflexivity. +- EvalOp. simpl. rewrite Val.swap_cmplu_bool. rewrite C; auto. +- EvalOp. simpl; rewrite C; auto. +- EvalOp. simpl; rewrite C; auto. +Qed. + +Theorem eval_cmpl: + forall c le a x b y v, + eval_expr ge sp e m le a x -> + eval_expr ge sp e m le b y -> + Val.cmpl c x y = Some v -> + eval_expr ge sp e m le (cmpl c a b) v. +Proof. + unfold cmpl; intros. destruct Archi.splitlong eqn:SL. + eapply SplitLongproof.eval_cmpl; eauto. + unfold Val.cmpl in H1. + destruct (Val.cmpl_bool c x y) as [vb|] eqn:C; simpl in H1; inv H1. + destruct (is_longconst a) as [n1|] eqn:LC1; destruct (is_longconst b) as [n2|] eqn:LC2; + try (assert (x = Vlong n1) by (eapply is_longconst_sound; eauto)); + try (assert (y = Vlong n2) by (eapply is_longconst_sound; eauto)); + subst. +- simpl in C; inv C. EvalOp. destruct (Int64.cmp c n1 n2); reflexivity. +- EvalOp. simpl. rewrite Val.swap_cmpl_bool. rewrite C; auto. +- EvalOp. simpl; rewrite C; auto. +- EvalOp. simpl; rewrite C; auto. +Qed. + +Theorem eval_longoffloat: + forall le a x y, + eval_expr ge sp e m le a x -> + Val.longoffloat x = Some y -> + exists v, eval_expr ge sp e m le (longoffloat a) v /\ Val.lessdef y v. +Proof. + unfold longoffloat. intros. destruct Archi.splitlong eqn:SL. + eapply SplitLongproof.eval_longoffloat; eauto. + TrivialExists. +Qed. + +Theorem eval_floatoflong: + forall le a x y, + eval_expr ge sp e m le a x -> + Val.floatoflong x = Some y -> + exists v, eval_expr ge sp e m le (floatoflong a) v /\ Val.lessdef y v. +Proof. + unfold floatoflong. intros. destruct Archi.splitlong eqn:SL. + eapply SplitLongproof.eval_floatoflong; eauto. + TrivialExists. +Qed. + +Theorem eval_longofsingle: + forall le a x y, + eval_expr ge sp e m le a x -> + Val.longofsingle x = Some y -> + exists v, eval_expr ge sp e m le (longofsingle a) v /\ Val.lessdef y v. +Proof. + intros; unfold longofsingle. + destruct x; simpl in H0; inv H0. destruct (Float32.to_long f) as [n|] eqn:EQ; simpl in H2; inv H2. + exploit eval_floatofsingle; eauto. intros (v & A & B). simpl in B. inv B. + apply Float32.to_long_double in EQ. + eapply eval_longoffloat; eauto. simpl. + change (Float.of_single f) with (Float32.to_double f); rewrite EQ; auto. +Qed. + +End CMCONSTR. diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp index 0a4b3ef6..2d9ae7a5 100644 --- a/powerpc/SelectOp.vp +++ b/powerpc/SelectOp.vp @@ -239,7 +239,7 @@ Definition mulhu (e1: expr) (e2: expr) := Eop Omulhu (e1 ::: e2 ::: Enil). (** ** Bitwise and, or, xor *) -Nondetfunction andimm (n1: int) (e2: expr) := +Nondetfunction andimm (n1: int) (e2: expr) := if Int.eq n1 Int.zero then Eop (Ointconst Int.zero) Enil else if Int.eq n1 Int.mone then e2 else match e2 with @@ -249,7 +249,7 @@ Nondetfunction andimm (n1: int) (e2: expr) := let n := Int.and n1 n2 in if Int.eq (Int.shru (Int.shl n amount) amount) n && Int.ltu amount Int.iwordsize - then rolm t2 (Int.sub Int.iwordsize amount) + then rolm t2 (Int.sub Int.iwordsize amount) (Int.and (Int.shru Int.mone amount) n) else Eop (Oandimm n) (Eop (Oshrimm amount) (t2:::Enil) ::: Enil) | Eop (Oandimm n2) (t2:::Enil) => @@ -259,7 +259,7 @@ Nondetfunction andimm (n1: int) (e2: expr) := | Eop (Oshrimm amount) (t2:::Enil) => if Int.eq (Int.shru (Int.shl n1 amount) amount) n1 && Int.ltu amount Int.iwordsize - then rolm t2 (Int.sub Int.iwordsize amount) + then rolm t2 (Int.sub Int.iwordsize amount) (Int.and (Int.shru Int.mone amount) n1) else Eop (Oandimm n1) (e2:::Enil) | _ => @@ -396,14 +396,14 @@ Nondetfunction compimm (default: comparison -> int -> condition) Eop (Ocmp (negate_condition c)) el else if Int.eq_dec n2 Int.one then Eop (Ocmp c) el - else + else Eop (Ointconst Int.zero) Enil | Cne, Eop (Ocmp c) el => if Int.eq_dec n2 Int.zero then Eop (Ocmp c) el else if Int.eq_dec n2 Int.one then Eop (Ocmp (negate_condition c)) el - else + else Eop (Ointconst Int.one) Enil | Ceq, Eop (Oandimm n1) (t1 ::: Enil) => if Int.eq_dec n2 Int.zero then @@ -483,7 +483,8 @@ Nondetfunction floatofintu (e: expr) := | Eop (Ointconst n) Enil => Eop (Ofloatconst (Float.of_intu n)) Enil | _ => - if Archi.ppc64 then Eop Ofloatofintu (e ::: Enil) else + if Archi.ppc64 then + Eop Ofloatofintu (e ::: Enil) else subf (Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil ::: e ::: Enil)) (Eop (Ofloatconst (Float.from_words Float.ox4330_0000 Int.zero)) Enil) end. @@ -493,7 +494,8 @@ Nondetfunction floatofint (e: expr) := | Eop (Ointconst n) Enil => Eop (Ofloatconst (Float.of_int n)) Enil | _ => - if Archi.ppc64 then Eop Ofloatofint (e ::: Enil) else + if Archi.ppc64 then + Eop Ofloatofint (e ::: Enil) else subf (Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil ::: addimm Float.ox8000_0000 e ::: Enil)) (Eop (Ofloatconst (Float.from_words Float.ox4330_0000 Float.ox8000_0000)) Enil) @@ -517,7 +519,7 @@ Definition floatofsingle (e: expr) := Eop Ofloatofsingle (e ::: Enil). (** ** Recognition of addressing modes for load and store operations *) Definition can_use_Aindexed2 (chunk: memory_chunk): bool := - match chunk with Mint64 => false | _ => true end. + match chunk with Mint64 => Archi.ppc64 | _ => true end. Nondetfunction addressing (chunk: memory_chunk) (e: expr) := match e with @@ -539,6 +541,7 @@ Nondetfunction builtin_arg (e: expr) := | Eop (Ointconst n) Enil => BA_int n | Eop (Oaddrsymbol id ofs) Enil => BA_addrglobal id ofs | Eop (Oaddrstack ofs) Enil => BA_addrstack ofs + | Eop (Olongconst n) Enil => BA_long n | Eop Omakelong (Eop (Ointconst h) Enil ::: Eop (Ointconst l) Enil ::: Enil) => BA_long (Int64.ofwords h l) | Eop Omakelong (h ::: l ::: Enil) => BA_splitlong (BA h) (BA l) diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v index 7f3da409..31ddf304 100644 --- a/powerpc/SelectOpproof.v +++ b/powerpc/SelectOpproof.v @@ -160,7 +160,7 @@ Remark shift_symbol_address: Genv.symbol_address ge id (Ptrofs.add ofs (Ptrofs.of_int delta)) = Val.add (Genv.symbol_address ge id ofs) (Vint delta). Proof. intros. unfold Genv.symbol_address. destruct (Genv.find_symbol ge id); auto. -Qed. +Qed. Theorem eval_addimm: forall n, unary_constructor_sound (addimm n) (fun x => Val.add x (Vint n)). @@ -172,7 +172,7 @@ Proof. case (addimm_match a); intros; InvEval; simpl; TrivialExists; simpl. rewrite Int.add_commut. auto. unfold Genv.symbol_address. destruct (Genv.find_symbol ge s); simpl; auto. rewrite Ptrofs.add_commut; auto. - destruct sp; simpl; auto. rewrite Ptrofs.add_assoc. do 3 f_equal. apply Ptrofs.add_commut. + destruct sp; simpl; auto. rewrite Ptrofs.add_assoc. do 3 f_equal. apply Ptrofs.add_commut. subst. rewrite Val.add_assoc. rewrite Int.add_commut. auto. subst. rewrite Ptrofs.add_commut. rewrite shift_symbol_address. rewrite ! Val.add_assoc. f_equal. f_equal. apply Val.add_commut. Qed. @@ -207,7 +207,7 @@ Proof. repeat rewrite Val.add_assoc. decEq. apply Val.add_commut. - subst. TrivialExists. econstructor. EvalOp. simpl. reflexivity. econstructor. eauto. constructor. - simpl. rewrite Val.add_permut, Val.add_commut. do 2 f_equal. + simpl. rewrite Val.add_permut, Val.add_commut. do 2 f_equal. destruct sp; simpl; auto. rewrite Ptrofs.add_assoc; auto. - replace (Val.add x y) with (Val.add (Genv.symbol_address ge s (Ptrofs.add ofs (Ptrofs.of_int n))) (Val.add v1 v0)). @@ -847,6 +847,7 @@ Proof. intros; unfold intoffloat. TrivialExists. Qed. + Theorem eval_intuoffloat: forall le a x y, eval_expr ge sp e m le a x -> @@ -1032,6 +1033,7 @@ Proof. - constructor. - constructor. - constructor. +- constructor. - simpl in H5. inv H5. constructor. - subst v. constructor; auto. - inv H. InvEval. simpl in H6; inv H6. constructor; auto. @@ -1040,4 +1042,3 @@ Proof. Qed. End CMCONSTR. - diff --git a/powerpc/Stacklayout.v b/powerpc/Stacklayout.v index 2b78fd11..17104b33 100644 --- a/powerpc/Stacklayout.v +++ b/powerpc/Stacklayout.v @@ -93,7 +93,7 @@ Local Opaque Z.add Z.mul sepconj range. apply range_drop_right with 8. omega. apply range_split. omega. apply range_split_2. fold ol; omega. omega. - apply range_split. omega. + apply range_split. omega. apply range_split. omega. apply range_drop_right with ostkdata. omega. eapply sep_drop2. eexact H. diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index 68cd001b..cb5f2304 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -359,6 +359,26 @@ module Target (System : SYSTEM):TARGET = assert (!count = 2 || (!count = 0 && !last)); (!mb, !me-1) + (* Encoding 64-bit masks for rldic PPC64 instructions *) + + let rolm64_mask n = + let rec leftmost_one pos mask = + assert (pos < 64); + let mask' = Int64.shift_right_logical mask 1 in + if Int64.logand n mask = 0L + then leftmost_one (pos + 1) mask' + else (pos, rightmost_one (pos + 1) mask') + and rightmost_one pos mask = + if pos >= 64 then + 63 + else if Int64.logand n mask > 0L then + rightmost_one (pos + 1) (Int64.shift_right_logical mask 1) + else if Int64.logand n (Int64.pred mask) = 0L then + pos - 1 + else + assert false + in leftmost_one 0 0x8000_0000_0000_0000L + (* Determine if the displacement of a conditional branch fits the short form *) let short_cond_branch tbl pc lbl_dest = @@ -370,7 +390,7 @@ module Target (System : SYSTEM):TARGET = (* Printing of instructions *) let print_instruction oc tbl pc fallthrough = function - | Padd(r1, r2, r3) -> + | Padd(r1, r2, r3) | Padd64(r1, r2, r3) -> fprintf oc " add %a, %a, %a\n" ireg r1 ireg r2 ireg r3 | Paddc(r1, r2, r3) -> fprintf oc " addc %a, %a, %a\n" ireg r1 ireg r2 ireg r3 @@ -378,22 +398,30 @@ module Target (System : SYSTEM):TARGET = fprintf oc " adde %a, %a, %a\n" ireg r1 ireg r2 ireg r3 | Paddi(r1, r2, c) -> fprintf oc " addi %a, %a, %a\n" ireg r1 ireg_or_zero r2 constant c + | Paddi64(r1, r2, n) -> + fprintf oc " addi %a, %a, %Ld\n" ireg r1 ireg_or_zero r2 (camlint64_of_coqint n) | Paddic(r1, r2, c) -> fprintf oc " addic %a, %a, %a\n" ireg r1 ireg_or_zero r2 constant c | Paddis(r1, r2, c) -> fprintf oc " addis %a, %a, %a\n" ireg r1 ireg_or_zero r2 constant c - | Paddze(r1, r2) -> + | Paddis64(r1, r2, n) -> + fprintf oc " addis %a, %a, %Ld\n" ireg r1 ireg_or_zero r2 (camlint64_of_coqint n) + | Paddze(r1, r2) | Paddze64(r1, r2) -> fprintf oc " addze %a, %a\n" ireg r1 ireg r2 | Pallocframe(sz, ofs, _) -> assert false - | Pand_(r1, r2, r3) -> + | Pand_(r1, r2, r3) | Pand_64(r1, r2, r3) -> fprintf oc " and. %a, %a, %a\n" ireg r1 ireg r2 ireg r3 | Pandc(r1, r2, r3) -> fprintf oc " andc %a, %a, %a\n" ireg r1 ireg r2 ireg r3 | Pandi_(r1, r2, c) -> fprintf oc " andi. %a, %a, %a\n" ireg r1 ireg r2 constant c + | Pandi_64(r1, r2, n) -> + fprintf oc " andi. %a, %a, %Ld\n" ireg r1 ireg r2 (camlint64_of_coqint n) | Pandis_(r1, r2, c) -> fprintf oc " andis. %a, %a, %a\n" ireg r1 ireg r2 constant c + | Pandis_64(r1, r2, n) -> + fprintf oc " andis. %a, %a, %Ld\n" ireg r1 ireg r2 (camlint64_of_coqint n) | Pb lbl -> fprintf oc " b %a\n" label (transl_label lbl) | Pbctr sg -> @@ -445,14 +473,24 @@ module Target (System : SYSTEM):TARGET = fprintf oc "%s end pseudoinstr btbl\n" comment | Pcmpb (r1, r2, r3) -> fprintf oc " cmpb %a, %a, %a\n" ireg r1 ireg r2 ireg r3 + | Pcmpld(r1, r2) -> + fprintf oc " cmpld %a, %a, %a\n" creg 0 ireg r1 ireg r2 + | Pcmpldi(r1, n) -> + fprintf oc " cmpldi %a, %a, %Ld\n" creg 0 ireg r1 (camlint64_of_coqint n) | Pcmplw(r1, r2) -> fprintf oc " cmplw %a, %a, %a\n" creg 0 ireg r1 ireg r2 | Pcmplwi(r1, c) -> fprintf oc " cmplwi %a, %a, %a\n" creg 0 ireg r1 constant c + | Pcmpd(r1, r2) -> + fprintf oc " cmpd %a, %a, %a\n" creg 0 ireg r1 ireg r2 + | Pcmpdi(r1, n) -> + fprintf oc " cmpdi %a, %a, %Ld\n" creg 0 ireg r1 (camlint64_of_coqint n) | Pcmpw(r1, r2) -> fprintf oc " cmpw %a, %a, %a\n" creg 0 ireg r1 ireg r2 | Pcmpwi(r1, c) -> fprintf oc " cmpwi %a, %a, %a\n" creg 0 ireg r1 constant c + | Pcntlzd(r1, r2) -> + fprintf oc " cntlzd %a, %a\n" ireg r1 ireg r2 | Pcntlzw(r1, r2) -> fprintf oc " cntlzw %a, %a\n" ireg r1 ireg r2 | Pcreqv(c1, c2, c3) -> @@ -477,6 +515,10 @@ module Target (System : SYSTEM):TARGET = fprintf oc " divw %a, %a, %a\n" ireg r1 ireg r2 ireg r3 | Pdivwu(r1, r2, r3) -> fprintf oc " divwu %a, %a, %a\n" ireg r1 ireg r2 ireg r3 + | Pdivd(r1, r2, r3) -> + fprintf oc " divd %a, %a, %a\n" ireg r1 ireg r2 ireg r3 + | Pdivdu(r1, r2, r3) -> + fprintf oc " divdu %a, %a, %a\n" ireg r1 ireg r2 ireg r3 | Peieio -> fprintf oc " eieio\n" | Peqv(r1, r2, r3) -> @@ -487,6 +529,8 @@ module Target (System : SYSTEM):TARGET = fprintf oc " extsh %a, %a\n" ireg r1 ireg r2 | Pextsw(r1, r2) -> fprintf oc " extsw %a, %a\n" ireg r1 ireg r2 + | Pextzw(r1, r2) -> + assert false | Pfreeframe(sz, ofs) -> assert false | Pfabs(r1, r2) | Pfabss(r1, r2) -> @@ -499,12 +543,16 @@ module Target (System : SYSTEM):TARGET = fprintf oc " fcmpu %a, %a, %a\n" creg 0 freg r1 freg r2 | Pfcfi(r1, r2) -> assert false + | Pfcfl(r1, r2) -> + assert false | Pfcfid(r1, r2) -> fprintf oc " fcfid %a, %a\n" freg r1 freg r2 | Pfcfiu(r1, r2) -> assert false | Pfcti(r1, r2) -> assert false + | Pfctid(r1, r2) -> + assert false | Pfctidz(r1, r2) -> fprintf oc " fctidz %a, %a\n" freg r1 freg r2 | Pfctiu(r1, r2) -> @@ -565,6 +613,10 @@ module Target (System : SYSTEM):TARGET = fprintf oc " lbz %a, %a(%a)\n" ireg r1 constant c ireg r2 | Plbzx(r1, r2, r3) -> fprintf oc " lbzx %a, %a, %a\n" ireg r1 ireg r2 ireg r3 + | Pld(r1, c, r2) | Pld_a(r1, c, r2) -> + fprintf oc " ld %a, %a(%a)\n" ireg r1 constant c ireg r2 + | Pldx(r1, r2, r3) | Pldx_a(r1, r2, r3) -> + fprintf oc " ldx %a, %a, %a\n" ireg r1 ireg r2 ireg r3 | Plfd(r1, c, r2) | Plfd_a(r1, c, r2) -> fprintf oc " lfd %a, %a(%a)\n" freg r1 constant c ireg r2 | Plfdx(r1, r2, r3) | Plfdx_a(r1, r2, r3) -> @@ -583,6 +635,17 @@ module Target (System : SYSTEM):TARGET = fprintf oc " lhz %a, %a(%a)\n" ireg r1 constant c ireg r2 | Plhzx(r1, r2, r3) -> fprintf oc " lhzx %a, %a, %a\n" ireg r1 ireg r2 ireg r3 + | Pldi(r1, c) -> + let lbl = new_label() in + fprintf oc " addis %a, 0, %a\n" ireg GPR12 label_high lbl; + fprintf oc " ld %a, %a(%a) %s %Ld\n" ireg r1 label_low lbl ireg GPR12 comment (camlint64_of_coqint c); + int64_literals := (lbl, camlint64_of_coqint c) :: !int64_literals; + | Plmake(_, _, _) -> + assert false + | Pllo _ -> + assert false + | Plhi(_, _) -> + assert false | Plfi(r1, c) -> let lbl = new_label() in fprintf oc " addis %a, 0, %a\n" ireg GPR12 label_high lbl; @@ -621,6 +684,8 @@ module Target (System : SYSTEM):TARGET = fprintf oc " mfspr %a, %ld\n" ireg rd (camlint_of_coqint spr) | Pmtspr(spr, rs) -> fprintf oc " mtspr %ld, %a\n" (camlint_of_coqint spr) ireg rs + | Pmulld(r1, r2, r3) -> + fprintf oc " mulld %a, %a, %a\n" ireg r1 ireg r2 ireg r3 | Pmulli(r1, r2, c) -> fprintf oc " mulli %a, %a, %a\n" ireg r1 ireg r2 constant c | Pmullw(r1, r2, r3) -> @@ -629,24 +694,51 @@ module Target (System : SYSTEM):TARGET = fprintf oc " mulhw %a, %a, %a\n" ireg r1 ireg r2 ireg r3 | Pmulhwu(r1, r2, r3) -> fprintf oc " mulhwu %a, %a, %a\n" ireg r1 ireg r2 ireg r3 + | Pmulhd (r1,r2,r3) -> + fprintf oc " mulhd %a, %a, %a\n" ireg r1 ireg r2 ireg r3 + | Pmulhdu (r1,r2,r3) -> + fprintf oc " mulhdu %a, %a, %a\n" ireg r1 ireg r2 ireg r3 | Pnand(r1, r2, r3) -> fprintf oc " nand %a, %a, %a\n" ireg r1 ireg r2 ireg r3 - | Pnor(r1, r2, r3) -> + | Pnor(r1, r2, r3) | Pnor64(r1, r2, r3) -> fprintf oc " nor %a, %a, %a\n" ireg r1 ireg r2 ireg r3 - | Por(r1, r2, r3) -> + | Por(r1, r2, r3) | Por64(r1, r2, r3) -> fprintf oc " or %a, %a, %a\n" ireg r1 ireg r2 ireg r3 | Porc(r1, r2, r3) -> fprintf oc " orc %a, %a, %a\n" ireg r1 ireg r2 ireg r3 | Pori(r1, r2, c) -> fprintf oc " ori %a, %a, %a\n" ireg r1 ireg r2 constant c + | Pori64(r1, r2, n) -> + fprintf oc " ori %a, %a, %Ld\n" ireg r1 ireg r2 (camlint64_of_coqint n) | Poris(r1, r2, c) -> fprintf oc " oris %a, %a, %a\n" ireg r1 ireg r2 constant c + | Poris64(r1, r2, n) -> + fprintf oc " oris %a, %a, %Ld\n" ireg r1 ireg r2 (camlint64_of_coqint n) | Prldicl(r1, r2, c1, c2) -> fprintf oc " rldicl %a, %a, %ld, %ld\n" ireg r1 ireg r2 (camlint_of_coqint c1) (camlint_of_coqint c2) - | Prldicr(r1, r2, c1, c2) -> - fprintf oc " rldicr %a, %a, %ld, %ld\n" - ireg r1 ireg r2 (camlint_of_coqint c1) (camlint_of_coqint c2) + | Prldinm(r1, r2, c1, c2) -> + let amount = camlint64_of_coqint c1 in + let mask = camlint64_of_coqint c2 in + let (first, last) = rolm64_mask mask in + if last = 63 then + fprintf oc " rldicl %a, %a, %Ld, %d %s 0x%Lx\n" + ireg r1 ireg r2 amount first comment mask + else if first = 0 then + fprintf oc " rldicr %a, %a, %Ld, %d %s 0x%Lx\n" + ireg r1 ireg r2 amount last comment mask + else if last = 63 - Int64.to_int amount then + fprintf oc " rldic %a, %a, %Ld, %d %s 0x%Lx\n" + ireg r1 ireg r2 amount first comment mask + else + assert false + | Prldimi(r1, r2, c1, c2) -> + let amount = camlint64_of_coqint c1 in + let mask = camlint64_of_coqint c2 in + let (first, last) = rolm64_mask mask in + assert (last = 63 - Int64.to_int amount); + fprintf oc " rldimi %a, %a, %Ld, %d %s 0x%Lx\n" + ireg r1 ireg r2 amount first comment mask | Prlwinm(r1, r2, c1, c2) -> let (mb, me) = rolm_mask (camlint_of_coqint c2) in fprintf oc " rlwinm %a, %a, %ld, %d, %d %s 0x%lx\n" @@ -657,18 +749,30 @@ module Target (System : SYSTEM):TARGET = fprintf oc " rlwimi %a, %a, %ld, %d, %d %s 0x%lx\n" ireg r1 ireg r2 (camlint_of_coqint c1) mb me comment (camlint_of_coqint c2) + | Psld(r1, r2, r3) -> + fprintf oc " sld %a, %a, %a\n" ireg r1 ireg r2 ireg r3 | Pslw(r1, r2, r3) -> fprintf oc " slw %a, %a, %a\n" ireg r1 ireg r2 ireg r3 + | Psrad(r1, r2, r3) -> + fprintf oc " srad %a, %a, %a\n" ireg r1 ireg r2 ireg r3 + | Psradi(r1, r2, c) -> + fprintf oc " sradi %a, %a, %ld\n" ireg r1 ireg r2 (camlint_of_coqint c) | Psraw(r1, r2, r3) -> fprintf oc " sraw %a, %a, %a\n" ireg r1 ireg r2 ireg r3 | Psrawi(r1, r2, c) -> fprintf oc " srawi %a, %a, %ld\n" ireg r1 ireg r2 (camlint_of_coqint c) + | Psrd(r1, r2, r3) -> + fprintf oc " srd %a, %a, %a\n" ireg r1 ireg r2 ireg r3 | Psrw(r1, r2, r3) -> fprintf oc " srw %a, %a, %a\n" ireg r1 ireg r2 ireg r3 | Pstb(r1, c, r2) -> fprintf oc " stb %a, %a(%a)\n" ireg r1 constant c ireg r2 | Pstbx(r1, r2, r3) -> fprintf oc " stbx %a, %a, %a\n" ireg r1 ireg r2 ireg r3 + | Pstd(r1, c, r2) | Pstd_a(r1, c, r2) -> + fprintf oc " std %a, %a(%a)\n" ireg r1 constant c ireg r2 + | Pstdx(r1, r2, r3) | Pstdx_a(r1, r2, r3) -> + fprintf oc " stdx %a, %a, %a\n" ireg r1 ireg r2 ireg r3 | Pstdu(r1, c, r2) -> fprintf oc " stdu %a, %a(%a)\n" ireg r1 constant c ireg r2 | Pstfd(r1, c, r2) | Pstfd_a(r1, c, r2) -> @@ -699,7 +803,7 @@ module Target (System : SYSTEM):TARGET = fprintf oc " stwbrx %a, %a, %a\n" ireg r1 ireg r2 ireg r3 | Pstwcx_(r1, r2, r3) -> fprintf oc " stwcx. %a, %a, %a\n" ireg r1 ireg r2 ireg r3 - | Psubfc(r1, r2, r3) -> + | Psubfc(r1, r2, r3) | Psubfc64(r1, r2, r3) -> fprintf oc " subfc %a, %a, %a\n" ireg r1 ireg r2 ireg r3 | Psubfe(r1, r2, r3) -> fprintf oc " subfe %a, %a, %a\n" ireg r1 ireg r2 ireg r3 @@ -707,16 +811,22 @@ module Target (System : SYSTEM):TARGET = fprintf oc " subfze %a, %a\n" ireg r1 ireg r2 | Psubfic(r1, r2, c) -> fprintf oc " subfic %a, %a, %a\n" ireg r1 ireg r2 constant c + | Psubfic64(r1, r2, n) -> + fprintf oc " subfic %a, %a, %Ld\n" ireg r1 ireg r2 (camlint64_of_coqint n) | Psync -> fprintf oc " sync\n" | Ptrap -> fprintf oc " trap\n" - | Pxor(r1, r2, r3) -> + | Pxor(r1, r2, r3) | Pxor64(r1, r2, r3) -> fprintf oc " xor %a, %a, %a\n" ireg r1 ireg r2 ireg r3 | Pxori(r1, r2, c) -> fprintf oc " xori %a, %a, %a\n" ireg r1 ireg r2 constant c + | Pxori64(r1, r2, n) -> + fprintf oc " xori %a, %a, %Ld\n" ireg r1 ireg r2 (camlint64_of_coqint n) | Pxoris(r1, r2, c) -> fprintf oc " xoris %a, %a, %a\n" ireg r1 ireg r2 constant c + | Pxoris64(r1, r2, n) -> + fprintf oc " xoris %a, %a, %Ld\n" ireg r1 ireg r2 (camlint64_of_coqint n) | Plabel lbl -> if (not fallthrough) && !Clflags.option_falignbranchtargets > 0 then fprintf oc " .balign %d\n" !Clflags.option_falignbranchtargets; @@ -826,12 +936,16 @@ module Target (System : SYSTEM):TARGET = let print_fun_info = elf_print_fun_info let emit_constants oc lit = - if !float64_literals <> [] || !float32_literals <> [] then begin + if !float64_literals <> [] || !float32_literals <> [] + || !int64_literals <> [] then begin section oc lit; fprintf oc " .balign 8\n"; + List.iter (print_literal64 oc) !int64_literals; + int64_literals := []; List.iter (print_literal64 oc) !float64_literals; + float64_literals := []; List.iter (print_literal32 oc) !float32_literals; - float64_literals := []; float32_literals := [] + float32_literals := [] end let print_optional_fun_info _ = () diff --git a/powerpc/ValueAOp.v b/powerpc/ValueAOp.v index 8081f557..f7f65e9e 100644 --- a/powerpc/ValueAOp.v +++ b/powerpc/ValueAOp.v @@ -34,6 +34,10 @@ Definition eval_static_condition (cond: condition) (vl: list aval): abool := | Cnotcompf c, v1 :: v2 :: nil => cnot (cmpf_bool c v1 v2) | Cmaskzero n, v1 :: nil => maskzero v1 n | Cmasknotzero n, v1 :: nil => cnot (maskzero v1 n) + | Ccompl c, v1 :: v2 :: nil => cmpl_bool c v1 v2 + | Ccomplu c, v1 :: v2 :: nil => cmplu_bool c v1 v2 + | Ccomplimm c n, v1 :: nil => cmpl_bool c v1 (L n) + | Ccompluimm c n, v1 :: nil => cmplu_bool c v1 (L n) | _, _ => Bnone end. @@ -87,6 +91,33 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Oshru, v1::v2::nil => shru v1 v2 | Orolm amount mask, v1::nil => rolm v1 amount mask | Oroli amount mask, v1::v2::nil => or (and v1 (I (Int.not mask))) (rolm v2 amount mask) + | Olongconst n, nil => L n + | Ocast32signed, v1::nil => longofint v1 + | Ocast32unsigned, v1::nil => longofintu v1 + | Oaddl, v1::v2::nil => addl v1 v2 + | Oaddlimm n, v1::nil => addl v1 (L n) + | Osubl, v1::v2::nil => subl v1 v2 + | Onegl, v1::nil => negl v1 + | Omull, v1::v2::nil => mull v1 v2 + | Omullhs, v1::v2::nil => mullhs v1 v2 + | Omullhu, v1::v2::nil => mullhu v1 v2 + | Odivl, v1::v2::nil => divls v1 v2 + | Odivlu, v1::v2::nil => divlu v1 v2 + | Oandl, v1::v2::nil => andl v1 v2 + | Oandlimm n, v1::nil => andl v1 (L n) + | Oorl, v1::v2::nil => orl v1 v2 + | Oorlimm n, v1::nil => orl v1 (L n) + | Oxorl, v1::v2::nil => xorl v1 v2 + | Oxorlimm n, v1::nil => xorl v1 (L n) + | Onotl, v1::nil => notl v1 + | Oshll, v1::v2::nil => shll v1 v2 + | Oshrl, v1::v2::nil => shrl v1 v2 + | Oshrlimm n, v1::nil => shrl v1 (I n) + | Oshrxlimm n, v1::nil => shrxl v1 (I n) + | Oshrlu, v1::v2::nil => shrlu v1 v2 + | Orolml amount mask, v1::nil => rolml v1 amount mask + | Olongoffloat, v1::nil => longoffloat v1 + | Ofloatoflong, v1::nil => floatoflong v1 | Onegf, v1::nil => negf v1 | Oabsf, v1::nil => absf v1 | Oaddf, v1::v2::nil => addf v1 v2 @@ -177,9 +208,9 @@ Proof. destruct (propagate_float_constants tt); constructor. rewrite Ptrofs.add_zero_l; eauto with va. fold (Val.sub (Vint i) a1). auto with va. + apply rolml_sound; auto. apply floatofwords_sound; auto. apply of_optbool_sound. eapply eval_static_condition_sound; eauto. Qed. End SOUNDNESS. - diff --git a/powerpc/extractionMachdep.v b/powerpc/extractionMachdep.v index b0f05536..b5ae048d 100644 --- a/powerpc/extractionMachdep.v +++ b/powerpc/extractionMachdep.v @@ -24,7 +24,7 @@ Extract Constant Asm.ireg_eq => "fun (x: ireg) (y: ireg) -> x = y". Extract Constant Asm.freg_eq => "fun (x: freg) (y: freg) -> x = y". Extract Constant Asm.preg_eq => "fun (x: preg) (y: preg) -> x = y". -(* Choice of PPC variant *) +(* Choice of PPC splitlong *) Extract Constant Archi.ppc64 => "begin match Configuration.model with | ""ppc64"" -> true |