Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / TODO.org @ 4f26dcf5

History | View | Annotate | Download (6.38 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
** Development
135
*** Done
136
- (ploc) retirer le parser Kind2 et revenir à celui de lustrec
137
*** To be done
138
**** Court terme
139
- (CG) etendre la syntaxe pour coller à la definition donnée ci-dessus
140
  - lexeur/parseur lustreSpec + document latex de grammaire
141
- repartir la branche acsl2018 qui contient la normalisation des eexpr
142
  - le refaire compiler
143
  - merger avec unstable 
144
- transformer cette normalisation pour partager les definitions locales de
145
  variables dans le noeud de spec, aka contract
146

    
147
**** Apres
148
- developper dans les backends
149
  - C
150
  - EMF
151
  - LustreV
152

    
153
* TODO refactoring + doc
154
- separate lustre types from machine types in different files
155
- split basic libs into backend specific files
156
- define mli for core steps: normalization and machine code
157
- define mli for lustre_type and machine_type (Garion)
158

    
159
* TODO
160
** include files
161
** main function
162
*** add a clean test to forbid array arguments for main node
163
    (no available input/output methods)
164
** test suite
165
*** for complex dependency graphs (notably mem/mem cyclic dependencies)
166
*** for clocks
167
*** for arrays (non-generic nodes)
168
** compare with lus2c (verimag)
169
** extension
170
*** array access: done
171
*** add an option to dynamically check array accesses: done
172
*** power operator: done
173
*** automaton
174
*** annotations to ACSL
175
** init checking
176
*** to be done !!!
177
** normalization
178
*** sub-expression sharing seems to be not totally working: fixed
179
*** improve behavior for power and access operators:done
180
*** more type-directed normalization (notably to improve code gen for arrays): done
181
*** reuse of dead vars instead of systematically allocating new local vars
182
*** add a clean test for used but undefined nodes
183
** typing
184
*** correct typing of arith ops (real/int with subtyping ?)
185
*** display array dimensions with correct names: done
186
*** clocks must not be static inputs: done
187
** clock calculus
188
*** extension from named clocks to valued clocks ?
189
*** static inputs should be polymorphic, as global constants are: done
190

    
191
* Horn backend
192
** enum types for automaton
193
   - issues with MBranches and clocks
194
     - control-on-clock generates a "if cond then expr else nothing
195
     - it has to be expressed in a functional way to enable its expression as
196
       horn
197

    
198

    
199
-  The issue seems mainly to lie in the out = f(in) every cond
200
   this generates the follwoingg imperative statements
201
   if cond then f_reset(*mem) else {(nothing, ie. not reset)}
202
   f_step(in,*put,*mem)
203

    
204
   In the machine code, this is done by generating the sequence of 2 instructions
205
   1. if cond then MReset() else {}  (* creation of a conditional statement *)
206
   2. MStep()
207

    
208
- For Xavier: Syntactically, how could you "reset" an arrow? When we see an
209
  Expr_arrow, we introduce a MReset instance to the set of instruction on the
210
  reset function of the current node, but is there any mean to do it with
211
  "every" ?
212

    
213

    
214

    
215

    
216
x = expr when c
217

    
218
if c then
219
  x= expr
220

    
221
else {}
222

    
223
x = if c then expr else x