source: src/ERTL/ERTLToLTL.ma @ 1274

Last change on this file since 1274 was 1274, checked in by mulligan, 8 years ago

starting removing axioms from adts and giving them proper implementations

File size: 32.1 KB
Line 
1include "ERTL/ERTL.ma".
2include "LTL/LTL.ma".
3include "ERTL/spill.ma".
4include "ERTL/uses.ma".
5include "ASM/Arithmetic.ma".
6
7(* XXX: define an interference graph for a function and colour it, allowing
8        the consultation of registers.
9definition initial_colouring ≝
10  λglobals.
11  λint_fun.
12  let 〈ignore, graph〉 ≝ build globals int_fun in
13  let coloured ≝ colour_initial graph in
14    coloured.
15
16definition interference_lookup ≝
17  λcoloured: initial_colouring.
18  λr.
19    colouring … coloured r.
20
21definition prepare_graph_for_second_colouring ≝
22  λglobals: list ident.
23  λcoloured: initial_colouring.
24    let g ≝ the_graph decision coloured in
25    let restricted ≝ ig_restrict g (λv.
26      match colouring decision coloured v with
27      [ decision_spill ⇒ true
28      | decision_colour _ ⇒ false
29      ]
30    )
31    in restricted.
32
33definition second_colouring ≝
34  λglobals: list ident.
35  λcoloured.
36    let prepared ≝ prepare_graph_for_second_colouring globals coloured in
37      colour_stack prepared.
38
39definition lookup ≝
40  λinitial.
41  λsecond.
42  λr.
43  match interference_lookup initial r with
44  [ decision_colour _ ⇒ ?
45  | decision_spill ⇒ ?
46  ].
47*)
48
49definition fresh_label ≝
50  λglobals: list ident.
51  λluniv.
52    fresh LabelTag luniv.
53
54definition ltl_statement_graph ≝
55  λglobals.
56    graph … (ltl_statement globals).
57
58definition add_graph ≝
59  λglobals.
60  λlabel.
61  λstmt: ltl_statement globals.
62  λgraph: ltl_statement_graph globals.
63    add LabelTag ? graph label stmt.
64
65definition generate ≝
66  λglobals: list ident.
67  λluniv.
68  λgraph: ltl_statement_graph globals.
69  λstmt: ltl_statement globals.
70  let 〈l, luniv〉 ≝ fresh_label globals luniv in
71  let graph ≝ add_graph globals l stmt graph in
72    〈l, graph, luniv〉.
73
74definition num_locals ≝
75  λglobals.
76  λint_fun.
77    colour_locals + (joint_if_stacksize globals (ertl_params globals) int_fun).
78
79definition stacksize ≝
80  λglobals.
81  λint_fun.
82    colour_locals + (joint_if_stacksize globals (ertl_params globals) int_fun).
83
84definition adjust_off ≝
85  λglobals.
86  λint_fun.
87  λoff.
88  let 〈ignore, int_off〉 ≝ half_add ? int_size off in
89  let 〈sub, ignore〉 ≝ sub_8_with_carry (bitvector_of_nat ? (num_locals globals int_fun)) int_off false in
90    sub.
91
92definition get_stack:
93 ∀globals. ertl_internal_function globals → graph (ltl_statement globals) → Register → Byte → label → ? ≝
94  λglobals: list ident.
95  λint_fun.
96  λgraph: graph (ltl_statement (globals)).
97  λr.
98  λoff.
99  λl.
100  λoriginal_label.
101    let off ≝ adjust_off globals int_fun off in
102    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
103    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc r)) l) in
104    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_load … globals it it it) l) in
105    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPH)) l) in
106    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Addc it it RegisterSPH) l) in
107    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_int … globals RegisterA (zero ?)) l) in
108    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPL)) l) in
109    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Add it it RegisterSPL) l) in
110      〈add_graph globals original_label (joint_st_sequential (ltl_params globals) globals (joint_instr_int … (ltl_params globals) globals RegisterA off) l) graph, luniv〉.
111
112definition set_stack:
113  ∀globals. ertl_internal_function globals → ltl_statement_graph globals → Byte
114    → Register → label → ? ≝
115  λglobals: list ident.
116  λint_fun.
117  λgraph: graph (ltl_statement (globals)).
118  λoff.
119  λr.
120  λl.
121  λoriginal_label.
122  let off ≝ adjust_off globals int_fun off in
123  let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
124  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_store … globals it it it) l) in
125  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc r)) l) in
126  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPH)) l) in
127  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Addc it it RegisterSPH) l) in
128  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_int … globals RegisterA (zero ?)) l) in
129  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPL)) l) in
130  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Add it it RegisterSPL) l) in
131    〈add_graph globals original_label (joint_st_sequential (ltl_params globals) globals (joint_instr_int … (ltl_params globals) globals RegisterA off) l) graph, luniv〉.
132
133
134definition write ≝
135  λglobals: list ident.
136  λint_fun: ertl_internal_function globals.
137  λvaluation.
138  λcoloured_graph.
139  λgraph.
140  λr.
141  λl.
142  λoriginal_label: label.
143  match colouring valuation coloured_graph (inl … r) with
144  [ decision_spill off ⇒
145    let luniv ≝ joint_if_luniverse … int_fun in
146    let 〈graph, luniv〉 ≝ set_stack globals int_fun graph (bitvector_of_nat … off) RegisterSST l original_label 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: ertl_internal_function globals.
156  λvaluation.
157  λcoloured_graph.
158  λgraph.
159  λr.
160  λstmt.
161  λoriginal_label: label.
162  match colouring valuation coloured_graph (inl … r) with
163  [ decision_colour hwr ⇒
164    let luniv ≝ joint_if_luniverse … int_fun in
165      〈add_graph globals original_label (stmt hwr) graph, luniv〉
166  | decision_spill off ⇒
167    let temphwr ≝ RegisterSST in
168    let luniv ≝ joint_if_luniverse … int_fun in
169    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (stmt temphwr) in
170      get_stack globals int_fun graph temphwr (bitvector_of_nat … off) l original_label
171  ].
172
173definition move ≝
174  λglobals: list ident.
175  λint_fun.
176  λgraph: graph (ltl_statement globals).
177  λdest: decision.
178  λsrc: decision.
179  λl: label.
180  λoriginal_label: label.
181  match dest with
182  [ decision_colour dest_hwr ⇒
183    match src with
184    [ decision_colour src_hwr ⇒
185      let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
186      if eq_Register dest_hwr src_hwr then
187        〈add_graph globals original_label (joint_st_goto … globals l) graph, luniv〉
188      else
189        let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc dest_hwr)) l) in
190          〈add_graph globals original_label (joint_st_sequential (ltl_params globals) globals (joint_instr_move … globals (to_acc src_hwr)) l) graph, luniv〉
191    | decision_spill src_off ⇒ get_stack globals int_fun graph dest_hwr (bitvector_of_nat … src_off) l original_label
192    ]
193  | decision_spill dest_off ⇒
194    match src with
195    [ decision_colour src_hwr ⇒ set_stack globals int_fun graph (bitvector_of_nat … dest_off) src_hwr l original_label
196    | decision_spill src_off ⇒
197      let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
198      if eq_nat dest_off src_off then
199        〈add_graph globals original_label (joint_st_goto … globals l) graph, luniv〉
200      else
201        let temp_hwr ≝ RegisterSST in
202        let 〈graph, luniv〉 ≝ set_stack globals int_fun graph (bitvector_of_nat … dest_off) temp_hwr l original_label in
203          get_stack globals int_fun graph temp_hwr (bitvector_of_nat … src_off) l original_label
204    ]
205  ].
206
207definition newframe ≝
208  λglobals: list ident.
209  λint_fun: ertl_internal_function globals.
210  λgraph: ltl_statement_graph globals.
211  λl: label.
212  λoriginal_label: label.
213  if eq_nat (stacksize globals int_fun) 0 then
214    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
215      〈add_graph globals original_label (joint_st_goto … globals l) graph, luniv〉
216  else
217    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
218    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterSPH)) l) in
219    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Sub it it RegisterDPH) l) in
220    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_int … globals RegisterDPH (zero ?)) l) in
221    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterSPH)) l) in
222    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterSPL)) l) in
223    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Sub it it RegisterDPL) l) in
224    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_clear_carry … globals) l) in
225    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
226      〈add_graph globals original_label (joint_st_sequential (ltl_params globals) globals (joint_instr_move … globals (to_acc RegisterSPL)) l) graph, luniv〉.
227
228definition delframe ≝
229  λglobals.
230  λint_fun.
231  λgraph: graph (ltl_statement globals).
232  λl.
233  λoriginal_label: label.
234  if eq_nat (stacksize globals int_fun) 0 then
235    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
236      〈add_graph globals original_label (joint_st_goto (ltl_params globals) globals l) graph, luniv〉
237  else
238    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
239    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterSPH)) l) in
240    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Addc it it RegisterSPH) l) in
241    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_int … globals RegisterA (zero ?)) l) in
242    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterSPL)) l) in
243    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Add it it RegisterSPL) l) in
244      〈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〉.
245
246definition translate_statement:
247  ∀globals: list ident. ertl_internal_function globals → ∀v: valuation.
248    coloured_graph v → ltl_statement_graph globals → ertl_statement globals →
249      label → ((ltl_statement_graph globals) × (universe LabelTag)) ≝
250  λglobals: list ident.
251  λint_fun.
252  λvaluation.
253  λcoloured_graph: coloured_graph valuation.
254  λgraph: ltl_statement_graph globals.
255  λstmt: ertl_statement globals.
256  λoriginal_label: label.
257  match stmt with
258  [ joint_st_sequential seq l ⇒
259    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
260    match seq with
261    [ joint_instr_comment c ⇒
262      〈add_graph globals original_label (joint_st_sequential … (joint_instr_comment … c) l) graph, luniv〉
263    | joint_instr_cost_label cost_lbl ⇒
264      〈add_graph globals original_label (joint_st_sequential … (joint_instr_cost_label … cost_lbl) l) graph, luniv〉
265    | joint_instr_pop r ⇒
266      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
267      let int_fun ≝ set_luniverse globals ? int_fun luniv in
268      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph r l fresh_lbl in
269      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc hdw)) l) in
270        〈add_graph globals original_label (joint_st_sequential ltl_params_ globals (joint_instr_pop … it) l) graph, luniv〉
271    | joint_instr_push r ⇒
272      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_push … it) l) in
273      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
274      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
275      let int_fun ≝ set_luniverse globals ? int_fun luniv in
276      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
277        〈add_graph globals original_label (joint_st_goto … fresh_lbl) graph, luniv〉
278    | joint_instr_cond srcr lbl_true ⇒
279      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_cond … it lbl_true) l) in
280      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
281      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
282      let int_fun' ≝ set_luniverse globals ? int_fun luniv in
283      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
284        〈add_graph globals original_label (joint_st_goto … fresh_lbl) graph, luniv〉
285    | joint_instr_call_id f ignore ignore' ⇒ 〈add_graph globals original_label (joint_st_sequential … (joint_instr_call_id … f ignore ignore') l) graph, luniv〉
286    | joint_instr_store addr1 addr2 srcr ⇒
287      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_store … it it it) l) in
288      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (to_acc RegisterST1)) l) in
289      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc RegisterDPH)) l) in
290      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (to_acc RegisterST0)) l) in
291      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc RegisterDPL)) l) in
292      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
293      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
294      let int_fun ≝ set_luniverse globals ? int_fun luniv in
295      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
296      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc RegisterST0)) fresh_lbl) in
297      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
298      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
299      let int_fun ≝ set_luniverse globals ? int_fun luniv in
300      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
301      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc RegisterST1)) fresh_lbl) in
302      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
303      let int_fun ≝ set_luniverse globals ? int_fun luniv in
304      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
305        〈add_graph globals original_label (joint_st_goto … l) graph, luniv〉
306    | joint_instr_load destr addr1 addr2 ⇒
307      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
308      let int_fun ≝ set_luniverse globals ? int_fun luniv in
309      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph destr l fresh_lbl in
310      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc hdw)) l) in
311      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_load … it it it) l) in
312      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc RegisterDPH)) l) in
313      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (to_acc RegisterST0)) l) in
314      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc RegisterDPL)) l) in
315      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
316      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
317      let int_fun ≝ set_luniverse globals ? int_fun luniv in
318      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
319      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc RegisterST0)) fresh_lbl) in
320      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
321      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
322      let int_fun ≝ set_luniverse globals ? int_fun luniv in
323      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
324        〈add_graph globals original_label (joint_st_goto … fresh_lbl) graph, luniv〉
325    | joint_instr_clear_carry ⇒ 〈add_graph globals original_label (joint_st_sequential … (joint_instr_clear_carry …) l) graph, luniv〉
326    | joint_instr_set_carry ⇒ 〈add_graph globals original_label (joint_st_sequential … (joint_instr_set_carry …) l) graph, luniv〉
327    | joint_instr_op2 op2 destr srcr1 srcr2 ⇒
328      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
329      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
330      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph destr l fresh_lbl in
331      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc hdw)) l) in
332      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_op2 … op2 it it RegisterB) l) in
333      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
334      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
335      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
336      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc RegisterB)) fresh_lbl) in
337      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
338      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
339      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
340        〈add_graph globals original_label (joint_st_goto … l) graph, luniv〉
341    | joint_instr_op1 op1 destr srcr ⇒
342      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
343      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
344      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph destr l fresh_lbl in
345      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc hdw)) l) in
346      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_op1 … op1 it it) l) in
347      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
348      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
349      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
350      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
351        〈add_graph globals original_label (joint_st_goto … l) graph, luniv〉
352    | joint_instr_int r i ⇒
353      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
354      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
355      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph r l fresh_lbl in
356        〈add_graph globals original_label (joint_st_sequential ltl_params_ globals (joint_instr_int … hdw i) l) graph, luniv〉
357    | joint_instr_move pair_regs ⇒
358      let regl ≝ \fst pair_regs in
359      let regr ≝ \snd pair_regs in
360      match regl with
361      [ pseudo p1  ⇒
362        match regr with
363        [ pseudo p2  ⇒ move globals int_fun graph (colouring valuation coloured_graph (inl … p1)) (colouring valuation coloured_graph (inl … p2)) l original_label
364        | hardware h ⇒ move globals int_fun graph (colouring valuation coloured_graph (inl … p1)) (decision_colour h) l original_label
365        ]
366      | hardware h1 ⇒
367        match regr with
368        [ pseudo p    ⇒ move globals int_fun graph (decision_colour h1) (colouring valuation coloured_graph (inl … p)) l original_label
369        | hardware h2 ⇒
370          let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc h1)) l) in
371            〈add_graph globals original_label (joint_st_sequential ltl_params_ … (joint_instr_move … (to_acc h2)) l) graph, luniv〉
372        ]
373      ]
374    | joint_instr_address lbl prf dpl dph ⇒
375      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
376      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
377      let 〈hdw1, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph dph l fresh_lbl 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 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
383      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
384      let 〈hdw2, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph dpl l fresh_lbl in
385      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw2)) l) in
386      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterDPL)) l) in
387        〈add_graph globals original_label (joint_st_sequential ltl_params_ globals (joint_instr_address … lbl prf it it) l) graph, luniv〉
388    | joint_instr_extension ext ⇒
389      match ext with
390      [ ertl_st_ext_new_frame ⇒ newframe globals int_fun graph l original_label
391      | ertl_st_ext_del_frame ⇒ delframe globals int_fun graph l original_label
392      | ertl_st_ext_frame_size r ⇒
393        let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
394        let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
395        let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph r l fresh_lbl in
396          〈add_graph globals original_label (joint_st_sequential ltl_params_ globals (joint_instr_int … hdw (bitvector_of_nat … (stacksize … int_fun))) l) graph, luniv〉
397      ]
398    | joint_instr_opaccs opaccs acc_a_reg acc_b_reg ⇒
399      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
400      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
401      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph acc_a_reg l fresh_lbl in
402      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc hdw)) l) in
403      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_opaccs … opaccs it it) l) in
404      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
405      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
406      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
407      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
408      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc RegisterB)) fresh_lbl) in
409      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
410      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
411      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
412      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
413      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_goto … fresh_lbl) in
414      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
415      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
416      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
417      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph acc_b_reg l fresh_lbl in
418      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc hdw)) l) in
419      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (to_acc RegisterB)) l) in
420      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_opaccs … opaccs it it) l) in
421      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
422      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
423      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
424      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
425      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterB)) fresh_lbl) in
426      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
427      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
428      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
429      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
430        〈add_graph globals original_label (joint_st_goto … globals fresh_lbl) graph, luniv〉
431    ]
432  | joint_st_return ⇒ 〈add_graph globals original_label (joint_st_return ltl_params_ globals) graph, joint_if_luniverse globals (ertl_params globals) int_fun〉
433  | 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〉
434  ].
435
436lemma Sm_leq_n_m_leq_n:
437  ∀m, n: nat.
438    S m ≤ n → m ≤ n.
439  #m #n /2/
440qed.
441
442let rec fold_aux
443  (a, b: Type[0]) (f: BitVector 16 → a → b → b) (seed: b) (n: nat)
444    on n: n ≤ 16 → BitVectorTrie a n → BitVector (16 - n) → b ≝
445  match n return λn: nat. n ≤ 16 → BitVectorTrie a n → BitVector (16 - n) → b with
446  [ O    ⇒ λinvariant: 0 ≤ 16. λtrie: BitVectorTrie a 0. λpath: BitVector 16.
447    match trie return λx: nat. λtrie': BitVectorTrie a x. ∀prf: x = 0. b with
448    [ Leaf l      ⇒ λproof. f path l seed
449    | Stub s      ⇒ λproof. seed
450    | Node n' l r ⇒ λabsrd. ⊥
451    ] (refl … 0)
452  | S n' ⇒ λinvariant: S n' ≤ 16. λtrie: BitVectorTrie a (S n'). λpath: BitVector (16 - S n').
453    match trie return λx: nat. λtrie': BitVectorTrie a x. ∀prf: x = S n'. b with
454    [ Leaf l      ⇒ λabsrd. ⊥
455    | Stub s      ⇒ λproof. seed
456    | Node n'' l r ⇒ λproof.
457        fold_aux a b f (fold_aux a b f seed n' ? (l⌈BitVectorTrie a n'' ↦ BitVectorTrie a n'⌉) ((false:::path)⌈S (16 - S n') ↦ 16 - n'⌉)) n' ? (r⌈BitVectorTrie a n'' ↦ BitVectorTrie a n'⌉) ((true:::path)⌈S (16 - S n') ↦ 16 - n'⌉)
458    ] (refl … (S n'))
459  ].
460  [ 1, 2: destruct(absrd)
461  | 3,8: >minus_S_S <minus_Sn_m // @le_S_S_to_le //
462  | 4,7: destruct(proof) %
463  | 5,6: @Sm_leq_n_m_leq_n // ]
464qed.
465
466definition bvt_fold ≝
467  λa, b: Type[0].
468  λf: label → a → b → b.
469  λtrie: BitVectorTrie a 16.
470  λseed: b.
471    let f' ≝ λbv: BitVector 16. λa. λb.
472      f (an_identifier LabelTag bv) a b
473    in
474      fold_aux a b f' seed 16 ? trie [[]].
475  //
476qed.
477
478definition graph_fold ≝
479  λglobals.
480  λb : Type[0].
481  λf    : label → ertl_statement globals → b → b.
482  λgraph: graph (ertl_statement globals).
483  λseed : b.
484  match graph with
485  [ an_id_map tree ⇒ bvt_fold (ertl_statement globals) b f tree seed
486  ]. 
487
488definition translate_internal: ∀globals: list ident.
489  ertl_internal_function globals → ltl_internal_function globals ≝
490  λglobals: list ident.
491  λint_fun: ertl_internal_function globals.
492  let graph ≝ (empty_map … : ltl_statement_graph globals) in
493  let valuation ≝ analyse globals int_fun in
494  let coloured_graph ≝ build valuation in
495  let 〈graph, luniv〉 ≝ graph_fold globals ((ltl_statement_graph globals) × (universe LabelTag)) (λlabel: label. λstmt: ertl_statement globals. λgraph_luniv: (? × (universe LabelTag)).
496    let 〈graph, luniv〉 ≝ graph_luniv in
497      match eliminable globals (valuation label) stmt with
498      [ Some successor ⇒ 〈add_graph globals label (joint_st_goto … successor) graph, luniv〉
499      | None           ⇒
500        translate_statement globals int_fun valuation coloured_graph graph stmt label
501      ]) (joint_if_code globals (ertl_params globals) int_fun) 〈graph, joint_if_luniverse … int_fun〉
502  in
503    match joint_if_entry … int_fun with
504    [ dp entry_label entry_label_prf ⇒
505      match joint_if_exit … int_fun with
506      [ dp exit_label exit_label_prf ⇒
507          mk_joint_internal_function globals (ltl_params globals)
508            luniv (joint_if_runiverse … int_fun)
509              it it it (joint_if_stacksize … int_fun)
510                graph ? ?
511      ]
512    ].
513  [1: %
514    [1: @entry_label
515    |2: cases daemon (* XXX *)
516    ]
517  |2: %
518    [1: @exit_label
519    |2: cases daemon (* XXX *)
520    ]
521  ]
522qed.
523
524definition ertl_to_ltl: ertl_program → ltl_program ≝
525  λp.
526    transform_program … p (transf_fundef … (translate_internal …)).
Note: See TracBrowser for help on using the repository browser.