The core of the prover implements a very limited simulation of an x86 processor. The intent of this simulation is not to run the program or yield results, but to quickly attempt reason about the instructions and values used in a program and to attempt to determine whether memory accesses are safe.
A surprisingly complex part of this process is decoding the x86 instructions into the actual operation and operands. Figure 7 shows the general form of a x86 instruction. The x86 is a CISC architecture and earns the designation ``complex.'' There are multiple opcodes for the same actual instruction, and the operands are determined by the opcode in ways that are frequently not well patterned. The instructions appear to be designed for a table-driven instruction decoder. For performance reasons, actual x86 chips probably implement this as optimized combinational logic, but development tools I looked at consistently used the table-driven decoding approach.
Appendix A of Intel's ISA reference[6] contains ``opcode maps,'' which are tables of the mapping between opcode byte values and the instructions and operands they represent. Tools for the x86 instruction set commonly adapt these tables to drive their decoding of the instruction set, so this approach was chosen for use in the prover. The general structure of the tables works well for an implementation. There were many errors in the tables provided in Intel's documentation; in most cases, these errors were obvious when read, but there were a few cases that were more subtle and caused problems that were found during debugging of the prover. I submitted the first few corrections to Intel's developer support group and have yet to receive any response. Given that many of these errors are in parts of the tables that have not changed in over twenty years, this is unfortunate.
Figure 8 lists the subset of the Intel operand codes that are currently supported by the prover. Operands relating to segmentation, floating point, media instructions, and privileged or machine control instructions are all unsupported because the instructions that might use them are unsupported. Also unsupported are operand types not generated by gcc. These operand codes are used directly in the decode tables of the prover, along with a function pointer that calls a function that actually implements the operation specified.
An example of the resulting decode structure is the entry for opcode 0x89:
{ insn_mov, OP_Ev, OP_Gv, OP_NONE, FL_NONE },
This structure indicates that the actual operation is performed by the
function insn_mov(), that its first parameter is a variable-length
(that is, determined by the current word size mode) general purpose register,
that its second parameter is a variable-length general purpose register or
memory location, that this function has no third parameter (which most don't),
and that this operation does not affect the %eflags register.
A set of important special cases are bytecodes that are not opcodes at all, and instead are prefixes that modify the following bytecodes. Most of these fall into categories of instructions that are not allowed (e.g., segment prefixes, address-size prefix, and the lock prefix), but two that need to be supported are the word-size prefix (0x66) and the two-byte opcode prefix (0x0f). Both are handled as if they were no-operand opcodes, and the functions that implement them return special values that are accumulated into an internal set of flags in the instruction decoder. These flags are accumulated and affect decoding of subsequent bytes until an ``ordinary'' instruction completion, at which point they are reset. One flag, used to implement the two-byte opcodes, switches the table used to decode opcode bytes. The other flag, used to implement the word-size prefix, causes a temporary operand structure to be created for the current instruction in which variable-length operand specifications are replaced with 16-bit length operand specifications (thus changing them from 32-bit operands to 16-bit operands).
Instruction execution is simulated through short functions. These functions are not meant to model the actual execution of instructions. They are meant to track whether their results are predictable or not, and, if so, attempt to predict or put a range on the output values. So, for example, the mov instruction simply copies its first operand to its second; its second operand therefore has the same predictability properties as its first. In contrast, the or instruction takes two values and does a bitwise operation on them. If the two values are exactly known, an exactly known result can be generated; otherwise, the result of a bitwise or operation on at least one unknown quantity with a known quantity is difficult to reason about, and is simply considered to yield an unknown result. This is not a significant problem in practice because bitwise operations are not commonly used to generate addresses, and the prover is primarily interested in tracking values that are used as addresses.
One particularly tricky problem is conditional branch instructions. The prover was originally intended to use a reasonably sophisticated technique of tracking where result flags values came from and using some of those sources together with conditional branches to constrain values. For example, in order to implement reasoning about variable-length input blocks, the prover needs to be able to look at a comparison with the length variable and to separate what code is executed if the length is greater than or less than the value compared against. Otherwise, the code could be correctly checking for length and not doing accesses beyond the buffer, but the prover wouldn't be able to determine that. A simpler technique turns out to be surprisingly successful; all conditional branches are treated as a nondeterministic branch, and both forks are checked independently. Combined with a large fixed input buffer length, the inability to reason about values is not a problem. This also captures the critical property that run-time conditionals are typically not certain in advance (otherwise there would be no need for such a conditional), but that both sides of the branch must be to code that will do something safe.
Levels of nondeterminism and the total number of instructions that can be executed in a path are bounded in the prover. This is not so much designed to bound the program (though that is a consequence) as it is to bound the run-time of the prover. The intended applications of this prover are places where speed and small memory usage are important, and must be rather tightly bounded. The current prover allows up to 32 levels of nondeterminism and up to 128 instructions per path. These limits allow short and simple programs to be proven, which is the intent of the prover, but are not enough to allow complex programs to be proven safe, which probably would be outside the capacity of the prover anyway. These limits are very easily increased at compile-time if needed. Note that nondeterministic branches currently cannot rejoin; they become separate from every other branch until they terminate.