04b8853a1d
It has type: reinit: t at r * t -> t at r It can be used to put a constant value in a location.
707 lines
24 KiB
OCaml
707 lines
24 KiB
OCaml
(****************************************************)
|
|
(* *)
|
|
(* Heptagon/BZR *)
|
|
(* *)
|
|
(* Author : Gwenaël Delaval *)
|
|
(* Organization : UJF, LIG *)
|
|
(* *)
|
|
(****************************************************)
|
|
|
|
(* Translation from the source language to Sigali polynomial systems *)
|
|
|
|
(* $Id: dynamic_system.ml 2652 2011-03-11 16:26:17Z delaval $ *)
|
|
|
|
open Misc
|
|
open Compiler_utils
|
|
open Names
|
|
open Idents
|
|
open Types
|
|
open Clocks
|
|
open Sigali
|
|
|
|
type mtype = Tint | Tbool | Tother
|
|
|
|
let actual_ty = function
|
|
| Tid({ qual = Pervasives; name = "bool"}) -> Tbool
|
|
| Tid({ qual = Pervasives; name = "int"}) -> Tint
|
|
| _ -> Tother
|
|
|
|
let var_list prefix n =
|
|
let rec varl acc = function
|
|
| 0 -> acc
|
|
| n ->
|
|
let acc = (prefix ^ (string_of_int n)) :: acc in
|
|
varl acc (n-1) in
|
|
varl [] n
|
|
|
|
let dummy_prefix = "d"
|
|
|
|
let translate_static_exp se =
|
|
match se.se_desc with
|
|
| Sint(v) -> Cint(v)
|
|
| Sfloat(_) -> failwith("Sigali: floats not implemented")
|
|
| Sbool(true) -> Ctrue
|
|
| Sbool(false) -> Cfalse
|
|
| Sop({ qual = Pervasives; name = "~-" },[{se_desc = Sint(v)}]) ->
|
|
Cint(-v)
|
|
| _ ->
|
|
Format.printf "Constant %a@\n"
|
|
Global_printer.print_static_exp se;
|
|
failwith("Sigali: untranslatable constant")
|
|
|
|
|
|
let rec translate_pat = function
|
|
| Minils.Evarpat(x) -> [name x]
|
|
| Minils.Etuplepat(pat_list) ->
|
|
List.fold_right (fun pat acc -> (translate_pat pat) @ acc) pat_list []
|
|
|
|
let rec translate_ck pref e = function
|
|
| Cbase | Cvar { contents = Cindex _ } ->
|
|
e
|
|
| Cvar { contents = Clink ck } -> translate_ck pref e ck
|
|
| Con(ck,c,var) ->
|
|
let e = translate_ck pref e ck in
|
|
Swhen(e,
|
|
match (shortname c) with
|
|
"true" -> Svar(pref ^ (name var))
|
|
| "false" -> Snot(Svar(pref ^ (name var)))
|
|
| _ -> assert false)
|
|
|
|
|
|
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
|
|
| Minils.Wvar(n) -> Svar(prefix ^ (name n))
|
|
| Minils.Wwhen(e, c, var) when ((actual_ty e.Minils.w_ty) = Tbool) ->
|
|
let e = translate_ext prefix e in
|
|
Swhen(e,
|
|
match (shortname c) with
|
|
"true" -> Svar(prefix ^ (name var))
|
|
| "false" -> Snot(Svar(prefix ^ (name var)))
|
|
| _ -> assert false)
|
|
| Minils.Wwhen(e, _c, _var) ->
|
|
translate_ext prefix e
|
|
| Minils.Wfield(_) ->
|
|
failwith("Sigali: structures not implemented")
|
|
| Minils.Wreinit _ -> failwith("Sigali: reinit not implemented")
|
|
|
|
(* [translate e = c] *)
|
|
let rec translate prefix ({ Minils.e_desc = desc; Minils.e_ty = ty } as e) =
|
|
match desc with
|
|
| Minils.Eextvalue(ext) -> translate_ext prefix ext
|
|
| Minils.Eapp (* pervasives binary or unary stateless operations *)
|
|
({ Minils.a_op = Minils.Efun({qual=Pervasives;name=n})},
|
|
e_list, _) ->
|
|
begin
|
|
match n, e_list with
|
|
| "not", [e] -> Snot(translate_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)
|
|
| Minils.Ewhen(e, _c, _var) ->
|
|
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
|
|
| 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
|
|
| Minils.Estruct(_) ->
|
|
failwith("Sigali: structures not implemented")
|
|
| Minils.Eiterator(_,_,_,_,_,_) ->
|
|
failwith("Sigali: iterators not implemented")
|
|
| Minils.Eapp({Minils.a_op = Minils.Enode(_)},_,_) ->
|
|
failwith("Sigali: node in expressions; programs should be normalized")
|
|
| Minils.Efby(_,_) ->
|
|
failwith("Sigali: fby in expressions; programs should be normalized")
|
|
| Minils.Eapp(_,_,_) ->
|
|
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
|
|
(acc_dep,acc_states,acc_init,acc_inputs,acc_ctrl,acc_cont,acc_eqs)
|
|
{ Minils.eq_lhs = pat; Minils.eq_rhs = e } =
|
|
|
|
let prefix = f ^ "_" in
|
|
|
|
let prefixed n = prefix ^ n in
|
|
|
|
let { Minils.e_desc = desc; Minils.e_base_ck = ck } = e in
|
|
match pat, desc with
|
|
| Minils.Evarpat(n), Minils.Efby(opt_c, e) ->
|
|
let sn = prefixed (name n) in
|
|
let sm = prefix ^ "mem_" ^ (name n) in
|
|
(* let acc_eqs = *)
|
|
(* (extend *)
|
|
(* constraints *)
|
|
(* (Slist[Sequal(Ssquare(Svar(sn)),Sconst(Ctrue))]))::acc_eqs in *)
|
|
let acc_eqs,acc_init =
|
|
match opt_c with
|
|
| None -> acc_eqs,Cfalse::acc_init
|
|
| Some(c) ->
|
|
let c = translate_static_exp c in
|
|
(extend
|
|
initialisations
|
|
(Slist[Sequal(Svar(sn),Sconst(c))]))::acc_eqs,
|
|
c::acc_init
|
|
in
|
|
let e_next = translate_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,
|
|
(extend
|
|
evolutions
|
|
(Slist[Sdefault(e_next,Svar(sn))]))
|
|
(* TODO *)
|
|
(* ::{ stmt_name = sn; *)
|
|
(* stmt_def = translate_ck prefix (Svar(sm)) ck } *)
|
|
::acc_eqs
|
|
| pat, Minils.Eapp({ Minils.a_op = Minils.Enode g_name;
|
|
Minils.a_id = Some a_id;
|
|
Minils.a_inlined = inlined }, e_list, None) ->
|
|
(*
|
|
g : n states (gq1,...,gqn), p inputs (gi1,...,gip), m outputs (go1,...,gom)
|
|
|
|
case inlined :
|
|
var_g : [gq1,...,gqn,gi1,...,gip]
|
|
var_inst_g : [hq1,...,hqn,e1,...,en]
|
|
case non inlined :
|
|
add inputs go1',...,gom'
|
|
var_g : [gq1,...,gqn,gi1,...,gip,go1,...,gom]
|
|
var_inst_g : [hq1,...,hqn,e1,...,en,go1',...,gom']
|
|
|
|
declare(d1,...,dn)
|
|
|
|
d : [d1,...,dn]
|
|
% q1 = if ck then d1 else hq1 %
|
|
q1 : d1 when ck default hq1
|
|
...
|
|
qn : dn when ck default hqn
|
|
|
|
% P_inst = P[var_inst_g/var_g] %
|
|
evol_g : l_subst(evolution(g),var_g,var_inst_g);
|
|
evolutions : concat(evolutions,l_subst([q1,...,qn],[d1,...,dn],evol_g)
|
|
initialisations : concat(initialisations, [subst(initial(g),var_g,var_inst_g)])
|
|
constraints : concat(constraints, [subst(constraint(g),var_g,var_inst_g)])
|
|
|
|
case inlined :
|
|
ho1 : subst(go1,var_g,var_inst_g)
|
|
...
|
|
hom : subst(gom,var_g,var_inst_g)
|
|
case non inlined :
|
|
(nothing)
|
|
*)
|
|
let g_name = shortname g_name in
|
|
let (g_p,g_p_contract) = NamesEnv.find g_name env in
|
|
let g = if inlined then g_name else g_name ^ "_contract" in
|
|
(* add dependency *)
|
|
let acc_dep = g :: acc_dep in
|
|
let name_list = translate_pat pat in
|
|
let g_p = if inlined then g_p else g_p_contract in
|
|
(* var_g : [gq1,...,gqn,gi1,...,gip] *)
|
|
let var_g = "var_" ^ g in
|
|
let vars =
|
|
match inlined with
|
|
| true -> g_p.proc_states @ g_p.proc_inputs
|
|
| false -> g_p.proc_states @ g_p.proc_inputs @ g_p.proc_outputs in
|
|
let acc_eqs =
|
|
{ stmt_name = var_g;
|
|
stmt_def = Slist(List.map (fun v -> Svar(v)) vars) }::acc_eqs in
|
|
(* var_inst_g : [hq1,...,hqn,e1,...,en] *)
|
|
let var_inst_g = "var_inst_" ^ g in
|
|
(* Coding contract states : S_n_id_s *)
|
|
(* id being the id of the application *)
|
|
(* n being the length of id *)
|
|
(* s being the name of the state*)
|
|
let a_id = (name a_id) in
|
|
let id_length = String.length a_id in
|
|
let s_prefix = "S_" ^ (string_of_int id_length) ^ "_" ^ a_id ^ "_" in
|
|
let new_states_list =
|
|
List.map
|
|
(fun g_state ->
|
|
(* Remove "g_" prefix *)
|
|
let l = String.length g in
|
|
let s =
|
|
String.sub
|
|
g_state (l+1)
|
|
((String.length g_state)-(l+1)) in
|
|
prefixed (s_prefix ^ s))
|
|
g_p.proc_states in
|
|
let e_states = List.map (fun hq -> Svar(hq)) new_states_list in
|
|
let e_list = List.map (translate_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
|
|
| Minils.Evarpat(n), _ ->
|
|
(* assert : no fby, no node application in e *)
|
|
let e' = translate prefix e in
|
|
let e' =
|
|
begin match (actual_ty e.Minils.e_ty) with
|
|
| Tbool -> translate_ck prefix e' ck
|
|
| _ -> e'
|
|
end in
|
|
acc_dep,acc_states,acc_init,
|
|
acc_inputs,acc_ctrl,acc_cont,
|
|
{ stmt_name = prefixed (name n);
|
|
stmt_def = e' }::acc_eqs
|
|
| _ -> assert false
|
|
|
|
let translate_eq_list env f eq_list =
|
|
List.fold_left
|
|
(fun (acc_dep,acc_states,acc_init,
|
|
acc_inputs,acc_ctrl,acc_cont,acc_eqs) eq ->
|
|
translate_eq
|
|
env f
|
|
(acc_dep,acc_states,acc_init,
|
|
acc_inputs,acc_ctrl,acc_cont,acc_eqs)
|
|
eq)
|
|
([],[],[],[],[],[],[])
|
|
eq_list
|
|
|
|
let translate_contract env f contract =
|
|
let prefix = f ^ "_" in
|
|
let var_a = prefix ^ "assume" in
|
|
let var_g = prefix ^ "guarantee" in
|
|
match contract with
|
|
| None ->
|
|
let body =
|
|
[{ stmt_name = var_g; stmt_def = Sconst(Ctrue) };
|
|
{ stmt_name = var_a; stmt_def = Sconst(Ctrue) }] in
|
|
[],[],[],body,(Svar(var_a),Svar(var_g)),[]
|
|
| Some {Minils.c_local = _locals;
|
|
Minils.c_eq = l_eqs;
|
|
Minils.c_assume = e_a;
|
|
Minils.c_enforce = e_g;
|
|
Minils.c_controllables = cl} ->
|
|
let dep,states,init,inputs,
|
|
controllables,_contracts,body =
|
|
translate_eq_list env f l_eqs in
|
|
assert (inputs = []);
|
|
assert (controllables = []);
|
|
let e_a = translate_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
|
|
let controllables =
|
|
List.map (fun { Minils.v_ident = id } -> prefix ^ (name id)) cl in
|
|
dep,states,init,body,(Svar(var_a),Svar(var_g)),controllables
|
|
|
|
|
|
|
|
let rec build_environment contracts =
|
|
match contracts with
|
|
| [] -> [],Sconst(Ctrue)
|
|
| [a,g] -> [a =>~ g],g
|
|
| (a,g)::l ->
|
|
let conts,assumes = build_environment l in
|
|
((a =>~ g) :: conts),(g &~ assumes)
|
|
|
|
let translate_node env
|
|
({ Minils.n_name = {name = f};
|
|
Minils.n_input = i_list; Minils.n_output = o_list;
|
|
Minils.n_local = _d_list; Minils.n_equs = eq_list;
|
|
Minils.n_contract = contract } as node) =
|
|
(* every variable is prefixed by its node name *)
|
|
let inputs =
|
|
List.map
|
|
(fun { Minils.v_ident = v } -> f ^ "_" ^ (name v)) i_list in
|
|
let outputs =
|
|
List.map
|
|
(fun { Minils.v_ident = v } -> f ^ "_" ^ (name v)) o_list in
|
|
let dep,states,init,add_inputs,add_controllables,contracts,body =
|
|
translate_eq_list env f eq_list in
|
|
let dep_c,states_c,init_c,body_c,(a_c,g_c),controllables =
|
|
translate_contract env f contract in
|
|
let inputs = inputs @ add_inputs in
|
|
let controllables = controllables @ add_controllables in
|
|
let body = List.rev body in
|
|
let states = List.rev states in
|
|
let body_c = List.rev body_c in
|
|
let states_c = List.rev states_c in
|
|
let constraints =
|
|
List.map
|
|
(fun v -> Sequal(Ssquare(Svar(v)),Sconst(Ctrue)))
|
|
(inputs@controllables) in
|
|
let contracts_components,assumes_components =
|
|
build_environment contracts in
|
|
let constraints = constraints @
|
|
contracts_components @ [Sequal (a_c,Sconst(Ctrue))] in
|
|
let impl = g_c &~ assumes_components in
|
|
let obj = Security(impl) in
|
|
let p = { proc_dep = unique (dep @ dep_c);
|
|
proc_name = f;
|
|
proc_inputs = inputs@controllables;
|
|
proc_uncont_inputs = inputs;
|
|
proc_outputs = outputs;
|
|
proc_controllables = controllables;
|
|
proc_states = states@states_c;
|
|
proc_init = init@init_c;
|
|
proc_constraints = constraints;
|
|
proc_body = body@body_c;
|
|
proc_objectives = [obj] } in
|
|
(* Hack : save inputs and states names for controller call *)
|
|
let remove_prefix =
|
|
let n = String.length f in
|
|
fun s ->
|
|
String.sub s (n+1) ((String.length s) - (n+1)) in
|
|
node.Minils.n_controller_call <-
|
|
(List.map remove_prefix inputs,
|
|
List.map remove_prefix (states@states_c));
|
|
|
|
let f_contract = f ^ "_contract" in
|
|
let inputs_c =
|
|
List.map
|
|
(fun { Minils.v_ident = v } -> f_contract ^ "_" ^ (name v)) i_list in
|
|
let outputs_c =
|
|
List.map
|
|
(fun { Minils.v_ident = v } -> f_contract ^ "_" ^ (name v)) o_list in
|
|
let dep_c,states_c,init_c,body_c,(_a_c,_g_c),_controllables =
|
|
translate_contract env f_contract contract in
|
|
let states_c = List.rev states_c in
|
|
let body_c = List.rev body_c in
|
|
let constraints_c =
|
|
List.map
|
|
(fun v -> Sequal(Ssquare(Svar(v)),Sconst(Ctrue)))
|
|
(inputs_c@outputs_c) in
|
|
let p_c = { proc_dep = dep_c;
|
|
proc_name = f ^ "_contract";
|
|
proc_inputs = inputs_c@outputs_c;
|
|
proc_uncont_inputs = inputs_c@outputs_c;
|
|
proc_outputs = [];
|
|
proc_controllables = [];
|
|
proc_states = states_c;
|
|
proc_init = init_c;
|
|
proc_constraints = constraints_c;
|
|
proc_body = body_c;
|
|
proc_objectives = [] } in
|
|
(NamesEnv.add f (p,p_c) env), (p,p_c)
|
|
|
|
let program p =
|
|
let _env,acc_proc =
|
|
List.fold_left
|
|
(fun (env,acc) p_desc ->
|
|
match p_desc with
|
|
| Minils.Pnode(node) ->
|
|
let env,(proc,contract) = translate_node env node in
|
|
env,contract::proc::acc
|
|
| _ -> env,acc)
|
|
(NamesEnv.empty,[])
|
|
p.Minils.p_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
|
|
|