Skip to content

Commit c217c2e

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 504b7f8 commit c217c2e

File tree

4 files changed

+80
-25
lines changed

4 files changed

+80
-25
lines changed

‎regression/cbmc/graphml_witness1/test.desc

-3
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

+65-7
Original file line numberDiff line numberDiff line change
@@ -304,14 +304,61 @@ static bool contains_symbol_prefix(const exprt &expr, const std::string &prefix)
304304
/// counterexample witness
305305
void graphml_witnesst::operator()(const goto_tracet &goto_trace)
306306
{
307+
unsigned int max_thread_idx = 0;
308+
bool trace_has_violation = false;
309+
for(goto_tracet::stepst::const_iterator it = goto_trace.steps.begin();
310+
it != goto_trace.steps.end();
311+
++it)
312+
{
313+
if(it->thread_nr > max_thread_idx)
314+
max_thread_idx = it->thread_nr;
315+
if(it->is_assert() && !it->cond_value)
316+
trace_has_violation = true;
317+
}
318+
307319
graphml.key_values["sourcecodelang"]="C";
308320

309321
const graphmlt::node_indext sink=graphml.add_node();
310322
graphml[sink].node_name="sink";
311-
graphml[sink].thread_nr=0;
312323
graphml[sink].is_violation=false;
313324
graphml[sink].has_invariant=false;
314325

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

@@ -350,14 +397,15 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace)
350397
std::to_string(it->pc->location_number)+"."+std::to_string(it->step_nr);
351398
graphml[node].file=source_location.get_file();
352399
graphml[node].line=source_location.get_line();
353-
graphml[node].thread_nr=it->thread_nr;
354400
graphml[node].is_violation=
355401
it->type==goto_trace_stept::typet::ASSERT && !it->cond_value;
356402
graphml[node].has_invariant=false;
357403

358404
step_to_node[it->step_nr]=node;
359405
}
360406

407+
unsigned thread_id = 0;
408+
361409
// build edges
362410
for(goto_tracet::stepst::const_iterator
363411
it=goto_trace.steps.begin();
@@ -390,6 +438,7 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace)
390438
case goto_trace_stept::typet::ASSIGNMENT:
391439
case goto_trace_stept::typet::ASSERT:
392440
case goto_trace_stept::typet::GOTO:
441+
case goto_trace_stept::typet::SPAWN:
393442
{
394443
xmlt edge(
395444
"edge",
@@ -405,6 +454,10 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace)
405454
xmlt &data_l=edge.new_element("data");
406455
data_l.set_attribute("key", "startline");
407456
data_l.data=id2string(graphml[from].line);
457+
458+
xmlt &data_t=edge.new_element("data");
459+
data_t.set_attribute("key", "threadId");
460+
data_t.data=std::to_string(it->thread_nr);
408461
}
409462

410463
const auto lhs_object = it->get_lhs_object();
@@ -413,11 +466,19 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace)
413466
lhs_object.has_value())
414467
{
415468
const std::string &lhs_id = id2string(lhs_object->get_identifier());
416-
if(
469+
if(lhs_id.find("pthread_create::thread") != std::string::npos)
470+
{
471+
xmlt &data_t = edge.new_element("data");
472+
data_t.set_attribute("key", "createThread");
473+
data_t.data = std::to_string(++thread_id);
474+
}
475+
else if(
417476
!contains_symbol_prefix(
418477
it->full_lhs_value, SYMEX_DYNAMIC_PREFIX "dynamic_object") &&
419478
!contains_symbol_prefix(
420479
it->full_lhs, SYMEX_DYNAMIC_PREFIX "dynamic_object") &&
480+
lhs_id.find("thread") == std::string::npos &&
481+
lhs_id.find("mutex") == std::string::npos &&
421482
(!it->full_lhs_value.is_constant() ||
422483
!it->full_lhs_value.has_operands() ||
423484
!has_prefix(
@@ -460,7 +521,6 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace)
460521
case goto_trace_stept::typet::OUTPUT:
461522
case goto_trace_stept::typet::SHARED_READ:
462523
case goto_trace_stept::typet::SHARED_WRITE:
463-
case goto_trace_stept::typet::SPAWN:
464524
case goto_trace_stept::typet::MEMORY_BARRIER:
465525
case goto_trace_stept::typet::ATOMIC_BEGIN:
466526
case goto_trace_stept::typet::ATOMIC_END:
@@ -482,7 +542,6 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation)
482542

483543
const graphmlt::node_indext sink=graphml.add_node();
484544
graphml[sink].node_name="sink";
485-
graphml[sink].thread_nr=0;
486545
graphml[sink].is_violation=false;
487546
graphml[sink].has_invariant=false;
488547

@@ -528,7 +587,6 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation)
528587
std::to_string(step_nr);
529588
graphml[node].file=source_location.get_file();
530589
graphml[node].line=source_location.get_line();
531-
graphml[node].thread_nr=it->source.thread_nr;
532590
graphml[node].is_violation=false;
533591
graphml[node].has_invariant=false;
534592

@@ -569,6 +627,7 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation)
569627
case goto_trace_stept::typet::ASSIGNMENT:
570628
case goto_trace_stept::typet::ASSERT:
571629
case goto_trace_stept::typet::GOTO:
630+
case goto_trace_stept::typet::SPAWN:
572631
{
573632
xmlt edge(
574633
"edge",
@@ -613,7 +672,6 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation)
613672
case goto_trace_stept::typet::OUTPUT:
614673
case goto_trace_stept::typet::SHARED_READ:
615674
case goto_trace_stept::typet::SHARED_WRITE:
616-
case goto_trace_stept::typet::SPAWN:
617675
case goto_trace_stept::typet::MEMORY_BARRIER:
618676
case goto_trace_stept::typet::ATOMIC_BEGIN:
619677
case goto_trace_stept::typet::ATOMIC_END:

‎src/xmllang/graphml.cpp

+15-14
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

-1
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)