source: src/ERTL/ERTLToLTLI.ma @ 1154

Last change on this file since 1154 was 1154, checked in by mulligan, 9 years ago

changes to ertl files: in process of removing ertltoltli.ma in favour or merge with ertltoltl.ma due to constraints imposed by functorised o'caml code

File size: 16.0 KB
Line 
1include "ERTL/ERTL.ma".
2include "LTL/LTL.ma".
3include "ASM/Arithmetic.ma".
4
5inductive decision: Type[0] ≝
6  | decision_spill: Byte → decision
7  | decision_colour: Register → decision.
8 
9(* these are supplied to the functor, fill in later *)
10axiom lookup: register → decision.
11axiom generate: ∀globals: list ident. ltl_statement globals → label.
12axiom fresh_label: ∀globals: list ident. ltl_function_definition globals → ltl_function_definition globals × label.
13axiom add_graph: ∀globals. label → ltl_statement globals → ltl_statement_graph globals → ltl_statement_graph globals.
14axiom num_locals: nat.
15
16definition num_locals ≝
17  λint_fun.
18    colour_locals + (ertl_if_stacksize int_fun).
19
20definition stacksize ≝
21  λint_fun.
22    colour_locals + (ertl_if_stacksize int_fun).
23(* *** *)
24
25definition adjust_off ≝
26  λoff.
27  let 〈ignore, int_off〉 ≝ half_add ? int_size off in
28  let 〈sub, ignore〉 ≝ sub_8_with_carry (bitvector_of_nat ? num_locals) int_off false in
29    sub.
30
31definition get_stack ≝
32  λglobals.
33  λr.
34  λoff.
35  λl.
36    let off ≝ adjust_off off in
37    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals r) l) in
38    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_load globals) l) in
39    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in
40    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Addc RegisterSPH) l) in
41    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_int globals RegisterA (zero ?)) l) in
42    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in
43    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Add RegisterSPL) l) in
44      joint_st_sequential ? globals (joint_instr_int globals RegisterA off) l.
45
46definition set_stack ≝
47  λglobals.
48  λoff.
49  λr.
50  λl.
51  let off ≝ adjust_off off in
52  let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_store globals) l) in
53  let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals r) l) in
54  let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in
55  let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Addc RegisterSPH) l) in
56  let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_int globals RegisterA (zero ?)) l) in
57  let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in
58  let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Add RegisterSPL) l) in
59    joint_st_sequential ? globals (joint_instr_int globals RegisterA off) l.
60
61definition write ≝
62  λglobals.
63  λr: register.
64  λl: label.
65  match lookup r with
66  [ decision_spill off ⇒ 〈RegisterSST, generate globals (set_stack globals off RegisterSST l)〉
67  | decision_colour hwr ⇒ 〈hwr, l〉
68  ].
69
70definition read ≝
71  λglobals.
72  λr: register.
73  λstmt: Register → ltl_statement globals.
74  match lookup r with
75  [ decision_colour hwr ⇒ generate globals (stmt hwr)
76  | decision_spill off ⇒
77    let temphwr ≝ RegisterSST in
78    let l ≝ generate globals (stmt temphwr) in
79      generate globals (get_stack globals temphwr off l)
80  ].
81
82definition move ≝
83  λglobals: list ident.
84  λdest: decision.
85  λsrc: decision.
86  λl: label.
87  match dest with
88  [ decision_colour dest_hwr ⇒
89    match src with
90    [ decision_colour src_hwr ⇒
91      if eq_Register dest_hwr src_hwr then
92        joint_st_goto ? globals l
93      else
94        let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals dest_hwr) l) in
95          joint_st_sequential ? globals (joint_instr_to_acc globals src_hwr) l
96    | decision_spill src_off ⇒ get_stack globals dest_hwr src_off l
97    ]
98  | decision_spill dest_off ⇒
99    match src with
100    [ decision_colour src_hwr ⇒ set_stack globals dest_off src_hwr l
101    | decision_spill src_off ⇒
102      if eq_bv ? dest_off src_off then
103        joint_st_goto ? globals l
104      else
105        let temp_hwr ≝ RegisterSST in
106        let l ≝ generate globals (set_stack globals dest_off temp_hwr l) in
107          get_stack globals temp_hwr src_off l
108    ]
109  ].
110
111definition newframe ≝
112  λglobals.
113  λl.
114  if eq_nat stacksize 0 then
115    joint_st_goto ? globals l
116  else
117    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPH) l) in
118    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Sub RegisterDPH) l) in
119    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_int globals RegisterDPH (zero ?)) l) in
120    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterSPH) l) in
121    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPL) l) in
122    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Sub RegisterDPL) l) in
123    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_clear_carry globals) l) in
124    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_int globals RegisterDPL (bitvector_of_nat ? stacksize)) l) in
125      joint_st_sequential ? globals (joint_instr_to_acc globals RegisterSPL) l.
126
127definition delframe ≝
128  λglobals.
129  λl.
130  if eq_nat stacksize 0 then
131    joint_st_goto ? globals l
132  else
133    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPH) l) in
134    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Addc RegisterSPH) l) in
135    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_int globals RegisterA (zero ?)) l) in
136    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPL) l) in
137    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Add RegisterSPL) l) in
138      joint_st_sequential ? globals (joint_instr_int globals RegisterA (bitvector_of_nat ? stacksize)) l.
139
140definition translate_statement ≝
141  λglobals: list ident.
142  λstmt: ertl_statement.
143  match stmt with
144  [ ertl_st_skip l ⇒ joint_st_goto ? globals l
145  | ertl_st_comment s l ⇒ joint_st_sequential ? globals (joint_instr_comment globals s) l
146  | ertl_st_cost cost_lbl l ⇒ joint_st_sequential ? globals (joint_instr_cost_label globals cost_lbl) l
147  | ertl_st_get_hdw destr sourcehwr l ⇒ move globals (lookup destr) (decision_colour sourcehwr) l
148  | ertl_st_set_hdw desthwr srcr l ⇒ move globals (decision_colour desthwr) (lookup srcr) l
149  | ertl_st_hdw_to_hdw r1 r2 l ⇒
150    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals r1) l) in
151      joint_st_sequential ? globals (joint_instr_to_acc globals r2) l
152  | ertl_st_new_frame l ⇒ newframe globals l
153  | ertl_st_del_frame l ⇒ delframe globals l
154  | ertl_st_frame_size r l ⇒
155    let 〈hdw, l〉 ≝ write globals r l in
156      joint_st_sequential ? globals (joint_instr_int globals hdw (bitvector_of_nat ? stacksize)) l
157  | ertl_st_pop r l ⇒
158    let 〈hdw, l〉 ≝ write globals r l in
159    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
160      joint_st_sequential ? globals (joint_instr_pop globals) l
161  | ertl_st_push r l ⇒
162    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_push globals) l) in
163    let l ≝ read globals r (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
164      joint_st_goto ? globals l
165  | ertl_st_addr rl rh x l ⇒
166    let 〈hdw1, l〉 ≝ write globals rh l in
167    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw1) l) in
168    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPH) l) in
169    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_address globals x ?) l) in
170    let 〈hdw2, l〉 ≝ write globals rl l in
171    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw2) l) in
172    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPL) l) in
173      joint_st_sequential ? globals (joint_instr_address globals x ?) l
174(*  | ertl_st_addr_h r x l ⇒
175    let 〈hdw, l〉 ≝ write globals r l in
176    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l)) in
177    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPH) l)) in
178      ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_address globals x ?) l)
179  | ertl_st_addr_l r x l ⇒
180    let 〈hdw, l〉 ≝ write globals r l in
181    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l)) in
182    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPL) l)) in
183      ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_address globals x ?) l)
184*)
185  | ertl_st_int r i l ⇒
186    let 〈hdw, l〉 ≝ write globals r l in
187      joint_st_sequential ? globals (joint_instr_int globals hdw i) l
188  | ertl_st_move r1 r2 l ⇒ move globals (lookup r1) (lookup r2) l
189  | ertl_st_opaccs opaccs destr1 destr2 srcr1 srcr2 l ⇒
190    let 〈hdw, l〉 ≝ write globals destr1 l in
191    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
192    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l) in
193    let l ≝ read globals srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
194    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
195    let l ≝ read globals srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
196    let l ≝ generate globals (joint_st_goto ? globals l) in
197    let 〈hdw, l〉 ≝ write globals destr2 l in
198    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
199    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterB) l) in
200    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l) in
201    let l ≝ read globals srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
202    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
203    let l ≝ read globals srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
204      joint_st_goto ? globals l
205(*
206  | ertl_st_opaccs_a opaccs destr srcr1 srcr2 l ⇒
207    let 〈hdw, l〉 ≝ write globals destr l in
208    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
209    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l) in
210    let l ≝ read globals srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
211    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
212    let l ≝ read globals srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
213      joint_st_goto ? globals l
214  | ertl_st_opaccs_b opaccs destr srcr1 srcr2 l ⇒
215    let 〈hdw, l〉 ≝ write globals destr l in
216    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
217    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterB) l) in
218    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l) in
219    let l ≝ read globals srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
220    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
221    let l ≝ read globals srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
222      joint_st_goto ? globals l
223*)
224  | ertl_st_op1 op1 destr srcr l ⇒
225    let 〈hdw, l〉 ≝ write globals destr l in
226    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
227    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op1 globals op1) l) in
228    let l ≝ read globals srcr (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
229      joint_st_goto ? globals l
230  | ertl_st_op2 op2 destr srcr1 srcr2 l ⇒
231    let 〈hdw, l〉 ≝ write globals destr l in
232    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
233    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals op2 RegisterB) l) in
234    let l ≝ read globals srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
235    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
236    let l ≝ read globals srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
237      joint_st_goto ? globals l
238  | ertl_st_clear_carry l ⇒ joint_st_sequential ? globals (joint_instr_clear_carry globals) l
239  | ertl_st_set_carry l ⇒ joint_st_sequential ? globals (joint_instr_set_carry globals) l
240  | ertl_st_load destr addr1 addr2 l ⇒
241    let 〈hdw, l〉 ≝ write globals destr l in
242    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
243    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_load globals) l) in
244    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in
245    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterST0) l) in
246    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in
247    let l ≝ read globals addr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
248    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterST0) l) in
249    let l ≝ read globals addr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
250      joint_st_goto ? globals l
251  | ertl_st_store addr1 addr2 srcr l ⇒
252    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_store globals) l) in
253    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterST1) l) in
254    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in
255    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterST0) l) in
256    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in
257    let l ≝ read globals addr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
258    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterST0) l) in
259    let l ≝ read globals addr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
260    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterST1) l) in
261    let l ≝ read globals srcr (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
262      joint_st_goto ? globals l
263  | ertl_st_call_id f ignore l ⇒ joint_st_sequential ? globals (joint_instr_call_id globals f) l
264  | ertl_st_cond srcr lbl_true lbl_false ⇒
265    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_cond_acc globals lbl_true) lbl_false) in
266    let l ≝ read globals srcr (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
267      joint_st_goto ? globals l
268  | ertl_st_return ⇒ joint_st_return ? globals
269  ].
270  cases daemon (* XXX: todo -- proofs regarding gvars *)
271qed.
Note: See TracBrowser for help on using the repository browser.