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.
Leave only comments about compilation passes.
Remove output of intermediate code on standard output: added
generation of <module>.log containing all intermediate code.
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.
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
* 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
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.
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.
These changes allow to handle the case where contracts are only used
for verification purposes, in which case the functions generated by
ReaX have no outputs and are not functions stricto sensu. Indeed, in
this case the new controller module still needs to be declared and
compiled as we may have re-qualified types during the generation of
the Controllable-Nbac code: we moved all types declared in the
original module into the controller module to break cyclic module
dependencies that would otherwise be introduced if the controller is
expressed using data of such types.
Contracts can now comprise a list of objectives (in any order).
One objective can be (e being a Boolean heptagon expression) :
- invariance, with the syntax "enforce e"
- reachability, "reachable e"
- attractivity, "attractive e"
- Controllable-Nbac export (CtrlNbacGen): correct handling of float
expressions, as well as alias types;
- Controllable-Nbac controller importer (CtrlNbacAsEpt): Declaration
of enumerated types and aliases that are relocated to controller
modules is now performed based on the interface. Dependencies
between type aliases are also taken into account now;
- ctrl2ept tool: correct loading of pervasives module.
To avoid cyclic module dependencies (that show up when trying to
compile, e.g, the generated C code), enumerated types declared in the
main program are now "moved" into the module containing the generated
controllers.
To enable recovery of parameter and output ordering by `ctrl2ept', the
Controllable-Nbac generation procedure now declares a new module
dedicated to the encapsulation of the controller functions yet to be
synthesized.
Handling of type declarations are probably buggy.
Handling of contracts when the "z3z" target is off. Equations of contracts are
put into the node in the Mls2obc pass (done by the "z3z" code generation).
Allowing additional inputs from abstractions within contracts. Thus,
calling non-inlined subnodes is allowed, as well as operations on
non-Boolean inputs or states (in contracts).
- Stripped portions of `myocamlbuild{,_config}.ml' that seem useless
when `-use-ocamlfind' is passed to ocamlbuild.
- Added some code in `myocamlbuild_config.ml' to be able to generate
documentation by merging interface and implementation files.
- CtrlNbac: new module for internal representation and output code for
Controllable-Nbac format;
- CtrlNbacGen: translation into Controllable-Nbac of Minils nodes
necessitating controller synthesis; the insertion of calls to
controllers is not yet done, and the nodes are left unchanged.
- Translation to z3z now evaluates constant expressions instead of
abstracting them. This non-feature could cause "false" synthesis
failures due to non-translatable yet constant expressions possibly
introduced by tomato (or manually), for instance `not false' in node
`n' bellow:
node n (a: bool) returns (ok: bool)
contract assume true enforce ok with ()
let
ok = a or not false;
tel
Corrected a somewhat unnoticeable but ugly bug in the generation of C
records, that could mess up the field names when they were not
assigned in the same order as in the declaration of the type.
