diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2019-04-15 17:50:30 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2019-05-20 18:00:46 +0200 |
| commit | 49342474c19558709c8cea6d70eaba9a4dd7a150 (patch) | |
| tree | 86fb6e9fc2081a71a2d770811164bb2f72b867e6 /arm/Asmgenproof1.v | |
| parent | 996f2e071baaf52105714283d141af2eac8ffbfb (diff) | |
| download | compcert-kvx-49342474c19558709c8cea6d70eaba9a4dd7a150.tar.gz compcert-kvx-49342474c19558709c8cea6d70eaba9a4dd7a150.zip | |
Implement a `Osel` operation for ARM
The operation comples down to conditional moves.
Both integer and floating-point conditional moves are supported.
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. *) |