From 4b119d6f9f0e846edccaf5c08788ca1615b22526 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 16 Aug 2009 15:35:09 +0000 Subject: 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 --- backend/CSE.v | 20 ++------------------ 1 file changed, 2 insertions(+), 18 deletions(-) (limited to 'backend/CSE.v') 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. -- cgit