diff --git a/_oasis b/_oasis index dbbac0ad171ef5cbede865860ac46046289d584e..a04aa0a934aa356e496e7a51a7ec9f220972fa90 100644 --- a/_oasis +++ b/_oasis @@ -1,6 +1,6 @@ OASISFormat: 0.4 Name: lustre-v6 -Version: 1.659 +Version: 1.660 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 0f44eed2971ade5a12a54cb13aaa0e7b614a64f8..89bac14106dfbbc27cbf222179e893173466c735 100644 --- a/src/evalClock.ml +++ b/src/evalClock.ml @@ -1,4 +1,4 @@ -(* Time-stamp: <modified the 14/01/2016 (at 10:40) by Erwan Jahier> *) +(* Time-stamp: <modified the 01/09/2016 (at 14:35) by Erwan Jahier> *) open AstPredef @@ -346,7 +346,7 @@ and (eval_by_pos_clock : IdSolver.t -> Lic.by_pos_op -> Lxm.t -> Lic.val_exp lis let current_clock = function | (id, BaseLic) -> (id, BaseLic) | (id, On(_,clk)) -> (id, clk) - | (_, ClockVar _) -> assert false + | (id, ClockVar i) -> (id, ClockVar i) in args, (List.map current_clock (List.flatten clocks_of_args), s) ) diff --git a/src/l2lCheckKcgKeyWord.ml b/src/l2lCheckKcgKeyWord.ml index 8a0d7635f0c34897a31c1f89c2ca13e1624a55c5..ec6499bcf9e7977c1c87fa46c351811055ebdca5 100644 --- a/src/l2lCheckKcgKeyWord.ml +++ b/src/l2lCheckKcgKeyWord.ml @@ -15,24 +15,27 @@ module StringSet = let compare = compare end) -let kcg_kw_list = ["state";"clock";"initial";"abstract"; "activate";"and";"assume";"automaton";"bool";"case"; "char"; "const";"default";"div"; "do";"else"; "elsif"; "emit"; "end"; "enum"; "every";"false"; "fby"; "final"; "flatten"; "fold"; "foldi"; "foldw";" foldwi"; "function"; -"guarantee";"group";"if";"imported";"initial";"int";"is";"last";"let";"make";"map";"mapfold";"mapi"; "mapw";"mapwi";"match";"merge";"mod";"node";"not";"numeric";"of";"onreset";"open";"or";"package";"parameter";"pre";"private";"probe";"public";"real";"restart";"resume";"returns";"reverse";"sensor";"sig";"specialize";"synchro";"tel";"then";"times";"transpose";"true";"unless";"until";"var";"when";"where";"with";"xor"] +let kcg_kw_list = [ + "state";"clock";"initial";"abstract"; "activate";"and"; + "assume";"automaton";"bool";"case"; "char"; "const";"default";"div"; "do"; + "else"; "elsif"; "emit"; "end"; "enum"; "every";"false"; "fby"; "final"; + "flatten"; "fold"; "foldi"; "foldw";" foldwi"; "function";"guarantee"; + "group";"if";"imported";"initial";"int";"is";"last";"let";"make";"map"; + "mapfold";"mapi"; "mapw";"mapwi";"match";"merge";"mod";"node";"not"; + "numeric";"of";"onreset";"open";"or";"package";"parameter";"pre"; + "private";"probe";"public";"real";"restart";"resume";"returns";"reverse"; + "sensor";"sig";"specialize";"synchro";"tel";"then";"times";"transpose";"true"; + "unless";"until";"var";"when";"where";"with";"xor"] let kcg_kw = StringSet.of_list kcg_kw_list let (check_var_info : Lic.var_info -> unit) = - fun v -> - - (match v with - |var_name_eff-> - if StringSet.mem v.var_name_eff kcg_kw then - (let msg = "kcg name clash" in - raise (Lv6errors.Global_error msg) - ); - |_ -> () - ) - - + fun v -> + if StringSet.mem v.var_name_eff kcg_kw then + let msg = "kcg name clash" in + raise (Lv6errors.Global_error msg) + + let (check_type :Lic.type_ -> unit) = fun typ -> (* (match typ.Named_type_exp with diff --git a/src/l2lExpandArrays.ml b/src/l2lExpandArrays.ml index 6f8b71b802f4eb45289ca7b4cc729075bef19276..0137488e4cdda13a21b22e6f1db941a64bcf5e22 100644 --- a/src/l2lExpandArrays.ml +++ b/src/l2lExpandArrays.ml @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 01/06/2016 (at 09:58) by Erwan Jahier> *) +(** Time-stamp: <modified the 02/09/2016 (at 16:10) by Erwan Jahier> *) (* Replace structures and arrays by as many variables as necessary. Since structures can be nested, it migth be a lot of new variables... @@ -46,7 +46,7 @@ type local_ctx = { XXX code dupl. with Split.new_var *) let new_var str lctx type_eff clock_eff = - let id = Lv6Id.of_string (FreshName.local_var str) in + let id = Lv6Id.of_string (FreshName.local_var (str)) in let var = { var_name_eff = id; diff --git a/src/l2lExpandMetaOp.ml b/src/l2lExpandMetaOp.ml index 128226f6add24abdcb349ff68258aa7c1569f7cb..cf38938227c6d824566a0148e2580e447bbfebc8 100644 --- a/src/l2lExpandMetaOp.ml +++ b/src/l2lExpandMetaOp.ml @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 14/01/2016 (at 10:40) by Erwan Jahier> *) +(** Time-stamp: <modified the 02/09/2016 (at 16:11) by Erwan Jahier> *) open Lxm open Lic @@ -14,7 +14,7 @@ type local_ctx = { (********************************************************************************) (* stuff to create fresh var names. *) let new_var str lctx type_eff clock_eff = - let id = Lv6Id.of_string (FreshName.local_var str) in + let id = Lv6Id.of_string (FreshName.local_var (str)) in let var = { var_name_eff = id; diff --git a/src/l2lExpandNodes.ml b/src/l2lExpandNodes.ml index 9135d094cc933fcb71271a225f5c6d217709d0b2..a9469e69cd5817578a2bba8bc22e10dd29543d95 100644 --- a/src/l2lExpandNodes.ml +++ b/src/l2lExpandNodes.ml @@ -1,4 +1,4 @@ -(* Time-stamp: <modified the 14/01/2016 (at 10:41) by Erwan Jahier> *) +(* Time-stamp: <modified the 02/09/2016 (at 16:12) by Erwan Jahier> *) open Lxm @@ -15,7 +15,14 @@ type local_ctx = { } (********************************************************************************) -let new_var = FreshName.var_info +let new_var label str t c = + let vi = FreshName.var_info str t c in + Lv6Verbose.exe + ~flag:dbg + (fun () -> Printf.printf "#EN: new_var[%s](%s)->%s%s'\n" + label str vi.var_name_eff (Lic.string_of_clock (snd c)) + ); + vi (********************************************************************************) let get_locals node = @@ -33,31 +40,61 @@ let rec (get_node_body : local_ctx -> Lic.node_exp -> Lic.node_body option) = | MetaOpLic -> None (********************************************************************************) -type subst = (Lv6Id.t * var_info) list -let rec (substitute : - subst -> Lic.eq_info Lxm.srcflagged -> Lic.eq_info Lxm.srcflagged) = +(* When expanding a node call such as + + x = toto(a when c); + + when toto params are (for example) on the base clock, we need to + propagate the substitution between the toto base clock and "on(c)" + ; for the toto arguments, it's been done during clock checking ; + but we need to remember this information to substitute the clock + of toto in its local variables. +*) +type new_base = clock + +(* to hold the substitution of parameters by arguments *) +module IdMap = Map.Make(struct type t = Lv6Id.t let compare = compare end) +type subst = Lic.var_info IdMap.t + +let (add_subst : subst -> Lv6Id.t -> Lic.var_info -> subst) = + fun s id vi -> IdMap.add id vi s + +let (subst_in_id : subst -> Lv6Id.t -> Lic.var_info) = + fun s id -> IdMap.find id s + +let (subst_in_id_id : subst -> Lv6Id.t -> Lv6Id.t) = + fun s id -> + try (subst_in_id s id).var_name_eff with Not_found -> id + +let rec (substitute : subst * new_base -> + Lic.eq_info Lxm.srcflagged -> Lic.eq_info Lxm.srcflagged) = fun s { it = (lhs,ve) ; src = lxm } -> - let lhs = List.map (subst_in_left s) lhs in + let lhs = List.map (subst_in_left s ) lhs in let newve = subst_in_val_exp s ve in { it = (lhs,newve) ; src = lxm } +and subst_in_var_info (s,_) vi = + try subst_in_id s vi.var_name_eff + with Not_found -> + assert false (* sno : all i/o have been replace ; fresh locs were created *) + and subst_in_left s left = match left with - | LeftVarLic(v,lxm) -> (try LeftVarLic(List.assoc v.var_name_eff s,lxm) with Not_found -> left) - | LeftFieldLic(left,id,t) -> LeftFieldLic(subst_in_left s left,id,t) - | LeftArrayLic(left,i, t) -> LeftArrayLic(subst_in_left s left,i, t) - | LeftSliceLic(left,si,t) -> LeftSliceLic(subst_in_left s left,si,t) + | LeftVarLic(v,lxm) -> LeftVarLic(subst_in_var_info s v,lxm) + | LeftFieldLic(left,id,t) -> LeftFieldLic(subst_in_left s left,id,t) + | LeftArrayLic(left,i, t) -> LeftArrayLic(subst_in_left s left,i, t) + | LeftSliceLic(left,si,t) -> LeftSliceLic(subst_in_left s left,si,t) -and (subst_in_clock : subst -> clock -> clock) = - fun s clk -> +and (subst_in_clock : subst * new_base -> clock -> clock) = + fun (s,new_base) clk -> match clk with - | BaseLic -> BaseLic - | ClockVar i -> ClockVar i + | BaseLic -> new_base + | ClockVar i -> ClockVar i (* sno *) | On ((cc,cv,ct),clk) -> - let cv = try (List.assoc cv s).var_name_eff with Not_found -> cv in - On ((cc,cv,ct), subst_in_clock s clk) + On((cc, subst_in_id_id s cv, ct), subst_in_clock (s,new_base) clk) + -and (subst_in_val_exp : subst -> val_exp -> val_exp) = +and (subst_in_val_exp : subst * new_base -> val_exp -> val_exp) = fun s ve -> let newve = { ve with @@ -70,14 +107,7 @@ and (subst_in_val_exp : subst -> val_exp -> val_exp) = let vel = List.map (subst_in_val_exp s) vel in let by_pos_op = match by_pos_op with | CONST_REF idl -> CONST_REF idl - | VAR_REF id -> - let id' = - try - let var = List.assoc id s in - var.var_name_eff - with Not_found -> id - in - VAR_REF id' + | VAR_REF id -> VAR_REF (subst_in_id_id (fst s) id) | WHEN(clk) -> WHEN(subst_in_clock s clk) | HAT(i) -> HAT(i) | PREDEF_CALL _| CALL _ | PRE | ARROW | FBY | CURRENT _ | TUPLE @@ -97,7 +127,12 @@ and (subst_in_val_exp : subst -> val_exp -> val_exp) = in newve -let mk_loc_subst l1 l2 = List.combine (List.map (fun v -> v.var_name_eff) l1) l2 +let (mk_loc_subst:subst -> Lic.var_info list -> Lic.var_info list -> subst) = + fun s l1 l2 -> + let l = List.combine l1 l2 in + List.fold_left + (fun s (v1,v2) -> add_subst s v1.var_name_eff v2) + s l (********************************************************************************) (** The functions below accumulate @@ -113,60 +148,63 @@ type acc = * (Lic.eq_info srcflagged) list (* equations *) * Lic.var_info list (* new local vars *) -let (mk_fresh_loc : local_ctx -> var_info -> clock -> var_info) = - fun lctx v c -> - new_var (Lv6Id.to_string v.var_name_eff) v.var_type_eff (fst v.var_clock_eff, c) - -(* When expanding a node call such as - - x = toto(a when c); +let (mk_fresh_loc : string -> local_ctx -> var_info -> clock -> var_info) = + fun label lctx v c -> + new_var label ((Lv6Id.to_string v.var_name_eff)) v.var_type_eff (fst v.var_clock_eff, c) - when toto params are (for example) on the base clock, we need to - propagate the substitution between the toto base clock and "on(c)" - ; for the toto arguments, it's been done during clock checking ; - but we need to remember this information to substitute the clock - of toto in its local variables. -*) -type clock_substs = (clock * clock) list + +let rec get_new_base c_arg c_par = + match c_arg, c_par with + | _, BaseLic -> c_arg + | On(_,c_arg), On(_,c_par) -> get_new_base c_arg c_par + | _,_ -> assert false (* sno *) -let (add_clock_subst: clock -> clock -> clock_substs -> clock_substs) = - fun c1 c2 cs -> - if List.mem_assoc c1 cs then cs else (c1,c2)::cs - -let (mk_input_subst: local_ctx -> Lxm.t -> var_info list -> - Lic.val_exp list -> acc -> subst * acc * clock_substs) = - fun lctx lxm vl vel acc -> - assert(List.length vl = List.length vel); + +let (mk_input_subst: local_ctx -> Lxm.t -> var_info list -> + Lic.val_exp list -> acc -> subst * acc * new_base option) = + fun lctx lxm vl vel acc -> + assert(List.length vl = List.length vel); + let s, acc, new_base_opt = List.fold_left2 - (fun (s,(a_acc,e_acc,v_acc),cs) v ve -> - (* we create a new var for each node argument, which is a little - bit « bourrin » if ever ve is a simple ident... *) - let clk = match ve.ve_clk with - | [c] -> c + (fun (s,(a_acc,e_acc,v_acc),nbase_opt) v ve -> + (* we create a new var for each node argument to make sure + that there is no expression in arguments. Is is generally + useless because of the l2lSplit pass, but, well... *) + let carg,cpar = match ve.ve_clk, v.var_clock_eff with + | [c1],(_,c2) -> c1,c2 | _ -> assert false in - let nv = mk_fresh_loc lctx v clk in + let new_base = get_new_base carg cpar in + let nv = mk_fresh_loc "input" lctx v carg in let neq = [LeftVarLic(nv,lxm)],ve in let neq = flagit neq lxm in - let cs = add_clock_subst (snd v.var_clock_eff) clk cs in - (v.var_name_eff,nv)::s,(a_acc, neq::e_acc, nv::v_acc), cs + let nbase_opt = match nbase_opt with + | None -> Some(new_base) + | Some(b) -> assert(b=new_base); Some(b) + in + add_subst s v.var_name_eff nv, + (a_acc, neq::e_acc, nv::v_acc), + nbase_opt ) - ([],acc,[]) + (IdMap.empty, acc, None) vl vel + in + s, acc, new_base_opt -(* create fresh vars if necessary *) -let (mk_output_subst : local_ctx -> Lxm.t -> var_info list -> Lic.left list -> clock_substs -> - acc -> subst * acc * clock_substs) = - fun lctx lxm vl leftl cs acc -> - assert(List.length vl = List.length leftl); +(* Create fresh vars if necessary, ie, if we have no trivial left parts *) +let (mk_output_subst : local_ctx -> Lxm.t -> subst -> var_info list -> Lic.left list -> + new_base option-> acc -> subst * acc * new_base) = + fun lctx lxm s vl leftl new_base_opt acc -> + assert(List.length vl = List.length leftl); + let s,acc,new_base_opt = List.fold_left2 - (fun (s,acc,cs) v left -> + (fun (s,acc,new_base_opt) v left -> match left with - | LeftVarLic(v2,lxm) -> (v.var_name_eff,v2)::s, acc,cs + | LeftVarLic(v2,lxm) -> add_subst s v.var_name_eff v2, acc,new_base_opt | _ -> let clk = Lic.clock_of_left left in - let nv = mk_fresh_loc lctx v clk in + let nv = mk_fresh_loc "output" lctx v clk in let nv_id = nv.var_name_eff in let nve = { ve_core = CallByPosLic({it=VAR_REF nv_id;src = lxm },[]); @@ -184,18 +222,29 @@ let (mk_output_subst : local_ctx -> Lxm.t -> var_info list -> Lic.left list -> c - create the substition n_output_par/_v *) let (aa,ae,av) = acc in - let cs = add_clock_subst (snd v.var_clock_eff) clk cs in - (v.var_name_eff,nv)::s, (aa, neq::ae, nv::av), cs + let new_base = get_new_base (Lic.clock_of_left left) (snd v.var_clock_eff) in + let new_base_opt = + match new_base_opt with + | Some x -> assert(x=new_base); Some x + | None -> Some new_base + in + add_subst s v.var_name_eff nv, (aa, neq::ae, nv::av), new_base_opt ) - ([],acc,cs) + (s,acc,new_base_opt) vl leftl - + in + let new_base = match new_base_opt with + | Some x -> x + | None -> assert false (* a node outgth to have at least an input or an output *) + in + s,acc,new_base + 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 | lctx, None -> lctx, (asserts, { src = lxm_eq ; it = eq }::eqs, locs) - | lctx, Some(nasserts, neqs, nlocs) -> + | lctx, Some(nasserts, neqs, nlocs) -> (lctx, (List.rev_append nasserts asserts, List.rev_append neqs eqs, @@ -243,29 +292,45 @@ and (expand_eq_aux: local_ctx -> Lic.eq_info -> local_ctx * acc option)= let node = node.it in let node_locs = get_locals node in let acc = [],[],[] in - let is,acc,cs = mk_input_subst lctx lxm node.inlist_eff vel acc in - let os,acc,cs = mk_output_subst lctx lxm node.outlist_eff lhs cs acc in + (* rename i/o using the calling context *) + let s,acc,new_base = mk_input_subst lctx lxm node.inlist_eff vel acc in + let s,acc,new_base = mk_output_subst lctx lxm s node.outlist_eff + lhs new_base acc in let rec (substitute_clock : clock -> clock) = fun c -> - try List.assoc c cs - with Not_found -> - match c with - | BaseLic - | ClockVar _ -> c (* XXX should/can it happen? *) - | On(v,clk) -> On(v, substitute_clock clk) + match c with + | BaseLic -> new_base + | ClockVar _ -> new_base (* SNO *) + | On(v,clk) -> On(v, substitute_clock clk) in - let clks = List.map (fun v -> substitute_clock (snd v.var_clock_eff)) node_locs in - let fresh_locs = List.map2 (mk_fresh_loc lctx) node_locs clks in - let ls = mk_loc_subst node_locs fresh_locs in - let s = List.rev_append is (List.rev_append os ls) in + let clks = List.map (fun v -> snd v.var_clock_eff) node_locs in + (* rename locals with fresh names to avoid clashes among locals *) + let fresh_locs = List.map2 (mk_fresh_loc "local" lctx) node_locs clks in + let s = mk_loc_subst s node_locs fresh_locs in let fresh_locs = (* substitute the new vars in clocks *) List.map (fun v -> let id,clk = v.var_clock_eff in - { v with var_clock_eff = id, subst_in_clock s clk }) + { v with var_clock_eff = + subst_in_id_id s id, subst_in_clock (s,new_base) clk }) + fresh_locs + in + let fresh_locs = + List.map + (fun v -> + let id,clk = v.var_clock_eff in + Lv6Verbose.exe + ~flag:dbg + (fun () -> + Printf.printf "#EN: remplace the base clk of %s by '%s'\n" + v.var_name_eff + (Lic.string_of_clock new_base)); + let clk = substitute_clock clk in + { v with var_clock_eff = id,clk } + ) 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 node_eqs = List.map (substitute (s, new_base)) node_eqs in + let subst_assert x = Lxm.flagit (subst_in_val_exp (s,new_base) x.it) x.src in 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 @@ -285,7 +350,7 @@ and (expand_assert : local_ctx * acc -> val_exp srcflagged -> local_ctx * acc) = let lxm = ve.src in let ve = ve.it in let clk = Lv6Id.of_string "dummy_expand_assert", BaseLic in - let assert_var = new_var "assert" Bool_type_eff clk in + let assert_var = new_var "assert" "assert" Bool_type_eff clk in let assert_eq = Lxm.flagit ([LeftVarLic(assert_var,lxm)], ve) lxm in let assert_op = Lic.VAR_REF(assert_var.var_name_eff) in let nve = { @@ -306,7 +371,7 @@ and (expand_node : local_ctx -> Lic.node_exp -> local_ctx * Lic.node_exp) = | ExternLic | AbstractLic _ -> lctx, n | BodyLic b -> - let locs = get_locals n in + 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 @@ -322,7 +387,7 @@ and (expand_node : local_ctx -> Lic.node_exp -> local_ctx * Lic.node_exp) = } in Lv6Verbose.exe ~flag:dbg (fun () -> - Printf.printf "#DBG: expand nodes of '%s'\n" + Printf.printf "#EN: '%s'\n" (Lic.string_of_node_key n.node_key_eff)); lctx, res | MetaOpLic -> lctx, n diff --git a/src/l2lNoWhenNot.ml b/src/l2lNoWhenNot.ml index acada301642af37c3a272c7f1f9aced0b782cc55..623331d5a81484b5b280439a8393a22807a67825 100644 --- a/src/l2lNoWhenNot.ml +++ b/src/l2lNoWhenNot.ml @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 30/08/2016 (at 14:18) by Erwan Jahier> *) + (** Time-stamp: <modified the 05/09/2016 (at 10:15) by Erwan Jahier> *) open Lxm open Lic @@ -22,25 +22,26 @@ type acc = * Lic.val_exp srcflagged list (* assertions *) * clock_tbl -let new_var cv type_eff clock_eff clk_tbl = +let new_var label cv type_eff sclk clk_tbl = try Hashtbl.find clk_tbl cv, true with Not_found -> let id = Lv6Id.of_string (FreshName.local_var cv) in Lv6Verbose.exe ~flag:dbg (fun() -> Printf.printf - "L2lNoWhenNot: negation of '%s' not found; create %s\n" cv id); - let var = { + "#NWN: negation of '%s' not found; create %s(%s) [%s]\n" + cv id (Lic.string_of_clock sclk) label); + let var = { var_name_eff = id; var_nature_eff = AstCore.VarLocal; var_number_eff = -1; var_type_eff = type_eff; - var_clock_eff = id,clock_eff; + var_clock_eff = id, sclk; } in Hashtbl.add clk_tbl cv var; var,false - + (********************************************************************************) (* The one that performs the real work, namely: @@ -48,10 +49,10 @@ let new_var cv type_eff clock_eff clk_tbl = - invent a fresh var name NV, - generate the equation defining NV (NV= not v);) *) -let (gen_ident : Lxm.t -> Lv6Id.t -> type_ -> Lic.clock -> acc -> +let (gen_ident : string -> Lxm.t -> Lv6Id.t -> type_ -> Lic.clock -> acc -> var_info * acc ) = - fun lxm cv ct clk (vl,eql,al,tbl) -> - let nv, already_done = new_var cv ct clk tbl in + fun label lxm cv ct clk (vl,eql,al,tbl) -> + let nv, already_done = new_var label cv ct clk tbl in if already_done then nv, (vl,eql,al,tbl) else @@ -76,7 +77,9 @@ let (gen_ident : Lxm.t -> Lv6Id.t -> type_ -> Lic.clock -> acc -> let rec update_clock : Lxm.t -> acc -> clock -> clock * acc = fun lxm acc clk -> match clk with - | BaseLic | ClockVar _ -> clk, acc + | BaseLic -> clk, acc + | ClockVar _ -> clk, acc + (* XXXX assert false *) | On((cc,cv,ct),sclk) -> let sclk, acc = update_clock lxm acc sclk in if cc <> ("Lustre","false") then @@ -85,8 +88,12 @@ let rec update_clock : Lxm.t -> acc -> clock -> clock * acc = let nv, acc = let (_,_,_,clk_tbl) = acc in try Hashtbl.find clk_tbl cv, acc - with Not_found -> gen_ident lxm cv ct sclk acc + with Not_found -> gen_ident "ici" lxm cv ct sclk acc in + Lv6Verbose.exe + ~flag:dbg + (fun() -> Printf.printf + "#NWN: not(%s) -> %s\n" cv nv.var_name_eff); On((("Lustre","true"),nv.var_name_eff, Bool_type_eff), sclk), acc let rec update_clock_list : Lxm.t -> clock list * acc -> clock -> clock list * acc = @@ -94,12 +101,21 @@ let rec update_clock_list : Lxm.t -> clock list * acc -> clock -> clock list * a let clk, acc = update_clock lxm acc clk in clk::res, acc - + let update_var_info : Lxm.t -> acc -> var_info -> var_info * acc = fun lxm acc vi -> let (id, clk) = vi.var_clock_eff in - let clk, acc = update_clock lxm acc clk in - { vi with var_clock_eff = id, clk }, acc + let nclk, acc = update_clock lxm acc clk in + Lv6Verbose.exe + ~flag:dbg + (fun() -> + if clk <> nclk then ( + Printf.printf + "#NWN: update_var_info of %s (%s->%s\n" + vi.var_name_eff + (Lic.string_of_clock clk) (Lic.string_of_clock nclk) + )); + { vi with var_clock_eff = id, nclk }, acc let update_var_info_list : Lxm.t -> var_info list * acc -> var_info -> var_info list * acc = @@ -180,7 +196,7 @@ and (do_val_exp: LicPrg.t -> val_exp -> acc -> val_exp * acc) = let nv, acc = let (_,_,_,clk_tbl) = acc in try Hashtbl.find clk_tbl cv, acc - with Not_found -> gen_ident op.src cv Bool_type_eff clk acc + with Not_found -> gen_ident "la" op.src cv Bool_type_eff clk acc in let true_cc = "Lustre","true" in let new_op = WHEN (On((true_cc, nv.var_name_eff, Bool_type_eff),clk)) in @@ -254,7 +270,7 @@ let rec (doit : LicPrg.t -> LicPrg.t) = (** transform nodes *) let rec (doit_node : Lic.node_key -> Lic.node_exp -> LicPrg.t -> LicPrg.t) = fun nk ne outprg -> - Lv6Verbose.exe ~flag:dbg (fun() -> Printf.printf "#DBG: L2lNoWhenNot '%s'\n" + Lv6Verbose.exe ~flag:dbg (fun() -> Printf.printf "#NWN: '%s'\n" (Lic.string_of_node_key nk)); let ne = do_node inprg ne in LicPrg.add_node nk ne outprg diff --git a/src/l2lWhenOnId.ml b/src/l2lWhenOnId.ml index da21228b3905c5f3a93c015a6e84e7b4878d28f0..ecba0ccd9260473dda799eb45939d13b7c1c7303 100644 --- a/src/l2lWhenOnId.ml +++ b/src/l2lWhenOnId.ml @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 30/08/2016 (at 14:18) by Erwan Jahier> *) +(** Time-stamp: <modified the 02/09/2016 (at 16:11) by Erwan Jahier> *) open Lxm open Lic @@ -27,11 +27,11 @@ let new_var (cc,cv) type_eff clock_eff clk_tbl = with Not_found -> let str = (snd cc) ^ "_" ^ cv in let str2 = (snd cc) ^ "(" ^ cv ^")" in + let id = Lv6Id.of_string (FreshName.local_var (str)) in Lv6Verbose.exe ~flag:dbg (fun() -> Printf.printf - "L2lWhenOnId: '%s' not found; create a var\n" str2); - let id = Lv6Id.of_string (FreshName.local_var str) in + "L2lWhenOnId: '%s' not found; create %s\n" str2 id); let var = { var_name_eff = id; diff --git a/src/lic.ml b/src/lic.ml index db8d35d0b02e6bdc2346f3167578a7b0c6756ab7..f1988a0c254c81188ae22402a535c62084214939 100644 --- a/src/lic.ml +++ b/src/lic.ml @@ -1,4 +1,4 @@ -(* Time-stamp: <modified the 07/07/2016 (at 10:23) by Erwan Jahier> *) +(* Time-stamp: <modified the 01/09/2016 (at 15:39) by Erwan Jahier> *) (** Define the Data Structure representing Compiled programs. By compiled we mean that constant are propagated, packages are @@ -661,8 +661,9 @@ and string_of_const = function and string_of_var_info x = (AstCore.string_of_var_nature x.var_nature_eff) ^ " " ^ (Lv6Id.to_string x.var_name_eff) ^ ":"^(string_of_type x.var_type_eff)^ - (string_of_clock (snd x.var_clock_eff)^"("^ (Lv6Id.to_string (fst x.var_clock_eff)) ^","^ - (string_of_int x.var_number_eff)^")") + (string_of_clock (snd x.var_clock_eff)^"(" + ^ (Lv6Id.to_string (fst x.var_clock_eff)) ^","^ + (string_of_int x.var_number_eff)^")") and string_of_var_list vl = String.concat " ; " (List.map string_of_var_info vl) diff --git a/src/licDump.ml b/src/licDump.ml index 88c9b8697ba56057a3162d437d4db908c3db9200..fa3f28a77b40df50be4390b4d314dcd6753c24a7 100644 --- a/src/licDump.ml +++ b/src/licDump.ml @@ -1,4 +1,4 @@ -(* Time-stamp: <modified the 26/08/2016 (at 16:49) by Erwan Jahier> *) +(* Time-stamp: <modified the 02/09/2016 (at 10:28) by Erwan Jahier> *) open Lv6errors open Printf @@ -760,11 +760,7 @@ and node_of_node_exp_eff (neff: Lic.node_exp): string = )^(if global_opt.kcg then if neff.def_eff = ExternLic then "imported " else "" else "") - ^(if global_opt.kcg then - string_of_node_key_rec (not global_opt.no_prefix) neff.node_key_eff - else - string_of_node_key_rec global_opt.no_prefix neff.node_key_eff - )^( + ^(string_of_node_key_rec global_opt.no_prefix neff.node_key_eff)^( profile_of_node_exp_eff neff ) ^ diff --git a/src/licPrg.ml b/src/licPrg.ml index e7dd3a4fa5afbc433715a6bbf90c0200e229b8d9..be2c2bcb26e084d244214c24ba2c9ba9c5150268 100644 --- a/src/licPrg.ml +++ b/src/licPrg.ml @@ -1,4 +1,4 @@ -(* Time-stamp: <modified the 31/05/2016 (at 15:30) by Erwan Jahier> *) +(* Time-stamp: <modified the 05/09/2016 (at 10:26) by Erwan Jahier> *) open Lv6MainArgs module ItemKeyMap = struct @@ -137,13 +137,13 @@ let to_file (opt: Lv6MainArgs.t) (this:t) (main_node: Lv6Id.idref option) = if (global_opt.Lv6MainArgs.lv4) then () else ( ItemKeyMap.iter (fun tn te -> - if (Lic.is_extern_type te) && ( - global_opt.Lv6MainArgs.kcg || - Lv6MainArgs.global_opt.Lv6MainArgs.expand_enums = AsEnum) - then + (* if (Lic.is_extern_type te) && ( *) + (* global_opt.Lv6MainArgs.kcg || *) + (* Lv6MainArgs.global_opt.Lv6MainArgs.expand_enums = AsEnum) *) + (* then *) output_string opt.Lv6MainArgs.oc (LicDump.type_decl tn te) - else - () + (* else *) + (* () *) ) this.types ); diff --git a/src/lv6Compile.ml b/src/lv6Compile.ml index ef55bab6fad6e391b6af8e2dcf4ac4daf237c683..a18dd58c8c51c70c3e9aae8d32613249c0f067e3 100644 --- a/src/lv6Compile.ml +++ b/src/lv6Compile.ml @@ -1,4 +1,4 @@ -(* Time-stamp: <modified the 26/08/2016 (at 15:39) by Erwan Jahier> *) +(* Time-stamp: <modified the 31/08/2016 (at 17:26) by Erwan Jahier> *) open Lxm open Lv6errors @@ -130,10 +130,10 @@ let (doit : Lv6MainArgs.t -> AstV6.pack_or_model list -> Lv6Id.idref option -> L zelic in let zelic = - if not Lv6MainArgs.global_opt.Lv6MainArgs.no_when_not then zelic else ( + if not Lv6MainArgs.global_opt.Lv6MainArgs.no_when_not then zelic else ( profile_info "Replace 'when not' statements by new variables...\n"; L2lNoWhenNot.doit zelic) - in + in (* Array and struct expansion: to do after polymorphism elimination and after node expansion *) let zelic = if not opt.Lv6MainArgs.expand_arrays then zelic else ( diff --git a/src/lv6Id.ml b/src/lv6Id.ml index de3edeb79c1313cade52d9f8f477c13b792ff3cd..3f93533ec12434d35e58f0bdd459943409836754 100644 --- a/src/lv6Id.ml +++ b/src/lv6Id.ml @@ -1,4 +1,4 @@ -(* Time-stamp: <modified the 27/05/2016 (at 16:02) by Erwan Jahier> *) +(* Time-stamp: <modified the 02/09/2016 (at 13:09) by Erwan Jahier> *) (* J'ai appele ca symbol (mais ca remplace le ident) : c'est juste une couche qui garantit l'unicite en memoire @@ -74,9 +74,14 @@ let (string_of_long : long -> string) = | "Lustre","true" -> "true" | "Lustre","false" -> "false" | _,_ -> -(* if Lv6MainArgs.global_opt.Lv6MainArgs.no_prefix then id else *) - Printf.sprintf "%s%s%s" pn sep id + (* if Lv6MainArgs.global_opt.Lv6MainArgs.no_prefix then id else *) + Printf.sprintf "%s%s%s" pn sep id +let (string_of_long2 : long -> string) = + fun (pn, id) -> + Printf.sprintf "%s::%s" pn id + + let (no_pack_string_of_long : long -> string) = fun (pn, id) -> id diff --git a/src/lv6Id.mli b/src/lv6Id.mli index 02d7886e5c1b33655188fbcbe57ed80d77cbe481..dcf8e7d208ed72ee0120b898f3b73ab6300cfbaa 100644 --- a/src/lv6Id.mli +++ b/src/lv6Id.mli @@ -1,4 +1,4 @@ -(* Time-stamp: <modified the 31/05/2016 (at 17:34) by Erwan Jahier> *) +(* Time-stamp: <modified the 02/09/2016 (at 12:56) by Erwan Jahier> *) (** *) @@ -15,6 +15,7 @@ val pack_name_to_string : pack_name -> string val pack_of_long : long -> pack_name val string_of_long : long -> string +val string_of_long2 : long -> string val long_of_string : string -> long (** To ignore pack name (meaningful when generating ec code for exemple *) diff --git a/src/lv6MainArgs.ml b/src/lv6MainArgs.ml index 81ab7f106fcf85e00249868900a8f753b8714206..5183ccbf01c9e4853346a89c23baf31134cab34f 100644 --- a/src/lv6MainArgs.ml +++ b/src/lv6MainArgs.ml @@ -1,4 +1,4 @@ -(* Time-stamp: <modified the 26/08/2016 (at 16:57) by Erwan Jahier> *) +(* Time-stamp: <modified the 05/09/2016 (at 10:28) 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, @@ -243,7 +243,6 @@ let set_ec_options opt = set_v4_options opt; global_opt.ec <- true; global_opt.no_when_not <- true; - global_opt.no_when_not <- true; global_opt.no_prefix <- true; opt.expand_nodes <- true; () diff --git a/src/lv6version.ml b/src/lv6version.ml index 34c6731dd99e3e392ce88ae22893c518857c3a2d..0e019745261315d98085fb7bf0c7e44d033fbc14 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 = "659" -let sha_1 = "45552c629fedcb120c3fa59e5a71293bce192ec7" +let commit = "660" +let sha_1 = "9c822b3b5e15c279cb863183108cc3a9598abae4" let str = (branch ^ "." ^ commit ^ " (" ^ sha_1 ^ ")") let maintainer = "jahier@imag.fr" diff --git a/src/socUtils.ml b/src/socUtils.ml index a009800a1a8e0ce8e79267b37275ae2330f986fc..eb0f52800446572d5f699f5716bed1f735f2a69d 100644 --- a/src/socUtils.ml +++ b/src/socUtils.ml @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 27/05/2016 (at 16:02) by Erwan Jahier> *) +(** Time-stamp: <modified the 02/09/2016 (at 13:03) by Erwan Jahier> *) open Soc diff --git a/test/lus2lic.sum b/test/lus2lic.sum index ebecc9090baf7c0626cf79e93d4e093180f4d352..69f4191fa9e6dff0672a73bbc1167fa4159a41f6 100644 --- a/test/lus2lic.sum +++ b/test/lus2lic.sum @@ -1,5 +1,5 @@ ==> lus2lic0.sum <== -Test Run By jahier on Tue Aug 30 14:29:56 +Test Run By jahier on Mon Sep 5 10:06:53 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 Aug 30 14:29:57 +Test Run By jahier on Mon Sep 5 10:06:53 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 Aug 30 14:30:14 +Test Run By jahier on Mon Sep 5 10:07:10 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 Tue Aug 30 14:30:52 +Test Run By jahier on Mon Sep 5 10:07:47 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 Tue Aug 30 14:31:04 +Test Run By jahier on Mon Sep 5 10:07:59 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 1 seconds -lus2lic1.log:testcase ./lus2lic.tests/test1.exp completed in 16 seconds +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 39 seconds +lus2lic4.log:testcase ./lus2lic.tests/test4.exp completed in 31 seconds * Ref time: -0.07user 0.02system 1:46.41elapsed 0%CPU (0avgtext+0avgdata 5560maxresident)k -128inputs+0outputs (0major+6076minor)pagefaults 0swaps +0.06user 0.03system 1:37.55elapsed 0%CPU (0avgtext+0avgdata 5624maxresident)k +128inputs+0outputs (0major+6050minor)pagefaults 0swaps * Quick time (-j 4): -0.06user 0.01system 0:50.20elapsed 0%CPU (0avgtext+0avgdata 5680maxresident)k -64inputs+0outputs (0major+6069minor)pagefaults 0swaps +0.02user 0.06system 0:45.45elapsed 0%CPU (0avgtext+0avgdata 5684maxresident)k +32inputs+0outputs (0major+6082minor)pagefaults 0swaps