Evaluate some pointer comparisons as true or false

Use the value-set to evaluate pointer comparisons as true or false
where possible

Author: Owen

src/goto-symex/renaming_level.h

@@ -15,7 +15,9 @@ Author: Romain Brenguier, [email protected]
 #include <map>
 #include <unordered_set>
 
+#include <util/expr_iterator.h>
 #include <util/irep.h>
+#include <util/range.h>
 #include <util/simplify_expr.h>
 #include <util/ssa_expr.h>
 
@@ -87,20 +89,50 @@ class renamedt
     (void)::simplify(value, ns);
   }
 
+  typedef std::function<optionalt<renamedt<exprt, level>>(const exprt &)>
+    expr_mutator_functiont;
+
+  /// This permits replacing subexpressions of the renamed value, so long as
+  /// each replacement is consistent with our current renaming level (for
+  /// example, replacing subexpressions of L2 expressions with ones which are
+  /// themselves L2 renamed).
+  /// The passed function will be called with each expression node in preorder
+  /// (i.e. parent expressions before children), and should return an empty
+  /// optional to make no change or a renamed expression to make a change.
+  void selectively_mutate(expr_mutator_functiont get_mutated_expr)
+  {
+    for(
+      auto it = value.depth_begin(), itend = value.depth_end();
+      it != itend;
+      ++it)
+    {
+      auto replacement = get_mutated_expr(*it);
+      if(replacement)
+        it.mutate() = replacement->get();
+    }
+  }
+
 private:
   underlyingt value;
 
   friend struct symex_level0t;
   friend struct symex_level1t;
   friend struct symex_level2t;
   friend class goto_symex_statet;
+  template <levelt make_renamed_level>
+  friend renamedt<exprt, make_renamed_level> make_renamed(constant_exprt constant);
 
   /// Only the friend classes can create renamedt objects
   explicit renamedt(underlyingt value) : value(std::move(value))
   {
   }
 };
 
+template <levelt level>
+renamedt<exprt, level> make_renamed(constant_exprt constant) {
+  return renamedt<exprt, level>(std::move(constant));
+}
+
 /// Functor to set the level 0 renaming of SSA expressions.
 /// Level 0 corresponds to threads.
 /// The renaming is built for one particular interleaving.

src/goto-symex/symex_goto.cpp

@@ -10,6 +10,7 @@ Author: Daniel Kroening, [email protected]
 /// Symbolic Execution
 
 #include "goto_symex.h"
+#include "goto_symex_is_constant.h"
 
 #include <algorithm>
 
@@ -20,6 +21,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/std_expr.h>
 
 #include <util/simplify_expr.h>
+#include <pointer-analysis/value_set_dereference.h>
 
 void goto_symext::apply_goto_condition(
   goto_symex_statet &current_state,
@@ -65,6 +67,172 @@ void goto_symext::apply_goto_condition(
   }
 }
 
+/// Try to evaluate a simple pointer comparison.
+/// \param [in,out] condition: An L2- renamed expression of the form
+///   "symbol_expr == other" or "symbol_expr != other" (or one of those with
+///   the lhs and rhs swapped)
+/// \param symbol_expr: The symbol expression in the condition
+/// \param other_operand: The other expression in the condition - must pass
+///   goto_symex_is_constant, and since it is pointer-typed it must therefore
+///   be an address of expression, a typecast of an address of expression or a
+///   null pointer
+/// \param value_set: The value-set for looking up what the symbol can point to
+/// \param language_mode: The language mode
+/// \param ns: A namespace
+static optionalt<renamedt<exprt, L2>>
+try_evaluate_pointer_comparison(
+  irep_idt operation,
+  const symbol_exprt &symbol_expr,
+  const exprt &other_operand,
+  const value_sett &value_set,
+  const irep_idt language_mode,
+  const namespacet &ns)
+{
+  const exprt *other_operand_with_typecasts_removed = &other_operand;
+  const typecast_exprt *typecast_expr = expr_try_dynamic_cast<typecast_exprt>(
+    *other_operand_with_typecasts_removed);
+
+  while(typecast_expr)
+  {
+    other_operand_with_typecasts_removed = &typecast_expr->op();
+    typecast_expr = expr_try_dynamic_cast<typecast_exprt>(
+      *other_operand_with_typecasts_removed);
+  }
+
+  const constant_exprt *constant_expr =
+    expr_try_dynamic_cast<constant_exprt>(other_operand);
+
+  INVARIANT(
+    other_operand_with_typecasts_removed->id() == ID_address_of ||
+      (constant_expr && constant_expr->get_value() == ID_NULL),
+    "An expression that passes goto_symex_is_constant and has "
+    "pointer-type must be an address of expression (possibly with some "
+    "typecasts) or a null pointer");
+
+  const ssa_exprt *ssa_symbol_expr =
+    expr_try_dynamic_cast<ssa_exprt>(symbol_expr);
+
+  value_setst::valuest value_set_elements;
+  value_set.get_value_set(
+    ssa_symbol_expr->get_l1_object(), value_set_elements, ns);
+
+  bool constant_found = false;
+
+  for(const auto &value_set_element : value_set_elements)
+  {
+    if(
+      value_set_element.id() == ID_unknown ||
+      value_set_element.id() == ID_invalid)
+    {
+      // If ID_unknown or ID_invalid are in the value-set then we can't
+      // conclude anything about it
+      return {};
+    }
+
+    if(!constant_found)
+    {
+      optionalt<exprt> reference =
+        value_set_dereferencet::build_reference_to_value_set_element(
+          value_set_element,
+          symbol_expr,
+          to_pointer_type(symbol_expr.type()),
+          language_mode,
+          ns);
+
+      if(reference && *reference == other_operand)
+      {
+        constant_found = true;
+        // We can't break because we have to make sure we find any instances of
+        // ID_unknown or ID_invalid
+      }
+    }
+  }
+
+  if(!constant_found)
+  {
+    // The symbol cannot possibly have the value \p other_operand because it
+    // isn't in the symbol's value-set
+    return operation == ID_equal ? make_renamed<L2>(false_exprt{})
+                                            : make_renamed<L2>(true_exprt{});
+  }
+  else if(value_set_elements.size() == 1)
+  {
+    // The symbol must have the value \p other_operand because it is the only
+    // thing in the symbol's value-set
+    return operation == ID_equal ? make_renamed<L2>(true_exprt{})
+                                            : make_renamed<L2>(false_exprt{});
+  }
+  else
+  {
+    return {};
+  }
+}
+
+/// Check if we have a simple pointer comparison, and if so try to evaluate it.
+/// \param [in,out] condition: An L2- renamed expression of the form
+///   "symbol_expr == other" or "symbol_expr != other" (or one of those with
+///   the lhs and rhs swapped)
+/// \param symbol_expr: The symbol expression in the condition
+/// \param other_operand: The other expression in the condition - must pass
+///   goto_symex_is_constant, and since it is pointer-typed it must therefore
+///   be an address of expression, a typecast of an address of expression or a
+///   null pointer
+/// \param value_set: The value-set for looking up what the symbol can point to
+/// \param language_mode: The language mode
+/// \param ns: A namespace
+static optionalt<renamedt<exprt, L2>>
+try_evaluate_pointer_comparison(
+  const exprt &expr,
+  const value_sett &value_set,
+  const irep_idt language_mode,
+  const namespacet &ns)
+{
+  if(expr.id() != ID_equal && expr.id() != ID_notequal)
+    return {};
+
+  if(!can_cast_type<pointer_typet>(expr.op0().type()))
+    return {};
+
+  exprt lhs = expr.op0(), rhs = expr.op1();
+  if(can_cast_expr<symbol_exprt>(rhs))
+    std::swap(lhs, rhs);
+
+  const symbol_exprt *symbol_expr_lhs =
+    expr_try_dynamic_cast<symbol_exprt>(lhs);
+
+  if(!symbol_expr_lhs)
+    return {};
+
+  if(!goto_symex_is_constantt()(rhs))
+    return {};
+
+  return try_evaluate_pointer_comparison(
+    expr.id(), *symbol_expr_lhs, rhs, value_set, language_mode, ns);
+}
+
+/// Try to evaluate pointer comparisons where they can be trivially determined
+/// using the value-set.
+/// \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
+static renamedt<exprt, L2> try_evaluate_pointer_comparisons(
+  renamedt<exprt, L2> condition,
+  const value_sett &value_set,
+  const irep_idt language_mode,
+  const namespacet &ns)
+{
+  condition.selectively_mutate(
+    [&value_set, &language_mode, &ns](const exprt &expr) {
+      return try_evaluate_pointer_comparison(
+        expr, value_set, language_mode, ns);
+    });
+
+  return condition;
+}
+
 void goto_symext::symex_goto(statet &state)
 {
   const goto_programt::instructiont &instruction=*state.source.pc;
@@ -73,6 +241,8 @@ void goto_symext::symex_goto(statet &state)
   clean_expr(new_guard, state, false);
 
   renamedt<exprt, L2> renamed_guard = state.rename(std::move(new_guard), ns);
+  renamed_guard = try_evaluate_pointer_comparisons(
+    std::move(renamed_guard), state.value_set, language_mode, ns);
   if(symex_config.simplify_opt)
     renamed_guard.simplify(ns);
   new_guard = renamed_guard.get();