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,12 +86,12 @@ 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;
 
-  goto_symext::merge_goto(goto_state, state);
+  goto_symext::merge_goto(std::move(goto_state), state);
 
   PRECONDITION(prev_pc->is_goto());
   if(

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

@@ -232,12 +232,15 @@ class goto_symext
 
   virtual void symex_assume(statet &, const exprt &cond);
 
-  // gotos
+  /// Merge all branches joining at the current program point. Applies
+  /// \ref merge_goto for each goto state (each of which corresponds to previous
+  /// branch).
   void merge_gotos(statet &);
 
-  virtual void merge_goto(const goto_statet &goto_state, statet &);
-
-  void merge_value_sets(const goto_statet &goto_state, statet &dest);
+  /// Merge a single branch, the symbolic state of which is held in \p
+  /// goto_state, into the current overall symbolic state. \p goto_state is no
+  /// longer expected to be valid afterwards.
+  virtual void merge_goto(goto_statet &&goto_state, statet &);
 
   void phi_function(const goto_statet &goto_state, statet &);
 

src/goto-symex/symex_goto.cpp

@@ -312,13 +312,13 @@ void goto_symext::merge_gotos(statet &state)
 
   for(auto list_it = state_list.rbegin(); list_it != state_list.rend();
       ++list_it)
-    merge_goto(*list_it, state);
+    merge_goto(std::move(*list_it), state);
 
   // clean up to save some memory
   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)
@@ -329,7 +329,11 @@ void goto_symext::merge_goto(const goto_statet &goto_state, statet &state)
   // do SSA phi functions
   phi_function(goto_state, state);
 
-  merge_value_sets(goto_state, state);
+  // merge value sets
+  if(state.guard.is_false() && !goto_state.guard.is_false())
+    state.value_set = std::move(goto_state.value_set);
+  else if(!goto_state.guard.is_false())
+    state.value_set.make_union(goto_state.value_set);
 
   // adjust guard
   state.guard|=goto_state.guard;
@@ -338,17 +342,6 @@ 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)
-{
-  if(dest.guard.is_false())
-  {
-    dest.value_set=src.value_set;
-    return;
-  }
-
-  dest.value_set.make_union(src.value_set);
-}
-
 /// Applies f to `(k, ssa, i, j)` if the first map maps k to (ssa, i) and
 /// the second to (ssa', j). If the first map has an entry for k but not the
 /// second one then j is 0, and when the first map has no entry for k then i = 0

src/pointer-analysis/value_set.h

@@ -47,6 +47,14 @@ class value_sett
 
   virtual ~value_sett() = default;
 
+  value_sett(const value_sett &other) = default;
+
+  value_sett &operator=(value_sett &&other)
+  {
+    values = std::move(other.values);
+    return *this;
+  }
+
   static bool field_sensitive(const irep_idt &id, const typet &type);
 
   /// Matches the location_number field of the instruction that corresponds