diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-09-02 12:42:19 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-09-02 12:42:19 +0000 |
| commit | 265fa07b34a813ba9d8249ddad82d71e6002c10d (patch) | |
| tree | 45831b1793c7920b10969fc7cf6316c202d78e91 /backend/RTLgenproof.v | |
| parent | 94470fb6a652cb993982269fcb7a0e8319b54488 (diff) | |
| download | compcert-kvx-265fa07b34a813ba9d8249ddad82d71e6002c10d.tar.gz compcert-kvx-265fa07b34a813ba9d8249ddad82d71e6002c10d.zip | |
Merge of the reuse-temps branch:
- Reload temporaries are marked as destroyed (set to Vundef) across
operations in the semantics of LTL, LTLin, Linear and Mach,
allowing Asmgen to reuse them.
- Added IA32 port.
- Cleaned up float conversions and axiomatization of floats.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1499 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend/RTLgenproof.v')
| -rw-r--r-- | backend/RTLgenproof.v | 17 |
1 files changed, 15 insertions, 2 deletions
diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v index 12a8e2be..b49b671a 100644 --- a/backend/RTLgenproof.v +++ b/backend/RTLgenproof.v @@ -587,7 +587,8 @@ Lemma transl_expr_Eop_correct: eval_operation ge sp op vargs = Some v -> transl_expr_prop le (Eop op args) v. Proof. - intros; red; intros. inv TE. + intros; red; intros. inv TE. +(* normal case *) exploit H0; eauto. intros [rs1 [EX1 [ME1 [RR1 RO1]]]]. exists (rs1#rd <- v). (* Exec *) @@ -1116,12 +1117,24 @@ Proof. constructor; auto. (* assign *) - inv TS. + inv TS. + (* optimized translation (not 2 addr) *) exploit transl_expr_correct; eauto. intros [rs' [A [B [C D]]]]. econstructor; split. right; split. eauto. Lt_state. econstructor; eauto. constructor. + (* alternate translation (2 addr) *) + exploit transl_expr_correct; eauto. + intros [rs' [A [B [C D]]]]. + exploit tr_move_correct; eauto. + intros [rs'' [P [Q R]]]. + econstructor; split. + right; split. eapply star_trans. eexact A. eexact P. traceEq. Lt_state. + econstructor; eauto. constructor. + simpl in B. apply match_env_invariant with (rs'#r <- v). + apply match_env_update_var; auto. + intros. rewrite Regmap.gsspec. destruct (peq r0 r). congruence. auto. (* store *) inv TS. |