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

822 commits

Author SHA1 Message Date
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