source: src/joint/BEMem.ma @ 1329

Last change on this file since 1329 was 1329, checked in by sacerdot, 9 years ago
  1. Definition of addresses moved to BEMem
  2. Basic functions on addresses implemented in BEMem and used everywhere
  3. Semantics of ERTL extended statements completed
File size: 1.7 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].
31
32(*CSC: for pointers of type Code and XData, the next function type can be
33 strengthtened to never fail *)
34definition address_of_pointer: pointer → res address ≝ beval_pair_of_pointer.
35
36definition addr_add: address → nat → res address ≝
37 λaddr,n.
38  do ptr ← pointer_of_address addr ;
39  address_of_pointer (shift_pointer 16 ptr (bitvector_of_nat … n)).
40
41definition addr_sub: address → nat → res address ≝
42 λaddr,n.
43  do ptr ← pointer_of_address addr ;
44  address_of_pointer (neg_shift_pointer 16 ptr (bitvector_of_nat … n)).
Note: See TracBrowser for help on using the repository browser.