Merge of last trunk commitsAdded fbyn(expr, n, init) to encodeinit -> pre (init -> pre (init -> ... pre expr))with n occurences of init
do not use lusi for horn, and some logging for horn
corrected a small bug when -horn option was active
some optimization in code optimization !!
some cosmetic changes in error messages when loading libraries
Major revision due to severe limitations and bugs of inlining capabilities: - destination dir should now work properly - lusic files now have a version number, to avoid nasty segfaults when loading lusic files created by an older compiler version - inlining should now work with generic nodes and generic array library...
LOTS of bug correction wrt inlining, still a work in progress... - global constants were not accounted for - no good avoidance of name capture when inlining - static parameters (array sizes and clocks) not handled - ill-typed generated expressions, when inlining array expressions
added some test files
correction of bugs: - a small problem in the parser - regarding the handling of destination directory, source directory, current directory, etc. It seems to be working now. A nice chasing after weird behaviors...
synch with svn
Fixed conflict with the svn trunk version
Added local inlining using the keyword (*! /inlining/:true *)
revert back to previous expression for path
mapping horn values to lustre values in xml format
Changed the option horntraces to a general traces optionThis annotation phases would have to be moved in optimization of normalized code
Solved bug found by Teme about asserts.
Previously assert expression containing -> would lead to unnormalized ite. Now each expression within the assert is normalized and may bind new node equations.This could be later optimized but is working now.
Revert the commit 384 by Xavier: adding dirname to the source_name introduced a bug: the .h file is empty!!! Strange behavior.
supports again relative path for lustre source file (regression bug)
- Dealt with compiling lusic from distant lusi files.- Header now do not allow the generation of function previously declared as C prototype
- changed the basic optimization scheme (option -O 2), which unfolds local variables and global variables that are either cheap to evaluate or used no more than once.
- corrected a bug in optimizating mode (option -O 3) - changed the printing of unused variables
- Added major feature: Lustre V6 automata !!! - one automata example added - changed the reset condition in node calls (now a simple bool expr) - bug corrected in clock calculus - bug corrected in traceability info - added field in variables to test whether they are original...
- code complete for automata - debugging in progress, not usable yet
- corrected bug with destination directory (-d option) - corrected several bugs in inlining - STILL, BUGS REMAINING in inlined code !!??!!
This is a major revision: - added interface files (.lusi) in the language, that can be compiled on their own, giving an object file (.lusic) and a header file (.h) - modular code generation, from Lustre to C level included. - nice amount of code refactoring
ooops, things got a bit scrambled with svn, restoring...
added some functions, prior to code refactoring
- started refactoring type definitions in .lus/.lusi, in order to ease the way .lusi interface files are handled.
- several bugs corrected when mixing tuples with clocks
- added missing constraint check when sub-clocking tuple expressions - added an algorithm that reuses dead or clock-disjoint variables instead of declaring/using new ones. - NOT carefully tested. Use option -O 3 if you want to give it a try...
Updated the licence info and header for each file.Moved backends in separate folders
- many bugs/limitations in lifting operators to tuples have been worked out: - typing/clock calculus/normalization now work properly - still, a bug in annot generation (this one is for Ploc !!) in file normalization, line 396 - bug corrected in subtyping...
work in progress (code optimization again)
Merged horn_traces branch
added some infrastructure to ease optimization (reusing vars)
Prepared first stage of code reorg:1. moved type def in lustrespec.ml2. moved constructor and basic functions in corelang3. Modified eexpr with prenext quantifiers
more steps toward reusing variables (dead ones + clock disjoint ones)
added construction of a fanin table for local variables of a node. could be useful for a finer variable elimination scheme at the Lustre level. to be continued...
added warnings for useless variables (at verbose level 1) - exact definition of 'useless' may be further refined - display could certainly be improved
Merged trunk updates
work in progress: - warnings for unused input/memory variables - optimization of machine code
Added the lustre backendStill some work on adapating the instruction scheduling
Restructured the main: call to optimization, scheduling performed out of machine_code, etcMerge Xavier last commitsUnfinished lustre backend
clean handling of undefined node application
Math lusi (trigo)
Solved bug:- loading lusi- loading lib in lusi files: "in m" is now "lib m"
Changed the load of lusi files: imported nodes or function can specify the linking lib and/or use a classical C prototype (without pointers).Parse updated as well as Makefile generation.
Added declaration/definition of stateless/stateful nodes. The 'function' keyword is for stateless nodes only, the 'node' keyword is any kind of node. Improves compilation and paves the way for more optimizations.
- work in progress for stateless/stateful status computation (to turn conditionals into merges, which yield more efficient C code)
corrected bugs in clock generalization that produced pessimistic C code (not wrong though); corrected bug with node importation policy wrt (re)declaration, (re)definition...
- added struct types declaration - added constant definition with a struct type - added checking for multiple definitions of nodes (behavior was buggy) - better and more uniform error messages for undefined/already defined symbols
We still need struct expressions...
more steps towards struct types...Cette ligne, et les suivantes ci-dessous, seront ignorées--
M trunk/src/corelang.mliM trunk/src/type_predef.mlM trunk/src/main_lustre_compiler.mlM trunk/src/types.mlM trunk/src/printers.mlM trunk/src/typing.ml...
corrected bug in arrow macros names, added storage attribute for static alloc macros, option -d now creates the destination directory if needed, with current dir as file permissions
- added generation of clock information in interface (.lusi) files- added clock checking between interface and implementation files
Reenabled the generation of witnesses for inline process.Systematic use of the build path
- merged test script - added -d support - corrected #open parser problem - corrected interface/implementation (.lusi/.lus) checking for types (not yet for clocks)
Merge trunk modif in branch
Solved some bugs in the lustre printerGeneration of a witness with both the main node and hte inlined main nodeTest script modified to check consistency of the inlining process
First fully working version of horn backend.
Has to be called with "-horn -node main_node"
The test script compute the smt2 file and calls z3 on them.
Is it working?
Initial copy of the horn output version. Not really working yet
Merge (if it works) of the lustre interfaces branche providing lusi files into trunk
Moved files to trunk in lustre_compiler