#include <remove_const_function_pointers.h>

Collaboration diagram for remove_const_function_pointerst:

Public Types
typedef std::unordered_set< symbol_exprt, irep_hash >	functionst

typedef std::list< exprt >	expressionst

Public Member Functions
	remove_const_function_pointerst (message_handlert &message_handler, const namespacet &ns, const symbol_table_baset &symbol_table)
	To take a function call on a function pointer, and if possible resolve it to a small collection of possible values. More...

bool	operator() (const exprt &base_expression, functionst &out_functions)
	To take a function call on a function pointer, and if possible resolve it to a small collection of possible values. More...

Private Member Functions
exprt	replace_const_symbols (const exprt &expression) const
	To collapse the symbols down to their values where possible This takes a very general approach, recreating the expr tree exactly as it was and ignoring what type of expressions are found and instead recurses over all the operands. More...

exprt	resolve_symbol (const symbol_exprt &symbol_expr) const
	Look up a symbol in the symbol table and return its value. More...

bool	try_resolve_function_call (const exprt &expr, functionst &out_functions)
	To resolve an expression to the specific function calls it can be. More...

bool	try_resolve_function_calls (const expressionst &exprs, functionst &out_functions)
	To resolve a collection of expressions to the specific function calls they can be. More...

bool	try_resolve_index_of_function_call (const index_exprt &index_expr, functionst &out_functions)
	To resolve an expression to the specific function calls it can be. More...

bool	try_resolve_member_function_call (const member_exprt &member_expr, functionst &out_functions)
	To resolve an expression to the specific function calls it can be. More...

bool	try_resolve_address_of_function_call (const address_of_exprt &address_expr, functionst &out_functions)
	To resolve an expression to the specific function calls it can be. More...

bool	try_resolve_dereference_function_call (const dereference_exprt &deref_expr, functionst &out_functions)
	To resolve an expression to the specific function calls it can be. More...

bool	try_resolve_typecast_function_call (const typecast_exprt &typecast_expr, functionst &out_functions)
	To resolve an expression to the specific function calls it can be. More...

bool	try_resolve_expression (const exprt &expr, expressionst &out_resolved_expression, bool &out_is_const)
	To squash various expr types to simplify the expression. More...

bool	try_resolve_index_of (const index_exprt &index_expr, expressionst &out_expressions, bool &out_is_const)
	To squash an index access by first finding the array it is accessing Then if the index can be resolved, return the squashed value. More...

bool	try_resolve_member (const member_exprt &member_expr, expressionst &out_expressions, bool &out_is_const)
	To squash an member access by first finding the struct it is accessing Then return the squashed value of the relevant component. More...

bool	try_resolve_dereference (const dereference_exprt &deref_expr, expressionst &out_expressions, bool &out_is_const)
	To squash a dereference access by first finding the address_of the dereference is dereferencing. More...

bool	try_resolve_typecast (const typecast_exprt &typecast_expr, expressionst &out_expressions, bool &out_is_const)
	To squash a typecast access. More...

bool	is_const_expression (const exprt &expression) const
	To evaluate the const-ness of the expression type. More...

bool	is_const_type (const typet &type) const
	To evaluate the const-ness of the type. More...

bool	try_resolve_index_value (const exprt &index_value_expr, mp_integer &out_array_index)
	Given an index into an array, resolve, if possible, the index that is being accessed. More...

exprt	get_component_value (const struct_exprt &struct_expr, const member_exprt &member_expr)
	To extract the value of the specific component within a struct. More...

Private Attributes
messaget	log

const namespacet &	ns

const symbol_table_baset &	symbol_table

Detailed Description

Definition at line 32 of file remove_const_function_pointers.h.

Member Typedef Documentation

◆ expressionst

typedef std::list<exprt> remove_const_function_pointerst::expressionst

Definition at line 36 of file remove_const_function_pointers.h.

◆ functionst

typedef std::unordered_set<symbol_exprt, irep_hash> remove_const_function_pointerst::functionst

Definition at line 35 of file remove_const_function_pointers.h.

Constructor & Destructor Documentation

◆ remove_const_function_pointerst()

remove_const_function_pointerst::remove_const_function_pointerst	(	message_handlert &	message_handler,
		const namespacet &	ns,
		const symbol_table_baset &	symbol_table
	)

To take a function call on a function pointer, and if possible resolve it to a small collection of possible values.

Parameters

message_handler	The message handler for messaget
ns	The namespace to use to resolve types
symbol_table	The symbol table to look up symbols in

Definition at line 34 of file remove_const_function_pointers.cpp.

Member Function Documentation

◆ get_component_value()

exprt remove_const_function_pointerst::get_component_value	(	const struct_exprt &	struct_expr,
		const member_exprt &	member_expr
	)

private

To extract the value of the specific component within a struct.

Parameters

struct_expr	The expression of the structure being accessed
member_expr	The expression saying which component is being accessed

Returns: Returns the value of a specific component for a given struct expression.

Definition at line 800 of file remove_const_function_pointers.cpp.

◆ is_const_expression()

bool remove_const_function_pointerst::is_const_expression ( const exprt & expression ) const

private

To evaluate the const-ness of the expression type.

Parameters

expression The expression to check

Returns: Returns true if the type of the expression is constant.

Definition at line 777 of file remove_const_function_pointers.cpp.

◆ is_const_type()

bool remove_const_function_pointerst::is_const_type ( const typet & type ) const

private

To evaluate the const-ness of the type.

Parameters

type	The type to check

Returns: Returns true if the type has ID_C_constant or is an array since arrays are implicitly const in C.

Definition at line 787 of file remove_const_function_pointers.cpp.

◆ operator()()

bool remove_const_function_pointerst::operator()	(	const exprt &	base_expression,
		functionst &	out_functions
	)

To take a function call on a function pointer, and if possible resolve it to a small collection of possible values.

It will resolve function pointers that are const and: - assigned directly to a function - assigned to a value in an array of functions - assigned to a const struct component Or variations within.

Parameters

base_expression	The function call through a function pointer
out_functions	The functions that (symbols of type ID_code) the base expression could take.

Returns: Returns true if it was able to resolve the call, false if not. If it returns true, out_functions will be populated by all the possible values the function pointer could be.

Definition at line 52 of file remove_const_function_pointers.cpp.

◆ replace_const_symbols()

exprt remove_const_function_pointerst::replace_const_symbols ( const exprt & expression ) const

private

To collapse the symbols down to their values where possible This takes a very general approach, recreating the expr tree exactly as it was and ignoring what type of expressions are found and instead recurses over all the operands.

Parameters

expression The expression to resolve symbols in

Returns: Returns a modified version of the expression, with all const symbols resolved to their actual values.

Definition at line 68 of file remove_const_function_pointers.cpp.

◆ resolve_symbol()

exprt remove_const_function_pointerst::resolve_symbol ( const symbol_exprt & symbol_expr ) const

private

Look up a symbol in the symbol table and return its value.

Parameters

symbol_expr The symbol expression

Returns: The expression value of the symbol.

Definition at line 109 of file remove_const_function_pointers.cpp.

◆ try_resolve_address_of_function_call()

bool remove_const_function_pointerst::try_resolve_address_of_function_call	(	const address_of_exprt &	address_expr,
		functionst &	out_functions
	)

private

To resolve an expression to the specific function calls it can be.

Specifically, this function deals with address_of expressions.

Parameters

address_expr	The address_of expression to resolve to possible function calls
out_functions	The functions this expression could be

Returns: Returns true if it was able to resolve the address_of expression to some specific functions. If this is the case, out_functions will contain the possible functions.

Definition at line 306 of file remove_const_function_pointers.cpp.

◆ try_resolve_dereference()

bool remove_const_function_pointerst::try_resolve_dereference	(	const dereference_exprt &	deref_expr,
		expressionst &	out_expressions,
		bool &	out_is_const
	)

private

To squash a dereference access by first finding the address_of the dereference is dereferencing.

Then return the squashed value of the relevant component.

Parameters

deref_expr	The dereference expression to resolve.
out_expressions	The expressions this dereference could be
out_is_const	Is the squashed expression constant

Returns: Returns true if it was able to squash the dereference expression If this is the case, out_expressions will contain the possible values this dereference could return The out_is_const will return whether the object that gets dereferenced is constant.

Definition at line 677 of file remove_const_function_pointers.cpp.

◆ try_resolve_dereference_function_call()

bool remove_const_function_pointerst::try_resolve_dereference_function_call	(	const dereference_exprt &	deref_expr,
		functionst &	out_functions
	)

private

To resolve an expression to the specific function calls it can be.

Specifically, this function deals with dereference expressions by using try_resolve_dereferebce and then recursing on its value.

Parameters

deref_expr	The dereference expression to resolve to possible function calls
out_functions	The functions this expression could be

Returns: Returns true if it was able to resolve the dereference expression to some specific functions. If this is the case, out_functions will contain the possible functions.

Definition at line 327 of file remove_const_function_pointers.cpp.

◆ try_resolve_expression()

bool remove_const_function_pointerst::try_resolve_expression	(	const exprt &	expr,
		expressionst &	out_resolved_expression,
		bool &	out_is_const
	)

private

To squash various expr types to simplify the expression.

ID_index -> dig to find ID_array and get the values out of it ID_member -> dig to find ID_struct and extract the component value ID_dereference -> dig to find ID_address_of and extract the value ID_typecast -> return the value ID_symbol -> return false, const symbols are squashed first and non const symbols cannot be squashed Everything else -> unchanged

Parameters

expr	The expression to try and squash
out_resolved_expression	The squashed version of this expression
out_is_const	Is the squashed expression constant

Returns: Returns true providing the squashing went OK (note it may not have squashed anything). The out_resolved_expression will in this case be all the possible squashed versions of the supplied expression. The out_is_const will return whether the squashed value is suitably const (e.g. if we squashed a struct access, was the struct const).

Definition at line 396 of file remove_const_function_pointers.cpp.

◆ try_resolve_function_call()

bool remove_const_function_pointerst::try_resolve_function_call	(	const exprt &	expr,
		functionst &	out_functions
	)

private

To resolve an expression to the specific function calls it can be.

This is different to try_resolve_expression which isn't explicitly looking for functions and is instead just trying to squash particular exprt structures.

Parameters

expr	The expression to get the possible function calls
out_functions	The functions this expression could be resolved to

Returns: Returns true if it was able to resolve the expression to some specific functions. If this is the case, out_functions will contain the possible functions.

Definition at line 124 of file remove_const_function_pointers.cpp.

◆ try_resolve_function_calls()

bool remove_const_function_pointerst::try_resolve_function_calls	(	const expressionst &	exprs,
		functionst &	out_functions
	)

private

To resolve a collection of expressions to the specific function calls they can be.

Returns a collection if and only if all of them can be resolved.

Parameters

exprs	The expressions to evaluate
out_functions	The functions these expressions resolve to

Returns: Returns true if able to resolve each of the expressions down to one or more functions.

Definition at line 208 of file remove_const_function_pointers.cpp.

◆ try_resolve_index_of()

bool remove_const_function_pointerst::try_resolve_index_of	(	const index_exprt &	index_expr,
		expressionst &	out_expressions,
		bool &	out_is_const
	)

private

To squash an index access by first finding the array it is accessing Then if the index can be resolved, return the squashed value.

If the index can't be determined then squash each value in the array and return them all.

Parameters

index_expr	The index expression to to resolve
out_expressions	The expressions this expression could be
out_is_const	Is the squashed expression constant

Returns: Returns true if it was able to squash the index expression If this is the case, out_expressions will contain the possible values this index_of could return The out_is_const will return whether either the array itself is const, or the values of the array are const.

Definition at line 508 of file remove_const_function_pointers.cpp.

◆ try_resolve_index_of_function_call()

bool remove_const_function_pointerst::try_resolve_index_of_function_call	(	const index_exprt &	index_expr,
		functionst &	out_functions
	)

private

To resolve an expression to the specific function calls it can be.

Specifically, this function deals with index expressions where it squashes its array and squash its index If we can get a precise number for the index, we try_resolve_function_call on its value otherwise try_resolve_function_call on each and return the union of them all

Parameters

index_expr	The index expression to resolve to possible function calls
out_functions	The functions this expression could be

Returns: Returns true if it was able to resolve the index expression to some specific functions. If this is the case, out_functions will contain the possible functions.

Definition at line 243 of file remove_const_function_pointers.cpp.

◆ try_resolve_index_value()

bool remove_const_function_pointerst::try_resolve_index_value	(	const exprt &	expr,
		mp_integer &	out_array_index
	)

private

Given an index into an array, resolve, if possible, the index that is being accessed.

This deals with symbols and typecasts to constant values.

Parameters

expr	The expression of the index of the index expression (e.g. index_exprt::index())
out_array_index	The constant value the index takes

Returns: Returns true if was able to find a constant value for the index expression. If true, then out_array_index will be the index within the array that the function pointer is pointing to.

Definition at line 465 of file remove_const_function_pointers.cpp.

◆ try_resolve_member()

bool remove_const_function_pointerst::try_resolve_member	(	const member_exprt &	member_expr,
		expressionst &	out_expressions,
		bool &	out_is_const
	)

private

To squash an member access by first finding the struct it is accessing Then return the squashed value of the relevant component.

Parameters

member_expr	The member expression to resolve.
out_expressions	The expressions this component could be
out_is_const	Is the squashed expression constant

Returns: Returns true if it was able to squash the member expression If this is the case, out_expressions will contain the possible values this member could return The out_is_const will return whether the struct is const.

Definition at line 610 of file remove_const_function_pointers.cpp.

◆ try_resolve_member_function_call()

bool remove_const_function_pointerst::try_resolve_member_function_call	(	const member_exprt &	member_expr,
		functionst &	out_functions
	)

private

To resolve an expression to the specific function calls it can be.

Specifically, this function deals with member expressions by using try_resolve_member and then recursing on its value.

Parameters

member_expr	The member expression to resolve to possible function calls
out_functions	The functions this expression could be

Returns: Returns true if it was able to resolve the member expression to some specific functions. If this is the case, out_functions will contain the possible functions.

Definition at line 275 of file remove_const_function_pointers.cpp.

◆ try_resolve_typecast()

bool remove_const_function_pointerst::try_resolve_typecast	(	const typecast_exprt &	typecast_expr,
		expressionst &	out_expressions,
		bool &	out_is_const
	)

private

To squash a typecast access.

Parameters

typecast_expr	The typecast expression to resolve.
out_expressions	The expressions this typecast could be
out_is_const	Is the squashed expression constant

Returns: Returns true if it was able to squash the typecast expression If this is the case, out_expressions will contain the possible values after removing the typecast.

Definition at line 747 of file remove_const_function_pointers.cpp.

◆ try_resolve_typecast_function_call()

bool remove_const_function_pointerst::try_resolve_typecast_function_call	(	const typecast_exprt &	typecast_expr,
		functionst &	out_functions
	)

private

To resolve an expression to the specific function calls it can be.

Specifically, this function deals with typecast expressions by looking at the type cast values.

Parameters

typecast_expr	The typecast expression to resolve to possible function calls
out_functions	The functions this expression could be

Returns: Returns true if it was able to resolve the typecast expression to some specific functions. If this is the case, out_functions will contain the possible functions.

Definition at line 359 of file remove_const_function_pointers.cpp.

Member Data Documentation

◆ log

messaget remove_const_function_pointerst::log

private

Definition at line 104 of file remove_const_function_pointers.h.

◆ ns

const namespacet& remove_const_function_pointerst::ns

private

Definition at line 105 of file remove_const_function_pointers.h.

◆ symbol_table

const symbol_table_baset& remove_const_function_pointerst::symbol_table

private

Definition at line 106 of file remove_const_function_pointers.h.

The documentation for this class was generated from the following files:

/home/runner/work/cbmc/cbmc/src/goto-programs/remove_const_function_pointers.h
/home/runner/work/cbmc/cbmc/src/goto-programs/remove_const_function_pointers.cpp

Public Types

Public Member Functions

Private Member Functions

Private Attributes

Detailed Description

Member Typedef Documentation

◆ expressionst

◆ functionst

Constructor & Destructor Documentation

◆ remove_const_function_pointerst()

Member Function Documentation

◆ get_component_value()

◆ is_const_expression()

◆ is_const_type()

◆ operator()()

◆ replace_const_symbols()

◆ resolve_symbol()

◆ try_resolve_address_of_function_call()

◆ try_resolve_dereference()

◆ try_resolve_dereference_function_call()

◆ try_resolve_expression()

◆ try_resolve_function_call()

◆ try_resolve_function_calls()

◆ try_resolve_index_of()

◆ try_resolve_index_of_function_call()

◆ try_resolve_index_value()

◆ try_resolve_member()

◆ try_resolve_member_function_call()

◆ try_resolve_typecast()

◆ try_resolve_typecast_function_call()

Member Data Documentation

◆ log

◆ ns

◆ symbol_table