From f5b35b4805330263c7fbc0849f2324622033ba9f Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 9 Feb 2021 00:54:07 +0000
Subject: [PATCH] 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: #123
---
 regression/cbmc-concurrency/array1/main.c    | 19 +++++++++++++++++++
 regression/cbmc-concurrency/array1/test.desc |  8 ++++++++
 src/goto-symex/goto_symex.cpp                | 18 ++++++++++++++++++
 3 files changed, 45 insertions(+)
 create mode 100644 regression/cbmc-concurrency/array1/main.c
 create mode 100644 regression/cbmc-concurrency/array1/test.desc

diff --git a/regression/cbmc-concurrency/array1/main.c b/regression/cbmc-concurrency/array1/main.c
new file mode 100644
index 00000000000..8574bbd66ff
--- /dev/null
+++ b/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");
+}
diff --git a/regression/cbmc-concurrency/array1/test.desc b/regression/cbmc-concurrency/array1/test.desc
new file mode 100644
index 00000000000..9efefbc7362
--- /dev/null
+++ b/regression/cbmc-concurrency/array1/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/src/goto-symex/goto_symex.cpp b/src/goto-symex/goto_symex.cpp
index 316a2dd5ace..9fff87a639d 100644
--- a/src/goto-symex/goto_symex.cpp
+++ b/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);
   }
 }