diff options
Diffstat (limited to 'cil/src/ext/dominators.ml')
-rwxr-xr-x | cil/src/ext/dominators.ml | 241 |
1 files changed, 241 insertions, 0 deletions
diff --git a/cil/src/ext/dominators.ml b/cil/src/ext/dominators.ml new file mode 100755 index 00000000..d838d23f --- /dev/null +++ b/cil/src/ext/dominators.ml @@ -0,0 +1,241 @@ +(* + * + * Copyright (c) 2001-2002, + * George C. Necula <necula@cs.berkeley.edu> + * Scott McPeak <smcpeak@cs.berkeley.edu> + * Wes Weimer <weimer@cs.berkeley.edu> + * All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are + * met: + * + * 1. Redistributions of source code must retain the above copyright + * notice, this list of conditions and the following disclaimer. + * + * 2. Redistributions in binary form must reproduce the above copyright + * notice, this list of conditions and the following disclaimer in the + * documentation and/or other materials provided with the distribution. + * + * 3. The names of the contributors may not be used to endorse or promote + * products derived from this software without specific prior written + * permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS + * IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED + * TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A + * PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER + * OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, + * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, + * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR + * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF + * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING + * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS + * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + * + *) + +(** Compute dominator information for the statements in a function *) +open Cil +open Pretty +module E = Errormsg +module H = Hashtbl +module U = Util +module IH = Inthash + +module DF = Dataflow + +let debug = false + +(* For each statement we maintain a set of statements that dominate it *) +module BS = Set.Make(struct + type t = Cil.stmt + let compare v1 v2 = Pervasives.compare v1.sid v2.sid + end) + + + + +(** Customization module for dominators *) +module DT = struct + let name = "dom" + + let debug = ref debug + + type t = BS.t + + (** For each statement in a function we keep the set of dominator blocks. + * Indexed by statement id *) + let stmtStartData: t IH.t = IH.create 17 + + let copy (d: t) = d + + let pretty () (d: t) = + dprintf "{%a}" + (docList (fun s -> dprintf "%d" s.sid)) + (BS.elements d) + + let computeFirstPredecessor (s: stmt) (d: BS.t) : BS.t = + (* Make sure we add this block to the set *) + BS.add s d + + let combinePredecessors (s: stmt) ~(old: BS.t) (d: BS.t) : BS.t option = + (* First, add this block to the data from the predecessor *) + let d' = BS.add s d in + if BS.subset old d' then + None + else + Some (BS.inter old d') + + let doInstr (i: instr) (d: t) = DF.Default + + let doStmt (s: stmt) (d: t) = DF.SDefault + + let doGuard condition _ = DF.GDefault + + + let filterStmt _ = true +end + + + +module Dom = DF.ForwardsDataFlow(DT) + +let getStmtDominators (data: BS.t IH.t) (s: stmt) : BS.t = + try IH.find data s.sid + with Not_found -> BS.empty (* Not reachable *) + + +let getIdom (idomInfo: stmt option IH.t) (s: stmt) = + try IH.find idomInfo s.sid + with Not_found -> + E.s (E.bug "Immediate dominator information not set for statement %d" + s.sid) + +(** Check whether one block dominates another. This assumes that the "idom" + * field has been computed. *) +let rec dominates (idomInfo: stmt option IH.t) (s1: stmt) (s2: stmt) = + s1 == s2 || + (let s2idom = getIdom idomInfo s2 in + match s2idom with + None -> false + | Some s2idom -> dominates idomInfo s1 s2idom) + + + + +let computeIDom (f: fundec) : stmt option IH.t = + (* We must prepare the CFG info first *) + prepareCFG f; + computeCFGInfo f false; + + IH.clear DT.stmtStartData; + let idomData: stmt option IH.t = IH.create 13 in + + let _ = + match f.sbody.bstmts with + [] -> () (* function has no body *) + | start :: _ -> begin + (* We start with only the start block *) + IH.add DT.stmtStartData start.sid (BS.singleton start); + + Dom.compute [start]; + + (* Dump the dominators information *) + if debug then + List.iter + (fun s -> + let sdoms = getStmtDominators DT.stmtStartData s in + if not (BS.mem s sdoms) then begin + (* It can be that the block is not reachable *) + if s.preds <> [] then + E.s (E.bug "Statement %d is not in its list of dominators" + s.sid); + end; + ignore (E.log "Dominators for %d: %a\n" s.sid + DT.pretty (BS.remove s sdoms))) + f.sallstmts; + + (* Now fill the immediate dominators for all nodes *) + let rec fillOneIdom (s: stmt) = + try + ignore (IH.find idomData s.sid) + (* Already set *) + with Not_found -> begin + (* Get the dominators *) + let sdoms = getStmtDominators DT.stmtStartData s in + (* Fill the idom for the dominators first *) + let idom = + BS.fold + (fun d (sofar: stmt option) -> + if d.sid = s.sid then + sofar (* Ignore the block itself *) + else begin + (* fill the idom information recursively *) + fillOneIdom d; + match sofar with + None -> Some d + | Some sofar' -> + (* See if d is dominated by sofar. We know that the + * idom information has been computed for both sofar + * and for d*) + if dominates idomData sofar' d then + Some d + else + sofar + end) + sdoms + None + in + IH.replace idomData s.sid idom + end + in + (* Scan all blocks and compute the idom *) + List.iter fillOneIdom f.sallstmts + end + in + idomData + + + +(** Compute the start of the natural loops. For each start, keep a list of + * origin of a back edge. The loop consists of the loop start and all + * predecessors of the origins of back edges, up to and including the loop + * start *) +let findNaturalLoops (f: fundec) + (idomData: stmt option IH.t) : (stmt * stmt list) list = + let loops = + List.fold_left + (fun acc b -> + (* Iterate over all successors, and see if they are among the + * dominators for this block *) + List.fold_left + (fun acc s -> + if dominates idomData s b then + (* s is the start of a natural loop *) + let rec addNaturalLoop = function + [] -> [(s, [b])] + | (s', backs) :: rest when s'.sid = s.sid -> + (s', b :: backs) :: rest + | l :: rest -> l :: addNaturalLoop rest + in + addNaturalLoop acc + else + acc) + acc + b.succs) + [] + f.sallstmts + in + + if debug then + ignore (E.log "Natural loops:\n%a\n" + (docList ~sep:line + (fun (s, backs) -> + dprintf " Start: %d, backs:%a" + s.sid + (docList (fun b -> num b.sid)) + backs)) + loops); + + loops |