source: src/ERTL/Interference.ma

Last change on this file was 3265, checked in by tranquil, 7 years ago

added validate_pointer filter
in Interference added that intereference only fires on non eliminable
statements

File size: 2.3 KB
RevLine 
[3014]1include "ERTL/liveness.ma".
[1127]2
[1229]3inductive decision: Type[0] ≝
[1232]4  | decision_spill: nat → decision
[1229]5  | decision_colour: Register → decision.
6
[3255]7definition DeqRegister : DeqSet ≝
8mk_DeqSet Register eq_Register ?.
9#x #y % [2: #EQ destruct cases y % ]
10cases x -x try (cases y -y normalize #EQ destruct %)
11qed.
12
13unification hint 0 ≔ ⊢ Register ≡ carr DeqRegister.
14
15definition is_src_of_move :
16∀globals.joint_statement ERTL globals → vertex → bool ≝
17λglobals,s,v.
18match 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
39definition 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.
44match v1 with
45[ inr R ⇒
46  match v2 with [ inl _ ⇒ R ∈ RegistersForbidden | _ ⇒ false ]
47| _ ⇒ false ]
48
49match stmt_at … (joint_if_code … fn) l with
50[ None ⇒ false
51| Some s ⇒
[3265]52  ¬eliminable … (liveafter l) s ∧
[3255]53  in_lattice v1 (defined … s) ∧ in_lattice v2 (liveafter l) ∧
54  ¬is_src_of_move … s v2
55].
56
57definition interferes ≝ λglobals,fn,liveafter,label,v1,v2.
58interferes_asym globals fn liveafter label v1 v2 ∨
59interferes_asym globals fn liveafter label v2 v1.
60
[1423]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 *)
[3255]64record coloured_graph (interferes : label → vertex → vertex → bool) : Type[1] ≝
[1423]65{ colouring: vertex → decision
66; spilled_no: nat
[3255]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
[1229]71}.
72
[2739]73definition coloured_graph_computer ≝
74 ∀globals.
[3014]75  ∀fn:joint_internal_function ERTL globals.
[2942]76   ∀liveafter.
[3263]77    list register → (* callee saved store *)
[3255]78    coloured_graph (interferes … fn liveafter).
Note: See TracBrowser for help on using the repository browser.