source: src/ERTL/ERTLToLTL.ma @ 1179

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

changes to ertl, ltl and lin to use new notion of joint params. ertl to ltl pass in process of being changed
File size: 25.7 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    | _ ⇒ ?
297    ]
298  | joint_st_return ⇒ 〈joint_st_return … globals, graph, ertl_if_luniverse globals int_fun〉
299  | joint_st_goto l ⇒ 〈joint_st_goto … globals l, graph, ertl_if_luniverse globals int_fun〉
300  | joint_st_extension ext ⇒
301    match ext with
302    [ ertl_st_ext_new_frame l ⇒ newframe globals int_fun graph l
303    | ertl_st_ext_del_frame l ⇒ delframe globals int_fun graph l
304    | ertl_st_ext_frame_size r l ⇒
305      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph r l in
306        〈joint_st_sequential … globals (joint_instr_int ltl_params globals hdw (bitvector_of_nat ? (stacksize globals int_fun))) l, graph, luniv〉
307    ]
308  ].
309 
310  match stmt with
311  | ertl_st_get_hdw destr sourcehwr l ⇒ move int_fun globals graph (lookup destr) (decision_colour sourcehwr) l
312  | ertl_st_set_hdw desthwr srcr l ⇒ move int_fun globals graph (decision_colour desthwr) (lookup srcr) l
313  | ertl_st_hdw_to_hdw r1 r2 l ⇒
314    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals r1) l) in
315      〈joint_st_sequential ? globals (joint_instr_to_acc globals r2) l, graph〉
316  | ertl_st_addr rl rh x l ⇒
317    let 〈hdw1, l〉 ≝ write int_fun globals graph rh l in
318    let 〈l, graph〉 ≝ l in
319    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw1) l) in
320    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPH) l) in
321    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_address globals x ?) l) in
322    let 〈hdw2, l〉 ≝ write int_fun globals graph rl l in
323    let 〈l, graph〉 ≝ l in
324    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw2) l) in
325    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPL) l) in
326      〈joint_st_sequential ? globals (joint_instr_address globals x ?) l, graph〉
327(*  | ertl_st_addr_h r x l ⇒
328    let 〈hdw, l〉 ≝ write int_fun globals graph r l in
329    let 〈l, graph〉 ≝ generate globals graph (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l)) in
330    let 〈l, graph〉 ≝ generate globals graph (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPH) l)) in
331      ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_address globals x ?) l)
332  | ertl_st_addr_l r x l ⇒
333    let 〈hdw, l〉 ≝ write int_fun globals graph r l in
334    let 〈l, graph〉 ≝ generate globals graph (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l)) in
335    let 〈l, graph〉 ≝ generate globals graph (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPL) l)) in
336      ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_address globals x ?) l)
337*)
338  | ertl_st_move r1 r2 l ⇒ move int_fun globals graph (lookup r1) (lookup r2) l
339(*
340  | ertl_st_opaccs_a opaccs destr srcr1 srcr2 l ⇒
341    let 〈hdw, l〉 ≝ write int_fun globals graph destr l in
342    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
343    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l) in
344    let 〈l, graph〉 ≝ read int_fun globals graph srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
345    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
346    let 〈l, graph〉 ≝ read int_fun globals graph srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
347      joint_st_goto ? globals l
348  | ertl_st_opaccs_b opaccs destr srcr1 srcr2 l ⇒
349    let 〈hdw, l〉 ≝ write int_fun globals graph destr l in
350    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
351    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterB) l) in
352    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l) in
353    let 〈l, graph〉 ≝ read int_fun globals graph srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
354    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
355    let 〈l, graph〉 ≝ read int_fun globals graph srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
356      joint_st_goto ? globals l
357*)
358  ].
359  cases daemon (* XXX: todo -- proofs regarding gvars *)
360qed.
361
362(* **** *)
363
364definition translate_internal ≝
365  λglobals: list ident.
366  λf.
367  λint_fun: ertl_internal_function.
368  let lookup ≝ λr.
369    match lookup r with
370    | colour_spill ->
371        ERTLToLTLI.Spill (Interference.Vertex.Map.find (Interference.lookup H.graph r) S.coloring)
372    | colour_colour color ->
373        ERTLToLTLI.Color color
374  in
375  let locals ≝ colour_locals + (ertl_if_stacksize int_fun) in
376  let stacksize ≝ (ertl_if_params int_fun) + locals in
377    mk_ltl_internal_function
378      globals
379      (ertl_if_luniverse int_fun)
380      (ertl_if_runiverse int_fun)
381      stacksize.
382
383  let () =
384    Label.Map.iter (fun label stmt ->
385      let stmt =
386        match Liveness.eliminable (G.liveafter label) stmt with
387        | Some successor ->
388            LTL.St_skip successor
389        | None ->
390            I.translate_statement stmt
391      in
392      graph := Label.Map.add label stmt !graph
393    ) int_fun.ERTL.f_graph
394  in
395
396definition translate_funct ≝
397  λname_def.
398  let 〈name, def〉 ≝ name_def in
399  let def' ≝
400    match def with
401    [ Internal def ⇒ Internal ? (translate_internal name def)
402    | External def ⇒ External ? def
403    ]
404  in
405    〈name, def'〉.
406
407definition translate ≝
408  λp.
409  let functs' ≝ map ? ? translate_funct (ertl_pr_functs p) in
410    mk_ltl_program (ertl_pr_globals p) functs' (ertl_pr_main p).
Note: See TracBrowser for help on using the repository browser.