source: src/ERTL/ERTLToLTLI.ma @ 1131

Last change on this file since 1131 was 1131, checked in by mulligan, 8 years ago

changes to syntax of ertl: removed ertl_st_addr_l and ertl_st_addr_h in favourn of unified instruction ertl_st_addr

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