Skip to content

Commit 00b6031

Browse files
tautschnigtautschnig
committed
Hack to make CPAchecker parse graphml concurrency witnesses
This does likely need more work, but at least got us some points in the past.
1 parent 853ce97 commit 00b6031

File tree

4 files changed

+80
-25
lines changed

4 files changed

+80
-25
lines changed

‎regression/cbmc/graphml_witness1/test.desc

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -16,9 +16,6 @@ main.c
1616
<key attr.name="enterLoopHead" attr.type="boolean" for="edge" id="enterLoopHead">
1717
<default>false</default>
1818
</key>
19-
<key attr.name="threadNumber" attr.type="int" for="node" id="thread">
20-
<default>0</default>
21-
</key>
2219
<key attr.name="sourcecodeLanguage" attr.type="string" for="graph" id="sourcecodelang"/>
2320
<key attr.name="programFile" attr.type="string" for="graph" id="programfile"/>
2421
<key attr.name="programHash" attr.type="string" for="graph" id="programhash"/>

‎src/goto-programs/graphml_witness.cpp

Lines changed: 65 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -292,14 +292,61 @@ static bool contains_symbol_prefix(const exprt &expr, const std::string &prefix)
292292
/// counterexample witness
293293
void graphml_witnesst::operator()(const goto_tracet &goto_trace)
294294
{
295+
unsigned int max_thread_idx = 0;
296+
bool trace_has_violation = false;
297+
for(goto_tracet::stepst::const_iterator it = goto_trace.steps.begin();
298+
it != goto_trace.steps.end();
299+
++it)
300+
{
301+
if(it->thread_nr > max_thread_idx)
302+
max_thread_idx = it->thread_nr;
303+
if(it->is_assert() && !it->cond_value)
304+
trace_has_violation = true;
305+
}
306+
295307
graphml.key_values["sourcecodelang"]="C";
296308

297309
const graphmlt::node_indext sink=graphml.add_node();
298310
graphml[sink].node_name="sink";
299-
graphml[sink].thread_nr=0;
300311
graphml[sink].is_violation=false;
301312
graphml[sink].has_invariant=false;
302313

314+
if(max_thread_idx > 0 && trace_has_violation)
315+
{
316+
std::vector<graphmlt::node_indext> nodes;
317+
318+
for(unsigned int i = 0; i <= max_thread_idx + 1; ++i)
319+
{
320+
nodes.push_back(graphml.add_node());
321+
graphml[nodes.back()].node_name = "N" + std::to_string(i);
322+
graphml[nodes.back()].is_violation = i == max_thread_idx + 1;
323+
graphml[nodes.back()].has_invariant = false;
324+
}
325+
326+
for(auto it = nodes.cbegin(); std::next(it) != nodes.cend(); ++it)
327+
{
328+
xmlt edge("edge");
329+
edge.set_attribute("source", graphml[*it].node_name);
330+
edge.set_attribute("target", graphml[*std::next(it)].node_name);
331+
const auto thread_id = std::distance(nodes.cbegin(), it);
332+
xmlt &data = edge.new_element("data");
333+
data.set_attribute("key", "createThread");
334+
data.data = std::to_string(thread_id);
335+
if(thread_id == 0)
336+
{
337+
xmlt &data = edge.new_element("data");
338+
data.set_attribute("key", "enterFunction");
339+
data.data = "main";
340+
}
341+
graphml[*std::next(it)].in[*it].xml_node = edge;
342+
graphml[*it].out[*std::next(it)].xml_node = edge;
343+
}
344+
345+
// we do not provide any further details as CPAchecker does not seem to
346+
// handle more detailed concurrency witnesses
347+
return;
348+
}
349+
303350
// step numbers start at 1
304351
std::vector<std::size_t> step_to_node(goto_trace.steps.size()+1, 0);
305352

@@ -338,14 +385,15 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace)
338385
std::to_string(it->pc->location_number)+"."+std::to_string(it->step_nr);
339386
graphml[node].file=source_location.get_file();
340387
graphml[node].line=source_location.get_line();
341-
graphml[node].thread_nr=it->thread_nr;
342388
graphml[node].is_violation=
343389
it->type==goto_trace_stept::typet::ASSERT && !it->cond_value;
344390
graphml[node].has_invariant=false;
345391

346392
step_to_node[it->step_nr]=node;
347393
}
348394

395+
unsigned thread_id = 0;
396+
349397
// build edges
350398
for(goto_tracet::stepst::const_iterator
351399
it=goto_trace.steps.begin();
@@ -378,6 +426,7 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace)
378426
case goto_trace_stept::typet::ASSIGNMENT:
379427
case goto_trace_stept::typet::ASSERT:
380428
case goto_trace_stept::typet::GOTO:
429+
case goto_trace_stept::typet::SPAWN:
381430
{
382431
xmlt edge(
383432
"edge",
@@ -393,6 +442,10 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace)
393442
xmlt &data_l=edge.new_element("data");
394443
data_l.set_attribute("key", "startline");
395444
data_l.data=id2string(graphml[from].line);
445+
446+
xmlt &data_t=edge.new_element("data");
447+
data_t.set_attribute("key", "threadId");
448+
data_t.data=std::to_string(it->thread_nr);
396449
}
397450

398451
const auto lhs_object = it->get_lhs_object();
@@ -401,11 +454,19 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace)
401454
lhs_object.has_value())
402455
{
403456
const std::string &lhs_id = id2string(lhs_object->get_identifier());
404-
if(
457+
if(lhs_id.find("pthread_create::thread") != std::string::npos)
458+
{
459+
xmlt &data_t = edge.new_element("data");
460+
data_t.set_attribute("key", "createThread");
461+
data_t.data = std::to_string(++thread_id);
462+
}
463+
else if(
405464
!contains_symbol_prefix(
406465
it->full_lhs_value, SYMEX_DYNAMIC_PREFIX "dynamic_object") &&
407466
!contains_symbol_prefix(
408467
it->full_lhs, SYMEX_DYNAMIC_PREFIX "dynamic_object") &&
468+
lhs_id.find("thread") == std::string::npos &&
469+
lhs_id.find("mutex") == std::string::npos &&
409470
(!it->full_lhs_value.is_constant() ||
410471
!it->full_lhs_value.has_operands() ||
411472
!has_prefix(
@@ -448,7 +509,6 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace)
448509
case goto_trace_stept::typet::OUTPUT:
449510
case goto_trace_stept::typet::SHARED_READ:
450511
case goto_trace_stept::typet::SHARED_WRITE:
451-
case goto_trace_stept::typet::SPAWN:
452512
case goto_trace_stept::typet::MEMORY_BARRIER:
453513
case goto_trace_stept::typet::ATOMIC_BEGIN:
454514
case goto_trace_stept::typet::ATOMIC_END:
@@ -470,7 +530,6 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation)
470530

471531
const graphmlt::node_indext sink=graphml.add_node();
472532
graphml[sink].node_name="sink";
473-
graphml[sink].thread_nr=0;
474533
graphml[sink].is_violation=false;
475534
graphml[sink].has_invariant=false;
476535

@@ -516,7 +575,6 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation)
516575
std::to_string(step_nr);
517576
graphml[node].file=source_location.get_file();
518577
graphml[node].line=source_location.get_line();
519-
graphml[node].thread_nr=it->source.thread_nr;
520578
graphml[node].is_violation=false;
521579
graphml[node].has_invariant=false;
522580

@@ -557,6 +615,7 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation)
557615
case goto_trace_stept::typet::ASSIGNMENT:
558616
case goto_trace_stept::typet::ASSERT:
559617
case goto_trace_stept::typet::GOTO:
618+
case goto_trace_stept::typet::SPAWN:
560619
{
561620
xmlt edge(
562621
"edge",
@@ -601,7 +660,6 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation)
601660
case goto_trace_stept::typet::OUTPUT:
602661
case goto_trace_stept::typet::SHARED_READ:
603662
case goto_trace_stept::typet::SHARED_WRITE:
604-
case goto_trace_stept::typet::SPAWN:
605663
case goto_trace_stept::typet::MEMORY_BARRIER:
606664
case goto_trace_stept::typet::ATOMIC_BEGIN:
607665
case goto_trace_stept::typet::ATOMIC_END:

‎src/xmllang/graphml.cpp

Lines changed: 15 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -54,7 +54,6 @@ static bool build_graph_rec(
5454
node.node_name=node_name;
5555
node.is_violation=false;
5656
node.has_invariant=false;
57-
node.thread_nr=0;
5857

5958
for(xmlt::elementst::const_iterator
6059
e_it=xml.elements.begin();
@@ -66,8 +65,6 @@ static bool build_graph_rec(
6665
if(e_it->get_attribute("key")=="violation" &&
6766
e_it->data=="true")
6867
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);
7168
else if(e_it->get_attribute("key")=="entry" &&
7269
e_it->data=="true")
7370
entrynode=node_name;
@@ -324,13 +321,24 @@ bool write_graphml(const graphmlt &src, std::ostream &os)
324321
}
325322

326323
// <key attr.name="threadId" attr.type="string" for="edge" id="threadId"/>
327-
// TODO: format for multi-threaded programs not defined yet
328324
{
329325
xmlt &key=graphml.new_element("key");
330-
key.set_attribute("attr.name", "threadNumber");
326+
key.set_attribute("attr.name", "threadId");
331327
key.set_attribute("attr.type", "int");
332-
key.set_attribute("for", "node");
333-
key.set_attribute("id", "thread");
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");
334342

335343
key.new_element("default").data="0";
336344
}
@@ -503,13 +511,6 @@ bool write_graphml(const graphmlt &src, std::ostream &os)
503511
entry_done=true;
504512
}
505513

506-
if(n.thread_nr!=0)
507-
{
508-
xmlt &entry=node.new_element("data");
509-
entry.set_attribute("key", "threadNumber");
510-
entry.data=std::to_string(n.thread_nr);
511-
}
512-
513514
// <node id="A14">
514515
// <data key="violation">true</data>
515516
// </node>

‎src/xmllang/graphml.h

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -32,7 +32,6 @@ struct xml_graph_nodet:public graph_nodet<xml_edget>
3232
std::string node_name;
3333
irep_idt file;
3434
irep_idt line;
35-
unsigned thread_nr;
3635
bool is_violation;
3736
bool has_invariant;
3837
std::string invariant;

0 commit comments

Comments
 (0)