From 2a0168fea37b68ad14e2cb60bf215111e49d4870 Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 23 Jul 2014 08:54:56 +0000 Subject: Merge of "newspilling" branch: - Support single-precision floats as first-class values - Introduce chunks Many32, Many64 and types Tany32, Tany64 to support saving and restoring registers without knowing the exact types (int/single/float) of their contents, just their sizes. - Memory model: generalize the opaque encoding of pointers to apply to any value, not just pointers, if chunks Many32/Many64 are selected. - More properties of FP arithmetic proved. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2537 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- powerpc/Asm.v | 60 ++++++++++++++++++++++++++++++++++++++++++++++++++--------- 1 file changed, 51 insertions(+), 9 deletions(-) (limited to 'powerpc/Asm.v') diff --git a/powerpc/Asm.v b/powerpc/Asm.v index aba78d45..a7e5eafe 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -165,20 +165,29 @@ Inductive instruction : Type := | Pextsh: ireg -> ireg -> instruction (**r 16-bit sign extension *) | Pfreeframe: Z -> int -> instruction (**r deallocate stack frame and restore previous frame *) | 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 *) | Pfcti: ireg -> freg -> instruction (**r float-to-signed-int conversion *) | Pfdiv: freg -> freg -> freg -> instruction (**r float division *) + | Pfdivs: freg -> freg -> freg -> instruction (**r float division *) | Pfmake: freg -> ireg -> ireg -> instruction (**r build a float from 2 ints *) | Pfmr: freg -> freg -> instruction (**r float move *) | Pfmul: freg -> freg -> freg -> instruction (**r float multiply *) + | Pfmuls: freg -> freg -> freg -> instruction (**r float multiply *) | Pfneg: freg -> freg -> instruction (**r float negation *) + | Pfnegs: freg -> freg -> instruction (**r float negation *) | Pfrsp: freg -> freg -> instruction (**r float round to single precision *) + | Pfxdp: freg -> freg -> instruction (**r float extend to double precision (pseudo) *) | Pfsub: freg -> freg -> freg -> instruction (**r float subtraction *) + | Pfsubs: freg -> freg -> freg -> instruction (**r float subtraction *) | Plbz: ireg -> constant -> ireg -> instruction (**r load 8-bit unsigned int *) | Plbzx: 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 *) + | Plfdx_a: freg -> ireg -> ireg -> instruction (**r same, with 2 index regs *) | Plfs: freg -> constant -> ireg -> instruction (**r load 32-bit float *) | Plfsx: freg -> ireg -> ireg -> instruction (**r same, with 2 index regs *) | Plha: ireg -> constant -> ireg -> instruction (**r load 16-bit signed int *) @@ -186,8 +195,11 @@ Inductive instruction : Type := | Plhz: ireg -> constant -> ireg -> instruction (**r load 16-bit unsigned int *) | Plhzx: ireg -> ireg -> ireg -> instruction (**r same, with 2 index regs *) | 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 *) | Plwzx: ireg -> ireg -> ireg -> instruction (**r same, with 2 index regs *) + | Plwz_a: ireg -> constant -> ireg -> instruction (**r load 32-bit quantity to int reg *) + | Plwzx_a: ireg -> ireg -> ireg -> instruction (**r same, with 2 index regs *) | Pmfcrbit: ireg -> crbit -> instruction (**r move condition bit to reg *) | Pmflr: ireg -> instruction (**r move LR to reg *) | Pmr: ireg -> ireg -> instruction (**r integer move *) @@ -196,7 +208,7 @@ Inductive instruction : Type := | Pmulli: ireg -> ireg -> constant -> instruction (**r integer multiply immediate *) | Pmullw: ireg -> ireg -> ireg -> instruction (**r integer multiply *) | Pmulhw: ireg -> ireg -> ireg -> instruction (**r multiply high signed *) - | Pmulhwu: ireg -> ireg -> ireg -> instruction (**r multiply high signed *) + | Pmulhwu: ireg -> ireg -> ireg -> instruction (**r multiply high signed *) | Pnand: ireg -> ireg -> ireg -> instruction (**r bitwise not-and *) | Pnor: ireg -> ireg -> ireg -> instruction (**r bitwise not-or *) | Por: ireg -> ireg -> ireg -> instruction (**r bitwise or *) @@ -213,12 +225,16 @@ Inductive instruction : Type := | Pstbx: ireg -> ireg -> ireg -> instruction (**r same, with 2 index regs *) | Pstfd: freg -> constant -> ireg -> instruction (**r store 64-bit float *) | Pstfdx: freg -> ireg -> ireg -> instruction (**r same, with 2 index regs *) + | Pstfd_a: freg -> constant -> ireg -> instruction (**r store 64-bit quantity from float reg *) + | Pstfdx_a: freg -> ireg -> ireg -> instruction (**r same, with 2 index regs *) | Pstfs: freg -> constant -> ireg -> instruction (**r store 32-bit float *) | Pstfsx: freg -> ireg -> ireg -> instruction (**r same, with 2 index regs *) | Psth: ireg -> constant -> ireg -> instruction (**r store 16-bit int *) | Psthx: ireg -> ireg -> ireg -> instruction (**r same, with 2 index regs *) | Pstw: ireg -> constant -> ireg -> instruction (**r store 32-bit int *) | Pstwx: ireg -> ireg -> ireg -> instruction (**r same, with 2 index regs *) + | Pstw_a: ireg -> constant -> ireg -> instruction (**r store 32-bit quantity from int reg *) + | Pstwx_a: ireg -> ireg -> ireg -> instruction (**r same, with 2 index regs *) | Psubfc: ireg -> ireg -> ireg -> instruction (**r reversed integer subtraction *) | Psubfe: ireg -> ireg -> ireg -> instruction (**r reversed integer subtraction with carry *) | Psubfic: ireg -> ireg -> constant -> instruction (**r integer subtraction from immediate *) @@ -645,26 +661,40 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out end | Pfabs rd r1 => Next (nextinstr (rs#rd <- (Val.absf rs#r1))) m + | Pfabss rd r1 => + Next (nextinstr (rs#rd <- (Val.absfs rs#r1))) m | Pfadd rd r1 r2 => Next (nextinstr (rs#rd <- (Val.addf rs#r1 rs#r2))) m + | Pfadds rd r1 r2 => + Next (nextinstr (rs#rd <- (Val.addfs rs#r1 rs#r2))) m | Pfcmpu r1 r2 => Next (nextinstr (compare_float rs rs#r1 rs#r2)) m | Pfcti rd r1 => Next (nextinstr (rs#FPR13 <- Vundef #rd <- (Val.maketotal (Val.intoffloat rs#r1)))) m | Pfdiv rd r1 r2 => Next (nextinstr (rs#rd <- (Val.divf rs#r1 rs#r2))) m + | Pfdivs rd r1 r2 => + Next (nextinstr (rs#rd <- (Val.divfs rs#r1 rs#r2))) m | Pfmake rd r1 r2 => Next (nextinstr (rs#rd <- (Val.floatofwords rs#r1 rs#r2))) m | Pfmr rd r1 => Next (nextinstr (rs#rd <- (rs#r1))) m | Pfmul rd r1 r2 => Next (nextinstr (rs#rd <- (Val.mulf rs#r1 rs#r2))) m + | Pfmuls rd r1 r2 => + Next (nextinstr (rs#rd <- (Val.mulfs rs#r1 rs#r2))) m | Pfneg rd r1 => Next (nextinstr (rs#rd <- (Val.negf rs#r1))) m + | Pfnegs rd r1 => + Next (nextinstr (rs#rd <- (Val.negfs rs#r1))) m | Pfrsp rd r1 => Next (nextinstr (rs#rd <- (Val.singleoffloat rs#r1))) m + | Pfxdp rd r1 => + Next (nextinstr (rs#rd <- (Val.floatofsingle rs#r1))) m | Pfsub rd r1 r2 => Next (nextinstr (rs#rd <- (Val.subf rs#r1 rs#r2))) m + | Pfsubs rd r1 r2 => + Next (nextinstr (rs#rd <- (Val.subfs rs#r1 rs#r2))) m | Plbz rd cst r1 => load1 Mint8unsigned rd cst r1 rs m | Plbzx rd r1 r2 => @@ -673,6 +703,10 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out 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_a rd r1 r2 => + load2 Many64 rd r1 r2 rs m | Plfs rd cst r1 => load1 Mfloat32 rd cst r1 rs m | Plfsx rd r1 r2 => @@ -687,10 +721,16 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out load2 Mint16unsigned rd r1 r2 rs m | Plfi rd f => Next (nextinstr (rs #GPR12 <- Vundef #rd <- (Vfloat f))) m + | Plfis rd f => + Next (nextinstr (rs #GPR12 <- Vundef #rd <- (Vsingle f))) m | Plwz rd cst r1 => load1 Mint32 rd cst r1 rs m | Plwzx rd r1 r2 => load2 Mint32 rd r1 r2 rs m + | Plwz_a rd cst r1 => + load1 Many32 rd cst r1 rs m + | Plwzx_a rd r1 r2 => + load2 Many32 rd r1 r2 rs m | Pmfcrbit rd bit => Next (nextinstr (rs#rd <- (rs#(reg_of_crbit bit)))) m | Pmflr rd => @@ -742,16 +782,14 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out store1 Mfloat64 rd cst r1 rs m | Pstfdx rd r1 r2 => store2 Mfloat64 rd r1 r2 rs m + | Pstfd_a rd cst r1 => + store1 Many64 rd cst r1 rs m + | Pstfdx_a rd r1 r2 => + store2 Many64 rd r1 r2 rs m | Pstfs rd cst r1 => - match store1 Mfloat32 rd cst r1 rs m with - | Next rs' m' => Next (rs'#FPR13 <- Vundef) m' - | Stuck => Stuck - end + store1 Mfloat32 rd cst r1 rs m | Pstfsx rd r1 r2 => - match store2 Mfloat32 rd r1 r2 rs m with - | Next rs' m' => Next (rs'#FPR13 <- Vundef) m' - | Stuck => Stuck - end + store2 Mfloat32 rd r1 r2 rs m | Psth rd cst r1 => store1 Mint16unsigned rd cst r1 rs m | Psthx rd r1 r2 => @@ -760,6 +798,10 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out store1 Mint32 rd cst r1 rs m | Pstwx rd r1 r2 => store2 Mint32 rd r1 r2 rs m + | Pstw_a rd cst r1 => + store1 Many32 rd cst r1 rs m + | Pstwx_a rd r1 r2 => + store2 Many32 rd r1 r2 rs m | 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 -- cgit