From 9e41fcf71ff3afa4dc2b333c59cb9419b6bb069f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Gwena=EBl=20Delaval?= Date: Thu, 5 May 2011 11:54:38 +0200 Subject: [PATCH] Current Boolean pass for Heptagon --- compiler/heptagon/main/hept_compiler.ml | 3 + .../transformations/boolean.ml | 176 +++++++++--------- .../transformations/boolean.mli | 4 +- compiler/minils/main/mls_compiler.ml | 5 - compiler/utilities/global/compiler_options.ml | 5 +- 5 files changed, 97 insertions(+), 96 deletions(-) rename compiler/{minils => heptagon}/transformations/boolean.ml (87%) rename compiler/{minils => heptagon}/transformations/boolean.mli (89%) diff --git a/compiler/heptagon/main/hept_compiler.ml b/compiler/heptagon/main/hept_compiler.ml index f3a31cd..e6aafc1 100644 --- a/compiler/heptagon/main/hept_compiler.ml +++ b/compiler/heptagon/main/hept_compiler.ml @@ -56,6 +56,9 @@ let compile_program p = (* Iterator fusion *) let p = pass "Iterator fusion" !do_iterator_fusion Itfusion.program p pp in + (* Boolean pass *) + let p = pass "Boolean" !boolean Boolean.program p pp in + (* Normalization *) let p = pass "Normalization" true Normalize.program p pp in diff --git a/compiler/minils/transformations/boolean.ml b/compiler/heptagon/transformations/boolean.ml similarity index 87% rename from compiler/minils/transformations/boolean.ml rename to compiler/heptagon/transformations/boolean.ml index aeaa830..2371528 100644 --- a/compiler/minils/transformations/boolean.ml +++ b/compiler/heptagon/transformations/boolean.ml @@ -47,14 +47,14 @@ open Idents open Signature open Types open Clocks -open Minils +open Heptagon let fresh = Idents.gen_fresh "bool" (fun s -> s) let ty_bool = Tid({ qual = Pervasives; name = "bool"}) -let strue = mk_static_exp ~ty:ty_bool (Sbool(true)) -let sfalse = mk_static_exp ~ty:ty_bool (Sbool(false)) +let strue = mk_static_exp ty_bool (Sbool(true)) +let sfalse = mk_static_exp ty_bool (Sbool(false)) let sbool = function | true -> strue @@ -107,7 +107,7 @@ type varinfo = clocked_var : var_tree; } -type type_info = Type of tdesc | Enum of enuminfo +type type_info = Type of type_dec_desc | Enum of enuminfo let enum_types : type_info QualEnv.t ref = ref QualEnv.empty @@ -172,30 +172,6 @@ let rec var_list clist = let t = Tree(t1,t2) in nv2 + 1, vl, t -(* purge type declarations from enumerated types ; build enuminfo env *) -let build_enum_env type_dec_list = - - let build (acc_types,env_enum) type_dec = - match type_dec.t_desc with - | Type_enum clist -> - let (n,env,t) = var_list clist in - (acc_types, - QualEnv.add type_dec.t_name - (Enum({ ty_nb_var = n; - ty_assoc = env; - ty_tree = t})) - env_enum) - | tdesc -> - (type_dec::acc_types), - QualEnv.add type_dec.t_name - (Type(tdesc)) - env_enum - in - - let (acc_types,env_enum) = List.fold_left build ([],QualEnv.empty) type_dec_list in - enum_types := env_enum; - List.rev acc_types - let var_list prefix n = let rec varl acc = function | 0 -> acc @@ -240,8 +216,6 @@ let translate_ty ty = end | Tprod(ty_list) -> Tprod(List.map trans ty_list) | Tarray(ty,se) -> Tarray(trans ty,se) - | Tmutable ty -> Tmutable(trans ty) - | Tunit -> Tunit in trans ty @@ -270,6 +244,11 @@ let rec translate_ck env ck = Con(ck,c,n) end +let rec translate_ct env ct = + match ct with + | Ck(ck) -> Ck(translate_ck env ck) + | Cprod(l) -> Cprod(List.map (translate_ct env) l) + let translate_const c ty e = match c.se_desc,ty with | _, Tid({ qual = Pervasives; name = "bool" }) -> Econst(c) @@ -299,7 +278,8 @@ let translate_const c ty e = end | _ -> Econst(c) -let new_var_list d_list ty ck n = +(* TODO HERE : ct/ck *) +let new_var_list d_list ty ct n = let rec varl acc d_list = function | 0 -> acc,d_list | n -> @@ -318,7 +298,7 @@ let intro_tuple context e = Eapp({a_op=Etuple},e_l,None) -> context,e_l | _ -> let (d_list,eq_list) = context in - let v_list,d_list = new_var_list d_list ty_bool e.e_ck n in + let v_list,d_list = new_var_list d_list ty_bool e.e_ct_annot n in let pat = Etuplepat(List.map (fun v -> Evarpat(v)) v_list) in let eq_list = (mk_equation pat e) :: eq_list in let e_list = List.map (fun v -> { e with e_ty = ty_bool; e_desc = Evar(v) }) v_list in @@ -330,7 +310,7 @@ let rec when_list e bl vtree = | b::bl', VNode(v,t0,t1) -> let (c,t) = if b then (ctrue,t1) else (cfalse,t0) in let e_when = { e with - e_ck = Con(e.e_ck,c,v); + e_ct_annot = Con(e.e_ct_annot,c,v); e_desc = Ewhen(e,c,v) } in when_list e_when bl' t | _::_, Vempty -> failwith("when_list: non-coherent boolean list and tree") @@ -340,23 +320,23 @@ let rec when_ck desc ty ck = | Cbase | Cvar _ -> { e_desc = desc; e_base_ck = Cbase; - e_ck = ck; + e_ct_annot = ck; e_ty = ty; e_loc = no_location } | Con(ck',c,v) -> let e = when_ck desc ty ck' in { e_desc = Ewhen(e,c,v); e_base_ck = Cbase; - e_ck = ck; + e_ct_annot = ck; e_ty = ty; e_loc = no_location } let rec base_value ck ty = match ty with | Tid({qual = Pervasives; name = "int" }) -> - when_ck (Econst(mk_static_exp ~ty:ty (Sint(0)))) ty ck + when_ck (Econst(mk_static_exp ty (Sint(0)))) ty ck | Tid({qual = Pervasives; name = "float"}) -> - when_ck (Econst(mk_static_exp ~ty:ty (Sfloat(0.)))) ty ck + when_ck (Econst(mk_static_exp ty (Sfloat(0.)))) ty ck | Tid({qual = Pervasives; name = "bool" }) -> when_ck (Econst(strue)) ty ck | Tid(sname) -> @@ -370,7 +350,7 @@ let rec base_value ck ty = | Type(Type_alias aty) -> base_value ck aty | Type(Type_enum(l)) -> when_ck - (Econst(mk_static_exp ~ty:ty (Sconstructor(List.hd l)))) + (Econst(mk_static_exp ty (Sconstructor(List.hd l)))) ty ck | Type(Type_struct(l)) -> let fields = @@ -390,7 +370,7 @@ let rec base_value ck ty = { e_desc = mk_tuple e_list; e_ty = Tprod(List.map (fun _ -> ty_bool) e_list); e_base_ck = Cbase; - e_ck = ck; + e_ct_annot = ck; e_loc = no_location } end with Not_found -> @@ -401,7 +381,7 @@ let rec base_value ck ty = { e_desc = mk_tuple e_list; e_ty = Tprod(List.map (fun e -> e.e_ty) e_list); e_base_ck = Cbase; - e_ck = ck; + e_ct_annot = ck; e_loc = no_location; } | Tarray(ty,se) -> @@ -409,17 +389,7 @@ let rec base_value ck ty = { e_desc = Eapp((mk_app ~params:[se] Earray_fill), [e], None); e_ty = Tarray(e.e_ty,se); e_base_ck = Cbase; - e_ck = ck; - e_loc = no_location; - } - | Tmutable ty -> - let e = base_value ck ty in - e - | Tunit -> - { e_desc = Eapp (mk_app Etuple, [], None); - e_ty = Tunit; - e_base_ck = Cbase; - e_ck = ck; + e_ct_annot = ck; e_loc = no_location; } @@ -428,7 +398,7 @@ let rec merge_tree ck ty e_map btree vtree = | Node(None), _ -> base_value ck ty | Node(Some name), _ -> let e = QualEnv.find name e_map in - { e with e_ck = ck } + { e with e_ct_annot = ck } | Tree(t1,t2), VNode(v,vt1,vt2) -> let e1 = merge_tree (Con(ck,ctrue,v)) ty e_map t1 vt1 and e2 = merge_tree (Con(ck,cfalse,v)) ty e_map t2 vt2 @@ -436,12 +406,13 @@ let rec merge_tree ck ty e_map btree vtree = { e_desc = Emerge(v,[(ctrue,e1);(cfalse,e2)]); e_ty = ty; e_base_ck = Cbase; - e_ck = ck; + e_ct_annot = ck; e_loc = no_location } | Tree (_,_), Vempty -> failwith("merge_tree: non-coherent trees") -let rec translate env context ({e_desc = desc; e_ty = ty; e_ck = ck} as e) = - let ck = translate_ck env ck in + +let rec translate env context ({e_desc = desc; e_ty = ty; e_ct_annot = ck} as e) = + let ck = translate_ct env ck in let context,desc = match desc with | Econst(c) -> @@ -457,7 +428,7 @@ let rec translate env context ({e_desc = desc; e_ty = ty; e_ck = ck} as e) = mk_tuple (List.map (fun v -> { e with e_ty = ty_bool; - e_ck = ck; + e_ct_annot = ck; e_desc = Evar(v); }) ident_list) with Not_found -> Evar(name) @@ -542,7 +513,7 @@ let rec translate env context ({e_desc = desc; e_ty = ty; e_ck = ck} as e) = context,{ e with e_desc = desc; e_ty = translate_ty ty; - e_ck = ck} + e_ct_annot = ck} and translate_list env context e_list = let context,acc_e = @@ -553,11 +524,22 @@ and translate_list env context e_list = (context,[]) e_list in context,List.rev acc_e -let translate_eq env context ({ eq_lhs = pat; eq_rhs = e } as eq) = - let pat = translate_pat env pat in - let (d_list,eq_list),e = translate env context e in - d_list,{ eq with eq_lhs = pat; eq_rhs = e }::eq_list - +let translate_eq env context ({eq_desc = desc} as eq) = + let desc,(d_list,eq_list) = + match desc with + | Eblock block -> + let block, _ = translate_block env [] [] block in + Eblock block, + context + | Eeq(pat,e) -> + let pat = translate_pat env pat in + let context,e = translate env context e in + Eeq(pat,e), + context + | _ -> failwith("Boolean pass: control structures should be removed") + in + d_list,{ eq with desc = desc }::eq_list + let translate_eqs env eq_list = List.fold_left (fun context eq -> @@ -579,7 +561,7 @@ let var_dec_list (acc_vd,acc_loc,acc_eq) var_from n = | [], _ -> { e_desc = Evar(var); e_base_ck = Cbase; - e_ck = ck; + e_ct_annot = Ck(ck); e_ty = ty_bool; e_loc = no_location } | _ckvar::l, Con(ck',c,v) -> @@ -587,7 +569,7 @@ let var_dec_list (acc_vd,acc_loc,acc_eq) var_from n = let e = when_ck l ck' var in { e_desc = Ewhen(e,c,v); e_base_ck = Cbase; - e_ck = ck; + e_ct_annot = Ck(ck); e_ty = ty_bool; e_loc = no_location } | _ -> failwith("when_ck: non coherent clock and var list") @@ -650,6 +632,7 @@ let var_dec_list (acc_vd,acc_loc,acc_eq) var_from n = let acc_loc = { v_ident = id; v_type = ty_bool; v_clock = ck; + v_last = Var; v_loc = no_location } :: acc_loc in (* vi_... = vi when ... when (True|False)(v1) *) let acc_eq = @@ -683,7 +666,7 @@ let var_dec_list (acc_vd,acc_loc,acc_eq) var_from n = let buildenv_var_dec (acc_vd,acc_loc,acc_eq,env) ({v_type = ty} as v) = match ty with - | Tprod _ | Tarray _ | Tmutable _ | Tunit -> + | Tprod _ | Tarray _ -> v::acc_vd, acc_loc, acc_eq, env | Tid(tname) -> begin @@ -723,6 +706,18 @@ let translate_var_dec env ({ v_clock = ck } as v) = let translate_var_dec_list env vlist = List.map (translate_var_dec env) vlist +let translate_block env add_locals add_eqs ({ b_local = v; + b_equs = eq_list; } as b) = + let v, v',v_eq,env = buildenv_var_dec_list env v in + let v = v@v'@add_locals in + let v = translate_var_dec_list env v in + let eq_list = eq_list@v_eq@add_eqs in + let context = translate_eqs env eq_list in + let d_list,eq_list = context in + { b with + b_local = v@d_list; + b_equs = eq_list }, env + let translate_contract env contract = match contract with | None -> None, env @@ -730,45 +725,52 @@ let translate_contract env contract = c_eq = eq_list; c_assume = e_a; c_enforce = e_g; - c_controllables = cl } -> + c_controllables = cl; + c_block = b } -> let cl, cl_loc, cl_eq, env = buildenv_var_dec_list env cl in let cl = translate_var_dec_list env cl in - let v, v', v_eq, env' = buildenv_var_dec_list env v in - let v = v@v'@cl_loc in - let v = translate_var_dec_list env v in - let eq_list = eq_list@v_eq@cl_eq in - let context = translate_eqs env' eq_list in - let context, e_a = translate env' context e_a in + let ({ b_local = v; + b_equs = eqs } as b), env' + = translate_block env cl_loc cl_eq b in + let context, e_a = translate env' (v,eqs) e_a in let context, e_g = translate env' context e_g in let (d_list,eq_list) = context in - Some { c_local = v@d_list; + Some { c_block = { b with + b_local = d_list; + b_equs = eq_list }; c_eq = eq_list; c_assume = e_a; c_enforce = e_g; c_controllables = cl }, env -let node ({ n_local = locals; - n_input = inputs; +let node ({ n_input = inputs; n_output = outputs; n_contract = contract; - n_equs = eq_list } as n) = + n_block = b } as n) = let inputs,in_loc,in_eq,env = buildenv_var_dec_list Env.empty inputs in let outputs,out_loc,out_eq,env = buildenv_var_dec_list env outputs in let contract, env = translate_contract env contract in - let locals,locals',loc_eq,env = buildenv_var_dec_list env locals in - let locals = locals@locals'@in_loc@out_loc in - let locals = translate_var_dec_list env locals in - let eq_list = eq_list@loc_eq@in_eq@out_eq in - let (d_list,eq_list) = translate_eqs env eq_list in + let add_locals = in_loc@out_loc in + let add_eqs = in_eq@out_eq in + let b = translate_block env add_locals add_eqs b in { n with - n_local = locals@d_list; n_input = List.rev inputs; n_output = List.rev outputs; n_contract = contract; - n_equs = eq_list } + n_block = b } -let program ({ p_types = pt_list; p_nodes = n_list } as p) = - let pt_list = build_enum_env pt_list in - let n_list = List.map node n_list in - { p with p_types = pt_list; p_nodes = n_list } +let build type_dec = + let tenv = + match type_dec.t_desc with + | Type_enum clist -> + let (n,env,t) = var_list clist in + Enum({ ty_nb_var = n; + ty_assoc = env; + ty_tree = t}) + | tdesc -> Type(tdesc) in + enum_types := QualEnv.add type_dec.t_name tenv !enum_types + +let program ({ p_types = t_list; p_nodes = n_list } as p) = + List.iter build t_list; + { p with p_nodes = List.map node n_list } diff --git a/compiler/minils/transformations/boolean.mli b/compiler/heptagon/transformations/boolean.mli similarity index 89% rename from compiler/minils/transformations/boolean.mli rename to compiler/heptagon/transformations/boolean.mli index 4b58411..c98bbd5 100644 --- a/compiler/minils/transformations/boolean.mli +++ b/compiler/heptagon/transformations/boolean.mli @@ -2,7 +2,7 @@ (* *) (* Heptagon/BZR *) (* *) -(* Author : Gwenaël Delaval *) +(* Author : Gwena�l Delaval *) (* Organization : INRIA Rennes, VerTeCs *) (* *) (****************************************************) @@ -31,4 +31,4 @@ (* $Id: boolean.mli 74 2009-03-11 10:21:25Z delaval $ *) -val program : Minils.program -> Minils.program +val program : Heptagon.program -> Heptagon.program diff --git a/compiler/minils/main/mls_compiler.ml b/compiler/minils/main/mls_compiler.ml index 8c1d802..91f40f7 100644 --- a/compiler/minils/main/mls_compiler.ml +++ b/compiler/minils/main/mls_compiler.ml @@ -31,11 +31,6 @@ let compile_program p = pass "Automata minimization checks" true Tomato.tomato_checks p pp in *) - (* Boolean translation of enumerated values *) - let sigali = List.mem "z3z" !target_languages in - let p = - pass "Boolean transformation" (!boolean or sigali) Boolean.program p pp in - (* Scheduling *) let p = pass "Scheduling" true Schedule.program p pp in diff --git a/compiler/utilities/global/compiler_options.ml b/compiler/utilities/global/compiler_options.ml index f1b3b72..db72e35 100644 --- a/compiler/utilities/global/compiler_options.ml +++ b/compiler/utilities/global/compiler_options.ml @@ -61,10 +61,13 @@ let set_simulation_node s = let create_object_file = ref false +let boolean = ref false + (* Target languages list for code generation *) let target_languages : string list ref = ref [] let add_target_language s = + if s = "z3z" then boolean := true; target_languages := s :: !target_languages (* Optional path for generated files (C or Java) *) @@ -85,8 +88,6 @@ let add_inlined_node s = inline := s :: !inline let flatten = ref false -let boolean = ref false - let deadcode = ref false let tomato = ref false