20 #include <unordered_set> 24 if(type.
id() != ID_struct)
33 if(t.
id()==ID_pointer)
36 const std::size_t bitwidth = t.
get_size_t(ID_width);
42 "all types constructed in java_types.cpp encode JVM types " 43 "with these bit widths");
45 return bitwidth == 64 ? 2u : 1u;
72 class_type.
set(ID_base_name, class_name);
74 class_type.
set(ID_incomplete_class,
true);
82 new_symbol.
type=class_type;
83 new_symbol.
mode=ID_java;
86 std::pair<symbolt &, bool> res=symbol_table.
insert(std::move(new_symbol));
92 "stub class symbol " <<
119 const std::string &friendly_name,
123 std::string qualified_name=
"java::"+friendly_name;
124 if(friendly_name.rfind(
':')==std::string::npos)
126 std::string prefix=qualified_name+
':';
127 std::set<irep_idt> matches;
129 for(
const auto &s : symbol_table.
symbols)
131 s.second.type.id()==ID_code)
132 matches.insert(s.first);
136 error=
"'"+friendly_name+
"' not found";
139 else if(matches.size()>1)
141 std::ostringstream message;
142 message <<
"'"+friendly_name+
"' is ambiguous between:";
145 for(
const auto &s : matches)
146 message <<
"\n " <<
id2string(s).substr(6);
153 return *matches.begin();
158 auto findit=symbol_table.
symbols.find(qualified_name);
159 if(findit==symbol_table.
symbols.end())
161 error=
"'"+friendly_name+
"' not found";
164 else if(findit->second.type.id()!=ID_code)
166 error=
"'"+friendly_name+
"' not a function";
171 return findit->first;
180 result.
set(ID_java_member_access,
true);
198 const std::string &src,
207 size_t c_pos=open_pos+1;
208 const size_t end_pos=src.size()-1;
211 while(c_pos<=end_pos)
213 if(src[c_pos] == open_char)
215 else if(src[c_pos] == close_char)
224 depth<=(src.size()-open_pos),
226 "\' found in signature to parse.");
229 return std::string::npos;
247 components.push_back(component);
264 func_symbol.
mode=ID_java;
265 func_symbol.
name=function_name;
266 func_symbol.
type=type;
267 symbol_table.
add(func_symbol);
284 std::string fun_name=
id2string(function_name);
300 const std::string to_strip_str=
id2string(to_strip);
301 const std::string prefix=
"java::";
304 return to_strip_str.substr(prefix.size(), std::string::npos);
314 std::string result(fqn_java_type);
315 const std::string java_cbmc_string(
"java::");
317 if(
has_prefix(fqn_java_type, java_cbmc_string))
318 result = fqn_java_type.substr(java_cbmc_string.length());
321 const std::string java_lang_string(
"java.lang.");
323 result = result.substr(java_lang_string.length());
344 bool include_interfaces)
347 symbol_table, class_hierarchy);
349 component_resolver(component_class_id, component_name, include_interfaces);
359 return resolved_component;
362 const symbolt &component_symbol=
367 access = component_symbol.
type.
get(ID_C_access);
369 if(access==ID_public || access==ID_protected)
372 return resolved_component;
377 if(access==ID_default)
379 const std::string &class_package=
381 const std::string &component_package=
385 if(component_package == class_package)
386 return resolved_component;
391 if(access==ID_private)
416 static const irep_idt in =
"java::java.lang.System.in";
417 static const irep_idt out =
"java::java.lang.System.out";
418 static const irep_idt err =
"java::java.lang.System.err";
419 return symbolid == in || symbolid == out || symbolid == err;
The type of an expression.
irep_idt name
The unique identifier.
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...
#define JAVA_STRING_LITERAL_PREFIX
const std::string & id2string(const irep_idt &d)
dereference_exprt checked_dereference(const exprt &expr, const typet &type)
Dereference an expression and flag it for a null-pointer check.
application of (mathematical) function
void java_root_class(symbolt &class_symbol)
Create components to an object of the root class (usually java.lang.Object) Specifically, we add a new component, '@class_identifier'.
Non-graph-based representation of the class hierarchy.
irep_idt mode
Language mode.
bool is_java_string_literal_id(const irep_idt &id)
bool java_is_array_type(const typet &type)
const std::string java_class_to_package(const std::string &canonical_classname)
irep_idt get_tag(const typet &type)
bool is_valid() const
Use to check if this inherited_componentt has been fully constructed.
std::vector< componentt > componentst
irep_idt pretty_name
Language-specific display name.
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
void generate_class_stub(const irep_idt &class_name, symbol_table_baset &symbol_table, message_handlert &message_handler, const struct_union_typet::componentst &componentst)
static mstreamt & eom(mstreamt &m)
bool is_java_array_tag(const irep_idt &tag)
See above.
#define INVARIANT(CONDITION, REASON)
mstreamt & warning() const
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 merge(const source_locationt &from)
Set all unset source-location fields in this object to their values in 'from'.
const irep_idt & id() const
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.
irep_idt strip_java_namespace_prefix(const irep_idt &to_strip)
Strip java:: prefix from given identifier.
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.
Operator to dereference a pointer.
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.
const irep_idt & get(const irep_namet &name) const
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
#define PRECONDITION(CONDITION)
void set_tag(const irep_idt &tag)
bool has_prefix(const std::string &s, const std::string &prefix)
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.
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 ...
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...
void declare_function(irep_idt function_name, const typet &type, symbol_table_baset &symbol_table)
Declare a function with the given name and type.
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
bool is_non_null_library_global(const irep_idt &symbolid)
Check if a symbol is a well-known non-null global.
std::vector< exprt > operandst
typet type
Type of symbol.
void merge_source_location_rec(exprt &expr, const source_locationt &source_location)
Attaches a source location to an expression and all of its subexpressions.
std::string trim_from_last_delimiter(const std::string &s, const char delim)
Base class for all expressions.
irep_idt get_class_identifier() const
const parameterst & parameters() const
irep_idt base_name
Base (non-scoped) name.
The symbol table base class interface.
std::string to_string(const string_constraintt &expr)
Used for debug printing.
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...
virtual std::pair< symbolt &, bool > insert(symbolt symbol)=0
Move or copy a new symbol to the symbol table.
source_locationt & add_source_location()
Expression to hold a symbol (variable)
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
goto_programt coverage_criteriont message_handlert & message_handler
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
std::size_t get_size_t(const irep_namet &name) const
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).
irep_idt get_full_component_identifier() const
Get the full name of this function.
void set(const irep_namet &name, const irep_idt &value)