cprover
dot.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Dump Goto-Program as DOT Graph
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "dot.h"
13
14#include <sstream>
15
17
19
20#define DOTGRAPHSETTINGS "color=black;" \
21 "orientation=portrait;" \
22 "fontsize=20;"\
23 "compound=true;"\
24 "size=\"30,40\";"\
25 "ratio=compress;"
26
27class dott
28{
29public:
30 explicit dott(
31 const goto_modelt &_goto_model):
32 goto_model(_goto_model),
34 {
35 }
36
37 void output(std::ostream &out);
38
39protected:
41
43
44 std::list<std::pair<std::string, exprt>> function_calls;
45 std::list<exprt> clusters;
46
47 void
48 write_dot_subgraph(std::ostream &, const irep_idt &, const goto_programt &);
49
50 void do_dot_function_calls(std::ostream &);
51
52 std::string &escape(std::string &str);
53
54 void write_edge(std::ostream &,
57 const std::string &);
58
61 std::set<goto_programt::const_targett> &,
62 std::set<goto_programt::const_targett> &);
63};
64
71 std::ostream &out,
72 const irep_idt &function_id,
73 const goto_programt &goto_program)
74{
75 clusters.push_back(exprt("cluster"));
76 clusters.back().set("name", function_id);
77 clusters.back().set("nr", subgraphscount);
78
79 out << "subgraph \"cluster_" << function_id << "\" {\n";
80 out << "label=\"" << function_id << "\";\n";
81
82 const goto_programt::instructionst &instructions =
83 goto_program.instructions;
84
85 if(instructions.empty())
86 {
87 out << "Node_" << subgraphscount << "_0 " <<
88 "[shape=Mrecord,fontsize=22,label=\"?\"];\n";
89 }
90 else
91 {
93
94 std::set<goto_programt::const_targett> seen;
96 worklist.push_back(instructions.begin());
97
98 while(!worklist.empty())
99 {
100 goto_programt::const_targett it=worklist.front();
101 worklist.pop_front();
102
103 if(it==instructions.end() ||
104 seen.find(it)!=seen.end()) continue;
105
106 std::stringstream tmp;
107 if(it->is_goto())
108 {
109 if(it->get_condition().is_true())
110 tmp.str("Goto");
111 else
112 {
113 std::string t = from_expr(ns, function_id, it->get_condition());
114 while(t[ t.size()-1 ]=='\n')
115 t = t.substr(0, t.size()-1);
116 tmp << escape(t) << "?";
117 }
118 }
119 else if(it->is_assume())
120 {
121 std::string t = from_expr(ns, function_id, it->get_condition());
122 while(t[ t.size()-1 ]=='\n')
123 t = t.substr(0, t.size()-1);
124 tmp << "Assume\\n(" << escape(t) << ")";
125 }
126 else if(it->is_assert())
127 {
128 std::string t = from_expr(ns, function_id, it->get_condition());
129 while(t[ t.size()-1 ]=='\n')
130 t = t.substr(0, t.size()-1);
131 tmp << "Assert\\n(" << escape(t) << ")";
132 }
133 else if(it->is_skip())
134 tmp.str("Skip");
135 else if(it->is_end_function())
136 tmp.str("End of Function");
137 else if(it->is_location())
138 tmp.str("Location");
139 else if(it->is_dead())
140 tmp.str("Dead");
141 else if(it->is_atomic_begin())
142 tmp.str("Atomic Begin");
143 else if(it->is_atomic_end())
144 tmp.str("Atomic End");
145 else if(it->is_function_call())
146 {
147 const code_function_callt function_call(
148 it->call_lhs(), it->call_function(), it->call_arguments());
149 std::string t = from_expr(ns, function_id, function_call);
150 while(t[ t.size()-1 ]=='\n')
151 t = t.substr(0, t.size()-1);
152 tmp.str(escape(t));
153
154 std::stringstream ss;
155 ss << "Node_" << subgraphscount << "_" << it->location_number;
156 function_calls.push_back(
157 std::pair<std::string, exprt>(ss.str(), it->call_function()));
158 }
159 else if(
160 it->is_assign() || it->is_decl() || it->is_set_return_value() ||
161 it->is_other())
162 {
163 std::string t = from_expr(ns, function_id, it->get_code());
164 while(t[ t.size()-1 ]=='\n')
165 t = t.substr(0, t.size()-1);
166 tmp.str(escape(t));
167 }
168 else if(it->is_start_thread())
169 tmp.str("Start of Thread");
170 else if(it->is_end_thread())
171 tmp.str("End of Thread");
172 else if(it->is_throw())
173 tmp.str("THROW");
174 else if(it->is_catch())
175 tmp.str("CATCH");
176 else
177 tmp.str("UNKNOWN");
178
179 out << "Node_" << subgraphscount << "_" << it->location_number;
180 out << " [shape=";
181 if(it->is_goto() && !it->get_condition().is_constant())
182 out << "diamond";
183 else
184 out <<"Mrecord";
185 out << ",fontsize=22,label=\"";
186 out << tmp.str();
187 out << "\"];\n";
188
189 std::set<goto_programt::const_targett> tres;
190 std::set<goto_programt::const_targett> fres;
191 find_next(instructions, it, tres, fres);
192
193 std::string tlabel;
194 std::string flabel;
195 if(!fres.empty() && !tres.empty())
196 {
197 tlabel = "true";
198 flabel = "false";
199 }
200
201 typedef std::set<goto_programt::const_targett> t;
202
203 for(t::iterator trit=tres.begin();
204 trit!=tres.end();
205 trit++)
206 write_edge(out, *it, **trit, tlabel);
207 for(t::iterator frit=fres.begin();
208 frit!=fres.end();
209 frit++)
210 write_edge(out, *it, **frit, flabel);
211
212 seen.insert(it);
213 const auto temp=goto_program.get_successors(it);
214 worklist.insert(worklist.end(), temp.begin(), temp.end());
215 }
216 }
217
218 out << "}\n";
220}
221
223 std::ostream &out)
224{
225 for(const auto &call : function_calls)
226 {
227 std::list<exprt>::const_iterator cit=clusters.begin();
228 for( ; cit!=clusters.end(); cit++)
229 if(cit->get("name") == call.second.get(ID_identifier))
230 break;
231
232 if(cit!=clusters.end())
233 {
234 out << call.first
235 << " -> "
236 "Node_"
237 << cit->get("nr") << "_0"
238 << " [lhead=\"cluster_" << call.second.get(ID_identifier) << "\","
239 << "color=blue];\n";
240 }
241 else
242 {
243 out << "subgraph \"cluster_" << call.second.get(ID_identifier)
244 << "\" {\n";
245 out << "rank=sink;\n";
246 out << "label=\"" << call.second.get(ID_identifier) << "\";\n";
247 out << "Node_" << subgraphscount << "_0 " <<
248 "[shape=Mrecord,fontsize=22,label=\"?\"];\n";
249 out << "}\n";
250 clusters.push_back(exprt("cluster"));
251 clusters.back().set("name", call.second.get(ID_identifier));
252 clusters.back().set("nr", subgraphscount);
253 out << call.first
254 << " -> "
255 "Node_"
256 << subgraphscount << "_0"
257 << " [lhead=\"cluster_" << call.second.get("identifier") << "\","
258 << "color=blue];\n";
260 }
261 }
262}
263
264void dott::output(std::ostream &out)
265{
266 out << "digraph G {\n";
267 out << DOTGRAPHSETTINGS << '\n';
268
269 for(const auto &gf_entry : goto_model.goto_functions.function_map)
270 {
271 if(gf_entry.second.body_available())
272 write_dot_subgraph(out, gf_entry.first, gf_entry.second.body);
273 }
274
276
277 out << "}\n";
278}
279
283std::string &dott::escape(std::string &str)
284{
285 for(std::string::size_type i=0; i<str.size(); i++)
286 {
287 if(str[i]=='\n')
288 {
289 str[i] = 'n';
290 str.insert(i, "\\");
291 }
292 else if(str[i]=='\"' ||
293 str[i]=='|' ||
294 str[i]=='\\' ||
295 str[i]=='>' ||
296 str[i]=='<' ||
297 str[i]=='{' ||
298 str[i]=='}')
299 {
300 str.insert(i, "\\");
301 i++;
302 }
303 }
304
305 return str;
306}
307
312 const goto_programt::instructionst &instructions,
314 std::set<goto_programt::const_targett> &tres,
315 std::set<goto_programt::const_targett> &fres)
316{
317 if(it->is_goto() && !it->get_condition().is_false())
318 {
319 for(const auto &target : it->targets)
320 tres.insert(target);
321 }
322
323 if(it->is_goto() && it->get_condition().is_true())
324 return;
325
326 goto_programt::const_targett next = it; next++;
327 if(next!=instructions.end())
328 fres.insert(next);
329}
330
335 std::ostream &out,
336 const goto_programt::instructiont &from,
338 const std::string &label)
339{
340 out << "Node_" << subgraphscount << "_" << from.location_number;
341 out << " -> ";
342 out << "Node_" << subgraphscount << "_" << to.location_number << " ";
343 if(!label.empty())
344 {
345 out << "[fontsize=20,label=\"" << label << "\"";
347 out << ",color=red";
348 out << "]";
349 }
350 out << ";\n";
351}
352
353void dot(const goto_modelt &src, std::ostream &out)
354{
355 dott dot(src);
356 dot.output(out);
357}
unsignedbv_typet size_type()
Definition: c_types.cpp:68
codet representation of a function call statement.
Definition: dot.cpp:28
std::list< std::pair< std::string, exprt > > function_calls
Definition: dot.cpp:44
std::list< exprt > clusters
Definition: dot.cpp:45
std::string & escape(std::string &str)
Escapes a string.
Definition: dot.cpp:283
unsigned subgraphscount
Definition: dot.cpp:42
void do_dot_function_calls(std::ostream &)
Definition: dot.cpp:222
void write_dot_subgraph(std::ostream &, const irep_idt &, const goto_programt &)
Write the dot graph that corresponds to the goto program to the output stream.
Definition: dot.cpp:70
const goto_modelt & goto_model
Definition: dot.cpp:40
dott(const goto_modelt &_goto_model)
Definition: dot.cpp:30
void output(std::ostream &out)
Definition: dot.cpp:264
void find_next(const goto_programt::instructionst &, const goto_programt::const_targett &, std::set< goto_programt::const_targett > &, std::set< goto_programt::const_targett > &)
finds an instructions successors (for goto graphs)
Definition: dot.cpp:311
void write_edge(std::ostream &, const goto_programt::instructiont &, const goto_programt::instructiont &, const std::string &)
writes an edge from the from node to the to node and with the given label to the output stream (dot f...
Definition: dot.cpp:334
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:180
unsigned location_number
A globally unique number to identify a program location.
Definition: goto_program.h:540
bool is_backwards_goto() const
Returns true if the instruction is a backwards branch.
Definition: goto_program.h:550
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:598
instructionst::const_iterator const_targett
Definition: goto_program.h:593
std::list< instructiont > instructionst
Definition: goto_program.h:590
std::list< const_targett > const_targetst
Definition: goto_program.h:595
std::list< Target > get_successors(Target target) const
Get control-flow successors of a given instruction.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
#define DOTGRAPHSETTINGS
Definition: dot.cpp:20
void dot(const goto_modelt &src, std::ostream &out)
Definition: dot.cpp:353
Dump Goto-Program as DOT Graph.
Symbol Table + CFG.
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)