Add --symex-cache-dereferences flag

This makes the dereference caching behaviour configurable

Author: Hannes Steffenhagen

jbmc/regression/jbmc/CMakeLists.txt

@@ -1,5 +1,5 @@
 add_test_pl_tests(
-    "$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation --validate-trace"
+    "$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation --validate-trace --symex-cache-dereferences"
 )
 
 if(DEFINED BDD_GUARDS)

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/CMakeLists.txt

@@ -6,21 +6,32 @@ else()
   set(gcc_only_string "")
 endif()
 
+# We run cbmc tests with dereference cache on by default. There are a handful
+# of tests (mostly tests that check SSA output) which that'd interefere with,
+# so we just exclude those here and run those few tests without dereference
+# caching.
 add_test_pl_tests(
-    "$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation" -X smt-backend ${gcc_only}
+    "$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation --symex-cache-dereferences" -X smt-backend -X no-dereference-cache ${gcc_only}
+)
+
+add_test_pl_profile(
+    "cbmc-no-dereference-cache"
+    "$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation"
+    "-C;-X;smt-backend;-I;no-dereference-cache;${gcc_only_string}"
+    "CORE"
 )
 
 add_test_pl_profile(
     "cbmc-paths-lifo"
-    "$<TARGET_FILE:cbmc> --paths lifo"
-    "-C;-X;thorough-paths;-X;smt-backend;-X;paths-lifo-expected-failure;${gcc_only_string}-s;paths-lifo"
+    "$<TARGET_FILE:cbmc> --paths lifo --symex-cache-dereferences"
+    "-C;-X;thorough-paths;-X;smt-backend;-X;paths-lifo-expected-failure;${gcc_only_string}-s;paths-lifo;-X;no-dereference-cache"
     "CORE"
 )
 
 add_test_pl_profile(
     "cbmc-cprover-smt2"
-    "$<TARGET_FILE:cbmc> --cprover-smt2"
-    "-C;-X;broken-smt-backend;-X;thorough-smt-backend;${gcc_only_string}-s;cprover-smt2"
+    "$<TARGET_FILE:cbmc> --cprover-smt2 --symex-cache-dereferences"
+    "-C;-X;broken-smt-backend;-X;thorough-smt-backend;${gcc_only_string}-s;cprover-smt2;-X;no-dereference-cache"
     "CORE"
 )
 

regression/cbmc/Makefile

@@ -10,13 +10,31 @@ GCC_ONLY =
 endif
 
 test:
-	@../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation" -X smt-backend $(GCC_ONLY)
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation --symex-cache-dereferences" \
+	   -X smt-backend \
+	   -X no-dereference-cache \
+	   $(GCC_ONLY)
+
+test-no-dereference-cache:
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation" \
+	  -X smt-backend \
+	  -I no-dereference-cache \
+	  $(GCC_ONLY)
 
 test-cprover-smt2:
-	@../test.pl -e -p -c "../../../src/cbmc/cbmc --cprover-smt2" -X broken-smt-backend -X thorough-smt-backend $(GCC_ONLY)
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --cprover-smt2 --symex-cache-dereferences" \
+	  -X broken-smt-backend \
+	  -X thorough-smt-backend \
+	  -X no-dereference-cache \
+	  $(GCC_ONLY)
 
 test-paths-lifo:
-	@../test.pl -e -p -c "../../../src/cbmc/cbmc --paths lifo" -X thorough-paths -X smt-backend -X paths-lifo-expected-failure $(GCC_ONLY)
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --paths lifo --symex-cache-dereferences" \
+	  -X thorough-paths \
+	  -X smt-backend \
+	  -X paths-lifo-expected-failure \
+	  -X no-dereference-cache \
+	  $(GCC_ONLY)
 
 tests.log: ../test.pl test
 

regression/cbmc/dereference-cache-flag/README.md

@@ -0,0 +1 @@
+This is just checking that the --symex-cache-dereferences flag actually turns dereference caching on

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

@@ -0,0 +1,15 @@
+CORE no-dereference-cache
+test.c
+--show-vcc
+\(main::1::p!0@1#2 = address_of
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+Note that dereference caching is turned ON by default
+in tests just to make sure that it doesn't break
+anything.
+
+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::dereference_cache!0#1 = 0
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+Note that dereference caching is turned ON by default in
+tests just to make sure that it doesn't break anything.

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);
+}

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/symex_config.h

@@ -55,6 +55,13 @@ 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.
+  ///   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

@@ -342,7 +342,7 @@ void goto_symext::dereference_rec(
     // would result in us referencing quantifier variables outside the scope of
     // the quantifier.
     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);

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")}
 {
 }