source: src/joint/BEMem.ma @ 1248

Last change on this file since 1248 was 1213, checked in by sacerdot, 9 years ago

1) New values (joint/BEValues.ma) and memory model for the back-ends

(joint/BEMem.ma) where all values are Byte-valued.

2) Improved joint semantics for the back-end languages based on the new

memory model (work in progress).

3) SmallStepExec? made more general to accomodate states with an arbitrary

memory inside.

4) New files common/Pointers.ma and common/GenMem.ma shared between the

front-end and the back-end. GenMem?.ma, at the moment, is not used in Mem.ma
(cut&paste code).

File size: 810 bytes
RevLine 
[1213]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.
Note: See TracBrowser for help on using the repository browser.