Changeset 1545 for src/Clight/Csem.ma


Ignore:
Timestamp:
Nov 23, 2011, 6:03:07 PM (8 years ago)
Author:
campbell
Message:

Use pointer record in front-end.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Csem.ma

    r1231 r1545  
    4747      n ≠ (zero ?) →
    4848      is_true (Vint sz n) (Tint sz sg)
    49   | is_true_pointer_pointer: ∀r,b,pc,ofs,s,t.
    50       is_true (Vptr r b pc ofs) (Tpointer s t)
     49  | is_true_pointer_pointer: ∀ptr,s,t.
     50      is_true (Vptr ptr) (Tpointer s t)
    5151  | is_true_float: ∀f,sz.
    5252      f ≠ Fzero →
     
    103103  | Tpointer _ _ ⇒
    104104      match v with
    105       [ Vptr _ _ _ _ ⇒ Some ? Vfalse
     105      [ Vptr _ ⇒ Some ? Vfalse
    106106      | Vnull _ ⇒ Some ? Vtrue
    107107      | _ ⇒ None ?
     
    132132  | add_case_pi ty ⇒                    (**r pointer plus integer *)
    133133      match v1 with
    134       [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with
    135         [ Vint sz2 n2 ⇒ Some ? (Vptr r1 b1 p1 (shift_offset_n ? ofs1 (sizeof ty) n2))
     134      [ Vptr ptr1 ⇒ match v2 with
     135        [ Vint sz2 n2 ⇒ Some ? (Vptr (shift_pointer_n ? ptr1 (sizeof ty) n2))
    136136        | _ ⇒ None ? ]
    137137      | Vnull r ⇒ match v2 with
     
    142142      match v1 with
    143143      [ Vint sz1 n1 ⇒ match v2 with
    144         [ Vptr r2 b2 p2 ofs2 ⇒ Some ? (Vptr r2 b2 p2 (shift_offset_n ? ofs2 (sizeof ty) n1))
     144        [ Vptr ptr2 ⇒ Some ? (Vptr (shift_pointer_n ? ptr2 (sizeof ty) n1))
    145145        | Vnull r ⇒ if eq_bv ? n1 (zero ?) then Some ? (Vnull r) else None ?
    146146        | _ ⇒ None ? ]
     
    166166  | sub_case_pi ty ⇒             (**r pointer minus integer *)
    167167      match v1 with
    168       [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with
    169         [ Vint sz2 n2 ⇒ Some ? (Vptr r1 b1 p1 (neg_shift_offset_n ? ofs1 (sizeof ty) n2))
     168      [ Vptr ptr1 ⇒ match v2 with
     169        [ Vint sz2 n2 ⇒ Some ? (Vptr (neg_shift_pointer_n ? ptr1 (sizeof ty) n2))
    170170        | _ ⇒ None ? ]
    171171      | Vnull r ⇒ match v2 with
     
    175175  | sub_case_pp ty ⇒             (**r pointer minus pointer *)
    176176      match v1 with
    177       [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with
    178         [ Vptr r2 b2 p2 ofs2 ⇒
    179           if eq_block b1 b2 then
     177      [ Vptr ptr1 ⇒ match v2 with
     178        [ Vptr ptr2 ⇒
     179          if eq_block (pblock ptr1) (pblock ptr2) then
    180180            if eqb (sizeof ty) 0 then None ?
    181             else match division_u ? (sub_offset ? ofs1 ofs2) (repr (sizeof ty)) with
     181            else match division_u ? (sub_offset ? (poff ptr1) (poff ptr2)) (repr (sizeof ty)) with
    182182                 [ None ⇒ None ?
    183183                 | Some v ⇒ Some ? (Vint I32 v) (* XXX choose size from result type? *)
     
    352352  | cmp_case_pp ⇒
    353353      match v1 with
    354       [ Vptr r1 b1 p1 ofs1 ⇒
     354      [ Vptr ptr1 ⇒
    355355        match v2 with
    356         [ Vptr r2 b2 p2 ofs2 ⇒
    357           if valid_pointer m r1 b1 ofs1
    358           ∧ valid_pointer m r2 b2 ofs2 then
    359             if eq_block b1 b2
    360             then Some ? (of_bool (cmp_offset c ofs1 ofs2))
     356        [ Vptr ptr2 ⇒
     357          if valid_pointer m ptr1
     358          ∧ valid_pointer m ptr2 then
     359            if eq_block (pblock ptr1) (pblock ptr2)
     360            then Some ? (of_bool (cmp_offset c (poff ptr1) (poff ptr2)))
    361361            else sem_cmp_mismatch c
    362362          else None ?
     
    365365      | Vnull r1 ⇒
    366366        match v2 with
    367         [ Vptr r2 b2 p2 ofs2 ⇒ sem_cmp_mismatch c
     367        [ Vptr ptr2 ⇒ sem_cmp_mismatch c
    368368        | Vnull r2 ⇒ sem_cmp_match c
    369369        | _ ⇒ None ?
     
    456456      cast m (Vfloat f) (Tfloat sz1) (Tfloat sz2)
    457457           (Vfloat (cast_float_float sz2 f))
    458   | cast_pp: ∀m,r,r',ty,ty',b,pc,ofs.
    459       type_region ty r
     458  | cast_pp: ∀m,ty,ty',ptr,r'.
     459      type_region ty (ptype ptr)
    460460      type_region ty' r' →
    461       ∀pc':pointer_compat b r'.
    462       cast m (Vptr r b pc ofs) ty ty' (Vptr r' b pc' ofs)
     461      ∀pc':pointer_compat (pblock ptr) r'.
     462      cast m (Vptr ptr) ty ty' (Vptr (mk_pointer r' (pblock ptr) pc' (poff ptr)))
    463463  | cast_ip_z: ∀m,sz,sg,ty',r.
    464464      type_region ty' r →
     
    493493let rec load_value_of_type (ty: type) (m: mem) (b: block) (ofs: offset) : option val ≝
    494494  match access_mode ty with
    495   [ By_value chunk ⇒ loadv chunk m (Vptr Any b ? ofs)
     495  [ By_value chunk ⇒ loadv chunk m (Vptr (mk_pointer Any b ? ofs))
    496496  | By_reference r ⇒
    497497    match pointer_compat_dec b r with
    498     [ inl p ⇒ Some ? (Vptr r b p ofs)
     498    [ inl p ⇒ Some ? (Vptr (mk_pointer r b p ofs))
    499499    | inr _ ⇒ None ?
    500500    ]
     
    511511let rec store_value_of_type (ty_dest: type) (m: mem) (loc: block) (ofs: offset) (v: val) : option mem ≝
    512512  match access_mode ty_dest with
    513   [ By_value chunk ⇒ storev chunk m (Vptr Any loc ? ofs) v
     513  [ By_value chunk ⇒ storev chunk m (Vptr (mk_pointer Any loc ? ofs)) v
    514514  | By_reference _ ⇒ None ?
    515515  | By_nothing ⇒ None ?
     
    608608      eval_lvalue ge e m a loc ofs tr →
    609609      ∀pc:pointer_compat loc r.
    610       eval_expr ge e m (Expr (Eaddrof a) (Tpointer r ty)) (Vptr r loc pc ofs) tr
     610      eval_expr ge e m (Expr (Eaddrof a) (Tpointer r ty)) (Vptr (mk_pointer r loc pc ofs)) tr
    611611  | eval_Esizeof: ∀ty',sz,sg.
    612612      eval_expr ge e m (Expr (Esizeof ty') (Tint sz sg)) (Vint sz (repr ? (sizeof ty'))) E0
     
    672672      eval_lvalue ge e m (Expr (Evar id) ty) l zero_offset E0
    673673  | eval_Ederef: ∀a,ty,r,l,p,ofs,tr.
    674       eval_expr ge e m a (Vptr r l p ofs) tr →
     674      eval_expr ge e m a (Vptr (mk_pointer r l p ofs)) tr →
    675675      eval_lvalue ge e m (Expr (Ederef a) ty) l ofs tr
    676676    (* Aside: note that each block of memory is entirely contained within one
     
    814814  (lvl:∀id,l,ty,H. Q ???? (eval_Evar_local ge e m id l ty H))
    815815  (lvg:∀id,l,ty,H1,H2. Q ???? (eval_Evar_global ge e m id l ty H1 H2))
    816   (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))
     816  (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))
    817817  (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))
    818818  (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))
     
    856856  (lvl:∀id,l,ty,H. Q ???? (eval_Evar_local ge e m id l ty H))
    857857  (lvg:∀id,l,ty,H1,H2. Q ???? (eval_Evar_global ge e m id l ty H1 H2))
    858   (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))
     858  (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))
    859859  (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))
    860860  (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))
     
    863863  [ eval_Evar_local id l ty H ⇒ lvl id l ty H
    864864  | eval_Evar_global id l ty H1 H2 ⇒ lvg id l ty H1 H2
    865   | 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)
     865  | 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)
    866866  | 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)
    867867  | 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.