Move exprt::bounded_size to complexity_limitert

src/goto-symex/complexity_limiter.cpp

@@ -136,7 +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.guard.as_expr().bounded_size(max_complexity);
+  std::size_t complexity =
+    bounded_expr_size(state.guard.as_expr(), max_complexity);
   if(complexity == 1)
     return complexity_violationt::NONE;
 
@@ -211,3 +212,29 @@ void complexity_limitert::run_transformations(
     for(auto transform_lambda : violation_transformations)
       transform_lambda.transform(complexity_violation, current_state);
 }
+
+/// Amount of nodes \p expr contains, with a bound on how far to search.
+/// Starts with an existing count.
+/// \return Size of \p expr added to count without searching significantly
+/// beyond the supplied limit.
+static std::size_t
+bounded_expr_size(const exprt &expr, std::size_t count, std::size_t limit)
+{
+  const auto &ops = expr.operands();
+  count += ops.size();
+  for(const auto &op : ops)
+  {
+    if(count >= limit)
+    {
+      return count;
+    }
+    count = bounded_expr_size(op, count, limit);
+  }
+  return count;
+}
+
+std::size_t
+complexity_limitert::bounded_expr_size(const exprt &expr, std::size_t limit)
+{
+  return ::bounded_expr_size(expr, 1, limit);
+}

src/goto-symex/complexity_limiter.h

@@ -69,6 +69,12 @@ class complexity_limitert
     complexity_violationt complexity_violation,
     goto_symex_statet &current_state);
 
+  /// Amount of nodes in \p expr approximately bounded by limit.
+  /// This is the size of the actual tree, ignoring memory/sub-tree sharing.
+  /// Expressions that make substantial use of sharing may result in excessive
+  /// run time.
+  static std::size_t bounded_expr_size(const exprt &expr, std::size_t limit);
+
 protected:
   mutable messaget log;
 

src/util/expr.cpp

@@ -24,30 +24,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <stack>
 
-/// 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
-{
-  const auto &ops = operands();
-  count += ops.size();
-  for(const auto &op : ops)
-  {
-    if(count >= limit)
-    {
-      return count;
-    }
-    count = op.bounded_size(count, limit);
-  }
-  return count;
-}
-
-/// 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.
 /// \return True if is a constant, false otherwise
 bool exprt::is_constant() const

src/util/expr.h

@@ -85,10 +85,6 @@ class exprt:public irept
     return static_cast<const typet &>(find(ID_type));
   }
 
-  /// 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
   { return !operands().empty(); }
@@ -124,10 +120,6 @@ 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/Makefile

@@ -54,6 +54,7 @@ SRC += analyses/ai/ai.cpp \
        goto-programs/remove_returns.cpp \
        goto-programs/xml_expr.cpp \
        goto-symex/apply_condition.cpp \
+       goto-symex/complexity_limiter.cpp \
        goto-symex/expr_skeleton.cpp \
        goto-symex/goto_symex_state.cpp \
        goto-symex/ssa_equation.cpp \

unit/goto-symex/complexity_limiter.cpp

@@ -0,0 +1,52 @@
+/*******************************************************************\
+
+Module: Unit test for goto-symex/complexity_limiter
+
+Author: Diffblue Ltd
+
+\*******************************************************************/
+
+#include <testing-utils/use_catch.h>
+
+#include <util/arith_tools.h>
+
+#include <goto-symex/complexity_limiter.h>
+
+TEST_CASE(
+  "Bounded expression size is computed correctly",
+  "[core][goto-symex][complexity_limiter]")
+{
+  // 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(complexity_limitert::bounded_expr_size(make_expression(1), 10) == 1);
+  REQUIRE(complexity_limitert::bounded_expr_size(make_expression(2), 10) == 2);
+  REQUIRE(complexity_limitert::bounded_expr_size(make_expression(3), 10) == 3);
+
+  REQUIRE(complexity_limitert::bounded_expr_size(make_expression(30), 10) < 13);
+  REQUIRE(
+    complexity_limitert::bounded_expr_size(make_expression(30), 10) >= 10);
+}
+
+TEST_CASE(
+  "Bounded expression size versus pathological example",
+  "[core][goto-symex][complexity_limiter]")
+{
+  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 expression size is not checking the bound this will never
+  // terminate.
+  REQUIRE(complexity_limitert::bounded_expr_size(pathology, 10) < 13);
+  REQUIRE(complexity_limitert::bounded_expr_size(pathology, 10) >= 10);
+}

unit/util/expr.cpp

@@ -36,36 +36,3 @@ 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);
-}