Changeset 1545


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

Use pointer record in front-end.

Location:
src
Files:
9 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Cexec.ma

    r1516 r1545  
    2323    | _ ⇒ Error ? (msg TypeMismatch)
    2424    ]
    25   | Vptr _ _ _ _ ⇒ match ty with
     25  | Vptr _ ⇒ match ty with
    2626    [ Tpointer _ _ ⇒ OK ? true
    2727    | _ ⇒ Error ? (msg TypeMismatch)
     
    3737#v #ty #r #H elim H; #v #t #H' elim H';
    3838  [ * #sg #i #ne %{ true} % // whd in ⊢ (??%?); >(eq_bv_false … ne) //
    39   | #r #b #pc #i #i0 #s %{ true} % //
     39  | #ptr #r #ty %{ true} % //
    4040  | #f #s #ne %{ true} % //; whd in ⊢ (??%?); >(Feq_zero_false … ne) //;
    4141  | * #sg %{ false} % //
     
    124124  | _ ⇒ Error ? (msg TypeMismatch)
    125125  ]
    126 | Vptr r b _ ofs
     126| Vptr ptr
    127127    do s ← match ty with [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code | _ ⇒ Error ? (msg TypeMismatch) ];
    128     do u ← match eq_region_dec r s with [ inl _ ⇒ OK ? it | inr _ ⇒ Error ? (msg BadCast) ];
     128    do u ← match eq_region_dec (ptype ptr) s with [ inl _ ⇒ OK ? it | inr _ ⇒ Error ? (msg BadCast) ];
    129129    do s' ← match ty' with
    130130         [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code
    131131         | _ ⇒ Error ? (msg BadCast)];
    132     match pointer_compat_dec b s' with
    133     [ inl p' ⇒ OK ? (Vptr s' b p' ofs)
     132    match pointer_compat_dec (pblock ptr) s' with
     133    [ inl p' ⇒ OK ? (Vptr (mk_pointer s' (pblock ptr) p' (poff ptr)))
    134134    | inr _ ⇒ Error ? (msg BadCast)
    135135    ]
     
    187187        match lo with [ pair loc ofs ⇒
    188188          match pointer_compat_dec loc r with
    189           [ inl pc ⇒ OK ? 〈Vptr r loc pc ofs, tr〉
     189          [ inl pc ⇒ OK ? 〈Vptr (mk_pointer r loc pc ofs), tr〉
    190190          | inr _ ⇒ Error ? (msg TypeMismatch)
    191191          ]
     
    249249      do 〈v,tr〉 ← exec_expr ge en m a;
    250250      match v with
    251       [ Vptr _ l _ ofs ⇒ OK ? 〈〈l,ofs〉,tr〉
     251      [ Vptr ptr ⇒ OK ? 〈〈pblock ptr, poff ptr〉,tr〉
    252252      | _ ⇒ Error ? (msg TypeMismatch)
    253253      ]
     
    535535    | #f %2 ; % *;   #r #H inversion H; #i #m #e destruct;
    536536    | #r %2 ; % *;   #r #H inversion H; #i #m #e destruct;
    537     | #r #b #pc #of %2 ; % *;   #r #H inversion H; #i #m #e destruct;
     537    | #ptr %2 ; % *;   #r #H inversion H; #i #m #e destruct;
    538538    ]
    539539  | #a #b %2 ; % *; #r #H inversion H; #i #m #e destruct;
  • src/Clight/CexecComplete.ma

    r1521 r1545  
    104104| #m #sz #sz' #sg #i whd in ⊢ (??%?); >intsize_eq_elim_true @refl
    105105| #m #f #sz #sz' @refl
    106 | #m #r #r' #ty #ty' #b #pc #ofs #H1 #H2 #pc'
     106| #m #ty #ty' * #r #b #pc #ofs #r' #H1 #H2 #pc'
    107107    elim H1 in pc ⊢ %; [ #r1 #ty1 #pc | #r1 #ty1 #n1 #pc | #tys1 #ty1 #pc letin r1 ≝ Code ]
    108108    whd in ⊢ (??%?);
     
    134134  [ #sz #sg #i #ne %{ true} % //; whd in ⊢ (??%?); >intsize_eq_elim_true
    135135    >(eq_bv_false … ne) //
    136   | #r #b #pc #i #i0 #s %{ true} % //
     136  | * #r #b #pc #i #i0 #s %{ true} % //
    137137  | #f #s #ne %{ true} % //; whd; >(Feq_zero_false … ne) //;
    138138  | #sz #sg %{ false} % // whd in ⊢ (??%?); >intsize_eq_elim_true >eq_bv_true //
     
    145145#v #ty #H elim H;
    146146  [ #i #is #s #ne whd in ⊢ (??%?); >intsize_eq_elim_true >(eq_bv_false … ne) //;
    147   | #p #b #i #i0 #s //
     147  | * #p #b #i #i0 #s //
    148148  | #f #s #ne whd; >(Feq_zero_false … ne) //;
    149149  ]
  • src/Clight/CexecSound.ma

    r1516 r1545  
    44 exec_bool_of_val v ty = OK ? r → bool_of_val v ty (of_bool r).
    55#v #ty #r
    6 cases v; [ | #sz #i | #f | #r1 | #r' #b #pc #of ]
     6cases v; [ | #sz #i | #f | #r1 | #ptr ]
    77cases ty; [ 2,11,20,29,38: #sz' #sg | 3,12,21,30,39: #sz' | 4,13,22,31,40: #rg #ty | 5,14,23,32,41: #r #ty #n | 6,15,24,33,42: #args #rty | 7,8,16,17,25,26,34,35,43,44: #id #fs | 9,18,27,36,45: #r #id ]
    88whd in ⊢ (??%? → ?);
     
    100100    cases ty' in H2; normalize; try #a try #b try #c try #d destruct;
    101101    @cast_pp_z //;
    102 | #r #b #pc #of whd in ⊢ (??%? → ?); #e
     102| #ptr whd in ⊢ (??%? → ?); #e
    103103    elim (bind_inversion ????? e) #s * #es #e'
    104104    elim (bind_inversion ????? e') #u * #eu #e'' -e';
     
    112112            whd in e:(??%?); destruct; //;
    113113        | #Hty'
    114             cut (s = r). elim (eq_region_dec r s) in eu; //; normalize; #_ #e destruct.
     114            cut (s = ptype ptr). elim (eq_region_dec (ptype ptr) s) in eu; //; normalize; #_ #e destruct.
    115115            #e >e in Hty; #Hty
    116             cases (pointer_compat_dec b s') in e''';
     116            cases (pointer_compat_dec (pblock ptr) s') in e''';
    117117            #Hcompat #e''' whd in e''':(??%?); destruct (e'''); /2/
    118118        ]
     
    207207    ]
    208208| #ty #e #He whd in ⊢ (???%);
    209     @bind2_OK #v cases v // #r #l #pc #ofs #tr #Hv whd
     209    @bind2_OK #v cases v // * #r #l #pc #ofs #tr #Hv whd
    210210    >Hv in He; #He
    211211    @eval_Ederef [ 3: @He | *: skip ]
    212212| #ty #e'' #ty'' #He'' @bind2_OK * #loc #ofs #tr #H
    213   cases ty // * #pty
     213  cases ty try (try #a try #b try #c @I) * #pty
    214214  cases loc in H ⊢ %; * #loc' #H
    215215  whd try @I
     
    276276
    277277lemma addrof_eval_lvalue: ∀ge,en,m,e,r,loc,pc,off,tr,ty.
    278 eval_expr ge en m (Expr (Eaddrof e) ty) (Vptr r loc pc off) tr →
     278eval_expr ge en m (Expr (Eaddrof e) ty) (Vptr (mk_pointer r loc pc off)) tr →
    279279eval_lvalue ge en m e loc off tr.
    280280#ge #en #m #e #r #loc #pc #off #tr #ty #H inversion H;
     
    303303lemma addrof_exec_lvalue: ∀ge,en,m,e,r,loc,off,tr.
    304304exec_lvalue ge en m e = OK ? 〈〈mk_block r loc,off〉,tr〉 →
    305 exec_expr ge en m (Expr (Eaddrof e) (Tpointer r Tvoid)) = OK ? 〈Vptr r (mk_block r loc) (same_compat ??) off, tr〉.
     305exec_expr ge en m (Expr (Eaddrof e) (Tpointer r Tvoid)) = OK ? 〈Vptr (mk_pointer r (mk_block r loc) (same_compat ??) off), tr〉.
    306306#ge #en #m #e #r #loc #off #tr #H whd in ⊢ (??%?);
    307307>H whd in ⊢ (??%?); cases r @refl
  • 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)
  • src/common/FrontEndOps.ma

    r1516 r1545  
    8484      match find_symbol s with
    8585      [ None ⇒ None ?
    86       | Some b ⇒ Some ? (Vptr Any b (match b with [ mk_block r id ⇒ universal_compat r id ]) (shift_offset ? zero_offset (repr I16 ofs)))
     86      | Some b ⇒ Some ? (Vptr (mk_pointer Any b (match b with [ mk_block r id ⇒ universal_compat r id ]) (shift_offset ? zero_offset (repr I16 ofs))))
    8787      ]
    8888  | Oaddrstack ofs ⇒
    89       Some ? (Vptr Any sp ? (shift_offset ? zero_offset (repr I16 ofs)))
     89      Some ? (Vptr (mk_pointer Any sp ? (shift_offset ? zero_offset (repr I16 ofs))))
    9090  ]. cases sp // qed.
    9191
     
    102102      match arg with
    103103      [ Vint sz1 n1 ⇒ Some ? (Vint sz (if (eq_bv ? n1 (zero ?)) then (repr ? 1) else (zero ?)))
    104       | Vptr _ _ _ _ ⇒ Some ? (Vint sz (zero ?))
     104      | Vptr _ ⇒ Some ? (Vint sz (zero ?))
    105105      | Vnull _ ⇒ Some ? (Vint sz (repr ? 1))
    106106      | _ ⇒ None ?
     
    125125[ ASTint sz sg ⇒ ∀i.P (Vint sz i)
    126126| ASTfloat sz ⇒ ∀f.P (Vfloat f)
    127 | ASTptr r ⇒ P (Vnull r) ∧ ∀b,c,o. P (Vptr r b c o)
     127| ASTptr r ⇒ P (Vnull r) ∧ ∀b,c,o. P (Vptr (mk_pointer r b c o))
    128128] →
    129129P v.
     
    197197definition ev_addp ≝ λv1,v2: val.
    198198  match v1 with
    199   [ Vptr r b1 p ofs1 ⇒ match v2 with
    200     [ Vint sz2 n2 ⇒ Some ? (Vptr r b1 p (shift_offset ? ofs1 n2))
     199  [ Vptr ptr1 ⇒ match v2 with
     200    [ Vint sz2 n2 ⇒ Some ? (Vptr (shift_pointer ? ptr1 n2))
    201201    | _ ⇒ None ? ]
    202202  | Vnull r ⇒ match v2 with
     
    208208definition ev_subpi ≝ λv1,v2: val.
    209209  match v1 with
    210   [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with
    211     [ Vint sz2 n2 ⇒ Some ? (Vptr r1 b1 p1 (neg_shift_offset ? ofs1 n2))
     210  [ Vptr ptr1 ⇒ match v2 with
     211    [ Vint sz2 n2 ⇒ Some ? (Vptr (neg_shift_pointer ? ptr1 n2))
    212212    | _ ⇒ None ? ]
    213213  | Vnull r ⇒ match v2 with [ Vint sz2 n2 ⇒ if eq_bv ? n2 (zero ?) then Some ? (Vnull r) else None ? | _ ⇒ None ? ]
     
    216216definition ev_subpp ≝ λsz. λv1,v2: val.
    217217  match v1 with
    218   [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with
    219     [ Vptr r2 b2 p2 ofs2 ⇒
    220         if eq_block b1 b2 then Some ? (Vint sz (sub_offset ? ofs1 ofs2)) else None ?
     218  [ Vptr ptr1 ⇒ match v2 with
     219    [ Vptr ptr2 ⇒
     220        if eq_block (pblock ptr1) (pblock ptr2)
     221          then Some ? (Vint sz (sub_offset ? (poff ptr1) (poff ptr2)))
     222          else None ?
    221223    | _ ⇒ None ? ]
    222224  | Vnull r ⇒ match v2 with [ Vnull r' ⇒ Some ? (Vint sz (zero ?)) | _ ⇒ None ? ]
     
    384386definition ev_cmpp ≝ λc: comparison. λv1,v2: val.
    385387  match v1 with
    386   [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with
    387     [ Vptr r2 b2 p2 ofs2 ⇒
    388         if eq_block b1 b2
    389         then Some ? (of_bool (cmp_offset c ofs1 ofs2))
     388  [ Vptr ptr1 ⇒ match v2 with
     389    [ Vptr ptr2 ⇒
     390        if eq_block (pblock ptr1) (pblock ptr2)
     391        then Some ? (of_bool (cmp_offset c (poff ptr1) (poff ptr2)))
    390392        else ev_cmp_mismatch c
    391393    | Vnull r2 ⇒ ev_cmp_mismatch c
    392394    | _ ⇒ None ? ]
    393395  | Vnull r1 ⇒ match v2 with
    394     [ Vptr _ _ _ _ ⇒ ev_cmp_mismatch c
     396    [ Vptr _ ⇒ ev_cmp_mismatch c
    395397    | Vnull r2 ⇒ ev_cmp_match c
    396398    | _ ⇒ None ?
  • src/common/Globalenvs.ma

    r1395 r1545  
    416416      | Some b' ⇒
    417417        match pointer_compat_dec b' r' with
    418         [ inl pc ⇒ store (Mpointer r') m r b p (Vptr r' b' pc (shift_offset ? zero_offset (repr I16 ofs)))
     418        [ inl pc ⇒ store (Mpointer r') m r b p (Vptr (mk_pointer r' b' pc (shift_offset ? zero_offset (repr I16 ofs))))
    419419        | inr _ ⇒ None ?
    420420        ]
     
    540540  init_mem_
    541541  (λF,ge. functions ? ge) (* find_funct_ptr *)
    542   (λF,ge,v. match v with [ Vptr _ b _ o ⇒ if eq_offset o zero_offset then functions ? ge b else None ? | _ ⇒ None ? ]) (* find_funct *)
     542  (λF,ge,v. match v with [ Vptr ptr ⇒ if eq_offset (poff ptr) zero_offset then functions ? ge (pblock ptr) else None ? | _ ⇒ None ? ]) (* find_funct *)
    543543  (λF,ge. symbols ? ge) (* find_symbol *)
    544544(*  ?
  • src/common/Mem.ma

    r1523 r1545  
    643643  given offset falls within the bounds of the corresponding block. *)
    644644
    645 definition valid_pointer : mem → region → block → offset → bool ≝
    646 λm,r,b,ofs. Zltb (block_id b) (nextblock m) ∧
    647   Zleb (low_bound m b) (offv ofs) ∧
    648   Zltb (offv ofs) (high_bound m b) ∧
    649   is_pointer_compat b r.
     645definition valid_pointer : mem → pointer → bool ≝
     646λm,ptr. Zltb (block_id (pblock ptr)) (nextblock m) ∧
     647  Zleb (low_bound m (pblock ptr)) (offv (poff ptr)) ∧
     648  Zltb (offv (poff ptr)) (high_bound m (pblock ptr)).
    650649
    651650(* [load chunk m r b ofs] perform a read in memory state [m], at address
     
    679678let rec loadv (chunk:memory_chunk) (m:mem) (addr:val) on addr : option val ≝
    680679  match addr with
    681   [ Vptr r b p ofs ⇒ load chunk m r b (offv ofs)
     680  [ Vptr ptr ⇒ load chunk m (ptype ptr) (pblock ptr) (offv (poff ptr))
    682681  | _ ⇒ None ? ].
    683682
     
    726725λchunk,m,addr,v.
    727726  match addr with
    728   [ Vptr r b p ofs ⇒ store chunk m r b (offv ofs) v
     727  [ Vptr ptr ⇒ store chunk m (ptype ptr) (pblock ptr) (offv (poff ptr)) v
    729728  | _ ⇒ None ? ].
    730729
     
    35153514  storev Mint8signed m a v = storev Mint8unsigned m a v.
    35163515#m #a #v whd in ⊢ (??%%); elim a //
    3517 #r #b #p #ofs whd in ⊢ (??%%);
     3516#ptr whd in ⊢ (??%%);
    35183517>(in_bounds_equiv Mint8signed Mint8unsigned … (option mem) ???) //
    35193518qed.
     
    35233522  storev Mint16signed m a v = storev Mint16unsigned m a v.
    35243523#m #a #v whd in ⊢ (??%%); elim a //
    3525 #r #b #p #ofs whd in ⊢ (??%%);
     3524#ptr whd in ⊢ (??%%);
    35263525>(in_bounds_equiv Mint16signed Mint16unsigned … (option mem) ???) //
    35273526qed.
  • src/common/Pointers.ma

    r1516 r1545  
    100100 λn,p,i. mk_pointer (ptype p) (pblock p) (pok p) (shift_offset n (poff p) i).
    101101
     102(* multiply shift by a nat (i.e., sizeof) without danger of overflow *)
     103definition shift_pointer_n: ∀n. pointer → nat → BitVector n → pointer ≝
     104 λn,p,i,j. mk_pointer (ptype p) (pblock p) (pok p) (shift_offset_n n (poff p) i j).
     105
    102106definition neg_shift_pointer: ∀n. pointer → BitVector n → pointer ≝
    103107 λn,p,i. mk_pointer (ptype p) (pblock p) (pok p) (neg_shift_offset n (poff p) i).
     108
     109definition neg_shift_pointer_n: ∀n. pointer → nat → BitVector n → pointer ≝
     110 λn,p,i,j. mk_pointer (ptype p) (pblock p) (pok p) (neg_shift_offset_n n (poff p) i j).
    104111
    105112definition eq_pointer: pointer → pointer → bool ≝
  • src/common/Values.ma

    r1510 r1545  
    3939  | Vfloat: float → val
    4040  | Vnull: region → val
    41   | Vptr: ∀r:region. ∀b:block. pointer_compat b r → offset → val.
     41  | Vptr: pointer → val.
    4242
    4343definition Vzero : intsize → val ≝ λsz. Vint sz (zero ?).
     
    5454  | VTfloat: ∀sz,f. val_typ (Vfloat f) (ASTfloat sz)
    5555  | VTnull: ∀r. val_typ (Vnull r) (ASTptr r)
    56   | VTptr: ∀r,b,c,o. val_typ (Vptr r b c o) (ASTptr r).
     56  | VTptr: ∀r,b,c,o. val_typ (Vptr (mk_pointer r b c o)) (ASTptr r).
    5757
    5858(*
     
    6464*)
    6565definition of_bool : bool → val ≝ λb. if b then Vtrue else Vfalse.
    66 (*
    67 definition has_type ≝ λv: val. λt: typ.
    68   match v with
    69   [ Vundef ⇒ True
    70   | Vint _ ⇒ match t with [ ASTint ⇒ True | _ ⇒ False ]
    71   | Vfloat _ ⇒ match t with [ ASTfloat ⇒ True | _ ⇒ False ]
    72   | Vptr _ _ _ ⇒ match t with [ ASTptr ⇒ True | _ ⇒ False ]
    73   | _ ⇒ False
    74   ].
    75 
    76 let rec has_type_list (vl: list val) (tl: list typ) on vl : Prop ≝
    77   match vl with
    78   [ nil ⇒ match tl with [ nil ⇒ True | _ ⇒ False ]
    79   | cons v1 vs ⇒ match tl with [ nil ⇒ False | cons t1 ts ⇒
    80                has_type v1 t1 ∧ has_type_list vs ts ]
    81   ].
    82 *)
     66
    8367(* * Truth values.  Pointers and non-zero integers are treated as [True].
    8468  The integer 0 (also used to represent the null pointer) is [False].
     
    8872  match v with
    8973  [ Vint _ n ⇒ n ≠ (zero ?)
    90   | Vptr _ b _ ofs ⇒ True
     74  | Vptr _ ⇒ True
    9175  | _ ⇒ False
    9276  ].
     
    10589      ∀sz. bool_of_val (Vzero sz) false
    10690  | bool_of_val_ptr:
    107       ∀r,b,p,ofs. bool_of_val (Vptr r b p ofs) true
     91      ∀p. bool_of_val (Vptr p) true
    10892  | bool_of_val_null:
    10993      ∀r. bool_of_val (Vnull r) true.
     
    11599[ Vint _ i ⇒ OK ? (notb (eq_bv ? i (zero ?)))
    116100| Vnull _ ⇒ OK ? false
    117 | Vptr _ _ _ _ ⇒ OK ? true
     101| Vptr _ ⇒ OK ? true
    118102| _ ⇒ Error ? (msg ValueNotABoolean)
    119103].
     
    170154  match v with
    171155  [ Vint sz n ⇒ of_bool (eq_bv ? n (zero ?))
    172   | Vptr _ b _ ofs ⇒ Vfalse
     156  | Vptr _ ⇒ Vfalse
    173157  | Vnull _ ⇒ Vtrue
    174158  | _ ⇒ Vundef
     
    200184                    (λn1. Vint sz2 (addition_n ? n1 n2))
    201185                    Vundef
    202     | Vptr r b2 p ofs2 ⇒ Vptr r b2 p (shift_offset ? ofs2 n1)
    203     | _ ⇒ Vundef ]
    204   | Vptr r b1 p ofs1 ⇒ match v2 with
    205     [ Vint _ n2 ⇒ Vptr r b1 p (shift_offset ? ofs1 n2)
     186    | Vptr ptr ⇒ Vptr (shift_pointer ? ptr n1)
     187    | _ ⇒ Vundef ]
     188  | Vptr ptr ⇒ match v2 with
     189    [ Vint _ n2 ⇒ Vptr (shift_pointer ? ptr n2)
    206190    | _ ⇒ Vundef ]
    207191  | _ ⇒ Vundef ].
     
    216200                    Vundef
    217201    | _ ⇒ Vundef ]
    218   | Vptr r1 b1 p1 ofs1 ⇒ match v2 with
    219     [ Vint sz2 n2 ⇒ Vptr r1 b1 p1 (neg_shift_offset ? ofs1 n2)
    220     | Vptr r2 b2 p2 ofs2 ⇒
    221         if eq_block b1 b2 then Vint I32 (sub_offset ? ofs1 ofs2) else Vundef
     202  | Vptr ptr1 ⇒ match v2 with
     203    [ Vint sz2 n2 ⇒ Vptr (neg_shift_pointer ? ptr1 n2)
     204    | Vptr ptr2 ⇒
     205        if eq_block (pblock ptr1) (pblock ptr2)
     206          then Vint I32 (sub_offset ? (poff ptr1) (poff ptr2))
     207          else Vundef
    222208    | _ ⇒ Vundef ]
    223209  | Vnull r ⇒ match v2 with [ Vnull r' ⇒ Vzero I32 | _ ⇒ Vundef ]
     
    430416                    Vundef
    431417    | _ ⇒ Vundef ]
    432   | Vptr r1 b1 p1 ofs1 ⇒ match v2 with
    433     [ Vptr r2 b2 p2 ofs2 ⇒
    434         if eq_block b1 b2
    435         then of_bool (cmp_offset c ofs1 ofs2)
     418  | Vptr ptr1 ⇒ match v2 with
     419    [ Vptr ptr2 ⇒
     420        if eq_block (pblock ptr1) (pblock ptr2)
     421        then of_bool (cmp_offset c (poff ptr1) (poff ptr2))
    436422        else cmp_mismatch c
    437423    | Vnull r2 ⇒ cmp_mismatch c
    438424    | _ ⇒ Vundef ]
    439425  | Vnull r1 ⇒ match v2 with
    440     [ Vptr _ _ _ _ ⇒ cmp_mismatch c
     426    [ Vptr _ ⇒ cmp_mismatch c
    441427    | Vnull r2 ⇒ cmp_match c
    442428    | _ ⇒ Vundef
     
    451437                    Vundef
    452438    | _ ⇒ Vundef ]
    453   | Vptr r1 b1 p1 ofs1 ⇒ match v2 with
    454     [ Vptr r2 b2 p2 ofs2 ⇒
    455         if eq_block b1 b2
    456         then of_bool (cmp_offset c ofs1 ofs2)
     439  | Vptr ptr1 ⇒ match v2 with
     440    [ Vptr ptr2 ⇒
     441        if eq_block (pblock ptr1) (pblock ptr2)
     442        then of_bool (cmp_offset c (poff ptr1) (poff ptr2))
    457443        else cmp_mismatch c
    458444    | Vnull r2 ⇒ cmp_mismatch c
    459445    | _ ⇒ Vundef ]
    460446  | Vnull r1 ⇒ match v2 with
    461     [ Vptr _ _ _ _ ⇒ cmp_mismatch c
     447    [ Vptr _ ⇒ cmp_mismatch c
    462448    | Vnull r2 ⇒ cmp_match c
    463449    | _ ⇒ Vundef
     
    495481    | _ ⇒ Vundef
    496482    ]
    497   | Vptr r b p ofs
     483  | Vptr ptr
    498484    match chunk with
    499     [ Mpointer r' ⇒ if eq_region r r' then Vptr r b p ofs else Vundef
     485    [ Mpointer r ⇒ if eq_region (ptype ptr) r then Vptr ptr else Vundef
    500486    | _ ⇒ Vundef
    501487    ]
Note: See TracChangeset for help on using the changeset viewer.