diff options
Diffstat (limited to 'powerpc')
| -rw-r--r-- | powerpc/Archi.v | 14 | ||||
| -rw-r--r-- | powerpc/Asm.v | 60 | ||||
| -rw-r--r-- | powerpc/Asmgen.v | 79 | ||||
| -rw-r--r-- | powerpc/Asmgenproof.v | 14 | ||||
| -rw-r--r-- | powerpc/Asmgenproof1.v | 135 | ||||
| -rw-r--r-- | powerpc/ConstpropOp.vp | 14 | ||||
| -rw-r--r-- | powerpc/ConstpropOpproof.v | 56 | ||||
| -rw-r--r-- | powerpc/Machregs.v | 37 | ||||
| -rw-r--r-- | powerpc/NeedOp.v | 8 | ||||
| -rw-r--r-- | powerpc/Op.v | 137 | ||||
| -rw-r--r-- | powerpc/PrintAsm.ml | 77 | ||||
| -rw-r--r-- | powerpc/SelectOp.vp | 29 | ||||
| -rw-r--r-- | powerpc/SelectOpproof.v | 124 | ||||
| -rw-r--r-- | powerpc/Unusedglob1.ml | 4 | ||||
| -rw-r--r-- | powerpc/ValueAOp.v | 9 | ||||
| -rw-r--r-- | powerpc/eabi/Conventions1.v | 64 |
16 files changed, 550 insertions, 311 deletions
diff --git a/powerpc/Archi.v b/powerpc/Archi.v index 0b871d9..070f7cc 100644 --- a/powerpc/Archi.v +++ b/powerpc/Archi.v @@ -25,10 +25,18 @@ Definition big_endian := true. Notation align_int64 := 8%Z (only parsing). Notation align_float64 := 8%Z (only parsing). -Program Definition default_pl : bool * nan_pl 53 := +Program Definition default_pl_64 : bool * nan_pl 53 := (false, nat_iter 51 xO xH). -Definition choose_binop_pl (s1: bool) (pl1: nan_pl 53) (s2: bool) (pl2: nan_pl 53) := +Definition choose_binop_pl_64 (s1: bool) (pl1: nan_pl 53) (s2: bool) (pl2: nan_pl 53) := false. (**r always choose first NaN *) -Global Opaque big_endian default_pl choose_binop_pl. +Program Definition default_pl_32 : bool * nan_pl 24 := + (false, nat_iter 22 xO xH). + +Definition choose_binop_pl_32 (s1: bool) (pl1: nan_pl 24) (s2: bool) (pl2: nan_pl 24) := + false. (**r always choose first NaN *) + +Global Opaque big_endian + default_pl_64 choose_binop_pl_64 + default_pl_32 choose_binop_pl_32. diff --git a/powerpc/Asm.v b/powerpc/Asm.v index aba78d4..a7e5eaf 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 diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v index 6b66686..5ca770d 100644 --- a/powerpc/Asmgen.v +++ b/powerpc/Asmgen.v @@ -122,40 +122,32 @@ Definition rolm (r1 r2: ireg) (amount mask: int) (k: code) := (** Accessing slots in the stack frame. *) +Definition accessind {A: Type} + (instr1: A -> constant -> ireg -> instruction) + (instr2: A -> ireg -> ireg -> instruction) + (base: ireg) (ofs: int) (r: A) (k: code) := + if Int.eq (high_s ofs) Int.zero + then instr1 r (Cint ofs) base :: k + else loadimm GPR0 ofs (instr2 r base GPR0 :: k). + Definition loadind (base: ireg) (ofs: int) (ty: typ) (dst: mreg) (k: code) := - match ty with - | Tint => - do r <- ireg_of dst; - OK (if Int.eq (high_s ofs) Int.zero then - Plwz r (Cint ofs) base :: k - else - loadimm GPR0 ofs (Plwzx r base GPR0 :: k)) - | Tfloat => - do r <- freg_of dst; - OK (if Int.eq (high_s ofs) Int.zero then - Plfd r (Cint ofs) base :: k - else - loadimm GPR0 ofs (Plfdx r base GPR0 :: k)) - | Tlong | Tsingle => - Error (msg "Asmgen.loadind") + match ty, preg_of dst with + | 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) + | Tfloat, FR r => OK(accessind Plfd Plfdx base ofs r k) + | Tany64, FR r => OK(accessind Plfd_a Plfdx_a base ofs r k) + | _, _ => Error (msg "Asmgen.loadind") end. Definition storeind (src: mreg) (base: ireg) (ofs: int) (ty: typ) (k: code) := - match ty with - | Tint => - do r <- ireg_of src; - OK (if Int.eq (high_s ofs) Int.zero then - Pstw r (Cint ofs) base :: k - else - loadimm GPR0 ofs (Pstwx r base GPR0 :: k)) - | Tfloat => - do r <- freg_of src; - OK (if Int.eq (high_s ofs) Int.zero then - Pstfd r (Cint ofs) base :: k - else - loadimm GPR0 ofs (Pstfdx r base GPR0 :: k)) - | Tlong | Tsingle => - Error (msg "Asmgen.storeind") + match ty, preg_of src with + | 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) + | Tfloat, FR r => OK(accessind Pstfd Pstfdx base ofs r k) + | Tany64, FR r => OK(accessind Pstfd_a Pstfdx_a base ofs r k) + | _, _ => Error (msg "Asmgen.storeind") end. (** Constructor for a floating-point comparison. The PowerPC has @@ -340,6 +332,8 @@ Definition transl_op do r <- ireg_of res; OK (loadimm r n k) | Ofloatconst f, nil => do r <- freg_of res; OK (Plfi r f :: k) + | Osingleconst f, nil => + do r <- freg_of res; OK (Plfis r f :: k) | Oaddrsymbol s ofs, nil => do r <- ireg_of res; OK (if symbol_is_small_data s ofs then @@ -477,9 +471,30 @@ Definition transl_op | Odivf, a1 :: a2 :: nil => do r1 <- freg_of a1; do r2 <- freg_of a2; do r <- freg_of res; OK (Pfdiv r r1 r2 :: k) + | Onegfs, a1 :: nil => + do r1 <- freg_of a1; do r <- freg_of res; + OK (Pfnegs r r1 :: k) + | Oabsfs, a1 :: nil => + do r1 <- freg_of a1; do r <- freg_of res; + OK (Pfabss r r1 :: k) + | Oaddfs, a1 :: a2 :: nil => + do r1 <- freg_of a1; do r2 <- freg_of a2; do r <- freg_of res; + OK (Pfadds r r1 r2 :: k) + | Osubfs, a1 :: a2 :: nil => + do r1 <- freg_of a1; do r2 <- freg_of a2; do r <- freg_of res; + OK (Pfsubs r r1 r2 :: k) + | Omulfs, a1 :: a2 :: nil => + do r1 <- freg_of a1; do r2 <- freg_of a2; do r <- freg_of res; + OK (Pfmuls r r1 r2 :: k) + | Odivfs, a1 :: a2 :: nil => + do r1 <- freg_of a1; do r2 <- freg_of a2; do r <- freg_of res; + OK (Pfdivs r r1 r2 :: k) | Osingleoffloat, a1 :: nil => do r1 <- freg_of a1; do r <- freg_of res; OK (Pfrsp r r1 :: k) + | Ofloatofsingle, a1 :: nil => + do r1 <- freg_of a1; do r <- freg_of res; + OK (Pfxdp r r1 :: k) | Ointoffloat, a1 :: nil => do r1 <- freg_of a1; do r <- ireg_of res; OK (Pfcti r r1 :: k) @@ -566,7 +581,7 @@ Definition transl_load (chunk: memory_chunk) (addr: addressing) | Mfloat64 => do r <- freg_of dst; transl_memory_access (Plfd r) (Plfdx r) addr args GPR12 k - | Mint64 => + | _ => Error (msg "Asmgen.transl_load") end. @@ -589,7 +604,7 @@ Definition transl_store (chunk: memory_chunk) (addr: addressing) | Mfloat64 => do r <- freg_of src; transl_memory_access (Pstfd r) (Pstfdx r) addr args temp k - | Mint64 => + | _ => Error (msg "Asmgen.transl_store") end. diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v index 879d752..913fb50 100644 --- a/powerpc/Asmgenproof.v +++ b/powerpc/Asmgenproof.v @@ -196,17 +196,21 @@ Remark loadind_label: forall base ofs ty dst k c, loadind base ofs ty dst k = OK c -> tail_nolabel k c. Proof. - unfold loadind; intros. - destruct ty; destruct (Int.eq (high_s ofs) Int.zero); + unfold loadind, accessind; intros. + destruct ty; try discriminate; + destruct (preg_of dst); try discriminate; + destruct (Int.eq (high_s ofs) Int.zero); TailNoLabel; eapply tail_nolabel_trans; TailNoLabel. Qed. Remark storeind_label: forall base ofs ty src k c, - storeind base src ofs ty k = OK c -> tail_nolabel k c. + storeind src base ofs ty k = OK c -> tail_nolabel k c. Proof. - unfold storeind; intros. - destruct ty; destruct (Int.eq (high_s ofs) Int.zero); + unfold storeind, accessind; intros. + destruct ty; try discriminate; + destruct (preg_of src); try discriminate; + destruct (Int.eq (high_s ofs) Int.zero); TailNoLabel; eapply tail_nolabel_trans; TailNoLabel. Qed. diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v index cfeb823..e1ab9a1 100644 --- a/powerpc/Asmgenproof1.v +++ b/powerpc/Asmgenproof1.v @@ -435,6 +435,36 @@ Qed. (** Indexed memory loads. *) +Lemma accessind_load_correct: + forall (A: Type) (inj: A -> preg) + (instr1: A -> constant -> ireg -> instruction) + (instr2: A -> ireg -> ireg -> instruction) + (base: ireg) ofs rx chunk v (rs: regset) m k, + (forall rs m r1 cst r2, + exec_instr ge fn (instr1 r1 cst r2) rs m = load1 ge chunk (inj r1) cst r2 rs m) -> + (forall rs m r1 r2 r3, + exec_instr ge fn (instr2 r1 r2 r3) rs m = load2 chunk (inj r1) r2 r3 rs m) -> + Mem.loadv chunk m (Val.add rs#base (Vint ofs)) = Some v -> + base <> GPR0 -> inj rx <> PC -> + exists rs', + exec_straight ge fn (accessind instr1 instr2 base ofs rx k) rs m k rs' m + /\ rs'#(inj rx) = v + /\ forall r, r <> PC -> r <> inj rx -> r <> GPR0 -> rs'#r = rs#r. +Proof. + intros. unfold accessind. destruct (Int.eq (high_s ofs) Int.zero). +- econstructor; split. apply exec_straight_one. + rewrite H. unfold load1. rewrite gpr_or_zero_not_zero by auto. simpl. + rewrite H1. eauto. unfold nextinstr. repeat Simplif. + split. unfold nextinstr. repeat Simplif. + intros. repeat Simplif. +- exploit (loadimm_correct GPR0 ofs); eauto. intros [rs' [P [Q R]]]. + econstructor; split. eapply exec_straight_trans. eexact P. + apply exec_straight_one. rewrite H0. unfold load2. rewrite Q, R by auto with asmgen. + rewrite H1. reflexivity. unfold nextinstr. repeat Simplif. + split. repeat Simplif. + intros. repeat Simplif. +Qed. + Lemma loadind_correct: forall (base: ireg) ofs ty dst k (rs: regset) m v c, loadind base ofs ty dst k = OK c -> @@ -445,38 +475,44 @@ Lemma loadind_correct: /\ rs'#(preg_of dst) = v /\ forall r, r <> PC -> r <> preg_of dst -> r <> GPR0 -> rs'#r = rs#r. Proof. -Opaque Int.eq. - unfold loadind; intros. destruct ty; monadInv H; simpl in H0. -(* integer *) - rewrite (ireg_of_eq _ _ EQ). - destruct (Int.eq (high_s ofs) Int.zero). - (* one load *) - econstructor; split. apply exec_straight_one. simpl. - unfold load1. rewrite gpr_or_zero_not_zero; auto. simpl. rewrite H0. eauto. auto. - intuition Simpl. - (* loadimm + load *) - exploit (loadimm_correct GPR0 ofs); eauto. intros [rs' [A [B C]]]. - exists (nextinstr (rs'#x <- v)); split. - eapply exec_straight_trans. eexact A. apply exec_straight_one; auto. - simpl. unfold load2. rewrite C; auto with asmgen. rewrite B. rewrite H0. auto. - intuition Simpl. -(* float *) - rewrite (freg_of_eq _ _ EQ). - destruct (Int.eq (high_s ofs) Int.zero). - (* one load *) - econstructor; split. apply exec_straight_one. simpl. - unfold load1. rewrite gpr_or_zero_not_zero; auto. simpl. rewrite H0. eauto. auto. - intuition Simpl. - (* loadimm + load *) - exploit (loadimm_correct GPR0 ofs); eauto. intros [rs' [A [B C]]]. - exists (nextinstr (rs'#x <- v)); split. - eapply exec_straight_trans. eexact A. apply exec_straight_one; auto. - simpl. unfold load2. rewrite C; auto with asmgen. rewrite B. rewrite H0. auto. - intuition Simpl. + 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 := FR) (chunk := Mfloat32); auto with asmgen. + apply accessind_load_correct with (inj := IR) (chunk := Many32); auto with asmgen. + apply accessind_load_correct with (inj := FR) (chunk := Many64); auto with asmgen. Qed. (** Indexed memory stores. *) +Lemma accessind_store_correct: + forall (A: Type) (inj: A -> preg) + (instr1: A -> constant -> ireg -> instruction) + (instr2: A -> ireg -> ireg -> instruction) + (base: ireg) ofs rx chunk (rs: regset) m m' k, + (forall rs m r1 cst r2, + exec_instr ge fn (instr1 r1 cst r2) rs m = store1 ge chunk (inj r1) cst r2 rs m) -> + (forall rs m r1 r2 r3, + exec_instr ge fn (instr2 r1 r2 r3) rs m = store2 chunk (inj r1) r2 r3 rs m) -> + Mem.storev chunk m (Val.add rs#base (Vint ofs)) (rs (inj rx)) = Some m' -> + base <> GPR0 -> inj rx <> PC -> inj rx <> GPR0 -> + exists rs', + exec_straight ge fn (accessind instr1 instr2 base ofs rx k) rs m k rs' m' + /\ forall r, r <> PC -> r <> GPR0 -> rs'#r = rs#r. +Proof. + intros. unfold accessind. destruct (Int.eq (high_s ofs) Int.zero). +- econstructor; split. apply exec_straight_one. + rewrite H. unfold store1. rewrite gpr_or_zero_not_zero by auto. simpl. + rewrite H1. eauto. unfold nextinstr. repeat Simplif. + intros. repeat Simplif. +- exploit (loadimm_correct GPR0 ofs); eauto. intros [rs' [P [Q R]]]. + econstructor; split. eapply exec_straight_trans. eexact P. + apply exec_straight_one. rewrite H0. unfold store2. + rewrite Q. rewrite R by auto with asmgen. rewrite R by auto. + rewrite H1. reflexivity. unfold nextinstr. repeat Simplif. + intros. repeat Simplif. +Qed. + Lemma storeind_correct: forall (base: ireg) ofs ty src k (rs: regset) m m' c, storeind src base ofs ty k = OK c -> @@ -488,33 +524,12 @@ Lemma storeind_correct: Proof. unfold storeind; intros. assert (preg_of src <> GPR0) by auto with asmgen. - destruct ty; monadInv H; simpl in H0. -(* integer *) - rewrite (ireg_of_eq _ _ EQ) in *. - destruct (Int.eq (high_s ofs) Int.zero). - (* one store *) - econstructor; split. apply exec_straight_one. simpl. - unfold store1. rewrite gpr_or_zero_not_zero; auto. simpl. rewrite H0. eauto. auto. - intros; Simpl. - (* loadimm + store *) - exploit (loadimm_correct GPR0 ofs); eauto. intros [rs' [A [B C]]]. - exists (nextinstr rs'); split. - eapply exec_straight_trans. eexact A. apply exec_straight_one; auto. - simpl. unfold store2. rewrite B. rewrite ! C; auto with asmgen. rewrite H0. auto. - intuition Simpl. -(* float *) - rewrite (freg_of_eq _ _ EQ) in *. - destruct (Int.eq (high_s ofs) Int.zero). - (* one store *) - econstructor; split. apply exec_straight_one. simpl. - unfold store1. rewrite gpr_or_zero_not_zero; auto. simpl. rewrite H0. eauto. auto. - intuition Simpl. - (* loadimm + store *) - exploit (loadimm_correct GPR0 ofs); eauto. intros [rs' [A [B C]]]. - exists (nextinstr rs'); split. - eapply exec_straight_trans. eexact A. apply exec_straight_one; auto. - simpl. unfold store2. rewrite B. rewrite ! C; auto with asmgen. rewrite H0. auto. - intuition Simpl. + 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 := FR) (chunk := Mfloat32); auto with asmgen. + apply accessind_store_correct with (inj := IR) (chunk := Many32); auto with asmgen. + apply accessind_store_correct with (inj := FR) (chunk := Many64); auto with asmgen. Qed. (** Float comparisons. *) @@ -1210,15 +1225,7 @@ Local Transparent destroyed_by_store. - (* Mint32 *) eapply BASE; eauto; erewrite ireg_of_eq by eauto; auto. - (* Mfloat32 *) - rewrite (freg_of_eq _ _ EQ) in H1. - eapply transl_memory_access_correct. eauto. eauto. eauto. - intros. econstructor; split. apply exec_straight_one. - simpl. unfold store1. rewrite H. rewrite H2; auto with asmgen. rewrite H1. eauto. auto. -Local Transparent destroyed_by_store. - simpl; intros. destruct H5 as [A [B C]]. Simpl. apply H2; auto with asmgen. destruct TEMP0; congruence. - intros. econstructor; split. apply exec_straight_one. - simpl. unfold store2. rewrite H. rewrite H2; auto with asmgen. rewrite H1. eauto. auto. - simpl; intros. destruct H5 as [A [B C]]. Simpl. apply H2; auto with asmgen. destruct TEMP0; congruence. + eapply BASE; eauto; erewrite freg_of_eq by eauto; auto. - (* Mfloat64 *) eapply BASE; eauto; erewrite freg_of_eq by eauto; auto. Qed. diff --git a/powerpc/ConstpropOp.vp b/powerpc/ConstpropOp.vp index e1e1960..bba0fad 100644 --- a/powerpc/ConstpropOp.vp +++ b/powerpc/ConstpropOp.vp @@ -136,18 +136,19 @@ Definition make_xorimm (n: int) (r: reg) := else (Oxorimm n, r :: nil). Definition make_mulfimm (n: float) (r r1 r2: reg) := - if Float.eq_dec n (Float.floatofint (Int.repr 2)) + if Float.eq_dec n (Float.of_int (Int.repr 2)) then (Oaddf, r :: r :: nil) else (Omulf, r1 :: r2 :: nil). +Definition make_mulfsimm (n: float32) (r r1 r2: reg) := + if Float32.eq_dec n (Float32.of_int (Int.repr 2)) + then (Oaddfs, r :: r :: nil) + else (Omulfs, r1 :: r2 :: nil). + Definition make_cast8signed (r: reg) (a: aval) := if vincl a (Sgn 8) then (Omove, r :: nil) else (Ocast8signed, r :: nil). Definition make_cast16signed (r: reg) (a: aval) := if vincl a (Sgn 16) then (Omove, r :: nil) else (Ocast16signed, r :: nil). -Definition make_singleoffloat (r: reg) (a: aval) := - if vincl a Fsingle && generate_float_constants tt - then (Omove, r :: nil) - else (Osingleoffloat, r :: nil). Nondetfunction op_strength_reduction (op: operation) (args: list reg) (vl: list aval) := @@ -174,10 +175,11 @@ Nondetfunction op_strength_reduction | Oshl, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shlimm n2 r1 r2 | Oshr, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shrimm n2 r1 r2 | Oshru, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shruimm n2 r1 r2 - | Osingleoffloat, r1 :: nil, v1 :: nil => make_singleoffloat r1 v1 | Ocmp c, args, vl => make_cmp c args vl | Omulf, r1 :: r2 :: nil, v1 :: F n2 :: nil => make_mulfimm n2 r1 r1 r2 | Omulf, r1 :: r2 :: nil, F n1 :: v2 :: nil => make_mulfimm n1 r2 r1 r2 + | Omulfs, r1 :: r2 :: nil, v1 :: FS n2 :: nil => make_mulfsimm n2 r1 r1 r2 + | Omulfs, r1 :: r2 :: nil, FS n1 :: v2 :: nil => make_mulfsimm n1 r2 r1 r2 | _, _, _ => (op, args) end. diff --git a/powerpc/ConstpropOpproof.v b/powerpc/ConstpropOpproof.v index 584865a..8498868 100644 --- a/powerpc/ConstpropOpproof.v +++ b/powerpc/ConstpropOpproof.v @@ -80,6 +80,10 @@ Ltac SimplVM := let E := fresh in assert (E: v = Vfloat n) by (inversion H; auto); rewrite E in *; clear H; SimplVM + | [ H: vmatch _ ?v (FS ?n) |- _ ] => + let E := fresh in + assert (E: v = Vsingle n) by (inversion H; auto); + rewrite E in *; clear H; SimplVM | [ H: vmatch _ ?v (Ptr(Gl ?id ?ofs)) |- _ ] => let E := fresh in assert (E: Val.lessdef v (Genv.symbol_address ge id ofs)) by (eapply vmatch_ptr_gl; eauto); @@ -315,7 +319,7 @@ Lemma make_mulfimm_correct: exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.mulf rs#r1 rs#r2) v. Proof. intros; unfold make_mulfimm. - destruct (Float.eq_dec n (Float.floatofint (Int.repr 2))); intros. + destruct (Float.eq_dec n (Float.of_int (Int.repr 2))); intros. simpl. econstructor; split. eauto. rewrite H; subst n. destruct (rs#r1); simpl; auto. rewrite Float.mul2_add; auto. simpl. econstructor; split; eauto. @@ -328,13 +332,40 @@ Lemma make_mulfimm_correct_2: exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.mulf rs#r1 rs#r2) v. Proof. intros; unfold make_mulfimm. - destruct (Float.eq_dec n (Float.floatofint (Int.repr 2))); intros. + destruct (Float.eq_dec n (Float.of_int (Int.repr 2))); intros. simpl. econstructor; split. eauto. rewrite H; subst n. destruct (rs#r2); simpl; auto. rewrite Float.mul2_add; auto. rewrite Float.mul_commut; auto. simpl. econstructor; split; eauto. Qed. +Lemma make_mulfsimm_correct: + forall n r1 r2, + rs#r2 = Vsingle n -> + let (op, args) := make_mulfsimm n r1 r1 r2 in + exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.mulfs rs#r1 rs#r2) v. +Proof. + intros; unfold make_mulfsimm. + destruct (Float32.eq_dec n (Float32.of_int (Int.repr 2))); intros. + simpl. econstructor; split. eauto. rewrite H; subst n. + destruct (rs#r1); simpl; auto. rewrite Float32.mul2_add; auto. + simpl. econstructor; split; eauto. +Qed. + +Lemma make_mulfsimm_correct_2: + forall n r1 r2, + rs#r1 = Vsingle n -> + let (op, args) := make_mulfsimm n r2 r1 r2 in + exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.mulfs rs#r1 rs#r2) v. +Proof. + intros; unfold make_mulfsimm. + destruct (Float32.eq_dec n (Float32.of_int (Int.repr 2))); intros. + simpl. econstructor; split. eauto. rewrite H; subst n. + destruct (rs#r2); simpl; auto. rewrite Float32.mul2_add; auto. + rewrite Float32.mul_commut; auto. + simpl. econstructor; split; eauto. +Qed. + Lemma make_cast8signed_correct: forall r x, vmatch bc rs#r x -> @@ -363,21 +394,6 @@ Proof. econstructor; split; simpl; eauto. Qed. -Lemma make_singleoffloat_correct: - forall r x, - vmatch bc rs#r x -> - let (op, args) := make_singleoffloat r x in - exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.singleoffloat rs#r) v. -Proof. - intros; unfold make_singleoffloat. - destruct (vincl x Fsingle && generate_float_constants tt) eqn:INCL. - InvBooleans. exists rs#r; split; auto. - assert (V: vmatch bc rs#r Fsingle). - { eapply vmatch_ge; eauto. apply vincl_ge; auto. } - inv V; simpl; auto. rewrite Float.singleoffloat_of_single by auto. auto. - econstructor; split; simpl; eauto. -Qed. - Lemma op_strength_reduction_correct: forall op args vl v, vl = map (fun r => AE.get r ae) args -> @@ -424,14 +440,16 @@ Proof. InvApproxRegs; SimplVM; inv H0. apply make_shrimm_correct; auto. (* shru *) InvApproxRegs; SimplVM; inv H0. apply make_shruimm_correct; auto. -(* singleoffloat *) - InvApproxRegs; SimplVM; inv H0. apply make_singleoffloat_correct; auto. (* cmp *) inv H0. apply make_cmp_correct; auto. (* mulf *) InvApproxRegs; SimplVM; inv H0. rewrite <- H2. apply make_mulfimm_correct; auto. InvApproxRegs; SimplVM; inv H0. fold (Val.mulf (Vfloat n1) rs#r2). rewrite <- H2. apply make_mulfimm_correct_2; auto. +(* mulfs *) + InvApproxRegs; SimplVM; inv H0. rewrite <- H2. apply make_mulfsimm_correct; auto. + InvApproxRegs; SimplVM; inv H0. fold (Val.mulfs (Vsingle n1) rs#r2). + rewrite <- H2. apply make_mulfsimm_correct_2; auto. (* default *) exists v; auto. Qed. diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v index baad496..f7ed779 100644 --- a/powerpc/Machregs.v +++ b/powerpc/Machregs.v @@ -54,23 +54,13 @@ Global Opaque mreg_eq. Definition mreg_type (r: mreg): typ := match r with - | R3 => Tint | R4 => Tint | R5 => Tint | R6 => Tint - | R7 => Tint | R8 => Tint | R9 => Tint | R10 => Tint - | R11 => Tint | R12 => Tint - | R14 => Tint | R15 => Tint | R16 => Tint - | R17 => Tint | R18 => Tint | R19 => Tint | R20 => Tint - | R21 => Tint | R22 => Tint | R23 => Tint | R24 => Tint - | R25 => Tint | R26 => Tint | R27 => Tint | R28 => Tint - | R29 => Tint | R30 => Tint | R31 => Tint - | F0 => Tfloat - | F1 => Tfloat | F2 => Tfloat | F3 => Tfloat | F4 => Tfloat - | F5 => Tfloat | F6 => Tfloat | F7 => Tfloat | F8 => Tfloat - | F9 => Tfloat | F10 => Tfloat | F11 => Tfloat | F12 => Tfloat - | F13 => Tfloat | F14 => Tfloat | F15 => Tfloat - | F16 => Tfloat | F17 => Tfloat | F18 => Tfloat | F19 => Tfloat - | F20 => Tfloat | F21 => Tfloat | F22 => Tfloat | F23 => Tfloat - | F24 => Tfloat | F25 => Tfloat | F26 => Tfloat | F27 => Tfloat - | F28 => Tfloat | F29 => Tfloat | F30 => Tfloat | F31 => Tfloat + | 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. Open Scope positive_scope. @@ -112,6 +102,7 @@ Definition is_stack_reg (r: mreg) : bool := false. Definition destroyed_by_op (op: operation): list mreg := match op with | Ofloatconst _ => R12 :: nil + | Osingleconst _ => R12 :: nil | Ointoffloat => F13 :: nil | _ => nil end. @@ -120,10 +111,7 @@ Definition destroyed_by_load (chunk: memory_chunk) (addr: addressing): list mreg R12 :: nil. Definition destroyed_by_store (chunk: memory_chunk) (addr: addressing): list mreg := - match chunk with - | Mfloat32 => R11 :: R12 :: F13 :: nil - | _ => R11 :: R12 :: nil - end. + R11 :: R12 :: nil. Definition destroyed_by_cond (cond: condition): list mreg := nil. @@ -135,21 +123,16 @@ Definition destroyed_by_builtin (ef: external_function): list mreg := match ef with | EF_builtin _ _ => F13 :: nil | EF_vload _ => nil - | EF_vstore Mfloat32 => F13 :: nil | EF_vstore _ => nil | EF_vload_global _ _ _ => R11 :: nil | EF_vstore_global Mint64 _ _ => R10 :: R11 :: R12 :: nil - | EF_vstore_global Mfloat32 _ _ => R11 :: R12 :: F13 :: nil | EF_vstore_global _ _ _ => R11 :: R12 :: nil | EF_memcpy _ _ => R11 :: R12 :: F13 :: nil | _ => nil end. Definition destroyed_by_setstack (ty: typ): list mreg := - match ty with - | Tsingle => F13 :: nil - | _ => nil - end. + nil. Definition destroyed_at_function_entry: list mreg := nil. diff --git a/powerpc/NeedOp.v b/powerpc/NeedOp.v index d43af3c..e130749 100644 --- a/powerpc/NeedOp.v +++ b/powerpc/NeedOp.v @@ -25,6 +25,7 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | Omove => op1 nv | Ointconst n => nil | Ofloatconst n => nil + | Osingleconst n => nil | Oaddrsymbol id ofs => nil | Oaddrstack ofs => nil | Ocast8signed => op1 (sign_ext 8 nv) @@ -52,7 +53,9 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | Oroli amount mask => op1 (default nv) | Onegf | Oabsf => op1 (default nv) | Oaddf | Osubf | Omulf | Odivf => op2 (default nv) - | Osingleoffloat => op1 (singleoffloat nv) + | Onegfs | Oabsfs => op1 (default nv) + | Oaddfs | Osubfs | Omulfs | Odivfs => op2 (default nv) + | Osingleoffloat | Ofloatofsingle => op1 (default nv) | Ointoffloat => op1 (default nv) | Ofloatofwords | Omakelong => op2 (default nv) | Olowlong | Ohighlong => op1 (default nv) @@ -66,7 +69,6 @@ Definition operation_is_redundant (op: operation) (nv: nval): bool := | Oandimm n => andimm_redundant nv n | Oorimm n => orimm_redundant nv n | Orolm amount mask => rolm_redundant nv amount mask - | Osingleoffloat => singleoffloat_redundant nv | _ => false end. @@ -136,7 +138,6 @@ Proof. - apply or_sound; auto. apply notint_sound; rewrite bitwise_idem; auto. - apply shrimm_sound; auto. - apply rolm_sound; auto. -- apply singleoffloat_sound; auto. - destruct (eval_condition c args m) as [b|] eqn:EC; simpl in H2. erewrite needs_of_condition_sound by eauto. subst v; simpl. auto with na. @@ -156,7 +157,6 @@ Proof. - apply andimm_redundant_sound; auto. - apply orimm_redundant_sound; auto. - apply rolm_redundant_sound; auto. -- apply singleoffloat_redundant_sound; auto. Qed. End SOUNDNESS. diff --git a/powerpc/Op.v b/powerpc/Op.v index 17cf072..dbec275 100644 --- a/powerpc/Op.v +++ b/powerpc/Op.v @@ -54,6 +54,7 @@ Inductive operation : Type := | Omove: operation (**r [rd = r1] *) | Ointconst: int -> operation (**r [rd] is set to the given integer constant *) | 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 -> int -> operation (**r [rd] is set to the the address of the symbol plus the offset *) | Oaddrstack: int -> operation (**r [rd] is set to the stack pointer plus the given offset *) (*c Integer arithmetic: *) @@ -96,7 +97,14 @@ Inductive operation : Type := | Osubf: operation (**r [rd = r1 - r2] *) | Omulf: operation (**r [rd = r1 * r2] *) | Odivf: operation (**r [rd = r1 / r2] *) + | Onegfs: operation (**r [rd = - r1] *) + | Oabsfs: operation (**r [rd = abs(r1)] *) + | Oaddfs: operation (**r [rd = r1 + r2] *) + | Osubfs: operation (**r [rd = r1 - r2] *) + | Omulfs: operation (**r [rd = r1 * r2] *) + | Odivfs: operation (**r [rd = r1 / r2] *) | Osingleoffloat: operation (**r [rd] is [r1] truncated to single-precision float *) + | Ofloatofsingle: operation (**r [rd] is [r1] extended to double-precision float *) (*c Conversions between int and float: *) | Ointoffloat: operation (**r [rd = signed_int_of_float(r1)] *) | Ofloatofwords: operation (**r [rd = float_of_words(r1,r2)] *) @@ -130,7 +138,7 @@ Defined. Definition eq_operation (x y: operation): {x=y} + {x<>y}. Proof. generalize Int.eq_dec; intro. - generalize Float.eq_dec; intro. + generalize Float.eq_dec Float32.eq_dec; intros. assert (forall (x y: ident), {x=y}+{x<>y}). exact peq. generalize eq_condition; intro. decide equality. @@ -172,6 +180,7 @@ Definition eval_operation | Omove, v1::nil => Some v1 | Ointconst n, nil => Some (Vint n) | Ofloatconst n, nil => Some (Vfloat n) + | Osingleconst n, nil => Some (Vsingle n) | Oaddrsymbol s ofs, nil => Some (Genv.symbol_address genv s ofs) | Oaddrstack ofs, nil => Some (Val.add sp (Vint ofs)) | Ocast8signed, v1::nil => Some (Val.sign_ext 8 v1) @@ -213,7 +222,14 @@ Definition eval_operation | Osubf, v1::v2::nil => Some(Val.subf v1 v2) | Omulf, v1::v2::nil => Some(Val.mulf v1 v2) | Odivf, v1::v2::nil => Some(Val.divf v1 v2) + | Onegfs, v1::nil => Some(Val.negfs v1) + | Oabsfs, v1::nil => Some(Val.absfs v1) + | Oaddfs, v1::v2::nil => Some(Val.addfs v1 v2) + | Osubfs, v1::v2::nil => Some(Val.subfs v1 v2) + | Omulfs, v1::v2::nil => Some(Val.mulfs v1 v2) + | Odivfs, v1::v2::nil => Some(Val.divfs v1 v2) | Osingleoffloat, v1::nil => Some(Val.singleoffloat v1) + | Ofloatofsingle, v1::nil => Some(Val.floatofsingle v1) | Ointoffloat, v1::nil => Val.intoffloat v1 | Ofloatofwords, v1::v2::nil => Some(Val.floatofwords v1 v2) | Omakelong, v1::v2::nil => Some(Val.longofwords v1 v2) @@ -265,7 +281,8 @@ Definition type_of_operation (op: operation) : list typ * typ := match op with | Omove => (nil, Tint) (* treated specially *) | Ointconst _ => (nil, Tint) - | Ofloatconst f => (nil, if Float.is_single_dec f then Tsingle else Tfloat) + | Ofloatconst f => (nil, Tfloat) + | Osingleconst f => (nil, Tsingle) | Oaddrsymbol _ _ => (nil, Tint) | Oaddrstack _ => (nil, Tint) | Ocast8signed => (Tint :: nil, Tint) @@ -306,7 +323,14 @@ Definition type_of_operation (op: operation) : list typ * typ := | Osubf => (Tfloat :: Tfloat :: nil, Tfloat) | Omulf => (Tfloat :: Tfloat :: nil, Tfloat) | Odivf => (Tfloat :: Tfloat :: nil, Tfloat) + | Onegfs => (Tsingle :: nil, Tsingle) + | Oabsfs => (Tsingle :: nil, Tsingle) + | Oaddfs => (Tsingle :: Tsingle :: nil, Tsingle) + | Osubfs => (Tsingle :: Tsingle :: nil, Tsingle) + | Omulfs => (Tsingle :: Tsingle :: nil, Tsingle) + | Odivfs => (Tsingle :: Tsingle :: nil, Tsingle) | Osingleoffloat => (Tfloat :: nil, Tsingle) + | Ofloatofsingle => (Tsingle :: nil, Tfloat) | Ointoffloat => (Tfloat :: nil, Tint) | Ofloatofwords => (Tint :: Tint :: nil, Tfloat) | Omakelong => (Tint :: Tint :: nil, Tlong) @@ -343,7 +367,8 @@ Proof with (try exact I). destruct op; simpl in H0; FuncInv; subst; simpl. congruence. exact I. - destruct (Float.is_single_dec f); auto. + auto. + auto. unfold Genv.symbol_address. destruct (Genv.find_symbol genv i)... destruct sp... destruct v0... @@ -386,8 +411,15 @@ Proof with (try exact I). destruct v0; destruct v1... destruct v0; destruct v1... destruct v0; destruct v1... - destruct v0... simpl. apply Float.singleoffloat_is_single. - destruct v0; simpl in H0; inv H0. destruct (Float.intoffloat f); inv H2... + destruct v0... + destruct v0... + destruct v0; destruct v1... + destruct v0; destruct v1... + destruct v0; destruct v1... + destruct v0; destruct v1... + destruct v0... + destruct v0... + destruct v0; simpl in H0; inv H0. destruct (Float.to_int f); inv H2... destruct v0; destruct v1... destruct v0; destruct v1... destruct v0... @@ -521,35 +553,6 @@ Proof. rewrite Val.add_assoc. auto. Qed. -(** Transformation of addressing modes with two operands or more - into an equivalent arithmetic operation. This is used in the [Reload] - pass when a store instruction cannot be reloaded directly because - it runs out of temporary registers. *) - -(** For the PowerPC, there is only one binary addressing mode: [Aindexed2]. - The corresponding operation is [Oadd]. *) - -Definition op_for_binary_addressing (addr: addressing) : operation := Oadd. - -Lemma eval_op_for_binary_addressing: - forall (F V: Type) (ge: Genv.t F V) sp addr args v m, - (length args >= 2)%nat -> - eval_addressing ge sp addr args = Some v -> - eval_operation ge sp (op_for_binary_addressing addr) args m = Some v. -Proof. - intros. - destruct addr; simpl in H0; FuncInv; simpl in H; try omegaContradiction. - simpl; congruence. -Qed. - -Lemma type_op_for_binary_addressing: - forall addr, - (length (type_of_addressing addr) >= 2)%nat -> - type_of_operation (op_for_binary_addressing addr) = (type_of_addressing addr, Tint). -Proof. - intros. destruct addr; simpl in H; reflexivity || omegaContradiction. -Qed. - (** Operations that are so cheap to recompute that CSE should not factor them out. *) Definition is_trivial_op (op: operation) : bool := @@ -578,61 +581,6 @@ Proof. destruct c; simpl; auto; discriminate. Qed. -(** Checking whether two addressings, applied to the same arguments, produce - separated memory addresses. Used in [CSE]. *) - -Definition addressing_separated (chunk1: memory_chunk) (addr1: addressing) - (chunk2: memory_chunk) (addr2: addressing) : bool := - match addr1, addr2 with - | Aindexed ofs1, Aindexed ofs2 => - Int.no_overlap ofs1 (size_chunk chunk1) ofs2 (size_chunk chunk2) - | Aglobal s1 ofs1, Aglobal s2 ofs2 => - if ident_eq s1 s2 then Int.no_overlap ofs1 (size_chunk chunk1) ofs2 (size_chunk chunk2) else true - | Abased s1 ofs1, Abased s2 ofs2 => - if ident_eq s1 s2 then Int.no_overlap ofs1 (size_chunk chunk1) ofs2 (size_chunk chunk2) else true - | Ainstack ofs1, Ainstack ofs2 => - Int.no_overlap ofs1 (size_chunk chunk1) ofs2 (size_chunk chunk2) - | _, _ => false - end. - -Lemma addressing_separated_sound: - forall (F V: Type) (ge: Genv.t F V) sp chunk1 addr1 chunk2 addr2 vl b1 n1 b2 n2, - addressing_separated chunk1 addr1 chunk2 addr2 = true -> - eval_addressing ge sp addr1 vl = Some(Vptr b1 n1) -> - eval_addressing ge sp addr2 vl = Some(Vptr b2 n2) -> - b1 <> b2 \/ Int.unsigned n1 + size_chunk chunk1 <= Int.unsigned n2 \/ Int.unsigned n2 + size_chunk chunk2 <= Int.unsigned n1. -Proof. - unfold addressing_separated; intros. - generalize (size_chunk_pos chunk1) (size_chunk_pos chunk2); intros SZ1 SZ2. - destruct addr1; destruct addr2; try discriminate; simpl in *; FuncInv. -(* Aindexed *) - destruct v; simpl in *; inv H1; inv H2. - right. apply Int.no_overlap_sound; auto. -(* Aglobal *) - unfold Genv.symbol_address in *. - destruct (Genv.find_symbol ge i1) eqn:?; inv H2. - destruct (Genv.find_symbol ge i) eqn:?; inv H1. - destruct (ident_eq i i1). subst. - replace (Int.unsigned n1) with (Int.unsigned (Int.add Int.zero n1)). - replace (Int.unsigned n2) with (Int.unsigned (Int.add Int.zero n2)). - right. apply Int.no_overlap_sound; auto. - rewrite Int.add_commut; rewrite Int.add_zero; auto. - rewrite Int.add_commut; rewrite Int.add_zero; auto. - left. red; intros; elim n. subst. eapply Genv.genv_vars_inj; eauto. -(* Abased *) - unfold Genv.symbol_address in *. - destruct (Genv.find_symbol ge i1) eqn:?; simpl in *; try discriminate. - destruct v; inv H2. - destruct (Genv.find_symbol ge i) eqn:?; inv H1. - destruct (ident_eq i i1). subst. - rewrite (Int.add_commut i0 i3). rewrite (Int.add_commut i2 i3). - right. apply Int.no_overlap_sound; auto. - left. red; intros; elim n. subst. eapply Genv.genv_vars_inj; eauto. -(* Ainstack *) - destruct sp; simpl in *; inv H1; inv H2. - right. apply Int.no_overlap_sound; auto. -Qed. - (** * Invariance and compatibility properties. *) (** [eval_operation] and [eval_addressing] depend on a global environment @@ -719,6 +667,8 @@ Ltac InvInject := inv H; InvInject | [ H: val_inject _ (Vfloat _) _ |- _ ] => inv H; InvInject + | [ H: val_inject _ (Vsingle _) _ |- _ ] => + inv H; InvInject | [ H: val_inject _ (Vptr _ _) _ |- _ ] => inv H; InvInject | [ H: val_list_inject _ nil _ |- _ ] => @@ -806,7 +756,14 @@ Proof. inv H4; inv H2; simpl; auto. inv H4; inv H2; simpl; auto. inv H4; simpl; auto. - inv H4; simpl in H1; inv H1. simpl. destruct (Float.intoffloat f0); simpl in H2; inv H2. + 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. + inv H4; simpl; auto. + inv H4; simpl; auto. + inv H4; simpl in H1; inv H1. simpl. destruct (Float.to_int f0); simpl in H2; inv H2. exists (Vint i); auto. inv H4; inv H2; simpl; auto. inv H4; inv H2; simpl; auto. diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml index b90b9f2..e3f0724 100644 --- a/powerpc/PrintAsm.ml +++ b/powerpc/PrintAsm.ml @@ -395,11 +395,11 @@ let print_builtin_vload_common oc chunk base offset res = fprintf oc " lhz %a, %a(%a)\n" ireg res constant offset ireg base | Mint16signed, IR res -> fprintf oc " lha %a, %a(%a)\n" ireg res constant offset ireg base - | Mint32, IR res -> + | (Mint32 | Many32), IR res -> fprintf oc " lwz %a, %a(%a)\n" ireg res constant offset ireg base | Mfloat32, FR res -> fprintf oc " lfs %a, %a(%a)\n" freg res constant offset ireg base - | Mfloat64, FR res -> + | (Mfloat64 | Many64), FR res -> fprintf oc " lfd %a, %a(%a)\n" freg res constant offset ireg base (* Mint64 is special-cased below *) | _ -> @@ -451,12 +451,11 @@ let print_builtin_vstore_common oc chunk base offset src = fprintf oc " stb %a, %a(%a)\n" ireg src constant offset ireg base | (Mint16signed | Mint16unsigned), IR src -> fprintf oc " sth %a, %a(%a)\n" ireg src constant offset ireg base - | Mint32, IR src -> + | (Mint32 | Many32), IR src -> fprintf oc " stw %a, %a(%a)\n" ireg src constant offset ireg base | Mfloat32, FR src -> - fprintf oc " frsp %a, %a\n" freg FPR13 freg src; - fprintf oc " stfs %a, %a(%a)\n" freg FPR13 constant offset ireg base - | Mfloat64, FR src -> + fprintf oc " stfs %a, %a(%a)\n" freg src constant offset ireg base + | (Mfloat64 | Many64), FR src -> fprintf oc " stfd %a, %a(%a)\n" freg src constant offset ireg base (* Mint64 is special-cased below *) | _ -> @@ -512,11 +511,11 @@ let align n a = (n + a - 1) land (-a) let rec next_arg_locations ir fr ofs = function | [] -> (ir, fr, ofs) - | Tint :: l -> + | (Tint | Tany32) :: l -> if ir < 8 then next_arg_locations (ir + 1) fr ofs l else next_arg_locations ir fr (ofs + 4) l - | (Tfloat | Tsingle) :: l -> + | (Tfloat | Tsingle | Tany64) :: l -> if fr < 8 then next_arg_locations ir (fr + 1) ofs l else next_arg_locations ir fr (align ofs 8 + 8) l @@ -676,6 +675,7 @@ let short_cond_branch tbl pc lbl_dest = (* Printing of instructions *) let float_literals : (int * int64) list ref = ref [] +let float32_literals : (int * int32) list ref = ref [] let jumptables : (int * label list) list ref = ref [] let print_instruction oc tbl pc fallthrough = function @@ -804,10 +804,12 @@ let print_instruction oc tbl pc fallthrough = function fprintf oc " addi %a, %a, %ld\n" ireg GPR1 ireg GPR1 sz else fprintf oc " lwz %a, %ld(%a)\n" ireg GPR1 ofs ireg GPR1 - | Pfabs(r1, r2) -> + | Pfabs(r1, r2) | Pfabss(r1, r2) -> fprintf oc " fabs %a, %a\n" freg r1 freg r2 | Pfadd(r1, r2, r3) -> fprintf oc " fadd %a, %a, %a\n" freg r1 freg r2 freg r3 + | Pfadds(r1, r2, r3) -> + fprintf oc " fadds %a, %a, %a\n" freg r1 freg r2 freg r3 | Pfcmpu(r1, r2) -> fprintf oc " fcmpu %a, %a, %a\n" creg 0 freg r1 freg r2 | Pfcti(r1, r2) -> @@ -821,6 +823,8 @@ let print_instruction oc tbl pc fallthrough = function fprintf oc "%s end pseudoinstr fcti\n" comment | Pfdiv(r1, r2, r3) -> fprintf oc " fdiv %a, %a, %a\n" freg r1 freg r2 freg r3 + | Pfdivs(r1, r2, r3) -> + fprintf oc " fdivs %a, %a, %a\n" freg r1 freg r2 freg r3 | Pfmake(rd, r1, r2) -> fprintf oc "%s begin pseudoinstr %a = fmake(%a, %a)\n" comment freg rd ireg r1 ireg r2; @@ -835,25 +839,37 @@ let print_instruction oc tbl pc fallthrough = function fprintf oc " fmr %a, %a\n" freg r1 freg r2 | Pfmul(r1, r2, r3) -> fprintf oc " fmul %a, %a, %a\n" freg r1 freg r2 freg r3 - | Pfneg(r1, r2) -> + | Pfmuls(r1, r2, r3) -> + fprintf oc " fmuls %a, %a, %a\n" freg r1 freg r2 freg r3 + | Pfneg(r1, r2) | Pfnegs(r1, r2) -> fprintf oc " fneg %a, %a\n" freg r1 freg r2 | Pfrsp(r1, r2) -> fprintf oc " frsp %a, %a\n" freg r1 freg r2 + | Pfxdp(r1, r2) -> + if r1 <> r2 then + fprintf oc " fmr %a, %a\n" freg r1 freg r2 | Pfsub(r1, r2, r3) -> fprintf oc " fsub %a, %a, %a\n" freg r1 freg r2 freg r3 + | Pfsubs(r1, r2, r3) -> + fprintf oc " fsubs %a, %a, %a\n" freg r1 freg r2 freg r3 | Plbz(r1, c, r2) -> 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 - | Plfd(r1, c, r2) -> + | 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(r1, r2, r3) | Plfdx_a(r1, r2, r3) -> fprintf oc " lfdx %a, %a, %a\n" freg r1 ireg r2 ireg r3 | Plfi(r1, c) -> let lbl = new_label() in fprintf oc " addis %a, 0, %a\n" ireg GPR12 label_high lbl; fprintf oc " lfd %a, %a(%a) %s %.18g\n" freg r1 label_low lbl ireg GPR12 comment (camlfloat_of_coqfloat c); - float_literals := (lbl, camlint64_of_coqint (Floats.Float.bits_of_double c)) :: !float_literals; + float_literals := (lbl, camlint64_of_coqint (Floats.Float.to_bits c)) :: !float_literals; + | Plfis(r1, c) -> + let lbl = new_label() in + fprintf oc " addis %a, 0, %a\n" ireg GPR12 label_high lbl; + fprintf oc " lfs %a, %a(%a) %s %.18g\n" freg r1 label_low lbl ireg GPR12 comment (camlfloat_of_coqfloat32 c); + float32_literals := (lbl, camlint_of_coqint (Floats.Float32.to_bits c)) :: !float32_literals; | Plfs(r1, c, r2) -> fprintf oc " lfs %a, %a(%a)\n" freg r1 constant c ireg r2 | Plfsx(r1, r2, r3) -> @@ -866,9 +882,9 @@ let print_instruction oc tbl pc fallthrough = function 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 - | Plwz(r1, c, r2) -> + | Plwz(r1, c, r2) | Plwz_a(r1, c, r2) -> fprintf oc " lwz %a, %a(%a)\n" ireg r1 constant c ireg r2 - | Plwzx(r1, r2, r3) -> + | Plwzx(r1, r2, r3) | Plwzx_a(r1, r2, r3) -> fprintf oc " lwzx %a, %a, %a\n" ireg r1 ireg r2 ireg r3 | Pmfcrbit(r1, bit) -> fprintf oc " mfcr %a\n" ireg r1; @@ -924,23 +940,21 @@ let print_instruction oc tbl pc fallthrough = function 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 - | Pstfd(r1, c, r2) -> + | Pstfd(r1, c, r2) | Pstfd_a(r1, c, r2) -> fprintf oc " stfd %a, %a(%a)\n" freg r1 constant c ireg r2 - | Pstfdx(r1, r2, r3) -> + | Pstfdx(r1, r2, r3) | Pstfdx_a(r1, r2, r3) -> fprintf oc " stfdx %a, %a, %a\n" freg r1 ireg r2 ireg r3 | Pstfs(r1, c, r2) -> - fprintf oc " frsp %a, %a\n" freg FPR13 freg r1; - fprintf oc " stfs %a, %a(%a)\n" freg FPR13 constant c ireg r2 + fprintf oc " stfs %a, %a(%a)\n" freg r1 constant c ireg r2 | Pstfsx(r1, r2, r3) -> - fprintf oc " frsp %a, %a\n" freg FPR13 freg r1; - fprintf oc " stfsx %a, %a, %a\n" freg FPR13 ireg r2 ireg r3 + fprintf oc " stfsx %a, %a, %a\n" freg r1 ireg r2 ireg r3 | Psth(r1, c, r2) -> fprintf oc " sth %a, %a(%a)\n" ireg r1 constant c ireg r2 | Psthx(r1, r2, r3) -> fprintf oc " sthx %a, %a, %a\n" ireg r1 ireg r2 ireg r3 - | Pstw(r1, c, r2) -> + | Pstw(r1, c, r2) | Pstw_a(r1, c, r2) -> fprintf oc " stw %a, %a(%a)\n" ireg r1 constant c ireg r2 - | Pstwx(r1, r2, r3) -> + | Pstwx(r1, r2, r3) | Pstwx_a(r1, r2, r3) -> fprintf oc " stwx %a, %a, %a\n" ireg r1 ireg r2 ireg r3 | Psubfc(r1, r2, r3) -> fprintf oc " subfc %a, %a, %a\n" ireg r1 ireg r2 ireg r3 @@ -1061,11 +1075,14 @@ let rec print_instructions oc tbl pc fallthrough = function (* Print the code for a function *) -let print_literal oc (lbl, n) = +let print_literal64 oc (lbl, n) = let nlo = Int64.to_int32 n and nhi = Int64.to_int32(Int64.shift_right_logical n 32) in fprintf oc "%a: .long 0x%lx, 0x%lx\n" label lbl nhi nlo +let print_literal32 oc (lbl, n) = + fprintf oc "%a: .long 0x%lx\n" label lbl n + let print_jumptable oc (lbl, tbl) = fprintf oc "%a:" label lbl; List.iter @@ -1075,6 +1092,7 @@ let print_jumptable oc (lbl, tbl) = let print_function oc name fn = Hashtbl.clear current_function_labels; float_literals := []; + float32_literals := []; jumptables := []; current_function_sig := fn.fn_sig; let (text, lit, jmptbl) = @@ -1095,11 +1113,12 @@ let print_function oc name fn = cfi_endproc oc; fprintf oc " .type %a, @function\n" symbol name; fprintf oc " .size %a, . - %a\n" symbol name symbol name; - if !float_literals <> [] then begin + if !float_literals <> [] || !float32_literals <> [] then begin section oc lit; fprintf oc " .balign 8\n"; - List.iter (print_literal oc) !float_literals; - float_literals := [] + List.iter (print_literal64 oc) !float_literals; + List.iter (print_literal32 oc) !float32_literals; + float_literals := []; float32_literals := [] end; if !jumptables <> [] then begin section oc jmptbl; @@ -1131,10 +1150,10 @@ let print_init oc = function (Int64.logand b 0xFFFFFFFFL) | Init_float32 n -> fprintf oc " .long 0x%lx %s %.18g\n" - (camlint_of_coqint (Floats.Float.bits_of_single n)) + (camlint_of_coqint (Floats.Float32.to_bits n)) comment (camlfloat_of_coqfloat n) | Init_float64 n -> - let b = camlint64_of_coqint (Floats.Float.bits_of_double n) in + let b = camlint64_of_coqint (Floats.Float.to_bits n) in fprintf oc " .long 0x%Lx, 0x%Lx %s %.18g\n" (Int64.shift_right_logical b 32) (Int64.logand b 0xFFFFFFFFL) diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp index 371a08a..70b1feb 100644 --- a/powerpc/SelectOp.vp +++ b/powerpc/SelectOp.vp @@ -374,6 +374,12 @@ Definition addf (e1 e2: expr) := Eop Oaddf (e1 ::: e2 ::: Enil). Definition subf (e1 e2: expr) := Eop Osubf (e1 ::: e2 ::: Enil). Definition mulf (e1 e2: expr) := Eop Omulf (e1 ::: e2 ::: Enil). +Definition negfs (e: expr) := Eop Onegfs (e ::: Enil). +Definition absfs (e: expr) := Eop Oabsfs (e ::: Enil). +Definition addfs (e1 e2: expr) := Eop Oaddfs (e1 ::: e2 ::: Enil). +Definition subfs (e1 e2: expr) := Eop Osubfs (e1 ::: e2 ::: Enil). +Definition mulfs (e1 e2: expr) := Eop Omulfs (e1 ::: e2 ::: Enil). + (** ** Comparisons *) Nondetfunction compimm (default: comparison -> int -> condition) @@ -433,6 +439,10 @@ Nondetfunction compu (c: comparison) (e1: expr) (e2: expr) := Definition compf (c: comparison) (e1: expr) (e2: expr) := Eop (Ocmp (Ccompf c)) (e1 ::: e2 ::: Enil). +Definition compfs (c: comparison) (e1: expr) (e2: expr) := + Eop (Ocmp (Ccompf c)) (Eop Ofloatofsingle (e1 ::: Enil) ::: + Eop Ofloatofsingle (e2 ::: Enil) ::: Enil). + (** ** Integer conversions *) Definition cast8unsigned (e: expr) := andimm (Int.repr 255) e. @@ -457,7 +467,7 @@ Definition intoffloat (e: expr) := Eop Ointoffloat (e ::: Enil). Definition intuoffloat (e: expr) := Elet e - (Elet (Eop (Ofloatconst (Float.floatofintu Float.ox8000_0000)) Enil) + (Elet (Eop (Ofloatconst (Float.of_intu Float.ox8000_0000)) Enil) (Econdition (CEcond (Ccompf Clt) (Eletvar 1 ::: Eletvar 0 ::: Enil)) (intoffloat (Eletvar 1)) (addimm Float.ox8000_0000 (intoffloat (subf (Eletvar 1) (Eletvar 0))))))%nat. @@ -465,7 +475,7 @@ Definition intuoffloat (e: expr) := Nondetfunction floatofintu (e: expr) := match e with | Eop (Ointconst n) Enil => - Eop (Ofloatconst (Float.floatofintu n)) Enil + Eop (Ofloatconst (Float.of_intu n)) Enil | _ => subf (Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil ::: e ::: Enil)) (Eop (Ofloatconst (Float.from_words Float.ox4330_0000 Int.zero)) Enil) @@ -474,14 +484,27 @@ Nondetfunction floatofintu (e: expr) := Nondetfunction floatofint (e: expr) := match e with | Eop (Ointconst n) Enil => - Eop (Ofloatconst (Float.floatofint n)) Enil + Eop (Ofloatconst (Float.of_int n)) Enil | _ => 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) end. +Definition intofsingle (e: expr) := + intoffloat (Eop Ofloatofsingle (e ::: Enil)). + +Definition singleofint (e: expr) := + Eop Osingleoffloat (floatofint e ::: Enil). + +Definition intuofsingle (e: expr) := + intuoffloat (Eop Ofloatofsingle (e ::: Enil)). + +Definition singleofintu (e: expr) := + Eop Osingleoffloat (floatofintu e ::: Enil). + Definition singleoffloat (e: expr) := Eop Osingleoffloat (e ::: Enil). +Definition floatofsingle (e: expr) := Eop Ofloatofsingle (e ::: Enil). (** ** Recognition of addressing modes for load and store operations *) diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v index cb48d51..8311b82 100644 --- a/powerpc/SelectOpproof.v +++ b/powerpc/SelectOpproof.v @@ -639,6 +639,31 @@ Proof. red; intros; TrivialExists. Qed. +Theorem eval_negfs: unary_constructor_sound negfs Val.negfs. +Proof. + red; intros. TrivialExists. +Qed. + +Theorem eval_absfs: unary_constructor_sound absfs Val.absfs. +Proof. + red; intros. TrivialExists. +Qed. + +Theorem eval_addfs: binary_constructor_sound addfs Val.addfs. +Proof. + red; intros; TrivialExists. +Qed. + +Theorem eval_subfs: binary_constructor_sound subfs Val.subfs. +Proof. + red; intros; TrivialExists. +Qed. + +Theorem eval_mulfs: binary_constructor_sound mulfs Val.mulfs. +Proof. + red; intros; TrivialExists. +Qed. + Section COMP_IMM. Variable default: comparison -> int -> condition. @@ -746,6 +771,18 @@ Proof. intros; red; intros. unfold compf. TrivialExists. Qed. +Theorem eval_compfs: + forall c, binary_constructor_sound (compfs c) (Val.cmpfs c). +Proof. + intros; red; intros. unfold compfs. + replace (Val.cmpfs c x y) with + (Val.cmpf c (Val.floatofsingle x) (Val.floatofsingle y)). + TrivialExists. constructor. EvalOp. simpl; reflexivity. + constructor. EvalOp. simpl; reflexivity. constructor. + auto. + destruct x; auto. destruct y; auto. unfold Val.cmpf, Val.cmpfs; simpl. + rewrite Float32.cmp_double. auto. +Qed. Theorem eval_cast8signed: unary_constructor_sound cast8signed (Val.sign_ext 8). Proof. @@ -778,6 +815,11 @@ Proof. red; intros. unfold singleoffloat. TrivialExists. Qed. +Theorem eval_floatofsingle: unary_constructor_sound floatofsingle Val.floatofsingle. +Proof. + red; intros. unfold floatofsingle. TrivialExists. +Qed. + Theorem eval_intoffloat: forall le a x y, eval_expr ge sp e m le a x -> @@ -794,10 +836,10 @@ Theorem eval_intuoffloat: exists v, eval_expr ge sp e m le (intuoffloat a) v /\ Val.lessdef y v. Proof. intros. destruct x; simpl in H0; try discriminate. - destruct (Float.intuoffloat f) as [n|] eqn:?; simpl in H0; inv H0. + destruct (Float.to_intu f) as [n|] eqn:?; simpl in H0; inv H0. exists (Vint n); split; auto. unfold intuoffloat. set (im := Int.repr Int.half_modulus). - set (fm := Float.floatofintu im). + set (fm := Float.of_intu im). assert (eval_expr ge sp e m (Vfloat fm :: Vfloat f :: le) (Eletvar (S O)) (Vfloat f)). constructor. auto. assert (eval_expr ge sp e m (Vfloat fm :: Vfloat f :: le) (Eletvar O) (Vfloat fm)). @@ -807,9 +849,9 @@ Proof. eapply eval_Econdition with (va := Float.cmp Clt f fm). eauto with evalexpr. destruct (Float.cmp Clt f fm) eqn:?. - exploit Float.intuoffloat_intoffloat_1; eauto. intro EQ. + exploit Float.to_intu_to_int_1; eauto. intro EQ. EvalOp. simpl. rewrite EQ; auto. - exploit Float.intuoffloat_intoffloat_2; eauto. + exploit Float.to_intu_to_int_2; eauto. change Float.ox8000_0000 with im. fold fm. intro EQ. set (t2 := subf (Eletvar (S O)) (Eletvar O)). set (t3 := intoffloat t2). @@ -834,7 +876,7 @@ Proof. intros until y. unfold floatofint. destruct (floatofint_match a); intros. InvEval. TrivialExists. rename e0 into a. destruct x; simpl in H0; inv H0. - exists (Vfloat (Float.floatofint i)); split; auto. + exists (Vfloat (Float.of_int i)); split; auto. set (t1 := addimm Float.ox8000_0000 a). set (t2 := Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil ::: t1 ::: Enil)). set (t3 := Eop (Ofloatconst (Float.from_words Float.ox4330_0000 Float.ox8000_0000)) Enil). @@ -844,7 +886,7 @@ Proof. unfold t2. EvalOp. constructor. EvalOp. simpl; eauto. constructor. eauto. constructor. unfold eval_operation. eauto. instantiate (2 := t3). unfold t3. EvalOp. simpl; eauto. - intros [v2 [A2 B2]]. simpl in B2. inv B2. rewrite Float.floatofint_from_words. auto. + intros [v2 [A2 B2]]. simpl in B2. inv B2. rewrite Float.of_int_from_words. auto. Qed. Theorem eval_floatofintu: @@ -856,7 +898,7 @@ Proof. intros until y. unfold floatofintu. destruct (floatofintu_match a); intros. InvEval. TrivialExists. rename e0 into a. destruct x; simpl in H0; inv H0. - exists (Vfloat (Float.floatofintu i)); split; auto. + exists (Vfloat (Float.of_intu i)); split; auto. unfold floatofintu. set (t2 := Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil ::: a ::: Enil)). set (t3 := Eop (Ofloatconst (Float.from_words Float.ox4330_0000 Int.zero)) Enil). @@ -864,7 +906,73 @@ Proof. unfold t2. EvalOp. constructor. EvalOp. simpl; eauto. constructor. eauto. constructor. unfold eval_operation. eauto. instantiate (2 := t3). unfold t3. EvalOp. simpl; eauto. - intros [v2 [A2 B2]]. simpl in B2. inv B2. rewrite Float.floatofintu_from_words. auto. + intros [v2 [A2 B2]]. simpl in B2. inv B2. rewrite Float.of_intu_from_words. auto. +Qed. + +Theorem eval_intofsingle: + forall le a x y, + eval_expr ge sp e m le a x -> + Val.intofsingle x = Some y -> + exists v, eval_expr ge sp e m le (intofsingle a) v /\ Val.lessdef y v. +Proof. + intros; unfold intofsingle. + assert (Val.intoffloat (Val.floatofsingle x) = Some y). + { destruct x; simpl in H0; try discriminate. + destruct (Float32.to_int f) eqn:F; inv H0. + apply Float32.to_int_double in F. + simpl. unfold Float32.to_double in F; rewrite F; auto. + } + apply eval_intoffloat with (Val.floatofsingle x); auto. EvalOp. +Qed. + +Theorem eval_singleofint: + forall le a x y, + eval_expr ge sp e m le a x -> + Val.singleofint x = Some y -> + exists v, eval_expr ge sp e m le (singleofint a) v /\ Val.lessdef y v. +Proof. + intros. unfold singleofint. + assert (exists z, Val.floatofint x = Some z /\ y = Val.singleoffloat z). + { + destruct x; inv H0. simpl. exists (Vfloat (Float.of_int i)); simpl; split; auto. + f_equal. apply Float32.of_int_double. + } + destruct H1 as (z & A & B). subst y. + exploit eval_floatofint; eauto. intros (v & C & D). + exists (Val.singleoffloat v); split. EvalOp. inv D; auto. +Qed. + +Theorem eval_intuofsingle: + forall le a x y, + eval_expr ge sp e m le a x -> + Val.intuofsingle x = Some y -> + exists v, eval_expr ge sp e m le (intuofsingle a) v /\ Val.lessdef y v. +Proof. + intros; unfold intuofsingle. + assert (Val.intuoffloat (Val.floatofsingle x) = Some y). + { destruct x; simpl in H0; try discriminate. + destruct (Float32.to_intu f) eqn:F; inv H0. + apply Float32.to_intu_double in F. + simpl. unfold Float32.to_double in F; rewrite F; auto. + } + apply eval_intuoffloat with (Val.floatofsingle x); auto. EvalOp. +Qed. + +Theorem eval_singleofintu: + forall le a x y, + eval_expr ge sp e m le a x -> + Val.singleofintu x = Some y -> + exists v, eval_expr ge sp e m le (singleofintu a) v /\ Val.lessdef y v. +Proof. + intros. unfold singleofintu. + assert (exists z, Val.floatofintu x = Some z /\ y = Val.singleoffloat z). + { + destruct x; inv H0. simpl. exists (Vfloat (Float.of_intu i)); simpl; split; auto. + f_equal. apply Float32.of_intu_double. + } + destruct H1 as (z & A & B). subst y. + exploit eval_floatofintu; eauto. intros (v & C & D). + exists (Val.singleoffloat v); split. EvalOp. inv D; auto. Qed. Theorem eval_addressing: diff --git a/powerpc/Unusedglob1.ml b/powerpc/Unusedglob1.ml index 49c0774..2d3efe3 100644 --- a/powerpc/Unusedglob1.ml +++ b/powerpc/Unusedglob1.ml @@ -42,18 +42,22 @@ let referenced_instr = function | Pcmpwi(_, c) | Plbz(_, c, _) | Plfd(_, c, _) + | Plfd_a(_, c, _) | Plfs(_, c, _) | Plha(_, c, _) | Plhz(_, c, _) | Plwz(_, c, _) + | Plwz_a(_, c, _) | Pmulli(_, _, c) | Pori(_, _, c) | Poris(_, _, c) | Pstb(_, c, _) | Pstfd(_, c, _) + | Pstfd_a(_, c, _) | Pstfs(_, c, _) | Psth(_, c, _) | Pstw(_, c, _) + | Pstw_a(_, c, _) | Psubfic(_, _, c) | Pxori(_, _, c) | Pxoris(_, _, c) -> referenced_constant c diff --git a/powerpc/ValueAOp.v b/powerpc/ValueAOp.v index 77463f4..a5a1db8 100644 --- a/powerpc/ValueAOp.v +++ b/powerpc/ValueAOp.v @@ -52,6 +52,7 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Omove, v1::nil => v1 | Ointconst n, nil => I n | Ofloatconst n, nil => if propagate_float_constants tt then F n else ftop + | Osingleconst n, nil => if propagate_float_constants tt then FS n else ftop | Oaddrsymbol id ofs, nil => Ptr (Gl id ofs) | Oaddrstack ofs, nil => Ptr (Stk ofs) | Ocast8signed, v1 :: nil => sign_ext 8 v1 @@ -92,7 +93,14 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Osubf, v1::v2::nil => subf v1 v2 | Omulf, v1::v2::nil => mulf v1 v2 | Odivf, v1::v2::nil => divf v1 v2 + | Onegfs, v1::nil => negfs v1 + | Oabsfs, v1::nil => absfs v1 + | Oaddfs, v1::v2::nil => addfs v1 v2 + | Osubfs, v1::v2::nil => subfs v1 v2 + | Omulfs, v1::v2::nil => mulfs v1 v2 + | Odivfs, v1::v2::nil => divfs v1 v2 | Osingleoffloat, v1::nil => singleoffloat v1 + | Ofloatofsingle, v1::nil => floatofsingle v1 | Ointoffloat, v1::nil => intoffloat v1 | Ofloatofwords, v1::v2::nil => floatofwords v1 v2 | Omakelong, v1::v2::nil => longofwords v1 v2 @@ -163,6 +171,7 @@ Proof. unfold eval_operation, eval_static_operation; intros; destruct op; InvHyps; eauto with va. destruct (propagate_float_constants tt); constructor. + destruct (propagate_float_constants tt); constructor. rewrite Int.add_zero_l; eauto with va. fold (Val.sub (Vint i) a1). auto with va. apply floatofwords_sound; auto. diff --git a/powerpc/eabi/Conventions1.v b/powerpc/eabi/Conventions1.v index 2db1f73..866e73d 100644 --- a/powerpc/eabi/Conventions1.v +++ b/powerpc/eabi/Conventions1.v @@ -15,6 +15,7 @@ Require Import Coqlib. Require Import AST. +Require Import Events. Require Import Locations. (** * Classification of machine registers *) @@ -180,13 +181,13 @@ Proof. Qed. Lemma int_callee_save_type: - forall r, In r int_callee_save_regs -> mreg_type r = Tint. + forall r, In r int_callee_save_regs -> mreg_type r = Tany32. Proof. intro. simpl; ElimOrEq; reflexivity. Qed. Lemma float_callee_save_type: - forall r, In r float_callee_save_regs -> mreg_type r = Tfloat. + forall r, In r float_callee_save_regs -> mreg_type r = Tany64. Proof. intro. simpl; ElimOrEq; reflexivity. Qed. @@ -239,12 +240,21 @@ Qed. Definition loc_result (s: signature) : list mreg := match s.(sig_res) with | None => R3 :: nil - | Some Tint => R3 :: nil - | Some (Tfloat | Tsingle) => F1 :: nil + | Some (Tint | Tany32) => R3 :: nil + | Some (Tfloat | Tsingle | Tany64) => F1 :: nil | Some Tlong => R3 :: R4 :: nil end. -(** The result location is a caller-save register *) +(** The result registers have types compatible with that given in the signature. *) + +Lemma loc_result_type: + forall sig, + subtype_list (proj_sig_res' sig) (map mreg_type (loc_result sig)) = true. +Proof. + intros. unfold proj_sig_res', loc_result. destruct (sig_res sig) as [[]|]; auto. +Qed. + +(** The result locations are caller-save registers *) Lemma loc_result_caller_save: forall (s: signature) (r: mreg), @@ -278,18 +288,18 @@ Fixpoint loc_arguments_rec (tyl: list typ) (ir fr ofs: Z) {struct tyl} : list loc := match tyl with | nil => nil - | Tint :: tys => + | (Tint | Tany32) as ty :: tys => match list_nth_z int_param_regs ir with | None => - S Outgoing ofs Tint :: loc_arguments_rec tys ir fr (ofs + 1) + S Outgoing ofs ty :: loc_arguments_rec tys ir fr (ofs + 1) | Some ireg => R ireg :: loc_arguments_rec tys (ir + 1) fr ofs end - | (Tfloat | Tsingle) :: tys => + | (Tfloat | Tsingle | Tany64) as ty :: tys => match list_nth_z float_param_regs fr with | None => let ofs := align ofs 2 in - S Outgoing ofs Tfloat :: loc_arguments_rec tys ir fr (ofs + 2) + S Outgoing ofs ty :: loc_arguments_rec tys ir fr (ofs + 2) | Some freg => R freg :: loc_arguments_rec tys ir (fr + 1) ofs end @@ -316,12 +326,12 @@ Definition loc_arguments (s: signature) : list loc := Fixpoint size_arguments_rec (tyl: list typ) (ir fr ofs: Z) {struct tyl} : Z := match tyl with | nil => ofs - | Tint :: tys => + | (Tint | Tany32) :: tys => match list_nth_z int_param_regs ir with | None => size_arguments_rec tys ir fr (ofs + 1) | Some ireg => size_arguments_rec tys (ir + 1) fr ofs end - | (Tfloat | Tsingle) :: tys => + | (Tfloat | Tsingle | Tany64) :: tys => match list_nth_z float_param_regs fr with | None => size_arguments_rec tys ir fr (align ofs 2 + 2) | Some freg => size_arguments_rec tys ir (fr + 1) ofs @@ -393,7 +403,7 @@ Opaque list_nth_z. destruct H. subst. split. omega. congruence. exploit IHtyl; eauto. destruct l; auto. destruct sl; auto. intuition omega. assert (ofs <= align ofs 2) by (apply align_le; omega). - destruct H. subst. split. omega. congruence. + destruct H. subst. split. omega. congruence. destruct H. subst. split. omega. congruence. exploit IHtyl; eauto. destruct l; auto. destruct sl; auto. intuition omega. - (* single *) @@ -404,6 +414,20 @@ Opaque list_nth_z. exploit IHtyl; eauto. destruct l; auto. destruct sl; auto. assert (ofs <= align ofs 2) by (apply align_le; omega). intuition omega. +- (* any32 *) + destruct (list_nth_z int_param_regs ir) as [r|] eqn:E; destruct H. + subst. left. eapply list_nth_z_in; eauto. + eapply IHtyl; eauto. + subst. split. omega. congruence. + exploit IHtyl; eauto. destruct l; auto. destruct sl; auto. intuition omega. +- (* any64 *) + destruct (list_nth_z float_param_regs fr) as [r|] eqn:E; destruct H. + subst. right. eapply list_nth_z_in; eauto. + eapply IHtyl; eauto. + subst. split. apply Zle_ge. apply align_le. omega. congruence. + exploit IHtyl; eauto. destruct l; auto. destruct sl; auto. + assert (ofs <= align ofs 2) by (apply align_le; omega). + intuition omega. Qed. Lemma loc_arguments_acceptable: @@ -441,6 +465,10 @@ Proof. destruct (list_nth_z float_param_regs fr); eauto. apply Zle_trans with (align ofs0 2). apply align_le; omega. apply Zle_trans with (align ofs0 2 + 2); auto; omega. + destruct (list_nth_z int_param_regs ir); eauto. apply Zle_trans with (ofs0 + 1); auto; omega. + destruct (list_nth_z float_param_regs fr); eauto. + apply Zle_trans with (align ofs0 2). apply align_le; omega. + apply Zle_trans with (align ofs0 2 + 2); auto; omega. Qed. Lemma size_arguments_above: @@ -493,6 +521,18 @@ Proof. destruct (list_nth_z float_param_regs fr); destruct H0. congruence. eauto. + inv H0. transitivity (align ofs0 2 + 2). simpl; omega. apply size_arguments_rec_above. + eauto. +- (* any32 *) + destruct (list_nth_z int_param_regs ir); destruct H0. + congruence. + eauto. + inv H0. apply size_arguments_rec_above. + eauto. +- (* any64 *) + destruct (list_nth_z float_param_regs fr); destruct H0. + congruence. + eauto. inv H0. apply size_arguments_rec_above. eauto. } eauto. |