Nicolas Berthier
fb6755efb2
Bugfix in ctrl2ept: do not reset symbol table after loading type declarations
2015-09-21 15:17:30 +02:00
Nicolas Berthier
14a7b67a70
New option to force abstraction of infinite-domain state variables in ctrln export
...
Also add an option to silence related warnings
2015-09-18 14:11:04 +02:00
Nicolas Berthier
2d874f8070
New option to silence warnings about untranslatable constructs
2015-09-18 13:59:33 +02:00
Nicolas Berthier
74b94c9718
Fix handling of nodes without actual controllers by ctrl2ept
...
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.
2015-09-18 09:51:41 +02:00
Gwenaël Delaval
61f043856a
Version 1.01.00
2015-09-17 10:29:20 +02:00
Gwenaël Delaval
9b75408f23
Bug correction in reset
...
"e1 fby e2" was not handled in the reset pass.
2015-09-04 17:35:12 +02:00
Adrien Guatto
dc47767ba4
Print an empty default statement at the end of all C switches
...
This prevents modern compilers from emitting warnings when the generated C code
contains switch statements with (intentionally) missing cases.
2015-06-12 17:49:59 +02:00
Gwenaël Delaval
e0bbc838d5
Allow use of declared parameters within parameters
...
Allow this node :
node f<<m:int; t1: int^m>>(a:int^m) = (o:int^m)
let
o = map<<m>> (+)(a, t1);
tel
2015-02-27 16:15:55 +01:00
Gwenaël Delaval
c5c5654068
Added bzreax script ; added uninstall target in Makefiles
2015-02-27 15:50:21 +01:00
Gwenaël Delaval
0d1aef8c78
Bug correction: support of enumerated types as input for simulation
...
- use of a buffer to translate enumerated types from string to enum value
- hepts : correct interface with main
2015-02-27 15:39:39 +01:00
Nicolas Berthier
95aa03ed21
Interface for new incremental API of menhir parsers' relies on MenhirLib
2015-01-28 18:08:53 +01:00
Gwenaël Delaval
3dfbeffeb6
Added syntax for reachability and attractivity in contracts
...
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"
2015-01-06 00:26:59 +01:00
Nicolas Berthier
177f5f9f3e
Avoid exporting contract-less or parametric nodes into DCS tool formats.
2014-12-15 15:56:37 +01:00
Nicolas Berthier
307f3d8418
Controllable-Nbac import&export now support relocation of alias types.
...
- 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.
2014-12-15 15:56:04 +01:00
Nicolas Berthier
c86d7af0b1
Introducing a hack to normalize comparison of tuples in Heptagon.
2014-12-15 15:42:37 +01:00
Nicolas Berthier
045e624f94
Bug fix with controllable-less contracts in ControllableNbac exporter.
2014-12-02 10:20:15 +01:00
Gwenaël Delaval
2a0927bd98
Bug correction in maybe_ctrln_pass
2014-12-01 14:44:08 +01:00
Nicolas Berthier
cbcf8b9ac0
Using unqualified names for string representation of constructors in C backend.
...
+ minor modifications in various places.
2014-11-13 09:45:15 +01:00
Nicolas Berthier
d4fe017864
Bug correction in names of C functions for converting constructors to string.
2014-10-31 15:40:05 +01:00
Nicolas Berthier
2d00f0a91c
Fix sink state variable generation in Controllable-Nbac export.
2014-10-31 14:42:37 +01:00
Nicolas Berthier
0afdb16c57
Requalify enumeration types only when exporintg to Controllable-Nbac.
2014-10-31 14:16:05 +01:00
Nicolas Berthier
39aa0e13c1
Ugly fix for handling enumerated types when exporting to Controllable-Nbac.
...
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.
2014-10-30 12:01:25 +01:00
Nicolas Berthier
be21bf31d8
Insertion of call to controller(s) when exporting to Controllable-Nbac node.
...
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.
2014-10-28 16:43:13 +01:00
Nicolas Berthier
d84ae09cab
Bug fix (preprocessor variable).
2014-10-23 11:23:36 +02:00
Nicolas Berthier
bc17d71e3f
New tool `ctrl2ept' for translating ReaX's output functions into Heptagon
...
Compilation of the tool is dependent on the presence of the
`reatk.ctrlNbac' library.
2014-10-22 17:46:05 +02:00
Nicolas Berthier
541dd83fca
Optional compilation of Controllable-Nbac-related modules and tools.
2014-10-21 15:41:40 +02:00
Nicolas Berthier
5506690de5
Merge branch 'decade' into ctrl-n
2014-10-03 10:58:41 +02:00
Nicolas Berthier
9a29c6fa4b
Upgrading to new ReaTK API (>= 0.9.4).
2014-10-03 10:57:23 +02:00
Valentin Perrelle
1f2e084e6e
Fixed a bug where loops were not generated for copying arrays.
2014-06-25 18:53:34 +02:00
Nicolas Berthier
99ab12aa13
Fixed warnings.
2014-03-18 11:01:56 +01:00
Nicolas Berthier
c3c7a331b6
Using ReaTK's Controllable-Nbac backend library.
2014-03-18 10:58:57 +01:00
Nicolas Berthier
850e8522dd
Merge branch 'decade' into ctrl-n
2014-03-03 16:46:21 +01:00
Gwenaël Delaval
478e621ac5
Handling of contracts in Mls2obc
...
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).
2014-02-22 23:53:49 +01:00
Gwenaël Delaval
8650ac5695
Version 1.00.06
2014-02-21 18:12:07 +01:00
Gwenaël Delaval
e885f82e00
Bug correction/feature adding: abstraction within contracts
...
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).
2014-02-21 17:39:37 +01:00
Gwenaël Delaval
9c4b3f3267
Version 1.00.05
2014-01-28 16:31:16 +01:00
Gwenaël Delaval
2d96b60c49
Bug corrections in contracts
...
Contracts handling : added variables for assume/guarantee
parts of subnodes as defined names in b_defnames
2014-01-27 00:26:24 +01:00
Gwenaël Delaval
c61e01f19b
Correct handling of comparison operators in Sigali
...
- bug fix: comparison between two non-constant integer expressions in Sigali
- bug fix: correct handling of "=" and "<>" operators in Sigali
2014-01-14 23:09:22 +01:00
Nicolas Berthier
c132b53732
Handle `when' operators in general expressions, in Controllable-Nbac backend.
...
- CtrlNbacGen: ignore sub-sampling in general expressions.
2013-11-26 18:03:07 +01:00
Nicolas Berthier
934c9f9a85
Handle `when' operators for non-Boolean expressions in Controllable-Nbac backend.
2013-11-20 12:13:01 +01:00
Nicolas Berthier
808b9772f3
Merge branch 'decade' into ctrl-n
2013-11-20 08:53:00 +01:00
Gwenaël Delaval
71497a82b2
Corrected bug in inline_extvalues
...
Inline_extvalues: added local variables of contracts into environments
2013-11-19 20:39:01 +01:00
Nicolas Berthier
ae6a3aac2e
Attractivity property of Controllable-Nbac output; minor refactorings.
2013-11-13 15:35:15 +01:00
Nicolas Berthier
216550c0d1
Fixed warnings & documentation comments.
...
- gitignore: ignore files generated by `configure' script.
2013-11-08 18:51:06 +01:00
Nicolas Berthier
10bdab4dc6
Exclusively use ocamlfind; source documentation generation.
...
- 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.
2013-11-08 15:50:36 +01:00
Nicolas Berthier
8aeab651ce
First draft for Controllable-Nbac format generation.
...
- 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.
2013-11-08 15:13:39 +01:00
Gwenaël Delaval
5b98f9cdf6
Version 1.00.02
...
Added CHANGES file
2013-10-29 19:03:31 +01:00
Gwenal Delaval
13d616c930
Scrollbars on inputs/outputs of hepts
...
Allowed shrinking hepts main window and added scrollbars on frames
for inputs and outputs.
2013-10-29 16:48:34 +01:00
Gwenaël Delaval
c0b84bd186
Abstraction of integers for Sigali
...
Correction of abstraction for Sigali: integer equations comprising no
integer variables should not be abstracted
2013-09-06 10:13:08 +02:00
Gwenaël Delaval
f3d34f57d1
Abstraction of integers for Sigali
...
Correction of abstraction for Sigali: integer equations comprising no
integer variables should not be abstracted
2013-09-05 19:03:22 +02:00
Gwenal Delaval
6e791e3199
More permissive syntax (trailing commas/semicols)
...
Allowing trailing commas and in parameters declarations
2013-08-02 14:14:14 +02:00
Gwenal Delaval
cd01f82cf6
Graphical simulator: output to GTKWave and TikZ
...
Added option -gtkwave, output in VCD (Value Change Dump) format
Button for TikZ (tikz-timing) export.
2013-08-02 14:14:13 +02:00
Gwenal Delaval
ee7ef158e7
Bug correction: java code generation for "~-."
...
Bug correction: handling of unary float "~-."
2013-08-02 14:14:13 +02:00
Gwenaël Delaval
71f7db2d11
Bug correction in Mls_printer and Hept_printer
...
Correction of infix operators printing : infix printing only
when two arguments of pervasives infix operators (no assertions
on number of arguments).
2013-07-10 09:57:19 +02:00
Gwenal Delaval
f696203eb1
Bug in sigalimain
...
Bug correction: code generation to sigali for stateless nodes
=> stateless nodes handled like stateful nodes, if not in pervasives.
2013-07-09 21:16:30 +02:00
Gwenal Delaval
2d150a3a3d
Infix operators in printers
...
Infix operators handled in Heptagon and Minils printers
2013-07-09 21:15:31 +02:00
Gwenaël Delaval
7720a632cc
Removed bugged local substitutions in Contracts pass
2013-05-17 23:21:43 +02:00
Cédric Pasteur
f5cc4625e0
And don't forget to type the argument of when
2013-05-07 17:13:00 +02:00
Cédric Pasteur
21aae319ee
Fixed linear typing of when
...
It is always a read. One has to use the
split operator for sampling linear variables.
2013-05-07 17:09:58 +02:00
Cédric Pasteur
a00620ca19
Fixed interference of fast memories
...
A fast memory should be considered alive during
the whole step function when its clock is false.
2013-05-06 11:47:05 +02:00
Cédric Pasteur
99dc7820c7
Avoid crash in memalloc
...
Check if both variables are optmized
2013-04-22 18:11:10 +02:00
Nicolas Berthier
8497bafa2e
Minor but correction in sigali output.
...
- 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
2013-04-11 17:30:30 +02:00
Nicolas Berthier
899d33afb6
Corrected a bug in generation of C records.
...
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.
2013-03-15 09:31:19 +01:00
Nicolas Berthier
9db97de879
Bug correction in `Sigalimain.translate_eq'.
...
- 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).
2013-03-12 16:53:52 +01:00
Gwenal Delaval
9b3ba83bb1
Bug correction in java generation
2013-03-11 16:04:12 +01:00
Gwenaël Delaval
f60b00e9e3
Bug correction in Inline_extvalues
...
Added handling of controllable variables in Inline_extvalues
2013-02-08 14:42:26 +01:00
Gwenal Delaval
e7f85d6b25
Configuration for binary release
...
- custom bytecode compilation
- added suffix (OS, cpu) in binary distrib
2013-01-28 15:55:56 +01:00
Gwenal Delaval
2be4e287b9
Take into account the -nosink option in Sigali
...
Corrected bug: do not suppress the last state
variable when -nosink is on.
2013-01-28 15:54:27 +01:00
Gwenaël Delaval
5a9b27d6a9
Correct handling of local assume/enforce of contracts
2012-12-11 08:20:04 +01:00
Gwenal Delaval
ce2e2bdcd0
Added -nbvars option for performance evaluation
2012-11-26 10:05:20 +01:00
Gwenaël Delaval
ef536f412d
Added option -nosink (CS optimisation)
...
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).
2012-11-23 12:23:17 +01:00
Gwenaël Delaval
5bdd891105
Handling of controllables in tomato
...
Added controllable variables as "inputs" in the
tomato pass.
2012-11-22 18:52:21 +01:00
Gwenaël Delaval
0e60d2e839
Boolean transformation: added inputs/outputs
...
Non transformation of inputs/outputs during
Boolean pass lead to bugs.
2012-11-22 18:49:12 +01:00
Gwenaël Delaval
e42ff23a4b
Corrected abstraction for z3z target
2012-11-22 18:37:32 +01:00
Gwenaël Delaval
3e8af67e07
Added Java 1.4 target (experimental)
...
Experimental : remains some bugs on arrays
2012-11-17 23:29:19 +01:00
Gwenal Delaval
74a760ee0a
Handling of controllables in Normalize_mem
2012-11-17 23:01:49 +01:00
Léonard Gérard
db89208f22
Translate last before removing automatons.
2012-11-05 10:10:32 +01:00
Guillaume Baudart
355998bab3
Fix printf typing
2012-10-31 15:59:26 +01:00
Léonard Gérard
b0e2e41299
Schedule: do only count optimized variables in costs.
2012-10-17 12:02:00 +02:00
Gwenaël Delaval
6dd1c743d6
Records in Java
...
Added support of records in Java
2012-09-30 01:40:18 +02:00
Gwenal Delaval
6a21e5d701
Iostream for Java
...
Added support of Iostream.printf (not fprintf)
for Java code gen.
2012-09-28 15:26:01 +02:00
Gwenal Delaval
eddeb1f4de
Bug correction tentative (itfusion)
...
Tentative of correction of itfusion bug:
The itfusion pass adds some "anonymous" nodes into the module.
This correction adds the signature of these created nodes.
This only shifts the bug (towards clocking pass).
2012-09-28 13:06:46 +02:00
Gwenal Delaval
b176384952
Java code generation: lexicography
...
Handling of weird lexical elements (e.g., idents with ', infix names...)
2012-09-28 13:04:08 +02:00
Cédric Pasteur
36bfa81b17
Fix for memalloc
...
Take the simplified versions of types (i.e.
with constants instantiated) to check the
equality of types
2012-09-14 16:08:26 +02:00
Cédric Pasteur
96e233b64c
Fix for tuples of consts used as args
2012-09-14 15:42:49 +02:00
Gwenal Delaval
9334b73ef1
Naive abstraction for sigali
2012-08-08 18:16:33 +02:00
Gwenal Delaval
b199de202b
Removed '~>' in clock prints
...
'~>' (representing links between clock variables)
are printed when -fti option is on.
2012-08-08 18:14:05 +02:00
Gwenal Delaval
b60ee4b91d
Bug correction in Completion pass
...
Completion pass: do not propagate defnames to
other equations
(see test test_option_flatten_t4 : flatten t4, compile C target code)
2012-08-06 12:04:39 +02:00
Gwenal Delaval
857dccd0b2
Corrected Boolean pass
...
e_level_ck correctly translated
Hept_clocking on stateless functions
2012-08-02 17:24:30 +02:00
Gwenal Delaval
41fccc66fb
Bugs corrections
...
- 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)
2012-08-01 17:08:58 +02:00
Gwenal Delaval
b858f0e987
Reads and writes of records in main simulation
2012-07-31 16:58:22 +02:00
Gwenal Delaval
ccab6f7aad
Normalization of record consts
...
Normalization of records as constant to ease the compilation:
f({ x = e })
->
v = { x = e };
f(v)
2012-07-31 16:58:22 +02:00
Gwenaël Delaval
ccc07cc7b9
Unalias missing in obc translation
2012-07-31 15:22:38 +02:00
Gwenaël Delaval
35bea85bf7
Boolean: no transformation on inputs/outputs
...
Only translate local variables, so as to not
modify node interfaces.
2012-07-26 01:45:38 +02:00
Gwenaël Delaval
72b1bd8de3
Typo in error message
2012-07-26 01:33:32 +02:00
Gwenaël Delaval
90dda27a3a
Bug correction in Schedule_interf
...
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.
2012-07-26 01:29:22 +02:00
Gwenal Delaval
5ed07e1e5a
Removed systematic qual. of infix op as pervasives
...
Bug: every infix operator was systematically qualified
as pervasive.
2012-07-24 17:09:51 +02:00
Gwenal Delaval
70cb94d0bd
Unroll correction
...
Order of statement was incorrect
2012-07-23 17:35:20 +02:00
Gwenal Delaval
7e90dccc0a
Cleared java simulation output
2012-07-16 11:37:50 +02:00
Gwenaël Delaval
a15e17c02d
Cleared simulation output
2012-07-16 00:58:40 +02:00