source: src/common/FrontEndMem.ma @ 1993

Last change on this file since 1993 was 1993, checked in by campbell, 7 years ago

Make front-end memory model only depend on the general definitions by
moving a few definitions from the back-end one. Give the front-end
model a more descriptive name.

File size: 1.6 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(* Only used by Clight semantics for pointer comparisons.  So in contrast to
49   CompCert, we allow a pointer-to-one-off-the-end. *)
50
51definition valid_pointer : mem → pointer → bool ≝
52λm,ptr. Zltb (block_id (pblock ptr)) (nextblock m) ∧
53  Zleb (low_bound m (pblock ptr)) (offv (poff ptr)) ∧
54  Zleb (offv (poff ptr)) (high_bound m (pblock ptr)).
55
Note: See TracBrowser for help on using the repository browser.