source: extracted/untrusted/build.ml @ 2740

Last change on this file since 2740 was 2740, checked in by sacerdot, 7 years ago

Graph colouring terminated up to Uses that will be implemented
in Matita.

File size: 5.1 KB
Line 
1(* Pasted from Pottier's PP compiler *)
2
3open ERTL
4open Untrusted_interference
5
6let build globals int_fun liveafter =
7
8  (* Create an interference graph whose vertices are the procedure's
9     pseudo-registers. This graph initially has no edges. *)
10
11  (*CSC: we are not precise here, we take all the pseudoregisters in the
12    universe; we could compute the set by iteration over the code *)
13  let f_locals =
14   let first_fresh = int_fun.Joint.joint_if_luniverse in
15   let rec aux n =
16    if Positive.eqb0 n first_fresh = Bool.True then
17     Pset.empty
18    else
19     Pset.add n (aux (Positive.succ n))
20   in
21    aux Positive.One in
22
23  let graph = create f_locals in
24
25  (* Every pseudo register interferes with special forbidden registers. *)
26
27  let graph = mkiph graph f_locals
28   (Untrusted_interference.hwregisterset_of_list I8051.registersForbidden) in
29
30  (* Iterate over all statements in the control flow graph and populate the
31     interference graph with interference and preference edges. *)
32
33  let graph =
34    Identifiers.foldi0 PreIdentifiers.LabelTag (fun label stmt graph ->
35      let live = liveafter label in
36      match Glue.option_of_matitaoption (Liveness.eliminable globals live stmt) with
37
38      | Some _ ->
39
40          (* This statement is eliminable and should be ignored. Eliminable
41             statements have not been eliminated yet, because we are still
42             in between ERTL and LTL. They *will* be eliminated soon, though,
43             so there is no reason to take them into account while building
44             the interference graph. *)
45
46          graph
47
48      | None ->
49
50          (* Create interference edges. The general rule is, every
51             pseudo-register or hardware register that is defined (written) by
52             a statement interferes with every pseudo-register or hardware
53             register (other than itself) that is live immediately after the
54             statement executes.
55
56             An exception to the general rule can be made for move
57             statements. In a move statement, we do not need the source
58             and destination pseudo-registers to be assigned distinct hardware
59             registers, since they contain the same value -- in fact, we would
60             like them to be assigned the same hardware register. So, for a
61             move statement, we let the register that is defined (written)
62             interfere with every pseudo-register, other than itself *and
63             other than the source pseudo-register*, that is live immediately
64             after the statement executes. This optimization is explained in
65             Chapter 10 of Appel's book (p. 221).
66
67             This special case is only a hack that works in many cases. There
68             are cases where it doesn't suffice. For instance, if two
69             successive move statements have the same source [r0], then
70             their destinations [r1] and [r2] *will* be considered as
71             interfering, even though it would in fact be correct and
72             desirable to map both of them to the same hardware register. A
73             more general solution would be to perform a static analysis that
74             determines, for every program point, which pseudo-registers
75             definitely hold the same value, and to exploit this information
76             to build fewer interference edges. *)
77
78          let defined = Liveness.defined globals stmt in
79          let exceptions =
80            match stmt with
81            | Joint.Sequential (Joint.Step_seq (Joint.MOVE arg),_) ->
82               (match Obj.magic arg with
83                  {Types.snd = Joint.Reg (ERTL.PSD sourcer)} ->
84                   Liveness.rl_psingleton sourcer
85                | {Types.snd = Joint.Reg (ERTL.HDW sourcehwr)} ->
86                   Liveness.rl_hsingleton sourcehwr
87                | _ -> Liveness.rl_bottom)
88            | _ ->
89                Liveness.rl_bottom
90          in
91          let graph =
92            mki graph (Obj.magic (Liveness.rl_diff live exceptions))
93             (Obj.magic defined)
94          in
95
96(*
97          (* Two registers written at the same time are interfering (they
98             obviously should not be associated the same address).
99             Only happens with St_addr. *)
100
101          let graph =
102            match stmt with
103              | St_addr (r1, r2, _, _) ->
104                mki graph (Liveness.L.psingleton r1) (Liveness.L.psingleton r2)
105              | _ ->
106                graph
107          in
108*)
109
110          (* Create preference edges between pseudo-registers. Two registers
111             should preferably be assigned the same color when they are
112             related by a move statement, so that the move statement can
113             be eliminated. *)
114
115          let graph =
116            match stmt with
117            | Joint.Sequential (Joint.Step_seq (Joint.MOVE arg),_) ->
118               (match Obj.magic arg with
119                  {Types.fst = ERTL.PSD r1 ; snd = Joint.Reg (ERTL.PSD r2)} ->
120                    mkppp graph r1 r2
121                | {Types.fst = ERTL.PSD r1 ; snd = Joint.Reg (ERTL.HDW r2)}
122                | {Types.fst = ERTL.HDW r2 ; snd = Joint.Reg (ERTL.PSD r1)} ->
123                    mkpph graph r1 r2
124                | _ -> graph)
125            | _ ->
126                graph
127          in
128  (*
129
130          (* Add interference edges between the hardware register [$zero]
131             and every pseudo-register that the statement renders
132             nonzeroable. See [Zero] for an explanation. *)
133
134          let graph =
135            mkiph graph (Zero.nonzeroable i) (MIPS.RegisterSet.singleton MIPS.zero)
136          in
137  *)
138          graph
139
140    ) (Obj.magic int_fun.Joint.joint_if_code) graph
141  in
142
143  (* Done. *)
144
145  graph
146
Note: See TracBrowser for help on using the repository browser.