Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / TODO.org @ master

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