Use simplify_expr_with_value_sett across goto-symex

value-set based simplifications may be helpful well outside just GOTO
conditions.

Author: tautschnig

src/goto-symex/field_sensitivity.cpp

@@ -12,9 +12,9 @@ Author: Michael Tautschnig
 #include <util/byte_operators.h>
 #include <util/c_types.h>
 #include <util/pointer_offset_size.h>
-#include <util/simplify_expr.h>
 
 #include "goto_symex_state.h"
+#include "simplify_expr_with_value_set.h"
 #include "symex_target.h"
 
 #define ENABLE_ARRAY_FIELD_SENSITIVITY
@@ -51,14 +51,14 @@ exprt field_sensitivityt::apply(
     !write && expr.id() == ID_member &&
     to_member_expr(expr).struct_op().id() == ID_struct)
   {
-    return simplify_opt(std::move(expr), ns);
+    return simplify_opt(std::move(expr), state.value_set, ns);
   }
 #ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
   else if(
     !write && expr.id() == ID_index &&
     to_index_expr(expr).array().id() == ID_array)
   {
-    return simplify_opt(std::move(expr), ns);
+    return simplify_opt(std::move(expr), state.value_set, ns);
   }
 #endif // ENABLE_ARRAY_FIELD_SENSITIVITY
   else if(expr.id() == ID_member)
@@ -151,7 +151,10 @@ exprt field_sensitivityt::apply(
     // than only the full array
     index_exprt &index = to_index_expr(expr);
     if(should_simplify)
-      simplify(index.index(), ns);
+    {
+      simplify_expr_with_value_sett{state.value_set, language_mode, ns}
+        .simplify(index.index());
+    }
 
     if(
       is_ssa_expr(index.array()) && index.array().type().id() == ID_array &&
@@ -162,7 +165,10 @@ exprt field_sensitivityt::apply(
       ssa_exprt tmp = to_ssa_expr(index.array());
       auto l2_index = state.rename(index.index(), ns).get();
       if(should_simplify)
-        simplify(l2_index, ns);
+      {
+        simplify_expr_with_value_sett{state.value_set, language_mode, ns}
+          .simplify(l2_index);
+      }
       bool was_l2 = !tmp.get_level_2().empty();
       exprt l2_size =
         state.rename(to_array_type(index.array().type()).size(), ns).get();
@@ -393,7 +399,10 @@ void field_sensitivityt::field_assignments_rec(
       const exprt member_rhs = apply(
         ns,
         state,
-        simplify_opt(member_exprt{ssa_rhs, comp.get_name(), comp.type()}, ns),
+        simplify_opt(
+          member_exprt{ssa_rhs, comp.get_name(), comp.type()},
+          state.value_set,
+          ns),
         false);
 
       const exprt &member_lhs = *fs_it;
@@ -437,6 +446,7 @@ void field_sensitivityt::field_assignments_rec(
         simplify_opt(
           make_byte_extract(
             ssa_rhs, from_integer(0, c_index_type()), comp.type()),
+          state.value_set,
           ns),
         false);
 
@@ -476,7 +486,9 @@ void field_sensitivityt::field_assignments_rec(
         ns,
         state,
         simplify_opt(
-          index_exprt{ssa_rhs, from_integer(i, type->index_type())}, ns),
+          index_exprt{ssa_rhs, from_integer(i, type->index_type())},
+          state.value_set,
+          ns),
         false);
 
       const exprt &index_lhs = *fs_it;
@@ -558,10 +570,14 @@ bool field_sensitivityt::is_divisible(
   return false;
 }
 
-exprt field_sensitivityt::simplify_opt(exprt e, const namespacet &ns) const
+exprt field_sensitivityt::simplify_opt(
+  exprt e,
+  const value_sett &value_set,
+  const namespacet &ns) const
 {
   if(!should_simplify)
     return e;
 
-  return simplify_expr(std::move(e), ns);
+  simplify_expr_with_value_sett{value_set, language_mode, ns}.simplify(e);
+  return e;
 }

src/goto-symex/field_sensitivity.h

@@ -14,6 +14,7 @@ Author: Michael Tautschnig
 class namespacet;
 class goto_symex_statet;
 class symex_targett;
+class value_sett;
 
 class field_sensitive_ssa_exprt : public exprt
 {
@@ -119,9 +120,14 @@ class field_sensitivityt
   /// \param max_array_size: maximum size for which field sensitivity will be
   ///   applied to array cells
   /// \param should_simplify: simplify expressions
-  field_sensitivityt(std::size_t max_array_size, bool should_simplify)
+  /// \param language_mode: mode of the language that expressions belong to.
+  field_sensitivityt(
+    std::size_t max_array_size,
+    bool should_simplify,
+    const irep_idt &language_mode)
     : max_field_sensitivity_array_size(max_array_size),
-      should_simplify(should_simplify)
+      should_simplify(should_simplify),
+      language_mode(language_mode)
   {
   }
 
@@ -201,6 +207,7 @@ class field_sensitivityt
   const std::size_t max_field_sensitivity_array_size;
 
   const bool should_simplify;
+  const irep_idt &language_mode;
 
   void field_assignments_rec(
     const namespacet &ns,
@@ -210,7 +217,10 @@ class field_sensitivityt
     symex_targett &target,
     bool allow_pointer_unsoundness) const;
 
-  [[nodiscard]] exprt simplify_opt(exprt e, const namespacet &ns) const;
+  [[nodiscard]] exprt simplify_opt(
+    exprt e,
+    const value_sett &value_set,
+    const namespacet &ns) const;
 };
 
 #endif // CPROVER_GOTO_SYMEX_FIELD_SENSITIVITY_H

src/goto-symex/goto_symex.cpp

@@ -11,28 +11,30 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "goto_symex.h"
 
-#include "expr_skeleton.h"
-#include "symex_assign.h"
-
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/format_expr.h>
 #include <util/fresh_symbol.h>
 #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>
 #include <util/string_utils.h>
 
+#include "expr_skeleton.h"
+#include "simplify_expr_with_value_set.h"
+#include "symex_assign.h"
+
 #include <climits>
 
-void goto_symext::do_simplify(exprt &expr)
+void goto_symext::do_simplify(exprt &expr, const value_sett &value_set)
 {
   if(symex_config.simplify_opt)
-    simplify(expr, ns);
+  {
+    simplify_expr_with_value_sett{value_set, language_mode, ns}.simplify(expr);
+  }
 }
 
 void goto_symext::symex_assign(
@@ -61,7 +63,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);
+  do_simplify(lhs, state.value_set);
   lhs = state.field_sensitivity.apply(ns, state, std::move(lhs), true);
 
   if(rhs.id() == ID_side_effect)
@@ -104,7 +106,13 @@ void goto_symext::symex_assign(
       assignment_type = symex_targett::assignment_typet::HIDDEN;
 
     symex_assignt symex_assign{
-      shadow_memory, state, assignment_type, ns, symex_config, target};
+      shadow_memory,
+      state,
+      assignment_type,
+      ns,
+      symex_config,
+      language_mode,
+      target};
 
     // Try to constant propagate potential side effects of the assignment, when
     // simplification is turned on and there is one thread only. Constant
@@ -134,7 +142,13 @@ void goto_symext::symex_assign(
 
     exprt::operandst lhs_if_then_else_conditions;
     symex_assignt{
-      shadow_memory, state, assignment_type, ns, symex_config, target}
+      shadow_memory,
+      state,
+      assignment_type,
+      ns,
+      symex_config,
+      language_mode,
+      target}
       .assign_rec(lhs, expr_skeletont{}, rhs, lhs_if_then_else_conditions);
 
     if(need_atomic_section)

src/goto-symex/goto_symex.h

@@ -27,6 +27,7 @@ class shadow_memory_field_definitionst;
 class side_effect_exprt;
 class symex_assignt;
 class typet;
+class value_sett;
 
 /// \brief The main class for the forward symbolic simulator
 /// \remarks
@@ -528,7 +529,7 @@ class goto_symext
   /// \param state: Symbolic execution state for current instruction
   void symex_catch(statet &state);
 
-  virtual void do_simplify(exprt &expr);
+  virtual void do_simplify(exprt &expr, const value_sett &value_set);
 
   /// Symbolically execute an ASSIGN instruction or simulate such an execution
   /// for a synthetic assignment

src/goto-symex/goto_symex_state.cpp

@@ -18,13 +18,13 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/exception_utils.h>
 #include <util/expr_util.h>
 #include <util/invariant.h>
-#include <util/simplify_expr.h>
 #include <util/std_expr.h>
 
 #include <analyses/dirty.h>
 #include <pointer-analysis/add_failed_symbols.h>
 
 #include "goto_symex_can_forward_propagate.h"
+#include "simplify_expr_with_value_set.h"
 #include "symex_target_equation.h"
 
 static void get_l1_name(exprt &expr);
@@ -33,14 +33,19 @@ goto_symex_statet::goto_symex_statet(
   const symex_targett::sourcet &_source,
   std::size_t max_field_sensitive_array_size,
   bool should_simplify,
+  const irep_idt &language_mode,
   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, should_simplify),
+    field_sensitivity(
+      max_field_sensitive_array_size,
+      should_simplify,
+      language_mode),
     record_events({true}),
+    language_mode(language_mode),
     fresh_l2_name_provider(fresh_l2_name_provider)
 {
   threads.emplace_back(guard_manager);
@@ -86,7 +91,7 @@ renamedt<ssa_exprt, L2> goto_symex_statet::assignment(
   // the type might need renaming
   rename<L2>(lhs.type(), l1_identifier, ns);
   if(rhs_is_simplified)
-    simplify(lhs, ns);
+    simplify_expr_with_value_sett{value_set, language_mode, ns}.simplify(lhs);
   lhs.update_type();
   if(run_validation_checks)
   {

src/goto-symex/goto_symex_state.h

@@ -45,6 +45,7 @@ class goto_symex_statet final : public goto_statet
     const symex_targett::sourcet &,
     std::size_t max_field_sensitive_array_size,
     bool should_simplify,
+    const irep_idt &language_mode,
     guard_managert &manager,
     std::function<std::size_t(const irep_idt &)> fresh_l2_name_provider);
   ~goto_symex_statet();
@@ -258,6 +259,7 @@ class goto_symex_statet final : public goto_statet
   }
 
 private:
+  const irep_idt &language_mode;
   std::function<std::size_t(const irep_idt &)> fresh_l2_name_provider;
 
   /// \brief Dangerous, do not use

src/goto-symex/symex_assign.cpp

@@ -15,10 +15,10 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/expr_util.h>
 #include <util/pointer_expr.h>
 #include <util/range.h>
-#include <util/simplify_expr.h>
 
 #include "expr_skeleton.h"
 #include "goto_symex_state.h"
+#include "simplify_expr_with_value_set.h"
 #include "symex_config.h"
 
 // We can either use with_exprt or update_exprt when building expressions that
@@ -207,7 +207,10 @@ void symex_assignt::assign_non_struct_symbol(
   assignmentt assignment{lhs, full_lhs, l2_rhs};
 
   if(symex_config.simplify_opt)
-    assignment.rhs = simplify_expr(std::move(assignment.rhs), ns);
+  {
+    simplify_expr_with_value_sett{state.value_set, language_mode, ns}.simplify(
+      assignment.rhs);
+  }
 
   const ssa_exprt l2_lhs = state
                              .assignment(

src/goto-symex/symex_assign.h

@@ -33,12 +33,14 @@ class symex_assignt
     symex_targett::assignment_typet assignment_type,
     const namespacet &ns,
     const symex_configt &symex_config,
+    const irep_idt &language_mode,
     symex_targett &target)
     : shadow_memory(shadow_memory),
       state(state),
       assignment_type(assignment_type),
       ns(ns),
       symex_config(symex_config),
+      language_mode(language_mode),
       target(target)
   {
   }
@@ -65,6 +67,7 @@ class symex_assignt
   symex_targett::assignment_typet assignment_type;
   const namespacet &ns;
   const symex_configt &symex_config;
+  const irep_idt &language_mode;
   symex_targett ⌖
 
   void assign_from_struct(

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);
+    do_simplify(read_guard_expr, state.value_set);
 
     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);
+    do_simplify(write_guard_expr, state.value_set);
 
     target.shared_write(
       write_guard_expr,