Rewrite do_exception_handling

Make the control-flow in the code understandable
Fix bugs caused by handlers in the exception table not being sorted so that ones that start and end at the same positions are all next to each other

Author: NathanJPhillips

jbmc/regression/jbmc/exceptions28/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 test.class
 --unwind 10
 ^\[java::test.main:\(\[Ljava/lang/String;\)V\.1\] line 7 no uncaught exception: FAILURE$

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -2335,105 +2335,78 @@ codet &java_bytecode_convert_methodt::do_exception_handling(
   const java_bytecode_convert_methodt::methodt &method,
   const std::set<method_offsett> &working_set,
   method_offsett cur_pc,
-  codet &c)
+  codet &code)
 {
-  std::vector<irep_idt> exception_ids;
-  std::vector<irep_idt> handler_labels;
-
-  // for each try-catch add a CATCH-PUSH instruction
-  // each CATCH-PUSH records a list of all the handler labels
-  // together with a list of all the exception ids
-
-  // be aware of different try-catch blocks with the same starting pc
-  method_offsett pos = 0;
-  method_offsett end_pc = 0;
-  while(pos < method.exception_table.size())
+  // For each try-catch add a CATCH-PUSH instruction
+  // Each CATCH-PUSH records a list of all the handler labels together with a
+  // list of all the exception ids
+
+  // Gather all try-catch blocks that have cur_pc as the starting pc
+  typedef std::vector<std::reference_wrapper<
+    const java_bytecode_convert_methodt::methodt::exceptiont>> exceptionst;
+  std::map<std::size_t, exceptionst> exceptions_by_end;
+  for(const java_bytecode_convert_methodt::methodt::exceptiont &exception
+    : method.exception_table)
   {
-    // check if this is the beginning of a try block
-    for(; pos < method.exception_table.size(); ++pos)
-    {
-      // unexplored try-catch?
-      if(cur_pc == method.exception_table[pos].start_pc && end_pc == 0)
-      {
-        end_pc = method.exception_table[pos].end_pc;
-      }
-
-      // currently explored try-catch?
-      if(
-        cur_pc == method.exception_table[pos].start_pc &&
-        method.exception_table[pos].end_pc == end_pc)
-      {
-        exception_ids.push_back(
-          method.exception_table[pos].catch_type.get_identifier());
-        // record the exception handler in the CATCH-PUSH
-        // instruction by generating a label corresponding to
-        // the handler's pc
-        handler_labels.push_back(
-          label(std::to_string(method.exception_table[pos].handler_pc)));
-      }
-      else
-        break;
-    }
-
-    // add the actual PUSH-CATCH instruction
-    if(!exception_ids.empty())
-    {
-      code_push_catcht catch_push;
-      INVARIANT(
-        exception_ids.size() == handler_labels.size(),
-        "Exception tags and handler labels should be 1-to-1");
-      code_push_catcht::exception_listt &exception_list =
-        catch_push.exception_list();
-      for(size_t i = 0; i < exception_ids.size(); ++i)
-      {
-        exception_list.push_back(
-          code_push_catcht::exception_list_entryt(
-            exception_ids[i], handler_labels[i]));
-      }
-
-      c = code_blockt({catch_push, c});
-    }
-    else
-    {
-      // advance
-      ++pos;
-    }
-
-    // reset
-    end_pc = 0;
-    exception_ids.clear();
-    handler_labels.clear();
+    if(exception.start_pc == cur_pc)
+      exceptions_by_end[exception.end_pc].push_back(exception);
+  }
+  for(const auto &exceptions : exceptions_by_end)
+  {
+    code_push_catcht catch_push;
+    code_push_catcht::exception_listt &exception_list =
+      catch_push.exception_list();
+    for(const java_bytecode_convert_methodt::methodt::exceptiont &exception
+      : exceptions.second)
+    {
+      exception_list.emplace_back(
+        exception.catch_type.get_identifier(),
+        // Record the exception handler in the CATCH-PUSH instruction by
+        // generating a label corresponding to the handler's pc
+        label(std::to_string(exception.handler_pc)));
+    }
+    // Prepend the CATCH-PUSH instruction
+    code = code_blockt({ catch_push, code });
   }
 
-  // next add the CATCH-POP instructions
-  size_t start_pc = 0;
-  // as the first try block may have start_pc 0, we
-  // must track it separately
-  bool first_handler = false;
-  // check if this is the end of a try block
+  // Next add the CATCH-POP instructions
+  // exception_row.end_pc is exclusive so append CATCH-POP instructions if this
+  // is the instruction before it.
+  // Dangerously, we assume that the lexically next bit of code after the try
+  // block (the catch block) is:
+  // a) the next code in the bytecode and therefore its start address matches
+  // the exclusive end position of the try block (probably a valid assumption
+  // for non-obfuscated bytecode generated by most compilers)
+  // b) the successor of a previous instruction and therefore in the working
+  // set (not a valid assumption when there aren't any throwing statements in
+  // the try block)
+  // We are therefore going to find all exception handlers that end at our
+  // earliest successor
+  if(working_set.empty())
+  {
+    // There was no throw in the try block
+    // TODO: This will result in non-balanced PUSH and POPs
+    return code;
+  }
+  const method_offsett &working_set_elt = *working_set.begin();
+  if(cur_pc >= working_set_elt)
+  {
+    // This just fails if we have a back-edge here
+    // TODO: This will result in non-balanced PUSH and POPs
+    return code;
+  }
+  // Count the distinct handler start positions that end at this location
+  std::set<std::size_t> start_positions;
   for(const auto &exception_row : method.exception_table)
   {
-    // add the CATCH-POP before the end of the try block
-    if(
-      cur_pc < exception_row.end_pc && !working_set.empty() &&
-      *working_set.begin() == exception_row.end_pc)
-    {
-      // have we already added a CATCH-POP for the current try-catch?
-      // (each row corresponds to a handler)
-      if(exception_row.start_pc != start_pc || !first_handler)
-      {
-        if(!first_handler)
-          first_handler = true;
-        // remember the beginning of the try-catch so that we don't add
-        // another CATCH-POP for the same try-catch
-        start_pc = exception_row.start_pc;
-        // add CATCH_POP instruction
-        code_pop_catcht catch_pop;
-        c = code_blockt({c, catch_pop});
-      }
-    }
+    // Check if working_set_elt is the end of a try block
+    if(working_set_elt == exception_row.end_pc)
+      start_positions.insert(exception_row.start_pc);
   }
-  return c;
+  for(std::size_t handler = 0; handler < start_positions.size(); ++handler)
+    // Append a CATCH-POP instruction before the end of the try block
+    code = code_blockt({ code, code_pop_catcht() });
+  return code;
 }
 
 code_blockt java_bytecode_convert_methodt::convert_multianewarray(