Line | |
---|

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

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

3 | |
---|

4 | definition build ≝ |
---|

5 | λint_fun: ertl_internal_function. |
---|

6 | let liveafter ≝ analyse int_fun in |
---|

7 | let graph ≝ ig_create (ertl_if_locals int_fun) in |
---|

8 | let graph ≝ ig_mkiph graph (ertl_if_locals int_fun) forbidden_registers in |
---|

9 | let graph ≝ |
---|

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

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

12 | match eliminable live stmt with |
---|

13 | [ Some _ ⇒ graph |
---|

14 | | None ⇒ |
---|

15 | let defined ≝ defined stmt in |
---|

16 | let exceptions ≝ |
---|

17 | match stmt with |
---|

18 | [ ertl_st_move _ sr _ ⇒ lattice_psingleton sr |
---|

19 | | ertl_st_set_hdw _ sr _ ⇒ lattice_psingleton sr |
---|

20 | | ertl_st_get_hdw _ sr _ ⇒ lattice_hsingleton sr |
---|

21 | | _ ⇒ ? |
---|

22 | ] |
---|

23 | in |
---|

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

25 | let graph ≝ |
---|

26 | match stmt with |
---|

27 | [ ertl_st_move r1 r2 _ ⇒ ig_mkppp graph r1 r2 |
---|

28 | | ertl_st_get_hdw r hwr _ ⇒ ig_mkpph graph r hwr |
---|

29 | | ertl_st_set_hdw hwr r _ ⇒ ig_mkpph graph r hwr |
---|

30 | | _ ⇒ graph |
---|

31 | ] |
---|

32 | in graph |
---|

33 | ]) (ertl_if_graph int_fun) graph |
---|

34 | in |
---|

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

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

37 | qed. |
---|

**Note:** See

TracBrowser
for help on using the repository browser.