diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-01-14 14:23:26 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-01-14 14:23:26 +0000 |
| commit | a82c9c0e4a0b8e37c9c3ea5ae99714982563606f (patch) | |
| tree | 93b9999698a4cd47ec4cb5fcdcdfd215d62f8e9e /arm/Asmgenproof.v | |
| parent | bb8f49c419eb8205ef541edcbe17f4d14aa99564 (diff) | |
| download | compcert-kvx-a82c9c0e4a0b8e37c9c3ea5ae99714982563606f.tar.gz compcert-kvx-a82c9c0e4a0b8e37c9c3ea5ae99714982563606f.zip | |
Merge of the nonstrict-ops branch:
- Most RTL operators now evaluate to Some Vundef instead of None
when undefined behavior occurs.
- More aggressive instruction selection.
- "Bertotization" of pattern-matchings now implemented by a proper preprocessor.
- Cast optimization moved to cfrontend/Cminorgen; removed backend/CastOptim.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1790 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'arm/Asmgenproof.v')
| -rw-r--r-- | arm/Asmgenproof.v | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v index 48f265b8..a888aae6 100644 --- a/arm/Asmgenproof.v +++ b/arm/Asmgenproof.v @@ -791,10 +791,9 @@ Proof. exists m'; split; auto. exists rs'; split. simpl. eexact P. assert (agree (Regmap.set res v ms) sp rs'). - apply agree_set_mreg with rs; auto. congruence. - auto with ppcgen. + apply agree_set_mreg with rs; auto. eapply Val.lessdef_trans; eauto. assert (agree (Regmap.set res v (undef_temps ms)) sp rs'). - apply agree_set_undef_mreg with rs; auto. congruence. + apply agree_set_undef_mreg with rs; auto. eapply Val.lessdef_trans; eauto. auto with ppcgen. destruct op; assumption. Qed. @@ -1086,7 +1085,8 @@ Proof. exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. intros A. exploit transl_cond_correct. eauto. eauto. - intros [rs2 [EX [RES OTH]]]. + instantiate (1 := rs). instantiate (1 := m'). unfold PregEq.t. rewrite A. + intros [rs2 [EX [RES OTH]]]. inv AT. simpl in H5. generalize (functions_transl _ _ H4); intro FN. generalize (functions_transl_no_overflow _ _ H4); intro NOOV. @@ -1120,7 +1120,8 @@ Proof. intro WTI. inv WTI. exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. intros A. - exploit transl_cond_correct. eauto. eauto. + exploit transl_cond_correct. eauto. + instantiate (1 := rs). instantiate (1 := m'). unfold PregEq.t. rewrite A. intros [rs2 [EX [RES OTH]]]. left; eapply exec_straight_steps; eauto with coqlib. exists m'; split; auto. |