summaryrefslogtreecommitdiff
path: root/powerpc
diff options
context:
space:
mode:
Diffstat (limited to 'powerpc')
-rw-r--r--powerpc/ConstpropOp.vp24
-rw-r--r--powerpc/ConstpropOpproof.v54
-rw-r--r--powerpc/SelectOp.vp57
-rw-r--r--powerpc/SelectOpproof.v46
4 files changed, 153 insertions, 28 deletions
diff --git a/powerpc/ConstpropOp.vp b/powerpc/ConstpropOp.vp
index 6aa0925..e1e1960 100644
--- a/powerpc/ConstpropOp.vp
+++ b/powerpc/ConstpropOp.vp
@@ -46,6 +46,23 @@ Nondetfunction cond_strength_reduction
(cond, args)
end.
+Definition make_cmp_base (c: condition) (args: list reg) (vl: list aval) :=
+ let (c', args') := cond_strength_reduction c args vl in (Ocmp c', args').
+
+Nondetfunction make_cmp (c: condition) (args: list reg) (vl: list aval) :=
+ match c, args, vl with
+ | Ccompimm Ceq n, r1 :: nil, v1 :: nil =>
+ if Int.eq_dec n Int.one && vincl v1 (Uns 1) then (Omove, r1 :: nil)
+ else if Int.eq_dec n Int.zero && vincl v1 (Uns 1) then (Oxorimm Int.one, r1 :: nil)
+ else make_cmp_base c args vl
+ | Ccompimm Cne n, r1 :: nil, v1 :: nil =>
+ if Int.eq_dec n Int.zero && vincl v1 (Uns 1) then (Omove, r1 :: nil)
+ else if Int.eq_dec n Int.one && vincl v1 (Uns 1) then (Oxorimm Int.one, r1 :: nil)
+ else make_cmp_base c args vl
+ | _, _, _ =>
+ make_cmp_base c args vl
+ end.
+
Definition make_addimm (n: int) (r: reg) :=
if Int.eq n Int.zero
then (Omove, r :: nil)
@@ -114,8 +131,8 @@ Definition make_orimm (n: int) (r: reg) :=
else (Oorimm n, r :: nil).
Definition make_xorimm (n: int) (r: reg) :=
- if Int.eq n Int.zero
- then (Omove, r :: nil)
+ if Int.eq n Int.zero then (Omove, r :: nil)
+ else if Int.eq n Int.mone then (Onot, r :: nil)
else (Oxorimm n, r :: nil).
Definition make_mulfimm (n: float) (r r1 r2: reg) :=
@@ -158,8 +175,7 @@ Nondetfunction op_strength_reduction
| 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 =>
- let (c', args') := cond_strength_reduction c args vl in (Ocmp c', args')
+ | 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
| _, _, _ => (op, args)
diff --git a/powerpc/ConstpropOpproof.v b/powerpc/ConstpropOpproof.v
index 0c88246..a28d908 100644
--- a/powerpc/ConstpropOpproof.v
+++ b/powerpc/ConstpropOpproof.v
@@ -106,6 +106,52 @@ Proof.
- auto.
Qed.
+Lemma make_cmp_base_correct:
+ forall c args vl,
+ vl = map (fun r => AE.get r ae) args ->
+ let (op', args') := make_cmp_base c args vl in
+ exists v, eval_operation ge (Vptr sp Int.zero) op' rs##args' m = Some v
+ /\ Val.lessdef (Val.of_optbool (eval_condition c rs##args m)) v.
+Proof.
+ intros. unfold make_cmp_base.
+ generalize (cond_strength_reduction_correct c args vl H).
+ destruct (cond_strength_reduction c args vl) as [c' args']. intros EQ.
+ econstructor; split. simpl; eauto. rewrite EQ. auto.
+Qed.
+
+Lemma make_cmp_correct:
+ forall c args vl,
+ vl = map (fun r => AE.get r ae) args ->
+ let (op', args') := make_cmp c args vl in
+ exists v, eval_operation ge (Vptr sp Int.zero) op' rs##args' m = Some v
+ /\ Val.lessdef (Val.of_optbool (eval_condition c rs##args m)) v.
+Proof.
+ intros c args vl.
+ assert (Y: forall r, vincl (AE.get r ae) (Uns 1) = true ->
+ rs#r = Vundef \/ rs#r = Vint Int.zero \/ rs#r = Vint Int.one).
+ { intros. apply vmatch_Uns_1 with bc. eapply vmatch_ge. eapply vincl_ge; eauto. apply MATCH. }
+ unfold make_cmp. case (make_cmp_match c args vl); intros.
+- destruct (Int.eq_dec n Int.one && vincl v1 (Uns 1)) eqn:E1.
+ simpl in H; inv H. InvBooleans. subst n.
+ exists (rs#r1); split; auto. simpl.
+ exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
+ destruct (Int.eq_dec n Int.zero && vincl v1 (Uns 1)) eqn:E0.
+ simpl in H; inv H. InvBooleans. subst n.
+ exists (Val.xor rs#r1 (Vint Int.one)); split; auto. simpl.
+ exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
+ apply make_cmp_base_correct; auto.
+- destruct (Int.eq_dec n Int.zero && vincl v1 (Uns 1)) eqn:E0.
+ simpl in H; inv H. InvBooleans. subst n.
+ exists (rs#r1); split; auto. simpl.
+ exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
+ destruct (Int.eq_dec n Int.one && vincl v1 (Uns 1)) eqn:E1.
+ simpl in H; inv H. InvBooleans. subst n.
+ exists (Val.xor rs#r1 (Vint Int.one)); split; auto. simpl.
+ exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
+ apply make_cmp_base_correct; auto.
+- apply make_cmp_base_correct; auto.
+Qed.
+
Lemma make_addimm_correct:
forall n r,
let (op, args) := make_addimm n r in
@@ -256,7 +302,9 @@ Lemma make_xorimm_correct:
Proof.
intros; unfold make_xorimm.
predSpec Int.eq Int.eq_spec n Int.zero; intros.
- subst n. exists (rs#r); split; auto. destruct (rs#r); simpl; auto. rewrite Int.xor_zero; auto.
+ subst n. exists (rs#r); split; auto. destruct (rs#r); simpl; auto. rewrite Int.xor_zero; auto.
+ predSpec Int.eq Int.eq_spec n Int.mone; intros.
+ subst n. exists (Val.notint rs#r); split; auto.
econstructor; split; eauto. auto.
Qed.
@@ -379,9 +427,7 @@ Proof.
(* singleoffloat *)
InvApproxRegs; SimplVM; inv H0. apply make_singleoffloat_correct; auto.
(* cmp *)
- generalize (cond_strength_reduction_correct c args0 vl0).
- destruct (cond_strength_reduction c args0 vl0) as [c' args']; intros.
- rewrite <- H1 in H0; auto. econstructor; split; eauto.
+ 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).
diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp
index ad4f3b9..371a08a 100644
--- a/powerpc/SelectOp.vp
+++ b/powerpc/SelectOp.vp
@@ -68,6 +68,7 @@ Nondetfunction notint (e: expr) :=
| Eop Onxor (t1:::t2:::Enil) => Eop Oxor (t1:::t2:::Enil)
| Eop Oandc (t1:::t2:::Enil) => Eop Oorc (t2:::t1:::Enil)
| Eop Oorc (t1:::t2:::Enil) => Eop Oandc (t2:::t1:::Enil)
+ | Eop (Oxorimm n) (t1:::Enil) => Eop (Oxorimm (Int.not n)) (t1:::Enil)
| _ => Eop Onot (e:::Enil)
end.
@@ -121,10 +122,22 @@ Nondetfunction add (e1: expr) (e2: expr) :=
(** ** Integer and pointer subtraction *)
+Nondetfunction subimm (n1: int) (e: expr) :=
+ match e with
+ | Eop (Ointconst n2) Enil =>
+ Eop (Ointconst (Int.sub n1 n2)) Enil
+ | Eop (Oaddimm n2) (t2:::Enil) =>
+ Eop (Osubimm (Int.sub n1 n2)) (t2 ::: Enil)
+ | _ =>
+ Eop (Osubimm n1) (e ::: Enil)
+ end.
+
Nondetfunction sub (e1: expr) (e2: expr) :=
match e1, e2 with
| t1, Eop (Ointconst n2) Enil =>
addimm (Int.neg n2) t1
+ | Eop (Ointconst n1) Enil, t2 =>
+ subimm n1 t2
| Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddimm n2) (t2:::Enil) =>
addimm (Int.sub n1 n2) (Eop Osub (t1:::t2:::Enil))
| Eop (Oaddimm n1) (t1:::Enil), t2 =>
@@ -135,7 +148,7 @@ Nondetfunction sub (e1: expr) (e2: expr) :=
Eop Osub (e1:::e2:::Enil)
end.
-Definition negint (e: expr) := Eop (Osubimm Int.zero) (e ::: Enil).
+Definition negint (e: expr) := subimm Int.zero e.
(** ** Rotates and immediate shifts *)
@@ -174,8 +187,12 @@ Definition shruimm (e1: expr) (n2: int) :=
Nondetfunction shrimm (e1: expr) (n2: int) :=
if Int.eq n2 Int.zero then
e1
+ else if negb (Int.ltu n2 Int.iwordsize) then
+ Eop Oshr (e1:::Eop (Ointconst n2) Enil:::Enil)
else
match e1 with
+ | Eop (Ointconst n1) Enil =>
+ Eop (Ointconst (Int.shr n1 n2)) Enil
| Eop (Oandimm mask1) (t1:::Enil) =>
if Int.lt mask1 Int.zero
then Eop (Oshrimm n2) (e1:::Enil)
@@ -293,9 +310,11 @@ Nondetfunction or (e1: expr) (e2: expr) :=
Nondetfunction xorimm (n1: int) (e2: expr) :=
if Int.eq n1 Int.zero then e2 else
+ if Int.eq n1 Int.mone then notint e2 else
match e2 with
| Eop (Ointconst n2) Enil => Eop (Ointconst (Int.xor n1 n2)) Enil
| Eop (Oxorimm n2) (t2:::Enil) => Eop (Oxorimm (Int.xor n1 n2)) (t2:::Enil)
+ | Eop Onot (t2:::Enil) => Eop (Oxorimm (Int.not n1)) (t2:::Enil)
| _ => Eop (Oxorimm n1) (e2:::Enil)
end.
@@ -418,11 +437,19 @@ Definition compf (c: comparison) (e1: expr) (e2: expr) :=
Definition cast8unsigned (e: expr) := andimm (Int.repr 255) e.
-Definition cast8signed (e: expr) := Eop Ocast8signed (e ::: Enil).
+Nondetfunction cast8signed (e: expr) :=
+ match e with
+ | Eop (Ointconst n) Enil => Eop (Ointconst (Int.sign_ext 8 n)) Enil
+ | _ => Eop Ocast8signed (e ::: Enil)
+ end.
Definition cast16unsigned (e: expr) := andimm (Int.repr 65535) e.
-Definition cast16signed (e: expr) := Eop Ocast16signed (e ::: Enil).
+Nondetfunction cast16signed (e: expr) :=
+ match e with
+ | Eop (Ointconst n) Enil => Eop (Ointconst (Int.sign_ext 16 n)) Enil
+ | _ => Eop Ocast16signed (e ::: Enil)
+ end.
(** ** Floating-point conversions *)
@@ -435,14 +462,24 @@ Definition intuoffloat (e: expr) :=
(intoffloat (Eletvar 1))
(addimm Float.ox8000_0000 (intoffloat (subf (Eletvar 1) (Eletvar 0))))))%nat.
-Definition floatofintu (e: expr) :=
- subf (Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil ::: e ::: Enil))
- (Eop (Ofloatconst (Float.from_words Float.ox4330_0000 Int.zero)) Enil).
+Nondetfunction floatofintu (e: expr) :=
+ match e with
+ | Eop (Ointconst n) Enil =>
+ Eop (Ofloatconst (Float.floatofintu n)) Enil
+ | _ =>
+ subf (Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil ::: e ::: Enil))
+ (Eop (Ofloatconst (Float.from_words Float.ox4330_0000 Int.zero)) Enil)
+ end.
-Definition floatofint (e: expr) :=
- 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).
+Nondetfunction floatofint (e: expr) :=
+ match e with
+ | Eop (Ointconst n) Enil =>
+ Eop (Ofloatconst (Float.floatofint 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 singleoffloat (e: expr) := Eop Osingleoffloat (e ::: Enil).
diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v
index 4d26cf6..b6412c0 100644
--- a/powerpc/SelectOpproof.v
+++ b/powerpc/SelectOpproof.v
@@ -150,6 +150,7 @@ Proof.
subst. exists (Val.and v0 (Val.notint v1)); split. EvalOp.
destruct v0; destruct v1; simpl; auto. rewrite Int.not_or_and_not. rewrite Int.not_involutive.
rewrite Int.and_commut. auto.
+ subst x. TrivialExists. simpl. rewrite Val.not_xor. rewrite Val.xor_assoc. auto.
TrivialExists.
Qed.
@@ -218,11 +219,23 @@ Proof.
- TrivialExists.
Qed.
+Theorem eval_subimm:
+ forall n, unary_constructor_sound (subimm n) (fun v => Val.sub (Vint n) v).
+Proof.
+ intros; red; intros until x. unfold subimm. destruct (subimm_match a); intros.
+ InvEval. TrivialExists.
+ InvEval. subst x. TrivialExists. unfold eval_operation. destruct v1; simpl; auto.
+ rewrite ! Int.sub_add_opp. rewrite Int.add_assoc. f_equal. f_equal. f_equal.
+ rewrite Int.neg_add_distr. apply Int.add_commut.
+ TrivialExists.
+Qed.
+
Theorem eval_sub: binary_constructor_sound sub Val.sub.
Proof.
red; intros until y.
unfold sub; case (sub_match a b); intros; InvEval.
rewrite Val.sub_add_opp. apply eval_addimm; auto.
+ apply eval_subimm; auto.
subst. rewrite Val.sub_add_l. rewrite Val.sub_add_r.
rewrite Val.add_assoc. simpl. rewrite Int.add_commut. rewrite <- Int.sub_add_opp.
apply eval_addimm; EvalOp.
@@ -233,7 +246,7 @@ Qed.
Theorem eval_negint: unary_constructor_sound negint (fun v => Val.sub Vzero v).
Proof.
- red; intros. unfold negint. TrivialExists.
+ red; intros. unfold negint. apply eval_subimm; auto.
Qed.
Lemma eval_rolm:
@@ -280,15 +293,19 @@ Proof.
red; intros until x. unfold shrimm.
predSpec Int.eq Int.eq_spec n Int.zero.
intros. subst. exists x; split; auto. destruct x; simpl; auto. rewrite Int.shr_zero; auto.
+ destruct (Int.ltu n Int.iwordsize) eqn:WS.
case (shrimm_match a); intros.
- destruct (Int.lt mask1 Int.zero) eqn:?.
+ InvEval. exists (Vint (Int.shr n1 n)); split. EvalOp. simpl; rewrite WS; auto.
+ simpl; destruct (Int.lt mask1 Int.zero) eqn:?.
TrivialExists.
replace (Val.shr x (Vint n)) with (Val.shru x (Vint n)).
apply eval_shruimm; auto.
- destruct x; simpl; auto. destruct (Int.ltu n Int.iwordsize); auto.
+ destruct x; simpl; auto. rewrite WS.
decEq. symmetry. InvEval. destruct v1; simpl in H0; inv H0.
apply Int.shr_and_is_shru_and; auto.
- TrivialExists.
+ simpl. TrivialExists.
+ intros. simpl. TrivialExists.
+ constructor. eauto. constructor. EvalOp. simpl; eauto. constructor. auto.
Qed.
Lemma eval_mulimm_base:
@@ -475,7 +492,9 @@ Proof.
intros. subst. exists x; split; auto. destruct x; simpl; auto. rewrite Int.xor_zero; auto.
clear H. destruct (xorimm_match a); intros; InvEval.
TrivialExists. simpl. rewrite Int.xor_commut; auto.
- subst. rewrite Val.xor_assoc. simpl. rewrite Int.xor_commut. TrivialExists.
+ subst. rewrite Val.xor_assoc. simpl. rewrite Int.xor_commut. TrivialExists.
+ subst x. TrivialExists. simpl. rewrite Val.not_xor. rewrite Val.xor_assoc.
+ simpl. rewrite Int.xor_commut; auto.
TrivialExists.
Qed.
@@ -735,7 +754,9 @@ Qed.
Theorem eval_cast8signed: unary_constructor_sound cast8signed (Val.sign_ext 8).
Proof.
- red; intros. unfold cast8signed. TrivialExists.
+ red; intros until x. unfold cast8signed. destruct (cast8signed_match a); intros.
+ InvEval; TrivialExists.
+ TrivialExists.
Qed.
Theorem eval_cast8unsigned: unary_constructor_sound cast8unsigned (Val.zero_ext 8).
@@ -746,7 +767,9 @@ Qed.
Theorem eval_cast16signed: unary_constructor_sound cast16signed (Val.sign_ext 16).
Proof.
- red; intros. unfold cast16signed. TrivialExists.
+ red; intros until x. unfold cast16signed. destruct (cast16signed_match a); intros.
+ InvEval; TrivialExists.
+ TrivialExists.
Qed.
Theorem eval_cast16unsigned: unary_constructor_sound cast16unsigned (Val.zero_ext 16).
@@ -813,9 +836,10 @@ Theorem eval_floatofint:
Val.floatofint x = Some y ->
exists v, eval_expr ge sp e m le (floatofint a) v /\ Val.lessdef y v.
Proof.
- intros. destruct x; simpl in H0; inv H0.
+ 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.
- unfold floatofint.
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).
@@ -834,7 +858,9 @@ Theorem eval_floatofintu:
Val.floatofintu x = Some y ->
exists v, eval_expr ge sp e m le (floatofintu a) v /\ Val.lessdef y v.
Proof.
- intros. destruct x; simpl in H0; inv H0.
+ 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.
unfold floatofintu.
set (t2 := Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil ::: a ::: Enil)).
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-11 21:10:03 +0000