source: etc/campbell/dev-notes/2012-07-10-reducing-memory-spaces.txt

Last change on this file was 2394, checked in by campbell, 7 years ago

I've kept the odd note on bits of CerCo? work I've been doing. James suggested
that it might be useful if these were recorded in the repository just in case
they contain some useful information that doesn't get recorded elsewhere.

File size: 1.1 KB
Line 
1I'm changing the representation of pointer offsets to bit vectors partly for
2the convenience of proving code generation correct, but also because I allowed
3too much data to be extracted from pointer offsets by subtraction and this is
4a definite way to restrict the amount of data available.
5
6To do it properly with memory spaces I'd need to parametrise the size of offset
7by the pointer type and pointed-to memory space, e.g.
8
9  an Any pointer to IData would have an 8 bit offset,
10  a PData pointer to PData would have an 8 bit offset, but
11  an XData pointer to PData would have a 16 bit offset.
12
13However, this is complex and we don't support memory spaces in the prototype or
14the back-end, so I'm collapsing the memory spaces to just XData and Code.  This
15removes the need to distinguish between different types of pointers, so regions
16only appear in the block, not the pointer, and the pointer compatible entry
17disappears.
18
19Note carefully that any comparison must check the region in the block; we should
20not give semantics to comparisons between code and data pointers because we
21won't know whether the concrete representations will be equal or not.
Note: See TracBrowser for help on using the repository browser.