lustrec / TODO.org @ 0d54d8a8
History | View | Annotate | Download (6.99 KB)
1 |
* Cocospec integration |
---|---|
2 |
** Objective |
3 |
Enable the parsing of cocospec in comments. The syntax is the one of Kind2 but |
4 |
could be extended later. |
5 |
|
6 |
In terms of integration within LustreC, it has to be done at all stages |
7 |
- parsing/lexing |
8 |
- typing |
9 |
- clocking |
10 |
- normalization: the cocospec lustre equations have to be normalized |
11 |
- printing |
12 |
- machine code |
13 |
- various backends |
14 |
- EMF |
15 |
- LustreV/Zustre |
16 |
- C code |
17 |
|
18 |
** Open questions |
19 |
|
20 |
The cocospec syntax is appealing for multiple aspects wrt the our previous |
21 |
annotation language. |
22 |
- more structure |
23 |
- notion of contracts that can be imported, reused |
24 |
- more expressivity: local variables within contracts (more like regular lustre |
25 |
definitions *) |
26 |
|
27 |
But also some not-so-nice features (ploc's remarks): |
28 |
- annotations next to the node header shall be before rather than after. We also |
29 |
don't want pure specification artifact as top level definition in the lustre |
30 |
file (no contract def outside comments) |
31 |
- Frama-C inspiration |
32 |
I would prefer like in framac: |
33 |
//@ensures prop; |
34 |
node foo (...) returns (...); |
35 |
|
36 |
Rather than |
37 |
node foo (...) returns (...); |
38 |
//@ensures prop; |
39 |
|
40 |
While it make sense when you provide specification within the lustre file, it |
41 |
is less appropriate when specifying outside the lustre model. Eg in a lusi, #open |
42 |
spec.lusi |
43 |
|
44 |
- Kind2 approach |
45 |
In Kind2 they have a notion of interfaces, but they need an explicit local |
46 |
annotation linking the node to the contract |
47 |
|
48 |
In foo.lus we would have |
49 |
#include foo_spec.lus |
50 |
|
51 |
node bar (...) returns (...); |
52 |
(*@ contract import bar_spec (in) returns (out); *) |
53 |
let ... tel |
54 |
|
55 |
In foo_spec.lus |
56 |
contract bar_spec (..) returns (..) |
57 |
|
58 |
- Remote specification (in lusi) |
59 |
We would like to enable both local spec and remote ones (in a separate file). |
60 |
A solution could be to extend the lusi syntax, for example something like |
61 |
node bar (...) returns (...) |
62 |
let |
63 |
@ensures ... |
64 |
@requires ... |
65 |
tel |
66 |
|
67 |
Or, more generally, support contracts definition only in lusi and assigning |
68 |
contracts to nodes in the lusi or in the lus |
69 |
|
70 |
For example in the lusi |
71 |
|
72 |
contract bar_spec1 () returns (); |
73 |
let |
74 |
... contract 1 |
75 |
tel |
76 |
|
77 |
contract bar_spec2 () returns (); |
78 |
let |
79 |
... contract 2 |
80 |
tel |
81 |
|
82 |
node bar (...) returns (...); |
83 |
(*@ contract |
84 |
import bar_spec1 (in) returns (out); |
85 |
import bar_spec2 (in) returns (out); |
86 |
*) |
87 |
|
88 |
node bar2 (...) returns (...); |
89 |
(*@ contract guarantee expr; *) |
90 |
|
91 |
Or with annotations before the headers |
92 |
(*@ contract |
93 |
import bar_spec1 (in) returns (out); |
94 |
import bar_spec2 (in) returns (out); |
95 |
*) |
96 |
node bar (...) returns (...); |
97 |
|
98 |
(*@ contract guarantee expr; *) |
99 |
node bar2 (...) returns (...); |
100 |
|
101 |
In the associated lustre file |
102 |
|
103 |
#open my_spec.lusi |
104 |
|
105 |
node bar (...) returns (...) |
106 |
let |
107 |
full definition |
108 |
tel |
109 |
|
110 |
node bar3 (...) returns (...) |
111 |
(*@ contract my_remote contract *) |
112 |
let |
113 |
full definition |
114 |
tel |
115 |
|
116 |
-- a local contract |
117 |
node bar4 (...) returns (...) |
118 |
(*@ contract guarantee expr; *) |
119 |
let |
120 |
full definition |
121 |
tel |
122 |
|
123 |
But no contracts definition within the lustre ourside of special comments |
124 |
|
125 |
** Current status |
126 |
- Existing works in lustrec |
127 |
ensures/requires/observer in the syntax, which were parsed, typed, normalized |
128 |
|
129 |
- Choice of placement of annotations |
130 |
- no contract in lustre only in lusi |
131 |
- in lustre file: contract attached to lustre node before the locals/let |
132 |
- in lusi file: contract attached to lustre node before the node foo ... |
133 |
|
134 |
- Dev. choices |
135 |
- contracts rely look like imported node: a signature and a contract content attached |
136 |
- in lusi one could have an alias for contract / imported node |
137 |
- in lus similarly a top level contract could be parsed as an imported node |
138 |
- contract import would amount to concatenate contract elements |
139 |
from provided nodes or imported nodes. |
140 |
|
141 |
** Development |
142 |
*** Done |
143 |
- (ploc) retirer le parser Kind2 et revenir à celui de lustrec |
144 |
*** To be done |
145 |
**** Court terme |
146 |
- (CG) etendre la syntaxe pour coller à la definition donnée ci-dessus |
147 |
- lexeur/parseur lustreSpec + document latex de grammaire |
148 |
- repartir la branche acsl2018 qui contient la normalisation des eexpr |
149 |
- le refaire compiler |
150 |
- merger avec unstable |
151 |
- transformer cette normalisation pour partager les definitions locales de |
152 |
variables dans le noeud de spec, aka contract |
153 |
|
154 |
**** Apres |
155 |
- developper dans les backends |
156 |
- C |
157 |
- EMF |
158 |
- LustreV |
159 |
|
160 |
* Slicing |
161 |
- reprendre le slicing inlined de seal pour |
162 |
- when provided with a main node and a selection of outputs or memories |
163 |
- slice the local node |
164 |
- for each node called try to slice to the selected vars |
165 |
- could be used to analyze counterexamples |
166 |
* TODO refactoring + doc |
167 |
- separate lustre types from machine types in different files |
168 |
- split basic libs into backend specific files |
169 |
- define mli for core steps: normalization and machine code |
170 |
- define mli for lustre_type and machine_type (Garion) |
171 |
|
172 |
* TODO |
173 |
** include files |
174 |
** main function |
175 |
*** add a clean test to forbid array arguments for main node |
176 |
(no available input/output methods) |
177 |
** test suite |
178 |
*** for complex dependency graphs (notably mem/mem cyclic dependencies) |
179 |
*** for clocks |
180 |
*** for arrays (non-generic nodes) |
181 |
** compare with lus2c (verimag) |
182 |
** extension |
183 |
*** array access: done |
184 |
*** add an option to dynamically check array accesses: done |
185 |
*** power operator: done |
186 |
*** automaton |
187 |
*** annotations to ACSL |
188 |
** init checking |
189 |
*** to be done !!! |
190 |
** normalization |
191 |
*** sub-expression sharing seems to be not totally working: fixed |
192 |
*** improve behavior for power and access operators:done |
193 |
*** more type-directed normalization (notably to improve code gen for arrays): done |
194 |
*** reuse of dead vars instead of systematically allocating new local vars |
195 |
*** add a clean test for used but undefined nodes |
196 |
** typing |
197 |
*** correct typing of arith ops (real/int with subtyping ?) |
198 |
*** display array dimensions with correct names: done |
199 |
*** clocks must not be static inputs: done |
200 |
** clock calculus |
201 |
*** extension from named clocks to valued clocks ? |
202 |
*** static inputs should be polymorphic, as global constants are: done |
203 |
|
204 |
* Horn backend |
205 |
** enum types for automaton |
206 |
- issues with MBranches and clocks |
207 |
- control-on-clock generates a "if cond then expr else nothing |
208 |
- it has to be expressed in a functional way to enable its expression as |
209 |
horn |
210 |
|
211 |
|
212 |
- The issue seems mainly to lie in the out = f(in) every cond |
213 |
this generates the follwoingg imperative statements |
214 |
if cond then f_reset(*mem) else {(nothing, ie. not reset)} |
215 |
f_step(in,*put,*mem) |
216 |
|
217 |
In the machine code, this is done by generating the sequence of 2 instructions |
218 |
1. if cond then MReset() else {} (* creation of a conditional statement *) |
219 |
2. MStep() |
220 |
|
221 |
- For Xavier: Syntactically, how could you "reset" an arrow? When we see an |
222 |
Expr_arrow, we introduce a MReset instance to the set of instruction on the |
223 |
reset function of the current node, but is there any mean to do it with |
224 |
"every" ? |
225 |
|
226 |
|
227 |
|
228 |
|
229 |
x = expr when c |
230 |
|
231 |
if c then |
232 |
x= expr |
233 |
|
234 |
else {} |
235 |
|
236 |
x = if c then expr else x |