From 4e267d82c6caeb0814061d7c94ec84fdfc963416 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Gwena=EBl=20Delaval?= Date: Thu, 10 Mar 2011 23:00:18 +0100 Subject: [PATCH 01/12] Boolean transformation pass (translate every enumeration type to boolean tuples) --- compiler/main/heptc.ml | 2 + compiler/minils/main/mls_compiler.ml | 5 + compiler/minils/transformations/boolean.ml | 738 ++++++++++++++++++ compiler/minils/transformations/boolean.mli | 34 + compiler/utilities/global/compiler_options.ml | 6 + 5 files changed, 785 insertions(+) create mode 100644 compiler/minils/transformations/boolean.ml create mode 100644 compiler/minils/transformations/boolean.mli diff --git a/compiler/main/heptc.ml b/compiler/main/heptc.ml index 1cf583c..ac7edfb 100644 --- a/compiler/main/heptc.ml +++ b/compiler/main/heptc.ml @@ -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, ""; diff --git a/compiler/minils/main/mls_compiler.ml b/compiler/minils/main/mls_compiler.ml index 8a42098..8c1d802 100644 --- a/compiler/minils/main/mls_compiler.ml +++ b/compiler/minils/main/mls_compiler.ml @@ -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 diff --git a/compiler/minils/transformations/boolean.ml b/compiler/minils/transformations/boolean.ml new file mode 100644 index 0000000..eba7fe2 --- /dev/null +++ b/compiler/minils/transformations/boolean.ml @@ -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 } diff --git a/compiler/minils/transformations/boolean.mli b/compiler/minils/transformations/boolean.mli new file mode 100644 index 0000000..4b58411 --- /dev/null +++ b/compiler/minils/transformations/boolean.mli @@ -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 diff --git a/compiler/utilities/global/compiler_options.ml b/compiler/utilities/global/compiler_options.ml index 516d448..f1b3b72 100644 --- a/compiler/utilities/global/compiler_options.ml +++ b/compiler/utilities/global/compiler_options.ml @@ -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 = "\tGenerated files will be placed in \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 = "\t\tInsert run-time assertions for boolean node " From eb164f426805e1f36a0f86044062a6fbfa29bcf0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Gwena=EBl=20Delaval?= Date: Thu, 10 Mar 2011 23:28:44 +0100 Subject: [PATCH 02/12] More complete check script Added options to check scrit: test of boolean pass, deadcode, tomato added caml compilation test --- test/check | 121 ++++++++++++++++++++++++++++++++++++++++++++++------- 1 file changed, 105 insertions(+), 16 deletions(-) diff --git a/test/check b/test/check index af5c853..c02a9ee 100755 --- a/test/check +++ b/test/check @@ -21,8 +21,12 @@ CC="gcc -std=c99" # par defaut : pas de test de generation de code +caml=0 java=0 +lustre=0 c=0 +minils=0 +vhdl=0 score=0 max=0 @@ -93,7 +97,8 @@ launch_check () { done echo echo "Tests goods" - for f in ../good/*.ept ../image_filters/*.ept; do + pushd good > /dev/null + for f in *.ept; do echec=0 if [ $verbose = 0 ]; then echo -n "." @@ -114,24 +119,32 @@ launch_check () { fi fi # Compil. java ? - #if [[ ($echec == 0) && ($java == 1) ]]; then - # pushd "${base_f}_java" > /dev/null - # for java_file in *.java ; do - # if $JAVAC -warn:-unused -sourcepath .:..:../t1 ${java_file} > /dev/null - # then - # echec=0 - # else - # echec=3 - # fi - # done - # popd > /dev/null - #fi + if [[ ($echec == 0) && ($java == 1) ]]; then + pushd "${base_f}" > /dev/null + for java_file in *.java ; do + if $JAVAC -warn:-unused -sourcepath .:..:../t1 ${java_file} > /dev/null + then + echec=0 + else + echec=3 + fi + done + popd > /dev/null + fi + # Compil. caml ? + if [[ ($echec == 0) && ($caml == 1) ]]; then + if $CAMLC -c ${base_f}.ml > /dev/null; then + echec=0 + else + echec=4 + fi + fi # Compil. c ? if [[ ($echec == 0) && ($c == 1) ]]; then pushd ${base_f}_c >/dev/null for cf in *.c; do - if $CC -c $cf >/dev/null 2>&1; then - echec=0 + if $CC -I ../t1_c -c $cf >/dev/null 2>&1; then + echec=$echec else echec=5 fi @@ -160,6 +173,18 @@ launch_check () { fi popd >/dev/null fi + # Compil. VHDL ? + if [[ ($echec == 0) && ($vhdl == 1) ]]; then + pushd ${base_f}_vhdl > /dev/null + for vhdl_file in *.vhd; do + if $VHDLC -a ${vhdl_file} && $VHDLC -e ${vhdl_file} > /dev/null 2>&1 + then + echec=${echec} + else + echec=8 + fi + done + fi if [[ $echec == 0 ]]; then score=`expr $score + 1`; @@ -169,8 +194,12 @@ launch_check () { case $echec in 1 ) echo "Compilation failed.";; + 2 ) + echo "Compilation to Minils failed.";; 3 ) - echo "Java compilation failed.";; + echo "Compilation to Java failed.";; + 4 ) + echo "Compilation to Caml failed.";; 5 ) echo "C compilation failed.";; 6 ) @@ -180,6 +209,7 @@ launch_check () { esac fi done + popd > /dev/null echo percent=`expr 100 \* $score / $max`; @@ -200,6 +230,16 @@ activate_java () { coption="$coption -target java" } +activate_caml () { + caml=1 + coption="$coption -target caml" +} + +activate_vhdl () { + vhdl=1 + coption="$coption -target vhdl" +} + activate_c () { c=1 coption="$coption -target c" @@ -210,6 +250,26 @@ activate_all () { activate_c } +activate_tomato () { + coption="$coption -tomato" +} + +activate_cse () { + coption="$coption -cse" +} + +activate_inter () { + coption="$coption -inter" +} + +activate_boolean () { + coption="$coption -bool" +} + +activate_deadcode () { + coption="$coption -deadcode" +} + # -1, -2, -3, -v1, -v2, -v3 kept for backward compatibility # (to be suppressed) while [ $# -gt 0 ]; do @@ -229,14 +289,43 @@ while [ $# -gt 0 ]; do "-c" ) activate_c shift;; + "-caml" ) + activate_caml + shift;; + "-vhdl" ) + activate_vhdl + shift;; "-mls" ) activate_minils shift;; + "-tomato" ) + activate_tomato + shift;; + "-cse" ) + activate_cse + shift;; + "-inter" ) + activate_inter + shift;; + "-bool" ) + activate_boolean + shift;; + "-deadcode" ) + activate_deadcode + shift;; "-h" ) echo "usage : $0 " echo "options : " echo "-clean : clean build dir" echo "-java : test of code generation (java code)" + echo "-caml : test of code generation (caml code)" + echo "-lustre : test of code generation (lustre code)" + echo "-vhdl : test of code generation (vhdl)" + echo "-bool : test of boolean translation" + echo "-deadcode : test of deadcode removal" + echo "-inter : test of intermediate equations removal" + echo "-tomato : test of automata minimization" + echo "-cse : test of common sub-expression elimination" echo "-c : test of code generation (c code)" echo "-all : test all" echo "-v : verbose" From 0f6ddb739bb7eeb27c5d06853fc18b1ba4548462 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Gwena=EBl=20Delaval?= Date: Fri, 11 Mar 2011 14:47:13 +0100 Subject: [PATCH 03/12] Correction of Boolean pass Corrections to handle modifications on AST (fresh/gen_fresh on idents, Tunit type, e_base_ck = Cbase everywhere) --- compiler/minils/transformations/boolean.ml | 22 ++++++++++++++++++++-- 1 file changed, 20 insertions(+), 2 deletions(-) diff --git a/compiler/minils/transformations/boolean.ml b/compiler/minils/transformations/boolean.ml index eba7fe2..2a4e5b7 100644 --- a/compiler/minils/transformations/boolean.ml +++ b/compiler/minils/transformations/boolean.ml @@ -49,6 +49,8 @@ open Types open Clocks open Minils +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)) @@ -238,6 +240,7 @@ let translate_ty ty = end | Tprod(ty_list) -> Tprod(List.map trans ty_list) | Tarray(ty,se) -> Tarray(trans ty,se) + | Tunit -> Tunit in trans ty @@ -336,12 +339,14 @@ let rec when_ck desc ty ck = match ck with | Cbase | Cvar _ -> { e_desc = desc; + e_base_ck = Cbase; 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_base_ck = Cbase; e_ck = ck; e_ty = ty; e_loc = no_location } @@ -384,6 +389,7 @@ let rec base_value ck ty = let e_list = aux [] n in { e_desc = mk_tuple e_list; e_ty = Tprod(List.map (fun _ -> ty_bool) e_list); + e_base_ck = Cbase; e_ck = ck; e_loc = no_location } end @@ -394,6 +400,7 @@ let rec base_value ck ty = 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_base_ck = Cbase; e_ck = ck; e_loc = no_location; } @@ -401,6 +408,14 @@ let rec base_value ck ty = 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_base_ck = Cbase; + e_ck = ck; + e_loc = no_location; + } + | Tunit -> + { e_desc = Eapp (mk_app Etuple, [], None); + e_ty = Tunit; + e_base_ck = Cbase; e_ck = ck; e_loc = no_location; } @@ -417,6 +432,7 @@ let rec merge_tree ck ty e_map btree vtree = in { e_desc = Emerge(v,[(ctrue,e1);(cfalse,e2)]); e_ty = ty; + e_base_ck = Cbase; e_ck = ck; e_loc = no_location } | Tree (_,_), Vempty -> failwith("merge_tree: non-coherent trees") @@ -558,6 +574,7 @@ let var_dec_list (acc_vd,acc_loc,acc_eq) var_from n = match ckvar_list,ck with | [], _ -> { e_desc = Evar(var); + e_base_ck = Cbase; e_ck = ck; e_ty = ty_bool; e_loc = no_location } @@ -565,6 +582,7 @@ let var_dec_list (acc_vd,acc_loc,acc_eq) var_from n = (* assert v = _ckvar *) let e = when_ck l ck' var in { e_desc = Ewhen(e,c,v); + e_base_ck = Cbase; e_ck = ck; e_ty = ty_bool; e_loc = no_location } @@ -622,7 +640,7 @@ let var_dec_list (acc_vd,acc_loc,acc_eq) var_from n = acc_loc,acc_eq,VNode(v1,t0,t1) | vi::v_list, _ -> (* Build name vi_(0|1)* *) - let v = (sourcename vi) ^ suffix in + let v = (name vi) ^ suffix in (* Build ident from this name *) let id = fresh v in let acc_loc = { v_ident = id; @@ -661,7 +679,7 @@ let var_dec_list (acc_vd,acc_loc,acc_eq) var_from n = 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 + | Tprod _ | Tarray _ | Tunit -> v::acc_vd, acc_loc, acc_eq, env | Tid(tname) -> begin match tname with From 70e2ce08a268bb94a5b48ba28bff436bba3aa3de Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Gwena=EBl=20Delaval?= Date: Fri, 11 Mar 2011 14:49:47 +0100 Subject: [PATCH 04/12] Correction of check script --- test/check | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/test/check b/test/check index c02a9ee..1e0c4bb 100755 --- a/test/check +++ b/test/check @@ -97,8 +97,7 @@ launch_check () { done echo echo "Tests goods" - pushd good > /dev/null - for f in *.ept; do + for f in ../good/*.ept; do echec=0 if [ $verbose = 0 ]; then echo -n "." @@ -209,7 +208,6 @@ launch_check () { esac fi done - popd > /dev/null echo percent=`expr 100 \* $score / $max`; From ac9715ad9035a7d6b4fddfe5d4cbd2f7eeb6ba5a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Gwena=C3=ABl?= Date: Tue, 15 Mar 2011 15:18:32 +0100 Subject: [PATCH 05/12] Correction of Boolean pass Correction of Boolean pass: correct translation of variable declarations, including full clock translation (in two passes for variable declarations: one to build the env, one for clock translation). --- compiler/minils/transformations/boolean.ml | 36 ++++++++++++++-------- 1 file changed, 24 insertions(+), 12 deletions(-) diff --git a/compiler/minils/transformations/boolean.ml b/compiler/minils/transformations/boolean.ml index 2a4e5b7..33506fc 100644 --- a/compiler/minils/transformations/boolean.ml +++ b/compiler/minils/transformations/boolean.ml @@ -265,7 +265,6 @@ let rec translate_ck env ck = 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 @@ -677,7 +676,7 @@ let var_dec_list (acc_vd,acc_loc,acc_eq) var_from n = (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) = +let buildenv_var_dec (acc_vd,acc_loc,acc_eq,env) ({v_type = ty} as v) = match ty with | Tprod _ | Tarray _ | Tunit -> v::acc_vd, acc_loc, acc_eq, env | Tid(tname) -> @@ -709,8 +708,14 @@ let translate_var_dec (acc_vd,acc_loc,acc_eq,env) ({v_type = ty} as v) = end end +let buildenv_var_dec_list env vlist = + List.fold_left buildenv_var_dec ([],[],[],env) vlist + +let translate_var_dec env ({ v_clock = ck } as v) = + { v with v_clock = translate_ck env ck } + let translate_var_dec_list env vlist = - List.fold_left translate_var_dec ([],[],[],env) vlist + List.map (translate_var_dec env) vlist let translate_contract env contract = match contract with @@ -720,14 +725,18 @@ let translate_contract env contract = 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 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 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; + Some { c_local = v@d_list; + c_eq = eq_list; c_assume = e_a; c_enforce = e_g; c_controllables = cl }, @@ -738,17 +747,20 @@ let node ({ n_local = locals; 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 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 = translate_var_dec_list env locals 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 { n with - n_local = locals@locals'@in_loc@out_loc@d_list; + n_local = locals@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 } + n_equs = eq_list } let program ({ p_types = pt_list; p_nodes = n_list } as p) = let pt_list = build_enum_env pt_list in From da37fd8e589979bd46a1041a81bd7f7aec9e203f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Gwena=C3=ABl=20Delaval?= Date: Wed, 16 Mar 2011 23:25:04 +0100 Subject: [PATCH 06/12] Sigali code generation Sigali AST and Sigalimain module for sigali code generation from normalized and Boolean minils program --- compiler/minils/sigali/sigali.ml | 435 +++++++++++++++++ compiler/minils/sigali/sigali.mli | 103 ++++ compiler/minils/sigali/sigalimain.ml | 664 ++++++++++++++++++++++++++ compiler/minils/sigali/sigalimain.mli | 14 + 4 files changed, 1216 insertions(+) create mode 100644 compiler/minils/sigali/sigali.ml create mode 100644 compiler/minils/sigali/sigali.mli create mode 100644 compiler/minils/sigali/sigalimain.ml create mode 100644 compiler/minils/sigali/sigalimain.mli diff --git a/compiler/minils/sigali/sigali.ml b/compiler/minils/sigali/sigali.ml new file mode 100644 index 0000000..5599058 --- /dev/null +++ b/compiler/minils/sigali/sigali.ml @@ -0,0 +1,435 @@ +(****************************************************) +(* *) +(* Sigali Library *) +(* *) +(* Author : Gwena�l Delaval *) +(* Organization : INRIA Rennes, VerTeCs *) +(* *) +(****************************************************) + +(* $Id: sigali.ml 2416 2011-01-13 17:00:15Z delaval $ *) + +(* Sigali representation and output *) + +type name = string + +type var = name + +type const = Cfalse | Cabsent | Ctrue | Cint of int + +type exp = + | Sconst of const + | Svar of name + | Swhen of exp * exp (* e1 when e2 *) + | Sdefault of exp * exp (* e1 default e2 *) + | Sequal of exp * exp (* e1 = e2 *) + | Ssquare of exp (* e^2 *) + | Snot of exp (* not e *) + | Sand of exp * exp (* e1 and e2 *) + | Sor of exp * exp (* e1 or e2 *) + | Sprim of name * exp list (* f(e1,...,en) *) + | Slist of exp list (* [e1,...,en] *) + | Splus of exp * exp (* e1 + e2 *) + | Sminus of exp * exp (* e1 - e2 *) + | Sprod of exp * exp (* e1 * e2 *) + +type statement = { (* name : definition *) + stmt_name : name; + stmt_def : exp; +} + +type objective = + | Security of exp + | Reachability of exp + | Attractivity of exp + +type processus = { + proc_dep : name list; + proc_name : name; + proc_inputs : var list; + proc_uncont_inputs : var list; + proc_outputs : var list; + proc_controllables : var list; + proc_states : var list; + proc_init : const list; + proc_constraints : exp list; + proc_body : statement list; + proc_objectives : objective list; +} + +type program = processus list + +let concat e1 e2 = + Sprim("concat",[e1;e2]) + +let evolutions = "evolutions" +let initialisations = "initialisations" +let constraints = "constraints" + +let extend var e = + { stmt_name = var ; + stmt_def = concat (Svar(var)) e } + +let subst e1 e2 e3 = + Sprim ("subst",[e1;e2;e3]) + +let l_subst e1 e2 e3 = + Sprim ("l_subst",[e1;e2;e3]) + +let evolution p = + Sprim ("evolution",[p]) + +let initial p = + Sprim ("initial",[p]) + +let pconstraint p = + Sprim ("constraint",[p]) + +let ifthenelse e1 e2 e3 = + Sdefault(Swhen(e2,e1),e3) + +let (&~) e1 e2 = + match e1,e2 with + | Sconst(Cfalse), _ + | _, Sconst(Cfalse) -> Sconst(Cfalse) + | Sconst(Ctrue), e + | e, Sconst(Ctrue) -> e + | _ -> Sand(e1,e2) + +let (|~) e1 e2 = + match e1,e2 with + | Sconst(Ctrue), _ + | _, Sconst(Ctrue) -> Sconst(Ctrue) + | Sconst(Cfalse), e + | e, Sconst(Cfalse) -> e + | _ -> Sor(e1,e2) + +let (=>~) e1 e2 = + match e1,e2 with + | Sconst(Ctrue), e -> e + | _, Sconst(Ctrue) + | Sconst(Cfalse), _ -> Sconst(Ctrue) + | _ -> Sor(Snot(e1),e2) + +let a_const e = + Sprim ("a_const",[e]) + +let a_var e e1 e2 e3 = + Sprim ("a_var", [e;e1;e2;e3]) + +let a_part e e1 e2 e3 = + Sprim ("a_part", [e;e1;e2;e3]) + +let a_inf e1 e2 = + Sprim ("a_inf", [e1;e2]) + +let a_sup e1 e2 = + Sprim ("a_sup", [e1;e2]) + +module Printer = + struct + open Format + + let rec print_list ff print sep l = + match l with + | [] -> () + | [x] -> print ff x + | x :: l -> + print ff x; + fprintf ff "%s@ " sep; + print_list ff print sep l + + let print_string ff s = + fprintf ff "%s" s + + let print_name ff n = + fprintf ff "%s" n + + let print_const ff c = + match c with + | Cfalse -> fprintf ff "-1" + | Ctrue -> fprintf ff "1" + | Cabsent -> fprintf ff "0" + | Cint(v) -> fprintf ff "%d" v + + let rec print_exp ff e = + match e with + | Sconst(c) -> print_const ff c + | Svar(v) -> print_name ff v + | Swhen(e1,e2) -> + fprintf ff "(%a@ when %a)" + print_exp e1 + print_exp e2 + | Sdefault(e1,e2) -> + fprintf ff "(%a@ default %a)" + print_exp e1 + print_exp e2 + | Sequal(e1,e2) -> + fprintf ff "(%a@ = %a)" + print_exp e1 + print_exp e2 + | Ssquare(e) -> + fprintf ff "(%a^2)" + print_exp e + | Snot(e) -> + fprintf ff "(not %a)" + print_exp e + | Sand(e1,e2) -> + fprintf ff "(%a@ and %a)" + print_exp e1 + print_exp e2 + | Sor(e1,e2) -> + fprintf ff "(%a@ or %a)" + print_exp e1 + print_exp e2 + | Sprim(f,e_l) -> + fprintf ff "%s(@[" f; + print_list ff print_exp "," e_l; + fprintf ff "@])" + | Slist(e_l) -> + fprintf ff "[@["; + print_list ff print_exp "," e_l; + fprintf ff "]@]" + | Splus(e1,e2) -> + fprintf ff "(%a@ + %a)" + print_exp e1 + print_exp e2 + | Sminus(e1,e2) -> + fprintf ff "(%a@ - %a)" + print_exp e1 + print_exp e2 + | Sprod(e1,e2) -> + fprintf ff "(%a@ * %a)" + print_exp e1 + print_exp e2 + + let print_statement ff { stmt_name = name; stmt_def = e } = + fprintf ff "@[%a : %a;@]" + print_name name + print_exp e + + let print_statements ff stmt_l = + fprintf ff "@["; + print_list ff print_statement "" stmt_l; + fprintf ff "@]@ " + + let print_objective name ff obj = + match obj with + | Security(e) -> + fprintf ff "%s : S_Security(%s,B_True(%s,%a));" + name name name + print_exp e + | Reachability(e) -> + fprintf ff "%s : S_Reachable(%s,B_True(%s,%a));" + name name name + print_exp e + | Attractivity(e) -> + fprintf ff "%s : S_Attractivity(%s,B_True(%s,%a));" + name name name + print_exp e + + let print_verification name ff obj = + match obj with + | Security(e) -> + fprintf ff "verif_result : verif_result andb notb Reachable(%s,B_False(%s,%a));" + name name + print_exp e + | Reachability(e) -> + fprintf ff "verif_result : verif_result andb Reachable(%s,B_True(%s,%a));" + name name + print_exp e + | Attractivity(_) -> failwith("Attractivity verification not allowed") + + let sigali_head = " +set_reorder(2); + +read(\"Property.lib\"); +read(\"Synthesis.lib\"); +read(\"Verif_Determ.lib\"); +read(\"Simul.lib\"); +read(\"Synthesis_Partial_order.lib\"); +read(\"Orbite.lib\"); +" + + let sigali_foot = "" + + let print_processus dir ({ proc_dep = dep_list; + proc_name = name; + proc_inputs = inputs; + proc_uncont_inputs = uncont_inputs; + proc_outputs = outputs; + proc_controllables = controllables; + proc_states = states; + proc_constraints = constraints; + proc_body = body; + proc_objectives = objectives; + }) = + let sigc = open_out (dir ^ "/" ^ name ^ ".z3z") in + let ff = formatter_of_out_channel sigc in + + Compiler_utils.print_header_info ff "%" "%"; + fprintf ff "%s" sigali_head; + let n = List.length states in + + (* declare dummy variables d1...dn *) + fprintf ff "@[declare(@[d1"; + for i = 2 to n do + fprintf ff ",@ d%d" i; + done; + fprintf ff "@]);@]@\n@\n"; + + fprintf ff "@["; + + (* dependencies *) + fprintf ff "%% -- dependencies --- %%@\n@\n"; + + List.iter + (fun dep_name -> + fprintf ff "read(\"%s.z3z\");@\n" dep_name) + dep_list; + + (* head comment *) + fprintf ff "%% ---------- process %s ---------- %%@\n@\n" name; + + (* variables declaration *) + fprintf ff "declare(@["; + print_list ff print_name "," (inputs@states); + fprintf ff "@]);@,"; + + (* inputs decl. *) + fprintf ff "conditions : [@["; + print_list ff print_name "," inputs; + fprintf ff "@]];@,"; + + (* states decl. *) + fprintf ff "states : [@["; + if states = [] then + (* dummy state var to avoid sigali segfault *) + fprintf ff "d1" + else + print_list ff print_name "," states; + fprintf ff "@]];@,"; + + (* controllables : *) + fprintf ff "controllables : [@["; + print_list ff print_name "," controllables; + fprintf ff "@]];@,"; + + (* init evolutions, initialisations *) + if states = [] then + fprintf ff "evolutions : [d1];@," + else + fprintf ff "evolutions : [];@,"; + fprintf ff "initialisations : [];@,"; + + (* body statements *) + print_statements ff body; + + (* constraints *) + fprintf ff "constraints : [@["; + print_list ff print_exp "," constraints; + fprintf ff "@]];@,"; + + (* outputs : comment *) + fprintf ff "@,%% --- outputs : [@["; + print_list ff print_name "," outputs; + fprintf ff "@]] --- %%@,"; + + (* process declaration *) + fprintf ff + ("%s : processus(" ^^ + "@[conditions," ^^ + "@ states," ^^ + "@ evolutions," ^^ + "@ initialisations," ^^ + "@ [gen(constraints)]," ^^ + "@ controllables@]);@,") + name; + + begin + match controllables with + [] -> + begin + (* No controllable variables: verification *) + + (* Initialisation of verification result *) + fprintf ff "verif_result : True;@,"; + + (* Verification of properties (update verif_result) *) + fprintf ff "@["; + print_list ff (print_verification name) "" objectives; + fprintf ff "@]@,"; + + (* Print result *) + fprintf ff "if verif_result then@,"; + fprintf ff " print(\"%s: property true.\")@," name; + fprintf ff "else@,"; + fprintf ff " print(\"%s: property false.\");@," name; + end + + | _::_ -> + begin + (* At least one controllable variable: synthesis *) + + (* Store the initial state for further check *) + fprintf ff "%s_init : initial(%s);@," name name; + + (* Controller synthesis *) + fprintf ff "@["; + print_list ff (print_objective name) "" objectives; + fprintf ff "@]@,"; + + (* Check that synthesis succeeded : initial state not modified *) + fprintf ff "dcs_result : equal(%s_init,initial(%s));@," name name; + + (* Print result *) + fprintf ff "if dcs_result then@,"; + fprintf ff " print(\"%s: synthesis succeeded.\")@," name; + fprintf ff "else@,"; + fprintf ff " print(\"%s: synthesis failed.\");@," name; + + fprintf ff "@\nif dcs_result then@,"; + (* Controller output *) + (* fprintf ff " simul(%s,\"%s.res\",\"%s.sim\")@\n" name name name; *) + fprintf ff " print(\"Triangulation and controller generation...\")@\n"; + fprintf ff "else@,"; + fprintf ff " quit(1);@,"; + + (* Triangulation *) + (* phantoms : *) + let phantom_vars = List.map (fun n -> "p_" ^ n) controllables in + (* phantom variables declaration *) + fprintf ff "declare(@["; + print_list ff print_name "," phantom_vars; + fprintf ff "@]);@,"; + fprintf ff "phantom_vars : [@["; + print_list ff print_name "," phantom_vars; + fprintf ff "@]];@,"; + fprintf ff "%s_triang : Triang(constraint(%s),controllables,phantom_vars);@," name name; + + (* controller vars *) + fprintf ff "controller_inputs : [@["; + print_list ff print_name "," (uncont_inputs + @states + @(List.map + (fun n -> "p_" ^ n) + controllables)); + fprintf ff "@]];@,"; + + (* Controller generation *) + fprintf ff "heptagon_controller(\"%s_controller.ept\",\"%s\",controller_inputs,controllables,%s_triang);@," name name name; + end + end; + + (* Footer and close file *) + fprintf ff "@]@."; + fprintf ff "%s" sigali_foot; + fprintf ff "@?"; + + close_out sigc + + + let print dir p_l = + List.iter (print_processus dir) p_l + end + diff --git a/compiler/minils/sigali/sigali.mli b/compiler/minils/sigali/sigali.mli new file mode 100644 index 0000000..8293878 --- /dev/null +++ b/compiler/minils/sigali/sigali.mli @@ -0,0 +1,103 @@ +(****************************************************) +(* *) +(* Sigali Library *) +(* *) +(* Author : Gwenaël Delaval *) +(* Organization : INRIA Rennes, VerTeCs *) +(* *) +(****************************************************) + +(* $Id: sigali.mli 2324 2010-12-05 10:22:36Z delaval $ *) + +(* Sigali representation and output *) + +type name = string + +type var = name + +type const = Cfalse | Cabsent | Ctrue | Cint of int + +type exp = + | Sconst of const + | Svar of name + | Swhen of exp * exp (* e1 when e2 *) + | Sdefault of exp * exp (* e1 default e2 *) + | Sequal of exp * exp (* e1 = e2 *) + | Ssquare of exp (* e^2 *) + | Snot of exp (* not e *) + | Sand of exp * exp (* e1 and e2 *) + | Sor of exp * exp (* e1 or e2 *) + | Sprim of name * exp list (* f(e1,...,en) *) + | Slist of exp list (* [e1,...,en] *) + | Splus of exp * exp (* e1 + e2 *) + | Sminus of exp * exp (* e1 - e2 *) + | Sprod of exp * exp (* e1 * e2 *) + +type statement = { (* name : definition *) + stmt_name : name; + stmt_def : exp; +} + +type objective = + | Security of exp + | Reachability of exp + | Attractivity of exp + +type processus = { + proc_dep : name list; + proc_name : name; + proc_inputs : var list; + proc_uncont_inputs : var list; + proc_outputs : var list; + proc_controllables : var list; + proc_states : var list; + proc_init : const list; + proc_constraints : exp list; + proc_body : statement list; + proc_objectives : objective list; +} + +type program = processus list + +val concat : exp -> exp -> exp + +val evolutions : string + +val initialisations : string + +val constraints : string + +val extend : name -> exp -> statement + +val subst : exp -> exp -> exp -> exp + +val l_subst : exp -> exp -> exp -> exp + +val evolution : exp -> exp + +val initial : exp -> exp + +val pconstraint : exp -> exp + +val ifthenelse : exp -> exp -> exp -> exp + +val ( &~ ) : exp -> exp -> exp + +val ( |~ ) : exp -> exp -> exp + +val ( =>~ ) : exp -> exp -> exp + +val a_const : exp -> exp + +val a_var : exp -> exp -> exp -> exp -> exp + +val a_part : exp -> exp -> exp -> exp -> exp + +val a_inf : exp -> exp -> exp + +val a_sup : exp -> exp -> exp + +module Printer : + sig + val print : string -> processus list -> unit + end diff --git a/compiler/minils/sigali/sigalimain.ml b/compiler/minils/sigali/sigalimain.ml new file mode 100644 index 0000000..033dd55 --- /dev/null +++ b/compiler/minils/sigali/sigalimain.ml @@ -0,0 +1,664 @@ +(****************************************************) +(* *) +(* Heptagon/BZR *) +(* *) +(* Author : Gwenaël Delaval *) +(* Organization : INRIA Rennes, VerTeCs *) +(* *) +(****************************************************) + +(* Translation from the source language to Sigali polynomial systems *) + +(* $Id: dynamic_system.ml 2652 2011-03-11 16:26:17Z delaval $ *) + +open Misc +open Compiler_utils +open Names +open Idents +open Types +open Clocks +open Sigali + +type mtype = Tint | Tbool | Tother + +let actual_ty = function + | Tid({ qual = "Pervasives"; name = "bool"}) -> Tbool + | Tid({ qual = "Pervasives"; name = "int"}) -> Tint + | _ -> Tother + +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 dummy_prefix = "d" + +let translate_static_exp se = + match se.se_desc with + | Sint(v) -> Cint(v) + | Sfloat(_) -> failwith("Sigali: floats not implemented") + | Sbool(true) -> Ctrue + | Sbool(false) -> Cfalse + | _ -> failwith("Sigali: untranslatable constant") + + +let rec translate_pat = function + | Minils.Evarpat(x) -> [name x] + | Minils.Etuplepat(pat_list) -> + List.fold_right (fun pat acc -> (translate_pat pat) @ acc) pat_list [] + +let rec translate_ck pref e = function + | Cbase | Cvar { contents = Cindex _ } -> + e + | Cvar { contents = Clink ck } -> translate_ck pref e ck + | Con(ck,c,var) -> + let e = translate_ck pref e ck in + Swhen(e, + match (shortname c) with + "true" -> Svar(pref ^ (name var)) + | "false" -> Snot(Svar(pref ^ (name var))) + | _ -> assert false) + +(* [translate e = c] *) +let rec translate prefix ({ Minils.e_desc = desc; Minils.e_ty = ty } as e) = + match desc with + | Minils.Econst(v) -> + begin match (actual_ty ty) with + | Tbool -> Sconst(translate_static_exp v) + | Tint -> a_const (Sconst(translate_static_exp v)) + | Tother -> failwith("Sigali: untranslatable type") + end + | Minils.Evar(n) -> Svar(prefix ^ (name n)) + | Minils.Eapp (* pervasives binary or unary stateless operations *) + ({ Minils.a_op = Minils.Efun({qual="Pervasives";name=n})}, + e_list, _) -> + begin + match n, e_list with + | "not", [e] -> Snot(translate prefix e) + | "or", [e1;e2] -> Sor((translate prefix e1),(translate prefix e2)) + | "&", [e1;e2] -> Sand((translate prefix e1),(translate prefix e2)) + (* a_inf and a_sup : +1 to translate ideals to boolean + polynomials *) + | ("<="|"<"|">="|">"), [e1;e2] -> + let op,modv = + begin match n with + | "<=" -> a_inf,0 + | "<" -> a_inf,-1 + | ">=" -> a_sup,0 + | _ -> a_sup,1 + end in + let e1 = translate prefix e1 in + begin match e2.Minils.e_desc with + | Minils.Econst({se_desc = Sint(v)}) -> + let e = op e1 (Sconst(Cint(v+modv))) in + Splus(e,Sconst(Ctrue)) + | _ -> + let e2 = translate prefix e2 in + let e = op (Sminus(e1,e2)) (Sconst(Cint(modv))) in + Splus(e,Sconst(Ctrue)) + end + | "+", [e1;e2] -> Splus((translate prefix e1),(translate prefix e2)) + | "-", [e1;e2] -> Sminus((translate prefix e1),(translate prefix e2)) + | "*", [e1;e2] -> Sprod((translate prefix e1),(translate prefix e2)) + | ("=" + | "<>"),_ -> failwith("Sigali: '=' or '<>' not yet implemented") + | _ -> assert false + end + | Minils.Ewhen(e, c, var) when ((actual_ty e.Minils.e_ty) = Tbool) -> + let e = translate prefix e in + Swhen(e, + match (shortname c) with + "true" -> Svar(prefix ^ (name var)) + | "false" -> Snot(Svar(prefix ^ (name var))) + | _ -> assert false) + | Minils.Ewhen(e, _c, _var) -> + translate prefix e + | Minils.Emerge(ck,[(c1,e1);(_c2,e2)]) -> + let e1 = translate prefix e1 in + let e2 = translate prefix e2 in + let e1,e2 = + begin + match (shortname c1) with + "true" -> e1,e2 + | "false" -> e2,e1 + | _ -> assert false + end in + let var_ck = Svar(prefix ^ (name ck)) in + begin match (actual_ty e.Minils.e_ty) with + | Tbool -> Sdefault(Swhen(e1,var_ck),e2) + | Tint -> a_part var_ck (a_const (Sconst(Cint(0)))) e1 e2 + | Tother -> assert false + end + | Minils.Estruct(_) -> + failwith("Sigali: structures not implemented") + | Minils.Eiterator(_,_,_,_,_) -> + failwith("Sigali: iterators not implemented") + | Minils.Eapp({Minils.a_op = Minils.Enode(_)},_,_) -> + failwith("Sigali: node in expressions; programs should be normalized") + | Minils.Efby(_,_) -> + failwith("Sigali: fby in expressions; programs should be normalized") + | Minils.Eapp(_,_,_) -> failwith("Sigali: not supported application") + | Minils.Emerge(_, _) -> assert false + +let rec translate_eq env f + (acc_dep,acc_states,acc_init,acc_inputs,acc_ctrl,acc_cont,acc_eqs) + { Minils.eq_lhs = pat; Minils.eq_rhs = e } = + + let prefix = f ^ "_" in + + let prefixed n = prefix ^ n in + + let { Minils.e_desc = desc; Minils.e_ck = ck } = e in + match pat, desc with + | Minils.Evarpat(n), Minils.Efby(opt_c, e) -> + let sn = prefixed (name n) in + let sm = prefix ^ "mem_" ^ (name n) in +(* let acc_eqs = *) +(* (extend *) +(* constraints *) +(* (Slist[Sequal(Ssquare(Svar(sn)),Sconst(Ctrue))]))::acc_eqs in *) + let acc_eqs,acc_init = + match opt_c with + | None -> acc_eqs,Cfalse::acc_init + | Some(c) -> + let c = translate_static_exp c in + (extend + initialisations + (Slist[Sequal(Svar(sn),Sconst(c))]))::acc_eqs, + c::acc_init + in + let e_next = translate prefix e in + let e_next = translate_ck prefix e_next ck in + acc_dep, + sn::acc_states, + acc_init,acc_inputs,acc_ctrl,acc_cont, + (extend + evolutions + (Slist[Sdefault(e_next,Svar(sn))])) + (* TODO *) +(* ::{ stmt_name = sn; *) +(* stmt_def = translate_ck prefix (Svar(sm)) ck } *) + ::acc_eqs + | pat, Minils.Eapp({ Minils.a_op = Minils.Enode g_name; + Minils.a_id = Some a_id; + Minils.a_inlined = inlined }, e_list, None) -> + (* + g : n states (gq1,...,gqn), p inputs (gi1,...,gip), m outputs (go1,...,gom) + + case inlined : + var_g : [gq1,...,gqn,gi1,...,gip] + var_inst_g : [hq1,...,hqn,e1,...,en] + case non inlined : + add inputs go1',...,gom' + var_g : [gq1,...,gqn,gi1,...,gip,go1,...,gom] + var_inst_g : [hq1,...,hqn,e1,...,en,go1',...,gom'] + + declare(d1,...,dn) + + d : [d1,...,dn] + % q1 = if ck then d1 else hq1 % + q1 : d1 when ck default hq1 + ... + qn : dn when ck default hqn + + % P_inst = P[var_inst_g/var_g] % + evol_g : l_subst(evolution(g),var_g,var_inst_g); + evolutions : concat(evolutions,l_subst([q1,...,qn],[d1,...,dn],evol_g) + initialisations : concat(initialisations, [subst(initial(g),var_g,var_inst_g)]) + constraints : concat(constraints, [subst(constraint(g),var_g,var_inst_g)]) + + case inlined : + ho1 : subst(go1,var_g,var_inst_g) + ... + hom : subst(gom,var_g,var_inst_g) + case non inlined : + (nothing) + *) + let g_name = shortname g_name in + let (g_p,g_p_contract) = NamesEnv.find g_name env in + let g = if inlined then g_name else g_name ^ "_contract" in + (* add dependency *) + let acc_dep = g :: acc_dep in + let name_list = translate_pat pat in + let g_p = if inlined then g_p else g_p_contract in + (* var_g : [gq1,...,gqn,gi1,...,gip] *) + let var_g = "var_" ^ g in + let vars = + match inlined with + | true -> g_p.proc_states @ g_p.proc_inputs + | false -> g_p.proc_states @ g_p.proc_inputs @ g_p.proc_outputs in + let acc_eqs = + { stmt_name = var_g; + stmt_def = Slist(List.map (fun v -> Svar(v)) vars) }::acc_eqs in + (* var_inst_g : [hq1,...,hqn,e1,...,en] *) + let var_inst_g = "var_inst_" ^ g in + (* Coding contract states : S_n_id_s *) + (* id being the id of the application *) + (* n being the length of id *) + (* s being the name of the state*) + let a_id = (name a_id) in + let id_length = String.length a_id in + let s_prefix = "S_" ^ (string_of_int id_length) ^ "_" ^ a_id ^ "_" in + let new_states_list = + List.map + (fun g_state -> + (* Remove "g_" prefix *) + let l = String.length g in + let s = + String.sub + g_state (l+1) + ((String.length g_state)-(l+1)) in + prefixed (s_prefix ^ s)) + g_p.proc_states in + let e_states = List.map (fun hq -> Svar(hq)) new_states_list in + let e_list = List.map (translate prefix) e_list in + let e_outputs,acc_inputs = + match inlined with + | true -> [],acc_inputs + | false -> + let new_outputs = + List.map (fun name -> prefixed name) name_list in + (List.map (fun v -> Svar(v)) new_outputs),(acc_inputs@new_outputs) in + let vars_inst = e_states@e_list@e_outputs in + let acc_eqs = + { stmt_name = var_inst_g; + stmt_def = Slist(vars_inst); }::acc_eqs in + let acc_states = List.rev_append new_states_list acc_states in + let acc_init = List.rev_append g_p.proc_init acc_init in + (* declare(d1,...,dn) *) + let dummy_list = var_list dummy_prefix (List.length g_p.proc_states) in + (* d : [d1,...dn] *) + let acc_eqs = + {stmt_name = dummy_prefix; + stmt_def = Slist(List.map (fun di -> Svar(di)) dummy_list)}::acc_eqs in + (* qi = di when ck default hqi *) + let q_list = List.map (fun _ -> "q_" ^ (gen_symbol ())) g_p.proc_states in + let e_list = + List.map2 + (fun hq d -> + let e = Svar(d) in + let e = translate_ck (prefixed "") e ck in + Sdefault(e,Svar(hq))) + new_states_list dummy_list in + let acc_eqs = + List.fold_left2 + (fun acc_eqs q e -> {stmt_name = q; stmt_def = e}::acc_eqs) + acc_eqs q_list e_list in + (* evol_g : l_subst(evolution(g),var_g,var_inst_g); *) + let evol_g = "evol_" ^ g in + let acc_eqs = + {stmt_name = evol_g; + stmt_def = l_subst (evolution (Svar g)) (Svar var_g) (Svar var_inst_g)} + ::acc_eqs in + (* evolutions : concat(evolutions,l_subst([q1,...,qn],[d1,...,dn],evol_g) *) + let acc_eqs = + (extend evolutions (l_subst + (Slist (List.map (fun q -> Svar(q)) q_list)) + (Slist (List.map (fun d -> Svar(d)) dummy_list)) + + (Svar evol_g))) + ::acc_eqs in + (* initialisations : concat(initialisations, [subst(initial(g),var_g,var_inst_g)]) *) + let acc_eqs = + (extend initialisations (Slist[subst + (initial (Svar g)) + (Svar var_g) + (Svar var_inst_g)])) + :: acc_eqs in + (* constraints : concat(constraints, [subst(constraint(g),var_g,var_inst_g)]) *) + let acc_eqs = + (extend constraints (Slist[subst + (pconstraint (Svar g)) + (Svar var_g) + (Svar var_inst_g)])) + ::acc_eqs in + (* if inlined, hoi : subst(goi,var_g,var_inst_g) *) + let acc_eqs = + match inlined with + | true -> + List.fold_left2 + (fun acc_eqs o go -> + {stmt_name = prefixed o; + stmt_def = subst (Svar(go)) (Svar(var_g)) (Svar(var_inst_g))} + ::acc_eqs) + acc_eqs name_list g_p.proc_outputs + | false -> acc_eqs in + (* assume & guarantee *) + (* f_g_assume_x : subst(g_assume,var_g,var_inst_g) *) + (* f_g_guarantee_x : subst(g_guarantee,var_g,var_inst_g) *) + let var_assume = prefixed (g ^ "_assume_" ^ (gen_symbol ())) in + let var_guarantee = prefixed (g ^ "_guarantee_" ^ (gen_symbol ())) in + let acc_eqs = + {stmt_name = var_assume; + stmt_def = subst (Svar(g ^ "_assume")) (Svar(var_g)) (Svar(var_inst_g))} :: + {stmt_name = var_guarantee; + stmt_def = subst (Svar(g ^ "_guarantee")) (Svar(var_g)) (Svar(var_inst_g))} :: + acc_eqs in + let acc_cont = + (Svar(var_assume),Svar(var_guarantee)) :: acc_cont in + acc_dep,acc_states,acc_init, + acc_inputs,acc_ctrl,acc_cont,acc_eqs + | pat, Minils.Eapp({ Minils.a_op = Minils.Enode g_name; + Minils.a_id = Some a_id; + Minils.a_inlined = inlined }, e_list, Some r) -> + (* + g : n states (gq1,...,gqn), p inputs (gi1,...,gip), + n init states (gq1_0,...,gqn_0) + + case inlined : + var_g : [gq1,...,gqn,gi1,...,gip] + var_inst_g : [hq1,...,hqn,e1,...,en] + case non inlined : + add inputs go1',...,gom' + var_g : [gq1,...,gqn,gi1,...,gip,go1,...,gom] + var_inst_g : [hq1,...,hqn,e1,...,en,go1',...,gom'] + + declare(d1,...,dn) + + d : [d1,...,dn] + % q1 = if ck then (if r then gq1_0 else d1) else hq1 % + q1 : (gq1_0 when r default d1) when ck default hq1 + ... + qn : (gqn_0 when r default dn) when ck default hqn + + % P_inst = P[var_inst_g/var_g] % + evol_g : l_subst(evolution(g),var_g,var_inst_g); + evolutions : concat(evolutions,l_subst([q1,...,qn],[d1,...,dn],evol_g) + initialisations : concat(initialisations, [subst(initial(g),var_g,var_inst_g)]) + constraints : concat(constraints, [subst(constraint(g),var_g,var_inst_g)]) + + case inlined : + ho1 : subst(go1,var_g,var_inst_g) + ... + hom : subst(gom,var_g,var_inst_g) + case non inlined : + (nothing) + *) + let g_name = shortname g_name in + let (g_p,g_p_contract) = NamesEnv.find g_name env in + let g = if inlined then g_name else g_name ^ "_contract" in + (* add dependency *) + let acc_dep = g :: acc_dep in + let name_list = translate_pat pat in + let g_p = if inlined then g_p else g_p_contract in + (* var_g : [gq1,...,gqn,gi1,...,gip] *) + let var_g = "var_" ^ g in + let vars = + match inlined with + | true -> g_p.proc_states @ g_p.proc_inputs + | false -> g_p.proc_states @ g_p.proc_inputs @ g_p.proc_outputs in + let acc_eqs = + { stmt_name = var_g; + stmt_def = Slist(List.map (fun v -> Svar(v)) vars) }::acc_eqs in + (* var_inst_g : [hq1,...,hqn,e1,...,en] *) + let var_inst_g = "var_inst_" ^ g in + (* Coding contract states : S_n_id_s *) + (* id being the id of the application *) + (* n being the length of id *) + (* s being the name of the state*) + let a_id = name a_id in + let id_length = String.length a_id in + let s_prefix = "S_" ^ (string_of_int id_length) ^ "_" ^ a_id ^ "_" in + let new_states_list = + List.map + (fun g_state -> + (* Remove "g_" prefix *) + let l = (String.length g) in + let s = + String.sub + g_state (l+1) + ((String.length g_state)-(l+1)) in + prefixed (s_prefix ^ s)) + g_p.proc_states in + let e_states = List.map (fun hq -> Svar(hq)) new_states_list in + let e_list = List.map (translate prefix) e_list in + let e_outputs,acc_inputs = + match inlined with + | true -> [],acc_inputs + | false -> + let new_outputs = + List.map (fun name -> prefixed name) name_list in + (List.map (fun v -> Svar(v)) new_outputs),(acc_inputs@new_outputs) in + let vars_inst = e_states@e_list@e_outputs in + let acc_eqs = + { stmt_name = var_inst_g; + stmt_def = Slist(vars_inst); }::acc_eqs in + let acc_states = List.rev_append new_states_list acc_states in + let acc_init = List.rev_append g_p.proc_init acc_init in + (* declare(d1,...,dn) *) + let dummy_list = var_list dummy_prefix (List.length g_p.proc_states) in + (* d : [d1,...dn] *) + let acc_eqs = + {stmt_name = dummy_prefix; + stmt_def = Slist(List.map (fun di -> Svar(di)) dummy_list)}::acc_eqs in + (* qi = (gqi_0 when r default di) when ck default hqi *) + let q_list = List.map (fun _ -> "q_" ^ (gen_symbol ())) g_p.proc_states in + let e_list = + List.map2 + (fun (q0,hq) d -> + let e = Sdefault(Swhen(Sconst(q0), + Svar(prefixed (name r))),Svar(d)) in + let e = translate_ck (prefixed "") e ck in + Sdefault(e,Svar(hq))) + (List.combine g_p.proc_init new_states_list) dummy_list in + let acc_eqs = + List.fold_left2 + (fun acc_eqs q e -> {stmt_name = q; stmt_def = e}::acc_eqs) + acc_eqs q_list e_list in + (* evol_g : l_subst(evolution(g),var_g,var_inst_g); *) + let evol_g = "evol_" ^ g in + let acc_eqs = + {stmt_name = evol_g; + stmt_def = l_subst (evolution (Svar g)) (Svar var_g) (Svar var_inst_g)} + ::acc_eqs in + (* evolutions : concat(evolutions,l_subst([q1,...,qn],[d1,...,dn],evol_g) *) + let acc_eqs = + (extend evolutions (l_subst + (Slist (List.map (fun q -> Svar(q)) q_list)) + (Slist (List.map (fun d -> Svar(d)) dummy_list)) + + (Svar evol_g))) + ::acc_eqs in + (* initialisations : concat(initialisations, [subst(initial(g),var_g,var_inst_g)]) *) + let acc_eqs = + (extend initialisations (Slist[subst + (initial (Svar g)) + (Svar var_g) + (Svar var_inst_g)])) + :: acc_eqs in + (* constraints : concat(constraints, [subst(constraint(g),var_g,var_inst_g)]) *) + let acc_eqs = + (extend constraints (Slist[subst + (pconstraint (Svar g)) + (Svar var_g) + (Svar var_inst_g)])) + ::acc_eqs in + (* if inlined, hoi : subst(goi,var_g,var_inst_g) *) + let acc_eqs = + match inlined with + | true -> + List.fold_left2 + (fun acc_eqs o go -> + {stmt_name = prefixed o; + stmt_def = subst (Svar(go)) (Svar(var_g)) (Svar(var_inst_g))} + ::acc_eqs) + acc_eqs name_list g_p.proc_outputs + | false -> acc_eqs in + (* assume & guarantee *) + (* f_g_assume_x : subst(g_assume,var_g,var_inst_g) *) + (* f_g_guarantee_x : subst(g_guarantee,var_g,var_inst_g) *) + let var_assume = prefixed (g ^ "_assume_" ^ (gen_symbol ())) in + let var_guarantee = prefixed (g ^ "_guarantee_" ^ (gen_symbol ())) in + let acc_eqs = + {stmt_name = var_assume; + stmt_def = subst (Svar(g ^ "_assume")) (Svar(var_g)) (Svar(var_inst_g))} :: + {stmt_name = var_guarantee; + stmt_def = subst (Svar(g ^ "_guarantee")) (Svar(var_g)) (Svar(var_inst_g))} :: + acc_eqs in + let acc_cont = + (Svar(var_assume),Svar(var_guarantee)) :: acc_cont in + acc_dep,acc_states,acc_init, + acc_inputs,acc_ctrl,acc_cont,acc_eqs + | Minils.Evarpat(n), _ -> + (* assert : no fby, no node application in e *) + let e' = translate prefix e in + let e' = + begin match (actual_ty e.Minils.e_ty) with + | Tbool -> translate_ck prefix e' ck + | _ -> e' + end in + acc_dep,acc_states,acc_init, + acc_inputs,acc_ctrl,acc_cont, + { stmt_name = prefixed (name n); + stmt_def = e' }::acc_eqs + | _ -> assert false + +let translate_eq_list env f eq_list = + List.fold_left + (fun (acc_dep,acc_states,acc_init, + acc_inputs,acc_ctrl,acc_cont,acc_eqs) eq -> + translate_eq + env f + (acc_dep,acc_states,acc_init, + acc_inputs,acc_ctrl,acc_cont,acc_eqs) + eq) + ([],[],[],[],[],[],[]) + eq_list + +let translate_contract env f contract = + let prefix = f ^ "_" in + let var_a = prefix ^ "assume" in + let var_g = prefix ^ "guarantee" in + match contract with + | None -> + let body = + [{ stmt_name = var_g; stmt_def = Sconst(Ctrue) }; + { stmt_name = var_a; stmt_def = Sconst(Ctrue) }] in + [],[],[],body,(Svar(var_a),Svar(var_g)),[] + | Some {Minils.c_local = _locals; + Minils.c_eq = l_eqs; + Minils.c_assume = e_a; + Minils.c_enforce = e_g; + Minils.c_controllables = cl} -> + let dep,states,init,inputs, + controllables,_contracts,body = + translate_eq_list env f l_eqs in + assert (inputs = []); + assert (controllables = []); + let e_a = translate prefix e_a in + let e_g = translate prefix e_g in + let body = + {stmt_name = var_g; stmt_def = e_g} :: + {stmt_name = var_a; stmt_def = e_a} :: + body in + let controllables = + List.map (fun { Minils.v_ident = id } -> prefix ^ (name id)) cl in + dep,states,init,body,(Svar(var_a),Svar(var_g)),controllables + + + +let rec build_environment contracts = + match contracts with + | [] -> [],Sconst(Ctrue) + | [a,g] -> [a =>~ g],g + | (a,g)::l -> + let conts,assumes = build_environment l in + ((a =>~ g) :: conts),(g &~ assumes) + +let translate_node env + ({ Minils.n_name = {name = f}; + Minils.n_input = i_list; Minils.n_output = o_list; + Minils.n_local = _d_list; Minils.n_equs = eq_list; + Minils.n_contract = contract } as node) = + (* every variable is prefixed by its node name *) + let inputs = + List.map + (fun { Minils.v_ident = v } -> f ^ "_" ^ (name v)) i_list in + let outputs = + List.map + (fun { Minils.v_ident = v } -> f ^ "_" ^ (name v)) o_list in + let dep,states,init,add_inputs,add_controllables,contracts,body = + translate_eq_list env f eq_list in + let dep_c,states_c,init_c,body_c,(a_c,g_c),controllables = + translate_contract env f contract in + let inputs = inputs @ add_inputs in + let controllables = controllables @ add_controllables in + let body = List.rev body in + let states = List.rev states in + let body_c = List.rev body_c in + let states_c = List.rev states_c in + let constraints = + List.map + (fun v -> Sequal(Ssquare(Svar(v)),Sconst(Ctrue))) + (inputs@controllables) in + let contracts_components,assumes_components = + build_environment contracts in + let constraints = constraints @ + contracts_components @ [Sequal (a_c,Sconst(Ctrue))] in + let impl = g_c &~ assumes_components in + let obj = Security(impl) in + let p = { proc_dep = unique (dep @ dep_c); + proc_name = f; + proc_inputs = inputs@controllables; + proc_uncont_inputs = inputs; + proc_outputs = outputs; + proc_controllables = controllables; + proc_states = states@states_c; + proc_init = init@init_c; + proc_constraints = constraints; + proc_body = body@body_c; + proc_objectives = [obj] } in + (* Hack : save inputs and states names for controller call *) + let remove_prefix = + let n = String.length f in + fun s -> + String.sub s (n+1) ((String.length s) - (n+1)) in + node.Minils.n_controller_call <- + (List.map remove_prefix inputs, + List.map remove_prefix (states@states_c)); + + let f_contract = f ^ "_contract" in + let inputs_c = + List.map + (fun { Minils.v_ident = v } -> f_contract ^ "_" ^ (name v)) i_list in + let outputs_c = + List.map + (fun { Minils.v_ident = v } -> f_contract ^ "_" ^ (name v)) o_list in + let dep_c,states_c,init_c,body_c,(_a_c,_g_c),_controllables = + translate_contract env f_contract contract in + let states_c = List.rev states_c in + let body_c = List.rev body_c in + let constraints_c = + List.map + (fun v -> Sequal(Ssquare(Svar(v)),Sconst(Ctrue))) + (inputs_c@outputs_c) in + let p_c = { proc_dep = dep_c; + proc_name = f ^ "_contract"; + proc_inputs = inputs_c@outputs_c; + proc_uncont_inputs = inputs_c@outputs_c; + proc_outputs = []; + proc_controllables = []; + proc_states = states_c; + proc_init = init_c; + proc_constraints = constraints_c; + proc_body = body_c; + proc_objectives = [] } in + (NamesEnv.add f (p,p_c) env), (p,p_c) + +let program p = + let _env,acc_proc = + List.fold_left + (fun (env,acc) node -> + let env,(proc,contract) = translate_node env node in + env,contract::proc::acc) + (NamesEnv.empty,[]) + p.Minils.p_nodes in + let procs = List.rev acc_proc in + let filename = filename_of_name p.Minils.p_modname in + let dirname = build_path (filename ^ "_z3z") in + let dir = clean_dir dirname in + Sigali.Printer.print dir procs + diff --git a/compiler/minils/sigali/sigalimain.mli b/compiler/minils/sigali/sigalimain.mli new file mode 100644 index 0000000..195b8cb --- /dev/null +++ b/compiler/minils/sigali/sigalimain.mli @@ -0,0 +1,14 @@ +(****************************************************) +(* *) +(* Heptagon/BZR *) +(* *) +(* Author : Gwenaël Delaval *) +(* Organization : Univ. Grenoble, LIG *) +(* *) +(****************************************************) + +(* Translation from the source language to Sigali polynomial systems *) + +(* $Id$ *) + +val program : Minils.program -> unit From 85bbe21d6cc0a1289cbbb9dc88b647acc20e275c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Gwena=C3=ABl=20Delaval?= Date: Wed, 16 Mar 2011 23:34:35 +0100 Subject: [PATCH 07/12] Sigali pass into compiler + added a_id field to applications - Added "z3z" target language, calling sigali code generation - a_id is application id, so as to identify node applications; added to Minils AST. a_id is given on hept2mls pass. This is needed for the controller execution from controller synthesis. --- compiler/main/hept2mls.ml | 8 +++++++- compiler/main/mls2obc.ml | 7 ++++++- compiler/main/mls2seq.ml | 2 ++ compiler/minils/_tags | 1 + compiler/minils/minils.ml | 15 ++++++++++----- 5 files changed, 26 insertions(+), 7 deletions(-) diff --git a/compiler/main/hept2mls.ml b/compiler/main/hept2mls.ml index d45269b..5b2ac21 100644 --- a/compiler/main/hept2mls.ml +++ b/compiler/main/hept2mls.ml @@ -44,6 +44,10 @@ struct raise Errors.Error end +let fresh = Idents.gen_fresh "hept2mls" + (function Heptagon.Enode f -> (shortname f) + | _ -> "n") + (* add an equation *) let equation locals eqs e = let n = Idents.gen_var "hept2mls" "ck" in @@ -87,7 +91,9 @@ let rec translate_op = function let translate_app app = mk_app ~params:app.Heptagon.a_params - ~unsafe:app.Heptagon.a_unsafe (translate_op app.Heptagon.a_op) + ~unsafe:app.Heptagon.a_unsafe + ~id:(Some (fresh app.Heptagon.a_op)) + (translate_op app.Heptagon.a_op) let rec translate_extvalue e = let mk_extvalue = mk_extvalue ~loc:e.Heptagon.e_loc ~ty:e.Heptagon.e_ty in diff --git a/compiler/main/mls2obc.ml b/compiler/main/mls2obc.ml index 93862f0..4afff64 100644 --- a/compiler/main/mls2obc.ml +++ b/compiler/main/mls2obc.ml @@ -461,7 +461,12 @@ and mk_node_call map call_context app loc name_list args ty = v @ nd.Minils.n_local, si, j, subst_act_list env s | Minils.Enode f | Minils.Efun f -> - let o = mk_obj_call_from_context call_context (gen_obj_ident f) in + let id = + begin match app.Minils.a_id with + None -> gen_obj_name f + | Some id -> name id + end in + let o = mk_obj_call_from_context call_context id in let obj = { o_ident = obj_ref_name o; o_class = f; o_params = app.Minils.a_params; diff --git a/compiler/main/mls2seq.ml b/compiler/main/mls2seq.ml index 1484058..a3c732a 100644 --- a/compiler/main/mls2seq.ml +++ b/compiler/main/mls2seq.ml @@ -42,10 +42,12 @@ let no_conf () = () let targets = [ "c",(Obc_no_params Cmain.program, no_conf); "java", (Obc Java_main.program, no_conf); + "z3z", (Minils_no_params Sigalimain.program, no_conf); "obc", (Obc write_obc_file, no_conf); "obc_np", (Obc_no_params write_obc_file, no_conf); "epo", (Minils write_object_file, no_conf) ] + let generate_target p s = let print_unfolded p_list = comment "Unfolding"; diff --git a/compiler/minils/_tags b/compiler/minils/_tags index 305173d..7d88cc5 100644 --- a/compiler/minils/_tags +++ b/compiler/minils/_tags @@ -1 +1,2 @@ or or
or :include +:include \ No newline at end of file diff --git a/compiler/minils/minils.ml b/compiler/minils/minils.ml index 4996bd2..ac7bce2 100644 --- a/compiler/minils/minils.ml +++ b/compiler/minils/minils.ml @@ -72,7 +72,11 @@ and edesc = * extvalue list * extvalue list * var_ident option (** map f <> (extvalue, extvalue...) reset ident *) -and app = { a_op: op; a_params: static_exp list; a_unsafe: bool } +and app = { a_op: op; + a_params: static_exp list; + a_unsafe: bool; + a_id: ident option; + a_inlined: bool } (** Unsafe applications could have side effects and be delicate about optimizations, !be careful! *) @@ -120,8 +124,8 @@ type node_dec = { n_input : var_dec list; n_output : var_dec list; n_contract : contract option; - (* GD: inglorious hack for controller call - mutable n_controller_call : var_ident list * var_ident list; *) + (* GD: inglorious hack for controller call *) + mutable n_controller_call : string list * string list; n_local : var_dec list; n_equs : eq list; n_loc : location; @@ -182,6 +186,7 @@ let mk_type_dec type_desc name loc = let mk_const_dec id ty e loc = { c_name = id; c_type = ty; c_value = e; c_loc = loc } -let mk_app ?(params=[]) ?(unsafe=false) op = - { a_op = op; a_params = params; a_unsafe = unsafe } +let mk_app ?(params=[]) ?(unsafe=false) ?(id=None) ?(inlined=false) op = + { a_op = op; a_params = params; a_unsafe = unsafe; + a_id = id; a_inlined = inlined } From 243fe4b4c7e6747e1bde31b68ff2ed772f275c6b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Gwena=C3=ABl=20Delaval?= Date: Wed, 16 Mar 2011 23:39:30 +0100 Subject: [PATCH 08/12] Keyword "inlined" for nodes Added a keyword "inlined": "inlined f(x)" is intended to inline only this application. (not effective yet) --- compiler/heptagon/heptagon.ml | 7 ++++--- compiler/heptagon/parsing/hept_lexer.mll | 1 + compiler/heptagon/parsing/hept_parser.mly | 8 ++++++-- compiler/heptagon/parsing/hept_parsetree.ml | 12 ++++++------ compiler/heptagon/parsing/hept_scoping.ml | 4 ++-- 5 files changed, 19 insertions(+), 13 deletions(-) diff --git a/compiler/heptagon/heptagon.ml b/compiler/heptagon/heptagon.ml index 4cd3924..7f5bc0d 100644 --- a/compiler/heptagon/heptagon.ml +++ b/compiler/heptagon/heptagon.ml @@ -52,7 +52,8 @@ and desc = and app = { a_op : op; a_params : static_exp list; - a_unsafe : bool } + a_unsafe : bool; + a_inlined : bool } and op = | Eequal @@ -194,8 +195,8 @@ let mk_exp desc ?(ct_annot = Clocks.invalid_clock) ?(loc = no_location) ty = { e_desc = desc; e_ty = ty; e_ct_annot = ct_annot; e_base_ck = Cbase; e_loc = loc; } -let mk_app ?(params=[]) ?(unsafe=false) op = - { a_op = op; a_params = params; a_unsafe = unsafe } +let mk_app ?(params=[]) ?(unsafe=false) ?(inlined=false) op = + { a_op = op; a_params = params; a_unsafe = unsafe; a_inlined = inlined } let mk_op_app ?(params=[]) ?(unsafe=false) ?(reset=None) op args = Eapp(mk_app ~params:params ~unsafe:unsafe op, args, reset) diff --git a/compiler/heptagon/parsing/hept_lexer.mll b/compiler/heptagon/parsing/hept_lexer.mll index e370f0d..7ad7845 100644 --- a/compiler/heptagon/parsing/hept_lexer.mll +++ b/compiler/heptagon/parsing/hept_lexer.mll @@ -53,6 +53,7 @@ List.iter (fun (str,tok) -> Hashtbl.add keyword_table str tok) [ "assume", ASSUME; "enforce", ENFORCE; "with", WITH; + "inlined",INLINED; "when", WHEN; "merge", MERGE; "map", MAP; diff --git a/compiler/heptagon/parsing/hept_parser.mly b/compiler/heptagon/parsing/hept_parser.mly index e3ad86f..6ffcb93 100644 --- a/compiler/heptagon/parsing/hept_parser.mly +++ b/compiler/heptagon/parsing/hept_parser.mly @@ -39,6 +39,7 @@ open Hept_parsetree %token ASSUME %token ENFORCE %token WITH +%token INLINED %token WHEN MERGE %token POWER %token LBRACKET LBRACKETGREATER @@ -411,6 +412,9 @@ _simple_exp: /* TODO : conflict with Eselect_dyn and or const*/ ; +node_name: + | q=qualname c=call_params { mk_app (Enode q) c false } + | INLINED q=qualname c=call_params { mk_app (Enode q) c true } merge_handlers: | hs=nonempty_list(merge_handler) { hs } @@ -426,8 +430,8 @@ _exp: | PRE exp { Epre (None, $2) } /* node call*/ - | n=qualname p=call_params LPAREN args=exps RPAREN - { Eapp(mk_app (Enode n) p , args) } + | n=node_name LPAREN args=exps RPAREN + { Eapp(n, args) } | NOT exp { mk_op_call "not" [$2] } | exp INFIX4 exp diff --git a/compiler/heptagon/parsing/hept_parsetree.ml b/compiler/heptagon/parsing/hept_parsetree.ml index f567ddb..afeab5a 100644 --- a/compiler/heptagon/parsing/hept_parsetree.ml +++ b/compiler/heptagon/parsing/hept_parsetree.ml @@ -77,7 +77,7 @@ and edesc = | Ewhen of exp * constructor_name * var_name | Emerge of var_name * (constructor_name * exp) list -and app = { a_op: op; a_params: exp list; } +and app = { a_op: op; a_params: exp list; a_inlined: bool } and op = | Eequal @@ -219,17 +219,17 @@ and interface_desc = let mk_exp desc ?(ct_annot = Clocks.invalid_clock) loc = { e_desc = desc; e_ct_annot = ct_annot; e_loc = loc } -let mk_app op params = - { a_op = op; a_params = params; } +let mk_app op params inlined = + { a_op = op; a_params = params; a_inlined = inlined } -let mk_call ?(params=[]) op exps = - Eapp (mk_app op params, exps) +let mk_call ?(params=[]) ?(inlined=false) op exps = + Eapp (mk_app op params inlined, exps) let mk_op_call ?(params=[]) s exps = mk_call ~params:params (Efun (Q (Names.pervasives_qn s))) exps let mk_iterator_call it ln params n pexps exps = - Eiterator (it, mk_app (Enode ln) params, n, pexps, exps) + Eiterator (it, mk_app (Enode ln) params false, n, pexps, exps) let mk_static_exp desc loc = { se_desc = desc; se_loc = loc } diff --git a/compiler/heptagon/parsing/hept_scoping.ml b/compiler/heptagon/parsing/hept_scoping.ml index 61ad4e6..1f5b56c 100644 --- a/compiler/heptagon/parsing/hept_scoping.ml +++ b/compiler/heptagon/parsing/hept_scoping.ml @@ -244,10 +244,10 @@ and translate_desc loc env = function List.map (fun (f,e) -> qualify_field f, translate_exp env e) f_e_list in Heptagon.Estruct f_e_list - | Eapp ({ a_op = op; a_params = params; }, e_list) -> + | Eapp ({ a_op = op; a_params = params; a_inlined = inl }, e_list) -> let e_list = List.map (translate_exp env) e_list in let params = List.map (expect_static_exp) params in - let app = Heptagon.mk_app ~params:params (translate_op op) in + let app = Heptagon.mk_op ~params:params ~inlined:inl (translate_op op) in Heptagon.Eapp (app, e_list, None) | Eiterator (it, { a_op = op; a_params = params }, n, pe_list, e_list) -> From 8c4217ab83182820ac5a160b356609a6ee64041e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Gwena=EBl=20Delaval?= Date: Wed, 20 Apr 2011 11:42:03 +0200 Subject: [PATCH 09/12] Rebase bzr branch on old decade --- compiler/heptagon/parsing/hept_scoping.ml | 2 +- compiler/main/hept2mls.ml | 2 ++ compiler/main/mls2obc.ml | 4 +-- compiler/minils/minils.ml | 4 ++- compiler/minils/sigali/sigalimain.ml | 10 ++++---- compiler/minils/transformations/boolean.ml | 30 +++++++++++++--------- 6 files changed, 31 insertions(+), 21 deletions(-) diff --git a/compiler/heptagon/parsing/hept_scoping.ml b/compiler/heptagon/parsing/hept_scoping.ml index 1f5b56c..d039d84 100644 --- a/compiler/heptagon/parsing/hept_scoping.ml +++ b/compiler/heptagon/parsing/hept_scoping.ml @@ -247,7 +247,7 @@ and translate_desc loc env = function | Eapp ({ a_op = op; a_params = params; a_inlined = inl }, e_list) -> let e_list = List.map (translate_exp env) e_list in let params = List.map (expect_static_exp) params in - let app = Heptagon.mk_op ~params:params ~inlined:inl (translate_op op) in + let app = Heptagon.mk_app ~params:params ~inlined:inl (translate_op op) in Heptagon.Eapp (app, e_list, None) | Eiterator (it, { a_op = op; a_params = params }, n, pe_list, e_list) -> diff --git a/compiler/main/hept2mls.ml b/compiler/main/hept2mls.ml index 5b2ac21..5efddc0 100644 --- a/compiler/main/hept2mls.ml +++ b/compiler/main/hept2mls.ml @@ -191,12 +191,14 @@ let node n = n_input = List.map translate_var n.Heptagon.n_input; n_output = List.map translate_var n.Heptagon.n_output; n_contract = translate_contract n.Heptagon.n_contract; + n_controller_call = ([],[]); n_local = List.map translate_var n.Heptagon.n_block.Heptagon.b_local; n_equs = List.map translate_eq n.Heptagon.n_block.Heptagon.b_equs; n_loc = n.Heptagon.n_loc ; n_params = n.Heptagon.n_params; n_params_constraints = n.Heptagon.n_params_constraints } + let typedec {Heptagon.t_name = n; Heptagon.t_desc = tdesc; Heptagon.t_loc = loc} = let onetype = function diff --git a/compiler/main/mls2obc.ml b/compiler/main/mls2obc.ml index 4afff64..85bad7d 100644 --- a/compiler/main/mls2obc.ml +++ b/compiler/main/mls2obc.ml @@ -463,8 +463,8 @@ and mk_node_call map call_context app loc name_list args ty = | Minils.Enode f | Minils.Efun f -> let id = begin match app.Minils.a_id with - None -> gen_obj_name f - | Some id -> name id + None -> gen_obj_ident f + | Some id -> id end in let o = mk_obj_call_from_context call_context id in let obj = diff --git a/compiler/minils/minils.ml b/compiler/minils/minils.ml index ac7bce2..e808f12 100644 --- a/compiler/minils/minils.ml +++ b/compiler/minils/minils.ml @@ -166,7 +166,8 @@ let mk_equation ?(loc = no_location) pat exp = { eq_lhs = pat; eq_rhs = exp; eq_loc = loc } let mk_node - ?(input = []) ?(output = []) ?(contract = None) ?(local = []) ?(eq = []) + ?(input = []) ?(output = []) ?(contract = None) ?(pinst = ([],[])) + ?(local = []) ?(eq = []) ?(stateful = true) ?(loc = no_location) ?(param = []) ?(constraints = []) name = { n_name = name; @@ -174,6 +175,7 @@ let mk_node n_input = input; n_output = output; n_contract = contract; + n_controller_call = pinst; n_local = local; n_equs = eq; n_loc = loc; diff --git a/compiler/minils/sigali/sigalimain.ml b/compiler/minils/sigali/sigalimain.ml index 033dd55..9a5dcbd 100644 --- a/compiler/minils/sigali/sigalimain.ml +++ b/compiler/minils/sigali/sigalimain.ml @@ -22,8 +22,8 @@ open Sigali type mtype = Tint | Tbool | Tother let actual_ty = function - | Tid({ qual = "Pervasives"; name = "bool"}) -> Tbool - | Tid({ qual = "Pervasives"; name = "int"}) -> Tint + | Tid({ qual = Pervasives; name = "bool"}) -> Tbool + | Tid({ qual = Pervasives; name = "int"}) -> Tint | _ -> Tother let var_list prefix n = @@ -73,7 +73,7 @@ let rec translate prefix ({ Minils.e_desc = desc; Minils.e_ty = ty } as e) = end | Minils.Evar(n) -> Svar(prefix ^ (name n)) | Minils.Eapp (* pervasives binary or unary stateless operations *) - ({ Minils.a_op = Minils.Efun({qual="Pervasives";name=n})}, + ({ Minils.a_op = Minils.Efun({qual=Pervasives;name=n})}, e_list, _) -> begin match n, e_list with @@ -134,7 +134,7 @@ let rec translate prefix ({ Minils.e_desc = desc; Minils.e_ty = ty } as e) = end | Minils.Estruct(_) -> failwith("Sigali: structures not implemented") - | Minils.Eiterator(_,_,_,_,_) -> + | Minils.Eiterator(_,_,_,_,_,_) -> failwith("Sigali: iterators not implemented") | Minils.Eapp({Minils.a_op = Minils.Enode(_)},_,_) -> failwith("Sigali: node in expressions; programs should be normalized") @@ -657,7 +657,7 @@ let program p = (NamesEnv.empty,[]) p.Minils.p_nodes in let procs = List.rev acc_proc in - let filename = filename_of_name p.Minils.p_modname in + let filename = filename_of_name (modul_to_string p.Minils.p_modname) in let dirname = build_path (filename ^ "_z3z") in let dir = clean_dir dirname in Sigali.Printer.print dir procs diff --git a/compiler/minils/transformations/boolean.ml b/compiler/minils/transformations/boolean.ml index 33506fc..aeaa830 100644 --- a/compiler/minils/transformations/boolean.ml +++ b/compiler/minils/transformations/boolean.ml @@ -51,7 +51,7 @@ open Minils let fresh = Idents.gen_fresh "bool" (fun s -> s) -let ty_bool = Tid({ qual = "Pervasives"; name = "bool"}) +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)) @@ -60,8 +60,8 @@ let sbool = function | true -> strue | false -> sfalse -let ctrue = { qual = "Pervasives"; name = "true" } -let cfalse = { qual = "Pervasives"; name = "false" } +let ctrue = { qual = Pervasives; name = "true" } +let cfalse = { qual = Pervasives; name = "false" } let mk_tuple e_l = Eapp((mk_app Etuple),e_l,None) @@ -224,7 +224,7 @@ let translate_pat env pat = let translate_ty ty = let rec trans ty = match ty with - | Tid({ qual = "Pervasives"; name = "bool" }) -> ty + | Tid({ qual = Pervasives; name = "bool" }) -> ty | Tid(name) -> begin try @@ -240,6 +240,7 @@ 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 @@ -271,7 +272,7 @@ let rec translate_ck env ck = let translate_const c ty e = match c.se_desc,ty with - | _, Tid({ qual = "Pervasives"; name = "bool" }) -> Econst(c) + | _, Tid({ qual = Pervasives; name = "bool" }) -> Econst(c) | Sconstructor(cname),Tid(tname) -> begin try @@ -352,11 +353,11 @@ let rec when_ck desc ty ck = let rec base_value ck ty = match ty with - | Tid({qual = "Pervasives"; name = "int" }) -> + | Tid({qual = Pervasives; name = "int" }) -> when_ck (Econst(mk_static_exp ~ty:ty (Sint(0)))) ty ck - | Tid({qual = "Pervasives"; name = "float"}) -> + | Tid({qual = Pervasives; name = "float"}) -> when_ck (Econst(mk_static_exp ~ty:ty (Sfloat(0.)))) ty ck - | Tid({qual = "Pervasives"; name = "bool" }) -> + | Tid({qual = Pervasives; name = "bool" }) -> when_ck (Econst(strue)) ty ck | Tid(sname) -> begin @@ -411,6 +412,9 @@ let rec base_value ck ty = 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; @@ -530,9 +534,10 @@ let rec translate env context ({e_desc = desc; e_ty = ty; e_ck = ck} as e) = (context,(c,e)::acc)) (context,[]) l in context,Estruct(List.rev acc) - | Eiterator(it,app,se,e_list,r) -> + | Eiterator(it,app,se,pe_list,e_list,r) -> + let context,pe_list = translate_list env context pe_list in let context,e_list = translate_list env context e_list in - context,Eiterator(it,app,se,e_list,r) + context,Eiterator(it,app,se,pe_list,e_list,r) in context,{ e with e_desc = desc; @@ -678,11 +683,12 @@ 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 _ | Tunit -> v::acc_vd, acc_loc, acc_eq, env + | Tprod _ | Tarray _ | Tmutable _ | Tunit -> + v::acc_vd, acc_loc, acc_eq, env | Tid(tname) -> begin match tname with - | { qual = "Pervasives"; name = ("bool" | "int" | "float") } -> + | { qual = Pervasives; name = ("bool" | "int" | "float") } -> v::acc_vd, acc_loc, acc_eq, env | _ -> begin 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 10/12] 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 From c77386d51726f9906965d41a5e30f646ddb4b98b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Gwena=EBl=20Delaval?= Date: Wed, 27 Jul 2011 11:21:34 +0200 Subject: [PATCH 11/12] Active Boolean pass and Sigali backend --- compiler/heptagon/transformations/boolean.ml | 183 +++++++++++-------- compiler/minils/sigali/sigalimain.ml | 99 +++++----- 2 files changed, 162 insertions(+), 120 deletions(-) diff --git a/compiler/heptagon/transformations/boolean.ml b/compiler/heptagon/transformations/boolean.ml index 2371528..625a3f0 100644 --- a/compiler/heptagon/transformations/boolean.ml +++ b/compiler/heptagon/transformations/boolean.ml @@ -172,7 +172,7 @@ let rec var_list clist = let t = Tree(t1,t2) in nv2 + 1, vl, t -let var_list prefix n = +let nvar_list prefix n = let rec varl acc = function | 0 -> acc | n -> @@ -209,13 +209,14 @@ let translate_ty ty = | Type(_) -> ty | Enum { ty_nb_var = 1 } -> ty_bool | Enum { ty_nb_var = n } -> - let strlist = var_list "" n in + let strlist = nvar_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) + | Tinvalid -> assert false in trans ty @@ -278,8 +279,7 @@ let translate_const c ty e = end | _ -> Econst(c) -(* TODO HERE : ct/ck *) -let new_var_list d_list ty ct n = +let new_var_list d_list ty ck n = let rec varl acc d_list = function | 0 -> acc,d_list | n -> @@ -289,6 +289,10 @@ let new_var_list d_list ty ct n = varl acc d_list (n-1) in varl [] d_list n +let assert_ck = function + Ck(ck) -> ck + | Cprod(_) -> assert false + let intro_tuple context e = let n = match e.e_ty with @@ -298,9 +302,11 @@ 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_ct_annot n in + (* e is not a tuple, therefore e.e_ct_annot = Ck(ck) *) + let ck = assert_ck e.e_ct_annot in + let v_list,d_list = new_var_list d_list ty_bool 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 eq_list = (mk_equation (Eeq(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 @@ -309,9 +315,11 @@ let rec when_list e bl vtree = | [], _ -> e | b::bl', VNode(v,t0,t1) -> let (c,t) = if b then (ctrue,t1) else (cfalse,t0) in + let ck = assert_ck e.e_ct_annot in + let e_v = mk_exp (Evar v) ~ct_annot:(Ck(ck)) ty_bool in let e_when = { e with - e_ct_annot = Con(e.e_ct_annot,c,v); - e_desc = Ewhen(e,c,v) } in + e_ct_annot = Ck(Con(ck,c,v)); + e_desc = Ewhen(e,c,e_v) } in when_list e_when bl' t | _::_, Vempty -> failwith("when_list: non-coherent boolean list and tree") @@ -320,14 +328,15 @@ let rec when_ck desc ty ck = | Cbase | Cvar _ -> { e_desc = desc; e_base_ck = Cbase; - e_ct_annot = ck; + e_ct_annot = 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); + let e_v = mk_exp (Evar v) ~ct_annot:(Ck(ck')) ty_bool in + { e_desc = Ewhen(e,c,e_v); e_base_ck = Cbase; - e_ct_annot = ck; + e_ct_annot = Ck(ck); e_ty = ty; e_loc = no_location } @@ -370,7 +379,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_ct_annot = ck; + e_ct_annot = Ck(ck); e_loc = no_location } end with Not_found -> @@ -381,7 +390,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_ct_annot = ck; + e_ct_annot = Ck(ck); e_loc = no_location; } | Tarray(ty,se) -> @@ -389,30 +398,32 @@ 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_ct_annot = ck; + e_ct_annot = Ck(ck); e_loc = no_location; } + | Tinvalid -> failwith("Boolean: invalid type") 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_ct_annot = ck } + { e with e_ct_annot = 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)]); + let e_v = mk_exp (Evar v) ~ct_annot:(Ck(ck)) ty_bool in + { e_desc = Emerge(e_v,[(ctrue,e1);(cfalse,e2)]); e_ty = ty; e_base_ck = Cbase; - e_ct_annot = ck; + e_ct_annot = 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_ct_annot = ck} as e) = - let ck = translate_ct env ck in +let rec translate env context ({e_desc = desc; e_ty = ty; e_ct_annot = ct} as e) = + let ct = translate_ct env ct in let context,desc = match desc with | Econst(c) -> @@ -428,21 +439,25 @@ let rec translate env context ({e_desc = desc; e_ty = ty; e_ct_annot = ck} as e) mk_tuple (List.map (fun v -> { e with e_ty = ty_bool; - e_ct_annot = ck; + e_ct_annot = ct; e_desc = Evar(v); }) ident_list) with Not_found -> Evar(name) end in context,desc - | Efby(None, e) -> + | Efby(e1,e2) -> + let context,e1 = translate env context e1 in + let context,e2 = translate env context e2 in + context,Efby(e1,e2) + | Epre(None, e) -> let context,e = translate env context e in - context,Efby(None,e) - | Efby(Some c,e) -> + context,Epre(None,e) + | Epre(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) + | Econst(c) -> context,Epre(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 @@ -453,14 +468,14 @@ let rec translate env context ({e_desc = desc; e_ty = ty; e_ct_annot = ck} as e) (List.map2 (fun c e -> { e with e_ty = ty_bool; - e_desc = Efby(Some c,e)}) + e_desc = Epre(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) -> + | Ewhen(e,c,({ e_desc = Evar(ck) } as e_ck)) -> let context,e = translate env context e in begin try @@ -470,20 +485,20 @@ let rec translate env context ({e_desc = desc; e_ty = ty; e_ct_annot = ck} as e) context,e_when.e_desc with Not_found -> (* Boolean clock *) - context,Ewhen(e,c,ck) + context,Ewhen(e,c,e_ck) end - | Emerge(ck_m,l) (* of name * (longname * exp) list *) + | Emerge(({ e_desc = Evar(ck) } as e_ck),l) (* of name * (longname * exp) list *) -> begin try - let info = Env.find ck_m env in + let info = Env.find ck 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 + merge_tree (assert_ck ct) ty e_map info.var_enum.ty_tree info.clocked_var in context,e_merge.e_desc @@ -495,7 +510,7 @@ let rec translate env context ({e_desc = desc; e_ty = ty; e_ct_annot = ck} as e) let context,e = translate env context e in context, (n,e)::acc_l) (context,[]) l in - context,Emerge(ck_m,l) + context,Emerge(e_ck,l) end | Estruct(l) -> let context,acc = @@ -509,11 +524,15 @@ let rec translate env context ({e_desc = desc; e_ty = ty; e_ct_annot = ck} as e) let context,pe_list = translate_list env context pe_list in let context,e_list = translate_list env context e_list in context,Eiterator(it,app,se,pe_list,e_list,r) + | Ewhen(_,_,_) + | Emerge(_,_) + | Elast _ -> + failwith("Boolean: not supported expression (abstract tree should be normalized)") in context,{ e with e_desc = desc; e_ty = translate_ty ty; - e_ct_annot = ck} + e_ct_annot = ct} and translate_list env context e_list = let context,acc_e = @@ -524,27 +543,6 @@ and translate_list env context e_list = (context,[]) e_list in context,List.rev acc_e -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 -> - 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 @@ -567,7 +565,8 @@ let var_dec_list (acc_vd,acc_loc,acc_eq) var_from n = | _ckvar::l, Con(ck',c,v) -> (* assert v = _ckvar *) let e = when_ck l ck' var in - { e_desc = Ewhen(e,c,v); + let e_v = mk_exp (Evar v) ~ct_annot:(Ck(ck')) ty_bool in + { e_desc = Ewhen(e,c,e_v); e_base_ck = Cbase; e_ct_annot = Ck(ck); e_ty = ty_bool; @@ -636,9 +635,8 @@ let var_dec_list (acc_vd,acc_loc,acc_eq) var_from n = 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 + (mk_equation (Eeq(Evarpat(id),(when_ck acc_var ck vi)))) + ::acc_eq in (* Build left son (ck on False(vi_...)) *) let ck_0 = Con(ck,cfalse,id) in let acc_loc,acc_eq,t0 = @@ -696,7 +694,8 @@ let buildenv_var_dec (acc_vd,acc_loc,acc_eq,env) ({v_type = ty} as v) = with Not_found -> v::acc_vd, acc_loc, acc_eq, env end end - + | Tinvalid -> failwith("Boolean: invalid type") + let buildenv_var_dec_list env vlist = List.fold_left buildenv_var_dec ([],[],[],env) vlist @@ -706,7 +705,7 @@ 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; +let rec 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 @@ -718,12 +717,31 @@ let translate_block env add_locals add_eqs ({ b_local = v; b_local = v@d_list; b_equs = eq_list }, env +and 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 eq_desc = desc }::eq_list + +and translate_eqs env eq_list = + List.fold_left + (fun context eq -> + translate_eq env context eq) ([],[]) eq_list + let translate_contract env contract = match contract with | None -> None, env - | Some { c_local = v; - c_eq = eq_list; - c_assume = e_a; + | Some { c_assume = e_a; c_enforce = e_g; c_controllables = cl; c_block = b } -> @@ -738,7 +756,6 @@ let translate_contract env contract = 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 }, @@ -753,24 +770,34 @@ let node ({ n_input = inputs; let contract, env = translate_contract env contract 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 + let b,_ = translate_block env add_locals add_eqs b in { n with n_input = List.rev inputs; n_output = List.rev outputs; n_contract = contract; n_block = b } - -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 } +let program_desc p_desc = + match p_desc with + | Pnode(n) -> Pnode(node n) + | _ -> p_desc + +let build p_desc = + match p_desc with + | Ptype(type_dec) -> + begin + 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 + end + | _ -> () + +let program ({ p_desc = d_list } as p) = + List.iter build d_list; + { p with p_desc = List.map program_desc d_list } diff --git a/compiler/minils/sigali/sigalimain.ml b/compiler/minils/sigali/sigalimain.ml index 9a5dcbd..55b3592 100644 --- a/compiler/minils/sigali/sigalimain.ml +++ b/compiler/minils/sigali/sigalimain.ml @@ -2,8 +2,8 @@ (* *) (* Heptagon/BZR *) (* *) -(* Author : Gwenaël Delaval *) -(* Organization : INRIA Rennes, VerTeCs *) +(* Author : Gwena�l Delaval *) +(* Organization : UJF, LIG *) (* *) (****************************************************) @@ -62,26 +62,42 @@ let rec translate_ck pref e = function | "false" -> Snot(Svar(pref ^ (name var))) | _ -> assert false) -(* [translate e = c] *) -let rec translate prefix ({ Minils.e_desc = desc; Minils.e_ty = ty } as e) = + +let rec translate_ext prefix ({ Minils.w_desc = desc; Minils.w_ty = ty } as e) = match desc with - | Minils.Econst(v) -> + | Minils.Wconst(v) -> begin match (actual_ty ty) with | Tbool -> Sconst(translate_static_exp v) | Tint -> a_const (Sconst(translate_static_exp v)) | Tother -> failwith("Sigali: untranslatable type") end - | Minils.Evar(n) -> Svar(prefix ^ (name n)) + | Minils.Wvar(n) -> Svar(prefix ^ (name n)) + | Minils.Wwhen(e, c, var) when ((actual_ty e.Minils.w_ty) = Tbool) -> + let e = translate_ext prefix e in + Swhen(e, + match (shortname c) with + "true" -> Svar(prefix ^ (name var)) + | "false" -> Snot(Svar(prefix ^ (name var))) + | _ -> assert false) + | Minils.Wwhen(e, _c, _var) -> + translate_ext prefix e + | Minils.Wfield(_) -> + failwith("Sigali: structures not implemented") + +(* [translate e = c] *) +let rec translate prefix ({ Minils.e_desc = desc; Minils.e_ty = ty } as e) = + match desc with + | Minils.Eextvalue(ext) -> translate_ext prefix ext | Minils.Eapp (* pervasives binary or unary stateless operations *) ({ Minils.a_op = Minils.Efun({qual=Pervasives;name=n})}, e_list, _) -> begin match n, e_list with - | "not", [e] -> Snot(translate prefix e) - | "or", [e1;e2] -> Sor((translate prefix e1),(translate prefix e2)) - | "&", [e1;e2] -> Sand((translate prefix e1),(translate prefix e2)) - (* a_inf and a_sup : +1 to translate ideals to boolean - polynomials *) + | "not", [e] -> Snot(translate_ext prefix e) + | "or", [e1;e2] -> Sor((translate_ext prefix e1), + (translate_ext prefix e2)) + | "&", [e1;e2] -> Sand((translate_ext prefix e1), + (translate_ext prefix e2)) | ("<="|"<"|">="|">"), [e1;e2] -> let op,modv = begin match n with @@ -90,35 +106,31 @@ let rec translate prefix ({ Minils.e_desc = desc; Minils.e_ty = ty } as e) = | ">=" -> a_sup,0 | _ -> a_sup,1 end in - let e1 = translate prefix e1 in - begin match e2.Minils.e_desc with - | Minils.Econst({se_desc = Sint(v)}) -> - let e = op e1 (Sconst(Cint(v+modv))) in - Splus(e,Sconst(Ctrue)) - | _ -> - let e2 = translate prefix e2 in - let e = op (Sminus(e1,e2)) (Sconst(Cint(modv))) in - Splus(e,Sconst(Ctrue)) - end - | "+", [e1;e2] -> Splus((translate prefix e1),(translate prefix e2)) - | "-", [e1;e2] -> Sminus((translate prefix e1),(translate prefix e2)) - | "*", [e1;e2] -> Sprod((translate prefix e1),(translate prefix e2)) + let e1 = translate_ext prefix e1 in + let sig_e = + begin match e2.Minils.w_desc with + | Minils.Wconst({se_desc = Sint(v)}) -> + op e1 (Sconst(Cint(v+modv))) + | _ -> + let e2 = translate_ext prefix e2 in + op (Sminus(e1,e2)) (Sconst(Cint(modv))) + end in + (* a_inf and a_sup : +1 to translate ideals to boolean + polynomials *) + Splus(sig_e,Sconst(Ctrue)) + | "+", [e1;e2] -> Splus((translate_ext prefix e1), + (translate_ext prefix e2)) + | "-", [e1;e2] -> Sminus((translate_ext prefix e1), + (translate_ext prefix e2)) + | "*", [e1;e2] -> Sprod((translate_ext prefix e1), + (translate_ext prefix e2)) | ("=" | "<>"),_ -> failwith("Sigali: '=' or '<>' not yet implemented") | _ -> assert false end - | Minils.Ewhen(e, c, var) when ((actual_ty e.Minils.e_ty) = Tbool) -> - let e = translate prefix e in - Swhen(e, - match (shortname c) with - "true" -> Svar(prefix ^ (name var)) - | "false" -> Snot(Svar(prefix ^ (name var))) - | _ -> assert false) - | Minils.Ewhen(e, _c, _var) -> - translate prefix e | Minils.Emerge(ck,[(c1,e1);(_c2,e2)]) -> - let e1 = translate prefix e1 in - let e2 = translate prefix e2 in + let e1 = translate_ext prefix e1 in + let e2 = translate_ext prefix e2 in let e1,e2 = begin match (shortname c1) with @@ -170,7 +182,7 @@ let rec translate_eq env f (Slist[Sequal(Svar(sn),Sconst(c))]))::acc_eqs, c::acc_init in - let e_next = translate prefix e in + let e_next = translate_ext prefix e in let e_next = translate_ck prefix e_next ck in acc_dep, sn::acc_states, @@ -254,7 +266,7 @@ let rec translate_eq env f prefixed (s_prefix ^ s)) g_p.proc_states in let e_states = List.map (fun hq -> Svar(hq)) new_states_list in - let e_list = List.map (translate prefix) e_list in + let e_list = List.map (translate_ext prefix) e_list in let e_outputs,acc_inputs = match inlined with | true -> [],acc_inputs @@ -414,7 +426,7 @@ let rec translate_eq env f prefixed (s_prefix ^ s)) g_p.proc_states in let e_states = List.map (fun hq -> Svar(hq)) new_states_list in - let e_list = List.map (translate prefix) e_list in + let e_list = List.map (translate_ext prefix) e_list in let e_outputs,acc_inputs = match inlined with | true -> [],acc_inputs @@ -651,11 +663,14 @@ let translate_node env let program p = let _env,acc_proc = List.fold_left - (fun (env,acc) node -> - let env,(proc,contract) = translate_node env node in - env,contract::proc::acc) + (fun (env,acc) p_desc -> + match p_desc with + | Minils.Pnode(node) -> + let env,(proc,contract) = translate_node env node in + env,contract::proc::acc + | _ -> env,acc) (NamesEnv.empty,[]) - p.Minils.p_nodes in + p.Minils.p_desc in let procs = List.rev acc_proc in let filename = filename_of_name (modul_to_string p.Minils.p_modname) in let dirname = build_path (filename ^ "_z3z") in From 2c4be9d42cc974b8bc2eb7c146929864537e5b48 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Gwena=EBl=20Delaval?= Date: Wed, 27 Jul 2011 16:13:45 +0200 Subject: [PATCH 12/12] Correct scoping and typing with contracts --- compiler/heptagon/analysis/typing.ml | 6 ++--- compiler/heptagon/hept_printer.ml | 2 +- compiler/heptagon/parsing/hept_scoping.ml | 24 +++++++++++-------- .../heptagon/transformations/normalize.ml | 18 +++++++++++++- compiler/main/mls2obc.ml | 10 +++++--- .../minils/transformations/normalize_mem.ml | 6 ++++- 6 files changed, 47 insertions(+), 19 deletions(-) diff --git a/compiler/heptagon/analysis/typing.ml b/compiler/heptagon/analysis/typing.ml index fbd3854..8af8f7d 100644 --- a/compiler/heptagon/analysis/typing.ml +++ b/compiler/heptagon/analysis/typing.ml @@ -1025,14 +1025,14 @@ let typing_contract const_env h contract = c_assume = e_a; c_enforce = e_g; c_controllables = c }) -> - let typed_b, defined_names, _ = typing_block const_env h b in + let typed_b, defined_names, h' = typing_block const_env h b in (* check that the equations do not define other unexpected names *) included_env defined_names Env.empty; (* assumption *) - let typed_e_a = expect const_env h (Tid Initial.pbool) e_a in + let typed_e_a = expect const_env h' (Tid Initial.pbool) e_a in (* property *) - let typed_e_g = expect const_env h (Tid Initial.pbool) e_g in + 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 diff --git a/compiler/heptagon/hept_printer.ml b/compiler/heptagon/hept_printer.ml index bd324ec..23e4d60 100644 --- a/compiler/heptagon/hept_printer.ml +++ b/compiler/heptagon/hept_printer.ml @@ -270,7 +270,7 @@ let rec print_type_def ff { t_name = name; t_desc = tdesc } = let print_contract ff { c_block = b; c_assume = e_a; c_enforce = e_g; c_controllables = c} = - fprintf ff "@[contract@\n%a@ assume %a@ enforce %a@ with (%a)@]" + fprintf ff "@[contract@\n%a@ assume %a@ enforce %a@ with (%a)@\n@]" print_block b print_exp e_a print_exp e_g diff --git a/compiler/heptagon/parsing/hept_scoping.ml b/compiler/heptagon/parsing/hept_scoping.ml index d039d84..6eaa2f1 100644 --- a/compiler/heptagon/parsing/hept_scoping.ml +++ b/compiler/heptagon/parsing/hept_scoping.ml @@ -371,12 +371,17 @@ and translate_last = function | Last (None) -> Heptagon.Last None | Last (Some e) -> Heptagon.Last (Some (expect_static_exp e)) -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_block = b } +let translate_contract env opt_ct = + match opt_ct with + | None -> None, env + | Some ct -> + let env' = Rename.append env ct.c_controllables in + let b, env = translate_block env ct.c_block in + Some + { 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_block = b }, env' let params_of_var_decs = List.map (fun vd -> Signature.mk_param @@ -396,10 +401,9 @@ let translate_node node = let params = params_of_var_decs node.n_params in let inputs = translate_vd_list env0 node.n_input in let outputs = translate_vd_list env0 node.n_output in - let b, env = translate_block env0 node.n_block in - let contract = - Misc.optional (translate_contract env) node.n_contract in - (* the env of the block is used in the contract translation *) + (* Enrich env with controllable variables (used in block) *) + let contract, env = translate_contract env0 node.n_contract in + let b, _ = translate_block env node.n_block 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/normalize.ml b/compiler/heptagon/transformations/normalize.ml index 57a5b61..439c756 100644 --- a/compiler/heptagon/transformations/normalize.ml +++ b/compiler/heptagon/transformations/normalize.ml @@ -284,7 +284,23 @@ let block funs _ b = let _, (v_acc, eq_acc) = Hept_mapfold.block funs ([],[]) b in { b with b_local = v_acc@b.b_local; b_equs = eq_acc}, ([], []) +let contract funs context c = + let ({ c_block = b } as c), void_context = + Hept_mapfold.contract funs context c in + (* Non-void context could mean lost equations *) + assert (void_context=([],[])); + let context, e_a = translate Any ([],[]) c.c_assume in + let context, e_e = translate Any context c.c_enforce in + let (d_list, eq_list) = context in + { c with + c_assume = e_a; + c_enforce = e_e; + c_block = { b with + b_local = d_list@b.b_local; + b_equs = eq_list@b.b_equs; } + }, void_context + let program p = - let funs = { defaults with block = block; eq = eq } in + let funs = { defaults with block = block; eq = eq; contract = contract } in let p, _ = Hept_mapfold.program funs ([], []) p in p diff --git a/compiler/main/mls2obc.ml b/compiler/main/mls2obc.ml index 85bad7d..7371083 100644 --- a/compiler/main/mls2obc.ml +++ b/compiler/main/mls2obc.ml @@ -585,12 +585,12 @@ let translate_contract map mem_var_tys = (** Returns a map, mapping variables names to the variables where they will be stored. *) -let subst_map inputs outputs locals mem_tys = +let subst_map inputs outputs controllables c_locals locals mem_tys = (* Create a map that simply maps each var to itself *) let map = List.fold_left (fun m { Minils.v_ident = x; Minils.v_type = ty } -> Env.add x (mk_pattern ty (Lvar x)) m) - Env.empty (inputs @ outputs @ locals) + Env.empty (inputs @ outputs @ controllables @ c_locals @ locals) in List.fold_left (fun map (x, x_ty) -> Env.add x (mk_pattern x_ty (Lmem x)) map) map mem_tys @@ -601,7 +601,11 @@ let translate_node } as n) = Idents.enter_node f; let mem_var_tys = Mls_utils.node_memory_vars n in - let subst_map = subst_map i_list o_list d_list mem_var_tys in + let c_list, c_locals = + match contract with + | None -> [], [] + | Some c -> c.Minils.c_controllables, c.Minils.c_local in + let subst_map = subst_map i_list o_list c_list c_locals d_list mem_var_tys in let (v, si, j, s_list) = translate_eq_list subst_map empty_call_context eq_list in let (si', j', s_list', d_list') = translate_contract subst_map mem_var_tys contract in let i_list = translate_var_dec i_list in diff --git a/compiler/minils/transformations/normalize_mem.ml b/compiler/minils/transformations/normalize_mem.ml index be05fc2..a67db4f 100644 --- a/compiler/minils/transformations/normalize_mem.ml +++ b/compiler/minils/transformations/normalize_mem.ml @@ -24,11 +24,15 @@ let eq _ (v, eqs) eq = match eq.eq_lhs, eq.eq_rhs.e_desc with | _, _ -> eq, (v, eq::eqs) +(* Leave contract unchanged (no output defined in it) *) +let contract funs acc c = c, acc + let node funs acc nd = let nd, (v, eqs) = Mls_mapfold.node_dec funs (nd.n_local, []) nd in { nd with n_local = v; n_equs = eqs }, acc let program p = - let funs = { Mls_mapfold.defaults with eq = eq; node_dec = node } in + let funs = { Mls_mapfold.defaults with + eq = eq; node_dec = node; contract = contract } in let p, _ = Mls_mapfold.program_it funs ([], []) p in p