source: src/joint/BEMem.ma @ 1395

Last change on this file since 1395 was 1395, checked in by sacerdot, 8 years ago

1) New versions of pointer_of_beval/beval_of_pointer with a stricter dependent

type. They allow to close several proof obligations.

2) Globalenvs no longer uses -1 as a valid function block. It starts with -2
3) joint/semantics.ma uses a -2 block for the fake address used to signal the

end of program execution. Differently from what happens in OCaml, the block
is not allocated.

File size: 1.9 KB
Line 
1(* Memory model used in the dynamic semantics of the back-end intermediate
2   languages. Inspired by common/Mem.ma, adapted from Compcert *)
3
4(* * This file develops the memory model that is used in the dynamic
5  semantics of all the languages used in the compiler.
6  It defines a type [mem] of memory states, the following 4 basic
7  operations over memory states, and their properties:
8- [load]: read a memory chunk at a given address;
9- [store]: store a memory chunk at a given address;
10- [alloc]: allocate a fresh memory block;
11- [free]: invalidate a memory block.
12*)
13
14include "joint/BEValues.ma".
15include "common/GenMem.ma".
16
17definition bemem ≝ mem (mk_contentT beval BVundef).
18
19axiom beloadv: ∀m:bemem. ∀ptr:pointer. option beval.
20axiom bestorev: ∀m:bemem. ∀ptr:pointer. beval → option bemem.
21
22(* CSC: only pointers to XRAM or code memory ATM *)
23definition address ≝ beval × beval.
24
25definition eq_address: address → address → bool ≝
26 λaddr1,addr2.
27  eq_beval (\fst addr1) (\fst addr2) ∧ eq_beval (\snd addr1) (\snd addr2).
28
29definition pointer_of_address: address → res pointer ≝
30 λp. let 〈v1,v2〉 ≝ p in pointer_of_bevals [v1;v2].
31definition address_of_pointer: pointer → res address ≝ beval_pair_of_pointer.
32
33definition code_pointer_of_address: address → res (Σp:pointer. ptype p = Code) ≝ code_pointer_of_beval_pair.
34definition address_of_code_pointer: (Σp:pointer. ptype p = Code) → address ≝ beval_pair_of_code_pointer.
35
36definition addr_add: address → nat → res address ≝
37 λaddr,n.
38  do ptr ← code_pointer_of_address addr ;
39  OK … (address_of_code_pointer (shift_pointer 16 ptr (bitvector_of_nat … n))).
40normalize cases ptr #p #E @E
41qed.
42
43definition addr_sub: address → nat → res address ≝
44 λaddr,n.
45  do ptr ← code_pointer_of_address addr ;
46  OK … (address_of_code_pointer (neg_shift_pointer 16 ptr (bitvector_of_nat … n))).
47normalize cases ptr #p #E @E
48qed.
Note: See TracBrowser for help on using the repository browser.