Changeset 1872 for src/Clight/Csyntax.ma
 Timestamp:
 Apr 4, 2012, 6:48:23 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/Csyntax.ma
r1599 r1872 591 591 Qed. 592 592 *) 593 (* * The [access_mode] function describes how a variable of the given 594 type must be accessed: 595  [By_value ch]: access by value, i.e. by loading from the address 596 of the variable using the memory chunk [ch]; 597  [By_reference]: access by reference, i.e. by just returning 598 the address of the variable; 599  [By_nothing]: no access is possible, e.g. for the [void] type. 600 601 We currently do not support 64bit integers and 128bit floats, so these 602 have an access mode of [By_nothing]. 603 *) 604 605 inductive mode: Type[0] ≝ 606  By_value: memory_chunk → mode 607  By_reference: region → mode 608  By_nothing: mode. 609 610 definition access_mode : type → mode ≝ λty. 611 match ty with 612 [ Tint i s ⇒ 613 match i with [ I8 ⇒ 614 match s with [ Signed ⇒ By_value Mint8signed 615  Unsigned ⇒ By_value Mint8unsigned ] 616  I16 ⇒ 617 match s with [ Signed ⇒ By_value Mint16signed 618  Unsigned ⇒ By_value Mint16unsigned ] 619  I32 ⇒ By_value Mint32 ] 620  Tfloat f ⇒ match f with [ F32 ⇒ By_value Mfloat32 621  F64 ⇒ By_value Mfloat64 ] 622  Tvoid ⇒ By_nothing 623  Tpointer r _ ⇒ By_value (Mpointer r) 624  Tarray r _ _ ⇒ By_reference r 625  Tfunction _ _ ⇒ By_reference Code 626  Tstruct _ fList ⇒ By_nothing 627  Tunion _ fList ⇒ By_nothing 628  Tcomp_ptr r _ ⇒ By_value (Mpointer r) 629 ]. 630 631 (* * Classification of arithmetic operations and comparisons. 632 The following [classify_] functions take as arguments the types 633 of the arguments of an operation. They return enough information 634 to resolve overloading for this operator applications, such as 635 ``both arguments are floats'', or ``the first is a pointer 636 and the second is an integer''. These functions are used to resolve 637 overloading both in the dynamic semantics (module [Csem]) and in the 638 compiler (module [Cshmgen]). 639 *) 640 641 inductive classify_add_cases : Type[0] ≝ 642  add_case_ii: classify_add_cases (**r int , int *) 643  add_case_ff: classify_add_cases (**r float , float *) 644  add_case_pi: type → classify_add_cases (**r ptr or array, int *) 645  add_case_ip: type → classify_add_cases (**r int, ptr or array *) 646  add_default: classify_add_cases. (**r other *) 647 648 definition classify_add ≝ λty1: type. λty2: type. 649 (* 650 match ty1, ty2 with 651 [ Tint _ _, Tint _ _ ⇒ add_case_ii 652  Tfloat _, Tfloat _ ⇒ add_case_ff 653  Tpointer ty, Tint _ _ ⇒ add_case_pi ty 654  Tarray ty _, Tint _ _ ⇒ add_case_pi ty 655  Tint _ _, Tpointer ty ⇒ add_case_ip ty 656  Tint _ _, Tarray ty _ ⇒ add_case_ip ty 657  _, _ ⇒ add_default 658 ]. 659 *) 660 match ty1 with 661 [ Tint _ _ ⇒ 662 match ty2 with 663 [ Tint _ _ ⇒ add_case_ii 664  Tpointer _ ty ⇒ add_case_ip ty 665  Tarray _ ty _ ⇒ add_case_ip ty 666  _ ⇒ add_default ] 667  Tfloat _ ⇒ match ty2 with [ Tfloat _ ⇒ add_case_ff  _ ⇒ add_default ] 668  Tpointer _ ty ⇒ match ty2 with [Tint _ _ ⇒ add_case_pi ty  _ ⇒ add_default ] 669  Tarray _ ty _ ⇒ match ty2 with [Tint _ _ ⇒ add_case_pi ty  _ ⇒ add_default ] 670  _ ⇒ add_default 671 ]. 672 673 inductive classify_sub_cases : Type[0] ≝ 674  sub_case_ii: classify_sub_cases (**r int , int *) 675  sub_case_ff: classify_sub_cases (**r float , float *) 676  sub_case_pi: type → classify_sub_cases (**r ptr or array , int *) 677  sub_case_pp: type → classify_sub_cases (**r ptr or array , ptr or array *) 678  sub_default: classify_sub_cases . (**r other *) 679 680 definition classify_sub ≝ λty1: type. λty2: type. 681 (* match ty1, ty2 with 682  Tint _ _ , Tint _ _ ⇒ sub_case_ii 683  Tfloat _ , Tfloat _ ⇒ sub_case_ff 684  Tpointer ty , Tint _ _ ⇒ sub_case_pi ty 685  Tarray ty _ , Tint _ _ ⇒ sub_case_pi ty 686  Tpointer ty , Tpointer _ ⇒ sub_case_pp ty 687  Tpointer ty , Tarray _ _⇒ sub_case_pp ty 688  Tarray ty _ , Tpointer _ ⇒ sub_case_pp ty 689  Tarray ty _ , Tarray _ _ ⇒ sub_case_pp ty 690  _ ,_ ⇒ sub_default 691 end. 692 *) 693 match ty1 with 694 [ Tint _ _ ⇒ match ty2 with [ Tint _ _ ⇒ sub_case_ii  _ ⇒ sub_default ] 695  Tfloat _ ⇒ match ty2 with [ Tfloat _ ⇒ sub_case_ff  _ ⇒ sub_default ] 696  Tpointer _ ty ⇒ 697 match ty2 with 698 [ Tint _ _ ⇒ sub_case_pi ty 699  Tpointer _ _ ⇒ sub_case_pp ty 700  Tarray _ _ _ ⇒ sub_case_pp ty 701  _ ⇒ sub_default ] 702  Tarray _ ty _ ⇒ 703 match ty2 with 704 [ Tint _ _ ⇒ sub_case_pi ty 705  Tpointer _ _ ⇒ sub_case_pp ty 706  Tarray _ _ _ ⇒ sub_case_pp ty 707  _ ⇒ sub_default ] 708  _ ⇒ sub_default 709 ]. 710 711 inductive classify_mul_cases : Type[0] ≝ 712  mul_case_ii: classify_mul_cases (**r int , int *) 713  mul_case_ff: classify_mul_cases (**r float , float *) 714  mul_default: classify_mul_cases . (**r other *) 715 716 definition classify_mul ≝ λty1: type. λty2: type. 717 match ty1 with 718 [ Tint _ _ ⇒ match ty2 with [ Tint _ _ ⇒ mul_case_ii  _ ⇒ mul_default ] 719  Tfloat _ ⇒ match ty2 with [ Tfloat _ ⇒ mul_case_ff  _ ⇒ mul_default ] 720  _ ⇒ mul_default 721 ]. 722 (* 723 match ty1,ty2 with 724  Tint _ _, Tint _ _ ⇒ mul_case_ii 725  Tfloat _ , Tfloat _ ⇒ mul_case_ff 726  _,_ ⇒ mul_default 727 end. 728 *) 729 inductive classify_div_cases : Type[0] ≝ 730  div_case_I32unsi: classify_div_cases (**r unsigned int32 , int *) 731  div_case_ii: classify_div_cases (**r int , int *) 732  div_case_ff: classify_div_cases (**r float , float *) 733  div_default: classify_div_cases. (**r other *) 734 735 definition classify_32un_aux ≝ λT:Type[0].λi.λs.λr1:T.λr2:T. 736 match i with [ I32 ⇒ 737 match s with [ Unsigned ⇒ r1  _ ⇒ r2 ] 738  _ ⇒ r2 ]. 739 740 definition classify_div ≝ λty1: type. λty2: type. 741 match ty1 with 742 [ Tint i1 s1 ⇒ 743 match ty2 with 744 [ Tint i2 s2 ⇒ 745 classify_32un_aux ? i1 s1 div_case_I32unsi 746 (classify_32un_aux ? i2 s2 div_case_I32unsi div_case_ii) 747  _ ⇒ div_default ] 748  Tfloat _ ⇒ match ty2 with [ Tfloat _ ⇒ div_case_ff  _ ⇒ div_default ] 749  _ ⇒ div_default 750 ]. 751 (* 752 definition classify_div ≝ λty1: type. λty2: type. 753 match ty1,ty2 with 754  Tint I32 Unsigned, Tint _ _ ⇒ div_case_I32unsi 755  Tint _ _ , Tint I32 Unsigned ⇒ div_case_I32unsi 756  Tint _ _ , Tint _ _ ⇒ div_case_ii 757  Tfloat _ , Tfloat _ ⇒ div_case_ff 758  _ ,_ ⇒ div_default 759 end. 760 *) 761 inductive classify_mod_cases : Type[0] ≝ 762  mod_case_I32unsi: classify_mod_cases (**r unsigned I32 , int *) 763  mod_case_ii: classify_mod_cases (**r int , int *) 764  mod_default: classify_mod_cases . (**r other *) 765 766 definition classify_mod ≝ λty1:type. λty2:type. 767 match ty1 with 768 [ Tint i1 s1 ⇒ 769 match ty2 with 770 [ Tint i2 s2 ⇒ 771 classify_32un_aux ? i1 s1 mod_case_I32unsi 772 (classify_32un_aux ? i2 s2 mod_case_I32unsi mod_case_ii) 773  _ ⇒ mod_default ] 774  _ ⇒ mod_default 775 ]. 776 (* 777 Definition classify_mod (ty1: type) (ty2: type) := 778 match ty1,ty2 with 779  Tint I32 Unsigned , Tint _ _ ⇒ mod_case_I32unsi 780  Tint _ _ , Tint I32 Unsigned ⇒ mod_case_I32unsi 781  Tint _ _ , Tint _ _ ⇒ mod_case_ii 782  _ , _ ⇒ mod_default 783 end . 784 *) 785 inductive classify_shr_cases :Type[0] ≝ 786  shr_case_I32unsi: classify_shr_cases (**r unsigned I32 , int *) 787  shr_case_ii :classify_shr_cases (**r int , int *) 788  shr_default : classify_shr_cases . (**r other *) 789 790 definition classify_shr ≝ λty1: type. λty2: type. 791 match ty1 with 792 [ Tint i1 s1 ⇒ 793 match ty2 with 794 [ Tint _ _ ⇒ 795 classify_32un_aux ? i1 s1 shr_case_I32unsi shr_case_ii 796  _ ⇒ shr_default ] 797  _ ⇒ shr_default 798 ]. 799 800 (* 801 Definition classify_shr (ty1: type) (ty2: type) := 802 match ty1,ty2 with 803  Tint I32 Unsigned , Tint _ _ ⇒ shr_case_I32unsi 804  Tint _ _ , Tint _ _ ⇒ shr_case_ii 805  _ , _ ⇒ shr_default 806 end. 807 *) 808 inductive classify_cmp_cases : Type[0] ≝ 809  cmp_case_I32unsi: classify_cmp_cases (**r unsigned I32 , int *) 810  cmp_case_ii: classify_cmp_cases (**r int, int*) 811  cmp_case_pp: classify_cmp_cases (**r ptrarray , ptrarray*) 812  cmp_case_ff: classify_cmp_cases (**r float , float *) 813  cmp_default: classify_cmp_cases . (**r other *) 814 815 definition classify_cmp ≝ λty1:type. λty2:type. 816 match ty1 with 817 [ Tint i1 s1 ⇒ 818 match ty2 with 819 [ Tint i2 s2 ⇒ 820 classify_32un_aux ? i1 s1 cmp_case_I32unsi 821 (classify_32un_aux ? i2 s2 cmp_case_I32unsi cmp_case_ii) 822  _ ⇒ cmp_default ] 823  Tfloat _ ⇒ match ty2 with [ Tfloat _ ⇒ cmp_case_ff  _ ⇒ cmp_default ] 824  Tpointer _ _ ⇒ 825 match ty2 with 826 [ Tpointer _ _ ⇒ cmp_case_pp 827  Tarray _ _ _ ⇒ cmp_case_pp 828  _ ⇒ cmp_default ] 829  Tarray _ _ _ ⇒ 830 match ty2 with 831 [ Tpointer _ _ ⇒ cmp_case_pp 832  Tarray _ _ _ ⇒ cmp_case_pp 833  _ ⇒ cmp_default ] 834  _ ⇒ cmp_default 835 ]. 836 837 (* 838 Definition classify_cmp (ty1: type) (ty2: type) := 839 match ty1,ty2 with 840  Tint I32 Unsigned , Tint _ _ ⇒ cmp_case_I32unsi 841  Tint _ _ , Tint I32 Unsigned ⇒ cmp_case_I32unsi 842  Tint _ _ , Tint _ _ ⇒ cmp_case_ipip 843  Tfloat _ , Tfloat _ ⇒ cmp_case_ff 844  Tpointer _ , Tint _ _ ⇒ cmp_case_ipip 845  Tarray _ _ , Tint _ _ ⇒ cmp_case_ipip 846  Tpointer _ , Tpointer _ ⇒ cmp_case_ipip 847  Tpointer _ , Tarray _ _ ⇒ cmp_case_ipip 848  Tarray _ _ ,Tpointer _ ⇒ cmp_case_ipip 849  Tarray _ _ ,Tarray _ _ ⇒ cmp_case_ipip 850  _ , _ ⇒ cmp_default 851 end. 852 *) 853 inductive classify_fun_cases : Type[0] ≝ 854  fun_case_f: typelist → type → classify_fun_cases (**r (pointer to) function *) 855  fun_default: classify_fun_cases . (**r other *) 856 857 definition classify_fun ≝ λty: type. 858 match ty with 859 [ Tfunction args res ⇒ fun_case_f args res 860  Tpointer _ ty' ⇒ match ty' with [ Tfunction args res ⇒ fun_case_f args res 861  _ ⇒ fun_default 862 ] 863  _ ⇒ fun_default 864 ]. 593 865 594 866 595 (* * Translating Clight types to Cminor types, function signatures, … … 875 604  Tarray r _ _ ⇒ ASTptr r 876 605  Tfunction _ _ ⇒ ASTptr Code 606  Tcomp_ptr r _ ⇒ ASTptr r 877 607  _ ⇒ ASTint I32 Unsigned (* structs and unions shouldn't be converted? *) 878 608 ]. … … 886 616  Tarray r _ _ ⇒ Some ? (ASTptr r) 887 617  Tfunction _ _ ⇒ Some ? (ASTptr Code) 618  Tcomp_ptr r _ ⇒ Some ? (ASTptr r) 888 619  _ ⇒ None ? (* structs and unions shouldn't be converted? *) 889 620 ]. … … 895 626 ]. 896 627 628 629 (* * The [access_mode] function describes how a variable of the given 630 type must be accessed: 631  [By_value ch]: access by value, i.e. by loading from the address 632 of the variable using the memory chunk [ch]; 633  [By_reference]: access by reference, i.e. by just returning 634 the address of the variable; 635  [By_nothing]: no access is possible, e.g. for the [void] type. 636 637 We currently do not support 64bit integers and 128bit floats, so these 638 have an access mode of [By_nothing]. 639 *) 640 641 inductive mode: typ → Type[0] ≝ 642  By_value: ∀t:typ. mode t 643  By_reference: ∀r:region. mode (ASTptr r) 644  By_nothing: ∀t. mode t. 645 646 definition access_mode : ∀ty. mode (typ_of_type ty) ≝ λty. 647 match ty return λty. mode (typ_of_type ty) with 648 [ Tint i s ⇒ By_value (ASTint i s) 649  Tfloat sz ⇒ By_value (ASTfloat sz) 650  Tvoid ⇒ By_nothing … 651  Tpointer r _ ⇒ By_value (ASTptr r) 652  Tarray r _ _ ⇒ By_reference r 653  Tfunction _ _ ⇒ By_reference Code 654  Tstruct _ fList ⇒ By_nothing … 655  Tunion _ fList ⇒ By_nothing … 656  Tcomp_ptr r _ ⇒ By_value (ASTptr r) 657 ]. 658 897 659 definition signature_of_type : typelist → type → signature ≝ λargs. λres. 898 660 mk_signature (typlist_of_typelist args) (opttyp_of_type res).
Note: See TracChangeset
for help on using the changeset viewer.