Optimise symex state management for straight-line code with GOTOs

In the situation of merge on a state that hasn't been traversed (with a false guard) try and move the names into the destination state instead of a merge or copy operation.

Author: JohnDumbell

src/goto-symex/goto_symex_state.h

@@ -73,10 +73,29 @@ class goto_statet
   unsigned remaining_vccs = 0;
 
   /// Constructors
+  goto_statet() = default;
+  goto_statet &operator=(const goto_statet &other) = default;
+  goto_statet &operator=(goto_statet &&other) = default;
+  goto_statet(const goto_statet &other) = default;
+
   explicit goto_statet(const class goto_symex_statet &s);
   explicit goto_statet(const symex_targett::sourcet &_source) : source(_source)
   {
   }
+
+  goto_statet(goto_statet &&other) :
+    depth(other.depth),
+    level2(other.level2),
+    value_set(std::move(other.value_set)),
+    guard(std::move(other.guard)),
+    source(std::move(other.source)),
+    propagation(std::move(other.propagation)),
+    atomic_section_id(other.atomic_section_id),
+    safe_pointers(other.safe_pointers),
+    total_vccs(other.total_vccs),
+    remaining_vccs(other.remaining_vccs)
+  {
+  }
 };
 
 // stack frames -- these are used for function calls and

src/goto-symex/symex_goto.cpp

@@ -155,6 +155,13 @@ void goto_symext::symex_goto(statet &state)
     state_pc=goto_target;
   }
 
+  // Before any storing or splitting we need to copy the current state of
+  // level 2 names, as no matter which symex strategy we use .
+  symex_level2t::current_namest names = *state.level2.current_names;
+  state.level2.local_generations = state.level2.local_generations
+                                   ? *state.level2.local_generations
+                                   : names;
+
   // Normally the next instruction to execute would be state_pc and we save
   // new_state_pc for later. But if we're executing from a saved state, then
   // new_state_pc should be the state that we saved from earlier, so let's
@@ -201,6 +208,13 @@ void goto_symext::symex_goto(statet &state)
     // pointing to; this needs to be inverted for the branch that we're saving,
     // so let its truth value for `backwards` be the same as ours for `forward`.
 
+    jump_target.state.level2.current_names = new symex_level2t::current_namest(
+      *jump_target.state.level2.current_names);
+
+    jump_target.state.level2.local_generations =
+      state.level2.local_generations ? *state.level2.local_generations
+                                     : *jump_target.state.level2.current_names;
+
     log.debug() << "Saving next instruction '"
                 << next_instruction.state.saved_target->source_location << "'"
                 << log.eom;
@@ -221,7 +235,14 @@ void goto_symext::symex_goto(statet &state)
   framet::goto_state_listt &goto_state_list =
     state.top().goto_state_map[new_state_pc];
 
-  goto_state_list.emplace_back(state);
+  if(new_guard.is_true())
+  {
+    goto_state_list.push_back(std::move(state));
+  }
+  else
+  {
+    goto_state_list.push_back(statet::goto_statet(state));
+  }
 
   symex_transition(state, state_pc, backward);
 
@@ -472,6 +493,14 @@ static void merge_names(
   //     initialized and therefore an invalid target.
 
   // These rules only apply to dynamic objects and locals.
+  INVARIANT(
+    !dest_state.guard.is_false(),
+    "if the destination state is currently unreachable we shouldn't be doing "
+    "a per-name merge");
+  INVARIANT(
+    !goto_state.guard.is_false(),
+    "an unreachable state should never have been queued for merging");
+
   if(dest_state.guard.is_false())
     rhs = goto_state_rhs;
   else if(goto_state.guard.is_false())
@@ -515,21 +544,29 @@ static void merge_names(
 }
 
 void goto_symext::phi_function(
-  const goto_statet &goto_state,
+  statet::goto_statet &goto_state,
   statet &dest_state)
 {
+  // If our destination is unreachable just replace with the incoming state.
+  if(dest_state.guard.is_false())
+  {
+    dest_state.level2.local_generations = std::move(goto_state.level2.local_generations);
+    dest_state.propagation = std::move(goto_state.propagation);
+    return;
+  }
+
   if(
-    goto_state.level2.current_names.empty() &&
-    dest_state.level2.current_names.empty())
+    goto_state.level2.get_current_names().empty() &&
+    dest_state.level2.get_current_names().empty())
     return;
 
   guardt diff_guard = goto_state.guard;
   // this gets the diff between the guards
   diff_guard -= dest_state.guard;
 
   for_each2(
-    goto_state.level2.current_names,
-    dest_state.level2.current_names,
+    goto_state.level2.get_current_names(),
+    dest_state.level2.get_current_names(),
     [&](const ssa_exprt &ssa, unsigned goto_count, unsigned dest_count) {
       merge_names(
         goto_state,

src/goto-symex/symex_target.h

@@ -53,6 +53,17 @@ class symex_targett
         pc(_goto_program.instructions.begin())
     {
     }
+
+    sourcet(sourcet &&other) noexcept
+      : thread_nr(other.thread_nr),
+        function_id(other.function_id),
+        pc(other.pc)
+    {
+    }
+
+    sourcet(const sourcet &other) = default;
+    sourcet &operator=(const sourcet &other) = default;
+    sourcet &operator=(sourcet &&other) = default;
   };
 
   enum class assignment_typet

src/pointer-analysis/value_set.h

@@ -45,6 +45,17 @@ class value_sett
   {
   }
 
+  value_sett(value_sett &&other) :
+    location_number(other.location_number),
+    values(std::move(other.values))
+  {
+  }
+
+  value_sett(const value_sett &other) = default;
+
+  value_sett &operator=(const value_sett &other) = default;
+  value_sett &operator=(value_sett &&other) = default;
+
   virtual ~value_sett() = default;
 
   static bool field_sensitive(const irep_idt &id, const typet &type);