Concurrency: treat updates to an unknown field as atomic

Writing to an object that is composed of multiple fields is generally
treated in a field-sensitive (and thus: single-field) manner, which had
fixed several issues in handling shared arrays or structs. When the
specific field being updated cannot be determined during symbolic
execution (as is the case with non-const indices into arrays), we update
all fields that make up the full object. Such a full-object update must
then be treated as an atomic operation to avoid losing intermittent
writes performed by other threads.

Fixes: diffblue#123

Author: tautschnig

regression/cbmc-concurrency/array1/main.c

@@ -0,0 +1,19 @@
+int data[2];
+unsigned sync;
+
+void thread()
+{
+  data[sync % 2] = 1;
+  __CPROVER_assert(data[sync % 2] == 1, "1");
+}
+
+int main()
+{
+  unsigned nondet;
+  sync = nondet;
+__CPROVER_ASYNC_1:
+  thread();
+  unsigned sync_value = sync;
+  data[(sync_value + 1) % 2] = 2;
+  __CPROVER_assert(data[(sync_value + 1) % 2] == 2, "2");
+}

regression/cbmc-concurrency/array1/test.desc

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

src/goto-symex/goto_symex.cpp

@@ -117,10 +117,28 @@ void goto_symext::symex_assign(
         return;
     }
 
+    // We may end up reading (and writing) all components of an object composed
+    // of multiple fields. In such cases, we must do so atomically to avoid
+    // overwriting components modified by another thread. Note that this also
+    // implies multiple shared reads on the rhs being treated as atomic.
+    const bool maybe_divisible =
+      lhs.id() == ID_index ||
+      (is_ssa_expr(lhs) &&
+       state.field_sensitivity.is_divisible(to_ssa_expr(lhs), false));
+    const bool need_atomic_section = maybe_divisible &&
+                                     state.threads.size() > 1 &&
+                                     state.atomic_section_id == 0;
+
+    if(need_atomic_section)
+      symex_atomic_begin(state);
+
     exprt::operandst lhs_if_then_else_conditions;
     symex_assignt{
       shadow_memory, state, assignment_type, ns, symex_config, target}
       .assign_rec(lhs, expr_skeletont{}, rhs, lhs_if_then_else_conditions);
+
+    if(need_atomic_section)
+      symex_atomic_end(state);
   }
 }