diff --git a/compiler/global/clocks.ml b/compiler/global/clocks.ml index 523d33a..58e237f 100644 --- a/compiler/global/clocks.ml +++ b/compiler/global/clocks.ml @@ -134,7 +134,7 @@ let rec last_clock ct = match ct with E.g. .... on C1(x) and .... on C2(x) are. *) let same_control ck1 ck2 = match ck_repr ck1, ck_repr ck2 with | Cbase, Cbase -> true - | Con(_,_,x1), Con(_,_,x2) -> x1 = x2 + | Con(_,_,x1), Con(_,_,x2) -> x1 = x2 | Cvar {contents = Cindex i1}, Cvar {contents = Cindex i2} -> i1 = i2 | _ -> false diff --git a/compiler/heptagon/analysis/hept_clocking.ml b/compiler/heptagon/analysis/hept_clocking.ml index b9f0bfc..3683d1a 100644 --- a/compiler/heptagon/analysis/hept_clocking.ml +++ b/compiler/heptagon/analysis/hept_clocking.ml @@ -73,17 +73,17 @@ let ident_list_of_pat pat = let rec typing h pat e = let ct,base = match e.e_desc with | Econst _ -> - let ck = fresh_clock() in - Ck ck, ck + let ck = fresh_clock() in + Ck ck, ck | Evar x -> - let ck = ck_of_name h x in - Ck ck, ck + let ck = ck_of_name h x in + Ck ck, ck | Efby (e1, e2) -> let ct,ck = typing h pat e1 in - expect h pat ct e2; + expect h pat ct e2; ct, ck | Epre(_,e) -> - typing h pat e + typing h pat e | Ewhen (e,c,n) -> let ck_n = ck_of_name h n in let base = expect h pat (skeleton ck_n e.e_ty) e in @@ -108,27 +108,27 @@ let rec typing h pat e = | Imapi -> (* clocking the node with the extra i input on [ck_r] *) let il (* stubs i as 0 *) = List.map (fun x -> mk_exp - (Econst (Initial.mk_static_int 0)) - ~ct_annot:(Some(Ck(base_ck))) - Initial.tint + (Econst (Initial.mk_static_int 0)) + ~ct_annot:(Some(Ck(base_ck))) + Initial.tint ~linearity:Linearity.Ltop - ) nl + ) nl in typing_app h base_ck pat op (pargs@args@il) | Ifold | Imapfold -> (* clocking node with equality constaint on last input and last output *) let ct = typing_app h base_ck pat op (pargs@args) in - Misc.optional (unify (Ck(Clocks.last_clock ct))) - (Misc.last_element args).e_ct_annot; + Misc.optional (unify (Ck(Clocks.last_clock ct))) + (Misc.last_element args).e_ct_annot; ct | Ifoldi -> (* clocking the node with the extra i and last in/out constraints *) let il (* stubs i as 0 *) = List.map (fun x -> mk_exp - (Econst (Initial.mk_static_int 0)) - ~ct_annot:(Some(Ck(base_ck))) - Initial.tint + (Econst (Initial.mk_static_int 0)) + ~ct_annot:(Some(Ck(base_ck))) + Initial.tint ~linearity:Linearity.Ltop - ) nl + ) nl in let rec insert_i args = match args with | [] -> il @@ -137,7 +137,7 @@ let rec typing h pat e = in let ct = typing_app h base_ck pat op (pargs@(insert_i args)) in Misc.optional (unify (Ck (Clocks.last_clock ct))) - (Misc.last_element args).e_ct_annot; + (Misc.last_element args).e_ct_annot; ct in ct, base_ck @@ -147,10 +147,10 @@ let rec typing h pat e = None -> () | Some e_ct -> try - unify ct e_ct + unify ct e_ct with Unify -> - eprintf "Incoherent clock annotation.@\n"; - error_message e.e_loc (Etypeclash (ct,e_ct)); + eprintf "Incoherent clock annotation.@\n"; + error_message e.e_loc (Etypeclash (ct,e_ct)); end; e.e_ct_annot <- Some(ct); ct, base @@ -177,8 +177,8 @@ and typing_app h base pat op e_list = match op with | None -> build_env a_l v_l env | Some n -> build_env a_l v_l ((n,v)::env)) | _ -> - Printf.printf "Fun/node : %s\n" (Names.fullname f); - Misc.internal_error "Clocking, non matching signature" + Printf.printf "Fun/node : %s\n" (Names.fullname f); + Misc.internal_error "Clocking, non matching signature" in let env_pat = build_env node.node_outputs pat_id_list [] in let env_args = build_env node.node_inputs e_list [] in @@ -200,8 +200,8 @@ and typing_app h base pat op e_list = match op with Clocks.Con (sigck_to_ck sck, c, id) in List.iter2 - (fun a e -> expect h pat (Ck(sigck_to_ck a.a_clock)) e) - node.node_inputs e_list; + (fun a e -> expect h pat (Ck(sigck_to_ck a.a_clock)) e) + node.node_inputs e_list; Clocks.prod (List.map (fun a -> sigck_to_ck a.a_clock) node.node_outputs) let append_env h vds = @@ -214,8 +214,8 @@ let rec typing_eq h ({ eq_desc = desc; eq_loc = loc } as eq) = let pat_ct = typing_pat h pat in (try unify ct pat_ct with Unify -> - eprintf "Incoherent clock between right and left side of the equation.@\n"; - error_message loc (Etypeclash (ct, pat_ct))) + eprintf "Incoherent clock between right and left side of the equation.@\n"; + error_message loc (Etypeclash (ct, pat_ct))) | Eblock b -> ignore(typing_block h b) | _ -> assert false diff --git a/compiler/heptagon/transformations/boolean.ml b/compiler/heptagon/transformations/boolean.ml index c4c624c..3d59f59 100644 --- a/compiler/heptagon/transformations/boolean.ml +++ b/compiler/heptagon/transformations/boolean.ml @@ -184,8 +184,8 @@ let print_enum_types () = (fun t ti () -> match ti with | Enum info -> - Printf.printf "type %s :\n" (fullname t); - print_enuminfo info + Printf.printf "type %s :\n" (fullname t); + print_enuminfo info | _ -> () ) !enum_types () *) @@ -198,9 +198,9 @@ 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 + 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) @@ -213,8 +213,8 @@ let rec var_list clist = | [] -> (0,QualEnv.empty,Node(None)) | [c] -> (1, QualEnv.add c [false] QualEnv.empty, Tree(Node(Some c),Node(None))) | [c1;c2] -> (1, - QualEnv.add c1 [false] (QualEnv.add c2 [true] QualEnv.empty), - Tree(Node(Some c1),Node(Some c2))) + QualEnv.add c1 [false] (QualEnv.add c2 [true] QualEnv.empty), + Tree(Node(Some c1),Node(Some c2))) | l -> let n = List.length l in let n1 = n asr 1 in @@ -226,27 +226,27 @@ let rec var_list clist = (* 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 *) +(* 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 *) +(* 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 (true::l) m) vl2 - (QualEnv.fold - (if nv1 = nv2 - then (fun c l m -> QualEnv.add c (false::l) m) - else (fun c l m -> QualEnv.add c (false::false::l) m)) - vl1 - QualEnv.empty) in + QualEnv.fold (fun c l m -> QualEnv.add c (true::l) m) vl2 + (QualEnv.fold + (if nv1 = nv2 + then (fun c l m -> QualEnv.add c (false::l) m) + else (fun c l m -> QualEnv.add c (false::false::l) m)) + vl1 + QualEnv.empty) in let t1 = if nv1 = nv2 then t1 else Tree(t1,Node(None)) in let t = Tree(t1,t2) in nv2 + 1, vl, t @@ -255,24 +255,24 @@ let nvar_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 + 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 + 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 @@ -281,18 +281,18 @@ let translate_ty 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 = nvar_list "" n in - Tprod(List.map (fun _ -> ty_bool) strlist) - end - with Not_found -> ty - end + 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 = 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 @@ -315,13 +315,13 @@ let rec translate_ck env 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 -> - (* Boolean clock *) - Con(ck,c,n) + 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 -> + (* Boolean clock *) + Con(ck,c,n) end let rec translate_ct env ct = @@ -334,27 +334,27 @@ let translate_const c ty e = | _, 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) + 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) @@ -362,10 +362,10 @@ 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 ~linearity:Linearity.Ltop) :: d_list in - varl acc d_list (n-1) in + let v = fresh "bool" in + let acc = v :: acc in + let d_list = (mk_var_dec ~clock:ck v ty ~linearity:Linearity.Ltop) :: d_list in + varl acc d_list (n-1) in varl [] d_list n let assert_ck = function @@ -397,8 +397,8 @@ let rec when_list e bl vtree = let ck = assert_ck e.e_ct_annot in (* let e_v = mk_exp (Evar v) ~ct_annot:(Some(Ck(ck))) ty_bool in *) let e_when = { e with - e_ct_annot = Some (Ck(Con(ck,c,v))); - e_desc = Ewhen(e,c,v) } in + e_ct_annot = Some (Ck(Con(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") @@ -406,20 +406,20 @@ let rec when_ck desc li ty ck = match ck with | Cbase | Cvar _ -> { e_desc = desc; - e_level_ck = ck; - e_ct_annot = Some(Ck(ck)); - e_linearity = li; - e_ty = ty; - e_loc = no_location } + e_level_ck = ck; + e_ct_annot = Some(Ck(ck)); + e_linearity = li; + e_ty = ty; + e_loc = no_location } | Con(ck',c,v) -> let e = when_ck desc li ty ck' in (* let e_v = mk_exp (Evar v) ~ct_annot:(Some(Ck(ck'))) ty_bool in *) { e_desc = Ewhen(e,c,v); - e_level_ck = ck; - e_ct_annot = Some(Ck(ck)); - e_linearity = li; - e_ty = ty; - e_loc = no_location } + e_level_ck = ck; + e_ct_annot = Some(Ck(ck)); + e_linearity = li; + e_ty = ty; + e_loc = no_location } let rec base_value ck li ty = match ty with @@ -431,59 +431,59 @@ let rec base_value ck li ty = when_ck (Econst(strue)) li 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 li aty - | Type(Type_enum(l)) -> - when_ck - (Econst(mk_static_exp ty (Sconstructor(List.hd l)))) - li ty ck - | Type(Type_struct(l)) -> - let fields = - List.map - (fun {f_name = name; f_type = ty} -> - name,(base_value ck li ty)) - l in - when_ck (Estruct(fields)) li ty ck - | Enum { ty_nb_var = 1 } -> - when_ck (Econst(strue)) li ty_bool ck - | Enum { ty_nb_var = n } -> - let e = when_ck (Econst(strue)) li 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_level_ck = Cbase; - e_ct_annot = Some(Ck(ck)); - e_linearity = li; - e_loc = no_location } - end - with Not_found -> - Printf.printf "Name : %s\n" sname.name; assert false + 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 li aty + | Type(Type_enum(l)) -> + when_ck + (Econst(mk_static_exp ty (Sconstructor(List.hd l)))) + li ty ck + | Type(Type_struct(l)) -> + let fields = + List.map + (fun {f_name = name; f_type = ty} -> + name,(base_value ck li ty)) + l in + when_ck (Estruct(fields)) li ty ck + | Enum { ty_nb_var = 1 } -> + when_ck (Econst(strue)) li ty_bool ck + | Enum { ty_nb_var = n } -> + let e = when_ck (Econst(strue)) li 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_level_ck = Cbase; + e_ct_annot = Some(Ck(ck)); + e_linearity = li; + 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 li) ty_list in { e_desc = mk_tuple e_list; - e_ty = Tprod(List.map (fun e -> e.e_ty) e_list); - e_level_ck = Cbase; - e_ct_annot = Some(Ck(ck)); - e_linearity = li; - e_loc = no_location; + e_ty = Tprod(List.map (fun e -> e.e_ty) e_list); + e_level_ck = Cbase; + e_ct_annot = Some(Ck(ck)); + e_linearity = li; + e_loc = no_location; } | Tarray(ty,se) -> let e = base_value ck li ty in { e_desc = Eapp((mk_app ~params:[se] Earray_fill), [e], None); - e_ty = Tarray(e.e_ty,se); - e_level_ck = Cbase; - e_ct_annot = Some(Ck(ck)); - e_linearity = li; - e_loc = no_location; + e_ty = Tarray(e.e_ty,se); + e_level_ck = Cbase; + e_ct_annot = Some(Ck(ck)); + e_linearity = li; + e_loc = no_location; } | Tinvalid -> failwith("Boolean: invalid type") @@ -499,11 +499,11 @@ let rec merge_tree ck ty li e_map btree vtree = in (* let e_v = mk_exp (Evar v) ~ct_annot:(Some(Ck(ck))) ty_bool in *) { e_desc = Emerge(v,[(cfalse,e1);(ctrue,e2)]); - e_ty = ty; - e_level_ck = Cbase; - e_ct_annot = Some(Ck(ck)); - e_linearity = li; - e_loc = no_location } + e_ty = ty; + e_level_ck = Cbase; + e_ct_annot = Some(Ck(ck)); + e_linearity = li; + e_loc = no_location } | Tree (_,_), Vempty -> failwith("merge_tree: non-coherent trees") @@ -512,121 +512,121 @@ let rec translate env context ({e_desc = desc; e_ty = ty; e_ct_annot = ct} as e) let context,desc = match desc with | Econst(c) -> - context, translate_const c ty e + 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_ct_annot = ct; - e_desc = Evar(v); }) - ident_list) - with Not_found -> Evar(name) - end in - context,desc + 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_ct_annot = ct; + e_desc = Evar(v); }) + ident_list) + with Not_found -> Evar(name) + end in + context,desc | Efby(e1,e2) -> - let context,e1 = translate env context e1 in - let context,e2 = translate env context e2 in - context,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,Epre(None,e) + let context,e = translate env context e in + 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,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 - | { 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 = Epre(Some c,e)}) - c_l e_l) - | _ -> assert false - end + 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,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 + | { 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 = 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) + 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 + 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,l) (* of name * (longname * exp) list *) -> - begin - try - 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 (assert_ck ct) ty e.e_linearity 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,l) - end + begin + try + 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 (assert_ck ct) ty e.e_linearity 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,l) + end | Esplit(e1,e2) -> - let context,e1 = translate env context e1 in - let context,e2 = translate env context e2 in - context,Esplit(e1,e2) + let context,e1 = translate env context e1 in + let context,e2 = translate env context e2 in + context,Esplit(e1,e2) | 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) + 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,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,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,pe_list,e_list,r) | Elast _ -> - failwith("Boolean: not supported expression (abstract tree should be normalized)") + 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 = ct} + e_desc = desc; + e_ty = translate_ty ty; + e_ct_annot = ct} 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)) + let context,e = translate env context e in + (context,e::acc_e)) (context,[]) e_list in context,List.rev acc_e @@ -644,22 +644,22 @@ let var_dec_list (acc_vd,acc_loc,acc_eq) var_from n = let rec when_ck ckvar_list ck var = match ckvar_list,ck with | [], _ -> - { e_desc = Evar(var); - e_level_ck = ck; - e_ct_annot = Some(Ck(ck)); - e_ty = ty_bool; - e_linearity = var_from.v_linearity; - e_loc = no_location } + { e_desc = Evar(var); + e_level_ck = ck; + e_ct_annot = Some(Ck(ck)); + e_ty = ty_bool; + e_linearity = var_from.v_linearity; + e_loc = no_location } | _ckvar::l, Con(ck',c,v) -> - (* assert v = _ckvar *) - let e = when_ck l ck' var in - (* let e_v = mk_exp (Evar v) ~ct_annot:(Some(Ck(ck'))) ty_bool in *) - { e_desc = Ewhen(e,c,v); - e_level_ck = ck; - e_ct_annot = Some(Ck(ck)); - e_ty = ty_bool; - e_linearity = var_from.v_linearity; - e_loc = no_location } + (* assert v = _ckvar *) + let e = when_ck l ck' var in + (* let e_v = mk_exp (Evar v) ~ct_annot:(Some(Ck(ck'))) ty_bool in *) + { e_desc = Ewhen(e,c,v); + e_level_ck = ck; + e_ct_annot = Some(Ck(ck)); + e_ty = ty_bool; + e_linearity = var_from.v_linearity; + e_loc = no_location } | _ -> failwith("when_ck: non coherent clock and var list") in @@ -671,13 +671,13 @@ let var_dec_list (acc_vd,acc_loc,acc_eq) var_from 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) + 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 @@ -691,59 +691,59 @@ let var_dec_list (acc_vd,acc_loc,acc_eq) var_from n = 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 + (* 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) + (* 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 = (name vi) ^ suffix in - (* Build ident from this name *) - let id = fresh v in - let acc_loc = { v_ident = id; - v_type = ty_bool; - v_linearity = var_from.v_linearity; - v_clock = ck; - v_last = Var; - v_loc = no_location } :: acc_loc in - (* vi_... = vi when ... when (True|False)(v1) *) - let acc_eq = - (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 = - 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) + (* Build name vi_(0|1)* *) + let v = (name vi) ^ suffix in + (* Build ident from this name *) + let id = fresh v in + let acc_loc = { v_ident = id; + v_type = ty_bool; + v_linearity = var_from.v_linearity; + v_clock = ck; + v_last = Var; + v_loc = no_location } :: acc_loc in + (* vi_... = vi when ... when (True|False)(v1) *) + let acc_eq = + (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 = + 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 @@ -758,34 +758,34 @@ let buildenv_var_dec (acc_vd,acc_loc,acc_eq,env) ({v_type = ty} as v) = 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 vi = { var_enum = info; - var_list = vl; - clocked_var = t } 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 + 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 vi = { var_enum = info; + var_list = vl; + clocked_var = t } 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 | Tinvalid -> failwith("Boolean: invalid type") @@ -799,7 +799,7 @@ let translate_var_dec_list env vlist = List.map (translate_var_dec env) vlist let rec translate_block env add_locals add_eqs ({ b_local = v; - b_equs = eq_list; } as b) = + 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 @@ -814,14 +814,14 @@ 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 + 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 + 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 @@ -835,29 +835,29 @@ let translate_contract env contract = match contract with | None -> None, env | Some { c_assume = e_a; - c_enforce = e_g; - c_controllables = cl; - c_block = b } -> + c_enforce = e_g; + 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 ({ b_local = v; - b_equs = eqs } as b), env' - = translate_block env cl_loc cl_eq b in + 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_block = { b with - b_local = d_list; - b_equs = eq_list }; - c_assume = e_a; - c_enforce = e_g; - c_controllables = cl }, + b_local = d_list; + b_equs = eq_list }; + c_assume = e_a; + c_enforce = e_g; + c_controllables = cl }, env let node ({ n_input = inputs; - n_output = outputs; - n_contract = contract; - n_block = b } as n) = + n_output = outputs; + n_contract = contract; + 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 @@ -879,15 +879,15 @@ 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 + 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 | _ -> () diff --git a/compiler/heptagon/transformations/boolean.mli b/compiler/heptagon/transformations/boolean.mli index c98bbd5..d3167a9 100644 --- a/compiler/heptagon/transformations/boolean.mli +++ b/compiler/heptagon/transformations/boolean.mli @@ -7,7 +7,7 @@ (* *) (****************************************************) -(* +(* Translate enumerated types (state variables) into boolean type t = A | B | C | D @@ -22,7 +22,7 @@ (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)) diff --git a/compiler/heptagon/transformations/normalize.ml b/compiler/heptagon/transformations/normalize.ml index 936fff0..f2e5e3a 100644 --- a/compiler/heptagon/transformations/normalize.ml +++ b/compiler/heptagon/transformations/normalize.ml @@ -237,21 +237,21 @@ and merge context e x c_e_list = let ty = (List.hd (List.hd e_lists)).e_ty in let lin = (List.hd (List.hd e_lists)).e_linearity in let rec build_c_e_list c_list e_lists = - match c_list, e_lists with - | [], [] -> [], [] - | c::c_l, (e::e_l)::e_ls -> - let c_e_list, e_lists = build_c_e_list c_l e_ls in - (c,e)::c_e_list, e_l::e_lists - | _ -> assert false in + match c_list, e_lists with + | [], [] -> [], [] + | c::c_l, (e::e_l)::e_ls -> + let c_e_list, e_lists = build_c_e_list c_l e_ls in + (c,e)::c_e_list, e_l::e_lists + | _ -> assert false in let rec build_merge_list c_list e_lists = - match e_lists with - [] -> assert false - | []::_ -> [] - | _ ::_ -> - let c_e_list, e_lists = build_c_e_list c_list e_lists in - let e_merge = mk_exp ~loc:e.e_loc (Emerge(x, c_e_list)) ty ~linearity:lin in - let e_merge_list = build_merge_list c_list e_lists in - e_merge::e_merge_list in + match e_lists with + [] -> assert false + | []::_ -> [] + | _ ::_ -> + let c_e_list, e_lists = build_c_e_list c_list e_lists in + let e_merge = mk_exp ~loc:e.e_loc (Emerge(x, c_e_list)) ty ~linearity:lin in + let e_merge_list = build_merge_list c_list e_lists in + e_merge::e_merge_list in build_merge_list c_list e_lists in let c_e_list, context = mapfold translate_tag context c_e_list in @@ -263,14 +263,14 @@ and merge context e x c_e_list = let e_lists = List.map (fun (_,e) -> e_to_e_list e) c_e_list in let e_lists, context = mapfold - (fun context e_list -> add_list context ExtValue e_list) - context e_lists in + (fun context e_list -> add_list context ExtValue e_list) + context e_lists in let e_list = mk_merge x c_list e_lists in context, { e with - e_desc = Eapp(mk_app Etuple, e_list, None) } + e_desc = Eapp(mk_app Etuple, e_list, None) } ) else context, { e with - e_desc = Emerge(x, c_e_list) } + e_desc = Emerge(x, c_e_list) } (* applies distribution rules *) (* [(p1,...,pn) = (e1,...,en)] into [p1 = e1;...;pn = en] *) @@ -332,8 +332,8 @@ let contract funs context c = 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; } + b_local = d_list@b.b_local; + b_equs = eq_list@b.b_equs; } }, void_context let program p = diff --git a/compiler/minils/sigali/sigali.ml b/compiler/minils/sigali/sigali.ml index 38c4ddb..adc3cfc 100644 --- a/compiler/minils/sigali/sigali.ml +++ b/compiler/minils/sigali/sigali.ml @@ -129,20 +129,20 @@ let 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 + | x :: l -> + print ff x; + fprintf ff "%s@ " sep; + print_list ff print sep l - let print_string ff s = + let print_string ff s = fprintf ff "%s" s - let print_name ff n = + let print_name ff n = fprintf ff "%s" n let print_const ff c = @@ -157,56 +157,56 @@ module Printer = | 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 + 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 + fprintf ff "(%a@ default %a)" + print_exp e1 + print_exp e2 | Sequal(e1,e2) -> - fprintf ff "(%a@ = %a)" - print_exp e1 - print_exp e2 + fprintf ff "(%a@ = %a)" + print_exp e1 + print_exp e2 | Ssquare(e) -> - fprintf ff "(%a^2)" - print_exp e + fprintf ff "(%a^2)" + print_exp e | Snot(e) -> - fprintf ff "(not %a)" - print_exp e + fprintf ff "(not %a)" + print_exp e | Sand(e1,e2) -> - fprintf ff "(%a@ and %a)" - print_exp e1 - print_exp 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 + 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 "@])" + 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 "]@]" + fprintf ff "[@["; + print_list ff print_exp "," e_l; + fprintf ff "]@]" | Splus(e1,e2) -> - fprintf ff "(%a@ + %a)" - print_exp e1 - print_exp e2 + fprintf ff "(%a@ + %a)" + print_exp e1 + print_exp e2 | Sminus(e1,e2) -> - fprintf ff "(%a@ - %a)" - print_exp e1 - print_exp e2 + fprintf ff "(%a@ - %a)" + print_exp e1 + print_exp e2 | Sprod(e1,e2) -> - fprintf ff "(%a@ * %a)" - print_exp e1 - print_exp 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 + print_name name + print_exp e let print_statements ff stmt_l = fprintf ff "@["; @@ -216,54 +216,51 @@ module Printer = 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 + 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 + 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 + 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 + 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 + 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_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; - }) = + 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 @@ -274,28 +271,28 @@ read(\"Orbite.lib\");\ (* declare dummy variables d1...dn *) fprintf ff "@[declare(@[d1"; for i = 2 to n do - fprintf ff ",@ d%d" i; + 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; + 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; @@ -304,10 +301,10 @@ read(\"Orbite.lib\");\ (* states decl. *) fprintf ff "states : [@["; if states = [] then - (* dummy state var to avoid sigali segfault *) - fprintf ff "d1" + (* dummy state var to avoid sigali segfault *) + fprintf ff "d1" else - print_list ff print_name "," states; + print_list ff print_name "," states; fprintf ff "@]];@,"; (* controllables : *) @@ -317,11 +314,11 @@ read(\"Orbite.lib\");\ (* init evolutions, initialisations *) if states = [] then - fprintf ff "evolutions : [d1];@," + fprintf ff "evolutions : [d1];@," else - fprintf ff "evolutions : [];@,"; + fprintf ff "evolutions : [];@,"; fprintf ff "initialisations : [];@,"; - + (* body statements *) print_statements ff body; @@ -336,91 +333,93 @@ read(\"Orbite.lib\");\ fprintf ff "@]] --- %%@,"; (* process declaration *) - fprintf ff - ("%s : processus(" ^^ - "@[conditions," ^^ - "@ states," ^^ - "@ evolutions," ^^ - "@ initialisations," ^^ - "@ [gen(constraints)]," ^^ - "@ controllables@]);@,") - name; + 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 + 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; @@ -432,4 +431,4 @@ read(\"Orbite.lib\");\ let print dir p_l = List.iter (print_processus dir) p_l end - + diff --git a/compiler/minils/sigali/sigalimain.ml b/compiler/minils/sigali/sigalimain.ml index 3c4a76b..f3e8b20 100644 --- a/compiler/minils/sigali/sigalimain.ml +++ b/compiler/minils/sigali/sigalimain.ml @@ -30,8 +30,8 @@ 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 + let acc = (prefix ^ (string_of_int n)) :: acc in + varl acc (n-1) in varl [] n let dummy_prefix = "d" @@ -46,7 +46,7 @@ let translate_static_exp se = Cint(-v) | _ -> Format.printf "Constant %a@\n" - Global_printer.print_static_exp se; + Global_printer.print_static_exp se; failwith("Sigali: untranslatable constant") @@ -62,32 +62,32 @@ let rec translate_ck pref e = function | 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) + match (shortname c) with + "true" -> Svar(pref ^ (name var)) + | "false" -> Snot(Svar(pref ^ (name var))) + | _ -> assert false) let rec translate_ext prefix ({ Minils.w_desc = desc; Minils.w_ty = ty } as e) = match desc with | 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 + 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.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) + 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 + translate_ext prefix e | Minils.Wfield(_) -> - failwith("Sigali: structures not implemented") + failwith("Sigali: structures not implemented") | Minils.Wreinit _ -> failwith("Sigali: reinit not implemented") (* [translate e = c] *) @@ -95,91 +95,91 @@ 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_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 - | "<=" -> a_inf,0 - | "<" -> a_inf,-1 - | ">=" -> a_sup,0 - | _ -> a_sup,1 - end in - 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.a_op = Minils.Efun({qual=Pervasives;name=n})}, + e_list, _) -> + begin + match n, e_list with + | "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 + | "<=" -> a_inf,0 + | "<" -> a_inf,-1 + | ">=" -> a_sup,0 + | _ -> a_sup,1 + end in + 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) + 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 + translate prefix e | Minils.Emerge(ck,[(c1,e1);(_c2,e2)]) -> - let e1 = translate_ext prefix e1 in - let e2 = translate_ext 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 + let e1 = translate_ext prefix e1 in + let e2 = translate_ext 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.Eapp({Minils.a_op = Minils.Eifthenelse},[e1;e2;e3],_) -> - let e1 = translate_ext prefix e1 in - let e2 = translate_ext prefix e2 in - let e3 = translate_ext prefix e3 in - begin match (actual_ty e.Minils.e_ty) with - | Tbool -> Sdefault(Swhen(e2,e1),e3) - | Tint -> a_part e1 (a_const (Sconst(Cint(0)))) e2 e3 - | Tother -> assert false - end + let e1 = translate_ext prefix e1 in + let e2 = translate_ext prefix e2 in + let e3 = translate_ext prefix e3 in + begin match (actual_ty e.Minils.e_ty) with + | Tbool -> Sdefault(Swhen(e2,e1),e3) + | Tint -> a_part e1 (a_const (Sconst(Cint(0)))) e2 e3 + | Tother -> assert false + end | Minils.Estruct(_) -> - failwith("Sigali: structures not implemented") + failwith("Sigali: structures not implemented") | Minils.Eiterator(_,_,_,_,_,_) -> - failwith("Sigali: iterators not implemented") + failwith("Sigali: iterators not implemented") | Minils.Eapp({Minils.a_op = Minils.Enode(_)},_,_) -> - failwith("Sigali: node in expressions; programs should be normalized") + failwith("Sigali: node in expressions; programs should be normalized") | Minils.Efby(_,_) -> - failwith("Sigali: fby in expressions; programs should be normalized") + failwith("Sigali: fby in expressions; programs should be normalized") | Minils.Eapp(_,_,_) -> - Format.printf "Application : %a@\n" - Mls_printer.print_exp e; - failwith("Sigali: not supported application") + Format.printf "Application : %a@\n" + Mls_printer.print_exp e; + failwith("Sigali: not supported application") | Minils.Emerge(_, _) -> assert false let rec translate_eq env f @@ -196,18 +196,18 @@ let rec translate_eq env f 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 *) +(* (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 + 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_ext prefix e in let e_next = translate_ck prefix e_next ck in @@ -215,46 +215,46 @@ let rec translate_eq env f sn::acc_states, acc_init,acc_inputs,acc_ctrl,acc_cont, (extend - evolutions - (Slist[Sdefault(e_next,Svar(sn))])) - (* TODO *) + evolutions + (Slist[Sdefault(e_next,Svar(sn))])) + (* TODO *) (* ::{ stmt_name = sn; *) -(* stmt_def = translate_ck prefix (Svar(sm)) ck } *) +(* 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) -> + 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) + 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 @@ -266,12 +266,12 @@ let rec translate_eq env f (* 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 + 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 + { 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 *) @@ -282,139 +282,139 @@ let rec translate_eq env f 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 + 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_ext 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 + 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 + { 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 + {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 + 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 + 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 + {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)) + (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 + (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 + (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 + (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 + 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 + {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 + (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) -> + 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) + 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 @@ -426,12 +426,12 @@ let rec translate_eq env f (* 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 + 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 + { 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 *) @@ -442,128 +442,128 @@ let rec translate_eq env f 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 + 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_ext 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 + 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 + { 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 + {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 + 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 + 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 + {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)) + (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 + (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 + (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 + (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 + 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 + {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 + (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 + 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 + 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 -> + 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) + env f + (acc_dep,acc_states,acc_init, + acc_inputs,acc_ctrl,acc_cont,acc_eqs) + eq) ([],[],[],[],[],[],[]) eq_list @@ -574,27 +574,27 @@ let translate_contract env f contract = match contract with | None -> let body = - [{ stmt_name = var_g; stmt_def = Sconst(Ctrue) }; - { stmt_name = var_a; stmt_def = Sconst(Ctrue) }] in + [{ 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} -> + 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 + controllables,_contracts,body = + translate_eq_list env f l_eqs in assert (inputs = []); assert (controllables = []); let e_a = translate_ext prefix e_a in let e_g = translate_ext prefix e_g in let body = - {stmt_name = var_g; stmt_def = e_g} :: - {stmt_name = var_a; stmt_def = e_a} :: - body in + {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 + List.map (fun { Minils.v_ident = id } -> prefix ^ (name id)) cl in dep,states,init,body,(Svar(var_a),Svar(var_g)),controllables @@ -640,16 +640,16 @@ let translate_node env 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 + 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 @@ -675,27 +675,27 @@ let translate_node env (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 + 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) p_desc -> - match p_desc with - | Minils.Pnode(node) -> - let env,(proc,contract) = translate_node env node in - env,contract::proc::acc - | _ -> env,acc) + 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_desc in let procs = List.rev acc_proc in diff --git a/test/good/threestates.ept b/test/good/threestates.ept index 20bf057..58498e7 100644 --- a/test/good/threestates.ept +++ b/test/good/threestates.ept @@ -3,28 +3,28 @@ let automaton state A do - y = 1; + y = 1; until (x = 0) then B state B do - y = 2; + y = 2; until (x = 1) then C state C do - automaton - state D - do - y = 3; - until (x = 2) then E - state E - do - y = 4; - until (x = 3) then F - state F - do - y = 5; - until (x = 4) then D - end + automaton + state D + do + y = 3; + until (x = 2) then E + state E + do + y = 4; + until (x = 3) then F + state F + do + y = 5; + until (x = 4) then D + end until (x = 5) then A end tel diff --git a/test/good/tt.ept b/test/good/tt.ept index e294c39..aaa3eb6 100644 --- a/test/good/tt.ept +++ b/test/good/tt.ept @@ -22,7 +22,7 @@ let o = false; until true then Cruise state Cruise do - o = true; + o = true; end tel *) diff --git a/test/image_filters/downscale.ept b/test/image_filters/downscale.ept index fd02a8e..65b2fc6 100644 --- a/test/image_filters/downscale.ept +++ b/test/image_filters/downscale.ept @@ -36,8 +36,8 @@ tel node mod_counter_r<>(res :bool) returns (cpt :int) let reset - cpt = (0 fby cpt) + 1 - every (res or (0 fby cpt = m)) + cpt = (0 fby cpt) + 1 + every (res or (0 fby cpt = m)) tel (* count from 1 to m included *) @@ -105,9 +105,9 @@ tel node down_img <> (x :pixel :: .) returns (y_flat :pixel; y_clock :bool; - y, y_dh, y_dh_t, y_dhv_t :pixel; + y, y_dh, y_dh_t, y_dhv_t :pixel; ck_y_dh, ck_y_dhv :bool - ) + ) var x_line, y_dh_t_line :bool; @@ -135,8 +135,8 @@ let tel*) node main<> () returns (img, out : pixel; ck_out :bool; - y, y_dh, y_dh_t, y_dhv_t :pixel; - ck_y_dh, ck_y_dhv :bool) + y, y_dh, y_dh_t, y_dhv_t :pixel; + ck_y_dh, ck_y_dhv :bool) (*var img : pixel;*) let (*ck_out = true fby false fby not ck_out;*) diff --git a/tools/enforce_style.sh b/tools/enforce_style.sh index 698b491..eaf3b61 100755 --- a/tools/enforce_style.sh +++ b/tools/enforce_style.sh @@ -1,2 +1,2 @@ #!/bin/sh -find . \! -path "*build*" -and \( -iname "*.ml" -or -iname "*.mli" -or -iname "*.mly" -or -iname "*.mll" -or -iname "*.ept" -or -iname "*.txt" \) -exec perl -pi -e 's/( |\t)+$//gi; s/\t/ /g' {} \; +find . \! -path "*build*" -and \( -iname "*.ml" -or -iname "*.mli" -or -iname "*.mly" -or -iname "*.mll" -or -iname "*.ept" -or -iname "*.txt" \) -exec perl -pi -e 's/( |\t)+$//gi; s/\t/ /g' {} \;