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

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

Author: tautschnig

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;
 }

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.

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;
     }
   }

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,

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))
   {

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;
 

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);
   }
 }
 

src/goto-symex/symex_dereference.cpp

@@ -9,20 +9,20 @@ 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_util.h>
+#include <util/find_symbols.h>
 #include <util/fresh_symbol.h>
 #include <util/invariant.h>
 #include <util/pointer_offset_size.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"
@@ -307,6 +307,28 @@ void goto_symext::dereference_rec(
     // dereference an L2 pointer, which it would not have an entry for.
 
     tmp1 = state.rename<L1_WITH_CONSTANT_PROPAGATION>(tmp1, ns).get();
+    if(
+      tmp1.id() != ID_address_of && state.threads.size() > 1 &&
+      !symex_config.allow_pointer_unsoundness)
+    {
+      // 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(const auto &sym_expr : find_symbols(tmp1))
+      {
+        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() || path_storage.dirty(obj_name)))
+        {
+          throw unsupported_operation_exceptiont(
+            "pointer handling for concurrency is unsound: " +
+            id2string(obj_name));
+        }
+      }
+    }
 
     do_simplify(tmp1, state.value_set);
 

unit/goto-symex/goto_symex_state.cpp

@@ -65,8 +65,7 @@ SCENARIO(
     WHEN("Symbol `foo` is assigned constant integer `475`")
     {
       const exprt rhs1 = from_integer(475, int_type);
-      const auto result =
-        state.assignment(ssa_foo, rhs1, ns, true, true, false);
+      const auto result = state.assignment(ssa_foo, rhs1, ns, true, true);
       THEN("The result is `foo` renamed to L2")
       {
         REQUIRE(result.get().get_identifier() == "foo!0#1");
@@ -88,8 +87,7 @@ SCENARIO(
       THEN("Symbol `foo` is assigned another integer 1834")
       {
         const exprt rhs2 = from_integer(1834, int_type);
-        const auto result2 =
-          state.assignment(ssa_foo, rhs2, ns, true, true, false);
+        const auto result2 = state.assignment(ssa_foo, rhs2, ns, true, true);
 
         THEN("The level 2 index of `foo` is incremented")
         {
@@ -128,7 +126,7 @@ SCENARIO(
     {
       const null_pointer_exprt null_pointer{int_pointer_type};
       const auto result =
-        state.assignment(ssa_foo, null_pointer, ns, true, true, false);
+        state.assignment(ssa_foo, null_pointer, ns, true, true);
       THEN("The result is `foo` renamed to L2")
       {
         REQUIRE(result.get().get_identifier() == "foo!0#1");
@@ -155,7 +153,7 @@ SCENARIO(
         const address_of_exprt rhs2{int_value};
         const renamedt<exprt, L2> l2_rhs2 = state.rename(rhs2, ns);
         const auto result2 =
-          state.assignment(ssa_foo, l2_rhs2.get(), ns, true, true, false);
+          state.assignment(ssa_foo, l2_rhs2.get(), ns, true, true);
 
         THEN("The level 2 index of `foo` is incremented")
         {