Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / TODO.org @ 32bafa6f

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
*** 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
- DONE separate lustre types from machine types in different files
168
- DONE split basic libs into backend specific files
169
- DONE 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
237
* Seal
238

    
239
The Seal library should be available from LustreV
240

    
241
lustrev -seal -node foo bar.lus 
242

    
243
shall inline completely the node foo in bar.lus and compile it as a
244
piecewise system: 
245
- Memories have to be identified and one needs to separate the update
246
  of the memories and the production of the output.
247
- The update block should be normalized so that any ite occuring in
248
  the definition of a memory should not define a local flow used in
249
  basic operations.  In other words, the definitions should look like
250
  mem_x = if g then e1 else e2 where e1 and e2 are either ite
251
  expression or expressions without ite. As soon as a not-ite
252
  expression is selected it cannot depend on the output of an ite.
253

    
254
In a first step this normalized update shall be printed in
255
stdout. Later it will associated to a SEAL datastructure through SEAL
256
API.
257

    
258
** Algorithm
259

    
260
*** 1. Computation of update block
261
- First we inline the node
262
- After normalization the memories are the variables defined by a pre
263
- Do we have to deal with arrows and reset?
264
- Develop a function to perform slicing. Restrict the node eqs to the ones used in these pre defs.
265
- one can also slice the expressions on the output variables
266

    
267
*** 2. Normalization: piecewise system
268
 ie. all ite pushed at the beginning
269

    
270
- use the scheduling to obtain the dependencies amongs eqs
271
- one can then iterate through eqs from the bottom to the top
272
  if the eq looks like x = if g then e1 else e2
273
  then tag x as ite(g,e1,e2)
274
  if the parent expr y = if g2 then x else ... make 
275
** More general use
276
Some ideas
277
- One could request multiple nodes: how to deal with these? Acting as
278
  as many calls to the basic procedure?
279
- Shall we keep the flatten update structure to the node? Another
280
  property on input could be propagated.
281
- The analysis will depend on bounds on input flows. Can we specialize
282
  the update blocks based on input values, ie. disabling some branches
283
  of the ite-tree?
284
- 
285

    
286
** TODO list
287

    
288
* Salsa
289
* Lusic 
290
  Lusic can be generated either from lusi files or from lus files
291
  They shall contain at least
292
  - the complete definitions of types
293
  - the complete definition of constants
294
  - the list of nodes and their types/clocks
295
  - the complete definition of specification components:
296
    - either defined in lusi as 
297
      - node spec: attached to a node
298
      - contract: expressed as an imported node with a spec
299
    - or defined in the lus
300
      - node spec
301
      - contract defined in a comment
302
  - some compilation related information if compiled from a lusi
303
    
304

    
305
  What happen when we compile first a lusi and then the lus file?
306
  - types of the lus node are checked wrt the ones available in the
307
    lusic (coming from the lusi)
308
  - do we want to update the lusic for additional specification
309
    defined in the lus, or do we assume that the lusi masks the spec
310
    artifacts defined in the lus file ?
311
  - do we want to embeded the node content in the compiled lusic,
312
    updating it?
313

    
314
  When opening another module, one loads the lusic file
315
  - if compilation directives are provided then can support the
316
    generation of the Makefile, linking proper libs.
317
  - if the lusic contains node content one may use these to perform
318
    inlining if asked by the users or in certain configurations
319
    - decision: lusic do not contain actual code: #include shall allow
320
      to include external lustre copde and inline it as if it was
321
      defined in the current file
322

    
323
  We would like to know whether a declared node:
324
  - is an external function, possibly specified but not associated
325
    eventually to some lustre node. Ie type conversion functions,
326
    array functions with loops, ...
327
  - is a pure specification function/node/contract
328
  - is just a signature(+spec) of a regular node
329

    
330
  Contracts in lusi are compiled as imported node with spec. We could
331
  keep the info that they will not be associated to some real code.
332
  While a regular imported node could.
333

    
334
  Now the question is how to tag a lusi file to explicitely state that
335
  no lus file will be associated to it. May be one can provide a link
336
  to the backend implemented.  Let say that this lusi file can be used
337
  for the C backend then a C file should be provided. Do we want to
338
  mention it in the lusi file?
339