From b49c37f7bf0e7c0ac296e303a310fb4331990ac0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Le=CC=81onard=20Ge=CC=81rard?= Date: Sun, 20 Nov 2011 23:21:24 +0100 Subject: [PATCH] Add ways to declare unsafe functions + unsafe fix --- compiler/global/signature.ml | 4 +- compiler/heptagon/analysis/unsafe.ml | 64 +++++++++++++++++++++ compiler/heptagon/hept_utils.ml | 4 +- compiler/heptagon/heptagon.ml | 1 + compiler/heptagon/main/hept_compiler.ml | 1 + compiler/heptagon/parsing/hept_lexer.mll | 1 + compiler/heptagon/parsing/hept_parser.mly | 12 +++- compiler/heptagon/parsing/hept_parsetree.ml | 2 + compiler/heptagon/parsing/hept_scoping.ml | 21 ++----- compiler/main/hept2mls.ml | 19 ++++-- compiler/minils/analysis/interference.ml | 4 +- compiler/minils/minils.ml | 41 ++++++------- compiler/minils/mls_utils.ml | 4 +- compiler/minils/transformations/tomato.ml | 4 +- 14 files changed, 131 insertions(+), 51 deletions(-) create mode 100644 compiler/heptagon/analysis/unsafe.ml diff --git a/compiler/global/signature.ml b/compiler/global/signature.ml index 1b2e72a..6bc12ae 100644 --- a/compiler/global/signature.ml +++ b/compiler/global/signature.ml @@ -39,6 +39,7 @@ type node = { node_inputs : arg list; node_outputs : arg list; node_stateful : bool; + node_unsafe : bool; node_params : param list; node_param_constraints : constrnt list; node_loc : location} @@ -136,10 +137,11 @@ let mk_field n ty = { f_name = n; f_type = ty } let mk_const_def ty value = { c_type = ty; c_value = value } -let mk_node ?(constraints = []) loc ins outs stateful params = +let mk_node ?(constraints = []) loc ins outs stateful unsafe params = { node_inputs = ins; node_outputs = outs; node_stateful = stateful; + node_unsafe = unsafe; node_params = params; node_param_constraints = constraints; node_loc = loc} diff --git a/compiler/heptagon/analysis/unsafe.ml b/compiler/heptagon/analysis/unsafe.ml new file mode 100644 index 0000000..1d6a75e --- /dev/null +++ b/compiler/heptagon/analysis/unsafe.ml @@ -0,0 +1,64 @@ +(**************************************************************************) +(* *) +(* Heptagon *) +(* *) +(* Author : Marc Pouzet *) +(* Organization : Demons, LRI, University of Paris-Sud, Orsay *) +(* *) +(**************************************************************************) +(* Checks that a node not declared unsafe is safe, and set app unsafe flag. *) +open Names +open Location +open Signature +open Modules +open Heptagon +open Hept_mapfold + +type error = + | Eshould_be_unsafe + +let message loc kind = + begin match kind with + | Eshould_be_unsafe -> + Format.eprintf "%aThis exp is unsafe but the current node is not declared unsafe.@." + print_location loc + end; + raise Errors.Error + +(* Returns whether an op is unsafe *) +let unsafe_op op = match op with + | Enode f | Efun f -> + (find_value f).node_unsafe + | _ -> (*TODO il y a des op unsafe ??*) + false + +(* Update app unsafe field + and gives an error if some exp is unsafe in a safe node ([unsafe]=false) *) +let exp funs unsafe e = + let e, unsafe = Hept_mapfold.exp funs unsafe e in + match e.e_desc with + | Eapp({ a_op = op } as app, e_l, r) -> + let u = (unsafe_op op) or app.a_unsafe in + if u & (not unsafe) + then message e.e_loc Eshould_be_unsafe + else {e with e_desc = Eapp({ app with a_unsafe = u }, e_l, r)}, (unsafe or u) + | Eiterator(it, ({ a_op = op } as app), n, pe_list, e_list, r) -> + let u = (unsafe_op op) or app.a_unsafe in + if u & (not unsafe) + then message e.e_loc Eshould_be_unsafe + else + {e with e_desc = Eiterator(it, { app with a_unsafe = u }, n, pe_list, e_list, r)} + , (unsafe or u) + | _ -> e, unsafe + +(* unsafe nodes are rejected if they are not declared unsafe *) +let node_dec funs _ n = Hept_mapfold.node_dec funs n.n_unsafe n + +let funs = + { Hept_mapfold.defaults with + exp = exp; + node_dec = node_dec; } + +let program p = + let p, _ = Hept_mapfold.program_it funs false p in + p diff --git a/compiler/heptagon/hept_utils.ml b/compiler/heptagon/hept_utils.ml index 1da4b53..a21d72a 100644 --- a/compiler/heptagon/hept_utils.ml +++ b/compiler/heptagon/hept_utils.ml @@ -74,10 +74,11 @@ let mk_signature name ins outs stateful params constraints loc = let mk_node ?(input = []) ?(output = []) ?(contract = None) - ?(stateful = true) ?(loc = no_location) ?(param = []) ?(constraints = []) + ?(stateful = true) ?(unsafe = false) ?(loc = no_location) ?(param = []) ?(constraints = []) name block = { n_name = name; n_stateful = stateful; + n_unsafe = unsafe; n_input = input; n_output = output; n_contract = contract; @@ -112,6 +113,7 @@ 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_unsafe = n.n_unsafe; node_params = n.n_params; node_param_constraints = n.n_param_constraints; node_loc = n.n_loc } diff --git a/compiler/heptagon/heptagon.ml b/compiler/heptagon/heptagon.ml index 7bdcf5e..2df60c4 100644 --- a/compiler/heptagon/heptagon.ml +++ b/compiler/heptagon/heptagon.ml @@ -150,6 +150,7 @@ type contract = { type node_dec = { n_name : qualname; n_stateful : bool; + n_unsafe : bool; n_input : var_dec list; n_output : var_dec list; n_contract : contract option; diff --git a/compiler/heptagon/main/hept_compiler.ml b/compiler/heptagon/main/hept_compiler.ml index c5fd40b..190c454 100644 --- a/compiler/heptagon/main/hept_compiler.ml +++ b/compiler/heptagon/main/hept_compiler.ml @@ -17,6 +17,7 @@ let pp p = if !verbose then Hept_printer.print stdout p let compile_program p = (* Typing *) let p = silent_pass "Statefulness check" true Stateful.program p in + let p = silent_pass "Unsafe check" true Unsafe.program p in let p = pass "Typing" true Typing.program p pp in let p = pass "Linear Typing" !do_linear_typing Linear_typing.program p pp in diff --git a/compiler/heptagon/parsing/hept_lexer.mll b/compiler/heptagon/parsing/hept_lexer.mll index 292034e..de00206 100644 --- a/compiler/heptagon/parsing/hept_lexer.mll +++ b/compiler/heptagon/parsing/hept_lexer.mll @@ -68,6 +68,7 @@ List.iter (fun (str,tok) -> Hashtbl.add keyword_table str tok) [ "init", INIT; "split", SPLIT; "reinit", REINIT; + "unsafe", UNSAFE; "quo", INFIX3("quo"); "mod", INFIX3("mod"); "land", INFIX3("land"); diff --git a/compiler/heptagon/parsing/hept_parser.mly b/compiler/heptagon/parsing/hept_parser.mly index 12fd71c..1d9ab96 100644 --- a/compiler/heptagon/parsing/hept_parser.mly +++ b/compiler/heptagon/parsing/hept_parser.mly @@ -18,7 +18,7 @@ open Hept_parsetree %token FLOAT %token BOOL %token PRAGMA -%token TYPE FUN NODE RETURNS VAR VAL OPEN END CONST +%token TYPE FUN NODE RETURNS VAR VAL OPEN END CONST UNSAFE %token FBY PRE SWITCH EVERY %token OR STAR NOT %token AMPERSAND @@ -170,11 +170,12 @@ returns: RETURNS | EQUAL {} ; node_dec: - | n=node_or_fun f=ident pc=node_params LPAREN i=in_params RPAREN + | u=unsafe n=node_or_fun f=ident pc=node_params LPAREN i=in_params RPAREN returns LPAREN o=out_params RPAREN c=contract b=block(LET) TEL {{ n_name = f; n_stateful = n; + n_unsafe = u; n_input = i; n_output = o; n_contract = c; @@ -655,14 +656,19 @@ interface: { { i_modname = ""; i_opened = o; i_desc = i } } ; +unsafe: + | UNSAFE { true } + | /*empty*/ { false } + interface_desc: | type_dec { Itypedef $1 } | const_dec { Iconstdef $1 } - | VAL n=node_or_fun f=ident pc=node_params LPAREN i=params_signature RPAREN + | u=unsafe VAL n=node_or_fun f=ident pc=node_params LPAREN i=params_signature RPAREN returns LPAREN o=params_signature RPAREN { Isignature({ sig_name = f; sig_inputs = i; sig_stateful = n; + sig_unsafe = u; sig_outputs = o; sig_params = fst pc; sig_param_constraints = snd pc; diff --git a/compiler/heptagon/parsing/hept_parsetree.ml b/compiler/heptagon/parsing/hept_parsetree.ml index cef9123..dd82838 100644 --- a/compiler/heptagon/parsing/hept_parsetree.ml +++ b/compiler/heptagon/parsing/hept_parsetree.ml @@ -177,6 +177,7 @@ type contract = type node_dec = { n_name : dec_name; n_stateful : bool; + n_unsafe : bool; n_input : var_dec list; n_output : var_dec list; n_contract : contract option; @@ -213,6 +214,7 @@ type signature = { sig_name : dec_name; sig_inputs : arg list; sig_stateful : bool; + sig_unsafe : bool; sig_outputs : arg list; sig_params : var_dec list; sig_param_constraints : exp list; diff --git a/compiler/heptagon/parsing/hept_scoping.ml b/compiler/heptagon/parsing/hept_scoping.ml index 9918232..8de8815 100644 --- a/compiler/heptagon/parsing/hept_scoping.ml +++ b/compiler/heptagon/parsing/hept_scoping.ml @@ -200,15 +200,6 @@ let translate_iterator_type = function | Ifoldi -> Heptagon.Ifoldi | Imapfold -> Heptagon.Imapfold -(** convention : static params are set as the first static args, - op (a3) == op (a2,a3) == op (a1,a2,a3) *) -let static_app_from_app app args= - match app.a_op with - | Efun (Q ({ qual = Pervasives } as q)) - | Enode (Q ({ qual = Pervasives } as q)) -> - q, (app.a_params @ args) - | _ -> raise Not_static - let rec translate_static_exp se = try let se_d = translate_static_exp_desc se.se_loc se.se_desc in @@ -430,11 +421,10 @@ let translate_contract env opt_ct = | 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' + 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 = @@ -476,6 +466,7 @@ let translate_node node = (* add the node signature to the environment *) let nnode = { Heptagon.n_name = n; Heptagon.n_stateful = node.n_stateful; + Heptagon.n_unsafe = node.n_unsafe; Heptagon.n_input = inputs; Heptagon.n_output = outputs; Heptagon.n_contract = contract; @@ -555,7 +546,7 @@ let translate_signature s = let o = List.map translate_arg s.sig_outputs in let p, _ = params_of_var_decs Rename.empty s.sig_params in let c = List.map translate_constrnt s.sig_param_constraints in - let sig_node = Signature.mk_node s.sig_loc i o s.sig_stateful p in + let sig_node = Signature.mk_node s.sig_loc i o s.sig_stateful s.sig_unsafe p in Signature.check_signature sig_node; safe_add s.sig_loc add_value n sig_node; mk_signature n i o s.sig_stateful p c s.sig_loc diff --git a/compiler/main/hept2mls.ml b/compiler/main/hept2mls.ml index 1f148a8..63e8a6e 100644 --- a/compiler/main/hept2mls.ml +++ b/compiler/main/hept2mls.ml @@ -90,9 +90,12 @@ let translate_app app = let rec translate_extvalue e = let mk_extvalue = - mk_extvalue - ~loc:e.Heptagon.e_loc ~linearity:e.Heptagon.e_linearity ~ty:e.Heptagon.e_ty - ~clock:(match e.Heptagon.e_ct_annot with None -> fresh_clock () | Some ct -> assert_1 (unprod ct)) + let clock = match e.Heptagon.e_ct_annot with + | None -> fresh_clock () + | Some ct -> assert_1 (unprod ct) + in + mk_extvalue ~loc:e.Heptagon.e_loc ~linearity:e.Heptagon.e_linearity + ~ty:e.Heptagon.e_ty ~clock:clock in match e.Heptagon.e_desc with | Heptagon.Econst c -> mk_extvalue (Wconst c) @@ -156,11 +159,15 @@ let rec translate_pat = function | Heptagon.Evarpat(n) -> Evarpat n | Heptagon.Etuplepat(l) -> Etuplepat (List.map translate_pat l) -let rec translate_eq - { Heptagon.eq_desc = desc; Heptagon.eq_loc = loc } = +let rec translate_eq { Heptagon.eq_desc = desc; Heptagon.eq_loc = loc } = match desc with | Heptagon.Eeq(p, e) -> - mk_equation ~loc:loc (translate_pat p) (translate e) + begin match e.Heptagon.e_desc with + | Heptagon.Eapp({ Heptagon.a_unsafe = unsafe },_,_) + | Heptagon.Eiterator(_,{ Heptagon.a_unsafe = unsafe},_,_,_,_) -> + mk_equation ~loc:loc unsafe (translate_pat p) (translate e) + | _ -> mk_equation ~loc:loc false (translate_pat p) (translate e) + end | Heptagon.Eblock _ | Heptagon.Eswitch _ | Heptagon.Epresent _ | Heptagon.Eautomaton _ | Heptagon.Ereset _ -> Error.message loc Error.Eunsupported_language_construct diff --git a/compiler/minils/analysis/interference.ml b/compiler/minils/analysis/interference.ml index 1adca56..93639c3 100644 --- a/compiler/minils/analysis/interference.ml +++ b/compiler/minils/analysis/interference.ml @@ -484,10 +484,10 @@ let process_eq ({ eq_lhs = pat; eq_rhs = e } as eq) = (resp at the bottom and top) *) let add_init_return_eq f = (** a_1,..,a_p = __init__ *) - let eq_init = mk_equation (Mls_utils.pat_from_dec_list f.n_input) + let eq_init = mk_equation false (Mls_utils.pat_from_dec_list f.n_input) (mk_extvalue_exp Cbase Initial.tint Ltop (Wconst (Initial.mk_static_int 0))) in (** __return__ = o_1,..,o_q *) - let eq_return = mk_equation (Etuplepat []) + let eq_return = mk_equation false (Etuplepat []) (mk_exp Cbase Tinvalid Ltop (Mls_utils.tuple_from_dec_list f.n_output)) in (eq_init::f.n_equs)@[eq_return] diff --git a/compiler/minils/minils.ml b/compiler/minils/minils.ml index eebd121..d548000 100644 --- a/compiler/minils/minils.ml +++ b/compiler/minils/minils.ml @@ -106,36 +106,37 @@ type pat = | Evarpat of var_ident type eq = { - eq_lhs : pat; - eq_rhs : exp; - eq_loc : location } + eq_lhs : pat; + eq_rhs : exp; + eq_unsafe : bool; + eq_loc : location } type var_dec = { - v_ident : var_ident; - v_type : ty; + v_ident : var_ident; + v_type : ty; v_linearity : linearity; - v_clock : ck; - v_loc : location } + v_clock : ck; + v_loc : location } type contract = { - c_assume : extvalue; - c_enforce : extvalue; + c_assume : extvalue; + c_enforce : extvalue; c_controllables : var_dec list; - c_local : var_dec list; - c_eq : eq list } + c_local : var_dec list; + c_eq : eq list } type node_dec = { - n_name : qualname; + n_name : qualname; n_stateful : bool; - n_input : var_dec list; - n_output : var_dec list; + 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; - n_params : param list; + n_local : var_dec list; + n_equs : eq list; + n_loc : location; + n_params : param list; n_param_constraints : constrnt list; n_mem_alloc : (ty * Interference_graph.ivar list) list; } @@ -195,8 +196,8 @@ let mk_extvalue_exp ?(clock = fresh_clock()) mk_exp ~ck:clock ~loc:loc level_ck ty ~linearity:linearity (Eextvalue (mk_extvalue ~clock:clock ~loc:loc ~linearity:linearity ~ty:ty desc)) -let mk_equation ?(loc = no_location) pat exp = - { eq_lhs = pat; eq_rhs = exp; eq_loc = loc } +let mk_equation ?(loc = no_location) unsafe pat exp = + { eq_lhs = pat; eq_rhs = exp; eq_unsafe = unsafe; eq_loc = loc } let mk_node ?(input = []) ?(output = []) ?(contract = None) ?(pinst = ([],[])) diff --git a/compiler/minils/mls_utils.ml b/compiler/minils/mls_utils.ml index 606e12a..649c475 100644 --- a/compiler/minils/mls_utils.ml +++ b/compiler/minils/mls_utils.ml @@ -233,7 +233,9 @@ let remove_eqs_from_node nd ids = let walk_vd vd vd_list = if IdentSet.mem vd.v_ident ids then vd_list else vd :: vd_list in let walk_eq eq eq_list = let defs = ident_list_of_pat eq.eq_lhs in - if List.for_all (fun v -> IdentSet.mem v ids) defs then eq_list else eq :: eq_list + if (not eq.eq_unsafe) & List.for_all (fun v -> IdentSet.mem v ids) defs + then eq_list + else eq :: eq_list in let vd_list = List.fold_right walk_vd nd.n_local [] in let eq_list = List.fold_right walk_eq nd.n_equs [] in diff --git a/compiler/minils/transformations/tomato.ml b/compiler/minils/transformations/tomato.ml index 5cad2fc..e9500df 100644 --- a/compiler/minils/transformations/tomato.ml +++ b/compiler/minils/transformations/tomato.ml @@ -356,7 +356,7 @@ let rec reconstruct ((tenv, cenv) as env) mapping = let pat = reconstruct_pattern mapping repr.er_pattern in - mk_equation pat e :: eq_list in + mk_equation false pat e :: eq_list in IntMap.fold reconstruct_class cenv [] and reconstruct_exp_desc mapping headd children = @@ -555,7 +555,7 @@ let rec fix_output_var_dec mapping vd (seen, equs, vd_list) = let new_vd = { vd with v_ident = new_id; v_clock = new_clock } in let new_eq = let w = mk_extvalue ~ty:vd.v_type ~clock:new_clock ~linearity:Linearity.Ltop (Wvar x) in - mk_equation + mk_equation false (Evarpat new_id) (mk_exp new_clock vd.v_type ~ct:(Ck new_clock) ~ck:new_clock ~linearity:Linearity.Ltop (Eextvalue w))