Changeset 480


Ignore:
Timestamp:
Jan 25, 2011, 5:30:37 PM (6 years ago)
Author:
campbell
Message:

"memory_space" to "region" replacement to match ocaml code

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

Legend:

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

    r478 r480  
    107107(* Memory spaces *)
    108108
    109 ninductive memory_space : Type ≝
    110   | Any : memory_space
    111   | Data : memory_space
    112   | IData : memory_space
    113   | PData : memory_space
    114   | XData : memory_space
    115   | Code : memory_space.
     109ninductive region : Type ≝
     110  | Any : region
     111  | Data : region
     112  | IData : region
     113  | PData : region
     114  | XData : region
     115  | Code : region.
    116116
    117117(* * Initialization data for global variables. *)
     
    142142  prog_funct: list (ident × F);
    143143  prog_main: ident;
    144   prog_vars: list (ident × (list init_data) × memory_space × V)
     144  prog_vars: list (ident × (list init_data) × region × V)
    145145}.
    146146
     
    149149
    150150ndefinition prog_var_names ≝ λF,V: Type. λp: program F V.
    151   map ?? (λx: ident × (list init_data) × memory_space × V. fst ?? (fst ?? (fst ?? x))) (prog_vars ?? p).
     151  map ?? (λx: ident × (list init_data) × region × V. fst ?? (fst ?? (fst ?? x))) (prog_vars ?? p).
    152152(*
    153153(** * Generic transformations over programs *)
  • Deliverables/D3.1/C-semantics/Cexec.ma

    r478 r480  
    162162].
    163163
    164 ndefinition ms_eq_dec : ∀s1,s2:memory_space. (s1 = s2) + (s1 ≠ s2).
     164ndefinition ms_eq_dec : ∀s1,s2:region. (s1 = s2) + (s1 ≠ s2).
    165165#s1; ncases s1; #s2; ncases s2; /2/; @2; @; #H; ndestruct; nqed.
    166166
     
    277277  ]
    278278]
    279 and exec_lvalue' (ge:genv) (en:env) (m:mem) (e':expr_descr) (ty:type) on e' : res (memory_space × block × int × trace) ≝
     279and exec_lvalue' (ge:genv) (en:env) (m:mem) (e':expr_descr) (ty:type) on e' : res (region × block × int × trace) ≝
    280280  match e' with
    281281  [ Evar id ⇒
     
    303303  | _ ⇒ Error ?
    304304  ]
    305 and exec_lvalue (ge:genv) (en:env) (m:mem) (e:expr) on e : res (memory_space × block × int × trace) ≝
     305and exec_lvalue (ge:genv) (en:env) (m:mem) (e:expr) on e : res (region × block × int × trace) ≝
    306306match e with [ Expr e' ty ⇒ exec_lvalue' ge en m e' ty ].
    307307
  • Deliverables/D3.1/C-semantics/Csem.ma

    r478 r480  
    406406| type_ptr_function : ∀tys,ty. type_pointable (Tfunction tys ty).
    407407
    408 ninductive type_space : type → memory_space → Prop ≝
     408ninductive type_space : type → region → Prop ≝
    409409| type_spc_pointer : ∀s,t. type_space (Tpointer s t) s
    410410| type_spc_array : ∀s,t,n. type_space (Tarray s t n) s
     
    470470  reference, the pointer [Vptr b ofs] is returned. *)
    471471
    472 nlet rec load_value_of_type (ty: type) (m: mem) (psp:memory_space) (b: block) (ofs: int) : option val ≝
     472nlet rec load_value_of_type (ty: type) (m: mem) (psp:region) (b: block) (ofs: int) : option val ≝
    473473  match access_mode ty with
    474474  [ By_value chunk ⇒ loadv chunk m (Vptr psp b ofs)
     
    482482  This is allowed only if [ty] indicates an access by value. *)
    483483
    484 nlet rec store_value_of_type (ty_dest: type) (m: mem) (psp:memory_space) (loc: block) (ofs: int) (v: val) : option mem ≝
     484nlet rec store_value_of_type (ty_dest: type) (m: mem) (psp:region) (loc: block) (ofs: int) (v: val) : option mem ≝
    485485  match access_mode ty_dest with
    486486  [ By_value chunk ⇒ storev chunk m (Vptr psp loc ofs) v
     
    633633  that contains the value of the expression [a]. *)
    634634
    635 with eval_lvalue (*(ge:genv) (e:env) (m:mem)*) : expr → memory_space → block → int → trace → Prop ≝
     635with eval_lvalue (*(ge:genv) (e:env) (m:mem)*) : expr → region → block → int → trace → Prop ≝
    636636  | eval_Evar_local:   ∀id,l,ty.
    637637      (* XXX notation? e!id*) get ??? id e = Some ? l →
     
    699699  (lfs:∀a,i,ty,psp,l,ofs,id,fList,delta,tr,H1,H2,H3. P a psp l ofs tr H1 → P ????? (eval_Efield_struct ge e m a i ty psp l ofs id fList delta tr H1 H2 H3))
    700700  (lfu:∀a,i,ty,psp,l,ofs,id,fList,tr,H1,H2. P a psp l ofs tr H1 → P ????? (eval_Efield_union ge e m a i ty psp l ofs id fList tr H1 H2))
    701   (a:expr) (psp:memory_space) (loc:block) (ofs:int) (tr:trace) (ev:eval_lvalue ge e m a psp loc ofs tr) on ev : P a psp loc ofs tr ev ≝
     701  (a:expr) (psp:region) (loc:block) (ofs:int) (tr:trace) (ev:eval_lvalue ge e m a psp loc ofs tr) on ev : P a psp loc ofs tr ev ≝
    702702  match ev with
    703703  [ eval_Evar_local id l ty H ⇒ lvl id l ty H
     
    717717    ∀x3: mem.
    718718     ∀x4: expr.
    719       ∀x5: memory_space.
     719      ∀x5: region.
    720720       ∀x6: block.
    721721        ∀x7: int.
     
    723723          ∀P:
    724724            ∀_z1430: expr.
    725              ∀_z1429: memory_space.
     725             ∀_z1429: region.
    726726              ∀_z1428: block. ∀_z1427: int. ∀_z1426: trace. Prop.
    727727           ∀_H1: ?.
     
    737737      (λx3:mem.
    738738        (λx4:expr.
    739           (λx5:memory_space.
     739          (λx5:region.
    740740            (λx6:block.
    741741              (λx7:int.
    742742                (λx8:trace.
    743743                  (λP:∀_z1430: expr.
    744                         ∀_z1429: memory_space.
     744                        ∀_z1429: region.
    745745                         ∀_z1428: block.
    746746                          ∀_z1427: int. ∀_z1426: trace. Prop.
     
    752752                              (λHterm:eval_lvalue x1 x2 x3 x4 x5 x6 x7 x8.
    753753                                ((λHcut:∀z1435: eq expr x4 x4.
    754                                           ∀z1434: eq memory_space x5 x5.
     754                                          ∀z1434: eq region x5 x5.
    755755                                           ∀z1433: eq block x6 x6.
    756756                                            ∀z1432: eq int x7 x7.
     
    758758                                              P x4 x5 x6 x7 x8.
    759759                                   (Hcut (refl expr x4)
    760                                      (refl memory_space x5) (refl block x6)
     760                                     (refl region x5) (refl block x6)
    761761                                     (refl int x7) (refl trace x8)))
    762762                                  ?)))))))))))))))).
     
    831831  (lfs:∀a,i,ty,psp,l,ofs,id,fList,delta,tr,H1,H2,H3. Q a psp l ofs tr H1 → Q ????? (eval_Efield_struct ge e m a i ty psp l ofs id fList delta tr H1 H2 H3))
    832832  (lfu:∀a,i,ty,psp,l,ofs,id,fList,tr,H1,H2. Q a psp l ofs tr H1 → Q ????? (eval_Efield_union ge e m a i ty psp l ofs id fList tr H1 H2))
    833   (a:expr) (psp:memory_space) (loc:block) (ofs:int) (tr:trace) (ev:eval_lvalue ge e m a psp loc ofs tr) on ev : Q a psp loc ofs tr ev ≝
     833  (a:expr) (psp:region) (loc:block) (ofs:int) (tr:trace) (ev:eval_lvalue ge e m a psp loc ofs tr) on ev : Q a psp loc ofs tr ev ≝
    834834  match ev with
    835835  [ eval_Evar_local id l ty H ⇒ lvl id l ty H
     
    886886  | Kswitch: cont -> cont
    887887       (**r catches [break] statements arising out of [switch] *)
    888   | Kcall: option (memory_space × block × int × type) ->   (**r where to store result *)
     888  | Kcall: option (region × block × int × type) ->   (**r where to store result *)
    889889           function ->                      (**r calling function *)
    890890           env ->                           (**r local env of calling function *)
  • Deliverables/D3.1/C-semantics/Csyntax.ma

    r478 r480  
    8787  | Tint: intsize → signedness → type   (**r integer types *)
    8888  | Tfloat: floatsize → type            (**r floating-point types *)
    89   | Tpointer: memory_space → type → type   (**r pointer types ([*ty]) *)
    90   | Tarray: memory_space → type → Z → type (**r array types ([ty[len]]) *)
     89  | Tpointer: region → type → type      (**r pointer types ([*ty]) *)
     90  | Tarray: region → type → Z → type    (**r array types ([ty[len]]) *)
    9191  | Tfunction: typelist → type → type   (**r function types *)
    9292  | Tstruct: ident → fieldlist → type   (**r struct types *)
     
    447447(* * Size of a type, in bytes. *)
    448448
    449 ndefinition sizeof_pointer : memory_space → Z ≝
     449ndefinition sizeof_pointer : region → Z ≝
    450450λsp. match sp with [ Data ⇒ 1 | IData ⇒ 1 | PData ⇒ 1 | XData ⇒ 2 | Code ⇒ 2 | Any ⇒ 3 ].
    451451
  • Deliverables/D3.1/C-semantics/Globalenvs.ma

    r474 r480  
    6666       a value, which must be a pointer with offset 0. *)
    6767
    68   find_symbol: ∀F: Type. genv_t F → ident → option (memory_space × block)(*;
     68  find_symbol: ∀F: Type. genv_t F → ident → option (region × block)(*;
    6969   (* * Return the address of the given global symbol, if any. *)
    7070
     
    317317  functions: block → option F;
    318318  nextfunction: Z;
    319   symbols: ident → option (memory_space × block)
     319  symbols: ident → option (region × block)
    320320}.
    321321(*
     
    346346            ((*PTree.set*) λi. match ident_eq (\fst name_fun) i with [ inl _ ⇒ Some ? 〈Code,b〉 | inr _ ⇒ (symbols ? g i) ]).
    347347
    348 ndefinition add_symbol : ∀F:Type. ident → memory_space → block → genv F → genv F ≝
     348ndefinition add_symbol : ∀F:Type. ident → region → block → genv F → genv F ≝
    349349λF,name,bsp,b,g.
    350350  mk_genv F (functions ? g)
     
    397397
    398398ndefinition add_globals : ∀F,V:Type.
    399        genv F × mem → list (ident × (list init_data) × memory_space × V) →
     399       genv F × mem → list (ident × (list init_data) × region × V) →
    400400       genv F × mem ≝
    401401λF,V,init,vars.
    402402  foldr ??
    403     (λid_init: ident × (list init_data) × memory_space × V. λg_st: genv F × mem.
     403    (λid_init: ident × (list init_data) × region × V. λg_st: genv F × mem.
    404404      match id_init with [ mk_pair id_init1 info ⇒
    405405      match id_init1 with [ mk_pair id_init2 bsp ⇒
  • Deliverables/D3.1/C-semantics/Mem.ma

    r474 r480  
    8989  high: Z;
    9090  contents: contentmap;
    91   space: memory_space
     91  space: region
    9292}.
    9393
     
    188188nqed.
    189189
    190 ndefinition empty_block : Z → Z → memory_space → block_contents ≝
     190ndefinition empty_block : Z → Z → region → block_contents ≝
    191191  λlo,hi,bty.mk_block_contents lo hi (λy. Undef) bty.
    192192
     
    208208nqed.
    209209
    210 ndefinition alloc : mem → Z → Z → memory_space → mem × block ≝
     210ndefinition alloc : mem → Z → Z → region → mem × block ≝
    211211  λm,lo,hi,bty.〈mk_mem
    212212              (update … (nextblock m)
     
    245245ndefinition high_bound : mem → block → Z ≝
    246246  λm,b.high (blocks m b).
    247 ndefinition block_space: mem → block → memory_space
     247ndefinition block_space: mem → block → region
    248248  λm,b.space (blocks m b).
    249249
     
    559559(* pointer_compat block_space pointer_space *)
    560560
    561 ninductive pointer_compat : memory_space → memory_space → Prop ≝
     561ninductive pointer_compat : region → region → Prop ≝
    562562|  same_compat : ∀s. pointer_compat s s
    563563| pxdata_compat : pointer_compat PData XData
     
    571571##] nqed.
    572572
    573 ndefinition is_pointer_compat : memory_space → memory_space → bool ≝
     573ndefinition is_pointer_compat : region → region → bool ≝
    574574λb,p. match pointer_compat_dec b p with [ inl _ ⇒ true | inr _ ⇒ false ].
    575575
     
    583583*)
    584584
    585 ninductive valid_access (m: mem) (chunk: memory_chunk) (psp: memory_space) (b: block) (ofs: Z)
     585ninductive valid_access (m: mem) (chunk: memory_chunk) (psp: region) (b: block) (ofs: Z)
    586586            : Prop ≝
    587587  | valid_access_intro:
     
    598598(* XXX: Using + and ¬ instead of Sum and Not causes trouble *)
    599599nlet rec in_bounds
    600   (m:mem) (chunk:memory_chunk) (psp:memory_space) (b:block) (ofs:Z) on b : 
     600  (m:mem) (chunk:memory_chunk) (psp:region) (b:block) (ofs:Z) on b : 
    601601    Sum (valid_access m chunk psp b ofs) (Not (valid_access m chunk psp b ofs)) ≝ ?.
    602602napply (Zltb_elim_Type0 b (nextblock m)); #Hnext;
     
    627627  given offset falls within the bounds of the corresponding block. *)
    628628
    629 ndefinition valid_pointer : mem → memory_space → block → Z → bool ≝
     629ndefinition valid_pointer : mem → region → block → Z → bool ≝
    630630λm,psp,b,ofs. Zltb b (nextblock m) ∧
    631631  Zleb (low_bound m b) ofs ∧
     
    637637  or the memory access is out of bounds. *)
    638638
    639 ndefinition load : memory_chunk → mem → memory_space → block → Z → option val ≝
     639ndefinition load : memory_chunk → mem → region → block → Z → option val ≝
    640640λchunk,m,psp,b,ofs.
    641641  match in_bounds m chunk psp b ofs with
     
    684684  or the memory access is out of bounds. *)
    685685
    686 ndefinition store : memory_chunk → mem → memory_space → block → Z → val → option mem ≝
     686ndefinition store : memory_chunk → mem → region → block → Z → val → option mem ≝
    687687λchunk,m,psp,b,ofs,v.
    688688  match in_bounds m chunk psp b ofs with
     
    780780*)
    781781
    782 ndefinition block_init_data : list init_data → memory_space → block_contents ≝
     782ndefinition block_init_data : list init_data → region → block_contents ≝
    783783  λi_data,bcl.mk_block_contents
    784784    OZ (size_init_data_list i_data) (contents_init_data OZ i_data) bcl.
    785785
    786 ndefinition alloc_init_data : mem → list init_data → memory_space → mem × block ≝
     786ndefinition alloc_init_data : mem → list init_data → region → mem × block ≝
    787787  λm,i_data,bcl.
    788788  〈mk_mem (update ? (nextblock m)
     
    902902nqed.
    903903
    904 nlemma memory_space_store:
     904nlemma region_store:
    905905  ∀chunk,m1,psp,b,ofs,v,m2.store chunk m1 psp b ofs v = Some ? m2 →
    906906  ∀b'. block_space m2 b' = block_space m1 b'.
     
    944944##|nrewrite > (low_bound_store … STORE …);//
    945945##|nrewrite > (high_bound_store … STORE …);//
    946 ##|nrewrite > (memory_space_store … STORE …);//]
     946##|nrewrite > (region_store … STORE …);//]
    947947nqed.
    948948
     
    959959##|nrewrite < (low_bound_store … STORE …);//
    960960##|nrewrite < (high_bound_store … STORE …);//
    961 ##|nrewrite < (memory_space_store … STORE …);//]
     961##|nrewrite < (region_store … STORE …);//]
    962962nqed.
    963963
     
    11991199   ##[#H1;#H2;#H3;nwhd in ⊢ (???%);nrewrite < H1;nrewrite < H2;
    12001200      napply (load_compat_pointer … psp);
    1201       ##[ nrewrite > (memory_space_store … STORE b);
     1201      ##[ nrewrite > (region_store … STORE b);
    12021202          ncases Hvalid; //;
    12031203      ##| napply (load_store_similar … STORE);//;
     
    12101210      ##|#H2;@2;//]
    12111211   ##|#H1;#H2;#H3;#H4; nlapply (load_compat_pointer … psp … Hx);
    1212      ##[ nrewrite > (memory_space_store … STORE b');
     1212     ##[ nrewrite > (region_store … STORE b');
    12131213         nrewrite > H1; nelim (store_valid_access_3 … STORE); //
    12141214     ##| nrewrite < H1 in ⊢ (% → ?);#Hx';
     
    12181218   ##|#H1;#H2;#H3;
    12191219       nlapply (load_compat_pointer … psp … Hx);
    1220        ##[ nrewrite > (memory_space_store … STORE b');
     1220       ##[ nrewrite > (region_store … STORE b');
    12211221           nrewrite > H1; nelim (store_valid_access_3 … STORE); //
    12221222       ##| nrewrite < H1 in Hx ⊢ %; nrewrite < H2; #Hx Hx';
     
    17361736ntheorem valid_pointer_store:
    17371737  ∀chunk: memory_chunk. ∀m1,m2: mem.
    1738   ∀psp,psp': memory_space. ∀b,b': block. ∀ofs,ofs': Z. ∀v: val.
     1738  ∀psp,psp': region. ∀b,b': block. ∀ofs,ofs': Z. ∀v: val.
    17391739  store chunk m1 psp' b' ofs' v = Some ? m2 →
    17401740  valid_pointer m1 psp b ofs = true → valid_pointer m2 psp b ofs = true.
  • Deliverables/D3.1/C-semantics/Values.ma

    r478 r480  
    4343  | Vint: int -> val
    4444  | Vfloat: float -> val
    45   | Vptr: memory_space → block -> int -> val.
     45  | Vptr: region → block -> int -> val.
    4646
    4747ndefinition Vzero: val ≝ Vint zero.
Note: See TracChangeset for help on using the changeset viewer.