Skip to content

Restore irept sharing #1855

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.

Sign up for GitHub

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

Closed
wants to merge 1 commit into from
Closed

Restore irept sharing #1855

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
60 changes: 18 additions & 42 deletions src/util/expr.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,64 +21,40 @@ Author: Daniel Kroening, [email protected]

void exprt::move_to_operands(exprt &expr)
{
operandst &op=operands();
op.push_back(static_cast<const exprt &>(get_nil_irep()));
op.back().swap(expr);
move_to_sub(expr);
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This looks nice in a "use the API, not the internals" kind of way.

}

void exprt::move_to_operands(exprt &e1, exprt &e2)
{
operandst &op=operands();
#ifndef USE_LIST
op.reserve(op.size()+2);
#endif
op.push_back(static_cast<const exprt &>(get_nil_irep()));
op.back().swap(e1);
op.push_back(static_cast<const exprt &>(get_nil_irep()));
op.back().swap(e2);
reserve_operands(get_operands_size() + 2);
move_to_sub(e1);
move_to_sub(e2);
}

void exprt::move_to_operands(exprt &e1, exprt &e2, exprt &e3)
{
operandst &op=operands();
#ifndef USE_LIST
op.reserve(op.size()+3);
#endif
op.push_back(static_cast<const exprt &>(get_nil_irep()));
op.back().swap(e1);
op.push_back(static_cast<const exprt &>(get_nil_irep()));
op.back().swap(e2);
op.push_back(static_cast<const exprt &>(get_nil_irep()));
op.back().swap(e3);
reserve_operands(get_operands_size() + 3);
move_to_sub(e1);
move_to_sub(e2);
move_to_sub(e3);
}

void exprt::copy_to_operands(const exprt &expr)
void exprt::copy_to_operands(exprt expr)
{
operands().push_back(expr);
// Move the copy created by passing the argument by value to the operands
move_to_operands(expr);
}

void exprt::copy_to_operands(const exprt &e1, const exprt &e2)
void exprt::copy_to_operands(exprt e1, exprt e2)
{
operandst &op=operands();
#ifndef USE_LIST
op.reserve(op.size()+2);
#endif
op.push_back(e1);
op.push_back(e2);
// Move the copies created by passing the arguments by value to the operands
move_to_operands(e1, e2);
}

void exprt::copy_to_operands(
const exprt &e1,
const exprt &e2,
const exprt &e3)
void exprt::copy_to_operands(exprt e1, exprt e2, exprt e3)
{
operandst &op=operands();
#ifndef USE_LIST
op.reserve(op.size()+3);
#endif
op.push_back(e1);
op.push_back(e2);
op.push_back(e3);
// Move the copies created by passing the arguments by value to the operands
move_to_operands(e1, e2, e3);
}

void exprt::make_typecast(const typet &_type)
Expand All @@ -105,7 +81,7 @@ void exprt::make_not()

if(id()==ID_not && operands().size()==1)
{
new_expr.swap(operands().front());
new_expr.swap(op0());
}
else
{
Expand Down
14 changes: 10 additions & 4 deletions src/util/expr.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -93,17 +93,23 @@ class exprt:public irept
const exprt &op3() const
{ return operands()[3]; }

operandst::size_type get_operands_size() const
{
return get_sub_size();
}
void reserve_operands(operandst::size_type n)
{ operands().reserve(n) ; }
{
reserve_sub(n);
}

// destroys expr, e1, e2, e3
void move_to_operands(exprt &expr);
void move_to_operands(exprt &e1, exprt &e2);
void move_to_operands(exprt &e1, exprt &e2, exprt &e3);
// does not destroy expr, e1, e2, e3
void copy_to_operands(const exprt &expr);
void copy_to_operands(const exprt &e1, const exprt &e2);
void copy_to_operands(const exprt &e1, const exprt &e2, const exprt &e3);
void copy_to_operands(exprt expr);
void copy_to_operands(exprt e1, exprt e2);
void copy_to_operands(exprt e1, exprt e2, exprt e3);

// the following are deprecated -- use constructors instead
void make_typecast(const typet &_type);
Expand Down
52 changes: 14 additions & 38 deletions src/util/irep.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -57,14 +57,14 @@ const irept &get_nil_irep()

void irept::move_to_named_sub(const irep_namet &name, irept &irep)
{
add(name).swap(irep);
add(name, std::move(irep));
irep.clear();
}

void irept::move_to_sub(irept &irep)
{
get_sub().push_back(get_nil_irep());
get_sub().back().swap(irep);
write(true).sub.push_back(std::move(irep));
irep.clear();
}

const irep_idt &irept::get(const irep_namet &name) const
Expand Down Expand Up @@ -121,13 +121,13 @@ long long irept::get_long_long(const irep_namet &name) const

void irept::set(const irep_namet &name, const long long value)
{
add(name).id(std::to_string(value));
set(name, std::to_string(value));
}

void irept::remove(const irep_namet &name)
{
named_subt &s=
is_comment(name)?get_comments():get_named_sub();
named_subt &s =
is_comment(name) ? write(true).comments : write(true).named_sub;

#ifdef SUB_IS_LIST
named_subt::iterator it=named_subt_lower_bound(s, name);
Expand Down Expand Up @@ -160,47 +160,23 @@ const irept &irept::find(const irep_namet &name) const
return it->second;
}

irept &irept::add(const irep_namet &name)
irept &irept::add(const irep_namet &name, bool mark_sharable)
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The flag is kinda critical; any chance of some documentation for it?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The documentation is now in the header file.

{
named_subt &s=
is_comment(name)?get_comments():get_named_sub();
named_subt &s =
is_comment(name)
? write(mark_sharable).comments : write(mark_sharable).named_sub;

#ifdef SUB_IS_LIST
named_subt::iterator it=named_subt_lower_bound(s, name);

if(it==s.end() ||
it->first!=name)
it=s.insert(it, std::make_pair(name, irept()));

return it->second;
#else
return s[name];
#endif
}

irept &irept::add(const irep_namet &name, const irept &irep)
{
named_subt &s=
is_comment(name)?get_comments():get_named_sub();

#ifdef SUB_IS_LIST
named_subt::iterator it=named_subt_lower_bound(s, name);

if(it==s.end() ||
it->first!=name)
it=s.insert(it, std::make_pair(name, irep));
else
it->second=irep;

if(it == s.end() || it->first != name)
it = s.emplace(it, name, irept());
return it->second;

#else
std::pair<named_subt::iterator, bool> entry=
s.insert(std::make_pair(name, irep));

if(!entry.second)
entry.first->second=irep;
return s[name];

return entry.first->second;
#endif
}

Expand Down
38 changes: 35 additions & 3 deletions src/util/irep.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -125,8 +125,14 @@ class irept
}

const irept &find(const irep_namet &name) const;
irept &add(const irep_namet &name);
irept &add(const irep_namet &name, const irept &irep);
irept &add(const irep_namet &name)
{
return add(name, false);
}
void add(const irep_namet &name, irept irep)
{
add(name, true) = std::move(irep);
}

const std::string &get_string(const irep_namet &name) const
{
Expand All @@ -141,7 +147,9 @@ class irept
long long get_long_long(const irep_namet &name) const;

void set(const irep_namet &name, const irep_idt &value)
{ add(name).id(value); }
{
add(name, true).id(value);
}
void set(const irep_namet &name, const irept &irep)
{ add(name, irep); }
void set(const irep_namet &name, const long long value);
Expand Down Expand Up @@ -176,6 +184,16 @@ class irept
return write(false).sub;
}
const subt &get_sub() const { return read().sub; }
subt::size_type get_sub_size() const
{
return read().sub.size();
}
void reserve_sub(subt::size_type n)
{
#ifndef USE_LIST
write(true).sub.reserve(n);
#endif
}
named_subt &get_named_sub()
{
return write(false).named_sub;
Expand All @@ -199,6 +217,20 @@ class irept
{ return !name.empty() && name[0]=='#'; }

private:
/// Adds a new irept to the comments or named_sub collection with the given
/// name or retrieves the existing irept with the matching name
/// \remarks
/// If name starts with a hash symbol ('#') then the comments collection is
/// used, otherwise the named_sub collection is used
/// If the reference returned by this call is potentially held long enough
/// that a copy of this irept could be made before it is disposed of then you
/// must pass false for mark_sharable to ensure safe behaviour.
/// \param name: The name of the irept to add/retrieve
/// \param mark_sharable: If false then future copies of this irept will
/// not use sharing
/// \returns The added or retrieved irept
irept &add(const irep_namet &name, bool mark_sharable);

class dt
#ifdef SHARING
: public copy_on_write_pointeet<unsigned>
Expand Down
80 changes: 20 additions & 60 deletions unit/util/irep_sharing.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@

#ifdef SHARING

SCENARIO("irept_sharing_trade_offs", "[!mayfail][core][utils][irept]")
SCENARIO("irept_sharing", "[core][utils][irept]")
{
GIVEN("An irept created with move_to_sub")
{
Expand All @@ -21,35 +21,6 @@ SCENARIO("irept_sharing_trade_offs", "[!mayfail][core][utils][irept]")
irept irep = test_irep;
REQUIRE(&irep.read() == &test_irep.read());
}
THEN("Changing subs in the original using a reference taken before "
"copying should not change them in the copy")
{
irept &sub = test_irep.get_sub()[0];
irept irep = test_irep;
sub.id(ID_0);
REQUIRE(test_irep.get_sub()[0].id() == ID_0);
REQUIRE(irep.get_sub()[0].id() == ID_1);
}
THEN("Holding a reference to a sub should not prevent sharing")
{
irept &sub = test_irep.get_sub()[0];
irept irep = test_irep;
REQUIRE(&irep.read() == &test_irep.read());
sub = irept(ID_0);
REQUIRE(irep.get_sub()[0].id() == test_irep.get_sub()[0].id());
}
}
}

SCENARIO("irept_sharing", "[core][utils][irept]")
{
GIVEN("An irept created with move_to_sub")
{
irept test_irep(ID_1);
irept test_subirep(ID_1);
irept test_subsubirep(ID_1);
test_subirep.move_to_sub(test_subsubirep);
test_irep.move_to_sub(test_subirep);
THEN("Copies of a copy should return object with the same address")
{
irept irep1 = test_irep;
Expand All @@ -69,6 +40,15 @@ SCENARIO("irept_sharing", "[core][utils][irept]")
REQUIRE(test_irep.get_sub()[0].id() == ID_1);
REQUIRE(irep.get_sub()[0].id() == ID_0);
}
THEN("Changing subs in the original using a reference taken before "
"copying should not change them in the copy")
{
irept &sub = test_irep.get_sub()[0];
irept irep = test_irep;
sub.id(ID_0);
REQUIRE(test_irep.get_sub()[0].id() == ID_0);
REQUIRE(irep.get_sub()[0].id() == ID_1);
}
THEN("Getting a reference to a sub in a copy should break sharing")
{
irept irep = test_irep;
Expand Down Expand Up @@ -104,7 +84,7 @@ SCENARIO("irept_sharing", "[core][utils][irept]")

#include <util/expr.h>

SCENARIO("exprt_sharing_trade_offs", "[!mayfail][core][utils][exprt]")
SCENARIO("exprt_sharing", "[core][utils][exprt]")
{
GIVEN("An expression created with move_to_operands")
{
Expand All @@ -118,35 +98,6 @@ SCENARIO("exprt_sharing_trade_offs", "[!mayfail][core][utils][exprt]")
exprt expr = test_expr;
REQUIRE(&expr.read() == &test_expr.read());
}
THEN("Changing operands in the original using a reference taken before "
"copying should not change them in the copy")
{
exprt &operand = test_expr.op0();
exprt expr = test_expr;
operand.id(ID_0);
REQUIRE(test_expr.op0().id() == ID_0);
REQUIRE(expr.op0().id() == ID_1);
}
THEN("Holding a reference to an operand should not prevent sharing")
{
exprt &operand = test_expr.op0();
exprt expr = test_expr;
REQUIRE(&expr.read() == &test_expr.read());
operand = exprt(ID_0);
REQUIRE(expr.op0().id() == test_expr.op0().id());
}
}
}

SCENARIO("exprt_sharing", "[core][utils][exprt]")
{
GIVEN("An expression created with move_to_operands")
{
exprt test_expr(ID_1);
exprt test_subexpr(ID_1);
exprt test_subsubexpr(ID_1);
test_subexpr.move_to_operands(test_subsubexpr);
test_expr.move_to_operands(test_subexpr);
THEN("Copies of a copy should return object with the same address")
{
exprt expr1 = test_expr;
Expand All @@ -166,6 +117,15 @@ SCENARIO("exprt_sharing", "[core][utils][exprt]")
REQUIRE(test_expr.op0().id() == ID_1);
REQUIRE(expr.op0().id() == ID_0);
}
THEN("Changing operands in the original using a reference taken before "
"copying should not change them in the copy")
{
exprt &operand = test_expr.op0();
exprt expr = test_expr;
operand.id(ID_0);
REQUIRE(test_expr.op0().id() == ID_0);
REQUIRE(expr.op0().id() == ID_1);
}
THEN("Getting a reference to an operand in a copy should break sharing")
{
exprt expr = test_expr;
Expand Down