Branch data Line data Source code
1 : : /* A graph for exploring trees of feasible paths through the egraph.
2 : : Copyright (C) 2021-2025 Free Software Foundation, Inc.
3 : : Contributed by David Malcolm <dmalcolm@redhat.com>.
4 : :
5 : : This file is part of GCC.
6 : :
7 : : GCC is free software; you can redistribute it and/or modify it
8 : : under the terms of the GNU General Public License as published by
9 : : the Free Software Foundation; either version 3, or (at your option)
10 : : any later version.
11 : :
12 : : GCC is distributed in the hope that it will be useful, but
13 : : WITHOUT ANY WARRANTY; without even the implied warranty of
14 : : MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
15 : : General Public License for more details.
16 : :
17 : : You should have received a copy of the GNU General Public License
18 : : along with GCC; see the file COPYING3. If not see
19 : : <http://www.gnu.org/licenses/>. */
20 : :
21 : : #include "analyzer/common.h"
22 : :
23 : : #include "cfg.h"
24 : : #include "gimple-iterator.h"
25 : : #include "cgraph.h"
26 : : #include "digraph.h"
27 : :
28 : : #include "analyzer/analyzer-logging.h"
29 : : #include "analyzer/sm.h"
30 : : #include "analyzer/pending-diagnostic.h"
31 : : #include "analyzer/diagnostic-manager.h"
32 : : #include "analyzer/call-string.h"
33 : : #include "analyzer/program-point.h"
34 : : #include "analyzer/store.h"
35 : : #include "analyzer/region-model.h"
36 : : #include "analyzer/constraint-manager.h"
37 : : #include "analyzer/supergraph.h"
38 : : #include "analyzer/program-state.h"
39 : : #include "analyzer/exploded-graph.h"
40 : : #include "analyzer/feasible-graph.h"
41 : :
42 : : #if ENABLE_ANALYZER
43 : :
44 : : namespace ana {
45 : :
46 : : /* class base_feasible_node : public dnode<fg_traits>. */
47 : :
48 : : /* Print an id to PP for this node suitable for use in .dot dumps. */
49 : :
50 : : void
51 : 214 : base_feasible_node::dump_dot_id (pretty_printer *pp) const
52 : : {
53 : 214 : pp_printf (pp, "fnode_%i", m_index);
54 : 214 : }
55 : :
56 : : /* class feasible_node : public base_feasible_node. */
57 : :
58 : : /* Implementation of dump_dot vfunc for feasible_node. */
59 : :
60 : : void
61 : 74 : feasible_node::dump_dot (graphviz_out *gv,
62 : : const dump_args_t &) const
63 : : {
64 : 74 : pretty_printer *pp = gv->get_pp ();
65 : :
66 : 74 : dump_dot_id (pp);
67 : 74 : pp_printf (pp, " [shape=none,margin=0,style=filled,fillcolor=%s,label=\"",
68 : 74 : m_inner_node->get_dot_fillcolor ());
69 : 74 : pp_write_text_to_stream (pp);
70 : :
71 : 74 : pp_printf (pp, "FN: %i (EN: %i); len=%i", m_index, m_inner_node->m_index,
72 : 74 : m_path_length);
73 : 74 : pp_newline (pp);
74 : :
75 : 74 : format f (true);
76 : 74 : m_inner_node->get_point ().print (pp, f);
77 : 74 : pp_newline (pp);
78 : :
79 : : /* Show the model at this point along expansion of the feasible path,
80 : : rather than the model within the enode. */
81 : 74 : m_state.get_model ().dump_to_pp (pp, true, true);
82 : 74 : pp_newline (pp);
83 : :
84 : 74 : m_inner_node->dump_saved_diagnostics (pp);
85 : :
86 : 74 : pp_write_text_as_dot_label_to_stream (pp, /*for_record=*/true);
87 : :
88 : 74 : pp_string (pp, "\"];\n\n");
89 : 74 : pp_flush (pp);
90 : 74 : }
91 : :
92 : : /* Implementation of dump_dot vfunc for infeasible_node.
93 : : In particular, show the rejected constraint. */
94 : :
95 : : void
96 : 0 : infeasible_node::dump_dot (graphviz_out *gv,
97 : : const dump_args_t &) const
98 : : {
99 : 0 : pretty_printer *pp = gv->get_pp ();
100 : :
101 : 0 : dump_dot_id (pp);
102 : 0 : pp_printf (pp, " [shape=none,margin=0,style=filled,fillcolor=%s,label=\"",
103 : 0 : m_inner_node->get_dot_fillcolor ());
104 : 0 : pp_write_text_to_stream (pp);
105 : :
106 : 0 : pp_printf (pp, "infeasible edge to EN: %i", m_inner_node->m_index);
107 : 0 : pp_newline (pp);
108 : :
109 : 0 : pp_string (pp, "rejected constraint:");
110 : 0 : pp_newline (pp);
111 : 0 : m_rc->dump_to_pp (pp);
112 : :
113 : 0 : pp_write_text_as_dot_label_to_stream (pp, /*for_record=*/true);
114 : :
115 : 0 : pp_string (pp, "\"];\n\n");
116 : 0 : pp_flush (pp);
117 : 0 : }
118 : :
119 : : /* class base_feasible_edge : public dedge<fg_traits>. */
120 : :
121 : : /* Implementation of dump_dot vfunc for base_easible_edge. */
122 : :
123 : : void
124 : 70 : base_feasible_edge::dump_dot (graphviz_out *gv, const dump_args_t &) const
125 : : {
126 : 70 : pretty_printer *pp = gv->get_pp ();
127 : :
128 : 70 : m_src->dump_dot_id (pp);
129 : 70 : pp_string (pp, " -> ");
130 : 70 : m_dest->dump_dot_id (pp);
131 : :
132 : 70 : m_inner_edge->dump_dot_label (pp);
133 : 70 : }
134 : :
135 : : /* class feasible_graph : public digraph <fg_traits>. */
136 : :
137 : : /* Ctor for feasible_graph. */
138 : :
139 : 6369 : feasible_graph::feasible_graph ()
140 : 6369 : : m_num_infeasible (0)
141 : : {
142 : 6369 : }
143 : :
144 : : /* Add a feasible_node to this graph for ENODE, STATE with the
145 : : given PATH_LENGTH. */
146 : :
147 : : feasible_node *
148 : 146330 : feasible_graph::add_node (const exploded_node *enode,
149 : : const feasibility_state &state,
150 : : unsigned path_length)
151 : : {
152 : : /* We don't attempt get_or_create here. */
153 : 146330 : feasible_node *fnode = new feasible_node (enode, m_nodes.length (),
154 : 286291 : state, path_length);
155 : 146330 : digraph<fg_traits>::add_node (fnode);
156 : 146330 : return fnode;
157 : : }
158 : :
159 : : /* Add an infeasible_node to this graph and an infeasible_edge connecting
160 : : to it from SRC_FNODE, capturing a failure of RC along EEDGE. */
161 : :
162 : : void
163 : 2248 : feasible_graph::add_feasibility_problem (feasible_node *src_fnode,
164 : : const exploded_edge *eedge,
165 : : std::unique_ptr<rejected_constraint> rc)
166 : : {
167 : 2248 : infeasible_node *dst_fnode
168 : 4496 : = new infeasible_node (eedge->m_dest, m_nodes.length (), std::move (rc));
169 : 2248 : digraph<fg_traits>::add_node (dst_fnode);
170 : 2248 : add_edge (new infeasible_edge (src_fnode, dst_fnode, eedge));
171 : 2248 : m_num_infeasible++;
172 : 2248 : }
173 : :
174 : : /* Make an exploded_path from the origin to FNODE's exploded_node,
175 : : following the edges in the feasible_graph. */
176 : :
177 : : std::unique_ptr<exploded_path>
178 : 6090 : feasible_graph::make_epath (feasible_node *fnode) const
179 : : {
180 : 6090 : std::unique_ptr<exploded_path> epath (new exploded_path ());
181 : :
182 : : /* FG is actually a tree. Built the path backwards, by walking
183 : : backwards from FNODE until we reach the origin. */
184 : 85187 : while (fnode->get_inner_node ()->m_index != 0)
185 : : {
186 : 79097 : gcc_assert (fnode->m_preds.length () == 1);
187 : 79097 : feasible_edge *pred_fedge
188 : 79097 : = static_cast <feasible_edge *> (fnode->m_preds[0]);
189 : 79097 : epath->m_edges.safe_push (pred_fedge->get_inner_edge ());
190 : 79097 : fnode = static_cast <feasible_node *> (pred_fedge->m_src);
191 : : }
192 : :
193 : : /* Now reverse it. */
194 : 6090 : epath->m_edges.reverse ();
195 : :
196 : 6090 : return epath;
197 : : }
198 : :
199 : : /* Dump the path to DST_FNODE in textual form to PP. */
200 : :
201 : : void
202 : 4 : feasible_graph::dump_feasible_path (const feasible_node &dst_fnode,
203 : : pretty_printer *pp) const
204 : : {
205 : 4 : const feasible_node *fnode = &dst_fnode;
206 : :
207 : 4 : auto_vec<const feasible_edge *> fpath;
208 : :
209 : : /* FG is actually a tree. Built the path backwards, by walking
210 : : backwards from FNODE until we reach the origin. */
211 : 74 : while (fnode->get_inner_node ()->m_index != 0)
212 : : {
213 : 70 : gcc_assert (fnode->m_preds.length () == 1);
214 : 70 : feasible_edge *pred_fedge
215 : 70 : = static_cast <feasible_edge *> (fnode->m_preds[0]);
216 : 70 : fpath.safe_push (pred_fedge);
217 : 70 : fnode = static_cast <const feasible_node *> (pred_fedge->m_src);
218 : : }
219 : :
220 : : /* Now reverse it. */
221 : 4 : fpath.reverse ();
222 : :
223 : 74 : for (unsigned i = 0; i < fpath.length (); i++)
224 : : {
225 : 70 : const feasible_edge *fedge = fpath[i];
226 : 70 : const feasible_node *src_fnode
227 : : = static_cast <const feasible_node *> (fedge->m_src);
228 : 70 : const feasible_node *dest_fnode
229 : : = static_cast <const feasible_node *> (fedge->m_dest);
230 : :
231 : 70 : pp_printf (pp, "fpath[%i]: FN %i (EN %i) -> FN %i (EN %i)",
232 : : i,
233 : : src_fnode->get_index (),
234 : 70 : src_fnode->get_inner_node ()->m_index,
235 : : dest_fnode->get_index (),
236 : 70 : dest_fnode->get_inner_node ()->m_index);
237 : 70 : pp_newline (pp);
238 : 70 : pp_printf (pp, " FN %i (EN %i):",
239 : : dest_fnode->get_index (),
240 : 70 : dest_fnode->get_inner_node ()->m_index);
241 : 70 : pp_newline (pp);
242 : 70 : const program_point &point = dest_fnode->get_inner_node ()->get_point ();
243 : 70 : point.print (pp, format (true));
244 : 70 : dest_fnode->get_state ().dump_to_pp (pp, true, true);
245 : 70 : pp_newline (pp);
246 : : }
247 : 4 : }
248 : :
249 : : /* Dump the path to DST_FNODE in textual form to FILENAME. */
250 : :
251 : : void
252 : 4 : feasible_graph::dump_feasible_path (const feasible_node &dst_fnode,
253 : : const char *filename) const
254 : : {
255 : 4 : FILE *fp = fopen (filename, "w");
256 : 4 : pretty_printer pp;
257 : 4 : pp_format_decoder (&pp) = default_tree_printer;
258 : 4 : pp.set_output_stream (fp);
259 : 4 : dump_feasible_path (dst_fnode, &pp);
260 : 4 : pp_flush (&pp);
261 : 4 : fclose (fp);
262 : 4 : }
263 : :
264 : : /* Dump stats about this graph to LOGGER. */
265 : :
266 : : void
267 : 0 : feasible_graph::log_stats (logger *logger) const
268 : : {
269 : 0 : logger->log ("#nodes: %i", m_nodes.length ());
270 : 0 : logger->log ("#edges: %i", m_edges.length ());
271 : 0 : logger->log ("#feasible nodes: %i", m_nodes.length () - m_num_infeasible);
272 : 0 : logger->log ("#feasible edges: %i", m_edges.length () - m_num_infeasible);
273 : 0 : logger->log ("#infeasible nodes/edges: %i", m_num_infeasible);
274 : 0 : }
275 : :
276 : : } // namespace ana
277 : :
278 : : #endif /* #if ENABLE_ANALYZER */
|
