diff --git a/lv6-ref-man/lv6-ref-man.tex b/lv6-ref-man/lv6-ref-man.tex index 07a8d006480515c887e7bd7fb7770f6b1a6fd382..8b9f7327e4c3e22971f16a4dbc97be623df9df33 100644 --- a/lv6-ref-man/lv6-ref-man.tex +++ b/lv6-ref-man/lv6-ref-man.tex @@ -752,9 +752,10 @@ BIN8::binary}). So we distinguish between \sx{Ident}, and \section{Functions and Nodes} -The main way of structuring Lustre equations is via {\em nodes}. A -Lustre node is made of an interface (input/output declarations) and a -set of equations defining the outputs. +The main way of structuring Lustre equations is via {\em nodes}. A +memoryless node can be declared a {\em function}. A Lustre node is +made of an interface (input/output declarations) and a set of +equations defining the outputs. @@ -762,14 +763,9 @@ set of equations defining the outputs. \newcommand{\syntaxNode}{ \begin{grammarrule} \begin{tabular}{lcl} -\sxDef{Function\_Decl} \is \sx{Function\_Header} [\sx{FN\_Body}] -\\ -\sxDef{Function\_Header} \is \lx{function} \lx{(} \sx{FN\_Params} \lx{)} -\\ && \mysp \lx{returns} \lx{(}\sx{FN\_Params} \lx{)} \prag\ \lx{;} -\\ \sxDef{Node\_Decl} \is \sx{Node\_Header} [ \sx{FN\_Body} ] \\ -\sxDef{Node\_Header} \is \lx{node} \lx{(} \sx{FN\_Params} \lx{)} +\sxDef{Node\_Header} \is [ \lx{unsafe} ] [ \lx{extern} ] (\lx{node} \sor \lx{function}) \lx{(} \sx{FN\_Params} \lx{)} \\ && \mysp \lx{returns} \lx{(}\sx{FN\_Params} \lx{)} \prag\ \lx{;} \\ \sxDef{FN\_Params} \is \sx{Var\_Decl\_List} @@ -798,16 +794,49 @@ set of equations defining the outputs. \begin{example}[Node] \begin{alltt} -\kwd{node} foo(A:int, B:bool, C: real) \kwd{returns} (X:int, Y: real) +\kwd{node} sum(A:int) \kwd{returns} (S:int) +\kwd{let} + S=A+(0->pre(S)); +\kwd{tel} +\kwd{function} plus(A,B:int) \kwd{returns} (X:int) \kwd{let} - ... + X=A+B; \kwd{tel} \end{alltt} \end{example} -XXX definir extern +Functions and nodes can be extern, in which case they should be +preceeded by the \kwd{extern} keyword, and have an empty body. Of +course if an extern entity is declared as a function while it has +memory, +% , or performs side effects, +the behavior of the whole program is unpredictable. + +\begin{example}[Extern Nodes] +\begin{alltt} +\kwd{extern} \kwd{node} foo\_with\_mem(A:int, B:bool, C: real) \kwd{returns} (X:int, Y: real); +\kwd{extern} \kwd{function} sin(A:real) \kwd{returns} (sinx: real); +\end{alltt} + +\end{example} + + +Extern nodes that performs side-effects should be declared as unsafe. +A node that uses unsafe node is unsafe (a warning is emitted if a +node is unsafe while it is not declared as such). + +\begin{example}[Unsafe Nodes] +\begin{alltt} +\kwd{unsafe} \kwd{extern} \kwd{node} rand() \kwd{returns} (R: real); +\kwd{unsafe} \kwd{node} randr(r:real) \kwd{returns} (R: int); +let + R = r*rand(); +tel +\end{alltt} + +\end{example} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% diff --git a/src/astCore.ml b/src/astCore.ml index f4f3ddb453ed35c03ce55d29b72892bd1649b72e..91cea96cac34fc3e910d6fdd797c28cb4a72504e 100644 --- a/src/astCore.ml +++ b/src/astCore.ml @@ -1,4 +1,4 @@ -(* Time-stamp: <modified the 26/08/2014 (at 16:06) by Erwan Jahier> *) +(* Time-stamp: <modified the 19/01/2015 (at 16:26) by Erwan Jahier> *) (** (Raw) Abstract syntax tree of source Lustre Core programs. *) @@ -31,7 +31,7 @@ and node_info = { loc_consts : (Lxm.t * const_info) list; def : node_def; has_mem : bool; - is_safe : bool; + is_safe : bool; (* safe <=> no side-effect are performed *) } and static_param = diff --git a/src/lv6lexer.mll b/src/lv6lexer.mll index e736870c7ae7b34f807e11476f89cc209405e380..7cbdddb71cbdd72e8bcd20673323088dbc38b412 100644 --- a/src/lv6lexer.mll +++ b/src/lv6lexer.mll @@ -23,6 +23,7 @@ let unget_lexbuf lb = (* table des mots-clé *) let keywords = Hashtbl.create 50 ;; Hashtbl.add keywords "extern" (function x -> TK_EXTERN x) ;; +Hashtbl.add keywords "unsafe" (function x -> TK_UNSAFE x) ;; Hashtbl.add keywords "and" (function x -> TK_AND x) ;; Hashtbl.add keywords "assert" (function x -> TK_ASSERT x) ;; @@ -79,6 +80,7 @@ let token_code tk = ( TK_EOF -> ("TK_EOF" , Lxm.dummy "eof") | TK_ERROR lxm -> ("TK_ERROR" , lxm) | TK_EXTERN lxm -> ("TK_EXTERN" , lxm) + | TK_UNSAFE lxm -> ("TK_UNSAFE" , lxm) | TK_AND lxm -> ("TK_AND" , lxm) | TK_ARROW lxm -> ("TK_ARROW" , lxm) | TK_ASSERT lxm -> ("TK_ASSERT" , lxm) diff --git a/src/lv6parser.mly b/src/lv6parser.mly index 24eb7966bce665313b10a6016eb0cd8a42990d82..c0aaba1c240c83dbe9399116afaebb254951e9d0 100644 --- a/src/lv6parser.mly +++ b/src/lv6parser.mly @@ -21,6 +21,7 @@ open Lv6parserUtils %token <Lxm.t> TK_ERROR %token <Lxm.t> TK_EXTERN +%token <Lxm.t> TK_UNSAFE %token <Lxm.t> TK_AND %token <Lxm.t> TK_ARROW @@ -220,14 +221,23 @@ Provide: $2 } /* noeud abstrait */ +| TK_UNSAFE TK_NODE Ident Params TK_RETURNS Params + { + treat_abstract_node true true $3 $4 $6 + } + /* fonction abstraite */ | TK_NODE Ident Params TK_RETURNS Params { - treat_abstract_node true $2 $3 $5 + treat_abstract_node false true $2 $3 $5 } /* fonction abstraite */ +| TK_UNSAFE TK_FUNCTION Ident Params TK_RETURNS Params + { + treat_abstract_node true false $3 $4 $6 + } | TK_FUNCTION Ident Params TK_RETURNS Params { - treat_abstract_node false $2 $3 $5 + treat_abstract_node false false $2 $3 $5 } /* type abstrait... */ | TK_TYPE OneTypeDecl @@ -514,9 +524,13 @@ Type: ExtNodeDecl: TK_EXTERN TK_FUNCTION Ident Params TK_RETURNS Params OptSemicol - { treat_external_node false $3 $4 $6 } + { treat_external_node false false $3 $4 $6 } +| TK_UNSAFE TK_EXTERN TK_FUNCTION Ident Params TK_RETURNS Params OptSemicol + { treat_external_node true false $4 $5 $7 } | TK_EXTERN TK_NODE Ident Params TK_RETURNS Params OptSemicol - { treat_external_node true $3 $4 $6 } + { treat_external_node false true $3 $4 $6 } +| TK_UNSAFE TK_EXTERN TK_NODE Ident Params TK_RETURNS Params OptSemicol + { treat_external_node true true $4 $5 $7 } ; /* noeuds */ @@ -526,14 +540,24 @@ NodeDecl: LocalNode {}; LocalNode: TK_NODE Ident StaticParams Params TK_RETURNS Params OptSemicol LocalDecls Body OptEndNode - { treat_node_decl true $2 $3 $4 $6 $8 (fst $9) (snd $9) } + { treat_node_decl false true $2 $3 $4 $6 $8 (fst $9) (snd $9) } | TK_FUNCTION Ident StaticParams Params TK_RETURNS Params OptSemicol LocalDecls Body OptEndNode - { treat_node_decl false $2 $3 $4 $6 $8 (fst $9) (snd $9) } + { treat_node_decl false false $2 $3 $4 $6 $8 (fst $9) (snd $9) } | TK_NODE Ident StaticParams NodeProfileOpt TK_EQ EffectiveNode OptSemicol - { treat_node_alias true $2 $3 $4 $6 } + { treat_node_alias false true $2 $3 $4 $6 } | TK_FUNCTION Ident StaticParams NodeProfileOpt TK_EQ EffectiveNode OptSemicol - { treat_node_alias false $2 $3 $4 $6 } + { treat_node_alias false false $2 $3 $4 $6 } + | TK_UNSAFE TK_NODE Ident StaticParams Params TK_RETURNS Params OptSemicol + LocalDecls Body OptEndNode + { treat_node_decl true true $3 $4 $5 $7 $9 (fst $10) (snd $10) } + | TK_UNSAFE TK_FUNCTION Ident StaticParams Params TK_RETURNS Params OptSemicol + LocalDecls Body OptEndNode + { treat_node_decl true false $3 $4 $5 $7 $9 (fst $10) (snd $10) } + | TK_UNSAFE TK_NODE Ident StaticParams NodeProfileOpt TK_EQ EffectiveNode OptSemicol + { treat_node_alias true true $3 $4 $5 $7 } + | TK_UNSAFE TK_FUNCTION Ident StaticParams NodeProfileOpt TK_EQ EffectiveNode OptSemicol + { treat_node_alias true false $3 $4 $5 $7 } ; NodeProfileOpt : diff --git a/src/lv6parserUtils.ml b/src/lv6parserUtils.ml index 6335758c852f910df9178512944d3214f5eabf09..eca40500e140c2ec967e3d73d97a8522e8b856ec 100644 --- a/src/lv6parserUtils.ml +++ b/src/lv6parserUtils.ml @@ -1,4 +1,4 @@ -(* Time-stamp: <modified the 11/04/2013 (at 15:48) by Erwan Jahier> *) +(* Time-stamp: <modified the 20/01/2015 (at 14:23) by Erwan Jahier> *) (** *) @@ -370,7 +370,7 @@ let (clocked_ids_to_var_infos : var_nature -> les déclarations locales comportent : - une liste de vars * une liste de consts *) -let (treat_node_decl : bool -> Lxm.t -> static_param srcflagged list -> +let (treat_node_decl : bool -> bool -> Lxm.t -> static_param srcflagged list -> clocked_ids list (* entrées *) -> clocked_ids list (* sorties *) -> (* clocked_ids list (* locales *) -> *) @@ -379,7 +379,7 @@ let (treat_node_decl : bool -> Lxm.t -> static_param srcflagged list -> (eq_info srcflagged) list (* liste des equations *) -> unit ) = - fun has_memory nlxm statics indefs outdefs locdecls asserts eqs -> + fun is_unsafe has_memory nlxm statics indefs outdefs locdecls asserts eqs -> let (locdefs, locconsts) = locdecls in let vtable = Hashtbl.create 50 in let rec (treat_vars : clocked_ids list -> var_nature -> var_info srcflagged list) = @@ -415,7 +415,7 @@ let (treat_node_decl : bool -> Lxm.t -> static_param srcflagged list -> loc_consts = locconsts; def = Body { asserts = asserts ; eqs = eqs }; has_mem = has_memory; - is_safe = true; + is_safe = not is_unsafe; } in add_info node_table "node" nlxm ninfo; @@ -423,10 +423,10 @@ let (treat_node_decl : bool -> Lxm.t -> static_param srcflagged list -> (**********************************************************************************) -let (treat_node_alias : bool -> Lxm.t -> static_param srcflagged list -> +let (treat_node_alias : bool -> bool -> Lxm.t -> static_param srcflagged list -> (var_info srcflagged list * var_info srcflagged list) option -> node_exp srcflagged -> unit) = - fun has_memory nlxm statics node_profile value -> + fun is_unsafe has_memory nlxm statics node_profile value -> let nstr = Lxm.id nlxm in let vars = match node_profile with @@ -440,7 +440,7 @@ let (treat_node_alias : bool -> Lxm.t -> static_param srcflagged list -> loc_consts = []; def = Alias (flagit (CALL_n value) value.src); has_mem = has_memory; - is_safe = true; + is_safe = not is_unsafe ; } in add_info node_table "(alias) node" nlxm ninfo; @@ -452,7 +452,7 @@ let (treat_node_alias : bool -> Lxm.t -> static_param srcflagged list -> (* Traitement d'un noeud abstrait *) let treat_abstract_or_extern_node_do (* cf the profile of [treat_abstract_node] *) - has_memory lxm inpars outpars is_abstract = + is_unsafe has_memory lxm inpars outpars is_abstract = let (invars, outvars : var_info srcflagged list * var_info srcflagged list) = clocked_ids_to_var_infos VarInput inpars, clocked_ids_to_var_infos VarOutput outpars @@ -465,31 +465,31 @@ let treat_abstract_or_extern_node_do (* cf the profile of [treat_abstract_node] loc_consts = []; def = if is_abstract then Abstract else Extern; has_mem = has_memory; - is_safe = true; + is_safe = not is_unsafe; } in xn -let (treat_abstract_node : bool -> Lxm.t -> +let (treat_abstract_node : bool -> bool -> Lxm.t -> (((Lxm.t list) * type_exp) list * AstCore.clock_exp) list -> (((Lxm.t list) * type_exp) list * AstCore.clock_exp) list -> item_info Lxm.srcflagged) = - fun has_memory lxm inpars outpars -> + fun is_unsafe has_memory lxm inpars outpars -> Lxm.flagit - (NodeInfo (treat_abstract_or_extern_node_do has_memory lxm inpars outpars true)) + (NodeInfo (treat_abstract_or_extern_node_do is_unsafe has_memory lxm inpars outpars true)) lxm (**********************************************************************************) -let (treat_external_node : bool -> Lxm.t -> +let (treat_external_node : bool -> bool -> Lxm.t -> (((Lxm.t list) * type_exp) list * AstCore.clock_exp) list -> (((Lxm.t list) * type_exp) list * AstCore.clock_exp) list -> unit ) = - fun has_memory ext_nodelxm inpars outpars -> + fun is_unsafe has_memory ext_nodelxm inpars outpars -> let ninfo = treat_abstract_or_extern_node_do (* external nodes look like abstract nodes indeed *) - has_memory ext_nodelxm inpars outpars false + is_unsafe has_memory ext_nodelxm inpars outpars false in let statics = [] in (* no static args for external node (for now at least) *) add_info node_table "(extern) node" ext_nodelxm ninfo ; diff --git a/src/lv6version.ml b/src/lv6version.ml index d361ce2c75a81e56d1b5d089df064f7e6d4686be..646b3c1bcb3e9df1b75fc05f2849a93855fbe127 100644 --- a/src/lv6version.ml +++ b/src/lv6version.ml @@ -1,7 +1,7 @@ (** Automatically generated from Makefile *) let tool = "lus2lic" let branch = "master" -let commit = "547" -let sha_1 = "79e85ff20f718dd61a30e2425983bd9aadc4424f" +let commit = "548" +let sha_1 = "d783b03e3d8467fbe37848dfce67e3e26e5dea71" let str = (branch ^ "." ^ commit ^ " (" ^ sha_1 ^ ")") let maintainer = "jahier@imag.fr" diff --git a/test/lus2lic.sum b/test/lus2lic.sum index d0adb9de2fd27bf62e6a46f69272bf6cde5f032a..10373f66a23dcf18540da5c8e9dbcceaf0a4588b 100644 --- a/test/lus2lic.sum +++ b/test/lus2lic.sum @@ -1,5 +1,5 @@ ==> lus2lic0.sum <== -Test Run By jahier on Mon Jan 19 16:04:58 +Test Run By jahier on Tue Jan 20 15:03:20 Native configuration is x86_64-unknown-linux-gnu === lus2lic0 tests === @@ -63,7 +63,7 @@ XFAIL: Test bad programs (assert): test_lus2lic_no_node should_fail/assert/lecte XFAIL: Test bad programs (assert): test_lus2lic_no_node should_fail/assert/s.lus ==> lus2lic1.sum <== -Test Run By jahier on Mon Jan 19 16:05:02 +Test Run By jahier on Tue Jan 20 15:03:33 Native configuration is x86_64-unknown-linux-gnu === lus2lic1 tests === @@ -397,7 +397,7 @@ PASS: gcc -o multipar.exec multipar_multipar.c multipar_multipar_loop.c PASS: /home/jahier/lus2lic/test/../utils/compare_exec_and_2c multipar.lus {} ==> lus2lic2.sum <== -Test Run By jahier on Mon Jan 19 16:05:04 +Test Run By jahier on Tue Jan 20 15:04:30 Native configuration is x86_64-unknown-linux-gnu === lus2lic2 tests === @@ -727,7 +727,7 @@ PASS: gcc -o zzz2.exec zzz2_zzz2.c zzz2_zzz2_loop.c PASS: /home/jahier/lus2lic/test/../utils/compare_exec_and_2c zzz2.lus {} ==> lus2lic3.sum <== -Test Run By jahier on Mon Jan 19 16:05:00 +Test Run By jahier on Tue Jan 20 15:05:48 Native configuration is x86_64-unknown-linux-gnu === lus2lic3 tests === @@ -1230,7 +1230,7 @@ PASS: ./myec2c {-o multipar.c multipar.ec} PASS: /home/jahier/lus2lic/test/../utils/test_lus2lic_no_node multipar.lus {} ==> lus2lic4.sum <== -Test Run By jahier on Mon Jan 19 16:05:06 +Test Run By jahier on Tue Jan 20 15:06:39 Native configuration is x86_64-unknown-linux-gnu === lus2lic4 tests === @@ -1726,14 +1726,12 @@ PASS: /home/jahier/lus2lic/test/../utils/test_lus2lic_no_node zzz2.lus {} # of unexpected failures 3 =============================== # Total number of failures: 14 -lus2lic0.log:testcase ./lus2lic.tests/test0.exp completed in 6 seconds -lus2lic1.log:testcase ./lus2lic.tests/test1.exp completed in 48 seconds -lus2lic2.log:testcase ./lus2lic.tests/test2.exp completed in 74 seconds -lus2lic3.log:testcase ./lus2lic.tests/test3.exp completed in 48 seconds -lus2lic4.log:testcase ./lus2lic.tests/test4.exp completed in 82 seconds +lus2lic0.log:testcase ./lus2lic.tests/test0.exp completed in 10 seconds +lus2lic1.log:testcase ./lus2lic.tests/test1.exp completed in 56 seconds +lus2lic2.log:testcase ./lus2lic.tests/test2.exp completed in 78 seconds +lus2lic3.log:testcase ./lus2lic.tests/test3.exp completed in 50 seconds +lus2lic4.log:testcase ./lus2lic.tests/test4.exp completed in 81 seconds * Ref time: -0.04user 0.10system 4:11.13elapsed 0%CPU (0avgtext+0avgdata 3016maxresident)k -0inputs+0outputs (0major+14906minor)pagefaults 0swaps +0.05user 0.09system 4:40.76elapsed 0%CPU (0avgtext+0avgdata 3016maxresident)k +0inputs+0outputs (0major+14902minor)pagefaults 0swaps * Quick time (-j 4): -0.06user 0.08system 1:30.70elapsed 0%CPU (0avgtext+0avgdata 3016maxresident)k -0inputs+0outputs (0major+14923minor)pagefaults 0swaps diff --git a/test/lus2lic.time b/test/lus2lic.time index a84daae2caf50d1b0b637a3706bb5d7bc2943c3a..ff4b191bf3c50a165a7bc35a328be150f9a41c30 100644 --- a/test/lus2lic.time +++ b/test/lus2lic.time @@ -1,11 +1,9 @@ -lus2lic0.log:testcase ./lus2lic.tests/test0.exp completed in 6 seconds -lus2lic1.log:testcase ./lus2lic.tests/test1.exp completed in 48 seconds -lus2lic2.log:testcase ./lus2lic.tests/test2.exp completed in 74 seconds -lus2lic3.log:testcase ./lus2lic.tests/test3.exp completed in 48 seconds -lus2lic4.log:testcase ./lus2lic.tests/test4.exp completed in 82 seconds +lus2lic0.log:testcase ./lus2lic.tests/test0.exp completed in 10 seconds +lus2lic1.log:testcase ./lus2lic.tests/test1.exp completed in 56 seconds +lus2lic2.log:testcase ./lus2lic.tests/test2.exp completed in 78 seconds +lus2lic3.log:testcase ./lus2lic.tests/test3.exp completed in 50 seconds +lus2lic4.log:testcase ./lus2lic.tests/test4.exp completed in 81 seconds * Ref time: -0.04user 0.10system 4:11.13elapsed 0%CPU (0avgtext+0avgdata 3016maxresident)k -0inputs+0outputs (0major+14906minor)pagefaults 0swaps +0.05user 0.09system 4:40.76elapsed 0%CPU (0avgtext+0avgdata 3016maxresident)k +0inputs+0outputs (0major+14902minor)pagefaults 0swaps * Quick time (-j 4): -0.06user 0.08system 1:30.70elapsed 0%CPU (0avgtext+0avgdata 3016maxresident)k -0inputs+0outputs (0major+14923minor)pagefaults 0swaps