Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src @ ba2f9fa1

# Date Author Comment
ba2f9fa1 04/08/2015 08:50 AM Pierre-Loïc Garoche

Prepare for tagging : Xia version 1.0

e9350b02 04/04/2015 03:59 PM Xavier Thirioux

corrected various bugs in the compilation/installation Makefile.in.

b3f91fdb 04/03/2015 06:22 PM Xavier Thirioux

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

7dd90f72 04/01/2015 06:41 PM Xavier Thirioux

added some test files

f4acee4c 04/01/2015 04:10 PM Xavier Thirioux

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

933ee7a3 03/24/2015 09:54 PM Teme Kahsai

synch with svn

eec8ce11 03/24/2015 09:54 PM Teme Kahsai

fixing double printing of horn rules

a5193ff5 03/24/2015 09:54 PM Teme Kahsai

Fixed conflict with the svn trunk version

6394042a 03/24/2015 07:26 PM Pierre-Loïc Garoche

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

9d01f989 03/17/2015 08:30 AM Pierre-Loïc Garoche

Print the types

c9570528 03/17/2015 08:24 AM Pierre-Loïc Garoche

revert back to previous expression for path

720f159a 03/16/2015 08:31 PM Teme Kahsai

mapping horn values to lustre values in xml format

96d33ff2 03/16/2015 08:31 PM Teme Kahsai

sync horn backend

97d3f81a 03/16/2015 08:31 PM Teme Kahsai

sync horn backend

58272238 03/16/2015 08:31 PM Teme Kahsai

modifed / to div in horn backend

24a55d0d 03/16/2015 08:30 PM Teme Kahsai

fixing double printing of horn rules

62f65f02 03/16/2015 08:30 PM Teme Kahsai

Fixed conflict with the svn trunk version

c065827c 03/06/2015 11:09 AM Pierre-Loïc Garoche

Changed the option horntraces to a general traces option
This annotation phases would have to be moved in optimization of normalized code

e9c64a30 03/05/2015 11:48 PM Pierre-Loïc Garoche

Reactivated the generation of traceability information
Changed the test-compile to use the horn-traces and the horn-queries option

f133f964 03/03/2015 09:10 PM Teme Kahsai

added invariants

ea94d58f 03/03/2015 09:10 PM Teme Kahsai

including invariants

3c862628 03/03/2015 09:10 PM Teme Kahsai

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

e42fb618 02/16/2015 11:52 PM Pierre-Loïc Garoche

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.

13fa31c2 12/10/2014 11:15 AM Pierre-Loïc Garoche

Revert the commit 384 by Xavier: adding dirname to the source_name introduced a bug: the .h file is empty!!! Strange behavior.

5d8ddbf7 12/10/2014 11:14 AM Pierre-Loïc Garoche

Added an install target in the src folder

86b99b69 12/09/2014 04:54 PM Xavier Thirioux

modified optimization info printout (option -print_reuse)

fb8b1da7 12/09/2014 04:30 PM Xavier Thirioux

supports again relative path for lustre source file (regression bug)

c825868a 12/09/2014 02:03 PM Xavier Thirioux

added a new option -print_reuse that prints clock disjoint variables and reuse policy.
useful for debugging and carrying correctness proofs to the C code level.
non trivial result only when option -O 3 or above is activated.

bed8ea64 12/09/2014 01:41 PM Pierre-Loïc Garoche

Moved Makefile into src folder

830de634 12/08/2014 09:09 PM Pierre-Loïc Garoche

Added a construct for Dependencies (was a tuple before) and a boolean attribute stateful

5ae8db15 12/01/2014 11:32 PM Pierre-Loïc Garoche

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

95763423 11/27/2014 03:30 PM Xavier Thirioux

corrected a bug that made an error silent, confusing users...

bc916448 09/29/2014 05:33 PM Xavier Thirioux

- corrected a bug in C code generation for multi-dimension arrays

307aba8d 09/26/2014 05:52 PM Xavier Thirioux

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

67896f6d 09/24/2014 12:13 PM Xavier Thirioux

- corrected a bug in optimizating mode (option -O 3)
- changed the printing of unused variables

d5fe9ac9 09/18/2014 05:25 PM Xavier Thirioux

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

6a1a01d2 09/14/2014 08:08 PM Xavier Thirioux

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

bc7b6c62 09/10/2014 06:01 PM Xavier Thirioux

- code complete for automata
- debugging in progress, not usable yet

1eda3e78 09/09/2014 06:03 PM Xavier Thirioux

- work in progress for automata...

77a01213 09/05/2014 03:06 PM Xavier Thirioux

- more work towards automata

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

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

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

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)

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

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

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

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

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

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.

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

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

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)