source: src/ERTL/ERTLToLTLI.ma @ 1083

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

ertl --> ltl statement generation nearly complete. required some changes to ltl and below

File size: 11.1 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  | _ ⇒ ?
159  ].
160
161  let translate_statement (stmt : ERTL.statement) : LTL.statement =
162    match stmt with
163
164      | ERTL.St_addrH (r, x, l) ->
165        let (hdw, l) = write r l in
166        let l = generate (LTL.St_from_acc (hdw, l)) in
167        let l = generate (LTL.St_to_acc (I8051.dph, l)) in
168        LTL.St_addr (x, l)
169
170      | ERTL.St_addrL (r, x, l) ->
171        let (hdw, l) = write r l in
172        let l = generate (LTL.St_from_acc (hdw, l)) in
173        let l = generate (LTL.St_to_acc (I8051.dpl, l)) in
174        LTL.St_addr (x, l)
175
176      | ERTL.St_int (r, i, l) ->
177        let (hdw, l) = write r l in
178        LTL.St_int (hdw, i, l)
179
180      | ERTL.St_move (r1, r2, l) ->
181        move (lookup r1) (lookup r2) l
182
183      | ERTL.St_opaccsA (opaccs, destr, srcr1, srcr2, l) ->
184        let (hdw, l) = write destr l in
185        let l = generate (LTL.St_from_acc (hdw, l)) in
186        let l = generate (LTL.St_opaccs (opaccs, l)) in
187        let l = read srcr1 (fun hdw -> LTL.St_to_acc (hdw, l)) in
188        let l = generate (LTL.St_from_acc (I8051.b, l)) in
189        let l = read srcr2 (fun hdw -> LTL.St_to_acc (hdw, l)) in
190        LTL.St_skip l
191
192      | ERTL.St_opaccsB (opaccs, destr, srcr1, srcr2, l) ->
193        let (hdw, l) = write destr l in
194        let l = generate (LTL.St_from_acc (hdw, l)) in
195        let l = generate (LTL.St_to_acc (I8051.b, l)) in
196        let l = generate (LTL.St_opaccs (opaccs, l)) in
197        let l = read srcr1 (fun hdw -> LTL.St_to_acc (hdw, l)) in
198        let l = generate (LTL.St_from_acc (I8051.b, l)) in
199        let l = read srcr2 (fun hdw -> LTL.St_to_acc (hdw, l)) in
200        LTL.St_skip l
201
202      | ERTL.St_op1 (op1, destr, srcr, l) ->
203        let (hdw, l) = write destr l in
204        let l = generate (LTL.St_from_acc (hdw, l)) in
205        let l = generate (LTL.St_op1 (op1, l)) in
206        let l = read srcr (fun hdw -> LTL.St_to_acc (hdw, l)) in
207        LTL.St_skip l
208
209      | ERTL.St_op2 (op2, destr, srcr1, srcr2, l) ->
210        let (hdw, l) = write destr l in
211        let l = generate (LTL.St_from_acc (hdw, l)) in
212        let l = generate (LTL.St_op2 (op2, I8051.b, l)) in
213        let l = read srcr1 (fun hdw -> LTL.St_to_acc (hdw, l)) in
214        let l = generate (LTL.St_from_acc (I8051.b, l)) in
215        let l = read srcr2 (fun hdw -> LTL.St_to_acc (hdw, l)) in
216        LTL.St_skip l
217
218      | ERTL.St_clear_carry l ->
219        LTL.St_clear_carry l
220
221      | ERTL.St_set_carry l ->
222        LTL.St_set_carry l
223
224      | ERTL.St_load (destr, addr1, addr2, l) ->
225        let (hdw, l) = write destr l in
226        let l = generate (LTL.St_from_acc (hdw, l)) in
227        let l = generate (LTL.St_load l) in
228        let l = generate (LTL.St_from_acc (I8051.dph, l)) in
229        let l = generate (LTL.St_to_acc (I8051.st0, l)) in
230        let l = generate (LTL.St_from_acc (I8051.dpl, l)) in
231        let l = read addr1 (fun hdw -> LTL.St_to_acc (hdw, l)) in
232        let l = generate (LTL.St_from_acc (I8051.st0, l)) in
233        let l = read addr2 (fun hdw -> LTL.St_to_acc (hdw, l)) in
234        LTL.St_skip l
235
236      | ERTL.St_store (addr1, addr2, srcr, l) ->
237        let l = generate (LTL.St_store l) in
238        let l = generate (LTL.St_to_acc (I8051.st1, l)) in
239        let l = generate (LTL.St_from_acc (I8051.dph, l)) in
240        let l = generate (LTL.St_to_acc (I8051.st0, l)) in
241        let l = generate (LTL.St_from_acc (I8051.dpl, l)) in
242        let l = read addr1 (fun hdw -> LTL.St_to_acc (hdw, l)) in
243        let l = generate (LTL.St_from_acc (I8051.st0, l)) in
244        let l = read addr2 (fun hdw -> LTL.St_to_acc (hdw, l)) in
245        let l = generate (LTL.St_from_acc (I8051.st1, l)) in
246        let l = read srcr (fun hdw -> LTL.St_to_acc (hdw, l)) in
247        LTL.St_skip l
248
249      | ERTL.St_call_id (f, _, l) ->
250        LTL.St_call_id (f, l)
251
252      | ERTL.St_cond (srcr, lbl_true, lbl_false) ->
253        let l = generate (LTL.St_condacc (lbl_true, lbl_false)) in
254        let l = read srcr (fun hdw -> LTL.St_to_acc (hdw, l)) in
255        LTL.St_skip l
256
257      | ERTL.St_return _ ->
258        LTL.St_return
Note: See TracBrowser for help on using the repository browser.