Changeset 1545 for src/Clight


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

Use pointer record in front-end.

Location:
src/Clight
Files:
4 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)
Note: See TracChangeset for help on using the changeset viewer.