source: Deliverables/D2.2/8051/src/utilities/graphUtilities.ml @ 1584

Last change on this file since 1584 was 1584, checked in by tranquil, 8 years ago
  • new form of translation written in graphUtilites (mainly as a test before implementation in Matita)
  • rewritten multiplication in RTLasbToRTL
File size: 7.4 KB
Line 
1module type GraphType = sig
2
3  type node
4  type statement
5
6  module NodeMap : Map.S with type key = node
7  module NodeSet : Set.S with type elt = node
8
9  type t = statement NodeMap.t
10
11  val successors : statement -> node list
12  val skip : node -> statement
13  val fill_succs : statement -> node list -> statement
14
15end
16
17module Util (G : GraphType) = struct
18
19  open G
20
21  let compute_predecessor_lists (graph : G.t) : G.node list G.NodeMap.t =
22    let add_to_preds pred map lbl =
23      let preds =
24        try
25          pred :: NodeMap.find lbl map
26        with
27          | Not_found -> [pred] in
28      NodeMap.add lbl preds map in
29    let add_predecessors lbl stmt map =
30    (* make sure the domain of the map will be equal to dom graph, adding *)
31    (* empty sets if need be *)
32      let map = if NodeMap.mem lbl map then map else
33          NodeMap.add lbl [] map in
34      List.fold_left (add_to_preds lbl) map (successors stmt) in
35    NodeMap.fold add_predecessors graph NodeMap.empty
36
37  let dfs_fold
38      (f : node -> statement -> 'a -> 'a)
39      (g : t)
40      (entry : node)
41      (init : 'a)
42      : 'a =
43  if not (NodeMap.mem entry g) then
44    invalid_arg "dfs_fold: entry is not in graph"
45  else
46    let rec process done_set = function
47      | [] -> init
48      | next :: worklist when NodeSet.mem next done_set ->
49        process done_set worklist
50      | next :: worklist ->
51        let stmt = NodeMap.find next g in
52        let succs = successors stmt in
53        f next stmt (process (NodeSet.add next done_set) (succs @ worklist)) in
54    process NodeSet.empty [entry]
55
56  let dfs_iter
57    (f : node -> statement -> unit)
58    (g : t)
59    (entry : node)
60    : unit =
61  if not (NodeMap.mem entry g) then
62    invalid_arg "dfs_iter: entry is not in graph"
63  else
64  let rec process done_set = function
65    | [] -> ();
66    | next :: worklist when NodeSet.mem next done_set ->
67      process done_set worklist
68    | next :: worklist ->
69      let stmt = NodeMap.find next g in
70      let succs = successors stmt in
71      f next stmt;
72      process (NodeSet.add next done_set) (succs @ worklist) in
73  process NodeSet.empty [entry]
74
75  let dead_code_elim
76      (g : t)
77      (entry : node)
78      : t =
79    let add lbl _ = NodeSet.add lbl in
80    let reachable = dfs_fold add g entry NodeSet.empty in
81    let is_reachable x _ = NodeSet.mem x reachable in
82    NodeMap.filter is_reachable g
83
84  let rec put_rev freshl stmts src dests graph =
85    match stmts, dests with
86      | [], [next] -> (src, NodeMap.add src (skip next) graph)
87      | [last], _ ->
88        (src, NodeMap.add src (fill_succs last dests) graph)
89      | last :: stmts, _ ->
90        let new_l = freshl () in
91        let graph = NodeMap.add new_l (fill_succs last dests) graph in
92        (new_l, snd (put_rev freshl stmts src [new_l] graph))
93      | _ ->
94        invalid_arg "successors of statement and translation do not match"
95
96  let replace freshl lbl stmts succs g =
97    let succs = match succs with
98      | Some x -> x
99      | None -> successors (NodeMap.find lbl g) in
100
101    snd (put_rev freshl (List.rev stmts) lbl succs g)
102
103  let replace'
104      (freshl : unit -> node)
105      (freshr : 'u -> 't -> 'u * 'r)
106      (lbl : node)
107      (stmts : (statement, 'r, 't) BList.t)
108      (succs : node list option)
109      (def : 'u)
110      (g : t)
111      : 'u * t =
112    let succs = match succs with
113      | Some x -> x
114      | None -> successors (NodeMap.find lbl g) in
115    let (def, l) = BList.compile freshr def stmts in
116    (def, snd (put_rev freshl l lbl succs g))
117
118  let insert freshl lbl stmts g =
119    let stmt = NodeMap.find lbl g in
120    let succs = successors (NodeMap.find lbl g) in
121    put_rev freshl (stmt :: List.rev stmts) lbl succs g
122
123  let insert' freshl freshr lbl stmts def g =
124    let stmt = NodeMap.find lbl g in
125    let succs = successors (NodeMap.find lbl g) in
126    let (def, l) = BList.compile freshr def stmts in
127    let (lbl, g) = put_rev freshl (stmt :: l) lbl succs g in
128    (def, lbl, g)
129
130end
131
132module Trans (Src : GraphType) (Trg : GraphType with type node = Src.node) =
133struct
134  type node = Src.node
135
136  (* keeping this general branching translation just in case *)
137  let translate_general
138      (fresh : unit -> Trg.node)
139      (f : 'a -> node -> Src.statement ->
140       'a * Trg.statement list * Trg.statement list list * node list option)
141      (info : 'a)
142      (g : Src.t) : 'a * Trg.t =
143
144    let rec put_rev stmts src dests graph =
145      match stmts, dests with
146        | [], [next] -> Trg.NodeMap.add src (Trg.skip next) graph
147        | [last], _ -> Trg.NodeMap.add src (Trg.fill_succs last dests) graph
148        | last :: stmts, _ ->
149          let new_l = fresh () in
150          let graph = Trg.NodeMap.add new_l (Trg.fill_succs last dests) graph in
151          put_rev stmts src [new_l] graph
152        | _ ->
153          invalid_arg "successors of statement and translation do not match" in
154
155    let rec put_block stmts blocks src dests graph =
156      match stmts, blocks, dests with
157        | [], [b], ds ->
158          let rev_b = List.rev b in
159          put_rev rev_b src ds graph
160        | [], _, _ ->
161          invalid_arg "translation: empty preamble with several destinations"
162        | _ ->
163          let f (lbls, g) blck dst =
164            let lbl = fresh () in
165            (lbl :: lbls, put_block [] [blck] lbl [dst] g) in
166          let (lbls, graph) = List.fold_left2 f ([], graph) blocks dests in
167          put_rev (List.rev stmts) src lbls graph in
168
169    let trans lbl stmt (x, graph) =
170      let (y, stmts, blocks, redirects) = f x lbl stmt in
171      let succs = match redirects with
172        | Some x -> x
173        | None -> Src.successors stmt in
174      (y, put_block stmts blocks lbl succs graph) in
175
176    Src.NodeMap.fold trans g (info, Trg.NodeMap.empty)
177
178  let translate fresh f =
179    let f' x lbl stmt =
180      let (y, stmts) = f x lbl stmt in
181      (y, [], [stmts], None) in
182    translate_general fresh f'
183
184  let translate_with_redirects fresh f =
185    let f' x lbl stmt =
186      let (y, stmts, redirects) = f x lbl stmt in
187      (y, [], [stmts], redirects) in
188    translate_general fresh f'
189
190  let translate_pure fresh f g =
191    let f' () l s = ((), [], [f l s], None) in
192    snd (translate_general fresh f' () g)
193
194  let translate_pure_with_redirects fresh f g =
195    let f' () l s =
196      let (res, redirects) = f l s in
197      ((), [], [res], redirects) in
198    snd (translate_general fresh f' () g)
199
200  open BList
201
202  let translate_with_redirects' freshl freshr f def g =
203    let f' def lbl stmt =
204      let (stmts, redirects) = f lbl stmt in
205      let (def, stmts) = BList.compile freshr def stmts in
206      (def, stmts, redirects) in
207    translate_with_redirects freshl f' def g
208
209  let translate' freshl freshr f =
210    let f' lbl stmt = (f lbl stmt, None) in
211    translate_with_redirects' freshl freshr f'
212
213
214
215  (* let translate f = *)
216  (*   let f' x _ stmt = *)
217  (*     let (y, stmts) = f x stmt in *)
218  (*     (y, stmts, [], [Src.successors stmt]) in *)
219  (*   translate_general f' *)
220
221  (* let translate_with_redirects f = *)
222  (*   let f' x _ stmt = *)
223  (*     let (y, stmts, redirects) = f x stmt in *)
224  (*     (y, stmts, [], [redirects]) in *)
225  (*   translate_general f' *)
226
227  (* let translate_pure f fresh g = *)
228  (*   let f' () _ stmt = *)
229  (*     ((), f stmt, [], [Src.successors stmt]) in *)
230  (*   snd (translate_general f' fresh () g) *)
231
232  (* let translate_pure_with_redirects f fresh g = *)
233  (*   let f' () _ stmt = *)
234  (*     let (res, redirects) = f stmt in *)
235  (*     ((), res, [], [redirects]) in *)
236  (*   snd (translate_general f' fresh () g) *)
237
238end
Note: See TracBrowser for help on using the repository browser.