Changeset 499


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

pointer_compat is a little more natural if it takes that block rather than
the block's region.

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

Legend:

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

    r498 r499  
    170170         [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code
    171171         | _ ⇒ Error ? ];
    172     if is_pointer_compat (block_region m b) s'
     172    if is_pointer_compat b s'
    173173    then OK ? (Vptr s' b ofs)
    174174    else Error ?
  • Deliverables/D3.1/C-semantics/CexecComplete.ma

    r498 r499  
    3939] qed.
    4040
    41 lemma is_pointer_compat_true: ∀m,b,sp.
    42   pointer_compat (block_region m b) sp →
    43   is_pointer_compat (block_region m b) sp = true.
    44 #m #b #sp #H whd in ⊢ (??%?);
    45 elim (pointer_compat_dec (block_region m b) sp);
     41lemma is_pointer_compat_true: ∀b,sp.
     42  pointer_compat b sp →
     43  is_pointer_compat b sp = true.
     44#b #sp #H whd in ⊢ (??%?);
     45elim (pointer_compat_dec b sp);
    4646[ //
    4747| #H' @False_ind @(absurd … H H')
  • Deliverables/D3.1/C-semantics/CexecSound.ma

    r498 r499  
    102102            #e <e
    103103            whd in match (is_pointer_compat ??) in e''';
    104             cases (pointer_compat_dec (block_region m b) s') in e'''; #Hcompat #e'''
     104            cases (pointer_compat_dec b s') in e'''; #Hcompat #e'''
    105105            whd in e''':(??%?); destruct (e'''); /2/
    106106        ]
  • Deliverables/D3.1/C-semantics/Csem.ma

    r498 r499  
    432432      type_region ty r →
    433433      type_region ty' r' →
    434       pointer_compat (block_region m b) r' →
     434      pointer_compat b r' →
    435435      cast m (Vptr r b ofs) ty ty' (Vptr r' b ofs)
    436436  | cast_ip_z: ∀m,sz,sg,ty',r.
  • Deliverables/D3.1/C-semantics/Mem.ma

    r498 r499  
    590590(* pointer_compat block_region pointer_region *)
    591591
    592 inductive pointer_compat : region → region → Prop ≝
    593 |        same_compat : ∀s. pointer_compat s s
    594 |      pxdata_compat : pointer_compat PData XData
    595 |   universal_compat : ∀b. pointer_compat b Any.
     592inductive pointer_compat : block → region → Prop ≝
     593|        same_compat : ∀s,id. pointer_compat (mk_block s id) s
     594|      pxdata_compat : ∀id. pointer_compat (mk_block PData id) XData
     595|   universal_compat : ∀r,id. pointer_compat (mk_block r id) Any.
    596596
    597597lemma pointer_compat_dec : ∀b,p. pointer_compat b p + ¬pointer_compat b p.
    598 #b #p cases b
    599 cases p /2/ %2 % #H inversion H #e1 #e2 destruct #e3 destruct
    600 qed.
    601 
    602 definition is_pointer_compat : region → region → bool ≝
     598* * #id *
     599try ( %1 // )
     600%2 % #H inversion H #e1 #e2 try #e3 try #e4 destruct
     601qed.
     602
     603definition is_pointer_compat : block → region → bool ≝
    603604λb,p. match pointer_compat_dec b p with [ inl _ ⇒ true | inr _ ⇒ false ].
    604605
     
    619620      ofs + size_chunk chunk ≤ high_bound m b →
    620621      (align_chunk chunk ∣ ofs) →
    621       pointer_compat (block_region m b) r →
     622      pointer_compat b r →
    622623      valid_access m chunk r b ofs.
    623624
     
    634635    [ @(Zleb_elim_Type0 (ofs + size_chunk chunk) (high_bound m (mk_block br bi))) #Hhi
    635636        [ elim (dec_dividesZ (align_chunk chunk) ofs); #Hal
    636           [ cases (pointer_compat_dec (block_region m (mk_block br bi)) r); #Hcl
     637          [ cases (pointer_compat_dec (mk_block br bi) r); #Hcl
    637638            [ %1 % // @Hnext ]
    638639          ]
     
    662663  Zleb (low_bound m b) ofs ∧
    663664  Zltb ofs (high_bound m b) ∧
    664   is_pointer_compat (block_region m b) r.
     665  is_pointer_compat b r.
    665666
    666667(* [load chunk m r b ofs] perform a read in memory state [m], at address
     
    885886|>(low_bound_store … STORE …) //
    886887|>(high_bound_store … STORE …) //
    887 |>(region_store … STORE …) //]
    888 qed.
     888] qed.
    889889
    890890lemma store_valid_access_2:
     
    900900|<(low_bound_store … STORE …) //
    901901|<(high_bound_store … STORE …) //
    902 |<(region_store … STORE …) //]
    903 qed.
     902] qed.
    904903
    905904lemma store_valid_access_3:
     
    915914lemma load_compat_pointer:
    916915  ∀chunk,m,r,r',b,ofs,v.
    917   pointer_compat (block_region m b) r' →
     916  pointer_compat b r' →
    918917  load chunk m r b ofs = Some ? v →
    919918  load chunk m r' b ofs = Some ? v.
Note: See TracChangeset for help on using the changeset viewer.