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

Include dependency graph for remove_virtual_functions.cpp:

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. More...

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)
	Duplicate ASSUME instructions involving `argument_for_this` for `temp_var_for_this`. More...

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. More...

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. More...

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. More...

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. More...

void	remove_virtual_functions (goto_modelt &goto_model)
	Remove virtual function calls from the specified model. More...

void	remove_virtual_functions (goto_modelt &goto_model, const class_hierarchyt &class_hierarchy)
	Remove virtual function calls from the specified model. More...

void	remove_virtual_functions (goto_model_functiont &function)
	Remove virtual function calls from the specified model function May change the location numbers in `function`. More...

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`. More...

goto_programt::targett	remove_virtual_function (symbol_tablet &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. More...

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. More...

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
	)

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

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 860 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 96 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 202 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 843 of file remove_virtual_functions.cpp.

◆ remove_virtual_function() [2/2]

goto_programt::targett remove_virtual_function	(	symbol_tablet &	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 822 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 779 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 795 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 756 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 767 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 728 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 745 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 260 of file remove_virtual_functions.cpp.

Classes

Functions

Detailed Description

Function Documentation

◆ analyse_checks_directly_preceding_function_call()

◆ collect_virtual_function_callees()

◆ create_static_function_call()

◆ process_this_argument()

◆ remove_virtual_function() [1/2]

◆ remove_virtual_function() [2/2]

◆ remove_virtual_functions() [1/6]

◆ remove_virtual_functions() [2/6]

◆ remove_virtual_functions() [3/6]

◆ remove_virtual_functions() [4/6]

◆ remove_virtual_functions() [5/6]

◆ remove_virtual_functions() [6/6]

◆ replace_virtual_function_with_dispatch_table()