Don't use let-bound temporaries for simple pointers

For example, we're willing to directly quote `p`, `(type *)p`, `p[some_constant]`
and other simple expressions directly when comparing a pointer against its possible
aliases-- the case we really must prevent is a large if-expression like
`q == &o1 ? o1 : q == &o2 ? o2 : ...` that can result from a nested dereference --
in this case we must use a let-bound temporary to avoid producing a very large expression
that can founder subsequent algorithms such as simplification, renaming and irep-merging.

Author: smowton

src/pointer-analysis/value_set_dereference.cpp

@@ -22,6 +22,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/c_types.h>
 #include <util/config.h>
 #include <util/cprover_prefix.h>
+#include <util/expr_iterator.h>
 #include <util/format_type.h>
 #include <util/fresh_symbol.h>
 #include <util/options.h>
@@ -30,6 +31,30 @@ Author: Daniel Kroening, [email protected]
 #include <util/simplify_expr.h>
 #include <util/ssa_expr.h>
 
+/// Returns true if \p expr is complicated enough that a local definition (using
+/// a let expression) is preferable to repeating it, potentially many times.
+/// Of course this is just a heuristic -- currently we allow any expression that
+/// only involves one symbol, such as "x", "(type*)x", "x[0]" (but not "x[y]").
+/// Particularly we want to make sure to insist on a local definition of \p expr
+/// is a large if-expression, such as `p == &o1 ? o1 : p == &o2 ? o2 : ...`, as
+/// can result from dereferencing a subexpression.
+static bool should_use_local_definition_for(const exprt &expr)
+{
+  bool seen_symbol = false;
+  for(auto it = expr.depth_begin(), itend = expr.depth_end(); it != itend; ++it)
+  {
+    if(it->id() == ID_symbol)
+    {
+      if(seen_symbol)
+        return true;
+      else
+        seen_symbol = true;
+    }
+  }
+
+  return false;
+}
+
 exprt value_set_dereferencet::dereference(const exprt &pointer)
 {
   if(pointer.type().id()!=ID_pointer)
@@ -78,7 +103,7 @@ exprt value_set_dereferencet::dereference(const exprt &pointer)
 
   exprt compare_against_pointer = pointer;
 
-  if(pointer.id() != ID_symbol && retained_values.size() >= 2)
+  if(retained_values.size() >= 2 && should_use_local_definition_for(pointer))
   {
     symbolt fresh_binder = get_fresh_aux_symbol(
       pointer.type(),