Changeset 124 for C-semantics/Csem.ma


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

Initial work on Clight semantics with 8051 memory spaces.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/Csem.ma

    r13 r124  
    3939  | is_false_int: ∀sz,sg.
    4040      is_false (Vint zero) (Tint sz sg)
    41   | is_false_pointer: ∀t.
    42       is_false (Vint zero) (Tpointer t)
     41  | is_false_pointer: ∀s,t.
     42      is_false (Vint zero) (Tpointer s t)
    4343 | is_false_float: ∀sz.
    4444      is_false (Vfloat Fzero) (Tfloat sz).
     
    4848      n ≠ zero →
    4949      is_true (Vint n) (Tint sz sg)
    50   | is_true_pointer_int: ∀b,ofs,sz,sg.
    51       is_true (Vptr b ofs) (Tint sz sg)
    52   | is_true_int_pointer: ∀n,t.
     50  | is_true_pointer_int: ∀pcl,b,ofs,sz,sg.
     51      is_true (Vptr pcl b ofs) (Tint sz sg)
     52  | is_true_int_pointer: ∀n,s,t.
    5353      n ≠ zero →
    54       is_true (Vint n) (Tpointer t)
    55   | is_true_pointer_pointer: ∀b,ofs,t.
    56       is_true (Vptr b ofs) (Tpointer t)
     54      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)
    5757  | is_true_float: ∀f,sz.
    5858      f ≠ Fzero →
     
    101101      match v with
    102102      [ Vint n ⇒ Some ? (of_bool (eq n zero))
    103       | Vptr _ _ ⇒ Some ? Vfalse
     103      | Vptr _ _ _ ⇒ Some ? Vfalse
    104104      | _ ⇒ None ?
    105105      ]
    106   | Tpointer _
     106  | Tpointer _ _
    107107      match v with
    108108      [ Vint n ⇒ Some ? (of_bool (eq n zero))
    109       | Vptr _ _ ⇒ Some ? Vfalse
     109      | Vptr _ _ _ ⇒ Some ? Vfalse
    110110      | _ ⇒ None ?
    111111      ]
     
    134134  | add_case_pi ty ⇒                    (**r pointer plus integer *)
    135135      match v1 with
    136       [ Vptr b1 ofs1 ⇒ match v2 with
    137         [ Vint n2 ⇒ Some ? (Vptr b1 (add ofs1 (mul (repr (sizeof ty)) n2)))
     136      [ Vptr pcl1 b1 ofs1 ⇒ match v2 with
     137        [ Vint n2 ⇒ Some ? (Vptr pcl1 b1 (add ofs1 (mul (repr (sizeof ty)) n2)))
    138138        | _ ⇒ None ? ]
    139139      | _ ⇒ None ? ]
     
    141141      match v1 with
    142142      [ Vint n1 ⇒ match v2 with
    143         [ Vptr b2 ofs2 ⇒ Some ? (Vptr b2 (add ofs2 (mul (repr (sizeof ty)) n1)))
     143        [ Vptr pcl2 b2 ofs2 ⇒ Some ? (Vptr pcl2 b2 (add ofs2 (mul (repr (sizeof ty)) n1)))
    144144        | _ ⇒ None ? ]
    145145      | _ ⇒ None ? ]
     
    163163  | sub_case_pi ty ⇒             (**r pointer minus integer *)
    164164      match v1 with
    165       [ Vptr b1 ofs1 ⇒ match v2 with
    166         [ Vint n2 ⇒ Some ? (Vptr b1 (sub ofs1 (mul (repr (sizeof ty)) n2)))
     165      [ Vptr pcl1 b1 ofs1 ⇒ match v2 with
     166        [ Vint n2 ⇒ Some ? (Vptr pcl1 b1 (sub ofs1 (mul (repr (sizeof ty)) n2)))
    167167        | _ ⇒ None ? ]
    168168      | _ ⇒ None ? ]
    169169  | sub_case_pp ty ⇒             (**r pointer minus pointer *)
    170170      match v1 with
    171       [ Vptr b1 ofs1 ⇒ match v2 with
    172         [ Vptr b2 ofs2 ⇒
     171      [ Vptr pcl1 b1 ofs1 ⇒ match v2 with
     172        [ Vptr pcl2 b2 ofs2 ⇒
    173173          if eqZb b1 b2 then
    174174            if eq (repr (sizeof ty)) zero then None ?
     
    179179  | sub_default ⇒ None ?
    180180  ].
    181  
     181
    182182nlet rec sem_mul (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝
    183183 match classify_mul t1 t2 with
     
    313313      [ Vint n1 ⇒ match v2 with
    314314         [ Vint n2 ⇒ Some ? (of_bool (cmp c n1 n2))
    315          | Vptr b ofs ⇒ if eq n1 zero then sem_cmp_mismatch c else None ?
     315         | Vptr pcl b ofs ⇒ if eq n1 zero then sem_cmp_mismatch c else None ?
    316316         | _ ⇒ None ?
    317317         ]
    318       | Vptr b1 ofs1 ⇒
     318      | Vptr pcl1 b1 ofs1 ⇒
    319319        match v2 with
    320         [ Vptr b2 ofs2 ⇒
    321           if valid_pointer m b1 (signed ofs1)
    322           ∧ valid_pointer m b2 (signed ofs2) then
     320        [ Vptr pcl2 b2 ofs2 ⇒
     321          if valid_pointer m pcl1 b1 (signed ofs1)
     322          ∧ valid_pointer m pcl2 b2 (signed ofs2) then
    323323            if eqZb b1 b2
    324324            then Some ? (of_bool (cmp c ofs1 ofs2))
     
    400400  ].
    401401
    402 ninductive neutral_for_cast: type → Prop ≝
    403   | nfc_int: ∀sg.
    404       neutral_for_cast (Tint I32 sg)
    405   | nfc_ptr: ∀ty.
    406       neutral_for_cast (Tpointer ty)
    407   | nfc_array: ∀ty,sz.
    408       neutral_for_cast (Tarray ty sz)
    409   | nfc_fun: ∀targs,tres.
    410       neutral_for_cast (Tfunction targs tres).
    411 
    412 ninductive cast : val → type → type → val → Prop ≝
    413   | cast_ii:   ∀i,sz2,sz1,si1,si2.            (**r int to int  *)
    414       cast (Vint i) (Tint sz1 si1) (Tint sz2 si2)
     402(* XXX should go somewhere else? *)
     403ndefinition 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].
     411ndefinition 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
     420ndefinition 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
     429ninductive type_pointable : type → Prop ≝
     430| type_ptr_int : type_pointable (Tint I32 Unsigned)
     431| type_ptr_pointer : ∀s,t. type_pointable (Tpointer s t)
     432| type_ptr_array : ∀s,t,n. type_pointable (Tarray s t n)
     433| type_ptr_function : ∀tys,ty. type_pointable (Tfunction tys ty).
     434
     435ninductive type_space : type → mem_space → Prop ≝
     436| type_spc_int : type_space (Tint I32 Unsigned) Generic
     437| type_spc_pointer : ∀s,t. type_space (Tpointer s t) s
     438| type_spc_array : ∀s,t,n. type_space (Tarray s t n) s
     439| type_spc_code : ∀tys,ty. type_space (Tfunction tys ty) Code.
     440
     441ninductive cast : mem → val → type → type → val → Prop ≝
     442  | cast_ii:   ∀m,i,sz2,sz1,si1,si2.            (**r int to int  *)
     443      cast m (Vint i) (Tint sz1 si1) (Tint sz2 si2)
    415444           (Vint (cast_int_int sz2 si2 i))
    416   | cast_fi:   ∀f,sz1,sz2,si2.                (**r float to int *)
    417       cast (Vfloat f) (Tfloat sz1) (Tint sz2 si2)
     445  | cast_fi:   ∀m,f,sz1,sz2,si2.                (**r float to int *)
     446      cast m (Vfloat f) (Tfloat sz1) (Tint sz2 si2)
    418447           (Vint (cast_int_int sz2 si2 (cast_float_int si2 f)))
    419   | cast_if:   ∀i,sz1,sz2,si1.                (**r int to float  *)
    420       cast (Vint i) (Tint sz1 si1) (Tfloat sz2)
     448  | cast_if:   ∀m,i,sz1,sz2,si1.                (**r int to float  *)
     449      cast m (Vint i) (Tint sz1 si1) (Tfloat sz2)
    421450          (Vfloat (cast_float_float sz2 (cast_int_float si1 i)))
    422   | cast_ff:   ∀f,sz1,sz2.                    (**r float to float *)
    423       cast (Vfloat f) (Tfloat sz1) (Tfloat sz2)
     451  | cast_ff:   ∀m,f,sz1,sz2.                    (**r float to float *)
     452      cast m (Vfloat f) (Tfloat sz1) (Tfloat sz2)
    424453           (Vfloat (cast_float_float sz2 f))
    425   | cast_nn_p: ∀b,ofs,t1,t2. (**r no change in data representation *)
     454  | cast_pp: ∀m,pcl,psp,ty,ty',b,ofs.
     455      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)
     459  | cast_pp_z: ∀m,ty,ty'.
     460      type_pointable ty → (* Don't care which space it is for the source type *)
     461      type_pointable ty' →
     462      cast m (Vint zero) ty ty' (Vint zero).
     463(* XXX: other integers?
     464  | cast_nn_i: ∀m,n,t1,t2.     (**r no change in data representation *)
    426465      neutral_for_cast t1 → neutral_for_cast t2 →
    427       cast (Vptr b ofs) t1 t2 (Vptr b ofs)
    428   | cast_nn_i: ∀n,t1,t2.     (**r no change in data representation *)
    429       neutral_for_cast t1 → neutral_for_cast t2 →
    430       cast (Vint n) t1 t2 (Vint n).
    431 
     466      cast m (Vint n) t1 t2 (Vint n).
     467*)
    432468(* * * Operational semantics *)
    433469
     
    442478  block. *)
    443479
    444 ndefinition env ≝ (tree_t ? PTree) block. (* map variable -> location *)
     480ndefinition env ≝ (tree_t ? PTree) (block_class × block). (* map variable -> location *)
    445481
    446482ndefinition empty_env: env ≝ (empty …).
     
    452488  reference, the pointer [Vptr b ofs] is returned. *)
    453489
    454 nlet rec load_value_of_type (ty: type) (m: mem) (b: block) (ofs: int) : option val ≝
     490nlet rec load_value_of_type (ty: type) (m: mem) (pcl:ptr_class) (b: block) (ofs: int) : option val ≝
    455491  match access_mode ty with
    456   [ By_value chunk ⇒ loadv chunk m (Vptr b ofs)
    457   | By_reference ⇒ Some ? (Vptr b ofs)
     492  [ By_value chunk ⇒ loadv chunk m (Vptr pcl b ofs)
     493  | By_reference ⇒ Some ? (Vptr pcl b ofs)
    458494  | By_nothing ⇒ None ?
    459495  ].
     
    464500  This is allowed only if [ty] indicates an access by value. *)
    465501
    466 nlet rec store_value_of_type (ty_dest: type) (m: mem) (loc: block) (ofs: int) (v: val) : option mem ≝
     502nlet rec store_value_of_type (ty_dest: type) (m: mem) (pcl:ptr_class) (loc: block) (ofs: int) (v: val) : option mem ≝
    467503  match access_mode ty_dest with
    468   [ By_value chunk ⇒ storev chunk m (Vptr loc ofs) v
     504  [ By_value chunk ⇒ storev chunk m (Vptr pcl loc ofs) v
    469505  | By_reference ⇒ None ?
    470506  | By_nothing ⇒ None ?
     
    486522  | alloc_variables_cons:
    487523      ∀e,m,id,ty,vars,m1,b1,m2,e2.
    488       alloc m 0 (sizeof ty) = 〈m1, b1〉 →
    489       alloc_variables (set … id b1 e) m1 vars e2 m2 →
     524      alloc m 0 (sizeof ty) UnspecifiedB = 〈m1, b1〉 → (* XXX *)
     525      alloc_variables (set … id 〈UnspecifiedB, b1〉 e) m1 vars e2 m2 →
    490526      alloc_variables e m (〈id, ty〉 :: vars) e2 m2.
    491527
     
    502538      bind_parameters e m (nil ?) (nil ?) m
    503539  | bind_parameters_cons:
    504       ∀e,m,id,ty,params,v1,vl,b,m1,m2.
    505       get ??? id e = Some ? b
    506       store_value_of_type ty m b zero v1 = Some ? m1 →
     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 →
    507543      bind_parameters e m1 params vl m2 →
    508544      bind_parameters e m (〈id, ty〉 :: params) (v1 :: vl) m2.
     
    511547
    512548ndefinition blocks_of_env : env → list block ≝ λe.
    513   map ?? (snd ident block) (elements ??? e).
     549  map ?? (λx. snd ?? (snd ?? x)) (elements ??? e).
    514550
    515551(* * Selection of the appropriate case of a [switch], given the value [n]
     
    552588  | eval_Econst_float:   ∀f,ty.
    553589      eval_expr ge e m (Expr (Econst_float f) ty) (Vfloat f)
    554   | eval_Elvalue: ∀a,ty,loc,ofs,v.
    555       eval_lvalue ge e m (Expr a ty) loc ofs ->
    556       load_value_of_type ty m loc ofs = Some ? v ->
     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 ->
    557593      eval_expr ge e m (Expr a ty) v
    558   | eval_Eaddrof: ∀a,ty,loc,ofs.
    559       eval_lvalue ge e m a loc ofs ->
    560       eval_expr ge e m (Expr (Eaddrof a) ty) (Vptr loc ofs)
     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)
    561597  | eval_Esizeof: ∀ty',ty.
    562598      eval_expr ge e m (Expr (Esizeof ty') ty) (Vint (repr (sizeof ty')))
     
    602638  | eval_Ecast:   ∀a,ty,ty',v1,v.
    603639      eval_expr ge e m a v1 ->
    604       cast v1 (typeof a) ty v ->
     640      cast m v1 (typeof a) ty v ->
    605641      eval_expr ge e m (Expr (Ecast ty a) ty') v
    606642
     
    609645  that contains the value of the expression [a]. *)
    610646
    611 with eval_lvalue (*(ge:genv) (e:env) (m:mem)*) : expr -> block -> int -> Prop ≝
    612   | eval_Evar_local:   ∀id,l,ty.
    613       (* XXX notation? e!id*) get ??? id e = Some ? l ->
    614       eval_lvalue ge e m (Expr (Evar id) ty) l zero
     647with 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
    615651  | eval_Evar_global: ∀id,l,ty.
    616652      (* XXX e!id *) get ??? id e = None ? ->
    617653      find_symbol ?? ge id = Some ? l ->
    618       eval_lvalue ge e m (Expr (Evar id) ty) l zero
    619   | eval_Ederef: ∀a,ty,l,ofs.
    620       eval_expr ge e m a (Vptr l ofs) ->
    621       eval_lvalue ge e m (Expr (Ederef a) ty) l ofs
    622  | eval_Efield_struct:   ∀a,i,ty,l,ofs,id,fList,delta.
    623       eval_lvalue ge e m a l ofs ->
     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 ->
    624660      typeof a = Tstruct id fList ->
    625661      field_offset i fList = OK ? delta ->
    626       eval_lvalue ge e m (Expr (Efield a i) ty) l (add ofs (repr delta))
    627  | eval_Efield_union:   ∀a,i,ty,l,ofs,id,fList.
    628       eval_lvalue ge e m a l ofs ->
     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 ->
    629665      typeof a = Tunion id fList ->
    630       eval_lvalue ge e m (Expr (Efield a i) ty) l ofs.
     666      eval_lvalue ge e m (Expr (Efield a i) ty) pcl l ofs.
    631667
    632668(*
     
    666702  | Kswitch: cont -> cont
    667703       (**r catches [break] statements arising out of [switch] *)
    668   | Kcall: option (block × int × type) ->   (**r where to store result *)
     704  | Kcall: option (ptr_class × block × int × type) ->   (**r where to store result *)
    669705           function ->                      (**r calling function *)
    670706           env ->                           (**r local env of calling function *)
     
    764800ninductive step (ge:genv) : state -> trace -> state -> Prop :=
    765801
    766   | step_assign:   ∀f,a1,a2,k,e,m,loc,ofs,v2,m'.
    767       eval_lvalue ge e m a1 loc ofs ->
     802  | step_assign:   ∀f,a1,a2,k,e,m,pcl,loc,ofs,v2,m'.
     803      eval_lvalue ge e m a1 pcl loc ofs ->
    768804      eval_expr ge e m a2 v2 ->
    769       store_value_of_type (typeof a1) m loc ofs v2 = Some ? m' ->
     805      store_value_of_type (typeof a1) m pcl loc ofs v2 = Some ? m' ->
    770806      step ge (State f (Sassign a1 a2) k e m)
    771807           E0 (State f Sskip k e m')
     
    779815           E0 (Callstate fd vargs (Kcall (None ?) f e k) m)
    780816
    781   | step_call_some:   ∀f,lhs,a,al,k,e,m,loc,ofs,vf,vargs,fd.
    782       eval_lvalue ge e m lhs loc ofs ->
     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 ->
    783819      eval_expr ge e m a vf ->
    784820      eval_exprlist ge e m al vargs ->
     
    786822      type_of_fundef fd = typeof a ->
    787823      step ge (State f (Scall (Some ? lhs) a al) k e m)
    788            E0 (Callstate fd vargs (Kcall (Some ? 〈〈loc, ofs〉, typeof lhs〉) f e k) m)
     824           E0 (Callstate fd vargs (Kcall (Some ? 〈〈〈pcl, loc〉, ofs〉, typeof lhs〉) f e k) m)
    789825
    790826  | step_seq:  ∀f,s1,s2,k,e,m.
     
    925961           E0 (State f Sskip k e m)
    926962
    927   | step_returnstate_1: ∀v,f,e,k,m,m',loc,ofs,ty.
    928       store_value_of_type ty m loc ofs v = Some ? m' ->
    929       step ge (Returnstate v (Kcall (Some ? 〈〈loc, ofs〉, ty〉) f e k) m)
     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)
    930966           E0 (State f Sskip k e m').
    931967(*
Note: See TracChangeset for help on using the changeset viewer.