filter value sets at gotos and assumes

When a conditional change of control flow in goto-symex
(i.e. gotos and assumes), if there is a pointer-typed symbol
in the condition then try to filter its value set separately
for each branch based on which values are actually possible
on that branch. We only do this when there is only one
pointer-typed symbol in the condition.

The intention is to make the value-sets more accurate. In
particular, this lays the groundwork for dealing with
virtual method dispatch much more efficiently. See diffblue#2122
for an approach that was rejected. For example in java,
code like `x.equals(y)`, where `x` could point to an Object
or a String, gets turned into code like
```
if (x.@class_identifier == 'java.lang.Object')
    x . java.lang.Object.equals(y)
else if (x.@class_identifier == 'java.lang.String')
    x . java.lang.String.equals(y)
```
When symex goes into java.lang.String.equals it doesn't
filter the value-set so that `this` (which is `x`) only
points to the String, not the Object. This causes symex to
add complicated expressions to the formula for field accesses
to fields that x won't have if it points to an Object.

Author: Owen

src/goto-symex/goto_symex.h

@@ -333,6 +333,29 @@ class goto_symext
     const exprt &new_guard,
     const namespacet &ns);
 
+  /// Try to filter value sets based on whether possible values of a
+  /// pointer-typed symbol make the condition true or false. We only do this
+  /// when there is only one pointer-typed symbol in \p condition.
+  /// \param state: The current state
+  /// \param condition: The condition which is being evaluated, which it expects
+  ///   will not have been cleaned or renamed. In practice, it's fine if it has
+  ///   been cleaned and renamed up to level L1.
+  /// \param original_value_set: The value set we will read from
+  /// \param jump_taken_value_set: The value set that will be used when the
+  ///   condition is true, so we remove any elements which we can tell will
+  ///   make the condition false, or nullptr if this shouldn't be done
+  /// \param jump_not_taken_value_set: The value set that will be used when the
+  ///   condition is false, so we remove any elements which we can tell will
+  ///   make the condition true, or nullptr if this shouldn't be done
+  /// \param ns: A namespace
+  void try_filter_value_sets(
+    goto_symex_statet &state,
+    exprt condition,
+    const value_sett &original_value_set,
+    value_sett *jump_taken_value_set,
+    value_sett *jump_not_taken_value_set,
+    const namespacet &ns);
+
   virtual void vcc(
     const exprt &,
     const std::string &msg,

src/goto-symex/symex_goto.cpp

@@ -30,6 +30,27 @@ void goto_symext::apply_goto_condition(
   const exprt &new_guard,
   const namespacet &ns)
 {
+  // It would be better to call try_filter_value_sets after apply_condition,
+  // and pass nullptr for value sets which apply_condition successfully updated
+  // already. However, try_filter_value_sets calls rename to do constant
+  // propagation, and apply_condition can update the constant propagator. Since
+  // apply condition will never succeed on both jump_taken_state and
+  // jump_not_taken_state, it should be possible to pass a reference to an
+  // unmodified goto_statet to use for renaming. But renaming needs a
+  // goto_symex_statet, not just a goto_statet, and we only have access to one
+  // of those. A future improvement would be to split rename into two parts:
+  // one part on goto_symex_statet which is non-const and deals with
+  // l2 thread reads, and one part on goto_statet which is const and could be
+  // used in try_filter_value_sets.
+
+  try_filter_value_sets(
+    current_state,
+    original_guard,
+    jump_taken_state.value_set,
+    &jump_taken_state.value_set,
+    &jump_not_taken_state.value_set,
+    ns);
+
   jump_taken_state.apply_condition(new_guard, current_state, ns);
 
   // Try to find a negative condition that implies an equality constraint on

src/goto-symex/symex_main.cpp

@@ -15,6 +15,7 @@ Author: Daniel Kroening, [email protected]
 #include <memory>
 
 #include <util/exception_utils.h>
+#include <util/expr_iterator.h>
 #include <util/expr_util.h>
 #include <util/make_unique.h>
 #include <util/mathematical_expr.h>
@@ -130,6 +131,22 @@ void goto_symext::symex_assume(statet &state, const exprt &cond)
   simplified_cond = state.rename(std::move(simplified_cond), ns).get();
   do_simplify(simplified_cond);
 
+  // It would be better to call try_filter_value_sets after apply_condition,
+  // and pass nullptr for value sets which apply_condition successfully updated
+  // already. However, try_filter_value_sets calls rename to do constant
+  // propagation, and apply_condition can update the constant propagator. Since
+  // apply condition will never succeed on both jump_taken_state and
+  // jump_not_taken_state, it should be possible to pass a reference to an
+  // unmodified goto_statet to use for renaming. But renaming needs a
+  // goto_symex_statet, not just a goto_statet, and we only have access to one
+  // of those. A future improvement would be to split rename into two parts:
+  // one part on goto_symex_statet which is non-const and deals with
+  // l2 thread reads, and one part on goto_statet which is const and could be
+  // used in try_filter_value_sets.
+
+  try_filter_value_sets(
+    state, cond, state.value_set, &state.value_set, nullptr, ns);
+
   // apply_condition must come after rename because it might change the
   // constant propagator and the value-set and we read from those in rename
   state.apply_condition(simplified_cond, state, ns);
@@ -543,3 +560,157 @@ void goto_symext::symex_step(
     UNREACHABLE;
   }
 }
+
+/// Check if an expression only contains one unique symbol (possibly repeated
+/// multiple times)
+/// \param expr: The expression to examine
+/// \return If only one unique symbol occurs in \p expr then return it;
+///   otherwise return an empty optionalt
+static optionalt<symbol_exprt>
+find_unique_pointer_typed_symbol(const exprt &expr)
+{
+  optionalt<symbol_exprt> return_value;
+  for(auto it = expr.depth_cbegin(); it != expr.depth_cend(); ++it)
+  {
+    const symbol_exprt *symbol_expr = expr_try_dynamic_cast<symbol_exprt>(*it);
+    if(symbol_expr && can_cast_type<pointer_typet>(symbol_expr->type()))
+    {
+      // If we already have a potential return value, check if it is the same
+      // symbol, and return an empty optionalt if not
+      if(return_value && *symbol_expr != *return_value)
+      {
+        return {};
+      }
+      return_value = *symbol_expr;
+    }
+  }
+
+  // Either expr contains no pointer-typed symbols or it contains one unique
+  // pointer-typed symbol, possibly repeated multiple times
+  return return_value;
+}
+
+/// This is a simplified version of value_set_dereferencet::build_reference_to.
+/// It ignores the ID_dynamic_object case (which doesn't occur in goto-symex)
+/// and gives up for integer addresses and non-trivial symbols
+/// \param value_set_element: An element of a value-set
+/// \param type: the type of the expression that might point to
+///   \p value_set_element
+/// \return An expression for the value of the pointer indicated by \p
+///   value_set_element if it is easy to determine, or an empty optionalt
+///   otherwise
+static optionalt<exprt>
+value_set_element_to_expr(exprt value_set_element, pointer_typet type)
+{
+  const object_descriptor_exprt *object_descriptor =
+    expr_try_dynamic_cast<object_descriptor_exprt>(value_set_element);
+  if(!object_descriptor)
+  {
+    return {};
+  }
+
+  const exprt &root_object = object_descriptor->root_object();
+  const exprt &object = object_descriptor->object();
+
+  if(root_object.id() == ID_null_object)
+  {
+    return null_pointer_exprt{type};
+  }
+  else if(root_object.id() == ID_integer_address)
+  {
+    return {};
+  }
+  else
+  {
+    // We should do something like
+    // value_set_dereference::dereference_type_compare, which deals with
+    // arrays having types containing void
+    if(object_descriptor->offset().is_zero() && object.type() == type.subtype())
+    {
+      return address_of_exprt(object);
+    }
+    else
+    {
+      return {};
+    }
+  }
+}
+
+void goto_symext::try_filter_value_sets(
+  goto_symex_statet &state,
+  exprt condition,
+  const value_sett &original_value_set,
+  value_sett *jump_taken_value_set,
+  value_sett *jump_not_taken_value_set,
+  const namespacet &ns)
+{
+  condition = state.rename<L1>(std::move(condition), ns).get();
+
+  optionalt<symbol_exprt> symbol_expr =
+    find_unique_pointer_typed_symbol(condition);
+
+  if(!symbol_expr)
+  {
+    return;
+  }
+
+  const pointer_typet &symbol_type = to_pointer_type(symbol_expr->type());
+
+  value_setst::valuest value_set_elements;
+  original_value_set.get_value_set(*symbol_expr, value_set_elements, ns);
+
+  // Try evaluating the condition with the symbol replaced by a pointer to each
+  // one of its possible values in turn. If that leads to a true for some
+  // value_set_element then we can delete it from the value set that will be
+  // used if the condition is false, and vice versa.
+  for(const auto &value_set_element : value_set_elements)
+  {
+    optionalt<exprt> possible_value =
+      value_set_element_to_expr(value_set_element, symbol_type);
+
+    if(!possible_value)
+    {
+      continue;
+    }
+
+    exprt modified_condition(condition);
+
+    address_of_aware_replace_symbolt replace_symbol{};
+    replace_symbol.insert(*symbol_expr, *possible_value);
+    replace_symbol(modified_condition);
+
+    // This do_simplify() is needed for the following reason: if condition is
+    // `*p == a` and we replace `p` with `&a` then we get `*&a == a`. Suppose
+    // our constant propagation knows that `a` is `. Without this call to
+    // do_simplify(), state.rename() turns this into `*&a == 1` (because
+    // rename() doesn't do constant propagation inside addresses), which
+    // do_simplify() turns into `a == 1`, which cannot be evaluated as true
+    // without another round of constant propagation.
+    // It would be sufficient to replace this call to do_simplify() with
+    // something that just replaces `*&x` with `x` whenever it finds it.
+    do_simplify(modified_condition);
+
+    const bool record_events = state.record_events;
+    state.record_events = false;
+    modified_condition = state.rename(std::move(modified_condition), ns).get();
+    state.record_events = record_events;
+
+    do_simplify(modified_condition);
+
+    if(jump_taken_value_set && modified_condition.is_false())
+    {
+      value_sett::entryt *entry = const_cast<value_sett::entryt *>(
+        jump_taken_value_set->get_entry_for_symbol(
+          symbol_expr->get_identifier(), symbol_type, "", ns));
+      jump_taken_value_set->erase_value_from_entry(*entry, value_set_element);
+    }
+    else if(jump_not_taken_value_set && modified_condition.is_true())
+    {
+      value_sett::entryt *entry = const_cast<value_sett::entryt *>(
+        jump_not_taken_value_set->get_entry_for_symbol(
+          symbol_expr->get_identifier(), symbol_type, "", ns));
+      jump_not_taken_value_set->erase_value_from_entry(
+        *entry, value_set_element);
+    }
+  }
+}

src/pointer-analysis/value_set.cpp

@@ -1615,3 +1615,25 @@ exprt value_sett::make_member(
 
   return member_expr;
 }
+
+void value_sett::erase_value_from_entry(
+  entryt &entry,
+  const exprt &value_to_erase)
+{
+  std::vector<object_map_dt::key_type> keys_to_erase;
+
+  for(const auto &key_value : entry.object_map.read())
+  {
+    const auto &rhs_object = to_expr(key_value);
+    if(rhs_object == value_to_erase)
+    {
+      keys_to_erase.emplace_back(key_value.first);
+    }
+  }
+
+  DATA_INVARIANT(
+    keys_to_erase.size() == 1,
+    "value_sett::erase_value_from_entry() should erase exactly one value");
+
+  entry.object_map.write().erase(keys_to_erase[0]);
+}

src/pointer-analysis/value_set.h

@@ -473,6 +473,8 @@ class value_sett
     const std::string &suffix,
     const namespacet &ns) const;
 
+  void erase_value_from_entry(entryt &entry, const exprt &value_to_erase);
+
 protected:
   /// Reads the set of objects pointed to by `expr`, including making
   /// recursive lookups for dereference operations etc.