Concurrency: ensure apply_condition's value is used

goto_statet::apply_condition generates an entry (with fresh L2 index) in
the propagation map with generating an assignment. We did not previously
use the propagation map when handling atomic sections, and thus had a
missing link between values, causing spurious verification failures.

The regression test is based on SV-COMP's
pthread-ext/23_lu-fig2.fixed.c.

There is further room for improvement, as shown in the
KNOWNBUG-regression test. This will be addressed in a separate commit.

Author: tautschnig

regression/cbmc-concurrency/atomic_section_sc7/main.c

@@ -0,0 +1,67 @@
+#include <assert.h>
+
+int start_main = 0;
+int mStartLock = 0;
+int __COUNT__ = 0;
+
+void __VERIFIER_atomic_acquire()
+{
+  __CPROVER_assume(mStartLock == 0);
+  mStartLock = 1;
+}
+
+void __VERIFIER_atomic_release()
+{
+  __CPROVER_assume(mStartLock == 1);
+  mStartLock = 0;
+}
+
+void __VERIFIER_atomic_thr1()
+{
+  if(__COUNT__ == 0)
+  {
+    __COUNT__ = __COUNT__ + 1;
+  }
+  else
+  {
+    assert(0);
+  }
+}
+
+void thr1()
+{
+  __VERIFIER_atomic_acquire();
+  start_main = 1;
+  __VERIFIER_atomic_thr1();
+  __VERIFIER_atomic_release();
+}
+
+void __VERIFIER_atomic_thr2()
+{
+  if(__COUNT__ == 1)
+  {
+    __COUNT__ = __COUNT__ + 1;
+  }
+  else
+  {
+    assert(0);
+  }
+}
+
+void thr2()
+{
+  __CPROVER_assume(start_main != 0);
+  __VERIFIER_atomic_acquire();
+  __VERIFIER_atomic_release();
+  __VERIFIER_atomic_thr2();
+}
+
+int main()
+{
+__CPROVER_ASYNC_1:
+  thr1();
+
+  thr2();
+
+  return 0;
+}

regression/cbmc-concurrency/atomic_section_sc7/test-guard.desc

@@ -0,0 +1,12 @@
+KNOWNBUG
+main.c
+--program-only
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+__COUNT__#\d+ == (1 \+ __COUNT__#\d+|__COUNT__#\d+ \+ 1)
+--
+__COUNT__ is guaranteed to have been read within the atomic section, there
+should not be a need to produce a conditional assignment, and therefore the
+value of __COUNT__ can be constant propagated.

regression/cbmc-concurrency/atomic_section_sc7/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

src/goto-symex/goto_symex_state.cpp

@@ -396,9 +396,9 @@ bool goto_symex_statet::l2_thread_read_encoding(
         guardt g = guard_in_list;
         g-=guard;
         if(g.is_true())
-          // there has already been a write to l1_identifier within
-          // this atomic section under the same guard, or a guard
-          // that implies the current one
+          // There has already been a write to l1_identifier within this atomic
+          // section under the same guard, or a guard implied by the current
+          // one.
           return false;
 
         write_guard |= guard_in_list;
@@ -418,9 +418,8 @@ bool goto_symex_statet::l2_thread_read_encoding(
       guardt g = a_s_read_guard; // copy
       g-=guard;
       if(g.is_true())
-        // there has already been a read l1_identifier within
-        // this atomic section under the same guard, or a guard
-        // that implies the current one
+        // There has already been a read of l1_identifier within this atomic
+        // section under the same guard, or a guard implied by the current one.
         return false;
 
       read_guard |= a_s_read_guard;
@@ -430,20 +429,29 @@ bool goto_symex_statet::l2_thread_read_encoding(
     if(!no_write.op().is_false())
       cond |= guardt{no_write.op(), guard_manager};
 
-    const renamedt<ssa_exprt, L2> l2_true_case = set_indices<L2>(ssa_l1, ns);
+    // It is safe to perform constant propagation in case we have read or
+    // written this object within the atomic section. We must actually do this,
+    // because goto_state::apply_condition may have placed the latest value in
+    // the propagation map without recording an assignment.
+    auto p_it = propagation.find(ssa_l1.get_identifier());
+    const exprt l2_true_case =
+      p_it.has_value() ? *p_it : set_indices<L2>(ssa_l1, ns).get();
 
-    if(a_s_read.second.empty())
-    {
+    if(!cond.is_true())
       level2.increase_generation(l1_identifier, ssa_l1, fresh_l2_name_provider);
+
+    if(a_s_read.second.empty())
       a_s_read.first = level2.latest_index(l1_identifier);
-    }
+
     const renamedt<ssa_exprt, L2> l2_false_case = set_indices<L2>(ssa_l1, ns);
 
     exprt tmp;
     if(cond.is_false())
       tmp = l2_false_case.get();
+    else if(cond.is_true())
+      tmp = l2_true_case;
     else
-      tmp = if_exprt{cond.as_expr(), l2_true_case.get(), l2_false_case.get()};
+      tmp = if_exprt{cond.as_expr(), l2_true_case, l2_false_case.get()};
 
     record_events.push(false);
     ssa_exprt ssa_l2 = assignment(std::move(ssa_l1), tmp, ns, true, true).get();