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 --- extraction/Kildall.ml.patch | 47 ++++++++++++++------------------------------- 1 file changed, 14 insertions(+), 33 deletions(-) (limited to 'extraction') diff --git a/extraction/Kildall.ml.patch b/extraction/Kildall.ml.patch index b7e5b0b..6c94854 100644 --- a/extraction/Kildall.ml.patch +++ b/extraction/Kildall.ml.patch @@ -1,40 +1,21 @@ -*** kildall.ml.orig 2009-06-03 11:32:52.297641897 +0200 ---- kildall.ml 2009-06-03 11:34:48.481516509 +0200 +*** kildall.ml.orig 2009-08-16 15:45:21.000000000 +0200 +--- kildall.ml 2009-08-16 15:45:27.000000000 +0200 *************** -*** 151,158 **** - -> (positive, LAT.t) prod list -> LAT.t PMap.t option **) +*** 252,259 **** - let fixpoint successors topnode transf entrypoints = -! DS.fixpoint (fun s -> PMap.get s (make_predecessors successors topnode)) -! topnode transf entrypoints - end - - module type ORDERED_TYPE_WITH_TOP = ---- 151,158 ---- - -> (positive, LAT.t) prod list -> LAT.t PMap.t option **) + (** val basic_block_map : positive list PTree.t -> positive -> bbmap **) - let fixpoint successors topnode transf entrypoints = -! let pred = make_predecessors successors topnode in -! DS.fixpoint (fun s -> PMap.get s pred) topnode transf entrypoints - end - - module type ORDERED_TYPE_WITH_TOP = -*************** -*** 248,255 **** - (** val basic_block_map : - (positive -> positive list) -> positive -> positive -> bbmap **) - -! let basic_block_map successors topnode entrypoint x = -! is_basic_block_head entrypoint (make_predecessors successors topnode) x - - (** val basic_block_list : positive -> bbmap -> positive list **) +! let basic_block_map successors entrypoint x = +! is_basic_block_head entrypoint (make_predecessors successors) x ---- 248,255 ---- - (** val basic_block_map : - (positive -> positive list) -> positive -> positive -> bbmap **) + (** val basic_block_list : + positive list PTree.t -> bbmap -> positive list **) +--- 252,259 ---- -! let basic_block_map successors topnode entrypoint = -! is_basic_block_head entrypoint (make_predecessors successors topnode) + (** val basic_block_map : positive list PTree.t -> positive -> bbmap **) - (** val basic_block_list : positive -> bbmap -> positive list **) +! let basic_block_map successors entrypoint = +! is_basic_block_head entrypoint (make_predecessors successors) + (** val basic_block_list : + positive list PTree.t -> bbmap -> positive list **) -- cgit v1.2.3