java_enum_static_init_unwind_handler.cpp

Go to the documentation of this file.

/*******************************************************************\
 
Module: Unwind loops in static initializers
 
Author: Chris Smowton, chris.smowton@diffblue.com
 
\*******************************************************************/
 
 
#include "java_enum_static_init_unwind_handler.h"
 
#include <util/invariant.h>
#include <util/ssa_expr.h> // IWYU pragma: keep
#include <util/suffix.h>
 
#include <goto-symex/call_stack.h>
 
#include "java_utils.h"
 
static irep_idt find_enum_function_on_stack(const call_stackt &context)
{
  static irep_idt reference_array_clone_id =
    "java::array[reference].clone:()Ljava/lang/Object;";
 
  PRECONDITION(!context.empty());
  const irep_idt &current_function = context.back().function_identifier;
 
  if(context.size() >= 2 && current_function == reference_array_clone_id)
  {
    const irep_idt &clone_caller =
      context.at(context.size() - 2).function_identifier;
    if(id2string(clone_caller).find(".values:()[L") != std::string::npos)
      return clone_caller;
    else
      return irep_idt();
  }
  else if(has_suffix(id2string(current_function), ".<clinit>:()V"))
    return current_function;
  else
    return irep_idt();
}
static irep_idt find_enum_function_on_stack(const call_stackt &context) {…}
 
tvt java_enum_static_init_unwind_handler(
  const call_stackt &context,
  unsigned loop_number,
  unsigned unwind_count,
  unsigned &unwind_max,
  const symbol_tablet &symbol_table)
{
  (void)loop_number; // unused parameter
 
  const irep_idt enum_function_id = find_enum_function_on_stack(context);
  if(enum_function_id.empty())
    return tvt::unknown();
 
  const symbolt &function_symbol = symbol_table.lookup_ref(enum_function_id);
  const auto class_id = declaring_class(function_symbol);
  INVARIANT(class_id, "Java methods should have a defining class.");
 
  const typet &class_type = symbol_table.lookup_ref(*class_id).type;
  size_t unwinds = class_type.get_size_t(ID_java_enum_static_unwind);
  if(unwinds != 0 && unwind_count < unwinds)
  {
    unwind_max = unwinds;
    return tvt(false); // Must unwind
  }
  else
  {
    return tvt::unknown(); // Defer to other unwind handlers
  }
}
tvt java_enum_static_init_unwind_handler( {…}