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