Changeset 155


Ignore:
Timestamp:
Oct 6, 2010, 2:20:30 PM (9 years ago)
Author:
campbell
Message:

More sensible handling of integer types and pointer casts.

Location:
C-semantics
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/CexecIO.ma

    r152 r155  
    191191   napply cast_pp_z; //; nqed.
    192192
     193ndefinition ms_eq_dec : ∀s1,s2:memory_space. (s1 = s2) + (s1 ≠ s2).
     194#s1; ncases s1; #s2; ncases s2; /2/; @2; @; #H; ndestruct; nqed.
     195
    193196nlet rec exec_cast (m:mem) (v:val) (ty:type) (ty':type) : res (Σv':val. cast m v ty ty' v') ≝
    194197match v with
     
    199202    [ Tint sz2 si2 ⇒ Some ? (OK ? (Vint (cast_int_int sz2 si2 i)))
    200203    | Tfloat sz2 ⇒ Some ? (OK ? (Vfloat (cast_float_float sz2 (cast_int_float si1 i))))
    201     | Tpointer _ _ ⇒ Some (res val) (r ← try_cast_null m i ty ty';: OK val r) (* XXX: is this ok for non-null values? *)
    202     | Tarray _ _ _ ⇒ Some (res val) (r ← try_cast_null m i ty ty';: OK val r) (* XXX: is this ok for non-null values? *)
    203     | Tfunction _ _ ⇒ Some (res val) (r ← try_cast_null m i ty ty';: OK val r) (* XXX: is this ok for non-null values? *)
     204    | Tpointer _ _ ⇒ Some (res val) (r ← try_cast_null m i ty ty';: OK val r)
     205    | Tarray _ _ _ ⇒ Some (res val) (r ← try_cast_null m i ty ty';: OK val r)
     206    | Tfunction _ _ ⇒ Some (res val) (r ← try_cast_null m i ty ty';: OK val r)
    204207    | _ ⇒ Some ? (Error ?)
    205208    ]
    206   | Tpointer _ _ ⇒ Some (res val) (r ← try_cast_null m i ty ty';: OK val r) (* XXX: is this ok for non-null values? *)
    207   | Tarray _ _ _ ⇒ Some (res val) (r ← try_cast_null m i ty ty';: OK val r) (* XXX: is this ok for non-null values? *)
    208   | Tfunction _ _ ⇒ Some (res val) (r ← try_cast_null m i ty ty';: OK val r) (* XXX: is this ok for non-null values? *)
     209  | Tpointer _ _ ⇒ Some (res val) (r ← try_cast_null m i ty ty';: OK val r)
     210  | Tarray _ _ _ ⇒ Some (res val) (r ← try_cast_null m i ty ty';: OK val r)
     211  | Tfunction _ _ ⇒ Some (res val) (r ← try_cast_null m i ty ty';: OK val r)
    209212  | _ ⇒ Some ? (Error ?)
    210213  ]
     
    221224| Vptr p b ofs ⇒
    222225  Some ? (
    223     u ← match ty with [ Tpointer _ _ ⇒ OK ? something | Tarray _ _ _ ⇒ OK ? something | Tfunction _ _ ⇒ OK ? something | _ ⇒ Error ? ];:
     226    s ← match ty with [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code | _ ⇒ Error ? ];:
     227    u ← match ms_eq_dec p s with [ inl _ ⇒ OK ? something | inr _ ⇒ Error ? ];:
    224228    s' ← match ty' with
    225229         [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code
    226          | Tint sz sg ⇒ match sg with [ Signed ⇒ Error ? | Unsigned ⇒
    227              if Zleb (sizeof_pointer p) (sizeof ty') then OK ? p else Error ? ]
    228230         | _ ⇒ Error ? ];:
    229231    if is_pointer_compat (block_space m b) s'
    230232    then OK ? (Vptr s' b ofs)
    231233    else Error ?)
    232   (* XXX: maybe should allow some Tint? *)
    233234| _ ⇒ Some ? (Error ?)
    234235]. nwhd; //;
    235236##[ ##1,2,3,4,5,6: napply sig_bind_OK; #v'; #H; ndestruct; napply H;
    236 ##| napply bind_OK; #u1 tyok;
    237     napply bind_OK; #s' es';
    238     ncut (type_pointable ty);
    239     ##[ ncases ty in tyok ⊢ %; //;
    240       ##[ #e; ##| ##3,6: #a e; ##| ##2,4,5: #a b e; ##] nwhd in e:(??%?); ndestruct;
    241     ##| ncut (type_space ty' s');
    242       ##[ ncases ty' in es' ⊢ %; ##[ #e; ##| ##3,9: #a e; ##| ##2,4,6,7,8: #a b e; ##| #a b c e; ##]
    243           nwhd in e:(??%?); ndestruct; //;
    244           ncases b in e ⊢ %; #e; nwhd in e:(??%?); ndestruct;
    245           napply type_spc_int; napply Zleb_true_to_Zle;
    246           ncut (c0 = s'); ##[
    247             nelim (Zleb (sizeof_pointer c0) (sizeof (Tint a Unsigned))) in e;
    248             nnormalize; #e; ndestruct; //;
    249           ##| #e2; nrewrite > e2 in e;
    250               nelim (Zleb (sizeof_pointer s') (sizeof (Tint a Unsigned)));
    251               //; nnormalize; #e; ndestruct;
    252           ##]
    253       ##| #Hty' Hty;
    254           nwhd in match (is_pointer_compat ??) in ⊢ %;
    255           ncases (pointer_compat_dec (block_space m c1) s'); #Hcompat;
    256           nwhd; /2/;
    257       ##]
     237##| napply bind_OK; #s es;
     238    ncut (type_space ty s);
     239    ##[ ncases ty in es ⊢ %;
     240      ##[ #e; ##| ##3,9: #a e; ##| ##2,4,6,7,8: #a b e; ##| #a b c e; ##] nwhd in e:(??%?); ndestruct; //;
     241    ##| #Hty;
     242        napply bind_OK; #u1 eeq;
     243        napply bind_OK; #s' es';
     244        ncut (type_space ty' s');
     245        ##[ ncases ty' in es' ⊢ %; ##[ #e; ##| ##3,9: #a e; ##| ##2,4,6,7,8: #a b e; ##| #a b c e; ##]
     246            nwhd in e:(??%?); ndestruct; //;
     247        ##| #Hty';
     248            ncut (s = c0). nelim (ms_eq_dec c0 s) in eeq; //; nnormalize; #_; #e; ndestruct.
     249            #e; nrewrite < e;
     250            nwhd in match (is_pointer_compat ??) in ⊢ %;
     251            ncases (pointer_compat_dec (block_space m c1) s'); #Hcompat;
     252            nwhd; /2/;
     253        ##]
    258254    ##]
    259255##] nqed.
     
    487483ndefinition fs_eq_dec : ∀s1,s2:floatsize. (s1 = s2) + (s1 ≠ s2).
    488484#s1; ncases s1; #s2; ncases s2; /2/; @2; @; #H; ndestruct; nqed.
    489 ndefinition ms_eq_dec : ∀s1,s2:memory_space. (s1 = s2) + (s1 ≠ s2).
    490 #s1; ncases s1; #s2; ncases s2; /2/; @2; @; #H; ndestruct; nqed.
    491485
    492486nlet rec assert_type_eq (t1,t2:type) : res (t1 = t2) ≝
  • C-semantics/Csem.ma

    r127 r155  
    402402ninductive type_pointable : type → Prop ≝
    403403          (* All integer sizes can represent at least one kind of pointer *)
    404 | type_ptr_int : ∀sz. type_pointable (Tint sz Unsigned)
    405404| type_ptr_pointer : ∀s,t. type_pointable (Tpointer s t)
    406405| type_ptr_array : ∀s,t,n. type_pointable (Tarray s t n)
     
    408407
    409408ninductive type_space : type → memory_space → Prop ≝
    410 | type_spc_int : ∀s,sz. sizeof_pointer s ≤ sizeof (Tint sz Unsigned) →
    411                            type_space (Tint sz Unsigned) s
    412409| type_spc_pointer : ∀s,t. type_space (Tpointer s t) s
    413410| type_spc_array : ∀s,t,n. type_space (Tarray s t n) s
     411(* XXX Is the following necessary? *)
    414412| type_spc_code : ∀tys,ty. type_space (Tfunction tys ty) Code.
    415413
     
    428426           (Vfloat (cast_float_float sz2 f))
    429427  | cast_pp: ∀m,psp,psp',ty,ty',b,ofs.
    430       type_pointable ty
     428      type_space ty psp
    431429      type_space ty' psp' →
    432430      pointer_compat (block_space m b) psp' →
    433431      cast m (Vptr psp b ofs) ty ty' (Vptr psp' b ofs)
     432  | cast_ip_z: ∀m,sz,sg,ty'.
     433      type_pointable ty' →
     434      cast m (Vint zero) (Tint sz sg) ty' (Vint zero)
    434435  | cast_pp_z: ∀m,ty,ty'.
    435436      type_pointable ty →
    436437      type_pointable ty' →
    437438      cast m (Vint zero) ty ty' (Vint zero).
     439(* Should probably also allow pointers to pass through sufficiently large
     440   unsigned integers. *)
    438441(* Perhaps a little too generous?  For example, some integers may not
    439442   represent a valid generic pointer.
Note: See TracChangeset for help on using the changeset viewer.