source: src/ERTL/ERTLToLTL.ma @ 1192

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

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