Changeset 2921
- Timestamp:
- Mar 21, 2013, 12:56:57 AM (5 years ago)
- Location:
- extracted
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
extracted/rTLabsToRTL.ml
r2913 r2921 150 150 -> 'a1) -> register_type -> 'a1 **) 151 151 let rec register_type_rect_Type4 h_register_int h_register_ptr = function 152 | Register_int x_ 21297 -> h_register_int x_21297153 | Register_ptr (x_ 21299, x_21298) -> h_register_ptr x_21299 x_21298152 | Register_int x_8 -> h_register_int x_8 153 | Register_ptr (x_10, x_9) -> h_register_ptr x_10 x_9 154 154 155 155 (** val register_type_rect_Type5 : … … 157 157 -> 'a1) -> register_type -> 'a1 **) 158 158 let rec register_type_rect_Type5 h_register_int h_register_ptr = function 159 | Register_int x_ 21303 -> h_register_int x_21303160 | Register_ptr (x_ 21305, x_21304) -> h_register_ptr x_21305 x_21304159 | Register_int x_14 -> h_register_int x_14 160 | Register_ptr (x_16, x_15) -> h_register_ptr x_16 x_15 161 161 162 162 (** val register_type_rect_Type3 : … … 164 164 -> 'a1) -> register_type -> 'a1 **) 165 165 let rec register_type_rect_Type3 h_register_int h_register_ptr = function 166 | Register_int x_2 1309 -> h_register_int x_21309167 | Register_ptr (x_2 1311, x_21310) -> h_register_ptr x_21311 x_21310166 | Register_int x_20 -> h_register_int x_20 167 | Register_ptr (x_22, x_21) -> h_register_ptr x_22 x_21 168 168 169 169 (** val register_type_rect_Type2 : … … 171 171 -> 'a1) -> register_type -> 'a1 **) 172 172 let rec register_type_rect_Type2 h_register_int h_register_ptr = function 173 | Register_int x_2 1315 -> h_register_int x_21315174 | Register_ptr (x_2 1317, x_21316) -> h_register_ptr x_21317 x_21316173 | Register_int x_26 -> h_register_int x_26 174 | Register_ptr (x_28, x_27) -> h_register_ptr x_28 x_27 175 175 176 176 (** val register_type_rect_Type1 : … … 178 178 -> 'a1) -> register_type -> 'a1 **) 179 179 let rec register_type_rect_Type1 h_register_int h_register_ptr = function 180 | Register_int x_ 21321 -> h_register_int x_21321181 | Register_ptr (x_ 21323, x_21322) -> h_register_ptr x_21323 x_21322180 | Register_int x_32 -> h_register_int x_32 181 | Register_ptr (x_34, x_33) -> h_register_ptr x_34 x_33 182 182 183 183 (** val register_type_rect_Type0 : … … 185 185 -> 'a1) -> register_type -> 'a1 **) 186 186 let rec register_type_rect_Type0 h_register_int h_register_ptr = function 187 | Register_int x_ 21327 -> h_register_int x_21327188 | Register_ptr (x_ 21329, x_21328) -> h_register_ptr x_21329 x_21328187 | Register_int x_38 -> h_register_int x_38 188 | Register_ptr (x_40, x_39) -> h_register_ptr x_40 x_39 189 189 190 190 (** val register_type_inv_rect_Type4 : … … 386 386 AST.ident List.list -> BackEndOps.op2 -> Registers.register List.list -> 387 387 Joint.psd_argument List.list -> Joint.psd_argument List.list -> 388 (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new**)388 Joint.joint_seq List.list **) 389 389 let translate_op globals op destrs srcrs1 srcrs2 = 390 390 (match op with 391 391 | BackEndOps.Add -> 392 (fun _ -> 393 (match destrs with 394 | List.Nil -> (fun _ _ _ -> let l = List.Nil in Bind_new.Bret l) 395 | List.Cons (destr, destrs') -> 396 (fun _ -> 397 (match srcrs1 with 398 | List.Nil -> (fun _ _ -> assert false (* absurd case *)) 399 | List.Cons (srcr1, srcrs1') -> 400 (fun _ _ -> 401 (match srcrs2 with 402 | List.Nil -> (fun _ _ -> assert false (* absurd case *)) 403 | List.Cons (srcr2, srcrs2') -> 404 (fun _ _ -> 405 let l = List.Cons ((Joint.OP2 (BackEndOps.Add, 406 (Obj.magic destr), (Obj.magic srcr1), 407 (Obj.magic srcr2))), 408 (translate_op_aux globals BackEndOps.Addc destrs' 409 srcrs1' srcrs2')) 410 in 411 Bind_new.Bret l)) __)) __)) __) 392 (match destrs with 393 | List.Nil -> (fun _ _ -> List.Nil) 394 | List.Cons (destr, destrs') -> 395 (match srcrs1 with 396 | List.Nil -> (fun _ -> assert false (* absurd case *)) 397 | List.Cons (srcr1, srcrs1') -> 398 (fun _ -> 399 match srcrs2 with 400 | List.Nil -> (fun _ -> assert false (* absurd case *)) 401 | List.Cons (srcr2, srcrs2') -> 402 (fun _ -> List.Cons ((Joint.OP2 (BackEndOps.Add, 403 (Obj.magic destr), (Obj.magic srcr1), (Obj.magic srcr2))), 404 (translate_op_aux globals BackEndOps.Addc destrs' srcrs1' 405 srcrs2')))))) 412 406 | BackEndOps.Addc -> 413 (fun _ _ _ -> 414 let l = 415 List.append (List.Cons (Joint.CLEAR_CARRY, List.Nil)) 416 (translate_op_aux globals BackEndOps.Addc destrs srcrs1 srcrs2) 417 in 418 Bind_new.Bret l) 407 (fun _ _ -> 408 List.append (List.Cons (Joint.CLEAR_CARRY, List.Nil)) 409 (translate_op_aux globals BackEndOps.Addc destrs srcrs1 srcrs2)) 419 410 | BackEndOps.Sub -> 420 (fun _ _ _ -> 421 let l = 422 List.append (List.Cons (Joint.CLEAR_CARRY, List.Nil)) 423 (translate_op_aux globals BackEndOps.Sub destrs srcrs1 srcrs2) 424 in 425 Bind_new.Bret l) 411 (fun _ _ -> 412 List.append (List.Cons (Joint.CLEAR_CARRY, List.Nil)) 413 (translate_op_aux globals BackEndOps.Sub destrs srcrs1 srcrs2)) 426 414 | BackEndOps.And -> 427 (fun _ _ _ -> 428 let l = translate_op_aux globals op destrs srcrs1 srcrs2 in 429 Bind_new.Bret l) 415 (fun _ _ -> translate_op_aux globals op destrs srcrs1 srcrs2) 430 416 | BackEndOps.Or -> 431 (fun _ _ _ -> 432 let l = translate_op_aux globals op destrs srcrs1 srcrs2 in 433 Bind_new.Bret l) 417 (fun _ _ -> translate_op_aux globals op destrs srcrs1 srcrs2) 434 418 | BackEndOps.Xor -> 435 (fun _ _ _ -> 436 let l = translate_op_aux globals op destrs srcrs1 srcrs2 in 437 Bind_new.Bret l)) __ __ __ 419 (fun _ _ -> translate_op_aux globals op destrs srcrs1 srcrs2)) __ __ 438 420 439 421 (** val cast_list : 'a1 -> Nat.nat -> 'a1 List.list -> 'a1 List.list **) … … 448 430 AST.ident List.list -> BackEndOps.op2 -> Registers.register List.list -> 449 431 Joint.psd_argument List.list -> Joint.psd_argument List.list -> 450 (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new**)432 Joint.joint_seq List.list **) 451 433 let translate_op_asym_unsigned globals op destrs srcrs1 srcrs2 = 452 434 let l = List.length destrs in … … 497 479 let { Types.fst = r1; Types.snd = r2 } = make_addr destrs in 498 480 List.Cons ((Joint.ADDRESS (id, (Obj.magic r1), (Obj.magic r2))), 499 (List.Cons ((Joint.OP2 (BackEndOps.Add, (Obj.magic r1), 500 (Obj.magic (Joint.psd_argument_from_reg r1)), 501 (Obj.magic 502 (Joint.psd_argument_from_byte (Joint.byte_of_nat offset))))), 503 (List.Cons ((Joint.OP2 (BackEndOps.Addc, (Obj.magic r2), 504 (Obj.magic (Joint.psd_argument_from_reg r2)), 505 (Obj.magic (Joint.psd_argument_from_byte Joint.zero_byte)))), 506 List.Nil)))))) 481 (match Nat.eqb offset Nat.O with 482 | Bool.True -> List.Nil 483 | Bool.False -> 484 translate_op globals BackEndOps.Add (List.Cons (r1, (List.Cons 485 (r2, List.Nil)))) (List.Cons ((Joint.psd_argument_from_reg r1), 486 (List.Cons ((Joint.psd_argument_from_reg r2), List.Nil)))) 487 (List.Cons 488 ((Joint.psd_argument_from_byte (Joint.byte_of_nat offset)), 489 (List.Cons ((Joint.psd_argument_from_byte Joint.zero_byte), 490 List.Nil))))))) 507 491 | FrontEndOps.Oaddrstack offset -> 508 492 (fun _ _ -> … … 512 496 (Obj.magic (RTL.Rtl_stack_address (r1, r2))) 513 497 in 514 x), (List.Cons ((Joint.OP2 (BackEndOps.Add, (Obj.magic r1), 515 (Obj.magic (Joint.psd_argument_from_reg r1)), 516 (Obj.magic 517 (Joint.psd_argument_from_byte (Joint.byte_of_nat offset))))), 518 (List.Cons ((Joint.OP2 (BackEndOps.Addc, (Obj.magic r2), 519 (Obj.magic (Joint.psd_argument_from_reg r2)), 520 (Obj.magic (Joint.psd_argument_from_byte Joint.zero_byte)))), 521 List.Nil))))))) __ __ 498 x), 499 (match Nat.eqb offset Nat.O with 500 | Bool.True -> List.Nil 501 | Bool.False -> 502 translate_op globals BackEndOps.Add (List.Cons (r1, (List.Cons 503 (r2, List.Nil)))) (List.Cons ((Joint.psd_argument_from_reg r1), 504 (List.Cons ((Joint.psd_argument_from_reg r2), List.Nil)))) 505 (List.Cons 506 ((Joint.psd_argument_from_byte (Joint.byte_of_nat offset)), 507 (List.Cons ((Joint.psd_argument_from_byte Joint.zero_byte), 508 List.Nil)))))))) __ __ 522 509 in 523 510 Bind_new.Bret l … … 618 605 BindLists.bappend (let l0 = srcrs1init.Types.snd in Bind_new.Bret l0) 619 606 (BindLists.bappend (let l0 = srcrs2init.Types.snd in Bind_new.Bret l0) 620 (translate_op globals op destrs srcrs1init.Types.fst 621 srcrs2init.Types.fst)))) 607 (let l0 = 608 translate_op globals op destrs srcrs1init.Types.fst 609 srcrs2init.Types.fst 610 in 611 Bind_new.Bret l0)))) 622 612 623 613 (** val translate_cast : … … 651 641 let l = translate_fill_with_zero globals dst_rest in 652 642 Bind_new.Bret l) 653 | List.Cons (x, x0) -> 654 let l = List.Nil in Bind_new.Bret l) 643 | List.Cons (x, x0) -> let l = List.Nil in Bind_new.Bret l) 655 644 656 645 (** val translate_notint : … … 663 652 (** val translate_negint : 664 653 AST.ident List.list -> Registers.register List.list -> Registers.register 665 List.list -> (Registers.register, Joint.joint_seq List.list) 666 Bind_new.bind_new **) 654 List.list -> Joint.joint_seq List.list **) 667 655 let translate_negint globals destrs srcrs = 668 BindLists.bappend 669 (let l = translate_notint globals destrs srcrs in Bind_new.Bret l) 656 List.append (translate_notint globals destrs srcrs) 670 657 (translate_op globals BackEndOps.Add destrs 671 658 (List.map (fun x -> Joint.Reg x) destrs) … … 723 710 (fun _ _ -> translate_cast globals src_sign destrs srcrs) 724 711 | FrontEndOps.Onegint (sz, sg) -> 725 (fun _ _ -> translate_negint globals destrs srcrs) 712 (fun _ _ -> 713 let l = translate_negint globals destrs srcrs in Bind_new.Bret l) 726 714 | FrontEndOps.Onotbool (x, x0, x1) -> 727 715 (fun _ _ -> translate_notbool globals destrs srcrs) … … 745 733 Nat.nat -> Registers.register List.list -> Joint.psd_argument List.list 746 734 -> Joint.psd_argument List.list -> Nat.nat -> Nat.nat Types.sig0 -> 747 (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new -> 748 (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new **) 735 Joint.joint_seq List.list -> Joint.joint_seq List.list **) 749 736 let translate_mul_i globals a b n tmp_destrs_dummy srcrs1 srcrs2 k i_sig acc = 750 737 let i = i_sig in … … 757 744 in 758 745 let tmp_destrs_view = List.ltl tmp_destrs_dummy k in 759 BindLists.bappend 760 (let l = List.Cons ((Joint.OPACCS (BackEndOps.Mul, (Obj.magic a), 761 (Obj.magic b), (Util.nth_safe i (Obj.magic srcrs1)), 762 (Util.nth_safe (Nat.minus k i) (Obj.magic srcrs2)))), List.Nil) 763 in 764 Bind_new.Bret l) 765 (BindLists.bappend 746 List.append (List.Cons ((Joint.OPACCS (BackEndOps.Mul, (Obj.magic a), 747 (Obj.magic b), (Util.nth_safe i (Obj.magic srcrs1)), 748 (Util.nth_safe (Nat.minus k i) (Obj.magic srcrs2)))), List.Nil)) 749 (List.append 766 750 (translate_op globals BackEndOps.Add tmp_destrs_view 767 751 (List.map (fun x -> Joint.Reg x) tmp_destrs_view) args) acc) … … 782 766 srcrs2 k) acc (Lists.range_strong (Nat.S k)) 783 767 in 784 BindLists.bappend 785 (let l = translate_fill_with_zero globals tmp_destrs in 786 Bind_new.Bret l) 787 (BindLists.bappend 788 (List.foldr translate_mul_k (let l = List.Nil in Bind_new.Bret l) 789 (Lists.range_strong (List.length destrs))) 790 (let l = 791 translate_move globals destrs 792 (List.map (fun x -> Joint.Reg x) tmp_destrs) 793 in 794 Bind_new.Bret l)))))) 768 let l = 769 List.append (translate_fill_with_zero globals tmp_destrs) 770 (List.append 771 (List.foldr translate_mul_k List.Nil 772 (Lists.range_strong (List.length destrs))) 773 (translate_move globals destrs 774 (List.map (fun x -> Joint.Reg x) tmp_destrs))) 775 in 776 Bind_new.Bret l)))) 795 777 796 778 (** val translate_divumodu8 : … … 919 901 (let l = translate_fill_with_zero globals destrs' in Bind_new.Bret l) 920 902 (BindLists.bappend 921 (translate_op globals BackEndOps.Sub 922 (List.make_list tmpr (List.length srcrs1)) srcrs1 srcrs2) 903 (let l = 904 translate_op globals BackEndOps.Sub 905 (List.make_list tmpr (List.length srcrs1)) srcrs1 srcrs2 906 in 907 Bind_new.Bret l) 923 908 (let l = List.Cons ((Joint.OP2 (BackEndOps.Addc, (Obj.magic destr), 924 909 (Obj.magic (Joint.psd_argument_from_byte Joint.zero_byte)), … … 1008 993 (match op2 with 1009 994 | FrontEndOps.Oadd (sz, sg) -> 1010 (fun _ _ _ -> translate_op globals BackEndOps.Add destrs srcrs1 srcrs2) 995 (fun _ _ _ -> 996 let l = translate_op globals BackEndOps.Add destrs srcrs1 srcrs2 in 997 Bind_new.Bret l) 1011 998 | FrontEndOps.Osub (sz, sg) -> 1012 (fun _ _ _ -> translate_op globals BackEndOps.Sub destrs srcrs1 srcrs2) 999 (fun _ _ _ -> 1000 let l = translate_op globals BackEndOps.Sub destrs srcrs1 srcrs2 in 1001 Bind_new.Bret l) 1013 1002 | FrontEndOps.Omul (sz, sg) -> 1014 1003 (fun _ _ _ -> translate_mul globals destrs srcrs1 srcrs2) … … 1022 1011 translate_divumodu8 globals Bool.False destrs srcrs1 srcrs2) 1023 1012 | FrontEndOps.Oand (sz, sg) -> 1024 (fun _ _ _ -> translate_op globals BackEndOps.And destrs srcrs1 srcrs2) 1013 (fun _ _ _ -> 1014 let l = translate_op globals BackEndOps.And destrs srcrs1 srcrs2 in 1015 Bind_new.Bret l) 1025 1016 | FrontEndOps.Oor (sz, sg) -> 1026 (fun _ _ _ -> translate_op globals BackEndOps.Or destrs srcrs1 srcrs2) 1017 (fun _ _ _ -> 1018 let l = translate_op globals BackEndOps.Or destrs srcrs1 srcrs2 in 1019 Bind_new.Bret l) 1027 1020 | FrontEndOps.Oxor (sz, sg) -> 1028 (fun _ _ _ -> translate_op globals BackEndOps.Xor destrs srcrs1 srcrs2) 1021 (fun _ _ _ -> 1022 let l = translate_op globals BackEndOps.Xor destrs srcrs1 srcrs2 in 1023 Bind_new.Bret l) 1029 1024 | FrontEndOps.Oshl (x, x0) -> assert false (* absurd case *) 1030 1025 | FrontEndOps.Oshr (x, x0) -> assert false (* absurd case *) … … 1045 1040 | FrontEndOps.Osubpp sz -> 1046 1041 (fun _ _ _ -> 1047 translate_op_asym_unsigned globals BackEndOps.Sub destrs srcrs1 srcrs2) 1042 let l = 1043 translate_op_asym_unsigned globals BackEndOps.Sub destrs srcrs1 1044 srcrs2 1045 in 1046 Bind_new.Bret l) 1048 1047 | FrontEndOps.Ocmpp (sg, c) -> 1049 (fun _ _ _ -> 1050 let is_Ocmpp = Nat.O in 1051 translate_cmp Bool.True globals c destrs srcrs1 srcrs2)) __ __ __ 1048 (fun _ _ _ -> translate_cmp Bool.True globals c destrs srcrs1 srcrs2)) 1049 __ __ __ 1052 1050 1053 1051 (** val translate_cond : … … 1093 1091 Bind_new.Bret l) 1094 1092 (BindLists.bappend 1095 (translate_op globals BackEndOps.Add (List.Cons (tmp_addr_l, 1096 (List.Cons (tmp_addr_h, List.Nil)))) (List.Cons 1097 ((Joint.psd_argument_from_reg tmp_addr_l), (List.Cons 1098 ((Joint.psd_argument_from_reg tmp_addr_h), List.Nil)))) 1099 (List.Cons ((Joint.psd_argument_from_byte Joint.zero_byte), 1100 (List.Cons 1101 ((let x = I8051.int_size in Joint.psd_argument_from_byte x), 1102 List.Nil))))) acc) 1093 (let l = 1094 translate_op globals BackEndOps.Add (List.Cons (tmp_addr_l, 1095 (List.Cons (tmp_addr_h, List.Nil)))) (List.Cons 1096 ((Joint.psd_argument_from_reg tmp_addr_l), (List.Cons 1097 ((Joint.psd_argument_from_reg tmp_addr_h), List.Nil)))) 1098 (List.Cons 1099 ((let x = I8051.int_size in Joint.psd_argument_from_byte x), 1100 (List.Cons ((Joint.psd_argument_from_byte Joint.zero_byte), 1101 List.Nil)))) 1102 in 1103 Bind_new.Bret l) acc) 1103 1104 in 1104 1105 List.foldr f (let l = List.Nil in Bind_new.Bret l) (Obj.magic destrs)))) … … 1124 1125 Bind_new.Bret l) 1125 1126 (BindLists.bappend 1126 (translate_op globals BackEndOps.Add (List.Cons (tmp_addr_l, 1127 (List.Cons (tmp_addr_h, List.Nil)))) (List.Cons 1128 ((Joint.psd_argument_from_reg tmp_addr_l), (List.Cons 1129 ((Joint.psd_argument_from_reg tmp_addr_h), List.Nil)))) 1130 (List.Cons ((Joint.psd_argument_from_byte Joint.zero_byte), 1131 (List.Cons 1132 ((let x = I8051.int_size in Joint.psd_argument_from_byte x), 1133 List.Nil))))) acc) 1127 (let l = 1128 translate_op globals BackEndOps.Add (List.Cons (tmp_addr_l, 1129 (List.Cons (tmp_addr_h, List.Nil)))) (List.Cons 1130 ((Joint.psd_argument_from_reg tmp_addr_l), (List.Cons 1131 ((Joint.psd_argument_from_reg tmp_addr_h), List.Nil)))) 1132 (List.Cons 1133 ((let x = I8051.int_size in Joint.psd_argument_from_byte x), 1134 (List.Cons ((Joint.psd_argument_from_byte Joint.zero_byte), 1135 List.Nil)))) 1136 in 1137 Bind_new.Bret l) acc) 1134 1138 in 1135 1139 List.foldr f (let l = List.Nil in Bind_new.Bret l) (Obj.magic srcrs)))) -
extracted/rTLabsToRTL.mli
r2867 r2921 246 246 AST.ident List.list -> BackEndOps.op2 -> Registers.register List.list -> 247 247 Joint.psd_argument List.list -> Joint.psd_argument List.list -> 248 (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new248 Joint.joint_seq List.list 249 249 250 250 val cast_list : 'a1 -> Nat.nat -> 'a1 List.list -> 'a1 List.list … … 253 253 AST.ident List.list -> BackEndOps.op2 -> Registers.register List.list -> 254 254 Joint.psd_argument List.list -> Joint.psd_argument List.list -> 255 (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new255 Joint.joint_seq List.list 256 256 257 257 val zero_args : Nat.nat -> Joint.psd_argument List.list Types.sig0 … … 300 300 val translate_negint : 301 301 AST.ident List.list -> Registers.register List.list -> Registers.register 302 List.list -> (Registers.register, Joint.joint_seq List.list) 303 Bind_new.bind_new 302 List.list -> Joint.joint_seq List.list 304 303 305 304 val translate_notbool : … … 317 316 -> Registers.register List.list -> Joint.psd_argument List.list -> 318 317 Joint.psd_argument List.list -> Nat.nat -> Nat.nat Types.sig0 -> 319 (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new -> 320 (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new 318 Joint.joint_seq List.list -> Joint.joint_seq List.list 321 319 322 320 val translate_mul :
Note: See TracChangeset
for help on using the changeset viewer.