Add documentation about GenC

src/sphinx/genc.rst

+.. _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.
+
+To convert a Scala program, one can use the ``--genc`` and ``--o=<output.c>`` command line options
+of Leon.
+
+.. NOTE::
+  Currently the memory model is limited to stack-allocated memory. Hence, no dynamic allocation
+  is done using ``malloc`` function family.
+
+
+Supported Features
+------------------
+
+The supported subset of Scala includes part of the core languages features, as well as some
+extensions from :ref:`XLang <xlang>`, while ensuring the same expression execution order in both
+languages.
+
+Currently all type and function definitions need to be included in one top level object.
+
+
+Types
+*****
+
+The following raw types and their corresponding literals are supported:
+
+.. list-table::
+  :header-rows: 1
+
+  * - Scala
+    - C99
+  * - ``Unit``
+    - ``void``
+  * - ``Boolean``
+    - ``bool``
+  * - ``Int`` (32-bit Integer)
+    - ``int32_t``
+
+Tuples
+^^^^^^
+
+Using ``TupleN[T1, ..., TN]`` results in the creation of a C structure with the same
+fields and 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.
+
+
+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)``.
+
+
+Case Classes
+^^^^^^^^^^^^
+
+The support for classes is restricted to non-recursive case classes for which fields are immutable.
+Instances of such data-types live on the stack.
+
+
+Functions
+*********
+
+Functions and nested functions are supported, with access to the variables in their respective
+scopes. However, higher order functions are as of this moment not supported.
+
+Since strings of characters are currently not available, to generate an executable program, one has
+to define a main function without any argument that returns an integer: ``def main: Int = ...``.
+
+Both ``val`` and ``var`` are supported with the limitations imposed by the :ref:`XLang <xlang>`
+extensions.
+
+
+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.
+
+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
+    - ``<``, ``<=``, ``==``, ``!=``, ``>=``, ``>``
+  * - Arithmetic operators over integers
+    - ``+``, ``-`` (unary & binary), ``*``, ``/``, ``%``
+  * - Bitwise operators over integers
+    - ``&``, ``|``, ``^``, ``~``, ``<<``, ``>>``
+
+

src/sphinx/index.rst

@@ -25,6 +25,7 @@ Contents:
    limitations
    synthesis
    repair
+   genc
    options
    faq
    references

src/sphinx/options.rst

@@ -20,41 +20,46 @@ Choosing which Leon feature to use
 The first group of options determine which feature of Leon will be used.
 These options are mutually exclusive (except when noted). By default, ``--verify`` is chosen.
 
-* ``--eval`` 
- 
+* ``--eval``
+
   Evaluates parameterless functions and value definitions.
-  
+
 * ``--verify``
-  
+
   Proves or disproves function contracts, as explained in the :ref:`verification` section.
 
 * ``--repair``
-  
+
   Runs program :ref:`repair <repair>`.
-  
+
 * ``--synthesis``
-  
+
   Partially synthesizes ``choose()`` constructs (see :ref:`synthesis` section).
 
 * ``--termination``
-  
+
   Runs termination analysis. Can be used along ``--verify``.
 
-* ``--inferInv`` 
+* ``--inferInv``
+
+  Infer invariants from the (instrumented) code (using Orb).
 
-  Infer invariants from the (instrumented) code (using Orb)
+* ``--instrument``
 
-* ``--instrument``                
+  Instrument the code for inferring time/depth/stack bounds (using Orb).
 
-  Instrument the code for inferring time/depth/stack bounds (using Orb)
+* ``--genc``
+
+  Translate a Scala program into C99 equivalent code (see :ref:`genc` section); requires
+  ``--xlang``.
 
 * ``--noop``
-  
+
   Runs the program through the extraction and preprocessing phases, then outputs it in the specified
   directory. Used mostly for debugging purposes.
 
 * ``--help``
-  
+
   Prints a helpful message, then exits.
 
 
@@ -65,44 +70,46 @@ Additional top-level options
 These options are available to all Leon components:
 
 * ``--debug=d1,d2,...``
-  
+
   Enables printing detailed messages for the components d1,d2,... .
-  Available components are: 
+  Available components are:
 
   * ``datagen`` (Data generators)
-  
+
   * ``eval`` (Evaluators)
-  
+
+  * ``genc`` (C code generation)
+
   * ``isabelle`` (:ref:`The Isabelle-based solver <isabelle>`)
 
   * ``leon`` (The top-level component)
-  
+
   * ``options`` (Options parsed by Leon)
- 
+
   * ``positions`` (When printing, attach positions to trees)
 
   * ``repair`` (Program repair)
-  
+
   * ``solver`` (SMT solvers and their wrappers)
-  
+
   * ``synthesis`` (Program synthesis)
-  
+
   * ``termination`` (Termination analysis)
-  
+
   * ``timers`` (Timers, timer pools)
-  
+
   * ``trees`` (Manipulation of trees)
- 
+
   * ``types`` (When printing, attach types to expressions)
 
   * ``verification`` (Verification)
-  
+
   * ``xlang`` (Transformation of XLang into Pure Scala programs)
 
 
 * ``--functions=f1,f2,...``
-  
-  Only consider functions f1, f2, ... . This applies to all functionalities 
+
+  Only consider functions f1, f2, ... . This applies to all functionalities
   where Leon manipulates the input in a per-function basis.
 
   Leon will match against suffixes of qualified names. For instance:
@@ -111,22 +118,22 @@ These options are available to all Leon components:
   This option supports ``_`` as wildcard: ``--functions=List._`` will
   match all ``List`` methods.
 
-* ``--solvers=s1,s2,...`` 
-  
-  Use solvers s1, s2,... . If more than one solver is chosen, all chosen 
+* ``--solvers=s1,s2,...``
+
+  Use solvers s1, s2,... . If more than one solver is chosen, all chosen
   solvers will be used in parallel, and the best result will be presented.
   By default, the ``fairz3`` solver is picked.
- 
-  Some solvers are specialized in proving verification conditions 
-  and will have hard time finding a counterexample in case of an invalid 
+
+  Some solvers are specialized in proving verification conditions
+  and will have hard time finding a counterexample in case of an invalid
   verification condition, whereas some are specialized in finding
   counterexamples, and some provide a compromise between the two.
   Also, some solvers do not as of now support higher-order functions.
 
   Available solvers include:
-  
-  * ``enum`` 
-    
+
+  * ``enum``
+
     Uses enumeration-based techniques to discover counterexamples.
     This solver does not actually invoke an SMT solver,
     and operates entirely on the level of Leon trees.
@@ -134,50 +141,50 @@ These options are available to all Leon components:
   * ``fairz3``
 
     Native Z3 with z3-templates for unfolding recursive functions (default).
-  
+
   * ``smt-cvc4``
-    
-    CVC4 through SMT-LIB. An algorithm within Leon takes up the unfolding 
-    of recursive functions, handling of lambdas etc. To use this or any 
+
+    CVC4 through SMT-LIB. An algorithm within Leon takes up the unfolding
+    of recursive functions, handling of lambdas etc. To use this or any
     of the following CVC4-based solvers, you need to have the ``cvc4``
     executable in your system path (the latest unstable version is recommended).
-  
+
   * ``smt-cvc4-cex``
- 
+
     CVC4 through SMT-LIB, in-solver finite-model-finding, for counter-examples only.
     Recursive functions are not unrolled, but encoded through the
     ``define-funs-rec`` construct available in the new SMTLIB-2.5 standard.
     Currently, this solver does not handle higher-order functions.
-  
+
   * ``smt-cvc4-proof``
-   
-    CVC4 through SMT-LIB, for proofs only. Functions are encoded as in 
+
+    CVC4 through SMT-LIB, for proofs only. Functions are encoded as in
     ``smt-cvc4-cex``.
     Currently, this solver does not handle higher-order functions.
-  
+
   * ``smt-z3``
-   
-    Z3 through SMT-LIB. To use this or the next solver, you need to 
+
+    Z3 through SMT-LIB. To use this or the next solver, you need to
     have the ``z3`` executable in your program path (the latest stable version
     is recommended). Inductive reasoning happens on the Leon side
     (similarly to ``smt-cvc4``).
-  
+
   * ``smt-z3-q``
-   
-    Z3 through SMT-LIB, but (recursive) functions are not unrolled and are 
+
+    Z3 through SMT-LIB, but (recursive) functions are not unrolled and are
     instead encoded with universal quantification.
     For example, ``def foo(x:A) = e`` would be encoded by asserting
-    
+
     .. math::
-    
+
       \forall (x:A). foo(x) = e
 
     even if ``e`` contains an invocation to ``foo``.
 
     Currently, this solver does not handle higher-order functions.
-  
+
   * ``unrollz3``
-    
+
     Native Z3, but inductive reasoning happens within Leon (similarly to ``smt-z3``).
 
   * ``ground``
@@ -187,21 +194,23 @@ These options are available to all Leon components:
   * ``isabelle``
 
     Solve verification conditions via Isabelle.
-  
+
 * ``--strict``
 
-  Terminate Leon after each phase if a non-fatal error is encountered 
+  Terminate Leon after each phase if a non-fatal error is encountered
   (such as a failed verification condition). By default, this option is activated.
 
 * ``--timeout=t``
 
   Set a timeout for each attempt to prove one verification condition/
   repair one function (in sec.)
-    
+
 * ``--xlang``
-  
+
   Support for additional language constructs described in :ref:`xlang`.
-  These constructs are desugared into :ref:`purescala` before other operations.
+  These constructs are desugared into :ref:`purescala` before other operations,
+  except for the ``--genc`` option which uses the original constructs to generate
+  :ref:`genc`.
 
 Additional Options (by component)
 ---------------------------------
@@ -222,10 +231,12 @@ File Output
 ***********
 
 * ``--o=dir``
-  
+
   Output files to the directory ``dir`` (default: leon.out).
   Used when ``--noop`` is selected.
 
+  When used with ``--genc`` this option designates the output *file*.
+
 Code Extraction
 ***************
 
@@ -245,21 +256,21 @@ Synthesis
   Shrink non-deterministic programs when tests pruning works well.
 
 * ``--cegis:vanuatoo``
- 
+
   Generate inputs using new korat-style generator.
-  
+
 * ``--costmodel=cm``
-  
+
   Use a specific cost model for this search.
   Available: ``Naive``, ``WeightedBranches``
 
 * ``--derivtrees``
-  
+
   Generate a derivation tree for every synthesized function.
   The trees will be output in ``*.dot`` files.
 
 * ``--manual=cmd``
-  
+
   Override Leon's automated search through the space of programs during synthesis.
   Instead, the user can navigate the program space manually
   by choosing which deductive synthesis rules is instantiated each time.
@@ -277,26 +288,26 @@ Fair-z3 Solver
   Double-check counter-examples with evaluator.
 
 * ``--codegen``
-  
+
   Use compiled evaluator instead of interpreter.
 
 * ``--evalground``
- 
+
   Use evaluator on functions applied to ground arguments.
-  
+
 * ``--feelinglucky``
-  
+
   Use evaluator to find counter-examples early.
 
 * ``--unrollcores``
- 
+
   Use unsat-cores to drive unrolling while remaining fair.
-  
+
 CVC4 Solver
 ***********
 
 * ``--solver:cvc4=<cvc4-opt>``
-  
+
   Pass extra command-line arguments to CVC4.
 
 Isabelle