diff --git a/compiler/global/global_printer.ml b/compiler/global/global_printer.ml index 456b68b..cb9f492 100644 --- a/compiler/global/global_printer.ml +++ b/compiler/global/global_printer.ml @@ -154,12 +154,14 @@ let print_interface_value ff (name,node) = let print_interface ff = let m = Modules.current_module () in + Format.fprintf ff "@["; NamesEnv.iter (fun key typdesc -> print_interface_type ff (key,typdesc)) m.m_types; NamesEnv.iter (fun key constdec -> print_interface_const ff (key,constdec)) m.m_consts; NamesEnv.iter (fun key sigtype -> print_interface_value ff (key,sigtype)) m.m_values; + Format.fprintf ff "@]"; Format.fprintf ff "@." diff --git a/compiler/heptagon/analysis/hept_clocking.ml b/compiler/heptagon/analysis/hept_clocking.ml new file mode 100644 index 0000000..12351bb --- /dev/null +++ b/compiler/heptagon/analysis/hept_clocking.ml @@ -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; } + diff --git a/compiler/heptagon/analysis/typing.ml b/compiler/heptagon/analysis/typing.ml index 1d03255..2e2247c 100644 --- a/compiler/heptagon/analysis/typing.ml +++ b/compiler/heptagon/analysis/typing.ml @@ -1112,14 +1112,14 @@ let typing_contract cenv h contract = c_assume = e_a; c_enforce = e_g; c_controllables = c }) -> - let typed_b, defined_names, _ = typing_block cenv h b in + let typed_b, defined_names, h' = typing_block cenv h b in (* check that the equations do not define other unexpected names *) included_env defined_names Env.empty; (* assumption *) - let typed_e_a = expect cenv h (Tid Initial.pbool) e_a in + let typed_e_a = expect cenv h' (Tid Initial.pbool) e_a in (* property *) - let typed_e_g = expect cenv h (Tid Initial.pbool) e_g in + let typed_e_g = expect cenv h' (Tid Initial.pbool) e_g in let typed_c, (c_names, h) = build cenv h c in diff --git a/compiler/heptagon/hept_printer.ml b/compiler/heptagon/hept_printer.ml index d0751e9..fbf89e7 100644 --- a/compiler/heptagon/hept_printer.ml +++ b/compiler/heptagon/hept_printer.ml @@ -283,7 +283,7 @@ let rec print_type_def ff { t_name = name; t_desc = tdesc } = let print_contract ff { c_block = b; c_assume = e_a; c_enforce = e_g; c_controllables = c} = - fprintf ff "@[contract@\n%a@ assume %a@ enforce %a@ with (%a)@]" + fprintf ff "@[contract@\n%a@ assume %a@ enforce %a@ with (%a)@\n@]" print_block b print_exp e_a print_exp e_g @@ -311,6 +311,8 @@ let print_open_module ff name = fprintf ff "open %s@." (modul_to_string name) let print oc { p_opened = po; p_desc = pd; } = let ff = Format.formatter_of_out_channel oc in + fprintf ff "@["; List.iter (print_open_module ff) po; List.iter (print_pdesc ff) pd; + fprintf ff "@]"; fprintf ff "@?" diff --git a/compiler/heptagon/hept_utils.ml b/compiler/heptagon/hept_utils.ml index 7ac21fe..ca24226 100644 --- a/compiler/heptagon/hept_utils.ml +++ b/compiler/heptagon/hept_utils.ml @@ -25,8 +25,8 @@ let mk_exp desc ?(linearity = Ltop) ?(level_ck = Cbase) ?(ct_annot = None) ?(loc { e_desc = desc; e_ty = ty; e_ct_annot = ct_annot; e_linearity = linearity; e_level_ck = level_ck; e_loc = loc; } -let mk_app ?(params=[]) ?(unsafe=false) op = - { a_op = op; a_params = params; a_unsafe = unsafe } +let mk_app ?(params=[]) ?(unsafe=false) ?(inlined=false) op = + { a_op = op; a_params = params; a_unsafe = unsafe; a_inlined = inlined } let mk_op_app ?(params=[]) ?(unsafe=false) ?(reset=None) op args = Eapp(mk_app ~params:params ~unsafe:unsafe op, args, reset) diff --git a/compiler/heptagon/heptagon.ml b/compiler/heptagon/heptagon.ml index bb10352..f48b9a7 100644 --- a/compiler/heptagon/heptagon.ml +++ b/compiler/heptagon/heptagon.ml @@ -30,7 +30,7 @@ type iterator_type = type exp = { e_desc : desc; e_ty : ty; - e_ct_annot : ct option; (* exists when a source annotation exists *) + mutable e_ct_annot : ct option; (* exists when a source annotation exists *) e_level_ck : ck; (* set by the switch pass, represents the activation base of the expression *) mutable e_linearity : linearity; e_loc : location } @@ -55,7 +55,8 @@ and desc = and app = { a_op : op; a_params : static_exp list; - a_unsafe : bool } + a_unsafe : bool; + a_inlined : bool } and op = | Etuple diff --git a/compiler/heptagon/main/hept_compiler.ml b/compiler/heptagon/main/hept_compiler.ml index 42092da..4825bd3 100644 --- a/compiler/heptagon/main/hept_compiler.ml +++ b/compiler/heptagon/main/hept_compiler.ml @@ -58,6 +58,12 @@ let compile_program p = (* Normalization *) let p = pass "Normalization" true Normalize.program p pp in + (* Boolean pass *) + let p = pass "Clocking(Heptagon)" !boolean Hept_clocking.program p pp in + let p = pass "Boolean" !boolean Boolean.program p pp in + let p = pass "Normalization" !boolean Normalize.program p pp in + + (* Block flatten *) let p = pass "Block" true Block.program p pp in diff --git a/compiler/heptagon/parsing/hept_lexer.mll b/compiler/heptagon/parsing/hept_lexer.mll index 81c3e9d..0db23a9 100644 --- a/compiler/heptagon/parsing/hept_lexer.mll +++ b/compiler/heptagon/parsing/hept_lexer.mll @@ -53,6 +53,7 @@ List.iter (fun (str,tok) -> Hashtbl.add keyword_table str tok) [ "assume", ASSUME; "enforce", ENFORCE; "with", WITH; + "inlined",INLINED; "when", WHEN; "whenot", WHENOT; "merge", MERGE; diff --git a/compiler/heptagon/parsing/hept_parser.mly b/compiler/heptagon/parsing/hept_parser.mly index a36195b..f3c2df3 100644 --- a/compiler/heptagon/parsing/hept_parser.mly +++ b/compiler/heptagon/parsing/hept_parser.mly @@ -41,6 +41,7 @@ open Hept_parsetree %token ENFORCE %token WITH %token WHEN WHENOT MERGE ON ONOT +%token INLINED %token POWER %token LBRACKET LBRACKETGREATER %token RBRACKET LESSRBRACKET @@ -456,6 +457,9 @@ _simple_exp: /* TODO : conflict with Eselect_dyn and or const*/ ; +node_name: + | q=qualname c=call_params { mk_app (Enode q) c false } + | INLINED q=qualname c=call_params { mk_app (Enode q) c true } merge_handlers: | hs=nonempty_list(merge_handler) { hs } @@ -471,8 +475,8 @@ _exp: | PRE exp { Epre (None, $2) } /* node call*/ - | n=qualname p=call_params LPAREN args=exps RPAREN - { Eapp(mk_app (Enode n) p , args) } + | n=node_name LPAREN args=exps RPAREN + { Eapp(n, args) } | SPLIT n=ident LPAREN e=exp RPAREN { Esplit(n, e) } | NOT exp diff --git a/compiler/heptagon/parsing/hept_parsetree.ml b/compiler/heptagon/parsing/hept_parsetree.ml index a86b1f9..ddeae11 100644 --- a/compiler/heptagon/parsing/hept_parsetree.ml +++ b/compiler/heptagon/parsing/hept_parsetree.ml @@ -87,7 +87,7 @@ and edesc = | Emerge of var_name * (constructor_name * exp) list | Esplit of var_name * exp -and app = { a_op: op; a_params: exp list; } +and app = { a_op: op; a_params: exp list; a_inlined: bool } and op = | Etuple @@ -234,17 +234,17 @@ and interface_desc = let mk_exp desc ?(ct_annot = None) loc = { e_desc = desc; e_ct_annot = ct_annot; e_loc = loc } -let mk_app op params = - { a_op = op; a_params = params; } +let mk_app op params inlined = + { a_op = op; a_params = params; a_inlined = inlined } -let mk_call ?(params=[]) op exps = - Eapp (mk_app op params, exps) +let mk_call ?(params=[]) ?(inlined=false) op exps = + Eapp (mk_app op params inlined, exps) let mk_op_call ?(params=[]) s exps = mk_call ~params:params (Efun (Q (Names.pervasives_qn s))) exps let mk_iterator_call it ln params n_list pexps exps = - Eiterator (it, mk_app (Enode ln) params, n_list, pexps, exps) + Eiterator (it, mk_app (Enode ln) params false, n_list, pexps, exps) let mk_static_exp desc loc = { se_desc = desc; se_loc = loc } diff --git a/compiler/heptagon/parsing/hept_scoping.ml b/compiler/heptagon/parsing/hept_scoping.ml index b357acb..65d057e 100644 --- a/compiler/heptagon/parsing/hept_scoping.ml +++ b/compiler/heptagon/parsing/hept_scoping.ml @@ -165,8 +165,11 @@ struct end -let mk_app ?(params=[]) ?(unsafe=false) op = - { Heptagon.a_op = op; Heptagon.a_params = params; Heptagon.a_unsafe = unsafe } +let mk_app ?(params=[]) ?(unsafe=false) ?(inlined = false) op = + { Heptagon.a_op = op; + Heptagon.a_params = params; + Heptagon.a_unsafe = unsafe; + Heptagon.a_inlined = inlined } let mk_signature name ins outs stateful params constraints loc = { Heptagon.sig_name = name; @@ -287,10 +290,10 @@ and translate_desc loc env = function List.map (fun (f,e) -> qualify_field f, translate_exp env e) f_e_list in Heptagon.Estruct f_e_list - | Eapp ({ a_op = op; a_params = params; }, e_list) -> + | Eapp ({ a_op = op; a_params = params; a_inlined = inl }, e_list) -> let e_list = List.map (translate_exp env) e_list in let params = List.map (expect_static_exp) params in - let app = mk_app ~params:params (translate_op op) in + let app = mk_app ~params:params ~inlined:inl (translate_op op) in Heptagon.Eapp (app, e_list, None) | Eiterator (it, { a_op = op; a_params = params }, n_list, pe_list, e_list) -> @@ -420,12 +423,17 @@ and translate_last = function | Last (None) -> Heptagon.Last None | Last (Some e) -> Heptagon.Last (Some (expect_static_exp e)) -let translate_contract env ct = - let b, _ = translate_block env ct.c_block in - { Heptagon.c_assume = translate_exp env ct.c_assume; - Heptagon.c_enforce = translate_exp env ct.c_enforce; - Heptagon.c_controllables = translate_vd_list env ct.c_controllables; - Heptagon.c_block = b } +let translate_contract env opt_ct = + match opt_ct with + | None -> None, env + | Some ct -> + let env' = Rename.append env ct.c_controllables in + let b, env = translate_block env ct.c_block in + Some + { Heptagon.c_assume = translate_exp env ct.c_assume; + Heptagon.c_enforce = translate_exp env ct.c_enforce; + Heptagon.c_controllables = translate_vd_list env' ct.c_controllables; + Heptagon.c_block = b }, env' let params_of_var_decs env p_l = let pofvd env vd = @@ -461,9 +469,9 @@ let translate_node node = (* Inputs and outputs define the initial local env *) let env0 = Rename.append env node.n_output in let outputs = translate_vd_list env0 node.n_output in - let b, env = translate_block env0 node.n_block in - (* the env of the block is used in the contract translation *) - let contract = Misc.optional (translate_contract env) node.n_contract in + (* Enrich env with controllable variables (used in block) *) + let contract, env = translate_contract env0 node.n_contract in + let b, _ = translate_block env node.n_block in (* add the node signature to the environment *) let nnode = { Heptagon.n_name = n; Heptagon.n_stateful = node.n_stateful; diff --git a/compiler/heptagon/transformations/automata.ml b/compiler/heptagon/transformations/automata.ml index 013bc4e..6ac1c77 100644 --- a/compiler/heptagon/transformations/automata.ml +++ b/compiler/heptagon/transformations/automata.ml @@ -76,7 +76,7 @@ let no_strong_transition state_handlers = let translate_automaton v eq_list handlers = - let type_name = Modules.fresh_type "automata" "state" in + let type_name = Modules.fresh_type "automata" "st" in (* the state env associate a name to a qualified constructor *) let state_env = List.fold_left diff --git a/compiler/heptagon/transformations/boolean.ml b/compiler/heptagon/transformations/boolean.ml new file mode 100644 index 0000000..3a74e4a --- /dev/null +++ b/compiler/heptagon/transformations/boolean.ml @@ -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 } diff --git a/compiler/heptagon/transformations/boolean.mli b/compiler/heptagon/transformations/boolean.mli new file mode 100644 index 0000000..c98bbd5 --- /dev/null +++ b/compiler/heptagon/transformations/boolean.mli @@ -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 diff --git a/compiler/heptagon/transformations/normalize.ml b/compiler/heptagon/transformations/normalize.ml index dfc8d87..0b5ed51 100644 --- a/compiler/heptagon/transformations/normalize.ml +++ b/compiler/heptagon/transformations/normalize.ml @@ -82,13 +82,13 @@ let equation (d_list, eq_list) e = (d_list, eq_list), Evar n (* [(e1,...,ek) when C(n) = (e1 when C(n),...,ek when C(n))] *) -let rec whenc context e c n = +let rec whenc context e c n e_orig = let when_on_c c n e = - { e with e_desc = Ewhen(e, c, n) } + { e_orig with e_desc = Ewhen(e, c, n); } in if is_list e then ( let e_list = List.map (when_on_c c n) (e_to_e_list e) in - context, { e with e_desc = Eapp(mk_app Etuple, e_list, None) } + context, { e_orig with e_desc = Eapp(mk_app Etuple, e_list, None) } ) else context, when_on_c c n e @@ -131,7 +131,7 @@ let rec translate kind context e = context, { e with e_desc = Estruct l } | Ewhen(e1, c, n) -> let context, e1 = translate kind context e1 in - whenc context e1 c n + whenc context e1 c n e | Emerge(n, tag_e_list) -> merge context e n tag_e_list | Eapp({ a_op = Eifthenelse }, [e1; e2; e3], _) -> @@ -226,24 +226,43 @@ and merge context e x c_e_list = let context, e = translate ExtValue context e in (tag, e), context in - let mk_merge x c_list e_list = - let ty = (List.hd e_list).e_ty in - let t_e_list = List.map2 (fun t e -> (t,e)) c_list e_list in - mk_exp ~loc:e.e_loc (Emerge(x, t_e_list)) ty + let rec mk_merge x c_list e_lists = + let ty = (List.hd (List.hd e_lists)).e_ty in + let rec build_c_e_list c_list e_lists = + match c_list, e_lists with + | [], [] -> [], [] + | c::c_l, (e::e_l)::e_ls -> + let c_e_list, e_lists = build_c_e_list c_l e_ls in + (c,e)::c_e_list, e_l::e_lists + | _ -> assert false in + let rec build_merge_list c_list e_lists = + match e_lists with + [] -> assert false + | []::_ -> [] + | _ ::_ -> + let c_e_list, e_lists = build_c_e_list c_list e_lists in + let e_merge = mk_exp ~loc:e.e_loc (Emerge(x, c_e_list)) ty in + let e_merge_list = build_merge_list c_list e_lists in + e_merge::e_merge_list in + build_merge_list c_list e_lists in let c_e_list, context = mapfold translate_tag context c_e_list in match c_e_list with | [] -> assert false - | (_,e)::_ -> - if is_list e then ( + | (_,e1)::_ -> + if is_list e1 then ( let c_list = List.map (fun (t,_) -> t) c_e_list in let e_lists = List.map (fun (_,e) -> e_to_e_list e) c_e_list in let e_lists, context = - mapfold (fun context e_list -> add_list context ExtValue e_list) context e_lists in - let e_list = List.map (mk_merge x c_list) e_lists in - context, { e with e_desc = Eapp(mk_app Etuple, e_list, None) } + mapfold + (fun context e_list -> add_list context ExtValue e_list) + context e_lists in + let e_list = mk_merge x c_list e_lists in + context, { e with + e_desc = Eapp(mk_app Etuple, e_list, None) } ) else - context, { e with e_desc = Emerge(x, c_e_list) } + context, { e with + e_desc = Emerge(x, c_e_list) } (* applies distribution rules *) (* [(p1,...,pn) = (e1,...,en)] into [p1 = e1;...;pn = en] *) @@ -293,7 +312,23 @@ let block funs _ b = let _, (v_acc, eq_acc) = Hept_mapfold.block funs ([],[]) b in { b with b_local = v_acc@b.b_local; b_equs = eq_acc}, ([], []) +let contract funs context c = + let ({ c_block = b } as c), void_context = + Hept_mapfold.contract funs context c in + (* Non-void context could mean lost equations *) + assert (void_context=([],[])); + let context, e_a = translate ExtValue ([],[]) c.c_assume in + let context, e_e = translate ExtValue context c.c_enforce in + let (d_list, eq_list) = context in + { c with + c_assume = e_a; + c_enforce = e_e; + c_block = { b with + b_local = d_list@b.b_local; + b_equs = eq_list@b.b_equs; } + }, void_context + let program p = - let funs = { defaults with block = block; eq = eq } in + let funs = { defaults with block = block; eq = eq; contract = contract } in let p, _ = Hept_mapfold.program funs ([], []) p in p diff --git a/compiler/main/hept2mls.ml b/compiler/main/hept2mls.ml index ecc6908..79064aa 100644 --- a/compiler/main/hept2mls.ml +++ b/compiler/main/hept2mls.ml @@ -44,6 +44,16 @@ struct raise Errors.Error end +let fresh = Idents.gen_fresh "hept2mls" + (function Heptagon.Enode f -> (shortname f) + | _ -> "n") + +(* add an equation *) +let equation locals eqs e = + let n = Idents.gen_var "hept2mls" "ck" in + n, + (mk_var_dec n e.e_ty) :: locals, + (mk_equation (Evarpat n) e):: eqs let translate_var { Heptagon.v_ident = n; Heptagon.v_type = ty; Heptagon.v_linearity = linearity; Heptagon.v_loc = loc; Heptagon.v_clock = ck } = @@ -80,7 +90,9 @@ let rec translate_op = function let translate_app app = mk_app ~params:app.Heptagon.a_params - ~unsafe:app.Heptagon.a_unsafe (translate_op app.Heptagon.a_op) + ~unsafe:app.Heptagon.a_unsafe + ~id:(Some (fresh app.Heptagon.a_op)) + (translate_op app.Heptagon.a_op) let rec translate_extvalue e = let mk_extvalue = @@ -174,6 +186,7 @@ let node n = n_input = List.map translate_var n.Heptagon.n_input; n_output = List.map translate_var n.Heptagon.n_output; n_contract = translate_contract n.Heptagon.n_contract; + n_controller_call = ([],[]); n_local = List.map translate_var n.Heptagon.n_block.Heptagon.b_local; n_equs = List.map translate_eq n.Heptagon.n_block.Heptagon.b_equs; n_loc = n.Heptagon.n_loc ; @@ -181,6 +194,7 @@ let node n = n_param_constraints = n.Heptagon.n_param_constraints; n_mem_alloc = [] } + let typedec {Heptagon.t_name = n; Heptagon.t_desc = tdesc; Heptagon.t_loc = loc} = let onetype = function diff --git a/compiler/main/heptc.ml b/compiler/main/heptc.ml index 0f96b9b..72e6e5a 100644 --- a/compiler/main/heptc.ml +++ b/compiler/main/heptc.ml @@ -100,6 +100,8 @@ let main () = "-c", Arg.Set create_object_file, doc_object_file; "-s", Arg.String set_simulation_node, doc_sim; "-hepts", Arg.Set hepts_simulation, doc_hepts; + "-bool", Arg.Set boolean, doc_boolean; + "-deadcode", Arg.Set deadcode, doc_deadcode; "-tomato", Arg.Set tomato, doc_tomato; "-tomanode", read_qualname add_tomato_node, doc_tomato; "-tomacheck", read_qualname add_tomato_check, ""; diff --git a/compiler/main/mls2obc.ml b/compiler/main/mls2obc.ml index e8e9030..d7c6001 100644 --- a/compiler/main/mls2obc.ml +++ b/compiler/main/mls2obc.ml @@ -533,7 +533,12 @@ and mk_node_call map call_context app loc (name_list : Obc.pattern list) args ty v @ nd.Minils.n_local, si, j, subst_act_list env s | Minils.Enode f | Minils.Efun f -> - let o = mk_obj_call_from_context call_context (gen_obj_ident f) in + let id = + begin match app.Minils.a_id with + None -> gen_obj_ident f + | Some id -> id + end in + let o = mk_obj_call_from_context call_context id in let obj = { o_ident = obj_ref_name o; o_class = f; o_params = app.Minils.a_params; @@ -665,12 +670,12 @@ let translate_contract map mem_var_tys = (** Returns a map, mapping variables names to the variables where they will be stored. *) -let subst_map inputs outputs locals mem_tys = +let subst_map inputs outputs controllables c_locals locals mem_tys = (* Create a map that simply maps each var to itself *) let map = List.fold_left (fun m { Minils.v_ident = x; Minils.v_type = ty } -> Env.add x (mk_pattern ty (Lvar x)) m) - Env.empty (inputs @ outputs @ locals) + Env.empty (inputs @ outputs @ controllables @ c_locals @ locals) in List.fold_left (fun map (x, x_ty) -> Env.add x (mk_pattern x_ty (Lmem x)) map) map mem_tys @@ -682,7 +687,11 @@ let translate_node } as n) = Idents.enter_node f; let mem_var_tys = Mls_utils.node_memory_vars n in - let subst_map = subst_map i_list o_list d_list mem_var_tys in + let c_list, c_locals = + match contract with + | None -> [], [] + | Some c -> c.Minils.c_controllables, c.Minils.c_local in + let subst_map = subst_map i_list o_list c_list c_locals d_list mem_var_tys in let (v, si, j, s_list) = translate_eq_list subst_map empty_call_context eq_list in let (si', j', s_list', d_list') = translate_contract subst_map mem_var_tys contract in let i_list = translate_var_dec i_list in diff --git a/compiler/main/mls2seq.ml b/compiler/main/mls2seq.ml index 510705a..4b4b3c9 100644 --- a/compiler/main/mls2seq.ml +++ b/compiler/main/mls2seq.ml @@ -41,11 +41,13 @@ let write_obc_file p = let no_conf () = () let targets = [ "c",(Obc_no_params Cmain.program, no_conf); - "java", (Obc Java_main.program, no_conf); + "java", (Obc Java_main.program, no_conf); + "z3z", (Minils_no_params Sigalimain.program, no_conf); "obc", (Obc write_obc_file, no_conf); "obc_np", (Obc_no_params write_obc_file, no_conf); "epo", (Minils write_object_file, no_conf) ] + let generate_target p s = (* let print_unfolded p_list = comment "Unfolding"; diff --git a/compiler/minils/_tags b/compiler/minils/_tags index 305173d..7d88cc5 100644 --- a/compiler/minils/_tags +++ b/compiler/minils/_tags @@ -1 +1,2 @@ or or
or :include +:include \ No newline at end of file diff --git a/compiler/minils/analysis/clocking.ml b/compiler/minils/analysis/clocking.ml index bf2482a..5ff5e43 100644 --- a/compiler/minils/analysis/clocking.ml +++ b/compiler/minils/analysis/clocking.ml @@ -182,7 +182,8 @@ let typing_eq h { eq_lhs = pat; eq_rhs = e; eq_loc = loc } = e.e_base_ck <- base; (try unify ct e.e_ct with Unify -> - eprintf "Incoherent clock annotation.@\n"; + eprintf "Incoherent clock annotation for exp %a.@\n" + Mls_printer.print_exp e; error_message e.e_loc (Etypeclash (ct,e.e_ct))); e.e_ct <- ct; ct, base diff --git a/compiler/minils/main/mls_compiler.ml b/compiler/minils/main/mls_compiler.ml index 1ae59b0..a8855af 100644 --- a/compiler/minils/main/mls_compiler.ml +++ b/compiler/minils/main/mls_compiler.ml @@ -40,7 +40,7 @@ let compile_program p = let p = pass "Automata minimization checks" true Tomato.tomato_checks p pp in *) - + (* Scheduling *) let p = if !Compiler_options.use_interf_scheduler then diff --git a/compiler/minils/minils.ml b/compiler/minils/minils.ml index db0609d..6b48182 100644 --- a/compiler/minils/minils.ml +++ b/compiler/minils/minils.ml @@ -77,7 +77,11 @@ and edesc = * extvalue list * extvalue list * var_ident option (** map f <> <(extvalue)> (extvalue) reset ident *) -and app = { a_op: op; a_params: static_exp list; a_unsafe: bool } +and app = { a_op: op; + a_params: static_exp list; + a_unsafe: bool; + a_id: ident option; + a_inlined: bool } (** Unsafe applications could have side effects and be delicate about optimizations, !be careful! *) @@ -126,6 +130,8 @@ type node_dec = { n_input : var_dec list; n_output : var_dec list; n_contract : contract option; + (* GD: inglorious hack for controller call *) + mutable n_controller_call : string list * string list; n_local : var_dec list; n_equs : eq list; n_loc : location; @@ -173,7 +179,8 @@ let mk_equation ?(loc = no_location) pat exp = { eq_lhs = pat; eq_rhs = exp; eq_loc = loc } let mk_node - ?(input = []) ?(output = []) ?(contract = None) ?(local = []) ?(eq = []) + ?(input = []) ?(output = []) ?(contract = None) ?(pinst = ([],[])) + ?(local = []) ?(eq = []) ?(stateful = true) ?(loc = no_location) ?(param = []) ?(constraints = []) ?(mem_alloc=[]) name = @@ -182,6 +189,7 @@ let mk_node n_input = input; n_output = output; n_contract = contract; + n_controller_call = pinst; n_local = local; n_equs = eq; n_loc = loc; @@ -195,6 +203,7 @@ let mk_type_dec type_desc name loc = let mk_const_dec id ty e loc = { c_name = id; c_type = ty; c_value = e; c_loc = loc } -let mk_app ?(params=[]) ?(unsafe=false) op = - { a_op = op; a_params = params; a_unsafe = unsafe } +let mk_app ?(params=[]) ?(unsafe=false) ?(id=None) ?(inlined=false) op = + { a_op = op; a_params = params; a_unsafe = unsafe; + a_id = id; a_inlined = inlined } diff --git a/compiler/minils/mls_printer.ml b/compiler/minils/mls_printer.ml index 5405a33..cc44fdc 100644 --- a/compiler/minils/mls_printer.ml +++ b/compiler/minils/mls_printer.ml @@ -30,9 +30,9 @@ let rec print_pat ff = function fprintf ff "@[<2>(%a)@]" (print_list_r print_pat """,""") pat_list let print_vd ff { v_ident = n; v_type = ty; v_linearity = lin; v_clock = ck } = - (* if !Compiler_options.full_type_info then*) + if !Compiler_options.full_type_info then fprintf ff "%a : %a%a :: %a" print_ident n print_type ty print_linearity lin print_ck ck - (*else fprintf ff "%a : %a" print_ident n print_type ty*) + else fprintf ff "%a : %a" print_ident n print_type ty let print_local_vars ff = function | [] -> () @@ -195,7 +195,7 @@ let rec print_type_dec ff { t_name = name; t_desc = tdesc } = let print_contract ff { c_local = l; c_eq = eqs; c_assume = e_a; c_enforce = e_g; c_controllables = c;} = - fprintf ff "@[contract@\n%a%a@ assume %a@ enforce %a@ with (%a)@]" + fprintf ff "@[contract@\n%a%a@ assume %a@ enforce %a@ with %a@\n@]" print_local_vars l print_eqs eqs print_extvalue e_a diff --git a/compiler/minils/sigali/sigali.ml b/compiler/minils/sigali/sigali.ml new file mode 100644 index 0000000..5599058 --- /dev/null +++ b/compiler/minils/sigali/sigali.ml @@ -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 "@[%a : %a;@]" + print_name name + print_exp e + + let print_statements ff stmt_l = + fprintf ff "@["; + 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(@[d1"; + for i = 2 to n do + fprintf ff ",@ d%d" i; + done; + fprintf ff "@]);@]@\n@\n"; + + fprintf ff "@["; + + (* 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(@["; + 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 "@["; + 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 "@["; + 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(@["; + 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 + diff --git a/compiler/minils/sigali/sigali.mli b/compiler/minils/sigali/sigali.mli new file mode 100644 index 0000000..8293878 --- /dev/null +++ b/compiler/minils/sigali/sigali.mli @@ -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 diff --git a/compiler/minils/sigali/sigalimain.ml b/compiler/minils/sigali/sigalimain.ml new file mode 100644 index 0000000..c01390c --- /dev/null +++ b/compiler/minils/sigali/sigalimain.ml @@ -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 + diff --git a/compiler/minils/sigali/sigalimain.mli b/compiler/minils/sigali/sigalimain.mli new file mode 100644 index 0000000..195b8cb --- /dev/null +++ b/compiler/minils/sigali/sigalimain.mli @@ -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 diff --git a/compiler/minils/transformations/normalize_mem.ml b/compiler/minils/transformations/normalize_mem.ml index c2849cb..52bc6a8 100644 --- a/compiler/minils/transformations/normalize_mem.ml +++ b/compiler/minils/transformations/normalize_mem.ml @@ -33,6 +33,9 @@ let eq _ (outputs, eqs, env) eq = match eq.eq_lhs, eq.eq_rhs.e_desc with | _, _ -> eq, (outputs, eq::eqs, env) +(* Leave contract unchanged (no output defined in it) *) +let contract funs acc c = c, acc + let node funs acc nd = let nd, (_, eqs, env) = Mls_mapfold.node_dec funs (nd.n_output, [], Env.empty) nd in let v = Env.fold @@ -46,6 +49,7 @@ let node funs acc nd = { nd with n_local = v; n_equs = List.rev eqs; n_output = o }, acc let program p = - let funs = { Mls_mapfold.defaults with eq = eq; node_dec = node } in + let funs = { Mls_mapfold.defaults with + eq = eq; node_dec = node; contract = contract } in let p, _ = Mls_mapfold.program_it funs ([], [], Env.empty) p in p diff --git a/compiler/utilities/global/compiler_options.ml b/compiler/utilities/global/compiler_options.ml index 7148d8c..5a6e968 100644 --- a/compiler/utilities/global/compiler_options.ml +++ b/compiler/utilities/global/compiler_options.ml @@ -60,10 +60,13 @@ let hepts_simulation = ref false let create_object_file = ref false +let boolean = ref false + (* Target languages list for code generation *) let target_languages : string list ref = ref [] let add_target_language s = + if s = "z3z" then boolean := true; target_languages := s :: !target_languages (* Optional path for generated files (C or Java) *) @@ -84,6 +87,8 @@ let add_inlined_node s = inline := s :: !inline let flatten = ref false +let deadcode = ref false + let tomato = ref false let tomato_nodes : qualname list ref = ref [] @@ -121,6 +126,8 @@ and doc_full_name = "\t\t\tPrint full variable name information" and doc_target_path = "\tGenerated files will be placed in \n\t\t\t(the directory is" ^ " cleaned)" +and doc_boolean = "\t\tTranslate enumerated values towards boolean vectors" +and doc_deadcode = "\t\tDeadcode removal" and doc_nocaus = "\t\tDisable causality analysis" and doc_noinit = "\t\tDisable initialization analysis" and doc_assert = "\t\tInsert run-time assertions for boolean node " diff --git a/compiler/utilities/minils/interference2dot.ml b/compiler/utilities/minils/interference2dot.ml index 83736af..a6aedf2 100644 --- a/compiler/utilities/minils/interference2dot.ml +++ b/compiler/utilities/minils/interference2dot.ml @@ -9,7 +9,8 @@ module DotG = struct let name = ref "" let color_to_graphviz_color i = - (i * 8364263947 + 855784368) + (* (i * 8364263947 + 855784368) *) + (i * 2 + 1) (*Functions for printing the graph *) let default_vertex_attributes _ = [] diff --git a/compiler/utilities/misc.ml b/compiler/utilities/misc.ml index 9d92b04..dc56977 100644 --- a/compiler/utilities/misc.ml +++ b/compiler/utilities/misc.ml @@ -226,30 +226,30 @@ let fold_righti f l acc = exception Assert_false let internal_error passe = - Format.eprintf "@.---------\n - Internal compiler error\n - Passe : %s\n + Format.eprintf "@.---------@\n + Internal compiler error@\n + Passe : %s@\n ----------@." passe; raise Assert_false exception Unsupported let unsupported passe = - Format.eprintf "@.---------\n - Unsupported feature, please report it\n - Passe : %s\n + Format.eprintf "@.---------@\n + Unsupported feature, please report it@\n + Passe : %s@\n ----------@." passe; raise Unsupported (* Functions to decompose a list into a tuple *) let _arity_error i l = - Format.eprintf "@.---------\n - Internal compiler error: wrong list size (found %d, expected %d).\n + Format.eprintf "@.---------@\n + Internal compiler error: wrong list size (found %d, expected %d).@\n ----------@." (List.length l) i; raise Assert_false let _arity_min_error i l = - Format.eprintf "@.---------\n - Internal compiler error: wrong list size (found %d, expected %d at least).\n + Format.eprintf "@.---------@\n + Internal compiler error: wrong list size (found %d, expected %d at least).@\n ----------@." (List.length l) i; raise Assert_false diff --git a/test/check b/test/check index a205537..219cd45 100755 --- a/test/check +++ b/test/check @@ -17,13 +17,16 @@ coption=-memalloc CAMLC=ocamlc JAVAC=javac LUSTREC=lustre -CC="gcc -std=c99 -I../../../lib/c" +CC="gcc -std=c99 -I../../../lib/c -I../t1_c" # par defaut : pas de test de generation de code tomato=0 java=0 +lustre=0 c=0 +minils=0 +vhdl=0 score=0 max=0 @@ -94,7 +97,7 @@ launch_check () { done echo echo "Tests goods" - for f in ../good/*.ept ../image_filters/*.ept; do + for f in ../good/*.ept; do echec=0 if [ $verbose = 0 ]; then echo -n "." @@ -115,18 +118,26 @@ launch_check () { fi fi # Compil. java ? - #if [[ ($echec == 0) && ($java == 1) ]]; then - # pushd "${base_f}_java" > /dev/null - # for java_file in *.java ; do - # if $JAVAC -warn:-unused -sourcepath .:..:../t1 ${java_file} > /dev/null - # then - # echec=0 - # else - # echec=3 - # fi - # done - # popd > /dev/null - #fi + if [[ ($echec == 0) && ($java == 1) ]]; then + pushd "${base_f}" > /dev/null + for java_file in *.java ; do + if $JAVAC -warn:-unused -sourcepath .:..:../t1 ${java_file} > /dev/null + then + echec=0 + else + echec=3 + fi + done + popd > /dev/null + fi + # Compil. caml ? + if [[ ($echec == 0) && ($caml == 1) ]]; then + if $CAMLC -c ${base_f}.ml > /dev/null; then + echec=0 + else + echec=4 + fi + fi # Compil. c ? if [[ ($echec == 0) && ($c == 1) ]]; then pushd ${base_f}_c >/dev/null @@ -163,6 +174,18 @@ launch_check () { fi popd >/dev/null fi + # Compil. VHDL ? + if [[ ($echec == 0) && ($vhdl == 1) ]]; then + pushd ${base_f}_vhdl > /dev/null + for vhdl_file in *.vhd; do + if $VHDLC -a ${vhdl_file} && $VHDLC -e ${vhdl_file} > /dev/null 2>&1 + then + echec=${echec} + else + echec=8 + fi + done + fi if [[ $echec == 0 ]]; then score=`expr $score + 1`; @@ -172,8 +195,12 @@ launch_check () { case $echec in 1 ) echo "Compilation failed.";; + 2 ) + echo "Compilation to Minils failed.";; 3 ) - echo "Java compilation failed.";; + echo "Compilation to Java failed.";; + 4 ) + echo "Compilation to Caml failed.";; 5 ) echo "C compilation failed.";; 6 ) @@ -203,6 +230,16 @@ activate_java () { coption="$coption -target java" } +activate_caml () { + caml=1 + coption="$coption -target caml" +} + +activate_vhdl () { + vhdl=1 + coption="$coption -target vhdl" +} + activate_c () { c=1 coption="$coption -target c" @@ -218,6 +255,14 @@ activate_all () { activate_c } +activate_boolean () { + coption="$coption -bool" +} + +activate_deadcode () { + coption="$coption -deadcode" +} + while [ $# -gt 0 ]; do case $1 in "-clean" ) @@ -235,17 +280,35 @@ while [ $# -gt 0 ]; do "-c" ) activate_c shift;; + "-caml" ) + activate_caml + shift;; + "-vhdl" ) + activate_vhdl + shift;; "-mls" ) activate_minils shift;; "-tomato" ) activate_tomato shift;; + "-bool" ) + activate_boolean + shift;; + "-deadcode" ) + activate_deadcode + shift;; "-h" ) echo "usage : $0 " echo "options : " echo "-clean : clean build dir" echo "-java : test of code generation (java code)" + echo "-caml : test of code generation (caml code)" + echo "-lustre : test of code generation (lustre code)" + echo "-vhdl : test of code generation (vhdl)" + echo "-bool : test of boolean translation" + echo "-deadcode : test of deadcode removal" + echo "-tomato : test of automata minimization" echo "-c : test of code generation (c code)" echo "-all : test all" echo "-v : verbose"