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

@@ -308,6 +308,28 @@ class goto_symext
   virtual void symex_other(statet &state);
 
   void symex_assert(const goto_programt::instructiont &, statet &);
+  
+  /// 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 value_set_for_true_case: A pointer to the value set that possible
+  ///   values should be removed from if they make the condition false, or
+  ///   nullptr if this shouldn't be done
+  /// \param value_set_for_false_case: A pointer to the value set that possible
+  ///   values should be removed from if they 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,
+    value_sett *value_set_for_true_case,
+    value_sett *value_set_for_false_case,
+    const namespacet &ns);
+
   virtual void vcc(
     const exprt &,
     const std::string &msg,

src/goto-symex/symex_goto.cpp

@@ -20,6 +20,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/std_expr.h>
 
 #include <analyses/dirty.h>
+#include <util/replace_symbol.h>
 #include <util/simplify_expr.h>
 
 void goto_symext::symex_goto(statet &state)
@@ -214,6 +215,18 @@ void goto_symext::symex_goto(statet &state)
 
   symex_transition(state, state_pc, backward);
 
+  if(!new_guard.is_true())
+  {
+    // update our value-set when particular objects are only compatible with
+    // one or other branch
+    try_filter_value_sets(
+      state,
+      instruction.get_condition(),
+      backward ? &state.value_set : &goto_state_list.back().value_set,
+      !backward ? &state.value_set : &goto_state_list.back().value_set,
+      ns);
+  }
+
   // adjust guards
   if(new_guard.is_true())
   {

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>
@@ -125,6 +126,13 @@ void goto_symext::vcc(
 
 void goto_symext::symex_assume(statet &state, const exprt &cond)
 {
+  if(!cond.is_false())
+  {
+    // try to update the value sets using information contained in the guard
+    try_filter_value_sets(
+      state, cond, &state.value_set, nullptr, ns);
+  }
+
   exprt simplified_cond=cond;
 
   clean_expr(simplified_cond, state, false);
@@ -534,3 +542,148 @@ 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,
+  value_sett *value_set_for_true_case,
+  value_sett *value_set_for_false_case,
+  const namespacet &ns)
+{
+  condition = state.rename<L1>(std::move(condition), ns);
+
+  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;
+  state.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);
+
+    do_simplify(modified_condition);
+
+    const bool record_events=state.record_events;
+    state.record_events=false;
+    modified_condition = state.rename(std::move(modified_condition), ns);
+    state.record_events=record_events;
+
+    do_simplify(modified_condition);
+
+    if(value_set_for_true_case && modified_condition.is_false())
+    {
+      value_sett::entryt *entry = const_cast<value_sett::entryt *>(
+        value_set_for_true_case->get_entry_for_symbol(
+          symbol_expr->get_identifier(), ns.follow(symbol_type), ""));
+      value_set_for_true_case->erase_value_from_entry(
+        *entry, value_set_element);
+    }
+    else if(value_set_for_false_case && modified_condition.is_true())
+    {
+      value_sett::entryt *entry = const_cast<value_sett::entryt *>(
+        value_set_for_false_case->get_entry_for_symbol(
+          symbol_expr->get_identifier(), ns.follow(symbol_type), ""));
+      value_set_for_false_case->erase_value_from_entry(
+        *entry, value_set_element);
+    }
+  }
+}

src/pointer-analysis/value_set.cpp

@@ -1607,3 +1607,22 @@ 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.empty(), "erase_value() should erase at least one value");
+  for(const auto &key : keys_to_erase)
+  {
+    entry.object_map.write().erase(key);
+  }
+}

src/pointer-analysis/value_set.h

@@ -465,6 +465,8 @@ class value_sett
     const typet &expr_type,
     const std::string &suffix) 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.