Merge pull request #5914 from TGWDB/optimize-expr-size

Refactor and optimise size to have approximate bound

Author: TGWDB

src/goto-symex/complexity_limiter.cpp

@@ -136,8 +136,8 @@ complexity_limitert::check_complexity(goto_symex_statet &state)
   if(!complexity_limits_active() || !state.reachable)
     return complexity_violationt::NONE;
 
-  std::size_t complexity = state.complexity();
-  if(complexity == 0)
+  std::size_t complexity = state.guard.as_expr().bounded_size(max_complexity);
+  if(complexity == 1)
     return complexity_violationt::NONE;
 
   auto &current_call_stack = state.call_stack();

src/goto-symex/goto_state.h

@@ -71,15 +71,6 @@ class goto_statet
   /// Threads
   unsigned atomic_section_id = 0;
 
-  /// Get the complexity for this state. Used to short-circuit states if they
-  /// have become too computationally complex.
-  inline std::size_t complexity()
-  {
-    // TODO: This isn't too efficent for BDDs, try using a different size
-    // like DAG size.
-    return guard.as_expr().size();
-  }
-
   /// Constructors
   goto_statet() = delete;
   goto_statet &operator=(const goto_statet &other) = delete;

src/util/expr.cpp

@@ -24,16 +24,28 @@ Author: Daniel Kroening, [email protected]
 
 #include <stack>
 
-std::size_t exprt::size() const
+/// Returns the size of the exprt added to count without searching significantly
+/// beyond the supplied limit.
+std::size_t exprt::bounded_size(std::size_t count, std::size_t limit) const
 {
-  // Initial size of 1 to count self.
-  std::size_t size = 1;
-  for(const auto &op : operands())
+  const auto &ops = operands();
+  count += ops.size();
+  for(const auto &op : ops)
   {
-    size += op.size();
+    if(count >= limit)
+    {
+      return count;
+    }
+    count = op.bounded_size(count, limit);
   }
+  return count;
+}
 
-  return size;
+/// Returns the size of the exprt without significantly searching beyond the
+/// supplied limit.
+std::size_t exprt::bounded_size(std::size_t limit) const
+{
+  return bounded_size(1, limit);
 }
 
 /// Return whether the expression is a constant.

src/util/expr.h

@@ -85,9 +85,9 @@ class exprt:public irept
     return static_cast<const typet &>(find(ID_type));
   }
 
-  /// Amount of nodes this expression tree contains. This is the size of the
-  /// actual tree, ignoring memory/sub-tree sharing.
-  std::size_t size() const;
+  /// Amount of nodes in this expression tree approximately bounded by limit.
+  /// This is the size of the actual tree, ignoring memory/sub-tree sharing.
+  std::size_t bounded_size(std::size_t limit) const;
 
   /// Return true if there is at least one operand.
   bool has_operands() const
@@ -124,6 +124,10 @@ class exprt:public irept
   const exprt &op3() const
   { return operands()[3]; }
 
+  /// Amount of nodes this expression tree contains, with a bound on how far
+  /// to search. Starts with an existing count.
+  std::size_t bounded_size(std::size_t count, std::size_t limit) const;
+
 public:
   void reserve_operands(operandst::size_type n)
   { operands().reserve(n) ; }

unit/util/expr.cpp

@@ -36,3 +36,36 @@ SCENARIO("bitfield-expr-is-zero", "[core][util][expr]")
     }
   }
 }
+
+TEST_CASE("Bounded size is computer correctly", "[core][util][expr]")
+{
+  // Helper types and functions for constructing test expressions.
+  const typet type = signedbv_typet(32);
+  std::function<exprt(size_t)> make_expression;
+  make_expression = [&](size_t size) -> exprt {
+    PRECONDITION(size != 0);
+    if(size <= 1)
+      return from_integer(1, type);
+    if(size == 2)
+      return unary_minus_exprt(from_integer(1, type));
+    return plus_exprt(from_integer(1, type), make_expression(size - 2));
+  };
+  // Actual test cases.
+  REQUIRE(make_expression(1).bounded_size(10) == 1);
+  REQUIRE(make_expression(2).bounded_size(10) == 2);
+  REQUIRE(make_expression(3).bounded_size(10) == 3);
+
+  REQUIRE(make_expression(30).bounded_size(10) < 13);
+  REQUIRE(make_expression(30).bounded_size(10) >= 10);
+}
+
+TEST_CASE("Bounded size versus pathological example", "[core][util][expr]")
+{
+  const typet type = signedbv_typet(32);
+  exprt pathology = plus_exprt(from_integer(1, type), from_integer(1, type));
+  // Create an infinite exprt by self reference!
+  pathology.add_to_operands(pathology);
+  // If bounded size is not checking the bound this will never terminate.
+  REQUIRE(pathology.bounded_size(10) < 13);
+  REQUIRE(pathology.bounded_size(10) >= 10);
+}