50 cmd.
isset(
"java-throw-runtime-exceptions") ||
51 cmd.
isset(
"throw-runtime-exceptions");
56 if(cmd.
isset(
"java-max-input-array-length"))
61 if(cmd.
isset(
"max-nondet-array-length"))
67 if(cmd.
isset(
"java-max-input-tree-depth"))
72 if(cmd.
isset(
"max-nondet-tree-depth"))
78 if(cmd.
isset(
"string-max-input-length"))
83 if(cmd.
isset(
"max-nondet-string-length"))
90 if(cmd.
isset(
"java-max-vla-length"))
93 if(cmd.
isset(
"symex-driven-lazy-loading"))
95 else if(!cmd.
isset(
"no-lazy-methods"))
107 if(cmd.
isset(
"java-load-class"))
109 const auto &values = cmd.
get_values(
"java-load-class");
113 if(cmd.
isset(
"java-no-load-class"))
115 const auto &values = cmd.
get_values(
"java-no-load-class");
119 const std::list<std::string> &extra_entry_points=
120 cmd.
get_values(
"lazy-methods-extra-entry-point");
122 extra_entry_points.begin(),
123 extra_entry_points.end(),
127 if(cmd.
isset(
"java-cp-include-files"))
133 jsont json_cp_config;
138 throw "cannot read JSON input configuration for JAR loading";
141 throw "the JSON file has a wrong format";
142 jsont include_files=json_cp_config[
"jar"];
144 throw "the JSON file has a wrong format";
147 for(
const jsont &file_entry : include_files.
array)
151 "classpath entry must be jar filename, but '" + file_entry.
value +
165 return {
"class",
"jar" };
185 const std::string &path)
195 auto get_string_base_classes = [
this](
const irep_idt &
id) {
218 std::string manifest_main_class=manifest[
"Main-Class"];
221 if(manifest_main_class!=
"")
230 status() <<
"JAR file without entry point: loading class files" <<
eom;
268 if(instruction.
statement ==
"getfield" ||
271 const exprt &fieldref = instruction.
args[0];
273 const symbolt *class_symbol = symbol_table.
lookup(class_symbol_id);
275 class_symbol !=
nullptr,
276 "all types containing fields should have been loaded");
279 const irep_idt &component_name = fieldref.
get(ID_component_name);
282 if(class_type->
get_bool(ID_incomplete_class))
285 symbolt &writable_class_symbol =
289 components.emplace_back(component_name, fieldref.
type());
290 components.back().set_base_name(component_name);
291 components.back().set_pretty_name(component_name);
298 !class_type->
bases().empty(),
300 +
"' (which was missing a field '" +
id2string(component_name)
301 +
"' referenced from method '" +
id2string(method.name)
302 +
"') should have an opaque superclass");
305 class_symbol_id = superclass_type.get_identifier();
330 new_class_symbol.
type = symbol_expr.
type();
333 "class identifier should have 'java::' prefix");
336 new_class_symbol.
mode = ID_java;
340 symbol_table.
add(new_class_symbol);
361 const exprt &ldc_arg0,
363 bool string_refinement_enabled)
365 if(ldc_arg0.
id() == ID_type)
372 else if(ldc_arg0.
id() == ID_java_string_literal)
377 ldc_arg0, symbol_table, string_refinement_enabled));
382 ldc_arg0.
id() == ID_constant,
383 "ldc argument should be constant, string literal or class literal");
400 bool string_refinement_enabled)
415 instruction.
args.size() != 0,
416 "ldc instructions should have an argument");
417 instruction.
args[0] =
421 string_refinement_enabled);
442 const typet &symbol_type,
444 bool force_nondet_init)
450 new_symbol.
name = symbol_id;
452 new_symbol.
type = symbol_type;
453 new_symbol.
type.
set(ID_C_class, class_id);
457 new_symbol.
type.
set(ID_C_access, ID_public);
459 new_symbol.
mode = ID_java;
464 if(symbol_type.
id() == ID_pointer && !force_nondet_init)
468 bool add_failed = symbol_table.
add(new_symbol);
470 !add_failed,
"caller should have checked symbol not already in table");
488 std::vector<irep_idt> classes_to_check;
489 classes_to_check.push_back(start_class_id);
491 while(!classes_to_check.empty())
493 irep_idt to_check = classes_to_check.back();
494 classes_to_check.pop_back();
498 to_check !=
"java::java.lang.Object")
504 class_hierarchy.
class_map.at(to_check).parents;
505 classes_to_check.insert(
506 classes_to_check.end(), parents.begin(), parents.end());
533 if(instruction.
statement ==
"getstatic" ||
537 instruction.
args.size() > 0,
538 "get/putstatic should have at least one argument");
539 irep_idt component = instruction.
args[0].get_string(ID_component_name);
541 !component.empty(),
"get/putstatic should specify a component");
542 irep_idt class_id = instruction.
args[0].get_string(ID_class);
544 !class_id.empty(),
"get/putstatic should specify a class");
555 if(!referred_component.is_valid())
562 class_id, symbol_table, class_hierarchy);
574 bool no_incomplete_ancestors = add_to_class_id.
empty();
575 if(no_incomplete_ancestors)
577 add_to_class_id = class_id;
581 log.
warning() <<
"Stub static field " << component <<
" found for " 582 <<
"non-stub type " << class_id <<
". In future this " 593 instruction.
args[0].type(),
595 no_incomplete_ancestors);
616 java_class_loadert::parse_tree_with_overridest_mapt::const_iterator it =
638 if(class_trees.second.front().parsed_class.name.empty())
663 if(c.second.front().parsed_class.name.empty())
668 c.second.front().parsed_class.name, symbol_table);
673 <<
"Not marking class " << c.first
674 <<
" implicitly generic due to missing outer class symbols" 692 const std::size_t before_constant_globals_size = symbol_table.
symbols.size();
701 status() <<
"Java: added " 702 << (symbol_table.
symbols.size() - before_constant_globals_size)
703 <<
" String or Class constant symbols" 716 journalling_symbol_tablet symbol_table_journal =
717 journalling_symbol_tablet::wrap(symbol_table);
747 journalling_symbol_tablet journalling_symbol_table =
748 journalling_symbol_tablet::wrap(symbol_table);
754 function_id_and_type.first, journalling_symbol_table);
762 for(
const auto &fn_name : journalling_symbol_table.get_inserted())
834 [
this, &symbol_table]
838 function_id, symbol_table, std::move(lazy_methods_needed));
868 std::unordered_set<irep_idt> &methods)
const 870 const std::string cprover_class_prefix =
"java::org.cprover.CProver.";
877 const std::string &method_id =
id2string(kv.first);
882 if(
has_prefix(method_id, cprover_class_prefix))
884 std::size_t method_name_end_offset =
885 method_id.find(
':', cprover_class_prefix.length());
887 method_name_end_offset != std::string::npos,
888 "org.cprover.CProver method should have a postfix type descriptor");
890 const std::string method_name =
892 cprover_class_prefix.length(),
893 method_name_end_offset - cprover_class_prefix.length());
898 methods.insert(kv.first);
902 methods.insert(kv.first);
921 journalling_symbol_tablet symbol_table=
922 journalling_symbol_tablet::wrap(symtab);
931 symbol_table.get_writeable_ref(function_id),
948 const exprt &function_body,
951 if(needed_lazy_methods)
957 if(it->id() == ID_code)
997 synthetic_methods_mapt::iterator synthetic_method_it;
1007 symbol, cmb->get().method.local_variable_table, symbol_table);
1010 exprt generated_code =
1013 generated_code.
is_not_nil(),
"Couldn't retrieve code for string method");
1017 symbol.
value = generated_code;
1027 switch(synthetic_method_it->second)
1032 function_id, symbol_table);
1056 symbol_table.
lookup_ref(cmb->get().class_id),
1062 std::move(needed_lazy_methods),
1074 type_try_dynamic_cast<pointer_typet>(function_type.
return_type()))
1086 needed_lazy_methods->add_all_needed_classes(*pointer_return_type);
1102 parse_trees.front().output(out);
1103 if(parse_trees.size() > 1)
1105 out <<
"\n\nClass has the following overlays:\n\n";
1106 for(
auto parse_tree_it = std::next(parse_trees.begin());
1107 parse_tree_it != parse_trees.end();
1110 parse_tree_it->output(out);
1112 out <<
"End of class overlays.\n";
1118 return util_make_unique<java_bytecode_languaget>();
1140 const std::string &code,
1141 const std::string &module,
1150 std::istringstream i_preprocessed(code);
1154 java_bytecode_parser.clear();
1155 java_bytecode_parser.filename=
"";
1156 java_bytecode_parser.in=&i_preprocessed;
1158 java_bytecode_parser.grammar=java_bytecode_parsert::EXPRESSION;
1159 java_bytecode_parser.mode=java_bytecode_parsert::GCC;
1160 java_bytecode_scanner_init();
1162 bool result=java_bytecode_parser.parse();
1164 if(java_bytecode_parser.parse_tree.items.empty())
1168 expr=java_bytecode_parser.parse_tree.items.front().value();
1178 java_bytecode_parser.clear();
std::vector< irep_idt > java_load_classes
The type of an expression.
irep_idt name
The unique identifier.
const std::list< std::string > & get_values(const std::string &option) const
std::string type2java(const typet &type, const namespacet &ns)
void create_static_initializer_wrappers(symbol_tablet &symbol_table, synthetic_methods_mapt &synthetic_methods, const bool thread_safe)
Create static initializer wrappers for all classes that need them.
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.
optionalt< std::reference_wrapper< const class_method_and_bytecodet > > opt_reft
void java_bytecode_typecheck_updated_symbols(journalling_symbol_tablet &symbol_table, message_handlert &message_handler, bool string_refinement_enabled)
bool throw_assertion_error
A static initializer wrapper (code of the form if(!already_run) clinit(); already_run = true;) These ...
const std::string & id2string(const irep_idt &d)
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
const jar_indext & get_jar_index(const std::string &jar_path)
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...
const_depth_iteratort depth_cbegin() const
Non-graph-based representation of the class hierarchy.
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.
java_class_loadert java_class_loader
bool assert_uncaught_exceptions
std::function< bool(const irep_idt &function_id, ci_lazy_methods_neededt)> method_convertert
Process a pattern to use as a regex for selecting extra entry points for ci_lazy_methodst.
irep_idt mode
Language mode.
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 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...
std::string java_cp_include_files
void modules_provided(std::set< std::string > &modules) override
const irep_idt & get_identifier() const
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
bool java_bytecode_typecheck(symbol_table_baset &symbol_table, message_handlert &message_handler, bool string_refinement_enabled)
std::size_t safe_string2size_t(const std::string &str, int base)
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
The null pointer constant.
exprt value
Initial value of symbol.
const componentst & components() const
std::string get_value(char option) const
jar_filet & jar_pool(java_class_loader_limitt &limit, const std::string &filename)
Load jar archive or retrieve from cache if already loaded.
codet get_thread_safe_clinit_wrapper_body(const irep_idt &function_id, symbol_table_baset &symbol_table)
Thread safe version of the static initialiser.
size_t max_user_array_length
irep_idt pretty_name
Language-specific display name.
const select_pointer_typet & get_pointer_type_selector() const
const class_typet & to_class_type(const typet &type)
Cast a generic typet to a class_typet.
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
java_string_library_preprocesst string_preprocess
void show_parse(std::ostream &out) override
auto expr_dynamic_cast(TExpr &base) -> typename detail::expr_dynamic_cast_return_typet< T, TExpr >::type
Cast a reference to a generic exprt to a specific derived class.
void initialize_conversion_table()
fill maps with correspondence from java method names to conversion functions
static mstreamt & eom(mstreamt &m)
class_hierarchyt class_hierarchy
bool get_bool(const irep_namet &name) const
codet get_clinit_wrapper_body(const irep_idt &function_id, symbol_table_baset &symbol_table)
Produces the static initialiser wrapper body for the given function.
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...
bool parse_json(std::istream &in, const std::string &filename, message_handlert &message_handler, jsont &dest)
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...
std::list< java_bytecode_parse_treet > parse_tree_with_overlayst
#define INVARIANT(CONDITION, REASON)
void load_entire_jar(java_class_loader_limitt &, const std::string &jar_path)
object_factory_parameterst object_factory_parameters
mstreamt & warning() const
bool from_expr(const exprt &expr, std::string &code, const namespacet &ns) override
Formats the given expression in a language-specific way.
bool assume_inputs_non_null
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 ...
JAVA Bytecode Language Type Checking.
const irep_idt & id() const
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.
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...
std::set< std::string > extensions() const override
virtual bool isset(char option) const
static std::string file_to_class_name(const std::string &)
void convert_synchronized_methods(symbol_tablet &symbol_table, message_handlert &message_handler)
Iterate through the symbol table to find and instrument synchronized methods.
A reference into the symbol table.
size_t max_nondet_tree_depth
Maximum depth for object hierarchy on input.
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...
resolve_inherited_componentt::inherited_componentt get_inherited_component(const irep_idt &component_class_id, const irep_idt &component_name, const symbol_tablet &symbol_table, const class_hierarchyt &class_hierarchy, bool include_interfaces)
Finds an inherited component (method or field), taking component visibility into account.
void get_all_function_names(std::unordered_set< irep_idt > &methods) const
static void notify_static_method_calls(const exprt &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...
JAVA Bytecode Language Conversion.
bool string_printable
Force string content to be ASCII printable characters when set to true.
virtual void get_language_options(const cmdlinet &) override
Consume options that are java bytecode specific.
fixed_keys_map_wrappert< parse_tree_with_overridest_mapt > get_class_with_overlays_map()
Map from class names to the bytecode parse trees.
void add_jar_file(const std::string &f)
bool typecheck(symbol_tablet &context, const std::string &module) override
void set_java_cp_include_files(const std::string &java_cp_include_files)
nonstd::optional< T > optionalt
virtual bool preprocess(std::istream &instream, const std::string &path, std::ostream &outstream) override
ANSI-C preprocessing.
const irep_idt & get(const irep_namet &name) const
Collect methods needed to be loaded using the lazy method.
std::vector< load_extra_methodst > extra_methods
codet get_stub_initializer_body(const irep_idt &function_id, symbol_table_baset &symbol_table, const object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector)
Create the body of a synthetic static initializer (clinit method), which initialise stub globals in t...
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)
std::string id() const override
#define PRECONDITION(CONDITION)
std::unique_ptr< languaget > new_java_bytecode_language()
bool has_prefix(const std::string &s, const std::string &prefix)
const std::unordered_set< std::string > cprover_methods_to_ignore
Methods belonging to the class org.cprover.CProver that should be ignored (not converted), leaving the driver program to stub them if it wishes.
virtual void set_message_handler(message_handlert &_message_handler)
struct configt::javat java
const typet & follow(const typet &) const
synthetic_methods_mapt synthetic_methods
Maps synthetic method names on to the particular type of synthetic method (static initializer...
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
void initialize_known_type_table()
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Operator to return the address of an object.
bool language_options_initialized
bool to_expr(const std::string &code, const std::string &module, exprt &expr, const namespacet &ns) override
Parses the given string into an expression.
bool from_type(const typet &type, std::string &code, const namespacet &ns) override
Formats the given type in a language-specific way.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
bool implements_function(const irep_idt &function_id) const
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...
bool has_component(const irep_idt &component_name) const
An exception that is raised checking whether a class is implicitly generic if a symbol for an outer c...
std::vector< irep_idt > idst
const std::unique_ptr< const select_pointer_typet > pointer_type_selector
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.
std::unordered_set< std::string > no_load_classes
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.
method_bytecodet method_bytecode
typet type
Type of symbol.
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...
message_handlert & get_message_handler()
bool do_ci_lazy_method_conversion(symbol_tablet &, method_bytecodet &)
Uses a simple context-insensitive ('ci') analysis to determine which methods may be reachable from th...
const java_method_typet & to_java_method_type(const typet &type)
size_t max_nondet_array_length
Maximum value for the non-deterministically-chosen length of an array.
mstreamt & result() const
mstreamt & status() const
void set_extra_class_refs_function(get_extra_class_refs_functiont func)
Sets a function that provides extra dependencies for a particular class.
exprt 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...
Base class for all expressions.
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.
size_t max_nondet_string_length
Maximum value for the non-deterministically-chosen length of a string.
bool parse(std::istream &instream, const std::string &path) override
irep_idt base_name
Base (non-scoped) name.
The symbol table base class interface.
const std::vector< std::string > exception_needed_classes
#define JAVA_CLASS_MODEL_SUFFIX
const_depth_iteratort depth_cend() const
symbol_exprt get_or_create_string_literal_symbol(const 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 basest & bases() const
void convert_threadblock(symbol_tablet &symbol_table)
Iterate through the symbol table to find and appropriately instrument thread-blocks.
void java_internal_additions(symbol_table_baset &dest)
Expression to hold a symbol (variable)
bool string_refinement_enabled
A generated (synthetic) static initializer function for a stub type.
bool has_suffix(const std::string &s, const std::string &suffix)
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
const pointer_typet & to_pointer_type(const typet &type)
Cast a generic typet to a pointer_typet.
lazy_methods_modet lazy_methods_mode
bool generate_support_functions(symbol_tablet &symbol_table) override
Create language-specific support functions, such as __CPROVER_start, __CPROVER_initialize and languag...
opt_reft get(const irep_idt &method_id)
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...
JAVA Bytecode Language Conversion.
#define DATA_INVARIANT(CONDITION, REASON)
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...
stub_global_initializer_factoryt stub_global_initializer_factory
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
message_handlert * message_handler
std::unordered_map< std::string, std::string > get_manifest()
Get contents of the Manifest file in the jar archive.
const typet & return_type() const
const java_class_typet & to_java_class_type(const typet &type)
virtual bool final(symbol_table_baset &context) override
Final adjustments, e.g.
std::vector< irep_idt > main_jar_classes
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 set(const irep_namet &name, const irep_idt &value)
std::string expr2java(const exprt &expr, const namespacet &ns)
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 object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector, bool string_refinement_enabled)
Given the symbol_table and the main_class to test, this function generates a new function __CPROVER__...
void convert_single_method(const irep_idt &function_id, symbol_table_baset &symbol_table)
auto expr_try_dynamic_cast(TExpr &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TExpr >::type
Try to cast a reference to a generic exprt to a specific derived class.
virtual ~java_bytecode_languaget()
bool throw_runtime_exceptions