Coding Conventions

C Coding Conventions and Style Guide

Formatting, style, and C language subset requirements, divided into general, user-level code, and kernel code, including requirements for verification.

The conventions below apply to all code maintained by the seL4 Foundation in the seL4 GitHub org. They do not apply to external libraries, where we refer to the existing conventions.

Some of the code pre-dates the conventions and we update files incrementally as they are touched, so it may not all comply. However, please ensure that any new code does follow the rules. In general, we strive to abide by the rule

Try and leave the code a little better than you found it.

This guide is in four parts: first, we list general coding conventions; then we divide the rest of the conventions between user level, kernel code, and verification requirements that apply to all kernel code. Please read the appropriate guide, as kernel and user-level conventions sometimes contradict each other.

General C code

This section applies to general C code. There are additional sections with more specifics for user-level and kernel code below.

Compiler options

Code should compile without warnings, with -Wall.

Automatic formatting

For automatic formatting of C code, we use astyle, version 3.1, with the settings declared in the sel4_tools astylerc.

Spacing and braces

  • Indent using four (4) spaces. Do not use tabs for indentation.
  • Use no space between * and the variable name in pointer expressions (int *foo).
  • Use space between keywords and parentheses; e.g., if (condition).

  • Put the opening brace of a function implementation on the line after the function’s return type, name, and argument list.

    int atoi(const char *nptr)
{
    /* ... */
}

  • Use the “one true brace style” (1TBS); use braces everywhere the syntax allows, including single-statement scopes.

    if (x == FOO) {
    do_something();
} else if (y == BAR) {
    do_something_else();
} else {
    do_last_else();
}

  • When a function argument list gets too long for one line, indent the remaining arguments on the next line just inboard of the parenthesis on the line above. For example:

    void myfunc(my_ridiculously_long_type_t foo,
            my_ridiculously_long_type_t bar)
{
    /* ... */
}

Header guards

Use #pragma once in header files to avoid duplicated includes.

Choosing data types

When using integral types (char, int, long, etc.), qualify them explicitly as unsigned except where negative values are meaningful and must be handled. Overflow of signed integral types is undefined behaviour in the C standard, whereas overflow of unsigned integral types is defined.

Naming of symbols (variables), types, and type aliases (typedef)

  • Use typedef to create aliases for all struct types.
  • The names of type aliases should always end in _t.
  • Function pointer type aliases should always end in _fn_t.

  • Do not alias pointer types with typedef; we keep them explicit.

    typedef tick_count unsigned int;

typedef tick_count_ptr_t *tick_count; /* NO */
tick_count *tick_count_ptr; /* yes */
  • Use snake_case to name a multi-word variable or type.
  • Non-static functions should be prefixed with appropriate names to avoid polluting the namespace.
    • The convention in library code is to use the name of the library.
    • A good guide for application code is to use the filename.
  • Name Boolean variables with a verb phrase including a verb like is_, has_, or want_ so that the intent of the variable is clear in expressions and conditionals.
  • Avoid magic numbers; define meaningful constants. Prefer C language symbols over preprocessor symbols, because the former are visible in a symbolic debugger like gdb.
  • Use SCREAMING_SNAKE_CASE for, and only for, preprocessor symbols and values of enumeration type.
  • Prefix architecture-specific code with arch_, platform-specific code with plat_, and mode-specific code with mode_.

Expressions

  • Avoid pointer arithmetic unless necessary.
  • Always use preprocessor macros for bit manipulation, e.g., use BIT(7) instead of 1 << 7.

Structure

  • Put architecture- and platform-specific code in dedicated directories.
  • Only static inline functions are permitted in header files, and then only for performance.
  • Variables at file scope must be marked as static.
  • Use public/private header files; avoid extern unless necessary.
  • General-purpose utility functions belong in shared libraries, not library-specific files, and vice versa. Consider checking libutils in the util_libs Git repository for existing functionality, and consider making useful additions there.
  • Prefer static inline functions over preprocessor macros unless preprocessor features are required or the macro is simple.
  • Put a comment after the #endif of an #if, #ifdef, or #ifndef blocks that refers to the preprocessor symbol(s) upon which the code is guarded.
  #ifdef CONFIG_BLAH
  /* ... */
  #endif /* CONFIG_BLAH */

Memory allocation

For memory that should be zeroed, use calloc rather than malloc followed by memset or bzero.

Commenting

  • Prefer /* this style */ comments over // this style.
  • Use Javadoc-style comments on function prototypes in headers.
  • Document function parameters and return types, at minimum.

User-level code

In addition to the general rules, please follow the below for user-level code. These are different to kernel code requirements.

Type conventions

Be aware that our code needs to be portable across 32- and 64-bit platforms.

  • Use seL4_Word for word-sized things.
  • Use void * for untyped addresses.
  • Use uintptr_t for pointer arithmetic…
  • …but avoid pointer arithmetic unless necessary.
  • Use size_t for sizes of objects (including pointers themselves).
  • Use unsigned int for values known to be small.
  • Use fixed-width types only when necessary, e.g., in device drivers.
  • Use long variants of built-in functions (CLZL) for 64-bit compatibility, unless operating on a fixed-width type.
  • Use typedef to create aliases for all enum types.

Format strings

  • Use 64-bit-friendly printing macros for printf, e.g., PRIi32 for uint32_t.
  • Use %p for pointers.
  • Use %zd and %zu for ssize_t and size_t respectively.

Error handling

  • Always check error codes.
  • Use assert only to test invariants in code.
  • Use ZF_LOGF for fatal errors: it will call abort().
  • For all other error reporting, use the appropriate ZF_LOG level.
  • Use only ZF_LOG macros for diagnostic messages–not printf.
  • Try to follow a transactional approach to error handling: check input and report errors before modifying state.

Kernel code

In addition to the general and verification requirements, use the following for kernel code. These are different to user level requirements.

  • Use word_t for word-sized things.
  • Do not explicitly typecast between pointers and references, i.e., integers used as, e.g., offsets into structures: use object-specific macros for this purpose, such as TCB_REF and TCB_PTR.

Format strings

The in-kernel printf implementation is limited.

  • Use %p for pointers.
  • Use %lu for words, and cast to avoid warnings.

Error handling

Within seL4, the decode stage must only check conditions; the invoke stage can alter state.

Verification requirements

Verified code such as in kernel code must follow these requirements. If in doubt, verified code requirements override anything in the general guide.

  • Follow the C99 standard. (The link is to the final draft before ratification; the official standard document cannot be distributed freely.)
  • Do not take the address of a variable of automatic storage class. In most C implementations, this means stack-allocated locals.
  • Do not use floating-point types, e.g., double or float.
  • Do not use restrict.
  • Do not use union types; use the bitfield generator instead.
  • Do not pre-increment or pre-decrement variables (++x, --y).

  • Do not use variable names that duplicate typedef type aliases:

    typedef int A;
A A; /* NO */
  • Do not use fall-through cases in switch statements.
  • Do not use variadic argument lists.
  • Declare functions that take no arguments as taking a void argument.
  • References to linker addresses must be via extern char[] declarations rather than declarations of other types such as extern char or extern void *.

  • Do not pass arrays as arguments to functions expecting pointers.

    void foo(int *some_pointer);
int my_array[10];
foo(my_array); /* NO */
  • Do not declare local variables as static.
  • Prefix struct fields with the name of the struct to avoid namespace conflicts in the proof. Much existing kernel code does not follow this directive; new code should adopt the recommended practice to avoid namespace collisions in proofs.
  • Do not use typedef to create a type alias for an enum; always specify enum types as word_t. Otherwise, the enum size is determined by the compiler.
  • All struct definitions must be packed, i.e. not contain any implicit padding that is inserted by the compiler – otherwise memory content is unspecified. Use explicit padding fields of the required type size to remove implicit compiler padding.

Further resources