10 #ifndef CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_LANGUAGE_H 11 #define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_LANGUAGE_H 30 #define JAVA_BYTECODE_LANGUAGE_OPTIONS \ 31 "(disable-uncaught-exception-check)" \ 32 "(throw-assertion-error)" \ 33 "(java-assume-inputs-non-null)" \ 34 "(throw-runtime-exceptions)" \ 35 "(max-nondet-array-length):" \ 36 "(max-nondet-tree-depth):" \ 37 "(java-max-vla-length):" \ 38 "(java-cp-include-files):" \ 40 "(lazy-methods-extra-entry-point):" \ 41 "(java-load-class):" \ 42 "(java-no-load-class):" 44 #define JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP \ 45 " --disable-uncaught-exception-check\n" \ 46 " ignore uncaught exceptions and errors\n" \ 47 " --throw-assertion-error throw java.lang.AssertionError on violated\n" \ 48 " assert statements instead of failing\n" \ 49 " at the location of the assert statement\n" \ 50 " --throw-runtime-exceptions make implicit runtime exceptions explicit\n" \ 51 " --max-nondet-array-length N limit nondet (e.g. input) array size to <= N\n" \ 52 " --max-nondet-tree-depth N limit size of nondet (e.g. input) object tree;\n" \ 53 " at level N references are set to null\n" \ 54 " --java-assume-inputs-non-null\n" \ 55 " never initialize reference-typed parameter to the\n" \ 56 " entry point with null\n" \ 57 " --java-max-vla-length N limit the length of user-code-created arrays\n" \ 58 " --java-cp-include-files r regexp or JSON list of files to load\n" \ 59 " (with '@' prefix)\n" \ 60 " --no-lazy-methods load and translate all methods given on\n" \ 61 " the command line and in --classpath\n" \ 62 " Default is to load methods that appear to be\n" \ 63 " reachable from the --function entry point\n" \ 65 " Note that --show-symbol-table, --show-goto-functions\n" \ 66 " and --show-properties output are restricted to\n" \ 67 " loaded methods by default.\n" \ 68 " --lazy-methods-extra-entry-point METHODNAME\n" \ 69 " treat METHODNAME as a possible program entry\n" \ 70 " point for the purpose of lazy method loading\n" \ 71 " METHODNAME can be a regex that will be matched\n" \ 72 " against all symbols. If missing a java:: prefix\n" \ 73 " will be added. If no descriptor is found, all\n" \ 74 " overloads of a method will also be added.\n" 86 #define JAVA_CLASS_MODEL_SUFFIX "@class_model" 94 std::istream &instream,
95 const std::string &path,
96 std::ostream &outstream)
override;
99 std::istream &instream,
100 const std::string &path)
override;
107 const std::string &module)
override;
142 const std::string &code,
143 const std::string &module,
148 {
return util_make_unique<java_bytecode_languaget>(); }
150 std::string
id()
const override {
return "java"; }
151 std::string
description()
const override {
return "Java Bytecode"; }
152 std::set<std::string>
extensions()
const override;
198 virtual std::vector<load_extra_methodst>
218 #endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_LANGUAGE_H std::vector< irep_idt > java_load_classes
The type of an expression, extends irept.
bool throw_assertion_error
std::unique_ptr< languaget > new_language() override
Non-graph-based representation of the class hierarchy.
java_class_loadert java_class_loader
bool assert_uncaught_exceptions
std::string java_cp_include_files
void modules_provided(std::set< std::string > &modules) override
size_t max_user_array_length
std::unique_ptr< languaget > new_java_bytecode_language()
const select_pointer_typet & get_pointer_type_selector() const
java_string_library_preprocesst string_preprocess
void show_parse(std::ostream &out) override
class_hierarchyt class_hierarchy
java_object_factory_parameterst object_factory_parameters
virtual void convert_lazy_method(const irep_idt &function_id, symbol_table_baset &symbol_table) override
Promote a lazy-converted method (one whose type is known but whose body hasn't been converted) into a...
bool from_expr(const exprt &expr, std::string &code, const namespacet &ns) override
Formats the given expression in a language-specific way.
bool assume_inputs_non_null
std::set< std::string > extensions() const override
virtual void methods_provided(std::unordered_set< irep_idt > &methods) const override
Provide feedback to language_filest so that when asked for a lazy method, it can delegate to this ins...
bool typecheck(symbol_tablet &context, const std::string &module) override
nonstd::optional< T > optionalt
virtual bool preprocess(std::istream &instream, const std::string &path, std::ostream &outstream) override
ANSI-C preprocessing.
Collect methods needed to be loaded using the lazy method.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
std::vector< load_extra_methodst > extra_methods
Abstract interface to support a programming language.
std::string id() const override
java_bytecode_languaget(std::unique_ptr< select_pointer_typet > pointer_type_selector)
synthetic_methods_mapt synthetic_methods
Maps synthetic method names on to the particular type of synthetic method (static initializer...
std::string description() const override
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
bool to_expr(const std::string &code, const std::string &module, exprt &expr, const namespacet &ns) override
Parses the given string into an expression.
bool from_type(const typet &type, std::string &code, const namespacet &ns) override
Formats the given type in a language-specific way.
const std::unique_ptr< const select_pointer_typet > pointer_type_selector
std::unordered_set< std::string > no_load_classes
method_bytecodet method_bytecode
bool do_ci_lazy_method_conversion(symbol_tablet &, method_bytecodet &)
Uses a simple context-insensitive ('ci') analysis to determine which methods may be reachable from th...
Base class for all expressions.
bool parse(std::istream &instream, const std::string &path) override
We set the main class (i.e. class to start the class loading analysis from, see java_class_loadert) d...
The symbol table base class interface.
virtual std::vector< load_extra_methodst > build_extra_entry_points(const optionst &) const
This method should be overloaded to provide alternative approaches for specifying extra entry points...
Class responsible to load .class files.
Synthetic methods are particular methods internally generated by the Java frontend, including thunks to ensure static initializers are run once and initializers created for unknown / stub types.
java_bytecode_languaget()
Context-insensitive lazy methods container.
void set_language_options(const optionst &) override
Consume options that are java bytecode specific.
bool string_refinement_enabled
std::unordered_map< irep_idt, synthetic_method_typet > synthetic_methods_mapt
Maps method names on to a synthetic method kind.
lazy_methods_modet lazy_methods_mode
bool generate_support_functions(symbol_tablet &symbol_table) override
Create language-specific support functions, such as __CPROVER_start, __CPROVER_initialize and languag...
stub_global_initializer_factoryt stub_global_initializer_factory
void parse_java_language_options(const cmdlinet &cmd, optionst &options)
Parse options that are java bytecode specific.
Handle selection of correct pointer type (for example changing abstract classes to concrete versions)...
std::vector< irep_idt > main_jar_classes
void convert_single_method(const irep_idt &function_id, symbol_table_baset &symbol_table)
Produce code for simple implementation of String Java libraries.
virtual ~java_bytecode_languaget()
bool throw_runtime_exceptions