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

Make block type a little more abstract; remove knowledge about the old
representation for a pointer from the evaluation of lvalues.

File:
1 edited

Legend:

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

    r497 r498  
    222222  mk_mem (λx.empty_block OZ OZ) (pos one) one_pos.
    223223
    224 definition nullptr: block ≝ 〈Any,OZ〉.
     224definition nullptr: block ≝ mk_block Any OZ.
    225225
    226226(* Allocation of a fresh block with the given bounds.  Return an updated
     
    237237
    238238definition alloc : mem → Z → Z → region → mem × block ≝
    239   λm,lo,hi,r.〈mk_mem
    240               (update_block … 〈r,nextblock m〉
    241                  (empty_block lo hi)
    242                  (blocks m))
    243               (Zsucc (nextblock m))
    244               (succ_nextblock_pos m),
    245             〈r,nextblock m〉〉.
     239  λm,lo,hi,r.
     240  let b ≝ mk_block r (nextblock m) in
     241  〈mk_mem
     242    (update_block … b
     243      (empty_block lo hi)
     244      (blocks m))
     245    (Zsucc (nextblock m))
     246    (succ_nextblock_pos m),
     247    b〉.
    246248
    247249(* Freeing a block.  Return the updated memory state where the given
     
    274276  λm,b.high (blocks m b).
    275277definition block_region: mem → block → region ≝
    276   λm,b.\fst b. (* TODO: should I keep the mem argument for uniformity, or get rid of it? *)
     278  λm,b.block_region b. (* TODO: should I keep the mem argument for uniformity, or get rid of it? *)
    277279
    278280(* A block address is valid if it was previously allocated. It remains valid
     
    281283(* TODO: should this check for region? *)
    282284definition valid_block : mem → block → Prop ≝
    283   λm,b.\snd b < nextblock m.
     285  λm,b.block_id b < nextblock m.
    284286
    285287(* FIXME: hacks to get around lack of nunfold *)
     
    288290lemma unfold_high_bound : ∀m,b. high_bound m b = high (blocks m b).
    289291//; qed.
    290 lemma unfold_valid_block : ∀m,b. (valid_block m b) = (\snd b < nextblock m).
     292lemma unfold_valid_block : ∀m,b. (valid_block m b) = (block_id b < nextblock m).
    291293//; qed.
    292294
     
    629631cases b #br #bi
    630632@(Zltb_elim_Type0 bi (nextblock m)) #Hnext
    631 [ @(Zleb_elim_Type0 (low_bound m 〈br,bi〉) ofs) #Hlo
    632     [ @(Zleb_elim_Type0 (ofs + size_chunk chunk) (high_bound m 〈br,bi〉)) #Hhi
     633[ @(Zleb_elim_Type0 (low_bound m (mk_block br bi)) ofs) #Hlo
     634    [ @(Zleb_elim_Type0 (ofs + size_chunk chunk) (high_bound m (mk_block br bi))) #Hhi
    633635        [ elim (dec_dividesZ (align_chunk chunk) ofs); #Hal
    634           [ cases (pointer_compat_dec (block_region m 〈br,bi〉) r); #Hcl
     636          [ cases (pointer_compat_dec (block_region m (mk_block br bi)) r); #Hcl
    635637            [ %1 % // @Hnext ]
    636638          ]
     
    657659
    658660definition valid_pointer : mem → region → block → Z → bool ≝
    659 λm,r,b,ofs. Zltb (\snd b) (nextblock m) ∧
     661λm,r,b,ofs. Zltb (block_id b) (nextblock m) ∧
    660662  Zleb (low_bound m b) ofs ∧
    661663  Zltb ofs (high_bound m b) ∧
Note: See TracChangeset for help on using the changeset viewer.