\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 execute more than 1,000
branches on hardware-specific details. 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. This strategy works best for
small functions, where a successful path through the function is
short.

% 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 in some
network drivers to select paths where the carrier is on, which enables
execution of the driver's packet transmission code.

In order to focus symbolic execution on the driver, the \tf\
prunes paths when control returns to the kernel successfully. 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 and 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.

Loops are challenging for symbolic execution because each iteration
may fork new paths.  \see\ provides an ``EdgeKiller'' plugin that a
developer may use to terminate complex loops early, but requires
developers to identify each loop's offset in the driver
binary~\cite{ckc12} and hence incur substantial developer effort.

\Arch\ addresses loops explicitly by prioritizing paths that exit the
loop quickly.  Suppose an execution path \textit{A} enters a loop,
executes it once, and during this iteration more paths are created.
If path \textit{A} does not exit the loop after one iteration, \Arch\
executes it for a second iteration and, unless it breaks out early,
deprioritizes the second iteration because it appears stuck in the
loop.  \Arch\ then selects some other path \textit{B} that path
\textit{A} forked, and executes it.  \Arch\ repeats this process until
it finds a path that exits the loop.  If no paths exit the loop
promptly, \Arch\ selects some path arbitrarily and prioritizes it on
each subsequent iteration, in the hope that it will exit the loop
eventually.  If this path still does not exit the loop within 20
iterations, \Arch\ prints a warning about excessive path forking as
there is no evident way to execute the loop efficiently without manual
annotation.

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.  Moreover, loops
that produce a value, such as a checksum calculation, cannot exit
early without stopping the driver's progress. However, 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.


% 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\ terminates all paths that
return to the kernel in order to focus execution within the
driver. In addition, 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 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 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 in order to execute code that requires specific inputs from the
kernel or applications.  \Arch\ can automatically make a Linux
driver's module parameters symbolic, executes the driver 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, and can be compared using the
\codesm{diff} utility.  \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.
