Ignore:
Timestamp:
Jul 12, 2012, 1:28:28 PM (8 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/Clight/test/memorymodel.ma

    r1993 r2176  
    2121   store. *)
    2222definition store0 := empty.
    23 definition store1block : mem × Σb:block.? ≝ alloc store0 0 4 Any.
     23definition store1block : mem × Σb:block.? ≝ alloc store0 0 4 XData.
    2424definition store1 : mem ≝ fst ?? store1block.
    2525definition block :block := pi1 … (snd ?? store1block).
     
    2727(* write a value *)
    2828definition store2 : mem.
    29   letin r ≝ (store (ASTint I16 Unsigned) store1 (mk_pointer Any block (same_compat …) zero_offset) (Vint I16 (repr ? 1)));
     29  letin r ≝ (store (ASTint I16 Unsigned) store1 (mk_pointer block zero_offset) (Vint I16 (repr ? 1)))
    3030
    3131  lapply (refl ? r); elim r in ⊢ (???% → ?); [ whd in ⊢ (??%? → ?); #H destruct
     
    3434(* overwrite the first byte of the value *)
    3535definition store3 : mem.
    36   letin r ≝ (store (ASTint I8 Unsigned) store2 (mk_pointer Any block (same_compat …) zero_offset) (Vint I8 (repr ? 1)));
     36  letin r ≝ (store (ASTint I8 Unsigned) store2 (mk_pointer block zero_offset) (Vint I8 (repr ? 1)))
    3737
    3838  lapply (refl ? r) elim r in ⊢ (???% → ?); [ whd in ⊢ (??%? → ?); #H destruct
     
    4141(* This is what happened under the original CompCert 1.6 ported memory model:
    4242   The size checking rejects the read and gives us Some Vundef.
    43 example vl_undef: load (ASTint I16 Signed) store3 (mk_pointer Any block (same_compat …) zero_offset) = Some ? Vundef. @refl qed.
     43example vl_undef: load (ASTint I16 Signed) store3 (mk_pointer block zero_offset) = Some ? Vundef. @refl qed.
    4444*)
    4545(* Now we do byte-wise values and get to see the altered integer. *)
    46 example vl_changed: load (ASTint I16 Signed) store3 (mk_pointer Any block (same_compat …) zero_offset) = Some ? (Vint I16 (repr ? 257)). @refl qed.
     46example vl_changed: load (ASTint I16 Signed) store3 (mk_pointer block zero_offset) = Some ? (Vint I16 (repr ? 257)). @refl qed.
    4747
    4848(* The read is successful and returns the value. *)
    49 example vl_ok': load (ASTint I8 Unsigned) store3 (mk_pointer Any block (same_compat …) zero_offset) = Some ? (Vint I8 (repr ? 1)). // qed.
     49example vl_ok': load (ASTint I8 Unsigned) store3 (mk_pointer block zero_offset) = Some ? (Vint I8 (repr ? 1)). // qed.
    5050
    5151(* NB: Double frees are allowed by the memory model (although not necessarily
     
    5757   stack memory in the semantics. *)
    5858definition storeA := empty.
    59 definition storeBblkB := alloc storeA 0 4 Any.
    60 definition storeCblkC := alloc (fst ?? storeBblkB) 0 8 Any.
     59definition storeBblkB := alloc storeA 0 4 XData.
     60definition storeCblkC := alloc (fst ?? storeBblkB) 0 8 XData.
    6161definition storeD := free (fst ?? storeCblkC) (snd ?? storeBblkB).
    6262definition storeE : mem. letin r ≝ (free storeD (snd ?? storeCblkC)).
     
    6767   doesn't currently expose parts of pointers. *)
    6868definition storeI := empty.
    69 definition storeIIblk := alloc storeI 0 4 Any.
     69definition storeIIblk := alloc storeI 0 4 XData.
    7070definition storeIII : mem.
    71  letin r ≝ (store (ASTint I32 Unsigned) (fst ?? storeIIblk) (mk_pointer Any (snd ?? storeIIblk) (same_compat …) zero_offset) (Vint I32 (repr ? 1)));
     71 letin r ≝ (store (ASTint I32 Unsigned) (fst ?? storeIIblk) (mk_pointer (snd ?? storeIIblk) zero_offset) (Vint I32 (repr ? 1)));
    7272  lapply (refl ? r) elim r in ⊢ (???% → ?); [ whd in ⊢ (??%? → ?); #H destruct
    7373  | #rr #_ @rr ] qed.
    74 definition byte := load (ASTint I8 Unsigned) storeIII (mk_pointer Any (snd ?? storeIIblk) (same_compat …) zero_offset).
     74definition byte := load (ASTint I8 Unsigned) storeIII (mk_pointer (snd ?? storeIIblk) zero_offset).
    7575example byteundef: byte = Some ? (Vint I8 (repr ? 0)). // qed. (* :) *)
     76
Note: See TracChangeset for help on using the changeset viewer.