Changeset 2827 for extracted/eRTLptrToLTL.ml
 Timestamp:
 Mar 8, 2013, 9:07:28 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/eRTLptrToLTL.ml
r2797 r2827 167 167 arg_decision > 'a1 **) 168 168 let rec arg_decision_rect_Type4 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function 169  Arg_decision_colour x_21 810 > h_arg_decision_colour x_21810170  Arg_decision_spill x_21 811 > h_arg_decision_spill x_21811171  Arg_decision_imm x_21 812 > h_arg_decision_imm x_21812169  Arg_decision_colour x_21936 > h_arg_decision_colour x_21936 170  Arg_decision_spill x_21937 > h_arg_decision_spill x_21937 171  Arg_decision_imm x_21938 > h_arg_decision_imm x_21938 172 172 173 173 (** val arg_decision_rect_Type5 : … … 175 175 arg_decision > 'a1 **) 176 176 let rec arg_decision_rect_Type5 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function 177  Arg_decision_colour x_21 817 > h_arg_decision_colour x_21817178  Arg_decision_spill x_21 818 > h_arg_decision_spill x_21818179  Arg_decision_imm x_21 819 > h_arg_decision_imm x_21819177  Arg_decision_colour x_21943 > h_arg_decision_colour x_21943 178  Arg_decision_spill x_21944 > h_arg_decision_spill x_21944 179  Arg_decision_imm x_21945 > h_arg_decision_imm x_21945 180 180 181 181 (** val arg_decision_rect_Type3 : … … 183 183 arg_decision > 'a1 **) 184 184 let rec arg_decision_rect_Type3 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function 185  Arg_decision_colour x_21 824 > h_arg_decision_colour x_21824186  Arg_decision_spill x_21 825 > h_arg_decision_spill x_21825187  Arg_decision_imm x_21 826 > h_arg_decision_imm x_21826185  Arg_decision_colour x_21950 > h_arg_decision_colour x_21950 186  Arg_decision_spill x_21951 > h_arg_decision_spill x_21951 187  Arg_decision_imm x_21952 > h_arg_decision_imm x_21952 188 188 189 189 (** val arg_decision_rect_Type2 : … … 191 191 arg_decision > 'a1 **) 192 192 let rec arg_decision_rect_Type2 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function 193  Arg_decision_colour x_21 831 > h_arg_decision_colour x_21831194  Arg_decision_spill x_21 832 > h_arg_decision_spill x_21832195  Arg_decision_imm x_21 833 > h_arg_decision_imm x_21833193  Arg_decision_colour x_21957 > h_arg_decision_colour x_21957 194  Arg_decision_spill x_21958 > h_arg_decision_spill x_21958 195  Arg_decision_imm x_21959 > h_arg_decision_imm x_21959 196 196 197 197 (** val arg_decision_rect_Type1 : … … 199 199 arg_decision > 'a1 **) 200 200 let rec arg_decision_rect_Type1 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function 201  Arg_decision_colour x_21 838 > h_arg_decision_colour x_21838202  Arg_decision_spill x_21 839 > h_arg_decision_spill x_21839203  Arg_decision_imm x_21 840 > h_arg_decision_imm x_21840201  Arg_decision_colour x_21964 > h_arg_decision_colour x_21964 202  Arg_decision_spill x_21965 > h_arg_decision_spill x_21965 203  Arg_decision_imm x_21966 > h_arg_decision_imm x_21966 204 204 205 205 (** val arg_decision_rect_Type0 : … … 207 207 arg_decision > 'a1 **) 208 208 let rec arg_decision_rect_Type0 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function 209  Arg_decision_colour x_21 845 > h_arg_decision_colour x_21845210  Arg_decision_spill x_21 846 > h_arg_decision_spill x_21846211  Arg_decision_imm x_21 847 > h_arg_decision_imm x_21847209  Arg_decision_colour x_21971 > h_arg_decision_colour x_21971 210  Arg_decision_spill x_21972 > h_arg_decision_spill x_21972 211  Arg_decision_imm x_21973 > h_arg_decision_imm x_21973 212 212 213 213 (** val arg_decision_inv_rect_Type4 : … … 340 340 341 341 (** val get_stack : 342 AST.ident List.list > I8051.register > Nat.nat > Joint.joint_seq 343 List.list **) 344 let get_stack globals r off = 345 List.append (set_dp_by_offset globals off) 342 AST.ident List.list > Nat.nat > I8051.register > Nat.nat > 343 Joint.joint_seq List.list **) 344 let get_stack globals localss r off = 345 let off0 = Nat.plus localss off in 346 List.append (set_dp_by_offset globals off0) 346 347 (List.append (List.Cons ((Joint.LOAD ((Obj.magic a), 347 348 (Obj.magic Types.It), (Obj.magic Types.It))), List.Nil)) … … 353 354 354 355 (** val set_stack_not_a : 355 AST.ident List.list > Nat.nat > I8051.register > Joint.joint_seq 356 List.list **) 357 let set_stack_not_a globals off r = 358 List.append (set_dp_by_offset globals off) (List.Cons ((Joint.MOVE 356 AST.ident List.list > Nat.nat > Nat.nat > I8051.register > 357 Joint.joint_seq List.list **) 358 let set_stack_not_a globals localss off r = 359 let off0 = Nat.plus localss off in 360 List.append (set_dp_by_offset globals off0) (List.Cons ((Joint.MOVE 359 361 (Obj.magic (Joint_LTL_LIN.To_acc (a, r)))), (List.Cons ((Joint.STORE 360 362 ((Obj.magic Types.It), (Obj.magic Types.It), (Obj.magic a))), … … 362 364 363 365 (** val set_stack_a : 364 AST.ident List.list > Nat.nat > Joint.joint_seq List.list **)365 let set_stack_a globals off =366 AST.ident List.list > Nat.nat > Nat.nat > Joint.joint_seq List.list **) 367 let set_stack_a globals localss off = 366 368 List.append (List.Cons ((Joint.MOVE 367 369 (Obj.magic (Joint_LTL_LIN.From_acc (I8051.registerST1, a)))), List.Nil)) 368 (set_stack_not_a globals off I8051.registerST1)370 (set_stack_not_a globals localss off I8051.registerST1) 369 371 370 372 (** val set_stack : 371 AST.ident List.list > Nat.nat > I8051.register > Joint.joint_seq372 List.list **)373 let set_stack globals off r =373 AST.ident List.list > Nat.nat > Nat.nat > I8051.register > 374 Joint.joint_seq List.list **) 375 let set_stack globals localss off r = 374 376 match I8051.eq_Register r I8051.RegisterA with 375  Bool.True > set_stack_a globals off376  Bool.False > set_stack_not_a globals off r377  Bool.True > set_stack_a globals localss off 378  Bool.False > set_stack_not_a globals localss off r 377 379 378 380 (** val set_stack_int : 379 AST.ident List.list > Nat.nat > BitVector.byte > Joint.joint_seq 380 List.list **) 381 let set_stack_int globals off int = 382 List.append (set_dp_by_offset globals off) (List.Cons ((Joint.MOVE 381 AST.ident List.list > Nat.nat > Nat.nat > BitVector.byte > 382 Joint.joint_seq List.list **) 383 let set_stack_int globals localss off int = 384 let off0 = Nat.plus localss off in 385 List.append (set_dp_by_offset globals off0) (List.Cons ((Joint.MOVE 383 386 (Obj.magic (Joint_LTL_LIN.Int_to_acc (a, int)))), (List.Cons 384 387 ((Joint.STORE ((Obj.magic Types.It), (Obj.magic Types.It), … … 386 389 387 390 (** val move : 388 AST.ident List.list > Bool.bool > Interference.decision > arg_decision389 > Joint.joint_seq List.list **)390 let move globals carry_lives_after dst src =391 AST.ident List.list > Nat.nat > Bool.bool > Interference.decision > 392 arg_decision > Joint.joint_seq List.list **) 393 let move globals localss carry_lives_after dst src = 391 394 match dst with 392 395  Interference.Decision_spill dsto > … … 394 397  Arg_decision_colour srcr > 395 398 preserve_carry_bit globals carry_lives_after 396 (set_stack globals dsto srcr)399 (set_stack globals localss dsto srcr) 397 400  Arg_decision_spill srco > 398 401 (match Nat.eqb srco dsto with … … 400 403  Bool.False > 401 404 preserve_carry_bit globals carry_lives_after 402 (List.append (get_stack globals I8051.RegisterA srco)403 (set_stack globals dsto I8051.RegisterA)))405 (List.append (get_stack globals localss I8051.RegisterA srco) 406 (set_stack globals localss dsto I8051.RegisterA))) 404 407  Arg_decision_imm int > 405 408 preserve_carry_bit globals carry_lives_after 406 (set_stack_int globals dsto int))409 (set_stack_int globals localss dsto int)) 407 410  Interference.Decision_colour dstr > 408 411 (match src with … … 428 431  Arg_decision_spill srco > 429 432 preserve_carry_bit globals carry_lives_after 430 (get_stack globals dstr srco)433 (get_stack globals localss dstr srco) 431 434  Arg_decision_imm int > 432 435 List.append (List.Cons ((Joint.MOVE … … 509 512 510 513 (** val translate_op2 : 511 AST.ident List.list > Bool.bool > BackEndOps.op2 >514 AST.ident List.list > Nat.nat > Bool.bool > BackEndOps.op2 > 512 515 Interference.decision > arg_decision > arg_decision > Joint.joint_seq 513 516 List.list **) 514 let translate_op2 globals carry_lives_after op dst arg1 arg2 =517 let translate_op2 globals localss carry_lives_after op dst arg1 arg2 = 515 518 List.append 516 519 (preserve_carry_bit globals … … 518 521 (Bool.orb (arg_is_spilled arg1) (arg_is_spilled arg2))) 519 522 (List.append 520 (move globals Bool.False (Interference.Decision_colour523 (move globals localss Bool.False (Interference.Decision_colour 521 524 I8051.RegisterB) arg2) 522 (move globals Bool.False (Interference.Decision_colour525 (move globals localss Bool.False (Interference.Decision_colour 523 526 I8051.RegisterA) arg1))) 524 527 (List.append (List.Cons ((Joint.OP2 (op, (Obj.magic a), (Obj.magic a), 525 528 (Obj.magic (Joint.hdw_argument_from_reg I8051.RegisterB)))), List.Nil)) 526 (move globals (Bool.andb (sets_carry op) carry_lives_after) dst529 (move globals localss (Bool.andb (sets_carry op) carry_lives_after) dst 527 530 (Arg_decision_colour I8051.RegisterA))) 528 531 529 532 (** val translate_op2_smart : 530 AST.ident List.list > Bool.bool > BackEndOps.op2 >533 AST.ident List.list > Nat.nat > Bool.bool > BackEndOps.op2 > 531 534 Interference.decision > arg_decision > arg_decision > Joint.joint_seq 532 535 List.list **) 533 let translate_op2_smart globals carry_lives_after op dst arg1 arg2 =536 let translate_op2_smart globals localss carry_lives_after op dst arg1 arg2 = 534 537 preserve_carry_bit globals 535 538 (Bool.andb (Bool.andb (Bool.notb (sets_carry op)) carry_lives_after) … … 539 542  Arg_decision_colour arg2r > 540 543 List.append 541 (move globals (uses_carry op) (Interference.Decision_colour544 (move globals localss (uses_carry op) (Interference.Decision_colour 542 545 I8051.RegisterA) arg1) 543 546 (List.append (List.Cons ((Joint.OP2 (op, (Obj.magic a), 544 547 (Obj.magic a), (Obj.magic (Joint.hdw_argument_from_reg arg2r)))), 545 548 List.Nil)) 546 (move globals (Bool.andb (sets_carry op) carry_lives_after) dst 549 (move globals localss 550 (Bool.andb (sets_carry op) carry_lives_after) dst 547 551 (Arg_decision_colour I8051.RegisterA))) 548 552  Arg_decision_spill x > … … 552 556  Arg_decision_colour arg1r > 553 557 List.append 554 (move globals (uses_carry op) (Interference.Decision_colour555 I8051.RegisterA) arg2)558 (move globals localss (uses_carry op) 559 (Interference.Decision_colour I8051.RegisterA) arg2) 556 560 (List.append (List.Cons ((Joint.OP2 (op, (Obj.magic a), 557 561 (Obj.magic a), 558 562 (Obj.magic (Joint.hdw_argument_from_reg arg1r)))), 559 563 List.Nil)) 560 (move globals (Bool.andb (sets_carry op) carry_lives_after) 561 dst (Arg_decision_colour I8051.RegisterA))) 564 (move globals localss 565 (Bool.andb (sets_carry op) carry_lives_after) dst 566 (Arg_decision_colour I8051.RegisterA))) 562 567  Arg_decision_spill x0 > 563 translate_op2 globals carry_lives_after op dst arg1 arg2568 translate_op2 globals localss carry_lives_after op dst arg1 arg2 564 569  Arg_decision_imm arg1i > 565 570 List.append 566 (move globals (uses_carry op) (Interference.Decision_colour567 I8051.RegisterA) arg2)571 (move globals localss (uses_carry op) 572 (Interference.Decision_colour I8051.RegisterA) arg2) 568 573 (List.append (List.Cons ((Joint.OP2 (op, (Obj.magic a), 569 574 (Obj.magic a), 570 575 (Obj.magic (Joint.hdw_argument_from_byte arg1i)))), 571 576 List.Nil)) 572 (move globals (Bool.andb (sets_carry op) carry_lives_after) 573 dst (Arg_decision_colour I8051.RegisterA)))) 577 (move globals localss 578 (Bool.andb (sets_carry op) carry_lives_after) dst 579 (Arg_decision_colour I8051.RegisterA)))) 574 580  Bool.False > 575 translate_op2 globals carry_lives_after op dst arg1 arg2)581 translate_op2 globals localss carry_lives_after op dst arg1 arg2) 576 582  Arg_decision_imm arg2i > 577 583 List.append 578 (move globals (uses_carry op) (Interference.Decision_colour584 (move globals localss (uses_carry op) (Interference.Decision_colour 579 585 I8051.RegisterA) arg1) 580 586 (List.append (List.Cons ((Joint.OP2 (op, (Obj.magic a), 581 587 (Obj.magic a), (Obj.magic (Joint.hdw_argument_from_byte arg2i)))), 582 588 List.Nil)) 583 (move globals (Bool.andb (sets_carry op) carry_lives_after) dst 589 (move globals localss 590 (Bool.andb (sets_carry op) carry_lives_after) dst 584 591 (Arg_decision_colour I8051.RegisterA)))) 585 592 … … 644 651 645 652 (** val translate_op1 : 646 AST.ident List.list > Bool.bool > BackEndOps.op1 >653 AST.ident List.list > Nat.nat > Bool.bool > BackEndOps.op1 > 647 654 Interference.decision > Interference.decision > Joint.joint_seq 648 655 List.list **) 649 let translate_op1 globals carry_lives_after op dst arg =656 let translate_op1 globals localss carry_lives_after op dst arg = 650 657 let preserve_carry = 651 658 Bool.andb carry_lives_after (Bool.orb (is_spilled dst) (is_spilled arg)) … … 653 660 preserve_carry_bit globals preserve_carry 654 661 (List.append 655 (move globals Bool.False (Interference.Decision_colour I8051.RegisterA)656 (dec_to_arg_dec arg)) (List.Cons ((Joint.OP1 (op,662 (move globals localss Bool.False (Interference.Decision_colour 663 I8051.RegisterA) (dec_to_arg_dec arg)) (List.Cons ((Joint.OP1 (op, 657 664 (Obj.magic Types.It), (Obj.magic Types.It))), 658 (move globals Bool.False dst (Arg_decision_colour I8051.RegisterA))))) 665 (move globals localss Bool.False dst (Arg_decision_colour 666 I8051.RegisterA))))) 659 667 660 668 (** val translate_opaccs : 661 AST.ident List.list > Bool.bool > BackEndOps.opAccs >669 AST.ident List.list > Nat.nat > Bool.bool > BackEndOps.opAccs > 662 670 Interference.decision > Interference.decision > arg_decision > 663 671 arg_decision > Joint.joint_seq List.list **) 664 let translate_opaccs globals carry_lives_after op dst1 dst2 arg1 arg2 =672 let translate_opaccs globals localss carry_lives_after op dst1 dst2 arg1 arg2 = 665 673 List.append 666 (move globals Bool.False (Interference.Decision_colour I8051.RegisterB)667 arg2)674 (move globals localss Bool.False (Interference.Decision_colour 675 I8051.RegisterB) arg2) 668 676 (List.append 669 (move globals Bool.False (Interference.Decision_colour I8051.RegisterA) 670 arg1) (List.Cons ((Joint.OPACCS (op, (Obj.magic Types.It), 671 (Obj.magic Types.It), (Obj.magic Types.It), (Obj.magic Types.It))), 677 (move globals localss Bool.False (Interference.Decision_colour 678 I8051.RegisterA) arg1) (List.Cons ((Joint.OPACCS (op, 679 (Obj.magic Types.It), (Obj.magic Types.It), (Obj.magic Types.It), 680 (Obj.magic Types.It))), 672 681 (List.append 673 (move globals Bool.False dst1 (Arg_decision_colour I8051.RegisterA)) 682 (move globals localss Bool.False dst1 (Arg_decision_colour 683 I8051.RegisterA)) 674 684 (List.append 675 (move globals Bool.False dst2 (Arg_decision_colour685 (move globals localss Bool.False dst2 (Arg_decision_colour 676 686 I8051.RegisterB)) 677 687 (match Bool.andb carry_lives_after … … 681 691 682 692 (** val move_to_dp : 683 AST.ident List.list > arg_decision > arg_decision > Joint.joint_seq684 List.list **)685 let move_to_dp globals arg1 arg2 =693 AST.ident List.list > Nat.nat > arg_decision > arg_decision > 694 Joint.joint_seq List.list **) 695 let move_to_dp globals localss arg1 arg2 = 686 696 match Bool.notb (arg_is_spilled arg1) with 687 697  Bool.True > 688 698 List.append 689 (move globals Bool.False (Interference.Decision_colour699 (move globals localss Bool.False (Interference.Decision_colour 690 700 I8051.RegisterDPH) arg2) 691 (move globals Bool.False (Interference.Decision_colour701 (move globals localss Bool.False (Interference.Decision_colour 692 702 I8051.RegisterDPL) arg1) 693 703  Bool.False > … … 695 705  Bool.True > 696 706 List.append 697 (move globals Bool.False (Interference.Decision_colour707 (move globals localss Bool.False (Interference.Decision_colour 698 708 I8051.RegisterDPL) arg1) 699 (move globals Bool.False (Interference.Decision_colour709 (move globals localss Bool.False (Interference.Decision_colour 700 710 I8051.RegisterDPH) arg2) 701 711  Bool.False > 702 712 List.append 703 (move globals Bool.False (Interference.Decision_colour713 (move globals localss Bool.False (Interference.Decision_colour 704 714 I8051.RegisterB) arg1) 705 715 (List.append 706 (move globals Bool.False (Interference.Decision_colour716 (move globals localss Bool.False (Interference.Decision_colour 707 717 I8051.RegisterDPH) arg2) 708 (move globals Bool.False (Interference.Decision_colour718 (move globals localss Bool.False (Interference.Decision_colour 709 719 I8051.RegisterDPL) (Arg_decision_colour I8051.RegisterB)))) 710 720 711 721 (** val translate_store : 712 AST.ident List.list > Bool.bool > arg_decision> arg_decision >713 arg_decision > Joint.joint_seq List.list **)714 let translate_store globals carry_lives_after addr1 addr2 src =722 AST.ident List.list > Nat.nat > Bool.bool > arg_decision > 723 arg_decision > arg_decision > Joint.joint_seq List.list **) 724 let translate_store globals localss carry_lives_after addr1 addr2 src = 715 725 preserve_carry_bit globals 716 726 (Bool.andb carry_lives_after 717 727 (Bool.orb (Bool.orb (arg_is_spilled addr1) (arg_is_spilled addr1)) 718 728 (arg_is_spilled src))) 719 (let move_to_dptr = move_to_dp globals addr1 addr2 in729 (let move_to_dptr = move_to_dp globals localss addr1 addr2 in 720 730 List.append 721 731 (match arg_is_spilled src with 722 732  Bool.True > 723 733 List.append 724 (move globals Bool.False (Interference.Decision_colour734 (move globals localss Bool.False (Interference.Decision_colour 725 735 I8051.registerST0) src) 726 736 (List.append move_to_dptr (List.Cons ((Joint.MOVE … … 732 742 733 743 (** val translate_load : 734 AST.ident List.list > Bool.bool > Interference.decision > arg_decision735 > arg_decision > Joint.joint_seq List.list **)736 let translate_load globals carry_lives_after dst addr1 addr2 =744 AST.ident List.list > Nat.nat > Bool.bool > Interference.decision > 745 arg_decision > arg_decision > Joint.joint_seq List.list **) 746 let translate_load globals localss carry_lives_after dst addr1 addr2 = 737 747 preserve_carry_bit globals 738 748 (Bool.andb carry_lives_after 739 749 (Bool.orb (Bool.orb (is_spilled dst) (arg_is_spilled addr1)) 740 750 (arg_is_spilled addr1))) 741 (List.append (move_to_dp globals addr1 addr2)751 (List.append (move_to_dp globals localss addr1 addr2) 742 752 (List.append (List.Cons ((Joint.LOAD ((Obj.magic a), 743 753 (Obj.magic Types.It), (Obj.magic Types.It))), List.Nil)) 744 (move globals Bool.False dst (Arg_decision_colour I8051.RegisterA)))) 754 (move globals localss Bool.False dst (Arg_decision_colour 755 I8051.RegisterA)))) 745 756 746 757 (** val translate_address : 747 __ List.list > Bool.bool > __ > Interference.decision >758 __ List.list > Nat.nat > Bool.bool > __ > Interference.decision > 748 759 Interference.decision > Joint.joint_seq List.list **) 749 let translate_address globals carry_lives_after id addr1 addr2 =760 let translate_address globals localss carry_lives_after id addr1 addr2 = 750 761 preserve_carry_bit (Obj.magic globals) 751 762 (Bool.andb carry_lives_after … … 754 765 (Obj.magic Types.It))), 755 766 (List.append 756 (move (Obj.magic globals) Bool.False addr1 (Arg_decision_colour767 (move (Obj.magic globals) localss Bool.False addr1 (Arg_decision_colour 757 768 I8051.RegisterDPL)) 758 (move (Obj.magic globals) Bool.False addr2 (Arg_decision_colour769 (move (Obj.magic globals) localss Bool.False addr2 (Arg_decision_colour 759 770 I8051.RegisterDPH))))) 760 771 761 772 (** val translate_low_address : 762 AST.ident List.list > Bool.bool > Interference.decision > Graphs.label763 > Joint.joint_seq List.list **)764 let translate_low_address globals carry_lives_after dst lbl =773 AST.ident List.list > Nat.nat > Bool.bool > Interference.decision > 774 Graphs.label > Joint.joint_seq List.list **) 775 let translate_low_address globals localss carry_lives_after dst lbl = 765 776 match dst with 766 777  Interference.Decision_spill x > 767 778 List.Cons ((Joint.Extension_seq 768 779 (Obj.magic (Joint_LTL_LIN.LOW_ADDRESS (I8051.RegisterA, lbl)))), 769 (move globals carry_lives_after dst (Arg_decision_colour780 (move globals localss carry_lives_after dst (Arg_decision_colour 770 781 I8051.RegisterA))) 771 782  Interference.Decision_colour r > … … 774 785 775 786 (** val translate_high_address : 776 AST.ident List.list > Bool.bool > Interference.decision > Graphs.label777 > Joint.joint_seq List.list **)778 let translate_high_address globals carry_lives_after dst lbl =787 AST.ident List.list > Nat.nat > Bool.bool > Interference.decision > 788 Graphs.label > Joint.joint_seq List.list **) 789 let translate_high_address globals localss carry_lives_after dst lbl = 779 790 match dst with 780 791  Interference.Decision_spill x > 781 792 List.Cons ((Joint.Extension_seq 782 793 (Obj.magic (Joint_LTL_LIN.HIGH_ADDRESS (I8051.RegisterA, lbl)))), 783 (move globals carry_lives_after dst (Arg_decision_colour794 (move globals localss carry_lives_after dst (Arg_decision_colour 784 795 I8051.RegisterA))) 785 796  Interference.Decision_colour r > … … 788 799 789 800 (** val translate_step : 790 AST.ident List.list > Fixpoints.valuation > Interference.coloured_graph 791 > Nat.nat > Graphs.label > Joint.joint_step > Blocks.bind_step_block **) 792 let translate_step globals after grph stack_sz lbl s = 801 AST.ident List.list > Nat.nat > Fixpoints.valuation > 802 Interference.coloured_graph > Nat.nat > Graphs.label > 803 Joint.joint_step > Blocks.bind_step_block **) 804 let translate_step globals localss after grph stack_sz lbl s = 793 805 Bind_new.Bret 794 806 (let lookup = fun r > grph.Interference.colouring (Types.Inl r) in … … 800 812 let carry_lives_after = Liveness.hlives I8051.RegisterCarry (after lbl) 801 813 in 802 let move0 = move globals carry_lives_after in814 let move0 = move globals localss carry_lives_after in 803 815 (match s with 804 816  Joint.COST_LABEL cost_lbl > … … 815 827 { Types.fst = { Types.fst = 816 828 (Blocks.add_dummy_variance 817 (move_to_dp globals (Obj.magic lookup_arg dpl)829 (move_to_dp globals localss (Obj.magic lookup_arg dpl) 818 830 (Obj.magic lookup_arg dph))); Types.snd = (fun x0 > Joint.CALL 819 831 ((Types.Inr { Types.fst = (Obj.magic Types.It); Types.snd = … … 860 872 Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL) 861 873 globals 862 (translate_address (Obj.magic globals) carry_lives_after874 (translate_address (Obj.magic globals) localss carry_lives_after 863 875 (Obj.magic lbl0) (Obj.magic lookup dpl) (Obj.magic lookup dph)) 864 876  Joint.OPACCS (op, dst1, dst2, arg1, arg2) > 865 877 Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL) 866 878 globals 867 (translate_opaccs globals carry_lives_after op879 (translate_opaccs globals localss carry_lives_after op 868 880 (Obj.magic lookup dst1) (Obj.magic lookup dst2) 869 881 (Obj.magic lookup_arg arg1) (Obj.magic lookup_arg arg2)) … … 871 883 Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL) 872 884 globals 873 (translate_op1 globals carry_lives_after op885 (translate_op1 globals localss carry_lives_after op 874 886 (Obj.magic lookup dst) (Obj.magic lookup arg)) 875 887  Joint.OP2 (op, dst, arg1, arg2) > 876 888 Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL) 877 889 globals 878 (translate_op2_smart globals carry_lives_after op890 (translate_op2_smart globals localss carry_lives_after op 879 891 (Obj.magic lookup dst) (Obj.magic lookup_arg arg1) 880 892 (Obj.magic lookup_arg arg2)) … … 888 900 Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL) 889 901 globals 890 (translate_load globals carry_lives_after (Obj.magic lookup dstr) 891 (Obj.magic lookup_arg addr1) (Obj.magic lookup_arg addr2)) 902 (translate_load globals localss carry_lives_after 903 (Obj.magic lookup dstr) (Obj.magic lookup_arg addr1) 904 (Obj.magic lookup_arg addr2)) 892 905  Joint.STORE (addr1, addr2, srcr) > 893 906 Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL) 894 907 globals 895 (translate_store globals carry_lives_after908 (translate_store globals localss carry_lives_after 896 909 (Obj.magic lookup_arg addr1) (Obj.magic lookup_arg addr2) 897 910 (Obj.magic lookup_arg srcr)) … … 908 921 (Joint.byte_of_nat stack_sz))) 909 922  ERTLptr.LOW_ADDRESS (r1, l) > 910 translate_low_address globals carry_lives_after (lookup r1) l 923 translate_low_address globals localss carry_lives_after 924 (lookup r1) l 911 925  ERTLptr.HIGH_ADDRESS (r1, l) > 912 translate_high_address globals carry_lives_after (lookup r1) l)))) 926 translate_high_address globals localss carry_lives_after 927 (lookup r1) l)))) 913 928 914 929 (** val translate_fin_step : … … 939 954 TranslateUtils.init_params = (Obj.magic Types.It); 940 955 TranslateUtils.init_stack_size = stack_sz; TranslateUtils.added_prologue = 941 List.Nil; TranslateUtils.f_step = 942 (translate_step globals after coloured_graph stack_sz); 943 TranslateUtils.f_fin = (translate_fin_step globals) } 944 945 (** val first_free_stack_addr : LTL.ltl_program > Nat.nat **) 946 let first_free_stack_addr p = 947 let globals_addr_internal = fun offset x_size > 948 let { Types.fst = eta4401; Types.snd = size } = x_size in 949 let { Types.fst = x; Types.snd = region } = eta4401 in 950 Nat.plus offset size 951 in 952 Util.foldl globals_addr_internal Nat.O p.AST.prog_vars 956 List.Nil; TranslateUtils.new_regs = List.Nil; TranslateUtils.f_step = 957 (translate_step globals (Types.pi1 int_fun).Joint.joint_if_local_stacksize 958 after coloured_graph stack_sz); TranslateUtils.f_fin = 959 (translate_fin_step globals) } 953 960 954 961 (** val ertlptr_to_ltl : … … 959 966 let ltlprog = 960 967 TranslateUtils.b_graph_transform_program ERTLptr.eRTLptr LTL.lTL 961 ( translate_data the_fixpoint build) pr968 (fun globals h > translate_data the_fixpoint build globals h) pr 962 969 in 963 970 { Types.fst = { Types.fst = ltlprog; Types.snd = … … 967 974 (Exp.exp (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 968 975 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 969 Nat.O))))))))))))))))) (first_free_stack_addr ltlprog)) } 970 976 Nat.O))))))))))))))))) 977 (Joint.globals_stacksize (Joint.graph_params_to_params LTL.lTL) ltlprog)) } 978
Note: See TracChangeset
for help on using the changeset viewer.