source: extracted/untrusted/build.ml @ 2742

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

Untrusted register colouring fully branched.

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