19 #include <util/vtable.h> 65 const std::string &
module):
75 const std::string &class_name(
id2string(class_type.
get(ID_name)));
81 const std::string &class_name=
id2string(class_type.
get(ID_name));
82 const std::string &base_class_name=
id2string(class_type.
get(ID_base_name));
84 result.
name=vtnamest::get_table(class_name);
85 result.
base_name=vtnamest::get_table_base(base_class_name);
87 result.
mode=type_symbol.mode;
89 result.
location=type_symbol.location;
100 return std::find_if(comps.begin(), comps.end(), pred)!=comps.end();
109 const class_typet::methodst::const_iterator ifc_method(
110 std::find_if(methods.begin(), methods.end(), pred));
111 assert(methods.end()!=ifc_method);
114 const irep_idt &ifc_name(ifc_method->get_name());
122 vtable_type.
components().push_back(entry_component);
132 const typet &type(static_cast<const typet &>(base.
find(ID_type)));
142 const typet &type(static_cast<const typet &>(base.
find(ID_type)));
151 return std::find_if(methods.begin(), methods.end(), pred)!=methods.end();
155 std::vector<class_typet> &result,
159 for(irept::subt::const_iterator it=types.begin();
160 it!=types.end(); ++it)
170 return method.
get_bool(ID_is_virtual)
171 && !method.
get_bool(ID_constructor);
181 std::vector<class_typet> bases;
184 for(
const std::vector<class_typet>::value_type &b : bases)
199 const std::string &class_name(
id2string(class_type.
get(ID_name)));
202 vtable_symbol.
value=vtable_value;
210 const std::string &class_name(
id2string(class_type.
get(ID_name)));
220 const std::string &class_name(
id2string(symbol_name));
227 for(
const class_typet::methodst::value_type &m : methods)
229 for(
const class_typet::methodst::value_type &m : methods)
251 const std::string &module)
254 std::vector<irep_idt> names;
255 names.reserve(symbols.size());
256 std::transform(symbols.begin(), symbols.end(), std::back_inserter(names),
257 [](
const std::pair<irep_idt, symbolt> &entry)
258 {
return entry.first;});
260 std::for_each(names.begin(), names.end(), factory);
261 return factory.has_error;
270 vt_symb_type.
name=vt_name;
271 vt_symb_type.
base_name=vtnamest::get_type_base(
274 vt_symb_type.
mode=class_symbol.
mode;
280 assert(!symbol_table.
add(vt_symb_type));
283 #define ID_vtable_pointer "@vtable_pointer" 295 comp.
set(
"is_vtptr",
true);
379 const std::string &name(
id2string(method.get(ID_name)));
381 std::string virtual_name(name.substr(vname_start));
386 const exprt &this_obj,
391 if(ID_symbol==type_id)
393 assert(ID_pointer==type_id);
400 const bool has_prefix(name.find(
"java::")!=std::string::npos);
402 has_prefix ? std::string(
"java::").size() : 0;
405 return name.substr(0, last_sep);
422 const exprt &this_obj)
424 const irep_idt &func_name(func.
get(ID_identifier));
428 if(class_id.find(
"java.")!=std::string::npos)
446 const member_exprt func_ptr(vtable, func_name, func_ptr_type);
const irep_idt & get_name() const
The type of an expression.
irep_idt name
The unique identifier.
static exprt get_ref(const exprt &this_obj, const symbol_typet &target_type)
void set_virtual_name(class_typet::methodt &method)
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
symbolt & lookup(const irep_idt &identifier)
Find a symbol in the symbol table.
const std::string & id2string(const irep_idt &d)
pointer_typet pointer_type(const typet &subtype)
const char ID_virtual_name[]
const class_typet & get_class_type(const irept &base)
bool is_virtual(const class_typet::methodt &method)
std::vector< irept > subt
irep_idt mode
Language mode.
void set_base_name(const irep_idt &base_name)
void set_name(const irep_idt &name)
void copy_to_operands(const exprt &expr)
void create_vtable_entry(struct_exprt &vtable_value, const class_typet &class_type, const class_typet::methodt &method)
std::vector< componentt > componentst
exprt value
Initial value of symbol.
const componentst & components() const
bool operator()(const class_typet::methodt &method) const
static void add_vtable_pointer_member(const irep_idt &vt_name, symbolt &class_symbol)
irep_idt module
Name of module the symbol belongs to.
irep_idt pretty_name
Language-specific display name.
unsignedbv_typet size_type()
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
const irep_idt & virtual_name
bool get_bool(const irep_namet &name) const
symbolt & get_vt_type_symbol(const class_typet &class_type)
java_bytecode_vtable_factoryt(symbol_tablet &symbol_table, const std::string &module)
bool has_method(const irept &base, const class_typet::methodt &method)
Extract member of struct or union.
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a generic typet to a struct_union_typet.
const irep_idt & id() const
bool has_vtable_info(const symbol_tablet &symbol_table, const symbolt &class_symbol)
const methodst & methods() const
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
A reference into the symbol table.
exprt make_vtable_function(const exprt &func, const exprt &this_obj)
void create_vtable_pointer(symbolt &class_symbol)
void set_vtable_value(symbolt &vtable_symbol, const class_typet &class_type, struct_exprt &vtable_value)
Operator to dereference a pointer.
API to expression classes.
const irep_idt & get(const irep_namet &name) const
void create_base_vtable_entries(struct_exprt &vtable_value, const class_typet &class_type, const class_typet::methodt &method)
std::unordered_map< irep_idt, symbolt, irep_id_hash > symbolst
Base class for tree-like data structures with sharing.
bool operator()(const class_typet::componentt &component) const
is_name_equalt(const irep_idt &name)
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Operator to return the address of an object.
bool has_component(const irep_idt &component_name) const
bool has_prefix(const std::string &s, const std::string &prefix)
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
static void create_vtable_type(const irep_idt &vt_name, symbol_tablet &symbol_table, const symbolt &class_symbol)
#define ID_vtable_pointer
symbol_tablet & symbol_table
void create_vtable_symbol(symbol_tablet &symbol_table, const symbolt &class_symbol)
typet type
Type of symbol.
source_locationt location
Source code location of definition of symbol.
void create_vtable_symbol(symbolt &result, const class_typet &class_type)
bool is_class_with_vt(const symbolt &symbol)
void operator()(const irep_idt &symbol_name)
Base class for all expressions.
irep_idt base_name
Base (non-scoped) name.
void set_pretty_name(const irep_idt &name)
is_virtual_name_equalt(const class_typet::methodt &method)
bool has_component(const class_typet &vtable_type, const irep_idt &ifc_name)
void add_vtable_entry(struct_exprt &vtable_value, const class_typet &interface, const class_typet &implementor, const class_typet::methodt &implementation)
bool has_symbol(const irep_idt &name) const
const std::string & module
Expression to hold a symbol (variable)
const irept::subt & bases() const
struct constructor from list of elements
bool java_bytecode_vtable(symbol_tablet &symbol_table, const std::string &module)
void extract_types(std::vector< class_typet > &result, const irept::subt &types, const class_typet::methodt &method)
const irept & find(const irep_namet &name) const
const irep_idt & get_identifier() const
static std::string get_full_class_name(const std::string &name)
void set(const irep_namet &name, const irep_idt &value)
const class_typet & to_class_type(const typet &type)
Cast a generic typet to a class_typet.