diff --git a/src/util/sharing_node.h b/src/util/sharing_node.h index 1e3d29a413e..f35801f870e 100644 --- a/src/util/sharing_node.h +++ b/src/util/sharing_node.h @@ -220,7 +220,7 @@ class sharing_nodet { containert &c=get_container(); - for(typename containert::const_iterator it=c.begin(); + for(typename containert::iterator it=c.begin(); it!=c.end(); it++) { const self_type &n=*it; diff --git a/unit/Makefile b/unit/Makefile index d089a0ed540..f2f34cc9a9e 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -1,6 +1,7 @@ .PHONY: all cprover.dir test SRC = unit_tests.cpp \ + util/sharing_map.cpp \ catch_example.cpp \ # Empty last line diff --git a/unit/sharing_map.cpp b/unit/sharing_map.cpp deleted file mode 100644 index 9911f460855..00000000000 --- a/unit/sharing_map.cpp +++ /dev/null @@ -1,336 +0,0 @@ -#include -#include - -#include - -typedef sharing_mapt smt; - -// helpers -void fill(smt &sm) -{ - sm.insert("i", "0"); - sm.insert("j", "1"); - sm.insert("k", "2"); -} - -void fill2(smt &sm) -{ - sm.insert("l", "3"); - sm.insert("m", "4"); - sm.insert("n", "5"); -} - -// tests - -void sharing_map_interface_test() -{ - std::cout << "Running interface test" << std::endl; - - // empty map - { - smt sm; - - assert(sm.empty()); - assert(sm.size()==0); - assert(!sm.has_key("i")); - } - - // insert elements - { - smt sm; - - smt::const_find_type r1=sm.insert(std::make_pair("i", "0")); - assert(r1.second); - - smt::const_find_type r2=sm.insert("j", "1"); - assert(r2.second); - - smt::const_find_type r3=sm.insert(std::make_pair("i", "0")); - assert(!r3.second); - - assert(sm.size()==2); - assert(!sm.empty()); - } - - // place elements - { - smt sm1; - smt sm2(sm1); - - smt::find_type r1=sm1.place("i", "0"); - assert(r1.second); - assert(!sm2.has_key("i")); - - std::string &s1=r1.first; - s1="1"; - - assert(sm1.at("i")=="1"); - } - - // retrieve elements - { - smt sm; - sm.insert("i", "0"); - sm.insert("j", "1"); - - const smt &sm2=sm; - - std::string s; - s=sm2.at("i"); - assert(s=="0"); - - try { - sm2.at("k"); - assert(false); - } catch (...) {} - - s=sm2.at("j"); - assert(s=="1"); - - assert(sm.has_key("i")); - assert(sm.has_key("j")); - assert(!sm.has_key("k")); - - std::string &s2=sm.at("i"); - s2="3"; - assert(sm2.at("i")=="3"); - - assert(sm.size()==2); - - smt::find_type r=sm.find("i"); - assert(r.second); - r.first="4"; - assert(sm2.at("i")=="4"); - - smt::const_find_type rc=sm2.find("k"); - assert(!rc.second); - } - - // remove elements - { - smt sm; - sm.insert("i", "0"); - sm.insert("j", "1"); - - assert(sm.erase("k")==0); - assert(sm.size()==2); - - assert(sm.erase("i")==1); - assert(!sm.has_key("i")); - - assert(sm.erase("j")==1); - assert(!sm.has_key("j")); - - sm.insert("i", "0"); - sm.insert("j", "1"); - - smt sm3(sm); - - assert(sm.has_key("i")); - assert(sm.has_key("j")); - assert(sm3.has_key("i")); - assert(sm3.has_key("j")); - - sm.erase("i"); - - assert(!sm.has_key("i")); - assert(sm.has_key("j")); - - assert(sm3.has_key("i")); - assert(sm3.has_key("j")); - - sm3.erase("i"); - assert(!sm3.has_key("i")); - } - - // operator[] - { - smt sm; - - sm["i"]; - assert(sm.has_key("i")); - - sm["i"]="0"; - assert(sm.at("i")=="0"); - - sm["j"]="1"; - assert(sm.at("j")=="1"); - } -} - -void sharing_map_copy_test() -{ - std::cout << "Running copy test" << std::endl; - - smt sm1; - const smt &sm2=sm1; - - fill(sm1); - - assert(sm2.find("i").first=="0"); - assert(sm2.find("j").first=="1"); - assert(sm2.find("k").first=="2"); - - smt sm3=sm1; - const smt &sm4=sm3; - - assert(sm3.erase("l")==0); - assert(sm3.erase("i")==1); - - assert(!sm4.has_key("i")); - sm3.place("i", "3"); - assert(sm4.find("i").first=="3"); -} - -class some_keyt -{ -public: - some_keyt(size_t s) : s(s) - { - } - - size_t s; - - bool operator==(const some_keyt &other) const - { - return s==other.s; - } -}; - -class some_key_hash -{ -public: - size_t operator()(const some_keyt &k) const - { - return k.s & 0x3; - } -}; - -void sharing_map_collision_test() -{ - std::cout << "Running collision test" << std::endl; - - typedef sharing_mapt smt; - - smt sm; - - sm.insert(0, "a"); - sm.insert(8, "b"); - sm.insert(16, "c"); - - sm.insert(1, "d"); - sm.insert(2, "e"); - - sm.erase(8); - - assert(sm.has_key(0)); - assert(sm.has_key(16)); - - assert(sm.has_key(1)); - assert(sm.has_key(2)); - - assert(!sm.has_key(8)); -} - -void sharing_map_view_test() -{ - std::cout << "Running view test" << std::endl; - - // view test - { - smt sm; - - fill(sm); - - smt::viewt view; - sm.get_view(view); - - assert(view.size()==3); - } - - // delta view test (no sharing, same keys) - { - smt sm1; - fill(sm1); - - smt sm2; - fill(sm2); - - smt::delta_viewt delta_view; - - sm1.get_delta_view(sm2, delta_view); - assert(delta_view.size()==3); - - delta_view.clear(); - sm1.get_delta_view(sm2, delta_view, false); - assert(delta_view.size()==3); - } - - // delta view test (all shared, same keys) - { - smt sm1; - fill(sm1); - - smt sm2(sm1); - - smt::delta_viewt delta_view; - - sm1.get_delta_view(sm2, delta_view); - assert(delta_view.size()==0); - - delta_view.clear(); - sm1.get_delta_view(sm2, delta_view, false); - assert(delta_view.size()==0); - } - - // delta view test (some sharing, same keys) - { - smt sm1; - fill(sm1); - - smt sm2(sm1); - auto r=sm2.find("i"); - assert(r.second); - r.first="3"; - - smt::delta_viewt delta_view; - - sm1.get_delta_view(sm2, delta_view); - assert(delta_view.size()>0); // not everything is shared - assert(delta_view.size()<3); // there is some sharing - - delta_view.clear(); - sm1.get_delta_view(sm2, delta_view, false); - assert(delta_view.size()>0); // not everything is shared - assert(delta_view.size()<3); // there is some sharing - } - - // delta view test (no sharing, different keys) - { - smt sm1; - fill(sm1); - - smt sm2; - fill2(sm2); - - smt::delta_viewt delta_view; - - sm1.get_delta_view(sm2, delta_view); - assert(delta_view.size()==0); - - delta_view.clear(); - sm1.get_delta_view(sm2, delta_view, false); - assert(delta_view.size()==3); - } -} - -int main() -{ - sharing_map_interface_test(); - sharing_map_copy_test(); - sharing_map_collision_test(); - sharing_map_view_test(); - - return 0; -} - diff --git a/unit/util/sharing_map.cpp b/unit/util/sharing_map.cpp new file mode 100644 index 00000000000..662dfc1649c --- /dev/null +++ b/unit/util/sharing_map.cpp @@ -0,0 +1,317 @@ +/*******************************************************************\ + + Module: Unit tests for the util/sharing_map + + Author: DiffBlue Limited. All rights reserved. + +\*******************************************************************/ + +#include + +#include +#include + +typedef sharing_mapt smt; + +// helpers +void fill(smt &sm) +{ + sm.insert("i", "0"); + sm.insert("j", "1"); + sm.insert("k", "2"); +} + +void fill2(smt &sm) +{ + sm.insert("l", "3"); + sm.insert("m", "4"); + sm.insert("n", "5"); +} + +typedef size_t some_keyt; + +class some_key_hasht +{ +public: + size_t operator()(const some_keyt &k) const + { + return k & 0x3; + } +}; + + + +TEST_CASE("sharing map", "[core][util][sharing_map]") +{ + SECTION("interface") + { + SECTION("empty map") + { + smt sm; + REQUIRE(sm.empty()); + REQUIRE(sm.size()==0); + REQUIRE(!sm.has_key("i")); + } + + SECTION("insert elements") + { + smt sm; + + smt::const_find_type r1=sm.insert(std::make_pair("i", "0")); + REQUIRE(r1.second); + + smt::const_find_type r2=sm.insert("j", "1"); + REQUIRE(r2.second); + + smt::const_find_type r3=sm.insert(std::make_pair("i", "0")); + REQUIRE(!r3.second); + + REQUIRE(sm.size()==2); + REQUIRE_FALSE(sm.empty()); + } + + SECTION("place elements") + { + smt sm1; + smt sm2(sm1); + + smt::find_type r1=sm1.place("i", "0"); + REQUIRE(r1.second); + REQUIRE_FALSE(sm2.has_key("i")); + + std::string &s1=r1.first; + s1="1"; + + REQUIRE(sm1.at("i")=="1"); + } + SECTION("retrieve elements") + { + smt sm; + sm.insert("i", "0"); + sm.insert("j", "1"); + + const smt &sm2=sm; + + std::string s; + s=sm2.at("i"); + REQUIRE(s=="0"); + + try + { + sm2.at("k"); + REQUIRE(false); + } catch (...) {} + + s=sm2.at("j"); + REQUIRE(s=="1"); + + REQUIRE(sm.has_key("i")); + REQUIRE(sm.has_key("j")); + REQUIRE_FALSE(sm.has_key("k")); + + std::string &s2=sm.at("i"); + s2="3"; + REQUIRE(sm2.at("i")=="3"); + + REQUIRE(sm.size()==2); + + smt::find_type r=sm.find("i"); + REQUIRE(r.second); + r.first="4"; + REQUIRE(sm2.at("i")=="4"); + + smt::const_find_type rc=sm2.find("k"); + REQUIRE_FALSE(rc.second); + } + + + SECTION("remove elements") + { + smt sm; + sm.insert("i", "0"); + sm.insert("j", "1"); + + REQUIRE(sm.erase("k")==0); + REQUIRE(sm.size()==2); + + REQUIRE(sm.erase("i")==1); + REQUIRE(!sm.has_key("i")); + + REQUIRE(sm.erase("j")==1); + REQUIRE(!sm.has_key("j")); + + sm.insert("i", "0"); + sm.insert("j", "1"); + + smt sm3(sm); + + REQUIRE(sm.has_key("i")); + REQUIRE(sm.has_key("j")); + REQUIRE(sm3.has_key("i")); + REQUIRE(sm3.has_key("j")); + + sm.erase("i"); + + REQUIRE(!sm.has_key("i")); + REQUIRE(sm.has_key("j")); + + REQUIRE(sm3.has_key("i")); + REQUIRE(sm3.has_key("j")); + + sm3.erase("i"); + REQUIRE(!sm3.has_key("i")); + } + + SECTION("operator[]") + { + smt sm; + + sm["i"]; + REQUIRE(sm.has_key("i")); + + sm["i"]="0"; + REQUIRE(sm.at("i")=="0"); + + sm["j"]="1"; + REQUIRE(sm.at("j")=="1"); + } + } + + SECTION("copy") + { + smt sm1; + const smt &sm2=sm1; + + fill(sm1); + + REQUIRE(sm2.find("i").first=="0"); + REQUIRE(sm2.find("j").first=="1"); + REQUIRE(sm2.find("k").first=="2"); + + smt sm3=sm1; + const smt &sm4=sm3; + + REQUIRE(sm3.erase("l")==0); + REQUIRE(sm3.erase("i")==1); + + REQUIRE(!sm4.has_key("i")); + sm3.place("i", "3"); + REQUIRE(sm4.find("i").first=="3"); + } + + SECTION("collision_test") + { + typedef sharing_mapt sm2t; + + sm2t sm; + + sm.insert(0, "a"); + sm.insert(8, "b"); + sm.insert(16, "c"); + + sm.insert(1, "d"); + sm.insert(2, "e"); + + sm.erase(8); + + REQUIRE(sm.has_key(0)); + REQUIRE(sm.has_key(16)); + + REQUIRE(sm.has_key(1)); + REQUIRE(sm.has_key(2)); + + REQUIRE(!sm.has_key(8)); + } + + SECTION("view_test") + { + SECTION("view test") + { + smt sm; + + fill(sm); + + smt::viewt view; + sm.get_view(view); + + REQUIRE(view.size()==3); + } + + SECTION("delta view test (no sharing, same keys)") + { + smt sm1; + fill(sm1); + + smt sm2; + fill(sm2); + + smt::delta_viewt delta_view; + + sm1.get_delta_view(sm2, delta_view); + REQUIRE(delta_view.size()==3); + + delta_view.clear(); + sm1.get_delta_view(sm2, delta_view, false); + REQUIRE(delta_view.size()==3); + } + + SECTION("delta view test (all shared, same keys)") + { + smt sm1; + fill(sm1); + + smt sm2(sm1); + + smt::delta_viewt delta_view; + + sm1.get_delta_view(sm2, delta_view); + REQUIRE(delta_view.size()==0); + + delta_view.clear(); + sm1.get_delta_view(sm2, delta_view, false); + REQUIRE(delta_view.size()==0); + } + + SECTION("delta view test (some sharing, same keys)") + { + smt sm1; + fill(sm1); + + smt sm2(sm1); + auto r=sm2.find("i"); + REQUIRE(r.second); + r.first="3"; + + smt::delta_viewt delta_view; + + sm1.get_delta_view(sm2, delta_view); + REQUIRE(delta_view.size()>0); // not everything is shared + REQUIRE(delta_view.size()<3); // there is some sharing + + delta_view.clear(); + sm1.get_delta_view(sm2, delta_view, false); + REQUIRE(delta_view.size()>0); // not everything is shared + REQUIRE(delta_view.size()<3); // there is some sharing + } + + SECTION("delta view test (no sharing, different keys)") + { + smt sm1; + fill(sm1); + + smt sm2; + fill2(sm2); + + smt::delta_viewt delta_view; + + sm1.get_delta_view(sm2, delta_view); + REQUIRE(delta_view.size()==0); + + delta_view.clear(); + sm1.get_delta_view(sm2, delta_view, false); + REQUIRE(delta_view.size()==3); + } + } +} + +