Changeset 1064 for src/RTLabs/RTLAbstoRTL.ma
 Timestamp:
 Jul 12, 2011, 5:52:07 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/RTLAbstoRTL.ma
r1063 r1064 125 125 〈〈srcrs1 @ added_regs, srcrs2〉, added_regs〉. 126 126 127 (* obvious, but proof doesn't look easy! *) 128 axiom complete_regs_length: 129 ∀def. 130 ∀left. 131 ∀right. 132 \fst (\fst (complete_regs def left right)) = \snd (\fst (complete_regs def left right)). 133 127 134 definition size_of_sig_type ≝ 128 135 λsig. … … 240 247  rtl_st_op1 op1 d s _ ⇒ rtl_st_op1 op1 d s lbl 241 248  rtl_st_op2 op2 d s1 s2 _ ⇒ rtl_st_op2 op2 d s1 s2 lbl 242  rtl_st_clear_carry _ ⇒ rtl_st_clear_carry lbl243 249  rtl_st_load d a1 a2 _ ⇒ rtl_st_load d a1 a2 lbl 244 250  rtl_st_store a1 a2 s _ ⇒ rtl_st_store a1 a2 s lbl … … 460 466 ]. 461 467 462 definition translate_intermediate_op1 ≝ 463 λop1. 464 λdestrs. 465 λsrcrs. 466 λstart_lbl. 467 λdest_lbl. 468 λdef. 468 definition translate_op1 ≝ 469 λop1: op1. 470 λdestrs: list register. 471 λsrcrs: list register. 469 472 λprf: destrs = srcrs. 473 λstart_lbl: label. 474 λdest_lbl: label. 475 λdef: rtl_internal_function. 470 476 match op1 with 471 [ intermediate_op1_cast src_size src_sign dest_size ⇒477 [ op_cast src_size src_sign dest_size ⇒ 472 478 translate_cast src_size src_sign dest_size destrs srcrs start_lbl dest_lbl def 473  intermediate_op1_negint ⇒479  op_neg_int ⇒ 474 480 translate_negint destrs srcrs start_lbl dest_lbl def prf 475  intermediate_op1_notbool ⇒481  op_not_bool ⇒ 476 482 translate_notbool destrs srcrs start_lbl dest_lbl def 477  intermediate_op1_notint ⇒483  op_not_int ⇒ 478 484 let f ≝ λdestr. λsrcr. rtl_st_op1 Cmpl destr srcr start_lbl in 479 485 let l ≝ map2 … f destrs srcrs prf in 480 486 adds_graph l start_lbl dest_lbl def 481  intermediate_op1_ptrofint ⇒487  op_ptr_of_int ⇒ 482 488 translate_move destrs srcrs start_lbl dest_lbl def 483  intermediate_op1_intofptr ⇒489  op_int_of_ptr ⇒ 484 490 translate_move destrs srcrs start_lbl dest_lbl def 485  intermediate_op1_id ⇒491  op_id ⇒ 486 492 translate_move destrs srcrs start_lbl dest_lbl def 487 493 ]. … … 618 624 translates @ tmp_destrs2'. 619 625 626 axiom translate_mul: 627 ∀destrs: list register. 628 ∀srcrs1: list register. 629 ∀srcrs2: list register. 630 ∀start_lbl: label. 631 ∀dest_lbl: label. 632 ∀def: rtl_internal_function. 633 rtl_internal_function. 634 635 (* 620 636 definition translate_mul ≝ 621 637 λdestrs: list register. … … 639 655 let insts_mul ≝ foldi ? ? [ ] srcrs2 in ?. [5: check insts_init. 640 656 add_translates (insts_init @ insts_mul) start_lbl dest_lbl def. 641 642 let translate_mul destrs srcrs1 srcrs2 start_lbl dest_lbl def = 643 let (def, dummy) = fresh_reg def in 644 let (def, tmpr) = fresh_reg def in 645 let (def, tmp_destrs) = fresh_regs def (List.length destrs) in 646 let (def, fresh_srcrs1) = fresh_regs def (List.length srcrs1) in 647 let (def, fresh_srcrs2) = fresh_regs def (List.length srcrs2) in 648 let insts_init = 649 [translate_move fresh_srcrs1 srcrs1 ; 650 translate_move fresh_srcrs2 srcrs2 ; 651 translate_cst (AST.Cst_int 0) destrs] in 652 let f = λi. translate_muli dummy tmpr destrs tmp_destrs fresh_srcrs1 start_lbl i ? in 653 let insts_mul = MiscPottier.foldi f [] srcrs2 in 654 add_translates (insts_init @ insts_mul) start_lbl dest_lbl def 657 *) 658 659 definition translate_divumodu8 ≝ 660 λorder: bool. 661 λdestrs: list register. 662 λsrcr1: register. 663 λsrcr2: register. 664 λstart_lbl: label. 665 λdest_lbl: label. 666 λdef: rtl_internal_function. 667 match destrs with 668 [ nil ⇒ add_graph start_lbl (rtl_st_skip dest_lbl) def 669  cons destr destrs ⇒ 670 let 〈def, dummy〉 ≝ fresh_reg def in 671 let 〈destr1, destr2〉 ≝ match order with [ true ⇒ 〈destr, dummy〉  _ ⇒ 〈dummy, destr〉 ] in 672 let inst_div ≝ adds_graph [ 673 rtl_st_opaccs DivuModu destr1 destr2 srcr1 srcr2 start_lbl 674 ] 675 in 676 let insts_rest ≝ translate_cst (Ointconst I8 (zero ?)) destrs in 677 add_translates [ inst_div; insts_rest ] start_lbl dest_lbl def 678 ]. 679 680 definition translate_ne: ? → ? → ? → ? → ? → ? → rtl_internal_function ≝ 681 λdestrs: list register. 682 λsrcrs1: list register. 683 λsrcrs2: list register. 684 λstart_lbl: label. 685 λdest_lbl: label. 686 λdef: rtl_internal_function. 687 match destrs with 688 [ nil ⇒ add_graph start_lbl (rtl_st_skip dest_lbl) def 689  cons destr destrs ⇒ 690 let 〈def, tmpr〉 ≝ fresh_reg def in 691 let 〈def, tmp_zero〉 ≝ fresh_reg def in 692 let 〈def, tmp_srcrs1〉 ≝ fresh_regs def (srcrs1) in 693 let save_srcrs1 ≝ translate_move tmp_srcrs1 srcrs1 in 694 let 〈def, tmp_srcrs2〉 ≝ fresh_regs def (srcrs2) in 695 let save_srcrs2 ≝ translate_move tmp_srcrs2 srcrs2 in 696 match reduce_strong ? tmp_srcrs1 tmp_srcrs2 with 697 [ dp crl their_proof ⇒ 698 let commonl ≝ \fst (\fst crl) in 699 let commonr ≝ \fst (\snd crl) in 700 let restl ≝ \snd (\snd crl) in 701 let restr ≝ \snd (\snd crl) in 702 let rest ≝ choose_rest ? restl restr ? ? in 703 let inits ≝ [ 704 rtl_st_int destr (zero ?) start_lbl; 705 rtl_st_int tmp_zero (zero ?) start_lbl 706 ] 707 in 708 let f_common ≝ λtmp_srcr1. λtmp_srcr2. [ 709 rtl_st_clear_carry start_lbl; 710 rtl_st_op2 Sub tmpr tmp_srcr1 tmp_srcr2 start_lbl; 711 rtl_st_op2 Or destr destr tmpr start_lbl 712 ] 713 in 714 let insts_common ≝ flatten ? (map2 … f_common commonl commonr ?) in 715 let f_rest ≝ λtmp_srcr. [ 716 rtl_st_clear_carry start_lbl; 717 rtl_st_op2 Sub tmpr tmp_zero tmp_srcr start_lbl; 718 rtl_st_op2 Or destr destr tmpr start_lbl 719 ] 720 in 721 let insts_rest ≝ flatten ? (map ? ? f_rest rest) in 722 let insts ≝ inits @ insts_common @ insts_rest in 723 let epilogue ≝ translate_cst (Ointconst I8 (zero ?)) destrs in 724 add_translates [ 725 save_srcrs1; save_srcrs2; adds_graph insts; epilogue 726 ] start_lbl dest_lbl def 727 ] 728 ]. 729 [1: @their_proof 730 *: cases not_implemented (* choose rest requires nonemptiness proofs but 731 these appear impossible to obtain, similar proof 732 to above *) 733 ] 734 qed. 735 736 definition translate_eq_reg ≝ 737 λtmp_zero: register. 738 λtmp_one: register. 739 λtmpr1: register. 740 λtmpr2: register. 741 λdestr: register. 742 λdummy_lbl: label. 743 λsrcr12: register × register. 744 let 〈srcr1, srcr2〉 ≝ srcr12 in 745 [ rtl_st_clear_carry dummy_lbl; 746 rtl_st_op2 Sub tmpr1 srcr1 srcr2 dummy_lbl; 747 rtl_st_op2 Addc tmpr1 tmp_zero tmp_zero dummy_lbl; 748 rtl_st_op2 Sub tmpr2 srcr2 srcr1 dummy_lbl; 749 rtl_st_op2 Addc tmpr2 tmp_zero tmp_zero dummy_lbl; 750 rtl_st_op2 Or tmpr1 tmpr1 tmpr2 dummy_lbl; 751 rtl_st_op2 Xor tmpr1 tmpr1 tmp_one dummy_lbl; 752 rtl_st_op2 And destr destr tmpr1 dummy_lbl ]. 753 754 definition translate_eq_list ≝ 755 λtmp_zero: register. 756 λtmp_one: register. 757 λtmpr1: register. 758 λtmpr2: register. 759 λdestr: register. 760 λleq: list (register × register). 761 λdummy_lbl: label. 762 let f ≝ translate_eq_reg tmp_zero tmp_one tmpr1 tmpr2 destr dummy_lbl in 763 (rtl_st_int destr (bitvector_of_nat ? 1) dummy_lbl) :: 764 flatten ? (map ? ? f leq). 765 766 definition translate_atom ≝ 767 λtmp_zero: register. 768 λtmp_one: register. 769 λtmpr1: register. 770 λtmpr2: register. 771 λtmpr3: register. 772 λdestr: register. 773 λdummy_lbl: label. 774 λleq: list (register × register). 775 λsrcr1: register. 776 λsrcr2: register. 777 translate_eq_list tmp_zero tmp_one tmpr1 tmpr2 tmpr3 leq dummy_lbl @ 778 [ rtl_st_clear_carry dummy_lbl; 779 rtl_st_op2 Sub tmpr1 srcr1 srcr2 dummy_lbl; 780 rtl_st_op2 Addc tmpr1 tmp_zero tmp_zero dummy_lbl; 781 rtl_st_op2 And tmpr3 tmpr3 tmpr1 dummy_lbl; 782 rtl_st_op2 Or destr destr tmpr3 dummy_lbl ]. 783 784 definition translate_lt_main ≝ 785 λtmp_zero: register. 786 λtmp_one: register. 787 λtmpr1: register. 788 λtmpr2: register. 789 λtmpr3: register. 790 λdestr: register. 791 λdummy_lbl: label. 792 λsrcrs1: list register. 793 λsrcrs2: list register. 794 λproof: srcrs1 = srcrs2. 795 let f ≝ λinsts_leq. λsrcr1. λsrcr2. 796 let 〈insts, leq〉 ≝ insts_leq in 797 let added_insts ≝ translate_atom tmp_zero tmp_one tmpr1 tmpr2 tmpr3 destr dummy_lbl leq srcr1 srcr2 in 798 〈insts @ added_insts, leq @ [〈srcr1, srcr2〉]〉 799 in 800 \fst (fold_left2 ? ? ? f 〈[ ], [ ]〉 srcrs1 srcrs2 proof). 801 802 definition fresh_regs_strong: 803 rtl_internal_function → ∀n: nat. Σfresh: rtl_internal_function × (list register). \snd fresh = n ≝ 804 λdef. 805 λn. 806 fresh_regs def n. 807 @fresh_regs_length 808 qed. 809 810 definition complete_regs_strong: 811 rtl_internal_function → list register → list register → Σcomplete: (list register) × (list register) × (list register). \fst (\fst complete) = \snd (\fst complete) ≝ 812 λdef. 813 λleft. 814 λright. 815 complete_regs def left right. 816 @complete_regs_length 817 qed. 818 819 definition translate_lt ≝ 820 λdestrs: list register. 821 λprf_destrs: lt 0 (destrs). 822 λsrcrs1: list register. 823 λsrcrs2: list register. 824 λprf_srcrs: srcrs1 = srcrs2. 825 λstart_lbl: label. 826 λdest_lbl: label. 827 λdef: rtl_internal_function. 828 match destrs with 829 [ nil ⇒ add_graph start_lbl (rtl_st_skip dest_lbl) def 830  _ ⇒ 831 match fresh_regs_strong def (destrs) with 832 [ dp def_tmp_destrs tmp_destrs_proof ⇒ 833 let def ≝ \fst def_tmp_destrs in 834 let tmp_destrs ≝ \snd def_tmp_destrs in 835 let tmp_destr ≝ hd_safe ? tmp_destrs ? in 836 let 〈def, tmp_zero〉 ≝ fresh_reg def in 837 let 〈def, tmp_one〉 ≝ fresh_reg def in 838 let 〈def, tmpr1〉 ≝ fresh_reg def in 839 let 〈def, tmpr2〉 ≝ fresh_reg def in 840 let 〈def, tmpr3〉 ≝ fresh_reg def in 841 match complete_regs_strong def srcrs1 srcrs2 with 842 [ dp srcrs12_added srcrs12_proof ⇒ 843 let srcrs1 ≝ \fst (\fst srcrs12_added) in 844 let srcrs2 ≝ \snd (\fst srcrs12_added) in 845 let added ≝ \snd srcrs12_added in 846 let srcrs1' ≝ rev ? srcrs1 in 847 let srcrs2' ≝ rev ? srcrs2 in 848 let insts_init ≝ [ 849 translate_cst (Ointconst I8 (zero ?)) tmp_destrs; 850 translate_cst (Ointconst I8 (zero ?)) added; 851 adds_graph [ 852 rtl_st_int tmp_zero (zero ?) start_lbl; 853 rtl_st_int tmp_one (bitvector_of_nat ? 1) start_lbl 854 ] 855 ] 856 in 857 let insts_main ≝ 858 translate_lt_main tmp_zero tmp_one tmpr1 tmpr2 tmpr3 tmp_destr start_lbl srcrs1' srcrs2' ? in 859 let insts_main ≝ [ adds_graph insts_main ] in 860 let insts_exit ≝ [ translate_move destrs tmp_destrs ] in 861 add_translates (insts_init @ insts_main @ insts_exit) start_lbl dest_lbl def 862 ] 863 ] 864 ]. 865 [2: >tmp_destrs_proof @prf_destrs 866 1: normalize nodelta 867 generalize in match srcrs12_proof 868 #HYP >rev_length >rev_length @HYP 869 ] 870 qed. 871 872 definition add_128_to_last ≝ 873 λtmp_128: register. 874 λrs. 875 λprf: 0 < rs. 876 λstart_lbl: label. 877 match rs with 878 [ nil ⇒ adds_graph [ ] start_lbl 879  _ ⇒ 880 let r ≝ last_safe ? rs prf in 881 adds_graph [ 882 rtl_st_op2 Add r r tmp_128 start_lbl 883 ] start_lbl 884 ]. 885 886 definition translate_lts ≝ 887 λdestrs: list register. 888 λdestrs_prf: lt 0 (destrs). 889 λsrcrs1: list register. 890 λsrcrs2: list register. 891 λsrcrs_prf: srcrs1 = srcrs2. 892 λsrcrs1_lt_prf: 0 < srcrs1. 893 λstart_lbl: label. 894 λdest_lbl: label. 895 λdef: rtl_internal_function. 896 match fresh_regs_strong def (srcrs1) with 897 [ dp def_tmp_srcrs1 srcrs1_prf ⇒ 898 let def ≝ \fst def_tmp_srcrs1 in 899 let tmp_srcrs1 ≝ \snd def_tmp_srcrs1 in 900 match fresh_regs_strong def (srcrs2) with 901 [ dp def_tmp_srcrs2 srcrs2_prf ⇒ 902 let def ≝ \fst def_tmp_srcrs2 in 903 let tmp_srcrs2 ≝ \snd def_tmp_srcrs2 in 904 let 〈def, tmp_128〉 ≝ fresh_reg def in 905 add_translates [ 906 translate_move tmp_srcrs1 srcrs1; 907 translate_move tmp_srcrs2 srcrs2; 908 adds_graph [ 909 rtl_st_int tmp_128 (bitvector_of_nat ? 128) start_lbl 910 ]; 911 add_128_to_last tmp_128 tmp_srcrs1 ?; 912 add_128_to_last tmp_128 tmp_srcrs2 ?; 913 translate_lt destrs destrs_prf tmp_srcrs1 tmp_srcrs2 ? 914 ] start_lbl dest_lbl def 915 ] 916 ]. 917 [2: >srcrs2_prf >srcrs1_prf @srcrs_prf 918 3: >srcrs2_prf <srcrs_prf @srcrs1_lt_prf 919 1: >srcrs1_prf @srcrs1_lt_prf 920 ] 921 qed. 922 923 definition translate_op2 ≝ 924 λop2. 925 λdestrs: list register. 926 λdestrs_prf: lt 0 (destrs). 927 λsrcrs1: list register. 928 λsrcrs2: list register. 929 λsrcrs_prf: srcrs1 = srcrs2. 930 λstart_lbl: label. 931 λdest_lbl: label. 932 λdef: rtl_internal_function. 933 match op2 with 934 [ op_add ⇒ 935 translate_op Addc destrs srcrs1 srcrs2 srcrs_prf start_lbl dest_lbl def 936  op_addp ⇒ 937 translate_op Addc destrs srcrs1 srcrs2 srcrs_prf start_lbl dest_lbl def 938  op_sub ⇒ 939 translate_op Sub destrs srcrs1 srcrs2 srcrs_prf start_lbl dest_lbl def 940  op_subp ⇒ 941 translate_op Sub destrs srcrs1 srcrs2 srcrs_prf start_lbl dest_lbl def 942  op_subpp ⇒ 943 translate_op Sub destrs srcrs1 srcrs2 srcrs_prf start_lbl dest_lbl def 944  op_mul ⇒ 945 translate_op Mul destrs srcrs1 srcrs2 srcrs_prf start_lbl dest_lbl def 946  op_divu ⇒ ? 947  op_modu ⇒ ? 948  op_and ⇒ 949 translate_op And destrs srcrs1 srcrs2 srcrs_prf start_lbl dest_lbl def 950  op_or ⇒ 951 translate_op Or destrs srcrs1 srcrs2 srcrs_prf start_lbl dest_lbl def 952  op_xor ⇒ 953 translate_op Xor destrs srcrs1 srcrs2 srcrs_prf start_lbl dest_lbl def 954  op_cmp c ⇒ 955 match c with 956 [ Compare_Equal ⇒ 957 add_translates [ 958 translate_ne destrs srcrs1 srcrs2 start_lbl dest_lbl def; 959 translate_op1 op_not_bool destrs destrs (refl ? (destrs)) 960 ] start_lbl dest_lbl def 961  Compare_NotEqual ⇒ translate_ne destrs srcrs1 srcrs2 start_lbl dest_lbl def 962  Compare_Less ⇒ translate_lts destrs destrs_prf srcrs1 srcrs2 srcrs_prf ? start_lbl dest_lbl def 963  Compare_Greater ⇒ translate_lts destrs destrs_prf srcrs2 srcrs1 srcrs_prf ? start_lbl dest_lbl def 964  Compare_LessEqual ⇒ 965 add_translates [ 966 translate_lts destrs destrs_prf srcrs2 srcrs1 srcrs_prf ? start_lbl dest_lbl def; 967 translate_op1 op_not_bool destrs destrs (refl ? (destrs)) 968 ] start_lbl dest_lbl def 969  Compare_GreaterEqual ⇒ 970 add_translates [ 971 translate_lts destrs destrs_prf srcrs1 srcrs2 srcrs_prf ? start_lbl dest_lbl def; 972 translate_op1 op_not_bool destrs destrs (refl ? (destrs)) 973 ] start_lbl dest_lbl def 974 ] 975  _ ⇒ ? 976 ]. 977 978 let rec translate_op2 op2 destrs srcrs1 srcrs2 start_lbl dest_lbl def = 979 match op2 with 980 981  AST.Op_divu when List.length srcrs1 = 1 && List.length srcrs2 = 1 > 982 translate_divumodu8 true destrs (List.hd srcrs1) (List.hd srcrs2) 983 start_lbl dest_lbl def 984 985  AST.Op_modu when List.length srcrs1 = 1 && List.length srcrs2 = 1 > 986 translate_divumodu8 false destrs (List.hd srcrs1) (List.hd srcrs2) 987 start_lbl dest_lbl def 988 989  AST.Op_cmp AST.Cmp_eq 990  AST.Op_cmpu AST.Cmp_eq 991  AST.Op_cmpp AST.Cmp_eq > 992 add_translates 993 [translate_op2 (AST.Op_cmpu AST.Cmp_ne) destrs srcrs1 srcrs2 ; 994 translate_op1 AST.Op_notbool destrs destrs] 995 start_lbl dest_lbl def 996 997  AST.Op_cmp AST.Cmp_ne 998  AST.Op_cmpu AST.Cmp_ne 999  AST.Op_cmpp AST.Cmp_ne > 1000 translate_ne destrs srcrs1 srcrs2 start_lbl dest_lbl def 1001 1002  AST.Op_cmp AST.Cmp_lt > 1003 translate_lts destrs srcrs1 srcrs2 start_lbl dest_lbl def 1004 1005  AST.Op_cmpu AST.Cmp_lt  AST.Op_cmpp AST.Cmp_lt > 1006 translate_lt destrs srcrs1 srcrs2 start_lbl dest_lbl def 1007 1008  AST.Op_cmp AST.Cmp_le > 1009 add_translates 1010 [translate_op2 (AST.Op_cmp AST.Cmp_lt) destrs srcrs2 srcrs1 ; 1011 translate_op1 AST.Op_notbool destrs destrs] 1012 start_lbl dest_lbl def 1013 1014  AST.Op_cmpu AST.Cmp_le > 1015 add_translates 1016 [translate_op2 (AST.Op_cmpu AST.Cmp_lt) destrs srcrs2 srcrs1 ; 1017 translate_op1 AST.Op_notbool destrs destrs] 1018 start_lbl dest_lbl def 1019 1020  AST.Op_cmpp AST.Cmp_le > 1021 add_translates 1022 [translate_op2 (AST.Op_cmpp AST.Cmp_lt) destrs srcrs2 srcrs1 ; 1023 translate_op1 AST.Op_notbool destrs destrs] 1024 start_lbl dest_lbl def 1025 1026  AST.Op_cmp AST.Cmp_gt > 1027 translate_op2 (AST.Op_cmp AST.Cmp_lt) 1028 destrs srcrs2 srcrs1 start_lbl dest_lbl def 1029 1030  AST.Op_cmpu AST.Cmp_gt > 1031 translate_op2 (AST.Op_cmpu AST.Cmp_lt) 1032 destrs srcrs2 srcrs1 start_lbl dest_lbl def 1033 1034  AST.Op_cmpp AST.Cmp_gt > 1035 translate_op2 (AST.Op_cmpp AST.Cmp_lt) 1036 destrs srcrs2 srcrs1 start_lbl dest_lbl def 1037 1038  AST.Op_cmp AST.Cmp_ge > 1039 add_translates 1040 [translate_op2 (AST.Op_cmp AST.Cmp_lt) destrs srcrs1 srcrs2 ; 1041 translate_op1 AST.Op_notbool destrs destrs] 1042 start_lbl dest_lbl def 1043 1044  AST.Op_cmpu AST.Cmp_ge > 1045 add_translates 1046 [translate_op2 (AST.Op_cmpu AST.Cmp_lt) destrs srcrs1 srcrs2 ; 1047 translate_op1 AST.Op_notbool destrs destrs] 1048 start_lbl dest_lbl def 1049 1050  AST.Op_cmpp AST.Cmp_ge > 1051 add_translates 1052 [translate_op2 (AST.Op_cmpp AST.Cmp_lt) destrs srcrs1 srcrs2 ; 1053 translate_op1 AST.Op_notbool destrs destrs] 1054 start_lbl dest_lbl def 1055 1056  AST.Op_div  AST.Op_divu  AST.Op_modu  AST.Op_mod  AST.Op_shl 1057  AST.Op_shr  AST.Op_shru > 1058 (* Unsupported, should have been replaced by a runtime function. *) 1059 assert false 1060 655 1061 656 1062 definition filter_and_to_list_local_env_internal ≝ … … 863 1269 rtl_st_cond_acc tmpr lbl_true lbl_false 864 1270 ] start_lbl start_lbl def. 1271 1272 865 1273 866 1274 (*
Note: See TracChangeset
for help on using the changeset viewer.