CBMC: /home/runner/work/cbmc/cbmc/src/xmllang/graphml.cpp Source File

CBMC
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 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,
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,
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
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
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
111 *e_it,
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")
126 e_it->data;
127 }
128 else if(xml.name=="data")
129 {
130 // ignored
131 }
132 else
133 {
135 return true;
136 }
137
138 return false;
139}
140
141 static bool build_graph(
142 const xmlt &xml,
143 graphmlt &dest,
145{
146 PRECONDITION(dest.empty());
147
149 std::map<std::string, std::map<std::string, std::string> > defaults;
150 std::string entrynode;
151
152 const bool err=
154 xml,
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,
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,
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 // Only add invariant.scope if it's not empty
535 if(!n.invariant_scope.empty())
536 {
537 xmlt &val_s = node.new_element("data");
538 val_s.set_attribute("key", "invariant.scope");
539 val_s.data = n.invariant_scope;
540 }
541 }
542
543 for(graphmlt::edgest::const_iterator
544 e_it=n.out.begin();
545 e_it!=n.out.end();
546 ++e_it)
547 graph.new_element(e_it->second.xml_node);
548 }
549
550 os << "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n";
551 os << graphml;
552
553 return !os.good();
554}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:566
key_valuest key_values
Definition graphml.h:67
nodet::node_indext node_indext
Definition graph.h:173
const edgest & out(node_indext n) const
Definition graph.h:227
node_indext add_node(arguments &&... values)
Definition graph.h:180
const edgest & in(node_indext n) const
Definition graph.h:222
std::size_t size() const
Definition graph.h:212
bool empty() const
Definition graph.h:217
Definition message.h:27
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
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
Definition graphml.h:30
bool has_invariant
Definition graphml.h:38
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

AltStyle によって変換されたページ (->オリジナル) /