\section{Design}
\label{section:implementation}

The \Arch\ architecture focuses on thorough testing of drivers to
ensure the code does not crash, hang, or incorrectly use the
kernel/driver interface. We target test
situations where the driver code is available, and uses that code to
simplify testing by combining symbolic execution, static
source-code analysis and transformation, and a fine-grained \tf.

The design of \Arch\ is shown in Figure \ref{fig:symdrive-arch}.  The OS
kernel and driver under test, as well as user-mode test programs,
execute in a virtual machine. The symbolic execution engine provides
symbolic devices for the driver. \Arch\ provides stubs that invoke
checkers on every call into or out of the driver. A \tf\ tracks
execution state and passes information to plugins running in the
engine to speed testing and improve test coverage.

We implemented \Arch\ for Linux and FreeBSD, as these kernels provide
a large number of drivers to test. The design applies to any operating
system supported by \see\ (32-bit OSes that run on QEMU~\cite{b05b}),
and only the \tf\ code is specialized to the OS.  We made small,
conditionally compiled changes to both kernels to print failures and
stack traces to the \see\ log and to register the module under test
with \see.  The breakdown of \Arch\ code is shown in
Table~\ref{table:lines-of-code}.

\Arch\ consists of five components: (i) a modified version of the
\see\ symbolic-execution engine, which consists of a
\Arch-specific plugin as well as changes to the underlying system;
(ii) symbolic devices to provide
symbolic hardware input to the driver; (iii) a {\em \tf} executing
within the kernel that guides symbolic execution; (iv) the {\em \ds}
static-analysis and code transformation tool to analyze and
prepare drivers for testing; and (v) a set of OS-specific {\em
  checkers} that interpose on the driver/kernel interface for
verifying and validating driver behavior.

\begin{figure}
\begin{center}
\includegraphics[keepaspectratio=true,width=2.2in]{figures/SymArch.pdf}
\end{center}
\vspace{-0.3in}
\caption{\small \bf The \Arch\ architecture. A developer produces the
  transformed driver with \ds\ and can write checkers and test
  programs to verify correctness.}
\label{fig:symdrive-arch}
\vspace{-0.1in}
\end{figure}

\begin{table}
\small
\centering
\begin{tabular}{l|r}
{\bf Component} & {\bf LoC} \\
\hline
Changes to \see & 1,954 \\
\ds & 2,681 \\
\Tf & 3,002 \\
Checkers & 564 \\
Support Library & 1,579 \\
Linux kernel changes & 153 \\
FreeBSD kernel changes & 81 \\
\end{tabular}
\vspace{-0.1in}
\caption{\small \bf Implementation size of \Arch. }
\label{table:lines-of-code}
\vspace{-0.2in}
\end{table}


\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 and constraint solving
capability necessary for symbolic execution.  It also implements the
path forking that takes place as symbolic values are compared against
each other.  All driver and kernel code, including the \tf, executes
within the \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.

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

The purpose of the opcodes is to communicate source-level information
to the VMM, which uses the information to guide the driver's
execution.  The opcodes fall into three sets that: (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


\subsection{Symbolic Devices}

Drivers interact with devices according to well-defined, narrow
interfaces.  For PCI device drivers, this interface is comprised of
I/O memory accessed via normal loads and stores, port I/O
instructions, bus operations, DMA memory, and interrupts.  Drivers
using other buses, such as SPI and \itwoc, use wrapper functions for
similar operations.

% From Matt - I cut the following paragraph as we seem to cover this
% in the subsequent sections.

%To provide symbolic hardware, \see\ provides symbolic data of the
%appropriate size each time the driver performs a read operation using
%memory or port I/O.  Similarly, the VMM treats the contents of DMA
%memory, indicated through DMA mapping functions, as symbolic.  The VMM
%does not insert symbolic interrupts; instead, \Arch\ invokes the
%driver's interrupt handler each time control passes from the driver to
%the kernel. For buses such as \itwoc\ that use I/O wrapper functions,
%\Arch\ rewrites the wrappers to return symbolic data.

\Arch\ provides a symbolic device for the driver under test, while at
the same time emulating the other devices in the system. A symbolic
device provides three key behaviors. First, it must be discovered, so
the kernel loads the appropriate driver. Second, it must provide
methods to read from and write to the device and return symbolic data
from reads. Third, it supports interrupts and DMA, if needed.
\Arch\ currently supports 5 buses on Linux: PCI (and its variants),
\itwoc\ (including SMBus), Serial Peripheral Interface (SPI), General
Purpose I/O (GPIO), and Platform;\footnote{The ``platform bus'' is a
  Linux-specific term that encompasses many embedded devices.  Linux's
  ARM implementation, for example, supports a variety of SoCs, each
  with its own set of integrated devices.  The drivers for these
  devices are often of the ``platform'' type.} and the PCI bus on
FreeBSD.

\paragraph{Device Discovery.}
%\fixme{Julia: this section is rather technical -- can it be simplified
%  and/or can we provide an example}

When possible, \Arch\ creates symbolic devices in the \see\ virtual
machine and lets existing bus code discover the new device and load
the appropriate driver.  For some buses, such as \itwoc, the kernel or
another driver normally creates a statically configured device object
during initialization. For such devices, we created a small kernel
module, consisting of 715 lines of code, that creates the desired
symbolic device.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% one reviewer wanted to know why we don't do USB.  Here's an example
% response that's way too long

%We believe SymDrive
%would work with USB, but would require a more effort to implement a
%symbolic bus.  USB device drivers interface with other drivers lower
%in a stack.  The host controller interface driver communicates with
%the hardware, and modern operating systems typically only need one
%such driver for USB 1.0, 2.0, and 3.0.  Supplying symbolic data at
%this level of abstraction is not practical, because it would need to
%pass through the host controller driver, and likely generate many
%uninteresting paths.

%To address this issue, we would need to write a symbolic bus similar
%to the one used by SymDrive's I2C support.  I2C provides a similar,
%high-level communication interface with the device, implemented in
%Linux's i2c-core and one of the various chip-specific drivers,
%e.g. PIIX4.  We've not done a similar implementation for USB because
%of time constraints.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


%For example, \Arch\ uses \see's symbolic
%hardware plugin to create a virtual PCI device with the desired I/O
%memory configuration and PCI identifiers, both easily found in
%driver source code. This device triggers the PCI code in Linux to load the
%driver.

% Edited to add that a number of drivers also create these devices.
% For example, many PCI-E video cards have thermal monitoring
% features, and these temperature sensors are often I2C, so the video
% card driver then creates the corresponding I2C device.

\Arch\ can make the device configuration space symbolic after loading
the driver by returning symbolic data from PCI bus functions with the
\tf (similar to \see's NDIS driver support).  PCI devices use this
region of I/O memory for plug-and-play information, such as the vendor
and device identifiers.  If this memory is symbolic, the driver will
execute different paths for each of its supported devices. Other buses
have similar configuration data, such as ``platform data'' on the SPI
bus. A developer can copy this data from the kernel source and provide
it when creating the device object, or make it symbolic for additional
code coverage.

\paragraph{Symbolic I/O.}
Most Linux and FreeBSD drivers do a mix of programmed I/O and DMA.
\Arch\ supports two forms of programmed I/O. For drivers that perform
I/O through hardware instructions, such as \codesm{inb}, or through
memory-mapped I/O, \Arch\ directs \see\ to ignore write operations,
because they do not return values that influence driver execution, and
return symbolic data from reads. The \tf\ overrides bus I/O functions,
such as those used in \itwoc\ drivers, to function analogously.

\paragraph{Symbolic Interrupts.}
After a driver registers an interrupt handler, the \tf\ invokes the interrupt
handler on every transition from the driver into the kernel.  This
model ensures the interrupt handler is called often enough to keep the
driver executing successfully, but represents a trade-off between
realism and complexity. A real device may generate interrupts more often,
including while the driver executes. However, testing the driver's
response to this many potential interrupts would result in path
explosion.  A real device may also raise fewer interrupts, in which case
case our approach tests the driver with spurious interrupts.

\paragraph{Symbolic DMA.}
When a driver invokes a DMA mapping function, such as
\codesm{dma\_alloc\_coherent}, the \tf\ uses an \see\ opcode to make
the memory act like a memory-mapped I/O region: each read returns a
new symbolic value and writes have no effect. Discarding writes to DMA
memory reflects the ability of the device to write the data via DMA at
any time.  The driver should not assume that data written here will be
available subsequently. When the driver unmaps the memory, the
\tf\ directs \see\ to revert the region to normal symbolic data, so
writes are seen by subsequent reads.

\subsection{Test Framework}

The \tf\ is a kernel module executing with the virtual machine that
assists symbolic execution and executes checkers.  \Arch\ relies on the
\tf\ to guide and monitor symbolic execution in three ways.  First,
the \tf\ implements policy regarding which paths to prioritize or
deprioritize.  Second, the \tf\ may inject additional symbolic data to
increase code coverage.  As mentioned above, it implements symbolic
I/O interfaces for some device classes. Finally, it provides the VMM
with a stack trace for {\em execution tracing}, which produces a trace
of the driver's I/O operations.

The \tf\ supports several load-time parameters for controlling its
behavior.  When loading the \tf\ with \codesm{insmod} or FreeBSD's
\codesm{kldload}, developers can direct the \tf\ to enable
high-coverage mode (described in Section~\ref{sec:exec-broadly}),
tracing, or a specific symbolic device.  To configure the device, developers
pass the device's I/O capabilities and name as parameters. Thus,
developers can script the creation of symbolic devices to automate
testing.

\Arch\ has to address two conflicting goals in testing drivers: (i)
executing as far as possible along a path, to complete initialization
and expose the rest of the driver's functionality; and (ii) executing
as much code as possible within each function for thoroughness.

\subsubsection{Reaching Deeply}
\label{sec:exec-broadly}
A key challenge in fully testing drivers is symbolically executing
branch-heavy code, such as loops and initialization code that probes
hardware. \Arch\ relies on two techniques to limit path explosion in
these cases: {\em favor-success scheduling} and {\em loop
  elision}. These techniques allow developers to execute further into
a driver, and test functionality that is only available after
initialization.

\paragraph{Favor-success scheduling.} Executing past driver
initialization is difficult because the code often has many
conditionals to support multiple chips and configurations.
Initializing a sound driver, for example, may require branching on
hardware-specific details over a thousand times. Each branch creates
additional paths to explore.

\Arch\ mitigates this problem with a {\em favor-success}
path-selection algorithm that prioritizes successfully executing
paths, making it a form of best-first search.  Notifications from the
\tf\ increase the priority of the current path at every successful
function return, both within the driver and at the driver/kernel
interface. Higher priority causes the current path to be explored
further before switching to another path.

% Next paragraph:
% Linux uses negative errno values, whereas FreeBSD uses positive
% errno values.  The text does not distinguish this detail but it
% doesn't seem important.

At every function exit, the \tf\ notifies \see\ of whether the
function completed successfully, which enables the VMM to prioritize
successful paths to facilitate deeper exploration of code. The
\tf\ determines success based on the function's return value. For
functions returning integers, the \tf\ detects success when the
function returns a value other than an \codesm{errno}, which are
standard Linux and FreeBSD error values. On success, the \tf\ will notify the VMM
to prioritize the current path.  If the developer wishes to prioritize
paths using another heuristic, he/she can add an annotation
prioritizing any piece of code. We use this approach only in some
network drivers to select paths where the carrier is on, which allow
execution of the driver's packet transmission code.

The \tf\ prunes paths when control returns to the kernel successfully to focus
symbolic execution just on the driver. It kills all other paths still
executing in the driver and uses an opcode to concretize all data in
the virtual machine, so the kernel executes on real values and will
not fork new paths.  This ensures that a single path runs in the
kernel, which allows developers to interact with the system and run
user-mode tests.

%
% E1000 checksum loop for reference
%
%     for (i = 0; i < (EEPROM_CHECKSUM_REG + 1); i++) {
%         if (e1000_read_eeprom(hw, i, 1, &eeprom_data) < 0) {
%             DEBUGOUT(``EEPROM Read Error\n'');
%             return -E1000_ERR_EEPROM;
%         }
%         checksum += eeprom_data;
%     }
%
%     if (checksum == (u16)EEPROM_SUM)
%         return E1000_SUCCESS;
%     else {
%         DEBUGOUT(``EEPROM Checksum Invalid\n'');
%         return -E1000_ERR_EEPROM;
%     }
%

\paragraph{Loop elision.} Loops are challenging for symbolic
execution, because each iteration may fork new paths.
\Arch\ addresses loops explicitly by prioritizing those paths that
exit them quickly.  When \Arch\ starts executing a loop's second
iteration, it checks whether the loop created any new paths on the
first iteration.  If so, \Arch\ automatically deprioritizes the path
that began the second loop iteration.  If a different path executes
the same loop for a second iteration, \Arch\ prioritizes this path on
subsequent iterations, hoping that it will terminate quickly.  The
rationale behind this heuristic is that it forces at least one other
possible path to execute the loop for one iteration, with the hope
that this other path will exit the loop.  If the loop executes more
than 20 iterations and continues generating paths, \Arch\ prints a
message warning of poor performance, since it was unable break out of
the loop early.

This approach executes hardware polling loops efficiently and
automatically, and warns developers when loops cause
performance problems.  However, this approach may fail if a loop is
present in uninstrumented kernel code.  It can also result in worse
coverage of code that executes only if a polling loop times
out.  Nevertheless, we have not found these problems to be
significant.

%For example, the E1000 network driver code shown in
%Figure~\ref{fig:eeprom} calculates a checksum over the device EEPROM
%data, and only continues if the checksum is valid.

\see\ provides an ``EdgeKiller'' plugin that a developer may use to
terminate complex loops early, but requires developers to identify
each loop's offset into the driver binary~\cite{ckc12}.  Moreover,
loops that produce a value, such as a checksum calculation, cannot
exit early without stopping the driver's progress.

% Other problematic situations:
% - Some driver entry points are called within loops in the kernel,
% and we can't instrument those typically, unless we do something like
% running SymGen over that code as well.
% 
% These loop problems have become much less significant since S2E was
% updated to defer calls to the constraint solver.

\Arch's approach extends the EdgeKiller plugin in two directions.
First, it allows developers to annotate driver source rather than
having to parse compiled code.  Second, source annotations persist
across driver revisions, whereas the binary offsets used in the
EdgeKiller plugin need updating each time the driver changes.
%Finally, \Arch\ provides more flexibility in path selection than
%EdgeKiller's simple termination strategy, and allows driver execution
%to proceed along a successful path.  For example, EdgeKiller does not
%allow checksum loops to exit early successfully.

Annotating code manually to improve its execution performance does
reduce \Arch's ability to find bugs in that code.  Wherever
annotations were needed in the drivers we examined, we strove to write
them in such a way as to execute the problematic loop at least once
before terminating early.  For example, after a checksum loop, we would
add a line to return a symbolic checksum value, which could then be
compared against a correct one.

\subsubsection{Increasing Coverage}
\label{sec:exec-deeply}

\Arch\ provides a {\em high-coverage} mode for testing specific
functions, for example those modified by a patch. This mode 
changes the path-prioritization policy and the behavior of kernel
functions. When the developer loads the \tf\ module, he/she can
specify any driver function to execute in this mode.  

When execution enters the specified function, the \tf\ notifies
\see\ to favor unexecuted code (the default \see\ policy) rather than
favoring successful paths. The \tf\ also terminates all paths that
return to the kernel in order to focus execution within the
driver. Finally, when the driver invokes a kernel function, the
\tf\ makes the return value symbolic.  This mode is similar to the
local consistency mode in \see~\cite{ckc12}, but requires no
developer-provided annotations or plugins, and supports all kernel
functions that return standard error values.  For example,
\codesm{kmalloc} returns a symbolic value constrained to be either
NULL or a valid address, which tests error handling in the driver.

For the small number of kernel functions that return non-standard
values, \ds\ has a list of exceptions and how to treat their return
values.  The full list of exceptions for Linux currently contains 100
functions shared across all supported drivers.  Of these, 64 are
hardware-access functions, such as \codesm{inb} and \codesm{readl},
that always return symbolic data.  A further 14 functions are
arithmetic operations, such as \codesm{div32}.  The remaining 22
functions return negative numbers in successful cases, or are used by
the compiler to trigger a compilation failure when used incorrectly,
such as \codesm{\_\_bad\_percpu\_size}.

% I'm not very confident in these results.
%In addition, we did a first-pass static analysis of the drivers/base/*
%and drivers/pci/* kernel source files, and found that none of the 118
%functions exported from there return negative values on success, and
%so would need no special treatment with \Arch's favor-success
%scheduling, though 14 may need special treatment with \Arch's
%high-coverage mode.  We believe a static analysis of Linux error
%codes, as in~\cite{graal08}, would provide a complete accounting of
%this list.

\Arch\ also improves code coverage by introducing additional symbolic
data, which allows a driver to execute code that requires specific
inputs from the kernel or applications.  \Arch\ can automatically make
a Linux driver's module parameters symbolic, which allows a driver to
execute with all possible parameters.  Checkers can also make
parameters to the driver symbolic, such as \codesm{ioctl} command
values. This allows all \codesm{ioctl} code to be tested with a single
invocation of the driver, because each comparison of the command will
fork execution. In addition, \see\ allows using symbolic data anywhere
in the virtual machine, so a user-mode test can pass symbolic data to
the driver.

% Note that FreeBSD does not support making parameters symbolic.
% FreeBSD module parameters don't exist -- instead, they access
% ``kernel environment variables'' or use the ``sysctl'' interface.
% We could add support for these in the future but don't have it yet.


%\fixme{Julia: did not like the next bit about PTR\_ERR.  She says
%  there are lots of functions like this.  Not a small number (over
%  1800 in a recent linux-next).  Presumably you do the same for NULL
%  as for negative ints?  It's not clear how short this list of
%  functions is.  Matt says: I'm confused by her comment.  All the
%  function does is cast a pointer to a long.  It does not necessarily
%  make sense to make a decision about whether to prioritize /
%  deprioritize based on that alone, which is why we have it in the
%  list.  As for the over 1800 functions like that, in those cases, it
%  likely is fine to apply the usual prio/deprio heuristic.  If we do
%  another example, there's e.g. test\_and\_set\_bit or any other
%  bit-manipulation function.  We currently have 23 functions in this
%  list though some I'd added preemptively and we may not need to leave
%  there.  We could also mention, e.g. \_\_bad\_percpu\_size which is a
%  function we should not instrument because it's specifically written
%  not to exist -- it's a C idiom to prevent compilation if the driver
%  developer specifies a bad parameter to certain macros/code.  Others
%  are \_\_bad\_size\_call\_parameter or \_\_xchg\_wrong\_size}


\subsubsection{Execution Tracing}

The \tf\ can generate execution traces, which are helpful to compare
the execution of two versions of a driver.  For example, when a driver
patch introduces new bugs, the traces can be used to compare its
behavior against previous versions. In addition, developers can use
other implementations of the driver, even from another operating
system, to find discrepancies that may signify incorrect interaction
with the hardware.

A developer can enable tracing via a command-line tool that uses a
custom opcode to notify \Arch\ to begin recording. In this mode, an
\see\ plugin records every driver I/O operation, including reads and
writes to port, MMIO, and DMA memory, and the driver stack at the
operation. The \tf\ passes the current stack to \see\ on every
function call.

The traces are stored as a trie (prefix tree) to represent multiple
paths through the code compactly (similar to \see), and can be
compared using the \codesm{diff} utility.  However, \Arch\ annotates
each trace entry with the driver call stack at the I/O operation. This
facilitates analysis of specific functions and comparing drivers
function-by-function, which is useful since traces are subject to
timing variations and different thread interleavings.  

\subsection{\ds}

All features of the \tf\ that interact with code, such as
favor-success scheduling, loop prioritization, and making kernel
return values symbolic are handled automatically via static analysis
and code generation.  The \ds\ tool analyzes driver code to identify
code relevant to testing, such as function boundaries and loops, and
instruments code with calls to the \tf\ and checkers.  \ds\ is built
using CIL~\cite{nmr+02}.

% \fixme{Julia: do we ever want to prioritize failure}

\paragraph{Stubs.}
\Arch\ interposes on all calls into and out of the driver with stubs
that call the \tf\ and checkers.  For each function in the
driver, \ds\ generates two stubs: a preamble, invoked at the top of
the function, and a postscript, invoked at the end. The generated code
passes the function's parameters and return value to these stubs, to
be used by checkers.  In addition, for each kernel function the driver
imports, \ds\ generates a stub function with the same signature that
wraps the function. These stubs ensure that the \tf\ can interpose on
all calls within the driver as well as calls into the kernel.

To support pre- and post-condition assertions, stubs invoke checkers
when the kernel calls into the driver or the driver calls into the
kernel. Checkers associated with a specific function
\codesm{function\_x} are named \codesm{function\_x\_check}. On the
first execution of a stub, the \tf\ looks for a corresponding checker
in the kernel symbol table. If such a function exists, the stub
records its address for future invocations.  While targeted at
functions in the kernel interface, this mechanism can invoke checkers
for any driver function.

Stubs employ a second lookup to find checkers associated with a
function pointer passed from the driver to the kernel, such as a PCI
probe function. Kernel stubs, when passed a function pointer, record
the function pointer and its purpose in a table. For example, the
Linux \codesm{pci\_register\_driver} function associates the address
of each function in the \codesm{pci\_driver} parameter with the name
of the structure and the field containing the function.  The stub for
the \codesm{probe} method of a \codesm{pci\_driver} structure is thus
named \codesm{pci\_driver\_probe\_check}.  FreeBSD drivers use a
similar technique.

% Note -
% FreeBSD drivers have a probe() function but these only look for the
% right PCI device and vendor IDs.  FreeBSD uses the term ``attach''
% to refer to their version of Linux's ``probe'' function.  FreeBSD
% also requires a slightly customized analysis to support the way they
% communicate these driver function addresses to the kernel, but the
% rest is the same.

Stubs detect that execution enters the driver by tracking the depth of
the call stack. The first function in the driver notifies the \tf\ at
its entry that driver execution is starting, and at its exit notifies
the \tf\ that control is returning to the kernel.  Stubs also
communicate this information to the VMM so that it can make path
scheduling decisions based on function return values.

\paragraph{Instrumentation.}
As in the case of the stubs, the underlying principle behind \ds's
instrumentation is to inform the VMM of source level information as it
executes the driver so it can make better decisions about which paths
to execute.  \ds\ instruments the start and end of each driver
function with a call into the stubs.  As part of the rewriting, it
converts functions to have a single exit point. It generates the same
instrumentation for inline functions, which are commonly used in the
Linux and FreeBSD kernel/driver interfaces.

\ds\ also instruments the start, end, and body of each loop with
calls to short functions that execute \Arch-specific opcodes.  These opcodes direct the VMM to
prioritize and deprioritize paths depending on whether they exit the
loop quickly. This instrumentation replaces most of the per-driver effort
required by \see\ to identify loops, as well as the per-class effort
of writing a consistency model for every function in the driver/kernel
interface.  \ds\ inserts loop opcodes into the driver, as shown in
Figure~\ref{fig:auto-loop-annot}, to tell \see\ which paths exit the
loop, and should receive a priority boost.\footnote{One interesting
  alternative is to prioritize paths that execute loops in their
  entirety.  The problem with this approach is that it may generate
  many states in the process, and slow testing.}


For complex code that slows testing, \ds\ supports programmer-supplied
annotations to simplify or disable the code temporarily. Short loops
and those which do not generate states require no manual developer
effort.  Only loops that must execute for many iterations and generate
new paths on each iteration need manual annotation, which we implement
through C \codesm{\#ifdef} statements.  For example, the E1000 network
driver that verifies an checksum over EEPROM, and we modified it
accept any checksum value.  We have found these cases to be rare.
When loops result poor performance, \Arch\ prints a warning with the
loop's location in the source code.  Identifying the root cause, such
as a checksum calculation, is then straightforward.


\begin{figure}[t!]
%\fvset{fontfamily=courier, fontsize=\footnotesize,xleftmargin=-5mm}
%\LVerbatimInput{code/e1000_checksum.c}
\begin{center}
\includegraphics[keepaspectratio=true,width=3in]{figures/auto_loop_annotation.pdf}
\end{center}
\vspace{-0.3in}
\caption{\small \bf \ds\ instruments the start, end, and body of loops
  automatically.  This code, from the 8139cp driver, was modified
  slightly since \ds\ produces preprocessed output.}
\label{fig:auto-loop-annot}
\vspace{-0.2in}
\end{figure}

\subsection{Limitations}
\Arch\ is neither sound nor complete.  The false positives we have
experienced fall into two major categories.  First, symbolic execution
is slow, which may cause the kernel to print warnings. In addition,
driver timers may fire at the wrong time causing the driver to behave
differently and report warnings.  Second, the quality of the checkers
is important.  If a checker verifies an execution property
incorrectly, then it will mistakenly report a bug even though the
driver is correct. Our current checkers have no known bugs, and 
we have not seen them generate false positives.


Although we have observed no false negatives among the checkers we
wrote, \Arch\ cannot check for all kinds of bugs.  Of 11 common
security vulnerabilities~\cite{chen:linux-vuln:apsys:2011}, \Arch\
cannot detect integer overflows and data races between threads, though
support for overflow detection is possible in principle because the
underlying VMM interprets code rather than executing it directly.  In
addition, \Arch's aggressive path pruning may terminate a path that
leads to a bug, causing \Arch\ to miss it. \Arch\ may also miss race
conditions, such as those requiring the interrupt handler to
interleave with another thread in a specific way.  Despite these
limitations, we find the tool to be a useful addition to the driver
development and patching process.
