59 "java-assume-inputs-non-null", cmd.
isset(
"java-assume-inputs-non-null"));
61 "throw-runtime-exceptions", cmd.
isset(
"throw-runtime-exceptions"));
63 "uncaught-exception-check", !cmd.
isset(
"disable-uncaught-exception-check"));
65 "throw-assertion-error", cmd.
isset(
"throw-assertion-error"));
67 "assert-no-exceptions-thrown", cmd.
isset(
"assert-no-exceptions-thrown"));
70 if(cmd.
isset(
"java-max-vla-length"))
73 "java-max-vla-length", cmd.
get_value(
"java-max-vla-length"));
77 "symex-driven-lazy-loading", cmd.
isset(
"symex-driven-lazy-loading"));
80 "ignore-manifest-main-class", cmd.
isset(
"ignore-manifest-main-class"));
82 if(cmd.
isset(
"context-include"))
85 if(cmd.
isset(
"context-exclude"))
88 if(cmd.
isset(
"java-load-class"))
91 if(cmd.
isset(
"java-no-load-class"))
94 "java-no-load-class", cmd.
get_values(
"java-no-load-class"));
96 if(cmd.
isset(
"lazy-methods-extra-entry-point"))
99 "lazy-methods-extra-entry-point",
100 cmd.
get_values(
"lazy-methods-extra-entry-point"));
102 if(cmd.
isset(
"java-cp-include-files"))
105 "java-cp-include-files", cmd.
get_value(
"java-cp-include-files"));
107 if(cmd.
isset(
"static-values"))
112 "java-lift-clinit-calls", cmd.
isset(
"java-lift-clinit-calls"));
117 std::vector<std::string> context_include;
118 std::vector<std::string> context_exclude;
120 context_include.push_back(
"java::" + include);
122 context_exclude.push_back(
"java::" + exclude);
123 return prefix_filtert(std::move(context_include), std::move(context_exclude));
126 std::unordered_multimap<irep_idt, symbolt> &
176 if(options.
is_set(
"java-load-class"))
182 if(options.
is_set(
"java-no-load-class"))
184 const auto &no_load_values = options.
get_list_option(
"java-no-load-class");
187 const std::list<std::string> &extra_entry_points =
190 extra_entry_points.begin(),
191 extra_entry_points.end(),
201 jsont json_cp_config;
206 throw "cannot read JSON input configuration for JAR loading";
209 throw "the JSON file has a wrong format";
210 jsont include_files=json_cp_config[
"jar"];
212 throw "the JSON file has a wrong format";
218 file_entry.is_string() &&
has_suffix(file_entry.value,
".jar"),
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" };
312 auto get_string_base_classes = [
this](
const irep_idt &
id) {
323 "Error: Could not find or load main class " + main_class);
335 const auto maybe_class_name =
337 if(!maybe_class_name)
342 status() <<
"Trying to load Java main class: " << maybe_class_name.value()
357 const auto &parse_trees =
359 if(parse_trees.empty() || !parse_trees.front().loading_successful)
384 std::istream &instream,
385 const std::string &path)
393 std::ifstream jar_file(path);
397 "Error: Unable to access jarfile " + path);
408 const std::string &entry_method =
config.
main.value();
409 const auto last_dot_position = entry_method.find_last_of(
'.');
410 main_class = entry_method.substr(0, last_dot_position);
415 std::string manifest_main_class = manifest[
"Main-Class"];
419 !manifest_main_class.empty() &&
432 status() <<
"JAR file without entry point: loading class files" <<
eom;
435 for(
const auto &c : classes)
467 const std::string statement =
469 if(statement ==
"getfield" || statement ==
"putfield")
472 expr_dynamic_cast<fieldref_exprt>(instruction.
args[0]);
474 const symbolt *class_symbol = symbol_table.
lookup(class_symbol_id);
476 class_symbol !=
nullptr,
477 "all types containing fields should have been loaded");
487 symbolt &writable_class_symbol =
491 components.emplace_back(component_name, fieldref.
type());
492 components.back().set_base_name(component_name);
493 components.back().set_pretty_name(component_name);
494 components.back().set_is_final(
true);
501 !class_type->
bases().empty(),
503 "' (which was missing a field '" +
id2string(component_name) +
504 "' referenced from method '" +
id2string(method.name) +
506 "') should have an opaque superclass");
507 const auto &superclass_type = class_type->
bases().front().type();
508 class_symbol_id = superclass_type.get_identifier();
533 new_class_symbol.
type = symbol_expr.
type();
536 "class identifier should have 'java::' prefix");
539 new_class_symbol.
mode = ID_java;
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));
586 ldc_arg0.
id() == ID_constant,
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)
658 new_symbol.
name = symbol_id;
660 new_symbol.
type = symbol_type;
665 new_symbol.
type.
set(ID_C_access, ID_public);
667 new_symbol.
type.
set(ID_C_constant,
true);
669 new_symbol.
mode = ID_java;
674 if(symbol_type.
id() == ID_pointer && !force_nondet_init)
678 bool add_failed = symbol_table.
add(new_symbol);
680 !add_failed,
"caller should have checked symbol not already in table");
698 std::vector<irep_idt> classes_to_check;
699 classes_to_check.push_back(start_class_id);
701 while(!classes_to_check.empty())
703 irep_idt to_check = classes_to_check.back();
704 classes_to_check.pop_back();
710 to_check !=
"java::java.lang.Object")
716 class_hierarchy.
class_map.at(to_check).parents;
717 classes_to_check.insert(
718 classes_to_check.end(), parents.begin(), parents.end());
745 const std::string statement =
747 if(statement ==
"getstatic" || statement ==
"putstatic")
750 instruction.
args.size() > 0,
751 "get/putstatic should have at least one argument");
753 expr_dynamic_cast<fieldref_exprt>(instruction.
args[0]);
759 const auto referred_component =
761 if(!referred_component)
768 class_id, symbol_table, class_hierarchy);
780 bool no_incomplete_ancestors = add_to_class_id.
empty();
781 if(no_incomplete_ancestors)
783 add_to_class_id = class_id;
788 <<
"non-stub type " << class_id <<
". In future this "
799 instruction.
args[0].type(),
801 no_incomplete_ancestors);
820 symbol_table.
begin() == symbol_table.
end(),
821 "the Java front-end should only be used with an empty symbol table");
832 java_class_loadert::parse_tree_with_overridest_mapt::const_iterator it =
853 if(class_trees.second.front().parsed_class.name.empty())
881 std::vector<irep_idt> methods_to_check;
884 for(
const auto &id_and_symbol : symbol_table)
886 const auto &symbol = id_and_symbol.second;
887 const auto &
id = symbol.name;
890 methods_to_check.push_back(
id);
894 for(
const auto &
id : methods_to_check)
913 if(c.second.front().parsed_class.name.empty())
918 c.second.front().parsed_class.name, symbol_table);
923 <<
"Not marking class " << c.first
924 <<
" implicitly generic due to missing outer class symbols"
942 const std::size_t before_constant_globals_size = symbol_table.
symbols.size();
951 status() <<
"Java: added "
952 << (symbol_table.
symbols.size() - before_constant_globals_size)
953 <<
" String or Class constant symbols"
1010 function_id_and_type.first,
1011 journalling_symbol_table,
1023 for(
const auto &fn_name : journalling_symbol_table.
get_inserted())
1079 "the program has no entry point",
1081 "Check that the specified entry point is included by your "
1082 "--context-include or --context-exclude options");
1087 symbol_table_builder,
1096 return java_build_arguments(
1099 language_options->assume_inputs_non_null,
1100 object_factory_parameters,
1101 get_pointer_type_selector(),
1102 get_message_handler());
1131 symbol_table_builder,
1132 std::move(lazy_methods_needed),
1146 return method_gather(
1163 std::unordered_set<irep_idt> &methods)
const
1165 const std::string cprover_class_prefix =
"java::org.cprover.CProver.";
1171 methods.insert(kv.first);
1174 methods.insert(kv.first);
1229 const codet &function_body,
1232 if(needed_lazy_methods)
1238 if(it->id() == ID_code)
1240 const auto fn_call = expr_try_dynamic_cast<code_function_callt>(*it);
1244 expr_try_dynamic_cast<symbol_exprt>(fn_call->function());
1246 needed_lazy_methods->add_needed_method(fn_sym->
get_identifier());
1249 it->id() == ID_side_effect &&
1254 expr_try_dynamic_cast<symbol_exprt>(call_expr.function());
1259 "Java synthetic methods are not "
1260 "expected to produce side_effect_expr_function_callt. If "
1261 "that has changed, remove this invariant. Also note that "
1262 "as of the time of writing remove_virtual_functions did "
1263 "not support this form of function call.");
1316 writable_symbol.
value =
1342 const auto &symbol = symbol_table.
lookup_ref(function_id);
1348 synthetic_methods_mapt::iterator synthetic_method_it;
1358 writable_symbol, cmb->get().method.local_variable_table, symbol_table);
1366 writable_symbol.
value = std::move(generated_code);
1376 switch(synthetic_method_it->second)
1400 const auto class_name =
1403 class_name,
"user_specified_clinit must be declared by a class.");
1406 "static-values JSON must be available");
1411 needed_lazy_methods,
1418 writable_symbol.
value =
1438 "CProver.createArrayWithType should only be registered if "
1439 "we have a real implementation available");
1441 writable_symbol, cmb->get().method.local_variable_table, symbol_table);
1459 symbol_table.
lookup_ref(cmb->get().class_id),
1465 std::move(needed_lazy_methods),
1474 if(needed_lazy_methods)
1481 type_try_dynamic_cast<pointer_typet>(function_type.
return_type()))
1493 needed_lazy_methods->add_all_needed_classes(*pointer_return_type);
1510 parse_trees.front().output(out);
1511 if(parse_trees.size() > 1)
1513 out <<
"\n\nClass has the following overlays:\n\n";
1514 for(
auto parse_tree_it = std::next(parse_trees.begin());
1515 parse_tree_it != parse_trees.end();
1518 parse_tree_it->output(out);
1520 out <<
"End of class overlays.\n";
1526 return util_make_unique<java_bytecode_languaget>();
1548 const std::string &code,
1549 const std::string &module,
1558 std::istringstream i_preprocessed(code);
1562 java_bytecode_parser.clear();
1563 java_bytecode_parser.filename=
"";
1564 java_bytecode_parser.in=&i_preprocessed;
1566 java_bytecode_parser.grammar=java_bytecode_parsert::EXPRESSION;
1567 java_bytecode_parser.mode=java_bytecode_parsert::GCC;
1568 java_bytecode_scanner_init();
1570 bool result=java_bytecode_parser.parse();
1572 if(java_bytecode_parser.parse_tree.items.empty())
1576 expr=java_bytecode_parser.parse_tree.items.front().value();
1586 java_bytecode_parser.clear();
1607 std::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.
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.
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.
const_depth_iteratort depth_cend() const
typet & type()
Return the type of the expression.
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 ...
Thrown when we can't handle something in an input source file.
void set(const irep_namet &name, const irep_idt &value)
const irep_idt & id() const
const irep_idt & get(const irep_namet &name) 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...
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()
void set_message_handler(message_handlert &message_handler) 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
bool do_ci_lazy_method_conversion(symbol_tablet &)
Uses a simple context-insensitive ('ci') analysis to determine which methods may be reachable from th...
class_hierarchyt class_hierarchy
bool generate_support_functions(symbol_tablet &symbol_table) override
Create language-specific support functions, such as __CPROVER_start, __CPROVER_initialize and languag...
void parse_from_main_class()
java_object_factory_parameterst object_factory_parameters
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 typecheck(symbol_tablet &context, const std::string &module) override
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.
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_tablet &symbol_table)
std::unordered_multimap< irep_idt, symbolt > map
Class that provides messages with a built-in verbosity 'level'.
message_handlert * message_handler
mstreamt & warning() const
mstreamt & status() const
mstreamt & result() const
message_handlert & get_message_handler()
virtual void set_message_handler(message_handlert &_message_handler)
opt_reft get(const irep_idt &method_id)
optionalt< 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
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...
void create_stub_global_initializer_symbols(symbol_tablet &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.
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.
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.
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)
virtual iteratort begin() override
virtual iteratort end() override
irep_idt base_name
Base (non-scoped) name.
source_locationt location
Source code location of definition of symbol.
typet type
Type of symbol.
irep_idt name
The unique identifier.
irep_idt pretty_name
Language-specific display name.
exprt value
Initial value of symbol.
irep_idt mode
Language mode.
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_tablet &symbol_table, message_handlert &message_handler)
Iterate through the symbol table to find and instrument synchronized methods.
void convert_threadblock(symbol_tablet &symbol_table)
Iterate through the symbol table to find and appropriately instrument thread-blocks.
bool java_bytecode_convert_class(const java_class_loadert::parse_tree_with_overlayst &parse_trees, symbol_tablet &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.
void mark_java_implicitly_generic_class_type(const irep_idt &class_name, symbol_tablet &symbol_table)
Checks if the class is implicitly generic, i.e., it is an inner class of any generic class.
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_tablet &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.
void parse_java_language_options(const cmdlinet &cmd, optionst &options)
Parse options that are java bytecode specific.
static void infer_opaque_type_fields(const java_bytecode_parse_treet &parse_tree, symbol_tablet &symbol_table)
Infer fields that must exist on opaque types from field accesses against them.
static void generate_constant_global_variables(java_bytecode_parse_treet &parse_tree, symbol_tablet &symbol_table, bool string_refinement_enabled)
Creates global variables for constants mentioned in a given method.
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 exprt get_ldc_result(const exprt &ldc_arg0, symbol_tablet &symbol_table, bool string_refinement_enabled)
Get result of a Java load-constant (ldc) instruction.
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_tablet &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 symbol_exprt get_or_create_class_literal_symbol(const irep_idt &class_id, symbol_tablet &symbol_table)
Create if necessary, then return the constant global java.lang.Class symbol for a given class id.
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.
void create_static_initializer_symbols(symbol_tablet &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.
std::unordered_multimap< irep_idt, symbolt > class_to_declared_symbols(const symbol_tablet &symbol_table)
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)
optionalt< resolve_inherited_componentt::inherited_componentt > get_inherited_component(const irep_idt &component_class_id, const irep_idt &component_name, const symbol_tablet &symbol_table, bool include_interfaces)
Finds an inherited component (method or field), taking component visibility into account.
optionalt< 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.
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.
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)
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.
void create_invokedynamic_synthetic_classes(const irep_idt &method_identifier, const java_bytecode_parse_treet::methodt::instructionst &instructions, symbol_tablet &symbol_table, synthetic_methods_mapt &synthetic_methods, message_handlert &message_handler)
Java lambda code synthesis.
codet lift_clinit_calls(codet input)
file Static initializer call lifting
std::function< std::vector< irep_idt >const symbol_tablet &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.
nonstd::optional< T > optionalt
#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.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_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
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.