Add CSE dereference feature

Author: Hannes Steffenhagen

regression/cbmc/double_deref/README

@@ -25,3 +25,9 @@ double_deref_with_cast.desc -- a double-deref with an intervening cast (*(int*)*
 double_deref_with_member.desc -- a double-deref with an intervening member expression (p->field1->field2), should use a let-expression
 double_deref_with_pointer_arithmetic.desc -- a double-deref with intervening pointer arithmetic (p[idx1][idx2]), should use a let-expression
 *_single_alias.desc -- variants of the above where the first dereference points to a single possible object, so no let-expression is necessary
+
+Why no-dereference-cache?
+-------------------------
+
+Because these tests test for specific VCCs to do with multiple nested complex
+dereferences and the dereference caching rewrites these.

regression/cbmc/double_deref/double_deref.desc

@@ -1,4 +1,4 @@
-CORE
+CORE no-dereference-cache
 double_deref.c
 --show-vcc
 \{1\} \(main::1::pptr!0@1#2 = address_of\(main::1::ptr[12]!0@1\) \? main::argc!0@1#1 = [12] : main::argc!0@1#1 = [12]\)

regression/cbmc/double_deref/double_deref_with_cast.desc

@@ -1,4 +1,4 @@
-CORE
+CORE no-dereference-cache
 double_deref_with_cast.c
 --show-vcc
 \{1\} \(cast\(main::1::pptr!0@1#2, signedbv\[32\]\*\*\) = address_of\(main::1::ptr2!0@1\) \? main::argc!0@1#1 = 2 \: main::argc!0@1#1 = 1\)

regression/cbmc/double_deref/double_deref_with_member.desc

@@ -1,4 +1,4 @@
-CORE
+CORE no-dereference-cache
 double_deref_with_member.c
 --show-vcc
 ^\{1\} \(main::1::cptr!0@1#2 = address_of\(main::1::container2!0@1\) \? main::argc!0@1#1 = 2 : main::argc!0@1#1 = 1\)

regression/cbmc/double_deref/double_deref_with_pointer_arithmetic.desc

@@ -1,4 +1,4 @@
-CORE
+CORE no-dereference-cache
 double_deref_with_pointer_arithmetic.c
 --show-vcc
 ^\{-[0-9]+\} derefd_pointer::derefd_pointer!0#1 = \{ symex_dynamic::dynamic_object1#3\[\[0\]\], symex_dynamic::dynamic_object1#3\[\[1\]\] \}\[cast\(mod #source_location=""\(main::argc!0@1#1, 2\), signedbv\[64\]\)\]

regression/cbmc/double_deref/double_deref_with_pointer_arithmetic_single_alias.desc

@@ -1,4 +1,4 @@
-CORE
+CORE no-dereference-cache
 double_deref_with_pointer_arithmetic_single_alias.c
 --show-vcc
 \{1\} \(derefd_pointer::derefd_pointer!0#1 = address_of\(symex_dynamic::dynamic_object2\) \? main::argc!0@1#1 = 1 : symex::invalid_object!0#0 = main::argc!0@1#1\)

src/goto-symex/goto_state.cpp

@@ -12,6 +12,27 @@ Author: Romain Brenguier, [email protected]
 
 #include <util/format_expr.h>
 
+optionalt<symbol_exprt>
+dereference_cachet::lookup(const exprt &dereference) const
+{
+  auto it = cache.find(dereference);
+  if(it == cache.end())
+  {
+    return nullopt;
+  }
+  else
+  {
+    return {it->second};
+  }
+}
+
+void dereference_cachet::insert(
+  exprt new_cached_expr,
+  symbol_exprt new_cache_symbol)
+{
+  cache.emplace(std::move(new_cached_expr), std::move(new_cache_symbol));
+}
+
 /// Print the constant propagation map in a human-friendly format.
 /// This is primarily for use from the debugger; please don't delete me just
 /// because there aren't any current callers.

src/goto-symex/goto_state.h

@@ -12,6 +12,7 @@ Author: Romain Brenguier, [email protected]
 #ifndef CPROVER_GOTO_SYMEX_GOTO_STATE_H
 #define CPROVER_GOTO_SYMEX_GOTO_STATE_H
 
+#include <unordered_map>
 #include <util/sharing_map.h>
 
 #include <analyses/guard.h>
@@ -24,6 +25,19 @@ Author: Romain Brenguier, [email protected]
 // by the parent class.
 class goto_symex_statet;
 
+/// This is used for eliminating repeated complicated dereferences.
+/// This is pretty much just a simple wrapper around a map.
+/// \see goto_symext::dereference_rec
+struct dereference_cachet
+{
+private:
+  std::unordered_map<exprt, symbol_exprt, irep_hash> cache;
+
+public:
+  optionalt<symbol_exprt> lookup(const exprt &pointer) const;
+  void insert(exprt new_cached_pointer_expr, symbol_exprt new_cache_symbol);
+};
+
 /// Container for data that varies per program point, e.g. the constant
 /// propagator state, when state needs to branch. This is copied out of
 /// goto_symex_statet at a control-flow fork and then back into it at a
@@ -38,6 +52,8 @@ class goto_statet
   symex_level2t level2;
 
 public:
+  dereference_cachet dereference_cache;
+
   const symex_level2t &get_level2() const
   {
     return level2;

src/goto-symex/goto_symex.h

@@ -299,7 +299,12 @@ class goto_symext
   exprt make_auto_object(const typet &, statet &);
   virtual void dereference(exprt &, statet &, bool write);
 
-  void dereference_rec(exprt &, statet &, bool write);
+  symbol_exprt cache_dereference(exprt &dereference_result, statet &state);
+  void dereference_rec(
+    exprt &expr,
+    statet &state,
+    bool write,
+    bool is_in_quantifier);
   exprt address_arithmetic(
     const exprt &,
     statet &,

src/goto-symex/symex_dereference.cpp

@@ -17,11 +17,14 @@ Author: Daniel Kroening, [email protected]
 #include <util/exception_utils.h>
 #include <util/expr_iterator.h>
 #include <util/expr_util.h>
+#include <util/fresh_symbol.h>
 #include <util/invariant.h>
 #include <util/pointer_offset_size.h>
 
 #include <pointer-analysis/value_set_dereference.h>
 
+#include "expr_skeleton.h"
+#include "symex_assign.h"
 #include "symex_dereference_state.h"
 
 /// Transforms an lvalue expression by replacing any dereference operations it
@@ -71,7 +74,7 @@ exprt goto_symext::address_arithmetic(
 
     // there could be further dereferencing in the offset
     exprt offset=be.offset();
-    dereference_rec(offset, state, false);
+    dereference_rec(offset, state, false, false);
 
     result=plus_exprt(result, offset);
 
@@ -107,14 +110,14 @@ exprt goto_symext::address_arithmetic(
     // just grab the pointer, but be wary of further dereferencing
     // in the pointer itself
     result=to_dereference_expr(expr).pointer();
-    dereference_rec(result, state, false);
+    dereference_rec(result, state, false, false);
   }
   else if(expr.id()==ID_if)
   {
     if_exprt if_expr=to_if_expr(expr);
 
     // the condition is not an address
-    dereference_rec(if_expr.cond(), state, false);
+    dereference_rec(if_expr.cond(), state, false, false);
 
     // recursive call
     if_expr.true_case() =
@@ -131,7 +134,7 @@ exprt goto_symext::address_arithmetic(
   {
     // give up, just dereference
     result=expr;
-    dereference_rec(result, state, false);
+    dereference_rec(result, state, false, false);
 
     // turn &array into &array[0]
     if(result.type().id() == ID_array && !keep_array)
@@ -191,14 +194,68 @@ exprt goto_symext::address_arithmetic(
   return result;
 }
 
+symbol_exprt
+goto_symext::cache_dereference(exprt &dereference_result, statet &state)
+{
+  auto const cache_key = [&] {
+    auto cache_key =
+      state.field_sensitivity.apply(ns, state, dereference_result, false);
+    if(auto let_expr = expr_try_dynamic_cast<let_exprt>(dereference_result))
+    {
+      let_expr->value() = state.rename<L2>(let_expr->value(), ns).get();
+    }
+    else
+    {
+      cache_key = state.rename<L2>(cache_key, ns).get();
+    }
+    return cache_key;
+  }();
+
+  if(auto cached = state.dereference_cache.lookup(cache_key))
+  {
+    return *cached;
+  }
+
+  auto const &cache_symbol = get_fresh_aux_symbol(
+    cache_key.type(),
+    "symex",
+    "dereference_cache",
+    dereference_result.source_location(),
+    ID_C,
+    ns,
+    state.symbol_table);
+
+  // we need to lift possible lets
+  // (come from the value set to avoid repeating complex pointer comparisons)
+  auto cache_value = cache_key;
+  lift_lets(state, cache_value);
+
+  exprt::operandst guard{};
+  auto assign = symex_assignt{
+    state, symex_targett::assignment_typet::STATE, ns, symex_config, target};
+
+  assign.assign_symbol(
+    to_ssa_expr(state.rename<L1>(cache_symbol.symbol_expr(), ns).get()),
+    expr_skeletont{},
+    cache_value,
+    guard);
+
+  state.dereference_cache.insert(cache_key, cache_symbol.symbol_expr());
+  return cache_symbol.symbol_expr();
+}
+
 /// If \p expr is a \ref dereference_exprt, replace it with explicit references
 /// to the objects it may point to. Otherwise recursively apply this function to
 /// \p expr's operands, with special cases for address-of (handled by \ref
 /// goto_symext::address_arithmetic) and certain common expression patterns
 /// such as `&struct.flexible_array[0]` (see inline comments in code).
 /// For full details of this method's pointer replacement and potential side-
 /// effects see \ref goto_symext::dereference
-void goto_symext::dereference_rec(exprt &expr, statet &state, bool write)
+void goto_symext::dereference_rec(
+  exprt &expr,
+  statet &state,
+  bool write,
+  bool is_in_quantifier)
 {
   if(expr.id()==ID_dereference)
   {
@@ -221,7 +278,7 @@ void goto_symext::dereference_rec(exprt &expr, statet &state, bool write)
     tmp1.swap(to_dereference_expr(expr).pointer());
 
     // first make sure there are no dereferences in there
-    dereference_rec(tmp1, state, false);
+    dereference_rec(tmp1, state, false, is_in_quantifier);
 
     // Depending on the nature of the pointer expression, the recursive deref
     // operation might have introduced a construct such as
@@ -271,10 +328,29 @@ void goto_symext::dereference_rec(exprt &expr, statet &state, bool write)
       dereference.dereference(tmp1, symex_config.show_points_to_sets);
     // std::cout << "**** " << format(tmp2) << '\n';
 
-    expr.swap(tmp2);
 
     // this may yield a new auto-object
-    trigger_auto_object(expr, state);
+    trigger_auto_object(tmp2, state);
+
+    // If the dereference result is not a complicated expression
+    // (i.e. of the form
+    //   [let p = <expr> in ]
+    //   (p == &something ? something : ...))
+    // we should just return it unchanged.
+    // also if we are on the lhs of an assignment we should also not attempt to
+    // go to the cache we cannot do this for quantified expressions because this
+    // would result in us referencing quantifier variables outside the scope of
+    // the quantifier.
+    if(
+      !write && !is_in_quantifier &&
+      (tmp2.id() == ID_if || tmp2.id() == ID_let))
+    {
+      expr = cache_dereference(tmp2, state);
+    }
+    else
+    {
+      expr = tmp2;
+    }
   }
   else if(
     expr.id() == ID_index && to_index_expr(expr).array().id() == ID_member &&
@@ -293,7 +369,7 @@ void goto_symext::dereference_rec(exprt &expr, statet &state, bool write)
     tmp.add_source_location()=expr.source_location();
 
     // recursive call
-    dereference_rec(tmp, state, write);
+    dereference_rec(tmp, state, write, is_in_quantifier);
 
     expr.swap(tmp);
   }
@@ -331,17 +407,18 @@ void goto_symext::dereference_rec(exprt &expr, statet &state, bool write)
             to_address_of_expr(tc_op).object(),
             from_integer(0, index_type())));
 
-      dereference_rec(expr, state, write);
+      dereference_rec(expr, state, write, is_in_quantifier);
     }
     else
     {
-      dereference_rec(tc_op, state, write);
+      dereference_rec(tc_op, state, write, is_in_quantifier);
     }
   }
   else
   {
+    bool is_quantifier = expr.id() == ID_forall || expr.id() == ID_exists;
     Forall_operands(it, expr)
-      dereference_rec(*it, state, write);
+      dereference_rec(*it, state, write, is_in_quantifier || is_quantifier);
   }
 }
 
@@ -409,7 +486,7 @@ void goto_symext::dereference(exprt &expr, statet &state, bool write)
   });
 
   // start the recursion!
-  dereference_rec(expr, state, write);
+  dereference_rec(expr, state, write, false);
   // dereferencing may introduce new symbol_exprt
   // (like __CPROVER_memory)
   expr = state.rename<L1>(std::move(expr), ns).get();