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 <sstream>
15 
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 
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 auto &function_call = it->get_function_call();
148  std::string t = from_expr(ns, function_id, function_call);
149  while(t[ t.size()-1 ]=='\n')
150  t = t.substr(0, t.size()-1);
151  tmp.str(escape(t));
152 
153  std::stringstream ss;
154  ss << "Node_" << subgraphscount << "_" << it->location_number;
155  function_calls.push_back(
156  std::pair<std::string, exprt>(ss.str(), it->call_function()));
157  }
158  else if(
159  it->is_assign() || it->is_decl() || it->is_set_return_value() ||
160  it->is_other())
161  {
162  std::string t = from_expr(ns, function_id, it->get_code());
163  while(t[ t.size()-1 ]=='\n')
164  t = t.substr(0, t.size()-1);
165  tmp.str(escape(t));
166  }
167  else if(it->is_start_thread())
168  tmp.str("Start of Thread");
169  else if(it->is_end_thread())
170  tmp.str("End of Thread");
171  else if(it->is_throw())
172  tmp.str("THROW");
173  else if(it->is_catch())
174  tmp.str("CATCH");
175  else
176  tmp.str("UNKNOWN");
177 
178  out << "Node_" << subgraphscount << "_" << it->location_number;
179  out << " [shape=";
180  if(it->is_goto() && !it->get_condition().is_constant())
181  out << "diamond";
182  else
183  out <<"Mrecord";
184  out << ",fontsize=22,label=\"";
185  out << tmp.str();
186  out << "\"];\n";
187 
188  std::set<goto_programt::const_targett> tres;
189  std::set<goto_programt::const_targett> fres;
190  find_next(instructions, it, tres, fres);
191 
192  std::string tlabel;
193  std::string flabel;
194  if(!fres.empty() && !tres.empty())
195  {
196  tlabel = "true";
197  flabel = "false";
198  }
199 
200  typedef std::set<goto_programt::const_targett> t;
201 
202  for(t::iterator trit=tres.begin();
203  trit!=tres.end();
204  trit++)
205  write_edge(out, *it, **trit, tlabel);
206  for(t::iterator frit=fres.begin();
207  frit!=fres.end();
208  frit++)
209  write_edge(out, *it, **frit, flabel);
210 
211  seen.insert(it);
212  const auto temp=goto_program.get_successors(it);
213  worklist.insert(worklist.end(), temp.begin(), temp.end());
214  }
215  }
216 
217  out << "}\n";
218  subgraphscount++;
219 }
220 
222  std::ostream &out)
223 {
224  for(const auto &call : function_calls)
225  {
226  std::list<exprt>::const_iterator cit=clusters.begin();
227  for( ; cit!=clusters.end(); cit++)
228  if(cit->get("name") == call.second.get(ID_identifier))
229  break;
230 
231  if(cit!=clusters.end())
232  {
233  out << call.first
234  << " -> "
235  "Node_"
236  << cit->get("nr") << "_0"
237  << " [lhead=\"cluster_" << call.second.get(ID_identifier) << "\","
238  << "color=blue];\n";
239  }
240  else
241  {
242  out << "subgraph \"cluster_" << call.second.get(ID_identifier)
243  << "\" {\n";
244  out << "rank=sink;\n";
245  out << "label=\"" << call.second.get(ID_identifier) << "\";\n";
246  out << "Node_" << subgraphscount << "_0 " <<
247  "[shape=Mrecord,fontsize=22,label=\"?\"];\n";
248  out << "}\n";
249  clusters.push_back(exprt("cluster"));
250  clusters.back().set("name", call.second.get(ID_identifier));
251  clusters.back().set("nr", subgraphscount);
252  out << call.first
253  << " -> "
254  "Node_"
255  << subgraphscount << "_0"
256  << " [lhead=\"cluster_" << call.second.get("identifier") << "\","
257  << "color=blue];\n";
258  subgraphscount++;
259  }
260  }
261 }
262 
263 void dott::output(std::ostream &out)
264 {
265  out << "digraph G {\n";
266  out << DOTGRAPHSETTINGS << '\n';
267 
268  for(const auto &gf_entry : goto_model.goto_functions.function_map)
269  {
270  if(gf_entry.second.body_available())
271  write_dot_subgraph(out, gf_entry.first, gf_entry.second.body);
272  }
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 
311  const goto_programt::instructionst &instructions,
313  std::set<goto_programt::const_targett> &tres,
314  std::set<goto_programt::const_targett> &fres)
315 {
316  if(it->is_goto() && !it->get_condition().is_false())
317  {
318  for(const auto &target : it->targets)
319  tres.insert(target);
320  }
321 
322  if(it->is_goto() && it->get_condition().is_true())
323  return;
324 
325  goto_programt::const_targett next = it; next++;
326  if(next!=instructions.end())
327  fres.insert(next);
328 }
329 
334  std::ostream &out,
335  const goto_programt::instructiont &from,
336  const goto_programt::instructiont &to,
337  const std::string &label)
338 {
339  out << "Node_" << subgraphscount << "_" << from.location_number;
340  out << " -> ";
341  out << "Node_" << subgraphscount << "_" << to.location_number << " ";
342  if(!label.empty())
343  {
344  out << "[fontsize=20,label=\"" << label << "\"";
345  if(from.is_backwards_goto() && from.location_number > to.location_number)
346  out << ",color=red";
347  out << "]";
348  }
349  out << ";\n";
350 }
351 
352 void dot(const goto_modelt &src, std::ostream &out)
353 {
354  dott dot(src);
355  dot.output(out);
356 }
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:649
goto_programt::instructionst
std::list< instructiont > instructionst
Definition: goto_program.h:644
dot
void dot(const goto_modelt &src, std::ostream &out)
Definition: dot.cpp:352
goto_model.h
Symbol Table + CFG.
dott::dott
dott(const goto_modelt &_goto_model)
Definition: dot.cpp:30
exprt
Base class for all expressions.
Definition: expr.h:54
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:1143
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:29
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:70
dott::do_dot_function_calls
void do_dot_function_calls(std::ostream &)
Definition: dot.cpp:221
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:91
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:333
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:310
dott::output
void output(std::ostream &out)
Definition: dot.cpp:263
goto_programt::instructiont::is_backwards_goto
bool is_backwards_goto() const
Returns true if the instruction is a backwards branch.
Definition: goto_program.h:604
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:652
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:594
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:71
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:647
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:178
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