diff --git a/compiler/global/signature.ml b/compiler/global/signature.ml index 71caa36..d8b60b6 100644 --- a/compiler/global/signature.ml +++ b/compiler/global/signature.ml @@ -13,7 +13,7 @@ open Static (** Warning: Whenever these types are modified, interface_format_version should be incremented. *) -let interface_format_version = "6" +let interface_format_version = "7" (** Node argument *) type arg = { a_name : name option; a_type : ty } @@ -24,6 +24,7 @@ type param = { p_name : name } type node = { node_inputs : arg list; node_outputs : arg list; + node_statefull : bool; node_params : param list; (** Static parameters *) node_params_constraints : size_constr list } diff --git a/compiler/heptagon/analysis/initialization.ml b/compiler/heptagon/analysis/initialization.ml index f750eab..69ca1c4 100644 --- a/compiler/heptagon/analysis/initialization.ml +++ b/compiler/heptagon/analysis/initialization.ml @@ -234,8 +234,8 @@ and apply h op e_list = let i2 = itype (typing h e2) in let i3 = itype (typing h e3) in max i1 (max i2 i3) - | Ecall ({ op_kind = Eop }, _), e_list -> - List.fold_left (fun acc e -> itype (typing h e)) izero e_list + (* | Ecall ({ op_kind = Efun }, _), e_list -> + List.fold_left (fun acc e -> itype (typing h e)) izero e_list *) | (Ecall _ | Earray_op _| Efield_update _) , e_list -> List.iter (fun e -> initialized_exp h e) e_list; izero diff --git a/compiler/heptagon/analysis/interface.ml b/compiler/heptagon/analysis/interface.ml index fdbbe19..551e6b4 100644 --- a/compiler/heptagon/analysis/interface.ml +++ b/compiler/heptagon/analysis/interface.ml @@ -19,11 +19,12 @@ open Types module Type = struct - let sigtype { sig_name = name; sig_inputs = i_list; + let sigtype { sig_name = name; sig_inputs = i_list; sig_statefull = statefull; sig_outputs = o_list; sig_params = params } = let check_arg a = { a with a_type = check_type a.a_type } in name, { node_inputs = List.map check_arg i_list; node_outputs = List.map check_arg o_list; + node_statefull = statefull; node_params = params; node_params_constraints = []; } diff --git a/compiler/heptagon/analysis/typing.ml b/compiler/heptagon/analysis/typing.ml index fb0725f..ef98a1d 100644 --- a/compiler/heptagon/analysis/typing.ml +++ b/compiler/heptagon/analysis/typing.ml @@ -222,14 +222,59 @@ let rec unify t1 t2 = let unify t1 t2 = try unify t1 t2 with Unify -> error (Etype_clash(t1, t2)) -let less_than statefull = (*if not statefull then error Estate_clash*) () +let less_than statefull = if not statefull then error Estate_clash -let kind f statefull = function - | { node_inputs = ty_list1; - node_outputs = ty_list2 } -> - let ty_of_arg v = v.a_type in - (*if n & not(statefull) then error (Eshould_be_a_node(f)) *) - (*else n,*) List.map ty_of_arg ty_list1, List.map ty_of_arg ty_list2 +let rec is_statefull_exp e = + match e.e_desc with + | Econst _ | Econstvar _ | Evar _-> false + | Elast _ -> true + | Etuple e_list -> List.exists is_statefull_exp e_list + | Eapp({ a_op = (Efby | Epre _ | Earrow) }, _) -> true + | Eapp({ a_op = Ecall ({ op_kind = Enode }, _)}, _) -> true + | Eapp(_, e_list) -> List.exists is_statefull_exp e_list + | Efield(e, _) -> is_statefull_exp e + | Estruct _ | Earray _ -> false + +let rec is_statefull_eq_desc = function + | Eautomaton(handlers) -> + (List.exists is_statefull_state_handler handlers) + | Eswitch(e, handlers) -> + (is_statefull_exp e) or + (List.exists is_statefull_switch_handler handlers) + | Epresent(handlers, b) -> + (is_statefull_block b) or + (List.exists is_statefull_present_handler handlers) + | Ereset(eq_list, e) -> + (is_statefull_exp e) or + (List.exists (fun eq -> eq.eq_statefull) eq_list) + | Eeq(_, e) -> is_statefull_exp e + +and is_statefull_block b = + b.b_statefull + +and is_statefull_present_handler ph = + (is_statefull_exp ph.p_cond) or + (is_statefull_block ph.p_block) + +and is_statefull_switch_handler sh = + is_statefull_block sh.w_block + +and is_statefull_state_handler sh = + (is_statefull_block sh.s_block) or + (List.exists is_statefull_escape sh.s_until) or + (List.exists is_statefull_escape sh.s_unless) + +and is_statefull_escape esc = + is_statefull_exp esc.e_cond + +let kind f statefull k + { node_inputs = ty_list1; + node_outputs = ty_list2; + node_statefull = n } = + let ty_of_arg v = v.a_type in + let k = if n then Enode else Efun in + if n & not(statefull) then error (Eshould_be_a_node f) + else k, List.map ty_of_arg ty_list1, List.map ty_of_arg ty_list2 let prod = function | [] -> assert false @@ -386,7 +431,7 @@ let check_field_unicity l = else S.add (shortname f) acc in - List.fold_left add_field S.empty l + ignore (List.fold_left add_field S.empty l) (** @return the qualified name and list of fields of the type with name [n]. @@ -520,9 +565,10 @@ and typing_app statefull h op e_list = let typed_e2, t1 = typing statefull h e2 in let typed_e3 = expect statefull h t1 e3 in t1, op, [typed_e1; typed_e2; typed_e3] - | Ecall ( { op_name = f; op_params = params } as op_desc , reset), e_list -> + | Ecall ( { op_name = f; op_params = params; op_kind = k } as op_desc + , reset), e_list -> let { qualid = q; info = ty_desc } = find_value f in - let expected_ty_list, result_ty_list = kind f statefull ty_desc in + let k, expected_ty_list, result_ty_list = kind f statefull k ty_desc in let m = List.combine (List.map (fun p -> p.p_name) ty_desc.node_params) params in let expected_ty_list = List.map (subst_type_vars m) expected_ty_list in @@ -532,7 +578,7 @@ and typing_app statefull h op e_list = let result_ty_list = List.map (subst_type_vars m) result_ty_list in List.iter add_size_constr size_constrs; (prod result_ty_list, - Ecall ( { op_desc with op_name = Modname(q) }, reset), + Ecall ( { op_desc with op_name = Modname q; op_kind = k }, reset), typed_e_list) | Earray_op op, e_list -> let ty, op, e_list = typing_array_op statefull h op e_list in @@ -596,11 +642,12 @@ and typing_array_op statefull h op e_list = end; let n = SOp (SPlus, size_exp t1, size_exp t2) in Tarray (element_type t1, n), op, [typed_e1; typed_e2] - | Eiterator (it, ({ op_name = f; op_params = params } as op_desc), reset), + | Eiterator (it, ({ op_name = f; op_params = params; + op_kind = k } as op_desc), reset), e::e_list -> let { qualid = q; info = ty_desc } = find_value f in let f = Modname(q) in - let expected_ty_list, result_ty_list = kind f statefull ty_desc in + let k, expected_ty_list, result_ty_list = kind f statefull k ty_desc in let m = List.combine (List.map (fun p -> p.p_name) ty_desc.node_params) params in let expected_ty_list = List.map (subst_type_vars m) expected_ty_list in @@ -613,7 +660,7 @@ and typing_array_op statefull h op e_list = expected_ty_list result_ty_list e_list in add_size_constr (LEqual (SConst 1, e)); List.iter add_size_constr size_constrs; - ty, Eiterator(it, { op_desc with op_name = f }, reset), + ty, Eiterator(it, { op_desc with op_name = f; op_kind = k }, reset), typed_e::typed_e_list (*Arity problems*) @@ -740,7 +787,7 @@ let rec typing_eq statefull h acc eq = Eeq(pat, typed_e), acc in { eq with - eq_statefull = statefull; + eq_statefull = is_statefull_eq_desc typed_desc; eq_desc = typed_desc }, acc @@ -831,7 +878,7 @@ and typing_block statefull h typing_eq_list statefull h0 Env.empty eq_list in let defnames = diff_env defined_names local_names in { b with - b_statefull = statefull; + b_statefull = List.exists (fun eq -> eq.eq_statefull) typed_eq_list; b_defnames = defnames; b_local = typed_l; b_equs = typed_eq_list }, @@ -895,12 +942,13 @@ let typing_contract statefull h contract = c_enforce = typed_e_g }, controllable_names, h -let signature const_env inputs returns params constraints = +let signature const_env statefull inputs returns params constraints = let arg_dec_of_var_dec vd = mk_arg (Some (name vd.v_ident)) (check_type vd.v_type) in { node_inputs = List.map arg_dec_of_var_dec inputs; node_outputs = List.map arg_dec_of_var_dec returns; + node_statefull = statefull; node_params = params; node_params_constraints = constraints; } @@ -910,7 +958,7 @@ let solve loc env cl = with Solve_failed c -> message loc (Econstraint_solve_failed c) -let node const_env ({ n_name = f; +let node const_env ({ n_name = f; n_statefull = statefull; n_input = i_list; n_output = o_list; n_contract = contract; n_local = l_list; n_equs = eq_list; n_loc = loc; @@ -921,11 +969,11 @@ let node const_env ({ n_name = f; (* typing contract *) let typed_contract, controllable_names, h = - typing_contract false h contract in + typing_contract statefull h contract in let typed_l_list, local_names, h = build h h l_list in let typed_eq_list, defined_names = - typing_eq_list false h Env.empty eq_list in + typing_eq_list statefull h Env.empty eq_list in (* if not (statefull) & (List.length o_list <> 1) then error (Etoo_many_outputs);*) let expected_names = add local_names output_names in @@ -934,7 +982,7 @@ let node const_env ({ n_name = f; let cl = get_size_constr () in let cl = solve loc const_env cl in - add_value f (signature const_env i_list o_list node_params cl); + add_value f (signature const_env statefull i_list o_list node_params cl); { n with n_input = List.rev typed_i_list; diff --git a/compiler/heptagon/heptagon.ml b/compiler/heptagon/heptagon.ml index 4ce5bd5..5a696fb 100644 --- a/compiler/heptagon/heptagon.ml +++ b/compiler/heptagon/heptagon.ml @@ -58,7 +58,7 @@ and array_op = [exp option] reset *) and op_desc = { op_name : longname; op_params: size_exp list; op_kind: op_kind } -and op_kind = | Eop | Enode +and op_kind = | Efun | Enode and const = | Cint of int @@ -138,7 +138,7 @@ type program = { } type signature = { - sig_name : name; sig_inputs : arg list; + sig_name : name; sig_inputs : arg list; sig_statefull : bool; sig_outputs : arg list; sig_params : param list } @@ -190,7 +190,7 @@ let mk_switch_equation ?(statefull = true) e l = (** @return a size exp operator from a Heptagon operator. *) let op_from_app app = match app.a_op with - | Ecall ( { op_name = op; op_kind = Eop }, _) -> op_from_app_name op + | Ecall ( { op_name = op; op_kind = Efun }, _) -> op_from_app_name op | _ -> raise Not_static (** Translates a Heptagon exp into a static size exp. *) diff --git a/compiler/heptagon/parsing/hept_parser.mly b/compiler/heptagon/parsing/hept_parser.mly index 562502a..b0b8677 100644 --- a/compiler/heptagon/parsing/hept_parser.mly +++ b/compiler/heptagon/parsing/hept_parser.mly @@ -554,6 +554,7 @@ interface_decl: RETURNS LPAREN params_signature RPAREN { mk_interface_decl (Isignature({ sig_name = $3; sig_inputs = $6; + sig_statefull = $2; sig_outputs = $10; sig_params = $4; })) } ; diff --git a/compiler/heptagon/parsing/parsetree.ml b/compiler/heptagon/parsing/parsetree.ml index a799d4c..06bbf65 100644 --- a/compiler/heptagon/parsing/parsetree.ml +++ b/compiler/heptagon/parsing/parsetree.ml @@ -54,7 +54,7 @@ and array_op = | Eiterator of iterator_type * op_desc and op_desc = { op_name : longname; op_params: exp list; op_kind: op_kind } -and op_kind = | Eop | Enode +and op_kind = | Efun | Enode and const = | Cint of int @@ -155,6 +155,7 @@ type arg = { a_type : ty; a_name : name option } type signature = { sig_name : name; sig_inputs : arg list; + sig_statefull : bool; sig_outputs : arg list; sig_params : name list; } @@ -183,7 +184,7 @@ let mk_call desc exps = Eapp (mk_app (Ecall desc), exps) let mk_op_call s params exps = - mk_call (mk_op_desc (Name s) params Eop) exps + mk_call (mk_op_desc (Name s) params Efun) exps let mk_array_op_call op exps = Eapp (mk_app (Earray_op op), exps) diff --git a/compiler/heptagon/parsing/scoping.ml b/compiler/heptagon/parsing/scoping.ml index 0ad88f4..519ebcb 100644 --- a/compiler/heptagon/parsing/scoping.ml +++ b/compiler/heptagon/parsing/scoping.ml @@ -100,7 +100,7 @@ let translate_iterator_type = function | Imapfold -> Heptagon.Imapfold let translate_op_kind = function - | Eop -> Heptagon.Eop + | Efun -> Heptagon.Efun | Enode -> Heptagon.Enode let translate_const = function @@ -110,7 +110,7 @@ let translate_const = function let op_from_app loc app = match app.a_op with - | Ecall { op_name = op; op_kind = Eop } -> op_from_app_name op + | Ecall { op_name = op; op_kind = Efun } -> op_from_app_name op | _ -> Error.message loc Error.Estatic_exp_expected let check_const_vars = ref true @@ -329,6 +329,7 @@ let translate_signature s = { Heptagon.sig_name = s.sig_name; Heptagon.sig_inputs = List.map (translate_arg const_env) s.sig_inputs; Heptagon.sig_outputs = List.map (translate_arg const_env) s.sig_outputs; + Heptagon.sig_statefull = s.sig_statefull; Heptagon.sig_params = List.map Signature.mk_param s.sig_params; } let translate_interface_desc const_env = function diff --git a/compiler/heptagon/transformations/reset.ml b/compiler/heptagon/transformations/reset.ml index b1849c7..0418f03 100644 --- a/compiler/heptagon/transformations/reset.ml +++ b/compiler/heptagon/transformations/reset.ml @@ -46,7 +46,7 @@ let mk_bool_var n = let mk_bool_param n = mk_var_dec n (Tid Initial.pbool) -let or_op_call = mk_op ( Ecall(mk_op_desc Initial.por [] Eop, None) ) +let or_op_call = mk_op ( Ecall(mk_op_desc Initial.por [] Efun, None) ) let pre_true e = { e with e_desc = Eapp(mk_op (Epre (Some (Cconstr Initial.ptrue))), [e]) @@ -230,7 +230,7 @@ and translate res e = (* create a new reset exp if necessary *) | Eapp({ a_op = Ecall(op_desc, None) } as op, e_list) -> let e_list = List.map (translate res) e_list in - if true_reset res & op_desc.op_kind <> Eop then + if true_reset res & op_desc.op_kind = Enode then let op = { op with a_op = Ecall(op_desc, Some (exp_of_res res)) } in { e with e_desc = Eapp(op, e_list) } else diff --git a/compiler/main/hept2mls.ml b/compiler/main/hept2mls.ml index 5c2ea59..09cbb93 100644 --- a/compiler/main/hept2mls.ml +++ b/compiler/main/hept2mls.ml @@ -189,7 +189,7 @@ let rec const = function | Heptagon.Carray(n, c) -> Carray(n, const c) let translate_op_kind = function - | Heptagon.Eop -> Eop + | Heptagon.Efun -> Efun | Heptagon.Enode -> Enode let translate_op_desc { Heptagon.op_name = n; Heptagon.op_params = p; diff --git a/compiler/minils/analysis/init.ml b/compiler/minils/analysis/init.ml index c0789df..deecd2f 100644 --- a/compiler/minils/analysis/init.ml +++ b/compiler/minils/analysis/init.ml @@ -214,7 +214,7 @@ let rec typing h e = | Etuple e_list -> product (List.map (typing h) e_list) (*TODO traitement singulier et empêche reset d'un 'op'*) - | Ecall (op, e_list, None) when op.op_kind = Eop -> + | Ecall (op, e_list, None) when op.op_kind = Efun -> let i = List.fold_left (fun acc e -> itype (typing h e)) izero e_list in skeleton i e.e_ty | Ecall (op, e_list, reset) when op.op_kind = Enode -> diff --git a/compiler/minils/minils.ml b/compiler/minils/minils.ml index 9c41acd..6d3b027 100644 --- a/compiler/minils/minils.ml +++ b/compiler/minils/minils.ml @@ -73,7 +73,7 @@ and array_op = optional reset condition *) and op_desc = { op_name: longname; op_params: size_exp list; op_kind: op_kind } -and op_kind = | Eop | Enode +and op_kind = | Efun | Enode and ct = | Ck of ck diff --git a/compiler/minils/mls_utils.ml b/compiler/minils/mls_utils.ml index 23a95fb..1a54c2b 100644 --- a/compiler/minils/mls_utils.ml +++ b/compiler/minils/mls_utils.ml @@ -53,6 +53,9 @@ let is_record_type ty = match ty with Not_found -> false) | _ -> false +let is_op = function + | Modname { qual = "Pervasives"; id = _ } -> true | _ -> false + module Vars = struct let add x acc = diff --git a/compiler/minils/parsing/mls_parser.mly b/compiler/minils/parsing/mls_parser.mly index 498b9da..f02540b 100644 --- a/compiler/minils/parsing/mls_parser.mly +++ b/compiler/minils/parsing/mls_parser.mly @@ -170,9 +170,9 @@ exp: | PRE exp { mk_exp (Efby(None,$2)) } | op=node_app a=exps r=reset { mk_exp (Ecall(op, a, r)) } | e1=exp i_op=infix e2=exp - { mk_exp (Ecall(mk_op ~op_kind:Eop i_op, [e1; e2], None)) } + { mk_exp (Ecall(mk_op ~op_kind:Efun i_op, [e1; e2], None)) } | p_op=prefix e=exp %prec prefixs - { mk_exp (Ecall(mk_op ~op_kind:Eop p_op, [e], None)) } + { mk_exp (Ecall(mk_op ~op_kind:Efun p_op, [e], None)) } | IF e1=exp THEN e2=exp ELSE e3=exp { mk_exp (Eifthenelse(e1, e2, e3)) } | e=simple_exp DOT m=longname { mk_exp (Efield(e, m)) } diff --git a/compiler/minils/sequential/mls2obc.ml b/compiler/minils/sequential/mls2obc.ml index 4d32fe3..506e411 100644 --- a/compiler/minils/sequential/mls2obc.ml +++ b/compiler/minils/sequential/mls2obc.ml @@ -25,9 +25,6 @@ let encode_longname_params n params = match n with | Modname { qual = qual; id = id } -> Modname { qual = qual; id = encode_name_params id params; } -let is_op = function - | Modname { qual = "Pervasives"; id = _ } -> true | _ -> false - let op_from_string op = Modname { qual = "Pervasives"; id = op; } let rec lhs_of_idx_list e = function @@ -82,8 +79,8 @@ let rec translate const_env map (m, si, j, s) | Minils.Econst v -> Const (translate_const const_env v) | Minils.Evar n -> Lhs (var_from_name map n) | Minils.Econstvar n -> Const (Cint (int_of_size_exp const_env (SVar n))) - | Minils.Ecall ({ Minils.op_name = n; Minils.op_kind = Minils.Eop }, - e_list, _) -> + | Minils.Ecall ({ Minils.op_name = n; Minils.op_kind = Minils.Efun }, + e_list, _) when Mls_utils.is_op n -> Op (n, List.map (translate const_env map (m, si, j, s)) e_list) | Minils.Ewhen (e, _, _) -> translate const_env map (m, si, j, s) e | Minils.Efield (e, field) -> @@ -153,22 +150,26 @@ let rec translate_eq const_env map { Minils.eq_lhs = pat; Minils.eq_rhs = e } m, si, j, (control map ck action) :: s | pat, Minils.Ecall ({ Minils.op_name = n; Minils.op_params = params; - Minils.op_kind = Minils.Enode }, + Minils.op_kind = (Minils.Enode + | Minils.Efun) as op_kind }, e_list, r) -> let name_list = translate_pat map pat in let c_list = List.map (translate const_env map (m, si, j, s)) e_list in let o = gen_symbol () in - let si = (Reinit o) :: si in + let si = + (match op_kind with + | Minils.Enode -> (Reinit o) :: si + | Minils.Efun -> si) in let params = List.map (int_of_size_exp const_env) params in let j = (o, (encode_longname_params n params), 1) :: j in let action = Step_ap (name_list, Context o, c_list) in - let s = (match r with - | None -> (control map ck action) :: s - | Some r -> + let s = (match r, op_kind with + | Some r, Minils.Enode -> let ra = control map (Minils.Con (ck, Name "true", r)) (Reinit o) in - ra :: (control map ck action) :: s ) in + ra :: (control map ck action) :: s + | _, _ -> (control map ck action) :: s) in m, si, j, s | Minils.Etuplepat p_list, Minils.Etuple act_list -> @@ -277,7 +278,7 @@ let rec translate_eq const_env map { Minils.eq_lhs = pat; Minils.eq_rhs = e } let n = int_of_size_exp const_env n in let si = (match k with - | Minils.Eop -> si + | Minils.Efun -> si | Minils.Enode -> (Reinit o) :: si) in let params = List.map (int_of_size_exp const_env) params in let j = (o, (encode_longname_params f params), n) :: j in diff --git a/compiler/minils/transformations/callgraph.ml b/compiler/minils/transformations/callgraph.ml index a9975c1..b89c206 100644 --- a/compiler/minils/transformations/callgraph.ml +++ b/compiler/minils/transformations/callgraph.ml @@ -53,10 +53,8 @@ let rec collect_exp nodes env e = | Efield_update(_, e1, e2) -> collect_exp nodes env e1; collect_exp nodes env e2 - (* Do the real work: call node *) - | Ecall( { op_name = ln; op_params = params; op_kind = Eop }, e_list, _) -> - List.iter (collect_exp nodes env) e_list - | Ecall( { op_name = ln; op_params = params; op_kind = Enode }, + (* Do the real work: call node *) + | Ecall( { op_name = ln; op_params = params; op_kind = _ }, e_list, _) -> List.iter (collect_exp nodes env) e_list; let params = List.map (int_of_size_exp env) params in diff --git a/compiler/minils/transformations/normalize.ml b/compiler/minils/transformations/normalize.ml index 6280d0d..392ec26 100644 --- a/compiler/minils/transformations/normalize.ml +++ b/compiler/minils/transformations/normalize.ml @@ -114,7 +114,8 @@ let add context expected_kind ({ e_desc = de } as e) = let up = match de, expected_kind with | (Evar _ | Efield _ ) , VRef -> false | _ , VRef -> true - | Ecall ({ op_kind = Eop }, _, _), (Exp|Act) -> false + | Ecall ({ op_kind = Efun; op_name = n }, _, _), + (Exp|Act) when is_op n -> false | ( Emerge _ | Etuple _ | Ecall _ | Efby _ | Earray_op _ ), Exp -> true | ( Ecall _ | Efby _ ), Act -> true