Changeset 2176 for src/Clight/test/memorymodel.ma
- Timestamp:
- Jul 12, 2012, 1:28:28 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/test/memorymodel.ma
r1993 r2176 21 21 store. *) 22 22 definition store0 := empty. 23 definition store1block : mem × Σb:block.? ≝ alloc store0 0 4 Any.23 definition store1block : mem × Σb:block.? ≝ alloc store0 0 4 XData. 24 24 definition store1 : mem ≝ fst ?? store1block. 25 25 definition block :block := pi1 … (snd ?? store1block). … … 27 27 (* write a value *) 28 28 definition 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))) 30 30 31 31 lapply (refl ? r); elim r in ⊢ (???% → ?); [ whd in ⊢ (??%? → ?); #H destruct … … 34 34 (* overwrite the first byte of the value *) 35 35 definition 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))) 37 37 38 38 lapply (refl ? r) elim r in ⊢ (???% → ?); [ whd in ⊢ (??%? → ?); #H destruct … … 41 41 (* This is what happened under the original CompCert 1.6 ported memory model: 42 42 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.43 example vl_undef: load (ASTint I16 Signed) store3 (mk_pointer block zero_offset) = Some ? Vundef. @refl qed. 44 44 *) 45 45 (* 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.46 example vl_changed: load (ASTint I16 Signed) store3 (mk_pointer block zero_offset) = Some ? (Vint I16 (repr ? 257)). @refl qed. 47 47 48 48 (* 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.49 example vl_ok': load (ASTint I8 Unsigned) store3 (mk_pointer block zero_offset) = Some ? (Vint I8 (repr ? 1)). // qed. 50 50 51 51 (* NB: Double frees are allowed by the memory model (although not necessarily … … 57 57 stack memory in the semantics. *) 58 58 definition storeA := empty. 59 definition storeBblkB := alloc storeA 0 4 Any.60 definition storeCblkC := alloc (fst ?? storeBblkB) 0 8 Any.59 definition storeBblkB := alloc storeA 0 4 XData. 60 definition storeCblkC := alloc (fst ?? storeBblkB) 0 8 XData. 61 61 definition storeD := free (fst ?? storeCblkC) (snd ?? storeBblkB). 62 62 definition storeE : mem. letin r ≝ (free storeD (snd ?? storeCblkC)). … … 67 67 doesn't currently expose parts of pointers. *) 68 68 definition storeI := empty. 69 definition storeIIblk := alloc storeI 0 4 Any.69 definition storeIIblk := alloc storeI 0 4 XData. 70 70 definition 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))); 72 72 lapply (refl ? r) elim r in ⊢ (???% → ?); [ whd in ⊢ (??%? → ?); #H destruct 73 73 | #rr #_ @rr ] qed. 74 definition byte := load (ASTint I8 Unsigned) storeIII (mk_pointer Any (snd ?? storeIIblk) (same_compat …) zero_offset).74 definition byte := load (ASTint I8 Unsigned) storeIII (mk_pointer (snd ?? storeIIblk) zero_offset). 75 75 example byteundef: byte = Some ? (Vint I8 (repr ? 0)). // qed. (* :) *) 76
Note: See TracChangeset
for help on using the changeset viewer.