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