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