Deputy Quick Reference


Getting Started

Run ivycc --deputy on a C file in place of gcc. (In many cases, this is as simple as changing CC in your makefile.) You will probably see a number of type errors, beginning with a series of warnings that suggest annotations. You can fix these errors by inserting annotations listed below. Hairier parts of the code can be skipped using the "trusted" annotations below. Once your file compiles, you'll need to use deputy for the linker as well so that Deputy can link in its (small) runtime library.

Now run and test your program. You will probably see some run-time errors due to insufficient or incorrect annotations. Fix these errors and you're good to go!


Pointer and Array Bounds

Pointer annotations are placed after the * in the pointer type. Array annotations are placed immediately before the name of the array, using parentheses. For example, the COUNT(42) annotation can be placed as follows:

int * COUNT(42) ptr; int (COUNT(42) array)[]:

The basic Deputy bounds annotations are given in the following table. The type checker assumes that every pointer and array in the program is annotated with one of these annotations. Deputy will provide a suitable default for each unannotated pointer.

BOUND(b, e)
BND(b, e)
The pointer is either null or it points to an array of objects of the base type with bounds given by the local expressions b and e. This pointer must be aligned with respect to both b and e. The keyword __this refers to the variable or expression to which this type is attached. To use automatic bounds, specify __auto in place of b and/or e.
COUNT(n) CT(n) The pointer is either null or it points to an array of n objects of the base type. Equivalent to BOUND(__this, __this + n). This annotation is the default for arrays with declared size n.
SAFE The pointer is either null or it bounds to a single object of the base type. Equivalent to COUNT(1) and BOUND(__this, __this + 1). This annotation is the default for global variables, structure fields, and function arguments and return values.
SNT This pointer is used only for comparison and never for dereference. Mostly equivalent to COUNT(0) and BOUND(__this, __this), but currently carries an extra attribute that allows it to be incremented and decremented freely.
SEQ A shorthand for BOUND(__auto, __auto). Deputy will insert automatic bounds variables for both bounds. Note that this annotation must be used with care on any externally-visible data! This annotation is the default for local variables.
FSEQ A shorthand for BOUND(__this, __auto). Deputy will insert an automatic bounds variable for the upper bound, and the lower bound is assumed to be the pointer itself. As with SEQ, this annotation must be used with care on any externally-visible data!

You may also indicate whether a pointer is non-null with the following annotations:

NONNULL Indicates that a pointer must be non-null.
OPT Indicates that a pointer may be null. This annotation is the default on all pointers.

Null-Terminated Pointers and Arrays

In addition to the bounds annotations provided above, you may also indicate that a pointer or array is null-terminated by using one of the following annotations:

NT Indicates that the upper bound of the pointer (as given by BOUND or one of its relatives) is the beginning of a null-terminated sequence of elements.
NTS A shorthand for NT COUNT(0)--think "null-terminated string". This annotation is often used for char * pointers that represent null-terminated strings. Note that because it includes a COUNT annotation, it is provided in place of (rather than in addition to) the bounds annotations in the previous section.

There are two operations that allow you to convert between null-terminated and regular pointers:

NTDROP(e) Converts a null-terminated pointer e with type NT BOUND(b, e) into a standard pointer with bounds BOUND(b, e). Because the null terminator lies outside of the specified bounds, this operation is safe; however, the null element (and any other elements outside the specified bounds) may no longer be accessible.
NTEXPAND(e) Expands the upper bound of e up to the null element. For example, if e has type NT COUNT(0) but points to a string with 5 characters (plus a null character), then NTEXPAND(e) will have type NT COUNT(5). This operation is often used immediately before an NTDROP in order to preserve access to all elements except for the null terminator itself.

Union Annotations

Unions are annotated by indicating when each field is active. For example:

struct foo { int tag; union foo { int *p WHEN(tag == 0); int n WHEN(tag == 1); } u; };

Note that the annotation is placed after the name of each field, not on the type of each field. The annotation is defined as follows:

WHEN(e) Indicates that the associated union field is selected when the local expression e evaluates to a non-zero value. The expression e is local with respect to the union itself, so it can refer to other names at the same level as the union. At most one field may be selected at any given time.

Special Function Annotations

Deputy provides annotations that identify several common C functions that require special treatment. These annotations are placed on the function type by writing them before the name of the function, in parentheses. For example:

void * (DALLOC(sz) malloc)(size_t sz);

These annotations are as follows:

DALLOC(e) This annotation indicates a function that acts as an allocator. The expression e indicates the size of the allocated block (in bytes) in terms of the function's formal parameters. The type of the allocation is determined by the pointer to which the result of this call is assigned, and the size is used to check (or set, in the case of automatic bounds) the bounds of the resulting pointer.
DFREE(p) This annotation indicates a function that frees memory. The argument p is the name of the formal parameter for the pointer being freed.
DREALLOC(p, e) This annotation indicates a function that acts as a reallocator; the arguments p and e function as specified in the previous two annotations. Note that newly-allocated portions of the array are not automatically zeroed by Deputy.
DMEMCPY(x, y, z)
DMEMSET(x, y, z)
DMEMCMP(x, y, z)
These annotations specify that the function behaves like memcpy, memset, or memcmp. The three arguments x, y, and z are meant to indicate the indices of the arguments that behave like the corresponding arguments for the original function; however, they are ignored by the current implementation. When Deputy sees a call to a function with one of these annotations, it verifies the bounds of the pointers passed to these functions, and when data is being written, it verifies that the data written has the correct type. In the case of memset, we allow arrays containing pointers to be initialized to zero (assuming, of course, that those pointers are not non-null).

Trusted Annotations

Deputy allows the user to trust code in cases where Deputy annotations cannot easily be provided. There are several ways to indicate trusted code:

First, you may specify trusted blocks of code. If you place TRUSTEDBLOCK after the opening brace of a block, Deputy will not attempt to check any code contained therein. If this block reads variables with automatic bounds, Deputy will adjust the code as necessary to allow the read to occur. However, writes to variables with automatic bounds are not allowed.

Second, you may use the TRUSTED annotation, which can appear in three places:

For convenience, you can use the macro TC(e) to convert a pointer expression e to a trusted version of the same pointer. This macro is very useful for performing trusted casts from one pointer type to another.