Introduce value-set supported simplifier for goto-symex

Move `try_evaluate_pointer_comparison` to a simplifier that can
eventually support more cases than just equalities in GOTO conditions.
The initial change does not alter behaviour (except that previously
`try_evaluate_pointer_comparison` was even used when simplification was
disabled).

A side-effect is that we can also clean up renamedt.

Author: tautschnig

src/goto-symex/Makefile

@@ -18,6 +18,7 @@ SRC = auto_objects.cpp \
       shadow_memory_util.cpp \
       show_program.cpp \
       show_vcc.cpp \
+      simplify_expr_with_value_set.cpp \
       slice.cpp \
       solver_hardness.cpp \
       ssa_step.cpp \

src/goto-symex/field_sensitivity.cpp

@@ -160,9 +160,9 @@ exprt field_sensitivityt::apply(
       // place the entire index expression, not just the array operand, in an
       // SSA expression
       ssa_exprt tmp = to_ssa_expr(index.array());
-      auto l2_index = state.rename(index.index(), ns);
+      auto l2_index = state.rename(index.index(), ns).get();
       if(should_simplify)
-        l2_index.simplify(ns);
+        simplify(l2_index, ns);
       bool was_l2 = !tmp.get_level_2().empty();
       exprt l2_size =
         state.rename(to_array_type(index.array().type()).size(), ns).get();
@@ -181,14 +181,14 @@ exprt field_sensitivityt::apply(
         numeric_cast_v<mp_integer>(to_constant_expr(l2_size)) <=
           max_field_sensitivity_array_size)
       {
-        if(l2_index.get().is_constant())
+        if(l2_index.is_constant())
         {
           // place the entire index expression, not just the array operand,
           // in an SSA expression
           ssa_exprt ssa_array = to_ssa_expr(index.array());
           ssa_array.remove_level_2();
           index.array() = ssa_array.get_original_expr();
-          index.index() = l2_index.get();
+          index.index() = l2_index;
           tmp.set_expression(index);
           if(was_l2)
           {

src/goto-symex/goto_symex.h

@@ -876,20 +876,4 @@ void symex_transition(
   goto_programt::const_targett to,
   bool is_backwards_goto);
 
-/// Try to evaluate pointer comparisons where they can be trivially determined
-/// using the value-set. This is optional as all it does is allow symex to
-/// resolve some comparisons itself and therefore create a simpler formula for
-/// the SAT solver.
-/// \param [in,out] condition: An L2-renamed expression with boolean type
-/// \param value_set: The value-set for determining what pointer-typed symbols
-///   might possibly point to
-/// \param language_mode: The language mode
-/// \param ns: A namespace
-/// \return The possibly modified condition
-renamedt<exprt, L2> try_evaluate_pointer_comparisons(
-  renamedt<exprt, L2> condition,
-  const value_sett &value_set,
-  const irep_idt &language_mode,
-  const namespacet &ns);
-
 #endif // CPROVER_GOTO_SYMEX_GOTO_SYMEX_H

src/goto-symex/goto_symex_state.cpp

@@ -18,6 +18,7 @@ Author: Daniel Kroening, [email protected]
 #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>

src/goto-symex/renamed.h

@@ -11,8 +11,8 @@ Author: Romain Brenguier, [email protected]
 #ifndef CPROVER_GOTO_SYMEX_RENAMED_H
 #define CPROVER_GOTO_SYMEX_RENAMED_H
 
-#include <util/expr_iterator.h>
-#include <util/simplify_expr.h>
+#include <util/simplify_expr_class.h>
+
 #include <util/std_expr.h>
 
 class ssa_exprt;
@@ -42,14 +42,11 @@ class renamedt : private underlyingt
     return static_cast<const underlyingt &>(*this);
   }
 
-  void simplify(const namespacet &ns)
+  void simplify(simplify_exprt &simplifier)
   {
-    (void)::simplify(value(), ns);
+    simplifier.simplify(value());
   }
 
-  using mutator_functiont =
-    std::function<std::optional<renamedt>(const renamedt &)>;
-
 private:
   underlyingt &value()
   {
@@ -62,49 +59,10 @@ class renamedt : private underlyingt
   friend struct symex_level2t;
   friend class goto_symex_statet;
 
-  template <levelt make_renamed_level>
-  friend renamedt<exprt, make_renamed_level>
-  make_renamed(constant_exprt constant);
-
-  template <levelt selectively_mutate_level>
-  friend void selectively_mutate(
-    renamedt<exprt, selectively_mutate_level> &renamed,
-    typename renamedt<exprt, selectively_mutate_level>::mutator_functiont
-      get_mutated_expr);
-
   /// Only the friend classes can create renamedt objects
   explicit renamedt(underlyingt value) : underlyingt(std::move(value))
   {
   }
 };
 
-template <levelt level>
-renamedt<exprt, level> make_renamed(constant_exprt constant)
-{
-  return renamedt<exprt, level>(std::move(constant));
-}
-
-/// This permits replacing subexpressions of the renamed value, so long as
-/// each replacement is consistent with our current renaming level (for
-/// example, replacing subexpressions of L2 expressions with ones which are
-/// themselves L2 renamed).
-/// The passed function will be called with each expression node in preorder
-/// (i.e. parent expressions before children), and should return an empty
-/// optional to make no change or a renamed expression to make a change.
-template <levelt level>
-void selectively_mutate(
-  renamedt<exprt, level> &renamed,
-  typename renamedt<exprt, level>::mutator_functiont get_mutated_expr)
-{
-  for(auto it = renamed.depth_begin(), itend = renamed.depth_end(); it != itend;
-      ++it)
-  {
-    std::optional<renamedt<exprt, level>> replacement =
-      get_mutated_expr(static_cast<const renamedt<exprt, level> &>(*it));
-
-    if(replacement)
-      it.mutate() = std::move(replacement->value());
-  }
-}
-
 #endif // CPROVER_GOTO_SYMEX_RENAMED_H

src/goto-symex/shadow_memory_util.cpp

@@ -20,6 +20,7 @@ Author: Peter Schrammel
 #include <util/invariant.h>
 #include <util/namespace.h>
 #include <util/pointer_offset_size.h>
+#include <util/simplify_expr.h>
 #include <util/ssa_expr.h>
 #include <util/std_expr.h>
 #include <util/string_constant.h>

src/goto-symex/simplify_expr_with_value_set.cpp

@@ -0,0 +1,156 @@
+/*******************************************************************\
+
+Module: Variant of simplify_exprt that uses a value_sett
+
+Author: Michael Tautschnig
+
+\*******************************************************************/
+
+#include "simplify_expr_with_value_set.h"
+
+#include <util/expr_util.h>
+#include <util/pointer_expr.h>
+#include <util/simplify_expr.h>
+#include <util/ssa_expr.h>
+
+#include <pointer-analysis/add_failed_symbols.h>
+#include <pointer-analysis/value_set.h>
+#include <pointer-analysis/value_set_dereference.h>
+
+#include "goto_symex_can_forward_propagate.h"
+
+/// Try to evaluate a simple pointer comparison.
+/// \param operation: ID_equal or ID_not_equal
+/// \param symbol_expr: The symbol expression in the condition
+/// \param other_operand: The other expression in the condition; we only support
+///   an address of expression, a typecast of an address of expression or a
+///   null pointer, and return an empty std::optional in all other cases
+/// \param value_set: The value-set for looking up what the symbol can point to
+/// \param language_mode: The language mode
+/// \param ns: A namespace
+/// \return If we were able to evaluate the condition as true or false then we
+///   return that, otherwise we return an empty std::optional
+static std::optional<exprt> try_evaluate_pointer_comparison(
+  const irep_idt &operation,
+  const symbol_exprt &symbol_expr,
+  const exprt &other_operand,
+  const value_sett &value_set,
+  const irep_idt language_mode,
+  const namespacet &ns)
+{
+  const constant_exprt *constant_expr =
+    expr_try_dynamic_cast<constant_exprt>(other_operand);
+
+  if(
+    skip_typecast(other_operand).id() != ID_address_of &&
+    (!constant_expr || !constant_expr->is_null_pointer()))
+  {
+    return {};
+  }
+
+  const ssa_exprt *ssa_symbol_expr =
+    expr_try_dynamic_cast<ssa_exprt>(symbol_expr);
+
+  ssa_exprt l1_expr{*ssa_symbol_expr};
+  l1_expr.remove_level_2();
+  const std::vector<exprt> value_set_elements =
+    value_set.get_value_set(l1_expr, ns);
+
+  bool constant_found = false;
+
+  for(const auto &value_set_element : value_set_elements)
+  {
+    if(
+      value_set_element.id() == ID_unknown ||
+      value_set_element.id() == ID_invalid ||
+      is_failed_symbol(
+        to_object_descriptor_expr(value_set_element).root_object()) ||
+      to_object_descriptor_expr(value_set_element).offset().id() == ID_unknown)
+    {
+      // We can't conclude anything about the value-set
+      return {};
+    }
+
+    if(!constant_found)
+    {
+      if(value_set_dereferencet::should_ignore_value(
+           value_set_element, false, language_mode))
+      {
+        continue;
+      }
+
+      value_set_dereferencet::valuet value =
+        value_set_dereferencet::build_reference_to(
+          value_set_element, symbol_expr, ns);
+
+      // use the simplifier to test equality as we need to skip over typecasts
+      // and cannot rely on canonical representations, which would permit a
+      // simple syntactic equality test
+      exprt test_equal = simplify_expr(
+        equal_exprt{
+          typecast_exprt::conditional_cast(value.pointer, other_operand.type()),
+          other_operand},
+        ns);
+      if(test_equal.is_true())
+      {
+        constant_found = true;
+        // We can't break because we have to make sure we find any instances of
+        // ID_unknown or ID_invalid
+      }
+      else if(!test_equal.is_false())
+      {
+        // We can't conclude anything about the value-set
+        return {};
+      }
+    }
+  }
+
+  if(!constant_found)
+  {
+    // The symbol cannot possibly have the value \p other_operand because it
+    // isn't in the symbol's value-set
+    return operation == ID_equal ? static_cast<exprt>(false_exprt{})
+                                 : static_cast<exprt>(true_exprt{});
+  }
+  else if(value_set_elements.size() == 1)
+  {
+    // The symbol must have the value \p other_operand because it is the only
+    // thing in the symbol's value-set
+    return operation == ID_equal ? static_cast<exprt>(true_exprt{})
+                                 : static_cast<exprt>(false_exprt{});
+  }
+  else
+  {
+    return {};
+  }
+}
+
+simplify_exprt::resultt<> simplify_expr_with_value_sett::simplify_inequality(
+  const binary_relation_exprt &expr)
+{
+  if(expr.id() != ID_equal && expr.id() != ID_notequal)
+    return simplify_exprt::simplify_inequality(expr);
+
+  if(!can_cast_type<pointer_typet>(to_binary_expr(expr).op0().type()))
+    return simplify_exprt::simplify_inequality(expr);
+
+  exprt lhs = to_binary_expr(expr).op0(), rhs = to_binary_expr(expr).op1();
+  if(can_cast_expr<symbol_exprt>(rhs))
+    std::swap(lhs, rhs);
+
+  const symbol_exprt *symbol_expr_lhs =
+    expr_try_dynamic_cast<symbol_exprt>(lhs);
+
+  if(!symbol_expr_lhs)
+    return simplify_exprt::simplify_inequality(expr);
+
+  if(!goto_symex_can_forward_propagatet(ns)(rhs))
+    return simplify_exprt::simplify_inequality(expr);
+
+  auto maybe_constant = try_evaluate_pointer_comparison(
+    expr.id(), *symbol_expr_lhs, rhs, value_set, language_mode, ns);
+  if(maybe_constant.has_value())
+    return changed(*maybe_constant);
+  else
+    return unchanged(expr);
+}

src/goto-symex/simplify_expr_with_value_set.h

@@ -0,0 +1,35 @@
+/*******************************************************************\
+
+Module: Variant of simplify_exprt that uses a value_sett
+
+Author: Michael Tautschnig
+
+\*******************************************************************/
+
+#ifndef CPROVER_GOTO_SYMEX_SIMPLIFY_EXPR_WITH_VALUE_SET_H
+#define CPROVER_GOTO_SYMEX_SIMPLIFY_EXPR_WITH_VALUE_SET_H
+
+#include <util/simplify_expr_class.h>
+
+class value_sett;
+
+class simplify_expr_with_value_sett : public simplify_exprt
+{
+public:
+  simplify_expr_with_value_sett(
+    const value_sett &_vs,
+    const namespacet &_ns,
+    const irep_idt &_mode)
+    : simplify_exprt(_ns), value_set(_vs), language_mode(_mode)
+  {
+  }
+
+  [[nodiscard]] resultt<>
+  simplify_inequality(const binary_relation_exprt &) override;
+
+protected:
+  const value_sett &value_set;
+  const irep_idt language_mode;
+};
+
+#endif // CPROVER_GOTO_SYMEX_SIMPLIFY_EXPR_WITH_VALUE_SET_H

src/goto-symex/symex_assign.cpp

@@ -15,6 +15,7 @@ Author: Daniel Kroening, [email protected]
 #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"

src/goto-symex/symex_builtin_functions.cpp

@@ -460,7 +460,10 @@ void goto_symext::symex_output(
   {
     renamedt<exprt, L2> l2_arg = state.rename(code.operands()[i], ns);
     if(symex_config.simplify_opt)
-      l2_arg.simplify(ns);
+    {
+      simplify_exprt simp{ns};
+      l2_arg.simplify(simp);
+    }
     args.emplace_back(l2_arg);
   }