Go to the documentation of this file.
30 const bool _throw_runtime_exceptions,
51 const exprt &array_struct,
56 const exprt &denominator,
64 const exprt &tested_expr,
79 "java.lang.ArithmeticException",
80 "java.lang.ArrayIndexOutOfBoundsException",
81 "java.lang.ClassCastException",
82 "java.lang.NegativeArraySizeException",
83 "java.lang.NullPointerException"};
115 exc_ptr_type,
"new_exception", original_loc,
"new_exception",
symbol_table);
139 const exprt &denominator,
149 "java.lang.ArithmeticException");
152 assertion_loc.
set_comment(
"Denominator should be nonzero");
170 const exprt &array_struct,
178 const and_exprt cond(ge_zero, lt_length);
184 "java.lang.ArrayIndexOutOfBoundsException");
189 low_check_loc.
set_comment(
"Array index should be >= 0");
193 high_check_loc.
set_comment(
"Array index should be < length");
199 return std::move(bounds_checks);
213 const exprt &tested_expr,
229 "java.lang.ClassCastException");
267 original_loc,
"java.lang.NullPointerException");
296 "java.lang.NegativeArraySizeException");
299 check_loc.
set_comment(
"Array size should be >= 0");
315 if(expr_instrumentation->get_statement() == ID_block)
318 block.
add(std::move(*expr_instrumentation));
335 instrumentation.
add(code);
336 code=instrumentation;
349 if(statement==ID_assign)
358 else if(statement==ID_expression)
367 else if(statement==ID_assert)
372 if(code_assert.
assertion().
id()==ID_java_instanceof)
375 const auto & instanceof
383 else if(statement==ID_block)
388 else if(statement==ID_label)
393 else if(statement==ID_ifthenelse)
403 else if(statement==ID_switch)
411 else if(statement==ID_return)
418 else if(statement==ID_function_call)
428 for(
const auto &arg : code_function_call.
arguments())
458 result.
add(std::move(*op_result));
462 if(expr.
id()==ID_plus &&
463 expr.
get_bool(ID_java_array_access))
468 if(plus_expr.
op0().
id()==ID_member)
471 if(member_expr.
compound().
id() == ID_dereference)
480 result.
add(std::move(bounds_check));
484 else if(expr.
id()==ID_side_effect)
488 if(statement==ID_throw)
495 else if(statement==ID_java_new_array)
503 else if((expr.
id()==ID_div || expr.
id()==ID_mod) &&
504 expr.
type().
id()==ID_signedbv)
510 else if(expr.
id()==ID_dereference &&
511 expr.
get_bool(ID_java_member_access))
517 result.
add(std::move(null_dereference_check));
523 return std::move(result);
547 const bool throw_runtime_exceptions,
552 throw_runtime_exceptions,
556 "java_bytecode_instrument expects a code-typed symbol but was called with"
557 " " +
id2string(symbol.
name) +
" which has a value with an id of " +
578 assert_location.
set_comment(
"no uncaught exception");
581 init_code.
add(std::move(assert_no_exception));
596 const bool throw_runtime_exceptions,
601 throw_runtime_exceptions,
604 std::vector<irep_idt> symbols_to_instrument;
605 for(
const auto &symbol_pair : symbol_table.
symbols)
607 if(symbol_pair.second.value.id() == ID_code)
609 symbols_to_instrument.push_back(symbol_pair.first);
615 for(
const auto &symbol : symbols_to_instrument)
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.
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
A codet representing sequential composition of program statements.
static exprt conditional_cast(const exprt &expr, const typet &type)
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
code_expressiont & to_code_expression(codet &code)
void set_comment(const irep_idt &comment)
#define Forall_operands(it, expr)
codet check_array_length(const exprt &length, const source_locationt &original_loc)
Checks whether length >= 0 and throws NegativeArraySizeException/ generates an assertion when necessa...
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
The type of an expression, extends irept.
const codet & then_case() const
void add_expr_instrumentation(code_blockt &block, const exprt &expr)
Checks whether expr requires instrumentation, and if so adds it to block.
typet type
Type of symbol.
Operator to dereference a pointer.
void operator()(codet &code)
Instruments code.
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 ArrayIndexOutofBoundsE...
A non-fatal assertion, which checks a condition then permits execution to continue.
The plus expression Associativity is not specified.
void generate_class_stub(const irep_idt &class_name, symbol_table_baset &symbol_table, message_handlert &message_handler, const struct_union_typet::componentst &componentst)
Base class for all expressions.
std::vector< componentt > componentst
A struct tag type, i.e., struct_typet with an identifier.
Java-specific exprt subclasses.
const exprt & cond() const
symbol_table_baset & symbol_table
side_effect_exprt & to_side_effect_expr(exprt &expr)
code_ifthenelset check_class_cast(const exprt &tested_expr, const struct_tag_typet &target_type, const source_locationt &original_loc)
Checks whether class1 is an instance of class2 and throws ClassCastException/generates an assertion w...
message_handlert & message_handler
code_blockt create_fatal_assertion(const exprt &condition, const source_locationt &loc)
Create a fatal assertion, which checks a condition and then halts if it does not hold.
codet representation of an if-then-else statement.
const irep_idt & get_line() const
const codet & to_code(const exprt &expr)
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
void prepend_instrumentation(codet &code, code_blockt &instrumentation)
Appends code to instrumentation and overwrites reference code with the augmented block if instrumenta...
typet & type()
Return the type of the expression.
optionalt< codet > instrument_expr(const exprt &expr)
Computes the instrumentation for expr in the form of either assertions or runtime exceptions.
const code_assertt & to_code_assert(const codet &code)
codet representation of a function call statement.
bool get_bool(const irep_namet &name) const
const exprt & assertion() const
code_ifthenelset 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 ...
The null pointer constant.
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
const std::string & id2string(const irep_idt &d)
const exprt & compound() const
const bool throw_runtime_exceptions
#define forall_operands(it, expr)
const code_ifthenelset & to_code_ifthenelse(const codet &code)
codet representation of a label for branch targets.
The symbol table base class interface.
const code_labelt & to_code_label(const codet &code)
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
pointer_typet pointer_type(const typet &subtype)
const irep_idt & id() const
const code_function_callt & to_code_function_call(const codet &code)
const code_returnt & to_code_return(const codet &code)
void add(const codet &code)
signedbv_typet java_int_type()
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
symbolt & fresh_java_symbol(const typet &type, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &function_name, symbol_table_baset &symbol_table)
nonstd::optional< T > optionalt
void java_bytecode_instrument_uncaught_exceptions(code_blockt &init_code, const symbolt &exc_symbol, const source_locationt &source_location)
Instruments the start function with an assertion that checks whether an exception has escaped the ent...
const irep_idt & get_statement() const
void java_bytecode_instrument(symbol_tablet &symbol_table, const bool throw_runtime_exceptions, message_handlert &message_handler)
Instruments all the code in the symbol_table with runtime exceptions or corresponding assertions.
Extract member of struct or union.
void merge_source_location_rec(exprt &expr, const source_locationt &source_location)
Attaches a source location to an expression and all of its subexpressions.
const exprt & value() const
void instrument_code(codet &code)
Augments code with instrumentation in the form of either assertions or runtime exceptions.
exprt value
Initial value of symbol.
codet representation of a "return from a function" statement.
const code_assignt & to_code_assign(const codet &code)
void check_code(const codet &code, const validation_modet vm)
Check that the given code statement is well-formed (shallow checks only, i.e., enclosed statements,...
const java_instanceof_exprt & to_java_instanceof_expr(const exprt &expr)
Cast an exprt to a java_instanceof_exprt.
const std::vector< std::string > exception_needed_classes
codet representing a switch statement.
void append(const code_blockt &extra_block)
Add all the codets from extra_block to the current code_blockt.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
A base class for relations, i.e., binary predicates whose two operands have the same type.
const codet & else_case() const
const code_switcht & to_code_switch(const codet &code)
Goto Programs with Functions.
java_bytecode_instrumentt(symbol_table_baset &_symbol_table, const bool _throw_runtime_exceptions, message_handlert &_message_handler)
A side_effect_exprt representation of a side effect that throws an exception.
const code_blockt & to_code_block(const codet &code)
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
void java_bytecode_instrument_symbol(symbol_table_baset &symbol_table, symbolt &symbol, const bool throw_runtime_exceptions, message_handlert &message_handler)
Instruments the code attached to symbol with runtime exceptions or corresponding assertions.
There are a large number of kinds of tree structured or tree-like data in CPROVER.
const exprt & expression() const
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
source_locationt & add_source_location()
const java_method_typet & to_java_method_type(const typet &type)
const codet & body() const
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
const exprt & return_value() const
empty_typet java_void_type()
A codet representing an assignment in the program.
const irep_idt & get_statement() const
A constant literal expression.
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
API to expression classes.
const source_locationt & source_location() const
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; E...
irep_idt name
The unique identifier.
An expression containing a side effect.
JAVA Bytecode Language Conversion.
codet representation of an expression statement.
void set_property_class(const irep_idt &property_class)
Data structure for representing an arbitrary statement in a program.