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