source: extracted/rTLabsToRTL.ml @ 2873

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

Extracted again.

File size: 48.9 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_21297 -> h_register_int x_21297
153| Register_ptr (x_21299, x_21298) -> h_register_ptr x_21299 x_21298
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_21303 -> h_register_int x_21303
160| Register_ptr (x_21305, x_21304) -> h_register_ptr x_21305 x_21304
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_21309 -> h_register_int x_21309
167| Register_ptr (x_21311, x_21310) -> h_register_ptr x_21311 x_21310
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_21315 -> h_register_int x_21315
174| Register_ptr (x_21317, x_21316) -> h_register_ptr x_21317 x_21316
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_21321 -> h_register_int x_21321
181| Register_ptr (x_21323, x_21322) -> h_register_ptr x_21323 x_21322
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_21327 -> h_register_int x_21327
188| Register_ptr (x_21329, x_21328) -> h_register_ptr x_21329 x_21328
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    (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new **)
389let translate_op globals op destrs srcrs1 srcrs2 =
390  (match op with
391   | BackEndOps.Add ->
392     (fun _ ->
393       (match destrs with
394        | List.Nil -> (fun _ _ _ -> let l = List.Nil in Bind_new.Bret l)
395        | List.Cons (destr, destrs') ->
396          (fun _ ->
397            (match srcrs1 with
398             | List.Nil -> (fun _ _ -> assert false (* absurd case *))
399             | List.Cons (srcr1, srcrs1') ->
400               (fun _ _ ->
401                 (match srcrs2 with
402                  | List.Nil -> (fun _ _ -> assert false (* absurd case *))
403                  | List.Cons (srcr2, srcrs2') ->
404                    (fun _ _ ->
405                      let l = List.Cons ((Joint.OP2 (BackEndOps.Add,
406                        (Obj.magic destr), (Obj.magic srcr1),
407                        (Obj.magic srcr2))),
408                        (translate_op_aux globals BackEndOps.Addc destrs'
409                          srcrs1' srcrs2'))
410                      in
411                      Bind_new.Bret l)) __)) __)) __)
412   | BackEndOps.Addc ->
413     (fun _ _ _ ->
414       let l =
415         List.append (List.Cons (Joint.CLEAR_CARRY, List.Nil))
416           (translate_op_aux globals BackEndOps.Addc destrs srcrs1 srcrs2)
417       in
418       Bind_new.Bret l)
419   | BackEndOps.Sub ->
420     (fun _ _ _ ->
421       let l =
422         List.append (List.Cons (Joint.CLEAR_CARRY, List.Nil))
423           (translate_op_aux globals BackEndOps.Sub destrs srcrs1 srcrs2)
424       in
425       Bind_new.Bret l)
426   | BackEndOps.And ->
427     (fun _ _ _ ->
428       let l = translate_op_aux globals op destrs srcrs1 srcrs2 in
429       Bind_new.Bret l)
430   | BackEndOps.Or ->
431     (fun _ _ _ ->
432       let l = translate_op_aux globals op destrs srcrs1 srcrs2 in
433       Bind_new.Bret l)
434   | BackEndOps.Xor ->
435     (fun _ _ _ ->
436       let l = translate_op_aux globals op destrs srcrs1 srcrs2 in
437       Bind_new.Bret l)) __ __ __
438
439(** val cast_list : 'a1 -> Nat.nat -> 'a1 List.list -> 'a1 List.list **)
440let cast_list deflt new_length l =
441  match Nat.leb (List.length l) new_length with
442  | Bool.True ->
443    List.append l
444      (List.make_list deflt (Nat.minus new_length (List.length l)))
445  | Bool.False -> List.lhd l new_length
446
447(** val translate_op_asym_unsigned :
448    AST.ident List.list -> BackEndOps.op2 -> Registers.register List.list ->
449    Joint.psd_argument List.list -> Joint.psd_argument List.list ->
450    (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new **)
451let translate_op_asym_unsigned globals op destrs srcrs1 srcrs2 =
452  let l = List.length destrs in
453  let srcrs1' =
454    cast_list (let x = Joint.psd_argument_from_byte Joint.zero_byte in x) l
455      srcrs1
456  in
457  let srcrs2' =
458    cast_list (let x = Joint.psd_argument_from_byte Joint.zero_byte in x) l
459      srcrs2
460  in
461  translate_op globals op destrs srcrs1' srcrs2'
462
463(** val zero_args : Nat.nat -> Joint.psd_argument List.list Types.sig0 **)
464let zero_args size =
465  List.make_list (Joint.psd_argument_from_byte Joint.zero_byte) size
466
467(** val one_args : Nat.nat -> Joint.psd_argument List.list Types.sig0 **)
468let one_args = function
469| Nat.O -> List.Nil
470| Nat.S k ->
471  List.Cons
472    ((let x = Joint.psd_argument_from_byte (Joint.byte_of_nat (Nat.S Nat.O))
473      in
474     x), (Types.pi1 (zero_args k)))
475
476(** val size_of_cst : AST.typ -> FrontEndOps.constant -> Nat.nat **)
477let size_of_cst typ = function
478| FrontEndOps.Ointconst (size, x, x0) -> AST.size_intsize size
479| FrontEndOps.Oaddrsymbol (x, x0) -> Nat.S (Nat.S Nat.O)
480| FrontEndOps.Oaddrstack x -> Nat.S (Nat.S Nat.O)
481
482(** val translate_cst :
483    AST.typ -> AST.ident List.list -> FrontEndOps.constant Types.sig0 ->
484    Registers.register List.list -> (Registers.register, Joint.joint_seq
485    List.list) Bind_new.bind_new **)
486let translate_cst ty globals cst_sig destrs =
487  let l =
488    (match Types.pi1 cst_sig with
489     | FrontEndOps.Ointconst (size, sign, const) ->
490       (fun _ _ ->
491         Util.map2 (fun r b -> Joint.MOVE
492           (Obj.magic { Types.fst = r; Types.snd =
493             (Joint.psd_argument_from_byte b) })) destrs
494           (Types.pi1 (split_into_bytes size const)))
495     | FrontEndOps.Oaddrsymbol (id, offset) ->
496       (fun _ _ ->
497         let { Types.fst = r1; Types.snd = r2 } = make_addr destrs in
498         List.Cons ((Joint.ADDRESS (id, (Obj.magic r1), (Obj.magic r2))),
499         (List.Cons ((Joint.OP2 (BackEndOps.Add, (Obj.magic r1),
500         (Obj.magic (Joint.psd_argument_from_reg r1)),
501         (Obj.magic
502           (Joint.psd_argument_from_byte (Joint.byte_of_nat offset))))),
503         (List.Cons ((Joint.OP2 (BackEndOps.Addc, (Obj.magic r2),
504         (Obj.magic (Joint.psd_argument_from_reg r2)),
505         (Obj.magic (Joint.psd_argument_from_byte Joint.zero_byte)))),
506         List.Nil))))))
507     | FrontEndOps.Oaddrstack offset ->
508       (fun _ _ ->
509         let { Types.fst = r1; Types.snd = r2 } = make_addr destrs in
510         List.Cons
511         ((let x = Joint.Extension_seq
512             (Obj.magic (RTL.Rtl_stack_address (r1, r2)))
513           in
514          x), (List.Cons ((Joint.OP2 (BackEndOps.Add, (Obj.magic r1),
515         (Obj.magic (Joint.psd_argument_from_reg r1)),
516         (Obj.magic
517           (Joint.psd_argument_from_byte (Joint.byte_of_nat offset))))),
518         (List.Cons ((Joint.OP2 (BackEndOps.Addc, (Obj.magic r2),
519         (Obj.magic (Joint.psd_argument_from_reg r2)),
520         (Obj.magic (Joint.psd_argument_from_byte Joint.zero_byte)))),
521         List.Nil))))))) __ __
522  in
523  Bind_new.Bret l
524
525(** val translate_move :
526    AST.ident List.list -> Registers.register List.list -> Joint.psd_argument
527    List.list -> Joint.joint_seq List.list **)
528let translate_move globals destrs srcrs =
529  Util.map2 (fun dst src -> Joint.MOVE
530    (Obj.magic { Types.fst = dst; Types.snd = src })) destrs srcrs
531
532(** val sign_mask :
533    AST.ident List.list -> Registers.register -> Joint.psd_argument ->
534    Joint.joint_seq List.list **)
535let sign_mask globals destr = function
536| Joint.Reg srcr ->
537  let byte_127 = Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
538    (Nat.S Nat.O))))))), Bool.False,
539    (BitVector.maximum (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
540      Nat.O)))))))))
541  in
542  List.Cons ((Joint.OP2 (BackEndOps.Or, (Obj.magic destr),
543  (Obj.magic (Joint.psd_argument_from_reg srcr)),
544  (Obj.magic (Joint.psd_argument_from_byte byte_127)))), (List.Cons
545  ((Joint.OP1 (BackEndOps.Rl, (Obj.magic destr), (Obj.magic destr))),
546  (List.Cons ((Joint.OP1 (BackEndOps.Inc, (Obj.magic destr),
547  (Obj.magic destr))), (List.Cons ((Joint.OP1 (BackEndOps.Cmpl,
548  (Obj.magic destr), (Obj.magic destr))), List.Nil)))))))
549| Joint.Imm b ->
550  (match Arithmetic.sign_bit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
551           (Nat.S Nat.O)))))))) b with
552   | Bool.True ->
553     List.Cons ((Joint.MOVE
554       (Obj.magic { Types.fst = destr; Types.snd =
555         (let x =
556            BitVector.maximum (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
557              (Nat.S (Nat.S Nat.O))))))))
558          in
559         Joint.psd_argument_from_byte x) })), List.Nil)
560   | Bool.False ->
561     List.Cons ((Joint.MOVE
562       (Obj.magic { Types.fst = destr; Types.snd =
563         (Joint.psd_argument_from_byte Joint.zero_byte) })), List.Nil))
564
565(** val translate_cast_signed :
566    AST.ident List.list -> Registers.register List.list -> Joint.psd_argument
567    -> (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new **)
568let translate_cast_signed globals destrs srca =
569  Bind_new.Bnew (fun tmp ->
570    let l =
571      List.append (sign_mask globals tmp srca)
572        (translate_move globals destrs
573          (List.make_list (Joint.Reg tmp) (List.length destrs)))
574    in
575    Bind_new.Bret l)
576
577(** val translate_fill_with_zero :
578    AST.ident List.list -> Registers.register List.list -> Joint.joint_seq
579    List.list **)
580let translate_fill_with_zero globals destrs =
581  translate_move globals destrs (Types.pi1 (zero_args (List.length destrs)))
582
583(** val last : 'a1 List.list -> 'a1 Types.option **)
584let rec last = function
585| List.Nil -> Types.None
586| List.Cons (hd, tl) ->
587  (match tl with
588   | List.Nil -> Types.Some hd
589   | List.Cons (x, x0) -> last tl)
590
591(** val translate_op_asym_signed :
592    AST.ident List.list -> BackEndOps.op2 -> Registers.register List.list ->
593    Joint.psd_argument List.list -> Joint.psd_argument List.list ->
594    (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new **)
595let translate_op_asym_signed globals op destrs srcrs1 srcrs2 =
596  Bind_new.Bnew (fun tmp1 -> Bind_new.Bnew (fun tmp2 ->
597    let l = List.length destrs in
598    let cast_srcrs = fun srcrs tmp ->
599      let srcrs_l = List.length srcrs in
600      (match Nat.leb srcrs_l l with
601       | Bool.True ->
602         (match last srcrs with
603          | Types.None ->
604            { Types.fst =
605              (List.make_list
606                (let x = Joint.psd_argument_from_byte Joint.zero_byte in x)
607                l); Types.snd = List.Nil }
608          | Types.Some last0 ->
609            { Types.fst =
610              (List.append srcrs
611                (List.make_list (Joint.Reg tmp) (Nat.minus l srcrs_l)));
612              Types.snd = (sign_mask globals tmp last0) })
613       | Bool.False ->
614         { Types.fst = (List.lhd srcrs l); Types.snd = List.Nil })
615    in
616    let srcrs1init = cast_srcrs srcrs1 tmp1 in
617    let srcrs2init = cast_srcrs srcrs2 tmp2 in
618    BindLists.bappend (let l0 = srcrs1init.Types.snd in Bind_new.Bret l0)
619      (BindLists.bappend (let l0 = srcrs2init.Types.snd in Bind_new.Bret l0)
620        (translate_op globals op destrs srcrs1init.Types.fst
621          srcrs2init.Types.fst))))
622
623(** val translate_cast :
624    AST.ident List.list -> AST.signedness -> Registers.register List.list ->
625    Registers.register List.list -> (Registers.register, Joint.joint_seq
626    List.list) Bind_new.bind_new **)
627let translate_cast globals src_sign destrs srcrs =
628  let t = Util.reduce_strong destrs srcrs in
629  let src_common = t.Types.fst.Types.fst in
630  let src_rest = t.Types.fst.Types.snd in
631  let dst_common = t.Types.snd.Types.fst in
632  let dst_rest = t.Types.snd.Types.snd in
633  BindLists.bappend
634    (let l =
635       translate_move globals src_common
636         (List.map (fun x -> Joint.Reg x) dst_common)
637     in
638    Bind_new.Bret l)
639    (match src_rest with
640     | List.Nil ->
641       (match src_sign with
642        | AST.Signed ->
643          (match last srcrs with
644           | Types.None ->
645             let l = translate_fill_with_zero globals dst_rest in
646             Bind_new.Bret l
647           | Types.Some src_last ->
648             translate_cast_signed globals dst_rest
649               (Joint.psd_argument_from_reg src_last))
650        | AST.Unsigned ->
651          let l = translate_fill_with_zero globals dst_rest in
652          Bind_new.Bret l)
653     | List.Cons (x, x0) -> let l = List.Nil in Bind_new.Bret l)
654
655(** val translate_notint :
656    AST.ident List.list -> Registers.register List.list -> Registers.register
657    List.list -> Joint.joint_seq List.list **)
658let translate_notint globals destrs srcrs =
659  Util.map2 (fun x x0 -> Joint.OP1 (BackEndOps.Cmpl, x, x0))
660    (Obj.magic destrs) (Obj.magic srcrs)
661
662(** val translate_negint :
663    AST.ident List.list -> Registers.register List.list -> Registers.register
664    List.list -> (Registers.register, Joint.joint_seq List.list)
665    Bind_new.bind_new **)
666let translate_negint globals destrs srcrs =
667  BindLists.bappend
668    (let l = translate_notint globals destrs srcrs in Bind_new.Bret l)
669    (translate_op globals BackEndOps.Add destrs
670      (List.map (fun x -> Joint.Reg x) destrs)
671      (Types.pi1 (one_args (List.length destrs))))
672
673(** val translate_notbool :
674    AST.ident List.list -> Registers.register List.list -> Registers.register
675    List.list -> (Registers.register, Joint.joint_seq List.list)
676    Bind_new.bind_new **)
677let translate_notbool globals destrs srcrs =
678  match destrs with
679  | List.Nil -> let l = List.Nil in Bind_new.Bret l
680  | List.Cons (destr, destrs') ->
681    BindLists.bappend
682      (let l = translate_fill_with_zero globals destrs' in Bind_new.Bret l)
683      (match srcrs with
684       | List.Nil ->
685         let l = List.Cons ((Joint.MOVE
686           (Obj.magic { Types.fst = destr; Types.snd =
687             (Joint.psd_argument_from_byte Joint.zero_byte) })), List.Nil)
688         in
689         Bind_new.Bret l
690       | List.Cons (srcr, srcrs') ->
691         BindLists.bappend
692           (BindLists.bcons (Joint.MOVE
693             (Obj.magic { Types.fst = destr; Types.snd =
694               (Joint.psd_argument_from_reg srcr) }))
695             (let l =
696                List.map (fun r -> Joint.OP2 (BackEndOps.Or,
697                  (Obj.magic destr),
698                  (Obj.magic (Joint.psd_argument_from_reg destr)),
699                  (Obj.magic (Joint.psd_argument_from_reg r)))) srcrs'
700              in
701             Bind_new.Bret l))
702           (BindLists.bcons Joint.CLEAR_CARRY (Bind_new.Bnew (fun tmp ->
703             let l = List.Cons ((Joint.MOVE
704               (Obj.magic { Types.fst = tmp; Types.snd =
705                 (Joint.psd_argument_from_byte Joint.zero_byte) })),
706               (List.Cons ((Joint.OP2 (BackEndOps.Sub, (Obj.magic destr),
707               (Obj.magic (Joint.psd_argument_from_reg tmp)),
708               (Obj.magic (Joint.psd_argument_from_reg tmp)))), (List.Cons
709               ((Joint.OP2 (BackEndOps.Addc, (Obj.magic destr),
710               (Obj.magic (Joint.psd_argument_from_reg tmp)),
711               (Obj.magic (Joint.psd_argument_from_reg tmp)))), List.Nil)))))
712             in
713             Bind_new.Bret l))))
714
715(** val translate_op1 :
716    AST.ident List.list -> AST.typ -> AST.typ -> FrontEndOps.unary_operation
717    -> Registers.register List.list -> Registers.register List.list ->
718    (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new **)
719let translate_op1 globals ty ty' op1 destrs srcrs =
720  (match op1 with
721   | FrontEndOps.Ocastint (x, src_sign, x0, x1) ->
722     (fun _ _ -> translate_cast globals src_sign destrs srcrs)
723   | FrontEndOps.Onegint (sz, sg) ->
724     (fun _ _ -> translate_negint globals destrs srcrs)
725   | FrontEndOps.Onotbool (x, x0, x1) ->
726     (fun _ _ -> translate_notbool globals destrs srcrs)
727   | FrontEndOps.Onotint (sz, sg) ->
728     (fun _ _ ->
729       let l = translate_notint globals destrs srcrs in Bind_new.Bret l)
730   | FrontEndOps.Oid t ->
731     (fun _ _ ->
732       let l =
733         translate_move globals destrs
734           (List.map (fun x -> Joint.Reg x) srcrs)
735       in
736       Bind_new.Bret l)
737   | FrontEndOps.Optrofint (sz, sg) ->
738     (fun _ _ -> translate_cast globals AST.Unsigned destrs srcrs)
739   | FrontEndOps.Ointofptr (sz, sg) ->
740     (fun _ _ -> translate_cast globals AST.Unsigned destrs srcrs)) __ __
741
742(** val translate_mul_i :
743    AST.ident List.list -> Registers.register -> Registers.register ->
744    Nat.nat -> Registers.register List.list -> Joint.psd_argument List.list
745    -> Joint.psd_argument List.list -> Nat.nat -> Nat.nat Types.sig0 ->
746    (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new ->
747    (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new **)
748let translate_mul_i globals a b n tmp_destrs_dummy srcrs1 srcrs2 k i_sig acc =
749  let i = i_sig in
750  let args =
751    List.append (List.Cons ((Joint.Reg a), (List.Cons ((Joint.Reg b),
752      List.Nil))))
753      (List.make_list
754        (let x = Joint.psd_argument_from_byte Joint.zero_byte in x)
755        (Nat.minus (Nat.minus n (Nat.S Nat.O)) k))
756  in
757  let tmp_destrs_view = List.ltl tmp_destrs_dummy k in
758  BindLists.bappend
759    (let l = List.Cons ((Joint.OPACCS (BackEndOps.Mul, (Obj.magic a),
760       (Obj.magic b), (Util.nth_safe i (Obj.magic srcrs1)),
761       (Util.nth_safe (Nat.minus k i) (Obj.magic srcrs2)))), List.Nil)
762     in
763    Bind_new.Bret l)
764    (BindLists.bappend
765      (translate_op globals BackEndOps.Add tmp_destrs_view
766        (List.map (fun x -> Joint.Reg x) tmp_destrs_view) args) acc)
767
768(** val translate_mul :
769    AST.ident List.list -> Registers.register List.list -> Joint.psd_argument
770    List.list -> Joint.psd_argument List.list -> (Registers.register,
771    Joint.joint_seq List.list) Bind_new.bind_new **)
772let translate_mul globals destrs srcrs1 srcrs2 =
773  Bind_new.Bnew (fun a -> Bind_new.Bnew (fun b ->
774    Bind_new.bnews_strong (List.length destrs) (fun tmp_destrs _ ->
775      Bind_new.Bnew (fun dummy ->
776      let translate_mul_k = fun k_sig acc ->
777        let k = k_sig in
778        List.foldr
779          (translate_mul_i globals a b (List.length destrs)
780            (List.append tmp_destrs (List.Cons (dummy, List.Nil))) srcrs1
781            srcrs2 k) acc (Lists.range_strong (Nat.S k))
782      in
783      BindLists.bappend
784        (let l = translate_fill_with_zero globals tmp_destrs in
785        Bind_new.Bret l)
786        (BindLists.bappend
787          (List.foldr translate_mul_k (let l = List.Nil in Bind_new.Bret l)
788            (Lists.range_strong (List.length destrs)))
789          (let l =
790             translate_move globals destrs
791               (List.map (fun x -> Joint.Reg x) tmp_destrs)
792           in
793          Bind_new.Bret l))))))
794
795(** val translate_divumodu8 :
796    AST.ident List.list -> Bool.bool -> Registers.register List.list ->
797    Joint.psd_argument List.list -> Joint.psd_argument List.list ->
798    (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new **)
799let translate_divumodu8 globals div_not_mod destrs srcrs1 srcrs2 =
800  (match destrs with
801   | List.Nil -> (fun _ -> let l = List.Nil in Bind_new.Bret l)
802   | List.Cons (destr, destrs') ->
803     (fun _ ->
804       match destrs' with
805       | List.Nil ->
806         (match srcrs1 with
807          | List.Nil -> (fun _ -> assert false (* absurd case *))
808          | List.Cons (srcr1, srcrs1') ->
809            (fun _ ->
810              (match srcrs2 with
811               | List.Nil -> (fun _ -> assert false (* absurd case *))
812               | List.Cons (srcr2, srcrs2') ->
813                 (fun _ -> Bind_new.Bnew (fun dummy ->
814                   let l =
815                     let { Types.fst = destr1; Types.snd = destr2 } =
816                       match div_not_mod with
817                       | Bool.True ->
818                         { Types.fst = destr; Types.snd = dummy }
819                       | Bool.False ->
820                         { Types.fst = dummy; Types.snd = destr }
821                     in
822                     List.Cons ((Joint.OPACCS (BackEndOps.DivuModu,
823                     (Obj.magic destr1), (Obj.magic destr2),
824                     (Obj.magic srcr1), (Obj.magic srcr2))), List.Nil)
825                   in
826                   Bind_new.Bret l))) __)) __
827       | List.Cons (x, x0) -> Logic.false_rect_Type0 __)) __
828
829(** val foldr2 :
830    ('a1 -> 'a2 -> 'a3 -> 'a3) -> 'a3 -> 'a1 List.list -> 'a2 List.list ->
831    'a3 **)
832let rec foldr2 f init l1 l2 =
833  (match l1 with
834   | List.Nil -> (fun _ -> init)
835   | List.Cons (a, l1') ->
836     (fun _ ->
837       (match l2 with
838        | List.Nil -> (fun _ -> assert false (* absurd case *))
839        | List.Cons (b, l2') -> (fun _ -> f a b (foldr2 f init l1' l2'))) __))
840    __
841
842(** val translate_ne :
843    AST.ident List.list -> Registers.register List.list -> Joint.psd_argument
844    List.list -> Joint.psd_argument List.list -> (Registers.register,
845    Joint.joint_seq List.list) Bind_new.bind_new **)
846let translate_ne globals destrs srcrs1 srcrs2 =
847  (match destrs with
848   | List.Nil -> (fun _ -> let l = List.Nil in Bind_new.Bret l)
849   | List.Cons (destr, destrs') ->
850     (fun _ ->
851       BindLists.bappend
852         (let l = translate_fill_with_zero globals destrs' in
853         Bind_new.Bret l)
854         ((match srcrs1 with
855           | List.Nil ->
856             (fun _ ->
857               let l = List.Cons ((Joint.MOVE
858                 (Obj.magic { Types.fst = destr; Types.snd =
859                   (Joint.psd_argument_from_byte Joint.zero_byte) })),
860                 List.Nil)
861               in
862               Bind_new.Bret l)
863           | List.Cons (srcr1, srcrs1') ->
864             (match srcrs2 with
865              | List.Nil -> (fun _ -> assert false (* absurd case *))
866              | List.Cons (srcr2, srcrs2') ->
867                (fun _ -> Bind_new.Bnew (fun tmpr ->
868                  let f = fun s1 s2 acc -> List.Cons ((Joint.OP2
869                    (BackEndOps.Xor, (Obj.magic tmpr), s1, s2)), (List.Cons
870                    ((Joint.OP2 (BackEndOps.Or, (Obj.magic destr),
871                    (Obj.magic (Joint.psd_argument_from_reg destr)),
872                    (Obj.magic (Joint.psd_argument_from_reg tmpr)))), acc)))
873                  in
874                  let epilogue = List.Cons (Joint.CLEAR_CARRY, (List.Cons
875                    ((Joint.OP2 (BackEndOps.Sub, (Obj.magic tmpr),
876                    (Obj.magic
877                      (Joint.psd_argument_from_byte Joint.zero_byte)),
878                    (Obj.magic (Joint.psd_argument_from_reg destr)))),
879                    (List.Cons ((Joint.OP2 (BackEndOps.Addc,
880                    (Obj.magic destr),
881                    (Obj.magic
882                      (Joint.psd_argument_from_byte Joint.zero_byte)),
883                    (Obj.magic
884                      (Joint.psd_argument_from_byte Joint.zero_byte)))),
885                    List.Nil)))))
886                  in
887                  let l = List.Cons ((Joint.OP2 (BackEndOps.Xor,
888                    (Obj.magic destr), (Obj.magic srcr1),
889                    (Obj.magic srcr2))),
890                    (foldr2 f epilogue (Obj.magic srcrs1')
891                      (Obj.magic srcrs2')))
892                  in
893                  Bind_new.Bret l)))) __))) __
894
895(** val translate_toggle_bool :
896    AST.ident List.list -> Registers.register List.list ->
897    (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new **)
898let translate_toggle_bool globals destrs =
899  (match destrs with
900   | List.Nil -> (fun _ -> let l = List.Nil in Bind_new.Bret l)
901   | List.Cons (destr, x) ->
902     (fun _ ->
903       let l = List.Cons ((Joint.OP1 (BackEndOps.Cmpl, (Obj.magic destr),
904         (Obj.magic destr))), List.Nil)
905       in
906       Bind_new.Bret l)) __
907
908(** val translate_lt_unsigned :
909    AST.ident List.list -> Registers.register List.list -> Joint.psd_argument
910    List.list -> Joint.psd_argument List.list -> (Registers.register,
911    Joint.joint_seq List.list) Bind_new.bind_new **)
912let translate_lt_unsigned globals destrs srcrs1 srcrs2 =
913  match destrs with
914  | List.Nil -> let l = List.Nil in Bind_new.Bret l
915  | List.Cons (destr, destrs') ->
916    Bind_new.Bnew (fun tmpr ->
917      BindLists.bappend
918        (let l = translate_fill_with_zero globals destrs' in Bind_new.Bret l)
919        (BindLists.bappend
920          (translate_op globals BackEndOps.Sub
921            (List.make_list tmpr (List.length srcrs1)) srcrs1 srcrs2)
922          (let l = List.Cons ((Joint.OP2 (BackEndOps.Addc, (Obj.magic destr),
923             (Obj.magic (Joint.psd_argument_from_byte Joint.zero_byte)),
924             (Obj.magic (Joint.psd_argument_from_byte Joint.zero_byte)))),
925             List.Nil)
926           in
927          Bind_new.Bret l)))
928
929(** val shift_signed :
930    AST.ident List.list -> Registers.register -> Joint.psd_argument List.list
931    -> (Joint.psd_argument List.list, Joint.joint_seq List.list) Types.prod
932    Types.sig0 **)
933let rec shift_signed globals tmp srcrs =
934  let byte_128 = Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
935    (Nat.S Nat.O))))))), Bool.True,
936    (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
937      Nat.O)))))))))
938  in
939  (match srcrs with
940   | List.Nil -> (fun _ -> { Types.fst = List.Nil; Types.snd = List.Nil })
941   | List.Cons (srcr, srcrs') ->
942     (fun _ ->
943       (match srcrs' with
944        | List.Nil ->
945          (fun _ -> { Types.fst = (List.Cons ((Joint.Reg tmp), List.Nil));
946            Types.snd = (List.Cons ((Joint.OP2 (BackEndOps.Add,
947            (Obj.magic tmp), (Obj.magic srcr),
948            (Obj.magic (Joint.psd_argument_from_byte byte_128)))),
949            List.Nil)) })
950        | List.Cons (x, x0) ->
951          (fun _ ->
952            let re = shift_signed globals tmp srcrs' in
953            { Types.fst = (List.Cons (srcr, (Types.pi1 re).Types.fst));
954            Types.snd = (Types.pi1 re).Types.snd })) __)) __
955
956(** val translate_lt_signed :
957    AST.ident List.list -> Registers.register List.list -> Joint.psd_argument
958    List.list -> Joint.psd_argument List.list -> (Registers.register,
959    Joint.joint_seq List.list) Bind_new.bind_new **)
960let translate_lt_signed globals destrs srcrs1 srcrs2 =
961  Bind_new.Bnew (fun tmp_last_s1 -> Bind_new.Bnew (fun tmp_last_s2 ->
962    let p1 = shift_signed globals tmp_last_s1 srcrs1 in
963    let new_srcrs1 = (Types.pi1 p1).Types.fst in
964    let shift_srcrs1 = (Types.pi1 p1).Types.snd in
965    let p2 = shift_signed globals tmp_last_s2 srcrs2 in
966    let new_srcrs2 = (Types.pi1 p2).Types.fst in
967    let shift_srcrs2 = (Types.pi1 p2).Types.snd in
968    BindLists.bappend (let l = shift_srcrs1 in Bind_new.Bret l)
969      (BindLists.bappend (let l = shift_srcrs2 in Bind_new.Bret l)
970        (translate_lt_unsigned globals destrs new_srcrs1 new_srcrs2))))
971
972(** val translate_lt :
973    Bool.bool -> AST.ident List.list -> Registers.register List.list ->
974    Joint.psd_argument List.list -> Joint.psd_argument List.list ->
975    (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new **)
976let translate_lt is_unsigned globals destrs srcrs1 srcrs2 =
977  match is_unsigned with
978  | Bool.True -> translate_lt_unsigned globals destrs srcrs1 srcrs2
979  | Bool.False -> translate_lt_signed globals destrs srcrs1 srcrs2
980
981(** val translate_cmp :
982    Bool.bool -> AST.ident List.list -> Integers.comparison ->
983    Registers.register List.list -> Joint.psd_argument List.list ->
984    Joint.psd_argument List.list -> (Registers.register, Joint.joint_seq)
985    BindLists.bind_list **)
986let translate_cmp is_unsigned globals cmp destrs srcrs1 srcrs2 =
987  match cmp with
988  | Integers.Ceq ->
989    BindLists.bappend (translate_ne globals destrs srcrs1 srcrs2)
990      (translate_toggle_bool globals destrs)
991  | Integers.Cne -> translate_ne globals destrs srcrs1 srcrs2
992  | Integers.Clt -> translate_lt is_unsigned globals destrs srcrs1 srcrs2
993  | Integers.Cle ->
994    BindLists.bappend (translate_lt is_unsigned globals destrs srcrs2 srcrs1)
995      (translate_toggle_bool globals destrs)
996  | Integers.Cgt -> translate_lt is_unsigned globals destrs srcrs2 srcrs1
997  | Integers.Cge ->
998    BindLists.bappend (translate_lt is_unsigned globals destrs srcrs1 srcrs2)
999      (translate_toggle_bool globals destrs)
1000
1001(** val translate_op2 :
1002    AST.ident List.list -> AST.typ -> AST.typ -> AST.typ ->
1003    FrontEndOps.binary_operation -> Registers.register List.list ->
1004    Joint.psd_argument List.list -> Joint.psd_argument List.list ->
1005    (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new **)
1006let translate_op2 globals ty1 ty2 ty3 op2 destrs srcrs1 srcrs2 =
1007  (match op2 with
1008   | FrontEndOps.Oadd (sz, sg) ->
1009     (fun _ _ _ -> translate_op globals BackEndOps.Add destrs srcrs1 srcrs2)
1010   | FrontEndOps.Osub (sz, sg) ->
1011     (fun _ _ _ -> translate_op globals BackEndOps.Sub destrs srcrs1 srcrs2)
1012   | FrontEndOps.Omul (sz, sg) ->
1013     (fun _ _ _ -> translate_mul globals destrs srcrs1 srcrs2)
1014   | FrontEndOps.Odiv x -> assert false (* absurd case *)
1015   | FrontEndOps.Odivu sz ->
1016     (fun _ _ _ ->
1017       translate_divumodu8 globals Bool.True destrs srcrs1 srcrs2)
1018   | FrontEndOps.Omod x -> assert false (* absurd case *)
1019   | FrontEndOps.Omodu sz ->
1020     (fun _ _ _ ->
1021       translate_divumodu8 globals Bool.False destrs srcrs1 srcrs2)
1022   | FrontEndOps.Oand (sz, sg) ->
1023     (fun _ _ _ -> translate_op globals BackEndOps.And destrs srcrs1 srcrs2)
1024   | FrontEndOps.Oor (sz, sg) ->
1025     (fun _ _ _ -> translate_op globals BackEndOps.Or destrs srcrs1 srcrs2)
1026   | FrontEndOps.Oxor (sz, sg) ->
1027     (fun _ _ _ -> translate_op globals BackEndOps.Xor destrs srcrs1 srcrs2)
1028   | FrontEndOps.Oshl (x, x0) -> assert false (* absurd case *)
1029   | FrontEndOps.Oshr (x, x0) -> assert false (* absurd case *)
1030   | FrontEndOps.Oshru (x, x0) -> assert false (* absurd case *)
1031   | FrontEndOps.Ocmp (sz, sg1, sg2, c) ->
1032     (fun _ _ _ -> translate_cmp Bool.False globals c destrs srcrs1 srcrs2)
1033   | FrontEndOps.Ocmpu (sz, sg, c) ->
1034     (fun _ _ _ -> translate_cmp Bool.True globals c destrs srcrs1 srcrs2)
1035   | FrontEndOps.Oaddpi sz ->
1036     (fun _ _ _ ->
1037       translate_op_asym_signed globals BackEndOps.Add destrs srcrs1 srcrs2)
1038   | FrontEndOps.Oaddip sz ->
1039     (fun _ _ _ ->
1040       translate_op_asym_signed globals BackEndOps.Add destrs srcrs2 srcrs1)
1041   | FrontEndOps.Osubpi sz ->
1042     (fun _ _ _ ->
1043       translate_op_asym_signed globals BackEndOps.Add destrs srcrs1 srcrs2)
1044   | FrontEndOps.Osubpp sz ->
1045     (fun _ _ _ ->
1046       translate_op_asym_unsigned globals BackEndOps.Sub destrs srcrs1 srcrs2)
1047   | FrontEndOps.Ocmpp (sg, c) ->
1048     (fun _ _ _ ->
1049       let is_Ocmpp = Nat.O in
1050       translate_cmp Bool.True globals c destrs srcrs1 srcrs2)) __ __ __
1051
1052(** val translate_cond :
1053    AST.ident List.list -> Registers.register List.list -> Graphs.label ->
1054    Blocks.bind_step_block **)
1055let translate_cond globals srcrs lbl_true =
1056  match srcrs with
1057  | List.Nil ->
1058    Bind_new.Bret
1059      (Blocks.ensure_step_block (Joint.graph_params_to_params RTL.rTL)
1060        globals List.Nil)
1061  | List.Cons (srcr, srcrs') ->
1062    Bind_new.Bnew (fun tmpr ->
1063      let f = fun r x -> Joint.OP2 (BackEndOps.Or, (Obj.magic tmpr),
1064        (Obj.magic (Joint.psd_argument_from_reg tmpr)),
1065        (Obj.magic (Joint.psd_argument_from_reg r)))
1066      in
1067      Bind_new.Bret { Types.fst = { Types.fst = (List.Cons ((fun x ->
1068      Joint.MOVE
1069      (Obj.magic { Types.fst = tmpr; Types.snd =
1070        (Joint.psd_argument_from_reg srcr) })), (List.map f srcrs')));
1071      Types.snd = (fun x -> Joint.COND ((Obj.magic tmpr), lbl_true)) };
1072      Types.snd = List.Nil })
1073
1074(** val translate_load :
1075    AST.ident List.list -> Joint.psd_argument List.list -> Registers.register
1076    List.list -> (Registers.register, Joint.joint_seq List.list)
1077    Bind_new.bind_new **)
1078let translate_load globals addr destrs =
1079  Bind_new.Bnew (fun tmp_addr_l -> Bind_new.Bnew (fun tmp_addr_h ->
1080    BindLists.bappend
1081      (let l =
1082         translate_move globals (List.Cons (tmp_addr_l, (List.Cons
1083           (tmp_addr_h, List.Nil)))) addr
1084       in
1085      Bind_new.Bret l)
1086      (let f = fun destr acc ->
1087         BindLists.bappend
1088           (let l = List.Cons ((Joint.LOAD (destr,
1089              (Obj.magic (Joint.Reg tmp_addr_l)),
1090              (Obj.magic (Joint.Reg tmp_addr_h)))), List.Nil)
1091            in
1092           Bind_new.Bret l)
1093           (BindLists.bappend
1094             (translate_op globals BackEndOps.Add (List.Cons (tmp_addr_l,
1095               (List.Cons (tmp_addr_h, List.Nil)))) (List.Cons
1096               ((Joint.psd_argument_from_reg tmp_addr_l), (List.Cons
1097               ((Joint.psd_argument_from_reg tmp_addr_h), List.Nil))))
1098               (List.Cons ((Joint.psd_argument_from_byte Joint.zero_byte),
1099               (List.Cons
1100               ((let x = I8051.int_size in Joint.psd_argument_from_byte x),
1101               List.Nil))))) acc)
1102       in
1103      List.foldr f (let l = List.Nil in Bind_new.Bret l) (Obj.magic destrs))))
1104
1105(** val translate_store :
1106    AST.ident List.list -> Joint.psd_argument List.list -> Joint.psd_argument
1107    List.list -> (Registers.register, Joint.joint_seq List.list)
1108    Bind_new.bind_new **)
1109let translate_store globals addr srcrs =
1110  Bind_new.Bnew (fun tmp_addr_l -> Bind_new.Bnew (fun tmp_addr_h ->
1111    BindLists.bappend
1112      (let l =
1113         translate_move globals (List.Cons (tmp_addr_l, (List.Cons
1114           (tmp_addr_h, List.Nil)))) addr
1115       in
1116      Bind_new.Bret l)
1117      (let f = fun srcr acc ->
1118         BindLists.bappend
1119           (let l = List.Cons ((Joint.STORE
1120              ((Obj.magic (Joint.Reg tmp_addr_l)),
1121              (Obj.magic (Joint.Reg tmp_addr_h)), srcr)), List.Nil)
1122            in
1123           Bind_new.Bret l)
1124           (BindLists.bappend
1125             (translate_op globals BackEndOps.Add (List.Cons (tmp_addr_l,
1126               (List.Cons (tmp_addr_h, List.Nil)))) (List.Cons
1127               ((Joint.psd_argument_from_reg tmp_addr_l), (List.Cons
1128               ((Joint.psd_argument_from_reg tmp_addr_h), List.Nil))))
1129               (List.Cons ((Joint.psd_argument_from_byte Joint.zero_byte),
1130               (List.Cons
1131               ((let x = I8051.int_size in Joint.psd_argument_from_byte x),
1132               List.Nil))))) acc)
1133       in
1134      List.foldr f (let l = List.Nil in Bind_new.Bret l) (Obj.magic srcrs))))
1135
1136(** val ensure_bind_step_block :
1137    Joint.params -> AST.ident List.list -> (Registers.register,
1138    Joint.joint_seq List.list) Bind_new.bind_new -> Blocks.bind_step_block **)
1139let ensure_bind_step_block p g b =
1140  Obj.magic
1141    (Monad.m_bind0 (Monad.max_def Bind_new.bindNew) (Obj.magic b) (fun l ->
1142      Obj.magic (Bind_new.Bret (Blocks.ensure_step_block p g l))))
1143
1144(** val translate_statement :
1145    AST.ident List.list -> (Registers.register, AST.typ) Types.prod List.list
1146    -> local_env -> RTLabs_syntax.statement -> ((Blocks.bind_step_block,
1147    Blocks.bind_fin_block) Types.sum, __) Types.dPair **)
1148let translate_statement globals locals lenv stmt =
1149  (match stmt with
1150   | RTLabs_syntax.St_skip lbl' ->
1151     (fun _ -> { Types.dpi1 = (Types.Inl (Bind_new.Bret
1152       (Blocks.ensure_step_block (Joint.graph_params_to_params RTL.rTL)
1153         globals List.Nil))); Types.dpi2 = (Obj.magic lbl') })
1154   | RTLabs_syntax.St_cost (cost_lbl, lbl') ->
1155     (fun _ -> { Types.dpi1 = (Types.Inl (Bind_new.Bret { Types.fst =
1156       { Types.fst = List.Nil; Types.snd = (fun x -> Joint.COST_LABEL
1157       cost_lbl) }; Types.snd = List.Nil })); Types.dpi2 =
1158       (Obj.magic lbl') })
1159   | RTLabs_syntax.St_const (ty, destr, cst, lbl') ->
1160     (fun _ -> { Types.dpi1 = (Types.Inl
1161       (ensure_bind_step_block (Joint.graph_params_to_params RTL.rTL) globals
1162         (translate_cst ty globals cst (find_local_env destr lenv))));
1163       Types.dpi2 = (Obj.magic lbl') })
1164   | RTLabs_syntax.St_op1 (ty, ty', op1, destr, srcr, lbl') ->
1165     (fun _ -> { Types.dpi1 = (Types.Inl
1166       (ensure_bind_step_block (Joint.graph_params_to_params RTL.rTL) globals
1167         (translate_op1 globals ty' ty op1 (find_local_env destr lenv)
1168           (find_local_env srcr lenv)))); Types.dpi2 = (Obj.magic lbl') })
1169   | RTLabs_syntax.St_op2 (ty1, ty2, ty3, op2, destr, srcr1, srcr2, lbl') ->
1170     (fun _ -> { Types.dpi1 = (Types.Inl
1171       (ensure_bind_step_block (Joint.graph_params_to_params RTL.rTL) globals
1172         (translate_op2 globals ty2 ty3 ty1 op2 (find_local_env destr lenv)
1173           (find_local_env_arg srcr1 lenv) (find_local_env_arg srcr2 lenv))));
1174       Types.dpi2 = (Obj.magic lbl') })
1175   | RTLabs_syntax.St_load (ignore, addr, destr, lbl') ->
1176     (fun _ -> { Types.dpi1 = (Types.Inl
1177       (ensure_bind_step_block (Joint.graph_params_to_params RTL.rTL) globals
1178         (translate_load globals (find_local_env_arg addr lenv)
1179           (find_local_env destr lenv)))); Types.dpi2 = (Obj.magic lbl') })
1180   | RTLabs_syntax.St_store (ignore, addr, srcr, lbl') ->
1181     (fun _ -> { Types.dpi1 = (Types.Inl
1182       (ensure_bind_step_block (Joint.graph_params_to_params RTL.rTL) globals
1183         (translate_store globals (find_local_env_arg addr lenv)
1184           (find_local_env_arg srcr lenv)))); Types.dpi2 =
1185       (Obj.magic lbl') })
1186   | RTLabs_syntax.St_call_id (f, args, retr, lbl') ->
1187     (fun _ -> { Types.dpi1 = (Types.Inl (Bind_new.Bret { Types.fst =
1188       { Types.fst = List.Nil; Types.snd = (fun x -> Joint.CALL ((Types.Inl
1189       f), (Obj.magic (rtl_args args lenv)),
1190       (match retr with
1191        | Types.None -> Obj.magic List.Nil
1192        | Types.Some retr0 -> Obj.magic (find_local_env retr0 lenv)))) };
1193       Types.snd = List.Nil })); Types.dpi2 = (Obj.magic lbl') })
1194   | RTLabs_syntax.St_call_ptr (f, args, retr, lbl') ->
1195     (fun _ ->
1196       let fs = find_and_addr_arg f lenv in
1197       { Types.dpi1 = (Types.Inl (Bind_new.Bret { Types.fst = { Types.fst =
1198       List.Nil; Types.snd = (fun x -> Joint.CALL ((Types.Inr
1199       (Obj.magic fs)), (Obj.magic (rtl_args args lenv)),
1200       (match retr with
1201        | Types.None -> Obj.magic List.Nil
1202        | Types.Some retr0 -> Obj.magic (find_local_env retr0 lenv)))) };
1203       Types.snd = List.Nil })); Types.dpi2 = (Obj.magic lbl') })
1204   | RTLabs_syntax.St_cond (r, lbl_true, lbl_false) ->
1205     (fun _ -> { Types.dpi1 = (Types.Inl
1206       (translate_cond globals (find_local_env r lenv) lbl_true));
1207       Types.dpi2 = (Obj.magic lbl_false) })
1208   | RTLabs_syntax.St_return ->
1209     (fun _ -> { Types.dpi1 = (Types.Inr (Bind_new.Bret { Types.fst =
1210       List.Nil; Types.snd = Joint.RETURN })); Types.dpi2 =
1211       (Obj.magic Types.It) })) __
1212
1213(** val translate_internal :
1214    AST.ident List.list -> RTLabs_syntax.internal_function ->
1215    Joint.joint_closed_internal_function **)
1216let translate_internal globals def =
1217  let runiverse' = def.RTLabs_syntax.f_reggen in
1218  let luniverse' = def.RTLabs_syntax.f_labgen in
1219  let stack_size' = def.RTLabs_syntax.f_stacksize in
1220  let entry' = Types.pi1 def.RTLabs_syntax.f_entry in
1221  let init = { Joint.joint_if_luniverse = luniverse';
1222    Joint.joint_if_runiverse = runiverse'; Joint.joint_if_result =
1223    (Obj.magic List.Nil); Joint.joint_if_params = (Obj.magic List.Nil);
1224    Joint.joint_if_stacksize = stack_size'; Joint.joint_if_local_stacksize =
1225    stack_size'; Joint.joint_if_code =
1226    (Obj.magic
1227      (Identifiers.add PreIdentifiers.LabelTag
1228        (Identifiers.empty_map PreIdentifiers.LabelTag) entry' (Joint.Final
1229        Joint.RETURN))); Joint.joint_if_entry = (Obj.magic entry') }
1230  in
1231  (let { Types.fst = init'; Types.snd = lenv } =
1232     Obj.magic initialize_locals_params_ret globals
1233       def.RTLabs_syntax.f_locals def.RTLabs_syntax.f_params
1234       def.RTLabs_syntax.f_result init
1235   in
1236  (fun _ ->
1237  let vars =
1238    List.append def.RTLabs_syntax.f_locals
1239      (List.append def.RTLabs_syntax.f_params
1240        (match def.RTLabs_syntax.f_result with
1241         | Types.None -> List.Nil
1242         | Types.Some x -> List.Cons (x, List.Nil)))
1243  in
1244  let f_trans = fun lbl stmt def0 ->
1245    let pr = translate_statement globals vars lenv stmt in
1246    (match pr.Types.dpi1 with
1247     | Types.Inl instrs ->
1248       (fun lbl' ->
1249         TranslateUtils.b_adds_graph RTL.rTL globals instrs lbl
1250           (Obj.magic lbl') def0)
1251     | Types.Inr instrs ->
1252       (fun x ->
1253         TranslateUtils.b_fin_adds_graph RTL.rTL globals instrs lbl def0))
1254      pr.Types.dpi2
1255  in
1256  Identifiers.foldi PreIdentifiers.LabelTag f_trans def.RTLabs_syntax.f_graph
1257    init')) __
1258
1259(** val rtlabs_to_rtl : RTLabs_syntax.rTLabs_program -> RTL.rtl_program **)
1260let rtlabs_to_rtl p =
1261  AST.transform_program p (fun varnames ->
1262    AST.transf_fundef (translate_internal varnames))
1263
Note: See TracBrowser for help on using the repository browser.