Fixed conflict with the svn trunk version
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@417 041b043f-8d7c-46b2-b46e-ef0dd855326e
Changed the option horntraces to a general traces optionThis annotation phases would have to be moved in optimization of normalized code
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@415 041b043f-8d7c-46b2-b46e-ef0dd855326e
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.
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@406 041b043f-8d7c-46b2-b46e-ef0dd855326e
Revert the commit 384 by Xavier: adding dirname to the source_name introduced a bug: the .h file is empty!!! Strange behavior.
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@387 041b043f-8d7c-46b2-b46e-ef0dd855326e
supports again relative path for lustre source file (regression bug)
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@384 041b043f-8d7c-46b2-b46e-ef0dd855326e
- Dealt with compiling lusic from distant lusi files.- Header now do not allow the generation of function previously declared as C prototype
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@375 041b043f-8d7c-46b2-b46e-ef0dd855326e
- 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.
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@339 041b043f-8d7c-46b2-b46e-ef0dd855326e
- corrected a bug in optimizating mode (option -O 3) - changed the printing of unused variables
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@338 041b043f-8d7c-46b2-b46e-ef0dd855326e
- 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
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@334 041b043f-8d7c-46b2-b46e-ef0dd855326e
- corrected bug with destination directory (-d option) - corrected several bugs in inlining - STILL, BUGS REMAINING in inlined code !!??!!
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@328 041b043f-8d7c-46b2-b46e-ef0dd855326e
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...
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@323 041b043f-8d7c-46b2-b46e-ef0dd855326e
added some functions, prior to code refactoring
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@322 041b043f-8d7c-46b2-b46e-ef0dd855326e
- started refactoring type definitions in .lus/.lusi, in order to ease the way .lusi interface files are handled.
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@321 041b043f-8d7c-46b2-b46e-ef0dd855326e
- several bugs corrected when mixing tuples with clocks
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@316 041b043f-8d7c-46b2-b46e-ef0dd855326e
- 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
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@313 041b043f-8d7c-46b2-b46e-ef0dd855326e
- 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)
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@306 041b043f-8d7c-46b2-b46e-ef0dd855326e
Merged horn_traces branch
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@303 041b043f-8d7c-46b2-b46e-ef0dd855326e
added some infrastructure to ease optimization (reusing vars)
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@302 041b043f-8d7c-46b2-b46e-ef0dd855326e
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
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/specification_reorg_corelang_parser@297 041b043f-8d7c-46b2-b46e-ef0dd855326e
more steps toward reusing variables (dead ones + clock disjoint ones)
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@295 041b043f-8d7c-46b2-b46e-ef0dd855326e
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...
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@291 041b043f-8d7c-46b2-b46e-ef0dd855326e
added warnings for useless variables (at verbose level 1) - exact definition of 'useless' may be further refined - display could certainly be improved
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@290 041b043f-8d7c-46b2-b46e-ef0dd855326e
Merged trunk updates
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/specification_acsl_new_backend@288 041b043f-8d7c-46b2-b46e-ef0dd855326e
work in progress: - warnings for unused input/memory variables - optimization of machine code
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@286 041b043f-8d7c-46b2-b46e-ef0dd855326e
Added the lustre backendStill some work on adapating the instruction scheduling
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/cleaner_backend@279 041b043f-8d7c-46b2-b46e-ef0dd855326e
Restructured the main: call to optimization, scheduling performed out of machine_code, etcMerge Xavier last commitsUnfinished lustre backend
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/simplifier@271 041b043f-8d7c-46b2-b46e-ef0dd855326e
clean handling of undefined node application
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@261 041b043f-8d7c-46b2-b46e-ef0dd855326e
Math lusi (trigo)
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@253 041b043f-8d7c-46b2-b46e-ef0dd855326e
Solved bug:- loading lusi- loading lib in lusi files: "in m" is now "lib m"
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@247 041b043f-8d7c-46b2-b46e-ef0dd855326e
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.
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@242 041b043f-8d7c-46b2-b46e-ef0dd855326e
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.
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@202 041b043f-8d7c-46b2-b46e-ef0dd855326e
- work in progress for stateless/stateful status computation (to turn conditionals into merges, which yield more efficient C code)
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@198 041b043f-8d7c-46b2-b46e-ef0dd855326e
corrected bugs in clock generalization that produced pessimistic C code (not wrong though); corrected bug with node importation policy wrt (re)declaration, (re)definition...
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@194 041b043f-8d7c-46b2-b46e-ef0dd855326e
- 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
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@181 041b043f-8d7c-46b2-b46e-ef0dd855326e
- added generation of clock information in interface (.lusi) files- added clock checking between interface and implementation files
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@176 041b043f-8d7c-46b2-b46e-ef0dd855326e
Reenabled the generation of witnesses for inline process.Systematic use of the build path
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@175 041b043f-8d7c-46b2-b46e-ef0dd855326e
- merged test script - added -d support - corrected #open parser problem - corrected interface/implementation (.lusi/.lus) checking for types (not yet for clocks)
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@171 041b043f-8d7c-46b2-b46e-ef0dd855326e
Merge trunk modif in branch
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/horn_encoding@168 041b043f-8d7c-46b2-b46e-ef0dd855326e
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
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/inlining@162 041b043f-8d7c-46b2-b46e-ef0dd855326e
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.
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/horn_encoding@152 041b043f-8d7c-46b2-b46e-ef0dd855326e
Is it working?
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/horn_encoding@150 041b043f-8d7c-46b2-b46e-ef0dd855326e
Initial copy of the horn output version. Not really working yet
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/horn_encoding@141 041b043f-8d7c-46b2-b46e-ef0dd855326e
Merge (if it works) of the lustre interfaces branche providing lusi files into trunk
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@123 041b043f-8d7c-46b2-b46e-ef0dd855326e
Moved files to trunk in lustre_compiler
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@116 041b043f-8d7c-46b2-b46e-ef0dd855326e