summaryrefslogtreecommitdiff
path: root/cil/src/ext/ssa.ml
blob: 942c92b6489920c1eadab72f22352a765546915d (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
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