diff --git a/compiler/heptagon/analysis/causality.ml b/compiler/heptagon/analysis/causality.ml index b06c90c..0b137af 100644 --- a/compiler/heptagon/analysis/causality.ml +++ b/compiler/heptagon/analysis/causality.ml @@ -147,7 +147,7 @@ and apply op e_list = let i3 = typing e3 in cseq t1 (cor i2 i3) | ( Efun _| Enode _ | Econcat | Eselect_slice - | Eselect_dyn | Eselect_trunc | Eselect | Earray_fill) -> + | Eselect_dyn | Eselect_trunc | Eselect | Earray_fill | Ereinit) -> ctuplelist (List.map typing e_list) | (Earray | Etuple) -> candlist (List.map typing e_list) diff --git a/compiler/heptagon/analysis/hept_clocking.ml b/compiler/heptagon/analysis/hept_clocking.ml index 1d26c47..b9f0bfc 100644 --- a/compiler/heptagon/analysis/hept_clocking.ml +++ b/compiler/heptagon/analysis/hept_clocking.ml @@ -165,7 +165,7 @@ and typing_app h base pat op e_list = match op with | 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 -> + | Eselect_slice | Econcat | Earray | Efield | Efield_update | Eifthenelse | Ereinit -> List.iter (expect h pat (Ck base)) e_list; Ck base | Enode f -> diff --git a/compiler/heptagon/analysis/linear_typing.ml b/compiler/heptagon/analysis/linear_typing.ml index 6a4711b..fdc5062 100644 --- a/compiler/heptagon/analysis/linear_typing.ml +++ b/compiler/heptagon/analysis/linear_typing.ml @@ -558,7 +558,7 @@ and typing_app env op e_list = match op with let env = safe_expect env Ltop e in Ltop, env | Eifthenelse | Efun _ | Enode _ | Etuple - | Eupdate | Efield_update -> assert false (*already done in expect_app*) + | Eupdate | Efield_update | Ereinit -> assert false (*already done in expect_app*) (** Check that the application of op to e_list can have the linearity expected_lin. *) @@ -610,6 +610,11 @@ and expect_app env expected_lin op e_list = match op with let env = List.fold_left (fun env -> safe_expect env Ltop) env idx in expect env expected_lin e1 + | Ereinit -> + let e1, e2 = assert_2 e_list in + let env = safe_expect env Ltop e2 in + expect env expected_lin e1 + | _ -> let actual_lin, env = typing_app env op e_list in unify_lin expected_lin actual_lin, env diff --git a/compiler/heptagon/analysis/typing.ml b/compiler/heptagon/analysis/typing.ml index 836d0d5..99363df 100644 --- a/compiler/heptagon/analysis/typing.ml +++ b/compiler/heptagon/analysis/typing.ml @@ -847,7 +847,11 @@ and typing_app cenv h app e_list = mk_static_int_op (mk_pervasives "+") [array_size t1; array_size t2] in Tarray (element_type t1, n), app, [typed_e1; typed_e2] - + | Ereinit -> + let e1, e2 = assert_2 e_list in + let typed_e1, ty = typing cenv h e1 in + let typed_e2 = expect cenv h ty e2 in + ty, app, [typed_e1; typed_e2] and typing_iterator cenv h it n_list args_ty_list result_ty_list e_list = diff --git a/compiler/heptagon/hept_printer.ml b/compiler/heptagon/hept_printer.ml index 596e4d0..6688901 100644 --- a/compiler/heptagon/hept_printer.ml +++ b/compiler/heptagon/hept_printer.ml @@ -216,6 +216,8 @@ and print_app ff (app, args) = | Earrow -> let e1, e2 = assert_2 args in fprintf ff "@[<2>%a ->@ %a@]" print_exp e1 print_exp e2 + | Ereinit -> + fprintf ff "@[split@,%a@]" print_exp_tuple args let rec print_eq ff eq = match eq.eq_desc with diff --git a/compiler/heptagon/heptagon.ml b/compiler/heptagon/heptagon.ml index 63f8b26..7bdcf5e 100644 --- a/compiler/heptagon/heptagon.ml +++ b/compiler/heptagon/heptagon.ml @@ -74,6 +74,7 @@ and op = | Eselect_slice | Eupdate | Econcat + | Ereinit and pat = | Etuplepat of pat list diff --git a/compiler/heptagon/parsing/hept_lexer.mll b/compiler/heptagon/parsing/hept_lexer.mll index 0db23a9..292034e 100644 --- a/compiler/heptagon/parsing/hept_lexer.mll +++ b/compiler/heptagon/parsing/hept_lexer.mll @@ -67,6 +67,7 @@ List.iter (fun (str,tok) -> Hashtbl.add keyword_table str tok) [ "at", AT; "init", INIT; "split", SPLIT; + "reinit", REINIT; "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 1610983..517e1df 100644 --- a/compiler/heptagon/parsing/hept_parser.mly +++ b/compiler/heptagon/parsing/hept_parser.mly @@ -49,7 +49,7 @@ open Hept_parsetree %token AROBASE %token DOUBLE_LESS DOUBLE_GREATER %token MAP MAPI FOLD FOLDI MAPFOLD -%token AT INIT SPLIT +%token AT INIT SPLIT REINIT %token PREFIX %token INFIX0 %token INFIX1 @@ -479,6 +479,8 @@ _exp: { Eapp(n, args) } | SPLIT n=ident LPAREN e=exp RPAREN { Esplit(n, e) } + | REINIT LPAREN e1=exp COMMA e2=exp RPAREN + { mk_call Ereinit [e1; e2] } | NOT exp { mk_op_call "not" [$2] } | exp INFIX4 exp diff --git a/compiler/heptagon/parsing/hept_parsetree.ml b/compiler/heptagon/parsing/hept_parsetree.ml index 3f18ea0..cef9123 100644 --- a/compiler/heptagon/parsing/hept_parsetree.ml +++ b/compiler/heptagon/parsing/hept_parsetree.ml @@ -105,6 +105,7 @@ and op = | Eselect_slice | Eupdate | Econcat + | Ereinit and pat = | Etuplepat of pat list diff --git a/compiler/heptagon/parsing/hept_scoping.ml b/compiler/heptagon/parsing/hept_scoping.ml index 9a69c72..9918232 100644 --- a/compiler/heptagon/parsing/hept_scoping.ml +++ b/compiler/heptagon/parsing/hept_scoping.ml @@ -339,6 +339,7 @@ and translate_op = function | Eselect_trunc -> Heptagon.Eselect_trunc | Efun ln -> Heptagon.Efun (qualify_value ln) | Enode ln -> Heptagon.Enode (qualify_value ln) + | Ereinit -> Heptagon.Ereinit and translate_pat loc env = function | Evarpat x -> Heptagon.Evarpat (Rename.var loc env x) diff --git a/compiler/heptagon/transformations/normalize.ml b/compiler/heptagon/transformations/normalize.ml index 913fe6c..936fff0 100644 --- a/compiler/heptagon/transformations/normalize.ml +++ b/compiler/heptagon/transformations/normalize.ml @@ -106,8 +106,8 @@ let add context expected_kind e = let up = match e.e_desc, expected_kind with (* static arrays should be normalized to simplify code generation *) | Econst { se_desc = Sarray _ }, ExtValue -> true - | (Evar _ | Eapp ({ a_op = Efield }, _, _) | Ewhen _ - | Eapp ({ a_op = Etuple }, _, _) | Econst _) , ExtValue -> false + | (Evar _ | Eapp ({ a_op = Efield | Etuple | Ereinit }, _, _) | Ewhen _ + | Econst _) , ExtValue -> false | _ , ExtValue -> true | _ -> false in if up then diff --git a/compiler/main/hept2mls.ml b/compiler/main/hept2mls.ml index 10475ba..2e57fab 100644 --- a/compiler/main/hept2mls.ml +++ b/compiler/main/hept2mls.ml @@ -80,6 +80,7 @@ let rec translate_op = function | Heptagon.Earray -> Earray | Heptagon.Etuple -> Misc.internal_error "hept2mls Etuple" | Heptagon.Earrow -> assert false + | Heptagon.Ereinit -> assert false let translate_app app = mk_app ~params:app.Heptagon.a_params @@ -102,6 +103,9 @@ let rec translate_extvalue e = let f = assert_1 params in let fn = match f.se_desc with Sfield fn -> fn | _ -> assert false in mk_extvalue (Wfield (translate_extvalue e, fn)) + | Heptagon.Eapp({ Heptagon.a_op = Heptagon.Ereinit }, e_list, _) -> + let e1, e2 = assert_2 e_list in + mk_extvalue (Wreinit (translate_extvalue e1, translate_extvalue e2)) | _ -> Error.message e.Heptagon.e_loc Error.Enormalization let rec translate ({ Heptagon.e_desc = desc; Heptagon.e_ty = ty; @@ -110,7 +114,7 @@ let rec translate ({ Heptagon.e_desc = desc; Heptagon.e_ty = ty; let desc = match desc with | Heptagon.Econst _ | Heptagon.Evar _ - | Heptagon.Eapp({ Heptagon.a_op = Heptagon.Efield }, _, _) -> + | Heptagon.Eapp({ Heptagon.a_op = Heptagon.Efield | Heptagon.Ereinit }, _, _) -> let w = translate_extvalue e in Eextvalue w | Heptagon.Ewhen (e,c,x) -> Ewhen (translate e, c, x) diff --git a/compiler/main/mls2obc.ml b/compiler/main/mls2obc.ml index a6676af..a8bde6d 100644 --- a/compiler/main/mls2obc.ml +++ b/compiler/main/mls2obc.ml @@ -226,7 +226,7 @@ let rec translate_extvalue map w = match w.Minils.w_desc with | Minils.Wconst v -> Wconst v | Minils.Wvar x -> assert false | Minils.Wfield (w1, f) -> Wfield (translate_extvalue map w1, f) - | Minils.Wwhen (w1, c, x) -> (translate_extvalue map w1).w_desc + | Minils.Wwhen (w1, _, _) | Minils.Wreinit(_, w1) -> (translate_extvalue map w1).w_desc in mk_ext_value w.Minils.w_ty desc diff --git a/compiler/minils/analysis/clocking.ml b/compiler/minils/analysis/clocking.ml index 916a0e7..40d76fe 100644 --- a/compiler/minils/analysis/clocking.ml +++ b/compiler/minils/analysis/clocking.ml @@ -67,6 +67,11 @@ let rec typing_extvalue h w = Con (ck_n, c, n) | Wfield (w1, _) -> typing_extvalue h w1 + | Wreinit (w1, w2) -> + let t1 = typing_extvalue h w1 in + let t2 = typing_extvalue h w2 in + unify_ck t1 t2; + t1 in w.w_ck <- ck; ck diff --git a/compiler/minils/analysis/interference.ml b/compiler/minils/analysis/interference.ml index 171f86c..1adca56 100644 --- a/compiler/minils/analysis/interference.ml +++ b/compiler/minils/analysis/interference.ml @@ -48,6 +48,7 @@ module InterfRead = struct | Wfield(w, f) -> Ifield (ivar_of_extvalue w, f) | Wwhen(w, _, _) -> ivar_of_extvalue w | Wconst _ -> raise Const_extvalue + | Wreinit (_, w) -> ivar_of_extvalue w let ivar_of_pat p = match p with | Evarpat x -> Ivar x diff --git a/compiler/minils/minils.ml b/compiler/minils/minils.ml index 1956827..eebd121 100644 --- a/compiler/minils/minils.ml +++ b/compiler/minils/minils.ml @@ -52,6 +52,7 @@ and extvalue_desc = | Wvar of var_ident | Wfield of extvalue * field_name | Wwhen of extvalue * constructor_name * var_ident (** extvalue when Constructor(ident) *) + | Wreinit of extvalue * extvalue and exp = { e_desc : edesc; @@ -100,7 +101,6 @@ and op = | Eupdate (** [ arg1 with arg3..arg_n = arg2 ] *) | Econcat (** arg1@@arg2 *) - type pat = | Etuplepat of pat list | Evarpat of var_ident diff --git a/compiler/minils/mls_compare.ml b/compiler/minils/mls_compare.ml index f290cf0..05330f1 100644 --- a/compiler/minils/mls_compare.ml +++ b/compiler/minils/mls_compare.ml @@ -38,6 +38,9 @@ struct | Wfield (w1, f1), Wfield(w2, f2) -> let cr = compare f1 f2 in if cr <> 0 then cr else extvalue_compare w1 w2 + | Wreinit (w1, ww1), Wreinit (w2, ww2) -> + let cr = extvalue_compare w1 w2 in + if cr <> 0 then cr else extvalue_compare ww1 ww2 | Wconst _, _ -> 1 @@ -47,7 +50,10 @@ struct | Wwhen _, (Wconst _ | Wvar _) -> -1 | Wwhen _, _ -> 1 - | Wfield _, _ -> -1 + | Wfield _, (Wconst _ | Wvar _ | Wwhen _) -> -1 + | Wfield _, Wreinit _ -> 1 + + | Wreinit _, _ -> -1 let rec exp_compare e1 e2 = let cr = Global_compare.type_compare e1.e_ty e2.e_ty in diff --git a/compiler/minils/mls_mapfold.ml b/compiler/minils/mls_mapfold.ml index fb10147..896c378 100644 --- a/compiler/minils/mls_mapfold.ml +++ b/compiler/minils/mls_mapfold.ml @@ -63,6 +63,10 @@ and extvalue_desc funs acc wd = match wd with | Wwhen (w, c, v) -> let w, acc = extvalue_it funs acc w in Wwhen (w,c,v), acc + | Wreinit (w1, w2) -> + let w1, acc = extvalue_it funs acc w1 in + let w2, acc = extvalue_it funs acc w2 in + Wreinit (w1, w2), acc and edesc_it funs acc ed = try funs.edesc funs acc ed diff --git a/compiler/minils/mls_printer.ml b/compiler/minils/mls_printer.ml index cc44fdc..f9e0225 100644 --- a/compiler/minils/mls_printer.ml +++ b/compiler/minils/mls_printer.ml @@ -32,7 +32,7 @@ let rec print_pat ff = function let print_vd ff { v_ident = n; v_type = ty; v_linearity = lin; v_clock = ck } = 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%a" print_ident n print_type ty print_linearity lin let print_local_vars ff = function | [] -> () @@ -94,6 +94,8 @@ and print_extvalue_desc ff = function | Wfield (w,f) -> fprintf ff "%a.%a" print_extvalue w print_qualname f | Wwhen (w, c, n) -> fprintf ff "@[<2>(%a@ when %a(%a))@]" print_extvalue w print_qualname c print_ident n + | Wreinit (w1, w2) -> + fprintf ff "@[reinit@,(%a, %a)@]" print_extvalue w1 print_extvalue w2 and print_exp_desc ff = function | Eextvalue w -> print_extvalue ff w diff --git a/compiler/minils/sigali/sigalimain.ml b/compiler/minils/sigali/sigalimain.ml index c01390c..3c4a76b 100644 --- a/compiler/minils/sigali/sigalimain.ml +++ b/compiler/minils/sigali/sigalimain.ml @@ -44,7 +44,7 @@ let translate_static_exp se = | 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") @@ -77,7 +77,7 @@ let rec translate_ext prefix ({ Minils.w_desc = desc; Minils.w_ty = ty } as e) = | 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) -> + | 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 @@ -88,6 +88,7 @@ let rec translate_ext prefix ({ Minils.w_desc = desc; Minils.w_ty = ty } as e) = translate_ext prefix e | Minils.Wfield(_) -> failwith("Sigali: structures not implemented") + | Minils.Wreinit _ -> failwith("Sigali: reinit not implemented") (* [translate e = c] *) let rec translate prefix ({ Minils.e_desc = desc; Minils.e_ty = ty } as e) = @@ -114,7 +115,7 @@ let rec translate prefix ({ Minils.e_desc = desc; Minils.e_ty = ty } as e) = let e1 = translate_ext prefix e1 in let sig_e = begin match e2.Minils.w_desc with - | Minils.Wconst({se_desc = Sint(v)}) -> + | Minils.Wconst({se_desc = Sint(v)}) -> op e1 (Sconst(Cint(v+modv))) | _ -> let e2 = translate_ext prefix e2 in @@ -129,11 +130,11 @@ let rec translate prefix ({ Minils.e_desc = desc; Minils.e_ty = ty } as e) = (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) -> + | 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 @@ -175,7 +176,7 @@ let rec translate prefix ({ Minils.e_desc = desc; Minils.e_ty = ty } as e) = failwith("Sigali: node in expressions; programs should be normalized") | Minils.Efby(_,_) -> failwith("Sigali: fby in expressions; programs should be normalized") - | Minils.Eapp(_,_,_) -> + | Minils.Eapp(_,_,_) -> Format.printf "Application : %a@\n" Mls_printer.print_exp e; failwith("Sigali: not supported application") @@ -183,12 +184,12 @@ let rec translate prefix ({ Minils.e_desc = desc; Minils.e_ty = ty } as e) = 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 } = - + { 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) -> @@ -198,13 +199,13 @@ let rec translate_eq env f (* (extend *) (* constraints *) (* (Slist[Sequal(Ssquare(Svar(sn)),Sconst(Ctrue))]))::acc_eqs in *) - let acc_eqs,acc_init = - match opt_c with + let acc_eqs,acc_init = + match opt_c with | None -> acc_eqs,Cfalse::acc_init - | Some(c) -> + | Some(c) -> let c = translate_static_exp c in - (extend - initialisations + (extend + initialisations (Slist[Sequal(Svar(sn),Sconst(c))]))::acc_eqs, c::acc_init in @@ -213,7 +214,7 @@ let rec translate_eq env f acc_dep, sn::acc_states, acc_init,acc_inputs,acc_ctrl,acc_cont, - (extend + (extend evolutions (Slist[Sdefault(e_next,Svar(sn))])) (* TODO *) @@ -225,7 +226,7 @@ let rec translate_eq env f 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] @@ -235,13 +236,13 @@ let rec translate_eq env f 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) @@ -282,22 +283,22 @@ let rec translate_eq env f let s_prefix = "S_" ^ (string_of_int id_length) ^ "_" ^ a_id ^ "_" in let new_states_list = List.map - (fun g_state -> + (fun g_state -> (* Remove "g_" prefix *) let l = String.length g in let s = - String.sub + 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 = + let e_outputs,acc_inputs = match inlined with | true -> [],acc_inputs - | false -> - let new_outputs = + | 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 @@ -333,24 +334,24 @@ let rec translate_eq env f ::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)) + (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) + (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) + (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) *) @@ -358,7 +359,7 @@ let rec translate_eq env f match inlined with | true -> List.fold_left2 - (fun acc_eqs o go -> + (fun acc_eqs o go -> {stmt_name = prefixed o; stmt_def = subst (Svar(go)) (Svar(var_g)) (Svar(var_inst_g))} ::acc_eqs) @@ -385,7 +386,7 @@ let rec translate_eq env f (* 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] @@ -395,19 +396,19 @@ let rec translate_eq env f 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) ... @@ -442,22 +443,22 @@ let rec translate_eq env f let s_prefix = "S_" ^ (string_of_int id_length) ^ "_" ^ a_id ^ "_" in let new_states_list = List.map - (fun g_state -> + (fun g_state -> (* Remove "g_" prefix *) let l = (String.length g) in let s = - String.sub + 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 = + let e_outputs,acc_inputs = match inlined with | true -> [],acc_inputs - | false -> - let new_outputs = + | 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 @@ -494,24 +495,24 @@ let rec translate_eq env f ::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)) + (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) + (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) + (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) *) @@ -519,7 +520,7 @@ let rec translate_eq env f match inlined with | true -> List.fold_left2 - (fun acc_eqs o go -> + (fun acc_eqs o go -> {stmt_name = prefixed o; stmt_def = subst (Svar(go)) (Svar(var_g)) (Svar(var_inst_g))} ::acc_eqs) @@ -543,9 +544,9 @@ let rec translate_eq env f | Minils.Evarpat(n), _ -> (* assert : no fby, no node application in e *) let e' = translate prefix e in - let e' = + let e' = begin match (actual_ty e.Minils.e_ty) with - | Tbool -> translate_ck prefix e' ck + | Tbool -> translate_ck prefix e' ck | _ -> e' end in acc_dep,acc_states,acc_init, @@ -553,36 +554,36 @@ let rec translate_eq env f { stmt_name = prefixed (name n); stmt_def = e' }::acc_eqs | _ -> assert false - + let translate_eq_list env f eq_list = - List.fold_left + List.fold_left (fun (acc_dep,acc_states,acc_init, - acc_inputs,acc_ctrl,acc_cont,acc_eqs) eq -> - translate_eq + 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) + acc_inputs,acc_ctrl,acc_cont,acc_eqs) eq) ([],[],[],[],[],[],[]) eq_list -let translate_contract env f contract = +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 = + | 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; + | 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 = + controllables,_contracts,body = translate_eq_list env f l_eqs in assert (inputs = []); assert (controllables = []); @@ -592,17 +593,17 @@ let translate_contract env f contract = {stmt_name = var_g; stmt_def = e_g} :: {stmt_name = var_a; stmt_def = e_a} :: body in - let controllables = + 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 -> + | (a,g)::l -> let conts,assumes = build_environment l in ((a =>~ g) :: conts),(g &~ assumes) @@ -618,9 +619,9 @@ let translate_node env 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 = + 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 = + 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 @@ -628,11 +629,11 @@ let translate_node env let states = List.rev states in let body_c = List.rev body_c in let states_c = List.rev states_c in - let constraints = + let constraints = List.map (fun v -> Sequal(Ssquare(Svar(v)),Sconst(Ctrue))) (inputs@controllables) in - let contracts_components,assumes_components = + let contracts_components,assumes_components = build_environment contracts in let constraints = constraints @ contracts_components @ [Sequal (a_c,Sconst(Ctrue))] in @@ -654,7 +655,7 @@ let translate_node env let n = String.length f in fun s -> String.sub s (n+1) ((String.length s) - (n+1)) in - node.Minils.n_controller_call <- + node.Minils.n_controller_call <- (List.map remove_prefix inputs, List.map remove_prefix (states@states_c)); @@ -665,11 +666,11 @@ let translate_node env 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 = + 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 = + let constraints_c = List.map (fun v -> Sequal(Ssquare(Svar(v)),Sconst(Ctrue))) (inputs_c@outputs_c) in @@ -702,4 +703,4 @@ let program p = let dirname = build_path (filename ^ "_z3z") in let dir = clean_dir dirname in Sigali.Printer.print dir procs - + diff --git a/compiler/minils/transformations/inline_extvalues.ml b/compiler/minils/transformations/inline_extvalues.ml index f416cbe..71bf64a 100644 --- a/compiler/minils/transformations/inline_extvalues.ml +++ b/compiler/minils/transformations/inline_extvalues.ml @@ -46,6 +46,7 @@ let gather_extvalues_node nd = | Wfield(w, _) -> var_of_extvalue w | Wwhen(w, _, _) -> var_of_extvalue w | Wconst _ -> None + | Wreinit (_, w) -> var_of_extvalue w in match var_of_extvalue w with | Some { w_ty = ty; w_desc = Wvar x; } -> diff --git a/compiler/minils/transformations/tomato.ml b/compiler/minils/transformations/tomato.ml index dc556b0..98f13aa 100644 --- a/compiler/minils/transformations/tomato.ml +++ b/compiler/minils/transformations/tomato.ml @@ -258,6 +258,7 @@ and extvalue is_input w class_id_list = let w_x = mk_extvalue ~ty:Initial.tbool ~clock:w.w_ck ~linearity:w.w_linearity (Wvar x) in let class_id_list, w = decompose w (class_ref_of_var is_input w_x x :: class_id_list) in class_id_list, Wwhen (w, cn, dummy_var) + | Wreinit _ -> assert false in class_id_list, { w with w_desc = wd; } in @@ -409,6 +410,7 @@ and reconstruct_extvalues mapping w_list children = | Wfield (w', fn) -> let w', children = reconstruct_extvalue w' children in { w with w_desc = Wfield (w', fn); }, children + | Wreinit _ -> assert false in let consume w (children, result_w_list) = diff --git a/test/good/reinit.ept b/test/good/reinit.ept new file mode 100644 index 0000000..29bd844 --- /dev/null +++ b/test/good/reinit.ept @@ -0,0 +1,9 @@ +const n:int = 100 +const t_0:int^n = 1^n + +node f(a:int^n at r; c:bool) returns (o:int^n at r) +var a1, a2:int^n at r; +let + (a1, a2) = split c (a); + o = merge c (true -> reinit (a1, t_0)) (false -> [ a2 with [0] = 0 ]) +tel \ No newline at end of file