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 #define DOTGRAPHSETTINGS "color=black;" \
19  "orientation=portrait;" \
20  "fontsize=20;"\
21  "compound=true;"\
22  "size=\"30,40\";"\
23  "ratio=compress;"
24 
25 class dott
26 {
27 public:
29  const goto_functionst &_goto_functions,
30  const namespacet &_ns):
31  ns(_ns),
32  goto_functions(_goto_functions),
34  {
35  }
36 
37  void output(std::ostream &out);
38 
39 protected:
40  const namespacet &ns;
42 
43  unsigned subgraphscount;
44 
45  std::list<exprt> function_calls;
46  std::list<exprt> clusters;
47 
48  void write_dot_subgraph(
49  std::ostream &,
50  const std::string &,
51  const goto_programt &);
52 
53  void do_dot_function_calls(std::ostream &);
54 
55  std::string &escape(std::string &str);
56 
57  void write_edge(std::ostream &,
58  const goto_programt::instructiont &,
59  const goto_programt::instructiont &,
60  const std::string &);
61 
64  std::set<goto_programt::const_targett> &,
65  std::set<goto_programt::const_targett> &);
66 };
67 
73  std::ostream &out,
74  const std::string &name,
75  const goto_programt &goto_program)
76 {
77  clusters.push_back(exprt("cluster"));
78  clusters.back().set("name", name);
79  clusters.back().set("nr", subgraphscount);
80 
81  out << "subgraph \"cluster_" << name << "\" {\n";
82  out << "label=\"" << name << "\";\n";
83 
84  const goto_programt::instructionst &instructions =
85  goto_program.instructions;
86 
87  if(instructions.empty())
88  {
89  out << "Node_" << subgraphscount << "_0 " <<
90  "[shape=Mrecord,fontsize=22,label=\"?\"];\n";
91  }
92  else
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->guard.is_true())
110  tmp.str("Goto");
111  else
112  {
113  std::string t = from_expr(ns, "", it->guard);
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, "", it->guard);
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, "", it->guard);
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  std::string t = from_expr(ns, "", it->code);
148  while(t[ t.size()-1 ]=='\n')
149  t = t.substr(0, t.size()-1);
150  tmp.str(escape(t));
151 
152  exprt fc;
153  std::stringstream ss;
154  ss << "Node_" << subgraphscount << "_" << it->location_number;
155  fc.operands().push_back(exprt(ss.str()));
156  fc.operands().push_back(it->code.op1());
157  function_calls.push_back(fc);
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, "", 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->guard.is_true() && !it->guard.is_false())
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="true";
195  std::string flabel="false";
196  if(fres.empty() || tres.empty())
197  {
198  tlabel="";
199  flabel="";
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 &expr : function_calls)
227  {
228  std::list<exprt>::const_iterator cit=clusters.begin();
229  for( ; cit!=clusters.end(); cit++)
230  if(cit->get("name")==expr.op1().get(ID_identifier))
231  break;
232 
233  if(cit!=clusters.end())
234  {
235  out << expr.op0().id() <<
236  " -> " "Node_" << cit->get("nr") << "_0" <<
237  " [lhead=\"cluster_" << expr.op1().get(ID_identifier) << "\"," <<
238  "color=blue];\n";
239  }
240  else
241  {
242  out << "subgraph \"cluster_" << expr.op1().get(ID_identifier) <<
243  "\" {\n";
244  out << "rank=sink;\n";
245  out << "label=\"" << expr.op1().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", expr.op1().get(ID_identifier));
251  clusters.back().set("nr", subgraphscount);
252  out << expr.op0().id() <<
253  " -> " "Node_" << subgraphscount << "_0" <<
254  " [lhead=\"cluster_" << expr.op1().get("identifier") << "\"," <<
255  "color=blue];\n";
256  subgraphscount++;
257  }
258  }
259 }
260 
261 void dott::output(std::ostream &out)
262 {
263  out << "digraph G {\n";
264  out << DOTGRAPHSETTINGS << '\n';
265 
266  std::list<exprt> clusters;
267 
269  if(it->second.body_available())
270  write_dot_subgraph(out, id2string(it->first), it->second.body);
271 
273 
274  out << "}\n";
275 }
276 
280 std::string &dott::escape(std::string &str)
281 {
282  for(std::string::size_type i=0; i<str.size(); i++)
283  {
284  if(str[i]=='\n')
285  {
286  str[i] = 'n';
287  str.insert(i, "\\");
288  }
289  else if(str[i]=='\"' ||
290  str[i]=='|' ||
291  str[i]=='\\' ||
292  str[i]=='>' ||
293  str[i]=='<' ||
294  str[i]=='{' ||
295  str[i]=='}')
296  {
297  str.insert(i, "\\");
298  i++;
299  }
300  }
301 
302  return str;
303 }
304 
310  const goto_programt::instructionst &instructions,
312  std::set<goto_programt::const_targett> &tres,
313  std::set<goto_programt::const_targett> &fres)
314 {
315  if(it->is_goto() && !it->guard.is_false())
316  {
317  for(const auto &target : it->targets)
318  tres.insert(target);
319  }
320 
321  if(it->is_goto() && it->guard.is_true())
322  return;
323 
324  goto_programt::const_targett next = it; next++;
325  if(next!=instructions.end())
326  fres.insert(next);
327 }
328 
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!="")
343  {
344  out << "[fontsize=20,label=\"" << label << "\"";
345  if(from.is_backwards_goto() &&
346  from.location_number > to.location_number)
347  out << ",color=red";
348  out << "]";
349  }
350  out << ";\n";
351 }
352 
353 void dot(
354  const goto_functionst &src,
355  const namespacet &ns,
356  std::ostream &out)
357 {
358  dott dot(src, ns);
359  dot.output(out);
360 }
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
instructionst instructions
The list of instructions in the goto program.
#define DOTGRAPHSETTINGS
Definition: dot.cpp:18
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
std::list< exprt > clusters
Definition: dot.cpp:46
unsignedbv_typet size_type()
Definition: c_types.cpp:57
const goto_functionst & goto_functions
Definition: dot.cpp:41
void output(std::ostream &out)
Definition: dot.cpp:261
const namespacet & ns
Definition: dot.cpp:40
std::list< Target > get_successors(Target target) const
instructionst::const_iterator const_targett
std::list< exprt > function_calls
Definition: dot.cpp:45
Definition: dot.cpp:25
std::string & escape(std::string &str)
escapes a string.
Definition: dot.cpp:280
void do_dot_function_calls(std::ostream &)
Definition: dot.cpp:223
Dump Goto-Program as DOT Graph.
TO_BE_DOCUMENTED.
Definition: namespace.h:62
dott(const goto_functionst &_goto_functions, const namespacet &_ns)
Definition: dot.cpp:28
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:309
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
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
Base class for all expressions.
Definition: expr.h:46
void dot(const goto_functionst &src, const namespacet &ns, std::ostream &out)
Definition: dot.cpp:353
#define forall_goto_functions(it, functions)
operandst & operands()
Definition: expr.h:70
unsigned subgraphscount
Definition: dot.cpp:43
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:72