CBMC
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 
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
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:36
symbol_tablet
The symbol table.
Definition: symbol_table.h:13
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:308
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:128
resolve_inherited_componentt::inherited_componentt
Definition: resolve_inherited_component.h:29
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:108
resolve_inherited_componentt::inherited_componentt::class_identifier
irep_idt class_identifier
Definition: resolve_inherited_component.h:46
resolve_inherited_component.h
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
get_identifier
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)
Definition: smt2_incremental_decision_procedure.cpp:328
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
std_types.h
struct_typet::bases
const basest & bases() const
Get the collection of base classes/structs.
Definition: std_types.h:262
range.h
dstringt::empty
bool empty() const
Definition: dstring.h:88
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
resolve_inherited_componentt::symbol_table
const symbol_tablet & symbol_table
Definition: resolve_inherited_component.h:62
symbolt
Symbol table entry.
Definition: symbol.h:27
struct_typet::baset::type
struct_tag_typet & type()
Definition: std_types.cpp:83
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:96
symbol_table.h
Author: Diffblue Ltd.
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:19
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:38
struct_typet::baset
Base class or struct that a class or struct inherits from.
Definition: std_types.h:251
resolve_inherited_componentt
Definition: resolve_inherited_component.h:24