TODO.org

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)

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