cprover
replace_java_nondet.cpp File Reference

Replace Java Nondet expressions. More...

#include "replace_java_nondet.h"
#include <goto-programs/goto_convert.h>
#include <goto-programs/goto_model.h>
#include <goto-programs/remove_skip.h>
#include <algorithm>
#include <regex>
Include dependency graph for replace_java_nondet.cpp:

Go to the source code of this file.

Classes

class  nondet_instruction_infot
 Holds information about any discovered nondet methods, with extreme type- safety. More...
 

Functions

static nondet_instruction_infot is_nondet_returning_object (const code_function_callt &function_call)
 Checks whether the function call is one of our nondet library functions. More...
 
static nondet_instruction_infot get_nondet_instruction_info (const goto_programt::const_targett &instr)
 Check whether the instruction is a function call which matches one of the recognised nondet library methods, and return some information about it. More...
 
static bool is_symbol_with_id (const exprt &expr, const irep_idt &identifier)
 Return whether the expression is a symbol with the specified identifier. More...
 
static bool is_typecast_with_id (const exprt &expr, const irep_idt &identifier)
 Return whether the expression is a typecast with the specified identifier. More...
 
static bool is_assignment_from (const goto_programt::instructiont &instr, const irep_idt &identifier)
 Return whether the instruction is an assignment, and the rhs is a symbol or typecast expression with the specified identifier. More...
 
static goto_programt::targett check_and_replace_target (goto_programt &goto_program, const goto_programt::targett &target)
 Given an iterator into a list of instructions, modify the list to replace 'nondet' library functions with CBMC-native nondet expressions, and return an iterator to the next instruction to check. More...
 
static void replace_java_nondet (goto_programt &goto_program)
 Checks each instruction in the goto program to see whether it is a method returning nondet. More...
 
void replace_java_nondet (goto_model_functiont &function)
 Replace calls to nondet library functions with an internal nondet representation in a single function. More...
 
void replace_java_nondet (goto_functionst &goto_functions)
 
void replace_java_nondet (goto_modelt &goto_model)
 Replace calls to nondet library functions with an internal nondet representation. More...
 

Detailed Description

Replace Java Nondet expressions.

Definition in file replace_java_nondet.cpp.

Function Documentation

◆ check_and_replace_target()

static goto_programt::targett check_and_replace_target ( goto_programt goto_program,
const goto_programt::targett target 
)
static

Given an iterator into a list of instructions, modify the list to replace 'nondet' library functions with CBMC-native nondet expressions, and return an iterator to the next instruction to check.

It's important to note that this method also deals with the fact that in the GOTO program it assigns function return values to temporary variables, performs validation and then assigns the value into the actual variable.

Example:

return_tmp0=org.cprover.CProver.nondetWithoutNull:()Ljava/lang/Object;(); ... Various validations of type and value here. obj = (<type-of-obj>)return_tmp0;

We're going to replace all of these lines with return_tmp0 = NONDET(<type-of-obj>)

Parameters
goto_programThe goto program to modify.
targetA single step of the goto program which may be erased and replaced.
Returns
The next instruction to process, probably with this function.

Definition at line 174 of file replace_java_nondet.cpp.

References DATA_INVARIANT, nondet_instruction_infot::FALSE, symbol_exprt::get_identifier(), get_nondet_instruction_info(), goto_program, goto_programt::insert_before(), goto_programt::instructions, INVARIANT, is_assignment_from(), irept::is_not_nil(), code_assignt::lhs(), code_function_callt::lhs(), goto_programt::instructiont::make_skip(), side_effect_expr_nondett::set_nullable(), to_code_assign(), to_code_function_call(), to_symbol_expr(), nondet_instruction_infot::TRUE, and goto_programt::update().

Referenced by replace_java_nondet().

◆ get_nondet_instruction_info()

static nondet_instruction_infot get_nondet_instruction_info ( const goto_programt::const_targett instr)
static

Check whether the instruction is a function call which matches one of the recognised nondet library methods, and return some information about it.

Parameters
instrA goto-program instruction to check.
Returns
A structure detailing the properties of the nondet method.

Definition at line 89 of file replace_java_nondet.cpp.

References is_nondet_returning_object(), to_code(), and to_code_function_call().

Referenced by check_and_replace_target().

◆ is_assignment_from()

static bool is_assignment_from ( const goto_programt::instructiont instr,
const irep_idt identifier 
)
static

Return whether the instruction is an assignment, and the rhs is a symbol or typecast expression with the specified identifier.

Parameters
instrA goto program instruction.
identifierSome identifier.
Returns
True if the expression is a typecast with one operand, and the typecast's identifier matches the specified identifier.

Definition at line 141 of file replace_java_nondet.cpp.

References goto_programt::instructiont::code, goto_programt::instructiont::is_assign(), is_symbol_with_id(), is_typecast_with_id(), code_assignt::rhs(), and to_code_assign().

Referenced by check_and_replace_target().

◆ is_nondet_returning_object()

static nondet_instruction_infot is_nondet_returning_object ( const code_function_callt function_call)
static

Checks whether the function call is one of our nondet library functions.

Parameters
function_callThe function call declaration to check.
Returns
A structure detailing whether the function call appears to be one of our nondet library methods, and if so, whether or not it allows null results.

Definition at line 67 of file replace_java_nondet.cpp.

References code_function_callt::function(), id2string(), and to_symbol_expr().

Referenced by get_nondet_instruction_info().

◆ is_symbol_with_id()

static bool is_symbol_with_id ( const exprt expr,
const irep_idt identifier 
)
static

Return whether the expression is a symbol with the specified identifier.

Parameters
exprThe expression which may be a symbol.
identifierSome identifier.
Returns
True if the expression is a symbol with the specified identifier.

Definition at line 108 of file replace_java_nondet.cpp.

References symbol_exprt::get_identifier(), irept::id(), and to_symbol_expr().

Referenced by is_assignment_from().

◆ is_typecast_with_id()

static bool is_typecast_with_id ( const exprt expr,
const irep_idt identifier 
)
static

Return whether the expression is a typecast with the specified identifier.

Parameters
exprThe expression which may be a typecast.
identifierSome identifier.
Returns
True if the expression is a typecast with one operand, and the typecast's identifier matches the specified identifier.

Definition at line 119 of file replace_java_nondet.cpp.

References symbol_exprt::get_identifier(), irept::id(), exprt::operands(), to_symbol_expr(), and to_typecast_expr().

Referenced by is_assignment_from().

◆ replace_java_nondet() [1/4]

static void replace_java_nondet ( goto_programt goto_program)
static

Checks each instruction in the goto program to see whether it is a method returning nondet.

If it is, replaces the function call with an irep representing a nondet side effect with an appropriate type.

Parameters
goto_programThe goto program to modify.

Definition at line 275 of file replace_java_nondet.cpp.

References check_and_replace_target(), goto_program, and goto_programt::instructions.

Referenced by jbmc_parse_optionst::process_goto_function(), and replace_java_nondet().

◆ replace_java_nondet() [2/4]

void replace_java_nondet ( goto_model_functiont function)

Replace calls to nondet library functions with an internal nondet representation in a single function.

Parameters
functionThe goto program to modify.

Definition at line 286 of file replace_java_nondet.cpp.

References remove_skip(), and replace_java_nondet().

◆ replace_java_nondet() [3/4]

void replace_java_nondet ( goto_functionst goto_functions)

◆ replace_java_nondet() [4/4]

void replace_java_nondet ( goto_modelt )

Replace calls to nondet library functions with an internal nondet representation.

Parameters
goto_modelThe goto program to modify.

Definition at line 304 of file replace_java_nondet.cpp.

References goto_modelt::goto_functions, and replace_java_nondet().