Safe 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.
Note
Currently the memory model is limited to stack allocations. 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
anduint8_t
,uint16_t
,uint32_t
,uint64_t
types are available;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 |
---|---|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
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 map 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¶
Array[T]
are implemented using regular C array when the array size is known at compile time, or
using Variable Length Array (VLA) when the size is only available at runtime. Both types of array
use the same unique structure type to keep track of the length of the array and its allocated
memory.
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.
Arrays can be created using the companion object, e.g. Array(1, 2, 3)
, or using the
Array.fill
method, e.g. Array.fill(size)(value)
.
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 mutablevar
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
andvar
are supported for local variable with the limitations imposed by the imperative phases of Stainlessgenerics:
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 |
|
Bitwise operators over integers |
|
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.