Skip to content

Allow non-const depth_iteratort to be created from a const root #1842

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 4 additions & 0 deletions src/util/expr.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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<exprt &()> 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); }
Expand Down
2 changes: 2 additions & 0 deletions src/util/expr.h
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]

#define OPERANDS_IN_GETSUB

#include <functional>
#include "type.h"

#define forall_operands(it, expr) \
Expand Down Expand Up @@ -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<exprt &()> 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;
Expand Down
101 changes: 80 additions & 21 deletions src/util/expr_iterator.h
Original file line number Diff line number Diff line change
Expand Up @@ -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 <typename other_depth_iterator_t>
friend class depth_iterator_baset;

template <typename other_depth_iterator_t>
bool operator==(
const depth_iterator_baset<other_depth_iterator_t> &other) const
{
return m_stack==other.m_stack;
}

template <typename other_depth_iterator_t>
bool operator!=(
const depth_iterator_baset<other_depth_iterator_t> &other) const
{
return !(*this == other);
}

/// Preincrement operator
/// Do not call on the end() iterator
depth_iterator_t &operator++()
Expand Down Expand Up @@ -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<exprt &>(m_stack.front().expr.get()));
// Cast the root expr to non-const
exprt *expr = &const_cast<exprt &>(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
Expand All @@ -194,13 +219,6 @@ class depth_iterator_baset
{ return static_cast<depth_iterator_t &>(*this); }
};

template<typename T, typename std::enable_if<
std::is_base_of<depth_iterator_baset<T>, 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<const_depth_iteratort>
{
Expand All @@ -215,17 +233,58 @@ class const_depth_iteratort final:
class depth_iteratort final:
public depth_iterator_baset<depth_iteratort>
{
private:
/// If this is non-empty then the root is currently const and this function
/// must be called before any mutations occur
std::function<exprt &()> 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<exprt &()> 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:
Expand Down
92 changes: 86 additions & 6 deletions unit/util/expr_iterator.cpp
Original file line number Diff line number Diff line change
@@ -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 <testing-utils/catch.hpp>
#include <util/expr.h>
Expand Down Expand Up @@ -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<const exprt &>(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<const exprt &>(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());
}
}
}
}