Changeset 1872 for src/Clight/Csyntax.ma


Ignore:
Timestamp:
Apr 4, 2012, 6:48:23 PM (8 years ago)
Author:
campbell
Message:

Make binary operations in Cminor/RTLabs properly typed.
A few extra bits and pieces that help:
Separate out Clight operation classification to its own file.
Use dependently typed classification to refine the types.
Fix bug in cast simplification.
Remove memory_chunk in favour of the low-level typ, as this now contains
exactly the right amount of information (unlike in CompCert?).
Make Cminor/RTLabs comparisons produce an 8-bit result (and cast if
necessary).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Csyntax.ma

    r1599 r1872  
    591591Qed.
    592592*)
    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 64-bit integers and 128-bit 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 ptr|array , ptr|array*)
    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
    865594
    866595(* * Translating Clight types to Cminor types, function signatures,
     
    875604  | Tarray r _ _ ⇒ ASTptr r
    876605  | Tfunction _ _ ⇒ ASTptr Code
     606  | Tcomp_ptr r _ ⇒ ASTptr r
    877607  | _ ⇒ ASTint I32 Unsigned (* structs and unions shouldn't be converted? *)
    878608  ].
     
    886616  | Tarray r _ _ ⇒ Some ? (ASTptr r)
    887617  | Tfunction _ _ ⇒ Some ? (ASTptr Code)
     618  | Tcomp_ptr r _ ⇒ Some ? (ASTptr r)
    888619  | _ ⇒ None ? (* structs and unions shouldn't be converted? *)
    889620  ].
     
    895626  ].
    896627
     628
     629(* * The [access_mode] function describes how a variable of the given
     630type 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
     637We currently do not support 64-bit integers and 128-bit floats, so these
     638have an access mode of [By_nothing].
     639*)
     640
     641inductive 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
     646definition 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
    897659definition signature_of_type : typelist → type → signature ≝ λargs. λres.
    898660  mk_signature (typlist_of_typelist args) (opttyp_of_type res).
Note: See TracChangeset for help on using the changeset viewer.