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

Correction and simplification of the sigali pass

Browse source 
Added a "Contracts" pass, after inlining, taking care of the
contracts of the nodes called in the body of a node. This pass
"inlines" the code and assume/guarantee parts of these subcontracts.

The "Sigali" pass both generates the sigali ("z3z") code and add the call to
the controller (which is a node generated further by the sigali tool).
Therefore this pass has been included into the mls compiler, and removed
from the targets (a "z3z" dummy target has been kept for backward compatibility
reasons).
This commit is contained in:
Gwenal Delaval 2012-06-06 15:59:08 +02:00
parent 1e46c2a73c
commit 2956002f85
9 changed files with 408 additions and 458 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
compiler/global/initial.ml
View file

@ -19,6 +19,8 @@ let tbool = Types.Tid pbool
let ptrue = { qual = Pervasives; name = "true" }
let pfalse = { qual = Pervasives; name = "false" }
let por = { qual = Pervasives; name = "or" }
let pand = { qual = Pervasives; name = "&" }
let pnot = { qual = Pervasives; name = "not" }
let pint = { qual = Pervasives; name = "int" }
let tint = Types.Tid pint
let pfloat = { qual = Pervasives; name = "float" }

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

@ -24,6 +24,9 @@ let compile_program p =
(* Inlining *)
let p = pass "Inlining" true Inline.program p pp in
(* Contracts handling *)
let p = pass "Contracts" true Contracts.program p pp in
(* Causality check *)
let p = silent_pass "Causality check" !causality Causality.program p in

14
compiler/heptagon/transformations/boolean.ml
View file

@ -329,7 +329,7 @@ let rec translate_ct env ct =
| Ck(ck) -> Ck(translate_ck env ck)
| Cprod(l) -> Cprod(List.map (translate_ct env) l)
let translate_const c ty e =
let translate_const c ty ct e =
match c.se_desc,ty with
| _, Tid({ qual = Pervasives; name = "bool" }) -> Econst(c)
| Sconstructor(cname),Tid(tname) ->
@ -350,6 +350,7 @@ let translate_const c ty e =
(List.map
(fun b -> {e with
e_desc = b;
e_ct_annot = ct;
e_ty = ty_bool })
b_list)
end
@ -512,7 +513,7 @@ 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 ct e
| Evar(name) ->
let desc = begin
try
@ -538,7 +539,7 @@ let rec translate env context ({e_desc = desc; e_ty = ty; e_ct_annot = ct} as 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 e_c = translate_const c ty ct e in
let context,e = translate env context e in
begin
match e_c with
@ -772,12 +773,9 @@ let buildenv_var_dec (acc_vd,acc_loc,acc_eq,env) ({v_type = ty} as v) =
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
v.v_ident
{ var_enum = info;
var_list = vl;
clocked_var = t }
@ -846,7 +844,7 @@ let translate_contract env contract =
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_a_loc = translate env' (v,eqs) e_a_loc in
let context, e_a_loc = translate env' context e_a_loc in
let context, e_g = translate env' context e_g in
let context, e_g_loc = translate env' context e_g_loc in
let (d_list,eq_list) = context in

227
compiler/heptagon/transformations/contracts.ml Normal file
View file

@ -0,0 +1,227 @@
(**************************************************************************)
(* *)
(* Heptagon *)
(* *)
(* Author : Gwenaël Delaval *)
(* Organization : LIG, UJF *)
(* *)
(**************************************************************************)
(* Inline code in contracts, collect assume/guarantee of subnodes *)
(* To be done before "completion" and "switch" transformations *)
open Names
open Heptagon
open Hept_utils
open Hept_mapfold
open Initial
open Signature
open Types
open Linearity
(** v_acc is the new local vars which were in lower levels,
eq_acc contains all the equations *)
let fresh = Idents.gen_var "contracts"
let mk_unique_contract nd =
let mk_bind vd =
let id = fresh (Idents.name vd.v_ident) in
(vd.v_ident, { vd with v_ident = id; v_clock = Clocks.fresh_clock () }) in
let c_local =
match nd.n_contract with
None -> []
| Some { c_block = b } -> b.b_local in
let subst = List.map mk_bind (c_local @ nd.n_input @ nd.n_output) in
let subst_var_dec _ () vd = (List.assoc vd.v_ident subst, ()) in
let subst_edesc funs () ed =
let ed, () = Hept_mapfold.edesc funs () ed in
let find vn = (List.assoc vn subst).v_ident in
(match ed with
| Evar vn -> Evar (find vn)
| Elast vn -> Elast (find vn)
| Ewhen (e, cn, vn) -> Ewhen (e, cn, find vn)
| Emerge (vn, e_l) -> Emerge (find vn, e_l)
| _ -> ed), ()
in
let subst_eqdesc funs () eqd =
let (eqd, ()) = Hept_mapfold.eqdesc funs () eqd in
match eqd with
| Eeq (pat, e) ->
let rec subst_pat pat = match pat with
| Evarpat vn -> Evarpat (try (List.assoc vn subst).v_ident
with Not_found -> vn)
| Etuplepat patl -> Etuplepat (List.map subst_pat patl) in
(Eeq (subst_pat pat, e), ())
| _ -> raise Errors.Fallback in
let funs = { defaults with
var_dec = subst_var_dec;
eqdesc = subst_eqdesc;
edesc = subst_edesc; } in
fst (Hept_mapfold.node_dec funs () nd)
let exp funs (env, newvars, newequs, contracts) exp =
let exp, (env, newvars, newequs, contracts) =
Hept_mapfold.exp funs (env, newvars, newequs, contracts) exp in
match exp.e_desc with
| Eapp ({ a_op = (Enode nn | Efun nn); } as op, argl, rso) ->
begin try
let add_reset eq = match rso with
| None -> eq
| Some x -> mk_equation (Ereset (mk_block [eq], x)) in
let ni = mk_unique_contract (QualEnv.find nn env) in
let ci = match ni.n_contract with
None -> raise Not_found
| Some c -> c in
let static_subst =
List.combine (List.map (fun p -> (local_qn p.p_name)) ni.n_params)
op.a_params in
(* Perform [static_exp] substitution. *)
let ni =
let apply_sexp_subst_sexp funs () sexp = match sexp.se_desc with
| Svar s -> ((try List.assoc s static_subst
with Not_found -> sexp), ())
| _ -> Global_mapfold.static_exp funs () sexp in
let funs =
{ defaults with global_funs =
{ Global_mapfold.defaults with Global_mapfold.static_exp =
apply_sexp_subst_sexp; }; } in
fst (Hept_mapfold.node_dec funs () ni) in
(* equation "x = e" for inputs *)
let mk_input_equ vd e = mk_equation (Eeq (Evarpat vd.v_ident, e)) in
(* output expression "y" *)
let mk_output_exp vd = mk_exp (Evar vd.v_ident) vd.v_type ~linearity:vd.v_linearity in
(* equation "y = f(x)" *)
let eq_app =
let pat = match ni.n_output with
[o] -> Evarpat(o.v_ident)
| ol -> Etuplepat(List.map (fun o -> Evarpat(o.v_ident)) ol) in
let v_argl =
List.map
(fun vd -> mk_exp (Evar vd.v_ident) vd.v_type ~linearity:vd.v_linearity)
ni.n_input in
mk_equation (Eeq (pat, { exp with e_desc = Eapp (op, v_argl, rso) })) in
(* variables for assume and guarantee *)
let v_a = fresh ((shortname nn) ^ "_assume") in
let v_g = fresh ((shortname nn) ^ "_guarantee") in
(* equations for assume/guarantee *)
let eq_a = mk_equation (Eeq (Evarpat v_a, ci.c_assume)) in
let eq_g = mk_equation (Eeq (Evarpat v_g, ci.c_enforce)) in
let newvars = ni.n_input @ ci.c_block.b_local @ ni.n_output @ newvars
and newequs =
List.map2 mk_input_equ ni.n_input argl
@ List.map add_reset ci.c_block.b_equs
@ [ eq_app; eq_a; eq_g ]
@ newequs
and contracts = (v_a,v_g)::contracts in
(* For clocking reason we cannot create 1-tuples. *)
let res_e = match ni.n_output with
| [o] -> mk_output_exp o
| _ ->
mk_exp (Eapp ({ op with a_op = Etuple; },
List.map mk_output_exp ni.n_output, None)) exp.e_ty
~linearity:exp.e_linearity in
(res_e, (env, newvars, newequs, contracts))
with
| Not_found ->
exp, (env, newvars, newequs, contracts)
end
| _ -> exp, (env, newvars, newequs, contracts)
let block funs (env, newvars, newequs, contracts) blk =
let (blk, (env, newvars', newequs', contracts')) =
Hept_mapfold.block funs (env, [], [], contracts) blk in
({ blk with b_local = newvars' @ blk.b_local; b_equs = newequs' @ blk.b_equs; },
(env, newvars, newequs, contracts'))
let not_exp e = mk_exp (mk_op_app (Efun pnot) [e]) tbool ~linearity:Ltop
let (&&&) e1 e2 = mk_exp (mk_op_app (Efun pand) [e1;e2]) tbool ~linearity:Ltop
let (|||) e1 e2 = mk_exp (mk_op_app (Efun por) [e1;e2]) tbool ~linearity:Ltop
let (=>) e1 e2 = (not_exp e1) ||| e2
let var_exp v = mk_exp (Evar v) tbool ~linearity:Ltop
let true_exp = mk_exp (Econst (mk_static_bool true)) tbool ~linearity:Ltop
let mk_vd_bool v = mk_var_dec ~last:(Last (Some (mk_static_bool true))) v tbool ~linearity:Ltop
let node_dec funs (env, newvars, newequs, contracts) nd =
let nd, (env, newvars, newequs, contracts) =
Hept_mapfold.node_dec funs (env, newvars, newequs, contracts) nd in
(* Build assume and guarantee parts from contract list (list of
ident pairs (v_a,v_g)). Returns also a list of variable
declarations. *)
let rec build_contract contracts =
match contracts with
[] -> true_exp, true_exp, []
| [(v_a,v_g)] ->
let e_a = var_exp v_a in
let e_g = var_exp v_g in
(* assume part : e_a => e_g ; guarantee part : e_a *)
(e_a => e_g), e_a, [mk_vd_bool v_a; mk_vd_bool v_g]
| (v_a,v_g)::l ->
let e_a_l,e_g_l,vd_l = build_contract l in
let e_a = var_exp v_a in
let e_g = var_exp v_g in
((e_a => e_g) &&& e_a_l), (e_a &&& e_g_l),
((mk_vd_bool v_a) :: (mk_vd_bool v_g) :: vd_l)
in
let assume_loc, enforce_loc, vd_contracts = build_contract contracts in
let nc =
match nd.n_contract, contracts with
c,[] -> c
| None,_::_ ->
Some { c_assume = true_exp;
c_enforce = true_exp;
c_assume_loc = assume_loc;
c_enforce_loc = enforce_loc;
c_controllables = [];
c_block = mk_block ~stateful:false [] }
| Some c,_::_ ->
Some { c with
c_assume_loc = assume_loc;
c_enforce_loc = enforce_loc } in
let nd =
{ nd with
n_contract = nc;
n_block =
{ nd.n_block with
b_local = newvars @ vd_contracts @ nd.n_block.b_local;
b_equs = newequs @ nd.n_block.b_equs } } in
let env = QualEnv.add nd.n_name nd env in
nd, (env, [], [], [])
let program p =
let funs =
{ defaults with exp = exp; block = block; node_dec = node_dec; eq = eq; } in
let (p, (_, newvars, newequs, contracts)) =
Hept_mapfold.program funs (QualEnv.empty, [], [], []) p in
assert (newvars = []);
assert (newequs = []);
assert (contracts = []);
p

4
compiler/main/hept2mls.ml
View file

@ -101,8 +101,8 @@ let rec translate_extvalue e =
match e.Heptagon.e_desc with
| Heptagon.Econst c -> mk_extvalue e (Wconst c)
| Heptagon.Evar x -> mk_extvalue e (Wvar x)
| Heptagon.Ewhen (e, c, x) ->
mk_extvalue e (Wwhen (translate_extvalue e, c, x))
| Heptagon.Ewhen (e', c, x) ->
mk_extvalue e (Wwhen (translate_extvalue e', c, x))
| Heptagon.Eapp({ Heptagon.a_op = Heptagon.Efield;
Heptagon.a_params = params }, e_list, _) ->
let e = assert_1 e_list in

2
compiler/main/mls2seq.ml
View file

@ -62,7 +62,7 @@ let java_conf () =
let targets =
[ mk_target ~interface:(IObc Cmain.interface) "c" (Obc_no_params Cmain.program);
mk_target ~load_conf:java_conf "java" (Obc Java_main.program);
mk_target "z3z" (Minils_no_params Sigalimain.program);
mk_target "z3z" (Minils_no_params ignore);
mk_target "obc" (Obc write_obc_file);
mk_target "obc_np" (Obc_no_params write_obc_file);
mk_target "epo" (Minils write_object_file) ]

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

@ -52,6 +52,17 @@ let compile_program p =
pass "Scheduling" true Schedule.program p pp
in
let z3z = List.mem "z3z" !target_languages in
let p = pass "Sigali generation" z3z Sigalimain.program p pp in
(* Re-scheduling after sigali generation *)
let p =
if not !Compiler_options.use_old_scheduler then
pass "Scheduling (with minimization of interferences)" z3z Schedule_interf.program p pp
else
pass "Scheduling" z3z Schedule.program p pp
in
(* Memory allocation *)
let p = pass "Memory allocation" !do_mem_alloc Interference.program p pp in

601
compiler/minils/sigali/sigalimain.ml
View file

@ -40,8 +40,12 @@ let translate_static_exp se =
match se.se_desc with
| Sint(v) -> Cint(v)
| Sfloat(_) -> failwith("Sigali: floats not implemented")
| Sbool(true) -> Ctrue
| Sbool(false) -> Cfalse
| Sbool(true)
| Sconstructor { qual = Pervasives; name = "true" }
-> Ctrue
| Sbool(false)
| Sconstructor { qual = Pervasives; name = "false" }
-> Cfalse
| Sop({ qual = Pervasives; name = "~-" },[{se_desc = Sint(v)}]) ->
Cint(-v)
| _ ->
@ -51,7 +55,7 @@ let translate_static_exp se =
let rec translate_pat = function
| Minils.Evarpat(x) -> [name x]
| Minils.Evarpat(x) -> [x]
| Minils.Etuplepat(pat_list) ->
List.fold_right (fun pat acc -> (translate_pat pat) @ acc) pat_list []
@ -68,7 +72,7 @@ let rec translate_ck pref e = function
| _ -> assert false)
let rec translate_ext prefix ({ Minils.w_desc = desc; Minils.w_ty = ty } as e) =
let rec translate_ext prefix ({ Minils.w_desc = desc; Minils.w_ty = ty }) =
match desc with
| Minils.Wconst(v) ->
begin match (actual_ty ty) with
@ -77,13 +81,15 @@ let rec translate_ext prefix ({ Minils.w_desc = desc; Minils.w_ty = ty } as e) =
| 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)
(* TODO remove if this works without *)
(* | Minils.Wwhen(e, c, var) when ((actual_ty e.Minils.w_ty) = Tbool) -> *)
(* let e = translate_ext prefix e in *)
(* Swhen(e, *)
(* match (shortname c) with *)
(* "true" -> Svar(prefix ^ (name var)) *)
(* | "false" -> Snot(Svar(prefix ^ (name var))) *)
(* | _ -> assert false) *)
| Minils.Wwhen(e, _c, _var) ->
translate_ext prefix e
| Minils.Wfield(_) ->
@ -91,7 +97,7 @@ let rec translate_ext prefix ({ Minils.w_desc = desc; Minils.w_ty = ty } as e) =
| Minils.Wreinit _ -> failwith("Sigali: reinit not implemented")
(* [translate e = c] *)
let rec translate prefix ({ Minils.e_desc = desc; Minils.e_ty = ty } as e) =
let rec translate prefix ({ Minils.e_desc = desc } as e) =
match desc with
| Minils.Eextvalue(ext) -> translate_ext prefix ext
| Minils.Eapp (* pervasives binary or unary stateless operations *)
@ -134,13 +140,13 @@ let rec translate prefix ({ Minils.e_desc = desc; Minils.e_ty = ty } as e) =
| "<>"),_ -> failwith("Sigali: '=' or '<>' not yet implemented")
| _ -> assert false
end
| Minils.Ewhen(e, c, var) when ((actual_ty e.Minils.e_ty) = Tbool) ->
let e = translate prefix e in
Swhen(e,
match (shortname c) with
"true" -> Svar(prefix ^ (name var))
| "false" -> Snot(Svar(prefix ^ (name var)))
| _ -> assert false)
(* | Minils.Ewhen(e, c, var) when ((actual_ty e.Minils.e_ty) = Tbool) -> *)
(* let e = translate prefix e in *)
(* Swhen(e, *)
(* match (shortname c) with *)
(* "true" -> Svar(prefix ^ (name var)) *)
(* | "false" -> Snot(Svar(prefix ^ (name var))) *)
(* | _ -> assert false) *)
| Minils.Ewhen(e, _c, _var) ->
translate prefix e
| Minils.Emerge(ck,[(c1,e1);(_c2,e2)]) ->
@ -182,8 +188,8 @@ let rec translate prefix ({ Minils.e_desc = desc; Minils.e_ty = ty } as e) =
failwith("Sigali: not supported application")
| Minils.Emerge(_, _) -> assert false
let rec translate_eq env f
(acc_dep,acc_states,acc_init,acc_inputs,acc_ctrl,acc_cont,acc_eqs)
let rec translate_eq f
(acc_states,acc_init,acc_inputs,acc_eqs)
{ Minils.eq_lhs = pat; Minils.eq_rhs = e; eq_base_ck = ck } =
let prefix = f ^ "_" in
@ -194,11 +200,10 @@ let rec translate_eq env f
match pat, desc with
| Minils.Evarpat(n), Minils.Efby(opt_c, e) ->
let sn = prefixed (name n) in
let sm = prefix ^ "mem_" ^ (name n) in
(* let acc_eqs = *)
(* (extend *)
(* constraints *)
(* (Slist[Sequal(Ssquare(Svar(sn)),Sconst(Ctrue))]))::acc_eqs in *)
let acc_eqs =
(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
@ -211,363 +216,47 @@ let rec translate_eq env f
in
let e_next = translate_ext prefix e in
let e_next = translate_ck prefix e_next ck in
acc_dep,
sn::acc_states,
acc_init,acc_inputs,acc_ctrl,acc_cont,
(n,sn)::acc_states,
acc_init,acc_inputs,
(extend
evolutions
(Slist[Sdefault(e_next,Svar(sn))]))
(* TODO *)
(* ::{ stmt_name = sn; *)
(* stmt_def = translate_ck prefix (Svar(sm)) ck } *)
::acc_eqs
| pat, Minils.Eapp({ Minils.a_op = Minils.Enode g_name;
Minils.a_id = Some a_id;
Minils.a_inlined = inlined }, e_list, None) ->
| pat, Minils.Eapp({ Minils.a_op = Minils.Enode _f; }, _e_list, None) ->
(*
g : n states (gq1,...,gqn), p inputs (gi1,...,gip), m outputs (go1,...,gom)
(y1,...,yp) = f(x1,...,xn)
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)
add inputs y1,...,yp. Link between yi and f's contract has
been done in the pass "Contracts".
*)
let g_name = shortname g_name in
let (g_p,g_p_contract) = NamesEnv.find g_name env in
let g = if inlined then g_name else g_name ^ "_contract" in
(* add dependency *)
let acc_dep = g :: acc_dep in
let name_list = translate_pat pat in
let g_p = if inlined then g_p else g_p_contract in
(* var_g : [gq1,...,gqn,gi1,...,gip] *)
let var_g = "var_" ^ g in
let vars =
match inlined with
| true -> g_p.proc_states @ g_p.proc_inputs
| false -> g_p.proc_states @ g_p.proc_inputs @ g_p.proc_outputs in
let acc_eqs =
{ stmt_name = var_g;
stmt_def = Slist(List.map (fun v -> Svar(v)) vars) }::acc_eqs in
(* var_inst_g : [hq1,...,hqn,e1,...,en] *)
let var_inst_g = "var_inst_" ^ g in
(* Coding contract states : S_n_id_s *)
(* id being the id of the application *)
(* n being the length of id *)
(* s being the name of the state*)
let a_id = (name a_id) in
let id_length = String.length a_id in
let s_prefix = "S_" ^ (string_of_int id_length) ^ "_" ^ a_id ^ "_" in
let new_states_list =
List.map
(fun g_state ->
(* Remove "g_" prefix *)
let l = String.length g in
let s =
String.sub
g_state (l+1)
((String.length g_state)-(l+1)) in
prefixed (s_prefix ^ s))
g_p.proc_states in
let e_states = List.map (fun hq -> Svar(hq)) new_states_list in
let e_list = List.map (translate_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
let vars_inst = e_states@e_list@e_outputs in
let acc_eqs =
{ stmt_name = var_inst_g;
stmt_def = Slist(vars_inst); }::acc_eqs in
let acc_states = List.rev_append new_states_list acc_states in
let acc_init = List.rev_append g_p.proc_init acc_init in
(* declare(d1,...,dn) *)
let dummy_list = var_list dummy_prefix (List.length g_p.proc_states) in
(* d : [d1,...dn] *)
let acc_eqs =
{stmt_name = dummy_prefix;
stmt_def = Slist(List.map (fun di -> Svar(di)) dummy_list)}::acc_eqs in
(* qi = di when ck default hqi *)
let q_list = List.map (fun _ -> "q_" ^ (gen_symbol ())) g_p.proc_states in
let e_list =
List.map2
(fun hq d ->
let e = Svar(d) in
let e = translate_ck (prefixed "") e ck in
Sdefault(e,Svar(hq)))
new_states_list dummy_list in
let acc_eqs =
List.fold_left2
(fun acc_eqs q e -> {stmt_name = q; stmt_def = e}::acc_eqs)
acc_eqs q_list e_list in
(* evol_g : l_subst(evolution(g),var_g,var_inst_g); *)
let evol_g = "evol_" ^ g in
let acc_eqs =
{stmt_name = evol_g;
stmt_def = l_subst (evolution (Svar g)) (Svar var_g) (Svar var_inst_g)}
::acc_eqs in
(* evolutions : concat(evolutions,l_subst([q1,...,qn],[d1,...,dn],evol_g) *)
let acc_eqs =
(extend evolutions (l_subst
(Slist (List.map (fun q -> Svar(q)) q_list))
(Slist (List.map (fun d -> Svar(d)) dummy_list))
(Svar evol_g)))
::acc_eqs in
(* initialisations : concat(initialisations, [subst(initial(g),var_g,var_inst_g)]) *)
let acc_eqs =
(extend initialisations (Slist[subst
(initial (Svar g))
(Svar var_g)
(Svar var_inst_g)]))
:: acc_eqs in
(* constraints : concat(constraints, [subst(constraint(g),var_g,var_inst_g)]) *)
let acc_eqs =
(extend constraints (Slist[subst
(pconstraint (Svar g))
(Svar var_g)
(Svar var_inst_g)]))
::acc_eqs in
(* if inlined, hoi : subst(goi,var_g,var_inst_g) *)
let acc_eqs =
match inlined with
| true ->
List.fold_left2
(fun acc_eqs o go ->
{stmt_name = prefixed o;
stmt_def = subst (Svar(go)) (Svar(var_g)) (Svar(var_inst_g))}
::acc_eqs)
acc_eqs name_list g_p.proc_outputs
| false -> acc_eqs in
(* assume & guarantee *)
(* f_g_assume_x : subst(g_assume,var_g,var_inst_g) *)
(* f_g_guarantee_x : subst(g_guarantee,var_g,var_inst_g) *)
let var_assume = prefixed (g ^ "_assume_" ^ (gen_symbol ())) in
let var_guarantee = prefixed (g ^ "_guarantee_" ^ (gen_symbol ())) in
let acc_eqs =
{stmt_name = var_assume;
stmt_def = subst (Svar(g ^ "_assume")) (Svar(var_g)) (Svar(var_inst_g))} ::
{stmt_name = var_guarantee;
stmt_def = subst (Svar(g ^ "_guarantee")) (Svar(var_g)) (Svar(var_inst_g))} ::
acc_eqs in
let acc_cont =
(Svar(var_assume),Svar(var_guarantee)) :: acc_cont in
acc_dep,acc_states,acc_init,
acc_inputs,acc_ctrl,acc_cont,acc_eqs
| pat, Minils.Eapp({ Minils.a_op = Minils.Enode g_name;
Minils.a_id = Some a_id;
Minils.a_inlined = inlined }, e_list, Some r) ->
(*
g : n states (gq1,...,gqn), p inputs (gi1,...,gip),
n init states (gq1_0,...,gqn_0)
case inlined :
var_g : [gq1,...,gqn,gi1,...,gip]
var_inst_g : [hq1,...,hqn,e1,...,en]
case non inlined :
add inputs go1',...,gom'
var_g : [gq1,...,gqn,gi1,...,gip,go1,...,gom]
var_inst_g : [hq1,...,hqn,e1,...,en,go1',...,gom']
declare(d1,...,dn)
d : [d1,...,dn]
% q1 = if ck then (if r then gq1_0 else d1) else hq1 %
q1 : (gq1_0 when r default d1) when ck default hq1
...
qn : (gqn_0 when r default dn) when ck default hqn
% P_inst = P[var_inst_g/var_g] %
evol_g : l_subst(evolution(g),var_g,var_inst_g);
evolutions : concat(evolutions,l_subst([q1,...,qn],[d1,...,dn],evol_g)
initialisations : concat(initialisations, [subst(initial(g),var_g,var_inst_g)])
constraints : concat(constraints, [subst(constraint(g),var_g,var_inst_g)])
case inlined :
ho1 : subst(go1,var_g,var_inst_g)
...
hom : subst(gom,var_g,var_inst_g)
case non inlined :
(nothing)
*)
let g_name = shortname g_name in
let (g_p,g_p_contract) = NamesEnv.find g_name env in
let g = if inlined then g_name else g_name ^ "_contract" in
(* add dependency *)
let acc_dep = g :: acc_dep in
let name_list = translate_pat pat in
let g_p = if inlined then g_p else g_p_contract in
(* var_g : [gq1,...,gqn,gi1,...,gip] *)
let var_g = "var_" ^ g in
let vars =
match inlined with
| true -> g_p.proc_states @ g_p.proc_inputs
| false -> g_p.proc_states @ g_p.proc_inputs @ g_p.proc_outputs in
let acc_eqs =
{ stmt_name = var_g;
stmt_def = Slist(List.map (fun v -> Svar(v)) vars) }::acc_eqs in
(* var_inst_g : [hq1,...,hqn,e1,...,en] *)
let var_inst_g = "var_inst_" ^ g in
(* Coding contract states : S_n_id_s *)
(* id being the id of the application *)
(* n being the length of id *)
(* s being the name of the state*)
let a_id = name a_id in
let id_length = String.length a_id in
let s_prefix = "S_" ^ (string_of_int id_length) ^ "_" ^ a_id ^ "_" in
let new_states_list =
List.map
(fun g_state ->
(* Remove "g_" prefix *)
let l = (String.length g) in
let s =
String.sub
g_state (l+1)
((String.length g_state)-(l+1)) in
prefixed (s_prefix ^ s))
g_p.proc_states in
let e_states = List.map (fun hq -> Svar(hq)) new_states_list in
let e_list = List.map (translate_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
let vars_inst = e_states@e_list@e_outputs in
let acc_eqs =
{ stmt_name = var_inst_g;
stmt_def = Slist(vars_inst); }::acc_eqs in
let acc_states = List.rev_append new_states_list acc_states in
let acc_init = List.rev_append g_p.proc_init acc_init in
(* declare(d1,...,dn) *)
let dummy_list = var_list dummy_prefix (List.length g_p.proc_states) in
(* d : [d1,...dn] *)
let acc_eqs =
{stmt_name = dummy_prefix;
stmt_def = Slist(List.map (fun di -> Svar(di)) dummy_list)}::acc_eqs in
(* qi = (gqi_0 when r default di) when ck default hqi *)
let q_list = List.map (fun _ -> "q_" ^ (gen_symbol ())) g_p.proc_states in
let e_list =
List.map2
(fun (q0,hq) d ->
let e = Sdefault(Swhen(Sconst(q0),
Svar(prefixed (name r))),Svar(d)) in
let e = translate_ck (prefixed "") e ck in
Sdefault(e,Svar(hq)))
(List.combine g_p.proc_init new_states_list) dummy_list in
let acc_eqs =
List.fold_left2
(fun acc_eqs q e -> {stmt_name = q; stmt_def = e}::acc_eqs)
acc_eqs q_list e_list in
(* evol_g : l_subst(evolution(g),var_g,var_inst_g); *)
let evol_g = "evol_" ^ g in
let acc_eqs =
{stmt_name = evol_g;
stmt_def = l_subst (evolution (Svar g)) (Svar var_g) (Svar var_inst_g)}
::acc_eqs in
(* evolutions : concat(evolutions,l_subst([q1,...,qn],[d1,...,dn],evol_g) *)
let acc_eqs =
(extend evolutions (l_subst
(Slist (List.map (fun q -> Svar(q)) q_list))
(Slist (List.map (fun d -> Svar(d)) dummy_list))
(Svar evol_g)))
::acc_eqs in
(* initialisations : concat(initialisations, [subst(initial(g),var_g,var_inst_g)]) *)
let acc_eqs =
(extend initialisations (Slist[subst
(initial (Svar g))
(Svar var_g)
(Svar var_inst_g)]))
:: acc_eqs in
(* constraints : concat(constraints, [subst(constraint(g),var_g,var_inst_g)]) *)
let acc_eqs =
(extend constraints (Slist[subst
(pconstraint (Svar g))
(Svar var_g)
(Svar var_inst_g)]))
::acc_eqs in
(* if inlined, hoi : subst(goi,var_g,var_inst_g) *)
let acc_eqs =
match inlined with
| true ->
List.fold_left2
(fun acc_eqs o go ->
{stmt_name = prefixed o;
stmt_def = subst (Svar(go)) (Svar(var_g)) (Svar(var_inst_g))}
::acc_eqs)
acc_eqs name_list g_p.proc_outputs
| false -> acc_eqs in
(* assume & guarantee *)
(* f_g_assume_x : subst(g_assume,var_g,var_inst_g) *)
(* f_g_guarantee_x : subst(g_guarantee,var_g,var_inst_g) *)
let var_assume = prefixed (g ^ "_assume_" ^ (gen_symbol ())) in
let var_guarantee = prefixed (g ^ "_guarantee_" ^ (gen_symbol ())) in
let acc_eqs =
{stmt_name = var_assume;
stmt_def = subst (Svar(g ^ "_assume")) (Svar(var_g)) (Svar(var_inst_g))} ::
{stmt_name = var_guarantee;
stmt_def = subst (Svar(g ^ "_guarantee")) (Svar(var_g)) (Svar(var_inst_g))} ::
acc_eqs in
let acc_cont =
(Svar(var_assume),Svar(var_guarantee)) :: acc_cont in
acc_dep,acc_states,acc_init,
acc_inputs,acc_ctrl,acc_cont,acc_eqs
let ident_list = translate_pat pat in
let acc_inputs =
acc_inputs @
(List.map (fun id -> (id,(prefixed (name id)))) ident_list) in
acc_states,acc_init,
acc_inputs,acc_eqs
| Minils.Evarpat(n), _ ->
(* assert : no fby, no node application in e *)
let e' = translate prefix e in
let e' =
begin match (actual_ty e.Minils.e_ty) with
| Tbool -> translate_ck prefix e' ck
| _ -> e'
end in
acc_dep,acc_states,acc_init,
acc_inputs,acc_ctrl,acc_cont,
(* let e' = *)
(* begin match (actual_ty e.Minils.e_ty) with *)
(* | Tbool -> translate_ck prefix e' ck *)
(* | _ -> e' *)
(* end in *)
acc_states,acc_init,
acc_inputs,
{ stmt_name = prefixed (name n);
stmt_def = e' }::acc_eqs
| _ -> assert false
let translate_eq_list env f eq_list =
let translate_eq_list f eq_list =
List.fold_left
(fun (acc_dep,acc_states,acc_init,
acc_inputs,acc_ctrl,acc_cont,acc_eqs) eq ->
translate_eq
env f
(acc_dep,acc_states,acc_init,
acc_inputs,acc_ctrl,acc_cont,acc_eqs)
eq)
([],[],[],[],[],[],[])
(fun (acc_states,acc_init, acc_inputs,acc_eqs) eq ->
translate_eq f (acc_states,acc_init,acc_inputs,acc_eqs) eq)
([],[],[],[])
eq_list
let translate_contract env f contract =
let translate_contract f contract =
let prefix = f ^ "_" in
let var_a = prefix ^ "assume" in
let var_g = prefix ^ "guarantee" in
@ -576,38 +265,32 @@ let translate_contract env f contract =
let body =
[{ stmt_name = var_g; stmt_def = Sconst(Ctrue) };
{ stmt_name = var_a; stmt_def = Sconst(Ctrue) }] in
[],[],[],body,(Svar(var_a),Svar(var_g)),[]
| Some {Minils.c_local = _locals;
[],[],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_assume_loc = e_a_loc;
Minils.c_enforce_loc = e_g_loc;
Minils.c_controllables = cl} ->
let dep,states,init,inputs,
controllables,_contracts,body =
translate_eq_list env f l_eqs in
let states,init,inputs,body = translate_eq_list 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 e_a_loc = translate_ext prefix e_a_loc in
let e_g_loc = translate_ext prefix e_g_loc in
let body =
{stmt_name = var_g; stmt_def = e_g} ::
{stmt_name = var_a; stmt_def = e_a} ::
{stmt_name = var_g; stmt_def = e_g &~ e_g_loc } ::
{stmt_name = var_a; stmt_def = e_a &~ e_a_loc } ::
body in
let controllables =
List.map (fun { Minils.v_ident = id } -> prefix ^ (name id)) cl in
dep,states,init,body,(Svar(var_a),Svar(var_g)),controllables
List.map
(fun ({ Minils.v_ident = id } as v) -> v,(prefix ^ (name id))) cl in
states,init,body,(Svar(var_a),Svar(var_g)),controllables,(locals@cl),l_eqs
let rec build_environment contracts =
match contracts with
| [] -> [],Sconst(Ctrue)
| [a,g] -> [a =>~ g],g
| (a,g)::l ->
let conts,assumes = build_environment l in
((a =>~ g) :: conts),(g &~ assumes)
let translate_node env
let translate_node
({ Minils.n_name = {name = f};
Minils.n_input = i_list; Minils.n_output = o_list;
Minils.n_local = _d_list; Minils.n_equs = eq_list;
@ -615,92 +298,118 @@ let translate_node env
(* every variable is prefixed by its node name *)
let inputs =
List.map
(fun { Minils.v_ident = v } -> f ^ "_" ^ (name v)) i_list in
let outputs =
(fun { Minils.v_ident = v } -> v,(f ^ "_" ^ (name v))) i_list in
let sig_outputs =
List.map
(fun { Minils.v_ident = v } -> f ^ "_" ^ (name v)) o_list in
let dep,states,init,add_inputs,add_controllables,contracts,body =
translate_eq_list env f eq_list in
let dep_c,states_c,init_c,body_c,(a_c,g_c),controllables =
translate_contract env f contract in
let states,init,add_inputs,body =
translate_eq_list f eq_list in
let states_c,init_c,body_c,(a_c,g_c),controllables,locals_c,eqs_c =
translate_contract f contract in
let inputs = inputs @ add_inputs in
let controllables = controllables @ add_controllables in
let body = List.rev body in
let states = List.rev states in
let body_c = List.rev body_c in
let states_c = List.rev states_c in
let mls_inputs,sig_inputs = List.split inputs in
let mls_states,sig_states = List.split (states@states_c) in
let mls_ctrl,sig_ctrl = List.split controllables in
let constraints =
List.map
(fun v -> Sequal(Ssquare(Svar(v)),Sconst(Ctrue)))
(inputs@controllables) in
let contracts_components,assumes_components =
build_environment contracts in
let constraints = constraints @
contracts_components @ [Sequal (a_c,Sconst(Ctrue))] in
let impl = g_c &~ assumes_components in
let obj = Security(impl) in
let p = { proc_dep = unique (dep @ dep_c);
(sig_inputs@sig_ctrl) in
let constraints = constraints @ [Sequal (a_c,Sconst(Ctrue))] in
let obj = Security(g_c) in
let p = { proc_dep = [];
proc_name = f;
proc_inputs = inputs@controllables;
proc_uncont_inputs = inputs;
proc_outputs = outputs;
proc_controllables = controllables;
proc_states = states@states_c;
proc_inputs = sig_inputs@sig_ctrl;
proc_uncont_inputs = sig_inputs;
proc_outputs = sig_outputs;
proc_controllables = sig_ctrl;
proc_states = sig_states;
proc_init = init@init_c;
proc_constraints = constraints;
proc_body = body@body_c;
proc_objectives = [obj] } in
(* Hack : save inputs and states names for controller call *)
let remove_prefix =
let n = String.length f in
fun s ->
String.sub s (n+1) ((String.length s) - (n+1)) in
node.Minils.n_controller_call <-
(List.map remove_prefix inputs,
List.map remove_prefix (states@states_c));
let f_contract = f ^ "_contract" in
let inputs_c =
let ctrlr_pat = Minils.Etuplepat(List.map (fun { Minils.v_ident = v } ->
Minils.Evarpat(v))
mls_ctrl) in
let ctrlr_name = f ^ "_controller" in
let ctrlr_fun_name = { qual = Module (String.capitalize ctrlr_name);
name = ctrlr_name } in
let ctrlr_exp =
Minils.mk_exp
Cbase
(Tprod (List.map (fun _ -> Initial.tbool) mls_ctrl))
~linearity:Linearity.Ltop
(Minils.Eapp(Minils.mk_app (Minils.Efun ctrlr_fun_name),
(List.map
(fun v ->
Minils.mk_extvalue
~ty:Initial.tbool
~linearity:Linearity.Ltop
~clock:Cbase
(Minils.Wvar v))
(mls_inputs@mls_states))
@ (List.map
(fun _ ->
Minils.mk_extvalue
~ty:Initial.tbool
~linearity:Linearity.Ltop
~clock:Cbase
(Minils.Wconst(Initial.mk_static_bool true)))
mls_ctrl),
None))
in
let ctrlr_call =
Minils.mk_equation ~base_ck:Cbase false ctrlr_pat ctrlr_exp in
let ctrlr_inputs =
(List.map
(fun v ->
Signature.mk_arg (Some v) Initial.tbool Linearity.Ltop Signature.Cbase)
(sig_inputs@sig_states))
@ (List.map
(fun v ->
Signature.mk_arg
(Some ("p_" ^ v)) Initial.tbool Linearity.Ltop Signature.Cbase)
sig_ctrl) in
let ctrlr_outputs =
List.map
(fun { Minils.v_ident = v } -> f_contract ^ "_" ^ (name v)) i_list in
let outputs_c =
List.map
(fun { Minils.v_ident = v } -> f_contract ^ "_" ^ (name v)) o_list in
let dep_c,states_c,init_c,body_c,(_a_c,_g_c),_controllables =
translate_contract env f_contract contract in
let states_c = List.rev states_c in
let body_c = List.rev body_c in
let constraints_c =
List.map
(fun v -> Sequal(Ssquare(Svar(v)),Sconst(Ctrue)))
(inputs_c@outputs_c) in
let p_c = { proc_dep = dep_c;
proc_name = f ^ "_contract";
proc_inputs = inputs_c@outputs_c;
proc_uncont_inputs = inputs_c@outputs_c;
proc_outputs = [];
proc_controllables = [];
proc_states = states_c;
proc_init = init_c;
proc_constraints = constraints_c;
proc_body = body_c;
proc_objectives = [] } in
(NamesEnv.add f (p,p_c) env), (p,p_c)
(fun v ->
Signature.mk_arg (Some v) Initial.tbool Linearity.Ltop Signature.Cbase)
sig_ctrl in
let ctrlr_signature =
Signature.mk_node Location.no_location ~extern:false
ctrlr_inputs ctrlr_outputs false false [] in
(* Add controller into modules *)
Modules.add_value ctrlr_fun_name ctrlr_signature;
let node =
{ node with
Minils.n_contract = None;
Minils.n_local = node.Minils.n_local @ locals_c;
Minils.n_equs = ctrlr_call :: (node.Minils.n_equs @ eqs_c);
} in
node, p
let program p =
let _env,acc_proc =
let acc_proc, acc_p_desc =
List.fold_left
(fun (env,acc) p_desc ->
(fun (acc_proc,acc_p_desc) p_desc ->
match p_desc with
| Minils.Pnode(node) ->
let env,(proc,contract) = translate_node env node in
env,contract::proc::acc
| _ -> env,acc)
(NamesEnv.empty,[])
let (node,proc) = translate_node node in
(proc::acc_proc),((Minils.Pnode(node))::acc_p_desc)
| p -> (acc_proc,p::acc_p_desc))
([],[])
p.Minils.p_desc in
let procs = List.rev acc_proc in
let filename = filename_of_name (modul_to_string p.Minils.p_modname) in
let dirname = build_path (filename ^ "_z3z") in
let dir = clean_dir dirname in
Sigali.Printer.print dir procs
Sigali.Printer.print dir procs;
{ p with Minils.p_desc = List.rev acc_p_desc }

2
compiler/minils/sigali/sigalimain.mli
View file

@ -11,4 +11,4 @@
(* $Id$ *)
val program : Minils.program -> unit
val program : Minils.program -> Minils.program