source: extracted/rTLabsToRTL.ml @ 2933

Last change on this file since 2933 was 2933, checked in by sacerdot, 6 years ago

New extraction, several bug fixed. RTL_semantics fixed by hand, will be fixed
automatically when Paolo commits.

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