java_static_initializers.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Java Static Initializers
 
Author: Chris Smowton, chris.smowton@diffblue.com
 
\*******************************************************************/
 
#ifndef CPROVER_JAVA_BYTECODE_JAVA_STATIC_INITIALIZERS_H
#define CPROVER_JAVA_BYTECODE_JAVA_STATIC_INITIALIZERS_H
 
#include "synthetic_methods_map.h"
 
#include <unordered_set>
 
#include <util/std_code.h>
#include <util/symbol.h>
 
#include "code_with_references.h"
 
class ci_lazy_methods_neededt;
class json_objectt;
class message_handlert;
class select_pointer_typet;
class symbol_table_baset;
class symbol_tablet;
struct java_object_factory_parameterst;
 
irep_idt clinit_wrapper_name(const irep_idt &class_name);
irep_idt user_specified_clinit_name(const irep_idt &class_name);
 
bool is_clinit_wrapper_function(const irep_idt &function_id);
bool is_clinit_function(const irep_idt &function_id);
bool is_user_specified_clinit_function(const irep_idt &function_id);
 
void create_static_initializer_symbols(
  symbol_tablet &symbol_table,
  synthetic_methods_mapt &synthetic_methods,
  const bool thread_safe,
  const bool is_user_clinit_needed);
 
code_blockt get_thread_safe_clinit_wrapper_body(
  const irep_idt &function_id,
  symbol_table_baset &symbol_table,
  const bool nondet_static,
  const bool replace_clinit,
  const java_object_factory_parameterst &object_factory_parameters,
  const select_pointer_typet &pointer_type_selector,
  message_handlert &message_handler);
 
code_ifthenelset get_clinit_wrapper_body(
  const irep_idt &function_id,
  symbol_table_baset &symbol_table,
  const bool nondet_static,
  const bool replace_clinit,
  const java_object_factory_parameterst &object_factory_parameters,
  const select_pointer_typet &pointer_type_selector,
  message_handlert &message_handler);
 
std::unordered_multimap<irep_idt, symbolt>
class_to_declared_symbols(const symbol_tablet &symbol_table);
 
code_blockt get_user_specified_clinit_body(
  const irep_idt &class_id,
  const json_objectt &static_values_json,
  symbol_table_baset &symbol_table,
  optionalt<ci_lazy_methods_neededt> needed_lazy_methods,
  size_t max_user_array_length,
  std::unordered_map<std::string, object_creation_referencet> &references,
  const std::unordered_multimap<irep_idt, symbolt>
    &class_to_declared_symbols_map);
 
class stub_global_initializer_factoryt
{
  typedef std::unordered_multimap<irep_idt, irep_idt> stub_globals_by_classt;
  stub_globals_by_classt stub_globals_by_class;
 
public:
  void create_stub_global_initializer_symbols(
    symbol_tablet &symbol_table,
    const std::unordered_set<irep_idt> &stub_globals_set,
    synthetic_methods_mapt &synthetic_methods);
 
  code_blockt get_stub_initializer_body(
    const irep_idt &function_id,
    symbol_table_baset &symbol_table,
    const java_object_factory_parameterst &object_factory_parameters,
    const select_pointer_typet &pointer_type_selector,
    message_handlert &message_handler);
};
 
void create_stub_global_initializers(
  symbol_tablet &symbol_table,
  const std::unordered_set<irep_idt> &stub_globals_set,
  const java_object_factory_parameterst &object_factory_parameters,
  const select_pointer_typet &pointer_type_selector);
 
#endif