Changeset 125 for C-semantics/Csem.ma


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

Unify memory space / pointer types.
Implement global variable initialisation and lookup.
Global variables get memory spaces, local variables could be anywhere (for now).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/Csem.ma

    r124 r125  
    4848      n ≠ zero →
    4949      is_true (Vint n) (Tint sz sg)
    50   | is_true_pointer_int: ∀pcl,b,ofs,sz,sg.
    51       is_true (Vptr pcl b ofs) (Tint sz sg)
     50  | is_true_pointer_int: ∀psp,b,ofs,sz,sg.
     51      is_true (Vptr psp b ofs) (Tint sz sg)
    5252  | is_true_int_pointer: ∀n,s,t.
    5353      n ≠ zero →
    5454      is_true (Vint n) (Tpointer s t)
    55   | is_true_pointer_pointer: ∀pcl,b,ofs,s,t.
    56       is_true (Vptr pcl b ofs) (Tpointer s t)
     55  | is_true_pointer_pointer: ∀psp,b,ofs,s,t.
     56      is_true (Vptr psp b ofs) (Tpointer s t)
    5757  | is_true_float: ∀f,sz.
    5858      f ≠ Fzero →
     
    313313      [ Vint n1 ⇒ match v2 with
    314314         [ Vint n2 ⇒ Some ? (of_bool (cmp c n1 n2))
    315          | Vptr pcl b ofs ⇒ if eq n1 zero then sem_cmp_mismatch c else None ?
     315         | Vptr psp b ofs ⇒ if eq n1 zero then sem_cmp_mismatch c else None ?
    316316         | _ ⇒ None ?
    317317         ]
     
    400400  ].
    401401
    402 (* XXX should go somewhere else? *)
    403 ndefinition ptr_cls_spc : ptr_class → mem_space ≝
    404 λp.match p with
    405 [ Universal ⇒ Generic
    406 | Data ⇒ Data
    407 | IData ⇒ IData
    408 | XData ⇒ XData
    409 | Code ⇒ Code
    410 ].
    411 ndefinition ptr_spc_cls : mem_space → ptr_class ≝
    412 λp.match p with
    413 [ Generic ⇒ Universal
    414 | Data ⇒ Data
    415 | IData ⇒ IData
    416 | XData ⇒ XData
    417 | Code ⇒ Code
    418 ].
    419 
    420 ndefinition blk_ptr_cls : block_class → ptr_class ≝
    421 λb.match b with
    422 [ UnspecifiedB ⇒ Universal
    423 | DataB ⇒ Data
    424 | IDataB ⇒ IData
    425 | XDataB ⇒ XData
    426 | CodeB ⇒ Code
    427 ].
    428 
    429402ninductive type_pointable : type → Prop ≝
    430403| type_ptr_int : type_pointable (Tint I32 Unsigned)
     
    433406| type_ptr_function : ∀tys,ty. type_pointable (Tfunction tys ty).
    434407
    435 ninductive type_space : type → mem_space → Prop ≝
    436 | type_spc_int : type_space (Tint I32 Unsigned) Generic
     408ninductive type_space : type → memory_space → Prop ≝
     409| type_spc_int : type_space (Tint I32 Unsigned) Any
    437410| type_spc_pointer : ∀s,t. type_space (Tpointer s t) s
    438411| type_spc_array : ∀s,t,n. type_space (Tarray s t n) s
     
    452425      cast m (Vfloat f) (Tfloat sz1) (Tfloat sz2)
    453426           (Vfloat (cast_float_float sz2 f))
    454   | cast_pp: ∀m,pcl,psp,ty,ty',b,ofs.
     427  | cast_pp: ∀m,psp,psp',ty,ty',b,ofs.
    455428      type_pointable ty →
    456       type_space ty' psp
    457       class_compat (blockclass m b) (ptr_spc_cls psp)
    458       cast m (Vptr pcl b ofs) ty ty' (Vptr (ptr_spc_cls psp) b ofs)
     429      type_space ty' psp'
     430      pointer_compat (block_space m b) psp'
     431      cast m (Vptr psp b ofs) ty ty' (Vptr psp' b ofs)
    459432  | cast_pp_z: ∀m,ty,ty'.
    460433      type_pointable ty → (* Don't care which space it is for the source type *)
     
    478451  block. *)
    479452
    480 ndefinition env ≝ (tree_t ? PTree) (block_class × block). (* map variable -> location *)
     453ndefinition env ≝ (tree_t ? PTree) block. (* map variable -> location *)
    481454
    482455ndefinition empty_env: env ≝ (empty …).
     
    488461  reference, the pointer [Vptr b ofs] is returned. *)
    489462
    490 nlet rec load_value_of_type (ty: type) (m: mem) (pcl:ptr_class) (b: block) (ofs: int) : option val ≝
     463nlet rec load_value_of_type (ty: type) (m: mem) (psp:memory_space) (b: block) (ofs: int) : option val ≝
    491464  match access_mode ty with
    492   [ By_value chunk ⇒ loadv chunk m (Vptr pcl b ofs)
    493   | By_reference ⇒ Some ? (Vptr pcl b ofs)
     465  [ By_value chunk ⇒ loadv chunk m (Vptr psp b ofs)
     466  | By_reference ⇒ Some ? (Vptr psp b ofs)
    494467  | By_nothing ⇒ None ?
    495468  ].
     
    500473  This is allowed only if [ty] indicates an access by value. *)
    501474
    502 nlet rec store_value_of_type (ty_dest: type) (m: mem) (pcl:ptr_class) (loc: block) (ofs: int) (v: val) : option mem ≝
     475nlet rec store_value_of_type (ty_dest: type) (m: mem) (psp:memory_space) (loc: block) (ofs: int) (v: val) : option mem ≝
    503476  match access_mode ty_dest with
    504   [ By_value chunk ⇒ storev chunk m (Vptr pcl loc ofs) v
     477  [ By_value chunk ⇒ storev chunk m (Vptr psp loc ofs) v
    505478  | By_reference ⇒ None ?
    506479  | By_nothing ⇒ None ?
     
    522495  | alloc_variables_cons:
    523496      ∀e,m,id,ty,vars,m1,b1,m2,e2.
    524       alloc m 0 (sizeof ty) UnspecifiedB = 〈m1, b1〉 → (* XXX *)
    525       alloc_variables (set … id 〈UnspecifiedB, b1〉 e) m1 vars e2 m2 →
     497      alloc m 0 (sizeof ty) Any = 〈m1, b1〉 →
     498      alloc_variables (set … id b1 e) m1 vars e2 m2 →
    526499      alloc_variables e m (〈id, ty〉 :: vars) e2 m2.
    527500
     
    538511      bind_parameters e m (nil ?) (nil ?) m
    539512  | bind_parameters_cons:
    540       ∀e,m,id,ty,params,v1,vl,bcls,b,m1,m2.
    541       get ??? id e = Some ? 〈bcls,b〉
    542       store_value_of_type ty m (blk_ptr_cls bcls) b zero v1 = Some ? m1 →
     513      ∀e,m,id,ty,params,v1,vl,b,m1,m2.
     514      get ??? id e = Some ? b
     515      store_value_of_type ty m Any b zero v1 = Some ? m1 →
    543516      bind_parameters e m1 params vl m2 →
    544517      bind_parameters e m (〈id, ty〉 :: params) (v1 :: vl) m2.
    545518
     519(* XXX: this doesn't look right - we're assigning arbitrary memory spaces to
     520   parameters? *)
     521
    546522(* * Return the list of blocks in the codomain of [e]. *)
    547523
    548524ndefinition blocks_of_env : env → list block ≝ λe.
    549   map ?? (λx. snd ?? (snd ?? x)) (elements ??? e).
     525  map ?? (λx. snd ?? x) (elements ??? e).
    550526
    551527(* * Selection of the appropriate case of a [switch], given the value [n]
     
    588564  | eval_Econst_float:   ∀f,ty.
    589565      eval_expr ge e m (Expr (Econst_float f) ty) (Vfloat f)
    590   | eval_Elvalue: ∀a,ty,pcl,loc,ofs,v.
    591       eval_lvalue ge e m (Expr a ty) pcl loc ofs ->
    592       load_value_of_type ty m pcl loc ofs = Some ? v ->
     566  | eval_Elvalue: ∀a,ty,psp,loc,ofs,v.
     567      eval_lvalue ge e m (Expr a ty) psp loc ofs ->
     568      load_value_of_type ty m psp loc ofs = Some ? v ->
    593569      eval_expr ge e m (Expr a ty) v
    594   | eval_Eaddrof: ∀a,ty,pcl,loc,ofs.
    595       eval_lvalue ge e m a pcl loc ofs ->
    596       eval_expr ge e m (Expr (Eaddrof a) ty) (Vptr pcl loc ofs)
     570  | eval_Eaddrof: ∀a,ty,psp,loc,ofs.
     571      eval_lvalue ge e m a psp loc ofs ->
     572      eval_expr ge e m (Expr (Eaddrof a) ty) (Vptr psp loc ofs)
    597573  | eval_Esizeof: ∀ty',ty.
    598574      eval_expr ge e m (Expr (Esizeof ty') ty) (Vint (repr (sizeof ty')))
     
    645621  that contains the value of the expression [a]. *)
    646622
    647 with eval_lvalue (*(ge:genv) (e:env) (m:mem)*) : expr → ptr_class → block -> int -> Prop ≝
    648   | eval_Evar_local:   ∀id,bcl,l,ty.
    649       (* XXX notation? e!id*) get ??? id e = Some ? 〈bcl,l〉 ->
    650       eval_lvalue ge e m (Expr (Evar id) ty) (blk_ptr_cls bcl) l zero
    651   | eval_Evar_global: ∀id,l,ty.
     623with eval_lvalue (*(ge:genv) (e:env) (m:mem)*) : expr → memory_space → block -> int -> Prop ≝
     624  | eval_Evar_local:   ∀id,l,ty.
     625      (* XXX notation? e!id*) get ??? id e = Some ? l →
     626      eval_lvalue ge e m (Expr (Evar id) ty) Any l zero
     627  | eval_Evar_global: ∀id,sp,l,ty.
    652628      (* XXX e!id *) get ??? id e = None ? ->
    653       find_symbol ?? ge id = Some ? l ->
    654       eval_lvalue ge e m (Expr (Evar id) ty) Universal l zero (* XXX *)
    655   | eval_Ederef: ∀a,ty,pcl,l,ofs.
    656       eval_expr ge e m a (Vptr pcl l ofs) ->
    657       eval_lvalue ge e m (Expr (Ederef a) ty) pcl l ofs
    658  | eval_Efield_struct:   ∀a,i,ty,pcl,l,ofs,id,fList,delta.
    659       eval_lvalue ge e m a pcl l ofs ->
     629      find_symbol ?? ge id = Some ? 〈sp,l〉 ->
     630      eval_lvalue ge e m (Expr (Evar id) ty) sp l zero
     631  | eval_Ederef: ∀a,ty,psp,l,ofs.
     632      eval_expr ge e m a (Vptr psp l ofs) ->
     633      eval_lvalue ge e m (Expr (Ederef a) ty) psp l ofs
     634 | eval_Efield_struct:   ∀a,i,ty,psp,l,ofs,id,fList,delta.
     635      eval_lvalue ge e m a psp l ofs ->
    660636      typeof a = Tstruct id fList ->
    661637      field_offset i fList = OK ? delta ->
    662       eval_lvalue ge e m (Expr (Efield a i) ty) pcl l (add ofs (repr delta))
    663  | eval_Efield_union:   ∀a,i,ty,pcl,l,ofs,id,fList.
    664       eval_lvalue ge e m a pcl l ofs ->
     638      eval_lvalue ge e m (Expr (Efield a i) ty) psp l (add ofs (repr delta))
     639 | eval_Efield_union:   ∀a,i,ty,psp,l,ofs,id,fList.
     640      eval_lvalue ge e m a psp l ofs ->
    665641      typeof a = Tunion id fList ->
    666       eval_lvalue ge e m (Expr (Efield a i) ty) pcl l ofs.
     642      eval_lvalue ge e m (Expr (Efield a i) ty) psp l ofs.
    667643
    668644(*
     
    702678  | Kswitch: cont -> cont
    703679       (**r catches [break] statements arising out of [switch] *)
    704   | Kcall: option (ptr_class × block × int × type) ->   (**r where to store result *)
     680  | Kcall: option (memory_space × block × int × type) ->   (**r where to store result *)
    705681           function ->                      (**r calling function *)
    706682           env ->                           (**r local env of calling function *)
     
    800776ninductive step (ge:genv) : state -> trace -> state -> Prop :=
    801777
    802   | step_assign:   ∀f,a1,a2,k,e,m,pcl,loc,ofs,v2,m'.
    803       eval_lvalue ge e m a1 pcl loc ofs ->
     778  | step_assign:   ∀f,a1,a2,k,e,m,psp,loc,ofs,v2,m'.
     779      eval_lvalue ge e m a1 psp loc ofs ->
    804780      eval_expr ge e m a2 v2 ->
    805       store_value_of_type (typeof a1) m pcl loc ofs v2 = Some ? m' ->
     781      store_value_of_type (typeof a1) m psp loc ofs v2 = Some ? m' ->
    806782      step ge (State f (Sassign a1 a2) k e m)
    807783           E0 (State f Sskip k e m')
     
    815791           E0 (Callstate fd vargs (Kcall (None ?) f e k) m)
    816792
    817   | step_call_some:   ∀f,lhs,a,al,k,e,m,pcl,loc,ofs,vf,vargs,fd.
    818       eval_lvalue ge e m lhs pcl loc ofs ->
     793  | step_call_some:   ∀f,lhs,a,al,k,e,m,psp,loc,ofs,vf,vargs,fd.
     794      eval_lvalue ge e m lhs psp loc ofs ->
    819795      eval_expr ge e m a vf ->
    820796      eval_exprlist ge e m al vargs ->
     
    822798      type_of_fundef fd = typeof a ->
    823799      step ge (State f (Scall (Some ? lhs) a al) k e m)
    824            E0 (Callstate fd vargs (Kcall (Some ? 〈〈〈pcl, loc〉, ofs〉, typeof lhs〉) f e k) m)
     800           E0 (Callstate fd vargs (Kcall (Some ? 〈〈〈psp, loc〉, ofs〉, typeof lhs〉) f e k) m)
    825801
    826802  | step_seq:  ∀f,s1,s2,k,e,m.
     
    961937           E0 (State f Sskip k e m)
    962938
    963   | step_returnstate_1: ∀v,f,e,k,m,m',pcl,loc,ofs,ty.
    964       store_value_of_type ty m pcl loc ofs v = Some ? m' ->
    965       step ge (Returnstate v (Kcall (Some ? 〈〈〈pcl,loc〉, ofs〉, ty〉) f e k) m)
     939  | step_returnstate_1: ∀v,f,e,k,m,m',psp,loc,ofs,ty.
     940      store_value_of_type ty m psp loc ofs v = Some ? m' ->
     941      step ge (Returnstate v (Kcall (Some ? 〈〈〈psp,loc〉, ofs〉, ty〉) f e k) m)
    966942           E0 (State f Sskip k e m').
    967943(*
     
    12811257      let ge := globalenv Genv ?? p in
    12821258      let m0 := init_mem Genv ?? p in
    1283       find_symbol ?? ge (prog_main ?? p) = Some ? b ->
     1259      find_symbol ?? ge (prog_main ?? p) = Some ? 〈Code,b〉 ->
    12841260      find_funct_ptr ?? ge b = Some ? f ->
    12851261      initial_state p (Callstate f (nil ?) Kstop m0).
Note: See TracChangeset for help on using the changeset viewer.