Changeset 2176 for src/Clight/Csem.ma


Ignore:
Timestamp:
Jul 12, 2012, 1:28:28 PM (9 years ago)
Author:
campbell
Message:

Remove memory spaces other than XData and Code; simplify pointers as a
result.

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/Clight/Csem.ma

    r2032 r2176  
    3939  | is_false_int: ∀sz,sg.
    4040      is_false (Vint sz (zero ?)) (Tint sz sg)
    41   | is_false_pointer: ∀r,r',t.
    42       is_false (Vnull r) (Tpointer r' t)
     41  | is_false_pointer: ∀t.
     42      is_false Vnull (Tpointer t)
    4343 | is_false_float: ∀sz.
    4444      is_false (Vfloat Fzero) (Tfloat sz).
    … …  
    4848      n ≠ (zero ?) →
    4949      is_true (Vint sz n) (Tint sz sg)
    50   | is_true_pointer_pointer: ∀ptr,s,t.
    51       is_true (Vptr ptr) (Tpointer s t)
     50  | is_true_pointer_pointer: ∀ptr,t.
     51      is_true (Vptr ptr) (Tpointer t)
    5252  | is_true_float: ∀f,sz.
    5353      f ≠ Fzero →
    … …  
    102102      | _ ⇒ None ?
    103103      ]
    104   | Tpointer _ _ ⇒
     104  | Tpointer _ ⇒
    105105      match v with
    106106      [ Vptr _ ⇒ Some ? Vfalse
    107       | Vnull _ ⇒ Some ? Vtrue
     107      | Vnull ⇒ Some ? Vtrue
    108108      | _ ⇒ None ?
    109109      ]
    … …  
    131131        | _ ⇒ None ? ]
    132132      | _ ⇒ None ? ]
    133   | add_case_pi _ _ ty _ _ ⇒                    (**r pointer plus integer *)
     133  | add_case_pi _ ty _ _ ⇒                    (**r pointer plus integer *)
    134134      match v1 with
    135135      [ Vptr ptr1 ⇒ match v2 with
    136136        [ Vint sz2 n2 ⇒ Some ? (Vptr (shift_pointer_n ? ptr1 (sizeof ty) n2))
    137137        | _ ⇒ None ? ]
    138       | Vnull r ⇒ match v2 with
    139         [ Vint sz2 n2 ⇒ if eq_bv ? n2 (zero ?) then Some ? (Vnull r) else None ?
    140         | _ ⇒ None ? ]
    141       | _ ⇒ None ? ]
    142   | add_case_ip _ _ _ _ ty ⇒                    (**r integer plus pointer *)
     138      | Vnull ⇒ match v2 with
     139        [ Vint sz2 n2 ⇒ if eq_bv ? n2 (zero ?) then Some ? Vnull else None ?
     140        | _ ⇒ None ? ]
     141      | _ ⇒ None ? ]
     142  | add_case_ip _ _ _ ty ⇒                    (**r integer plus pointer *)
    143143      match v1 with
    144144      [ Vint sz1 n1 ⇒ match v2 with
    145145        [ Vptr ptr2 ⇒ Some ? (Vptr (shift_pointer_n ? ptr2 (sizeof ty) n1))
    146         | Vnull r ⇒ if eq_bv ? n1 (zero ?) then Some ? (Vnull r) else None ?
     146        | Vnull ⇒ if eq_bv ? n1 (zero ?) then Some ? Vnull else None ?
    147147        | _ ⇒ None ? ]
    148148      | _ ⇒ None ? ]
    … …  
    165165        | _ ⇒ None ? ]
    166166      | _ ⇒ None ? ]
    167   | sub_case_pi _ _ ty _ _ ⇒             (**r pointer minus integer *)
     167  | sub_case_pi _ ty _ _ ⇒             (**r pointer minus integer *)
    168168      match v1 with
    169169      [ Vptr ptr1 ⇒ match v2 with
    170170        [ Vint sz2 n2 ⇒ Some ? (Vptr (neg_shift_pointer_n ? ptr1 (sizeof ty) n2))
    171171        | _ ⇒ None ? ]
    172       | Vnull r ⇒ match v2 with
    173         [ Vint sz2 n2 ⇒ if eq_bv ? n2 (zero ?) then Some ? (Vnull r) else None ?
    174         | _ ⇒ None ? ]
    175       | _ ⇒ None ? ]
    176   | sub_case_pp _ _ _ ty _ _ ⇒             (**r pointer minus pointer *)
     172      | Vnull ⇒ match v2 with
     173        [ Vint sz2 n2 ⇒ if eq_bv ? n2 (zero ?) then Some ? Vnull else None ?
     174        | _ ⇒ None ? ]
     175      | _ ⇒ None ? ]
     176  | sub_case_pp _ _ ty _ ⇒             (**r pointer minus pointer *)
    177177      match v1 with
    178178      [ Vptr ptr1 ⇒ match v2 with
    … …  
    186186          else None ?
    187187        | _ ⇒ None ? ]
    188       | Vnull r ⇒ match v2 with [ Vnull r' ⇒ Some ? (Vint I32 (*XXX*) (zero ?)) | _ ⇒ None ? ]
     188      | Vnull ⇒ match v2 with [ Vnull ⇒ Some ? (Vint I32 (*XXX*) (zero ?)) | _ ⇒ None ? ]
    189189      | _ ⇒ None ? ]
    190190  | sub_default _ _ ⇒ None ?
    … …  
    343343      | _ ⇒ None ?     
    344344      ]
    345   | cmp_case_pp _ _ _ ⇒
     345  | cmp_case_pp _ _ ⇒
    346346      match v1 with
    347347      [ Vptr ptr1 ⇒
    … …  
    354354            else sem_cmp_mismatch c
    355355          else None ?
    356         | Vnull r2 ⇒ sem_cmp_mismatch c
    357         | _ ⇒ None ? ]
    358       | Vnull r1 ⇒
     356        | Vnull ⇒ sem_cmp_mismatch c
     357        | _ ⇒ None ? ]
     358      | Vnull ⇒
    359359        match v2 with
    360360        [ Vptr ptr2 ⇒ sem_cmp_mismatch c
    361         | Vnull r2 ⇒ sem_cmp_match c
     361        | Vnull ⇒ sem_cmp_match c
    362362        | _ ⇒ None ?
    363363        ]
    … …  
    430430  ].
    431431
     432(* Only for full 8051 memory spaces
    432433inductive type_region : type → region → Prop ≝
    433434| type_rgn_pointer : ∀s,t. type_region (Tpointer s t) s
    434435| type_rgn_array : ∀s,t,n. type_region (Tarray s t n) s
    435 (* XXX Is the following necessary? *)
     436(* Is the following necessary? *)
    436437| type_rgn_code : ∀tys,ty. type_region (Tfunction tys ty) Code.
     438*)
     439
     440inductive type_ptr : type → Prop ≝
     441| type_pointer : ∀t. type_ptr (Tpointer t)
     442| type_array : ∀t,n. type_ptr (Tarray t n)
     443| type_fun : ∀tys,ty. type_ptr (Tfunction tys ty).
    437444
    438445inductive cast : mem → val → type → type → val → Prop ≝
    … …  
    449456      cast m (Vfloat f) (Tfloat sz1) (Tfloat sz2)
    450457           (Vfloat (cast_float_float sz2 f))
    451   | cast_pp: ∀m,ty,ty',ptr,r'.
    452       type_region ty (ptype ptr) →
     458  | cast_pp: ∀m,ty,ty',ptr.
     459(*      type_region ty (ptype ptr) →
    453460      type_region ty' r' →
    454461      ∀pc':pointer_compat (pblock ptr) r'.
    455       cast m (Vptr ptr) ty ty' (Vptr (mk_pointer r' (pblock ptr) pc' (poff ptr)))
    456   | cast_ip_z: ∀m,sz,sg,ty',r.
    457       type_region ty' r →
    458       cast m (Vint sz (zero ?)) (Tint sz sg) ty' (Vnull r)
    459   | cast_pp_z: ∀m,ty,ty',r,r'.
    460       type_region ty r →
    461       type_region ty' r' →
    462       cast m (Vnull r) ty ty' (Vnull r').
     462      cast m (Vptr ptr) ty ty' (Vptr (mk_pointer r' (pblock ptr) pc' (poff ptr)))*)
     463      type_ptr ty →
     464      type_ptr ty' →
     465      cast m (Vptr ptr) ty ty' (Vptr ptr)
     466  | cast_ip_z: ∀m,sz,sg,ty'.
     467(*     type_region ty' r →*)
     468      type_ptr ty' →
     469      cast m (Vint sz (zero ?)) (Tint sz sg) ty' Vnull
     470  | cast_pp_z: ∀m,ty,ty'.
     471(*      type_region ty r →
     472      type_region ty' r' →*)
     473      type_ptr ty →
     474      type_ptr ty' →
     475      cast m Vnull ty ty' Vnull.
    463476
    464477(* * * Operational semantics *)
    … …  
    486499let rec load_value_of_type (ty: type) (m: mem) (b: block) (ofs: offset) : option val ≝
    487500  match access_mode ty with
    488   [ By_value chunk ⇒ loadv chunk m (Vptr (mk_pointer Any b ? ofs))
    489   | By_reference r ⇒
    490     match pointer_compat_dec b r with
     501  [ By_value chunk ⇒ loadv chunk m (Vptr (mk_pointer b ofs))
     502  | By_reference  ⇒ Some ? (Vptr (mk_pointer b ofs))
     503(*    match pointer_compat_dec b r with
    491504    [ inl p ⇒ Some ? (Vptr (mk_pointer r b p ofs))
    492505    | inr _ ⇒ None ?
    493     ]
     506    ]*)
    494507  | By_nothing _ ⇒ None ?
    495508  ].
    496 cases b //
    497 qed.
     509(*cases b //
     510qed.*)
    498511
    499512(* * Symmetrically, [store_value_of_type ty m b ofs v] returns the
    … …  
    504517let rec store_value_of_type (ty_dest: type) (m: mem) (loc: block) (ofs: offset) (v: val) : option mem ≝
    505518  match access_mode ty_dest with
    506   [ By_value chunk ⇒ storev chunk m (Vptr (mk_pointer Any loc ? ofs)) v
    507   | By_reference _ ⇒ None ?
     519  [ By_value chunk ⇒ storev chunk m (Vptr (mk_pointer loc ofs)) v
     520  | By_reference ⇒ None ?
    508521  | By_nothing _ ⇒ None ?
    509522  ].
    510 cases loc //
    511 qed.
     523(*cases loc //
     524qed.*)
    512525
    513526(* * Allocation of function-local variables.
    … …  
    526539  | alloc_variables_cons:
    527540      ∀e,m,id,ty,vars,m1,b1,m2,e2.
    528       alloc m 0 (sizeof ty) Any = 〈m1, b1〉 →
     541      alloc m 0 (sizeof ty) XData = 〈m1, b1〉 →
    529542      alloc_variables (add … e id (pi1 … b1)) m1 vars e2 m2 →
    530543      alloc_variables e m (〈id, ty〉 :: vars) e2 m2.
    … …  
    598611      load_value_of_type ty m loc ofs = Some ? v →
    599612      eval_expr ge e m (Expr a ty) v tr
    600   | eval_Eaddrof: ∀a,ty,r,loc,ofs,tr.
     613  | eval_Eaddrof: ∀a,ty,loc,ofs,tr.
    601614      eval_lvalue ge e m a loc ofs tr →
    602       ∀pc:pointer_compat loc r.
    603       eval_expr ge e m (Expr (Eaddrof a) (Tpointer r ty)) (Vptr (mk_pointer r loc pc ofs)) tr
     615(*      ∀pc:pointer_compat loc r.*)
     616      eval_expr ge e m (Expr (Eaddrof a) (Tpointer ty)) (Vptr (mk_pointer loc ofs)) tr
    604617  | eval_Esizeof: ∀ty',sz,sg.
    605618      eval_expr ge e m (Expr (Esizeof ty') (Tint sz sg)) (Vint sz (repr ? (sizeof ty'))) E0
    … …  
    664677      find_symbol … ge id = Some ? l →
    665678      eval_lvalue ge e m (Expr (Evar id) ty) l zero_offset E0
    666   | eval_Ederef: ∀a,ty,r,l,p,ofs,tr.
    667       eval_expr ge e m a (Vptr (mk_pointer r l p ofs)) tr →
     679  | eval_Ederef: ∀a,ty,l,ofs,tr.
     680      eval_expr ge e m a (Vptr (mk_pointer  l ofs)) tr →
    668681      eval_lvalue ge e m (Expr (Ederef a) ty) l ofs tr
    669682    (* Aside: note that each block of memory is entirely contained within one
    … …  
    685698  (ecF:∀f,ty. P ??? (eval_Econst_float ge e m f ty))
    686699  (elv:∀a,ty,loc,ofs,v,tr,H1,H2. P ??? (eval_Elvalue ge e m a ty loc ofs v tr H1 H2))
    687   (ead:∀a,ty,r,loc,pc,ofs,tr,H. P ??? (eval_Eaddrof ge e m a ty r loc pc ofs tr H))
     700  (ead:∀a,ty,loc,ofs,tr,H. P ??? (eval_Eaddrof ge e m a ty loc ofs tr H))
    688701  (esz:∀ty',sz,sg. P ??? (eval_Esizeof ge e m ty' sz sg))
    689702  (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))
    … …  
    702715  | eval_Econst_float f ty ⇒ ecF f ty
    703716  | eval_Elvalue a ty loc ofs v tr H1 H2 ⇒ elv a ty loc ofs v tr H1 H2
    704   | eval_Eaddrof a ty r loc pc ofs tr H ⇒ ead a ty r loc pc ofs tr H
     717  | eval_Eaddrof a ty loc ofs tr H ⇒ ead a ty loc ofs tr H
    705718  | eval_Esizeof ty' sz sg ⇒ esz ty' sz sg
    706719  | eval_Eunop op a ty v1 v tr H1 H2 ⇒ eun op a ty v1 v tr H1 H2 (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a v1 tr H1)
    … …  
    722735  (lvl:∀id,l,ty,H. P ???? (eval_Evar_local ge e m id l ty H))
    723736  (lvg:∀id,l,ty,H1,H2. P ???? (eval_Evar_global ge e m id l ty H1 H2))
    724   (lde:∀a,ty,r,l,pc,ofs,tr,H. P ???? (eval_Ederef ge e m a ty r l pc ofs tr H))
     737  (lde:∀a,ty,l,ofs,tr,H. P ???? (eval_Ederef ge e m a ty l ofs tr H))
    725738  (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))
    726739  (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))
    … …  
    729742  [ eval_Evar_local id l ty H ⇒ lvl id l ty H
    730743  | eval_Evar_global id l ty H1 H2 ⇒ lvg id l ty H1 H2
    731   | eval_Ederef a ty r l pc ofs tr H ⇒ lde a ty r l pc ofs tr H
     744  | eval_Ederef a ty l ofs tr H ⇒ lde a ty l ofs tr H
    732745  | 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)
    733746  | 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)
    … …  
    793806  (ecF:∀f,ty. P ??? (eval_Econst_float ge e m f ty))
    794807  (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))
    795   (ead:∀a,ty,r,loc,pc,ofs,tr,H. Q a loc ofs tr H → P ??? (eval_Eaddrof ge e m a ty r loc ofs tr H pc))
     808  (ead:∀a,ty,loc,ofs,tr,H. Q a loc ofs tr H → P ??? (eval_Eaddrof ge e m a ty loc ofs tr H))
    796809  (esz:∀ty',sz,sg. P ??? (eval_Esizeof ge e m ty' sz sg))
    797810  (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))
    … …  
    807820  (lvl:∀id,l,ty,H. Q ???? (eval_Evar_local ge e m id l ty H))
    808821  (lvg:∀id,l,ty,H1,H2. Q ???? (eval_Evar_global ge e m id l ty H1 H2))
    809   (lde:∀a,ty,r,l,pc,ofs,tr,H. P a (Vptr (mk_pointer r l pc ofs)) tr H → Q ???? (eval_Ederef ge e m a ty r l pc ofs tr H))
     822  (lde:∀a,ty,l,ofs,tr,H. P a (Vptr (mk_pointer l ofs)) tr H → Q ???? (eval_Ederef ge e m a ty l ofs tr H))
    810823  (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))
    811824  (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))
    … …  
    816829  | eval_Econst_float f ty ⇒ ecF f ty
    817830  | 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)
    818   | eval_Eaddrof a ty r loc ofs tr H pc ⇒ ead a ty r loc pc 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)
     831  | eval_Eaddrof a ty loc ofs tr H ⇒ ead a ty 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)
    819832  | eval_Esizeof ty' sz sg ⇒ esz ty' sz sg
    820833  | 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)
    … …  
    835848  (ecF:∀f,ty. P ??? (eval_Econst_float ge e m f ty))
    836849  (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))
    837   (ead:∀a,ty,r,loc,pc,ofs,tr,H. Q a loc ofs tr H → P ??? (eval_Eaddrof ge e m a ty r loc ofs tr H pc))
     850  (ead:∀a,ty,loc,ofs,tr,H. Q a loc ofs tr H → P ??? (eval_Eaddrof ge e m a ty loc ofs tr H))
    838851  (esz:∀ty',sz,sg. P ??? (eval_Esizeof ge e m ty' sz sg))
    839852  (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))
    … …  
    849862  (lvl:∀id,l,ty,H. Q ???? (eval_Evar_local ge e m id l ty H))
    850863  (lvg:∀id,l,ty,H1,H2. Q ???? (eval_Evar_global ge e m id l ty H1 H2))
    851   (lde:∀a,ty,r,l,pc,ofs,tr,H. P a (Vptr (mk_pointer r l pc ofs)) tr H → Q ???? (eval_Ederef ge e m a ty r l pc ofs tr H))
     864  (lde:∀a,ty,l,ofs,tr,H. P a (Vptr (mk_pointer l ofs)) tr H → Q ???? (eval_Ederef ge e m a ty l ofs tr H))
    852865  (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))
    853866  (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))
    … …  
    856869  [ eval_Evar_local id l ty H ⇒ lvl id l ty H
    857870  | eval_Evar_global id l ty H1 H2 ⇒ lvg id l ty H1 H2
    858   | eval_Ederef a ty r l pc ofs tr H ⇒ lde a ty r l pc 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 (mk_pointer r l pc ofs)) tr H)
     871  | eval_Ederef a ty l ofs tr H ⇒ lde a ty 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 (mk_pointer l ofs)) tr H)
    859872  | 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)
    860873  | 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)
    … …  
    10141027| Tint a b ⇒ Tint a b
    10151028| Tfloat a ⇒ Tfloat a
    1016 | Tpointer _ ty ⇒ ty
    1017 | Tarray a b c ⇒ Tarray a b c
     1029| Tpointer ty ⇒ ty
     1030| Tarray a b ⇒ Tarray a b
    10181031| Tfunction a b ⇒ Tfunction a b
    10191032| Tstruct a b ⇒ Tstruct a b
    10201033| Tunion a b ⇒ Tunion a b
    1021 | Tcomp_ptr a b ⇒ Tcomp_ptr a b
     1034| Tcomp_ptr a ⇒ Tcomp_ptr a
    10221035].
    10231036
Note: See TracChangeset for help on using the changeset viewer.