Before this commit, the C backend would put the translated definitions
of an interface file A.epi into A.{h,c}. This is inconsistent with the
C code generated for source files, which expects to find A_types.{h,c}.
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.
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.
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.
jeltz
Gwenaël Delaval
Adrien Guatto
Nicolas Berthier
Timothy Bourke