Last change
on this file since 1185 was
1185,
checked in by mulligan, 9 years ago

ported liveness analysis to new code

File size:
1.9 KB

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  [ joint_st_sequential seq l ⇒ 

19  match seq with 

20  [ joint_instr_move pair_reg ⇒ 

21  let reg_r ≝ \snd pair_reg in 

22  match reg_r with 

23  [ hardware hw ⇒ lattice_hsingleton hw 

24   pseudo ps ⇒ lattice_psingleton ps 

25  ] 

26   _ ⇒ ? 

27  ] 

28   _ ⇒ ? 

29  ] 

30  in 

31  let graph ≝ ig_mki graph (lattice_diff live exceptions) defined in 

32  let graph ≝ 

33  match stmt with 

34  [ joint_st_sequential seq l ⇒ 

35  match seq with 

36  [ joint_instr_move pair_reg ⇒ 

37  let reg_l ≝ \fst pair_reg in 

38  let reg_r ≝ \snd pair_reg in 

39  match reg_l with 

40  [ pseudo ps1 ⇒ 

41  match reg_r with 

42  [ pseudo ps2 ⇒ ig_mkppp graph ps1 ps2 

43   hardware hw ⇒ ig_mkpph graph ps1 hw 

44  ] 

45   hardware hw1 ⇒ 

46  match reg_r with 

47  [ pseudo ps ⇒ ig_mkpph graph ps hw1 

48   hardware hw2 ⇒ graph 

49  ] 

50   _ ⇒ graph 

51  ] 

52   _ ⇒ graph 

53  ] 

54  in graph 

55  ]) (ertl_if_graph int_fun) graph 

56  in 

57  〈liveafter, graph〉. 

58  [*: @lattice_bottom ] (* XXX: matita bug here! *) 

59  qed. 

Note: See
TracBrowser
for help on using the repository browser.