| Branch: | Tag: | Revision:

lustrec @ 29ced7be

# Date Author Comment
29ced7be 09/04/2014 04:20 PM Xavier Thirioux

- some steps towards integration of automata

2ac56807 09/03/2014 08:47 PM Xavier Thirioux

- some code cleaning
- removed a potential source of bug in scheduler

cfdb4fe9 09/03/2014 04:02 PM Xavier Thirioux

- corrected bugs with the inlining mode

3f823d04 09/02/2014 05:46 PM Xavier Thirioux

- corrected bug with destination directory (-d option)
- corrected several bugs in inlining
- STILL, BUGS REMAINING in inlined code !!??!!

70e1006b 09/02/2014 02:43 PM Xavier Thirioux

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

ed431cc2 07/15/2014 03:01 PM Xavier Thirioux

ooops, things got a bit scrambled with svn, restoring...

7dedc5f0 07/15/2014 02:15 PM Xavier Thirioux

added some functions, prior to code refactoring

6aeb3388 07/15/2014 09:27 AM Xavier Thirioux

- started refactoring type definitions in .lus/.lusi,
in order to ease the way .lusi interface files are handled.

084c1ce4 07/12/2014 02:23 PM Xavier Thirioux

- reimplementation of the reuse algorithm (option -O 3),
much more simple and efficient.

8fa083d5 07/11/2014 04:29 PM Xavier Thirioux

- still some improvements in optimizing in machine code ...

8ac7a0c7 07/11/2014 02:57 PM Xavier Thirioux

- missing case in clock disjunction predicate, the absence of which produced
weak (but still correct) optimization results.

32f508aa 07/10/2014 11:19 PM Xavier Thirioux

- corrected a small bug in clock calculus

d52e7821 07/10/2014 05:19 PM Xavier Thirioux

- several bugs corrected when mixing tuples with clocks

01f1a1f4 07/10/2014 12:49 PM Xavier Thirioux

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

b38ffff3 07/09/2014 09:57 AM Pierre-Loïc Garoche

Updated the licence info and header for each file.
Moved backends in separate folders

817d5bcb 07/09/2014 12:35 AM Teme Kahsai

Fixed horn backend to make query for properties. More work needed for cex

fcf1fd96 07/09/2014 12:35 AM Teme Kahsai

Fixed horn backend to make query for properties. More work needed for cex

15787c5b 07/08/2014 06:17 PM Teme Kahsai

added git version of svn_version

2cf39a8e 07/08/2014 04:53 PM Xavier Thirioux

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

34a5a072 07/07/2014 10:35 AM Xavier Thirioux

work in progress in liveness analysis...

7cd31331 07/04/2014 04:57 PM Xavier Thirioux

work in progress (code optimization again)

36454535 07/03/2014 10:46 PM Pierre-Loïc Garoche

Merged horn_traces branch

1837ce98 07/03/2014 10:40 PM Xavier Thirioux

added some infrastructure to ease optimization (reusing vars)

920c31de 07/02/2014 05:32 PM Pierre-Loïc Garoche

Merged branches specification_reorg_corelang_parser (see last commit message, moved definitions/functions btw files and changed eexpr type)

0038002e 07/02/2014 05:29 PM Pierre-Loïc Garoche

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

7ecdb0aa 07/02/2014 04:14 PM Xavier Thirioux

more steps toward reusing variables (dead ones + clock disjoint ones)

d96d54ac 06/27/2014 04:29 PM Xavier Thirioux

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

9aaee7f9 06/26/2014 04:48 PM Xavier Thirioux

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

54adb917 06/25/2014 05:38 PM Pierre-Loïc Garoche

Merged with new specification backend: only eacsl makefile for the now on

e95470b3 06/25/2014 05:37 PM Pierre-Loïc Garoche

Merged trunk updates

587cdc0d 06/25/2014 05:00 PM Pierre-Loïc Garoche

Solved Bug in horn backend: when main node is stateless

c1b14ce6 06/25/2014 02:33 PM Xavier Thirioux

work in progress:
- warnings for unused input/memory variables
- optimization of machine code

cee0feb8 06/25/2014 01:11 PM Pierre-Loïc Garoche

New branch to copy the specgeneration using the new backend functors

56484623 06/25/2014 01:06 PM Pierre-Loïc Garoche

Merged the new backend split into trunk

713176a4 06/25/2014 12:47 PM Pierre-Loïc Garoche

Specialized the prefix/postfix modifiers through functors arguments

522938b5 06/25/2014 11:13 AM Pierre-Loïc Garoche

Split all functions of C backends in separate files

49ddf66d 06/25/2014 10:54 AM Pierre-Loïc Garoche

Added the lustre backend
Still some work on adapating the instruction scheduling

d2be420e 06/25/2014 10:15 AM Pierre-Loïc Garoche

Moved c_backend in separate folder

a77bd1e3 06/25/2014 08:20 AM Pierre-Loïc Garoche

Solved bug in optimization of machine code: output variable def should not be eliminated

7130028e 06/25/2014 07:45 AM Pierre-Loïc Garoche

Solved local var name bugs for stateless nodes as outlined by Teme

6e73c87e 06/24/2014 09:53 PM Pierre-Loïc Garoche

Added branch to separate code gen/file creation/spec/proof

7a6b5deb 06/24/2014 04:30 PM Pierre-Loïc Garoche

Mini bug solved: do not unfold array constants

3ab9437b 06/24/2014 03:57 PM Pierre-Loïc Garoche

Missing files

59294251 06/24/2014 03:57 PM Pierre-Loïc Garoche

Restructured the main: call to optimization, scheduling performed out of machine_code, etc
Merge Xavier last commits
Unfinished lustre backend

db1c5c00 06/24/2014 03:16 PM Pierre-Loïc Garoche

Extracted scheduling from machine code computation

1ad092fb 06/24/2014 01:54 PM Pierre-Loïc Garoche

Create a Step call only for functions that are not in basic lib

fa0db9d5 06/23/2014 09:56 AM Xavier Thirioux

- bug correction (regression from previous versions !) introduced
in C code generated from relational operators.

6b4d172f 06/20/2014 04:59 PM Xavier Thirioux

- refactorization of typing code (simpler subtyping rules)
- simplification of clock calculus (may be still buggy, work in progress)
no impact on unclocked programs.

839ca600 06/17/2014 11:56 PM Pierre-Loïc Garoche

Update on the test script

f6fa97f9 06/12/2014 05:53 PM Xavier Thirioux

clean handling of undefined node application

5b5625e1 06/12/2014 02:08 PM Pierre-Loïc Garoche

Updated typing error

9f8c4c1d 05/23/2014 02:51 PM Pierre-Loïc Garoche

inlining update

f044d0b0 05/23/2014 09:36 AM Pierre-Loïc Garoche

Convertion operators

14d694c7 05/22/2014 10:29 AM Xavier Thirioux

bug correction in homomorphic extension

1174cdd9 05/20/2014 02:12 PM Xavier Thirioux

typo corrected in code generation for array memories (bad parentheses)

90028770 05/20/2014 01:47 PM Pierre-Loïc Garoche

Math lusi (trigo)

075fd56f 05/19/2014 03:51 PM Xavier Thirioux

bug corrected for allocation of dynamic arrays in node memory

7ac15bcf 05/19/2014 02:38 PM Xavier Thirioux

node memory namespace bug corrected; library linear_ctl/arrays corrected

4437ddbc 05/19/2014 01:57 PM Pierre-Loïc Garoche

Updated list with new tests

45c0d258 05/19/2014 01:46 PM Pierre-Loïc Garoche

Solved bug:
- loading lusi
- loading lib in lusi files: "in m" is now "lib m"

7a1ec3fa 05/19/2014 01:45 PM Pierre-Loïc Garoche

Additional checks in transpose

316af809 05/19/2014 01:45 PM Pierre-Loïc Garoche

Check node is stateful

d9d34564 05/19/2014 01:44 PM Pierre-Loïc Garoche

Bug solved on tuple equalities in expressions (eg. OK = (a,b,c) = (d,e,f))

c00d0b42 05/16/2014 05:26 PM Pierre-Loïc Garoche

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.

97498b53 04/01/2014 06:03 PM Xavier Thirioux

still computing disjoint clock information (for reusing more variables)

7a737ed5 03/31/2014 04:29 PM Xavier Thirioux

computing statically disjoint variables (to enhance resusability)

66e38617 03/24/2014 02:37 PM Xavier Thirioux

removed debug message

0b78e972 03/24/2014 02:36 PM Xavier Thirioux

changed name generation to avoid conflict with C predefined symbols; added checking for declared but not defined node symbol

a1f57a52 03/24/2014 09:22 AM Xavier Thirioux

- some minor adjustments...

84d9893e 03/24/2014 09:05 AM Xavier Thirioux

- corrected causality bug (cf. previous commit)

e8c0f452 03/20/2014 03:41 PM Xavier Thirioux

liveness analysis improved. BUG found in causality wrt clocks...

3c48346d 03/19/2014 11:00 PM Xavier Thirioux

- modified example (arguments are now in the right order wrt clock declaration).
- debugged liveness analysis...

d4101ea0 03/19/2014 06:08 PM Xavier Thirioux

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

6cf31814 03/18/2014 06:05 PM Xavier Thirioux

added liveness analysis for reusing dead variables. Not yet used.

14ebde97 03/17/2014 01:01 PM Xavier Thirioux

improved code generation by factorizing out arrows

8a5f633d 03/17/2014 12:46 PM Pierre-Loïc Garoche

Version compatible avec le francais

1699b8ff 03/17/2014 09:06 AM Pierre-Loïc Garoche

Updated test script: changed path and verbose mode

67ba882b 03/17/2014 07:44 AM Pierre-Loïc Garoche

Moved tests outside of source code to avoid useless duplication.

cbe93c65 03/17/2014 07:40 AM Pierre-Loïc Garoche

Added Alice Tailliar example

5538b7ac 03/17/2014 12:17 AM Xavier Thirioux

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.

d3e4c22f 03/14/2014 05:45 PM Xavier Thirioux

- work in progress for stateless/stateful status computation
(to turn conditionals into merges, which yield more efficient C code)

2ea1e4a6 03/13/2014 05:30 PM Xavier Thirioux

corrected bugs in clock generalization that produced pessimistic C code (not wrong though); corrected bug with node importation policy wrt (re)declaration, (re)definition...

6affc9f5 03/11/2014 03:41 PM Xavier Thirioux

- 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...
51768260 03/10/2014 05:56 PM Xavier Thirioux

work in progress for struct types...

aa223e69 03/10/2014 09:55 AM Xavier Thirioux

more steps towards struct types...
Cette ligne, et les suivantes ci-dessous, seront ignorées--

M trunk/src/corelang.mli
M trunk/src/
M trunk/src/
M trunk/src/
M trunk/src/
M trunk/src/

6560bb94 03/06/2014 04:33 PM Xavier Thirioux

first steps towards struct types...

9bdfc99f 03/06/2014 03:39 PM Xavier Thirioux

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

c6acbdaa 03/05/2014 04:32 PM Xavier Thirioux

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

6bab3787 03/05/2014 02:35 PM Xavier Thirioux

In order to export any type of constants, moved type definitions from .c to .h

b3202935 03/04/2014 02:41 PM Eric Noulard

Generate extern declarations for constant as well.

3e79b3a5 03/01/2014 03:38 PM Xavier Thirioux

- stupid svn had removed a file, again

c518d082 03/01/2014 03:37 PM Xavier Thirioux

- added generation of clock information in interface (.lusi) files
- added clock checking between interface and implementation files

2842f7ca 03/01/2014 12:01 AM Pierre-Loïc Garoche

Reenabled the generation of witnesses for inline process.
Systematic use of the build path

626e6f03 02/28/2014 11:59 PM Pierre-Loïc Garoche

Updated script. Does not seem to be fully functional yet.

3e36d4e0 02/28/2014 11:59 PM Pierre-Loïc Garoche

Added default ensures statements

7f611a35 02/28/2014 05:09 PM Xavier Thirioux

- added dummy_lib.lusi (accidentally removed !?)

8b3afe43 02/28/2014 04:56 PM Xavier Thirioux

- merged test script
- added -d support
- corrected #open parser problem
- corrected interface/implementation (.lusi/.lus) checking
for types (not yet for clocks)

29ad4531 02/28/2014 03:28 PM Pierre-Loïc Garoche

Merge back horn backend branch in trunk

64aa99c4 02/28/2014 02:05 PM Pierre-Loïc Garoche

Merge trunk modif in branch

addb1a3a 02/28/2014 02:04 PM Pierre-Loïc Garoche