Changeset 1875


Ignore:
Timestamp:
Apr 4, 2012, 6:48:25 PM (8 years ago)
Author:
campbell
Message:

Update brief memory model test.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/test/memorymodel.ma

    r1634 r1875  
    2020   access, preventing you reading back more information than the memory can
    2121   store. *)
    22 definition store0 := empty.
    23 definition store1block : mem × block ≝ alloc store0 0 4 Any.
     22definition store0 := empty becontentT.
     23definition store1block : mem × Σb:block.? ≝ alloc ? store0 0 4 Any.
    2424definition store1 : mem ≝ fst ?? store1block.
    25 definition block := snd ?? store1block.
     25definition block :block := pi1 … (snd ?? store1block).
    2626
    2727(* write a value *)
    2828definition store2 : mem.
    29   letin r ≝ (store Mint16unsigned store1 Any block 0 (Vint I16 (repr ? 1)));
     29  letin r ≝ (store (ASTint I16 Unsigned) store1 (mk_pointer Any block (same_compat …) 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 Mint8unsigned store1 Any block 0 (Vint I8 (repr ? 1)));
     36  letin r ≝ (store (ASTint I8 Unsigned) store2 (mk_pointer Any block (same_compat …) zero_offset) (Vint I8 (repr ? 1)));
    3737
    3838  lapply (refl ? r) elim r in ⊢ (???% → ?); [ whd in ⊢ (??%? → ?); #H destruct
    3939  | #rr #_ @ rr ] qed.
    4040 
    41 (* The size checking rejects the read and gives us Some Vundef. *)
    42 example vl_undef: load Mint16signed store3 Any block 0 = Some ? Vundef. @refl qed.
     41(* This is what happened under the original CompCert 1.6 ported memory model:
     42   The size checking rejects the read and gives us Some Vundef.
     43example vl_undef: load (ASTint I16 Signed) store3 (mk_pointer Any block (same_compat …) zero_offset) = Some ? Vundef. @refl qed.
     44*)
     45(* Now we do byte-wise values and get to see the altered integer. *)
     46example vl_changed: load (ASTint I16 Signed) store3 (mk_pointer Any block (same_compat …) zero_offset) = Some ? (Vint I16 (repr ? 257)). @refl qed.
    4347
    4448(* The read is successful and returns the value. *)
    45 example vl_ok': load Mint8unsigned store3 Any block 0 = Some ? (Vint I8 (repr ? 1)). // qed.
     49example vl_ok': load (ASTint I8 Unsigned) store3 (mk_pointer Any block (same_compat …) zero_offset) = Some ? (Vint I8 (repr ? 1)). // qed.
    4650
    4751(* NB: Double frees are allowed by the memory model (although not necessarily
    4852       by the language). *)
    49 definition store4 := free store3 block.
    50 definition store5 : mem. letin r ≝ (free store3 block); whd in r; @r qed.
     53definition store4 := free ? store3 block.
     54definition store5 : mem. letin r ≝ (free ? store3 block); whd in r; @r qed.
    5155
    5256(* No ordering is imposed on deallocation (even though alloc and free are only used for
    5357   stack memory in the semantics. *)
    54 definition storeA := empty.
    55 definition storeBblkB := alloc storeA 0 4 Any.
    56 definition storeCblkC := alloc (fst ?? storeBblkB) 0 8 Any.
    57 definition storeD := free (fst ?? storeCblkC) (snd ?? storeBblkB).
    58 definition storeE : mem. letin r ≝ (free storeD (snd ?? storeCblkC)).
     58definition storeA := empty becontentT.
     59definition storeBblkB := alloc ? storeA 0 4 Any.
     60definition storeCblkC := alloc ? (fst ?? storeBblkB) 0 8 Any.
     61definition storeD := free ? (fst ?? storeCblkC) (snd ?? storeBblkB).
     62definition storeE : mem. letin r ≝ (free ? storeD (snd ?? storeCblkC)).
    5963whd in r; @r qed.
    6064
    61 (* Access to the "object representation" (as the C standard puts it) is not specified. *)
    62 definition storeI := empty.
    63 definition storeIIblk := alloc storeA 0 4 Any.
     65(* Access to the "object representation" (as the C standard puts it) was not specified,
     66   but can now split up integer values into bytes.  The front-end interface
     67   doesn't currently expose parts of pointers. *)
     68definition storeI := empty becontentT.
     69definition storeIIblk := alloc ? storeA 0 4 Any.
    6470definition storeIII : mem.
    65  letin r ≝ (store Mint32 (fst ?? storeIIblk) Any (snd ?? storeIIblk) 0 (Vint I32 (repr ? 1)));
     71 letin r ≝ (store (ASTint I32 Unsigned) (fst ?? storeIIblk) (mk_pointer Any (snd ?? storeIIblk) (same_compat …) zero_offset) (Vint I32 (repr ? 1)));
    6672  lapply (refl ? r) elim r in ⊢ (???% → ?); [ whd in ⊢ (??%? → ?); #H destruct
    6773  | #rr #_ @rr ] qed.
    68 definition byte := load Mint8unsigned storeIII Any (snd ?? storeIIblk) 0.
    69 example byteundef: byte = Some ? Vundef. // qed. (* :( *)
     74definition byte := load (ASTint I8 Unsigned) storeIII (mk_pointer Any (snd ?? storeIIblk) (same_compat …) zero_offset).
     75example byteundef: byte = Some ? (Vint I8 (repr ? 0)). // qed. (* :) *)
Note: See TracChangeset for help on using the changeset viewer.