1 | include "ERTL/liveness.ma". |
---|
2 | include "utilities/Interference.ma". |
---|
3 | |
---|
4 | definition vertex ≝ register ⊎ Register. |
---|
5 | |
---|
6 | record graph: Type[0] ≝ |
---|
7 | { |
---|
8 | interferes: vertex → vertex → bool |
---|
9 | }. |
---|
10 | |
---|
11 | axiom create: ∀globals: list ident. ertl_internal_function globals → graph. |
---|
12 | |
---|
13 | inductive decision: Type[0] ≝ |
---|
14 | | decision_spill: decision |
---|
15 | | decision_colour: Register → decision. |
---|
16 | |
---|
17 | record coloured_graph (d: Type[0]): Type[1] ≝ |
---|
18 | { |
---|
19 | the_graph: graph; |
---|
20 | colouring: register → d; |
---|
21 | prop_colouring: ∀v1. ∀v2. (interferes the_graph (inl … v1) (inl … v2) = true) → colouring v1 ≠ colouring v2 |
---|
22 | }. |
---|
23 | |
---|
24 | definition initial_colouring ≝ coloured_graph decision. |
---|
25 | definition stack_colouring ≝ coloured_graph nat. |
---|
26 | |
---|
27 | (* |
---|
28 | definition build ≝ |
---|
29 | λglobals: list ident. |
---|
30 | λint_fun: ertl_internal_function globals. |
---|
31 | let liveafter ≝ analyse globals int_fun in |
---|
32 | let graph ≝ ig_create (ertl_if_locals globals int_fun) in |
---|
33 | let graph ≝ ig_mkiph graph (ertl_if_locals globals int_fun) RegistersForbidden in |
---|
34 | let graph ≝ |
---|
35 | foldi ? ? ? (λlabel. λstmt. λgraph. |
---|
36 | let live ≝ liveafter label in |
---|
37 | match eliminable globals live stmt with |
---|
38 | [ Some _ ⇒ graph |
---|
39 | | None ⇒ |
---|
40 | let defined ≝ defined globals stmt in |
---|
41 | let exceptions ≝ |
---|
42 | match stmt with |
---|
43 | [ joint_st_sequential seq l ⇒ |
---|
44 | match seq with |
---|
45 | [ joint_instr_move pair_reg ⇒ |
---|
46 | let reg_r ≝ \snd pair_reg in |
---|
47 | match reg_r with |
---|
48 | [ hardware hw ⇒ lattice_hsingleton hw |
---|
49 | | pseudo ps ⇒ lattice_psingleton ps |
---|
50 | ] |
---|
51 | | _ ⇒ ? |
---|
52 | ] |
---|
53 | | _ ⇒ ? |
---|
54 | ] |
---|
55 | in |
---|
56 | let graph ≝ ig_mki graph (lattice_diff live exceptions) defined in |
---|
57 | let graph ≝ |
---|
58 | match stmt with |
---|
59 | [ joint_st_sequential seq l ⇒ |
---|
60 | match seq with |
---|
61 | [ joint_instr_move pair_reg ⇒ |
---|
62 | let reg_l ≝ \fst pair_reg in |
---|
63 | let reg_r ≝ \snd pair_reg in |
---|
64 | match reg_l with |
---|
65 | [ pseudo ps1 ⇒ |
---|
66 | match reg_r with |
---|
67 | [ pseudo ps2 ⇒ ig_mkppp graph ps1 ps2 |
---|
68 | | hardware hw ⇒ ig_mkpph graph ps1 hw |
---|
69 | ] |
---|
70 | | hardware hw1 ⇒ |
---|
71 | match reg_r with |
---|
72 | [ pseudo ps ⇒ ig_mkpph graph ps hw1 |
---|
73 | | hardware hw2 ⇒ graph |
---|
74 | ] |
---|
75 | ] |
---|
76 | | _ ⇒ graph |
---|
77 | ] |
---|
78 | | _ ⇒ graph |
---|
79 | ] |
---|
80 | in graph |
---|
81 | ]) (ertl_if_graph globals int_fun) graph |
---|
82 | in |
---|
83 | 〈liveafter, graph〉. |
---|
84 | [*: @lattice_bottom ] (* XXX: matita bug here! *) |
---|
85 | qed. *) |
---|