cprover
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 <algorithm>
10 
12 
16  const symbol_tablet &symbol_table)
17  : symbol_table(symbol_table)
18 {
19 }
20 
35  const irep_idt &class_id,
36  const irep_idt &component_name,
37  bool include_interfaces,
38  const std::function<bool(const symbolt &)> user_filter)
39 {
40  PRECONDITION(!class_id.empty());
41  PRECONDITION(!component_name.empty());
42 
43  std::vector<irep_idt> classes_to_visit;
44  classes_to_visit.push_back(class_id);
45  while(!classes_to_visit.empty())
46  {
47  irep_idt current_class = classes_to_visit.back();
48  classes_to_visit.pop_back();
49 
50  const irep_idt &full_component_identifier=
51  build_full_component_identifier(current_class, component_name);
52 
53  const symbolt *symbol = symbol_table.lookup(full_component_identifier);
54  if(symbol && user_filter(*symbol))
55  {
56  return inherited_componentt(current_class, component_name);
57  }
58 
59  const auto current_class_symbol_it =
60  symbol_table.symbols.find(current_class);
61 
62  if(current_class_symbol_it != symbol_table.symbols.end())
63  {
64  const auto parents =
65  make_range(to_struct_type(current_class_symbol_it->second.type).bases())
66  .map([](const struct_typet::baset &base) {
67  return base.type().get_identifier();
68  });
69 
70  if(include_interfaces)
71  {
72  classes_to_visit.insert(
73  classes_to_visit.end(), parents.begin(), parents.end());
74  }
75  else
76  {
77  if(!parents.empty())
78  classes_to_visit.push_back(*parents.begin());
79  }
80  }
81  }
82 
83  return {};
84 }
85 
93  const irep_idt &class_name, const irep_idt &component_name)
94 {
95  // Verify the parameters are called in the correct order.
96  PRECONDITION(id2string(class_name).find("::")!=std::string::npos);
97  PRECONDITION(id2string(component_name).find("::")==std::string::npos);
98  return id2string(class_name)+'.'+id2string(component_name);
99 }
100 
105 {
108 }
109 
125  const irep_idt &call_basename,
126  const irep_idt &classname,
128 {
130  auto exclude_abstract_methods = [&](const symbolt &symbol) {
131  return !symbol.type.get_bool(ID_C_abstract);
132  };
133 
134  auto resolved_call =
135  call_resolver(classname, call_basename, false, exclude_abstract_methods);
136  if(!resolved_call)
137  {
138  // Check for a default implementation:
139  resolved_call =
140  call_resolver(classname, call_basename, true, exclude_abstract_methods);
141  }
142  if(!resolved_call)
143  {
144  // Finally accept any abstract definition, which will likely get stubbed:
145  resolved_call = call_resolver(classname, call_basename, true);
146  }
147  return resolved_call;
148 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:303
get_inherited_method_implementation
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.
Definition: resolve_inherited_component.cpp:124
resolve_inherited_componentt::inherited_componentt
Definition: resolve_inherited_component.h:27
resolve_inherited_componentt::inherited_componentt::component_identifier
irep_idt component_identifier
Definition: resolve_inherited_component.h:44
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:104
resolve_inherited_componentt::inherited_componentt::class_identifier
irep_idt class_identifier
Definition: resolve_inherited_component.h:43
resolve_inherited_component.h
Given a class and a component (either field or method), find the closest parent that defines that com...
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
struct_typet::bases
const basest & bases() const
Get the collection of base classes/structs.
Definition: std_types.h:257
dstringt::empty
bool empty() const
Definition: dstring.h:88
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
struct_typet::baset::type
struct_tag_typet & type()
Definition: std_types.cpp:73
resolve_inherited_componentt::symbol_table
const symbol_tablet & symbol_table
Definition: resolve_inherited_component.h:59
symbolt
Symbol table entry.
Definition: symbol.h:28
symbol_table_baset::symbols
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Definition: symbol_table_base.h:30
symbol_table_baset::lookup
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:95
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:92
make_range
ranget< iteratort > make_range(iteratort begin, iteratort end)
Definition: range.h:524
resolve_inherited_componentt::resolve_inherited_componentt
resolve_inherited_componentt(const symbol_tablet &symbol_table)
See the operator() method comment.
Definition: resolve_inherited_component.cpp:15
resolve_inherited_componentt::operator()
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.
Definition: resolve_inherited_component.cpp:34
struct_typet::baset
Base class or struct that a class or struct inherits from.
Definition: std_types.h:247
resolve_inherited_componentt
Definition: resolve_inherited_component.h:22