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

Enforce style : no tab, no trailing whitespace.

Browse Source
master
Léonard Gérard 13 years ago committed by Léonard Gérard
parent 3bc5824175
commit 646cfab82b
11 changed files with 975 additions and 976 deletions
Show Stats Download Patch File Download Diff File

2
compiler/global/clocks.ml
Unescape Escape View File

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

52
compiler/heptagon/analysis/hept_clocking.ml
Unescape Escape View File

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

740
compiler/heptagon/transformations/boolean.ml
Unescape Escape View File

@ -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
| _ -> ()

4
compiler/heptagon/transformations/boolean.mli
Unescape Escape View File

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

40
compiler/heptagon/transformations/normalize.ml
Unescape Escape View File

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

349
compiler/minils/sigali/sigali.ml
Unescape Escape View File

@ -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 "@[<hov 2>%a : %a;@]"
print_name name
print_exp e
print_name name
print_exp e
let print_statements ff stmt_l =
fprintf ff "@[<v>";
@ -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(@[<hov>d1";
for i = 2 to n do
fprintf ff ",@ d%d" i;
fprintf ff ",@ d%d" i;
done;
fprintf ff "@]);@]@\n@\n";
fprintf ff "@[<v>";
(* 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(@[<hov>";
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 "@[<v>";
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 "@[<v>";
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(@[<hov>";
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 "@[<v>";
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 "@[<v>";
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(@[<hov>";
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

716
compiler/minils/sigali/sigalimain.ml
Unescape Escape View File

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

32
test/good/threestates.ept
Unescape Escape View File

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

2
test/good/tt.ept
Unescape Escape View File

@ -22,7 +22,7 @@ let
o = false;
until true then Cruise
state Cruise do
o = true;
o = true;
end
tel
*)

12
test/image_filters/downscale.ept
Unescape Escape View File

@ -36,8 +36,8 @@ tel
node mod_counter_r<<m :int>>(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 <<size_x, size_y, ratio_x, ratio_y :int>> (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<<size_x, size_y:int>> () 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;*)

2
tools/enforce_style.sh
Unescape Escape View File

@ -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' {} \;

Write Preview
Loading…
Cancel
Save