From bc006295799bf153942e59def9dcd0bf95484778 Mon Sep 17 00:00:00 2001 From: Thomas Given-Wilson Date: Thu, 11 Mar 2021 09:54:22 +0000 Subject: [PATCH 1/3] Optimise size to have approximate bound This optimises the size function that was only used when checking for a bound. The new bounded_size takes an explicit bound argument and reduces the search when this bound is (approximately) reached. --- src/goto-symex/complexity_limiter.cpp | 2 +- src/goto-symex/goto_state.h | 9 --------- src/util/expr.cpp | 24 ++++++++++++++++++------ src/util/expr.h | 10 +++++++--- 4 files changed, 26 insertions(+), 19 deletions(-) diff --git a/src/goto-symex/complexity_limiter.cpp b/src/goto-symex/complexity_limiter.cpp index 311c4846814..3aefbdccdec 100644 --- a/src/goto-symex/complexity_limiter.cpp +++ b/src/goto-symex/complexity_limiter.cpp @@ -136,7 +136,7 @@ complexity_limitert::check_complexity(goto_symex_statet &state) if(!complexity_limits_active() || !state.reachable) return complexity_violationt::NONE; - std::size_t complexity = state.complexity(); + std::size_t complexity = state.guard.as_expr().bounded_size(max_complexity); if(complexity == 0) return complexity_violationt::NONE; diff --git a/src/goto-symex/goto_state.h b/src/goto-symex/goto_state.h index 85cbdf3d51f..f2ce7660229 100644 --- a/src/goto-symex/goto_state.h +++ b/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; diff --git a/src/util/expr.cpp b/src/util/expr.cpp index 509edbf0804..95c43f96435 100644 --- a/src/util/expr.cpp +++ b/src/util/expr.cpp @@ -24,16 +24,28 @@ Author: Daniel Kroening, kroening@kroening.com #include -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. diff --git a/src/util/expr.h b/src/util/expr.h index 32f0e89489a..01512baab01 100644 --- a/src/util/expr.h +++ b/src/util/expr.h @@ -85,9 +85,9 @@ class exprt:public irept return static_cast(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) ; } From b3c4aeb1193dc00130085a44db34edea06996081 Mon Sep 17 00:00:00 2001 From: Thomas Given-Wilson Date: Wed, 24 Mar 2021 11:15:13 +0000 Subject: [PATCH 2/3] Fix bug in complexity calculation By definition exprts have at least size (complexity) 1, so check for complexity == 1 not complexity == 0. --- src/goto-symex/complexity_limiter.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/goto-symex/complexity_limiter.cpp b/src/goto-symex/complexity_limiter.cpp index 3aefbdccdec..5833f4d5404 100644 --- a/src/goto-symex/complexity_limiter.cpp +++ b/src/goto-symex/complexity_limiter.cpp @@ -137,7 +137,7 @@ complexity_limitert::check_complexity(goto_symex_statet &state) return complexity_violationt::NONE; std::size_t complexity = state.guard.as_expr().bounded_size(max_complexity); - if(complexity == 0) + if(complexity == 1) return complexity_violationt::NONE; auto ¤t_call_stack = state.call_stack(); From ef2f3e16b90bc7042871972f2e228dd2cf3ea504 Mon Sep 17 00:00:00 2001 From: Thomas Given-Wilson Date: Mon, 22 Mar 2021 15:04:15 +0000 Subject: [PATCH 3/3] Add unit tests for bounded_size This adds unit tests for the bounded_size function for exprs. Note that the pathological case is designed to break incorrect implementations of bounded size and is intentionally a malformed exprt. --- unit/util/expr.cpp | 33 +++++++++++++++++++++++++++++++++ 1 file changed, 33 insertions(+) diff --git a/unit/util/expr.cpp b/unit/util/expr.cpp index 61f089ecb93..248976a038a 100644 --- a/unit/util/expr.cpp +++ b/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 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); +}