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 #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/symex_goto.cpp

@@ -230,6 +230,15 @@ void goto_symext::symex_goto(statet &state)
 
     symex_transition(state, state_pc, backward);
 
+    // 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().second.value_set,
+      !backward ? &state.value_set : &goto_state_list.back().second.value_set,
+      ns);
+
     // produce new guard symbol
     exprt guard_expr;
 

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>
@@ -124,6 +125,12 @@ 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);
@@ -539,3 +546,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,
+  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);
+
+    // 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);
+    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(), symbol_type, "", ns));
+      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(), symbol_type, "", ns));
+      value_set_for_false_case->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.