Go to the documentation of this file.
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" };
313 auto get_string_base_classes = [
this](
const irep_idt &
id) {
324 "Error: Could not find or load main class " + main_class);
336 const auto maybe_class_name =
338 if(!maybe_class_name)
343 status() <<
"Trying to load Java main class: " << maybe_class_name.value()
358 if(parse_trees.empty() || !parse_trees.front().loading_successful)
383 std::istream &instream,
384 const std::string &path)
392 std::ifstream jar_file(path);
396 "Error: Unable to access jarfile " + 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() &&
431 status() <<
"JAR file without entry point: loading class files" <<
eom;
433 for(
const auto &c : classes)
465 const std::string statement =
467 if(statement ==
"getfield" || statement ==
"putfield")
470 expr_dynamic_cast<fieldref_exprt>(instruction.
args[0]);
472 const symbolt *class_symbol = symbol_table.
lookup(class_symbol_id);
474 class_symbol !=
nullptr,
475 "all types containing fields should have been loaded");
485 symbolt &writable_class_symbol =
489 components.emplace_back(component_name, fieldref.
type());
490 components.back().set_base_name(component_name);
491 components.back().set_pretty_name(component_name);
492 components.back().set_is_final(
true);
499 !class_type->
bases().empty(),
501 "' (which was missing a field '" +
id2string(component_name) +
502 "' referenced from method '" +
id2string(method.name) +
504 "') should have an opaque superclass");
505 const auto &superclass_type = class_type->
bases().front().type();
506 class_symbol_id = superclass_type.get_identifier();
531 new_class_symbol.
type = symbol_expr.
type();
534 "class identifier should have 'java::' prefix");
537 new_class_symbol.
mode = ID_java;
541 new_class_symbol.
type.
set(ID_C_no_nondet_initialization,
true);
542 symbol_table.
add(new_class_symbol);
563 const exprt &ldc_arg0,
565 bool string_refinement_enabled)
567 if(ldc_arg0.
id() == ID_type)
575 const auto &literal =
576 expr_try_dynamic_cast<java_string_literal_exprt>(ldc_arg0))
579 *literal, symbol_table, string_refinement_enabled));
584 ldc_arg0.
id() == ID_constant,
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);
648 const typet &symbol_type,
650 bool force_nondet_init)
656 new_symbol.
name = symbol_id;
658 new_symbol.
type = symbol_type;
663 new_symbol.
type.
set(ID_C_access, ID_public);
665 new_symbol.
type.
set(ID_C_constant,
true);
667 new_symbol.
mode = ID_java;
672 if(symbol_type.
id() == ID_pointer && !force_nondet_init)
676 bool add_failed = symbol_table.
add(new_symbol);
678 !add_failed,
"caller should have checked symbol not already in table");
696 std::vector<irep_idt> classes_to_check;
697 classes_to_check.push_back(start_class_id);
699 while(!classes_to_check.empty())
701 irep_idt to_check = classes_to_check.back();
702 classes_to_check.pop_back();
708 to_check !=
"java::java.lang.Object")
714 class_hierarchy.
class_map.at(to_check).parents;
715 classes_to_check.insert(
716 classes_to_check.end(), parents.begin(), parents.end());
743 const std::string statement =
745 if(statement ==
"getstatic" || statement ==
"putstatic")
748 instruction.
args.size() > 0,
749 "get/putstatic should have at least one argument");
751 expr_dynamic_cast<fieldref_exprt>(instruction.
args[0]);
757 const auto referred_component =
759 if(!referred_component)
766 class_id, symbol_table, class_hierarchy);
778 bool no_incomplete_ancestors = add_to_class_id.
empty();
779 if(no_incomplete_ancestors)
781 add_to_class_id = class_id;
786 <<
"non-stub type " << class_id <<
". In future this "
797 instruction.
args[0].type(),
799 no_incomplete_ancestors);
818 symbol_table.
begin() == symbol_table.
end(),
819 "the Java front-end should only be used with an empty symbol table");
830 java_class_loadert::parse_tree_with_overridest_mapt::const_iterator it =
851 if(class_trees.second.front().parsed_class.name.empty())
879 std::vector<irep_idt> methods_to_check;
882 for(
const auto &id_and_symbol : symbol_table)
884 const auto &symbol = id_and_symbol.second;
885 const auto &
id = symbol.name;
888 methods_to_check.push_back(
id);
892 for(
const auto &
id : methods_to_check)
911 if(c.second.front().parsed_class.name.empty())
916 c.second.front().parsed_class.name, symbol_table);
921 <<
"Not marking class " << c.first
922 <<
" implicitly generic due to missing outer class symbols"
940 const std::size_t before_constant_globals_size = symbol_table.
symbols.size();
949 status() <<
"Java: added "
950 << (symbol_table.
symbols.size() - before_constant_globals_size)
951 <<
" String or Class constant symbols"
1008 function_id_and_type.first,
1009 journalling_symbol_table,
1021 for(
const auto &fn_name : journalling_symbol_table.
get_inserted())
1077 "the program has no entry point",
1079 "Check that the specified entry point is included by your "
1080 "--context-include or --context-exclude options");
1085 symbol_table_builder,
1094 return java_build_arguments(
1097 language_options->assume_inputs_non_null,
1098 object_factory_parameters,
1099 get_pointer_type_selector(),
1100 get_message_handler());
1129 symbol_table_builder,
1130 std::move(lazy_methods_needed),
1145 return method_gather(symbol_table,
method_bytecode, method_converter);
1161 std::unordered_set<irep_idt> &methods)
const
1163 const std::string cprover_class_prefix =
"java::org.cprover.CProver.";
1169 methods.insert(kv.first);
1172 methods.insert(kv.first);
1227 const codet &function_body,
1230 if(needed_lazy_methods)
1236 if(it->id() == ID_code)
1238 const auto fn_call = expr_try_dynamic_cast<code_function_callt>(*it);
1242 expr_try_dynamic_cast<symbol_exprt>(fn_call->function());
1244 needed_lazy_methods->add_needed_method(fn_sym->
get_identifier());
1247 it->id() == ID_side_effect &&
1252 expr_try_dynamic_cast<symbol_exprt>(call_expr.function());
1257 "Java synthetic methods are not "
1258 "expected to produce side_effect_expr_function_callt. If "
1259 "that has changed, remove this invariant. Also note that "
1260 "as of the time of writing remove_virtual_functions did "
1261 "not support this form of function call.");
1314 writable_symbol.
value =
1340 const auto &symbol = symbol_table.
lookup_ref(function_id);
1346 synthetic_methods_mapt::iterator synthetic_method_it;
1356 writable_symbol, cmb->get().method.local_variable_table, symbol_table);
1359 codet generated_code =
1364 writable_symbol.
value = std::move(generated_code);
1374 switch(synthetic_method_it->second)
1398 const auto class_name =
1401 class_name,
"user_specified_clinit must be declared by a class.");
1404 "static-values JSON must be available");
1409 needed_lazy_methods,
1416 writable_symbol.
value =
1436 "CProver.createArrayWithType should only be registered if "
1437 "we have a real implementation available");
1439 writable_symbol, cmb->get().method.local_variable_table, symbol_table);
1457 symbol_table.
lookup_ref(cmb->get().class_id),
1463 std::move(needed_lazy_methods),
1472 if(needed_lazy_methods)
1479 type_try_dynamic_cast<pointer_typet>(function_type.
return_type()))
1491 needed_lazy_methods->add_all_needed_classes(*pointer_return_type);
1508 parse_trees.front().output(out);
1509 if(parse_trees.size() > 1)
1511 out <<
"\n\nClass has the following overlays:\n\n";
1512 for(
auto parse_tree_it = std::next(parse_trees.begin());
1513 parse_tree_it != parse_trees.end();
1516 parse_tree_it->output(out);
1518 out <<
"End of class overlays.\n";
1524 return util_make_unique<java_bytecode_languaget>();
1546 const std::string &code,
1547 const std::string &module,
1556 std::istringstream i_preprocessed(code);
1560 java_bytecode_parser.clear();
1561 java_bytecode_parser.filename=
"";
1562 java_bytecode_parser.in=&i_preprocessed;
1564 java_bytecode_parser.grammar=java_bytecode_parsert::EXPRESSION;
1565 java_bytecode_parser.mode=java_bytecode_parsert::GCC;
1566 java_bytecode_scanner_init();
1568 bool result=java_bytecode_parser.parse();
1570 if(java_bytecode_parser.parse_tree.items.empty())
1574 expr=java_bytecode_parser.parse_tree.items.front().value();
1584 java_bytecode_parser.clear();
1605 std::vector<load_extra_methodst>
Class that provides messages with a built-in verbosity 'level'.
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.
jar_poolt jar_pool
a cache for jar_filet, by path name
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
method_bytecodet method_bytecode
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...
#define JAVA_CLASS_MODEL_SUFFIX
@ STATIC_INITIALIZER_WRAPPER
A static initializer wrapper (code of the form if(!already_run) clinit(); already_run = true;) These ...
void convert_synchronized_methods(symbol_tablet &symbol_table, message_handlert &message_handler)
Iterate through the symbol table to find and instrument synchronized methods.
std::set< std::string > extensions() const override
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.
const_depth_iteratort depth_cbegin() const
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
@ LAZY_METHODS_MODE_EAGER
optionalt< prefix_filtert > method_context
If set, method bodies are only elaborated if they pass the filter.
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
Non-graph-based representation of the class hierarchy.
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...
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 parse_java_language_options(const cmdlinet &cmd, optionst &options)
Parse options that are java bytecode specific.
static journalling_symbol_tablet wrap(symbol_table_baset &base_symbol_table)
codet lift_clinit_calls(codet input)
file Static initializer call lifting
virtual bool isset(char option) const
const std::unique_ptr< const select_pointer_typet > pointer_type_selector
Provides filtering of strings vai inclusion/exclusion lists of prefixes.
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.
bool should_lift_clinit_calls
Should we lift clinit calls in function bodies to the top? For example, turning if(x) A....
synthetic_methods_mapt synthetic_methods
Maps synthetic method names on to the particular type of synthetic method (static initializer,...
bool to_expr(const std::string &code, const std::string &module, exprt &expr, const namespacet &ns) override
Parses the given string into an expression.
The type of an expression, extends irept.
const std::string get_option(const std::string &option) const
mstreamt & status() const
java_bytecode_language_optionst()=default
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.
typet type
Type of symbol.
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...
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.
Represents the argument of an instruction that uses a CONSTANT_Fieldref This is used for example as a...
Process a pattern to use as a regex for selecting extra entry points for ci_lazy_methodst.
optionalt< std::reference_wrapper< const class_method_and_bytecodet > > opt_reft
optionalt< java_bytecode_language_optionst > language_options
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)
optionalt< irep_idt > declaring_class(const symbolt &symbol)
Gets the identifier of the class which declared a given symbol.
std::vector< irep_idt > load_entire_jar(const std::string &jar_path)
Load all class files from a .jar file.
std::unique_ptr< languaget > new_java_bytecode_language()
optionalt< std::string > main
Representation of a constant Java string.
opt_reft get(const irep_idt &method_id)
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.
@ INVOKEDYNAMIC_CAPTURE_CONSTRUCTOR
A generated constructor for a class capturing the parameters of an invokedynamic instruction.
@ INVOKEDYNAMIC_METHOD
A generated method for a class capturing the parameters of an invokedynamic instruction.
Base class for all expressions.
bool implements_function(const irep_idt &function_id) const
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.
irep_idt base_name
Base (non-scoped) name.
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...
std::unordered_map< std::string, object_creation_referencet > references
Map used in all calls to functions that deterministically create objects (currently only assign_from_...
A struct tag type, i.e., struct_typet with an identifier.
bool from_type(const typet &type, std::string &code, const namespacet &ns) override
Formats the given type in a language-specific way.
void convert_threadblock(symbol_tablet &symbol_table)
Iterate through the symbol table to find and appropriately instrument thread-blocks.
Thrown when we can't handle something in an input source file.
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
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)
void initialize_known_type_table()
void set_option(const std::string &option, const bool value)
irep_idt component_name() const
side_effect_exprt & to_side_effect_expr(exprt &expr)
std::function< bool(const irep_idt &function_id, ci_lazy_methods_neededt)> method_convertert
json_arrayt & to_json_array(jsont &json)
Expression to hold a symbol (variable)
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.
bool has_suffix(const std::string &s, const std::string &suffix)
virtual bool final(symbol_table_baset &context) override
Final adjustments, e.g.
std::unordered_multimap< irep_idt, symbolt > class_to_declared_symbols(const symbol_tablet &symbol_table)
An exception that is raised checking whether a class is implicitly generic if a symbol for an outer c...
void set(const optionst &)
Assigns the parameters from given options.
virtual iteratort begin() override
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...
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.
stub_global_initializer_factoryt stub_global_initializer_factory
irep_idt pretty_name
Language-specific display name.
const codet & to_code(const exprt &expr)
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.
lazy_methods_modet lazy_methods_mode
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
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...
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...
typet & type()
Return the type of the expression.
bool can_cast_type< code_typet >(const typet &type)
Check whether a reference to a typet is a code_typet.
void set_language_options(const optionst &) override
Consume options that are java bytecode specific.
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.
irep_idt mode
Language mode.
mstreamt & result() const
std::list< java_bytecode_parse_treet > parse_tree_with_overlayst
A list of parse trees supporting overlay classes.
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::vector< irep_idt > main_jar_classes
@ USER_SPECIFIED_STATIC_INITIALIZER
Only exists if the --static-values option was used.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
virtual iteratort end() override
The null pointer constant.
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
const std::string & id2string(const irep_idt &d)
virtual ~java_bytecode_languaget()
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.
java_class_loadert java_class_loader
bool ignore_manifest_main_class
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.
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.
bool is_set(const std::string &option) const
N.B. opts.is_set("foo") does not imply opts.get_bool_option("foo")
#define PRECONDITION(CONDITION)
const irep_idt & get_identifier() const
The symbol table base class interface.
bool do_ci_lazy_method_conversion(symbol_tablet &)
Uses a simple context-insensitive ('ci') analysis to determine which methods may be reachable from th...
void get_all_function_names(std::unordered_set< irep_idt > &methods) const
Implementation of CProver.createArrayWithType intrinsic.
void show_parse(std::ostream &out) override
codet code_for_function(const symbolt &symbol, symbol_table_baset &symbol_table)
Should be called to provide code for string functions that are used in the code but for which no impl...
std::vector< irep_idt > java_load_classes
list of classes to force load even without reference from the entry point
prefix_filtert get_context(const optionst &options)
bool generate_support_functions(symbol_tablet &symbol_table) override
Create language-specific support functions, such as __CPROVER_start, __CPROVER_initialize and languag...
#define INITIALIZE_FUNCTION
std::string get_value(char option) const
void initialize_class_loader()
virtual void set_message_handler(message_handlert &_message_handler)
const basest & bases() const
Get the collection of base classes/structs.
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 ...
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 add_classpath_entry(const std::string &)
Appends an entry to the class path, used for loading classes.
virtual bool parse()
We set the main class (i.e. class to start the class loading analysis, see java_class_loadert) when w...
void java_bytecode_typecheck_updated_symbols(journalling_symbol_tablet &symbol_table, message_handlert &message_handler, bool string_refinement_enabled)
bool has_component(const irep_idt &component_name) const
static void throwMainClassLoadingError(const std::string &main_class)
const irep_idt & id() const
std::vector< irep_idt > idst
JAVA Bytecode Language Conversion.
std::string java_cp_include_files
void modules_provided(std::set< std::string > &modules) override
java_string_library_preprocesst string_preprocess
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
bool assert_no_exceptions_thrown
Transform athrow bytecode instructions into assert FALSE followed by assume FALSE.
bool can_load_class(const irep_idt &class_name)
Checks whether class_name is parseable from the classpath, ignoring class loading limits.
nonstd::optional< T > optionalt
void set_extra_class_refs_function(get_extra_class_refs_functiont func)
Sets a function that provides extra dependencies for a particular class.
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__...
unsigned int get_unsigned_int_option(const std::string &option) const
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.
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...
Collect methods needed to be loaded using the lazy method.
std::unordered_multimap< irep_idt, symbolt > & get(const symbol_tablet &symbol_table)
@ CREATE_ARRAY_WITH_TYPE
Our internal implementation of CProver.createArrayWithType, which needs to access internal type-id fi...
bool assume_inputs_non_null
assume inputs variables to be non-null
const irep_idt & get_statement() const
codet invokedynamic_synthetic_constructor(const irep_idt &function_id, symbol_table_baset &symbol_table, message_handlert &message_handler)
Create invokedynamic synthetic constructor.
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.
Class representing a filter for class file loading.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
bool from_expr(const exprt &expr, std::string &code, const namespacet &ns) override
Formats the given expression in a language-specific way.
Java lambda code synthesis.
const componentst & components() const
exprt value
Initial value of symbol.
message_handlert & get_message_handler()
const select_pointer_typet & get_pointer_type_selector() const
class_hierarchyt class_hierarchy
void java_internal_additions(symbol_table_baset &dest)
irep_idt class_name() const
@ STUB_CLASS_STATIC_INITIALIZER
A generated (synthetic) static initializer function for a stub type.
message_handlert * message_handler
bool typecheck(symbol_tablet &context, const std::string &module) override
optionalt< json_objectt > static_values_json
JSON which contains initial values of static fields (right after the static initializer of the class ...
Forward depth-first search iterators These iterators' copy operations are expensive,...
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 set_message_handler(message_handlert &message_handler) override
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...
json_objectt & to_json_object(jsont &json)
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
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.
const irep_idt & get(const irep_namet &name) const
const_depth_iteratort depth_cend() const
source_locationt location
Source code location of definition of symbol.
fixed_keys_map_wrappert< parse_tree_with_overridest_mapt > get_class_with_overlays_map()
Map from class names to the bytecode parse trees.
const std::vector< std::string > exception_needed_classes
void set(const irep_namet &name, const irep_idt &value)
static symbol_table_buildert wrap(symbol_table_baset &base_symbol_table)
std::string id() const override
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.
bool get_bool_option(const std::string &option) const
bool throw_runtime_exceptions
const symbolst & symbols
Read-only field, used to look up symbols given their names.
std::vector< load_extra_methodst > extra_methods
bool assert_uncaught_exceptions
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.
bool throw_assertion_error
struct configt::javat java
std::string type2java(const typet &type, const namespacet &ns)
@ LAZY_METHODS_MODE_CONTEXT_INSENSITIVE
java_object_factory_parameterst object_factory_parameters
std::string expr2java(const exprt &expr, const namespacet &ns)
Map classes to the symbols they declare but is only computed once it is needed and the map is then ke...
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
const typet & return_type() const
bool has_prefix(const std::string &s, const std::string &prefix)
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 initialize_conversion_table()
fill maps with correspondence from java method names to conversion functions
bool java_bytecode_typecheck(symbol_table_baset &symbol_table, message_handlert &message_handler, bool string_refinement_enabled)
const java_class_typet & to_java_class_type(const typet &type)
void parse_from_main_class()
const changesett & get_inserted() const
void clear_classpath()
Clear all classpath entries.
std::unordered_set< std::string > no_load_classes
List of classes to never load.
Operator to return the address of an object.
void convert_single_method(const irep_idt &function_id, symbol_table_baset &symbol_table, lazy_class_to_declared_symbols_mapt &class_to_declared_symbols)
const java_method_typet & to_java_method_type(const typet &type)
bool string_refinement_enabled
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
struct bytecode_infot const bytecode_info[]
@ LAZY_METHODS_MODE_EXTERNAL_DRIVER
mstreamt & warning() const
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
virtual bool preprocess(std::istream &instream, const std::string &path, std::ostream &outstream) override
ANSI-C preprocessing.
const std::list< std::string > & get_values(const std::string &option) const
bool parse_json(std::istream &in, const std::string &filename, message_handlert &message_handler, jsont &dest)
A symbol table wrapper that records which entries have been updated/removedA caller can pass a journa...
const value_listt & get_list_option(const std::string &option) const
irep_idt name
The unique identifier.
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 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...
std::unordered_multimap< irep_idt, symbolt > map
JAVA Bytecode Language Type Checking.
JAVA Bytecode Language Conversion.
size_t max_user_array_length
max size for user code created arrays
Data structure for representing an arbitrary statement in a program.
irep_idt get_create_array_with_type_name()
Returns the symbol name for org.cprover.CProver.createArrayWithType