diff options
Diffstat (limited to 'cil/src/ext/ssa.ml')
-rw-r--r-- | cil/src/ext/ssa.ml | 696 |
1 files changed, 0 insertions, 696 deletions
diff --git a/cil/src/ext/ssa.ml b/cil/src/ext/ssa.ml deleted file mode 100644 index 942c92b6..00000000 --- a/cil/src/ext/ssa.ml +++ /dev/null @@ -1,696 +0,0 @@ -module B=Bitmap -module E = Errormsg - -open Cil -open Pretty - -let debug = false - -(* Globalsread, Globalswritten should be closed under call graph *) - -module StringOrder = - struct - type t = string - let compare s1 s2 = - if s1 = s2 then 0 else - if s1 < s2 then -1 else 1 - end - -module StringSet = Set.Make (StringOrder) - -module IntOrder = - struct - type t = int - let compare i1 i2 = - if i1 = i2 then 0 else - if i1 < i2 then -1 else 1 - end - -module IntSet = Set.Make (IntOrder) - - -type cfgInfo = { - name: string; (* The function name *) - start : int; - size : int; - blocks: cfgBlock array; (** Dominating blocks must come first *) - successors: int list array; (* block indices *) - predecessors: int list array; - mutable nrRegs: int; - mutable regToVarinfo: varinfo array; (** Map register IDs to varinfo *) - } - -(** A block corresponds to a statement *) -and cfgBlock = { - bstmt: Cil.stmt; - - (* We abstract the statement as a list of def/use instructions *) - instrlist: instruction list; - mutable livevars: (reg * int) list; - (** For each variable ID that is live at the start of the block, the - * block whose definition reaches this point. If that block is the same - * as the current one, then the variable is a phi variable *) - mutable reachable: bool; - } - -and instruction = (reg list * reg list) - (* lhs variables, variables on rhs. *) - - -and reg = int - -type idomInfo = int array (* immediate dominator *) - -and dfInfo = (int list) array (* dominance frontier *) - -and oneSccInfo = { - nodes: int list; - headers: int list; - backEdges: (int*int) list; - } - -and sccInfo = oneSccInfo list - -(* Muchnick's Domin_Fast, 7.16 *) - -let compute_idom (flowgraph: cfgInfo): idomInfo = - let start = flowgraph.start in - let size = flowgraph.size in - let successors = flowgraph.successors in - let predecessors = flowgraph.predecessors in - let n0 = size in (* a new node (not in the flowgraph) *) - let idom = Array.make size (-1) in (* Make an array of immediate dominators *) - let nnodes = size + 1 in - let nodeSet = B.init nnodes (fun i -> true) in - - let ndfs = Array.create nnodes 0 in (* mapping from depth-first - * number to nodes. DForder - * starts at 1, with 0 used as - * an invalid entry *) - let parent = Array.create nnodes 0 in (* the parent in depth-first - * spanning tree *) - - (* A semidominator of w is the node v with the minimal DForder such - * that there is a path from v to w containing only nodes with the - * DForder larger than w. *) - let sdno = Array.create nnodes 0 in (* depth-first number of - * semidominator *) - - (* The set of nodes whose - * semidominator is ndfs(i) *) - let bucket = Array.init nnodes (fun _ -> B.cloneEmpty nodeSet) in - - (* The functions link and eval maintain a forest within the - * depth-first spanning tree. Ancestor is n0 is the node is a root in - * the forest. Label(v) is the node in the ancestor chain with the - * smallest depth-first number of its semidominator. Child and Size - * are used to keep the trees in the forest balanced *) - let ancestor = Array.create nnodes 0 in - let label = Array.create nnodes 0 in - let child = Array.create nnodes 0 in - let size = Array.create nnodes 0 in - - - let n = ref 0 in (* depth-first scan and numbering. - * Initialize data structures. *) - ancestor.(n0) <- n0; - label.(n0) <- n0; - let rec depthFirstSearchDom v = - incr n; - sdno.(v) <- !n; - ndfs.(!n) <- v; label.(v) <- v; - ancestor.(v) <- n0; (* All nodes are roots initially *) - child.(v) <- n0; size.(v) <- 1; - List.iter - (fun w -> - if sdno.(w) = 0 then begin - parent.(w) <- v; depthFirstSearchDom w - end) - successors.(v); - in - (* Determine the ancestor of v whose semidominator has the the minimal - * DFnumber. In the process, compress the paths in the forest. *) - let eval v = - let rec compress v = - if ancestor.(ancestor.(v)) <> n0 then - begin - compress ancestor.(v); - if sdno.(label.(ancestor.(v))) < sdno.(label.(v)) then - label.(v) <- label.(ancestor.(v)); - ancestor.(v) <- ancestor.(ancestor.(v)) - end - in - if ancestor.(v) = n0 then label.(v) - else begin - compress v; - if sdno.(label.(ancestor.(v))) >= sdno.(label.(v)) then - label.(v) - else label.(ancestor.(v)) - end - in - - let link v w = - let s = ref w in - while sdno.(label.(w)) < sdno.(label.(child.(!s))) do - if size.(!s) + size.(child.(child.(!s))) >= 2* size.(child.(!s)) then - (ancestor.(child.(!s)) <- !s; - child.(!s) <- child.(child.(!s))) - else - (size.(child.(!s)) <- size.(!s); - ancestor.(!s) <- child.(!s); s := child.(!s)); - done; - label.(!s) <- label.(w); - size.(v) <- size.(v) + size.(w); - if size.(v) < 2 * size.(w) then begin - let tmp = !s in - s := child.(v); - child.(v) <- tmp; - end; - while !s <> n0 do - ancestor.(!s) <- v; - s := child.(!s); - done; - in - (* Start now *) - depthFirstSearchDom start; - for i = !n downto 2 do - let w = ndfs.(i) in - List.iter (fun v -> - let u = eval v in - if sdno.(u) < sdno.(w) then sdno.(w) <- sdno.(u);) - predecessors.(w); - B.set bucket.(ndfs.(sdno.(w))) w true; - link parent.(w) w; - while not (B.empty bucket.(parent.(w))) do - let v = - match B.toList bucket.(parent.(w)) with - x :: _ -> x - | [] -> ignore(print_string "Error in dominfast");0 in - B.set bucket.(parent.(w)) v false; - let u = eval v in - idom.(v) <- if sdno.(u) < sdno.(v) then u else parent.(w); - done; - done; - - for i=2 to !n do - let w = ndfs.(i) in - if idom.(w) <> ndfs.(sdno.(w)) then begin - let newDom = idom.(idom.(w)) in - idom.(w) <- newDom; - end - done; - idom - - - - - -let dominance_frontier (flowgraph: cfgInfo) : dfInfo = - let idom = compute_idom flowgraph in - let size = flowgraph.size in - let children = Array.create size [] in - for i = 0 to size - 1 do - if (idom.(i) != -1) then children.(idom.(i)) <- i :: children.(idom.(i)); - done; - - let size = flowgraph.size in - let start = flowgraph.start in - let successors = flowgraph.successors in - - let df = Array.create size [] in - (* Compute the dominance frontier *) - - let bottom = Array.make size true in (* bottom of the dominator tree *) - for i = 0 to size - 1 do - if (i != start) && idom.(i) <> -1 then bottom.(idom.(i)) <- false; - done; - - let processed = Array.make size false in (* to record the nodes added to work_list *) - let workList = ref ([]) in (* to iterate in a bottom-up traversal of the dominator tree *) - for i = 0 to size - 1 do - if (bottom.(i)) then workList := i :: !workList; - done; - while (!workList != []) do - let x = List.hd !workList in - let update y = if idom.(y) <> x then df.(x) <- y::df.(x) in - (* compute local component *) - -(* We use whichPred instead of whichSucc because ultimately this info is - * needed by control dependence dag which is constructed from REVERSE - * dominance frontier *) - List.iter (fun succ -> update succ) successors.(x); - (* add on up component *) - List.iter (fun z -> List.iter (fun y -> update y) df.(z)) children.(x); - processed.(x) <- true; - workList := List.tl !workList; - if (x != start) then begin - let i = idom.(x) in - if i <> -1 && - (List.for_all (fun child -> processed.(child)) children.(i)) then workList := i :: !workList; - end; - done; - df - - -(* Computes for each register, the set of nodes that need a phi definition - * for the register *) - -let add_phi_functions_info (flowgraph: cfgInfo) : unit = - let df = dominance_frontier flowgraph in - let size = flowgraph.size in - let nrRegs = flowgraph.nrRegs in - - - let defs = Array.init size (fun i -> B.init nrRegs (fun j -> false)) in - for i = 0 to size-1 do - List.iter - (fun (lhs,rhs) -> - List.iter (fun (r: reg) -> B.set defs.(i) r true) lhs; - ) - flowgraph.blocks.(i).instrlist - done; - let iterCount = ref 0 in - let hasAlready = Array.create size 0 in - let work = Array.create size 0 in - let w = ref ([]) in - let dfPlus = Array.init nrRegs ( - fun i -> - let defIn = B.make size in - for j = 0 to size - 1 do - if B.get defs.(j) i then B.set defIn j true - done; - let res = ref [] in - incr iterCount; - B.iter (fun x -> work.(x) <- !iterCount; w := x :: !w;) defIn; - while (!w != []) do - let x = List.hd !w in - w := List.tl !w; - List.iter (fun y -> - if (hasAlready.(y) < !iterCount) then begin - res := y :: !res; - hasAlready.(y) <- !iterCount; - if (work.(y) < !iterCount) then begin - work.(y) <- !iterCount; - w := y :: !w; - end; - end; - ) df.(x) - done; - (* res := List.filter (fun blkId -> B.get liveIn.(blkId) i) !res; *) - !res - ) in - let result = Array.create size ([]) in - for i = 0 to nrRegs - 1 do - List.iter (fun node -> result.(node) <- i::result.(node);) dfPlus.(i) - done; -(* result contains for each node, the list of variables that need phi - * definition *) - for i = 0 to size-1 do - flowgraph.blocks.(i).livevars <- - List.map (fun r -> (r, i)) result.(i); - done - - - -(* add dominating definitions info *) - -let add_dom_def_info (f: cfgInfo): unit = - let blocks = f.blocks in - let start = f.start in - let size = f.size in - let nrRegs = f.nrRegs in - - let idom = compute_idom f in - let children = Array.create size [] in - for i = 0 to size - 1 do - if (idom.(i) != -1) then children.(idom.(i)) <- i :: children.(idom.(i)); - done; - - if debug then begin - ignore (E.log "Immediate dominators\n"); - for i = 0 to size - 1 do - ignore (E.log " block %d: idom=%d, children=%a\n" - i idom.(i) - (docList num) children.(i)); - done - end; - - (* For each variable, maintain a stack of blocks that define it. When you - * process a block, the top of the stack is the closest dominator that - * defines the variable *) - let s = Array.make nrRegs ([start]) in - - (* Search top-down in the idom tree *) - let rec search (x: int): unit = (* x is a graph node *) - (* Push the current block for the phi variables *) - List.iter - (fun ((r: reg), dr) -> - if x = dr then s.(r) <- x::s.(r)) - blocks.(x).livevars; - - (* Clear livevars *) - blocks.(x).livevars <- []; - - (* Compute livevars *) - for i = 0 to nrRegs-1 do - match s.(i) with - | [] -> assert false - | fst :: _ -> - blocks.(x).livevars <- (i, fst) :: blocks.(x).livevars - done; - - - (* Update s for the children *) - List.iter - (fun (lhs,rhs) -> - List.iter (fun (lreg: reg) -> s.(lreg) <- x::s.(lreg) ) lhs; - ) - blocks.(x).instrlist; - - - (* Go and do the children *) - List.iter search children.(x); - - (* Then we pop x, whenever it is on top of a stack *) - Array.iteri - (fun i istack -> - let rec dropX = function - [] -> [] - | x' :: rest when x = x' -> dropX rest - | l -> l - in - s.(i) <- dropX istack) - s; - in - search(start) - - - -let prune_cfg (f: cfgInfo): cfgInfo = - let size = f.size in - if size = 0 then f else - let reachable = Array.make size false in - let worklist = ref([f.start]) in - while (!worklist != []) do - let h = List.hd !worklist in - worklist := List.tl !worklist; - reachable.(h) <- true; - List.iter (fun s -> if (reachable.(s) = false) then worklist := s::!worklist; - ) f.successors.(h); - done; -(* - let dummyblock = { bstmt = mkEmptyStmt (); - instrlist = []; - livevars = [] } - in -*) - let successors = Array.init size (fun i -> List.filter (fun s -> reachable.(s)) f.successors.(i)) in - let predecessors = Array.init size (fun i -> List.filter (fun s -> reachable.(s)) f.predecessors.(i)) in - Array.iteri (fun i b -> b.reachable <- reachable.(i)) f.blocks; - let result: cfgInfo = - { name = f.name; - start = f.start; - size = f.size; - successors = successors; - predecessors = predecessors; - blocks = f.blocks; - nrRegs = f.nrRegs; - regToVarinfo = f.regToVarinfo; - } - in - result - - -let add_ssa_info (f: cfgInfo): unit = - let f = prune_cfg f in - let d_reg () (r: int) = - dprintf "%s(%d)" f.regToVarinfo.(r).vname r - in - if debug then begin - ignore (E.log "Doing SSA for %s. Initial data:\n" f.name); - Array.iteri (fun i b -> - ignore (E.log " block %d:\n succs=@[%a@]\n preds=@[%a@]\n instr=@[%a@]\n" - i - (docList num) f.successors.(i) - (docList num) f.predecessors.(i) - (docList ~sep:line (fun (lhs, rhs) -> - dprintf "%a := @[%a@]" - (docList (d_reg ())) lhs (docList (d_reg ())) rhs)) - b.instrlist)) - f.blocks; - end; - - add_phi_functions_info f; - add_dom_def_info f; - - if debug then begin - ignore (E.log "After SSA\n"); - Array.iter (fun b -> - ignore (E.log " block %d livevars: @[%a@]\n" - b.bstmt.sid - (docList (fun (i, fst) -> - dprintf "%a def at %d" d_reg i fst)) - b.livevars)) - f.blocks; - end - - -let set2list s = - let result = ref([]) in - IntSet.iter (fun element -> result := element::!result) s; - !result - - - - -let preorderDAG (nrNodes: int) (successors: (int list) array): int list = - let processed = Array.make nrNodes false in - let revResult = ref ([]) in - let predecessorsSet = Array.make nrNodes (IntSet.empty) in - for i = 0 to nrNodes -1 do - List.iter (fun s -> predecessorsSet.(s) <- IntSet.add i predecessorsSet.(s)) successors.(i); - done; - let predecessors = Array.init nrNodes (fun i -> set2list predecessorsSet.(i)) in - let workList = ref([]) in - for i = 0 to nrNodes - 1 do - if (predecessors.(i) = []) then workList := i::!workList; - done; - while (!workList != []) do - let x = List.hd !workList in - workList := List.tl !workList; - revResult := x::!revResult; - processed.(x) <- true; - List.iter (fun s -> - if (List.for_all (fun p -> processed.(p)) predecessors.(s)) then - workList := s::!workList; - ) successors.(x); - done; - List.rev !revResult - - -(* Muchnick Fig 7.12 *) -(* takes an SCC description as an input and returns prepares the appropriate SCC *) -let preorder (nrNodes: int) (successors: (int list) array) (r: int): oneSccInfo = - if debug then begin - ignore (E.log "Inside preorder \n"); - for i = 0 to nrNodes - 1 do - ignore (E.log "succ(%d) = %a" i (docList (fun i -> num i)) successors.(i)); - done; - end; - let i = ref(0) in - let j = ref(0) in - let pre = Array.make nrNodes (-1) in - let post = Array.make nrNodes (-1) in - let visit = Array.make nrNodes (false) in - let backEdges = ref ([]) in - let headers = ref(IntSet.empty) in - let rec depth_first_search_pp (x:int) = - visit.(x) <- true; - pre.(x) <- !j; - incr j; - List.iter (fun (y:int) -> - if (not visit.(y)) then - (depth_first_search_pp y) - else - if (post.(y) = -1) then begin - backEdges := (x,y)::!backEdges; - headers := IntSet.add y !headers; - end; - ) successors.(x); - post.(x) <- !i; - incr i; - in - depth_first_search_pp r; - let nodes = Array.make nrNodes (-1) in - for y = 0 to nrNodes - 1 do - if (pre.(y) != -1) then nodes.(pre.(y)) <- y; - done; - let nodeList = List.filter (fun i -> (i != -1)) (Array.to_list nodes) in - let result = { headers = set2list !headers; backEdges = !backEdges; nodes = nodeList; } in - result - - -exception Finished - - -let strong_components (f: cfgInfo) (debug: bool) = - let size = f.size in - let parent = Array.make size (-1) in - let color = Array.make size (-1) in - let finish = Array.make size (-1) in - let root = Array.make size (-1) in - -(* returns a list of SCC. Each SCC is a tuple of SCC root and SCC nodes *) - let dfs (successors: (int list) array) (order: int array) = - let time = ref(-1) in - let rec dfs_visit u = - color.(u) <- 1; - incr time; - (* d.(u) <- time; *) - List.iter (fun v -> - if color.(v) = 0 then (parent.(v) <- u; dfs_visit v) - ) successors.(u); - color.(u) <- 2; - incr time; - finish.(u) <- !time - in - for u = 0 to size - 1 do - color.(u) <- 0; (* white = 0, gray = 1, black = 2 *) - parent.(u) <- -1; (* nil = -1 *) - root.(u) <- 0; (* Is u a root? *) - done; - time := 0; - Array.iter (fun u -> - if (color.(u) = 0) then begin - root.(u) <- 1; - dfs_visit u; - end; - ) order; - in - - let simpleOrder = Array.init size (fun i -> i) in - dfs f.successors simpleOrder; - Array.sort (fun i j -> if (finish.(i) > finish.(j)) then -1 else 1) simpleOrder; - - dfs f.predecessors simpleOrder; -(* SCCs have been computed. (The trees represented by non-null parent edges - * represent the SCCS. We call the black nodes as the roots). Now put the - * result in the ouput format *) - let allScc = ref([]) in - for u = 0 to size - 1 do - if root.(u) = 1 then begin - let sccNodes = ref(IntSet.empty) in - let workList = ref([u]) in - while (!workList != []) do - let h=List.hd !workList in - workList := List.tl !workList; - sccNodes := IntSet.add h !sccNodes; - List.iter (fun s -> if parent.(s)=h then workList := s::!workList;) f.predecessors.(h); - done; - allScc := (u,!sccNodes)::!allScc; - if (debug) then begin - ignore (E.log "Got an SCC with root %d and nodes %a" u (docList num) (set2list !sccNodes)); - end; - end; - done; - !allScc - - -let stronglyConnectedComponents (f: cfgInfo) (debug: bool): sccInfo = - let size = f.size in - if (debug) then begin - ignore (E.log "size = %d\n" size); - for i = 0 to size - 1 do - ignore (E.log "Successors(%d): %a\n" i (docList (fun n -> num n)) f.successors.(i)); - done; - end; - - let allScc = strong_components f debug in - let all_sccArray = Array.of_list allScc in - - if (debug) then begin - ignore (E.log "Computed SCCs\n"); - for i = 0 to (Array.length all_sccArray) - 1 do - ignore(E.log "SCC #%d: " i); - let (_,sccNodes) = all_sccArray.(i) in - IntSet.iter (fun i -> ignore(E.log "%d, " i)) sccNodes; - ignore(E.log "\n"); - done; - end; - - - (* Construct sccId: Node -> Scc Id *) - let sccId = Array.make size (-1) in - Array.iteri (fun i (r,sccNodes) -> - IntSet.iter (fun n -> sccId.(n) <- i) sccNodes; - ) all_sccArray; - - if (debug) then begin - ignore (E.log "\nComputed SCC IDs: "); - for i = 0 to size - 1 do - ignore (E.log "SCCID(%d) = %d " i sccId.(i)); - done; - end; - - - (* Construct sccCFG *) - let nrScc = Array.length all_sccArray in - let successors = Array.make nrScc [] in - for x = 0 to nrScc - 1 do - successors.(x) <- - let s = ref(IntSet.empty) in - IntSet.iter (fun y -> - List.iter (fun z -> - let sy = sccId.(y) in - let sz = sccId.(z) in - if (not(sy = sz)) then begin - s := IntSet.add sz !s; - end - ) f.successors.(y) - ) (snd all_sccArray.(x)); - set2list !s - done; - - if (debug) then begin - ignore (E.log "\nComputed SCC CFG, which should be a DAG:"); - ignore (E.log "nrSccs = %d " nrScc); - for i = 0 to nrScc - 1 do - ignore (E.log "successors(%d) = [%a] " i (docList (fun j -> num j)) successors.(i)); - done; - end; - - - (* Order SCCs. The graph is a DAG here *) - let sccorder = preorderDAG nrScc successors in - - if (debug) then begin - ignore (E.log "\nComputed SCC Preorder: "); - ignore (E.log "Nodes in Preorder = [%a]" (docList (fun i -> num i)) sccorder); - end; - - (* Order nodes of each SCC. The graph is a SCC here.*) - let scclist = List.map (fun i -> - let successors = Array.create size [] in - for j = 0 to size - 1 do - successors.(j) <- List.filter (fun x -> IntSet.mem x (snd all_sccArray.(i))) f.successors.(j); - done; - preorder f.size successors (fst all_sccArray.(i)) - ) sccorder in - if (debug) then begin - ignore (E.log "Computed Preorder for Nodes of each SCC\n"); - List.iter (fun scc -> - ignore (E.log "BackEdges = %a \n" - (docList (fun (src,dest) -> dprintf "(%d,%d)" src dest)) - scc.backEdges);) - scclist; - end; - scclist - - - - - - - - - |