source: src/ERTL/ERTLToLTL.ma @ 1423

Last change on this file since 1423 was 1423, checked in by sacerdot, 9 years ago
  • spill no longer used
  • BUG IN Interference: generating the destruct principle takes too long
  • ERTLToLTL not compiling ATM
File size: 27.2 KB
Line 
1include "ERTL/ERTL.ma".
2include "LTL/LTL.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 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 globals int_fun graph temphwr (bitvector_of_nat … off) l original_label
132  ].
133
134definition move ≝
135  λglobals: list ident.
136  λint_fun.
137  λgraph: graph (ltl_statement globals).
138  λdest: decision.
139  λsrc: decision.
140  λl: label.
141  λoriginal_label: label.
142  match dest with
143  [ decision_colour dest_hwr ⇒
144    match src with
145    [ decision_colour src_hwr ⇒
146      let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
147      if eq_Register dest_hwr src_hwr then
148        〈add_graph globals original_label (GOTO … globals l) graph, luniv〉
149      else
150        let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc dest_hwr)) l) in
151          〈add_graph globals original_label (sequential (ltl_params globals) globals (MOVE … globals (to_acc src_hwr)) l) graph, luniv〉
152    | decision_spill src_off ⇒ get_stack globals int_fun graph dest_hwr (bitvector_of_nat … src_off) l original_label
153    ]
154  | decision_spill dest_off ⇒
155    match src with
156    [ decision_colour src_hwr ⇒ set_stack globals int_fun graph (bitvector_of_nat … dest_off) src_hwr l original_label
157    | decision_spill src_off ⇒
158      let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
159      if eq_nat dest_off src_off then
160        〈add_graph globals original_label (GOTO … globals l) graph, luniv〉
161      else
162        let temp_hwr ≝ RegisterSST in
163        let 〈graph, luniv〉 ≝ set_stack globals int_fun graph (bitvector_of_nat … dest_off) temp_hwr l original_label in
164          get_stack globals int_fun graph temp_hwr (bitvector_of_nat … src_off) l original_label
165    ]
166  ].
167
168definition newframe ≝
169  λglobals: list ident.
170  λint_fun: ertl_internal_function globals.
171  λgraph: ltl_statement_graph globals.
172  λl: label.
173  λoriginal_label: label.
174  if eq_nat (stacksize globals int_fun) 0 then
175    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
176      〈add_graph globals original_label (GOTO … globals l) graph, luniv〉
177  else
178    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
179    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc RegisterSPH)) l) in
180    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (OP2 … globals Sub it it RegisterDPH) l) in
181    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (INT … globals RegisterDPH (zero ?)) l) in
182    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (to_acc RegisterSPH)) l) in
183    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc RegisterSPL)) l) in
184    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (OP2 … globals Sub it it RegisterDPL) l) in
185    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (CLEAR_CARRY … globals) l) in
186    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (INT … globals RegisterDPL (bitvector_of_nat ? (stacksize globals int_fun))) l) in
187      〈add_graph globals original_label (sequential (ltl_params globals) globals (MOVE … globals (to_acc RegisterSPL)) l) graph, luniv〉.
188
189definition delframe ≝
190  λglobals.
191  λint_fun.
192  λgraph: graph (ltl_statement globals).
193  λl.
194  λoriginal_label: label.
195  if eq_nat (stacksize globals int_fun) 0 then
196    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
197      〈add_graph globals original_label (GOTO (ltl_params globals) globals l) graph, luniv〉
198  else
199    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
200    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc RegisterSPH)) l) in
201    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (OP2 … globals Addc it it RegisterSPH) l) in
202    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (INT … globals RegisterA (zero ?)) l) in
203    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc RegisterSPL)) l) in
204    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (OP2 … globals Add it it RegisterSPL) l) in
205      〈add_graph globals original_label (sequential (ltl_params globals) globals (INT ? globals RegisterA (bitvector_of_nat ? (stacksize globals int_fun))) l) graph, luniv〉.
206
207definition translate_statement:
208  ∀globals: list ident. ertl_internal_function globals → ∀v: valuation.
209    coloured_graph v → ltl_statement_graph globals → ertl_statement globals →
210      label → ((ltl_statement_graph globals) × (universe LabelTag)) ≝
211  λglobals: list ident.
212  λint_fun.
213  λvaluation.
214  λcoloured_graph: coloured_graph valuation.
215  λgraph: ltl_statement_graph globals.
216  λstmt: ertl_statement globals.
217  λoriginal_label: label.
218  match stmt with
219  [ sequential seq l ⇒
220    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
221    match seq with
222    [ COMMENT c ⇒
223      〈add_graph globals original_label (sequential … (COMMENT … c) l) graph, luniv〉
224    | COST_LABEL cost_lbl ⇒
225      〈add_graph globals original_label (sequential … (COST_LABEL … cost_lbl) l) graph, luniv〉
226    | POP r ⇒
227      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
228      let int_fun ≝ set_luniverse globals ? int_fun luniv in
229      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph r l fresh_lbl in
230      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc hdw)) l) in
231        〈add_graph globals original_label (sequential ltl_params_ globals (POP … it) l) graph, luniv〉
232    | PUSH r ⇒
233      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (PUSH … globals it) l) in
234      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
235      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
236      let int_fun ≝ set_luniverse globals ? int_fun luniv in
237      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph r (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in
238        〈add_graph globals original_label (GOTO … fresh_lbl) graph, luniv〉
239    | COND srcr lbl_true ⇒
240      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (COND … it lbl_true) l) in
241      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
242      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
243      let int_fun' ≝ set_luniverse globals ? int_fun luniv in
244      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in
245        〈add_graph globals original_label (GOTO … fresh_lbl) graph, luniv〉
246    | CALL_ID f ignore ignore' ⇒ 〈add_graph globals original_label (sequential … (CALL_ID … f ignore ignore') l) graph, luniv〉
247    | STORE addr1 addr2 srcr ⇒
248      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (STORE … it it it) l) in
249      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (to_acc RegisterST1)) l) in
250      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc RegisterDPH)) l) in
251      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (to_acc RegisterST0)) l) in
252      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc RegisterDPL)) l) in
253      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
254      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
255      let int_fun ≝ set_luniverse globals ? int_fun luniv in
256      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr1 (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in
257      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc RegisterST0)) fresh_lbl) in
258      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
259      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
260      let int_fun ≝ set_luniverse globals ? int_fun luniv in
261      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr2 (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in
262      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc RegisterST1)) fresh_lbl) in
263      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
264      let int_fun ≝ set_luniverse globals ? int_fun luniv in
265      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in
266        〈add_graph globals original_label (GOTO … l) graph, luniv〉
267    | LOAD destr addr1 addr2 ⇒
268      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
269      let int_fun ≝ set_luniverse globals ? int_fun luniv in
270      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph destr l fresh_lbl in
271      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc hdw)) l) in
272      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (LOAD … it it it) l) in
273      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc RegisterDPH)) l) in
274      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (to_acc RegisterST0)) l) in
275      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc RegisterDPL)) l) in
276      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
277      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
278      let int_fun ≝ set_luniverse globals ? int_fun luniv in
279      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr1 (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in
280      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc RegisterST0)) fresh_lbl) in
281      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
282      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
283      let int_fun ≝ set_luniverse globals ? int_fun luniv in
284      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr2 (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in
285        〈add_graph globals original_label (GOTO … fresh_lbl) graph, luniv〉
286    | CLEAR_CARRY ⇒ 〈add_graph globals original_label (sequential … (CLEAR_CARRY …) l) graph, luniv〉
287    | SET_CARRY ⇒ 〈add_graph globals original_label (sequential … (SET_CARRY …) l) graph, luniv〉
288    | OP2 op2 destr srcr1 srcr2 ⇒
289      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
290      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
291      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph destr l fresh_lbl in
292      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc hdw)) l) in
293      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (OP2 … op2 it it RegisterB) l) in
294      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
295      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
296      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr1 (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in
297      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc RegisterB)) fresh_lbl) in
298      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
299      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
300      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr2 (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in
301        〈add_graph globals original_label (GOTO … l) graph, luniv〉
302    | OP1 op1 destr srcr ⇒
303      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
304      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
305      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph destr l fresh_lbl in
306      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc hdw)) l) in
307      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (OP1 … op1 it it) l) in
308      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
309      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
310      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
311      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in
312        〈add_graph globals original_label (GOTO … l) graph, luniv〉
313    | INT r i ⇒
314      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
315      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
316      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph r l fresh_lbl in
317        〈add_graph globals original_label (sequential ltl_params_ globals (INT … hdw i) l) graph, luniv〉
318    | MOVE pair_regs ⇒
319      let regl ≝ \fst pair_regs in
320      let regr ≝ \snd pair_regs in
321      match regl with
322      [ pseudo p1  ⇒
323        match regr with
324        [ pseudo p2  ⇒ move globals int_fun graph (colouring valuation coloured_graph (inl … p1)) (colouring valuation coloured_graph (inl … p2)) l original_label
325        | hardware h ⇒ move globals int_fun graph (colouring valuation coloured_graph (inl … p1)) (decision_colour h) l original_label
326        ]
327      | hardware h1 ⇒
328        match regr with
329        [ pseudo p    ⇒ move globals int_fun graph (decision_colour h1) (colouring valuation coloured_graph (inl … p)) l original_label
330        | hardware h2 ⇒
331          let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc h1)) l) in
332            〈add_graph globals original_label (sequential ltl_params_ … (MOVE … (to_acc h2)) l) graph, luniv〉
333        ]
334      ]
335    | ADDRESS lbl prf dpl dph ⇒
336      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
337      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
338      let 〈hdw1, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph dph l fresh_lbl in
339      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc hdw1)) l) in
340      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (to_acc RegisterDPH)) l) in
341      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (ADDRESS … globals lbl prf it it) l) in
342      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
343      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
344      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
345      let 〈hdw2, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph dpl l fresh_lbl in
346      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc hdw2)) l) in
347      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (to_acc RegisterDPL)) l) in
348        〈add_graph globals original_label (sequential ltl_params_ globals (ADDRESS … lbl prf it it) l) graph, luniv〉
349    | extension ext ⇒
350      match ext with
351      [ ertl_st_ext_new_frame ⇒ newframe globals int_fun graph l original_label
352      | ertl_st_ext_del_frame ⇒ delframe globals int_fun graph l original_label
353      | ertl_st_ext_frame_size r ⇒
354        let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
355        let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
356        let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph r l fresh_lbl in
357          〈add_graph globals original_label (sequential ltl_params_ globals (INT … hdw (bitvector_of_nat … (stacksize … int_fun))) l) graph, luniv〉
358      ]
359    | OPACCS opaccs dacc_a_reg dacc_b_reg sacc_a_reg sacc_b_reg ⇒
360      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
361      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph dacc_a_reg l fresh_lbl in
362      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc hdw)) l) in
363      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (OPACCS … opaccs it it it it) l) in
364      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
365      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
366      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
367      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
368      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc RegisterB)) fresh_lbl) in
369      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
370      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
371      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
372      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
373        〈add_graph globals original_label (GOTO … globals fresh_lbl) graph, luniv〉
374    ]
375  | RETURN ⇒ 〈add_graph globals original_label (RETURN ltl_params_ globals) graph, joint_if_luniverse globals (ertl_params globals) int_fun〉
376  | GOTO l ⇒ 〈add_graph globals original_label (GOTO ltl_params_ globals l) graph, joint_if_luniverse globals (ertl_params globals) int_fun〉
377  ].
378
379lemma Sm_leq_n_m_leq_n:
380  ∀m, n: nat.
381    S m ≤ n → m ≤ n.
382  #m #n /2/
383qed.
384
385let rec fold_aux
386  (a, b: Type[0]) (f: BitVector 16 → a → b → b) (seed: b) (n: nat)
387    on n: n ≤ 16 → BitVectorTrie a n → BitVector (16 - n) → b ≝
388  match n return λn: nat. n ≤ 16 → BitVectorTrie a n → BitVector (16 - n) → b with
389  [ O    ⇒ λinvariant: 0 ≤ 16. λtrie: BitVectorTrie a 0. λpath: BitVector 16.
390    match trie return λx: nat. λtrie': BitVectorTrie a x. ∀prf: x = 0. b with
391    [ Leaf l      ⇒ λproof. f path l seed
392    | Stub s      ⇒ λproof. seed
393    | Node n' l r ⇒ λabsrd. ⊥
394    ] (refl … 0)
395  | S n' ⇒ λinvariant: S n' ≤ 16. λtrie: BitVectorTrie a (S n'). λpath: BitVector (16 - S n').
396    match trie return λx: nat. λtrie': BitVectorTrie a x. ∀prf: x = S n'. b with
397    [ Leaf l      ⇒ λabsrd. ⊥
398    | Stub s      ⇒ λproof. seed
399    | Node n'' l r ⇒ λproof.
400        fold_aux a b f (fold_aux a b f seed n' ? (l⌈BitVectorTrie a n'' ↦ BitVectorTrie a n'⌉) ((false:::path)⌈S (16 - S n') ↦ 16 - n'⌉)) n' ? (r⌈BitVectorTrie a n'' ↦ BitVectorTrie a n'⌉) ((true:::path)⌈S (16 - S n') ↦ 16 - n'⌉)
401    ] (refl … (S n'))
402  ].
403  [ 1, 2: destruct(absrd)
404  | 3,8: >minus_S_S <minus_Sn_m // @le_S_S_to_le //
405  | 4,7: destruct(proof) %
406  | 5,6: @Sm_leq_n_m_leq_n // ]
407qed.
408
409definition bvt_fold ≝
410  λa, b: Type[0].
411  λf: label → a → b → b.
412  λtrie: BitVectorTrie a 16.
413  λseed: b.
414    let f' ≝ λbv: BitVector 16. λa. λb.
415      f (an_identifier LabelTag bv) a b
416    in
417      fold_aux a b f' seed 16 ? trie [[]].
418  //
419qed.
420
421definition graph_fold ≝
422  λglobals.
423  λb : Type[0].
424  λf    : label → ertl_statement globals → b → b.
425  λgraph: graph (ertl_statement globals).
426  λseed : b.
427  match graph with
428  [ an_id_map tree ⇒ bvt_fold (ertl_statement globals) b f tree seed
429  ]. 
430
431definition translate_internal: ∀globals: list ident.
432  ertl_internal_function globals → ltl_internal_function globals ≝
433  λglobals: list ident.
434  λint_fun: ertl_internal_function globals.
435  let graph ≝ (empty_map … : ltl_statement_graph globals) in
436  let valuation ≝ analyse globals int_fun in
437  let coloured_graph ≝ build valuation in
438  let 〈graph, luniv〉 ≝ graph_fold globals ((ltl_statement_graph globals) × (universe LabelTag)) (λlabel: label. λstmt: ertl_statement globals. λgraph_luniv: (? × (universe LabelTag)).
439    let 〈graph, luniv〉 ≝ graph_luniv in
440      match eliminable globals (valuation label) stmt with
441      [ Some successor ⇒ 〈add_graph globals label (GOTO … successor) graph, luniv〉
442      | None           ⇒
443        translate_statement globals int_fun valuation coloured_graph graph stmt label
444      ]) (joint_if_code globals (ertl_params globals) int_fun) 〈graph, joint_if_luniverse … int_fun〉
445  in
446    match joint_if_entry … int_fun with
447    [ dp entry_label entry_label_prf ⇒
448      match joint_if_exit … int_fun with
449      [ dp exit_label exit_label_prf ⇒
450          mk_joint_internal_function globals (ltl_params globals)
451            luniv (joint_if_runiverse … int_fun)
452              it it it (joint_if_stacksize … int_fun)
453                graph ? ?
454      ]
455    ].
456  [1: %
457    [1: @entry_label
458    |2: cases daemon (* XXX *)
459    ]
460  |2: %
461    [1: @exit_label
462    |2: cases daemon (* XXX *)
463    ]
464  ]
465qed.
466
467definition ertl_to_ltl: ertl_program → ltl_program ≝
468  λp.transform_program … p (transf_fundef … (translate_internal …)).
Note: See TracBrowser for help on using the repository browser.