From 7d6106d0aae78037f793f57d6671194c5db4b802 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Gwena=C3=ABl=20Delaval?= Date: Tue, 23 May 2017 22:13:32 +0200 Subject: [PATCH] Passes optimization Translation to tail-recursive versions of functions for handling of (very) big nodes. --- compiler/heptagon/analysis/causality.ml | 14 +++++++---- compiler/heptagon/parsing/hept_scoping.ml | 6 ++--- .../heptagon/transformations/completion.ml | 4 ++-- compiler/heptagon/transformations/last.ml | 19 ++++++++------- compiler/main/hept2mls.ml | 8 +++---- compiler/main/mls2obc.ml | 17 ++++++------- compiler/minils/analysis/clocking.ml | 4 ++-- .../minils/transformations/normalize_mem.ml | 4 ++-- compiler/obc/control.ml | 24 +++++++++---------- 9 files changed, 54 insertions(+), 46 deletions(-) diff --git a/compiler/heptagon/analysis/causality.ml b/compiler/heptagon/analysis/causality.ml index 3599e9e..f498aa6 100644 --- a/compiler/heptagon/analysis/causality.ml +++ b/compiler/heptagon/analysis/causality.ml @@ -42,11 +42,15 @@ let cand c1 c2 = match c1, c2 with | Cempty, _ -> c2 | _, Cempty -> c1 | c1, c2 -> Cand(c1, c2) -let rec candlist l = +let candlist l = + let rec candlist_aux acc l = + match l with + | [] -> acc + | [c] -> cand acc c + | c1 :: l -> candlist_aux (cand c1 acc) l in match l with - | [] -> Cempty - | [c] -> c - | c1 :: l -> cand c1 (candlist l) + | [] -> Cempty + | c :: l -> candlist_aux c l let ctuplelist l = match l with | [c] -> c @@ -185,7 +189,7 @@ let rec typing_pat = function candlist (List.map typing_pat pat_list) (** Typing equations *) -let rec typing_eqs eq_list = candlist (List.map typing_eq eq_list) +let rec typing_eqs eq_list = candlist (List.rev_map typing_eq eq_list) and typing_eq eq = match eq.eq_desc with diff --git a/compiler/heptagon/parsing/hept_scoping.ml b/compiler/heptagon/parsing/hept_scoping.ml index a9c8e1a..d4c5302 100644 --- a/compiler/heptagon/parsing/hept_scoping.ml +++ b/compiler/heptagon/parsing/hept_scoping.ml @@ -403,7 +403,7 @@ and translate_eq_desc loc env = function and translate_block env b = let env = Rename.append env b.b_local in { Heptagon.b_local = translate_vd_list env b.b_local; - Heptagon.b_equs = List.map (translate_eq env) b.b_equs; + Heptagon.b_equs = List.rev_map (translate_eq env) b.b_equs; Heptagon.b_defnames = Env.empty; Heptagon.b_stateful = false; Heptagon.b_loc = b.b_loc; }, env @@ -442,8 +442,8 @@ and translate_var_dec env vd = Heptagon.v_loc = vd.v_loc } (** [env] should contain the declared variables prior to this translation *) -and translate_vd_list env = - List.map (translate_var_dec env) +and translate_vd_list env v_list = + List.rev (List.rev_map (translate_var_dec env) v_list) and translate_last = function | Var -> Heptagon.Var diff --git a/compiler/heptagon/transformations/completion.ml b/compiler/heptagon/transformations/completion.ml index 99624cc..b28d000 100644 --- a/compiler/heptagon/transformations/completion.ml +++ b/compiler/heptagon/transformations/completion.ml @@ -74,8 +74,8 @@ let complete_with_last defined_names local_defined_names eq_list = let block funs defnames b = let b, _ = Hept_mapfold.block funs Env.empty b in (*recursive call*) - let added_eq = complete_with_last defnames b.b_defnames [] in - { b with b_equs = b.b_equs @ added_eq; b_defnames = defnames } + let eqs = complete_with_last defnames b.b_defnames b.b_equs in + { b with b_equs = eqs; b_defnames = defnames } , defnames let eqdesc funs _ ed = match ed with diff --git a/compiler/heptagon/transformations/last.ml b/compiler/heptagon/transformations/last.ml index 0b1ae8d..5589089 100644 --- a/compiler/heptagon/transformations/last.ml +++ b/compiler/heptagon/transformations/last.ml @@ -52,7 +52,8 @@ let last (eq_list, env, v) { v_ident = n; v_type = t; v_linearity = lin; v_last Env.add n lastn env, (mk_var_dec lastn t ~linearity:lin) :: v -let extend_env env v = List.fold_left last ([], env, []) v +let extend_env env eq_list acc_vd vd_list = + List.fold_left last (eq_list, env, acc_vd) vd_list let edesc _ env ed = match ed with | Elast x -> @@ -60,19 +61,21 @@ let edesc _ env ed = match ed with | _ -> raise Errors.Fallback let block funs env b = - let eq_lastn_n_list, env, last_v = extend_env env b.b_local in + let eq_list, env, vd_list = extend_env env b.b_equs b.b_local b.b_local in let b, _ = Hept_mapfold.block funs env b in - { b with b_local = b.b_local @ last_v; - b_equs = eq_lastn_n_list @ b.b_equs }, env + { b with b_local = vd_list; + b_equs = eq_list }, + env let node_dec funs _ n = Idents.enter_node n.n_name; - let _, env, _ = extend_env Env.empty n.n_input in - let eq_lasto_list, env, last_o = extend_env env n.n_output in + let { n_block } = n in + let _, env, _ = extend_env Env.empty [] [] n.n_input in + let eq_list, env, vd_list = extend_env env n_block.b_equs n_block.b_local n.n_output in let n, _ = Hept_mapfold.node_dec funs env n in { n with n_block = - { n.n_block with b_local = n.n_block.b_local @ last_o; - b_equs = eq_lasto_list @ n.n_block.b_equs } }, env + { n_block with b_local = vd_list; + b_equs = eq_list } }, env let program p = let funs = { Hept_mapfold.defaults with diff --git a/compiler/main/hept2mls.ml b/compiler/main/hept2mls.ml index d848f53..7692881 100644 --- a/compiler/main/hept2mls.ml +++ b/compiler/main/hept2mls.ml @@ -209,8 +209,8 @@ let translate_contract contract = Heptagon.c_assume_loc = e_a_loc; Heptagon.c_enforce_loc = e_g_loc; Heptagon.c_controllables = l_c } -> - Some { c_local = List.map translate_var v; - c_eq = List.map translate_eq eq_list; + Some { c_local = List.rev_map translate_var v; + c_eq = List.rev_map translate_eq eq_list; c_assume = translate_extvalue e_a; c_objectives = List.map translate_objective objs; c_assume_loc = translate_extvalue e_a_loc; @@ -225,8 +225,8 @@ 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_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_local = List.rev_map translate_var n.Heptagon.n_block.Heptagon.b_local; + n_equs = List.rev_map translate_eq n.Heptagon.n_block.Heptagon.b_equs; n_loc = n.Heptagon.n_loc ; n_params = n.Heptagon.n_params; n_param_constraints = n.Heptagon.n_param_constraints; diff --git a/compiler/main/mls2obc.ml b/compiler/main/mls2obc.ml index 2a22c43..7abba2e 100644 --- a/compiler/main/mls2obc.ml +++ b/compiler/main/mls2obc.ml @@ -234,7 +234,7 @@ let translate_var_dec l = let one_var { Minils.v_ident = x; Minils.v_type = t; Minils.v_linearity = lin; v_loc = loc } = mk_var_dec ~loc:loc ~linearity:lin x t in - List.map one_var l + List.rev (List.rev_map one_var l) let rec translate_extvalue map w = match w.Minils.w_desc with | Minils.Wvar x -> ext_value_of_pattern (var_from_name map x) @@ -452,12 +452,12 @@ let empty_call_context = None [s] the actions used in the step method. [v] var decs *) let rec translate_eq map call_context - ({ Minils.eq_lhs = pat; Minils.eq_base_ck = ck; Minils.eq_rhs = e } as eq) - (v, si, j, s) = + (v, si, j, s) + ({ Minils.eq_lhs = pat; Minils.eq_base_ck = ck; Minils.eq_rhs = e } as eq) = let { Minils.e_desc = desc; Minils.e_loc = loc } = e in match (pat, desc) with | _pat, Minils.Ewhen (e,_,_) -> - translate_eq map call_context {eq with Minils.eq_rhs = e} (v, si, j, s) + translate_eq map call_context (v, si, j, s) {eq with Minils.eq_rhs = e} (* TODO Efby and Eifthenelse should be dealt with in translate_act, no ? *) | Minils.Evarpat n, Minils.Efby (opt_c, e) -> let x = var_from_name map n in @@ -529,7 +529,8 @@ let rec translate_eq map call_context v, si, j, action @ s and translate_eq_list map call_context act_list = - List.fold_right (translate_eq map call_context) act_list ([], [], [], []) + let rev_act = List.rev act_list in + List.fold_left (translate_eq map call_context) ([], [], [], []) rev_act and mk_node_call map call_context app loc (name_list : Obc.pattern list) args ty = match app.Minils.a_op with @@ -734,17 +735,17 @@ let translate_node let (m_c, si', j', s_list', d_list') = translate_contract subst_map mem_var_tys contract in let i_list = translate_var_dec i_list in let o_list = translate_var_dec o_list in - let d_list = translate_var_dec (v @ d_list) in + let d_list = translate_var_dec (List.rev_append v d_list) in let m, d_list = List.partition (fun vd -> List.exists (fun (i,_) -> i = vd.v_ident) mem_var_tys) d_list in let m', o_list = List.partition (fun vd -> List.exists (fun (i,_) -> i = vd.v_ident) mem_var_tys) o_list in - let s = s_list @ s_list' in + let s = List.rev_append (List.rev s_list) s_list' in let j = j' @ j in let si = si @ si' in let stepm = { m_name = Mstep; m_inputs = i_list; m_outputs = o_list; - m_body = mk_block ~locals:(d_list' @ d_list) s } + m_body = mk_block ~locals:(List.rev_append d_list' d_list) s } in let resetm = { m_name = Mreset; m_inputs = []; m_outputs = []; m_body = mk_block si } in if stateful diff --git a/compiler/minils/analysis/clocking.ml b/compiler/minils/analysis/clocking.ml index 1761605..da7537b 100644 --- a/compiler/minils/analysis/clocking.ml +++ b/compiler/minils/analysis/clocking.ml @@ -249,7 +249,7 @@ let typing_eq h ({ eq_lhs = pat; eq_rhs = e; eq_loc = loc } as eq) = error_message loc (Etypeclash (ct, pat_ct))); { eq with eq_base_ck = base_ck } -let typing_eqs h eq_list = List.map (typing_eq h) eq_list +let typing_eqs h eq_list = List.rev_map (typing_eq h) eq_list let append_env h vds = List.fold_left (fun h { v_ident = n; v_clock = ck } -> Env.add n ck h) h vds @@ -290,7 +290,7 @@ let typing_node node = 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; - n_local = List.map set_clock node.n_local; + n_local = List.rev_map set_clock node.n_local; n_equs = equs; n_contract = contract; } in diff --git a/compiler/minils/transformations/normalize_mem.ml b/compiler/minils/transformations/normalize_mem.ml index c5f2baf..1feefec 100644 --- a/compiler/minils/transformations/normalize_mem.ml +++ b/compiler/minils/transformations/normalize_mem.ml @@ -107,10 +107,10 @@ let contract _ acc c = c, acc let node funs acc nd = let env = build_env nd in let nd, (_, _, v, eqs) = - Mls_mapfold.node_dec funs (env, nd.n_local @ nd.n_output, [], []) nd + Mls_mapfold.node_dec funs (env, nd.n_output @ nd.n_local, nd.n_local, []) nd in (* return updated node *) - { nd with n_local = v @ nd.n_local; n_equs = List.rev eqs }, acc + { nd with n_local = v; n_equs = List.rev eqs }, acc let program p = let funs = { Mls_mapfold.defaults with diff --git a/compiler/obc/control.ml b/compiler/obc/control.ml index 1ec2639..613344f 100644 --- a/compiler/obc/control.ml +++ b/compiler/obc/control.ml @@ -113,31 +113,31 @@ let is_deadcode = function (* TODO Etrange puisque c'est apres la passe de deadc | _ -> false let rec joinlist j l = - let rec join_next l = + let rec join_next acc l = match l with - | [] -> [] - | [s1] -> [s1] + | [] -> acc + | [s1] -> s1::acc | s1::s2::l -> match s1, s2 with | Acase(e1, h1), Acase(e2, h2) when Obc_compare.exp_compare e1 e2 = 0 -> let fused_switch = Acase(e1, joinhandlers j h1 h2) in if is_modified_handlers j e2 h1 then - fused_switch::(join_first l) + join_first (fused_switch::acc) l else - join_next (fused_switch::l) - | s1, s2 -> s1::(join_first (s2::l)) - and join_first l = + join_next acc (fused_switch::l) + | s1, s2 -> join_first (s1::acc) (s2::l) + and join_first acc l = match l with - | [] -> [] + | [] -> acc | (Acase(e1, h1))::l -> if is_modified_handlers j e1 h1 then - (Acase(e1, h1))::(join_next l) + join_next ((Acase(e1, h1))::acc) l else - join_next ((Acase(e1, h1))::l) - | _ -> join_next l + join_next acc ((Acase(e1, h1))::l) + | _ -> join_next acc l in - join_first l + List.rev (join_first [] l) and join_block j b =