source: src/joint/BEMem.ma @ 1651

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

All axioms closed.

File size: 2.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 becontentT ≝ mk_contentT beval BVundef.
18definition bemem ≝ mem becontentT.
19
20(* This function should be moved to common/GenMem.ma and replaces in_bounds *)
21definition do_if_in_bounds:
22 ∀A:Type[0]. bemem → pointer → (block → block_contents becontentT → Z → A) → option A ≝
23 λS,m,ptr,F.
24  let b ≝ pblock ptr in
25  if Zltb (block_id b) (nextblock … m) then
26   let content ≝ blocks … m b in
27   let off ≝ offv (poff ptr) in
28   if andb (Zleb (low … content) off) (Zleb off (high … content)) then
29    Some … (F b content off)
30   else
31    None ?
32  else
33   None ?.
34
35definition beloadv: ∀m:bemem. ∀ptr:pointer. option beval ≝
36 λm,ptr. do_if_in_bounds … m ptr (λb,content,off. contents … content off).
37
38definition bestorev: ∀m:bemem. ∀ptr:pointer. beval → option bemem ≝
39 λm,ptr,v. do_if_in_bounds … m ptr
40  (λb,content,off.
41    let contents ≝ update … off v (contents … content) in
42    let content ≝ mk_block_contents (mk_contentT beval BVundef) (low … content) (high … content) contents in
43    let blocks ≝ update_block … b content (blocks … m) in
44     mk_mem … blocks (nextblock … m) (nextblock_pos … m)).
45
46(* CSC: only pointers to XRAM or code memory ATM *)
47definition address ≝ beval × beval.
48
49definition eq_address: address → address → bool ≝
50 λaddr1,addr2.
51  eq_beval (\fst addr1) (\fst addr2) ∧ eq_beval (\snd addr1) (\snd addr2).
52
53definition pointer_of_address: address → res pointer ≝
54 λp. let 〈v1,v2〉 ≝ p in pointer_of_bevals [v1;v2].
55definition address_of_pointer: pointer → res address ≝ beval_pair_of_pointer.
56
57definition code_pointer_of_address: address → res (Σp:pointer. ptype p = Code) ≝ code_pointer_of_beval_pair.
58definition address_of_code_pointer: (Σp:pointer. ptype p = Code) → address ≝ beval_pair_of_code_pointer.
59
60definition addr_add: address → nat → res address ≝
61 λaddr,n.
62  do ptr ← code_pointer_of_address addr ;
63  OK … (address_of_code_pointer (shift_pointer 16 ptr (bitvector_of_nat … n))).
64normalize cases ptr #p #E @E
65qed.
66
67definition addr_sub: address → nat → res address ≝
68 λaddr,n.
69  do ptr ← code_pointer_of_address addr ;
70  OK … (address_of_code_pointer (neg_shift_pointer 16 ptr (bitvector_of_nat … n))).
71normalize cases ptr #p #E @E
72qed.
Note: See TracBrowser for help on using the repository browser.