diff options
Diffstat (limited to 'powerpc')
-rw-r--r-- | powerpc/Asm.v | 4 | ||||
-rw-r--r-- | powerpc/Asmgen.v | 7 | ||||
-rw-r--r-- | powerpc/Asmgenproof.v | 1 | ||||
-rw-r--r-- | powerpc/Asmgenproof1.v | 22 | ||||
-rw-r--r-- | powerpc/Op.v | 15 | ||||
-rw-r--r-- | powerpc/PrintAsm.ml | 5 | ||||
-rw-r--r-- | powerpc/SelectOp.v | 45 | ||||
-rw-r--r-- | powerpc/SelectOpproof.v | 12 |
8 files changed, 92 insertions, 19 deletions
diff --git a/powerpc/Asm.v b/powerpc/Asm.v index fc29db04..d876144b 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -195,6 +195,7 @@ Inductive instruction : Type := | Pori: ireg -> ireg -> constant -> instruction (**r or with immediate *) | Poris: ireg -> ireg -> constant -> instruction (**r or with immediate high *) | Prlwinm: ireg -> ireg -> int -> int -> instruction (**r rotate and mask *) + | Prlwimi: ireg -> ireg -> int -> int -> instruction (**r rotate and insert *) | Pslw: ireg -> ireg -> ireg -> instruction (**r shift left *) | Psraw: ireg -> ireg -> ireg -> instruction (**r shift right signed *) | Psrawi: ireg -> ireg -> int -> instruction (**r shift right signed immediate *) @@ -697,6 +698,9 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome OK (nextinstr (rs#rd <- (Val.or rs#r1 (const_high cst)))) m | Prlwinm rd r1 amount mask => OK (nextinstr (rs#rd <- (Val.rolm rs#r1 amount mask))) m + | Prlwimi rd r1 amount mask => + OK (nextinstr (rs#rd <- (Val.or (Val.and rs#rd (Vint (Int.not mask))) + (Val.rolm rs#r1 amount mask)))) m | Pslw rd r1 r2 => OK (nextinstr (rs#rd <- (Val.shl rs#r1 rs#r2))) m | Psraw rd r1 r2 => diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v index 4370753b..cecc13e9 100644 --- a/powerpc/Asmgen.v +++ b/powerpc/Asmgen.v @@ -320,6 +320,13 @@ Definition transl_op Psrw (ireg_of r) (ireg_of a1) (ireg_of a2) :: k | Orolm amount mask, a1 :: nil => Prlwinm (ireg_of r) (ireg_of a1) amount mask :: k + | Oroli amount mask, a1 :: a2 :: nil => + if mreg_eq a1 r then (**r should always be true *) + Prlwimi (ireg_of r) (ireg_of a2) amount mask :: k + else + Pmr GPR0 (ireg_of a1) :: + Prlwimi GPR0 (ireg_of a2) amount mask :: + Pmr (ireg_of r) GPR0 :: k | Onegf, a1 :: nil => Pfneg (freg_of r) (freg_of a1) :: k | Oabsf, a1 :: nil => diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v index 0efe646d..97b04bb5 100644 --- a/powerpc/Asmgenproof.v +++ b/powerpc/Asmgenproof.v @@ -450,6 +450,7 @@ Proof. case (symbol_is_small_data i i0); reflexivity. case (Int.eq (high_s i) Int.zero); autorewrite with labels; reflexivity. case (Int.eq (high_s i) Int.zero); autorewrite with labels; reflexivity. + destruct (mreg_eq m r); reflexivity. Qed. Hint Rewrite transl_op_label: labels. diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v index ee3aa38a..55a74be1 100644 --- a/powerpc/Asmgenproof1.v +++ b/powerpc/Asmgenproof1.v @@ -1340,7 +1340,27 @@ Proof. apply agree_nextinstr. unfold rs1. apply agree_nextinstr_commut. apply agree_set_commut. auto with ppcgen. apply agree_set_other. apply agree_set_mireg_twice; auto with ppcgen. - compute; auto. auto with ppcgen. + compute; auto. auto with ppcgen. + (* Oroli *) + destruct (mreg_eq m0 res). subst m0. + TranslOpSimpl. + econstructor; split. + eapply exec_straight_three. + simpl. reflexivity. + simpl. reflexivity. + simpl. reflexivity. + auto. auto. auto. + set (rs1 := nextinstr (rs # GPR0 <- (rs (ireg_of m0)))). + set (rs2 := nextinstr (rs1 # GPR0 <- + (Val.or (Val.and (rs1 GPR0) (Vint (Int.not i0))) + (Val.rolm (rs1 (ireg_of m1)) i i0)))). + apply agree_nextinstr. apply agree_set_mireg; auto. apply agree_set_mreg. + apply agree_undef_temps with rs. auto. + intros. unfold rs2. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto. + unfold rs1. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto. + unfold rs2. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. + unfold rs1. repeat rewrite nextinstr_inv; auto with ppcgen. + rewrite Pregmap.gss. rewrite Pregmap.gso; auto with ppcgen. decEq. auto with ppcgen. (* Ointoffloat *) econstructor; split. apply exec_straight_one. simpl; eauto. auto. diff --git a/powerpc/Op.v b/powerpc/Op.v index d4669613..7bd42478 100644 --- a/powerpc/Op.v +++ b/powerpc/Op.v @@ -85,6 +85,7 @@ Inductive operation : Type := | Oshrximm: int -> operation (**r [rd = r1 / 2^n] (signed) *) | 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 Floating-point arithmetic: *) | Onegf: operation (**r [rd = - r1] *) | Oabsf: operation (**r [rd = abs(r1)] *) @@ -238,6 +239,8 @@ Definition eval_operation if Int.ltu n2 Int.iwordsize then Some (Vint (Int.shru n1 n2)) else None | Orolm amount mask, Vint n1 :: nil => Some (Vint (Int.rolm n1 amount mask)) + | Oroli amount mask, Vint n1 :: Vint n2 :: nil => + Some (Vint (Int.or (Int.and n1 (Int.not mask)) (Int.rolm n2 amount mask))) | Onegf, Vfloat f1 :: nil => Some (Vfloat (Float.neg f1)) | Oabsf, Vfloat f1 :: nil => Some (Vfloat (Float.abs f1)) | Oaddf, Vfloat f1 :: Vfloat f2 :: nil => Some (Vfloat (Float.add f1 f2)) @@ -456,6 +459,7 @@ Definition type_of_operation (op: operation) : list typ * typ := | Oshrximm _ => (Tint :: nil, Tint) | Oshru => (Tint :: Tint :: nil, Tint) | Orolm _ _ => (Tint :: nil, Tint) + | Oroli _ _ => (Tint :: Tint :: nil, Tint) | Onegf => (Tfloat :: nil, Tfloat) | Oabsf => (Tfloat :: nil, Tfloat) | Oaddf => (Tfloat :: Tfloat :: nil, Tfloat) @@ -604,6 +608,8 @@ Definition eval_operation_total (sp: val) (op: operation) (vl: list val) : val : | Oshrximm n, v1::nil => Val.shrx v1 (Vint n) | Oshru, v1::v2::nil => Val.shru v1 v2 | Orolm amount mask, v1::nil => Val.rolm v1 amount mask + | Oroli amount mask, v1::v2::nil => + Val.or (Val.and v1 (Vint (Int.not mask))) (Val.rolm v2 amount mask) | Onegf, v1::nil => Val.negf v1 | Oabsf, v1::nil => Val.absf v1 | Oaddf, v1::v2::nil => Val.addf v1 v2 @@ -1004,9 +1010,13 @@ Proof. intros. destruct addr; simpl in H; reflexivity || omegaContradiction. Qed. -(** Two-address operations. There are none in the PowerPC architecture. *) +(** Two-address operations. There is only one: rotate-mask-insert. *) -Definition two_address_op (op: operation) : bool := false. +Definition two_address_op (op: operation) : bool := + match op with + | Oroli _ _ => true + | _ => false + end. (** Operations that are so cheap to recompute that CSE should not factor them out. *) @@ -1019,7 +1029,6 @@ Definition is_trivial_op (op: operation) : bool := | _ => false end. - (** Operations that depend on the memory state. *) Definition op_depends_on_memory (op: operation) : bool := diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml index 0c199322..eacf1dd0 100644 --- a/powerpc/PrintAsm.ml +++ b/powerpc/PrintAsm.ml @@ -687,6 +687,11 @@ let print_instruction oc = function fprintf oc " rlwinm %a, %a, %ld, %d, %d %s 0x%lx\n" ireg r1 ireg r2 (camlint_of_coqint c1) mb me comment (camlint_of_coqint c2) + | Prlwimi(r1, r2, c1, c2) -> + let (mb, me) = rolm_mask (camlint_of_coqint c2) in + 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) | Pslw(r1, r2, r3) -> fprintf oc " slw %a, %a, %a\n" ireg r1 ireg r2 ireg r3 | Psraw(r1, r2, r3) -> diff --git a/powerpc/SelectOp.v b/powerpc/SelectOp.v index b735fad0..b1889935 100644 --- a/powerpc/SelectOp.v +++ b/powerpc/SelectOp.v @@ -69,10 +69,11 @@ Definition addrstack (ofs: int) := << Definition notint (e: expr) := match e with + | Eop (Ointconst n) Enil => Eop (Ointconst (Int.not n)) Enil | Eop Oand (t1:::t2:::Enil) => Eop Onand (t1:::t2:::Enil) | Eop Oor (t1:::t2:::Enil) => Eop Onor (t1:::t2:::Enil) | Eop Oxor (t1:::t2:::Enil) => Eop Onxor (t1:::t2:::Enil) - | _ => Elet(e, Eop Onor (Eletvar O ::: Eletvar O ::: Enil) + | _ => Elet e (Eop Onor (Eletvar O ::: Eletvar O ::: Enil)) end. >> However, Coq expands complex pattern-matchings like the above into @@ -88,13 +89,16 @@ Definition notint (e: expr) := Inductive notint_cases: forall (e: expr), Type := | notint_case1: - forall (t1: expr) (t2: expr), - notint_cases (Eop Oand (t1:::t2:::Enil)) + forall n, + notint_cases (Eop (Ointconst n) Enil) | notint_case2: - forall (t1: expr) (t2: expr), - notint_cases (Eop Oor (t1:::t2:::Enil)) + forall t1 t2, + notint_cases (Eop Oand (t1:::t2:::Enil)) | notint_case3: - forall (t1: expr) (t2: expr), + forall t1 t2, + notint_cases (Eop Oor (t1:::t2:::Enil)) + | notint_case4: + forall t1 t2, notint_cases (Eop Oxor (t1:::t2:::Enil)) | notint_default: forall (e: expr), @@ -109,12 +113,14 @@ Inductive notint_cases: forall (e: expr), Type := Definition notint_match (e: expr) := match e as z1 return notint_cases z1 with + | Eop (Ointconst n) Enil => + notint_case1 n | Eop Oand (t1:::t2:::Enil) => - notint_case1 t1 t2 - | Eop Oor (t1:::t2:::Enil) => notint_case2 t1 t2 - | Eop Oxor (t1:::t2:::Enil) => + | Eop Oor (t1:::t2:::Enil) => notint_case3 t1 t2 + | Eop Oxor (t1:::t2:::Enil) => + notint_case4 t1 t2 | e => notint_default e end. @@ -130,11 +136,13 @@ Definition notint_match (e: expr) := Definition notint (e: expr) := match notint_match e with - | notint_case1 t1 t2 => - Eop Onand (t1:::t2:::Enil) + | notint_case1 n => + Eop (Ointconst (Int.not n)) Enil | notint_case2 t1 t2 => - Eop Onor (t1:::t2:::Enil) + Eop Onand (t1:::t2:::Enil) | notint_case3 t1 t2 => + Eop Onor (t1:::t2:::Enil) + | notint_case4 t1 t2 => Eop Onxor (t1:::t2:::Enil) | notint_default e => Elet e (Eop Onor (Eletvar O ::: Eletvar O ::: Enil)) @@ -674,9 +682,16 @@ Definition or (e1: expr) (e2: expr) := | or_case1 amount1 mask1 t1 amount2 mask2 t2 => if Int.eq amount1 amount2 && is_rlw_mask (Int.or mask1 mask2) - && same_expr_pure t1 t2 - then Eop (Orolm amount1 (Int.or mask1 mask2)) (t1:::Enil) - else Eop Oor (e1:::e2:::Enil) + && same_expr_pure t1 t2 then + Eop (Orolm amount1 (Int.or mask1 mask2)) (t1:::Enil) + else if Int.eq amount1 Int.zero + && Int.eq mask1 (Int.not mask2) then + Eop (Oroli amount2 mask2) (t1:::t2:::Enil) + else if Int.eq amount2 Int.zero + && Int.eq mask2 (Int.not mask1) then + Eop (Oroli amount1 mask1) (t2:::t1:::Enil) + else + Eop Oor (e1:::e2:::Enil) | or_default e1 e2 => Eop Oor (e1:::e2:::Enil) end. diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v index 6d1e3c5c..b23e5a50 100644 --- a/powerpc/SelectOpproof.v +++ b/powerpc/SelectOpproof.v @@ -124,6 +124,7 @@ Theorem eval_notint: eval_expr ge sp e m le (notint a) (Vint (Int.not x)). Proof. unfold notint; intros until x; case (notint_match a); intros; InvEval. + EvalOp. EvalOp. simpl. congruence. EvalOp. simpl. congruence. EvalOp. simpl. congruence. @@ -524,11 +525,22 @@ Proof. generalize (Int.eq_spec amount1 amount2). rewrite H6. intro. subst amount2. exploit eval_same_expr; eauto. intros [EQ1 EQ2]. inv EQ1. inv EQ2. simpl. EvalOp. simpl. rewrite Int.or_rolm. auto. + caseEq (Int.eq amount1 Int.zero && Int.eq mask1 (Int.not mask2)); intro. + destruct (andb_prop _ _ H4). + generalize (Int.eq_spec amount1 Int.zero). rewrite H5. intro. + generalize (Int.eq_spec mask1 (Int.not mask2)). rewrite H6. intro. + subst. rewrite Int.rolm_zero. EvalOp. + caseEq (Int.eq amount2 Int.zero && Int.eq mask2 (Int.not mask1)); intro. + destruct (andb_prop _ _ H5). + generalize (Int.eq_spec amount2 Int.zero). rewrite H6. intro. + generalize (Int.eq_spec mask2 (Int.not mask1)). rewrite H7. intro. + subst. rewrite Int.rolm_zero. rewrite Int.or_commut. EvalOp. simpl. apply eval_Eop with (Vint x :: Vint y :: nil). econstructor. EvalOp. simpl. congruence. econstructor. EvalOp. simpl. congruence. constructor. auto. EvalOp. Qed. + Theorem eval_divs: forall le a b x y, eval_expr ge sp e m le a (Vint x) -> |