Revision 36454535
Added by Pierre-Loïc Garoche over 10 years ago
src/inliner.ml | ||
---|---|---|
7 | 7 |
| _ -> false) |
8 | 8 |
|
9 | 9 |
|
10 |
let rename_expr rename expr = expr_replace_var rename expr |
|
11 |
let rename_eq rename eq = |
|
12 |
{ eq with |
|
13 |
eq_lhs = List.map rename eq.eq_lhs; |
|
14 |
eq_rhs = rename_expr rename eq.eq_rhs |
|
15 |
} |
|
16 |
|
|
10 | 17 |
(* |
11 | 18 |
expr, locals', eqs = inline_call id args' reset locals nodes |
12 | 19 |
|
... | ... | |
27 | 34 |
node.node_id uid v; |
28 | 35 |
Format.flush_str_formatter () |
29 | 36 |
in |
30 |
let eqs' = List.map |
|
31 |
(fun eq -> { eq with |
|
32 |
eq_lhs = List.map rename eq.eq_lhs; |
|
33 |
eq_rhs = expr_replace_var rename eq.eq_rhs |
|
34 |
} ) node.node_eqs |
|
37 |
let eqs' = List.map (rename_eq rename) node.node_eqs |
|
35 | 38 |
in |
36 | 39 |
let rename_var v = { v with var_id = rename v.var_id } in |
37 | 40 |
let inputs' = List.map rename_var node.node_inputs in |
... | ... | |
51 | 54 |
loc |
52 | 55 |
(List.map (fun v -> mkexpr loc (Expr_ident v.var_id)) outputs') |
53 | 56 |
in |
54 |
expr , inputs'@outputs'@locals'@locals, assign_inputs::eqs' |
|
57 |
let asserts' = (* We rename variables in assert expressions *) |
|
58 |
List.map |
|
59 |
(fun a -> |
|
60 |
{a with assert_expr = |
|
61 |
let expr = a.assert_expr in |
|
62 |
rename_expr rename expr |
|
63 |
}) |
|
64 |
node.node_asserts |
|
65 |
in |
|
66 |
expr, |
|
67 |
inputs'@outputs'@locals'@locals, |
|
68 |
assign_inputs::eqs', |
|
69 |
asserts' |
|
55 | 70 |
|
56 | 71 |
|
57 | 72 |
|
... | ... | |
65 | 80 |
*) |
66 | 81 |
let rec inline_expr expr locals nodes = |
67 | 82 |
let inline_tuple el = |
68 |
List.fold_right (fun e (el_tail, locals, eqs) -> |
|
69 |
let e', locals', eqs' = inline_expr e locals nodes in |
|
70 |
e'::el_tail, locals', eqs'@eqs |
|
71 |
) el ([], locals, []) |
|
83 |
List.fold_right (fun e (el_tail, locals, eqs, asserts) ->
|
|
84 |
let e', locals', eqs', asserts' = inline_expr e locals nodes in
|
|
85 |
e'::el_tail, locals', eqs'@eqs, asserts@asserts'
|
|
86 |
) el ([], locals, [], [])
|
|
72 | 87 |
in |
73 | 88 |
let inline_pair e1 e2 = |
74 |
let el', l', eqs' = inline_tuple [e1;e2] in |
|
89 |
let el', l', eqs', asserts' = inline_tuple [e1;e2] in
|
|
75 | 90 |
match el' with |
76 |
| [e1'; e2'] -> e1', e2', l', eqs' |
|
91 |
| [e1'; e2'] -> e1', e2', l', eqs', asserts'
|
|
77 | 92 |
| _ -> assert false |
78 | 93 |
in |
79 | 94 |
let inline_triple e1 e2 e3 = |
80 |
let el', l', eqs' = inline_tuple [e1;e2;e3] in |
|
95 |
let el', l', eqs', asserts' = inline_tuple [e1;e2;e3] in
|
|
81 | 96 |
match el' with |
82 |
| [e1'; e2'; e3'] -> e1', e2', e3', l', eqs' |
|
97 |
| [e1'; e2'; e3'] -> e1', e2', e3', l', eqs', asserts'
|
|
83 | 98 |
| _ -> assert false |
84 | 99 |
in |
85 | 100 |
|
86 | 101 |
match expr.expr_desc with |
87 | 102 |
| Expr_appl (id, args, reset) -> |
88 |
let args', locals', eqs' = inline_expr args locals nodes in |
|
103 |
let args', locals', eqs', asserts' = inline_expr args locals nodes in
|
|
89 | 104 |
if List.exists (check_node_name id) nodes then |
90 | 105 |
(* The node should be inlined *) |
91 |
(* let _ = Format.eprintf "Inlining call to %s@." id in
|
|
92 |
*) let node = try List.find (check_node_name id) nodes
|
|
106 |
(* let _ = Format.eprintf "Inlining call to %s@." id in *)
|
|
107 |
let node = try List.find (check_node_name id) nodes |
|
93 | 108 |
with Not_found -> (assert false) in |
94 |
let node = match node.top_decl_desc with Node nd -> nd | _ -> assert false in |
|
109 |
let node = |
|
110 |
match node.top_decl_desc with Node nd -> nd | _ -> assert false in |
|
95 | 111 |
let node = inline_node node nodes in |
96 |
let expr, locals', eqs'' = |
|
112 |
let expr, locals', eqs'', asserts'' =
|
|
97 | 113 |
inline_call expr args' reset locals' node in |
98 |
expr, locals', eqs'@eqs'' |
|
114 |
expr, locals', eqs'@eqs'', asserts'@asserts''
|
|
99 | 115 |
else |
100 | 116 |
(* let _ = Format.eprintf "Not inlining call to %s@." id in *) |
101 |
{ expr with expr_desc = Expr_appl(id, args', reset)}, locals', eqs' |
|
117 |
{ expr with expr_desc = Expr_appl(id, args', reset)}, |
|
118 |
locals', |
|
119 |
eqs', |
|
120 |
asserts' |
|
102 | 121 |
|
103 | 122 |
(* For other cases, we just keep the structure, but convert sub-expressions *) |
104 | 123 |
| Expr_const _ |
105 |
| Expr_ident _ -> expr, locals, [] |
|
124 |
| Expr_ident _ -> expr, locals, [], []
|
|
106 | 125 |
| Expr_tuple el -> |
107 |
let el', l', eqs' = inline_tuple el in |
|
108 |
{ expr with expr_desc = Expr_tuple el' }, l', eqs' |
|
126 |
let el', l', eqs', asserts' = inline_tuple el in
|
|
127 |
{ expr with expr_desc = Expr_tuple el' }, l', eqs', asserts'
|
|
109 | 128 |
| Expr_ite (g, t, e) -> |
110 |
let g', t', e', l', eqs' = inline_triple g t e in |
|
111 |
{ expr with expr_desc = Expr_ite (g', t', e') }, l', eqs' |
|
129 |
let g', t', e', l', eqs', asserts' = inline_triple g t e in
|
|
130 |
{ expr with expr_desc = Expr_ite (g', t', e') }, l', eqs', asserts'
|
|
112 | 131 |
| Expr_arrow (e1, e2) -> |
113 |
let e1', e2', l', eqs' = inline_pair e1 e2 in |
|
114 |
{ expr with expr_desc = Expr_arrow (e1', e2') } , l', eqs' |
|
132 |
let e1', e2', l', eqs', asserts' = inline_pair e1 e2 in
|
|
133 |
{ expr with expr_desc = Expr_arrow (e1', e2') } , l', eqs', asserts'
|
|
115 | 134 |
| Expr_fby (e1, e2) -> |
116 |
let e1', e2', l', eqs' = inline_pair e1 e2 in |
|
117 |
{ expr with expr_desc = Expr_fby (e1', e2') }, l', eqs' |
|
135 |
let e1', e2', l', eqs', asserts' = inline_pair e1 e2 in
|
|
136 |
{ expr with expr_desc = Expr_fby (e1', e2') }, l', eqs', asserts'
|
|
118 | 137 |
| Expr_array el -> |
119 |
let el', l', eqs' = inline_tuple el in |
|
120 |
{ expr with expr_desc = Expr_array el' }, l', eqs' |
|
138 |
let el', l', eqs', asserts' = inline_tuple el in
|
|
139 |
{ expr with expr_desc = Expr_array el' }, l', eqs', asserts'
|
|
121 | 140 |
| Expr_access (e, dim) -> |
122 |
let e', l', eqs' = inline_expr e locals nodes in |
|
123 |
{ expr with expr_desc = Expr_access (e', dim) }, l', eqs' |
|
141 |
let e', l', eqs', asserts' = inline_expr e locals nodes in
|
|
142 |
{ expr with expr_desc = Expr_access (e', dim) }, l', eqs', asserts'
|
|
124 | 143 |
| Expr_power (e, dim) -> |
125 |
let e', l', eqs' = inline_expr e locals nodes in |
|
126 |
{ expr with expr_desc = Expr_power (e', dim) }, l', eqs' |
|
144 |
let e', l', eqs', asserts' = inline_expr e locals nodes in
|
|
145 |
{ expr with expr_desc = Expr_power (e', dim) }, l', eqs', asserts'
|
|
127 | 146 |
| Expr_pre e -> |
128 |
let e', l', eqs' = inline_expr e locals nodes in |
|
129 |
{ expr with expr_desc = Expr_pre e' }, l', eqs' |
|
147 |
let e', l', eqs', asserts' = inline_expr e locals nodes in
|
|
148 |
{ expr with expr_desc = Expr_pre e' }, l', eqs', asserts'
|
|
130 | 149 |
| Expr_when (e, id, label) -> |
131 |
let e', l', eqs' = inline_expr e locals nodes in |
|
132 |
{ expr with expr_desc = Expr_when (e', id, label) }, l', eqs' |
|
150 |
let e', l', eqs', asserts' = inline_expr e locals nodes in
|
|
151 |
{ expr with expr_desc = Expr_when (e', id, label) }, l', eqs', asserts'
|
|
133 | 152 |
| Expr_merge (id, branches) -> |
134 |
let el, l', eqs' = inline_tuple (List.map snd branches) in |
|
153 |
let el, l', eqs', asserts' = inline_tuple (List.map snd branches) in
|
|
135 | 154 |
let branches' = List.map2 (fun (label, _) v -> label, v) branches el in |
136 |
{ expr with expr_desc = Expr_merge (id, branches') }, l', eqs' |
|
155 |
{ expr with expr_desc = Expr_merge (id, branches') }, l', eqs', asserts'
|
|
137 | 156 |
and inline_node nd nodes = |
138 |
let new_locals, eqs = |
|
139 |
List.fold_left (fun (locals, eqs) eq -> |
|
140 |
let eq_rhs', locals', new_eqs' = |
|
157 |
let new_locals, eqs, asserts =
|
|
158 |
List.fold_left (fun (locals, eqs, asserts) eq ->
|
|
159 |
let eq_rhs', locals', new_eqs', asserts' =
|
|
141 | 160 |
inline_expr eq.eq_rhs locals nodes |
142 | 161 |
in |
143 |
locals', { eq with eq_rhs = eq_rhs' }::new_eqs'@eqs
|
|
144 |
) (nd.node_locals, []) nd.node_eqs |
|
162 |
locals', { eq with eq_rhs = eq_rhs' }::new_eqs'@eqs, asserts'@asserts
|
|
163 |
) (nd.node_locals, [], nd.node_asserts) nd.node_eqs
|
|
145 | 164 |
in |
146 | 165 |
{ nd with |
147 | 166 |
node_locals = new_locals; |
148 |
node_eqs = eqs |
|
167 |
node_eqs = eqs; |
|
168 |
node_asserts = asserts; |
|
149 | 169 |
} |
150 | 170 |
|
151 | 171 |
let inline_all_calls node nodes = |
Also available in: Unified diff
Merged horn_traces branch