From 21433f641671c0d4996f050d83802dd35bee4bb7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?C=C3=A9dric=20Pasteur?= Date: Thu, 20 Oct 2011 09:16:51 +0200 Subject: [PATCH] Only do one copy for two recursive registers --- .../minils/transformations/normalize_mem.ml | 52 +++++++++++++++---- 1 file changed, 41 insertions(+), 11 deletions(-) diff --git a/compiler/minils/transformations/normalize_mem.ml b/compiler/minils/transformations/normalize_mem.ml index 56c3201..8b76297 100644 --- a/compiler/minils/transformations/normalize_mem.ml +++ b/compiler/minils/transformations/normalize_mem.ml @@ -2,6 +2,7 @@ open Idents open Signature open Minils open Mls_mapfold +open Mls_utils (** Adds an extra equation for outputs that are also memories. For instance, if o is an output, then: @@ -9,6 +10,14 @@ open Mls_mapfold becomes mem_o = v fby e; o = mem_o + + We also need to add one copy if two registers are defined by each other, eg: + x = v fby y; + y = v fby x; + becomes + mem_x = v fby y; + x = mem_x; + y = v fby x *) let memory_vars_vds nd = @@ -20,10 +29,31 @@ let memory_vars_vds nd = let mem_var_tys = Mls_utils.node_memory_vars nd in List.map (fun (x, _) -> Env.find x env) mem_var_tys -let eq _ (outputs, v, eqs) eq = match eq.eq_lhs, eq.eq_rhs.e_desc with - | Evarpat x, Efby _ -> - if Mls_utils.vd_mem x outputs then - let vd = Mls_utils.vd_find x outputs in +let copies_done = ref [] +let add_copy x y = + copies_done := (x, y) :: !copies_done +let clear_copies () = + copies_done := [] +let is_copy_done x y = + List.mem (x, y) !copies_done + +(* If x and y are both registers, only create one copy *) +let should_be_normalized outputs mems x w = match w.w_desc with + | Wvar y -> + add_copy x y; + (vd_mem x outputs) or (vd_mem x mems && not (is_copy_done y x)) + | _ -> + (vd_mem x outputs) or (vd_mem x mems) + +let find_vd x outputs mems = + if vd_mem x outputs then + vd_find x outputs + else + vd_find x mems + +let eq _ (outputs, mems, v, eqs) eq = match eq.eq_lhs, eq.eq_rhs.e_desc with + | Evarpat x, Efby (_, w) when should_be_normalized outputs mems x w -> + let vd = find_vd x outputs mems in let x_mem = Idents.gen_var "normalize_mem" ("mem_"^(Idents.name x)) in let vd_mem = { vd with v_ident = x_mem } in let exp_mem_x = mk_extvalue_exp vd.v_clock vd.v_type @@ -32,23 +62,23 @@ let eq _ (outputs, v, eqs) eq = match eq.eq_lhs, eq.eq_rhs.e_desc with let eq_copy = { eq with eq_lhs = Evarpat x_mem } in (* o = mem_o *) let eq = { eq with eq_rhs = exp_mem_x } in - eq, (outputs, vd_mem::v, eq::eq_copy::eqs) - else (* this memory is not an output *) - eq, (outputs, v, eq::eqs) + eq, (outputs, mems, vd_mem::v, eq::eq_copy::eqs) | _, _ -> - eq, (outputs, v, eq::eqs) + eq, (outputs, mems, v, eq::eqs) (* Leave contract unchanged (no output defined in it) *) let contract funs acc c = c, acc let node funs acc nd = - let outputs_mems = nd.n_output @ memory_vars_vds nd in - let nd, (_, v, eqs) = Mls_mapfold.node_dec funs (outputs_mems, nd.n_local, []) nd in + clear_copies (); + let nd, (_, _, v, eqs) = + Mls_mapfold.node_dec funs (nd.n_output, memory_vars_vds nd, nd.n_local, []) nd + in (* return updated node *) { nd with n_local = v; n_equs = List.rev eqs }, acc let program p = let funs = { Mls_mapfold.defaults with eq = eq; node_dec = node; contract = contract } in - let p, _ = Mls_mapfold.program_it funs ([], [], []) p in + let p, _ = Mls_mapfold.program_it funs ([], [], [], []) p in p