Generating C Code

Stainless can generate from Scala code an equivalent and safe C99 code. Using the verification, repair and synthesis features of Stainless this conversion can be made safely. Additionally, the produced code can be compiled with any standard-compliant C99 compiler to target the desired hardware architecture without extra dependencies. The motivation, detailed supported features, design decisions and performance benchmarks can be found in Extending Safe C Support In Leon. Furthermore, this Master Thesis Report explains how to achieve compliance under the MISRA C guidelines.

To convert a Scala program, please use the --genc option of Stainless.

The option --genc-output=file specifies the file name for GenC output (default: stainless.c).

Note

Currently the memory model is limited to stack allocation and global state. Hence, no dynamic allocation is done using malloc function family.

Requirements

The following is required from the Scala program fed to GenC:

• Any functions reachable from the main function, and the types they use, should be exclusively in the set of features described below, with the exceptions of the code used for verification conditions;

• The program should be successfully verified with the --strict-arithmetic flag to ensure that arithmetic operations, array accesses, function preconditions and so on, are safely converted into C code.

The generated C code should be compiled with a C99-compliant compiler that satisfy these extra conditions:

• CHAR_BITS is defined to be 8;

• The int8_t, int16_t, int32_t, int64_t and uint8_t, uint16_t, uint32_t, uint64_t types are available (see Pure Scala for description);

• Casting from unsigned to signed integer, and vice-versa, is not well supported at the moment.

Supported Features

The supported subset of Scala includes part of the core languages features, as well as some imperative features, while ensuring the same expression execution order in both languages.

The input program can use types and functions defined in other units; Stainless will scan each dependency in turn starting from the main unit. It is therefore mandatory that every dependency use exclusively supported features to allow the conversion to succeed.

Types

The following raw types and their corresponding literals are supported:

Scala	C99
Unit	void
Boolean	bool
Byte and Int8 (8-bit integer)	int8_t
Short and Int16 (16-bit integer)	int16_t
Int and Int32 (32-bit integer)	int32_t
Long and Int64 (64-bit integer)	int64_t
UInt8 (8-bit unsigned integer)	uint8_t
UInt16 (16-bit integer)	uint16_t
UInt32 (32-bit integer)	uint32_t
UInt64 (64-bit integer)	uint64_t

Additionally, GenC has a partial support for character and string literals made of ASCII characters only but it has no API to manipulate strings at the moment: Char is mapped to char and String is mapped to char*.

Tuples

Using TupleN[T1, ..., TN] results in the creation of a C structure with the same fields and matching types for every combination of any supported type T1, ..., TN. The name of the generated structure will be unique and reflect the sequence of types.

Arrays

Arrays are compiled by GenC into C structs that also store the length of the array. For Array[Int] we get:

typedef struct {
  int32_t* data;
  int32_t length;
} array_int32;

Note

Arrays live on the stack and therefore cannot be returned by functions. This limitation is extended to other types having an array as field. In some cases, it is acceptable to use the @inline annotation from Stainless’s library to workaround this limitation.

For case classes containing arrays whose length is known at compile time, we avoid using a struct wrapper for the array, and instead directly inline the array in the struct of the case class. We trigger this optimized transformation when the array length is specified in the case class invariant (with require) as a conjunct. The left-hand-side needs to be a.length where a is the array, and the right-hand-side needs to be a constant (or evaluate to a constant at compile time).

See below for a case class with a fixed length array and its transformation in C:

val CONSTANT1: UInt16 = 5
val CONSTANT2: UInt16 = 12
val CONSTANT3: UInt16 = CONSTANT1 + CONSTANT2

@cCode.export
case class W(x: Int, a: Array[Int], y: Int) {
  require(
    a.length == CONSTANT3.toInt &&
    0 <= x && x <= 1000 &&
    0 <= y && y <= 1000
  )
}

typedef struct {
  int32_t x;
  int32_t a[17];
  int32_t y;
} W;

Classes

The support for classes is restricted to non-recursive ones so that instances of such data-types live on the stack. The following language features are available:

• case class with mutable var fields;

• generics:

  • similarly to Array[T] or tuples, each combination of type parameters is mapped to a specific C structure;

• inheritance:

  • when all leaf classes have no fields, the class hierarchy is mapped to a C enumeration,

  • otherwise, a tagged-union is used to represent the class hierarchy in C;

• external types:

  • see @cCode.typedef below.

Functions

Functions with access to the variables in their respective scopes. The following language features are available:

• top level, nested or member functions:

  • both val and var are supported for local variable with the limitations imposed by the imperative phases of Stainless

• generics:

  • each combination of type parameters generates a different, specialised C function;

• overloading:

  • the Scala compiler is responsible for identifying the correct function at each call site;

• higher-order functions:

  • named functions that do not capture their environment can be used as value;

• external functions:

  • see @cCode.function below;

Since strings of characters are currently not (fully) available, in order to generate an executable program, one has to define a main function without any argument, that can optionally return an integer, as follows: def _main(): Int = .... Moreover, an extern main function of the following form is required in order to preserve the executability of the Scala program:

@extern
def main(args: Array[String]): Unit = _main()

Constructs

The idiomatic if statements such as val b = if (x >= 0) true else false are converted into a sequence of equivalent statements.

Imperative while loops are also supported.

Pattern matching is supported, with the exception of the Unapply Patterns, as long as it is exempt of side effect.

Assertions, invariant, pre- and post-conditions are not translated into C99 and are simply ignored.

Operators

The following operators are supported:

Category	Operators
Boolean operators	&&, ||, !, !=, ==
Comparision operators over integers	<, <=, ==, !=, >=, >
Comparision operators over instances of classes	==, !=
Arithmetic operators over integers	+, - (unary & binary), *, /, %
Bitwise operators over integers	&, |, ^, ~, <<, >>>

Global State

At the moment, Stainless does not support global mutable variables declared in objects. It is however possible to simulate global state by using classes marked with @cCode.global, as shown in the Global.scala example:

@cCode.global
case class GlobalState(
  val data: Array[Int] = Array.fill(100)(0),
  var stable: Boolean = true,
  var x: Int = 5,
  var y: Int = 7,
) {
  require(
    data.length == 100 && (
      !stable || (
        0 <= x && x <= 100 &&
        0 <= y && y <= 100 &&
        x + y == 12
      )
    )
  )
}

Note

In classes annotated with @cCode.global, only arrays with a fixed length are allowed. Please check the paragraph about arrays to learn how to specify the array length.

This annotation triggers some checks to make sure that indeed the GlobalState class (the name of the class can be changed, and there can be multiple such classes) is used as a global state:

• Functions can take as argument at most one instance per each global class such as GlobalState.

• There can be at most one instance created for each global class such as GlobalState (in a function that doesn’t already take an instance of that class as argument).

• A GlobalState instance can only be used for reads and assignments (e.g. it cannot be let bound, except for the declaration mentioned above).

• The only global state that can be passed to other functions is the one we create or the one we received as a function argument.

These checks ensure that the fields of GlobalState can be compiled as global variables in C. Consider the move function from the Global.scala example:

def move()(implicit state: GlobalState): Unit = {
  require(state.stable && state.y > 0)
  state.stable = false
  state.x += 1
  state.y -= 1
  state.data(state.y) = 1
  state.stable = true
  if (state.y > 0) move()
}.ensuring(_ => state.stable)

After compilation to C, we get the following function, with global declarations stable, x, y, and data.

int32_t data[100] = { 0 };
bool stable = true;
int32_t x = 5;
int32_t y = 7;

void move() {
    stable = false;
    x = x + 1;
    y = y - 1;
    data[y] = 1;
    stable = true;
    if (y > 0) {
        move();
    }
}

Note that the initial values for the global variables correspond to the default values given in the Stainless class declaration (default values are mandatory when using the @cCode.global annotation). When creating a global state instance (the only one), we do not pass arguments, to make sure that the instance is created using the default values:

@cCode.export
def main() {
  implicit val gs = GlobalState()
  StdOut.print(gs.x)
  StdOut.print(gs.y)
  move()
  StdOut.print(gs.data(6))
  StdOut.print(gs.data(7))
  StdOut.print(gs.x)
  StdOut.println(gs.y)
}

Stainless supports two variants of the @cCode.global annotation, namely @cCode.globalUninitialized and @cCode.globalExternal. The first one generates global declarations without initial values. These global variables are thus initialized according to C semantics, and there can be a mismatch between the global state instance created by the user, and the initial values in C. The second one hides the global declarations, which can be useful when interacting with C code that declares global variables outside of the Stainless program.

Export

Functions and classes can be marked with @export, which affects GenC compilation in several ways. First, the names of these functions and classes will not get mangled when generating the C code. Second, the signatures of the functions, and the type definitions corresponding to exported classes, will go into the header file (by default stainless.h). Finally, preconditions of exported functions (which are meant to be called from external C code), are transformed into runtime assertions.

Custom Conversion

When it comes to function using system calls, such as I/Os, no automated conversion is possible. In those situations the user can define his own implementation for functions, add manual conversion from Scala types to C types or even drop some functions and types from the translation, with @cCode.function, @cCode.typedef and @cCode.drop annotations from the package stainless.annotation, respectively. Their usage is described below.

Custom Function Implementation

In order to circumvent some current limitations of GenC, one can use @cCode.function(code, includes) to define the corresponding implementation of any top-level function or method, usually accompanied by @extern. Its usage is as follows:

• For convenience, the C implementation generated by code is represented using a String and not an Abstract Syntax Tree. The user is responsible for the correctness of the provided C99 code. Because GenC might rename the function, e.g. to deal with overloading, the special __FUNCTION__ token should be used instead of the original name. Furthermore, the parameters and return type should match the signature automatically generated by GenC.

• The optional parameter includes can hold a colon separated list of required C99 include header files.

Here is a typical example:

// Print a 32-bit integer using the *correct*
// format for printf in C99
@cCode.function(
  code = """
    | void __FUNCTION__(int32_t x) {
    |  printf("%"PRIi32, x);
    | }
    """,
  includes = "inttypes.h:stdio.h"
)
def myprint(x: Int): Unit = {
  print(x)
}

Custom Type Translation

When a whole type need to be represented using a special C type, the @cCode.typedef(alias, include) annotation can be used. Here the include parameter is also optional, however it can only refer to one header, as it is not expected to have a type defined in several headers. The alias string must represent an existing and valid type.

Using an aliasing from S to C implies that every function that accept a S in the input program must accept a C in the generated C code. Usually, using this annotation implicates manually defining the implementation of functions using this type with @cCode.function.

Here is an example:

@cCode.typedef(alias = "FILE*", include = "stdio.h")
case class MyFile( ...

Ignore Function or Type

It is also possible to skip the translation of some functions or types that are only used as implementation details in proofs, for example, using the @cCode.drop() annotation.

API For Safe Low Level Programs

In this section we describe the APIs that can be used to make the bridge between some Scala programming facilities and their low level, equivalent, C features.

I/Os

Similarly to Scala’s scala.io.StdIn and scala.io.StdOut, Stainless provides stainless.io.StdIn and stainless.io.StdOut. These two APIs are provided with equivalent C code for easy translation with GenC, but are also shaped to allow users to write proofs in a non-deterministic environment.

Furthermore, Stainless provides stainless.io.FileInputStream to read data and stainless.io.FileOutputStream to write data to a file with a C99 compatible API.

Note

It is important that you close the stream after it was created or your C application might leak resources.