source: src/ERTL/ERTLToLTL.ma @ 1515

Last change on this file since 1515 was 1515, checked in by campbell, 10 years ago

Add type of maps on positive binary numbers, and use them for identifers.

Also:

  • fix interpretation for - on positives
  • move eq_nat_dec to a more appropriate place
  • split out costs from other identifiers in ASM
  • use identifier abstractions in back-end
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    [ dp entry_label entry_label_prf ⇒
407      match joint_if_exit … int_fun with
408      [ dp 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.