diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-08-16 15:35:09 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-08-16 15:35:09 +0000 |
commit | 4b119d6f9f0e846edccaf5c08788ca1615b22526 (patch) | |
tree | 66cf55decd8d950d0bdc1050448aa3ee448ca13a /backend/Allocation.v | |
parent | 1fe28ba1ec3dd0657b121c4a911ee1cb046bab09 (diff) | |
download | compcert-4b119d6f9f0e846edccaf5c08788ca1615b22526.tar.gz compcert-4b119d6f9f0e846edccaf5c08788ca1615b22526.zip |
Cil2Csyntax: added goto and labels; added assignment between structs
Kildall: simplified the interface
Constprop, CSE, Allocation, Linearize: updated for the new Kildall
RTL, LTL: removed the well-formedness condition on the CFG,
it is no longer necessary with the new Kildall and it is problematic
for validated optimizations.
Maps: more efficient implementation of PTree.fold.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1124 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend/Allocation.v')
-rw-r--r-- | backend/Allocation.v | 16 |
1 files changed, 2 insertions, 14 deletions
diff --git a/backend/Allocation.v b/backend/Allocation.v index 2389a331..7d843e57 100644 --- a/backend/Allocation.v +++ b/backend/Allocation.v @@ -116,7 +116,7 @@ Module RegsetLat := LFSet(Regset). Module DS := Backward_Dataflow_Solver(RegsetLat)(NodeSetBackward). Definition analyze (f: RTL.function): option (PMap.t Regset.t) := - DS.fixpoint (successors f) f.(fn_nextpc) (transfer f) nil. + DS.fixpoint (successors f) (transfer f) nil. (** * Translation from RTL to LTL *) @@ -171,16 +171,6 @@ Definition transf_instr Lreturn (option_map assign optarg) end. -Lemma transf_body_wf: - forall (f: RTL.function) (live: PMap.t Regset.t) (assign: reg -> loc), - let tc := PTree.map (transf_instr f live assign) (RTL.fn_code f) in - forall (pc: node), Plt pc (RTL.fn_nextpc f) \/ tc!pc = None. -Proof. - intros. elim (RTL.fn_code_wf f pc); intro. - left. auto. right. unfold tc. rewrite PTree.gmap. - unfold option_map. rewrite H. auto. -Qed. - Definition transf_fun (f: RTL.function) (live: PMap.t Regset.t) (assign: reg -> loc) : LTL.function := LTL.mkfunction @@ -188,9 +178,7 @@ Definition transf_fun (f: RTL.function) (live: PMap.t Regset.t) (List.map assign (RTL.fn_params f)) (RTL.fn_stacksize f) (PTree.map (transf_instr f live assign) (RTL.fn_code f)) - (RTL.fn_entrypoint f) - (RTL.fn_nextpc f) - (transf_body_wf f live assign). + (RTL.fn_entrypoint f). (** The translation of a function performs liveness analysis, construction and coloring of the inference graph, and per-instruction |