Changeset 127


Ignore:
Timestamp:
Sep 24, 2010, 10:31:34 AM (9 years ago)
Author:
campbell
Message:

Allow the storage of pointers in suitably large integers.

Location:
C-semantics
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/CexecIO.ma

    r125 r127  
    221221| Vptr p b ofs ⇒
    222222  Some ? (
    223     p ← match ty with [ Tpointer _ _ ⇒ OK ? something | Tarray _ _ _ ⇒ OK ? something | Tfunction _ _ ⇒ OK ? something | _ ⇒ Error ? ];:
    224     s' ← match ty' with [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code | _ ⇒ Error ? ];:
     223    u ← match ty with [ Tpointer _ _ ⇒ OK ? something | Tarray _ _ _ ⇒ OK ? something | Tfunction _ _ ⇒ OK ? something | _ ⇒ Error ? ];:
     224    s' ← match ty' with
     225         [ 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 ? ]
     228         | _ ⇒ Error ? ];:
    225229    if is_pointer_compat (block_space m b) s'
    226230    then OK ? (Vptr s' b ofs)
     
    238242      ##[ ncases ty' in es' ⊢ %; ##[ #e; ##| ##3,9: #a e; ##| ##2,4,6,7,8: #a b e; ##| #a b c e; ##]
    239243          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          ##]
    240253      ##| #Hty' Hty;
    241254          nwhd in match (is_pointer_compat ??) in ⊢ %;
  • C-semantics/Csem.ma

    r125 r127  
    401401
    402402ninductive type_pointable : type → Prop ≝
    403 | type_ptr_int : type_pointable (Tint I32 Unsigned)
     403          (* All integer sizes can represent at least one kind of pointer *)
     404| type_ptr_int : ∀sz. type_pointable (Tint sz Unsigned)
    404405| type_ptr_pointer : ∀s,t. type_pointable (Tpointer s t)
    405406| type_ptr_array : ∀s,t,n. type_pointable (Tarray s t n)
     
    407408
    408409ninductive type_space : type → memory_space → Prop ≝
    409 | type_spc_int : type_space (Tint I32 Unsigned) Any
     410| type_spc_int : ∀s,sz. sizeof_pointer s ≤ sizeof (Tint sz Unsigned) →
     411                           type_space (Tint sz Unsigned) s
    410412| type_spc_pointer : ∀s,t. type_space (Tpointer s t) s
    411413| type_spc_array : ∀s,t,n. type_space (Tarray s t n) s
     
    431433      cast m (Vptr psp b ofs) ty ty' (Vptr psp' b ofs)
    432434  | cast_pp_z: ∀m,ty,ty'.
    433       type_pointable ty → (* Don't care which space it is for the source type *)
     435      type_pointable ty →
    434436      type_pointable ty' →
    435437      cast m (Vint zero) ty ty' (Vint zero).
    436 (* XXX: other integers?
    437   | cast_nn_i: ∀m,n,t1,t2.     (**r no change in data representation *)
    438       neutral_for_cast t1 → neutral_for_cast t2 →
     438(* Perhaps a little too generous?  For example, some integers may not
     439   represent a valid generic pointer.
     440  | cast_pp_i: ∀m,n,ty,ty',t1,t2.     (**r no change in data representation *)
     441      type_pointable ty →
     442      type_pointable ty' →
     443      sizeof ty ≤ sizeof ty' →
    439444      cast m (Vint n) t1 t2 (Vint n).
    440445*)
     446
    441447(* * * Operational semantics *)
    442448
  • C-semantics/Csyntax.ma

    r126 r127  
    437437(* * Size of a type, in bytes. *)
    438438
     439ndefinition sizeof_pointer : memory_space → Z ≝
     440λsp. match sp with [ Data ⇒ 1 | IData ⇒ 1 | XData ⇒ 2 | Code ⇒ 2 | Any ⇒ 3 ].
     441
    439442nlet rec sizeof (t: type) : Z ≝
    440443  match t return λ_.Z with
     
    442445  | Tint i _ ⇒ match i return λ_.Z with [ I8 ⇒ 1 | I16 ⇒ 2 | I32 ⇒ 4 ]
    443446  | Tfloat f ⇒ match f return λ_.Z with [ F32 ⇒ 4 | F64 ⇒ 8 ]
    444   | Tpointer sp _ ⇒ match sp with [ Data ⇒ 1 | IData ⇒ 1 | XData ⇒ 2 | Code ⇒ 2 | Any ⇒ 4 ]
     447  | Tpointer sp _ ⇒ sizeof_pointer sp
    445448  | Tarray _ t' n ⇒ sizeof t' * Zmax 1 n
    446449  | Tfunction _ _ ⇒ 1
Note: See TracChangeset for help on using the changeset viewer.