From 499a3f474c0f9672a9b0c2898d05332538e0c0e4 Mon Sep 17 00:00:00 2001
From: Erwan Jahier <jahier@imag.fr>
Date: Wed, 22 May 2013 14:46:03 +0200
Subject: [PATCH] Fix a bug when expanding nodes (-en). A Node that calls a
node that itself calls another node on a non-trivial clock (i.e., using a
when) was not producing correct code.
I've fixed this by performing the fix-point on nodes rather than on
equations. Indeed its more natural and efficient, and it avoid the
problem above. However, I did not really fix the problem, but just
turn around it. All tests seems to work fine though.
nb : #FAILS=81->80 (and -2 unresolved, but because I fixed the prog)
---
src/l2lExpandNodes.ml | 162 +++++++++---------
src/licPrg.mli | 4 +-
src/rif_base.ml | 3 +-
test/Makefile | 1 +
test/lus2lic.sum | 16 +-
test/lus2lic.time | 4 +-
test/should_work/ck5.lus | 5 +-
.../long_et_stupide_nom_de_noeud.lus | 2 +-
test/site.exp | 4 +
todo.org | 19 ++
todo.org_archive | 11 ++
11 files changed, 140 insertions(+), 91 deletions(-)
diff --git a/src/l2lExpandNodes.ml b/src/l2lExpandNodes.ml
index dccfcb71..e6597dc5 100644
--- a/src/l2lExpandNodes.ml
+++ b/src/l2lExpandNodes.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 24/04/2013 (at 17:42) by Erwan Jahier> *)
+(* Time-stamp: <modified the 22/05/2013 (at 11:17) by Erwan Jahier> *)
open Lxm
@@ -9,10 +9,9 @@ let dbg = (Verbose.get_flag "en")
(* pack useful info into a single struct *)
type local_ctx = {
- idgen : LicPrg.id_generator;
- node : Lic.node_exp;
- prg : LicPrg.t;
- nodes : string list; (* nodes to repserve from expansion *)
+ init_prg : LicPrg.t; (* nodes before expansion *)
+ curr_prg : LicPrg.t; (* nodes that have already been expanded *)
+ nodes : string list; (* nodes to preserve from expansion *)
}
(********************************************************************************)
@@ -119,6 +118,8 @@ let mk_loc_subst l1 l2 = List.combine (List.map (fun v -> v.var_name_eff) l1) l2
(1) the assertions
(2) the new equations
(3) the fresh variables
+
+The fix-point is performed on nodes.
*)
type acc =
@@ -204,32 +205,39 @@ let (mk_output_subst : local_ctx -> Lxm.t -> var_info list -> Lic.left list -> c
vl
leftl
-let rec (expand_eq : local_ctx -> acc -> Lic.eq_info Lxm.srcflagged -> acc) =
- fun lctx (asserts, eqs, locs) { src = lxm_eq ; it = eq } ->
+let rec (expand_eq : local_ctx * acc -> Lic.eq_info Lxm.srcflagged -> local_ctx * acc) =
+ fun (lctx, (asserts, eqs, locs)) { src = lxm_eq ; it = eq } ->
match expand_eq_aux lctx eq with
- | None -> asserts, { src = lxm_eq ; it = eq }::eqs, locs
- | Some(nasserts, neqs, nlocs) ->
- List.rev_append nasserts asserts,
- List.rev_append neqs eqs,
- List.rev_append nlocs locs
+ | lctx, None -> lctx, (asserts, { src = lxm_eq ; it = eq }::eqs, locs)
+ | lctx, Some(nasserts, neqs, nlocs) ->
+ (lctx,
+ (List.rev_append nasserts asserts,
+ List.rev_append neqs eqs,
+ List.rev_append nlocs locs))
-and (expand_eq_aux: local_ctx -> Lic.eq_info -> acc option)=
+and (expand_eq_aux: local_ctx -> Lic.eq_info -> local_ctx * acc option)=
fun lctx (lhs,ve) ->
match ve.ve_core with
| CallByPosLic( { it = Lic.CALL node_key ; src = lxm }, vel) ->
- let node =
- match LicPrg.find_node lctx.prg node_key.it with
- | Some n -> n
- | None ->
- prerr_string (
- "*** "^ (LicDump.string_of_node_key_rec false node_key.it) ^" not defined.\n" ^
- "*** Defined nodes are:"^
- (String.concat ",\n"
- (List.map (fun (nk,_) -> "\""^LicDump.string_of_node_key_rec false nk^"\"")
- (LicPrg.list_nodes lctx.prg)))
- );
- flush stderr;
- assert false
+ let lctx, node =
+ match LicPrg.find_node lctx.curr_prg node_key.it with
+ | Some node -> lctx, node
+ | None -> (* node has not been expanded yet: fix point! *)
+ let raw_node =
+ match LicPrg.find_node lctx.init_prg node_key.it with
+ | Some n -> n
+ | None ->
+ prerr_string (
+ "*** "^ (LicDump.string_of_node_key_rec false node_key.it) ^" not defined.\n" ^
+ "*** Defined nodes are:"^
+ (String.concat ",\n"
+ (List.map (fun (nk,_) -> "\""^LicDump.string_of_node_key_rec false nk^"\"")
+ (LicPrg.list_nodes lctx.init_prg)))
+ );
+ flush stderr;
+ assert false
+ in
+ expand_node lctx raw_node
in
let node = flagit node lxm in
let node = match node.it.def_eff with
@@ -240,10 +248,10 @@ and (expand_eq_aux: local_ctx -> Lic.eq_info -> acc option)=
let nname = Ident.string_of_long2 (fst node.it.node_key_eff) in
(List.mem nname lctx.nodes)
then
- None
+ lctx, None
else
(match get_node_body lctx node.it with
- | None -> None
+ | None -> lctx, None
| Some node_body ->
let node_eqs = node_body.eqs_eff
and asserts = node_body.asserts_eff in
@@ -272,20 +280,18 @@ and (expand_eq_aux: local_ctx -> Lic.eq_info -> acc option)=
{ v with var_clock_eff = id, subst_in_clock s clk })
fresh_locs
in
- let acc = match acc with (a,b,c) -> (a,b,c@fresh_locs) in
let node_eqs = List.map (substitute s) node_eqs in
let subst_assert x = Lxm.flagit (subst_in_val_exp s x.it) x.src in
- let asserts = List.map subst_assert asserts in
- let acc = List.fold_left (expand_eq lctx) acc node_eqs in
- let acc = List.fold_left (expand_assert lctx) acc asserts in
- Some acc
+ let asserts = List.map subst_assert asserts in
+ let acc = match acc with (a,b,c) -> (a@asserts,b@node_eqs,c@fresh_locs) in
+ lctx, Some acc
)
| CallByPosLic (_, _)
| Merge (_, _)
- | CallByNameLic (_, _) -> None
+ | CallByNameLic (_, _) -> lctx, None
-and (expand_assert : local_ctx -> acc -> val_exp srcflagged -> acc) =
- fun lctx (a_acc,e_acc,v_acc) ve ->
+and (expand_assert : local_ctx * acc -> val_exp srcflagged -> local_ctx * acc) =
+ fun (lctx, (a_acc,e_acc,v_acc)) ve ->
let lxm = ve.src in
let ve = ve.it in
let clk = Ident.of_string "dummy_expand_assert", BaseLic in
@@ -298,33 +304,40 @@ and (expand_assert : local_ctx -> acc -> val_exp srcflagged -> acc) =
ve_clk = [BaseLic]
}
in
- expand_eq lctx ((Lxm.flagit nve lxm)::a_acc, e_acc, assert_var::v_acc) assert_eq
-
+ expand_eq (lctx, ((Lxm.flagit nve lxm)::a_acc, e_acc, assert_var::v_acc)) assert_eq
-
-let (node : local_ctx -> Lic.node_exp -> Lic.node_exp) =
+and (expand_node : local_ctx -> Lic.node_exp -> local_ctx * Lic.node_exp) =
fun lctx n ->
- match n.def_eff with
- | ExternLic
- | AbstractLic _ -> n
- | BodyLic b ->
- let locs = get_locals n in
- let acc = List.fold_left (expand_eq lctx) ([],[],locs) b.eqs_eff in
- let acc = List.fold_left (expand_assert lctx) acc b.asserts_eff in
- let (asserts,neqs, nv) = acc in
- let nb = {
- eqs_eff = neqs ;
- asserts_eff = asserts
- }
- in
- let res =
- { n with
- loclist_eff = Some nv;
- def_eff = BodyLic nb
- }
- in
- res
- | MetaOpLic -> n
+ match LicPrg.find_node lctx.curr_prg n.node_key_eff with
+ | Some n -> lctx, n
+ | None ->
+ let lctx, exp_node =
+ match n.def_eff with
+ | ExternLic
+ | AbstractLic _ -> lctx, n
+ | BodyLic b ->
+ let locs = get_locals n in
+ let lctx,acc = List.fold_left expand_eq (lctx, ([],[],locs)) b.eqs_eff in
+ let lctx,acc = List.fold_left expand_assert (lctx, acc) b.asserts_eff in
+ let (asserts,neqs, nv) = acc in
+ let nb = {
+ eqs_eff = neqs ;
+ asserts_eff = asserts
+ }
+ in
+ let res =
+ { n with
+ loclist_eff = Some nv;
+ def_eff = BodyLic nb
+ }
+ in
+ Verbose.exe ~flag:dbg (fun () ->
+ Printf.printf "#DBG: expand nodes of '%s'\n" (Lic.string_of_node_key n.node_key_eff));
+ lctx, res
+ | MetaOpLic -> lctx, n
+ in
+ { lctx with curr_prg = LicPrg.add_node n.node_key_eff exp_node lctx.curr_prg },
+ exp_node
(* exported *)
let (doit : string list -> LicPrg.t -> LicPrg.t) =
@@ -333,21 +346,16 @@ let (doit : string list -> LicPrg.t -> LicPrg.t) =
(** types and constants do not change *)
let outprg = LicPrg.fold_types LicPrg.add_type inprg outprg in
let outprg = LicPrg.fold_consts LicPrg.add_const inprg outprg in
+ let lctx_init = {
+ init_prg = inprg;
+ curr_prg = outprg;
+ nodes = nodes;
+ }
+ in
(** transform nodes *)
- let rec (do_node : Lic.node_key -> Lic.node_exp -> LicPrg.t -> LicPrg.t) =
- fun nk ne outprg ->
- Verbose.exe ~flag:dbg (fun () ->
- Printf.printf "#DBG: expand nodes of '%s'\n"
- (Lic.string_of_node_key nk));
- let lctx = {
- idgen = LicPrg.fresh_var_id_generator inprg ne;
- node = ne;
- prg = inprg;
- nodes = nodes;
- }
- in
- let ne = node lctx ne in
- LicPrg.add_node nk ne outprg
+ let rec (do_node : Lic.node_key -> Lic.node_exp -> local_ctx -> local_ctx) =
+ fun nk ne lctx ->
+ fst (expand_node lctx ne)
in
- let outprg = LicPrg.fold_nodes do_node inprg outprg in
- outprg
+ let lctx = LicPrg.fold_nodes do_node inprg lctx_init in
+ lctx.curr_prg
diff --git a/src/licPrg.mli b/src/licPrg.mli
index b3c313c3..42d2fff4 100644
--- a/src/licPrg.mli
+++ b/src/licPrg.mli
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 12/04/2013 (at 08:50) by Erwan Jahier> *)
+(* Time-stamp: <modified the 21/05/2013 (at 16:29) by Erwan Jahier> *)
(** The data structure resulting from the compilation process *)
@@ -25,7 +25,7 @@
type t
-
+(** nb: previous bindings disappear *)
val add_type : Lic.item_key -> Lic.type_ -> t -> t
val add_const : Lic.item_key -> Lic.const -> t -> t
val add_node : Lic.node_key -> Lic.node_exp -> t -> t
diff --git a/src/rif_base.ml b/src/rif_base.ml
index f5f822fa..e33b12d0 100644
--- a/src/rif_base.ml
+++ b/src/rif_base.ml
@@ -11,7 +11,7 @@
open List
-let lexer = Genlex.make_lexer ["q"; "nil"; "#"; "x"; "load_luc"; "#@"; "@#"]
+let lexer = Genlex.make_lexer ["q"; "nil"; "ERROR"; "#"; "x"; "load_luc"; "#@"; "@#"]
(* xxx Which pragmas should be defined ? *)
@@ -164,6 +164,7 @@ and (parse_rif_stream : in_channel -> out_channel option -> vntl -> stream ->
parse_rif_stream ic oc vntl (get_stream ic oc)
tbl pragma
| (Genlex.Kwd (_,"nil"))::_ -> print_string "# nil value read. bye!\n"; raise Bye
+ | (Genlex.Kwd (_,"ERROR"))::_ -> print_string "#ERROR value read. bye!\n"; raise Bye
| (Genlex.Kwd (_,"q"))::_ -> print_string "# bye!\n"; raise Bye
| (Genlex.Kwd (_,"#@"))::_ ->
(* Beginning of multi-line comment. Note that here,
diff --git a/test/Makefile b/test/Makefile
index 1e619e75..d3a16d3f 100644
--- a/test/Makefile
+++ b/test/Makefile
@@ -25,6 +25,7 @@ lus2lic.diff:
lus2lic.time:
grep "testcase \./lus2lic" lus2lic.log > lus2lic.time
+ cat lus2lic.time >> lus2lic.sum
cat lus2lic.time
utest:
diff --git a/test/lus2lic.sum b/test/lus2lic.sum
index 728de6c7..0e225769 100644
--- a/test/lus2lic.sum
+++ b/test/lus2lic.sum
@@ -1,4 +1,4 @@
-Test Run By jahier on Tue May 21 09:29:18 2013
+Test Run By jahier on Wed May 22 14:36:57 2013
Native configuration is i686-pc-linux-gnu
=== lus2lic tests ===
@@ -20,7 +20,7 @@ PASS: ../utils/test_lus2lic_no_node should_work/argos.lus
PASS: ./lus2lic {-o /tmp/ck5.lic should_work/ck5.lus}
PASS: ./lus2lic {-ec -o /tmp/ck5.ec should_work/ck5.lus}
PASS: ./ec2c {-o /tmp/ck5.c /tmp/ck5.ec}
-UNRESOLVED: Time out: ../utils/test_lus2lic_no_node should_work/ck5.lus
+PASS: ../utils/test_lus2lic_no_node should_work/ck5.lus
PASS: ./lus2lic {-o /tmp/assertion.lic should_work/assertion.lus}
PASS: ./lus2lic {-ec -o /tmp/assertion.ec should_work/assertion.lus}
PASS: ./ec2c {-o /tmp/assertion.c /tmp/assertion.ec}
@@ -531,7 +531,7 @@ PASS: ../utils/test_lus2lic_no_node should_work/predef01.lus
PASS: ./lus2lic {-o /tmp/long_et_stupide_nom_de_noeud.lic should_work/long_et_stupide_nom_de_noeud.lus}
PASS: ./lus2lic {-ec -o /tmp/long_et_stupide_nom_de_noeud.ec should_work/long_et_stupide_nom_de_noeud.lus}
PASS: ./ec2c {-o /tmp/long_et_stupide_nom_de_noeud.c /tmp/long_et_stupide_nom_de_noeud.ec}
-UNRESOLVED: Time out: ../utils/test_lus2lic_no_node should_work/long_et_stupide_nom_de_noeud.lus
+PASS: ../utils/test_lus2lic_no_node should_work/long_et_stupide_nom_de_noeud.lus
PASS: ./lus2lic {-o /tmp/CURRENT.lic should_work/CURRENT.lus}
PASS: ./lus2lic {-ec -o /tmp/CURRENT.ec should_work/CURRENT.lus}
PASS: ./ec2c {-o /tmp/CURRENT.c /tmp/CURRENT.ec}
@@ -581,7 +581,7 @@ FAIL: Try to compare lus2lic -exec and ecexe: ../utils/test_lus2lic_no_node shou
PASS: ./lus2lic {-o /tmp/TIME_STABLE.lic should_work/TIME_STABLE.lus}
PASS: ./lus2lic {-ec -o /tmp/TIME_STABLE.ec should_work/TIME_STABLE.lus}
PASS: ./ec2c {-o /tmp/TIME_STABLE.c /tmp/TIME_STABLE.ec}
-FAIL: Try to compare lus2lic -exec and ecexe: ../utils/test_lus2lic_no_node should_work/TIME_STABLE.lus
+PASS: ../utils/test_lus2lic_no_node should_work/TIME_STABLE.lus
PASS: ./lus2lic {-o /tmp/cpt.lic should_work/cpt.lus}
PASS: ./lus2lic {-ec -o /tmp/cpt.ec should_work/cpt.lus}
PASS: ./ec2c {-o /tmp/cpt.c /tmp/cpt.ec}
@@ -1039,8 +1039,10 @@ XPASS: Test bad programs (semantics): lus2lic {-o /tmp/bug.lic should_fail/seman
=== lus2lic Summary ===
-# of expected passes 875
-# of unexpected failures 81
+# of expected passes 878
+# of unexpected failures 80
# of unexpected successes 12
# of expected failures 37
-# of unresolved testcases 22
+# of unresolved testcases 20
+testcase ./lus2lic.tests/non-reg.exp completed in 417 seconds
+testcase ./lus2lic.tests/progression.exp completed in 0 seconds
diff --git a/test/lus2lic.time b/test/lus2lic.time
index f1ae924f..cbc6a242 100644
--- a/test/lus2lic.time
+++ b/test/lus2lic.time
@@ -1,2 +1,2 @@
-testcase ./lus2lic.tests/non-reg.exp completed in 313 seconds
-testcase ./lus2lic.tests/progression.exp completed in 2 seconds
+testcase ./lus2lic.tests/non-reg.exp completed in 417 seconds
+testcase ./lus2lic.tests/progression.exp completed in 0 seconds
diff --git a/test/should_work/ck5.lus b/test/should_work/ck5.lus
index 8f27f6c7..dd0273ae 100644
--- a/test/should_work/ck5.lus
+++ b/test/should_work/ck5.lus
@@ -1,6 +1,9 @@
node ck5 (b,c: bool) returns (e: bool);
+var
+ c_prime: bool;
let
- e = current edge(b when c);
+ c_prime = true fby c;
+ e = current (edge(b when c_prime));
tel
node edge(x:bool) returns (y: bool);
diff --git a/test/should_work/long_et_stupide_nom_de_noeud.lus b/test/should_work/long_et_stupide_nom_de_noeud.lus
index 62a6f852..01210ed5 100644
--- a/test/should_work/long_et_stupide_nom_de_noeud.lus
+++ b/test/should_work/long_et_stupide_nom_de_noeud.lus
@@ -11,5 +11,5 @@
node long_et_stupide_nom_de_noeud(long_parametre:int)
returns (long_et_stupide_nom_de_sortie:int);
let
- long_et_stupide_nom_de_sortie = long_parametre + pre(long_parametre);
+ long_et_stupide_nom_de_sortie = long_parametre + 0 fby long_parametre;
tel
diff --git a/test/site.exp b/test/site.exp
index cfcb120b..a4d838a5 100644
--- a/test/site.exp
+++ b/test/site.exp
@@ -34,6 +34,10 @@ proc should_work { test_name command_line args } {
set failed 1
exp_continue
}
+ "ERROR" {
+ set failed 1
+ exp_continue
+ }
"oops: an internal" {
set failed 1
exp_continue
diff --git a/todo.org b/todo.org
index 8ddc98f1..28d567aa 100644
--- a/todo.org
+++ b/todo.org
@@ -194,8 +194,27 @@ l'appel depuis l'oracle au noeud à tester est mal typé...
modifer
file:~/lus2lic/utils/test_lus2lic_no_node
+* Performances
+Ceux là sont particulierement long (dont certains vraiment sans raison)
+en fait, quand ecexe se plante (oracle), il bloque tout le monde...
+
+# of unresolved testcases 20
+
+../utils/test_lus2lic_no_node should_work/left.lus
+../utils/test_lus2lic_no_node should_work/assertion.lus
+../utils/test_lus2lic_no_node should_work/normal.lus
+../utils/test_lus2lic_no_node should_work/Gyroscope2.lus
+ ../utils/test_lus2lic_no_node should_work/ELMU.lus
+ ../utils/test_lus2lic_no_node should_work/aux.lus
+../utils/test_lus2lic_no_node should_work/X1.lus
+../utils/test_lus2lic_no_node should_work/alarme.lus
+../utils/test_lus2lic_no_node should_work/onlyroll2.lus
+../utils/test_lus2lic_no_node should_work/integrator.lus
+../utils/test_lus2lic_no_node should_work/over2.lus
+../utils/test_lus2lic_no_node should_work/left.lus
* Divers
+
** TODO msg d'erreur un peu mavais sur ce programme
#+begin_src lustre
diff --git a/todo.org_archive b/todo.org_archive
index 71f5b7cb..5b3236ba 100644
--- a/todo.org_archive
+++ b/todo.org_archive
@@ -752,6 +752,17 @@ Bon, finalement, j'oblige les gens a ecrire Lustre::gt et puis ca marre.
File "objlinux/lic2soc.ml", line 680, column 18
when compiling lustre program should_work/morel3.lus
-> It was due to a bad handling in slices apprearinf at the lhs od equations.
+* TODO pb avec -en sur programme avec des when
+ - State "TODO" from "" [2013-05-21 Tue 11:10]
+ :PROPERTIES:
+ :ARCHIVE_TIME: 2013-05-21 Tue 17:30
+ :ARCHIVE_FILE: ~/lus2lic/todo.org
+ :ARCHIVE_OLPATH: Divers
+ :ARCHIVE_CATEGORY: lv6
+ :ARCHIVE_TODO: TODO
+ :END:
+ ./lus2lic _ck5_oracle.lus -n ck5_oracle -en
+
--
GitLab