source: extracted/rTLabsToRTL.ml @ 2951

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

New extraction. Novely: a pre-main is used in the back-end. Initialization
of global data is performed in LINToASM.

Note: the cost-emission of the initialization costlabel in the front-end is
virtual, but not performed in the traces I generate and print. To be fixed
(how?)

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