Field sensitivity: do not simplify unconditionally

The option --no-simplify should be honoured by field sensitivity. This
also made apparent that we have tests that only pass thanks to the
simplifier, and perhaps aren't even expected to pass. See diffblue#6101 for
further discussion.

Author: tautschnig

regression/cbmc/member_bounds3/test.desc

@@ -1,8 +1,10 @@
-CORE broken-smt-backend
+KNOWNBUG broken-smt-backend
 main.c
 --no-simplify
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring
+--
+See #6101 for a discussion as to whether this should be supported at all.

regression/cbmc/member_bounds4/test.desc

@@ -1,8 +1,10 @@
-CORE broken-smt-backend
+KNOWNBUG broken-smt-backend
 main.c
 --no-simplify
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring
+--
+See #6101 for a discussion as to whether this should be supported at all.

src/goto-symex/field_sensitivity.cpp

@@ -52,14 +52,14 @@ exprt field_sensitivityt::apply(
     !write && expr.id() == ID_member &&
     to_member_expr(expr).struct_op().id() == ID_struct)
   {
-    return simplify_expr(std::move(expr), ns);
+    return simplify_opt(std::move(expr), ns);
   }
 #ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
   else if(
     !write && expr.id() == ID_index &&
     to_index_expr(expr).array().id() == ID_array)
   {
-    return simplify_expr(std::move(expr), ns);
+    return simplify_opt(std::move(expr), ns);
   }
 #endif // ENABLE_ARRAY_FIELD_SENSITIVITY
   else if(expr.id() == ID_member)
@@ -95,7 +95,8 @@ exprt field_sensitivityt::apply(
     // encoding the index access into an array as an individual symbol rather
     // than only the full array
     index_exprt &index = to_index_expr(expr);
-    simplify(index.index(), ns);
+    if(should_simplify)
+      simplify(index.index(), ns);
 
     if(
       is_ssa_expr(index.array()) && index.array().type().id() == ID_array &&
@@ -105,7 +106,8 @@ exprt field_sensitivityt::apply(
       // SSA expression
       ssa_exprt tmp = to_ssa_expr(index.array());
       auto l2_index = state.rename(index.index(), ns);
-      l2_index.simplify(ns);
+      if(should_simplify)
+        l2_index.simplify(ns);
       bool was_l2 = !tmp.get_level_2().empty();
       exprt l2_size =
         state.rename(to_array_type(index.array().type()).size(), ns).get();
@@ -262,7 +264,8 @@ void field_sensitivityt::field_assignments_rec(
   else if(is_ssa_expr(lhs_fs))
   {
     exprt ssa_rhs = state.rename(lhs, ns).get();
-    simplify(ssa_rhs, ns);
+    if(should_simplify)
+      simplify(ssa_rhs, ns);
 
     const ssa_exprt ssa_lhs = state
                                 .assignment(
@@ -363,3 +366,11 @@ bool field_sensitivityt::is_divisible(const ssa_exprt &expr) const
 
   return false;
 }
+
+exprt field_sensitivityt::simplify_opt(exprt e, const namespacet &ns) const
+{
+  if(!should_simplify)
+    return e;
+
+  return simplify_expr(std::move(e), ns);
+}

src/goto-symex/field_sensitivity.h

@@ -84,8 +84,10 @@ class field_sensitivityt
 public:
   /// \param max_array_size: maximum size for which field sensitivity will be
   ///   applied to array cells
-  explicit field_sensitivityt(std::size_t max_array_size)
-    : max_field_sensitivity_array_size(max_array_size)
+  /// \param should_simplify: simplify expressions
+  field_sensitivityt(std::size_t max_array_size, bool should_simplify)
+    : max_field_sensitivity_array_size(max_array_size),
+      should_simplify(should_simplify)
   {
   }
 
@@ -157,13 +159,17 @@ class field_sensitivityt
 
   const std::size_t max_field_sensitivity_array_size;
 
+  const bool should_simplify;
+
   void field_assignments_rec(
     const namespacet &ns,
     goto_symex_statet &state,
     const exprt &lhs_fs,
     const exprt &lhs,
     symex_targett &target,
     bool allow_pointer_unsoundness);
+
+  exprt simplify_opt(exprt e, const namespacet &ns) const;
 };
 
 #endif // CPROVER_GOTO_SYMEX_FIELD_SENSITIVITY_H

src/goto-symex/goto_symex_state.cpp

@@ -31,13 +31,14 @@ static void get_l1_name(exprt &expr);
 goto_symex_statet::goto_symex_statet(
   const symex_targett::sourcet &_source,
   std::size_t max_field_sensitive_array_size,
+  bool should_simplify,
   guard_managert &manager,
   std::function<std::size_t(const irep_idt &)> fresh_l2_name_provider)
   : goto_statet(manager),
     source(_source),
     guard_manager(manager),
     symex_target(nullptr),
-    field_sensitivity(max_field_sensitive_array_size),
+    field_sensitivity(max_field_sensitive_array_size, should_simplify),
     record_events({true}),
     fresh_l2_name_provider(fresh_l2_name_provider)
 {

src/goto-symex/goto_symex_state.h

@@ -44,6 +44,7 @@ class goto_symex_statet final : public goto_statet
   goto_symex_statet(
     const symex_targett::sourcet &,
     std::size_t max_field_sensitive_array_size,
+    bool should_simplify,
     guard_managert &manager,
     std::function<std::size_t(const irep_idt &)> fresh_l2_name_provider);
   ~goto_symex_statet();

src/goto-symex/symex_main.cpp

@@ -422,6 +422,7 @@ std::unique_ptr<goto_symext::statet> goto_symext::initialize_entry_point_state(
   auto state = util_make_unique<statet>(
     symex_targett::sourcet(entry_point_id, start_function->body),
     symex_config.max_field_sensitivity_array_size,
+    symex_config.simplify_opt,
     guard_manager,
     [storage](const irep_idt &id) { return storage->get_unique_l2_index(id); });
 

unit/goto-symex/apply_condition.cpp

@@ -44,10 +44,12 @@ SCENARIO(
   guard_managert guard_manager;
   std::size_t count = 0;
   auto fresh_name = [&count](const irep_idt &) { return count++; };
-  goto_symex_statet state{source,
-                          DEFAULT_MAX_FIELD_SENSITIVITY_ARRAY_SIZE,
-                          guard_manager,
-                          fresh_name};
+  goto_symex_statet state{
+    source,
+    DEFAULT_MAX_FIELD_SENSITIVITY_ARRAY_SIZE,
+    true,
+    guard_manager,
+    fresh_name};
 
   goto_statet goto_state{state};
   const exprt renamed_b = state.rename<L2>(b, ns).get();

unit/goto-symex/goto_symex_state.cpp

@@ -40,7 +40,11 @@ SCENARIO(
     return fresh_name_count++;
   };
   goto_symex_statet state{
-    source, DEFAULT_MAX_FIELD_SENSITIVITY_ARRAY_SIZE, manager, fresh_name};
+    source,
+    DEFAULT_MAX_FIELD_SENSITIVITY_ARRAY_SIZE,
+    true,
+    manager,
+    fresh_name};
 
   // Initialize dirty field of state
   incremental_dirtyt dirty;

unit/goto-symex/symex_assign.cpp

@@ -51,7 +51,11 @@ SCENARIO(
     return fresh_name_count++;
   };
   goto_symex_statet state{
-    source, DEFAULT_MAX_FIELD_SENSITIVITY_ARRAY_SIZE, manager, fresh_name};
+    source,
+    DEFAULT_MAX_FIELD_SENSITIVITY_ARRAY_SIZE,
+    true,
+    manager,
+    fresh_name};
 
   // Initialize dirty field of state
   incremental_dirtyt dirty;

unit/goto-symex/try_evaluate_pointer_comparisons.cpp

@@ -54,10 +54,12 @@ SCENARIO(
   guard_managert guard_manager;
   std::size_t count = 0;
   auto fresh_name = [&count](const irep_idt &) { return count++; };
-  goto_symex_statet state{source,
-                          DEFAULT_MAX_FIELD_SENSITIVITY_ARRAY_SIZE,
-                          guard_manager,
-                          fresh_name};
+  goto_symex_statet state{
+    source,
+    DEFAULT_MAX_FIELD_SENSITIVITY_ARRAY_SIZE,
+    true,
+    guard_manager,
+    fresh_name};
 
   GIVEN("A value set in which pointer symbol `ptr1` only points to `&value1`")
   {
@@ -249,7 +251,7 @@ SCENARIO(
     // struct_symbol..pointer_field <- &value1
     {
       field_sensitivityt field_sensitivity{
-        DEFAULT_MAX_FIELD_SENSITIVITY_ARRAY_SIZE};
+        DEFAULT_MAX_FIELD_SENSITIVITY_ARRAY_SIZE, true};
       const exprt index_fs =
         field_sensitivity.apply(ns, state, member_l1.get(), true);
       value_set.assign(index_fs, address1_l1.get(), ns, false, false);