source: driver/extracted/rTLabsToRTL.ml @ 3106

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

New extraction

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