source: src/ERTL/ERTLToLTL.ma @ 1263

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

changes

File size: 31.7 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: 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. ertl_internal_function globals → ∀v: valuation.
249    coloured_graph v → ltl_statement_graph globals → ertl_statement globals →
250      label → ((ltl_statement_graph globals) × (universe LabelTag)) ≝
251  λglobals: list ident.
252  λint_fun.
253  λvaluation.
254  λcoloured_graph: coloured_graph valuation.
255  λgraph: ltl_statement_graph globals.
256  λstmt: ertl_statement globals.
257  λoriginal_label: label.
258  match stmt with
259  [ joint_st_sequential seq l ⇒
260    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
261    match seq with
262    [ joint_instr_comment c ⇒
263      〈add_graph globals original_label (joint_st_sequential … (joint_instr_comment … c) l) graph, luniv〉
264    | joint_instr_cost_label cost_lbl ⇒
265      〈add_graph globals original_label (joint_st_sequential … (joint_instr_cost_label … cost_lbl) l) graph, luniv〉
266    | joint_instr_pop r ⇒
267      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
268      let int_fun ≝ set_luniverse globals ? int_fun luniv in
269      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph r l fresh_lbl in
270      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc hdw)) l) in
271        〈add_graph globals original_label (joint_st_sequential ltl_params_ globals (joint_instr_pop … it) l) graph, luniv〉
272    | joint_instr_push r ⇒
273      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_push … it) l) in
274      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
275      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
276      let int_fun ≝ set_luniverse globals ? int_fun luniv in
277      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph r (λhdw. joint_st_sequential … (joint_instr_move … (to_acc hdw)) l) fresh_lbl in
278        〈add_graph globals original_label (joint_st_goto … fresh_lbl) graph, luniv〉
279    | joint_instr_cond srcr lbl_true ⇒
280      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_cond … it lbl_true) l) in
281      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
282      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
283      let int_fun' ≝ set_luniverse globals ? int_fun luniv in
284      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr (λhdw. joint_st_sequential … (joint_instr_move … (to_acc hdw)) l) fresh_lbl in
285        〈add_graph globals original_label (joint_st_goto … fresh_lbl) graph, luniv〉
286    | joint_instr_call_id f ignore ⇒ 〈add_graph globals original_label (joint_st_sequential … (joint_instr_call_id … f ignore) l) graph, luniv〉
287    | joint_instr_store addr1 addr2 srcr ⇒
288      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_store … it it it) l) in
289      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (to_acc RegisterST1)) l) in
290      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc RegisterDPH)) l) in
291      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (to_acc RegisterST0)) l) in
292      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc RegisterDPL)) l) in
293      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
294      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
295      let int_fun ≝ set_luniverse globals ? int_fun luniv in
296      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr1 (λhdw. joint_st_sequential … (joint_instr_move … (to_acc hdw)) l) fresh_lbl in
297      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc RegisterST0)) fresh_lbl) in
298      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
299      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
300      let int_fun ≝ set_luniverse globals ? int_fun luniv in
301      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr2 (λhdw. joint_st_sequential … (joint_instr_move … (to_acc hdw)) l) fresh_lbl in
302      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc RegisterST1)) fresh_lbl) in
303      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
304      let int_fun ≝ set_luniverse globals ? int_fun luniv in
305      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr (λhdw. joint_st_sequential … (joint_instr_move … (to_acc hdw)) l) fresh_lbl in
306        〈add_graph globals original_label (joint_st_goto … l) graph, luniv〉
307    | joint_instr_load destr addr1 addr2 ⇒
308      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
309      let int_fun ≝ set_luniverse globals ? int_fun luniv in
310      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph destr l fresh_lbl in
311      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc hdw)) l) in
312      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_load … it it it) l) in
313      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc RegisterDPH)) l) in
314      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (to_acc RegisterST0)) l) in
315      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc RegisterDPL)) l) in
316      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
317      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
318      let int_fun ≝ set_luniverse globals ? int_fun luniv in
319      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr1 (λhdw. joint_st_sequential … (joint_instr_move … (to_acc hdw)) l) fresh_lbl in
320      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc RegisterST0)) fresh_lbl) in
321      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
322      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
323      let int_fun ≝ set_luniverse globals ? int_fun luniv in
324      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr2 (λhdw. joint_st_sequential … (joint_instr_move … (to_acc hdw)) l) fresh_lbl in
325        〈add_graph globals original_label (joint_st_goto … fresh_lbl) graph, luniv〉
326    | joint_instr_clear_carry ⇒ 〈add_graph globals original_label (joint_st_sequential … (joint_instr_clear_carry …) l) graph, luniv〉
327    | joint_instr_set_carry ⇒ 〈add_graph globals original_label (joint_st_sequential … (joint_instr_set_carry …) l) graph, luniv〉
328    | joint_instr_op2 op2 destr srcr1 srcr2 ⇒
329      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
330      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
331      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph destr l fresh_lbl in
332      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc hdw)) l) in
333      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_op2 … op2 it it RegisterB) l) in
334      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
335      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
336      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr1 (λhdw. joint_st_sequential … (joint_instr_move … (to_acc hdw)) l) fresh_lbl in
337      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc RegisterB)) fresh_lbl) in
338      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
339      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
340      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr2 (λhdw. joint_st_sequential … (joint_instr_move … (to_acc hdw)) l) fresh_lbl in
341        〈add_graph globals original_label (joint_st_goto … l) graph, luniv〉
342    | joint_instr_op1 op1 destr srcr ⇒
343      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
344      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
345      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph destr l fresh_lbl in
346      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc hdw)) l) in
347      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_op1 … op1 it it) l) in
348      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
349      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
350      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
351      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr (λhdw. joint_st_sequential … (joint_instr_move … (to_acc hdw)) l) fresh_lbl in
352        〈add_graph globals original_label (joint_st_goto … l) graph, luniv〉
353    | joint_instr_int r i ⇒
354      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
355      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
356      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph r l fresh_lbl in
357        〈add_graph globals original_label (joint_st_sequential ltl_params_ globals (joint_instr_int … hdw i) l) graph, luniv〉
358    | joint_instr_move pair_regs ⇒
359      let regl ≝ \fst pair_regs in
360      let regr ≝ \snd pair_regs in
361      match regl with
362      [ pseudo p1  ⇒
363        match regr with
364        [ pseudo p2  ⇒ move globals int_fun graph (colouring valuation coloured_graph (inl … p1)) (colouring valuation coloured_graph (inl … p2)) l original_label
365        | hardware h ⇒ move globals int_fun graph (colouring valuation coloured_graph (inl … p1)) (decision_colour h) l original_label
366        ]
367      | hardware h1 ⇒
368        match regr with
369        [ pseudo p    ⇒ move globals int_fun graph (decision_colour h1) (colouring valuation coloured_graph (inl … p)) l original_label
370        | hardware h2 ⇒
371          let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc h1)) l) in
372            〈add_graph globals original_label (joint_st_sequential ltl_params_ … (joint_instr_move … (to_acc h2)) l) graph, luniv〉
373        ]
374      ]
375    | joint_instr_address lbl prf dpl dph ⇒
376      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
377      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
378      let 〈hdw1, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph dph l fresh_lbl in
379      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw1)) l) in
380      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterDPH)) l) in
381      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_address … globals lbl prf it it) l) in
382      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
383      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
384      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
385      let 〈hdw2, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph dpl l fresh_lbl in
386      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw2)) l) in
387      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterDPL)) l) in
388        〈add_graph globals original_label (joint_st_sequential ltl_params_ globals (joint_instr_address … lbl prf it it) l) graph, luniv〉
389    | joint_instr_extension ext ⇒
390      match ext with
391      [ ertl_st_ext_new_frame ⇒ newframe globals int_fun graph l original_label
392      | ertl_st_ext_del_frame ⇒ delframe globals int_fun graph l original_label
393      | ertl_st_ext_frame_size r ⇒
394        let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
395        let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
396        let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph r l fresh_lbl in
397          〈add_graph globals original_label (joint_st_sequential ltl_params_ globals (joint_instr_int … hdw (bitvector_of_nat … (stacksize … int_fun))) l) graph, luniv〉
398      ]
399    | joint_instr_opaccs opaccs acc_a_reg acc_b_reg ⇒
400      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
401      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
402      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph acc_a_reg l fresh_lbl in
403      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc hdw)) l) in
404      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_opaccs … opaccs it it) l) in
405      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
406      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
407      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
408      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph acc_a_reg (λhdw. joint_st_sequential … (joint_instr_move … (to_acc hdw)) l) fresh_lbl in
409      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc RegisterB)) fresh_lbl) in
410      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
411      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
412      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
413      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph acc_b_reg (λhdw. joint_st_sequential … (joint_instr_move … (to_acc hdw)) l) fresh_lbl in
414      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_goto … fresh_lbl) in
415      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
416      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
417      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
418      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph acc_b_reg l fresh_lbl in
419      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc hdw)) l) in
420      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (to_acc RegisterB)) l) in
421      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_opaccs … opaccs it it) l) in
422      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
423      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
424      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
425      let 〈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) fresh_lbl in
426      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterB)) fresh_lbl) in
427      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
428      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
429      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
430      let 〈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) fresh_lbl in
431        〈add_graph globals original_label (joint_st_goto … globals fresh_lbl) graph, luniv〉
432    ]
433  | joint_st_return ⇒ 〈add_graph globals original_label (joint_st_return ltl_params_ globals) graph, joint_if_luniverse globals (ertl_params globals) int_fun〉
434  | joint_st_goto l ⇒ 〈add_graph globals original_label (joint_st_goto ltl_params_ globals l) graph, joint_if_luniverse globals (ertl_params globals) int_fun〉
435  ].
436
437lemma Sm_leq_n_m_leq_n:
438  ∀m, n: nat.
439    S m ≤ n → m ≤ n.
440  #m #n /2/
441qed.
442
443let rec mapi_aux
444  (a: Type[0]) (b: Type[0]) (f: BitVector 16 → a → b) (n: nat)
445    on n: n ≤ 16 → BitVectorTrie a n → BitVector (16 - n) → BitVectorTrie b n ≝
446  match n return λn: nat. n ≤ 16 → BitVectorTrie a n → BitVector (16 - n) → BitVectorTrie b n with
447  [ O ⇒ λinvariant. λtrie: BitVectorTrie a 0. λaccu: BitVector 16.
448    match trie return λx: nat. λtrie: BitVectorTrie a x. ∀prf: x = 0. BitVectorTrie b x with
449    [ Leaf l ⇒ λprf. Leaf … (f accu l)
450    | Stub s ⇒ λprf. Stub … s
451    | Node n' l r ⇒ λabsrd. ⊥
452    ] (refl … 0)
453  | S n' ⇒ λinvariant. λtrie: BitVectorTrie a (S n'). λaccu: BitVector (16 - (S n')).
454    match trie return λx: nat. λtrie: BitVectorTrie a x. ∀prf: x = S n'. BitVectorTrie b x with
455    [ Leaf l ⇒ λabsrd. ⊥
456    | Stub s ⇒ λprf. Stub … s
457    | Node n'' l r ⇒ λprf.
458      Node ? n'' ? ?
459    ] (refl nat (S n'))
460  ].
461  [ 1,2: destruct(absrd)
462  | 3  : destruct(prf)
463         @(mapi_aux a b f n' ? l ((false ::: accu)⌈S (16 - S n') ↦ 16 - n'⌉))
464         [ 1: @Sm_leq_n_m_leq_n
465              assumption
466         | 2: <minus_Sn_m
467              [ 1: >minus_S_S %
468              | 2: assumption
469              ]
470         ]
471  | 4  : destruct(prf)
472         @(mapi_aux a b f n' ? r ((true ::: accu)⌈S (16 - S n') ↦ 16 - n'⌉))
473         [ 1: @Sm_leq_n_m_leq_n
474              assumption
475         | 2: <minus_Sn_m
476              [ 1: >minus_S_S %
477              | 2: assumption
478              ]
479         ]
480  ]
481qed.
482
483definition mapi ≝
484  λa, b: Type[0].
485  λf: label → a → b.
486  λtrie: BitVectorTrie a 16.
487    let f' ≝ λbv: BitVector 16. λa.
488      f (an_identifier LabelTag bv) a
489    in
490      mapi_aux a b f' 16 ? trie [[]].
491  //
492qed.
493 
494definition translate_internal ≝
495  λglobals.
496  λint_fun.
497  let graph ≝ ((empty_map …) : ltl_statement_graph globals) in
498  let valuation ≝ analyse globals int_fun in
499  let coloured_graph ≝ build valuation in
500  let liveafter ≝ analyse globals int_fun in
501  let blah ≝ mapi … (λlabel. λstmt_graph_luniv.
502    let stmt ≝
503      match eliminable globals (liveafter label) stmt with
504      [ Some successor ⇒ 〈joint_st_goto … successor, graph, joint_if_luniverse … int_fun〉
505      | None           ⇒ translate_statement globals int_fun valuation coloured_graph graph stmt
506      ]
507    in
508      ?) (joint_if_code … int_fun)
509  in ?.
510 
511 
512 
513      let stmt =
514        match Liveness.eliminable (G.liveafter label) stmt with
515        | Some successor ->
516            LTL.St_skip successor
517        | None ->
518            I.translate_statement stmt
519      in
520      graph := Label.Map.add label stmt !graph
521    ) int_fun.ERTL.f_graph
522
523definition translate_funct ≝
524  λname_def.
525  let 〈name, def〉 ≝ name_def in
526  let def' ≝
527    match def with
528    [ Internal def ⇒ Internal ? (translate_internal name def)
529    | External def ⇒ External ? def
530    ]
531  in
532    〈name, def'〉.
533
534definition translate ≝
535  λp.
536  let functs' ≝ map ? ? translate_funct (ertl_pr_functs p) in
537    mk_ltl_program (ertl_pr_globals p) functs' (ertl_pr_main p).
Note: See TracBrowser for help on using the repository browser.