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

First pass at moving regions to block type.

File:
1 edited

Legend:

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

    r487 r496  
    169169      [ Vptr pcl1 b1 ofs1 ⇒ match v2 with
    170170        [ Vptr pcl2 b2 ofs2 ⇒
    171           if eqZb b1 b2 then
     171          if eq_block b1 b2 then
    172172            if eq (repr (sizeof ty)) zero then None ?
    173173            else Some ? (Vint (divu (sub ofs1 ofs2) (repr (sizeof ty))))
     
    326326          if valid_pointer m r1 b1 (signed ofs1)
    327327          ∧ valid_pointer m r2 b2 (signed ofs2) then
    328             if eqZb b1 b2
     328            if eq_block b1 b2
    329329            then Some ? (of_bool (cmp c ofs1 ofs2))
    330330            else sem_cmp_mismatch c
     
    432432      type_region ty r →
    433433      type_region ty' r' →
    434       pointer_compat (block_space m b) r' →
     434      pointer_compat (block_region m b) r' →
    435435      cast m (Vptr r b ofs) ty ty' (Vptr r' b ofs)
    436436  | cast_ip_z: ∀m,sz,sg,ty',r.
     
    567567  | eval_Econst_float:   ∀f,ty.
    568568      eval_expr ge e m (Expr (Econst_float f) ty) (Vfloat f) E0
    569   | eval_Elvalue: ∀a,ty,psp,loc,ofs,v,tr.
    570       eval_lvalue ge e m (Expr a ty) psp loc ofs tr →
    571       load_value_of_type ty m psp loc ofs = Some ? v →
     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 →
    572572      eval_expr ge e m (Expr a ty) v tr
    573   | eval_Eaddrof: ∀a,ty,psp,loc,ofs,tr.
    574       eval_lvalue ge e m a psp loc ofs tr →
    575       eval_expr ge e m (Expr (Eaddrof a) ty) (Vptr psp loc ofs) tr
     573  | 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
    576576  | eval_Esizeof: ∀ty',ty.
    577577      eval_expr ge e m (Expr (Esizeof ty') ty) (Vint (repr (sizeof ty'))) E0
     
    623623      eval_expr ge e m (Expr (Ecost l a) ty) v (tr⧺Echarge l)
    624624
    625 (* * [eval_lvalue ge e m a b ofs] defines the evaluation of expression [a]
     625(* * [eval_lvalue ge e m a r b ofs] defines the evaluation of expression [a]
    626626  in l-value position.  The result is the memory location [b, ofs]
    627   that contains the value of the expression [a]. *)
     627  that contains the value of the expression [a].  The memory location should
     628  be representable in a pointer of region r. *)
    628629
    629630with eval_lvalue (*(ge:genv) (e:env) (m:mem)*) : expr → region → block → int → trace → Prop ≝
     
    631632      (* XXX notation? e!id*) get ??? id e = Some ? l →
    632633      eval_lvalue ge e m (Expr (Evar id) ty) Any l zero E0
    633   | eval_Evar_global: ∀id,sp,l,ty.
     634  | eval_Evar_global: ∀id,r,l,ty.
    634635      (* XXX e!id *) get ??? id e = None ? →
    635       find_symbol ?? ge id = Some ? 〈sp,l〉 →
    636       eval_lvalue ge e m (Expr (Evar id) ty) sp l zero E0
    637   | eval_Ederef: ∀a,ty,psp,l,ofs,tr.
    638       eval_expr ge e m a (Vptr psp l ofs) tr →
    639       eval_lvalue ge e m (Expr (Ederef a) ty) psp l ofs tr
    640  | eval_Efield_struct:   ∀a,i,ty,psp,l,ofs,id,fList,delta,tr.
    641       eval_lvalue ge e m a psp l ofs tr →
     636      find_symbol ?? ge id = Some ? 〈r,l〉 →
     637      eval_lvalue ge e m (Expr (Evar id) ty) r 〈r,l〉 zero E0
     638  | eval_Ederef: ∀a,ty,r,l,ofs,tr.
     639      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 →
    642643      typeof a = Tstruct id fList →
    643644      field_offset i fList = OK ? delta →
    644       eval_lvalue ge e m (Expr (Efield a i) ty) psp l (add ofs (repr delta)) tr
    645  | eval_Efield_union:   ∀a,i,ty,psp,l,ofs,id,fList,tr.
    646       eval_lvalue ge e m a psp l ofs tr →
     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 →
    647648      typeof a = Tunion id fList →
    648       eval_lvalue ge e m (Expr (Efield a i) ty) psp l ofs tr.
     649      eval_lvalue ge e m (Expr (Efield a i) ty) r l ofs tr.
    649650
    650651let rec eval_expr_ind (ge:genv) (e:env) (m:mem)
     
    14791480      globalenv Genv ?? p = OK ? ge →
    14801481      init_mem Genv ?? p = OK ? m0 →
    1481       find_symbol ?? ge (prog_main ?? p) = Some ? 〈Code,b〉
     1482      find_symbol ?? ge (prog_main ?? p) = Some ? b
    14821483      find_funct_ptr ?? ge b = Some ? f →
    14831484      initial_state p (Callstate f (nil ?) Kstop m0).
Note: See TracChangeset for help on using the changeset viewer.