53 if(cmd.
isset(
"java-max-input-array-length"))
55 std::stoi(cmd.
get_value(
"java-max-input-array-length"));
56 if(cmd.
isset(
"java-max-input-tree-depth"))
58 std::stoi(cmd.
get_value(
"java-max-input-tree-depth"));
59 if(cmd.
isset(
"string-max-input-length"))
61 std::stoi(cmd.
get_value(
"string-max-input-length"));
62 else if(cmd.
isset(
"string-max-length"))
64 std::stoi(cmd.
get_value(
"string-max-length"));
67 if(cmd.
isset(
"java-max-vla-length"))
69 if(cmd.
isset(
"symex-driven-lazy-loading"))
71 else if(cmd.
isset(
"lazy-methods"))
83 if(cmd.
isset(
"java-load-class"))
85 const auto &values = cmd.
get_values(
"java-load-class");
89 if(cmd.
isset(
"java-no-load-class"))
91 const auto &values = cmd.
get_values(
"java-no-load-class");
95 const std::list<std::string> &extra_entry_points=
96 cmd.
get_values(
"lazy-methods-extra-entry-point");
99 extra_entry_points.begin(),
100 extra_entry_points.end());
102 if(cmd.
isset(
"java-cp-include-files"))
108 jsont json_cp_config;
113 throw "cannot read JSON input configuration for JAR loading";
116 throw "the JSON file has a wrong format";
117 jsont include_files=json_cp_config[
"jar"];
119 throw "the JSON file has a wrong format";
122 for(
const jsont &file_entry : include_files.
array)
126 "classpath entry must be jar filename, but '" + file_entry.
value +
140 return {
"class",
"jar" };
150 std::istream &instream,
151 const std::string &path,
152 std::ostream &outstream)
159 std::istream &instream,
160 const std::string &path)
170 auto get_string_base_classes = [
this](
const irep_idt &
id) {
193 std::string manifest_main_class=manifest[
"Main-Class"];
196 if(manifest_main_class!=
"")
205 status() <<
"JAR file without entry point: loading class files" <<
eom;
243 if(instruction.
statement ==
"getfield" ||
246 const exprt &fieldref = instruction.
args[0];
248 const symbolt *class_symbol = symbol_table.
lookup(class_symbol_id);
250 class_symbol !=
nullptr,
251 "all types containing fields should have been loaded");
254 const irep_idt &component_name = fieldref.
get(ID_component_name);
257 if(class_type->
get_bool(ID_incomplete_class))
260 symbolt &writable_class_symbol =
264 components.emplace_back(component_name, fieldref.
type());
265 components.back().set_base_name(component_name);
266 components.back().set_pretty_name(component_name);
273 !class_type->
bases().empty(),
275 +
"' (which was missing a field '" +
id2string(component_name)
276 +
"' referenced from method '" +
id2string(method.name)
277 +
"') should have an opaque superclass");
280 class_symbol_id = superclass_type.get_identifier();
305 new_class_symbol.
type = symbol_expr.
type();
308 "class identifier should have 'java::' prefix");
311 new_class_symbol.
mode = ID_java;
315 symbol_table.
add(new_class_symbol);
336 const exprt &ldc_arg0,
338 bool string_refinement_enabled)
340 if(ldc_arg0.
id() == ID_type)
347 else if(ldc_arg0.
id() == ID_java_string_literal)
352 ldc_arg0, symbol_table, string_refinement_enabled));
357 ldc_arg0.
id() == ID_constant,
358 "ldc argument should be constant, string literal or class literal");
375 bool string_refinement_enabled)
390 instruction.
args.size() != 0,
391 "ldc instructions should have an argument");
392 instruction.
args[0] =
396 string_refinement_enabled);
417 const typet &symbol_type,
419 bool force_nondet_init)
425 new_symbol.
name = symbol_id;
427 new_symbol.
type = symbol_type;
428 new_symbol.
type.
set(ID_C_class, class_id);
432 new_symbol.
type.
set(ID_C_access, ID_public);
434 new_symbol.
mode = ID_java;
439 if(symbol_type.
id() == ID_pointer && !force_nondet_init)
443 bool add_failed = symbol_table.
add(new_symbol);
445 !add_failed,
"caller should have checked symbol not already in table");
463 std::vector<irep_idt> classes_to_check;
464 classes_to_check.push_back(start_class_id);
466 while(!classes_to_check.empty())
468 irep_idt to_check = classes_to_check.back();
469 classes_to_check.pop_back();
473 to_check !=
"java::java.lang.Object")
479 class_hierarchy.
class_map.at(to_check).parents;
480 classes_to_check.insert(
481 classes_to_check.end(), parents.begin(), parents.end());
508 if(instruction.
statement ==
"getstatic" ||
512 instruction.
args.size() > 0,
513 "get/putstatic should have at least one argument");
514 irep_idt component = instruction.
args[0].get_string(ID_component_name);
516 !component.empty(),
"get/putstatic should specify a component");
517 irep_idt class_id = instruction.
args[0].get_string(ID_class);
519 !class_id.empty(),
"get/putstatic should specify a class");
531 if(!referred_component.is_valid())
538 class_id, symbol_table, class_hierarchy);
550 bool no_incomplete_ancestors = add_to_class_id.
empty();
551 if(no_incomplete_ancestors)
553 add_to_class_id = class_id;
557 log.
warning() <<
"Stub static field " << component <<
" found for " 558 <<
"non-stub type " << class_id <<
". In future this " 569 instruction.
args[0].type(),
571 no_incomplete_ancestors);
580 const std::string &module)
592 java_class_loadert::parse_tree_with_overridest_mapt::const_iterator it =
614 if(class_trees.second.front().parsed_class.name.empty())
639 if(c.second.front().parsed_class.name.empty())
644 c.second.front().parsed_class.name, symbol_table);
649 <<
"Not marking class " << c.first
650 <<
" implicitly generic due to missing outer class symbols" 668 const std::size_t before_constant_globals_size = symbol_table.
symbols.size();
677 status() <<
"Java: added " 678 << (symbol_table.
symbols.size() - before_constant_globals_size)
679 <<
" String or Class constant symbols" 692 journalling_symbol_tablet symbol_table_journal =
693 journalling_symbol_tablet::wrap(symbol_table);
723 journalling_symbol_tablet journalling_symbol_table =
724 journalling_symbol_tablet::wrap(symbol_table);
730 function_id_and_type.first, journalling_symbol_table);
738 for(
const auto &fn_name : journalling_symbol_table.get_inserted())
807 [
this, &symbol_table]
811 function_id, symbol_table, std::move(lazy_methods_needed));
841 std::unordered_set<irep_idt> &methods)
const 843 static std::string cprover_class_prefix =
"java::org.cprover.CProver.";
850 const std::string &method_id =
id2string(kv.first);
855 if(
has_prefix(method_id, cprover_class_prefix))
857 std::size_t method_name_end_offset =
858 method_id.find(
':', cprover_class_prefix.length());
860 method_name_end_offset != std::string::npos,
861 "org.cprover.CProver method should have a postfix type descriptor");
863 const std::string method_name =
865 cprover_class_prefix.length(),
866 method_name_end_offset - cprover_class_prefix.length());
871 methods.insert(kv.first);
875 methods.insert(kv.first);
894 journalling_symbol_tablet symbol_table=
895 journalling_symbol_tablet::wrap(symtab);
904 symbol_table.get_writeable_ref(function_id),
921 const exprt &function_body,
924 if(needed_lazy_methods)
930 if(it->id() == ID_code)
970 synthetic_methods_mapt::iterator synthetic_method_it;
980 symbol, cmb->get().method.local_variable_table, symbol_table);
983 exprt generated_code =
986 generated_code.
is_not_nil(),
"Couldn't retrieve code for string method");
990 symbol.
value = generated_code;
1000 switch(synthetic_method_it->second)
1005 function_id, symbol_table);
1029 symbol_table.
lookup_ref(cmb->get().class_id),
1035 std::move(needed_lazy_methods),
1046 type_try_dynamic_cast<pointer_typet>(function_type.
return_type()))
1058 needed_lazy_methods->add_all_needed_classes(*pointer_return_type);
1074 parse_trees.front().output(out);
1075 if(parse_trees.size() > 1)
1077 out <<
"\n\nClass has the following overlays:\n\n";
1078 for(
auto parse_tree_it = std::next(parse_trees.begin());
1079 parse_tree_it != parse_trees.end();
1082 parse_tree_it->output(out);
1084 out <<
"End of class overlays.\n";
1090 return util_make_unique<java_bytecode_languaget>();
1112 const std::string &code,
1113 const std::string &module,
1122 std::istringstream i_preprocessed(code);
1126 java_bytecode_parser.clear();
1127 java_bytecode_parser.filename=
"";
1128 java_bytecode_parser.in=&i_preprocessed;
1130 java_bytecode_parser.grammar=java_bytecode_parsert::EXPRESSION;
1131 java_bytecode_parser.mode=java_bytecode_parsert::GCC;
1132 java_bytecode_scanner_init();
1134 bool result=java_bytecode_parser.parse();
1136 if(java_bytecode_parser.parse_tree.items.empty())
1140 expr=java_bytecode_parser.parse_tree.items.front().value();
1150 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
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
irep_idt mode
Language mode.
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
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 convert_threadblock(symbol_tablet &symbol_table)
Iterate through the symbol table to find and appropriately instrument thread-blocks.
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)
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
std::vector< irep_idt > lazy_methods_extra_entry_points
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 &)
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...
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)
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.
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...
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()
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.
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...
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 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...
resolve_inherited_componentt::inherited_componentt get_inherited_component(const irep_idt &component_class_id, const irep_idt &component_name, const irep_idt &user_class_id, 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.
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