30 const bool _throw_runtime_exceptions,
52 const exprt &array_struct,
57 const exprt &denominator,
80 "java.lang.ArithmeticException",
81 "java.lang.ArrayIndexOutOfBoundsException",
82 "java.lang.ClassCastException",
83 "java.lang.NegativeArraySizeException",
84 "java.lang.NullPointerException"};
128 throw_expr.copy_to_operands(new_symbol.
symbol_expr());
147 const exprt &denominator,
157 "java.lang.ArithmeticException");
160 assertion_loc.
set_comment(
"Denominator should be nonzero");
178 const exprt &array_struct,
186 const and_exprt cond(ge_zero, lt_length);
192 "java.lang.ArrayIndexOutOfBoundsException");
197 low_check_loc.
set_comment(
"Array index should be >= 0");
201 high_check_loc.
set_comment(
"Array index should be < length");
207 return std::move(bounds_checks);
226 class1, ID_java_instanceof, class2);
229 exprt null_check_op=class1;
230 if(null_check_op.
type()!=voidptr)
240 "java.lang.ClassCastException");
278 original_loc,
"java.lang.NullPointerException");
307 "java.lang.NegativeArraySizeException");
310 check_loc.
set_comment(
"Array size should be >= 0");
326 if(expr_instrumentation->get_statement() == ID_block)
329 block.
add(std::move(*expr_instrumentation));
346 instrumentation.
add(code);
347 code=instrumentation;
360 if(statement==ID_assign)
369 else if(statement==ID_expression)
378 else if(statement==ID_assert)
383 if(code_assert.
assertion().
id()==ID_java_instanceof)
389 "Instanceof should have 2 operands");
398 else if(statement==ID_block)
403 else if(statement==ID_label)
408 else if(statement==ID_ifthenelse)
418 else if(statement==ID_switch)
426 else if(statement==ID_return)
435 else if(statement==ID_function_call)
445 for(
const auto &arg : code_function_call.
arguments())
449 if(function_type.has_this())
476 result.add(std::move(*op_result));
480 if(expr.
id()==ID_plus &&
481 expr.
get_bool(ID_java_array_access))
486 if(plus_expr.
op0().
id()==ID_member)
489 if(member_expr.
op0().
id()==ID_dereference)
498 result.add(std::move(bounds_check));
502 else if(expr.
id()==ID_side_effect)
506 if(statement==ID_throw)
512 else if(statement==ID_java_new_array)
519 else if((expr.
id()==ID_div || expr.
id()==ID_mod) &&
520 expr.
type().
id()==ID_signedbv)
525 else if(expr.
id()==ID_dereference &&
526 expr.
get_bool(ID_java_member_access))
530 codet null_dereference_check=
532 dereference_expr.
op0(),
534 result.add(std::move(null_dereference_check));
564 const bool throw_runtime_exceptions,
569 throw_runtime_exceptions,
573 "java_bytecode_instrument expects a code-typed symbol but was called with" 574 " " +
id2string(symbol.
name) +
" which has a value with an id of " +
595 assert_location.
set_comment(
"no uncaught exception");
598 init_code.
add(std::move(assert_no_exception));
613 const bool throw_runtime_exceptions,
618 throw_runtime_exceptions,
621 std::vector<irep_idt> symbols_to_instrument;
622 for(
const auto &symbol_pair : symbol_table.
symbols)
624 if(symbol_pair.second.value.id() == ID_code)
626 symbols_to_instrument.push_back(symbol_pair.first);
632 for(
const auto &symbol : symbols_to_instrument)
void operator()(codet &code)
Instruments code.
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...
const irep_idt & get_statement() const
The type of an expression, extends irept.
irep_idt name
The unique identifier.
const codet & then_case() const
optionalt< codet > instrument_expr(const exprt &expr)
Computes the instrumentation for expr in the form of either assertions or runtime exceptions...
codet representing a switch statement.
A base class for relations, i.e., binary predicates.
const std::string & id2string(const irep_idt &d)
pointer_typet pointer_type(const typet &subtype)
void set_property_class(const irep_idt &property_class)
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
const exprt & cond() const
message_handlert & message_handler
void set_comment(const irep_idt &comment)
Goto Programs with Functions.
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
std::vector< componentt > componentst
Fresh auxiliary symbol creation.
The null pointer constant.
exprt value
Initial value of symbol.
A struct tag type, i.e., struct_typet with an identifier.
typet & type()
Return the type of the expression.
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...
void generate_class_stub(const irep_idt &class_name, symbol_table_baset &symbol_table, message_handlert &message_handler, const struct_union_typet::componentst &componentst)
A constant literal expression.
bool get_bool(const irep_namet &name) const
codet representation of an expression statement.
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...
java_bytecode_instrumentt(symbol_table_baset &_symbol_table, const bool _throw_runtime_exceptions, message_handlert &_message_handler)
code_expressiont & to_code_expression(codet &code)
A side_effect_exprt representation of a side effect that throws an exception.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
side_effect_exprt & to_side_effect_expr(exprt &expr)
Extract member of struct or union.
const code_assignt & to_code_assign(const codet &code)
const irep_idt & id() const
void add(const codet &code)
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
void add_expr_instrumentation(code_blockt &block, const exprt &expr)
Checks whether expr requires instrumentation, and if so adds it to block.
const bool throw_runtime_exceptions
const irep_idt & get_line() const
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...
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
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.
JAVA Bytecode Language Conversion.
codet check_array_length(const exprt &length, const source_locationt &original_loc)
Checks whether length >= 0 and throws NegativeArraySizeException/ generates an assertion when necessa...
Operator to dereference a pointer.
void prepend_instrumentation(codet &code, code_blockt &instrumentation)
Appends code to instrumentation and overwrites reference code with the augmented block if instrumenta...
nonstd::optional< T > optionalt
API to expression classes.
codet representation of a label for branch targets.
void append(const code_blockt &extra_block)
Add all the codets from extra_block to the current code_blockt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Base class for tree-like data structures with sharing.
codet representation of a function call statement.
#define forall_operands(it, expr)
The plus expression Associativity is not specified.
Class that provides messages with a built-in verbosity 'level'.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
void instrument_code(codet &code)
Augments code with instrumentation in the form of either assertions or runtime exceptions.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
const codet & body() const
const code_switcht & to_code_switch(const codet &code)
code_ifthenelset 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 w...
symbol_table_baset & symbol_table
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.
A non-fatal assertion, which checks a condition then permits execution to continue.
const exprt & value() const
typet type
Type of symbol.
message_handlert & get_message_handler()
const java_method_typet & to_java_method_type(const typet &type)
mstreamt & result() const
void merge_source_location_rec(exprt &expr, const source_locationt &source_location)
Attaches a source location to an expression and all of its subexpressions.
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with the requested name pattern.
Base class for all expressions.
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.
The symbol table base class interface.
const std::vector< std::string > exception_needed_classes
const source_locationt & source_location() const
const exprt & expression() 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 ...
#define Forall_operands(it, expr)
source_locationt & add_source_location()
A codet representing sequential composition of program statements.
const codet & to_code(const exprt &expr)
codet representation of an if-then-else statement.
const code_blockt & to_code_block(const codet &code)
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Data structure for representing an arbitrary statement in a program.
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
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...
const code_labelt & to_code_label(const codet &code)
An expression containing a side effect.
const code_assertt & to_code_assert(const codet &code)
const codet & else_case() const
const code_ifthenelset & to_code_ifthenelse(const codet &code)
void make_typecast(const typet &_type)
Create a typecast_exprt to the given type.
A codet representing an assignment in the program.
const irep_idt & get_statement() const
const code_function_callt & to_code_function_call(const codet &code)
const exprt & assertion() const