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