1 | include "ERTL/liveness.ma". |
---|

2 | include "utilities/Interference.ma". |
---|

3 | |
---|

4 | axiom graph : Type[0]. |
---|

5 | axiom create: ∀globals: list ident. ertl_internal_function globals → graph. |
---|

6 | |
---|

7 | record build_properties: Type[1] ≝ |
---|

8 | { |
---|

9 | lookup: graph → register → vertex |
---|

10 | }. |
---|

11 | |
---|

12 | (* |
---|

13 | definition build ≝ |
---|

14 | λglobals: list ident. |
---|

15 | λint_fun: ertl_internal_function globals. |
---|

16 | let liveafter ≝ analyse globals int_fun in |
---|

17 | let graph ≝ ig_create (ertl_if_locals globals int_fun) in |
---|

18 | let graph ≝ ig_mkiph graph (ertl_if_locals globals int_fun) RegistersForbidden in |
---|

19 | let graph ≝ |
---|

20 | foldi ? ? ? (λlabel. λstmt. λgraph. |
---|

21 | let live ≝ liveafter label in |
---|

22 | match eliminable globals live stmt with |
---|

23 | [ Some _ ⇒ graph |
---|

24 | | None ⇒ |
---|

25 | let defined ≝ defined globals stmt in |
---|

26 | let exceptions ≝ |
---|

27 | match stmt with |
---|

28 | [ joint_st_sequential seq l ⇒ |
---|

29 | match seq with |
---|

30 | [ joint_instr_move pair_reg ⇒ |
---|

31 | let reg_r ≝ \snd pair_reg in |
---|

32 | match reg_r with |
---|

33 | [ hardware hw ⇒ lattice_hsingleton hw |
---|

34 | | pseudo ps ⇒ lattice_psingleton ps |
---|

35 | ] |
---|

36 | | _ ⇒ ? |
---|

37 | ] |
---|

38 | | _ ⇒ ? |
---|

39 | ] |
---|

40 | in |
---|

41 | let graph ≝ ig_mki graph (lattice_diff live exceptions) defined in |
---|

42 | let graph ≝ |
---|

43 | match stmt with |
---|

44 | [ joint_st_sequential seq l ⇒ |
---|

45 | match seq with |
---|

46 | [ joint_instr_move pair_reg ⇒ |
---|

47 | let reg_l ≝ \fst pair_reg in |
---|

48 | let reg_r ≝ \snd pair_reg in |
---|

49 | match reg_l with |
---|

50 | [ pseudo ps1 ⇒ |
---|

51 | match reg_r with |
---|

52 | [ pseudo ps2 ⇒ ig_mkppp graph ps1 ps2 |
---|

53 | | hardware hw ⇒ ig_mkpph graph ps1 hw |
---|

54 | ] |
---|

55 | | hardware hw1 ⇒ |
---|

56 | match reg_r with |
---|

57 | [ pseudo ps ⇒ ig_mkpph graph ps hw1 |
---|

58 | | hardware hw2 ⇒ graph |
---|

59 | ] |
---|

60 | ] |
---|

61 | | _ ⇒ graph |
---|

62 | ] |
---|

63 | | _ ⇒ graph |
---|

64 | ] |
---|

65 | in graph |
---|

66 | ]) (ertl_if_graph globals int_fun) graph |
---|

67 | in |
---|

68 | 〈liveafter, graph〉. |
---|

69 | [*: @lattice_bottom ] (* XXX: matita bug here! *) |
---|

70 | qed. *) |
---|