From 2239ec1d91cefb88462d7f6359b35019e99173c4 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 22 Mar 2018 18:45:32 +0000 Subject: [PATCH 1/2] Unit test of irept's public API --- unit/Makefile | 1 + unit/util/irep.cpp | 224 +++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 225 insertions(+) create mode 100644 unit/util/irep.cpp diff --git a/unit/Makefile b/unit/Makefile index 1157bb72db0..010311e454d 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -45,6 +45,7 @@ SRC += unit_tests.cpp \ solvers/refinement/string_refinement/union_find_replace.cpp \ util/expr_cast/expr_cast.cpp \ util/expr_iterator.cpp \ + util/irep.cpp \ util/message.cpp \ util/parameter_indices.cpp \ util/simplify_expr.cpp \ diff --git a/unit/util/irep.cpp b/unit/util/irep.cpp new file mode 100644 index 00000000000..c33ec3c181c --- /dev/null +++ b/unit/util/irep.cpp @@ -0,0 +1,224 @@ +// Copyright 2018 Michael Tautschnig + +/// \file Tests that irept memory consumption is fixed + +#include +#include + +SCENARIO("irept_memory", "[core][utils][irept]") +{ + GIVEN("Always") + { + THEN("An irept is just a pointer") + { + REQUIRE(sizeof(irept) == sizeof(void *)); + } + + THEN("get_nil_irep yields ID_nil") + { + REQUIRE(get_nil_irep().id() == ID_nil); + REQUIRE(get_nil_irep().is_nil()); + REQUIRE(!get_nil_irep().is_not_nil()); + } + } + + GIVEN("An initialized irep") + { + irept irep("some_id"); + irept irep_copy(irep); + irept irep_assign = irep; + + irept irep_other("some_other_id"); + + THEN("Its id is some_id") + { + REQUIRE(irep.id() == "some_id"); + REQUIRE(irep_copy.id() == "some_id"); + REQUIRE(irep_assign.id() == "some_id"); + + REQUIRE(irep_other.id() == "some_other_id"); + + // TODO(tautschnig): id_string() should be deprecated in favour of + // id2string(...) + REQUIRE(irep.id_string().size() == 7); + } + + THEN("Swapping works") + { + irep.swap(irep_other); + + REQUIRE(irep.id() == "some_other_id"); + REQUIRE(irep_copy.id() == "some_id"); + REQUIRE(irep_assign.id() == "some_id"); + + REQUIRE(irep_other.id() == "some_id"); + } + } + + GIVEN("An irep") + { + irept irep; + + THEN("Its id is empty") + { + REQUIRE(irep.is_not_nil()); + REQUIRE(irep.id().empty()); + } + + THEN("Its id can be set") + { + irep.id("new_id"); + REQUIRE(irep.id() == "new_id"); + } + + THEN("find of a non-existent element yields nil") + { + REQUIRE(irep.find("no-such-element").is_nil()); + } + + THEN("Adding/removing elements is possible") + { + REQUIRE(irep.get_sub().empty()); + REQUIRE(irep.get_named_sub().empty()); + REQUIRE(irep.get_comments().empty()); + + irept &e = irep.add("a_new_element"); + REQUIRE(e.id().empty()); + e.id("some_id"); + REQUIRE(irep.find("a_new_element").id() == "some_id"); + + irept irep2("second_irep"); + irep.add("a_new_element", irep2); + REQUIRE(irep.find("a_new_element").id() == "second_irep"); + REQUIRE(irep.get_named_sub().size() == 1); + + irep.add("#a_comment", irep2); + REQUIRE(irep.find("#a_comment").id() == "second_irep"); + REQUIRE(irep.get_comments().size() == 1); + + irept bak(irep); + irep.remove("no_such_id"); + REQUIRE(bak == irep); + irep.remove("a_new_element"); + REQUIRE(bak != irep); + REQUIRE(irep.find("a_new_element").is_nil()); + + irep.move_to_sub(bak); + REQUIRE(irep.get_sub().size() == 1); + + irep.move_to_named_sub("another_entry", irep2); + REQUIRE(irep.get_sub().size() == 1); + REQUIRE(irep.get_named_sub().size() == 1); + REQUIRE(irep.get_comments().size() == 1); + + irept irep3; + irep.move_to_named_sub("#a_comment", irep3); + REQUIRE(irep.find("#a_comment").id().empty()); + REQUIRE(irep.get_sub().size() == 1); + REQUIRE(irep.get_named_sub().size() == 1); + REQUIRE(irep.get_comments().size() == 1); + + irept irep4; + irep.move_to_named_sub("#another_comment", irep4); + REQUIRE(irep.get_comments().size() == 2); + } + + THEN("Setting and getting works") + { + // TODO(tautschnig): get_string() should be deprecated in favour of + // id2string(...) + REQUIRE(irep.get_string("no_such_id").empty()); + + REQUIRE(irep.get("no_such_id").empty()); + // TODO(tautschnig): it's not clear whether we need all of the below + // variants in the API + REQUIRE(!irep.get_bool("no_such_id")); + REQUIRE(irep.get_int("no_such_id") == 0); + REQUIRE(irep.get_unsigned_int("no_such_id") == 0u); + REQUIRE(irep.get_size_t("no_such_id") == 0u); + REQUIRE(irep.get_long_long("no_such_id") == 0); + + irep.set("some_id", "some string"); + REQUIRE(irep.get("some_id") == "some string"); + irept irep2("second_irep"); + irep.set("a_new_element", irep2); + REQUIRE(irep.find("a_new_element").id() == "second_irep"); + irep.set("numeric_id", 1); + REQUIRE(irep.get_bool("numeric_id")); + irep.set("numeric_id", 42); + REQUIRE(!irep.get_bool("numeric_id")); + REQUIRE(irep.get_int("numeric_id") == 42); + REQUIRE(irep.get_unsigned_int("numeric_id") == 42u); + REQUIRE(irep.get_size_t("numeric_id") == 42u); + REQUIRE(irep.get_long_long("numeric_id") == 42); + + irep.clear(); + REQUIRE(irep.id().empty()); + REQUIRE(irep.get_sub().empty()); + REQUIRE(irep.get_named_sub().empty()); + REQUIRE(irep.get_comments().empty()); + + irep.make_nil(); + REQUIRE(irep.id() == ID_nil); + REQUIRE(irep.get_sub().empty()); + REQUIRE(irep.get_named_sub().empty()); + REQUIRE(irep.get_comments().empty()); + } + + THEN("Pretty printing works") + { + irept sub("sub_id"); + + irep.id("our_id"); + irep.add("some_op", sub); + irep.add("#comment", sub); + irep.move_to_sub(sub); + + std::string pretty = irep.pretty(); + REQUIRE( + pretty == + "our_id\n" + " * some_op: sub_id\n" + " * #comment: sub_id\n" + " 0: sub_id"); + } + + THEN("Hashing works") + { + irep.id("some_id"); + irep.set("#a_comment", 42); + + REQUIRE(irep.hash() != 0); + REQUIRE(irep.full_hash() != 0); + REQUIRE(irep.hash() != irep.full_hash()); + } + } + + GIVEN("Multiple ireps") + { + irept irep1, irep2; + + THEN("Comparison works") + { + REQUIRE(irep1 == irep2); + REQUIRE(irep1.full_eq(irep2)); + + irep1.id("id1"); + irep2.id("id2"); + REQUIRE(irep1 != irep2); + const bool one_lt_two = irep1 < irep2; + const bool two_lt_one = irep2 < irep1; + REQUIRE(one_lt_two != two_lt_one); + REQUIRE(irep1.ordering(irep2) != irep2.ordering(irep1)); + REQUIRE(irep1.compare(irep2) != 0); + + irep2.id("id1"); + REQUIRE(irep1 == irep2); + REQUIRE(irep1.full_eq(irep2)); + + irep2.set("#a_comment", 42); + REQUIRE(irep1 == irep2); + REQUIRE(!irep1.full_eq(irep2)); + } + } +} From 0902ae78156d11c612442655aec5f4e8ae703bee Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Fri, 16 Feb 2018 13:43:33 +0000 Subject: [PATCH 2/2] Tests to demonstrate expected sharing behaviour of irept --- unit/Makefile | 1 + unit/util/irep_sharing.cpp | 202 +++++++++++++++++++++++++++++++++++++ 2 files changed, 203 insertions(+) create mode 100644 unit/util/irep_sharing.cpp diff --git a/unit/Makefile b/unit/Makefile index 010311e454d..11468e5cf2f 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -46,6 +46,7 @@ SRC += unit_tests.cpp \ util/expr_cast/expr_cast.cpp \ util/expr_iterator.cpp \ util/irep.cpp \ + util/irep_sharing.cpp \ util/message.cpp \ util/parameter_indices.cpp \ util/simplify_expr.cpp \ diff --git a/unit/util/irep_sharing.cpp b/unit/util/irep_sharing.cpp new file mode 100644 index 00000000000..86b3880bef3 --- /dev/null +++ b/unit/util/irep_sharing.cpp @@ -0,0 +1,202 @@ +/// Author: Diffblue Ltd. + +/// \file Tests that irep sharing works correctly + +#include +#include + +#ifdef SHARING + +SCENARIO("irept_sharing_trade_offs", "[!mayfail][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("Calling read() on a copy should return object with the same address") + { + 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; + irept irep2 = irep1; + REQUIRE(&irep1.read() == &irep2.read()); + } + THEN("Changing subs in the original should not change them in a copy") + { + irept irep = test_irep; + test_irep.get_sub()[0].id(ID_0); + REQUIRE(irep.get_sub()[0].id() == ID_1); + } + THEN("Changing subs in a copy should not change them in the original") + { + irept irep = test_irep; + irep.get_sub()[0].id(ID_0); + REQUIRE(test_irep.get_sub()[0].id() == ID_1); + REQUIRE(irep.get_sub()[0].id() == ID_0); + } + THEN("Getting a reference to a sub in a copy should break sharing") + { + irept irep = test_irep; + irept &sub = irep.get_sub()[0]; + REQUIRE(&irep.read() != &test_irep.read()); + sub = irept(ID_0); + REQUIRE(irep.get_sub()[0].id() != test_irep.get_sub()[0].id()); + } + THEN( + "Getting a reference to a sub in the original should break sharing") + { + irept irep = test_irep; + irept &sub = test_irep.get_sub()[0]; + REQUIRE(&irep.read() != &test_irep.read()); + sub = irept(ID_0); + REQUIRE(irep.get_sub()[0].id() != test_irep.get_sub()[0].id()); + } + THEN("Changing an id in the original should break sharing") + { + irept irep = test_irep; + test_irep.id(ID_0); + REQUIRE(&irep.read() != &test_irep.read()); + REQUIRE(irep.id() != test_irep.id()); + } + THEN("Changing an id should not prevent sharing") + { + test_irep.id(ID_0); + irept irep = test_irep; + REQUIRE(&irep.read() == &test_irep.read()); + } + } +} + +#include + +SCENARIO("exprt_sharing_trade_offs", "[!mayfail][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("Calling read() on a copy should return object with the same address") + { + 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; + exprt expr2 = expr1; + REQUIRE(&expr1.read() == &expr2.read()); + } + THEN("Changing operands in the original should not change them in a copy") + { + exprt expr = test_expr; + test_expr.op0().id(ID_0); + REQUIRE(expr.op0().id() == ID_1); + } + THEN("Changing operands in a copy should not change them in the original") + { + exprt expr = test_expr; + expr.op0().id(ID_0); + REQUIRE(test_expr.op0().id() == ID_1); + REQUIRE(expr.op0().id() == ID_0); + } + THEN("Getting a reference to an operand in a copy should break sharing") + { + exprt expr = test_expr; + exprt &operand = expr.op0(); + REQUIRE(&expr.read() != &test_expr.read()); + operand = exprt(ID_0); + REQUIRE(expr.op0().id() != test_expr.op0().id()); + } + THEN( + "Getting a reference to an operand in the original should break sharing") + { + exprt expr = test_expr; + exprt &operand = test_expr.op0(); + REQUIRE(&expr.read() != &test_expr.read()); + operand = exprt(ID_0); + REQUIRE(expr.op0().id() != test_expr.op0().id()); + } + THEN("Changing an id in the original should break sharing") + { + exprt expr = test_expr; + test_expr.id(ID_0); + REQUIRE(&expr.read() != &test_expr.read()); + REQUIRE(expr.id() != test_expr.id()); + } + THEN("Changing an id should not prevent sharing") + { + test_expr.id(ID_0); + exprt expr = test_expr; + REQUIRE(&expr.read() == &test_expr.read()); + } + } +} + +#endif