Changeset 583 for Deliverables


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.

Location:
Deliverables/D3.1/C-semantics
Files:
5 edited

Legend:

Unmodified
Added
Removed

  • Deliverables/D3.1/C-semantics/Cexec.ma

    r500 r583  
    263263  ]
    264264]
    265 and exec_lvalue' (ge:genv) (en:env) (m:mem) (e':expr_descr) (ty:type) on e' : res (block × int × trace) ≝
     265and exec_lvalue' (ge:genv) (en:env) (m:mem) (e':expr_descr) (ty:type) on e' : res (block × offset × trace) ≝
    266266  match e' with
    267267  [ Evar id ⇒
    268268      match (get … id en) with
    269       [ None ⇒ do l ← opt_to_res ? (find_symbol ? ? ge id); OK ? 〈〈l,zero〉,E0〉 (* global *)
    270       | Some loc ⇒ OK ? 〈〈loc,zero〉,E0〉 (* local *)
     269      [ None ⇒ do l ← opt_to_res ? (find_symbol ? ? ge id); OK ? 〈〈l,zero_offset〉,E0〉 (* global *)
     270      | Some loc ⇒ OK ? 〈〈loc,zero_offset〉,E0〉 (* local *)
    271271      ]
    272272  | Ederef a ⇒
    … …  
    281281          do 〈lofs,tr〉 ← exec_lvalue ge en m a;
    282282          do delta ← field_offset i fList;
    283           OK ? 〈〈\fst lofs,add (\snd lofs) (repr delta)〉,tr〉
     283          OK ? 〈〈\fst lofs,shift_offset (\snd lofs) (repr delta)〉,tr〉
    284284      | Tunion id fList ⇒
    285285          do 〈lofs,tr〉 ← exec_lvalue ge en m a;
    … …  
    289289  | _ ⇒ Error ?
    290290  ]
    291 and exec_lvalue (ge:genv) (en:env) (m:mem) (e:expr) on e : res (block × int × trace) ≝
     291and exec_lvalue (ge:genv) (en:env) (m:mem) (e:expr) on e : res (block × offset × trace) ≝
    292292match e with [ Expr e' ty ⇒ exec_lvalue' ge en m e' ty ].
    293293
    … …  
    332332      | cons v1 vl ⇒
    333333          do b ← opt_to_res ? (get … id e);
    334           do m1 ← opt_to_res ? (store_value_of_type ty m b zero v1);
     334          do m1 ← opt_to_res ? (store_value_of_type ty m b zero_offset v1);
    335335          exec_bind_parameters e m1 params' vl
    336336      ]

  • 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

  • Deliverables/D3.1/C-semantics/Globalenvs.ma

    r500 r583  
    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 ofs)
     418        [ inl pc ⇒ store (Mpointer r') m r b p (Vptr r' b' pc (shift_offset zero_offset ofs))
    419419        | inr _ ⇒ None ?
    420420        ]
    … …  
    523523  init_mem_
    524524  (λF,ge. functions ? ge) (* find_funct_ptr *)
    525   (λF,ge,v. match v with [ Vptr _ b _ o ⇒ if eq o zero then functions ? ge b else None ? | _ ⇒ None ? ]) (* find_funct *)
     525  (λF,ge,v. match v with [ Vptr _ b _ o ⇒ if eq_offset o zero_offset then functions ? ge b else None ? | _ ⇒ None ? ]) (* find_funct *)
    526526  (λF,ge. symbols ? ge) (* find_symbol *)
    527527(*  ?

  • Deliverables/D3.1/C-semantics/Mem.ma

    r500 r583  
    644644  given offset falls within the bounds of the corresponding block. *)
    645645
    646 definition valid_pointer : mem → region → block → Z → bool ≝
     646definition valid_pointer : mem → region → block → offset → bool ≝
    647647λm,r,b,ofs. Zltb (block_id b) (nextblock m) ∧
    648   Zleb (low_bound m b) ofs ∧
    649   Zltb ofs (high_bound m b) ∧
     648  Zleb (low_bound m b) (offv ofs) ∧
     649  Zltb (offv ofs) (high_bound m b) ∧
    650650  is_pointer_compat b r.
    651651
    … …  
    680680let rec loadv (chunk:memory_chunk) (m:mem) (addr:val) on addr : option val ≝
    681681  match addr with
    682   [ Vptr r b p ofs ⇒ load chunk m r b (signed ofs)
     682  [ Vptr r b p ofs ⇒ load chunk m r b (offv ofs)
    683683  | _ ⇒ None ? ].
    684684
    … …  
    727727λchunk,m,addr,v.
    728728  match addr with
    729   [ Vptr r b p ofs ⇒ store chunk m r b (signed ofs) v
     729  [ Vptr r b p ofs ⇒ store chunk m r b (offv ofs) v
    730730  | _ ⇒ None ? ].
    731731

  • Deliverables/D3.1/C-semantics/Values.ma

    r500 r583  
    6060λb,p. match pointer_compat_dec b p with [ inl _ ⇒ true | inr _ ⇒ false ].
    6161
     62record offset : Type[0] ≝ { offv : Z }.
     63
     64definition eq_offset ≝ λx,y. eqZb (offv x) (offv y).
     65definition shift_offset : offset → int → offset ≝
     66  λo,i. mk_offset (offv o + signed i).
     67definition neg_shift_offset : offset → int → offset ≝
     68  λo,i. mk_offset (offv o - signed i).
     69definition sub_offset : offset → offset → int ≝
     70  λx,y. repr (offv x - offv y).
     71definition zero_offset ≝ mk_offset OZ.
     72definition lt_offset : offset → offset → bool ≝
     73  λx,y. Zltb (offv x) (offv y).
     74
    6275(* * A value is either:
    6376- a machine integer;
    … …  
    7689  | Vfloat: float → val
    7790  | Vnull: region → val
    78   | Vptr: ∀r:region. ∀b:block. pointer_compat b r → int → val.
     91  | Vptr: ∀r:region. ∀b:block. pointer_compat b r → offset → val.
    7992
    8093definition Vzero: val ≝ Vint zero.
    … …  
    219232  [ Vint n1 ⇒ match v2 with
    220233    [ Vint n2 ⇒ Vint (add n1 n2)
    221     | Vptr r b2 p ofs2 ⇒ Vptr r b2 p (add ofs2 n1)
     234    | Vptr r b2 p ofs2 ⇒ Vptr r b2 p (shift_offset ofs2 n1)
    222235    | _ ⇒ Vundef ]
    223236  | Vptr r b1 p ofs1 ⇒ match v2 with
    224     [ Vint n2 ⇒ Vptr r b1 p (add ofs1 n2)
     237    [ Vint n2 ⇒ Vptr r b1 p (shift_offset ofs1 n2)
    225238    | _ ⇒ Vundef ]
    226239  | _ ⇒ Vundef ].
    … …  
    232245    | _ ⇒ Vundef ]
    233246  | Vptr r1 b1 p1 ofs1 ⇒ match v2 with
    234     [ Vint n2 ⇒ Vptr r1 b1 p1 (sub ofs1 n2)
     247    [ Vint n2 ⇒ Vptr r1 b1 p1 (neg_shift_offset ofs1 n2)
    235248    | Vptr r2 b2 p2 ofs2 ⇒
    236         if eq_block b1 b2 then Vint (sub ofs1 ofs2) else Vundef
     249        if eq_block b1 b2 then Vint (sub_offset ofs1 ofs2) else Vundef
    237250    | _ ⇒ Vundef ]
    238251  | Vnull r ⇒ match v2 with [ Vnull r' ⇒ Vint zero | _ ⇒ Vundef ]
    … …  
    397410  ].
    398411
    399 (* TODO: consider whether to check pointer representations *)
     412definition cmp_offset ≝
     413λc: comparison. λx,y:offset.
     414  match c with
     415  [ Ceq ⇒  eq_offset x y
     416  | Cne ⇒ ¬eq_offset x y
     417  | Clt ⇒  lt_offset x y
     418  | Cle ⇒ ¬lt_offset y x
     419  | Cgt ⇒  lt_offset y x
     420  | Cge ⇒ ¬lt_offset x y
     421  ].
     422
    400423definition cmp ≝ λc: comparison. λv1,v2: val.
    401424  match v1 with
    … …  
    406429    [ Vptr r2 b2 p2 ofs2 ⇒
    407430        if eq_block b1 b2
    408         then of_bool (cmp c ofs1 ofs2)
     431        then of_bool (cmp_offset c ofs1 ofs2)
    409432        else cmp_mismatch c
    410433    | Vnull r2 ⇒ cmp_mismatch c
    … …  
    425448    [ Vptr r2 b2 p2 ofs2 ⇒
    426449        if eq_block b1 b2
    427         then of_bool (cmpu c ofs1 ofs2)
     450        then of_bool (cmp_offset c ofs1 ofs2)
    428451        else cmp_mismatch c
    429452    | Vnull r2 ⇒ cmp_mismatch c
Note: See TracChangeset for help on using the changeset viewer.