source: src/ERTL/ERTLToLTL.ma @ 1730

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

Files ported to new version of the standard library.
File size: 25.9 KB
Line 
1include "LTL/LTL.ma".
2include "ERTL/Interference.ma".
3include "ASM/Arithmetic.ma".
4
5definition fresh_label ≝
6  λglobals: list ident.
7  λluniv.
8    fresh LabelTag luniv.
9
10definition ltl_statement_graph ≝
11  λglobals.
12    graph … (ltl_statement globals).
13
14definition add_graph ≝
15  λglobals.
16  λlabel.
17  λstmt: ltl_statement globals.
18  λgraph: ltl_statement_graph globals.
19    add LabelTag ? graph label stmt.
20
21definition generate ≝
22  λglobals: list ident.
23  λluniv.
24  λgraph: ltl_statement_graph globals.
25  λstmt: ltl_statement globals.
26  let 〈l, luniv〉 ≝ fresh_label globals luniv in
27  let graph ≝ add_graph globals l stmt graph in
28    〈l, graph, luniv〉.
29
30definition num_locals ≝
31  λspilled_no.
32  λglobals.
33  λint_fun.
34    spilled_no + (joint_if_stacksize globals (ertl_params globals) int_fun).
35
36definition stacksize ≝
37  λspilled_no.
38  λglobals.
39  λint_fun.
40    spilled_no + (joint_if_stacksize globals (ertl_params globals) int_fun).
41
42definition adjust_off ≝
43  λspilled_no.
44  λglobals.
45  λint_fun.
46  λoff.
47  let 〈ignore, int_off〉 ≝ half_add ? int_size off in
48  let 〈sub, ignore〉 ≝ sub_8_with_carry (bitvector_of_nat ? (num_locals spilled_no globals int_fun)) int_off false in
49    sub.
50
51definition get_stack:
52 nat → ∀globals. ertl_internal_function globals → graph (ltl_statement globals) → Register → Byte → label → ? ≝
53  λspilled_no.
54  λglobals: list ident.
55  λint_fun.
56  λgraph: graph (ltl_statement (globals)).
57  λr.
58  λoff.
59  λl.
60  λoriginal_label.
61    let off ≝ adjust_off spilled_no globals int_fun off in
62    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
63    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc r)) l) in
64    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (LOAD … globals it it it) l) in
65    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc RegisterDPH)) l) in
66    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (OP2 … globals Addc it it RegisterSPH) l) in
67    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (INT … globals RegisterA (zero ?)) l) in
68    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc RegisterDPL)) l) in
69    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (OP2 … globals Add it it RegisterSPL) l) in
70      〈add_graph globals original_label (sequential (ltl_params globals) globals (INT … (ltl_params globals) globals RegisterA off) l) graph, luniv〉.
71
72definition set_stack:
73  nat → ∀globals. ertl_internal_function globals → ltl_statement_graph globals → Byte
74    → Register → label → ? ≝
75  λspilled_no.
76  λglobals: list ident.
77  λint_fun.
78  λgraph: graph (ltl_statement (globals)).
79  λoff.
80  λr.
81  λl.
82  λoriginal_label.
83  let off ≝ adjust_off spilled_no globals int_fun off in
84  let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
85  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (STORE … globals it it it) l) in
86  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (to_acc r)) l) in
87  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc RegisterDPH)) l) in
88  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (OP2 … globals Addc it it RegisterSPH) l) in
89  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (INT … globals RegisterA (zero ?)) l) in
90  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc RegisterDPL)) l) in
91  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (OP2 … globals Add it it RegisterSPL) l) in
92    〈add_graph globals original_label (sequential (ltl_params globals) globals (INT … (ltl_params globals) globals RegisterA off) l) graph, luniv〉.
93
94
95definition write ≝
96  λglobals: list ident.
97  λint_fun: ertl_internal_function globals.
98  λvaluation.
99  λcoloured_graph.
100  λgraph.
101  λr.
102  λl.
103  λoriginal_label: label.
104  match colouring valuation coloured_graph (inl … r) with
105  [ decision_spill off ⇒
106    let luniv ≝ joint_if_luniverse … int_fun in
107    let 〈graph, luniv〉 ≝ set_stack (spilled_no … coloured_graph) globals int_fun graph (bitvector_of_nat … off) RegisterSST l original_label in
108      〈RegisterSST, l, graph, luniv〉
109  | decision_colour hwr ⇒
110    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
111      〈hwr, l, graph, luniv〉
112  ].
113
114definition read ≝
115  λglobals: list ident.
116  λint_fun: ertl_internal_function globals.
117  λvaluation.
118  λcoloured_graph.
119  λgraph.
120  λr.
121  λstmt.
122  λoriginal_label: label.
123  match colouring valuation coloured_graph (inl … r) with
124  [ decision_colour hwr ⇒
125    let luniv ≝ joint_if_luniverse … int_fun in
126      〈add_graph globals original_label (stmt hwr) graph, luniv〉
127  | decision_spill off ⇒
128    let temphwr ≝ RegisterSST in
129    let luniv ≝ joint_if_luniverse … int_fun in
130    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (stmt temphwr) in
131      get_stack (spilled_no … coloured_graph) globals int_fun graph temphwr (bitvector_of_nat … off) l original_label
132  ].
133
134definition move ≝
135  λspilled_no.
136  λglobals: list ident.
137  λint_fun.
138  λgraph: graph (ltl_statement globals).
139  λdest: decision.
140  λsrc: decision.
141  λl: label.
142  λoriginal_label: label.
143  match dest with
144  [ decision_colour dest_hwr ⇒
145    match src with
146    [ decision_colour src_hwr ⇒
147      let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
148      if eq_Register dest_hwr src_hwr then
149        〈add_graph globals original_label (GOTO … globals l) graph, luniv〉
150      else
151        let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc dest_hwr)) l) in
152          〈add_graph globals original_label (sequential (ltl_params globals) globals (MOVE … globals (to_acc src_hwr)) l) graph, luniv〉
153    | decision_spill src_off ⇒ get_stack spilled_no globals int_fun graph dest_hwr (bitvector_of_nat … src_off) l original_label
154    ]
155  | decision_spill dest_off ⇒
156    match src with
157    [ decision_colour src_hwr ⇒ set_stack spilled_no globals int_fun graph (bitvector_of_nat … dest_off) src_hwr l original_label
158    | decision_spill src_off ⇒
159      let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
160      if eq_nat dest_off src_off then
161        〈add_graph globals original_label (GOTO … globals l) graph, luniv〉
162      else
163        let temp_hwr ≝ RegisterSST in
164        let 〈graph, luniv〉 ≝ set_stack spilled_no globals int_fun graph (bitvector_of_nat … dest_off) temp_hwr l original_label in
165          get_stack spilled_no globals int_fun graph temp_hwr (bitvector_of_nat … src_off) l original_label
166    ]
167  ].
168
169definition newframe ≝
170  λspilled_no.
171  λglobals: list ident.
172  λint_fun: ertl_internal_function globals.
173  λgraph: ltl_statement_graph globals.
174  λl: label.
175  λoriginal_label: label.
176  if eq_nat (stacksize spilled_no globals int_fun) 0 then
177    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
178      〈add_graph globals original_label (GOTO … globals l) graph, luniv〉
179  else
180    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
181    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc RegisterSPH)) l) in
182    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (OP2 … globals Sub it it RegisterDPH) l) in
183    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (INT … globals RegisterDPH (zero ?)) l) in
184    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (to_acc RegisterSPH)) l) in
185    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc RegisterSPL)) l) in
186    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (OP2 … globals Sub it it RegisterDPL) l) in
187    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (CLEAR_CARRY … globals) l) in
188    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (INT … globals RegisterDPL (bitvector_of_nat ? (stacksize spilled_no globals int_fun))) l) in
189      〈add_graph globals original_label (sequential (ltl_params globals) globals (MOVE … globals (to_acc RegisterSPL)) l) graph, luniv〉.
190
191definition delframe ≝
192  λspilled_no.
193  λglobals.
194  λint_fun.
195  λgraph: graph (ltl_statement globals).
196  λl.
197  λoriginal_label: label.
198  if eq_nat (stacksize spilled_no globals int_fun) 0 then
199    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
200      〈add_graph globals original_label (GOTO (ltl_params globals) globals l) graph, luniv〉
201  else
202    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
203    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc RegisterSPH)) l) in
204    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (OP2 … globals Addc it it RegisterSPH) l) in
205    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (INT … globals RegisterA (zero ?)) l) in
206    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc RegisterSPL)) l) in
207    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (OP2 … globals Add it it RegisterSPL) l) in
208      〈add_graph globals original_label (sequential (ltl_params globals) globals (INT ? globals RegisterA (bitvector_of_nat ? (stacksize spilled_no globals int_fun))) l) graph, luniv〉.
209
210definition translate_statement:
211  ∀globals: list ident. ertl_internal_function globals → ∀v: valuation.
212    coloured_graph v → ltl_statement_graph globals → ertl_statement globals →
213      label → ((ltl_statement_graph globals) × (universe LabelTag)) ≝
214  λglobals: list ident.
215  λint_fun.
216  λvaluation.
217  λcoloured_graph: coloured_graph valuation.
218  λgraph: ltl_statement_graph globals.
219  λstmt: ertl_statement globals.
220  λoriginal_label: label.
221  match stmt with
222  [ sequential seq l ⇒
223    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
224    match seq with
225    [ COMMENT c ⇒
226      〈add_graph globals original_label (sequential … (COMMENT … c) l) graph, luniv〉
227    | COST_LABEL cost_lbl ⇒
228      〈add_graph globals original_label (sequential … (COST_LABEL … cost_lbl) l) graph, luniv〉
229    | POP r ⇒
230      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
231      let int_fun ≝ set_luniverse globals ? int_fun luniv in
232      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph r l fresh_lbl in
233      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc hdw)) l) in
234        〈add_graph globals original_label (sequential ltl_params_ globals (POP … it) l) graph, luniv〉
235    | PUSH r ⇒
236      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (PUSH … globals it) l) in
237      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
238      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
239      let int_fun ≝ set_luniverse globals ? int_fun luniv in
240      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph r (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in
241        〈add_graph globals original_label (GOTO … fresh_lbl) graph, luniv〉
242    | COND srcr lbl_true ⇒
243      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (COND … it lbl_true) l) in
244      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
245      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
246      let int_fun' ≝ set_luniverse globals ? int_fun luniv in
247      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in
248        〈add_graph globals original_label (GOTO … fresh_lbl) graph, luniv〉
249    | CALL_ID f ignore ignore' ⇒ 〈add_graph globals original_label (sequential … (CALL_ID … f ignore ignore') l) graph, luniv〉
250    | STORE addr1 addr2 srcr ⇒
251      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (STORE … it it it) l) in
252      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (to_acc RegisterST1)) l) in
253      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc RegisterDPH)) l) in
254      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (to_acc RegisterST0)) l) in
255      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc RegisterDPL)) l) in
256      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
257      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
258      let int_fun ≝ set_luniverse globals ? int_fun luniv in
259      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr1 (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in
260      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc RegisterST0)) fresh_lbl) in
261      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
262      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
263      let int_fun ≝ set_luniverse globals ? int_fun luniv in
264      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr2 (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in
265      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc RegisterST1)) fresh_lbl) in
266      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
267      let int_fun ≝ set_luniverse globals ? int_fun luniv in
268      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in
269        〈add_graph globals original_label (GOTO … l) graph, luniv〉
270    | LOAD destr addr1 addr2 ⇒
271      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
272      let int_fun ≝ set_luniverse globals ? int_fun luniv in
273      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph destr l fresh_lbl in
274      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc hdw)) l) in
275      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (LOAD … it it it) l) in
276      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc RegisterDPH)) l) in
277      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (to_acc RegisterST0)) l) in
278      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc RegisterDPL)) 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 addr1 (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in
283      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc RegisterST0)) fresh_lbl) in
284      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
285      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
286      let int_fun ≝ set_luniverse globals ? int_fun luniv in
287      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr2 (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in
288        〈add_graph globals original_label (GOTO … fresh_lbl) graph, luniv〉
289    | CLEAR_CARRY ⇒ 〈add_graph globals original_label (sequential … (CLEAR_CARRY …) l) graph, luniv〉
290    | SET_CARRY ⇒ 〈add_graph globals original_label (sequential … (SET_CARRY …) l) graph, luniv〉
291    | OP2 op2 destr srcr1 srcr2 ⇒
292      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
293      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
294      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph destr l fresh_lbl in
295      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc hdw)) l) in
296      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (OP2 … op2 it it RegisterB) l) in
297      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
298      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
299      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr1 (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in
300      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc RegisterB)) fresh_lbl) in
301      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
302      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
303      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr2 (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in
304        〈add_graph globals original_label (GOTO … l) graph, luniv〉
305    | OP1 op1 destr srcr ⇒
306      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
307      let int_fun ≝ set_luniverse globals (ertl_params 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 (sequential … (MOVE … (from_acc hdw)) l) in
310      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (OP1 … op1 it it) l) in
311      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
312      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
313      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
314      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in
315        〈add_graph globals original_label (GOTO … l) graph, luniv〉
316    | INT r i ⇒
317      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
318      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
319      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph r l fresh_lbl in
320        〈add_graph globals original_label (sequential ltl_params_ globals (INT … hdw i) l) graph, luniv〉
321    | MOVE pair_regs ⇒
322      let regl ≝ \fst pair_regs in
323      let regr ≝ \snd pair_regs in
324      match regl with
325      [ pseudo p1  ⇒
326        match regr with
327        [ pseudo p2  ⇒ move (spilled_no … coloured_graph) globals int_fun graph (colouring valuation coloured_graph (inl … p1)) (colouring valuation coloured_graph (inl … p2)) l original_label
328        | hardware h ⇒ move (spilled_no … coloured_graph) globals int_fun graph (colouring valuation coloured_graph (inl … p1)) (decision_colour h) l original_label
329        ]
330      | hardware h1 ⇒
331        match regr with
332        [ pseudo p    ⇒ move (spilled_no … coloured_graph) globals int_fun graph (decision_colour h1) (colouring valuation coloured_graph (inl … p)) l original_label
333        | hardware h2 ⇒
334          let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc h1)) l) in
335            〈add_graph globals original_label (sequential ltl_params_ … (MOVE … (to_acc h2)) l) graph, luniv〉
336        ]
337      ]
338    | ADDRESS lbl prf dpl dph ⇒
339      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
340      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
341      let 〈hdw1, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph dph l fresh_lbl in
342      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc hdw1)) l) in
343      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (to_acc RegisterDPH)) l) in
344      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (ADDRESS … globals lbl prf it it) l) in
345      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
346      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
347      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
348      let 〈hdw2, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph dpl l fresh_lbl in
349      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc hdw2)) l) in
350      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (to_acc RegisterDPL)) l) in
351        〈add_graph globals original_label (sequential ltl_params_ globals (ADDRESS … lbl prf it it) l) graph, luniv〉
352    | extension ext ⇒
353      match ext with
354      [ ertl_st_ext_new_frame ⇒ newframe (spilled_no … coloured_graph)globals int_fun graph l original_label
355      | ertl_st_ext_del_frame ⇒ delframe (spilled_no … coloured_graph) globals int_fun graph l original_label
356      | ertl_st_ext_frame_size r ⇒
357        let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
358        let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
359        let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph r l fresh_lbl in
360          〈add_graph globals original_label (sequential ltl_params_ globals (INT … hdw (bitvector_of_nat … (stacksize (spilled_no … coloured_graph) … int_fun))) l) graph, luniv〉
361      ]
362    | OPACCS opaccs dacc_a_reg dacc_b_reg sacc_a_reg sacc_b_reg ⇒
363      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
364      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph dacc_a_reg l fresh_lbl in
365      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc hdw)) l) in
366      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (OPACCS … opaccs it it it it) l) in
367      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
368      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
369      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
370      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph sacc_a_reg (λhdw. sequential … globals (MOVE … globals (to_acc hdw)) l) fresh_lbl in
371      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc RegisterB)) fresh_lbl) in
372      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
373      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
374      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
375      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph sacc_b_reg (λhdw. sequential … globals (MOVE … globals (to_acc hdw)) l) fresh_lbl in
376        〈add_graph globals original_label (GOTO … globals fresh_lbl) graph, luniv〉
377    ]
378  | RETURN ⇒ 〈add_graph globals original_label (RETURN ltl_params_ globals) graph, joint_if_luniverse globals (ertl_params globals) int_fun〉
379  | GOTO l ⇒ 〈add_graph globals original_label (GOTO ltl_params_ globals l) graph, joint_if_luniverse globals (ertl_params globals) int_fun〉
380  ].
381
382definition graph_fold ≝
383  λglobals.
384  λb : Type[0].
385  λf    : label → ertl_statement globals → b → b.
386  λgraph: graph (ertl_statement globals).
387  λseed : b.
388    foldi (ertl_statement globals) b ? f graph seed.
389
390definition translate_internal: ∀globals: list ident.
391  ertl_internal_function globals → ltl_internal_function globals ≝
392  λglobals: list ident.
393  λint_fun: ertl_internal_function globals.
394  let graph ≝ (empty_map … : ltl_statement_graph globals) in
395  let valuation ≝ analyse globals int_fun in
396  let coloured_graph ≝ build valuation in
397  let 〈graph, luniv〉 ≝ graph_fold globals ((ltl_statement_graph globals) × (universe LabelTag)) (λlabel: label. λstmt: ertl_statement globals. λgraph_luniv: (? × (universe LabelTag)).
398    let 〈graph, luniv〉 ≝ graph_luniv in
399      match eliminable globals (valuation label) stmt with
400      [ Some successor ⇒ 〈add_graph globals label (GOTO … successor) graph, luniv〉
401      | None           ⇒
402        translate_statement globals int_fun valuation coloured_graph graph stmt label
403      ]) (joint_if_code globals (ertl_params globals) int_fun) 〈graph, joint_if_luniverse … int_fun〉
404  in
405    match joint_if_entry … int_fun with
406    [ mk_Sig entry_label entry_label_prf ⇒
407      match joint_if_exit … int_fun with
408      [ mk_Sig exit_label exit_label_prf ⇒
409          mk_joint_internal_function globals (ltl_params globals)
410            luniv (joint_if_runiverse … int_fun)
411              it it it (joint_if_stacksize … int_fun)
412                graph ? ?
413      ]
414    ].
415  [1: %
416    [1: @entry_label
417    |2: cases daemon (* XXX *)
418    ]
419  |2: %
420    [1: @exit_label
421    |2: cases daemon (* XXX *)
422    ]
423  ]
424qed.
425
426definition ertl_to_ltl: ertl_program → ltl_program ≝
427  λp.transform_program … p (transf_fundef … (translate_internal …)).
Note: See TracBrowser for help on using the repository browser.