aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--powerpc/Asm.v4
-rw-r--r--powerpc/Asmgen.v7
-rw-r--r--powerpc/Asmgenproof.v1
-rw-r--r--powerpc/Asmgenproof1.v22
-rw-r--r--powerpc/Op.v15
-rw-r--r--powerpc/PrintAsm.ml5
-rw-r--r--powerpc/SelectOp.v45
-rw-r--r--powerpc/SelectOpproof.v12
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) ->
generated by cgit (git 2.34.1) at 2024-06-02 23:27:27 +0000