source: extracted/rTLabsToRTL.ml @ 3006

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

New extraction, bugs fixed.

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