\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.  For each kernel function the driver
imports, \ds\ generates a stub function with the same signature that
wraps the function.

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.}
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\ also 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 verifies a checksum over EEPROM, and we modified it to
accept any checksum value.  We have found these cases to be rare.


\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}
