source: extracted/rTLabsToRTL.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: 46.4 KB
Line 
1open Preamble
2
3open Graphs
4
5open Order
6
7open Registers
8
9open FrontEndVal
10
11open Hide
12
13open ByteValues
14
15open GenMem
16
17open FrontEndMem
18
19open Division
20
21open Z
22
23open BitVectorZ
24
25open Pointers
26
27open Coqlib
28
29open Values
30
31open FrontEndOps
32
33open BitVectorTrie
34
35open CostLabel
36
37open Proper
38
39open PositiveMap
40
41open Deqsets
42
43open ErrorMessages
44
45open PreIdentifiers
46
47open Errors
48
49open Extralib
50
51open Setoids
52
53open Monad
54
55open Option
56
57open Lists
58
59open Positive
60
61open Identifiers
62
63open Exp
64
65open Arithmetic
66
67open Vector
68
69open Div_and_mod
70
71open Jmeq
72
73open Russell
74
75open List
76
77open Util
78
79open FoldStuff
80
81open BitVector
82
83open Extranat
84
85open Bool
86
87open Relations
88
89open Nat
90
91open Integers
92
93open Types
94
95open AST
96
97open Hints_declaration
98
99open Core_notation
100
101open Pts
102
103open Logic
104
105open RTLabs_syntax
106
107open String
108
109open Sets
110
111open Listb
112
113open LabelledObjects
114
115open I8051
116
117open BackEndOps
118
119open Joint
120
121open RTL
122
123open AssocList
124
125open Deqsets
126
127open State
128
129open Bind_new
130
131open BindLists
132
133open Blocks
134
135open TranslateUtils
136
137(** val size_of_sig_type : AST.typ -> Nat.nat **)
138let size_of_sig_type = function
139| AST.ASTint (isize, sign) ->
140  (match isize with
141   | AST.I8 -> Nat.S Nat.O
142   | AST.I16 -> Nat.S (Nat.S Nat.O)
143   | AST.I32 -> Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))
144| AST.ASTptr -> Nat.S (Nat.S Nat.O)
145
146type register_type =
147| Register_int of Registers.register
148| Register_ptr of Registers.register * Registers.register
149
150(** val register_type_rect_Type4 :
151    (Registers.register -> 'a1) -> (Registers.register -> Registers.register
152    -> 'a1) -> register_type -> 'a1 **)
153let rec register_type_rect_Type4 h_register_int h_register_ptr = function
154| Register_int x_17702 -> h_register_int x_17702
155| Register_ptr (x_17704, x_17703) -> h_register_ptr x_17704 x_17703
156
157(** val register_type_rect_Type5 :
158    (Registers.register -> 'a1) -> (Registers.register -> Registers.register
159    -> 'a1) -> register_type -> 'a1 **)
160let rec register_type_rect_Type5 h_register_int h_register_ptr = function
161| Register_int x_17708 -> h_register_int x_17708
162| Register_ptr (x_17710, x_17709) -> h_register_ptr x_17710 x_17709
163
164(** val register_type_rect_Type3 :
165    (Registers.register -> 'a1) -> (Registers.register -> Registers.register
166    -> 'a1) -> register_type -> 'a1 **)
167let rec register_type_rect_Type3 h_register_int h_register_ptr = function
168| Register_int x_17714 -> h_register_int x_17714
169| Register_ptr (x_17716, x_17715) -> h_register_ptr x_17716 x_17715
170
171(** val register_type_rect_Type2 :
172    (Registers.register -> 'a1) -> (Registers.register -> Registers.register
173    -> 'a1) -> register_type -> 'a1 **)
174let rec register_type_rect_Type2 h_register_int h_register_ptr = function
175| Register_int x_17720 -> h_register_int x_17720
176| Register_ptr (x_17722, x_17721) -> h_register_ptr x_17722 x_17721
177
178(** val register_type_rect_Type1 :
179    (Registers.register -> 'a1) -> (Registers.register -> Registers.register
180    -> 'a1) -> register_type -> 'a1 **)
181let rec register_type_rect_Type1 h_register_int h_register_ptr = function
182| Register_int x_17726 -> h_register_int x_17726
183| Register_ptr (x_17728, x_17727) -> h_register_ptr x_17728 x_17727
184
185(** val register_type_rect_Type0 :
186    (Registers.register -> 'a1) -> (Registers.register -> Registers.register
187    -> 'a1) -> register_type -> 'a1 **)
188let rec register_type_rect_Type0 h_register_int h_register_ptr = function
189| Register_int x_17732 -> h_register_int x_17732
190| Register_ptr (x_17734, x_17733) -> h_register_ptr x_17734 x_17733
191
192(** val register_type_inv_rect_Type4 :
193    register_type -> (Registers.register -> __ -> 'a1) -> (Registers.register
194    -> Registers.register -> __ -> 'a1) -> 'a1 **)
195let register_type_inv_rect_Type4 hterm h1 h2 =
196  let hcut = register_type_rect_Type4 h1 h2 hterm in hcut __
197
198(** val register_type_inv_rect_Type3 :
199    register_type -> (Registers.register -> __ -> 'a1) -> (Registers.register
200    -> Registers.register -> __ -> 'a1) -> 'a1 **)
201let register_type_inv_rect_Type3 hterm h1 h2 =
202  let hcut = register_type_rect_Type3 h1 h2 hterm in hcut __
203
204(** val register_type_inv_rect_Type2 :
205    register_type -> (Registers.register -> __ -> 'a1) -> (Registers.register
206    -> Registers.register -> __ -> 'a1) -> 'a1 **)
207let register_type_inv_rect_Type2 hterm h1 h2 =
208  let hcut = register_type_rect_Type2 h1 h2 hterm in hcut __
209
210(** val register_type_inv_rect_Type1 :
211    register_type -> (Registers.register -> __ -> 'a1) -> (Registers.register
212    -> Registers.register -> __ -> 'a1) -> 'a1 **)
213let register_type_inv_rect_Type1 hterm h1 h2 =
214  let hcut = register_type_rect_Type1 h1 h2 hterm in hcut __
215
216(** val register_type_inv_rect_Type0 :
217    register_type -> (Registers.register -> __ -> 'a1) -> (Registers.register
218    -> Registers.register -> __ -> 'a1) -> 'a1 **)
219let register_type_inv_rect_Type0 hterm h1 h2 =
220  let hcut = register_type_rect_Type0 h1 h2 hterm in hcut __
221
222(** val register_type_discr : register_type -> register_type -> __ **)
223let register_type_discr x y =
224  Logic.eq_rect_Type2 x
225    (match x with
226     | Register_int a0 -> Obj.magic (fun _ dH -> dH __)
227     | Register_ptr (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
228
229(** val register_type_jmdiscr : register_type -> register_type -> __ **)
230let register_type_jmdiscr x y =
231  Logic.eq_rect_Type2 x
232    (match x with
233     | Register_int a0 -> Obj.magic (fun _ dH -> dH __)
234     | Register_ptr (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
235
236type local_env = Registers.register List.list Identifiers.identifier_map
237
238(** val find_local_env :
239    PreIdentifiers.identifier -> local_env -> Registers.register List.list **)
240let find_local_env r lenv =
241  Option.opt_safe (Identifiers.lookup0 PreIdentifiers.RegisterTag lenv r)
242
243(** val find_local_env_arg :
244    Registers.register -> local_env -> Joint.psd_argument List.list **)
245let find_local_env_arg r lenv =
246  List.map (fun x -> Joint.Reg x) (find_local_env r lenv)
247
248(** val m_iter : Monad.monad -> ('a1 -> __) -> Nat.nat -> __ -> __ **)
249let rec m_iter m f n m0 =
250  match n with
251  | Nat.O -> m0
252  | Nat.S k -> Monad.m_bind0 m m0 (fun v -> m_iter m f k (f v))
253
254(** val fresh_registers :
255    Joint.params -> AST.ident List.list -> Nat.nat -> Registers.register
256    List.list Monad.smax_def__o__monad **)
257let fresh_registers p g0 n =
258  let f = fun acc ->
259    Monad.m_bind0 (Monad.smax_def State.state_monad)
260      (TranslateUtils.fresh_register p g0) (fun m ->
261      Monad.m_return0 (Monad.smax_def State.state_monad) (List.Cons (m, acc)))
262  in
263  m_iter (Monad.smax_def State.state_monad) f n
264    (Monad.m_return0 (Monad.smax_def State.state_monad) List.Nil)
265
266(** val map_list_local_env :
267    Registers.register List.list Identifiers.identifier_map ->
268    (Registers.register, AST.typ) Types.prod List.list -> Registers.register
269    List.list **)
270let rec map_list_local_env lenv regs =
271  (match regs with
272   | List.Nil -> (fun _ -> List.Nil)
273   | List.Cons (hd0, tl) ->
274     (fun _ ->
275       List.append (find_local_env hd0.Types.fst lenv)
276         (map_list_local_env lenv tl))) __
277
278(** val initialize_local_env :
279    AST.ident List.list -> (Registers.register, AST.typ) Types.prod List.list
280    -> local_env Monad.smax_def__o__monad **)
281let initialize_local_env globals registers0 =
282  let f = fun r_sig lenv ->
283    let { Types.fst = r; Types.snd = sig1 } = r_sig in
284    let size = size_of_sig_type sig1 in
285    Monad.m_bind0 (Monad.smax_def State.state_monad)
286      (fresh_registers (Joint.graph_params_to_params RTL.rTL) globals size)
287      (fun regs ->
288      Monad.m_return0 (Monad.smax_def State.state_monad)
289        (Identifiers.add PreIdentifiers.RegisterTag lenv r regs))
290  in
291  Monad.m_fold (Monad.smax_def State.state_monad) f registers0
292    (Identifiers.empty_map PreIdentifiers.RegisterTag)
293
294(** val initialize_locals_params_ret :
295    AST.ident List.list -> (Registers.register, AST.typ) Types.prod List.list
296    -> (Registers.register, AST.typ) Types.prod List.list ->
297    (Registers.register, AST.typ) Types.prod Types.option -> local_env
298    Monad.smax_def__o__monad **)
299let initialize_locals_params_ret globals locals params0 ret =
300  Obj.magic (fun def ->
301    (let { Types.fst = def'; Types.snd = lenv } =
302       Obj.magic initialize_local_env globals
303         (List.append
304           (match ret with
305            | Types.None -> List.Nil
306            | Types.Some r_sig -> List.Cons (r_sig, List.Nil))
307           (List.append locals params0)) def
308     in
309    (fun _ ->
310    let params' = map_list_local_env lenv params0 in
311    let ret' =
312      (match ret with
313       | Types.None -> (fun _ -> List.Nil)
314       | Types.Some r_sig -> (fun _ -> find_local_env r_sig.Types.fst lenv))
315        __
316    in
317    let def'' = { Joint.joint_if_luniverse = def'.Joint.joint_if_luniverse;
318      Joint.joint_if_runiverse = def'.Joint.joint_if_runiverse;
319      Joint.joint_if_result = (Obj.magic ret'); Joint.joint_if_params =
320      (Obj.magic params'); Joint.joint_if_stacksize =
321      def'.Joint.joint_if_stacksize; Joint.joint_if_code =
322      def'.Joint.joint_if_code; Joint.joint_if_entry =
323      def'.Joint.joint_if_entry }
324    in
325    { Types.fst = def''; Types.snd = lenv })) __)
326
327(** val make_addr : 'a1 List.list -> ('a1, 'a1) Types.prod **)
328let make_addr lst =
329  { Types.fst = (Util.nth_safe Nat.O lst); Types.snd =
330    (Util.nth_safe (Nat.S Nat.O) lst) }
331
332(** val find_and_addr :
333    PreIdentifiers.identifier -> local_env -> (Registers.register,
334    Registers.register) Types.prod **)
335let find_and_addr r lenv =
336  make_addr (find_local_env r lenv)
337
338(** val find_and_addr_arg :
339    Registers.register -> local_env -> (Joint.psd_argument,
340    Joint.psd_argument) Types.prod **)
341let find_and_addr_arg r lenv =
342  make_addr (find_local_env_arg r lenv)
343
344(** val rtl_args :
345    Registers.register List.list -> local_env -> Joint.psd_argument List.list **)
346let rec rtl_args args env =
347  (match args with
348   | List.Nil -> (fun _ -> List.Nil)
349   | List.Cons (hd0, tl) ->
350     (fun _ -> List.append (find_local_env_arg hd0 env) (rtl_args tl env)))
351    __
352
353(** val vrsplit :
354    Nat.nat -> Nat.nat -> 'a1 Vector.vector -> 'a1 Vector.vector List.list
355    Types.sig0 **)
356let rec vrsplit m n =
357  match m with
358  | Nat.O -> (fun v -> List.Nil)
359  | Nat.S k ->
360    (fun v ->
361      let spl = Vector.vsplit n (Nat.times k n) v in
362      List.Cons (spl.Types.fst, (Types.pi1 (vrsplit k n spl.Types.snd))))
363
364(** val split_into_bytes :
365    AST.intsize -> AST.bvint -> BitVector.byte List.list Types.sig0 **)
366let split_into_bytes size =
367  vrsplit (AST.size_intsize size) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
368    (Nat.S (Nat.S Nat.O))))))))
369
370(** val list_inject_All_aux : 'a1 List.list -> 'a1 Types.sig0 List.list **)
371let rec list_inject_All_aux l =
372  (match l with
373   | List.Nil -> (fun _ -> List.Nil)
374   | List.Cons (hd0, tl) ->
375     (fun _ -> List.Cons (hd0, (list_inject_All_aux tl)))) __
376
377(** val translate_op :
378    AST.ident List.list -> BackEndOps.op2 -> Registers.register List.list ->
379    Joint.psd_argument List.list -> Joint.psd_argument List.list ->
380    (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new **)
381let translate_op globals op4 destrs srcrs1 srcrs2 =
382  let l =
383    List.append
384      (match op4 with
385       | BackEndOps.Add -> List.Nil
386       | BackEndOps.Addc -> List.Cons (Joint.CLEAR_CARRY, List.Nil)
387       | BackEndOps.Sub -> List.Cons (Joint.CLEAR_CARRY, List.Nil)
388       | BackEndOps.And -> List.Nil
389       | BackEndOps.Or -> List.Nil
390       | BackEndOps.Xor -> List.Nil)
391      (Util.map3 (fun x x0 x1 -> Joint.OP2 (op4, x, x0, x1))
392        (Obj.magic destrs) (Obj.magic srcrs1) (Obj.magic srcrs2))
393  in
394  Bind_new.Bret l
395
396(** val cast_list : 'a1 -> Nat.nat -> 'a1 List.list -> 'a1 List.list **)
397let cast_list deflt new_length l =
398  match Nat.leb (List.length l) new_length with
399  | Bool.True ->
400    List.append l
401      (List.make_list deflt (Nat.minus new_length (List.length l)))
402  | Bool.False -> List.lhd l new_length
403
404(** val translate_op_asym_unsigned :
405    AST.ident List.list -> BackEndOps.op2 -> Registers.register List.list ->
406    Joint.psd_argument List.list -> Joint.psd_argument List.list ->
407    (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new **)
408let translate_op_asym_unsigned globals op4 destrs srcrs1 srcrs2 =
409  let l = List.length destrs in
410  let srcrs1' =
411    cast_list (let x = Joint.psd_argument_from_byte Joint.zero_byte in x) l
412      srcrs1
413  in
414  let srcrs2' =
415    cast_list (let x = Joint.psd_argument_from_byte Joint.zero_byte in x) l
416      srcrs2
417  in
418  translate_op globals op4 destrs srcrs1' srcrs2'
419
420(** val nat_to_args :
421    Nat.nat -> Nat.nat -> Joint.psd_argument List.list Types.sig0 **)
422let rec nat_to_args size k =
423  (match size with
424   | Nat.O -> (fun _ -> List.Nil)
425   | Nat.S size' ->
426     (fun _ -> List.Cons
427       ((let x = Joint.psd_argument_from_byte (Joint.byte_of_nat k) in x),
428       (Types.pi1
429         (nat_to_args size'
430           (Util.division k (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
431             (Nat.S Nat.O)))))))))))))) __
432
433(** val size_of_cst : AST.typ -> FrontEndOps.constant -> Nat.nat **)
434let size_of_cst typ0 = function
435| FrontEndOps.Ointconst (size, x, x0) -> AST.size_intsize size
436| FrontEndOps.Oaddrsymbol (x, x0) -> Nat.S (Nat.S Nat.O)
437| FrontEndOps.Oaddrstack x -> Nat.S (Nat.S Nat.O)
438
439(** val translate_cst :
440    AST.typ -> AST.ident List.list -> FrontEndOps.constant Types.sig0 ->
441    Registers.register List.list -> (Registers.register, Joint.joint_seq
442    List.list) Bind_new.bind_new **)
443let translate_cst ty globals cst_sig destrs =
444  let l =
445    (match Types.pi1 cst_sig with
446     | FrontEndOps.Ointconst (size, sign, const) ->
447       (fun _ _ ->
448         Util.map2 (fun r b -> Joint.MOVE
449           (Obj.magic { Types.fst = r; Types.snd =
450             (Joint.psd_argument_from_byte b) })) destrs
451           (Types.pi1 (split_into_bytes size const)))
452     | FrontEndOps.Oaddrsymbol (id, offset0) ->
453       (fun _ _ ->
454         let { Types.fst = r5; Types.snd = r6 } = make_addr destrs in
455         List.Cons ((Joint.ADDRESS (id, (Obj.magic r5), (Obj.magic r6))),
456         List.Nil))
457     | FrontEndOps.Oaddrstack offset0 ->
458       (fun _ _ ->
459         let { Types.fst = r5; Types.snd = r6 } = make_addr destrs in
460         List.Cons
461         ((let x = Joint.Extension_seq
462             (Obj.magic (RTL.Rtl_stack_address (r5, r6)))
463           in
464          x), List.Nil))) __ __
465  in
466  Bind_new.Bret l
467
468(** val translate_move :
469    AST.ident List.list -> Registers.register List.list -> Joint.psd_argument
470    List.list -> Joint.joint_seq List.list **)
471let translate_move globals destrs srcrs =
472  Util.map2 (fun dst src -> Joint.MOVE
473    (Obj.magic { Types.fst = dst; Types.snd = src })) destrs srcrs
474
475(** val sign_mask :
476    AST.ident List.list -> Registers.register -> Joint.psd_argument ->
477    Joint.joint_seq List.list **)
478let sign_mask globals destr = function
479| Joint.Reg srcr ->
480  let byte_127 = Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
481    (Nat.S Nat.O))))))), Bool.False,
482    (BitVector.maximum (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
483      Nat.O)))))))))
484  in
485  List.Cons ((Joint.OP2 (BackEndOps.Or, (Obj.magic destr),
486  (Obj.magic (Joint.psd_argument_from_reg srcr)),
487  (Obj.magic (Joint.psd_argument_from_byte byte_127)))), (List.Cons
488  ((Joint.OP1 (BackEndOps.Rl, (Obj.magic destr), (Obj.magic destr))),
489  (List.Cons ((Joint.OP1 (BackEndOps.Inc, (Obj.magic destr),
490  (Obj.magic destr))), (List.Cons ((Joint.OP1 (BackEndOps.Cmpl,
491  (Obj.magic destr), (Obj.magic destr))), List.Nil)))))))
492| Joint.Imm b ->
493  (match Arithmetic.sign_bit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
494           (Nat.S Nat.O)))))))) b with
495   | Bool.True ->
496     List.Cons ((Joint.MOVE
497       (Obj.magic { Types.fst = destr; Types.snd =
498         (let x =
499            BitVector.maximum (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
500              (Nat.S (Nat.S Nat.O))))))))
501          in
502         Joint.psd_argument_from_byte x) })), List.Nil)
503   | Bool.False ->
504     List.Cons ((Joint.MOVE
505       (Obj.magic { Types.fst = destr; Types.snd =
506         (Joint.psd_argument_from_byte Joint.zero_byte) })), List.Nil))
507
508(** val translate_cast_signed :
509    AST.ident List.list -> Registers.register List.list -> Joint.psd_argument
510    -> (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new **)
511let translate_cast_signed globals destrs srca =
512  Bind_new.Bnew (fun tmp ->
513    let l =
514      List.append (sign_mask globals tmp srca)
515        (translate_move globals destrs
516          (List.make_list (Joint.Reg tmp) (List.length destrs)))
517    in
518    Bind_new.Bret l)
519
520(** val translate_fill_with_zero :
521    AST.ident List.list -> Registers.register List.list -> Joint.joint_seq
522    List.list **)
523let translate_fill_with_zero globals destrs =
524  let res1 = nat_to_args (List.length destrs) Nat.O in
525  translate_move globals destrs res1
526
527(** val last : 'a1 List.list -> 'a1 Types.option **)
528let rec last = function
529| List.Nil -> Types.None
530| List.Cons (hd0, tl) ->
531  (match tl with
532   | List.Nil -> Types.Some hd0
533   | List.Cons (x, x0) -> last tl)
534
535(** val translate_op_asym_signed :
536    AST.ident List.list -> BackEndOps.op2 -> Registers.register List.list ->
537    Joint.psd_argument List.list -> Joint.psd_argument List.list ->
538    (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new **)
539let translate_op_asym_signed globals op4 destrs srcrs1 srcrs2 =
540  Bind_new.Bnew (fun tmp1 -> Bind_new.Bnew (fun tmp2 ->
541    let l = List.length destrs in
542    let cast_srcrs = fun srcrs tmp ->
543      let srcrs_l = List.length srcrs in
544      (match Nat.leb srcrs_l l with
545       | Bool.True ->
546         (match last srcrs with
547          | Types.None ->
548            { Types.fst =
549              (List.make_list
550                (let x = Joint.psd_argument_from_byte Joint.zero_byte in x)
551                l); Types.snd = List.Nil }
552          | Types.Some last0 ->
553            { Types.fst =
554              (List.append srcrs
555                (List.make_list (Joint.Reg tmp) (Nat.minus l srcrs_l)));
556              Types.snd = (sign_mask globals tmp last0) })
557       | Bool.False ->
558         { Types.fst = (List.lhd srcrs l); Types.snd = List.Nil })
559    in
560    let srcrs1init = cast_srcrs srcrs1 tmp1 in
561    let srcrs2init = cast_srcrs srcrs2 tmp2 in
562    BindLists.bappend (let l0 = srcrs1init.Types.snd in Bind_new.Bret l0)
563      (BindLists.bappend (let l0 = srcrs2init.Types.snd in Bind_new.Bret l0)
564        (translate_op globals op4 destrs srcrs1init.Types.fst
565          srcrs2init.Types.fst))))
566
567(** val translate_cast :
568    AST.ident List.list -> AST.signedness -> Registers.register List.list ->
569    Registers.register List.list -> (Registers.register, Joint.joint_seq
570    List.list) Bind_new.bind_new **)
571let translate_cast globals src_sign destrs srcrs =
572  let t = Util.reduce_strong destrs srcrs in
573  let src_common = t.Types.fst.Types.fst in
574  let src_rest = t.Types.fst.Types.snd in
575  let dst_common = t.Types.snd.Types.fst in
576  let dst_rest = t.Types.snd.Types.snd in
577  BindLists.bappend
578    (let l =
579       translate_move globals src_common
580         (List.map (fun x -> Joint.Reg x) dst_common)
581     in
582    Bind_new.Bret l)
583    (match src_rest with
584     | List.Nil ->
585       (match src_sign with
586        | AST.Signed ->
587          (match last srcrs with
588           | Types.None ->
589             let l = translate_fill_with_zero globals dst_rest in
590             Bind_new.Bret l
591           | Types.Some src_last ->
592             translate_cast_signed globals dst_rest
593               (Joint.psd_argument_from_reg src_last))
594        | AST.Unsigned ->
595          let l = translate_fill_with_zero globals dst_rest in
596          Bind_new.Bret l)
597     | List.Cons (x, x0) -> let l = List.Nil in Bind_new.Bret l)
598
599(** val translate_notint :
600    AST.ident List.list -> Registers.register List.list -> Registers.register
601    List.list -> Joint.joint_seq List.list **)
602let translate_notint globals destrs srcrs =
603  Util.map2 (fun x x0 -> Joint.OP1 (BackEndOps.Cmpl, x, x0))
604    (Obj.magic destrs) (Obj.magic srcrs)
605
606(** val translate_negint :
607    AST.ident List.list -> Registers.register List.list -> Registers.register
608    List.list -> (Registers.register, Joint.joint_seq List.list)
609    Bind_new.bind_new **)
610let translate_negint globals destrs srcrs =
611  BindLists.bappend
612    (let l = translate_notint globals destrs srcrs in Bind_new.Bret l)
613    (translate_op globals BackEndOps.Add destrs
614      (List.map (fun x -> Joint.Reg x) destrs)
615      (Types.pi1 (nat_to_args (List.length destrs) (Nat.S Nat.O))))
616
617(** val translate_notbool :
618    AST.ident List.list -> Registers.register List.list -> Registers.register
619    List.list -> (Registers.register, Joint.joint_seq List.list)
620    Bind_new.bind_new **)
621let translate_notbool globals destrs srcrs =
622  match destrs with
623  | List.Nil -> let l = List.Nil in Bind_new.Bret l
624  | List.Cons (destr, destrs') ->
625    BindLists.bappend
626      (let l = translate_fill_with_zero globals destrs' in Bind_new.Bret l)
627      (match srcrs with
628       | List.Nil ->
629         let l = List.Cons ((Joint.MOVE
630           (Obj.magic { Types.fst = destr; Types.snd =
631             (Joint.psd_argument_from_byte Joint.zero_byte) })), List.Nil)
632         in
633         Bind_new.Bret l
634       | List.Cons (srcr, srcrs') ->
635         BindLists.bappend
636           (BindLists.bcons (Joint.MOVE
637             (Obj.magic { Types.fst = destr; Types.snd =
638               (Joint.psd_argument_from_reg srcr) }))
639             (let l =
640                List.map (fun r -> Joint.OP2 (BackEndOps.Or,
641                  (Obj.magic destr),
642                  (Obj.magic (Joint.psd_argument_from_reg destr)),
643                  (Obj.magic (Joint.psd_argument_from_reg r)))) srcrs'
644              in
645             Bind_new.Bret l))
646           (BindLists.bcons Joint.CLEAR_CARRY (Bind_new.Bnew (fun tmp ->
647             let l = List.Cons ((Joint.MOVE
648               (Obj.magic { Types.fst = tmp; Types.snd =
649                 (Joint.psd_argument_from_byte Joint.zero_byte) })),
650               (List.Cons ((Joint.OP2 (BackEndOps.Sub, (Obj.magic destr),
651               (Obj.magic (Joint.psd_argument_from_reg tmp)),
652               (Obj.magic (Joint.psd_argument_from_reg tmp)))), (List.Cons
653               ((Joint.OP2 (BackEndOps.Addc, (Obj.magic destr),
654               (Obj.magic (Joint.psd_argument_from_reg tmp)),
655               (Obj.magic (Joint.psd_argument_from_reg tmp)))), List.Nil)))))
656             in
657             Bind_new.Bret l))))
658
659(** val translate_op1 :
660    AST.ident List.list -> AST.typ -> AST.typ -> FrontEndOps.unary_operation
661    -> Registers.register List.list -> Registers.register List.list ->
662    (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new **)
663let translate_op1 globals ty ty' op4 destrs srcrs =
664  (match op4 with
665   | FrontEndOps.Ocastint (x, src_sign, x0, x1) ->
666     (fun _ _ -> translate_cast globals src_sign destrs srcrs)
667   | FrontEndOps.Onegint (sz, sg) ->
668     (fun _ _ -> translate_negint globals destrs srcrs)
669   | FrontEndOps.Onotbool (x, x0, x1) ->
670     (fun _ _ -> translate_notbool globals destrs srcrs)
671   | FrontEndOps.Onotint (sz, sg) ->
672     (fun _ _ ->
673       let l = translate_notint globals destrs srcrs in Bind_new.Bret l)
674   | FrontEndOps.Oid t ->
675     (fun _ _ ->
676       let l =
677         translate_move globals destrs
678           (List.map (fun x -> Joint.Reg x) srcrs)
679       in
680       Bind_new.Bret l)
681   | FrontEndOps.Optrofint (sz, sg) ->
682     (fun _ _ -> translate_cast globals AST.Unsigned destrs srcrs)
683   | FrontEndOps.Ointofptr (sz, sg) ->
684     (fun _ _ -> translate_cast globals AST.Unsigned destrs srcrs)) __ __
685
686(** val translate_mul_i :
687    AST.ident List.list -> Registers.register -> Registers.register ->
688    Nat.nat -> Registers.register List.list -> Joint.psd_argument List.list
689    -> Joint.psd_argument List.list -> Nat.nat -> Nat.nat Types.sig0 ->
690    (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new ->
691    (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new **)
692let translate_mul_i globals a b n tmp_destrs_dummy srcrs1 srcrs2 k i_sig acc =
693  let i = i_sig in
694  let args =
695    List.append (List.Cons ((Joint.Reg a), (List.Cons ((Joint.Reg b),
696      List.Nil))))
697      (List.make_list
698        (let x = Joint.psd_argument_from_byte Joint.zero_byte in x)
699        (Nat.minus (Nat.minus n (Nat.S Nat.O)) k))
700  in
701  let tmp_destrs_view = List.ltl tmp_destrs_dummy k in
702  BindLists.bappend
703    (let l = List.Cons ((Joint.OPACCS (BackEndOps.Mul, (Obj.magic a),
704       (Obj.magic b), (Util.nth_safe i (Obj.magic srcrs1)),
705       (Util.nth_safe (Nat.minus k i) (Obj.magic srcrs2)))), List.Nil)
706     in
707    Bind_new.Bret l)
708    (BindLists.bappend
709      (translate_op globals BackEndOps.Add tmp_destrs_view
710        (List.map (fun x -> Joint.Reg x) tmp_destrs_view) args) acc)
711
712(** val translate_mul :
713    AST.ident List.list -> Registers.register List.list -> Joint.psd_argument
714    List.list -> Joint.psd_argument List.list -> (Registers.register,
715    Joint.joint_seq List.list) Bind_new.bind_new **)
716let translate_mul globals destrs srcrs1 srcrs2 =
717  Bind_new.Bnew (fun a -> Bind_new.Bnew (fun b ->
718    Bind_new.bnews_strong (List.length destrs) (fun tmp_destrs _ ->
719      Bind_new.Bnew (fun dummy ->
720      let translate_mul_k = fun k_sig acc ->
721        let k = k_sig in
722        List.foldr
723          (translate_mul_i globals a b (List.length destrs)
724            (List.append tmp_destrs (List.Cons (dummy, List.Nil))) srcrs1
725            srcrs2 k) acc (Lists.range_strong (Nat.S k))
726      in
727      BindLists.bappend
728        (let l = translate_fill_with_zero globals tmp_destrs in
729        Bind_new.Bret l)
730        (BindLists.bappend
731          (List.foldr translate_mul_k (let l = List.Nil in Bind_new.Bret l)
732            (Lists.range_strong (List.length destrs)))
733          (let l =
734             translate_move globals destrs
735               (List.map (fun x -> Joint.Reg x) tmp_destrs)
736           in
737          Bind_new.Bret l))))))
738
739(** val translate_divumodu8 :
740    AST.ident List.list -> Bool.bool -> Registers.register List.list ->
741    Joint.psd_argument List.list -> Joint.psd_argument List.list ->
742    (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new **)
743let translate_divumodu8 globals div_not_mod destrs srcrs1 srcrs2 =
744  (match destrs with
745   | List.Nil -> (fun _ -> let l = List.Nil in Bind_new.Bret l)
746   | List.Cons (destr, destrs') ->
747     (fun _ ->
748       match destrs' with
749       | List.Nil ->
750         (match srcrs1 with
751          | List.Nil -> (fun _ -> assert false (* absurd case *))
752          | List.Cons (srcr1, srcrs1') ->
753            (fun _ ->
754              (match srcrs2 with
755               | List.Nil -> (fun _ -> assert false (* absurd case *))
756               | List.Cons (srcr2, srcrs2') ->
757                 (fun _ -> Bind_new.Bnew (fun dummy ->
758                   let l =
759                     let { Types.fst = destr1; Types.snd = destr2 } =
760                       match div_not_mod with
761                       | Bool.True ->
762                         { Types.fst = destr; Types.snd = dummy }
763                       | Bool.False ->
764                         { Types.fst = dummy; Types.snd = destr }
765                     in
766                     List.Cons ((Joint.OPACCS (BackEndOps.DivuModu,
767                     (Obj.magic destr1), (Obj.magic destr2),
768                     (Obj.magic srcr1), (Obj.magic srcr2))), List.Nil)
769                   in
770                   Bind_new.Bret l))) __)) __
771       | List.Cons (x, x0) -> Logic.false_rect_Type0 __)) __
772
773(** val foldr2 :
774    ('a1 -> 'a2 -> 'a3 -> 'a3) -> 'a3 -> 'a1 List.list -> 'a2 List.list ->
775    'a3 **)
776let rec foldr2 f init l1 l2 =
777  (match l1 with
778   | List.Nil -> (fun _ -> init)
779   | List.Cons (a, l1') ->
780     (fun _ ->
781       (match l2 with
782        | List.Nil -> (fun _ -> assert false (* absurd case *))
783        | List.Cons (b, l2') -> (fun _ -> f a b (foldr2 f init l1' l2'))) __))
784    __
785
786(** val translate_ne :
787    AST.ident List.list -> Registers.register List.list -> Joint.psd_argument
788    List.list -> Joint.psd_argument List.list -> (Registers.register,
789    Joint.joint_seq List.list) Bind_new.bind_new **)
790let translate_ne globals destrs srcrs1 srcrs2 =
791  (match destrs with
792   | List.Nil -> (fun _ -> let l = List.Nil in Bind_new.Bret l)
793   | List.Cons (destr, destrs') ->
794     (fun _ ->
795       BindLists.bappend
796         (let l = translate_fill_with_zero globals destrs' in
797         Bind_new.Bret l)
798         ((match srcrs1 with
799           | List.Nil ->
800             (fun _ ->
801               let l = List.Cons ((Joint.MOVE
802                 (Obj.magic { Types.fst = destr; Types.snd =
803                   (Joint.psd_argument_from_byte Joint.zero_byte) })),
804                 List.Nil)
805               in
806               Bind_new.Bret l)
807           | List.Cons (srcr1, srcrs1') ->
808             (match srcrs2 with
809              | List.Nil -> (fun _ -> assert false (* absurd case *))
810              | List.Cons (srcr2, srcrs2') ->
811                (fun _ -> Bind_new.Bnew (fun tmpr ->
812                  let f = fun s1 s2 acc -> List.Cons ((Joint.OP2
813                    (BackEndOps.Xor, (Obj.magic tmpr), s1, s2)), (List.Cons
814                    ((Joint.OP2 (BackEndOps.Or, (Obj.magic destr),
815                    (Obj.magic (Joint.psd_argument_from_reg destr)),
816                    (Obj.magic (Joint.psd_argument_from_reg tmpr)))), acc)))
817                  in
818                  let epilogue = List.Cons (Joint.CLEAR_CARRY, (List.Cons
819                    ((Joint.OP2 (BackEndOps.Sub, (Obj.magic tmpr),
820                    (Obj.magic
821                      (Joint.psd_argument_from_byte Joint.zero_byte)),
822                    (Obj.magic (Joint.psd_argument_from_reg destr)))),
823                    (List.Cons ((Joint.OP2 (BackEndOps.Addc,
824                    (Obj.magic destr),
825                    (Obj.magic
826                      (Joint.psd_argument_from_byte Joint.zero_byte)),
827                    (Obj.magic
828                      (Joint.psd_argument_from_byte Joint.zero_byte)))),
829                    List.Nil)))))
830                  in
831                  let l = List.Cons ((Joint.OP2 (BackEndOps.Xor,
832                    (Obj.magic destr), (Obj.magic srcr1),
833                    (Obj.magic srcr2))),
834                    (foldr2 f epilogue (Obj.magic srcrs1')
835                      (Obj.magic srcrs2')))
836                  in
837                  Bind_new.Bret l)))) __))) __
838
839(** val translate_toggle_bool :
840    AST.ident List.list -> Registers.register List.list ->
841    (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new **)
842let translate_toggle_bool globals destrs =
843  (match destrs with
844   | List.Nil -> (fun _ -> let l = List.Nil in Bind_new.Bret l)
845   | List.Cons (destr, x) ->
846     (fun _ ->
847       let l = List.Cons ((Joint.OP1 (BackEndOps.Cmpl, (Obj.magic destr),
848         (Obj.magic destr))), List.Nil)
849       in
850       Bind_new.Bret l)) __
851
852(** val translate_lt_unsigned :
853    AST.ident List.list -> Registers.register List.list -> Joint.psd_argument
854    List.list -> Joint.psd_argument List.list -> (Registers.register,
855    Joint.joint_seq List.list) Bind_new.bind_new **)
856let translate_lt_unsigned globals destrs srcrs1 srcrs2 =
857  match destrs with
858  | List.Nil -> let l = List.Nil in Bind_new.Bret l
859  | List.Cons (destr, destrs') ->
860    Bind_new.Bnew (fun tmpr ->
861      BindLists.bappend
862        (let l = translate_fill_with_zero globals destrs' in Bind_new.Bret l)
863        (BindLists.bappend
864          (translate_op globals BackEndOps.Sub
865            (List.make_list tmpr (List.length srcrs1)) srcrs1 srcrs2)
866          (let l = List.Cons ((Joint.OP2 (BackEndOps.Addc, (Obj.magic destr),
867             (Obj.magic (Joint.psd_argument_from_byte Joint.zero_byte)),
868             (Obj.magic (Joint.psd_argument_from_byte Joint.zero_byte)))),
869             List.Nil)
870           in
871          Bind_new.Bret l)))
872
873(** val shift_signed :
874    AST.ident List.list -> Registers.register -> Joint.psd_argument List.list
875    -> (Joint.psd_argument List.list, Joint.joint_seq List.list) Types.prod
876    Types.sig0 **)
877let rec shift_signed globals tmp srcrs =
878  let byte_128 = Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
879    (Nat.S Nat.O))))))), Bool.True,
880    (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
881      Nat.O)))))))))
882  in
883  (match srcrs with
884   | List.Nil -> (fun _ -> { Types.fst = List.Nil; Types.snd = List.Nil })
885   | List.Cons (srcr, srcrs') ->
886     (fun _ ->
887       (match srcrs' with
888        | List.Nil ->
889          (fun _ -> { Types.fst = (List.Cons ((Joint.Reg tmp), List.Nil));
890            Types.snd = (List.Cons ((Joint.OP2 (BackEndOps.Add,
891            (Obj.magic tmp), (Obj.magic srcr),
892            (Obj.magic (Joint.psd_argument_from_byte byte_128)))),
893            List.Nil)) })
894        | List.Cons (x, x0) ->
895          (fun _ ->
896            let re = shift_signed globals tmp srcrs' in
897            { Types.fst = (List.Cons (srcr, (Types.pi1 re).Types.fst));
898            Types.snd = (Types.pi1 re).Types.snd })) __)) __
899
900(** val translate_lt_signed :
901    AST.ident List.list -> Registers.register List.list -> Joint.psd_argument
902    List.list -> Joint.psd_argument List.list -> (Registers.register,
903    Joint.joint_seq List.list) Bind_new.bind_new **)
904let translate_lt_signed globals destrs srcrs1 srcrs2 =
905  Bind_new.Bnew (fun tmp_last_s1 -> Bind_new.Bnew (fun tmp_last_s2 ->
906    let p3 = shift_signed globals tmp_last_s1 srcrs1 in
907    let new_srcrs1 = (Types.pi1 p3).Types.fst in
908    let shift_srcrs1 = (Types.pi1 p3).Types.snd in
909    let p4 = shift_signed globals tmp_last_s2 srcrs2 in
910    let new_srcrs2 = (Types.pi1 p4).Types.fst in
911    let shift_srcrs2 = (Types.pi1 p4).Types.snd in
912    BindLists.bappend (let l = shift_srcrs1 in Bind_new.Bret l)
913      (BindLists.bappend (let l = shift_srcrs2 in Bind_new.Bret l)
914        (translate_lt_unsigned globals destrs new_srcrs1 new_srcrs2))))
915
916(** val translate_lt :
917    Bool.bool -> AST.ident List.list -> Registers.register List.list ->
918    Joint.psd_argument List.list -> Joint.psd_argument List.list ->
919    (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new **)
920let translate_lt is_unsigned globals destrs srcrs1 srcrs2 =
921  match is_unsigned with
922  | Bool.True -> translate_lt_unsigned globals destrs srcrs1 srcrs2
923  | Bool.False -> translate_lt_signed globals destrs srcrs1 srcrs2
924
925(** val translate_cmp :
926    Bool.bool -> AST.ident List.list -> Integers.comparison ->
927    Registers.register List.list -> Joint.psd_argument List.list ->
928    Joint.psd_argument List.list -> (Registers.register, Joint.joint_seq)
929    BindLists.bind_list **)
930let translate_cmp is_unsigned globals cmp1 destrs srcrs1 srcrs2 =
931  match cmp1 with
932  | Integers.Ceq ->
933    BindLists.bappend (translate_ne globals destrs srcrs1 srcrs2)
934      (translate_toggle_bool globals destrs)
935  | Integers.Cne -> translate_ne globals destrs srcrs1 srcrs2
936  | Integers.Clt -> translate_lt is_unsigned globals destrs srcrs1 srcrs2
937  | Integers.Cle ->
938    BindLists.bappend (translate_lt is_unsigned globals destrs srcrs2 srcrs1)
939      (translate_toggle_bool globals destrs)
940  | Integers.Cgt -> translate_lt is_unsigned globals destrs srcrs2 srcrs1
941  | Integers.Cge ->
942    BindLists.bappend (translate_lt is_unsigned globals destrs srcrs1 srcrs2)
943      (translate_toggle_bool globals destrs)
944
945(** val translate_op2 :
946    AST.ident List.list -> AST.typ -> AST.typ -> AST.typ ->
947    FrontEndOps.binary_operation -> Registers.register List.list ->
948    Joint.psd_argument List.list -> Joint.psd_argument List.list ->
949    (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new **)
950let translate_op2 globals ty1 ty2 ty3 op4 destrs srcrs1 srcrs2 =
951  (match op4 with
952   | FrontEndOps.Oadd (sz, sg) ->
953     (fun _ _ _ -> translate_op globals BackEndOps.Add destrs srcrs1 srcrs2)
954   | FrontEndOps.Osub (sz, sg) ->
955     (fun _ _ _ -> translate_op globals BackEndOps.Sub destrs srcrs1 srcrs2)
956   | FrontEndOps.Omul (sz, sg) ->
957     (fun _ _ _ -> translate_mul globals destrs srcrs1 srcrs2)
958   | FrontEndOps.Odiv x -> assert false (* absurd case *)
959   | FrontEndOps.Odivu sz ->
960     (fun _ _ _ ->
961       translate_divumodu8 globals Bool.True destrs srcrs1 srcrs2)
962   | FrontEndOps.Omod x -> assert false (* absurd case *)
963   | FrontEndOps.Omodu sz ->
964     (fun _ _ _ ->
965       translate_divumodu8 globals Bool.False destrs srcrs1 srcrs2)
966   | FrontEndOps.Oand (sz, sg) ->
967     (fun _ _ _ -> translate_op globals BackEndOps.And destrs srcrs1 srcrs2)
968   | FrontEndOps.Oor (sz, sg) ->
969     (fun _ _ _ -> translate_op globals BackEndOps.Or destrs srcrs1 srcrs2)
970   | FrontEndOps.Oxor (sz, sg) ->
971     (fun _ _ _ -> translate_op globals BackEndOps.Xor destrs srcrs1 srcrs2)
972   | FrontEndOps.Oshl (x, x0) -> assert false (* absurd case *)
973   | FrontEndOps.Oshr (x, x0) -> assert false (* absurd case *)
974   | FrontEndOps.Oshru (x, x0) -> assert false (* absurd case *)
975   | FrontEndOps.Ocmp (sz, sg1, sg2, c) ->
976     (fun _ _ _ -> translate_cmp Bool.False globals c destrs srcrs1 srcrs2)
977   | FrontEndOps.Ocmpu (sz, sg, c) ->
978     (fun _ _ _ -> translate_cmp Bool.True globals c destrs srcrs1 srcrs2)
979   | FrontEndOps.Oaddpi sz ->
980     (fun _ _ _ ->
981       translate_op_asym_signed globals BackEndOps.Add destrs srcrs1 srcrs2)
982   | FrontEndOps.Oaddip sz ->
983     (fun _ _ _ ->
984       translate_op_asym_signed globals BackEndOps.Add destrs srcrs2 srcrs1)
985   | FrontEndOps.Osubpi sz ->
986     (fun _ _ _ ->
987       translate_op_asym_signed globals BackEndOps.Add destrs srcrs1 srcrs2)
988   | FrontEndOps.Osubpp sz ->
989     (fun _ _ _ ->
990       translate_op_asym_unsigned globals BackEndOps.Sub destrs srcrs1 srcrs2)
991   | FrontEndOps.Ocmpp (sg, c) ->
992     (fun _ _ _ ->
993       let is_Ocmpp = Nat.O in
994       translate_cmp Bool.True globals c destrs srcrs1 srcrs2)) __ __ __
995
996(** val translate_cond :
997    AST.ident List.list -> Registers.register List.list -> Graphs.label ->
998    Blocks.bind_step_block **)
999let translate_cond globals srcrs lbl_true =
1000  match srcrs with
1001  | List.Nil ->
1002    Bind_new.Bret
1003      (Blocks.ensure_step_block (Joint.graph_params_to_params RTL.rTL)
1004        globals List.Nil)
1005  | List.Cons (srcr, srcrs') ->
1006    Bind_new.Bnew (fun tmpr ->
1007      let f = fun r x -> Joint.OP2 (BackEndOps.Or, (Obj.magic tmpr),
1008        (Obj.magic (Joint.psd_argument_from_reg tmpr)),
1009        (Obj.magic (Joint.psd_argument_from_reg r)))
1010      in
1011      Bind_new.Bret { Types.fst = { Types.fst = (List.Cons ((fun x ->
1012      Joint.MOVE
1013      (Obj.magic { Types.fst = tmpr; Types.snd =
1014        (Joint.psd_argument_from_reg srcr) })), (List.map f srcrs')));
1015      Types.snd = (fun x -> Joint.COND ((Obj.magic tmpr), lbl_true)) };
1016      Types.snd = List.Nil })
1017
1018(** val translate_load :
1019    AST.ident List.list -> Joint.psd_argument List.list -> Registers.register
1020    List.list -> (Registers.register, Joint.joint_seq List.list)
1021    Bind_new.bind_new **)
1022let translate_load globals addr destrs =
1023  Bind_new.Bnew (fun tmp_addr_l -> Bind_new.Bnew (fun tmp_addr_h ->
1024    BindLists.bappend
1025      (let l =
1026         translate_move globals (List.Cons (tmp_addr_l, (List.Cons
1027           (tmp_addr_h, List.Nil)))) addr
1028       in
1029      Bind_new.Bret l)
1030      (let f = fun destr acc ->
1031         BindLists.bappend
1032           (let l = List.Cons ((Joint.LOAD (destr,
1033              (Obj.magic (Joint.Reg tmp_addr_l)),
1034              (Obj.magic (Joint.Reg tmp_addr_h)))), List.Nil)
1035            in
1036           Bind_new.Bret l)
1037           (BindLists.bappend
1038             (translate_op globals BackEndOps.Add (List.Cons (tmp_addr_l,
1039               (List.Cons (tmp_addr_h, List.Nil)))) (List.Cons
1040               ((Joint.psd_argument_from_reg tmp_addr_l), (List.Cons
1041               ((Joint.psd_argument_from_reg tmp_addr_h), List.Nil))))
1042               (List.Cons ((Joint.psd_argument_from_byte Joint.zero_byte),
1043               (List.Cons
1044               ((let x = I8051.int_size in Joint.psd_argument_from_byte x),
1045               List.Nil))))) acc)
1046       in
1047      List.foldr f (let l = List.Nil in Bind_new.Bret l) (Obj.magic destrs))))
1048
1049(** val translate_store :
1050    AST.ident List.list -> Joint.psd_argument List.list -> Joint.psd_argument
1051    List.list -> (Registers.register, Joint.joint_seq List.list)
1052    Bind_new.bind_new **)
1053let translate_store globals addr srcrs =
1054  Bind_new.Bnew (fun tmp_addr_l -> Bind_new.Bnew (fun tmp_addr_h ->
1055    BindLists.bappend
1056      (let l =
1057         translate_move globals (List.Cons (tmp_addr_l, (List.Cons
1058           (tmp_addr_h, List.Nil)))) addr
1059       in
1060      Bind_new.Bret l)
1061      (let f = fun srcr acc ->
1062         BindLists.bappend
1063           (let l = List.Cons ((Joint.STORE
1064              ((Obj.magic (Joint.Reg tmp_addr_l)),
1065              (Obj.magic (Joint.Reg tmp_addr_h)), srcr)), List.Nil)
1066            in
1067           Bind_new.Bret l)
1068           (BindLists.bappend
1069             (translate_op globals BackEndOps.Add (List.Cons (tmp_addr_l,
1070               (List.Cons (tmp_addr_h, List.Nil)))) (List.Cons
1071               ((Joint.psd_argument_from_reg tmp_addr_l), (List.Cons
1072               ((Joint.psd_argument_from_reg tmp_addr_h), List.Nil))))
1073               (List.Cons ((Joint.psd_argument_from_byte Joint.zero_byte),
1074               (List.Cons
1075               ((let x = I8051.int_size in Joint.psd_argument_from_byte x),
1076               List.Nil))))) acc)
1077       in
1078      List.foldr f (let l = List.Nil in Bind_new.Bret l) (Obj.magic srcrs))))
1079
1080(** val ensure_bind_step_block :
1081    Joint.params -> AST.ident List.list -> (Registers.register,
1082    Joint.joint_seq List.list) Bind_new.bind_new -> Blocks.bind_step_block **)
1083let ensure_bind_step_block p g0 b =
1084  Obj.magic
1085    (Monad.m_bind0 (Monad.max_def Bind_new.bindNew) (Obj.magic b) (fun l ->
1086      Obj.magic (Bind_new.Bret (Blocks.ensure_step_block p g0 l))))
1087
1088(** val translate_statement :
1089    AST.ident List.list -> (Registers.register, AST.typ) Types.prod List.list
1090    -> local_env -> RTLabs_syntax.statement -> ((Blocks.bind_step_block,
1091    Blocks.bind_fin_block) Types.sum, __) Types.dPair **)
1092let translate_statement globals locals lenv stmt =
1093  (match stmt with
1094   | RTLabs_syntax.St_skip lbl' ->
1095     (fun _ -> { Types.dpi1 = (Types.Inl (Bind_new.Bret
1096       (Blocks.ensure_step_block (Joint.graph_params_to_params RTL.rTL)
1097         globals List.Nil))); Types.dpi2 = (Obj.magic lbl') })
1098   | RTLabs_syntax.St_cost (cost_lbl, lbl') ->
1099     (fun _ -> { Types.dpi1 = (Types.Inl (Bind_new.Bret { Types.fst =
1100       { Types.fst = List.Nil; Types.snd = (fun x -> Joint.COST_LABEL
1101       cost_lbl) }; Types.snd = List.Nil })); Types.dpi2 =
1102       (Obj.magic lbl') })
1103   | RTLabs_syntax.St_const (ty, destr, cst, lbl') ->
1104     (fun _ -> { Types.dpi1 = (Types.Inl
1105       (ensure_bind_step_block (Joint.graph_params_to_params RTL.rTL) globals
1106         (translate_cst ty globals cst (find_local_env destr lenv))));
1107       Types.dpi2 = (Obj.magic lbl') })
1108   | RTLabs_syntax.St_op1 (ty, ty', op4, destr, srcr, lbl') ->
1109     (fun _ -> { Types.dpi1 = (Types.Inl
1110       (ensure_bind_step_block (Joint.graph_params_to_params RTL.rTL) globals
1111         (translate_op1 globals ty' ty op4 (find_local_env destr lenv)
1112           (find_local_env srcr lenv)))); Types.dpi2 = (Obj.magic lbl') })
1113   | RTLabs_syntax.St_op2 (ty1, ty2, ty3, op4, destr, srcr1, srcr2, lbl') ->
1114     (fun _ -> { Types.dpi1 = (Types.Inl
1115       (ensure_bind_step_block (Joint.graph_params_to_params RTL.rTL) globals
1116         (translate_op2 globals ty2 ty3 ty1 op4 (find_local_env destr lenv)
1117           (find_local_env_arg srcr1 lenv) (find_local_env_arg srcr2 lenv))));
1118       Types.dpi2 = (Obj.magic lbl') })
1119   | RTLabs_syntax.St_load (ignore, addr, destr, lbl') ->
1120     (fun _ -> { Types.dpi1 = (Types.Inl
1121       (ensure_bind_step_block (Joint.graph_params_to_params RTL.rTL) globals
1122         (translate_load globals (find_local_env_arg addr lenv)
1123           (find_local_env destr lenv)))); Types.dpi2 = (Obj.magic lbl') })
1124   | RTLabs_syntax.St_store (ignore, addr, srcr, lbl') ->
1125     (fun _ -> { Types.dpi1 = (Types.Inl
1126       (ensure_bind_step_block (Joint.graph_params_to_params RTL.rTL) globals
1127         (translate_store globals (find_local_env_arg addr lenv)
1128           (find_local_env_arg srcr lenv)))); Types.dpi2 =
1129       (Obj.magic lbl') })
1130   | RTLabs_syntax.St_call_id (f, args, retr, lbl') ->
1131     (fun _ -> { Types.dpi1 = (Types.Inl (Bind_new.Bret { Types.fst =
1132       { Types.fst = List.Nil; Types.snd = (fun x -> Joint.CALL ((Types.Inl
1133       f), (Obj.magic (rtl_args args lenv)),
1134       (match retr with
1135        | Types.None -> Obj.magic List.Nil
1136        | Types.Some retr0 -> Obj.magic (find_local_env retr0 lenv)))) };
1137       Types.snd = List.Nil })); Types.dpi2 = (Obj.magic lbl') })
1138   | RTLabs_syntax.St_call_ptr (f, args, retr, lbl') ->
1139     (fun _ ->
1140       let fs = find_and_addr_arg f lenv in
1141       { Types.dpi1 = (Types.Inl (Bind_new.Bret { Types.fst = { Types.fst =
1142       List.Nil; Types.snd = (fun x -> Joint.CALL ((Types.Inr
1143       (Obj.magic fs)), (Obj.magic (rtl_args args lenv)),
1144       (match retr with
1145        | Types.None -> Obj.magic List.Nil
1146        | Types.Some retr0 -> Obj.magic (find_local_env retr0 lenv)))) };
1147       Types.snd = List.Nil })); Types.dpi2 = (Obj.magic lbl') })
1148   | RTLabs_syntax.St_cond (r, lbl_true, lbl_false) ->
1149     (fun _ -> { Types.dpi1 = (Types.Inl
1150       (translate_cond globals (find_local_env r lenv) lbl_true));
1151       Types.dpi2 = (Obj.magic lbl_false) })
1152   | RTLabs_syntax.St_return ->
1153     (fun _ -> { Types.dpi1 = (Types.Inr (Bind_new.Bret { Types.fst =
1154       List.Nil; Types.snd = Joint.RETURN })); Types.dpi2 =
1155       (Obj.magic Types.It) })) __
1156
1157(** val translate_internal :
1158    AST.ident List.list -> RTLabs_syntax.internal_function ->
1159    Joint.joint_closed_internal_function **)
1160let translate_internal globals def =
1161  let runiverse' = def.RTLabs_syntax.f_reggen in
1162  let luniverse' = def.RTLabs_syntax.f_labgen in
1163  let stack_size' = def.RTLabs_syntax.f_stacksize in
1164  let entry' = def.RTLabs_syntax.f_entry in
1165  let init = { Joint.joint_if_luniverse = luniverse';
1166    Joint.joint_if_runiverse = runiverse'; Joint.joint_if_result =
1167    (Obj.magic List.Nil); Joint.joint_if_params = (Obj.magic List.Nil);
1168    Joint.joint_if_stacksize = stack_size'; Joint.joint_if_code =
1169    (Obj.magic
1170      (Identifiers.add PreIdentifiers.LabelTag
1171        (Identifiers.empty_map PreIdentifiers.LabelTag) (Types.pi1 entry')
1172        (Joint.Final Joint.RETURN))); Joint.joint_if_entry =
1173    (Types.pi1 (Obj.magic entry')) }
1174  in
1175  (let { Types.fst = init'; Types.snd = lenv } =
1176     Obj.magic initialize_locals_params_ret globals
1177       def.RTLabs_syntax.f_locals def.RTLabs_syntax.f_params
1178       def.RTLabs_syntax.f_result init
1179   in
1180  (fun _ ->
1181  let vars =
1182    List.append def.RTLabs_syntax.f_locals
1183      (List.append def.RTLabs_syntax.f_params
1184        (match def.RTLabs_syntax.f_result with
1185         | Types.None -> List.Nil
1186         | Types.Some x -> List.Cons (x, List.Nil)))
1187  in
1188  let f_trans = fun lbl stmt def0 ->
1189    let pr = translate_statement globals vars lenv stmt in
1190    (match pr.Types.dpi1 with
1191     | Types.Inl instrs ->
1192       (fun lbl' ->
1193         TranslateUtils.b_adds_graph RTL.rTL globals instrs lbl
1194           (Obj.magic lbl') def0)
1195     | Types.Inr instrs ->
1196       (fun x ->
1197         TranslateUtils.b_fin_adds_graph RTL.rTL globals instrs lbl def0))
1198      pr.Types.dpi2
1199  in
1200  Identifiers.foldi0 PreIdentifiers.LabelTag f_trans
1201    def.RTLabs_syntax.f_graph init')) __
1202
1203(** val rtlabs_to_rtl : RTLabs_syntax.rTLabs_program -> RTL.rtl_program **)
1204let rtlabs_to_rtl p =
1205  AST.transform_program p (fun varnames ->
1206    AST.transf_fundef (translate_internal varnames))
1207
Note: See TracBrowser for help on using the repository browser.