diff --git a/src/l2lOptimIte.ml b/src/l2lOptimIte.ml index e6107a7a41ee4a3846e71b4ed55bb1dd33da87de..00514a7b1ba4c8dc8f22a64266aa49bdff64f9c6 100644 --- a/src/l2lOptimIte.ml +++ b/src/l2lOptimIte.ml @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 19/01/2015 (at 15:21) by Erwan Jahier> *) +(** Time-stamp: <modified the 21/01/2015 (at 11:47) by Erwan Jahier> *) open Lxm open Lic @@ -23,7 +23,7 @@ type acc = let new_var = LicName.new_var_info (********************************************************************************) -let (is_memory_less_val_exp : LicPrg.t -> Lic.val_exp -> bool) = +let (is_memory_less_and_safe_val_exp : LicPrg.t -> Lic.val_exp -> bool) = fun licprg ve -> let rec (aux_val_exp : Lic.val_exp -> bool) = fun ve -> aux_val_exp_core ve.ve_core @@ -45,7 +45,7 @@ let (is_memory_less_val_exp : LicPrg.t -> Lic.val_exp -> bool) = | CALL({it=nk}) | PREDEF_CALL({it=nk}) -> ( match LicPrg.find_node licprg nk with | None -> assert false (* SNO *) - | Some node_exp -> not node_exp.has_mem_eff + | Some node_exp -> node_exp.is_safe_eff && not node_exp.has_mem_eff ) | CURRENT _ (* XXX not clear. false is the safe value anyway. *) | PRE | ARROW | FBY -> false @@ -57,7 +57,7 @@ let (is_memory_less_val_exp : LicPrg.t -> Lic.val_exp -> bool) = in aux_val_exp ve -let (clock_of_cond: val_exp -> bool -> acc -> clock list * acc) = +let (clock_of_cond: val_exp -> bool -> acc -> clock * acc) = fun ve b acc -> let ve_clk = match ve.ve_clk with [clk] -> clk | _ -> assert false in let b = if b then "true" else "false" in @@ -72,21 +72,37 @@ let (clock_of_cond: val_exp -> bool -> acc -> clock list * acc) = let acc = nv::v,eq::eqs,ass in nv.var_name_eff, acc in - [On((cc,cv,Bool_type_eff), List.hd ve.ve_clk)], acc + On((cc,cv,Bool_type_eff), List.hd ve.ve_clk), acc + + +let (val_exp_when_clk : Lic.val_exp -> Lic.clock -> Lic.val_exp) = + fun ve clk -> +(* return "ve when clk" *) + let lxm = Lic.lxm_of_val_exp ve in + { ve with + ve_clk = List.map (fun _ -> clk) ve.ve_clk; (* *) + ve_core = CallByPosLic({ src=lxm; it=Lic.WHEN clk },[ve]); + } let (gen_merge : Lxm.t -> Lic.val_exp -> Lic.val_exp -> Lic.val_exp -> acc -> Lic.val_exp_core * acc ) = - fun lxm cond ve1 ve2 acc -> + fun lxm cond ve1 ve2 acc -> (* this is the core of the module *) let true_cst = { it=Bool_const_eff true ; src = lxm } in let false_cst = { it=Bool_const_eff false; src = lxm } in - let clk_true,acc = clock_of_cond cond true acc in - let clk_false,acc = clock_of_cond cond false acc in - let case_true = true_cst, { ve1 with ve_clk = clk_true } in - let case_false = false_cst, { ve2 with ve_clk = clk_false } in - Merge(cond, [case_true; case_false]), acc + let clk_true,acc = clock_of_cond cond true acc in + let clk_false,acc = clock_of_cond cond false acc in + let ve1 = val_exp_when_clk ve1 clk_true in + let ve2 = val_exp_when_clk ve2 clk_false in + Merge(cond, [(true_cst, ve1); (false_cst, ve2)]), acc +let is_var_ref ve = + match ve.ve_core with + | CallByPosLic({it=VAR_REF _},[]) -> true + | _ -> false + + (* All the remaining are admnistrative functions *) let rec (do_eq : LicPrg.t -> Lic.eq_info srcflagged -> acc -> acc) = @@ -131,11 +147,13 @@ and (do_val_exp: LicPrg.t -> val_exp -> acc -> val_exp * acc) = (List.rev vel) in match op.it with + | CALL({src=if_lxm; it=("Lustre","if"),[]}) | PREDEF_CALL({src=if_lxm; it=("Lustre","if"),[]}) -> ( match vel with - | [cond; ve1; ve2] -> - if is_memory_less_val_exp licprg ve1 && - is_memory_less_val_exp licprg ve2 + | [ cond ; ve1; ve2] -> + if is_memory_less_and_safe_val_exp licprg ve1 && + is_memory_less_and_safe_val_exp licprg ve2 && + is_var_ref cond (* exclude "if true then ..." from this optim *) then gen_merge op.src cond ve1 ve2 acc else diff --git a/src/l2lSplit.ml b/src/l2lSplit.ml index 0df56ea1d91d78122edd2c9b2238f874a7ced26a..683c8b3be9faf0de96b8f6814decf19551684174 100644 --- a/src/l2lSplit.ml +++ b/src/l2lSplit.ml @@ -204,11 +204,20 @@ and (split_val_exp : bool -> bool -> LicPrg.id_generator -> Lic.val_exp -> assert (List.length typ_l = List.length clk_l); let nv_l = List.map2 (new_var getid) typ_l clk_l in let lxm = lxm_of_val_exp ve in + let vi2val_exp nv = + let _,clk = nv.var_clock_eff in + { + ve_core = CallByPosLic(Lxm.flagit (Lic.VAR_REF (nv.var_name_eff)) lxm,[]); + ve_typ = [nv.var_type_eff]; + ve_clk = [clk]; + } + in let nve = match nv_l with - | [nv] -> { ve with ve_core = - CallByPosLic( - Lxm.flagit (Lic.VAR_REF (nv.var_name_eff)) lxm, [])} - | _ -> assert false + | [] -> assert false (* SNO *) + | [nv] -> vi2val_exp nv + | _ -> { ve with ve_core = + CallByPosLic(Lxm.flagit Lic.TUPLE lxm, List.map vi2val_exp nv_l) + } in let lpl = List.map (fun nv -> LeftVarLic(nv, lxm)) nv_l in let eq = Lxm.flagit (lpl, rhs) lxm in diff --git a/src/lic.ml b/src/lic.ml index b5cc04de0619b883a3578bb677efb1eacf2b5709..c2ba1524c06c3529f91a600ab864cfef3afa8f9c 100644 --- a/src/lic.ml +++ b/src/lic.ml @@ -1,4 +1,4 @@ -(* Time-stamp: <modified the 16/01/2015 (at 14:50) by Erwan Jahier> *) +(* Time-stamp: <modified the 20/01/2015 (at 16:04) by Erwan Jahier> *) (** Define the Data Structure representing Compiled programs. By compiled we mean that constant are propagated, packages are diff --git a/src/licEvalType.ml b/src/licEvalType.ml index ed8865d89fda55b16c26b3c502b962c5ebcca1a8..143e5f919bb694c720e132d4a8ee7d3f9ae62201 100644 --- a/src/licEvalType.ml +++ b/src/licEvalType.ml @@ -1,4 +1,4 @@ -(* Time-stamp: <modified the 26/06/2014 (at 18:31) by Erwan Jahier> *) +(* Time-stamp: <modified the 21/01/2015 (at 11:26) by Erwan Jahier> *) open AstPredef open Lxm @@ -324,7 +324,7 @@ let make_node_exp_eff (id_solver: IdSolver.t) (has_mem: bool option) (op: op) (l outlist_eff = outlist_eff; loclist_eff = None; def_eff = ExternLic; - has_mem_eff = (match has_mem with Some b -> b | None -> true); + has_mem_eff = (match has_mem with Some b -> b | None -> false); is_safe_eff = true; lxm = lxm; (* is_polym_eff = *) @@ -366,7 +366,7 @@ let make_simple_node_exp_eff (has_mem: bool option) (op: op) (lxm: Lxm.t) : Lic. outlist_eff = outlist_eff; loclist_eff = None; def_eff = ExternLic; - has_mem_eff = (match has_mem with Some b -> b | None -> true); + has_mem_eff = (match has_mem with Some b -> b | None -> false ); is_safe_eff = true; lxm = lxm; (* is_polym_eff = *) diff --git a/src/lv6MainArgs.ml b/src/lv6MainArgs.ml index 01029b1a6f11c9fbd46f653a03a109bf4f992b6a..c4d009460d3bfd34d91b62110558a99b79615cfe 100644 --- a/src/lv6MainArgs.ml +++ b/src/lv6MainArgs.ml @@ -1,4 +1,4 @@ -(* Time-stamp: <modified the 19/01/2015 (at 14:22) by Erwan Jahier> *) +(* Time-stamp: <modified the 21/01/2015 (at 11:53) by Erwan Jahier> *) (* Le manager d'argument adapté de celui de lutin, plus joli N.B. solution un peu batarde : les options sont stockées, comme avant, dans Global, @@ -90,7 +90,7 @@ let (make_opt : unit -> t) = expand_nodes = false; expand_node_call = []; expand_arrays = false; - optim_ite = false; + optim_ite = false; gen_autotest = false; (** the output channel *) oc = Pervasives.stdout; @@ -204,7 +204,9 @@ let set_ec_options opt = set_v4_options opt; global_opt.ec <- true; global_opt.no_prefix <- true; - opt.expand_nodes <- true + opt.expand_nodes <- true; + opt.optim_ite <- false ; (* because merge won't work *) + () (*** USER OPTIONS TAB **) let mkoptab (opt:t) : unit = ( diff --git a/src/lv6version.ml b/src/lv6version.ml index 646b3c1bcb3e9df1b75fc05f2849a93855fbe127..d888f2b4fa6691f12a68c7bf347710f17ab1f26e 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 = "548" -let sha_1 = "d783b03e3d8467fbe37848dfce67e3e26e5dea71" +let commit = "549" +let sha_1 = "54138036f775e06382e1ebee19efdbdd44b4d082" let str = (branch ^ "." ^ commit ^ " (" ^ sha_1 ^ ")") let maintainer = "jahier@imag.fr" diff --git a/test/lus2lic.sum b/test/lus2lic.sum index 10373f66a23dcf18540da5c8e9dbcceaf0a4588b..a47bdd8d7b555fe75b7e7ede744702429362fdc5 100644 --- a/test/lus2lic.sum +++ b/test/lus2lic.sum @@ -1,5 +1,5 @@ ==> lus2lic0.sum <== -Test Run By jahier on Tue Jan 20 15:03:20 +Test Run By jahier on Wed Jan 21 13:55:27 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 Tue Jan 20 15:03:33 +Test Run By jahier on Wed Jan 21 13:55:29 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 Tue Jan 20 15:04:30 +Test Run By jahier on Wed Jan 21 13:55:31 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 Tue Jan 20 15:05:48 +Test Run By jahier on Wed Jan 21 13:55:35 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 Tue Jan 20 15:06:39 +Test Run By jahier on Wed Jan 21 13:55:33 Native configuration is x86_64-unknown-linux-gnu === lus2lic4 tests === @@ -1726,12 +1726,14 @@ 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 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 +lus2lic0.log:testcase ./lus2lic.tests/test0.exp completed in 4 seconds +lus2lic1.log:testcase ./lus2lic.tests/test1.exp completed in 55 seconds +lus2lic2.log:testcase ./lus2lic.tests/test2.exp completed in 70 seconds +lus2lic3.log:testcase ./lus2lic.tests/test3.exp completed in 53 seconds +lus2lic4.log:testcase ./lus2lic.tests/test4.exp completed in 78 seconds * Ref time: -0.05user 0.09system 4:40.76elapsed 0%CPU (0avgtext+0avgdata 3016maxresident)k -0inputs+0outputs (0major+14902minor)pagefaults 0swaps +0.07user 0.08system 3:42.41elapsed 0%CPU (0avgtext+0avgdata 3020maxresident)k +0inputs+0outputs (0major+14898minor)pagefaults 0swaps * Quick time (-j 4): +0.04user 0.08system 1:25.07elapsed 0%CPU (0avgtext+0avgdata 3020maxresident)k +0inputs+0outputs (0major+14926minor)pagefaults 0swaps diff --git a/test/lus2lic.time b/test/lus2lic.time index ff4b191bf3c50a165a7bc35a328be150f9a41c30..c32bccb54d4f404ee86b735ba89baf46087c5053 100644 --- a/test/lus2lic.time +++ b/test/lus2lic.time @@ -1,9 +1,11 @@ -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 +lus2lic0.log:testcase ./lus2lic.tests/test0.exp completed in 4 seconds +lus2lic1.log:testcase ./lus2lic.tests/test1.exp completed in 55 seconds +lus2lic2.log:testcase ./lus2lic.tests/test2.exp completed in 70 seconds +lus2lic3.log:testcase ./lus2lic.tests/test3.exp completed in 53 seconds +lus2lic4.log:testcase ./lus2lic.tests/test4.exp completed in 78 seconds * Ref time: -0.05user 0.09system 4:40.76elapsed 0%CPU (0avgtext+0avgdata 3016maxresident)k -0inputs+0outputs (0major+14902minor)pagefaults 0swaps +0.07user 0.08system 3:42.41elapsed 0%CPU (0avgtext+0avgdata 3020maxresident)k +0inputs+0outputs (0major+14898minor)pagefaults 0swaps * Quick time (-j 4): +0.04user 0.08system 1:25.07elapsed 0%CPU (0avgtext+0avgdata 3020maxresident)k +0inputs+0outputs (0major+14926minor)pagefaults 0swaps diff --git a/test/should_work/carV2.lus b/test/should_work/carV2.lus index fcb007077fb8ac6eed118f1809c16e541fe483e1..f64e37a47aca2a43df9c73e8c7aadc2685b033c0 100644 --- a/test/should_work/carV2.lus +++ b/test/should_work/carV2.lus @@ -140,17 +140,20 @@ let else if(pre(mode) = 5 and not turn_r_Complete ) then 5-- not completed turning else if(pre(mode) = 5 and turn_r_Complete) then 6 -- after turn right , go to stop mode else 6; - -- blocked =-- 1 imply there is no obstacle in front, 0 imply there is a obstacle in front=> there - - - - (DIRECTION,VELOCITY) = if (mode =1 or mode =3) then (dir1,vel1) else if(mode =4) then (2,vel1) else if(mode = 5) then (3,vel1) else (0,0); - BUZZER = (mode = 3 or mode =4 or mode =5) ; -- buzzer on imply that car is parking mode else off - - + (DIRECTION,VELOCITY) = if (mode =1 or mode =3) + then (dir1,vel1) + else + if(mode =4) + then (2,vel1) + else + if(mode = 5) + then (3,vel1) + else (0,0); + BUZZER = (mode = 3 or mode = 4 or mode = 5) ; + -- buzzer on imply that car is parking mode else off tel diff --git a/test/should_work/heater_control.lus b/test/should_work/heater_control.lus index 5d0db95f44856de04d6e8ed9e621631e85b8cac6..9a668a47462344540c82fe6570846ad38b3b6ae1 100644 --- a/test/should_work/heater_control.lus +++ b/test/should_work/heater_control.lus @@ -77,48 +77,48 @@ tel ----------------------------------------------------------------------- -- returns the absolute value of 2 reals -node abs (v : real) returns (a : real) ; +function abs (v : real) returns (a : real) ; let a = if v >= 0.0 then v else -v ; tel -- returns the average values of 2 reals -node Average(a, b: real) returns (z : real); +function Average(a, b: real) returns (z : real); let z = (a+b)/2.0 ; tel -- returns the median values of 3 reals -node Median(a, b, c : real) returns (z : real); +function Median(a, b, c : real) returns (z : real); let z = a + b + c - min2 (a, min2(b,c)) - max2 (a, max2(b,c)) ; tel -- returns the maximum values of 2 reals -node max2 (one, two : real) returns (m : real) ; +function max2 (one, two : real) returns (m : real) ; let m = if one > two then one else two ; tel -- returns the minimum values of 2 reals -node min2 (one, two : real) returns (m : real) ; +function min2 (one, two : real) returns (m : real) ; let m = if one < two then one else two ; tel -node noneoftree (f1, f2, f3 : bool) returns (r : bool) +function noneoftree (f1, f2, f3 : bool) returns (r : bool) let r = not f1 and not f2 and not f3 ; tel -node alloftree (f1, f2, f3 : bool) returns (r : bool) +function alloftree (f1, f2, f3 : bool) returns (r : bool) let r = f1 and f2 and f3 ; tel -node oneoftree (f1, f2, f3 : bool) returns (r : bool) +function oneoftree (f1, f2, f3 : bool) returns (r : bool) let r = f1 and not f2 and not f3 or f2 and not f1 and not f3 or