Changeset 880 for src/Clight/toCminor.ma


Ignore:
Timestamp:
Jun 3, 2011, 5:35:31 PM (8 years ago)
Author:
campbell
Message:

Add type information into Cminor.
As a result, the Clight to Cminor stage now does extra type checking.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminor.ma

    r816 r880  
    11
    22include "Clight/Csyntax.ma".
     3include "Clight/TypeComparison.ma".
    34include "utilities/lists.ma".
    45(*
     
    189190axiom BadLvalue : String.
    190191axiom MissingField : String.
    191 axiom TypeMismatch : String.
    192192
    193193alias id "CLunop" = "cic:/matita/cerco/Clight/Csyntax/unary_operation.ind(1,0,0)".
     
    211211
    212212definition translate_add ≝
    213 λe1,ty1,e2,ty2.
     213λty1,e1,ty2,e2,ty'.
     214let ty1' ≝ typ_of_type ty1 in
     215let ty2' ≝ typ_of_type ty2 in
    214216match classify_add ty1 ty2 with
    215 [ add_case_ii ⇒ OK ? (Op2 Oadd e1 e2)
    216 | add_case_ff ⇒ OK ? (Op2 Oaddf e1 e2)
    217 | add_case_pi ty ⇒ OK ? (Op2 Oaddp e1 (Op2 Omul e2 (Cst (Ointconst (repr (sizeof ty))))))
    218 | add_case_ip ty ⇒ OK ? (Op2 Oaddp e2 (Op2 Omul e1 (Cst (Ointconst (repr (sizeof ty))))))
     217[ add_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Oadd e1 e2)
     218| add_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' Oaddf e1 e2)
     219| add_case_pi ty ⇒ OK ? (Op2 ty1' ty2' ty' Oaddp e1 (Op2 ty2' ty2' ty2' Omul e2 (Cst ? (Ointconst (repr (sizeof ty))))))
     220| add_case_ip ty ⇒ OK ? (Op2 ty2' ty1' ty' Oaddp e2 (Op2 ty1' ty1' ty1' Omul e1 (Cst ? (Ointconst (repr (sizeof ty))))))
    219221| add_default ⇒ Error ? (msg TypeMismatch)
    220222].
    221223
    222224definition translate_sub ≝
    223 λe1,ty1,e2,ty2.
     225λty1,e1,ty2,e2,ty'.
     226let ty1' ≝ typ_of_type ty1 in
     227let ty2' ≝ typ_of_type ty2 in
    224228match classify_sub ty1 ty2 with
    225 [ sub_case_ii ⇒ OK ? (Op2 Osub e1 e2)
    226 | sub_case_ff ⇒ OK ? (Op2 Osubf e1 e2)
    227 | sub_case_pi ty ⇒ OK ? (Op2 Osubpi e1 (Op2 Omul e2 (Cst (Ointconst (repr (sizeof ty))))))
    228 | sub_case_pp ty ⇒ OK ? (Op2 Odivu (Op2 Osubpp e1 e2) (Cst (Ointconst (repr (sizeof ty)))))
     229[ sub_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Osub e1 e2)
     230| sub_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' Osubf e1 e2)
     231| sub_case_pi ty ⇒ OK ? (Op2 ty1' ty2' ty' Osubpi e1 (Op2 ty2' ty2' ty2' Omul e2 (Cst ? (Ointconst (repr (sizeof ty))))))
     232| sub_case_pp ty ⇒ OK ? (Op2 ty' ty' ty' Odivu (Op2 ty1' ty2' ty' Osubpp e1 e2) (Cst ? (Ointconst (repr (sizeof ty)))))
    229233| sub_default ⇒ Error ? (msg TypeMismatch)
    230234].
    231235
    232236definition translate_mul ≝
    233 λe1,ty1,e2,ty2.
     237λty1,e1,ty2,e2,ty'.
     238let ty1' ≝ typ_of_type ty1 in
     239let ty2' ≝ typ_of_type ty2 in
    234240match classify_mul ty1 ty2 with
    235 [ mul_case_ii ⇒ OK ? (Op2 Omul e1 e2)
    236 | mul_case_ff ⇒ OK ? (Op2 Omulf e1 e2)
     241[ mul_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Omul e1 e2)
     242| mul_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' Omulf e1 e2)
    237243| mul_default ⇒ Error ? (msg TypeMismatch)
    238244].
    239245
    240246definition translate_div ≝
    241 λe1,ty1,e2,ty2.
     247λty1,e1,ty2,e2,ty'.
     248let ty1' ≝ typ_of_type ty1 in
     249let ty2' ≝ typ_of_type ty2 in
    242250match classify_div ty1 ty2 with
    243 [ div_case_I32unsi ⇒ OK ? (Op2 Odivu e1 e2) (* FIXME: should be 8 bit only *)
    244 | div_case_ii ⇒ OK ? (Op2 Odiv e1 e2)
    245 | div_case_ff ⇒ OK ? (Op2 Odivf e1 e2)
     251[ div_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' Odivu e1 e2) (* FIXME: should be 8 bit only *)
     252| div_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Odiv e1 e2)
     253| div_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' Odivf e1 e2)
    246254| div_default ⇒ Error ? (msg TypeMismatch)
    247255].
    248256
    249257definition translate_mod ≝
    250 λe1,ty1,e2,ty2.
     258λty1,e1,ty2,e2,ty'.
     259let ty1' ≝ typ_of_type ty1 in
     260let ty2' ≝ typ_of_type ty2 in
    251261match classify_mod ty1 ty2 with
    252 [ mod_case_I32unsi ⇒ OK ? (Op2 Omodu e1 e2) (* FIXME: should be 8 bit only *)
    253 | mod_case_ii ⇒ OK ? (Op2 Omod e1 e2)
     262[ mod_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' Omodu e1 e2) (* FIXME: should be 8 bit only *)
     263| mod_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Omod e1 e2)
    254264| mod_default ⇒ Error ? (msg TypeMismatch)
    255265].
    256266
    257267definition translate_shr ≝
    258 λe1,ty1,e2,ty2.
     268λty1,e1,ty2,e2,ty'.
     269let ty1' ≝ typ_of_type ty1 in
     270let ty2' ≝ typ_of_type ty2 in
    259271match classify_shr ty1 ty2 with
    260 [ shr_case_I32unsi ⇒ OK ? (Op2 Oshru e1 e2) (* FIXME: should be 8 bit only *)
    261 | shr_case_ii ⇒ OK ? (Op2 Oshr e1 e2)
     272[ shr_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' Oshru e1 e2) (* FIXME: should be 8 bit only *)
     273| shr_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Oshr e1 e2)
    262274| shr_default ⇒ Error ? (msg TypeMismatch)
    263275].
    264276
    265277definition translate_cmp ≝
    266 λc,e1,ty1,e2,ty2.
     278λc,ty1,e1,ty2,e2,ty'.
     279let ty1' ≝ typ_of_type ty1 in
     280let ty2' ≝ typ_of_type ty2 in
    267281match classify_cmp ty1 ty2 with
    268 [ cmp_case_I32unsi ⇒ OK ? (Op2 (Ocmpu c) e1 e2)
    269 | cmp_case_ii ⇒ OK ? (Op2 (Ocmp c) e1 e2)
    270 | cmp_case_pp ⇒ OK ? (Op2 (Ocmpp c) e1 e2)
    271 | cmp_case_ff ⇒ OK ? (Op2 (Ocmpf c) e1 e2)
     282[ cmp_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' (Ocmpu c) e1 e2)
     283| cmp_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' (Ocmp c) e1 e2)
     284| cmp_case_pp ⇒ OK ? (Op2 ty1' ty2' ty' (Ocmpp c) e1 e2)
     285| cmp_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' (Ocmpf c) e1 e2)
    272286| cmp_default ⇒ Error ? (msg TypeMismatch)
    273287].
    274288
    275 definition translate_binop : binary_operation → CMexpr → type → CMexpr → type → res CMexpr ≝
    276 λop,e1,ty1,e2,ty2.
     289definition translate_binop : binary_operation → type → CMexpr ? → type → CMexpr ? → type → res (CMexpr ?) ≝
     290λop,ty1,e1,ty2,e2,ty.
     291let ty' ≝ typ_of_type ty in
    277292match op with
    278 [ Oadd ⇒ translate_add e1 ty1 e2 ty2
    279 | Osub ⇒ translate_sub e1 ty1 e2 ty2
    280 | Omul ⇒ translate_mul e1 ty1 e2 ty2
    281 | Omod ⇒ translate_mod e1 ty1 e2 ty2
    282 | Odiv ⇒ translate_div e1 ty1 e2 ty2
    283 | Oand ⇒ OK ? (Op2 Oand e1 e2)
    284 | Oor  ⇒ OK ? (Op2 Oor e1 e2)
    285 | Oxor ⇒ OK ? (Op2 Oxor e1 e2)
    286 | Oshl ⇒ OK ? (Op2 Oshl e1 e2)
    287 | Oshr ⇒ translate_shr e1 ty1 e2 ty2
    288 | Oeq ⇒ translate_cmp Ceq e1 ty1 e2 ty2
    289 | One ⇒ translate_cmp Cne e1 ty1 e2 ty2
    290 | Olt ⇒ translate_cmp Clt e1 ty1 e2 ty2
    291 | Ogt ⇒ translate_cmp Cgt e1 ty1 e2 ty2
    292 | Ole ⇒ translate_cmp Cle e1 ty1 e2 ty2
    293 | Oge ⇒ translate_cmp Cge e1 ty1 e2 ty2
    294 ].
    295 
    296 definition translate_cast : type → type → CMexpr → res CMexpr ≝
    297 λty1,ty2,e.
    298 match ty1 with
    299 [ Tint sz1 sg1 ⇒
    300     match ty2 with
    301     [ Tint sz2 sg2 ⇒ OK ? e (* FIXME: do we need to do zero/sign ext?  Ought to be 8 bit anyway... *)
    302     | Tfloat sz2 ⇒ OK ? (Op1 (match sg1 with [ Unsigned ⇒ Ofloatofintu | _ ⇒ Ofloatofint]) e)
    303     | Tpointer r _ ⇒ OK ? (Op1 (Optrofint r) e)
    304     | Tarray r _ _ ⇒ OK ? (Op1 (Optrofint r) e)
     293[ Oadd ⇒ translate_add ty1 e1 ty2 e2 ty'
     294| Osub ⇒ translate_sub ty1 e1 ty2 e2 ty'
     295| Omul ⇒ translate_mul ty1 e1 ty2 e2 ty'
     296| Omod ⇒ translate_mod ty1 e1 ty2 e2 ty'
     297| Odiv ⇒ translate_div ty1 e1 ty2 e2 ty'
     298| Oand ⇒ OK ? (Op2 (typ_of_type ty1) (typ_of_type ty2) ty' Oand e1 e2)
     299| Oor  ⇒ OK ? (Op2 (typ_of_type ty1) (typ_of_type ty2) ty' Oor e1 e2)
     300| Oxor ⇒ OK ? (Op2 (typ_of_type ty1) (typ_of_type ty2) ty' Oxor e1 e2)
     301| Oshl ⇒ OK ? (Op2 (typ_of_type ty1) (typ_of_type ty2) ty' Oshl e1 e2)
     302| Oshr ⇒ translate_shr ty1 e1 ty2 e2 ty'
     303| Oeq ⇒ translate_cmp Ceq ty1 e1 ty2 e2 ty'
     304| One ⇒ translate_cmp Cne ty1 e1 ty2 e2 ty'
     305| Olt ⇒ translate_cmp Clt ty1 e1 ty2 e2 ty'
     306| Ogt ⇒ translate_cmp Cgt ty1 e1 ty2 e2 ty'
     307| Ole ⇒ translate_cmp Cle ty1 e1 ty2 e2 ty'
     308| Oge ⇒ translate_cmp Cge ty1 e1 ty2 e2 ty'
     309].
     310
     311
     312(* We'll need to implement proper translation of pointers if we really do memory
     313   spaces. *)
     314definition check_region : ∀r1:region. ∀r2:region. ∀P:region → Type[0]. P r1 → res (P r2) ≝
     315λr1,r2,P.
     316  match r1 return λx.P x → res (P r2) with
     317  [ Any ⇒   match r2 return λx.P Any → res (P x) with [ Any ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ]
     318  | Data ⇒  match r2 return λx.P Data → res (P x) with [ Data ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ]
     319  | IData ⇒ match r2 return λx.P IData → res (P x) with [ IData ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ]
     320  | PData ⇒ match r2 return λx.P PData → res (P x) with [ PData ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ]
     321  | XData ⇒ match r2 return λx.P XData → res (P x) with [ XData ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ]
     322  | Code ⇒  match r2 return λx.P Code → res (P x) with [ Code ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ]
     323  ].
     324
     325definition translate_ptr : ∀r1,r2. CMexpr (ASTptr r1) → res (CMexpr (ASTptr r2)) ≝
     326λr1,r2,e. check_region r1 r2 ? e.
     327
     328definition translate_cast : type → ∀ty2:type. CMexpr ? → res (CMexpr (typ_of_type ty2)) ≝
     329λty1,ty2.
     330match ty1 return λx.CMexpr (typ_of_type x) → ? with
     331[ Tint sz1 sg1 ⇒ λe.
     332    match ty2 return λx.res (CMexpr (typ_of_type x)) with
     333    [ Tint sz2 sg2 ⇒ OK ? (Op1 ?? Oid e) (* FIXME: do we need to do zero/sign ext?  Ought to be 8 bit anyway... *)
     334    | Tfloat sz2 ⇒ OK ? (Op1 ?? (match sg1 with [ Unsigned ⇒ Ofloatofintu | _ ⇒ Ofloatofint]) e)
     335    | Tpointer r _ ⇒ OK ? (Op1 ?? (Optrofint r) e)
     336    | Tarray r _ _ ⇒ OK ? (Op1 ?? (Optrofint r) e)
    305337    | _ ⇒ Error ? (msg TypeMismatch)
    306338    ]
    307 | Tfloat sz1 ⇒
    308     match ty2 with
    309     [ Tint sz2 sg2 ⇒ OK ? (Op1 (match sg2 with [ Unsigned ⇒ Ointuoffloat | _ ⇒ Ointoffloat]) e)
    310     | Tfloat sz2 ⇒ OK ? e
     339| Tfloat sz1 ⇒ λe.
     340    match ty2 return λx.res (CMexpr (typ_of_type x)) with
     341    [ Tint sz2 sg2 ⇒ OK ? (Op1 ?? (match sg2 with [ Unsigned ⇒ Ointuoffloat | _ ⇒ Ointoffloat]) e)
     342    | Tfloat sz2 ⇒ OK ? (Op1 ?? Oid e) (* FIXME *)
    311343    | _ ⇒ Error ? (msg TypeMismatch)
    312344    ]
    313 | Tpointer _ _ ⇒ (* will need changed for memory regions *)
    314     match ty2 with
    315     [ Tint sz2 sg2 ⇒ OK ? (Op1 Ointofptr e)
    316     | Tarray _ _ _ ⇒ OK ? e
    317     | Tpointer _ _ ⇒ OK ? e
     345| Tpointer r1 _ ⇒ λe. (* will need changed for memory regions *)
     346    match ty2 return λx.res (CMexpr (typ_of_type x)) with
     347    [ Tint sz2 sg2 ⇒ OK ? (Op1 ?? Ointofptr e)
     348    | Tarray r2 _ _ ⇒ translate_ptr r1 r2 e
     349    | Tpointer r2 _ ⇒ translate_ptr r1 r2 e
    318350    | _ ⇒ Error ? (msg TypeMismatch)
    319351    ]
    320 | Tarray _ _ _ ⇒ (* will need changed for memory regions *)
    321     match ty2 with
    322     [ Tint sz2 sg2 ⇒ OK ? (Op1 Ointofptr e)
    323     | Tarray _ _ _ ⇒ OK ? e
    324     | Tpointer _ _ ⇒ OK ? e
     352| Tarray r1 _ _ ⇒ λe. (* will need changed for memory regions *)
     353    match ty2 return λx.res (CMexpr (typ_of_type x)) with
     354    [ Tint sz2 sg2 ⇒ OK ? (Op1 (ASTptr r1) (ASTint sz2 sg2) Ointofptr e)
     355    | Tarray r2 _ _ ⇒ translate_ptr r1 r2 e
     356    | Tpointer r2 _ ⇒ translate_ptr r1 r2 e
    325357    | _ ⇒ Error ? (msg TypeMismatch)
    326358    ]
    327 | _ ⇒ Error ? (msg TypeMismatch)
    328 ].
    329 
    330 let rec translate_expr (vars:var_types) (e:expr) on e : res CMexpr ≝
     359| _ ⇒ λ_. Error ? (msg TypeMismatch)
     360].
     361
     362definition type_should_eq : ∀ty1,ty2. ∀P:type → Type[0]. P ty1 → res (P ty2) ≝
     363λty1,ty2,P,p.
     364  do E ← assert_type_eq ty1 ty2;
     365  OK ? (match E return λx.λ_. P ty1 → P x with [ refl ⇒ λp.p ] p).
     366
     367definition typ_should_eq : ∀ty1,ty2. ∀P:typ → Type[0]. P ty1 → res (P ty2).
     368* [ #sz1 #sg1 | #r1 | #sz1 ]
     369* [ 1,5,9: | *: #a #b #c try #d @(Error ? (msg TypeMismatch)) ]
     370[ *; cases sz1 [ 1,5,9: | *: #a #b #c @(Error ? (msg TypeMismatch)) ]
     371  *; cases sg1 #P #p try @(OK ? p) @(Error ? (msg TypeMismatch))
     372| *; cases r1 #P #p try @(OK ? p) @(Error ? (msg TypeMismatch))
     373| *; cases sz1 #P #p try @(OK ? p) @(Error ? (msg TypeMismatch))
     374] qed.
     375
     376let rec translate_expr (vars:var_types) (e:expr) on e : res (CMexpr (typ_of_type (typeof e))) ≝
    331377match e with
    332378[ Expr ed ty ⇒
    333379  match ed with
    334   [ Econst_int i ⇒ OK ? (Cst (Ointconst i))
    335   | Econst_float f ⇒ OK ? (Cst (Ofloatconst f))
     380  [ Econst_int i ⇒ OK ? (Cst ? (Ointconst i))
     381  | Econst_float f ⇒ OK ? (Cst ? (Ofloatconst f))
    336382  | Evar id ⇒
    337383      do c ← opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id);
     
    339385      [ Global ⇒
    340386          match access_mode ty with
    341           [ By_value q ⇒ OK ? (Mem q (Cst (Oaddrsymbol id zero)))
    342           | By_reference _ ⇒ OK ? (Cst (Oaddrsymbol id zero))
     387          [ By_value q ⇒ OK ? (Mem ? q (Cst ? (Oaddrsymbol id zero)))
     388          | By_reference _ ⇒ OK ? (Cst ? (Oaddrsymbol id zero))
    343389          | By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
    344390          ]
    345391      | Stack n ⇒
    346392          match access_mode ty with
    347           [ By_value q ⇒ OK ? (Mem q (Cst (Oaddrstack (repr n))))
    348           | By_reference _ ⇒ OK ? (Cst (Oaddrstack (repr n)))
     393          [ By_value q ⇒ OK ? (Mem ? q (Cst ? (Oaddrstack (repr n))))
     394          | By_reference _ ⇒ OK ? (Cst ? (Oaddrstack (repr n)))
    349395          | By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
    350396          ]
    351       | Local ⇒ OK ? (Id id)
     397      | Local ⇒ OK ? (Id ? id)
    352398      ]
    353399  | Ederef e1 ⇒
    354400      do e1' ← translate_expr vars e1;
    355       match access_mode ty with
    356       [ By_value q ⇒ OK ? (Mem q e1')
     401      do e1' ← typ_should_eq ? (ASTptr Any) ? e1';
     402      do e' ← match access_mode ty with
     403      [ By_value q ⇒ OK ? (Mem ? q e1')
    357404      | By_reference _ ⇒ OK ? e1'
    358405      | By_nothing ⇒ Error ? (msg BadlyTypedAccess)
     406      ];
     407      typ_should_eq ? (typ_of_type (typeof e)) ? e'
     408  | Eaddrof e1 ⇒
     409      do e1' ← translate_addr vars e1;
     410      match typ_of_type (typeof e) return λx.res (CMexpr x) with
     411      [ ASTptr r ⇒ match r return λx.res (CMexpr (ASTptr x)) with [ Any ⇒ OK ? e1' | _ ⇒ Error ? (msg TypeMismatch) ]
     412      | _ ⇒ Error ? (msg TypeMismatch)
    359413      ]
    360   | Eaddrof e1 ⇒ translate_addr vars e1
    361414  | Eunop op e1 ⇒
    362415      do op' ← translate_unop ty op;
    363416      do e1' ← translate_expr vars e1;
    364       OK ? (Op1 op' e1')
     417      OK ? (Op1 ?? op' e1')
    365418  | Ebinop op e1 e2 ⇒
    366419      do e1' ← translate_expr vars e1;
    367420      do e2' ← translate_expr vars e2;
    368       translate_binop op e1' (typeof e1) e2' (typeof e2)
     421      translate_binop op (typeof e1) e1' (typeof e2) e2' (typeof e)
    369422  | Ecast ty1 e1 ⇒
    370423      do e1' ← translate_expr vars e1;
    371       translate_cast ty ty1 e1'
     424      do e' ← translate_cast (typeof e1) ty1 e1';
     425      typ_should_eq ? (typ_of_type (typeof e)) ? e'
    372426  | Econdition e1 e2 e3 ⇒
    373427      do e1' ← translate_expr vars e1;
    374428      do e2' ← translate_expr vars e2;
     429      do e2' ← type_should_eq ? (typeof e) (λx.CMexpr (typ_of_type x)) e2';
    375430      do e3' ← translate_expr vars e3;
    376       OK ? (Cond e1' e2' e3')
     431      do e3' ← type_should_eq ? (typeof e) (λx.CMexpr (typ_of_type x)) e3';
     432      match typ_of_type (typeof e1) return λx.CMexpr x → ? with
     433      [ ASTint _ _ ⇒ λe1'. OK ? (Cond ??? e1' e2' e3')
     434      | _ ⇒ λ_.Error ? (msg TypeMismatch)
     435      ] e1'
    377436  | Eandbool e1 e2 ⇒
    378437      do e1' ← translate_expr vars e1;
    379438      do e2' ← translate_expr vars e2;
    380       OK ? (Cond e1' e2' (Cst (Ointconst zero)))
     439      do e2' ← type_should_eq ? (typeof e) (λx.CMexpr (typ_of_type x)) e2';
     440      match typ_of_type (typeof e1) return λx.CMexpr x → res (CMexpr (typ_of_type (typeof e))) with
     441      [ ASTint _ _ ⇒ λe1'. OK ? (Cond ??? e1' e2' (Cst ? (Ointconst zero)))
     442      | _ ⇒ λ_.Error ? (msg TypeMismatch)
     443      ] e1'
    381444  | Eorbool e1 e2 ⇒
    382445      do e1' ← translate_expr vars e1;
    383446      do e2' ← translate_expr vars e2;
    384       OK ? (Cond e1' (Cst (Ointconst one)) e2')
    385   | Esizeof ty1 ⇒ OK ? (Cst (Ointconst (repr (sizeof ty1))))
     447      do e2' ← type_should_eq ? (typeof e) (λx.CMexpr (typ_of_type x)) e2';
     448      match typ_of_type (typeof e1) return λx.CMexpr x → res (CMexpr (typ_of_type (typeof e))) with
     449      [ ASTint _ _ ⇒ λe1'. OK ? (Cond ??? e1' (Cst ? (Ointconst one)) e2')
     450      | _ ⇒ λ_.Error ? (msg TypeMismatch)
     451      ] e1'
     452  | Esizeof ty1 ⇒ OK ? (Cst ? (Ointconst (repr (sizeof ty1))))
    386453  | Efield e1 id ⇒
    387       match typeof e1 with
     454      do e' ← match typeof e1 with
    388455      [ Tstruct _ fl ⇒
    389456          do e1' ← translate_addr vars e1;
    390457          do off ← field_offset id fl;
    391458          match access_mode ty with
    392           [ By_value q ⇒ OK ? (Mem q (Op2 Oaddp e1' (Cst (Ointconst (repr off)))))
    393           | By_reference _ ⇒ OK ? (Op2 Oaddp e1' (Cst (Ointconst (repr off))))
     459          [ By_value q ⇒ OK ? (Mem ? q (Op2 ? (ASTint I32 Unsigned (* XXX efficiency? *)) ? Oaddp e1' (Cst ? (Ointconst (repr off)))))
     460          | By_reference _ ⇒ OK ? (Op2 ? (ASTint I32 Unsigned (* XXX efficiency? *)) ? Oaddp e1' (Cst ? (Ointconst (repr off))))
    394461          | By_nothing ⇒ Error ? (msg BadlyTypedAccess)
    395462          ]
     
    397464          do e1' ← translate_addr vars e1;
    398465          match access_mode ty with
    399           [ By_value q ⇒ OK ? (Mem q e1')
     466          [ By_value q ⇒ OK ? (Mem ? q e1')
    400467          | By_reference _ ⇒ OK ? e1'
    401468          | By_nothing ⇒ Error ? (msg BadlyTypedAccess)
    402469          ]
    403470      | _ ⇒ Error ? (msg BadlyTypedAccess)
    404       ]
     471      ];
     472      typ_should_eq ? (typ_of_type (typeof e)) ? e'
    405473  | Ecost l e1 ⇒
    406474      do e1' ← translate_expr vars e1;
    407       OK ? (Ecost l e1')
     475      do e' ← OK ? (Ecost ? l e1');
     476      typ_should_eq ? (typ_of_type (typeof e)) ? e'
    408477  ]
    409 ] and translate_addr (vars:var_types) (e:expr) on e : res CMexpr
     478] and translate_addr (vars:var_types) (e:expr) on e : res (CMexpr (ASTptr Any))
    410479match e with
    411480[ Expr ed _ ⇒
     
    414483      do c ← opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id);
    415484      match c with
    416       [ Global ⇒ OK ? (Cst (Oaddrsymbol id zero))
    417       | Stack n ⇒ OK ? (Cst (Oaddrstack (repr n)))
     485      [ Global ⇒ OK ? (Cst ? (Oaddrsymbol id zero))
     486      | Stack n ⇒ OK ? (Cst ? (Oaddrstack (repr n)))
    418487      | Local ⇒ Error ? (msg BadlyTypedAccess) (* TODO: could rule out? *)
    419488      ]
    420   | Ederef e1 ⇒ translate_expr vars e1
     489  | Ederef e1 ⇒
     490      do e1' ← translate_expr vars e1;
     491      match typ_of_type (typeof e1) return λx. CMexpr x → res (CMexpr (ASTptr Any)) with
     492      [ ASTptr r ⇒ match r return λx. CMexpr (ASTptr x) → res (CMexpr (ASTptr Any)) with [ Any ⇒ λe1'.OK ? e1' | _ ⇒ λ_.Error ? (msg BadlyTypedAccess) ]
     493      | _ ⇒ λ_.Error ? (msg BadlyTypedAccess)
     494      ] e1'
    421495  | Efield e1 id ⇒
    422496      match typeof e1 with
     
    424498          do e1' ← translate_addr vars e1;
    425499          do off ← field_offset id fl;
    426           OK ? (Op2 Oaddp e1' (Cst (Ointconst (repr off))))
     500          OK ? (Op2 (ASTptr Any) (ASTint I32 Unsigned (* FIXME inefficient?*)) (ASTptr Any) Oaddp e1' (Cst ? (Ointconst (repr off))))
    427501      | Tunion _ _ ⇒ translate_addr vars e1
    428502      | _ ⇒ Error ? (msg BadlyTypedAccess)
     
    434508inductive destination : Type[0] ≝
    435509| IdDest : ident → destination
    436 | MemDest : memory_chunk → CMexpr → destination.
     510| MemDest : memory_chunk → CMexpr (ASTptr Any) → destination.
    437511
    438512definition translate_dest ≝
     
    450524            match c with
    451525            [ Local ⇒ OK ? (IdDest id)
    452             | Global ⇒ OK ? (MemDest q (Cst (Oaddrsymbol id zero)))
    453             | Stack n ⇒ OK ? (MemDest q (Cst (Oaddrstack (repr n))))
     526            | Global ⇒ OK ? (MemDest q (Cst ? (Oaddrsymbol id zero)))
     527            | Stack n ⇒ OK ? (MemDest q (Cst ? (Oaddrstack (repr n))))
    454528            ]
    455529        | _ ⇒
     
    488562do dest ← translate_dest vars e1 (typeof e2);
    489563match dest with
    490 [ IdDest id ⇒ OK ? (St_assign id e2')
    491 | MemDest q e1' ⇒ OK ? (St_store q e1' e2')
     564[ IdDest id ⇒ OK ? (St_assign ? id e2')
     565| MemDest q e1' ⇒ OK ? (St_store ? q e1' e2')
    492566].
    493567
     
    498572| Some a ⇒ do b ← f a; OK ? (Some ? b)
    499573].
     574
     575definition translate_expr_sigma : var_types → expr → res (Σt:typ.CMexpr t) ≝
     576λv,e.
     577  do e' ← translate_expr v e;
     578  OK ? (dp ? (λt:typ.CMexpr t) ? e').
    500579
    501580axiom FIXME : String.
     
    507586| Scall ret ef args ⇒
    508587    do ef' ← translate_expr vars ef;
    509     do args' ← mmap … (translate_expr vars) args;
     588    do ef' ← typ_should_eq ? (ASTptr Code) ? ef';
     589    do args' ← mmap … (translate_expr_sigma vars) args;
    510590    match ret with
    511591    [ None ⇒ OK ? (St_call (None ?) ef' args')
     
    516596        | MemDest q e1' ⇒
    517597            let tmp' ≝ match q with [ Mpointer _ ⇒ tmpp | _ ⇒ tmp ] in
    518             OK ? (St_seq (St_call (Some ? tmp) ef' args') (St_store q e1' (Id tmp)))
     598            OK ? (St_seq (St_call (Some ? tmp) ef' args') (St_store ? (typ_of_memory_chunk q) q e1' (Id ? tmp)))
    519599        ]
    520600    ]
     
    525605| Sifthenelse e1 s1 s2 ⇒
    526606    do e1' ← translate_expr vars e1;
    527     do s1' ← translate_statement vars tmp tmpp s1;
    528     do s2' ← translate_statement vars tmp tmpp s2;
    529     OK ? (St_ifthenelse e1' s1' s2')
     607    match typ_of_type (typeof e1) return λx.CMexpr x → ? with
     608    [ ASTint _ _ ⇒ λe1'.
     609        do s1' ← translate_statement vars tmp tmpp s1;
     610        do s2' ← translate_statement vars tmp tmpp s2;
     611        OK ? (St_ifthenelse ?? e1' s1' s2')
     612    | _ ⇒ λ_.Error ? (msg TypeMismatch)
     613    ] e1'
    530614| Swhile e1 s1 ⇒
    531615    do e1' ← translate_expr vars e1;
    532     do s1' ← translate_statement vars tmp tmpp s1;
    533     (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
    534     OK ? (St_block
    535            (St_loop
    536              (St_ifthenelse e1' (St_block s1') (St_exit 0))))
     616    match typ_of_type (typeof e1) return λx.CMexpr x → ? with
     617    [ ASTint _ _ ⇒ λe1'.
     618        do s1' ← translate_statement vars tmp tmpp s1;
     619        (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
     620        OK ? (St_block
     621               (St_loop
     622                 (St_ifthenelse ?? e1' (St_block s1') (St_exit 0))))
     623    | _ ⇒ λ_.Error ? (msg TypeMismatch)
     624    ] e1'
    537625| Sdowhile e1 s1 ⇒
    538626    do e1' ← translate_expr vars e1;
    539     do s1' ← translate_statement vars tmp tmpp s1;
    540     (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
    541     OK ? (St_block
    542            (St_loop
    543              (St_seq (St_block s1') (St_ifthenelse e1' St_skip (St_exit 0)))))
     627    match typ_of_type (typeof e1) return λx.CMexpr x → ? with
     628    [ ASTint _ _ ⇒ λe1'.
     629        do s1' ← translate_statement vars tmp tmpp s1;
     630        (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
     631        OK ? (St_block
     632               (St_loop
     633                 (St_seq (St_block s1') (St_ifthenelse ?? e1' St_skip (St_exit 0)))))
     634    | _ ⇒ λ_.Error ? (msg TypeMismatch)
     635    ] e1'
    544636| Sfor s1 e1 s2 s3 ⇒
    545637    do e1' ← translate_expr vars e1;
    546     do s1' ← translate_statement vars tmp tmpp s1;
    547     do s2' ← translate_statement vars tmp tmpp s2;
    548     do s3' ← translate_statement vars tmp tmpp s3;
    549     (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
    550     OK ? (St_seq s1'
    551          (St_block
    552            (St_loop
    553              (St_ifthenelse e1' (St_seq (St_block s3') s2') (St_exit 0)))))
     638    match typ_of_type (typeof e1) return λx.CMexpr x → ? with
     639    [ ASTint _ _ ⇒ λe1'.
     640        do s1' ← translate_statement vars tmp tmpp s1;
     641        do s2' ← translate_statement vars tmp tmpp s2;
     642        do s3' ← translate_statement vars tmp tmpp s3;
     643        (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
     644        OK ? (St_seq s1'
     645             (St_block
     646               (St_loop
     647                 (St_ifthenelse ?? e1' (St_seq (St_block s3') s2') (St_exit 0)))))
     648    | _ ⇒ λ_.Error ? (msg TypeMismatch)
     649    ] e1'
    554650| Sbreak ⇒ OK ? (St_exit 1)
    555651| Scontinue ⇒ OK ? (St_exit 0)
    556652| Sreturn ret ⇒
    557     do ret' ← m_option_map ?? (translate_expr vars) ret;
    558     OK ? (St_return ret')
     653    match ret with
     654    [ None ⇒ OK ? (St_return (None ?))
     655    | Some e1 ⇒
     656        do e1' ← translate_expr vars e1;
     657        OK ? (St_return (Some ? (dp … e1')))
     658    ]
    559659| Sswitch e1 ls ⇒ Error ? (msg FIXME)
    560660| Slabel l s1 ⇒
Note: See TracChangeset for help on using the changeset viewer.