Changeset 880 for src/Clight/Cexec.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/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)) ≝
Note: See TracChangeset for help on using the changeset viewer.