filter value sets at gotos and assumes

Author: Owen

src/goto-symex/goto_symex.h

@@ -225,6 +225,25 @@ class goto_symext
   virtual void symex_dead(statet &);
   virtual void symex_other(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
+  /// \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)
@@ -224,6 +225,18 @@ void goto_symext::symex_goto(statet &state)
 
   symex_transition(state, state_pc, backward);
 
+  if(!new_guard.is_true())
+  {
+    // try to update the value sets using information contained in which branch
+    // is being taken
+    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

@@ -133,9 +133,15 @@ void goto_symext::symex_assume(statet &state, const exprt &cond)
   else
     state.guard.add(simplified_cond);
 
-  if(state.atomic_section_id!=0 &&
-     state.guard.is_false())
+  if(state.atomic_section_id != 0 && state.guard.is_false())
     symex_atomic_end(state);
+
+  if(!simplified_cond.is_false())
+  {
+    // try to update the value sets using information contained in the guard
+    try_filter_value_sets(
+      state, simplified_cond, &state.value_set, nullptr, ns);
+  }
 }
 
 void goto_symext::rewrite_quantifiers(exprt &expr, statet &state)
@@ -519,3 +525,115 @@ void goto_symext::symex_step(
     UNREACHABLE;
   }
 }
+
+/// Collect all sub-expressions of an expression that are pointer-typed symbols
+/// \param expr: The expression to examine
+/// \param [out] output: The set to put the results into
+static void
+collect_pointer_typed_symbols(const exprt &expr, std::set<symbol_exprt> &output)
+{
+  const symbol_exprt *symbol_expr = expr_try_dynamic_cast<symbol_exprt>(expr);
+  if(symbol_expr && can_cast_type<pointer_typet>(symbol_expr->type()))
+  {
+    output.insert(*symbol_expr);
+  }
+
+  for(const exprt &op : expr.operands())
+  {
+    collect_pointer_typed_symbols(op, output);
+  }
+}
+
+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<goto_symex_statet::L1>(std::move(condition), ns);
+
+  std::set<symbol_exprt> pointer_typed_symbols{};
+  collect_pointer_typed_symbols(condition, pointer_typed_symbols);
+
+  if(pointer_typed_symbols.size() == 1)
+  {
+    const symbol_exprt &symbol_expr = *pointer_typed_symbols.begin();
+    const pointer_typet &symbol_type = to_pointer_type(symbol_expr.type());
+
+    // If symbol_expr has already been L2-renamed then we need to strip it back
+    // to L1-renaming for the purposes of getting its value set
+    const symbol_exprt symbol_expr_l1 =
+      is_ssa_expr(symbol_expr) ? to_ssa_expr(symbol_expr).get_l1_object()
+                               : symbol_expr;
+    value_setst::valuest possible_values;
+    state.value_set.get_value_set(symbol_expr_l1, possible_values, ns);
+
+    // Try evaluating the condition with symbol_expr pointing to each one of
+    // its possible values in turn. If that leads to a true from o1 then we can
+    // delete that o1 from the value set that will be used if the condition is
+    // false, and vice versa.
+    for(const auto &possible_value : possible_values)
+    {
+      if(!can_cast_expr<object_descriptor_exprt>(possible_value))
+      {
+        continue;
+      }
+
+      object_descriptor_exprt o = to_object_descriptor_expr(possible_value);
+
+      const exprt &root_object = o.root_object();
+      const exprt &object = o.object();
+      exprt value_for_symbol_expr;
+
+      if(root_object.id() == ID_null_object)
+      {
+        value_for_symbol_expr = null_pointer_exprt{symbol_type};
+      }
+      else if(root_object.id() == ID_integer_address)
+      {
+        continue;
+      }
+      else
+      {
+        // We should do something like
+        // value_set_dereference::dereference_type_compare, which deals with
+        // arrays having types containing void
+        if(o.offset().is_zero() && object.type() == symbol_type.subtype())
+        {
+          value_for_symbol_expr = address_of_exprt(object);
+        }
+        else
+        {
+          continue;
+        }
+      }
+
+      exprt modified_condition(condition);
+
+      replace_symbolt replace_symbol{};
+      replace_symbol.insert(symbol_expr, value_for_symbol_expr);
+      replace_symbol(modified_condition);
+
+      do_simplify(modified_condition);
+      modified_condition = state.rename(std::move(modified_condition), ns);
+      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_l1.get_identifier(), ns.follow(symbol_type), ""));
+        value_set_for_true_case->erase_value_from_entry(*entry, possible_value);
+      }
+      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_l1.get_identifier(), ns.follow(symbol_type), ""));
+        value_set_for_false_case->erase_value_from_entry(
+          *entry, possible_value);
+      }
+    }
+  }
+}

src/pointer-analysis/value_set.cpp

@@ -1611,3 +1611,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

@@ -452,6 +452,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.