.. _genc: Safe C Code =========== Leon can generate from Scala code an equivalent and safe C99 code. Using the verification, repair and synthesis features of Leon 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, one can use the ``--genc`` and ``--o=`` command line options of Leon. .. 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 use 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``, ``int32_t`` and ``uint32_t`` types are available; - And casting from unsigned to signed integer, and vice-versa, is carried out as a regular reintepretation of the binary representation of the integer. Supported Features ------------------ The supported subset of Scala includes part of the core languages features, as well as some extensions from :ref:`XLang `, while ensuring the same expression execution order in both languages. The input program can use types and functions defined in other units; Leon 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: .. list-table:: :header-rows: 1 * - Scala - C99 * - ``Unit`` - ``void`` * - ``Boolean`` - ``bool`` * - ``Byte`` (8-bit integer) - ``int8_t`` * - ``Int`` (32-bit integer) - ``int32_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 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 Leon'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 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 :ref:`XLang ` extensions; - 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 caputre 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: .. code-block:: scala @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: .. list-table:: :header-rows: 1 * - Category - Operators * - Boolean operators - ``&&``, ``||``, ``!``, ``!=``, ``==`` * - Comparision operators over integers - ``<``, ``<=``, ``==``, ``!=``, ``>=``, ``>`` * - Comparision operators over instances of classes - ``==``, ``!=`` * - Arithmetic operators over integers - ``+``, ``-`` (unary & binary), ``*``, ``/``, ``%`` * - 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 ``leon.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: .. code-block:: scala // 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: .. code-block:: scala @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``, Leon provides ``leon.io.StdIn`` and ``leon.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, Leon provides ``leon.io.FileInputStream`` to read data and ``leon.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.