CristalCaveGem » LustreC

- Primitive Tiny backend
- Renamed Mpfr to lustrec_mpfr
- Introduced dependency in Zarith. Trying to move away from Num

printing nodes + more progress on seal export

- Refactored Error exception and messages
- Bugs in partial evaluation for equalities among bool constants
and a nice recursive call generating a stack overflow! Now solved
- Setup a timeout for z3 in seal
- Better log for seal

better location error

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

Merge branch 'salsa' into lustrec-seal

Reformating plugin signatures. Better report management

Unified compilation of lusi and lus files
Different parsers yet but shared process.
In case of lusi input the C backend is bypassed since the .h is generated from the lusic and no C code should be generated since it may overwrite existing manually written code...

- Dep type with a tuple has been replaced by a record type
- Modules now is more integrated and performed the building of the type/clock env.
previously some computation were performed twice by different functions. Some of these functions have been moved from compiler_common to modules

- Module.load_header and load_program were merged.
- Contract were extended with list of statements.

Merge branch 'unstable' into lustrec-seal

Merge branch 'cocospec_to_be_merged' into unstable
Mainly adapting to new cocospec syntax for contracts

Merge branch 'unstable' into lustrec-seal

- Global type env and clock env now availble as a global reference (Global module)
- Adapted the parsing of specification with a cocospec compatible one
- The data structure of contracts is now almost cocospec compatible
- Lustrec-test has been updated to use the newest syntax

Temporily disabling Mehnir as a parser.

Merge branch 'unstable' into lustrec-seal

Tuning the pretty printing of Salsa plugin

Merge branch 'unstable' into lustrec-seal

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

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

- Normalization parameters (alias and unfold_array) are now provided as parameter
- program type renamed as program_t
- Initiating the lustrev tool with dependencies to z3 and seal.

[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

No existing input file returns a 1 error code

Moved stage1 in separate file: it is shared among binaries

Missing last fprintf @. in the lustre output

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

Refactor error printing.

Refactored some code: optimization of machine

Added a feature to alias ite contructs argument. To be used by EMF backend

- 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

Providing means to have specification as dynamic checks.
[bug] seems to crash with EMF backend

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

Merge branch 'unstable' into seahorn_a6df3
a6df3 is the initial commit of branch seahorn

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

trying to improving pretty printing. Not so perfect for the moment

Merge branch 'testgen' into merging_unstable_testgen

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

functional_backend function moved to corelang

first version (doesn't even compile) of mutation and test generation standalone command: lustret
mostly a recovery of an ancient svn repo: mutations

Working on EMF backend to express cocospec infos as Simulink blocks

slight improvement of causality error messages

moving C files name declaration in backend. Preparation for additional cmake target

...

full merge of salsa/mpfr and master

Bug solved in automaton part

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

regression bugs corrected

Plugin based framework

major branche merging salsa/mpfr with trunk

bug correction in typing: tuple types were computed but not recorded

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

bug correction in typing: tuple types were computed but not recorded

Refactoring of the horn backend with Reset/Step instead of Init/Step.
Teme, please perform a string non regression test wrt the previous version, to make sure we have the same model checking results.

numerous bugs corrected:
- bug in expansion of array accesses with constant arrays
- bug in printing complex array indexes (not C compliant)
- bug wrt C99 typing policy for constant arrays
- bug in signaling wrong useless static input

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

numerous bugs corrected:
- bug in expansion of array accesses with constant arrays
- bug in printing complex array indexes (not C compliant)
- bug wrt C99 typing policy for constant arrays
- bug in signaling wrong useless static input

Merge of last trunk commits
Added fbyn(expr, n, init) to encode
init -> pre (init -> pre (init -> ... pre expr))
with n occurences of init

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

Merge of last trunk commits
Added fbyn(expr, n, init) to encode
init -> pre (init -> pre (init -> ... pre expr))
with n occurences of init

do not use lusi for horn, and some logging for horn

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

do not use lusi for horn, and some logging for horn

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

some optimization in code optimization !!

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

some optimization in code optimization !!

some cosmetic changes in error messages when loading libraries

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

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

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

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

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

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

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

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

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

synch with svn

Fixed conflict with the svn trunk version

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

Fixed conflict with the svn trunk version

Added local inlining using the keyword (*! /inlining/:true *)

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

Added local inlining using the keyword (*! /inlining/:true *)

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

revert back to previous expression for path

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

mapping horn values to lustre values in xml format

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

Fixed conflict with the svn trunk version

Changed the option horntraces to a general traces option
This 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

Changed the option horntraces to a general traces option
This 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.

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.

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

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)

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

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

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

- 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

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