cprover
|
#include "java_types.h"
#include <unordered_set>
#include <util/message.h>
#include <util/std_expr.h>
#include <util/symbol_table.h>
#include <goto-programs/resolve_inherited_component.h>
Go to the source code of this file.
Macros | |
#define | JAVA_STRING_LITERAL_PREFIX "java::java.lang.String.Literal" |
Functions | |
bool | java_is_array_type (const typet &type) |
void | generate_class_stub (const irep_idt &class_name, symbol_table_baset &symbol_table, message_handlert &message_handler, const struct_union_typet::componentst &componentst) |
unsigned | java_local_variable_slots (const typet &t) |
Returns the number of JVM local variables (slots) taken by a local variable that, when translated to goto, has type t . More... | |
unsigned | java_method_parameter_slots (const java_method_typet &t) |
Returns the the number of JVM local variables (slots) used by the JVM to pass, upon call, the arguments of a Java method whose type is t . More... | |
const std::string | java_class_to_package (const std::string &canonical_classname) |
void | merge_source_location_rec (exprt &expr, const source_locationt &source_location) |
Attaches a source location to an expression and all of its subexpressions. More... | |
bool | is_java_string_literal_id (const irep_idt &id) |
irep_idt | resolve_friendly_method_name (const std::string &friendly_name, const symbol_table_baset &symbol_table, std::string &error) |
Resolves a user-friendly method name (like packagename.Class.method) into an internal name (like java::packagename.Class.method:()V) The input may also have a type descriptor suffix to resolve ambiguity. More... | |
dereference_exprt | checked_dereference (const exprt &expr, const typet &type) |
Dereference an expression and flag it for a null-pointer check. More... | |
void | java_add_components_to_class (symbolt &class_symbol, const struct_union_typet::componentst &components_to_add) |
Add the components in components_to_add to the class denoted by class symbol. More... | |
size_t | find_closing_delimiter (const std::string &src, size_t position, char open_char, char close_char) |
Finds the corresponding closing delimiter to the given opening delimiter. More... | |
void | declare_function (irep_idt function_name, const typet &type, symbol_table_baset &symbol_table) |
Declare a function with the given name and type. More... | |
exprt | make_function_application (const irep_idt &function_name, const exprt::operandst &arguments, const typet &type, symbol_table_baset &symbol_table) |
Create a function application expression. More... | |
irep_idt | strip_java_namespace_prefix (const irep_idt &to_strip) |
Strip java:: prefix from given identifier. More... | |
std::string | pretty_print_java_type (const std::string &fqn_java_type) |
Strip the package name from a java type, for the type to be pretty printed (java::java.lang.Integer -> Integer). More... | |
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. More... | |
bool | is_non_null_library_global (const irep_idt &) |
Check if a symbol is a well-known non-null global. More... | |
Variables | |
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. More... | |
#define JAVA_STRING_LITERAL_PREFIX "java::java.lang.String.Literal" |
Definition at line 53 of file java_utils.h.
Referenced by get_or_create_string_literal_symbol(), and is_java_string_literal_id().
dereference_exprt checked_dereference | ( | const exprt & | expr, |
const typet & | type | ||
) |
Dereference an expression and flag it for a null-pointer check.
expr | expression to dereference and check |
type | expected result type (typically expr.type().subtype()) |
Definition at line 176 of file java_utils.cpp.
References irept::set().
Referenced by java_string_library_preprocesst::code_assign_components_to_java_string(), java_string_library_preprocesst::code_assign_java_string_to_string_expr(), java_string_library_preprocesst::make_equals_function_code(), java_string_library_preprocesst::make_object_get_class_code(), java_string_library_preprocesst::make_string_length_code(), java_string_library_preprocesst::replace_char_array(), and to_member().
void declare_function | ( | irep_idt | function_name, |
const typet & | type, | ||
symbol_table_baset & | symbol_table | ||
) |
Declare a function with the given name and type.
function_name | a name |
type | a type |
symbol_table | symbol table |
Definition at line 255 of file java_utils.cpp.
References symbol_table_baset::add(), symbolt::base_name, symbolt::is_static_lifetime, symbolt::mode, symbolt::name, symbolt::pretty_name, and symbolt::type.
Referenced by make_function_application().
size_t find_closing_delimiter | ( | const std::string & | src, |
size_t | open_pos, | ||
char | open_char, | ||
char | close_char | ||
) |
Finds the corresponding closing delimiter to the given opening delimiter.
It is assumed that open_pos
points to the opening delimiter open_char
in the src
string. The depth of nesting is counted to identify the correct closing delimiter.
A typical use case is for example Java generic types, e.g., List<List<T>>
src | the source string to scan |
open_pos | the initial position of the opening delimiter from where to start the search |
open_char | the opening delimiter |
close_char | the closing delimiter |
src
Definition at line 197 of file java_utils.cpp.
References INVARIANT, PRECONDITION, and to_string().
Referenced by build_class_name(), erase_type_arguments(), extract_generic_interface_reference(), extract_generic_superclass_reference(), find_closing_semi_colon_for_reference_type(), java_generic_type_from_string(), and java_type_from_string().
void generate_class_stub | ( | const irep_idt & | class_name, |
symbol_table_baset & | symbol_table, | ||
message_handlert & | message_handler, | ||
const struct_union_typet::componentst & | componentst | ||
) |
Definition at line 63 of file java_utils.cpp.
References symbolt::base_name, messaget::eom(), id2string(), symbol_table_baset::insert(), symbolt::is_type, java_add_components_to_class(), java_root_class(), message_handler, symbolt::mode, symbolt::name, symbolt::pretty_name, irept::set(), java_class_typet::set_name(), struct_union_typet::set_tag(), symbolt::type, and messaget::warning().
Referenced by java_bytecode_convert_classt::operator()(), and java_bytecode_instrumentt::throw_exception().
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.
component_class_id | class to start searching from. For example, if trying to resolve a reference to A.b, component_class_id is "A". |
component_name | component basename to search for. If searching for A.b, this is "b". |
symbol_table | global symbol table. |
class_hierarchy | global class hierarchy. |
include_interfaces | if true, search for the given component in all ancestors including interfaces, rather than just parents. |
Definition at line 339 of file java_utils.cpp.
References dstringt::empty(), irept::get(), resolve_inherited_componentt::inherited_componentt::get_class_identifier(), resolve_inherited_componentt::inherited_componentt::get_full_component_identifier(), id2string(), resolve_inherited_componentt::inherited_componentt::is_valid(), java_class_to_package(), symbol_table_baset::lookup(), symbolt::type, and UNREACHABLE.
Referenced by create_stub_global_symbols(), java_bytecode_convert_methodt::get_static_field(), and java_bytecode_convert_methodt::is_method_inherited().
bool is_java_string_literal_id | ( | const irep_idt & | id | ) |
id | any string |
Definition at line 113 of file java_utils.cpp.
References has_prefix(), id2string(), and JAVA_STRING_LITERAL_PREFIX.
Referenced by java_static_lifetime_init(), and should_init_symbol().
bool is_non_null_library_global | ( | const irep_idt & | symbolid | ) |
Check if a symbol is a well-known non-null global.
symbolid | symbol id to check |
Definition at line 414 of file java_utils.cpp.
Referenced by stub_global_initializer_factoryt::get_stub_initializer_body(), and java_static_lifetime_init().
void java_add_components_to_class | ( | symbolt & | class_symbol, |
const struct_union_typet::componentst & | components_to_add | ||
) |
Add the components in components_to_add to the class denoted by class symbol.
class_symbol | The symbol representing the class we want to modify. |
components_to_add | The vector with the components we want to add. |
Definition at line 236 of file java_utils.cpp.
References irept::id(), symbolt::is_type, PRECONDITION, to_struct_type(), and symbolt::type.
Referenced by generate_class_stub().
const std::string java_class_to_package | ( | const std::string & | canonical_classname | ) |
Definition at line 58 of file java_utils.cpp.
References trim_from_last_delimiter().
Referenced by get_inherited_component().
bool java_is_array_type | ( | const typet & | type | ) |
Definition at line 22 of file java_utils.cpp.
References get_tag(), irept::id(), is_java_array_tag(), and to_struct_type().
unsigned java_local_variable_slots | ( | const typet & | t | ) |
Returns the number of JVM local variables (slots) taken by a local variable that, when translated to goto, has type t
.
Definition at line 29 of file java_utils.cpp.
References irept::get_size_t(), irept::id(), and INVARIANT.
Referenced by java_bytecode_convert_methodt::convert(), java_bytecode_initialize_parameter_names(), and java_method_parameter_slots().
unsigned java_method_parameter_slots | ( | const java_method_typet & | t | ) |
Returns the the number of JVM local variables (slots) used by the JVM to pass, upon call, the arguments of a Java method whose type is t
.
Definition at line 48 of file java_utils.cpp.
References java_local_variable_slots(), and code_typet::parameters().
Referenced by java_bytecode_convert_methodt::convert(), and java_bytecode_initialize_parameter_names().
exprt make_function_application | ( | const irep_idt & | function_name, |
const exprt::operandst & | arguments, | ||
const typet & | type, | ||
symbol_table_baset & | symbol_table | ||
) |
Create a function application expression.
function_name | the name of the function |
arguments | a list of arguments |
type | return type of the function |
symbol_table | a symbol table |
function_name(arguments)
Definition at line 277 of file java_utils.cpp.
References function_application_exprt::arguments(), declare_function(), and id2string().
Referenced by code_assign_function_application(), java_string_library_preprocesst::code_return_function_application(), get_or_create_string_literal_symbol(), and java_string_library_preprocesst::make_equals_function_code().
void merge_source_location_rec | ( | exprt & | expr, |
const source_locationt & | source_location | ||
) |
Attaches a source location to an expression and all of its subexpressions.
Usually only codet needs this, but there are a few known examples of expressions needing a location, such as goto_convertt::do_function_call_symbol
(function() needs a location) and goto_convertt::clean_expr
(any subexpression being split into a separate instruction needs a location), so for safety we give every mentioned expression a location. Any code or expressions with source location fields already set keep those fields using rules of source_locationt::merge.
Definition at line 104 of file java_utils.cpp.
References exprt::add_source_location(), source_locationt::merge(), merge_source_location_rec(), and exprt::operands().
Referenced by java_bytecode_convert_methodt::convert_instructions(), java_bytecode_instrumentt::instrument_code(), and merge_source_location_rec().
std::string pretty_print_java_type | ( | const std::string & | fqn_java_type | ) |
Strip the package name from a java type, for the type to be pretty printed (java::java.lang.Integer -> Integer).
fqn_java_type | The java type we want to pretty print. |
Definition at line 312 of file java_utils.cpp.
References has_prefix().
irep_idt resolve_friendly_method_name | ( | const std::string & | friendly_name, |
const symbol_table_baset & | symbol_table, | ||
std::string & | error | ||
) |
Resolves a user-friendly method name (like packagename.Class.method) into an internal name (like java::packagename.Class.method:()V) The input may also have a type descriptor suffix to resolve ambiguity.
On error, returns irep_idt() and sets error.
friendly_name | user-friendly method name | |
symbol_table | global symbol table | |
[out] | error | gets error description on failure |
Definition at line 118 of file java_utils.cpp.
References has_prefix(), id2string(), and symbol_table_baset::symbols.
Referenced by get_main_symbol().
Strip java:: prefix from given identifier.
to_strip | identifier from which the prefix is stripped |
Definition at line 298 of file java_utils.cpp.
References has_prefix(), id2string(), and PRECONDITION.
Referenced by java_bytecode_convert_methodt::convert_instructions(), get_dependencies_from_generic_parameters_rec(), and pretty_java_type().
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.
Definition at line 425 of file java_utils.cpp.
Referenced by java_bytecode_convert_method(), and java_bytecode_languaget::methods_provided().