source: src/common/FrontEndMem.ma @ 2548

Last change on this file since 2548 was 2429, checked in by garnier, 7 years ago

Restrict semantics of pointer comparison to what CompCert? does - i.e. no more pointer one of the end of a block.

File size: 2.0 KB
Line 
1include "common/GenMem.ma".
2include "common/FrontEndVal.ma".
3
4let rec loadn (m:mem) (ptr:pointer) (n:nat) on n : option (list beval) ≝
5match n with
6[ O ⇒ Some ? ([ ])
7| S n' ⇒
8  match beloadv m ptr with
9  [ None ⇒ None ?
10  | Some v ⇒ match loadn m (shift_pointer 2 ptr (bitvector_of_nat … 1)) n' with
11             [ None ⇒ None ?
12             | Some vs ⇒ Some ? (v::vs) ]
13  ]
14].
15
16definition load : typ → mem → pointer → option val ≝
17λt,m,ptr.
18  match loadn m ptr (typesize t) with
19  [ None ⇒ None ?
20  | Some vs ⇒ Some ? (be_to_fe_value t vs)
21  ].
22
23let rec loadv (t:typ) (m:mem) (addr:val) on addr : option val ≝
24match addr with
25[ Vptr ptr ⇒ load t m ptr
26| _ ⇒ None ?
27].
28
29let rec storen (m:mem) (ptr:pointer) (vs:list beval) on vs : option mem ≝
30match vs with
31[ nil ⇒ Some ? m
32| cons v tl ⇒
33  match bestorev m ptr v with
34  [ None ⇒ None ?
35  | Some m' ⇒ storen m' (shift_pointer 2 ptr (bitvector_of_nat … 1)) tl
36  ]
37].
38
39definition store : typ → mem → pointer → val → option mem ≝
40λt,m,ptr,v. storen m ptr (fe_to_be_values t v).
41
42definition storev : typ → mem → val → val → option mem ≝
43λt,m,addr,v.
44  match addr with
45  [ Vptr ptr ⇒ store t m ptr v
46  | _ ⇒ None ? ].
47
48(* A pointer that can be dereferenced.  Only used for front-end pointer
49   comparison at present. *)
50
51definition valid_pointer : mem → pointer → bool ≝
52λm,ptr.
53  let off ≝ Z_of_unsigned_bitvector … (offv (poff ptr)) in
54  Zltb (block_id (pblock ptr)) (nextblock m) ∧
55  Zleb (low_bound m (pblock ptr)) off ∧
56  Zltb off (high_bound m (pblock ptr)).
57
58(* In contrast to CompCert, we also allow a pointer-to-one-off-the-end.  This is
59   not entirely straightforward, as comparisons of an off-the-end pointer with a
60   pointer from another block cannot be defined; if we did then we might change
61   the result when coalescing blocks. *)
62
63(* Reverting to CompCert restriction.
64definition end_pointer : mem → pointer → bool ≝
65λm,ptr.
66  let off ≝ Z_of_unsigned_bitvector … (offv (poff ptr)) in
67  eqZb off (high_bound m (pblock ptr)).
68*)
69
Note: See TracBrowser for help on using the repository browser.