cprover
|
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... | |
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< codet > | instrument_expr (const exprt &expr) |
Computes the instrumentation for expr in the form of either assertions or runtime exceptions. More... | |
Protected Attributes | |
symbol_table_baset & | symbol_table |
const bool | throw_runtime_exceptions |
message_handlert & | message_handler |
Additional Inherited Members |
Definition at line 25 of file java_bytecode_instrument.cpp.
|
inline |
Definition at line 28 of file java_bytecode_instrument.cpp.
|
protected |
Checks whether expr
requires instrumentation, and if so adds it to block
.
[out] | block | block where instrumentation will be added |
expr | expression 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().
|
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.
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().
|
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.
array_struct | array being accessed |
idx | index into the array |
original_loc | source location in the original code |
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().
|
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.
length | the checked length |
original_loc | source location in the original code |
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().
|
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.
class1 | the subclass |
class2 | the super class |
original_loc | source location in the original code |
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().
|
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.
expr | the checked expression original_loc: source location in the original code \return Based on the value of the flag throw_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().
|
protected |
Augments expr
with instrumentation in the form of either assertions or runtime exceptions.
<tt>expr</tt> | the expression to be instrumented |
Definition at line 361 of file java_bytecode_instrument.cpp.
References add_expr_instrumentation(), code_function_callt::arguments(), code_assertt::assertion(), code_switcht::body(), check_class_cast(), check_null_dereference(), code_labelt::code(), code_ifthenelset::cond(), exprt::copy_to_operands(), code_ifthenelset::else_case(), dstringt::empty(), code_expressiont::expression(), Forall_operands, code_function_callt::function(), source_locationt::get_line(), codet::get_statement(), irept::id(), INVARIANT, irept::is_not_nil(), code_assignt::lhs(), code_function_callt::lhs(), merge_source_location_rec(), exprt::op0(), exprt::op1(), exprt::operands(), prepend_instrumentation(), code_assignt::rhs(), exprt::source_location(), code_ifthenelset::then_case(), to_code(), to_code_assert(), to_code_assign(), to_code_expression(), to_code_function_call(), to_code_ifthenelse(), to_code_label(), to_code_switch(), to_code_type(), exprt::type(), and code_switcht::value().
Referenced by operator()().
Computes the instrumentation for expr
in the form of either assertions or runtime exceptions.
expr | the expression for which we compute instrumentation |
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().
void java_bytecode_instrumentt::operator() | ( | codet & | code | ) |
Instruments expr
expr | the expression to be instrumented |
Definition at line 562 of file java_bytecode_instrument.cpp.
References instrument_code().
|
protected |
Appends code
to instrumentation
and overwrites reference code
with the augmented block if instrumentation
is non-empty.
[in,out] | code | code being instrumented |
instrumentation | instrumentation 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().
|
protected |
Creates a class stub for exc_name and generates a conditional GOTO such that exc_name is thrown when cond is met.
cond | condition to be met in order to throw an exception |
original_loc | source location in the original program |
exc_name | the name of the exception to be thrown |
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().
|
protected |
Definition at line 44 of file java_bytecode_instrument.cpp.
|
protected |
Definition at line 42 of file java_bytecode_instrument.cpp.
Referenced by throw_exception().
|
protected |
Definition at line 43 of file java_bytecode_instrument.cpp.
Referenced by check_arithmetic_exception(), check_array_access(), check_array_length(), check_class_cast(), and check_null_dereference().