Changeset 1872 for src/Clight


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).

Location:
src/Clight
Files:
1 added
5 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Csem.ma

    r1713 r1872  
    2727(*include "Events.ma".*)
    2828include "common/Smallstep.ma".
     29include "Clight/ClassifyOp.ma".
    2930
    3031(* * * Semantics of type-dependent operations *)
     
    117118let rec sem_add (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝
    118119  match classify_add t1 t2 with
    119   [ add_case_ii ⇒                       (**r integer addition *)
     120  [ add_case_ii _ _ ⇒                       (**r integer addition *)
    120121      match v1 with
    121122      [ Vint sz1 n1 ⇒ match v2 with
     
    124125        | _ ⇒ None ? ]
    125126      | _ ⇒ None ? ]
    126   | add_case_ff ⇒                       (**r float addition *)
     127  | add_case_ff _ ⇒                       (**r float addition *)
    127128      match v1 with
    128129      [ Vfloat n1 ⇒ match v2 with
     
    130131        | _ ⇒ None ? ]
    131132      | _ ⇒ None ? ]
    132   | add_case_pi ty ⇒                    (**r pointer plus integer *)
     133  | add_case_pi _ _ ty _ _ ⇒                    (**r pointer plus integer *)
    133134      match v1 with
    134135      [ Vptr ptr1 ⇒ match v2 with
     
    139140        | _ ⇒ None ? ]
    140141      | _ ⇒ None ? ]
    141   | add_case_ip ty ⇒                    (**r integer plus pointer *)
     142  | add_case_ip _ _ _ _ ty ⇒                    (**r integer plus pointer *)
    142143      match v1 with
    143144      [ Vint sz1 n1 ⇒ match v2 with
     
    146147        | _ ⇒ None ? ]
    147148      | _ ⇒ None ? ]
    148   | add_default ⇒ None ?
     149  | add_default _ _ ⇒ None ?
    149150].
    150151
    151152let rec sem_sub (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝
    152153  match classify_sub t1 t2 with
    153   [ sub_case_ii ⇒                (**r integer subtraction *)
     154  [ sub_case_ii _ _ ⇒                (**r integer subtraction *)
    154155      match v1 with
    155156      [ Vint sz1 n1 ⇒ match v2 with
     
    158159        | _ ⇒ None ? ]
    159160      | _ ⇒ None ? ]
    160   | sub_case_ff ⇒                (**r float subtraction *)
     161  | sub_case_ff _ ⇒                (**r float subtraction *)
    161162      match v1 with
    162163      [ Vfloat f1 ⇒ match v2 with
     
    164165        | _ ⇒ None ? ]
    165166      | _ ⇒ None ? ]
    166   | sub_case_pi ty ⇒             (**r pointer minus integer *)
     167  | sub_case_pi _ _ ty _ _ ⇒             (**r pointer minus integer *)
    167168      match v1 with
    168169      [ Vptr ptr1 ⇒ match v2 with
     
    173174        | _ ⇒ None ? ]
    174175      | _ ⇒ None ? ]
    175   | sub_case_pp ty ⇒             (**r pointer minus pointer *)
     176  | sub_case_pp _ _ _ ty _ _ ⇒             (**r pointer minus pointer *)
    176177      match v1 with
    177178      [ Vptr ptr1 ⇒ match v2 with
     
    187188      | Vnull r ⇒ match v2 with [ Vnull r' ⇒ Some ? (Vint I32 (*XXX*) (zero ?)) | _ ⇒ None ? ]
    188189      | _ ⇒ None ? ]
    189   | sub_default ⇒ None ?
     190  | sub_default _ _ ⇒ None ?
    190191  ].
    191192
    192193let rec sem_mul (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝
    193  match classify_mul t1 t2 with
    194   [ mul_case_ii
     194 match classify_aop t1 t2 with
     195  [ aop_case_ii _ _
    195196      match v1 with
    196197      [ Vint sz1 n1 ⇒ match v2 with
     
    199200        | _ ⇒ None ? ]
    200201      | _ ⇒ None ? ]
    201   | mul_case_ff
     202  | aop_case_ff _
    202203      match v1 with
    203204      [ Vfloat f1 ⇒ match v2 with
     
    205206        | _ ⇒ None ? ]
    206207      | _ ⇒ None ? ]
    207   | mul_default
     208  | aop_default _ _
    208209      None ?
    209210].
    210211
    211212let rec sem_div (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝
    212   match classify_div t1 t2 with
    213   [ div_case_I32unsi ⇒
    214       match v1 with
    215       [ Vint sz1 n1 ⇒ match v2 with
    216         [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
    217                         (λn1. option_map … (Vint ?) (division_u ? n1 n2)) (None ?)
    218         | _ ⇒ None ? ]
    219       | _ ⇒ None ? ]
    220   | div_case_ii ⇒
     213  match classify_aop t1 t2 with
     214  [ aop_case_ii _ sg ⇒
    221215      match v1 with
    222216       [ Vint sz1 n1 ⇒ match v2 with
    223          [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     217         [ Vint sz2 n2 ⇒
     218           match sg with
     219           [ Signed ⇒  intsize_eq_elim ? sz1 sz2 ? n1
    224220                         (λn1. option_map … (Vint ?) (division_s ? n1 n2)) (None ?)
     221           | Unsigned ⇒  intsize_eq_elim ? sz1 sz2 ? n1
     222                         (λn1. option_map … (Vint ?) (division_u ? n1 n2)) (None ?)
     223           ]
    225224         | _ ⇒ None ? ]
    226225      | _ ⇒ None ? ]
    227   | div_case_ff
     226  | aop_case_ff _
    228227      match v1 with
    229228      [ Vfloat f1 ⇒ match v2 with
     
    231230        | _ ⇒ None ? ]
    232231      | _ ⇒ None ? ]
    233   | div_default
     232  | aop_default _ _
    234233      None ?
    235234  ].
    236235
    237236let rec sem_mod (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝
    238   match classify_mod t1 t2 with
    239   [ mod_case_I32unsi
     237  match classify_aop t1 t2 with
     238  [ aop_case_ii sz sg
    240239      match v1 with
    241240      [ Vint sz1 n1 ⇒ match v2 with
    242         [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     241        [ Vint sz2 n2 ⇒
     242          match sg with
     243          [ Unsigned ⇒ intsize_eq_elim ? sz1 sz2 ? n1
    243244                        (λn1. option_map … (Vint ?) (modulus_u ? n1 n2)) (None ?)
    244         | _ ⇒ None ? ]
    245       | _ ⇒ None ? ]
    246   | mod_case_ii ⇒
    247       match v1 with
    248       [ Vint sz1 n1 ⇒ match v2 with
    249         [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
    250                         (λn1. option_map … (Vint ?) (modulus_s ? n1 n2)) (None ?)
    251         | _ ⇒ None ? ]
    252       | _ ⇒ None ? ]
    253   | mod_default ⇒
     245          | Signed ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     246                      (λn1. option_map … (Vint ?) (modulus_s ? n1 n2)) (None ?)
     247          ]
     248        | _ ⇒ None ? ]
     249      | _ ⇒ None ? ]
     250  | _ ⇒
    254251      None ?
    255252  ].
     
    293290
    294291let rec sem_shr (v1: val) (t1: type) (v2: val) (t2: type): option val ≝
    295   match classify_shr t1 t2 with
    296   [ shr_case_I32unsi ⇒
     292  match classify_aop t1 t2 with
     293  [ aop_case_ii _ sg ⇒
    297294      match v1 with
    298295      [ Vint sz1 n1 ⇒ match v2 with
    299296        [ Vint sz2 n2 ⇒
     297          match sg with
     298          [ Unsigned ⇒
    300299            if lt_u ? n2 (bitvector_of_nat … (bitsize_of_intsize sz1))
    301300            then Some ? (Vint ? (shift_right ?? (nat_of_bitvector … n2) n1 false))
    302301            else None ?
    303         | _ ⇒ None ? ]
    304       | _ ⇒ None ? ]
    305    | shr_case_ii =>
    306       match v1 with
    307       [ Vint sz1 n1 ⇒ match v2 with
    308         [ Vint sz2 n2 ⇒
     302          | Signed ⇒
    309303            if lt_u ? n2 (bitvector_of_nat … (bitsize_of_intsize sz1))
    310304            then Some ? (Vint ? (shift_right ?? (nat_of_bitvector … n2) n1 (head' … n1)))
    311305            else None ?
    312         | _ ⇒ None ? ]
    313       | _ ⇒ None ? ]
    314    | shr_default ⇒
     306          ]
     307        | _ ⇒ None ? ]
     308      | _ ⇒ None ? ]
     309   | _ ⇒
    315310      None ?
    316311   ].
     
    318313let rec sem_cmp_mismatch (c: comparison): option val ≝
    319314  match c with
    320   [ Ceq =>  Some ? Vfalse
    321   | Cne =>  Some ? Vtrue
    322   | _   => None ?
     315  [ Ceq   Some ? Vfalse
     316  | Cne   Some ? Vtrue
     317  | _    None ?
    323318  ].
    324319
    325320let rec sem_cmp_match (c: comparison): option val ≝
    326321  match c with
    327   [ Ceq =>  Some ? Vtrue
    328   | Cne =>  Some ? Vfalse
    329   | _   => None ?
     322  [ Ceq   Some ? Vtrue
     323  | Cne   Some ? Vfalse
     324  | _    None ?
    330325  ].
    331326 
     
    334329                  (m: mem): option val ≝
    335330  match classify_cmp t1 t2 with
    336   [ cmp_case_I32unsi
     331  [ cmp_case_ii _ sg
    337332      match v1 with
    338333      [ Vint sz1 n1 ⇒ match v2 with
    339         [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     334         [ Vint sz2 n2 ⇒
     335           match sg with
     336           [ Unsigned ⇒ intsize_eq_elim ? sz1 sz2 ? n1
    340337                        (λn1. Some ? (of_bool (cmpu_int ? c n1 n2))) (None ?)
    341         | _ ⇒ None ? ]
    342       | _ ⇒ None ? ]
    343   | cmp_case_ii ⇒
    344       match v1 with
    345       [ Vint sz1 n1 ⇒ match v2 with
    346          [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
    347                          (λn1. Some ? (of_bool (cmp_int ? c n1 n2))) (None ?)
     338           | Signed ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     339                       (λn1. Some ? (of_bool (cmp_int ? c n1 n2))) (None ?)
     340           ]
    348341         | _ ⇒ None ?
    349342         ]
    350343      | _ ⇒ None ?     
    351344      ]
    352   | cmp_case_pp
     345  | cmp_case_pp _ _ _
    353346      match v1 with
    354347      [ Vptr ptr1 ⇒
     
    370363        ]
    371364      | _ ⇒ None ? ]
    372   | cmp_case_ff
     365  | cmp_case_ff _
    373366      match v1 with
    374367      [ Vfloat f1 ⇒
     
    377370        | _ ⇒ None ? ]
    378371      | _ ⇒ None ? ]
    379   | cmp_default ⇒ None ?
     372  | cmp_default _ _ ⇒ None ?
    380373  ].
    381374
     
    499492    | inr _ ⇒ None ?
    500493    ]
    501   | By_nothing ⇒ None ?
     494  | By_nothing _ ⇒ None ?
    502495  ].
    503496cases b //
     
    513506  [ By_value chunk ⇒ storev chunk m (Vptr (mk_pointer Any loc ? ofs)) v
    514507  | By_reference _ ⇒ None ?
    515   | By_nothing ⇒ None ?
     508  | By_nothing _ ⇒ None ?
    516509  ].
    517510cases loc //
  • 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).
  • src/Clight/SimplifyCasts.ma

    r1224 r1872  
    114114            〈false, Expr (Ebinop op e1' e2') ty〉
    115115      else
    116         let 〈desired_type1, e1'〉 ≝ simplify_expr e1 ty in
    117         let 〈desired_type2, e2'〉 ≝ simplify_expr e2 ty in
     116        let 〈desired_type1, e1'〉 ≝ simplify_expr e1 (typeof e1) in
     117        let 〈desired_type2, e2'〉 ≝ simplify_expr e2 (typeof e2) in
    118118          〈type_eq ty ty', Expr (Ebinop op e1' e2') ty〉
    119119  | Ecast ty e1 ⇒
  • src/Clight/TypeComparison.ma

    r1515 r1872  
    9393λt1,t2. match type_eq_dec t1 t2 with [ inl _ ⇒ true | inr _ ⇒ false ].
    9494
     95
     96definition if_type_eq : ∀t1,t2:type. ∀P:type → type → Type[0]. P t1 t1 → P t1 t2 → P t1 t2 ≝
     97λt1,t2,P. match type_eq_dec t1 t2 return λ_. P t1 t1 → P t1 t2 → P t1 t2 with [ inl E ⇒ λx,d. x⌈P t1 t1 ↦ P t1 t2⌉ | inr _ ⇒ λx,d. d ].
     98// qed.
  • src/Clight/toCminor.ma

    r1871 r1872  
    1 include "Clight/Csyntax.ma".
    2 include "Clight/TypeComparison.ma".
     1include "Clight/ClassifyOp.ma".
    32include "basics/lists/list.ma".
    43include "Clight/fresh.ma".
     
    322321  Consistency of the type is enforced by explicit checks.
    323322*)
     323
     324(* First, how to get rid of a abstract-away pointer or array type *)
     325definition fix_ptr_type : ∀r,ty,n. expr (typ_of_type (ptr_type r ty n)) → expr (ASTptr r) ≝
     326λr,ty,n,e. e⌈expr (typ_of_type (ptr_type r ty n)) ↦ expr (ASTptr r)⌉.
     327cases n //
     328qed.
     329
    324330definition translate_add ≝
    325 λty1,e1,ty2,e2,ty'.
     331λty1,ty2,ty'.
    326332let ty1' ≝ typ_of_type ty1 in
    327333let ty2' ≝ typ_of_type ty2 in
    328 match classify_add ty1 ty2 with
    329 [ add_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Oadd e1 e2)
    330 | add_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' Oaddf e1 e2)
    331 (* XXX using the integer size for e2 as the offset's size isn't right, because
    332    if e2 produces an 8bit value then the true offset might overflow *)
    333 | add_case_pi ty ⇒
    334     match ty2' with
    335     [ ASTint sz2 _ ⇒ OK ? (Op2 ty1' ty2' ty' Oaddp e1 (Op2 ty2' ty2' ty2' Omul e2 (Cst ? (Ointconst sz2 (repr ? (sizeof ty))))))
    336     | _ ⇒ Error ? (msg TypeMismatch) (* XXX impossible *)
    337     ]
    338 | add_case_ip ty ⇒
    339     match ty1' with
    340     [ ASTint sz1 _ ⇒ OK ? (Op2 ty2' ty1' ty' Oaddp e2 (Op2 ty1' ty1' ty1' Omul e1 (Cst ? (Ointconst sz1 (repr ? (sizeof ty))))))
    341     | _ ⇒ Error ? (msg TypeMismatch) (* XXX impossible *)
    342     ]
    343 | add_default ⇒ Error ? (msg TypeMismatch)
     334match classify_add ty1 ty2 return λty1,ty2.λ_. CMexpr (typ_of_type ty1) → CMexpr (typ_of_type ty2) → res (CMexpr (typ_of_type ty')) with
     335[ add_case_ii sz sg ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Oadd ??) e1 e2)
     336| add_case_ff sz ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Oaddf sz) e1 e2)
     337(* XXX we cast up to I16 Signed to prevent overflow, but often we could use I8 *)
     338| add_case_pi n r ty sz sg ⇒
     339    λe1,e2. typ_should_eq ??? (Op2 ??? (Oaddp I16 r) (fix_ptr_type … e1) (Op2 ??? (Omul I16 Signed) (Op1 ?? (Ocastint sz sg I16 Signed) e2) (Cst ? (Ointconst I16 (repr ? (sizeof ty))))))
     340| add_case_ip n sz sg r ty ⇒
     341    λe1,e2. typ_should_eq ??? (Op2 ??? (Oaddp I16 r) (fix_ptr_type … e2) (Op2 ??? (Omul I16 Signed) (Op1 ?? (Ocastint sz sg I16 Signed) e1) (Cst ? (Ointconst I16 (repr ? (sizeof ty))))))
     342| add_default _ _ ⇒ λe1,e2. Error ? (msg TypeMismatch)
    344343].
    345344
    346345
    347346definition translate_sub ≝
    348 λty1,e1,ty2,e2,ty'.
     347λty1,ty2,ty'.
    349348let ty1' ≝ typ_of_type ty1 in
    350349let ty2' ≝ typ_of_type ty2 in
    351 match classify_sub ty1 ty2 with
    352 [ sub_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Osub e1 e2)
    353 | sub_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' Osubf e1 e2)
    354 (* XXX choosing offset sizes? *)
    355 | sub_case_pi ty ⇒ OK ? (Op2 ty1' ty2' ty' Osubpi e1 (Op2 ty2' ty2' ty2' Omul e2 (Cst ? (Ointconst I16 (repr ? (sizeof ty))))))
    356 | sub_case_pp ty ⇒
    357     match ty' with (* XXX overflow *)
    358     [ ASTint sz _ ⇒ OK ? (Op2 ty' ty' ty' Odivu (Op2 ty1' ty2' ty' (Osubpp sz) e1 e2) (Cst ? (Ointconst sz (repr ? (sizeof ty)))))
    359     | _ ⇒ Error ? (msg TypeMismatch) (* XXX impossible *)
    360     ]
    361 | sub_default ⇒ Error ? (msg TypeMismatch)
     350match classify_sub ty1 ty2 return λty1,ty2.λ_. CMexpr (typ_of_type ty1) → CMexpr (typ_of_type ty2) → res (CMexpr (typ_of_type ty')) with
     351[ sub_case_ii sz sg ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Osub ??) e1 e2)
     352| sub_case_ff sz ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Osubf sz) e1 e2)
     353(* XXX could optimise cast as above *)
     354| sub_case_pi n r ty sz sg ⇒
     355    λe1,e2. typ_should_eq ??? (Op2 ??? (Osubpi I16 r) (fix_ptr_type … e1) (Op2 ??? (Omul I16 Signed) (Op1 ?? (Ocastint sz sg I16 Signed) e2) (Cst ? (Ointconst I16 (repr ? (sizeof ty))))))
     356(* XXX check in detail? *)
     357| sub_case_pp n1 n2 r1 ty1 r2 ty2 ⇒
     358    λe1,e2. match ty' return λty'. res (CMexpr (typ_of_type ty')) with
     359    [ Tint sz sg ⇒ OK ? (Op1 ?? (Ocastint I16 Signed sz sg) (Op2 ??? (Odiv I16) (Op2 ??? (Osubpp I16 r1 r2) (fix_ptr_type … e1) (fix_ptr_type ??? e2)) (Cst ? (Ointconst I16 (repr ? (sizeof ty2))))))
     360    | _ ⇒ Error ? (msg TypeMismatch)
     361    ]
     362| sub_default _ _ ⇒ λ_.λ_. Error ? (msg TypeMismatch)
    362363].
    363364
    364365definition translate_mul ≝
    365 λty1,e1,ty2,e2,ty'.
     366λty1,ty2,ty'.
    366367let ty1' ≝ typ_of_type ty1 in
    367368let ty2' ≝ typ_of_type ty2 in
    368 match classify_mul ty1 ty2 with
    369 [ mul_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Omul e1 e2)
    370 | mul_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' Omulf e1 e2)
    371 | mul_default ⇒ Error ? (msg TypeMismatch)
     369match classify_aop ty1 ty2 return λty1,ty2.λ_. CMexpr (typ_of_type ty1) → CMexpr (typ_of_type ty2) → res (CMexpr (typ_of_type ty')) with
     370[ aop_case_ii sz sg ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Omul …) e1 e2)
     371| aop_case_ff sz ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Omulf …) e1 e2)
     372| aop_default _ _ ⇒ λ_.λ_. Error ? (msg TypeMismatch)
    372373].
    373374
    374375definition translate_div ≝
    375 λty1,e1,ty2,e2,ty'.
     376λty1,ty2,ty'.
    376377let ty1' ≝ typ_of_type ty1 in
    377378let ty2' ≝ typ_of_type ty2 in
    378 match classify_div ty1 ty2 with
    379 [ div_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' Odivu e1 e2)
    380 | div_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Odiv e1 e2)
    381 | div_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' Odivf e1 e2)
    382 | div_default ⇒ Error ? (msg TypeMismatch)
     379match classify_aop ty1 ty2 return λty1,ty2.λ_. CMexpr (typ_of_type ty1) → CMexpr (typ_of_type ty2) → res (CMexpr (typ_of_type ty')) with
     380[ aop_case_ii sz sg ⇒
     381    match sg return λsg. CMexpr (ASTint sz sg) → CMexpr (ASTint sz sg) → res (CMexpr (typ_of_type ty')) with
     382    [ Unsigned ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Odivu …) e1 e2)
     383    | Signed ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Odiv …) e1 e2)
     384    ]
     385| aop_case_ff sz ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Odivf …) e1 e2)
     386| aop_default _ _ ⇒ λ_.λ_. Error ? (msg TypeMismatch)
    383387].
    384388
    385389definition translate_mod ≝
    386 λty1,e1,ty2,e2,ty'.
     390λty1,ty2,ty'.
    387391let ty1' ≝ typ_of_type ty1 in
    388392let ty2' ≝ typ_of_type ty2 in
    389 match classify_mod ty1 ty2 with
    390 [ mod_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' Omodu e1 e2)
    391 | mod_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Omod e1 e2)
    392 | mod_default ⇒ Error ? (msg TypeMismatch)
     393match classify_aop ty1 ty2 return λty1,ty2.λ_. CMexpr (typ_of_type ty1) → CMexpr (typ_of_type ty2) → res (CMexpr (typ_of_type ty')) with
     394[ aop_case_ii sz sg ⇒
     395    match sg return λsg. CMexpr (ASTint sz sg) → CMexpr (ASTint sz sg) → res (CMexpr (typ_of_type ty')) with
     396    [ Unsigned ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Omodu …) e1 e2)
     397    | Signed ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Omod …) e1 e2)
     398    ]
     399(* no float case *)
     400| _ ⇒ λ_.λ_. Error ? (msg TypeMismatch)
    393401].
    394402
    395403definition translate_shr ≝
    396 λty1,e1,ty2,e2,ty'.
     404λty1,ty2,ty'.
    397405let ty1' ≝ typ_of_type ty1 in
    398406let ty2' ≝ typ_of_type ty2 in
    399 match classify_shr ty1 ty2 with
    400 [ shr_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' Oshru e1 e2)
    401 | shr_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Oshr e1 e2)
    402 | shr_default ⇒ Error ? (msg TypeMismatch)
     407match classify_aop ty1 ty2 return λty1,ty2.λ_. CMexpr (typ_of_type ty1) → CMexpr (typ_of_type ty2) → res (CMexpr (typ_of_type ty')) with
     408[ aop_case_ii sz sg ⇒
     409    match sg return λsg. CMexpr (ASTint sz sg) → CMexpr (ASTint sz sg) → res (CMexpr (typ_of_type ty')) with
     410    [ Unsigned ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Omodu …) e1 e2)
     411    | Signed ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Omod …) e1 e2)
     412    ]
     413(* no float case *)
     414| _ ⇒ λ_.λ_. Error ? (msg TypeMismatch)
     415].
     416
     417definition complete_cmp : ∀ty'. CMexpr (ASTint I8 Unsigned) → res (CMexpr (typ_of_type ty')) ≝
     418λty',e.
     419match ty' return λty'. res (CMexpr (typ_of_type ty')) with
     420[ Tint sz sg ⇒ OK ? (Op1 ?? (Ocastint I8 Unsigned sz sg) e)
     421| _ ⇒ Error ? (msg TypeMismatch)
    403422].
    404423
    405424definition translate_cmp ≝
    406 λc,ty1,e1,ty2,e2,ty'.
     425λc,ty1,ty2,ty'.
    407426let ty1' ≝ typ_of_type ty1 in
    408427let ty2' ≝ typ_of_type ty2 in
    409 match classify_cmp ty1 ty2 with
    410 [ cmp_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' (Ocmpu c) e1 e2)
    411 | cmp_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' (Ocmp c) e1 e2)
    412 | cmp_case_pp ⇒ OK ? (Op2 ty1' ty2' ty' (Ocmpp c) e1 e2)
    413 | cmp_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' (Ocmpf c) e1 e2)
    414 | cmp_default ⇒ Error ? (msg TypeMismatch)
     428match classify_cmp ty1 ty2 return λty1,ty2.λ_. CMexpr (typ_of_type ty1) → CMexpr (typ_of_type ty2) → res (CMexpr (typ_of_type ty')) with
     429[ cmp_case_ii sz sg ⇒
     430    match sg return λsg. CMexpr (ASTint sz sg) → CMexpr (ASTint sz sg) → res (CMexpr (typ_of_type ty')) with
     431    [ Unsigned ⇒ λe1,e2. complete_cmp ty' (Op2 ??? (Ocmpu … c) e1 e2)
     432    | Signed ⇒ λe1,e2. complete_cmp ty' (Op2 ??? (Ocmp … c) e1 e2)
     433    ]
     434| cmp_case_pp n r ty ⇒
     435    λe1,e2. complete_cmp ty' (Op2 ??? (Ocmpp … c) (fix_ptr_type … e1) (fix_ptr_type … e2))
     436| cmp_case_ff sz ⇒ λe1,e2. complete_cmp ty' (Op2 ??? (Ocmpf … c) e1 e2)
     437| cmp_default _ _ ⇒ λ_.λ_. Error ? (msg TypeMismatch)
     438].
     439
     440definition translate_misc_aop ≝
     441λty1,ty2,ty',op.
     442let ty1' ≝ typ_of_type ty1 in
     443let ty2' ≝ typ_of_type ty2 in
     444match classify_aop ty1 ty2 return λty1,ty2.λ_. CMexpr (typ_of_type ty1) → CMexpr (typ_of_type ty2) → res (CMexpr (typ_of_type ty')) with
     445[ aop_case_ii sz sg ⇒ λe1,e2. typ_should_eq ??? (Op2 ?? (ASTint sz sg) (op sz sg) e1 e2)
     446| _ ⇒ λ_.λ_. Error ? (msg TypeMismatch)
    415447].
    416448
     
    419451let ty' ≝ typ_of_type ty in
    420452match op with
    421 [ Oadd ⇒ translate_add ty1 e1 ty2 e2 ty'
    422 | Osub ⇒ translate_sub ty1 e1 ty2 e2 ty'
    423 | Omul ⇒ translate_mul ty1 e1 ty2 e2 ty'
    424 | Omod ⇒ translate_mod ty1 e1 ty2 e2 ty'
    425 | Odiv ⇒ translate_div ty1 e1 ty2 e2 ty'
    426 | Oand ⇒ OK ? (Op2 (typ_of_type ty1) (typ_of_type ty2) ty' Oand e1 e2)
    427 | Oor  ⇒ OK ? (Op2 (typ_of_type ty1) (typ_of_type ty2) ty' Oor e1 e2)
    428 | Oxor ⇒ OK ? (Op2 (typ_of_type ty1) (typ_of_type ty2) ty' Oxor e1 e2)
    429 | Oshl ⇒ OK ? (Op2 (typ_of_type ty1) (typ_of_type ty2) ty' Oshl e1 e2)
    430 | Oshr ⇒ translate_shr ty1 e1 ty2 e2 ty'
    431 | Oeq ⇒ translate_cmp Ceq ty1 e1 ty2 e2 ty'
    432 | One ⇒ translate_cmp Cne ty1 e1 ty2 e2 ty'
    433 | Olt ⇒ translate_cmp Clt ty1 e1 ty2 e2 ty'
    434 | Ogt ⇒ translate_cmp Cgt ty1 e1 ty2 e2 ty'
    435 | Ole ⇒ translate_cmp Cle ty1 e1 ty2 e2 ty'
    436 | Oge ⇒ translate_cmp Cge ty1 e1 ty2 e2 ty'
    437 ].
     453[ Oadd ⇒ translate_add ty1 ty2 ty e1 e2
     454| Osub ⇒ translate_sub ty1 ty2 ty e1 e2
     455| Omul ⇒ translate_mul ty1 ty2 ty e1 e2
     456| Omod ⇒ translate_mod ty1 ty2 ty e1 e2
     457| Odiv ⇒ translate_div ty1 ty2 ty e1 e2
     458| Oand ⇒ translate_misc_aop ty1 ty2 ty Oand e1 e2
     459| Oor  ⇒ translate_misc_aop ty1 ty2 ty Oor e1 e2
     460| Oxor ⇒ translate_misc_aop ty1 ty2 ty Oxor e1 e2
     461| Oshl ⇒ translate_misc_aop ty1 ty2 ty Oshl e1 e2
     462| Oshr ⇒ translate_shr ty1 ty2 ty e1 e2
     463| Oeq ⇒ translate_cmp Ceq ty1 ty2 ty e1 e2
     464| One ⇒ translate_cmp Cne ty1 ty2 ty e1 e2
     465| Olt ⇒ translate_cmp Clt ty1 ty2 ty e1 e2
     466| Ogt ⇒ translate_cmp Cgt ty1 ty2 ty e1 e2
     467| Ole ⇒ translate_cmp Cle ty1 ty2 ty e1 e2
     468| Oge ⇒ translate_cmp Cge ty1 ty2 ty e1 e2
     469].
     470
     471lemma typ_equals : ∀t1,t2. ∀P:∀t. expr t → Prop. ∀v1,v2.
     472  typ_should_eq t1 t2 expr v1 = OK ? v2 →
     473  P t1 v1 →
     474  P t2 v2.
     475* [ * * | * | * ]
     476* try * try *
     477#P #v1 #v2 #E whd in E:(??%?); destruct
     478#H @H
     479qed.
     480
     481lemma unfix_ptr_type : ∀r,ty,n,e.∀P:∀t. expr t → Prop.
     482  P (typ_of_type (ptr_type r ty n)) e →
     483  P (ASTptr r) (fix_ptr_type r ty n e).
     484#r #ty * [ 2: #n ] #e #P #H @H
     485qed.
    438486
    439487(* Recall that [expr_vars], defined in Cminor/Syntax.ma, asserts a predicate on
     
    442490  a proof that all variables of [translate_binop op _ e1 _ e2 _] satisfy this
    443491  predicate. *)
     492
    444493lemma translate_binop_vars : ∀P,op,ty1,e1,ty2,e2,ty,e.
    445494  expr_vars ? e1 P →
     
    449498#P * #ty1 #e1 #ty2 #e2 #ty #e #H1 #H2
    450499whd in ⊢ (??%? → ?);
    451 [ cases (classify_add ty1 ty2)
    452   [ 3,4: #z ] whd in ⊢ (??%? → ?);
    453   [ generalize in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ])? → ?);
    454     * #a #b try #c try #d try whd in b:(??%?); try ( destruct (b))
    455     whd in c:(??%?); destruct % [ @H1 | % // @H2 ]
    456   | generalize in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ])? → ?);
    457     * #a #b try #c try #d try whd in b:(??%?); try ( destruct (b))
    458     whd in c:(??%?); destruct % [ @H2 | % // @H1 ]
    459   | *: #E destruct (E) % try @H1 @H2
     500[ inversion (classify_add ty1 ty2) in ⊢ ?;
     501  [ #sz #sg #E1 #E2 #E3 destruct >E3 #E4 -E3 change with (typ_should_eq ???? = OK ??) in E4;
     502    @(typ_equals … E4) % //
     503  | #sz #E1 #E2 #E3 destruct >E3 #E4
     504    @(typ_equals … E4) % //
     505  | #n #r #ty0 #sz #sg #E1 #E2 #E3 destruct >E3 #E4
     506    @(typ_equals … E4) -E4 -E3 % [ @(unfix_ptr_type ???? (λt,e. expr_vars t e P) H1)| % // ]
     507  | #n #sz #sg #r #ty0 #E1 #E2 #E3 destruct >E3 #E4
     508    @(typ_equals … E4) % [ @(unfix_ptr_type ???? (λt,e. expr_vars t e P) H2)| % // ]
     509  | #ty1' #ty2' #E1 #E2 #E3 destruct >E3 #E4 whd in E4:(??%?); destruct
    460510  ]
    461 | cases (classify_sub ty1 ty2)
    462   [ 3,4: #z] whd in ⊢ (??%? → ?);
    463   [ 2: generalize in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ])? → ?);
    464     * #a #b try #c try #d try whd in b:(??%?); try ( destruct (b))
    465     whd in c:(??%?); destruct % [ % try @H1 @H2 ] @I
    466   | *: #E destruct (E) % try @H1 try @H2 % // @H2
     511| inversion (classify_sub ty1 ty2) in ⊢ ?;
     512  [ #sz #sg #E1 #E2 #E3 destruct >E3 #E4
     513    @(typ_equals … E4) % //
     514  | #sz #E1 #E2 #E3 destruct >E3 #E4
     515    @(typ_equals … E4) % //
     516  | #n #r #ty0 #sz #sg #E1 #E2 #E3 destruct >E3 #E4
     517    @(typ_equals … E4) % [ @(unfix_ptr_type ???? (λt,e. expr_vars t e P) H1)| % // ]
     518  | #n1 #n2 #r1 #ty1' #r2 #ty2' #E1 #E2 #E3 destruct >E3
     519    whd in ⊢ (??%? → ?); cases ty in e ⊢ %;
     520    [ 2: #sz #sg #e #E4 | 4: #r #ty #e #E4 | 5: #r #ty' #n' #e #E4
     521    | *: normalize #X1 #X2 try #X3 try #X4 destruct
     522    ] whd in E4:(??%?); destruct % // %
     523    [ @(unfix_ptr_type ???? (λt,e. expr_vars t e P) H1) | @(unfix_ptr_type ???? (λt,e. expr_vars t e P) H2) ]
     524  | #ty1' #ty2' #E1 #E2 #E3 destruct >E3 #E4 whd in E4:(??%?); destruct
    467525  ]
    468 | cases (classify_mul ty1 ty2) #E whd in E:(??%?); destruct
    469     % try @H1 @H2
    470 | cases (classify_div ty1 ty2) #E whd in E:(??%?); destruct
    471     % try @H1 @H2
    472 | cases (classify_mod ty1 ty2) #E whd in E:(??%?); destruct
    473     % try @H1 @H2
    474 | 6,7,8,9: #E destruct % try @H1 @H2
    475 | cases (classify_shr ty1 ty2) #E whd in E:(??%?); destruct % try @H1 @H2
    476 | 11,12,13,14,15,16: cases (classify_cmp ty1 ty2) #E whd in E:(??%?); destruct % try @H1 @H2
     526| 3,4,5,6,7,8,9,10: inversion (classify_aop ty1 ty2) in ⊢ ?;
     527  (* Note that some cases require a split on signedness of integer type. *)
     528  [ 1,4,7,10,13,16,19,22: #sz * #E1 #E2 #E3 destruct >E3 #E4
     529    @(typ_equals … E4) % //
     530  | 2,5: #sz #E1 #E2 #E3 destruct >E3 #E4
     531    @(typ_equals … E4) % //
     532  | 8,11,14,17,20,23: #sz #E1 #E2 #E3 destruct >E3 #E4 whd in E4:(??%?); destruct
     533  | 3,6,9,12,15,18,21,24: #ty1' #ty2' #E1 #E2 #E3 destruct >E3 #E4 whd in E4:(??%?); destruct
     534  ]
     535| 11,12,13,14,15,16: inversion (classify_cmp ty1 ty2) in ⊢ ?;
     536  [ 1,5,9,13,17,21: #sz * #E1 #E2 #E3 destruct >E3
     537  | 2,6,10,14,18,22: #n #r #ty' #E1 #E2 #E3 destruct >E3
     538  | 3,7,11,15,19,23: #sz #E1 #E2 #E3 destruct >E3
     539  | *: #ty1' #ty2' #E1 #E2 #E3 destruct >E3 #E4 whd in E4:(??%?); @⊥ destruct
     540  ] whd in ⊢ (??%? → ?); cases ty in e ⊢ %;
     541  try (normalize #X1 #X2 try #X3 try #X4 try #X5 destruct #FAIL)
     542  #sz #sg #e #E4
     543  whd in E4:(??%?); destruct %
     544  [ 25,27,29,31,33,35: @(unfix_ptr_type ???? (λt,e. expr_vars t e P) H1)
     545  | 26,28,30,32,34,36: @(unfix_ptr_type ???? (λt,e. expr_vars t e P) H2)
     546  | *: //
     547  ]
    477548] qed.
     549
    478550
    479551(* We'll need to implement proper translation of pointers if we really do memory
     
    532604]. whd normalize nodelta @pi2
    533605qed.
    534 
    535 (* Small inversion lemma : if the access mode of a type is by reference, then it must be a ptr type. *)
    536 lemma access_mode_typ : ∀ty,r. access_mode ty = By_reference r → typ_of_type ty = ASTptr r.
    537 *
    538 [ 5: #r #ty #n #r' normalize #E destruct @refl
    539 | 6: #args #ret #r normalize #E destruct @refl
    540 | *: normalize #a #b try #c try #d destruct
    541   [ cases a in d; normalize; cases b; normalize #E destruct
    542   | cases a in c; normalize #E destruct
    543   ]
    544 ] qed.
    545606
    546607(* Translate Clight exprs into Cminor ones.
     
    570631             - By_nothing : error
    571632           *)
    572           match access_mode ty with
    573           [ By_value q ⇒ OK ? «Mem ? r q (Cst ? (Oaddrsymbol id 0)), ?» (* Mem is "load" in compcert *)
     633          match access_mode ty return λt.λ_. res (Σe':CMexpr t. expr_vars ? e' (local_id vars)) with
     634          [ By_value t ⇒ OK ? «Mem t r (Cst ? (Oaddrsymbol id 0)), ?» (* Mem is "load" in compcert *)
    574635          | By_reference _ ⇒ OK ? «Cst ? (Oaddrsymbol id 0), ?»
    575           | By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
     636          | By_nothing _ ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
    576637          ]
    577638      | Stack n ⇒ λE.
    578639          (* We have decided that the variable should be allocated on the stack,
    579640           * because its adress was taken somewhere or becauste it's a structured data. *)
    580           match access_mode ty with
    581           [ By_value q ⇒ OK ? «Mem ? Any q (Cst ? (Oaddrstack n)), ?»
     641          match access_mode ty return λt.λ_. res (Σe':CMexpr t. expr_vars ? e' (local_id vars)) with
     642          [ By_value t ⇒ OK ? «Mem t Any (Cst ? (Oaddrstack n)), ?»
    582643          | By_reference _ ⇒ OK ? «Cst ? (Oaddrstack n), ?»
    583           | By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
     644          | By_nothing _ ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
    584645          ]
    585646          (* This is a local variable. Keep it as an identifier in the Cminor code, ensuring that the type of the original expr and of ty match. *)
     
    596657      match typ_of_type (typeof e1) return λx.(Σz:CMexpr x.expr_vars ? z (local_id vars)) → ? with
    597658      [ ASTptr r ⇒ λe1'.
    598           match access_mode ty return λx.? → res (Σe':CMexpr (typ_of_type ty). expr_vars ? e' (local_id vars)) with
    599           [ By_value q ⇒ λ_.OK ? «Mem (typ_of_type ty) ? q (pi1 … e1'), ?»
    600           | By_reference r' ⇒ λE. do e1' ← region_should_eq r r' ? e1';
    601                                   OK ? e1'⌈Σe':CMexpr ?. expr_vars ? e' (local_id vars) ↦ Σe':CMexpr (typ_of_type ty). expr_vars ? e' (local_id vars)⌉
    602           | By_nothing ⇒ λ_. Error ? (msg BadlyTypedAccess)
    603           ] (access_mode_typ ty)
     659          match access_mode ty return λt.λ_. res (Σe':CMexpr t. expr_vars ? e' (local_id vars)) with
     660          [ By_value t ⇒ OK ? «Mem t ? (pi1 … e1'), ?»
     661          | By_reference r' ⇒ region_should_eq r r' ? e1'
     662          | By_nothing _ ⇒ Error ? (msg BadlyTypedAccess)
     663          ]
    604664      | _ ⇒ λ_. Error ? (msg TypeMismatch)
    605665      ] e1'
     
    673733          [ mk_DPair r e1' ⇒
    674734            do off ← field_offset id fl;
    675             match access_mode ty with
    676             [ By_value q ⇒ OK ? «Mem ? r q (Op2 ? (ASTint I32 Unsigned (* XXX efficiency? *)) ? Oaddp e1' (Cst ? (Ointconst I32 (repr ? off)))),?»
    677             | By_reference _ ⇒ OK ? «Op2 ? (ASTint I32 Unsigned (* XXX efficiency? *)) ? Oaddp e1' (Cst ? (Ointconst I32 (repr ? off))),?»
    678             | By_nothing ⇒ Error ? (msg BadlyTypedAccess)
     735            match access_mode ty return λt.λ_. res (Σe':CMexpr t. expr_vars ? e' (local_id vars)) with
     736            [ By_value t ⇒
     737                OK ? «Mem t r (Op2 ? (ASTint I16 Signed (* XXX efficiency? *)) ?
     738                                   (Oaddp …) e1' (Cst ? (Ointconst I16 (repr ? off)))),?»
     739            | By_reference r' ⇒
     740                do e1' ← region_should_eq r r' ? e1';
     741                OK ? «Op2 (ASTptr r') (ASTint I16 Signed (* XXX efficiency? *)) (ASTptr r')
     742                        (Oaddp …) e1' (Cst ? (Ointconst I16 (repr ? off))),?»
     743            | By_nothing _ ⇒ Error ? (msg BadlyTypedAccess)
    679744            ]
    680745          ]
     
    683748          match e1' with
    684749          [ mk_DPair r e1' ⇒
    685             match access_mode ty return λx. access_mode ty = x → res ? with
    686             [ By_value q ⇒ λ_. OK ? «Mem ?? q e1', ?»
    687             | By_reference r' ⇒  λE. do e1' ← region_should_eq r r' ? e1';
    688                                 OK ? e1'⌈Σz:CMexpr (ASTptr r').? ↦ Σz:CMexpr (typ_of_type ty).?⌉
    689             | By_nothing ⇒ λ_. Error ? (msg BadlyTypedAccess)
    690             ] (refl ? (access_mode ty))
     750            match access_mode ty return λt.λ_. res (Σz:CMexpr t.?) with
     751            [ By_value t ⇒ OK ? «Mem t ? e1', ?»
     752            | By_reference r' ⇒ region_should_eq r r' ? e1'
     753            | By_nothing _ ⇒ Error ? (msg BadlyTypedAccess)
     754            ]
    691755          ]
    692756      | _ ⇒ Error ? (msg BadlyTypedAccess)
     
    723787          do off ← field_offset id fl;
    724788          match e1' with
    725           [ mk_DPair r e1'' ⇒ OK (𝚺r:region.Σe:CMexpr (ASTptr r).?) (❬r, «Op2 (ASTptr r) (ASTint I32 Unsigned (* FIXME inefficient?*)) (ASTptr r) Oaddp e1'' (Cst ? (Ointconst I32 (repr ? off))), ?» ❭)
     789          [ mk_DPair r e1'' ⇒ OK (𝚺r:region.Σe:CMexpr (ASTptr r).?)
     790             (❬r, «Op2 (ASTptr r) (ASTint I16 Signed (* FIXME inefficient?*)) (ASTptr r)
     791                     (Oaddp I16 r) e1'' (Cst ? (Ointconst I16 (repr ? off))), ?» ❭)
    726792          ]
    727793      | Tunion _ _ ⇒ translate_addr vars e1
     
    733799whd try @I
    734800[ >E whd @refl
    735 | >(E ? (refl ??)) @refl
    736 | 3,4: @pi2
     801| 2,3: @pi2
    737802| @(translate_binop_vars … E) @pi2
    738803| % [ % ] @pi2
     
    741806| % [ @pi2 | @I ]
    742807| % [ @pi2 | @I ]
    743 | >(access_mode_typ … E) @refl
    744808| @pi2
    745809| @pi2
     
    747811] qed.
    748812
     813(* We provide a function to work out how to do an assignment to an lvalue
     814   expression.  It is used for both Clight assignments and Clight function call
     815   destinations, but doesn't take the value to be assigned so that we can use
     816   it to form a single St_store when possible (and avoid introducing an
     817   unnecessary temporary variable and assignment).
     818   *)
    749819inductive destination (vars:var_types) : Type[0] ≝
    750820| IdDest : ∀id,ty. local_id vars id (typ_of_type ty) → destination vars
    751 | MemDest : ∀r:region. memory_chunk → (Σe:CMexpr (ASTptr r).expr_vars ? e (local_id vars)) → destination vars.
     821| MemDest : ∀r:region. (Σe:CMexpr (ASTptr r).expr_vars ? e (local_id vars)) → destination vars.
    752822
    753823(* Let a source Clight expression be assign(e1, e2). First of all, observe that [e1] is a
     
    767837*)
    768838definition translate_dest ≝
    769 λvars,e1,ty2.
    770     do q ← match access_mode ty2 with
    771            [ By_value q ⇒ OK ? q
    772            | By_reference r ⇒ OK ? (Mpointer r)
    773            | By_nothing ⇒ Error ? (msg BadlyTypedAccess)
    774            ];
    775     match e1 with
    776     [ Expr ed1 ty1 ⇒
    777         match ed1 with
    778         [ Evar id ⇒
    779             do 〈c,t〉 as E ← lookup' vars id;
    780             match c return λx.? → ? with
    781             [ Local ⇒ λE. OK ? (IdDest vars id t ?)
    782             | Global r ⇒ λE. OK ? (MemDest ? r q (Cst ? (Oaddrsymbol id 0)))
    783             | Stack n ⇒ λE. OK ? (MemDest ? Any q (Cst ? (Oaddrstack n)))
    784             ] E
    785         | _ ⇒
    786             do e1' ← translate_addr vars e1;
    787             match e1' with [ mk_DPair r e1' ⇒ OK ? (MemDest ? r q e1') ]
    788         ]
    789     ].
     839λvars,e1.
     840  match e1 with
     841  [ Expr ed1 ty1 ⇒
     842      match ed1 with
     843      [ Evar id ⇒
     844          do 〈c,t〉 as E ← lookup' vars id;
     845          match c return λx.? → ? with
     846          [ Local ⇒ λE. OK ? (IdDest vars id t ?)
     847          | Global r ⇒ λE. OK ? (MemDest ? r (Cst ? (Oaddrsymbol id 0)))
     848          | Stack n ⇒ λE. OK ? (MemDest ? Any (Cst ? (Oaddrstack n)))
     849          ] E
     850      | _ ⇒
     851          do e1' ← translate_addr vars e1;
     852          match e1' with [ mk_DPair r e1' ⇒ OK ? (MemDest ? r e1') ]
     853      ]
     854  ].
    790855whd // >E @refl
    791856qed.
     
    884949definition translate_assign : ∀vars:var_types. expr → expr → res (Σs:stmt. stmt_inv vars s) ≝
    885950λvars,e1,e2.
    886 do e2' ← translate_expr vars e2;             
    887 do dest ← translate_dest vars e1 (typeof e2);
     951do e2' ← translate_expr vars e2;
     952do dest ← translate_dest vars e1;
    888953match dest with
    889954[ IdDest id ty p ⇒
    890955    do e2' ← type_should_eq (typeof e2) ty ? e2';
    891956    OK ? «St_assign ? id e2', ?»
    892 | MemDest r q e1' ⇒ OK ? «St_store ? r q e1' e2', ?»
     957| MemDest r e1' ⇒ OK ? «St_store ? r e1' e2', ?»
    893958].
    894959% try (//)  try (elim e2' //) elim e1' //
     
    10461111[ Sskip ⇒ OK ? «〈uv, ul, St_skip〉, ?»
    10471112| Sassign e1 e2 ⇒
    1048     do e2' ← translate_expr vars e2;              (* rhs *)
    1049     do dest ← translate_dest vars e1 (typeof e2); (* e1 *)
     1113    do e2' ← translate_expr vars e2;  (* rhs *)
     1114    do dest ← translate_dest vars e1; (* e1 *)
    10501115    match dest with
    10511116    [ IdDest id ty p ⇒
    10521117       do e2' ← type_should_eq (typeof e2) ty ? e2';
    10531118       OK ? «〈uv, ul, St_assign ? id e2'〉, ?»
    1054     | MemDest r q e1' ⇒
    1055        OK ? «〈uv, ul, St_store ? r q e1' e2'〉, ?»
     1119    | MemDest r e1' ⇒
     1120       OK ? «〈uv, ul, St_store ? r e1' e2'〉, ?»
    10561121    ]
    10571122| Scall ret ef args ⇒
     
    10621127    [ None ⇒ OK ? «〈uv, ul, St_call (None ?) ef' args'〉, ?»
    10631128    | Some e1 ⇒
    1064         do dest ← translate_dest vars e1 (typeof e1); (* TODO: check if it's sane to use e1's type rather than the return type *)
     1129        do dest ← translate_dest vars e1;
    10651130        match dest with
    10661131        [ IdDest id ty p ⇒ OK ? «〈uv, ul, St_call (Some ? 〈id,typ_of_type ty〉) ef' args'〉, ?»
    1067         | MemDest r q e1' ⇒
     1132        | MemDest r e1' ⇒
    10681133            let 〈tmp, uv1〉 as Etmp ≝ alloc_tmp ? (typeof e1) uv in
    1069             OK ? «〈uv1, ul, St_seq (St_call (Some ? 〈tmp,typ_of_type (typeof e1)〉) ef' args') (St_store (typ_of_type (typeof e1)) r q e1' (Id ? tmp))〉, ?»
     1134            OK ? «〈uv1, ul, St_seq (St_call (Some ? 〈tmp,typ_of_type (typeof e1)〉) ef' args') (St_store (typ_of_type (typeof e1)) r e1' (Id ? tmp))〉, ?»
    10701135        ]
    10711136    ]
     
    13641429  [ Local ⇒ λE. OK (Σs:(tmpgen vars)×labgen×stmt.?) «result,Is»
    13651430  | Stack n ⇒ λE.
    1366       do q ← match access_mode ty with
    1367       [ By_value q ⇒ OK ? q
    1368       | By_reference r ⇒ OK ? (Mpointer r)
    1369       | By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
    1370       ];
    1371       OK ? «〈fgens1, St_seq (St_store ? Any q (Cst ? (Oaddrstack n)) (Id (typ_of_type ty') id)) s〉, ?»
     1431      OK ? «〈fgens1, St_seq (St_store ? Any (Cst ? (Oaddrstack n)) (Id (typ_of_type ty') id)) s〉, ?»
    13721432  | Global _ ⇒ λE. Error ? [MSG ParamGlobalMixup; CTX ? id]
    13731433  ] E) (OK ? s) params.
Note: See TracChangeset for help on using the changeset viewer.