54 "java-assume-inputs-non-null",
cmd.isset(
"java-assume-inputs-non-null"));
56 "throw-runtime-exceptions",
cmd.isset(
"throw-runtime-exceptions"));
58 "uncaught-exception-check", !
cmd.isset(
"disable-uncaught-exception-check"));
60 "throw-assertion-error",
cmd.isset(
"throw-assertion-error"));
62 "assert-no-exceptions-thrown",
cmd.isset(
"assert-no-exceptions-thrown"));
63 options.
set_option(
"java-threading",
cmd.isset(
"java-threading"));
65 if(
cmd.isset(
"java-max-vla-length"))
68 "java-max-vla-length",
cmd.get_value(
"java-max-vla-length"));
72 "symex-driven-lazy-loading",
cmd.isset(
"symex-driven-lazy-loading"));
75 "ignore-manifest-main-class",
cmd.isset(
"ignore-manifest-main-class"));
77 if(
cmd.isset(
"context-include"))
78 options.
set_option(
"context-include",
cmd.get_values(
"context-include"));
80 if(
cmd.isset(
"context-exclude"))
81 options.
set_option(
"context-exclude",
cmd.get_values(
"context-exclude"));
83 if(
cmd.isset(
"java-load-class"))
84 options.
set_option(
"java-load-class",
cmd.get_values(
"java-load-class"));
86 if(
cmd.isset(
"java-no-load-class"))
89 "java-no-load-class",
cmd.get_values(
"java-no-load-class"));
91 if(
cmd.isset(
"lazy-methods-extra-entry-point"))
94 "lazy-methods-extra-entry-point",
95 cmd.get_values(
"lazy-methods-extra-entry-point"));
97 if(
cmd.isset(
"java-cp-include-files"))
100 "java-cp-include-files",
cmd.get_value(
"java-cp-include-files"));
102 if(
cmd.isset(
"static-values"))
104 options.
set_option(
"static-values",
cmd.get_value(
"static-values"));
107 "java-lift-clinit-calls",
cmd.isset(
"java-lift-clinit-calls"));
109 options.
set_option(
"lazy-methods", !
cmd.isset(
"no-lazy-methods"));
123std::unordered_multimap<irep_idt, symbolt> &
173 if(options.
is_set(
"java-load-class"))
179 if(options.
is_set(
"java-no-load-class"))
202 throw "cannot read JSON input configuration for JAR loading";
206 throw "the JSON file has a wrong format";
209 throw "the JSON file has a wrong format";
216 "classpath entry must be jar filename, but '" +
file_entry.value +
226 if(options.
is_set(
"static-values"))
228 const std::string filename = options.
get_option(
"static-values");
234 <<
"Provided JSON file for static-values cannot be parsed; it"
241 log.warning() <<
"Provided JSON file for static-values is not a JSON "
252 if(options.
is_set(
"context-include") || options.
is_set(
"context-exclude"))
274 return {
"class",
"jar" };
319 "Error: Could not find or load main class " + main_class);
330 log.status() <<
"Trying to load Java main class: " <<
main_class
342 log.status() <<
"Trying to load Java main class: "
373 const std::string &path,
421 log.status() <<
"JAR file without entry point: loading class files"
457 const std::string statement =
459 if(statement ==
"getfield" || statement ==
"putfield")
467 "all types containing fields should have been loaded");
472 while(!
class_type->has_component(component_name))
481 components.emplace_back(component_name,
fieldref.type());
482 components.back().set_base_name(component_name);
483 components.back().set_pretty_name(component_name);
484 components.back().set_is_final(
true);
493 "' (which was missing a field '" +
id2string(component_name) +
494 "' referenced from method '" +
id2string(method.name) +
496 "') should have an opaque superclass");
527 "class identifier should have 'java::' prefix");
557 bool string_refinement_enabled)
571 *
literal, symbol_table, string_refinement_enabled));
577 "ldc argument should be constant, string literal or class literal");
594 bool string_refinement_enabled)
603 const std::string statement =
606 if(statement ==
"ldc" ||
607 statement ==
"ldc2" ||
608 statement ==
"ldc_w" ||
609 statement ==
"ldc2_w")
613 instruction.args.size() != 0,
614 "ldc instructions should have an argument");
615 instruction.args[0] =
619 string_refinement_enabled);
645 new_symbol.is_static_lifetime =
true;
646 new_symbol.is_lvalue =
true;
647 new_symbol.is_state_var =
true;
656 new_symbol.pretty_name = new_symbol.name;
663 new_symbol.value.make_nil();
666 !
add_failed,
"caller should have checked symbol not already in table");
696 to_check !=
"java::java.lang.Object")
702 class_hierarchy.
class_map.at(to_check).parents;
731 const std::string statement =
733 if(statement ==
"getstatic" || statement ==
"putstatic")
736 instruction.args.size() > 0,
737 "get/putstatic should have at least one argument");
754 class_id, symbol_table, class_hierarchy);
773 log.warning() <<
"Stub static field " <<
component <<
" found for "
774 <<
"non-stub type " << class_id <<
". In future this "
785 instruction.args[0].type(),
807 symbol_table.
begin() == symbol_table.
end(),
808 "the Java front-end should only be used with an empty symbol table");
819 java_class_loadert::parse_tree_with_overridest_mapt::const_iterator it =
840 if(
class_trees.second.front().parsed_class.name.empty())
874 const auto &
id = symbol.name;
900 if(
c.second.front().parsed_class.name.empty())
905 c.second.front().parsed_class.name, symbol_table);
910 log.warning() <<
"Not marking class " <<
c.first
911 <<
" implicitly generic due to missing outer class symbols"
940 log.status() <<
"Java: added "
1033 symbol_table,
language_options->throw_runtime_exceptions, message_handler);
1037 symbol_table, message_handler,
language_options->string_refinement_enabled);
1060 if(!
res.is_success())
1061 return res.is_error();
1073 "the program has no entry point",
1075 "Check that the specified entry point is included by your "
1076 "--context-include or --context-exclude options");
1090 return java_build_arguments(
1093 language_options->assume_inputs_non_null,
1094 object_factory_parameters,
1095 get_pointer_type_selector(),
1160 std::unordered_set<irep_idt> &methods)
const
1168 methods.insert(
kv.first);
1171 methods.insert(
kv.first);
1213 symbol_table, message_handler,
language_options->string_refinement_enabled);
1228 std::optional<ci_lazy_methods_neededt> needed_lazy_methods)
1230 if(needed_lazy_methods)
1244 needed_lazy_methods->add_needed_method(
fn_sym->get_identifier());
1257 "Java synthetic methods are not "
1258 "expected to produce side_effect_expr_function_callt. If "
1259 "that has changed, remove this invariant. Also note that "
1260 "as of the time of writing remove_virtual_functions did "
1261 "not support this form of function call.");
1285 std::optional<ci_lazy_methods_neededt> needed_lazy_methods,
1313 needed_lazy_methods,
1344 std::optional<ci_lazy_methods_neededt> needed_lazy_methods,
1348 const auto &symbol = symbol_table.
lookup_ref(function_id);
1406 const auto class_name =
1409 class_name,
"user_specified_clinit must be declared by a class.");
1412 "static-values JSON must be available");
1417 needed_lazy_methods,
1434 function_id, symbol_table, message_handler);
1438 function_id, symbol_table, message_handler);
1444 "CProver.createArrayWithType should only be registered if "
1445 "we have a real implementation available");
1471 std::move(needed_lazy_methods),
1480 if(needed_lazy_methods)
1521 out <<
"\n\nClass has the following overlays:\n\n";
1528 out <<
"End of class overlays.\n";
1534 return std::make_unique<java_bytecode_languaget>();
1556 const std::string &code,
1557 const std::string &
module,
1604 (
void)message_handler;
1617std::vector<load_extra_methodst>
struct bytecode_infot const bytecode_info[]
Collect methods needed to be loaded using the lazy method.
std::function< bool(const irep_idt &function_id, ci_lazy_methods_neededt)> method_convertert
Operator to return the address of an object.
virtual void output(const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program, std::ostream &out) const
Output the abstract states for a single function.
virtual void clear()
Reset the abstract state.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Non-graph-based representation of the class hierarchy.
std::vector< irep_idt > idst
const typet & return_type() const
Data structure for representing an arbitrary statement in a program.
std::optional< std::string > main
struct configt::javat java
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
typet & type()
Return the type of the expression.
Represents the argument of an instruction that uses a CONSTANT_Fieldref This is used for example as a...
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
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...
synthetic_methods_mapt synthetic_methods
Maps synthetic method names on to the particular type of synthetic method (static initializer,...
std::vector< irep_idt > main_jar_classes
bool to_expr(const std::string &code, const std::string &module, exprt &expr, const namespacet &ns, message_handlert &message_handler) override
Parses the given string into an expression.
virtual bool final(symbol_table_baset &context) override
Final adjustments, e.g.
std::string id() const override
stub_global_initializer_factoryt stub_global_initializer_factory
std::set< std::string > extensions() const override
virtual ~java_bytecode_languaget()
bool from_type(const typet &type, std::string &code, const namespacet &ns) override
Formats the given type in a language-specific way.
void set_language_options(const optionst &, message_handlert &) override
Consume options that are java bytecode specific.
method_bytecodet method_bytecode
const std::unique_ptr< const select_pointer_typet > pointer_type_selector
class_hierarchyt class_hierarchy
java_object_factory_parameterst object_factory_parameters
void show_parse(std::ostream &out, message_handlert &) override
void initialize_class_loader(message_handlert &)
java_string_library_preprocesst string_preprocess
void modules_provided(std::set< std::string > &modules) override
java_class_loadert java_class_loader
virtual void convert_lazy_method(const irep_idt &function_id, symbol_table_baset &symbol_table, message_handlert &message_handler) override
Promote a lazy-converted method (one whose type is known but whose body hasn't been converted) into a...
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.
std::optional< java_bytecode_language_optionst > language_options
const select_pointer_typet & get_pointer_type_selector() const
void parse_from_main_class(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 &)
Convert a method (one whose type is known but whose body hasn't been converted) but don't run typeche...
bool from_expr(const exprt &expr, std::string &code, const namespacet &ns) override
Formats the given expression in a language-specific way.
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)
std::unordered_map< std::string, object_creation_referencet > references
Map used in all calls to functions that deterministically create objects (currently only assign_from_...
bool typecheck(symbol_table_baset &context, const std::string &module, message_handlert &message_handler) override
virtual bool preprocess(std::istream &instream, const std::string &path, std::ostream &outstream, message_handlert &message_handler) override
ANSI-C preprocessing.
bool generate_support_functions(symbol_table_baset &symbol_table, message_handlert &message_handler) override
Create language-specific support functions, such as __CPROVER_start, __CPROVER_initialize and languag...
bool do_ci_lazy_method_conversion(symbol_table_baset &, message_handlert &)
Uses a simple context-insensitive ('ci') analysis to determine which methods may be reachable from th...
bool parse(std::istream &instream, const std::string &path, message_handlert &message_handler) override
We set the main class (i.e. class to start the class loading analysis, see java_class_loadert) when w...
void add_classpath_entry(const std::string &, message_handlert &)
Appends an entry to the class path, used for loading classes.
void clear_classpath()
Clear all classpath entries.
jar_poolt jar_pool
a cache for jar_filet, by path name
Class representing a filter for class file loading.
std::vector< irep_idt > java_load_classes
Classes to be explicitly loaded.
std::vector< irep_idt > load_entire_jar(const std::string &jar_path, message_handlert &)
Load all class files from a .jar file.
bool can_load_class(const irep_idt &class_name, message_handlert &)
Checks whether class_name is parseable from the classpath, ignoring class loading limits.
fixed_keys_map_wrappert< parse_tree_with_overridest_mapt > get_class_with_overlays_map()
Map from class names to the bytecode parse trees.
void set_extra_class_refs_function(get_extra_class_refs_functiont func)
Sets a function that provides extra dependencies for a particular class.
void set_java_cp_include_files(const std::string &cp_include_files)
Set the argument of the class loader limit java_class_loader_limitt.
std::list< java_bytecode_parse_treet > parse_tree_with_overlayst
A list of parse trees supporting overlay classes.
void add_load_classes(const std::vector< irep_idt > &classes)
Adds the list of classes to the load queue, forcing them to be loaded even without explicit reference...
void get_all_function_names(std::unordered_set< irep_idt > &methods) const
bool implements_function(const irep_idt &function_id) const
std::vector< irep_idt > get_string_type_base_classes(const irep_idt &class_name)
Gets the base classes for known String and String-related types, or returns an empty list for other t...
void initialize_conversion_table()
fill maps with correspondence from java method names to conversion functions
codet code_for_function(const symbolt &symbol, symbol_table_baset &symbol_table, message_handlert &message_handler)
Should be called to provide code for string functions that are used in the code but for which no impl...
void initialize_known_type_table()
A symbol table wrapper that records which entries have been updated/removedA caller can pass a journa...
static journalling_symbol_tablet wrap(symbol_table_baset &base_symbol_table)
Map classes to the symbols they declare but is only computed once it is needed and the map is then ke...
std::unordered_multimap< irep_idt, symbolt > & get(const symbol_table_baset &symbol_table)
std::unordered_multimap< irep_idt, symbolt > map
Class that provides messages with a built-in verbosity 'level'.
opt_reft get(const irep_idt &method_id)
std::optional< std::reference_wrapper< const class_method_and_bytecodet > > opt_reft
An exception that is raised checking whether a class is implicitly generic if a symbol for an outer c...
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
The null pointer constant.
unsigned int get_unsigned_int_option(const std::string &option) const
bool is_set(const std::string &option) const
N.B. opts.is_set("foo") does not imply opts.get_bool_option("foo")
bool get_bool_option(const std::string &option) const
void set_option(const std::string &option, const bool value)
const std::string get_option(const std::string &option) const
const value_listt & get_list_option(const std::string &option) const
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Provides filtering of strings vai inclusion/exclusion lists of prefixes.
const irep_idt & get_statement() const
A struct tag type, i.e., struct_typet with an identifier.
void create_stub_global_initializer_symbols(symbol_table_baset &symbol_table, const std::unordered_set< irep_idt > &stub_globals_set, synthetic_methods_mapt &synthetic_methods)
Create static initializer symbols for each distinct class that has stub globals.
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)
Create the body of a synthetic static initializer (clinit method), which initialise stub globals in t...
Expression to hold a symbol (variable)
const irep_idt & get_identifier() const
The symbol table base class interface.
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
virtual iteratort begin()=0
const symbolst & symbols
Read-only field, used to look up symbols given their names.
virtual iteratort end()=0
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
static symbol_table_buildert wrap(symbol_table_baset &base_symbol_table)
source_locationt location
Source code location of definition of symbol.
exprt value
Initial value of symbol.
Thrown when some external system fails unexpectedly.
The type of an expression, extends irept.
irep_idt get_create_array_with_type_name()
Returns the symbol name for org.cprover.CProver.createArrayWithType
codet create_array_with_type_body(const irep_idt &function_id, symbol_table_baset &symbol_table, message_handlert &message_handler)
Returns the internal implementation for org.cprover.CProver.createArrayWithType.
Implementation of CProver.createArrayWithType intrinsic.
std::string type2java(const typet &type, const namespacet &ns)
std::string expr2java(const exprt &expr, const namespacet &ns)
Forward depth-first search iterators These iterators' copy operations are expensive,...
const std::string & id2string(const irep_idt &d)
void convert_synchronized_methods(symbol_table_baset &symbol_table, message_handlert &message_handler)
Iterate through the symbol table to find and instrument synchronized methods.
void convert_threadblock(symbol_table_baset &symbol_table)
Iterate through the symbol table to find and appropriately instrument thread-blocks.
void mark_java_implicitly_generic_class_type(const irep_idt &class_name, symbol_table_baset &symbol_table)
Checks if the class is implicitly generic, i.e., it is an inner class of any generic class.
bool java_bytecode_convert_class(const java_class_loadert::parse_tree_with_overlayst &parse_trees, symbol_table_baset &symbol_table, message_handlert &message_handler, size_t max_array_length, method_bytecodet &method_bytecode, java_string_library_preprocesst &string_preprocess, const std::unordered_set< std::string > &no_load_classes)
See class java_bytecode_convert_classt.
JAVA Bytecode Language Conversion.
void java_bytecode_initialize_parameter_names(symbolt &method_symbol, const java_bytecode_parse_treet::methodt::local_variable_tablet &local_variable_table, symbol_table_baset &symbol_table)
This uses a cut-down version of the logic in java_bytecode_convert_methodt::convert to initialize sym...
void java_bytecode_convert_method(const symbolt &class_symbol, const java_bytecode_parse_treet::methodt &method, symbol_table_baset &symbol_table, message_handlert &message_handler, size_t max_array_length, bool throw_assertion_error, std::optional< ci_lazy_methods_neededt > needed_lazy_methods, java_string_library_preprocesst &string_preprocess, const class_hierarchyt &class_hierarchy, bool threading_support, const std::optional< prefix_filtert > &method_context, bool assert_no_exceptions_thrown)
JAVA Bytecode Language Conversion.
void java_bytecode_instrument_symbol(symbol_table_baset &symbol_table, symbolt &symbol, const bool throw_runtime_exceptions, message_handlert &message_handler)
Instruments the code attached to symbol with runtime exceptions or corresponding assertions.
void java_bytecode_instrument(symbol_table_baset &symbol_table, const bool throw_runtime_exceptions, message_handlert &message_handler)
Instruments all the code in the symbol_table with runtime exceptions or corresponding assertions.
const std::vector< std::string > exception_needed_classes
void java_internal_additions(symbol_table_baset &dest)
static void generate_constant_global_variables(java_bytecode_parse_treet &parse_tree, symbol_table_baset &symbol_table, bool string_refinement_enabled)
Creates global variables for constants mentioned in a given method.
static exprt get_ldc_result(const exprt &ldc_arg0, symbol_table_baset &symbol_table, bool string_refinement_enabled)
Get result of a Java load-constant (ldc) instruction.
void parse_java_language_options(const cmdlinet &cmd, optionst &options)
Parse options that are java bytecode specific.
std::unique_ptr< languaget > new_java_bytecode_language()
static symbol_exprt get_or_create_class_literal_symbol(const irep_idt &class_id, symbol_table_baset &symbol_table)
Create if necessary, then return the constant global java.lang.Class symbol for a given class id.
static void infer_opaque_type_fields(const java_bytecode_parse_treet &parse_tree, symbol_table_baset &symbol_table)
Infer fields that must exist on opaque types from field accesses against them.
static void create_stub_global_symbol(symbol_table_baset &symbol_table, const irep_idt &symbol_id, const irep_idt &symbol_basename, const typet &symbol_type, const irep_idt &class_id, bool force_nondet_init)
Add a stub global symbol to the symbol table, initialising pointer-typed symbols with null and primit...
static void throwMainClassLoadingError(const std::string &main_class)
prefix_filtert get_context(const optionst &options)
static void create_stub_global_symbols(const java_bytecode_parse_treet &parse_tree, symbol_table_baset &symbol_table, const class_hierarchyt &class_hierarchy, messaget &log)
Search for getstatic and putstatic instructions in a class' bytecode and create stub symbols for any ...
static irep_idt get_any_incomplete_ancestor_for_stub_static_field(const irep_idt &start_class_id, const symbol_table_baset &symbol_table, const class_hierarchyt &class_hierarchy)
Find any incomplete ancestor of a given class that can have a stub static field attached to it.
static void notify_static_method_calls(const codet &function_body, std::optional< ci_lazy_methods_neededt > needed_lazy_methods)
Notify ci_lazy_methods, if present, of any static function calls made by the given function body.
@ LAZY_METHODS_MODE_EAGER
@ LAZY_METHODS_MODE_EXTERNAL_DRIVER
@ LAZY_METHODS_MODE_CONTEXT_INSENSITIVE
#define JAVA_CLASS_MODEL_SUFFIX
prefix_filtert get_context(const optionst &options)
bool java_bytecode_typecheck(symbol_table_baset &symbol_table, message_handlert &message_handler, bool string_refinement_enabled)
void java_bytecode_typecheck_updated_symbols(journalling_symbol_tablet &symbol_table, message_handlert &message_handler, bool string_refinement_enabled)
JAVA Bytecode Language Type Checking.
bool java_entry_point(symbol_table_baset &symbol_table, const irep_idt &main_class, message_handlert &message_handler, bool assume_init_pointers_not_null, bool assert_uncaught_exceptions, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector, bool string_refinement_enabled, const build_argumentst &build_arguments)
Given the symbol_table and the main_class to test, this function generates a new function __CPROVER__...
void create_java_initialize(symbol_table_baset &symbol_table)
Adds __cprover_initialize to the symbol_table but does not generate code for it yet.
void java_static_lifetime_init(symbol_table_baset &symbol_table, const source_locationt &source_location, bool assume_init_pointers_not_null, java_object_factory_parameterst object_factory_parameters, const select_pointer_typet &pointer_type_selector, bool string_refinement_enabled, message_handlert &message_handler)
Adds the body to __CPROVER_initialize.
main_function_resultt get_main_symbol(const symbol_table_baset &symbol_table, const irep_idt &main_class, message_handlert &message_handler)
Figures out the entry point of the code to verify.
std::unordered_multimap< irep_idt, symbolt > class_to_declared_symbols(const symbol_table_baset &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, std::optional< 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)
Create the body of a user_specified_clinit function for a given class, which includes assignments for...
void create_static_initializer_symbols(symbol_table_baset &symbol_table, synthetic_methods_mapt &synthetic_methods, const bool thread_safe, const bool is_user_clinit_needed)
Create static initializer wrappers and possibly user-specified functions for initial static field val...
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)
Produces the static initializer wrapper body for the given function.
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)
Thread safe version of the static initializer.
Representation of a constant Java string.
symbol_exprt get_or_create_string_literal_symbol(const java_string_literal_exprt &string_expr, symbol_table_baset &symbol_table, bool string_refinement_enabled)
Creates or gets an existing constant global symbol for a given string literal.
const java_method_typet & to_java_method_type(const typet &type)
const java_class_typet & to_java_class_type(const typet &type)
std::optional< irep_idt > declaring_class(const symbolt &symbol)
Gets the identifier of the class which declared a given symbol.
void set_declaring_class(symbolt &symbol, const irep_idt &declaring_class)
Sets the identifier of the class which declared a given symbol to declaring_class.
std::optional< std::string > class_name_from_method_name(const std::string &method_name)
Get JVM type name of the class in which method_name is defined.
std::optional< resolve_inherited_componentt::inherited_componentt > get_inherited_component(const irep_idt &component_class_id, const irep_idt &component_name, const symbol_table_baset &symbol_table, bool include_interfaces)
Finds an inherited component (method or field), taking component visibility into account.
json_objectt & to_json_object(jsont &json)
json_arrayt & to_json_array(jsont &json)
bool parse_json(std::istream &in, const std::string &filename, message_handlert &message_handler, jsont &dest)
void create_invokedynamic_synthetic_classes(const irep_idt &method_identifier, const java_bytecode_parse_treet::methodt::instructionst &instructions, symbol_table_baset &symbol_table, synthetic_methods_mapt &synthetic_methods, message_handlert &message_handler)
codet invokedynamic_synthetic_constructor(const irep_idt &function_id, symbol_table_baset &symbol_table, message_handlert &message_handler)
Create invokedynamic synthetic constructor.
codet invokedynamic_synthetic_method(const irep_idt &function_id, symbol_table_baset &symbol_table, message_handlert &message_handler)
Create the body for the synthetic method implementing an invokedynamic method.
Java lambda code synthesis.
codet lift_clinit_calls(codet input)
file Static initializer call lifting
std::function< std::vector< irep_idt >(const symbol_table_baset &symbol_table)> build_load_method_by_regex(const std::string &pattern)
Create a lambda that returns the symbols that the given pattern should be loaded.If the pattern doesn...
Process a pattern to use as a regex for selecting extra entry points for ci_lazy_methodst.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
#define INITIALIZE_FUNCTION
side_effect_exprt & to_side_effect_expr(exprt &expr)
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
const codet & to_code(const exprt &expr)
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
bool assert_uncaught_exceptions
bool assert_no_exceptions_thrown
Transform athrow bytecode instructions into assert FALSE followed by assume FALSE.
bool throw_runtime_exceptions
bool should_lift_clinit_calls
Should we lift clinit calls in function bodies to the top? For example, turning if(x) A....
std::string java_cp_include_files
std::optional< prefix_filtert > method_context
If set, method bodies are only elaborated if they pass the filter.
lazy_methods_modet lazy_methods_mode
bool string_refinement_enabled
bool throw_assertion_error
bool assume_inputs_non_null
assume inputs variables to be non-null
bool ignore_manifest_main_class
size_t max_user_array_length
max size for user code created arrays
java_bytecode_language_optionst()=default
std::vector< irep_idt > java_load_classes
list of classes to force load even without reference from the entry point
std::unordered_set< std::string > no_load_classes
List of classes to never load.
std::vector< load_extra_methodst > extra_methods
std::optional< json_objectt > static_values_json
JSON which contains initial values of static fields (right after the static initializer of the class ...
void set(const optionst &)
Assigns the parameters from given options.
bool has_suffix(const std::string &s, const std::string &suffix)
@ INVOKEDYNAMIC_METHOD
A generated method for a class capturing the parameters of an invokedynamic instruction.
@ USER_SPECIFIED_STATIC_INITIALIZER
Only exists if the --static-values option was used.
@ STATIC_INITIALIZER_WRAPPER
A static initializer wrapper (code of the form if(!already_run) clinit(); already_run = true;) These ...
@ STUB_CLASS_STATIC_INITIALIZER
A generated (synthetic) static initializer function for a stub type.
@ CREATE_ARRAY_WITH_TYPE
Our internal implementation of CProver.createArrayWithType, which needs to access internal type-id fi...
@ INVOKEDYNAMIC_CAPTURE_CONSTRUCTOR
A generated constructor for a class capturing the parameters of an invokedynamic instruction.