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

Use dependent pointer type to ensure that the representation is always
compatible with the memory region used.
Add a couple of missing checks as a result...

File:
1 edited

Legend:

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

    r499 r500  
    4848      n ≠ zero →
    4949      is_true (Vint n) (Tint sz sg)
    50   | is_true_pointer_pointer: ∀psp,b,ofs,s,t.
    51       is_true (Vptr psp b ofs) (Tpointer s t)
     50  | is_true_pointer_pointer: ∀r,b,pc,ofs,s,t.
     51      is_true (Vptr r b pc ofs) (Tpointer s t)
    5252  | is_true_float: ∀f,sz.
    5353      f ≠ Fzero →
     
    9696      match v with
    9797      [ Vint n ⇒ Some ? (of_bool (eq n zero))
    98       | Vptr _ _ _ ⇒ Some ? Vfalse
     98      | Vptr _ _ _ _ ⇒ Some ? Vfalse
    9999      | _ ⇒ None ?
    100100      ]
     
    102102      match v with
    103103      [ Vint n ⇒ Some ? (of_bool (eq n zero))
    104       | Vptr _ _ _ ⇒ Some ? Vfalse
     104      | Vptr _ _ _ _ ⇒ Some ? Vfalse
    105105      | _ ⇒ None ?
    106106      ]
     
    129129  | add_case_pi ty ⇒                    (**r pointer plus integer *)
    130130      match v1 with
    131       [ Vptr pcl1 b1 ofs1 ⇒ match v2 with
    132         [ Vint n2 ⇒ Some ? (Vptr pcl1 b1 (add ofs1 (mul (repr (sizeof ty)) n2)))
     131      [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with
     132        [ Vint n2 ⇒ Some ? (Vptr r1 b1 p1 (add ofs1 (mul (repr (sizeof ty)) n2)))
    133133        | _ ⇒ None ? ]
    134134      | Vnull r ⇒ match v2 with
     
    139139      match v1 with
    140140      [ Vint n1 ⇒ match v2 with
    141         [ Vptr pcl2 b2 ofs2 ⇒ Some ? (Vptr pcl2 b2 (add ofs2 (mul (repr (sizeof ty)) n1)))
     141        [ Vptr r2 b2 p2 ofs2 ⇒ Some ? (Vptr r2 b2 p2 (add ofs2 (mul (repr (sizeof ty)) n1)))
    142142        | _ ⇒ None ? ]
    143143      | _ ⇒ None ? ]
     
    161161  | sub_case_pi ty ⇒             (**r pointer minus integer *)
    162162      match v1 with
    163       [ Vptr pcl1 b1 ofs1 ⇒ match v2 with
    164         [ Vint n2 ⇒ Some ? (Vptr pcl1 b1 (sub ofs1 (mul (repr (sizeof ty)) n2)))
     163      [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with
     164        [ Vint n2 ⇒ Some ? (Vptr r1 b1 p1 (sub ofs1 (mul (repr (sizeof ty)) n2)))
    165165        | _ ⇒ None ? ]
    166166      | _ ⇒ None ? ]
    167167  | sub_case_pp ty ⇒             (**r pointer minus pointer *)
    168168      match v1 with
    169       [ Vptr pcl1 b1 ofs1 ⇒ match v2 with
    170         [ Vptr pcl2 b2 ofs2 ⇒
     169      [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with
     170        [ Vptr r2 b2 p2 ofs2 ⇒
    171171          if eq_block b1 b2 then
    172172            if eq (repr (sizeof ty)) zero then None ?
     
    321321         | _ ⇒ None ?
    322322         ]
    323       | Vptr r1 b1 ofs1 ⇒
     323      | Vptr r1 b1 p1 ofs1 ⇒
    324324        match v2 with
    325         [ Vptr r2 b2 ofs2 ⇒
     325        [ Vptr r2 b2 p2 ofs2 ⇒
    326326          if valid_pointer m r1 b1 (signed ofs1)
    327327          ∧ valid_pointer m r2 b2 (signed ofs2) then
     
    334334      | Vnull r1 ⇒
    335335        match v2 with
    336         [ Vptr r2 b2 ofs2 ⇒ sem_cmp_mismatch c
     336        [ Vptr r2 b2 p2 ofs2 ⇒ sem_cmp_mismatch c
    337337        | Vnull r2 ⇒ sem_cmp_match c
    338338        | _ ⇒ None ?
     
    429429      cast m (Vfloat f) (Tfloat sz1) (Tfloat sz2)
    430430           (Vfloat (cast_float_float sz2 f))
    431   | cast_pp: ∀m,r,r',ty,ty',b,ofs.
     431  | cast_pp: ∀m,r,r',ty,ty',b,pc,ofs.
    432432      type_region ty r →
    433433      type_region ty' r' →
    434       pointer_compat b r' →
    435       cast m (Vptr r b ofs) ty ty' (Vptr r' b ofs)
     434      ∀pc':pointer_compat b r'.
     435      cast m (Vptr r b pc ofs) ty ty' (Vptr r' b pc' ofs)
    436436  | cast_ip_z: ∀m,sz,sg,ty',r.
    437437      type_region ty' r →
     
    466466let 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 Any b ofs)
    469   | By_reference r ⇒ Some ? (Vptr r b ofs)
     468  [ By_value chunk ⇒ loadv chunk m (Vptr Any b ? ofs)
     469  | By_reference r ⇒
     470    match pointer_compat_dec b r with
     471    [ inl p ⇒ Some ? (Vptr r b p ofs)
     472    | inr _ ⇒ None ?
     473    ]
    470474  | By_nothing ⇒ None ?
    471475  ].
     476cases b //
     477qed.
    472478
    473479(* * Symmetrically, [store_value_of_type ty m b ofs v] returns the
     
    478484let rec store_value_of_type (ty_dest: type) (m: mem) (loc: block) (ofs: int) (v: val) : option mem ≝
    479485  match access_mode ty_dest with
    480   [ By_value chunk ⇒ storev chunk m (Vptr Any loc ofs) v
     486  [ By_value chunk ⇒ storev chunk m (Vptr Any loc ? ofs) v
    481487  | By_reference _ ⇒ None ?
    482488  | By_nothing ⇒ None ?
    483489  ].
     490cases loc //
     491qed.
    484492
    485493(* * Allocation of function-local variables.
     
    570578  | eval_Eaddrof: ∀a,ty,r,loc,ofs,tr.
    571579      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
     580      ∀pc:pointer_compat loc r.
     581      eval_expr ge e m (Expr (Eaddrof a) (Tpointer r ty)) (Vptr r loc pc ofs) tr
    573582  | eval_Esizeof: ∀ty',ty.
    574583      eval_expr ge e m (Expr (Esizeof ty') ty) (Vint (repr (sizeof ty'))) E0
     
    633642      find_symbol ?? ge id = Some ? l →
    634643      eval_lvalue ge e m (Expr (Evar id) ty) l zero E0
    635   | eval_Ederef: ∀a,ty,r,l,ofs,tr.
    636       eval_expr ge e m a (Vptr r l ofs) tr →
     644  | eval_Ederef: ∀a,ty,r,l,p,ofs,tr.
     645      eval_expr ge e m a (Vptr r l p ofs) tr →
    637646      eval_lvalue ge e m (Expr (Ederef a) ty) l ofs tr
    638647    (* Aside: note that each block of memory is entirely contained within one
     
    654663  (ecF:∀f,ty. P ??? (eval_Econst_float ge e m f ty))
    655664  (elv:∀a,ty,loc,ofs,v,tr,H1,H2. P ??? (eval_Elvalue ge e m a ty loc ofs v tr H1 H2))
    656   (ead:∀a,ty,psp,loc,ofs,tr,H. P ??? (eval_Eaddrof ge e m a ty psp loc ofs tr H))
     665  (ead:∀a,ty,r,loc,pc,ofs,tr,H. P ??? (eval_Eaddrof ge e m a ty r loc pc ofs tr H))
    657666  (esz:∀ty',ty. P ??? (eval_Esizeof ge e m ty' ty))
    658667  (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))
     
    671680  | eval_Econst_float f ty ⇒ ecF f ty
    672681  | eval_Elvalue a ty loc ofs v tr H1 H2 ⇒ elv a ty loc ofs v tr H1 H2
    673   | eval_Eaddrof a ty psp loc ofs tr H ⇒ ead a ty psp loc ofs tr H
     682  | eval_Eaddrof a ty r loc pc ofs tr H ⇒ ead a ty r loc pc ofs tr H
    674683  | eval_Esizeof ty' ty ⇒ esz ty' ty
    675684  | 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)
     
    691700  (lvl:∀id,l,ty,H. P ???? (eval_Evar_local ge e m id l ty H))
    692701  (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))
     702  (lde:∀a,ty,r,l,pc,ofs,tr,H. P ???? (eval_Ederef ge e m a ty r l pc ofs tr H))
    694703  (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))
    695704  (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))
     
    698707  [ eval_Evar_local id l ty H ⇒ lvl id l ty H
    699708  | eval_Evar_global id l ty H1 H2 ⇒ lvg id l ty H1 H2
    700   | eval_Ederef a ty psp l ofs tr H ⇒ lde a ty psp l ofs tr H
     709  | eval_Ederef a ty r l pc ofs tr H ⇒ lde a ty r l pc ofs tr H
    701710  | 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)
    702711  | 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)
     
    762771  (ecF:∀f,ty. P ??? (eval_Econst_float ge e m f ty))
    763772  (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))
     773  (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))
    765774  (esz:∀ty',ty. P ??? (eval_Esizeof ge e m ty' ty))
    766775  (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))
     
    776785  (lvl:∀id,l,ty,H. Q ???? (eval_Evar_local ge e m id l ty H))
    777786  (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))
     787  (lde:∀a,ty,r,l,pc,ofs,tr,H. P a (Vptr r l pc ofs) tr H → Q ???? (eval_Ederef ge e m a ty r l pc ofs tr H))
    779788  (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))
    780789  (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))
     
    785794  | eval_Econst_float f ty ⇒ ecF f ty
    786795  | 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)
     796  | 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)
    788797  | eval_Esizeof ty' ty ⇒ esz ty' ty
    789798  | 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)
     
    804813  (ecF:∀f,ty. P ??? (eval_Econst_float ge e m f ty))
    805814  (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))
     815  (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))
    807816  (esz:∀ty',ty. P ??? (eval_Esizeof ge e m ty' ty))
    808817  (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))
     
    818827  (lvl:∀id,l,ty,H. Q ???? (eval_Evar_local ge e m id l ty H))
    819828  (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))
     829  (lde:∀a,ty,r,l,pc,ofs,tr,H. P a (Vptr r l pc ofs) tr H → Q ???? (eval_Ederef ge e m a ty r l pc ofs tr H))
    821830  (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))
    822831  (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))
     
    825834  [ eval_Evar_local id l ty H ⇒ lvl id l ty H
    826835  | eval_Evar_global id l ty H1 H2 ⇒ lvg id l ty H1 H2
    827   | 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)
     836  | 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 r l pc ofs) tr H)
    828837  | 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)
    829838  | 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)
Note: See TracChangeset for help on using the changeset viewer.