From 8c4d8c5373f2b59124c274c8dc66b5f018235774 Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Wed, 10 May 2017 11:41:29 +0100 Subject: [PATCH 1/2] Enable goto_modelt move assignment Propagate this change through goto_programt and goto_function_templatet --- src/goto-programs/goto_functions_template.h | 25 ++++++++++++++---- src/goto-programs/goto_model.h | 24 +++++++++++++---- src/goto-programs/goto_program.h | 24 ++++++++++++++++- src/goto-programs/goto_program_template.h | 29 ++++++++++++++------- 4 files changed, 81 insertions(+), 21 deletions(-) diff --git a/src/goto-programs/goto_functions_template.h b/src/goto-programs/goto_functions_template.h index 7c427b4f72f..0618774f57e 100644 --- a/src/goto-programs/goto_functions_template.h +++ b/src/goto-programs/goto_functions_template.h @@ -66,18 +66,33 @@ class goto_function_templatet parameter_identifiers.swap(other.parameter_identifiers); } - void copy_from(const goto_function_templatet &other) + void copy_from(const goto_function_templatet &other) { body.copy_from(other.body); type=other.type; parameter_identifiers=other.parameter_identifiers; } - goto_function_templatet(const goto_function_templatet &src): - type(src.type), - parameter_identifiers(src.parameter_identifiers) + goto_function_templatet(const goto_function_templatet &other) + : type(other.type), + parameter_identifiers(other.parameter_identifiers) { - body.copy_from(src.body); + body.copy_from(other.body); + } + + goto_function_templatet(goto_function_templatet &&other): + body(std::move(other.body)), + type(std::move(other.type)), + parameter_identifiers(std::move(other.parameter_identifiers)) + { + } + + goto_function_templatet &operator=(goto_function_templatet &&other) + { + body=std::move(other.body); + type=std::move(other.type); + parameter_identifiers=std::move(other.parameter_identifiers); + return *this; } }; diff --git a/src/goto-programs/goto_model.h b/src/goto-programs/goto_model.h index ff7a671e074..37b491dc996 100644 --- a/src/goto-programs/goto_model.h +++ b/src/goto-programs/goto_model.h @@ -38,14 +38,28 @@ class goto_modelt { } - goto_modelt(goto_modelt &&other) + // Copying is normally too expensive + goto_modelt(const goto_modelt &)=delete; + goto_modelt &operator=(const goto_modelt &)=delete; + + // Move operations need to be explicitly enabled as they are deleted with the + // copy operations + // default for move operations isn't available on Windows yet, so define + // explicitly (see https://msdn.microsoft.com/en-us/library/hh567368.aspx + // under "Defaulted and Deleted Functions") + + goto_modelt(goto_modelt &&other): + symbol_table(std::move(other.symbol_table)), + goto_functions(std::move(other.goto_functions)) { - symbol_table.swap(other.symbol_table); - goto_functions.swap(other.goto_functions); } - // copying is likely too expensive - goto_modelt(const goto_modelt &) = delete; + goto_modelt &operator=(goto_modelt &&other) + { + symbol_table=std::move(other.symbol_table); + goto_functions=std::move(other.goto_functions); + return *this; + } }; #endif // CPROVER_GOTO_PROGRAMS_GOTO_MODEL_H diff --git a/src/goto-programs/goto_program.h b/src/goto-programs/goto_program.h index 06e2895529f..83fb020c096 100644 --- a/src/goto-programs/goto_program.h +++ b/src/goto-programs/goto_program.h @@ -15,7 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "goto_program_template.h" -/*! \brief A specialization of goto_program_templatet do +/*! \brief A specialization of goto_program_templatet over goto programs in which instructions have codet type. \ingroup gr_goto_programs */ @@ -36,6 +36,28 @@ class goto_programt:public goto_program_templatet goto_programt() { } + // Copying is unavailable as base class copy is deleted + // MSVC is unable to automatically determine this + goto_programt(const goto_programt &)=delete; + goto_programt &operator=(const goto_programt &)=delete; + + // Move operations need to be explicitly enabled as they are deleted with the + // copy operations + // default for move operations isn't available on Windows yet, so define + // explicitly (see https://msdn.microsoft.com/en-us/library/hh567368.aspx + // under "Defaulted and Deleted Functions") + + goto_programt(goto_programt &&other): + goto_program_templatet(std::move(other)) + { + } + + goto_programt &operator=(goto_programt &&other) + { + goto_program_templatet::operator=(std::move(other)); + return *this; + } + // get the variables in decl statements typedef std::set decl_identifierst; void get_decl_identifiers(decl_identifierst &decl_identifiers) const; diff --git a/src/goto-programs/goto_program_template.h b/src/goto-programs/goto_program_template.h index 6b42ad250ea..dd6e0ae74b3 100644 --- a/src/goto-programs/goto_program_template.h +++ b/src/goto-programs/goto_program_template.h @@ -56,17 +56,26 @@ template class goto_program_templatet { public: - /*! \brief copy constructor - \param[in] src an empty goto program - \remark Use copy_from to copy non-empty goto-programs - */ - goto_program_templatet(const goto_program_templatet &src)=delete; + // Copying is deleted as this class contains pointers that cannot be copied + goto_program_templatet(const goto_program_templatet &)=delete; + goto_program_templatet &operator=(const goto_program_templatet &)=delete; - /*! \brief assignment operator - \param[in] src an empty goto program - \remark Use copy_from to copy non-empty goto-programs - */ - goto_program_templatet &operator=(const goto_program_templatet &src)=delete; + // Move operations need to be explicitly enabled as they are deleted with the + // copy operations + // default for move operations isn't available on Windows yet, so define + // explicitly (see https://msdn.microsoft.com/en-us/library/hh567368.aspx + // under "Defaulted and Deleted Functions") + + goto_program_templatet(goto_program_templatet &&other): + instructions(std::move(other.instructions)) + { + } + + goto_program_templatet &operator=(goto_program_templatet &&other) + { + instructions=std::move(other.instructions); + return *this; + } /*! \brief Container for an instruction of the goto-program */ From 389fbcd22bddc7475bae0e2bceed512f9c1c9389 Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Wed, 10 May 2017 13:41:29 +0100 Subject: [PATCH 2/2] Removed copy constructor from goto_function_templatet Rather than telling people not to use the copy constructor, actually don't use it --- src/goto-instrument/wmm/goto2graph.cpp | 9 ++++---- src/goto-programs/goto_functions.h | 23 +++++++++++++++++++++ src/goto-programs/goto_functions_template.h | 22 ++++++++++++-------- 3 files changed, 40 insertions(+), 14 deletions(-) diff --git a/src/goto-instrument/wmm/goto2graph.cpp b/src/goto-instrument/wmm/goto2graph.cpp index beb96579f34..390a21b6c3a 100644 --- a/src/goto-instrument/wmm/goto2graph.cpp +++ b/src/goto-instrument/wmm/goto2graph.cpp @@ -1532,13 +1532,12 @@ bool instrumentert::is_cfg_spurious(const event_grapht::critical_cyclet &cyc) } /* now test whether this part of the code can exist */ + goto_functionst::function_mapt map; goto_function_templatet one_interleaving; one_interleaving.body.copy_from(interleaving); - - std::pair > p( - goto_functionst::entry_point(), one_interleaving); - goto_functionst::function_mapt map; - map.insert(p); + map.insert(std::make_pair( + goto_functionst::entry_point(), + std::move(one_interleaving))); goto_functionst this_interleaving; this_interleaving.function_map=std::move(map); diff --git a/src/goto-programs/goto_functions.h b/src/goto-programs/goto_functions.h index 60c7fa90658..096fab391ec 100644 --- a/src/goto-programs/goto_functions.h +++ b/src/goto-programs/goto_functions.h @@ -17,6 +17,29 @@ Date: June 2003 class goto_functionst:public goto_functions_templatet { public: + goto_functionst()=default; + + // Copying is unavailable as base class copy is deleted + // MSVC is unable to automatically determine this + goto_functionst(const goto_functionst &)=delete; + goto_functionst &operator=(const goto_functionst &)=delete; + + // Move operations need to be explicitly enabled as they are deleted with the + // copy operations + // default for move operations isn't available on Windows yet, so define + // explicitly (see https://msdn.microsoft.com/en-us/library/hh567368.aspx + // under "Defaulted and Deleted Functions") + + goto_functionst(goto_functionst &&other): + goto_functions_templatet(std::move(other)) + { + } + + goto_functionst &operator=(goto_functionst &&other) + { + goto_functions_templatet::operator=(std::move(other)); + return *this; + } }; #define Forall_goto_functions(it, functions) \ diff --git a/src/goto-programs/goto_functions_template.h b/src/goto-programs/goto_functions_template.h index 0618774f57e..9333cce06b3 100644 --- a/src/goto-programs/goto_functions_template.h +++ b/src/goto-programs/goto_functions_template.h @@ -73,12 +73,8 @@ class goto_function_templatet parameter_identifiers=other.parameter_identifiers; } - goto_function_templatet(const goto_function_templatet &other) - : type(other.type), - parameter_identifiers(other.parameter_identifiers) - { - body.copy_from(other.body); - } + goto_function_templatet(const goto_function_templatet &)=delete; + goto_function_templatet &operator=(const goto_function_templatet &)=delete; goto_function_templatet(goto_function_templatet &&other): body(std::move(other.body)), @@ -108,10 +104,18 @@ class goto_functions_templatet { } - // copy constructor, don't use me! - goto_functions_templatet(const goto_functions_templatet &src) + goto_functions_templatet(const goto_functions_templatet &)=delete; + goto_functions_templatet &operator=(const goto_functions_templatet &)=delete; + + goto_functions_templatet(goto_functions_templatet &&other): + function_map(std::move(other.function_map)) + { + } + + goto_functions_templatet &operator=(goto_functions_templatet &&other) { - assert(src.function_map.empty()); + function_map=std::move(other.function_map); + return *this; } void clear()