From 8f61a227a4a7c198a099bd7a3f306fb3e19e611e Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 31 Mar 2021 15:34:22 +0000 Subject: [PATCH] Move exprt::bounded_size to complexity_limitert complexity_limitert is really the only user of this method, and may be fine with its implementation details (cf. discussion in #5914). For other potential users such assumptions might not be safe. --- src/goto-symex/complexity_limiter.cpp | 29 +++++++++++++- src/goto-symex/complexity_limiter.h | 6 +++ src/util/expr.cpp | 24 ------------ src/util/expr.h | 8 ---- unit/Makefile | 1 + unit/goto-symex/complexity_limiter.cpp | 52 ++++++++++++++++++++++++++ unit/util/expr.cpp | 33 ---------------- 7 files changed, 87 insertions(+), 66 deletions(-) create mode 100644 unit/goto-symex/complexity_limiter.cpp diff --git a/src/goto-symex/complexity_limiter.cpp b/src/goto-symex/complexity_limiter.cpp index 5833f4d5404..594bd3dde0c 100644 --- a/src/goto-symex/complexity_limiter.cpp +++ b/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); +} diff --git a/src/goto-symex/complexity_limiter.h b/src/goto-symex/complexity_limiter.h index 478e7c104b3..ad996b6292e 100644 --- a/src/goto-symex/complexity_limiter.h +++ b/src/goto-symex/complexity_limiter.h @@ -69,6 +69,12 @@ class complexity_limitert complexity_violationt complexity_violation, goto_symex_statet ¤t_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; diff --git a/src/util/expr.cpp b/src/util/expr.cpp index 95c43f96435..d5169f943f4 100644 --- a/src/util/expr.cpp +++ b/src/util/expr.cpp @@ -24,30 +24,6 @@ Author: Daniel Kroening, kroening@kroening.com #include -/// 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 diff --git a/src/util/expr.h b/src/util/expr.h index 01512baab01..61b7a1caedb 100644 --- a/src/util/expr.h +++ b/src/util/expr.h @@ -85,10 +85,6 @@ class exprt:public irept return static_cast(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) ; } diff --git a/unit/Makefile b/unit/Makefile index 43b4ec56ea8..c49e7bcb18d 100644 --- a/unit/Makefile +++ b/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 \ diff --git a/unit/goto-symex/complexity_limiter.cpp b/unit/goto-symex/complexity_limiter.cpp new file mode 100644 index 00000000000..e60e30e8ff3 --- /dev/null +++ b/unit/goto-symex/complexity_limiter.cpp @@ -0,0 +1,52 @@ +/*******************************************************************\ + +Module: Unit test for goto-symex/complexity_limiter + +Author: Diffblue Ltd + +\*******************************************************************/ + +#include + +#include + +#include + +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 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); +} diff --git a/unit/util/expr.cpp b/unit/util/expr.cpp index 248976a038a..61f089ecb93 100644 --- a/unit/util/expr.cpp +++ b/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 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); -}