cprover
Loading...
Searching...
No Matches
resolve_inherited_component.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: GOTO Program Utilities
4
5Author: Diffblue Ltd.
6
7\*******************************************************************/
8
10
11#include <util/range.h>
12#include <util/std_types.h>
13#include <util/symbol_table.h>
14
15#include <algorithm>
16
20 const symbol_tablet &symbol_table)
21 : symbol_table(symbol_table)
22{
23}
24
39 const irep_idt &class_id,
40 const irep_idt &component_name,
41 bool include_interfaces,
42 const std::function<bool(const symbolt &)> user_filter)
43{
44 PRECONDITION(!class_id.empty());
45 PRECONDITION(!component_name.empty());
46
47 std::vector<irep_idt> classes_to_visit;
48 classes_to_visit.push_back(class_id);
49 while(!classes_to_visit.empty())
50 {
51 irep_idt current_class = classes_to_visit.back();
52 classes_to_visit.pop_back();
53
54 const irep_idt &full_component_identifier=
55 build_full_component_identifier(current_class, component_name);
56
57 const symbolt *symbol = symbol_table.lookup(full_component_identifier);
58 if(symbol && user_filter(*symbol))
59 {
60 return inherited_componentt(current_class, component_name);
61 }
62
63 const auto current_class_symbol_it =
64 symbol_table.symbols.find(current_class);
65
66 if(current_class_symbol_it != symbol_table.symbols.end())
67 {
68 const auto parents =
69 make_range(to_struct_type(current_class_symbol_it->second.type).bases())
70 .map([](const struct_typet::baset &base) {
71 return base.type().get_identifier();
72 });
73
74 if(include_interfaces)
75 {
76 classes_to_visit.insert(
77 classes_to_visit.end(), parents.begin(), parents.end());
78 }
79 else
80 {
81 if(!parents.empty())
82 classes_to_visit.push_back(*parents.begin());
83 }
84 }
85 }
86
87 return {};
88}
89
97 const irep_idt &class_name, const irep_idt &component_name)
98{
99 // Verify the parameters are called in the correct order.
100 PRECONDITION(id2string(class_name).find("::")!=std::string::npos);
101 PRECONDITION(id2string(component_name).find("::")==std::string::npos);
102 return id2string(class_name)+'.'+id2string(component_name);
103}
104
109{
112}
113
129 const irep_idt &call_basename,
130 const irep_idt &classname,
132{
134 auto exclude_abstract_methods = [&](const symbolt &symbol) {
135 return !symbol.type.get_bool(ID_C_abstract);
136 };
137
138 auto resolved_call =
139 call_resolver(classname, call_basename, false, exclude_abstract_methods);
140 if(!resolved_call)
141 {
142 // Check for a default implementation:
143 resolved_call =
144 call_resolver(classname, call_basename, true, exclude_abstract_methods);
145 }
146 if(!resolved_call)
147 {
148 // Finally accept any abstract definition, which will likely get stubbed:
149 resolved_call = call_resolver(classname, call_basename, true);
150 }
151 return resolved_call;
152}
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
bool empty() const
Definition: dstring.h:88
irep_idt get_full_component_identifier() const
Get the full name of this function.
resolve_inherited_componentt(const symbol_tablet &symbol_table)
See the operator() method comment.
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...
optionalt< 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.
Base class or struct that a class or struct inherits from.
Definition: std_types.h:252
struct_tag_typet & type()
Definition: std_types.cpp:77
const basest & bases() const
Get the collection of base classes/structs.
Definition: std_types.h:262
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
The symbol table.
Definition: symbol_table.h:14
Symbol table entry.
Definition: symbol.h:28
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
nonstd::optional< T > optionalt
Definition: optional.h:35
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< iteratort > make_range(iteratort begin, iteratort end)
Definition: range.h:524
Given a class and a component (either field or method), find the closest parent that defines that com...
optionalt< resolve_inherited_componentt::inherited_componentt > get_inherited_method_implementation(const irep_idt &call_basename, const irep_idt &classname, const symbol_tablet &symbol_table)
Given a class and a component, identify the concrete method it is resolved to.
static optionalt< smt_termt > get_identifier(const exprt &expr, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_handle_identifiers, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_identifiers)
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
Pre-defined types.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:308
Author: Diffblue Ltd.