cprover
goto_check_java.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Checks for Errors in Java Programs
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "goto_check_java.h"
13 
14 #include <algorithm>
15 
16 #include <util/arith_tools.h>
17 #include <util/array_name.h>
18 #include <util/bitvector_expr.h>
19 #include <util/c_types.h>
20 #include <util/config.h>
21 #include <util/cprover_prefix.h>
22 #include <util/expr_util.h>
23 #include <util/find_symbols.h>
24 #include <util/floatbv_expr.h>
25 #include <util/ieee_float.h>
26 #include <util/invariant.h>
27 #include <util/make_unique.h>
28 #include <util/message.h>
29 #include <util/options.h>
30 #include <util/pointer_expr.h>
33 #include <util/prefix.h>
34 #include <util/simplify_expr.h>
35 #include <util/std_code.h>
36 #include <util/std_expr.h>
37 
38 #include <langapi/language.h>
39 #include <langapi/mode.h>
40 
43 
45 
47 {
48 public:
50  const namespacet &_ns,
51  const optionst &_options,
52  message_handlert &_message_handler)
53  : ns(_ns), local_bitvector_analysis(nullptr), log(_message_handler)
54  {
55  enable_bounds_check = _options.get_bool_option("bounds-check");
56  enable_pointer_check = _options.get_bool_option("pointer-check");
57  enable_div_by_zero_check = _options.get_bool_option("div-by-zero-check");
59  _options.get_bool_option("signed-overflow-check");
61  _options.get_bool_option("unsigned-overflow-check");
62  enable_conversion_check = _options.get_bool_option("conversion-check");
64  _options.get_bool_option("float-overflow-check");
65  enable_simplify = _options.get_bool_option("simplify");
66  enable_nan_check = _options.get_bool_option("nan-check");
67  retain_trivial = _options.get_bool_option("retain-trivial-checks");
68  enable_assert_to_assume = _options.get_bool_option("assert-to-assume");
69  enable_assertions = _options.get_bool_option("assertions");
71  _options.get_bool_option("built-in-assertions");
72  enable_assumptions = _options.get_bool_option("assumptions");
73  error_labels = _options.get_list_option("error-label");
74  }
75 
77 
78  void goto_check(
79  const irep_idt &function_identifier,
80  goto_functiont &goto_function);
81 
82 protected:
83  const namespacet &ns;
84  std::unique_ptr<local_bitvector_analysist> local_bitvector_analysis;
87 
92  void check_rec_address(const exprt &expr);
93 
103  bool check_rec_member(const member_exprt &member);
104 
108  void check_rec_div(const div_exprt &div_expr);
109 
113  void check_rec_arithmetic_op(const exprt &expr);
114 
119  void check_rec(const exprt &expr);
120 
123  void check(const exprt &expr);
124 
125  struct conditiont
126  {
127  conditiont(const exprt &_assertion, const std::string &_description)
128  : assertion(_assertion), description(_description)
129  {
130  }
131 
133  std::string description;
134  };
135 
136  using conditionst = std::list<conditiont>;
137 
138  void bounds_check(const exprt &);
139  void bounds_check_index(const index_exprt &);
140  void div_by_zero_check(const div_exprt &);
141  void mod_overflow_check(const mod_exprt &);
142 
147  void
148  pointer_validity_check(const dereference_exprt &expr, const exprt &src_expr);
149 
151  get_pointer_is_null_condition(const exprt &address, const exprt &size);
152 
154  const exprt &address,
155  const exprt &size);
156  void integer_overflow_check(const exprt &);
157  void conversion_check(const exprt &);
158  void float_overflow_check(const exprt &);
159  void nan_check(const exprt &);
161 
162  std::string array_name(const exprt &);
163 
170  void add_property(
171  const exprt &asserted_expr,
172  const std::string &comment,
173  const std::string &property_class,
174  const source_locationt &source_location,
175  const exprt &src_expr);
176 
178  typedef std::set<std::pair<exprt, exprt>> assertionst;
180 
185  void invalidate(const exprt &lhs);
186 
202 
205 };
206 
208 {
209  if(lhs.id() == ID_index)
210  invalidate(to_index_expr(lhs).array());
211  else if(lhs.id() == ID_member)
212  invalidate(to_member_expr(lhs).struct_op());
213  else if(lhs.id() == ID_symbol)
214  {
215  // clear all assertions about 'symbol'
216  find_symbols_sett find_symbols_set{to_symbol_expr(lhs).get_identifier()};
217 
218  for(auto it = assertions.begin(); it != assertions.end();)
219  {
220  if(
221  has_symbol(it->second, find_symbols_set) ||
222  has_subexpr(it->second, ID_dereference))
223  {
224  it = assertions.erase(it);
225  }
226  else
227  ++it;
228  }
229  }
230  else
231  {
232  // give up, clear all
233  assertions.clear();
234  }
235 }
236 
238 {
240  return;
241 
242  // add divison by zero subgoal
243 
244  exprt zero = from_integer(0, expr.op1().type());
245  const notequal_exprt inequality(expr.op1(), std::move(zero));
246 
247  add_property(
248  inequality,
249  "division by zero",
250  "division-by-zero",
251  expr.find_source_location(),
252  expr);
253 }
254 
257 {
259  return;
260 
261  const auto &type = expr.type();
262 
263  if(type.id() == ID_signedbv)
264  {
265  // INT_MIN % -1 is, in principle, defined to be zero in
266  // ANSI C, C99, C++98, and C++11. Most compilers, however,
267  // fail to produce 0, and in some cases generate an exception.
268  // C11 explicitly makes this case undefined.
269 
270  notequal_exprt int_min_neq(
271  expr.op0(), to_signedbv_type(type).smallest_expr());
272 
273  notequal_exprt minus_one_neq(
274  expr.op1(), from_integer(-1, expr.op1().type()));
275 
276  add_property(
277  or_exprt(int_min_neq, minus_one_neq),
278  "result of signed mod is not representable",
279  "overflow",
280  expr.find_source_location(),
281  expr);
282  }
283 }
284 
286 {
288  return;
289 
290  // First, check type.
291  const typet &type = expr.type();
292 
293  if(type.id() != ID_signedbv && type.id() != ID_unsignedbv)
294  return;
295 
296  if(expr.id() == ID_typecast)
297  {
298  const auto &op = to_typecast_expr(expr).op();
299 
300  // conversion to signed int may overflow
301  const typet &old_type = op.type();
302 
303  if(type.id() == ID_signedbv)
304  {
305  std::size_t new_width = to_signedbv_type(type).get_width();
306 
307  if(old_type.id() == ID_signedbv) // signed -> signed
308  {
309  std::size_t old_width = to_signedbv_type(old_type).get_width();
310  if(new_width >= old_width)
311  return; // always ok
312 
313  const binary_relation_exprt no_overflow_upper(
314  op, ID_le, from_integer(power(2, new_width - 1) - 1, old_type));
315 
316  const binary_relation_exprt no_overflow_lower(
317  op, ID_ge, from_integer(-power(2, new_width - 1), old_type));
318 
319  add_property(
320  and_exprt(no_overflow_lower, no_overflow_upper),
321  "arithmetic overflow on signed type conversion",
322  "overflow",
323  expr.find_source_location(),
324  expr);
325  }
326  else if(old_type.id() == ID_unsignedbv) // unsigned -> signed
327  {
328  std::size_t old_width = to_unsignedbv_type(old_type).get_width();
329  if(new_width >= old_width + 1)
330  return; // always ok
331 
332  const binary_relation_exprt no_overflow_upper(
333  op, ID_le, from_integer(power(2, new_width - 1) - 1, old_type));
334 
335  add_property(
336  no_overflow_upper,
337  "arithmetic overflow on unsigned to signed type conversion",
338  "overflow",
339  expr.find_source_location(),
340  expr);
341  }
342  else if(old_type.id() == ID_floatbv) // float -> signed
343  {
344  // Note that the fractional part is truncated!
345  ieee_floatt upper(to_floatbv_type(old_type));
346  upper.from_integer(power(2, new_width - 1));
347  const binary_relation_exprt no_overflow_upper(
348  op, ID_lt, upper.to_expr());
349 
350  ieee_floatt lower(to_floatbv_type(old_type));
351  lower.from_integer(-power(2, new_width - 1) - 1);
352  const binary_relation_exprt no_overflow_lower(
353  op, ID_gt, lower.to_expr());
354 
355  add_property(
356  and_exprt(no_overflow_lower, no_overflow_upper),
357  "arithmetic overflow on float to signed integer type conversion",
358  "overflow",
359  expr.find_source_location(),
360  expr);
361  }
362  }
363  else if(type.id() == ID_unsignedbv)
364  {
365  std::size_t new_width = to_unsignedbv_type(type).get_width();
366 
367  if(old_type.id() == ID_signedbv) // signed -> unsigned
368  {
369  std::size_t old_width = to_signedbv_type(old_type).get_width();
370 
371  if(new_width >= old_width - 1)
372  {
373  // only need lower bound check
374  const binary_relation_exprt no_overflow_lower(
375  op, ID_ge, from_integer(0, old_type));
376 
377  add_property(
378  no_overflow_lower,
379  "arithmetic overflow on signed to unsigned type conversion",
380  "overflow",
381  expr.find_source_location(),
382  expr);
383  }
384  else
385  {
386  // need both
387  const binary_relation_exprt no_overflow_upper(
388  op, ID_le, from_integer(power(2, new_width) - 1, old_type));
389 
390  const binary_relation_exprt no_overflow_lower(
391  op, ID_ge, from_integer(0, old_type));
392 
393  add_property(
394  and_exprt(no_overflow_lower, no_overflow_upper),
395  "arithmetic overflow on signed to unsigned type conversion",
396  "overflow",
397  expr.find_source_location(),
398  expr);
399  }
400  }
401  else if(old_type.id() == ID_unsignedbv) // unsigned -> unsigned
402  {
403  std::size_t old_width = to_unsignedbv_type(old_type).get_width();
404  if(new_width >= old_width)
405  return; // always ok
406 
407  const binary_relation_exprt no_overflow_upper(
408  op, ID_le, from_integer(power(2, new_width) - 1, old_type));
409 
410  add_property(
411  no_overflow_upper,
412  "arithmetic overflow on unsigned to unsigned type conversion",
413  "overflow",
414  expr.find_source_location(),
415  expr);
416  }
417  else if(old_type.id() == ID_floatbv) // float -> unsigned
418  {
419  // Note that the fractional part is truncated!
420  ieee_floatt upper(to_floatbv_type(old_type));
421  upper.from_integer(power(2, new_width) - 1);
422  const binary_relation_exprt no_overflow_upper(
423  op, ID_lt, upper.to_expr());
424 
425  ieee_floatt lower(to_floatbv_type(old_type));
426  lower.from_integer(-1);
427  const binary_relation_exprt no_overflow_lower(
428  op, ID_gt, lower.to_expr());
429 
430  add_property(
431  and_exprt(no_overflow_lower, no_overflow_upper),
432  "arithmetic overflow on float to unsigned integer type conversion",
433  "overflow",
434  expr.find_source_location(),
435  expr);
436  }
437  }
438  }
439 }
440 
442 {
444  return;
445 
446  // First, check type.
447  const typet &type = expr.type();
448 
449  if(type.id() == ID_signedbv && !enable_signed_overflow_check)
450  return;
451 
452  if(type.id() == ID_unsignedbv && !enable_unsigned_overflow_check)
453  return;
454 
455  // add overflow subgoal
456 
457  if(expr.id() == ID_div)
458  {
459  // undefined for signed division INT_MIN/-1
460  if(type.id() == ID_signedbv)
461  {
462  const auto &div_expr = to_div_expr(expr);
463 
464  equal_exprt int_min_eq(
465  div_expr.dividend(), to_signedbv_type(type).smallest_expr());
466 
467  equal_exprt minus_one_eq(div_expr.divisor(), from_integer(-1, type));
468 
469  add_property(
470  not_exprt(and_exprt(int_min_eq, minus_one_eq)),
471  "arithmetic overflow on signed division",
472  "overflow",
473  expr.find_source_location(),
474  expr);
475  }
476 
477  return;
478  }
479  else if(expr.id() == ID_unary_minus)
480  {
481  if(type.id() == ID_signedbv)
482  {
483  // overflow on unary- on signed integers can only happen with the
484  // smallest representable number 100....0
485 
486  equal_exprt int_min_eq(
487  to_unary_minus_expr(expr).op(), to_signedbv_type(type).smallest_expr());
488 
489  add_property(
490  not_exprt(int_min_eq),
491  "arithmetic overflow on signed unary minus",
492  "overflow",
493  expr.find_source_location(),
494  expr);
495  }
496  else if(type.id() == ID_unsignedbv)
497  {
498  // Overflow on unary- on unsigned integers happens for all operands
499  // that are not zero.
500 
501  notequal_exprt not_eq_zero(
502  to_unary_minus_expr(expr).op(), to_unsignedbv_type(type).zero_expr());
503 
504  add_property(
505  not_eq_zero,
506  "arithmetic overflow on unsigned unary minus",
507  "overflow",
508  expr.find_source_location(),
509  expr);
510  }
511 
512  return;
513  }
514  else if(expr.id() == ID_shl)
515  {
516  if(type.id() == ID_signedbv)
517  {
518  const auto &shl_expr = to_shl_expr(expr);
519  const auto &op = shl_expr.op();
520  const auto &op_type = to_signedbv_type(type);
521  const auto op_width = op_type.get_width();
522  const auto &distance = shl_expr.distance();
523  const auto &distance_type = distance.type();
524 
525  // a left shift of a negative value is undefined;
526  // yet this isn't an overflow
527  exprt neg_value_shift;
528 
529  if(op_type.id() == ID_unsignedbv)
530  neg_value_shift = false_exprt();
531  else
532  neg_value_shift =
533  binary_relation_exprt(op, ID_lt, from_integer(0, op_type));
534 
535  // a shift with negative distance is undefined;
536  // yet this isn't an overflow
537  exprt neg_dist_shift;
538 
539  if(distance_type.id() == ID_unsignedbv)
540  neg_dist_shift = false_exprt();
541  else
542  {
543  neg_dist_shift = binary_relation_exprt(
544  distance, ID_lt, from_integer(0, distance_type));
545  }
546 
547  // shifting a non-zero value by more than its width is undefined;
548  // yet this isn't an overflow
549  const exprt dist_too_large = binary_predicate_exprt(
550  distance, ID_gt, from_integer(op_width, distance_type));
551 
552  const exprt op_zero = equal_exprt(op, from_integer(0, op_type));
553 
554  auto new_type = to_bitvector_type(op_type);
555  new_type.set_width(op_width * 2);
556 
557  const exprt op_ext = typecast_exprt(op, new_type);
558 
559  const exprt op_ext_shifted = shl_exprt(op_ext, distance);
560 
561  // The semantics of signed left shifts are contentious for the case
562  // that a '1' is shifted into the signed bit.
563  // Assuming 32-bit integers, 1<<31 is implementation-defined
564  // in ANSI C and C++98, but is explicitly undefined by C99,
565  // C11 and C++11.
566  bool allow_shift_into_sign_bit = true;
567 
568  const unsigned number_of_top_bits =
569  allow_shift_into_sign_bit ? op_width : op_width + 1;
570 
571  const exprt top_bits = extractbits_exprt(
572  op_ext_shifted,
573  new_type.get_width() - 1,
574  new_type.get_width() - number_of_top_bits,
575  unsignedbv_typet(number_of_top_bits));
576 
577  const exprt top_bits_zero =
578  equal_exprt(top_bits, from_integer(0, top_bits.type()));
579 
580  // a negative distance shift isn't an overflow;
581  // a negative value shift isn't an overflow;
582  // a shift that's too far isn't an overflow;
583  // a shift of zero isn't overflow;
584  // else check the top bits
585  add_property(
586  disjunction({neg_value_shift,
587  neg_dist_shift,
588  dist_too_large,
589  op_zero,
590  top_bits_zero}),
591  "arithmetic overflow on signed shl",
592  "overflow",
593  expr.find_source_location(),
594  expr);
595  }
596 
597  return;
598  }
599 
600  multi_ary_exprt overflow(
601  "overflow-" + expr.id_string(), expr.operands(), bool_typet());
602 
603  if(expr.operands().size() >= 3)
604  {
605  // The overflow checks are binary!
606  // We break these up.
607 
608  for(std::size_t i = 1; i < expr.operands().size(); i++)
609  {
610  exprt tmp;
611 
612  if(i == 1)
613  tmp = to_multi_ary_expr(expr).op0();
614  else
615  {
616  tmp = expr;
617  tmp.operands().resize(i);
618  }
619 
620  std::string kind = type.id() == ID_unsignedbv ? "unsigned" : "signed";
621 
622  add_property(
623  not_exprt{binary_overflow_exprt{tmp, expr.id(), expr.operands()[i]}},
624  "arithmetic overflow on " + kind + " " + expr.id_string(),
625  "overflow",
626  expr.find_source_location(),
627  expr);
628  }
629  }
630  else if(expr.operands().size() == 2)
631  {
632  std::string kind = type.id() == ID_unsignedbv ? "unsigned" : "signed";
633 
634  const binary_exprt &bexpr = to_binary_expr(expr);
635  add_property(
636  not_exprt{binary_overflow_exprt{bexpr.lhs(), expr.id(), bexpr.rhs()}},
637  "arithmetic overflow on " + kind + " " + expr.id_string(),
638  "overflow",
639  expr.find_source_location(),
640  expr);
641  }
642  else
643  {
644  PRECONDITION(expr.id() == ID_unary_minus);
645 
646  std::string kind = type.id() == ID_unsignedbv ? "unsigned" : "signed";
647 
648  add_property(
649  not_exprt{unary_overflow_exprt{expr.id(), to_unary_expr(expr).op()}},
650  "arithmetic overflow on " + kind + " " + expr.id_string(),
651  "overflow",
652  expr.find_source_location(),
653  expr);
654  }
655 }
656 
658 {
660  return;
661 
662  // First, check type.
663  const typet &type = expr.type();
664 
665  if(type.id() != ID_floatbv)
666  return;
667 
668  // add overflow subgoal
669 
670  if(expr.id() == ID_typecast)
671  {
672  // Can overflow if casting from larger
673  // to smaller type.
674  const auto &op = to_typecast_expr(expr).op();
675  if(op.type().id() == ID_floatbv)
676  {
677  // float-to-float
678  or_exprt overflow_check{isinf_exprt(op), not_exprt(isinf_exprt(expr))};
679 
680  add_property(
681  std::move(overflow_check),
682  "arithmetic overflow on floating-point typecast",
683  "overflow",
684  expr.find_source_location(),
685  expr);
686  }
687  else
688  {
689  // non-float-to-float
690  add_property(
691  not_exprt(isinf_exprt(expr)),
692  "arithmetic overflow on floating-point typecast",
693  "overflow",
694  expr.find_source_location(),
695  expr);
696  }
697 
698  return;
699  }
700  else if(expr.id() == ID_div)
701  {
702  // Can overflow if dividing by something small
703  or_exprt overflow_check(
704  isinf_exprt(to_div_expr(expr).dividend()), not_exprt(isinf_exprt(expr)));
705 
706  add_property(
707  std::move(overflow_check),
708  "arithmetic overflow on floating-point division",
709  "overflow",
710  expr.find_source_location(),
711  expr);
712 
713  return;
714  }
715  else if(expr.id() == ID_mod)
716  {
717  // Can't overflow
718  return;
719  }
720  else if(expr.id() == ID_unary_minus)
721  {
722  // Can't overflow
723  return;
724  }
725  else if(expr.id() == ID_plus || expr.id() == ID_mult || expr.id() == ID_minus)
726  {
727  if(expr.operands().size() == 2)
728  {
729  // Can overflow
730  or_exprt overflow_check(
731  isinf_exprt(to_binary_expr(expr).op0()),
732  isinf_exprt(to_binary_expr(expr).op1()),
733  not_exprt(isinf_exprt(expr)));
734 
735  std::string kind = expr.id() == ID_plus
736  ? "addition"
737  : expr.id() == ID_minus
738  ? "subtraction"
739  : expr.id() == ID_mult ? "multiplication" : "";
740 
741  add_property(
742  std::move(overflow_check),
743  "arithmetic overflow on floating-point " + kind,
744  "overflow",
745  expr.find_source_location(),
746  expr);
747 
748  return;
749  }
750  else if(expr.operands().size() >= 3)
751  {
752  DATA_INVARIANT(expr.id() != ID_minus, "minus expression must be binary");
753 
754  // break up
756  return;
757  }
758  }
759 }
760 
762 {
763  if(!enable_nan_check)
764  return;
765 
766  // first, check type
767  if(expr.type().id() != ID_floatbv)
768  return;
769 
770  if(
771  expr.id() != ID_plus && expr.id() != ID_mult && expr.id() != ID_div &&
772  expr.id() != ID_minus)
773  return;
774 
775  // add NaN subgoal
776 
777  exprt isnan;
778 
779  if(expr.id() == ID_div)
780  {
781  const auto &div_expr = to_div_expr(expr);
782 
783  // there a two ways to get a new NaN on division:
784  // 0/0 = NaN and x/inf = NaN
785  // (note that x/0 = +-inf for x!=0 and x!=inf)
786  const and_exprt zero_div_zero(
788  div_expr.op0(), from_integer(0, div_expr.dividend().type())),
790  div_expr.op1(), from_integer(0, div_expr.divisor().type())));
791 
792  const isinf_exprt div_inf(div_expr.op1());
793 
794  isnan = or_exprt(zero_div_zero, div_inf);
795  }
796  else if(expr.id() == ID_mult)
797  {
798  if(expr.operands().size() >= 3)
799  return nan_check(make_binary(expr));
800 
801  const auto &mult_expr = to_mult_expr(expr);
802 
803  // Inf * 0 is NaN
804  const and_exprt inf_times_zero(
805  isinf_exprt(mult_expr.op0()),
807  mult_expr.op1(), from_integer(0, mult_expr.op1().type())));
808 
809  const and_exprt zero_times_inf(
811  mult_expr.op1(), from_integer(0, mult_expr.op1().type())),
812  isinf_exprt(mult_expr.op0()));
813 
814  isnan = or_exprt(inf_times_zero, zero_times_inf);
815  }
816  else if(expr.id() == ID_plus)
817  {
818  if(expr.operands().size() >= 3)
819  return nan_check(make_binary(expr));
820 
821  const auto &plus_expr = to_plus_expr(expr);
822 
823  // -inf + +inf = NaN and +inf + -inf = NaN,
824  // i.e., signs differ
825  ieee_float_spect spec = ieee_float_spect(to_floatbv_type(plus_expr.type()));
826  exprt plus_inf = ieee_floatt::plus_infinity(spec).to_expr();
827  exprt minus_inf = ieee_floatt::minus_infinity(spec).to_expr();
828 
829  isnan = or_exprt(
830  and_exprt(
831  equal_exprt(plus_expr.op0(), minus_inf),
832  equal_exprt(plus_expr.op1(), plus_inf)),
833  and_exprt(
834  equal_exprt(plus_expr.op0(), plus_inf),
835  equal_exprt(plus_expr.op1(), minus_inf)));
836  }
837  else if(expr.id() == ID_minus)
838  {
839  // +inf - +inf = NaN and -inf - -inf = NaN,
840  // i.e., signs match
841 
842  const auto &minus_expr = to_minus_expr(expr);
843 
844  ieee_float_spect spec =
845  ieee_float_spect(to_floatbv_type(minus_expr.type()));
846  exprt plus_inf = ieee_floatt::plus_infinity(spec).to_expr();
847  exprt minus_inf = ieee_floatt::minus_infinity(spec).to_expr();
848 
849  isnan = or_exprt(
850  and_exprt(
851  equal_exprt(minus_expr.lhs(), plus_inf),
852  equal_exprt(minus_expr.rhs(), plus_inf)),
853  and_exprt(
854  equal_exprt(minus_expr.lhs(), minus_inf),
855  equal_exprt(minus_expr.rhs(), minus_inf)));
856  }
857  else
858  UNREACHABLE;
859 
860  add_property(
861  boolean_negate(isnan),
862  "NaN on " + expr.id_string(),
863  "NaN",
864  expr.find_source_location(),
865  expr);
866 }
867 
869  const dereference_exprt &expr,
870  const exprt &src_expr)
871 {
873  return;
874 
875  const exprt &pointer = expr.pointer();
876 
877  exprt size;
878 
879  if(expr.type().id() == ID_empty)
880  {
881  // a dereference *p (with p being a pointer to void) is valid if p points to
882  // valid memory (of any size). the smallest possible size of the memory
883  // segment p could be pointing to is 1, hence we use this size for the
884  // address check
885  size = from_integer(1, size_type());
886  }
887  else
888  {
889  auto size_of_expr_opt = size_of_expr(expr.type(), ns);
890  CHECK_RETURN(size_of_expr_opt.has_value());
891  size = size_of_expr_opt.value();
892  }
893 
894  auto conditions = get_pointer_dereferenceable_conditions(pointer, size);
895 
896  for(const auto &c : conditions)
897  {
898  add_property(
899  c.assertion,
900  "dereference failure: " + c.description,
901  "pointer dereference",
902  src_expr.find_source_location(),
903  src_expr);
904  }
905 }
906 
909  const exprt &address,
910  const exprt &size)
911 {
912  auto maybe_null_condition = get_pointer_is_null_condition(address, size);
913 
914  if(maybe_null_condition.has_value())
915  return {*maybe_null_condition};
916  else
917  return {};
918 }
919 
920 std::string goto_check_javat::array_name(const exprt &expr)
921 {
922  return ::array_name(ns, expr);
923 }
924 
926 {
928  return;
929 
930  if(
931  expr.find(ID_C_bounds_check).is_not_nil() &&
932  !expr.get_bool(ID_C_bounds_check))
933  {
934  return;
935  }
936 
937  if(expr.id() == ID_index)
939 }
940 
942 {
943  const typet &array_type = expr.array().type();
944 
945  if(array_type.id() == ID_pointer)
946  throw "index got pointer as array type";
947  else if(array_type.id() != ID_array && array_type.id() != ID_vector)
948  throw "bounds check expected array or vector type, got " +
949  array_type.id_string();
950 
951  std::string name = array_name(expr.array());
952 
953  const exprt &index = expr.index();
955  ode.build(expr, ns);
956 
957  if(index.type().id() != ID_unsignedbv)
958  {
959  // we undo typecasts to signedbv
960  if(
961  index.id() == ID_typecast &&
962  to_typecast_expr(index).op().type().id() == ID_unsignedbv)
963  {
964  // ok
965  }
966  else
967  {
968  const auto i = numeric_cast<mp_integer>(index);
969 
970  if(!i.has_value() || *i < 0)
971  {
972  exprt effective_offset = ode.offset();
973 
974  if(ode.root_object().id() == ID_dereference)
975  {
976  exprt p_offset =
978 
979  effective_offset = plus_exprt{p_offset,
981  effective_offset, p_offset.type())};
982  }
983 
984  exprt zero = from_integer(0, ode.offset().type());
985 
986  // the final offset must not be negative
987  binary_relation_exprt inequality(
988  effective_offset, ID_ge, std::move(zero));
989 
990  add_property(
991  inequality,
992  name + " lower bound",
993  "array bounds",
994  expr.find_source_location(),
995  expr);
996  }
997  }
998  }
999 
1000  if(ode.root_object().id() == ID_dereference)
1001  {
1002  const exprt &pointer = to_dereference_expr(ode.root_object()).pointer();
1003 
1004  const plus_exprt effective_offset{
1005  ode.offset(),
1007  pointer_offset(pointer), ode.offset().type())};
1008 
1009  binary_relation_exprt inequality{
1010  effective_offset,
1011  ID_lt,
1013  object_size(pointer), effective_offset.type())};
1014 
1015  add_property(
1016  inequality,
1017  name + " dynamic object upper bound",
1018  "array bounds",
1019  expr.find_source_location(),
1020  expr);
1021 
1022  return;
1023  }
1024 
1025  const exprt &size = array_type.id() == ID_array
1026  ? to_array_type(array_type).size()
1027  : to_vector_type(array_type).size();
1028 
1029  if(size.is_nil())
1030  {
1031  // Linking didn't complete, we don't have a size.
1032  // Not clear what to do.
1033  }
1034  else if(size.id() == ID_infinity)
1035  {
1036  }
1037  else if(size.is_zero() && expr.array().id() == ID_member)
1038  {
1039  // a variable sized struct member
1040  //
1041  // Excerpt from the C standard on flexible array members:
1042  // However, when a . (or ->) operator has a left operand that is (a pointer
1043  // to) a structure with a flexible array member and the right operand names
1044  // that member, it behaves as if that member were replaced with the longest
1045  // array (with the same element type) that would not make the structure
1046  // larger than the object being accessed; [...]
1047  const auto type_size_opt = size_of_expr(ode.root_object().type(), ns);
1048  CHECK_RETURN(type_size_opt.has_value());
1049 
1050  binary_relation_exprt inequality(
1052  ode.offset(), type_size_opt.value().type()),
1053  ID_lt,
1054  type_size_opt.value());
1055 
1056  add_property(
1057  inequality,
1058  name + " upper bound",
1059  "array bounds",
1060  expr.find_source_location(),
1061  expr);
1062  }
1063  else
1064  {
1065  binary_relation_exprt inequality{
1066  typecast_exprt::conditional_cast(index, size.type()), ID_lt, size};
1067 
1068  add_property(
1069  inequality,
1070  name + " upper bound",
1071  "array bounds",
1072  expr.find_source_location(),
1073  expr);
1074  }
1075 }
1076 
1078  const exprt &asserted_expr,
1079  const std::string &comment,
1080  const std::string &property_class,
1081  const source_locationt &source_location,
1082  const exprt &src_expr)
1083 {
1084  // first try simplifier on it
1085  exprt simplified_expr =
1086  enable_simplify ? simplify_expr(asserted_expr, ns) : asserted_expr;
1087 
1088  // throw away trivial properties?
1089  if(!retain_trivial && simplified_expr.is_true())
1090  return;
1091 
1092  if(assertions.insert(std::make_pair(src_expr, simplified_expr)).second)
1093  {
1094  auto t = new_code.add(
1096  std::move(simplified_expr), source_location)
1098  std::move(simplified_expr), source_location));
1099 
1100  std::string source_expr_string;
1101  get_language_from_mode(ID_java)->from_expr(
1102  src_expr, source_expr_string, ns);
1103 
1104  t->source_location_nonconst().set_comment(
1105  comment + " in " + source_expr_string);
1106  t->source_location_nonconst().set_property_class(property_class);
1107  }
1108 }
1109 
1111 {
1112  // we don't look into quantifiers
1113  if(expr.id() == ID_exists || expr.id() == ID_forall)
1114  return;
1115 
1116  if(expr.id() == ID_dereference)
1117  {
1118  check_rec(to_dereference_expr(expr).pointer());
1119  }
1120  else if(expr.id() == ID_index)
1121  {
1122  const index_exprt &index_expr = to_index_expr(expr);
1123  check_rec_address(index_expr.array());
1124  check_rec(index_expr.index());
1125  }
1126  else
1127  {
1128  for(const auto &operand : expr.operands())
1129  check_rec_address(operand);
1130  }
1131 }
1132 
1134 {
1135  const dereference_exprt &deref = to_dereference_expr(member.struct_op());
1136 
1137  check_rec(deref.pointer());
1138 
1139  // avoid building the following expressions when pointer_validity_check
1140  // would return immediately anyway
1142  return true;
1143 
1144  // we rewrite s->member into *(s+member_offset)
1145  // to avoid requiring memory safety of the entire struct
1146  auto member_offset_opt = member_offset_expr(member, ns);
1147 
1148  if(member_offset_opt.has_value())
1149  {
1150  pointer_typet new_pointer_type = to_pointer_type(deref.pointer().type());
1151  new_pointer_type.base_type() = member.type();
1152 
1153  const exprt char_pointer = typecast_exprt::conditional_cast(
1154  deref.pointer(), pointer_type(char_type()));
1155 
1156  const exprt new_address_casted = typecast_exprt::conditional_cast(
1157  plus_exprt{char_pointer,
1159  member_offset_opt.value(), pointer_diff_type())},
1160  new_pointer_type);
1161 
1162  dereference_exprt new_deref{new_address_casted};
1163  new_deref.add_source_location() = deref.source_location();
1164  pointer_validity_check(new_deref, member);
1165 
1166  return true;
1167  }
1168  return false;
1169 }
1170 
1172 {
1173  div_by_zero_check(to_div_expr(div_expr));
1174 
1175  if(div_expr.type().id() == ID_signedbv)
1176  integer_overflow_check(div_expr);
1177  else if(div_expr.type().id() == ID_floatbv)
1178  {
1179  nan_check(div_expr);
1180  float_overflow_check(div_expr);
1181  }
1182 }
1183 
1185 {
1186  if(expr.type().id() == ID_signedbv || expr.type().id() == ID_unsignedbv)
1187  {
1188  integer_overflow_check(expr);
1189  }
1190  else if(expr.type().id() == ID_floatbv)
1191  {
1192  nan_check(expr);
1193  float_overflow_check(expr);
1194  }
1195 }
1196 
1198 {
1199  // we don't look into quantifiers
1200  if(expr.id() == ID_exists || expr.id() == ID_forall)
1201  return;
1202 
1203  if(expr.id() == ID_address_of)
1204  {
1205  check_rec_address(to_address_of_expr(expr).object());
1206  return;
1207  }
1208  else if(
1209  expr.id() == ID_member &&
1210  to_member_expr(expr).struct_op().id() == ID_dereference)
1211  {
1212  if(check_rec_member(to_member_expr(expr)))
1213  return;
1214  }
1215 
1216  forall_operands(it, expr)
1217  check_rec(*it);
1218 
1219  if(expr.id() == ID_index)
1220  {
1221  bounds_check(expr);
1222  }
1223  else if(expr.id() == ID_div)
1224  {
1225  check_rec_div(to_div_expr(expr));
1226  }
1227  else if(expr.id() == ID_shl)
1228  {
1229  if(expr.type().id() == ID_signedbv)
1230  integer_overflow_check(expr);
1231  }
1232  else if(expr.id() == ID_mod)
1233  {
1235  }
1236  else if(
1237  expr.id() == ID_plus || expr.id() == ID_minus || expr.id() == ID_mult ||
1238  expr.id() == ID_unary_minus)
1239  {
1241  }
1242  else if(expr.id() == ID_typecast)
1243  conversion_check(expr);
1244  else if(expr.id() == ID_dereference)
1245  {
1247  }
1248 }
1249 
1251 {
1252  check_rec(expr);
1253 }
1254 
1257 {
1258  bool modified = false;
1259 
1260  for(auto &op : expr.operands())
1261  {
1262  auto op_result = rw_ok_check(op);
1263  if(op_result.has_value())
1264  {
1265  op = *op_result;
1266  modified = true;
1267  }
1268  }
1269 
1270  if(expr.id() == ID_r_ok || expr.id() == ID_w_ok || expr.id() == ID_rw_ok)
1271  {
1272  // these get an address as first argument and a size as second
1274  expr.operands().size() == 2, "r/w_ok must have two operands");
1275 
1276  const auto conditions = get_pointer_dereferenceable_conditions(
1277  to_r_or_w_ok_expr(expr).pointer(), to_r_or_w_ok_expr(expr).size());
1278 
1279  exprt::operandst conjuncts;
1280 
1281  for(const auto &c : conditions)
1282  conjuncts.push_back(c.assertion);
1283 
1284  return conjunction(conjuncts);
1285  }
1286  else if(modified)
1287  return std::move(expr);
1288  else
1289  return {};
1290 }
1291 
1293  const irep_idt &function_identifier,
1294  goto_functiont &goto_function)
1295 {
1296  const auto &function_symbol = ns.lookup(function_identifier);
1297 
1298  if(function_symbol.mode != ID_java)
1299  return;
1300 
1301  assertions.clear();
1302 
1303  bool did_something = false;
1304 
1306  util_make_unique<local_bitvector_analysist>(goto_function, ns);
1307 
1308  goto_programt &goto_program = goto_function.body;
1309 
1310  Forall_goto_program_instructions(it, goto_program)
1311  {
1312  current_target = it;
1313  goto_programt::instructiont &i = *it;
1314 
1315  new_code.clear();
1316 
1317  // we clear all recorded assertions if
1318  // 1) we want to generate all assertions or
1319  // 2) the instruction is a branch target
1320  if(retain_trivial || i.is_target())
1321  assertions.clear();
1322 
1323  if(i.has_condition())
1324  {
1325  check(i.get_condition());
1326 
1327  if(has_subexpr(i.get_condition(), [](const exprt &expr) {
1328  return expr.id() == ID_r_ok || expr.id() == ID_w_ok ||
1329  expr.id() == ID_rw_ok;
1330  }))
1331  {
1332  auto rw_ok_cond = rw_ok_check(i.get_condition());
1333  if(rw_ok_cond.has_value())
1334  i.set_condition(*rw_ok_cond);
1335  }
1336  }
1337 
1338  // magic ERROR label?
1339  for(const auto &label : error_labels)
1340  {
1341  if(std::find(i.labels.begin(), i.labels.end(), label) != i.labels.end())
1342  {
1343  auto t = new_code.add(
1347  false_exprt{}, i.source_location()));
1348 
1349  t->source_location_nonconst().set_property_class("error label");
1350  t->source_location_nonconst().set_comment("error label " + label);
1351  t->source_location_nonconst().set("user-provided", true);
1352  }
1353  }
1354 
1355  if(i.is_other())
1356  {
1357  const auto &code = i.get_other();
1358  const irep_idt &statement = code.get_statement();
1359 
1360  if(statement == ID_expression)
1361  {
1362  check(code);
1363  }
1364  else if(statement == ID_printf)
1365  {
1366  for(const auto &op : code.operands())
1367  check(op);
1368  }
1369  }
1370  else if(i.is_assign())
1371  {
1372  const exprt &assign_lhs = i.assign_lhs();
1373  const exprt &assign_rhs = i.assign_rhs();
1374 
1375  check(assign_lhs);
1376  check(assign_rhs);
1377 
1378  // the LHS might invalidate any assertion
1379  invalidate(assign_lhs);
1380 
1381  if(has_subexpr(assign_rhs, [](const exprt &expr) {
1382  return expr.id() == ID_r_ok || expr.id() == ID_w_ok ||
1383  expr.id() == ID_rw_ok;
1384  }))
1385  {
1386  auto rw_ok_cond = rw_ok_check(assign_rhs);
1387  if(rw_ok_cond.has_value())
1388  i.assign_rhs_nonconst() = *rw_ok_cond;
1389  }
1390  }
1391  else if(i.is_function_call())
1392  {
1393  const auto &function = i.call_function();
1394 
1395  // for Java, need to check whether 'this' is null
1396  // on non-static method invocations
1397  if(
1398  enable_pointer_check && !i.call_arguments().empty() &&
1399  function.type().id() == ID_code &&
1400  to_code_type(function.type()).has_this())
1401  {
1402  exprt pointer = i.call_arguments()[0];
1403 
1406 
1407  if(flags.is_unknown() || flags.is_null())
1408  {
1409  notequal_exprt not_eq_null(
1410  pointer, null_pointer_exprt(to_pointer_type(pointer.type())));
1411 
1412  add_property(
1413  not_eq_null,
1414  "this is null on method invocation",
1415  "pointer dereference",
1416  i.source_location(),
1417  pointer);
1418  }
1419  }
1420 
1421  check(i.call_lhs());
1422  check(i.call_function());
1423 
1424  for(const auto &arg : i.call_arguments())
1425  check(arg);
1426 
1427  // the call might invalidate any assertion
1428  assertions.clear();
1429  }
1430  else if(i.is_set_return_value())
1431  {
1432  check(i.return_value());
1433  // the return value invalidate any assertion
1434  invalidate(i.return_value());
1435 
1436  if(has_subexpr(i.return_value(), [](const exprt &expr) {
1437  return expr.id() == ID_r_ok || expr.id() == ID_w_ok ||
1438  expr.id() == ID_rw_ok;
1439  }))
1440  {
1441  exprt &return_value = i.return_value();
1442  auto rw_ok_cond = rw_ok_check(return_value);
1443  if(rw_ok_cond.has_value())
1444  return_value = *rw_ok_cond;
1445  }
1446  }
1447  else if(i.is_throw())
1448  {
1449  if(
1450  i.get_code().get_statement() == ID_expression &&
1451  i.get_code().operands().size() == 1 &&
1452  i.get_code().op0().operands().size() == 1)
1453  {
1454  // must not throw NULL
1455 
1456  exprt pointer = to_unary_expr(i.get_code().op0()).op();
1457 
1458  const notequal_exprt not_eq_null(
1459  pointer, null_pointer_exprt(to_pointer_type(pointer.type())));
1460 
1461  add_property(
1462  not_eq_null,
1463  "throwing null",
1464  "pointer dereference",
1465  i.source_location(),
1466  pointer);
1467  }
1468 
1469  // this has no successor
1470  assertions.clear();
1471  }
1472  else if(i.is_assert())
1473  {
1474  bool is_user_provided = i.source_location().get_bool("user-provided");
1475 
1476  if(
1477  (is_user_provided && !enable_assertions &&
1478  i.source_location().get_property_class() != "error label") ||
1479  (!is_user_provided && !enable_built_in_assertions))
1480  {
1481  i.turn_into_skip();
1482  did_something = true;
1483  }
1484  }
1485  else if(i.is_assume())
1486  {
1487  if(!enable_assumptions)
1488  {
1489  i.turn_into_skip();
1490  did_something = true;
1491  }
1492  }
1493  else if(i.is_dead())
1494  {
1496  {
1497  const symbol_exprt &variable = i.dead_symbol();
1498 
1499  // is it dirty?
1500  if(local_bitvector_analysis->dirty(variable))
1501  {
1502  // need to mark the dead variable as dead
1503  exprt lhs = ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr();
1504  exprt address_of_expr = typecast_exprt::conditional_cast(
1505  address_of_exprt(variable), lhs.type());
1506  if_exprt rhs(
1508  std::move(address_of_expr),
1509  lhs);
1512  std::move(lhs), std::move(rhs), i.source_location()));
1513  t->code_nonconst().add_source_location() = i.source_location();
1514  }
1515 
1516  if(
1517  variable.type().id() == ID_pointer &&
1518  function_identifier != "alloca" &&
1519  (ns.lookup(variable.get_identifier()).base_name ==
1520  "return_value___builtin_alloca" ||
1521  ns.lookup(variable.get_identifier()).base_name ==
1522  "return_value_alloca"))
1523  {
1524  // mark pointer to alloca result as dead
1525  exprt lhs = ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr();
1526  exprt alloca_result =
1527  typecast_exprt::conditional_cast(variable, lhs.type());
1528  if_exprt rhs(
1530  std::move(alloca_result),
1531  lhs);
1534  std::move(lhs), std::move(rhs), i.source_location()));
1535  t->code_nonconst().add_source_location() = i.source_location();
1536  }
1537  }
1538  }
1539 
1540  for(auto &instruction : new_code.instructions)
1541  {
1542  if(instruction.source_location().is_nil())
1543  {
1544  instruction.source_location_nonconst().id(irep_idt());
1545 
1546  if(!it->source_location().get_file().empty())
1547  instruction.source_location_nonconst().set_file(
1548  it->source_location().get_file());
1549 
1550  if(!it->source_location().get_line().empty())
1551  instruction.source_location_nonconst().set_line(
1552  it->source_location().get_line());
1553 
1554  if(!it->source_location().get_function().empty())
1555  instruction.source_location_nonconst().set_function(
1556  it->source_location().get_function());
1557 
1558  if(!it->source_location().get_column().empty())
1559  {
1560  instruction.source_location_nonconst().set_column(
1561  it->source_location().get_column());
1562  }
1563 
1564  if(!it->source_location().get_java_bytecode_index().empty())
1565  {
1566  instruction.source_location_nonconst().set_java_bytecode_index(
1567  it->source_location().get_java_bytecode_index());
1568  }
1569  }
1570  }
1571 
1572  // insert new instructions -- make sure targets are not moved
1573  did_something |= !new_code.instructions.empty();
1574 
1575  while(!new_code.instructions.empty())
1576  {
1577  goto_program.insert_before_swap(it, new_code.instructions.front());
1578  new_code.instructions.pop_front();
1579  it++;
1580  }
1581  }
1582 
1583  if(did_something)
1584  remove_skip(goto_program);
1585 }
1586 
1589  const exprt &address,
1590  const exprt &size)
1591 {
1593  PRECONDITION(address.type().id() == ID_pointer);
1594  const auto &pointer_type = to_pointer_type(address.type());
1597 
1598  if(flags.is_unknown() || flags.is_null())
1599  {
1600  notequal_exprt not_eq_null(address, null_pointer_exprt{pointer_type});
1601  return {conditiont{not_eq_null, "reference is null"}};
1602  }
1603 
1604  return {};
1605 }
1606 
1608  const irep_idt &function_identifier,
1609  goto_functionst::goto_functiont &goto_function,
1610  const namespacet &ns,
1611  const optionst &options,
1612  message_handlert &message_handler)
1613 {
1614  goto_check_javat goto_check(ns, options, message_handler);
1615  goto_check.goto_check(function_identifier, goto_function);
1616 }
1617 
1619  const namespacet &ns,
1620  const optionst &options,
1621  goto_functionst &goto_functions,
1622  message_handlert &message_handler)
1623 {
1624  goto_check_javat goto_check(ns, options, message_handler);
1625 
1626  for(auto &gf_entry : goto_functions.function_map)
1627  {
1628  goto_check.goto_check(gf_entry.first, gf_entry.second);
1629  }
1630 }
1631 
1633  const optionst &options,
1634  goto_modelt &goto_model,
1635  message_handlert &message_handler)
1636 {
1637  const namespacet ns(goto_model.symbol_table);
1638  goto_check_java(ns, options, goto_model.goto_functions, message_handler);
1639 }
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
std::string array_name(const namespacet &ns, const exprt &expr)
Definition: array_name.cpp:19
Misc Utilities.
API to expression classes for bitvectors.
const shl_exprt & to_shl_expr(const exprt &expr)
Cast an exprt to a shl_exprt.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
unsignedbv_typet size_type()
Definition: c_types.cpp:68
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:253
signedbv_typet pointer_diff_type()
Definition: c_types.cpp:238
bitvector_typet char_type()
Definition: c_types.cpp:124
Operator to return the address of an object.
Definition: pointer_expr.h:361
Boolean AND.
Definition: std_expr.h:1974
const exprt & size() const
Definition: std_types.h:790
A base class for binary expressions.
Definition: std_expr.h:550
exprt & op1()
Definition: expr.h:102
exprt & lhs()
Definition: std_expr.h:580
exprt & op0()
Definition: expr.h:99
exprt & rhs()
Definition: std_expr.h:590
A Boolean expression returning true, iff operation kind would result in an overflow when applied to o...
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition: std_expr.h:643
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:674
std::size_t get_width() const
Definition: std_types.h:864
The Boolean type.
Definition: std_types.h:36
exprt & op0()
Definition: expr.h:99
const irep_idt & get_statement() const
Definition: std_code_base.h:65
Operator to dereference a pointer.
Definition: pointer_expr.h:648
Division.
Definition: std_expr.h:1064
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Equality.
Definition: std_expr.h:1225
Base class for all expressions.
Definition: expr.h:54
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition: expr.cpp:165
std::vector< exprt > operandst
Definition: expr.h:56
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:33
source_locationt & add_source_location()
Definition: expr.h:235
const source_locationt & source_location() const
Definition: expr.h:230
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:64
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
Extracts a sub-range of a bit-vector operand.
The Boolean constant false.
Definition: std_expr.h:2865
goto_check_javat(const namespacet &_ns, const optionst &_options, message_handlert &_message_handler)
void check(const exprt &expr)
Initiate the recursively analysis of expr with its ‘guard’ set to TRUE.
bool check_rec_member(const member_exprt &member)
Check that a member expression is valid:
void goto_check(const irep_idt &function_identifier, goto_functiont &goto_function)
void check_rec(const exprt &expr)
Recursively descend into expr and run the appropriate check for each sub-expression,...
std::unique_ptr< local_bitvector_analysist > local_bitvector_analysis
const namespacet & ns
void invalidate(const exprt &lhs)
Remove all assertions containing the symbol in lhs as well as all assertions containing dereference.
void integer_overflow_check(const exprt &)
void float_overflow_check(const exprt &)
void mod_overflow_check(const mod_exprt &)
check a mod expression for the case INT_MIN % -1
optionst::value_listt error_labelst
void add_property(const exprt &asserted_expr, const std::string &comment, const std::string &property_class, const source_locationt &source_location, const exprt &src_expr)
Include the asserted_expr in the code conditioned by the guard.
goto_functionst::goto_functiont goto_functiont
std::list< conditiont > conditionst
void bounds_check(const exprt &)
std::string array_name(const exprt &)
goto_programt::const_targett current_target
optionalt< goto_check_javat::conditiont > get_pointer_is_null_condition(const exprt &address, const exprt &size)
void pointer_validity_check(const dereference_exprt &expr, const exprt &src_expr)
Generates VCCs for the validity of the given dereferencing operation.
optionalt< exprt > rw_ok_check(exprt)
expand the r_ok, w_ok and rw_ok predicates
void nan_check(const exprt &)
void check_rec_arithmetic_op(const exprt &expr)
Check that an arithmetic operation is valid: overflow check, NaN-check (for floating point numbers),...
error_labelst error_labels
void check_rec_div(const div_exprt &div_expr)
Check that a division is valid: check for division by zero, overflow and NaN (for floating point numb...
conditionst get_pointer_dereferenceable_conditions(const exprt &address, const exprt &size)
void bounds_check_index(const index_exprt &)
void check_rec_address(const exprt &expr)
Check an address-of expression: if it is a dereference then check the pointer if it is an index then ...
std::set< std::pair< exprt, exprt > > assertionst
goto_programt new_code
void div_by_zero_check(const div_exprt &)
void conversion_check(const exprt &)
assertionst assertions
A collection of goto functions.
function_mapt function_map
::goto_functiont goto_functiont
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
Definition: goto_function.h:24
goto_programt body
Definition: goto_function.h:26
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:180
void turn_into_skip()
Transforms an existing instruction into a skip, retaining the source_location.
Definition: goto_program.h:448
const exprt & call_lhs() const
Get the lhs of a FUNCTION_CALL (may be nil)
Definition: goto_program.h:285
bool is_target() const
Is this node a branch target?
Definition: goto_program.h:434
bool is_set_return_value() const
Definition: goto_program.h:473
const codet & get_other() const
Get the statement for OTHER.
Definition: goto_program.h:313
const exprt & call_function() const
Get the function that is called for FUNCTION_CALL.
Definition: goto_program.h:271
bool has_condition() const
Does this instruction have a condition?
Definition: goto_program.h:360
exprt & assign_rhs_nonconst()
Get the rhs of the assignment for ASSIGN.
Definition: goto_program.h:220
const exprt & return_value() const
Get the return value of a SET_RETURN_VALUE instruction.
Definition: goto_program.h:257
const exprt & get_condition() const
Get the condition of gotos, assume, assert.
Definition: goto_program.h:367
const codet & get_code() const
Get the code represented by this instruction.
Definition: goto_program.h:187
const exprt & assign_rhs() const
Get the rhs of the assignment for ASSIGN.
Definition: goto_program.h:213
const source_locationt & source_location() const
Definition: goto_program.h:332
void set_condition(exprt c)
Set the condition of gotos, assume, assert.
Definition: goto_program.h:375
const symbol_exprt & dead_symbol() const
Get the symbol for DEAD.
Definition: goto_program.h:243
const exprt & assign_lhs() const
Get the lhs of the assignment for ASSIGN.
Definition: goto_program.h:199
const exprt::operandst & call_arguments() const
Get the arguments of a FUNCTION_CALL.
Definition: goto_program.h:299
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:934
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:598
void clear()
Clear the goto program.
Definition: goto_program.h:809
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:619
instructionst::iterator targett
Definition: goto_program.h:592
instructionst::const_iterator const_targett
Definition: goto_program.h:593
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:715
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:922
IEEE-floating-point equality.
Definition: floatbv_expr.h:264
constant_exprt to_expr() const
Definition: ieee_float.cpp:702
static ieee_floatt plus_infinity(const ieee_float_spect &_spec)
Definition: ieee_float.h:212
static ieee_floatt minus_infinity(const ieee_float_spect &_spec)
Definition: ieee_float.h:215
void from_integer(const mp_integer &i)
Definition: ieee_float.cpp:515
The trinary if-then-else operator.
Definition: std_expr.h:2226
Array index operator.
Definition: std_expr.h:1328
exprt & array()
Definition: std_expr.h:1353
exprt & index()
Definition: std_expr.h:1363
bool get_bool(const irep_idt &name) const
Definition: irep.cpp:58
const irept & find(const irep_idt &name) const
Definition: irep.cpp:106
const std::string & id_string() const
Definition: irep.h:399
bool is_not_nil() const
Definition: irep.h:380
const irep_idt & id() const
Definition: irep.h:396
bool is_nil() const
Definition: irep.h:376
Evaluates to true if the operand is infinite.
Definition: floatbv_expr.h:132
Extract member of struct or union.
Definition: std_expr.h:2667
const exprt & struct_op() const
Definition: std_expr.h:2697
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
Definition: std_expr.h:1135
A base class for multi-ary expressions Associativity is not specified.
Definition: std_expr.h:824
exprt & op0()
Definition: std_expr.h:844
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
Boolean negation.
Definition: std_expr.h:2181
Disequality.
Definition: std_expr.h:1283
The null pointer constant.
Definition: pointer_expr.h:723
Split an expression into a base object and a (byte) offset.
Definition: pointer_expr.h:167
void build(const exprt &expr, const namespacet &ns)
Given an expression expr, attempt to find the underlying object it represents by skipping over type c...
static const exprt & root_object(const exprt &expr)
bool get_bool_option(const std::string &option) const
Definition: options.cpp:44
const value_listt & get_list_option(const std::string &option) const
Definition: options.cpp:80
std::list< std::string > value_listt
Definition: options.h:25
Boolean OR.
Definition: std_expr.h:2082
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 ...
Definition: pointer_expr.h:24
const typet & base_type() const
The type of the data what we point to.
Definition: pointer_expr.h:35
Left shift.
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1520
const irep_idt & get_property_class() const
Expression to hold a symbol (variable)
Definition: std_expr.h:80
const irep_idt & get_identifier() const
Definition: std_expr.h:109
Semantic type conversion.
Definition: std_expr.h:1920
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
const exprt & op() const
Definition: std_expr.h:293
A Boolean expression returning true, iff operation kind would result in an overflow when applied to t...
Fixed-width bit-vector with unsigned binary interpretation.
const constant_exprt & size() const
Definition: std_types.cpp:253
#define CPROVER_PREFIX
#define forall_operands(it, expr)
Definition: expr.h:18
exprt make_binary(const exprt &expr)
splits an expression with >=3 operands into nested binary expressions
Definition: expr_util.cpp:35
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
Definition: expr_util.cpp:138
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Definition: expr_util.cpp:126
Deprecated expression utility functions.
bool has_symbol(const exprt &src, const find_symbols_sett &symbols, bool current, bool next)
std::unordered_set< irep_idt > find_symbols_sett
Definition: find_symbols.h:21
API to expression classes for floating-point arithmetic.
void goto_check(const irep_idt &function_identifier, goto_functionst::goto_functiont &goto_function, const namespacet &ns, const optionst &options, message_handlert &message_handler)
Definition: goto_check.cpp:18
void goto_check_java(const irep_idt &function_identifier, goto_functionst::goto_functiont &goto_function, const namespacet &ns, const optionst &options, message_handlert &message_handler)
Check for Errors in Java Programs.
Symbol Table + CFG.
#define Forall_goto_program_instructions(it, program)
dstringt irep_idt
Definition: irep.h:37
Abstract interface to support a programming language.
Field-insensitive, location-sensitive bitvector analysis.
std::unique_ptr< languaget > get_language_from_mode(const irep_idt &mode)
Get the language corresponding to the given mode.
Definition: mode.cpp:51
nonstd::optional< T > optionalt
Definition: optional.h:35
Options.
API to expression classes for Pointers.
const r_or_w_ok_exprt & to_r_or_w_ok_expr(const exprt &expr)
Definition: pointer_expr.h:752
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:704
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:79
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:398
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
optionalt< exprt > member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
Pointer Logic.
exprt pointer_offset(const exprt &pointer)
exprt object_size(const exprt &pointer)
Various predicates over pointers in programs.
static std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:109
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:88
Program Transformation.
exprt simplify_expr(exprt src, const namespacet &ns)
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition: std_expr.cpp:34
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition: std_expr.cpp:22
API to expression classes.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
const mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
Definition: std_expr.h:1160
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1954
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
Definition: std_expr.h:420
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
Definition: std_expr.h:1113
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
Definition: std_expr.h:998
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 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 member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2751
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:328
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1391
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
Definition: std_expr.h:1044
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition: std_types.h:1040
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:744
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:832
conditiont(const exprt &_assertion, const std::string &_description)