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

tautschnig · tautschnig · commit 243a31b97229 · 2025-12-01T17:29:23.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 no-new-smt gcc-only
 account.c
 
 ^EXIT=10$
diff --git a/regression/cbmc-concurrency/CMakeLists.txt b/regression/cbmc-concurrency/CMakeLists.txt
@@ -1,4 +1,4 @@
-if((NOT WIN32) AND (NOT APPLE) AND (NOT (CMAKE_SYSTEM_NAME STREQUAL "FreeBSD")))
+if(NOT WIN32)
 add_test_pl_tests(
     "$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation"
 )
diff --git a/regression/cbmc-concurrency/Makefile b/regression/cbmc-concurrency/Makefile
@@ -3,9 +3,8 @@ default: tests.log
 include ../../src/config.inc
 include ../../src/common
 
-ifeq ($(filter-out OSX MSVC FreeBSD,$(BUILD_ENV_)),)
+ifeq ($(filter-out MSVC,$(BUILD_ENV_)),)
 	# no POSIX threads on Windows
-	# for OSX and FreeBSD we'd need sound handling of pointers in multi-threaded programs
 	no_pthread = -X pthread
 endif
 
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
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 no-new-smt gcc-only`
`2`	`2`	`account.c`
`3`	`3`
`4`	`4`	`^EXIT=10$`
Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-if((NOT WIN32) AND (NOT APPLE) AND (NOT (CMAKE_SYSTEM_NAME STREQUAL "FreeBSD")))`
	`1`	`+if(NOT WIN32)`
`2`	`2`	`add_test_pl_tests(`
`3`	`3`	`"$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation"`
`4`	`4`	`)`
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$`