source: src/ERTL/ERTLToLTL.ma @ 1191

Last change on this file since 1191 was 1191, checked in by mulligan, 10 years ago

ertl to ertl pass back where it was before the changes to joint

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