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).
- 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
- In Sigalimain: untranslatable non-boolean expressions should not be
added as inputs of the controller.
- Avoided some compiler warnings in the same module (with OCaml ≥ 4).
The -nosink option suppress the sink state of sigali equations.
This optimizes the controller synthesis, but work only
when the synthesis objective instantaneoulsy depends only
on the current state (and not on current inputs).
- callgraph: add idents used for instantiated nodes
- cgen : added Idents.enter_node
- cmain : removed error when simulated node does not exist (existence
of simulated node was tested for every program, comprising loaded ones)
Bug due to the fact that a variable can be "defined" and "read"
(in scheduling sense) by the same equation, without being a memory:
e.g., a clock defined as the result of a node application, together
with another result on this same clock.
Bug correction: basically removed the "assert false" on killed_vars,
decr_uses; do not count as "use" the self reads.
- We can do a better allocation if we take into
account 'when' in extvalues
(test/good/memalloc_clocks.ept shows the
improvement)
- Fixed a bug with memalloc on records: if we
translate:
o = { a with .f = u }
to
o = a; o.f = u
then we cannot share u and o.f
Added a "Contracts" pass, after inlining, taking care of the
contracts of the nodes called in the body of a node. This pass
"inlines" the code and assume/guarantee parts of these subcontracts.
The "Sigali" pass both generates the sigali ("z3z") code and add the call to
the controller (which is a node generated further by the sigali tool).
Therefore this pass has been included into the mls compiler, and removed
from the targets (a "z3z" dummy target has been kept for backward compatibility
reasons).
To know the variables read by an equation, we should
only look at the clock of variables. Otherwise,
there could be a problem for node calls that
define new clocks.
