source: src/ERTL/build.ma @ 1185

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 
1include "ERTL/liveness.ma".
2include "utilities/Interference.ma".
3
4definition 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! *)
59qed.
Note: See TracBrowser for help on using the repository browser.