Commit graph

940 commits

Author SHA1 Message Date
Gwenaël Delaval
e0d1900f3a Version 1.05.00
- Option -simple-scheduler active for scheduling post-ctrln code generation
 - Handle implication operator in Sigali backend
 - Compatibility with reatk >= 0.14
2018-06-19 22:07:03 +02:00
Gwenaël Delaval
b51c292231 Allow use of simple scheduler after control synthesis code generation
The -simple-scheduler option now imply the use of simple scheduler
both before and after control synthesis code generation.
2018-06-07 11:57:51 +02:00
Nicolas Berthier
7abe92dc0d Adapt to new interface of reatk.ctrlNbac (≥ 0.14) 2018-06-06 14:45:50 +01:00
Nicolas Berthier
8872bb3998 Do not remove sub-directories in `Compiler_utils.clean_dir' 2018-03-02 14:27:15 +00:00
Nicolas Berthier
95bb1a72ad Handle implication operator in Sigali backend 2018-03-02 14:26:10 +00:00
Gwenaël Delaval
95c9eb699b Version 1.04.00 2017-09-29 14:58:37 +02:00
Timothy Bourke
63289fe9f6 Allow semicolons after tel's 2017-09-29 00:08:42 +02:00
Timothy Bourke
0747494c7a Fix line counting. Ignore kind2 property comments 2017-09-29 00:08:42 +02:00
Timothy Bourke
abfc038b6b Accept single line "--" comments 2017-09-29 00:08:42 +02:00
Timothy Bourke
2d9fb52bec Fix a mistake in new when patterns 2017-09-29 00:08:42 +02:00
Timothy Bourke
4dadf6b4d6 Enforce well-formedness of clocks
For a clock (ck on x) to be well-formed in an environment H, we must
have H x = ck, i.e., the clock of x is the same as the clock ck of the
stream being sampled.

This constraint is guaranteed by construction for fully inferred clocks
(by the rules for when and merge), but nothing guarantees that user
declarations be well-formed. This can lead to problems.

For instance, this invalid program is incorrectly accepted:

    node f (x : bool; a : bool :: . on b;
		      b : bool :: . on a) returns (y:bool);
    let
	y = true;
    tel

as is this one:

    node f(a: bool :: . on a; b: bool :: . on a)
    returns (z: bool);
    var w : bool;
    let
	w = a when b;
	z = false fby w;
    tel

This invalid program is incorrectly accepted and leads to an internal
compiler error:

    node f (x : bool) returns (y:bool);
    var a : bool :: . on b;
	b : bool :: . on a;
    let
	y = true;
	a = true;
	b = true;
    tel

This patch enforces the well-formedness constraint. It gives a sensible
error message when the constraint cannot be satisfied.
2017-09-29 00:08:42 +02:00
Timothy Bourke
cae38d0e60 Accept when-syntax for declaring clocks
The parameter or local declaration:
    x : bool :: . on y

Can now be made using the 'standard' Lustre syntax:
    x : bool when y

In this case, the translation gives x the clock:
    'a on y

and relies on the (MiniLS) Clocking pass to instantiate the fresh clock
variables.
2017-09-29 00:08:42 +02:00
Timothy Bourke
0ef0ac5529 Allow "and" as a synonym for "&" 2017-09-29 00:08:42 +02:00
Timothy Bourke
3d75602a0d Accept "e when not x" for "e whenot x" 2017-09-29 00:08:42 +02:00
Timothy Bourke
9de1a96843 Allow (optional) semicolon after returns clause 2017-09-29 00:08:42 +02:00
Timothy Bourke
685c3aa862 Accept .lus file extension 2017-09-29 00:08:42 +02:00
Timothy Bourke
66da5f4b5c Minor fix to Merlin improvements. 2017-09-29 00:08:42 +02:00
Timothy Bourke
f8afddd0d9 Work better with merlin 2017-09-29 00:08:42 +02:00
Nicolas Berthier
100c08ee36 Bug correction in normalization of merge: fix propagation of type annotations
Minils.CtrlNbacGen relies on such type annotations to generat
Controllable-Nbac nodes.  This fix allows the use of ReaX to enforce
contracts of nodes involving merge operations on tuples over multiple
data types, such as:

  (a, b) = merge c
           (true -> ((true when c), (0 when c)))
           (false -> ((false whenot c), (2 whenot c)));

This kind of code previously led to erroneous Controllable-Nbac code.
2017-09-21 16:29:06 +01:00
Nicolas Berthier
15b2c09425 Adapt to new interface of reatk.ctrlNbac (≥ 0.11) 2017-09-20 16:47:17 +01:00
Gwenaël Delaval
4274b21733 Version 1.03.04 2017-05-24 01:19:55 +02:00
Gwenaël Delaval
b942f456ed "Last" pass bug correction 2017-05-23 23:30:11 +02:00
Gwenaël Delaval
35bce1d5e8 Added simple scheduler with -simple-scheduler option
Scheduler_simple module: simplest possible scheduler, with
only topological sort and without any "smart" algo/heuristic.
2017-05-23 22:16:57 +02:00
Gwenaël Delaval
7d6106d0aa Passes optimization
Translation to tail-recursive versions of functions
for handling of (very) big nodes.
2017-05-23 22:13:32 +02:00
Gwenaël Delaval
b9870eefc0 Debug mode in _tags.in 2017-05-23 22:12:27 +02:00
Gwenaël Delaval
1ead8a98ea Correction of unary minus priority
To fix: see test minus_pre.ept:

node main() = (o,p:int)
let
  o = ~-1 -> pre o + 1;
  p = -1 fby p + 1
tel
2017-05-23 22:01:05 +02:00
Gwenaël Delaval
028c564a31 Clean-up of verbose output
Leave only comments about compilation passes.
Remove output of intermediate code on standard output: added
generation of <module>.log containing all intermediate code.
2017-05-23 11:37:30 +02:00
Gwenaël Delaval
63e090633c Corrected bug in causality analysis
The following node was accepted by the causality analysis:

node m(x:int) = (y,z:int)
let
    automaton
    state A
    do
      y = x + z;
      z = x + 1;
    until x = 3 then B
    state B
    do
      y = x + 3;
      z = y * x;
    until x = 10 then A
    end
tel

Each state is indeed causal, but once the automaton is translated to equations
(which is the systematic way in the current version), the node is not
schedulable.

Correction: all "Or" of dependency constraints translated to "And".

This constraint could be relaxed if code generation is done from Heptagon code,
before translation to minils equations.
2017-05-23 10:56:50 +02:00
Gwenaël Delaval
cc666cb32c Bug correction in init analysis
Correction: nodes instances must have well initialized inputs.
2017-03-17 15:18:31 +01:00
Gwenaël Delaval
e4f51fea68 Switch to non-deprecated String functions
Use of String.*_ascii non-deprecated versions.

NB: Heptagon becomes available only for Ocaml versions >= 4.03.0.
2017-03-14 12:24:29 +01:00
Gwenaël Delaval
d2dfed5019 Correction of shift/reduce conflict in syntax
Correction: in a contract, the list of objectives cannot be empty.
2017-03-14 12:14:19 +01:00
Gwenaël Delaval
0515cf4f80 Handling of implication operator in Ctrln back-end 2017-03-13 18:01:05 +01:00
Gwenaël Delaval
6c3caec234 Bug correction in ctrl2ept: no systematic conversion from int to float 2017-03-04 01:53:32 +01:00
Gwenaël Delaval
2f18926bf4 Clean up documentation comments 2017-03-03 11:41:57 +01:00
Gwenaël Delaval
2e107cd872 Suppress "c_" prefix in Ctrl-Nbac generation 2017-02-23 02:45:04 +01:00
Gwenaël Delaval
5b215f832b Version 1.03.02 2017-02-08 21:36:04 +01:00
Gwenaël Delaval
a0e97b82ea CtrlNbac backend: systematic sink state, outputs as local variables
Changes in CtrlNbac back-end :
- systematic sink state, only in ctrln code
- sink state "ok" removed (useless as was coded)
- no sink state in minils code
- outputs in ctrln are local variables, no longer state variables
2016-06-25 08:40:50 +02:00
Gwenaël Delaval
69b8cc5a18 Added operator (=>) in Pervasives module
Operator (=>) for implication added in Pervasives module.

"a => b" is translated into "not a or b" at code generation.
2016-06-25 08:37:47 +02:00
Gwenaël Delaval
5e277fcc8a Version 1.03.01 2016-06-02 01:59:51 +02:00
Gwenaël Delaval
83905f9039 Remove traces and warnings 2016-06-02 01:33:02 +02:00
Gwenaël Delaval
d8d24ffd95 Handle modularity/several controllers by module
* Several controllers by module : added option "-m <Module>" in ctrl2ept

Generate controllers for each node of one module in <module>_controller.ept

* Types of <Module> no longer moved to <Module>_controller

* Added "_types" suffix for type dependencies for C target
2016-06-02 01:33:02 +02:00
Gwenaël Delaval
05150f2078 [ctrl-n] Suppression of type declarations in Heptagon controller
TODO : move type declarations in separated module.
2016-06-02 01:33:02 +02:00
Timothy Bourke
0b7eba8458 Add error for non-stateful decls. in pervasives
Attempts to compile a pervasives.epi containing functions with multiple
outputs or nodes now fail with an informative error message.

* The following files demonstrate the problem:

  pervasives.epi:
    type bool = true | false
    external val node test(bool;bool) returns bool

  broken.ept:
    node broken() returns (y : bool)
    let
      y = test(false, false);
    tel

  Running:
    heptc -nopervasives pervasives.epi
    heptc -stdlib . -target c broken.ept

  Fails with:

    ---------
    Internal compiler error
    Passe : Static evaluation failed of the pervasive operator test
    ----------
    Fatal error: exception Misc.Assert_false

* A different error occurs for nodes that return multiple outputs:

  pervasives.epi:
    type bool = true | false
    external val node test(bool;bool) returns (bool;bool)

  broken.ept:
    node broken() returns (y : bool)
    var l1 : bool;
    let
      (y,l1) = test(false, false);
    tel

  Running:
    heptc -nopervasives pervasives.epi
    heptc -stdlib . broken.ept

  Gives:
    Inconsistent clock annotation for exp test(false, false).
    File "broken.ept", line 4, characters 11-29:
    >  (y,l1) = test(false, false);
    >           ^^^^^^^^^^^^^^^^^^
    Clock Clash: this expression has clock 'a3,
    but is expected to have clock ('a4 * 'a5).

  The name "test" is parsed as an Eextvalue (rather than an Eapp), and there
  is an implicit assumption in compiler/minils/analysis/clocking.ml that such
  values have a simple clock.
2016-04-26 16:34:26 +02:00
Nicolas Berthier
755b570a96 Correct typing of numericals when translating Controllable-Nbac nodes
Without this change one could end up with inconsistent numerical types
when expressions like 1 + xx /. 3.0 >= 0 (with xx being a float), that
is correctly handled in ReaTK's frontend, are translated into the
heptagon's internal representation.
2016-03-30 17:35:56 +01:00
Gwenaël Delaval
4f0ef44ebd Version 1.03.00 2016-01-18 17:43:25 +01:00
Gwenaël Delaval
e9540a2159 hepts: enum types & alias
The graphical simulator hepts now support type aliasing.
2016-01-18 17:24:51 +01:00
Gwenaël Delaval
2aed0f6537 Deadcode removal improvement
Deadcode removal in Obc :
- suppression of switch unused cases :

switch(true) {
  case false: ...
}

- activation with -deadcode option
2016-01-18 14:32:54 +01:00
Gwenaël Delaval
64b8c0592a Pretty-printing class parameters in obc 2016-01-18 14:31:04 +01:00
Gwenaël Delaval
19911506de Removal of warnings 2016-01-18 14:30:20 +01:00
Gwenaël Delaval
e8ec3e012c Merge branch 'ctrl-n' into decade 2015-12-15 09:33:25 +01:00