Fix concurrent traces generated via --trace

regression/cbmc-concurrency/trace1/main.c

@@ -0,0 +1,28 @@
+// #include <pthread.h>
+#include <assert.h>
+
+volatile unsigned x = 0, y = 0;
+volatile unsigned r1 = 0, r2 = 0;
+
+void* thr1(void* arg) {
+  x = 1;
+  r1 = y + 1;
+  return 0;
+}
+
+void* thr2(void* arg) {
+  y = 1;
+  r2 = x + 1;
+  return 0;
+}
+
+int main(){
+  // pthread_t t1, t2;
+  // pthread_create(&t1, NULL, thr1, NULL);
+  // pthread_create(&t2, NULL, thr2, NULL);
+__CPROVER_ASYNC_1: thr1(0);
+__CPROVER_ASYNC_2: thr2(0);
+  assert(r1 != 1 || r2 != 1);
+  return 0;
+}
+

regression/cbmc-concurrency/trace1/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--mm tso --trace
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+^[[:space:]]*r2=1u \(.*\)$
+--
+^warning: ignoring

src/goto-symex/build_goto_trace.cpp

@@ -158,11 +158,17 @@ void build_goto_trace(
 
   mp_integer current_time=0;
 
+  const goto_trace_stept *end_ptr=nullptr;
+  bool end_step_seen=false;
+
   for(symex_target_equationt::SSA_stepst::const_iterator
       it=target.SSA_steps.begin();
-      it!=end_step;
+      it!=target.SSA_steps.end();
       it++)
   {
+    if(it==end_step)
+      end_step_seen=true;
+
     const symex_target_equationt::SSA_stept &SSA_step=*it;
 
     if(prop_conv.l_get(SSA_step.guard_literal)!=tvt(true))
@@ -221,6 +227,8 @@ void build_goto_trace(
     goto_tracet::stepst &steps=time_map[current_time];
     steps.push_back(goto_trace_stept());
     goto_trace_stept &goto_trace_step=steps.back();
+    if(!end_step_seen)
+      end_ptr=&goto_trace_step;
 
     goto_trace_step.thread_nr=SSA_step.source.thread_nr;
     goto_trace_step.pc=SSA_step.source.pc;
@@ -286,6 +294,17 @@ void build_goto_trace(
   for(auto &t_it : time_map)
     goto_trace.steps.splice(goto_trace.steps.end(), t_it.second);
 
+  // cut off the trace at the desired end
+  for(goto_tracet::stepst::iterator
+      s_it1=goto_trace.steps.begin();
+      s_it1!=goto_trace.steps.end();
+      ++s_it1)
+    if(end_step_seen && end_ptr==&(*s_it1))
+    {
+      goto_trace.trim_after(s_it1);
+      break;
+    }
+
   // produce the step numbers
   unsigned step_nr=0;
 
@@ -321,7 +340,7 @@ void build_goto_trace(
       s_it1++)
     if(s_it1->is_assert() && !s_it1->cond_value)
     {
-      goto_trace.steps.erase(++s_it1, goto_trace.steps.end());
+      goto_trace.trim_after(s_it1);
       break;
     }
 }