Add --symex-cache-dereferences flag

This makes the dereference caching behaviour configurable

Author: Hannes Steffenhagen

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -425,6 +425,9 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
     options.set_option("validate-goto-model", true);
   }
 
+  options.set_option(
+    "symex-cache-dereferences", cmdline.isset("symex-cache-dereferences"));
+
   PARSE_OPTIONS_GOTO_TRACE(cmdline, options);
 
   if(cmdline.isset("no-lazy-methods"))

regression/cbmc/Makefile

@@ -34,4 +34,4 @@ tests.log: ../test.pl test
 clean:
 	find . -name '*.out' -execdir $(RM) '{}' \;
 	find . -name '*.smt2' -execdir $(RM) '{}' \;
-	$(RM) tests*.log
+	$(RM) tests*.log tests-paths-lifo.log tests-cprover-smt2.log

regression/cbmc/dereference-cache-flag/test-no-cache.desc

@@ -0,0 +1,14 @@
+CORE
+test.c
+--show-vcc
+\(main::1::p!0@1#2 = address_of
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+This is just checking that the --symex-cache-dereferences flag actually turns
+dereference caching on and off.
+
+I would like to match the expression more precisely, but the order of
+comparisons for address of depends on platform-specific logic (unordered_xxx),
+and the corresponding regex would look ridiculous.

regression/cbmc/dereference-cache-flag/test-with-cache.desc

@@ -0,0 +1,10 @@
+CORE
+test.c
+--show-vcc --symex-cache-dereferences
+symex::dereference_cache!0#1 = 0
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+This is just checking that the --symex-cache-dereferences flag actually
+turns dereference caching on.

regression/cbmc/dereference-cache-flag/test.c

@@ -0,0 +1,7 @@
+#include <assert.h>
+
+int main(void)
+{
+  int cond, x, y, *p = cond ? &x : &y;
+  assert(*p == 0);
+}

regression/cbmc/double_deref/README

@@ -25,9 +25,3 @@ 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 no-dereference-cache
+CORE
 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 no-dereference-cache
+CORE
 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 no-dereference-cache
+CORE
 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 no-dereference-cache
+CORE
 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 no-dereference-cache
+CORE
 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/cbmc/cbmc_parse_options.cpp

@@ -342,6 +342,9 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
       "max-node-refinement",
       cmdline.get_value("max-node-refinement"));
 
+  options.set_option(
+    "symex-cache-dereferences", cmdline.isset("symex-cache-dereferences"));
+
   if(cmdline.isset("incremental-loop"))
   {
     options.set_option(

src/goto-checker/bmc_util.h

@@ -197,7 +197,8 @@ void run_property_decider(
   "(incremental-loop):" \
   "(unwind-min):" \
   "(unwind-max):" \
-  "(ignore-properties-before-unwind-min)"
+  "(ignore-properties-before-unwind-min)" \
+  "(symex-cache-dereferences)" \
 
 #define HELP_BMC \
   " --paths [strategy]           explore paths one at a time\n" \
@@ -251,7 +252,8 @@ void run_property_decider(
   "                              iteration are allowed to fail due to\n" \
   "                              complexity violations before the loop\n" \
   "                              gets blacklisted\n" \
-  " --graphml-witness filename   write the witness in GraphML format to filename\n" // NOLINT(*)
+  " --graphml-witness filename   write the witness in GraphML format to filename\n" /* NOLINT(*) */ \
+  " --symex-cache-dereferences   enable caching of repeated dereferences" \
 // clang-format on
 
 #endif // CPROVER_GOTO_CHECKER_BMC_UTIL_H

src/goto-symex/goto_state.h

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

src/goto-symex/symex_config.h

@@ -55,6 +55,14 @@ struct symex_configt final
   /// enables certain analyses that otherwise aren't run.
   bool complexity_limits_active;
 
+  /// \brief Whether or not to replace multiple occurrences of the same
+  ///   dereference with a single symbol that contains the result of that
+  ///   dereference. Can sometimes lead to a significant performance
+  ///   improvement, but sometimes also makes things worse.
+  ///   See https://github.com/diffblue/cbmc/pull/5964 for performance data.
+  ///   Used in goto_symext::dereference_rec
+  bool cache_dereferences;
+
   /// \brief Construct a symex_configt using options specified in an
   /// \ref optionst
   explicit symex_configt(const optionst &options);

src/goto-symex/symex_dereference.cpp

@@ -221,7 +221,7 @@ goto_symext::cache_dereference(exprt &dereference_result, statet &state)
     "symex",
     "dereference_cache",
     dereference_result.source_location(),
-    ID_C,
+    language_mode,
     ns,
     state.symbol_table);
 
@@ -230,25 +230,29 @@ goto_symext::cache_dereference(exprt &dereference_result, statet &state)
   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};
 
+  auto cache_symbol_expr = cache_symbol.symbol_expr();
   assign.assign_symbol(
-    to_ssa_expr(state.rename<L1>(cache_symbol.symbol_expr(), ns).get()),
+    to_ssa_expr(state.rename<L1>(cache_symbol_expr, ns).get()),
     expr_skeletont{},
     cache_value,
-    guard);
+    {});
 
-  state.dereference_cache.insert(cache_key, cache_symbol.symbol_expr());
-  return cache_symbol.symbol_expr();
+  state.dereference_cache.insert(cache_key, cache_symbol_expr);
+  return cache_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).
+/// Note that \p write is used to alter behaviour when this function is
+/// operating on the LHS of an assignment. Similarly \p is_in_quantifier
+/// indicates when the dereference is inside a quantifier (related to scoping
+/// when dereference caching is enabled).
 /// For full details of this method's pointer replacement and potential side-
 /// effects see \ref goto_symext::dereference
 void goto_symext::dereference_rec(
@@ -332,24 +336,24 @@ void goto_symext::dereference_rec(
     // this may yield a new auto-object
     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.
+    // Check various conditions for when we should try to cache the expression.
+    // 1. Caching dereferences must be enabled.
+    // 2. Do not cache inside LHS of writes.
+    // 3. Do not cache inside quantifiers (references variables outside their
+    //    scope).
+    // 4. Only cache "complicated" expressions, i.e. of the form
+    //     [let p = <expr> in ]
+    //     (p == &something ? something : ...))
+    // Otherwise we should just return it unchanged.
     if(
-      !write && !is_in_quantifier &&
+      symex_config.cache_dereferences && !write && !is_in_quantifier &&
       (tmp2.id() == ID_if || tmp2.id() == ID_let))
     {
       expr = cache_dereference(tmp2, state);
     }
     else
     {
-      expr = tmp2;
+      expr = std::move(tmp2);
     }
   }
   else if(

src/goto-symex/symex_main.cpp

@@ -56,7 +56,8 @@ symex_configt::symex_configt(const optionst &options)
                 "max-field-sensitivity-array-size")
             : DEFAULT_MAX_FIELD_SENSITIVITY_ARRAY_SIZE),
     complexity_limits_active(
-      options.get_signed_int_option("symex-complexity-limit") > 0)
+      options.get_signed_int_option("symex-complexity-limit") > 0),
+    cache_dereferences{options.get_bool_option("symex-cache-dereferences")}
 {
 }