cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
resolve_inherited_component.cpp
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: GOTO Program Utilities
4
5
Author: Diffblue Ltd.
6
7
\*******************************************************************/
8
9
#include "
resolve_inherited_component.h
"
10
11
#include <
util/range.h
>
12
#include <
util/std_types.h
>
13
#include <
util/symbol_table_base.h
>
14
17
resolve_inherited_componentt::resolve_inherited_componentt
(
18
const
symbol_table_baset
&
symbol_table
)
19
:
symbol_table
(
symbol_table
)
20
{
21
}
22
35
std::optional<resolve_inherited_componentt::inherited_componentt>
36
resolve_inherited_componentt::operator()
(
37
const
irep_idt
&class_id,
38
const
irep_idt
&component_name,
39
bool
include_interfaces,
40
const
std::function<
bool
(
const
symbolt
&)> user_filter)
41
{
42
PRECONDITION
(!class_id.
empty
());
43
PRECONDITION
(!component_name.
empty
());
44
45
std::vector<irep_idt> classes_to_visit;
46
classes_to_visit.push_back(class_id);
47
while
(!classes_to_visit.empty())
48
{
49
irep_idt
current_class = classes_to_visit.back();
50
classes_to_visit.pop_back();
51
52
const
irep_idt
&full_component_identifier=
53
build_full_component_identifier
(current_class, component_name);
54
55
const
symbolt
*symbol =
symbol_table
.lookup(full_component_identifier);
56
if
(symbol && user_filter(*symbol))
57
{
58
return
inherited_componentt
(current_class, component_name);
59
}
60
61
const
auto
current_class_symbol_it =
62
symbol_table
.symbols.find(current_class);
63
64
if
(current_class_symbol_it !=
symbol_table
.symbols.end())
65
{
66
const
auto
parents =
67
make_range
(
to_struct_type
(current_class_symbol_it->second.type).
bases
())
68
.map([](
const
struct_typet::baset
&base) {
69
return
base.
type
().
get_identifier
();
70
});
71
72
if
(include_interfaces)
73
{
74
classes_to_visit.insert(
75
classes_to_visit.end(), parents.begin(), parents.end());
76
}
77
else
78
{
79
if
(!parents.empty())
80
classes_to_visit.push_back(*parents.begin());
81
}
82
}
83
}
84
85
return
{};
86
}
87
94
irep_idt
resolve_inherited_componentt::build_full_component_identifier
(
95
const
irep_idt
&class_name,
const
irep_idt
&component_name)
96
{
97
// Verify the parameters are called in the correct order.
98
PRECONDITION
(
id2string
(class_name).find(
"::"
)!=std::string::npos);
99
PRECONDITION
(
id2string
(component_name).find(
"::"
)==std::string::npos);
100
return
id2string
(class_name)+
'.'
+
id2string
(component_name);
101
}
102
105
irep_idt
resolve_inherited_componentt::inherited_componentt::
106
get_full_component_identifier
()
const
107
{
108
return
resolve_inherited_componentt::build_full_component_identifier
(
109
class_identifier
,
component_identifier
);
110
}
111
125
std::optional<resolve_inherited_componentt::inherited_componentt>
126
get_inherited_method_implementation
(
127
const
irep_idt
&call_basename,
128
const
irep_idt
&classname,
129
const
symbol_table_baset
&
symbol_table
)
130
{
131
resolve_inherited_componentt
call_resolver{
symbol_table
};
132
auto
exclude_abstract_methods = [&](
const
symbolt
&symbol) {
133
return
!symbol.type.get_bool(ID_C_abstract);
134
};
135
136
auto
resolved_call =
137
call_resolver(classname, call_basename,
false
, exclude_abstract_methods);
138
if
(!resolved_call)
139
{
140
// Check for a default implementation:
141
resolved_call =
142
call_resolver(classname, call_basename,
true
, exclude_abstract_methods);
143
}
144
if
(!resolved_call)
145
{
146
// Finally accept any abstract definition, which will likely get stubbed:
147
resolved_call = call_resolver(classname, call_basename,
true
);
148
}
149
return
resolved_call;
150
}
dstringt::empty
bool empty() const
Definition
dstring.h:89
resolve_inherited_componentt::inherited_componentt
Definition
resolve_inherited_component.h:30
resolve_inherited_componentt::inherited_componentt::component_identifier
irep_idt component_identifier
Definition
resolve_inherited_component.h:47
resolve_inherited_componentt::inherited_componentt::get_full_component_identifier
irep_idt get_full_component_identifier() const
Get the full name of this function.
Definition
resolve_inherited_component.cpp:106
resolve_inherited_componentt::inherited_componentt::class_identifier
irep_idt class_identifier
Definition
resolve_inherited_component.h:46
resolve_inherited_componentt
Definition
resolve_inherited_component.h:25
resolve_inherited_componentt::resolve_inherited_componentt
resolve_inherited_componentt(const symbol_table_baset &symbol_table)
See the operator() method comment.
Definition
resolve_inherited_component.cpp:17
resolve_inherited_componentt::operator()
std::optional< inherited_componentt > operator()(const irep_idt &class_id, const irep_idt &component_name, bool include_interfaces, std::function< bool(const symbolt &)> user_filter=[](const symbolt &) { return true;})
Given a class and a component, identify the concrete field or method it is resolved to.
Definition
resolve_inherited_component.cpp:36
resolve_inherited_componentt::build_full_component_identifier
static irep_idt build_full_component_identifier(const irep_idt &class_name, const irep_idt &component_name)
Build a component name as found in a GOTO symbol table equivalent to the name of a concrete component...
Definition
resolve_inherited_component.cpp:94
resolve_inherited_componentt::symbol_table
const symbol_table_baset & symbol_table
Definition
resolve_inherited_component.h:62
struct_typet::baset
Base class or struct that a class or struct inherits from.
Definition
std_types.h:252
struct_typet::baset::type
struct_tag_typet & type()
Definition
std_types.cpp:84
struct_typet::bases
const basest & bases() const
Get the collection of base classes/structs.
Definition
std_types.h:262
symbol_table_baset
The symbol table base class interface.
Definition
symbol_table_base.h:23
symbolt
Symbol table entry.
Definition
symbol.h:28
tag_typet::get_identifier
const irep_idt & get_identifier() const
Definition
std_types.h:410
id2string
const std::string & id2string(const irep_idt &d)
Definition
irep.h:44
range.h
Ranges: pair of begin and end iterators, which can be initialized from containers,...
make_range
ranget< iteratort > make_range(iteratort begin, iteratort end)
Definition
range.h:522
resolve_inherited_component.h
Given a class and a component (either field or method), find the closest parent that defines that com...
get_inherited_method_implementation
std::optional< resolve_inherited_componentt::inherited_componentt > get_inherited_method_implementation(const irep_idt &call_basename, const irep_idt &classname, const symbol_table_baset &symbol_table)
Given a class and a component, identify the concrete method it is resolved to.
Definition
resolve_inherited_component.cpp:126
PRECONDITION
#define PRECONDITION(CONDITION)
Definition
invariant.h:463
std_types.h
Pre-defined types.
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition
std_types.h:308
symbol_table_base.h
Author: Diffblue Ltd.
irep_idt
dstringt irep_idt
Definition
verification_result.h:16
goto-programs
resolve_inherited_component.cpp
Generated by
1.17.0