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

tautschnig · tautschnig · commit 60c6582f6017 · 2025-11-30T18:43:35.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
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
+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
+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/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-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,20 +9,21 @@ 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>
 #include <util/pointer_offset_size.h>
 
+#include <pointer-analysis/add_failed_symbols.h>
 #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 +250,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 +357,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
`@@ -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
`@@ -359,15 +359,13 @@ void field_sensitivityt::field_assignments(`
`359`	`359`	`goto_symex_statet &state,`
`360`	`360`	`const ssa_exprt &lhs,`
`361`	`361`	`const exprt &rhs,`
`362`		`- symex_targett &target,`
`363`		`- bool allow_pointer_unsoundness) const`
	`362`	`+ symex_targett &target) const`
`364`	`363`	`{`
`365`	`364`	`const exprt lhs_fs = get_fields(ns, state, lhs, false);`
`366`	`365`
`367`	`366`	`if(lhs != lhs_fs)`
`368`	`367`	`{`
`369`		`- field_assignments_rec(`
`370`		`- ns, state, lhs_fs, rhs, target, allow_pointer_unsoundness);`
	`368`	`+ field_assignments_rec(ns, state, lhs_fs, rhs, target);`
`371`	`369`	`// Erase the composite symbol from our working state. Note that we need to`
`372`	`370`	`// have it in the propagation table and the value set while doing the field`
`373`	`371`	`// assignments, thus we cannot skip putting it in there above.`
`@@ -388,22 +386,18 @@ void field_sensitivityt::field_assignments(`
`388`	`386`	`/// \param lhs_fs: expanded symbol`
`389`	`387`	`/// \param ssa_rhs: right-hand-side value to assign`
`390`	`388`	`/// \param target: symbolic execution equation store`
`391`		`-/// \param allow_pointer_unsoundness: allow pointer unsoundness`
`392`	`389`	`void field_sensitivityt::field_assignments_rec(`
`393`	`390`	`const namespacet &ns,`
`394`	`391`	`goto_symex_statet &state,`
`395`	`392`	`const exprt &lhs_fs,`
`396`	`393`	`const exprt &ssa_rhs,`
`397`		`- symex_targett &target,`
`398`		`- bool allow_pointer_unsoundness) const`
	`394`	`+ symex_targett &target) const`
`399`	`395`	`{`
`400`	`396`	`if(is_ssa_expr(lhs_fs))`
`401`	`397`	`{`
`402`	`398`	`const ssa_exprt &l1_lhs = to_ssa_expr(lhs_fs);`
`403`	`399`	`const ssa_exprt ssa_lhs =`
`404`		`- state`
`405`		`- .assignment(l1_lhs, ssa_rhs, ns, true, true, allow_pointer_unsoundness)`
`406`		`- .get();`
	`400`	`+ state.assignment(l1_lhs, ssa_rhs, ns, true, true).get();`
`407`	`401`
`408`	`402`	`// do the assignment`
`409`	`403`	`target.assignment(`
`@@ -454,16 +448,10 @@ void field_sensitivityt::field_assignments_rec(`
`454`	`448`	`expr_try_dynamic_cast<field_sensitive_ssa_exprt>(member_lhs))`
`455`	`449`	`{`
`456`	`450`	`field_assignments_rec(`
`457`		`- ns,`
`458`		`- state,`
`459`		`- fs_ssa->get_object_ssa(),`
`460`		`- member_rhs,`
`461`		`- target,`
`462`		`- allow_pointer_unsoundness);`
	`451`	`+ ns, state, fs_ssa->get_object_ssa(), member_rhs, target);`
`463`	`452`	`}`
`464`	`453`
`465`		`- field_assignments_rec(`
`466`		`- ns, state, member_lhs, member_rhs, target, allow_pointer_unsoundness);`
	`454`	`+ field_assignments_rec(ns, state, member_lhs, member_rhs, target);`
`467`	`455`	`++fs_it;`
`468`	`456`	`}`
`469`	`457`	`}`
`@@ -499,16 +487,10 @@ void field_sensitivityt::field_assignments_rec(`
`499`	`487`	`expr_try_dynamic_cast<field_sensitive_ssa_exprt>(member_lhs))`
`500`	`488`	`{`
`501`	`489`	`field_assignments_rec(`
`502`		`- ns,`
`503`		`- state,`
`504`		`- fs_ssa->get_object_ssa(),`
`505`		`- member_rhs,`
`506`		`- target,`
`507`		`- allow_pointer_unsoundness);`
	`490`	`+ ns, state, fs_ssa->get_object_ssa(), member_rhs, target);`
`508`	`491`	`}`
`509`	`492`
`510`		`- field_assignments_rec(`
`511`		`- ns, state, member_lhs, member_rhs, target, allow_pointer_unsoundness);`
	`493`	`+ field_assignments_rec(ns, state, member_lhs, member_rhs, target);`
`512`	`494`	`++fs_it;`
`513`	`495`	`}`
`514`	`496`	`}`
`@@ -540,16 +522,10 @@ void field_sensitivityt::field_assignments_rec(`
`540`	`522`	`expr_try_dynamic_cast<field_sensitive_ssa_exprt>(index_lhs))`
`541`	`523`	`{`
`542`	`524`	`field_assignments_rec(`
`543`		`- ns,`
`544`		`- state,`
`545`		`- fs_ssa->get_object_ssa(),`
`546`		`- index_rhs,`
`547`		`- target,`
`548`		`- allow_pointer_unsoundness);`
	`525`	`+ ns, state, fs_ssa->get_object_ssa(), index_rhs, target);`
`549`	`526`	`}`
`550`	`527`
`551`		`- field_assignments_rec(`
`552`		`- ns, state, index_lhs, index_rhs, target, allow_pointer_unsoundness);`
	`528`	`+ field_assignments_rec(ns, state, index_lhs, index_rhs, target);`
`553`	`529`	`++fs_it;`
`554`	`530`	`}`
`555`	`531`	`}`
`@@ -565,17 +541,10 @@ void field_sensitivityt::field_assignments_rec(`
`565`	`541`	`{`
`566`	`542`	`if(auto fs_ssa = expr_try_dynamic_cast<field_sensitive_ssa_exprt>(*fs_it))`
`567`	`543`	`{`
`568`		`- field_assignments_rec(`
`569`		`- ns,`
`570`		`- state,`
`571`		`- fs_ssa->get_object_ssa(),`
`572`		`- op,`
`573`		`- target,`
`574`		`- allow_pointer_unsoundness);`
	`544`	`+ field_assignments_rec(ns, state, fs_ssa->get_object_ssa(), op, target);`
`575`	`545`	`}`
`576`	`546`
`577`		`- field_assignments_rec(`
`578`		`- ns, state, *fs_it, op, target, allow_pointer_unsoundness);`
	`547`	`+ field_assignments_rec(ns, state, *fs_it, op, target);`
`579`	`548`	`++fs_it;`
`580`	`549`	`}`
`581`	`550`	`}`