Proposed extension changes to improve backward compatibility

Motivation

One of the benefits of C is that C compilers are available for almost all platforms. You can write portable C code that can run almost anywhere. This is important for open-source code bases.

Because of this, some Checked C users want to compile their Checked C code with exisitng compilers that do not understand Checked C. They will have the benefits of Checked C when using a compiler that understands the extension. Their code will run elsewhere but be less secure.

We propose a set of changes to Checked C to allow the C preprocessor to be used to remove Checked C extensions. You would modify your C files to include a header file that results in Checked C annotations and changes being removed when the compiler does not support Checked C. In this design, we will name the header file optcheckedc.h. Another name would fine.

Types

Pointer types

The Checked C extension has 3 new pointer types: _Array_ptr, _Nt_array_ptr, and _Ptr. It also adds checked array types. The pointer types use syntax based on C++ templates because is is easier to understand.

_Array_ptr<int> p = 0;

declares a pointer to an array of integers where accesses via the pointer are bounds checked.

C has type qualifiers that change the meaning of a type: _Atomic, const, volatile, and restrict. This can be applied to a pointer type by following the * with a list of qualifiers:

int *p const = ...

We propose adding 3 new qualifiers for pointer types:

_Array _Nt_array _Single

These provide an alternate way of declaring the new pointer types:

int *p _Array = ...

declares an array_ptr to an integer. It is equivalent to

_Array_ptr<int> p = ...

The idea of using type qualifiers this way was first proposed by the Deputy system from Berkeley (Jeremy Condit et al., Dependent Types for Low-Level Programming, ESOP '07)

In the case where a C compiler does not support Checked C, the type qualifiers are #defined to an empty string:

#define _Array
#define _Nt_array
#define _Single

Arrays

It is easy to handle checked array types. They are marked by prefixing the dimension with he keyword _Checked example int arr _Checked[5]. In the header file, when a compiler does not support Checked C, we #define the keyword _Checked to the empty string:

#define _Checked

This will also eliminate the _Checked keyword used for _Checked blocks.

Generic types

For generic type applications, we will use a macro to wrap the type arguments. It will discard and the type arguments when Checked C is not available:

#define _TyArg(...) 

and maps it to the Checked C syntax when Checked C is available

#define _TyArg(...) <__VA_ARGS__>

As an example,

malloc<int>(e)

becomes

malloc _TyArg(int) (e)

We propose a two-part approach for generic function definitions and generic struct definitions. These bind type variables that can appear in code. When Checked C is not available, _For_any can be a macro that discards its arguments:

#define _For_any(...) 

The programmer will conditionally typedef void for each type variable bound by the _For_any, so that they are still defined and can be used in code.

#ifndef __checkedc__
typedef void T
#endif
_For_any(T) f(T * _Ptr) { ...}

The typedef is not hidden behind a macro because typedef is a definition in C. There are limits on where definitions can be introduced and using a macro at all locations where _For_any is allowed could produce syntactically incorrect programs.

The same approaches can be used with _Itype_for_any

Existential types

This section is to be filled in.

Bounds annotations

Checked C has bounds annotations that are added to declarations using : bounds-exp, where bounds-exp can be count(e1), bounds(e1, e2), byte_count(e1), or bounds(any). The : lets the parser know that certain identifiers have a context-sensitive meaning, so that we do not have to use an underscore to prefix the name.

To avoid the need for the :, we can introduce four new keywords: _Any, _Bounds, _Byte_count, and _Count. These can be the names of bounds expressions. We can then allow a declarator to be followed by a bounds expression, instead of requiring a :.

When Checked C is not supported, we can introduce macros that discard the keywords:

#define _Any
#define _Bounds(e1, e2)
#define _Byte_count(e1)
#define _Count(e1)

We can introduce a new keyword _Itype for itype annotations also.

Dynamic check expressions

For dynamic check expressions, when a compiler does not support Checked C, we can have a macro that evaluates the argument but does nothing with it.

#define _Dynamic_check(e1) ((void)(e1))

An alternative is to make use of the assert macro:

#define _Dynamic_check(e1) ((e1) ? (void)0 : assert(0))

Bounds cast expressions

_Dynamic_bounds_cast and _Assume_bounds_cast expressions have the form op<T>(e, bounds-expression). The type argument is a problem a problem for non-Checked C compiler. We can introduce variadic macros that take 2 or 3 arguments. For now, we proposed just using an _M as a suffix to indicate that this is a macro. We are open to other suggestions.

_Dynamic_bounds_cast_M(T, e1, ...)
_Assume_bounds_cast_M(T, e1, ...)

When Checked C is supported, they would map to their corresponding syntax forms:

#define _Dymamic_bounds_cast_M(T, e1, ... ) _Dynamic_bounds_cast<T>(e1, __VA_ARGS__)
#define _Assume_bounds_cast_M(T, e1, ...) _Assume_bound_cast<T>(e1, __VA_ARGS__)

When it is not supported, they would become a C-style cast:

#define _Dynamic_bounds_M(T, e1, ...) ((T) e1)
#define _Assume_bounds_cast_M(T, e1, ...) ((T) e1)

Where clauses

For where clauses, we can allow optional parentheses to surround the where clause:

_Where (e1 _And _e2)

When a compiler does not support Checked C, we can have macro that discards the body of the where clause:

#define _Where(e)