Changeset 481


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

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

Location:
Deliverables/D3.1/C-semantics
Files:
5 edited

Legend:

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

    r480 r481  
    422422    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
    423423    |  _ ⇒ inr ?? (nmk ? (λH.?)) ]
    424 | Tcomp_ptr i ⇒ match t2 return λt'. (Tcomp_ptr ? = t') + (Tcomp_ptr ? ≠ t')  with [ Tcomp_ptr i' ⇒
    425     match ident_eq i i' with [ inl e1 ⇒ inl ???
     424| Tcomp_ptr r i ⇒ match t2 return λt'. (Tcomp_ptr ? ? = t') + (Tcomp_ptr ? ? ≠ t')  with [ Tcomp_ptr r' i' ⇒
     425    match ms_eq_dec r r' with [ inl e1 ⇒
     426      match ident_eq i i' with [ inl e2 ⇒ inl ???
     427      | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
    426428    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
    427429    | _ ⇒ inr ?? (nmk ? (λH.?)) ]
  • Deliverables/D3.1/C-semantics/CexecComplete.ma

    r468 r481  
    267267  (st:∀i,fl. P (Tstruct i fl))
    268268  (un:∀i,fl. P (Tunion i fl))
    269   (cp:∀i. P (Tcomp_ptr i))
     269  (cp:∀r,i. P (Tcomp_ptr r i))
    270270  (nl:Q Tnil)
    271271  (cs:∀t,tl. P t → Q tl → Q (Tcons t tl))
     
    280280  | Tstruct i fs ⇒ st i fs
    281281  | Tunion i fs ⇒ un i fs
    282   | Tcomp_ptr i ⇒ cp i
     282  | Tcomp_ptr r i ⇒ cp r i
    283283  ]
    284284and typelist_ind2l
     
    292292  (st:∀i,fl. P (Tstruct i fl))
    293293  (un:∀i,fl. P (Tunion i fl))
    294   (cp:∀i. P (Tcomp_ptr i))
     294  (cp:∀r,i. P (Tcomp_ptr r i))
    295295  (nl:Q Tnil)
    296296  (cs:∀t,tl. P t → Q tl → Q (Tcons t tl))
  • Deliverables/D3.1/C-semantics/CexecSound.ma

    r399 r481  
    66ncases v; ##[ ##2: #i ##| ##3: #f ##| ##4: #sp b of ##]
    77nwhd; ##[ ##4: #H; nwhd in H:(??%?); ndestruct ##]
    8 ncases ty; ##[ ##2,11,20: #sz sg ##| ##3,12,21: #sz ##| ##4,13,22: #sp ty ##| ##5,14,23: #sp ty n ##| ##6,15,24: #args rty ##| ##7,8,16,17,25,26: #id fs ##| ##9,18,27: #id ##]
     8ncases ty; ##[ ##2,11,20: #sz sg ##| ##3,12,21: #sz ##| ##4,13,22: #sp ty ##| ##5,14,23: #sp ty n ##| ##6,15,24: #args rty ##| ##7,8,16,17,25,26: #id fs ##| ##9,18,27: #r id ##]
    99#H; nwhd in H:(??%?); ndestruct;
    1010##[ ##1,4: nlapply (eq_spec i zero); nelim (eq i zero);
     
    3535nlapply (eq_spec i zero); ncases (eq i zero);
    3636##[ #e; nrewrite > e;
    37     ncases ty; ##[ ##| #sz sg ##| #fs ##| #sp ty ##| #sp ty n ##| #args rty ##| #id fs ##| #id fs ##| #id ##]
     37    ncases ty; ##[ ##| #sz sg ##| #fs ##| #sp ty ##| #sp ty n ##| #args rty ##| #id fs ##| #id fs ##| #r id ##]
    3838    nwhd in ⊢ (??%? → ?); ##[ ##1,3,7,8,9: #H; ndestruct ##]
    39     ncases ty'; ##[ ##2,11,20,29: #sz' sg' ##| ##3,12,21,30: #sz' ##| ##4,13,22,31: #sp' ty' ##| ##5,14,23,32: #sp' ty' n' ##| ##6,15,24,33: #args' res' ##| ##7,8,16,17,25,26,34,35: #id' fs' ##| ##9,18,27,36: #id' ##]
     39    ncases ty'; ##[ ##2,11,20,29: #sz' sg' ##| ##3,12,21,30: #sz' ##| ##4,13,22,31: #sp' ty' ##| ##5,14,23,32: #sp' ty' n' ##| ##6,15,24,33: #args' res' ##| ##7,8,16,17,25,26,34,35: #id' fs' ##| ##9,18,27,36: #r id' ##]
    4040    nwhd in ⊢ (??%? → ?); #H; ndestruct (H);
    4141    ##[ ##1,5,9: napply cast_ip_z ##| ##*: napply cast_pp_z ##] //;
     
    5050##| #i; ncases ty;
    5151  ##[ #H; nwhd in H:(??%?); ndestruct;
    52   ##| ##3,9: #a; #H; nwhd in H:(??%?); ndestruct;
    53   ##| ##7,8: #a b; #H; nwhd in H:(??%?); ndestruct;
     52  ##| ##3: #a; #H; nwhd in H:(??%?); ndestruct;
     53  ##| ##7,8,9: #a b; #H; nwhd in H:(??%?); ndestruct;
    5454  ##| #sz1 si1; ncases ty';
    5555    ##[ #H; nwhd in H:(??%?); ndestruct;
    56     ##| ##3,9: #a; #H; nwhd in H:(??%?); ndestruct; //
    57     ##| ##2,7,8: #a b; #H; nwhd in H:(??%?); ndestruct; //
     56    ##| ##3: #a; #H; nwhd in H:(??%?); ndestruct; //
     57    ##| ##2,7,8,9: #a b; #H; nwhd in H:(??%?); ndestruct; //
    5858    ##| ##4,5,6: ##[ #sp ty''; nletin t ≝ (Tpointer sp ty'')
    5959                 ##| #sp ty'' n; nletin t ≝ (Tarray sp ty'' n)
     
    7676        ##]
    7777  ##]
    78 ##| #f; ncases ty;  ##[ ##3,9: #x; ##| ##2,4,6,7,8: #x y; ##| ##5: #x y z; ##]
    79                     ##[ ncases ty'; ##[ #e; ##| ##3,9: #a e; ##| ##2,4,6,7,8: #a b e; ##| #a b c e; ##]
     78##| #f; ncases ty;  ##[ ##3: #x; ##| ##2,4,6,7,8,9: #x y; ##| ##5: #x y z; ##]
     79                    ##[ ncases ty'; ##[ #e; ##| ##3: #a e; ##| ##2,4,6,7,8,9: #a b e; ##| #a b c e; ##]
    8080                        nwhd in e:(??%?); ndestruct; //;
    8181                    ##| ##*: #e; nwhd in e:(??%?); ndestruct
     
    8686    nelim (bind_inversion ????? e''); #s'; *; #es' e''';
    8787    ncut (type_space ty s);
    88     ##[ ncases ty in es:(??%?) ⊢ %; ##[ #e; ##| ##3,9: #a e; ##| ##2,4,6,7,8: #a b e; ##| #a b c e; ##]
     88    ##[ ncases ty in es:(??%?) ⊢ %; ##[ #e; ##| ##3: #a e; ##| ##2,4,6,7,8,9: #a b e; ##| #a b c e; ##]
    8989        nwhd in e:(??%?); ndestruct; //;
    9090    ##| #Hty;
    9191        ncut (type_space ty' s');
    92         ##[ ncases ty' in es' ⊢ %; ##[ #e; ##| ##3,9: #a e; ##| ##2,4,6,7,8: #a b e; ##| #a b c e; ##]
     92        ##[ ncases ty' in es' ⊢ %; ##[ #e; ##| ##3: #a e; ##| ##2,4,6,7,8,9: #a b e; ##| #a b c e; ##]
    9393            nwhd in e:(??%?); ndestruct; //;
    9494        ##| #Hty';
  • Deliverables/D3.1/C-semantics/Csem.ma

    r480 r481  
    993993| Tstruct a b ⇒ Tstruct a b
    994994| Tunion a b ⇒ Tunion a b
    995 | Tcomp_ptr a ⇒ Tcomp_ptr a
     995| Tcomp_ptr a b ⇒ Tcomp_ptr a b
    996996].
    997997
  • 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.