source: src/ERTL/ERTLToLTL.ma @ 1274

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

starting removing axioms from adts and giving them proper implementations

File size: 32.1 KB
RevLine 
[733]1include "ERTL/ERTL.ma".
[1084]2include "LTL/LTL.ma".
[1128]3include "ERTL/spill.ma".
[1241]4include "ERTL/uses.ma".
[1154]5include "ASM/Arithmetic.ma".
6
[1230]7(* XXX: define an interference graph for a function and colour it, allowing
[1232]8        the consultation of registers.
[1230]9definition initial_colouring ≝
[1192]10  λglobals.
11  λint_fun.
[1230]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.
[1192]18  λr.
[1230]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.
[1192]42  λr.
[1230]43  match interference_lookup initial r with
44  [ decision_colour _ ⇒ ?
45  | decision_spill ⇒ ?
46  ].
[1232]47*)
[1154]48
[1160]49definition fresh_label ≝
50  λglobals: list ident.
51  λluniv.
52    fresh LabelTag luniv.
53
[1232]54definition ltl_statement_graph ≝
55  λglobals.
56    graph … (ltl_statement globals).
57
[1160]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
[1163]72    〈l, graph, luniv〉.
[1160]73
[1154]74definition num_locals ≝
[1163]75  λglobals.
[1154]76  λint_fun.
[1249]77    colour_locals + (joint_if_stacksize globals (ertl_params globals) int_fun).
[1154]78
79definition stacksize ≝
[1163]80  λglobals.
[1154]81  λint_fun.
[1249]82    colour_locals + (joint_if_stacksize globals (ertl_params globals) int_fun).
[1154]83
84definition adjust_off ≝
[1163]85  λglobals.
[1160]86  λint_fun.
[1154]87  λoff.
88  let 〈ignore, int_off〉 ≝ half_add ? int_size off in
[1163]89  let 〈sub, ignore〉 ≝ sub_8_with_carry (bitvector_of_nat ? (num_locals globals int_fun)) int_off false in
[1154]90    sub.
91
[1168]92definition get_stack:
[1260]93 ∀globals. ertl_internal_function globals → graph (ltl_statement globals) → Register → Byte → label → ? ≝
[1165]94  λglobals: list ident.
[1160]95  λint_fun.
96  λgraph: graph (ltl_statement (globals)).
[1154]97  λr.
98  λoff.
99  λl.
[1260]100  λoriginal_label.
[1163]101    let off ≝ adjust_off globals int_fun off in
[1249]102    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
[1168]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
[1260]106    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Addc it it RegisterSPH) l) in
[1168]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
[1260]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〉.
[1154]111
[1170]112definition set_stack:
113  ∀globals. ertl_internal_function globals → ltl_statement_graph globals → Byte
[1260]114    → Register → label → ? ≝
[1170]115  λglobals: list ident.
[1160]116  λint_fun.
117  λgraph: graph (ltl_statement (globals)).
[1154]118  λoff.
119  λr.
120  λl.
[1260]121  λoriginal_label.
[1170]122  let off ≝ adjust_off globals int_fun off in
[1249]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
[1170]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
[1260]127  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Addc it it RegisterSPH) l) in
[1170]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
[1260]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〉.
[1154]132
[1260]133
[1232]134definition write ≝
[1170]135  λglobals: list ident.
[1260]136  λint_fun: ertl_internal_function globals.
[1232]137  λvaluation.
138  λcoloured_graph.
[1170]139  λgraph.
140  λr.
141  λl.
[1260]142  λoriginal_label: label.
[1251]143  match colouring valuation coloured_graph (inl … r) with
[1160]144  [ decision_spill off ⇒
[1260]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
[1170]147      〈RegisterSST, l, graph, luniv〉
[1161]148  | decision_colour hwr ⇒
[1249]149    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
[1170]150      〈hwr, l, graph, luniv〉
[1154]151  ].
152
[1232]153definition read ≝
154  λglobals: list ident.
[1260]155  λint_fun: ertl_internal_function globals.
[1232]156  λvaluation.
157  λcoloured_graph.
[1170]158  λgraph.
159  λr.
160  λstmt.
[1260]161  λoriginal_label: label.
[1251]162  match colouring valuation coloured_graph (inl … r) with
[1260]163  [ decision_colour hwr ⇒
164    let luniv ≝ joint_if_luniverse … int_fun in
165      〈add_graph globals original_label (stmt hwr) graph, luniv〉
[1154]166  | decision_spill off ⇒
167    let temphwr ≝ RegisterSST in
[1260]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
[1154]171  ].
172
173definition move ≝
[1170]174  λglobals: list ident.
[1160]175  λint_fun.
176  λgraph: graph (ltl_statement globals).
[1154]177  λdest: decision.
178  λsrc: decision.
179  λl: label.
[1263]180  λoriginal_label: label.
[1154]181  match dest with
182  [ decision_colour dest_hwr ⇒
183    match src with
184    [ decision_colour src_hwr ⇒
[1249]185      let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
[1154]186      if eq_Register dest_hwr src_hwr then
[1260]187        〈add_graph globals original_label (joint_st_goto … globals l) graph, luniv〉
[1154]188      else
[1170]189        let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc dest_hwr)) l) in
[1260]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
[1154]192    ]
193  | decision_spill dest_off ⇒
194    match src with
[1260]195    [ decision_colour src_hwr ⇒ set_stack globals int_fun graph (bitvector_of_nat … dest_off) src_hwr l original_label
[1154]196    | decision_spill src_off ⇒
[1249]197      let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
[1232]198      if eq_nat dest_off src_off then
[1260]199        〈add_graph globals original_label (joint_st_goto … globals l) graph, luniv〉
[1154]200      else
201        let temp_hwr ≝ RegisterSST in
[1260]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
[1154]204    ]
205  ].
206
207definition newframe ≝
[1172]208  λglobals: list ident.
209  λint_fun: ertl_internal_function globals.
[1170]210  λgraph: ltl_statement_graph globals.
[1172]211  λl: label.
[1260]212  λoriginal_label: label.
[1170]213  if eq_nat (stacksize globals int_fun) 0 then
[1260]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〉
[1154]216  else
[1249]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
[1260]219    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Sub it it RegisterDPH) l) in
[1249]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
[1260]223    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Sub it it RegisterDPL) l) in
[1249]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
[1260]226      〈add_graph globals original_label (joint_st_sequential (ltl_params globals) globals (joint_instr_move … globals (to_acc RegisterSPL)) l) graph, luniv〉.
[1154]227
228definition delframe ≝
[1171]229  λglobals.
[1160]230  λint_fun.
231  λgraph: graph (ltl_statement globals).
[1154]232  λl.
[1260]233  λoriginal_label: label.
[1171]234  if eq_nat (stacksize globals int_fun) 0 then
[1260]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〉
[1154]237  else
[1249]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
[1260]240    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Addc it it RegisterSPH) l) in
[1249]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
[1260]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〉.
[1154]245
[1263]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)) ≝
[1171]250  λglobals: list ident.
[1160]251  λint_fun.
[1232]252  λvaluation.
253  λcoloured_graph: coloured_graph valuation.
[1171]254  λgraph: ltl_statement_graph globals.
255  λstmt: ertl_statement globals.
[1260]256  λoriginal_label: label.
[1154]257  match stmt with
[1175]258  [ joint_st_sequential seq l ⇒
[1249]259    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
[1175]260    match seq with
261    [ joint_instr_comment c ⇒
[1263]262      〈add_graph globals original_label (joint_st_sequential … (joint_instr_comment … c) l) graph, luniv〉
[1175]263    | joint_instr_cost_label cost_lbl ⇒
[1263]264      〈add_graph globals original_label (joint_st_sequential … (joint_instr_cost_label … cost_lbl) l) graph, luniv〉
[1175]265    | joint_instr_pop r ⇒
[1263]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〉
[1175]271    | joint_instr_push r ⇒
[1263]272      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_push … it) l) in
[1249]273      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
[1260]274      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
[1263]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〉
[1175]278    | joint_instr_cond srcr lbl_true ⇒
[1263]279      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_cond … it lbl_true) l) in
[1249]280      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
[1263]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〉
[1271]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〉
[1175]286    | joint_instr_store addr1 addr2 srcr ⇒
[1263]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
[1249]292      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
[1263]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
[1249]297      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
[1263]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〉
[1175]306    | joint_instr_load destr addr1 addr2 ⇒
[1263]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
[1249]315      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
[1263]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
[1249]320      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
[1263]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〉
[1260]327    | joint_instr_op2 op2 destr srcr1 srcr2 ⇒
[1263]328      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
[1249]329      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
[1263]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〉
[1175]352    | joint_instr_int r i ⇒
[1263]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〉
[1191]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  ⇒
[1263]362        match regr with
[1260]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
[1191]365        ]
366      | hardware h1 ⇒
367        match regr with
[1260]368        [ pseudo p    ⇒ move globals int_fun graph (decision_colour h1) (colouring valuation coloured_graph (inl … p)) l original_label
[1191]369        | hardware h2 ⇒
[1263]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〉
[1191]372        ]
373      ]
374    | joint_instr_address lbl prf dpl dph ⇒
[1263]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
[1191]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
[1249]381      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
[1263]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
[1191]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
[1263]387        〈add_graph globals original_label (joint_st_sequential ltl_params_ globals (joint_instr_address … lbl prf it it) l) graph, luniv〉
[1250]388    | joint_instr_extension ext ⇒
389      match ext with
[1263]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
[1260]392      | ertl_st_ext_frame_size r ⇒
[1263]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〉
[1250]397      ]
[1263]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〉
[1171]431    ]
[1263]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〉
[1171]434  ].
[1154]435
[1260]436lemma Sm_leq_n_m_leq_n:
[1256]437  ∀m, n: nat.
438    S m ≤ n → m ≤ n.
[1260]439  #m #n /2/
440qed.
[1256]441
[1271]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
[1256]450    | Node n' l r ⇒ λabsrd. ⊥
[1271]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'))
[1256]459  ].
[1271]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 // ]
[1256]464qed.
[1260]465
[1271]466definition bvt_fold ≝
[1260]467  λa, b: Type[0].
[1271]468  λf: label → a → b → b.
[1260]469  λtrie: BitVectorTrie a 16.
[1271]470  λseed: b.
471    let f' ≝ λbv: BitVector 16. λa. λb.
472      f (an_identifier LabelTag bv) a b
[1260]473    in
[1271]474      fold_aux a b f' seed 16 ? trie [[]].
[1260]475  //
476qed.
[1271]477
478definition graph_fold ≝
[1232]479  λglobals.
[1271]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
[1260]493  let valuation ≝ analyse globals int_fun in
494  let coloured_graph ≝ build valuation in
[1271]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〉
[1084]502  in
[1274]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  ]
[1271]522qed.
[1084]523
[1274]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.