Convert side_effect_expr_nondett expressions. More...

#include "convert_java_nondet.h"
#include <goto-programs/goto_convert.h>
#include <goto-programs/goto_model.h>
#include <goto-programs/remove_skip.h>
#include "java_object_factory.h"
#include "java_object_factory_parameters.h"
#include "java_utils.h"

Include dependency graph for convert_java_nondet.cpp:

Go to the source code of this file.

Functions
static bool	is_nondet_pointer (exprt expr)
	Returns true if `expr` is a nondet pointer that isn't a function pointer or a void* pointer as these can be meaningfully non-det initialized. More...

static goto_programt	get_gen_nondet_init_instructions (const symbol_exprt &aux_symbol_expr, const source_locationt &source_loc, symbol_table_baset &symbol_table, message_handlert &message_handler, const java_object_factory_parameterst &object_factory_parameters, const irep_idt &mode)
	Populate `instructions` with goto instructions to nondet init `aux_symbol_expr` More...

static std::pair< goto_programt::targett, bool >	insert_nondet_init_code (const irep_idt &function_identifier, goto_programt &goto_program, const goto_programt::targett &target, symbol_table_baset &symbol_table, message_handlert &message_handler, java_object_factory_parameterst object_factory_parameters, const irep_idt &mode)
	Checks an instruction to see whether it contains an assignment from side_effect_expr_nondet. More...

void	convert_nondet (const irep_idt &function_identifier, goto_programt &goto_program, symbol_table_baset &symbol_table, message_handlert &message_handler, const java_object_factory_parameterst &user_object_factory_parameters, const irep_idt &mode)
	For each instruction in the goto program, checks if it is an assignment from nondet and replaces it with the appropriate composite initialization code if so. More...

void	convert_nondet (goto_model_functiont &function, message_handlert &message_handler, const java_object_factory_parameterst &object_factory_parameters, const irep_idt &mode)
	Converts side_effect_exprt_nondett expressions using java_object_factory. More...

void	convert_nondet (goto_functionst &goto_functions, symbol_table_baset &symbol_table, message_handlert &message_handler, const java_object_factory_parameterst &object_factory_parameters)
	Converts side_effect_exprt_nondett expressions using java_object_factory. More...

void	convert_nondet (goto_modelt &goto_model, message_handlert &message_handler, const java_object_factory_parameterst &object_factory_parameters)

Detailed Description

Convert side_effect_expr_nondett expressions.

Definition in file convert_java_nondet.cpp.

Function Documentation

◆ convert_nondet() [1/4]

void convert_nondet	(	const irep_idt &	function_identifier,
		goto_programt &	goto_program,
		symbol_table_baset &	symbol_table,
		message_handlert &	message_handler,
		const java_object_factory_parameterst &	user_object_factory_parameters,
		const irep_idt &	mode
	)

For each instruction in the goto program, checks if it is an assignment from nondet and replaces it with the appropriate composite initialization code if so.

Parameters

function_identifier	Name of the function `goto_program`.
goto_program	The goto program to modify.
symbol_table	The global symbol table.
message_handler	Handles logging.
user_object_factory_parameters	Parameters for the generation of nondet objects.
mode	Language mode

Definition at line 165 of file convert_java_nondet.cpp.

◆ convert_nondet() [2/4]

void convert_nondet	(	goto_functionst &	goto_functions,
		symbol_table_baset &	symbol_table,
		message_handlert &	message_handler,
		const java_object_factory_parameterst &	object_factory_parameters
	)

Converts side_effect_exprt_nondett expressions using java_object_factory.

For example, NONDET(SomeClass *) may become a nondet choice between a null pointer and a fresh instance of SomeClass, whose fields are in turn nondet initialized in the same way. See java_object_factory.h for details.

Note the code introduced has been freshly goto_convert'd without any passes such as remove_java_new being run. Therefore the caller may need to (re-)run this and other expected GOTO transformations after this pass completes.

Parameters

goto_functions	The set of goto programs to modify.
symbol_table	The symbol table to query/update.
message_handler	For error logging.
object_factory_parameters	Parameters for the generation of nondet objects.

Definition at line 217 of file convert_java_nondet.cpp.

◆ convert_nondet() [3/4]

void convert_nondet	(	goto_model_functiont &	function,
		message_handlert &	message_handler,
		const java_object_factory_parameterst &	object_factory_parameters,
		const irep_idt &	mode
	)

Converts side_effect_exprt_nondett expressions using java_object_factory.

For example, NONDET(SomeClass *) may become a nondet choice between a null pointer and a fresh instance of SomeClass, whose fields are in turn nondet initialized in the same way. See java_object_factory.h for details.

Note the code introduced has been freshly goto_convert'd without any passes such as remove_java_new being run. Therefore the caller may need to (re-)run this and other expected GOTO transformations after this pass completes.

Parameters

function	goto program to modify
message_handler	For error logging.
object_factory_parameters	Parameters for the generation of nondet objects.
mode	Mode for newly created symbols

Definition at line 200 of file convert_java_nondet.cpp.

◆ convert_nondet() [4/4]

void convert_nondet	(	goto_modelt &	goto_model,
		message_handlert &	message_handler,
		const java_object_factory_parameterst &	object_factory_parameters
	)

Definition at line 246 of file convert_java_nondet.cpp.

◆ get_gen_nondet_init_instructions()

static goto_programt get_gen_nondet_init_instructions	(	const symbol_exprt &	aux_symbol_expr,
		const source_locationt &	source_loc,
		symbol_table_baset &	symbol_table,
		message_handlert &	message_handler,
		const java_object_factory_parameterst &	object_factory_parameters,
		const irep_idt &	mode
	)

static

Populate instructions with goto instructions to nondet init aux_symbol_expr

Definition at line 40 of file convert_java_nondet.cpp.

◆ insert_nondet_init_code()

static std::pair<goto_programt::targett, bool> insert_nondet_init_code	(	const irep_idt &	function_identifier,
		goto_programt &	goto_program,
		const goto_programt::targett &	target,
		symbol_table_baset &	symbol_table,
		message_handlert &	message_handler,
		java_object_factory_parameterst	object_factory_parameters,
		const irep_idt &	mode
	)

static

Checks an instruction to see whether it contains an assignment from side_effect_expr_nondet.

If so, replaces the instruction with a range of instructions to properly nondet-initialize the lhs.

Parameters

function_identifier	Name of the function containing `target`.
goto_program	The goto program to modify.
target	One of the steps in that goto program.
symbol_table	The global symbol table.
message_handler	Handles logging.
object_factory_parameters	Parameters for the generation of nondet objects.
mode	Language mode

Returns: The next instruction to process with this function and a boolean indicating whether any changes were made to the goto program.

Definition at line 80 of file convert_java_nondet.cpp.

◆ is_nondet_pointer()

static bool is_nondet_pointer ( exprt expr )

static

Returns true if expr is a nondet pointer that isn't a function pointer or a void* pointer as these can be meaningfully non-det initialized.

Definition at line 24 of file convert_java_nondet.cpp.

Functions

Detailed Description

Function Documentation

◆ convert_nondet() [1/4]

◆ convert_nondet() [2/4]

◆ convert_nondet() [3/4]

◆ convert_nondet() [4/4]

◆ get_gen_nondet_init_instructions()

◆ insert_nondet_init_code()

◆ is_nondet_pointer()