source: src/ERTL/ERTLToLTL.ma @ 1168

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

Joint statements parameterized over a record.

File size: 21.9 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
72      〈joint_st_sequential ? ltl_params globals (joint_instr_int ? globals RegisterA off) l, graph, luniv〉.
[1154]73
74definition set_stack ≝
[1160]75  λint_fun.
[1154]76  λglobals.
[1160]77  λgraph: graph (ltl_statement (globals)).
[1154]78  λoff.
79  λr.
80  λl.
[1160]81  let off ≝ adjust_off int_fun off in
[1161]82  let luniv ≝ ertl_if_luniverse int_fun in
83  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_store globals) l) in
84  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_to_acc globals r) l) in
85  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in
86  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_op2 globals Addc RegisterSPH) l) in
87  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_int globals RegisterA (zero ?)) l) in
88  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in
89  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_op2 globals Add RegisterSPL) l) in
90    〈joint_st_sequential ? globals (joint_instr_int globals RegisterA off) l, 〈graph, luniv〉〉.
[1154]91
92definition write ≝
[1160]93  λint_fun.
[1154]94  λglobals.
[1160]95  λgraph: graph (ltl_statement (globals)).
[1154]96  λr: register.
97  λl: label.
98  match lookup r with
[1160]99  [ decision_spill off ⇒
[1161]100    let 〈stmt, graph, luniv〉 ≝ set_stack int_fun globals graph off RegisterSST l in
101    let 〈l, graph, int_fun〉 ≝ generate globals luniv graph stmt in
102      〈RegisterSST, 〈l, 〈graph, luniv〉〉〉
103  | decision_colour hwr ⇒
104    let luniv ≝ ertl_if_luniverse int_fun in
105      〈hwr, 〈l, 〈graph, luniv〉〉〉
[1154]106  ].
107
108definition read ≝
[1160]109  λint_fun.
[1154]110  λglobals.
[1160]111  λgraph: graph (ltl_statement (globals)).
[1154]112  λr: register.
113  λstmt: Register → ltl_statement globals.
114  match lookup r with
[1160]115  [ decision_colour hwr ⇒ generate globals graph (stmt hwr)
[1154]116  | decision_spill off ⇒
117    let temphwr ≝ RegisterSST in
[1160]118    let 〈l, graph〉 ≝ generate globals graph (stmt temphwr) in
119    let 〈stmt, graph〉 ≝ get_stack int_fun globals graph temphwr off l in
120      generate globals graph stmt
[1154]121  ].
122
123definition move ≝
[1160]124  λint_fun.
[1154]125  λglobals: list ident.
[1160]126  λgraph: graph (ltl_statement globals).
[1154]127  λdest: decision.
128  λsrc: decision.
129  λl: label.
130  match dest with
131  [ decision_colour dest_hwr ⇒
132    match src with
133    [ decision_colour src_hwr ⇒
134      if eq_Register dest_hwr src_hwr then
[1160]135        〈joint_st_goto ? globals l, graph〉
[1154]136      else
[1160]137        let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals dest_hwr) l) in
138          〈joint_st_sequential ? globals (joint_instr_to_acc globals src_hwr) l, graph〉
139    | decision_spill src_off ⇒ get_stack int_fun globals graph dest_hwr src_off l
[1154]140    ]
141  | decision_spill dest_off ⇒
142    match src with
[1160]143    [ decision_colour src_hwr ⇒ set_stack int_fun globals graph dest_off src_hwr l
[1154]144    | decision_spill src_off ⇒
145      if eq_bv ? dest_off src_off then
[1160]146        〈joint_st_goto ? globals l, graph〉
[1154]147      else
148        let temp_hwr ≝ RegisterSST in
[1160]149        let 〈stmt, graph〉 ≝ set_stack int_fun globals graph dest_off temp_hwr l in
150        let 〈l, graph〉 ≝ generate globals graph stmt in
151          get_stack int_fun globals graph temp_hwr src_off l
[1154]152    ]
153  ].
154
155definition newframe ≝
[1160]156  λint_fun.
[1154]157  λglobals.
[1160]158  λgraph: graph (ltl_statement globals).
[1154]159  λl.
[1160]160  if eq_nat (stacksize int_fun) 0 then
161    〈joint_st_goto ? globals l, graph〉
[1154]162  else
[1160]163    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPH) l) in
164    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_op2 globals Sub RegisterDPH) l) in
165    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_int globals RegisterDPH (zero ?)) l) in
166    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterSPH) l) in
167    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPL) l) in
168    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_op2 globals Sub RegisterDPL) l) in
169    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_clear_carry globals) l) in
170    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_int globals RegisterDPL (bitvector_of_nat ? (stacksize int_fun))) l) in
171      〈joint_st_sequential ? globals (joint_instr_to_acc globals RegisterSPL) l, graph〉.
[1154]172
173definition delframe ≝
[1160]174  λint_fun.
[1154]175  λglobals.
[1160]176  λgraph: graph (ltl_statement globals).
[1154]177  λl.
[1160]178  if eq_nat (stacksize int_fun) 0 then
179    〈joint_st_goto ? globals l, graph〉
[1154]180  else
[1160]181    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPH) l) in
182    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_op2 globals Addc RegisterSPH) l) in
183    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_int globals RegisterA (zero ?)) l) in
184    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPL) l) in
185    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_op2 globals Add RegisterSPL) l) in
186      〈joint_st_sequential ? globals (joint_instr_int globals RegisterA (bitvector_of_nat ? (stacksize int_fun))) l, graph〉.
[1154]187
188definition translate_statement ≝
[1160]189  λint_fun.
[1154]190  λglobals: list ident.
[1160]191  λgraph: graph (ltl_statement globals).
[1154]192  λstmt: ertl_statement.
193  match stmt with
[1160]194  [ ertl_st_skip l ⇒ 〈joint_st_goto ? globals l, graph〉
195  | ertl_st_comment s l ⇒ 〈joint_st_sequential ? globals (joint_instr_comment globals s) l, graph〉
196  | ertl_st_cost cost_lbl l ⇒ 〈joint_st_sequential ? globals (joint_instr_cost_label globals cost_lbl) l, graph〉
197  | ertl_st_get_hdw destr sourcehwr l ⇒ move int_fun globals graph (lookup destr) (decision_colour sourcehwr) l
198  | ertl_st_set_hdw desthwr srcr l ⇒ move int_fun globals graph (decision_colour desthwr) (lookup srcr) l
[1154]199  | ertl_st_hdw_to_hdw r1 r2 l ⇒
[1160]200    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals r1) l) in
201      〈joint_st_sequential ? globals (joint_instr_to_acc globals r2) l, graph〉
202  | ertl_st_new_frame l ⇒ newframe int_fun globals graph l
203  | ertl_st_del_frame l ⇒ delframe int_fun globals graph l
[1154]204  | ertl_st_frame_size r l ⇒
[1160]205    let 〈hdw, l〉 ≝ write int_fun globals graph r l in
206    let 〈l, graph〉 ≝ l in
207      〈joint_st_sequential ? globals (joint_instr_int globals hdw (bitvector_of_nat ? (stacksize int_fun))) l, graph〉
[1154]208  | ertl_st_pop r l ⇒
[1160]209    let 〈hdw, l〉 ≝ write int_fun globals graph r l in
210    let 〈l, graph〉 ≝ l in
211    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
212      〈joint_st_sequential ? globals (joint_instr_pop globals) l, graph〉
[1154]213  | ertl_st_push r l ⇒
[1160]214    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_push globals) l) in
215    let 〈l, graph〉 ≝ read int_fun globals graph r (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
216      〈joint_st_goto ? globals l, graph〉
[1154]217  | ertl_st_addr rl rh x l ⇒
[1160]218    let 〈hdw1, l〉 ≝ write int_fun globals graph rh l in
219    let 〈l, graph〉 ≝ l in
220    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw1) l) in
221    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPH) l) in
222    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_address globals x ?) l) in
223    let 〈hdw2, l〉 ≝ write int_fun globals graph rl l in
224    let 〈l, graph〉 ≝ l in
225    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw2) l) in
226    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPL) l) in
227      〈joint_st_sequential ? globals (joint_instr_address globals x ?) l, graph〉
[1154]228(*  | ertl_st_addr_h r x l ⇒
[1160]229    let 〈hdw, l〉 ≝ write int_fun globals graph r l in
230    let 〈l, graph〉 ≝ generate globals graph (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l)) in
231    let 〈l, graph〉 ≝ generate globals graph (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPH) l)) in
[1154]232      ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_address globals x ?) l)
233  | ertl_st_addr_l r x l ⇒
[1160]234    let 〈hdw, l〉 ≝ write int_fun globals graph r l in
235    let 〈l, graph〉 ≝ generate globals graph (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l)) in
236    let 〈l, graph〉 ≝ generate globals graph (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPL) l)) in
[1154]237      ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_address globals x ?) l)
238*)
239  | ertl_st_int r i l ⇒
[1160]240    let 〈hdw, l〉 ≝ write int_fun globals graph r l in
241    let 〈l, graph〉 ≝ l in
242      〈joint_st_sequential ? globals (joint_instr_int globals hdw i) l, graph〉
243  | ertl_st_move r1 r2 l ⇒ move int_fun globals graph (lookup r1) (lookup r2) l
[1154]244  | ertl_st_opaccs opaccs destr1 destr2 srcr1 srcr2 l ⇒
[1160]245    let 〈hdw, l〉 ≝ write int_fun globals graph destr1 l in
246    let 〈l, graph〉 ≝ l in
247    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
248    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l) in
249    let 〈l, graph〉 ≝ read int_fun globals graph srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
250    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
251    let 〈l, graph〉 ≝ read int_fun globals graph srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
252    let 〈l, graph〉 ≝ generate globals graph (joint_st_goto ? globals l) in
253    let 〈hdw, l〉 ≝ write int_fun globals graph destr2 l in
254    let 〈l, graph〉 ≝ l in
255    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
256    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterB) l) in
257    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l) in
258    let 〈l, graph〉 ≝ read int_fun globals graph srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
259    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
260    let 〈l, graph〉 ≝ read int_fun globals graph srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
261      〈joint_st_goto ? globals l, graph〉
[1154]262(*
263  | ertl_st_opaccs_a opaccs destr srcr1 srcr2 l ⇒
[1160]264    let 〈hdw, l〉 ≝ write int_fun globals graph destr l in
265    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
266    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l) in
267    let 〈l, graph〉 ≝ read int_fun globals graph srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
268    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
269    let 〈l, graph〉 ≝ read int_fun globals graph srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
[1154]270      joint_st_goto ? globals l
271  | ertl_st_opaccs_b opaccs destr srcr1 srcr2 l ⇒
[1160]272    let 〈hdw, l〉 ≝ write int_fun globals graph destr l in
273    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
274    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterB) l) in
275    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l) in
276    let 〈l, graph〉 ≝ read int_fun globals graph srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
277    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
278    let 〈l, graph〉 ≝ read int_fun globals graph srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
[1154]279      joint_st_goto ? globals l
280*)
281  | ertl_st_op1 op1 destr srcr l ⇒
[1160]282    let 〈hdw, l〉 ≝ write int_fun globals graph destr l in
283    let 〈l, graph〉 ≝ l in
284    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
285    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_op1 globals op1) l) in
286    let 〈l, graph〉 ≝ read int_fun globals graph srcr (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
287      〈joint_st_goto ? globals l, graph〉
[1154]288  | ertl_st_op2 op2 destr srcr1 srcr2 l ⇒
[1160]289    let 〈hdw, l〉 ≝ write int_fun globals graph destr l in
290    let 〈l, graph〉 ≝ l in
291    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
292    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_op2 globals op2 RegisterB) l) in
293    let 〈l, graph〉 ≝ read int_fun globals graph srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
294    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
295    let 〈l, graph〉 ≝ read int_fun globals graph srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
296      〈joint_st_goto ? globals l, graph〉
297  | ertl_st_clear_carry l ⇒ 〈joint_st_sequential ? globals (joint_instr_clear_carry globals) l, graph〉
298  | ertl_st_set_carry l ⇒ 〈joint_st_sequential ? globals (joint_instr_set_carry globals) l, graph〉
[1154]299  | ertl_st_load destr addr1 addr2 l ⇒
[1160]300    let 〈hdw, l〉 ≝ write int_fun globals graph destr l in
301    let 〈l, graph〉 ≝ l in
302    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
303    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_load globals) l) in
304    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in
305    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterST0) l) in
306    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in
307    let 〈l, graph〉 ≝ read int_fun globals graph addr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
308    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterST0) l) in
309    let 〈l, graph〉 ≝ read int_fun globals graph addr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
310      〈joint_st_goto ? globals l, graph〉
[1154]311  | ertl_st_store addr1 addr2 srcr l ⇒
[1160]312    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_store globals) l) in
313    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterST1) l) in
314    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in
315    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterST0) l) in
316    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in
317    let 〈l, graph〉 ≝ read int_fun globals graph addr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
318    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterST0) l) in
319    let 〈l, graph〉 ≝ read int_fun globals graph addr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
320    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterST1) l) in
321    let 〈l, graph〉 ≝ read int_fun globals graph srcr (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
322      〈joint_st_goto ? globals l, graph〉
323  | ertl_st_call_id f ignore l ⇒ 〈joint_st_sequential ? globals (joint_instr_call_id globals f) l, graph〉
[1154]324  | ertl_st_cond srcr lbl_true lbl_false ⇒
[1160]325    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_cond_acc globals lbl_true) lbl_false) in
326    let 〈l, graph〉 ≝ read int_fun globals graph srcr (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
327      〈joint_st_goto ? globals l, graph〉
328  | ertl_st_return ⇒ 〈joint_st_return ? globals, graph〉
[1154]329  ].
330  cases daemon (* XXX: todo -- proofs regarding gvars *)
331qed.
332
333(* **** *)
334
[1088]335definition translate_internal ≝
[1152]336  λglobals: list ident.
[1088]337  λf.
338  λint_fun: ertl_internal_function.
[1152]339  let lookup ≝ λr.
[1144]340    match lookup r with
[1152]341    | colour_spill ->
[1144]342        ERTLToLTLI.Spill (Interference.Vertex.Map.find (Interference.lookup H.graph r) S.coloring)
[1152]343    | colour_colour color ->
[1144]344        ERTLToLTLI.Color color
345  in
[1152]346  let locals ≝ colour_locals + (ertl_if_stacksize int_fun) in
347  let stacksize ≝ (ertl_if_params int_fun) + locals in
348    mk_ltl_internal_function
349      globals
350      (ertl_if_luniverse int_fun)
351      (ertl_if_runiverse int_fun)
352      stacksize.
[1144]353
354  let () =
355    Label.Map.iter (fun label stmt ->
356      let stmt =
357        match Liveness.eliminable (G.liveafter label) stmt with
358        | Some successor ->
359            LTL.St_skip successor
360        | None ->
361            I.translate_statement stmt
362      in
363      graph := Label.Map.add label stmt !graph
364    ) int_fun.ERTL.f_graph
365  in
366
[1084]367definition translate_funct ≝
368  λname_def.
369  let 〈name, def〉 ≝ name_def in
370  let def' ≝
371    match def with
372    [ Internal def ⇒ Internal ? (translate_internal name def)
373    | External def ⇒ External ? def
374    ]
375  in
376    〈name, def'〉.
377
378definition translate ≝
379  λp.
380  let functs' ≝ map ? ? translate_funct (ertl_pr_functs p) in
381    mk_ltl_program (ertl_pr_globals p) functs' (ertl_pr_main p).
Note: See TracBrowser for help on using the repository browser.