replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

Merge pull request #4413 from danpoe/refactor/sharing-map 

Sharing map refactorings
This commit is contained in:
Daniel Poetzl 2019-03-21 12:20:27 +00:00 committed by GitHub
parent d61900d41c 468717f39e
commit 039ac77841
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
6 changed files with 163 additions and 122 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

20
src/util/sharing_map.h
View File

@ -350,7 +350,7 @@ protected:
std::size_t count_unmarked_nodes(
bool leafs_only,
std::set<void *> &marked,
std::set<const void *> &marked,
bool mark = true) const;
// dummy element returned when no element was found
@ -423,8 +423,10 @@ SHARING_MAPT(void)
}
SHARING_MAPT(std::size_t)
::count_unmarked_nodes(bool leafs_only, std::set<void *> &marked, bool mark)
const
::count_unmarked_nodes(
bool leafs_only,
std::set<const void *> &marked,
bool mark) const
{
if(empty())
return 0;
@ -447,8 +449,10 @@ SHARING_MAPT(std::size_t)
// internal node or container node
const innert *ip = static_cast<const innert *>(bp);
const unsigned use_count = ip->data.use_count();
void *raw_ptr = ip->data.get();
const unsigned use_count = ip->use_count();
const void *raw_ptr = ip->is_internal()
? (const void *)&ip->read_internal()
: (const void *)&ip->read_container();
if(use_count >= 2)
{
@ -488,8 +492,8 @@ SHARING_MAPT(std::size_t)
for(const auto &l : ll)
{
const unsigned leaf_use_count = l.data.use_count();
void *leaf_raw_ptr = l.data.get();
const unsigned leaf_use_count = l.use_count();
const void *leaf_raw_ptr = &l.read();
if(leaf_use_count >= 2)
{
@ -528,7 +532,7 @@ SHARING_MAPT3(Iterator, , sharing_map_statst)
Iterator end,
std::function<sharing_mapt &(const Iterator)> f)
{
std::set<void *> marked;
std::set<const void *> marked;
sharing_map_statst sms;
// We do a separate pass over the tree for each statistic. This is not very

152
src/util/sharing_node.h
View File

@ -105,6 +105,9 @@ class sharing_node_baset
SN_TYPE_PAR_DEF class sharing_node_innert : public sharing_node_baset
{
public:
typedef small_shared_two_way_ptrt<SN_PTR_TYPE_ARGS> datat;
typedef typename datat::use_countt use_countt;
typedef d_internalt<SN_TYPE_ARGS> d_it;
typedef d_containert<SN_TYPE_ARGS> d_ct;
@ -113,18 +116,18 @@ public:
typedef typename d_ct::leaft leaft;
typedef typename d_ct::leaf_listt leaf_listt;
sharing_node_innert() : data(empty_data)
sharing_node_innert()
{
}
bool empty() const
{
return data == empty_data;
return !data;
}
void clear()
{
data = empty_data;
data.reset();
}
bool shares_with(const sharing_node_innert &other) const
@ -134,6 +137,11 @@ public:
return data == other.data;
}
use_countt use_count() const
{
return data.use_count();
}
void swap(sharing_node_innert &other)
{
data.swap(other.data);
@ -151,22 +159,6 @@ public:
return data.is_derived_v();
}
d_it &write_internal()
{
if(data == empty_data)
{
data = make_shared_derived_u<SN_PTR_TYPE_ARGS>();
}
else if(data.use_count() > 1)
{
data = make_shared_derived_u<SN_PTR_TYPE_ARGS>(*data.get_derived_u());
}
SN_ASSERT(data.use_count() == 1);
return *data.get_derived_u();
}
const d_it &read_internal() const
{
SN_ASSERT(!empty());
@ -174,22 +166,6 @@ public:
return *data.get_derived_u();
}
d_ct &write_container()
{
if(data == empty_data)
{
data = make_shared_derived_v<SN_PTR_TYPE_ARGS>();
}
else if(data.use_count() > 1)
{
data = make_shared_derived_v<SN_PTR_TYPE_ARGS>(*data.get_derived_v());
}
SN_ASSERT(data.use_count() == 1);
return *data.get_derived_v();
}
const d_ct &read_container() const
{
SN_ASSERT(!empty());
@ -338,13 +314,41 @@ public:
SN_ASSERT_USE(r, r == 1);
}
small_shared_two_way_ptrt<SN_PTR_TYPE_ARGS> data;
static small_shared_two_way_ptrt<SN_PTR_TYPE_ARGS> empty_data;
};
protected:
d_it &write_internal()
{
if(!data)
{
data = make_shared_derived_u<SN_PTR_TYPE_ARGS>();
}
else if(data.use_count() > 1)
{
data = make_shared_derived_u<SN_PTR_TYPE_ARGS>(*data.get_derived_u());
}
SN_TYPE_PAR_DEF small_shared_two_way_ptrt<SN_PTR_TYPE_ARGS>
sharing_node_innert<SN_TYPE_ARGS>::empty_data =
small_shared_two_way_ptrt<SN_PTR_TYPE_ARGS>();
SN_ASSERT(data.use_count() == 1);
return *data.get_derived_u();
}
d_ct &write_container()
{
if(!data)
{
data = make_shared_derived_v<SN_PTR_TYPE_ARGS>();
}
else if(data.use_count() > 1)
{
data = make_shared_derived_v<SN_PTR_TYPE_ARGS>(*data.get_derived_v());
}
SN_ASSERT(data.use_count() == 1);
return *data.get_derived_v();
}
datat data;
};
// Leafs
@ -362,9 +366,12 @@ public:
SN_TYPE_PAR_DEF class sharing_node_leaft : public sharing_node_baset
{
public:
typedef small_shared_ptrt<SN_PTR_TYPE_ARG> datat;
typedef decltype(datat().use_count()) use_countt;
typedef d_leaft<SN_TYPE_ARGS> d_lt;
sharing_node_leaft(const keyT &k, const valueT &v) : data(empty_data)
sharing_node_leaft(const keyT &k, const valueT &v)
{
SN_ASSERT(empty());
@ -384,12 +391,12 @@ public:
bool empty() const
{
return data == empty_data;
return !data;
}
void clear()
{
data = empty_data;
data.reset();
}
bool shares_with(const sharing_node_leaft &other) const
@ -397,34 +404,16 @@ public:
return data == other.data;
}
use_countt use_count() const
{
return data.use_count();
}
void swap(sharing_node_leaft &other)
{
data.swap(other.data);
}
d_lt &write()
{
SN_ASSERT(data.use_count() > 0);
if(data == empty_data)
{
data = make_small_shared_ptr<d_lt>();
}
else if(data.use_count() > 1)
{
data = make_small_shared_ptr<d_lt>(*data);
}
SN_ASSERT(data.use_count() == 1);
return *data;
}
const d_lt &read() const
{
return *data;
}
// Accessors
const keyT &get_key() const
@ -452,12 +441,29 @@ public:
return write().v;
}
small_shared_ptrt<SN_PTR_TYPE_ARG> data;
static small_shared_ptrt<SN_PTR_TYPE_ARG> empty_data;
const d_lt &read() const
{
return *data;
}
protected:
d_lt &write()
{
if(!data)
{
data = make_small_shared_ptr<d_lt>();
}
else if(data.use_count() > 1)
{
data = make_small_shared_ptr<d_lt>(*data);
}
SN_ASSERT(data.use_count() == 1);
return *data;
}
datat data;
};
SN_TYPE_PAR_DEF small_shared_ptrt<SN_PTR_TYPE_ARG>
sharing_node_leaft<SN_TYPE_ARGS>::empty_data =
make_small_shared_ptr<SN_PTR_TYPE_ARG>();
#endif

57
src/util/small_shared_two_way_ptr.h
View File

@ -101,30 +101,13 @@ public:
~small_shared_two_way_ptrt()
{
if(!p)
{
return;
}
destruct();
}
auto use_count = p->use_count();
if(use_count == 1)
{
if(p->is_derived_u())
{
U *u = static_cast<U *>(p);
delete u;
}
else
{
V *v = static_cast<V *>(p);
delete v;
}
}
else
{
p->decrement_use_count();
}
void reset()
{
destruct();
p = nullptr;
}
void swap(small_shared_two_way_ptrt &rhs)
@ -186,6 +169,34 @@ public:
}
private:
void destruct()
{
if(!p)
{
return;
}
auto use_count = p->use_count();
if(use_count == 1)
{
if(p->is_derived_u())
{
U *u = static_cast<U *>(p);
delete u;
}
else
{
V *v = static_cast<V *>(p);
delete v;
}
}
else
{
p->decrement_use_count();
}
}
pointeet *p = nullptr;
};

4
unit/util/sharing_map.cpp
View File

@ -385,7 +385,7 @@ void sharing_map_sharing_stats_test()
{
SECTION("count nodes")
{
std::set<void *> marked;
std::set<const void *> marked;
smt sm;
int count = 0;
@ -410,7 +410,7 @@ void sharing_map_sharing_stats_test()
SECTION("marking")
{
std::set<void *> marked;
std::set<const void *> marked;
smt sm;
fill(sm);

47
unit/util/sharing_node.cpp
View File

@ -7,7 +7,37 @@
#include <testing-utils/use_catch.h>
#include <util/sharing_node.h>
void sharing_node_test()
class leaft : public sharing_node_leaft<int, int>
{
public:
leaft(const int &a, const int &b) : sharing_node_leaft<int, int>(a, b)
{
}
friend void sharing_node_internals_test();
};
void sharing_node_internals_test()
{
SECTION("Leaf test")
{
// Detaching
{
leaft leaf(1, 2);
auto p = leaf.data.get();
leaf.write();
REQUIRE(leaf.data.get() == p);
}
}
}
TEST_CASE("Sharing node internals", "[core][util]")
{
sharing_node_internals_test();
}
TEST_CASE("Sharing node", "[core][util]")
{
SECTION("Leaf test")
{
@ -45,16 +75,6 @@ void sharing_node_test()
REQUIRE(leaf2.get_value() == 3);
REQUIRE(!leaf2.shares_with(leaf1));
}
// Detaching
{
leaft leaf(1, 2);
auto p = leaf.data.get();
leaf.write();
REQUIRE(leaf.data.get() == p);
}
}
SECTION("Inner node test")
@ -201,8 +221,3 @@ void sharing_node_test()
REQUIRE(map2.shares_with(map));
}
}
TEST_CASE("Sharing node")
{
sharing_node_test();
}

5
unit/util/small_shared_two_way_ptr.cpp
View File

@ -61,6 +61,7 @@ TEST_CASE("Small shared two-way pointer")
SECTION("Basic")
{
spt sp1;
REQUIRE(!sp1);
REQUIRE(sp1.use_count() == 0);
const d1t *p;
@ -86,6 +87,10 @@ TEST_CASE("Small shared two-way pointer")
REQUIRE(sp1.use_count() == 3);
REQUIRE(sp2.use_count() == 3);
REQUIRE(sp3.use_count() == 3);
sp1.reset();
REQUIRE(!sp1);
REQUIRE(sp1.use_count() == 0);
}
SECTION("Creation")