cprover
Loading...
Searching...
No Matches
goto_check_java.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Checks for Errors in Java Programs
4
5Author: 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{
48public:
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
82protected:
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
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
248 inequality,
249 "division by zero",
250 "division-by-zero",
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
277 or_exprt(int_min_neq, minus_one_neq),
278 "result of signed mod is not representable",
279 "overflow",
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
320 and_exprt(no_overflow_lower, no_overflow_upper),
321 "arithmetic overflow on signed type conversion",
322 "overflow",
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
336 no_overflow_upper,
337 "arithmetic overflow on unsigned to signed type conversion",
338 "overflow",
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
356 and_exprt(no_overflow_lower, no_overflow_upper),
357 "arithmetic overflow on float to signed integer type conversion",
358 "overflow",
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
378 no_overflow_lower,
379 "arithmetic overflow on signed to unsigned type conversion",
380 "overflow",
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
394 and_exprt(no_overflow_lower, no_overflow_upper),
395 "arithmetic overflow on signed to unsigned type conversion",
396 "overflow",
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
411 no_overflow_upper,
412 "arithmetic overflow on unsigned to unsigned type conversion",
413 "overflow",
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
431 and_exprt(no_overflow_lower, no_overflow_upper),
432 "arithmetic overflow on float to unsigned integer type conversion",
433 "overflow",
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
470 not_exprt(and_exprt(int_min_eq, minus_one_eq)),
471 "arithmetic overflow on signed division",
472 "overflow",
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
490 not_exprt(int_min_eq),
491 "arithmetic overflow on signed unary minus",
492 "overflow",
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
505 not_eq_zero,
506 "arithmetic overflow on unsigned unary minus",
507 "overflow",
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
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",
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
623 not_exprt{binary_overflow_exprt{tmp, expr.id(), expr.operands()[i]}},
624 "arithmetic overflow on " + kind + " " + expr.id_string(),
625 "overflow",
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);
636 not_exprt{binary_overflow_exprt{bexpr.lhs(), expr.id(), bexpr.rhs()}},
637 "arithmetic overflow on " + kind + " " + expr.id_string(),
638 "overflow",
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
649 not_exprt{unary_overflow_exprt{expr.id(), to_unary_expr(expr).op()}},
650 "arithmetic overflow on " + kind + " " + expr.id_string(),
651 "overflow",
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
681 std::move(overflow_check),
682 "arithmetic overflow on floating-point typecast",
683 "overflow",
685 expr);
686 }
687 else
688 {
689 // non-float-to-float
691 not_exprt(isinf_exprt(expr)),
692 "arithmetic overflow on floating-point typecast",
693 "overflow",
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
707 std::move(overflow_check),
708 "arithmetic overflow on floating-point division",
709 "overflow",
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
742 std::move(overflow_check),
743 "arithmetic overflow on floating-point " + kind,
744 "overflow",
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{
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
859
861 boolean_negate(isnan),
862 "NaN on " + expr.id_string(),
863 "NaN",
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 {
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
920std::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
991 inequality,
992 name + " lower bound",
993 "array bounds",
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
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
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
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 {
1189 }
1190 else if(expr.type().id() == ID_floatbv)
1191 {
1192 nan_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 {
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 {
1226 }
1227 else if(expr.id() == ID_shl)
1228 {
1229 if(expr.type().id() == ID_signedbv)
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;
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(
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
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
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
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 {
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)
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
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 bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_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.
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 & lhs()
Definition std_expr.h:580
exprt & rhs()
Definition std_expr.h:590
exprt & op0()
Definition expr.h:99
exprt & op1()
Definition expr.h:102
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
bool has_this() const
Definition std_types.h:616
exprt & op0()
Definition expr.h:99
const irep_idt & get_statement() const
Operator to dereference a pointer.
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
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
const source_locationt & source_location() const
Definition expr.h:230
source_locationt & add_source_location()
Definition expr.h:235
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 &)
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...
goto_programt body
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.
const symbol_exprt & dead_symbol() const
Get the symbol for DEAD.
const exprt & call_lhs() const
Get the lhs of a FUNCTION_CALL (may be nil)
void turn_into_skip()
Transforms an existing instruction into a skip, retaining the source_location.
bool is_target() const
Is this node a branch target?
const exprt & return_value() const
Get the return value of a SET_RETURN_VALUE instruction.
const codet & get_code() const
Get the code represented by this instruction.
bool has_condition() const
Does this instruction have a condition?
const codet & get_other() const
Get the statement for OTHER.
const exprt & get_condition() const
Get the condition of gotos, assume, assert.
const exprt::operandst & call_arguments() const
Get the arguments of a FUNCTION_CALL.
const exprt & assign_lhs() const
Get the lhs of the assignment for ASSIGN.
const exprt & assign_rhs() const
Get the rhs of the assignment for ASSIGN.
const exprt & call_function() const
Get the function that is called for FUNCTION_CALL.
void set_condition(exprt c)
Set the condition of gotos, assume, assert.
exprt & assign_rhs_nonconst()
Get the rhs of the assignment for ASSIGN.
const source_locationt & source_location() const
A generic container class for the GOTO intermediate representation of one function.
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
instructionst instructions
The list of instructions in the goto program.
void clear()
Clear the goto program.
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
instructionst::iterator targett
instructionst::const_iterator const_targett
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.
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
IEEE-floating-point equality.
constant_exprt to_expr() const
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)
The trinary if-then-else operator.
Definition std_expr.h:2226
Array index operator.
Definition std_expr.h:1328
exprt & index()
Definition std_expr.h:1363
exprt & array()
Definition std_expr.h:1353
bool get_bool(const irep_idt &name) const
Definition irep.cpp:58
const irept & find(const irep_idt &name) const
Definition irep.cpp:106
bool is_not_nil() const
Definition irep.h:380
const std::string & id_string() const
Definition irep.h:399
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.
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().
Boolean negation.
Definition std_expr.h:2181
Disequality.
Definition std_expr.h:1283
The null pointer constant.
Split an expression into a base object and a (byte) offset.
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 ...
const typet & base_type() const
The type of the data what we point to.
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
#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
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
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
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)
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)
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
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.
optionalt< exprt > member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
optionalt< exprt > size_of_expr(const typet &type, 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)
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
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 index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1391
const mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
Definition std_expr.h:1160
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
Definition std_expr.h:1044
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:1954
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
Definition std_expr.h:1113
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
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
Definition std_expr.h:998
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:189
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 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)