From 2ae809c971d50ad504702b2b6132334c6294fa5a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9onard=20G=C3=A9rard?= Date: Tue, 14 Dec 2010 18:29:55 +0100 Subject: [PATCH] Fresh vars, and ident refactoring. Idents.enter_node should be called when entering a node, it is done automagically by the mapfold unless you call directly Hept_mapfold.node_dec. --- compiler/global/idents.ml | 53 ++++++++++++------- compiler/global/idents.mli | 25 ++++----- compiler/global/modules.ml | 30 ++++++----- compiler/global/names.ml | 4 ++ compiler/heptagon/analysis/statefull.ml | 1 + compiler/heptagon/analysis/typing.ml | 14 ++--- compiler/heptagon/hept_mapfold.ml | 14 ++--- compiler/heptagon/parsing/hept_parser.mly | 6 +-- compiler/heptagon/parsing/hept_scoping.ml | 6 +-- compiler/heptagon/transformations/automata.ml | 18 ++++--- compiler/heptagon/transformations/inline.ml | 1 + compiler/heptagon/transformations/last.ml | 7 ++- compiler/heptagon/transformations/reset.ml | 11 ++-- compiler/main/hept2mls.ml | 12 ++--- compiler/main/heptc.ml | 2 +- compiler/main/mls2obc.ml | 12 +++-- compiler/minils/analysis/clocking.ml | 2 +- compiler/minils/main/mls2seq.ml | 2 +- compiler/minils/minils.ml | 6 +-- compiler/minils/mls_mapfold.ml | 6 ++- compiler/minils/mls_printer.ml | 2 +- compiler/minils/parsing/mls_parser.mly | 18 +++---- compiler/minils/transformations/callgraph.ml | 31 ++++++----- compiler/minils/transformations/checkpass.ml | 2 +- compiler/minils/transformations/introvars.ml | 2 +- compiler/minils/transformations/itfusion.ml | 16 ++++-- compiler/minils/transformations/normalize.ml | 4 +- .../minils/transformations/singletonvars.ml | 4 +- compiler/minils/transformations/tomato.ml | 8 +-- compiler/obc/c/cmain.ml | 40 +++++++------- compiler/utilities/misc.ml | 11 ++++ compiler/utilities/misc.mli | 7 +++ 32 files changed, 227 insertions(+), 150 deletions(-) diff --git a/compiler/global/idents.ml b/compiler/global/idents.ml index dffcec5..9fdddab 100644 --- a/compiler/global/idents.ml +++ b/compiler/global/idents.ml @@ -9,6 +9,11 @@ (* naming and local environment *) +(* TODO AG : preprocessing pour avoir un release efficace : +IFDEF RELEASE type iden = int +ELSE *) + + type ident = { num : int; (* a unique index *) @@ -21,16 +26,15 @@ type var_ident = ident let num = ref 0 let ident_compare id1 id2 = compare id1.num id2.num -let sourcename id = id.source + +(* used only for debuging *) let name id = if id.is_generated then id.source ^ "_" ^ (string_of_int id.num) else id.source -let set_sourcename id v = - { id with source = v } - +(* used only for debuging *) let fprint_t ff id = Format.fprintf ff "%s" (name id) module M = struct @@ -77,13 +81,21 @@ end module S = Set.Make (struct type t = string let compare = Pervasives.compare end) + +(** Module used to generate unique string (inside a node) per ident. + /!\ Any pass generating a name must call [enter_node] and use gen_fresh *) module UniqueNames = struct - let used_names = ref S.empty - let env = ref Env.empty + open Names + let used_names = ref (ref S.empty) (** Used strings in the current node *) + let env = ref Env.empty (** Map idents to their string *) + let (node_env : S.t ref QualEnv.t ref) = ref QualEnv.empty - let new_function () = - used_names := S.empty + (** This function should be called every time we enter a node *) + let enter_node n = + (if not (QualEnv.mem n !node_env) + then node_env := QualEnv.add n (ref S.empty) !node_env); + used_names := QualEnv.find n !node_env (** @return a unique string for each identifier. Idents corresponding to variables defined in the source file have the same name unless @@ -91,33 +103,34 @@ struct let assign_name n = let fresh s = num := !num + 1; - s ^ "_" ^ (string_of_int !num) - in + s ^ "_" ^ (string_of_int !num) in let rec fresh_string base = - let base = fresh base in - if S.mem base !used_names then fresh_string base else base - in - if not (Env.mem n !env) then - let s = name n in - let s = if S.mem s !used_names then fresh_string s else s in - used_names := S.add s !used_names; - env := Env.add n s !env + let fs = fresh base in + if S.mem fs !(!used_names) then fresh_string base else fs in + if not (Env.mem n !env) then + (let s = n.source in + let s = if S.mem s !(!used_names) then fresh_string s else s in + !used_names := S.add s !(!used_names); + env := Env.add n s !env) let name id = Env.find id !env end -let fresh s = +let gen_fresh pass_name kind_to_string kind = + let s = "__" ^ pass_name ^ "_" ^ (kind_to_string kind) in num := !num + 1; let id = { num = !num; source = s; is_generated = true } in UniqueNames.assign_name id; id +let gen_var pass_name name = gen_fresh pass_name (fun () -> name) () + let ident_of_name s = num := !num + 1; let id = { num = !num; source = s; is_generated = false } in UniqueNames.assign_name id; id let name id = UniqueNames.name id -let new_function () = UniqueNames.new_function () +let enter_node n = UniqueNames.enter_node n let print_ident ff id = Format.fprintf ff "%s" (name id) diff --git a/compiler/global/idents.mli b/compiler/global/idents.mli index fb6e88b..ee1ab96 100644 --- a/compiler/global/idents.mli +++ b/compiler/global/idents.mli @@ -1,8 +1,9 @@ +open Names + (** This modules manages unique identifiers, - [fresh] generates an identifier from a name - [name] returns a unique name from an identifier. *) - + [gen_fresh] generates an identifier + [name] returns a unique name (inside its node) from an identifier. *) (** The (abstract) type of identifiers*) type ident @@ -13,21 +14,21 @@ type var_ident = ident (** Comparision on idents with the same properties as [Pervasives.compare] *) val ident_compare : ident -> ident -> int -(** Get the source name from an identifier*) -val sourcename : ident -> string (** Get the full name of an identifier (it is guaranteed to be unique) *) val name : ident -> string -(** [set_sourcename id v] returns id with its source name changed to v. *) -val set_sourcename : ident -> string -> ident -(** [fresh n] returns a fresh identifier with source name n *) -val fresh : string -> ident +(** [gen_fresh pass_name kind_to_string kind] + generate a fresh ident with a sweet [name]. + It should be used to define a [fresh] function specific to a pass. *) +val gen_fresh : string -> ('a -> string) -> 'a -> ident +val gen_var : string -> string -> ident + (** [ident_of_name n] returns an identifier corresponding to a _source_ variable (do not use it for generated variables). *) val ident_of_name : string -> ident -(** Resets the sets that makes sure that idents are mapped to unique - identifiers. Should be called when scoping a new function. *) -val new_function : unit -> unit + +(** /!\ This function should be called every time we enter a node *) +val enter_node : Names.qualname -> unit (** Maps taking an identifier as a key. *) module Env : diff --git a/compiler/global/modules.ml b/compiler/global/modules.ml index 6fce969..26762d6 100644 --- a/compiler/global/modules.ml +++ b/compiler/global/modules.ml @@ -225,28 +225,34 @@ let current_qual n = { qual = g_env.current_mod; name = n } (** { 3 Fresh functions return a fresh qualname for the current module } *) -let rec fresh_value name = - let q = current_qual ("__" ^ name ^ "_" ^ Misc.gen_symbol()) in +let rec fresh_value pass_name name = + let q = current_qual ("__"^ pass_name ^"_"^ name) in if QualEnv.mem q g_env.values - then fresh_value name + then fresh_value pass_name (name ^"_"^ Misc.gen_symbol()) else q -let rec fresh_type name = - let q = current_qual ("__" ^ name ^ "_" ^ Misc.gen_symbol()) in +let rec fresh_value_in pass_name name qualifier = + let q = { qual = qualifier; name = "__"^ pass_name ^"_"^ name } in + if QualEnv.mem q g_env.values + then fresh_value_in pass_name (name ^"_"^ Misc.gen_symbol()) qualifier + else q + +let rec fresh_type pass_name name = + let q = current_qual ("__"^ pass_name ^"_"^ name) in if QualEnv.mem q g_env.types - then fresh_type name + then fresh_type pass_name (name ^"_"^ Misc.gen_symbol()) else q -let rec fresh_const name = - let q = current_qual ("__" ^ name ^ "_" ^ Misc.gen_symbol()) in +let rec fresh_const pass_name name = + let q = current_qual ("__"^ pass_name ^"_"^ name) in if QualEnv.mem q g_env.consts - then fresh_const name + then fresh_const pass_name (name ^"_"^ Misc.gen_symbol()) else q -let rec fresh_constr name = - let q = current_qual ("__" ^ name ^ "_" ^ Misc.gen_symbol()) in +let rec fresh_constr pass_name name = + let q = current_qual ("__"^ pass_name ^"_"^ name) in if QualEnv.mem q g_env.constrs - then fresh_constr name + then fresh_constr pass_name (name ^"_"^ Misc.gen_symbol()) else q diff --git a/compiler/global/names.ml b/compiler/global/names.ml index 273f2e3..2fe3877 100644 --- a/compiler/global/names.ml +++ b/compiler/global/names.ml @@ -75,3 +75,7 @@ let print_raw_qualname ff {qual = q; name = n} = let opname qn = match qn with | { qual = "Pervasives"; name = m; } -> m | { qual = qual; name = n; } -> qual ^ "." ^ n + +(** Use a printer to generate a string compatible with a name *) +let print_pp_to_name p x = + Misc.sanitize_string (Misc.print_pp_to_string p x) diff --git a/compiler/heptagon/analysis/statefull.ml b/compiler/heptagon/analysis/statefull.ml index f15e84b..a862492 100644 --- a/compiler/heptagon/analysis/statefull.ml +++ b/compiler/heptagon/analysis/statefull.ml @@ -67,6 +67,7 @@ let present_handler funs acc ph = { ph with p_cond = p_cond; p_block = p_block }, acc let node_dec funs _ n = + Idents.enter_node n.n_name; let n, statefull = Hept_mapfold.node_dec funs false n in if statefull & not (n.n_statefull) then message n.n_loc Eshould_be_a_node; diff --git a/compiler/heptagon/analysis/typing.ml b/compiler/heptagon/analysis/typing.ml index f01c393..64c5bd7 100644 --- a/compiler/heptagon/analysis/typing.ml +++ b/compiler/heptagon/analysis/typing.ml @@ -231,7 +231,7 @@ let typ_of_name h x = try let { ty = ty } = Env.find x h in ty with - Not_found -> error (Eundefined(sourcename x)) + Not_found -> error (Eundefined(name x)) let desc_of_ty = function | Tid n when n = pbool -> Tenum [ptrue; pfalse] @@ -290,7 +290,7 @@ let diff_const defined_names local_names = the difference *) let included_env s1 s2 = Env.iter - (fun elt _ -> if not (Env.mem elt s2) then error (Emissing(sourcename elt))) + (fun elt _ -> if not (Env.mem elt s2) then error (Emissing(name elt))) s1 let diff_env defined_names local_names = @@ -321,7 +321,7 @@ let all_last h env = Env.iter (fun elt _ -> if not (Env.find elt h).last - then error (Elast_undefined(sourcename elt))) + then error (Elast_undefined(name elt))) env let last = function | Var -> false | Last _ -> true @@ -977,7 +977,7 @@ and build const_env h dec = | Var | Last None -> vd.v_last in if Env.mem vd.v_ident h then - error (Ealready_defined(sourcename vd.v_ident)); + error (Ealready_defined(name vd.v_ident)); let acc_defined = Env.add vd.v_ident ty acc_defined in let h = Env.add vd.v_ident { ty = ty; last = last vd.v_last } h in @@ -994,7 +994,7 @@ let typing_contract const_env h contract = | Some ({ c_block = b; c_assume = e_a; c_enforce = e_g; - c_controllables = c }) -> + c_controllables = c }) -> let typed_b, defined_names, _ = typing_block const_env h b in (* check that the equations do not define other unexpected names *) included_env defined_names Env.empty; @@ -1005,11 +1005,11 @@ let typing_contract const_env h contract = let typed_e_g = expect const_env h (Tid Initial.pbool) e_g in let typed_c, (c_names, h) = build const_env h c in - + Some { c_block = typed_b; c_assume = typed_e_a; c_enforce = typed_e_g; - c_controllables = typed_c }, h + c_controllables = typed_c }, h let solve loc cl = try diff --git a/compiler/heptagon/hept_mapfold.ml b/compiler/heptagon/hept_mapfold.ml index d2a5484..3d730ea 100644 --- a/compiler/heptagon/hept_mapfold.ml +++ b/compiler/heptagon/hept_mapfold.ml @@ -257,20 +257,22 @@ and contract funs acc c = let c_assume, acc = exp_it funs acc c.c_assume in let c_enforce, acc = exp_it funs acc c.c_enforce in let c_block, acc = block_it funs acc c.c_block in - let c_controllables, acc = mapfold (var_dec_it funs) acc c.c_controllables in + let c_controllables, acc = mapfold (var_dec_it funs) acc c.c_controllables in { c with c_assume = c_assume; - c_enforce = c_enforce; - c_block = c_block; - c_controllables = c_controllables }, - acc + c_enforce = c_enforce; + c_block = c_block; + c_controllables = c_controllables }, + acc and param_it funs acc vd = funs.param funs acc vd and param funs acc vd = let v_last, acc = last_it funs acc vd.v_last in { vd with v_last = v_last }, acc -and node_dec_it funs acc nd = funs.node_dec funs acc nd +and node_dec_it funs acc nd = + Idents.enter_node nd.n_name; + funs.node_dec funs acc nd and node_dec funs acc nd = let n_input, acc = mapfold (var_dec_it funs) acc nd.n_input in let n_output, acc = mapfold (var_dec_it funs) acc nd.n_output in diff --git a/compiler/heptagon/parsing/hept_parser.mly b/compiler/heptagon/parsing/hept_parser.mly index 52d5a44..7226a64 100644 --- a/compiler/heptagon/parsing/hept_parser.mly +++ b/compiler/heptagon/parsing/hept_parser.mly @@ -224,7 +224,7 @@ contract: { Some{ c_block = b; c_assume = $4; c_enforce = $5; - c_controllables = $6 } } + c_controllables = $6 } } ; opt_assume: @@ -445,8 +445,8 @@ _exp: { mk_op_call $2 [$1; $3] } | exp INFIX2 exp { mk_op_call $2 [$1; $3] } - | e=exp WHEN c=constructor_or_bool LPAREN n=IDENT RPAREN - { Ewhen (e, c, n) } + | e=exp WHEN c=constructor_or_bool LPAREN ce=IDENT RPAREN + { Ewhen (e, c, ce) } | MERGE n=IDENT hs=merge_handlers { Emerge (n, hs) } | exp INFIX1 exp diff --git a/compiler/heptagon/parsing/hept_scoping.ml b/compiler/heptagon/parsing/hept_scoping.ml index 71dee7d..cadd4f9 100644 --- a/compiler/heptagon/parsing/hept_scoping.ml +++ b/compiler/heptagon/parsing/hept_scoping.ml @@ -369,7 +369,7 @@ let translate_contract env ct = let b, _ = translate_block env ct.c_block in { Heptagon.c_assume = translate_exp env ct.c_assume; Heptagon.c_enforce = translate_exp env ct.c_enforce; - Heptagon.c_controllables = translate_vd_list env ct.c_controllables; + Heptagon.c_controllables = translate_vd_list env ct.c_controllables; Heptagon.c_block = b } let params_of_var_decs = @@ -383,7 +383,8 @@ let args_of_var_decs = (translate_type vd.v_loc vd.v_type)) let translate_node node = - Idents.new_function (); + let n = current_qual node.n_name in + Idents.enter_node n; (* Inputs and outputs define the initial local env *) let env0 = Rename.append Rename.empty (node.n_input @ node.n_output) in let params = params_of_var_decs node.n_params in @@ -393,7 +394,6 @@ let translate_node node = let contract = Misc.optional (translate_contract env) node.n_contract in (* the env of the block is used in the contract translation *) - let n = current_qual node.n_name in (* add the node signature to the environment *) let i = args_of_var_decs node.n_input in let o = args_of_var_decs node.n_output in diff --git a/compiler/heptagon/transformations/automata.ml b/compiler/heptagon/transformations/automata.ml index 98e45d1..9bd1a00 100644 --- a/compiler/heptagon/transformations/automata.ml +++ b/compiler/heptagon/transformations/automata.ml @@ -17,6 +17,10 @@ open Hept_mapfold open Initial open Modules +type var = S | NS | R | NR | PNR +let fresh = Idents.gen_fresh "automata" + (function S -> "s" | NS -> "ns" | R -> "r" | NR -> "nr" | PNR -> "pnr") + let mk_var_exp n ty = mk_exp (Evar n) ty @@ -46,7 +50,7 @@ let state_type_dec_list = ref [] (* create and add to the env the constructors corresponding to a name state *) let intro_state_constr type_name state state_env = - let c = Modules.fresh_constr state in + let c = Modules.fresh_constr "automata" state in Modules.add_constrs c type_name; NamesEnv.add state c state_env (* create and add the the global env and to state_type_dec_list @@ -68,7 +72,7 @@ let no_strong_transition state_handlers = let translate_automaton v eq_list handlers = - let type_name = Modules.fresh_type ("states") in + let type_name = Modules.fresh_type "automata" "states" in (* the state env associate a name to a qualified constructor *) let state_env = List.fold_left @@ -80,11 +84,11 @@ let translate_automaton v eq_list handlers = (* The initial state constructor *) let initial = (NamesEnv.find (List.hd handlers).s_state state_env) in - let statename = Idents.fresh "s" in - let next_statename = Idents.fresh "ns" in - let resetname = Idents.fresh "r" in - let next_resetname = Idents.fresh "nr" in - let pre_next_resetname = Idents.fresh "pnr" in + let statename = fresh S in + let next_statename = fresh NS in + let resetname = fresh R in + let next_resetname = fresh NR in + let pre_next_resetname = fresh PNR in let name n = NamesEnv.find n state_env in let state n = diff --git a/compiler/heptagon/transformations/inline.ml b/compiler/heptagon/transformations/inline.ml index 9fe8e76..972e9e5 100644 --- a/compiler/heptagon/transformations/inline.ml +++ b/compiler/heptagon/transformations/inline.ml @@ -105,6 +105,7 @@ let block funs (env, newvars, newequs) blk = (env, [], [])) let node_dec funs (env, newvars, newequs) nd = + Idents.enter_node nd.n_name; let nd, (env, newvars, newequs) = Hept_mapfold.node_dec funs (env, newvars, newequs) nd in ({ nd with n_block = diff --git a/compiler/heptagon/transformations/last.ml b/compiler/heptagon/transformations/last.ml index f0aa6bd..cf3420b 100644 --- a/compiler/heptagon/transformations/last.ml +++ b/compiler/heptagon/transformations/last.ml @@ -11,13 +11,17 @@ open Heptagon open Hept_mapfold open Idents + +let fresh = Idents.gen_fresh "last" Idents.name + + (* introduce a fresh equation [last_x = pre(x)] for every *) (* variable declared with a last *) let last (eq_list, env, v) { v_ident = n; v_type = t; v_last = last } = match last with | Var -> (eq_list, env, v) | Last(default) -> - let lastn = Idents.fresh ("last" ^ (sourcename n)) in + let lastn = fresh n in let eq = mk_equation (Eeq (Evarpat lastn, mk_exp (Epre (default, mk_exp (Evar n) t)) t)) in @@ -39,6 +43,7 @@ let block funs env b = b_equs = eq_lastn_n_list @ b.b_equs }, env let node_dec funs _ n = + Idents.enter_node n.n_name; let _, env, _ = extend_env Env.empty n.n_input in let eq_lasto_list, env, last_o = extend_env env n.n_output in let n, _ = Hept_mapfold.node_dec funs env n in diff --git a/compiler/heptagon/transformations/reset.ml b/compiler/heptagon/transformations/reset.ml index 244a617..0fecdf2 100644 --- a/compiler/heptagon/transformations/reset.ml +++ b/compiler/heptagon/transformations/reset.ml @@ -45,6 +45,11 @@ open Initial e1 -> e2 is translated into if (true fby false) then e1 else e2 *) + + +let fresh = Idents.gen_fresh "reset" (fun () -> "r") + + let mk_bool_var n = mk_exp (Evar n) (Tid Initial.pbool) let mk_bool_param n = mk_var_dec n (Tid Initial.pbool) @@ -73,7 +78,7 @@ let ifres res e2 e3 = (* add an equation *) let equation v acc_eq_list e = - let n = Idents.fresh "r" in + let n = fresh() in n, (mk_bool_param n) :: v, (mk_equation (Eeq(Evarpat n, e))) ::acc_eq_list @@ -133,8 +138,8 @@ let edesc funs (res, v, acc_eq_list) ed = let switch_handlers funs (res, v, acc_eq_list) switch_handlers = (* introduce a reset bit for each branch *) - let m_list = List.map (fun _ -> Idents.fresh "r") switch_handlers in - let lm_list = List.map (fun _ -> Idents.fresh "r") switch_handlers in + let m_list = List.map (fun {w_name = c} -> fresh()) switch_handlers in + let lm_list = List.map (fun {w_name = c} -> fresh()) switch_handlers in let body i ({ w_block = b } as sh) m lm = let defnames = List.fold_left (fun acc m -> diff --git a/compiler/main/hept2mls.ml b/compiler/main/hept2mls.ml index 3403f1b..5baeeb6 100644 --- a/compiler/main/hept2mls.ml +++ b/compiler/main/hept2mls.ml @@ -90,7 +90,7 @@ end (* add an equation *) let equation locals l_eqs e = - let n = Idents.fresh "ck" in + let n = Idents.gen_var "hept2mls" "ck" in n, (mk_var_dec n e.e_ty) :: locals, (mk_equation (Evarpat n) e):: l_eqs @@ -260,7 +260,7 @@ let rec translate_pat = function let rec rename_pat ni locals s_eqs = function | Heptagon.Evarpat(n), ty -> if IdentSet.mem n ni then ( - let n_copy = Idents.fresh (sourcename n) in + let n_copy = Idents.gen_var "hept2mls" (name n) in Evarpat n_copy, (mk_var_dec n_copy ty) :: locals, add n (mk_exp ~ty:ty (Evar n_copy)) s_eqs @@ -352,7 +352,7 @@ let translate_contract env contract = Heptagon.b_equs = eq_list }; Heptagon.c_assume = e_a; Heptagon.c_enforce = e_g; - Heptagon.c_controllables = l_c } -> + Heptagon.c_controllables = l_c } -> let env' = Env.add v env in let locals = translate_locals [] v in let locals, l_eqs, s_eqs = @@ -360,12 +360,12 @@ let translate_contract env contract = let l_eqs, _ = add_locals IdentSet.empty l_eqs [] s_eqs in let e_a = translate env' e_a in let e_g = translate env' e_g in - let env = Env.add l_c env in + let env = Env.add l_c env in Some { c_local = locals; c_eq = l_eqs; c_assume = e_a; c_enforce = e_g; - c_controllables = List.map translate_var l_c }, + c_controllables = List.map translate_var l_c }, env @@ -387,7 +387,7 @@ let node n_input = List.map translate_var i; n_output = List.map translate_var o; n_contract = contract; - n_controller_call = ([],[]); + n_controller_call = ([],[]); n_local = locals; n_equs = l_eqs; n_loc = loc ; diff --git a/compiler/main/heptc.ml b/compiler/main/heptc.ml index dc1f1a2..a7a8878 100644 --- a/compiler/main/heptc.ml +++ b/compiler/main/heptc.ml @@ -90,7 +90,7 @@ let main () = "-nopervasives", Arg.Unit set_no_pervasives, doc_no_pervasives; "-target", Arg.String add_target_language, doc_target; "-targetpath", Arg.String set_target_path, doc_target_path; - "-nocaus", Arg.Clear causality, doc_nocaus; + "-nocaus", Arg.Clear causality, doc_nocaus; "-noinit", Arg.Clear init, doc_noinit; "-fti", Arg.Set full_type_info, doc_full_type_info; "-itfusion", Arg.Set do_iterator_fusion, doc_itfusion; diff --git a/compiler/main/mls2obc.ml b/compiler/main/mls2obc.ml index 2fd1acc..6bced29 100644 --- a/compiler/main/mls2obc.ml +++ b/compiler/main/mls2obc.ml @@ -19,6 +19,8 @@ open Static open Obc_mapfold open Initial +let fresh_it () = Idents.gen_var "mls2obc" "i" + (** Not giving any type and called after typing, DO NOT use it anywhere else *) let static_exp_of_int i = Types.mk_static_exp (Types.Sint i) @@ -131,8 +133,8 @@ and translate_act map pat | Minils.Evarpat x, Minils.Eapp ({ Minils.a_op = Minils.Econcat }, [e1; e2], _) -> - let cpt1 = Idents.fresh "i" in - let cpt2 = Idents.fresh "i" in + let cpt1 = fresh_it () in + let cpt2 = fresh_it () in let x = var_from_name map x in (match e1.Minils.e_ty, e2.Minils.e_ty with | Tarray (_, n1), Tarray (_, n2) -> @@ -157,7 +159,7 @@ and translate_act map pat | Minils.Evarpat x, Minils.Eapp ({ Minils.a_op = Minils.Earray_fill; Minils.a_params = [n] }, [e], _) -> - let cpt = Idents.fresh "i" in + let cpt = fresh_it () in let e = translate map e in [ Afor (cpt, mk_static_int 0, n, mk_block [Aassgn (mk_lhs (Larray (var_from_name map x, @@ -166,7 +168,7 @@ and translate_act map pat | Minils.Evarpat x, Minils.Eapp ({ Minils.a_op = Minils.Eselect_slice; Minils.a_params = [idx1; idx2] }, [e], _) -> - let cpt = Idents.fresh "i" in + let cpt = fresh_it () in let e = translate map e in let idx = mk_exp (Eop (op_from_string "+", [mk_evar cpt; @@ -296,7 +298,7 @@ let rec translate_eq map call_context { Minils.eq_lhs = pat; Minils.eq_rhs = e } let name_list = translate_pat map pat in let c_list = List.map (translate map) e_list in - let x = Idents.fresh "i" in + let x = fresh_it () in let call_context = Oarray ("n", mk_lhs (Lvar x)), Some n in let si', j', action = translate_iterator map call_context it name_list app loc n x c_list in diff --git a/compiler/minils/analysis/clocking.ml b/compiler/minils/analysis/clocking.ml index 3fbe459..b13cc27 100644 --- a/compiler/minils/analysis/clocking.ml +++ b/compiler/minils/analysis/clocking.ml @@ -140,7 +140,7 @@ let typing_contract h contract base = c_eq = eq_list; c_assume = e_a; c_enforce = e_g; - c_controllables = c_list } -> + c_controllables = c_list } -> let h' = build h l_list in (* assumption *) (* property *) diff --git a/compiler/minils/main/mls2seq.ml b/compiler/minils/main/mls2seq.ml index bfbd199..8df6acf 100644 --- a/compiler/minils/main/mls2seq.ml +++ b/compiler/minils/main/mls2seq.ml @@ -30,7 +30,7 @@ let write_object_file p = close_out epoc; comment "Generating of object file" -(** Writes a .epo file for program [p]. *) +(** Writes a .obc file for program [p]. *) let write_obc_file p = let obc_name = (filename_of_name p.Obc.p_modname)^".obc" in let obc = open_out obc_name in diff --git a/compiler/minils/minils.ml b/compiler/minils/minils.ml index 7d15357..ad40894 100644 --- a/compiler/minils/minils.ml +++ b/compiler/minils/minils.ml @@ -146,13 +146,13 @@ let mk_equation ?(loc = no_location) pat exp = let mk_node ?(input = []) ?(output = []) ?(contract = None) ?(local = []) ?(eq = []) - ?(loc = no_location) ?(param = []) ?(constraints = []) - ?(pinst = ([],[])) name = + ?(loc = no_location) ?(param = []) ?(constraints = []) + ?(pinst = ([],[])) name = { n_name = name; n_input = input; n_output = output; n_contract = contract; - n_controller_call = pinst; + n_controller_call = pinst; n_local = local; n_equs = eq; n_loc = loc; diff --git a/compiler/minils/mls_mapfold.ml b/compiler/minils/mls_mapfold.ml index 07fb58a..314ff4b 100644 --- a/compiler/minils/mls_mapfold.ml +++ b/compiler/minils/mls_mapfold.ml @@ -49,7 +49,7 @@ and edesc funs acc ed = match ed with | Econst se -> let se, acc = static_exp_it funs.global_funs acc se in Econst se, acc - | Evar x -> ed, acc + | Evar _ -> ed, acc | Efby (se, e) -> let se, acc = optional_wacc (static_exp_it funs.global_funs) acc se in let e, acc = exp_it funs acc e in @@ -126,7 +126,9 @@ and contract funs acc c = , acc -and node_dec_it funs acc nd = funs.node_dec funs acc nd +and node_dec_it funs acc nd = + Idents.enter_node nd.n_name; + funs.node_dec funs acc nd and node_dec funs acc nd = let n_input, acc = var_decs_it funs acc nd.n_input in let n_output, acc = var_decs_it funs acc nd.n_output in diff --git a/compiler/minils/mls_printer.ml b/compiler/minils/mls_printer.ml index a6c5f32..8bebfc0 100644 --- a/compiler/minils/mls_printer.ml +++ b/compiler/minils/mls_printer.ml @@ -189,7 +189,7 @@ let rec print_type_dec ff { t_name = name; t_desc = tdesc } = let print_contract ff { c_local = l; c_eq = eqs; c_assume = e_a; c_enforce = e_g; - c_controllables = c;} = + c_controllables = c;} = fprintf ff "@[contract@\n%a%a@ assume %a@ enforce %a@ with (%a)@]" print_local_vars l print_eqs eqs diff --git a/compiler/minils/parsing/mls_parser.mly b/compiler/minils/parsing/mls_parser.mly index 73b2048..c028adc 100644 --- a/compiler/minils/parsing/mls_parser.mly +++ b/compiler/minils/parsing/mls_parser.mly @@ -118,10 +118,10 @@ node_dec: NODE n=qualname p=params(n_param) LPAREN args=args RPAREN RETURNS LPAREN out=args RPAREN contract=contract vars=loc_vars eqs=equs - { mk_node p args out vars eqs - ~loc:(Loc ($startpos,$endpos)) - ~contract:contract - n } + { mk_node p args out vars eqs + ~loc:(Loc ($startpos,$endpos)) + ~contract:contract + n } contract: @@ -129,14 +129,14 @@ contract: | CONTRACT locvars=loc_vars eqs=opt_equs - assume=opt_assume - enforce=opt_enforce + assume=opt_assume + enforce=opt_enforce withvar=opt_with { Some{ c_local=locvars; - c_equs=eqs; + c_equs=eqs; c_assume = assume; c_enforce = enforce; - c_controllables = withvar } } + c_controllables = withvar } } ; opt_assume: @@ -181,7 +181,7 @@ var: | ns=snlist(COMMA, NAME) COLON t=type_ident c=clock_annot { List.map (fun n -> mk_var_dec n t c (Loc ($startpos,$endpos))) ns } -opt_equs: +opt_equs: | /* empty */ { [] } | LET e=slist(SEMICOL, equ) TEL { e } diff --git a/compiler/minils/transformations/callgraph.ml b/compiler/minils/transformations/callgraph.ml index 46fe579..928f006 100644 --- a/compiler/minils/transformations/callgraph.ml +++ b/compiler/minils/transformations/callgraph.ml @@ -92,14 +92,16 @@ struct [ln] with the static parameters [params] and stores it. *) let generate_new_name ln params = match params with | [] -> nodes_names := M.add (ln, params) ln !nodes_names - | _ -> let { qual = q; name = n } = ln in - let new_ln = { qual = q; - (* TODO ??? c'est quoi ce nom ??? *) - (* l'utilite de fresh n'est vrai que si toute les fonctions - sont touchees.. ce qui n'est pas vrai cf main_nodes *) - (* TODO mettre les valeurs des params dans le nom *) - name = n^(Idents.name (Idents.fresh "")) } in - nodes_names := M.add (ln, params) new_ln !nodes_names + | _ -> + let { qual = q; name = n } = ln in + let param_string = + List.fold_left + (fun s se -> + s ^ (Names.print_pp_to_name Global_printer.print_static_exp se)) + "_params_" params in + let new_ln = + Modules.fresh_value_in "callgraph" (n^param_string^"_") q in + nodes_names := M.add (ln, params) new_ln !nodes_names (** Adds an instance of a node. *) let add_node_instance ln params = @@ -167,6 +169,7 @@ struct in ed, m let node_dec_instance modname n params = + Idents.enter_node n.n_name; let global_funs = { Global_mapfold.defaults with static_exp = static_exp } in let funs = @@ -301,9 +304,9 @@ let program p = (* Find the nodes without static parameters *) let main_nodes = List.filter (fun n -> is_empty n.n_params) p.p_nodes in let main_nodes = List.map (fun n -> n.n_name, []) main_nodes in - info.opened <- NamesEnv.add p.p_modname p NamesEnv.empty; - (* Creates the list of instances starting from these nodes *) - List.iter call_node main_nodes; - let p_list = NamesEnv.fold (fun _ p l -> p::l) info.opened [] in - (* Generate all the needed instances *) - List.map Param_instances.Instantiate.program p_list + info.opened <- NamesEnv.add p.p_modname p NamesEnv.empty; + (* Creates the list of instances starting from these nodes *) + List.iter call_node main_nodes; + let p_list = NamesEnv.fold (fun _ p l -> p::l) info.opened [] in + (* Generate all the needed instances *) + List.map Param_instances.Instantiate.program p_list diff --git a/compiler/minils/transformations/checkpass.ml b/compiler/minils/transformations/checkpass.ml index 3b39b26..437c519 100644 --- a/compiler/minils/transformations/checkpass.ml +++ b/compiler/minils/transformations/checkpass.ml @@ -26,7 +26,7 @@ let add_check prefix pass nd nd_list = let nd'_name = { nd.n_name with name = prefix ^ "_" ^ nd.n_name.name; } in let nd' = pass nd in let nd' = { nd' with n_name = nd'_name; } in - let output = Idents.fresh "o" in + let output = Idents.gen_var "checkpass" "o" in let echeck = let ty_r = match nd.n_output with diff --git a/compiler/minils/transformations/introvars.ml b/compiler/minils/transformations/introvars.ml index f48fb08..f0c910b 100644 --- a/compiler/minils/transformations/introvars.ml +++ b/compiler/minils/transformations/introvars.ml @@ -93,7 +93,7 @@ and intro_var e (eq_list, var_list) = match e.e_desc with | Evar _ -> (e, eq_list, var_list) | _ -> - let id = Idents.fresh prefix in + let id = Idents.gen_var "introvars" prefix in let new_eq = mk_equation (Evarpat id) e and var_dc = mk_var_dec id e.e_ty in (mk_exp ~ty:e.e_ty (Evar id), new_eq :: eq_list, var_dc :: var_list) diff --git a/compiler/minils/transformations/itfusion.ml b/compiler/minils/transformations/itfusion.ml index 7c8b7b0..f3effeb 100644 --- a/compiler/minils/transformations/itfusion.ml +++ b/compiler/minils/transformations/itfusion.ml @@ -7,8 +7,15 @@ open Minils (* Iterator fusion *) (* Functions to temporarily store anonymous nodes*) -let mk_fresh_node_name () = - current_qual (Idents.name (Idents.fresh "_n_")) +let mk_fresh_node_name () = Modules.fresh_value "itfusion" "temp" + +let fresh_vd_of_arg = + Idents.gen_fresh "itfusion" + (fun a -> match a.a_name with + | None -> "v" + | Some n -> n) + +let fresh_var = Idents.gen_fresh "itfusion" (fun () -> "x") let anon_nodes = ref QualEnv.empty @@ -44,8 +51,7 @@ let tuple_of_vd_list l = mk_exp ~ty:ty (Eapp (mk_app Etuple, el, None)) let vd_of_arg ad = - let n = match ad.a_name with None -> "_v" | Some n -> n in - mk_var_dec (Idents.fresh n) ad.a_type + mk_var_dec (fresh_vd_of_arg ad) ad.a_type (** @return the lists of inputs and outputs (as var_dec) of an app object. *) @@ -100,7 +106,7 @@ let edesc funs acc ed = let new_inp, e, acc_eq_list = mk_call g acc_eq_list in new_inp @ inp, acc_eq_list, e::largs, local_args @ args, true | _ -> - let vd = mk_var_dec (Idents.fresh "_x") e.e_ty in + let vd = mk_var_dec (fresh_var ()) e.e_ty in let x = mk_exp (Evar vd.v_ident) in vd::inp, acc_eq_list, x::largs, e::args, b in diff --git a/compiler/minils/transformations/normalize.ml b/compiler/minils/transformations/normalize.ml index cbd4f53..a15d639 100644 --- a/compiler/minils/transformations/normalize.ml +++ b/compiler/minils/transformations/normalize.ml @@ -25,7 +25,7 @@ let flatten_e_list l = let equation (d_list, eq_list) e = let add_one_var ty d_list = - let n = Idents.fresh "_v" in + let n = Idents.gen_var "normalize" "v" in let d_list = (mk_var_dec ~clock:e.e_ck n ty) :: d_list in n, d_list in @@ -306,7 +306,7 @@ and fby kind context e v e1 = let e_list = List.map mk_pre e_list in let e = { e with e_desc = Eapp(app, e_list, r) } in translate kind context e - | Econst { se_desc = Stuple se_list }, None -> + | Econst { se_desc = Stuple _ }, None -> context, e1 | _ -> let context, e1' = diff --git a/compiler/minils/transformations/singletonvars.ml b/compiler/minils/transformations/singletonvars.ml index deb22d3..cbea34f 100644 --- a/compiler/minils/transformations/singletonvars.ml +++ b/compiler/minils/transformations/singletonvars.ml @@ -59,7 +59,7 @@ struct let node nd = let funs = { Mls_mapfold.defaults with Mls_mapfold.edesc = edesc; } in - snd (Mls_mapfold.node_dec funs Env.empty nd) + snd (Mls_mapfold.node_dec_it funs Env.empty nd) end module InlineSingletons = @@ -72,7 +72,7 @@ struct let inline_node subst nd = let funs = { Mls_mapfold.defaults with Mls_mapfold.exp = exp; } in - fst (Mls_mapfold.node_dec funs subst nd) + fst (Mls_mapfold.node_dec_it funs subst nd) let inline_exp subst e = let funs = { Mls_mapfold.defaults with diff --git a/compiler/minils/transformations/tomato.ml b/compiler/minils/transformations/tomato.ml index 5519839..5b358dc 100644 --- a/compiler/minils/transformations/tomato.ml +++ b/compiler/minils/transformations/tomato.ml @@ -32,7 +32,7 @@ let ident_of_int = fun (name : string) (i : int) -> try Hashtbl.find ht i with Not_found -> - let new_ident = Idents.fresh name in + let new_ident = Idents.gen_var "tomato" name in Hashtbl.add ht i new_ident; new_ident @@ -151,10 +151,10 @@ struct let funs = { Mls_mapfold.defaults with Mls_mapfold.exp = exp; Mls_mapfold.var_dec = var_dec; } in - fst (Mls_mapfold.node_dec funs subst nd) + fst (Mls_mapfold.node_dec_it funs subst nd) end -let empty_var = Idents.fresh "EMPTY" +let empty_var = Idents.gen_var "tomato" "EMPTY" let dummy_exp = mk_exp (Evar empty_var) let exp_of_ident vi = mk_exp (Evar vi) @@ -460,7 +460,7 @@ let introduce_copies_for_outputs nd = let var_dec vd (iset, vd_list, eq_list) = if IdentSet.mem vd.v_ident iset then (* introduce copy, change vd *) - let fresh = Idents.fresh (Idents.name vd.v_ident) in + let fresh = Idents.gen_var "tomato" (Idents.name vd.v_ident) in let new_eq = let e = mk_exp ~ty:vd.v_type (Evar vd.v_ident) in mk_equation (Evarpat fresh) e in diff --git a/compiler/obc/c/cmain.ml b/compiler/obc/c/cmain.ml index 1b1a2a8..d295da5 100644 --- a/compiler/obc/c/cmain.ml +++ b/compiler/obc/c/cmain.ml @@ -24,9 +24,13 @@ open Compiler_utils (** {1 Main C function generation} *) +let _ = Idents.enter_node (Modules.fresh_value "cmain" "main") + +let fresh n = Idents.name (Idents.gen_var "cmain" n) + (* Unique names for C variables handling step counts. *) -let step_counter = Idents.fresh "step_c" -and max_step = Idents.fresh "step_max" +let step_counter = fresh "step_c" +and max_step = fresh"step_max" let assert_node_res cd = let stepm = find_step_method cd in @@ -43,10 +47,10 @@ let assert_node_res cd = exit 1); let name = cname_of_qn cd.cd_name in let mem = - (Idents.name (Idents.fresh ("mem_for_" ^ name)), + (fresh ("mem_for_" ^ name), Cty_id (qn_append cd.cd_name "_mem")) and out = - (Idents.name (Idents.fresh ("out_for_" ^ name)), + (fresh ("out_for_" ^ name), Cty_id (qn_append cd.cd_name "_out")) in let reset_i = Cfun_call (name ^ "_reset", [Caddrof (Cvar (fst mem))]) in @@ -71,7 +75,7 @@ let assert_node_res cd = [Cconst (Cstrlit ("Node \\\"" ^ name ^ "\\\" failed at step" ^ " %d.\\n")); - Clhs (Cvar (Idents.name step_counter))])); + Clhs (Cvar step_counter)])); Creturn (Cconst (Ccint 1))], []); ]; @@ -104,7 +108,7 @@ let main_def_of_class_def cd = (** Generates scanf statements. *) let rec read_lhs_of_ty lhs ty = match ty with | Tarray (ty, n) -> - let iter_var = Idents.name (Idents.fresh "i") in + let iter_var = fresh "i" in let lhs = Carray (lhs, Clhs (Cvar iter_var)) in let (reads, bufs) = read_lhs_of_ty lhs ty in ([Cfor (iter_var, 0, int_of_static_exp n, reads)], bufs) @@ -130,7 +134,7 @@ let main_def_of_class_def cd = match need_buf_for_ty ty with | None -> ([scan_exp], []) | Some tyn -> - let varn = Idents.name (Idents.fresh "buf") in + let varn = fresh "buf" in ([scan_exp; Csexpr (Cfun_call (tyn ^ "_of_string", [Clhs (Cvar varn)]))], @@ -140,14 +144,14 @@ let main_def_of_class_def cd = resulting values of enum types. *) let rec write_lhs_of_ty lhs ty = match ty with | Tarray (ty, n) -> - let iter_var = Idents.name (Idents.fresh "i") in + let iter_var = fresh "i" in let lhs = Carray (lhs, Clhs (Cvar iter_var)) in let (reads, bufs) = write_lhs_of_ty lhs ty in ([cprint_string "[ "; Cfor (iter_var, 0, int_of_static_exp n, reads); cprint_string "]"], bufs) | _ -> - let varn = Idents.name (Idents.fresh "buf") in + let varn = fresh "buf" in let format_s = format_for_type ty in let nbuf_opt = need_buf_for_ty ty in let ep = match nbuf_opt with @@ -217,7 +221,7 @@ let main_skel var_list prologue body = f_args = [("argc", Cty_int); ("argv", Cty_ptr (Cty_ptr Cty_char))]; f_body = { var_decls = - (name step_counter, Cty_int) :: (name max_step, Cty_int) :: var_list; + (step_counter, Cty_int) :: (max_step, Cty_int) :: var_list; block_body = [ (* @@ -226,10 +230,10 @@ let main_skel var_list prologue body = if (argc == 2) max_step = atoi(argv[1]); *) - Caffect (Cvar (name step_counter), Cconst (Ccint 0)); - Caffect (Cvar (name max_step), Cconst (Ccint 0)); + Caffect (Cvar step_counter, Cconst (Ccint 0)); + Caffect (Cvar max_step, Cconst (Ccint 0)); Cif (Cbop ("==", Clhs (Cvar "argc"), Cconst (Ccint 2)), - [Caffect (Cvar (name max_step), + [Caffect (Cvar max_step, Cfun_call ("atoi", [Clhs (Carray (Cvar "argv", Cconst (Ccint 1)))]))], []); @@ -238,14 +242,14 @@ let main_skel var_list prologue body = (* while (!max_step || step_c < max_step) *) @ [ Cwhile (Cbop ("||", - Cuop ("!", Clhs (Cvar (name max_step))), + Cuop ("!", Clhs (Cvar max_step)), Cbop ("<", - Clhs (Cvar (name step_counter)), - Clhs (Cvar (name max_step)))), + Clhs (Cvar step_counter), + Clhs (Cvar max_step))), (* step_counter = step_counter + 1; *) - Caffect (Cvar (name step_counter), + Caffect (Cvar step_counter, Cbop ("+", - Clhs (Cvar (name step_counter)), + Clhs (Cvar step_counter), Cconst (Ccint 1))) :: body); Creturn (Cconst (Ccint 0)); diff --git a/compiler/utilities/misc.ml b/compiler/utilities/misc.ml index 206790b..e3ca75e 100644 --- a/compiler/utilities/misc.ml +++ b/compiler/utilities/misc.ml @@ -30,6 +30,17 @@ let rec split_string s c = with Not_found -> [s] +(** Print to a string *) +let print_pp_to_string print_fun element = + let _ = Format.flush_str_formatter () in (* Ensure that the buffer is empty *) + print_fun Format.str_formatter element; + Format.flush_str_formatter () + +(** Replace all non [a-z A-Z 0-9] character of a string by [_] *) +let sanitize_string s = + Str.global_replace (Str.regexp "[^a-zA-Z0-9]") "_" s + + (* creation of names. Ensure unicity for the whole compilation chain *) let symbol = ref 0 diff --git a/compiler/utilities/misc.mli b/compiler/utilities/misc.mli index a332b87..d8583ab 100644 --- a/compiler/utilities/misc.mli +++ b/compiler/utilities/misc.mli @@ -76,3 +76,10 @@ val assert_1min : 'a list -> 'a * 'a list val assert_2 : 'a list -> 'a * 'a val assert_2min : 'a list -> 'a * 'a * 'a list val assert_3 : 'a list -> 'a * 'a * 'a + +(** Print to string *) +val print_pp_to_string : (Format.formatter -> 'a -> unit) -> 'a -> string + +(** Replace all non [a-z A-Z 0-9] character of a string by [_] *) +val sanitize_string : string -> string +