cprover
java_bytecode_instrumentt Class Reference
Inheritance diagram for java_bytecode_instrumentt:
[legend]
Collaboration diagram for java_bytecode_instrumentt:
[legend]

Public Member Functions

 java_bytecode_instrumentt (symbol_table_baset &_symbol_table, const bool _throw_runtime_exceptions, message_handlert &_message_handler)
 
void operator() (codet &code)
 Instruments expr More...
 
- Public Member Functions inherited from messaget
virtual void set_message_handler (message_handlert &_message_handler)
 
message_handlertget_message_handler ()
 
 messaget ()
 
 messaget (const messaget &other)
 
messagetoperator= (const messaget &other)
 
 messaget (message_handlert &_message_handler)
 
virtual ~messaget ()
 
mstreamtget_mstream (unsigned message_level) const
 
mstreamterror () const
 
mstreamtwarning () const
 
mstreamtresult () const
 
mstreamtstatus () const
 
mstreamtstatistics () const
 
mstreamtprogress () const
 
mstreamtdebug () const
 
void conditional_output (mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const
 Generate output to mstream using output_generator if the configured verbosity is at least as high as that of mstream. More...
 

Protected Member Functions

codet throw_exception (const exprt &cond, const source_locationt &original_loc, const irep_idt &exc_name)
 Creates a class stub for exc_name and generates a conditional GOTO such that exc_name is thrown when cond is met. More...
 
codet check_array_access (const exprt &array_struct, const exprt &idx, const source_locationt &original_loc)
 Checks whether the array access array_struct[idx] is out-of-bounds, and throws ArrayIndexOutofBoundsException/generates an assertion if necessary; Exceptions are thrown when the throw_runtime_exceptions flag is set. More...
 
codet check_arithmetic_exception (const exprt &denominator, const source_locationt &original_loc)
 Checks whether there is a division by zero and throws ArithmeticException if necessary. More...
 
codet check_null_dereference (const exprt &expr, const source_locationt &original_loc)
 Checks whether expr is null and throws NullPointerException/ generates an assertion when necessary; Exceptions are thrown when the throw_runtime_exceptions flag is set. More...
 
codet check_class_cast (const exprt &class1, const exprt &class2, const source_locationt &original_loc)
 Checks whether class1 is an instance of class2 and throws ClassCastException/generates an assertion when necessary; Exceptions are thrown when the throw_runtime_exceptions flag is set. More...
 
codet check_array_length (const exprt &length, const source_locationt &original_loc)
 Checks whether length>=0 and throws NegativeArraySizeException/ generates an assertion when necessary; Exceptions are thrown when the throw_runtime_exceptions flag is set. More...
 
void instrument_code (codet &code)
 Augments expr with instrumentation in the form of either assertions or runtime exceptions. More...
 
void add_expr_instrumentation (code_blockt &block, const exprt &expr)
 Checks whether expr requires instrumentation, and if so adds it to block. More...
 
void prepend_instrumentation (codet &code, code_blockt &instrumentation)
 Appends code to instrumentation and overwrites reference code with the augmented block if instrumentation is non-empty. More...
 
optionalt< codetinstrument_expr (const exprt &expr)
 Computes the instrumentation for expr in the form of either assertions or runtime exceptions. More...
 

Protected Attributes

symbol_table_basetsymbol_table
 
const bool throw_runtime_exceptions
 
message_handlertmessage_handler
 
- Protected Attributes inherited from messaget
message_handlertmessage_handler
 
mstreamt mstream
 

Additional Inherited Members

- Public Types inherited from messaget
enum  message_levelt {
  M_ERROR =1, M_WARNING =2, M_RESULT =4, M_STATUS =6,
  M_STATISTICS =8, M_PROGRESS =9, M_DEBUG =10
}
 
- Static Public Member Functions inherited from messaget
static unsigned eval_verbosity (const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest)
 Parse a (user-)provided string as a verbosity level and set it as the verbosity of dest. More...
 
static mstreamteom (mstreamt &m)
 
static mstreamtendl (mstreamt &m)
 

Detailed Description

Definition at line 25 of file java_bytecode_instrument.cpp.

Constructor & Destructor Documentation

◆ java_bytecode_instrumentt()

java_bytecode_instrumentt::java_bytecode_instrumentt ( symbol_table_baset _symbol_table,
const bool  _throw_runtime_exceptions,
message_handlert _message_handler 
)
inline

Definition at line 28 of file java_bytecode_instrument.cpp.

Member Function Documentation

◆ add_expr_instrumentation()

void java_bytecode_instrumentt::add_expr_instrumentation ( code_blockt block,
const exprt expr 
)
protected

Checks whether expr requires instrumentation, and if so adds it to block.

Parameters
[out]blockblock where instrumentation will be added
exprexpression to instrument

Definition at line 327 of file java_bytecode_instrument.cpp.

References code_blockt::append(), instrument_expr(), exprt::move_to_operands(), and to_code_block().

Referenced by instrument_code().

◆ check_arithmetic_exception()

codet java_bytecode_instrumentt::check_arithmetic_exception ( const exprt denominator,
const source_locationt original_loc 
)
protected

Checks whether there is a division by zero and throws ArithmeticException if necessary.

Exceptions are thrown when the throw_runtime_exceptions flag is set.

Returns
Based on the value of the flag throw_runtime_exceptions, it returns code that either throws an ArithmeticException or asserts a nonzero denominator.

Definition at line 151 of file java_bytecode_instrument.cpp.

References create_fatal_assertion(), from_integer(), source_locationt::set_comment(), source_locationt::set_property_class(), throw_exception(), throw_runtime_exceptions, and exprt::type().

Referenced by instrument_expr().

◆ check_array_access()

codet java_bytecode_instrumentt::check_array_access ( const exprt array_struct,
const exprt idx,
const source_locationt original_loc 
)
protected

Checks whether the array access array_struct[idx] is out-of-bounds, and throws ArrayIndexOutofBoundsException/generates an assertion if necessary; Exceptions are thrown when the throw_runtime_exceptions flag is set.

Otherwise, assertions are emitted.

Parameters
array_structarray being accessed
idxindex into the array
original_locsource location in the original code
Returns
Based on the value of the flag throw_runtime_exceptions, it returns code that either throws an ArrayIndexOutPfBoundsException or emits an assertion checking the array access

Definition at line 182 of file java_bytecode_instrument.cpp.

References code_blockt::add(), create_fatal_assertion(), from_integer(), java_int_type(), source_locationt::set_comment(), source_locationt::set_property_class(), throw_exception(), and throw_runtime_exceptions.

Referenced by instrument_expr().

◆ check_array_length()

codet java_bytecode_instrumentt::check_array_length ( const exprt length,
const source_locationt original_loc 
)
protected

Checks whether length>=0 and throws NegativeArraySizeException/ generates an assertion when necessary; Exceptions are thrown when the throw_runtime_exceptions flag is set.

Otherwise, assertions are emitted.

Parameters
lengththe checked length
original_locsource location in the original code
Returns
Based on the value of the flag throw_runtime_exceptions, it returns code that either throws an NegativeArraySizeException or emits an assertion checking the subtype relation

Definition at line 303 of file java_bytecode_instrument.cpp.

References create_fatal_assertion(), from_integer(), java_int_type(), source_locationt::set_comment(), source_locationt::set_property_class(), throw_exception(), and throw_runtime_exceptions.

Referenced by instrument_expr().

◆ check_class_cast()

codet java_bytecode_instrumentt::check_class_cast ( const exprt class1,
const exprt class2,
const source_locationt original_loc 
)
protected

Checks whether class1 is an instance of class2 and throws ClassCastException/generates an assertion when necessary; Exceptions are thrown when the throw_runtime_exceptions flag is set.

Otherwise, assertions are emitted.

Parameters
class1the subclass
class2the super class
original_locsource location in the original code
Returns
Based on the value of the flag throw_runtime_exceptions, it returns code that either throws an ClassCastException or emits an assertion checking the subtype relation

Definition at line 225 of file java_bytecode_instrument.cpp.

References code_ifthenelset::cond(), create_fatal_assertion(), exprt::make_typecast(), pointer_type(), source_locationt::set_comment(), source_locationt::set_property_class(), code_ifthenelset::then_case(), throw_exception(), throw_runtime_exceptions, and exprt::type().

Referenced by instrument_code().

◆ check_null_dereference()

codet java_bytecode_instrumentt::check_null_dereference ( const exprt expr,
const source_locationt original_loc 
)
protected

Checks whether expr is null and throws NullPointerException/ generates an assertion when necessary; Exceptions are thrown when the throw_runtime_exceptions flag is set.

Otherwise, assertions are emitted.

Parameters
exprthe checked expression original_loc: source location in the original code \return Based on the value of the flagthrow_runtime_exceptions`, it returns code that either throws an NullPointerException or emits an assertion checking the subtype relation

Definition at line 274 of file java_bytecode_instrument.cpp.

References create_fatal_assertion(), source_locationt::set_comment(), source_locationt::set_property_class(), throw_exception(), throw_runtime_exceptions, to_pointer_type(), and exprt::type().

Referenced by instrument_code(), and instrument_expr().

◆ instrument_code()

◆ instrument_expr()

optionalt< codet > java_bytecode_instrumentt::instrument_expr ( const exprt expr)
protected

Computes the instrumentation for expr in the form of either assertions or runtime exceptions.

Parameters
exprthe expression for which we compute instrumentation
Returns
: The instrumentation for expr if required

Definition at line 477 of file java_bytecode_instrument.cpp.

References check_arithmetic_exception(), check_array_access(), check_array_length(), check_null_dereference(), forall_operands, irept::get_bool(), side_effect_exprt::get_statement(), irept::id(), exprt::op0(), exprt::op1(), messaget::result(), exprt::source_location(), to_dereference_expr(), to_member_expr(), to_plus_expr(), to_side_effect_expr(), and exprt::type().

Referenced by add_expr_instrumentation().

◆ operator()()

void java_bytecode_instrumentt::operator() ( codet code)

Instruments expr

Parameters
exprthe expression to be instrumented

Definition at line 562 of file java_bytecode_instrument.cpp.

References instrument_code().

◆ prepend_instrumentation()

void java_bytecode_instrumentt::prepend_instrumentation ( codet code,
code_blockt instrumentation 
)
protected

Appends code to instrumentation and overwrites reference code with the augmented block if instrumentation is non-empty.

Parameters
[in,out]codecode being instrumented
instrumentationinstrumentation code block to prepend

Definition at line 344 of file java_bytecode_instrument.cpp.

References code_blockt::append(), exprt::copy_to_operands(), codet::get_statement(), and to_code_block().

Referenced by instrument_code().

◆ throw_exception()

codet java_bytecode_instrumentt::throw_exception ( const exprt cond,
const source_locationt original_loc,
const irep_idt exc_name 
)
protected

Creates a class stub for exc_name and generates a conditional GOTO such that exc_name is thrown when cond is met.

Parameters
condcondition to be met in order to throw an exception
original_locsource location in the original program
exc_namethe name of the exception to be thrown
Returns
Returns the code initialising the throwing the exception

Definition at line 95 of file java_bytecode_instrument.cpp.

References exprt::add_source_location(), code_ifthenelset::cond(), exprt::copy_to_operands(), generate_class_stub(), get_fresh_aux_symbol(), messaget::get_message_handler(), symbol_table_baset::has_symbol(), id2string(), exprt::move_to_operands(), pointer_type(), symbolt::symbol_expr(), symbol_table, and code_ifthenelset::then_case().

Referenced by check_arithmetic_exception(), check_array_access(), check_array_length(), check_class_cast(), and check_null_dereference().

Member Data Documentation

◆ message_handler

message_handlert& java_bytecode_instrumentt::message_handler
protected

Definition at line 44 of file java_bytecode_instrument.cpp.

◆ symbol_table

symbol_table_baset& java_bytecode_instrumentt::symbol_table
protected

Definition at line 42 of file java_bytecode_instrument.cpp.

Referenced by throw_exception().

◆ throw_runtime_exceptions

const bool java_bytecode_instrumentt::throw_runtime_exceptions
protected

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