forked from diffblue/cbmc
-
Notifications
You must be signed in to change notification settings - Fork 1
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
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.
- Loading branch information
Showing
8 changed files
with
197 additions
and
196 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -14,7 +14,7 @@ Author: Daniel Kroening, [email protected] | |
#include "class_hierarchy.h" | ||
#include "class_identifier.h" | ||
|
||
#include <goto-programs/resolve_concrete_function_call.h> | ||
#include <goto-programs/resolve_inherited_component.h> | ||
|
||
#include <util/c_types.h> | ||
#include <util/prefix.h> | ||
|
@@ -48,7 +48,7 @@ class remove_virtual_functionst | |
|
||
void get_functions(const exprt &, dispatch_table_entriest &); | ||
typedef std::function< | ||
resolve_concrete_function_callt::concrete_function_callt( | ||
resolve_inherited_componentt::inherited_componentt( | ||
const irep_idt &, | ||
const irep_idt &)> | ||
function_call_resolvert; | ||
|
@@ -343,13 +343,14 @@ void remove_virtual_functionst::get_child_functions_rec( | |
} | ||
if(function.symbol_expr == symbol_exprt()) | ||
{ | ||
const resolve_concrete_function_callt::concrete_function_callt | ||
const resolve_inherited_componentt::inherited_componentt | ||
&resolved_call = resolve_function_call(child, component_name); | ||
if(resolved_call.is_valid()) | ||
{ | ||
function.class_id = resolved_call.get_class_identifier(); | ||
const symbolt &called_symbol = | ||
symbol_table.lookup_ref(resolved_call.get_virtual_method_name()); | ||
symbol_table.lookup_ref( | ||
resolved_call.get_full_component_identifier()); | ||
|
||
function.symbol_expr = called_symbol.symbol_expr(); | ||
function.symbol_expr.set( | ||
|
@@ -384,15 +385,15 @@ void remove_virtual_functionst::get_functions( | |
const std::string function_name_string(id2string(function_name)); | ||
INVARIANT(!class_id.empty(), "All virtual functions must have a class"); | ||
|
||
resolve_concrete_function_callt get_virtual_call_target( | ||
resolve_inherited_componentt get_virtual_call_target( | ||
symbol_table, class_hierarchy); | ||
const function_call_resolvert resolve_function_call = | ||
[&get_virtual_call_target]( | ||
const irep_idt &class_id, const irep_idt &function_name) { | ||
return get_virtual_call_target(class_id, function_name); | ||
}; | ||
|
||
const resolve_concrete_function_callt::concrete_function_callt | ||
const resolve_inherited_componentt::inherited_componentt | ||
&resolved_call = get_virtual_call_target(class_id, function_name); | ||
|
||
dispatch_table_entryt root_function; | ||
|
@@ -402,7 +403,7 @@ void remove_virtual_functionst::get_functions( | |
root_function.class_id=resolved_call.get_class_identifier(); | ||
|
||
const symbolt &called_symbol = | ||
symbol_table.lookup_ref(resolved_call.get_virtual_method_name()); | ||
symbol_table.lookup_ref(resolved_call.get_full_component_identifier()); | ||
|
||
root_function.symbol_expr=called_symbol.symbol_expr(); | ||
root_function.symbol_expr.set( | ||
|
@@ -454,7 +455,7 @@ exprt remove_virtual_functionst::get_method( | |
const irep_idt &component_name) const | ||
{ | ||
const irep_idt &id= | ||
resolve_concrete_function_callt::build_virtual_method_name( | ||
resolve_inherited_componentt::build_full_component_identifier( | ||
class_id, component_name); | ||
|
||
const symbolt *symbol; | ||
|
This file was deleted.
Oops, something went wrong.
This file was deleted.
Oops, something went wrong.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,102 @@ | ||
/*******************************************************************\ | ||
Module: GOTO Program Utilities | ||
Author: DiffBlue Limited. All rights reserved. | ||
\*******************************************************************/ | ||
|
||
#include <algorithm> | ||
|
||
#include "resolve_inherited_component.h" | ||
|
||
/// See the operator() method comment. | ||
/// \param symbol_table: The symbol table to resolve the component against | ||
resolve_inherited_componentt::resolve_inherited_componentt( | ||
const symbol_tablet &symbol_table): | ||
symbol_table(symbol_table) | ||
{ | ||
class_hierarchy(symbol_table); | ||
} | ||
|
||
/// See the operator() method comment | ||
/// \param symbol_table: The symbol table to resolve the component against | ||
/// \param class_hierarchy: A prebuilt class_hierachy based on the symbol_table | ||
/// | ||
resolve_inherited_componentt::resolve_inherited_componentt( | ||
const symbol_tablet &symbol_table, const class_hierarchyt &class_hierarchy): | ||
class_hierarchy(class_hierarchy), | ||
symbol_table(symbol_table) | ||
{ | ||
// We require the class_hierarchy to be already populated if we are being | ||
// supplied it. | ||
PRECONDITION(!class_hierarchy.class_map.empty()); | ||
} | ||
|
||
/// Given a class and a component, identify the concrete field or method it is | ||
/// resolved to. For example, a reference Child.abc refers to Child's method or | ||
/// field if it exists, or else Parent.abc, and so on regarding Parent's | ||
/// ancestors. If none are found, an empty string will be returned. | ||
/// \param class_id: The name of the class the function is being called on | ||
/// \param component_name: The base name of the component (i.e. without the | ||
/// class specifier) | ||
/// \return The concrete component that has been resolved | ||
resolve_inherited_componentt::inherited_componentt | ||
resolve_inherited_componentt::operator()( | ||
const irep_idt &class_id, const irep_idt &component_name) | ||
{ | ||
PRECONDITION(!class_id.empty()); | ||
PRECONDITION(!component_name.empty()); | ||
|
||
irep_idt current_class=class_id; | ||
while(!current_class.empty()) | ||
{ | ||
const irep_idt &full_component_identifier= | ||
build_full_component_identifier(current_class, component_name); | ||
|
||
if(symbol_table.has_symbol(full_component_identifier)) | ||
{ | ||
return inherited_componentt(current_class, component_name); | ||
} | ||
|
||
const class_hierarchyt::idst &parents= | ||
class_hierarchy.class_map[current_class].parents; | ||
|
||
if(parents.empty()) | ||
break; | ||
current_class=parents.front(); | ||
} | ||
|
||
return inherited_componentt(); | ||
} | ||
|
||
/// Build a component name as found in a GOTO symbol table equivalent to the | ||
/// name of a concrete component component_name on class class_name | ||
/// \param component_name: The name of the component | ||
/// \param class_name: The class the implementation would be found on. | ||
/// \return A name for looking up in the symbol table for classes `class_name`'s | ||
/// component `component_name` | ||
irep_idt resolve_inherited_componentt::build_full_component_identifier( | ||
const irep_idt &class_name, const irep_idt &component_name) | ||
{ | ||
// Verify the parameters are called in the correct order. | ||
PRECONDITION(id2string(class_name).find("::")!=std::string::npos); | ||
PRECONDITION(id2string(component_name).find("::")==std::string::npos); | ||
return id2string(class_name)+'.'+id2string(component_name); | ||
} | ||
|
||
/// Get the full name of this function | ||
/// \return The symbol name for this function call | ||
irep_idt resolve_inherited_componentt::inherited_componentt:: | ||
get_full_component_identifier() const | ||
{ | ||
return resolve_inherited_componentt::build_full_component_identifier( | ||
class_identifier, component_identifier); | ||
} | ||
|
||
/// Use to check if this inherited_componentt has been fully constructed. | ||
/// \return True if this represents a real concrete component | ||
bool resolve_inherited_componentt::inherited_componentt::is_valid() const | ||
{ | ||
return !class_identifier.empty(); | ||
} |
Oops, something went wrong.