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.
- reimplementation of the reuse algorithm (option -O 3), much more simple and efficient.
- still some improvements in optimizing in machine code ...
- missing case in clock disjunction predicate, the absence of which produced weak (but still correct) optimization results.
- corrected a small bug in clock calculus
- 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
Fixed horn backend to make query for properties. More work needed for cex
- 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...
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
Solved Bug in horn backend: when main node is stateless
work in progress: - warnings for unused input/memory variables - optimization of machine code
Specialized the prefix/postfix modifiers through functors arguments
Split all functions of C backends in separate files
Added the lustre backendStill some work on adapating the instruction scheduling
Moved c_backend in separate folder
Solved bug in optimization of machine code: output variable def should not be eliminated
Solved local var name bugs for stateless nodes as outlined by Teme
Mini bug solved: do not unfold array constants
Restructured the main: call to optimization, scheduling performed out of machine_code, etcMerge Xavier last commitsUnfinished lustre backend
Extracted scheduling from machine code computation
Create a Step call only for functions that are not in basic lib
- bug correction (regression from previous versions !) introduced in C code generated from relational operators.
- refactorization of typing code (simpler subtyping rules) - simplification of clock calculus (may be still buggy, work in progress) no impact on unclocked programs.
clean handling of undefined node application
Updated typing error
bug correction in homomorphic extension
typo corrected in code generation for array memories (bad parentheses)
Math lusi (trigo)
bug corrected for allocation of dynamic arrays in node memory
node memory namespace bug corrected; library linear_ctl/arrays corrected
Solved bug:- loading lusi- loading lib in lusi files: "in m" is now "lib m"
Additional checks in transpose
Check node is stateful
Bug solved on tuple equalities in expressions (eg. OK = (a,b,c) = (d,e,f))
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.
still computing disjoint clock information (for reusing more variables)
computing statically disjoint variables (to enhance resusability)
removed debug message
changed name generation to avoid conflict with C predefined symbols; added checking for declared but not defined node symbol
- some minor adjustments...
- corrected causality bug (cf. previous commit)
liveness analysis improved. BUG found in causality wrt clocks...
- modified example (arguments are now in the right order wrt clock declaration). - debugged liveness analysis...
- 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...
added liveness analysis for reusing dead variables. Not yet used.
improved code generation by factorizing out arrows
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...
work in progress for struct types...
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...
first steps towards struct types...
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
answer to #feature 50: - arrows are now factorized out and become part of include as files arrow.h and arrow.c - no more arrows in generated code - compiling and linking arrow.c is only necessary in case of dynamic allocation - version now includes installation prefix (for the standard lib)...
In order to export any type of constants, moved type definitions from .c to .h
Generate extern declarations for constant as well.
- 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 back horn backend branch in trunk
Merge trunk modif in branch
Merge inlining branch within trunk.The test target requires branch lustrec/horn as binary lustreh.
Do not use stable sort because it requires recent ocamlgraphlibrary (1.8.3) which is not widely available in distro repository.Moreover "stable" sort is not necessary, sort will do.Fixes Issue #49: https://cavale.enseeiht.fr/redmine/issues/49
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
better error message for tuple type mismatch
again, debugged tuple subtyping
removed debug printing
corrected wrong subtyping rule for tuple assignment
added subtyping in equations (rhs may be a subtype of lhs)
Improvements as suggested by e. Noulard: better install of include; modified generated makefile
Fixed bug on the main part
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?
Working on bugs
Second (almost) working version
First (almost) working version
In the middle of the coding process. Just pushing thinks
The missing file
Initial copy of the horn output version. Not really working yet
- Renamed the only target of the generated makefile- Solved bug: xor are now printed as bitwise xor in c : a ^ b and not a xor b.