diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-05-08 07:07:25 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-05-08 07:07:25 +0000 |
| commit | c45fc2431ea70e0cb5a80e65d0ac99f91e94693e (patch) | |
| tree | dfc11f4507c6ddaab96074382d8406dbc4031f60 /driver/Compiler.v | |
| parent | 67e74f6f1a24247bfcd3d6c165a2d6cd45c83b06 (diff) | |
Added pass CleanupLabels to remove unreferenced labels in a proved way.
ia32/PrintAsm.ml: simplified accordingly; other PrintAsm.ml to be fixed.
ia32/Asm.v: Pmov_ri can undef flags (if translated to xor)
cparser/Ceval.ml: treat ~ in constant exprs
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1647 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'driver/Compiler.v')
| -rw-r--r-- | driver/Compiler.v | 14 |
1 files changed, 11 insertions, 3 deletions
diff --git a/driver/Compiler.v b/driver/Compiler.v index cf05b3c..bde6308 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -49,6 +49,7 @@ Require CSE. Require Allocation. Require Tunneling. Require Linearize. +Require CleanupLabels. Require Reload. Require Stacking. Require Asmgen. @@ -74,6 +75,8 @@ Require Tunnelingproof. Require Tunnelingtyping. Require Linearizeproof. Require Linearizetyping. +Require CleanupLabelsproof. +Require CleanupLabelstyping. Require Reloadproof. Require Reloadtyping. Require Stackingproof. @@ -142,6 +145,7 @@ Definition transf_rtl_fundef (f: RTL.fundef) : res Asm.fundef := @@@ Allocation.transf_fundef @@ Tunneling.tunnel_fundef @@@ Linearize.transf_fundef + @@ CleanupLabels.transf_fundef @@ print print_LTLin @@ Reload.transf_fundef @@@ Stacking.transf_fundef @@ -305,13 +309,17 @@ Proof. repeat rewrite transform_program_print_identity in *. subst. exploit transform_partial_program_identity; eauto. intro EQ. subst. - generalize Alloctyping.program_typing_preserved Tunnelingtyping.program_typing_preserved - Linearizetyping.program_typing_preserved Reloadtyping.program_typing_preserved + generalize Alloctyping.program_typing_preserved + Tunnelingtyping.program_typing_preserved + Linearizetyping.program_typing_preserved + CleanupLabelstyping.program_typing_preserved + Reloadtyping.program_typing_preserved Stackingtyping.program_typing_preserved; intros. eapply Asmgenproof.transf_program_correct; eauto 6. - eapply Stackingproof.transf_program_correct; eauto. + eapply Stackingproof.transf_program_correct; eauto 6. eapply Reloadproof.transf_program_correct; eauto. + eapply CleanupLabelsproof.transf_program_correct; eauto. eapply Linearizeproof.transf_program_correct; eauto. eapply Tunnelingproof.transf_program_correct; eauto. eapply Allocproof.transf_program_correct; eauto. |