CBMC
graphml.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Read/write graphs as GraphML
4 
5 Author: Michael Tautschnig, mt@eecs.qmul.ac.uk
6 
7 \*******************************************************************/
8 
11 
12 #include "graphml.h"
13 
14 // include last to make sure #define stack(x) of parser.h does not
15 // collide with std::stack included by graph.h
16 #include "xml_parser.h"
17 
18 typedef std::map<std::string, graphmlt::node_indext> name_mapt;
19 
21  const std::string &name,
22  name_mapt &name_to_node,
23  graphmlt &graph)
24 {
25  std::pair<name_mapt::iterator, bool> entry=
26  name_to_node.insert(std::make_pair(name, 0));
27  if(entry.second)
28  entry.first->second=graph.add_node();
29 
30  return entry.first->second;
31 }
32 
33 static bool build_graph_rec(
34  const xmlt &xml,
35  name_mapt &name_to_node,
36  std::map<std::string, std::map<std::string, std::string> > &defaults,
37  graphmlt &dest,
38  std::string &entrynode)
39 {
40  if(xml.name=="node")
41  {
42  const std::string node_name=xml.get_attribute("id");
43 
44  const graphmlt::node_indext n=
45  add_node(node_name, name_to_node, dest);
46 
47  graphmlt::nodet &node=dest[n];
48  node.node_name=node_name;
49  node.is_violation=false;
50  node.has_invariant=false;
51 
52  for(xmlt::elementst::const_iterator
53  e_it=xml.elements.begin();
54  e_it!=xml.elements.end();
55  e_it++)
56  {
57  DATA_INVARIANT(e_it->name == "data", "expected data node");
58 
59  if(e_it->get_attribute("key")=="violation" &&
60  e_it->data=="true")
61  node.is_violation=e_it->data=="true";
62  else if(e_it->get_attribute("key")=="entry" &&
63  e_it->data=="true")
64  entrynode=node_name;
65  }
66  }
67  else if(xml.name=="edge")
68  {
69  const std::string source=xml.get_attribute("source");
70  const std::string target=xml.get_attribute("target");
71 
72  const graphmlt::node_indext s=add_node(source, name_to_node, dest);
73  const graphmlt::node_indext t=add_node(target, name_to_node, dest);
74 
75  // add edge and annotate
76  xmlt xml_w_defaults=xml;
77 
78  std::map<std::string, std::string> &edge_defaults=defaults["edge"];
79  for(std::map<std::string, std::string>::const_iterator
80  it=edge_defaults.begin();
81  it!=edge_defaults.end();
82  ++it)
83  {
84  bool found=false;
85  for(xmlt::elementst::const_iterator
86  e_it=xml.elements.begin();
87  e_it!=xml.elements.end() && !found;
88  ++e_it)
89  found=e_it->get_attribute("key")==it->first;
90 
91  if(!found)
92  {
93  xmlt &d=xml_w_defaults.new_element("data");
94  d.set_attribute("key", it->first);
95  d.data=it->second;
96  }
97  }
98 
99  dest[s].out[t].xml_node=xml_w_defaults;
100  dest[t].in[s].xml_node=xml_w_defaults;
101  }
102  else if(xml.name=="graphml" ||
103  xml.name=="graph")
104  {
105  for(xmlt::elementst::const_iterator
106  e_it=xml.elements.begin();
107  e_it!=xml.elements.end();
108  e_it++)
109  // recursive call
110  if(build_graph_rec(
111  *e_it,
112  name_to_node,
113  defaults,
114  dest,
115  entrynode))
116  return true;
117  }
118  else if(xml.name=="key")
119  {
120  for(xmlt::elementst::const_iterator
121  e_it=xml.elements.begin();
122  e_it!=xml.elements.end();
123  ++e_it)
124  if(e_it->name=="default")
125  defaults[xml.get_attribute("for")][xml.get_attribute("id")]=
126  e_it->data;
127  }
128  else if(xml.name=="data")
129  {
130  // ignored
131  }
132  else
133  {
134  UNREACHABLE;
135  return true;
136  }
137 
138  return false;
139 }
140 
141 static bool build_graph(
142  const xmlt &xml,
143  graphmlt &dest,
144  graphmlt::node_indext &entry)
145 {
146  PRECONDITION(dest.empty());
147 
148  name_mapt name_to_node;
149  std::map<std::string, std::map<std::string, std::string> > defaults;
150  std::string entrynode;
151 
152  const bool err=
154  xml,
155  name_to_node,
156  defaults,
157  dest,
158  entrynode);
159  CHECK_RETURN(!entrynode.empty());
160 
161  for(std::size_t i=0; !err && i<dest.size(); ++i)
162  {
163  const graphmlt::nodet &n=dest[i];
164 
165  INVARIANT(!n.node_name.empty(), "node should be named");
166  }
167 
168  name_mapt::const_iterator it=name_to_node.find(entrynode);
169  CHECK_RETURN(it != name_to_node.end());
170  entry=it->second;
171 
172  return err;
173 }
174 
176  std::istream &is,
177  graphmlt &dest,
178  graphmlt::node_indext &entry,
179  message_handlert &message_handler)
180 {
181  xmlt xml;
182 
183  if(parse_xml(is, "", message_handler, xml))
184  return true;
185 
186  return build_graph(xml, dest, entry);
187 }
188 
190  const std::string &filename,
191  graphmlt &dest,
192  graphmlt::node_indext &entry,
193  message_handlert &message_handler)
194 {
195  xmlt xml;
196 
197  if(parse_xml(filename, message_handler, xml))
198  return true;
199 
200  return build_graph(xml, dest, entry);
201 }
202 
203 bool write_graphml(const graphmlt &src, std::ostream &os)
204 {
205  xmlt graphml("graphml");
206  graphml.set_attribute(
207  "xmlns:xsi",
208  "http://www.w3.org/2001/XMLSchema-instance");
209  graphml.set_attribute(
210  "xmlns",
211  "http://graphml.graphdrawing.org/xmlns");
212 
213  // <key attr.name="originFileName" attr.type="string" for="edge"
214  // id="originfile">
215  // <default>"&lt;command-line&gt;"</default>
216  // </key>
217  {
218  xmlt &key=graphml.new_element("key");
219  key.set_attribute("attr.name", "originFileName");
220  key.set_attribute("attr.type", "string");
221  key.set_attribute("for", "edge");
222  key.set_attribute("id", "originfile");
223 
224  if(src.key_values.find("programfile")!=src.key_values.end())
225  key.new_element("default").data=src.key_values.at("programfile");
226  else
227  key.new_element("default").data="<command-line>";
228  }
229 
230  // <key attr.name="invariant" attr.type="string" for="node" id="invariant"/>
231  {
232  xmlt &key=graphml.new_element("key");
233  key.set_attribute("attr.name", "invariant");
234  key.set_attribute("attr.type", "string");
235  key.set_attribute("for", "node");
236  key.set_attribute("id", "invariant");
237  }
238 
239  // <key attr.name="invariant.scope" attr.type="string" for="node"
240  // id="invariant.scope"/>
241  {
242  xmlt &key=graphml.new_element("key");
243  key.set_attribute("attr.name", "invariant.scope");
244  key.set_attribute("attr.type", "string");
245  key.set_attribute("for", "node");
246  key.set_attribute("id", "invariant.scope");
247  }
248 
249  // <key attr.name="isViolationNode" attr.type="boolean" for="node"
250  // id="violation">
251  // <default>false</default>
252  // </key>
253  {
254  xmlt &key=graphml.new_element("key");
255  key.set_attribute("attr.name", "isViolationNode");
256  key.set_attribute("attr.type", "boolean");
257  key.set_attribute("for", "node");
258  key.set_attribute("id", "violation");
259 
260  key.new_element("default").data="false";
261  }
262 
263  // <key attr.name="isEntryNode" attr.type="boolean" for="node" id="entry">
264  // <default>false</default>
265  // </key>
266  {
267  xmlt &key=graphml.new_element("key");
268  key.set_attribute("attr.name", "isEntryNode");
269  key.set_attribute("attr.type", "boolean");
270  key.set_attribute("for", "node");
271  key.set_attribute("id", "entry");
272 
273  key.new_element("default").data="false";
274  }
275 
276  // <key attr.name="isSinkNode" attr.type="boolean" for="node" id="sink">
277  // <default>false</default>
278  // </key>
279  {
280  xmlt &key=graphml.new_element("key");
281  key.set_attribute("attr.name", "isSinkNode");
282  key.set_attribute("attr.type", "boolean");
283  key.set_attribute("for", "node");
284  key.set_attribute("id", "sink");
285 
286  key.new_element("default").data="false";
287  }
288 
289  // <key attr.name="enterLoopHead" attr.type="boolean" for="edge"
290  // id="enterLoopHead">
291  // <default>false</default>
292  // </key>
293  {
294  xmlt &key=graphml.new_element("key");
295  key.set_attribute("attr.name", "enterLoopHead");
296  key.set_attribute("attr.type", "boolean");
297  key.set_attribute("for", "edge");
298  key.set_attribute("id", "enterLoopHead");
299 
300  key.new_element("default").data="false";
301  }
302 
303  // <key attr.name="cyclehead" attr.type="boolean" for="node"
304  // id="cyclehead">
305  // <default>false</default>
306  // </key>
307  {
308  xmlt &key = graphml.new_element("key");
309  key.set_attribute("attr.name", "cyclehead");
310  key.set_attribute("attr.type", "boolean");
311  key.set_attribute("for", "node");
312  key.set_attribute("id", "cyclehead");
313 
314  key.new_element("default").data = "false";
315  }
316 
317  // <key attr.name="threadId" attr.type="string" for="edge" id="threadId"/>
318  {
319  xmlt &key=graphml.new_element("key");
320  key.set_attribute("attr.name", "threadId");
321  key.set_attribute("attr.type", "int");
322  key.set_attribute("for", "edge");
323  key.set_attribute("id", "threadId");
324 
325  key.new_element("default").data = "0";
326  }
327 
328  // <key attr.name="createThread" attr.type="string"
329  // for="edge" id="createThread"/>
330  {
331  xmlt &key = graphml.new_element("key");
332  key.set_attribute("attr.name", "createThread");
333  key.set_attribute("attr.type", "int");
334  key.set_attribute("for", "edge");
335  key.set_attribute("id", "createThread");
336 
337  key.new_element("default").data="0";
338  }
339 
340  // <key attr.name="sourcecodeLanguage" attr.type="string" for="graph"
341  // id="sourcecodelang"/>
342  {
343  xmlt &key=graphml.new_element("key");
344  key.set_attribute("attr.name", "sourcecodeLanguage");
345  key.set_attribute("attr.type", "string");
346  key.set_attribute("for", "graph");
347  key.set_attribute("id", "sourcecodelang");
348  }
349 
350  // <key attr.name="programFile" attr.type="string" for="graph"
351  // id="programfile"/>
352  {
353  xmlt &key=graphml.new_element("key");
354  key.set_attribute("attr.name", "programFile");
355  key.set_attribute("attr.type", "string");
356  key.set_attribute("for", "graph");
357  key.set_attribute("id", "programfile");
358  }
359 
360  // <key attr.name="programHash" attr.type="string" for="graph"
361  // id="programhash"/>
362  {
363  xmlt &key=graphml.new_element("key");
364  key.set_attribute("attr.name", "programHash");
365  key.set_attribute("attr.type", "string");
366  key.set_attribute("for", "graph");
367  key.set_attribute("id", "programhash");
368  }
369 
370  // <key attr.name="specification" attr.type="string" for="graph"
371  // id="specification"/>
372  {
373  xmlt &key=graphml.new_element("key");
374  key.set_attribute("attr.name", "specification");
375  key.set_attribute("attr.type", "string");
376  key.set_attribute("for", "graph");
377  key.set_attribute("id", "specification");
378  }
379 
380  // <key attr.name="architecture" attr.type="string" for="graph"
381  // id="architecture"/>
382  {
383  xmlt &key=graphml.new_element("key");
384  key.set_attribute("attr.name", "architecture");
385  key.set_attribute("attr.type", "string");
386  key.set_attribute("for", "graph");
387  key.set_attribute("id", "architecture");
388  }
389 
390  // <key attr.name="producer" attr.type="string" for="graph"
391  // id="producer"/>
392  {
393  xmlt &key=graphml.new_element("key");
394  key.set_attribute("attr.name", "producer");
395  key.set_attribute("attr.type", "string");
396  key.set_attribute("for", "graph");
397  key.set_attribute("id", "producer");
398  }
399 
400  // <key attr.name="creationtime" attr.type="string" for="graph"
401  // id="creationtime"/>
402  {
403  xmlt &key = graphml.new_element("key");
404  key.set_attribute("attr.name", "creationtime");
405  key.set_attribute("attr.type", "string");
406  key.set_attribute("for", "graph");
407  key.set_attribute("id", "creationtime");
408  }
409 
410  // <key attr.name="startline" attr.type="int" for="edge" id="startline"/>
411  {
412  xmlt &key=graphml.new_element("key");
413  key.set_attribute("attr.name", "startline");
414  key.set_attribute("attr.type", "int");
415  key.set_attribute("for", "edge");
416  key.set_attribute("id", "startline");
417  }
418 
419  // <key attr.name="control" attr.type="string" for="edge" id="control"/>
420  {
421  xmlt &key=graphml.new_element("key");
422  key.set_attribute("attr.name", "control");
423  key.set_attribute("attr.type", "string");
424  key.set_attribute("for", "edge");
425  key.set_attribute("id", "control");
426  }
427 
428  // <key attr.name="assumption" attr.type="string" for="edge" id="assumption"/>
429  {
430  xmlt &key=graphml.new_element("key");
431  key.set_attribute("attr.name", "assumption");
432  key.set_attribute("attr.type", "string");
433  key.set_attribute("for", "edge");
434  key.set_attribute("id", "assumption");
435  }
436 
437  // <key attr.name="assumption.resultfunction" attr.type="string" for="edge"
438  // id="assumption.resultfunction"/>
439  {
440  xmlt &key=graphml.new_element("key");
441  key.set_attribute("attr.name", "assumption.resultfunction");
442  key.set_attribute("attr.type", "string");
443  key.set_attribute("for", "edge");
444  key.set_attribute("id", "assumption.resultfunction");
445  }
446 
447  // <key attr.name="assumption.scope" attr.type="string" for="edge"
448  // id="assumption.scope"/>
449  {
450  xmlt &key=graphml.new_element("key");
451  key.set_attribute("attr.name", "assumption.scope");
452  key.set_attribute("attr.type", "string");
453  key.set_attribute("for", "edge");
454  key.set_attribute("id", "assumption.scope");
455  }
456 
457  // <key attr.name="enterFunction" attr.type="string" for="edge"
458  // id="enterFunction"/>
459  {
460  xmlt &key=graphml.new_element("key");
461  key.set_attribute("attr.name", "enterFunction");
462  key.set_attribute("attr.type", "string");
463  key.set_attribute("for", "edge");
464  key.set_attribute("id", "enterFunction");
465  }
466 
467  // <key attr.name="returnFromFunction" attr.type="string" for="edge"
468  // id="returnFrom"/>
469  {
470  xmlt &key=graphml.new_element("key");
471  key.set_attribute("attr.name", "returnFromFunction");
472  key.set_attribute("attr.type", "string");
473  key.set_attribute("for", "edge");
474  key.set_attribute("id", "returnFrom");
475  }
476 
477  // <key attr.name="witness-type" attr.type="string" for="graph"
478  // id="witness-type"/>
479  {
480  xmlt &key=graphml.new_element("key");
481  key.set_attribute("attr.name", "witness-type");
482  key.set_attribute("attr.type", "string");
483  key.set_attribute("for", "graph");
484  key.set_attribute("id", "witness-type");
485  }
486 
487  xmlt &graph=graphml.new_element("graph");
488  graph.set_attribute("edgedefault", "directed");
489 
490  for(const auto &kv : src.key_values)
491  {
492  xmlt &data=graph.new_element("data");
493  data.set_attribute("key", kv.first);
494  data.data=kv.second;
495  }
496 
497  bool entry_done=false;
498  for(graphmlt::node_indext i=0; i<src.size(); ++i)
499  {
500  const graphmlt::nodet &n=src[i];
501 
502  // <node id="A12"/>
503  xmlt &node=graph.new_element("node");
504  node.set_attribute("id", n.node_name);
505 
506  // <node id="A1">
507  // <data key="entry">true</data>
508  // </node>
509  if(!entry_done && n.node_name!="sink")
510  {
511  xmlt &entry=node.new_element("data");
512  entry.set_attribute("key", "entry");
513  entry.data="true";
514 
515  entry_done=true;
516  }
517 
518  // <node id="A14">
519  // <data key="violation">true</data>
520  // </node>
521  if(n.is_violation)
522  {
523  xmlt &entry=node.new_element("data");
524  entry.set_attribute("key", "violation");
525  entry.data="true";
526  }
527 
528  if(n.has_invariant)
529  {
530  xmlt &val=node.new_element("data");
531  val.set_attribute("key", "invariant");
532  val.data=n.invariant;
533 
534  xmlt &val_s=node.new_element("data");
535  val_s.set_attribute("key", "invariant.scope");
536  val_s.data=n.invariant_scope;
537  }
538 
539  for(graphmlt::edgest::const_iterator
540  e_it=n.out.begin();
541  e_it!=n.out.end();
542  ++e_it)
543  graph.new_element(e_it->second.xml_node);
544  }
545 
546  os << "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n";
547  os << graphml;
548 
549  return !os.good();
550 }
edgest out
Definition: graph.h:42
key_valuest key_values
Definition: graphml.h:67
const edgest & in(node_indext n) const
Definition: graph.h:222
nodet::node_indext node_indext
Definition: graph.h:173
node_indext add_node(arguments &&... values)
Definition: graph.h:180
std::size_t size() const
Definition: graph.h:212
bool empty() const
Definition: graph.h:217
const edgest & out(node_indext n) const
Definition: graph.h:227
Definition: xml.h:21
std::string get_attribute(const std::string &attribute) const
Definition: xml.h:63
void set_attribute(const std::string &attribute, unsigned value)
Definition: xml.cpp:198
xmlt & new_element(const std::string &key)
Definition: xml.h:95
elementst elements
Definition: xml.h:42
std::string data
Definition: xml.h:39
std::string name
Definition: xml.h:39
void err(int eval, const char *fmt,...)
Definition: err.c:13
bool read_graphml(std::istream &is, graphmlt &dest, graphmlt::node_indext &entry, message_handlert &message_handler)
Definition: graphml.cpp:175
static graphmlt::node_indext add_node(const std::string &name, name_mapt &name_to_node, graphmlt &graph)
Definition: graphml.cpp:20
bool write_graphml(const graphmlt &src, std::ostream &os)
Definition: graphml.cpp:203
std::map< std::string, graphmlt::node_indext > name_mapt
Definition: graphml.cpp:18
static bool build_graph(const xmlt &xml, graphmlt &dest, graphmlt::node_indext &entry)
Definition: graphml.cpp:141
static bool build_graph_rec(const xmlt &xml, name_mapt &name_to_node, std::map< std::string, std::map< std::string, std::string > > &defaults, graphmlt &dest, std::string &entrynode)
Definition: graphml.cpp:33
Read/write graphs as GraphML.
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:110
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:525
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:534
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
std::string invariant
Definition: graphml.h:39
bool has_invariant
Definition: graphml.h:38
std::string invariant_scope
Definition: graphml.h:40
bool is_violation
Definition: graphml.h:37
std::string node_name
Definition: graphml.h:34
bool parse_xml(std::istream &in, const std::string &filename, message_handlert &message_handler, xmlt &dest)
Definition: xml_parser.cpp:29