diff --git a/src/util/expr.cpp b/src/util/expr.cpp index d252e6cbd91..ad4c0a4e856 100644 --- a/src/util/expr.cpp +++ b/src/util/expr.cpp @@ -526,6 +526,10 @@ const_depth_iteratort exprt::depth_cbegin() const { return const_depth_iteratort(*this); } const_depth_iteratort exprt::depth_cend() const { return const_depth_iteratort(); } +depth_iteratort exprt::depth_begin(std::function mutate_root) const +{ + return depth_iteratort(*this, std::move(mutate_root)); +} const_unique_depth_iteratort exprt::unique_depth_begin() const { return const_unique_depth_iteratort(*this); } diff --git a/src/util/expr.h b/src/util/expr.h index b58803f5689..2dddb4f0757 100644 --- a/src/util/expr.h +++ b/src/util/expr.h @@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com #define OPERANDS_IN_GETSUB +#include #include "type.h" #define forall_operands(it, expr) \ @@ -172,6 +173,7 @@ class exprt:public irept const_depth_iteratort depth_end() const; const_depth_iteratort depth_cbegin() const; const_depth_iteratort depth_cend() const; + depth_iteratort depth_begin(std::function mutate_root) const; const_unique_depth_iteratort unique_depth_begin() const; const_unique_depth_iteratort unique_depth_end() const; const_unique_depth_iteratort unique_depth_cbegin() const; diff --git a/src/util/expr_iterator.h b/src/util/expr_iterator.h index 1c43c953d69..c1ceb3fe07e 100644 --- a/src/util/expr_iterator.h +++ b/src/util/expr_iterator.h @@ -73,11 +73,24 @@ class depth_iterator_baset typedef const exprt *pointer; // NOLINT typedef const exprt &reference; // NOLINT typedef std::forward_iterator_tag iterator_category; // NOLINT - bool operator==(const depth_iterator_t &other) const + + template + friend class depth_iterator_baset; + + template + bool operator==( + const depth_iterator_baset &other) const { return m_stack==other.m_stack; } + template + bool operator!=( + const depth_iterator_baset &other) const + { + return !(*this == other); + } + /// Preincrement operator /// Do not call on the end() iterator depth_iterator_t &operator++() @@ -152,27 +165,39 @@ class depth_iterator_baset depth_iterator_baset &operator=(depth_iterator_baset &&other) { m_stack=std::move(other.m_stack); } - /// Obtain non-const exprt reference. Performs a copy-on-write on - /// the root node as a side effect. To be called only if a the root - /// is a non-const exprt. Do not call on the end() iterator + const exprt &get_root() + { + return m_stack.front().expr.get(); + } + + /// Obtain non-const exprt reference. Performs a copy-on-write on the root + /// node as a side effect. + /// \remarks + /// To be called only if a the root is a non-const exprt. + /// Do not call on the end() iterator exprt &mutate() { PRECONDITION(!m_stack.empty()); - auto expr=std::ref(const_cast(m_stack.front().expr.get())); + // Cast the root expr to non-const + exprt *expr = &const_cast(get_root()); for(auto &state : m_stack) { - auto &operands=expr.get().operands(); + // This deliberately breaks sharing as expr is now non-const + auto &operands = expr->operands(); + // Get iterators into the operands of the new expr corresponding to the + // ones into the operands of the old expr const auto i=operands.size()-(state.end-state.it); const auto it=operands.begin()+i; - state.expr=expr.get(); + state.expr = *expr; state.it=it; state.end=operands.end(); + // Get the expr for the next level down to use in the next iteration if(!(state==m_stack.back())) { - expr=std::ref(*it); + expr = &*it; } } - return expr.get(); + return *expr; } /// Pushes expression onto the stack @@ -194,13 +219,6 @@ class depth_iterator_baset { return static_cast(*this); } }; -template, T>::value, int>::type=0> -bool operator!=( - const T &left, - const T &right) -{ return !(left==right); } - class const_depth_iteratort final: public depth_iterator_baset { @@ -215,17 +233,58 @@ class const_depth_iteratort final: class depth_iteratort final: public depth_iterator_baset { +private: + /// If this is non-empty then the root is currently const and this function + /// must be called before any mutations occur + std::function mutate_root; + public: /// Create an end iterator depth_iteratort()=default; + /// Create iterator starting at the supplied node (root) /// All mutations of the child nodes will be reflected on this node - explicit depth_iteratort(exprt &expr): - depth_iterator_baset(expr) { } - /// Obtain non-const reference to the pointed exprt instance - /// Modifies root expression + /// \param expr: The root node to begin iteration at + explicit depth_iteratort(exprt &expr) : depth_iterator_baset(expr) + { + } + + /// Create iterator starting at the supplied node (root) + /// If mutations of the child nodes are required then the passed + /// mutate_root function will be called to get a non-const copy of the same + /// root on which the mutations will be done. + /// \param expr: The root node to begin iteration at + /// \param mutate_root: The function to call to get a non-const copy of the + /// same root expression passed in the expr parameter + explicit depth_iteratort( + const exprt &expr, + std::function mutate_root) + : depth_iterator_baset(expr), mutate_root(std::move(mutate_root)) + { + // If you don't provide a mutate_root function then you must pass a + // non-const exprt (use the other constructor). + PRECONDITION(this->mutate_root); + } + + /// Obtain non-const reference to the exprt instance currently pointed to + /// by the iterator. + /// If the iterator is currently using a const root exprt then calls + /// mutate_root to get a non-const root and copies it if it is shared + /// \returns A non-const reference to the element this iterator is + /// currently pointing to exprt &mutate() - { return depth_iterator_baset::mutate(); } + { + if(mutate_root) + { + exprt &new_root = mutate_root(); + INVARIANT( + &new_root.read() == &get_root().read(), + "mutate_root must return the same root node that depth_iteratort was " + "constructed with"); + mutate_root = nullptr; + } + return depth_iterator_baset::mutate(); + } }; class const_unique_depth_iteratort final: diff --git a/unit/util/expr_iterator.cpp b/unit/util/expr_iterator.cpp index 0ec6807aef0..ab3af5f70b8 100644 --- a/unit/util/expr_iterator.cpp +++ b/unit/util/expr_iterator.cpp @@ -1,10 +1,6 @@ -/*******************************************************************\ +// Copyright 2018 DiffBlue Limited. All Rights Reserved. - Module: Example Catch Tests - - Author: DiffBlue Limited. All rights reserved. - -\*******************************************************************/ +/// \file Tests for depth_iteratort and friends #include #include @@ -156,3 +152,87 @@ TEST_CASE("next_sibling_or_parent, next parent ") it.next_sibling_or_parent(); REQUIRE(it==input[0].depth_end()); } + +/// The mutate_root feature of depth_iteratort can be useful when you have an +/// `exprt` and want to depth iterate its first operand. As part of that +/// iteration you may or may not decide to mutate one of the children, +/// depending on the state of those children. If you do not decide to mutate +/// a child then you probably don't want to call the non-const version of +/// `op0()` because that will break sharing, so you create the depth iterator +/// with the const `exprt` returned from the const invocation of `op0()`, but +/// if you decide during iteration that you do want to mutate a child then +/// you can call the non-const version of `op0()` on the original `exprt` in +/// order to get a non-const `exprt` that the iterator can copy-on-write +/// update to change the child. At this point the iterator needs to be +/// informed that it is now safe to write to the `exprt` it contains. This is +/// achieved by providing a call-back function to the iterator. +SCENARIO("depth_iterator_mutate_root", "[core][utils][depth_iterator]") +{ + GIVEN("A sample expression with a child with id() == ID_1") + { + // Set up test expression + exprt test_expr; + // This is the expression we will iterate over + exprt test_root; + // This is the expression we might mutate when we find it + exprt test_operand(ID_1); + test_root.move_to_operands(test_operand); + test_expr.move_to_operands(test_root); + WHEN("Iteration occurs without mutation") + { + // Create shared copies + exprt original_expr = test_expr; + exprt expr = original_expr; + THEN("Shared copy should return object with same address from read()") + { + REQUIRE(&expr.read() == &original_expr.read()); + } + // Create iterator on first operand of expr + // We don't want to copy-on-write expr, so we get its first operand + // using a const reference to it + const exprt &root = static_cast(expr).op0(); + // This function gets a mutable version of root but in so doing it + // copy-on-writes expr + auto get_non_const_root = [&expr]() -> exprt & { return expr.op0(); }; + // Create the iterator over root + depth_iteratort it = root.depth_begin(get_non_const_root); + for(; it != root.depth_cend(); ++it) + { + if(it->id() == ID_0) // This will never happen + it.mutate().id(ID_1); + } + THEN("No breaking of sharing should have occurred") + { + REQUIRE(&expr.read() == &original_expr.read()); + } + } + WHEN("Iteration occurs with mutation") + { + // Create shared copies + exprt original_expr = test_expr; + exprt expr = original_expr; + THEN("Shared copy should return object with same address from read()") + { + REQUIRE(&expr.read() == &original_expr.read()); + } + // Create iterator on first operand of expr + // We don't want to copy-on-write expr, so we get its first operand + // using a const reference to it + const exprt &root = static_cast(expr).op0(); + // This function gets a mutable version of root but in so doing it + // copy-on-writes expr + auto get_non_const_root = [&expr]() -> exprt & { return expr.op0(); }; + // Create the iterator over root + depth_iteratort it = root.depth_begin(get_non_const_root); + for(; it != root.depth_cend(); ++it) + { + if(it->id() == ID_1) + it.mutate().id(ID_0); + } + THEN("Breaking of sharing should have occurred") + { + REQUIRE(&expr.read() != &original_expr.read()); + } + } + } +}