diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-04 23:54:54 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-04 23:54:54 +0200 |
| commit | a4f081bd7972c9007104942bdf90a4042397e167 (patch) | |
| tree | e8594c94bfe317361e11a6f44f8d8f10aad742b9 | |
| parent | f3e66ed3163115c4ecb605190cc83c52ad0e1ba5 (diff) | |
| download | compcert-kvx-a4f081bd7972c9007104942bdf90a4042397e167.tar.gz compcert-kvx-a4f081bd7972c9007104942bdf90a4042397e167.zip | |
some more Oselect comparisons
| -rw-r--r-- | mppa_k1c/Asmblockgen.v | 2 | ||||
| -rw-r--r-- | mppa_k1c/Asmblockgenproof1.v | 13 |
2 files changed, 14 insertions, 1 deletions
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index 722c4acc..d770eebc 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -737,6 +737,8 @@ Definition transl_op (match cond with | Ccomp0 cmp => OK (Pcmove (btest_for_cmpswz cmp) r0 rS r1 ::i k) + | Ccompl0 cmp => + OK (Pcmove (btest_for_cmpsdz cmp) r0 rS r1 ::i k) | _ => Error (msg "Asmblockgen Oselect") end) diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v index e8e04019..e58c7f0c 100644 --- a/mppa_k1c/Asmblockgenproof1.v +++ b/mppa_k1c/Asmblockgenproof1.v @@ -1638,7 +1638,7 @@ Opaque Int.eq. exploit transl_cond_op_correct; eauto. intros (rs' & A & B & C). exists rs'; split. eexact A. eauto with asmgen. - (* Oselect *) - destruct cond in *; simpl in *; try congruence; injection EQ3; clear EQ3; intro Hrew; rewrite <- Hrew in *. + destruct cond in *; simpl in *; try congruence; injection EQ3; clear EQ3; intro Hrew; rewrite <- Hrew in *; econstructor; split. + eapply exec_straight_one. @@ -1652,6 +1652,17 @@ Opaque Int.eq. destruct b; simpl; rewrite Pregmap.gss; constructor. * intros. rewrite Pregmap.gso; congruence. + + eapply exec_straight_one. + simpl; reflexivity. + + 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. - (* Oselectl *) econstructor; split. + eapply exec_straight_one. |