diff options
Diffstat (limited to 'mppa_k1c/Asmblockgenproof1.v')
| -rw-r--r-- | mppa_k1c/Asmblockgenproof1.v | 128 |
1 files changed, 111 insertions, 17 deletions
diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v index 874e40a8..6cf5c60c 100644 --- a/mppa_k1c/Asmblockgenproof1.v +++ b/mppa_k1c/Asmblockgenproof1.v @@ -1698,7 +1698,7 @@ Opaque Int.eq. * intros. rewrite Pregmap.gso; congruence. -- (* Oselect *) +- (* Oselectl *) destruct cond in *; simpl in *; try congruence; try monadInv EQ3; try (injection EQ3; clear EQ3; intro Hrew; rewrite <- Hrew in * ; clear Hrew); @@ -1760,31 +1760,125 @@ Opaque Int.eq. rewrite Pregmap.gso; congruence. - (* Oselectf *) - econstructor; split. - + eapply exec_straight_one. - simpl; reflexivity. + destruct cond in *; simpl in *; try congruence; + try monadInv EQ3; + try (injection EQ3; clear EQ3; intro Hrew; rewrite <- Hrew in * ; clear Hrew); + econstructor; split; + try ( eapply exec_straight_one; simpl; reflexivity ). + (* Cmp *) + split. - * unfold eval_selectf. - destruct (rs x1) eqn:eqX1; try constructor. + * unfold eval_select. destruct (rs x) eqn:eqX; try constructor. destruct (rs x0) eqn:eqX0; try constructor. - simpl. - rewrite int_eq_comm. - destruct (Int.eq i Int.zero); simpl; rewrite Pregmap.gss; constructor. + destruct c0 in *; simpl; + destruct (Val.cmp_bool _ _); simpl; try constructor; + destruct b; simpl; rewrite Pregmap.gss; constructor. * intros. rewrite Pregmap.gso; congruence. + (* Cmpu *) + + split. + * unfold eval_select. + destruct (rs x) eqn:eqX; try constructor. + destruct (rs x0) eqn:eqX0; try constructor. + destruct c0 in *; simpl in *; inv EQ2; simpl. + ** assert (Hcmpuabs := (Val_cmpu_bool_correct m Ceq (rs x1) (Vint Int.zero))). + destruct (Val.cmpu_bool _ _); simpl; try constructor. + destruct b in *; simpl in *; [ rewrite (Hcmpuabs true) | rewrite (Hcmpuabs false)]; trivial; + rewrite Pregmap.gss; constructor. + ** assert (Hcmpuabs := (Val_cmpu_bool_correct m Cne (rs x1) (Vint Int.zero))). + destruct (Val.cmpu_bool _ _); simpl; try constructor. + destruct b in *; simpl in *; [ rewrite (Hcmpuabs true) | rewrite (Hcmpuabs false)]; trivial; + rewrite Pregmap.gss; constructor. + * intros. + rewrite Pregmap.gso; congruence. + + (* Cmpl *) + + split. + * unfold eval_select. + destruct (rs x) eqn:eqX; try constructor. + destruct (rs x0) eqn:eqX0; try constructor. + destruct c0 in *; simpl; + destruct (Val.cmpl_bool _ _); simpl; try constructor; + destruct b; simpl; rewrite Pregmap.gss; constructor. + * intros. + rewrite Pregmap.gso; congruence. + + (* Cmplu *) + + split. + * unfold eval_select. + destruct (rs x) eqn:eqX; try constructor. + destruct (rs x0) eqn:eqX0; try constructor. + destruct c0 in *; simpl in *; inv EQ2; simpl. + ** assert (Hcmpluabs := (Val_cmplu_bool_correct m Ceq (rs x1) (Vlong Int64.zero))). + destruct (Val.cmplu_bool _ _); simpl; try constructor. + destruct b in *; simpl in *; [ rewrite (Hcmpluabs true) | rewrite (Hcmpluabs false)]; trivial; + rewrite Pregmap.gss; constructor. + ** assert (Hcmpluabs := (Val_cmplu_bool_correct m Cne (rs x1) (Vlong Int64.zero))). + destruct (Val.cmplu_bool _ _); simpl; try constructor. + destruct b in *; simpl in *; [ rewrite (Hcmpluabs true) | rewrite (Hcmpluabs false)]; trivial; + rewrite Pregmap.gss; constructor. + * intros. + rewrite Pregmap.gso; congruence. + + - (* Oselectfs *) - econstructor; split. - + eapply exec_straight_one. - simpl; reflexivity. + destruct cond in *; simpl in *; try congruence; + try monadInv EQ3; + try (injection EQ3; clear EQ3; intro Hrew; rewrite <- Hrew in * ; clear Hrew); + econstructor; split; + try ( eapply exec_straight_one; simpl; reflexivity ). + (* Cmp *) + + split. + * unfold eval_select. + destruct (rs x) eqn:eqX; try constructor. + destruct (rs x0) eqn:eqX0; try constructor. + destruct c0 in *; simpl; + destruct (Val.cmp_bool _ _); simpl; try constructor; + destruct b; simpl; rewrite Pregmap.gss; constructor. + * intros. + rewrite Pregmap.gso; congruence. + (* Cmpu *) + + split. + * unfold eval_select. + destruct (rs x) eqn:eqX; try constructor. + destruct (rs x0) eqn:eqX0; try constructor. + destruct c0 in *; simpl in *; inv EQ2; simpl. + ** assert (Hcmpuabs := (Val_cmpu_bool_correct m Ceq (rs x1) (Vint Int.zero))). + destruct (Val.cmpu_bool _ _); simpl; try constructor. + destruct b in *; simpl in *; [ rewrite (Hcmpuabs true) | rewrite (Hcmpuabs false)]; trivial; + rewrite Pregmap.gss; constructor. + ** assert (Hcmpuabs := (Val_cmpu_bool_correct m Cne (rs x1) (Vint Int.zero))). + destruct (Val.cmpu_bool _ _); simpl; try constructor. + destruct b in *; simpl in *; [ rewrite (Hcmpuabs true) | rewrite (Hcmpuabs false)]; trivial; + rewrite Pregmap.gss; constructor. + * intros. + rewrite Pregmap.gso; congruence. + + (* Cmpl *) + + split. + * unfold eval_select. + destruct (rs x) eqn:eqX; try constructor. + destruct (rs x0) eqn:eqX0; try constructor. + destruct c0 in *; simpl; + destruct (Val.cmpl_bool _ _); simpl; try constructor; + destruct b; simpl; rewrite Pregmap.gss; constructor. + * intros. + rewrite Pregmap.gso; congruence. + + (* Cmplu *) + split. - * unfold eval_selectfs. - destruct (rs x1) eqn:eqX1; try constructor. + * unfold eval_select. destruct (rs x) eqn:eqX; try constructor. destruct (rs x0) eqn:eqX0; try constructor. - simpl. - rewrite int_eq_comm. - destruct (Int.eq i Int.zero); simpl; rewrite Pregmap.gss; constructor. + destruct c0 in *; simpl in *; inv EQ2; simpl. + ** assert (Hcmpluabs := (Val_cmplu_bool_correct m Ceq (rs x1) (Vlong Int64.zero))). + destruct (Val.cmplu_bool _ _); simpl; try constructor. + destruct b in *; simpl in *; [ rewrite (Hcmpluabs true) | rewrite (Hcmpluabs false)]; trivial; + rewrite Pregmap.gss; constructor. + ** assert (Hcmpluabs := (Val_cmplu_bool_correct m Cne (rs x1) (Vlong Int64.zero))). + destruct (Val.cmplu_bool _ _); simpl; try constructor. + destruct b in *; simpl in *; [ rewrite (Hcmpluabs true) | rewrite (Hcmpluabs false)]; trivial; + rewrite Pregmap.gss; constructor. * intros. rewrite Pregmap.gso; congruence. Qed. |