Ignore:
Timestamp:
Feb 11, 2011, 4:45:28 PM (9 years ago)
Author:
campbell
Message:

First pass at moving regions to block type.

File:
1 edited

Legend:

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

    r487 r496  
    6666       a value, which must be a pointer with offset 0. *)
    6767
    68   find_symbol: ∀F: Type[0]. genv_t F → ident → option (region × block)(*;
     68  find_symbol: ∀F: Type[0]. genv_t F → ident → option 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 (region × block)
     319  symbols: ident → option block
    320320}.
    321321(*
     
    342342λF,name_fun,g.
    343343  let b ≝ nextfunction ? g in
    344   mk_genv F ((*ZMap.set*) λb'. if eqZb b b' then (Some ? (\snd name_fun)) else (functions ? g b'))
     344  mk_genv F ((*ZMap.set*) λb'. if eq_block 〈Code,b〉 b' then (Some ? (\snd name_fun)) else (functions ? g b'))
    345345            (Zpred b)
    346346            ((*PTree.set*) λi. match ident_eq (\fst name_fun) i with [ inl _ ⇒ Some ? 〈Code,b〉 | inr _ ⇒ (symbols ? g i) ]).
    347347
    348 definition add_symbol : ∀F:Type[0]. ident → region → block → genv F → genv F ≝
    349 λF,name,bsp,b,g.
     348definition add_symbol : ∀F:Type[0]. ident → block → genv F → genv F ≝
     349λF,name,b,g.
    350350  mk_genv F (functions ? g)
    351351            (nextfunction ? g)
    352             ((*PTree.set*) λi. match ident_eq name i with [ inl _ ⇒ Some ? 〈bsp,b〉 | inr _ ⇒ symbols ? g i ]).
     352            ((*PTree.set*) λi. match ident_eq name i with [ inl _ ⇒ Some ? b | inr _ ⇒ symbols ? g i ]).
    353353(*
    354354Definition find_funct_ptr ? (g: genv) (b: block) : option F :=
     
    398398(* init *)
    399399
    400 definition store_init_data : ∀F.genv F → mem → region → block → Z → init_data → option mem ≝
    401 λF,ge,m,r,b,p,id.
     400definition store_init_data : ∀F.genv F → mem → block → Z → init_data → option mem ≝
     401λF,ge,m,b,p,id.
     402  (* store checks that the address came from something capable of representing
     403     addresses of the memory region in question - here there are no real
     404     pointers, so use the real region. *)
     405  let r ≝ \fst b in
    402406  match id with
    403407  [ Init_int8 n ⇒ store Mint8unsigned m r b p (Vint n)
     
    409413      match (*find_symbol ge symb*) symbols ? ge symb with
    410414      [ None ⇒ None ?
    411       | Some b' ⇒ store (Mpointer r') m r b p (Vptr r' (snd ?? b') ofs)
     415      | Some b' ⇒ store (Mpointer r') m r b p (Vptr r' b' ofs)
    412416      ]
    413417  | Init_space n ⇒ Some ? m
     
    427431
    428432let rec store_init_data_list (F:Type[0]) (ge:genv F)
    429                               (m: mem) (r: region) (b: block) (p: Z) (idl: list init_data)
     433                              (m: mem) (b: block) (p: Z) (idl: list init_data)
    430434                              on idl : option mem ≝
    431435  match idl with
    432436  [ nil ⇒ Some ? m
    433437  | cons id idl' ⇒
    434       match store_init_data F ge m r b p id with
     438      match store_init_data F ge m b p id with
    435439      [ None ⇒ None ?
    436       | Some m' ⇒ store_init_data_list F ge m' r b (p + size_init_data id) idl'
     440      | Some m' ⇒ store_init_data_list F ge m' b (p + size_init_data id) idl'
    437441      ]
    438442  ].
     
    463467
    464468definition alloc_init_data : mem → list init_data → region → mem × block ≝
    465   λm,i_data,bcl.
    466   〈mk_mem (update ? (nextblock m)
    467                  (mk_block_contents OZ (size_init_data_list i_data) (λ_.Undef) bcl)
     469  λm,i_data,r.
     470  〈mk_mem (update_block ? 〈r, nextblock m〉
     471                 (mk_block_contents OZ (size_init_data_list i_data) (λ_.Undef))
    468472                 (blocks m))
    469473         (Zsucc (nextblock m))
    470474         (succ_nextblock_pos m),
    471    (nextblock m)〉.
     475   〈r, nextblock m〉〉.
    472476
    473477(* init *)
     
    484488        do 〈g,st〉 ← g_st;
    485489        match alloc_init_data st init r with [ pair st' b ⇒
    486           let g' ≝ add_symbol ? id r b g in
    487           do st'' ← opt_to_res ? (store_init_data_list F g' st' r b OZ init);
     490          let g' ≝ add_symbol ? id b g in
     491          do st'' ← opt_to_res ? (store_init_data_list F g' st' b OZ init);
    488492            OK ? 〈g', st''〉
    489493        ] ] ] ])
Note: See TracChangeset for help on using the changeset viewer.