CristalCaveGem » LustreC

clean handling of undefined node application

Updated typing error

inlining update

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.mli
M trunk/src/type_predef.ml
M trunk/src/main_lustre_compiler.ml
M trunk/src/types.ml
M trunk/src/printers.ml
M 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

desome

Merge inlining branch within trunk.
The test target requires branch lustrec/horn as binary lustreh.

inliner function

Minor bugs

Do not use stable sort because it requires recent ocamlgraph
library (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 printer
Generation of a witness with both the main node and hte inlined main node
Test 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

Ongoing ...

Ongoing ...

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.

- work in progress for interface typing

- small bug correction in dimension typing
- #open keyword instead of open
- dummy generic matrix/vector library interface added
- modified examples according to the new syntax

Merge (if it works) of the lustre interfaces branche providing lusi files into trunk

Moved files to trunk in lustre_compiler