Skip to content

Commit f3160e1

Browse files
committed
resolve_concrete_function_callt -> resolve_inherited_componentt
This actually doesn't have any logic specific to function calls, and can be used to resolve inherited fields too.
1 parent ef08ae2 commit f3160e1

8 files changed

+197
-196
lines changed

src/goto-programs/Makefile

+1-1
Original file line numberDiff line numberDiff line change
@@ -52,7 +52,7 @@ SRC = basic_blocks.cpp \
5252
remove_vector.cpp \
5353
remove_virtual_functions.cpp \
5454
replace_java_nondet.cpp \
55-
resolve_concrete_function_call.cpp \
55+
resolve_inherited_component.cpp \
5656
safety_checker.cpp \
5757
set_properties.cpp \
5858
show_goto_functions.cpp \

src/goto-programs/remove_virtual_functions.cpp

+9-8
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@ Author: Daniel Kroening, [email protected]
1414
#include "class_hierarchy.h"
1515
#include "class_identifier.h"
1616

17-
#include <goto-programs/resolve_concrete_function_call.h>
17+
#include <goto-programs/resolve_inherited_component.h>
1818

1919
#include <util/c_types.h>
2020
#include <util/prefix.h>
@@ -48,7 +48,7 @@ class remove_virtual_functionst
4848

4949
void get_functions(const exprt &, dispatch_table_entriest &);
5050
typedef std::function<
51-
resolve_concrete_function_callt::concrete_function_callt(
51+
resolve_inherited_componentt::inherited_componentt(
5252
const irep_idt &,
5353
const irep_idt &)>
5454
function_call_resolvert;
@@ -343,13 +343,14 @@ void remove_virtual_functionst::get_child_functions_rec(
343343
}
344344
if(function.symbol_expr == symbol_exprt())
345345
{
346-
const resolve_concrete_function_callt::concrete_function_callt
346+
const resolve_inherited_componentt::inherited_componentt
347347
&resolved_call = resolve_function_call(child, component_name);
348348
if(resolved_call.is_valid())
349349
{
350350
function.class_id = resolved_call.get_class_identifier();
351351
const symbolt &called_symbol =
352-
symbol_table.lookup_ref(resolved_call.get_virtual_method_name());
352+
symbol_table.lookup_ref(
353+
resolved_call.get_full_component_identifier());
353354

354355
function.symbol_expr = called_symbol.symbol_expr();
355356
function.symbol_expr.set(
@@ -384,15 +385,15 @@ void remove_virtual_functionst::get_functions(
384385
const std::string function_name_string(id2string(function_name));
385386
INVARIANT(!class_id.empty(), "All virtual functions must have a class");
386387

387-
resolve_concrete_function_callt get_virtual_call_target(
388+
resolve_inherited_componentt get_virtual_call_target(
388389
symbol_table, class_hierarchy);
389390
const function_call_resolvert resolve_function_call =
390391
[&get_virtual_call_target](
391392
const irep_idt &class_id, const irep_idt &function_name) {
392393
return get_virtual_call_target(class_id, function_name);
393394
};
394395

395-
const resolve_concrete_function_callt::concrete_function_callt
396+
const resolve_inherited_componentt::inherited_componentt
396397
&resolved_call = get_virtual_call_target(class_id, function_name);
397398

398399
dispatch_table_entryt root_function;
@@ -402,7 +403,7 @@ void remove_virtual_functionst::get_functions(
402403
root_function.class_id=resolved_call.get_class_identifier();
403404

404405
const symbolt &called_symbol =
405-
symbol_table.lookup_ref(resolved_call.get_virtual_method_name());
406+
symbol_table.lookup_ref(resolved_call.get_full_component_identifier());
406407

407408
root_function.symbol_expr=called_symbol.symbol_expr();
408409
root_function.symbol_expr.set(
@@ -454,7 +455,7 @@ exprt remove_virtual_functionst::get_method(
454455
const irep_idt &component_name) const
455456
{
456457
const irep_idt &id=
457-
resolve_concrete_function_callt::build_virtual_method_name(
458+
resolve_inherited_componentt::build_full_component_identifier(
458459
class_id, component_name);
459460

460461
const symbolt *symbol;

src/goto-programs/resolve_concrete_function_call.cpp

-102
This file was deleted.

src/goto-programs/resolve_concrete_function_call.h

-75
This file was deleted.
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,102 @@
1+
/*******************************************************************\
2+
3+
Module: GOTO Program Utilities
4+
5+
Author: DiffBlue Limited. All rights reserved.
6+
7+
\*******************************************************************/
8+
9+
#include <algorithm>
10+
11+
#include "resolve_inherited_component.h"
12+
13+
/// See the operator() method comment.
14+
/// \param symbol_table: The symbol table to resolve the component against
15+
resolve_inherited_componentt::resolve_inherited_componentt(
16+
const symbol_tablet &symbol_table):
17+
symbol_table(symbol_table)
18+
{
19+
class_hierarchy(symbol_table);
20+
}
21+
22+
/// See the operator() method comment
23+
/// \param symbol_table: The symbol table to resolve the component against
24+
/// \param class_hierarchy: A prebuilt class_hierachy based on the symbol_table
25+
///
26+
resolve_inherited_componentt::resolve_inherited_componentt(
27+
const symbol_tablet &symbol_table, const class_hierarchyt &class_hierarchy):
28+
class_hierarchy(class_hierarchy),
29+
symbol_table(symbol_table)
30+
{
31+
// We require the class_hierarchy to be already populated if we are being
32+
// supplied it.
33+
PRECONDITION(!class_hierarchy.class_map.empty());
34+
}
35+
36+
/// Given a class and a component, identify the concrete field or method it is
37+
/// resolved to. For example, a reference Child.abc refers to Child's method or
38+
/// field if it exists, or else Parent.abc, and so on regarding Parent's
39+
/// ancestors. If none are found, an empty string will be returned.
40+
/// \param class_id: The name of the class the function is being called on
41+
/// \param component_name: The base name of the component (i.e. without the
42+
/// class specifier)
43+
/// \return The concrete component that has been resolved
44+
resolve_inherited_componentt::inherited_componentt
45+
resolve_inherited_componentt::operator()(
46+
const irep_idt &class_id, const irep_idt &component_name)
47+
{
48+
PRECONDITION(!class_id.empty());
49+
PRECONDITION(!component_name.empty());
50+
51+
irep_idt current_class=class_id;
52+
while(!current_class.empty())
53+
{
54+
const irep_idt &full_component_identifier=
55+
build_full_component_identifier(current_class, component_name);
56+
57+
if(symbol_table.has_symbol(full_component_identifier))
58+
{
59+
return inherited_componentt(current_class, component_name);
60+
}
61+
62+
const class_hierarchyt::idst &parents=
63+
class_hierarchy.class_map[current_class].parents;
64+
65+
if(parents.empty())
66+
break;
67+
current_class=parents.front();
68+
}
69+
70+
return inherited_componentt();
71+
}
72+
73+
/// Build a component name as found in a GOTO symbol table equivalent to the
74+
/// name of a concrete component component_name on class class_name
75+
/// \param component_name: The name of the component
76+
/// \param class_name: The class the implementation would be found on.
77+
/// \return A name for looking up in the symbol table for classes `class_name`'s
78+
/// component `component_name`
79+
irep_idt resolve_inherited_componentt::build_full_component_identifier(
80+
const irep_idt &class_name, const irep_idt &component_name)
81+
{
82+
// Verify the parameters are called in the correct order.
83+
PRECONDITION(id2string(class_name).find("::")!=std::string::npos);
84+
PRECONDITION(id2string(component_name).find("::")==std::string::npos);
85+
return id2string(class_name)+'.'+id2string(component_name);
86+
}
87+
88+
/// Get the full name of this function
89+
/// \return The symbol name for this function call
90+
irep_idt resolve_inherited_componentt::inherited_componentt::
91+
get_full_component_identifier() const
92+
{
93+
return resolve_inherited_componentt::build_full_component_identifier(
94+
class_identifier, component_identifier);
95+
}
96+
97+
/// Use to check if this inherited_componentt has been fully constructed.
98+
/// \return True if this represents a real concrete component
99+
bool resolve_inherited_componentt::inherited_componentt::is_valid() const
100+
{
101+
return !class_identifier.empty();
102+
}

0 commit comments

Comments
 (0)