summaryrefslogtreecommitdiff
path: root/powerpc
diff options
context:
space:
mode:
Diffstat (limited to 'powerpc')
-rw-r--r--powerpc/Asm.v6
-rw-r--r--powerpc/Asmgen.v6
-rw-r--r--powerpc/ConstpropOp.vp2
-rw-r--r--powerpc/Op.v10
-rw-r--r--powerpc/PrintAsm.ml4
-rw-r--r--powerpc/SelectOp.vp32
-rw-r--r--powerpc/SelectOpproof.v74
7 files changed, 63 insertions, 71 deletions
diff --git a/powerpc/Asm.v b/powerpc/Asm.v
index bbe2d3e..e6e9d76 100644
--- a/powerpc/Asm.v
+++ b/powerpc/Asm.v
@@ -193,6 +193,8 @@ Inductive instruction : Type :=
| Pmtlr: ireg -> instruction (**r move ireg to LR *)
| 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 *)
| 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 *)
@@ -702,6 +704,10 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome
Next (nextinstr (rs#rd <- (Val.mul rs#r1 (const_low cst)))) m
| Pmullw rd r1 r2 =>
Next (nextinstr (rs#rd <- (Val.mul rs#r1 rs#r2))) m
+ | Pmulhw rd r1 r2 =>
+ Next (nextinstr (rs#rd <- (Val.mulhs rs#r1 rs#r2))) m
+ | Pmulhwu rd r1 r2 =>
+ Next (nextinstr (rs#rd <- (Val.mulhu rs#r1 rs#r2))) m
| Pnand rd r1 r2 =>
Next (nextinstr (rs#rd <- (Val.notint (Val.and rs#r1 rs#r2)))) m
| Pnor rd r1 r2 =>
diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v
index 2b6d80d..cc9a51c 100644
--- a/powerpc/Asmgen.v
+++ b/powerpc/Asmgen.v
@@ -371,6 +371,12 @@ Definition transl_op
Pmulli r r1 (Cint n) :: k
else
loadimm GPR0 n (Pmullw r r1 GPR0 :: k))
+ | Omulhs, a1 :: a2 :: nil =>
+ do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res;
+ OK (Pmulhw r r1 r2 :: k)
+ | Omulhu, a1 :: a2 :: nil =>
+ do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res;
+ OK (Pmulhwu r r1 r2 :: k)
| Odiv, a1 :: a2 :: nil =>
do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res;
OK (Pdivw r r1 r2 :: k)
diff --git a/powerpc/ConstpropOp.vp b/powerpc/ConstpropOp.vp
index e7e4095..d0322c1 100644
--- a/powerpc/ConstpropOp.vp
+++ b/powerpc/ConstpropOp.vp
@@ -95,6 +95,8 @@ Nondetfunction eval_static_operation (op: operation) (vl: list approx) :=
| Osubimm n, I n1 :: nil => I (Int.sub n n1)
| Omul, I n1 :: I n2 :: nil => I(Int.mul n1 n2)
| Omulimm n, I n1 :: nil => I(Int.mul n1 n)
+ | Omulhs, I n1 :: I n2 :: nil => I(Int.mulhs n1 n2)
+ | Omulhu, I n1 :: I n2 :: nil => I(Int.mulhu n1 n2)
| Odiv, I n1 :: I n2 :: nil =>
if Int.eq n2 Int.zero then Unknown else
if Int.eq n1 (Int.repr Int.min_signed) && Int.eq n2 Int.mone then Unknown
diff --git a/powerpc/Op.v b/powerpc/Op.v
index 1952304..085a098 100644
--- a/powerpc/Op.v
+++ b/powerpc/Op.v
@@ -65,6 +65,8 @@ Inductive operation : Type :=
| Osubimm: int -> operation (**r [rd = n - r1] *)
| Omul: operation (**r [rd = r1 * r2] *)
| Omulimm: int -> operation (**r [rd = r1 * n] *)
+ | Omulhs: operation (**r [rd = high part of r1 * r2, signed] *)
+ | Omulhu: operation (**r [rd = high part of r1 * r2, unsigned] *)
| Odiv: operation (**r [rd = r1 / r2] (signed) *)
| Odivu: operation (**r [rd = r1 / r2] (unsigned) *)
| Oand: operation (**r [rd = r1 & r2] *)
@@ -185,6 +187,8 @@ Definition eval_operation
| Osubimm n, v1::nil => Some (Val.sub (Vint n) v1)
| Omul, v1::v2::nil => Some (Val.mul v1 v2)
| Omulimm n, v1::nil => Some (Val.mul v1 (Vint n))
+ | Omulhs, v1::v2::nil => Some (Val.mulhs v1 v2)
+ | Omulhu, v1::v2::nil => Some (Val.mulhu v1 v2)
| Odiv, v1::v2::nil => Val.divs v1 v2
| Odivu, v1::v2::nil => Val.divu v1 v2
| Oand, v1::v2::nil => Some(Val.and v1 v2)
@@ -276,6 +280,8 @@ Definition type_of_operation (op: operation) : list typ * typ :=
| Osubimm _ => (Tint :: nil, Tint)
| Omul => (Tint :: Tint :: nil, Tint)
| Omulimm _ => (Tint :: nil, Tint)
+ | Omulhs => (Tint :: Tint :: nil, Tint)
+ | Omulhu => (Tint :: Tint :: nil, Tint)
| Odiv => (Tint :: Tint :: nil, Tint)
| Odivu => (Tint :: Tint :: nil, Tint)
| Oand => (Tint :: Tint :: nil, Tint)
@@ -351,6 +357,8 @@ Proof with (try exact I).
destruct v0...
destruct v0; destruct v1...
destruct v0...
+ destruct v0; destruct v1...
+ destruct v0; destruct v1...
destruct v0; destruct v1; simpl in *; inv H0.
destruct (Int.eq i0 Int.zero
|| Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H2...
@@ -759,6 +767,8 @@ Proof.
inv H4; auto.
inv H4; inv H2; simpl; auto.
inv H4; simpl; auto.
+ inv H4; inv H2; simpl; auto.
+ inv H4; inv H2; simpl; auto.
inv H4; inv H3; simpl in H1; inv H1. simpl.
destruct (Int.eq i0 Int.zero
|| Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H2. TrivialExists.
diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml
index 879d755..08438df 100644
--- a/powerpc/PrintAsm.ml
+++ b/powerpc/PrintAsm.ml
@@ -818,6 +818,10 @@ let print_instruction oc tbl pc fallthrough = function
fprintf oc " mulli %a, %a, %a\n" ireg r1 ireg r2 constant c
| Pmullw(r1, r2, r3) ->
fprintf oc " mullw %a, %a, %a\n" ireg r1 ireg r2 ireg r3
+ | Pmulhw(r1, r2, r3) ->
+ fprintf oc " mulhw %a, %a, %a\n" ireg r1 ireg r2 ireg r3
+ | Pmulhwu(r1, r2, r3) ->
+ fprintf oc " mulhwu %a, %a, %a\n" ireg r1 ireg r2 ireg r3
| Pnand(r1, r2, r3) ->
fprintf oc " nand %a, %a, %a\n" ireg r1 ireg r2 ireg r3
| Pnor(r1, r2, r3) ->
diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp
index 7b15ccc..bc9b677 100644
--- a/powerpc/SelectOp.vp
+++ b/powerpc/SelectOp.vp
@@ -290,8 +290,6 @@ Nondetfunction xor (e1: expr) (e2: expr) :=
(** ** Integer division and modulus *)
-Definition divs (e1: expr) (e2: expr) := Eop Odiv (e1:::e2:::Enil).
-
Definition mod_aux (divop: operation) (e1 e2: expr) :=
Elet e1
(Elet (lift e2)
@@ -301,31 +299,13 @@ Definition mod_aux (divop: operation) (e1 e2: expr) :=
Enil) :::
Enil))).
-Definition mods := mod_aux Odiv.
-
-Definition divuimm (e: expr) (n: int) :=
- match Int.is_power2 n with
- | Some l => shruimm e l
- | None => Eop Odivu (e ::: Eop (Ointconst n) Enil ::: Enil)
- end.
-
-Nondetfunction divu (e1: expr) (e2: expr) :=
- match e2 with
- | Eop (Ointconst n2) Enil => divuimm e1 n2
- | _ => Eop Odivu (e1:::e2:::Enil)
- end.
-
-Definition moduimm (e: expr) (n: int) :=
- match Int.is_power2 n with
- | Some l => andimm (Int.sub n Int.one) e
- | None => mod_aux Odivu e (Eop (Ointconst n) Enil)
- end.
+Definition divs_base (e1: expr) (e2: expr) := Eop Odiv (e1:::e2:::Enil).
+Definition mods_base := mod_aux Odiv.
+Definition divu_base (e1: expr) (e2: expr) := Eop Odivu (e1:::e2:::Enil).
+Definition modu_base := mod_aux Odivu.
-Nondetfunction modu (e1: expr) (e2: expr) :=
- match e2 with
- | Eop (Ointconst n2) Enil => moduimm e1 n2
- | _ => mod_aux Odivu e1 e2
- end.
+Definition shrximm (e1: expr) (n2: int) :=
+ if Int.eq n2 Int.zero then e1 else Eop (Oshrximm n2) (e1:::Enil).
(** ** General shifts *)
diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v
index 5a0a903..177d64a 100644
--- a/powerpc/SelectOpproof.v
+++ b/powerpc/SelectOpproof.v
@@ -465,14 +465,14 @@ Proof.
TrivialExists.
Qed.
-Theorem eval_divs:
+Theorem eval_divs_base:
forall le a b x y z,
eval_expr ge sp e m le a x ->
eval_expr ge sp e m le b y ->
Val.divs x y = Some z ->
- exists v, eval_expr ge sp e m le (divs a b) v /\ Val.lessdef z v.
+ exists v, eval_expr ge sp e m le (divs_base a b) v /\ Val.lessdef z v.
Proof.
- intros. unfold divs. exists z; split. EvalOp. auto.
+ intros. unfold divs_base. exists z; split. EvalOp. auto.
Qed.
Lemma eval_mod_aux:
@@ -501,73 +501,57 @@ Proof.
reflexivity.
Qed.
-Theorem eval_mods:
+Theorem eval_mods_base:
forall le a b x y z,
eval_expr ge sp e m le a x ->
eval_expr ge sp e m le b y ->
Val.mods x y = Some z ->
- exists v, eval_expr ge sp e m le (mods a b) v /\ Val.lessdef z v.
+ exists v, eval_expr ge sp e m le (mods_base a b) v /\ Val.lessdef z v.
Proof.
- intros; unfold mods.
+ intros; unfold mods_base.
exploit Val.mods_divs; eauto. intros [v [A B]].
subst. econstructor; split; eauto.
apply eval_mod_aux with (semdivop := Val.divs); auto.
Qed.
-Theorem eval_divuimm:
- forall le n a x z,
- eval_expr ge sp e m le a x ->
- Val.divu x (Vint n) = Some z ->
- exists v, eval_expr ge sp e m le (divuimm a n) v /\ Val.lessdef z v.
-Proof.
- intros; unfold divuimm.
- destruct (Int.is_power2 n) eqn:?.
- replace z with (Val.shru x (Vint i)). apply eval_shruimm; auto.
- eapply Val.divu_pow2; eauto.
- TrivialExists.
- econstructor. eauto. econstructor. EvalOp. simpl; eauto. constructor. auto.
-Qed.
-
-Theorem eval_divu:
- forall le a x b y z,
+Theorem eval_divu_base:
+ forall le a b x y z,
eval_expr ge sp e m le a x ->
eval_expr ge sp e m le b y ->
Val.divu x y = Some z ->
- exists v, eval_expr ge sp e m le (divu a b) v /\ Val.lessdef z v.
+ exists v, eval_expr ge sp e m le (divu_base a b) v /\ Val.lessdef z v.
Proof.
- intros until z. unfold divu; destruct (divu_match b); intros; InvEval.
- eapply eval_divuimm; eauto.
- TrivialExists.
+ intros. unfold divu_base. exists z; split. EvalOp. auto.
Qed.
-Theorem eval_moduimm:
- forall le n a x z,
+Theorem eval_modu_base:
+ forall le a b x y z,
eval_expr ge sp e m le a x ->
- Val.modu x (Vint n) = Some z ->
- exists v, eval_expr ge sp e m le (moduimm a n) v /\ Val.lessdef z v.
+ eval_expr ge sp e m le b y ->
+ Val.modu x y = Some z ->
+ exists v, eval_expr ge sp e m le (modu_base a b) v /\ Val.lessdef z v.
Proof.
- intros; unfold moduimm.
- destruct (Int.is_power2 n) eqn:?.
- replace z with (Val.and x (Vint (Int.sub n Int.one))). apply eval_andimm; auto.
- eapply Val.modu_pow2; eauto.
+ intros; unfold modu_base.
exploit Val.modu_divu; eauto. intros [v [A B]].
subst. econstructor; split; eauto.
apply eval_mod_aux with (semdivop := Val.divu); auto.
- EvalOp.
Qed.
-Theorem eval_modu:
- forall le a x b y z,
+Theorem eval_shrximm:
+ forall le a n x z,
eval_expr ge sp e m le a x ->
- eval_expr ge sp e m le b y ->
- Val.modu x y = Some z ->
- exists v, eval_expr ge sp e m le (modu a b) v /\ Val.lessdef z v.
+ Val.shrx x (Vint n) = Some z ->
+ exists v, eval_expr ge sp e m le (shrximm a n) v /\ Val.lessdef z v.
Proof.
- intros until y; unfold modu; case (modu_match b); intros; InvEval.
- eapply eval_moduimm; eauto.
- exploit Val.modu_divu; eauto. intros [v [A B]].
- subst. econstructor; split; eauto.
- apply eval_mod_aux with (semdivop := Val.divu); auto.
+ intros. unfold shrximm.
+ predSpec Int.eq Int.eq_spec n Int.zero.
+ subst n. exists x; split; auto.
+ destruct x; simpl in H0; try discriminate.
+ destruct (Int.ltu Int.zero (Int.repr 31)); inv H0.
+ replace (Int.shrx i Int.zero) with i. auto.
+ unfold Int.shrx, Int.divs. rewrite Int.shl_zero.
+ change (Int.signed Int.one) with 1. rewrite Z.quot_1_r. rewrite Int.repr_signed; auto.
+ econstructor; split. EvalOp. auto.
Qed.
Theorem eval_shl: binary_constructor_sound shl Val.shl.
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-03 18:17:48 +0000