source: Deliverables/D3.3/id-lookup-branch/ERTL/ERTLToLTL.ma

Last change on this file was 1311, checked in by campbell, 9 years ago

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