Changeset 1872 for src/Clight/Csem.ma


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

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

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/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 //
Note: See TracChangeset for help on using the changeset viewer.