Skip to content

Commit b686a8f

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 86cd58b commit b686a8f

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
@@ -294,14 +294,61 @@ static bool contains_symbol_prefix(const exprt &expr, const std::string &prefix)
294294
/// counterexample witness
295295
void graphml_witnesst::operator()(const goto_tracet &goto_trace)
296296
{
297+
unsigned int max_thread_idx = 0;
298+
bool trace_has_violation = false;
299+
for(goto_tracet::stepst::const_iterator it = goto_trace.steps.begin();
300+
it != goto_trace.steps.end();
301+
++it)
302+
{
303+
if(it->thread_nr > max_thread_idx)
304+
max_thread_idx = it->thread_nr;
305+
if(it->is_assert() && !it->cond_value)
306+
trace_has_violation = true;
307+
}
308+
297309
graphml.key_values["sourcecodelang"]="C";
298310

299311
const graphmlt::node_indext sink=graphml.add_node();
300312
graphml[sink].node_name="sink";
301-
graphml[sink].thread_nr=0;
302313
graphml[sink].is_violation=false;
303314
graphml[sink].has_invariant=false;
304315

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

@@ -340,14 +387,15 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace)
340387
std::to_string(it->pc->location_number)+"."+std::to_string(it->step_nr);
341388
graphml[node].file=source_location.get_file();
342389
graphml[node].line=source_location.get_line();
343-
graphml[node].thread_nr=it->thread_nr;
344390
graphml[node].is_violation=
345391
it->type==goto_trace_stept::typet::ASSERT && !it->cond_value;
346392
graphml[node].has_invariant=false;
347393

348394
step_to_node[it->step_nr]=node;
349395
}
350396

397+
unsigned thread_id = 0;
398+
351399
// build edges
352400
for(goto_tracet::stepst::const_iterator
353401
it=goto_trace.steps.begin();
@@ -380,6 +428,7 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace)
380428
case goto_trace_stept::typet::ASSIGNMENT:
381429
case goto_trace_stept::typet::ASSERT:
382430
case goto_trace_stept::typet::GOTO:
431+
case goto_trace_stept::typet::SPAWN:
383432
{
384433
xmlt edge(
385434
"edge",
@@ -395,6 +444,10 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace)
395444
xmlt &data_l=edge.new_element("data");
396445
data_l.set_attribute("key", "startline");
397446
data_l.data=id2string(graphml[from].line);
447+
448+
xmlt &data_t=edge.new_element("data");
449+
data_t.set_attribute("key", "threadId");
450+
data_t.data=std::to_string(it->thread_nr);
398451
}
399452

400453
const auto lhs_object = it->get_lhs_object();
@@ -403,11 +456,19 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace)
403456
lhs_object.has_value())
404457
{
405458
const std::string &lhs_id = id2string(lhs_object->get_identifier());
406-
if(
459+
if(lhs_id.find("pthread_create::thread") != std::string::npos)
460+
{
461+
xmlt &data_t = edge.new_element("data");
462+
data_t.set_attribute("key", "createThread");
463+
data_t.data = std::to_string(++thread_id);
464+
}
465+
else if(
407466
!contains_symbol_prefix(
408467
it->full_lhs_value, SYMEX_DYNAMIC_PREFIX "dynamic_object") &&
409468
!contains_symbol_prefix(
410469
it->full_lhs, SYMEX_DYNAMIC_PREFIX "dynamic_object") &&
470+
lhs_id.find("thread") == std::string::npos &&
471+
lhs_id.find("mutex") == std::string::npos &&
411472
(!it->full_lhs_value.is_constant() ||
412473
!it->full_lhs_value.has_operands() ||
413474
!has_prefix(
@@ -450,7 +511,6 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace)
450511
case goto_trace_stept::typet::OUTPUT:
451512
case goto_trace_stept::typet::SHARED_READ:
452513
case goto_trace_stept::typet::SHARED_WRITE:
453-
case goto_trace_stept::typet::SPAWN:
454514
case goto_trace_stept::typet::MEMORY_BARRIER:
455515
case goto_trace_stept::typet::ATOMIC_BEGIN:
456516
case goto_trace_stept::typet::ATOMIC_END:
@@ -472,7 +532,6 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation)
472532

473533
const graphmlt::node_indext sink=graphml.add_node();
474534
graphml[sink].node_name="sink";
475-
graphml[sink].thread_nr=0;
476535
graphml[sink].is_violation=false;
477536
graphml[sink].has_invariant=false;
478537

@@ -518,7 +577,6 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation)
518577
std::to_string(step_nr);
519578
graphml[node].file=source_location.get_file();
520579
graphml[node].line=source_location.get_line();
521-
graphml[node].thread_nr=it->source.thread_nr;
522580
graphml[node].is_violation=false;
523581
graphml[node].has_invariant=false;
524582

@@ -559,6 +617,7 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation)
559617
case goto_trace_stept::typet::ASSIGNMENT:
560618
case goto_trace_stept::typet::ASSERT:
561619
case goto_trace_stept::typet::GOTO:
620+
case goto_trace_stept::typet::SPAWN:
562621
{
563622
xmlt edge(
564623
"edge",
@@ -603,7 +662,6 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation)
603662
case goto_trace_stept::typet::OUTPUT:
604663
case goto_trace_stept::typet::SHARED_READ:
605664
case goto_trace_stept::typet::SHARED_WRITE:
606-
case goto_trace_stept::typet::SPAWN:
607665
case goto_trace_stept::typet::MEMORY_BARRIER:
608666
case goto_trace_stept::typet::ATOMIC_BEGIN:
609667
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)