Merge branch 'bzr' into decade
- Added Boolean module (enum types to boolean vectors) - Added Hept_clocking analysis, called before Boolean - Added z3z target from minils (sigali format) - Bug corrections in Normalize, Normalize_mem Conflicts: compiler/heptagon/analysis/typing.ml compiler/heptagon/heptagon.ml compiler/heptagon/parsing/hept_parser.mly compiler/heptagon/parsing/hept_parsetree.ml compiler/heptagon/parsing/hept_scoping.ml compiler/main/hept2mls.ml compiler/main/heptc.ml compiler/main/mls2seq.ml compiler/minils/minils.ml compiler/minils/transformations/normalize_mem.ml test/checkmaster
Gwenaël Delaval
13 years ago
commit
c57b71b6aa
@ -0,0 +1,279 @@
|
||||
(**************************************************************************)
|
||||
(* *)
|
||||
(* Heptagon *)
|
||||
(* *)
|
||||
(* Author : Marc Pouzet *)
|
||||
(* Organization : Demons, LRI, University of Paris-Sud, Orsay *)
|
||||
(* *)
|
||||
(**************************************************************************)
|
||||
(* clock checking *)
|
||||
|
||||
(* v_clock is expected to contain correct clocks before entering here :
|
||||
either explicit with Cbase representing the node activation clock
|
||||
or fresh_clock() for unannoted variables.
|
||||
Idem for e_ct : if explicit, it represents a clock annotation.
|
||||
Unification is done on this mutable fields.
|
||||
e_base_ck is set according to node signatures.
|
||||
|
||||
*)
|
||||
|
||||
open Misc
|
||||
open Idents
|
||||
open Heptagon
|
||||
open Hept_utils
|
||||
open Global_printer
|
||||
open Hept_printer
|
||||
open Signature
|
||||
open Types
|
||||
open Clocks
|
||||
open Location
|
||||
open Format
|
||||
|
||||
(** Error Kind *)
|
||||
type error_kind = | Etypeclash of ct * ct | Eclockclash of ck * ck | Edefclock
|
||||
|
||||
let error_message loc = function
|
||||
| Etypeclash (actual_ct, expected_ct) ->
|
||||
Format.eprintf "%aClock Clash: this expression has clock %a,@\n\
|
||||
but is expected to have clock %a.@."
|
||||
print_location loc
|
||||
print_ct actual_ct
|
||||
print_ct expected_ct;
|
||||
raise Errors.Error
|
||||
| Eclockclash (actual_ck, expected_ck) ->
|
||||
Format.eprintf "%aClock Clash: this value has clock %a,@\n\
|
||||
but is exprected to have clock %a.@."
|
||||
print_location loc
|
||||
print_ck actual_ck
|
||||
print_ck expected_ck;
|
||||
raise Errors.Error
|
||||
| Edefclock ->
|
||||
Format.eprintf "%aArguments defining clocks should be given as names@."
|
||||
print_location loc;
|
||||
raise Errors.Error
|
||||
|
||||
|
||||
let ck_of_name h x =
|
||||
if is_reset x
|
||||
then fresh_clock()
|
||||
else Env.find x h
|
||||
|
||||
let rec typing_pat h = function
|
||||
| Evarpat x -> Ck (ck_of_name h x)
|
||||
| Etuplepat pat_list -> Cprod (List.map (typing_pat h) pat_list)
|
||||
|
||||
let ident_list_of_pat pat =
|
||||
let rec f acc pat = match pat with
|
||||
| Evarpat id -> id::acc
|
||||
| Etuplepat pat_l -> List.fold_left f acc pat_l
|
||||
in
|
||||
List.rev (f [] pat)
|
||||
|
||||
(* typing the expression, returns ct, ck_base *)
|
||||
let rec typing h pat e =
|
||||
let ct,base = match e.e_desc with
|
||||
| Econst _ ->
|
||||
let ck = fresh_clock() in
|
||||
Ck ck, ck
|
||||
| Evar x ->
|
||||
let ck = ck_of_name h x in
|
||||
Ck ck, ck
|
||||
| Efby (e1, e2) ->
|
||||
let ct,ck = typing h pat e1 in
|
||||
expect h pat ct e2;
|
||||
ct, ck
|
||||
| Epre(_,e) ->
|
||||
typing h pat e
|
||||
| Ewhen (e,c,n) ->
|
||||
let ck_n = ck_of_name h n in
|
||||
let base = expect h pat (skeleton ck_n e.e_ty) e in
|
||||
skeleton (Con (ck_n, c, n)) e.e_ty, Con (ck_n, c, n)
|
||||
| Emerge (x, c_e_list) ->
|
||||
let ck = ck_of_name h x in
|
||||
List.iter (fun (c,e) -> expect h pat (Ck(Con (ck,c,x))) e) c_e_list;
|
||||
Ck ck, ck
|
||||
| Estruct l ->
|
||||
let ck = fresh_clock () in
|
||||
List.iter (fun (_, e) -> expect h pat (Ck ck) e) l;
|
||||
Ck ck, ck
|
||||
| Eapp({a_op = op}, args, _) -> (* hyperchronous reset *)
|
||||
let base_ck = fresh_clock () in
|
||||
let ct = typing_app h base_ck pat op args in
|
||||
ct, base_ck
|
||||
| Eiterator (it, {a_op = op}, nl, pargs, args, _) -> (* hyperchronous reset *)
|
||||
let base_ck = fresh_clock() in
|
||||
let ct = match it with
|
||||
| Imap -> (* exactly as if clocking the node *)
|
||||
typing_app h base_ck pat op (pargs@args)
|
||||
| Imapi -> (* clocking the node with the extra i input on [ck_r] *)
|
||||
let il (* stubs i as 0 *) =
|
||||
List.map (fun x -> mk_exp
|
||||
(Econst (Initial.mk_static_int 0))
|
||||
~ct_annot:(Some(Ck(base_ck)))
|
||||
Initial.tint
|
||||
) nl
|
||||
in
|
||||
typing_app h base_ck pat op (pargs@args@il)
|
||||
| Ifold | Imapfold ->
|
||||
(* clocking node with equality constaint on last input and last output *)
|
||||
let ct = typing_app h base_ck pat op (pargs@args) in
|
||||
Misc.optional (unify (Ck(Clocks.last_clock ct)))
|
||||
(Misc.last_element args).e_ct_annot;
|
||||
ct
|
||||
| Ifoldi -> (* clocking the node with the extra i and last in/out constraints *)
|
||||
let il (* stubs i as 0 *) =
|
||||
List.map (fun x -> mk_exp
|
||||
(Econst (Initial.mk_static_int 0))
|
||||
~ct_annot:(Some(Ck(base_ck)))
|
||||
Initial.tint
|
||||
) nl
|
||||
in
|
||||
let rec insert_i args = match args with
|
||||
| [] -> il
|
||||
| [l] -> il @ [l]
|
||||
| h::l -> h::(insert_i l)
|
||||
in
|
||||
let ct = typing_app h base_ck pat op (pargs@(insert_i args)) in
|
||||
Misc.optional (unify (Ck (Clocks.last_clock ct)))
|
||||
(Misc.last_element args).e_ct_annot;
|
||||
ct
|
||||
in
|
||||
ct, base_ck
|
||||
| Esplit _ | Elast _ -> assert false
|
||||
in
|
||||
begin match e.e_ct_annot with
|
||||
None -> ()
|
||||
| Some e_ct ->
|
||||
try
|
||||
unify ct e_ct
|
||||
with Unify ->
|
||||
eprintf "Incoherent clock annotation.@\n";
|
||||
error_message e.e_loc (Etypeclash (ct,e_ct));
|
||||
end;
|
||||
e.e_ct_annot <- Some(ct);
|
||||
ct, base
|
||||
|
||||
and expect h pat expected_ct e =
|
||||
let actual_ct,base = typing h pat e in
|
||||
(try unify actual_ct expected_ct
|
||||
with Unify -> error_message e.e_loc (Etypeclash (actual_ct, expected_ct)))
|
||||
|
||||
and typing_app h base pat op e_list = match op with
|
||||
| Etuple (* to relax ? *)
|
||||
| Earrow
|
||||
| Efun _ (* stateless functions: inputs and outputs on the same clock *)
|
||||
| Earray_fill | Eselect | Eselect_dyn | Eselect_trunc | Eupdate
|
||||
| Eselect_slice | Econcat | Earray | Efield | Efield_update | Eifthenelse ->
|
||||
List.iter (expect h pat (Ck base)) e_list;
|
||||
Ck base
|
||||
| Enode f ->
|
||||
let node = Modules.find_value f in
|
||||
let pat_id_list = ident_list_of_pat pat in
|
||||
let rec build_env a_l v_l env = match a_l, v_l with
|
||||
| [],[] -> env
|
||||
| a::a_l, v::v_l -> (match a.a_name with
|
||||
| None -> build_env a_l v_l env
|
||||
| Some n -> build_env a_l v_l ((n,v)::env))
|
||||
| _ ->
|
||||
Printf.printf "Fun/node : %s\n" (Names.fullname f);
|
||||
Misc.internal_error "Clocking, non matching signature"
|
||||
in
|
||||
let env_pat = build_env node.node_outputs pat_id_list [] in
|
||||
let env_args = build_env node.node_inputs e_list [] in
|
||||
(* implement with Cbase as base, replace name dep by ident dep *)
|
||||
let rec sigck_to_ck sck = match sck with
|
||||
| Signature.Cbase -> base
|
||||
| Signature.Con (sck,c,x) ->
|
||||
(* find x in the envs : *)
|
||||
let id = try List.assoc x env_pat
|
||||
with Not_found ->
|
||||
try
|
||||
let e = List.assoc x env_args in
|
||||
(match e.e_desc with
|
||||
| Evar id -> id
|
||||
| _ -> error_message e.e_loc Edefclock)
|
||||
with Not_found ->
|
||||
Misc.internal_error "Clocking, non matching signature 2"
|
||||
in
|
||||
Clocks.Con (sigck_to_ck sck, c, id)
|
||||
in
|
||||
List.iter2
|
||||
(fun a e -> expect h pat (Ck(sigck_to_ck a.a_clock)) e)
|
||||
node.node_inputs e_list;
|
||||
Clocks.prod (List.map (fun a -> sigck_to_ck a.a_clock) node.node_outputs)
|
||||
|
||||
let append_env h vds =
|
||||
List.fold_left (fun h { v_ident = n; v_clock = ck } -> Env.add n ck h) h vds
|
||||
|
||||
let rec typing_eq h ({ eq_desc = desc; eq_loc = loc } as eq) =
|
||||
match desc with
|
||||
| Eeq(pat,e) ->
|
||||
let ct,_ = typing h pat e in
|
||||
let pat_ct = typing_pat h pat in
|
||||
(try unify ct pat_ct
|
||||
with Unify ->
|
||||
eprintf "Incoherent clock between right and left side of the equation.@\n";
|
||||
error_message loc (Etypeclash (ct, pat_ct)))
|
||||
| Eblock b ->
|
||||
ignore(typing_block h b)
|
||||
| _ -> assert false
|
||||
|
||||
and typing_eqs h eq_list = List.iter (typing_eq h) eq_list
|
||||
|
||||
and typing_block h
|
||||
({ b_local = l; b_equs = eq_list; b_loc = loc } as b) =
|
||||
let h' = append_env h l in
|
||||
typing_eqs h' eq_list;
|
||||
h'
|
||||
|
||||
let typing_contract h contract =
|
||||
match contract with
|
||||
| None -> h
|
||||
| Some { c_block = b;
|
||||
c_assume = e_a;
|
||||
c_enforce = e_g;
|
||||
c_controllables = c_list } ->
|
||||
let h' = typing_block h b in
|
||||
(* assumption *)
|
||||
expect h' (Etuplepat []) (Ck Cbase) e_a;
|
||||
(* property *)
|
||||
expect h' (Etuplepat []) (Ck Cbase) e_g;
|
||||
append_env h c_list
|
||||
|
||||
let args_of_var_decs =
|
||||
List.map (fun vd -> Signature.mk_arg (Some (Idents.source_name vd.v_ident))
|
||||
vd.v_type (Signature.ck_to_sck vd.v_clock))
|
||||
|
||||
let signature_of_node n =
|
||||
{ node_inputs = args_of_var_decs n.n_input;
|
||||
node_outputs = args_of_var_decs n.n_output;
|
||||
node_stateful = n.n_stateful;
|
||||
node_params = n.n_params;
|
||||
node_param_constraints = n.n_param_constraints;
|
||||
node_loc = n.n_loc }
|
||||
|
||||
let typing_node node =
|
||||
let h0 = append_env Env.empty node.n_input in
|
||||
let h0 = append_env h0 node.n_output in
|
||||
let h = typing_contract h0 node.n_contract in
|
||||
typing_block h node.n_block;
|
||||
(* synchronize input and output on base : find the free vars and set them to base *)
|
||||
Env.iter (fun _ ck -> unify_ck Cbase (root_ck_of ck)) h0;
|
||||
(*update clock info in variables descriptions *)
|
||||
let set_clock vd = { vd with v_clock = ck_repr (Env.find vd.v_ident h) } in
|
||||
let node = { node with n_input = List.map set_clock node.n_input;
|
||||
n_output = List.map set_clock node.n_output }
|
||||
in
|
||||
(* check signature causality and update it in the global env *)
|
||||
let sign = signature_of_node node in
|
||||
Signature.check_signature sign;
|
||||
Modules.replace_value node.n_name sign;
|
||||
node
|
||||
|
||||
let program p =
|
||||
let program_desc pd = match pd with
|
||||
| Pnode nd -> Pnode (typing_node nd)
|
||||
| _ -> pd
|
||||
in
|
||||
{ p with p_desc = List.map program_desc p.p_desc; }
|
||||
|
||||
@ -0,0 +1,896 @@
|
||||
(****************************************************)
|
||||
(* *)
|
||||
(* Heptagon/BZR *)
|
||||
(* *)
|
||||
(* Author : Gwenaël Delaval *)
|
||||
(* Organization : INRIA Rennes, VerTeCs *)
|
||||
(* *)
|
||||
(****************************************************)
|
||||
|
||||
(*
|
||||
Translate enumerated types (state variables) into boolean
|
||||
|
||||
type t = A | B | C | D
|
||||
|
||||
A --> 00
|
||||
B --> 01
|
||||
C --> 10
|
||||
D --> 11
|
||||
|
||||
x : t --> x1,x2,x2_0,x2_1 : bool (x2_i for keeping correct clocks)
|
||||
|
||||
x = B;
|
||||
-->
|
||||
(x1,x2) = (0,1);
|
||||
x2_0 = x2 when False(x1);
|
||||
x2_1 = x2 when True(x1);
|
||||
|
||||
(e when A(x))
|
||||
-->
|
||||
(e when False(x1)) when False(x2_0)
|
||||
|
||||
ck on A(x)
|
||||
-->
|
||||
ck on False(x1) on False(x2_0)
|
||||
|
||||
merge x (A -> e0) (B -> e1) (C -> e2) (D -> e3)
|
||||
-->
|
||||
merge x1 (False -> merge x2_0 (False -> e0) (True -> e1))
|
||||
(True -> merge x2_1 (False -> e2) (True -> e3))
|
||||
*)
|
||||
|
||||
(* $Id: boolean.ml 833 2010-02-10 14:15:00Z delaval $ *)
|
||||
|
||||
open Names
|
||||
open Location
|
||||
open Idents
|
||||
open Signature
|
||||
open Types
|
||||
open Clocks
|
||||
open Heptagon
|
||||
open Hept_utils
|
||||
|
||||
let fresh = Idents.gen_fresh "bool" (fun s -> s)
|
||||
|
||||
let ty_bool = Tid({ qual = Pervasives; name = "bool"})
|
||||
|
||||
let strue = mk_static_exp ty_bool (Sbool(true))
|
||||
let sfalse = mk_static_exp ty_bool (Sbool(false))
|
||||
|
||||
let sbool = function
|
||||
| true -> strue
|
||||
| false -> sfalse
|
||||
|
||||
let ctrue = { qual = Pervasives; name = "true" }
|
||||
let cfalse = { qual = Pervasives; name = "false" }
|
||||
|
||||
let mk_tuple e_l =
|
||||
Eapp((mk_app Etuple),e_l,None)
|
||||
|
||||
(* boolean decision tree ; left branch for true ; nodes are constructors *)
|
||||
type btree = Node of constructor_name option | Tree of btree * btree
|
||||
|
||||
(* Debug
|
||||
let print_indent n =
|
||||
for i = 1 to n do
|
||||
Printf.printf " "
|
||||
done
|
||||
|
||||
let rec print_btree indent bt =
|
||||
match bt with
|
||||
| Node(None) ->
|
||||
print_indent indent;
|
||||
Printf.printf "None\n"
|
||||
| Node(Some c) ->
|
||||
print_indent indent;
|
||||
Printf.printf "%s\n" (fullname c)
|
||||
| Tree(t1,t2) ->
|
||||
print_indent indent;
|
||||
Printf.printf "0\n";
|
||||
print_btree (indent+2) t1;
|
||||
print_indent indent;
|
||||
Printf.printf "1\n";
|
||||
print_btree (indent+2) t2
|
||||
*)
|
||||
|
||||
(* info associated to each enum type *)
|
||||
type enuminfo =
|
||||
{
|
||||
ty_nb_var : int; (* nb of boolean var representing this type *)
|
||||
ty_assoc : bool list QualEnv.t;
|
||||
ty_tree : btree
|
||||
}
|
||||
|
||||
(*
|
||||
let rec print_bl bl =
|
||||
match bl with
|
||||
| [] -> ()
|
||||
| b::bl ->
|
||||
Printf.printf "%s" (if b then "1" else "0");
|
||||
print_bl bl
|
||||
|
||||
let print_enuminfo info =
|
||||
Printf.printf "{ ty_nb_var = %d;\n ty_assoc = " info.ty_nb_var;
|
||||
QualEnv.fold
|
||||
(fun c l () ->
|
||||
Printf.printf "(%s : " (fullname c);
|
||||
print_bl l;
|
||||
Printf.printf "), ")
|
||||
info.ty_assoc ();
|
||||
Printf.printf ";\n ty_tree =\n";
|
||||
print_btree 0 info.ty_tree
|
||||
*)
|
||||
|
||||
(* ty_nb_var = n : var x of enum type will be represented by
|
||||
boolean variables x_1,...,x_n
|
||||
|
||||
ty_assoc(A) = [b_1,...,b_n] : constant A will be represented by
|
||||
x_1,...,x_n where x_i = b_i
|
||||
|
||||
assert length(ty_assoc(A)) = ty_nb_var
|
||||
*)
|
||||
|
||||
(* Type var_tree : variable binary tree, each variable being of clock
|
||||
of its direct father (false clock for left son, true for right son).
|
||||
|
||||
Then if x translates to (x1,x2)
|
||||
the corresponding var_tree is
|
||||
x1
|
||||
/ \
|
||||
x2_0 x2_1
|
||||
|
||||
x2_0 being on clock False(x1)
|
||||
x2_1 being on clock True(x1)
|
||||
*)
|
||||
type var_tree = Vempty | VNode of var_ident * var_tree * var_tree
|
||||
|
||||
(*
|
||||
let rec print_var_tree indent t =
|
||||
match t with
|
||||
| Vempty ->
|
||||
print_indent indent;
|
||||
Printf.printf "Empty\n"
|
||||
| VNode(v,t1,t2) ->
|
||||
print_indent indent;
|
||||
Printf.printf "0 : %s\n" (name v);
|
||||
print_var_tree (indent+2) t1;
|
||||
print_var_tree (indent+2) t2
|
||||
*)
|
||||
|
||||
type varinfo =
|
||||
{
|
||||
var_enum : enuminfo;
|
||||
var_list : var_ident list;
|
||||
clocked_var : var_tree;
|
||||
}
|
||||
|
||||
(*
|
||||
let print_varinfo info =
|
||||
Printf.printf "{ var_enum = \n";
|
||||
print_enuminfo info.var_enum;
|
||||
Printf.printf ";\n var_list = ";
|
||||
List.iter (fun v -> Printf.printf "%s, " (name v)) info.var_list;
|
||||
Printf.printf ";\n clocked_var =\n";
|
||||
print_var_tree 0 info.clocked_var
|
||||
*)
|
||||
|
||||
type type_info = Type of type_dec_desc | Enum of enuminfo
|
||||
|
||||
let enum_types : type_info QualEnv.t ref = ref QualEnv.empty
|
||||
|
||||
(*
|
||||
let print_enum_types () =
|
||||
QualEnv.fold
|
||||
(fun t ti () ->
|
||||
match ti with
|
||||
| Enum info ->
|
||||
Printf.printf "type %s :\n" (fullname t);
|
||||
print_enuminfo info
|
||||
| _ -> ()
|
||||
) !enum_types ()
|
||||
*)
|
||||
|
||||
let get_enum name =
|
||||
QualEnv.find name !enum_types
|
||||
|
||||
(* split2 k [x1;...;xn] = ([x1;...;xk],[xk+1;...;xn]) *)
|
||||
let split2 n l =
|
||||
let rec splitaux k acc l =
|
||||
if k = 0 then (acc,l) else
|
||||
begin
|
||||
match l with
|
||||
| x::t -> splitaux (k-1) (x::acc) t
|
||||
| _ -> assert false
|
||||
end in
|
||||
let (l1,l2) = splitaux n [] l in
|
||||
(List.rev l1,l2)
|
||||
|
||||
|
||||
|
||||
(* create an info from the elements of a name list *)
|
||||
let rec var_list clist =
|
||||
match clist with
|
||||
| [] -> (0,QualEnv.empty,Node(None))
|
||||
| [c] -> (1, QualEnv.add c [false] QualEnv.empty, Tree(Node(Some c),Node(None)))
|
||||
| [c1;c2] -> (1,
|
||||
QualEnv.add c1 [false] (QualEnv.add c2 [true] QualEnv.empty),
|
||||
Tree(Node(Some c1),Node(Some c2)))
|
||||
| l ->
|
||||
let n = List.length l in
|
||||
let n1 = n asr 1 in
|
||||
let l1,l2 = split2 n1 l in
|
||||
let (nv1,vl1,t1) = var_list l1
|
||||
and (nv2,vl2,t2) = var_list l2 in
|
||||
(* test and debug *)
|
||||
(* assert ((nv1 = nv2) or (nv1 = nv2 - 1)); *)
|
||||
(* QualEnv.iter (fun _ l -> assert ((List.length l) = nv1)) vl1; *)
|
||||
(* QualEnv.iter (fun _ l -> assert ((List.length l) = nv2)) vl2; *)
|
||||
(* let nt1 = *)
|
||||
(* begin *)
|
||||
(* match (count t1) with *)
|
||||
(* None -> assert false *)
|
||||
(* | Some n -> n *)
|
||||
(* end in *)
|
||||
(* assert (nt1 = nv1); *)
|
||||
(* let nt2 = *)
|
||||
(* begin *)
|
||||
(* match (count t2) with *)
|
||||
(* | None -> assert false *)
|
||||
(* | Some n -> n *)
|
||||
(* end in *)
|
||||
(* assert (nt2 = nv2); *)
|
||||
let vl =
|
||||
QualEnv.fold (fun c l m -> QualEnv.add c (true::l) m) vl2
|
||||
(QualEnv.fold
|
||||
(if nv1 = nv2
|
||||
then (fun c l m -> QualEnv.add c (false::l) m)
|
||||
else (fun c l m -> QualEnv.add c (false::false::l) m))
|
||||
vl1
|
||||
QualEnv.empty) in
|
||||
let t1 = if nv1 = nv2 then t1 else Tree(t1,Node(None)) in
|
||||
let t = Tree(t1,t2) in
|
||||
nv2 + 1, vl, t
|
||||
|
||||
let nvar_list prefix n =
|
||||
let rec varl acc = function
|
||||
| 0 -> acc
|
||||
| n ->
|
||||
let acc = (prefix ^ "_" ^ (string_of_int n)) :: acc in
|
||||
varl acc (n-1) in
|
||||
varl [] n
|
||||
|
||||
let translate_pat env pat =
|
||||
let rec trans = function
|
||||
| Evarpat(name) ->
|
||||
begin
|
||||
try
|
||||
let info = Env.find name env in
|
||||
match info.var_enum.ty_nb_var with
|
||||
| 1 ->
|
||||
Evarpat(List.nth info.var_list 0)
|
||||
| _ ->
|
||||
let varpat_list = info.var_list in
|
||||
Etuplepat(List.map (fun v -> Evarpat(v)) varpat_list)
|
||||
with Not_found -> Evarpat(name)
|
||||
end
|
||||
| Etuplepat(pat_list) -> Etuplepat(List.map trans pat_list) in
|
||||
trans pat
|
||||
|
||||
let translate_ty ty =
|
||||
let rec trans ty =
|
||||
match ty with
|
||||
| Tid({ qual = Pervasives; name = "bool" }) -> ty
|
||||
| Tid(name) ->
|
||||
begin
|
||||
try
|
||||
let info = get_enum name in
|
||||
begin match info with
|
||||
| Type(_) -> ty
|
||||
| Enum { ty_nb_var = 1 } -> ty_bool
|
||||
| Enum { ty_nb_var = n } ->
|
||||
let strlist = nvar_list "" n in
|
||||
Tprod(List.map (fun _ -> ty_bool) strlist)
|
||||
end
|
||||
with Not_found -> ty
|
||||
end
|
||||
| Tprod(ty_list) -> Tprod(List.map trans ty_list)
|
||||
| Tarray(ty,se) -> Tarray(trans ty,se)
|
||||
| Tinvalid -> assert false
|
||||
in
|
||||
trans ty
|
||||
|
||||
let rec on_list ck bl vtree =
|
||||
match bl, vtree with
|
||||
| [], _ -> ck
|
||||
| b::bl', VNode(v,t0,t1) ->
|
||||
let (c,t) = if b then (ctrue,t1) else (cfalse,t0) in
|
||||
on_list (Con(ck,c,v)) bl' t
|
||||
| _::_, Vempty -> failwith("on_list: non-coherent boolean list and tree")
|
||||
|
||||
let rec translate_ck env ck =
|
||||
match ck with
|
||||
| Cbase -> Cbase
|
||||
| Cvar {contents = Clink(ck)} -> translate_ck env ck
|
||||
| Cvar {contents = Cindex(_)} -> ck
|
||||
| Con(ck,c,n) ->
|
||||
let ck = translate_ck env ck in
|
||||
begin
|
||||
try
|
||||
let info = Env.find n env in
|
||||
let bl = QualEnv.find c info.var_enum.ty_assoc in
|
||||
on_list ck bl info.clocked_var
|
||||
with Not_found ->
|
||||
(* Boolean clock *)
|
||||
Con(ck,c,n)
|
||||
end
|
||||
|
||||
let rec translate_ct env ct =
|
||||
match ct with
|
||||
| Ck(ck) -> Ck(translate_ck env ck)
|
||||
| Cprod(l) -> Cprod(List.map (translate_ct env) l)
|
||||
|
||||
let translate_const c ty e =
|
||||
match c.se_desc,ty with
|
||||
| _, Tid({ qual = Pervasives; name = "bool" }) -> Econst(c)
|
||||
| Sconstructor(cname),Tid(tname) ->
|
||||
begin
|
||||
try
|
||||
begin
|
||||
match (get_enum tname) with
|
||||
| Type _ -> Econst(c)
|
||||
| Enum { ty_assoc = assoc } ->
|
||||
let bl = QualEnv.find cname assoc in
|
||||
let b_list = List.map (fun b -> Econst(sbool b)) bl in
|
||||
begin
|
||||
match b_list with
|
||||
| [] -> assert false
|
||||
| [b] -> b
|
||||
| _::_ ->
|
||||
mk_tuple
|
||||
(List.map
|
||||
(fun b -> {e with
|
||||
e_desc = b;
|
||||
e_ty = ty_bool })
|
||||
b_list)
|
||||
end
|
||||
end
|
||||
with Not_found -> Econst(c)
|
||||
end
|
||||
| _ -> Econst(c)
|
||||
|
||||
let new_var_list d_list ty ck n =
|
||||
let rec varl acc d_list = function
|
||||
| 0 -> acc,d_list
|
||||
| n ->
|
||||
let v = fresh "bool" in
|
||||
let acc = v :: acc in
|
||||
let d_list = (mk_var_dec ~clock:ck v ty) :: d_list in
|
||||
varl acc d_list (n-1) in
|
||||
varl [] d_list n
|
||||
|
||||
let assert_ck = function
|
||||
Some(Ck(ck)) -> ck
|
||||
| _ -> assert false
|
||||
|
||||
let intro_tuple context e =
|
||||
let n =
|
||||
match e.e_ty with
|
||||
| Tprod(l) -> List.length l
|
||||
| _ -> assert false in
|
||||
match e.e_desc with
|
||||
Eapp({a_op=Etuple},e_l,None) -> context,e_l
|
||||
| _ ->
|
||||
let (d_list,eq_list) = context in
|
||||
(* e is not a tuple, therefore e.e_ct_annot = Ck(ck) *)
|
||||
let ck = assert_ck e.e_ct_annot in
|
||||
let v_list,d_list = new_var_list d_list ty_bool ck n in
|
||||
let pat = Etuplepat(List.map (fun v -> Evarpat(v)) v_list) in
|
||||
let eq_list = (mk_equation (Eeq(pat,e))) :: eq_list in
|
||||
let e_list = List.map (fun v -> { e with e_ty = ty_bool; e_desc = Evar(v) }) v_list in
|
||||
(d_list,eq_list),e_list
|
||||
|
||||
let rec when_list e bl vtree =
|
||||
match bl, vtree with
|
||||
| [], _ -> e
|
||||
| b::bl', VNode(v,t0,t1) ->
|
||||
let (c,t) = if b then (ctrue,t1) else (cfalse,t0) in
|
||||
let ck = assert_ck e.e_ct_annot in
|
||||
(* let e_v = mk_exp (Evar v) ~ct_annot:(Some(Ck(ck))) ty_bool in *)
|
||||
let e_when = { e with
|
||||
e_ct_annot = Some (Ck(Con(ck,c,v)));
|
||||
e_desc = Ewhen(e,c,v) } in
|
||||
when_list e_when bl' t
|
||||
| _::_, Vempty -> failwith("when_list: non-coherent boolean list and tree")
|
||||
|
||||
let rec when_ck desc li ty ck =
|
||||
match ck with
|
||||
| Cbase | Cvar _ ->
|
||||
{ e_desc = desc;
|
||||
e_level_ck = ck;
|
||||
e_ct_annot = Some(Ck(ck));
|
||||
e_linearity = li;
|
||||
e_ty = ty;
|
||||
e_loc = no_location }
|
||||
| Con(ck',c,v) ->
|
||||
let e = when_ck desc li ty ck' in
|
||||
(* let e_v = mk_exp (Evar v) ~ct_annot:(Some(Ck(ck'))) ty_bool in *)
|
||||
{ e_desc = Ewhen(e,c,v);
|
||||
e_level_ck = ck;
|
||||
e_ct_annot = Some(Ck(ck));
|
||||
e_linearity = li;
|
||||
e_ty = ty;
|
||||
e_loc = no_location }
|
||||
|
||||
let rec base_value ck li ty =
|
||||
match ty with
|
||||
| Tid({qual = Pervasives; name = "int" }) ->
|
||||
when_ck (Econst(mk_static_exp ty (Sint(0)))) li ty ck
|
||||
| Tid({qual = Pervasives; name = "float"}) ->
|
||||
when_ck (Econst(mk_static_exp ty (Sfloat(0.)))) li ty ck
|
||||
| Tid({qual = Pervasives; name = "bool" }) ->
|
||||
when_ck (Econst(strue)) li ty ck
|
||||
| Tid(sname) ->
|
||||
begin
|
||||
try
|
||||
begin
|
||||
let info = get_enum sname in
|
||||
(* boolean tuple *)
|
||||
match info with
|
||||
| Type(Type_abs) -> failwith("Abstract types not implemented")
|
||||
| Type(Type_alias aty) -> base_value ck li aty
|
||||
| Type(Type_enum(l)) ->
|
||||
when_ck
|
||||
(Econst(mk_static_exp ty (Sconstructor(List.hd l))))
|
||||
li ty ck
|
||||
| Type(Type_struct(l)) ->
|
||||
let fields =
|
||||
List.map
|
||||
(fun {f_name = name; f_type = ty} ->
|
||||
name,(base_value ck li ty))
|
||||
l in
|
||||
when_ck (Estruct(fields)) li ty ck
|
||||
| Enum { ty_nb_var = 1 } ->
|
||||
when_ck (Econst(strue)) li ty_bool ck
|
||||
| Enum { ty_nb_var = n } ->
|
||||
let e = when_ck (Econst(strue)) li ty_bool ck in
|
||||
let rec aux acc = function
|
||||
| 0 -> acc
|
||||
| n -> aux (e::acc) (n-1) in
|
||||
let e_list = aux [] n in
|
||||
{ e_desc = mk_tuple e_list;
|
||||
e_ty = Tprod(List.map (fun _ -> ty_bool) e_list);
|
||||
e_level_ck = Cbase;
|
||||
e_ct_annot = Some(Ck(ck));
|
||||
e_linearity = li;
|
||||
e_loc = no_location }
|
||||
end
|
||||
with Not_found ->
|
||||
Printf.printf "Name : %s\n" sname.name; assert false
|
||||
end
|
||||
| Tprod(ty_list) ->
|
||||
let e_list = List.map (base_value ck li) ty_list in
|
||||
{ e_desc = mk_tuple e_list;
|
||||
e_ty = Tprod(List.map (fun e -> e.e_ty) e_list);
|
||||
e_level_ck = Cbase;
|
||||
e_ct_annot = Some(Ck(ck));
|
||||
e_linearity = li;
|
||||
e_loc = no_location;
|
||||
}
|
||||
| Tarray(ty,se) ->
|
||||
let e = base_value ck li ty in
|
||||
{ e_desc = Eapp((mk_app ~params:[se] Earray_fill), [e], None);
|
||||
e_ty = Tarray(e.e_ty,se);
|
||||
e_level_ck = Cbase;
|
||||
e_ct_annot = Some(Ck(ck));
|
||||
e_linearity = li;
|
||||
e_loc = no_location;
|
||||
}
|
||||
| Tinvalid -> failwith("Boolean: invalid type")
|
||||
|
||||
let rec merge_tree ck ty li e_map btree vtree =
|
||||
match btree, vtree with
|
||||
| Node(None), _ -> base_value ck li ty
|
||||
| Node(Some name), _ ->
|
||||
let e = QualEnv.find name e_map in
|
||||
{ e with e_ct_annot = Some(Ck(ck)) }
|
||||
| Tree(t1,t2), VNode(v,vt1,vt2) ->
|
||||
let e1 = merge_tree (Con(ck,cfalse,v)) ty li e_map t1 vt1
|
||||
and e2 = merge_tree (Con(ck,ctrue,v)) ty li e_map t2 vt2
|
||||
in
|
||||
(* let e_v = mk_exp (Evar v) ~ct_annot:(Some(Ck(ck))) ty_bool in *)
|
||||
{ e_desc = Emerge(v,[(cfalse,e1);(ctrue,e2)]);
|
||||
e_ty = ty;
|
||||
e_level_ck = Cbase;
|
||||
e_ct_annot = Some(Ck(ck));
|
||||
e_linearity = li;
|
||||
e_loc = no_location }
|
||||
| Tree (_,_), Vempty -> failwith("merge_tree: non-coherent trees")
|
||||
|
||||
|
||||
let rec translate env context ({e_desc = desc; e_ty = ty; e_ct_annot = ct} as e) =
|
||||
let ct = Misc.optional (translate_ct env) ct in
|
||||
let context,desc =
|
||||
match desc with
|
||||
| Econst(c) ->
|
||||
context, translate_const c ty e
|
||||
| Evar(name) ->
|
||||
let desc = begin
|
||||
try
|
||||
let info = Env.find name env in
|
||||
if info.var_enum.ty_nb_var = 1 then
|
||||
Evar(List.nth info.var_list 0)
|
||||
else
|
||||
let ident_list = info.var_list in
|
||||
mk_tuple (List.map
|
||||
(fun v -> { e with
|
||||
e_ty = ty_bool;
|
||||
e_ct_annot = ct;
|
||||
e_desc = Evar(v); })
|
||||
ident_list)
|
||||
with Not_found -> Evar(name)
|
||||
end in
|
||||
context,desc
|
||||
| Efby(e1,e2) ->
|
||||
let context,e1 = translate env context e1 in
|
||||
let context,e2 = translate env context e2 in
|
||||
context,Efby(e1,e2)
|
||||
| Epre(None, e) ->
|
||||
let context,e = translate env context e in
|
||||
context,Epre(None,e)
|
||||
| Epre(Some c,e) ->
|
||||
let e_c = translate_const c ty e in
|
||||
let context,e = translate env context e in
|
||||
begin
|
||||
match e_c with
|
||||
| Econst(c) -> context,Epre(Some c,e)
|
||||
| Eapp({ a_op = Etuple },e_c_l,None) ->
|
||||
let context,e_l = intro_tuple context e in
|
||||
let c_l = List.map (function
|
||||
| { e_desc = Econst(c) } -> c
|
||||
| _ -> assert false) e_c_l in
|
||||
context,
|
||||
mk_tuple
|
||||
(List.map2
|
||||
(fun c e -> { e with
|
||||
e_ty = ty_bool;
|
||||
e_desc = Epre(Some c,e)})
|
||||
c_l e_l)
|
||||
| _ -> assert false
|
||||
end
|
||||
| Eapp(app, e_list, r) ->
|
||||
let context,e_list = translate_list env context e_list in
|
||||
context, Eapp(app, e_list, r)
|
||||
| Ewhen(e,c,ck) ->
|
||||
let context,e = translate env context e in
|
||||
begin
|
||||
try
|
||||
let info = Env.find ck env in
|
||||
let bl = QualEnv.find c info.var_enum.ty_assoc in
|
||||
let e_when = when_list e bl info.clocked_var in
|
||||
context,e_when.e_desc
|
||||
with Not_found ->
|
||||
(* Boolean clock *)
|
||||
context,Ewhen(e,c,ck)
|
||||
end
|
||||
| Emerge(ck,l) (* of name * (longname * exp) list *)
|
||||
->
|
||||
begin
|
||||
try
|
||||
let info = Env.find ck env in
|
||||
let context,e_map = List.fold_left
|
||||
(fun (context,e_map) (n,e) ->
|
||||
let context,e = translate env context e in
|
||||
context,QualEnv.add n e e_map)
|
||||
(context,QualEnv.empty) l in
|
||||
let e_merge =
|
||||
merge_tree (assert_ck ct) ty e.e_linearity e_map
|
||||
info.var_enum.ty_tree
|
||||
info.clocked_var in
|
||||
context,e_merge.e_desc
|
||||
with Not_found ->
|
||||
(* Boolean clock *)
|
||||
let context, l =
|
||||
List.fold_left
|
||||
(fun (context,acc_l) (n,e) ->
|
||||
let context,e = translate env context e in
|
||||
context, (n,e)::acc_l)
|
||||
(context,[]) l in
|
||||
context,Emerge(ck,l)
|
||||
end
|
||||
| Esplit(e1,e2) ->
|
||||
let context,e1 = translate env context e1 in
|
||||
let context,e2 = translate env context e2 in
|
||||
context,Esplit(e1,e2)
|
||||
| Estruct(l) ->
|
||||
let context,acc =
|
||||
List.fold_left
|
||||
(fun (context,acc) (c,e) ->
|
||||
let context,e = translate env context e in
|
||||
(context,(c,e)::acc))
|
||||
(context,[]) l in
|
||||
context,Estruct(List.rev acc)
|
||||
| Eiterator(it,app,se,pe_list,e_list,r) ->
|
||||
let context,pe_list = translate_list env context pe_list in
|
||||
let context,e_list = translate_list env context e_list in
|
||||
context,Eiterator(it,app,se,pe_list,e_list,r)
|
||||
| Elast _ ->
|
||||
failwith("Boolean: not supported expression (abstract tree should be normalized)")
|
||||
in
|
||||
context,{ e with
|
||||
e_desc = desc;
|
||||
e_ty = translate_ty ty;
|
||||
e_ct_annot = ct}
|
||||
|
||||
and translate_list env context e_list =
|
||||
let context,acc_e =
|
||||
List.fold_left
|
||||
(fun (context,acc_e) e ->
|
||||
let context,e = translate env context e in
|
||||
(context,e::acc_e))
|
||||
(context,[]) e_list in
|
||||
context,List.rev acc_e
|
||||
|
||||
(* Tranlate variable declaration list : outputs
|
||||
- new declaration list
|
||||
- added local variables suffixed with "(_(1|0))*" for clock coherence
|
||||
- equations of these added variables
|
||||
*)
|
||||
let var_dec_list (acc_vd,acc_loc,acc_eq) var_from n =
|
||||
|
||||
(* when_ck [v3_1_0;v2_1;v1] (ck on True(v1) on False(v2_1) on True(v3_1_0)) v4
|
||||
= ((v4 when True(v1)) when False(v2_1)) when True(v3_1_0)
|
||||
-> builds v4_1_0_1
|
||||
*)
|
||||
let rec when_ck ckvar_list ck var =
|
||||
match ckvar_list,ck with
|
||||
| [], _ ->
|
||||
{ e_desc = Evar(var);
|
||||
e_level_ck = ck;
|
||||
e_ct_annot = Some(Ck(ck));
|
||||
e_ty = ty_bool;
|
||||
e_linearity = var_from.v_linearity;
|
||||
e_loc = no_location }
|
||||
| _ckvar::l, Con(ck',c,v) ->
|
||||
(* assert v = _ckvar *)
|
||||
let e = when_ck l ck' var in
|
||||
(* let e_v = mk_exp (Evar v) ~ct_annot:(Some(Ck(ck'))) ty_bool in *)
|
||||
{ e_desc = Ewhen(e,c,v);
|
||||
e_level_ck = ck;
|
||||
e_ct_annot = Some(Ck(ck));
|
||||
e_ty = ty_bool;
|
||||
e_linearity = var_from.v_linearity;
|
||||
e_loc = no_location }
|
||||
| _ -> failwith("when_ck: non coherent clock and var list")
|
||||
in
|
||||
|
||||
let prefix = name var_from.v_ident in
|
||||
|
||||
(* From v, build of v1...vn *)
|
||||
let rec varl acc_vd k =
|
||||
if k>n
|
||||
then acc_vd
|
||||
else
|
||||
begin
|
||||
let var_prefix = prefix ^ "_" ^ (string_of_int k) in
|
||||
let var = fresh var_prefix in
|
||||
(* addition of var_k *)
|
||||
let acc_vd = { var_from with
|
||||
v_ident = var;
|
||||
v_type = ty_bool } :: acc_vd in
|
||||
varl acc_vd (k+1)
|
||||
end in
|
||||
|
||||
let vd_list = varl [] 1 in
|
||||
(* v_list = [vn;...;v1] *)
|
||||
let acc_vd = List.rev_append vd_list acc_vd in
|
||||
|
||||
let v_list = List.rev_map (fun vd -> vd.v_ident) vd_list in
|
||||
|
||||
(* From v1...vn, build clocked tree
|
||||
( vi_(0|1)* on ... on (True|False) (v1) ) *)
|
||||
let rec clocked_tree (acc_loc,acc_eq) acc_var suffix v_list ck =
|
||||
begin match v_list, acc_var with
|
||||
[], _ ->
|
||||
(* Leafs *)
|
||||
acc_loc,acc_eq,Vempty
|
||||
| v1::v_list, [] ->
|
||||
(* Root : no new id, only rec calls for sons *)
|
||||
(* Build left son (ck on False(vi_...)) *)
|
||||
let ck_0 = Con(ck,cfalse,v1) in
|
||||
let acc_loc,acc_eq,t0 =
|
||||
clocked_tree
|
||||
(acc_loc,acc_eq)
|
||||
([v1])
|
||||
("_0")
|
||||
v_list ck_0 in
|
||||
(* Build right son (ck on True(vi_...))*)
|
||||
let ck_1 = Con(ck,ctrue,v1) in
|
||||
let acc_loc,acc_eq,t1 =
|
||||
clocked_tree
|
||||
(acc_loc,acc_eq)
|
||||
([v1])
|
||||
("_1")
|
||||
v_list ck_1 in
|
||||
acc_loc,acc_eq,VNode(v1,t0,t1)
|
||||
| vi::v_list, _ ->
|
||||
(* Build name vi_(0|1)* *)
|
||||
let v = (name vi) ^ suffix in
|
||||
(* Build ident from this name *)
|
||||
let id = fresh v in
|
||||
let acc_loc = { v_ident = id;
|
||||
v_type = ty_bool;
|
||||
v_linearity = var_from.v_linearity;
|
||||
v_clock = ck;
|
||||
v_last = Var;
|
||||
v_loc = no_location } :: acc_loc in
|
||||
(* vi_... = vi when ... when (True|False)(v1) *)
|
||||
let acc_eq =
|
||||
(mk_equation (Eeq(Evarpat(id),(when_ck acc_var ck vi))))
|
||||
::acc_eq in
|
||||
(* Build left son (ck on False(vi_...)) *)
|
||||
let ck_0 = Con(ck,cfalse,id) in
|
||||
let acc_loc,acc_eq,t0 =
|
||||
clocked_tree
|
||||
(acc_loc,acc_eq)
|
||||
(id::acc_var)
|
||||
(suffix ^ "_0")
|
||||
v_list ck_0 in
|
||||
(* Build right son (ck on True(vi_...))*)
|
||||
let ck_1 = Con(ck,ctrue,id) in
|
||||
let acc_loc,acc_eq,t1 =
|
||||
clocked_tree
|
||||
(acc_loc,acc_eq)
|
||||
(id::acc_var)
|
||||
(suffix ^ "_1")
|
||||
v_list ck_1 in
|
||||
acc_loc,acc_eq,VNode(id,t0,t1)
|
||||
end
|
||||
in
|
||||
|
||||
let acc_loc,acc_eq,t =
|
||||
clocked_tree (acc_loc,acc_eq) [] "" v_list var_from.v_clock in
|
||||
|
||||
(acc_vd,acc_loc,acc_eq,v_list,t)
|
||||
|
||||
let buildenv_var_dec (acc_vd,acc_loc,acc_eq,env) ({v_type = ty} as v) =
|
||||
match ty with
|
||||
| Tprod _ | Tarray _ ->
|
||||
v::acc_vd, acc_loc, acc_eq, env
|
||||
| Tid(tname) ->
|
||||
begin
|
||||
match tname with
|
||||
| { qual = Pervasives; name = ("bool" | "int" | "float") } ->
|
||||
v::acc_vd, acc_loc, acc_eq, env
|
||||
| _ ->
|
||||
begin
|
||||
try
|
||||
begin
|
||||
match (get_enum tname) with
|
||||
| Type _ -> v::acc_vd, acc_loc, acc_eq ,env
|
||||
| Enum(info) ->
|
||||
let (acc_vd,acc_loc,acc_eq,vl,t) =
|
||||
var_dec_list
|
||||
(acc_vd,acc_loc,acc_eq)
|
||||
v info.ty_nb_var in
|
||||
let vi = { var_enum = info;
|
||||
var_list = vl;
|
||||
clocked_var = t } in
|
||||
let env =
|
||||
Env.add
|
||||
v.v_ident
|
||||
{ var_enum = info;
|
||||
var_list = vl;
|
||||
clocked_var = t }
|
||||
env in
|
||||
acc_vd, acc_loc, acc_eq, env
|
||||
end
|
||||
with Not_found -> v::acc_vd, acc_loc, acc_eq, env
|
||||
end
|
||||
end
|
||||
| Tinvalid -> failwith("Boolean: invalid type")
|
||||
|
||||
let buildenv_var_dec_list env vlist =
|
||||
List.fold_left buildenv_var_dec ([],[],[],env) vlist
|
||||
|
||||
let translate_var_dec env ({ v_clock = ck } as v) =
|
||||
{ v with v_clock = translate_ck env ck }
|
||||
|
||||
let translate_var_dec_list env vlist =
|
||||
List.map (translate_var_dec env) vlist
|
||||
|
||||
let rec translate_block env add_locals add_eqs ({ b_local = v;
|
||||
b_equs = eq_list; } as b) =
|
||||
let v, v',v_eq,env = buildenv_var_dec_list env v in
|
||||
let v = v@v'@add_locals in
|
||||
let v = translate_var_dec_list env v in
|
||||
let eq_list = eq_list@v_eq@add_eqs in
|
||||
let context = translate_eqs env eq_list in
|
||||
let d_list,eq_list = context in
|
||||
{ b with
|
||||
b_local = v@d_list;
|
||||
b_equs = eq_list }, env
|
||||
|
||||
and translate_eq env context ({eq_desc = desc} as eq) =
|
||||
let desc,(d_list,eq_list) =
|
||||
match desc with
|
||||
| Eblock block ->
|
||||
let block, _ = translate_block env [] [] block in
|
||||
Eblock block,
|
||||
context
|
||||
| Eeq(pat,e) ->
|
||||
let pat = translate_pat env pat in
|
||||
let context,e = translate env context e in
|
||||
Eeq(pat,e),
|
||||
context
|
||||
| _ -> failwith("Boolean pass: control structures should be removed")
|
||||
in
|
||||
d_list,{ eq with eq_desc = desc }::eq_list
|
||||
|
||||
and translate_eqs env eq_list =
|
||||
List.fold_left
|
||||
(fun context eq ->
|
||||
translate_eq env context eq) ([],[]) eq_list
|
||||
|
||||
let translate_contract env contract =
|
||||
match contract with
|
||||
| None -> None, env
|
||||
| Some { c_assume = e_a;
|
||||
c_enforce = e_g;
|
||||
c_controllables = cl;
|
||||
c_block = b } ->
|
||||
let cl, cl_loc, cl_eq, env = buildenv_var_dec_list env cl in
|
||||
let cl = translate_var_dec_list env cl in
|
||||
let ({ b_local = v;
|
||||
b_equs = eqs } as b), env'
|
||||
= translate_block env cl_loc cl_eq b in
|
||||
let context, e_a = translate env' (v,eqs) e_a in
|
||||
let context, e_g = translate env' context e_g in
|
||||
let (d_list,eq_list) = context in
|
||||
Some { c_block = { b with
|
||||
b_local = d_list;
|
||||
b_equs = eq_list };
|
||||
c_assume = e_a;
|
||||
c_enforce = e_g;
|
||||
c_controllables = cl },
|
||||
env
|
||||
|
||||
let node ({ n_input = inputs;
|
||||
n_output = outputs;
|
||||
n_contract = contract;
|
||||
n_block = b } as n) =
|
||||
let inputs,in_loc,in_eq,env = buildenv_var_dec_list Env.empty inputs in
|
||||
let outputs,out_loc,out_eq,env = buildenv_var_dec_list env outputs in
|
||||
let contract, env = translate_contract env contract in
|
||||
let add_locals = in_loc@out_loc in
|
||||
let add_eqs = in_eq@out_eq in
|
||||
let b,_ = translate_block env add_locals add_eqs b in
|
||||
{ n with
|
||||
n_input = List.rev inputs;
|
||||
n_output = List.rev outputs;
|
||||
n_contract = contract;
|
||||
n_block = b }
|
||||
|
||||
let program_desc p_desc =
|
||||
match p_desc with
|
||||
| Pnode(n) -> Pnode(node n)
|
||||
| _ -> p_desc
|
||||
|
||||
let build p_desc =
|
||||
match p_desc with
|
||||
| Ptype(type_dec) ->
|
||||
begin
|
||||
let tenv =
|
||||
match type_dec.t_desc with
|
||||
| Type_enum clist ->
|
||||
let (n,env,t) = var_list clist in
|
||||
Enum({ ty_nb_var = n;
|
||||
ty_assoc = env;
|
||||
ty_tree = t})
|
||||
| tdesc -> Type(tdesc) in
|
||||
enum_types := QualEnv.add type_dec.t_name tenv !enum_types
|
||||
end
|
||||
| _ -> ()
|
||||
|
||||
let program ({ p_desc = d_list } as p) =
|
||||
List.iter build d_list;
|
||||
{ p with p_desc = List.map program_desc d_list }
|
||||
@ -0,0 +1,34 @@
|
||||
(****************************************************)
|
||||
(* *)
|
||||
(* Heptagon/BZR *)
|
||||
(* *)
|
||||
(* Author : Gwenaël Delaval *)
|
||||
(* Organization : INRIA Rennes, VerTeCs *)
|
||||
(* *)
|
||||
(****************************************************)
|
||||
|
||||
(*
|
||||
Translate enumerated types (state variables) into boolean
|
||||
|
||||
type t = A | B | C | D
|
||||
|
||||
A --> 00
|
||||
B --> 01
|
||||
C --> 10
|
||||
D --> 11
|
||||
|
||||
x : t --> x1,x2 : bool
|
||||
|
||||
(e when A(x))
|
||||
-->
|
||||
(e when False(x1)) when False(x2)
|
||||
|
||||
merge x (A -> e0) (B -> e1) (C -> e2) (D -> e3)
|
||||
-->
|
||||
merge x1 (False -> merge x2 (False -> e0) (True -> e1))
|
||||
(True -> merge x2 (False -> e2) (True -> e3))
|
||||
*)
|
||||
|
||||
(* $Id: boolean.mli 74 2009-03-11 10:21:25Z delaval $ *)
|
||||
|
||||
val program : Heptagon.program -> Heptagon.program
|
||||
@ -1 +1,2 @@
|
||||
<analysis> or <transformations> or <main> or <parsing>:include
|
||||
<sigali>:include
|
||||
@ -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
|
||||
|
||||
@ -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
|
||||
@ -0,0 +1,705 @@
|
||||
(****************************************************)
|
||||
(* *)
|
||||
(* 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")
|
||||
|
||||
(* [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
|
||||
|
||||
@ -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
|
||||
Loading…
Reference in New Issue