Computing Verified Machine Address Bounds During Symbolic Exploration of Code

When operational semantics is used as the basis for mechanized verification of machine code programs it is often necessary for the theorem prover to determine whether one expression denoting a machine address is unequal to another. For example, this problem arises when trying to determine whether a read at the address given by expression a is affected by an earlier write at the address given by b. If it can be determined that a and b are definitely unequal, the write does not affect the read. Such address expressions are typically composed of “machine arithmetic function symbols” such as +, *, mod, ash, logand, logxor, etc., as well as numeric constants and values read from other addresses. In this chapter we present an abstract interpreter for machine address expressions that attempts to produce a bounded natural number interval guaranteed to contain the value of the expression. The interpreter has been proved correct by the ACL2 theorem prover and is one of several key technologies used to do fast symbolic execution of machine code programs with respect to a formal operational semantics. We discuss the interpreter, what has been proved about it by ACL2, and how it is used in symbolic reasoning about machine code.