Loading...

Searching...

No Matches

java_utils.cpp File Reference

#include "java_root_class.h"
#include <util/fresh_symbol.h>
#include <util/invariant.h>
#include <util/mathematical_expr.h>
#include <util/mathematical_types.h>
#include <util/message.h>
#include <util/prefix.h>
#include <util/std_types.h>
#include <util/string_utils.h>
#include <util/symbol_table_base.h>
#include "java_string_library_preprocess.h"
#include "java_utils.h"
#include <set>
#include <unordered_set>

+ Include dependency graph for java_utils.cpp:

[フレーム]

Go to the source code of this file.

Functions

bool is_java_string_type (const struct_typet &struct_type)

Returns true iff the argument represents a string type (CharSequence, StringBuilder, StringBuffer or String).

const java_boxed_type_infot * get_boxed_type_info_by_name (const irep_idt &type_name)

If type_name is a Java boxed type tag, return information about it, otherwise return null.

const java_primitive_type_infot * get_java_primitive_type_info (const typet &maybe_primitive_type)

If primitive_type is a Java primitive type, return information about it, otherwise return null.

bool is_primitive_wrapper_type_id (const irep_idt &id)

Returns true iff the argument is the symbol-table identifier of a Java primitive wrapper type (for example, java::java.lang.Byte)

bool is_primitive_wrapper_type_name (const std::string &type_name)

Returns true iff the argument is the fully qualified name of a Java primitive wrapper type (for example, java.lang.Byte)

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.

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.

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.

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.

pointer_typet pointer_to_replacement_type (const pointer_typet &given_pointer_type, const java_class_typet &replacement_class_type)

Given a pointer type to a Java class and a type representing a more specific Java class, return a pointer type to the more specific class with the same structure as the original pointer type.

dereference_exprt checked_dereference (const exprt &expr)

Dereference an expression and flag it for a null-pointer check.

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.

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.

static auxiliary_symbolt declare_function (const irep_idt &function_name, const mathematical_function_typet &type, symbol_table_baset &symbol_table)

Declare a function with the given name and type.

exprt make_function_application (const irep_idt &function_name, const exprt::operandst &arguments, const typet &range, symbol_table_baset &symbol_table)

Create a (mathematical) function application expression.

irep_idt strip_java_namespace_prefix (const irep_idt &to_strip)

Strip java:: prefix from given identifier.

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

std::optional< resolve_inherited_componentt::inherited_componentt > get_inherited_component (const irep_idt &component_class_id, const irep_idt &component_name, const symbol_table_baset &symbol_table, bool include_interfaces)

Finds an inherited component (method or field), taking component visibility into account.

bool is_non_null_library_global (const irep_idt &symbolid)

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

symbolt & fresh_java_symbol (const typet &type, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &function_name, symbol_table_baset &symbol_table)

std::optional< irep_idt > declaring_class (const symbolt &symbol)

Gets the identifier of the class which declared a given symbol.

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.

std::optional< 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.

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.

Function Documentation

◆ checked_dereference()

dereference_exprt checked_dereference ( const exprt & expr )

Dereference an expression and flag it for a null-pointer check.

Parameters: expr expression to dereference and check

Definition at line 281 of file java_utils.cpp.

◆ class_name_from_method_name()

std::optional< 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.

Returns an empty optional if the class name cannot be retrieved, e.g. method_name is an internal function.

Definition at line 580 of file java_utils.cpp.

◆ declare_function()

static auxiliary_symbolt declare_function ( const irep_idt & function_name,

const mathematical_function_typet & type,

symbol_table_baset & symbol_table

)

static

Declare a function with the given name and type.

Parameters: function_name a name

type a type

symbol_table symbol table

Returns: newly created symbol

Definition at line 358 of file java_utils.cpp.

◆ declaring_class()

std::optional< irep_idt > declaring_class ( const symbolt & symbol )

Gets the identifier of the class which declared a given symbol.

If the symbol is not declared by a class then an empty optional is returned. This is used for method symbols and static field symbols to link them back to the class which declared them.

Definition at line 568 of file java_utils.cpp.

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

Returns: the index of the matching corresponding closing delimiter in src

Definition at line 302 of file java_utils.cpp.

◆ fresh_java_symbol()

symbolt & fresh_java_symbol ( const typet & type,

const std::string & basename_prefix,

const source_locationt & source_location,

const irep_idt & function_name,

symbol_table_baset & symbol_table

)

Parameters: type type of new symbol

basename_prefix new symbol will be named function_name::basename_prefix$num

source_location new symbol source loc

function_name name of the function in which the symbol is defined

symbol_table table to add the new symbol to

Returns: fresh-named symbol with the requested name pattern

Definition at line 555 of file java_utils.cpp.

◆ generate_class_stub()

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 162 of file java_utils.cpp.

◆ get_boxed_type_info_by_name()

const java_boxed_type_infot * get_boxed_type_info_by_name ( const irep_idt & type_name )

If type_name is a Java boxed type tag, return information about it, otherwise return null.

Definition at line 36 of file java_utils.cpp.

◆ get_inherited_component()

std::optional< resolve_inherited_componentt::inherited_componentt > get_inherited_component ( const irep_idt & component_class_id,

const irep_idt & component_name,

const symbol_table_baset & symbol_table,

bool include_interfaces

)

Finds an inherited component (method or field), taking component visibility into account.

Parameters: 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.

include_interfaces if 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 448 of file java_utils.cpp.

◆ get_java_primitive_type_info()

const java_primitive_type_infot * get_java_primitive_type_info ( const typet & maybe_primitive_type )

If primitive_type is a Java primitive type, return information about it, otherwise return null.

Definition at line 63 of file java_utils.cpp.

◆ is_java_string_literal_id()

bool is_java_string_literal_id ( const irep_idt & id )

Parameters: id any string

Returns: Returns true if 'id' identifies a string literal symbol

Definition at line 207 of file java_utils.cpp.

◆ is_java_string_type()

bool is_java_string_type ( const struct_typet & struct_type )

Returns true iff the argument represents a string type (CharSequence, StringBuilder, StringBuffer or String).

The check for the length and data components is necessary in the case where string refinement is not activated. In this case, struct_type only contains the standard Object fields (or may have some other model entirely), and in particular may not have length and data fields.

Definition at line 27 of file java_utils.cpp.

◆ 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: symbolid symbol id to check

Returns: true if this static field is known never to be null

Definition at line 519 of file java_utils.cpp.

◆ is_primitive_wrapper_type_id()

bool is_primitive_wrapper_type_id ( const irep_idt & id )

Returns true iff the argument is the symbol-table identifier of a Java primitive wrapper type (for example, java::java.lang.Byte)

Definition at line 109 of file java_utils.cpp.

◆ is_primitive_wrapper_type_name()

bool is_primitive_wrapper_type_name ( const std::string & type_name )

Returns true iff the argument is the fully qualified name of a Java primitive wrapper type (for example, java.lang.Byte)

Definition at line 114 of file java_utils.cpp.

◆ 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_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 341 of file java_utils.cpp.

◆ java_class_to_package()

const std::string java_class_to_package ( const std::string & canonical_classname )

Definition at line 157 of file java_utils.cpp.

◆ 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 128 of file java_utils.cpp.

◆ 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 147 of file java_utils.cpp.

◆ make_function_application()

exprt make_function_application ( const irep_idt & function_name,

const exprt::operandst & arguments,

const typet & range,

symbol_table_baset & symbol_table

)

Create a (mathematical) function application expression.

The application has the type of the codomain (range) of the function.

Parameters: function_name the name of the function

arguments a list of arguments (an element of the domain)

range return type (codomain) of the function

symbol_table a symbol table

Returns: a function application expression representing: function_name(arguments)

Definition at line 384 of file java_utils.cpp.

◆ 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 198 of file java_utils.cpp.

◆ pointer_to_replacement_type()

pointer_typet pointer_to_replacement_type ( const pointer_typet & given_pointer_type,

const java_class_typet & replacement_class_type

)

Given a pointer type to a Java class and a type representing a more specific Java class, return a pointer type to the more specific class with the same structure as the original pointer type.

Definition at line 269 of file java_utils.cpp.

◆ 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_type The java type we want to pretty print.

Returns: The pretty printed type if there was a match of the qualifiers, or the type as it was passed otherwise.

Definition at line 421 of file java_utils.cpp.

◆ 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_name user-friendly method name

symbol_table global symbol table

[out] error gets error description on failure

Definition at line 212 of file java_utils.cpp.

◆ set_declaring_class()

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.

Definition at line 574 of file java_utils.cpp.

◆ strip_java_namespace_prefix()

irep_idt strip_java_namespace_prefix ( const irep_idt & to_strip )

Strip java:: prefix from given identifier.

Parameters: to_strip identifier from which the prefix is stripped

Returns: the identifier without without java:: prefix

Definition at line 407 of file java_utils.cpp.

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

"getMonitorCount"}

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 529 of file java_utils.cpp.