Introduce value-set supported simplifier for goto-symex

regression/cbmc/pointer-offset-02/main.c

@@ -0,0 +1,7 @@
+#include <stdlib.h>
+
+int main()
+{
+  int *p = malloc(sizeof(int));
+  __CPROVER_assert(__CPROVER_POINTER_OFFSET(p) == 0, "");
+}

regression/cbmc/pointer-offset-02/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--verbosity 8
+^Generated \d+ VCC\(s\), 0 remaining after simplification$
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

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

@@ -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 &&
@@ -160,9 +163,12 @@ 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_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();
@@ -181,14 +187,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)
           {
@@ -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, [email protected]
 
 #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
@@ -876,20 +877,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

@@ -24,6 +24,7 @@ Author: Daniel Kroening, [email protected]
 #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);
@@ -32,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);
@@ -85,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