Merge pull request #5683 from tautschnig/atomic-section

Concurrency: ensure apply_condition's value is used

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

@@ -395,9 +395,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;
@@ -417,9 +417,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;
@@ -429,20 +428,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();