source: src/ERTL/ERTLToLTL.ma @ 1260

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

commit for csc

File size: 29.0 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 fresh_label ≝
51  λglobals: list ident.
52  λluniv.
53    fresh LabelTag luniv.
54
55definition ltl_statement_graph ≝
56  λglobals.
57    graph … (ltl_statement globals).
58
59definition add_graph ≝
60  λglobals.
61  λlabel.
62  λstmt: ltl_statement globals.
63  λgraph: ltl_statement_graph globals.
64    add LabelTag ? graph label stmt.
65
66definition generate ≝
67  λglobals: list ident.
68  λluniv.
69  λgraph: ltl_statement_graph globals.
70  λstmt: ltl_statement globals.
71  let 〈l, luniv〉 ≝ fresh_label globals luniv in
72  let graph ≝ add_graph globals l stmt graph in
73    〈l, graph, luniv〉.
74
75definition num_locals ≝
76  λglobals.
77  λint_fun.
78    colour_locals + (joint_if_stacksize globals (ertl_params globals) int_fun).
79
80definition stacksize ≝
81  λglobals.
82  λint_fun.
83    colour_locals + (joint_if_stacksize globals (ertl_params globals) int_fun).
84
85definition adjust_off ≝
86  λglobals.
87  λint_fun.
88  λoff.
89  let 〈ignore, int_off〉 ≝ half_add ? int_size off in
90  let 〈sub, ignore〉 ≝ sub_8_with_carry (bitvector_of_nat ? (num_locals globals int_fun)) int_off false in
91    sub.
92
93definition get_stack:
94 ∀globals. ertl_internal_function globals → graph (ltl_statement globals) → Register → Byte → label → ? ≝
95  λglobals: list ident.
96  λint_fun.
97  λgraph: graph (ltl_statement (globals)).
98  λr.
99  λoff.
100  λl.
101  λoriginal_label.
102    let off ≝ adjust_off globals int_fun off in
103    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
104    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc r)) l) in
105    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_load … globals it it it) l) in
106    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPH)) l) in
107    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Addc it it RegisterSPH) l) in
108    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_int … globals RegisterA (zero ?)) l) in
109    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPL)) l) in
110    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Add it it RegisterSPL) l) in
111      〈add_graph globals original_label (joint_st_sequential (ltl_params globals) globals (joint_instr_int … (ltl_params globals) globals RegisterA off) l) graph, luniv〉.
112
113definition set_stack:
114  ∀globals. ertl_internal_function globals → ltl_statement_graph globals → Byte
115    → Register → label → ? ≝
116  λglobals: list ident.
117  λint_fun.
118  λgraph: graph (ltl_statement (globals)).
119  λoff.
120  λr.
121  λl.
122  λoriginal_label.
123  let off ≝ adjust_off globals int_fun off in
124  let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
125  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_store … globals it it it) l) in
126  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc r)) l) in
127  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPH)) l) in
128  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Addc it it RegisterSPH) l) in
129  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_int … globals RegisterA (zero ?)) l) in
130  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPL)) l) in
131  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Add it it RegisterSPL) l) in
132    〈add_graph globals original_label (joint_st_sequential (ltl_params globals) globals (joint_instr_int … (ltl_params globals) globals RegisterA off) l) graph, luniv〉.
133
134
135definition write ≝
136  λglobals: list ident.
137  λint_fun: ertl_internal_function globals.
138  λvaluation.
139  λcoloured_graph.
140  λgraph.
141  λr.
142  λl.
143  λoriginal_label: label.
144  match colouring valuation coloured_graph (inl … r) with
145  [ decision_spill off ⇒
146    let luniv ≝ joint_if_luniverse … int_fun in
147    let 〈graph, luniv〉 ≝ set_stack globals int_fun graph (bitvector_of_nat … off) RegisterSST l original_label in
148      〈RegisterSST, l, graph, luniv〉
149  | decision_colour hwr ⇒
150    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
151      〈hwr, l, graph, luniv〉
152  ].
153
154definition read ≝
155  λglobals: list ident.
156  λint_fun: ertl_internal_function globals.
157  λvaluation.
158  λcoloured_graph.
159  λgraph.
160  λr.
161  λstmt.
162  λoriginal_label: label.
163  match colouring valuation coloured_graph (inl … r) with
164  [ decision_colour hwr ⇒
165    let luniv ≝ joint_if_luniverse … int_fun in
166      〈add_graph globals original_label (stmt hwr) graph, luniv〉
167  | decision_spill off ⇒
168    let temphwr ≝ RegisterSST in
169    let luniv ≝ joint_if_luniverse … int_fun in
170    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (stmt temphwr) in
171      get_stack globals int_fun graph temphwr (bitvector_of_nat … off) l original_label
172  ].
173
174definition move ≝
175  λglobals: list ident.
176  λint_fun.
177  λgraph: graph (ltl_statement globals).
178  λdest: decision.
179  λsrc: decision.
180  λl: label.
181  λoriginal_label.
182  match dest with
183  [ decision_colour dest_hwr ⇒
184    match src with
185    [ decision_colour src_hwr ⇒
186      let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
187      if eq_Register dest_hwr src_hwr then
188        〈add_graph globals original_label (joint_st_goto … globals l) graph, luniv〉
189      else
190        let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc dest_hwr)) l) in
191          〈add_graph globals original_label (joint_st_sequential (ltl_params globals) globals (joint_instr_move … globals (to_acc src_hwr)) l) graph, luniv〉
192    | decision_spill src_off ⇒ get_stack globals int_fun graph dest_hwr (bitvector_of_nat … src_off) l original_label
193    ]
194  | decision_spill dest_off ⇒
195    match src with
196    [ decision_colour src_hwr ⇒ set_stack globals int_fun graph (bitvector_of_nat … dest_off) src_hwr l original_label
197    | decision_spill src_off ⇒
198      let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
199      if eq_nat dest_off src_off then
200        〈add_graph globals original_label (joint_st_goto … globals l) graph, luniv〉
201      else
202        let temp_hwr ≝ RegisterSST in
203        let 〈graph, luniv〉 ≝ set_stack globals int_fun graph (bitvector_of_nat … dest_off) temp_hwr l original_label in
204          get_stack globals int_fun graph temp_hwr (bitvector_of_nat … src_off) l original_label
205    ]
206  ].
207
208definition newframe ≝
209  λglobals: list ident.
210  λint_fun: ertl_internal_function globals.
211  λgraph: ltl_statement_graph globals.
212  λl: label.
213  λoriginal_label: label.
214  if eq_nat (stacksize globals int_fun) 0 then
215    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
216      〈add_graph globals original_label (joint_st_goto … globals l) graph, luniv〉
217  else
218    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
219    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterSPH)) l) in
220    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Sub it it RegisterDPH) l) in
221    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_int … globals RegisterDPH (zero ?)) l) in
222    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterSPH)) l) in
223    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterSPL)) l) in
224    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Sub it it RegisterDPL) l) in
225    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_clear_carry … globals) l) in
226    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
227      〈add_graph globals original_label (joint_st_sequential (ltl_params globals) globals (joint_instr_move … globals (to_acc RegisterSPL)) l) graph, luniv〉.
228
229definition delframe ≝
230  λglobals.
231  λint_fun.
232  λgraph: graph (ltl_statement globals).
233  λl.
234  λoriginal_label: label.
235  if eq_nat (stacksize globals int_fun) 0 then
236    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
237      〈add_graph globals original_label (joint_st_goto (ltl_params globals) globals l) graph, luniv〉
238  else
239    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
240    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterSPH)) l) in
241    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Addc it it RegisterSPH) l) in
242    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_int … globals RegisterA (zero ?)) l) in
243    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterSPL)) l) in
244    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Add it it RegisterSPL) l) in
245      〈add_graph globals original_label (joint_st_sequential (ltl_params globals) globals (joint_instr_int … globals RegisterA (bitvector_of_nat ? (stacksize globals int_fun))) l) graph, luniv〉.
246
247definition translate_statement ≝
248  λglobals: list ident.
249  λint_fun.
250  λvaluation.
251  λcoloured_graph: coloured_graph valuation.
252  λgraph: ltl_statement_graph globals.
253  λstmt: ertl_statement globals.
254  λoriginal_label: label.
255  match stmt with
256  [ joint_st_sequential seq l ⇒
257    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
258    match seq with
259    [ joint_instr_comment c ⇒
260      〈add_graph globals original_label (joint_st_sequential (ltl_params globals) globals (joint_instr_comment … globals c) l) graph, luniv〉
261    | joint_instr_cost_label cost_lbl ⇒
262      〈add_graph globals original_label (joint_st_sequential … globals (joint_instr_cost_label … globals cost_lbl) l) graph, luniv〉
263    | joint_instr_pop r ⇒
264      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph r l in
265      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
266        〈add_graph globals original_label (joint_st_sequential (ltl_params globals) globals (joint_instr_pop … globals it) l) graph, luniv〉
267    | joint_instr_push r ⇒
268      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_push … globals it) l) in
269      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
270      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
271      let int_fun' ≝ set_luniverse globals ? int_fun luniv in
272      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph r (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l frees) in
273        〈add_graph globals original_label (joint_st_goto … globals l) graph, luniv〉
274    | _ ⇒ ?
275    ]
276  | _ ⇒ ?
277  ].
278    | joint_instr_cond srcr lbl_true ⇒
279      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_cond … globals it lbl_true) l) in
280      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv 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        〈add_graph globals original_label (joint_st_goto (ltl_params globals) globals l) graph, luniv〉
283    | joint_instr_call_id f ignore ⇒ 〈add_graph globals original_label (joint_st_sequential … globals (joint_instr_call_id … globals f ignore) l) graph, luniv〉
284    | joint_instr_store addr1 addr2 srcr ⇒
285      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_store … globals it it it) l) in
286      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterST1)) 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      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterST1)) l) in
296      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
297        〈add_graph globals original_label (joint_st_goto (ltl_params globals) globals l) graph, luniv〉
298    | joint_instr_load destr addr1 addr2 ⇒
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_load … globals it it it) l) in
302      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPH)) l) in
303      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterST0)) l) in
304      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPL)) l) in
305      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
306      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
307      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterST0)) l) in
308      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
309      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
310        〈add_graph globals original_label (joint_st_goto (ltl_params globals) globals l) graph, luniv〉
311    | joint_instr_clear_carry ⇒ 〈add_graph globals original_label (joint_st_sequential … globals (joint_instr_clear_carry … globals) l) graph, luniv〉
312    | joint_instr_set_carry ⇒ 〈add_graph globals original_label (joint_st_sequential … globals (joint_instr_set_carry … globals) l) graph, luniv〉
313    | joint_instr_op2 op2 destr srcr1 srcr2 ⇒
314      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph destr l in
315      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
316      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals op2 it it RegisterB) l) in
317      let luniv ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
318      let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr1 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
319      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterB)) l) in
320      let luniv ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
321      let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr2 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
322        〈add_graph globals original_label (joint_st_goto (ltl_params globals) globals l) graph, luniv〉
323    | joint_instr_op1 op1 destr srcr  ⇒
324      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph destr l in
325      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
326      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op1 … globals op1 it it) l) in
327      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
328      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
329        〈add_graph globals original_label (joint_st_goto (ltl_params globals) globals l) graph, luniv〉
330    | joint_instr_int r i ⇒
331      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph r l in
332        〈add_graph globals original_label (joint_st_sequential (ltl_params globals) globals (joint_instr_int … globals hdw i) l) graph, luniv〉
333    | joint_instr_opaccs opaccs acc_a_reg acc_b_reg ⇒
334      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph acc_a_reg l in
335      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
336      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_opaccs … globals opaccs it it) l) in
337      let luniv ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
338      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
339      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterB)) l) in
340      let luniv ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
341      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
342      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_goto … globals l) in
343      let luniv ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
344      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph acc_b_reg l in
345      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
346      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterB)) l) in
347      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_opaccs … globals opaccs it it) l) in
348      let luniv ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
349      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
350      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterB)) l) in
351      let luniv ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
352      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
353        〈add_graph globals original_label (joint_st_goto … globals l) graph, luniv〉
354    | joint_instr_move pair_regs ⇒
355      let regl ≝ \fst pair_regs in
356      let regr ≝ \snd pair_regs in
357      match regl with
358      [ pseudo p1  ⇒
359        match regr with
360        [ pseudo p2  ⇒ move globals int_fun graph (colouring valuation coloured_graph (inl … p1)) (colouring valuation coloured_graph (inl … p2)) l original_label
361        | hardware h ⇒ move globals int_fun graph (colouring valuation coloured_graph (inl … p1)) (decision_colour h) l original_label
362        ]
363      | hardware h1 ⇒
364        match regr with
365        [ pseudo p    ⇒ move globals int_fun graph (decision_colour h1) (colouring valuation coloured_graph (inl … p)) l original_label
366        | hardware h2 ⇒
367          let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc h1)) l) in
368            〈add_graph globals original_label (joint_st_sequential (ltl_params globals) globals (joint_instr_move (ltl_params globals) globals (to_acc h2)) l) graph, luniv〉
369        ]
370      ]
371      | _ ⇒ ?
372    ]
373  | _ ⇒ ?
374  ].
375   
376    | joint_instr_address lbl prf dpl dph ⇒
377      let 〈hdw1, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph dph l in
378      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw1)) l) in
379      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterDPH)) l) in
380      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_address … globals lbl prf it it) l) in
381      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
382      let 〈hdw2, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph dpl l in
383      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw2)) l) in
384      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterDPL)) l) in
385        〈joint_st_sequential (ltl_params globals) globals (joint_instr_address … globals lbl prf it it) l, graph, luniv〉
386    | joint_instr_extension ext ⇒
387      match ext with
388      [ ertl_st_ext_new_frame ⇒ newframe globals int_fun graph l
389      | ertl_st_ext_del_frame ⇒ delframe globals int_fun graph l
390      | ertl_st_ext_frame_size r ⇒
391        let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph r l in
392          〈joint_st_sequential (ltl_params globals) globals (joint_instr_int … globals hdw (bitvector_of_nat ? (stacksize globals int_fun))) l, graph, luniv〉
393      ]
394    ]
395  | joint_st_return ⇒ 〈joint_st_return … globals, graph, joint_if_luniverse globals (ertl_params globals) int_fun〉
396  | joint_st_goto l ⇒ 〈joint_st_goto … globals l, graph, joint_if_luniverse globals (ertl_params globals) int_fun〉
397  ].
398
399lemma Sm_leq_n_m_leq_n:
400  ∀m, n: nat.
401    S m ≤ n → m ≤ n.
402  #m #n /2/
403qed.
404
405let rec mapi_aux
406  (a: Type[0]) (b: Type[0]) (f: BitVector 16 → a → b) (n: nat)
407    on n: n ≤ 16 → BitVectorTrie a n → BitVector (16 - n) → BitVectorTrie b n ≝
408  match n return λn: nat. n ≤ 16 → BitVectorTrie a n → BitVector (16 - n) → BitVectorTrie b n with
409  [ O ⇒ λinvariant. λtrie: BitVectorTrie a 0. λaccu: BitVector 16.
410    match trie return λx: nat. λtrie: BitVectorTrie a x. ∀prf: x = 0. BitVectorTrie b x with
411    [ Leaf l ⇒ λprf. Leaf … (f accu l)
412    | Stub s ⇒ λprf. Stub … s
413    | Node n' l r ⇒ λabsrd. ⊥
414    ] (refl … 0)
415  | S n' ⇒ λinvariant. λtrie: BitVectorTrie a (S n'). λaccu: BitVector (16 - (S n')).
416    match trie return λx: nat. λtrie: BitVectorTrie a x. ∀prf: x = S n'. BitVectorTrie b x with
417    [ Leaf l ⇒ λabsrd. ⊥
418    | Stub s ⇒ λprf. Stub … s
419    | Node n'' l r ⇒ λprf.
420      Node ? n'' ? ?
421    ] (refl nat (S n'))
422  ].
423  [ 1,2: destruct(absrd)
424  | 3  : destruct(prf)
425         @(mapi_aux a b f n' ? l ((false ::: accu)⌈S (16 - S n') ↦ 16 - n'⌉))
426         [ 1: @Sm_leq_n_m_leq_n
427              assumption
428         | 2: <minus_Sn_m
429              [ 1: >minus_S_S %
430              | 2: assumption
431              ]
432         ]
433  | 4  : destruct(prf)
434         @(mapi_aux a b f n' ? r ((true ::: accu)⌈S (16 - S n') ↦ 16 - n'⌉))
435         [ 1: @Sm_leq_n_m_leq_n
436              assumption
437         | 2: <minus_Sn_m
438              [ 1: >minus_S_S %
439              | 2: assumption
440              ]
441         ]
442  ]
443qed.
444
445definition mapi ≝
446  λa, b: Type[0].
447  λf: label → a → b.
448  λtrie: BitVectorTrie a 16.
449    let f' ≝ λbv: BitVector 16. λa.
450      f (an_identifier LabelTag bv) a
451    in
452      mapi_aux a b f' 16 ? trie [[]].
453  //
454qed.
455 
456definition translate_internal ≝
457  λglobals.
458  λint_fun.
459  let graph ≝ ((empty_map …) : ltl_statement_graph globals) in
460  let valuation ≝ analyse globals int_fun in
461  let coloured_graph ≝ build valuation in
462  let liveafter ≝ analyse globals int_fun in
463  let blah ≝ mapi … (λlabel. λstmt_graph_luniv.
464    let stmt ≝
465      match eliminable globals (liveafter label) stmt with
466      [ Some successor ⇒ 〈joint_st_goto … successor, graph, joint_if_luniverse … int_fun〉
467      | None           ⇒ translate_statement globals int_fun valuation coloured_graph graph stmt
468      ]
469    in
470      ?) (joint_if_code … int_fun)
471  in ?.
472 
473 
474 
475      let stmt =
476        match Liveness.eliminable (G.liveafter label) stmt with
477        | Some successor ->
478            LTL.St_skip successor
479        | None ->
480            I.translate_statement stmt
481      in
482      graph := Label.Map.add label stmt !graph
483    ) int_fun.ERTL.f_graph
484
485definition translate_funct ≝
486  λname_def.
487  let 〈name, def〉 ≝ name_def in
488  let def' ≝
489    match def with
490    [ Internal def ⇒ Internal ? (translate_internal name def)
491    | External def ⇒ External ? def
492    ]
493  in
494    〈name, def'〉.
495
496definition translate ≝
497  λp.
498  let functs' ≝ map ? ? translate_funct (ertl_pr_functs p) in
499    mk_ltl_program (ertl_pr_globals p) functs' (ertl_pr_main p).
Note: See TracBrowser for help on using the repository browser.