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

Current Boolean pass for Heptagon

Browse source
This commit is contained in:
Gwenal Delaval 2011-05-05 11:54:38 +02:00
parent 8c4217ab83
commit 9e41fcf71f
5 changed files with 97 additions and 96 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
compiler/heptagon/main/hept_compiler.ml
View file

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

176
compiler/minils/transformations/boolean.ml → compiler/heptagon/transformations/boolean.ml
View file

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

4
compiler/minils/transformations/boolean.mli → compiler/heptagon/transformations/boolean.mli
View file

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

5
compiler/minils/main/mls_compiler.ml
View file

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

5
compiler/utilities/global/compiler_options.ml
View file

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