source: driver/extracted/rTLToERTL.ml @ 3106

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

New major extraction that should have solved all remaining issues.
As tests/PROBLEMI shows, we still have some bugs with:

a) initialization of global data (regression)
b) function pointers call

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