Ignore:
Timestamp:
Jan 25, 2011, 6:22:21 PM (9 years ago)
Author:
campbell
Message:

Tcomp_ptr should take the memory region and use that to calculate its size.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/C-semantics/Csyntax.ma

    r480 r481  
    6969  argument gives the names and types of the members.  The identifier
    7070  [id] is a local name which can be used in conjuction with the
    71   [Tcomp_ptr] constructor to express recursive types.  [Tcomp_ptr id]
     71  [Tcomp_ptr] constructor to express recursive types.  [Tcomp_ptr rg id]
    7272  stands for a pointer type to the nearest enclosing [Tstruct]
    73   or [Tunion] type named [id].  For instance. the structure [s1]
    74   defined above in C is expressed by
     73  or [Tunion] type named [id] in memory region [rg].  For instance.
     74  the structure [s1] defined above in C is expressed by
    7575<<
    7676  Tstruct "s1" (Fcons "n" (Tint I32 Signed)
    77                (Fcons "next" (Tcomp_ptr "id")
     77               (Fcons "next" (Tcomp_ptr Any "id")
    7878               Fnil))
    7979>>
     
    9292  | Tstruct: ident → fieldlist → type   (**r struct types *)
    9393  | Tunion: ident → fieldlist → type    (**r union types *)
    94   | Tcomp_ptr: ident → type             (**r pointer to named struct or union *)
     94  | Tcomp_ptr: region → ident → type    (**r pointer to named struct or union *)
    9595
    9696with typelist : Type ≝
     
    113113  (st:∀i,fl. P (Tstruct i fl))
    114114  (un:∀i,fl. P (Tunion i fl))
    115   (cp:∀i. P (Tcomp_ptr i))
     115  (cp:∀rg,i. P (Tcomp_ptr rg i))
    116116  (t:type) on t : P t ≝
    117117  match t return λt'.P t' with
     
    124124  | Tstruct i fs ⇒ st i fs
    125125  | Tunion i fs ⇒ un i fs
    126   | Tcomp_ptr i ⇒ cp i
     126  | Tcomp_ptr rg i ⇒ cp rg i
    127127  ].
    128128 
     
    361361
    362362(* * Natural alignment of a type, in bytes. *)
    363 
     363(* FIXME: these are old values for 32 bit machines *)
    364364nlet rec alignof (t: type) : Z ≝
    365365  match t return λ_.Z (* XXX appears to infer nat otherwise *) with
     
    372372  | Tstruct _ fld ⇒ alignof_fields fld
    373373  | Tunion _ fld ⇒ alignof_fields fld
    374   | Tcomp_ptr _ ⇒ 4
     374  | Tcomp_ptr _ _ ⇒ 4
    375375  ]
    376376
     
    397397  (st:∀i,fl. Q fl → P (Tstruct i fl))
    398398  (un:∀i,fl. Q fl → P (Tunion i fl))
    399   (cp:∀i. P (Tcomp_ptr i))
     399  (cp:∀r,i. P (Tcomp_ptr r i))
    400400  (nl:Q Fnil)
    401401  (cs:∀i,t,f'. P t → Q f' → Q (Fcons i t f'))
     
    410410  | Tstruct i fs ⇒ st i fs (fieldlist_ind2 P Q vo it fl pt ar fn st un cp nl cs fs)
    411411  | Tunion i fs ⇒ un i fs (fieldlist_ind2 P Q vo it fl pt ar fn st un cp nl cs fs)
    412   | Tcomp_ptr i ⇒ cp i
     412  | Tcomp_ptr r i ⇒ cp r i
    413413  ]
    414414and fieldlist_ind2
     
    422422  (st:∀i,fl. Q fl → P (Tstruct i fl))
    423423  (un:∀i,fl. Q fl → P (Tunion i fl))
    424   (cp:∀i. P (Tcomp_ptr i))
     424  (cp:∀r,i. P (Tcomp_ptr r i))
    425425  (nl:Q Fnil)
    426426  (cs:∀i,t,f'. P t → Q f' → Q (Fcons i t f'))
     
    455455  | Tint i _ ⇒ match i return λ_.Z with [ I8 ⇒ 1 | I16 ⇒ 2 | I32 ⇒ 4 ]
    456456  | Tfloat f ⇒ match f return λ_.Z with [ F32 ⇒ 4 | F64 ⇒ 8 ]
    457   | Tpointer sp _ ⇒ sizeof_pointer sp
     457  | Tpointer r _ ⇒ sizeof_pointer r
    458458  | Tarray _ t' n ⇒ sizeof t' * Zmax 1 n
    459459  | Tfunction _ _ ⇒ 1
    460460  | Tstruct _ fld ⇒ align (Zmax 1 (sizeof_struct fld 0)) (alignof t)
    461461  | Tunion _ fld ⇒ align (Zmax 1 (sizeof_union fld)) (alignof t)
    462   | Tcomp_ptr _ ⇒ 4
     462  | Tcomp_ptr r _ ⇒ sizeof_pointer r
    463463  ]
    464464
     
    631631  | By_nothing: mode.
    632632
     633ndefinition access_mode_pointer : region → mode ≝ λr.
     634By_value (match r with
     635[ Any   ⇒ Mint24
     636| Data  ⇒ Mint8unsigned
     637| IData ⇒ Mint8unsigned
     638| PData ⇒ Mint8unsigned
     639| XData ⇒ Mint16unsigned
     640| Code ⇒ Mint16unsigned
     641]).
     642
    633643ndefinition access_mode : type → mode ≝ λty.
    634644  match ty with
     
    644654                            | F64 ⇒ By_value Mfloat64 ]
    645655  | Tvoid ⇒ By_nothing
    646   | Tpointer sp _ ⇒ By_value (match sp with [ Any ⇒ Mint24 | Data ⇒ Mint8unsigned | IData ⇒ Mint8unsigned | PData ⇒ Mint8unsigned | XData ⇒ Mint16unsigned | Code ⇒ Mint16unsigned ])
     656  | Tpointer r _ ⇒ access_mode_pointer r
    647657  | Tarray _ _ _ ⇒ By_reference
    648658  | Tfunction _ _ ⇒ By_reference
    649659  | Tstruct _ fList ⇒ By_nothing
    650660  | Tunion _ fList ⇒ By_nothing
    651   | Tcomp_ptr _ ⇒ By_value Mint32
     661  | Tcomp_ptr r _ ⇒ access_mode_pointer r
    652662  ].
    653663
Note: See TracChangeset for help on using the changeset viewer.