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.