source: src/ERTL/ERTLToLTL.ma @ 1280

Last change on this file since 1280 was 1275, checked in by sacerdot, 9 years ago

RTL ported to joint syntax, but:

  1. bug discovered: opaccs should have taken four registers
  2. push/pop should not be present in RTL :-(

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