java_bytecode_language.h

Go to the documentation of this file.

/*******************************************************************\
 
Module:
 
Author: Daniel Kroening, kroening@kroening.com
 
\*******************************************************************/
 
 
#ifndef CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_LANGUAGE_H
#define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_LANGUAGE_H
 
#include <util/json.h>
#include <util/prefix_filter.h>
#include <util/symbol.h> // IWYU pragma: keep
 
#include <langapi/language.h>
 
#include "ci_lazy_methods.h"
#include "ci_lazy_methods_needed.h"
#include "code_with_references.h" // IWYU pragma: keep
#include "java_class_loader.h"
#include "java_object_factory_parameters.h"
#include "java_static_initializers.h"
#include "java_string_library_preprocess.h"
#include "select_pointer_type.h"
#include "synthetic_methods_map.h"
 
#include <memory>
 
// clang-format off
#define JAVA_BYTECODE_LANGUAGE_OPTIONS /*NOLINT*/ \
  "(disable-uncaught-exception-check)" \
  "(throw-assertion-error)" \
  "(assert-no-exceptions-thrown)" \
  "(java-assume-inputs-non-null)" \
  "(java-assume-inputs-interval):" \
  "(java-assume-inputs-integral)" \
  "(throw-runtime-exceptions)" \
  "(max-nondet-array-length):" \
  "(max-nondet-tree-depth):" \
  "(java-max-vla-length):" \
  "(java-cp-include-files):" \
  "(ignore-manifest-main-class)" \
  "(context-include):" \
  "(context-exclude):" \
  "(no-lazy-methods)" \
  "(lazy-methods-extra-entry-point):" \
  "(java-load-class):" \
  "(java-no-load-class):" \
  "(static-values):" \
  "(java-lift-clinit-calls)"
 
#define JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP \
  " {y--disable-uncaught-exception-check} \t " \
  "ignore uncaught exceptions and errors\n" \
  " {y--throw-assertion-error} \t " \
  "throw java.lang.AssertionError on violated assert statements instead of " \
  "failing at the location of the assert statement\n" \
  " {y--throw-runtime-exceptions} \t " \
  "make implicit runtime exceptions explicit\n" \
  " {y--assert-no-exceptions-thrown} \t " \
  "transform `throw` instructions into `assert FALSE` followed by " \
  "`assume FALSE`.\n" \
  " {y--max-nondet-array-length} {uN} \t " \
  "limit nondet (e.g. input) array size to <= {uN}\n" \
  " {y--max-nondet-tree-depth} {uN} \t " \
  "limit size of nondet (e.g. input) object tree; at level {uN} references " \
  "are set to null\n" \
  " {y--java-assume-inputs-non-null} \t " \
  "never initialize reference-typed parameter to the entry point with null\n" \
  " {y--java-assume-inputs-interval} {y[}{uL}{y:}{uU}|{uL}{y:}|{y:}{uU}{y]} " \
  "\t " \
  "force numerical primitive-typed inputs (byte, short, int, long, float, " \
  "double) to be initialized within the given range; lower bound {uL} and " \
  "upper bound {uU} must be integers; does not work for arrays\n" \
  " {y--java-assume-inputs-integral} \t " \
  "force float and double inputs to have integer values; does not work for " \
  "arrays\n" \
  " {y--java-max-vla-length} {uN} \t " \
  "limit the length of user-code-created arrays\n" \
  " {y--java-cp-include-files} {ur} \t " \
  "regexp or JSON list of files to load (with '@' prefix)\n" \
  " {y--java-load-class} {uCLASS} \t also load code from class {uCLASS}\n" \
  " {y--java-no-load-class} {uCLASS} \t never load code from class " \
  "{uCLASS}\n" \
  " {y--ignore-manifest-main-class} \t " \
  "ignore Main-Class entries in JAR manifest files. If this option is " \
  "specified and the options {y--function} and {y--main-class} are not, we " \
  "can be certain that all classes in the JAR file are loaded.\n" \
  " {y--context-include} {ui} \t " \
  "only analyze code matching specification {ui}\n" \
  " {y--context-exclude} {ue} \t " \
  "only analyze code does not match specification {ue}. All other methods " \
  "are excluded, i.e. we load their signatures and meta-information, but not " \
  "their bodies. A specification is any prefix of a package, class or method " \
  "name, e.g. \"org.cprover.\" or \"org.cprover.MyClass.\" or " \
  "\"org.cprover.MyClass.methodToStub:(I)Z\". These options can be given " \
  "multiple times. The default for context-include is 'all included'; " \
  "default for context-exclude is 'nothing excluded'.\n" \
  " {y--no-lazy-methods} \t " \
  "load and translate all methods given on the command line and in " \
  "{y--classpath}. Default is to load methods that appear to be reachable " \
  "from the {y--function} entry point or main class Note that " \
  "{y--show-symbol-table}, {y--show-goto-functions} and " \
  "{y--show-properties} output are restricted to loaded methods by default.\n" \
  " {y--lazy-methods-extra-entry-point} {uMETHODNAME} \t " \
  "treat {uMETHODNAME} as a possible program entry point for the purpose of " \
  "lazy method loading {uMETHODNAME} can be a regex that will be matched " \
  "against all symbols. If missing a java:: prefix will be added. If no " \
  "descriptor is found, all overloads of a method will also be added.\n" \
  " {y--static-values} {uf} \t " \
  "Load initial values of static fields from the given JSON file {uf}. We " \
  "assign static fields to these values instead of calling the normal " \
  "static initializer (clinit) method. The argument can be a relative or " \
  "absolute path to the file.\n" \
  " {y--java-lift-clinit-calls} \t " \
  "Lifts clinit calls in function bodies to the top of the function. This " \
  "may reduce the overall cost of static initialisation, but may be unsound " \
  "if there are cyclic dependencies between static initializers due to " \
  "potentially changing their order of execution, or if static initializers " \
  "have side-effects such as updating another class' static field.\n" \
 
#ifdef _WIN32
  #define JAVA_CLASSPATH_SEPARATOR ";"
#else
  #define JAVA_CLASSPATH_SEPARATOR ":"
#endif
 
#define HELP_JAVA_CLASSPATH \
  " {y-classpath} {udirs/jars}, {y-cp} {udirs/jars}, " \
  "{y--classpath} {udirs/jars} \t " \
  "set class search path of directories and jar files to a " \
  JAVA_CLASSPATH_SEPARATOR "-separated list of directories and JAR " \
  "archives to search for class files\n" \
  " {y--main-class} {uclass-name} \t set the name of the main class\n"
 
#define HELP_JAVA_METHOD_NAME \
  "  {umethod-name} \t " \
  "fully qualified name of method  used as entry point, e.g. " \
  "mypackage.Myclass.foo:(I)Z\n"
 
#define HELP_JAVA_CLASS_NAME \
  "  {uclass-name} \t " \
  "name of class. The entry point is the method specified by --function, " \
  "or otherwise, the public static void main(String[]) method of the given " \
  "class.\n"
 
#define OPT_JAVA_JAR \
  "(jar):"
 
#define HELP_JAVA_JAR \
  " {y-jar} {ujarfile} \t " \
  "JAR file to be checked. The entry point is the method specified by " \
  "{y--function} or otherwise, the public static void main(String[]) method " \
  "of the class specified by {y--main-class} or the main class specified in " \
  "the JAR manifest (checked in this order).\n"
 
#define OPT_JAVA_GOTO_BINARY \
  "(gb):"
 
#define HELP_JAVA_GOTO_BINARY \
  " {y--gb} {ugoto-binary} \t " \
  "goto-binary file to be checked. The entry point is the method specified " \
  "by {y--function}, or otherwise, the public static void main(String[]) of " \
  "the class specified by {y--main-class} (checked in this order).\n"
// clang-format on
 
enum lazy_methods_modet
{
  LAZY_METHODS_MODE_EAGER,
  LAZY_METHODS_MODE_CONTEXT_INSENSITIVE,
  LAZY_METHODS_MODE_EXTERNAL_DRIVER
};
 
class lazy_class_to_declared_symbols_mapt
{
public:
  lazy_class_to_declared_symbols_mapt() = default;
 
  std::unordered_multimap<irep_idt, symbolt> &
  get(const symbol_table_baset &symbol_table);
 
  void reinitialize();
 
private:
  bool initialized = false;
  std::unordered_multimap<irep_idt, symbolt> map;
};
 
struct java_bytecode_language_optionst
{
  java_bytecode_language_optionst(const optionst &options, message_handlert &);
 
  java_bytecode_language_optionst() = default;
 
  bool assume_inputs_non_null = false;
  bool string_refinement_enabled = false;
  bool throw_runtime_exceptions = false;
  bool assert_uncaught_exceptions = false;
  bool throw_assertion_error = false;
  bool threading_support = false;
  bool nondet_static = false;
  bool ignore_manifest_main_class = false;
 
  bool assert_no_exceptions_thrown = false;
 
  size_t max_user_array_length = 0;
  lazy_methods_modet lazy_methods_mode =
    lazy_methods_modet::LAZY_METHODS_MODE_EAGER;
 
  std::vector<irep_idt> java_load_classes;
  std::string java_cp_include_files;
  std::optional<json_objectt> static_values_json;
 
  std::unordered_set<std::string> no_load_classes;
 
  std::vector<load_extra_methodst> extra_methods;
 
  std::optional<prefix_filtert> method_context;
 
  bool should_lift_clinit_calls;
 
  std::optional<std::string> main_jar;
};
 
#define JAVA_CLASS_MODEL_SUFFIX "@class_model"
 
class java_bytecode_languaget:public languaget
{
public:
  void set_language_options(const optionst &, message_handlert &) override;
 
  virtual bool preprocess(
    std::istream &instream,
    const std::string &path,
    std::ostream &outstream,
    message_handlert &message_handler) override;
 
  // This is an extension to languaget
  // required because parsing of Java programs can be initiated without
  // opening a file first or providing a path to a file
  // as dictated by \ref languaget.
  virtual bool parse(message_handlert &);
 
  bool parse(
    std::istream &instream,
    const std::string &path,
    message_handlert &message_handler) override;
 
  bool generate_support_functions(
    symbol_table_baset &symbol_table,
    message_handlert &message_handler) override;
 
  bool typecheck(
    symbol_table_baset &context,
    const std::string &module,
    message_handlert &message_handler) override;
 
  virtual bool final(symbol_table_baset &context) override;
 
  void show_parse(std::ostream &out, message_handlert &) override;
 
  virtual ~java_bytecode_languaget();
  java_bytecode_languaget(
    std::unique_ptr<select_pointer_typet> pointer_type_selector)
    : object_factory_parameters(),
      pointer_type_selector(std::move(pointer_type_selector))
  {
  }
 
  java_bytecode_languaget():
    java_bytecode_languaget(
      std::unique_ptr<select_pointer_typet>(new select_pointer_typet()))
  {
  }
 
  bool from_expr(
    const exprt &expr,
    std::string &code,
    const namespacet &ns) override;
 
  bool from_type(
    const typet &type,
    std::string &code,
    const namespacet &ns) override;
 
  bool to_expr(
    const std::string &code,
    const std::string &module,
    exprt &expr,
    const namespacet &ns,
    message_handlert &message_handler) override;
 
  std::unique_ptr<languaget> new_language() override
  {
    return std::make_unique<java_bytecode_languaget>();
  }
 
  std::string id() const override { return "java"; }
  std::string description() const override { return "Java Bytecode"; }
  std::set<std::string> extensions() const override;
 
  void modules_provided(std::set<std::string> &modules) override;
  virtual void
  methods_provided(std::unordered_set<irep_idt> &methods) const override;
  virtual void convert_lazy_method(
    const irep_idt &function_id,
    symbol_table_baset &symbol_table,
    message_handlert &message_handler) override;
 
protected:
  void convert_single_method(
    const irep_idt &function_id,
    symbol_table_baset &symbol_table,
    lazy_class_to_declared_symbols_mapt &class_to_declared_symbols,
    message_handlert &message_handler)
  {
    convert_single_method(
      function_id,
      symbol_table,
      std::optional<ci_lazy_methods_neededt>(),
      class_to_declared_symbols,
      message_handler);
  }
  bool convert_single_method(
    const irep_idt &function_id,
    symbol_table_baset &symbol_table,
    std::optional<ci_lazy_methods_neededt> needed_lazy_methods,
    lazy_class_to_declared_symbols_mapt &class_to_declared_symbols,
    message_handlert &);
  bool convert_single_method_code(
    const irep_idt &function_id,
    symbol_table_baset &symbol_table,
    std::optional<ci_lazy_methods_neededt> needed_lazy_methods,
    lazy_class_to_declared_symbols_mapt &class_to_declared_symbols,
    message_handlert &);
 
  bool do_ci_lazy_method_conversion(symbol_table_baset &, message_handlert &);
  const select_pointer_typet &get_pointer_type_selector() const;
 
  std::optional<java_bytecode_language_optionst> language_options;
  irep_idt main_class;
  std::vector<irep_idt> main_jar_classes;
  java_class_loadert java_class_loader;
  java_object_factory_parameterst object_factory_parameters;
  method_bytecodet method_bytecode;
  java_string_library_preprocesst string_preprocess;
 
private:
  virtual std::vector<load_extra_methodst>
  build_extra_entry_points(const optionst &) const;
  const std::unique_ptr<const select_pointer_typet> pointer_type_selector;
 
  synthetic_methods_mapt synthetic_methods;
  stub_global_initializer_factoryt stub_global_initializer_factory;
  class_hierarchyt class_hierarchy;
 
  std::unordered_map<std::string, object_creation_referencet> references;
 
  void parse_from_main_class(message_handlert &);
  void initialize_class_loader(message_handlert &);
};
 
std::unique_ptr<languaget> new_java_bytecode_language();
 
void parse_java_language_options(const cmdlinet &cmd, optionst &options);
 
prefix_filtert get_context(const optionst &options);
 
#endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_LANGUAGE_H