source: extracted/untrusted/build.ml @ 2968

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

Exported again, now the execution is correct up to LIN for a simple program.

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