Kill let-bound variables after the current instruction completes

This avoids both wasted storage due to let-bound variables staying in the L2 renaming map,
propagator and/or value-set, and avoids generating pointless PHI-node instructions for them.

Author: smowton

src/goto-symex/goto_symex.h

@@ -219,8 +219,8 @@ class goto_symext
 
   /// \brief Called for each step in the symbolic execution
   /// This calls \ref print_symex_step to print symex's current instruction if
-  /// required, then \ref execute_instruction to execute the actual instruction
-  /// body.
+  /// required, then \ref execute_next_instruction to execute the actual
+  /// instruction body.
   /// \param get_goto_function: The delegate to retrieve function bodies (see
   ///   \ref get_goto_functiont)
   /// \param state: Symbolic execution state for current instruction
@@ -239,6 +239,11 @@ class goto_symext
     const get_goto_functiont &get_goto_function,
     statet &state);
 
+  /// Kills any variables in \ref instruction_local_symbols (these are currently
+  /// always let-bound variables defined in the course of executing the current
+  /// instruction), then clears \ref instruction_local_symbols.
+  void kill_instruction_local_symbols(statet &state);
+
   /// Prints the route of symex as it walks through the code. Used for
   /// debugging.
   void print_symex_step(statet &state);
@@ -281,6 +286,11 @@ class goto_symext
   /// instruction
   unsigned atomic_section_counter;
 
+  /// Variables that should be killed at the end of the current symex_step
+  /// invocation. Currently this is used for let-bound variables executed during
+  /// symex, whose lifetime is at most one instruction long.
+  std::vector<symbol_exprt> instruction_local_symbols;
+
   /// The messaget to write log messages to
   mutable messaget log;
 
@@ -531,8 +541,8 @@ class goto_symext
 
   /// Execute a single let expression, which should not have any nested let
   /// expressions (use \ref lift_lets instead if there might be).
-  /// The caller is responsible for killing the newly-defined variable when
-  /// appropriate.
+  /// Records the newly-defined variable in \ref instruction_local_symbols,
+  /// meaning it will be killed when \ref symex_step concludes.
   void lift_let(statet &state, const let_exprt &let_expr);
 
   void symex_assign_rec(

src/goto-symex/symex_clean_expr.cpp

@@ -186,6 +186,9 @@ void goto_symext::lift_let(statet &state, const let_exprt &let_expr)
     let_value,
     value_assignment_guard,
     symex_targett::assignment_typet::HIDDEN);
+
+  // Schedule the bound variable to be cleaned up at the end of symex_step:
+  instruction_local_symbols.push_back(let_expr.symbol());
 }
 
 void goto_symext::lift_lets(statet &state, exprt &rhs)

src/goto-symex/symex_main.cpp

@@ -513,6 +513,7 @@ void goto_symext::symex_step(
   // Print debug statements if they've been enabled.
   print_symex_step(state);
   execute_next_instruction(get_goto_function, state);
+  kill_instruction_local_symbols(state);
 }
 
 void goto_symext::execute_next_instruction(
@@ -652,6 +653,13 @@ void goto_symext::execute_next_instruction(
   }
 }
 
+void goto_symext::kill_instruction_local_symbols(statet &state)
+{
+  for(const auto &symbol_expr : instruction_local_symbols)
+    symex_dead(state, symbol_expr);
+  instruction_local_symbols.clear();
+}
+
 /// Check if an expression only contains one unique symbol (possibly repeated
 /// multiple times)
 /// \param expr: The expression to examine