57 "java-assume-inputs-non-null",
cmd.isset(
"java-assume-inputs-non-null"));
59 "throw-runtime-exceptions",
cmd.isset(
"throw-runtime-exceptions"));
61 "uncaught-exception-check", !
cmd.isset(
"disable-uncaught-exception-check"));
63 "throw-assertion-error",
cmd.isset(
"throw-assertion-error"));
65 "assert-no-exceptions-thrown",
cmd.isset(
"assert-no-exceptions-thrown"));
66 options.
set_option(
"java-threading",
cmd.isset(
"java-threading"));
68 if(
cmd.isset(
"java-max-vla-length"))
71 "java-max-vla-length",
cmd.get_value(
"java-max-vla-length"));
75 "symex-driven-lazy-loading",
cmd.isset(
"symex-driven-lazy-loading"));
78 "ignore-manifest-main-class",
cmd.isset(
"ignore-manifest-main-class"));
80 if(
cmd.isset(
"context-include"))
81 options.
set_option(
"context-include",
cmd.get_values(
"context-include"));
83 if(
cmd.isset(
"context-exclude"))
84 options.
set_option(
"context-exclude",
cmd.get_values(
"context-exclude"));
86 if(
cmd.isset(
"java-load-class"))
87 options.
set_option(
"java-load-class",
cmd.get_values(
"java-load-class"));
89 if(
cmd.isset(
"java-no-load-class"))
92 "java-no-load-class",
cmd.get_values(
"java-no-load-class"));
94 if(
cmd.isset(
"lazy-methods-extra-entry-point"))
97 "lazy-methods-extra-entry-point",
98 cmd.get_values(
"lazy-methods-extra-entry-point"));
100 if(
cmd.isset(
"java-cp-include-files"))
103 "java-cp-include-files",
cmd.get_value(
"java-cp-include-files"));
105 if(
cmd.isset(
"static-values"))
107 options.
set_option(
"static-values",
cmd.get_value(
"static-values"));
110 "java-lift-clinit-calls",
cmd.isset(
"java-lift-clinit-calls"));
112 options.
set_option(
"lazy-methods", !
cmd.isset(
"no-lazy-methods"));
126std::unordered_multimap<irep_idt, symbolt> &
176 if(options.
is_set(
"java-load-class"))
182 if(options.
is_set(
"java-no-load-class"))
206 throw "cannot read JSON input configuration for JAR loading";
209 throw "the JSON file has a wrong format";
212 throw "the JSON file has a wrong format";
219 "classpath entry must be jar filename, but '" +
file_entry.value +
229 if(options.
is_set(
"static-values"))
231 const std::string filename = options.
get_option(
"static-values");
236 <<
"Provided JSON file for static-values cannot be parsed; it"
243 log.
warning() <<
"Provided JSON file for static-values is not a JSON "
254 if(options.
is_set(
"context-include") || options.
is_set(
"context-exclude"))
274 return {
"class",
"jar" };
323 "Error: Could not find or load main class " + main_class);
385 const std::string &path)
431 status() <<
"JAR file without entry point: loading class files" <<
eom;
466 const std::string statement =
468 if(statement ==
"getfield" || statement ==
"putfield")
476 "all types containing fields should have been loaded");
481 while(!
class_type->has_component(component_name))
490 components.emplace_back(component_name,
fieldref.type());
491 components.back().set_base_name(component_name);
492 components.back().set_pretty_name(component_name);
493 components.back().set_is_final(
true);
502 "' (which was missing a field '" +
id2string(component_name) +
503 "' referenced from method '" +
id2string(method.name) +
505 "') should have an opaque superclass");
535 "class identifier should have 'java::' prefix");
565 bool string_refinement_enabled)
579 *
literal, symbol_table, string_refinement_enabled));
585 "ldc argument should be constant, string literal or class literal");
602 bool string_refinement_enabled)
611 const std::string statement =
614 if(statement ==
"ldc" ||
615 statement ==
"ldc2" ||
616 statement ==
"ldc_w" ||
617 statement ==
"ldc2_w")
621 instruction.args.size() != 0,
622 "ldc instructions should have an argument");
623 instruction.args[0] =
627 string_refinement_enabled);
653 new_symbol.is_static_lifetime =
true;
654 new_symbol.is_lvalue =
true;
655 new_symbol.is_state_var =
true;
664 new_symbol.pretty_name = new_symbol.name;
671 new_symbol.value.make_nil();
674 !
add_failed,
"caller should have checked symbol not already in table");
704 to_check !=
"java::java.lang.Object")
710 class_hierarchy.
class_map.at(to_check).parents;
739 const std::string statement =
741 if(statement ==
"getstatic" || statement ==
"putstatic")
744 instruction.args.size() > 0,
745 "get/putstatic should have at least one argument");
762 class_id, symbol_table, class_hierarchy);
782 <<
"non-stub type " << class_id <<
". In future this "
793 instruction.args[0].type(),
814 symbol_table.
begin() == symbol_table.
end(),
815 "the Java front-end should only be used with an empty symbol table");
826 java_class_loadert::parse_tree_with_overridest_mapt::const_iterator it =
847 if(
class_trees.second.front().parsed_class.name.empty())
881 const auto &
id = symbol.name;
907 if(
c.second.front().parsed_class.name.empty())
912 c.second.front().parsed_class.name, symbol_table);
917 <<
"Not marking class " <<
c.first
918 <<
" implicitly generic due to missing outer class symbols"
945 status() <<
"Java: added "
947 <<
" String or Class constant symbols"
1061 if(!
res.is_success())
1062 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(),
1096 get_message_handler());
1157 std::unordered_set<irep_idt> &methods)
const
1165 methods.insert(
kv.first);
1168 methods.insert(
kv.first);
1226 if(needed_lazy_methods)
1240 needed_lazy_methods->add_needed_method(
fn_sym->get_identifier());
1253 "Java synthetic methods are not "
1254 "expected to produce side_effect_expr_function_callt. If "
1255 "that has changed, remove this invariant. Also note that "
1256 "as of the time of writing remove_virtual_functions did "
1257 "not support this form of function call.");
1336 const auto &symbol = symbol_table.
lookup_ref(function_id);
1394 const auto class_name =
1397 class_name,
"user_specified_clinit must be declared by a class.");
1400 "static-values JSON must be available");
1405 needed_lazy_methods,
1432 "CProver.createArrayWithType should only be registered if "
1433 "we have a real implementation available");
1459 std::move(needed_lazy_methods),
1468 if(needed_lazy_methods)
1507 out <<
"\n\nClass has the following overlays:\n\n";
1514 out <<
"End of class overlays.\n";
1542 const std::string &code,
1543 const std::string &
module,
1601std::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.
optionalt< 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...
void show_parse(std::ostream &out) override
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
virtual bool final(symbol_table_baset &context) override
Final adjustments, e.g.
virtual bool preprocess(std::istream &instream, const std::string &path, std::ostream &outstream) override
ANSI-C preprocessing.
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 generate_support_functions(symbol_table_baset &symbol_table) override
Create language-specific support functions, such as __CPROVER_start, __CPROVER_initialize and languag...
void set_message_handler(message_handlert &message_handler) override
bool typecheck(symbol_table_baset &context, const std::string &module) override
void set_language_options(const optionst &) override
Consume options that are java bytecode specific.
void initialize_class_loader()
bool from_type(const typet &type, std::string &code, const namespacet &ns) override
Formats the given type in a language-specific way.
bool to_expr(const std::string &code, const std::string &module, exprt &expr, const namespacet &ns) override
Parses the given string into an expression.
method_bytecodet method_bytecode
const std::unique_ptr< const select_pointer_typet > pointer_type_selector
class_hierarchyt class_hierarchy
void parse_from_main_class()
java_object_factory_parameterst object_factory_parameters
bool do_ci_lazy_method_conversion(symbol_table_baset &)
Uses a simple context-insensitive ('ci') analysis to determine which methods may be reachable from th...
optionalt< java_bytecode_language_optionst > language_options
java_string_library_preprocesst string_preprocess
void modules_provided(std::set< std::string > &modules) override
java_class_loadert java_class_loader
bool convert_single_method_code(const irep_idt &function_id, symbol_table_baset &symbol_table, optionalt< ci_lazy_methods_neededt > needed_lazy_methods, lazy_class_to_declared_symbols_mapt &class_to_declared_symbols)
Convert a method (one whose type is known but whose body hasn't been converted) but don't run typeche...
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.
virtual bool parse()
We set the main class (i.e. class to start the class loading analysis, see java_class_loadert) when w...
const select_pointer_typet & get_pointer_type_selector() const
bool from_expr(const exprt &expr, std::string &code, const namespacet &ns) override
Formats the given expression in a language-specific way.
std::unordered_map< std::string, object_creation_referencet > references
Map used in all calls to functions that deterministically create objects (currently only assign_from_...
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...
void convert_single_method(const irep_idt &function_id, symbol_table_baset &symbol_table, lazy_class_to_declared_symbols_mapt &class_to_declared_symbols)
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 > 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'.
message_handlert * message_handler
message_handlert & get_message_handler()
mstreamt & warning() const
virtual void set_message_handler(message_handlert &_message_handler)
mstreamt & result() const
mstreamt & status() const
opt_reft get(const irep_idt &method_id)
An exception that is raised checking whether a class is implicitly generic if a symbol for an outer c...
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
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.
bool has_prefix(const std::string &s, const std::string &prefix)
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, optionalt< ci_lazy_methods_neededt > needed_lazy_methods, java_string_library_preprocesst &string_preprocess, const class_hierarchyt &class_hierarchy, bool threading_support, const optionalt< 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 notify_static_method_calls(const codet &function_body, optionalt< ci_lazy_methods_neededt > needed_lazy_methods)
Notify ci_lazy_methods, if present, of any static function calls made by the given function body.
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.
@ 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)
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_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)
Create the body of a user_specified_clinit function for a given class, which includes assignments for...
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)
NODISCARD optionalt< 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.
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.
optionalt< irep_idt > declaring_class(const symbolt &symbol)
Gets the identifier of the class which declared a given symbol.
optionalt< 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())
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
optionalt< prefix_filtert > method_context
If set, method bodies are only elaborated if they pass the filter.
optionalt< json_objectt > static_values_json
JSON which contains initial values of static fields (right after the static initializer of the class ...
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
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.