merge_value_sets: Avoid assignment when actually values can be moved

We don't need the contents of the source anymore. Running on SV-COMP's
ReachSafety-ECA, this saves 741s, which is approximately 9% of the runtime of
goto_symext::merge_goto.

Author: tautschnig

src/goto-checker/symex_bmc.cpp

@@ -86,7 +86,7 @@ void symex_bmct::symex_step(
   }
 }
 
-void symex_bmct::merge_goto(const goto_statet &goto_state, statet &state)
+void symex_bmct::merge_goto(goto_statet &goto_state, statet &state)
 {
   const goto_programt::const_targett prev_pc = goto_state.source.pc;
   const guardt prev_guard = goto_state.guard;

src/goto-checker/symex_bmc.h

@@ -94,7 +94,7 @@ class symex_bmct : public goto_symext
   void symex_step(const get_goto_functiont &get_goto_function, statet &state)
     override;
 
-  void merge_goto(const goto_statet &goto_state, statet &state) override;
+  void merge_goto(goto_statet &goto_state, statet &state) override;
 
   bool should_stop_unwind(
     const symex_targett::sourcet &source,

src/goto-symex/goto_symex.h

@@ -251,9 +251,9 @@ class goto_symext
   // gotos
   void merge_gotos(statet &);
 
-  virtual void merge_goto(const goto_statet &goto_state, statet &);
+  virtual void merge_goto(goto_statet &goto_state, statet &);
 
-  void merge_value_sets(const goto_statet &goto_state, statet &dest);
+  void merge_value_sets(goto_statet &goto_state, statet &dest);
 
   void phi_function(const goto_statet &goto_state, statet &);
 

src/goto-symex/symex_goto.cpp

@@ -318,7 +318,7 @@ void goto_symext::merge_gotos(statet &state)
   frame.goto_state_map.erase(state_map_it);
 }
 
-void goto_symext::merge_goto(const goto_statet &goto_state, statet &state)
+void goto_symext::merge_goto(goto_statet &goto_state, statet &state)
 {
   // check atomic section
   if(state.atomic_section_id != goto_state.atomic_section_id)
@@ -338,11 +338,13 @@ void goto_symext::merge_goto(const goto_statet &goto_state, statet &state)
   state.depth=std::min(state.depth, goto_state.depth);
 }
 
-void goto_symext::merge_value_sets(const goto_statet &src, statet &dest)
+void goto_symext::merge_value_sets(goto_statet &src, statet &dest)
 {
   if(dest.guard.is_false())
   {
-    dest.value_set=src.value_set;
+    // we don't actually need dest.value_set anymore, leave cleanup to later
+    // cleanup of goto states
+    dest.value_set.swap(src.value_set);
     return;
   }
 

src/pointer-analysis/value_set.h

@@ -308,6 +308,11 @@ class value_sett
     values.clear();
   }
 
+  void swap(value_sett &other)
+  {
+    std::swap(values, other.values);
+  }
+
   /// Finds an entry in this value-set. The interface differs from get_entry
   /// because get_value_set_rec wants to check for a struct's first component
   /// before stripping the suffix as is done in get_entry.