97 open Hints_declaration
139 (** val size_of_sig_type : AST.typ -> Nat.nat **)
140 let size_of_sig_type = function
141 | AST.ASTint (isize, sign) ->
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)
148 (** val sign_of_sig_type : AST.typ -> AST.signedness **)
149 let sign_of_sig_type = function
150 | AST.ASTint (x, sign) -> sign
151 | AST.ASTptr -> AST.Unsigned
154 | Register_int of Registers.register
155 | Register_ptr of Registers.register * Registers.register
157 (** val register_type_rect_Type4 :
158 (Registers.register -> 'a1) -> (Registers.register -> Registers.register
159 -> 'a1) -> register_type -> 'a1 **)
160 let rec register_type_rect_Type4 h_register_int h_register_ptr = function
161 | Register_int x_18380 -> h_register_int x_18380
162 | Register_ptr (x_18382, x_18381) -> h_register_ptr x_18382 x_18381
164 (** val register_type_rect_Type5 :
165 (Registers.register -> 'a1) -> (Registers.register -> Registers.register
166 -> 'a1) -> register_type -> 'a1 **)
167 let rec register_type_rect_Type5 h_register_int h_register_ptr = function
168 | Register_int x_18386 -> h_register_int x_18386
169 | Register_ptr (x_18388, x_18387) -> h_register_ptr x_18388 x_18387
171 (** val register_type_rect_Type3 :
172 (Registers.register -> 'a1) -> (Registers.register -> Registers.register
173 -> 'a1) -> register_type -> 'a1 **)
174 let rec register_type_rect_Type3 h_register_int h_register_ptr = function
175 | Register_int x_18392 -> h_register_int x_18392
176 | Register_ptr (x_18394, x_18393) -> h_register_ptr x_18394 x_18393
178 (** val register_type_rect_Type2 :
179 (Registers.register -> 'a1) -> (Registers.register -> Registers.register
180 -> 'a1) -> register_type -> 'a1 **)
181 let rec register_type_rect_Type2 h_register_int h_register_ptr = function
182 | Register_int x_18398 -> h_register_int x_18398
183 | Register_ptr (x_18400, x_18399) -> h_register_ptr x_18400 x_18399
185 (** val register_type_rect_Type1 :
186 (Registers.register -> 'a1) -> (Registers.register -> Registers.register
187 -> 'a1) -> register_type -> 'a1 **)
188 let rec register_type_rect_Type1 h_register_int h_register_ptr = function
189 | Register_int x_18404 -> h_register_int x_18404
190 | Register_ptr (x_18406, x_18405) -> h_register_ptr x_18406 x_18405
192 (** val register_type_rect_Type0 :
193 (Registers.register -> 'a1) -> (Registers.register -> Registers.register
194 -> 'a1) -> register_type -> 'a1 **)
195 let rec register_type_rect_Type0 h_register_int h_register_ptr = function
196 | Register_int x_18410 -> h_register_int x_18410
197 | Register_ptr (x_18412, x_18411) -> h_register_ptr x_18412 x_18411
199 (** val register_type_inv_rect_Type4 :
200 register_type -> (Registers.register -> __ -> 'a1) -> (Registers.register
201 -> Registers.register -> __ -> 'a1) -> 'a1 **)
202 let register_type_inv_rect_Type4 hterm h1 h2 =
203 let hcut = register_type_rect_Type4 h1 h2 hterm in hcut __
205 (** val register_type_inv_rect_Type3 :
206 register_type -> (Registers.register -> __ -> 'a1) -> (Registers.register
207 -> Registers.register -> __ -> 'a1) -> 'a1 **)
208 let register_type_inv_rect_Type3 hterm h1 h2 =
209 let hcut = register_type_rect_Type3 h1 h2 hterm in hcut __
211 (** val register_type_inv_rect_Type2 :
212 register_type -> (Registers.register -> __ -> 'a1) -> (Registers.register
213 -> Registers.register -> __ -> 'a1) -> 'a1 **)
214 let register_type_inv_rect_Type2 hterm h1 h2 =
215 let hcut = register_type_rect_Type2 h1 h2 hterm in hcut __
217 (** val register_type_inv_rect_Type1 :
218 register_type -> (Registers.register -> __ -> 'a1) -> (Registers.register
219 -> Registers.register -> __ -> 'a1) -> 'a1 **)
220 let register_type_inv_rect_Type1 hterm h1 h2 =
221 let hcut = register_type_rect_Type1 h1 h2 hterm in hcut __
223 (** val register_type_inv_rect_Type0 :
224 register_type -> (Registers.register -> __ -> 'a1) -> (Registers.register
225 -> Registers.register -> __ -> 'a1) -> 'a1 **)
226 let register_type_inv_rect_Type0 hterm h1 h2 =
227 let hcut = register_type_rect_Type0 h1 h2 hterm in hcut __
229 (** val register_type_discr : register_type -> register_type -> __ **)
230 let register_type_discr x y =
231 Logic.eq_rect_Type2 x
233 | Register_int a0 -> Obj.magic (fun _ dH -> dH __)
234 | Register_ptr (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
236 (** val register_type_jmdiscr : register_type -> register_type -> __ **)
237 let register_type_jmdiscr x y =
238 Logic.eq_rect_Type2 x
240 | Register_int a0 -> Obj.magic (fun _ dH -> dH __)
241 | Register_ptr (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
243 type local_env = Registers.register List.list Identifiers.identifier_map
245 (** val find_local_env :
246 PreIdentifiers.identifier -> local_env -> Registers.register List.list **)
247 let find_local_env r lenv =
248 Option.opt_safe (Identifiers.lookup PreIdentifiers.RegisterTag lenv r)
250 (** val find_local_env_arg :
251 Registers.register -> local_env -> Joint.psd_argument List.list **)
252 let find_local_env_arg r lenv =
253 List.map (fun x -> Joint.Reg x) (find_local_env r lenv)
255 (** val m_iter : Monad.monad -> ('a1 -> __) -> Nat.nat -> __ -> __ **)
256 let rec m_iter m f n m0 =
259 | Nat.S k -> Monad.m_bind0 m m0 (fun v -> m_iter m f k (f v))
261 (** val fresh_registers :
262 Joint.params -> AST.ident List.list -> Nat.nat -> Registers.register
263 List.list Monad.smax_def__o__monad **)
264 let fresh_registers p g n =
266 Monad.m_bind0 (Monad.smax_def State.state_monad)
267 (TranslateUtils.fresh_register p g) (fun m ->
268 Monad.m_return0 (Monad.smax_def State.state_monad) (List.Cons (m, acc)))
270 m_iter (Monad.smax_def State.state_monad) f n
271 (Monad.m_return0 (Monad.smax_def State.state_monad) List.Nil)
273 (** val map_list_local_env :
274 Registers.register List.list Identifiers.identifier_map ->
275 (Registers.register, AST.typ) Types.prod List.list -> Registers.register
277 let rec map_list_local_env lenv regs =
279 | List.Nil -> (fun _ -> List.Nil)
280 | List.Cons (hd, tl) ->
282 List.append (find_local_env hd.Types.fst lenv)
283 (map_list_local_env lenv tl))) __
285 (** val initialize_local_env :
286 AST.ident List.list -> (Registers.register, AST.typ) Types.prod List.list
287 -> local_env Monad.smax_def__o__monad **)
288 let initialize_local_env globals registers =
289 let f = fun r_sig lenv ->
290 let { Types.fst = r; Types.snd = sig0 } = r_sig in
291 let size = size_of_sig_type sig0 in
292 Monad.m_bind0 (Monad.smax_def State.state_monad)
293 (fresh_registers (Joint.graph_params_to_params RTL.rTL) globals size)
295 Monad.m_return0 (Monad.smax_def State.state_monad)
296 (Identifiers.add PreIdentifiers.RegisterTag lenv r regs))
298 Monad.m_fold (Monad.smax_def State.state_monad) f registers
299 (Identifiers.empty_map PreIdentifiers.RegisterTag)
301 (** val initialize_locals_params_ret :
302 AST.ident List.list -> (Registers.register, AST.typ) Types.prod List.list
303 -> (Registers.register, AST.typ) Types.prod List.list ->
304 (Registers.register, AST.typ) Types.prod Types.option -> local_env
305 Monad.smax_def__o__monad **)
306 let initialize_locals_params_ret globals locals params ret =
307 Obj.magic (fun def ->
308 (let { Types.fst = def'; Types.snd = lenv } =
309 Obj.magic initialize_local_env globals
312 | Types.None -> List.Nil
313 | Types.Some r_sig -> List.Cons (r_sig, List.Nil))
314 (List.append locals params)) def
317 let params' = map_list_local_env lenv params in
320 | Types.None -> (fun _ -> List.Nil)
321 | Types.Some r_sig -> (fun _ -> find_local_env r_sig.Types.fst lenv))
324 let def'' = { Joint.joint_if_luniverse = def'.Joint.joint_if_luniverse;
325 Joint.joint_if_runiverse = def'.Joint.joint_if_runiverse;
326 Joint.joint_if_result = (Obj.magic ret'); Joint.joint_if_params =
327 (Obj.magic params'); Joint.joint_if_stacksize =
328 def'.Joint.joint_if_stacksize; Joint.joint_if_local_stacksize =
329 def'.Joint.joint_if_local_stacksize; Joint.joint_if_code =
330 def'.Joint.joint_if_code; Joint.joint_if_entry =
331 def'.Joint.joint_if_entry }
333 { Types.fst = def''; Types.snd = lenv })) __)
335 (** val make_addr : 'a1 List.list -> ('a1, 'a1) Types.prod **)
337 { Types.fst = (Util.nth_safe Nat.O lst); Types.snd =
338 (Util.nth_safe (Nat.S Nat.O) lst) }
340 (** val find_and_addr :
341 PreIdentifiers.identifier -> local_env -> (Registers.register,
342 Registers.register) Types.prod **)
343 let find_and_addr r lenv =
344 make_addr (find_local_env r lenv)
346 (** val find_and_addr_arg :
347 Registers.register -> local_env -> (Joint.psd_argument,
348 Joint.psd_argument) Types.prod **)
349 let find_and_addr_arg r lenv =
350 make_addr (find_local_env_arg r lenv)
353 Registers.register List.list -> local_env -> Joint.psd_argument List.list **)
354 let rec rtl_args args env =
356 | List.Nil -> (fun _ -> List.Nil)
357 | List.Cons (hd, tl) ->
358 (fun _ -> List.append (find_local_env_arg hd env) (rtl_args tl env))) __
361 Nat.nat -> Nat.nat -> 'a1 Vector.vector -> 'a1 Vector.vector List.list
363 let rec vrsplit m n =
365 | Nat.O -> (fun v -> List.Nil)
368 let spl = Vector.vsplit n (Nat.times k n) v in
369 List.Cons (spl.Types.fst, (Types.pi1 (vrsplit k n spl.Types.snd))))
371 (** val split_into_bytes :
372 AST.intsize -> AST.bvint -> BitVector.byte List.list Types.sig0 **)
373 let split_into_bytes size int =
376 (vrsplit (AST.size_intsize size) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
377 (Nat.S (Nat.S (Nat.S Nat.O)))))))) int))
379 (** val list_inject_All_aux : 'a1 List.list -> 'a1 Types.sig0 List.list **)
380 let rec list_inject_All_aux l =
382 | List.Nil -> (fun _ -> List.Nil)
383 | List.Cons (hd, tl) ->
384 (fun _ -> List.Cons (hd, (list_inject_All_aux tl)))) __
386 (** val translate_op_aux :
387 AST.ident List.list -> BackEndOps.op2 -> Registers.register List.list ->
388 Joint.psd_argument List.list -> Joint.psd_argument List.list ->
389 Joint.joint_seq List.list **)
390 let translate_op_aux globals op destrs srcrs1 srcrs2 =
391 Util.map3 (fun x x0 x1 -> Joint.OP2 (op, x, x0, x1)) (Obj.magic destrs)
392 (Obj.magic srcrs1) (Obj.magic srcrs2)
394 (** val translate_op :
395 AST.ident List.list -> BackEndOps.op2 -> Registers.register List.list ->
396 Joint.psd_argument List.list -> Joint.psd_argument List.list ->
397 Joint.joint_seq List.list **)
398 let translate_op globals op destrs srcrs1 srcrs2 =
402 | List.Nil -> (fun _ _ -> List.Nil)
403 | List.Cons (destr, destrs') ->
405 | List.Nil -> (fun _ -> assert false (* absurd case *))
406 | List.Cons (srcr1, srcrs1') ->
409 | List.Nil -> (fun _ -> assert false (* absurd case *))
410 | List.Cons (srcr2, srcrs2') ->
411 (fun _ -> List.Cons ((Joint.OP2 (BackEndOps.Add,
412 (Obj.magic destr), (Obj.magic srcr1), (Obj.magic srcr2))),
413 (translate_op_aux globals BackEndOps.Addc destrs' srcrs1'
417 List.append (List.Cons (Joint.CLEAR_CARRY, List.Nil))
418 (translate_op_aux globals BackEndOps.Addc destrs srcrs1 srcrs2))
421 List.append (List.Cons (Joint.CLEAR_CARRY, List.Nil))
422 (translate_op_aux globals BackEndOps.Sub destrs srcrs1 srcrs2))
424 (fun _ _ -> translate_op_aux globals op destrs srcrs1 srcrs2)
426 (fun _ _ -> translate_op_aux globals op destrs srcrs1 srcrs2)
428 (fun _ _ -> translate_op_aux globals op destrs srcrs1 srcrs2)) __ __
430 (** val cast_list : 'a1 -> Nat.nat -> 'a1 List.list -> 'a1 List.list **)
431 let cast_list deflt new_length l =
432 match Nat.leb (List.length l) new_length with
435 (List.make_list deflt (Nat.minus new_length (List.length l)))
436 | Bool.False -> List.lhd l new_length
438 (** val translate_op_asym_unsigned :
439 AST.ident List.list -> BackEndOps.op2 -> Registers.register List.list ->
440 Joint.psd_argument List.list -> Joint.psd_argument List.list ->
441 Joint.joint_seq List.list **)
442 let translate_op_asym_unsigned globals op destrs srcrs1 srcrs2 =
443 let l = List.length destrs in
445 cast_list (let x = Joint.psd_argument_from_byte Joint.zero_byte in x) l
449 cast_list (let x = Joint.psd_argument_from_byte Joint.zero_byte in x) l
452 translate_op globals op destrs srcrs1' srcrs2'
454 (** val zero_args : Nat.nat -> Joint.psd_argument List.list Types.sig0 **)
456 List.make_list (Joint.psd_argument_from_byte Joint.zero_byte) size
458 (** val one_args : Nat.nat -> Joint.psd_argument List.list Types.sig0 **)
459 let one_args = function
463 ((let x = Joint.psd_argument_from_byte (Joint.byte_of_nat (Nat.S Nat.O))
465 x), (Types.pi1 (zero_args k)))
467 (** val size_of_cst : AST.typ -> FrontEndOps.constant -> Nat.nat **)
468 let size_of_cst typ = function
469 | FrontEndOps.Ointconst (size, x, x0) -> AST.size_intsize size
470 | FrontEndOps.Oaddrsymbol (x, x0) -> Nat.S (Nat.S Nat.O)
471 | FrontEndOps.Oaddrstack x -> Nat.S (Nat.S Nat.O)
473 (** val translate_cst :
474 AST.typ -> AST.ident List.list -> FrontEndOps.constant Types.sig0 ->
475 Registers.register List.list -> (Registers.register, Joint.joint_seq
476 List.list) Bind_new.bind_new **)
477 let translate_cst ty globals cst_sig destrs =
479 (match Types.pi1 cst_sig with
480 | FrontEndOps.Ointconst (size, sign, const) ->
482 Util.map2 (fun r b -> Joint.MOVE
483 (Obj.magic { Types.fst = r; Types.snd =
484 (Joint.psd_argument_from_byte b) })) destrs
485 (Types.pi1 (split_into_bytes size const)))
486 | FrontEndOps.Oaddrsymbol (id, offset) ->
488 let { Types.fst = r1; Types.snd = r2 } = make_addr destrs in
490 Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
491 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
492 (Nat.S (Nat.S Nat.O)))))))))))))))) offset
494 List.Cons ((Joint.ADDRESS (id, off, (Obj.magic r1),
495 (Obj.magic r2))), List.Nil))
496 | FrontEndOps.Oaddrstack offset ->
498 let { Types.fst = r1; Types.snd = r2 } = make_addr destrs in
500 ((let x = Joint.Extension_seq
501 (Obj.magic (RTL.Rtl_stack_address (r1, r2)))
504 (match Nat.eqb offset Nat.O with
505 | Bool.True -> List.Nil
507 translate_op globals BackEndOps.Add (List.Cons (r1, (List.Cons
508 (r2, List.Nil)))) (List.Cons ((Joint.psd_argument_from_reg r1),
509 (List.Cons ((Joint.psd_argument_from_reg r2), List.Nil))))
511 ((Joint.psd_argument_from_byte (Joint.byte_of_nat offset)),
512 (List.Cons ((Joint.psd_argument_from_byte Joint.zero_byte),
513 List.Nil)))))))) __ __
517 (** val translate_move :
518 AST.ident List.list -> Registers.register List.list -> Joint.psd_argument
519 List.list -> Joint.joint_seq List.list **)
520 let translate_move globals destrs srcrs =
521 Util.map2 (fun dst src -> Joint.MOVE
522 (Obj.magic { Types.fst = dst; Types.snd = src })) destrs srcrs
525 AST.ident List.list -> Registers.register -> Joint.psd_argument ->
526 Joint.joint_seq List.list **)
527 let sign_mask globals destr = function
529 let byte_127 = Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
530 (Nat.S Nat.O))))))), Bool.False,
531 (BitVector.maximum (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
534 List.Cons ((Joint.OP2 (BackEndOps.Or, (Obj.magic destr),
535 (Obj.magic (Joint.psd_argument_from_reg srcr)),
536 (Obj.magic (Joint.psd_argument_from_byte byte_127)))), (List.Cons
537 ((Joint.OP1 (BackEndOps.Rl, (Obj.magic destr), (Obj.magic destr))),
538 (List.Cons ((Joint.OP1 (BackEndOps.Inc, (Obj.magic destr),
539 (Obj.magic destr))), (List.Cons ((Joint.OP1 (BackEndOps.Cmpl,
540 (Obj.magic destr), (Obj.magic destr))), List.Nil)))))))
542 (match Arithmetic.sign_bit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
543 (Nat.S Nat.O)))))))) b with
545 List.Cons ((Joint.MOVE
546 (Obj.magic { Types.fst = destr; Types.snd =
548 BitVector.maximum (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
549 (Nat.S (Nat.S Nat.O))))))))
551 Joint.psd_argument_from_byte x) })), List.Nil)
553 List.Cons ((Joint.MOVE
554 (Obj.magic { Types.fst = destr; Types.snd =
555 (Joint.psd_argument_from_byte Joint.zero_byte) })), List.Nil))
557 (** val translate_cast_signed :
558 AST.ident List.list -> Registers.register List.list -> Joint.psd_argument
559 -> (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new **)
560 let translate_cast_signed globals destrs srca =
561 Bind_new.Bnew (fun tmp ->
563 List.append (sign_mask globals tmp srca)
564 (translate_move globals destrs
565 (List.make_list (Joint.Reg tmp) (List.length destrs)))
569 (** val translate_fill_with_zero :
570 AST.ident List.list -> Registers.register List.list -> Joint.joint_seq
572 let translate_fill_with_zero globals destrs =
573 translate_move globals destrs (Types.pi1 (zero_args (List.length destrs)))
575 (** val last : 'a1 List.list -> 'a1 Types.option **)
576 let rec last = function
577 | List.Nil -> Types.None
578 | List.Cons (hd, tl) ->
580 | List.Nil -> Types.Some hd
581 | List.Cons (x, x0) -> last tl)
583 (** val translate_op_asym_signed :
584 AST.ident List.list -> BackEndOps.op2 -> Registers.register List.list ->
585 Joint.psd_argument List.list -> Joint.psd_argument List.list ->
586 (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new **)
587 let translate_op_asym_signed globals op destrs srcrs1 srcrs2 =
588 Bind_new.Bnew (fun tmp1 -> Bind_new.Bnew (fun tmp2 ->
589 let l = List.length destrs in
590 let cast_srcrs = fun srcrs tmp ->
591 let srcrs_l = List.length srcrs in
592 (match Nat.leb (Nat.S srcrs_l) l with
594 (match last srcrs with
598 (let x = Joint.psd_argument_from_byte Joint.zero_byte in x)
599 l); Types.snd = List.Nil }
600 | Types.Some last0 ->
603 (List.make_list (Joint.Reg tmp) (Nat.minus l srcrs_l)));
604 Types.snd = (sign_mask globals tmp last0) })
606 { Types.fst = (List.lhd srcrs l); Types.snd = List.Nil })
608 let srcrs1init = cast_srcrs srcrs1 tmp1 in
609 let srcrs2init = cast_srcrs srcrs2 tmp2 in
610 BindLists.bappend (let l0 = srcrs1init.Types.snd in Bind_new.Bret l0)
611 (BindLists.bappend (let l0 = srcrs2init.Types.snd in Bind_new.Bret l0)
613 translate_op globals op destrs srcrs1init.Types.fst
618 (** val translate_cast :
619 AST.ident List.list -> AST.signedness -> Registers.register List.list ->
620 Registers.register List.list -> (Registers.register, Joint.joint_seq
621 List.list) Bind_new.bind_new **)
622 let translate_cast globals src_sign destrs srcrs =
623 let t = Util.reduce_strong srcrs destrs in
624 let src_common = t.Types.fst.Types.fst in
625 let src_rest = t.Types.fst.Types.snd in
626 let dst_common = t.Types.snd.Types.fst in
627 let dst_rest = t.Types.snd.Types.snd in
630 translate_move globals dst_common
631 (List.map (fun x -> Joint.Reg x) src_common)
638 (match last srcrs with
640 let l = translate_fill_with_zero globals dst_rest in
642 | Types.Some src_last ->
643 translate_cast_signed globals dst_rest
644 (Joint.psd_argument_from_reg src_last))
646 let l = translate_fill_with_zero globals dst_rest in
648 | List.Cons (x, x0) -> let l = List.Nil in Bind_new.Bret l)
650 (** val translate_notint :
651 AST.ident List.list -> Registers.register List.list -> Registers.register
652 List.list -> Joint.joint_seq List.list **)
653 let translate_notint globals destrs srcrs =
654 Util.map2 (fun x x0 -> Joint.OP1 (BackEndOps.Cmpl, x, x0))
655 (Obj.magic destrs) (Obj.magic srcrs)
657 (** val translate_negint :
658 AST.ident List.list -> Registers.register List.list -> Registers.register
659 List.list -> Joint.joint_seq List.list **)
660 let translate_negint globals destrs srcrs =
661 List.append (translate_notint globals destrs srcrs)
662 (translate_op globals BackEndOps.Add destrs
663 (List.map (fun x -> Joint.Reg x) destrs)
664 (Types.pi1 (one_args (List.length destrs))))
666 (** val translate_notbool :
667 AST.ident List.list -> Registers.register List.list -> Registers.register
668 List.list -> (Registers.register, Joint.joint_seq List.list)
669 Bind_new.bind_new **)
670 let translate_notbool globals destrs srcrs =
672 | List.Nil -> let l = List.Nil in Bind_new.Bret l
673 | List.Cons (destr, destrs') ->
675 (let l = translate_fill_with_zero globals destrs' in Bind_new.Bret l)
678 let l = List.Cons ((Joint.MOVE
679 (Obj.magic { Types.fst = destr; Types.snd =
680 (Joint.psd_argument_from_byte Joint.zero_byte) })), List.Nil)
683 | List.Cons (srcr, srcrs') ->
685 (BindLists.bcons (Joint.MOVE
686 (Obj.magic { Types.fst = destr; Types.snd =
687 (Joint.psd_argument_from_reg srcr) }))
689 List.map (fun r -> Joint.OP2 (BackEndOps.Or,
691 (Obj.magic (Joint.psd_argument_from_reg destr)),
692 (Obj.magic (Joint.psd_argument_from_reg r)))) srcrs'
695 (BindLists.bcons Joint.CLEAR_CARRY (Bind_new.Bnew (fun tmp ->
696 let l = List.Cons ((Joint.MOVE
697 (Obj.magic { Types.fst = tmp; Types.snd =
698 (Joint.psd_argument_from_byte Joint.zero_byte) })),
699 (List.Cons ((Joint.OP2 (BackEndOps.Sub, (Obj.magic destr),
700 (Obj.magic (Joint.psd_argument_from_reg tmp)),
701 (Obj.magic (Joint.psd_argument_from_reg tmp)))), (List.Cons
702 ((Joint.OP2 (BackEndOps.Addc, (Obj.magic destr),
703 (Obj.magic (Joint.psd_argument_from_reg tmp)),
704 (Obj.magic (Joint.psd_argument_from_reg tmp)))), List.Nil)))))
708 (** val translate_op1 :
709 AST.ident List.list -> AST.typ -> AST.typ -> FrontEndOps.unary_operation
710 -> Registers.register List.list -> Registers.register List.list ->
711 (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new **)
712 let translate_op1 globals ty ty' op1 destrs srcrs =
714 | FrontEndOps.Ocastint (x, src_sign, x0, x1) ->
715 (fun _ _ -> translate_cast globals src_sign destrs srcrs)
716 | FrontEndOps.Onegint (sz, sg) ->
718 let l = translate_negint globals destrs srcrs in Bind_new.Bret l)
719 | FrontEndOps.Onotbool (x, x0, x1) ->
720 (fun _ _ -> translate_notbool globals destrs srcrs)
721 | FrontEndOps.Onotint (sz, sg) ->
723 let l = translate_notint globals destrs srcrs in Bind_new.Bret l)
724 | FrontEndOps.Oid t ->
727 translate_move globals destrs
728 (List.map (fun x -> Joint.Reg x) srcrs)
731 | FrontEndOps.Optrofint (sz, sg) ->
732 (fun _ _ -> translate_cast globals AST.Unsigned destrs srcrs)
733 | FrontEndOps.Ointofptr (sz, sg) ->
734 (fun _ _ -> translate_cast globals AST.Unsigned destrs srcrs)) __ __
736 (** val translate_mul_i :
737 AST.ident List.list -> Registers.register -> Registers.register ->
738 Nat.nat -> Registers.register List.list -> Joint.psd_argument List.list
739 -> Joint.psd_argument List.list -> Nat.nat -> Nat.nat Types.sig0 ->
740 Joint.joint_seq List.list -> Joint.joint_seq List.list **)
741 let translate_mul_i globals a b n tmp_destrs_dummy srcrs1 srcrs2 k i_sig acc =
744 List.append (List.Cons ((Joint.Reg a), (List.Cons ((Joint.Reg b),
747 (let x = Joint.psd_argument_from_byte Joint.zero_byte in x)
748 (Nat.minus (Nat.minus n (Nat.S Nat.O)) k))
750 let tmp_destrs_view = List.ltl tmp_destrs_dummy k in
751 List.append (List.Cons ((Joint.OPACCS (BackEndOps.Mul, (Obj.magic a),
752 (Obj.magic b), (Util.nth_safe i (Obj.magic srcrs1)),
753 (Util.nth_safe (Nat.minus k i) (Obj.magic srcrs2)))), List.Nil))
755 (translate_op globals BackEndOps.Add tmp_destrs_view
756 (List.map (fun x -> Joint.Reg x) tmp_destrs_view) args) acc)
758 (** val translate_mul :
759 AST.ident List.list -> Registers.register List.list -> Joint.psd_argument
760 List.list -> Joint.psd_argument List.list -> (Registers.register,
761 Joint.joint_seq List.list) Bind_new.bind_new **)
762 let translate_mul globals destrs srcrs1 srcrs2 =
763 Bind_new.Bnew (fun a -> Bind_new.Bnew (fun b ->
764 Bind_new.bnews_strong (List.length destrs) (fun tmp_destrs _ ->
765 Bind_new.Bnew (fun dummy ->
766 BindLists.bcons (Joint.MOVE
767 (Obj.magic { Types.fst = dummy; Types.snd =
768 (Joint.psd_argument_from_byte (Joint.byte_of_nat Nat.O)) }))
769 (let translate_mul_k = fun k_sig acc ->
772 (translate_mul_i globals a b (List.length destrs)
773 (List.append tmp_destrs (List.Cons (dummy, List.Nil))) srcrs1
774 srcrs2 k) acc (Lists.range_strong (Nat.S k))
777 List.append (translate_fill_with_zero globals tmp_destrs)
779 (List.foldr translate_mul_k List.Nil
780 (Lists.range_strong (List.length destrs)))
781 (translate_move globals destrs
782 (List.map (fun x -> Joint.Reg x) tmp_destrs)))
786 (** val translate_divumodu8 :
787 AST.ident List.list -> Bool.bool -> Registers.register List.list ->
788 Joint.psd_argument List.list -> Joint.psd_argument List.list ->
789 (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new **)
790 let translate_divumodu8 globals div_not_mod destrs srcrs1 srcrs2 =
792 | List.Nil -> (fun _ -> let l = List.Nil in Bind_new.Bret l)
793 | List.Cons (destr, destrs') ->
798 | List.Nil -> (fun _ -> assert false (* absurd case *))
799 | List.Cons (srcr1, srcrs1') ->
802 | List.Nil -> (fun _ -> assert false (* absurd case *))
803 | List.Cons (srcr2, srcrs2') ->
804 (fun _ -> Bind_new.Bnew (fun dummy ->
806 let { Types.fst = destr1; Types.snd = destr2 } =
807 match div_not_mod with
809 { Types.fst = destr; Types.snd = dummy }
811 { Types.fst = dummy; Types.snd = destr }
813 List.Cons ((Joint.OPACCS (BackEndOps.DivuModu,
814 (Obj.magic destr1), (Obj.magic destr2),
815 (Obj.magic srcr1), (Obj.magic srcr2))), List.Nil)
817 Bind_new.Bret l))) __)) __
818 | List.Cons (x, x0) -> Logic.false_rect_Type0 __)) __
821 ('a1 -> 'a2 -> 'a3 -> 'a3) -> 'a3 -> 'a1 List.list -> 'a2 List.list ->
823 let rec foldr2 f init l1 l2 =
825 | List.Nil -> (fun _ -> init)
826 | List.Cons (a, l1') ->
829 | List.Nil -> (fun _ -> assert false (* absurd case *))
830 | List.Cons (b, l2') -> (fun _ -> f a b (foldr2 f init l1' l2'))) __))
833 (** val translate_ne :
834 AST.ident List.list -> Registers.register List.list -> Joint.psd_argument
835 List.list -> Joint.psd_argument List.list -> (Registers.register,
836 Joint.joint_seq List.list) Bind_new.bind_new **)
837 let translate_ne globals destrs srcrs1 srcrs2 =
839 | List.Nil -> (fun _ -> let l = List.Nil in Bind_new.Bret l)
840 | List.Cons (destr, destrs') ->
843 (let l = translate_fill_with_zero globals destrs' in
848 let l = List.Cons ((Joint.MOVE
849 (Obj.magic { Types.fst = destr; Types.snd =
850 (Joint.psd_argument_from_byte Joint.zero_byte) })),
854 | List.Cons (srcr1, srcrs1') ->
856 | List.Nil -> (fun _ -> assert false (* absurd case *))
857 | List.Cons (srcr2, srcrs2') ->
858 (fun _ -> Bind_new.Bnew (fun tmpr ->
859 let f = fun s1 s2 acc -> List.Cons ((Joint.OP2
860 (BackEndOps.Xor, (Obj.magic tmpr), s1, s2)), (List.Cons
861 ((Joint.OP2 (BackEndOps.Or, (Obj.magic destr),
862 (Obj.magic (Joint.psd_argument_from_reg destr)),
863 (Obj.magic (Joint.psd_argument_from_reg tmpr)))), acc)))
865 let epilogue = List.Cons (Joint.CLEAR_CARRY, (List.Cons
866 ((Joint.OP2 (BackEndOps.Sub, (Obj.magic tmpr),
868 (Joint.psd_argument_from_byte Joint.zero_byte)),
869 (Obj.magic (Joint.psd_argument_from_reg destr)))),
870 (List.Cons ((Joint.OP2 (BackEndOps.Addc,
873 (Joint.psd_argument_from_byte Joint.zero_byte)),
875 (Joint.psd_argument_from_byte Joint.zero_byte)))),
878 let l = List.Cons ((Joint.OP2 (BackEndOps.Xor,
879 (Obj.magic destr), (Obj.magic srcr1),
881 (foldr2 f epilogue (Obj.magic srcrs1')
882 (Obj.magic srcrs2')))
884 Bind_new.Bret l)))) __))) __
886 (** val translate_toggle_bool :
887 AST.ident List.list -> Registers.register List.list ->
888 (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new **)
889 let translate_toggle_bool globals destrs =
891 | List.Nil -> (fun _ -> let l = List.Nil in Bind_new.Bret l)
892 | List.Cons (destr, x) ->
894 let l = List.Cons ((Joint.OP2 (BackEndOps.Xor, (Obj.magic destr),
895 (Obj.magic (Joint.psd_argument_from_reg destr)),
897 (Joint.psd_argument_from_byte (Joint.byte_of_nat (Nat.S Nat.O)))))),
902 (** val translate_lt_unsigned :
903 AST.ident List.list -> Registers.register List.list -> Joint.psd_argument
904 List.list -> Joint.psd_argument List.list -> (Registers.register,
905 Joint.joint_seq List.list) Bind_new.bind_new **)
906 let translate_lt_unsigned globals destrs srcrs1 srcrs2 =
908 | List.Nil -> let l = List.Nil in Bind_new.Bret l
909 | List.Cons (destr, destrs') ->
910 Bind_new.Bnew (fun tmpr ->
912 (let l = translate_fill_with_zero globals destrs' in Bind_new.Bret l)
915 translate_op globals BackEndOps.Sub
916 (List.make_list tmpr (List.length srcrs1)) srcrs1 srcrs2
919 (let l = List.Cons ((Joint.OP2 (BackEndOps.Addc, (Obj.magic destr),
920 (Obj.magic (Joint.psd_argument_from_byte Joint.zero_byte)),
921 (Obj.magic (Joint.psd_argument_from_byte Joint.zero_byte)))),
926 (** val shift_signed :
927 AST.ident List.list -> Registers.register -> Joint.psd_argument List.list
928 -> (Joint.psd_argument List.list, Joint.joint_seq List.list) Types.prod
930 let rec shift_signed globals tmp srcrs =
931 let byte_128 = Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
932 (Nat.S Nat.O))))))), Bool.True,
933 (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
937 | List.Nil -> (fun _ -> { Types.fst = List.Nil; Types.snd = List.Nil })
938 | List.Cons (srcr, srcrs') ->
942 (fun _ -> { Types.fst = (List.Cons ((Joint.Reg tmp), List.Nil));
943 Types.snd = (List.Cons ((Joint.OP2 (BackEndOps.Add,
944 (Obj.magic tmp), (Obj.magic srcr),
945 (Obj.magic (Joint.psd_argument_from_byte byte_128)))),
947 | List.Cons (x, x0) ->
949 let re = shift_signed globals tmp srcrs' in
950 { Types.fst = (List.Cons (srcr, (Types.pi1 re).Types.fst));
951 Types.snd = (Types.pi1 re).Types.snd })) __)) __
953 (** val translate_lt_signed :
954 AST.ident List.list -> Registers.register List.list -> Joint.psd_argument
955 List.list -> Joint.psd_argument List.list -> (Registers.register,
956 Joint.joint_seq List.list) Bind_new.bind_new **)
957 let translate_lt_signed globals destrs srcrs1 srcrs2 =
958 Bind_new.Bnew (fun tmp_last_s1 -> Bind_new.Bnew (fun tmp_last_s2 ->
959 let p1 = shift_signed globals tmp_last_s1 srcrs1 in
960 let new_srcrs1 = (Types.pi1 p1).Types.fst in
961 let shift_srcrs1 = (Types.pi1 p1).Types.snd in
962 let p2 = shift_signed globals tmp_last_s2 srcrs2 in
963 let new_srcrs2 = (Types.pi1 p2).Types.fst in
964 let shift_srcrs2 = (Types.pi1 p2).Types.snd in
965 BindLists.bappend (let l = shift_srcrs1 in Bind_new.Bret l)
966 (BindLists.bappend (let l = shift_srcrs2 in Bind_new.Bret l)
967 (translate_lt_unsigned globals destrs new_srcrs1 new_srcrs2))))
969 (** val translate_lt :
970 Bool.bool -> AST.ident List.list -> Registers.register List.list ->
971 Joint.psd_argument List.list -> Joint.psd_argument List.list ->
972 (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new **)
973 let translate_lt is_unsigned globals destrs srcrs1 srcrs2 =
974 match is_unsigned with
975 | Bool.True -> translate_lt_unsigned globals destrs srcrs1 srcrs2
976 | Bool.False -> translate_lt_signed globals destrs srcrs1 srcrs2
978 (** val translate_cmp :
979 Bool.bool -> AST.ident List.list -> Integers.comparison ->
980 Registers.register List.list -> Joint.psd_argument List.list ->
981 Joint.psd_argument List.list -> (Registers.register, Joint.joint_seq)
982 BindLists.bind_list **)
983 let translate_cmp is_unsigned globals cmp destrs srcrs1 srcrs2 =
986 BindLists.bappend (translate_ne globals destrs srcrs1 srcrs2)
987 (translate_toggle_bool globals destrs)
988 | Integers.Cne -> translate_ne globals destrs srcrs1 srcrs2
989 | Integers.Clt -> translate_lt is_unsigned globals destrs srcrs1 srcrs2
991 BindLists.bappend (translate_lt is_unsigned globals destrs srcrs2 srcrs1)
992 (translate_toggle_bool globals destrs)
993 | Integers.Cgt -> translate_lt is_unsigned globals destrs srcrs2 srcrs1
995 BindLists.bappend (translate_lt is_unsigned globals destrs srcrs1 srcrs2)
996 (translate_toggle_bool globals destrs)
998 (** val translate_op2 :
999 AST.ident List.list -> AST.typ -> AST.typ -> AST.typ ->
1000 FrontEndOps.binary_operation -> Registers.register List.list ->
1001 Joint.psd_argument List.list -> Joint.psd_argument List.list ->
1002 (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new **)
1003 let translate_op2 globals ty1 ty2 ty3 op2 destrs srcrs1 srcrs2 =
1005 | FrontEndOps.Oadd (sz, sg) ->
1007 let l = translate_op globals BackEndOps.Add destrs srcrs1 srcrs2 in
1009 | FrontEndOps.Osub (sz, sg) ->
1011 let l = translate_op globals BackEndOps.Sub destrs srcrs1 srcrs2 in
1013 | FrontEndOps.Omul (sz, sg) ->
1014 (fun _ _ _ -> translate_mul globals destrs srcrs1 srcrs2)
1015 | FrontEndOps.Odiv x -> assert false (* absurd case *)
1016 | FrontEndOps.Odivu sz ->
1018 translate_divumodu8 globals Bool.True destrs srcrs1 srcrs2)
1019 | FrontEndOps.Omod x -> assert false (* absurd case *)
1020 | FrontEndOps.Omodu sz ->
1022 translate_divumodu8 globals Bool.False destrs srcrs1 srcrs2)
1023 | FrontEndOps.Oand (sz, sg) ->
1025 let l = translate_op globals BackEndOps.And destrs srcrs1 srcrs2 in
1027 | FrontEndOps.Oor (sz, sg) ->
1029 let l = translate_op globals BackEndOps.Or destrs srcrs1 srcrs2 in
1031 | FrontEndOps.Oxor (sz, sg) ->
1033 let l = translate_op globals BackEndOps.Xor destrs srcrs1 srcrs2 in
1035 | FrontEndOps.Oshl (x, x0) -> assert false (* absurd case *)
1036 | FrontEndOps.Oshr (x, x0) -> assert false (* absurd case *)
1037 | FrontEndOps.Oshru (x, x0) -> assert false (* absurd case *)
1038 | FrontEndOps.Ocmp (sz, sg1, sg2, c) ->
1039 (fun _ _ _ -> translate_cmp Bool.False globals c destrs srcrs1 srcrs2)
1040 | FrontEndOps.Ocmpu (sz, sg, c) ->
1041 (fun _ _ _ -> translate_cmp Bool.True globals c destrs srcrs1 srcrs2)
1042 | FrontEndOps.Oaddpi sz ->
1044 translate_op_asym_signed globals BackEndOps.Add destrs srcrs1 srcrs2)
1045 | FrontEndOps.Oaddip sz ->
1047 translate_op_asym_signed globals BackEndOps.Add destrs srcrs2 srcrs1)
1048 | FrontEndOps.Osubpi sz ->
1050 translate_op_asym_signed globals BackEndOps.Add destrs srcrs1 srcrs2)
1051 | FrontEndOps.Osubpp sz ->
1054 translate_op_asym_unsigned globals BackEndOps.Sub destrs srcrs1
1058 | FrontEndOps.Ocmpp (sg, c) ->
1059 (fun _ _ _ -> translate_cmp Bool.True globals c destrs srcrs1 srcrs2))
1062 (** val translate_cond :
1063 AST.ident List.list -> Registers.register List.list -> Graphs.label ->
1064 Blocks.bind_step_block **)
1065 let translate_cond globals srcrs lbl_true =
1069 (Blocks.ensure_step_block (Joint.graph_params_to_params RTL.rTL)
1071 | List.Cons (srcr, srcrs') ->
1072 Bind_new.Bnew (fun tmpr ->
1073 let f = fun r x -> Joint.OP2 (BackEndOps.Or, (Obj.magic tmpr),
1074 (Obj.magic (Joint.psd_argument_from_reg tmpr)),
1075 (Obj.magic (Joint.psd_argument_from_reg r)))
1077 Bind_new.Bret { Types.fst = { Types.fst = (List.Cons ((fun x ->
1079 (Obj.magic { Types.fst = tmpr; Types.snd =
1080 (Joint.psd_argument_from_reg srcr) })), (List.map f srcrs')));
1081 Types.snd = (fun x -> Joint.COND ((Obj.magic tmpr), lbl_true)) };
1082 Types.snd = List.Nil })
1084 (** val translate_load :
1085 AST.ident List.list -> Joint.psd_argument List.list -> Registers.register
1086 List.list -> (Registers.register, Joint.joint_seq List.list)
1087 Bind_new.bind_new **)
1088 let translate_load globals addr destrs =
1089 Bind_new.Bnew (fun tmp_addr_l -> Bind_new.Bnew (fun tmp_addr_h ->
1092 translate_move globals (List.Cons (tmp_addr_l, (List.Cons
1093 (tmp_addr_h, List.Nil)))) addr
1096 (let f = fun destr acc ->
1098 (let l = List.Cons ((Joint.LOAD (destr,
1099 (Obj.magic (Joint.Reg tmp_addr_l)),
1100 (Obj.magic (Joint.Reg tmp_addr_h)))), List.Nil)
1105 translate_op globals BackEndOps.Add (List.Cons (tmp_addr_l,
1106 (List.Cons (tmp_addr_h, List.Nil)))) (List.Cons
1107 ((Joint.psd_argument_from_reg tmp_addr_l), (List.Cons
1108 ((Joint.psd_argument_from_reg tmp_addr_h), List.Nil))))
1110 ((let x = I8051.int_size in Joint.psd_argument_from_byte x),
1111 (List.Cons ((Joint.psd_argument_from_byte Joint.zero_byte),
1114 Bind_new.Bret l) acc)
1116 List.foldr f (let l = List.Nil in Bind_new.Bret l) (Obj.magic destrs))))
1118 (** val translate_store :
1119 AST.ident List.list -> Joint.psd_argument List.list -> Joint.psd_argument
1120 List.list -> (Registers.register, Joint.joint_seq List.list)
1121 Bind_new.bind_new **)
1122 let translate_store globals addr srcrs =
1123 Bind_new.Bnew (fun tmp_addr_l -> Bind_new.Bnew (fun tmp_addr_h ->
1126 translate_move globals (List.Cons (tmp_addr_l, (List.Cons
1127 (tmp_addr_h, List.Nil)))) addr
1130 (let f = fun srcr acc ->
1132 (let l = List.Cons ((Joint.STORE
1133 ((Obj.magic (Joint.Reg tmp_addr_l)),
1134 (Obj.magic (Joint.Reg tmp_addr_h)), srcr)), List.Nil)
1139 translate_op globals BackEndOps.Add (List.Cons (tmp_addr_l,
1140 (List.Cons (tmp_addr_h, List.Nil)))) (List.Cons
1141 ((Joint.psd_argument_from_reg tmp_addr_l), (List.Cons
1142 ((Joint.psd_argument_from_reg tmp_addr_h), List.Nil))))
1144 ((let x = I8051.int_size in Joint.psd_argument_from_byte x),
1145 (List.Cons ((Joint.psd_argument_from_byte Joint.zero_byte),
1148 Bind_new.Bret l) acc)
1150 List.foldr f (let l = List.Nil in Bind_new.Bret l) (Obj.magic srcrs))))
1152 (** val ensure_bind_step_block :
1153 Joint.params -> AST.ident List.list -> (Registers.register,
1154 Joint.joint_seq List.list) Bind_new.bind_new -> Blocks.bind_step_block **)
1155 let ensure_bind_step_block p g b =
1157 (Monad.m_bind0 (Monad.max_def Bind_new.bindNew) (Obj.magic b) (fun l ->
1158 Obj.magic (Bind_new.Bret (Blocks.ensure_step_block p g l))))
1160 (** val translate_statement :
1161 AST.ident List.list -> (Registers.register, AST.typ) Types.prod List.list
1162 -> local_env -> RTLabs_syntax.statement -> ((Blocks.bind_step_block,
1163 Blocks.bind_fin_block) Types.sum, __) Types.dPair **)
1164 let translate_statement globals locals lenv stmt =
1166 | RTLabs_syntax.St_skip lbl' ->
1167 (fun _ -> { Types.dpi1 = (Types.Inl (Bind_new.Bret
1168 (Blocks.ensure_step_block (Joint.graph_params_to_params RTL.rTL)
1169 globals List.Nil))); Types.dpi2 = (Obj.magic lbl') })
1170 | RTLabs_syntax.St_cost (cost_lbl, lbl') ->
1171 (fun _ -> { Types.dpi1 = (Types.Inl (Bind_new.Bret { Types.fst =
1172 { Types.fst = List.Nil; Types.snd = (fun x -> Joint.COST_LABEL
1173 cost_lbl) }; Types.snd = List.Nil })); Types.dpi2 =
1175 | RTLabs_syntax.St_const (ty, destr, cst, lbl') ->
1176 (fun _ -> { Types.dpi1 = (Types.Inl
1177 (ensure_bind_step_block (Joint.graph_params_to_params RTL.rTL) globals
1178 (translate_cst ty globals cst (find_local_env destr lenv))));
1179 Types.dpi2 = (Obj.magic lbl') })
1180 | RTLabs_syntax.St_op1 (ty, ty', op1, destr, srcr, lbl') ->
1181 (fun _ -> { Types.dpi1 = (Types.Inl
1182 (ensure_bind_step_block (Joint.graph_params_to_params RTL.rTL) globals
1183 (translate_op1 globals ty' ty op1 (find_local_env destr lenv)
1184 (find_local_env srcr lenv)))); Types.dpi2 = (Obj.magic lbl') })
1185 | RTLabs_syntax.St_op2 (ty1, ty2, ty3, op2, destr, srcr1, srcr2, lbl') ->
1186 (fun _ -> { Types.dpi1 = (Types.Inl
1187 (ensure_bind_step_block (Joint.graph_params_to_params RTL.rTL) globals
1188 (translate_op2 globals ty2 ty3 ty1 op2 (find_local_env destr lenv)
1189 (find_local_env_arg srcr1 lenv) (find_local_env_arg srcr2 lenv))));
1190 Types.dpi2 = (Obj.magic lbl') })
1191 | RTLabs_syntax.St_load (ignore, addr, destr, lbl') ->
1192 (fun _ -> { Types.dpi1 = (Types.Inl
1193 (ensure_bind_step_block (Joint.graph_params_to_params RTL.rTL) globals
1194 (translate_load globals (find_local_env_arg addr lenv)
1195 (find_local_env destr lenv)))); Types.dpi2 = (Obj.magic lbl') })
1196 | RTLabs_syntax.St_store (ignore, addr, srcr, lbl') ->
1197 (fun _ -> { Types.dpi1 = (Types.Inl
1198 (ensure_bind_step_block (Joint.graph_params_to_params RTL.rTL) globals
1199 (translate_store globals (find_local_env_arg addr lenv)
1200 (find_local_env_arg srcr lenv)))); Types.dpi2 =
1202 | RTLabs_syntax.St_call_id (f, args, retr, lbl') ->
1203 (fun _ -> { Types.dpi1 = (Types.Inl (Bind_new.Bret { Types.fst =
1204 { Types.fst = List.Nil; Types.snd = (fun x -> Joint.CALL ((Types.Inl
1205 f), (Obj.magic (rtl_args args lenv)),
1207 | Types.None -> Obj.magic List.Nil
1208 | Types.Some retr0 -> Obj.magic (find_local_env retr0 lenv)))) };
1209 Types.snd = List.Nil })); Types.dpi2 = (Obj.magic lbl') })
1210 | RTLabs_syntax.St_call_ptr (f, args, retr, lbl') ->
1212 let fs = find_and_addr_arg f lenv in
1213 { Types.dpi1 = (Types.Inl (Bind_new.Bret { Types.fst = { Types.fst =
1214 List.Nil; Types.snd = (fun x -> Joint.CALL ((Types.Inr
1215 (Obj.magic fs)), (Obj.magic (rtl_args args lenv)),
1217 | Types.None -> Obj.magic List.Nil
1218 | Types.Some retr0 -> Obj.magic (find_local_env retr0 lenv)))) };
1219 Types.snd = List.Nil })); Types.dpi2 = (Obj.magic lbl') })
1220 | RTLabs_syntax.St_cond (r, lbl_true, lbl_false) ->
1221 (fun _ -> { Types.dpi1 = (Types.Inl
1222 (translate_cond globals (find_local_env r lenv) lbl_true));
1223 Types.dpi2 = (Obj.magic lbl_false) })
1224 | RTLabs_syntax.St_return ->
1225 (fun _ -> { Types.dpi1 = (Types.Inr (Bind_new.Bret { Types.fst =
1226 List.Nil; Types.snd = Joint.RETURN })); Types.dpi2 =
1227 (Obj.magic Types.It) })) __
1229 (** val translate_internal :
1230 AST.ident List.list -> RTLabs_syntax.internal_function ->
1231 Joint.joint_closed_internal_function **)
1232 let translate_internal globals def =
1233 let runiverse' = def.RTLabs_syntax.f_reggen in
1234 let luniverse' = def.RTLabs_syntax.f_labgen in
1235 let stack_size' = def.RTLabs_syntax.f_stacksize in
1236 let entry' = Types.pi1 def.RTLabs_syntax.f_entry in
1237 let init = { Joint.joint_if_luniverse = luniverse';
1238 Joint.joint_if_runiverse = runiverse'; Joint.joint_if_result =
1239 (Obj.magic List.Nil); Joint.joint_if_params = (Obj.magic List.Nil);
1240 Joint.joint_if_stacksize = stack_size'; Joint.joint_if_local_stacksize =
1241 stack_size'; Joint.joint_if_code =
1243 (Identifiers.add PreIdentifiers.LabelTag
1244 (Identifiers.empty_map PreIdentifiers.LabelTag) entry' (Joint.Final
1245 Joint.RETURN))); Joint.joint_if_entry = (Obj.magic entry') }
1247 (let { Types.fst = init'; Types.snd = lenv } =
1248 Obj.magic initialize_locals_params_ret globals
1249 def.RTLabs_syntax.f_locals def.RTLabs_syntax.f_params
1250 def.RTLabs_syntax.f_result init
1254 List.append def.RTLabs_syntax.f_locals
1255 (List.append def.RTLabs_syntax.f_params
1256 (match def.RTLabs_syntax.f_result with
1257 | Types.None -> List.Nil
1258 | Types.Some x -> List.Cons (x, List.Nil)))
1260 let f_trans = fun lbl stmt def0 ->
1261 let pr = translate_statement globals vars lenv stmt in
1262 (match pr.Types.dpi1 with
1263 | Types.Inl instrs ->
1265 TranslateUtils.b_adds_graph RTL.rTL globals instrs lbl
1266 (Obj.magic lbl') def0)
1267 | Types.Inr instrs ->
1269 TranslateUtils.b_fin_adds_graph RTL.rTL globals instrs lbl def0))
1272 Identifiers.foldi PreIdentifiers.LabelTag f_trans def.RTLabs_syntax.f_graph
1275 (** val rtlabs_to_rtl :
1276 CostLabel.costlabel -> RTLabs_syntax.rTLabs_program -> RTL.rtl_program **)
1277 let rtlabs_to_rtl init_cost p =
1278 { Joint.jp_functions = (AST.prog_funct_names p); Joint.joint_prog =
1279 (AST.transform_program p (fun varnames ->
1281 (translate_internal (List.append varnames (AST.prog_funct_names p)))));
1282 Joint.init_cost_label = init_cost }