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<exprt> function_calls;
45  std::list<exprt> clusters;
46 
47  void write_dot_subgraph(
48  std::ostream &,
49  const std::string &,
50  const goto_programt &);
51 
52  void do_dot_function_calls(std::ostream &);
53 
54  std::string &escape(std::string &str);
55 
56  void write_edge(std::ostream &,
59  const std::string &);
60 
63  std::set<goto_programt::const_targett> &,
64  std::set<goto_programt::const_targett> &);
65 };
66 
72  std::ostream &out,
73  const std::string &name,
75 {
76  clusters.push_back(exprt("cluster"));
77  clusters.back().set("name", name);
78  clusters.back().set("nr", subgraphscount);
79 
80  out << "subgraph \"cluster_" << name << "\" {\n";
81  out << "label=\"" << name << "\";\n";
82 
83  const goto_programt::instructionst &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->guard.is_true())
111  tmp.str("Goto");
112  else
113  {
114  std::string t = from_expr(ns, it->function, it->guard);
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, it->function, it->guard);
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, it->function, it->guard);
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  std::string t = from_expr(ns, it->function, it->code);
149  while(t[ t.size()-1 ]=='\n')
150  t = t.substr(0, t.size()-1);
151  tmp.str(escape(t));
152 
153  exprt fc;
154  std::stringstream ss;
155  ss << "Node_" << subgraphscount << "_" << it->location_number;
156  fc.operands().push_back(exprt(ss.str()));
157  fc.operands().push_back(it->code.op1());
158  function_calls.push_back(fc);
159  }
160  else if(it->is_assign() ||
161  it->is_decl() ||
162  it->is_return() ||
163  it->is_other())
164  {
165  std::string t = from_expr(ns, it->function, it->code);
166  while(t[ t.size()-1 ]=='\n')
167  t = t.substr(0, t.size()-1);
168  tmp.str(escape(t));
169  }
170  else if(it->is_start_thread())
171  tmp.str("Start of Thread");
172  else if(it->is_end_thread())
173  tmp.str("End of Thread");
174  else if(it->is_throw())
175  tmp.str("THROW");
176  else if(it->is_catch())
177  tmp.str("CATCH");
178  else
179  tmp.str("UNKNOWN");
180 
181  out << "Node_" << subgraphscount << "_" << it->location_number;
182  out << " [shape=";
183  if(it->is_goto() && !it->guard.is_true() && !it->guard.is_false())
184  out << "diamond";
185  else
186  out <<"Mrecord";
187  out << ",fontsize=22,label=\"";
188  out << tmp.str();
189  out << "\"];\n";
190 
191  std::set<goto_programt::const_targett> tres;
192  std::set<goto_programt::const_targett> fres;
193  find_next(instructions, it, tres, fres);
194 
195  std::string tlabel="true";
196  std::string flabel="false";
197  if(fres.empty() || tres.empty())
198  {
199  tlabel="";
200  flabel="";
201  }
202 
203  typedef std::set<goto_programt::const_targett> t;
204 
205  for(t::iterator trit=tres.begin();
206  trit!=tres.end();
207  trit++)
208  write_edge(out, *it, **trit, tlabel);
209  for(t::iterator frit=fres.begin();
210  frit!=fres.end();
211  frit++)
212  write_edge(out, *it, **frit, flabel);
213 
214  seen.insert(it);
215  const auto temp=goto_program.get_successors(it);
216  worklist.insert(worklist.end(), temp.begin(), temp.end());
217  }
218  }
219 
220  out << "}\n";
221  subgraphscount++;
222 }
223 
225  std::ostream &out)
226 {
227  for(const auto &expr : function_calls)
228  {
229  std::list<exprt>::const_iterator cit=clusters.begin();
230  for( ; cit!=clusters.end(); cit++)
231  if(cit->get("name")==expr.op1().get(ID_identifier))
232  break;
233 
234  if(cit!=clusters.end())
235  {
236  out << expr.op0().id() <<
237  " -> " "Node_" << cit->get("nr") << "_0" <<
238  " [lhead=\"cluster_" << expr.op1().get(ID_identifier) << "\"," <<
239  "color=blue];\n";
240  }
241  else
242  {
243  out << "subgraph \"cluster_" << expr.op1().get(ID_identifier) <<
244  "\" {\n";
245  out << "rank=sink;\n";
246  out << "label=\"" << expr.op1().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", expr.op1().get(ID_identifier));
252  clusters.back().set("nr", subgraphscount);
253  out << expr.op0().id() <<
254  " -> " "Node_" << subgraphscount << "_0" <<
255  " [lhead=\"cluster_" << expr.op1().get("identifier") << "\"," <<
256  "color=blue];\n";
257  subgraphscount++;
258  }
259  }
260 }
261 
262 void dott::output(std::ostream &out)
263 {
264  out << "digraph G {\n";
265  out << DOTGRAPHSETTINGS << '\n';
266 
267  std::list<exprt> clusters;
268 
270  if(it->second.body_available())
271  write_dot_subgraph(out, id2string(it->first), it->second.body);
272 
274 
275  out << "}\n";
276 }
277 
281 std::string &dott::escape(std::string &str)
282 {
283  for(std::string::size_type i=0; i<str.size(); i++)
284  {
285  if(str[i]=='\n')
286  {
287  str[i] = 'n';
288  str.insert(i, "\\");
289  }
290  else if(str[i]=='\"' ||
291  str[i]=='|' ||
292  str[i]=='\\' ||
293  str[i]=='>' ||
294  str[i]=='<' ||
295  str[i]=='{' ||
296  str[i]=='}')
297  {
298  str.insert(i, "\\");
299  i++;
300  }
301  }
302 
303  return str;
304 }
305 
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->guard.is_false())
317  {
318  for(const auto &target : it->targets)
319  tres.insert(target);
320  }
321 
322  if(it->is_goto() && it->guard.is_true())
323  return;
324 
325  goto_programt::const_targett next = it; next++;
326  if(next!=instructions.end())
327  fres.insert(next);
328 }
329 
335  std::ostream &out,
336  const goto_programt::instructiont &from,
337  const goto_programt::instructiont &to,
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!="")
344  {
345  out << "[fontsize=20,label=\"" << label << "\"";
346  if(from.is_backwards_goto() &&
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 }
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
unsigned location_number
A globally unique number to identify a program location.
Definition: goto_program.h:364
#define DOTGRAPHSETTINGS
Definition: dot.cpp:20
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
std::list< exprt > clusters
Definition: dot.cpp:45
unsignedbv_typet size_type()
Definition: c_types.cpp:58
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
void output(std::ostream &out)
Definition: dot.cpp:262
bool is_backwards_goto() const
Returns true if the instruction is a backwards branch.
Definition: goto_program.h:374
const goto_modelt & goto_model
Definition: dot.cpp:40
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:173
std::list< instructiont > instructionst
Definition: goto_program.h:395
void dot(const goto_modelt &src, std::ostream &out)
Definition: dot.cpp:354
std::list< const_targett > const_targetst
Definition: goto_program.h:400
std::list< exprt > function_calls
Definition: dot.cpp:44
Definition: dot.cpp:27
std::string & escape(std::string &str)
escapes a string.
Definition: dot.cpp:281
void do_dot_function_calls(std::ostream &)
Definition: dot.cpp:224
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:403
dott(const goto_modelt &_goto_model)
Definition: dot.cpp:30
Dump Goto-Program as DOT Graph.
instructionst::const_iterator const_targett
Definition: goto_program.h:398
std::list< Target > get_successors(Target target) const
Definition: goto_program.h:646
TO_BE_DOCUMENTED.
Definition: namespace.h:74
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
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
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
Base class for all expressions.
Definition: expr.h:42
goto_programt & goto_program
Definition: cover.cpp:63
#define forall_goto_functions(it, functions)
operandst & operands()
Definition: expr.h:66
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
unsigned subgraphscount
Definition: dot.cpp:42
void write_dot_subgraph(std::ostream &, const std::string &, const goto_programt &)
writes the dot graph that corresponds to the goto program to the output stream.
Definition: dot.cpp:71