diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-05-21 16:26:30 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-05-21 16:26:30 +0000 |
| commit | 0053b1aa1d26da5d1f995a603b127daf799c2da9 (patch) | |
| tree | fec49ad37e5edffa5be742bafcadff3c8b8ede7f /backend/RTLgenproof.v | |
| parent | 219a2d178dcd5cc625f6b6261759f392cfca367b (diff) | |
| download | compcert-kvx-0053b1aa1d26da5d1f995a603b127daf799c2da9.tar.gz compcert-kvx-0053b1aa1d26da5d1f995a603b127daf799c2da9.zip | |
Merge of the newmem branch:
- Revised memory model with Max and Cur permissions, but without bounds
- Constant propagation of 'const' globals
- Function inlining at RTL level
- (Unprovable) elimination of unreferenced static definitions
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1899 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend/RTLgenproof.v')
| -rw-r--r-- | backend/RTLgenproof.v | 33 |
1 files changed, 30 insertions, 3 deletions
diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v index c5182db4..e06224a6 100644 --- a/backend/RTLgenproof.v +++ b/backend/RTLgenproof.v @@ -1142,7 +1142,8 @@ Proof. econstructor; eauto. constructor. (* call *) - inv TS. + inv TS; inv H. + (* indirect *) exploit transl_expr_correct; eauto. intros [rs' [A [B [C D]]]]. exploit transl_exprlist_correct; eauto. @@ -1154,9 +1155,21 @@ Proof. apply sig_transl_function; auto. traceEq. rewrite G. constructor. auto. econstructor; eauto. + (* direct *) + exploit transl_exprlist_correct; eauto. + intros [rs'' [E [F [G J]]]]. + exploit functions_translated; eauto. intros [tf' [P Q]]. + econstructor; split. + left; eapply plus_right. eexact E. + eapply exec_Icall; eauto. simpl. rewrite symbols_preserved. rewrite H4. + rewrite Genv.find_funct_find_funct_ptr in P. eauto. + apply sig_transl_function; auto. + traceEq. + rewrite G. constructor. auto. econstructor; eauto. (* tailcall *) - inv TS. + inv TS; inv H. + (* indirect *) exploit transl_expr_correct; eauto. intros [rs' [A [B [C D]]]]. exploit transl_exprlist_correct; eauto. @@ -1168,7 +1181,21 @@ Proof. left; eapply plus_right. eapply star_trans. eexact A. eexact E. reflexivity. eapply exec_Itailcall; eauto. simpl. rewrite J. rewrite C. eauto. simpl; auto. apply sig_transl_function; auto. - rewrite H2; eauto. + rewrite H; eauto. + traceEq. + rewrite G. constructor; auto. + (* direct *) + exploit transl_exprlist_correct; eauto. + intros [rs'' [E [F [G J]]]]. + exploit functions_translated; eauto. intros [tf' [P Q]]. + exploit match_stacks_call_cont; eauto. intros [U V]. + assert (fn_stacksize tf = fn_stackspace f). inv TF; auto. + econstructor; split. + left; eapply plus_right. eexact E. + eapply exec_Itailcall; eauto. simpl. rewrite symbols_preserved. rewrite H5. + rewrite Genv.find_funct_find_funct_ptr in P. eauto. + apply sig_transl_function; auto. + rewrite H; eauto. traceEq. rewrite G. constructor; auto. |