Changeset 880


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

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

Location:
src
Files:
1 added
7 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Cexec.ma

    r797 r880  
    55include "common/SmallstepExec.ma".
    66include "Clight/Csem.ma".
     7include "Clight/TypeComparison.ma".
    78
    89(*
     
    4344  λA,P,a. match a with [ Error _ ⇒ True | OK v ⇒ P v ].
    4445
    45 axiom TypeMismatch : String.
    4646axiom ValueIsNotABoolean : String.
    4747
     
    333333      ]
    334334  ] ].
    335 
    336 definition sz_eq_dec : ∀s1,s2:intsize. (s1 = s2) + (s1 ≠ s2).
    337 #s1 cases s1; #s2 cases s2; /2/; %2 ; % #H destruct; qed.
    338 definition sg_eq_dec : ∀s1,s2:signedness. (s1 = s2) + (s1 ≠ s2).
    339 #s1 cases s1; #s2 cases s2; /2/; %2 ; % #H destruct; qed.
    340 definition fs_eq_dec : ∀s1,s2:floatsize. (s1 = s2) + (s1 ≠ s2).
    341 #s1 cases s1; #s2 cases s2; /2/; %2 ; % #H destruct; qed.
    342 
    343 definition eq_nat_dec : ∀n,m:nat. Sum (n=m) (n≠m).
    344 #n #m lapply (refl ? (eqb n m)) cases (eqb n m) in ⊢ (???% → ?) #E
    345 [ %1 | %2 ] @(eqb_elim … E) // #_ #H destruct qed.
    346 
    347 let rec type_eq_dec (t1,t2:type) : Sum (t1 = t2) (t1 ≠ t2) ≝
    348 match t1 return λt'. (t' = t2) + (t' ≠ t2) with
    349 [ Tvoid ⇒ match t2 return λt'. (Tvoid = t') + (Tvoid ≠ t') with [ Tvoid ⇒ inl ?? (refl ??) | _ ⇒ inr ?? (nmk ? (λH.?)) ]
    350 | Tint sz sg ⇒ match t2 return λt'. (Tint ?? = t') + (Tint ?? ≠ t')  with [ Tint sz' sg' ⇒
    351     match sz_eq_dec sz sz' with [ inl e1 ⇒
    352     match sg_eq_dec sg sg' with [ inl e2 ⇒ inl ???
    353     | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
    354     | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
    355     | _ ⇒ inr ?? (nmk ? (λH.?)) ]
    356 | Tfloat f ⇒ match t2 return λt'. (Tfloat ? = t') + (Tfloat ? ≠ t')  with [ Tfloat f' ⇒
    357     match fs_eq_dec f f' with [ inl e1 ⇒ inl ???
    358     | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
    359     | _ ⇒ inr ?? (nmk ? (λH.?)) ]
    360 | Tpointer s t ⇒ match t2 return λt'. (Tpointer ?? = t') + (Tpointer ?? ≠ t')  with [ Tpointer s' t' ⇒
    361     match eq_region_dec s s' with [ inl e1 ⇒
    362       match type_eq_dec t t' with [ inl e2 ⇒ inl ???
    363       | inr e2 ⇒ inr ?? (nmk ? (λH.match e2 with [ nmk e' ⇒ e' ? ])) ]
    364     | inr e1 ⇒ inr ?? (nmk ? (λH.match e1 with [ nmk e' ⇒ e' ? ])) ] | _ ⇒ inr ?? (nmk ? (λH.?)) ]
    365 | Tarray s t n ⇒ match t2 return λt'. (Tarray ??? = t') + (Tarray ??? ≠ t')  with [ Tarray s' t' n' ⇒
    366     match eq_region_dec s s' with [ inl e1 ⇒
    367       match type_eq_dec t t' with [ inl e2 ⇒
    368         match eq_nat_dec n n' with [ inl e3 ⇒ inl ???
    369         | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
    370         | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
    371         | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
    372         | _ ⇒ inr ?? (nmk ? (λH.?)) ]
    373 | Tfunction tl t ⇒ match t2 return λt'. (Tfunction ?? = t') + (Tfunction ?? ≠ t')  with [ Tfunction tl' t' ⇒
    374     match typelist_eq_dec tl tl' with [ inl e1 ⇒
    375     match type_eq_dec t t' with [ inl e2 ⇒ inl ???
    376     | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
    377     | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
    378   | _ ⇒ inr ?? (nmk ? (λH.?)) ]
    379 | Tstruct i fl ⇒
    380     match t2 return λt'. (Tstruct ?? = t') + (Tstruct ?? ≠ t')  with [ Tstruct i' fl' ⇒
    381     match ident_eq i i' with [ inl e1 ⇒
    382     match fieldlist_eq_dec fl fl' with [ inl e2 ⇒ inl ???
    383     | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
    384     | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
    385     | _ ⇒ inr ?? (nmk ? (λH.?)) ]
    386 | Tunion i fl ⇒
    387     match t2 return λt'. (Tunion ?? = t') + (Tunion ?? ≠ t')  with [ Tunion i' fl' ⇒
    388     match ident_eq i i' with [ inl e1 ⇒
    389     match fieldlist_eq_dec fl fl' with [ inl e2 ⇒ inl ???
    390     | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
    391     | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
    392     |  _ ⇒ inr ?? (nmk ? (λH.?)) ]
    393 | Tcomp_ptr r i ⇒ match t2 return λt'. (Tcomp_ptr ? ? = t') + (Tcomp_ptr ? ? ≠ t')  with [ Tcomp_ptr r' i' ⇒
    394     match eq_region_dec r r' with [ inl e1 ⇒
    395       match ident_eq i i' with [ inl e2 ⇒ inl ???
    396       | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
    397     | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
    398     | _ ⇒ inr ?? (nmk ? (λH.?)) ]
    399 ]
    400 and typelist_eq_dec (tl1,tl2:typelist) : (tl1 = tl2) + (tl1 ≠ tl2) ≝
    401 match tl1 return λtl'. (tl' = tl2) + (tl' ≠ tl2) with
    402 [ Tnil ⇒ match tl2 return λtl'. (Tnil = tl') + (Tnil ≠ tl') with [ Tnil ⇒ inl ?? (refl ??) | _ ⇒ inr ?? (nmk ? (λH.?)) ]
    403 | Tcons t1 ts1 ⇒ match tl2 return λtl'. (Tcons ?? = tl') + (Tcons ?? ≠ tl') with [ Tnil ⇒ inr ?? (nmk ? (λH.?)) | Tcons t2 ts2 ⇒
    404     match type_eq_dec t1 t2 with [ inl e1 ⇒
    405     match typelist_eq_dec ts1 ts2 with [ inl e2 ⇒ inl ???
    406     | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
    407     | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ] ]
    408 ]
    409 and fieldlist_eq_dec (fl1,fl2:fieldlist) : (fl1 = fl2) + (fl1 ≠ fl2) ≝
    410 match fl1 return λfl'. (fl' = fl2) + (fl' ≠ fl2) with
    411 [ Fnil ⇒ match fl2 return λfl'. (Fnil = fl') + (Fnil ≠ fl') with [ Fnil ⇒ inl ?? (refl ??) | _ ⇒ inr ?? (nmk ? (λH.?)) ]
    412 | Fcons i1 t1 fs1 ⇒ match fl2 return λfl'. (Fcons ??? = fl') + (Fcons ??? ≠ fl') with [ Fnil ⇒ inr ?? (nmk ? (λH.?)) | Fcons i2 t2 fs2 ⇒
    413     match ident_eq i1 i2 with [ inl e1 ⇒
    414       match type_eq_dec t1 t2 with [ inl e2 ⇒
    415         match fieldlist_eq_dec fs1 fs2 with [ inl e3 ⇒ inl ???
    416         | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
    417         | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
    418         | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ] ]
    419 ]. destruct; //; qed.
    420 
    421 definition assert_type_eq : ∀t1,t2:type. res (t1 = t2) ≝
    422 λt1,t2. match type_eq_dec t1 t2 with [ inl p ⇒ OK ? p | inr _ ⇒ Error ? (msg TypeMismatch)].
    423335
    424336let rec is_is_call_cont (k:cont) : Sum (is_call_cont k) (Not (is_call_cont k)) ≝
  • 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 ⇒
  • src/Cminor/initialisation.ma

    r758 r880  
    55include "common/Globalenvs.ma".
    66
    7 definition init_expr : init_data → option (memory_chunk × expr) ≝
     7(* XXX having to specify the return type in the match is annoying. *)
     8definition init_expr : init_data → option (Σc:memory_chunk. expr (typ_of_memory_chunk c)) ≝
    89λinit.
    9 match init with
    10 [ Init_int8 i          ⇒ Some ? 〈Mint8unsigned, Cst (Ointconst i)〉
    11 | Init_int16 i         ⇒ Some ? 〈Mint16unsigned, Cst (Ointconst i)〉
    12 | Init_int32 i         ⇒ Some ? 〈Mint32, Cst (Ointconst i)〉
    13 | Init_float32 f       ⇒ Some ? 〈Mfloat32, Cst (Ofloatconst f)〉
    14 | Init_float64 f       ⇒ Some ? 〈Mfloat64, Cst (Ofloatconst f)〉
     10match init return λ_.option (Σc:memory_chunk. expr (typ_of_memory_chunk c)) with
     11[ Init_int8 i          ⇒ Some ? (dp ?? Mint8unsigned (Cst ? (Ointconst i)))
     12| Init_int16 i         ⇒ Some ? (dp ?? Mint16unsigned (Cst ? (Ointconst i)))
     13| Init_int32 i         ⇒ Some ? (dp ?? Mint32 (Cst ? (Ointconst i)))
     14| Init_float32 f       ⇒ Some ? (dp ?? Mfloat32 (Cst ? (Ofloatconst f)))
     15| Init_float64 f       ⇒ Some ? (dp ?? Mfloat64 (Cst ? (Ofloatconst f)))
    1516| Init_space n         ⇒ None ?
    16 | Init_null r          ⇒ Some ? 〈Mpointer r, Op1 (Optrofint r) (Cst (Ointconst zero))〉
    17 | Init_addrof r id off ⇒ Some ? 〈Mpointer r, Cst (Oaddrsymbol id off)〉
     17| Init_null r          ⇒ Some ? (dp ?? (Mpointer r) (Op1 (ASTint I8 Unsigned) ? (Optrofint r) (Cst ? (Ointconst zero))))
     18| Init_addrof r id off ⇒ Some ? (dp ?? (Mpointer r) (Cst ? (Oaddrsymbol id off)))
    1819].
    1920
     
    2627[ None ⇒ St_skip
    2728| Some x ⇒
    28     let 〈chunk, e〉 ≝ x in
    29     St_store chunk (Cst (Oaddrsymbol id off)) e
     29    match x with [ dp chunk e ⇒
     30      St_store ? chunk (Cst ? (Oaddrsymbol id off)) e
     31    ]
    3032].
    3133
  • src/Cminor/semantics.ma

    r879 r880  
    5050axiom FailedLoad : String.
    5151
    52 let rec eval_expr (ge:genv) (e:expr) (en:env) (sp:block) (m:mem) on e : res (trace × val) ≝
     52let rec eval_expr (ge:genv) (ty0:typ) (e:expr ty0) (en:env) (sp:block) (m:mem) on e : res (trace × val) ≝
    5353match e with
    54 [ Id i ⇒
     54[ Id _ i ⇒
    5555    do r ← opt_to_res … [MSG UnknownLocal; CTX ? i] (lookup ?? en i);
    5656    OK ? 〈E0, r〉
    57 | Cst c ⇒
     57| Cst _ c ⇒
    5858    do r ← opt_to_res … (msg FailedConstant) (eval_constant (find_symbol … ge) sp c);
    5959    OK ? 〈E0, r〉
    60 | Op1 op e' ⇒
    61     do 〈tr,v〉 ← eval_expr ge e' en sp m;
     60| Op1 ty ty' op e' ⇒
     61    do 〈tr,v〉 ← eval_expr ge ? e' en sp m;
    6262    do r ← opt_to_res … (msg FailedOp) (eval_unop op v);
    6363    OK ? 〈tr, r〉
    64 | Op2 op e1 e2 ⇒
    65     do 〈tr1,v1〉 ← eval_expr ge e1 en sp m;
    66     do 〈tr2,v2〉 ← eval_expr ge e2 en sp m;
     64| Op2 ty1 ty2 ty' op e1 e2 ⇒
     65    do 〈tr1,v1〉 ← eval_expr ge ? e1 en sp m;
     66    do 〈tr2,v2〉 ← eval_expr ge ? e2 en sp m;
    6767    do r ← opt_to_res … (msg FailedOp) (eval_binop op v1 v2);
    6868    OK ? 〈tr1 ⧺ tr2, r〉
    69 | Mem chunk e ⇒
    70     do 〈tr,v〉 ← eval_expr ge e en sp m;
     69| Mem ty chunk e ⇒
     70    do 〈tr,v〉 ← eval_expr ge ? e en sp m;
    7171    do r ← opt_to_res … (msg FailedLoad) (loadv chunk m v);
    7272    OK ? 〈tr, r〉
    73 | Cond e' e1 e2 ⇒
    74     do 〈tr,v〉 ← eval_expr ge e' en sp m;
     73| Cond sz sg ty e' e1 e2 ⇒
     74    do 〈tr,v〉 ← eval_expr ge ? e' en sp m;
    7575    do b ← eval_bool_of_val v;
    76     do 〈tr',r〉 ← eval_expr ge (if b then e1 else e2) en sp m;
     76    do 〈tr',r〉 ← eval_expr ge ? (if b then e1 else e2) en sp m;
    7777    OK ? 〈tr ⧺ tr', r〉
    78 | Ecost l e' ⇒
    79     do 〈tr,r〉 ← eval_expr ge e' en sp m;
     78| Ecost ty l e' ⇒
     79    do 〈tr,r〉 ← eval_expr ge ty e' en sp m;
    8080    OK ? 〈Echarge l ⧺ tr, r〉
    8181].
     
    113113    | Some sk ⇒ Some ? sk
    114114    ]
    115 | St_ifthenelse _ s1 s2 ⇒
     115| St_ifthenelse _ _ _ s1 s2 ⇒
    116116    match find_label l s1 k with
    117117    [ None ⇒ find_label l s2 k
     
    165165        | Kcall _ _ _ _ _ ⇒ ret ? 〈E0, Returnstate (None ?) (free m sp) k〉
    166166        ]
    167     | St_assign id e ⇒
    168         ! 〈tr,v〉 ← eval_expr ge e en sp m;
     167    | St_assign _ id e ⇒
     168        ! 〈tr,v〉 ← eval_expr ge ? e en sp m;
    169169        ! en' ← update ?? en id v;
    170170        ret ? 〈tr, State f St_skip en' m sp k〉
    171     | St_store chunk edst e ⇒
    172         ! 〈tr,vdst〉 ← eval_expr ge edst en sp m;
    173         ! 〈tr',v〉 ← eval_expr ge e en sp m;
     171    | St_store _ chunk edst e ⇒
     172        ! 〈tr,vdst〉 ← eval_expr ge ? edst en sp m;
     173        ! 〈tr',v〉 ← eval_expr ge ? e en sp m;
    174174        ! m' ← opt_to_res … (msg FailedStore) (storev chunk m vdst v);
    175175        ret ? 〈tr ⧺ tr', State f St_skip en m' sp k〉
    176176
    177177    | St_call dst ef args ⇒
    178         ! 〈tr,vf〉 ← eval_expr ge ef en sp m;
     178        ! 〈tr,vf〉 ← eval_expr ge ? ef en sp m;
    179179        ! fd ← opt_to_res … (msg BadFunctionValue) (find_funct ?? ge vf);
    180         ! 〈tr',vargs〉 ← trace_map … (λe. eval_expr ge e en sp m) args;
     180        ! 〈tr',vargs〉 ← trace_map … (λe. match e with [ dp ty e ⇒ eval_expr ge ? e en sp m ]) args;
    181181        ret ? 〈tr ⧺ tr', Callstate fd vargs m (Kcall dst f sp en k)〉
    182182    | St_tailcall ef args ⇒
    183         ! 〈tr,vf〉 ← eval_expr ge ef en sp m;
     183        ! 〈tr,vf〉 ← eval_expr ge ? ef en sp m;
    184184        ! fd ← opt_to_res … (msg BadFunctionValue) (find_funct ?? ge vf);
    185         ! 〈tr',vargs〉 ← trace_map … (λe. eval_expr ge e en sp m) args;
     185        ! 〈tr',vargs〉 ← trace_map … (λe. match e with [ dp ty e ⇒ eval_expr ge ? e en sp m ]) args;
    186186        ret ? 〈tr ⧺ tr', Callstate fd vargs (free m sp) (call_cont k)〉
    187187       
    188188    | St_seq s1 s2 ⇒ ret ? 〈E0, State f s1 en m sp (Kseq s2 k)〉
    189     | St_ifthenelse e strue sfalse ⇒
    190         ! 〈tr,v〉 ← eval_expr ge e en sp m;
     189    | St_ifthenelse _ _ e strue sfalse ⇒
     190        ! 〈tr,v〉 ← eval_expr ge ? e en sp m;
    191191        ! b ← eval_bool_of_val v;
    192192        ret ? 〈tr, State f (if b then strue else sfalse) en m sp k〉
     
    196196        ! k' ← k_exit n k;
    197197        ret ? 〈E0, State f St_skip en m sp k'〉
    198     | St_switch e cs default ⇒
    199         ! 〈tr,v〉 ← eval_expr ge e en sp m;
     198    | St_switch _ _ e cs default ⇒
     199        ! 〈tr,v〉 ← eval_expr ge ? e en sp m;
    200200        match v with
    201201        [ Vint i ⇒
     
    208208        [ None ⇒ ret ? 〈E0, Returnstate (None ?) (free m sp) (call_cont k)〉
    209209        | Some e ⇒
    210             ! 〈tr,v〉 ← eval_expr ge e en sp m;
    211             ret ? 〈tr, Returnstate (Some ? v) (free m sp) (call_cont k)〉
     210            match e with [ dp ty e ⇒
     211              ! 〈tr,v〉 ← eval_expr ge ? e en sp m;
     212              ret ? 〈tr, Returnstate (Some ? v) (free m sp) (call_cont k)〉
     213            ]
    212214        ]
    213215    | St_label l s' ⇒ ret ? 〈E0, State f s' en m sp k〉
  • src/Cminor/syntax.ma

    r878 r880  
    33include "common/CostLabel.ma".
    44
    5 inductive expr : Type[0] ≝
    6 | Id : ident → expr
    7 | Cst : constant → expr
    8 | Op1 : unary_operation → expr → expr
    9 | Op2 : binary_operation → expr → expr → expr
    10 | Mem : memory_chunk → expr → expr
    11 | Cond : expr → expr → expr → expr
    12 | Ecost : costlabel → expr → expr.
     5(* TODO: consider making the typing stricter. *)
     6
     7inductive expr : typ → Type[0] ≝
     8| Id : ∀t. ident → expr t
     9| Cst : ∀t. constant → expr t
     10| Op1 : ∀t,t'. unary_operation → expr t → expr t'
     11| Op2 : ∀t1,t2,t'. binary_operation → expr t1 → expr t2 → expr t'
     12| Mem : ∀t. memory_chunk → expr (ASTptr Any) → expr t
     13| Cond : ∀sz,sg,t. expr (ASTint sz sg) → expr t → expr t → expr t
     14| Ecost : ∀t. costlabel → expr t → expr t.
    1315
    1416inductive stmt : Type[0] ≝
    1517| St_skip : stmt
    16 | St_assign : ident → expr → stmt
    17 | St_store : memory_chunk → expr → expr → stmt
     18| St_assign : ∀t. ident → expr t → stmt
     19| St_store : ∀t. memory_chunk → expr (ASTptr Any) → expr t → stmt
    1820(* ident for returned value, expression to identify fn, args. *)
    19 | St_call : option ident → expr → list expr → stmt
    20 | St_tailcall : expr → list expr → stmt
     21| St_call : option ident → expr (ASTptr Code) → list (Σt. expr t) → stmt
     22| St_tailcall : expr (ASTptr Code) → list (Σt. expr t) → stmt
    2123| St_seq : stmt → stmt → stmt
    22 | St_ifthenelse : expr → stmt → stmt → stmt
     24| St_ifthenelse : ∀sz,sg. expr (ASTint sz sg) → stmt → stmt → stmt
    2325| St_loop : stmt → stmt
    2426| St_block : stmt → stmt
    2527| St_exit : nat → stmt
    2628(* expr to switch on, table of 〈switch value, #blocks to exit〉, default *)
    27 | St_switch : expr → list (int × nat) → nat → stmt
    28 | St_return : option expr → stmt
     29| St_switch : ∀sz,sg. expr (ASTint sz sg) → list (int × nat) → nat → stmt
     30| St_return : option (Σt. expr t) → stmt
    2931| St_label : ident → stmt → stmt
    3032| St_goto : ident → stmt
  • src/Cminor/toRTLabs.ma

    r816 r880  
    6767                       (f_stacksize f) (f_graph f) (f_entry f) (f_exit f)〉.
    6868
    69 let rec expr_yields_pointer (e:expr) (ptrs:list ident) : bool ≝
     69let rec expr_yields_pointer (ty:typ) (e:expr ty) (ptrs:list ident) on e : bool ≝
    7070match e with
    71 [ Id i ⇒ exists ? (eq_identifier ? i) ptrs
    72 | Cst c ⇒ match c with [ Oaddrsymbol _ _ ⇒ true | Oaddrstack _ ⇒ true | _ ⇒ false ]
    73 | Op1 op e' ⇒
     71[ Id _ i ⇒ exists ? (eq_identifier ? i) ptrs
     72| Cst _ c ⇒ match c with [ Oaddrsymbol _ _ ⇒ true | Oaddrstack _ ⇒ true | _ ⇒ false ]
     73| Op1 _ _ op e' ⇒
    7474    match op with
    75     [ Oid ⇒ expr_yields_pointer e' ptrs
     75    [ Oid ⇒ expr_yields_pointer ? e' ptrs
    7676    | Optrofint _ ⇒ true
    7777    | _ ⇒ false
    7878    ]
    79 | Op2 op e1 e2 ⇒
     79| Op2 _ _ _ op e1 e2 ⇒
    8080    match op with
    8181    [ Oaddp ⇒ true
     
    8383    | _ ⇒ false
    8484    ]
    85 | Mem q e' ⇒
     85| Mem _ q e' ⇒
    8686    match q with
    8787    [ Mpointer _ ⇒ true
     
    8989    ]
    9090(* Both branches ought to be the same? *)
    91 | Cond e' e1 e2 ⇒ (expr_yields_pointer e1 ptrs) ∨ (expr_yields_pointer e2 ptrs)
    92 | Ecost _ e' ⇒ expr_yields_pointer e' ptrs
     91| Cond _ _ _ e' e1 e2 ⇒ (expr_yields_pointer ? e1 ptrs) ∨ (expr_yields_pointer ? e2 ptrs)
     92| Ecost _ _ e' ⇒ expr_yields_pointer ? e' ptrs
    9393].
    9494
    9595axiom UnknownVariable : String.
    9696
    97 definition choose_reg : env → expr → list ident → internal_function → res (register × internal_function) ≝
    98 λenv,e,ptrs,f.
     97definition choose_reg : env → ∀t.expr t → list ident → internal_function → res (register × internal_function) ≝
     98λenv,ty,e,ptrs,f.
    9999  match e with
    100   [ Id i ⇒
     100  [ Id _ i ⇒
    101101      do r ← opt_to_res … [MSG UnknownVariable; CTX ? i] (lookup … env i);
    102102      OK ? 〈r, f〉
    103103  | _ ⇒
    104       if expr_yields_pointer e ptrs then fresh_ptr_reg f else fresh_reg f
     104      if expr_yields_pointer ? e ptrs then fresh_ptr_reg f else fresh_reg f
    105105  ].
    106106
    107 definition choose_regs : env → list expr → list ident → internal_function → res (list register × internal_function) ≝
     107definition choose_regs : env → list (Σt:typ.expr t) → list ident → internal_function → res (list register × internal_function) ≝
    108108λenv,es,ptrs,f.
    109   foldr ?? (λe,acc. do 〈rs,f〉 ← acc;
    110                     do 〈r,f'〉 ← choose_reg env e ptrs f;
    111                     OK ? 〈r::rs,f'〉) (OK ? 〈[ ], f〉) es.
     109  foldr (Σt:typ.expr t) ?
     110    (λe,acc. do 〈rs,f〉 ← acc;
     111             do 〈r,f'〉 ← match e with [ dp t e ⇒ choose_reg env t e ptrs f ];
     112             OK ? 〈r::rs,f'〉) (OK ? 〈[ ], f〉) es.
    112113
    113114axiom BadCminorProgram : String.
    114115
    115 let rec add_expr (env:env) (e:expr) (dst:register) (ptrs:list ident) (f:internal_function) on e: res internal_function ≝
     116let rec add_expr (env:env) (ty:typ) (e:expr ty) (dst:register) (ptrs:list ident) (f:internal_function) on e: res internal_function ≝
    116117match e with
    117 [ Id i ⇒
     118[ Id _ i ⇒
    118119    do r ← opt_to_res … [MSG UnknownVariable; CTX ? i] (lookup ?? env i);
    119120    match register_eq r dst with
     
    121122    | inr _ ⇒ add_fresh_to_graph (St_op1 Oid dst r) f
    122123    ]
    123 | Cst c ⇒ add_fresh_to_graph (St_const dst c) f
    124 | Op1 op e' ⇒
    125     do 〈r,f〉 ← choose_reg env e' ptrs f;
     124| Cst _ c ⇒ add_fresh_to_graph (St_const dst c) f
     125| Op1 _ _ op e' ⇒
     126    do 〈r,f〉 ← choose_reg env ? e' ptrs f;
    126127    do f ← add_fresh_to_graph (St_op1 op dst r) f;
    127     add_expr env e' r ptrs f
    128 | Op2 op e1 e2 ⇒
    129     do 〈r1,f〉 ← choose_reg env e1 ptrs f;
    130     do 〈r2,f〉 ← choose_reg env e2 ptrs f;
     128    add_expr env ? e' r ptrs f
     129| Op2 _ _ _ op e1 e2 ⇒
     130    do 〈r1,f〉 ← choose_reg env ? e1 ptrs f;
     131    do 〈r2,f〉 ← choose_reg env ? e2 ptrs f;
    131132    do f ← add_fresh_to_graph (St_op2 op dst r1 r2) f;
    132     do f ← add_expr env e2 r2 ptrs f;
    133     add_expr env e1 r1 ptrs f
    134 | Mem q e' ⇒
    135     add_with_addressing_internal env e' (λm,rs. St_load q m rs dst) ptrs f (add_expr env e')
    136 | Cond e' e1 e2 ⇒
     133    do f ← add_expr env ? e2 r2 ptrs f;
     134    add_expr env ? e1 r1 ptrs f
     135| Mem _ q e' ⇒
     136    add_with_addressing_internal env ? e' (λm,rs. St_load q m rs dst) ptrs f (add_expr env ? e')
     137| Cond _ _ _ e' e1 e2 ⇒
    137138    let resume_at ≝ f_entry f in
    138     do f ← add_expr env e2 dst ptrs f;
     139    do f ← add_expr env ? e2 dst ptrs f;
    139140    let lfalse ≝ f_entry f in
    140141    do f ← add_fresh_to_graph (λ_.St_skip resume_at) f;
    141     do f ← add_expr env e1 dst ptrs f;
    142     add_branch_internal env e' (f_entry f) lfalse ptrs f (add_expr env e')
    143 | Ecost l e' ⇒
    144     do f ← add_expr env e' dst ptrs f;
     142    do f ← add_expr env ? e1 dst ptrs f;
     143    add_branch_internal env ? e' (f_entry f) lfalse ptrs f (add_expr env ? e')
     144| Ecost _ l e' ⇒
     145    do f ← add_expr env ? e' dst ptrs f;
    145146    add_fresh_to_graph (St_cost l) f
    146147   
     
    149150   add_<whatever> afterwards. *)
    150151]
    151 and add_with_addressing_internal (env:env) (e:expr)
     152and add_with_addressing_internal (env:env) (ty:typ) (e:expr ty)
    152153                          (s:∀m:addressing. addr m → label → statement)
    153154                          (ptrs:list ident)
     
    156157                          on e : res internal_function ≝
    157158let add_default : unit → res internal_function ≝ λ_.
    158     do 〈r, f〉 ← choose_reg env e ptrs f;
     159    do 〈r, f〉 ← choose_reg env ? e ptrs f;
    159160    do f ← add_fresh_to_graph (s (Aindexed zero) [[ r ]]) f;
    160161    termination_hack r ptrs f
    161162in
    162163match e with
    163 [ Cst c ⇒
     164[ Cst _ c ⇒
    164165    match c with
    165166    [ Oaddrsymbol id i ⇒ add_fresh_to_graph (s (Aglobal id i) [[ ]]) f
     
    167168    | _ ⇒ Error ? (msg BadCminorProgram) (* int and float constants are nonsense here *)
    168169    ]
    169 | Op2 op e1 e2 ⇒
     170| Op2 _ _ _ op e1 e2 ⇒
    170171    match op with
    171172    [ Oaddp ⇒
    172173        let add_generic_addp : unit → res internal_function ≝ λ_.
    173           do 〈r1, f〉 ← choose_reg env e1 ptrs f;
    174           do 〈r2, f〉 ← choose_reg env e2 ptrs f;
     174          do 〈r1, f〉 ← choose_reg env ? e1 ptrs f;
     175          do 〈r2, f〉 ← choose_reg env ? e2 ptrs f;
    175176          do f ← add_fresh_to_graph (s Aindexed2 [[ r1 ; r2 ]]) f;
    176           do f ← add_expr env e2 r2 ptrs f;
    177           add_expr env e1 r1 ptrs f
     177          do f ← add_expr env ? e2 r2 ptrs f;
     178          add_expr env ? e1 r1 ptrs f
    178179        in
    179180        match e1 with
    180         [ Cst c ⇒
     181        [ Cst _ c ⇒
    181182            match c with
    182183            [ Oaddrsymbol id i ⇒
    183                 do 〈r, f〉 ← choose_reg env e ptrs f;
     184                do 〈r, f〉 ← choose_reg env ? e ptrs f;
    184185                do f ← add_fresh_to_graph (s (Abased id i) [[ r ]]) f;
    185                 add_expr env e2 r ptrs f
     186                add_expr env ? e2 r ptrs f
    186187            | _ ⇒ add_generic_addp it
    187188            ]
     
    193194]
    194195(* and again *)
    195 and add_branch_internal (env:env) (e:expr) (ltrue:label) (lfalse:label) (ptrs:list ident) (f:internal_function)
     196and add_branch_internal (env:env) (ty:typ) (e:expr ty) (ltrue:label) (lfalse:label) (ptrs:list ident) (f:internal_function)
    196197        (termination_hack_add_expr : register → list ident → internal_function → res internal_function) on e : res internal_function ≝
    197198match e with
    198 [ Id i ⇒
     199[ Id _ i ⇒
    199200    do r ← opt_to_res … [MSG UnknownVariable; CTX ? i] (lookup ?? env i);
    200201    add_fresh_to_graph (λ_. St_cond1 Oid r ltrue lfalse) f
    201 | Cst c ⇒
     202| Cst _ c ⇒
    202203    add_fresh_to_graph (λ_. St_condcst c ltrue lfalse) f
    203 | Op1 op e' ⇒
    204     do 〈r,f〉 ← choose_reg env e' ptrs f;
     204| Op1 _ _ op e' ⇒
     205    do 〈r,f〉 ← choose_reg env ? e' ptrs f;
    205206    do f ← add_fresh_to_graph (λ_. St_cond1 op r ltrue lfalse) f;
    206     add_expr env e' r ptrs f
    207 | Op2 op e1 e2 ⇒
    208     do 〈r1,f〉 ← choose_reg env e1 ptrs f;
    209     do 〈r2,f〉 ← choose_reg env e2 ptrs f;
     207    add_expr env ? e' r ptrs f
     208| Op2 _ _ _ op e1 e2 ⇒
     209    do 〈r1,f〉 ← choose_reg env ? e1 ptrs f;
     210    do 〈r2,f〉 ← choose_reg env ? e2 ptrs f;
    210211    do f ← add_fresh_to_graph (λ_. St_cond2 op r1 r2 ltrue lfalse) f;
    211     do f ← add_expr env e2 r2 ptrs f;
    212     add_expr env e1 r1 ptrs f
     212    do f ← add_expr env ? e2 r2 ptrs f;
     213    add_expr env ? e1 r1 ptrs f
    213214| _ ⇒
    214     do 〈r,f〉 ← choose_reg env e ptrs f;
     215    do 〈r,f〉 ← choose_reg env ? e ptrs f;
    215216    do f ← add_fresh_to_graph (λ_. St_cond1 Oid r ltrue lfalse) f;
    216217    termination_hack_add_expr r ptrs f
     
    219220(* See comment above. *)
    220221definition add_with_addressing ≝
    221 λenv,e,s,ptrs,f. add_with_addressing_internal env e s ptrs f (add_expr env e).
     222λenv,ty,e,s,ptrs,f. add_with_addressing_internal env ty e s ptrs f (add_expr env ty e).
    222223definition add_branch ≝
    223 λenv,e,ltrue,lfalse,ptrs,f. add_branch_internal env e ltrue lfalse ptrs f (add_expr env e).
     224λenv,ty,e,ltrue,lfalse,ptrs,f. add_branch_internal env ty e ltrue lfalse ptrs f (add_expr env ty e).
    224225
    225226(* This shouldn't occur; maybe use vectors? *)
    226227axiom WrongNumberOfArguments : String.
    227228
    228 let rec add_exprs (env:env) (es:list expr) (dsts:list register) (ptrs:list ident) (f:internal_function) on es: res internal_function ≝
     229let rec add_exprs (env:env) (es:list (Σt:typ.expr t)) (dsts:list register) (ptrs:list ident) (f:internal_function) on es: res internal_function ≝
    229230match es with
    230231[ nil ⇒ match dsts with [ nil ⇒ OK ? f | cons _ _ ⇒ Error ? (msg WrongNumberOfArguments) ]
     
    234235    | cons r rt ⇒
    235236        do f ← add_exprs env et rt ptrs f;
    236         add_expr env e r ptrs f
     237        match e with [ dp ty e ⇒ add_expr env ty e r ptrs f ]
    237238    ]
    238239].
     
    244245match s with
    245246[ St_skip ⇒ OK ? f
    246 | St_assign x e ⇒
     247| St_assign _ x e ⇒
    247248    do dst ← opt_to_res … [MSG UnknownVariable; CTX ? x] (lookup ?? env x);
    248     add_expr env e dst ptrs f
    249 | St_store q e1 e2 ⇒
    250     do 〈val_reg, f〉 ← choose_reg env e2 ptrs f;
    251     do f ← add_with_addressing env e1 (λm,rs. St_store q m rs val_reg) ptrs f;
    252     add_expr env e2 val_reg ptrs f
     249    add_expr env ? e dst ptrs f
     250| St_store _ q e1 e2 ⇒
     251    do 〈val_reg, f〉 ← choose_reg env ? e2 ptrs f;
     252    do f ← add_with_addressing env ? e1 (λm,rs. St_store q m rs val_reg) ptrs f;
     253    add_expr env ? e2 val_reg ptrs f
    253254| St_call return_opt_id e args ⇒
    254255    do return_opt_reg ←
     
    260261    do f ←
    261262      match e with
    262       [ Id id ⇒ add_fresh_to_graph (St_call_id id args_regs return_opt_reg) f
     263      [ Id _ id ⇒ add_fresh_to_graph (St_call_id id args_regs return_opt_reg) f
    263264      | _ ⇒
    264         do 〈fnr, f〉 ← choose_reg env e ptrs f;
     265        do 〈fnr, f〉 ← choose_reg env ? e ptrs f;
    265266        do f ← add_fresh_to_graph (St_call_ptr fnr args_regs return_opt_reg) f;
    266         add_expr env e fnr ptrs f
     267        add_expr env ? e fnr ptrs f
    267268      ];
    268269    add_exprs env args args_regs ptrs f
     
    271272    do f ←
    272273      match e with
    273       [ Id id ⇒ add_fresh_to_graph (λ_. St_tailcall_id id args_regs) f
     274      [ Id _ id ⇒ add_fresh_to_graph (λ_. St_tailcall_id id args_regs) f
    274275      | _ ⇒
    275         do 〈fnr, f〉 ← choose_reg env e ptrs f;
     276        do 〈fnr, f〉 ← choose_reg env ? e ptrs f;
    276277        do f ← add_fresh_to_graph (λ_. St_tailcall_ptr fnr args_regs) f;
    277         add_expr env e fnr ptrs f
     278        add_expr env ? e fnr ptrs f
    278279      ];
    279280    add_exprs env args args_regs ptrs f
     
    281282    do f ← add_stmt env label_env s2 exits ptrs f;
    282283    add_stmt env label_env s1 exits ptrs f
    283 | St_ifthenelse e s1 s2 ⇒
     284| St_ifthenelse _ _ e s1 s2 ⇒
    284285    let l_next ≝ f_entry f in
    285286    do f ← add_stmt env label_env s2 exits ptrs f;
     
    287288    do f ← add_fresh_to_graph ? (* XXX: fails, but works if applied afterwards: λ_. St_skip l_next*) f;
    288289    do f ← add_stmt env label_env s1 exits ptrs f;
    289     add_branch env e (f_entry f) l2 ptrs f
     290    add_branch env ? e (f_entry f) l2 ptrs f
    290291| St_loop s ⇒
    291292    do f ← add_loop_label_to_graph f;
     
    298299    do l ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits);
    299300    add_fresh_to_graph (* XXX another: λ_. St_skip l*)? f
    300 | St_switch e tab n ⇒
    301     do 〈r,f〉 ← choose_reg env e ptrs f;
     301| St_switch _ _ e tab n ⇒
     302    do 〈r,f〉 ← choose_reg env ? e ptrs f;
    302303    do l_default ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits);
    303304    do f ← add_fresh_to_graph (* XXX grrrr: λ_. St_skip l_default*)? f;
     
    309310      do f ← add_fresh_to_graph (St_cond2 (Ocmpu Ceq) (* signed? *) r cr l_case) f;
    310311      add_fresh_to_graph (St_const cr (Ointconst i)) f) (OK ? f) tab;
    311     add_expr env e r ptrs f
     312    add_expr env ? e r ptrs f
    312313| St_return opt_e ⇒
    313314    do f ← add_fresh_to_graph (λ_. St_return) f;
     
    317318        match f_result f with
    318319        [ None ⇒ Error ? (msg ReturnMismatch)
    319         | Some r ⇒ add_expr env e r ptrs f
     320        | Some r ⇒ match e with [ dp ty e ⇒ add_expr env ? e r ptrs f ]
    320321        ]
    321322    ]
     
    343344match s with
    344345[ St_seq s1 s2 ⇒ (labels_of s1) @ (labels_of s2)
    345 | St_ifthenelse _ s1 s2 ⇒ (labels_of s1) @ (labels_of s2)
     346| St_ifthenelse _ _ _ s1 s2 ⇒ (labels_of s1) @ (labels_of s2)
    346347| St_loop s ⇒ labels_of s
    347348| St_block s ⇒ labels_of s
  • src/common/AST.ma

    r879 r880  
    171171  | Mfloat64 : memory_chunk        (*r 64-bit double-precision float *)
    172172  | Mpointer : region → memory_chunk. (* pointer addressing given region *)
     173
     174definition typ_of_memory_chunk : memory_chunk → typ ≝
     175λc. match c with
     176[ Mint8signed ⇒ ASTint I8 Signed
     177| Mint8unsigned ⇒ ASTint I8 Unsigned
     178| Mint16signed ⇒ ASTint I16 Signed
     179| Mint16unsigned ⇒ ASTint I16 Unsigned
     180| Mint32 ⇒ ASTint I32 Unsigned (* XXX signed? *)
     181| Mfloat32 ⇒ ASTfloat F32
     182| Mfloat64 ⇒ ASTfloat F64
     183| Mpointer r ⇒ ASTptr r
     184].
    173185
    174186(* * Initialization data for global variables. *)
Note: See TracChangeset for help on using the changeset viewer.