Go to the documentation of this file.
24 #include <unordered_set>
28 if(type.
id() != ID_struct)
44 static std::unordered_map<irep_idt, java_boxed_type_infot> type_info_by_name =
46 {
"java::java.lang.Boolean",
48 {
"java::java.lang.Byte",
50 {
"java::java.lang.Character",
52 {
"java::java.lang.Double",
54 {
"java::java.lang.Float",
56 {
"java::java.lang.Integer",
58 {
"java::java.lang.Long",
60 {
"java::java.lang.Short",
64 auto found = type_info_by_name.find(type_name);
65 return found == type_info_by_name.end() ? nullptr : &found->second;
71 static std::unordered_map<typet, java_primitive_type_infot, irep_hash>
72 type_info_by_primitive_type = {
74 {
"java::java.lang.Boolean",
75 "java::java.lang.Boolean.valueOf:(Z)Ljava/lang/Boolean;",
76 "java::java.lang.Boolean.booleanValue:()Z"}},
78 {
"java::java.lang.Byte",
79 "java::java.lang.Byte.valueOf:(B)Ljava/lang/Byte;",
80 "java::java.lang.Number.byteValue:()B"}},
82 {
"java::java.lang.Character",
83 "java::java.lang.Character.valueOf:(C)"
84 "Ljava/lang/Character;",
85 "java::java.lang.Character.charValue:()C"}},
87 {
"java::java.lang.Double",
88 "java::java.lang.Double.valueOf:(D)"
90 "java::java.lang.Number.doubleValue:()D"}},
92 {
"java::java.lang.Float",
93 "java::java.lang.Float.valueOf:(F)"
95 "java::java.lang.Number.floatValue:()F"}},
97 {
"java::java.lang.Integer",
98 "java::java.lang.Integer.valueOf:(I)"
99 "Ljava/lang/Integer;",
100 "java::java.lang.Number.intValue:()I"}},
102 {
"java::java.lang.Long",
103 "java::java.lang.Long.valueOf:(J)Ljava/lang/Long;",
104 "java::java.lang.Number.longValue:()J"}},
106 {
"java::java.lang.Short",
107 "java::java.lang.Short.valueOf:(S)"
109 "java::java.lang.Number.shortValue:()S"}}};
111 auto found = type_info_by_primitive_type.find(maybe_primitive_type);
112 return found == type_info_by_primitive_type.end() ? nullptr : &found->second;
122 static const std::unordered_set<std::string> primitive_wrapper_type_names = {
125 "java.lang.Character",
131 return primitive_wrapper_type_names.count(type_name) > 0;
138 if(t.
id()==ID_pointer)
147 "all types constructed in java_types.cpp encode JVM types "
148 "with these bit widths");
150 return bitwidth == 64 ? 2u : 1u;
176 class_type.
set_tag(class_name);
185 new_symbol.
type=class_type;
186 new_symbol.
mode=ID_java;
189 std::pair<symbolt &, bool> res=symbol_table.
insert(std::move(new_symbol));
195 "stub class symbol " <<
222 const std::string &friendly_name,
226 std::string qualified_name=
"java::"+friendly_name;
227 if(friendly_name.rfind(
':')==std::string::npos)
229 std::string prefix=qualified_name+
':';
230 std::set<irep_idt> matches;
232 for(
const auto &s : symbol_table.
symbols)
234 s.second.type.id()==ID_code)
235 matches.insert(s.first);
239 error=
"'"+friendly_name+
"' not found";
242 else if(matches.size()>1)
245 message <<
"'"+friendly_name+
"' is ambiguous between:";
248 for(
const auto &s : matches)
256 return *matches.begin();
261 auto findit=symbol_table.
symbols.find(qualified_name);
262 if(findit==symbol_table.
symbols.end())
264 error=
"'"+friendly_name+
"' not found";
267 else if(findit->second.type.id()!=ID_code)
269 error=
"'"+friendly_name+
"' not a function";
274 return findit->first;
295 result.
set(ID_java_member_access,
true);
313 const std::string &src,
322 size_t c_pos=open_pos+1;
323 const size_t end_pos=src.size()-1;
326 while(c_pos<=end_pos)
328 if(src[c_pos] == open_char)
330 else if(src[c_pos] == close_char)
339 depth<=(src.size()-open_pos),
341 "\' found in signature to parse.");
344 return std::string::npos;
360 components.end(), components_to_add.begin(), components_to_add.end());
378 func_symbol.
mode=ID_java;
379 func_symbol.
name=function_name;
380 func_symbol.
type=type;
381 symbol_table.
add(func_symbol);
400 std::vector<typet> argument_types;
401 for(
const auto &arg : arguments)
402 argument_types.push_back(arg.type());
419 const std::string to_strip_str=
id2string(to_strip);
420 const std::string prefix=
"java::";
423 return to_strip_str.substr(prefix.size(), std::string::npos);
433 std::string result(fqn_java_type);
434 const std::string java_cbmc_string(
"java::");
436 if(
has_prefix(fqn_java_type, java_cbmc_string))
437 result = fqn_java_type.substr(java_cbmc_string.length());
440 const std::string java_lang_string(
"java.lang.");
442 result = result.substr(java_lang_string.length());
462 bool include_interfaces)
465 const auto resolved_component =
466 component_resolver(component_class_id, component_name, include_interfaces);
472 if(resolved_component)
475 if(component_class_id == resolved_component->get_class_identifier())
476 return *resolved_component;
480 resolved_component->get_full_component_identifier());
484 access = component_symbol.
type.
get(ID_C_access);
486 if(access==ID_public || access==ID_protected)
489 return *resolved_component;
494 if(access==ID_default)
496 const std::string &class_package=
499 id2string(resolved_component->get_class_identifier()));
500 if(component_package == class_package)
501 return *resolved_component;
506 if(access==ID_private)
531 static const irep_idt in =
"java::java.lang.System.in";
532 static const irep_idt out =
"java::java.lang.System.out";
533 static const irep_idt err =
"java::java.lang.System.err";
534 return symbolid == in || symbolid == out || symbolid == err;
568 const std::string &basename_prefix,
574 const std::string name_prefix =
id2string(function_name);
576 type, name_prefix, basename_prefix, source_location, ID_java, symbol_table);
593 const auto signature_index = method_name.rfind(
":");
594 const auto method_index = method_name.rfind(
".", signature_index);
595 if(method_index == std::string::npos)
597 return method_name.substr(0, method_index);
Class that provides messages with a built-in verbosity 'level'.
#define UNREACHABLE
This should be used to mark dead code.
const componentst & components() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
const typet & subtype() const
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...
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
bool is_java_string_literal_id(const irep_idt &id)
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.
The type of an expression, extends irept.
Fresh auxiliary symbol creation.
signedbv_typet java_long_type()
typet type
Type of symbol.
Operator to dereference a pointer.
dereference_exprt checked_dereference(const exprt &expr)
Dereference an expression and flag it for a null-pointer check.
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.
const std::string java_class_to_package(const std::string &canonical_classname)
optionalt< irep_idt > declaring_class(const symbolt &symbol)
Gets the identifier of the class which declared a given symbol.
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)
Base class for all expressions.
std::vector< componentt > componentst
bool is_java_array_tag(const irep_idt &tag)
See above.
Produce code for simple implementation of String Java libraries.
irep_idt base_name
Base (non-scoped) name.
A struct tag type, i.e., struct_typet with an identifier.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
std::string trim_from_last_delimiter(const std::string &s, const char delim)
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.
irep_idt pretty_name
Language-specific display name.
irep_idt strip_java_namespace_prefix(const irep_idt &to_strip)
Strip java:: prefix from given identifier.
static const char * message(const static_verifier_resultt::statust &status)
Makes a status message string from a status.
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.
Return type for get_boxed_type_info_by_name.
irep_idt mode
Language mode.
bool is_java_string_type(const struct_typet &struct_type)
Returns true iff the argument represents a string type (CharSequence, StringBuilder,...
const std::string & id2string(const irep_idt &d)
void set_tag(const irep_idt &tag)
bool can_cast_type< struct_tag_typet >(const typet &type)
Check whether a reference to a typet is a struct_tag_typet.
#define PRECONDITION(CONDITION)
The symbol table base class interface.
void merge(const source_locationt &from)
Set all unset source-location fields in this object to their values in 'from'.
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.
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...
bool is_non_null_library_global(const irep_idt &symbolid)
Check if a symbol is a well-known non-null global.
Application of (mathematical) function.
pointer_typet pointer_type(const typet &subtype)
static bool implements_java_char_sequence(const typet &type)
bool has_component(const irep_idt &component_name) const
const irep_idt & id() const
std::vector< exprt > operandst
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 ...
const std::unordered_set< std::string > cprover_methods_to_ignore
Methods belonging to the class org.cprover.CProver that should be ignored (not converted),...
signedbv_typet java_int_type()
const parameterst & parameters() const
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,...
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)
nonstd::optional< T > optionalt
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.
Return type for get_java_primitive_type_info.
signedbv_typet java_short_type()
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.
signedbv_typet java_byte_type()
std::size_t get_width() const
const irep_idt & get_name() const
Get the name of the struct, which can be used to look up its symbol in the symbol table.
void set_is_stub(bool is_stub)
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
void merge_source_location_rec(exprt &expr, const source_locationt &source_location)
Attaches a source location to an expression and all of its subexpressions.
Structure type, corresponds to C style structs.
floatbv_typet java_double_type()
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,...
const irep_idt & get(const irep_namet &name) const
void set(const irep_namet &name, const irep_idt &value)
const symbolst & symbols
Read-only field, used to look up symbols given their names.
unsignedbv_typet java_char_type()
void set_name(const irep_idt &name)
Set the name of the struct, which can be used to look up its symbol in the symbol table.
c_bool_typet java_boolean_type()
virtual std::pair< symbolt &, bool > insert(symbolt symbol)=0
Move or copy a new symbol to the symbol table.
void java_root_class(symbolt &class_symbol)
Create components to an object of the root class (usually java.lang.Object) Specifically,...
bool has_prefix(const std::string &s, const std::string &prefix)
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.
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....
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
source_locationt & add_source_location()
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...
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
A type for mathematical functions (do not confuse with functions/methods in code)
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.
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, const namespacet &ns, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with respect to the given namespace ns with the requested name pattern ...
#define JAVA_STRING_LITERAL_PREFIX
irep_idt name
The unique identifier.
floatbv_typet java_float_type()
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
API to expression classes for 'mathematical' expressions.
static irep_idt get_tag(const typet &type)