remove_instanceof.cpp File Reference

#include "remove_instanceof.h"
#include <goto-programs/class_hierarchy.h>
#include <goto-programs/class_identifier.h>
#include <goto-programs/goto_model.h>
#include <java_bytecode/java_types.h>
#include <util/arith_tools.h>

Include dependency graph for remove_instanceof.cpp:

Go to the source code of this file.

Classes
class	remove_instanceoft

Functions
static exprt	subtype_expr (const exprt &classid_field, const irep_idt &target_type, const class_hierarchyt &class_hierarchy)
	Produce an expression of the form classid_field == "A" || classid_field == "B" || ... where A, B, ... More...
static bool	contains_instanceof (const exprt &e)
void	remove_instanceof (const irep_idt &function_identifier, goto_programt::targett target, goto_programt &goto_program, symbol_table_baset &symbol_table, const class_hierarchyt &class_hierarchy, message_handlert &message_handler)
	Replace an instanceof in the expression or guard of the passed instruction of the given function body with an explicit class-identifier test. More...
void	remove_instanceof (const irep_idt &function_identifier, goto_functionst::goto_functiont &function, symbol_table_baset &symbol_table, const class_hierarchyt &class_hierarchy, message_handlert &message_handler)
	Replace every instanceof in the passed function with an explicit class-identifier test. More...
void	remove_instanceof (goto_functionst &goto_functions, symbol_table_baset &symbol_table, const class_hierarchyt &class_hierarchy, message_handlert &message_handler)
	Replace every instanceof in every function with an explicit class-identifier test. More...
void	remove_instanceof (goto_modelt &goto_model, const class_hierarchyt &class_hierarchy, message_handlert &message_handler)
	Replace every instanceof in every function with an explicit class-identifier test. More...

Detailed Description

Remove Instance-of Operators

Definition in file remove_instanceof.cpp.

Function Documentation

contains_instanceof()

static bool contains_instanceof ( const exprt &  e )

static

Definition at line 218 of file remove_instanceof.cpp.

remove_instanceof() [1/4]

void remove_instanceof	(	const irep_idt &	function_identifier,
		goto_functionst::goto_functiont &	function,
		symbol_table_baset &	symbol_table,
		const class_hierarchyt &	class_hierarchy,
		message_handlert &	message_handler
	)

Replace every instanceof in the passed function with an explicit class-identifier test.

Remarks

Extra auxiliary variables may be introduced into symbol_table.

Parameters

function_identifier	name of the goto function function
function	The function to work on.
symbol_table	The symbol table to add symbols to.
class_hierarchy	class hierarchy analysis of symbol_table
message_handler	logging output

Definition at line 326 of file remove_instanceof.cpp.

remove_instanceof() [2/4]

void remove_instanceof	(	const irep_idt &	function_identifier,
		goto_programt::targett	target,
		goto_programt &	goto_program,
		symbol_table_baset &	symbol_table,
		const class_hierarchyt &	class_hierarchy,
		message_handlert &	message_handler
	)

Replace an instanceof in the expression or guard of the passed instruction of the given function body with an explicit class-identifier test.

Remarks

Extra auxiliary variables may be introduced into symbol_table.

Parameters

function_identifier	name of the goto function goto_program
target	The instruction to work on.
goto_program	The function body containing the instruction.
symbol_table	The symbol table to add symbols to.
class_hierarchy	class hierarchy analysis of symbol_table
message_handler	logging output

Definition at line 306 of file remove_instanceof.cpp.

remove_instanceof() [3/4]

void remove_instanceof	(	goto_functionst &	goto_functions,
		symbol_table_baset &	symbol_table,
		const class_hierarchyt &	class_hierarchy,
		message_handlert &	message_handler
	)

Replace every instanceof in every function with an explicit class-identifier test.

Remarks

Extra auxiliary variables may be introduced into symbol_table.

Parameters

goto_functions	The functions to work on.
symbol_table	The symbol table to add symbols to.
class_hierarchy	class hierarchy analysis of symbol_table
message_handler	logging output

Definition at line 344 of file remove_instanceof.cpp.

remove_instanceof() [4/4]

void remove_instanceof	(	goto_modelt &	goto_model,
		const class_hierarchyt &	class_hierarchy,
		message_handlert &	message_handler
	)

Replace every instanceof in every function with an explicit class-identifier test.

Remarks

Extra auxiliary variables may be introduced into symbol_table.

Parameters

goto_model	The functions to work on and the symbol table to add
class_hierarchy	class hierarchy analysis of goto_model's symbol table
message_handler	logging output symbols to.

Definition at line 366 of file remove_instanceof.cpp.

subtype_expr()

static exprt subtype_expr ( const exprt &  classid_field, const irep_idt &  target_type, const class_hierarchyt &  class_hierarchy  )

static

Produce an expression of the form classid_field == "A" || classid_field == "B" || ... where A, B, ...

are the possible subtypes of target_type.

Parameters

classid_field	field to compare, usually a @class_identifier field denoting an object's runtime type
target_type	the type all of whose subtypes (including itself) should be accepted
class_hierarchy	class hierarchy

Returns

disjunction of the possible matched subtypes

Definition at line 67 of file remove_instanceof.cpp.