This version of the document refers to CCured 1.3.5 (based
on CIL 1.3.5) and was last modified on 28th September, 2006
CCured 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. Many programs can be made
memory-safe this way while losing only 10–60% run-time performance (the
performance cost is smaller for cleaner programs, and can be improved further
by holding CCured's hand on the parts of the program that it does not
understand by itself). Using CCured we have found bugs that Purify misses with
an order of magnitude smaller run-time cost.
Small programs can be passed through CCured automatically. For medium size
and large programs you have to hold CCured's hand a bit but we tried to
explain the process clearly in this manual. We have used CCured on programs
such as sendmail, bind, openssl, Apache modules, Linux
device drivers, and the SPEC95 benchmarks. Some of these programs are quite
big (300Kloc) and it can take a few days for somebody to “port” the program
to CCured.
The translator itself is written in Ocaml (a dialect of ML). There is also a
Perl script, ccured, that operates as a drop-in replacement for 'gcc', so
that software packages' existing Makefiles can be used with very minor
changes. Finally, CCured provides a library of runtime functions (including
the Boehm-Weiser conservative garbage collector).
CCured is implemented on top of the CIL framework. for analysis and transformation
of C programs. This one you can use to write easily a program analysis
module that works on ANSI C code as well as on code that uses the GNU C
extensions.
If you are anxious to see CCured in action you can try out our
online demo.
In this manual you can find a tutorial on getting started with CCured
(Chapter 3), 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 took to use CCured on several example programs
(Chapter 6). We suggest that you read the chapters in order and go to
the “Advanced CCured Features” only if you need it. The Chapter 10 (CCured
Warnings and Errors) will help you figure out if you are running into an error
that is covered by an advanced feature.
In addition to this manual, you can find information on CCured in the
research papers that we have written. A comprehensive look at CCured
can be found in our ACM TOPLAS article, which
includes much of the material from the other CCured papers. You may
also be interested in the POPL '02 paper
describing the type system and inference algorithm, and the
“CCured in the Real World” paper from PLDI '03
that discusses several advanced features that we discovered were
important for large legacy systems.
1.1 Authors
CCured was developed primarily by
George Necula,
Scott McPeak,
Westley Weimer,
Matthew Harren and
Jeremy Condit. Other people helped with
various components: Shree Rahul, Raymond To, Aman Bhargava, James Lee, Winston
Liaw.
This work was supported in part by the National Science Foundation under
Grants No. 9875171, 0085949 and 0081588, 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.
CCured works on Linux and MS Windows (Win95 operation is unreliable but Win98
and (highly recommended instead) Win2k or WinXP should work). CCured might
also work on other systems that use gcc, but we have not tried it.
CCured is somewhat sensitive to the version of the compiler that you are
using. More precisely, CCured is sensitive to the format of the system include
files that you are using. When you install CCured 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 CCured. If your include files
are different from those that we used to create the patches then the CCured
installation might fail. At the moment we have tested CCured with the
following compilers:
-
On Windows, cl compiler version 12.00.8168, 13.00.9466, and
13.10.3077. Run cl with no arguments to get the compiler version.
- On Windows, using cygwin and gcc version 2.95.3, and
versions 3.0.4 through 3.4.4.
- On Linux, using gcc version 2.95.3, and versions 3.2 through 3.3.5.
Some of the system include files that CCured depends on are really part of
the standard library. CCured has been tried with the following versions of
glibc: glibc-2.2.3, glibc-2.2.5, glibc-2.2.93, and
glibc-2.3.2. To find out the version of your glibc you can run
/lib/libc.so.6 on Linux.
If you want to use CCured on Windows then you must get a complete
installation of cygwin (make sure you install the development tools such
as gcc and ld as well and the perl interpreter) and the 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 CCured. If you have not done this before
then take a look here. (Don't need to worry
about cvs and ssh unless you will need to use the master CVS
repository for CCured.)
2.1 Get the CCured sources
Download the CCured distribution (latest version is
distrib/ccured-1.3.5.tar.gz). See the Section 13 for recent changes to the CCured distribution.
2.2 Configure and Compile CCured
Run the following commands in the top level directory. If you are using
Windows then at least the configure command must be run from within
bash.
./configure
make
make quicktest (optional)
cd test
make testrun/hello INFERBOX=infer
The configure script tries to find appropriate defaults for your system.
You can control its actions by passing the following arguments:
-
CC=foo Specifies the path for the gcc executable. By default
whichever version is in the PATH is used.
The last line in the above sequence of commands will apply CCured (and then
run the result) on the file test/small1/hello.c. (See the
test/Makefile for the sequence of commands.)
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 CCured for or to extend the patch files so that they
match your includes. It is not hard, and it is explained in the
patcher documentation.
After running make you have built a few executables (in the obj
directory) and have configured the bin/ccured Perl script. If you want to
move this script to another directory (e.g. to /usr/local/bin) make sure
to copy the CilConfig.pm file to the same directory.
Now you can continue with a tutorial (Chapter 3), or you can jump
ahead and find out how to run CCured (Chapter 4).
2.3 Test CCured
Once you have built CCured you can run
make quicktest
This will run a few small examples.
CCured 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 CCured 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.
CCured leaves unchanged code that does not use pointers or arrays. Actually,
CCured 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:
-
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.
- All type and structure declarations are moved to the beginning of the
file.
- 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.
- Anonymous structures and unions are given unique names.
- All implicit casts and conversion are expressed as explicit casts.
- All GNU CC extensions are compiled into regular C code.
For a complete description of the CIL infrastructure see
the CIL documentation.
3.1 CCured Attributes
The most significant difference between C and CCured is that CCured 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 CCured
which pointer kinds you want for your pointers. The same notation is then used
by CCured to explain in the transformed program what pointer kind if inferred
for each pointer.
CCured uses type attributes to express the kind of pointers. Type attributes
exist in a limited form in ANSI C (i.e. the volatile, const and
restrict type qualifiers) and in a richer form in the GCC dialect of C.
CCured, 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, CCured 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 following the * pointer-type constructor and the attribute of a name is
written immediately before the semicolon or the = sign that terminates the
declaration of the name. CCured uses pointer-kinds such as SAFE,
SEQ and WILD and the corresponding attribute are formed by adding two
leading underscores. For example, in the following declaration:
int * __WILD * __SEQ x __SAFE;
the type of x is declared to be a SEQuence pointer to a WILD
pointer (just like pointer-types in C, attributes are read from
right-to-left). The __SAFE attribute in this case applies to the name
x, which in the context of CCured means that whenever we take the address
of the variable x we are going to obtain a SAFE pointer. The type of
such a pointer would be int * __WILD * __SEQ * __SAFE (read as a
SAFE pointer to a SEQ pointer to a WILD pointer to an integer.).
(The complete attribute-parsing rules for CIL are described in the
CIL manual.)
CCured is designed to work on regular C programs (i.e. without pointer-kind
attributes). One of the main features of CCured is that it will analyze your
pointer usage and will find for all pointers in your program what is the best
pointer-kind that can be ascribed to that pointer. However, you can also place
pointer-kind annotations and force CCured to use certain pointer kinds.
3.2 SAFE pointers
The main action in CCured concerns pointers and arrays. 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. CCured allows all the pointer operations that C allows but
gives preferential treatment to pointers that are not subject to arithmetic or
to casts. CCured refers to such pointers as SAFE pointers.
Consider for example this small code-fragment that computes the length of a
linked list:
struct list {
void * car;
struct list * cdr;
};
int length(struct list * l) {
int i = 0;
while(l) {
l = l->cdr;
i ++;
}
return i;
}
Browse the CCured inferred pointer kinds,
or see the CCured output
for this code fragment
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 cured code
that CCured has inferred that these pointers are indeed SAFE.
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:
-
Cannot be subject to pointer arithmetic (adding or subtracting an
integer from it).
- Cannot be cast (except subject to stringent rules which we'll discuss
below). Note that assignment, passing actual arguments and returning are
implicit casts.
- Can be set to a compile-time constant equal to 0 but not to any other
integer expression.
- Can be cast to an integer and can be subtracted from another pointer.
This is useful for comparisons.
- SAFE pointers are represented using the standard C representation
on one word.
- Every time a SAFE pointer is dereferenced, a null check is inserted
before the dereference.
All of these restrictions are such that the following invariant holds for all
SAFE pointers:
A SAFE pointer to type T is either 0 or else it points to a valid area
of memory containing an object of type T. Furthermore, all other pointers
to the same area are also SAFE and agree on the type T of the stored
object.
3.2.1 Safe Casts
Casting a pointer to an integer is always allowed. CCured 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 integers. 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. CCured 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 physical subtyping. For example, in the code shown below, all of
the four casts implicit in the assignments are safe and CCured will infer that
all pointers involved are SAFE.
struct large {
struct small {
int * f1;
int * f2;
} a;
int * f3;
} x;
struct small * s1 = & x;
int * * s2 = & x;
struct { int *a1, *a2, *a3; } * s3 = & x;
struct { int *a1, *a2[2]; } * s4 = & x;
Browse the CCured inferred pointer kinds,
or see the CCured output
for this code fragment
Notice that all of the s1, s2, s3 and s4 are aliases for the
address of 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 CCured infers the WILD kind for the pointers
involved):
int y1;
int * * x1 = & y1; // Cast an int * to a int * *
int y2;
struct { int * a1, a2; } * x2 = &y2;
Browse the CCured inferred pointer kinds,
or see the CCured output
for this code fragment
If the first cast were allowed then by writing to y1 an arbitrary
integer we would be invalidating the assumption that x1 points to a
pointer value. The second cast is similar.
3.2.2 Union types
Further complications arise in the case of union types. A pointer to union
type can be SAFE if it obeys all of the restrictions mentioned above and
also for all two fields of the union type, they agree on the types of the
elements in the overlap. For example, in the code below the type of x can
be a SAFE pointer.
union {
int *f1;
int *f2[2];
struct { int *a1, *a2, *a3; } f3;
} * x;
int* foo() { return x->f1; } //use x so it is analyzed.
Browse the CCured inferred pointer kinds,
or see the CCured output
for this code fragment
But in the following code the type of x cannot possibly be SAFE
because the type of the field f3.a2 does not match the type of the
overlapping field
f2[1] and thus x->f3.a2 could be used to write an arbitrary integer
that can later be interpreted as a pointer using the expression x->f2[1].
union {
int *f1;
int *f2[2];
struct { int *a1, a2, *a3; } f3;
} * x;
int* foo() { return x->f1; } //use x so it is analyzed.
Browse the CCured inferred pointer kinds,
or see the CCured output
for this code fragment
If your program uses a union with incompatible fields you can still obtain
SAFE pointers if you rewrite the union to be a struct. This will
waste some space but in some cases (in which the program requires the type to
have a given size) it might break the semantics of the program.
Or, you can use tagged unions (Section 9.7) in which CCured will
insert run-time checks to ensure that you are not trying to read a pointer for
a field of a union when you wrote a scalar (or an incompatible pointer) using
another field.
3.2.3 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 CCured is if your
program uses external function without prototypes. This makes CCured think
that the function is taking no arguments and returning an integer and every
time you use it in a different way CCured behaves as if you are casting the
function pointer (denoted implicitly by the function's name) to the type
needed in the cast. CCured will print warnings about using functions without
prototype and we recommend that you fix those problems and try CCured again.
For a discussion of what happens when you do not use your function pointer in
a clean way you should read to the end of this tutorial chapter and then read
Section 9.1.
3.3 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 CCured as a call to the function
CHECK_NULL. This and other run-time checking functions used by CCured
have a name that starts with the prefix CHECK_ and are declared in the
file ccuredcheck.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 CCured will
add a run-time check that s is not null before computing the value of
x. Then again there will be a check that x is not null before
dereferencing it.
struct str {
int a, b;
};
int getaddr(struct str * s) {
int * x = & (s->b);
return *x;
}
Browse the CCured inferred pointer kinds,
or see the CCured output
for this code fragment
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 x would be 4 (on most machines) which would break the invariant
and would defeat the second null-check thus letting you dereference an invalid
pointer.
At this point you are starting to see some of the subtleties in the design of
CCured. To ensure that we got everything right we have formalized the type
system of CCured and we proved (for a subset of CCured) that the set of
run-time checks and invariants achieve memory safety. In fact, in the first
implementation of CCured we had forgotten about the first null check in the
above example and the need for it was revealed while trying to prove that
CCured is sound. To read our formalization and see the soundness proofs take a
look at our paper “CCured: Type-Safe Retrofitting of
Legacy Code”.
CCured 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 s is a non-null SAFE pointer
to struct str then &(s->b) is guaranteed to be non-null as well, thus
the second check is not really necessary.
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 offsetof in many C libraries):
struct str {
int a, b;
};
int get_offset_of_b() {
return (int) &(((struct str*)0)->b);
}
Browse the CCured inferred pointer kinds,
or see the CCured output
for this code fragment
CCured recognizes in this specific case that you are casting the result of
the & operator to an integer, so it avoids the run-time check.
3.4 Checks for Returning Pointers
Note: Checks for returning stack pointers have been disabled
in the current version. This was done because recent versions of
gcc perform more aggressive inlining that results in false positives
for our return-pointer checks. For more information, contact the
CCured developers.
One of the unsafe features of C is that the address of a local variable can
be returned from a function and later be used in a context in which the
storage for the local variable has been reused. Many C compilers try to give
warnings when they notice this happening but it is way to easy to fool them.
For example, in the code example below the function bar does return the
address of its local variable and this is going to be missed by most
compilers.
int *foo(int *in) { // in is a stack address
*in = 5;
return in;
}
int* bar() {
int local = 0;
return foo(&local);
}
Browse the CCured inferred pointer kinds,
or see the CCured output
for this code fragment
Each function that returns a pointer value will have one call to
CHECK_RETURNPTR that will verify that the pointer value is not in the
stack frame of the function that is returning. Note that the pointer value can
be 0, or can be a pointer to a heap area or to a cooler stack frame (a
caller stack frame).
There is one complication with the return checks. There is no portable way to
implement the check that a pointer is in the frame of the returning function.
Currently CCured checks that the pointer value is not in the 1Mbyte range
that starts at the current address of the frame pointer going towards lower
addresses. However, getting the address of the frame pointer is somewhat
unreliable in the context of heavy optimizations. The method that seems to
work best is to introduce a volatile local variable whose address is then the
address of the stack frame. Since the address of the variable is taken and the
variable appears first in the local declarations, it appears that both GCC and
MSVC will allocate such a variable at the highest address in the frame.
Note that we have observed the CHECK_RETURNPTR check to lead to spurious
failures in the case when the function returning a pointer is inlined into its
caller. For example, the code example from above the check for the return of
foo should succeed and the one for the return of bar should fail. If
foo is inlined into bar then foo's check will see that in is
in the current stack frame and will generate a run-time error. This is not an
ideal situation and we are looking for a better solution.
3.5 Checks for Writing Pointers
Another possible unsoundness with addresses of local variables is when the
address of a local variable is written to a global or to the heap. In that
case the pointer value might be used later at a time when the underlying
storage is being reused by another activation frame.
For example, in the following code fragment, both of the assignments are
checked using the CHECK_STOREPTR run-time function. The first one is
checked because we are obviously writing to a global variable. The second one
is checked because we are writing through a pointer and thus we cannot know
for sure whether we are writing to the heap or to the stack.
int *g;
void foo(int * *x) {
g = *x; // Check this
*x = g; // Check this
}
Browse the CCured inferred pointer kinds,
or see the CCured output
for this code fragment
The CHECK_STOREPTR is passed both the address we are writing to and the
pointer that is being written. This function will in fact allow writing of
stack pointers into cooler stack locations (deeper into the stack). The
function will also allow the writing of null pointers anywhere. As a special
feature, CCured will allow the writing of stack pointers that are in the stack
frame of main or at higher addresses. This is useful because the
command-line arguments and the environment strings are allocated on the stack
of the program before main is called.
In rare occasions, we have encountered programs that do want to write the
address of locals variables into global variables. CCured provides an
easy-to-use mechanism for dealing with those situations. If you add the
attribute __HEAPIFY to the name of a local variable, the CCured will
move that variable to the heap using dynamic memory allocation. In fact, just
one allocation is made for all __HEAPIFY local variables in a stack
frame. Take a look at what happens in the following code fragment (do not be
fooled by the call to free; in CCured that is only a hint to the built-in
garbage collector):
int *g;
void foo() {
int local __HEAPIFY = 5;
g = &local;
}
Browse the CCured inferred pointer kinds,
or see the CCured output
for this code fragment
3.6 SEQuence Pointers
So far we have discussed pointers for which we disallow most casts and
pointer arithmetic. In this section we will discuss another family of CCured
pointers that can be used in pointer arithmetic operations. We call these
sequence pointers and they come in two flavors: those that can only be
advanced through pointer arithmetic (called forward-sequence pointers or
FSEQ) and the regular sequence pointer that can be moved both forward and
backward (we use the kind SEQfor these pointers). The cost that the
programmer pays for using these more capable pointers is that each dereference
will be accompanied by a bounds check.
Consider the following code fragment. The pointer x cannot be SAFE
because it is involved in pointer arithmetic. Since we are adding a
non-constant value CCured cannot be certain that the pointer is only advancing
so it will assign the more general SEQ kind to it.
int * arith(int * x, int delta) {
return x + delta;
}
Browse the CCured inferred pointer kinds,
or see the CCured output
for this code fragment
3.6.1 Representation
By looking at the CCured output for the above code you will notice several
changes in the code. First, the type of the x parameter and the name of
the function have changed as follows:
struct seq_int {
int * __SEQ _p ;
struct meta_seq_int {
void *_b ;
void *_e ;
} _ms ;
};
typedef struct seq_int seq_int;
int * arith_sq(seq_int p, int delta);
We see that CCured has created the type seq_int (sequence pointer to an
integer). This type has two components, the regular pointer value (field
_p) and a metadata component (the field _ms). Metadata is the
CCured terminology for additional information that CCured is carrying with the
pointers in order to be able to check their usage. All multi-word pointers in
CCured are represented as a structure with two elements: a field _p that
stores the value of the pointer and the field _ms that stores the
metadata for the pointer.
In the case of a SEQ pointer the metadata consists of two pointers, one
that stores the beginning of the memory area in which a pointer was created
(stored in field _b), and the end of that memory area (in field _e).
Such a memory area is also called a home area for a pointer. The
meta-data of the home area are generated by CCured for a pointer obtained by
allocation or by taking the address of a variable, and is passed along in an
assignment. Thus, a SEQ pointer carries with it the beginning and the end
of the home area from which it originates and these values will be used to
perform the necessary bounds checking.
The structures denoting fat pointers are named by adding a prefix
corresponding to the kind of fat pointer to a canonical name of the type. For
the general rules for naming types, see Section A.1.
Notice also that the name of the arith function has changed. CCured
mangles the names of globals whose type has changed. We do this to ensure that
you are not going to be linking your CCured code with a library that, for
example, calls the arith function with a regular pointer argument. The
mangling is always in the form of a suffix separated from the main name by an
underscore. The suffix is constructed as a sequence of letters, each one
signifying a certain kind of pointer (q stands for SEQ). The order of
the letters corresponds to the order in which the pointer type is encountered
in a depth-first in-order traversal of the structure of the global's type
(for functions we scan the result type first and then the arguments in order;
however, we do not scan structures and unions). For the general rules on
global name mangling, see Section 8.1.
Sequence pointers have an additional capability: they can be set to any
integer value, not just to 0 as in the case of SAFE pointers. We allow this
because the sequence pointers have the additional fields that can be encoded to
identify an integer disguised as a pointer. In particular both the _b and
the _e fields of a SEQ pointer are null in the case when the pointer
is actually an integer. The example below uses this capability of sequence
pointers. Notice that null pointers (those in which all three fields are 0)
are just a special case in which a SEQ pointer is actually an integer.
int * __SEQ getSeq() {
return 5;
}
Browse the CCured inferred pointer kinds,
or see the CCured output
for this code fragment
3.6.2 Invariants for SEQ pointers
-
Cannot be cast (except subject to stringent rules which we'll discuss
below). Note that assignment, passing actual arguments and returning are
implicit casts.
- Can be subject to pointer arithmetic (adding or subtracting an
integer from it).
- Can be set to any integer value.
- Can be cast to an integer and can be subtracted from another pointer.
This is useful for comparisons.
- SEQ pointers are represented using three words.
- Every time a SEQ pointer is dereferenced, both a check that the
pointer is not null or a disguised integer and a bounds check are inserted.
When sequence pointers are assigned, passed as arguments or as return values,
written or read from memory they carry their metadata unchanged. Same happens
when they are subject to casts or to pointer arithmetic. (Pointer arithmetic
affects only the _p component of the sequence pointer but not the home
area.) There are two operations in which SEQ pointers “are born”: by
using the name of a global or local array (possibly embedded inside other
structures or arrays) or by dynamic memory allocation. It is at that time that
the metadata for the SEQ pointers is computed and initialized, in the case
of an array based on the array length. and in the case of memory allocation
based on the allocated size. Take a look at the code CCured generates to
initialize the metadata for the r1 and r2 pointers in the code below,
both for the case of the memory allocation and for using the name of an array.
extern void* malloc(unsigned int);
int foo(int x) {
int *p, *r1, *r2;
int a[8];
r1 = (int*)malloc(16);
r2 = a;
p = r1;
p = r2;
return *(p + x); // Force p to be SEQ
}
Browse the CCured inferred pointer kinds,
or see the CCured output
for this code fragment
Whenever a pointer is subject to pointer arithmetic CCured will force that
pointer to be SEQ. This means that the pointer should come accompanied by
appropriate metadata. Thus the CCured inferencer will propagate the request
for the metadata backwards through the data flow, across function calls
and returns, to all the places where the pointer might be produced. For
example in the previous example p is subject to pointer arithmetic so it
must be SEQ. But since p is assigned from r1 and r2, they too
must be SEQ. Finally the request reaches the name of the array a (in
which case the metadata for a SEQ pointer is computed based on the length of
a) and also the malloc (in which case the metadata is computed based
on the allocated length).
3.6.3 Run-time checks for SEQ pointers
One of the design decisions for SEQ pointers was whether to check that the
pointer remains within bounds after each arithmetic operation, or to allow
pointer to go temporarily out of bounds and do the check when you use the
pointer. We chose to check the dereferences because the C standard actually
allows pointers to point outside their home area.
Sometimes a pointer is subject to arithmetic and then assigned to a pointer
that is used only for reading and writing. The latter pointer will be inferred
to be SAFE and the SEQ pointer will be converted to a SAFE pointer.
int foo(int x) {
int *p, *safe;
p += x; // p is SEQ
safe = p; // safe is SAFE
return *safe;
}
Browse the CCured inferred pointer kinds,
or see the CCured output
for this code fragment
To convert a SEQ pointer to SAFE we must check that it is in
within the bounds of the home area or is null. Note that even though a SEQ
pointer might contain arbitrary integers, a SAFE pointer can only contain
the integer 0. In the above code you can observe a run-time call to
CHECK_xxx that performs the bounds checking. The same check is used when
reading or writing through a SEQ pointer, as in the example below.
int addAll(int * p, int len, int stride) {
int sum = 0, i;
for(; len >= 0; len -= stride, p += stride) {
sum += *p;
}
return sum;
}
Browse the CCured inferred pointer kinds,
or see the CCured output
for this code fragment
Just like for SAFE pointers we must check the pointer validity when taking
the address of a field of an object pointed to by a SEQ pointer:
struct elem {
int f1, f2;
int nested[8];
};
int foo(struct elem *array, int len) {
int * pnested, * pnestedseq;
array += len; // Make array a SEQ
pnested = & array->f2; // A bounds check here
pnestedseq = & array->nested[2]; // A bounds check here
pnestedseq += len; // pnestedseq is a SEQ
}
Browse the CCured inferred pointer kinds,
or see the CCured output
for this code fragment
In the example above array is a SEQ pointer pointing to elements of
type struct elem. As long as we only do pointer arithmetic on array no
bounds checking is necessary. However, when we take the address of the field
f2 we will obtain a SAFE pointer and thus we must be sure that
arrayis within the bounds of its home area. Another interesting situation
occurs on the next line in the above example where we obtain a SEQ pointer
with a home included within the home of array. The home of pnestedseq
is the nested array within the struct elem element pointed to by
array. But again we must know that array is within bounds.
Just like for SAFE pointers we must check for stack addresses when a
SEQ pointer is written through a pointer or returned from a function. But
in this case the check is more subtle. To see why consider the following
program fragment:
// return a fat pointer to my own local, but using arithmetic
// to hide the fact that it's mine
int * sneaky()
{
int local[2];
int *x = local;
x += 200; // push x (apparently) above my frame
return x;
}
int main() {
int *plocal = sneaky();
return *(plocal - 200); // Back into its (vanished) home
}
Browse the CCured inferred pointer kinds,
or see the CCured output
for this code fragment
If we were to check that the _p field is not a local stack address we
would fail to notice the unsoundness in the above example. For this reason the
stack checks are performed using the _b pointer. Another to do so is that
if the _b pointer is null then we are returning an integer disguised as a
pointer and we should not care whether it is equal to a stack address (since
such a pointer cannot ever be dereferenced).
The bounds checks in CCured are more involved that in languages like Java
where all of the elements have the same size. It turns out that we can write
faster checks if we maintain the invariant that each FSEQ or SEQ pointer
points to an area that contains a whole number of elements of the given type.
Consider the following code fragment:
char buffer[17];
int main() {
long * __FSEQ p = buffer; // This will fail
return p[2];
}
Browse the CCured inferred pointer kinds,
or see the CCured output
for this code fragment
This will fail with an alignment check because there is no room for a whole
number of long elements in buffer.
Failure ALIGNSEQ at ./foo.c:3: main(): Creating an unaligned sequence
In general, this check can appear as part of a cast from a sequence pointer
to a sequence pointer of a wider base type. However, the above program is
perfectly fine. We can do several things:
3.6.4 Casts allowed for SEQ pointers
.
It is always possible to cast
a SEQ pointer to a SAFE pointer with the same underlying type. A
bounds-check is performed in that case. It is also possible to cast a SAFE
pointer to a SEQ pointer, in which case the home area of the new pointer is
the memory range occupied by one element of the SAFE pointer type.
Casting of SEQ pointers is only allowed when the underlying types are the
same or very closely related. We cannot freely allow the casting of SEQ
pointers using the physical subtyping rules that we used for SAFE pointers.
To see why consider the following program:
[--noSplitPointers]
struct wide {
int i;
int *p;
};
void foo(struct wide * __SEQ x) {
int * __SEQ pi = (int*)wide;
*(pi + 1) = 5;
}
Notice that the cast has the property that it casts a pointer to a large
structure to a pointer to smaller structure that is compatible with the large
one. If we were to allow the above program then we would be able to write an
arbitrary integer in a place where the pointer-type field p is stored. The
rule for SEQ pointers is that an infinite-tiling of the two types being
cast is compatible. This allows us to cast a pointer to an array into a
pointer to array elements (a very useful operation when working with
multi-dimensional arrays):
double a[8][8];
int zero() {
double * pa = a;
for(int i=0; i<sizeof(a)/sizeof(double); i++) {
* pa ++ = 0.0;
}
}
Browse the CCured inferred pointer kinds,
or see the CCured output
for this code fragment
3.7 FSEQ Pointers
We observed in our experiments that most SEQ pointers only move forward.
Thus the lower-bound check is not needed and also the _b field of the
SEQ pointer is also not needed. To capture this common case CCured is
using the FSEQ pointer kind (forward sequence). The FSEQ pointer is
very similar to the SEQ pointer with a few exceptions.
Consider the following example:
int addAll(int * p, int len) {
int sum = 0, i;
for(; len >= 0; len --, p ++) {
sum += *p;
}
return sum;
}
Browse the CCured inferred pointer kinds,
or see the CCured output
for this code fragment
A FSEQ pointer is represented as a two-word structure with just the
_p (actual pointer value) and _ms._e (end of the home area) fields:
struct meta_fseqp_int {
void *_e ;
};
struct fseqp_int {
int * __FSEQ _p ;
struct meta_fseqp_int _ms ;
};
typedef struct fseqp_int fseqp_int;
int addAll_f(int * __FSEQ p, void *p_ms_e , int len);
A FSEQ pointer can also encode an integer, in which case the _e field
is null.
A FSEQ pointer with a non-null _e field points always to an address
that is above or equal to the beginning of the home area. However, it might be
beyond the end of the home area, and that is why a FSEQ pointer requires an
upper-bound check whenever it is used (see the CCured output for the above
example).
When doing stack checks for the FSEQ pointer we use the value of the
_e field.
However, we must check for each arithmetic operation on FSEQ pointers
whether it is advancing the pointer or not. This is done using the
CHECK_ADVANCE run-time function. Notice that just because we add 1 to a
pointer it does not mean that we are advancing it. We might be trying to
overflow the addition and to break the invariant.
What remains to be said about FSEQ pointer is how does CCured infer that a
pointer is FSEQ as opposed to SEQ. CCured looks at all arithmetic
operations and if we always adding a positive constant to a pointer then
CCured will infer that pointer to be FSEQ. Another useful heuristic that
CCured uses is that pointer arithmetic expressed using the array indexing
notation is taken as an indication that we are advancing the pointer:
int addAll(int * p, int len) {
int sum = 0, i;
for(i=0; i<len; i++) {
sum += p[i];
}
return sum;
}
Browse the CCured inferred pointer kinds,
or see the CCured output
for this code fragment
Finally, FSEQ pointers can be cast to and from SAFE pointers using the
same rules that we discussed for SEQ pointers. FSEQ pointers can also be
cast to and from SEQ pointers. When casting a SEQ pointer into a FSEQ
pointer we must perform a lower-bound check. When casting a FSEQ pointer
into a SEQ pointer we consider that the home area starts at the place where
the pointer is pointing (provided that the pointer is not encoding an integer
and is within bounds). Note however that such a cast will never occur in a
program without pointer-kind annotations. The CCured inferencer will instead
prefer to propagate the constraint that all pointers which are assigned to
SEQ pointer must themselves be SEQ pointers and thus have a valid
_b field.
3.7.1 Arrays of unspecified length
We saw that a SEQ pointer obtains its metadata from the length present in
the array type from which they originate. But occasionally it is useful to
have arrays with either unspecified length or with a zero-length. Consider the
following code, in which the struct open is open-ended, that is the number
of integer pointers contained in the rest array field is determined at the
allocation time (in this case 4):
struct open {
int count;
int * rest[0];
};
extern void* malloc(unsigned int);
int main() {
struct open *p = (struct open*)malloc(20);
return p->rest[5];
}
Browse the CCured inferred pointer kinds,
or see the CCured output
for this code fragment
CCured supports this paradigm and computes the size of the rest field at
the time of the allocation. Then CCured will turn the array rest into a
sized array, which is essentially a structure with two fields: a field
_size which stores the size of the array and a second field _array
which contains the array itself:
struct _sized_a_char {
unsigned int _size ;
char ( __SIZED _array)[20] ;
};
Sized arrays are very similar to the Java arrays in that they store their
length in the first word of the data structure. When a SEQ pointer is
created from such an array the metadata is computed based on the stored size.
There is one more situation in which CCured will automatically infer that an
array must be sized. That is when the array is declared external and without a
length:
extern a[];
int main() {
return a[3];
}
Browse the CCured inferred pointer kinds,
or see the CCured output
for this code fragment
Additionally, the programmer can request that an array be represented in sized
form by using the __SIZED attribute on the array name:
int *a [8] __SIZED;
Browse the CCured inferred pointer kinds,
or see the CCured output
for this code fragment
Note that CCured does not support the allocation of sequences of arrays of
structures with open arrays. For example, the following code will produce a
warning and will allocate a sequence of struct open elements each with a
zero-length rest field!
struct open {
int count;
int * rest[0];
};
extern void* malloc(unsigned int);
int main() {
struct open *p = (struct open*)malloc(20);
p ++; // Make p FSEQ
return p->rest[5];
}
Browse the CCured inferred pointer kinds,
or see the CCured output
for this code fragment
You might have noticed in the previous example that when reading from a
SEQ pointer, CCured will allow the reading of the byte immediately
following the array. This “feature” is part of our current mechanism for
handling null-terminated strings, in which case the terminal null character
can be read but not written, as discussed in the next example.
3.8 WILD Pointers
The pointer kinds we have seen so far can be dereferenced and can be subject
to pointer arithmetic but can only be cast in very restrictive ways. Therefore
we cannot really hope to be able to annotate all existing C programs with
kinds like SAFE, SEQ and FSEQ. We also need a pointer
kind that can also be cast to any other type. The WILD pointer kind plays
this role. Looking back at the kinds of pointers we have introduced so far we
observe that the most restrictive kind of pointer, the SAFE pointer, is
also the cheapest to use. It requires only one word for storage and only a
null check for dereference; just like Java references. Then as we add more
capabilities we also increase the cost of the pointer. The FSEQ pointers
have all the capabilities of SAFE pointers but can also move forward. The
additional cost is an extra word required for the storage of the end of the
valid range and an upped-bound check required before dereference. The SEQ
pointers have the additional capability of moving backwards and the additional
cost of one more storage word and a lower-bound check before dereference.
Keeping with this trend it is to be expected that WILD pointers are going
to be even more costly. As we shall see, the WILD pointers must be able not
only to find the bounds of the range in which they are supposed to navigate but
they must also know for each word in that range whether it is a pointer or a
non-pointer. The previously-introduced kinds of pointers did not need to
maintain that information at run-time because the lack of casts allowed the
compiler to keep track of such information statically.
One way to think of the CCured pointer-kind inferencer is as an analysis that
classifies your pointers into two big categories: those for which the static
type is an accurate description of the values pointed to; and those for which
it is not. We refer to the first category as the statically-typed
pointers and they consist of the pointers discussed so far: SAFE, SEQ,
and FSEQ. The second category consist of the dynamically-typed pointers and include the WILD pointers. Since the
compiler cannot verify statically the type of the values the WILD pointers
point to, then CCured inserts code to maintain at run-time information about
the contents of a memory range pointed to by WILDpointers.
Consider the following example, in which a (of type int
*) is cast to type int * *:
int foo(int * a) {
int * * g = (int * *)a; // Bad cast
return 0;
}
Browse the CCured inferred pointer kinds,
or see the CCured output
for this code fragment
There are several new things in the CCured version of the above
program fragment. We start with the type of a:
struct meta_wildp_int {
void *_b ;
} ;
struct wildp_int {
int * __WILD _p ;
struct meta_wildp_int _ms ;
} ;
typedef struct wildp_int wildp_int;
int foo_w(wildp_int __WILD a);
A WILD pointer is represented as a two-word structure. As usual the
_p field stores the actual pointer and just like for SEQ pointers the
_b field stores the beginning of the pointer's home area. The major
difference in the representation of WILD pointers is the layout of the home
area. Since we must keep track at run-time what is stored in each location in
a dynamically-typed area we will store a bitmap (one bit per word) at the end
of the home area. And just like for sized arrays the word immediately before
the home area stores the size in words of the home area. Such an example is
shown in the code below where the address of the local variable h is the
home for the pointer p.
void foo() {
int * h = 0;
int * p = (int *) &h;
return 0;
}
Browse the CCured inferred pointer kinds,
or see the CCured output
for this code fragment
The type of h is:
struct _tagged_wildp_int {
unsigned int _len ;
wildp_int _data __attribute__((__packed__)) ;
int _tags[(sizeof(wildp_int ) + 127U) >> 7] __attribute__((__packed__)) ;
};
typedef struct _tagged_wildp_int _tagged_wildp_int;
The _data field in a tagged area stores the actual data, which in this
case is a WILD pointer. The _tags field contains one word for every 32
words of data. Each bit in the tags is 1 if the corresponding word in the data
field stores the _b field of a WILD pointer, and 0 otherwise (if it
contains an integer or the _p field of a WILD pointer or equivalently
a value that is not CCured metadata). To maintain this invariant we
must update the tag bits every time we perform a memory write. When we write an
integer into a word we clear the bit corresponding to that word. When we write
a WILD pointer then we set the two bits corresponding to the two words to 0
and 1 respectively. When we read an integer we do not need to check tags. When
we read a WILD pointer then we check that the tag bit for the word from
which we'll read the _b component has a set tag bit. If this is not true
then we check whether the _b component that we'll read is 0. In this
latter case we would be reading a pointer that cannot be used for memory
dereference anyway. This latter situation occurs when we read a pointer from
an area that has been initialized with zeros.
Notice that this scheme ensures that we will never interpret a word in a
tagged area as a _b field except if it was last written with a contents
of a _b field. This however does not prevent code that overwrites the
_p fields from running (except that the resulting pointers might not be
later usable).
The following run-time support functions are used in conjunction with WILD
pointers:
/* Fetch the size (in words) of the tagged area pointed to by a WILD pointer.
This also checks that the pointer has a valid _b field */
unsigned int
CHECK_FETCHLENGTH(void *_p, /* The _p field of the pointer */
void *_b); /* The _b field */
/* Do bounds checking for WILD pointers */
CHECK_BOUNDS_LEN(void *_b,
unsigned int bwords,/* Result of FETCHLENGTH */
void *_p,
unsigned int plen); /* The size in bytes of the memory area
being accessed */
/* Clear the tags for a memory range. This is called before writing a scalar
or a structure containing at least one scalar into a tagged area. */
CHECK_ZEROTAGS(void *base, /* The base of the tagged area */
unsigned int nrwords, /* Number of data words in the area */
void *start, /* Start of the memory range for which
to clear the tags */
unsigned int size); /* Size in bytes of the memory range for
which to clear the tags */
/* Set the tags for writing a pointer. This also checks that we are not
writing a stack pointer. This is called for EACH pointer in a structure
that is being written. */
CHECK_WILDPOINTERWRITE(void *base, /* The base of the tagged area in which
we write */
unsigned int nrwords, /* Number of data words in the
area */
void **where, /* The address in the tagged area where
we are about to write */
void *_b, /* The _b field of the written pointer */
void *_p); /* The _p field of the written pointer */
/* Check that the pointer we are about to read has a _b field that has not
been tampered with */
CHECK_WILDPOINTERREAD(void *base, /* The base of the tagged area in which
we write */
unsigned int nrwords, /* Number of data words in the
area */
void **where, /* The address in the tagged area where
we are about to write */
void *_b, /* The _b field of the written pointer */
void *_p); /* The _p field of the written pointer */
The code fragment below uses these runtime functions:
struct s {
int i; // Some integer
int *q; // And some pointer
} g, * __WILD pg = &g;
int foo(struct s * __WILD x) {
// Read an integer from x.
// Must do bounds check
int read = x->i;
// Read a pointer from x
// Must do bounds check and check that the _b field is valid
int * ptr = x->q;
// Write an integer
x->i = 5;
// Write a pointer
x->q = (int*)6;
// Read and write the whole struct
g = *x;
}
Browse the CCured inferred pointer kinds,
or see the CCured output
for this code fragment
A WILD pointer can be used in a very flexible way but there are some
constraints. Like any of the other pointers that can be subject to pointer
arithmetic the WILD pointer carries with it the identity of the home area
and can be used to access only that area. But most importantly a WILD
pointer can only be case to and from another WILD pointer and can only
point to scalars or other WILD pointers. Essentially this means that the
dynamically-typed universe can touch the statically-typed universe in only a
single way: a WILD pointer can be stored in a statically-typed area.
The following pointer kind is not legal “int * SAFE * WILD”. To
see why consider the (ill-typed) code below:
int foo(int * __SAFE * __WILD x) {
int * __SAFE y;
*(int __WILD *)x = 5; // Ok since x can be cast to another __WILD pointer
y = * x; // Ok
return *y; // Ok since y is SAFE and non-null
}
Essentially we cannot count on the accuracy of the types pointed to by
WILD pointers. For this reason we can only allow WILD pointers to point
to scalars or other WILD pointers. So, in the above example CCured does not
recognize x as a valid type.
For the same reason we cannot cast between WILD pointers and non-WILD
pointers.
3.9 Split Metadata
In the previous examples pointers with metadata are represented as
structures. It turns out that gcc or the Microsoft Visual C compiler
are not very effective at optimizing code that uses many variables with
structured types. Thus, CCured has the ability to split such variables into
several single-word variables. Consider again one of the examples from before:
int * arith(int * x, int delta) {
return x + delta;
}
Browse the CCured inferred pointer kinds,
or see the CCured output
for this code fragment
Notice that x becomes split into three variables: x (for the _p
field, or the regular pointer value), and x_b and x_e for the
beginning and end metadata fields. Notice also that function parameters and
arguments (but not the results are split in the same way):
int * arith_sq(int * x, void * x_b, void * x_e, int delta);
By default, CCured splits the metadata. You must pass the argument
–noSplitPointers to prevent it.
CCured consists of several components: an Ocaml application that does the
main work, a set of Perl scripts that are used to invoke the CCured
application, and a set of header and run-time library files.
The easiest way to use CCured is through the bin/ccured script. This
script is intended to be used in the same context and with the same
command-options as either the gcc compiler or the Microsoft Visual C
compiler (MSVC). This script is configured at installation time to know where
the rest of the CCured installation resides. If you move this script to
another directory you must also make a copy in the new directory of the
CilConfig.pm file.
Since ccured is a drop-in replacement for gcc, for most software
projects you can reuse the regular build-infrastructure:
make mystuff CC="bin/ccured [options]"
Here is the sequence of actions that the ccured script performs:
-
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 .i in the same directory as the source file.
- For every .i file that it produces and that must be compiled (i.e.
the -E option was not specified to require only preprocessing) ccured
will save a copy of the file with the extension .o, thus “fooling”
make that the object file was actually produced.
- Whenever ccured is invoked to link into a library a number of
.o files that are actually preprocessed sources saved in the previous
step, the CCured engine will be invoked to parse all of the files and produce
a single 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 –mode=AR argument to CCured if you want to pass the
remaining arguments as for the ar utility. More details about the merging
stage that CCured used can be found .
- Finally, when ccured is called to link 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 CCured 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 ccured.c. Finally this file is
preprocessed, compiled and linked using the underlying compiler.
Notice that by default the curing process is invoked on the whole program.
This is necessary to allow the CCured inferencer to see all the uses of your
pointers. An alternative is to annotate the include files with pointer-kind
annotation and let the inferencer do the inference within one file only.
4.1 Command-line options
You always run CCured with the command options of gcc (e.g., -c to
compile only, -o to specify the output file, etc.). Here are some common
ways to use invoke CCured:
-
bin/ccured –nocure –nomerge hello1.c hello2.c -o hello.exe
- Compiles and links without curing and without merging (still
uses the CIL front-end)
- bin/ccured –nocure hello1.c hello2.c -o hello.exe
-Merges using CIL, then compiles and links with gcc
- bin/ccured hello1.c hello2.c -o hello.exe -Merges using
CIL, processes with CCured, the compiles and links with gcc
- bin/ccured -c hello1.c hello2.c -Just put preprocessed source in the object files
- bin/ccured hello1.o hello2.o -o hello.exe -Take the
preprocessed source in the object file, merge, cure, gcc.
- bin/ccured –mode=AR cr hello.a hello1.o hello2.o -Merge
the preprocessed source in the object files into an archive (which itself
contains source)
- bin/ccured hello.a main.c -o hello.exe -Preprocess the C
source, merge with the sources in the archive, cure and gcc.
Most of the command-line options that you pass to ccured will be passed
along to the underlying preprocessor, compiler or linker. However the
ccured script recognizes the following special options:
-
General options
-
–save-temps. It tells the CCured script to save the temporary files
(including the output of CCured).
- –nocure. It does not actually cure the code. However, it reads it
in using the CIL front-end and then it prints it out immediately. Use this in
the first phase to check that the CIL front-end works for you.
- –mode=AR. Invoke CCured to act as the archiver. In this case there
should be no more arguments, except those that the ar utility would take.
This is because the ar arguments are positional.
- –mode=MSVC. Use instead of the Microsoft Visual C compiler
(cl). CCured and the CIL front-end know how to handle the MSVC extensions.
- –leavealone=foo. CCured 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 CCured to see (e.g., if they are really ugly and you are ashamed of
what you did!). See Section 7.4 for details.
- –stats. Print some statistics about the inserted checks.
- –stages. Print details about the various stages.
- –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).
- –nomerge. Invoke the curing process during the compilation stage,
without waiting to have the whole program.
- –keepunused. Disable the removal of apparently unused elements from
the file, such as local variables or prototypes.
- Inference
-
–noemitbrowser. Do not produce the browser information (speed up
curing).
- –browserdir=<dir>. Use <dir> as the name of the directory where
to store the browser information. By default it is placed in a directory whose
name is formed from the name of the executable followed by .browser.
- –browserSourceFileSize=N. Specify the number of statements to put
in a source file fragment. Default is 2000. Larger value means fewer source
fragments but also slower browser operation.
- –browserNodeFileSize=N. Specify the number of inference nodes to
put in a file. Default is 2000. Larger value means fewer
source fragments but also slower browser operation.
- –emitinfer. This means that the result of inference is also printed
in a file fooinfer.c where foo is the desired executable. See
Chapter A. It is recommended that you use the browser instead.
- –emitGraphDetailLevel. Controls how much information to put in the
infer file. Values range from 0 to 3.
- Curing
-
–allowInlineAssembly. Allow (unsound, best-effort) handling of
inline assembly.
- –nogc. Will assume that you do not use a garbage collector. In this
case the cured code will use explicit deallocation and might be unsafe.
- –optimize. Run the optimizer after curing.
- –releaselib. Use the release library (compiled with optimizations
on)
- –noUnrefPointerChecks. Treat as scalars those pointer variables
whose values are never used as pointers.
- –allowPartialElementsInSequence. Do not check that a sequence
contains a whole number of elements. If you turn this on, more programs will
cure, but the bounds checks for sequence pointers will be more expensive (see
Section 3.6.3).
- –noSplitPointers. Do not split CCured multi-word pointers into
single-word variables (Section 3.9).
- –alwaysStopOnError. Generate code that always stops on error
(slightly faster).
- –failIsTerse. Do not print source-file location on failure. This
makes your program smaller and faster.
- –noPrintLn. Turns off the printing of line-number information. This
way the errors will be referenced to the Cured file not the source file.
- –commPrintLn. Print line-number information as comments. This
way the errors that CCured 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.
- –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.
For most performance you should use the options:
--optimize --releaselib --alwaysStopOnError --failIsTerse
All of the other options that start with – (and are not recognized as
compiler options) are passed unmodified to the CCured Ocaml application.
4.2 Controlling error handling at run time
After you cure a program you can run it as usual. The operations of the
CCured-inserted run-time checks can be controlled with a few environment
variables when the target program is run:
-
CCURED_CONTINUE_ON_ERROR: if set and if –alwaysStopOnError
was not used during curing, the execution will continue on error. This means
that your program might be unsafe. It might also be possible that a cascade of
check failures will be triggered.
- CCURED_SLEEP_ON_ERROR: if set the program goes to sleep on an
error. When it does so, it prints the process id. You can then connect to it
using gdb as follows (replace test with the name of your executable
and 10343 with the actual process id printed when the process goes to
sleep.):
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 -g and
you did not use –releaselib. I also prefer to use -commPrintLn so
that the debugging information refers to the cured file, not the original.
- CCURED_ERROR_HANDLERS: if set, then its value is taken to be the
name of a text file that contains indications on how to handle various error
conditions. First, the error messages that CCured prints are like this:
Failure UBOUND at hello.c:10: main(): Ubound
Each message has an error name (UBOUND), a file location (hello.c), a
line number (10), a function in which the error occurred (main), and
some explanation. You can specify error handlers based on the error name and
error location.
Each line in the error handler file must look like this:
[stop|warn|sleep|ignore|//] [*|ERRNAME] at [*|FILE] : [*|LINE] : [*:FUNC]
Note that you can almost copy and paste CCured error messages into this file.
stop means that the execution stops, warn that a warning is printed
and the execution continues, ignore that not even a warning is printed.
// means that the rest of the line is to be ignored.
* is a wildcard that matches anything. Except for the first two elements,
any suffix of the line can be missing. Whatever comes after the function name
is ignored. Empty lines are ignored and lines are matched in order. The file
is parsed when the program starts and then it is indexed by the error number
and looked up when an error occurs. Note that you cannot override
–alwaysStopOnError this way!
For example, the following file:
ignore UBOUND
stop * at hello.c: 10
ignore LBOUND at *:*:tricky
means that all UBOUND errors are ignored, the execution stops for any error
in line 10 of hello.c (except UBOUND), and LBOUND in function tricky is
ignored (except if it happens in line 10 of hello.c). Errors that do not
match are treated in the default way (stop if –alwaysStopOnError or
CCURED_CONTINUE_ON_ERROR are not specified).
- CCURED_DUMP_HANDLERS: if set, then CCured dumps its error handler
table (so that you can check that it has the values you want).
- CCURED_ERROR_LOG: If set, CCured will print all error
messages (except those which are are listed as ignore in the error
handling file) to the specified log file in addition to
stderr. This variable should be set to the absolute path of the
log file.
- CCURED_NO_SIGABRT: When CCured handles an error by
stopping the program's execution, it will normally call abort().
If this variable is set, CCured will use exit(-1) instead of
abort(), which means that SIGABRT is not thrown.
Chapter 5 CCured Type Inference
If you do not pass pass the –nocure argument to ccured, CCured
will automatically infer pointer kinds (see Section 3.1) for the
pointer types in your program. In a nutshell, this is done by creating a graph
with one node for every pointer type in the program. If the program contains a
cast or assignment from one type to another, the graph contains an edge
between the corresponding nodes.
Once the graph has been created, the inferencer will examine every node and
edge in the graph. If the edge represents a cast that is not captured by
our notion of physical subtyping (i.e., a cast that we cannot statically
verify to be valid) we mark the involved nodes (and thus the pointers in
the program they are associated with) as WILD. Since WILDpointers may
only point to other WILDareas, any node connected to a WILDnode must
also be WILD.
The inferencer then checks the remaining nodes to see if the types they
represent are involved in pointer arithmetic. A node that is only
incremented can be made FSEQwhile a node that is subject to general
arithmetic must be SEQ. All remaining nodes (i.e., those that adhere to
our notion of physical subtyping and have no other constraints) become SAFE.
The actual inferencer includes support for a number of specialty pointer
types, like the run-time type information pointer (RTTI), but the basic idea
remains as described above. The end result of the inferencer is the graph,
which serves as a mapping from types in the program to pointer kinds. The
module that inserts run-time checks into the program uses this information to
determine which checks to put where.
In the process of adding run-time checks to make the program type- and
memory-safe, CCured introduces new types, changes old types and changes
function prototypes. In each of these cases a new name is introduced to
eliminate confusion and to prevent the resulting program from linking
improperly.
5.1 Using the pointer browser
To inspect the results of the inference you should use the pointer browser.
Every time you run CCured it will produce a directory called foo.browser
(where foo is the name of the executable you are creating).
Alternatively, you can use the –browserdir option to CCured to specify in
which directory it should place the browser.
That
directory contains HTML files and Javascript programs that you can use to find
the reasoning that CCured has used during pointer kind inference. To start the
browser, point your web browser (Mozilla or IE; Netscape was broken beyond
belief when we checked last in September 2002) to the file
foo.browser/index.html and get going.
The browser will show you the preprocessed and merged file with annotations
about the pointer kinds. The file that you will see also has the result
of processing the polymorphism directives (see Section 7.1) and the wrappers
(see Chapter 8).
The documentation for the pointer browser is at browser_help.html.
There is an alternative lower-level way to inspect the result of the
inference, which is described in Appendix A.
In this chapter we describe the typical steps that must be taken to use
CCured 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 Chapter 10. Take a look there if the explanation here is too
terse.
-
Regular build First try to download the sources and build them in
the regular manner (using 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.
- Build using CIL Next you should try to build the package using CIL
(the front-end that CCured 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 and the linker):
ifdef CCURED
CC:=/home/necula/ccured/bin/ccured
endif
ifdef NOCURE
CC+= --nocure
endif
ifdef NOMERGE
CC+= --nomerge
endif
If your project includes a more complicated setup, you must make the
necessary changes to use the above commands instead of gcc (both for
compiling and for linking).
Then you can run:
make clean
make CCURED=1 NOCURE=1 NOMERGE=1
This should build your project as before, except that each source file is
first preprocessed, then passed through the ccured.asm.exe executable to
produce the CIL output (a file with suffix 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 gcc. Here is an example of what you
should see for the file util.c from the mathopd package:
/home/necula/ccured/bin/ccured --nocure --nomerge -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/ccured/obj/x86_LINUX/ccured.asm.exe --cilout ./utilcil.c --nocure --warnall ./util.i
gcc -D_GNUCC -E -O -DHAVE_CRYPT_H -I/home/necula/ccured/include ./utilcil.c -o ./utilcil.i
gcc -D_GNUCC -c -O -DHAVE_CRYPT_H -Wall -o util.o ./utilcil.i
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
ccured Perl script that tries to impersonate gcc. CIL has been tested
extensively, so you can consider yourself truly unfortunate. Please let us know
about your problem.
Next, we try the same thing, but this time with merging. In this mode of
operation, the CIL front-end will attempt to create a single C source file
from all of the files in your project. In this case, when make invokes
ccured to compile a source file, the resulting object file will contain
just the preprocessed version of the source. And when ccured is invoked to
link the executable then all of the preprocessed sources are merged into a
single file (with the suffix combcil.c), which is processed as before. Here is
an example of what you should see for the mathopd package:
make clean
make CCURED=1 NOCURE=1
...
gcc -D_GNUCC -E -O -DHAVE_CRYPT_H util.c -o ./util.i
/home/necula/ccured/bin/ccured --nocure -o mathopd base64.o cgi.o config.o core.o dump.o imap.o log.o main.o redirect.o request.o util.o -lcrypt
/home/necula/ccured/obj/x86_LINUX/ccured.asm.exe --cilout ./mathopd_combcil.c --nocure base64.o cgi.o config.o core.o dump.o imap.o log.o main.o redirect.o request.o util.o
gcc -D_GNUCC -E -I/home/necula/ccured/include ./mathopd_combcil.c -o ./mathopd_combcil.i
gcc -D_GNUCC -c -o mathopd_comb.o ./mathopd_combcil.i
gcc -D_GNUCC -o mathopd mathopd_comb.o -lcrypt
You should again try to run your executable. If it does not work as expected
then you have found a bug in the merger. This is again unlikely, but if it
happens, let us know.
If your project is built by first creating some libraries then merging works
in a slightly different way. Take a look at the UCSPI TCP example
(Section 6.2) next to see how that goes.
- Build with CCured
Now we start using CCured:
make clean
make CCURED=1
The sequence of operations is the same as in the case of CIL with merging,
except that this time, after the sources are merged into foo_comb.c, the
ccured.asm.exe engine is invoked.
CCured 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 CCured 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 Chapter 10.
- Write the wrappers
If curing succeeds the resulting file (with suffix cured.c) is passed to
gcc for compilation and linking. Often you will see linking errors that
mean that CCured has changed the interface of a function in a way that is
incompatible with the library version of the function. See the examples below
and Chapter 8 for a tutorial on writing wrappers.
- Run and debug the cured code
Now that you have build your executable with CCured you should run it on as
many examples as possible. Remember that CCured 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 CCured static analyzer, so CCured just
silently inserts a 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 CCured you should investigate it to see if
it is a false alarm or a true bug.
You can tell CCured to continue the execution after it encounters an error if
you set the environment variable CCURED_CONTINUE_ON_ERROR.
Next we look at concrete examples. If you want to try your hand at using
CCured on real code you might want to try it on these packages and then use
the instructions when you get stuck.
6.1 Example: mathopd HTTP server
6.1.1 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 mathopd-1.4-gamma.tar.gz, unpack, change the Makefile as
required for Linux and then we try it out:
cd src
make
Next we edit the configuration file (doc/sample.cfg) so that we can run
the server on port 8000. Right after the line Server { we add Port
8000. Then we must become root and create a directory for the log:
su root
mkdir /var/mathopd
chmod 777 /var/mathopd
exit
./mathopd <../doc/sample.cfg
Now from another machine (make sure you have /public_html/index.html on the
server machine):
explorer http://manju.cs.berkeley.edu:8000/~necula/
and we see that it works.
6.1.2 Step 2: Build with CIL
Completely uneventful.
6.1.3 Step 3: Build with CCured
For mathopd we saw the warning:
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!
As explained in Chapter 10, we take a look at the implementation of
log_d (we find it in the merged file mathopd_comb.c) to make sure
CCured did not miss anything. Sure enough, log_d is a printf warning.
Same thing for die. We fix this by adding the following pragma in
main.c (see Section 9.6.1 for details):
#pragma ccuredvararg("log_d", printf(1))
#pragma ccuredvararg("die", printf(2))
In the process of doing mathopd, we encountered the warning:
/home/necula/ccured/include/netdb_wrappers.h:329: Warning: Solver: changing User Specified SAFE node 1371 (the local variable p_ith_alias) to WILD
This turned out to be a bug in the wrapper for the socket functions. We found
it using the browser (see Section 5.1).
Then we saw a warning:
/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".
This turned out to be due to the same socket wrapper error.
Another warning you might see when you run CCured is:
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
This means that a 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 __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:
ptrkinds: Graph contains 12886 nodes
ptrkinds: SAFE - 9256 ( 72\%)
ptrkinds: SEQ - 429 ( 3\%)
ptrkinds: FSEQ - 3201 ( 25\%)
6.1.4 Step 4: Write the wrappers
We see now that there are some missing functions:
mathopd_comb.o: In function `log_request':
mathopd_comb.o(.text+0x1b02d): undefined reference to `asctime_qs'
See Chapter 8 for information on how to write this wrapper: Essentially
this is what we had to add to time_wrappers.h file:
#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);
}
6.1.5 Step 5: Run and Debug the cured code
We ran the mathopd server and we get an error right away:
Failure at config.c:924: new_pool(): Ubound
Aborted
We look at the code and we see this code in config.c:
p->ceiling = t + s;
This looks like the pointer that is stored in the ceiling field is
outside bounds, that that is Ok. This field is never used as a pointer. So, we
change its type to long instead. We could change it to FSEQ as well.
See Chapter 10 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.
6.2 Example: UCSPI TCP Suite
6.2.1 Step 1: Regular Build
This is a package that provides “tcpserver” and “tcpclient”. From their
web page (): “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:
gunzip ucspi-tcp-0.88.tar
tar -xf ucspi-tcp-0.88.tar
cd ucspi-tcp-0.88
make
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:
make setup check
And now the big moment:
./http@ www.yahoo.com
Bingo!
6.2.2 Step 2: Build with CIL
This software package has a strange build interface. The Makefile contains
things like:
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
What is happening is that the compile script is created from the first line
of conf-cc and then used as a compiler. That line contains gcc -O2
right now. We change that file to use instead the value of the CC environment variable:
$CC -O2
(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:
export CC:=gcc
ifdef CCURED
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
Just to test the new setup we make it again and test it again.
Now we try to make it with CIL.
make clean
make CCURED=1 NOCURE=1 NOMERGE=1
Now we get an error:
tcpserver.o: In function `main':
tcpserver.o(.text+0xa29): undefined reference to `env_get'
tcpserver.o(.text+0xa50): undefined reference to `env_get'
Clearly we have done something wrong. A quick investigation reveals that
tcpserver.c does need env_get, which is defined in env.c, but seems to
be missing from 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 –keepunused flag to CCured.
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 makelib to make a library
and load to make an executable.
For the load script all we need to change is the conf-ld to use
$CC instead of gcc. We do this and we run with merging. We get this
error:
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
As explained in Chapter 10, this is because we should not use ar to
archive files in the merging mode, but we should use ccured –mode=AR. We
achieve this by changing the Makefile, which creates the makelib script.
We change it such that the makelib script uses the environment variable
AR instead of ar. And we defined AR in the Makefile as follows:
export AR:=ar
ifdef CCURED
ifndef NOMERGE
AR:=/home/necula/ccured/bin/ccured --mode=AR
endif
endif
We run again in merging mode and now we get:
ranlib: cdb.a: File format not recognized
You look at cdb.a and find that it is a merged source file. You should
not use ranlib on such files. We edit the Makefile again and rerun.
Now we get this error message when trying to merge rblsmtpd from a number
of object files and libraries:
/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 )
What happens is that the file rblsmtpd.c defines its own global accept
(luckily, with a different type than the one in the library; otherwise CCured
would not have noticed!). Yet, one of the
other files that are merged (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 socket_accept will be
resolved to the “accept” from rblsmtpd (which is clearly not an
acceptable replacement for the socket function).
We change the name of the “accept” in 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. tcpclient_comb.c. And, we have found a bug even before we started
to use the actual CCured!
6.2.3 Step 3: Build with CCured
The first thing we see when we enable CCured on this package is:
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 ()
Two warnings, both due to missing or incomplete prototypes. In the cast of
getgroups it is a missing prototype. We add to chkshgr.c the following:
#include <unistd.h> // For getgroups
#include <grp.h> // For setgroups
We also exit the prototype of _exit in exit.h:
extern void _exit(int); // The "int" was missing
Now CCured succeeds in making this executable and proceeds to make
tcpserver. Here we find this one:
tcpserver.c:352: Error: You did not turn on the handling of inline assembly. Better hide this assembly somewhere else!
This is interesting! We look at the inline assembly (a good place to look in
is tcpserver_comb.c, you'll see them all in there). One is a use of
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 FD_SET and
friends from <sys/select.h>. We investigate and we find that these macros
are defined in <bits/select.h>, and luckily that file also provides
regular C implementation for them, along the following lines:
#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 */
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.
-
First, we tell CCured that <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 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
cil/Makefile.gcc and add to the list of PATCH_SYSINCLUDES the name
bits/select.h (but we do it only in the Linux section).
- Then, we specify the patch. We add the following to the file cil/ccured_GNUCC.patch:
<<< file=bits/select.h, system=linux
#if defined __GNUC__ && __GNUC__ >= 2
===
#if 0 && defined __GNUC__ && __GNUC__ >= 2
>>>
This says that the specified patch should be applied to the file
bits/select.h when CCured is run on a Linux system. (Not all
platforms have bits/select.h.)
Matching is done whitespace-insensitive. Now you rebuild CCured (just run
make) and you should find the patched file in the
cil/include/gcc_2.95.3/bits. Make sure it is as you need. More information
about the patcher is at ../cil/patcher.html
And since we have left one inline assembly in, we must tell CCured to accept
it as is. We change the Makefile to pass the –allowInlineAssembly to
CCured.
Now we find more missing prototype problems:
tcpserver.c:210: Warning: Calling function close with 1 arguments when expecting 0: will be WILD.
close has type int ()
In fact, close does not have a prototype at all. CCured has supplied one
without arguments while making unix.a! We add the “#include <unistd.h>”
to tcpserver.c and go on.
We add a few more prototypes and then we get:
buffer_get.c:10: Warning: Calling function (*op) with 3 arguments when expecting 0: will be WILD.
(*op) has type int ()
We find in buffer.h and 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
Chapter 7 for general techniques). We see this message:
** 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
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:
e = (char **) alloc((elen + 1) * sizeof(char *));
This is a custom allocator. We must declare it (in alloc.h):
extern void *alloc(unsigned int);
#pragma ccuredalloc("alloc", nozero, sizein(1)) // We added this line
We run CCured again and no more bad casts (it looks like all the others were
due to alloc), but still a bunch of WILD:
pointers:
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
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 void
* pointer that is used with several incompatible types (in this case char
* and char **). See Section 7.1 for more details on this. This turns
out to be because the function alloc_free with a declared argument of
type void * is used in two places with different argument types. We simply
declare that function to be polymorphic (in alloc.h):
#pragma ccuredpoly("alloc_free")
Finally, CCured succeeds, with no WILD pointers, but there still is a
warning that we have not looked at:
pathexec_env.c:42: Warning: Encountered sizeof(char */* __attribute__((___ptrnode__(2595))) */) when type contains pointers. Use sizeof expression. Type has a disconnected node.
As explained in Section 9.5 we should take a look at the code. We find
this typical example, and we fix it accordingly:
e = (char **) alloc((elen + 1) * sizeof(* e)); // Was sizeof(char *)
6.2.4 Step 4: Write the wrappers
In this package there in an interesting case:
tcpserver_comb.o: In function `env_get_qf':
tcpserver_comb.o(.text+0x15d10): undefined reference to `environ_qq'
This time the global that needs a wrapper is a pointer to data, not a
function. You cannot write a wrapper for this, but you can replace its
accesses with functions.
Since the program accesses environ always with an index operation
environ[i], we can write a function environ_idx that takes an integer
and returns the ith element in environ. I show below the case where
it appropriate to trust that the index is within the bounds:
extern char ** environ;
char* environ_idx(int i) {
char * __SAFE * __SAFE p_environ = __trusted_add(environ, i);
// We are going to believe that i is within bounds
return __mkptr_string(* p_environ);
}
6.2.5 Step 5: 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 CCURED_CONTINUE_ON_ERROR
(Section 4.2) to see them all.
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
There are two distinct errors. We'll fix them, but here is a way to silence
CCured if you are lazy: we can use
CCURED_ERROR_HANDLERS to specify that we want to ignore all
STORE_SP errors in those two functions. For this we write a text file
(ucspi.handlers):
ignore STORE_SP at *:*:pathexec_qq
ignore STORE_SP at *:*:__deepcopy_stringarray_to_compat___0_ssqq
Now we run as follows:
CCURED_ERROR_HANDLERS=ucspi.handlers ./http@
and 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 environ variable. It turns out that
those strings are on the stack (allocated before main is invoked). The
solution would be to copy those strings on the heap. But right after I saw
this error I realized that CCured should not complain if the address that is
being stored is in the stack frame of main or at higher addresses. So, I
added this feature to CCured and now you will not see these particular errors.
But if you run http@ www.yahoo.com you will get:
Failure STORE_SP at dns_transmit.c:213: dns_transmit_start_sqqff(): Storing stack address
It does not take much to find that this is due to the following code:
# 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;
dns_transmit_start then stores the address of the array servers
into the heap. The solution here is to move the servers array into the
heap (or make it a global). We can achieve the former by declaring:
char servers[64] __HEAPIFY;
and CCured will move it to the heap (see Section 3.5).
Bingo! It seems to work. Now, you can start measuring performance and, if
desired, you can try to make CCured infer better checks for your code.
6.3 Example: PING
In this section I describe what it took to do the ping utility from
netkit-base-0.17.
We download, compile, test it. Then we setup the Makefiles to use ccured
instead of gcc and we test that it works in the –nocure mode. Then we
turn on curing.
First we see two errors pointing out that there is inline assembly in
ping. CCured also prints the instructions and we see that they are just
bit manipulations. So, we just pass –allowInlineAssembly to ccured and go
on.
Now we get:
Failure UBOUND at ping.c:1303: main(): Ubound
To investigate this one we can use CCURED_SLEEP_ON_ERROR (see
Chapter 4). The fragment of code that causes this error is similar to the
following code:
struct icmp {
int various;
char data[1];
};
char outpack[65536];
char foo() {
// Get the 8th data character
return ((struct icmp*)outpack)->data[8];
}
The problem is that once outpack is cast to a 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:
char foo() {
// Get the offset of the 8th data character
int off = (int) & ((struct icmp*)0)->data[8];
return outpack[off];
}
We need to fix that problem in all accesses to the data field. After
that, we run into another problem:
Failure ALIGNSEQ at ./ping_combcured.c:3923: pinger(): Creating an unaligned sequence
This is because at some point we create a sequence pointer whose home area
does not contain a whole number of elements. See Section 3.6.3 for the
various ways to address this problem. We choose to simply tell CCured to allow
partial elements in structures and to adapt its checks accordingly. To achieve
this we pass –allowPartialElementsInSequence to CCured.
Now it works, we are done.
6.4 Example: THTTPD Server
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 . The version I work
with is 2.23 beta 1.
6.4.1 Step 1: Regular Build
First, we unpack the files:
gunzip thttpd-2.23beta1.tar.gz
tar -xvf thttpd-2.23beta1.tar
Look into the directory for the file configure. We don't want to mess up
the /usr/local/ folder, so go into configure and delete the folder path
from ac_default_prefix. Now Makefile should make thttpd to the folder
where the source code resides. Run configure.
./configure
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 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
thttpd. Run the program and test the server from another computer. In my
case, I steered my browser to http://manju.cs.berkeley.edu:7500/ andypang/.
make
a few seconds later...
./thttpd
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. http://manju.cs.berkeley.edu:7500/). A page with a green
background should appear notifying you that thttpd is running.
6.4.2 Step 2: Build with CIL
It's time to look into that Makefile.in that came with thttpd.
Makefile.in is the file from which configure generates 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 CC variable as in the other tutorials.
ifdef CCURED
CC:=/home/andypang/cil/bin/ccured
endif
ifdef NOCURE
CC+= --nocure
endif
ifdef NOMERGE
CC+= --nomerge
endif
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/CCured is run, so I added
the following to clean up the CIL files and folders that will be generated:
CIL = $(SRC:.c=.i) *cil*
COMB = *comb*
I modified the variable CLEANFILES to include those files.
CLEANFILES = $(ALL) $(OBJ) $(GENSRC) $(GENHDR) $(CIL) $(COMB)
Now we are ready to compile using CIL. First, we run configure again to
update the Makefile.
./configure
make clean
make CCURED=1 NOCURE=1 NOMERGE=1
Ensure the application still works correctly. It should. Now build with
merging.
make clean
make CCURED=1 NOCURE=1
Again, check for proper functionality.
6.4.3 Step 3: Build with CCured
The big moment.
make clean
make CCURED=1
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:
libhttpd.c:226: Warning: Malformed format string [child wait - %m]
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:
thttpd.c:437: Warning: Calling function sigset without proper prototype: will be WILD.
sigset has type void * __attribute__((___ptrnode__(1666))) /* /* missing proto */ */()
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:
chmod -R u+w thttpd-2.23beta1
Back to the problem at hand. If one punches in sigset on Google, one
will that it is a function in signal.h. Add the following thttpd.c
to remedy the warning:
extern void *sigset(int, void*);
Although the warning also appeared for the file libhttpd.c, the
prototype in thttpd.c will work for all files in the project.
The next most prevalent warning should be a sscanf error, where CCured
warns that it does not expect the type char *. CCured does not accept
strings in sscanf because one could potentially read in an unbounded
string. This characteristic could be used for malicious intentions.
Although %400[a-zA-Z] is used and hence strings that are accepted by
sscanf will be limited to 400 bytes, CCured 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 %s.
To fix this error, use CCured's sscanf/fscanf functions in place of
the ones in stdio.h. Please refer to Section 9.6.3
for more details. As an example, the following is how I modified the code
at Line 213 in tdate_parse.c.
/* 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 ) )
{
Then we see several warnings regarding the use of sizeof:
libhttpd.c:2782: Warning: Encountered sizeof(char */* __attribute__((___ptrnode__(5491))) */) when type contains pointers. Use sizeof expression. Type has a disconnected node.
We take a look at this line and find that it is a function call to RENEW.
nameptrs = RENEW( nameptrs, char*, maxnames );
The definition of RENEW can be found in libhttpd.h.
#define RENEW(o,t,n) ((t*) realloc( (void*) o, sizeof(t) * (n) ))
The warning arises from the fact that the CCured inferencer cannot make
the connection between nameptrs and char *'s. See Section 9.5
for more details.
To fix the warning, we let CCured inference the argument in sizeof
to nameptr by modifying the code in the following way:
In libhttpd.c
nameptrs = RENEW( nameptrs, nameptr*, maxnames );
In libhttpd.h
#define RENEW(o,t,n) (realloc( (void*) o, sizeof(t) * (n) ))
Now CCured will know that we are allocating memory based on the size of
the pointers to nameptr.
The macro NEW is defined one line before RENEW, and we fix a couple
of calls to NEW in the same way.
We now face a number of warnings of the following form:
libhttpd.c:2519: Warning: Solver: changing User Specified SAFE node 5283 (an unnamed location (often an inserted cast)) to FSEQ
A quick look at libhttpd.c shows that a call to qsort is made.
The wrapper for qsort can be found in stdlib_wrappers.h, and there
appears to be two versions of qsort. One versions supports polymorphism
and the other does not. Add -DUSE_POLYMORPHIC_QSORT in Makefile.in
after we make the call to cil/bin/ccured, so that CCured will know to
use the polymorphic qsort.
This fixes the problems in libhttpd.c but not 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 char *,
but they are also cast to struct strlong * in the function. This is a
bad cast. Change the types of the accepted arguments to void * and
the problem is solved.
Next we tackle a similar problem in tdate_parse.c:
** 1: Bad cast (seq) at tdate_parse.c:202 (struct tm *7100 ->char *7136)
Once again, we use the browser to track down the problem, and find a cast
from a struct tm * to a char *. We change the char * to a
void * and the bad cast disappears.
(void) memset( (void*) &tm, 0, sizeof(struct tm) );
The last bad cast:
** 1: Bad cast at timers.h:41 (void */* __NODE(346) */ *347 ->long *349)
Going to Line 41 reveals a union of void *, int, and long. This
cannot possibly be safe because i could later be used as a pointer
with p. We change this union to a tagged union as instructed in
Section 9.7.
union ClientData {
void* p;
int i;
long l;
} __TAGGED;
typedef union ClientData ClientData;
Chapter 7 How to Eliminate WILD Pointers
As explained in the tutorial, you can use the WILD pointer types to do
most of the things that you can do with pointers in C. And, in fact, CCured's
inferencer will turn some of your pointers into WILD pointers if you use
them in unusual ways.
WILD pointers are bad. Every time you access them you have to also access
the tags. And what makes them really annoying is that they spread very
quickly. Even a few bad casts in your program can lead to a contamination of
30% of the pointers with WILDness. And that means that you'll have to
write lots of wrappers, and hard ones. (In fact, the support that we provide
for writing wrappers does not work in all cases in the presence of WILD
pointers.)
So, we recommend that you take a look at the warnings and messages that
CCured 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
CCured has to help you do that.
First, a few notes:
-
Do not use functions without prototypes. They will be WILD along with
their arguments and result values.
- 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. CCured will
accept that but will make the function WILD!
- If your program has custom memory allocators (generally wrappers around
malloc and friend), you must declare them (Section 7.2).
- If you have functions that use pointers polymorphically, make sure those
pointer types are void * (not char * as it was common before ANSI C).
When it notices bad casts, CCured will print something like this:
** 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
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 (Section 5.1).
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:
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
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 void
* pointer that is used with several incompatible types (in this case char
* and char **). See Section 7.1 for more details on this.
7.1 Polymorphism
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:
int identity_bad(int x) { return x; }
This function can be used with any type that fits in an integer, provided the
appropriate casts from the type to int and back are inserted. But as we
have already discussed in Section 9.4 this won't work in CCured because
the pointers you get out are not usable.
A better way to do this is as follows:
void* identity(void* x) { return x; }
It is a common paradigm in C to use void* for a “pointer to I don't know
what” type. CCured supports this view directly by considering each use of
void * in the program as an occurrence of an unknown type. The CCured
inferencer will try to find a replacement type that makes sense in that
context. For example, in the following code fragment CCured will think of both
occurrences of void * as actually being int * *.
void* identity(void* x) { return x; }
int main() {
int * * p = 0;
int * * res = identity(p);
}
Browse the CCured inferred pointer kinds,
or see the CCured output
for this code fragment
This model works for even very complicated code, such as the following
fragment that
defines a function apply which applies a function pointer to some
arguments (see in the output that all pointers are inferred SAFE):
// 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);
}
Browse the CCured inferred pointer kinds,
or see the CCured output
for this code fragment
In the above example there are four occurrences of void * in the
definition of apply. Based on the actual usage of apply the first two
are mapped to int * and the latter two are mapped to int * *.
This very flexible scheme breaks down when you have inconsistent usage of a
void * type, such as in the following code:
void* identity(void* x) { return x; }
int main() {
int * p = 0;
int * * res_pp = identity(& p);
int * res_p = identity(p);
}
Browse the CCured inferred pointer kinds,
or see the CCured output
for this code fragment
In the above code the identity function is used both with int * and
int ** argument. Since CCured cannot find any single non-WILD type that
is compatible with all contexts in which the void * is used, it is going
to infer that the type of the void * argument is WILD. And since the
argument is assigned to the result (implicitly due to the return
statement) the result type is also WILD. (You can use the browser to see
all the different incompatible types that “flow” into a void *). It
seems that we need a way to tell CCured to treat the two invocations
separately.
CCured has a crude but effective mechanism for doing just that. First, you
have to tell CCured that a function is polymorphic:
#pragma ccuredpoly("identity")
(you can list multiple names in one ccuredpoly pragma. The pragma can
appear anywhere in your program.).
If you tell CCured that a function is polymorphic it will take the following
steps:
-
For each call site of the function, CCured will create a copy of the
function and it will assign it the name /*15*/identity, where the number
15 is a running counter to ensure that the names are different.
- Then it will perform the usual inference in which case each copy of the
identity function is used only once.
- Finally, for each combination of pointer kinds in the
various flavors of identity CCured will keep one copy and erase all the
others.
Consider as an example the code from above, in which all pointers are now
SAFE. The output contains calls to /*1*/identity and /*2*/identity
but since they both have the same pointer kinds for the arguments and results,
only the body of /*1*/identity is kept:
#pragma ccuredpoly("identity")
void* identity(void* x) { return x; }
int main() {
int * p = 0;
int * * res_pp = identity(& p);
int * res_p = identity(p);
}
Browse the CCured inferred pointer kinds,
or see the CCured output
for this code fragment
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 identity function:
#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);
}
Browse the CCured inferred pointer kinds,
or see the CCured output
for this code fragment
Polymorphic types
A similar mechanism is also available for types. You can add in the arguments
of the ccuredpoly pragma strings like "struct list" to say that a copy of
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 CCured type inference.
Note: If the polymorphism directives do not seem to take any effect, pass the
-verbose to ccured to see how it parses them.
For example, here is how you would write polymorphic list length:
#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);
}
Browse the CCured inferred pointer kinds,
or see the CCured output
for this code fragment
You can see in the browser information that the references to struct list
have been replaced with separate names such as 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.
CCured has polymorphism for types and for functions because those are the
entities that can be copied legally in C. There is no similar
polymorphism for data variables, nor should there be..
If you have a type name for a polymorphic structure, then CCured 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.
7.2 User-defined memory allocators
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.
CCured allows you to declare a function to be a user-defined memory allocator
using one of the following pragmas:
#pragma ccuredalloc("myfunc", <zerospec>, <sizespec>)
<zerospec> ::= zero | nozero
<sizespec> ::= sizein(k) | sizemul(k1, k2)
The zero argument means that the allocator zeroes the allocated area.
Otherwise CCured will zero it itself, if it contains pointers. The
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 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
malloc and calloc:
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))
A memory allocator should have return type void *. In the pre-ANSI C days
allocators were written with the type char *. Once you declare a function
to be allocator, its return type will be changed to unsigned long. At all
call sites CCured 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 CCured 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, CCured 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 CCured. The
following program will succeed in trying to dereference the address 5!
#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 !!!
}
Browse the CCured inferred pointer kinds,
or see the CCured output
for this code fragment
Most often the custom-memory allocators are just wrappers around the system
malloc. In that case there is no danger of unsoundness.
Note also that CCured 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 CCured knows what kind of metadata to create.
7.3 Pointers with Run-Time Type Information
There are many C programs in which void * pointers are used
non-parametrically. An example is a global variable (of type void *) that
is used to store values of different types at different times. Consider for
example the following code, where CCured is forced to infer that the g
pointer has kind WILD because the struct foo and struct bar are
incompatible:
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;
}
Browse the CCured inferred pointer kinds,
or see the CCured output
for this code fragment
In this example 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.) CCured will consider the casts on g
as bad and will mark those pointers WILD.
CCured 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 RTTI
annotation:
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;
}
Browse the CCured inferred pointer kinds,
or see the CCured output
for this code fragment
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 CCured output for
the above example you will see that instead the 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 g is
assigned to and is checked when g is used.
CCured can work with run-time type information only for certain pointer
types. We call such types as extensible and for each type we also
construct a name. Specifically, the extensible types are:
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, struct boo and struct bar are extensible
pointers and we can cast pointers to these structs to void * RTTI and
back.
CCured also supports the RTTI pointer kind on pointers whose base type is
different from void. Consider the following example:
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;
}
Browse the CCured inferred pointer kinds,
or see the CCured output
for this code fragment
Notice that the RTTI pointer kind is used with the base kind struct
foo. An RTTI pointer is strictly more powerful than a SAFE pointer of
the same base type. This means that g in the code above can be used to
access the field f1 and f2 without any overhead. This is because
CCured enforces the requirement that an RTTI pointer of base type
T contains only pointer values whose base type extends T. The
extension relationship is a subset of the physical subtyping relationship: we
say that type T extends type Q if:
-
Both T and Q are extensible, and
- Either T and Q are the same type, or
- Q is void, or
- There exists a pragma ccured_extends(T, T') and T' extends
Q. In this case CCured verifies that it is safe to cast a pointer to T
to a pointer to T', using the usual physical subtyping relationships.
The ccured_extends pragmas use extensible type names to declare a
extension hierarchy (similar to a single-inheritance class hierarchy) in which
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
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
void or non-leaf in the extension hierarchy.
For example, in the following code
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")
we can use the RTTI pointer kind for struct foo * and MY_INT *
but not for 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:
-
The RTTI pointer kind is never inferred by the CCured inferencer. You
must specify it on some pointers and then the inferencer will propagate it.
- The RTTI pointer kind is not able to carry bounds information. Thus
you cannot use it on pointers that are involved in pointer arithmetic.
- Only pointers to extensible types can be cast to and from RTTI
pointer types. Additionally, you may cast scalars into RTTI pointers.
- You must use ccured_extends pragmas to declare the extension
hierarchy.
- void* polymorphism is turned off for the __RTTI types.
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:
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);
}
}
Browse the CCured inferred pointer kinds,
or see the CCured output
for this code fragment
Notice the use of the __NOUNROLL typedefs for the function types.
7.3.1 Implementation Details
CCured collects all extensible types in your program (either those declared
using the 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 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
CHECK_RTTICAST is used to walk this encoding to verify a cast from a
RTTI pointer into a SAFE pointer or another RTTI pointer.
7.4 Specifying Trusted Code
In this section we describe a few mechanisms that you can use to override
CCured's reasoning. These are powerful mechanisms but you can use them to
write unsafe code.
7.4.1 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 CCured. In that case, you can use the
__trusted_cast built-in function. In the following example we know that
the boxedint type can encode an integer (if odd) or a pointer to a
boxedint if even. We could use RTTI pointers to encode this safely in
CCured. Or, we can use a trusted cast:
typedef int boxedint; // If even, then a pointer to a boxedint
int unroll(boxedint x) {
if(x & 1) return x;
return unroll(* (int*)__trusted_cast(x));
}
Browse the CCured inferred pointer kinds,
or see the CCured output
for this code fragment
CCured will not complain if the argument and result type of
__trusted_cast are incompatible. However, it will ensure the following:
-
A __trusted_cast 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.
For example, in the following example, the variable q and the field
f1 in struct foo are made FSEQ. The FSEQ constraint propagates
back through __trusted_cast to p.
struct foo {
int * f1;
int f2;
};
struct bar {
int * f1; // This is FSEQ !
int * f2;
};
int main(struct bar * p) {
struct foo * q = __trusted_cast(p);
p->f1 ++; // Make foo.f1 FSEQ
return q[1].f2; // Make q FSEQ
}
Browse the CCured inferred pointer kinds,
or see the CCured output
for this code fragment