1 | (* Pasted from Pottier's PP compiler *) |
---|
2 | |
---|
3 | open ERTL |
---|
4 | open Untrusted_interference |
---|
5 | |
---|
6 | let 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 | |
---|