Revision ca7ff3f7
Added by Lélio Brun 8 months ago
| src/optimize_prog.ml | ||
|---|---|---|
| 14 | 14 |
(* open LustreSpec *) |
| 15 | 15 |
|
| 16 | 16 |
(* Consts unfoooolding *) |
| 17 |
let is_const i consts = |
|
| 18 |
List.exists (fun c -> c.const_id = i) consts |
|
| 17 |
let is_const i consts = List.exists (fun c -> c.const_id = i) consts |
|
| 19 | 18 |
|
| 20 | 19 |
let get_const i consts = |
| 21 | 20 |
let c = List.find (fun c -> c.const_id = i) consts in |
| 22 | 21 |
c.const_value |
| 23 | 22 |
|
| 24 |
let rec expr_unfold_consts consts e =
|
|
| 25 |
{ e with expr_desc = expr_desc_unfold_consts consts e.expr_desc e.expr_type }
|
|
| 23 |
let rec expr_unfold_consts consts e = |
|
| 24 |
{ e with expr_desc = expr_desc_unfold_consts consts e.expr_desc e.expr_type }
|
|
| 26 | 25 |
|
| 27 | 26 |
and expr_desc_unfold_consts consts e e_type = |
| 28 | 27 |
let unfold = expr_unfold_consts consts in |
| 29 | 28 |
match e with |
| 30 |
| Expr_const _ -> e |
|
| 31 |
| Expr_ident i -> if is_const i consts && not (Types.is_array_type e_type) then Expr_const (get_const i consts) else e |
|
| 32 |
| Expr_array el -> Expr_array (List.map unfold el) |
|
| 33 |
| Expr_access (e1, d) -> Expr_access (unfold e1, d) |
|
| 34 |
| Expr_power (e1, d) -> Expr_power (unfold e1, d) |
|
| 35 |
| Expr_tuple el -> Expr_tuple (List.map unfold el) |
|
| 36 |
| Expr_ite (c, t, e) -> Expr_ite (unfold c, unfold t, unfold e) |
|
| 37 |
| Expr_arrow (e1, e2)-> Expr_arrow (unfold e1, unfold e2) |
|
| 38 |
| Expr_fby (e1, e2) -> Expr_fby (unfold e1, unfold e2) |
|
| 29 |
| Expr_const _ -> |
|
| 30 |
e |
|
| 31 |
| Expr_ident i -> |
|
| 32 |
if is_const i consts && not (Types.is_array_type e_type) then |
|
| 33 |
Expr_const (get_const i consts) |
|
| 34 |
else e |
|
| 35 |
| Expr_array el -> |
|
| 36 |
Expr_array (List.map unfold el) |
|
| 37 |
| Expr_access (e1, d) -> |
|
| 38 |
Expr_access (unfold e1, d) |
|
| 39 |
| Expr_power (e1, d) -> |
|
| 40 |
Expr_power (unfold e1, d) |
|
| 41 |
| Expr_tuple el -> |
|
| 42 |
Expr_tuple (List.map unfold el) |
|
| 43 |
| Expr_ite (c, t, e) -> |
|
| 44 |
Expr_ite (unfold c, unfold t, unfold e) |
|
| 45 |
| Expr_arrow (e1, e2) -> |
|
| 46 |
Expr_arrow (unfold e1, unfold e2) |
|
| 47 |
| Expr_fby (e1, e2) -> |
|
| 48 |
Expr_fby (unfold e1, unfold e2) |
|
| 39 | 49 |
(* | Expr_concat (e1, e2) -> Expr_concat (unfold e1, unfold e2) *) |
| 40 | 50 |
(* | Expr_tail e' -> Expr_tail (unfold e') *) |
| 41 |
| Expr_pre e' -> Expr_pre (unfold e') |
|
| 42 |
| Expr_when (e', i, l)-> Expr_when (unfold e', i, l) |
|
| 43 |
| Expr_merge (i, hl) -> Expr_merge (i, List.map (fun (t, h) -> (t, unfold h)) hl) |
|
| 44 |
| Expr_appl (i, e', i') -> Expr_appl (i, unfold e', i') |
|
| 51 |
| Expr_pre e' -> |
|
| 52 |
Expr_pre (unfold e') |
|
| 53 |
| Expr_when (e', i, l) -> |
|
| 54 |
Expr_when (unfold e', i, l) |
|
| 55 |
| Expr_merge (i, hl) -> |
|
| 56 |
Expr_merge (i, List.map (fun (t, h) -> t, unfold h) hl) |
|
| 57 |
| Expr_appl (i, e', i') -> |
|
| 58 |
Expr_appl (i, unfold e', i') |
|
| 45 | 59 |
|
| 46 | 60 |
let eq_unfold_consts consts eq = |
| 47 | 61 |
{ eq with eq_rhs = expr_unfold_consts consts eq.eq_rhs }
|
| ... | ... | |
| 49 | 63 |
let node_unfold_consts consts node = |
| 50 | 64 |
let eqs, automata = get_node_eqs node in |
| 51 | 65 |
assert (automata = []); |
| 52 |
{ node with node_stmts = List.map (fun eq -> Eq (eq_unfold_consts consts eq)) eqs }
|
|
| 66 |
{
|
|
| 67 |
node with |
|
| 68 |
node_stmts = List.map (fun eq -> Eq (eq_unfold_consts consts eq)) eqs; |
|
| 69 |
} |
|
| 53 | 70 |
|
| 54 | 71 |
let prog_unfold_consts prog = |
| 55 | 72 |
let consts = List.map const_of_top (get_consts prog) in |
| 56 |
List.map ( |
|
| 57 |
fun decl -> match decl.top_decl_desc with |
|
| 58 |
| Node nd -> {decl with top_decl_desc = Node (node_unfold_consts consts nd)}
|
|
| 59 |
| _ -> decl |
|
| 60 |
) prog |
|
| 73 |
List.map |
|
| 74 |
(fun decl -> |
|
| 75 |
match decl.top_decl_desc with |
|
| 76 |
| Node nd -> |
|
| 77 |
{ decl with top_decl_desc = Node (node_unfold_consts consts nd) }
|
|
| 78 |
| _ -> |
|
| 79 |
decl) |
|
| 80 |
prog |
|
| 61 | 81 |
|
| 62 |
(* Distribution of when inside sub-expressions, i.e. (a+b) when c --> a when c + b when c
|
|
| 63 |
May increase clock disjointness of variables, which is useful for code optimization
|
|
| 64 |
*) |
|
| 82 |
(* Distribution of when inside sub-expressions, i.e. (a+b) when c --> a when c + |
|
| 83 |
b when c May increase clock disjointness of variables, which is useful for
|
|
| 84 |
code optimization *)
|
|
| 65 | 85 |
let apply_stack expr stack = |
| 66 |
List.fold_left (fun expr (v, t) -> mkexpr expr.expr_loc (Expr_when (expr, v, t))) expr stack |
|
| 86 |
List.fold_left |
|
| 87 |
(fun expr (v, t) -> mkexpr expr.expr_loc (Expr_when (expr, v, t))) |
|
| 88 |
expr stack |
|
| 67 | 89 |
|
| 68 | 90 |
let expr_distribute_when expr = |
| 69 | 91 |
let rec distrib stack expr = |
| 70 | 92 |
match expr.expr_desc with |
| 71 |
| Expr_const _ |
|
| 72 |
| Expr_ident _ |
|
| 73 |
| Expr_arrow _ |
|
| 74 |
| Expr_fby _ |
|
| 75 |
| Expr_pre _ |
|
| 76 |
-> apply_stack expr stack |
|
| 93 |
| Expr_const _ | Expr_ident _ | Expr_arrow _ | Expr_fby _ | Expr_pre _ -> |
|
| 94 |
apply_stack expr stack |
|
| 77 | 95 |
| Expr_appl (id, _, _) when not (Stateless.check_node (node_from_name id)) |
| 78 |
-> apply_stack expr stack |
|
| 79 |
| Expr_ite (c, t, e) |
|
| 80 |
-> let cid = ident_of_expr c in |
|
| 81 |
mkexpr expr.expr_loc |
|
| 82 |
(Expr_merge (cid, |
|
| 83 |
[(tag_true , distrib ((cid,tag_true )::stack) t); |
|
| 84 |
(tag_false, distrib ((cid,tag_false)::stack) e)])) |
|
| 85 |
| Expr_array el -> { expr with expr_desc = (Expr_array (List.map (distrib stack) el)) }
|
|
| 86 |
| Expr_access (e1, d) -> { expr with expr_desc = Expr_access (distrib stack e1, d) }
|
|
| 87 |
| Expr_power (e1, d) -> { expr with expr_desc = Expr_power (distrib stack e1, d) }
|
|
| 88 |
| Expr_tuple el -> { expr with expr_desc = Expr_tuple (List.map (distrib stack) el) }
|
|
| 89 |
| Expr_when (e', i, l)-> distrib ((i, l)::stack) e' |
|
| 90 |
| Expr_merge (i, hl) -> { expr with expr_desc = Expr_merge (i, List.map (fun (t, h) -> (t, distrib stack h)) hl) }
|
|
| 91 |
| Expr_appl (id, e', i') -> { expr with expr_desc = Expr_appl (id, distrib stack e', i')}
|
|
| 92 |
in distrib [] expr |
|
| 96 |
-> |
|
| 97 |
apply_stack expr stack |
|
| 98 |
| Expr_ite (c, t, e) -> |
|
| 99 |
let cid = ident_of_expr c in |
|
| 100 |
mkexpr expr.expr_loc |
|
| 101 |
(Expr_merge |
|
| 102 |
( cid, |
|
| 103 |
[ |
|
| 104 |
tag_true, distrib ((cid, tag_true) :: stack) t; |
|
| 105 |
tag_false, distrib ((cid, tag_false) :: stack) e; |
|
| 106 |
] )) |
|
| 107 |
| Expr_array el -> |
|
| 108 |
{ expr with expr_desc = Expr_array (List.map (distrib stack) el) }
|
|
| 109 |
| Expr_access (e1, d) -> |
|
| 110 |
{ expr with expr_desc = Expr_access (distrib stack e1, d) }
|
|
| 111 |
| Expr_power (e1, d) -> |
|
| 112 |
{ expr with expr_desc = Expr_power (distrib stack e1, d) }
|
|
| 113 |
| Expr_tuple el -> |
|
| 114 |
{ expr with expr_desc = Expr_tuple (List.map (distrib stack) el) }
|
|
| 115 |
| Expr_when (e', i, l) -> |
|
| 116 |
distrib ((i, l) :: stack) e' |
|
| 117 |
| Expr_merge (i, hl) -> |
|
| 118 |
{
|
|
| 119 |
expr with |
|
| 120 |
expr_desc = |
|
| 121 |
Expr_merge (i, List.map (fun (t, h) -> t, distrib stack h) hl); |
|
| 122 |
} |
|
| 123 |
| Expr_appl (id, e', i') -> |
|
| 124 |
{ expr with expr_desc = Expr_appl (id, distrib stack e', i') }
|
|
| 125 |
in |
|
| 126 |
distrib [] expr |
|
| 93 | 127 |
|
| 94 |
let eq_distribute_when eq = |
|
| 95 |
{ eq with eq_rhs = expr_distribute_when eq.eq_rhs }
|
|
| 128 |
let eq_distribute_when eq = { eq with eq_rhs = expr_distribute_when eq.eq_rhs }
|
|
| 96 | 129 |
|
| 97 | 130 |
let node_distribute_when node = |
| 98 | 131 |
let eqs, automata = get_node_eqs node in |
| ... | ... | |
| 100 | 133 |
{ node with node_stmts = List.map (fun eq -> Eq (eq_distribute_when eq)) eqs }
|
| 101 | 134 |
|
| 102 | 135 |
let prog_distribute_when prog = |
| 103 |
List.map ( |
|
| 104 |
fun decl -> match decl.top_decl_desc with |
|
| 105 |
| Node nd -> {decl with top_decl_desc = Node (node_distribute_when nd)}
|
|
| 106 |
| _ -> decl |
|
| 107 |
) prog |
|
| 136 |
List.map |
|
| 137 |
(fun decl -> |
|
| 138 |
match decl.top_decl_desc with |
|
| 139 |
| Node nd -> |
|
| 140 |
{ decl with top_decl_desc = Node (node_distribute_when nd) }
|
|
| 141 |
| _ -> |
|
| 142 |
decl) |
|
| 143 |
prog |
|
| 108 | 144 |
(* Local Variables: *) |
| 109 | 145 |
(* compile-command:"make -C .." *) |
| 110 | 146 |
(* End: *) |
Also available in: Unified diff
reformatting