jeltz/heptagon
1
0
Fork 0
Code Issues Pull requests Releases Activity
1141 commits 2 branches 0 tags 6.9 MiB
Commit graph

917 commits

Author SHA1 Message Date
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
Gwenaël Delaval
e103d60c26 Removed eprintf in schedule_interf 
eprintf -> Interference.print_debug
 2012-07-14 14:31:46 +02:00
Cédric Pasteur
84e502d7a9 Made val optional for functions 
external val node f is a little bit too long
 2012-07-04 17:26:38 +02:00
Gwenaël Delaval
bf03077cd9 Correct output toward hepts 2012-06-29 02:01:49 +02:00
Gwenaël Delaval
ef00823cf7 Added Marc as co-author 2012-06-29 01:43:15 +02:00
Gwenaël Delaval
c080ad6cf3 Controller call only when controllables 
Avoid built of dummy empty controllers
 2012-06-29 01:41:13 +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
5e1dad630b Force fby to be scheduled at the end 2012-06-20 17:09:30 +02:00
Cédric Pasteur
7a10ba028a Fixed disjoint clock computation 2012-06-20 17:09:17 +02:00
Cédric Pasteur
ffeb81f529 Use idents instead of ivars in scheduling 2012-06-20 16:33:06 +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
Cédric Pasteur
ed2c08315b Should be affinity, not copy 2012-06-19 09:33:27 +02:00
Gwenal Delaval
502c5e446f Makefile correction (install target) 
Makefile correction: install target for simulator
 2012-06-13 15:13:53 +02:00
Gwenal Delaval
352bad4735 Correction of Inline pass 
- correction of Hept_mapfold : inclusion of mapfold for b_defnames (blocks)
- Inlining : deep replacement of idents
 2012-06-13 15:06:05 +02:00
Gwenal Delaval
cf22ba3989 Optional block in contracts 
Optional let...tel block in contracts
Sink state in sigali
 2012-06-07 17:48:31 +02:00
Gwenal Delaval
2bd31db883 Causality and scheduling with contracts 
Correction of the causality analysis and scheduling (with interference)
to take contracts into account.
 2012-06-07 15:27:07 +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
1e46c2a73c Makefile : removed target "all" from target "install" 
On some systems, the targets "all" and "install" must be
made with different rights. Then "all" cannot be a dependendy of
"install", especially since ocamlbuild try to read/modify some
files even if there is no compilation to perform.
 2012-06-06 15:55:23 +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
8153bc4eb5 Fixed Tomato: did not reconstruct internal clocks of extvalues 2012-03-30 14:47:47 +02:00