Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / TODO.org @ f5c36991

History | View | Annotate | Download (3.83 KB)

1
* TODO
2
** include files
3
** main function
4
*** add a clean test to forbid array arguments for main node
5
    (no available input/output methods)
6
** test suite
7
*** for complex dependency graphs (notably mem/mem cyclic dependencies)
8
*** for clocks
9
*** for arrays (non-generic nodes)
10
** compare with lus2c (verimag)
11
** extension
12
*** array access: done
13
*** add an option to dynamically check array accesses: done
14
*** power operator: done
15
*** automaton
16
*** annotations to ACSL
17
** init checking
18
*** to be done !!!
19
** normalization
20
*** sub-expression sharing seems to be not totally working: fixed
21
*** improve behavior for power and access operators:done
22
*** more type-directed normalization (notably to improve code gen for arrays): done
23
*** reuse of dead vars instead of systematically allocating new local vars
24
*** add a clean test for used but undefined nodes
25
** typing
26
*** correct typing of arith ops (real/int with subtyping ?)
27
*** display array dimensions with correct names: done
28
*** clocks must not be static inputs: done
29
** clock calculus
30
*** extension from named clocks to valued clocks ?
31
*** static inputs should be polymorphic, as global constants are: done
32
* TODO Revalidation of k-inductive properties at code level
33
We identified the following items to be taken care of to reach the fully
34
working prototype
35
** How to access to ACSL datatypes and printers
36
*** Problematics
37
we have to choose one of those options or create a new one
38
**** option1 (ugly)
39
     - link directly with the cmx in /usr/loca/share/framac
40
     - see example
41
     - problem with namespace (all framac modules may conflict with lustrec
42
       modules)
43
     - but good option to start to code (access to types and printers)
44
**** option 2: create a standalone framac.cmxa archive file
45
     - requires to compile frama-c with -pack framac
46
     - problem today with framac compilation
47
     - meeting with CEA to see if they want to add this feature
48
**** option3: as a plugin of frama-c
49
     - depending on the configure option, create one or two tools
50
       - lustrec without annotations (current version)
51
       - lustrec with ACSL as a frama-c plugin
52
	 eg. frama-c -lustrec args ....
53
     - question on the entry point: single bash script that, depending on
54
       options, redirects to the binary or the framac plugin
55
** Compilation of lustre nodes as ACSL predicate
56
*** Problematics
57
   - expressed over pure struct (no pointers, static struct)
58
   - generation of static struct
59
   - generation of init and step (no pointers for output, nor mem state)
60
     step(in, out, memstate_before, memstate_after)
61
**** how do to it properly
62
     - for the moment it is a sort of hack within the C backend
63
     - shoudln't it be more like a specific ACSL backend that will be evaluated
64
       only on selected nodes
65
     - for example a frama-c plugin could call the "compiler" twice, 
66
       - one to generate an ACSL encoding for (all|a selection of) nodes
67
       - one to generate annotated C code, knowing that those predicates init
68
         and step and static struct exist
69

    
70

    
71
** Stateful observers
72
*** Problematics
73
   - generate (ghost) code to express the memories as additional (ghost) fields
74
     of the node struct
75
   - introduce (ghost) code update for those memories
76
    
77
     
78
** Relationship between pointer based struct and static struct
79
** Annotation of C instructions with live variables (as in optim/*.c files)
80
*** Problematics
81
   - while iterating through scheduled list of instructions, introduce the
82
     assert predicate_X; and keep its definition in an environement.
83
   - this env of predicate has to be printed in the header of the source file
84
   - need the support of Xavier for that (clocks related stuff)
85
   - xavier, does it need to be done while doing the dead variables analysis ?
86
     I (pl) undertood that it was independant and generic
87
** Prove the ACSL predicate Pre and Post as k-inductive wrt predicates Init and Step