jeltz/heptagon
1
0
Fork 0
Code Issues Pull requests Releases Activity

Only do one copy for two recursive registers

Browse source
This commit is contained in:
Cédric Pasteur 2011-10-20 09:16:51 +02:00
parent 72cac326a8
commit 21433f6416
1 changed files with 41 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

52
compiler/minils/transformations/normalize_mem.ml
View file

@ -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