source: src/ERTL/ERTLToLTL.ma @ 1179

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

changes to ertl, ltl and lin to use new notion of joint params. ertl to ltl pass in process of being changed

File size: 25.7 KB
RevLine 
[733]1include "ERTL/ERTL.ma".
[1084]2include "LTL/LTL.ma".
[1128]3include "ERTL/spill.ma".
[1154]4include "ASM/Arithmetic.ma".
5
6(* XXX: change from O'Caml: former contents of ERTLToLTLI.ma *)
7
8inductive decision: Type[0] ≝
9  | decision_spill: Byte → decision
10  | decision_colour: Register → decision.
11 
12axiom lookup: register → decision.
13
[1160]14definition fresh_label ≝
15  λglobals: list ident.
16  λluniv.
17    fresh LabelTag luniv.
18
19definition add_graph ≝
20  λglobals.
21  λlabel.
22  λstmt: ltl_statement globals.
23  λgraph: ltl_statement_graph globals.
24    add LabelTag ? graph label stmt.
25
26definition generate ≝
27  λglobals: list ident.
28  λluniv.
29  λgraph: ltl_statement_graph globals.
30  λstmt: ltl_statement globals.
31  let 〈l, luniv〉 ≝ fresh_label globals luniv in
32  let graph ≝ add_graph globals l stmt graph in
[1163]33    〈l, graph, luniv〉.
[1160]34
[1154]35definition num_locals ≝
[1163]36  λglobals.
[1154]37  λint_fun.
[1163]38    colour_locals + (ertl_if_stacksize globals int_fun).
[1154]39
40definition stacksize ≝
[1163]41  λglobals.
[1154]42  λint_fun.
[1163]43    colour_locals + (ertl_if_stacksize globals int_fun).
[1154]44
45definition adjust_off ≝
[1163]46  λglobals.
[1160]47  λint_fun.
[1154]48  λoff.
49  let 〈ignore, int_off〉 ≝ half_add ? int_size off in
[1163]50  let 〈sub, ignore〉 ≝ sub_8_with_carry (bitvector_of_nat ? (num_locals globals int_fun)) int_off false in
[1154]51    sub.
52
[1168]53definition get_stack:
54 ∀globals. ertl_internal_function globals → graph (ltl_statement globals) → Register → Byte → label →
55  ltl_statement globals × (graph (ltl_statement globals)) × (universe LabelTag)
56
[1165]57  λglobals: list ident.
[1160]58  λint_fun.
59  λgraph: graph (ltl_statement (globals)).
[1154]60  λr.
61  λoff.
62  λl.
[1163]63    let off ≝ adjust_off globals int_fun off in
64    let luniv ≝ ertl_if_luniverse globals int_fun in
[1168]65    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc r)) l) in
66    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_load … globals it it it) l) in
67    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPH)) l) in
68    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Addc it RegisterSPH) l) in
69    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_int … globals RegisterA (zero ?)) l) in
70    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPL)) l) in
71    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Add it RegisterSPL) l) in
[1172]72      〈joint_st_sequential … ltl_params globals (joint_instr_int ? globals RegisterA off) l, graph, luniv〉.
[1154]73
[1170]74definition set_stack:
75  ∀globals. ertl_internal_function globals → ltl_statement_graph globals → Byte
76    → Register → label → ((ltl_statement globals) × (ltl_statement_graph globals) × (universe LabelTag)) ≝
77  λglobals: list ident.
[1160]78  λint_fun.
79  λgraph: graph (ltl_statement (globals)).
[1154]80  λoff.
81  λr.
82  λl.
[1170]83  let off ≝ adjust_off globals int_fun off in
84  let luniv ≝ ertl_if_luniverse globals int_fun in
[1172]85  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_store ltl_params … globals it it it) l) in
[1170]86  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc r)) l) in
87  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPH)) l) in
88  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Addc it RegisterSPH) l) in
89  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_int … globals RegisterA (zero ?)) l) in
90  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPL)) l) in
91  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Add it RegisterSPL) l) in
[1172]92    〈joint_st_sequential … ltl_params globals (joint_instr_int ? globals RegisterA off) l, graph, luniv〉.
[1154]93
[1170]94definition write:
95  ∀globals: list ident. ertl_internal_function globals → ltl_statement_graph globals → register → label →
96    ? ≝
97  λglobals: list ident.
[1160]98  λint_fun.
[1170]99  λgraph.
100  λr.
101  λl.
[1154]102  match lookup r with
[1160]103  [ decision_spill off ⇒
[1170]104    let 〈stmt, graph, luniv〉 ≝ set_stack globals int_fun graph off RegisterSST l in
[1161]105    let 〈l, graph, int_fun〉 ≝ generate globals luniv graph stmt in
[1170]106      〈RegisterSST, l, graph, luniv〉
[1161]107  | decision_colour hwr ⇒
[1170]108    let luniv ≝ ertl_if_luniverse globals int_fun in
109      〈hwr, l, graph, luniv〉
[1154]110  ].
111
[1170]112definition read:
113  ∀globals: list ident. ertl_internal_function globals → ltl_statement_graph globals → register
114    → (Register → ltl_statement globals) → ? ≝
115  λglobals.
[1160]116  λint_fun.
[1170]117  λgraph.
118  λr.
119  λstmt.
[1154]120  match lookup r with
[1170]121  [ decision_colour hwr ⇒ generate globals (ertl_if_luniverse globals int_fun) graph (stmt hwr)
[1154]122  | decision_spill off ⇒
123    let temphwr ≝ RegisterSST in
[1170]124    let 〈l, graph, luniv〉 ≝ generate globals (ertl_if_luniverse globals int_fun) graph (stmt temphwr) in
125    let 〈stmt, graph, luniv〉 ≝ get_stack globals int_fun graph temphwr off l in
126      generate globals luniv graph stmt
[1154]127  ].
128
129definition move ≝
[1170]130  λglobals: list ident.
[1160]131  λint_fun.
132  λgraph: graph (ltl_statement globals).
[1154]133  λdest: decision.
134  λsrc: decision.
135  λl: label.
136  match dest with
137  [ decision_colour dest_hwr ⇒
138    match src with
139    [ decision_colour src_hwr ⇒
[1170]140      let luniv ≝ ertl_if_luniverse globals int_fun in
[1154]141      if eq_Register dest_hwr src_hwr then
[1170]142        〈joint_st_goto … globals l, graph, luniv〉
[1154]143      else
[1170]144        let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc dest_hwr)) l) in
[1172]145          〈joint_st_sequential … globals (joint_instr_move … ltl_params globals (to_acc src_hwr)) l, graph, luniv〉
[1170]146    | decision_spill src_off ⇒ get_stack globals int_fun graph dest_hwr src_off l
[1154]147    ]
148  | decision_spill dest_off ⇒
149    match src with
[1170]150    [ decision_colour src_hwr ⇒ set_stack globals int_fun graph dest_off src_hwr l
[1154]151    | decision_spill src_off ⇒
[1170]152      let luniv ≝ ertl_if_luniverse globals int_fun in
[1154]153      if eq_bv ? dest_off src_off then
[1170]154        〈joint_st_goto … globals l, graph, luniv〉
[1154]155      else
156        let temp_hwr ≝ RegisterSST in
[1170]157        let 〈stmt, graph, luniv〉 ≝ set_stack globals int_fun graph dest_off temp_hwr l in
158        let 〈l, graph, luniv〉 ≝ generate globals luniv graph stmt in
159          get_stack globals int_fun graph temp_hwr src_off l
[1154]160    ]
161  ].
162
163definition newframe ≝
[1172]164  λglobals: list ident.
165  λint_fun: ertl_internal_function globals.
[1170]166  λgraph: ltl_statement_graph globals.
[1172]167  λl: label.
[1170]168  if eq_nat (stacksize globals int_fun) 0 then
[1179]169    〈joint_st_goto ltl_params globals l, graph, (ertl_if_luniverse globals int_fun)〉
[1154]170  else
[1170]171    let luniv ≝ ertl_if_luniverse globals int_fun in
[1179]172    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_move … globals (from_acc RegisterSPH)) l) in
173    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_op2 … globals Sub it RegisterDPH) l) in
174    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_int … globals RegisterDPH (zero ?)) l) in
175    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_move … globals (to_acc RegisterSPH)) l) in
176    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_move … globals (from_acc RegisterSPL)) l) in
177    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_op2 … globals Sub it RegisterDPL) l) in
178    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_clear_carry … globals) l) in
179    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_int … globals RegisterDPL (bitvector_of_nat ? (stacksize globals int_fun))) l) in
180      〈joint_st_sequential ltl_params globals (joint_instr_move ltl_params globals (to_acc RegisterSPL)) l, graph, luniv〉.
[1154]181
182definition delframe ≝
[1171]183  λglobals.
[1160]184  λint_fun.
185  λgraph: graph (ltl_statement globals).
[1154]186  λl.
[1171]187  if eq_nat (stacksize globals int_fun) 0 then
[1179]188    〈joint_st_goto ltl_params globals l, graph, ertl_if_luniverse globals int_fun〉
[1154]189  else
[1171]190    let luniv ≝ ertl_if_luniverse globals int_fun in
[1179]191    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_move … globals (from_acc RegisterSPH)) l) in
192    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_op2 … globals Addc it RegisterSPH) l) in
193    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_int … globals RegisterA (zero ?)) l) in
194    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_move … globals (from_acc RegisterSPL)) l) in
195    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_op2 … globals Add it RegisterSPL) l) in
196      〈joint_st_sequential ltl_params globals (joint_instr_int ltl_params globals RegisterA (bitvector_of_nat ? (stacksize globals int_fun))) l, graph, luniv〉.
[1154]197
198definition translate_statement ≝
[1171]199  λglobals: list ident.
[1160]200  λint_fun.
[1171]201  λgraph: ltl_statement_graph globals.
202  λstmt: ertl_statement globals.
[1154]203  match stmt with
[1175]204  [ joint_st_sequential seq l ⇒
205    let luniv ≝ ertl_if_luniverse globals int_fun in
206    match seq with
207    [ joint_instr_comment c ⇒
[1179]208      〈joint_st_sequential ltl_params globals (joint_instr_comment … globals c) l, graph, luniv〉
[1175]209    | joint_instr_cost_label cost_lbl ⇒
210      〈joint_st_sequential … globals (joint_instr_cost_label … globals cost_lbl) l, graph, luniv〉
211    | joint_instr_pop r ⇒
212      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph r l in
213      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
214        〈joint_st_sequential … globals (joint_instr_pop ltl_params globals it) l, graph, luniv〉
215    | joint_instr_push r ⇒
216      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_push … globals it) l) in
217      let int_fun ≝ set_luniverse globals int_fun luniv in
218      let 〈l, graph, luniv〉 ≝ read globals int_fun graph r (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
[1179]219        〈joint_st_goto ltl_params globals l, graph, luniv〉
[1175]220    | joint_instr_cond srcr lbl_true ⇒
221      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_cond … globals it lbl_true) l) in
222      let int_fun ≝ set_luniverse globals int_fun luniv in
223      let 〈l, graph, luniv〉 ≝ read globals int_fun graph srcr (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
[1179]224        〈joint_st_goto ltl_params globals l, graph, luniv〉
[1175]225    | joint_instr_call_id f ignore ⇒ 〈joint_st_sequential … globals (joint_instr_call_id … globals f ignore) l, graph, luniv〉
226    | joint_instr_store addr1 addr2 srcr ⇒
227      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_store … globals it it it) l) in
228      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterST1)) l) in
229      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPH)) l) in
230      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterST0)) l) in
231      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPL)) l) in
232      let int_fun ≝ set_luniverse globals int_fun luniv in
233      let 〈l, graph, luniv〉 ≝ read globals int_fun graph addr1 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
234      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterST0)) l) in
235      let int_fun ≝ set_luniverse globals int_fun luniv in
236      let 〈l, graph, luniv〉 ≝ read globals int_fun graph addr2 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
237      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterST1)) l) in
238      let 〈l, graph, luniv〉 ≝ read globals int_fun graph srcr (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
[1179]239        〈joint_st_goto ltl_params globals l, graph, luniv〉
[1175]240    | joint_instr_load destr addr1 addr2 ⇒
241      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph destr l in
242      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
243      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_load … globals it it it) l) in
244      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPH)) l) in
245      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterST0)) l) in
246      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPL)) l) in
247      let int_fun ≝ set_luniverse globals int_fun luniv in
248      let 〈l, graph, luniv〉 ≝ read globals int_fun graph addr1 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
249      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterST0)) l) in
250      let int_fun ≝ set_luniverse globals int_fun luniv in
251      let 〈l, graph, luniv〉 ≝ read globals int_fun graph addr2 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
[1179]252        〈joint_st_goto ltl_params globals l, graph, luniv〉
[1175]253    | joint_instr_clear_carry ⇒ 〈joint_st_sequential … globals (joint_instr_clear_carry … globals) l, graph, luniv〉
254    | joint_instr_set_carry ⇒ 〈joint_st_sequential … globals (joint_instr_set_carry … globals) l, graph, luniv〉
255    | joint_instr_op2 op2 destr srcr ⇒
256      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph destr l in
257      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
258      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals op2 it RegisterB) l) in
259      let luniv ≝ set_luniverse globals int_fun luniv in
260      let 〈l, graph, luniv〉 ≝ read globals int_fun graph destr (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
261      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterB)) l) in
262      let luniv ≝ set_luniverse globals int_fun luniv in
263      let 〈l, graph, luniv〉 ≝ read globals int_fun graph srcr (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
[1179]264        〈joint_st_goto ltl_params globals l, graph, luniv〉
[1175]265    | joint_instr_op1 op1 acc_a ⇒
266      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph acc_a l in
267      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
268      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op1 … globals op1 it) l) in
269      let int_fun ≝ set_luniverse globals int_fun luniv in
270      let 〈l, graph, luniv〉 ≝ read globals int_fun graph acc_a (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
[1179]271        〈joint_st_goto ltl_params globals l, graph, luniv〉
[1175]272    | joint_instr_int r i ⇒
273      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph r l in
[1179]274        〈joint_st_sequential ltl_params globals (joint_instr_int … globals hdw i) l, graph, luniv〉
[1175]275    | joint_instr_opaccs opaccs acc_a_reg acc_b_reg ⇒
276      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph acc_a_reg l in
277      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
278      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_opaccs … globals opaccs it it) l) in
279      let luniv ≝ set_luniverse globals int_fun luniv in
280      let 〈l, graph, luniv〉 ≝ read globals int_fun graph acc_a_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
281      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterB)) l) in
282      let luniv ≝ set_luniverse globals int_fun luniv in
283      let 〈l, graph, luniv〉 ≝ read globals int_fun graph acc_b_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
284      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_goto … globals l) in
285      let luniv ≝ set_luniverse globals int_fun luniv in
286      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph acc_b_reg l in
287      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
288      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterB)) l) in
289      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_opaccs … globals opaccs it it) l) in
290      let luniv ≝ set_luniverse globals int_fun luniv in
291      let 〈l, graph, luniv〉 ≝ read globals int_fun graph acc_a_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
292      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterB)) l) in
293      let luniv ≝ set_luniverse globals int_fun luniv in
294      let 〈l, graph, luniv〉 ≝ read globals int_fun graph acc_b_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
[1179]295        〈joint_st_goto ltl_params globals l, graph, luniv〉
[1175]296    | _ ⇒ ?
[1171]297    ]
[1175]298  | joint_st_return ⇒ 〈joint_st_return … globals, graph, ertl_if_luniverse globals int_fun〉
299  | joint_st_goto l ⇒ 〈joint_st_goto … globals l, graph, ertl_if_luniverse globals int_fun〉
300  | joint_st_extension ext ⇒
301    match ext with
302    [ ertl_st_ext_new_frame l ⇒ newframe globals int_fun graph l
303    | ertl_st_ext_del_frame l ⇒ delframe globals int_fun graph l
304    | ertl_st_ext_frame_size r l ⇒
305      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph r l in
[1179]306        〈joint_st_sequential … globals (joint_instr_int ltl_params globals hdw (bitvector_of_nat ? (stacksize globals int_fun))) l, graph, luniv〉
[1175]307    ]
[1171]308  ].
309 
310  match stmt with
[1160]311  | ertl_st_get_hdw destr sourcehwr l ⇒ move int_fun globals graph (lookup destr) (decision_colour sourcehwr) l
312  | ertl_st_set_hdw desthwr srcr l ⇒ move int_fun globals graph (decision_colour desthwr) (lookup srcr) l
[1154]313  | ertl_st_hdw_to_hdw r1 r2 l ⇒
[1160]314    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals r1) l) in
315      〈joint_st_sequential ? globals (joint_instr_to_acc globals r2) l, graph〉
[1154]316  | ertl_st_addr rl rh x l ⇒
[1160]317    let 〈hdw1, l〉 ≝ write int_fun globals graph rh l in
318    let 〈l, graph〉 ≝ l in
319    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw1) l) in
320    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPH) l) in
321    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_address globals x ?) l) in
322    let 〈hdw2, l〉 ≝ write int_fun globals graph rl l in
323    let 〈l, graph〉 ≝ l in
324    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw2) l) in
325    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPL) l) in
326      〈joint_st_sequential ? globals (joint_instr_address globals x ?) l, graph〉
[1154]327(*  | ertl_st_addr_h r x l ⇒
[1160]328    let 〈hdw, l〉 ≝ write int_fun globals graph r l in
329    let 〈l, graph〉 ≝ generate globals graph (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l)) in
330    let 〈l, graph〉 ≝ generate globals graph (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPH) l)) in
[1154]331      ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_address globals x ?) l)
332  | ertl_st_addr_l r x l ⇒
[1160]333    let 〈hdw, l〉 ≝ write int_fun globals graph r l in
334    let 〈l, graph〉 ≝ generate globals graph (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l)) in
335    let 〈l, graph〉 ≝ generate globals graph (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPL) l)) in
[1154]336      ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_address globals x ?) l)
337*)
[1160]338  | ertl_st_move r1 r2 l ⇒ move int_fun globals graph (lookup r1) (lookup r2) l
[1154]339(*
340  | ertl_st_opaccs_a opaccs destr srcr1 srcr2 l ⇒
[1160]341    let 〈hdw, l〉 ≝ write int_fun globals graph destr l in
342    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
343    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l) in
344    let 〈l, graph〉 ≝ read int_fun globals graph srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
345    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
346    let 〈l, graph〉 ≝ read int_fun globals graph srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
[1154]347      joint_st_goto ? globals l
348  | ertl_st_opaccs_b opaccs destr srcr1 srcr2 l ⇒
[1160]349    let 〈hdw, l〉 ≝ write int_fun globals graph destr l in
350    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
351    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterB) l) in
352    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l) in
353    let 〈l, graph〉 ≝ read int_fun globals graph srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
354    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
355    let 〈l, graph〉 ≝ read int_fun globals graph srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
[1154]356      joint_st_goto ? globals l
357*)
358  ].
359  cases daemon (* XXX: todo -- proofs regarding gvars *)
360qed.
361
362(* **** *)
363
[1088]364definition translate_internal ≝
[1152]365  λglobals: list ident.
[1088]366  λf.
367  λint_fun: ertl_internal_function.
[1152]368  let lookup ≝ λr.
[1144]369    match lookup r with
[1152]370    | colour_spill ->
[1144]371        ERTLToLTLI.Spill (Interference.Vertex.Map.find (Interference.lookup H.graph r) S.coloring)
[1152]372    | colour_colour color ->
[1144]373        ERTLToLTLI.Color color
374  in
[1152]375  let locals ≝ colour_locals + (ertl_if_stacksize int_fun) in
376  let stacksize ≝ (ertl_if_params int_fun) + locals in
377    mk_ltl_internal_function
378      globals
379      (ertl_if_luniverse int_fun)
380      (ertl_if_runiverse int_fun)
381      stacksize.
[1144]382
383  let () =
384    Label.Map.iter (fun label stmt ->
385      let stmt =
386        match Liveness.eliminable (G.liveafter label) stmt with
387        | Some successor ->
388            LTL.St_skip successor
389        | None ->
390            I.translate_statement stmt
391      in
392      graph := Label.Map.add label stmt !graph
393    ) int_fun.ERTL.f_graph
394  in
395
[1084]396definition translate_funct ≝
397  λname_def.
398  let 〈name, def〉 ≝ name_def in
399  let def' ≝
400    match def with
401    [ Internal def ⇒ Internal ? (translate_internal name def)
402    | External def ⇒ External ? def
403    ]
404  in
405    〈name, def'〉.
406
407definition translate ≝
408  λp.
409  let functs' ≝ map ? ? translate_funct (ertl_pr_functs p) in
410    mk_ltl_program (ertl_pr_globals p) functs' (ertl_pr_main p).
Note: See TracBrowser for help on using the repository browser.