source: etc/campbell/dev-notes/2012-08-15-unsigned-offsets.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: 799 bytes
1Ilias asked about this and I don't appear to have a note from before:
3Our pointer offsets are just bitvectors, and our memory model allows for
4looking up negative offsets (given in Z) in memory.  So do we take the
5bitvectors to be signed or unsigned?
7They must be unsigned, because we can have offsets > 2^{15}, e.g., by
8allocating most of the memory in a 40kB array and making a pointer to the
9last element.  We only use the pointer type to access memory in CerCo at the
10moment, so negative offsets are inaccessible.  CompCert has a similar
11arrangement, but its memory model has a load function that takes an offset
12in Z directly (in addition to the one that take a pointer value and can only
13hit positive offsets), so they can access negative offsets from other parts of
14the language semantics.
Note: See TracBrowser for help on using the repository browser.