Merge pull request #6121 from tautschnig/concurrency-dirty-1

Concurrency: do not remove shared or dirty pointers from the value set

Author: tautschnig

regression/cbmc-concurrency/dirty_local3/main.c

@@ -0,0 +1,24 @@
+void worker(int *p)
+{
+  __CPROVER_assert(*p == 1, "reading from dirty object");
+}
+
+void create_thread(int **p)
+{
+#ifdef locals_bug
+  int z = 1;
+__CPROVER_ASYNC_1:
+  worker(&z);
+#else
+__CPROVER_ASYNC_1:
+  worker(*p);
+#endif
+}
+
+int main()
+{
+  int y = 1;
+  int *x[1] = {&y};
+  create_thread(&x[0]);
+  return 0;
+}

regression/cbmc-concurrency/dirty_local3/test-local.desc

@@ -0,0 +1,18 @@
+KNOWNBUG
+main.c
+-Dlocals_bug
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+There is a need for further debugging around copying local objects in
+the procedure spawning threads as we generate the following non-sensical
+constraint:
+// 28 file regression/cbmc-concurrency/dirty_local3/main.c line 3 function worker
+(57) CONSTRAINT(z!1@0#2 == z!1@0 || !choice_rf0)
+                ^^^^^^^^^^^^^^^^
+                comparison of L2 and L1 SSA symbols
+// 28 file regression/cbmc-concurrency/dirty_local3/main.c line 3 function worker
+(58) CONSTRAINT(choice_rf0)

regression/cbmc-concurrency/dirty_local3/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

src/goto-symex/symex_dead.cpp

@@ -11,7 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "goto_symex.h"
 
-#include <util/find_symbols.h>
 #include <util/std_expr.h>
 
 void goto_symext::symex_dead(statet &state)
@@ -20,23 +19,27 @@ void goto_symext::symex_dead(statet &state)
   symex_dead(state, instruction.dead_symbol());
 }
 
-void goto_symext::symex_dead(statet &state, const symbol_exprt &symbol_expr)
+static void remove_l1_object_rec(
+  goto_symext::statet &state,
+  const exprt &l1_expr,
+  const namespacet &ns)
 {
-  ssa_exprt to_rename = is_ssa_expr(symbol_expr) ? to_ssa_expr(symbol_expr)
-                                                 : ssa_exprt{symbol_expr};
-  ssa_exprt ssa = state.rename_ssa<L1>(to_rename, ns).get();
-
-  const exprt fields = state.field_sensitivity.get_fields(ns, state, ssa);
-  find_symbols_sett fields_set;
-  find_symbols_or_nexts(fields, fields_set);
-
-  for(const irep_idt &l1_identifier : fields_set)
+  if(is_ssa_expr(l1_expr))
   {
+    const ssa_exprt &l1_ssa = to_ssa_expr(l1_expr);
+    const irep_idt &l1_identifier = l1_ssa.get_identifier();
+
     // We cannot remove the object from the L1 renaming map, because L1 renaming
     // information is not local to a path, but removing it from the propagation
     // map and value-set is safe as 1) it is local to a path and 2) this
-    // instance can no longer appear.
-    state.value_set.values.erase_if_exists(l1_identifier);
+    // instance can no longer appear (unless shared across threads).
+    if(
+      state.threads.size() <= 1 ||
+      state.write_is_shared(l1_ssa, ns) ==
+        goto_symex_statet::write_is_shared_resultt::NOT_SHARED)
+    {
+      state.value_set.values.erase_if_exists(l1_identifier);
+    }
     state.propagation.erase_if_exists(l1_identifier);
     // Remove from the local L2 renaming map; this means any reads from the dead
     // identifier will use generation 0 (e.g. x!N@M#0, where N and M are
@@ -45,4 +48,21 @@ void goto_symext::symex_dead(statet &state, const symbol_exprt &symbol_expr)
     // identifier is still live.
     state.drop_l1_name(l1_identifier);
   }
+  else if(l1_expr.id() == ID_array || l1_expr.id() == ID_struct)
+  {
+    for(const auto &op : l1_expr.operands())
+      remove_l1_object_rec(state, op, ns);
+  }
+  else
+    UNREACHABLE;
+}
+
+void goto_symext::symex_dead(statet &state, const symbol_exprt &symbol_expr)
+{
+  ssa_exprt to_rename = is_ssa_expr(symbol_expr) ? to_ssa_expr(symbol_expr)
+                                                 : ssa_exprt{symbol_expr};
+  ssa_exprt ssa = state.rename_ssa<L1>(to_rename, ns).get();
+
+  const exprt fields = state.field_sensitivity.get_fields(ns, state, ssa);
+  remove_l1_object_rec(state, fields, ns);
 }