Ignore:
Timestamp:
Feb 22, 2011, 4:23:13 PM (10 years ago)
Author:
campbell
Message:

Abstract pointer offsets a little, similar to the changes for the prototype
proposed in Bologna.

File:
1 edited

Legend:

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

    r582 r583  
    129129      match v1 with
    130130      [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with
    131         [ Vint n2 ⇒ Some ? (Vptr r1 b1 p1 (add ofs1 (mul (repr (sizeof ty)) n2)))
     131        [ Vint n2 ⇒ Some ? (Vptr r1 b1 p1 (shift_offset ofs1 (mul (repr (sizeof ty)) n2)))
    132132        | _ ⇒ None ? ]
    133133      | Vnull r ⇒ match v2 with
     
    138138      match v1 with
    139139      [ Vint n1 ⇒ match v2 with
    140         [ Vptr r2 b2 p2 ofs2 ⇒ Some ? (Vptr r2 b2 p2 (add ofs2 (mul (repr (sizeof ty)) n1)))
     140        [ Vptr r2 b2 p2 ofs2 ⇒ Some ? (Vptr r2 b2 p2 (shift_offset ofs2 (mul (repr (sizeof ty)) n1)))
    141141        | _ ⇒ None ? ]
    142142      | _ ⇒ None ? ]
     
    161161      match v1 with
    162162      [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with
    163         [ Vint n2 ⇒ Some ? (Vptr r1 b1 p1 (sub ofs1 (mul (repr (sizeof ty)) n2)))
     163        [ Vint n2 ⇒ Some ? (Vptr r1 b1 p1 (neg_shift_offset ofs1 (mul (repr (sizeof ty)) n2)))
    164164        | _ ⇒ None ? ]
    165165      | _ ⇒ None ? ]
     
    170170          if eq_block b1 b2 then
    171171            if eq (repr (sizeof ty)) zero then None ?
    172             else Some ? (Vint (divu (sub ofs1 ofs2) (repr (sizeof ty))))
     172            else Some ? (Vint (divu (sub_offset ofs1 ofs2) (repr (sizeof ty))))
    173173          else None ?
    174174        | _ ⇒ None ? ]
     
    323323        match v2 with
    324324        [ Vptr r2 b2 p2 ofs2 ⇒
    325           if valid_pointer m r1 b1 (signed ofs1)
    326           ∧ valid_pointer m r2 b2 (signed ofs2) then
     325          if valid_pointer m r1 b1 ofs1
     326          ∧ valid_pointer m r2 b2 ofs2 then
    327327            if eq_block b1 b2
    328             then Some ? (of_bool (cmp c ofs1 ofs2))
     328            then Some ? (of_bool (cmp_offset c ofs1 ofs2))
    329329            else sem_cmp_mismatch c
    330330          else None ?
     
    463463  reference, the pointer [Vptr b ofs] is returned. *)
    464464
    465 let rec load_value_of_type (ty: type) (m: mem) (b: block) (ofs: int) : option val ≝
     465let rec load_value_of_type (ty: type) (m: mem) (b: block) (ofs: offset) : option val ≝
    466466  match access_mode ty with
    467467  [ By_value chunk ⇒ loadv chunk m (Vptr Any b ? ofs)
     
    481481  This is allowed only if [ty] indicates an access by value. *)
    482482
    483 let rec store_value_of_type (ty_dest: type) (m: mem) (loc: block) (ofs: int) (v: val) : option mem ≝
     483let rec store_value_of_type (ty_dest: type) (m: mem) (loc: block) (ofs: offset) (v: val) : option mem ≝
    484484  match access_mode ty_dest with
    485485  [ By_value chunk ⇒ storev chunk m (Vptr Any loc ? ofs) v
     
    523523      ∀e,m,id,ty,params,v1,vl,b,m1,m2.
    524524      get ??? id e = Some ? b →
    525       store_value_of_type ty m b zero v1 = Some ? m1 →
     525      store_value_of_type ty m b zero_offset v1 = Some ? m1 →
    526526      bind_parameters e m1 params vl m2 →
    527527      bind_parameters e m (〈id, ty〉 :: params) (v1 :: vl) m2.
     
    633633  be representable in a pointer of region r. *)
    634634
    635 with eval_lvalue (*(ge:genv) (e:env) (m:mem)*) : expr → block → int → trace → Prop ≝
     635with eval_lvalue (*(ge:genv) (e:env) (m:mem)*) : expr → block → offset → trace → Prop ≝
    636636  | eval_Evar_local:   ∀id,l,ty.
    637637      (* XXX notation? e!id*) get ??? id e = Some ? l →
    638       eval_lvalue ge e m (Expr (Evar id) ty) l zero E0
     638      eval_lvalue ge e m (Expr (Evar id) ty) l zero_offset E0
    639639  | eval_Evar_global: ∀id,l,ty.
    640640      (* XXX e!id *) get ??? id e = None ? →
    641641      find_symbol ?? ge id = Some ? l →
    642       eval_lvalue ge e m (Expr (Evar id) ty) l zero E0
     642      eval_lvalue ge e m (Expr (Evar id) ty) l zero_offset E0
    643643  | eval_Ederef: ∀a,ty,r,l,p,ofs,tr.
    644644      eval_expr ge e m a (Vptr r l p ofs) tr →
     
    651651      typeof a = Tstruct id fList →
    652652      field_offset i fList = OK ? delta →
    653       eval_lvalue ge e m (Expr (Efield a i) ty) l (add ofs (repr delta)) tr
     653      eval_lvalue ge e m (Expr (Efield a i) ty) l (shift_offset ofs (repr delta)) tr
    654654 | eval_Efield_union:   ∀a,i,ty,l,ofs,id,fList,tr.
    655655      eval_lvalue ge e m a l ofs tr →
     
    702702  (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))
    703703  (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))
    704   (a:expr) (loc:block) (ofs:int) (tr:trace) (ev:eval_lvalue ge e m a loc ofs tr) on ev : P a loc ofs tr ev ≝
     704  (a:expr) (loc:block) (ofs:offset) (tr:trace) (ev:eval_lvalue ge e m a loc ofs tr) on ev : P a loc ofs tr ev ≝
    705705  match ev with
    706706  [ eval_Evar_local id l ty H ⇒ lvl id l ty H
     
    721721     ∀x4: expr.
    722722       ∀x6: block.
    723         ∀x7: int.
     723        ∀x7: offset.
    724724         ∀x8: trace.
    725725          ∀P:
    726726            ∀_z1430: expr.
    727               ∀_z1428: block. ∀_z1427: int. ∀_z1426: trace. Prop.
     727              ∀_z1428: block. ∀_z1427: offset. ∀_z1426: trace. Prop.
    728728           ∀_H1: ?.
    729729            ∀_H2: ?.
     
    739739        (λx4:expr.
    740740            (λx6:block.
    741               (λx7:int.
     741              (λx7:offset.
    742742                (λx8:trace.
    743743                  (λP:∀_z1430: expr.
    744744                         ∀_z1428: block.
    745                           ∀_z1427: int. ∀_z1426: trace. Prop.
     745                          ∀_z1427: offset. ∀_z1426: trace. Prop.
    746746                    (λH1:?.
    747747                      (λH2:?.
     
    752752                                ((λHcut:∀z1435: eq expr x4 x4.
    753753                                           ∀z1433: eq block x6 x6.
    754                                             ∀z1432: eq int x7 x7.
     754                                            ∀z1432: eq offset x7 x7.
    755755                                             ∀z1431: eq trace x8 x8.
    756756                                              P x4 x6 x7 x8.
    757757                                   (Hcut (refl expr x4)
    758758                                     (refl block x6)
    759                                      (refl int x7) (refl trace x8)))
     759                                     (refl offset x7) (refl trace x8)))
    760760                                  ?))))))))))))))).
    761761[ @(eval_lvalue_ind x1 x2 x3 (λa,loc,ofs,tr,e. ∀e1:eq ? x4 a. ∀e3:eq ? x6 loc. ∀e4:eq ? x7 ofs. ∀e5:eq ? x8 tr. P a loc ofs tr) … Hterm)
     
    829829  (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))
    830830  (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))
    831   (a:expr) (loc:block) (ofs:int) (tr:trace) (ev:eval_lvalue ge e m a loc ofs tr) on ev : Q a loc ofs tr ev ≝
     831  (a:expr) (loc:block) (ofs:offset) (tr:trace) (ev:eval_lvalue ge e m a loc ofs tr) on ev : Q a loc ofs tr ev ≝
    832832  match ev with
    833833  [ eval_Evar_local id l ty H ⇒ lvl id l ty H
     
    884884  | Kswitch: cont -> cont
    885885       (**r catches [break] statements arising out of [switch] *)
    886   | Kcall: option (block × int × type) ->  (**r where to store result *)
    887            function ->                      (**r calling function *)
    888            env ->                           (**r local env of calling function *)
     886  | Kcall: option (block × offset × type) -> (**r where to store result *)
     887           function ->                       (**r calling function *)
     888           env ->                            (**r local env of calling function *)
    889889           cont -> cont.
    890890
Note: See TracChangeset for help on using the changeset viewer.