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.cpp

@@ -495,7 +495,8 @@ bool goto_symex_statet::l2_thread_read_encoding(
 
 /// Allocates a fresh L2 name for the given L1 identifier, and makes it the
 /// latest generation on this path.
-void goto_symex_statet::increase_generation(
+/// \return the newly allocated generation number
+std::size_t goto_symex_statet::increase_generation(
   const irep_idt l1_identifier,
   const ssa_exprt &lhs)
 {
@@ -504,6 +505,8 @@ void goto_symex_statet::increase_generation(
 
   current_emplace_res.first->second.second =
     fresh_l2_name_provider(l1_identifier);
+
+  return current_emplace_res.first->second.second;
 }
 
 /// Allocates a fresh L2 name for the given L1 identifier, and makes it the

src/goto-symex/goto_symex_state.h

@@ -207,7 +207,8 @@ class goto_symex_statet final : public goto_statet
 
   /// Allocates a fresh L2 name for the given L1 identifier, and makes it the
   //  latest generation on this path.
-  void increase_generation(const irep_idt l1_identifier, const ssa_exprt &lhs);
+  std::size_t
+  increase_generation(const irep_idt l1_identifier, const ssa_exprt &lhs);
 
   /// Increases the generation of the L1 identifier. Does nothing if there
   /// isn't an expression keyed by it.

src/goto-symex/symex_dead.cpp

@@ -43,7 +43,6 @@ void goto_symext::symex_dead(statet &state)
   // map is safe as 1) it is local to a path and 2) this instance can no longer
   // appear
   state.propagation.erase(l1_identifier);
-
   // increment the L2 index to ensure a merge on join points will propagate the
   // value for branches that are still live
   state.increase_generation_if_exists(l1_identifier);

src/goto-symex/symex_decl.cpp

@@ -66,10 +66,8 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
   }
 
   // L2 renaming
-  bool is_new =
-    state.level2.current_names.emplace(l1_identifier, std::make_pair(ssa, 1))
-      .second;
-  CHECK_RETURN(is_new);
+  std::size_t generation = state.increase_generation(l1_identifier, ssa);
+  CHECK_RETURN(generation == 1);
 
   const bool record_events=state.record_events;
   state.record_events=false;

src/goto-symex/symex_goto.cpp

@@ -210,7 +210,17 @@ void goto_symext::symex_goto(statet &state)
   // merge_gotos when we visit new_state_pc
   framet::goto_state_listt &goto_state_list =
     state.call_stack().top().goto_state_map[new_state_pc];
-  goto_state_list.emplace_back(state.source, state);
+
+  // If the guard is true (and the alternative branch unreachable) we can move
+  // the state in this case as it'll never be accessed on the alternate branch.
+  if(new_guard.is_true())
+  {
+    goto_state_list.emplace_back(state.source, std::move(state));
+  }
+  else
+  {
+    goto_state_list.emplace_back(state.source, state);
+  }
 
   symex_transition(state, state_pc, backward);
 
@@ -319,20 +329,27 @@ void goto_symext::merge_goto(
       "atomic sections differ across branches",
       state.source.pc->source_location);
 
-  // do SSA phi functions
-  phi_function(goto_state, state);
+  if(!goto_state.guard.is_false())
+  {
+    if(state.guard.is_false())
+    {
+      static_cast<goto_statet &>(state) = std::move(goto_state);
+    }
+    else
+    {
+      // do SSA phi functions
+      phi_function(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);
+      // merge value sets
+      state.value_set.make_union(goto_state.value_set);
 
-  // adjust guard
-  state.guard|=goto_state.guard;
+      // adjust guard
+      state.guard |= goto_state.guard;
 
-  // adjust depth
-  state.depth=std::min(state.depth, goto_state.depth);
+      // adjust depth
+      state.depth = std::min(state.depth, goto_state.depth);
+    }
+  }
 }
 
 /// Applies f to `(k, ssa, i, j)` if the first map maps k to (ssa, i) and