Skip to content

Latest commit

 

History

History
341 lines (278 loc) · 11.1 KB

TODO.org

File metadata and controls

341 lines (278 loc) · 11.1 KB

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

refactoring + doc

  • DONE separate lustre types from machine types in different files
  • DONE split basic libs into backend specific files
  • DONE define mli for core steps: normalization and machine code
  • define mli for lustre_type and machine_type (Garion)

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

Seal

The Seal library should be available from LustreV

lustrev -seal -node foo bar.lus

shall inline completely the node foo in bar.lus and compile it as a piecewise system:

  • Memories have to be identified and one needs to separate the update of the memories and the production of the output.
  • The update block should be normalized so that any ite occuring in the definition of a memory should not define a local flow used in basic operations. In other words, the definitions should look like mem_x = if g then e1 else e2 where e1 and e2 are either ite expression or expressions without ite. As soon as a not-ite expression is selected it cannot depend on the output of an ite.

In a first step this normalized update shall be printed in stdout. Later it will associated to a SEAL datastructure through SEAL API.

Algorithm

1. Computation of update block

  • First we inline the node
  • After normalization the memories are the variables defined by a pre
  • Do we have to deal with arrows and reset?
  • Develop a function to perform slicing. Restrict the node eqs to the ones used in these pre defs.
  • one can also slice the expressions on the output variables

2. Normalization: piecewise system

ie. all ite pushed at the beginning

  • use the scheduling to obtain the dependencies amongs eqs
  • one can then iterate through eqs from the bottom to the top if the eq looks like x = if g then e1 else e2 then tag x as ite(g,e1,e2) if the parent expr y = if g2 then x else … make

More general use

Some ideas

  • One could request multiple nodes: how to deal with these? Acting as as many calls to the basic procedure?
  • Shall we keep the flatten update structure to the node? Another property on input could be propagated.
  • The analysis will depend on bounds on input flows. Can we specialize the update blocks based on input values, ie. disabling some branches of the ite-tree?

list

Salsa

Lusic

Lusic can be generated either from lusi files or from lus files They shall contain at least

  • the complete definitions of types
  • the complete definition of constants
  • the list of nodes and their types/clocks
  • the complete definition of specification components:
    • either defined in lusi as
      • node spec: attached to a node
      • contract: expressed as an imported node with a spec
    • or defined in the lus
      • node spec
      • contract defined in a comment
  • some compilation related information if compiled from a lusi

What happen when we compile first a lusi and then the lus file?

  • types of the lus node are checked wrt the ones available in the lusic (coming from the lusi)
  • do we want to update the lusic for additional specification defined in the lus, or do we assume that the lusi masks the spec artifacts defined in the lus file ?
  • do we want to embeded the node content in the compiled lusic, updating it?

When opening another module, one loads the lusic file

  • if compilation directives are provided then can support the generation of the Makefile, linking proper libs.
  • if the lusic contains node content one may use these to perform inlining if asked by the users or in certain configurations
    • decision: lusic do not contain actual code: #include shall allow to include external lustre copde and inline it as if it was defined in the current file

We would like to know whether a declared node:

  • is an external function, possibly specified but not associated eventually to some lustre node. Ie type conversion functions, array functions with loops, …
  • is a pure specification function/node/contract
  • is just a signature(+spec) of a regular node

Contracts in lusi are compiled as imported node with spec. We could keep the info that they will not be associated to some real code. While a regular imported node could.

Now the question is how to tag a lusi file to explicitely state that no lus file will be associated to it. May be one can provide a link to the backend implemented. Let say that this lusi file can be used for the C backend then a C file should be provided. Do we want to mention it in the lusi file?