diff options
Diffstat (limited to 'powerpc')
| -rw-r--r-- | powerpc/ConstpropOp.vp | 16 | ||||
| -rw-r--r-- | powerpc/ConstpropOpproof.v | 45 |
2 files changed, 55 insertions, 6 deletions
diff --git a/powerpc/ConstpropOp.vp b/powerpc/ConstpropOp.vp index f18a72e9..2d492b66 100644 --- a/powerpc/ConstpropOp.vp +++ b/powerpc/ConstpropOp.vp @@ -65,6 +65,12 @@ Nondetfunction cond_strength_reduction 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'). +Definition is_an_integer (v: aval) : bool := + match v with + | Vbot | I _ | Uns _ _ | Sgn _ _ => true + | _ => false + end. + Nondetfunction make_cmp (c: condition) (args: list reg) (vl: list aval) := match c, args, vl with | Ccompimm Ceq n, r1 :: nil, v1 :: nil => @@ -75,6 +81,16 @@ Nondetfunction make_cmp (c: condition) (args: list reg) (vl: list aval) := if Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1) then (Omove, r1 :: nil) else if Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1) then (Oxorimm Int.one, r1 :: nil) else make_cmp_base c args vl + | Ccompuimm Ceq n, r1 :: nil, v1 :: nil => + if Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1) then (Omove, r1 :: nil) + else if Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1) then (Oxorimm Int.one, r1 :: nil) + else if is_an_integer v1 then make_cmp_base (Ccompimm Ceq n) args vl + else make_cmp_base c args vl + | Ccompuimm Cne n, r1 :: nil, v1 :: nil => + if Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1) then (Omove, r1 :: nil) + else if Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1) then (Oxorimm Int.one, r1 :: nil) + else if is_an_integer v1 then make_cmp_base (Ccompimm Cne n) args vl + else make_cmp_base c args vl | _, _, _ => make_cmp_base c args vl end. diff --git a/powerpc/ConstpropOpproof.v b/powerpc/ConstpropOpproof.v index 7fddd053..fe061e5b 100644 --- a/powerpc/ConstpropOpproof.v +++ b/powerpc/ConstpropOpproof.v @@ -156,25 +156,58 @@ Proof. assert (Y: forall r, vincl (AE.get r ae) (Uns Ptop 1) = true -> rs#r = Vundef \/ rs#r = Vint Int.zero \/ rs#r = Vint Int.one). { intros. apply vmatch_Uns_1 with bc Ptop. eapply vmatch_ge. eapply vincl_ge; eauto. apply MATCH. } + assert (Z: forall r, is_an_integer (AE.get r ae) = true -> + match rs#r with Vptr _ _ => False | _ => True end). + { intros. generalize (MATCH r); intro V. revert H. inv V; auto; discriminate. } unfold make_cmp. case (make_cmp_match c args vl); intros. - destruct (Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1)) eqn:E1. - simpl in H; inv H. InvBooleans. subst n. ++ 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 Ptop 1)) eqn:E0. - simpl in H; inv H. InvBooleans. subst n. ++ destruct (Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 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 Ptop 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 Ptop 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. +- destruct (Int.eq_dec n Int.one && vincl v1 (Uns Ptop 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 Ptop 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. +* destruct (is_an_integer v1) eqn:E. +** simpl in H; inv H. + replace (eval_condition (Ccompuimm Ceq n) rs##(r1::nil) m) + with (eval_condition (Ccompimm Ceq n) rs##(r1::nil) m). apply make_cmp_base_correct; auto. + simpl. apply Z in E. destruct (rs#r1); auto; contradiction. +** apply make_cmp_base_correct; auto. - destruct (Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1)) eqn:E0. - simpl in H; inv H. InvBooleans. subst n. ++ 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 Ptop 1)) eqn:E1. - simpl in H; inv H. InvBooleans. subst n. ++ destruct (Int.eq_dec n Int.one && vincl v1 (Uns Ptop 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. +* destruct (is_an_integer v1) eqn:E. +** simpl in H; inv H. + replace (eval_condition (Ccompuimm Cne n) rs##(r1::nil) m) + with (eval_condition (Ccompimm Cne n) rs##(r1::nil) m). apply make_cmp_base_correct; auto. + simpl. apply Z in E. destruct (rs#r1); auto; contradiction. +** apply make_cmp_base_correct; auto. - apply make_cmp_base_correct; auto. Qed. |