source: src/ERTL/ERTLToLTL.ma @ 1230

Last change on this file since 1230 was 1230, checked in by mulligan, 8 years ago

more changes

File size: 24.4 KB
Line 
1include "ERTL/ERTL.ma".
2include "LTL/LTL.ma".
3include "ERTL/spill.ma".
4include "ERTL/build.ma".
5include "ERTL/Interference.ma".
6include "ASM/Arithmetic.ma".
7
8(* XXX: define an interference graph for a function and colour it, allowing
9        the consultation of registers. *)
10definition initial_colouring ≝
11  λglobals.
12  λint_fun.
13  let 〈ignore, graph〉 ≝ build globals int_fun in
14  let coloured ≝ colour_initial graph in
15    coloured.
16
17definition interference_lookup ≝
18  λcoloured: initial_colouring.
19  λr.
20    colouring … coloured r.
21
22definition prepare_graph_for_second_colouring ≝
23  λglobals: list ident.
24  λcoloured: initial_colouring.
25    let g ≝ the_graph decision coloured in
26    let restricted ≝ ig_restrict g (λv.
27      match colouring decision coloured v with
28      [ decision_spill ⇒ true
29      | decision_colour _ ⇒ false
30      ]
31    )
32    in restricted.
33
34definition second_colouring ≝
35  λglobals: list ident.
36  λcoloured.
37    let prepared ≝ prepare_graph_for_second_colouring globals coloured in
38      colour_stack prepared.
39
40definition lookup ≝
41  λinitial.
42  λsecond.
43  λr.
44  match interference_lookup initial r with
45  [ decision_colour _ ⇒ ?
46  | decision_spill ⇒ ?
47  ].
48
49definition fresh_label ≝
50  λglobals: list ident.
51  λluniv.
52    fresh LabelTag luniv.
53
54definition add_graph ≝
55  λglobals.
56  λlabel.
57  λstmt: ltl_statement globals.
58  λgraph: ltl_statement_graph globals.
59    add LabelTag ? graph label stmt.
60
61definition generate ≝
62  λglobals: list ident.
63  λluniv.
64  λgraph: ltl_statement_graph globals.
65  λstmt: ltl_statement globals.
66  let 〈l, luniv〉 ≝ fresh_label globals luniv in
67  let graph ≝ add_graph globals l stmt graph in
68    〈l, graph, luniv〉.
69
70definition num_locals ≝
71  λglobals.
72  λint_fun.
73    colour_locals + (ertl_if_stacksize globals int_fun).
74
75definition stacksize ≝
76  λglobals.
77  λint_fun.
78    colour_locals + (ertl_if_stacksize globals int_fun).
79
80definition adjust_off ≝
81  λglobals.
82  λint_fun.
83  λoff.
84  let 〈ignore, int_off〉 ≝ half_add ? int_size off in
85  let 〈sub, ignore〉 ≝ sub_8_with_carry (bitvector_of_nat ? (num_locals globals int_fun)) int_off false in
86    sub.
87
88definition get_stack:
89 ∀globals. ertl_internal_function globals → graph (ltl_statement globals) → Register → Byte → label →
90  ltl_statement globals × (graph (ltl_statement globals)) × (universe LabelTag)
91
92  λglobals: list ident.
93  λint_fun.
94  λgraph: graph (ltl_statement (globals)).
95  λr.
96  λoff.
97  λl.
98    let off ≝ adjust_off globals int_fun off in
99    let luniv ≝ ertl_if_luniverse globals int_fun in
100    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc r)) l) in
101    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_load … globals it it it) l) in
102    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPH)) l) in
103    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Addc it RegisterSPH) l) in
104    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_int … globals RegisterA (zero ?)) l) in
105    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPL)) l) in
106    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Add it RegisterSPL) l) in
107      〈joint_st_sequential … ltl_params globals (joint_instr_int ? globals RegisterA off) l, graph, luniv〉.
108
109definition set_stack:
110  ∀globals. ertl_internal_function globals → ltl_statement_graph globals → Byte
111    → Register → label → ((ltl_statement globals) × (ltl_statement_graph globals) × (universe LabelTag)) ≝
112  λglobals: list ident.
113  λint_fun.
114  λgraph: graph (ltl_statement (globals)).
115  λoff.
116  λr.
117  λl.
118  let off ≝ adjust_off globals int_fun off in
119  let luniv ≝ ertl_if_luniverse globals int_fun in
120  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_store ltl_params … globals it it it) l) in
121  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc r)) l) in
122  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPH)) l) in
123  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Addc it RegisterSPH) l) in
124  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_int … globals RegisterA (zero ?)) l) in
125  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPL)) l) in
126  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Add it RegisterSPL) l) in
127    〈joint_st_sequential … ltl_params globals (joint_instr_int ? globals RegisterA off) l, graph, luniv〉.
128
129definition write:
130  ∀globals: list ident. ertl_internal_function globals → ltl_statement_graph globals → register → label →
131    ? ≝
132  λglobals: list ident.
133  λint_fun.
134  λgraph.
135  λr.
136  λl.
137  match lookup r with
138  [ decision_spill off ⇒
139    let 〈stmt, graph, luniv〉 ≝ set_stack globals int_fun graph off RegisterSST l in
140    let 〈l, graph, int_fun〉 ≝ generate globals luniv graph stmt in
141      〈RegisterSST, l, graph, luniv〉
142  | decision_colour hwr ⇒
143    let luniv ≝ ertl_if_luniverse globals int_fun in
144      〈hwr, l, graph, luniv〉
145  ].
146
147definition read:
148  ∀globals: list ident. ertl_internal_function globals → ltl_statement_graph globals → register
149    → (Register → ltl_statement globals) → ? ≝
150  λglobals.
151  λint_fun.
152  λgraph.
153  λr.
154  λstmt.
155  match lookup r with
156  [ decision_colour hwr ⇒ generate globals (ertl_if_luniverse globals int_fun) graph (stmt hwr)
157  | decision_spill off ⇒
158    let temphwr ≝ RegisterSST in
159    let 〈l, graph, luniv〉 ≝ generate globals (ertl_if_luniverse globals int_fun) graph (stmt temphwr) in
160    let 〈stmt, graph, luniv〉 ≝ get_stack globals int_fun graph temphwr off l in
161      generate globals luniv graph stmt
162  ].
163
164definition move ≝
165  λglobals: list ident.
166  λint_fun.
167  λgraph: graph (ltl_statement globals).
168  λdest: decision.
169  λsrc: decision.
170  λl: label.
171  match dest with
172  [ decision_colour dest_hwr ⇒
173    match src with
174    [ decision_colour src_hwr ⇒
175      let luniv ≝ ertl_if_luniverse globals int_fun in
176      if eq_Register dest_hwr src_hwr then
177        〈joint_st_goto … globals l, graph, luniv〉
178      else
179        let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc dest_hwr)) l) in
180          〈joint_st_sequential … globals (joint_instr_move … ltl_params globals (to_acc src_hwr)) l, graph, luniv〉
181    | decision_spill src_off ⇒ get_stack globals int_fun graph dest_hwr src_off l
182    ]
183  | decision_spill dest_off ⇒
184    match src with
185    [ decision_colour src_hwr ⇒ set_stack globals int_fun graph dest_off src_hwr l
186    | decision_spill src_off ⇒
187      let luniv ≝ ertl_if_luniverse globals int_fun in
188      if eq_bv ? dest_off src_off then
189        〈joint_st_goto … globals l, graph, luniv〉
190      else
191        let temp_hwr ≝ RegisterSST in
192        let 〈stmt, graph, luniv〉 ≝ set_stack globals int_fun graph dest_off temp_hwr l in
193        let 〈l, graph, luniv〉 ≝ generate globals luniv graph stmt in
194          get_stack globals int_fun graph temp_hwr src_off l
195    ]
196  ].
197
198definition newframe ≝
199  λglobals: list ident.
200  λint_fun: ertl_internal_function globals.
201  λgraph: ltl_statement_graph globals.
202  λl: label.
203  if eq_nat (stacksize globals int_fun) 0 then
204    〈joint_st_goto ltl_params globals l, graph, (ertl_if_luniverse globals int_fun)〉
205  else
206    let luniv ≝ ertl_if_luniverse globals int_fun in
207    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_move … globals (from_acc RegisterSPH)) l) in
208    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_op2 … globals Sub it RegisterDPH) l) in
209    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_int … globals RegisterDPH (zero ?)) l) in
210    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_move … globals (to_acc RegisterSPH)) l) in
211    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_move … globals (from_acc RegisterSPL)) l) in
212    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_op2 … globals Sub it RegisterDPL) l) in
213    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_clear_carry … globals) l) in
214    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_int … globals RegisterDPL (bitvector_of_nat ? (stacksize globals int_fun))) l) in
215      〈joint_st_sequential ltl_params globals (joint_instr_move ltl_params globals (to_acc RegisterSPL)) l, graph, luniv〉.
216
217definition delframe ≝
218  λglobals.
219  λint_fun.
220  λgraph: graph (ltl_statement globals).
221  λl.
222  if eq_nat (stacksize globals int_fun) 0 then
223    〈joint_st_goto ltl_params globals l, graph, ertl_if_luniverse globals int_fun〉
224  else
225    let luniv ≝ ertl_if_luniverse globals int_fun in
226    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_move … globals (from_acc RegisterSPH)) l) in
227    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_op2 … globals Addc it RegisterSPH) l) in
228    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_int … globals RegisterA (zero ?)) l) in
229    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_move … globals (from_acc RegisterSPL)) l) in
230    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_op2 … globals Add it RegisterSPL) l) in
231      〈joint_st_sequential ltl_params globals (joint_instr_int ltl_params globals RegisterA (bitvector_of_nat ? (stacksize globals int_fun))) l, graph, luniv〉.
232
233definition translate_statement ≝
234  λglobals: list ident.
235  λint_fun.
236  λgraph: ltl_statement_graph globals.
237  λstmt: ertl_statement globals.
238  match stmt with
239  [ joint_st_sequential seq l ⇒
240    let luniv ≝ ertl_if_luniverse globals int_fun in
241    match seq with
242    [ joint_instr_comment c ⇒
243      〈joint_st_sequential ltl_params globals (joint_instr_comment … globals c) l, graph, luniv〉
244    | joint_instr_cost_label cost_lbl ⇒
245      〈joint_st_sequential … globals (joint_instr_cost_label … globals cost_lbl) l, graph, luniv〉
246    | joint_instr_pop r ⇒
247      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph r l in
248      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
249        〈joint_st_sequential … globals (joint_instr_pop ltl_params globals it) l, graph, luniv〉
250    | joint_instr_push r ⇒
251      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_push … globals it) l) in
252      let int_fun ≝ set_luniverse globals int_fun luniv in
253      let 〈l, graph, luniv〉 ≝ read globals int_fun graph r (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
254        〈joint_st_goto ltl_params globals l, graph, luniv〉
255    | joint_instr_cond srcr lbl_true ⇒
256      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_cond … globals it lbl_true) l) in
257      let int_fun ≝ set_luniverse globals int_fun luniv in
258      let 〈l, graph, luniv〉 ≝ read globals int_fun graph srcr (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
259        〈joint_st_goto ltl_params globals l, graph, luniv〉
260    | joint_instr_call_id f ignore ⇒ 〈joint_st_sequential … globals (joint_instr_call_id … globals f ignore) l, graph, luniv〉
261    | joint_instr_store addr1 addr2 srcr ⇒
262      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_store … globals it it it) l) in
263      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterST1)) l) in
264      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPH)) l) in
265      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterST0)) l) in
266      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPL)) l) in
267      let int_fun ≝ set_luniverse globals int_fun luniv in
268      let 〈l, graph, luniv〉 ≝ read globals int_fun graph addr1 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
269      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterST0)) l) in
270      let int_fun ≝ set_luniverse globals int_fun luniv in
271      let 〈l, graph, luniv〉 ≝ read globals int_fun graph addr2 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
272      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterST1)) l) in
273      let 〈l, graph, luniv〉 ≝ read globals int_fun graph srcr (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
274        〈joint_st_goto ltl_params globals l, graph, luniv〉
275    | joint_instr_load destr addr1 addr2 ⇒
276      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph destr l in
277      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
278      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_load … globals it it it) l) in
279      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPH)) l) in
280      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterST0)) l) in
281      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPL)) l) in
282      let int_fun ≝ set_luniverse globals int_fun luniv in
283      let 〈l, graph, luniv〉 ≝ read globals int_fun graph addr1 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
284      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterST0)) l) in
285      let int_fun ≝ set_luniverse globals int_fun luniv in
286      let 〈l, graph, luniv〉 ≝ read globals int_fun graph addr2 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
287        〈joint_st_goto ltl_params globals l, graph, luniv〉
288    | joint_instr_clear_carry ⇒ 〈joint_st_sequential … globals (joint_instr_clear_carry … globals) l, graph, luniv〉
289    | joint_instr_set_carry ⇒ 〈joint_st_sequential … globals (joint_instr_set_carry … globals) l, graph, luniv〉
290    | joint_instr_op2 op2 destr srcr ⇒
291      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph destr l in
292      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
293      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals op2 it RegisterB) l) in
294      let luniv ≝ set_luniverse globals int_fun luniv in
295      let 〈l, graph, luniv〉 ≝ read globals int_fun graph destr (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
296      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterB)) l) in
297      let luniv ≝ set_luniverse globals int_fun luniv in
298      let 〈l, graph, luniv〉 ≝ read globals int_fun graph srcr (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
299        〈joint_st_goto ltl_params globals l, graph, luniv〉
300    | joint_instr_op1 op1 acc_a ⇒
301      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph acc_a l in
302      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
303      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op1 … globals op1 it) l) in
304      let int_fun ≝ set_luniverse globals int_fun luniv in
305      let 〈l, graph, luniv〉 ≝ read globals int_fun graph acc_a (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
306        〈joint_st_goto ltl_params globals l, graph, luniv〉
307    | joint_instr_int r i ⇒
308      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph r l in
309        〈joint_st_sequential ltl_params globals (joint_instr_int … globals hdw i) l, graph, luniv〉
310    | joint_instr_opaccs opaccs acc_a_reg acc_b_reg ⇒
311      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph acc_a_reg l in
312      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
313      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_opaccs … globals opaccs it it) l) in
314      let luniv ≝ set_luniverse globals int_fun luniv in
315      let 〈l, graph, luniv〉 ≝ read globals int_fun graph acc_a_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
316      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterB)) l) in
317      let luniv ≝ set_luniverse globals int_fun luniv in
318      let 〈l, graph, luniv〉 ≝ read globals int_fun graph acc_b_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
319      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_goto … globals l) in
320      let luniv ≝ set_luniverse globals int_fun luniv in
321      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph acc_b_reg l in
322      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
323      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterB)) l) in
324      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_opaccs … globals opaccs it it) l) in
325      let luniv ≝ set_luniverse globals int_fun luniv in
326      let 〈l, graph, luniv〉 ≝ read globals int_fun graph acc_a_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
327      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterB)) l) in
328      let luniv ≝ set_luniverse globals int_fun luniv in
329      let 〈l, graph, luniv〉 ≝ read globals int_fun graph acc_b_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
330        〈joint_st_goto ltl_params globals l, graph, luniv〉
331    | joint_instr_move pair_regs ⇒
332      let regl ≝ \fst pair_regs in
333      let regr ≝ \snd pair_regs in
334      match regl with
335      [ pseudo p1  ⇒
336        match regr with
337        [ pseudo p2  ⇒ move globals int_fun graph (lookup p1) (lookup p2) l
338        | hardware h ⇒ move globals int_fun graph (lookup p1) (decision_colour h) l
339        ]
340      | hardware h1 ⇒
341        match regr with
342        [ pseudo p    ⇒ move globals int_fun graph (decision_colour h1) (lookup p) l
343        | hardware h2 ⇒
344          let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc h1)) l) in
345            〈joint_st_sequential ltl_params globals (joint_instr_move ltl_params globals (to_acc h2)) l, graph, luniv〉
346        ]
347      ]
348    | joint_instr_address lbl prf dpl dph ⇒
349      let 〈hdw1, l, graph, luniv〉 ≝ write globals int_fun graph dph l in
350      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw1)) l) in
351      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterDPH)) l) in
352      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_address … globals lbl prf it it) l) in
353      let int_fun ≝ set_luniverse globals int_fun luniv in
354      let 〈hdw2, l, graph, luniv〉 ≝ write globals int_fun graph dpl l in
355      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw2)) l) in
356      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterDPL)) l) in
357        〈joint_st_sequential ltl_params globals (joint_instr_address … globals lbl prf it it) l, graph, luniv〉
358    ]
359  | joint_st_return ⇒ 〈joint_st_return … globals, graph, ertl_if_luniverse globals int_fun〉
360  | joint_st_goto l ⇒ 〈joint_st_goto … globals l, graph, ertl_if_luniverse globals int_fun〉
361  | joint_st_extension ext ⇒
362    match ext with
363    [ ertl_st_ext_new_frame l ⇒ newframe globals int_fun graph l
364    | ertl_st_ext_del_frame l ⇒ delframe globals int_fun graph l
365    | ertl_st_ext_frame_size r l ⇒
366      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph r l in
367        〈joint_st_sequential … globals (joint_instr_int ltl_params globals hdw (bitvector_of_nat ? (stacksize globals int_fun))) l, graph, luniv〉
368    ]
369  ].
370
371definition translate_internal ≝
372  λglobals: list ident.
373  λf.
374  λint_fun: ertl_internal_function.
375  let lookup ≝ λr.
376    match lookup r with
377    | colour_spill ->
378        ERTLToLTLI.Spill (Interference.Vertex.Map.find (Interference.lookup H.graph r) S.coloring)
379    | colour_colour color ->
380        ERTLToLTLI.Color color
381  in
382  let locals ≝ colour_locals + (ertl_if_stacksize int_fun) in
383  let stacksize ≝ (ertl_if_params int_fun) + locals in
384    mk_ltl_internal_function
385      globals
386      (ertl_if_luniverse int_fun)
387      (ertl_if_runiverse int_fun)
388      stacksize.
389
390  let () =
391    Label.Map.iter (fun label stmt ->
392      let stmt =
393        match Liveness.eliminable (G.liveafter label) stmt with
394        | Some successor ->
395            LTL.St_skip successor
396        | None ->
397            I.translate_statement stmt
398      in
399      graph := Label.Map.add label stmt !graph
400    ) int_fun.ERTL.f_graph
401  in
402
403definition translate_funct ≝
404  λname_def.
405  let 〈name, def〉 ≝ name_def in
406  let def' ≝
407    match def with
408    [ Internal def ⇒ Internal ? (translate_internal name def)
409    | External def ⇒ External ? def
410    ]
411  in
412    〈name, def'〉.
413
414definition translate ≝
415  λp.
416  let functs' ≝ map ? ? translate_funct (ertl_pr_functs p) in
417    mk_ltl_program (ertl_pr_globals p) functs' (ertl_pr_main p).
Note: See TracBrowser for help on using the repository browser.