Use BDDs for encoding symex guards

.travis.yml

@@ -201,7 +201,7 @@ jobs:
         - cmake --build build -- -j4
       script: (cd build; bin/unit "[core][irept]")
 
-    # cmake build using g++-7, enable CMAKE_USE_CUDD
+    # cmake build using g++-7, enable CMAKE_USE_CUDD and BDD_GUARDS
     - stage: Test different OS/CXX/Flags
       os: linux
       sudo: false
@@ -223,7 +223,7 @@ jobs:
       install:
         - ccache -z
         - ccache --max-size=1G
-        - cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release'  '-DCMAKE_CXX_COMPILER=/usr/bin/g++-7' '-DCMAKE_USE_CUDD=true'
+        - cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release'  '-DCMAKE_CXX_COMPILER=/usr/bin/g++-7' '-DCMAKE_USE_CUDD=true' -DCMAKE_CXX_FLAGS="-DBDD_GUARDS"
         - git submodule update --init --recursive
         - cmake --build build -- -j4
       script: (cd build; ctest -V -L CORE -j2)

COMPILING.md

@@ -310,3 +310,22 @@ If compiling with cmake:
    ```
    cmake --build build
    ```
+
+## Use BDDs for guards
+
+There are two implementation for symex guards. The default one uses the
+internal representation of expression. The other one uses BDDs and
+though experimental, it is expected to have better performance,
+in particular when used in conjunction with CUDD.
+
+To use the BDD implementation of guards, add the `BDD_GUARDS`
+compilation flag:
+  * If compiling with make:
+    ```
+    make -C src CXXFLAGS="-O2 -DBDD_GUARDS"
+    ```
+  * If compiling with CMake:
+    ```
+    cmake -H. -Bbuild -DCMAKE_CXX_FLAGS="-DBDD_GUARDS"
+    ```
+    and then `cmake --build build`

jbmc/regression/jbmc/CMakeLists.txt

@@ -2,9 +2,18 @@ add_test_pl_tests(
     "$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation"
 )
 
-add_test_pl_profile(
-    "jbmc-symex-driven-lazy-loading"
-    "$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading"
-    "-C;-X;symex-driven-lazy-loading-expected-failure;-s;symex-driven-loading"
-    "CORE"
-)
+if(DEFINED BDD_GUARDS)
+    add_test_pl_profile(
+            "jbmc-symex-driven-lazy-loading"
+            "$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading"
+            "-C;-X;symex-driven-lazy-loading-expected-failure;-s;symex-driven-loading"
+            "CORE"
+    )
+else()
+    add_test_pl_profile(
+            "jbmc-symex-driven-lazy-loading"
+            "$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading"
+            "-C;-X;symex-driven-lazy-loading-expected-failure;-X;bdd-expected-timeout;-s;symex-driven-loading"
+            "CORE"
+    )
+endif()

jbmc/regression/jbmc/Makefile

@@ -4,11 +4,19 @@ include ../../src/config.inc
 
 test:
 	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
+ifeq ($(filter %DBDD_GUARDS, $(CXXFLAGS)),)
 	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
+else
+	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -X bdd-expected-timeout -s symex-driven-loading
+endif
 
 tests.log: ../$(CPROVER_DIR)/regression/test.pl
 	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
+ifeq ($(filter %DBDD_GUARDS, $(CXXFLAGS)),)
 	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
+else
+	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -X bdd-expected-timeout -s symex-driven-loading
+endif
 
 show:
 	@for dir in *; do \

jbmc/regression/jbmc/class-literals/test.desc

@@ -1,8 +1,13 @@
-CORE
+CORE bdd-expected-timeout
 Test.class
 --function Test.main
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
+--
+This test is deactivated for the build with BDDs because it takes more
+than 10 minutes for the test to complete.
+This is due to the size of the BDD representing the guards growing more than
+they do when represented as exprt.

src/analyses/CMakeLists.txt

@@ -3,4 +3,8 @@ add_library(analyses ${sources})
 
 generic_includes(analyses)
 
-target_link_libraries(analyses util pointer-analysis)
+if(CMAKE_USE_CUDD)
+    target_include_directories(analyses PUBLIC ${CUDD_INCLUDE}/cudd/)
+endif()
+
+target_link_libraries(analyses util pointer-analysis solvers)

src/analyses/Makefile

@@ -12,6 +12,8 @@ SRC = ai.cpp \
       global_may_alias.cpp \
       goto_check.cpp \
       goto_rw.cpp \
+      guard_bdd.cpp \
+      guard_expr.cpp \
       interval_analysis.cpp \
       interval_domain.cpp \
       invariant_propagation.cpp \

src/analyses/goto_check.cpp

@@ -20,7 +20,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/cprover_prefix.h>
 #include <util/expr_util.h>
 #include <util/find_symbols.h>
-#include <util/guard.h>
 #include <util/ieee_float.h>
 #include <util/invariant.h>
 #include <util/make_unique.h>
@@ -36,6 +35,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <goto-programs/remove_skip.h>
 
+#include "guard.h"
 #include "local_bitvector_analysis.h"
 
 class goto_checkt
@@ -84,6 +84,7 @@ class goto_checkt
   const namespacet &ns;
   std::unique_ptr<local_bitvector_analysist> local_bitvector_analysis;
   goto_programt::const_targett current_target;
+  guard_managert guard_manager;
 
   void check_rec(
     const exprt &expr,
@@ -1650,7 +1651,7 @@ void goto_checkt::check_rec(const exprt &expr, guardt &guard, bool address)
 
 void goto_checkt::check(const exprt &expr)
 {
-  guardt guard{true_exprt{}};
+  guardt guard{true_exprt{}, guard_manager};
   check_rec(expr, guard, false);
 }
 
@@ -1782,7 +1783,7 @@ void goto_checkt::goto_check(
             "pointer dereference",
             i.source_location,
             pointer,
-            guardt(true_exprt()));
+            guardt(true_exprt(), guard_manager));
         }
       }
 
@@ -1820,7 +1821,7 @@ void goto_checkt::goto_check(
           "pointer dereference",
           i.source_location,
           pointer,
-          guardt(true_exprt()));
+          guardt(true_exprt(), guard_manager));
       }
 
       // this has no successor
@@ -1897,7 +1898,7 @@ void goto_checkt::goto_check(
           "memory-leak",
           source_location,
           eq,
-          guardt(true_exprt()));
+          guardt(true_exprt(), guard_manager));
       }
     }
 

src/analyses/goto_rw.h

@@ -17,7 +17,7 @@ Date: April 2010
 #include <map>
 #include <memory> // unique_ptr
 
-#include <util/guard.h>
+#include "guard.h"
 
 #include <goto-programs/goto_model.h>
 
@@ -352,8 +352,11 @@ class rw_guarded_range_set_value_sett:public rw_range_set_value_sett
 public:
   rw_guarded_range_set_value_sett(
     const namespacet &_ns,
-    value_setst &_value_sets):
-    rw_range_set_value_sett(_ns, _value_sets)
+    value_setst &_value_sets,
+    guard_managert &guard_manager)
+    : rw_range_set_value_sett(_ns, _value_sets),
+      guard_manager(guard_manager),
+      guard(true_exprt(), guard_manager)
   {
   }
 
@@ -370,7 +373,7 @@ class rw_guarded_range_set_value_sett:public rw_range_set_value_sett
     get_modet mode,
     const exprt &expr) override
   {
-    guard = guardt(true_exprt());
+    guard = guardt(true_exprt(), guard_manager);
 
     rw_range_set_value_sett::get_objects_rec(_function, _target, mode, expr);
   }
@@ -384,7 +387,8 @@ class rw_guarded_range_set_value_sett:public rw_range_set_value_sett
   }
 
 protected:
-  guardt guard = guardt(true_exprt());
+  guard_managert &guard_manager;
+  guardt guard;
 
   using rw_range_sett::get_objects_rec;
 

src/analyses/guard.h

@@ -0,0 +1,31 @@
+/*******************************************************************\
+
+Module: Guard Data Structure
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+/// \file
+/// Guard Data Structure
+
+#ifndef CPROVER_ANALYSES_GUARD_H
+#define CPROVER_ANALYSES_GUARD_H
+
+#ifdef BDD_GUARDS
+
+#include "guard_bdd.h"
+
+using guard_managert = bdd_exprt;
+using guardt = guard_bddt;
+
+#else
+
+#include "guard_expr.h"
+
+using guard_managert = guard_expr_managert;
+using guardt = guard_exprt;
+
+#endif // BDD_GUARDS
+
+#endif // CPROVER_ANALYSES_GUARD_H

src/analyses/guard_bdd.cpp

@@ -0,0 +1,94 @@
+/*******************************************************************\
+
+Module: Guard Data Structure
+
+Author: Romain Brenguier, [email protected]
+
+\*******************************************************************/
+
+/// \file
+/// Implementation of guards using BDDs
+
+#include "guard_bdd.h"
+
+#include <algorithm>
+#include <ostream>
+#include <set>
+
+#include <solvers/bdd/bdd.h>
+#include <solvers/prop/bdd_expr.h>
+#include <util/expr_util.h>
+#include <util/invariant.h>
+#include <util/make_unique.h>
+#include <util/namespace.h>
+#include <util/simplify_utils.h>
+#include <util/std_expr.h>
+#include <util/symbol_table.h>
+
+guard_bddt::guard_bddt(const exprt &e, bdd_exprt &manager)
+  : manager(manager), bdd(manager.from_expr(e))
+{
+}
+
+guard_bddt &guard_bddt::operator=(const guard_bddt &other)
+{
+  PRECONDITION(&manager == &other.manager);
+  bdd = other.bdd;
+  return *this;
+}
+
+guard_bddt &guard_bddt::operator=(guard_bddt &&other)
+{
+  PRECONDITION(&manager == &other.manager);
+  std::swap(bdd, other.bdd);
+  return *this;
+}
+
+exprt guard_bddt::guard_expr(exprt expr) const
+{
+  if(is_true())
+  {
+    // do nothing
+    return expr;
+  }
+  else
+  {
+    if(expr.is_false())
+    {
+      return boolean_negate(as_expr());
+    }
+    else
+    {
+      return implies_exprt{as_expr(), expr};
+    }
+  }
+}
+
+guard_bddt &guard_bddt::append(const guard_bddt &guard)
+{
+  bdd = bdd.bdd_and(guard.bdd);
+  return *this;
+}
+
+guard_bddt &guard_bddt::add(const exprt &expr)
+{
+  bdd = bdd.bdd_and(manager.from_expr(expr));
+  return *this;
+}
+
+guard_bddt &operator-=(guard_bddt &g1, const guard_bddt &g2)
+{
+  g1.bdd = g1.bdd.constrain(g2.bdd.bdd_or(g1.bdd));
+  return g1;
+}
+
+guard_bddt &operator|=(guard_bddt &g1, const guard_bddt &g2)
+{
+  g1.bdd = g1.bdd.bdd_or(g2.bdd);
+  return g1;
+}
+
+exprt guard_bddt::as_expr() const
+{
+  return manager.as_expr(bdd);
+}