Track and kill let-bound variables when their statement is executed

This is done using the owner class symex_live_let_variablest, which is passed down
by utility functions to those such as symex_assign that are responsible for executing
a whole instruction. When the instruction execution is complete (i.e. all VCCs attributable
to it, and which can refer to the let-bound variable, are emitted) the instance is allowed
to die, and it in turn kills the now-unneeded binders.

Author: smowton

src/goto-symex/goto_symex.h

@@ -18,6 +18,7 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/abstract_goto_model.h>
 
 #include "path_storage.h"
+#include "symex_live_let_variables.h"
 
 class byte_extract_exprt;
 class typet;
@@ -273,11 +274,11 @@ class goto_symext
   /// \param expr: The expression to clean up
   /// \param state
   /// \param write
-  void clean_expr(exprt &expr, statet &state, bool write);
+  symex_live_let_variablest clean_expr(exprt &expr, statet &state, bool write);
 
   void trigger_auto_object(const exprt &, statet &);
   void initialize_auto_object(const exprt &, statet &);
-  void process_array_expr(statet &, exprt &);
+  symex_live_let_variablest process_array_expr(statet &, exprt &);
   exprt make_auto_object(const typet &, statet &);
   virtual void dereference(exprt &, statet &, bool write);
 
@@ -496,7 +497,7 @@ class goto_symext
 
   typedef symex_targett::assignment_typet assignment_typet;
 
-  void lift_lets(statet &, exprt &, assignment_typet);
+  symex_live_let_variablest lift_lets(statet &, exprt &);
   void lift_let(statet &state, const let_exprt &let_expr);
 
   void symex_assign_rec(
@@ -579,7 +580,7 @@ class goto_symext
   /// \param state: Symbolic execution state for current instruction
   /// \param lhs: The expression to assign to
   /// \param code: The `new` expression
-  virtual void
+  virtual symex_live_let_variablest
   symex_cpp_new(statet &state, const exprt &lhs, const side_effect_exprt &code);
   /// Symbolically execute a FUNCTION_CALL instruction for a function whose
   /// name starts with CPROVER_FKT_PREFIX
@@ -667,6 +668,8 @@ class goto_symext
   {
     target.validate(ns, vm);
   }
+
+  friend class symex_live_let_variablest;
 };
 
 /// Transition to the next instruction, which increments the internal program

src/goto-symex/symex_assign.cpp

@@ -33,8 +33,10 @@ void goto_symext::symex_assign(statet &state, const code_assignt &code)
   DATA_INVARIANT(
     lhs.type() == rhs.type(), "assignments must be type consistent");
 
-  clean_expr(lhs, state, true);
-  clean_expr(rhs, state, false);
+  // These let-variables containers kill the bound variables when they are
+  // destroyed (i.e. at the end of symex_assign)
+  auto live_let_variables = clean_expr(lhs, state, true);
+  live_let_variables.add(clean_expr(rhs, state, false));
 
   if(rhs.id()==ID_side_effect)
   {
@@ -44,7 +46,7 @@ void goto_symext::symex_assign(statet &state, const code_assignt &code)
     if(
       statement == ID_cpp_new || statement == ID_cpp_new_array ||
       statement == ID_java_new_array_data)
-      symex_cpp_new(state, lhs, side_effect_expr);
+      live_let_variables.add(symex_cpp_new(state, lhs, side_effect_expr));
     else if(statement==ID_allocate)
       symex_allocate(state, lhs, side_effect_expr);
     else if(statement==ID_printf)

src/goto-symex/symex_builtin_functions.cpp

@@ -378,7 +378,7 @@ void goto_symext::symex_output(
 /// \param state: Symex state
 /// \param lhs: left-hand side of assignment
 /// \param code: right-hand side containing side effect
-void goto_symext::symex_cpp_new(
+symex_live_let_variablest goto_symext::symex_cpp_new(
   statet &state,
   const exprt &lhs,
   const side_effect_exprt &code)
@@ -412,10 +412,11 @@ void goto_symext::symex_cpp_new(
   else
     INVARIANT_WITH_IREP(false, "Unexpected side effect expression", code);
 
+  symex_live_let_variablest live_let_variables(*this, state);
   if(do_array)
   {
     exprt size_arg = static_cast<const exprt &>(code.find(ID_size));
-    clean_expr(size_arg, state, false);
+    live_let_variables.add(clean_expr(size_arg, state, false));
     symbol.type = array_typet(pointer_type.subtype(), size_arg);
   }
   else
@@ -438,6 +439,8 @@ void goto_symext::symex_cpp_new(
     rhs.copy_to_operands(symbol.symbol_expr());
 
   symex_assign(state, code_assignt(lhs, rhs));
+
+  return live_let_variables;
 }
 
 void goto_symext::symex_cpp_delete(

src/goto-symex/symex_clean_expr.cpp

@@ -120,17 +120,20 @@ process_array_expr(exprt &expr, bool do_simplify, const namespacet &ns)
   }
 }
 
-void goto_symext::process_array_expr(statet &state, exprt &expr)
+symex_live_let_variablest goto_symext::process_array_expr(
+  statet &state, exprt &expr)
 {
   symex_dereference_statet symex_dereference_state(state, ns);
 
   value_set_dereferencet dereference(
     ns, state.symbol_table, symex_dereference_state, language_mode, false);
 
   expr = dereference.dereference(expr);
-  lift_lets(state, expr);
+  auto live_let_variables = lift_lets(state, expr);
 
   ::process_array_expr(expr, symex_config.simplify_opt, ns);
+
+  return live_let_variables;
 }
 
 /// Rewrite index/member expressions in byte_extract to offset
@@ -174,7 +177,10 @@ replace_nondet(exprt &expr, symex_nondet_generatort &build_symex_nondet)
 void goto_symext::lift_let(statet &state, const let_exprt &let_expr)
 {
   exprt let_value = let_expr.value();
-  clean_expr(let_value, state, false);
+  auto nested_let_variables = clean_expr(let_value, state, false);
+  INVARIANT(
+    nested_let_variables.empty(),
+    "lift_let should have nested lets removed first");
   let_value = state.rename(std::move(let_value), ns).get();
   do_simplify(let_value);
 
@@ -190,38 +196,45 @@ void goto_symext::lift_let(statet &state, const let_exprt &let_expr)
 
 symex_live_let_variablest goto_symext::lift_lets(statet &state, exprt &rhs)
 {
+  symex_live_let_variablest lifted_let_variables(*this, state);
+
   for(auto it = rhs.depth_begin(), itend = rhs.depth_end(); it != itend;)
   {
     if(it->id() == ID_let)
     {
       // Visit post-order, so more-local definitions are made before usage:
       exprt &replaced_expr = it.mutate();
       let_exprt &replaced_let = to_let_expr(replaced_expr);
-      lift_lets(state, replaced_let.value());
-      lift_lets(state, replaced_let.where());
+      lifted_let_variables.add(lift_lets(state, replaced_let.value()));
+      lifted_let_variables.add(lift_lets(state, replaced_let.where()));
 
       lift_let(state, replaced_let);
+      lifted_let_variables.add(replaced_let.symbol());
       replaced_expr = replaced_let.where();
 
       it.next_sibling_or_parent();
     }
     else
       ++it;
   }
+
+  return lifted_let_variables;
 }
 
-void goto_symext::clean_expr(
+symex_live_let_variablest goto_symext::clean_expr(
   exprt &expr,
   statet &state,
   const bool write)
 {
   replace_nondet(expr, path_storage.build_symex_nondet);
   dereference(expr, state, write);
-  lift_lets(state, expr);
+  auto live_let_variables = lift_lets(state, expr);
 
   // make sure all remaining byte extract operations use the root
   // object to avoid nesting of with/update and byte_update when on
   // lhs
   if(write)
     adjust_byte_extract_rec(expr, ns);
+
+  return live_let_variables;
 }

src/goto-symex/symex_function_call.cpp

@@ -132,8 +132,8 @@ void goto_symext::parameter_assignments(
         assignment_type =
           symex_targett::assignment_typet::VISIBLE_ACTUAL_PARAMETER;
 
-      clean_expr(lhs, state, true);
-      clean_expr(rhs, state, false);
+      auto lhs_let_variables = clean_expr(lhs, state, true);
+      auto rhs_let_variables = clean_expr(rhs, state, false);
 
       exprt::operandst lhs_conditions;
       symex_assign_rec(
@@ -200,13 +200,14 @@ void goto_symext::symex_function_call_symbol(
 {
   code_function_callt code = original_code;
 
+  symex_live_let_variablest live_let_variables(*this, state);
   if(code.lhs().is_not_nil())
-    clean_expr(code.lhs(), state, true);
+    live_let_variables.add(clean_expr(code.lhs(), state, true));
 
-  clean_expr(code.function(), state, false);
+  live_let_variables.add(clean_expr(code.function(), state, false));
 
   Forall_expr(it, code.arguments())
-    clean_expr(*it, state, false);
+    live_let_variables.add(clean_expr(*it, state, false));
 
   target.location(state.guard.as_expr(), state.source);
 

src/goto-symex/symex_goto.cpp

@@ -70,7 +70,7 @@ void goto_symext::symex_goto(statet &state)
   const goto_programt::instructiont &instruction=*state.source.pc;
 
   exprt new_guard = instruction.get_condition();
-  clean_expr(new_guard, state, false);
+  auto live_let_variables = clean_expr(new_guard, state, false);
 
   renamedt<exprt, L2> renamed_guard = state.rename(std::move(new_guard), ns);
   if(symex_config.simplify_opt)

src/goto-symex/symex_live_let_variables.cpp

@@ -0,0 +1,19 @@
+/*******************************************************************\
+
+Module: Container for live let-bound variables used by goto-symex
+
+Author: Diffblue Ltd.
+
+\*******************************************************************/
+
+/// \file
+/// Container for live let-bound variables used by goto-symex
+
+#include "goto_symex.h"
+#include "symex_live_let_variables.h"
+
+symex_live_let_variablest::~symex_live_let_variablest()
+{
+  for(const auto &symbol_expr : live_let_variables)
+    symex.symex_dead(state, symbol_expr);
+}

src/goto-symex/symex_live_let_variables.h

@@ -0,0 +1,63 @@
+/*******************************************************************\
+
+Module: Container for live let-bound variables used by goto-symex
+
+Author: Diffblue Ltd.
+
+\*******************************************************************/
+
+/// \file
+/// Container for live let-bound variables used by goto-symex
+
+#ifndef CPROVER_GOTO_SYMEX_SYMEX_LIVE_LET_VARIABLES_H
+#define CPROVER_GOTO_SYMEX_SYMEX_LIVE_LET_VARIABLES_H
+
+#include <util/nodiscard.h>
+#include <util/ssa_expr.h>
+
+#include <vector>
+
+class goto_symext;
+class goto_symex_statet;
+
+/// Owner class for let-bound variables that will be killed when this instance
+/// is destroyed. Returned by clean_expr and related functions that execute let
+/// or other local definitions, and then allowed to die when all VCCs that may
+/// refer to the bound variable have been created.
+class NODISCARD symex_live_let_variablest
+{
+  std::vector<symbol_exprt> live_let_variables;
+  goto_symext &symex;
+  goto_symex_statet &state;
+
+public:
+  symex_live_let_variablest(goto_symext &symex, goto_symex_statet &state) :
+    symex(symex), state(state) { }
+  symex_live_let_variablest(const symex_live_let_variablest &) = delete;
+  symex_live_let_variablest(symex_live_let_variablest &&) = default;
+  const symex_live_let_variablest &operator=(const symex_live_let_variablest &)
+    = delete;
+  symex_live_let_variablest &operator=(symex_live_let_variablest &&) = delete;
+
+  ~symex_live_let_variablest();
+
+  void add(const symbol_exprt &symbol_expr)
+  {
+    live_let_variables.push_back(symbol_expr);
+  }
+
+  void add(symex_live_let_variablest &&other)
+  {
+    live_let_variables.insert(
+      live_let_variables.end(),
+      other.live_let_variables.begin(),
+      other.live_let_variables.end());
+    other.live_let_variables.clear();
+  }
+
+  bool empty() const {
+    return live_let_variables.empty();
+  }
+};
+
+#endif

src/goto-symex/symex_main.cpp

@@ -82,7 +82,7 @@ void goto_symext::symex_assert(
   statet &state)
 {
   exprt condition = instruction.get_condition();
-  clean_expr(condition, state, false);
+  auto live_let_variables = clean_expr(condition, state, false);
 
   // First, push negations in and perhaps convert existential quantifiers into
   // universals:
@@ -127,7 +127,7 @@ void goto_symext::symex_assume(statet &state, const exprt &cond)
 {
   exprt simplified_cond=cond;
 
-  clean_expr(simplified_cond, state, false);
+  auto live_let_variables = clean_expr(simplified_cond, state, false);
   simplified_cond = state.rename(std::move(simplified_cond), ns).get();
   do_simplify(simplified_cond);