cprover
java_utils.cpp File Reference
#include "java_utils.h"
#include "java_root_class.h"
#include <util/invariant.h>
#include <util/message.h>
#include <util/prefix.h>
#include <util/std_types.h>
#include <util/string_utils.h>
#include <set>
#include <unordered_set>
Include dependency graph for java_utils.cpp:

Go to the source code of this file.

Functions

bool java_is_array_type (const typet &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. 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 generate_class_stub (const irep_idt &class_name, symbol_table_baset &symbol_table, message_handlert &message_handler, const struct_union_typet::componentst &componentst)
 
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...
 
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. 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...
 
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 &symbolid)
 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...
 

Function Documentation

◆ checked_dereference()

dereference_exprt checked_dereference ( const exprt expr,
const typet type 
)

◆ declare_function()

void declare_function ( irep_idt  function_name,
const typet type,
symbol_table_baset symbol_table 
)

Declare a function with the given name and type.

Parameters
function_namea name
typea type
symbol_tablesymbol 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().

◆ find_closing_delimiter()

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>>

Parameters
srcthe source string to scan
open_posthe initial position of the opening delimiter from where to start the search
open_charthe opening delimiter
close_charthe closing delimiter
Returns
the index of the matching corresponding closing delimiter in 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().

◆ generate_class_stub()

◆ get_inherited_component()

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.

Parameters
component_class_idclass to start searching from. For example, if trying to resolve a reference to A.b, component_class_id is "A".
component_namecomponent basename to search for. If searching for A.b, this is "b".
symbol_tableglobal symbol table.
class_hierarchyglobal class hierarchy.
include_interfacesif true, search for the given component in all ancestors including interfaces, rather than just parents.
Returns
the concrete component referred to if any is found, or an invalid resolve_inherited_componentt::inherited_componentt otherwise.

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().

◆ is_java_string_literal_id()

bool is_java_string_literal_id ( const irep_idt id)
Parameters
idany string
Returns
Returns true if 'id' identifies a string literal symbol

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().

◆ is_non_null_library_global()

bool is_non_null_library_global ( const irep_idt symbolid)

Check if a symbol is a well-known non-null global.

Parameters
symbolidsymbol id to check
Returns
true if this static field is known never to be null

Definition at line 414 of file java_utils.cpp.

Referenced by stub_global_initializer_factoryt::get_stub_initializer_body(), and java_static_lifetime_init().

◆ java_add_components_to_class()

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.

Parameters
class_symbolThe symbol representing the class we want to modify.
components_to_addThe 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().

◆ java_class_to_package()

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().

◆ java_is_array_type()

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().

◆ java_local_variable_slots()

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().

◆ 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().

◆ make_function_application()

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.

Parameters
function_namethe name of the function
argumentsa list of arguments
typereturn type of the function
symbol_tablea symbol table
Returns
a function application expression representing: 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().

◆ merge_source_location_rec()

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().

◆ pretty_print_java_type()

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).

Parameters
fqn_java_typeThe java type we want to pretty print.
Returns
The pretty printed type if there was a match of the

Definition at line 312 of file java_utils.cpp.

References has_prefix().

◆ resolve_friendly_method_name()

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.

Parameters
friendly_nameuser-friendly method name
symbol_tableglobal symbol table
[out]errorgets 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_namespace_prefix()

irep_idt strip_java_namespace_prefix ( const irep_idt to_strip)

Strip java:: prefix from given identifier.

Parameters
to_stripidentifier from which the prefix is stripped
Returns
the identifier without without java:: prefix

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().

Variable Documentation

◆ cprover_methods_to_ignore

const std::unordered_set<std::string> cprover_methods_to_ignore
Initial value:
{
"nondetBoolean",
"nondetByte",
"nondetChar",
"nondetShort",
"nondetInt",
"nondetLong",
"nondetFloat",
"nondetDouble",
"nondetWithNull",
"nondetWithoutNull",
"notModelled",
"atomicBegin",
"atomicEnd",
"startThread",
"endThread",
"getCurrentThreadID"
}

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().