Loading...

Searching...

No Matches

remove_virtual_functions.cpp File Reference

Remove Virtual Function (Method) Calls. More...

#include "remove_virtual_functions.h"
#include <util/expr_iterator.h>
#include <util/expr_util.h>
#include <util/fresh_symbol.h>
#include <util/pointer_expr.h>
#include "class_hierarchy.h"
#include "class_identifier.h"
#include "goto_model.h"
#include "remove_skip.h"
#include "resolve_inherited_component.h"
#include <algorithm>

+ Include dependency graph for remove_virtual_functions.cpp:

[フレーム]

Go to the source code of this file.

Classes

class get_virtual_calleest

class remove_virtual_functionst

Functions

static void create_static_function_call (code_function_callt &call, const symbol_exprt &function_symbol, const namespacet &ns)

Create a concrete function call to replace a virtual one.

static goto_programt analyse_checks_directly_preceding_function_call (const goto_programt &goto_program, goto_programt::const_targett instr_it, const exprt &argument_for_this, const symbol_exprt &temp_var_for_this, const source_locationt &vcall_source_loc)

Duplicate ASSUME instructions involving argument_for_this for temp_var_for_this.

static void process_this_argument (const irep_idt &function_id, const goto_programt &goto_program, const goto_programt::targett target, exprt &argument_for_this, symbol_table_baset &symbol_table, const source_locationt &vcall_source_loc, goto_programt &new_code_for_this_argument)

If argument_for_this contains a dereference then create a temporary variable for it and use that instead.

static goto_programt::targett replace_virtual_function_with_dispatch_table (symbol_table_baset &symbol_table, const irep_idt &function_id, goto_programt &goto_program, goto_programt::targett target, const dispatch_table_entriest &functions, virtual_dispatch_fallback_actiont fallback_action)

Replace virtual function call with a static function call Achieved by substituting a virtual function with its most derived implementation.

void remove_virtual_functions (symbol_table_baset &symbol_table, goto_functionst &goto_functions)

Remove virtual function calls from all functions in the specified list and replace them with their most derived implementations.

void remove_virtual_functions (symbol_table_baset &symbol_table, goto_functionst &goto_functions, const class_hierarchyt &class_hierarchy)

Remove virtual function calls from all functions in the specified list and replace them with their most derived implementations.

void remove_virtual_functions (goto_modelt &goto_model)

Remove virtual function calls from the specified model.

void remove_virtual_functions (goto_modelt &goto_model, const class_hierarchyt &class_hierarchy)

Remove virtual function calls from the specified model.

void remove_virtual_functions (goto_model_functiont &function)

Remove virtual function calls from the specified model function May change the location numbers in function.

void remove_virtual_functions (goto_model_functiont &function, const class_hierarchyt &class_hierarchy)

Remove virtual function calls from the specified model function May change the location numbers in function.

goto_programt::targett remove_virtual_function (symbol_table_baset &symbol_table, const irep_idt &function_id, goto_programt &goto_program, goto_programt::targett instruction, const dispatch_table_entriest &dispatch_table, virtual_dispatch_fallback_actiont fallback_action)

Replace virtual function call with a static function call Achieved by substituting a virtual function with its most derived implementation.

goto_programt::targett remove_virtual_function (goto_modelt &goto_model, const irep_idt &function_id, goto_programt &goto_program, goto_programt::targett instruction, const dispatch_table_entriest &dispatch_table, virtual_dispatch_fallback_actiont fallback_action)

void collect_virtual_function_callees (const exprt &function, const symbol_table_baset &symbol_table, const class_hierarchyt &class_hierarchy, dispatch_table_entriest &overridden_functions)

Given a function expression representing a virtual method of a class, the function computes all overridden methods of that virtual method.

Detailed Description

Remove Virtual Function (Method) Calls.

Definition in file remove_virtual_functions.cpp.

Function Documentation

◆ analyse_checks_directly_preceding_function_call()

static goto_programt analyse_checks_directly_preceding_function_call ( const goto_programt & goto_program,

goto_programt::const_targett instr_it,

const exprt & argument_for_this,

const symbol_exprt & temp_var_for_this,

const source_locationt & vcall_source_loc

)

static

Duplicate ASSUME instructions involving argument_for_this for temp_var_for_this.

We only look at the ASSERT and ASSUME instructions which directly precede the virtual function call. This is mainly aimed at null checks, because local_safe_pointerst would otherwise lose track of known-not-null pointers due to the newly introduced assignment.

Parameters: goto_program The goto program containing the virtual function call

instr_it Iterator to the virtual function call in goto_program

argument_for_this The original expression for the this argument of the virtual function call

temp_var_for_this The new expression for the this argument of the virtual function call

vcall_source_loc The source location of the function call, which is used for new instructions that are added

Returns: A goto program consisting of all the amended asserts and assumes

Definition at line 145 of file remove_virtual_functions.cpp.

◆ collect_virtual_function_callees()

void collect_virtual_function_callees ( const exprt & function,

const symbol_table_baset & symbol_table,

const class_hierarchyt & class_hierarchy,

dispatch_table_entriest & overridden_functions

)

Given a function expression representing a virtual method of a class, the function computes all overridden methods of that virtual method.

Parameters: function The virtual function expression for which the overridden methods will be searched for.

symbol_table A symbol table.

class_hierarchy A class hierarchy.

[out] overridden_functions Output collection into which all overridden functions will be stored.

Definition at line 846 of file remove_virtual_functions.cpp.

◆ create_static_function_call()

static void create_static_function_call ( code_function_callt & call,

const symbol_exprt & function_symbol,

const namespacet & ns

)

static

Create a concrete function call to replace a virtual one.

Parameters: [in,out] call the function call to update

function_symbol the function to be called

ns namespace

Definition at line 94 of file remove_virtual_functions.cpp.

◆ process_this_argument()

static void process_this_argument ( const irep_idt & function_id,

const goto_programt & goto_program,

const goto_programt::targett target,

exprt & argument_for_this,

symbol_table_baset & symbol_table,

const source_locationt & vcall_source_loc,

goto_programt & new_code_for_this_argument

)

static

If argument_for_this contains a dereference then create a temporary variable for it and use that instead.

Parameters: function_id The identifier of the function we are currently analysing

goto_program The goto program containing the virtual function call

target Iterator to the virtual function call in goto_program

[in,out] argument_for_this The first argument of the function call

symbol_table The symbol table to add the new symbol to

vcall_source_loc The source location of the function call, which is used for new instructions that are added

[out] new_code_for_this_argument New instructions are added here

Definition at line 203 of file remove_virtual_functions.cpp.

◆ remove_virtual_function() [1/2]

goto_programt::targett remove_virtual_function ( goto_modelt & goto_model,

const irep_idt & function_id,

goto_programt & goto_program,

goto_programt::targett instruction,

const dispatch_table_entriest & dispatch_table,

virtual_dispatch_fallback_actiont fallback_action

)

Definition at line 829 of file remove_virtual_functions.cpp.

◆ remove_virtual_function() [2/2]

goto_programt::targett remove_virtual_function ( symbol_table_baset & symbol_table,

const irep_idt & function_id,

goto_programt & goto_program,

goto_programt::targett instruction,

const dispatch_table_entriest & dispatch_table,

virtual_dispatch_fallback_actiont fallback_action

)

Replace virtual function call with a static function call Achieved by substituting a virtual function with its most derived implementation.

If there's a type mismatch between implementation and the instance type or if fallback_action is set to ASSUME_FALSE, then function is substituted with a call to ASSUME(false)

Parameters: symbol_table Symbol table

function_id The identifier of the function we are currently analysing

[in,out] goto_program GOTO program to modify

instruction Iterator to the GOTO instruction in the supplied GOTO program to be removed. Must point to a function call

dispatch_table Dispatch table - all possible implementations of this function sorted from the least to the most derived

fallback_action - ASSUME_FALSE to replace virtual function calls with ASSUME(false) or CALL_LAST_FUNCTION to replace them with the most derived matching call

Returns: Returns a pointer to the statement in the supplied GOTO program after replaced function call

Definition at line 808 of file remove_virtual_functions.cpp.

◆ remove_virtual_functions() [1/6]

void remove_virtual_functions ( goto_model_functiont & function )

Remove virtual function calls from the specified model function May change the location numbers in function.

Parameters: function function from which virtual functions should be converted to explicit dispatch tables.

Definition at line 765 of file remove_virtual_functions.cpp.

◆ remove_virtual_functions() [2/6]

void remove_virtual_functions ( goto_model_functiont & function,

const class_hierarchyt & class_hierarchy

)

Remove virtual function calls from the specified model function May change the location numbers in function.

Parameters: function function from which virtual functions should be converted to explicit dispatch tables.

class_hierarchy class hierarchy derived from function.symbol_table This should already be populated (i.e. class_hierarchyt::operator() has already been called)

Definition at line 781 of file remove_virtual_functions.cpp.

◆ remove_virtual_functions() [3/6]

void remove_virtual_functions ( goto_modelt & goto_model )

Remove virtual function calls from the specified model.

Parameters: goto_model model from which to remove virtual functions

Definition at line 742 of file remove_virtual_functions.cpp.

◆ remove_virtual_functions() [4/6]

void remove_virtual_functions ( goto_modelt & goto_model,

const class_hierarchyt & class_hierarchy

)

Remove virtual function calls from the specified model.

Parameters: goto_model model from which to remove virtual functions

class_hierarchy class hierarchy derived from model.symbol_table This should already be populated (i.e. class_hierarchyt::operator() has already been called)

Definition at line 753 of file remove_virtual_functions.cpp.

◆ remove_virtual_functions() [5/6]

void remove_virtual_functions ( symbol_table_baset & symbol_table,

goto_functionst & goto_functions

)

Remove virtual function calls from all functions in the specified list and replace them with their most derived implementations.

Parameters: symbol_table symbol table associated with goto_functions

goto_functions functions from which to remove virtual function calls

Definition at line 714 of file remove_virtual_functions.cpp.

◆ remove_virtual_functions() [6/6]

void remove_virtual_functions ( symbol_table_baset & symbol_table,

goto_functionst & goto_functions,

const class_hierarchyt & class_hierarchy

)

Remove virtual function calls from all functions in the specified list and replace them with their most derived implementations.

Parameters: symbol_table symbol table associated with goto_functions

goto_functions functions from which to remove virtual function calls

class_hierarchy class hierarchy derived from symbol_table This should already be populated (i.e. class_hierarchyt::operator() has already been called)

Definition at line 731 of file remove_virtual_functions.cpp.

◆ replace_virtual_function_with_dispatch_table()

static goto_programt::targett replace_virtual_function_with_dispatch_table ( symbol_table_baset & symbol_table,

const irep_idt & function_id,

goto_programt & goto_program,

goto_programt::targett target,

const dispatch_table_entriest & functions,

virtual_dispatch_fallback_actiont fallback_action

)

static

Replace virtual function call with a static function call Achieved by substituting a virtual function with its most derived implementation.

If there's a type mismatch between implementation and the instance type or if fallback_action is set to ASSUME_FALSE, then function is substituted with a call to ASSUME(false)

Parameters: symbol_table Symbol table associated with goto_program

function_id The identifier of the function we are currently analysing

[in,out] goto_program GOTO program to modify

target Iterator to the GOTO instruction in the supplied GOTO program to be removed. Must point to a function call

functions Dispatch table - all possible implementations of this function sorted from the least to the most derived

fallback_action - ASSUME_FALSE to replace virtual function calls with ASSUME(false) or CALL_LAST_FUNCTION to replace them with the most derived matching call

Returns: Returns a pointer to the statement in the supplied GOTO program after replaced function call

Definition at line 265 of file remove_virtual_functions.cpp.