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 /powerpc/Constprop.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 'powerpc/Constprop.v')
-rw-r--r-- | powerpc/Constprop.v | 19 |
1 files changed, 2 insertions, 17 deletions
diff --git a/powerpc/Constprop.v b/powerpc/Constprop.v index 76ea153c..109125c3 100644 --- a/powerpc/Constprop.v +++ b/powerpc/Constprop.v @@ -674,7 +674,7 @@ Definition transfer (f: function) (pc: node) (before: D.t) := Module DS := Dataflow_Solver(D)(NodeSetForward). Definition analyze (f: RTL.function): PMap.t D.t := - match DS.fixpoint (successors f) f.(fn_nextpc) (transfer f) + match DS.fixpoint (successors f) (transfer f) ((f.(fn_entrypoint), D.top) :: nil) with | None => PMap.init D.top | Some res => res @@ -1062,19 +1062,6 @@ Definition transf_instr (approx: D.t) (instr: instruction) := Definition transf_code (approxs: PMap.t D.t) (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 @@ -1082,9 +1069,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 (fd: fundef) : fundef := AST.transf_fundef transf_function fd. |