Merge pull request #395 from smowton/call_destructors_on_goto_out_of_scope

Call destructors on goto out of scope

Author: Daniel Kroening

regression/cbmc-java/destructor1/Break.class

@@ -0,0 +1,14 @@
+
+public class Break {
+
+  public static void main() {
+
+    int j = 0;
+    ++j;
+    for(int i = 0; i < 10; ++i)
+      if(i == 5) break;
+    for(j = 0; j < 10; ++j)
+      if(j == 5) break;
+  }
+
+}

regression/cbmc-java/destructor1/Break.java

@@ -0,0 +1,8 @@
+CORE
+Break.class
+--show-goto-functions
+^EXIT=0$
+^SIGNAL=0$
+dead i;
+--
+GOTO 10

regression/cbmc-java/destructor1/test.desc

@@ -57,11 +57,11 @@ Function: goto_convertt::finish_gotos
 
 \*******************************************************************/
 
-void goto_convertt::finish_gotos()
+void goto_convertt::finish_gotos(goto_programt &dest)
 {
   for(const auto &g_it : targets.gotos)
   {
-    goto_programt::instructiont &i=*g_it;
+    goto_programt::instructiont &i=*(g_it.first);
 
     if(i.code.get_statement()=="non-deterministic-goto")
     {
@@ -81,7 +81,7 @@ void goto_convertt::finish_gotos()
           throw 0;
         }
 
-        i.targets.push_back(l_it->second);
+        i.targets.push_back(l_it->second.first);
       }
     }
     else if(i.is_start_thread())
@@ -98,7 +98,7 @@ void goto_convertt::finish_gotos()
         throw 0;
       }
 
-      i.targets.push_back(l_it->second);
+      i.targets.push_back(l_it->second.first);
     }
     else if(i.code.get_statement()==ID_goto)
     {
@@ -114,7 +114,49 @@ void goto_convertt::finish_gotos()
       }
 
       i.targets.clear();
-      i.targets.push_back(l_it->second);
+      i.targets.push_back(l_it->second.first);
+
+      // If the goto recorded a destructor stack, execute as much as is
+      // appropriate for however many automatic variables leave scope.
+      // We don't currently handle variables *entering* scope, which is illegal
+      // for C++ non-pod types and impossible in Java in any case.
+      auto goto_stack=g_it.second;
+      const auto& label_stack=l_it->second.second;
+      bool stack_is_prefix=true;
+      if(label_stack.size()>goto_stack.size())
+        stack_is_prefix=false;
+      for(unsigned i=0, ilim=label_stack.size();
+          i!=ilim && stack_is_prefix;
+          ++i)
+      {
+        if(goto_stack[i]!=label_stack[i])
+          stack_is_prefix=false;
+      }
+
+      if(!stack_is_prefix)
+      {
+        warning() << "Encountered goto (" << goto_label <<
+          ") that enters one or more lexical blocks;" <<
+          "omitting constructors and destructors." << eom;
+      }
+      else
+      {
+        auto unwind_to_size=label_stack.size();
+        if(unwind_to_size<goto_stack.size())
+        {
+          status() << "Adding goto-destructor code on jump to " <<
+            goto_label << eom;
+          goto_programt destructor_code;
+          unwind_destructor_stack(
+            i.code.add_source_location(),
+            unwind_to_size,
+            destructor_code,
+            goto_stack);
+          dest.destructive_insert(g_it.first, destructor_code);
+          // This should leave iterators intact, as long as
+          // goto_programt::instructionst is std::list.
+        }
+      }
     }
     else
     {
@@ -169,7 +211,7 @@ void goto_convertt::finish_computed_gotos(goto_programt &goto_program)
       goto_programt::targett t=
         goto_program.insert_after(g_it);
 
-      t->make_goto(label.second);
+      t->make_goto(label.second.first);
       t->source_location=i.source_location;
       t->guard=guard;
     }
@@ -180,6 +222,50 @@ void goto_convertt::finish_computed_gotos(goto_programt &goto_program)
 
 /*******************************************************************\
 
+Function: goto_convertt::finish_guarded_gotos
+
+  Inputs: Destination goto program
+
+ Outputs:
+
+ Purpose: For each if(x) goto z; goto y; z: emitted,
+          see if any destructor statements were inserted
+          between goto z and z, and if not, simplify into
+          if(!x) goto y;
+
+\*******************************************************************/
+
+void goto_convertt::finish_guarded_gotos(goto_programt &dest)
+{
+  for(auto& gg : guarded_gotos)
+  {
+    // Check if any destructor code has been inserted:
+    bool destructor_present=false;
+    for(auto it=gg.ifiter;
+        it!=gg.gotoiter && !destructor_present;
+        ++it)
+    {
+      if(!(it->is_goto() || it->is_skip()))
+        destructor_present=true;
+    }
+
+    // If so, can't simplify.
+    if(destructor_present)
+      continue;
+
+    // Simplify: remove whatever code was generated for the condition
+    // and attach the original guard to the goto instruction.
+    gg.gotoiter->guard=gg.guard;
+    // goto_programt doesn't provide an erase operation,
+    // perhaps for a good reason, so let's be cautious and just
+    // flatten the un-needed instructions into skips.
+    for(auto it=gg.ifiter, itend=gg.gotoiter; it!=itend; ++it)
+      it->make_skip();
+  }
+}
+
+/*******************************************************************\
+
 Function: goto_convertt::goto_convert
 
   Inputs:
@@ -213,8 +299,9 @@ void goto_convertt::goto_convert_rec(
 {
   convert(code, dest);
 
-  finish_gotos();
+  finish_gotos(dest);
   finish_computed_gotos(dest);
+  finish_guarded_gotos(dest);
 }
 
 /*******************************************************************\
@@ -282,8 +369,7 @@ void goto_convertt::convert_label(
   goto_programt::targett target=tmp.instructions.begin();
   dest.destructive_append(tmp);
 
-  targets.labels.insert(std::pair<irep_idt, goto_programt::targett>
-                        (label, target));
+  targets.labels.insert({label, {target, targets.destructor_stack}});
   target->labels.push_front(label);
 }
 
@@ -1628,7 +1714,7 @@ void goto_convertt::convert_goto(
   t->code=code;
 
   // remember it to do target later
-  targets.gotos.push_back(t);
+  targets.gotos.push_back(std::make_pair(t,targets.destructor_stack));
 }
 
 /*******************************************************************\
@@ -2130,6 +2216,24 @@ void goto_convertt::collect_operands(
 
 /*******************************************************************\
 
+Function: is_size_one
+
+  Inputs: Goto program 'g'
+
+ Outputs: True if 'g' has one instruction
+
+ Purpose: This is (believed to be) faster than using std::list.size
+
+\*******************************************************************/
+
+static inline bool is_size_one(const goto_programt &g)
+{
+  return (!g.instructions.empty()) &&
+    ++g.instructions.begin()==g.instructions.end();
+}
+
+/*******************************************************************\
+
 Function: goto_convertt::generate_ifthenelse
 
   Inputs:
@@ -2161,24 +2265,24 @@ void goto_convertt::generate_ifthenelse(
     return;
   }
 
+  bool is_guarded_goto=false;
+
   // do guarded gotos directly
   if(is_empty(false_case) &&
-     // true_case.instructions.size()==1 optimised
-     !true_case.instructions.empty() &&
-     ++true_case.instructions.begin()==true_case.instructions.end() &&
+     is_size_one(true_case) &&
      true_case.instructions.back().is_goto() &&
      true_case.instructions.back().guard.is_true() &&
      true_case.instructions.back().labels.empty())
   {
     // The above conjunction deliberately excludes the instance
     // if(some) { label: goto somewhere; }
-    true_case.instructions.back().guard=guard;
-    dest.destructive_append(true_case);
-    return;
+    // Don't perform the transformation here, as code might get inserted into
+    // the true case to perform destructors. This will be attempted in finish_guarded_gotos.
+    is_guarded_goto=true;
   }
 
   // similarly, do guarded assertions directly
-  if(true_case.instructions.size()==1 &&
+  if(is_size_one(true_case) &&
      true_case.instructions.back().is_assert() &&
      true_case.instructions.back().guard.is_false() &&
      true_case.instructions.back().labels.empty())
@@ -2191,7 +2295,7 @@ void goto_convertt::generate_ifthenelse(
   }
 
   // similarly, do guarded assertions directly
-  if(false_case.instructions.size()==1 &&
+  if(is_size_one(false_case) &&
      false_case.instructions.back().is_assert() &&
      false_case.instructions.back().guard.is_false() &&
      false_case.instructions.back().labels.empty())
@@ -2258,6 +2362,15 @@ void goto_convertt::generate_ifthenelse(
   assert(!tmp_w.instructions.empty());
   x->source_location=tmp_w.instructions.back().source_location;
 
+  // See if we can simplify this guarded goto later.
+  // Note this depends on the fact that `instructions` is a std::list
+  // and so goto-program-destructive-append preserves iterator validity.
+  if(is_guarded_goto)
+    guarded_gotos.push_back({
+      tmp_v.instructions.begin(),
+      tmp_w.instructions.begin(),
+      guard});
+
   dest.destructive_append(tmp_v);
   dest.destructive_append(tmp_w);
 

src/goto-programs/goto_convert.cpp

@@ -216,22 +216,29 @@ class goto_convertt:public messaget
   // exceptions
   //
 
+  typedef std::vector<codet> destructor_stackt;
+
   symbol_exprt exception_flag();
   void unwind_destructor_stack(
     const source_locationt &,
     std::size_t stack_size,
     goto_programt &dest);
+  void unwind_destructor_stack(
+    const source_locationt &,
+    std::size_t stack_size,
+    goto_programt &dest,
+    destructor_stackt &stack);
 
   //
   // gotos
   //
 
-  void finish_gotos();
+  void finish_gotos(goto_programt &dest);
   void finish_computed_gotos(goto_programt &dest);
+  void finish_guarded_gotos(goto_programt &dest);
 
-  typedef std::vector<codet> destructor_stackt;
-  typedef std::map<irep_idt, goto_programt::targett> labelst;
-  typedef std::list<goto_programt::targett> gotost;
+  typedef std::map<irep_idt, std::pair<goto_programt::targett, destructor_stackt> > labelst;
+  typedef std::list<std::pair<goto_programt::targett, destructor_stackt> > gotost;
   typedef std::list<goto_programt::targett> computed_gotost;
   typedef exprt::operandst caset;
   typedef std::list<std::pair<goto_programt::targett, caset> > casest;
@@ -412,6 +419,14 @@ class goto_convertt:public messaget
     std::size_t leave_stack_size;
   };
 
+  struct guarded_gotot {
+    goto_programt::targett ifiter;
+    goto_programt::targett gotoiter;
+    exprt guard;
+  };
+  typedef std::list<guarded_gotot> guarded_gotost;
+  guarded_gotost guarded_gotos;
+
   exprt case_guard(
     const exprt &value,
     const caset &case_op);

src/goto-programs/goto_convert_class.h

@@ -374,23 +374,36 @@ void goto_convertt::unwind_destructor_stack(
   const source_locationt &source_location,
   std::size_t final_stack_size,
   goto_programt &dest)
+{
+  unwind_destructor_stack(
+    source_location,
+    final_stack_size,
+    dest,
+    targets.destructor_stack);
+}
+
+void goto_convertt::unwind_destructor_stack(
+  const source_locationt &source_location,
+  std::size_t final_stack_size,
+  goto_programt &dest,
+  destructor_stackt &destructor_stack)
 {
   // There might be exceptions happening in the exception
   // handler. We thus pop off the stack, and then later
   // one restore the original stack.
-  destructor_stackt old_stack=targets.destructor_stack;
+  destructor_stackt old_stack=destructor_stack;
 
-  while(targets.destructor_stack.size()>final_stack_size)
+  while(destructor_stack.size()>final_stack_size)
   {
-    codet d_code=targets.destructor_stack.back();
+    codet d_code=destructor_stack.back();
     d_code.add_source_location()=source_location;
 
     // pop now to avoid doing this again
-    targets.destructor_stack.pop_back();
+    destructor_stack.pop_back();
 
     convert(d_code, dest);
   }
 
   // Now restore old stack.
-  old_stack.swap(targets.destructor_stack);
+  old_stack.swap(destructor_stack);
 }