cprover
Loading...
Searching...
No Matches
java_bytecode_instrument.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Instrument codet with assertions/runtime exceptions
4
5Author: Cristina David
6
7Date: June 2017
8
9\*******************************************************************/
10
12
14
15#include <util/arith_tools.h>
16#include <util/c_types.h>
17#include <util/std_code.h>
18#include <util/symbol_table.h>
19
20#include "java_expr.h"
21#include "java_types.h"
22#include "java_utils.h"
23
25{
26public:
28 symbol_table_baset &_symbol_table,
29 const bool _throw_runtime_exceptions,
30 message_handlert &_message_handler)
31 : symbol_table(_symbol_table),
32 throw_runtime_exceptions(_throw_runtime_exceptions),
33 message_handler(_message_handler)
34 {
35 }
36
37 void operator()(codet &code);
38
39protected:
43
45 const exprt &cond,
46 const source_locationt &original_loc,
47 const irep_idt &exc_name);
48
50 const exprt &array_struct,
51 const exprt &idx,
52 const source_locationt &original_loc);
53
55 const exprt &denominator,
56 const source_locationt &original_loc);
57
59 const exprt &expr,
60 const source_locationt &original_loc);
61
63 const exprt &tested_expr,
64 const struct_tag_typet &target_type,
65 const source_locationt &original_loc);
66
68 const exprt &length,
69 const source_locationt &original_loc);
70
71 void instrument_code(codet &code);
72 void add_expr_instrumentation(code_blockt &block, const exprt &expr);
73 void prepend_instrumentation(codet &code, code_blockt &instrumentation);
75};
76
77const std::vector<std::string> exception_needed_classes = {
78 "java.lang.ArithmeticException",
79 "java.lang.ArrayIndexOutOfBoundsException",
80 "java.lang.ClassCastException",
81 "java.lang.NegativeArraySizeException",
82 "java.lang.NullPointerException"};
83
94 const exprt &cond,
95 const source_locationt &original_loc,
96 const irep_idt &exc_name)
97{
98 irep_idt exc_class_name("java::"+id2string(exc_name));
99
100 if(!symbol_table.has_symbol(exc_class_name))
101 {
103 exc_name,
107 }
108
109 pointer_typet exc_ptr_type = pointer_type(struct_tag_typet(exc_class_name));
110
111 // Allocate and throw an instance of the exception class:
112
113 symbolt &new_symbol = fresh_java_symbol(
114 exc_ptr_type, "new_exception", original_loc, "new_exception", symbol_table);
115
116 side_effect_exprt new_instance(ID_java_new, exc_ptr_type, original_loc);
117 code_assignt assign_new(new_symbol.symbol_expr(), new_instance);
118
119 side_effect_expr_throwt throw_expr(irept(), typet(), original_loc);
120 throw_expr.copy_to_operands(new_symbol.symbol_expr());
121
122 code_ifthenelset if_code(
123 cond, code_blockt({assign_new, code_expressiont(throw_expr)}));
124
125 if_code.add_source_location()=original_loc;
126
127 return if_code;
128}
129
138 const exprt &denominator,
139 const source_locationt &original_loc)
140{
141 const constant_exprt &zero=from_integer(0, denominator.type());
142 const binary_relation_exprt equal_zero(denominator, ID_equal, zero);
143
145 return throw_exception(
146 equal_zero,
147 original_loc,
148 "java.lang.ArithmeticException");
149
150 source_locationt assertion_loc = original_loc;
151 assertion_loc.set_comment("Denominator should be nonzero");
152 assertion_loc.set_property_class("integer-divide-by-zero");
153
155 binary_relation_exprt(denominator, ID_notequal, zero), assertion_loc);
156}
157
169 const exprt &array_struct,
170 const exprt &idx,
171 const source_locationt &original_loc)
172{
173 const constant_exprt &zero=from_integer(0, java_int_type());
174 const binary_relation_exprt ge_zero(idx, ID_ge, zero);
175 const member_exprt length_field(array_struct, "length", java_int_type());
176 const binary_relation_exprt lt_length(idx, ID_lt, length_field);
177 const and_exprt cond(ge_zero, lt_length);
178
180 return throw_exception(
181 not_exprt(cond),
182 original_loc,
183 "java.lang.ArrayIndexOutOfBoundsException");
184
185 code_blockt bounds_checks;
186
187 source_locationt low_check_loc = original_loc;
188 low_check_loc.set_comment("Array index should be >= 0");
189 low_check_loc.set_property_class("array-index-out-of-bounds-low");
190
191 source_locationt high_check_loc = original_loc;
192 high_check_loc.set_comment("Array index should be < length");
193 high_check_loc.set_property_class("array-index-out-of-bounds-high");
194
195 bounds_checks.add(create_fatal_assertion(ge_zero, low_check_loc));
196 bounds_checks.add(create_fatal_assertion(lt_length, high_check_loc));
197
198 return std::move(bounds_checks);
199}
200
212 const exprt &tested_expr,
213 const struct_tag_typet &target_type,
214 const source_locationt &original_loc)
215{
216 java_instanceof_exprt class_cast_check(tested_expr, target_type);
217
219 exprt null_check_op = typecast_exprt::conditional_cast(tested_expr, voidptr);
220
223 {
226 not_exprt(class_cast_check),
227 original_loc,
228 "java.lang.ClassCastException");
229 }
230 else
231 {
232 source_locationt check_loc = original_loc;
233 check_loc.set_comment("Dynamic cast check");
234 check_loc.set_property_class("bad-dynamic-cast");
235
236 codet assert_class = create_fatal_assertion(class_cast_check, check_loc);
237
238 check_code=std::move(assert_class);
239 }
240
241 return code_ifthenelset(
242 notequal_exprt(std::move(null_check_op), null_pointer_exprt(voidptr)),
243 std::move(*check_code));
244}
245
256 const exprt &expr,
257 const source_locationt &original_loc)
258{
259 const equal_exprt equal_expr(
260 expr,
262
264 return throw_exception(
265 equal_expr,
266 original_loc, "java.lang.NullPointerException");
267
268 source_locationt check_loc = original_loc;
269 check_loc.set_comment("Null pointer check");
270 check_loc.set_property_class("null-pointer-exception");
271
272 return create_fatal_assertion(not_exprt(equal_expr), check_loc);
273}
274
285 const exprt &length,
286 const source_locationt &original_loc)
287{
288 const constant_exprt &zero=from_integer(0, java_int_type());
289 const binary_relation_exprt ge_zero(length, ID_ge, zero);
290
292 return throw_exception(
293 not_exprt(ge_zero),
294 original_loc,
295 "java.lang.NegativeArraySizeException");
296
297 source_locationt check_loc;
298 check_loc.set_comment("Array size should be >= 0");
299 check_loc.set_property_class("array-create-negative-size");
300
301 return create_fatal_assertion(ge_zero, check_loc);
302}
303
309 code_blockt &block,
310 const exprt &expr)
311{
312 if(optionalt<codet> expr_instrumentation = instrument_expr(expr))
313 {
314 if(expr_instrumentation->get_statement() == ID_block)
315 block.append(to_code_block(*expr_instrumentation));
316 else
317 block.add(std::move(*expr_instrumentation));
318 }
319}
320
326 codet &code,
327 code_blockt &instrumentation)
328{
329 if(instrumentation!=code_blockt())
330 {
331 if(code.get_statement()==ID_block)
332 instrumentation.append(to_code_block(code));
333 else
334 instrumentation.add(code);
335 code=instrumentation;
336 }
337}
338
343{
344 source_locationt old_source_location=code.source_location();
345
346 const irep_idt &statement=code.get_statement();
347
348 if(statement==ID_assign)
349 {
350 code_assignt code_assign=to_code_assign(code);
351
352 code_blockt block;
353 add_expr_instrumentation(block, code_assign.lhs());
354 add_expr_instrumentation(block, code_assign.rhs());
355 prepend_instrumentation(code, block);
356 }
357 else if(statement==ID_expression)
358 {
359 code_expressiont code_expression=
360 to_code_expression(code);
361
362 code_blockt block;
363 add_expr_instrumentation(block, code_expression.expression());
364 prepend_instrumentation(code, block);
365 }
366 else if(statement==ID_assert)
367 {
368 const code_assertt &code_assert=to_code_assert(code);
369
370 // does this correspond to checkcast?
371 if(code_assert.assertion().id()==ID_java_instanceof)
372 {
373 code_blockt block;
374 const auto & instanceof
375 = to_java_instanceof_expr(code_assert.assertion());
376
377 code = check_class_cast(instanceof.tested_expr(),
378 instanceof
379 .target_type(), code_assert.source_location());
380 }
381 }
382 else if(statement==ID_block)
383 {
384 Forall_operands(it, code)
386 }
387 else if(statement==ID_label)
388 {
389 code_labelt &code_label=to_code_label(code);
390 instrument_code(code_label.code());
391 }
392 else if(statement==ID_ifthenelse)
393 {
394 code_blockt block;
395 code_ifthenelset &code_ifthenelse=to_code_ifthenelse(code);
396 add_expr_instrumentation(block, code_ifthenelse.cond());
397 instrument_code(code_ifthenelse.then_case());
398 if(code_ifthenelse.else_case().is_not_nil())
399 instrument_code(code_ifthenelse.else_case());
400 prepend_instrumentation(code, block);
401 }
402 else if(statement==ID_switch)
403 {
404 code_blockt block;
405 code_switcht &code_switch=to_code_switch(code);
406 add_expr_instrumentation(block, code_switch.value());
407 add_expr_instrumentation(block, code_switch.body());
408 prepend_instrumentation(code, block);
409 }
410 else if(statement==ID_return)
411 {
412 code_blockt block;
413 code_returnt &code_return = to_code_return(code);
414 add_expr_instrumentation(block, code_return.return_value());
415 prepend_instrumentation(code, block);
416 }
417 else if(statement==ID_function_call)
418 {
419 code_blockt block;
420 code_function_callt &code_function_call=to_code_function_call(code);
421 add_expr_instrumentation(block, code_function_call.lhs());
422 add_expr_instrumentation(block, code_function_call.function());
423
424 const java_method_typet &function_type =
425 to_java_method_type(code_function_call.function().type());
426
427 for(const auto &arg : code_function_call.arguments())
428 add_expr_instrumentation(block, arg);
429
430 // Check for a null this-argument of a virtual call:
431 if(function_type.has_this())
432 {
434 code_function_call.arguments()[0],
435 code_function_call.source_location()));
436 }
437
438 prepend_instrumentation(code, block);
439 }
440
441 // Ensure source location is retained:
442 if(!old_source_location.get_line().empty())
443 merge_source_location_rec(code, old_source_location);
444}
445
451{
452 code_blockt result;
453 // First check our operands:
454 forall_operands(it, expr)
455 {
456 if(optionalt<codet> op_result = instrument_expr(*it))
457 result.add(std::move(*op_result));
458 }
459
460 // Add any check due at this node:
461 if(expr.id()==ID_plus &&
462 expr.get_bool(ID_java_array_access))
463 {
464 // this corresponds to ?aload and ?astore so
465 // we check that 0<=index<array.length
466 const plus_exprt &plus_expr=to_plus_expr(expr);
467 if(plus_expr.op0().id()==ID_member)
468 {
469 const member_exprt &member_expr=to_member_expr(plus_expr.op0());
470 if(member_expr.compound().id() == ID_dereference)
471 {
472 const dereference_exprt &dereference_expr =
473 to_dereference_expr(member_expr.compound());
474 codet bounds_check=
476 dereference_expr,
477 plus_expr.op1(),
478 expr.source_location());
479 result.add(std::move(bounds_check));
480 }
481 }
482 }
483 else if(expr.id()==ID_side_effect)
484 {
485 const side_effect_exprt &side_effect_expr=to_side_effect_expr(expr);
486 const irep_idt &statement=side_effect_expr.get_statement();
487 if(statement==ID_throw)
488 {
489 // this corresponds to a throw and so we check that
490 // we don't throw null
492 to_unary_expr(expr).op(), expr.source_location()));
493 }
494 else if(statement==ID_java_new_array)
495 {
496 // this corresponds to new array so we check that
497 // length is >=0
498 result.add(check_array_length(
499 to_multi_ary_expr(expr).op0(), expr.source_location()));
500 }
501 }
502 else if((expr.id()==ID_div || expr.id()==ID_mod) &&
503 expr.type().id()==ID_signedbv)
504 {
505 // check division by zero (for integer types only)
507 to_binary_expr(expr).op1(), expr.source_location()));
508 }
509 else if(expr.id()==ID_dereference &&
510 expr.get_bool(ID_java_member_access))
511 {
512 // Check pointer non-null before access:
513 const dereference_exprt &dereference_expr = to_dereference_expr(expr);
514 codet null_dereference_check = check_null_dereference(
515 dereference_expr.pointer(), dereference_expr.source_location());
516 result.add(std::move(null_dereference_check));
517 }
518
519 if(result==code_blockt())
520 return {};
521 else
522 return std::move(result);
523}
524
528{
529 instrument_code(code);
530}
531
544 symbol_table_baset &symbol_table,
545 symbolt &symbol,
546 const bool throw_runtime_exceptions,
547 message_handlert &message_handler)
548{
549 java_bytecode_instrumentt instrument(
550 symbol_table,
551 throw_runtime_exceptions,
552 message_handler);
553 INVARIANT(
554 symbol.value.id()==ID_code,
555 "java_bytecode_instrument expects a code-typed symbol but was called with"
556 " " + id2string(symbol.name) + " which has a value with an id of " +
557 id2string(symbol.value.id()));
558 instrument(to_code(symbol.value));
559}
560
567 code_blockt &init_code,
568 const symbolt &exc_symbol,
569 const source_locationt &source_location)
570{
571 // check that there is no uncaught exception
572 code_assertt assert_no_exception(equal_exprt(
573 exc_symbol.symbol_expr(),
575
576 source_locationt assert_location = source_location;
577 assert_location.set_comment("no uncaught exception");
578 assert_no_exception.add_source_location() = assert_location;
579
580 init_code.add(std::move(assert_no_exception));
581}
582
594 symbol_tablet &symbol_table,
595 const bool throw_runtime_exceptions,
596 message_handlert &message_handler)
597{
598 java_bytecode_instrumentt instrument(
599 symbol_table,
600 throw_runtime_exceptions,
601 message_handler);
602
603 std::vector<irep_idt> symbols_to_instrument;
604 for(const auto &symbol_pair : symbol_table.symbols)
605 {
606 if(symbol_pair.second.value.id() == ID_code)
607 {
608 symbols_to_instrument.push_back(symbol_pair.first);
609 }
610 }
611
612 // instrument(...) can add symbols to the table, so it's
613 // not safe to hold a reference to a symbol across a call.
614 for(const auto &symbol : symbols_to_instrument)
615 {
616 instrument(to_code(symbol_table.get_writeable_ref(symbol).value));
617 }
618}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
pointer_typet pointer_type(const typet &subtype)
Definition c_types.cpp:253
Boolean AND.
Definition std_expr.h:1974
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:674
A non-fatal assertion, which checks a condition then permits execution to continue.
Definition std_code.h:270
const exprt & assertion() const
Definition std_code.h:276
A codet representing an assignment in the program.
A codet representing sequential composition of program statements.
Definition std_code.h:130
void append(const code_blockt &extra_block)
Add all the codets from extra_block to the current code_blockt.
Definition std_code.cpp:89
void add(const codet &code)
Definition std_code.h:168
codet representation of an expression statement.
Definition std_code.h:1394
const exprt & expression() const
Definition std_code.h:1401
codet representation of a function call statement.
codet representation of an if-then-else statement.
Definition std_code.h:460
const exprt & cond() const
Definition std_code.h:478
const codet & else_case() const
Definition std_code.h:498
const codet & then_case() const
Definition std_code.h:488
codet representation of a label for branch targets.
Definition std_code.h:959
codet & code()
Definition std_code.h:977
codet representation of a "return from a function" statement.
const exprt & return_value() const
codet representing a switch statement.
Definition std_code.h:548
const codet & body() const
Definition std_code.h:565
const exprt & value() const
Definition std_code.h:555
bool has_this() const
Definition std_types.h:616
Data structure for representing an arbitrary statement in a program.
const irep_idt & get_statement() const
A constant literal expression.
Definition std_expr.h:2807
Operator to dereference a pointer.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
bool empty() const
Definition dstring.h:88
Equality.
Definition std_expr.h:1225
Base class for all expressions.
Definition expr.h:54
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition expr.h:129
typet & type()
Return the type of the expression.
Definition expr.h:82
const source_locationt & source_location() const
Definition expr.h:230
source_locationt & add_source_location()
Definition expr.h:235
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition irep.h:372
bool get_bool(const irep_idt &name) const
Definition irep.cpp:58
bool is_not_nil() const
Definition irep.h:380
const irep_idt & id() const
Definition irep.h:396
java_bytecode_instrumentt(symbol_table_baset &_symbol_table, const bool _throw_runtime_exceptions, message_handlert &_message_handler)
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...
void operator()(codet &code)
Instruments code.
void prepend_instrumentation(codet &code, code_blockt &instrumentation)
Appends code to instrumentation and overwrites reference code with the augmented block if instrumenta...
void add_expr_instrumentation(code_blockt &block, const exprt &expr)
Checks whether expr requires instrumentation, and if so adds it to block.
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.
codet check_array_length(const exprt &length, const source_locationt &original_loc)
Checks whether length >= 0 and throws NegativeArraySizeException/ generates an assertion when necessa...
void instrument_code(codet &code)
Augments code with instrumentation in the form of either assertions or runtime exceptions.
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 ...
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...
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...
optionalt< codet > instrument_expr(const exprt &expr)
Computes the instrumentation for expr in the form of either assertions or runtime exceptions.
Extract member of struct or union.
Definition std_expr.h:2667
const exprt & compound() const
Definition std_expr.h:2708
exprt & op1()
Definition std_expr.h:850
exprt & op0()
Definition std_expr.h:844
Boolean negation.
Definition std_expr.h:2181
Disequality.
Definition std_expr.h:1283
The null pointer constant.
The plus expression Associativity is not specified.
Definition std_expr.h:914
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
A side_effect_exprt representation of a side effect that throws an exception.
Definition std_code.h:1757
An expression containing a side effect.
Definition std_code.h:1450
const irep_idt & get_statement() const
Definition std_code.h:1472
void set_comment(const irep_idt &comment)
void set_property_class(const irep_idt &property_class)
const irep_idt & get_line() const
A struct tag type, i.e., struct_typet with an identifier.
Definition std_types.h:449
std::vector< componentt > componentst
Definition std_types.h:140
The symbol table base class interface.
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
The symbol table.
Symbol table entry.
Definition symbol.h:28
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition symbol.cpp:121
typet type
Type of symbol.
Definition symbol.h:31
irep_idt name
The unique identifier.
Definition symbol.h:40
exprt value
Initial value of symbol.
Definition symbol.h:34
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:1928
The type of an expression, extends irept.
Definition type.h:29
#define forall_operands(it, expr)
Definition expr.h:18
#define Forall_operands(it, expr)
Definition expr.h:25
const code_function_callt & to_code_function_call(const codet &code)
const code_assignt & to_code_assign(const codet &code)
const code_returnt & to_code_return(const codet &code)
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
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.
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 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 std::vector< std::string > exception_needed_classes
Java-specific exprt subclasses.
const java_instanceof_exprt & to_java_instanceof_expr(const exprt &expr)
Cast an exprt to a java_instanceof_exprt.
Definition java_expr.h:86
signedbv_typet java_int_type()
empty_typet java_void_type()
const java_method_typet & to_java_method_type(const typet &type)
Definition java_types.h:184
void generate_class_stub(const irep_idt &class_name, symbol_table_baset &symbol_table, message_handlert &message_handler, const struct_union_typet::componentst &componentst)
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)
void merge_source_location_rec(exprt &expr, const source_locationt &source_location)
Attaches a source location to an expression and all of its subexpressions.
nonstd::optional< T > optionalt
Definition optional.h:35
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
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.
Definition std_code.cpp:123
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition std_code.h:1506
const code_assertt & to_code_assert(const codet &code)
Definition std_code.h:304
const code_labelt & to_code_label(const codet &code)
Definition std_code.h:1004
const code_blockt & to_code_block(const codet &code)
Definition std_code.h:203
const code_ifthenelset & to_code_ifthenelse(const codet &code)
Definition std_code.h:530
const code_switcht & to_code_switch(const codet &code)
Definition std_code.h:592
code_expressiont & to_code_expression(codet &code)
Definition std_code.h:1428
const codet & to_code(const exprt &expr)
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition std_expr.h:627
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
Definition std_expr.h:953
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition std_expr.h:328
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition std_expr.h:899
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:2751
Author: Diffblue Ltd.
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,...