diff --git a/src/util/expr.cpp b/src/util/expr.cpp index af2cff9946f..3dd1cd666d5 100644 --- a/src/util/expr.cpp +++ b/src/util/expr.cpp @@ -21,64 +21,40 @@ Author: Daniel Kroening, kroening@kroening.com void exprt::move_to_operands(exprt &expr) { - operandst &op=operands(); - op.push_back(static_cast(get_nil_irep())); - op.back().swap(expr); + move_to_sub(expr); } 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(get_nil_irep())); - op.back().swap(e1); - op.push_back(static_cast(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(get_nil_irep())); - op.back().swap(e1); - op.push_back(static_cast(get_nil_irep())); - op.back().swap(e2); - op.push_back(static_cast(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) @@ -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 { diff --git a/src/util/expr.h b/src/util/expr.h index 9e18d0a0c18..a381308095e 100644 --- a/src/util/expr.h +++ b/src/util/expr.h @@ -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); diff --git a/src/util/irep.cpp b/src/util/irep.cpp index d46a06e216c..4364f99ceeb 100644 --- a/src/util/irep.cpp +++ b/src/util/irep.cpp @@ -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 @@ -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); @@ -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) { - 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 entry= - s.insert(std::make_pair(name, irep)); - if(!entry.second) - entry.first->second=irep; + return s[name]; - return entry.first->second; #endif } diff --git a/src/util/irep.h b/src/util/irep.h index fbaf0ad5a94..e444bc629bc 100644 --- a/src/util/irep.h +++ b/src/util/irep.h @@ -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 { @@ -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); @@ -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; @@ -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 diff --git a/unit/util/irep_sharing.cpp b/unit/util/irep_sharing.cpp index 86b3880bef3..64886f82c55 100644 --- a/unit/util/irep_sharing.cpp +++ b/unit/util/irep_sharing.cpp @@ -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") { @@ -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; @@ -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; @@ -104,7 +84,7 @@ SCENARIO("irept_sharing", "[core][utils][irept]") #include -SCENARIO("exprt_sharing_trade_offs", "[!mayfail][core][utils][exprt]") +SCENARIO("exprt_sharing", "[core][utils][exprt]") { GIVEN("An expression created with move_to_operands") { @@ -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; @@ -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;