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

Sigali code generation

Browse source 
Sigali AST and Sigalimain module for sigali code generation
from normalized and Boolean minils program
This commit is contained in:
Gwenaël Delaval 2011-03-16 23:25:04 +01:00 committed by Gwenal Delaval
parent ac9715ad90
commit da37fd8e58
4 changed files with 1216 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

435
compiler/minils/sigali/sigali.ml Normal file
View file

@ -0,0 +1,435 @@
(****************************************************)
(* *)
(* Sigali Library *)
(* *)
(* Author : Gwenaël Delaval *)
(* Organization : INRIA Rennes, VerTeCs *)
(* *)
(****************************************************)
(* $Id: sigali.ml 2416 2011-01-13 17:00:15Z delaval $ *)
(* Sigali representation and output *)
type name = string
type var = name
type const = Cfalse | Cabsent | Ctrue | Cint of int
type exp =
| Sconst of const
| Svar of name
| Swhen of exp * exp (* e1 when e2 *)
| Sdefault of exp * exp (* e1 default e2 *)
| Sequal of exp * exp (* e1 = e2 *)
| Ssquare of exp (* e^2 *)
| Snot of exp (* not e *)
| Sand of exp * exp (* e1 and e2 *)
| Sor of exp * exp (* e1 or e2 *)
| Sprim of name * exp list (* f(e1,...,en) *)
| Slist of exp list (* [e1,...,en] *)
| Splus of exp * exp (* e1 + e2 *)
| Sminus of exp * exp (* e1 - e2 *)
| Sprod of exp * exp (* e1 * e2 *)
type statement = { (* name : definition *)
stmt_name : name;
stmt_def : exp;
}
type objective =
| Security of exp
| Reachability of exp
| Attractivity of exp
type processus = {
proc_dep : name list;
proc_name : name;
proc_inputs : var list;
proc_uncont_inputs : var list;
proc_outputs : var list;
proc_controllables : var list;
proc_states : var list;
proc_init : const list;
proc_constraints : exp list;
proc_body : statement list;
proc_objectives : objective list;
}
type program = processus list
let concat e1 e2 =
Sprim("concat",[e1;e2])
let evolutions = "evolutions"
let initialisations = "initialisations"
let constraints = "constraints"
let extend var e =
{ stmt_name = var ;
stmt_def = concat (Svar(var)) e }
let subst e1 e2 e3 =
Sprim ("subst",[e1;e2;e3])
let l_subst e1 e2 e3 =
Sprim ("l_subst",[e1;e2;e3])
let evolution p =
Sprim ("evolution",[p])
let initial p =
Sprim ("initial",[p])
let pconstraint p =
Sprim ("constraint",[p])
let ifthenelse e1 e2 e3 =
Sdefault(Swhen(e2,e1),e3)
let (&~) e1 e2 =
match e1,e2 with
| Sconst(Cfalse), _
| _, Sconst(Cfalse) -> Sconst(Cfalse)
| Sconst(Ctrue), e
| e, Sconst(Ctrue) -> e
| _ -> Sand(e1,e2)
let (|~) e1 e2 =
match e1,e2 with
| Sconst(Ctrue), _
| _, Sconst(Ctrue) -> Sconst(Ctrue)
| Sconst(Cfalse), e
| e, Sconst(Cfalse) -> e
| _ -> Sor(e1,e2)
let (=>~) e1 e2 =
match e1,e2 with
| Sconst(Ctrue), e -> e
| _, Sconst(Ctrue)
| Sconst(Cfalse), _ -> Sconst(Ctrue)
| _ -> Sor(Snot(e1),e2)
let a_const e =
Sprim ("a_const",[e])
let a_var e e1 e2 e3 =
Sprim ("a_var", [e;e1;e2;e3])
let a_part e e1 e2 e3 =
Sprim ("a_part", [e;e1;e2;e3])
let a_inf e1 e2 =
Sprim ("a_inf", [e1;e2])
let a_sup e1 e2 =
Sprim ("a_sup", [e1;e2])
module Printer =
struct
open Format
let rec print_list ff print sep l =
match l with
| [] -> ()
| [x] -> print ff x
| x :: l ->
print ff x;
fprintf ff "%s@ " sep;
print_list ff print sep l
let print_string ff s =
fprintf ff "%s" s
let print_name ff n =
fprintf ff "%s" n
let print_const ff c =
match c with
| Cfalse -> fprintf ff "-1"
| Ctrue -> fprintf ff "1"
| Cabsent -> fprintf ff "0"
| Cint(v) -> fprintf ff "%d" v
let rec print_exp ff e =
match e with
| Sconst(c) -> print_const ff c
| Svar(v) -> print_name ff v
| Swhen(e1,e2) ->
fprintf ff "(%a@ when %a)"
print_exp e1
print_exp e2
| Sdefault(e1,e2) ->
fprintf ff "(%a@ default %a)"
print_exp e1
print_exp e2
| Sequal(e1,e2) ->
fprintf ff "(%a@ = %a)"
print_exp e1
print_exp e2
| Ssquare(e) ->
fprintf ff "(%a^2)"
print_exp e
| Snot(e) ->
fprintf ff "(not %a)"
print_exp e
| Sand(e1,e2) ->
fprintf ff "(%a@ and %a)"
print_exp e1
print_exp e2
| Sor(e1,e2) ->
fprintf ff "(%a@ or %a)"
print_exp e1
print_exp e2
| Sprim(f,e_l) ->
fprintf ff "%s(@[" f;
print_list ff print_exp "," e_l;
fprintf ff "@])"
| Slist(e_l) ->
fprintf ff "[@[";
print_list ff print_exp "," e_l;
fprintf ff "]@]"
| Splus(e1,e2) ->
fprintf ff "(%a@ + %a)"
print_exp e1
print_exp e2
| Sminus(e1,e2) ->
fprintf ff "(%a@ - %a)"
print_exp e1
print_exp e2
| Sprod(e1,e2) ->
fprintf ff "(%a@ * %a)"
print_exp e1
print_exp e2
let print_statement ff { stmt_name = name; stmt_def = e } =
fprintf ff "@[<hov 2>%a : %a;@]"
print_name name
print_exp e
let print_statements ff stmt_l =
fprintf ff "@[<v>";
print_list ff print_statement "" stmt_l;
fprintf ff "@]@ "
let print_objective name ff obj =
match obj with
| Security(e) ->
fprintf ff "%s : S_Security(%s,B_True(%s,%a));"
name name name
print_exp e
| Reachability(e) ->
fprintf ff "%s : S_Reachable(%s,B_True(%s,%a));"
name name name
print_exp e
| Attractivity(e) ->
fprintf ff "%s : S_Attractivity(%s,B_True(%s,%a));"
name name name
print_exp e
let print_verification name ff obj =
match obj with
| Security(e) ->
fprintf ff "verif_result : verif_result andb notb Reachable(%s,B_False(%s,%a));"
name name
print_exp e
| Reachability(e) ->
fprintf ff "verif_result : verif_result andb Reachable(%s,B_True(%s,%a));"
name name
print_exp e
| Attractivity(_) -> failwith("Attractivity verification not allowed")
let sigali_head = "
set_reorder(2);
read(\"Property.lib\");
read(\"Synthesis.lib\");
read(\"Verif_Determ.lib\");
read(\"Simul.lib\");
read(\"Synthesis_Partial_order.lib\");
read(\"Orbite.lib\");
"
let sigali_foot = ""
let print_processus dir ({ proc_dep = dep_list;
proc_name = name;
proc_inputs = inputs;
proc_uncont_inputs = uncont_inputs;
proc_outputs = outputs;
proc_controllables = controllables;
proc_states = states;
proc_constraints = constraints;
proc_body = body;
proc_objectives = objectives;
}) =
let sigc = open_out (dir ^ "/" ^ name ^ ".z3z") in
let ff = formatter_of_out_channel sigc in
Compiler_utils.print_header_info ff "%" "%";
fprintf ff "%s" sigali_head;
let n = List.length states in
(* declare dummy variables d1...dn *)
fprintf ff "@[declare(@[<hov>d1";
for i = 2 to n do
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;
(* 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;
fprintf ff "@]];@,";
(* states decl. *)
fprintf ff "states : [@[";
if states = [] then
(* dummy state var to avoid sigali segfault *)
fprintf ff "d1"
else
print_list ff print_name "," states;
fprintf ff "@]];@,";
(* controllables : *)
fprintf ff "controllables : [@[";
print_list ff print_name "," controllables;
fprintf ff "@]];@,";
(* init evolutions, initialisations *)
if states = [] then
fprintf ff "evolutions : [d1];@,"
else
fprintf ff "evolutions : [];@,";
fprintf ff "initialisations : [];@,";
(* body statements *)
print_statements ff body;
(* constraints *)
fprintf ff "constraints : [@[";
print_list ff print_exp "," constraints;
fprintf ff "@]];@,";
(* outputs : comment *)
fprintf ff "@,%% --- outputs : [@[";
print_list ff print_name "," outputs;
fprintf ff "@]] --- %%@,";
(* process declaration *)
fprintf ff
("%s : processus(" ^^
"@[conditions," ^^
"@ states," ^^
"@ evolutions," ^^
"@ initialisations," ^^
"@ [gen(constraints)]," ^^
"@ controllables@]);@,")
name;
begin
match controllables with
[] ->
begin
(* No controllable variables: verification *)
(* Initialisation of verification result *)
fprintf ff "verif_result : True;@,";
(* Verification of properties (update verif_result) *)
fprintf ff "@[<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;
fprintf ff "@?";
close_out sigc
let print dir p_l =
List.iter (print_processus dir) p_l
end

103
compiler/minils/sigali/sigali.mli Normal file
View file

@ -0,0 +1,103 @@
(****************************************************)
(* *)
(* Sigali Library *)
(* *)
(* Author : Gwenaël Delaval *)
(* Organization : INRIA Rennes, VerTeCs *)
(* *)
(****************************************************)
(* $Id: sigali.mli 2324 2010-12-05 10:22:36Z delaval $ *)
(* Sigali representation and output *)
type name = string
type var = name
type const = Cfalse | Cabsent | Ctrue | Cint of int
type exp =
| Sconst of const
| Svar of name
| Swhen of exp * exp (* e1 when e2 *)
| Sdefault of exp * exp (* e1 default e2 *)
| Sequal of exp * exp (* e1 = e2 *)
| Ssquare of exp (* e^2 *)
| Snot of exp (* not e *)
| Sand of exp * exp (* e1 and e2 *)
| Sor of exp * exp (* e1 or e2 *)
| Sprim of name * exp list (* f(e1,...,en) *)
| Slist of exp list (* [e1,...,en] *)
| Splus of exp * exp (* e1 + e2 *)
| Sminus of exp * exp (* e1 - e2 *)
| Sprod of exp * exp (* e1 * e2 *)
type statement = { (* name : definition *)
stmt_name : name;
stmt_def : exp;
}
type objective =
| Security of exp
| Reachability of exp
| Attractivity of exp
type processus = {
proc_dep : name list;
proc_name : name;
proc_inputs : var list;
proc_uncont_inputs : var list;
proc_outputs : var list;
proc_controllables : var list;
proc_states : var list;
proc_init : const list;
proc_constraints : exp list;
proc_body : statement list;
proc_objectives : objective list;
}
type program = processus list
val concat : exp -> exp -> exp
val evolutions : string
val initialisations : string
val constraints : string
val extend : name -> exp -> statement
val subst : exp -> exp -> exp -> exp
val l_subst : exp -> exp -> exp -> exp
val evolution : exp -> exp
val initial : exp -> exp
val pconstraint : exp -> exp
val ifthenelse : exp -> exp -> exp -> exp
val ( &~ ) : exp -> exp -> exp
val ( |~ ) : exp -> exp -> exp
val ( =>~ ) : exp -> exp -> exp
val a_const : exp -> exp
val a_var : exp -> exp -> exp -> exp -> exp
val a_part : exp -> exp -> exp -> exp -> exp
val a_inf : exp -> exp -> exp
val a_sup : exp -> exp -> exp
module Printer :
sig
val print : string -> processus list -> unit
end

664
compiler/minils/sigali/sigalimain.ml Normal file
View file

@ -0,0 +1,664 @@
(****************************************************)
(* *)
(* Heptagon/BZR *)
(* *)
(* Author : Gwenaël Delaval *)
(* Organization : INRIA Rennes, VerTeCs *)
(* *)
(****************************************************)
(* Translation from the source language to Sigali polynomial systems *)
(* $Id: dynamic_system.ml 2652 2011-03-11 16:26:17Z delaval $ *)
open Misc
open Compiler_utils
open Names
open Idents
open Types
open Clocks
open Sigali
type mtype = Tint | Tbool | Tother
let actual_ty = function
| Tid({ qual = "Pervasives"; name = "bool"}) -> Tbool
| Tid({ qual = "Pervasives"; name = "int"}) -> Tint
| _ -> Tother
let var_list prefix n =
let rec varl acc = function
| 0 -> acc
| n ->
let acc = (prefix ^ (string_of_int n)) :: acc in
varl acc (n-1) in
varl [] n
let dummy_prefix = "d"
let translate_static_exp se =
match se.se_desc with
| Sint(v) -> Cint(v)
| Sfloat(_) -> failwith("Sigali: floats not implemented")
| Sbool(true) -> Ctrue
| Sbool(false) -> Cfalse
| _ -> failwith("Sigali: untranslatable constant")
let rec translate_pat = function
| Minils.Evarpat(x) -> [name x]
| Minils.Etuplepat(pat_list) ->
List.fold_right (fun pat acc -> (translate_pat pat) @ acc) pat_list []
let rec translate_ck pref e = function
| Cbase | Cvar { contents = Cindex _ } ->
e
| Cvar { contents = Clink ck } -> translate_ck pref e ck
| Con(ck,c,var) ->
let e = translate_ck pref e ck in
Swhen(e,
match (shortname c) with
"true" -> Svar(pref ^ (name var))
| "false" -> Snot(Svar(pref ^ (name var)))
| _ -> assert false)
(* [translate e = c] *)
let rec translate prefix ({ Minils.e_desc = desc; Minils.e_ty = ty } as e) =
match desc with
| Minils.Econst(v) ->
begin match (actual_ty ty) with
| Tbool -> Sconst(translate_static_exp v)
| Tint -> a_const (Sconst(translate_static_exp v))
| Tother -> failwith("Sigali: untranslatable type")
end
| Minils.Evar(n) -> Svar(prefix ^ (name n))
| Minils.Eapp (* pervasives binary or unary stateless operations *)
({ Minils.a_op = Minils.Efun({qual="Pervasives";name=n})},
e_list, _) ->
begin
match n, e_list with
| "not", [e] -> Snot(translate prefix e)
| "or", [e1;e2] -> Sor((translate prefix e1),(translate prefix e2))
| "&", [e1;e2] -> Sand((translate prefix e1),(translate prefix e2))
(* a_inf and a_sup : +1 to translate ideals to boolean
polynomials *)
| ("<="|"<"|">="|">"), [e1;e2] ->
let op,modv =
begin match n with
| "<=" -> a_inf,0
| "<" -> a_inf,-1
| ">=" -> a_sup,0
| _ -> a_sup,1
end in
let e1 = translate prefix e1 in
begin match e2.Minils.e_desc with
| Minils.Econst({se_desc = Sint(v)}) ->
let e = op e1 (Sconst(Cint(v+modv))) in
Splus(e,Sconst(Ctrue))
| _ ->
let e2 = translate prefix e2 in
let e = op (Sminus(e1,e2)) (Sconst(Cint(modv))) in
Splus(e,Sconst(Ctrue))
end
| "+", [e1;e2] -> Splus((translate prefix e1),(translate prefix e2))
| "-", [e1;e2] -> Sminus((translate prefix e1),(translate prefix e2))
| "*", [e1;e2] -> Sprod((translate prefix e1),(translate prefix e2))
| ("="
| "<>"),_ -> failwith("Sigali: '=' or '<>' not yet implemented")
| _ -> assert false
end
| Minils.Ewhen(e, c, var) when ((actual_ty e.Minils.e_ty) = Tbool) ->
let e = translate prefix e in
Swhen(e,
match (shortname c) with
"true" -> Svar(prefix ^ (name var))
| "false" -> Snot(Svar(prefix ^ (name var)))
| _ -> assert false)
| Minils.Ewhen(e, _c, _var) ->
translate prefix e
| Minils.Emerge(ck,[(c1,e1);(_c2,e2)]) ->
let e1 = translate prefix e1 in
let e2 = translate prefix e2 in
let e1,e2 =
begin
match (shortname c1) with
"true" -> e1,e2
| "false" -> e2,e1
| _ -> assert false
end in
let var_ck = Svar(prefix ^ (name ck)) in
begin match (actual_ty e.Minils.e_ty) with
| Tbool -> Sdefault(Swhen(e1,var_ck),e2)
| Tint -> a_part var_ck (a_const (Sconst(Cint(0)))) e1 e2
| Tother -> assert false
end
| Minils.Estruct(_) ->
failwith("Sigali: structures not implemented")
| Minils.Eiterator(_,_,_,_,_) ->
failwith("Sigali: iterators not implemented")
| Minils.Eapp({Minils.a_op = Minils.Enode(_)},_,_) ->
failwith("Sigali: node in expressions; programs should be normalized")
| Minils.Efby(_,_) ->
failwith("Sigali: fby in expressions; programs should be normalized")
| Minils.Eapp(_,_,_) -> failwith("Sigali: not supported application")
| Minils.Emerge(_, _) -> assert false
let rec translate_eq env f
(acc_dep,acc_states,acc_init,acc_inputs,acc_ctrl,acc_cont,acc_eqs)
{ Minils.eq_lhs = pat; Minils.eq_rhs = e } =
let prefix = f ^ "_" in
let prefixed n = prefix ^ n in
let { Minils.e_desc = desc; Minils.e_ck = ck } = e in
match pat, desc with
| Minils.Evarpat(n), Minils.Efby(opt_c, e) ->
let sn = prefixed (name n) in
let sm = prefix ^ "mem_" ^ (name n) in
(* let acc_eqs = *)
(* (extend *)
(* constraints *)
(* (Slist[Sequal(Ssquare(Svar(sn)),Sconst(Ctrue))]))::acc_eqs in *)
let acc_eqs,acc_init =
match opt_c with
| None -> acc_eqs,Cfalse::acc_init
| Some(c) ->
let c = translate_static_exp c in
(extend
initialisations
(Slist[Sequal(Svar(sn),Sconst(c))]))::acc_eqs,
c::acc_init
in
let e_next = translate prefix e in
let e_next = translate_ck prefix e_next ck in
acc_dep,
sn::acc_states,
acc_init,acc_inputs,acc_ctrl,acc_cont,
(extend
evolutions
(Slist[Sdefault(e_next,Svar(sn))]))
(* TODO *)
(* ::{ stmt_name = sn; *)
(* stmt_def = translate_ck prefix (Svar(sm)) ck } *)
::acc_eqs
| pat, Minils.Eapp({ Minils.a_op = Minils.Enode g_name;
Minils.a_id = Some a_id;
Minils.a_inlined = inlined }, e_list, None) ->
(*
g : n states (gq1,...,gqn), p inputs (gi1,...,gip), m outputs (go1,...,gom)
case inlined :
var_g : [gq1,...,gqn,gi1,...,gip]
var_inst_g : [hq1,...,hqn,e1,...,en]
case non inlined :
add inputs go1',...,gom'
var_g : [gq1,...,gqn,gi1,...,gip,go1,...,gom]
var_inst_g : [hq1,...,hqn,e1,...,en,go1',...,gom']
declare(d1,...,dn)
d : [d1,...,dn]
% q1 = if ck then d1 else hq1 %
q1 : d1 when ck default hq1
...
qn : dn when ck default hqn
% P_inst = P[var_inst_g/var_g] %
evol_g : l_subst(evolution(g),var_g,var_inst_g);
evolutions : concat(evolutions,l_subst([q1,...,qn],[d1,...,dn],evol_g)
initialisations : concat(initialisations, [subst(initial(g),var_g,var_inst_g)])
constraints : concat(constraints, [subst(constraint(g),var_g,var_inst_g)])
case inlined :
ho1 : subst(go1,var_g,var_inst_g)
...
hom : subst(gom,var_g,var_inst_g)
case non inlined :
(nothing)
*)
let g_name = shortname g_name in
let (g_p,g_p_contract) = NamesEnv.find g_name env in
let g = if inlined then g_name else g_name ^ "_contract" in
(* add dependency *)
let acc_dep = g :: acc_dep in
let name_list = translate_pat pat in
let g_p = if inlined then g_p else g_p_contract in
(* var_g : [gq1,...,gqn,gi1,...,gip] *)
let var_g = "var_" ^ g in
let vars =
match inlined with
| true -> g_p.proc_states @ g_p.proc_inputs
| false -> g_p.proc_states @ g_p.proc_inputs @ g_p.proc_outputs in
let acc_eqs =
{ stmt_name = var_g;
stmt_def = Slist(List.map (fun v -> Svar(v)) vars) }::acc_eqs in
(* var_inst_g : [hq1,...,hqn,e1,...,en] *)
let var_inst_g = "var_inst_" ^ g in
(* Coding contract states : S_n_id_s *)
(* id being the id of the application *)
(* n being the length of id *)
(* s being the name of the state*)
let a_id = (name a_id) in
let id_length = String.length a_id in
let s_prefix = "S_" ^ (string_of_int id_length) ^ "_" ^ a_id ^ "_" in
let new_states_list =
List.map
(fun g_state ->
(* Remove "g_" prefix *)
let l = String.length g in
let s =
String.sub
g_state (l+1)
((String.length g_state)-(l+1)) in
prefixed (s_prefix ^ s))
g_p.proc_states in
let e_states = List.map (fun hq -> Svar(hq)) new_states_list in
let e_list = List.map (translate prefix) e_list in
let e_outputs,acc_inputs =
match inlined with
| true -> [],acc_inputs
| false ->
let new_outputs =
List.map (fun name -> prefixed name) name_list in
(List.map (fun v -> Svar(v)) new_outputs),(acc_inputs@new_outputs) in
let vars_inst = e_states@e_list@e_outputs in
let acc_eqs =
{ stmt_name = var_inst_g;
stmt_def = Slist(vars_inst); }::acc_eqs in
let acc_states = List.rev_append new_states_list acc_states in
let acc_init = List.rev_append g_p.proc_init acc_init in
(* declare(d1,...,dn) *)
let dummy_list = var_list dummy_prefix (List.length g_p.proc_states) in
(* d : [d1,...dn] *)
let acc_eqs =
{stmt_name = dummy_prefix;
stmt_def = Slist(List.map (fun di -> Svar(di)) dummy_list)}::acc_eqs in
(* qi = di when ck default hqi *)
let q_list = List.map (fun _ -> "q_" ^ (gen_symbol ())) g_p.proc_states in
let e_list =
List.map2
(fun hq d ->
let e = Svar(d) in
let e = translate_ck (prefixed "") e ck in
Sdefault(e,Svar(hq)))
new_states_list dummy_list in
let acc_eqs =
List.fold_left2
(fun acc_eqs q e -> {stmt_name = q; stmt_def = e}::acc_eqs)
acc_eqs q_list e_list in
(* evol_g : l_subst(evolution(g),var_g,var_inst_g); *)
let evol_g = "evol_" ^ g in
let acc_eqs =
{stmt_name = evol_g;
stmt_def = l_subst (evolution (Svar g)) (Svar var_g) (Svar var_inst_g)}
::acc_eqs in
(* evolutions : concat(evolutions,l_subst([q1,...,qn],[d1,...,dn],evol_g) *)
let acc_eqs =
(extend evolutions (l_subst
(Slist (List.map (fun q -> Svar(q)) q_list))
(Slist (List.map (fun d -> Svar(d)) dummy_list))
(Svar evol_g)))
::acc_eqs in
(* initialisations : concat(initialisations, [subst(initial(g),var_g,var_inst_g)]) *)
let acc_eqs =
(extend initialisations (Slist[subst
(initial (Svar g))
(Svar var_g)
(Svar var_inst_g)]))
:: acc_eqs in
(* constraints : concat(constraints, [subst(constraint(g),var_g,var_inst_g)]) *)
let acc_eqs =
(extend constraints (Slist[subst
(pconstraint (Svar g))
(Svar var_g)
(Svar var_inst_g)]))
::acc_eqs in
(* if inlined, hoi : subst(goi,var_g,var_inst_g) *)
let acc_eqs =
match inlined with
| true ->
List.fold_left2
(fun acc_eqs o go ->
{stmt_name = prefixed o;
stmt_def = subst (Svar(go)) (Svar(var_g)) (Svar(var_inst_g))}
::acc_eqs)
acc_eqs name_list g_p.proc_outputs
| false -> acc_eqs in
(* assume & guarantee *)
(* f_g_assume_x : subst(g_assume,var_g,var_inst_g) *)
(* f_g_guarantee_x : subst(g_guarantee,var_g,var_inst_g) *)
let var_assume = prefixed (g ^ "_assume_" ^ (gen_symbol ())) in
let var_guarantee = prefixed (g ^ "_guarantee_" ^ (gen_symbol ())) in
let acc_eqs =
{stmt_name = var_assume;
stmt_def = subst (Svar(g ^ "_assume")) (Svar(var_g)) (Svar(var_inst_g))} ::
{stmt_name = var_guarantee;
stmt_def = subst (Svar(g ^ "_guarantee")) (Svar(var_g)) (Svar(var_inst_g))} ::
acc_eqs in
let acc_cont =
(Svar(var_assume),Svar(var_guarantee)) :: acc_cont in
acc_dep,acc_states,acc_init,
acc_inputs,acc_ctrl,acc_cont,acc_eqs
| pat, Minils.Eapp({ Minils.a_op = Minils.Enode g_name;
Minils.a_id = Some a_id;
Minils.a_inlined = inlined }, e_list, Some r) ->
(*
g : n states (gq1,...,gqn), p inputs (gi1,...,gip),
n init states (gq1_0,...,gqn_0)
case inlined :
var_g : [gq1,...,gqn,gi1,...,gip]
var_inst_g : [hq1,...,hqn,e1,...,en]
case non inlined :
add inputs go1',...,gom'
var_g : [gq1,...,gqn,gi1,...,gip,go1,...,gom]
var_inst_g : [hq1,...,hqn,e1,...,en,go1',...,gom']
declare(d1,...,dn)
d : [d1,...,dn]
% q1 = if ck then (if r then gq1_0 else d1) else hq1 %
q1 : (gq1_0 when r default d1) when ck default hq1
...
qn : (gqn_0 when r default dn) when ck default hqn
% P_inst = P[var_inst_g/var_g] %
evol_g : l_subst(evolution(g),var_g,var_inst_g);
evolutions : concat(evolutions,l_subst([q1,...,qn],[d1,...,dn],evol_g)
initialisations : concat(initialisations, [subst(initial(g),var_g,var_inst_g)])
constraints : concat(constraints, [subst(constraint(g),var_g,var_inst_g)])
case inlined :
ho1 : subst(go1,var_g,var_inst_g)
...
hom : subst(gom,var_g,var_inst_g)
case non inlined :
(nothing)
*)
let g_name = shortname g_name in
let (g_p,g_p_contract) = NamesEnv.find g_name env in
let g = if inlined then g_name else g_name ^ "_contract" in
(* add dependency *)
let acc_dep = g :: acc_dep in
let name_list = translate_pat pat in
let g_p = if inlined then g_p else g_p_contract in
(* var_g : [gq1,...,gqn,gi1,...,gip] *)
let var_g = "var_" ^ g in
let vars =
match inlined with
| true -> g_p.proc_states @ g_p.proc_inputs
| false -> g_p.proc_states @ g_p.proc_inputs @ g_p.proc_outputs in
let acc_eqs =
{ stmt_name = var_g;
stmt_def = Slist(List.map (fun v -> Svar(v)) vars) }::acc_eqs in
(* var_inst_g : [hq1,...,hqn,e1,...,en] *)
let var_inst_g = "var_inst_" ^ g in
(* Coding contract states : S_n_id_s *)
(* id being the id of the application *)
(* n being the length of id *)
(* s being the name of the state*)
let a_id = name a_id in
let id_length = String.length a_id in
let s_prefix = "S_" ^ (string_of_int id_length) ^ "_" ^ a_id ^ "_" in
let new_states_list =
List.map
(fun g_state ->
(* Remove "g_" prefix *)
let l = (String.length g) in
let s =
String.sub
g_state (l+1)
((String.length g_state)-(l+1)) in
prefixed (s_prefix ^ s))
g_p.proc_states in
let e_states = List.map (fun hq -> Svar(hq)) new_states_list in
let e_list = List.map (translate prefix) e_list in
let e_outputs,acc_inputs =
match inlined with
| true -> [],acc_inputs
| false ->
let new_outputs =
List.map (fun name -> prefixed name) name_list in
(List.map (fun v -> Svar(v)) new_outputs),(acc_inputs@new_outputs) in
let vars_inst = e_states@e_list@e_outputs in
let acc_eqs =
{ stmt_name = var_inst_g;
stmt_def = Slist(vars_inst); }::acc_eqs in
let acc_states = List.rev_append new_states_list acc_states in
let acc_init = List.rev_append g_p.proc_init acc_init in
(* declare(d1,...,dn) *)
let dummy_list = var_list dummy_prefix (List.length g_p.proc_states) in
(* d : [d1,...dn] *)
let acc_eqs =
{stmt_name = dummy_prefix;
stmt_def = Slist(List.map (fun di -> Svar(di)) dummy_list)}::acc_eqs in
(* qi = (gqi_0 when r default di) when ck default hqi *)
let q_list = List.map (fun _ -> "q_" ^ (gen_symbol ())) g_p.proc_states in
let e_list =
List.map2
(fun (q0,hq) d ->
let e = Sdefault(Swhen(Sconst(q0),
Svar(prefixed (name r))),Svar(d)) in
let e = translate_ck (prefixed "") e ck in
Sdefault(e,Svar(hq)))
(List.combine g_p.proc_init new_states_list) dummy_list in
let acc_eqs =
List.fold_left2
(fun acc_eqs q e -> {stmt_name = q; stmt_def = e}::acc_eqs)
acc_eqs q_list e_list in
(* evol_g : l_subst(evolution(g),var_g,var_inst_g); *)
let evol_g = "evol_" ^ g in
let acc_eqs =
{stmt_name = evol_g;
stmt_def = l_subst (evolution (Svar g)) (Svar var_g) (Svar var_inst_g)}
::acc_eqs in
(* evolutions : concat(evolutions,l_subst([q1,...,qn],[d1,...,dn],evol_g) *)
let acc_eqs =
(extend evolutions (l_subst
(Slist (List.map (fun q -> Svar(q)) q_list))
(Slist (List.map (fun d -> Svar(d)) dummy_list))
(Svar evol_g)))
::acc_eqs in
(* initialisations : concat(initialisations, [subst(initial(g),var_g,var_inst_g)]) *)
let acc_eqs =
(extend initialisations (Slist[subst
(initial (Svar g))
(Svar var_g)
(Svar var_inst_g)]))
:: acc_eqs in
(* constraints : concat(constraints, [subst(constraint(g),var_g,var_inst_g)]) *)
let acc_eqs =
(extend constraints (Slist[subst
(pconstraint (Svar g))
(Svar var_g)
(Svar var_inst_g)]))
::acc_eqs in
(* if inlined, hoi : subst(goi,var_g,var_inst_g) *)
let acc_eqs =
match inlined with
| true ->
List.fold_left2
(fun acc_eqs o go ->
{stmt_name = prefixed o;
stmt_def = subst (Svar(go)) (Svar(var_g)) (Svar(var_inst_g))}
::acc_eqs)
acc_eqs name_list g_p.proc_outputs
| false -> acc_eqs in
(* assume & guarantee *)
(* f_g_assume_x : subst(g_assume,var_g,var_inst_g) *)
(* f_g_guarantee_x : subst(g_guarantee,var_g,var_inst_g) *)
let var_assume = prefixed (g ^ "_assume_" ^ (gen_symbol ())) in
let var_guarantee = prefixed (g ^ "_guarantee_" ^ (gen_symbol ())) in
let acc_eqs =
{stmt_name = var_assume;
stmt_def = subst (Svar(g ^ "_assume")) (Svar(var_g)) (Svar(var_inst_g))} ::
{stmt_name = var_guarantee;
stmt_def = subst (Svar(g ^ "_guarantee")) (Svar(var_g)) (Svar(var_inst_g))} ::
acc_eqs in
let acc_cont =
(Svar(var_assume),Svar(var_guarantee)) :: acc_cont in
acc_dep,acc_states,acc_init,
acc_inputs,acc_ctrl,acc_cont,acc_eqs
| Minils.Evarpat(n), _ ->
(* assert : no fby, no node application in e *)
let e' = translate prefix e in
let e' =
begin match (actual_ty e.Minils.e_ty) with
| Tbool -> translate_ck prefix e' ck
| _ -> e'
end in
acc_dep,acc_states,acc_init,
acc_inputs,acc_ctrl,acc_cont,
{ stmt_name = prefixed (name n);
stmt_def = e' }::acc_eqs
| _ -> assert false
let translate_eq_list env f eq_list =
List.fold_left
(fun (acc_dep,acc_states,acc_init,
acc_inputs,acc_ctrl,acc_cont,acc_eqs) eq ->
translate_eq
env f
(acc_dep,acc_states,acc_init,
acc_inputs,acc_ctrl,acc_cont,acc_eqs)
eq)
([],[],[],[],[],[],[])
eq_list
let translate_contract env f contract =
let prefix = f ^ "_" in
let var_a = prefix ^ "assume" in
let var_g = prefix ^ "guarantee" in
match contract with
| None ->
let body =
[{ stmt_name = var_g; stmt_def = Sconst(Ctrue) };
{ stmt_name = var_a; stmt_def = Sconst(Ctrue) }] in
[],[],[],body,(Svar(var_a),Svar(var_g)),[]
| Some {Minils.c_local = _locals;
Minils.c_eq = l_eqs;
Minils.c_assume = e_a;
Minils.c_enforce = e_g;
Minils.c_controllables = cl} ->
let dep,states,init,inputs,
controllables,_contracts,body =
translate_eq_list env f l_eqs in
assert (inputs = []);
assert (controllables = []);
let e_a = translate prefix e_a in
let e_g = translate prefix e_g in
let body =
{stmt_name = var_g; stmt_def = e_g} ::
{stmt_name = var_a; stmt_def = e_a} ::
body in
let controllables =
List.map (fun { Minils.v_ident = id } -> prefix ^ (name id)) cl in
dep,states,init,body,(Svar(var_a),Svar(var_g)),controllables
let rec build_environment contracts =
match contracts with
| [] -> [],Sconst(Ctrue)
| [a,g] -> [a =>~ g],g
| (a,g)::l ->
let conts,assumes = build_environment l in
((a =>~ g) :: conts),(g &~ assumes)
let translate_node env
({ Minils.n_name = {name = f};
Minils.n_input = i_list; Minils.n_output = o_list;
Minils.n_local = _d_list; Minils.n_equs = eq_list;
Minils.n_contract = contract } as node) =
(* every variable is prefixed by its node name *)
let inputs =
List.map
(fun { Minils.v_ident = v } -> f ^ "_" ^ (name v)) i_list in
let outputs =
List.map
(fun { Minils.v_ident = v } -> f ^ "_" ^ (name v)) o_list in
let dep,states,init,add_inputs,add_controllables,contracts,body =
translate_eq_list env f eq_list in
let dep_c,states_c,init_c,body_c,(a_c,g_c),controllables =
translate_contract env f contract in
let inputs = inputs @ add_inputs in
let controllables = controllables @ add_controllables in
let body = List.rev body in
let states = List.rev states in
let body_c = List.rev body_c in
let states_c = List.rev states_c in
let constraints =
List.map
(fun v -> Sequal(Ssquare(Svar(v)),Sconst(Ctrue)))
(inputs@controllables) in
let contracts_components,assumes_components =
build_environment contracts in
let constraints = constraints @
contracts_components @ [Sequal (a_c,Sconst(Ctrue))] in
let impl = g_c &~ assumes_components in
let obj = Security(impl) in
let p = { proc_dep = unique (dep @ dep_c);
proc_name = f;
proc_inputs = inputs@controllables;
proc_uncont_inputs = inputs;
proc_outputs = outputs;
proc_controllables = controllables;
proc_states = states@states_c;
proc_init = init@init_c;
proc_constraints = constraints;
proc_body = body@body_c;
proc_objectives = [obj] } in
(* Hack : save inputs and states names for controller call *)
let remove_prefix =
let n = String.length f in
fun s ->
String.sub s (n+1) ((String.length s) - (n+1)) in
node.Minils.n_controller_call <-
(List.map remove_prefix inputs,
List.map remove_prefix (states@states_c));
let f_contract = f ^ "_contract" in
let inputs_c =
List.map
(fun { Minils.v_ident = v } -> f_contract ^ "_" ^ (name v)) i_list in
let outputs_c =
List.map
(fun { Minils.v_ident = v } -> f_contract ^ "_" ^ (name v)) o_list in
let dep_c,states_c,init_c,body_c,(_a_c,_g_c),_controllables =
translate_contract env f_contract contract in
let states_c = List.rev states_c in
let body_c = List.rev body_c in
let constraints_c =
List.map
(fun v -> Sequal(Ssquare(Svar(v)),Sconst(Ctrue)))
(inputs_c@outputs_c) in
let p_c = { proc_dep = dep_c;
proc_name = f ^ "_contract";
proc_inputs = inputs_c@outputs_c;
proc_uncont_inputs = inputs_c@outputs_c;
proc_outputs = [];
proc_controllables = [];
proc_states = states_c;
proc_init = init_c;
proc_constraints = constraints_c;
proc_body = body_c;
proc_objectives = [] } in
(NamesEnv.add f (p,p_c) env), (p,p_c)
let program p =
let _env,acc_proc =
List.fold_left
(fun (env,acc) node ->
let env,(proc,contract) = translate_node env node in
env,contract::proc::acc)
(NamesEnv.empty,[])
p.Minils.p_nodes in
let procs = List.rev acc_proc in
let filename = filename_of_name p.Minils.p_modname in
let dirname = build_path (filename ^ "_z3z") in
let dir = clean_dir dirname in
Sigali.Printer.print dir procs

14
compiler/minils/sigali/sigalimain.mli Normal file
View file

@ -0,0 +1,14 @@
(****************************************************)
(* *)
(* Heptagon/BZR *)
(* *)
(* Author : Gwenaël Delaval *)
(* Organization : Univ. Grenoble, LIG *)
(* *)
(****************************************************)
(* Translation from the source language to Sigali polynomial systems *)
(* $Id$ *)
val program : Minils.program -> unit