Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / TODO.org @ 17e1d0f4

History | View | Annotate | Download (6.37 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
*** To be done
137
**** Court terme
138

    
139
- repartir la branche acsl2018 qui contient la normalisation des eexpr
140
  - le refaire compiler
141
  - merger avec unstable 
142
- transformer cette normalisation pour partager les definitions locales de
143
  variables dans le noeud de spec, aka contract
144
- retirer le parser Kind21 et revenir à celui de lustrec
145
- (CG) etendre la syntaxe pour coller à la definition donnée ci-dessus
146
  - lexeur/parseur lustreSpec + document latex de grammaire
147

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

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

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

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

    
199

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

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

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

    
214

    
215

    
216

    
217
x = expr when c
218

    
219
if c then
220
  x= expr
221

    
222
else {}
223

    
224
x = if c then expr else x