source: extracted/rTLabsToRTL.ml @ 2817

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

Extracted again after James's cleanup and the implementation of the
new testing function to be used in the untrusted code.

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