Ignore:
Timestamp:
Feb 11, 2011, 4:45:36 PM (9 years ago)
Author:
campbell
Message:

Make block type a little more abstract; remove knowledge about the old
representation for a pointer from the evaluation of lvalues.

File:
1 edited

Legend:

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

    r496 r498  
    464464  reference, the pointer [Vptr b ofs] is returned. *)
    465465
    466 let rec load_value_of_type (ty: type) (m: mem) (psp:region) (b: block) (ofs: int) : option val ≝
     466let rec load_value_of_type (ty: type) (m: mem) (b: block) (ofs: int) : option val ≝
    467467  match access_mode ty with
    468   [ By_value chunk ⇒ loadv chunk m (Vptr psp b ofs)
    469   | By_reference ⇒ Some ? (Vptr psp b ofs)
     468  [ By_value chunk ⇒ loadv chunk m (Vptr Any b ofs)
     469  | By_reference r ⇒ Some ? (Vptr r b ofs)
    470470  | By_nothing ⇒ None ?
    471471  ].
     
    476476  This is allowed only if [ty] indicates an access by value. *)
    477477
    478 let rec store_value_of_type (ty_dest: type) (m: mem) (psp:region) (loc: block) (ofs: int) (v: val) : option mem ≝
     478let rec store_value_of_type (ty_dest: type) (m: mem) (loc: block) (ofs: int) (v: val) : option mem ≝
    479479  match access_mode ty_dest with
    480   [ By_value chunk ⇒ storev chunk m (Vptr psp loc ofs) v
    481   | By_reference ⇒ None ?
     480  [ By_value chunk ⇒ storev chunk m (Vptr Any loc ofs) v
     481  | By_reference _ ⇒ None ?
    482482  | By_nothing ⇒ None ?
    483483  ].
     
    516516      ∀e,m,id,ty,params,v1,vl,b,m1,m2.
    517517      get ??? id e = Some ? b →
    518       store_value_of_type ty m Any b zero v1 = Some ? m1 →
     518      store_value_of_type ty m b zero v1 = Some ? m1 →
    519519      bind_parameters e m1 params vl m2 →
    520520      bind_parameters e m (〈id, ty〉 :: params) (v1 :: vl) m2.
    521 
    522 (* XXX: this doesn't look right - we're assigning arbitrary memory spaces to
    523    parameters? *)
    524521
    525522(* * Return the list of blocks in the codomain of [e]. *)
     
    567564  | eval_Econst_float:   ∀f,ty.
    568565      eval_expr ge e m (Expr (Econst_float f) ty) (Vfloat f) E0
    569   | eval_Elvalue: ∀a,ty,r,loc,ofs,v,tr.
    570       eval_lvalue ge e m (Expr a ty) r loc ofs tr →
    571       load_value_of_type ty m r loc ofs = Some ? v →
     566  | eval_Elvalue: ∀a,ty,loc,ofs,v,tr.
     567      eval_lvalue ge e m (Expr a ty) loc ofs tr →
     568      load_value_of_type ty m loc ofs = Some ? v →
    572569      eval_expr ge e m (Expr a ty) v tr
    573570  | eval_Eaddrof: ∀a,ty,r,loc,ofs,tr.
    574       eval_lvalue ge e m a r loc ofs tr →
    575       eval_expr ge e m (Expr (Eaddrof a) ty) (Vptr r loc ofs) tr
     571      eval_lvalue ge e m a loc ofs tr →
     572      eval_expr ge e m (Expr (Eaddrof a) (Tpointer r ty)) (Vptr r loc ofs) tr
    576573  | eval_Esizeof: ∀ty',ty.
    577574      eval_expr ge e m (Expr (Esizeof ty') ty) (Vint (repr (sizeof ty'))) E0
     
    628625  be representable in a pointer of region r. *)
    629626
    630 with eval_lvalue (*(ge:genv) (e:env) (m:mem)*) : expr → region → block → int → trace → Prop ≝
     627with eval_lvalue (*(ge:genv) (e:env) (m:mem)*) : expr → block → int → trace → Prop ≝
    631628  | eval_Evar_local:   ∀id,l,ty.
    632629      (* XXX notation? e!id*) get ??? id e = Some ? l →
    633       eval_lvalue ge e m (Expr (Evar id) ty) Any l zero E0
    634   | eval_Evar_global: ∀id,r,l,ty.
     630      eval_lvalue ge e m (Expr (Evar id) ty) l zero E0
     631  | eval_Evar_global: ∀id,l,ty.
    635632      (* XXX e!id *) get ??? id e = None ? →
    636       find_symbol ?? ge id = Some ? 〈r,l〉
    637       eval_lvalue ge e m (Expr (Evar id) ty) r 〈r,l〉 zero E0
     633      find_symbol ?? ge id = Some ? l
     634      eval_lvalue ge e m (Expr (Evar id) ty) l zero E0
    638635  | eval_Ederef: ∀a,ty,r,l,ofs,tr.
    639636      eval_expr ge e m a (Vptr r l ofs) tr →
    640       eval_lvalue ge e m (Expr (Ederef a) ty) r l ofs tr
    641  | eval_Efield_struct:   ∀a,i,ty,r,l,ofs,id,fList,delta,tr.
    642       eval_lvalue ge e m a r l ofs tr →
     637      eval_lvalue ge e m (Expr (Ederef a) ty) l ofs tr
     638    (* Aside: note that each block of memory is entirely contained within one
     639       memory region; hence adding a field offset will not produce a location
     640       outside of the original location's region. *)
     641 | eval_Efield_struct:   ∀a,i,ty,l,ofs,id,fList,delta,tr.
     642      eval_lvalue ge e m a l ofs tr →
    643643      typeof a = Tstruct id fList →
    644644      field_offset i fList = OK ? delta →
    645       eval_lvalue ge e m (Expr (Efield a i) ty) r l (add ofs (repr delta)) tr
    646  | eval_Efield_union:   ∀a,i,ty,r,l,ofs,id,fList,tr.
    647       eval_lvalue ge e m a r l ofs tr →
     645      eval_lvalue ge e m (Expr (Efield a i) ty) l (add ofs (repr delta)) tr
     646 | eval_Efield_union:   ∀a,i,ty,l,ofs,id,fList,tr.
     647      eval_lvalue ge e m a l ofs tr →
    648648      typeof a = Tunion id fList →
    649       eval_lvalue ge e m (Expr (Efield a i) ty) r l ofs tr.
     649      eval_lvalue ge e m (Expr (Efield a i) ty) l ofs tr.
    650650
    651651let rec eval_expr_ind (ge:genv) (e:env) (m:mem)
     
    653653  (eci:∀i,ty. P ??? (eval_Econst_int ge e m i ty))
    654654  (ecF:∀f,ty. P ??? (eval_Econst_float ge e m f ty))
    655   (elv:∀a,ty,psp,loc,ofs,v,tr,H1,H2. P ??? (eval_Elvalue ge e m a ty psp loc ofs v tr H1 H2))
     655  (elv:∀a,ty,loc,ofs,v,tr,H1,H2. P ??? (eval_Elvalue ge e m a ty loc ofs v tr H1 H2))
    656656  (ead:∀a,ty,psp,loc,ofs,tr,H. P ??? (eval_Eaddrof ge e m a ty psp loc ofs tr H))
    657657  (esz:∀ty',ty. P ??? (eval_Esizeof ge e m ty' ty))
     
    670670  [ eval_Econst_int i ty ⇒ eci i ty
    671671  | eval_Econst_float f ty ⇒ ecF f ty
    672   | eval_Elvalue a ty psp loc ofs v tr H1 H2 ⇒ elv a ty psp loc ofs v tr H1 H2
     672  | eval_Elvalue a ty loc ofs v tr H1 H2 ⇒ elv a ty loc ofs v tr H1 H2
    673673  | eval_Eaddrof a ty psp loc ofs tr H ⇒ ead a ty psp loc ofs tr H
    674674  | eval_Esizeof ty' ty ⇒ esz ty' ty
     
    688688
    689689let rec eval_lvalue_ind (ge:genv) (e:env) (m:mem)
    690   (P:∀a,psp,loc,ofs,tr. eval_lvalue ge e m a psp loc ofs tr → Prop)
    691   (lvl:∀id,l,ty,H. P ????? (eval_Evar_local ge e m id l ty H))
    692   (lvg:∀id,sp,l,ty,H1,H2. P ????? (eval_Evar_global ge e m id sp l ty H1 H2))
    693   (lde:∀a,ty,psp,l,ofs,tr,H. P ????? (eval_Ederef ge e m a ty psp l ofs tr H))
    694   (lfs:∀a,i,ty,psp,l,ofs,id,fList,delta,tr,H1,H2,H3. P a psp l ofs tr H1 → P ????? (eval_Efield_struct ge e m a i ty psp l ofs id fList delta tr H1 H2 H3))
    695   (lfu:∀a,i,ty,psp,l,ofs,id,fList,tr,H1,H2. P a psp l ofs tr H1 → P ????? (eval_Efield_union ge e m a i ty psp l ofs id fList tr H1 H2))
    696   (a:expr) (psp:region) (loc:block) (ofs:int) (tr:trace) (ev:eval_lvalue ge e m a psp loc ofs tr) on ev : P a psp loc ofs tr ev ≝
     690  (P:∀a,loc,ofs,tr. eval_lvalue ge e m a loc ofs tr → Prop)
     691  (lvl:∀id,l,ty,H. P ???? (eval_Evar_local ge e m id l ty H))
     692  (lvg:∀id,l,ty,H1,H2. P ???? (eval_Evar_global ge e m id l ty H1 H2))
     693  (lde:∀a,ty,psp,l,ofs,tr,H. P ???? (eval_Ederef ge e m a ty psp l ofs tr H))
     694  (lfs:∀a,i,ty,l,ofs,id,fList,delta,tr,H1,H2,H3. P a l ofs tr H1 → P ???? (eval_Efield_struct ge e m a i ty l ofs id fList delta tr H1 H2 H3))
     695  (lfu:∀a,i,ty,l,ofs,id,fList,tr,H1,H2. P a l ofs tr H1 → P ???? (eval_Efield_union ge e m a i ty l ofs id fList tr H1 H2))
     696  (a:expr) (loc:block) (ofs:int) (tr:trace) (ev:eval_lvalue ge e m a loc ofs tr) on ev : P a loc ofs tr ev ≝
    697697  match ev with
    698698  [ eval_Evar_local id l ty H ⇒ lvl id l ty H
    699   | eval_Evar_global id sp l ty H1 H2 ⇒ lvg id sp l ty H1 H2
     699  | eval_Evar_global id l ty H1 H2 ⇒ lvg id l ty H1 H2
    700700  | eval_Ederef a ty psp l ofs tr H ⇒ lde a ty psp l ofs tr H
    701   | eval_Efield_struct a i ty psp l ofs id fList delta tr H1 H2 H3 ⇒ lfs a i ty psp l ofs id fList delta tr H1 H2 H3 (eval_lvalue_ind ge e m P lvl lvg lde lfs lfu a psp l ofs tr H1)
    702   | eval_Efield_union a i ty psp l ofs id fList tr H1 H2 ⇒ lfu a i ty psp l ofs id fList tr H1 H2 (eval_lvalue_ind ge e m P lvl lvg lde lfs lfu a psp l ofs tr H1)
     701  | eval_Efield_struct a i ty l ofs id fList delta tr H1 H2 H3 ⇒ lfs a i ty l ofs id fList delta tr H1 H2 H3 (eval_lvalue_ind ge e m P lvl lvg lde lfs lfu a l ofs tr H1)
     702  | eval_Efield_union a i ty l ofs id fList tr H1 H2 ⇒ lfu a i ty l ofs id fList tr H1 H2 (eval_lvalue_ind ge e m P lvl lvg lde lfs lfu a l ofs tr H1)
    703703  ].
    704704
     
    712712    ∀x3: mem.
    713713     ∀x4: expr.
    714       ∀x5: region.
    715714       ∀x6: block.
    716715        ∀x7: int.
     
    718717          ∀P:
    719718            ∀_z1430: expr.
    720              ∀_z1429: region.
    721719              ∀_z1428: block. ∀_z1427: int. ∀_z1426: trace. Prop.
    722720           ∀_H1: ?.
     
    725723              ∀_H4: ?.
    726724               ∀_H5: ?.
    727                 ∀_Hterm: eval_lvalue x1 x2 x3 x4 x5 x6 x7 x8.
    728                  P x4 x5 x6 x7 x8
     725                ∀_Hterm: eval_lvalue x1 x2 x3 x4 x6 x7 x8.
     726                 P x4 x6 x7 x8
    729727:=
    730728  (λx1:genv.
     
    732730      (λx3:mem.
    733731        (λx4:expr.
    734           (λx5:region.
    735732            (λx6:block.
    736733              (λx7:int.
    737734                (λx8:trace.
    738735                  (λP:∀_z1430: expr.
    739                         ∀_z1429: region.
    740736                         ∀_z1428: block.
    741737                          ∀_z1427: int. ∀_z1426: trace. Prop.
     
    745741                          (λH4:?.
    746742                            (λH5:?.
    747                               (λHterm:eval_lvalue x1 x2 x3 x4 x5 x6 x7 x8.
     743                              (λHterm:eval_lvalue x1 x2 x3 x4 x6 x7 x8.
    748744                                ((λHcut:∀z1435: eq expr x4 x4.
    749                                           ∀z1434: eq region x5 x5.
    750745                                           ∀z1433: eq block x6 x6.
    751746                                            ∀z1432: eq int x7 x7.
    752747                                             ∀z1431: eq trace x8 x8.
    753                                               P x4 x5 x6 x7 x8.
     748                                              P x4 x6 x7 x8.
    754749                                   (Hcut (refl expr x4)
    755                                      (refl region x5) (refl block x6)
     750                                     (refl block x6)
    756751                                     (refl int x7) (refl trace x8)))
    757                                   ?)))))))))))))))).
    758 [ @(eval_lvalue_ind x1 x2 x3 (λa,psp,loc,ofs,tr,e. ∀e1:eq ? x4 a. ∀e2:eq ? x5 psp. ∀e3:eq ? x6 loc. ∀e4:eq ? x7 ofs. ∀e5:eq ? x8 tr. P a psp loc ofs tr) … Hterm)
     752                                  ?))))))))))))))).
     753[ @(eval_lvalue_ind x1 x2 x3 (λa,loc,ofs,tr,e. ∀e1:eq ? x4 a. ∀e3:eq ? x6 loc. ∀e4:eq ? x7 ofs. ∀e5:eq ? x8 tr. P a loc ofs tr) … Hterm)
    759754  [ @H1 | @H2 | @H3 | @H4 | @H5 ]
    760755| *: skip
     
    763758let rec eval_expr_ind2 (ge:genv) (e:env) (m:mem)
    764759  (P:∀a,v,tr. eval_expr ge e m a v tr → Prop)
    765   (Q:∀a,psp,loc,ofs,tr. eval_lvalue ge e m a psp loc ofs tr → Prop)
     760  (Q:∀a,loc,ofs,tr. eval_lvalue ge e m a loc ofs tr → Prop)
    766761  (eci:∀i,ty. P ??? (eval_Econst_int ge e m i ty))
    767762  (ecF:∀f,ty. P ??? (eval_Econst_float ge e m f ty))
    768   (elv:∀a,ty,psp,loc,ofs,v,tr,H1,H2. Q (Expr a ty) psp loc ofs tr H1 → P ??? (eval_Elvalue ge e m a ty psp loc ofs v tr H1 H2))
    769   (ead:∀a,ty,psp,loc,ofs,tr,H. Q a psp loc ofs tr H → P ??? (eval_Eaddrof ge e m a ty psp loc ofs tr H))
     763  (elv:∀a,ty,loc,ofs,v,tr,H1,H2. Q (Expr a ty) loc ofs tr H1 → P ??? (eval_Elvalue ge e m a ty loc ofs v tr H1 H2))
     764  (ead:∀a,ty,psp,loc,ofs,tr,H. Q a loc ofs tr H → P ??? (eval_Eaddrof ge e m a ty psp loc ofs tr H))
    770765  (esz:∀ty',ty. P ??? (eval_Esizeof ge e m ty' ty))
    771766  (eun:∀op,a,ty,v1,v,tr,H1,H2. P a v1 tr H1 → P ??? (eval_Eunop ge e m op a ty v1 v tr H1 H2))
     
    779774  (ecs:∀a,ty,ty',v1,v,tr,H1,H2. P a v1 tr H1 → P ??? (eval_Ecast ge e m a ty ty' v1 v tr H1 H2))
    780775  (eco:∀a,ty,v,l,tr,H. P a v tr H → P ??? (eval_Ecost ge e m a ty v l tr H))
    781   (lvl:∀id,l,ty,H. Q ????? (eval_Evar_local ge e m id l ty H))
    782   (lvg:∀id,sp,l,ty,H1,H2. Q ????? (eval_Evar_global ge e m id sp l ty H1 H2))
    783   (lde:∀a,ty,psp,l,ofs,tr,H. P a (Vptr psp l ofs) tr H → Q ????? (eval_Ederef ge e m a ty psp l ofs tr H))
    784   (lfs:∀a,i,ty,psp,l,ofs,id,fList,delta,tr,H1,H2,H3. Q a psp l ofs tr H1 → Q ????? (eval_Efield_struct ge e m a i ty psp l ofs id fList delta tr H1 H2 H3))
    785   (lfu:∀a,i,ty,psp,l,ofs,id,fList,tr,H1,H2. Q a psp l ofs tr H1 → Q ????? (eval_Efield_union ge e m a i ty psp l ofs id fList tr H1 H2))
     776  (lvl:∀id,l,ty,H. Q ???? (eval_Evar_local ge e m id l ty H))
     777  (lvg:∀id,l,ty,H1,H2. Q ???? (eval_Evar_global ge e m id l ty H1 H2))
     778  (lde:∀a,ty,psp,l,ofs,tr,H. P a (Vptr psp l ofs) tr H → Q ???? (eval_Ederef ge e m a ty psp l ofs tr H))
     779  (lfs:∀a,i,ty,l,ofs,id,fList,delta,tr,H1,H2,H3. Q a l ofs tr H1 → Q ???? (eval_Efield_struct ge e m a i ty l ofs id fList delta tr H1 H2 H3))
     780  (lfu:∀a,i,ty,l,ofs,id,fList,tr,H1,H2. Q a l ofs tr H1 → Q ???? (eval_Efield_union ge e m a i ty l ofs id fList tr H1 H2))
    786781 
    787782  (a:expr) (v:val) (tr:trace) (ev:eval_expr ge e m a v tr) on ev : P a v tr ev ≝
     
    789784  [ eval_Econst_int i ty ⇒ eci i ty
    790785  | eval_Econst_float f ty ⇒ ecF f ty
    791   | eval_Elvalue a ty psp loc ofs v tr H1 H2 ⇒ elv a ty psp loc ofs v tr H1 H2 (eval_lvalue_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu (Expr a ty) psp loc ofs tr H1)
    792   | eval_Eaddrof a ty psp loc ofs tr H ⇒ ead a ty psp loc ofs tr H (eval_lvalue_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a psp loc ofs tr H)
     786  | eval_Elvalue a ty loc ofs v tr H1 H2 ⇒ elv a ty loc ofs v tr H1 H2 (eval_lvalue_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu (Expr a ty) loc ofs tr H1)
     787  | eval_Eaddrof a ty psp loc ofs tr H ⇒ ead a ty psp loc ofs tr H (eval_lvalue_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a loc ofs tr H)
    793788  | eval_Esizeof ty' ty ⇒ esz ty' ty
    794789  | eval_Eunop op a ty v1 v tr H1 H2 ⇒ eun op a ty v1 v tr H1 H2 (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a v1 tr H1)
     
    805800and eval_lvalue_ind2 (ge:genv) (e:env) (m:mem)
    806801  (P:∀a,v,tr. eval_expr ge e m a v tr → Prop)
    807   (Q:∀a,psp,loc,ofs,tr. eval_lvalue ge e m a psp loc ofs tr → Prop)
     802  (Q:∀a,loc,ofs,tr. eval_lvalue ge e m a loc ofs tr → Prop)
    808803  (eci:∀i,ty. P ??? (eval_Econst_int ge e m i ty))
    809804  (ecF:∀f,ty. P ??? (eval_Econst_float ge e m f ty))
    810   (elv:∀a,ty,psp,loc,ofs,v,tr,H1,H2. Q (Expr a ty) psp loc ofs tr H1 → P ??? (eval_Elvalue ge e m a ty psp loc ofs v tr H1 H2))
    811   (ead:∀a,ty,psp,loc,ofs,tr,H. Q a psp loc ofs tr H → P ??? (eval_Eaddrof ge e m a ty psp loc ofs tr H))
     805  (elv:∀a,ty,loc,ofs,v,tr,H1,H2. Q (Expr a ty) loc ofs tr H1 → P ??? (eval_Elvalue ge e m a ty loc ofs v tr H1 H2))
     806  (ead:∀a,ty,psp,loc,ofs,tr,H. Q a loc ofs tr H → P ??? (eval_Eaddrof ge e m a ty psp loc ofs tr H))
    812807  (esz:∀ty',ty. P ??? (eval_Esizeof ge e m ty' ty))
    813808  (eun:∀op,a,ty,v1,v,tr,H1,H2. P a v1 tr H1 → P ??? (eval_Eunop ge e m op a ty v1 v tr H1 H2))
     
    821816  (ecs:∀a,ty,ty',v1,v,tr,H1,H2. P a v1 tr H1 → P ??? (eval_Ecast ge e m a ty ty' v1 v tr H1 H2))
    822817  (eco:∀a,ty,v,l,tr,H. P a v tr H → P ??? (eval_Ecost ge e m a ty v l tr H))
    823   (lvl:∀id,l,ty,H. Q ????? (eval_Evar_local ge e m id l ty H))
    824   (lvg:∀id,sp,l,ty,H1,H2. Q ????? (eval_Evar_global ge e m id sp l ty H1 H2))
    825   (lde:∀a,ty,psp,l,ofs,tr,H. P a (Vptr psp l ofs) tr H → Q ????? (eval_Ederef ge e m a ty psp l ofs tr H))
    826   (lfs:∀a,i,ty,psp,l,ofs,id,fList,delta,tr,H1,H2,H3. Q a psp l ofs tr H1 → Q ????? (eval_Efield_struct ge e m a i ty psp l ofs id fList delta tr H1 H2 H3))
    827   (lfu:∀a,i,ty,psp,l,ofs,id,fList,tr,H1,H2. Q a psp l ofs tr H1 → Q ????? (eval_Efield_union ge e m a i ty psp l ofs id fList tr H1 H2))
    828   (a:expr) (psp:region) (loc:block) (ofs:int) (tr:trace) (ev:eval_lvalue ge e m a psp loc ofs tr) on ev : Q a psp loc ofs tr ev ≝
     818  (lvl:∀id,l,ty,H. Q ???? (eval_Evar_local ge e m id l ty H))
     819  (lvg:∀id,l,ty,H1,H2. Q ???? (eval_Evar_global ge e m id l ty H1 H2))
     820  (lde:∀a,ty,psp,l,ofs,tr,H. P a (Vptr psp l ofs) tr H → Q ???? (eval_Ederef ge e m a ty psp l ofs tr H))
     821  (lfs:∀a,i,ty,l,ofs,id,fList,delta,tr,H1,H2,H3. Q a l ofs tr H1 → Q ???? (eval_Efield_struct ge e m a i ty l ofs id fList delta tr H1 H2 H3))
     822  (lfu:∀a,i,ty,l,ofs,id,fList,tr,H1,H2. Q a l ofs tr H1 → Q ???? (eval_Efield_union ge e m a i ty l ofs id fList tr H1 H2))
     823  (a:expr) (loc:block) (ofs:int) (tr:trace) (ev:eval_lvalue ge e m a loc ofs tr) on ev : Q a loc ofs tr ev ≝
    829824  match ev with
    830825  [ eval_Evar_local id l ty H ⇒ lvl id l ty H
    831   | eval_Evar_global id sp l ty H1 H2 ⇒ lvg id sp l ty H1 H2
     826  | eval_Evar_global id l ty H1 H2 ⇒ lvg id l ty H1 H2
    832827  | eval_Ederef a ty psp l ofs tr H ⇒ lde a ty psp l ofs tr H (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a (Vptr psp l ofs) tr H)
    833   | eval_Efield_struct a i ty psp l ofs id fList delta tr H1 H2 H3 ⇒ lfs a i ty psp l ofs id fList delta tr H1 H2 H3 (eval_lvalue_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a psp l ofs tr H1)
    834   | eval_Efield_union a i ty psp l ofs id fList tr H1 H2 ⇒ lfu a i ty psp l ofs id fList tr H1 H2 (eval_lvalue_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a psp l ofs tr H1)
     828  | eval_Efield_struct a i ty l ofs id fList delta tr H1 H2 H3 ⇒ lfs a i ty l ofs id fList delta tr H1 H2 H3 (eval_lvalue_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a l ofs tr H1)
     829  | eval_Efield_union a i ty l ofs id fList tr H1 H2 ⇒ lfu a i ty l ofs id fList tr H1 H2 (eval_lvalue_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a l ofs tr H1)
    835830  ].
    836831
     
    881876  | Kswitch: cont -> cont
    882877       (**r catches [break] statements arising out of [switch] *)
    883   | Kcall: option (region × block × int × type) ->   (**r where to store result *)
     878  | Kcall: option (block × int × type) ->   (**r where to store result *)
    884879           function ->                      (**r calling function *)
    885880           env ->                           (**r local env of calling function *)
     
    995990inductive step (ge:genv) : state → trace → state → Prop ≝
    996991
    997   | step_assign:   ∀f,a1,a2,k,e,m,psp,loc,ofs,v2,m',tr1,tr2.
    998       eval_lvalue ge e m a1 psp loc ofs tr1 →
     992  | step_assign:   ∀f,a1,a2,k,e,m,loc,ofs,v2,m',tr1,tr2.
     993      eval_lvalue ge e m a1 loc ofs tr1 →
    999994      eval_expr ge e m a2 v2 tr2 →
    1000       store_value_of_type (typeof a1) m psp loc ofs v2 = Some ? m' →
     995      store_value_of_type (typeof a1) m loc ofs v2 = Some ? m' →
    1001996      step ge (State f (Sassign a1 a2) k e m)
    1002997           (tr1⧺tr2) (State f Sskip k e m')
     
    10101005           (tr1⧺tr2) (Callstate fd vargs (Kcall (None ?) f e k) m)
    10111006
    1012   | step_call_some:   ∀f,lhs,a,al,k,e,m,psp,loc,ofs,vf,vargs,fd,tr1,tr2,tr3.
    1013       eval_lvalue ge e m lhs psp loc ofs tr1 →
     1007  | step_call_some:   ∀f,lhs,a,al,k,e,m,loc,ofs,vf,vargs,fd,tr1,tr2,tr3.
     1008      eval_lvalue ge e m lhs loc ofs tr1 →
    10141009      eval_expr ge e m a vf tr2 →
    10151010      eval_exprlist ge e m al vargs tr3 →
     
    10171012      type_of_fundef fd = fun_typeof a →
    10181013      step ge (State f (Scall (Some ? lhs) a al) k e m)
    1019            (tr1⧺tr2⧺tr3) (Callstate fd vargs (Kcall (Some ? 〈〈〈psp, loc〉, ofs〉, typeof lhs〉) f e k) m)
     1014           (tr1⧺tr2⧺tr3) (Callstate fd vargs (Kcall (Some ? 〈〈loc, ofs〉, typeof lhs〉) f e k) m)
    10201015
    10211016  | step_seq:  ∀f,s1,s2,k,e,m.
     
    11561151           E0 (State f Sskip k e m)
    11571152
    1158   | step_returnstate_1: ∀v,f,e,k,m,m',psp,loc,ofs,ty.
    1159       store_value_of_type ty m psp loc ofs v = Some ? m' →
    1160       step ge (Returnstate v (Kcall (Some ? 〈〈〈psp,loc〉, ofs〉, ty〉) f e k) m)
     1153  | step_returnstate_1: ∀v,f,e,k,m,m',loc,ofs,ty.
     1154      store_value_of_type ty m loc ofs v = Some ? m' →
     1155      step ge (Returnstate v (Kcall (Some ? 〈〈loc, ofs〉, ty〉) f e k) m)
    11611156           E0 (State f Sskip k e m')
    11621157           
Note: See TracChangeset for help on using the changeset viewer.