source: src/ERTL/ERTLToLTL.ma @ 1172

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

ertltoltl.ma half complete

File size: 23.8 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 label unit 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 label unit ltl_params globals (joint_instr_move … globals (from_acc RegisterSPH)) l) in
173    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential label unit ltl_params globals (joint_instr_op2 … globals Sub it RegisterDPH) l) in
174    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential label unit ltl_params globals (joint_instr_int … globals RegisterDPH (zero ?)) l) in
175    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential label unit ltl_params globals (joint_instr_move … globals (to_acc RegisterSPH)) l) in
176    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential label unit ltl_params globals (joint_instr_move … globals (from_acc RegisterSPL)) l) in
177    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential label unit ltl_params globals (joint_instr_op2 … globals Sub it RegisterDPL) l) in
178    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential label unit ltl_params globals (joint_instr_clear_carry … globals) l) in
179    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential label unit ltl_params globals (joint_instr_int … globals RegisterDPL (bitvector_of_nat ? (stacksize globals int_fun))) l) in
180      〈joint_st_sequential label unit 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 … 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 … globals (joint_instr_move … globals (from_acc RegisterSPH)) l) in
192    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Addc it RegisterSPH) l) in
193    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_int … globals RegisterA (zero ?)) l) in
194    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterSPL)) l) in
195    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Add it RegisterSPL) l) in
196      〈joint_st_sequential label unit 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  [ ertl_st_lift_pre pre ⇒
205    match pre with
206    [ joint_st_sequential seq l ⇒
207      match seq with
208      [ joint_instr_comment c ⇒ 〈joint_st_sequential ? globals (joint_instr_comment globals s) l, graph〉
209      | _ ⇒ ?
210      ]
211    | joint_st_return ⇒ 〈joint_st_return … globals, graph, ertl_if_luniverse globals int_fun〉
212    | joint_st_goto l ⇒ 〈joint_st_goto … globals l, graph, ertl_if_luniverse globals int_fun〉
213    ]
214  | ertl_st_new_frame l ⇒ newframe globals int_fun graph l
215  | ertl_st_del_frame l ⇒ delframe globals int_fun graph l
216  | ertl_st_frame_size r l ⇒
217    let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph r l in
218      〈joint_st_sequential … globals (joint_instr_int ltl_params … globals hdw (bitvector_of_nat ? (stacksize globals int_fun))) l, graph, luniv〉
219  ].
220 
221  match stmt with
222  | ertl_st_comment s l ⇒
223  | ertl_st_cost cost_lbl l ⇒ 〈joint_st_sequential ? globals (joint_instr_cost_label globals cost_lbl) l, graph〉
224  | ertl_st_get_hdw destr sourcehwr l ⇒ move int_fun globals graph (lookup destr) (decision_colour sourcehwr) l
225  | ertl_st_set_hdw desthwr srcr l ⇒ move int_fun globals graph (decision_colour desthwr) (lookup srcr) l
226  | ertl_st_hdw_to_hdw r1 r2 l ⇒
227    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals r1) l) in
228      〈joint_st_sequential ? globals (joint_instr_to_acc globals r2) l, graph〉
229  | ertl_st_new_frame l ⇒
230  | ertl_st_del_frame l ⇒
231  | ertl_st_frame_size r l ⇒
232  | ertl_st_pop r l ⇒
233    let 〈hdw, l〉 ≝ write int_fun globals graph r l in
234    let 〈l, graph〉 ≝ l in
235    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
236      〈joint_st_sequential ? globals (joint_instr_pop globals) l, graph〉
237  | ertl_st_push r l ⇒
238    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_push globals) l) in
239    let 〈l, graph〉 ≝ read int_fun globals graph r (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
240      〈joint_st_goto ? globals l, graph〉
241  | ertl_st_addr rl rh x l ⇒
242    let 〈hdw1, l〉 ≝ write int_fun globals graph rh l in
243    let 〈l, graph〉 ≝ l in
244    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw1) l) in
245    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPH) l) in
246    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_address globals x ?) l) in
247    let 〈hdw2, l〉 ≝ write int_fun globals graph rl l in
248    let 〈l, graph〉 ≝ l in
249    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw2) l) in
250    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPL) l) in
251      〈joint_st_sequential ? globals (joint_instr_address globals x ?) l, graph〉
252(*  | ertl_st_addr_h r x l ⇒
253    let 〈hdw, l〉 ≝ write int_fun globals graph r l in
254    let 〈l, graph〉 ≝ generate globals graph (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l)) in
255    let 〈l, graph〉 ≝ generate globals graph (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPH) l)) in
256      ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_address globals x ?) l)
257  | ertl_st_addr_l r x l ⇒
258    let 〈hdw, l〉 ≝ write int_fun globals graph r l in
259    let 〈l, graph〉 ≝ generate globals graph (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l)) in
260    let 〈l, graph〉 ≝ generate globals graph (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPL) l)) in
261      ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_address globals x ?) l)
262*)
263  | ertl_st_int r i l ⇒
264    let 〈hdw, l〉 ≝ write int_fun globals graph r l in
265    let 〈l, graph〉 ≝ l in
266      〈joint_st_sequential ? globals (joint_instr_int globals hdw i) l, graph〉
267  | ertl_st_move r1 r2 l ⇒ move int_fun globals graph (lookup r1) (lookup r2) l
268  | ertl_st_opaccs opaccs destr1 destr2 srcr1 srcr2 l ⇒
269    let 〈hdw, l〉 ≝ write int_fun globals graph destr1 l in
270    let 〈l, graph〉 ≝ l in
271    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
272    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l) in
273    let 〈l, graph〉 ≝ read int_fun globals graph srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
274    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
275    let 〈l, graph〉 ≝ read int_fun globals graph srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
276    let 〈l, graph〉 ≝ generate globals graph (joint_st_goto ? globals l) in
277    let 〈hdw, l〉 ≝ write int_fun globals graph destr2 l in
278    let 〈l, graph〉 ≝ l in
279    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
280    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterB) l) in
281    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l) in
282    let 〈l, graph〉 ≝ read int_fun globals graph srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
283    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
284    let 〈l, graph〉 ≝ read int_fun globals graph srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
285      〈joint_st_goto ? globals l, graph〉
286(*
287  | ertl_st_opaccs_a opaccs destr srcr1 srcr2 l ⇒
288    let 〈hdw, l〉 ≝ write int_fun globals graph destr l in
289    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
290    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l) in
291    let 〈l, graph〉 ≝ read int_fun globals graph srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
292    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
293    let 〈l, graph〉 ≝ read int_fun globals graph srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
294      joint_st_goto ? globals l
295  | ertl_st_opaccs_b opaccs destr srcr1 srcr2 l ⇒
296    let 〈hdw, l〉 ≝ write int_fun globals graph destr l in
297    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
298    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterB) l) in
299    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l) in
300    let 〈l, graph〉 ≝ read int_fun globals graph srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
301    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
302    let 〈l, graph〉 ≝ read int_fun globals graph srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
303      joint_st_goto ? globals l
304*)
305  | ertl_st_op1 op1 destr srcr l ⇒
306    let 〈hdw, l〉 ≝ write int_fun globals graph destr l in
307    let 〈l, graph〉 ≝ l in
308    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
309    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_op1 globals op1) l) in
310    let 〈l, graph〉 ≝ read int_fun globals graph srcr (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
311      〈joint_st_goto ? globals l, graph〉
312  | ertl_st_op2 op2 destr srcr1 srcr2 l ⇒
313    let 〈hdw, l〉 ≝ write int_fun globals graph destr l in
314    let 〈l, graph〉 ≝ l in
315    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
316    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_op2 globals op2 RegisterB) l) in
317    let 〈l, graph〉 ≝ read int_fun globals graph srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
318    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
319    let 〈l, graph〉 ≝ read int_fun globals graph srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
320      〈joint_st_goto ? globals l, graph〉
321  | ertl_st_clear_carry l ⇒ 〈joint_st_sequential ? globals (joint_instr_clear_carry globals) l, graph〉
322  | ertl_st_set_carry l ⇒ 〈joint_st_sequential ? globals (joint_instr_set_carry globals) l, graph〉
323  | ertl_st_load destr addr1 addr2 l ⇒
324    let 〈hdw, l〉 ≝ write int_fun globals graph destr l in
325    let 〈l, graph〉 ≝ l in
326    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
327    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_load globals) l) in
328    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in
329    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterST0) l) in
330    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in
331    let 〈l, graph〉 ≝ read int_fun globals graph addr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
332    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterST0) l) in
333    let 〈l, graph〉 ≝ read int_fun globals graph addr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
334      〈joint_st_goto ? globals l, graph〉
335  | ertl_st_store addr1 addr2 srcr l ⇒
336    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_store globals) l) in
337    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterST1) l) in
338    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in
339    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterST0) l) in
340    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in
341    let 〈l, graph〉 ≝ read int_fun globals graph addr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
342    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterST0) l) in
343    let 〈l, graph〉 ≝ read int_fun globals graph addr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
344    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterST1) l) in
345    let 〈l, graph〉 ≝ read int_fun globals graph srcr (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
346      〈joint_st_goto ? globals l, graph〉
347  | ertl_st_call_id f ignore l ⇒ 〈joint_st_sequential ? globals (joint_instr_call_id globals f) l, graph〉
348  | ertl_st_cond srcr lbl_true lbl_false ⇒
349    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_cond_acc globals lbl_true) lbl_false) in
350    let 〈l, graph〉 ≝ read int_fun globals graph srcr (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
351      〈joint_st_goto ? globals l, graph〉
352  ].
353  cases daemon (* XXX: todo -- proofs regarding gvars *)
354qed.
355
356(* **** *)
357
358definition translate_internal ≝
359  λglobals: list ident.
360  λf.
361  λint_fun: ertl_internal_function.
362  let lookup ≝ λr.
363    match lookup r with
364    | colour_spill ->
365        ERTLToLTLI.Spill (Interference.Vertex.Map.find (Interference.lookup H.graph r) S.coloring)
366    | colour_colour color ->
367        ERTLToLTLI.Color color
368  in
369  let locals ≝ colour_locals + (ertl_if_stacksize int_fun) in
370  let stacksize ≝ (ertl_if_params int_fun) + locals in
371    mk_ltl_internal_function
372      globals
373      (ertl_if_luniverse int_fun)
374      (ertl_if_runiverse int_fun)
375      stacksize.
376
377  let () =
378    Label.Map.iter (fun label stmt ->
379      let stmt =
380        match Liveness.eliminable (G.liveafter label) stmt with
381        | Some successor ->
382            LTL.St_skip successor
383        | None ->
384            I.translate_statement stmt
385      in
386      graph := Label.Map.add label stmt !graph
387    ) int_fun.ERTL.f_graph
388  in
389
390definition translate_funct ≝
391  λname_def.
392  let 〈name, def〉 ≝ name_def in
393  let def' ≝
394    match def with
395    [ Internal def ⇒ Internal ? (translate_internal name def)
396    | External def ⇒ External ? def
397    ]
398  in
399    〈name, def'〉.
400
401definition translate ≝
402  λp.
403  let functs' ≝ map ? ? translate_funct (ertl_pr_functs p) in
404    mk_ltl_program (ertl_pr_globals p) functs' (ertl_pr_main p).
Note: See TracBrowser for help on using the repository browser.