Do not use value-set supported simplification with multiple threads

Shared pointers may be updated in yet-to-be-executed threads.

Author: tautschnig

regression/cbmc-concurrency/global_pointer1/no_deref.desc

@@ -1,11 +1,8 @@
-KNOWNBUG
+CORE
 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/goto_symex.cpp

@@ -18,6 +18,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/mathematical_expr.h>
 #include <util/mathematical_types.h>
 #include <util/pointer_offset_size.h>
+#include <util/simplify_expr.h>
 #include <util/simplify_utils.h>
 #include <util/std_code.h>
 #include <util/string_expr.h>
@@ -29,11 +30,17 @@ Author: Daniel Kroening, [email protected]
 
 #include <climits>
 
-void goto_symext::do_simplify(exprt &expr, const value_sett &value_set)
+void goto_symext::do_simplify(exprt &expr, const statet &state)
 {
   if(symex_config.simplify_opt)
   {
-    simplify_expr_with_value_sett{value_set, language_mode, ns}.simplify(expr);
+    if(state.threads.size() == 1)
+    {
+      simplify_expr_with_value_sett{state.value_set, language_mode, ns}
+        .simplify(expr);
+    }
+    else
+      simplify(expr, ns);
   }
 }
 
@@ -63,7 +70,7 @@ void goto_symext::symex_assign(
   // "byte_extract <type> from an_lvalue offset this_rvalue") can affect whether
   // we use field-sensitive symbols or not, so L2-rename them up front:
   lhs = state.l2_rename_rvalues(lhs, ns);
-  do_simplify(lhs, state.value_set);
+  do_simplify(lhs, state);
   lhs = state.field_sensitivity.apply(ns, state, std::move(lhs), true);
 
   if(rhs.id() == ID_side_effect)

src/goto-symex/goto_symex.h

@@ -526,7 +526,7 @@ class goto_symext
   /// \param state: Symbolic execution state for current instruction
   void symex_catch(statet &state);
 
-  virtual void do_simplify(exprt &expr, const value_sett &value_set);
+  virtual void do_simplify(exprt &expr, const statet &state);
 
   /// Symbolically execute an ASSIGN instruction or simulate such an execution
   /// for a synthetic assignment

src/goto-symex/symex_atomic_section.cpp

@@ -58,7 +58,7 @@ void goto_symext::symex_atomic_end(statet &state)
         ++it)
       read_guard|=*it;
     exprt read_guard_expr=read_guard.as_expr();
-    do_simplify(read_guard_expr, state.value_set);
+    do_simplify(read_guard_expr, state);
 
     target.shared_read(
       read_guard_expr,
@@ -80,7 +80,7 @@ void goto_symext::symex_atomic_end(statet &state)
         ++it)
       write_guard|=*it;
     exprt write_guard_expr=write_guard.as_expr();
-    do_simplify(write_guard_expr, state.value_set);
+    do_simplify(write_guard_expr, state);
 
     target.shared_write(
       write_guard_expr,

src/goto-symex/symex_builtin_functions.cpp

@@ -293,7 +293,7 @@ void goto_symext::symex_va_start(
 
   array = clean_expr(std::move(array), state, false);
   array = state.rename(std::move(array), ns).get();
-  do_simplify(array, state.value_set);
+  do_simplify(array, state);
   symex_assign(state, va_array.symbol_expr(), std::move(array));
 
   exprt rhs = address_of_exprt{index_exprt{
@@ -388,7 +388,7 @@ void goto_symext::symex_printf(
   exprt tmp_rhs = rhs;
   clean_expr(tmp_rhs, state, false);
   tmp_rhs = state.rename(std::move(tmp_rhs), ns).get();
-  do_simplify(tmp_rhs, state.value_set);
+  do_simplify(tmp_rhs, state);
 
   const exprt::operandst &operands=tmp_rhs.operands();
   std::list<exprt> args;
@@ -426,7 +426,7 @@ void goto_symext::symex_printf(
         parameter = to_address_of_expr(parameter).object();
       clean_expr(parameter, state, false);
       parameter = state.rename(std::move(parameter), ns).get();
-      do_simplify(parameter, state.value_set);
+      do_simplify(parameter, state);
 
       args.push_back(std::move(parameter));
     }
@@ -454,7 +454,7 @@ void goto_symext::symex_input(
   for(std::size_t i=1; i<code.operands().size(); i++)
   {
     exprt l2_arg = state.rename(code.operands()[i], ns).get();
-    do_simplify(l2_arg, state.value_set);
+    do_simplify(l2_arg, state);
     args.emplace_back(std::move(l2_arg));
   }
 

src/goto-symex/symex_clean_expr.cpp

@@ -135,7 +135,7 @@ void goto_symext::process_array_expr(statet &state, exprt &expr)
   lift_lets(state, expr);
 
   ::process_array_expr(expr, ns);
-  do_simplify(expr, state.value_set);
+  do_simplify(expr, state);
 }
 
 /// Rewrite index/member expressions in byte_extract to offset
@@ -178,7 +178,7 @@ void goto_symext::lift_let(statet &state, const let_exprt &let_expr)
 {
   exprt let_value = clean_expr(let_expr.value(), state, false);
   let_value = state.rename(std::move(let_value), ns).get();
-  do_simplify(let_value, state.value_set);
+  do_simplify(let_value, state);
 
   exprt::operandst value_assignment_guard;
   symex_assignt{

src/goto-symex/symex_dereference.cpp

@@ -101,7 +101,7 @@ exprt goto_symext::address_arithmetic(
     // recursive call
     result = address_arithmetic(be, state, keep_array);
 
-    do_simplify(result, state.value_set);
+    do_simplify(result, state);
   }
   else if(expr.id()==ID_dereference)
   {
@@ -158,7 +158,7 @@ exprt goto_symext::address_arithmetic(
 
       result = address_arithmetic(be, state, keep_array);
 
-      do_simplify(result, state.value_set);
+      do_simplify(result, state);
     }
     else
       result=address_of_exprt(result);
@@ -330,7 +330,7 @@ void goto_symext::dereference_rec(
       }
     }
 
-    do_simplify(tmp1, state.value_set);
+    do_simplify(tmp1, state);
 
     if(symex_config.run_validation_checks)
     {
@@ -537,7 +537,7 @@ void goto_symext::dereference(exprt &expr, statet &state, bool write)
   // when all we need is
   // s1 := s1 with (member := X) [and guard b]
   // s2 := s2 with (member := X) [and guard !b]
-  do_simplify(expr, state.value_set);
+  do_simplify(expr, state);
 
   if(symex_config.run_validation_checks)
   {

src/goto-symex/symex_goto.cpp

@@ -118,7 +118,7 @@ void goto_symext::symex_goto(statet &state)
       // generate assume(false) or a suitable negation if this
       // instruction is a conditional goto
       exprt negated_guard = boolean_negate(new_guard);
-      do_simplify(negated_guard, state.value_set);
+      do_simplify(negated_guard, state);
       log.statistics() << "replacing self-loop at "
                        << state.source.pc->source_location() << " by assume("
                        << from_expr(ns, state.source.function_id, negated_guard)

src/goto-symex/symex_main.cpp

@@ -157,7 +157,7 @@ void goto_symext::symex_assert(
   // First, push negations in and perhaps convert existential quantifiers into
   // universals:
   if(has_subexpr(condition, ID_exists) || has_subexpr(condition, ID_forall))
-    do_simplify(condition, state.value_set);
+    do_simplify(condition, state);
 
   // Second, L2-rename universal quantifiers:
   if(has_subexpr(condition, ID_forall))
@@ -167,7 +167,7 @@ void goto_symext::symex_assert(
   exprt l2_condition = state.rename(std::move(condition), ns).get();
 
   // now try simplifier on it
-  do_simplify(l2_condition, state.value_set);
+  do_simplify(l2_condition, state);
 
   std::string msg = id2string(instruction.source_location().get_comment());
   if(msg.empty())
@@ -200,7 +200,7 @@ void goto_symext::symex_assume(statet &state, const exprt &cond)
 {
   exprt simplified_cond = clean_expr(cond, state, false);
   simplified_cond = state.rename(std::move(simplified_cond), ns).get();
-  do_simplify(simplified_cond, state.value_set);
+  do_simplify(simplified_cond, state);
 
   // It would be better to call try_filter_value_sets after apply_condition,
   // but it is not currently possible. See the comment at the beginning of
@@ -848,13 +848,13 @@ void goto_symext::try_filter_value_sets(
     // without another round of constant propagation.
     // It would be sufficient to replace this call to do_simplify() with
     // something that just replaces `*&x` with `x` whenever it finds it.
-    do_simplify(modified_condition, state.value_set);
+    do_simplify(modified_condition, state);
 
     state.record_events.push(false);
     modified_condition = state.rename(std::move(modified_condition), ns).get();
     state.record_events.pop();
 
-    do_simplify(modified_condition, state.value_set);
+    do_simplify(modified_condition, state);
 
     if(jump_taken_value_set && modified_condition == false)
     {

src/goto-symex/symex_other.cpp

@@ -151,14 +151,14 @@ void goto_symext::symex_other(
       {
         src_array = make_byte_extract(
           src_array, from_integer(0, c_index_type()), dest_array.type());
-        do_simplify(src_array, state.value_set);
+        do_simplify(src_array, state);
       }
       else
       {
         // ID_array_replace
         dest_array = make_byte_extract(
           dest_array, from_integer(0, c_index_type()), src_array.type());
-        do_simplify(dest_array, state.value_set);
+        do_simplify(dest_array, state);
       }
     }
 
@@ -197,7 +197,7 @@ void goto_symext::symex_other(
     {
       auto array_size = size_of_expr(array_expr.type(), ns);
       CHECK_RETURN(array_size.has_value());
-      do_simplify(array_size.value(), state.value_set);
+      do_simplify(array_size.value(), state);
       array_expr = make_byte_extract(
         array_expr,
         from_integer(0, c_index_type()),