source: src/ERTL/ERTLToLTLI.ma @ 1124

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

changes to get ertltoltli to compile

File size: 14.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.
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 (joint_st_sequential ? globals (joint_instr_from_acc globals r) l) in
31    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_load globals) l) in
32    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in
33    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Addc RegisterSPH) l) in
34    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_int globals RegisterA (zero ?)) l) in
35    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in
36    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Add RegisterSPL) l) in
37      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 (joint_st_sequential ? globals (joint_instr_store globals) l) in
46  let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals r) l) in
47  let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in
48  let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Addc RegisterSPH) l) in
49  let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_int globals RegisterA (zero ?)) l) in
50  let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in
51  let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Add RegisterSPL) l) in
52    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        joint_st_sequential ? globals (joint_instr_skip globals) l
86      else
87        let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals dest_hwr) l) in
88          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        joint_st_sequential ? globals (joint_instr_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    joint_st_sequential ? globals (joint_instr_skip globals) l
109  else
110    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPH) l) in
111    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Sub RegisterDPH) l) in
112    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_int globals RegisterDPH (zero ?)) l) in
113    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterSPH) l) in
114    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPL) l) in
115    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Sub RegisterDPL) l) in
116    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_clear_carry globals) l) in
117    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_int globals RegisterDPL (bitvector_of_nat ? stacksize)) l) in
118      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    joint_st_sequential ? globals (joint_instr_skip globals) l
125  else
126    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPH) l) in
127    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Addc RegisterSPH) l) in
128    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_int globals RegisterA (zero ?)) l) in
129    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPL) l) in
130    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Add RegisterSPL) l) in
131      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 ⇒ joint_st_sequential ? globals (joint_instr_skip globals) l
138  | ertl_st_comment s l ⇒ joint_st_sequential ? globals (joint_instr_comment globals s) l
139  | ertl_st_cost cost_lbl l ⇒ 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 (joint_st_sequential ? globals (joint_instr_from_acc globals r1) l) in
144      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      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 (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
153      joint_st_sequential ? globals (joint_instr_pop globals) l
154  | ertl_st_push r l ⇒
155    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_push globals) l) in
156    let l ≝ read globals r (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
157      joint_st_sequential ? globals (joint_instr_skip globals) l
158  | ertl_st_addr_h r x l ⇒
159    let 〈hdw, l〉 ≝ write globals r l in
160    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
161    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPH) l) in
162      joint_st_sequential ? globals (joint_instr_address globals x ?) l
163  | ertl_st_addr_l r x l ⇒
164    let 〈hdw, l〉 ≝ write globals r l in
165    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
166    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPL) l) in
167      joint_st_sequential ? globals (joint_instr_address globals x ?) l
168  | ertl_st_int r i l ⇒
169    let 〈hdw, l〉 ≝ write globals r l in
170      joint_st_sequential ? globals (joint_instr_int globals hdw i) l
171  | ertl_st_move r1 r2 l ⇒ move globals (lookup r1) (lookup r2) l
172  | ertl_st_opaccs_a opaccs destr srcr1 srcr2 l ⇒
173    let 〈hdw, l〉 ≝ write globals destr l in
174    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
175    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l) in
176    let l ≝ read globals srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
177    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
178    let l ≝ read globals srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
179      joint_st_sequential ? globals (joint_instr_skip globals) l
180  | ertl_st_opaccs_b opaccs destr srcr1 srcr2 l ⇒
181    let 〈hdw, l〉 ≝ write globals destr l in
182    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
183    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterB) l) in
184    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l) in
185    let l ≝ read globals srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
186    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
187    let l ≝ read globals srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
188      joint_st_sequential ? globals (joint_instr_skip globals) l
189  | ertl_st_op1 op1 destr srcr l ⇒
190    let 〈hdw, l〉 ≝ write globals destr 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_op1 globals op1) l) in
193    let l ≝ read globals srcr (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
194      joint_st_sequential ? globals (joint_instr_skip globals) l
195  | ertl_st_op2 op2 destr srcr1 srcr2 l ⇒
196    let 〈hdw, l〉 ≝ write globals destr l in
197    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
198    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals op2 RegisterB) l) in
199    let l ≝ read globals srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
200    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
201    let l ≝ read globals srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
202      joint_st_sequential ? globals (joint_instr_skip globals) l
203  | ertl_st_clear_carry l ⇒ joint_st_sequential ? globals (joint_instr_clear_carry globals) l
204  | ertl_st_set_carry l ⇒ joint_st_sequential ? globals (joint_instr_set_carry globals) l
205  | ertl_st_load destr addr1 addr2 l ⇒
206    let 〈hdw, l〉 ≝ write globals destr l in
207    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
208    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_load globals) l) in
209    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in
210    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterST0) l) in
211    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in
212    let l ≝ read globals addr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
213    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterST0) l) in
214    let l ≝ read globals addr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
215      joint_st_sequential ? globals (joint_instr_skip globals) l
216  | ertl_st_store addr1 addr2 srcr l ⇒
217    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_store globals) l) in
218    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterST1) l) in
219    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in
220    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterST0) l) in
221    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in
222    let l ≝ read globals addr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
223    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterST0) l) in
224    let l ≝ read globals addr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
225    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterST1) l) in
226    let l ≝ read globals srcr (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
227      joint_st_sequential ? globals (joint_instr_skip globals) l
228  | ertl_st_call_id f ignore l ⇒  joint_st_sequential ? globals (joint_instr_call_id globals f) l
229  | ertl_st_cond srcr lbl_true lbl_false ⇒
230    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_cond_acc globals lbl_true) lbl_false) in
231    let l ≝ read globals srcr (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
232      joint_st_sequential ? globals (joint_instr_skip globals) l
233  | ertl_st_return ⇒ joint_st_return ? globals
234  ].
235  cases daemon (* XXX: todo -- proofs regarding gvars *)
236qed.
Note: See TracBrowser for help on using the repository browser.