Commit graph

195 commits

Author SHA1 Message Date
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
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
9a29c6fa4b Upgrading to new ReaTK API (>= 0.9.4). 2014-10-03 10:57:23 +02:00
Nicolas Berthier
99ab12aa13 Fixed warnings. 2014-03-18 11:01:56 +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
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
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
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
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
3e8af67e07 Added Java 1.4 target (experimental)
Experimental : remains some bugs on arrays
2012-11-17 23:29:19 +01: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
Gwenaël Delaval
ccc07cc7b9 Unalias missing in obc translation 2012-07-31 15:22:38 +02:00
Gwenaël Delaval
ef00823cf7 Added Marc as co-author 2012-06-29 01:43:15 +02:00
Gwenaël Delaval
58086190eb Headers and license file for GPL
Headers for every source file (excluding examples), mentioning
authors, copyright and license (GPL)

COPYING file with GPLv3 content.
2012-06-27 18:14:29 +02:00
Cédric Pasteur
8815a2cd03 Better handling of clocks in memalloc
- 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
2012-06-20 09:17:13 +02:00
Cédric Pasteur
ee7d60120b Fixed bug in translation to minils 2012-06-19 15:56:54 +02:00
Gwenal Delaval
2956002f85 Correction and simplification of the sigali pass
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).
2012-06-06 15:59:08 +02:00
Gwenal Delaval
bb0bc8bfe5 Added local assume/guarantee
Added local assume/guarantee in contracts.

No syntax associated to these local asume/guarantee: internal use only.
2012-05-29 14:14:46 +02:00
Adrien Guatto
e05f3732a0 Timing framework. 2012-03-07 17:48:08 +01:00
Adrien Guatto
f09792485e Hept2mls: fixed missing enter_node 2012-03-07 17:48:08 +01:00
Léonard Gérard
8a78bc7d7d Add [external] in the signatures. fix callgraph acordingly. 2012-02-21 16:07:29 +01:00
Adrien Guatto
76ae2f4518 Loop unrolling. 2012-02-08 16:16:41 +01:00
Cédric Pasteur
2f993a602c Fixed base clock in code generation
Put the base clock inside the equation where it 
belongs.
2012-01-25 09:34:58 +01:00
Adrien Guatto
cad8a0149f Option to perform type inference on all types 2012-01-23 13:36:24 +01:00
Léonard Gérard
f0cbbccc2a unsafe in minils node 2011-12-12 11:27:18 +01:00
Cédric Pasteur
54cde301f6 C code generation for printf 2011-12-12 10:36:24 +01:00
Cédric Pasteur
f76667e042 Second part of the fix 2011-12-06 15:44:20 +01:00
Léonard Gérard
d5f72c278c mls2obc bug fix
y = (if then else) when c
ou bien
y = f() when c
ne compilait pas.
2011-11-28 15:12:22 +01:00
Adrien Guatto
1b73f3444e Clock before dumping .epci 2011-11-24 11:41:11 +01:00
Léonard Gérard
fdab1ac55c Strict-SSA option to switch array encoding. 2011-11-21 03:26:26 +01:00
Léonard Gérard
b49c37f7bf Add ways to declare unsafe functions + unsafe fix 2011-11-21 03:26:26 +01:00
Léonard Gérard
efa6b5cf70 Correct scalarize and java load_conf 2011-11-18 12:32:37 +01:00
Adrien Guatto
1a9dc17618 Fixed clocking annotations.
1. Transmit annotations to extvaluese in Hept2mls.

2. Handle a pre-existing w_ck when clocking extvalues.
2011-11-10 15:36:54 +01:00
Léonard Gérard
76109b553a Add -O option to enable optims. 2011-11-02 17:23:23 +01:00
Léonard Gérard
33021aaa90 Print stateful in heptagon.
Conflicts:

	compiler/heptagon/hept_printer.ml
2011-11-02 13:15:33 +01:00
Léonard Gérard
ffe2b23a82 new sheduler by default 2011-10-23 17:42:26 +02:00
Cédric Pasteur
04b8853a1d Added a new reinit operator
It has type:
reinit: t at r * t -> t at r

It can be used to put a constant value in a 
location.
2011-10-17 15:28:04 +02:00
Cédric Pasteur
4d912e9349 Added more options for memalloc
There is now three options for memory allocation:
  - -only-linear activates only the linear 
annotations (with typing and code generation)
  - -only-memalloc does only memory allocation
  - -memalloc does both

When linear typing is not activated, linearity 
annotations are ignored (the signature in the .epi
does not contain the annotations)
2011-09-09 16:05:44 +02:00
Cédric Pasteur
81947eca40 Made linearity field not optional
This helped solve a few bugs with linear types,
for instance when using automata.
The intermediate code is not well-typed (wrt to
linear types only), after the encoding of automata.
2011-09-07 17:51:31 +02:00
Cédric Pasteur
33bc0adff1 Type should be unaliased when expecting an array 2011-09-06 13:39:44 +02:00
Cédric Pasteur
8cc879be7a Generate code from interface (.epi) files
It includes the definition of types, constants
and prototypes defined in the interface.
2011-09-06 11:55:06 +02:00
Cédric Pasteur
379f509dfc Added typing of signatures
This fixes a bug where mapfold would insert 
untyped constants in the code.
2011-09-05 15:33:31 +02:00