\subsection{Virtual Machine}
\label{section:vm}

\Arch\ uses \see~\cite{ckc12} version 1.1-10.09.2011, itself based on
QEMU~\cite{b05b} and KLEE \cite{cde08}, for symbolic execution.
\see\ provides the execution environment, path forking, and constraint solving
capability necessary for symbolic execution.  All driver and kernel code, including the \tf, executes
within an \see\ VM.  Changes to \see\ fall into two categories: (i)
improved support for symbolic hardware, and (ii) the \Arch\ 
path-selection mechanism, which is an \see\ plugin.

\Arch\ uses invalid x86 opcodes for communication with the VMM and
\see\ plugins to provide additional control over the executing code.
We augment \see\ with new opcodes for the \tf\ that pass information
into our extensions. These opcodes are inserted into driver code by
\ds\ and also invoked directly by the \tf.

The purpose of the opcodes is to communicate source-level information
to the \Arch\ plugins, which uses the information to guide the
driver's execution.  The opcodes (i) control whether memory regions
are symbolic, as when mapping data for DMA; (ii) influence path
scheduling by adjusting priority, search strategy, or killing other
paths; and (iii) support tracing by turning it on/off and providing
stack information.

\ignore{
\begin{table}[t!]
\small
\centering
\begin{tabular}{p{1.2in}|p{1.7in}}
{\bf Opcode} & {\bf Description} \\
\hline
\hline

\codesm{make\_dma\_symbolic}, \codesm{free\_dma\_symbolic} & Allocate
/ deallocate regions of DMA memory. \\

\hline

\codesm{concretize} & Concretize all symbolic data in the current
state. \\

\hline
\hline

\codesm{prioritize}, \codesm{deprioritize} & Modify the relative
priority of the currently executing path. \\

\hline

\codesm{favor\_successful} & Toggle the heuristic that favors
successful path exploration at the expense of coverage. \\

\hline

\codesm{loop\_before}, \codesm{loop\_body} \codesm{loop\_after} &
Notify the VMM that a loop is beginning, executing its body, or
ending. \\

\hline

\codesm{kill\_all\_others} & Terminate all other paths but leave the
current one executing. \\

\hline
\hline

\codesm{driver\_call\_stack} & Notify the VMM of the location
of the current path in the code. \\

\hline

\codesm{enable\_tracing}, \codesm{disable\_tracing} & Enable / disable
tracing of I/O operations. \\

\end{tabular}
\caption{\small \bf Opcodes added in \Arch.}
\label{fig:table-opcodes}
\vspace{-0.2in}
\end{table}
} %% \ignore
