Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / TODO.org @ 9b0432bc

History | View | Annotate | Download (11.1 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

    
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