Application-level view of the x86 model
The x86 model can be used in the application-level view
when the value of the field
Some supervisor-level features are neither used nor required for the analysis of application software. In most cases, a application cares about the correctness of his application program while assuming that services like paging and I/O operations are provided reliably by the operating system. The application-level view of our model attempts to provide the same environment to a application for reasoning as is provided by an OS for programming. In this mode, our memory model provides the 2^48-byte linear address space specified for modern 64-bit Intel machines.
A 64-bit canonical address can be in either of the two ranges below:0 to 2^47-1 or 2^64-2^47 to 2^64-1
Note that this address space is 2^48 bytes of memory. So I can use the addresses0 to 2^47-1
to map the first range, and the addresses-2^47 to -1
to map the second range.0 to 2^47-1 | 0 to 2^47-1
The advantage of doing so is that we will avoid bignum creation during address computations.
We define some linear memory read and write functions, like rvm08 and wvm08. These functions are called by the top-level
functions, like rml08 and wml08 when
The guards of the linear memory functions are stricter than those