Boolean transformation pass (translate every enumeration type to boolean tuples)
This commit is contained in:
Gwenal Delaval
parent
d6240e1c67
commit
4e267d82c6
|
|
@ -99,6 +99,8 @@ let main () =
|
|||
"-stdlib", Arg.String set_stdlib, doc_stdlib;
|
||||
"-c", Arg.Set create_object_file, doc_object_file;
|
||||
"-s", Arg.String set_simulation_node, doc_sim;
|
||||
"-bool", Arg.Set boolean, doc_boolean;
|
||||
"-deadcode", Arg.Set deadcode, doc_deadcode;
|
||||
"-tomato", Arg.Set tomato, doc_tomato;
|
||||
"-tomanode", read_qualname add_tomato_node, doc_tomato;
|
||||
"-tomacheck", read_qualname add_tomato_check, "";
|
||||
|
|
|
|||
|
|
@ -30,6 +30,11 @@ let compile_program p =
|
|||
let 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
|
||||
|
|
|
|||
738
compiler/minils/transformations/boolean.ml
Normal file
738
compiler/minils/transformations/boolean.ml
Normal file
|
|
@ -0,0 +1,738 @@
|
|||
(****************************************************)
|
||||
(* *)
|
||||
(* Heptagon/BZR *)
|
||||
(* *)
|
||||
(* Author : Gwenaël Delaval *)
|
||||
(* Organization : INRIA Rennes, VerTeCs *)
|
||||
(* *)
|
||||
(****************************************************)
|
||||
|
||||
(*
|
||||
Translate enumerated types (state variables) into boolean
|
||||
|
||||
type t = A | B | C | D
|
||||
|
||||
A --> 00
|
||||
B --> 01
|
||||
C --> 10
|
||||
D --> 11
|
||||
|
||||
x : t --> x1,x2,x2_0,x2_1 : bool (x2_i for keeping correct clocks)
|
||||
|
||||
x = B;
|
||||
-->
|
||||
(x1,x2) = (0,1);
|
||||
x2_0 = x2 when False(x1);
|
||||
x2_1 = x2 when True(x1);
|
||||
|
||||
(e when A(x))
|
||||
-->
|
||||
(e when False(x1)) when False(x2_0)
|
||||
|
||||
ck on A(x)
|
||||
-->
|
||||
ck on False(x1) on False(x2_0)
|
||||
|
||||
merge x (A -> e0) (B -> e1) (C -> e2) (D -> e3)
|
||||
-->
|
||||
merge x1 (False -> merge x2_0 (False -> e0) (True -> e1))
|
||||
(True -> merge x2_1 (False -> e2) (True -> e3))
|
||||
*)
|
||||
|
||||
(* $Id: boolean.ml 833 2010-02-10 14:15:00Z delaval $ *)
|
||||
|
||||
open Names
|
||||
open Location
|
||||
open Idents
|
||||
open Signature
|
||||
open Types
|
||||
open Clocks
|
||||
open Minils
|
||||
|
||||
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 sbool = function
|
||||
| true -> strue
|
||||
| false -> sfalse
|
||||
|
||||
let ctrue = { qual = "Pervasives"; name = "true" }
|
||||
let cfalse = { qual = "Pervasives"; name = "false" }
|
||||
|
||||
let mk_tuple e_l =
|
||||
Eapp((mk_app Etuple),e_l,None)
|
||||
|
||||
(* boolean decision tree ; left branch for true ; nodes are constructors *)
|
||||
type btree = Node of constructor_name option | Tree of btree * btree
|
||||
|
||||
(* info associated to each enum type *)
|
||||
type enuminfo =
|
||||
{
|
||||
ty_nb_var : int; (* nb of boolean var representing this type *)
|
||||
ty_assoc : bool list QualEnv.t;
|
||||
ty_tree : btree
|
||||
}
|
||||
|
||||
(* ty_nb_var = n : var x of enum type will be represented by
|
||||
boolean variables x_1,...,x_n
|
||||
|
||||
ty_assoc(A) = [b_1,...,b_n] : constant A will be represented by
|
||||
x_1,...,x_n where x_i = b_i
|
||||
|
||||
assert length(ty_assoc(A)) = ty_nb_var
|
||||
*)
|
||||
|
||||
(* Type var_tree : variable binary tree, each variable being of clock
|
||||
of its direct father (false clock for left son, true for right son).
|
||||
|
||||
Then if x translates to (x1,x2)
|
||||
the corresponding var_tree is
|
||||
x1
|
||||
/ \
|
||||
x2_0 x2_1
|
||||
|
||||
x2_0 being on clock False(x1)
|
||||
x2_1 being on clock True(x1)
|
||||
*)
|
||||
type var_tree = Vempty | VNode of var_ident * var_tree * var_tree
|
||||
|
||||
type varinfo =
|
||||
{
|
||||
var_enum : enuminfo;
|
||||
var_list : var_ident list;
|
||||
clocked_var : var_tree;
|
||||
}
|
||||
|
||||
type type_info = Type of tdesc | Enum of enuminfo
|
||||
|
||||
let enum_types : type_info QualEnv.t ref = ref QualEnv.empty
|
||||
|
||||
let get_enum name =
|
||||
QualEnv.find name !enum_types
|
||||
|
||||
(* split2 k [x1;...;xn] = ([x1;...;xk],[xk+1;...;xn]) *)
|
||||
let split2 n l =
|
||||
let rec splitaux k acc l =
|
||||
if k = 0 then (acc,l) else
|
||||
begin
|
||||
match l with
|
||||
| x::t -> splitaux (k-1) (x::acc) t
|
||||
| _ -> assert false
|
||||
end in
|
||||
let (l1,l2) = splitaux n [] l in
|
||||
(List.rev l1,l2)
|
||||
|
||||
|
||||
|
||||
(* create an info from the elements of a name list *)
|
||||
let rec var_list clist =
|
||||
match clist with
|
||||
| [] -> (0,QualEnv.empty,Node(None))
|
||||
| [c] -> (1, QualEnv.add c [true] QualEnv.empty, Tree(Node(Some c),Node(None)))
|
||||
| [c1;c2] -> (1,
|
||||
QualEnv.add c1 [true] (QualEnv.add c2 [false] QualEnv.empty),
|
||||
Tree(Node(Some c1),Node(Some c2)))
|
||||
| l ->
|
||||
let n = List.length l in
|
||||
let n1 = n asr 1 in
|
||||
let l1,l2 = split2 n1 l in
|
||||
let (nv1,vl1,t1) = var_list l1
|
||||
and (nv2,vl2,t2) = var_list l2 in
|
||||
(* test and debug *)
|
||||
(* assert ((nv1 = nv2) or (nv1 = nv2 - 1)); *)
|
||||
(* QualEnv.iter (fun _ l -> assert ((List.length l) = nv1)) vl1; *)
|
||||
(* QualEnv.iter (fun _ l -> assert ((List.length l) = nv2)) vl2; *)
|
||||
(* let nt1 = *)
|
||||
(* begin *)
|
||||
(* match (count t1) with *)
|
||||
(* None -> assert false *)
|
||||
(* | Some n -> n *)
|
||||
(* end in *)
|
||||
(* assert (nt1 = nv1); *)
|
||||
(* let nt2 = *)
|
||||
(* begin *)
|
||||
(* match (count t2) with *)
|
||||
(* | None -> assert false *)
|
||||
(* | Some n -> n *)
|
||||
(* end in *)
|
||||
(* assert (nt2 = nv2); *)
|
||||
let vl =
|
||||
QualEnv.fold (fun c l m -> QualEnv.add c (false::l) m) vl2
|
||||
(QualEnv.fold
|
||||
(if nv1 = nv2
|
||||
then (fun c l m -> QualEnv.add c (true::l) m)
|
||||
else (fun c l m -> QualEnv.add c (true::false::l) m))
|
||||
vl1
|
||||
QualEnv.empty) in
|
||||
let t1 = if nv1 = nv2 then t1 else Tree(Node(None),t1) in
|
||||
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
|
||||
| n ->
|
||||
let acc = (prefix ^ "_" ^ (string_of_int n)) :: acc in
|
||||
varl acc (n-1) in
|
||||
varl [] n
|
||||
|
||||
let translate_pat env pat =
|
||||
let rec trans = function
|
||||
| Evarpat(name) ->
|
||||
begin
|
||||
try
|
||||
let info = Env.find name env in
|
||||
match info.var_enum.ty_nb_var with
|
||||
| 1 ->
|
||||
Evarpat(List.nth info.var_list 0)
|
||||
| _ ->
|
||||
let varpat_list = info.var_list in
|
||||
Etuplepat(List.map (fun v -> Evarpat(v)) varpat_list)
|
||||
with Not_found -> Evarpat(name)
|
||||
end
|
||||
| Etuplepat(pat_list) -> Etuplepat(List.map trans pat_list) in
|
||||
trans pat
|
||||
|
||||
let translate_ty ty =
|
||||
let rec trans ty =
|
||||
match ty with
|
||||
| Tid({ qual = "Pervasives"; name = "bool" }) -> ty
|
||||
| Tid(name) ->
|
||||
begin
|
||||
try
|
||||
let info = get_enum name in
|
||||
begin match info with
|
||||
| Type(_) -> ty
|
||||
| Enum { ty_nb_var = 1 } -> ty_bool
|
||||
| Enum { ty_nb_var = n } ->
|
||||
let strlist = var_list "" n in
|
||||
Tprod(List.map (fun _ -> ty_bool) strlist)
|
||||
end
|
||||
with Not_found -> ty
|
||||
end
|
||||
| Tprod(ty_list) -> Tprod(List.map trans ty_list)
|
||||
| Tarray(ty,se) -> Tarray(trans ty,se)
|
||||
in
|
||||
trans ty
|
||||
|
||||
let rec on_list ck bl vtree =
|
||||
match bl, vtree with
|
||||
| [], _ -> ck
|
||||
| b::bl', VNode(v,t0,t1) ->
|
||||
let (c,t) = if b then (ctrue,t1) else (cfalse,t0) in
|
||||
on_list (Con(ck,c,v)) bl' t
|
||||
| _::_, Vempty -> failwith("on_list: non-coherent boolean list and tree")
|
||||
|
||||
let rec translate_ck env ck =
|
||||
match ck with
|
||||
| Cbase -> Cbase
|
||||
| Cvar {contents = Clink(ck)} -> translate_ck env ck
|
||||
| Cvar {contents = Cindex(_)} -> ck
|
||||
| Con(ck,c,n) ->
|
||||
let ck = translate_ck env ck in
|
||||
begin
|
||||
try
|
||||
let info = Env.find n env in
|
||||
let bl = QualEnv.find c info.var_enum.ty_assoc in
|
||||
on_list ck bl info.clocked_var
|
||||
with Not_found ->
|
||||
Printf.printf "Not found in env : %s\n" (name n);
|
||||
(* Boolean clock *)
|
||||
Con(ck,c,n)
|
||||
end
|
||||
|
||||
let translate_const c ty e =
|
||||
match c.se_desc,ty with
|
||||
| _, Tid({ qual = "Pervasives"; name = "bool" }) -> Econst(c)
|
||||
| Sconstructor(cname),Tid(tname) ->
|
||||
begin
|
||||
try
|
||||
begin
|
||||
match (get_enum tname) with
|
||||
| Type _ -> Econst(c)
|
||||
| Enum { ty_assoc = assoc } ->
|
||||
let bl = QualEnv.find cname assoc in
|
||||
let b_list = List.map (fun b -> Econst(sbool b)) bl in
|
||||
begin
|
||||
match b_list with
|
||||
| [] -> assert false
|
||||
| [b] -> b
|
||||
| _::_ ->
|
||||
mk_tuple
|
||||
(List.map
|
||||
(fun b -> {e with
|
||||
e_desc = b;
|
||||
e_ty = ty_bool })
|
||||
b_list)
|
||||
end
|
||||
end
|
||||
with Not_found -> Econst(c)
|
||||
end
|
||||
| _ -> Econst(c)
|
||||
|
||||
let new_var_list d_list ty ck n =
|
||||
let rec varl acc d_list = function
|
||||
| 0 -> acc,d_list
|
||||
| n ->
|
||||
let v = fresh "bool" in
|
||||
let acc = v :: acc in
|
||||
let d_list = (mk_var_dec ~clock:ck v ty) :: d_list in
|
||||
varl acc d_list (n-1) in
|
||||
varl [] d_list n
|
||||
|
||||
let intro_tuple context e =
|
||||
let n =
|
||||
match e.e_ty with
|
||||
| Tprod(l) -> List.length l
|
||||
| _ -> assert false in
|
||||
match e.e_desc with
|
||||
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 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
|
||||
(d_list,eq_list),e_list
|
||||
|
||||
let rec when_list e bl vtree =
|
||||
match bl, vtree with
|
||||
| [], _ -> e
|
||||
| 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_desc = Ewhen(e,c,v) } in
|
||||
when_list e_when bl' t
|
||||
| _::_, Vempty -> failwith("when_list: non-coherent boolean list and tree")
|
||||
|
||||
let rec when_ck desc ty ck =
|
||||
match ck with
|
||||
| Cbase | Cvar _ ->
|
||||
{ e_desc = desc;
|
||||
e_ck = 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_ck = 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
|
||||
| Tid({qual = "Pervasives"; name = "float"}) ->
|
||||
when_ck (Econst(mk_static_exp ~ty:ty (Sfloat(0.)))) ty ck
|
||||
| Tid({qual = "Pervasives"; name = "bool" }) ->
|
||||
when_ck (Econst(strue)) ty ck
|
||||
| Tid(sname) ->
|
||||
begin
|
||||
try
|
||||
begin
|
||||
let info = get_enum sname in
|
||||
(* boolean tuple *)
|
||||
match info with
|
||||
| Type(Type_abs) -> failwith("Abstract types not implemented")
|
||||
| Type(Type_alias aty) -> base_value ck aty
|
||||
| Type(Type_enum(l)) ->
|
||||
when_ck
|
||||
(Econst(mk_static_exp ~ty:ty (Sconstructor(List.hd l))))
|
||||
ty ck
|
||||
| Type(Type_struct(l)) ->
|
||||
let fields =
|
||||
List.map
|
||||
(fun {f_name = name; f_type = ty} ->
|
||||
name,(base_value ck ty))
|
||||
l in
|
||||
when_ck (Estruct(fields)) ty ck
|
||||
| Enum { ty_nb_var = 1 } ->
|
||||
when_ck (Econst(strue)) ty_bool ck
|
||||
| Enum { ty_nb_var = n } ->
|
||||
let e = when_ck (Econst(strue)) ty_bool ck in
|
||||
let rec aux acc = function
|
||||
| 0 -> acc
|
||||
| n -> aux (e::acc) (n-1) in
|
||||
let e_list = aux [] n in
|
||||
{ e_desc = mk_tuple e_list;
|
||||
e_ty = Tprod(List.map (fun _ -> ty_bool) e_list);
|
||||
e_ck = ck;
|
||||
e_loc = no_location }
|
||||
end
|
||||
with Not_found ->
|
||||
Printf.printf "Name : %s\n" sname.name; assert false
|
||||
end
|
||||
| Tprod(ty_list) ->
|
||||
let e_list = List.map (base_value ck) ty_list in
|
||||
{ e_desc = mk_tuple e_list;
|
||||
e_ty = Tprod(List.map (fun e -> e.e_ty) e_list);
|
||||
e_ck = ck;
|
||||
e_loc = no_location;
|
||||
}
|
||||
| Tarray(ty,se) ->
|
||||
let e = base_value ck ty in
|
||||
{ e_desc = Eapp((mk_app ~params:[se] Earray_fill), [e], None);
|
||||
e_ty = Tarray(e.e_ty,se);
|
||||
e_ck = ck;
|
||||
e_loc = no_location;
|
||||
}
|
||||
|
||||
let rec merge_tree ck ty e_map btree vtree =
|
||||
match btree, vtree with
|
||||
| Node(None), _ -> base_value ck ty
|
||||
| Node(Some name), _ ->
|
||||
let e = QualEnv.find name e_map in
|
||||
{ e with e_ck = 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
|
||||
in
|
||||
{ e_desc = Emerge(v,[(ctrue,e1);(cfalse,e2)]);
|
||||
e_ty = ty;
|
||||
e_ck = 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 context,desc =
|
||||
match desc with
|
||||
| Econst(c) ->
|
||||
context, translate_const c ty e
|
||||
| Evar(name) ->
|
||||
let desc = begin
|
||||
try
|
||||
let info = Env.find name env in
|
||||
if info.var_enum.ty_nb_var = 1 then
|
||||
Evar(List.nth info.var_list 0)
|
||||
else
|
||||
let ident_list = info.var_list in
|
||||
mk_tuple (List.map
|
||||
(fun v -> { e with
|
||||
e_ty = ty_bool;
|
||||
e_ck = ck;
|
||||
e_desc = Evar(v); })
|
||||
ident_list)
|
||||
with Not_found -> Evar(name)
|
||||
end in
|
||||
context,desc
|
||||
| Efby(None, e) ->
|
||||
let context,e = translate env context e in
|
||||
context,Efby(None,e)
|
||||
| Efby(Some c,e) ->
|
||||
let e_c = translate_const c ty e in
|
||||
let context,e = translate env context e in
|
||||
begin
|
||||
match e_c with
|
||||
| Econst(c) -> context,Efby(Some c,e)
|
||||
| Eapp({ a_op = Etuple },e_c_l,None) ->
|
||||
let context,e_l = intro_tuple context e in
|
||||
let c_l = List.map (function
|
||||
| { e_desc = Econst(c) } -> c
|
||||
| _ -> assert false) e_c_l in
|
||||
context,
|
||||
mk_tuple
|
||||
(List.map2
|
||||
(fun c e -> { e with
|
||||
e_ty = ty_bool;
|
||||
e_desc = Efby(Some c,e)})
|
||||
c_l e_l)
|
||||
| _ -> assert false
|
||||
end
|
||||
| Eapp(app, e_list, r) ->
|
||||
let context,e_list = translate_list env context e_list in
|
||||
context, Eapp(app, e_list, r)
|
||||
| Ewhen(e,c,ck) ->
|
||||
let context,e = translate env context e in
|
||||
begin
|
||||
try
|
||||
let info = Env.find ck env in
|
||||
let bl = QualEnv.find c info.var_enum.ty_assoc in
|
||||
let e_when = when_list e bl info.clocked_var in
|
||||
context,e_when.e_desc
|
||||
with Not_found ->
|
||||
(* Boolean clock *)
|
||||
context,Ewhen(e,c,ck)
|
||||
end
|
||||
| Emerge(ck_m,l) (* of name * (longname * exp) list *)
|
||||
->
|
||||
begin
|
||||
try
|
||||
let info = Env.find ck_m env in
|
||||
let context,e_map = List.fold_left
|
||||
(fun (context,e_map) (n,e) ->
|
||||
let context,e = translate env context e in
|
||||
context,QualEnv.add n e e_map)
|
||||
(context,QualEnv.empty) l in
|
||||
let e_merge =
|
||||
merge_tree ck ty e_map
|
||||
info.var_enum.ty_tree
|
||||
info.clocked_var in
|
||||
context,e_merge.e_desc
|
||||
with Not_found ->
|
||||
(* Boolean clock *)
|
||||
let context, l =
|
||||
List.fold_left
|
||||
(fun (context,acc_l) (n,e) ->
|
||||
let context,e = translate env context e in
|
||||
context, (n,e)::acc_l)
|
||||
(context,[]) l in
|
||||
context,Emerge(ck_m,l)
|
||||
end
|
||||
| Estruct(l) ->
|
||||
let context,acc =
|
||||
List.fold_left
|
||||
(fun (context,acc) (c,e) ->
|
||||
let context,e = translate env context e in
|
||||
(context,(c,e)::acc))
|
||||
(context,[]) l in
|
||||
context,Estruct(List.rev acc)
|
||||
| Eiterator(it,app,se,e_list,r) ->
|
||||
let context,e_list = translate_list env context e_list in
|
||||
context,Eiterator(it,app,se,e_list,r)
|
||||
in
|
||||
context,{ e with
|
||||
e_desc = desc;
|
||||
e_ty = translate_ty ty;
|
||||
e_ck = ck}
|
||||
|
||||
and translate_list env context e_list =
|
||||
let context,acc_e =
|
||||
List.fold_left
|
||||
(fun (context,acc_e) e ->
|
||||
let context,e = translate env context e in
|
||||
(context,e::acc_e))
|
||||
(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_eqs env eq_list =
|
||||
List.fold_left
|
||||
(fun context eq ->
|
||||
translate_eq env context eq) ([],[]) eq_list
|
||||
|
||||
(* Tranlate variable declaration list : outputs
|
||||
- new declaration list
|
||||
- added local variables suffixed with "(_(1|0))*" for clock coherence
|
||||
- equations of these added variables
|
||||
*)
|
||||
let var_dec_list (acc_vd,acc_loc,acc_eq) var_from n =
|
||||
|
||||
(* when_ck [v3_1_0;v2_1;v1] (ck on True(v1) on False(v2_1) on True(v3_1_0)) v4
|
||||
= ((v4 when True(v1)) when False(v2_1)) when True(v3_1_0)
|
||||
-> builds v4_1_0_1
|
||||
*)
|
||||
let rec when_ck ckvar_list ck var =
|
||||
match ckvar_list,ck with
|
||||
| [], _ ->
|
||||
{ e_desc = Evar(var);
|
||||
e_ck = ck;
|
||||
e_ty = ty_bool;
|
||||
e_loc = no_location }
|
||||
| _ckvar::l, Con(ck',c,v) ->
|
||||
(* assert v = _ckvar *)
|
||||
let e = when_ck l ck' var in
|
||||
{ e_desc = Ewhen(e,c,v);
|
||||
e_ck = ck;
|
||||
e_ty = ty_bool;
|
||||
e_loc = no_location }
|
||||
| _ -> failwith("when_ck: non coherent clock and var list")
|
||||
in
|
||||
|
||||
let prefix = name var_from.v_ident in
|
||||
|
||||
(* From v, build of v1...vn *)
|
||||
let rec varl acc_vd k =
|
||||
if k>n
|
||||
then acc_vd
|
||||
else
|
||||
begin
|
||||
let var_prefix = prefix ^ "_" ^ (string_of_int k) in
|
||||
let var = fresh var_prefix in
|
||||
(* addition of var_k *)
|
||||
let acc_vd = { var_from with
|
||||
v_ident = var;
|
||||
v_type = ty_bool } :: acc_vd in
|
||||
varl acc_vd (k+1)
|
||||
end in
|
||||
|
||||
let vd_list = varl [] 1 in
|
||||
(* v_list = [vn;...;v1] *)
|
||||
let acc_vd = List.rev_append vd_list acc_vd in
|
||||
|
||||
let v_list = List.rev_map (fun vd -> vd.v_ident) vd_list in
|
||||
|
||||
(* From v1...vn, build clocked tree
|
||||
( vi_(0|1)* on ... on (True|False) (v1) ) *)
|
||||
let rec clocked_tree (acc_loc,acc_eq) acc_var suffix v_list ck =
|
||||
begin match v_list, acc_var with
|
||||
[], _ ->
|
||||
(* Leafs *)
|
||||
acc_loc,acc_eq,Vempty
|
||||
| v1::v_list, [] ->
|
||||
(* Root : no new id, only rec calls for sons *)
|
||||
(* Build left son (ck on False(vi_...)) *)
|
||||
let ck_0 = Con(ck,cfalse,v1) in
|
||||
let acc_loc,acc_eq,t0 =
|
||||
clocked_tree
|
||||
(acc_loc,acc_eq)
|
||||
([v1])
|
||||
("_0")
|
||||
v_list ck_0 in
|
||||
(* Build right son (ck on True(vi_...))*)
|
||||
let ck_1 = Con(ck,ctrue,v1) in
|
||||
let acc_loc,acc_eq,t1 =
|
||||
clocked_tree
|
||||
(acc_loc,acc_eq)
|
||||
([v1])
|
||||
("_1")
|
||||
v_list ck_1 in
|
||||
acc_loc,acc_eq,VNode(v1,t0,t1)
|
||||
| vi::v_list, _ ->
|
||||
(* Build name vi_(0|1)* *)
|
||||
let v = (sourcename vi) ^ suffix in
|
||||
(* Build ident from this name *)
|
||||
let id = fresh v in
|
||||
let acc_loc = { v_ident = id;
|
||||
v_type = ty_bool;
|
||||
v_clock = ck;
|
||||
v_loc = no_location } :: acc_loc in
|
||||
(* vi_... = vi when ... when (True|False)(v1) *)
|
||||
let acc_eq =
|
||||
{ eq_lhs = Evarpat(id);
|
||||
eq_rhs = when_ck acc_var ck vi;
|
||||
eq_loc = no_location }::acc_eq in
|
||||
(* Build left son (ck on False(vi_...)) *)
|
||||
let ck_0 = Con(ck,cfalse,id) in
|
||||
let acc_loc,acc_eq,t0 =
|
||||
clocked_tree
|
||||
(acc_loc,acc_eq)
|
||||
(id::acc_var)
|
||||
(suffix ^ "_0")
|
||||
v_list ck_0 in
|
||||
(* Build right son (ck on True(vi_...))*)
|
||||
let ck_1 = Con(ck,ctrue,id) in
|
||||
let acc_loc,acc_eq,t1 =
|
||||
clocked_tree
|
||||
(acc_loc,acc_eq)
|
||||
(id::acc_var)
|
||||
(suffix ^ "_1")
|
||||
v_list ck_1 in
|
||||
acc_loc,acc_eq,VNode(id,t0,t1)
|
||||
end
|
||||
in
|
||||
|
||||
let acc_loc,acc_eq,t =
|
||||
clocked_tree (acc_loc,acc_eq) [] "" v_list var_from.v_clock in
|
||||
|
||||
(acc_vd,acc_loc,acc_eq,v_list,t)
|
||||
|
||||
let translate_var_dec (acc_vd,acc_loc,acc_eq,env) ({v_type = ty} as v) =
|
||||
match ty with
|
||||
| Tprod _ | Tarray _ -> v::acc_vd, acc_loc, acc_eq, env
|
||||
| Tid(tname) ->
|
||||
begin
|
||||
match tname with
|
||||
| { qual = "Pervasives"; name = ("bool" | "int" | "float") } ->
|
||||
v::acc_vd, acc_loc, acc_eq, env
|
||||
| _ ->
|
||||
begin
|
||||
try
|
||||
begin
|
||||
match (get_enum tname) with
|
||||
| Type _ -> v::acc_vd, acc_loc, acc_eq ,env
|
||||
| Enum(info) ->
|
||||
let (acc_vd,acc_loc,acc_eq,vl,t) =
|
||||
var_dec_list
|
||||
(acc_vd,acc_loc,acc_eq)
|
||||
v info.ty_nb_var in
|
||||
let env =
|
||||
Env.add
|
||||
v.v_ident
|
||||
{ var_enum = info;
|
||||
var_list = vl;
|
||||
clocked_var = t }
|
||||
env in
|
||||
acc_vd, acc_loc, acc_eq, env
|
||||
end
|
||||
with Not_found -> v::acc_vd, acc_loc, acc_eq, env
|
||||
end
|
||||
end
|
||||
|
||||
let translate_var_dec_list env vlist =
|
||||
List.fold_left translate_var_dec ([],[],[],env) vlist
|
||||
|
||||
let translate_contract env contract =
|
||||
match contract with
|
||||
| None -> None, env
|
||||
| Some { c_local = v;
|
||||
c_eq = eq_list;
|
||||
c_assume = e_a;
|
||||
c_enforce = e_g;
|
||||
c_controllables = cl } ->
|
||||
let cl, cl_loc, cl_eq, env = translate_var_dec_list env cl in
|
||||
let v, v', v_eq, env' = translate_var_dec_list env v in
|
||||
let context = translate_eqs env' eq_list in
|
||||
let context, e_a = translate env' context e_a in
|
||||
let context, e_g = translate env' context e_g in
|
||||
let (d_list,eq_list) = context in
|
||||
Some { c_local = v@v'@cl_loc@d_list;
|
||||
c_eq = eq_list@v_eq@cl_eq;
|
||||
c_assume = e_a;
|
||||
c_enforce = e_g;
|
||||
c_controllables = cl },
|
||||
env
|
||||
|
||||
let node ({ n_local = locals;
|
||||
n_input = inputs;
|
||||
n_output = outputs;
|
||||
n_contract = contract;
|
||||
n_equs = eq_list } as n) =
|
||||
let inputs,in_loc,in_eq,env = translate_var_dec_list Env.empty inputs in
|
||||
let outputs,out_loc,out_eq,env = translate_var_dec_list env outputs in
|
||||
let contract, env = translate_contract env contract in
|
||||
let locals,locals',loc_eq,env = translate_var_dec_list env locals in
|
||||
let (d_list,eq_list) = translate_eqs env eq_list in
|
||||
{ n with
|
||||
n_local = locals@locals'@in_loc@out_loc@d_list;
|
||||
n_input = List.rev inputs;
|
||||
n_output = List.rev outputs;
|
||||
n_contract = contract;
|
||||
n_equs = eq_list@loc_eq@in_eq@out_eq }
|
||||
|
||||
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 }
|
||||
34
compiler/minils/transformations/boolean.mli
Normal file
34
compiler/minils/transformations/boolean.mli
Normal file
|
|
@ -0,0 +1,34 @@
|
|||
(****************************************************)
|
||||
(* *)
|
||||
(* Heptagon/BZR *)
|
||||
(* *)
|
||||
(* Author : Gwenaël Delaval *)
|
||||
(* Organization : INRIA Rennes, VerTeCs *)
|
||||
(* *)
|
||||
(****************************************************)
|
||||
|
||||
(*
|
||||
Translate enumerated types (state variables) into boolean
|
||||
|
||||
type t = A | B | C | D
|
||||
|
||||
A --> 00
|
||||
B --> 01
|
||||
C --> 10
|
||||
D --> 11
|
||||
|
||||
x : t --> x1,x2 : bool
|
||||
|
||||
(e when A(x))
|
||||
-->
|
||||
(e when False(x1)) when False(x2)
|
||||
|
||||
merge x (A -> e0) (B -> e1) (C -> e2) (D -> e3)
|
||||
-->
|
||||
merge x1 (False -> merge x2 (False -> e0) (True -> e1))
|
||||
(True -> merge x2 (False -> e2) (True -> e3))
|
||||
*)
|
||||
|
||||
(* $Id: boolean.mli 74 2009-03-11 10:21:25Z delaval $ *)
|
||||
|
||||
val program : Minils.program -> Minils.program
|
||||
|
|
@ -85,6 +85,10 @@ let add_inlined_node s = inline := s :: !inline
|
|||
|
||||
let flatten = ref false
|
||||
|
||||
let boolean = ref false
|
||||
|
||||
let deadcode = ref false
|
||||
|
||||
let tomato = ref false
|
||||
|
||||
let tomato_nodes : qualname list ref = ref []
|
||||
|
|
@ -117,6 +121,8 @@ and doc_full_name = "\t\t\tPrint full variable name information"
|
|||
and doc_target_path =
|
||||
"<path>\tGenerated files will be placed in <path>\n\t\t\t(the directory is"
|
||||
^ " cleaned)"
|
||||
and doc_boolean = "\t\tTranslate enumerated values towards boolean vectors"
|
||||
and doc_deadcode = "\t\tDeadcode removal"
|
||||
and doc_nocaus = "\t\tDisable causality analysis"
|
||||
and doc_noinit = "\t\tDisable initialization analysis"
|
||||
and doc_assert = "<node>\t\tInsert run-time assertions for boolean node <node>"
|
||||
|
|
|
|||
Loading…
Reference in a new issue