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
|
|
145
|
*** To be done
|
146
|
|
147
|
**** Court terme
|
148
|
- (CG) etendre la syntaxe pour coller à la definition donnée ci-dessus
|
149
|
- lexeur/parseur lustreSpec + document latex de grammaire
|
150
|
- repartir la branche acsl2018 qui contient la normalisation des eexpr
|
151
|
- le refaire compiler
|
152
|
- merger avec unstable
|
153
|
- transformer cette normalisation pour partager les definitions locales de
|
154
|
variables dans le noeud de spec, aka contract
|
155
|
|
156
|
**** Apres
|
157
|
- developper dans les backends
|
158
|
- C
|
159
|
- EMF
|
160
|
- LustreV
|
161
|
|
162
|
* Slicing
|
163
|
- reprendre le slicing inlined de seal pour
|
164
|
- when provided with a main node and a selection of outputs or memories
|
165
|
- slice the local node
|
166
|
- for each node called try to slice to the selected vars
|
167
|
- could be used to analyze counterexamples
|
168
|
* TODO refactoring + doc
|
169
|
- DONE separate lustre types from machine types in different files
|
170
|
- DONE split basic libs into backend specific files
|
171
|
- DONE define mli for core steps: normalization and machine code
|
172
|
- define mli for lustre_type and machine_type (Garion)
|
173
|
|
174
|
* TODO
|
175
|
** include files
|
176
|
** main function
|
177
|
*** add a clean test to forbid array arguments for main node
|
178
|
(no available input/output methods)
|
179
|
** test suite
|
180
|
*** for complex dependency graphs (notably mem/mem cyclic dependencies)
|
181
|
*** for clocks
|
182
|
*** for arrays (non-generic nodes)
|
183
|
** compare with lus2c (verimag)
|
184
|
** extension
|
185
|
*** array access: done
|
186
|
*** add an option to dynamically check array accesses: done
|
187
|
*** power operator: done
|
188
|
*** automaton
|
189
|
*** annotations to ACSL
|
190
|
** init checking
|
191
|
*** to be done !!!
|
192
|
** normalization
|
193
|
*** sub-expression sharing seems to be not totally working: fixed
|
194
|
*** improve behavior for power and access operators:done
|
195
|
*** more type-directed normalization (notably to improve code gen for arrays): done
|
196
|
*** reuse of dead vars instead of systematically allocating new local vars
|
197
|
*** add a clean test for used but undefined nodes
|
198
|
** typing
|
199
|
*** correct typing of arith ops (real/int with subtyping ?)
|
200
|
*** display array dimensions with correct names: done
|
201
|
*** clocks must not be static inputs: done
|
202
|
** clock calculus
|
203
|
*** extension from named clocks to valued clocks ?
|
204
|
*** static inputs should be polymorphic, as global constants are: done
|
205
|
|
206
|
* Horn backend
|
207
|
** enum types for automaton
|
208
|
- issues with MBranches and clocks
|
209
|
- control-on-clock generates a "if cond then expr else nothing
|
210
|
- it has to be expressed in a functional way to enable its expression as
|
211
|
horn
|
212
|
|
213
|
|
214
|
- The issue seems mainly to lie in the out = f(in) every cond
|
215
|
this generates the follwoingg imperative statements
|
216
|
if cond then f_reset(*mem) else {(nothing, ie. not reset)}
|
217
|
f_step(in,*put,*mem)
|
218
|
|
219
|
In the machine code, this is done by generating the sequence of 2 instructions
|
220
|
1. if cond then MReset() else {} (* creation of a conditional statement *)
|
221
|
2. MStep()
|
222
|
|
223
|
- For Xavier: Syntactically, how could you "reset" an arrow? When we see an
|
224
|
Expr_arrow, we introduce a MReset instance to the set of instruction on the
|
225
|
reset function of the current node, but is there any mean to do it with
|
226
|
"every" ?
|
227
|
|
228
|
|
229
|
|
230
|
|
231
|
x = expr when c
|
232
|
|
233
|
if c then
|
234
|
x= expr
|
235
|
|
236
|
else {}
|
237
|
|
238
|
x = if c then expr else x
|
239
|
* Seal
|
240
|
|
241
|
The Seal library should be available from LustreV
|
242
|
|
243
|
lustrev -seal -node foo bar.lus
|
244
|
|
245
|
shall inline completely the node foo in bar.lus and compile it as a
|
246
|
piecewise system:
|
247
|
- Memories have to be identified and one needs to separate the update
|
248
|
of the memories and the production of the output.
|
249
|
- The update block should be normalized so that any ite occuring in
|
250
|
the definition of a memory should not define a local flow used in
|
251
|
basic operations. In other words, the definitions should look like
|
252
|
mem_x = if g then e1 else e2 where e1 and e2 are either ite
|
253
|
expression or expressions without ite. As soon as a not-ite
|
254
|
expression is selected it cannot depend on the output of an ite.
|
255
|
|
256
|
In a first step this normalized update shall be printed in
|
257
|
stdout. Later it will associated to a SEAL datastructure through SEAL
|
258
|
API.
|
259
|
|
260
|
** Algorithm
|
261
|
|
262
|
*** 1. Computation of update block
|
263
|
- First we inline the node
|
264
|
- After normalization the memories are the variables defined by a pre
|
265
|
- Do we have to deal with arrows and reset?
|
266
|
- Develop a function to perform slicing. Restrict the node eqs to the ones used in these pre defs.
|
267
|
- one can also slice the expressions on the output variables
|
268
|
|
269
|
*** 2. Normalization: piecewise system
|
270
|
ie. all ite pushed at the beginning
|
271
|
|
272
|
- use the scheduling to obtain the dependencies amongs eqs
|
273
|
- one can then iterate through eqs from the bottom to the top
|
274
|
if the eq looks like x = if g then e1 else e2
|
275
|
then tag x as ite(g,e1,e2)
|
276
|
if the parent expr y = if g2 then x else ... make
|
277
|
** More general use
|
278
|
Some ideas
|
279
|
- One could request multiple nodes: how to deal with these? Acting as
|
280
|
as many calls to the basic procedure?
|
281
|
- Shall we keep the flatten update structure to the node? Another
|
282
|
property on input could be propagated.
|
283
|
- The analysis will depend on bounds on input flows. Can we specialize
|
284
|
the update blocks based on input values, ie. disabling some branches
|
285
|
of the ite-tree?
|
286
|
-
|
287
|
|
288
|
** TODO list
|
289
|
|
290
|
* Salsa
|
291
|
* Lusic
|
292
|
Lusic can be generated either from lusi files or from lus files
|
293
|
They shall contain at least
|
294
|
- the complete definitions of types
|
295
|
- the complete definition of constants
|
296
|
- the list of nodes and their types/clocks
|
297
|
- the complete definition of specification components:
|
298
|
- either defined in lusi as
|
299
|
- node spec: attached to a node
|
300
|
- contract: expressed as an imported node with a spec
|
301
|
- or defined in the lus
|
302
|
- node spec
|
303
|
- contract defined in a comment
|
304
|
- some compilation related information if compiled from a lusi
|
305
|
|
306
|
|
307
|
What happen when we compile first a lusi and then the lus file?
|
308
|
- types of the lus node are checked wrt the ones available in the
|
309
|
lusic (coming from the lusi)
|
310
|
- do we want to update the lusic for additional specification
|
311
|
defined in the lus, or do we assume that the lusi masks the spec
|
312
|
artifacts defined in the lus file ?
|
313
|
- do we want to embeded the node content in the compiled lusic,
|
314
|
updating it?
|
315
|
|
316
|
When opening another module, one loads the lusic file
|
317
|
- if compilation directives are provided then can support the
|
318
|
generation of the Makefile, linking proper libs.
|
319
|
- if the lusic contains node content one may use these to perform
|
320
|
inlining if asked by the users or in certain configurations
|
321
|
- decision: lusic do not contain actual code: #include shall allow
|
322
|
to include external lustre copde and inline it as if it was
|
323
|
defined in the current file
|
324
|
|
325
|
We would like to know whether a declared node:
|
326
|
- is an external function, possibly specified but not associated
|
327
|
eventually to some lustre node. Ie type conversion functions,
|
328
|
array functions with loops, ...
|
329
|
- is a pure specification function/node/contract
|
330
|
- is just a signature(+spec) of a regular node
|
331
|
|
332
|
Contracts in lusi are compiled as imported node with spec. We could
|
333
|
keep the info that they will not be associated to some real code.
|
334
|
While a regular imported node could.
|
335
|
|
336
|
Now the question is how to tag a lusi file to explicitely state that
|
337
|
no lus file will be associated to it. May be one can provide a link
|
338
|
to the backend implemented. Let say that this lusi file can be used
|
339
|
for the C backend then a C file should be provided. Do we want to
|
340
|
mention it in the lusi file?
|
341
|
|