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