CristalCaveGem » LustreC

* Cocospec integration

** Objective

Enable the parsing of cocospec in comments. The syntax is the one of Kind2 but

could be extended later.

In terms of integration within LustreC, it has to be done at all stages

- parsing/lexing

- typing

- clocking

- normalization: the cocospec lustre equations have to be normalized 

- printing

- machine code

- various backends

  - EMF

  - LustreV/Zustre

  - C code

** Open questions

The cocospec syntax is appealing for multiple aspects wrt the our previous

annotation language.

- more structure

- notion of contracts that can be imported, reused

- more expressivity: local variables within contracts (more like regular lustre

  definitions *)

But also some not-so-nice features (ploc's remarks):

- annotations next to the node header shall be before rather than after. We also

  don't want pure specification artifact as top level definition in the lustre

  file (no contract def outside comments)

  - Frama-C inspiration

    I would prefer like in framac:  

    //@ensures prop; 

    node foo (...) returns (...);

    Rather than

    node foo (...) returns (...);

    //@ensures prop; 

    While it make sense when you provide specification within the lustre file, it

    is less appropriate when specifying outside the lustre model. Eg in a lusi, #open

    spec.lusi

  - Kind2 approach

    In Kind2 they have a notion of interfaces, but they need an explicit local

    annotation linking the node to the contract

    In foo.lus we would have 

    #include foo_spec.lus

    node bar (...) returns (...);

    (*@ contract import bar_spec (in) returns (out); *)

    let  ... tel 

    In foo_spec.lus 

    contract bar_spec (..) returns (..)

  - Remote specification (in lusi)

    We would like to enable both local spec and remote ones (in a separate file).

    A solution could be to extend the lusi syntax, for example something like

    node bar (...) returns (...)

    let

      @ensures ...

      @requires ...

    tel

    Or, more generally, support contracts definition only in lusi and assigning

    contracts to nodes in the lusi or in the lus

    For example in the lusi

    contract bar_spec1 () returns ();

    let 

     ... contract 1

    tel

    contract bar_spec2 () returns ();

    let 

     ... contract 2

    tel

    node bar (...) returns (...);

    (*@ contract 

          import bar_spec1 (in) returns (out);

          import bar_spec2 (in) returns (out);

    *)

    node bar2 (...) returns (...);

    (*@ contract guarantee expr; *)

    Or with annotations before the headers

    (*@ contract 

          import bar_spec1 (in) returns (out);

          import bar_spec2 (in) returns (out);

    *)

    node bar (...) returns (...);

    (*@ contract guarantee expr; *)

    node bar2 (...) returns (...);

    In the associated lustre file

    #open my_spec.lusi

    node bar (...) returns (...)

    let

      full definition

    tel

    node bar3 (...) returns (...)

    (*@ contract my_remote contract *)

    let

      full definition

    tel

    -- a local contract

    node bar4 (...) returns (...)

    (*@ contract guarantee expr; *)

    let

      full definition

    tel

    But no contracts definition within the lustre ourside of special comments

** Current status

- Existing works in lustrec

  ensures/requires/observer in the syntax, which were parsed, typed, normalized

- Choice of placement of annotations

  - no contract in lustre only in lusi

  - in lustre file: contract attached to lustre node before the locals/let

  - in lusi file: contract attached to lustre node before the node foo ...

- Dev. choices

  - contracts rely look like imported node: a signature and a contract content attached

    - in lusi one could have an alias for contract / imported node

    - in lus similarly a top level contract could be parsed as an imported node

    - contract import would amount to concatenate contract elements

      from provided nodes or imported nodes.

** Development

*** Done

- (ploc) retirer le parser Kind2 et revenir à celui de lustrec

*** To be done

**** Court terme

- (CG) etendre la syntaxe pour coller à la definition donnée ci-dessus

  - lexeur/parseur lustreSpec + document latex de grammaire

- repartir la branche acsl2018 qui contient la normalisation des eexpr

  - le refaire compiler

  - merger avec unstable 

- transformer cette normalisation pour partager les definitions locales de

  variables dans le noeud de spec, aka contract

**** Apres

- developper dans les backends

  - C

  - EMF

  - LustreV

* Slicing

  - reprendre le slicing inlined de seal pour

  - when provided with a main node and a selection of outputs or memories

    - slice the local node

    - for each node called try to slice to the selected vars

  - could be used to analyze counterexamples

* TODO refactoring + doc

- separate lustre types from machine types in different files

- split basic libs into backend specific files

- define mli for core steps: normalization and machine code

- define mli for lustre_type and machine_type (Garion)

* TODO

** include files

** main function

*** add a clean test to forbid array arguments for main node

    (no available input/output methods)

** test suite

*** for complex dependency graphs (notably mem/mem cyclic dependencies)

*** for clocks

*** for arrays (non-generic nodes)

** compare with lus2c (verimag)

** extension

*** array access: done

*** add an option to dynamically check array accesses: done

*** power operator: done

*** automaton

*** annotations to ACSL

** init checking

*** to be done !!!

** normalization

*** sub-expression sharing seems to be not totally working: fixed

*** improve behavior for power and access operators:done

*** more type-directed normalization (notably to improve code gen for arrays): done

*** reuse of dead vars instead of systematically allocating new local vars

*** add a clean test for used but undefined nodes

** typing

*** correct typing of arith ops (real/int with subtyping ?)

*** display array dimensions with correct names: done

*** clocks must not be static inputs: done

** clock calculus

*** extension from named clocks to valued clocks ?

*** static inputs should be polymorphic, as global constants are: done

* Horn backend

** enum types for automaton

   - issues with MBranches and clocks

     - control-on-clock generates a "if cond then expr else nothing

     - it has to be expressed in a functional way to enable its expression as

       horn

-  The issue seems mainly to lie in the out = f(in) every cond

   this generates the follwoingg imperative statements

   if cond then f_reset(*mem) else {(nothing, ie. not reset)}

   f_step(in,*put,*mem)

   In the machine code, this is done by generating the sequence of 2 instructions

   1. if cond then MReset() else {}  (* creation of a conditional statement *)

   2. MStep()

- For Xavier: Syntactically, how could you "reset" an arrow? When we see an

  Expr_arrow, we introduce a MReset instance to the set of instruction on the

  reset function of the current node, but is there any mean to do it with

  "every" ?

x = expr when c

if c then

  x= expr

else {}

x = if c then expr else x