source: src/ERTL/ERTLToLTL.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: 17.4 KB
Line 
1include "ERTL/ERTL.ma".
2include "ERTL/ERTLToLTLI.ma".
3include "LTL/LTL.ma".
4include "ERTL/spill.ma".
5
6include "ERTL/ERTL.ma".
7include "LTL/LTL.ma".
8include "ASM/Arithmetic.ma".
9
10(* XXX: change from O'Caml: former contents of ERTLToLTLI.ma *)
11
12inductive decision: Type[0] ≝
13  | decision_spill: Byte → decision
14  | decision_colour: Register → decision.
15 
16axiom lookup: register → decision.
17axiom generate: ∀globals: list ident. ltl_statement globals → label.
18axiom fresh_label: ∀globals: list ident. ltl_function_definition globals → ltl_function_definition globals × label.
19axiom add_graph: ∀globals. label → ltl_statement globals → ltl_statement_graph globals → ltl_statement_graph globals.
20axiom num_locals: nat.
21
22definition num_locals ≝
23  λint_fun.
24    colour_locals + (ertl_if_stacksize int_fun).
25
26definition stacksize ≝
27  λint_fun.
28    colour_locals + (ertl_if_stacksize int_fun).
29
30definition adjust_off ≝
31  λoff.
32  let 〈ignore, int_off〉 ≝ half_add ? int_size off in
33  let 〈sub, ignore〉 ≝ sub_8_with_carry (bitvector_of_nat ? num_locals) int_off false in
34    sub.
35
36definition get_stack ≝
37  λglobals.
38  λr.
39  λoff.
40  λl.
41    let off ≝ adjust_off off in
42    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals r) l) in
43    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_load globals) l) in
44    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in
45    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Addc RegisterSPH) l) in
46    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_int globals RegisterA (zero ?)) l) in
47    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in
48    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Add RegisterSPL) l) in
49      joint_st_sequential ? globals (joint_instr_int globals RegisterA off) l.
50
51definition set_stack ≝
52  λglobals.
53  λoff.
54  λr.
55  λl.
56  let off ≝ adjust_off off in
57  let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_store globals) l) in
58  let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals r) l) in
59  let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in
60  let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Addc RegisterSPH) l) in
61  let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_int globals RegisterA (zero ?)) l) in
62  let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in
63  let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Add RegisterSPL) l) in
64    joint_st_sequential ? globals (joint_instr_int globals RegisterA off) l.
65
66definition write ≝
67  λglobals.
68  λr: register.
69  λl: label.
70  match lookup r with
71  [ decision_spill off ⇒ 〈RegisterSST, generate globals (set_stack globals off RegisterSST l)〉
72  | decision_colour hwr ⇒ 〈hwr, l〉
73  ].
74
75definition read ≝
76  λglobals.
77  λr: register.
78  λstmt: Register → ltl_statement globals.
79  match lookup r with
80  [ decision_colour hwr ⇒ generate globals (stmt hwr)
81  | decision_spill off ⇒
82    let temphwr ≝ RegisterSST in
83    let l ≝ generate globals (stmt temphwr) in
84      generate globals (get_stack globals temphwr off l)
85  ].
86
87definition move ≝
88  λglobals: list ident.
89  λdest: decision.
90  λsrc: decision.
91  λl: label.
92  match dest with
93  [ decision_colour dest_hwr ⇒
94    match src with
95    [ decision_colour src_hwr ⇒
96      if eq_Register dest_hwr src_hwr then
97        joint_st_goto ? globals l
98      else
99        let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals dest_hwr) l) in
100          joint_st_sequential ? globals (joint_instr_to_acc globals src_hwr) l
101    | decision_spill src_off ⇒ get_stack globals dest_hwr src_off l
102    ]
103  | decision_spill dest_off ⇒
104    match src with
105    [ decision_colour src_hwr ⇒ set_stack globals dest_off src_hwr l
106    | decision_spill src_off ⇒
107      if eq_bv ? dest_off src_off then
108        joint_st_goto ? globals l
109      else
110        let temp_hwr ≝ RegisterSST in
111        let l ≝ generate globals (set_stack globals dest_off temp_hwr l) in
112          get_stack globals temp_hwr src_off l
113    ]
114  ].
115
116definition newframe ≝
117  λglobals.
118  λl.
119  if eq_nat stacksize 0 then
120    joint_st_goto ? globals l
121  else
122    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPH) l) in
123    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Sub RegisterDPH) l) in
124    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_int globals RegisterDPH (zero ?)) l) in
125    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterSPH) l) in
126    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPL) l) in
127    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Sub RegisterDPL) l) in
128    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_clear_carry globals) l) in
129    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_int globals RegisterDPL (bitvector_of_nat ? stacksize)) l) in
130      joint_st_sequential ? globals (joint_instr_to_acc globals RegisterSPL) l.
131
132definition delframe ≝
133  λglobals.
134  λl.
135  if eq_nat stacksize 0 then
136    joint_st_goto ? globals l
137  else
138    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPH) l) in
139    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Addc RegisterSPH) l) in
140    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_int globals RegisterA (zero ?)) l) in
141    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPL) l) in
142    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Add RegisterSPL) l) in
143      joint_st_sequential ? globals (joint_instr_int globals RegisterA (bitvector_of_nat ? stacksize)) l.
144
145definition translate_statement ≝
146  λglobals: list ident.
147  λstmt: ertl_statement.
148  match stmt with
149  [ ertl_st_skip l ⇒ joint_st_goto ? globals l
150  | ertl_st_comment s l ⇒ joint_st_sequential ? globals (joint_instr_comment globals s) l
151  | ertl_st_cost cost_lbl l ⇒ joint_st_sequential ? globals (joint_instr_cost_label globals cost_lbl) l
152  | ertl_st_get_hdw destr sourcehwr l ⇒ move globals (lookup destr) (decision_colour sourcehwr) l
153  | ertl_st_set_hdw desthwr srcr l ⇒ move globals (decision_colour desthwr) (lookup srcr) l
154  | ertl_st_hdw_to_hdw r1 r2 l ⇒
155    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals r1) l) in
156      joint_st_sequential ? globals (joint_instr_to_acc globals r2) l
157  | ertl_st_new_frame l ⇒ newframe globals l
158  | ertl_st_del_frame l ⇒ delframe globals l
159  | ertl_st_frame_size r l ⇒
160    let 〈hdw, l〉 ≝ write globals r l in
161      joint_st_sequential ? globals (joint_instr_int globals hdw (bitvector_of_nat ? stacksize)) l
162  | ertl_st_pop r l ⇒
163    let 〈hdw, l〉 ≝ write globals r l in
164    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
165      joint_st_sequential ? globals (joint_instr_pop globals) l
166  | ertl_st_push r l ⇒
167    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_push globals) l) in
168    let l ≝ read globals r (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
169      joint_st_goto ? globals l
170  | ertl_st_addr rl rh x l ⇒
171    let 〈hdw1, l〉 ≝ write globals rh l in
172    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw1) l) in
173    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPH) l) in
174    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_address globals x ?) l) in
175    let 〈hdw2, l〉 ≝ write globals rl l in
176    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw2) l) in
177    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPL) l) in
178      joint_st_sequential ? globals (joint_instr_address globals x ?) l
179(*  | ertl_st_addr_h 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 RegisterDPH) l)) in
183      ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_address globals x ?) l)
184  | ertl_st_addr_l r x l ⇒
185    let 〈hdw, l〉 ≝ write globals r l in
186    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l)) in
187    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPL) l)) in
188      ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_address globals x ?) l)
189*)
190  | ertl_st_int r i l ⇒
191    let 〈hdw, l〉 ≝ write globals r l in
192      joint_st_sequential ? globals (joint_instr_int globals hdw i) l
193  | ertl_st_move r1 r2 l ⇒ move globals (lookup r1) (lookup r2) l
194  | ertl_st_opaccs opaccs destr1 destr2 srcr1 srcr2 l ⇒
195    let 〈hdw, l〉 ≝ write globals destr1 l in
196    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
197    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l) in
198    let l ≝ read globals srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
199    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
200    let l ≝ read globals srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
201    let l ≝ generate globals (joint_st_goto ? globals l) in
202    let 〈hdw, l〉 ≝ write globals destr2 l in
203    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
204    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterB) l) in
205    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l) in
206    let l ≝ read globals srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
207    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
208    let l ≝ read globals srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
209      joint_st_goto ? globals l
210(*
211  | ertl_st_opaccs_a opaccs destr srcr1 srcr2 l ⇒
212    let 〈hdw, l〉 ≝ write globals destr l in
213    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
214    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l) in
215    let l ≝ read globals srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
216    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
217    let l ≝ read globals srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
218      joint_st_goto ? globals l
219  | ertl_st_opaccs_b opaccs destr srcr1 srcr2 l ⇒
220    let 〈hdw, l〉 ≝ write globals destr l in
221    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
222    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterB) l) in
223    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l) in
224    let l ≝ read globals srcr1 (λ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 RegisterB) l) in
226    let l ≝ read globals srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
227      joint_st_goto ? globals l
228*)
229  | ertl_st_op1 op1 destr srcr l ⇒
230    let 〈hdw, l〉 ≝ write globals destr l in
231    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
232    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op1 globals op1) l) in
233    let l ≝ read globals srcr (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
234      joint_st_goto ? globals l
235  | ertl_st_op2 op2 destr srcr1 srcr2 l ⇒
236    let 〈hdw, l〉 ≝ write globals destr l in
237    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
238    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals op2 RegisterB) l) in
239    let l ≝ read globals srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
240    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
241    let l ≝ read globals srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
242      joint_st_goto ? globals l
243  | ertl_st_clear_carry l ⇒ joint_st_sequential ? globals (joint_instr_clear_carry globals) l
244  | ertl_st_set_carry l ⇒ joint_st_sequential ? globals (joint_instr_set_carry globals) l
245  | ertl_st_load destr addr1 addr2 l ⇒
246    let 〈hdw, l〉 ≝ write globals destr l in
247    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
248    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_load globals) l) in
249    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in
250    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterST0) l) in
251    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in
252    let l ≝ read globals addr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
253    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterST0) l) in
254    let l ≝ read globals addr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
255      joint_st_goto ? globals l
256  | ertl_st_store addr1 addr2 srcr l ⇒
257    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_store globals) l) in
258    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterST1) l) in
259    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in
260    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterST0) l) in
261    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in
262    let l ≝ read globals addr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
263    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterST0) l) in
264    let l ≝ read globals addr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
265    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterST1) l) 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_call_id f ignore l ⇒ joint_st_sequential ? globals (joint_instr_call_id globals f) l
269  | ertl_st_cond srcr lbl_true lbl_false ⇒
270    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_cond_acc globals lbl_true) lbl_false) in
271    let l ≝ read globals srcr (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
272      joint_st_goto ? globals l
273  | ertl_st_return ⇒ joint_st_return ? globals
274  ].
275  cases daemon (* XXX: todo -- proofs regarding gvars *)
276qed.
277
278(* **** *)
279
280definition translate_internal ≝
281  λglobals: list ident.
282  λf.
283  λint_fun: ertl_internal_function.
284  let lookup ≝ λr.
285    match lookup r with
286    | colour_spill ->
287        ERTLToLTLI.Spill (Interference.Vertex.Map.find (Interference.lookup H.graph r) S.coloring)
288    | colour_colour color ->
289        ERTLToLTLI.Color color
290  in
291  let locals ≝ colour_locals + (ertl_if_stacksize int_fun) in
292  let stacksize ≝ (ertl_if_params int_fun) + locals in
293    mk_ltl_internal_function
294      globals
295      (ertl_if_luniverse int_fun)
296      (ertl_if_runiverse int_fun)
297      stacksize.
298
299  let () =
300    Label.Map.iter (fun label stmt ->
301      let stmt =
302        match Liveness.eliminable (G.liveafter label) stmt with
303        | Some successor ->
304            LTL.St_skip successor
305        | None ->
306            I.translate_statement stmt
307      in
308      graph := Label.Map.add label stmt !graph
309    ) int_fun.ERTL.f_graph
310  in
311
312definition translate_funct ≝
313  λname_def.
314  let 〈name, def〉 ≝ name_def in
315  let def' ≝
316    match def with
317    [ Internal def ⇒ Internal ? (translate_internal name def)
318    | External def ⇒ External ? def
319    ]
320  in
321    〈name, def'〉.
322
323definition translate ≝
324  λp.
325  let functs' ≝ map ? ? translate_funct (ertl_pr_functs p) in
326    mk_ltl_program (ertl_pr_globals p) functs' (ertl_pr_main p).
Note: See TracBrowser for help on using the repository browser.