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