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