source: src/ERTL/ERTLToLTL.ma @ 1250

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