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

@@ -494,7 +494,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)
 {
@@ -503,6 +504,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

@@ -205,7 +205,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);
+
+  // 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);
+  }
+  else
+  {
+    goto_state_list.emplace_back(state);
+  }
 
   symex_transition(state, state_pc, backward);
 
@@ -314,14 +324,23 @@ void goto_symext::merge_goto(goto_statet &&goto_state, statet &state)
       "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())
+    {
+      state.level2 = std::move(goto_state.level2);
+      state.propagation = std::move(goto_state.propagation);
+      state.value_set = std::move(goto_state.value_set);
+    }
+    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;