Merge pull request #1062 from diffblue/fix_for_miniBDD

fix for operator< on reverse_keyt in miniBDD, fixing segfault in ebmc

Author: Daniel Kroening

src/solvers/miniBDD/miniBDD.cpp

@@ -463,14 +463,20 @@ mini_bddt mini_bdd_mgrt::mk(
 }
 
 bool mini_bdd_mgrt::reverse_keyt::operator<(
-  const mini_bdd_mgrt::reverse_keyt &other) const
+  const mini_bdd_mgrt::reverse_keyt &y) const
 {
-  if(var<other.var || low<other.low)
+  const reverse_keyt &x=*this;
+
+  if(x.var<y.var)
     return true;
-  if(var>other.var || low>other.low)
+  else if(x.var>y.var)
     return false;
-
-  return high<other.high;
+  else if(x.low<y.low)
+    return true;
+  else if(x.low>y.low)
+    return false;
+  else
+    return x.high<y.high;
 }
 
 void mini_bdd_mgrt::DumpTable(std::ostream &out) const

src/solvers/miniBDD/miniBDD.h

@@ -124,7 +124,7 @@ class mini_bdd_mgrt
     reverse_keyt(
       unsigned _var, const mini_bddt &_low, const mini_bddt &_high);
 
-    bool operator<(const reverse_keyt &other) const;
+    bool operator<(const reverse_keyt &) const;
   };
 
   typedef std::map<reverse_keyt, mini_bdd_nodet *> reverse_mapt;

src/util/invariant.h

@@ -149,6 +149,9 @@ void report_exception_to_stderr(const invariant_failedt &);
 /// \param params : (variadic) parameters to forward to ET's constructor
 ///  its backtrace member will be set before it is used.
 template<class ET, typename ...Params>
+#ifdef __GNUC__
+__attribute__((noreturn))
+#endif
 typename std::enable_if<std::is_base_of<invariant_failedt, ET>::value>::type
 invariant_violated_structured(
   const std::string &file,
@@ -171,6 +174,9 @@ invariant_violated_structured(
 /// \param function : C string giving the name of the function.
 /// \param line : The line number of the invariant
 /// \param reason : brief description of the invariant violation.
+#ifdef __GNUC__
+__attribute__((noreturn))
+#endif
 inline void invariant_violated_string(
   const std::string &file,
   const std::string &function,

unit/Makefile

@@ -11,6 +11,7 @@ SRC += unit_tests.cpp \
        analyses/does_remove_const/does_expr_lose_const.cpp \
        analyses/does_remove_const/does_type_preserve_const_correctness.cpp \
        analyses/does_remove_const/is_type_at_least_as_const_as.cpp \
+       miniBDD_new.cpp \
        catch_example.cpp \
        # Empty last line
 

unit/miniBDD_new.cpp

@@ -0,0 +1,277 @@
+/*******************************************************************\
+
+ Module: Unit tests for miniBDD
+
+ Author: DiffBlue Limited. All rights reserved.
+
+\*******************************************************************/
+
+/// \file
+/// Unit tests for miniBDD
+
+#include <catch.hpp>
+
+#include <solvers/miniBDD/miniBDD.h>
+#include <solvers/flattening/boolbv.h>
+
+#include <util/symbol_table.h>
+#include <util/arith_tools.h>
+#include <util/expanding_vector.h>
+
+#include <iostream>
+
+class bdd_propt:public propt
+{
+public:
+  mini_bdd_mgrt &mgr;
+
+  explicit bdd_propt(mini_bdd_mgrt &_mgr):mgr(_mgr)
+  {
+    // True and False
+    bdd_map.push_back(mgr.False());
+    bdd_map.push_back(mgr.True());
+  }
+
+  mini_bddt to_bdd(literalt a)
+  {
+    if(a.is_true())
+      return mgr.True();
+    if(a.is_false())
+      return mgr.False();
+    INVARIANT(a.var_no()<bdd_map.size(), "literal in map");
+    mini_bddt bdd=bdd_map[a.var_no()];
+    INVARIANT(bdd.is_initialized(), "initialized");
+    if(a.sign())
+      return !bdd;
+    else
+      return bdd;
+  }
+
+  literalt to_literal(const mini_bddt &bdd)
+  {
+    if(bdd.is_constant())
+      return const_literal(bdd.is_true());
+    std::size_t index=bdd.node_number();
+    bdd_map[index]=bdd;
+    return literalt(index, false);
+  }
+
+  literalt land(literalt a, literalt b) override
+  {
+    return to_literal(to_bdd(a) & to_bdd(b));
+  }
+
+  literalt lor(literalt a, literalt b) override
+  {
+    UNREACHABLE;
+  }
+
+  literalt land(const bvt &bv) override
+  {
+    mini_bddt result=mgr.True();
+
+    for(const auto &l : bv)
+      result=result&to_bdd(l);
+
+    return to_literal(result);
+  }
+
+  literalt lor(const bvt &bv) override
+  {
+    mini_bddt result=mgr.False();
+
+    for(const auto &l : bv)
+      result=result|to_bdd(l);
+
+    return to_literal(result);
+  }
+
+  literalt lxor(literalt a, literalt b) override
+  {
+    return to_literal(to_bdd(a) ^ to_bdd(b));
+  }
+
+  literalt lxor(const bvt &bv) override
+  {
+    UNREACHABLE;
+  }
+
+  literalt lnand(literalt a, literalt b) override
+  {
+    UNREACHABLE;
+  }
+
+  literalt lnor(literalt a, literalt b) override
+  {
+    UNREACHABLE;
+  }
+
+  literalt lequal(literalt a, literalt b) override
+  {
+    return to_literal(to_bdd(a)==to_bdd(b));
+  }
+
+  literalt limplies(literalt a, literalt b) override
+  {
+    UNREACHABLE;
+  }
+
+  literalt lselect(literalt a, literalt b, literalt c) override
+  {
+    UNREACHABLE;
+  }
+
+  void lcnf(const bvt &bv) override
+  {
+    UNREACHABLE;
+  }
+
+  literalt new_variable() override
+  {
+    return to_literal(mgr.Var(""));
+  }
+
+  size_t no_variables() const override
+  {
+    return bdd_map.size();
+  }
+
+  const std::string solver_text() override
+  {
+    return "BDDs";
+  }
+
+  resultt prop_solve() override
+  {
+    UNREACHABLE;
+  }
+
+  tvt l_get(literalt a) const override
+  {
+    UNREACHABLE;
+  }
+
+  expanding_vectort<mini_bddt> bdd_map;
+
+  bool has_set_to() const override { return false; }
+  bool cnf_handled_well() const override { return false; }
+};
+
+SCENARIO("miniBDD", "[core][solver][miniBDD]")
+{
+  GIVEN("A bdd for x&!x")
+  {
+    symbol_tablet symbol_table;
+    namespacet ns(symbol_table);
+    mini_bdd_mgrt bdd_mgr;
+    bdd_propt bdd_prop(bdd_mgr);
+    prop_conv_solvert solver(ns, bdd_prop);
+
+    symbol_exprt var("x", bool_typet());
+    literalt result=
+      solver.convert(and_exprt(var, not_exprt(var)));
+
+    REQUIRE(result.is_false());
+  }
+
+  GIVEN("A bdd for x&!x==0")
+  {
+    symbol_tablet symbol_table;
+    namespacet ns(symbol_table);
+    mini_bdd_mgrt bdd_mgr;
+    bdd_propt bdd_prop(bdd_mgr);
+    boolbvt boolbv(ns, bdd_prop);
+
+    unsignedbv_typet type(2);
+    symbol_exprt var("x", type);
+    equal_exprt equality(
+      bitand_exprt(var, bitnot_exprt(var)),
+      from_integer(0, type));
+
+    literalt result=
+      boolbv.convert(equality);
+
+    REQUIRE(result.is_true());
+  }
+
+  GIVEN("A bdd for x+x==1")
+  {
+    symbol_tablet symbol_table;
+    namespacet ns(symbol_table);
+    mini_bdd_mgrt bdd_mgr;
+    bdd_propt bdd_prop(bdd_mgr);
+    boolbvt boolbv(ns, bdd_prop);
+
+    unsignedbv_typet type(32);
+    symbol_exprt var("x", type);
+    equal_exprt equality(
+      plus_exprt(var, var),
+      from_integer(1, type));
+
+    literalt result=
+      boolbv.convert(equality);
+
+    REQUIRE(result.is_false());
+  }
+
+  GIVEN("A bdd for x*y==y*x")
+  {
+    symbol_tablet symbol_table;
+    namespacet ns(symbol_table);
+    mini_bdd_mgrt bdd_mgr;
+    bdd_propt bdd_prop(bdd_mgr);
+    boolbvt boolbv(ns, bdd_prop);
+
+    unsignedbv_typet type(4);
+    symbol_exprt var_x("x", type);
+    symbol_exprt var_y("y", type);
+    equal_exprt equality(
+      mult_exprt(var_x, var_y),
+      mult_exprt(var_y, var_x));
+
+    literalt result=
+      boolbv.convert(equality);
+
+    REQUIRE(result.is_true());
+  }
+
+  GIVEN("A bdd for x*x==2")
+  {
+    symbol_tablet symbol_table;
+    namespacet ns(symbol_table);
+    mini_bdd_mgrt bdd_mgr;
+    bdd_propt bdd_prop(bdd_mgr);
+    boolbvt boolbv(ns, bdd_prop);
+
+    unsignedbv_typet type(8);
+    symbol_exprt var_x("x", type);
+    equal_exprt equality(
+      mult_exprt(var_x, var_x),
+      from_integer(2, type));
+
+    literalt result=
+      boolbv.convert(equality);
+
+    REQUIRE(result.is_false());
+  }
+
+  GIVEN("A bdd for x*x==4")
+  {
+    symbol_tablet symbol_table;
+    namespacet ns(symbol_table);
+    mini_bdd_mgrt bdd_mgr;
+    bdd_propt bdd_prop(bdd_mgr);
+    boolbvt boolbv(ns, bdd_prop);
+
+    unsignedbv_typet type(8);
+    symbol_exprt var_x("x", type);
+    equal_exprt equality(
+      mult_exprt(var_x, var_x),
+      from_integer(4, type));
+
+    literalt result=
+      boolbv.convert(equality);
+
+    REQUIRE(!result.is_constant());
+  }
+}