diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-21 22:24:31 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-21 22:24:31 +0200 |
| commit | 1bd4d678fb719a6a52ade232eb2b36a6e621677a (patch) | |
| tree | bfd0c171a8184fd3395b6a0fced0b8ac45d42f69 /driver | |
| parent | 9cc12b684ee6833971c9549aa76cc683ba931090 (diff) | |
| download | compcert-kvx-1bd4d678fb719a6a52ade232eb2b36a6e621677a.tar.gz compcert-kvx-1bd4d678fb719a6a52ade232eb2b36a6e621677a.zip | |
Require autogen
Diffstat (limited to 'driver')
| -rw-r--r-- | driver/Compiler.vexpand | 38 |
1 files changed, 4 insertions, 34 deletions
diff --git a/driver/Compiler.vexpand b/driver/Compiler.vexpand index 4c7c963a..d0ba33d3 100644 --- a/driver/Compiler.vexpand +++ b/driver/Compiler.vexpand @@ -35,22 +35,7 @@ Require Cshmgen. Require Cminorgen. Require Selection. Require RTLgen. -Require Tailcall. -Require Inlining. -Require Profiling. -Require ProfilingExploit. -Require FirstNop. -Require Renumber. -Require Duplicate. -Require Constprop. -Require LICM. -Require CSE. -Require ForwardMoves. -Require CSE2. -Require CSE3. -Require Deadcode. -Require Unusedglob. -Require Allnontrap. +EXPAND_RTL_REQUIRE Require Allocation. Require Tunneling. Require Linearize. @@ -65,22 +50,7 @@ Require Cshmgenproof. Require Cminorgenproof. Require Selectionproof. Require RTLgenproof. -Require Tailcallproof. -Require Inliningproof. -Require Profilingproof. -Require ProfilingExploitproof. -Require FirstNopproof. -Require Renumberproof. -Require Duplicateproof. -Require Constpropproof. -Require LICMproof. -Require CSEproof. -Require ForwardMovesproof. -Require CSE2proof. -Require CSE3proof. -Require Deadcodeproof. -Require Unusedglobproof. -Require Allnontrapproof. +EXPAND_RTL_REQUIRE_PROOF Require Allocproof. Require Tunnelingproof. Require Linearizeproof. @@ -138,7 +108,7 @@ Definition partial_if {A: Type} Definition transf_rtl_program (f: RTL.program) : res Asm.program := OK f @@ print (print_RTL 0) -EXPAND_TRANSF_PROGRAM +EXPAND_RTL_TRANSF_PROGRAM @@@ time "Register allocation" Allocation.transf_program @@ print print_LTL @@ time "Branch tunneling" Tunneling.tunnel_program @@ -308,7 +278,7 @@ Proof. set (p13quater := total_if optim_forward_moves ForwardMoves.transf_program p13ter) in *. destruct (partial_if optim_redundancy Deadcode.transf_program p13quater) as [p14|e] eqn:P14; simpl in T; try discriminate. set (p14bis := total_if all_loads_nontrap Allnontrap.transf_program p14) in *. - destruct (Unusedglob.transform_program p14bis) as [p15|e] eqn:P15; simpl in T; try discriminate. + destruct (Unusedglob.transf_program p14bis) as [p15|e] eqn:P15; simpl in T; try discriminate. destruct (Allocation.transf_program p15) as [p16|e] eqn:P16; simpl in T; try discriminate. set (p17 := Tunneling.tunnel_program p16) in *. destruct (Linearize.transf_program p17) as [p18|e] eqn:P18; simpl in T; try discriminate. |