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"));
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"))
80 if(cmd.
isset(
"context-exclude"))
83 if(cmd.
isset(
"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"))
107 "java-lift-clinit-calls", cmd.
isset(
"java-lift-clinit-calls"));
114 std::vector<std::string> context_include;
115 std::vector<std::string> context_exclude;
117 context_include.push_back(
"java::" + include);
119 context_exclude.push_back(
"java::" + exclude);
120 return prefix_filtert(std::move(context_include), std::move(context_exclude));
123 std::unordered_multimap<irep_idt, symbolt> &
173 if(options.
is_set(
"java-load-class"))
179 if(options.
is_set(
"java-no-load-class"))
181 const auto &no_load_values = options.
get_list_option(
"java-no-load-class");
184 const std::list<std::string> &extra_entry_points =
187 extra_entry_points.begin(),
188 extra_entry_points.end(),
198 jsont json_cp_config;
202 throw "cannot read JSON input configuration for JAR loading";
206 throw "the JSON file has a wrong format";
207 jsont include_files=json_cp_config[
"jar"];
209 throw "the JSON file has a wrong format";
215 file_entry.is_string() &&
has_suffix(file_entry.value,
".jar"),
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");
231 if(
parse_json(filename, message_handler, tmp_json))
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" };
308 auto get_string_base_classes = [
this](
const irep_idt &
id) {
319 "Error: Could not find or load main class " + main_class);
330 log.status() <<
"Trying to load Java main class: " <<
main_class
335 const auto maybe_class_name =
337 if(!maybe_class_name)
342 log.status() <<
"Trying to load Java main class: "
345 maybe_class_name.value(), message_handler))
358 if(parse_trees.empty() || !parse_trees.front().loading_successful)
383 std::istream &instream,
384 const std::string &path,
393 std::ifstream jar_file(path);
407 const std::string &entry_method =
config.
main.value();
408 const auto last_dot_position = entry_method.find_last_of(
'.');
409 main_class = entry_method.substr(0, last_dot_position);
414 std::string manifest_main_class = manifest[
"Main-Class"];
418 !manifest_main_class.empty() &&
432 log.status() <<
"JAR file without entry point: loading class files"
436 for(
const auto &c : classes)
468 const std::string statement =
470 if(statement ==
"getfield" || statement ==
"putfield")
473 expr_dynamic_cast<fieldref_exprt>(instruction.
args[0]);
475 const symbolt *class_symbol = symbol_table.
lookup(class_symbol_id);
477 class_symbol !=
nullptr,
478 "all types containing fields should have been loaded");
488 symbolt &writable_class_symbol =
492 components.emplace_back(component_name, fieldref.
type());
493 components.back().set_base_name(component_name);
494 components.back().set_pretty_name(component_name);
495 components.back().set_is_final(
true);
502 !class_type->
bases().empty(),
504 "' (which was missing a field '" +
id2string(component_name) +
505 "' referenced from method '" +
id2string(method.name) +
507 "') should have an opaque superclass");
508 const auto &superclass_type = class_type->
bases().front().type();
509 class_symbol_id = superclass_type.get_identifier();
536 new_class_symbol.name.starts_with(
"java::"),
537 "class identifier should have 'java::' prefix");
538 new_class_symbol.base_name =
539 id2string(new_class_symbol.name).substr(6);
540 new_class_symbol.is_lvalue =
true;
541 new_class_symbol.is_state_var =
true;
542 new_class_symbol.is_static_lifetime =
true;
543 new_class_symbol.type.set(ID_C_no_nondet_initialization,
true);
544 symbol_table.
add(new_class_symbol);
565 const exprt &ldc_arg0,
567 bool string_refinement_enabled)
569 if(ldc_arg0.
id() == ID_type)
577 const auto &literal =
578 expr_try_dynamic_cast<java_string_literal_exprt>(ldc_arg0))
581 *literal, symbol_table, string_refinement_enabled));
587 "ldc argument should be constant, string literal or class literal");
604 bool string_refinement_enabled)
613 const std::string statement =
616 if(statement ==
"ldc" ||
617 statement ==
"ldc2" ||
618 statement ==
"ldc_w" ||
619 statement ==
"ldc2_w")
623 instruction.
args.size() != 0,
624 "ldc instructions should have an argument");
625 instruction.
args[0] =
629 string_refinement_enabled);
650 const typet &symbol_type,
652 bool force_nondet_init)
654 symbolt new_symbol{symbol_id, symbol_type, ID_java};
655 new_symbol.is_static_lifetime =
true;
656 new_symbol.is_lvalue =
true;
657 new_symbol.is_state_var =
true;
658 new_symbol.base_name = symbol_basename;
663 new_symbol.type.set(ID_C_access, ID_public);
665 new_symbol.type.set(ID_C_constant,
true);
666 new_symbol.pretty_name = new_symbol.name;
670 if(symbol_type.
id() == ID_pointer && !force_nondet_init)
673 new_symbol.value.make_nil();
674 bool add_failed = symbol_table.
add(new_symbol);
676 !add_failed,
"caller should have checked symbol not already in table");
694 std::vector<irep_idt> classes_to_check;
695 classes_to_check.push_back(start_class_id);
697 while(!classes_to_check.empty())
699 irep_idt to_check = classes_to_check.back();
700 classes_to_check.pop_back();
706 to_check !=
"java::java.lang.Object")
712 class_hierarchy.
class_map.at(to_check).parents;
713 classes_to_check.insert(
714 classes_to_check.end(), parents.begin(), parents.end());
741 const std::string statement =
743 if(statement ==
"getstatic" || statement ==
"putstatic")
746 instruction.
args.size() > 0,
747 "get/putstatic should have at least one argument");
749 expr_dynamic_cast<fieldref_exprt>(instruction.
args[0]);
755 const auto referred_component =
757 if(!referred_component)
764 class_id, symbol_table, class_hierarchy);
776 bool no_incomplete_ancestors = add_to_class_id.
empty();
777 if(no_incomplete_ancestors)
779 add_to_class_id = class_id;
783 log.warning() <<
"Stub static field " <<
component <<
" found for "
784 <<
"non-stub type " << class_id <<
". In future this "
795 instruction.
args[0].type(),
797 no_incomplete_ancestors);
817 symbol_table.
begin() == symbol_table.
end(),
818 "the Java front-end should only be used with an empty symbol table");
829 java_class_loadert::parse_tree_with_overridest_mapt::const_iterator it =
850 if(class_trees.second.front().parsed_class.name.empty())
878 std::vector<irep_idt> methods_to_check;
881 for(
const auto &id_and_symbol : symbol_table)
883 const auto &symbol = id_and_symbol.second;
884 const auto &
id = symbol.name;
887 methods_to_check.push_back(
id);
891 for(
const auto &
id : methods_to_check)
910 if(c.second.front().parsed_class.name.empty())
915 c.second.front().parsed_class.name, symbol_table);
920 log.warning() <<
"Not marking class " << c.first
921 <<
" implicitly generic due to missing outer class symbols"
939 const std::size_t before_constant_globals_size = symbol_table.
symbols.size();
950 log.status() <<
"Java: added "
951 << (symbol_table.
symbols.size() - before_constant_globals_size)
1008 function_id_and_type.first,
1009 journalling_symbol_table,
1018 journalling_symbol_table,
1024 journalling_symbol_table,
1028 for(
const auto &fn_name : journalling_symbol_table.
get_inserted())
1043 symbol_table,
language_options->throw_runtime_exceptions, message_handler);
1047 symbol_table, message_handler,
language_options->string_refinement_enabled);
1083 "the program has no entry point",
1085 "Check that the specified entry point is included by your "
1086 "--context-include or --context-exclude options");
1091 symbol_table_builder,
1100 return java_build_arguments(
1103 language_options->assume_inputs_non_null,
1104 object_factory_parameters,
1105 get_pointer_type_selector(),
1137 symbol_table_builder,
1138 std::move(lazy_methods_needed),
1153 return method_gather(
1170 std::unordered_set<irep_idt> &methods)
const
1172 const std::string cprover_class_prefix =
"java::org.cprover.CProver.";
1178 methods.insert(kv.first);
1181 methods.insert(kv.first);
1223 symbol_table, message_handler,
language_options->string_refinement_enabled);
1237 const codet &function_body,
1238 std::optional<ci_lazy_methods_neededt> needed_lazy_methods)
1240 if(needed_lazy_methods)
1246 if(it->id() == ID_code)
1248 const auto fn_call = expr_try_dynamic_cast<code_function_callt>(*it);
1252 expr_try_dynamic_cast<symbol_exprt>(fn_call->function());
1254 needed_lazy_methods->add_needed_method(fn_sym->
get_identifier());
1257 it->id() == ID_side_effect &&
1262 expr_try_dynamic_cast<symbol_exprt>(call_expr.function());
1267 "Java synthetic methods are not "
1268 "expected to produce side_effect_expr_function_callt. If "
1269 "that has changed, remove this invariant. Also note that "
1270 "as of the time of writing remove_virtual_functions did "
1271 "not support this form of function call.");
1295 std::optional<ci_lazy_methods_neededt> needed_lazy_methods,
1323 needed_lazy_methods,
1330 writable_symbol.
value =
1354 std::optional<ci_lazy_methods_neededt> needed_lazy_methods,
1358 const auto &symbol = symbol_table.
lookup_ref(function_id);
1364 synthetic_methods_mapt::iterator synthetic_method_it;
1374 writable_symbol, cmb->get().method.local_variable_table, symbol_table);
1378 writable_symbol, symbol_table, message_handler);
1382 writable_symbol.
value = std::move(generated_code);
1392 switch(synthetic_method_it->second)
1416 const auto class_name =
1419 class_name,
"user_specified_clinit must be declared by a class.");
1422 "static-values JSON must be available");
1427 needed_lazy_methods,
1434 writable_symbol.
value =
1444 function_id, symbol_table, message_handler);
1448 function_id, symbol_table, message_handler);
1454 "CProver.createArrayWithType should only be registered if "
1455 "we have a real implementation available");
1457 writable_symbol, cmb->get().method.local_variable_table, symbol_table);
1458 writable_symbol.
value =
1475 symbol_table.
lookup_ref(cmb->get().class_id),
1481 std::move(needed_lazy_methods),
1490 if(needed_lazy_methods)
1497 type_try_dynamic_cast<pointer_typet>(function_type.
return_type()))
1509 needed_lazy_methods->add_all_needed_classes(*pointer_return_type);
1528 parse_trees.front().output(out);
1529 if(parse_trees.size() > 1)
1531 out <<
"\n\nClass has the following overlays:\n\n";
1532 for(
auto parse_tree_it = std::next(parse_trees.begin());
1533 parse_tree_it != parse_trees.end();
1536 parse_tree_it->output(out);
1538 out <<
"End of class overlays.\n";
1544 return std::make_unique<java_bytecode_languaget>();
1566 const std::string &code,
1567 const std::string &module,
1577 std::istringstream i_preprocessed(code);
1581 java_bytecode_parser.clear();
1582 java_bytecode_parser.filename=
"";
1583 java_bytecode_parser.in=&i_preprocessed;
1584 java_bytecode_parser.set_message_handler(message_handler);
1585 java_bytecode_parser.grammar=java_bytecode_parsert::EXPRESSION;
1586 java_bytecode_parser.mode=java_bytecode_parsert::GCC;
1587 java_bytecode_scanner_init();
1589 bool result=java_bytecode_parser.parse();
1591 if(java_bytecode_parser.parse_tree.items.empty())
1595 expr=java_bytecode_parser.parse_tree.items.front().value();
1597 result=java_bytecode_convert(expr,
"", message_handler);
1605 java_bytecode_parser.clear();
1614 (void)message_handler;
1627 std::vector<load_extra_methodst>
static abstract_object_pointert transform(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns)
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.
Non-graph-based representation of the class hierarchy.
std::vector< irep_idt > idst
std::string get_value(char option) const
virtual bool isset(char option) const
const std::list< std::string > & get_values(const std::string &option) const
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.
const_depth_iteratort depth_cend() const
typet & type()
Return the type of the expression.
bool is_constant() const
Return whether the expression is a constant.
const_depth_iteratort depth_cbegin() const
Represents the argument of an instruction that uses a CONSTANT_Fieldref This is used for example as a...
irep_idt class_name() const
irep_idt component_name() const
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
const irep_idt & get(const irep_idt &name) const
const irep_idt & id() const
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
virtual bool parse(message_handlert &)
We set the main class (i.e. class to start the class loading analysis, see java_class_loadert) when w...
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...
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.
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.
fixed_keys_map_wrappert< parse_tree_with_overridest_mapt > get_class_with_overlays_map()
Map from class names to the bytecode parse trees.
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...
const componentst & components() const
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)
const changesett & get_inserted() const
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 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.
const basest & bases() const
Get the collection of base classes/structs.
bool has_component(const irep_idt &component_name) const
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.
virtual iteratort begin()=0
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
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.
static symbol_table_buildert wrap(symbol_table_baset &base_symbol_table)
source_locationt location
Source code location of definition of symbol.
typet type
Type of symbol.
irep_idt name
The unique identifier.
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.
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.
std::unique_ptr< languaget > new_java_bytecode_language()
@ LAZY_METHODS_MODE_EAGER
@ LAZY_METHODS_MODE_EXTERNAL_DRIVER
@ LAZY_METHODS_MODE_CONTEXT_INSENSITIVE
#define JAVA_CLASS_MODEL_SUFFIX
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.
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.
std::unordered_multimap< irep_idt, symbolt > class_to_declared_symbols(const symbol_table_baset &symbol_table)
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_class_typet & to_java_class_type(const typet &type)
const java_method_typet & to_java_method_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< 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.
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.
json_arrayt & to_json_array(jsont &json)
json_objectt & to_json_object(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 can_cast_type< code_typet >(const typet &type)
Check whether a reference to a typet is a code_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.