source: extracted/rTLToERTL.ml @ 2882

Last change on this file since 2882 was 2882, checked in by sacerdot, 7 years ago

...

File size: 17.7 KB
Line 
1open Preamble
2
3open Order
4
5open Proper
6
7open PositiveMap
8
9open Deqsets
10
11open ErrorMessages
12
13open PreIdentifiers
14
15open Errors
16
17open Extralib
18
19open Lists
20
21open Positive
22
23open Identifiers
24
25open Registers
26
27open Exp
28
29open Setoids
30
31open Monad
32
33open Option
34
35open Extranat
36
37open Vector
38
39open Div_and_mod
40
41open Russell
42
43open Types
44
45open List
46
47open Util
48
49open FoldStuff
50
51open BitVector
52
53open Arithmetic
54
55open Jmeq
56
57open Bool
58
59open Hints_declaration
60
61open Core_notation
62
63open Pts
64
65open Logic
66
67open Relations
68
69open Nat
70
71open I8051
72
73open RegisterSet
74
75open String
76
77open Sets
78
79open Listb
80
81open LabelledObjects
82
83open BitVectorTrie
84
85open Graphs
86
87open CostLabel
88
89open Hide
90
91open Integers
92
93open AST
94
95open Division
96
97open Z
98
99open BitVectorZ
100
101open Pointers
102
103open ByteValues
104
105open BackEndOps
106
107open Joint
108
109open RTL
110
111open ERTL
112
113open Deqsets_extra
114
115open State
116
117open Bind_new
118
119open BindLists
120
121open Blocks
122
123open TranslateUtils
124
125(** val save_hdws :
126    AST.ident List.list -> (Registers.register, I8051.register) Types.prod
127    List.list -> Joint.joint_seq List.list **)
128let save_hdws globals =
129  let save_hdws_internal = fun destr_srcr -> Joint.MOVE
130    (Obj.magic { Types.fst = (ERTL.PSD destr_srcr.Types.fst); Types.snd =
131      (ERTL.move_src_from_dst (ERTL.HDW destr_srcr.Types.snd)) })
132  in
133  List.map save_hdws_internal
134
135(** val restore_hdws :
136    AST.ident List.list -> (Joint.psd_argument, I8051.register) Types.prod
137    List.list -> Joint.joint_seq List.list **)
138let restore_hdws globals =
139  let restore_hdws_internal = fun destr_srcr -> Joint.MOVE
140    (Obj.magic { Types.fst = (ERTL.HDW destr_srcr.Types.snd); Types.snd =
141      (ERTL.psd_argument_move_src destr_srcr.Types.fst) })
142  in
143  List.map restore_hdws_internal
144
145(** val get_params_hdw :
146    AST.ident List.list -> Registers.register List.list -> Joint.joint_seq
147    List.list **)
148let get_params_hdw globals params =
149  save_hdws globals (Util.zip_pottier params I8051.registerParams)
150
151(** val get_param_stack :
152    AST.ident List.list -> Registers.register -> Registers.register ->
153    Registers.register -> Joint.joint_seq List.list **)
154let get_param_stack globals addr1 addr2 destr =
155  List.Cons ((Joint.LOAD ((Obj.magic destr),
156    (Obj.magic (Joint.psd_argument_from_reg addr1)),
157    (Obj.magic (Joint.psd_argument_from_reg addr2)))), (List.Cons ((Joint.OP2
158    (BackEndOps.Add, (Obj.magic addr1),
159    (Obj.magic (Joint.psd_argument_from_reg addr1)),
160    (let x = I8051.int_size in Obj.magic (Joint.psd_argument_from_byte x)))),
161    (List.Cons ((Joint.OP2 (BackEndOps.Addc, (Obj.magic addr2),
162    (Obj.magic (Joint.psd_argument_from_reg addr2)),
163    (Obj.magic (Joint.psd_argument_from_byte Joint.zero_byte)))),
164    List.Nil)))))
165
166(** val get_params_stack :
167    AST.ident List.list -> Registers.register -> Registers.register ->
168    Registers.register -> Registers.register List.list -> Joint.joint_seq
169    List.list **)
170let get_params_stack globals tmpr addr1 addr2 params =
171  let params_length_byte =
172    Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
173      (Nat.S (Nat.S Nat.O)))))))) (List.length params)
174  in
175  List.append (List.Cons
176    ((let x =
177        ERTL.ertl_seq_joint globals (Obj.magic (ERTL.Ertl_frame_size tmpr))
178      in
179     x), (List.Cons (Joint.CLEAR_CARRY, (List.Cons ((Joint.OP2
180    (BackEndOps.Sub, (Obj.magic tmpr),
181    (Obj.magic (Joint.psd_argument_from_reg tmpr)),
182    (Obj.magic (Joint.psd_argument_from_byte params_length_byte)))),
183    (List.Cons ((Joint.MOVE
184    (Obj.magic { Types.fst = (ERTL.PSD addr1); Types.snd =
185      (ERTL.move_src_from_dst (ERTL.HDW I8051.registerSPL)) })), (List.Cons
186    ((Joint.MOVE
187    (Obj.magic { Types.fst = (ERTL.PSD addr2); Types.snd =
188      (ERTL.move_src_from_dst (ERTL.HDW I8051.registerSPH)) })), (List.Cons
189    ((Joint.OP2 (BackEndOps.Add, (Obj.magic addr1),
190    (Obj.magic (Joint.psd_argument_from_reg addr1)),
191    (Obj.magic (Joint.psd_argument_from_reg tmpr)))), (List.Cons ((Joint.OP2
192    (BackEndOps.Addc, (Obj.magic addr2),
193    (Obj.magic (Joint.psd_argument_from_reg addr2)),
194    (Obj.magic (Joint.psd_argument_from_byte Joint.zero_byte)))),
195    List.Nil))))))))))))))
196    (List.flatten (List.map (get_param_stack globals addr1 addr2) params))
197
198(** val get_params :
199    AST.ident List.list -> Registers.register -> Registers.register ->
200    Registers.register -> Registers.register List.list -> Joint.joint_seq
201    List.list **)
202let get_params globals tmpr addr1 addr2 params =
203  let n = Nat.min (List.length params) (List.length I8051.registerParams) in
204  let { Types.fst = hdw_params; Types.snd = stack_params } =
205    Util.list_split n params
206  in
207  List.append (get_params_hdw globals hdw_params)
208    (get_params_stack globals tmpr addr1 addr2 stack_params)
209
210(** val save_return :
211    AST.ident List.list -> Joint.psd_argument List.list -> Joint.joint_seq
212    List.list **)
213let save_return globals ret_regs =
214  let crl = Util.reduce_strong I8051.registerSTS ret_regs in
215  let commonl = crl.Types.fst.Types.fst in
216  let commonr = crl.Types.snd.Types.fst in
217  let restl = crl.Types.fst.Types.snd in
218  List.append
219    (Util.map2 (fun st r -> Joint.MOVE
220      (Obj.magic { Types.fst = (ERTL.HDW st); Types.snd =
221        (ERTL.psd_argument_move_src r) })) commonl commonr)
222    (List.map (fun st -> Joint.MOVE
223      (Obj.magic { Types.fst = (ERTL.HDW st); Types.snd =
224        (ERTL.byte_to_ertl_snd_argument__o__psd_argument_to_move_src
225          Joint.zero_byte) })) restl)
226
227(** val assign_result : AST.ident List.list -> Joint.joint_seq List.list **)
228let assign_result globals =
229  let crl = Util.reduce_strong I8051.registerRets I8051.registerSTS in
230  let commonl = crl.Types.fst.Types.fst in
231  let commonr = crl.Types.snd.Types.fst in
232  Util.map2 (fun ret st -> Joint.MOVE
233    (Obj.magic { Types.fst = (ERTL.HDW ret); Types.snd =
234      (ERTL.move_src_from_dst (ERTL.HDW st)) })) commonl commonr
235
236(** val epilogue :
237    AST.ident List.list -> Registers.register List.list -> Registers.register
238    -> Registers.register -> (Registers.register, I8051.register) Types.prod
239    List.list -> Joint.joint_seq List.list Types.sig0 **)
240let epilogue globals ret_regs sral srah sregs =
241  List.append
242    (save_return globals (List.map (fun x -> Joint.Reg x) ret_regs))
243    (List.append
244      (restore_hdws globals
245        (List.map (fun pr -> { Types.fst = (Joint.Reg pr.Types.fst);
246          Types.snd = pr.Types.snd }) sregs))
247      (List.append (List.Cons ((Joint.PUSH
248        (Obj.magic (Joint.psd_argument_from_reg sral))), (List.Cons
249        ((Joint.PUSH (Obj.magic (Joint.psd_argument_from_reg srah))),
250        (List.Cons
251        ((ERTL.ertl_seq_joint globals (Obj.magic ERTL.Ertl_del_frame)),
252        List.Nil)))))) (assign_result globals)))
253
254(** val prologue :
255    AST.ident List.list -> Registers.register List.list -> Registers.register
256    -> Registers.register -> Registers.register -> Registers.register ->
257    Registers.register -> (Registers.register, I8051.register) Types.prod
258    List.list -> (Registers.register, Joint.joint_seq List.list)
259    Bind_new.bind_new **)
260let prologue globals params sral srah tmpr addr1 addr2 sregs =
261  let l =
262    List.append (List.Cons
263      ((let x = ERTL.ertl_seq_joint globals (Obj.magic ERTL.Ertl_new_frame)
264        in
265       x), (List.Cons ((Joint.POP (Obj.magic srah)), (List.Cons ((Joint.POP
266      (Obj.magic sral)), List.Nil))))))
267      (List.append (save_hdws globals sregs)
268        (get_params globals tmpr addr1 addr2 params))
269  in
270  Bind_new.Bret l
271
272(** val set_params_hdw :
273    AST.ident List.list -> Joint.psd_argument List.list -> Joint.joint_seq
274    List.list **)
275let set_params_hdw globals params =
276  restore_hdws globals (Util.zip_pottier params I8051.registerParams)
277
278(** val set_param_stack :
279    AST.ident List.list -> Registers.register -> Registers.register ->
280    Joint.psd_argument -> Joint.joint_seq List.list **)
281let set_param_stack globals addr1 addr2 arg =
282  List.Cons ((Joint.STORE ((Obj.magic (Joint.psd_argument_from_reg addr1)),
283    (Obj.magic (Joint.psd_argument_from_reg addr2)), (Obj.magic arg))),
284    (List.Cons ((Joint.OP2 (BackEndOps.Add, (Obj.magic addr1),
285    (Obj.magic (Joint.psd_argument_from_reg addr1)),
286    (let x = I8051.int_size in Obj.magic (Joint.psd_argument_from_byte x)))),
287    (List.Cons ((Joint.OP2 (BackEndOps.Addc, (Obj.magic addr2),
288    (Obj.magic (Joint.psd_argument_from_reg addr2)),
289    (Obj.magic (Joint.psd_argument_from_byte Joint.zero_byte)))),
290    List.Nil)))))
291
292(** val set_params_stack :
293    AST.ident List.list -> Joint.psd_argument List.list ->
294    (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new **)
295let set_params_stack globals params =
296  Bind_new.Bnew (fun addr1 -> Bind_new.Bnew (fun addr2 ->
297    let params_length_byte =
298      Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
299        (Nat.S (Nat.S Nat.O)))))))) (List.length params)
300    in
301    let l =
302      List.append (List.Cons ((Joint.MOVE
303        (Obj.magic { Types.fst = (ERTL.PSD addr1); Types.snd =
304          (ERTL.move_src_from_dst (ERTL.HDW I8051.registerSPL)) })),
305        (List.Cons ((Joint.MOVE
306        (Obj.magic { Types.fst = (ERTL.PSD addr2); Types.snd =
307          (ERTL.move_src_from_dst (ERTL.HDW I8051.registerSPH)) })),
308        (List.Cons (Joint.CLEAR_CARRY, (List.Cons ((Joint.OP2
309        (BackEndOps.Sub, (Obj.magic addr1),
310        (Obj.magic (Joint.psd_argument_from_reg addr1)),
311        (Obj.magic (Joint.psd_argument_from_byte params_length_byte)))),
312        (List.Cons ((Joint.OP2 (BackEndOps.Sub, (Obj.magic addr2),
313        (Obj.magic (Joint.psd_argument_from_reg addr2)),
314        (Obj.magic (Joint.psd_argument_from_byte Joint.zero_byte)))),
315        List.Nil))))))))))
316        (List.flatten
317          (List.map (set_param_stack globals addr1 addr2) params))
318    in
319    Bind_new.Bret l))
320
321(** val set_params :
322    AST.ident List.list -> Joint.psd_argument List.list ->
323    (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new
324    Types.sig0 **)
325let set_params globals params =
326  let n = Nat.min (List.length params) (List.length I8051.registerParams) in
327  let hdw_stack_params = List.split params n in
328  let hdw_params = hdw_stack_params.Types.fst in
329  let stack_params = hdw_stack_params.Types.snd in
330  BindLists.bappend
331    (let l = set_params_hdw globals hdw_params in Bind_new.Bret l)
332    (set_params_stack globals stack_params)
333
334(** val fetch_result :
335    AST.ident List.list -> Registers.register List.list -> Joint.joint_seq
336    List.list Types.sig0 **)
337let fetch_result globals ret_regs =
338  (let crl = Util.reduce_strong I8051.registerSTS I8051.registerRets in
339    (fun _ ->
340    let commonl = crl.Types.fst.Types.fst in
341    let commonr = crl.Types.snd.Types.fst in
342    List.append
343      (Util.map2 (fun st r -> Joint.MOVE
344        (Obj.magic { Types.fst = (ERTL.HDW st); Types.snd =
345          (ERTL.move_src_from_dst (ERTL.HDW r)) })) commonl commonr)
346      (let crl0 = Util.reduce_strong ret_regs I8051.registerSTS in
347      let commonl0 = crl0.Types.fst.Types.fst in
348      let commonr0 = crl0.Types.snd.Types.fst in
349      Util.map2 (fun ret st -> Joint.MOVE
350        (Obj.magic { Types.fst = (ERTL.PSD ret); Types.snd =
351          (ERTL.move_src_from_dst (ERTL.HDW st)) })) commonl0 commonr0))) __
352
353(** val translate_step :
354    AST.ident List.list -> Graphs.label -> Joint.joint_step ->
355    Blocks.bind_step_block **)
356let translate_step globals x = function
357| Joint.COST_LABEL lbl ->
358  Bind_new.Bret { Types.fst = { Types.fst = List.Nil; Types.snd = (fun x0 ->
359    Joint.COST_LABEL lbl) }; Types.snd = List.Nil }
360| Joint.CALL (f, args, ret_regs) ->
361  Obj.magic
362    (Monad.m_bind0 (Monad.max_def Bind_new.bindNew)
363      (Types.pi1 (Obj.magic (set_params globals (Obj.magic args))))
364      (fun pref ->
365      Obj.magic (Bind_new.Bret { Types.fst = { Types.fst =
366        (Blocks.add_dummy_variance pref); Types.snd = (fun x0 -> Joint.CALL
367        (f, (Obj.magic (List.length (Obj.magic args))),
368        (Obj.magic Types.It))) }; Types.snd =
369        (Types.pi1 (fetch_result globals (Obj.magic ret_regs))) })))
370| Joint.COND (r, ltrue) ->
371  Bind_new.Bret { Types.fst = { Types.fst = List.Nil; Types.snd = (fun x0 ->
372    Joint.COND (r, ltrue)) }; Types.snd = List.Nil }
373| Joint.Step_seq s0 ->
374  Bind_new.Bret
375    (match s0 with
376     | Joint.COMMENT msg ->
377       Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
378         globals (List.Cons ((Joint.COMMENT msg), List.Nil))
379     | Joint.MOVE rs ->
380       Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
381         globals (List.Cons ((Joint.MOVE
382         (Obj.magic { Types.fst = (ERTL.PSD (Obj.magic rs).Types.fst);
383           Types.snd =
384           (ERTL.psd_argument_move_src (Obj.magic rs).Types.snd) })),
385         List.Nil))
386     | Joint.POP x0 ->
387       Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
388         globals List.Nil
389     | Joint.PUSH x0 ->
390       Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
391         globals List.Nil
392     | Joint.ADDRESS (x0, r1, r2) ->
393       Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
394         globals (List.Cons ((Joint.ADDRESS (x0, r1, r2)), List.Nil))
395     | Joint.OPACCS (op, destr1, destr2, srcr1, srcr2) ->
396       Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
397         globals (List.Cons ((Joint.OPACCS (op, destr1, destr2, srcr1,
398         srcr2)), List.Nil))
399     | Joint.OP1 (op1, destr, srcr) ->
400       Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
401         globals (List.Cons ((Joint.OP1 (op1, destr, srcr)), List.Nil))
402     | Joint.OP2 (op2, destr, srcr1, srcr2) ->
403       Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
404         globals (List.Cons ((Joint.OP2 (op2, destr, srcr1, srcr2)),
405         List.Nil))
406     | Joint.CLEAR_CARRY ->
407       Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
408         globals (List.Cons (Joint.CLEAR_CARRY, List.Nil))
409     | Joint.SET_CARRY ->
410       Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
411         globals (List.Cons (Joint.SET_CARRY, List.Nil))
412     | Joint.LOAD (destr, addr1, addr2) ->
413       Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
414         globals (List.Cons ((Joint.LOAD (destr, addr1, addr2)), List.Nil))
415     | Joint.STORE (addr1, addr2, srcr) ->
416       Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
417         globals (List.Cons ((Joint.STORE (addr1, addr2, srcr)), List.Nil))
418     | Joint.Extension_seq ext ->
419       let RTL.Rtl_stack_address (addr1, addr2) = Obj.magic ext in
420       Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
421         globals (List.Cons ((Joint.MOVE
422         (Obj.magic { Types.fst = (ERTL.PSD addr1); Types.snd =
423           (ERTL.move_src_from_dst (ERTL.HDW I8051.registerSPL)) })),
424         (List.Cons ((Joint.MOVE
425         (Obj.magic { Types.fst = (ERTL.PSD addr2); Types.snd =
426           (ERTL.move_src_from_dst (ERTL.HDW I8051.registerSPH)) })),
427         List.Nil)))))
428
429(** val translate_fin_step :
430    AST.ident List.list -> Registers.register List.list -> Registers.register
431    -> Registers.register -> (Registers.register, I8051.register) Types.prod
432    List.list -> Graphs.label -> Joint.joint_fin_step ->
433    Blocks.bind_fin_block **)
434let translate_fin_step globals ret_regs ral rah to_restore x = function
435| Joint.GOTO lbl' ->
436  Bind_new.Bret { Types.fst = List.Nil; Types.snd = (Joint.GOTO lbl') }
437| Joint.RETURN ->
438  Bind_new.Bret { Types.fst =
439    (Types.pi1 (epilogue globals ret_regs ral rah to_restore)); Types.snd =
440    Joint.RETURN }
441| Joint.TAILCALL (x0, x1) -> assert false (* absurd case *)
442
443(** val allocate_regs :
444    ((Registers.register, I8051.register) Types.prod List.list ->
445    (Registers.register, 'a1) Bind_new.bind_new) -> (Registers.register, 'a1)
446    Bind_new.bind_new **)
447let allocate_regs f =
448  let allocate_regs_internal = fun acc r ->
449    Monad.m_bind0 (Monad.max_def Bind_new.bindNew) acc (fun tl ->
450      Obj.magic (Bind_new.Bnew (fun r' ->
451        Obj.magic
452          (Monad.m_return0 (Monad.max_def Bind_new.bindNew) (List.Cons
453            ({ Types.fst = r'; Types.snd = r }, tl))))))
454  in
455  Obj.magic
456    (Monad.m_bind0 (Monad.max_def Bind_new.bindNew)
457      (Util.foldl allocate_regs_internal
458        (Monad.m_return0 (Monad.max_def Bind_new.bindNew) List.Nil)
459        I8051.registerCalleeSaved) (fun to_save -> Obj.magic f to_save))
460
461(** val translate_data :
462    AST.ident List.list -> Joint.joint_closed_internal_function ->
463    TranslateUtils.bound_b_graph_translate_data **)
464let translate_data globals def =
465  let params = (Types.pi1 def).Joint.joint_if_params in
466  let new_stacksize =
467    Nat.plus (Types.pi1 def).Joint.joint_if_stacksize
468      (Nat.minus (List.length (Obj.magic params))
469        (List.length I8051.registerParams))
470  in
471  allocate_regs (fun to_save -> Bind_new.Bnew (fun ral -> Bind_new.Bnew
472    (fun rah -> Bind_new.Bnew (fun tmpr -> Bind_new.Bnew (fun addr1 ->
473    Bind_new.Bnew (fun addr2 ->
474    Obj.magic
475      (Monad.m_bind0 (Monad.max_def Bind_new.bindNew)
476        (Obj.magic
477          (prologue globals (Obj.magic params) ral rah tmpr addr1 addr2
478            to_save)) (fun prologue0 ->
479        Monad.m_return0 (Monad.max_def Bind_new.bindNew)
480          { TranslateUtils.init_ret = (Obj.magic Types.It);
481          TranslateUtils.init_params =
482          (Obj.magic (List.length (Obj.magic params)));
483          TranslateUtils.init_stack_size = new_stacksize;
484          TranslateUtils.added_prologue = prologue0;
485          TranslateUtils.new_regs =
486          (List.reverse (List.Cons (addr2, (List.Cons (addr1, (List.Cons
487            (tmpr, (List.Cons (rah, (List.Cons (ral,
488            (List.map (fun x -> x.Types.fst) to_save))))))))))));
489          TranslateUtils.f_step = (translate_step globals);
490          TranslateUtils.f_fin =
491          (translate_fin_step globals
492            (Obj.magic (Types.pi1 def).Joint.joint_if_result) ral rah
493            to_save) }))))))))
494
495(** val rtl_to_ertl : RTL.rtl_program -> ERTL.ertl_program **)
496let rtl_to_ertl =
497  TranslateUtils.b_graph_transform_program RTL.rTL ERTL.eRTL translate_data
498
Note: See TracBrowser for help on using the repository browser.