1 | include "ERTL/liveness.ma". |
---|
2 | |
---|
3 | inductive decision: Type[0] ≝ |
---|
4 | | decision_spill: nat → decision |
---|
5 | | decision_colour: Register → decision. |
---|
6 | |
---|
7 | definition DeqRegister : DeqSet ≝ |
---|
8 | mk_DeqSet Register eq_Register ?. |
---|
9 | #x #y % [2: #EQ destruct cases y % ] |
---|
10 | cases x -x try (cases y -y normalize #EQ destruct %) |
---|
11 | qed. |
---|
12 | |
---|
13 | unification hint 0 ≔ ⊢ Register ≡ carr DeqRegister. |
---|
14 | |
---|
15 | definition is_src_of_move : |
---|
16 | ∀globals.joint_statement ERTL globals → vertex → bool ≝ |
---|
17 | λglobals,s,v. |
---|
18 | match s with |
---|
19 | [ sequential s _ ⇒ |
---|
20 | match s with |
---|
21 | [ step_seq s ⇒ |
---|
22 | match s with |
---|
23 | [ MOVE pr ⇒ |
---|
24 | match \snd pr with |
---|
25 | [ Reg r ⇒ |
---|
26 | match r with |
---|
27 | [ PSD r ⇒ match v with [ inl r' ⇒ eq_identifier … r r' | _ ⇒ false ] |
---|
28 | | HDW r ⇒ match v with [ inr r' ⇒ eq_Register r r' | _ ⇒ false ] |
---|
29 | ] |
---|
30 | | _ ⇒ false |
---|
31 | ] |
---|
32 | | _ ⇒ false |
---|
33 | ] |
---|
34 | | _ ⇒ false |
---|
35 | ] |
---|
36 | | _ ⇒ false |
---|
37 | ]. |
---|
38 | |
---|
39 | definition interferes_asym : |
---|
40 | ∀globals.joint_internal_function ERTL globals → |
---|
41 | valuation register_lattice → |
---|
42 | label → vertex → vertex → bool ≝ |
---|
43 | λglobals,fn,liveafter,l,v1,v2. |
---|
44 | match v1 with |
---|
45 | [ inr R ⇒ |
---|
46 | match v2 with [ inl _ ⇒ R ∈ RegistersForbidden | _ ⇒ false ] |
---|
47 | | _ ⇒ false ] |
---|
48 | ∨ |
---|
49 | match stmt_at … (joint_if_code … fn) l with |
---|
50 | [ None ⇒ false |
---|
51 | | Some s ⇒ |
---|
52 | ¬eliminable … (liveafter l) s ∧ |
---|
53 | in_lattice v1 (defined … s) ∧ in_lattice v2 (liveafter l) ∧ |
---|
54 | ¬is_src_of_move … s v2 |
---|
55 | ]. |
---|
56 | |
---|
57 | definition interferes ≝ λglobals,fn,liveafter,label,v1,v2. |
---|
58 | interferes_asym globals fn liveafter label v1 v2 ∨ |
---|
59 | interferes_asym globals fn liveafter label v2 v1. |
---|
60 | |
---|
61 | (* prop_colouring is the non interferece |
---|
62 | prop_colouring 2 and 3 together say that spilled_no is the number of spilled |
---|
63 | registers *) |
---|
64 | record coloured_graph (interferes : label → vertex → vertex → bool) : Type[1] ≝ |
---|
65 | { colouring: vertex → decision |
---|
66 | ; spilled_no: nat |
---|
67 | ; prop_colouring: ∀l. ∀v1, v2: vertex. |
---|
68 | interferes l v1 v2 → colouring v1 = colouring v2 → v1 = v2 |
---|
69 | ; prop_spilled_no: ∀v1:vertex.∀i.colouring v1 = decision_spill i → i < spilled_no |
---|
70 | ; hdw_same_colouring : ∀R.colouring (inr … R) = decision_colour R |
---|
71 | }. |
---|
72 | |
---|
73 | definition coloured_graph_computer ≝ |
---|
74 | ∀globals. |
---|
75 | ∀fn:joint_internal_function ERTL globals. |
---|
76 | ∀liveafter. |
---|
77 | list register → (* callee saved store *) |
---|
78 | coloured_graph (interferes … fn liveafter). |
---|