diff --git a/_oasis b/_oasis index db5e822072499270382380a202104680a7e6b0f1..1c0f1d4f08cb48c8a6557c7fe426992ae05513d9 100644 --- a/_oasis +++ b/_oasis @@ -1,6 +1,6 @@ OASISFormat: 0.4 Name: lustre-v6 -Version: 1.639 +Version: 1.640 Synopsis: The Lustre V6 Verimag compiler Description: This package contains: - lus2lic: the (current) name of the compiler (and interpreter via -exec). diff --git a/src/lv6version.ml b/src/lv6version.ml index f1567e677dcf4558c3709303ddeee528a0e13aee..4913c107bf57fd0c77f75d824bb01baf230e1f44 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 = "639" -let sha_1 = "3d108df4086884271b6da788d44f1de6f0b2ad6d" +let commit = "640" +let sha_1 = "ed60151225485eeab12d7f347632e47f99e47eee" let str = (branch ^ "." ^ commit ^ " (" ^ sha_1 ^ ")") let maintainer = "jahier@imag.fr" diff --git a/src/sortActions.ml b/src/sortActions.ml index 6affbe2b69c114d12aa192abd83edd092d85adb1..6b974b4df57fd454b4bd0bbdb21302124101e654 100644 --- a/src/sortActions.ml +++ b/src/sortActions.ml @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 01/02/2016 (at 17:12) by Erwan Jahier> *) +(** Time-stamp: <modified the 03/02/2016 (at 10:03) by Erwan Jahier> *) (** topological sort of actions (that may optimize test openning) *) @@ -10,73 +10,22 @@ let info msg = (*********************************************************************************) -module OrderedAction = struct - type t = Action.t - let compare = compare -end -module MapAction = Map.Make(OrderedAction) - - -type color = Grey | Black (* in process | done *) -type color_table = color MapAction.t - -exception DependencyCycle of Action.t * Action.t list -(* exception DependencyCycle of Soc.var_expr list *) - -let (grey_actions : color_table -> Action.t list) = - fun ct -> - MapAction.fold - (fun action color acc -> if color=Grey then action::acc else acc) ct [] - -let rec (visit : ActionsDeps.t -> color_table -> Action.t -> color_table) = - fun succ_t color_t n -> - if not (ActionsDeps.have_deps succ_t n) then MapAction.add n Black color_t else - let color_t = - List.fold_left - (fun color_t nt -> - try - match MapAction.find nt color_t with - | Grey -> raise (DependencyCycle (n, grey_actions color_t)) - | Black -> color_t - with - (* The node [nt] is white *) - Not_found -> visit succ_t color_t nt - ) - (MapAction.add n Grey color_t) - (ActionsDeps.find_deps succ_t n) - in - MapAction.add n Black color_t - -(* TEDLT *) -let (check_there_is_no_cycle : Action.t list -> ActionsDeps.t -> unit) = - fun actions t -> - ignore (List.fold_left - (fun acc action -> visit t acc action) MapAction.empty actions) +module TopoSortActions = + TopoSort.Make( + struct + type elt = Action.t + type store = ActionsDeps.t + let find_dep = ActionsDeps.find_deps + let have_dep = ActionsDeps.have_deps + let remove_dep = ActionsDeps.remove_dep + end + ) let (topo_sort : Action.t list -> ActionsDeps.t -> Action.t list) = fun actions stbl -> - let visited_init = - List.fold_left (fun acc x -> MapAction.add x false acc) MapAction.empty actions - in - let rec f (acc:Action.t list) (l:Action.t list) (stbl:t) (visited:bool MapAction.t) = - (* The graph contains no cycle! *) - match l with - | [] -> List.rev acc - | x::tail -> - if (try MapAction.find x visited with Not_found -> assert false) - then - f acc tail stbl visited - else - let x_succ = ActionsDeps.find_deps stbl x in - if x_succ = [] then - f (x::acc) tail stbl (MapAction.add x true visited) - else - f acc (x_succ @ l) (ActionsDeps.remove_dep stbl x) visited - in - info "check_there_is_no_cycle...\n"; - check_there_is_no_cycle actions stbl; - info "topo_sort...\n"; - f [] actions stbl visited_init + info "topo_sort...\n"; + TopoSortActions.f stbl actions + (*********************************************************************************) (* From actions to gaos *) @@ -160,7 +109,7 @@ let (f : Action.t list -> ActionsDeps.t -> Lxm.t -> Soc.gao list) = let gaol = List.map (List.map gao_of_action) actions in SortActionsExpe.optimize_test_openning gaol ) - with DependencyCycle(x,l) -> + with TopoSortActions.DependencyCycle(x,l) -> let l = List.map Action.to_string l in let msg = "A combinational cycle been detected "^ (Lxm.details lxm)^" on \n "^(Action.to_string x)^ diff --git a/src/topoSort.ml b/src/topoSort.ml new file mode 100644 index 0000000000000000000000000000000000000000..da11bfdcc6aef7f14885a9c424451e005294d589 --- /dev/null +++ b/src/topoSort.ml @@ -0,0 +1,90 @@ +(** Time-stamp: <modified the 03/02/2016 (at 10:05) by Erwan Jahier> *) + + +module type PartialOrder = + sig + type elt + type store + val have_dep : store -> elt -> bool + val find_dep : store -> elt -> elt list + val remove_dep:store -> elt -> store + end + +module type S = + sig + type elt + type store + exception DependencyCycle of elt * elt list + val check_there_is_no_cycle : store -> elt list -> unit + val f : store -> elt list -> elt list +end + + +module Make(PO: PartialOrder) = struct + type elt = PO.elt + type store = PO.store + + module Ordered = struct + type t=elt + let compare = compare + end + module Mapt = Map.Make(Ordered) + + exception DependencyCycle of elt * elt list + + type color = Grey | Black (* in process | done *) + type color_table = color Mapt.t + + let (grey_actions : color_table -> elt list) = + fun ct -> + Mapt.fold + (fun x color acc -> if color=Grey then x::acc else acc) ct [] + +let rec (visit : store -> color_table -> elt -> color_table) = + fun store color_t n -> + if not (PO.have_dep store n) then Mapt.add n Black color_t else + let color_t = + List.fold_left + (fun color_t nt -> + try + match Mapt.find nt color_t with + | Grey -> raise (DependencyCycle (n, grey_actions color_t)) + | Black -> color_t + with + (* The node [nt] is white *) + Not_found -> visit store color_t nt + ) + (Mapt.add n Grey color_t) + (PO.find_dep store n) + in + Mapt.add n Black color_t + +(* TEDLT *) +let (check_there_is_no_cycle : store -> elt list -> unit) = + fun store l -> + ignore (List.fold_left (fun acc x -> visit store acc x) Mapt.empty l) + +let (f : store -> elt list -> elt list) = + fun store l -> + let visited_init = + List.fold_left (fun acc x -> Mapt.add x false acc) Mapt.empty l + in + let rec aux (store:store) (acc:elt list) (l:elt list) (visited:bool Mapt.t) = + (* The graph contains no cycle! *) + match l with + | [] -> List.rev acc + | x::tail -> + if (try Mapt.find x visited with Not_found -> assert false) + then + aux store acc tail visited + else + let x_succ = PO.find_dep store x in + if x_succ = [] then + aux store (x::acc) tail (Mapt.add x true visited) + else + aux (PO.remove_dep store x) acc (x_succ @ l) visited + in + check_there_is_no_cycle store l; + aux store [] l visited_init + +end diff --git a/src/topoSort.mli b/src/topoSort.mli new file mode 100644 index 0000000000000000000000000000000000000000..192670778c395ca1bee4d5ffac98b6d59038eec0 --- /dev/null +++ b/src/topoSort.mli @@ -0,0 +1,25 @@ +(** Time-stamp: <modified the 03/02/2016 (at 10:04) by Erwan Jahier> *) + + +module type PartialOrder = + sig + type elt + type store + val have_dep : store -> elt -> bool + val find_dep : store -> elt -> elt list + val remove_dep:store -> elt -> store + end + +module type S = + sig + type elt + type store + exception DependencyCycle of elt * elt list + val check_there_is_no_cycle : store -> elt list -> unit + val f : store -> elt list -> elt list +end + + +module Make(PO: PartialOrder) : S + with type elt = PO.elt + with type store = PO.store diff --git a/test/lus2lic.sum b/test/lus2lic.sum index 6cacdcdd4219bfdf903301afabbc390047530c4c..9b4bcf1e743e92e866749be4a43ccf46f59f6cea 100644 --- a/test/lus2lic.sum +++ b/test/lus2lic.sum @@ -1,5 +1,5 @@ ==> lus2lic0.sum <== -Test Run By jahier on Tue Feb 2 15:36:04 +Test Run By jahier on Wed Feb 3 09:55:09 Native configuration is x86_64-unknown-linux-gnu === lus2lic0 tests === @@ -64,7 +64,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 Tue Feb 2 15:36:05 +Test Run By jahier on Wed Feb 3 09:55:10 Native configuration is x86_64-unknown-linux-gnu === lus2lic1 tests === @@ -396,7 +396,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 Tue Feb 2 15:36:21 +Test Run By jahier on Wed Feb 3 09:55:25 Native configuration is x86_64-unknown-linux-gnu === lus2lic2 tests === @@ -741,7 +741,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 Tue Feb 2 15:37:09 +Test Run By jahier on Wed Feb 3 09:56:12 Native configuration is x86_64-unknown-linux-gnu === lus2lic3 tests === @@ -1243,7 +1243,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 Tue Feb 2 15:37:23 +Test Run By jahier on Wed Feb 3 09:56:26 Native configuration is x86_64-unknown-linux-gnu === lus2lic4 tests === @@ -1764,14 +1764,14 @@ PASS: /home/jahier/lus2lic/test/../utils/test_lus2lic_no_node zzz2.lus {} # of unexpected failures 4 =============================== # Total number of failures: 23 -lus2lic0.log:testcase ./lus2lic.tests/test0.exp completed in 0 seconds +lus2lic0.log:testcase ./lus2lic.tests/test0.exp completed in 1 seconds lus2lic1.log:testcase ./lus2lic.tests/test1.exp completed in 15 seconds -lus2lic2.log:testcase ./lus2lic.tests/test2.exp completed in 48 seconds +lus2lic2.log:testcase ./lus2lic.tests/test2.exp completed in 47 seconds lus2lic3.log:testcase ./lus2lic.tests/test3.exp completed in 14 seconds -lus2lic4.log:testcase ./lus2lic.tests/test4.exp completed in 48 seconds +lus2lic4.log:testcase ./lus2lic.tests/test4.exp completed in 49 seconds * Ref time: -0.04user 0.03system 2:06.76elapsed 0%CPU (0avgtext+0avgdata 5220maxresident)k -0inputs+0outputs (0major+5594minor)pagefaults 0swaps +0.04user 0.03system 2:05.33elapsed 0%CPU (0avgtext+0avgdata 5208maxresident)k +0inputs+0outputs (0major+5552minor)pagefaults 0swaps * Quick time (-j 4): -0.04user 0.01system 0:56.10elapsed 0%CPU (0avgtext+0avgdata 5164maxresident)k -32inputs+0outputs (0major+5629minor)pagefaults 0swaps +0.05user 0.01system 0:53.79elapsed 0%CPU (0avgtext+0avgdata 5220maxresident)k +32inputs+0outputs (0major+5577minor)pagefaults 0swaps diff --git a/test/should_work/dadic.lv6 b/test/should_work/dadic.lv6 new file mode 100644 index 0000000000000000000000000000000000000000..24421488e9fbe4ca7eb22f697f35f0d5148d7d0d --- /dev/null +++ b/test/should_work/dadic.lv6 @@ -0,0 +1,72 @@ +(****************************************************** +dadic.lv6 version 1.00 +******************************************************) + +package Dadic +provides + (* O : x -> 2*x *) + node O(x : bool) returns (y : bool); + (* I : x -> 2*x + 1 *) + node I(x : bool) returns (y : bool); + (* Add : x,y -> x + y *) + node Add(x, y : bool) returns (xpy : bool); + (* Chs : x -> -x *) + node Chs(x : bool) returns (ux : bool); + (* Mult : const n, x -> n*x *) + node Mult<<const n : int>>(x : bool) returns (y : bool); + (* OfInt : const n -> x *) +body + +node O(x : bool) returns (y : bool); +let y = false -> pre x; tel + +node I(x : bool) returns (y : bool); +let y = true -> pre x; tel + +node Add(x, y : bool) returns (xpy : bool); +var + c : bool; +let + c = if (false -> pre c) then (x or y) else (x and y); + xpy = ((false-> pre c) = (x = y)); +tel + +node Chs(x : bool) returns (ux : bool); +var + after_x : bool; +let + ux = if (after_x) then (not x) else (x); + after_x = false -> pre(after_x or x); +tel + +node Mult<<const n : int>>(x : bool) returns (y : bool); +let + y = with (n < 0) then ( + Mult<<-n>>(Chs(x)) + ) + else with (n = 0) then false + else with (n = 1) then x + else with ((n mod 2) = 0) then ( + Mult<<n div 2>>(O(x)) + ) else ( --(n div 2) = 1 + Add(Mult<<n div 2>>(O(x)), x) + ); + +tel + +(* ici -> pas de noeuds sans entree ? *) +node OfInt<<const n : int>>(_:bool) returns (y : bool); +let + y = with (n = -1) then true + else with (n = 0) then false + else with ((n mod 2) = 0) then + O(OfInt<<n div 2>>(true)) + else with (n > 0) then + I(OfInt<<n div 2>>(true)) + else + --attention aux négatifs ! + I(OfInt<<(n-1) div 2>>(true)); +tel + +end + diff --git a/test/should_work/dadic_x5_a.lus b/test/should_work/dadic_x5_a.lus new file mode 100644 index 0000000000000000000000000000000000000000..6f4037caf876537aa79eb6e0bbe058787506cc6d --- /dev/null +++ b/test/should_work/dadic_x5_a.lus @@ -0,0 +1,3 @@ +-- nonreg: dadic.lv6 +node dadic_x5_a = Dadic::Mult<<5>>; + diff --git a/test/should_work/dadic_x5_b.lus b/test/should_work/dadic_x5_b.lus new file mode 100644 index 0000000000000000000000000000000000000000..b57a9a3b6dfc5dfd2728c602a983f4375c342987 --- /dev/null +++ b/test/should_work/dadic_x5_b.lus @@ -0,0 +1,7 @@ +-- nonreg: dadic.lv6 +package Toto1 +provides + node x5(x:bool)returns (y:bool); +body + node x5 = Dadic::Mult<<5>>; +end diff --git a/test/should_work/dadic_x5_c.lus b/test/should_work/dadic_x5_c.lus new file mode 100644 index 0000000000000000000000000000000000000000..7866709cb8f393a1809e331673ec831dbc5b0842 --- /dev/null +++ b/test/should_work/dadic_x5_c.lus @@ -0,0 +1,8 @@ + +package Toto2 +uses Dadic; +provides + node x5(x:bool)returns (y:bool); +body + node x5 = Mult<<5>>; +end