Ignore:
Timestamp:
Jul 12, 2012, 1:28:28 PM (6 years ago)
Author:
campbell
Message:

Remove memory spaces other than XData and Code; simplify pointers as a
result.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Pointers.ma

    r1882 r2176  
    4343qed.
    4444
     45(* This is only required for full 8051 memory spaces.
     46
    4547(* Characterise the memory regions which the pointer representations can
    4648   address.
     
    6163definition is_pointer_compat : block → region → bool ≝
    6264λb,p. match pointer_compat_dec b p with [ inl _ ⇒ true | inr _ ⇒ false ].
     65*)
    6366
    6467(* Offsets into the block.  We allow integers like CompCert so that we have
     
    9194(*CSC: use this definition everywhere in Values.ma and Mem.ma. *)
    9295record pointer: Type[0] ≝ {
    93    ptype: region;
     96(*   ptype: region;*)
    9497   pblock: block;
    95    pok: pointer_compat pblock ptype;
     98(*   pok: pointer_compat pblock ptype;*)
    9699   poff: offset
    97100 }.
    98101
     102(* As we don't have full memory space support, grab the region from the block
     103   instead. *)
     104definition ptype : pointer → region ≝ λp. block_region (pblock p).
     105
    99106definition shift_pointer: ∀n. pointer → BitVector n → pointer ≝
    100  λn,p,i. mk_pointer (ptype p) (pblock p) (pok p) (shift_offset n (poff p) i).
     107 λn,p,i. mk_pointer (*ptype p*) (pblock p) (*pok p*) (shift_offset n (poff p) i).
    101108
    102109(* multiply shift by a nat (i.e., sizeof) without danger of overflow *)
    103110definition shift_pointer_n: ∀n. pointer → nat → BitVector n → pointer ≝
    104  λn,p,i,j. mk_pointer (ptype p) (pblock p) (pok p) (shift_offset_n n (poff p) i j).
     111 λn,p,i,j. mk_pointer (*ptype p*) (pblock p) (*pok p*) (shift_offset_n n (poff p) i j).
    105112
    106113definition neg_shift_pointer: ∀n. pointer → BitVector n → pointer ≝
    107  λn,p,i. mk_pointer (ptype p) (pblock p) (pok p) (neg_shift_offset n (poff p) i).
     114 λn,p,i. mk_pointer (*ptype p*) (pblock p) (*pok p*) (neg_shift_offset n (poff p) i).
    108115
    109116definition neg_shift_pointer_n: ∀n. pointer → nat → BitVector n → pointer ≝
    110  λn,p,i,j. mk_pointer (ptype p) (pblock p) (pok p) (neg_shift_offset_n n (poff p) i j).
     117 λn,p,i,j. mk_pointer (*ptype p*) (pblock p) (*pok p*) (neg_shift_offset_n n (poff p) i j).
    111118
    112119definition eq_pointer: pointer → pointer → bool ≝
    113120 λp1,p2.
    114   eq_region (ptype p1) (ptype p2) ∧ (eq_block (pblock p1) (pblock p2)) ∧
     121  (*eq_region (ptype p1) (ptype p2) ∧*) (eq_block (pblock p1) (pblock p2)) ∧
    115122   eq_offset (poff p1) (poff p2).
    116123
     
    121128lemma eq_pointer_elim : ∀P : bool → Prop.∀p0,p1.
    122129  (p0 = p1 → P true) → (p0 ≠ p1 → P false) → P (eq_pointer p0 p1).
    123 #P * #r0 #b0 #H0 * #o0 * #r1 #b1 #H1 * #o1
     130#P * #b0 * #o0 * #b1 * #o1
    124131#Ptrue #Pfalse
    125132whd in match (eq_pointer ??);
    126 @eq_region_elim #reg_eq
    127 [ @eq_block_elim #block_eq
    128   [ change with (eqZb ??) in match (eq_offset ??);
    129     @eqZb_elim #offset_eq
    130     [ destruct @Ptrue %
    131     ]
     133@eq_block_elim #block_eq
     134[ change with (eqZb ??) in match (eq_offset ??);
     135  @eqZb_elim #offset_eq
     136  [ destruct @Ptrue %
    132137  ]
    133138]
Note: See TracChangeset for help on using the changeset viewer.