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/CSE.v | |
| parent | 1fe28ba1ec3dd0657b121c4a911ee1cb046bab09 (diff) | |
| download | compcert-kvx-4b119d6f9f0e846edccaf5c08788ca1615b22526.tar.gz compcert-kvx-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/CSE.v')
| -rw-r--r-- | backend/CSE.v | 20 |
1 files changed, 2 insertions, 18 deletions
diff --git a/backend/CSE.v b/backend/CSE.v index cad35034..ff8d41aa 100644 --- a/backend/CSE.v +++ b/backend/CSE.v @@ -364,8 +364,7 @@ Definition transfer (f: function) (pc: node) (before: numbering) := and effectively deactivates the CSE optimization. *) Definition analyze (f: RTL.function): PMap.t numbering := - match Solver.fixpoint (successors f) f.(fn_nextpc) - (transfer f) f.(fn_entrypoint) with + match Solver.fixpoint (successors f) (transfer f) f.(fn_entrypoint) with | None => PMap.init empty_numbering | Some res => res end. @@ -410,19 +409,6 @@ Definition transf_instr (n: numbering) (instr: instruction) := Definition transf_code (approxs: PMap.t numbering) (instrs: code) : code := PTree.map (fun pc instr => transf_instr approxs!!pc instr) instrs. -Lemma transf_code_wf: - forall f approxs, - (forall pc, Plt pc f.(fn_nextpc) \/ f.(fn_code)!pc = None) -> - (forall pc, Plt pc f.(fn_nextpc) - \/ (transf_code approxs f.(fn_code))!pc = None). -Proof. - intros. - elim (H pc); intro. - left; auto. - right. unfold transf_code. rewrite PTree.gmap. - unfold option_map; rewrite H0. reflexivity. -Qed. - Definition transf_function (f: function) : function := let approxs := analyze f in mkfunction @@ -430,9 +416,7 @@ Definition transf_function (f: function) : function := f.(fn_params) f.(fn_stacksize) (transf_code approxs f.(fn_code)) - f.(fn_entrypoint) - f.(fn_nextpc) - (transf_code_wf f approxs f.(fn_code_wf)). + f.(fn_entrypoint). Definition transf_fundef (f: fundef) : fundef := AST.transf_fundef transf_function f. |