diff options
| author | Bernhard Schommer <bschommer@users.noreply.github.com> | 2017-05-03 11:18:32 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-05-03 11:18:32 +0200 |
| commit | 7873af34a9520ee5a8a6f10faddf3255a4ff02b2 (patch) | |
| tree | 74500c845c99b39ba91a5507656060dea60404ea /powerpc | |
| parent | 25ea686abc4cce13aba92196dbeb284f727b6e0e (diff) | |
| download | compcert-kvx-7873af34a9520ee5a8a6f10faddf3255a4ff02b2.tar.gz compcert-kvx-7873af34a9520ee5a8a6f10faddf3255a4ff02b2.zip | |
Hybrid 64bit/32bit PowerPC port
This commit adds code generation for 64bit PowerPC architectures which execute
32bit applications.
The main difference to the normal 32bit PowerPC port is that it uses the
available 64bit instructions instead of using the runtime library functions.
However pointers are still 32bit and the 32bit calling convention is used.
In order to use this port the target architecture must be either in Server
execution mode or if in Embedded execution mode the high order 32 bits of GPRs
must be implemented in 32-bit mode. Furthermore the operating system must
preserve the high order 32 bits of GPRs.
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 |