diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2007-10-27 10:23:16 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2007-10-27 10:23:16 +0000 |
commit | e882493e2c4b91024b42f0603ca6869e95695e85 (patch) | |
tree | 1d90dda6b56b541310d8b8703152fdcd49e8a7fa /caml | |
parent | 7f6ac3209e7fb7d822780c7e990fb604b11a6409 (diff) | |
download | compcert-e882493e2c4b91024b42f0603ca6869e95695e85.tar.gz compcert-e882493e2c4b91024b42f0603ca6869e95695e85.zip |
Linearize: utilisation d'une heuristique externe d'enumeration des noeuds du CFG
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@437 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'caml')
-rw-r--r-- | caml/Linearizeaux.ml | 83 |
1 files changed, 83 insertions, 0 deletions
diff --git a/caml/Linearizeaux.ml b/caml/Linearizeaux.ml new file mode 100644 index 00000000..8a4297f4 --- /dev/null +++ b/caml/Linearizeaux.ml @@ -0,0 +1,83 @@ +open BinPos +open Coqlib +open Datatypes +open LTL +open Lattice +open CList +open Maps +open Camlcoq + +(* Trivial enumeration, in decreasing order of PC *) + +(*** +let enumerate_aux f reach = + positive_rec + Coq_nil + (fun pc nodes -> + if PMap.get pc reach + then Coq_cons (pc, nodes) + else nodes) + f.fn_nextpc +***) + +(* More clever enumeration that flattens basic blocks *) + +let rec int_of_pos = function + | Coq_xI p -> (int_of_pos p lsl 1) + 1 + | Coq_xO p -> int_of_pos p lsl 1 + | Coq_xH -> 1 + +(* Count the reachable predecessors for each node *) + +let reachable_predecessors f reach = + let count = Array.make (int_of_pos f.fn_nextpc) 0 in + let increment pc = + let i = int_of_pos pc in + count.(i) <- count.(i) + 1 in + positive_rec + () + (fun pc _ -> + if PMap.get pc reach then coqlist_iter increment (successors f pc)) + f.fn_nextpc; + count + +(* Recognize instructions with only one successor *) + +let single_successor f pc = + match PTree.get pc f.fn_code with + | Some i -> + (match i with + | Lnop s -> Some s + | Lop (op, args, res, s) -> Some s + | Lload (chunk, addr, args, dst, s) -> Some s + | Lstore (chunk, addr, args, src, s) -> Some s + | Lcall (sig0, ros, args, res, s) -> Some s + | Ltailcall (sig0, ros, args) -> None + | Lalloc (arg, res, s) -> Some s + | Lcond (cond, args, ifso, ifnot) -> None + | Lreturn optarg -> None) + | None -> None + +(* Build the enumeration *) + +let enumerate_aux f reach = + let preds = reachable_predecessors f reach in + let enum = ref Coq_nil in + let emitted = Array.make (int_of_pos f.fn_nextpc) false in + let rec emit_basic_block pc = + enum := Coq_cons(pc, !enum); + emitted.(int_of_pos pc) <- true; + match single_successor f pc with + | None -> () + | Some pc' -> + let npc' = int_of_pos pc' in + if preds.(npc') <= 1 && not emitted.(npc') then emit_basic_block pc' in + let rec emit_all pc = + if pc <> Coq_xH then begin + let pc = coq_Ppred pc in + if not emitted.(int_of_pos pc) && PMap.get pc reach + then emit_basic_block pc; + emit_all pc + end in + emit_all f.fn_nextpc; + CList.rev !enum |