\documentclass{book}

\usepackage{hevea}
\usepackage{graphicx}       % for includegraphics

%\begin{latexonly}
%\ifx\pdfoutput\undefined
%  \usepackage{hyperref}
%\else
%  \usepackage[pdftex]{hyperref}
%\fi
%\end{latexonly}

\usepackage{color}

% deputy.version.tex is generated automatically to define \deputyversion 
% and \deputyversion
\include{deputy.version}

\renewcommand\t[1]{{\tt #1}}
\newcommand\codecolor{\ifhevea\blue\else\fi}
\renewcommand\c[1]{{\codecolor #1}} % Use for code fragments
\newcommand\SAFE{\t{SAFE}}
\newcommand\BND{\t{BND}}
\newcommand\NTS{\t{NTS}}
\newcommand\COUNT{\t{COUNT}}
\newcommand\AUTO{\t{\_\_auto}}
\newcommand\THIS{\t{\_\_this}}

\newcommand\RTTI{\t{RTTI???}}
\newcommand\SEQ{\t{SEQ???}}
\newcommand\FSEQ{\t{FSEQ???}}
\newcommand\WILD{\t{WILD???}}

\newcommand\TODO[1]{{\ifhevea\red\else\fi TODO: #1}}
\newcommand\secref[1]{Section~\ref{sec-#1}}
\newcommand\chref[1]{Chapter~\ref{ch-#1}}
\newcommand\appref[1]{Appendix~\ref{ch-#1}}

%%% Define an environment for code
%% Unfortunately since hevea is not quite TeX you have to use this as follows
%\begin{code}
% ...
%\end{verbatim}\end{code}
\def\code{\begingroup\codecolor\begin{verbatim}}
\def\endcode{\endgroup}

%
% \begin{deputycode}...\end{deputycode} is taken care by deputycode.pl
%

%use this for links to external pages.  It will open pages in the
%top frame.
\newcommand\ahreftop[2]{{\ahref{javascript:loadTop('#1')}{#2}}}



% Make sure that most documents show up in the main frame,
% and define javascript:loadTop for those links that should fill the window.
% Use BEGIN/END IMAGE to make sure that makeatletter/makeatother
% appear in the image file too.
%BEGIN IMAGE
\makeatletter
%END IMAGE 
\let\oldmeta=\@meta
\def\@meta{%
\oldmeta
\begin{rawhtml}
<base target="main">
<script language="JavaScript">
<!-- Begin
function loadTop(url) {
  parent.location.href= url;
}
// -->
</script>
\end{rawhtml}}
%BEGIN IMAGE
\makeatother
%END IMAGE 

        
\begin{document}
\begin{latexonly}
\title{Deputy \deputyversion: User Manual}
\end{latexonly}
\maketitle

\chapter{Introduction}

 \emph{This version of the document refers to Deputy {\deputyversion} 
       and was last modified on \today. This document is also available in 
       \ahref{DEPUTY.pdf}{PDF format}}


Deputy is a source-to-source translator for C. It analyzes the C program to
determine the smallest number of run-time checks that must be inserted in the
program to prevent all memory safety violations. The resulting program is
memory safe, meaning that it will stop rather than overrun a buffer or
scribble over memory that it shouldn't touch. ...

 Deputy relies on a lightweight system of annotations on pointer types. The
programmer must supply the annotations for all global pointers (function
arguments and returns, structure fields, types of global variables) and Deputy
will attempt to infer the annotations for local variables and for type casts. 

 The Deputy itself is written in Ocaml (a dialect of ML). There is also a
Perl script, \c{deputy}, that operates as a drop-in replacement for 'gcc', so
that software packages' existing Makefiles can be used with very minor
changes. 
 
 Deputy is implemented on top of the \@print{<a target="\_blank"
href="../cil/index.html">CIL framework</a>}. for analysis and transformation
of C programs. CIL allows the quick development of program analysis
modules that works on ANSI C code as well as on code that uses the GNU C
extensions.

  If you are anxious to see Deputy in action you can try out our 
\@print{<a target="\_blank" href="web/index.html">online demo</a>}.

 In this manual you can find a tutorial on getting started with Deputy
(\chref{tutorial}), documentation for all of the features (actually some of
the more researchy features are not yet fully documented) and step-by-step
accounts on what it takes to use Deputy on several example programs
(\chref{examples}). We suggest that you read the chapters in order and go to
the ``Advanced Deputy Features'' only if you need it. The \chref{warn} (Deputy
Warnings and Errors) will help you figure out if you are running into an error
that is covered by an advanced feature.

\section{Authors}

 Deputy was developed primarily by
\ahref{mailto:jcondit@cs.berkeley.edu}{Jeremy Condit},
\ahref{mailto:matth@cs.berkeley.edu}{Matthew Harren} and
\ahref{mailto:necula@cs.berkeley.edu}{George Necula}. 
Other people helped with
various components: ...

 This work was supported in part by the National Science Foundation under
Grants No. ???, and gifts from Microsoft Research. Any opinions, findings, and
conclusions or recommendations expressed in this material are those of the
author(s) and do not necessarily reflect the views of the National Science
Foundation or the other sponsors.

        \chapter{Installation}\label{ch-start}

 Deputy works on Linux and MS Windows (for now only with cygwin).

 Deputy is somewhat sensitive to the version of the compiler that you are
using. More precisely, Deputy is sensitive to the format of the system include
files that you are using. When you install Deputy it will create slightly
modified copies of some of the system include files. These copies are created
based on some patches that we distribute with Deputy. If your include files
are different from those that we used to create the patches then the Deputy
installation might fail. At the moment we have tested Deputy with the
following compilers:

\begin{itemize}
\item On Windows, using \c{cygwin} and \c{gcc} version 3.4.4.
\item On Linux, using \c{gcc} version 3.4.4
\end{itemize}

 If you want to use Deputy on Windows then you must get a complete
installation of \c{cygwin} (make sure you install the development tools such
as \c{gcc} and \c{ld} as well and the \c{perl} interpreter) and the {\bf
source-code} Ocaml distribution and compile it yourself using the cygwin tools
(as opposed to getting the Win32 native-code version of Ocaml). You will need
Ocaml release 3.08 or higher to build Deputy. If you have not done this before
then take a look \ahref{../ccured/setup.html}{here}. (Don't need to worry
about \c{cvs} and \c{ssh} unless you will need to use the master CVS
repository for Deputy.)

\section{Get the Deputy sources}

 Download the Deputy \ahref{distrib}{distribution} (latest version is
\ahrefurl{distrib/deputy-\deputyversion.tar.gz}). See the \secref{changes} for
recent changes to the Deputy distribution.

 If you are one of the Deputy developers you can ask Jeremy Condit
(\mailto{jcondit@cs.berkeley.edu}) for an account that allows you to use the
master CVS repository on \c{manju.cs.berkeley.edu}. Assuming you have already
setup \c{cvs} and \c{ssh} as discussed in \ahrefurl{cvssetup.html}, you can
check out the sources in a subdirectory \c{deputy} as follows:

\begin{verbatim}
  % cvs -d :ext:jcondit@manju.cs.berkeley.edu:/home/cvs-repository checkout deputy
                ^^^^^^^
         use your username instead
\end{verbatim}

\section{Configure and Compile Deputy}

 Run the following commands in the top level directory. If you are using
Windows then at least the \c{configure} command must be run from within
\c{bash}. 
\begin{verbatim}
./configure
make
make quicktest (optional)
\end{verbatim}

 The \c{configure} script tries to find appropriate defaults for your system.

 It is possible that you get a configuration error saying that certain patterns
did not match. This means that your standard include files are different than
those that we have prepared the distribution for. (See the above discussion.)
Your recourse in this case is either to install one of the versions of the
compiler that we tested Deputy for or to extend the patch files so that they
match your includes. It is not hard, and it is explained in the
\ahref{../cil/patcher.html}{patcher} documentation.

 After running \c{make} you have built a few executables (in the \c{obj}
directory) and have configured the \c{bin/deputy} Perl script. If you want to
move this script to another directory (e.g. to \c{/usr/local/bin}) make sure
to copy the \c{DeputyConfig.pm} file to the same directory. 

 Now you can continue with a tutorial (\chref{tutorial}), or you can jump
ahead and find out how to run Deputy (\chref{invoke}).

\section{Test Deputy}
 
  Once you have built Deputy you can run 
\begin{verbatim}
make quicktest
\end{verbatim}

  This will run a few small examples. If you want to test Deputy on a large
part of our own regression suite you need to do the following:
\begin{itemize}
\item In the \t{test} directory, run
\begin{verbatim}
runtests --run
\end{verbatim}

 See \secref{regtest} for details on how to use the regression tester.

\end{itemize}


\chapter{Deputy Tutorial}\label{ch-tutorial}\cutname{tutorial.html} 

 Deputy is an extension of the C programming language that distinguishes among
various kinds of pointers depending on their usage. The purpose of this
distinction is to be able to prevent improper usage of pointers and thus to
guarantee that your programs do not access memory areas they shouldn't access.
You can continue to write C programs but Deputy will change them slightly so
that they are type safe. In this chapter we explain in what situations will
your program be changed and in which way. 

 Deputy leaves unchanged code that does not use pointers or arrays. Actually,
Deputy is implemented on top of the C Intermediate Language (CIL)
infrastructure, which means that C programs are first translated into a subset
of the C language that has simple semantic rules. The following are some of
the transformations that are performed:
\begin{itemize}
\item C expressions and statements are separated into expressions (no
side-effect and no control-flow), instructions (assignments and function
calls, with one side-effect and no control-flow) and statements (the
control-flow constructs). This means that CIL serializes the side-effects and
the control-flow. 
\item All type and structure declarations are moved to the beginning of the
file. 
\item The scope of variables is resolved and local variables are renamed
accordingly. All local variables are moved to function-scope and are declared
at the beginning of the function body. The initialization for such variables
is done using explicit assignment instructions.
\item Anonymous structures and unions are given unique names. 
\item All implicit casts and conversion are expressed as explicit casts.
\item All GNU CC extensions are compiled into regular C code. 
\end{itemize}

 For a complete description of the CIL infrastructure see
\ahref{../cil/index.html}{the CIL documentation}.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
     \section{Deputy Annotations}\label{sec-typeannot}

 The most significant difference between C and Deputy is that Deputy pays
close attention to how pointers are manipulated and it classifies pointers
into various kinds according to what you do with them. We'll discuss the
various kinds starting in the next section but before that we need to
introduce an important notation that you can use to communicate to Deputy
which pointer kinds you want for your pointers.

 Deputy uses type attributes to express the kind of pointers. Type attributes
exist in a limited form in ANSI C (i.e. the \c{volatile}, \c{const} and
\c{restrict} type qualifiers) and in a richer form in the GCC dialect of C.
Deputy, just like GCC, allows any attributes to be specified for types, names
of variables, functions or fields, and for structure or union declarations.
Unlike GCC, Deputy has precise rules for how attributes are interpreted in a
declaration (instead GCC relies on knowing the semantics of the attribute in
order to associate it with the proper element of a declaration). The rule of
thumb is that the attribute of a pointer type is written immediately {\bf
following} the \c{*} pointer-type constructor and the attribute of a name is
written immediately before the semicolon or the \c{=} sign that terminates the
declaration of the name. Deputy uses pointer-kinds such as \SAFE{}, \NTS{} and 
\BND{} and the corresponding attribute use the same names. For example, in the following declaration:
\begin{deputycode}[]
int * NTS * SAFE x; 
\end{deputycode}

 the type of \c{x} is declared to be a \SAFE pointer to a null-terminated C
string (\NTS). Just like pointer-types in C, attributes are read from
right-to-left. The \c{SAFE} attribute in this case applies to the pointer-type
of \c{x}. 

  (The complete attribute-parsing rules for CIL are described in the
\ahref{../cil/attributes.html}{CIL manual}.)

 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \section{\SAFE{} pointers}

 The main action in Deputy concerns the features that endanger type safety in
C: pointer, arrays, union types, and variable argument functions. Pointers in
C can be assigned to l-values, dereferenced, subject to pointer arithmetic and
cast to other pointer or non-pointer types. In contrast, pointers in a typical
type-safe language (e.g. Java, Basic, ML) cannot be subject to arithmetic or
(arbitrary) casts. Deputy allows (almost) all the pointer operations that C
allows but gives preferential treatment to pointers that are not subject to
arithmetic or to casts. Deputy refers to such pointers as \SAFE{} pointers.

 Consider for example this small code-fragment that computes the length of a
linked list:
\begin{deputycode}[]
struct list { 
   int car; 
   struct list * SAFE cdr; 
};

int length(struct list * SAFE l) {
  int i = 0;
  while(l) {
    l = l->cdr; 
    i ++;
  }
  return i;
}
\end{deputycode}

 The only pointers used in this code fragment are pointers to list cells and
they are not subject to arithmetic or to casts. In fact, this code fragment
can be transcribed literally into Java or C\#. You can see in the output of
Deputy that the pointer dereferences contain only \TODO{what? There are
  actually no checks} checks.

\paragraph{Properties of \SAFE{} pointers}
 The \SAFE{} pointers are the ``best'' kind of pointers, meaning that they
incur the least amount of run-time cost. Here is a list of the properties of
\SAFE{} pointers:
\begin{itemize}
\item Cannot be subject to pointer arithmetic (adding or subtracting an
integer from it).
\item Cannot be cast (except subject to stringent rules which we'll discuss
below). Note that assignment, passing actual arguments and returning are
implicit casts. 
\item Can be set to a compile-time constant equal to 0 but not to any other
integer expression.
\item Can be cast to an integer and can be subtracted from another pointer.
This is useful for comparisons.
\item \SAFE{} pointers are represented using the standard C representation
using one word. 
\item Every time a \SAFE{} pointer is dereferenced, a null check is inserted
before the dereference. 
\end{itemize}

 All of these restrictions are such that the following invariant holds for all
\SAFE{} pointers:
\begin{center}\bf
A \SAFE{} pointer to type \c{T} is either 0 or else it points to a valid area
of memory containing an object of type \c{T}. Furthermore, all other pointers
to the same area agree on the type \c{T} of the stored object.
\end{center}


%  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%5
%  \subsection{Safe Casts}
%
% Casting a pointer to an integer is always allowed. Deputy does actually allow
%certain other casts on \SAFE{} pointers. For example it is safe to cast a
%pointer to a structure containing two integers into a pointer to integer. In
%general it is safe to cast a pointer to a long structure into a pointer to a
%short structure as long as the two structures agree on the types of the
%elements in the overlapping portion. Deputy is actually quite liberal about
%these rules and will think of nested combinations of structures and arrays as
%one big structure with non-structure and non-array fields. This feature is
%called {\em physical subtyping}. For example, in the code shown below, all of
%the four casts implicit in the assignments are safe and Deputy will infer that
%all pointers involved are \SAFE{}.
%
%\begin{deputycode}[]
%struct large {
%  struct small {
%      int * SAFE f1;
%      int * SAFE f2; 
%  } a;
%  int * SAFE f3;
%} x;
%
%struct small * SAFE s1 = & x;
%int *  SAFE  * SAFE s2 = & x;
%struct large1 { int * SAFE a1, * SAFE a2, * SAFE a3; } * SAFE s3 = & x;
%struct large2 { int * SAFE a1, * SAFE a2[2];   } * SAFE s4 = & x;
%\end{deputycode}
%
% Notice that all of the \c{s1}, \c{s2}, \c{s3} and \c{s4} are aliases for the
%address of \c{x} but they agree on the type of the object pointed to.
%
% Following are two examples of casts that are not allowed (for \SAFE{}
%pointers; you can see that Deputy infers the \WILD{} kind for the pointers
%involved) \TODO{what we need to say here. Deputy allows this}:
%\begin{deputycode}[]
%int y1;
%int * * x1 = & y1; // Cast an int * to a int * *  
%int y2;
%struct large { int * a1, a2; } * x2 = &y2;
%\end{deputycode}
%
%  If the first cast were allowed then by writing to \c{y1} an arbitrary
%integer we would be invalidating the assumption that \c{x1} points to a
%pointer value. The second cast is similar. 


 %%%%%%%%%%%%%%%%%%%%%%%%%%
 \subsection{\SAFE{} Function Pointers}

 There is nothing special about function pointers. They can be safe provided
that they are not cast to incompatible pointer types. A function pointer type
is compatible only with another function pointer type with the same number and
type of arguments and the same result type. 

 A common problem with function pointers (and functions) in Deputy is if your
program uses external function without prototypes. This makes Deputy think
that the function is taking no arguments and returning an integer and every
time you use it in a different way Deputy behaves as if you are casting the
function pointer (denoted implicitly by the function's name) to the type
needed in the cast. Deputy will give errors when you are using 
using functions without
prototype and we recommend that you fix those problems and try Deputy again.


 %%%%%%%%%%%%%%%%%%%%%%%%%\
 \section{Checks for \SAFE{} Pointers}

 As we mentioned above, every time a \SAFE{} pointer is dereferenced it must be
checked whether it is null or not. We know from the invariant for \SAFE{}
pointers that non-null pointers can be dereferenced and we can count that the
value read through them has the type given by the pointer type. 

 A null check appears in the output of Deputy as a call to the function
\c{CNonNull}. This and other run-time checking functions used by Deputy have a
name that starts with the prefix \c{C} and are declared in the file
\ahrefurl{include/deputy/checks.h}. You will see in that file that most of
these functions are declared inline.

 Checking for null pointers is necessary not just when reading or writing
through them but also when they are used to compute the address of a subobject
of the object they point to. For example, in the following code Deputy will
add a run-time check that \c{s} is not null before computing the value of
\c{x}. Then again there will be a check that \c{x} is not null before
dereferencing it.
\begin{deputycode}[]
struct str  {
   int a, b;
};

int getaddr(struct str * SAFE s) { 
   int * SAFE x = & (s->b);
   return *x;        
}
\end{deputycode}

 The first check in the code above is necessary to enforce the invariant that
\SAFE{} pointers are either 0 or else valid pointers. Without that check the
value of \c{x} would be 4 (on most machines) which would break the invariant
and would defeat the second null-check\TODO{How come there is no run-time
  check on *x? We should explain.}  thus letting you dereference an invalid
pointer. 

 At this point you are starting to see some of the subtleties in the design of
Deputy. To ensure that we got everything right we have formalized the type
system of Deputy and we proved (for a subset of Deputy) that the set of
run-time checks and invariants achieve memory safety.

 Deputy includes a simple optimizer that tries to eliminate redundant
checks and checks that cannot possibly fail (such as checking that the address
of a global variable is non-null). Currently the optimizer is fairly naive.
For example, it does not know that since \c{s} is a non-null \SAFE{} pointer
to \c{struct str} then \c{\&(s->b)} is guaranteed to be non-null as well, thus
the second check is not really necessary.\TODO{It might actually already know
that.}  

 Speaking of too many checks, some of the more experienced C programmers
will have noticed that our run-time checks prevent a common idiom for computing
the offset of fields in structures. The typical code for doing that is shown
below (as is defined as the macro \c{offsetof} in many C libraries):
\begin{deputycode}[]
struct str  {
   int a, b;
};

int get_offset_of_b() {
  return (int) &(((struct str*)0)->b);
}
\end{deputycode}

 Deputy recognizes in this specific case that you are casting the result of
the \c{\&} operator to an integer, so it avoids the run-time check.\TODO{Does
  Deputy recognize this? It should.} 

 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
      \section{Pointer Arithmetic}

 So far we have discussed pointers for which we disallow most casts and
pointer arithmetic. In this section we will generalize \SAFE{} pointers to
allow pointer arithmetic, while allowing for static and run-time checks
against buffer overrun. The cost that the programmer pays for using these more
capable pointers is that each dereference will be accompanied by bounds
checks.

\TODO{I am trying to add the checks one by one}
 Consider the following code fragment. The pointer \c{x} cannot be \SAFE{}
because adding \c{delta} to it is not guaranteed to yield a meaningful result.
Instead, we declare \c{x} as a pointer to at least 8 integers.
\begin{deputycode}[]
int increment(int * COUNT(8) x, int delta) {
  return (int)(x + delta);
}
\end{deputycode}

  You can see in the Deputy output for the above example that Deputy first
checks that \t{x} is not null, and then adds a series of checks. First, there
are checks that ensure that \c{x + delta} does not overflow (\c{COverflow}),
and it remains within the declared bounds (two instances of \c{CUnsignedLE}). 

  Deputy also inserts checks on assignment of pointer to buffers:
\begin{deputycode}[]
int index(int * COUNT(count) x, int count) {
  int * COUNT(2) y = x;
  return *y;
}
\end{deputycode}

 We see that Deputy requires that either \c{x} is null, or else \c{x} $\leq$ x
$\leq$ \c{x + 2} (check \c{CNullOrLE}) to ensure that after the assignment
\c{y = x} we establish the invariant required for $y$. (The last check in the
above example is due to the reading from \c{y}; only a null check is needed
since we know that if \c{y} is not-null it is safe to read from it.)

 Now we can put together the arithmetic check and the coercion check:
\begin{deputycode}
int index (int * COUNT(count) x, int count) {
  int * COUNT(1) y = x + 2;
  return *y;
}
\end{deputycode}

\TODO{How come we do not have an overflow check above? What if x + 2 overflows?}

\subsection{Bounded Pointers}

 The most general form of bounded pointers uses the \BND{} annotation, with
two expressions denoting the start (inclusive) and the end (exclusive) of the
memory area pointed-to by a pointer. 

 For example, in the following program \t{x} is declared to be either null, or
 larger or equal to \t{b} and less than \t{b + 8}: 
\begin{deputycode}
int foo(int * BND(b, b + 8) x, int * b) {
    return x[3];
} 
\end{deputycode}

 In fact, the \SAFE{} and \COUNT{} annotations described before are just
special cases of \BND{} annotations:
\begin{verbatim}
#define COUNT(n) BND(__this, __this + (n))
#define SAFE     BND(__this, __this + 1)
\end{verbatim}

\subsection{Invariants for bounded pointers}
\begin{itemize}
\item Cannot be cast (except subject to stringent rules which we'll discuss
below). Note that assignment, passing actual arguments and returning are
implicit casts. 
\item Can be subject to pointer arithmetic (adding or subtracting an
integer from it). 
\item Can be cast to an integer and can be subtracted from another pointer.
This is useful for comparisons.
\item Every time a bounded pointer is dereferenced, both a check that the
pointer is not null and a bounds check are inserted.
\end{itemize}

\begin{deputycode}
extern void* (DALLOC(sz) malloc)(unsigned int sz);
int foo(int x) {
  int * COUNT(8) p, * COUNT(16) r1, * COUNT(8) r2;
  int a[8];

  r1 = (int*)malloc(16);
  r2 = a;
  p = r1; 
  p = r2;
  return *(p + x); 
}
\end{deputycode}

The invariant for a pointer \t{p} with type \t{T * BND(b,e)} is that it is
either null, or else there exists a valid allocation area starting at \t{a},
containing \t{n} elements of type \t{T}, and $\t{a} \leq \t{b} \leq \t{p} \leq
\t{e} \leq \t{a + n}$. Furthermore, \t{b}, \t{p} and \t{e} are aligned with
respect to the start of the allocation area and the type \t{T}. 

\subsection{Run-time checks for bounded pointers}\label{sec-checkseq}

 Every time we dereference a bounded pointer, we must check that it is
non-null and it is not equal to the declared upper bound.  

Also, for a pointer arithmetic operation we check that the pointer is
non-null and after the operation is stays in the same area as the original
pointer. 

 For example, in the following code we must check that the operation \t{x + i}
results in a pointer withing the declared bounds of \t{x}. 
\begin{deputycode}
int foo(int * BND(b, b + 8) x, int * b, int i) {
  int * BND(b, b + 8) p = x + i;
  return *p;
}
\end{deputycode}

 An interesting situation is when we assign bounded pointers:
\begin{deputycode}
int foo(int * BND(b, b + 8) x, int * b, int * e, int i) {
  int * BND(e, e + 2) p = x + i;
  return *p;
}
\end{deputycode}


% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       \section{Auto Bounds}

 Deputy allows the programmer to control a mechanism for inferring the bounds
of pointers. To invoke this mechanism, you can use the keyword \AUTO{} in
place of one or both of the arguments of the \BND{} annotation. When seeing
such an annotation the 
\begin{itemize}
\item If \AUTO{} appears in the type of a local variable, a formal argument,
  or a cast, Deputy will create a local variable (or formal argument) for the
  corresponding bound and will insert code to track its value
\begin{deputycode}
int foo(int * COUNT(n) p, int n) {
  int * x;
  if(*p) {
    x = p;
  } else {
    x = p + 2;
  }
  return *x;
}
\end{deputycode}

  This local use of \AUTO{} is entirely safe, and in fact Deputy will use tihs
  feature for all local variables and casts that do not have bounds
  annotations. 

\item If \AUTO{} appears in the return type of a function, the type of a
  global variable, the type of a field, or the base type of a pointer type,
  then the annotated pointer type is transformed into a ``fat'' structure with
  new fields to carry the necessary data:
\begin{deputycode}
struct foo {
   int * BND(__this, __auto) fseq;
} p;
int array[8];
int main() {
  p.fseq  = & array[2];
}
\end{deputycode}

  Here is an example with \AUTO{} in the return type of a function:
\begin{deputycode}
int array[8];
int * BND(__this, __auto) getints(void) {
  return & array[2];
}
\end{deputycode}

Such uses of \AUTO{} are dangerous because they change the representation of
data in a way that is visible from other functions. To prevent you from
accidentaly mixing deputized and native versions of the same globals, Deputy
will change the name of globals (or functions) whose representation (or
calling convention) changes.

\end{itemize}


% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       \section{Default Annotations}

 If a pointer is missing bounds annotations then Deputy will add its own
 annotation as follows:
\begin{itemize}
\item If this is a cast or the type of a local variable it adds \BND(\AUTO,
  \AUTO), in essence demanding the creation of local variables to track the
  bounds. 
\item In all other cases, Deputy adds the annotation \SAFE. 
\end{itemize}

% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       \section{String Pointers}

The C idiom of using a character pointer for passing character strings
is so ubiquitous that Deputy has a specialized kind of pointer qualifier
for this usage, called \TODO{??}.


%Conceptually, a string pointer is just like an \FSEQ{} pointer, except the
%end-pointer is implicitly stored in the string data itself, rather than
%alongside the main pointer.  In particular, the memory pointed-to is
%declared to be an array of characters, and is always used in a way
%consistent with that declaration.
%
%String pointers maintain the invariant that (unless \c{NULL}) they always 
%point within a valid array of characters, and there is always a 0 byte
%just beyond the end of the array.
%
% String pointers can be converted to \FSEQ{} pointers using an invocation of
%the 
%\begin{deputycode}
%int foo(char __RWSTRING *s) {
%  char * __FSEQ x = s;
%}
%\end{deputycode}
% 
%
%The 0 byte beyond the end cannot be changed by the program, whether through
%a string pointer or through another kind of pointer.  Other kinds of
%pointers will have their metadata arranged to prevent writing the 0.
%Strings are never allowed to overwrite \emph{any} 0 byte they encounter
%(because it could be the last one).
%
%To guarantee the existence and immutability of the 0 byte, every occurrence
%in the program of the type ``array of characters of length $n$'' is
%rewritten to be ``array of characters of length $n+1$''.  But, this happens
%after boxing, so all pointer metadata continues to disallow access beyond
%the $n$th byte, hence the 0 byte is protected.  Further, any call
%to \c{malloc} requesting $n$ bytes gets at least $n+1$ bytes of data, all
%initialized to zero (a possible improvement is to allocate the extra
%byte more selectively, only when a string pointer will point to the memory
%being allocated).
%
%One problem with this scheme is the program might ask for the size of an
%array using \c{sizeof}.  Since the length has changed, \c{sizeof} will
%return $n+1$, which is now an observable consequence of translation.  To
%partially mitigate this, any occurrence of ``\c{sizeof($e$)}'' where $e$ has
%type ``array of characters'' is rewritten to be ``\c{(sizeof($e$)-1)}''.
%This rewriting does not look inside structure types, for example, so it does
%not completely hide the effect.  However, it has proven sufficient for
%the programs translated so far.
%
%All of the rewriting described in this section is done by the
%\c{expandCharArrays} visitor in \c{box.ml}.


 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Safe Union Types}\label{sec-union}
 
Union types are another potential source of unsoundness in C programs.
Deputy supports {\em tagged unions}, in which a tag value near the
union denotes which field of the union is ``active''.  These
tags are already present in most C code; Deputy enforces them in a
type-safe way.

The following example shows the most common form of a tagged union: a
union and its tag together in a struct.  In this program, the tag
\c{x.tag} is used to determine the active field of union \c{x.data}.

\begin{deputycode}[]
enum tagValues { ZERO, ONE, TWO, THREE };
struct twothings { int a; int* p; };

struct variant {
  enum tagValues tag;
  union un { 
    int f1                WHEN(tag == ONE);
    int * SAFE f2         WHEN(tag == TWO);
    struct twothings f3   WHEN(tag == ZERO || tag == THREE);
  } data;
} x;

int foo() { 
  return x.data.f1; 
}
\end{deputycode}

Tags are defined by annotating each union field with \c{WHEN($exp$)}
where \c{$exp$} is a boolean expression that is true when the field is
active. \c{WHEN} conditions can contain integer arithmetic and
comparisons, and they can depend on one or more names in the same
context as the union.  So if a local variable has union type, its
\c{WHEN} clauses can depend on other locals, while a union type used
as a struct field (by far the most common case) can depend on other
fields of the struct.  
\TODO{Make sure this matches the terminology (e.g. ``contexts'')
that's used in the discussion of pointer dependencies.}

You must ensure that the \c{WHEN} annotations are disjoint.  That is,
no two fields should be ``selected'' at once.  Deputy does not yet check
this statically, so it's a runtime error to use a tag value that
selects more than one field.

There are three key rules when using tagged unions:
\begin{itemize}
\item Whenever you read from or write to a field, Deputy will check that
  the tag value(s) satisfy the \c{WHEN} clause for that field.
\item Whenever you change a tag value, the entire union must first be
  zeroed.  Doing this ensures that the new active field can be
  immediately read; a pointer field will be \t{NULL}, which is always
  valid for a pointer type.
\item You may not take the address of a union field.  (This would be
  unsound, if the pointer to the field was used after the tag changed.)
\end{itemize}

If you want to change the value of both a union and a tag, you should
do the following.  This is analogous to the procedure for changing
dependent pointers, in which you must usually zero the pointer before
changing the length.
\begin{enumerate}
\item Zero the entire body of the union (\c{memset} is easiest).
\item Change the tag(s) as desired.
\item Set the newly-active union field to the new value.
\end{enumerate}

\begin{deputycode}[]
#include <string.h>

enum tagValues { ZERO, ONE, TWO, THREE };
struct twothings { int a; int* p; };

struct variant {
  enum tagValues tag;
  union un { 
    int f1                WHEN(tag == ONE);
    int * SAFE f2         WHEN(tag == TWO);
    struct twothings f3   WHEN(tag == ZERO || tag == THREE);
  } data;
} x;

int setData(int new_a, int* new_p) {

  memset(&x.data, 0 , sizeof(x.data));
  //It is now legal to change x.tag to any value

  x.tag = THREE;
  //x.data.f3 is now the active field of x.data.

  x.data.f3.a = new_a;
  x.data.f3.p = new_p;
  return *x.data.f3.p;
}
\end{deputycode}



\subsection{Non-pointer fields}

For the sake of type safety, you must provide a \c{WHEN} annotation
for a field whose type contains a pointer.  But these annotations are
optional for fields that don't involve pointers.  Deputy allows reads
from unannotated fields regardless of the tag value, which is sound
because Deputy's type safety invariants apply only to pointers, not
integers.

This union contains no pointers, so it can be left completely
unannotated.  In fact, the programmer may very well be intending to
write to one field but read from another.
\begin{code}
typedef union _LARGE_INTEGER {
  struct parts {
    ULONG LowPart;
    LONG HighPart;
  } u;
  LONGLONG QuadPart;
} LARGE_INTEGER;
\end{verbatim}\end{code}

If you want to avoid accidentally confusing the fields of this union,
you can always choose to annotate it.  If \c{WHEN} clauses are used,
they will be enforced even though memory safety doesn't require it.

One common use of this rule is unions that have both integer and
pointer fields, where the program may want to write to a pointer field
but read from the integer field.  In this case, you can leave the
integer field unannotated to indicate that all reads through that
field are allowed.  Of course, it's illegal to write to the unannotated
field if any annotated field is currently selected.

\begin{deputycode}[]
enum tagValues { ZERO, ONE, TWO, THREE };
struct twothings { int a; int* p; };
extern int hash(int z);

struct variant {
  enum tagValues tag;
  union un { 
    int hashcode ;        // No WHEN annotation
    double * SAFE f1      WHEN(tag == ONE);
    int * SAFE f2         WHEN(tag == TWO);
    struct twothings f3   WHEN(tag == THREE);
  } data;
};

int hash_of_variant(struct variant* x) {
  // Reading x->data.hashcode is legal no matter which field of
  // the union is selected.
  return hash(x->data.hashcode);
}

void write(struct variant* x) {
  //This will fail at runtime if x->tag is 1, 2, or 3! 
  x->data.hashcode = 0xdeadbeef;
}
\end{deputycode}

\subsection{Trusted unions}

If you want to ignore the unsoundness of a union that contains
pointers, or if you've convinced yourself that the union is used in a
sound way, you can mark the union as \c{TRUSTED}.  Deputy will do no
checking of trusted unions, and will allow you to take the address
of union fields.

You can place the \c{TRUSTED} annotation after either the word
\c{union} or the closing right brace.

\begin{deputycode}[]
union TRUSTED afl { 
  double f1;
  int * SAFE f2;
} data1;

//This is an equivalent placement of TRUSTED:
union cio { 
  double f1;
  int * SAFE f2;
} TRUSTED data2;

int* SAFE * SAFE intpp;

void unsound() {
  intpp = &data1.f2;
  data1.f1 = 3.14159;
}
\end{deputycode}



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\chapter{Not-Yet Documented Features}

\TODO{This section contains only reminders of features to document}
\begin{itemize}
\item When you take the address of an element into an array, the inferred
  pointer type refers to the whole array. In other words ``\& array[idx]''
  behaves exacly like ``array + idx''.
\end{itemize}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\chapter{Invoking Deputy}\label{ch-invoke}

\TODO{this section}
 
 Deputy consists of several components: an Ocaml application that does the
main work, a set of Perl scripts that are used to invoke the Deputy
application, and a set of header and run-time library files. 

 The easiest way to use Deputy is through the \c{bin/deputy} script. This
script is intended to be used in the same context and with the same
command-options as either the \c{gcc} compiler or the Microsoft Visual C
compiler (MSVC). This script is configured at installation time to know where
the rest of the Deputy installation resides. If you move this script to
another directory you must also make a copy in the new directory of the
\c{DeputyConfig.pm} file. 

 Since \c{deputy} is a drop-in replacement for \c{gcc}, for most software
projects you can reuse the regular build-infrastructure:
\begin{verbatim}
make mystuff CC="bin/deputy [options]"
\end{verbatim}

 Here is the sequence of actions that the \c{deputy} script performs:
\begin{enumerate}
\item It recognizes among the command-line arguments those that are intended
for the pre-processor; then, for each source file (i.e. with the extension
t{.c}), calls the preprocessor and places the result in a file with the
extension \c{.i} in the same directory as the source file.
\item For every \c{.i} file that it produces and that must be compiled (i.e.
the \c{-E} option was not specified to require only preprocessing) \c{ccured}
will save a copy of the file with the extension \c{.o}, thus ``fooling''
\c{make} that the object file was actually produced. 
\item Whenever \c{ccured} is invoked to link {\em into a library} a number of
\c{.o} files that are actually preprocessed sources saved in the previous
step, the Deputy engine will be invoked to parse all of the files and produce
a single \c{C} file with the same content but with names of types and
variables properly renamed. The output is then saved as the resulting library.
You should use the \c{--mode=AR} argument to Deputy if you want to pass the
remaining arguments as for the \c{ar} utility. More details about the merging
stage that Deputy used can be found \ahref{../cil/merger.html}.
\item Finally, when \c{ccured} is called to link {\em into an executable} a
number of object files and libraries it will separate from them those that are
actually saved sources and will merge them all in memory. The resulting file
is then subject to Deputy type inference followed by the insertion of run-time
checks. Optionally, an optimizer is invoked to try to clean up some of the
inserted run-time checks. The result is saved using the full name of the
desired executable with the suffix \c{ccured.c}. Finally this file is
preprocessed, compiled and linked using the underlying compiler. 
\end{enumerate}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%5
\section{Command-line options}\label{sec-commandline}

\TODO{this section}

 You always run Deputy with the command options of \c{gcc} (e.g., \c{-c} to
compile only, \c{-o} to specify the output file, etc.). Here are some common
ways to use invoke Deputy:
\begin{itemize}
\item \c{bin/ccured --nocure --nomerge hello1.c hello2.c -o hello.exe}
\hspace{1cm}- Compiles and links without curing and without merging (still
uses the CIL front-end)
\item \c{bin/ccured --nocure hello1.c hello2.c -o hello.exe}
\hspace{1cm}-Merges using CIL, then compiles and links with \c{gcc}
\item \c{bin/ccured hello1.c hello2.c -o hello.exe} \hspace{1cm}-Merges using
CIL, processes with Deputy, the compiles and links with \c{gcc}
\item \c{bin/ccured -c hello1.c hello2.c} \hspace{1cm}-Just put preprocessed source in the object files
\item \c{bin/ccured hello1.o hello2.o -o hello.exe} \hspace{1cm}-Take the
preprocessed source in the object file, merge, cure, gcc. 
\item \c{bin/ccured --mode=AR cr hello.a hello1.o hello2.o} \hspace{1cm}-Merge
the preprocessed source in the object files into an archive (which itself
contains source)
\item \c{bin/ccured hello.a main.c -o hello.exe}\hspace{1cm}-Preprocess the C
source, merge with the sources in the archive, cure and gcc. 
\end{itemize}

\TODO{I made a pass over the arguments}

 Most of the command-line options that you pass to \c{ccured} will be passed
along to the underlying preprocessor, compiler or linker. However the
\c{ccured} script recognizes the following special options:
\begin{itemize}
\item General options
\begin{itemize}
\item \c{--save-temps}. It tells the Deputy script to save the temporary files
  (including the output of Deputy).
\item \c{--mode=MSVC}. Use instead of the Microsoft Visual C compiler
(\c{cl}). Deputy and the CIL front-end know how to handle the MSVC extensions.
\item \c{--leavealone=foo}. Deputy will not merge and will not process the
file whose name starts with foo. Instead it will compile it as usual and will
link it in when needed. You can put in this file functions that you do not
want Deputy to see (e.g., if they are really ugly and you are ashamed of
what you did!). See \secref{trusted} for details.
\item \c{--stats}. Print some statistics about the inserted checks.
\item \c{--stages}. Print details about the various stages.
\item \c{--extrafiles=<xxx>}. Give the name of a text file that contains
whitespace-separated named of additional files to process (in case your
command lines are too long).
\item \c{--keepunused}. Disable the removal of apparently unused elements from
the file, such as local variables or prototypes.
\item \c{--noPrintLn}. Turns off the printing of line-number information. This
way the errors will be referenced to the Cured file not the source file.
\item \c{--commPrintLn}. Print line-number information as comments. This
way the errors that Deputy prints at run-time and the debugging information in
the cured code refer to the cured file, not the original source, but
you can still figure out from what file this is coming.
\item \t{--printCilAsIs}. Do not attempt to simplify the program while
  printing. If this is turned on, then all loops will be printed as
  ``while(1)'', as they are in the internal language.
\end{itemize}

\item Options controlling compile-time behaviour
\begin{itemize}
\item \c{--deputyverbose}. Print information about what Deputy is doing.
\item \c{--deputyinferout=foo}. Print in the file \c{foo} a version of the
  source that contains the information that Deputy has inferred.
\item \c{--deputyopt=n}. Choose the optimization level:
      \begin{itemize}
        \item \c{0} - no optimization. Not recomended because it leads to so
                      many checks that gcc is overwhelmed
        \item \c{1} - flow-insensitve optimizations.
        \item \c{2} - flow-sensitive optimizations. 
      \end{itemize}
\end{itemize}


\item Options controlling run-time behaviour
\begin{itemize}
\item \c{--deputyAlwaysStopOnError}. Generate code that always stops on error
       (slightly faster).
\item \c{--failIsTerse}. Do not print source-file location on failure. This
       makes your program smaller and faster.
\end{itemize}
\end{itemize}

 For most performance you should use the options:
\begin{verbatim}
--deputyopt=2 --releaselib --deputyAlwaysStopOnError --failIsTerse
\end{verbatim}

 All of the other options that start with \c{--} (and are not recognized as
compiler options) are passed unmodified to the Deputy Ocaml application.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Controlling error handling at run time}\label{sec-errorhandle}

 After you process a program you can run it as usual. If you have used the
\c{--deputyAlwaysStopOnError} flag to Deputy then the only option you have
when a check fails is to stop the execution. This assumption allows the
compiler to generate faster checking code. If you do not use that flag then by
default the program will print failure messages on standard error and the
execution will continue as if Deputy has not been used. \TODO{This would be a
nice property to have. I am not sure we have it though (e.g., unions)}

 Alternatively, you have the option to set the environment variable
 \c{DEPUTY\_ONERROR} to one of the following values.
\begin{itemize}
\item \c{warn} - warning messages are printed and the execution continues.
  This is as if you did not set the \c{DEPUTY\_ONERROR} variable. 
\item \c{stop} - execution stops on the first error, after printing the error
  message. This is almost as if you had specified
  \c{--deputyAlwaysSleepOnError} except that the program might be slightly
  slower. 
\item \c{ignore} - the failure messages are ignored (not even printed) and the
  execution continues. 
\item \c{sleep} - the program goes to sleep on an error. When it does so, it
prints the process id to standard error. You can then connect to it using
\t{gdb} as follows (replace \t{test} with the name of your executable and
\t{10343} with the actual process id printed when the process goes to sleep.):
\begin{itemize}
\item Start \t{gdb} (preferably from within Emacs)
\item Type
\begin{verbatim}
(gdb) file test
(gdb) attach 10343
\end{verbatim}
\end{itemize}

 This is useful for debugging multi-threaded code or code that
is started by daemons. This has effect only if the program would actually stop
there.

 Note that this mode is most useful when you compiled the code with \t{-g} and
you did not use \t{--releaselib}. I also prefer to use \t{-commPrintLn} so
that the debugging information refers to the cured file, not the original. 
\end{itemize}

%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%
\chapter{Using Deputy}\label{ch-examples}

 In this chapter we describe the typical steps that must be taken to use
Deputy on a new software package. For each step we give general instructions.
Then, we look at a few concrete software packages and we describe all the
steps that were necessary. We describe the warnings and the errors that we ran
into and how we solved them. Most of these warnings and errors are also
discussed in \chref{warn}. Take a look there if the explanation here is too
terse.
 
\begin{enumerate}
\item {\bf Regular build} First try to download the sources and build them in
the regular manner (using \c{gcc}). It might be a good idea to setup a CVS
repository right after you download the sources, in order to better keep track
of the changes you are making.

\item {\bf Build using CIL} Next you should try to build the package using CIL
(the front-end that Deputy uses). This step is optional but is a good idea
just in case your software package exposes a bug in CIL. To perform this step
you should edit the Makefile as follows (assuming it uses CC to invoke the
compiler \emph{and} the linker):
\begin{verbatim}
ifdef DEPUTY
 CC:=/home/necula/ccured/bin/ccured
endif
ifdef ONLYCIL
 CC+= --nodeputy
endif
\end{verbatim}
\TODO{We ought to support CIL-only build mode with the deputy script. This
 should define away the attributes}

 If your project includes a more complicated setup, you must make the
necessary changes to use the above commands instead of \c{gcc}. 

 Then you can run:
\begin{verbatim}
make clean
make DEPUTY=1 ONLYCIL=1
\end{verbatim}

 This should build your project as before, except that each source file is
first preprocessed, then passed through the \c{deputy.asm.exe} executable to
produce the CIL output (a file with suffix \c{cil.c} that contains the source
of your program after being processed by the CIL front-end), then preprocessed
again and then finally passed to \c{gcc}. Here is an example of what you
should see for the file \c{util.c} from the \c{mathopd} package:

\begin{verbatim}
/home/necula/deputy/bin/deputy --nodeputy -c -O -Wall -DHAVE_CRYPT_H util.c -o util.o
gcc -D_GNUCC -E  -O -DHAVE_CRYPT_H util.c -o ./util.i
/home/necula/deputy/obj/x86_LINUX/deputy.asm.exe --cilout ./utilcil.c --nodeputy --warnall ./util.i
gcc -D_GNUCC -E  -O -DHAVE_CRYPT_H -I/home/necula/deputy/include ./util.cil.c -o ./util.cil.i
gcc -D_GNUCC -c -O -DHAVE_CRYPT_H -Wall -o util.o ./util.cil.i
\end{verbatim}

 At this point you should ensure that the executable still works as expected.
If it does not then you have found a bug in the CIL front-end or in the
\c{deputy} Perl script that tries to impersonate \c{gcc}. CIL has been tested
extensively, so you can consider yourself truly unfortunate. Please let us know
about your problem.
\TODO{Should we explain how to use merging?}

\item {\bf Build with Deputy}
 Now we start using Deputy:
\begin{verbatim}
make clean
make DEPUTY=1
\end{verbatim}

Deputy will print information about the stages that it goes through. You
should watch for warnings and error messages, especially in the ``Inference''
stage and in the ``Curing'' stage. If you are lucky the above steps are enough
to build the executable. However, many times Deputy will stop with some error.
The first thing you should do in that case is to scan the warnings that lead
to the error and proceed as explained in \chref{warn}. 

\item {\bf Run and debug the processed code}
\TODO{Would be nice to have an attribute to use where we used ``cured'' before}
 Now that you have build your executable with Deputy you should run it on as
many examples as possible. Remember that Deputy is engineered to catch the
majority of the bugs at run-time (it is designed with the philosophy that the
C programmer is better than the Deputy static analyzer, so Deputy just
silently inserts run-time checks when it cannot ensure statically that what
the program is doing is guaranteed to be correct). 

 When you get an error message from Deputy you should investigate it to see if
it is a false alarm or a true bug. 

 You can tell Deputy to continue the execution after it encounters an error if
you set the environment variable \c{DEPUTY\_CONTINUE\_ON\_ERROR}.

\end{enumerate}

 Next we look at concrete examples. If you want to try your hand at using
Deputy on real code you might want to try it on these packages and then use
the instructions when you get stuck.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \section{Example: \t{mathopd} HTTP server}\label{sec-mathopd}
\TODO{this example}

    \subsection{Step 1: Regular Build}

From the README file: ``This is Mathopd, a fast, lightweight, non-forking HTTP
 server for UN*X systems.''

 We describe here the steps required for processing the version 1.4-gamma of
mathopd (a development version). This package contains of 5000 lines of code. 

 We download \c{mathopd-1.4-gamma.tar.gz}, unpack, change the Makefile as
required for Linux and then we try it out: 
\begin{verbatim}
cd src
make
\end{verbatim}

 Next we edit the configuration file (\c{doc/sample.cfg}) so that we can run
the server on port 8000. Right after the line \c{Server \{} we add \c{Port
 8000}. Then we must become root and create a directory for the log:
\begin{verbatim}
su root
mkdir /var/mathopd
chmod 777 /var/mathopd
exit
./mathopd <../doc/sample.cfg
\end{verbatim}

 Now from another machine (make sure you have ~/public\_html/index.html on the
 server machine):
\begin{verbatim}
explorer http://manju.cs.berkeley.edu:8000/~necula/
\end{verbatim}

 and we see that it works.

   \subsection{Step 2: Build with CIL}

  Completely uneventful.

   \subsection{Step 3: Build with Deputy}

 For \c{mathopd} we saw the warning:
\begin{verbatim}
Warning: Generated automatic vararg descriptor for log_d: struct autoVarargDescr_log_d : char const   */* __attribute__((___ptrnode__(922))) */,
uid_t
If this is a printf-like function you should declare it!
\end{verbatim}

 As explained in \chref{warn}, we take a look at the implementation of
\c{log\_d} (we find it in the merged file \c{mathopd\_comb.c}) to make sure
Deputy did not miss anything. Sure enough, \c{log\_d} is a printf warning.
Same thing for \c{die}. We fix this by adding the following pragma in
\c{main.c} (see \secref{manualvararg} for details):
\begin{verbatim}
#pragma ccuredvararg("log_d", printf(1))
#pragma ccuredvararg("die", printf(2))
\end{verbatim}


 In the process of doing mathopd, we encountered the warning:
\begin{verbatim}
/home/necula/ccured/include/netdb_wrappers.h:329: Warning: Solver: changing User Specified SAFE node 1371 (the local variable p_ith_alias) to WILD
\end{verbatim}

 This turned out to be a bug in the wrapper for the socket functions. We found
it using the browser (see \secref{browser}). 

 Then we saw a warning:
\begin{verbatim}
/usr/include/sys/socket.h:156: Warning: sendmsg appears to be external
  (it has a wrapper), yet it has a mangled name: sendmsg_scsws_.
  Did you forget to use __ptrof and a version of __mkptr?
 For more information, consult the online documentation on
  "Writing Wrappers".
\end{verbatim}

 This turned out to be due to the same socket wrapper error.

 Another warning you might see when you run Deputy is:
\begin{verbatim}
3 incompatible types flow into node void  *1127
  Type struct iovec_LEAN  *1178 at /home/necula/ccured/include/socket_wrappers.h:237
  Type char */* __NODE(1371) __ROSTRING  */ *1372 at /home/necula/ccured/include/netdb_wrappers.h:332
  Type struct iovec_LEAN  *1146 at /home/necula/ccured/include/socket_wrappers.h:219
\end{verbatim}
 
 This means that a \c{void *} node is cast to several incompatible types. When
you investigate this (using the browser, for example, or just following the
line numbers) you discover that the \c{\_\_trusted\_add\_iov} issue is the
cause of this also. 

 Once we fix the above problem we notice that there are no more \WILD{}
pointers: 
\begin{verbatim}
ptrkinds: Graph contains 12886 nodes
ptrkinds:   SAFE - 9256 ( 72\%)
ptrkinds:   SEQ - 429 (  3\%)
ptrkinds:   FSEQ - 3201 ( 25\%)
\end{verbatim}

    \subsection{Step 4: Write the wrappers}

We see now that there are some missing functions:
\begin{verbatim}
mathopd_comb.o: In function `log_request':
mathopd_comb.o(.text+0x1b02d): undefined reference to `asctime_qs'
\end{verbatim}

 See \chref{wrapper} for information on how to write this wrapper: Essentially
this is what we had to add to \c{time\_wrappers.h} file:
\begin{verbatim}
#pragma ccuredwrapper("asctime_wrapper", of("asctime"))
__inline static
char *asctime_wrapper(const struct tm *timep) {
  struct tm *thinTimep = __ptrof(timep);
  char *thinRet = asctime(thinTimep);
  return __mkptr_string(thinRet);
}
\end{verbatim}

   \subsection{Step 5: Run and Debug the cured code}

 We ran the \c{mathopd} server and we get an error right away:
\begin{verbatim}
Failure at config.c:924: new_pool(): Ubound
Aborted
\end{verbatim}

 We look at the code and we see this code in \c{config.c}:
\begin{code}
p->ceiling = t + s;
\end{verbatim}\end{code}

 This looks like the pointer that is stored in the \c{ceiling} field is
outside bounds, that that is Ok. This field is never used as a pointer. So, we
change its type to \c{long} instead. We could change it to \FSEQ{} as well.
See \chref{warn} for more possible solutions. 

 Now mathopd seems to work!! But of course you should be using it for real in
order to find the bugs. 


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%55
   \section{Example: UCSPI TCP Suite}\label{sec-ucspi}
\TODO{this example}

  \subsection{Step 1: Regular Build}

 This is a package that provides ``tcpserver'' and ``tcpclient''. From their
web page (\ahreftop{http://cr.yp.to/ucspi-tcp.html}): ``they are easy-to-use
command-line tools for building TCP client-server applications.'' The package
also includes a number of clients built using these tools. There are 6700
lines of code in this package. We actually found one bug in this library. 


 We downloaded the version 0.88 (as of January 9, 2003). Following the
instructions:
\begin{verbatim}
gunzip ucspi-tcp-0.88.tar
tar -xf ucspi-tcp-0.88.tar
cd ucspi-tcp-0.88
make
\end{verbatim}

 Before we install it, we edit the file conf\_home to point to the current
directory (we do not want to mess up the /usr/local). Then we continue:
\begin{verbatim}
make setup check
\end{verbatim}

 And now the big moment:
\begin{verbatim}
./http@ www.yahoo.com
\end{verbatim}

 Bingo!

     \subsection{Step 2: Build with CIL}

 This software package has a strange build interface. The Makefile contains
things like:
\begin{verbatim}
addcr.o: \
compile addcr.c buffer.h exit.h
        ./compile addcr.c

compile: \
warn-auto.sh conf-cc
        ( cat warn-auto.sh; \
        echo exec "`head -1 conf-cc`" '-c $${1+"$$@"}' \
        ) > compile
        chmod 755 compile
\end{verbatim}

 What is happening is that the compile script is created from the first line
of \c{conf-cc} and then used as a compiler. That line contains \c{gcc -O2}
right now. We change that file to use instead the value of the CC environment variable:
\begin{verbatim}
$CC -O2
\end{verbatim}
% $

 (You might want to also change warn-auto.sh to add a -v argument to /bin/sh
 so that you see what is going on.)

 Then we add the stuff to Makefile to define CC (and export it to child
scripts). It turns out that this file also was missing a clean target, so we
add that as well:
\begin{verbatim}
export CC:=gcc
ifdef DEPUTY
 CC:=/home/necula/ccured/bin/ccured
endif
ifdef NOCURE
 CC+= --nocure
endif
ifdef NOMERGE
 CC+= --nomerge
endif

clean:
        rm -f *.i *.o *.a
        rm -f *cil.c *infer.c *comb.c *cured.c
        rm http@ tcpclient tcpserver
\end{verbatim}

 Just to test the new setup we make it again and test it again. 

 Now we try to make it with CIL.
\begin{verbatim}
make clean
make DEPUTY=1 NOCURE=1 NOMERGE=1
\end{verbatim}

 Now we get an error:
\begin{verbatim}
tcpserver.o: In function `main':
tcpserver.o(.text+0xa29): undefined reference to `env_get'
tcpserver.o(.text+0xa50): undefined reference to `env_get'
\end{verbatim}

 Clearly we have done something wrong. A quick investigation reveals that
tcpserver.c does need \c{env\_get}, which is defined in env.c, but seems to
be missing from \c{envcil.c}. This means that the CIL front-end has dropped
this function. This is an embarrassing CIL bug. Now, when you have things
disappear then the fault is most often in the algorithm that CIL uses to
remove ``unnecessary'' things (such as locals or prototypes that are not
used). To disable that stage, pass the \c{--keepunused} flag to Deputy.

 Anyway, we fix that bug and now everything works. We now have to try the
merging. For this we must also intervene in the way the Makefile links
libraries and executables. It uses the scripts \c{makelib} to make a library
and \c{load} to make an executable. 

 For the \c{load} script all we need to change is the \c{conf-ld} to use
\c{\$CC} instead of \c{gcc}. We do this and we run with merging. We get this
error:
\begin{verbatim}
gcc -D_GNUCC  -o tcpserver -s tcpserver_comb.o cdb.a dns.a time.a unix.a byte.a
cdb.a: could not read symbols: Archive has no index; run ranlib to add one
\end{verbatim}

 As explained in \chref{warn}, this is because we should not use \c{ar} to
archive files in the merging mode, but we should use \c{ccured --mode=AR}. We
achieve this by changing the Makefile, which creates the \c{makelib} script.
We change it such that the \c{makelib} script uses the environment variable
\c{AR} instead of \c{ar}. And we defined AR in the Makefile as follows:
\begin{verbatim}
export AR:=ar
ifdef DEPUTY
  ifndef NOMERGE
    AR:=/home/necula/ccured/bin/ccured --mode=AR
  endif
endif

\end{verbatim}

 We run again in merging mode and now we get:
\begin{verbatim}
ranlib: cdb.a: File format not recognized
\end{verbatim}

 You look at \c{cdb.a} and find that it is a merged source file. You should
not use \c{ranlib} on such files. We edit the Makefile again and rerun. 

 Now we get this error message when trying to merge \c{rblsmtpd} from a number
of object files and libraries:
\begin{verbatim}
/usr/include/sys/socket.h:189: Error: Incompatible declaration for accept (4). Previous was at rblsmtpd.c:103 (0) (different type constructors: void  vs. int )
\end{verbatim}


 What happens is that the file \c{rblsmtpd.c} defines its own global \c{accept}
(luckily, with a different type than the one in the library; otherwise Deputy
would not have noticed!). Yet, one of the
other files that are merged (\c{socket\_accept.c}) uses the standard
library's accept. This looks like a bug. When the linker puts everything
together the references to the ``accept'' from \c{socket\_accept} will be
resolved to the ``accept'' from \c{rblsmtpd} (which is clearly not an
acceptable replacement for the socket function). 

 We change the name of the ``accept'' in \c{rblsmtpd} and we rerun and now
everything works. A result of your work so far is that for all of the utility
programs that make up this package you have their sources in one source file
(e.g. \c{tcpclient\_comb.c}. And, we have found a bug even before we started
to use the actual Deputy!

      \subsection{Step 3: Build with Deputy}

 The first thing we see when we enable Deputy on this package is:
\begin{verbatim}
chkshsgr.c:8: Warning: Calling function getgroups without proper prototype: will be WILD.
  getgroups has type void * __attribute__((___ptrnode__(12))) /* /* missing proto */  */()
chkshsgr.c:8: Warning: Calling function _exit with 1 arguments when expecting 0: will be WILD.
  _exit has type void ()
\end{verbatim}

 Two warnings, both due to missing or incomplete prototypes. In the cast of
\c{getgroups} it is a missing prototype. We add to \c{chkshgr.c} the following:
\begin{verbatim}
#include <unistd.h> // For getgroups
#include <grp.h>    // For setgroups
\end{verbatim}

 We also exit the prototype of \c{\_exit} in \c{exit.h}:

\begin{verbatim}
extern void _exit(int); // The "int" was missing
\end{verbatim}

 Now Deputy succeeds in making this executable and proceeds to make
\c{tcpserver}. Here we find this one:
\begin{verbatim}
tcpserver.c:352: Error: You did not turn on the handling of inline assembly. Better hide this assembly somewhere else!
\end{verbatim}

 This is interesting! We look at the inline assembly (a good place to look in
is \c{tcpserver\_comb.c}, you'll see them all in there). One is a use of
\c{ntohs}, which is harmless because it does not involve pointers. We'll
leave this alone. 

 But the other 5 or 6 such things are uses of the macros \c{FD\_SET} and
friends from \c{<sys/select.h>}. We investigate and we find that these macros
are defined in \c{<bits/select.h>}, and luckily that file also provides
regular C implementation for them, along the following lines:
\begin{verbatim}
#if defined __GNUC__ && __GNUC__ >= 2

# define __FD_ZERO(fdsp) \
  do {                                                                        \
    int __d0, __d1;                                                           \
    __asm__ __volatile__ ("cld; rep; stosl"                                   \
                          : "=c" (__d0), "=D" (__d1)                          \
                          : "a" (0), "0" (sizeof (fd_set)                     \
                                          / sizeof (__fd_mask)),              \
                            "1" (&__FDS_BITS (fdsp)[0])                       \
                          : "memory");                                        \
  } while (0)
#else   /* ! GNU CC */
# define __FD_ZERO(set)  \
  do {                                                                        \
    unsigned int __i;                                                         \
    fd_set *__arr = (set);                                                    \
    for (__i = 0; __i < sizeof (fd_set) / sizeof (__fd_mask); ++__i)          \
      __FDS_BITS (__arr)[__i] = 0;                                            \
  } while (0)

#endif  /* GNU CC */
\end{verbatim}

 I am going to patch that include file to make the conditional test always
false and thus ensure that the C version is used always. 
\begin{enumerate}
\item First, we tell Deputy that \c{<bits/select.h>} is a file that must be
patched (you can see that it is not patched already because it is not present
in the directory \c{cil/include/gcc\_2.95.3}; by the time you read this it this
whole patching business should have been done already). We go into
\c{cil/Makefile.gcc} and add to the list of \c{PATCH\_SYSINCLUDES} the name
\c{bits/select.h} (but we do it only in the Linux section). 
\item Then, we specify the patch. We add the following to the file \c{cil/ccured\_GNUCC.patch}:
\begin{verbatim}
<<< file=bits/select.h, system=linux
#if defined __GNUC__ && __GNUC__ >= 2
===
#if 0 && defined __GNUC__ && __GNUC__ >= 2
>>> 
\end{verbatim}
 
This says that the specified patch should be applied to the file
 \c{bits/select.h} when Deputy is run on a Linux system. (Not all
 platforms have bits/select.h.)
Matching is done whitespace-insensitive. Now you rebuild Deputy (just run
\c{make}) and you should find the patched file in the
\c{cil/include/gcc\_2.95.3/bits}. Make sure it is as you need. More information
about the patcher is at \ahrefurl{../cil/patcher.html}
\end{enumerate}

 And since we have left one inline assembly in, we must tell Deputy to accept
it as is. We change the Makefile to pass the \c{--allowInlineAssembly} to
Deputy.

 Now we find more missing prototype problems:
\begin{verbatim}
tcpserver.c:210: Warning: Calling function close with 1 arguments when expecting 0: will be WILD.
  close has type int ()
\end{verbatim}

 In fact, \c{close} does not have a prototype at all. Deputy has supplied one
without arguments while making \c{unix.a}! We add the ``\#include <unistd.h>''
to \c{tcpserver.c} and go on. 

 We add a few more prototypes and then we get:
\begin{verbatim}
buffer_get.c:10: Warning: Calling function (*op) with 3 arguments when expecting 0: will be WILD.
  (*op) has type int ()
\end{verbatim}

 We find in \c{buffer.h} and \c{buffer\_get} a function pointer type declared
as ``int (*op)()''. Again the missing argument types. We fill those in. 

 Now starts the real fun, chasing away the \WILD{} pointers (see
\chref{nowild} for general techniques). We see this message:
\begin{verbatim}
** 1: Bad cast at cdb_make.c:36 (char  *510 ->struct cdb_hplist  *1376)
** 2: Bad cast at pathexec_env.c:42 (char  *510 ->char */* __NODE(2537)  */ *2538)
** 3: Bad cast at pathexec_env.c:67 (char */* __NODE(2537)  */ *2538 ->char  *2553)
** 4: Bad cast at sig.c:12 (void (int  ) *2695 ->void () *2694)
** 5: Bad cast at sig_catch.c:9 (void () *673 ->void (int  ) *2711)
ptrkinds: Graph contains 4383 nodes
ptrkinds:   SAFE - 3142 ( 72%)
ptrkinds:   SEQ - 15 (  0%)
ptrkinds:   FSEQ - 127 (  3%)
ptrkinds:   WILD - 1099 ( 25%)
535 pointers are void*
5 bad casts of which 0 involved void* and 2 involved function pointers
1 (20%) of the bad casts are downcasts
0 incompatible equivalence classes
\end{verbatim}

 The casts 4 and 5 are due to missing argument types function types. We edit
sig.h to add the ``int'' as the argument type for signal handler. 

 We investigate cast number 2 and we find something like this:
\begin{verbatim}
 e = (char **) alloc((elen + 1) * sizeof(char *));
\end{verbatim}

 This is a custom allocator. We must declare it (in alloc.h):
\begin{verbatim}
extern void *alloc(unsigned int);
#pragma ccuredalloc("alloc", nozero, sizein(1)) // We added this line
\end{verbatim}

 We run Deputy again and no more bad casts (it looks like all the others were
due to \c{alloc}), but still a bunch of \WILD{}:
pointers: 
\begin{verbatim}
ptrkinds: Graph contains 4575 nodes
ptrkinds:   SAFE - 3324 ( 73%)
ptrkinds:   SEQ - 41 (  1%)
ptrkinds:   FSEQ - 150 (  3%)
ptrkinds:   WILD - 1060 ( 23%)
579 pointers are void*
0 bad casts of which 0 involved void* and 0 involved function pointers
No bad casts, so no downcasts
2 incompatible types flow into node void  *518
  Type char */* __NODE(2549)  */ *2550 at pathexec_env.c:67
  Type char  *102 at dns_transmit.c:63
2 incompatible equivalence classes
\end{verbatim}

 Notice that we have more pointers in the program. This is due to the
allocator, which is now polymorphic and is duplicated several times. But we
also have incompatible equivalence classes. This is because there is a \c{void
*} pointer that is used with several incompatible types (in this case \c{char
*} and \c{char **}). See \secref{poly} for more details on this. This turns
out to be because the function \c{alloc\_free} with a declared argument of
type \c{void *} is used in two places with different argument types. We simply
declare that function to be polymorphic (in \c{alloc.h}):
\begin{verbatim}
#pragma ccuredpoly("alloc_free")
\end{verbatim}
 
 Finally, Deputy succeeds, with no \WILD{} pointers, but there still is a
warning that we have not looked at:
\begin{verbatim}
pathexec_env.c:42: Warning: Encountered sizeof(char */* __attribute__((___ptrnode__(2595))) */) when type contains pointers. Use sizeof expression. Type has a disconnected node.
\end{verbatim}

 As explained in \secref{sizeof} we should take a look at the code. We find
this typical example, and we fix it accordingly:
\begin{verbatim}
  e = (char **) alloc((elen + 1) * sizeof(* e)); // Was sizeof(char *)
\end{verbatim}


  \subsection{Step 4: Run and debug the cured code}

 
 We have built the suite of tools and now we run it. Right away we get a
run-time error, so we set \c{DEPUTY\_CONTINUE\_ON\_ERROR}
(\secref{errorhandle}) to see them all. 
\begin{verbatim}
Failure STORE_SP at pathexec_env.c:47: pathexec_qq(): Storing stack address
...
Failure STORE_SP at /home/necula/ccured/include/functions/deepcopy_stringarray.h:70: __deepcopy_stringarray_to_compat___0_ssqq(): Storing stack address
\end{verbatim}

 There are two distinct errors. We'll fix them, but here is a way to silence
Deputy if you are lazy: we can use
\c{DEPUTY\_ERROR\_HANDLERS} to specify that we want to ignore all
\c{STORE\_SP} errors in those two functions. For this we write a text file
(ucspi.handlers):
\begin{verbatim}
ignore STORE_SP at *:*:pathexec_qq
ignore STORE_SP at *:*:__deepcopy_stringarray_to_compat___0_ssqq
\end{verbatim}

 Now we run as follows:
\begin{verbatim}
DEPUTY_ERROR_HANDLERS=ucspi.handlers ./http@
\end{verbatim}

 and \t{http@} seems to work.


 Let's go back to fixing these errors. These errors are all trying to store
strings that are obtained from the \c{environ} variable. It turns out that
those strings are on the stack (allocated before \c{main} is invoked). The
solution would be to copy those strings on the heap. But right after I saw
this error I realized that Deputy should not complain if the address that is
being stored is in the stack frame of \c{main} or at higher addresses. So, I
added this feature to Deputy and now you will not see these particular errors.
But if you run \t{http@ www.yahoo.com} you will get:
\begin{verbatim}
Failure STORE_SP at dns_transmit.c:213: dns_transmit_start_sqqff(): Storing stack address
\end{verbatim}

 It does not take much to find that this is due to the following code:
\begin{verbatim}
# 5 "dns_resolve.c"
int dns_resolve(char *q,char qtype[2])
{
  struct taia stamp;
  struct taia deadline;
  char servers[64];

  if (dns_transmit_start(&dns_resolve_tx,servers,1,q,qtype,"\0\0\0\0") == -1) return -1;
\end{verbatim}

 \t{dns\_transmit\_start} then stores the address of the array \c{servers}
into the heap. The solution here is to move the \c{servers} array into the
heap (or make it a global). We can achieve the former by declaring:
\begin{verbatim}
 char servers[64]  __HEAPIFY;
\end{verbatim}

 and Deputy will move it to the heap (see \secref{storeptr}).

 Bingo! It seems to work. Now, you can start measuring performance and, if
desired, you can try to make Deputy infer better checks for your code. 

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
      \section{Example: PING}
\TODO{this example}
 
 In this section I describe what it took to do the \t{ping} utility from
\t{netkit-base-0.17}. 

 We download, compile, test it. Then we setup the Makefiles to use ccured
instead of \t{gcc} and we test that it works in the \t{--nocure} mode. Then we
turn on curing. 

 First we see two errors pointing out that there is inline assembly in
\t{ping}. Deputy also prints the instructions and we see that they are just
bit manipulations. So, we just pass \t{--allowInlineAssembly} to ccured and go
on. 

 Now we get:
\begin{verbatim}
Failure UBOUND at ping.c:1303: main(): Ubound
\end{verbatim}

 To investigate this one we can use \t{DEPUTY\_SLEEP\_ON\_ERROR} (see
\chref{invoke}). The fragment of code that causes this error is similar to the
following code:
\begin{deputycode}[norun]
struct icmp {
   int various;
   char data[1];
};
char outpack[65536];

char foo() {
 // Get the 8th data character
 return ((struct icmp*)outpack)->data[8];
}
\end{deputycode}

 The problem is that once \c{outpack} is cast to a \c{struct icmp *} it looses
the ability to access most element in the original array. The solution for
this particular error involves a slight rewrite of the access as:
\begin{deputycode}[norun]
char foo() {
 // Get the offset of the 8th data character
 int off = (int) & ((struct icmp*)0)->data[8];
 return outpack[off];
}
\end{deputycode}

 We need to fix that problem in all accesses to the \t{data} field. After
that, we run into another problem:
\begin{verbatim}
Failure ALIGNSEQ at ./ping_combcured.c:3923: pinger(): Creating an unaligned sequence
\end{verbatim}

 This is because at some point we create a sequence pointer whose home area
does not contain a whole number of elements. See \secref{checkseq} for the
various ways to address this problem. We choose to simply tell Deputy to allow
partial elements in structures and to adapt its checks accordingly. To achieve
this we pass \t{--allowPartialElementsInSequence} to Deputy.

 Now it works, we are done.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
      \section{Example: THTTPD Server}
\TODO{this example}

In this section, we take a look into how to cure thttpd, described by its 
author as ``a simple, small, portable, fast, and secure HTTP server.'' It 
is currently the fifth most popular HTTP server on the net. You can get it 
at \ahreftop{http://www.acme.com/software/thttpd/}. The version I work 
with is 2.23 beta 1.

      \subsection{Step 1: Regular Build}

First, we unpack the files:

\begin{verbatim}
gunzip thttpd-2.23beta1.tar.gz
tar -xvf thttpd-2.23beta1.tar
\end{verbatim}

Look into the directory for the file \c{configure}. We don't want to mess up 
the /usr/local/ folder, so go into \c{configure} and delete the folder path 
from \c{ac\_default\_prefix}. Now Makefile should make thttpd to the folder 
where the source code resides. Run \c{configure}.

\begin{verbatim}
./configure
\end{verbatim}

The file should do some work and generate a few files. 

There is also another modification we should make to avoid conflicts with any 
existing http servers (e.g. Apache). In \c{config.h}, go-to Line 321 and 
change the default port from 80 to something like 7500. 

Now we can run make. The compiler does work and should produce a file named 
\c{thttpd}. Run the program and test the server from another computer. In my 
case, I steered my browser to \c{http://manju.cs.berkeley.edu:7500/~andypang/}.

\begin{verbatim}
make
\end{verbatim}
a few seconds later...
\begin{verbatim}
./thttpd
\end{verbatim}

If you see your homepage, thttpd is working. If not, make sure you have a 
public\_html folder. If you are lazy, there is another way to check if thttpd 
is working. Check whether the site for the server is up at the port you 
specified (e.g. \c{http://manju.cs.berkeley.edu:7500/}). A page with a green 
background should appear notifying you that thttpd is running.

\subsection{Step 2: Build with CIL}

It's time to look into that \c{Makefile.in} that came with thttpd. 
\c{Makefile.in} is the file from which \c{configure} generates \c{Makefile}, 
which in turn is used to build the application. 

Below the line that says ``You shouldn't need to edit anything below here,'' 
we make the same changes to the \c{CC} variable as in the other tutorials.

\begin{verbatim}
ifdef DEPUTY
 CC:=/home/andypang/cil/bin/ccured
endif
ifdef NOCURE
 CC+= --nocure
endif
ifdef NOMERGE
 CC+= --nomerge
endif
\end{verbatim}

Be sure to insert these ifdefs below the block of variable declarations (below 
line 60). Otherwise, gcc would be used to compile the files.

There will also be more files to clean after CIL/Deputy is run, so I added 
the following to clean up the CIL files and folders that will be generated:

\begin{verbatim}
CIL =           $(SRC:.c=.i) *cil*

COMB =          *comb*
\end{verbatim}
% $

I modified the variable CLEANFILES to include those files.

\begin{verbatim}
CLEANFILES =    $(ALL) $(OBJ) $(GENSRC) $(GENHDR) $(CIL) $(COMB)
\end{verbatim}

Now we are ready to compile using CIL. First, we run \c{configure} again to 
update the Makefile.

\begin{verbatim}
./configure
make clean
make DEPUTY=1 NOCURE=1 NOMERGE=1
\end{verbatim}

Ensure the application still works correctly. It should. Now build with 
merging.

\begin{verbatim}
make clean
make DEPUTY=1 NOCURE=1
\end{verbatim}

Again, check for proper functionality.

\subsection{Step 3: Build with Deputy}

The big moment.

\begin{verbatim}
make clean
make DEPUTY=1
\end{verbatim}

You should see a number of errors and warnings. Many of these will involve 
a warning of a ``malformed format string'' looking something like this:

\begin{verbatim}
libhttpd.c:226: Warning: Malformed format string [child wait - %m]
\end{verbatim}

If you take a look at the string, the warning stems from a call to syslog 
with a \%m. This is safe, and can be safely ignored. ***********


Now we see a prototyping warning:

\begin{verbatim}
thttpd.c:437: Warning: Calling function sigset without proper prototype: will be WILD.
  sigset has type void * __attribute__((___ptrnode__(1666))) /* /* missing proto */  */()
\end{verbatim}

At this point we realize that some files are read-only. We chmod the thttp folder from its 
parent directory so that we can write to any file in the directory:

\begin{verbatim}
chmod -R u+w thttpd-2.23beta1
\end{verbatim}

Back to the problem at hand. If one punches in \c{sigset} on Google, one 
will that it is a function in \c{signal.h}. Add the following \c{thttpd.c} 
to remedy the warning:

\begin{verbatim}
extern void *sigset(int, void*);
\end{verbatim}

Although the warning also appeared for the file \c{libhttpd.c}, the 
prototype in \c{thttpd.c} will work for all files in the project.


The next most prevalent warning should be a sscanf error, where Deputy 
warns that it does not expect the type \c{char *}. Deputy does not accept 
strings in sscanf because one could potentially read in an unbounded 
string. This characteristic could be used for malicious intentions. 

Although \c{\%400[a-zA-Z]} is used and hence strings that are accepted by 
sscanf will be limited to 400 bytes, Deputy currently does not support this. 
This may change in the future, because this method of scanning strings is 
not suspectible to the same problems as simply using \c{\%s}.

To fix this error, use Deputy's sscanf/fscanf functions in place of 
the ones in \c{stdio.h}. Please refer to \secref{scanf-like} 
for more details. As an example, the following is how I modified the code 
at Line 213 in \c{tdate\_parse.c}.

\begin{verbatim}
    /* DD-mth-YY HH:MM:SS GMT */
    if ( 
        (resetSScanfCount(cp), 
         tm_mday = ccured_fscanf_int(ccured_sscanf_file, "$d-"),
         ccured_fscanf_string(ccured_sscanf_file, "%400[a-zA-Z]-", str_mon),
         tm_year = ccured_fscanf_int(ccured_sscanf_file, "$d "),
         tm_hour = ccured_fscanf_int(ccured_sscanf_file, "$d:"),
         tm_min = ccured_fscanf_int(ccured_sscanf_file, "$d:"),
         tm_sec = ccured_fscanf_int(ccured_sscanf_file, "$d GMT"),
         getScanfCount()) == 6 &&
        /*
        sscanf( cp, "%d-%400[a-zA-Z]-%d %d:%d:%d GMT",
                &tm_mday, str_mon, &tm_year, &tm_hour, &tm_min,
                &tm_sec ) == 6 &&
        */
            scan_mon( str_mon, &tm_mon ) )
        {
\end{verbatim} 
% $


Then we see several warnings regarding the use of sizeof:

\begin{verbatim}
libhttpd.c:2782: Warning: Encountered sizeof(char */* __attribute__((___ptrnode__(5491))) */) when type contains pointers. Use sizeof expression. Type has a disconnected node.
\end{verbatim}

We take a look at this line and find that it is a function call to \c{RENEW}. 

\begin{verbatim}
nameptrs = RENEW( nameptrs, char*, maxnames );
\end{verbatim}

The definition of \c{RENEW} can be found in \c{libhttpd.h}. 

\begin{verbatim}
#define RENEW(o,t,n) ((t*) realloc( (void*) o, sizeof(t) * (n) ))
\end{verbatim}

The warning arises from the fact that the Deputy inferencer cannot make
the connection between \c{nameptrs} and \c{char *}'s. See \secref{sizeof} 
for more details.

To fix the warning, we let Deputy inference the argument in \c{sizeof} 
to \c{nameptr} by modifying the code in the following way:

In libhttpd.c
\begin{verbatim}
nameptrs = RENEW( nameptrs, nameptr*, maxnames );
\end{verbatim}

In libhttpd.h
\begin{verbatim}
#define RENEW(o,t,n) (realloc( (void*) o, sizeof(t) * (n) ))
\end{verbatim}

Now Deputy will know that we are allocating memory based on the size of 
the pointers to \c{nameptr}. 

The macro \c{NEW} is defined one line before \c{RENEW}, and we fix a couple 
of calls to \c{NEW} in the same way. 


We now face a number of warnings of the following form:

\begin{verbatim}
libhttpd.c:2519: Warning: Solver: changing User Specified SAFE node 5283 (an unnamed location (often an inserted cast)) to FSEQ
\end{verbatim}

A quick look at \c{libhttpd.c} shows that a call to \c{qsort} is made. 
The wrapper for qsort can be found in \c{stdlib\_wrappers.h}, and there 
appears to be two versions of \c{qsort}. One versions supports polymorphism 
and the other does not. Add \c{-DUSE\_POLYMORPHIC\_QSORT} in \c{Makefile.in} 
after we make the call to \c{cil/bin/ccured}, so that Deputy will know to 
use the polymorphic qsort. 


This fixes the problems in \c{libhttpd.c} but not \c{tdate\_parse.c}. We go 
to Line 113 and find a call to qsort. At first it looks like a problem with 
sizeof, but fixing the calls to sizeof proves to be fruitless (although still 
a good programming practice). 

Let's turn to the browser to track down the bad cast for us. Looking at the 
problematic node will show us that it is in the arguments passed into the 
comparator for qsort. The arguments of the comparator are declared as \c{char *}, 
but they are also cast to \c{struct strlong *} in the function. This is a 
bad cast. Change the types of the accepted arguments to \c{void *} and 
the problem is solved. 


Next we tackle a similar problem in \c{tdate\_parse.c}:
\begin{verbatim}
** 1: Bad cast (seq) at tdate_parse.c:202 (struct tm  *7100 ->char  *7136)
\end{verbatim}

Once again, we use the browser to track down the problem, and find a cast 
from a \c{struct tm *} to a \c{char *}. We change the \c{char *} to a 
\c{void *} and the bad cast disappears.

\begin{verbatim}
    (void) memset( (void*) &tm, 0, sizeof(struct tm) );
\end{verbatim}


The last bad cast:
\begin{verbatim}
** 1: Bad cast at timers.h:41 (void */* __NODE(346)  */ *347 ->long  *349)
\end{verbatim}

Going to Line 41 reveals a union of \c{void *}, \c{int}, and \c{long}. This 
cannot possibly be safe because \c{i} could later be used as a pointer 
with \c{p}. We change this union to a tagged union as instructed in 
\secref{taggedunion}.

\begin{verbatim}
union ClientData {
    void* p;
    int i;
    long l;
} __TAGGED;
typedef union ClientData ClientData;
\end{verbatim}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 

\section{Porting Code from CCured to Deputy}\label{sec-ccuredport}
One way to determine which pointers will need annotation for Deputy is
to run CCured's whole-program analysis.  The CCured flag
\c{-{}-listnonsafe} will list the pointers in your program that need
bounds information.

Using this tool requires that CCured is able to compile your program.
This itself involves some porting effort, but hopefully many of the
changes needed for CCured are also needed for Deputy.

This is a simple, unpolished tool.  Send suggested improvements to
\ahref{mailto:matth@cs}{Matt}.

\subsection{Running CCured}
To use the \c{-{}-listnonsafe} option, make sure each file in your
program includes \c{deputy/include/ccuredport.h}.  This file redefines
the Deputy macros so that any Deputy annotations you've added are
translated to CCured annotations.  Any pointers that already have
Deputy annotations are marked so that you won't see additional
warnings that those nodes need annotations.

Now run \c{ccured -{}-listnonsafe} on your program.  You can do this
from within Emacs' compile-mode so that it's easy to find the
associated code.  You'll see a list of items like this:

\begin{verbatim}
test.c:36: node (int * __NODE(9)  ) in field "y" is Seq/FSeq
test.c:36: node (int * __NODE(9)  ) in field "y" is a void* that CCured has inferred to be a int *
test.c:28: node (int * __NODE(216)  ) in the return value is Seq/FSeq
test.c:28: node (int * __NODE(217)  ) in formal "x" is Seq/FSeq
test.c:28: node (int * __NODE(217)  * __NODE(218)  ) in formal "x" is Seq/FSeq
\end{verbatim}

Currently, you'll be notified of all Seq/FSeq pointers (which need
bounds information) that are used in the types of fields, formals, and
return types.  With local variables, Deputy's inference will often
obviate the need for annotations.  So for these we don't prompt for
bounds information unless the type is a pointer to a pointer and the
inner pointer needs bounds.  Finally, you'll also be notified of
\c{void*} pointers that CCured inferred to have a more specific type.
If a pointer already has a Deputy annotation on it, it is not listed
in the output.

\subsection{Limitations}

\begin{itemize}
\item One requirement of Deputy is that any annotations on a global
  appear on all declarations of that global (e.g. in .h files).
  Because CIL's merger combines all declared types into one node,
  there's no way for CCured to warn about half-missing annotations.
\item CCured's features don't match Deputy's, so annotations such as
  \c{\_\_SIZE} in CCured have no exact equivalent in Deputy.
\item If a function or struct uses CCured-style polymorphism, you'll
  get several messages that ``\t{foo is a void* that CCured has inferred
  to be X}'', for various X.  For now, you'll probably have to make
  this node TRUSTED in Deputy.
\item Types in cast expressions are not reported.
\end{itemize}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%5555
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
\chapter{Advanced Deputy Issues}
\TODO{this entire chapter}

 In this chapter we discuss a collection of issues having to do with using
Deputy on real programs. Some of the issues are related to sound handling of
dark corners of the C programming language (e.g. function pointers,
initialization of globals, variable argument functions). Other issues are
related to mechanisms to give hints to the Deputy inferencer.


 We recommend that you take a look at the warnings and messages that
Deputy gives and try to address the bad casts. In this chapter, we describe
a few tricks that you can use to change the code, and a few features that
Deputy has to help you do that. 

 First, a few notes:
\begin{itemize}
\item Do not use functions without prototypes. They will be \WILD{} along with
their arguments and result values.

\item Fill in the full type of functions and pointers. In C it is technically
sufficient to leave the argument part of a function type empty, and this
allows to call the function with whatever arguments you feel like. Deputy will
accept that but will make the function \WILD{}!

\item If your program has custom memory allocators (generally wrappers around
\c{malloc} and friend), you must declare them (\secref{malloc}).

\item If you have functions that use pointers polymorphically, make sure those
pointer types are \c{void *} (not \c{char *} as it was common before ANSI C). 
\end{itemize}

 When it notices bad casts, Deputy will print something like this:
\begin{verbatim}
** 1: Bad cast at cdb_make.c:36 (char  *510 ->struct cdb_hplist  *1376)
** 2: Bad cast at pathexec_env.c:42 (char  *510 ->char */* __NODE(2537)  */ *2538)
** 3: Bad cast at pathexec_env.c:67 (char */* __NODE(2537)  */ *2538 ->char  *2553)
** 4: Bad cast at sig.c:12 (void (int  ) *2695 ->void () *2694)
** 5: Bad cast at sig_catch.c:9 (void () *673 ->void (int  ) *2711)
ptrkinds: Graph contains 4383 nodes
ptrkinds:   SAFE - 3142 ( 72%)
ptrkinds:   SEQ - 15 (  0%)
ptrkinds:   FSEQ - 127 (  3%)
ptrkinds:   WILD - 1099 ( 25%)
535 pointers are void*
5 bad casts of which 0 involved void* and 2 involved function pointers
1 (20%) of the bad casts are downcasts
0 incompatible equivalence classes
\end{verbatim}

 This means that there are 5 bad casts (which contaminate 25\% of your
pointers). There are no incompatible equivalence classes in this case. 

 You can either go directly at the line numbers in which the bad casts are
reported, or you can use the browser (\secref{browser}).

 Bad cast number 4 and 5 in the example above are clear indications that there
are some incomplete function types in your program. Go and add the argument
types. 

 The other bad casts are due to an undeclared memory allocator. After we fix
 those we rerun and we get:
\begin{verbatim}
ptrkinds: Graph contains 4575 nodes
ptrkinds:   SAFE - 3324 ( 73%)
ptrkinds:   SEQ - 41 (  1%)
ptrkinds:   FSEQ - 150 (  3%)
ptrkinds:   WILD - 1060 ( 23%)
579 pointers are void*
0 bad casts of which 0 involved void* and 0 involved function pointers
No bad casts, so no downcasts
2 incompatible types flow into node void  *518
  Type char */* __NODE(2549)  */ *2550 at pathexec_env.c:67
  Type char  *102 at dns_transmit.c:63
2 incompatible equivalence classes
\end{verbatim}

 Notice that we have more pointers in the program. This is due to the
allocator, which is now polymorphic and is duplicated several times. But we
also have incompatible equivalence classes. This is because there is a \c{void
*} pointer that is used with several incompatible types (in this case \c{char
*} and \c{char **}). See \secref{poly} for more details on this. 

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
          \section{Polymorphism}\label{sec-poly}

% Polymorphism is the ability a program fragment to operate on data of
%different types. This is a useful thing to be able to do and since C does not
%have special support for it, each programmer implements polymorphism by
%extensive use of casting. But not all casts are equal. Consider for example a
%function that just returns its argument:
%\begin{code}
%int identity_bad(int x) { return x; }
%\end{verbatim}\end{code}
%
% This function can be used with any type that fits in an integer, provided the
%appropriate casts from the type to \c{int} and back are inserted. But as we
%have already discussed in \secref{castint} this won't work in Deputy because
%the pointers you get out are not usable. 
%
% A better way to do this is as follows:
%\begin{code}
%void* identity(void* x) { return x; }
%\end{verbatim}\end{code}
%
% It is a common paradigm in C to use \c{void*} for a ``pointer to I don't know
%what'' type. Deputy supports this view directly by considering each use of
%\c{void *} in the program as an occurrence of an unknown type. The Deputy
%inferencer will try to find a replacement type that makes sense in that
%context. For example, in the following code fragment Deputy will think of both
%occurrences of \c{void *} as actually being \c{int * *}.
%\begin{deputycode}
%void* identity(void* x) { return x; }
%
%int main() {
%    int * * p = 0;
%    int * * res = identity(p);
%}
%\end{deputycode}
%
% This model works for even very complicated code, such as the following
%fragment that
%defines a function \c{apply} which applies a function pointer to some
%arguments (see in the output that all pointers are inferred \SAFE{}):
%\begin{deputycode}
%// Applies a function to an argument
%void * apply(void* (*f)(void*), void *arg) {
%   return f(arg);
%}
%
%// A simple dereference function
%int * deref(int * * addr) {
%    return *addr;
%} 
%
%int  main() {
%     int * x = 0;
%     int * res = apply(deref, & x);
%}
%\end{deputycode}
%
%
% In the above example there are four occurrences of \c{void *} in the
%definition of \c{apply}. Based on the actual usage of \c{apply} the first two
%are mapped to \c{int *} and the latter two are mapped to \c{int * *}.
%
% This very flexible scheme breaks down when you have inconsistent usage of a
%\c{void *} type, such as in the following code:
%\begin{deputycode}
%void* identity(void* x) { return x; }
%
%int main() {
%    int * p = 0;
%    int * * res_pp = identity(& p);
%    int * res_p    = identity(p);
%}
%\end{deputycode}
%
% In the above code the \c{identity} function is used both with \c{int *} and
%\c{int **} argument. Since Deputy cannot find any single non-\WILD{} type that
%is compatible with all contexts in which the \c{void *} is used, it is going
%to infer that the type of the \c{void *} argument is \WILD{}. And since the
%argument is assigned to the result (implicitly due to the \c{return}
%statement) the result type is also \WILD{}. (You can use the browser to see
%all the different incompatible types that ``flow'' into a \c{void *}). It
%seems that we need a way to tell Deputy to treat the two invocations
%separately.
%
% Deputy has a crude but effective mechanism for doing just that. First, you
%have to tell Deputy that a function is polymorphic:
%\begin{code}
%#pragma ccuredpoly("identity")
%\end{verbatim}\end{code}
%
% (you can list multiple names in one \c{ccuredpoly} pragma. The pragma can
% appear anywhere in your program.).
%
%If you tell Deputy that a function is polymorphic it will take the following
%steps:
%\begin{enumerate}
%\item For each call site of the function, Deputy will create a copy of the
%function and it will assign it the name \c{/*15*/identity}, where the number
%15 is a running counter to ensure that the names are different. 
%\item Then it will perform the usual inference in which case each copy of the
%\c{identity} function is used only once. 
%\item Finally, for each combination of pointer kinds in the
%various flavors of \c{identity} Deputy will keep one copy and erase all the
%others. 
%\end{enumerate}
%
% Consider as an example the code from above, in which all pointers are now
%\SAFE{}. The output contains calls to \c{/*1*/identity} and \c{/*2*/identity}
%but since they both have the same pointer kinds for the arguments and results,
%only the body of \c{/*1*/identity} is kept:
%\begin{deputycode}
%#pragma ccuredpoly("identity")
%void* identity(void* x) { return x; }
%
%int main() {
%    int * p = 0;
%    int * * res_pp = identity(& p);
%    int * res_p    = identity(p);
%}
%\end{deputycode}
%
% If the copies of the polymorphic function do not all have the same pointer
%kind then multiple definitions are kept, as in the code below where we have
%both a \SAFE{} and a \WILD{} copy of the \c{identity} function:
%\begin{deputycode}
%#pragma ccuredpoly("identity")
%void* identity(void* x) { return x; }
%
%int main() {
%    int * __WILD p = 0;
%    int * * res_pp = identity(& p);
%    int * res_p    = identity(p);
%}
%\end{deputycode}
% 
%% For some reason this does not work anymore
%% Deputy creates a new instantiation of a polymorphic function also for each
%%place where the address of the function is taken:
%%\begin{deputycode}
%%#pragma ccuredpoly("identity")
%%void* identity(void* x) { return x; }
%%
%%int main() {
%%    int * __WILD p = 0;
%%    int * * (*p_identity)(int * *)  = identity; // Take its address
%%    int * * res_pp = p_identity(& p);
%%    int * res_p    = identity(p);
%%}
%%\end{deputycode}
%%
%
%
%\paragraph{Polymorphic types} 
%
%A similar mechanism is also available for types. You can add in the arguments
%of the \c{ccuredpoly} pragma strings like \c{"struct list"} to say that a copy of
%\c{struct list} must be created for each occurrence in the program. The
%inference will then find out which of the copies have to be compatible and at
%the very end will keep only one copy for each kind. Note however that this
%form of polymorphism does not have any run-time cost because only types are
%duplicated. It will however slow down the Deputy type inference. 
%
% Note: If the polymorphism directives do not seem to take any effect, pass the
% \t{-verbose} to ccured to see how it parses them.
%
% For example, here is how you would write polymorphic list length:
%\begin{deputycode}
%#pragma ccuredpoly("length", "struct list")
%struct list {
%   void *car;
%   struct list *cdr;
%};
%
%int length(struct list *l) {
%  for(int i = 0; l; i ++, l=l->cdr) ;
%}
%
%int main() {
%    struct list list_of_int = { 5, 0 };
%    struct list list_of_wild_ptr = { (int * __WILD)5, 0 };
%    struct list wild_list = { 5 , (struct list * __WILD)0 };
%
%    int l1 = length(& list_of_int);
%    int l2 = length(& list_of_wild_ptr);
%    int l3 = length(& wild_list);
%}
%\end{deputycode}
%
% You can see in the browser information that the references to \t{struct list}
%have been replaced with separate names such as \t{struct /*45*/list}. 
%
% In the case of recursive structures (whose name is refered directly or
%indirectly in the name of the fields), the fields use the same version of the
%structure as the structure itself. 
%
% Deputy has polymorphism for types and for functions because those are the
%entities that can be copied legally in C. {\em There is no similar
%polymorphism for data variables, nor should there be.}. 
%
% If you have a type name for a polymorphic structure, then Deputy will replace
% all occurrences of the type name with a reference to the structure itself,
% meaning that each use of the type name gets its own independent copy. 


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \section{User-defined memory allocators}\label{sec-malloc}

% If your program has a user-defined memory allocator that is used to allocate
%data of different types then its return type will be \WILD{} and so will be
%all of the pointers you store with the allocated area. Declaring such a
%function to be polymorphic will likely not help because the function is
%probably using a global data structure (the allocation buffer) that is shared
%by all polymorphic copies of the function.
%
% Deputy allows you to declare a function to be a user-defined memory allocator
%using one of the following pragmas:
%\begin{code}
%#pragma ccuredalloc("myfunc", <zerospec>, <sizespec>)
%<zerospec> ::= zero | nozero
%<sizespec> ::= sizein(k) | sizemul(k1, k2)
%\end{verbatim}\end{code}
%
% The \c{zero} argument means that the allocator zeroes the allocated area.
%Otherwise Deputy will zero it itself, if it contains pointers. The
%\c{sizein(k)} argument means that the allocator is being passed the size (in
%bytes) of the area to be allocated in argument number $k$ (counting starts at
%1). The \c{sizemul(k1, k2)} argument means that the allocator allocates a
%number of bytes equal to the product of the arguments number $k1$ and $k2$.
%
% For example the following are the pragmas for the standard library allocators
%\c{malloc} and \c{calloc}:
%\begin{code}
%void* malloc(unsigned int size);
%#pragma ccuredalloc("malloc", nozero, sizein(1))
%void* calloc(unsigned int nr_elems, unsigned int size);
%#pragma ccuredalloc("calloc", zero, sizemul(1, 2))
%\end{verbatim}\end{code}
%
% A memory allocator should have return type \c{void *}. In the pre-ANSI C days 
%allocators were written with the type \c{char *}. Once you declare a function
%to be allocator, its return type will be changed to \c{unsigned long}. At all
%call sites Deputy will examine what kind of data is being allocated and will
%construct the metadata for it. 
%
% Note that declaring a function an allocator has the effect of also making it
%polymorphic. This means that Deputy will create as many copies of your
%allocators as you have allocation sites. (After curing only copies with
%distinct calling convention will be kept, however.)
%
% Note that when you declare a custom-memory allocator as such, Deputy will
%trust that you are not going to re-use the memory area that you return. This
%means that you can use this feature to write unsafe programs in Deputy. The
%following program will succeed in trying to dereference the address 5!
%\begin{deputycode}
%#pragma curealloc("myalloc", sizein(1), zero)
%int data[8];
%void* myalloc(int sz) {
%  return data;
%}
%int main() {
% int ** p = (int **)myalloc(8);
% data[1] = 5; 
% return *p[1]; // Will dereference 5 !!!
%}
%\end{deputycode}
%
% Most often the custom-memory allocators are just wrappers around the system
%\t{malloc}. In that case there is no danger of unsoundness. 
%
% Note also that Deputy relies on the fact that the result of the custom-memory
%allocators is assigned to a variable of the right type. It is from the
%type of the destination of the allocator, or from the type cast with which the
%allocators is used, that Deputy knows what kind of metadata to create. 

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \section{Pointers with Run-Time Type Information}\label{sec-rtti}

% There are many C programs in which \c{void *} pointers are used
%non-parametrically. An example is a global variable (of type \c{void *}) that
%is used to store values of different types at different times. Consider for
%example the following code, where Deputy is forced to infer that the \c{g}
%pointer has kind \WILD{} because the \c{struct foo} and \c{struct bar} are
%incompatible:
%\begin{deputycode}
%struct foo { 
%  int f1;
%} gfoo;
%
%struct bar {
%  int * f1;
%  int f2;
%} gbar;
%
%void * g;
%
%int main() {
%  int acc = 0;
%  g = (void *)&gfoo; 
%  acc += ((struct foo *)g)->f1;
%  g = (void *)&gbar; 
%  acc += ((struct bar *)g)->f2;
%  return acc;
%}
%\end{deputycode}
%
% In this example \c{g} is used polymorphically but not in a way that could be
%handled through our support of polymorphism. (This form of polymorphism is
%called non-parametric polymorphism.) Deputy will consider the casts on \c{g}
%as bad and will mark those pointers \WILD{}. 
%
% Deputy contains special support for handling such cases, by tagging the
%polymorphic values with information about their actual type. To enable this
%behavior you must use the \RTTI{} pointer kind qualifier on the polymorphic
%pointer. Consider again the example from before but with a \c{RTTI}
%annotation:
%\begin{deputycode}
%struct foo { 
%  int f1;
%} gfoo;
%
%struct bar {
%  int * f1;
%  int f2;
%} gbar;
%
%void * __RTTI g;
%
%int main() {
%  int acc = 0;
%  g = (void *)&gfoo; 
%  acc += ((struct foo *)g)->f1;
%  g = (void *)&gbar; 
%  acc += ((struct bar *)g)->f2;
%  return acc;
%}
%\end{deputycode}
%
% If you use the browser, you will see that there are no more bad casts and no
%\WILD{} pointers in this example. If you also look at the Deputy output for
%the above example you will see that instead the \c{g} variable is now
%represented using two words, one to store its value and another to store the
%actual type of the pointer it contains. This type is created when \c{g} is
%assigned to and is checked when \c{g} is used. 
%
% Deputy can work with run-time type information only for certain pointer
%types. We call such types as {\em extensible} and for each type we also
%construct a name. Specifically, the extensible types are:
%\begin{itemize}
%\item \c{void}, named \c{"void"}
%\item A structure or union type, in which case the name is the letter \c{"S"}
%followed by the name of the structure or union type. Equivalently it can be a
%\c{typedef} name for a structure or union type. 
%\item A \c{typedef} (that {\em does not} refer to a structure or union type),
%in which case the name is the letter \c{"T"} followed by the type name.
%However, since Deputy eagerly unrolls typedefs, you {\ bf should give the
%\c{\_\_NOUNROLL} attribute}:
%\begin{verbatim}
%typedef int * MY_TYPE_NAME __NOUNROLL;
%\end{verbatim}
%\end{itemize}
%
% \RTTI{} pointers can be created on by casting from a scalar or a \SAFE{} pointer to an
%extensible type and can be cast only to scalars and a \SAFE{} pointer to an extensible
%type. In the example above, \c{struct boo} and \c{struct bar} are extensible
%pointers and we can cast pointers to these structs to \c{void * RTTI} and
%back. 
%
% Deputy also supports the \RTTI{} pointer kind on pointers whose base type is
%different from \c{void}. Consider the following example: 
%\begin{deputycode}
%struct foo {
%   int *f1;
%   int  f2;    
%} gfoo;
%
%struct bar {
%   int *f3;
%   int  f4;
%   int  f5;
%} gbar;
%
%#pragma ccured_extends("Sbar", "Sfoo")
%
%struct foo * __RTTI g;
%
%int main() {
%  int acc = 0;
%  g = (struct foo *)&gfoo; 
%  acc += g->f2;
%  g = (struct foo *)&gbar; 
%  acc += g->f2;
%  acc += ((struct bar *)g)->f5;
%  gfoo.f1 ++; // To make foo.f1 and bar.f3 both FSEQ pointers
%  return acc;
%}
%\end{deputycode}
%
% Notice that the \RTTI{} pointer kind is used with the base kind \c{struct
%foo}. An \RTTI{} pointer is strictly more powerful than a \SAFE{} pointer of
%the same base type. This means that \c{g} in the code above can be used to
%access the field \c{f1} and \c{f2} without any overhead. This is because
%Deputy enforces the requirement that an \RTTI{} pointer of base type
%\c{T} contains only pointer values whose base type {\em extends} \c{T}. The
%extension relationship is a subset of the physical subtyping relationship: we
%say that type \c{T} {\em extends} type \c{Q} if:
%\begin{itemize}
%\item Both \c{T} and \c{Q} are extensible, and
%\item Either \c{T} and \c{Q} are the same type, or
%\item \c{Q} is \c{void}, or
%\item There exists a pragma \c{ccured\_extends(T, T')} and \c{T'} {\em extends}
%\c{Q}. In this case Deputy verifies that it is safe to cast a pointer to \c{T}
%to a pointer to \c{T'}, using the usual physical subtyping relationships. 
%\end{itemize}
%
% The \c{ccured\_extends} pragmas use extensible type names to declare a
%extension hierarchy (similar to a single-inheritance class hierarchy) in which
%\c{void} is the top. Note that only extensible types can appear in the
%hierarchy and an extensible type can appear at most once on the left-side of a
%\c{ccured\_extends} pragma. An \RTTI{} pointer can contain values that are
%pointers to some extensible base type that extends that of the \RTTI{} pointer
%itself.
%
% The \RTTI{} pointer kind can be applied only to base types that are either
%\c{void} or non-leaf in the extension hierarchy.
%
% For example, in the following code
%\begin{verbatim}
%struct foo { int x; }
%struct bar { int y; int z; }
%typedef int MY_INT __NOUNROLL;
%#pragma ccured_extends("Sbar", "Sfoo")
%#pragma ccured_extends("Sfoo", "TMY_INT")
%\end{verbatim}
%
% we can use the \RTTI{} pointer kind for \c{struct foo *} and \c{MY\_INT *}
%but not for \c{struct bar}. Notice that in all declared extension
%relationships physical subtyping is respected. 
%
% The inferencer will spread the \RTTI{} pointer kind backwards through
%assignments but only on pointers that can be \RTTI{}. If you want to cut short
%the propagation of the \RTTI{} pointer king you can use the \SAFE{} pointer
%kind. 
%
% To summarize, \RTTI{} pointers can be used with the following constraints:
%\begin{itemize}
%\item The \RTTI{} pointer kind is never inferred by the Deputy inferencer. You
%must specify it on some pointers and then the inferencer will propagate it. 
%
%\item The \RTTI{} pointer kind is not able to carry bounds information. Thus
%you cannot use it on pointers that are involved in pointer arithmetic. 
%
%\item Only pointers to extensible types can be cast to and from \c{RTTI}
%pointer types. Additionally, you may cast scalars into \c{RTTI} pointers. 
%
%\item You must use \c{ccured\_extends} pragmas to declare the extension
%hierarchy. 
%
%\item \c{void*} polymorphism is turned off for the \_\_RTTI types.
%\end{itemize}
%
% Interestingly enough the \RTTI{} pointer kind can be used to implement in a
%type-safe way virtual method dispatch, as shown in the example below:
%\begin{deputycode}
%typedef struct parent {
%  void * __RTTI * vtbl; // virtual table, with various types of functions
%  int  *f1;             // some field
%} Parent;
%
%#pragma ccured_extends("Schild", "Sparent")
%
%typedef struct child {
%  void * __RTTI * vtbl;
%  int  *f2;
%  int   f3;
%} Child;
%
%// virtual method foo for class P
%// notice that the self parameter is an RTTI. It must 
%// be of base type void to ensure that foo_P and foo_C have the 
%// same type
%int* foo_P(void * __RTTI self_rtti, Parent *x) {
%  Parent * self = (Parent *)self_rtti; // downcast
%  return self->f1;
%}
%
%// virtual method bar for class P
%int * bar_P(void * __RTTI self_rtti) {
%  Parent * self = (Parent *)self_rtti;
%  return self->f1;
%}
%
%int* foo_C(void * __RTTI self_rtti, Parent *x) {
%  Child * self = (Child *)self_rtti;
%  return self->f2 + self->f3;
%}
%
%// Name the types of the virtual methods, to make them extensible
%typedef int * FOO_METHOD(void *, Parent *) __NOUNROLL;
%typedef int * BAR_METHOD(void *) __NOUNROLL;
%
%// Now the virtual tables
%void * vtbl_P[] = { (void*) (FOO_METHOD *)foo_P,
%                    (void*) (BAR_METHOD *)bar_P };
%
%
%// child inherits bar_P
%void * vtbl_C[] = { (void*) (FOO_METHOD *)foo_C,
%                    (void*) (BAR_METHOD *)bar_P };
%
%
%int array[8];
%
%// Now the constructors
%void ctor_P(Parent * p) {  p->vtbl = vtbl_P; p->f1 = array; }
%
%void ctor_C(Child * c) {  c->vtbl = vtbl_C;  c->f2 = array;  c->f3 = 5; }
%
%int main() {
%  Parent p;
%  Child c;
%  Parent * pp = &p, * pc = &c;
%  Child  * pc1;
%      
%  // Construct
%  ctor_P(&p); ctor_C(&c);
%
%  // Now try a downcast
%  pc1 = (Child * __RTTI)pc;
%  // Now invoke some virtual methods
%  {
%    FOO_METHOD *pfoo = (FOO_METHOD *) pp->vtbl[0];
%    pfoo((void *)pp, pc);
%    pfoo = (FOO_METHOD *) pc->vtbl[0];
%    pfoo1((void *)pc, pp);  
%   }
%}
%\end{deputycode}
%
% Notice the use of the \c{\_\_NOUNROLL} typedefs for the function types. 
%
% \subsection{Implementation Details}
%
% Deputy collects all extensible types in your program (either those declared
%using the \c{ccured\_extends} pragma or those that are used in casts to and
%from \RTTI{} pointers) and constructs the extension hierarchy. An encoding of
%this hierarchy is dumped in the resulting code in the array \c{RTTI\_ARRAY}.
%Each entry in the array corresponds to an extensible type and it contains the
%difference between the entry corresponding to the parent of the extensible
%entry and the index of th current entry. The root of the extension hierarchy
%is always at index 0 and that entry contains 0. The function
%\c{CHECK\_RTTICAST} is used to walk this encoding to verify a cast from a
%\RTTI{} pointer into a \SAFE{} pointer or another \RTTI{} pointer. 



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Specifying Trusted Code}\label{sec-trusted}
\TODO{this section}

 In this section we describe a few mechanisms that you can use to override
Deputy's reasoning. These are powerful mechanisms but you can use them to
write unsafe code. 

 \subsection{Trusted casts}

 Occasionally there are casts in your program that are judged as bad, yet you
know that they are sound and it is too inconvenient to change the program to
expose the soundness to Deputy. In that case, you can use the
\c{TC} built-in function. In the following example we know that
the \c{boxedint} type can encode an integer (if odd) or a pointer to a
\c{boxedint} if even. We could use \RTTI{} pointers to encode this safely in
Deputy. Or, we can use a trusted cast:
\begin{deputycode}[fails]
typedef void * boxedint; // If even, then a pointer to a boxedint
int unroll(boxedint x) {
  if((unsigned long)x & 1) return x;
  return unroll(* (boxedint * SAFE)TC(x));
}
\end{deputycode}
\TODO{Why does this code fail? Fix it, and remove the fails annotation}

 Deputy will not complain if the argument and result type of
\c{TC} are incompatible. However, it will ensure the following:
\begin{itemize}
\item A \c{TC} acts as a cast from the point of view of
  propagating the \SEQ{} and \FSEQ{} requirement. This means that both the
  argument and the result type will have the same kind. 
%\item The argument and the result type are compared and in those pointer types
%  in them that correspond, are forced to have the same kind.
\end{itemize}

 For example, in the following example, the variable \c{q} and the field
\c{f1} in \c{struct foo} are made \FSEQ{}. The \FSEQ{} constraint propagates
back through \c{TC} to \c{p}.
%\begin{deputycode}
%struct foo {
%   int   * f1;
%   int     f2;
%};
%struct bar {
%   int   * f1; 
%   int   * f2;
%};
%int main(struct bar * p) {
%    struct foo * q = TC(p);
%    p->f1 ++;        // Make foo.f1 FSEQ
%    return q[1].f2; // Make q FSEQ
%}
%\end{deputycode}

 If you look carefully at the above examples you will see one of the potential
dangers of using \c{TC}: you are on your own to ensure that the
argument type and the result type match. In the above example, this is not
true because the field \c{f1} in \c{struct bar} is \SAFE{} while the field
\c{f1} in \c{struct foo} is \FSEQ{}!

 If you want to prevent a pointer arithmetic operation from generating
sequence pointers, you can use the \c{TC} function:
\begin{deputycode}
int foo(int *p) {
    int * q = TC(p) + 4;
    return *q;
}
\end{deputycode}

 You can use a \c{TC} to cast an integer into a pointer. This
works as expected if the type of the resulting pointer is \SAFE{} (as in the
example with \c{boxedint} earlier in this section). But if it is \FSEQ{} or
\SEQ{} then you will get exactly the same effect as if the
\c{TC} was not there: you will obtain a pointer with null
metadata and thus unusable for memory dereference.


 \subsection{Turning off Deputy}

 You can turn the curing off for a fragment of a source file, for a function,
or for a block statement. 

% You can use the \t{cure} pragma to turn curing off for a fragment of a source
%file (in Deputy pragmas can only appear at global scope and therefore you
%cannot use this mechanism to turn curing off for part of the definition of a
%global function):
%%\begin{deputycode}
%%int * g; // This is a pointer to several integers
%%         // but we do not want to make it SEQ
%%#pragma ccured(off)
%%int foo() {
%%   return g[2]; // Deputy won't see this and will leave g SAFE
%%                // But also Deputy won't check this code
%%}
%%#pragma ccured(on)
%%\end{deputycode}
%
% Alternatively, you can add the \t{nocure} attribute to a function to tell
%Deputy to not cure this function:
%
%\begin{deputycode}
%int * g; // This is a pointer to several integers
%         // but we do not want to make it SEQ
%
%// We must put the attribute in a prototype
%int foo(void) __NOCURE;
%int foo(void) {
%   return g[2]; // Deputy won't see this and will leave g SAFE
%                // But also Deputy won't check this code
%}
%\end{deputycode}
%
% At a finer-grained level, you can use the \t{\_\_NOCUREBLOCK} attribute with
%a block statement:
%\begin{deputycode}
%int * g; // This is a pointer to several integers
%         // but we do not want to make it SEQ
%
%int foo(void) { 
%   int res;
%   { __NOCUREBLOCK
%     res = g[2]; // Deputy won't see this and will leave g SAFE
%   }
%   return res; 
%}
%\end{deputycode}
%
% In all of these cases, the Deputy inferencer does not even look at the
%non-cured portions of the code. However, Deputy will at least change the
%non-cured code to access the fat pointers properly. For example, in the
%following example the global \c{g} is a sequence pointer. While Deputy will
%not complain about the unsafe cast to \c{int **}, it will make sure that at
%least the proper component of \c{g} is used:
% 
%\begin{deputycode}
%int * g; // This will be FSEQ
%
%int ** foo(void) { 
%   int res = g[2]; // Make g FSEQ
%   { __NOCUREBLOCK
%     return (int **)g; // But not WILD
%   }
%}
%\end{deputycode}
%
% Finally, to avoid curing a whole source file (say \t{trusted\_foo.c}), you can
%use the \t{--leavealone=trusted} argument to Deputy. All source files whose
%names start with the given ``leave alone'' prefix, are not merged and are not
%scanned by Deputy at all. Instead they are compiled with \t{gcc} and linked in
%the final executable. 





%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    \section{Function Pointers}\label{sec-funptr}
\TODO{this section}

 One of the signs that a C program is a ``serious'' one is the use of function
pointers. There would be nothing wrong or unsafe about that if it wasn't also
the case that most programmers do not feel necessary to use accurate types for
function pointers, or to even use function prototypes. This is probably due to
the fact that the syntax for function types in C is terrible. How often have
you declared your function pointers to have type \c{void (*)()} when you
actually wanted to say \c{int * (* (* x3))(int x)(float)} (a pointer to a
function that takes an \c{int} and returns a pointer to a function that takes
a \c{float} and returns a pointer to an \c{int}).

 Of course, misusing function pointers can lead to the worst kind of errors.
Fortunately such error rarely go unnoticed in code that is executed. 

 Deputy supports two kinds of function pointers. The \SAFE{} function pointers
can only be invoked with the same number of arguments. If the types of the
arguments are not right it is the argument that becomes \WILD{} not the
function pointer. A \SAFE{} function pointer can only be cast to an integer or
to the same function pointer type. We also have \WILD{} function pointers
which you can (try to) use as you please. In fact a \WILD{} function pointer
can be cast to any other \WILD{} pointer type and can be stored in any tagged
area. For this reason its representation must match that of any \WILD{}
pointer. However the capabilities of a \WILD{} function pointer are typically
quite different from those of a regular function pointer. For example, you
should not be able to read or write from a function pointer. 

 Any function whose address is taken and becomes \WILD{}, or that is used
without a prototype (see the discussion at the end of this section) is a {\em
tagged function} and has an associated descriptor that encodes the actual code
to the function and the number of arguments. Here is an example:

%\begin{deputycode}
%int taggedfun(int anint, int * aptr) {
%    return anint + * aptr;
%}
%
%int main() {
%  int * i = taggedfun; // Bad cast. wildfun becomes tagged
%  // Now we invoke it
%  ((void (*)(int,int*))i)(5, i);
%}
%\end{deputycode}

 The structure of a function descriptor is as shown below and a pointer to the
\c{\_pfun} field is used as the \c{\_b} field whenever the address of the
function is taken.

\begin{code}
struct __functionDescriptor {
  unsigned int _len ; // Always 0
  void (* _pfun)() ; // Pointer to a function
  unsigned int _nrargs ; // The number of arguments
};
\end{verbatim}\end{code}

 Since the \c{\_len} field is always initialized to zero, whenever this
\WILD{} pointer is used for a read or a write it would appear that it points
into a zero-length tagged memory area, so the bounds check will fail. We then
have to protect against the pointer being subject to arithmetic prior to
invocation. We do this by storing in the function descriptor the actual
pointer to the function and checking at the time of a call through a \WILD{}
function pointer that the \c{\_p} field of the pointer is equal to the
\c{\_pfun} field in the descriptor. 

 Finally we have to ensure that the function is called with the right number
and kinds of arguments. There is no hope to be able to ensure this statically
because a \WILD{} function pointer can be used very liberally as any other
\WILD{} pointer. So, Deputy conservatively forces
all arguments and the return type to be \WILD{} pointers. This includes
arguments and return types that are actually scalars (see the example above
for how integers are wrapped into \WILD{} pointers). This will ensure that the
types are the same (or compatible) and all we have to check is the right
number of arguments is passed to the function. To perform these checks we use
the following run-time support function:
\begin{code}
/* Check that a function pointer points to a valid tagged function and check
   that we are passing enough arguments. We allow the passing of more
   arguments than the function actually expects */
__CHECK_FUNCTIONPOINTER(void *_p, /* The _p field of the function pointer */
                        void *_b, /* The _b field */
                        int nrActualArgs); /* The number of actual arguments */
\end{verbatim}\end{code}

 Also, {\em always use prototypes for the external functions you are using}.
Otherwise, it will appear to Deputy that you are casting the function pointer
to various incompatible types corresponding to each use and the function will
be declared tagged (and pointers to such function to be \WILD{}). You get some
help from Deputy here because its whole-program merger will construct
prototypes for the functions that are defined somewhere in your program. But
when you use even simple things like \c{printf} you must include the proper
header files. 


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \section{Global Initialization}\label{sec-globinit}
\TODO{this section}

 C has a very rich language of initializers for globals and locals. The
language is so rich that neither \c{gcc} nor MSVC implement it fully. For a
discussion of how our front-end handles initialization, please see the \ahref{../cil/index.html}{the CIL documentation}.
 
 Once programs are presented to Deputy all the initialization for locals is
turned into assignments, but most initialization code for globals is
preserved. However, in some cases Deputy must insert some checks related to
the initializers. These checks are placed in a special function called a {\em
global initializer}.



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%5
     \section{Casting Integers to Pointers}\label{sec-castint}
\TODO{this section}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       \section{Variable argument functions}\label{sec-vararg}
\TODO{this section}

 Variable-argument functions in C are inherently unsafe since there is no
language-level mechanism to ensure that the actual arguments agree in type and
number with the arguments that the function will be using. There are several
ways to implement variable argument functions in C and Deputy supports some of
them quite well:
\begin{itemize}
\item You can try to implement such function by taking the address of a formal
argument and working your way through the stack frame. If you do this we wish
you luck and perseverance and you'll need them both while trying to figure out
why your program does not behave for compilers such as \c{gcc}. Deputy
certainly cannot allow this because this is exactly the kind of operation that
viruses would want to perform.
\item A better alternative is to use the \c{\_\_builtin\_next\_arg} function on
\c{gcc} and then work your way up the stack. Deputy does not support this
low-level implementation of variable argument functions, but see next.
\item You can write your variable argument functions using the standard macros
in \c{<stdarg.h>} and \c{<vararg.h>}. Deputy supports most such functions with
minimal programmer intervention.
\end{itemize}


 There are two kinds of variable-argument functions in C:
\begin{itemize}
\item Those that take an arbitrary number of arguments following the last
specified formal (their function type contains \c{...} after the last formal).
We'll call these functions {\em vararg} functions. An example is \c{printf}:
\begin{code}
int printf(const char* format, ...)
\end{verbatim}\end{code}

\item Those that take as arguments one or more pointers to lists of arguments.
We'll call these functions {\em valist} functions. An example is \c{vprintf}:
\begin{code}
int vprintf(const char* format, va_list args)
\end{verbatim}\end{code}
\end{itemize}

 Deputy supports both kinds of functions and will scan the program to find out
for each function what types of arguments are passed. In \secref{manualvararg}
we describe how the programmer can prevent this automatic inference by
specifying the set of types of arguments. 

 Deputy redefines the macros in \c{<stdarg.h>} and \c{<vararg.h>} to do
special bookkeeping. In vararg functions, the macro \c{va\_start} is used to
initialize an \c{va\_list} variable to point to the trailing arguments. Deputy
checks that the second argument is the last formal before the \c{...}.

 Both in vararg and valist functions the macro \c{va\_arg} can be used, as
follows: 
\begin{code}
 T x = va_arg(args, T)
\end{verbatim}\end{code}

 \c{args} must be a \c{va\_list} variable and \c{T} must be compatible after
the usual actual argument promotions (e.g. \c{char} and \c{short} to \c{int}
and \c{float} to \c{double}) with one of the types in the \c{struct} associated
with \c{args}. Deputy checks this at run-time.

 The Deputy support for variable argument functions is quite flexible.
Multiple variable argument lists can be processed in parallel, an argument
list can be re-initialized with \c{va\_start} and processed multiple times. A
function can even work with variable argument lists that have different sets
of types accepted (but for this you need to specify manually the set of types
of arguments as explained in \secref{manualvararg}). Variable argument lists
can be passed down but the regular Deputy checks for stack allocated variables
will prevent the passing of these lists up the call chain and also their
storing in the heap.

 The main thing that is not supported in Deputy is the fetching of an argument
with a different type than it was stored. It remains to be seen if this is a
problem. We have looked at several variable argument functions (including full
implementations of \c{printf} and \c{sprintf}) and so far we have found that
Deputy accepts those functions without any change except for the specification
of the \c{struct} of the accepted argument types (as explained below).


    \subsection{Programmer control over vararg functions}
    \label{sec-manualvararg}

 If you do not want Deputy to find automatically all the types that can be
passed to a function, you can specify the set of types that can be used for
arguments. Also, you should not let Deputy infer the argument types for
\c{printf}-like functions, but you should instead use the special support for
them, as explained in \secref{printf}.

  You can declare the argument types by declaring a descriptor. This is a
\c{struct} data type whose fields have the types that can be passed to the
function. The order and the names of the fields do not matter. For example,
such a struct for \c{printf} would be the following (this structure is defined
in \t{ccured.h}):
\begin{code}
struct printf_arguments {
   int      f_int;
   double   f_double;
   char    *f_string;
};
\end{verbatim}\end{code}

 The simplest way to specify that such a \c{struct} describes the types of
arguments for a variable argument function is to use a pragma:
\begin{code}
#pragma ccuredvararg("myvarargfunction", sizeof(struct printf_arguments))
\end{verbatim}\end{code}

Notes:
\begin{itemize}
\item Since most variable argument functions are \t{printf}-like, Deputy
  provides special support for them. See \secref{printf} if your function is
  of this kind. 

\item Note that Deputy predefines the \c{struct printf\_arguments} so you do
not have to redefine it.

\item Like all Deputy pragmas, you can put them anywhere in your project since
Deputy is going to merge all files into one. However, I typically prefer to
put such pragmas in header files near the prototype for the function.

\item This method does not work for specifying pointers to variable argument
  functions. You must use the attribute method described below.

\item The \c{sizeof} operator is there because the syntax of pragmas is pretty
much that of function calls and thus we cannot use types directly. 

\item This pragma can be used with both kinds of
variable argument functions. In the case of valist functions it specifies that
{\em all} formals and locals of type \c{va\_list} can hold arguments of the
given types. 
\end{itemize}

 An equivalent method is to associate the \c{\_\_DEPUTYVARARG(struct
printf\_arguments)} attribute with the type of the function
\c{myvarargfunction}:
\begin{code}
int (__DEPUTYVARARG(struct printf_arguments) myvarargfunction)(int last, ...);
\end{verbatim}\end{code}

 You have to use this method if you want to specify that a function pointer is
variable argument:
\begin{code}
int (__DEPUTYVARARG(struct printf_arguments) * myvarargptr)(int last, ...);
typedef int (_DEPUTYVARARG(struct printf_arguments) fptr)(char *format,...);
\end{verbatim}\end{code}

 A more fine-grained way to specify the same thing is to use the
\c{\_\_DEPUTYVARARG} {\em type attributes} for \c{va\_list} every time it appears.
This allows you to specify different sets of types for different locals:
\begin{code}
va_list __DEPUTYVARARG(struct printf_arguments) args1, 
        __DEPUTYVARARG(struct some_other_type) args2;
\end{verbatim}\end{code}


         \subsection{Printf-like functions}\label{sec-printf}

 Since the vast majority of uses of variable argument functions if for
\c{printf}-like functions, Deputy contains special support for them.
Specifically if a vararg function is declared to be a \c{printf}-like function
then all of its invocations in which the format string is a constant will be
checked statically. For the other invocations a wrapper for printf will be
called that will check the types of the actuals against the format string
before calling the real \c{printf} function.

 To declare a function to be \c{printf}-like use the following pragma:
\begin{code}
#pragma ccuredvararg("myprintf", printf(1))
\end{verbatim}\end{code}

 where the last argument is the index of the format argument in the argument
list (starting with 1). Note that you will get a run-time error if you try to
use the \c{va\_arg} macro in the implementation of such a function. In those
implementations you should invoke functions like \c{vprintf} and \c{vsprintf}
instead.

 GCC already has support for communicating to the compiler that a function is
\c{printf}-like. This is done as follows:
\begin{code}
int myprintf(const char* format, ...) __attribute__((format(printf, 1, 2)))
\end{verbatim}\end{code}
 
 where the ``1'' means that the first argument is the format string and the
``2'' means that we should start checking with the second argument. Deputy
recognizes this attribute and it considers it equivalent with the
\c{ccuredvararg} from above. Note that the second argument in the
\c{format} attribute is ignored in Deputy.

 You can use the \t{format} attribute even for function pointers:
\begin{code}
int (__attribute__((format(printf, 1, 2))) *myptr)(char *format, ...);
\end{verbatim}\end{code}

 Note that Deputy does not currently like passing pointers to \c{printf} with
the intention of printing the pointer value. You should manually cast those
pointers to \c{long} when passing them to \c{printf}-like functions.

 Also, you should not let Deputy infer automatically the descriptors for
\c{printf}-like functions. Otherwise, it is quite likely that the descriptor
that will be inferred is different than the built-in descriptor
\c{printf\_arguments} (which the runtime library is using to check the calls
to \c{printf}-like functions. Deputy will warn you about all automatically
inferred descriptors and you should manually inspect all the functions
involved. 


 As for the regular variable argument functions, the \t{pragma} works only for
named functions but not for pointers to functions. For that purpose you must
use attributes: 

\begin{code}
int (__DEPUTYFORMAT(1) * myprintf)(char *format, ...);
typedef int (_DEPUTYFORMAT(1) fptr)(char *format,...);
\end{verbatim}\end{code}

 
         \subsection{Scanf-like functions}\label{sec-scanf-like}

 Since it proved too much trouble to handle \c{scanf}-like functions in a safe
yet transparent way we currently require the programmer to rewrite the
invocations to \c{scanf} using a number of functions that we provide. For
example instead of 
\begin{code}
  int entry;   double then;   char buffer[6];

 ... fscanf(file, "Entry:%d;  Then:%lf;  5 digits:%5[0-9]; useless text.", 
            &entry, &then, buffer) ...
\end{verbatim}\end{code}

 you should write
\begin{code}
 ... (resetScanfCount(), 
      entry = ccured_fscanf_int(file, "Entry:%d"),
      then  = ccured_fscanf_double(file, ";  Then:%lf"),
      ccured_fscanf_string(file, ";  5 digits:%5[0-9]", buffer), 
      ccured_fscanf_nothing(file, "; useless text."), //advance the file pointer.
      getScanfCount ()) ...
\end{verbatim}\end{code}

 The functions \c{resetScanfCount} and \c{getScanfCount} are necessary only
if you use the result of the call to \c{fscanf} in the original code. Note
that our replacement \c{scanf} functions can be used to return only one result
at a time, consequently the format string that is passed must contain only one
format specifier, possibly along with characters to be matched. 

 The following are the \c{scanf}-like functions that we currently support:
\begin{code}
  extern int    ccured_fscanf_int(FILE *, char *format);
  extern double ccured_fscanf_double(FILE *, char *format);
  extern void   ccured_fscanf_string(FILE *, char *format, char *string);
  extern void   ccured_fscanf_nothing(FILE *, char *format);
\end{verbatim}\end{code}

 If the original program uses \c{scanf}, just consider that you are using
\c{fscanf} from \c{stdin}. If instead your program contains \c{sscanf} then
you can use the function 
\begin{code}
void resetSScanfCount(char *string);
\end{verbatim}\end{code}

to dump the string to the temporary file \c{ccured\_sscanf\_file}
then use the replacement for \c{fscanf} from above.  For example, 

\begin{code}
 ... (resetSScanfCount(inputString), 
      entry = ccured_fscanf_int(ccured_sscanf_file, "Entry:%d"),
      then  = ccured_fscanf_double(ccured_sscanf_file, ";   Then:%lf"),
      ccured_fscanf_string(ccured_sscanf_file, ";   5 digits:%5[0-9]", buffer), 
      getScanfCount ()) ...   //getScanfCount is required when using resetSScanfCount
\end{verbatim}\end{code}

 {\bf Note that the current support for \c{scanf} is far from satisfactory and
 will likely change in the future}


           \subsection{Implementation Issues}

 Almost all of the checking for variable-argument functions is done at
run-time. At the time of a call each actual argument is compared with the
types in the \c{struct} associated with the vararg function. A global data
structure is filled with the number of arguments (in the global
\c{\_\_ccured\_va\_count} and a list of indices describing for each actual
argument the index within the \c{struct} types (in \c{\_\_ccured\_va\_tags}). 

 In the body of a vararg function, a data structure is allocated on the stack
to hold a copy of the global description of the arguments that was created by
the caller. The call to \c{va\_start} initializes this data structure and each
call to \c{va\_arg} checks that we are not reading past the end of the
actuals and also that the type of the fetched argument matches that of the
actual argument. 




%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \section{Annotated Lengths}\label{sec-dependent}

Programmers can annotate array pointers with length attributes.
Deputy will then use the annotated length whenever it needs to do a
bounds check on that pointer, instead of transforming the pointer into
a fat pointer.  This has two advantages: 
\begin{itemize}
\item Deputy will not need to change the representation of this
  pointer, which improves compatibility with precompiled code.
\item Using a Deputy fat pointer to store the length of a buffer may
  be redundant if the program already maintains a similar length value
  near the pointer.
\end{itemize}

Length annotations are allowed in two situations:  struct fields may
have length annotations that depend on the values of other fields in
that struct, and function parameters may have lengths that depend on
other parameters in that function. (NB: but the annotations on
function parameters are not yet implemented.  Coming soon ...)
% TODO: return values, constant expressions, etc.

Only pointer types may be annotated.  The annotation
\c{\_\_SIZE($exp$)} on a field means that the associated pointer is
$exp$ bytes long, where the expression $exp$ can involve integer
constants, arithmetic, \t{sizeof}, and the names of other fields in
the same struct.  So \c{\_\_SIZE(1 + foo)} means that the specified
pointer has a length that's one greater than the runtime value of
field foo in the same object.

\c{\_\_COUNT($exp$)} means that the pointer is $exp$ elements long.
So when annotating a pointer with type \c{T*}, the
annotation \c{\_\_COUNT($exp$)} is equivalent to \c{\_\_SIZE($exp$ *
sizeof(T))}.

Any field that is referred to by a \c{\_\_SIZE} or \c{\_\_COUNT}
annotation is a {\em metadata field}.  When a metadata field is
modified, any pointer fields that depend on it are set to NULL.  {\em
Therefore, when writing both the metadata and pointer fields, programs
must always modify the metadata first, followed by the pointer.} 

 When an annotated pointer field is read, Deputy will read any
metadata fields as well, and associate that length with the pointer.
When a pointer field is written, Deputy will check that the buffer's
length is less than or equal to the length specified by the current
value of the metadata fields.

\begin{deputycode}
extern void* (DALLOC(sz) malloc)(int sz);

struct bar {
  int nrInts;
  int *ints COUNT(nrInts);
};

struct foo {
  int sizeBars;
  struct bar * bars COUNT(sizeBars);
};

// Now the function that uses it

void init(struct foo* pFoo) {
  int nrBars = 5;
  pFoo->sizeBars = nrBars * sizeof(* pFoo->bars);
  pFoo->bars = (struct bar*)malloc(pFoo->sizeBars);
}
\end{deputycode}


In this code, we first overwrite the field \t{pFoo->sizeBars}, which
automatically sets the field \t{pFoo->bars} to NULL.  The next step is
to write a new pointer to the \t{pFoo->bars} field.  During this
write, Deputy will check that the pointer being written (in this case,
the result of \t{malloc}) is at least ``pFoo->sizeBars'' bytes long.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \section{Memory Management}\label{sec-gc}
\TODO{this section}

 The high order bit: we use the Boehm-Weiser garbage collector. 

 TODO : finish this section

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \section{Deputy Pragmas}\label{sec-pragma}
\TODO{this section}
 
% ======================================================================
\chapter{Deputy Warnings and Errors}\label{ch-warn}
\TODO{this section}

 As you use Deputy you might encounter various kinds of problems. Most of
these are due to a combination of aggressive coding practices and Deputy being
less smart than the programmer. (Note: this section is continuously being
expanded; if you do not see the answer to your question, or if the answer is
not helpful, let us know).


%%%%%%%%%%%%%%%%%%%%%%%
\section{Compile-time Errors}\label{sec-warn-compile}
\begin{itemize}
\item Type mismatch: If Deputy sees an assignment where the types on the left-
  and right-hand sides aren't compatible, it will print this error. Either fix
  the types or insert a trusted cast by putting \c{TC(...)} around the
  right-hand side.

\item Incorrect allocation type: Deputy expects to be able to infer the type
of an allocation (e.g., \c{malloc}) from the right-hand side alone. The
argument to \c{malloc} should be of the form \c{e * sizeof(t)}, where \c{e} is
an expression containing constants, locals, *, and +. You can omit the
\c{sizeof(t)} if \c{t} is \c{char}. If \c{t} is void, you'll have to specify
\c{sizeof(void)} (which is, surprisingly enough, equal to 1). (This could be
better, I know!) \TODO{this explanation should be in memory allocators}

\item Missing WHEN expression: If Deputy sees a union whose fields are
unannotated, it will complain. You can add \c{WHEN(e)} to each item, or you
can choose to trust the union by placing \c{TRUSTED} after the \c{union \{ ...
\}} definition.
\end{itemize}


%%%%%%%%%%%%%%%%%%%%%%%%%%55
%%%%%%%%%%%%%%%%%%%%%%%%%%% RUNNING
\section{Run-time Errors}\label{sec-warn-run}

 When you run the code you might get run-time errors. Make sure you read the
\chref{invoke} on ways to control the handling of errors. 

\begin{itemize}

\item \TODO{The run-time errors}

\end{itemize}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%55
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\chapter{License}

Copyright (c) 2005-2006,
\begin{itemize}
\item Jeremy Condit       <jcondit@cs.berkeley.edu>
\item George Necula       <necula@cs.berkeley.edu>
\end{itemize}
All rights reserved.

Redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions are met:

1. Redistributions of source code must retain the above copyright notice,
this list of conditions and the following disclaimer.

2. Redistributions in binary form must reproduce the above copyright notice,
this list of conditions and the following disclaimer in the documentation
and/or other materials provided with the distribution.

3. The names of the contributors may not be used to endorse or promote
products derived from this software without specific prior written
permission.

THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
POSSIBILITY OF SUCH DAMAGE.

\chapter{Bug reports}

 If you find a bug in Deputy, please send email to
\ahref{mailto:jcondit@cs.berkeley.edu}{Jeremy Condit}.

\chapter{Changes}\label{sec-changes}\cutname{changes.html}

 Below are some of the changes in the Deputy system. These are in addition to
\ahref{../cil/changes.html}
{changes made to the underlying CIL infrastructure}

\begin{itemize}
\item {\bf May 1, 2006} First version of this manual.
\end{itemize}


 
\appendix


 
% ========================= Regression Tester ========================
\chapter{Using the Regression Tester}\label{ch-regtest}

 The regression tester is a program that allows you to do two things: 
\begin{itemize}
\item Run a list of shell commands and capture their standard and error output
 in a log file, and

\item Analyze such log files and extract various information, among which the
 most important is which test cases have succeeded and which have failed. 

\item Compare results of two runs according to many parameters, such as
whether the test succeeded or not, how much time Deputy took to process it,
how many different kinds of pointers were inferred and how fast is the
resulting program. 
\end{itemize}

 Since the running of the tests and the analysis of the output is separated
you can easily do things like compare the results on multiple runs, extract
various reports from a single output (like what tests have succeeded, which
have failed, plus such information split by test groups). You can also extract
some data from each test (such as the running time) and make simple reports. 

 Test cases can have comments associated with them (such as reminders of why
it fails) and can be associated with zero or more test groups.

 \section{Running the regression}\label{sec-regtest}

 The regression tester is implemented in Perl as "\t{runtests.pl}", which in
turn contains simple wrappers for functions provided by the more generic
\t{RegTest.pm}.

 The regression tester uses relative paths so it must be run in the
 \t{deputy/test} directory.

 The basic command for running the tests is "\t{runtests --run}". This runs
all of the test cases, saving the log in the file "\t{runtests.log}". Before
creating this file, it renames previous versions of this file as
"\t{runtests.log.<n>}" where n is an integer starting from 1 to a maximum number
that is configurable.

 The following command line options are useful for running the tests (see
 "\t{runtests --help}" for a complete list:

\begin{verbatim}
 --one <testname>       : runs only the named test
 --gory                 : shows lots of details about the execution of the
                          test, such as the commands executed
 --dryrun               : only pretends to run the test. Useful to see what
                          would be run
 --log                  : select the base name of the log file (default
                          "safec.log")
 --logversions <n>      : keep logs up to version <n>. Default is 5.
 --noremake             : runs the commands without trying to remake the safec
                          compiler before each test. Useful if you want to 
                          work on the compiler while the tests are running
 --safecdebug           : uses the DEBUG version of the safec compiler and
                          uses the C compiler in debug mode. By default it
                          used the RELEASE version and the optimizing compiler.



 --group <groupname>    : adds all the tests in the named group to the list of 
                          tests to be run or to participate in the analysis of
                          the log. (Right now we have NO groups)
                          If no such option is
                          specified then all tests are selected. Multiple such
                          options can be given and are cumulative. 
 --nogroup <groupname>  : excludes the tests in the named group from running
                          or from the analysis. Multiple such options can be
                          given and are cumulative. These options are
                          processed after all --group options have 
                          been processed. 

 --listtests            : list the tests that are enabled along with their
                          group membership. This is useful to find out what
                          tests and groups exist.

 --stoponerror          : stop at the first error
 --showoutput           : show the output on the console. Normally output is
                          saved in a file.  
\end{verbatim}

 \section{Analyzing the results}

 The basic command for analyzing log files is "\t{runtests}". This will
prompt the user to select one of the several log files that exist in the
current directory and then (by default) it will print a list of the failed
test cases, with a short (user provided) comment and the last error message
detected in the output for that test case.

 The following commands are useful during analysis:
\begin{verbatim}
 --log                  : select the log file (see above)
 --group, --nogroup     : select groups (see above)
 --listtests            : list tests and groups (see above)
 --param=<pnames>       : show a report about the successes, with the columns
                          being the named parameters (separated by ,). Run
                          "testsafec --help" to see what parameters are
                          available. Use --param=ALL to make a report with 
                          all available parameters.
 --sort=<pnames>        : sorts the report by the given parameters. 
\end{verbatim}

 Furthermore, the reports that are generated can be compared. To compare the
 results of two runs (whose logs are say ``runtests.log.1'' and ``runtests.log.2'',
 run 

\begin{verbatim}
 test/compare runtests.log.2 runtests.log.1 --group=slow
\end{verbatim}

 This will compare the results of \t{runtests.log.2} using as reference the
results in log \t{runtests.log.1}.

 \section{Configuring the regression}


 For this you have to edit runtests.pl. You will see a large section in the
 middle of the file containing lines like:

\begin{verbatim}
addDeputyTest("foo");
\end{verbatim}


 (check out the definition of \t{addDeputyTest} at the bottom of the file). 
 This adds the test named "\t{foo}", which processes \t{test/small/foo.c}.


 To add just one test do:

\begin{verbatim}
    $TEST->newTest(Name => "mytestname",
                   Dir => "..",
                   Cmd => "make something",
                   Enabled => 1,
                   Comm => "Print this along with the test name",
                   Group => ["mygroup"],
                   Patterns => \%mypatterns);
\end{verbatim} % $
 Sometimes you might want to add just a comment or to add one group to a
 certain test. Use the following simple functions: 

 There are some wrappers defined at the end of runtests.pl:

\begin{verbatim}
  addBadComment("li-box", "bug in box.ml");
\end{verbatim}%$


% ------------------------ automatic tester ------------------
\section{The Automated Regression Tester}

 Every time you commit a change to the DEPUTY repositories you trigger a
 regression test and you should be receiving email with the results. If you
don't then it must be that the automated regression tester is not running or
it has encountered a problem that it cannot fix. 

 The automated regression tester is implemented as a script \t{mk-reports.pl}
and lives in the home directory of user \t{regtest} on \t{manju}. To see
whether the tester is running run \t{ps -Af} and look for a line \t{perl
mk-reports.pl -daemon}. If you do not see any let me know. 

 Here are the operations that are performed by the tester:

\begin{enumerate}
\item A new directory is created under \t{/home/regtest/deputy.nightly}. The name
of the directory encodes the time of the commit (e.g.
\t{2001-12-07\_17\_50\_-0800.dir} is the directory for the commit at 17:50 on
07/12/2001 in the timezone that is 8 hours behind UTC). 
\item A complete copy of DEPUTY is checked out in that directory and
\t{make} is run in there. 
\item Then in the \t{test} directory we run \t{runtests} but only on the
groups that are known to terminate quickly. This run takes about 3 minutes. A
copy of the \t{runtests.log} file generated is saved as \t{/home/regtest/deputy.nightly/2001-12-07\_17\_50\_-0800.runtests.quick.log}.
\item Then we run \t{runtests} again to produce a report with all available
parameters. This report is saved as
\t{/home/regtest/deputy.nightly/2001-12-07\_17\_50\_-0800.report.quick.txt}. In the
event that any of the previous steps fail this file will be created but with
zero length.
\item Then we compare this report both with the previous commit and with a
reference report and a message is sent to the user who performed the commit.
This report is also saved as \t{/home/regtest/deputy.nightly/2001-12-07\_17\_50\_-0800.msg.quick.txt}. 
\end{enumerate}

%%%%%%%%%%%%%%%%%
\chapter{Debugging support}\label{sec-debugger}

 Most of the time we debug our code using the Errormsg module along with the
pretty printer. But if you want to use the Ocaml debugger here is an easy way
to do it. Say that you want to debug the invocation of Deputy that arises out
of the following command:
\begin{verbatim}
ccured --separate -c hello.c 
\end{verbatim}

 You must follow the installation \ahref{../ccured/setup.html}{instructions}
to install the Elist support files for ocaml and to extend your .emacs
appropriately. Then from within Emacs you do
\begin{verbatim}
ALT-X my-camldebug
\end{verbatim}

 This will ask you for the command to use for running the Ocaml debugger
(initially the default will be ``ocamldebug'' or the last command you
introduced). You use the following command:
\begin{verbatim}
ccured --ocamldebug -c hello.c 
\end{verbatim}

 This will run \t{ccured} as usual and invoke the Ocaml debugger when the cilly
engine starts. The advantage of this way of invoking the debugger is that the
directory search paths are set automatically and the right set or arguments is
passed to the debugger. 

 For the \t{make}-based interface to our regression tests you can pass the
argument \t{OCAMLDEBUG=1} to \t{make} to achieve the same effect. 

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\chapter{Experimental Features}

\end{document}


% LocalWords:  unannotated memset
