GOTO conversion: create temporaries with minimal scope

GOTO conversion introduces temporaries when cleaning expression, e.g.,
removing side effects. We previously considered them to have block scope
as they only were marked dead when the block containing them was left.
This, however, can be a much larger range of instructions than for what
instructions they actually need to be live for. As a consequence, GOTO
conversion frequently deemed it necessary to introduce declaration hops
for we had goto instructions that would jump over the declaration of the
temporary, but still within the block that contained that temporary (and
well after the last actual use of that temporary).

This PR now largely (with the exception of compound literals, which
yield temporaries that must have block scope) removes the side effect
that creating temporaries had on scope tracking. Instead, methods
explicitly return the list of temporaries in need of cleanup.

This avoids performance penalties seen when trying to upgrade Kani to
CBMC version 6. Kani makes extensive use of statement expressions, which
are one case of instructions that yield a temporary that needs to be
cleaned up as soon as possible.

src/ansi-c/goto-conversion/builtin_functions.cpp

@@ -27,6 +27,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <langapi/language_util.h>
 
+#include "destructor.h"
 #include "format_strings.h"
 
 void goto_convertt::do_prob_uniform(
@@ -400,14 +401,15 @@ void goto_convertt::do_cpp_new(
   bool new_array = rhs.get(ID_statement) == ID_cpp_new_array;
 
   exprt count;
+  needs_destructiont new_vars;
 
   if(new_array)
   {
     count = typecast_exprt::conditional_cast(
       static_cast<const exprt &>(rhs.find(ID_size)), object_size.type());
 
     // might have side-effect
-    clean_expr(count, dest, ID_cpp);
+    new_vars.add(clean_expr(count, dest, ID_cpp));
   }
 
   exprt tmp_symbol_expr;
@@ -493,6 +495,10 @@ void goto_convertt::do_cpp_new(
     typecast_exprt(tmp_symbol_expr, lhs.type()),
     rhs.find_source_location()));
 
+  new_vars.minimal_scope.push_front(
+    to_symbol_expr(tmp_symbol_expr).get_identifier());
+  destruct_locals(new_vars.minimal_scope, dest, ns);
+
   // grab initializer
   goto_programt tmp_initializer;
   cpp_new_initializer(lhs, rhs, tmp_initializer);
@@ -685,6 +691,8 @@ void goto_convertt::do_havoc_slice(
 
   codet array_replace(ID_array_replace, {arg0, arg1}, source_location);
   dest.add(goto_programt::make_other(array_replace, source_location));
+
+  destruct_locals({nondet_contents.name}, dest, ns);
 }
 
 /// alloca allocates memory that is freed when leaving the function (and not the
@@ -773,6 +781,9 @@ void goto_convertt::do_alloca(
   dest.add(goto_programt::make_assignment(
     this_alloca_ptr, std::move(rhs), source_location));
 
+  if(lhs.is_nil())
+    destruct_locals({to_symbol_expr(new_lhs).get_identifier()}, dest, ns);
+
   // mark pointer to alloca result as dead, unless the alloca result (in
   // this_alloca_ptr)  is still NULL
   symbol_exprt dead_object_sym =

src/ansi-c/goto-conversion/destructor.cpp

@@ -11,10 +11,12 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "destructor.h"
 
+#include <util/c_types.h>
 #include <util/namespace.h>
 #include <util/pointer_expr.h>
+#include <util/symbol.h>
 
-#include <goto-programs/goto_instruction_code.h>
+#include <goto-programs/goto_program.h>
 
 code_function_callt get_destructor(const namespacet &ns, const typet &type)
 {
@@ -56,3 +58,33 @@ code_function_callt get_destructor(const namespacet &ns, const typet &type)
 
   return static_cast<const code_function_callt &>(get_nil_irep());
 }
+
+void destruct_locals(
+  const std::list<irep_idt> &vars,
+  goto_programt &dest,
+  const namespacet &ns)
+{
+  for(const auto &id : vars)
+  {
+    const symbolt &symbol = ns.lookup(id);
+
+    // do destructor
+    code_function_callt destructor = get_destructor(ns, symbol.type);
+
+    if(destructor.is_not_nil())
+    {
+      // add "this"
+      address_of_exprt this_expr(
+        symbol.symbol_expr(), pointer_type(symbol.type));
+      destructor.arguments().push_back(this_expr);
+
+      dest.add(goto_programt::make_function_call(
+        destructor, destructor.source_location()));
+    }
+
+    // now create a 'dead' instruction -- will be added after the
+    // destructor created below as unwind_destructor_stack pops off the
+    // top of the destructor stack
+    dest.add(goto_programt::make_dead(symbol.symbol_expr(), symbol.location));
+  }
+}

src/ansi-c/goto-conversion/destructor.h

@@ -12,10 +12,20 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_GOTO_PROGRAMS_DESTRUCTOR_H
 #define CPROVER_GOTO_PROGRAMS_DESTRUCTOR_H
 
+#include <util/irep.h>
+
+#include <list>
+
+class goto_programt;
 class namespacet;
 class typet;
 
 class code_function_callt
 get_destructor(const namespacet &ns, const typet &type);
 
+void destruct_locals(
+  const std::list<irep_idt> &vars,
+  goto_programt &dest,
+  const namespacet &ns);
+
 #endif // CPROVER_GOTO_PROGRAMS_DESTRUCTOR_H