CristalCaveGem » LustreC

work on spec generation almost done

start again with spec representation

start with Spec AST generation

corrections on loggers + spec in AST

minor rewriting

fix almost all warnings

migration draft on dune

Array access: solved issues in C backend when basic operations in array access dimensions. Also better handling in EMF, ie further normalization through new equations

- tag_true and tag_false moved to lustre_types
- real constants are hidden in Real.ml{i} module

scheduling now report unused vars and remove their definition instead of stopping processing.

Cocospec: parsing, normalizing and processing machines for contracts.

Merge branch 'salsa' into lustrec-seal

Serious refactoring of scopes plug-in:
- now properly records the scopes
- only register requested ones

Some progress on compiling cocospec contract.
Contract resolution still need to be done as well as dealing with the machine code level and so on.

Major refreshing of machine generation

Some progress on EMF bqckend. Refactoring machines code

Merge branch 'unstable' into lustrec-seal

Pretty serious update:
- a bug in regressio ntest Simulink/integrator_ext_IC_matrix_test revealed the following (serious issue):
when building the list of instruction (in the machine code) the access to variable were hardcoded to LocalVar or StateVAr depending whether the variables was part of the identified memories....

Moved find_eq from Machine_code to Corelang and sort_eqs from Machine_code to Scheduling

Scheduling of node equations is now attached to machine type

Further restructuring:
- arrow.ml* to define basic builder for arrow (node, name, ...)
- machine_code_common similar to corelang but for machine_code (printers, some builders, ...)
- machine_code restricted to the translatation from normalized nodes to machines

MLI for normalization and machine_code.
Structs defining machines are now in machine_code_types

- Makefile: solved dependency problem when compiling include lusi
- Renamed type declarations as lustre_types and machine_code_types

[general] large modification: added machine types, a second typing phase dealing with machine types (eg uint8)
typing was transformed as a functor and parametrized by basic types (int/real/bool)
it can also be applied multiple times on the same program

[general] Refactor get_node_eqs to produce (eqs, auts) with automatons

First working version of algebraic loop resolution. Disabled by default.

Refactored some code: optimization of machine

Refactored EMF backend. Handle now the call to existing math and conv libraries

Renamed ISet of Machine_code to VSet: was sets of variable and was conflicting with ISet from Utils which carries strings.

Improved EMF backend. Working on the whole fmcad suite

Solved bug in machine code generation for asserts that contain memories

Cleaned horrible ocaml practice (optional parameters and mli issues)

- Added a field lustre_eq to machine instruction in order to record the originating lustre equation
- EMF backend now impose the optimization level to be set to 0 in order to avoid equation elimination that would render traceability difficult
- Options.ml has been split into Options.ml / Options_management.ml. Options.ml only contains references and no functions

- Addtional encapsulation of machine_code instr in a struct to enable future extension of type with more metadata.
- Improved EMF backend with META information

EMF backend now relies on machine code representation.
Impact:
- EMF backend has an extra machines argument
- specific option to avoid merge of ite constructs
- set_backend function to improve backend selection

Most code was extracted from seahorn_backend through c0f8

Improved include folders behaviors:
- allow multiple -I dir, will be used in order (first one declared
is first used)

- when declaring a global library #open <foo>, foo is first checked
in local folders, than in global one (install path). This
does not apply to local libraries opened with #open "foo".

[bug solved] issues with asserts (invalid eqs scheduling)

Removing silly warning message

Merge branch 'unstable' into merging_plugins
Non regression results were similar to master branch

Solved a bug in the compilation of asserts. Now different behavior depending on the backend:
functional: keep it as is
non func: introduce a fresh local var v and replace assert(e) by v=e; assert (v);

Merge branch 'github_master' into integ_github_jan10
Intregrate all modifs by Teme et al

adding -I options to lustrec

updating to onera version 30f766a:2016-12-04

...

full merge of salsa/mpfr and master

Updated to onera_git commit version 9421e24

Resolved conflict when merging salsa with horn_encoding. The current branch is the most updated.

Merge branch 'salsa' into merge_salsa_horn_2
Postponed conflicts to be solved
Conflicts:
src/_tags
src/backends/Horn/horn_backend.ml
src/machine_code.ml
src/main_lustre_compiler.ml
src/myocamlbuild.ml.in
src/optimize_machine.ml

Introduced the opposite of Reset call: NoReset. This simplify the general compilation process and makes the code more symmetric, hence simpler and clearer code.

Merge branch 'master' into horn_enum_types

Conflicts:
src/backends/Horn/horn_backend.ml

major branche merging salsa/mpfr with trunk

bug corrected: in some cases, local const vars were assigned twice

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@483 041b043f-8d7c-46b2-b46e-ef0dd855326e

bug corrected: in some cases, local const vars were assigned twice

Two fresh branches :)
to manage enum and arrays in the horn backend.

first commit

corrected a small bug when -horn option was active

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@450 041b043f-8d7c-46b2-b46e-ef0dd855326e

corrected a small bug when -horn option was active

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...

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...

modifed / to div in horn backend

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@420 041b043f-8d7c-46b2-b46e-ef0dd855326e

modifed / to div in horn backend

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

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.

- 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

- Dealt with compiling lusic from distant lusi files.
- Header now do not allow the generation of function previously declared as C prototype

- 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

- corrected bug in node reset clock
- cleaner (but heavier !) code generation scheme for automata

- 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...

- 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...

- work in progress for automata...

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@333 041b043f-8d7c-46b2-b46e-ef0dd855326e

- work in progress for automata...

- 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 bugs with the inlining mode

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...

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

- 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...

- 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

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...

- 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

work in progress (code optimization again)

Merged horn_traces branch

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@303 041b043f-8d7c-46b2-b46e-ef0dd855326e

Merged horn_traces branch

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

added some infrastructure to ease optimization (reusing vars)

Prepared first stage of code reorg:
1. moved type def in lustrespec.ml
2. moved constructor and basic functions in corelang
3. 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

Prepared first stage of code reorg:
1. moved type def in lustrespec.ml
2. moved constructor and basic functions in corelang
3. Modified eexpr with prenext quantifiers

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

added warnings for useless variables (at verbose level 1)
- exact definition of 'useless' may be further refined
- display could certainly be improved

Extracted scheduling from machine code computation

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@270 041b043f-8d7c-46b2-b46e-ef0dd855326e

Extracted scheduling from machine code computation

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

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.

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@268 041b043f-8d7c-46b2-b46e-ef0dd855326e

- 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.

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@267 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.

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