Print the types
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@425 041b043f-8d7c-46b2-b46e-ef0dd855326e
revert back to previous expression for path
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@424 041b043f-8d7c-46b2-b46e-ef0dd855326e
mapping horn values to lustre values in xml format
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@423 041b043f-8d7c-46b2-b46e-ef0dd855326e
sync horn backend
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@422 041b043f-8d7c-46b2-b46e-ef0dd855326e
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@421 041b043f-8d7c-46b2-b46e-ef0dd855326e
modifed / to div in horn backend
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@420 041b043f-8d7c-46b2-b46e-ef0dd855326e
fixing double printing of horn rules
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@419 041b043f-8d7c-46b2-b46e-ef0dd855326e
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
Reactivated the generation of traceability informationChanged the test-compile to use the horn-traces and the horn-queries option
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@414 041b043f-8d7c-46b2-b46e-ef0dd855326e
added invariants
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@412 041b043f-8d7c-46b2-b46e-ef0dd855326e
including invariants
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@411 041b043f-8d7c-46b2-b46e-ef0dd855326e
Fixed horn backend to make query for properties. More work needed for cex
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@410 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
Added an install target in the src folder
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@386 041b043f-8d7c-46b2-b46e-ef0dd855326e
modified optimization info printout (option -print_reuse)
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@385 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
added a new option -print_reuse that prints clock disjoint variables and reuse policy. useful for debugging and carrying correctness proofs to the C code level. non trivial result only when option -O 3 or above is activated.
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@383 041b043f-8d7c-46b2-b46e-ef0dd855326e
Moved Makefile into src folder
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@382 041b043f-8d7c-46b2-b46e-ef0dd855326e
Added a construct for Dependencies (was a tuple before) and a boolean attribute stateful
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@380 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
corrected a bug that made an error silent, confusing users...
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@370 041b043f-8d7c-46b2-b46e-ef0dd855326e
- corrected a bug in C code generation for multi-dimension arrays
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@340 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
- corrected bug in node reset clock - cleaner (but heavier !) code generation scheme for automata
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@337 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
- work in progress for automata...
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@333 041b043f-8d7c-46b2-b46e-ef0dd855326e
- more work towards automata
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@332 041b043f-8d7c-46b2-b46e-ef0dd855326e
- some steps towards integration of automata
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@331 041b043f-8d7c-46b2-b46e-ef0dd855326e
- some code cleaning - removed a potential source of bug in scheduler
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@330 041b043f-8d7c-46b2-b46e-ef0dd855326e
- corrected bugs with the inlining mode
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@329 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
- reimplementation of the reuse algorithm (option -O 3), much more simple and efficient.
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@320 041b043f-8d7c-46b2-b46e-ef0dd855326e
- still some improvements in optimizing in machine code ...
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@319 041b043f-8d7c-46b2-b46e-ef0dd855326e
- missing case in clock disjunction predicate, the absence of which produced weak (but still correct) optimization results.
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@318 041b043f-8d7c-46b2-b46e-ef0dd855326e
- corrected a small bug in clock calculus
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@317 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
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@311 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 in liveness analysis...
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@307 041b043f-8d7c-46b2-b46e-ef0dd855326e
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
Solved Bug in horn backend: when main node is stateless
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@287 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
Specialized the prefix/postfix modifiers through functors arguments
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/cleaner_backend@281 041b043f-8d7c-46b2-b46e-ef0dd855326e
Split all functions of C backends in separate files
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/cleaner_backend@280 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
Moved c_backend in separate folder
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/cleaner_backend@278 041b043f-8d7c-46b2-b46e-ef0dd855326e
Solved bug in optimization of machine code: output variable def should not be eliminated
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@277 041b043f-8d7c-46b2-b46e-ef0dd855326e
Solved local var name bugs for stateless nodes as outlined by Teme
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@276 041b043f-8d7c-46b2-b46e-ef0dd855326e
Mini bug solved: do not unfold array constants
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@273 041b043f-8d7c-46b2-b46e-ef0dd855326e
Missing files
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/simplifier@272 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
Extracted scheduling from machine code computation
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@270 041b043f-8d7c-46b2-b46e-ef0dd855326e
Create a Step call only for functions that are not in basic lib
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@269 041b043f-8d7c-46b2-b46e-ef0dd855326e
- bug correction (regression from previous versions !) introduced in C code generated from relational operators.
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@268 041b043f-8d7c-46b2-b46e-ef0dd855326e
- refactorization of typing code (simpler subtyping rules) - simplification of clock calculus (may be still buggy, work in progress) no impact on unclocked programs.
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@267 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
Updated typing error
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@260 041b043f-8d7c-46b2-b46e-ef0dd855326e
inlining update
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@259 041b043f-8d7c-46b2-b46e-ef0dd855326e
bug correction in homomorphic extension
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@257 041b043f-8d7c-46b2-b46e-ef0dd855326e
typo corrected in code generation for array memories (bad parentheses)
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@255 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
bug corrected for allocation of dynamic arrays in node memory
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@251 041b043f-8d7c-46b2-b46e-ef0dd855326e
node memory namespace bug corrected; library linear_ctl/arrays corrected
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@249 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
Additional checks in transpose
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@246 041b043f-8d7c-46b2-b46e-ef0dd855326e
Check node is stateful
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@245 041b043f-8d7c-46b2-b46e-ef0dd855326e
Bug solved on tuple equalities in expressions (eg. OK = (a,b,c) = (d,e,f))
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@244 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
still computing disjoint clock information (for reusing more variables)
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@240 041b043f-8d7c-46b2-b46e-ef0dd855326e
computing statically disjoint variables (to enhance resusability)
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@239 041b043f-8d7c-46b2-b46e-ef0dd855326e
removed debug message
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@230 041b043f-8d7c-46b2-b46e-ef0dd855326e
changed name generation to avoid conflict with C predefined symbols; added checking for declared but not defined node symbol
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@229 041b043f-8d7c-46b2-b46e-ef0dd855326e
- some minor adjustments...
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@228 041b043f-8d7c-46b2-b46e-ef0dd855326e
- corrected causality bug (cf. previous commit)
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@227 041b043f-8d7c-46b2-b46e-ef0dd855326e
liveness analysis improved. BUG found in causality wrt clocks...
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@224 041b043f-8d7c-46b2-b46e-ef0dd855326e
- modified example (arguments are now in the right order wrt clock declaration). - debugged liveness analysis...
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@217 041b043f-8d7c-46b2-b46e-ef0dd855326e
- reimplemented computation of dead variables - added computation of a reuse policy (depending on types) - not yet used though, would have to change code generation in order to be useful...
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@216 041b043f-8d7c-46b2-b46e-ef0dd855326e
added liveness analysis for reusing dead variables. Not yet used.
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@215 041b043f-8d7c-46b2-b46e-ef0dd855326e
improved code generation by factorizing out arrows
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@207 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......