Topic/genc v2: ready for general review #290
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
mantognini
force-pushed
the
topic/genc_v2
branch
from
732d4c1
to
f317373
Compare
- 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)
Removed GenC in view of GenC v2
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.
This avoids propagating failures from one test to the next.
Hope is that shutting down fsc will prevent two concurrent build to mess with one another.
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.
Since the introduction of the new dependency finder, many functions/types were no longer examined by GenC.
On most systems, the return value from a program is truncated to its least significant byte.
Note: this could get supported by generating the proper function definitions and replacing the operator by a function call.
This can also prevent some clashes with C std functions.
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.
Let the user know this is not 100% MISRA compliant. With stack size analysis this issue could be solved.
Except for the main function which should not be static
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.
Because they are slow to generate, slow to compile and slow to execute, they cannot be part of the regression suite.
Use comments to select the kernel you want to use, then recompile.
mantognini
force-pushed
the
topic/genc_v2
branch
from
f317373
to
e27a4f7
Compare
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR brings a lot of improvements and new features to the GenC module. It also have minor impacts on the general codebase of Leon.
What is missing for merging?
What is in here? [Highlight]
TimedLeonPhasetrait that provided boilerplates for timers and the--debug=timersoption.RemoveVCPhasephase that removed invariants from the AST.enum),Bytearithmetic.main/_mainfunctions which allows VC to contain fragments of Scala not supported by GenC.testcases/genc/: Lempel–Ziv–Welch (LZW) universal lossless data compression algorithm.What's next (independent of this PR)?
Feedback welcomed.