goto-symex/concurrency: limit unsoundness-abort to dereferencing shared pointers

tautschnig · tautschnig · commit aa610abfbe7d · 2025-11-30T20:12:29.000Z
Reading and writing pointers is not not itself unsound, only the interaction with value sets may cause unsound results. Hence, do not reject programs that never dereference a shared pointer. Fixes: #8714 Fixes: #7957
diff --git a/regression/book-examples/account/C10.desc b/regression/book-examples/account/C10.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 account.c
 
 ^EXIT=10$
diff --git a/regression/cbmc-concurrency/dirty_local1/test.desc b/regression/cbmc-concurrency/dirty_local1/test.desc
@@ -1,8 +1,8 @@
 CORE
 main.c
 --no-standard-checks
-^EXIT=10$
+pointer handling for concurrency is unsound
+^EXIT=6$
 ^SIGNAL=0$
-^VERIFICATION FAILED$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-concurrency/global_pointer1/detect_unsoundness.desc b/regression/cbmc-concurrency/global_pointer1/detect_unsoundness.desc
@@ -0,0 +1,8 @@
+CORE pthread
+main.c
+
+pointer handling for concurrency is unsound
+^EXIT=6$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/regression/cbmc-concurrency/global_pointer1/main.c b/regression/cbmc-concurrency/global_pointer1/main.c
@@ -12,7 +12,9 @@ void *thread1(void * arg)
 void *thread2(void *arg)
 {
   assert(v == &g);
+#ifndef NO_DEREF
   *v = 1;
+#endif
 }
 
 int main()
@@ -26,7 +28,9 @@ int main()
   pthread_join(t2, 0);
 
   assert(v == &g);
+#ifndef NO_DEREF
   assert(*v == 1);
+#endif
 
   return 0;
 }
diff --git a/regression/cbmc-concurrency/global_pointer1/no_deref.desc b/regression/cbmc-concurrency/global_pointer1/no_deref.desc
@@ -0,0 +1,11 @@
+KNOWNBUG pthread
+main.c
+-DNO_DEREF
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Simplification with value sets causes unsound results despite the absence of
+dereferencing.
diff --git a/regression/cbmc-concurrency/global_pointer1/test.desc b/regression/cbmc-concurrency/global_pointer1/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+KNOWNBUG pthread
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-concurrency/malloc1/test.desc b/regression/cbmc-concurrency/malloc1/test.desc
@@ -1,8 +1,8 @@
 CORE
 main.c
 --no-malloc-may-fail
-^EXIT=0$
+pointer handling for concurrency is unsound
+^EXIT=6$
 ^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-concurrency/malloc2/test.desc b/regression/cbmc-concurrency/malloc2/test.desc
@@ -1,8 +1,8 @@
 CORE
 main.c
 --no-malloc-may-fail
-^EXIT=0$
+pointer handling for concurrency is unsound
+^EXIT=6$
 ^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-concurrency/thread_chain_posix2/test.desc b/regression/cbmc-concurrency/thread_chain_posix2/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG pthread
+CORE pthread
 main.c
 -D_ENABLE_CHAIN_ --unwind 2
 ^EXIT=0$
diff --git a/regression/cbmc-concurrency/thread_chain_posix3/test.desc b/regression/cbmc-concurrency/thread_chain_posix3/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG pthread
+CORE pthread
 main.c
 -D_ENABLE_CHAIN_ -D_SANITY_CHECK_ --unwind 2
 ^EXIT=10$
diff --git a/regression/cbmc-library/realloc-03/test.desc b/regression/cbmc-library/realloc-03/test.desc
@@ -1,12 +1,8 @@
 CORE
 main.c
-
-^EXIT=6$
+--no-malloc-may-fail
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
 ^SIGNAL=0$
-pointer handling for concurrency is unsound
 --
 ^warning: ignoring
---
-The test uses "__CPROVER_ASYNC_1:" and the async-called function foo does
-pointer operations over allocated memory - which is not handled in a sound way
-in CBMC.
diff --git a/src/goto-symex/field_sensitivity.cpp b/src/goto-symex/field_sensitivity.cpp
@@ -359,15 +359,13 @@ void field_sensitivityt::field_assignments(
   goto_symex_statet &state,
   const ssa_exprt &lhs,
   const exprt &rhs,
-  symex_targett &target,
-  bool allow_pointer_unsoundness) const
+  symex_targett &target) const
 {
   const exprt lhs_fs = get_fields(ns, state, lhs, false);
 
   if(lhs != lhs_fs)
   {
-    field_assignments_rec(
-      ns, state, lhs_fs, rhs, target, allow_pointer_unsoundness);
+    field_assignments_rec(ns, state, lhs_fs, rhs, target);
     // Erase the composite symbol from our working state. Note that we need to
     // have it in the propagation table and the value set while doing the field
     // assignments, thus we cannot skip putting it in there above.
@@ -388,22 +386,18 @@ void field_sensitivityt::field_assignments(
 /// \param lhs_fs: expanded symbol
 /// \param ssa_rhs: right-hand-side value to assign
 /// \param target: symbolic execution equation store
-/// \param allow_pointer_unsoundness: allow pointer unsoundness
 void field_sensitivityt::field_assignments_rec(
   const namespacet &ns,
   goto_symex_statet &state,
   const exprt &lhs_fs,
   const exprt &ssa_rhs,
-  symex_targett &target,
-  bool allow_pointer_unsoundness) const
+  symex_targett &target) const
 {
   if(is_ssa_expr(lhs_fs))
   {
     const ssa_exprt &l1_lhs = to_ssa_expr(lhs_fs);
     const ssa_exprt ssa_lhs =
-      state
-        .assignment(l1_lhs, ssa_rhs, ns, true, true, allow_pointer_unsoundness)
-        .get();
+      state.assignment(l1_lhs, ssa_rhs, ns, true, true).get();
 
     // do the assignment
     target.assignment(
@@ -454,16 +448,10 @@ void field_sensitivityt::field_assignments_rec(
           expr_try_dynamic_cast<field_sensitive_ssa_exprt>(member_lhs))
       {
         field_assignments_rec(
-          ns,
-          state,
-          fs_ssa->get_object_ssa(),
-          member_rhs,
-          target,
-          allow_pointer_unsoundness);
+          ns, state, fs_ssa->get_object_ssa(), member_rhs, target);
       }
 
-      field_assignments_rec(
-        ns, state, member_lhs, member_rhs, target, allow_pointer_unsoundness);
+      field_assignments_rec(ns, state, member_lhs, member_rhs, target);
       ++fs_it;
     }
   }
@@ -499,16 +487,10 @@ void field_sensitivityt::field_assignments_rec(
           expr_try_dynamic_cast<field_sensitive_ssa_exprt>(member_lhs))
       {
         field_assignments_rec(
-          ns,
-          state,
-          fs_ssa->get_object_ssa(),
-          member_rhs,
-          target,
-          allow_pointer_unsoundness);
+          ns, state, fs_ssa->get_object_ssa(), member_rhs, target);
       }
 
-      field_assignments_rec(
-        ns, state, member_lhs, member_rhs, target, allow_pointer_unsoundness);
+      field_assignments_rec(ns, state, member_lhs, member_rhs, target);
       ++fs_it;
     }
   }
@@ -540,16 +522,10 @@ void field_sensitivityt::field_assignments_rec(
           expr_try_dynamic_cast<field_sensitive_ssa_exprt>(index_lhs))
       {
         field_assignments_rec(
-          ns,
-          state,
-          fs_ssa->get_object_ssa(),
-          index_rhs,
-          target,
-          allow_pointer_unsoundness);
+          ns, state, fs_ssa->get_object_ssa(), index_rhs, target);
       }
 
-      field_assignments_rec(
-        ns, state, index_lhs, index_rhs, target, allow_pointer_unsoundness);
+      field_assignments_rec(ns, state, index_lhs, index_rhs, target);
       ++fs_it;
     }
   }
@@ -565,17 +541,10 @@ void field_sensitivityt::field_assignments_rec(
     {
       if(auto fs_ssa = expr_try_dynamic_cast<field_sensitive_ssa_exprt>(*fs_it))
       {
-        field_assignments_rec(
-          ns,
-          state,
-          fs_ssa->get_object_ssa(),
-          op,
-          target,
-          allow_pointer_unsoundness);
+        field_assignments_rec(ns, state, fs_ssa->get_object_ssa(), op, target);
       }
 
-      field_assignments_rec(
-        ns, state, *fs_it, op, target, allow_pointer_unsoundness);
+      field_assignments_rec(ns, state, *fs_it, op, target);
       ++fs_it;
     }
   }
diff --git a/src/goto-symex/field_sensitivity.h b/src/goto-symex/field_sensitivity.h
@@ -142,14 +142,12 @@ class field_sensitivityt
   /// \param rhs: right-hand-side value that was used in the preceding update of
   ///   the full object
   /// \param target: symbolic execution equation store
-  /// \param allow_pointer_unsoundness: allow pointer unsoundness
   void field_assignments(
     const namespacet &ns,
     goto_symex_statet &state,
     const ssa_exprt &lhs,
     const exprt &rhs,
-    symex_targett &target,
-    bool allow_pointer_unsoundness) const;
+    symex_targett &target) const;
 
   /// Turn an expression \p expr into a field-sensitive SSA expression.
   /// Field-sensitive SSA expressions have individual symbols for each
@@ -215,8 +213,7 @@ class field_sensitivityt
     goto_symex_statet &state,
     const exprt &lhs_fs,
     const exprt &ssa_rhs,
-    symex_targett &target,
-    bool allow_pointer_unsoundness) const;
+    symex_targett &target) const;
 
   [[nodiscard]] exprt simplify_opt(
     exprt e,
diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp
@@ -79,8 +79,7 @@ renamedt<ssa_exprt, L2> goto_symex_statet::assignment(
   const exprt &rhs, // L2
   const namespacet &ns,
   bool rhs_is_simplified,
-  bool record_value,
-  bool allow_pointer_unsoundness)
+  bool record_value)
 {
   // identifier should be l0 or l1, make sure it's l1
   lhs = rename_ssa<L1>(std::move(lhs), ns).get();
@@ -110,11 +109,6 @@ renamedt<ssa_exprt, L2> goto_symex_statet::assignment(
     DATA_INVARIANT(!check_renaming(rhs), "rhs renaming failed on l2");
   }
 
-  // see #305 on GitHub for a simple example and possible discussion
-  if(is_shared && lhs.type().id() == ID_pointer && !allow_pointer_unsoundness)
-    throw unsupported_operation_exceptiont(
-      "pointer handling for concurrency is unsound");
-
   // Update constant propagation map -- the RHS is L2
   if(!is_shared && record_value && goto_symex_can_forward_propagatet(ns)(rhs))
   {
diff --git a/src/goto-symex/goto_symex_state.h b/src/goto-symex/goto_symex_state.h
@@ -116,8 +116,7 @@ class goto_symex_statet final : public goto_statet
     const exprt &rhs, // L2
     const namespacet &ns,
     bool rhs_is_simplified,
-    bool record_value,
-    bool allow_pointer_unsoundness = false);
+    bool record_value);
 
   field_sensitivityt field_sensitivity;
 
diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp
@@ -217,8 +217,7 @@ void symex_assignt::assign_non_struct_symbol(
                                assignment.rhs,
                                ns,
                                symex_config.simplify_opt,
-                               symex_config.constant_propagation,
-                               symex_config.allow_pointer_unsoundness)
+                               symex_config.constant_propagation)
                              .get();
 
   state.record_events.push(false);
@@ -254,12 +253,7 @@ void symex_assignt::assign_non_struct_symbol(
   {
     // Split composite symbol lhs into its components
     state.field_sensitivity.field_assignments(
-      ns,
-      state,
-      l1_lhs,
-      assignment.rhs,
-      target,
-      symex_config.allow_pointer_unsoundness);
+      ns, state, l1_lhs, assignment.rhs, target);
   }
 }
 
diff --git a/src/goto-symex/symex_dereference.cpp b/src/goto-symex/symex_dereference.cpp
@@ -9,12 +9,11 @@ Author: Daniel Kroening, kroening@kroening.com
 /// \file
 /// Symbolic Execution of ANSI-C
 
-#include "goto_symex.h"
-
 #include <util/arith_tools.h>
 #include <util/byte_operators.h>
 #include <util/c_types.h>
 #include <util/exception_utils.h>
+#include <util/expr_iterator.h>
 #include <util/expr_util.h>
 #include <util/fresh_symbol.h>
 #include <util/invariant.h>
@@ -23,6 +22,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <pointer-analysis/value_set_dereference.h>
 
 #include "expr_skeleton.h"
+#include "goto_symex.h"
 #include "path_storage.h"
 #include "symex_assign.h"
 #include "symex_dereference_state.h"
@@ -249,6 +249,41 @@ goto_symext::cache_dereference(exprt &dereference_result, statet &state)
   return cache_symbol_expr;
 }
 
+/// Inspect \p expr to confirm that it can be safely dereferenced even in a
+/// concurrent setting. Uses \p ns and \p dirty to identify potentially-shared
+/// objects.
+static void check_concurrency_soundness(
+  const exprt &expr,
+  const incremental_dirtyt &dirty,
+  const namespacet &ns)
+{
+  // Make sure we are not trying to dereference a shared pointer, as this may be
+  // unsound: see #305 on GitHub for a simple example and possible discussion.
+  for(auto it = expr.depth_cbegin(); it != expr.depth_cend(); /* no ++it */)
+  {
+    if(it->id() == ID_address_of)
+    {
+      it.next_sibling_or_parent();
+      continue;
+    }
+    else if(auto sym_expr = expr_try_dynamic_cast<symbol_exprt>(*it))
+    {
+      const irep_idt obj_name = is_ssa_expr(*sym_expr)
+                                  ? to_ssa_expr(*sym_expr).get_object_name()
+                                  : sym_expr->get_identifier();
+      if(
+        obj_name != goto_symex_statet::guard_identifier() &&
+        (ns.lookup(obj_name).is_shared() || dirty(obj_name)))
+      {
+        throw unsupported_operation_exceptiont(
+          "pointer handling for concurrency is unsound: " +
+          id2string(obj_name));
+      }
+    }
+    ++it;
+  }
+}
+
 /// If \p expr is a \ref dereference_exprt, replace it with explicit references
 /// to the objects it may point to. Otherwise recursively apply this function to
 /// \p expr's operands, with special cases for address-of (handled by \ref
@@ -321,6 +356,9 @@ void goto_symext::dereference_rec(
 
     tmp1 = state.field_sensitivity.apply(ns, state, std::move(tmp1), false);
 
+    if(state.threads.size() > 1 && !symex_config.allow_pointer_unsoundness)
+      check_concurrency_soundness(tmp1, path_storage.dirty, ns);
+
     // we need to set up some elaborate call-backs
     symex_dereference_statet symex_dereference_state(state, ns);
 
diff --git a/unit/goto-symex/goto_symex_state.cpp b/unit/goto-symex/goto_symex_state.cpp

Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-KNOWNBUG`
	`1`	`+CORE`
`2`	`2`	`account.c`
`3`	`3`
`4`	`4`	`^EXIT=10$`
Original file line number	Diff line number	Diff line change
`@@ -12,7 +12,9 @@ void thread1(void arg)`
`12`	`12`	`void thread2(void arg)`
`13`	`13`	`{`
`14`	`14`	`assert(v == &g);`
	`15`	`+#ifndef NO_DEREF`
`15`	`16`	`*v = 1;`
	`17`	`+#endif`
`16`	`18`	`}`
`17`	`19`
`18`	`20`	`int main()`
`@@ -26,7 +28,9 @@ int main()`
`26`	`28`	`pthread_join(t2, 0);`
`27`	`29`
`28`	`30`	`assert(v == &g);`
	`31`	`+#ifndef NO_DEREF`
`29`	`32`	`assert(*v == 1);`
	`33`	`+#endif`
`30`	`34`
`31`	`35`	`return 0;`
`32`	`36`	`}`
Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-KNOWNBUG`
	`1`	`+KNOWNBUG pthread`
`2`	`2`	`main.c`
`3`	`3`
`4`	`4`	`^EXIT=0$`
Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-KNOWNBUG pthread`
	`1`	`+CORE pthread`
`2`	`2`	`main.c`
`3`	`3`	`-D_ENABLE_CHAIN_ --unwind 2`
`4`	`4`	`^EXIT=0$`