source: src/joint/BEMem.ma @ 1329

Last change on this file since 1329 was 1329, checked in by sacerdot, 10 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.