diff --git a/_oasis b/_oasis index 9f4273884044d2eb27c4e7ce5b9e95e929bd9304..95c29b0141d397a10a7c881f9f0616b1ddf95262 100644 --- a/_oasis +++ b/_oasis @@ -1,6 +1,6 @@ OASISFormat: 0.4 Name: lustre-v6 -Version: 1.661 +Version: 1.662 Synopsis: The Lustre V6 Verimag compiler Description: This package contains: (1) lus2lic: the (current) name of the compiler (and interpreter via -exec). diff --git a/src/evalClock.ml b/src/evalClock.ml index 89bac14106dfbbc27cbf222179e893173466c735..bf7f44e04d35df284dfc951279036da6ca66b427 100644 --- a/src/evalClock.ml +++ b/src/evalClock.ml @@ -1,4 +1,4 @@ -(* Time-stamp: <modified the 01/09/2016 (at 14:35) by Erwan Jahier> *) +(* Time-stamp: <modified the 09/09/2016 (at 09:57) by Erwan Jahier> *) open AstPredef @@ -218,319 +218,329 @@ let rec (get_lxm_list : Lic.val_exp list -> int -> Lxm.t list) = (** Now we can go on and define [f]. *) let rec (f : IdSolver.t -> subst -> Lic.val_exp -> Lxm.t list -> Lic.clock list -> - Lic.val_exp * Lic.id_clock list * subst) = + Lic.val_exp * Lic.id_clock list * subst) = fun id_solver s ve lxms exp_clks -> - (* we split f so that we can reinit the fresh clock var generator *) - let ve, inf_clks, s = f_aux id_solver s ve in - let s = - if exp_clks = [] then s else ( - if (List.length exp_clks <> List.length inf_clks) then - raise (Compile_error(lxm_of_val_exp ve, "Bad arity")) - else - fold_left3 - (fun s lxm eclk iclk -> UnifyClock.f s lxm eclk iclk) - s - lxms - exp_clks - (List.map (fun (_,clk) -> clk) inf_clks) - ) - in - let inf_clks = List.map (fun (id,clk) -> id, apply_subst2 s clk) inf_clks in - let clks = snd (List.split inf_clks) in - let ve = apply_subst_val_exp s ve in - if Lv6Verbose.level() > 2 then - print_string ( + (* we split f so that we can reinit the fresh clock var generator *) + let ve, inf_clks, s = f_aux id_solver s ve in + let s = + if exp_clks = [] then s else ( + if (List.length exp_clks <> List.length inf_clks) then + raise (Compile_error(lxm_of_val_exp ve, "Bad arity")) + else + fold_left3 + (fun s lxm eclk iclk -> UnifyClock.f s lxm eclk iclk) + s + lxms + exp_clks + (List.map (fun (_,clk) -> clk) inf_clks) + ) + in + let inf_clks = List.map (fun (id,clk) -> id, apply_subst2 s clk) inf_clks in + let clks = snd (List.split inf_clks) in + let ve = apply_subst_val_exp s ve in + if Lv6Verbose.level() > 2 then + print_string ( "Clocking the expression '" ^ (LicDump.string_of_val_exp_eff ve) ^"': "^ (LicDump.string_of_clock2 (List.hd clks)) ^"\n"); - assert(ve.ve_clk <> []); - ve, inf_clks, s + assert(ve.ve_clk <> []); + ve, inf_clks, s -and (f_aux : IdSolver.t -> subst -> Lic.val_exp -> Lic.val_exp * Lic.id_clock list * subst) = +and (f_aux : IdSolver.t -> subst -> Lic.val_exp -> + Lic.val_exp * Lic.id_clock list * subst) = fun id_solver s ve -> - let ve, cel, s, lxm = - match ve.ve_core with - | CallByPosLic ({it=posop; src=lxm}, args) -> ( - let args, cel, s = eval_by_pos_clock id_solver posop lxm args s in - let ve = - match posop,args with - | CURRENT None, { ve_clk = (On((cc,cv,ct),cv_clk))::_ }::_ -> - (* We attach the clock constructor to CURRENT and the + let ve, cel, s, lxm = + match ve.ve_core with + | CallByPosLic ({it=posop; src=lxm}, args) -> ( + let args, cel, s = eval_by_pos_clock id_solver posop lxm args s in + (* current of a constant: we can ignore the current *) + if + (match posop with CURRENT _ -> true | _ -> false) && + (List.length args = 1) && Lic.val_exp_is_constant (List.hd args) + then + let ve,cel,s = f_aux id_solver s (List.hd args) in + ve, cel, s, lxm + else + let ve = + match posop,args with + | CURRENT None, { ve_clk = (On((cc,cv,ct),cv_clk))::_ }::_ -> + (* We attach the clock constructor to CURRENT and the clock var to the list of args. Indeed, the user does not need to specify the clock when it uses current ; hence we add this information as soon as it is computed, i.e., here. - *) - let cv_val_exp = flagit (Lic.VAR_REF cv) lxm in - let cv_val_exp = Lic.CallByPosLic(cv_val_exp,[]) in - let cv_val_exp = { ve_core = cv_val_exp ; ve_typ = [ct] ; ve_clk = [cv_clk] } in - let posop,args = CURRENT (Some cc), cv_val_exp::args in - let ve = { ve with - ve_core = CallByPosLic ({it=posop; src=lxm}, args) ; - ve_clk = [cv_clk] - } in - ve - | _ -> { ve with ve_core = CallByPosLic ({it=posop; src=lxm}, args)} - in - List.iter (fun arg -> assert (arg.ve_clk <> [])) args; - ve, cel, s, lxm - ) - | CallByNameLic ({it=nmop; src=lxm}, nmargs) -> ( - try - let nmargs, cel, s = eval_by_name_clock id_solver nmop lxm nmargs s in - let ve = { ve with ve_core = CallByNameLic ({it=nmop; src=lxm}, nmargs) } in - List.iter (fun (_,arg) -> assert (arg.ve_clk <> [])) nmargs; - ve, cel, s, lxm - with EvalConst_error msg -> - raise (Compile_error(lxm, "\n*** can't eval constant: "^msg)) - ) - | Merge(ce, cl) -> - let ce, cel, s = f_aux id_solver s ce in - let (merge_clk : Lic.clock) = List.hd ce.ve_clk in - let ce_id,lxm = match ce with - | { ve_core= CallByPosLic({it = VAR_REF id ; src = lxm },[]) } -> id,lxm - | _ -> assert false - in - let check_case (s,acc) (c,ve) = - (* Check that ve is on c(ce) on merge_clk *) - let id_clk = - match c.it with - | Bool_const_eff true -> "Lustre", "true" - | Bool_const_eff false -> "Lustre", "false" - | Enum_const_eff (s,_) -> s - | _ -> assert false - in - let id_clk = (id_clk, ce_id, Lic.type_of_const c.it) in - let exp_clk = [On(id_clk, merge_clk)] in - let ve,cel,s = f id_solver s ve [c.src] exp_clk in - s, (c,ve)::acc - in - let s,cl = List.fold_left check_case (s,[]) cl in - let ve = { ve with ve_core = Merge(ce, List.rev cl) } in - ve, [ce_id,merge_clk], s, lxm - in - let new_clk = snd (List.split cel) in - let s, ve = - if ve.ve_clk = [] then (s, { ve with ve_clk = new_clk }) else - let s = - assert(List.length ve.ve_clk = List.length new_clk); - List.fold_left2 (fun s -> UnifyClock.f s lxm) s ve.ve_clk new_clk in - s, ve - in - let ve = apply_subst_val_exp s ve in - assert(ve.ve_clk <> []); - ve, cel, s + *) + let cv_val_exp = flagit (Lic.VAR_REF cv) lxm in + let cv_val_exp = Lic.CallByPosLic(cv_val_exp,[]) in + let cv_val_exp = { ve_core = cv_val_exp ; ve_typ = [ct] ; + ve_clk = [cv_clk] } in + let posop,args = CURRENT (Some cc), cv_val_exp::args in + let ve = { ve with + ve_core = CallByPosLic ({it=posop; src=lxm}, args) ; + ve_clk = [cv_clk] + } in + ve + | _ -> { ve with ve_core = CallByPosLic ({it=posop; src=lxm}, args)} + in + List.iter (fun arg -> assert (arg.ve_clk <> [])) args; + ve, cel, s, lxm + ) + | CallByNameLic ({it=nmop; src=lxm}, nmargs) -> ( + try + let nmargs, cel, s = eval_by_name_clock id_solver nmop lxm nmargs s in + let ve = { ve with ve_core = CallByNameLic ({it=nmop; src=lxm}, nmargs) } in + List.iter (fun (_,arg) -> assert (arg.ve_clk <> [])) nmargs; + ve, cel, s, lxm + with EvalConst_error msg -> + raise (Compile_error(lxm, "\n*** can't eval constant: "^msg)) + ) + | Merge(ce, cl) -> + let ce, cel, s = f_aux id_solver s ce in + let (merge_clk : Lic.clock) = List.hd ce.ve_clk in + let ce_id,lxm = match ce with + | { ve_core= CallByPosLic({it = VAR_REF id ; src = lxm },[]) } -> id,lxm + | _ -> assert false + in + let check_case (s,acc) (c,ve) = + (* Check that ve is on c(ce) on merge_clk *) + let id_clk = + match c.it with + | Bool_const_eff true -> "Lustre", "true" + | Bool_const_eff false -> "Lustre", "false" + | Enum_const_eff (s,_) -> s + | _ -> assert false + in + let id_clk = (id_clk, ce_id, Lic.type_of_const c.it) in + let exp_clk = [On(id_clk, merge_clk)] in + let ve,cel,s = f id_solver s ve [c.src] exp_clk in + s, (c,ve)::acc + in + let s,cl = List.fold_left check_case (s,[]) cl in + let ve = { ve with ve_core = Merge(ce, List.rev cl) } in + ve, [ce_id,merge_clk], s, lxm + in + let new_clk = snd (List.split cel) in + let s, ve = + if ve.ve_clk = [] then (s, { ve with ve_clk = new_clk }) else + let s = + assert(List.length ve.ve_clk = List.length new_clk); + List.fold_left2 (fun s -> UnifyClock.f s lxm) s ve.ve_clk new_clk in + s, ve + in + let ve = apply_subst_val_exp s ve in + assert(ve.ve_clk <> []); + ve, cel, s (* iterate f on a list of expressions *) and (f_list : IdSolver.t -> subst -> Lic.val_exp list -> - Lic.val_exp list * Lic.id_clock list list * subst) = + Lic.val_exp list * Lic.id_clock list list * subst) = fun id_solver s args -> - let aux (args,acc,s) arg = - let arg, cil, s = f_aux id_solver s arg in - (arg::args, cil::acc, s) - in - let (args, cil, s) = List.fold_left aux ([],[],s) args in - let args = List.rev args in - let cil = List.rev cil in - let cil = List.map (List.map(fun (id,clk) -> id, apply_subst2 s clk)) cil in - List.iter (fun arg -> assert (arg.ve_clk <> [])) args; - args, cil, s + let aux (args,acc,s) arg = + let arg, cil, s = f_aux id_solver s arg in + (arg::args, cil::acc, s) + in + let (args, cil, s) = List.fold_left aux ([],[],s) args in + let args = List.rev args in + let cil = List.rev cil in + let cil = List.map (List.map(fun (id,clk) -> id, apply_subst2 s clk)) cil in + List.iter (fun arg -> assert (arg.ve_clk <> [])) args; + args, cil, s and (eval_by_pos_clock : IdSolver.t -> Lic.by_pos_op -> Lxm.t -> Lic.val_exp list -> - subst -> Lic.val_exp list * Lic.id_clock list * subst) = + subst -> Lic.val_exp list * Lic.id_clock list * subst) = fun id_solver posop lxm args s -> - let apply_subst s (id,clk) = id, UnifyClock.apply_subst s clk in - let args, (cl,s) = - match posop,args with - | Lic.CURRENT (Some _), clk_arg::_ -> assert false - | Lic.CURRENT None, [arg] -> ( (* we return the clock of the argument *) - let args, clocks_of_args, s = f_list id_solver s [arg] in - let current_clock = function - | (id, BaseLic) -> (id, BaseLic) - | (id, On(_,clk)) -> (id, clk) - | (id, ClockVar i) -> (id, ClockVar i) - in - args, (List.map current_clock (List.flatten clocks_of_args), s) - ) - | Lic.CURRENT None, _ -> assert false (* SNO *) - | Lic.CURRENT (Some _), _ -> assert false (* SNO *) - | Lic.WHEN when_exp_clk,args -> ( - let c_clk = - match when_exp_clk with - | BaseLic -> BaseLic - | ClockVar _ -> assert false - | On((cc,c,_), c_clk) -> - (* | NamedClock { it = (cc,c) ; src = lxm } -> *) - (* let id, c_clk = (id_solver.id2var c lxm).var_clock_eff in *) - c_clk - in - let aux_when exp_clk s = - (* + let apply_subst s (id,clk) = id, UnifyClock.apply_subst s clk in + let args, (cl,s) = + match posop,args with + | Lic.CURRENT (Some _), clk_arg::_ -> assert false + | Lic.CURRENT None, [arg] -> ( (* we return the clock of the argument *) + let args, clocks_of_args, s = f_list id_solver s [arg] in + let current_clock = function + | (id, BaseLic) -> (id, BaseLic) + | (id, On(_,clk)) -> (id, clk) + | (id, ClockVar i) -> (id, ClockVar i) + in + args, (List.map current_clock (List.flatten clocks_of_args), s) + ) + | Lic.CURRENT None, _ -> assert false (* SNO *) + | Lic.CURRENT (Some _), _ -> assert false (* SNO *) + | Lic.WHEN when_exp_clk,args -> ( + let c_clk = + match when_exp_clk with + | BaseLic -> BaseLic + | ClockVar _ -> assert false + | On((cc,c,_), c_clk) -> + (* | NamedClock { it = (cc,c) ; src = lxm } -> *) + (* let id, c_clk = (id_solver.id2var c lxm).var_clock_eff in *) + c_clk + in + let aux_when exp_clk s = + (* In order to clock check an expression such as exp when C(c) we first need to check that the clock of c (c_clk) is a sub-clock of the clock of exp (exp_clk). - *) - match is_a_sub_clock lxm s exp_clk (fst exp_clk,c_clk) with - | None -> - let msg = "\n*** clock error: '" ^ (ci2str (snd exp_clk)) ^ - "' is not a sub-clock of '" ^ (ci2str c_clk) ^ "'" - in - raise (Compile_error(lxm, msg)) - | Some s -> - let id_when_exp_clk, s = - match exp_clk with - | id, On(var, _) -> (id, when_exp_clk), s - | id, BaseLic -> (id, when_exp_clk), s - | id, ClockVar i -> - let id_when_exp_clk = id, when_exp_clk in - let (s1,s2) = s in - id_when_exp_clk, - (s1, UnifyClock.add_subst2 i when_exp_clk s2) - in - id_when_exp_clk, s - in - (match f_list id_solver s args with - (* XXX ce cas ne sert à rien !!! + *) + match is_a_sub_clock lxm s exp_clk (fst exp_clk,c_clk) with + | None -> + let msg = "\n*** clock error: '" ^ (ci2str (snd exp_clk)) ^ + "' is not a sub-clock of '" ^ (ci2str c_clk) ^ "'" + in + raise (Compile_error(lxm, msg)) + | Some s -> + let id_when_exp_clk, s = + match exp_clk with + | id, On(var, _) -> (id, when_exp_clk), s + | id, BaseLic -> (id, when_exp_clk), s + | id, ClockVar i -> + let id_when_exp_clk = id, when_exp_clk in + let (s1,s2) = s in + id_when_exp_clk, + (s1, UnifyClock.add_subst2 i when_exp_clk s2) + in + id_when_exp_clk, s + in + (match f_list id_solver s args with + (* XXX ce cas ne sert à rien !!! le traitement du cas ou la liste ne contient qu'un element n'a aucun raison d'etre particulier, si ??? - *) - | args,[[exp_clk]], s -> - let (exp_clk,s) = aux_when exp_clk s in - args,([exp_clk], s) - - | args, [exp_clk_list], s -> - (* when on tuples *) - let exp_clk_list, s = - List.fold_left - (fun (acc,s) exp_clk -> - let (exp_clk,s) = aux_when exp_clk s in - exp_clk::acc, s - ) - ([],s) - exp_clk_list - in - args,(List.rev exp_clk_list, s) - | _ -> assert false (* "(x1,x2) when node (x,y)" *) - ) - ) - | Lic.HAT(i), [] -> assert false - | Lic.HAT(i), ve::_ -> - let (ve,clk,s) = f_aux id_solver s ve in - [ve],(clk,s) - - | Lic.VAR_REF id,args -> - let vi = IdSolver.var_info_of_ident id_solver id lxm in - args,([var_info_eff_to_clock_eff vi], s) - - | Lic.CONST c, args -> ( - let s, clk = UnifyClock.new_clock_var s in - args,([Lic.string_of_const c, clk], s) - ) - | Lic.CONST_REF idl,args -> - let _const = IdSolver.const_eff_of_item_key id_solver idl lxm in - let s, clk = UnifyClock.new_clock_var s in - args,([Lv6Id.of_long idl, clk], s) - | Lic.CALL nkf,args -> - let node_key = nkf.it in - let lxm = nkf.src in - let node_exp_eff = IdSolver.node_exp_of_node_key id_solver node_key lxm in - let (cil_arg, cil_res) = get_clock_profile node_exp_eff in - let s, rel_base = UnifyClock.new_clock_var s in - (* the value of the base clock of a node is actually relative + *) + | args,[[exp_clk]], s -> + let (exp_clk,s) = aux_when exp_clk s in + args,([exp_clk], s) + + | args, [exp_clk_list], s -> + (* when on tuples *) + let exp_clk_list, s = + List.fold_left + (fun (acc,s) exp_clk -> + let (exp_clk,s) = aux_when exp_clk s in + exp_clk::acc, s + ) + ([],s) + exp_clk_list + in + args,(List.rev exp_clk_list, s) + | _ -> assert false (* "(x1,x2) when node (x,y)" *) + ) + ) + | Lic.HAT(i), [] -> assert false + | Lic.HAT(i), ve::_ -> + let (ve,clk,s) = f_aux id_solver s ve in + [ve],(clk,s) + + | Lic.VAR_REF id,args -> + let vi = IdSolver.var_info_of_ident id_solver id lxm in + args,([var_info_eff_to_clock_eff vi], s) + + | Lic.CONST c, args -> ( + let s, clk = UnifyClock.new_clock_var s in + args,([Lic.string_of_const c, clk], s) + ) + | Lic.CONST_REF idl,args -> + let _const = IdSolver.const_eff_of_item_key id_solver idl lxm in + let s, clk = UnifyClock.new_clock_var s in + args,([Lv6Id.of_long idl, clk], s) + | Lic.CALL nkf,args -> + let node_key = nkf.it in + let lxm = nkf.src in + let node_exp_eff = IdSolver.node_exp_of_node_key id_solver node_key lxm in + let (cil_arg, cil_res) = get_clock_profile node_exp_eff in + let s, rel_base = UnifyClock.new_clock_var s in + (* the value of the base clock of a node is actually relative to the context into which the node is called. Hence we create a fresh var clock, that will be instanciated by the caller. - *) - let (replace_base : Lic.clock -> Lic.id_clock -> Lic.id_clock) = - fun rel_base (id,ci) -> - (* [replace_base rel_base ci ] replaces in [ci] any occurences of the + *) + let (replace_base : Lic.clock -> Lic.id_clock -> Lic.id_clock) = + fun rel_base (id,ci) -> + (* [replace_base rel_base ci ] replaces in [ci] any occurences of the base clock by [rel_base] *) - let rec aux ci = - match ci with - | BaseLic -> rel_base - | On(v,clk) -> On(v, aux clk) - | ClockVar i -> ci - in - id, aux ci - in - let cil_arg = List.map (replace_base rel_base) cil_arg in - let cil_res = List.map (replace_base rel_base) cil_res in - let args, clk_args, s = f_list id_solver s args in - let lxms = get_lxm_list args (List.length cil_arg) in - let s = check_args lxms s cil_arg (List.flatten clk_args) in - let cil_res = List.map (apply_subst s) cil_res in - args, (cil_res, s) - - | Lic.PREDEF_CALL (nkf),args -> - let op = AstPredef.string_to_op (snd(fst nkf.it)) in - let args, clk_args, s = f_list id_solver s args in - let flat_clk_args = List.flatten clk_args in (* all predef nodes are mono-clock! *) - let _,flat_clk_args = List.split flat_clk_args in - let lxms = get_lxm_list args (List.length flat_clk_args) in - let clk_list, s = - if args = [] then [],s else - let _clk,s = UnifyClock.list lxms flat_clk_args s in - List.map (List.map (apply_subst s)) clk_args, s - in - args, LicEvalClock.f id_solver op lxm s clk_list - - (* One argument. *) - | Lic.PRE,args - | Lic.STRUCT_ACCESS _,args - | Lic.ARRAY_ACCES (_),args - | Lic.ARRAY_SLICE (_),args -> - assert(List.length args = 1); - let (arg,clk,s) = f_aux id_solver s (List.hd args) in - [arg], (clk,s) - - (* may have tuples as arguments *) - | Lic.TUPLE,args - | Lic.ARROW,args - | Lic.FBY ,args - | Lic.CONCAT,args - | Lic.ARRAY,args -> ( - (* Check that all args are of the same (unifiable) clocks. + let rec aux ci = + match ci with + | BaseLic -> rel_base + | On(v,clk) -> On(v, aux clk) + | ClockVar i -> ci + in + id, aux ci + in + let cil_arg = List.map (replace_base rel_base) cil_arg in + let cil_res = List.map (replace_base rel_base) cil_res in + let args, clk_args, s = f_list id_solver s args in + let lxms = get_lxm_list args (List.length cil_arg) in + let s = check_args lxms s cil_arg (List.flatten clk_args) in + let cil_res = List.map (apply_subst s) cil_res in + args, (cil_res, s) + + | Lic.PREDEF_CALL (nkf),args -> + let op = AstPredef.string_to_op (snd(fst nkf.it)) in + let args, clk_args, s = f_list id_solver s args in + let flat_clk_args = List.flatten clk_args in (* all predef nodes are mono-clock! *) + let _,flat_clk_args = List.split flat_clk_args in + let lxms = get_lxm_list args (List.length flat_clk_args) in + let clk_list, s = + if args = [] then [],s else + let _clk,s = UnifyClock.list lxms flat_clk_args s in + List.map (List.map (apply_subst s)) clk_args, s + in + args, LicEvalClock.f id_solver op lxm s clk_list + + (* One argument. *) + | Lic.PRE,args + | Lic.STRUCT_ACCESS _,args + | Lic.ARRAY_ACCES (_),args + | Lic.ARRAY_SLICE (_),args -> + assert(List.length args = 1); + let (arg,clk,s) = f_aux id_solver s (List.hd args) in + [arg], (clk,s) + + (* may have tuples as arguments *) + | Lic.TUPLE,args + | Lic.ARROW,args + | Lic.FBY ,args + | Lic.CONCAT,args + | Lic.ARRAY,args -> ( + (* Check that all args are of the same (unifiable) clocks. XXX : we suppose that all those operators are mono-clocks (i.e., when they return tuples, all elements are on the same clock). It would be sensible to have, e.g., arrows on multiple clocks. We'll refine later. *) - let args, clk_args, s = f_list id_solver s args in - let flat_clk_args = List.flatten clk_args in (* => mono-clock! *) - let idl,flat_clk_args = List.split flat_clk_args in - let lxms = get_lxm_list args (List.length flat_clk_args) in - let clk,s = UnifyClock.list lxms flat_clk_args s in - let clk_list = - match posop with - | Lic.TUPLE -> - let clk_l = List.map (UnifyClock.apply_subst s) flat_clk_args in - List.combine idl clk_l - | _ -> List.map (apply_subst s) (List.hd clk_args) - in - args, (clk_list, s) - ) - in - args, cl, s + let args, clk_args, s = f_list id_solver s args in + let flat_clk_args = List.flatten clk_args in (* => mono-clock! *) + let idl,flat_clk_args = List.split flat_clk_args in + let lxms = get_lxm_list args (List.length flat_clk_args) in + let clk,s = UnifyClock.list lxms flat_clk_args s in + let clk_list = + match posop with + | Lic.TUPLE -> + let clk_l = List.map (UnifyClock.apply_subst s) flat_clk_args in + List.combine idl clk_l + | _ -> List.map (apply_subst s) (List.hd clk_args) + in + args, (clk_list, s) + ) + in + args, cl, s and (eval_by_name_clock : IdSolver.t -> Lic.by_name_op -> Lxm.t -> - (Lv6Id.t Lxm.srcflagged * Lic.val_exp) list -> subst -> - (Lv6Id.t Lxm.srcflagged * Lic.val_exp) list * Lic.id_clock list * subst) = + (Lv6Id.t Lxm.srcflagged * Lic.val_exp) list -> subst -> + (Lv6Id.t Lxm.srcflagged * Lic.val_exp) list * Lic.id_clock list * subst) = fun id_solver namop lxm namargs s -> - let apply_subst s (id,clk) = id, UnifyClock.apply_subst s clk in - let args = List.map (fun (id,ve) -> ve) namargs in - (* XXX The 3 following lines duplicates the code of TUPLE_eff and co *) - let args, clk_args, s = f_list id_solver s args in - let namargs = List.map2 (fun (id,_ve) ve -> id,ve) namargs args in - let flat_clk_args = List.flatten clk_args in (* => mono-clock! *) - let _,flat_clk_args = List.split flat_clk_args in - let lxms = get_lxm_list args (List.length flat_clk_args) in - let clk,s = UnifyClock.list lxms flat_clk_args s in - let clk_list = List.map (apply_subst s) (List.hd clk_args) in - match namop with - | Lic.STRUCT_anonymous -> assert false (* cf EvalType.E *) - | Lic.STRUCT(_) -> namargs, clk_list, s - | Lic.STRUCT_with(_, dft) -> - (* XXX should i do something here ??? *) - namargs,clk_list, s + let apply_subst s (id,clk) = id, UnifyClock.apply_subst s clk in + let args = List.map (fun (id,ve) -> ve) namargs in + (* XXX The 3 following lines duplicates the code of TUPLE_eff and co *) + let args, clk_args, s = f_list id_solver s args in + let namargs = List.map2 (fun (id,_ve) ve -> id,ve) namargs args in + let flat_clk_args = List.flatten clk_args in (* => mono-clock! *) + let _,flat_clk_args = List.split flat_clk_args in + let lxms = get_lxm_list args (List.length flat_clk_args) in + let clk,s = UnifyClock.list lxms flat_clk_args s in + let clk_list = List.map (apply_subst s) (List.hd clk_args) in + match namop with + | Lic.STRUCT_anonymous -> assert false (* cf EvalType.E *) + | Lic.STRUCT(_) -> namargs, clk_list, s + | Lic.STRUCT_with(_, dft) -> + (* XXX should i do something here ??? *) + namargs,clk_list, s diff --git a/src/lic.ml b/src/lic.ml index f1988a0c254c81188ae22402a535c62084214939..6794ff2d7165321b54c609abc99ed419a4ff4575 100644 --- a/src/lic.ml +++ b/src/lic.ml @@ -1,4 +1,4 @@ -(* Time-stamp: <modified the 01/09/2016 (at 15:39) by Erwan Jahier> *) +(* Time-stamp: <modified the 09/09/2016 (at 08:32) by Erwan Jahier> *) (** Define the Data Structure representing Compiled programs. By compiled we mean that constant are propagated, packages are @@ -534,6 +534,9 @@ let (is_extern_const : const -> bool) = | Abstract_const_eff (_,_,_, true) -> true | _ -> false +let (val_exp_is_constant : val_exp -> bool) = function + | { ve_core = CallByPosLic({it=CONST_REF _ | CONST _},_) } -> true + | _ -> false let type_of_val_exp ve = ve.ve_typ diff --git a/src/lv6version.ml b/src/lv6version.ml index a8e0b2dda7572455406c1c31c13f6feace7bb552..d2c6a60816a6ea626de397a020228bdc6f55145f 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 = "661" -let sha_1 = "4508ea9fa98a3e651c3c3039d1525255d50ef17b" +let commit = "662" +let sha_1 = "dc44269befd884f2e80129d89556aad0f66ad829" let str = (branch ^ "." ^ commit ^ " (" ^ sha_1 ^ ")") let maintainer = "jahier@imag.fr" diff --git a/src/main.ml b/src/main.ml index 66a455d9131113522f0ae89afdcdcf73c0c7c2cf..48838b5f07c1aaf2b22c1f11a9248c768dea9fd9 100644 --- a/src/main.ml +++ b/src/main.ml @@ -1,4 +1,4 @@ -(* Time-stamp: <modified the 01/03/2016 (at 15:21) by Erwan Jahier> *) +(* Time-stamp: <modified the 06/09/2016 (at 10:29) by Erwan Jahier> *) open Lv6Verbose open AstV6 @@ -89,7 +89,8 @@ let (gen_autotest_files : LicPrg.t -> Lv6Id.idref option -> Lv6MainArgs.t -> uni let main_node = Lv6Id.to_idref name in let nk = (Lic.node_key_of_idref main_node) in if LicPrg.node_exists lic_prg nk then ( - output_string stdout ("WARNING: No main node is specified. I'll try with " ^ name ^"\n"); + output_string stdout ("WARNING: No main node is specified. I'll try with " + ^ name ^"\n"); flush stdout; let msk, zesoc = Lic2soc.f lic_prg nk in msk, zesoc, main_node @@ -113,7 +114,8 @@ let (gen_autotest_files : LicPrg.t -> Lv6Id.idref option -> Lv6MainArgs.t -> uni let assertions_cstr = List.map assertion_to_lutin_cstr assertions in let assertions_cstr = List.filter (fun str -> str<>"") assertions_cstr in let assertion_cstr = String.concat " &> " assertions_cstr in - let assertion_cstr = if assertion_cstr = "" then "loop true" else "{ "^assertion_cstr^" }" in + let assertion_cstr = if assertion_cstr = "" then "loop true" + else "{ "^assertion_cstr^" }" in let my_type_to_string range_flag t = (* Remove the module name to have correct Lutin and lv4 type decl *) let str = Data.type_to_string t in @@ -151,12 +153,13 @@ let (gen_autotest_files : LicPrg.t -> Lv6Id.idref option -> Lv6MainArgs.t -> uni let prg = "node "^name^"_oracle("^(String.concat ";" (invars_str@outvars_str)) in let locals_str = List.map (fun (n,t) -> n^":"^(my_type_to_string false t)) locals in let ok = (* avoid name clash*) - let all_vars = List.map fst (List.rev_append (List.rev_append locals invars) outvars) in + let all_vars = List.map fst (List.rev_append + (List.rev_append locals invars) outvars) in let rec gen_ok str = if List.mem str all_vars then gen_ok ("_"^str) else str in gen_ok "ok" in let prg = "-- oracle to compare Lustre compilers\n" ^ prg in - let prg = prg ^") \nreturns("^ok^":bool;"^(String.concat ";" locals_str)^");\nlet\n" in + let prg = prg^") \nreturns("^ok^":bool;"^(String.concat ";" locals_str)^");\nlet\n" in let locals_name = List.map fst locals in let invars_name = List.map fst invars in let prg = prg^" ("^(String.concat "," locals_name)^") = "^name in @@ -180,9 +183,11 @@ let (gen_autotest_files : LicPrg.t -> Lv6Id.idref option -> Lv6MainArgs.t -> uni in aux x y t in - let prg = try prg^(String.concat " and\n \t\t " - (List.flatten (List.map2 var_to_equals locals outvars))) ^");\ntel;\n" - with _ -> assert false + let prg = try prg^(String.concat + " and\n \t\t " + (List.flatten + (List.map2 var_to_equals locals outvars))) ^");\ntel;\n" + with _ -> assert false in let prg = prg^"\n-- oracle to compare two programs \n" in let prg = prg^"node "^name^"_oracle_prog("^(String.concat ";" (invars_str)) in @@ -273,7 +278,7 @@ let main () = ( let name = find_a_node opt in let nk = (Lic.node_key_of_idref (Lv6Id.to_idref name)) in if LicPrg.node_exists lic_prg nk then ( - print_string ("WARNING: No main node is specified. I'll try with " ^ name ^"\n"); + print_string ("WARNING: No main node is specified. I'll try with "^name^"\n"); flush stdout; profile_info "Start compiling to soc...\n"; let msk,zesoc = Lic2soc.f lic_prg nk in diff --git a/src/soc2c.ml b/src/soc2c.ml index 0142d6abfe475f54bd30b5b0101d2b0dac95888d..64bba351afdb1aec9991659d01f029843d1488c0 100644 --- a/src/soc2c.ml +++ b/src/soc2c.ml @@ -1,4 +1,4 @@ -(* Time-stamp: <modified the 21/06/2016 (at 09:48) by Erwan Jahier> *) +(* Time-stamp: <modified the 06/09/2016 (at 11:16) by Erwan Jahier> *) (* let put (os: out_channel) (fmt:('a, unit, string, unit) format4) : 'a = *) diff --git a/src/soc2cExtern.ml b/src/soc2cExtern.ml index ebf31039cb955bc9e6f603e73e4b815cb3c499b5..73b1adb5b920dd8dbc1a09c36f33300a45d958f2 100644 --- a/src/soc2cExtern.ml +++ b/src/soc2cExtern.ml @@ -1,4 +1,4 @@ -(* Time-stamp: <modified the 20/03/2015 (at 17:31) by Erwan Jahier> *) +(* Time-stamp: <modified the 06/09/2016 (at 10:39) by Erwan Jahier> *) open Soc2cIdent @@ -96,7 +96,8 @@ let (const_declaration : LicPrg.t -> string) = open Soc -let (gen_files : Soc.t -> Soc.tbl -> LicPrg.t -> string -> string-> string -> bool * bool) = +let (gen_files : Soc.t -> Soc.tbl -> LicPrg.t -> string -> string -> string -> + bool * bool) = fun msoc stbl licprg ext_cfile ext_hfile hfile -> let extern_steps = SocMap.fold (fun sk soc acc -> @@ -113,7 +114,7 @@ let (gen_files : Soc.t -> Soc.tbl -> LicPrg.t -> string -> string-> string -> bo (fun _ c acc -> match c with Lic.Extern_const_eff(ec,_) -> ec::acc | _ -> acc) licprg [] in - let needs_cfile = extern_steps <> [] in + let needs_cfile = extern_steps <> [] || extern_consts <> [] in let needs_hfile = needs_cfile || extern_types<>[] || extern_consts<>[] in if not (Sys.file_exists ext_hfile) && needs_hfile then ( diff --git a/src/soc2cGenAssign.ml b/src/soc2cGenAssign.ml index b5f1453a391f3998aad55803c403f98e759f6e83..2293691521233ba8f18a7365ef9c67efc3f235b8 100644 --- a/src/soc2cGenAssign.ml +++ b/src/soc2cGenAssign.ml @@ -1,4 +1,4 @@ -(* Time-stamp: <modified the 26/02/2015 (at 13:48) by Erwan Jahier> *) +(* Time-stamp: <modified the 06/09/2016 (at 11:15) by Erwan Jahier> *) open Data open Lic @@ -45,13 +45,14 @@ let (gen_used_types : Soc.t list -> Data.t list) = in let acc = List.fold_left aux DataSet.empty socs in DataSet.elements acc - + (* exported *) let (f: Data.t -> string) = fun t -> let t_str = Soc2cIdent.type_to_short_string t in - let t_def = Printf.sprintf " + let t_def = + Printf.sprintf " #ifndef _assign_%s #define _assign_%s(dest, source, size) memcpy(dest, source, size) #endif diff --git a/src/soc2cGenAssign.mli b/src/soc2cGenAssign.mli index cd02306d454342b8385cc46055d91d11ae0bdec4..0abc6108764a9d2a760b294f9f437a81cd08cb3c 100644 --- a/src/soc2cGenAssign.mli +++ b/src/soc2cGenAssign.mli @@ -1,4 +1,4 @@ - (* Time-stamp: <modified the 08/10/2014 (at 18:35) by Erwan Jahier> *) + (* Time-stamp: <modified the 06/09/2016 (at 11:07) by Erwan Jahier> *) (* Returns the list of non-trivial data types (i.e., arrays and extern) that are used in a program, with no duplicates *) diff --git a/src/socPredef.ml b/src/socPredef.ml index 26d6ccae1788a9bc74973618ff3ecac82a5ea3ab..b3b51548e8099366d1e196a2ff6bd6dad3d50773 100644 --- a/src/socPredef.ml +++ b/src/socPredef.ml @@ -1,4 +1,4 @@ -(* Time-stamp: <modified the 27/05/2016 (at 16:02) by Erwan Jahier> *) +(* Time-stamp: <modified the 08/09/2016 (at 17:08) by Erwan Jahier> *) (** Synchronous Object Code for Predefined operators. *) @@ -485,65 +485,65 @@ let output_type_of_op op tl = let (soc_interface_of_pos_op: Lxm.t -> Lic.by_pos_op -> Data.t list -> Soc.var_expr option -> Soc.t) = fun lxm op types fby_init_opt -> - match (op, types,fby_init_opt) with - - | Lic.PREDEF_CALL ({Lxm.it=("Lustre","if"),[]}),_ ,_ -> - let concrete_type = List.nth types 1 in - let soc = of_soc_key ("Lustre::if", types@[concrete_type], Nomore) in - instanciate_soc soc concrete_type - | Lic.PREDEF_CALL {Lxm.it=(op,sargs)}, _, _ -> - assert (sargs=[]); - let soc_name = Lv6Id.string_of_long op in - let out_type = output_type_of_op soc_name types in - let soc = of_soc_key (soc_name, types@[out_type], Nomore) in - soc - | Lic.FBY, _, Some init -> - let concrete_type = List.nth types 0 in - let soc = of_fby_soc_key init (("Lustre::fby"), - types@[concrete_type], MemInit init) in - instanciate_soc soc concrete_type - | Lic.FBY, _, None -> assert false (* should ot occur *) - | Lic.PRE, _, _ -> - let concrete_type = List.nth types 0 in - let soc = of_soc_key (("Lustre::pre"), types@[concrete_type], Nomore) in - instanciate_soc soc concrete_type - | Lic.CURRENT (Some(cc)), _, _ -> - let concrete_type = try List.nth types 1 with _ -> assert false in - let soc = of_soc_key (("Lustre::current"), types@[concrete_type], Curr(cc)) in - instanciate_soc soc concrete_type - | Lic.CURRENT (_), _, _ -> assert false - | Lic.ARROW, _, _ -> - let concrete_type = List.nth types 0 in - let soc = of_soc_key (("Lustre::arrow"), types@[concrete_type], - MemInit(Const("_true", Data.Bool))) - in - let soc = instanciate_soc soc concrete_type in - soc - | Lic.HAT i,_, _ -> - let elt_type = List.nth types 0 in - (make_hat_soc i elt_type) - - | Lic.ARRAY, _, _ -> - let elt_type = List.nth types 0 in - let i = (List.length types) in - (make_array_soc i elt_type) - - | Lic.ARRAY_SLICE sinfo, [Array (t, s)], _ -> (make_array_slice_soc sinfo s t) - | Lic.ARRAY_SLICE sinfo, _, _ -> assert false - - | Lic.CONCAT, [Array (t1, s1); Array (t2, s2)], _-> - assert (t1=t2); - (make_array_concat_soc s1 s2 t1) - | Lic.CONCAT , _, _ -> assert false - - | Lic.CALL _,_,_ -> assert false - | Lic.CONST _ , _,_ -> assert false - - (* Those are not soc *) - | Lic.VAR_REF _, _,_ -> assert false - | Lic.CONST_REF _, _,_ -> assert false - | Lic.STRUCT_ACCESS _, _,_ -> assert false - | Lic.WHEN _, _,_ -> assert false - | Lic.TUPLE, _,_ -> assert false - | Lic.ARRAY_ACCES _, _,_ -> assert false + match (op, types,fby_init_opt) with + + | Lic.PREDEF_CALL ({Lxm.it=("Lustre","if"),[]}),_ ,_ -> + let concrete_type = List.nth types 1 in + let soc = of_soc_key ("Lustre::if", types@[concrete_type], Nomore) in + instanciate_soc soc concrete_type + | Lic.PREDEF_CALL {Lxm.it=(op,sargs)}, _, _ -> + assert (sargs=[]); + let soc_name = Lv6Id.string_of_long op in + let out_type = output_type_of_op soc_name types in + let soc = of_soc_key (soc_name, types@[out_type], Nomore) in + soc + | Lic.FBY, _, Some init -> + let concrete_type = List.nth types 0 in + let soc = of_fby_soc_key init (("Lustre::fby"), + types@[concrete_type], MemInit init) in + instanciate_soc soc concrete_type + | Lic.FBY, _, None -> assert false (* should ot occur *) + | Lic.PRE, _, _ -> + let concrete_type = List.nth types 0 in + let soc = of_soc_key (("Lustre::pre"), types@[concrete_type], Nomore) in + instanciate_soc soc concrete_type + | Lic.CURRENT (Some(cc)), _, _ -> + let concrete_type = try List.nth types 1 with _ -> assert false in + let soc = of_soc_key (("Lustre::current"), types@[concrete_type], Curr(cc)) in + instanciate_soc soc concrete_type + | Lic.CURRENT (_), _, _ -> assert false (* sno *) + | Lic.ARROW, _, _ -> + let concrete_type = List.nth types 0 in + let soc = of_soc_key (("Lustre::arrow"), types@[concrete_type], + MemInit(Const("_true", Data.Bool))) + in + let soc = instanciate_soc soc concrete_type in + soc + | Lic.HAT i,_, _ -> + let elt_type = List.nth types 0 in + (make_hat_soc i elt_type) + + | Lic.ARRAY, _, _ -> + let elt_type = List.nth types 0 in + let i = (List.length types) in + (make_array_soc i elt_type) + + | Lic.ARRAY_SLICE sinfo, [Array (t, s)], _ -> (make_array_slice_soc sinfo s t) + | Lic.ARRAY_SLICE sinfo, _, _ -> assert false + + | Lic.CONCAT, [Array (t1, s1); Array (t2, s2)], _-> + assert (t1=t2); + (make_array_concat_soc s1 s2 t1) + | Lic.CONCAT , _, _ -> assert false + + | Lic.CALL _,_,_ -> assert false + | Lic.CONST _ , _,_ -> assert false + + (* Those are not soc *) + | Lic.VAR_REF _, _,_ -> assert false + | Lic.CONST_REF _, _,_ -> assert false + | Lic.STRUCT_ACCESS _, _,_ -> assert false + | Lic.WHEN _, _,_ -> assert false + | Lic.TUPLE, _,_ -> assert false + | Lic.ARRAY_ACCES _, _,_ -> assert false diff --git a/test/lus2lic.sum b/test/lus2lic.sum index 69f4191fa9e6dff0672a73bbc1167fa4159a41f6..91481c680e48a72a2cc7d0dc76507beb8bb9b29b 100644 --- a/test/lus2lic.sum +++ b/test/lus2lic.sum @@ -1,5 +1,5 @@ ==> lus2lic0.sum <== -Test Run By jahier on Mon Sep 5 10:06:53 +Test Run By jahier on Fri Sep 9 10:20:20 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 Mon Sep 5 10:06:53 +Test Run By jahier on Fri Sep 9 10:20:21 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 Sep 5 10:07:10 +Test Run By jahier on Fri Sep 9 10:20:42 Native configuration is x86_64-unknown-linux-gnu === lus2lic2 tests === @@ -743,7 +743,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 Sep 5 10:07:47 +Test Run By jahier on Fri Sep 9 10:21:25 Native configuration is x86_64-unknown-linux-gnu === lus2lic3 tests === @@ -1249,7 +1249,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 Sep 5 10:07:59 +Test Run By jahier on Fri Sep 9 10:21:39 Native configuration is x86_64-unknown-linux-gnu === lus2lic4 tests === @@ -1773,14 +1773,14 @@ PASS: /home/jahier/lus2lic/test/../utils/test_lus2lic_no_node zzz2.lus {} # of unexpected failures 4 =============================== # Total number of failures: 26 -lus2lic0.log:testcase ./lus2lic.tests/test0.exp completed in 0 seconds -lus2lic1.log:testcase ./lus2lic.tests/test1.exp completed in 17 seconds -lus2lic2.log:testcase ./lus2lic.tests/test2.exp completed in 37 seconds -lus2lic3.log:testcase ./lus2lic.tests/test3.exp completed in 11 seconds -lus2lic4.log:testcase ./lus2lic.tests/test4.exp completed in 31 seconds +lus2lic0.log:testcase ./lus2lic.tests/test0.exp completed in 1 seconds +lus2lic1.log:testcase ./lus2lic.tests/test1.exp completed in 21 seconds +lus2lic2.log:testcase ./lus2lic.tests/test2.exp completed in 43 seconds +lus2lic3.log:testcase ./lus2lic.tests/test3.exp completed in 13 seconds +lus2lic4.log:testcase ./lus2lic.tests/test4.exp completed in 34 seconds * Ref time: -0.06user 0.03system 1:37.55elapsed 0%CPU (0avgtext+0avgdata 5624maxresident)k -128inputs+0outputs (0major+6050minor)pagefaults 0swaps +0.04user 0.02system 1:53.24elapsed 0%CPU (0avgtext+0avgdata 5660maxresident)k +0inputs+0outputs (0major+6112minor)pagefaults 0swaps * Quick time (-j 4): -0.02user 0.06system 0:45.45elapsed 0%CPU (0avgtext+0avgdata 5684maxresident)k -32inputs+0outputs (0major+6082minor)pagefaults 0swaps +0.04user 0.02system 1:15.54elapsed 0%CPU (0avgtext+0avgdata 5640maxresident)k +0inputs+0outputs (0major+6117minor)pagefaults 0swaps