diff options
Diffstat (limited to 'arm/Asmgenproof1.v')
| -rw-r--r-- | arm/Asmgenproof1.v | 25 |
1 files changed, 24 insertions, 1 deletions
diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v index edf35bb8..807e069d 100644 --- a/arm/Asmgenproof1.v +++ b/arm/Asmgenproof1.v @@ -1189,7 +1189,7 @@ Lemma transl_op_correct_same: forall op args res k c (rs: regset) m v, transl_op op args res k = OK c -> eval_operation ge rs#IR13 op (map rs (map preg_of args)) m = Some v -> - match op with Ocmp _ => False | Oaddrstack _ => False | _ => True end -> + match op with Ocmp _ => False | Osel _ _ => False | Oaddrstack _ => False | _ => True end -> exists rs', exec_straight ge fn c rs m k rs' m /\ rs'#(preg_of res) = v @@ -1333,6 +1333,8 @@ Transparent destroyed_by_op. intuition Simpl. (* Ocmp *) contradiction. + (* Osel *) + contradiction. Qed. Lemma transl_op_correct: @@ -1369,6 +1371,27 @@ Proof. split; intros; Simpl. destruct (eval_condition c0 rs ## (preg_of ## args) m) as [b|]; simpl; auto. destruct B as [B1 B2]; rewrite B1. destruct b; auto. +- (* Osel *) + clear SAME. simpl in H. ArgsInv. simpl in H0; inv H0. + assert (D1: data_preg (preg_of m0) = true) by auto with asmgen. + assert (D2: data_preg (preg_of m1) = true) by auto with asmgen. + destruct (preg_of res) eqn:RES; monadInv H. ++ inv EQ2. rewrite (ireg_of_eq _ _ EQ), (ireg_of_eq _ _ EQ1) in *. + exploit transl_cond_correct; eauto. instantiate (1 := rs). instantiate (1 := m). intros [rs1 [A [B C]]]. + econstructor; split. + eapply exec_straight_trans. eexact A. apply exec_straight_one. simpl; eauto. auto. + split; intros; Simpl. + rewrite ! C by auto. + destruct (eval_condition c0 rs ## (preg_of ## args) m) as [b|]; simpl; auto. + destruct B as [B1 B2]; rewrite B1. destruct b; apply Val.lessdef_normalize. ++ inv EQ2. rewrite (freg_of_eq _ _ EQ), (freg_of_eq _ _ EQ1) in *. + exploit transl_cond_correct; eauto. instantiate (1 := rs). instantiate (1 := m). intros [rs1 [A [B C]]]. + econstructor; split. + eapply exec_straight_trans. eexact A. apply exec_straight_one. simpl; eauto. auto. + split; intros; Simpl. + rewrite ! C by auto. + destruct (eval_condition c0 rs ## (preg_of ## args) m) as [b|]; simpl; auto. + destruct B as [B1 B2]; rewrite B1. destruct b; apply Val.lessdef_normalize. Qed. (** Translation of loads and stores. *) |