|
|
|---|
|
|
|
|---|
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 user 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 an 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-1Note that this address space is 2^48 bytes of memory. So I can use the addresses
0 to 2^47-1to map the first range, and the addresses
-2^47 to -1to map the second range.
0 to 2^47-1 | 0 to 2^47-1The 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
of