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

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

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

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

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

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

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

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

dereference_exprt	checked_dereference (const exprt &expr)
	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...

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

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

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

bool	is_non_null_library_global (const irep_idt &symbolid)
	Check if a symbol is a well-known non-null global. More...

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`. More...

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`. More...

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

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.

Functions

Variables

Function Documentation

◆ checked_dereference()

◆ class_name_from_method_name()

◆ declare_function()

◆ declaring_class()

◆ find_closing_delimiter()

◆ fresh_java_symbol()

◆ generate_class_stub()

◆ get_boxed_type_info_by_name()

◆ get_inherited_component()

◆ get_java_primitive_type_info()

◆ is_java_string_literal_id()

◆ is_java_string_type()

◆ is_non_null_library_global()

◆ is_primitive_wrapper_type_id()

◆ is_primitive_wrapper_type_name()

◆ java_add_components_to_class()

◆ java_class_to_package()

◆ java_local_variable_slots()

◆ java_method_parameter_slots()

◆ make_function_application()

◆ merge_source_location_rec()

◆ pointer_to_replacement_type()

◆ pretty_print_java_type()

◆ resolve_friendly_method_name()

◆ set_declaring_class()

◆ strip_java_namespace_prefix()

Variable Documentation

◆ cprover_methods_to_ignore