Topic/genc v2: ready for general review #290
Commits on Feb 13, 2017
-
- augment list of known compilers (with compcert) - adapt this list for the current OS - use advanced parameters (e.g. sanitizers) - run all found compilers - add ability to disable a given compiler on a case-by-case basis - ignore files generated by tests - improve error messages - report warnings and other errors from the GenC phase (and others)
-
-
-
-
This new implementation of GenC uses a pipelined approach: the translation of Scala code into C99 equivalent code is split into several phases that live in the `leon.genc.phases` package. The overall process is bases on several versions of an Intermediate Representation (IR) that is defined under `leon.genc.ir`. Additionally, the C AST was partially redesigned. This new implementation is supposed to be better than the previous version in terms of bugs but there remain a few areas for improvement: * The `ClassLifter` is slightly incomplete: class fields should be processed as well. * When converting nested generic functions, the Scala2IRPhase might not do a proper job. Both of these points are explained in the source code; see the corresponding TODOs.
-
Make sure to use a new reporter for each test in GenCSuite
This avoids propagating failures from one test to the next.
-
-
-
-
-
-
Blind attempt to improve GenCSuite for Larabot
Hope is that shutting down fsc will prevent two concurrent build to mess with one another.
-
Explicitly reject ArrayUpdated constructs
ArrayUpdated, which represents Array.updated(index, newValue) and therefore builds a new array, should not be confused by ArrayUpdate, which updates a given array element in place.
-
-
-
-
Ensure GenC tests actually test something
Since the introduction of the new dependency finder, many functions/types were no longer examined by GenC.
-
-
Make GenC tests return a value in [0, 255] to avoid false positive
On most systems, the return value from a program is truncated to its least significant byte.
-
Add regression test for operator Equals
Note: this could get supported by generating the proper function definitions and replacing the operator by a function call.
-
-
-
-
Remove useless optimisation of id translation
This can also prevent some clashes with C std functions.
-
Update regression test about invalid pattern matching
Xlang now ensures no side effect so we remove this test from GenC.
-
Note: when using the private ctor of FIS/FOS, Leon will emit something like this: [info] [ Error ] Test.scala:93:16: Class leon.io.FileInputStream not defined? [info] val fis1 = FIS(Some("input.txt")) [info] ^^^ and therefore identifying the call to the constructor as faulty. -
-
-
-
- Use >>> in Scala to represent >> in C; - Cast signed integer to unsigned integer before shifting, and cast result back to signed integer afterward (see NOTE in code for rational)
-
-
Make GenCSuite robust against encoding issues
Now the outputs are compared at a byte level, not at a string level (which can be invalid).
-
Add support for more forms of Pattern Matching in GenC
Namely, LetTuple & LetPattern constructs
-
-
-
-
-
-
-
-
-
Add some aliasing regression tests that should get rejected
They are currently disabled because implementing a rejection phase for those is not as simple as it might seem. Similar cases can occur though pattern matching, for example.
-
Emit warnings on recursive functions
Let the user know this is not 100% MISRA compliant. With stack size analysis this issue could be solved.
-
Enable more C optimisation by making every function static
Except for the main function which should not be static
-
-
-
-
-
-
-
-
-
-
Use a different representation for Dictionary in LZW
This representation is less efficient in terms of speed of the produced code, but requires far less small arrays and therefore significantly improve the performance of GenC and C compilers to compile the code. Also, less properties are proven on this implementation.
-
-
-
-
Moving LZW implementations to a new testcases section
Because they are slow to generate, slow to compile and slow to execute, they cannot be part of the regression suite.
-
-
-
-
-
-
-
-
-
-
-
Add case study ImageProcessing for GenC
Use comments to select the kernel you want to use, then recompile.
