jeltz/heptagon
1
0
Fork 0
Code Issues Pull requests Releases Activity

Fresh vars, and ident refactoring.

Browse source 
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.
This commit is contained in:
Léonard Gérard 2010-12-14 18:29:55 +01:00
parent 83feda2afb
commit 2ae809c971
32 changed files with 227 additions and 150 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

53
compiler/global/idents.ml
View file

@ -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)

25
compiler/global/idents.mli
View file

@ -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 :

30
compiler/global/modules.ml
View file

@ -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

4
compiler/global/names.ml
View file

@ -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)

1
compiler/heptagon/analysis/statefull.ml
View file

@ -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;

14
compiler/heptagon/analysis/typing.ml
View file

@ -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

14
compiler/heptagon/hept_mapfold.ml
View file

@ -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

6
compiler/heptagon/parsing/hept_parser.mly
View file

@ -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

6
compiler/heptagon/parsing/hept_scoping.ml
View file

@ -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

18
compiler/heptagon/transformations/automata.ml
View file

@ -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 =

1
compiler/heptagon/transformations/inline.ml
View file

@ -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 =

7
compiler/heptagon/transformations/last.ml
View file

@ -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

11
compiler/heptagon/transformations/reset.ml
View file

@ -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 ->

12
compiler/main/hept2mls.ml
View file

@ -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 ;

2
compiler/main/heptc.ml
View file

@ -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;

12
compiler/main/mls2obc.ml
View file

@ -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

2
compiler/minils/analysis/clocking.ml
View file

@ -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 *)

2
compiler/minils/main/mls2seq.ml
View file

@ -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

6
compiler/minils/minils.ml
View file

@ -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;

6
compiler/minils/mls_mapfold.ml
View file

@ -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

2
compiler/minils/mls_printer.ml
View file

@ -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 "@[<v2>contract@\n%a%a@ assume %a@ enforce %a@ with (%a)@]"
print_local_vars l
print_eqs eqs

18
compiler/minils/parsing/mls_parser.mly
View file

@ -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 }

31
compiler/minils/transformations/callgraph.ml
View file

@ -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

2
compiler/minils/transformations/checkpass.ml
View file

@ -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

2
compiler/minils/transformations/introvars.ml
View file

@ -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)

16
compiler/minils/transformations/itfusion.ml
View file

@ -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

4
compiler/minils/transformations/normalize.ml
View file

@ -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' =

4
compiler/minils/transformations/singletonvars.ml
View file

@ -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

8
compiler/minils/transformations/tomato.ml
View file

@ -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

40
compiler/obc/c/cmain.ml
View file

@ -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));

11
compiler/utilities/misc.ml
View file

@ -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

7
compiler/utilities/misc.mli
View file

@ -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