source: extracted/rTLToERTL.ml @ 2717

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

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

File size: 17.8 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 Setoids
20
21open Monad
22
23open Option
24
25open Lists
26
27open Positive
28
29open Identifiers
30
31open Registers
32
33open Exp
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 Graphs
84
85open BitVectorTrie
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
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 params0 =
149  save_hdws globals (Util.zip_pottier params0 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 List.list ->
168    (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new **)
169let get_params_stack globals params0 =
170  Bind_new.Bnew (fun tmpr -> Bind_new.Bnew (fun addr1 -> Bind_new.Bnew
171    (fun addr2 ->
172    let params_length_byte =
173      Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
174        (Nat.S (Nat.S Nat.O)))))))) (List.length params0)
175    in
176    let l =
177      List.append (List.Cons
178        ((let x =
179            ERTL.ertl_seq_joint globals
180              (Obj.magic (ERTL.Ertl_frame_size tmpr))
181          in
182         x), (List.Cons (Joint.CLEAR_CARRY, (List.Cons ((Joint.OP2
183        (BackEndOps.Sub, (Obj.magic tmpr),
184        (Obj.magic (Joint.psd_argument_from_reg tmpr)),
185        (Obj.magic (Joint.psd_argument_from_byte params_length_byte)))),
186        (List.Cons ((Joint.MOVE
187        (Obj.magic { Types.fst = (ERTL.PSD addr1); Types.snd =
188          (ERTL.move_src_from_dst (ERTL.HDW I8051.registerSPL)) })),
189        (List.Cons ((Joint.MOVE
190        (Obj.magic { Types.fst = (ERTL.PSD addr2); Types.snd =
191          (ERTL.move_src_from_dst (ERTL.HDW I8051.registerSPH)) })),
192        (List.Cons ((Joint.OP2 (BackEndOps.Add, (Obj.magic addr1),
193        (Obj.magic (Joint.psd_argument_from_reg addr1)),
194        (Obj.magic (Joint.psd_argument_from_reg tmpr)))), (List.Cons
195        ((Joint.OP2 (BackEndOps.Addc, (Obj.magic addr2),
196        (Obj.magic (Joint.psd_argument_from_reg addr2)),
197        (Obj.magic (Joint.psd_argument_from_byte Joint.zero_byte)))),
198        List.Nil))))))))))))))
199        (List.flatten
200          (List.map (get_param_stack globals addr1 addr2) params0))
201    in
202    Bind_new.Bret l)))
203
204(** val get_params :
205    AST.ident List.list -> Registers.register List.list ->
206    (Registers.register, Joint.joint_seq) BindLists.bind_list **)
207let get_params globals params0 =
208  let n = Nat.min (List.length params0) (List.length I8051.registerParams) in
209  let { Types.fst = hdw_params; Types.snd = stack_params } =
210    Util.list_split n params0
211  in
212  BindLists.bappend
213    (let l = get_params_hdw globals hdw_params in Bind_new.Bret l)
214    (get_params_stack globals stack_params)
215
216(** val save_return :
217    AST.ident List.list -> Joint.psd_argument List.list -> Joint.joint_seq
218    List.list **)
219let save_return globals ret_regs =
220  let crl = Util.reduce_strong I8051.registerSTS ret_regs in
221  let commonl = crl.Types.fst.Types.fst in
222  let commonr = crl.Types.snd.Types.fst in
223  let restl = crl.Types.fst.Types.snd in
224  List.append
225    (Util.map2 (fun st r -> Joint.MOVE
226      (Obj.magic { Types.fst = (ERTL.HDW st); Types.snd =
227        (ERTL.psd_argument_move_src r) })) commonl commonr)
228    (List.map (fun st -> Joint.MOVE
229      (Obj.magic { Types.fst = (ERTL.HDW st); Types.snd =
230        (ERTL.byte_to_ertl_snd_argument__o__psd_argument_to_move_src
231          Joint.zero_byte) })) restl)
232
233(** val assign_result : AST.ident List.list -> Joint.joint_seq List.list **)
234let assign_result globals =
235  let crl = Util.reduce_strong I8051.registerRets I8051.registerSTS in
236  let commonl = crl.Types.fst.Types.fst in
237  let commonr = crl.Types.snd.Types.fst in
238  Util.map2 (fun ret st -> Joint.MOVE
239    (Obj.magic { Types.fst = (ERTL.HDW ret); Types.snd =
240      (ERTL.move_src_from_dst (ERTL.HDW st)) })) commonl commonr
241
242(** val epilogue :
243    AST.ident List.list -> Registers.register List.list -> Registers.register
244    -> Registers.register -> (Registers.register, I8051.register) Types.prod
245    List.list -> Joint.joint_seq List.list Types.sig0 **)
246let epilogue globals ret_regs sral srah sregs =
247  List.append
248    (save_return globals (List.map (fun x -> Joint.Reg x) ret_regs))
249    (List.append
250      (restore_hdws globals
251        (List.map (fun pr -> { Types.fst = (Joint.Reg pr.Types.fst);
252          Types.snd = pr.Types.snd }) sregs))
253      (List.append (List.Cons ((Joint.PUSH
254        (Obj.magic (Joint.psd_argument_from_reg srah))), (List.Cons
255        ((Joint.PUSH (Obj.magic (Joint.psd_argument_from_reg sral))),
256        (List.Cons
257        ((ERTL.ertl_seq_joint globals (Obj.magic ERTL.Ertl_del_frame)),
258        List.Nil)))))) (assign_result globals)))
259
260(** val prologue :
261    AST.ident List.list -> Registers.register List.list -> Registers.register
262    -> Registers.register -> (Registers.register, I8051.register) Types.prod
263    List.list -> (Registers.register, Joint.joint_seq List.list)
264    Bind_new.bind_new **)
265let prologue globals params0 sral srah sregs =
266  BindLists.bappend
267    (let l = List.Cons
268       ((let x = ERTL.ertl_seq_joint globals (Obj.magic ERTL.Ertl_new_frame)
269         in
270        x), (List.Cons ((Joint.POP (Obj.magic sral)), (List.Cons ((Joint.POP
271       (Obj.magic srah)), List.Nil)))))
272     in
273    Bind_new.Bret l)
274    (BindLists.bappend (let l = save_hdws globals sregs in Bind_new.Bret l)
275      (get_params globals params0))
276
277(** val set_params_hdw :
278    AST.ident List.list -> Joint.psd_argument List.list -> Joint.joint_seq
279    List.list **)
280let set_params_hdw globals params0 =
281  restore_hdws globals (Util.zip_pottier params0 I8051.registerParams)
282
283(** val set_param_stack :
284    AST.ident List.list -> Registers.register -> Registers.register ->
285    Joint.psd_argument -> Joint.joint_seq List.list **)
286let set_param_stack globals addr1 addr2 arg =
287  List.Cons ((Joint.STORE ((Obj.magic (Joint.psd_argument_from_reg addr1)),
288    (Obj.magic (Joint.psd_argument_from_reg addr2)), (Obj.magic arg))),
289    (List.Cons ((Joint.OP2 (BackEndOps.Add, (Obj.magic addr1),
290    (Obj.magic (Joint.psd_argument_from_reg addr1)),
291    (let x = I8051.int_size in Obj.magic (Joint.psd_argument_from_byte x)))),
292    (List.Cons ((Joint.OP2 (BackEndOps.Addc, (Obj.magic addr2),
293    (Obj.magic (Joint.psd_argument_from_reg addr2)),
294    (Obj.magic (Joint.psd_argument_from_byte Joint.zero_byte)))),
295    List.Nil)))))
296
297(** val set_params_stack :
298    AST.ident List.list -> Joint.psd_argument List.list ->
299    (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new **)
300let set_params_stack globals params0 =
301  Bind_new.Bnew (fun addr1 -> Bind_new.Bnew (fun addr2 ->
302    let params_length_byte =
303      Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
304        (Nat.S (Nat.S Nat.O)))))))) (List.length params0)
305    in
306    let l =
307      List.append (List.Cons ((Joint.MOVE
308        (Obj.magic { Types.fst = (ERTL.PSD addr1); Types.snd =
309          (ERTL.move_src_from_dst (ERTL.HDW I8051.registerSPL)) })),
310        (List.Cons ((Joint.MOVE
311        (Obj.magic { Types.fst = (ERTL.PSD addr2); Types.snd =
312          (ERTL.move_src_from_dst (ERTL.HDW I8051.registerSPH)) })),
313        (List.Cons (Joint.CLEAR_CARRY, (List.Cons ((Joint.OP2
314        (BackEndOps.Sub, (Obj.magic addr1),
315        (Obj.magic (Joint.psd_argument_from_reg addr1)),
316        (Obj.magic (Joint.psd_argument_from_byte params_length_byte)))),
317        (List.Cons ((Joint.OP2 (BackEndOps.Sub, (Obj.magic addr2),
318        (Obj.magic (Joint.psd_argument_from_reg addr2)),
319        (Obj.magic (Joint.psd_argument_from_byte Joint.zero_byte)))),
320        List.Nil))))))))))
321        (List.flatten
322          (List.map (set_param_stack globals addr1 addr2) params0))
323    in
324    Bind_new.Bret l))
325
326(** val set_params :
327    AST.ident List.list -> Joint.psd_argument List.list ->
328    (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new
329    Types.sig0 **)
330let set_params globals params0 =
331  let n = Nat.min (List.length params0) (List.length I8051.registerParams) in
332  let hdw_stack_params = List.split params0 n in
333  let hdw_params = hdw_stack_params.Types.fst in
334  let stack_params = hdw_stack_params.Types.snd in
335  BindLists.bappend
336    (let l = set_params_hdw globals hdw_params in Bind_new.Bret l)
337    (set_params_stack globals stack_params)
338
339(** val fetch_result :
340    AST.ident List.list -> Registers.register List.list -> Joint.joint_seq
341    List.list Types.sig0 **)
342let fetch_result globals ret_regs =
343  (let crl = Util.reduce_strong I8051.registerSTS I8051.registerRets in
344    (fun _ ->
345    let commonl = crl.Types.fst.Types.fst in
346    let commonr = crl.Types.snd.Types.fst in
347    List.append
348      (Util.map2 (fun st r -> Joint.MOVE
349        (Obj.magic { Types.fst = (ERTL.HDW st); Types.snd =
350          (ERTL.move_src_from_dst (ERTL.HDW r)) })) commonl commonr)
351      (let crl0 = Util.reduce_strong ret_regs I8051.registerSTS in
352      let commonl0 = crl0.Types.fst.Types.fst in
353      let commonr0 = crl0.Types.snd.Types.fst in
354      Util.map2 (fun ret st -> Joint.MOVE
355        (Obj.magic { Types.fst = (ERTL.PSD ret); Types.snd =
356          (ERTL.move_src_from_dst (ERTL.HDW st)) })) commonl0 commonr0))) __
357
358(** val translate_step :
359    AST.ident List.list -> Graphs.label -> Joint.joint_step ->
360    Blocks.bind_step_block **)
361let translate_step globals x = function
362| Joint.COST_LABEL lbl ->
363  Bind_new.Bret { Types.fst = { Types.fst = List.Nil; Types.snd = (fun x0 ->
364    Joint.COST_LABEL lbl) }; Types.snd = List.Nil }
365| Joint.CALL (f, args, ret_regs) ->
366  Obj.magic
367    (Monad.m_bind0 (Monad.max_def Bind_new.bindNew)
368      (Types.pi1 (Obj.magic (set_params globals (Obj.magic args))))
369      (fun pref ->
370      Obj.magic (Bind_new.Bret { Types.fst = { Types.fst =
371        (Blocks.add_dummy_variance pref); Types.snd = (fun x0 -> Joint.CALL
372        (f, (Obj.magic (List.length (Obj.magic args))),
373        (Obj.magic Types.It))) }; Types.snd =
374        (Types.pi1 (fetch_result globals (Obj.magic ret_regs))) })))
375| Joint.COND (r, ltrue) ->
376  Bind_new.Bret { Types.fst = { Types.fst = List.Nil; Types.snd = (fun x0 ->
377    Joint.COND (r, ltrue)) }; Types.snd = List.Nil }
378| Joint.Step_seq s0 ->
379  (match s0 with
380   | Joint.COMMENT msg0 ->
381     Bind_new.Bret
382       (Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
383         globals (List.Cons ((Joint.COMMENT msg0), List.Nil)))
384   | Joint.MOVE rs ->
385     Bind_new.Bret
386       (Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
387         globals (List.Cons ((Joint.MOVE
388         (Obj.magic { Types.fst = (ERTL.PSD (Obj.magic rs).Types.fst);
389           Types.snd =
390           (ERTL.psd_argument_move_src (Obj.magic rs).Types.snd) })),
391         List.Nil)))
392   | Joint.POP x0 ->
393     Bind_new.Bret
394       (Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
395         globals List.Nil)
396   | Joint.PUSH x0 ->
397     Bind_new.Bret
398       (Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
399         globals List.Nil)
400   | Joint.ADDRESS (x0, r5, r6) ->
401     Bind_new.Bret
402       (Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
403         globals (List.Cons ((Joint.ADDRESS (x0, r5, r6)), List.Nil)))
404   | Joint.OPACCS (op4, destr1, destr2, srcr1, srcr2) ->
405     Bind_new.Bret
406       (Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
407         globals (List.Cons ((Joint.OPACCS (op4, destr1, destr2, srcr1,
408         srcr2)), List.Nil)))
409   | Joint.OP1 (op4, destr, srcr) ->
410     Bind_new.Bret
411       (Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
412         globals (List.Cons ((Joint.OP1 (op4, destr, srcr)), List.Nil)))
413   | Joint.OP2 (op4, destr, srcr1, srcr2) ->
414     Bind_new.Bret
415       (Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
416         globals (List.Cons ((Joint.OP2 (op4, destr, srcr1, srcr2)),
417         List.Nil)))
418   | Joint.CLEAR_CARRY ->
419     Bind_new.Bret
420       (Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
421         globals (List.Cons (Joint.CLEAR_CARRY, List.Nil)))
422   | Joint.SET_CARRY ->
423     Bind_new.Bret
424       (Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
425         globals (List.Cons (Joint.SET_CARRY, List.Nil)))
426   | Joint.LOAD (destr, addr1, addr2) ->
427     Bind_new.Bret
428       (Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
429         globals (List.Cons ((Joint.LOAD (destr, addr1, addr2)), List.Nil)))
430   | Joint.STORE (addr1, addr2, srcr) ->
431     Bind_new.Bret
432       (Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
433         globals (List.Cons ((Joint.STORE (addr1, addr2, srcr)), List.Nil)))
434   | Joint.Extension_seq ext ->
435     let RTL.Rtl_stack_address (addr1, addr2) = Obj.magic ext in
436     Bind_new.Bret
437     (Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
438       globals (List.Cons ((Joint.MOVE
439       (Obj.magic { Types.fst = (ERTL.PSD addr1); Types.snd =
440         (ERTL.move_src_from_dst (ERTL.HDW I8051.registerSPL)) })),
441       (List.Cons ((Joint.MOVE
442       (Obj.magic { Types.fst = (ERTL.PSD addr2); Types.snd =
443         (ERTL.move_src_from_dst (ERTL.HDW I8051.registerSPH)) })),
444       List.Nil))))))
445
446(** val translate_fin_step :
447    AST.ident List.list -> Registers.register List.list -> Registers.register
448    -> Registers.register -> (Registers.register, I8051.register) Types.prod
449    List.list -> Graphs.label -> Joint.joint_fin_step ->
450    Blocks.bind_fin_block **)
451let translate_fin_step globals ret_regs ral rah to_restore x = function
452| Joint.GOTO lbl' ->
453  Bind_new.Bret { Types.fst = List.Nil; Types.snd = (Joint.GOTO lbl') }
454| Joint.RETURN ->
455  Bind_new.Bret { Types.fst =
456    (Types.pi1 (epilogue globals ret_regs ral rah to_restore)); Types.snd =
457    Joint.RETURN }
458| Joint.TAILCALL (x0, x1) -> assert false (* absurd case *)
459
460(** val allocate_regs :
461    (Registers.register -> Registers.register -> (Registers.register,
462    I8051.register) Types.prod List.list -> (Registers.register, 'a1)
463    Bind_new.bind_new) -> (Registers.register, 'a1) Bind_new.bind_new **)
464let allocate_regs f =
465  Bind_new.Bnew (fun ral -> Bind_new.Bnew (fun rah ->
466    let allocate_regs_internal = fun acc r ->
467      Monad.m_bind0 (Monad.max_def Bind_new.bindNew) acc (fun tl ->
468        Obj.magic (Bind_new.Bnew (fun r' ->
469          Obj.magic
470            (Monad.m_return0 (Monad.max_def Bind_new.bindNew) (List.Cons
471              ({ Types.fst = r'; Types.snd = r }, tl))))))
472    in
473    Obj.magic
474      (Monad.m_bind0 (Monad.max_def Bind_new.bindNew)
475        (Util.foldl allocate_regs_internal
476          (Monad.m_return0 (Monad.max_def Bind_new.bindNew) List.Nil)
477          I8051.registerCalleeSaved) (fun to_save ->
478        Obj.magic f ral rah to_save))))
479
480(** val translate_data :
481    AST.ident List.list -> Joint.joint_closed_internal_function ->
482    (Registers.register, TranslateUtils.b_graph_translate_data)
483    Bind_new.bind_new **)
484let translate_data globals def =
485  let params0 = (Types.pi1 def).Joint.joint_if_params in
486  let new_stacksize =
487    Nat.plus (Types.pi1 def).Joint.joint_if_stacksize
488      (Nat.minus (List.length (Obj.magic params0))
489        (List.length I8051.registerParams))
490  in
491  allocate_regs (fun ral rah to_save ->
492    Obj.magic
493      (Monad.m_bind0 (Monad.max_def Bind_new.bindNew)
494        (Obj.magic (prologue globals (Obj.magic params0) ral rah to_save))
495        (fun prologue0 ->
496        Monad.m_return0 (Monad.max_def Bind_new.bindNew)
497          { TranslateUtils.init_ret = (Obj.magic Types.It);
498          TranslateUtils.init_params =
499          (Obj.magic (List.length (Obj.magic params0)));
500          TranslateUtils.init_stack_size = new_stacksize;
501          TranslateUtils.added_prologue = prologue0; TranslateUtils.f_step =
502          (translate_step globals); TranslateUtils.f_fin =
503          (translate_fin_step globals
504            (Obj.magic (Types.pi1 def).Joint.joint_if_result) ral rah
505            to_save) })))
506
507(** val rtl_to_ertl : RTL.rtl_program -> ERTL.ertl_program **)
508let rtl_to_ertl =
509  TranslateUtils.b_graph_transform_program RTL.rTL ERTL.eRTL translate_data
510
Note: See TracBrowser for help on using the repository browser.