Changeset 1872


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
Files:
1 added
16 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.
  • src/Cminor/initialisation.ma

    r1631 r1872  
    66
    77(* XXX having to specify the return type in the match is annoying. *)
    8 definition init_expr : init_data → option (𝚺c:memory_chunk. expr (typ_of_memory_chunk c)) ≝
     8definition init_expr : init_data → option (𝚺t:typ. expr t) ≝
    99λinit.
    10 match init return λ_.option (𝚺c:memory_chunk. expr (typ_of_memory_chunk c)) with
    11 [ Init_int8 i          ⇒ Some ? (mk_DPair ?? Mint8unsigned (Cst ? (Ointconst I8 i)))
    12 | Init_int16 i         ⇒ Some ? (mk_DPair ?? Mint16unsigned (Cst ? (Ointconst I16 i)))
    13 | Init_int32 i         ⇒ Some ? (mk_DPair ?? Mint32 (Cst ? (Ointconst I32 i)))
    14 | Init_float32 f       ⇒ Some ? (mk_DPair ?? Mfloat32 (Cst ? (Ofloatconst f)))
    15 | Init_float64 f       ⇒ Some ? (mk_DPair ?? Mfloat64 (Cst ? (Ofloatconst f)))
     10match init return λ_.option (𝚺t:typ. expr t) with
     11[ Init_int8 i          ⇒ Some ? (mk_DPair ?? (ASTint I8 Unsigned) (Cst ? (Ointconst I8 i)))
     12| Init_int16 i         ⇒ Some ? (mk_DPair ?? (ASTint I16 Unsigned) (Cst ? (Ointconst I16 i)))
     13| Init_int32 i         ⇒ Some ? (mk_DPair ?? (ASTint I32 Unsigned) (Cst ? (Ointconst I32 i)))
     14| Init_float32 f       ⇒ Some ? (mk_DPair ?? (ASTfloat F32) (Cst ? (Ofloatconst f)))
     15| Init_float64 f       ⇒ Some ? (mk_DPair ?? (ASTfloat F64) (Cst ? (Ofloatconst f)))
    1616| Init_space n         ⇒ None ?
    17 | Init_null r          ⇒ Some ? (mk_DPair ?? (Mpointer r) (Op1 (ASTint I8 Unsigned) ? (Optrofint ?? r) (Cst ? (Ointconst I8 (zero ?)))))
    18 | Init_addrof r id off ⇒ Some ? (mk_DPair ?? (Mpointer r) (Cst ? (Oaddrsymbol id off)))
     17| Init_null r          ⇒ Some ? (mk_DPair ?? (ASTptr r) (Op1 (ASTint I8 Unsigned) ? (Optrofint ?? r) (Cst ? (Ointconst I8 (zero ?)))))
     18| Init_addrof r id off ⇒ Some ? (mk_DPair ?? (ASTptr r) (Cst ? (Oaddrsymbol id off)))
    1919].
    2020
     
    3434[ None ⇒ St_skip
    3535| Some x ⇒
    36     match x with [ mk_DPair chunk e ⇒
    37       St_store ? r chunk (Cst ? (Oaddrsymbol id off)) e
     36    match x with [ mk_DPair t e ⇒
     37      St_store t r (Cst ? (Oaddrsymbol id off)) e
    3838    ]
    3939].
  • src/Cminor/semantics.ma

    r1713 r1872  
    104104    do 〈tr1,v1〉 ← eval_expr ge ? e1 en ? sp m;
    105105    do 〈tr2,v2〉 ← eval_expr ge ? e2 en ? sp m;
    106     do r ← opt_to_res … (msg FailedOp) (eval_binop op v1 v2);
     106    do r ← opt_to_res … (msg FailedOp) (eval_binop ??? op v1 v2);
    107107    OK ? 〈tr1 ⧺ tr2, r〉
    108 | Mem rg ty chunk e ⇒ λEnv.
     108| Mem ty rg e ⇒ λEnv.
    109109    do 〈tr,v〉 ← eval_expr ge ? e en ? sp m;
    110     do r ← opt_to_res … (msg FailedLoad) (loadv chunk m v);
     110    do r ← opt_to_res … (msg FailedLoad) (loadv ty m v);
    111111    OK ? 〈tr, r〉
    112112| Cond sz sg ty e' e1 e2 ⇒ λEnv.
     
    306306        let en' ≝ update_present ?? en id ? v in
    307307        return 〈tr, State f St_skip en' ? ? m sp k ? st〉
    308     | St_store _ _ chunk edst e ⇒ λInv.
     308    | St_store ty _ edst e ⇒ λInv.
    309309        ! 〈tr,vdst〉 ← eval_expr ge ? edst en ? sp m;
    310310        ! 〈tr',v〉 ← eval_expr ge ? e en ? sp m;
    311         ! m' ← opt_to_res … (msg FailedStore) (storev chunk m vdst v);
     311        ! m' ← opt_to_res … (msg FailedStore) (storev ty m vdst v);
    312312        return 〈tr ⧺ tr', State f St_skip en fInv ? m' sp k ? st〉
    313313
  • src/Cminor/syntax.ma

    r1680 r1872  
    1010| Cst : ∀t. constant → expr t
    1111| Op1 : ∀t,t'. unary_operation t t' → expr t → expr t'
    12 | Op2 : ∀t1,t2,t'. binary_operation → expr t1 → expr t2 → expr t'
    13 | Mem : ∀t,r. memory_chunk → expr (ASTptr r) → expr t
     12| Op2 : ∀t1,t2,t'. binary_operation t1 t2 t' → expr t1 → expr t2 → expr t'
     13| Mem : ∀t,r. expr (ASTptr r) → expr t
    1414| Cond : ∀sz,sg,t. expr (ASTint sz sg) → expr t → expr t → expr t
    1515| Ecost : ∀t. costlabel → expr t → expr t.
     
    2222| Op1 _ _ _ e ⇒ expr_vars ? e P
    2323| Op2 _ _ _ _ e1 e2 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P
    24 | Mem _ _ _ e ⇒ expr_vars ? e P
     24| Mem _ _ e ⇒ expr_vars ? e P
    2525| Cond _ _ _ e1 e2 e3 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P ∧ expr_vars ? e3 P
    2626| Ecost _ _ e ⇒ expr_vars ? e P
     
    4040| St_skip : stmt
    4141| St_assign : ∀t. ident → expr t → stmt
    42 | St_store : ∀t,r. memory_chunk → expr (ASTptr r) → expr t → stmt
     42| St_store : ∀t,r. expr (ASTptr r) → expr t → stmt
    4343(* ident for returned value, expression to identify fn, args. *)
    4444| St_call : option (ident × typ) → expr (ASTptr Code) → list (𝚺t. expr t) → stmt
     
    8282match s with
    8383[ St_assign t i e ⇒ P i t ∧ expr_vars ? e P
    84 | St_store _ _ _ e1 e2 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P
     84| St_store _ _ e1 e2 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P
    8585| St_call oi e es ⇒ match oi with [ None ⇒ True | Some i ⇒ P (\fst i) (\snd i) ] ∧ expr_vars ? e P ∧ All ? (λe.match e with [ mk_DPair _ e ⇒ expr_vars ? e P ]) es
    8686(*
     
    115115[ //
    116116| #t #id #e * /4/
    117 | #t #r #q #e1 #e2 * /4/
     117| #t #r #e1 #e2 * /4/
    118118| * normalize [ 2: #id ] #e #es * * #H1 #H2 #H3 % [ 1,3: % /3/ | *: @(All_mp … H3) * #t #e normalize @expr_vars_mp @H ]
    119119(*
  • src/Cminor/toRTLabs.ma

    r1680 r1872  
    526526    let ❬f,r1❭ ≝ choose_reg … e1 f (proj1 … Env) in
    527527    let ❬f,r2❭ ≝ choose_reg … e2 f (proj2 … Env) in
    528     let f ≝ add_fresh_to_graph … (St_op2 op dst r1 r2) f ?? in
     528    let f ≝ add_fresh_to_graph … (St_op2 ??? op dst r1 r2) f ?? in
    529529    let f ≝ add_expr … env ? e2 (proj2 … Env) f «r2, ?» in
    530530    let f ≝ add_expr … env ? e1 (proj1 … Env) f «r1, ?» in
    531531      «pi1 … f, ?»
    532 | Mem _ _ q e' ⇒ λEnv,dst.
     532| Mem t _ e' ⇒ λEnv,dst.
    533533    let ❬f,r❭ ≝ choose_reg … e' f Env in
    534     let f ≝ add_fresh_to_graph … (St_load q r dst) f ?? in
     534    let f ≝ add_fresh_to_graph … (St_load t r dst) f ?? in
    535535    let f ≝ add_expr … env ? e' Env f «r,?» in
    536536      «pi1 … f, ?»
     
    682682    let dst ≝ lookup_reg env x t (π1 (π1 Env)) in
    683683    OK ? «pi1 … (add_expr ? env ? e (π2 (π1 Env)) f dst), ?»
    684 | St_store _ _ q e1 e2 ⇒ λEnv.
     684| St_store t _ e1 e2 ⇒ λEnv.
    685685    let ❬f, val_reg❭ ≝ choose_reg … e2 f (π2 (π1 Env)) in
    686686    let ❬f, addr_reg❭ ≝ choose_reg … e1 f (π1 (π1 Env)) in
    687     let f ≝ add_fresh_to_graph … (St_store q addr_reg val_reg) f ?? in
     687    let f ≝ add_fresh_to_graph … (St_store t addr_reg val_reg) f ?? in
    688688    let f ≝ add_expr ? env ? e1 (π1 (π1 Env)) f «addr_reg, ?» in
    689689    OK ? «pi1 … (add_expr ? env ? e2 (π2 (π1 Env)) f «val_reg, ?»), ?»
     
    752752      do l_case ← nth_sig ?? (msg BadCminorProgram) exits n;
    753753      let f ≝ add_fresh_to_graph … (St_cond br l_case) f ?? in
    754       let f ≝ add_fresh_to_graph … (St_op2 (Ocmpu Ceq) (* signed? *) br r cr) f ?? in
     754      let f ≝ add_fresh_to_graph … (St_op2 … (Ocmpu I8 Unsigned Ceq) (* signed? *) br r cr) f ?? in
    755755      let f ≝ add_fresh_to_graph … (St_const cr (Ointconst ? i)) f ?? in
    756756        OK ? «pi1 … f, ?») (OK ? f) tab;
  • src/RTLabs/semantics.ma

    r1713 r1872  
    105105      ! locals ← reg_store dst v' (locals f);
    106106      return 〈E0, State (mk_frame (func f) locals l ? (sp f) (retdst f)) fs m〉
    107   | St_op2 op dst src1 src2 l ⇒ λH.
     107  | St_op2 _ _ _  op dst src1 src2 l ⇒ λH.
    108108      ! v1 ← reg_retrieve (locals f) src1;
    109109      ! v2 ← reg_retrieve (locals f) src2;
    110       ! v' ← opt_to_res … (msg FailedOp) (eval_binop op v1 v2);
     110      ! v' ← opt_to_res … (msg FailedOp) (eval_binop ??? op v1 v2);
    111111      ! locals ← reg_store dst v' (locals f);
    112112      return 〈E0, State (mk_frame (func f) locals l ? (sp f) (retdst f)) fs m〉
     
    298298  | #r #c #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #locals' #Eloc #E whd in E:(??%?); destruct % %
    299299  | #t1 #t2 #op #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct % %
    300   | #op #r1 #r2 #r3 #l #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct % %
     300  | #t1 #t2 #t' #op #r1 #r2 #r3 #l #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct % %
    301301  | #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct % %
    302302  | #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct % %
  • src/RTLabs/syntax.ma

    r1705 r1872  
    1414| St_const : register → constant → label → statement
    1515| St_op1 : ∀t,t'. unary_operation t' t → register → register → label → statement (* destination source *)
    16 | St_op2 : binary_operation → register → register → register → label → statement (* destination source1 source2 *)
    17 | St_load : memory_chunk → register → register → label → statement
    18 | St_store : memory_chunk → register → register → label → statement
     16| St_op2 : ∀t1,t2,t'. binary_operation t1 t2 t' → register → register → register → label → statement (* destination source1 source2 *)
     17| St_load : typ → register → register → label → statement
     18| St_store : typ → register → register → label → statement
    1919| St_call_id : ident → list register → option register → label → statement
    2020| St_call_ptr : register → list register → option register → label → statement
     
    4343| St_const _ _ l ⇒ P l
    4444| St_op1 _ _ _ _ _ l ⇒ P l
    45 | St_op2 _ _ _ _ l ⇒ P l
     45| St_op2 _ _ _ _ _ _ _ l ⇒ P l
    4646| St_load _ _ _ l ⇒ P l
    4747| St_store _ _ _ l ⇒ P l
  • src/common/AST.ma

    r1640 r1872  
    9090#r1 #r2 @(eq_region_elim ? r1 r2) /2/; qed.
    9191
     92(* Carefully defined to be convertably nonzero *)
    9293definition size_pointer : region → nat ≝
    93 λsp. match sp with [ Data ⇒ 1 | IData ⇒ 1 | PData ⇒ 1 | XData ⇒ 2 | Code ⇒ 2 | Any ⇒ 3 ].
     94λsp. S match sp with [ Data ⇒ 0 | IData ⇒ 0 | PData ⇒ 0 | XData ⇒ 1 | Code ⇒ 1 | Any ⇒ 2 ].
    9495
    9596(* We maintain some reasonable type information through the front end of the
     
    155156* * * #NE try @refl @False_ind @NE @refl
    156157qed.
     158
     159definition signedness_check : ∀sg1,sg2:signedness. ∀P:signedness → signedness → Type[0].
     160 P sg1 sg1 → P sg1 sg2 → P sg1 sg2 ≝
     161λsg1,sg2,P.
     162match sg1 return λsg1. P sg1 sg1 → P sg1 sg2 → P sg1 sg2 with
     163[ Signed ⇒ λx. match sg2 return λsg2. P ? sg2 → P Signed sg2 with [ Signed ⇒ λd. x | _ ⇒ λd. d ]
     164| Unsigned ⇒ λx. match sg2 return λsg2. P ? sg2 → P Unsigned sg2 with [ Unsigned ⇒ λd. x | _ ⇒ λd. d ]
     165].
     166
     167let rec inttyp_eq_elim' (sz1,sz2:intsize) (sg1,sg2:signedness) (P:intsize → signedness → intsize → signedness → Type[0]) on sz1 :
     168  P sz1 sg1 sz1 sg1 → P sz1 sg1 sz2 sg2 → P sz1 sg1 sz2 sg2 ≝
     169match sz1 return λsz. P sz sg1 sz sg1 → P sz sg1 sz2 sg2 → P sz sg1 sz2 sg2 with
     170[ I8  ⇒ λx. match sz2 return λsz. P ?? sz ? → P I8 ? sz ? with [ I8  ⇒ signedness_check sg1 sg2 (λs1,s2. P ? s1 ? s2) x | _ ⇒ λd. d ]
     171| I16 ⇒ λx. match sz2 return λsz. P I16 sg1 sz sg2 → P I16 sg1 sz sg2 with [ I16 ⇒ signedness_check sg1 sg2 (λs1,s2. P ? s1 ? s2) x | _ ⇒ λd. d ]
     172| I32 ⇒ λx. match sz2 return λsz. P I32 sg1 sz sg2 → P I32 sg1 sz sg2 with [ I32 ⇒ signedness_check sg1 sg2 (λs1,s2. P ? s1 ? s2) x | _ ⇒ λd. d ]
     173].
     174
     175let rec intsize_eq_elim' (sz1,sz2:intsize) (P:intsize → intsize → Type[0]) on sz1 :
     176  P sz1 sz1 → P sz1 sz2 → P sz1 sz2 ≝
     177match sz1 return λsz. P sz sz → P sz sz2 → P sz sz2 with
     178[ I8  ⇒ λx. match sz2 return λsz. P ? sz → P I8 sz with [ I8  ⇒ λd. x | _ ⇒ λd. d ]
     179| I16 ⇒ λx. match sz2 return λsz. P ? sz → P I16 sz with [ I16 ⇒ λd. x | _ ⇒ λd. d ]
     180| I32 ⇒ λx. match sz2 return λsz. P ? sz → P I32 sz with [ I32 ⇒ λd. x | _ ⇒ λd. d ]
     181].
    157182
    158183(* [intsize_eq_elim ? sz1 sz2 ? n (λn.e1) e2] checks if [sz1] equals [sz2] and
     
    189214λsz. S match sz with [ F32 ⇒ 3 | F64 ⇒ 7 ].
    190215
     216let rec floatsize_eq_elim (sz1,sz2:floatsize) (P:floatsize → floatsize → Type[0]) on sz1 :
     217  P sz1 sz1 → P sz1 sz2 → P sz1 sz2 ≝
     218match sz1 return λsz. P sz sz → P sz sz2 → P sz sz2 with
     219[ F32 ⇒ λx. match sz2 return λsz. P ? sz → P F32 sz with [ F32 ⇒ λd. x | _ ⇒ λd. d ]
     220| F64 ⇒ λx. match sz2 return λsz. P ? sz → P F64 sz with [ F64 ⇒ λd. x | _ ⇒ λd. d ]
     221].
     222
     223
    191224definition typesize : typ → nat ≝ λty.
    192225  match ty with
     
    231264  | Some t ⇒ t
    232265  ].
    233 
    234 (* * Memory accesses (load and store instructions) are annotated by
    235   a ``memory chunk'' indicating the type, size and signedness of the
    236   chunk of memory being accessed. *)
    237 
    238 inductive memory_chunk : Type[0] ≝
    239   | Mint8signed : memory_chunk     (*r 8-bit signed integer *)
    240   | Mint8unsigned : memory_chunk   (*r 8-bit unsigned integer *)
    241   | Mint16signed : memory_chunk    (*r 16-bit signed integer *)
    242   | Mint16unsigned : memory_chunk  (*r 16-bit unsigned integer *)
    243   | Mint32 : memory_chunk          (*r 32-bit integer, or pointer *)
    244   | Mfloat32 : memory_chunk        (*r 32-bit single-precision float *)
    245   | Mfloat64 : memory_chunk        (*r 64-bit double-precision float *)
    246   | Mpointer : region → memory_chunk. (* pointer addressing given region *)
    247 
    248 definition typ_of_memory_chunk : memory_chunk → typ ≝
    249 λc. match c with
    250 [ Mint8signed ⇒ ASTint I8 Signed
    251 | Mint8unsigned ⇒ ASTint I8 Unsigned
    252 | Mint16signed ⇒ ASTint I16 Signed
    253 | Mint16unsigned ⇒ ASTint I16 Unsigned
    254 | Mint32 ⇒ ASTint I32 Unsigned (* XXX signed? *)
    255 | Mfloat32 ⇒ ASTfloat F32
    256 | Mfloat64 ⇒ ASTfloat F64
    257 | Mpointer r ⇒ ASTptr r
    258 ].
    259266
    260267(* * Initialization data for global variables. *)
  • src/common/FrontEndOps.ma

    r1545 r1872  
    4444  | Ointofptr: ∀sz,sg,r. unary_operation (ASTptr r) (ASTint sz sg).            (**r pointer to int *)
    4545
    46 inductive binary_operation : Type[0] ≝
    47   | Oadd: binary_operation                 (**r integer addition *)
    48   | Osub: binary_operation                 (**r integer subtraction *)
    49   | Omul: binary_operation                 (**r integer multiplication *)
    50   | Odiv: binary_operation                 (**r integer signed division *)
    51   | Odivu: binary_operation                (**r integer unsigned division *)
    52   | Omod: binary_operation                 (**r integer signed modulus *)
    53   | Omodu: binary_operation                (**r integer unsigned modulus *)
    54   | Oand: binary_operation                 (**r bitwise ``and'' *)
    55   | Oor: binary_operation                  (**r bitwise ``or'' *)
    56   | Oxor: binary_operation                 (**r bitwise ``xor'' *)
    57   | Oshl: binary_operation                 (**r left shift *)
    58   | Oshr: binary_operation                 (**r right signed shift *)
    59   | Oshru: binary_operation                (**r right unsigned shift *)
    60   | Oaddf: binary_operation                (**r float addition *)
    61   | Osubf: binary_operation                (**r float subtraction *)
    62   | Omulf: binary_operation                (**r float multiplication *)
    63   | Odivf: binary_operation                (**r float division *)
    64   | Ocmp: comparison -> binary_operation  (**r integer signed comparison *)
    65   | Ocmpu: comparison -> binary_operation (**r integer unsigned comparison *)
    66   | Ocmpf: comparison -> binary_operation (**r float comparison *)
    67   | Oaddp: binary_operation                (**r add an integer to a pointer *)
    68   | Osubpi: binary_operation               (**r subtract int from a pointers *)
    69   | Osubpp: intsize → binary_operation     (**r subtract two pointers *)
    70   | Ocmpp: comparison → binary_operation.  (**r compare pointers *)
     46inductive binary_operation : typ → typ → typ → Type[0] ≝
     47  | Oadd:  ∀sz,sg. binary_operation (ASTint sz sg)       (ASTint sz sg)       (ASTint sz sg)       (**r integer addition *)
     48  | Osub:  ∀sz,sg. binary_operation (ASTint sz sg)       (ASTint sz sg)       (ASTint sz sg)       (**r integer subtraction *)
     49  | Omul:  ∀sz,sg. binary_operation (ASTint sz sg)       (ASTint sz sg)       (ASTint sz sg)       (**r integer multiplication *)
     50  | Odiv:  ∀sz.    binary_operation (ASTint sz Signed)   (ASTint sz Signed)   (ASTint sz Signed)   (**r integer signed division *)
     51  | Odivu: ∀sz.    binary_operation (ASTint sz Unsigned) (ASTint sz Unsigned) (ASTint sz Unsigned) (**r integer unsigned division *)
     52  | Omod:  ∀sz.    binary_operation (ASTint sz Signed)   (ASTint sz Signed)   (ASTint sz Signed)   (**r integer signed modulus *)
     53  | Omodu: ∀sz.    binary_operation (ASTint sz Unsigned) (ASTint sz Unsigned) (ASTint sz Unsigned) (**r integer unsigned modulus *)
     54  | Oand:  ∀sz,sg. binary_operation (ASTint sz sg)       (ASTint sz sg)       (ASTint sz sg)       (**r bitwise ``and'' *)
     55  | Oor:   ∀sz,sg. binary_operation (ASTint sz sg)       (ASTint sz sg)       (ASTint sz sg)       (**r bitwise ``or'' *)
     56  | Oxor:  ∀sz,sg. binary_operation (ASTint sz sg)       (ASTint sz sg)       (ASTint sz sg)       (**r bitwise ``xor'' *)
     57  | Oshl:  ∀sz,sg. binary_operation (ASTint sz sg)       (ASTint sz sg)       (ASTint sz sg)       (**r left shift *)
     58  | Oshr:  ∀sz,sg. binary_operation (ASTint sz sg)       (ASTint sz sg)       (ASTint sz sg)       (**r right signed shift *)
     59  | Oshru: ∀sz,sg. binary_operation (ASTint sz Unsigned) (ASTint sz sg)       (ASTint sz sg)       (**r right unsigned shift *)
     60  | Oaddf: ∀sz.    binary_operation (ASTfloat sz)        (ASTfloat sz)        (ASTfloat sz)        (**r float addition *)
     61  | Osubf: ∀sz.    binary_operation (ASTfloat sz)        (ASTfloat sz)        (ASTfloat sz)        (**r float subtraction *)
     62  | Omulf: ∀sz.    binary_operation (ASTfloat sz)        (ASTfloat sz)        (ASTfloat sz)        (**r float multiplication *)
     63  | Odivf: ∀sz.    binary_operation (ASTfloat sz)        (ASTfloat sz)        (ASTfloat sz)        (**r float division *)
     64  | Ocmp: ∀sz,sg,sg'. comparison -> binary_operation (ASTint sz sg)       (ASTint sz sg)       (ASTint I8 sg') (**r integer signed comparison *)
     65  | Ocmpu: ∀sz,sg'.   comparison -> binary_operation (ASTint sz Unsigned) (ASTint sz Unsigned) (ASTint I8 sg') (**r integer unsigned comparison *)
     66  | Ocmpf: ∀sz,sg'.   comparison -> binary_operation (ASTfloat sz)        (ASTfloat sz)        (ASTint I8 sg') (**r float comparison *)
     67  | Oaddp: ∀sz,r.  binary_operation (ASTptr r)           (ASTint sz Signed)   (ASTptr r)           (**r add an integer to a pointer *)
     68  | Osubpi: ∀sz,r. binary_operation (ASTptr r)           (ASTint sz Signed)   (ASTptr r)           (**r subtract int from a pointers *)
     69  | Osubpp: ∀sz,r1,r2. binary_operation (ASTptr r1)      (ASTptr r2)          (ASTint sz Signed)   (**r subtract two pointers *)
     70  | Ocmpp: ∀r,sg'. comparison → binary_operation (ASTptr r) (ASTptr r) (ASTint I8 sg').  (**r compare pointers *)
    7171
    7272
     
    361361  | _ ⇒ None ? ].
    362362
     363definition FEtrue : val ≝ Vint I8 (repr I8 1).
     364definition FEfalse : val ≝ Vint I8 (repr I8 0).
     365definition FE_of_bool : bool → val ≝
     366λb. if b then FEtrue else FEfalse.
     367
    363368definition ev_cmp_match : comparison → option val ≝ λc.
    364369  match c with
    365   [ Ceq ⇒ Some ? Vtrue
    366   | Cne ⇒ Some ? Vfalse
     370  [ Ceq ⇒ Some ? FEtrue
     371  | Cne ⇒ Some ? FEfalse
    367372  | _   ⇒ None ?
    368373  ].
     
    370375definition ev_cmp_mismatch : comparison → option val ≝ λc.
    371376  match c with
    372   [ Ceq ⇒ Some ? Vfalse
    373   | Cne ⇒ Some ? Vtrue
     377  [ Ceq ⇒ Some ? FEfalse
     378  | Cne ⇒ Some ? FEtrue
    374379  | _   ⇒ None ?
    375380  ].
     
    379384  [ Vint sz1 n1 ⇒ match v2 with
    380385    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
    381                     (λn1. Some ? (of_bool (cmp_int ? c n1 n2)))
     386                    (λn1. Some ? (FE_of_bool (cmp_int ? c n1 n2)))
    382387                    (None ?)
    383388    | _ ⇒ None ? ]
     
    389394    [ Vptr ptr2 ⇒
    390395        if eq_block (pblock ptr1) (pblock ptr2)
    391         then Some ? (of_bool (cmp_offset c (poff ptr1) (poff ptr2)))
     396        then Some ? (FE_of_bool (cmp_offset c (poff ptr1) (poff ptr2)))
    392397        else ev_cmp_mismatch c
    393398    | Vnull r2 ⇒ ev_cmp_mismatch c
     
    405410  [ Vint sz1 n1 ⇒ match v2 with
    406411    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
    407                     (λn1. Some ? (of_bool (cmpu_int ? c n1 n2)))
     412                    (λn1. Some ? (FE_of_bool (cmpu_int ? c n1 n2)))
    408413                    (None ?)
    409414    | _ ⇒ None ? ]
     
    413418  match v1 with
    414419  [ Vfloat f1 ⇒ match v2 with
    415     [ Vfloat f2 ⇒ Some ? (of_bool (Fcmp c f1 f2))
    416     | _ ⇒ None ? ]
    417   | _ ⇒ None ? ].
    418 
    419 definition eval_binop : binary_operation → val → val → option val ≝
    420 λop.
     420    [ Vfloat f2 ⇒ Some ? (FE_of_bool (Fcmp c f1 f2))
     421    | _ ⇒ None ? ]
     422  | _ ⇒ None ? ].
     423
     424definition eval_binop : ∀t1,t2,t'. binary_operation t1 t2 t' → val → val → option val ≝
     425λt1,t2,t',op.
    421426  match op with
    422   [ Oadd ⇒ ev_add
    423   | Osub ⇒ ev_sub
    424   | Omul ⇒ ev_mul
    425   | Odiv ⇒ ev_divs
    426   | Odivu ⇒ ev_divu
    427   | Omod ⇒ ev_mods
    428   | Omodu ⇒ ev_modu
    429   | Oand ⇒ ev_and
    430   | Oor ⇒ ev_or
    431   | Oxor ⇒ ev_xor
    432   | Oshl ⇒ ev_shl
    433   | Oshr ⇒ ev_shr
    434   | Oshru ⇒ ev_shru
    435   | Oaddf ⇒ ev_addf
    436   | Osubf ⇒ ev_subf
    437   | Omulf ⇒ ev_mulf
    438   | Odivf ⇒ ev_divf
    439   | Ocmp c ⇒ ev_cmp c
    440   | Ocmpu c ⇒ ev_cmpu c
    441   | Ocmpf c ⇒ ev_cmpf c
    442   | Oaddp ⇒ ev_addp
    443   | Osubpi ⇒ ev_subpi
    444   | Osubpp sz ⇒ ev_subpp sz
    445   | Ocmpp c ⇒ ev_cmpp c
    446   ].
    447 
     427  [ Oadd _ _ ⇒ ev_add
     428  | Osub _ _ ⇒ ev_sub
     429  | Omul _ _ ⇒ ev_mul
     430  | Odiv _ ⇒ ev_divs
     431  | Odivu _ ⇒ ev_divu
     432  | Omod _ ⇒ ev_mods
     433  | Omodu _ ⇒ ev_modu
     434  | Oand _ _ ⇒ ev_and
     435  | Oor _ _ ⇒ ev_or
     436  | Oxor _ _ ⇒ ev_xor
     437  | Oshl _ _ ⇒ ev_shl
     438  | Oshr _ _ ⇒ ev_shr
     439  | Oshru _ _ ⇒ ev_shru
     440  | Oaddf _ ⇒ ev_addf
     441  | Osubf _ ⇒ ev_subf
     442  | Omulf _ ⇒ ev_mulf
     443  | Odivf _ ⇒ ev_divf
     444  | Ocmp _ _ _ c ⇒ ev_cmp c
     445  | Ocmpu _ _ c ⇒ ev_cmpu c
     446  | Ocmpf _ _ c ⇒ ev_cmpf c
     447  | Oaddp _ _ ⇒ ev_addp
     448  | Osubpi _ _ ⇒ ev_subpi
     449  | Osubpp sz _ _ ⇒ ev_subpp sz
     450  | Ocmpp _ _ c ⇒ ev_cmpp c
     451  ].
     452
     453lemma eval_binop_typ_correct : ∀t1,t2,t',op,v1,v2,v'.
     454  val_typ v1 t1 → val_typ v2 t2 →
     455  eval_binop t1 t2 t' op v1 v2 = Some ? v' →
     456  val_typ v' t'.
     457#t1x #t2x #tx' *
     458[ 1,2,3,8,9,10:
     459  #sz #sg #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) #i1 @(elim_val_typ … V2) #i2
     460  whd in ⊢ (??%? → ?); >intsize_eq_elim_true #E destruct //
     461| #sz #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) #i1 @(elim_val_typ … V2) #i2
     462  whd in ⊢ (??%? → ?); >intsize_eq_elim_true cases (division_s ???) [ | #res ] #E whd in E:(??%?); destruct //
     463| #sz #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) #i1 @(elim_val_typ … V2) #i2
     464  whd in ⊢ (??%? → ?); >intsize_eq_elim_true cases (division_u ???) [ | #res ] #E whd in E:(??%?); destruct //
     465| #sz #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) #i1 @(elim_val_typ … V2) #i2
     466  whd in ⊢ (??%? → ?); >intsize_eq_elim_true cases (modulus_s ???) [ | #res ] #E whd in E:(??%?); destruct //
     467| #sz #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) #i1 @(elim_val_typ … V2) #i2
     468  whd in ⊢ (??%? → ?); >intsize_eq_elim_true cases (modulus_u ???) [ | #res ] #E whd in E:(??%?); destruct //
     469(* shifts *)
     470| 11,12,13: #sz #sg #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) #i1 @(elim_val_typ … V2) #i2
     471  whd in ⊢ (??%? → ?); cases (lt_u ???) whd in ⊢ (??%? → ?); #E destruct //
     472(* floats *)
     473| 14,15,16,17: #sz #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) #f1 @(elim_val_typ … V2) #f2
     474  whd in ⊢ (??%? → ?); #E destruct //
     475(* comparisons *)
     476| #sz #sg #sg' #c #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) #i1 @(elim_val_typ … V2) #i2
     477  whd in ⊢ (??%? → ?); >intsize_eq_elim_true cases (cmp_int ????) #E destruct //
     478| #sz #sg' #c #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) #i1 @(elim_val_typ … V2) #i2
     479  whd in ⊢ (??%? → ?); >intsize_eq_elim_true cases (cmpu_int ????) #E destruct //
     480| #sz #sg' #c #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) #f1 @(elim_val_typ … V2) #f2
     481  whd in ⊢ (??%? → ?); cases (Fcmp ???) #E destruct //
     482(* pointers *)
     483| 21,22: #sz #r #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) % [ 2,4: #b #c #o ] @(elim_val_typ … V2) #i2
     484  whd in ⊢ (??%? → ?); [ 3,4: cases (eq_bv ???) whd in ⊢ (??%? → ?); | ] #E destruct //
     485| #sz #r1 #r2 #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) % [ | #b1 #c1 #o1 ] @(elim_val_typ … V2) % [ 2,4: #b2 #c2 #o2 ]
     486  whd in ⊢ (??%? → ?); [ 2: cases (eq_block ??) whd in ⊢ (??%? → ?); | ] #E destruct //
     487| #r #sg' #c #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) % [ 2: #b1 #c1 #o1 ] @(elim_val_typ … V2) % [ 2,4: #b2 #c2 #o2 ]
     488  whd in ⊢ (??%? → ?); [ cases (eq_block ??) cases (cmp_offset ???) ] cases c whd in ⊢ (??%? → ?); #E destruct //
     489] qed.
     490
     491
  • src/common/Globalenvs.ma

    r1599 r1872  
    406406  let r ≝ block_region m b in
    407407  match id with
    408   [ Init_int8 n ⇒ store Mint8unsigned m r b p (Vint I8 n)
    409   | Init_int16 n ⇒ store Mint16unsigned m r b p (Vint I16 n)
    410   | Init_int32 n ⇒ store Mint32 m r b p (Vint I32 n)
    411   | Init_float32 n ⇒ store Mfloat32 m r b p (Vfloat n)
    412   | Init_float64 n ⇒ store Mfloat64 m r b p (Vfloat n)
     408  [ Init_int8 n ⇒ store (ASTint I8 Unsigned) m r b p (Vint I8 n)
     409  | Init_int16 n ⇒ store (ASTint I16 Unsigned) m r b p (Vint I16 n)
     410  | Init_int32 n ⇒ store (ASTint I32 Unsigned) m r b p (Vint I32 n)
     411  | Init_float32 n ⇒ store (ASTfloat F32) m r b p (Vfloat n)
     412  | Init_float64 n ⇒ store (ASTfloat F64) m r b p (Vfloat n)
    413413  | Init_addrof r' symb ofs ⇒
    414414      match (*find_symbol ge symb*) symbols ? ge symb with
     
    416416      | Some b' ⇒
    417417        match pointer_compat_dec b' r' with
    418         [ inl pc ⇒ store (Mpointer r') m r b p (Vptr (mk_pointer r' b' pc (shift_offset ? zero_offset (repr I16 ofs))))
     418        [ inl pc ⇒ store (ASTptr r') m r b p (Vptr (mk_pointer r' b' pc (shift_offset ? zero_offset (repr I16 ofs))))
    419419        | inr _ ⇒ None ?
    420420        ]
    421421      ]
    422422  | Init_space n ⇒ Some ? m
    423   | Init_null r' ⇒ store (Mpointer r') m r b p (Vnull r')
     423  | Init_null r' ⇒ store (ASTptr r') m r b p (Vnull r')
    424424  ].
    425425
  • src/common/Mem.ma

    r1599 r1872  
    124124(* * Operations on memory stores *)
    125125
    126 (* Memory reads and writes are performed by quantities called memory chunks,
    127   encoding the type, size and signedness of the chunk being addressed.
    128   The following functions extract the size information from a chunk. *)
    129 
    130 definition size_chunk : memory_chunk → nat ≝
    131   λchunk.match chunk with
    132   [ Mint8signed => 1
    133   | Mint8unsigned => 1
    134   | Mint16signed => 2
    135   | Mint16unsigned => 2
    136   | Mint32 => 4
    137   | Mfloat32 => 4
    138   | Mfloat64 => 8
    139   | Mpointer r ⇒ size_pointer r
     126definition pred_size_chunk : typ → nat ≝
     127  λchunk. match chunk with
     128  [ ASTint sz _ ⇒ pred (size_intsize sz)
     129  | ASTptr r ⇒ pred (size_pointer r)
     130  | ASTfloat sz ⇒ pred (size_floatsize sz)
    140131  ].
    141 
    142 definition pred_size_pointer : region → nat ≝
    143 λsp. match sp with [ Data ⇒ 0 | IData ⇒ 0 | PData ⇒ 0 | XData ⇒ 1 | Code ⇒ 1 | Any ⇒ 2 ].
    144 
    145 definition pred_size_chunk : memory_chunk → nat ≝
    146   λchunk.match chunk with
    147   [ Mint8signed => 0
    148   | Mint8unsigned => 0
    149   | Mint16signed => 1
    150   | Mint16unsigned => 1
    151   | Mint32 => 3
    152   | Mfloat32 => 3
    153   | Mfloat64 => 7
    154   | Mpointer r ⇒ pred_size_pointer r
    155   ].
    156 
    157 alias symbol "plus" (instance 2) = "integer plus".
     132 
    158133lemma size_chunk_pred:
    159   ∀chunk. size_chunk chunk = 1 + pred_size_chunk chunk.
    160 #chunk cases chunk;//; #r cases r; @refl
    161 qed.
    162 
    163 lemma size_chunk_pos:
    164   ∀chunk. 0 < size_chunk chunk.
    165 #chunk >(size_chunk_pred ?) cases (pred_size_chunk chunk);
    166 normalize;//;
    167 qed.
     134  ∀chunk. typesize chunk = 1 + pred_size_chunk chunk.
     135* //
     136qed.
     137
    168138
    169139(* Memory reads and writes must respect alignment constraints:
     
    177147  appropriate for PowerPC and ARM. *)
    178148
    179 definition align_chunk : memory_chunk → Z ≝
     149definition align_chunk : typ → Z ≝
    180150  λchunk.match chunk return λ_.Z with
    181   [ Mint8signed ⇒ 1
    182   | Mint8unsigned ⇒ 1
    183   | Mint16signed ⇒ 1
    184   | Mint16unsigned ⇒ 1
    185   | _ ⇒ 1 ].
     151  [ ASTint _ _ ⇒ 1
     152  | ASTptr _ ⇒ 1
     153  | ASTfloat _ ⇒ 1
     154  ].
    186155
    187156lemma align_chunk_pos:
     
    191160
    192161lemma align_size_chunk_divides:
    193   ∀chunk. (align_chunk chunk ∣ size_chunk chunk).
    194 #chunk cases chunk;[8:#r cases r ]normalize;/3 by witness/;
     162  ∀chunk. (align_chunk chunk ∣ typesize chunk).
     163#chunk cases chunk * [ 1,2,3: * ] normalize /3 by witness/
    195164qed.
    196165
    197166lemma align_chunk_compat:
    198167  ∀chunk1,chunk2.
    199     size_chunk chunk1 = size_chunk chunk2 →
     168    typesize chunk1 = typesize chunk2 →
    200169      align_chunk chunk1 = align_chunk chunk2.
    201 #chunk1 #chunk2
    202 cases chunk1; try ( #r1 #cases #r1 )
    203 cases chunk2; try ( #r2 #cases #r2 )
    204 normalize;//;
     170* * [ 1,2,3: * ]
     171* * [ 1,2,3,12,13,14,23,24,25: * ]
     172normalize //
    205173qed.
    206174
     
    595563*)
    596564
    597 inductive valid_access (m: mem) (chunk: memory_chunk) (r: region) (b: block) (ofs: Z)
     565inductive valid_access (m: mem) (chunk: typ) (r: region) (b: block) (ofs: Z)
    598566            : Prop ≝
    599567  | valid_access_intro:
    600568      valid_block m b →
    601569      low_bound m b ≤ ofs →
    602       ofs + size_chunk chunk ≤ high_bound m b →
     570      ofs + typesize chunk ≤ high_bound m b →
    603571      (align_chunk chunk ∣ ofs) →
    604572      pointer_compat b r →
     
    610578(* XXX: Using + and ¬ instead of Sum and Not causes trouble *)
    611579let rec in_bounds
    612   (m:mem) (chunk:memory_chunk) (r:region) (b:block) (ofs:Z) on b : 
     580  (m:mem) (chunk:typ) (r:region) (b:block) (ofs:Z) on b : 
    613581    Sum (valid_access m chunk r b ofs) (Not (valid_access m chunk r b ofs)) ≝ ?.
    614582cases b #br #bi
    615583@(Zltb_elim_Type0 bi (nextblock m)) #Hnext
    616584[ @(Zleb_elim_Type0 (low_bound m (mk_block br bi)) ofs) #Hlo
    617     [ @(Zleb_elim_Type0 (ofs + size_chunk chunk) (high_bound m (mk_block br bi))) #Hhi
     585    [ @(Zleb_elim_Type0 (ofs + typesize chunk) (high_bound m (mk_block br bi))) #Hhi
    618586        [ elim (dec_dividesZ (align_chunk chunk) ofs); #Hal
    619587          [ cases (pointer_compat_dec (mk_block br bi) r); #Hcl
     
    653621  by a pointer with region [r]. *)
    654622
    655 definition load : memory_chunk → mem → region → block → Z → option val ≝
     623definition load : typ → mem → region → block → Z → option val ≝
    656624λchunk,m,r,b,ofs.
    657625  match in_bounds m chunk r b ofs with
     
    676644  as a single value [addr], which must be a pointer value. *)
    677645
    678 let rec loadv (chunk:memory_chunk) (m:mem) (addr:val) on addr : option val ≝
     646let rec loadv (chunk:typ) (m:mem) (addr:val) on addr : option val ≝
    679647  match addr with
    680648  [ Vptr ptr ⇒ load chunk m (ptype ptr) (pblock ptr) (offv (poff ptr))
     
    684652   in block [b]. *)
    685653
    686 definition unchecked_store : memory_chunk → mem → block → Z → val → mem ≝
     654definition unchecked_store : typ → mem → block → Z → val → mem ≝
    687655λchunk,m,b,ofs,v.
    688656  let c ≝ (blocks m b) in
     
    701669  by a pointer with region [r]. *)
    702670
    703 definition store : memory_chunk → mem → region → block → Z → val → option mem ≝
     671definition store : typ → mem → region → block → Z → val → option mem ≝
    704672λchunk,m,r,b,ofs,v.
    705673  match in_bounds m chunk r b ofs with
     
    722690  as a single value [addr], which must be a pointer value. *)
    723691
    724 definition storev : memory_chunk → mem → val → val → option mem ≝
     692definition storev : typ → mem → val → val → option mem ≝
    725693λchunk,m,addr,v.
    726694  match addr with
     
    753721lemma valid_access_compat:
    754722  ∀m,chunk1,chunk2,r,b,ofs.
    755   size_chunk chunk1 = size_chunk chunk2 →
     723  typesize chunk1 = typesize chunk2 →
    756724  valid_access m chunk1 r b ofs →
    757725  valid_access m chunk2 r b ofs.
     
    34983466lemma in_bounds_equiv:
    34993467  ∀chunk1,chunk2,m,r,b,ofs.∀A:Type[0].∀a1,a2: A.
    3500   size_chunk chunk1 = size_chunk chunk2 →
     3468  typesize chunk1 = typesize chunk2 →
    35013469  (match in_bounds m chunk1 r b ofs with [ inl _ ⇒ a1 | inr _ ⇒ a2]) =
    35023470  (match in_bounds m chunk2 r b ofs with [ inl _ ⇒ a1 | inr _ ⇒ a2]).
     
    35123480lemma storev_8_signed_unsigned:
    35133481  ∀m,a,v.
    3514   storev Mint8signed m a v = storev Mint8unsigned m a v.
     3482  storev (ASTint I8 Signed) m a v = storev (ASTint I8 Unsigned) m a v.
    35153483#m #a #v whd in ⊢ (??%%); elim a //
    35163484#ptr whd in ⊢ (??%%);
    3517 >(in_bounds_equiv Mint8signed Mint8unsigned … (option mem) ???) //
     3485>(in_bounds_equiv (ASTint I8 Signed) (ASTint I8 Unsigned) … (option mem) ???) //
    35183486qed.
    35193487
    35203488lemma storev_16_signed_unsigned:
    35213489  ∀m,a,v.
    3522   storev Mint16signed m a v = storev Mint16unsigned m a v.
     3490  storev (ASTint I16 Signed) m a v = storev (ASTint I16 Unsigned) m a v.
    35233491#m #a #v whd in ⊢ (??%%); elim a //
    35243492#ptr whd in ⊢ (??%%);
    3525 >(in_bounds_equiv Mint16signed Mint16unsigned … (option mem) ???) //
     3493>(in_bounds_equiv (ASTint I16 Signed) (ASTint I16 Unsigned) … (option mem) ???) //
    35263494qed.
    35273495
  • src/common/Values.ma

    r1545 r1872  
    470470       should we be able to extract bytes? *)
    471471
    472 let rec load_result (chunk: memory_chunk) (v: val) ≝
     472let rec load_result (chunk: typ) (v: val) ≝
    473473  match v with
    474474  [ Vint sz n ⇒
    475475    match chunk with
    476     [ Mint8signed ⇒ match sz with [ I8 ⇒ v | _ ⇒ Vundef ]
    477     | Mint8unsigned ⇒ match sz with [ I8 ⇒ v | _ ⇒ Vundef ]
    478     | Mint16signed ⇒ match sz with [ I16 ⇒ v | _ ⇒ Vundef ]
    479     | Mint16unsigned ⇒ match sz with [ I16 ⇒ v | _ ⇒ Vundef ]
    480     | Mint32 ⇒  match sz with [ I32 ⇒ v | _ ⇒ Vundef ]
     476    [ ASTint sz' sg ⇒ if eq_intsize sz sz' then v else Vundef
    481477    | _ ⇒ Vundef
    482478    ]
    483479  | Vptr ptr ⇒
    484480    match chunk with
    485     [ Mpointer r ⇒ if eq_region (ptype ptr) r then Vptr ptr else Vundef
     481    [ ASTptr r ⇒ if eq_region (ptype ptr) r then Vptr ptr else Vundef
    486482    | _ ⇒ Vundef
    487483    ]
    488484  | Vnull r ⇒
    489485    match chunk with
    490     [ Mpointer r' ⇒ if eq_region r r' then Vnull r else Vundef
     486    [ ASTptr r' ⇒ if eq_region r r' then Vnull r else Vundef
    491487    | _ ⇒ Vundef
    492488    ]
    493489  | Vfloat f ⇒
    494490    match chunk with
    495     [ Mfloat32 ⇒ Vfloat(singleoffloat f)
    496     | Mfloat64 ⇒ Vfloat f
     491    [ ASTfloat sz ⇒ match sz with [ F32 ⇒ Vfloat(singleoffloat f) | F64 ⇒ Vfloat f ]
    497492    | _ ⇒ Vundef
    498493    ]
     
    10851080  Val_lessdef v1 v2 → Val_lessdef (load_result chunk v1) (load_result chunk v2).
    10861081#chunk #v1 #v2 #H inversion H; //; #v #e1 #e2 #e3 cases chunk
    1087 [ 8: #r ] whd in ⊢ (?%?); //;
     1082[ #sz #sg | #r | #sz ] whd in ⊢ (?%?); //;
    10881083qed.
    10891084
Note: See TracChangeset for help on using the changeset viewer.