cprover
java_utils.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #ifndef CPROVER_JAVA_BYTECODE_JAVA_UTILS_H
10 #define CPROVER_JAVA_BYTECODE_JAVA_UTILS_H
11 
12 #include "java_types.h"
13 
14 #include <unordered_set>
15 
16 #include <util/message.h>
17 #include <util/nodiscard.h>
18 #include <util/optional.h>
19 #include <util/std_expr.h>
20 #include <util/symbol_table.h>
21 
23 
24 DEPRECATED(SINCE(2019, 6, 10, "use is_java_array_type instead"))
25 bool java_is_array_type(const typet &type);
26 
33 bool is_java_string_type(const struct_typet &struct_type);
34 
37 {
48 };
49 
53 get_java_primitive_type_info(const typet &maybe_primitive_type);
54 
57 {
63 };
64 
68 get_boxed_type_info_by_name(const irep_idt &type_name);
69 
73 
76 bool is_primitive_wrapper_type_name(const std::string &type_name);
77 
79  const irep_idt &class_name,
80  symbol_table_baset &symbol_table,
81  message_handlert &message_handler,
82  const struct_union_typet::componentst &componentst);
83 
86 unsigned java_local_variable_slots(const typet &t);
87 
91 
92 const std::string java_class_to_package(const std::string &canonical_classname);
93 
104  exprt &expr,
105  const source_locationt &source_location);
106 
107 #define JAVA_STRING_LITERAL_PREFIX "java::java.lang.String.Literal"
108 
111 bool is_java_string_literal_id(const irep_idt &id);
112 
121  const std::string &friendly_name,
122  const symbol_table_baset &symbol_table,
123  std::string &error);
124 
129  const pointer_typet &given_pointer_type,
130  const java_class_typet &replacement_class_type);
131 
135 
141  symbolt &class_symbol,
142  const struct_union_typet::componentst &components_to_add);
143 
145  const std::string &src,
146  size_t position,
147  char open_char,
148  char close_char);
149 
151  const irep_idt &function_name,
152  const exprt::operandst &arguments,
153  const typet &range,
154  symbol_table_baset &symbol_table);
155 
157 
158 std::string pretty_print_java_type(const std::string &fqn_java_type);
159 
162  const irep_idt &component_class_id,
163  const irep_idt &component_name,
164  const symbol_tablet &symbol_table,
165  bool include_interfaces);
166 
168 
169 extern const std::unordered_set<std::string> cprover_methods_to_ignore;
170 
172  const typet &type,
173  const std::string &basename_prefix,
174  const source_locationt &source_location,
175  const irep_idt &function_name,
176  symbol_table_baset &symbol_table);
177 
183 
187 
192 class_name_from_method_name(const std::string &method_name);
193 
194 #endif // CPROVER_JAVA_BYTECODE_JAVA_UTILS_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
NODISCARD
#define NODISCARD
Definition: nodiscard.h:22
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 ...
Definition: java_utils.cpp:134
java_primitive_type_infot::boxed_type_factory_method
const irep_idt boxed_type_factory_method
Full identifier of the boxed type's factory method that takes the corresponding primitive as its sole...
Definition: java_utils.h:42
typet
The type of an expression, extends irept.
Definition: type.h:29
optional.h
is_java_string_literal_id
bool is_java_string_literal_id(const irep_idt &id)
Definition: java_utils.cpp:216
dereference_exprt
Operator to dereference a pointer.
Definition: std_expr.h:2888
find_closing_delimiter
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.
Definition: java_utils.cpp:312
declaring_class
optionalt< irep_idt > declaring_class(const symbolt &symbol)
Gets the identifier of the class which declared a given symbol.
Definition: java_utils.cpp:579
java_primitive_type_infot::boxed_type_name
const irep_idt boxed_type_name
Name, including java:: prefix, of the corresponding boxed type.
Definition: java_utils.h:39
nodiscard.h
checked_dereference
dereference_exprt checked_dereference(const exprt &expr)
Dereference an expression and flag it for a null-pointer check.
Definition: java_utils.cpp:291
exprt
Base class for all expressions.
Definition: expr.h:53
struct_union_typet::componentst
std::vector< componentt > componentst
Definition: std_types.h:135
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,...
Definition: java_utils.cpp:153
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: java_utils.cpp:585
resolve_inherited_component.h
Given a class and a component (either field or method), find the closest parent that defines that com...
java_class_typet
Definition: java_types.h:199
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...
Definition: java_utils.cpp:221
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 ex...
Definition: java_utils.cpp:115
java_boxed_type_infot
Return type for get_boxed_type_info_by_name.
Definition: java_utils.h:57
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.
Definition: java_utils.cpp:351
java_primitive_type_infot::unboxing_function_name
const irep_idt unboxing_function_name
Full identifier of the most general boxed-type method that yields this type.
Definition: java_utils.h:47
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....
Definition: java_utils.cpp:431
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:22
java_is_array_type
bool java_is_array_type(const typet &type)
Definition: java_utils.cpp:26
class_name_from_method_name
NODISCARD optionalt< 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.
Definition: java_utils.cpp:591
java_class_to_package
const std::string java_class_to_package(const std::string &canonical_classname)
Definition: java_utils.cpp:163
message_handlert
Definition: message.h:28
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
strip_java_namespace_prefix
irep_idt strip_java_namespace_prefix(const irep_idt &to_strip)
Strip java:: prefix from given identifier.
Definition: java_utils.cpp:417
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.
Definition: java_utils.cpp:207
get_inherited_component
optionalt< resolve_inherited_componentt::inherited_componentt > get_inherited_component(const irep_idt &component_class_id, const irep_idt &component_name, const symbol_tablet &symbol_table, bool include_interfaces)
Finds an inherited component (method or field), taking component visibility into account.
Definition: java_utils.cpp:458
SINCE
#define SINCE(year, month, day, msg)
Definition: deprecate.h:26
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
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: java_utils.cpp:69
java_primitive_type_infot
Return type for get_java_primitive_type_info.
Definition: java_utils.h:37
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 examp...
Definition: java_utils.cpp:120
source_locationt
Definition: source_location.h:20
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:226
DEPRECATED
#define DEPRECATED(msg)
Definition: deprecate.h:23
symbolt
Symbol table entry.
Definition: symbol.h:28
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: java_utils.cpp:42
java_boxed_type_infot::unboxing_function_name
const irep_idt unboxing_function_name
Name of the function defined on the boxed type that returns the boxed value.
Definition: java_utils.h:60
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.
Definition: java_utils.cpp:394
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,...
Definition: java_utils.cpp:33
java_types.h
cprover_methods_to_ignore
const std::unordered_set< std::string > cprover_methods_to_ignore
Methods belonging to the class org.cprover.CProver that should be ignored (not converted),...
Definition: java_utils.cpp:540
symbol_table.h
Author: Diffblue Ltd.
pointer_typet
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: std_types.h:1488
message.h
std_expr.h
API to expression classes.
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: java_utils.cpp:168
java_method_typet
Definition: java_types.h:103
java_boxed_type_infot::corresponding_primitive_type
const typet corresponding_primitive_type
Primitive type that this boxed type contains.
Definition: java_utils.h:62
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,...
Definition: java_utils.cpp:279
is_non_null_library_global
bool is_non_null_library_global(const irep_idt &)
Check if a symbol is a well-known non-null global.
Definition: java_utils.cpp:529
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)
Definition: java_utils.cpp:566