|
1
|
* TODO refactoring + doc
|
|
2
|
- separate lustre types from machine types in different files
|
|
3
|
- split basic libs into backend specific files
|
|
4
|
- define mli for core steps: normalization and machine code
|
|
5
|
- define mli for lustre_type and machine_type (Garion)
|
|
6
|
|
|
7
|
* TODO
|
|
8
|
** include files
|
|
9
|
** main function
|
|
10
|
*** add a clean test to forbid array arguments for main node
|
|
11
|
(no available input/output methods)
|
|
12
|
** test suite
|
|
13
|
*** for complex dependency graphs (notably mem/mem cyclic dependencies)
|
|
14
|
*** for clocks
|
|
15
|
*** for arrays (non-generic nodes)
|
|
16
|
** compare with lus2c (verimag)
|
|
17
|
** extension
|
|
18
|
*** array access: done
|
|
19
|
*** add an option to dynamically check array accesses: done
|
|
20
|
*** power operator: done
|
|
21
|
*** automaton
|
|
22
|
*** annotations to ACSL
|
|
23
|
** init checking
|
|
24
|
*** to be done !!!
|
|
25
|
** normalization
|
|
26
|
*** sub-expression sharing seems to be not totally working: fixed
|
|
27
|
*** improve behavior for power and access operators:done
|
|
28
|
*** more type-directed normalization (notably to improve code gen for arrays): done
|
|
29
|
*** reuse of dead vars instead of systematically allocating new local vars
|
|
30
|
*** add a clean test for used but undefined nodes
|
|
31
|
** typing
|
|
32
|
*** correct typing of arith ops (real/int with subtyping ?)
|
|
33
|
*** display array dimensions with correct names: done
|
|
34
|
*** clocks must not be static inputs: done
|
|
35
|
** clock calculus
|
|
36
|
*** extension from named clocks to valued clocks ?
|
|
37
|
*** static inputs should be polymorphic, as global constants are: done
|
|
38
|
|
|
39
|
* Horn backend
|
|
40
|
** enum types for automaton
|
|
41
|
- issues with MBranches and clocks
|
|
42
|
- control-on-clock generates a "if cond then expr else nothing
|
|
43
|
- it has to be expressed in a functional way to enable its expression as
|
|
44
|
horn
|
|
45
|
|
|
46
|
|
|
47
|
- The issue seems mainly to lie in the out = f(in) every cond
|
|
48
|
this generates the follwoingg imperative statements
|
|
49
|
if cond then f_reset(*mem) else {(nothing, ie. not reset)}
|
|
50
|
f_step(in,*put,*mem)
|
|
51
|
|
|
52
|
In the machine code, this is done by generating the sequence of 2 instructions
|
|
53
|
1. if cond then MReset() else {} (* creation of a conditional statement *)
|
|
54
|
2. MStep()
|
|
55
|
|
|
56
|
- For Xavier: Syntactically, how could you "reset" an arrow? When we see an
|
|
57
|
Expr_arrow, we introduce a MReset instance to the set of instruction on the
|
|
58
|
reset function of the current node, but is there any mean to do it with
|
|
59
|
"every" ?
|
|
60
|
|
|
61
|
|
|
62
|
|
|
63
|
|
|
64
|
x = expr when c
|
|
65
|
|
|
66
|
if c then
|
|
67
|
x= expr
|
|
68
|
|
|
69
|
else {}
|
|
70
|
|
|
71
|
x = if c then expr else x
|