cprover
Loading...
Searching...
No Matches
interval.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3 Module: intervals
4
5 Author: Daniel Neville (2017), Diffblue Ltd
6
7\*******************************************************************/
8
9/*
10 *
11 * Types: Should we store a type for the entire interval?
12 * IMO: I think YES (for the case where we have -inf -> inf, we don't know otherwise
13 *
14 * This initial implementation only implements support for integers.
15 */
16
17#include "interval.h"
18
19#include <ostream>
20
21#include "arith_tools.h"
22#include "bitvector_expr.h"
23#include "c_types.h"
24#include "namespace.h"
25#include "simplify_expr.h"
26#include "std_expr.h"
27#include "symbol_table.h"
28
30{
31 return op0();
32}
33
35{
36 return op1();
37}
38
40{
41 return *this;
42}
43
45{
47 {
49 }
50
51 exprt lower;
52 exprt upper;
53
55 {
56 lower = min();
57 }
58 else
59 {
61 }
62
64 {
65 upper = max();
66 }
67 else
68 {
70 }
71
72 return constant_interval_exprt(lower, upper);
73}
74
77{
79 {
81 }
82
83 exprt lower = min();
84 exprt upper = max();
85
86 if(is_max(get_upper()) || is_max(o.get_upper()))
87 {
88 upper = max_exprt(type());
89 }
90 else
91 {
93 !is_max(get_upper()) && !is_max(o.get_upper()),
94 "We just excluded this case");
96 }
97
98 if(is_min(get_lower()) || is_min(o.get_lower()))
99 {
100 lower = min_exprt(type());
101 }
102 else
103 {
104 INVARIANT(
105 !is_min(get_lower()) && !is_min(o.get_lower()),
106 "We just excluded that case");
108 }
109
110 return simplified_interval(lower, upper);
111}
112
115{
117 {
118 handle_constant_binary_expression(other, ID_minus);
119 }
120
121 // [this.lower - other.upper, this.upper - other.lower]
122 return plus(other.unary_minus());
123}
124
127{
129 {
131 }
132
133 return get_extremes(*this, o, ID_mult);
134}
135
138{
140 {
142 }
143
144 // If other might be division by zero, set everything to top.
145 if(o.contains_zero())
146 {
147 return top();
148 }
149
150 return get_extremes(*this, o, ID_div);
151}
152
155{
156 // SEE https://stackoverflow.com/questions/11720656/modulo-operation-with-negative-numbers
157
159 {
161 }
162
163 if(o.is_bottom())
164 {
165 return top();
166 }
167
168 // If the RHS is 1, or -1 (signed only), then return zero.
169 if(
171 (o.is_signed() && o == constant_interval_exprt(from_integer(-1, o.type()))))
172 {
174 }
175
176 // If other might be modulo by zero, set everything to top.
177 if(o.contains_zero())
178 {
179 return top();
180 }
181
182 if(is_zero())
183 {
185 }
186
187 exprt lower = min();
188 exprt upper = max();
189
190 // Positive case (cannot have zero on RHS).
191 // 10 % 5 = [0, 4], 3 % 5 = [0, 3]
192 if(!is_negative() && o.is_positive())
193 {
194 lower = zero();
195 upper = get_min(get_upper(), o.decrement().get_upper());
196 }
197
198 // [-5, 5] % [3]
200 {
201 INVARIANT(
203 "Zero should be between a negative and a positive value");
204 // This can be done more accurately.
205 lower = get_min(o.get_lower(), get_lower());
206 upper = get_max(o.get_upper(), get_upper());
207 }
208
209 if(is_negative() && o.is_negative())
210 {
211 lower = get_min(o.get_lower(), o.get_lower());
212 upper = zero();
213 }
214
215 return constant_interval_exprt(lower, upper);
216}
217
219{
220 // tvt not
221 return !is_definitely_false();
222}
223
225{
226 if(type().id() == ID_bool)
227 {
229 {
230 return tvt(get_lower() == false_exprt());
231 }
232 else
233 {
234 return tvt::unknown();
235 }
236 }
237
239 {
240 return tvt(true);
241 }
242
244 {
245 INVARIANT(
247 "If an interval contains zero its lower bound can't be positive"
248 " and its upper bound can't be negative");
249 return tvt::unknown();
250 }
251
252 return tvt(false);
253}
254
256{
257 PRECONDITION(type().id() == ID_bool);
258 PRECONDITION(o.type().id() == ID_bool);
259
261 tvt b = o.is_definitely_true();
262
263 return (a || b);
264}
265
267{
268 PRECONDITION(type().id() == ID_bool);
269 PRECONDITION(o.type().id() == ID_bool);
270
271 return (is_definitely_true() && o.is_definitely_true());
272}
273
275{
276 PRECONDITION(type().id() == ID_bool);
277 PRECONDITION(o.type().id() == ID_bool);
278
279 return (
282}
283
285{
286 PRECONDITION(type().id() == ID_bool);
287
289 {
290 return tvt(false);
291 }
292
294 {
295 return tvt(true);
296 }
297
298 return tvt::unknown();
299}
300
303{
305 {
306 return handle_constant_binary_expression(o, ID_shl);
307 }
308
309 if(is_negative(o.get_lower()))
310 {
311 return top();
312 }
313
314 return get_extremes(*this, o, ID_shl);
315}
316
317// Arithmetic
320{
322 {
323 return handle_constant_binary_expression(o, ID_ashr);
324 }
325
326 if(is_negative(o.get_lower()))
327 {
328 return top();
329 }
330
331 return get_extremes(*this, o, ID_ashr);
332}
333
336{
338 {
339 return handle_constant_binary_expression(o, ID_bitxor);
340 }
341
342 return top();
343}
344
347{
349 {
350 return handle_constant_binary_expression(o, ID_bitor);
351 }
352
353 return top();
354}
355
358{
360 {
361 return handle_constant_binary_expression(o, ID_bitand);
362 }
363
364 return top();
365}
366
368{
370 {
371 return handle_constant_unary_expression(ID_bitnot);
372 }
373
374 return top();
375}
376
378{
379 // [get_lower, get_upper] < [o.get_lower(), o.get_upper()]
381 {
382 return tvt(less_than(get_lower(), o.get_lower()));
383 }
384
385 if(less_than(get_upper(), o.get_lower()))
386 {
387 return tvt(true);
388 }
389
391 {
392 return tvt(false);
393 }
394
395 return tvt::unknown();
396}
397
399 const constant_interval_exprt &o) const
400{
401 return o.less_than(*this);
402}
403
405 const constant_interval_exprt &o) const
406{
408 {
410 }
411
412 // [get_lower, get_upper] <= [o.get_lower(), o.get_upper()]
414 {
415 return tvt(true);
416 }
417
419 {
420 return tvt(false);
421 }
422
423 return tvt::unknown();
424}
425
427 const constant_interval_exprt &o) const
428{
429 return o.less_than_or_equal(*this);
430}
431
433{
435 {
436 return tvt(equal(get_lower(), o.get_lower()));
437 }
438
439 if(equal(get_upper(), o.get_upper()) && equal(get_lower(), o.get_lower()))
440 {
441 return tvt(true);
442 }
443
444 if(
445 less_than(o).is_true() || greater_than(o).is_true() ||
446 o.less_than(*this).is_true() || o.greater_than(*this).is_true())
447 {
448 return tvt(false);
449 }
450
451 // Don't know. Could have [3, 5] == [4] (not equal)
452 return tvt::unknown();
453}
454
456{
457 return !equal(o);
458}
459
461{
463}
464
466{
468}
469
473 const irep_idt &operation)
474{
475 std::vector<exprt> results;
476
477 generate_expression(a.get_lower(), b.get_lower(), operation, results);
478 generate_expression(a.get_lower(), b.get_upper(), operation, results);
479 generate_expression(a.get_upper(), b.get_lower(), operation, results);
480 generate_expression(a.get_upper(), b.get_upper(), operation, results);
481
482 for(auto result : results)
483 {
484 if(!is_extreme(result) && contains_extreme(result))
485 {
486 return constant_interval_exprt(result.type());
487 }
488 }
489
490 exprt min = get_min(results);
491 exprt max = get_max(results);
492
493 return simplified_interval(min, max);
494}
495
497 std::vector<exprt> values,
498 bool min_value)
499{
500 symbol_tablet symbol_table;
501 namespacet ns(symbol_table); // Empty
502
503 if(values.size() == 0)
504 {
505 return nil_exprt();
506 }
507
508 if(values.size() == 1)
509 {
510 return *(values.begin());
511 }
512
513 if(values.size() == 2)
514 {
515 if(min_value)
516 {
517 return get_min(values.front(), values.back());
518 }
519 else
520 {
521 return get_max(values.front(), values.back());
522 }
523 }
524
525 typet type = values.begin()->type();
526
527 for(auto v : values)
528 {
529 if((min_value && is_min(v)) || (!min_value && is_max(v)))
530 {
531 return v;
532 }
533 }
534
535 for(auto left : values)
536 {
537 bool all_left_OP_right = true;
538
539 for(auto right : values)
540 {
541 if(
542 (min_value && less_than_or_equal(left, right)) ||
543 (!min_value && greater_than_or_equal(left, right)))
544 {
545 continue;
546 }
547
548 all_left_OP_right = false;
549 break;
550 }
551
552 if(all_left_OP_right)
553 {
554 return left;
555 }
556 }
557
558 /* Return top */
559 if(min_value)
560 {
561 return min_exprt(type);
562 }
563 else
564 {
565 return max_exprt(type);
566 }
567
569}
570
572 const exprt &lhs,
573 const exprt &rhs,
574 const irep_idt &operation,
575 std::vector<exprt> &collection)
576{
577 if(operation == ID_mult)
578 {
579 append_multiply_expression(lhs, rhs, collection);
580 }
581 else if(operation == ID_div)
582 {
583 collection.push_back(generate_division_expression(lhs, rhs));
584 }
585 else if(operation == ID_mod)
586 {
587 collection.push_back(generate_modulo_expression(lhs, rhs));
588 }
589 else if(operation == ID_shl || operation == ID_ashr)
590 {
591 collection.push_back(generate_shift_expression(lhs, rhs, operation));
592 }
593}
594
601 const exprt &lower,
602 const exprt &upper,
603 std::vector<exprt> &collection)
604{
605 PRECONDITION(lower.type().is_not_nil() && is_numeric(lower.type()));
606
607 if(is_max(lower))
608 {
609 append_multiply_expression_max(upper, collection);
610 }
611 else if(is_max(upper))
612 {
613 append_multiply_expression_max(lower, collection);
614 }
615 else if(is_min(lower))
616 {
617 append_multiply_expression_min(lower, upper, collection);
618 }
619 else if(is_min(upper))
620 {
621 append_multiply_expression_min(upper, lower, collection);
622 }
623 else
624 {
625 INVARIANT(
626 !is_extreme(lower) && !is_extreme(upper),
627 "We ruled out extreme cases beforehand");
628
629 auto result = mult_exprt(lower, upper);
630 collection.push_back(simplified_expr(result));
631 }
632}
633
639 const exprt &expr,
640 std::vector<exprt> &collection)
641{
642 if(is_min(expr))
643 {
644 INVARIANT(!is_positive(expr), "Min value cannot be >0.");
645 INVARIANT(
646 is_negative(expr) || is_zero(expr), "Non-negative MIN must be zero.");
647 }
648
649 if(is_zero(expr))
650 collection.push_back(expr);
651 else
652 {
653 collection.push_back(max_exprt(expr));
654 collection.push_back(min_exprt(expr));
655 }
656}
657
664 const exprt &min,
665 const exprt &other,
666 std::vector<exprt> &collection)
667{
669 INVARIANT(!is_positive(min), "Min value cannot be >0.");
670 INVARIANT(is_negative(min) || is_zero(min), "Non-negative MIN must be zero.");
671
672 if(is_zero(min))
673 collection.push_back(min);
674 else if(is_zero(other))
675 collection.push_back(other);
676 else
677 {
678 collection.push_back(min_exprt(min));
679 collection.push_back(max_exprt(min));
680 }
681}
682
684 const exprt &lhs,
685 const exprt &rhs)
686{
688
690
691 if(rhs.is_one())
692 {
693 return lhs;
694 }
695
696 if(is_max(lhs))
697 {
698 if(is_negative(rhs))
699 {
700 return min_exprt(lhs);
701 }
702
703 return lhs;
704 }
705
706 if(is_min(lhs))
707 {
708 if(is_negative(rhs))
709 {
710 return max_exprt(lhs);
711 }
712
713 return lhs;
714 }
715
716 INVARIANT(!is_extreme(lhs), "We ruled out extreme cases beforehand");
717
718 if(is_max(rhs))
719 {
720 return zero(rhs);
721 }
722
723 if(is_min(rhs))
724 {
725 INVARIANT(
726 is_signed(rhs), "We think this is a signed integer for some reason?");
727 return zero(rhs);
728 }
729
730 INVARIANT(
732 "We ruled out extreme cases beforehand");
733
734 auto div_expr = div_exprt(lhs, rhs);
735 return simplified_expr(div_expr);
736}
737
739 const exprt &lhs,
740 const exprt &rhs)
741{
743
745
746 if(rhs.is_one())
747 {
748 return lhs;
749 }
750
751 if(is_max(lhs))
752 {
753 if(is_negative(rhs))
754 {
755 return min_exprt(lhs);
756 }
757
758 return lhs;
759 }
760
761 if(is_min(lhs))
762 {
763 if(is_negative(rhs))
764 {
765 return max_exprt(lhs);
766 }
767
768 return lhs;
769 }
770
771 INVARIANT(!is_extreme(lhs), "We rule out this case beforehand");
772
773 if(is_max(rhs))
774 {
775 return zero(rhs);
776 }
777
778 if(is_min(rhs))
779 {
780 INVARIANT(is_signed(rhs), "We assume this is signed for some reason?");
781 return zero(rhs);
782 }
783
784 INVARIANT(
786 "We ruled out extreme values beforehand");
787
788 auto modulo_expr = mod_exprt(lhs, rhs);
789 return simplified_expr(modulo_expr);
790}
791
793{
794 if(id == ID_unary_plus)
795 {
796 return unary_plus();
797 }
798 if(id == ID_unary_minus)
799 {
800 return unary_minus();
801 }
802 if(id == ID_bitnot)
803 {
804 return bitwise_not();
805 }
806 if(id == ID_not)
807 {
809 }
810
811 return top();
812}
813
815 const irep_idt &binary_operator,
816 const constant_interval_exprt &other) const
817{
818 if(binary_operator == ID_plus)
819 {
820 return plus(other);
821 }
822 if(binary_operator == ID_minus)
823 {
824 return minus(other);
825 }
826 if(binary_operator == ID_mult)
827 {
828 return multiply(other);
829 }
830 if(binary_operator == ID_div)
831 {
832 return divide(other);
833 }
834 if(binary_operator == ID_mod)
835 {
836 return modulo(other);
837 }
838 if(binary_operator == ID_shl)
839 {
840 return left_shift(other);
841 }
842 if(binary_operator == ID_ashr)
843 {
844 return right_shift(other);
845 }
846 if(binary_operator == ID_bitor)
847 {
848 return bitwise_or(other);
849 }
850 if(binary_operator == ID_bitand)
851 {
852 return bitwise_and(other);
853 }
854 if(binary_operator == ID_bitxor)
855 {
856 return bitwise_xor(other);
857 }
858 if(binary_operator == ID_lt)
859 {
860 return tvt_to_interval(less_than(other));
861 }
862 if(binary_operator == ID_le)
863 {
864 return tvt_to_interval(less_than_or_equal(other));
865 }
866 if(binary_operator == ID_gt)
867 {
868 return tvt_to_interval(greater_than(other));
869 }
870 if(binary_operator == ID_ge)
871 {
873 }
874 if(binary_operator == ID_equal)
875 {
876 return tvt_to_interval(equal(other));
877 }
878 if(binary_operator == ID_notequal)
879 {
880 return tvt_to_interval(not_equal(other));
881 }
882 if(binary_operator == ID_and)
883 {
884 return tvt_to_interval(logical_and(other));
885 }
886 if(binary_operator == ID_or)
887 {
888 return tvt_to_interval(logical_or(other));
889 }
890 if(binary_operator == ID_xor)
891 {
892 return tvt_to_interval(logical_xor(other));
893 }
894
895 return top();
896}
897
899 const exprt &lhs,
900 const exprt &rhs,
901 const irep_idt &operation)
902{
903 PRECONDITION(operation == ID_shl || operation == ID_ashr);
904
905 if(is_zero(lhs) || is_zero(rhs))
906 {
907 // Shifting zero does nothing.
908 // Shifting BY zero also does nothing.
909 return lhs;
910 }
911
912 INVARIANT(!is_negative(rhs), "Should be caught at an earlier stage.");
913
914 if(is_max(lhs))
915 {
916 return lhs;
917 }
918
919 if(is_min(lhs))
920 {
921 return lhs;
922 }
923
924 if(is_max(rhs))
925 {
926 return min_exprt(rhs);
927 }
928
929 INVARIANT(
931 "We ruled out extreme cases beforehand");
932
933 auto shift_expr = shift_exprt(lhs, operation, rhs);
934 return simplified_expr(shift_expr);
935}
936
939 const irep_idt &op) const
940{
942 {
943 auto expr = unary_exprt(op, get_lower());
945 }
946 return top();
947}
948
951 const constant_interval_exprt &other,
952 const irep_idt &op) const
953{
955 auto expr = binary_exprt(get_lower(), op, other.get_lower());
957}
958
960{
961 return greater_than(a, b) ? a : b;
962}
963
965{
966 return less_than(a, b) ? a : b;
967}
968
969exprt constant_interval_exprt::get_min(std::vector<exprt> &values)
970{
971 return get_extreme(values, true);
972}
973
974exprt constant_interval_exprt::get_max(std::vector<exprt> &values)
975{
976 return get_extreme(values, false);
977}
978
979/* we don't simplify in the constructor otherwise */
982{
984}
985
987{
988 symbol_tablet symbol_table;
989 const namespacet ns(symbol_table);
990
992
993 return simplify_expr(expr, ns);
994}
995
997{
999 INVARIANT(
1000 zero.is_zero() || (type.id() == ID_bool && zero.is_false()),
1001 "The value created from 0 should be zero or false");
1002 return zero;
1003}
1004
1006{
1007 return zero(expr.type());
1008}
1009
1012{
1013 return zero(interval.type());
1014}
1015
1017{
1018 return zero(type());
1019}
1020
1022{
1023 return min_exprt(type());
1024}
1025
1027{
1028 return max_exprt(type());
1029}
1030
1032{
1033 return (has_no_lower_bound() && has_no_upper_bound());
1034}
1035
1037{
1038 // This should ONLY happen for bottom.
1039 return is_min(get_upper()) || is_max(get_lower());
1040}
1041
1043{
1045}
1046
1048{
1050}
1051
1053{
1054 return constant_interval_exprt(type());
1055}
1056
1058{
1059 return bottom(type());
1060}
1061
1062/* Helpers */
1063
1065{
1066 return is_int(type());
1067}
1068
1070{
1071 return is_float(type());
1072}
1073
1075{
1076 return is_int(type) || is_float(type);
1077}
1078
1080{
1081 return is_numeric(type());
1082}
1083
1085{
1086 return is_numeric(expr.type());
1087}
1088
1090 const constant_interval_exprt &interval)
1091{
1092 return interval.is_numeric();
1093}
1094
1096{
1097 return (is_signed(type) || is_unsigned(type));
1098}
1099
1101{
1102 return src.id() == ID_floatbv;
1103}
1104
1106{
1107 return is_int(expr.type());
1108}
1109
1111{
1112 return interval.is_int();
1113}
1114
1116{
1117 return is_float(expr.type());
1118}
1119
1121{
1122 return interval.is_float();
1123}
1124
1126{
1127 return t.id() == ID_bv || t.id() == ID_signedbv || t.id() == ID_unsignedbv ||
1128 t.id() == ID_c_bool ||
1129 (t.id() == ID_c_bit_field &&
1130 is_bitvector(to_c_bit_field_type(t).underlying_type()));
1131}
1132
1134{
1135 return t.id() == ID_signedbv ||
1136 (t.id() == ID_c_bit_field &&
1137 is_signed(to_c_bit_field_type(t).underlying_type()));
1138}
1139
1141{
1142 return t.id() == ID_bv || t.id() == ID_unsignedbv || t.id() == ID_c_bool ||
1143 t.id() == ID_c_enum ||
1144 (t.id() == ID_c_bit_field &&
1145 is_unsigned(to_c_bit_field_type(t).underlying_type()));
1146}
1147
1149{
1150 return is_signed(interval.type());
1151}
1152
1154 const constant_interval_exprt &interval)
1155{
1156 return is_unsigned(interval.type());
1157}
1158
1160 const constant_interval_exprt &interval)
1161{
1162 return is_bitvector(interval.type());
1163}
1164
1166{
1167 return is_signed(expr.type());
1168}
1169
1171{
1172 return is_unsigned(expr.type());
1173}
1174
1176{
1177 return is_bitvector(expr.type());
1178}
1179
1181{
1182 return is_signed(type());
1183}
1184
1186{
1187 return is_unsigned(type());
1188}
1189
1191{
1192 return is_bitvector(type());
1193}
1194
1196{
1197 return (is_max(expr) || is_min(expr));
1198}
1199
1200bool constant_interval_exprt::is_extreme(const exprt &expr1, const exprt &expr2)
1201{
1202 return is_extreme(expr1) || is_extreme(expr2);
1203}
1204
1206{
1207 return is_max(get_upper());
1208}
1209
1211{
1212 return is_min(get_lower());
1213}
1214
1216{
1217 return expr.id() == ID_max;
1218}
1219
1221{
1222 return expr.id() == ID_min;
1223}
1224
1226{
1227 exprt simplified = simplified_expr(expr);
1228
1229 if(expr.is_nil() || !simplified.is_constant() || expr.get(ID_value) == "")
1230 {
1231 return false;
1232 }
1233
1234 if(is_unsigned(expr) || is_max(expr))
1235 {
1236 return true;
1237 }
1238
1239 INVARIANT(is_signed(expr), "Not implemented for floats");
1240 // Floats later
1241
1242 if(is_min(expr))
1243 {
1244 return false;
1245 }
1246
1247 return greater_than(expr, zero(expr));
1248}
1249
1251{
1252 if(is_min(expr))
1253 {
1254 if(is_unsigned(expr))
1255 {
1256 return true;
1257 }
1258 else
1259 {
1260 return false;
1261 }
1262 }
1263
1264 if(is_max(expr))
1265 {
1266 return false;
1267 }
1268
1269 INVARIANT(!is_max(expr) && !is_min(expr), "We excluded those cases");
1270
1271 if(expr.is_zero())
1272 {
1273 return true;
1274 }
1275
1276 return equal(expr, zero(expr));
1277}
1278
1280{
1281 if(is_unsigned(expr) || is_max(expr))
1282 {
1283 return false;
1284 }
1285
1286 INVARIANT(
1287 is_signed(expr), "We don't support anything other than integers yet");
1288
1289 if(is_min(expr))
1290 {
1291 return true;
1292 }
1293
1294 INVARIANT(!is_extreme(expr), "We excluded these cases before");
1295
1296 return less_than(expr, zero(expr));
1297}
1298
1300{
1301 if(is_signed(expr) && is_min(expr))
1302 {
1303 return max_exprt(expr);
1304 }
1305
1306 if(is_max(expr) || is_unsigned(expr) || is_zero(expr) || is_positive(expr))
1307 {
1308 return expr;
1309 }
1310
1311 return simplified_expr(unary_minus_exprt(expr));
1312}
1313
1315{
1316 if(a == b)
1317 {
1318 return true;
1319 }
1320
1321 if(!is_numeric(a) || !is_numeric(b))
1322 {
1323 INVARIANT(
1324 !(a == b),
1325 "Best we can do now is a==b?, but this is covered by the above, so "
1326 "always false");
1327 return false;
1328 }
1329
1330 if(is_max(a) && is_max(b))
1331 {
1332 return true;
1333 }
1334
1335 exprt l = (is_min(a) && is_unsigned(a)) ? zero(a) : a;
1336 exprt r = (is_min(b) && is_unsigned(b)) ? zero(b) : b;
1337
1338 // CANNOT use is_zero(X) but can use X.is_zero();
1339 if((is_min(l) && is_min(r)))
1340 {
1341 return true;
1342 }
1343
1344 if(
1345 (is_max(l) && !is_max(r)) || (is_min(l) && !is_min(r)) ||
1346 (is_max(r) && !is_max(l)) || (is_min(r) && !is_min(l)))
1347 {
1348 return false;
1349 }
1350
1351 INVARIANT(!is_extreme(l, r), "We've excluded this before");
1352
1353 return simplified_expr(equal_exprt(l, r)).is_true();
1354}
1355
1356// TODO: Signed/unsigned comparisons.
1358{
1359 if(!is_numeric(a) || !is_numeric(b))
1360 {
1361 return false;
1362 }
1363
1364 exprt l = (is_min(a) && is_unsigned(a)) ? zero(a) : a;
1365 exprt r = (is_min(b) && is_unsigned(b)) ? zero(b) : b;
1366
1367 if(is_max(l))
1368 {
1369 return false;
1370 }
1371
1372 INVARIANT(!is_max(l), "We've just excluded this case");
1373
1374 if(is_min(r))
1375 {
1376 // Can't be smaller than min.
1377 return false;
1378 }
1379
1380 INVARIANT(!is_max(l) && !is_min(r), "We've excluded these cases");
1381
1382 if(is_min(l))
1383 {
1384 return true;
1385 }
1386
1387 INVARIANT(
1388 !is_max(l) && !is_min(r) && !is_min(l),
1389 "These cases should have all been handled before this point");
1390
1391 if(is_max(r))
1392 {
1393 // If r is max, then l is less, unless l is max.
1394 return !is_max(l);
1395 }
1396
1397 INVARIANT(
1398 !is_extreme(l) && !is_extreme(r),
1399 "We have excluded all of these cases in the code above");
1400
1401 return simplified_expr(binary_relation_exprt(l, ID_lt, r)).is_true();
1402}
1403
1405{
1406 return less_than(b, a);
1407}
1408
1410{
1411 return less_than(a, b) || equal(a, b);
1412}
1413
1415 const exprt &a,
1416 const exprt &b)
1417{
1418 return greater_than(a, b) || equal(a, b);
1419}
1420
1422{
1423 return !equal(a, b);
1424}
1425
1427 const constant_interval_exprt &interval) const
1428{
1429 // [a, b] Contains [c, d] If c >= a and d <= b.
1430 return (
1431 less_than_or_equal(interval.get_upper(), get_upper()) &&
1433}
1434
1436{
1437 std::stringstream out;
1438 out << *this;
1439 return out.str();
1440}
1441
1442std::ostream &operator<<(std::ostream &out, const constant_interval_exprt &i)
1443{
1444 out << "[";
1445
1446 if(!i.has_no_lower_bound())
1447 {
1448 // FIXME Not everything that's a bitvector is also an integer
1449 if(i.is_bitvector(i.get_lower()))
1450 {
1451 out << integer2string(*numeric_cast<mp_integer>(i.get_lower()));
1452 }
1453 else
1454 {
1455 // TODO handle floating point numbers?
1456 out << i.get_lower().get(ID_value);
1457 }
1458 }
1459 else
1460 {
1461 if(i.is_signed(i.get_lower()))
1462 {
1463 out << "MIN";
1464 }
1465 else
1466 {
1467 // FIXME Extremely sketchy, the opposite of
1468 // FIXME "signed" isn't "unsigned" but
1469 // FIXME "literally anything else"
1470 out << "0";
1471 }
1472 }
1473
1474 out << ",";
1475
1476 // FIXME See comments on is_min
1477 if(!i.has_no_upper_bound())
1478 {
1479 if(i.is_bitvector(i.get_upper()))
1480 {
1481 out << integer2string(*numeric_cast<mp_integer>(i.get_upper()));
1482 }
1483 else
1484 {
1485 out << i.get_upper().get(ID_value);
1486 }
1487 }
1488 else
1489 out << "MAX";
1490
1491 out << "]";
1492
1493 return out;
1494}
1495
1497 const constant_interval_exprt &lhs,
1498 const constant_interval_exprt &rhs)
1499{
1500 return lhs.less_than(rhs).is_true();
1501}
1502
1504 const constant_interval_exprt &lhs,
1505 const constant_interval_exprt &rhs)
1506{
1507 return lhs.greater_than(rhs).is_true();
1508}
1509
1511 const constant_interval_exprt &lhs,
1512 const constant_interval_exprt &rhs)
1513{
1514 return lhs.less_than_or_equal(rhs).is_true();
1515}
1516
1518 const constant_interval_exprt &lhs,
1519 const constant_interval_exprt &rhs)
1520{
1521 return lhs.greater_than(rhs).is_true();
1522}
1523
1525 const constant_interval_exprt &lhs,
1526 const constant_interval_exprt &rhs)
1527{
1528 return lhs.equal(rhs).is_true();
1529}
1530
1532 const constant_interval_exprt &lhs,
1533 const constant_interval_exprt &rhs)
1534{
1535 return lhs.not_equal(rhs).is_true();
1536}
1537
1539 const constant_interval_exprt &lhs,
1540 const constant_interval_exprt &rhs)
1541{
1542 return lhs.unary_plus(rhs);
1543}
1544
1546 const constant_interval_exprt &lhs,
1547 const constant_interval_exprt &rhs)
1548{
1549 return lhs.minus(rhs);
1550}
1551
1553 const constant_interval_exprt &lhs,
1554 const constant_interval_exprt &rhs)
1555{
1556 return lhs.divide(rhs);
1557}
1558
1560 const constant_interval_exprt &lhs,
1561 const constant_interval_exprt &rhs)
1562{
1563 return lhs.multiply(rhs);
1564}
1565
1567 const constant_interval_exprt &lhs,
1568 const constant_interval_exprt &rhs)
1569{
1570 return lhs.modulo(rhs);
1571}
1572
1574 const constant_interval_exprt &lhs,
1575 const constant_interval_exprt &rhs)
1576{
1577 return lhs.bitwise_and(rhs);
1578}
1579
1581 const constant_interval_exprt &lhs,
1582 const constant_interval_exprt &rhs)
1583{
1584 return lhs.bitwise_or(rhs);
1585}
1586
1588 const constant_interval_exprt &lhs,
1589 const constant_interval_exprt &rhs)
1590{
1591 return lhs.bitwise_xor(rhs);
1592}
1593
1595{
1596 return lhs.bitwise_not();
1597}
1598
1600 const constant_interval_exprt &lhs,
1601 const constant_interval_exprt &rhs)
1602{
1603 return lhs.left_shift(rhs);
1604}
1605
1607 const constant_interval_exprt &lhs,
1608 const constant_interval_exprt &rhs)
1609{
1610 return lhs.right_shift(rhs);
1611}
1612
1615{
1616 return a.unary_plus();
1617}
1618
1621{
1622 return a.unary_minus();
1623}
1624
1627{
1628 if(this->type().id() == ID_bool && is_int(type))
1629 {
1630 bool lower = !has_no_lower_bound() && get_lower().is_true();
1631 bool upper = has_no_upper_bound() || get_upper().is_true();
1632
1633 INVARIANT(!lower || upper, "");
1634
1635 constant_exprt lower_num = from_integer(lower, type);
1636 constant_exprt upper_num = from_integer(upper, type);
1637
1638 return constant_interval_exprt(lower_num, upper_num, type);
1639 }
1640 else
1641 {
1642 auto do_typecast = [&type](exprt e) {
1643 if(e.id() == ID_min || e.id() == ID_max)
1644 {
1645 e.type() = type;
1646 }
1647 else
1648 {
1650 }
1651 return e;
1652 };
1653
1654 exprt lower = do_typecast(get_lower());
1655 POSTCONDITION(lower.id() == get_lower().id());
1656
1657 exprt upper = do_typecast(get_upper());
1658 POSTCONDITION(upper.id() == get_upper().id());
1659
1660 return constant_interval_exprt(lower, upper, type);
1661 }
1662}
1663
1664/* Binary */
1666 const constant_interval_exprt &a,
1667 const constant_interval_exprt &b)
1668{
1669 return a.plus(b);
1670}
1671
1673 const constant_interval_exprt &a,
1674 const constant_interval_exprt &b)
1675{
1676 return a.minus(b);
1677}
1678
1680 const constant_interval_exprt &a,
1681 const constant_interval_exprt &b)
1682{
1683 return a.multiply(b);
1684}
1685
1687 const constant_interval_exprt &a,
1688 const constant_interval_exprt &b)
1689{
1690 return a.divide(b);
1691}
1692
1694 const constant_interval_exprt &a,
1695 const constant_interval_exprt &b)
1696{
1697 return a.modulo(b);
1698}
1699
1700/* Binary shifts */
1702 const constant_interval_exprt &a,
1703 const constant_interval_exprt &b)
1704{
1705 return a.left_shift(b);
1706}
1707
1709 const constant_interval_exprt &a,
1710 const constant_interval_exprt &b)
1711{
1712 return a.right_shift(b);
1713}
1714
1715/* Unary bitwise */
1718{
1719 return a.bitwise_not();
1720}
1721
1722/* Binary bitwise */
1724 const constant_interval_exprt &a,
1725 const constant_interval_exprt &b)
1726{
1727 return a.bitwise_xor(b);
1728}
1729
1731 const constant_interval_exprt &a,
1732 const constant_interval_exprt &b)
1733{
1734 return a.bitwise_or(b);
1735}
1736
1738 const constant_interval_exprt &a,
1739 const constant_interval_exprt &b)
1740{
1741 return a.bitwise_and(b);
1742}
1743
1745 const constant_interval_exprt &a,
1746 const constant_interval_exprt &b)
1747{
1748 return a.less_than(b);
1749}
1750
1752 const constant_interval_exprt &a,
1753 const constant_interval_exprt &b)
1754{
1755 return a.greater_than(b);
1756}
1757
1759 const constant_interval_exprt &a,
1760 const constant_interval_exprt &b)
1761{
1762 return a.less_than_or_equal(b);
1763}
1764
1766 const constant_interval_exprt &a,
1767 const constant_interval_exprt &b)
1768{
1769 return a.greater_than_or_equal(b);
1770}
1771
1773 const constant_interval_exprt &a,
1774 const constant_interval_exprt &b)
1775{
1776 return a.equal(b);
1777}
1778
1780 const constant_interval_exprt &a,
1781 const constant_interval_exprt &b)
1782{
1783 return a.equal(b);
1784}
1785
1788{
1789 return a.increment();
1790}
1791
1794{
1795 return a.decrement();
1796}
1797
1799{
1800 return a.is_empty();
1801}
1802
1804 const constant_interval_exprt &a)
1805{
1806 return a.is_single_value_interval();
1807}
1808
1810{
1811 return a.is_top();
1812}
1813
1815{
1816 return a.is_bottom();
1817}
1818
1820{
1821 return a.has_no_lower_bound();
1822}
1823
1825{
1826 return a.has_no_upper_bound();
1827}
1828
1830{
1831 forall_operands(it, expr)
1832 {
1833 if(is_extreme(*it))
1834 {
1835 return true;
1836 }
1837
1838 if(it->has_operands())
1839 {
1840 return contains_extreme(*it);
1841 }
1842 }
1843
1844 return false;
1845}
1846
1848 const exprt expr1,
1849 const exprt expr2)
1850{
1851 return contains_extreme(expr1) || contains_extreme(expr2);
1852}
1853
1855{
1857 {
1858 return false;
1859 }
1860
1861 return true;
1862}
1863
1865{
1866 return !is_extreme(get_lower()) && !is_extreme(get_upper()) &&
1868}
1869
1871{
1872 if(!is_numeric())
1873 {
1874 return false;
1875 }
1876
1877 if(get_lower().is_zero() || get_upper().is_zero())
1878 {
1879 return true;
1880 }
1881
1882 if(is_unsigned() && is_min(get_lower()))
1883 {
1884 return true;
1885 }
1886
1887 if(
1890 {
1891 return true;
1892 }
1893
1894 return false;
1895}
1896
1898 const constant_interval_exprt &interval)
1899{
1900 return interval.is_positive();
1901}
1902
1904{
1905 return interval.is_zero();
1906}
1907
1909 const constant_interval_exprt &interval)
1910{
1911 return interval.is_negative();
1912}
1913
1915{
1917}
1918
1920{
1921 return is_zero(get_lower()) && is_zero(get_upper());
1922}
1923
1925{
1927}
1928
1930{
1931 return a.is_definitely_true();
1932}
1933
1935{
1936 return a.is_definitely_false();
1937}
1938
1940 const constant_interval_exprt &a,
1941 const constant_interval_exprt &b)
1942{
1943 return a.logical_and(b);
1944}
1945
1947 const constant_interval_exprt &a,
1948 const constant_interval_exprt &b)
1949{
1950 return a.logical_or(b);
1951}
1952
1954 const constant_interval_exprt &a,
1955 const constant_interval_exprt &b)
1956{
1957 return a.logical_xor(b);
1958}
1959
1961{
1962 return a.logical_not();
1963}
1964
1966{
1967 if(val.is_true())
1968 {
1970 }
1971 else if(val.is_false())
1972 {
1974 }
1975 else
1976 {
1978 }
1979}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
API to expression classes for bitvectors.
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
Definition: c_types.h:58
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 base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:674
The Boolean type.
Definition: std_types.h:36
A constant literal expression.
Definition: std_expr.h:2807
Represents an interval of values.
Definition: interval.h:48
static constant_interval_exprt get_extremes(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs, const irep_idt &operation)
Definition: interval.cpp:470
bool is_negative() const
Definition: interval.cpp:1924
static exprt generate_division_expression(const exprt &lhs, const exprt &rhs)
Definition: interval.cpp:683
static bool is_bottom(const constant_interval_exprt &a)
Definition: interval.cpp:1814
constant_interval_exprt bottom() const
Definition: interval.cpp:1057
constant_interval_exprt minus(const constant_interval_exprt &other) const
Definition: interval.cpp:114
tvt greater_than_or_equal(const constant_interval_exprt &o) const
Definition: interval.cpp:426
bool is_signed() const
Definition: interval.cpp:1180
tvt greater_than(const constant_interval_exprt &o) const
Definition: interval.cpp:398
constant_interval_exprt bitwise_or(const constant_interval_exprt &o) const
Definition: interval.cpp:346
constant_interval_exprt decrement() const
Definition: interval.cpp:465
tvt less_than_or_equal(const constant_interval_exprt &o) const
Definition: interval.cpp:404
tvt is_definitely_false() const
Definition: interval.cpp:224
constant_interval_exprt left_shift(const constant_interval_exprt &o) const
Definition: interval.cpp:302
tvt not_equal(const constant_interval_exprt &o) const
Definition: interval.cpp:455
static exprt generate_shift_expression(const exprt &lhs, const exprt &rhs, const irep_idt &operation)
Definition: interval.cpp:898
bool has_no_upper_bound() const
Definition: interval.cpp:1205
bool is_bottom() const
Definition: interval.cpp:1036
static bool is_top(const constant_interval_exprt &a)
Definition: interval.cpp:1809
constant_interval_exprt typecast(const typet &type) const
Definition: interval.cpp:1626
constant_interval_exprt multiply(const constant_interval_exprt &o) const
Definition: interval.cpp:126
static constant_interval_exprt tvt_to_interval(const tvt &val)
Definition: interval.cpp:1965
constant_interval_exprt unary_plus() const
Definition: interval.cpp:39
constant_interval_exprt plus(const constant_interval_exprt &o) const
Definition: interval.cpp:76
static exprt get_extreme(std::vector< exprt > values, bool min=true)
Definition: interval.cpp:496
bool is_numeric() const
Definition: interval.cpp:1079
static void append_multiply_expression(const exprt &lower, const exprt &upper, std::vector< exprt > &collection)
Adds all possible values that may arise from multiplication (more than one, in case of past the type ...
Definition: interval.cpp:600
constant_interval_exprt bitwise_xor(const constant_interval_exprt &o) const
Definition: interval.cpp:335
bool is_positive() const
Definition: interval.cpp:1914
bool is_single_value_interval() const
Definition: interval.cpp:1864
constant_interval_exprt increment() const
Definition: interval.cpp:460
bool is_bitvector() const
Definition: interval.cpp:1190
std::string to_string() const
Definition: interval.cpp:1435
bool contains(const constant_interval_exprt &interval) const
Definition: interval.cpp:1426
static bool is_extreme(const exprt &expr)
Definition: interval.cpp:1195
tvt logical_or(const constant_interval_exprt &o) const
Definition: interval.cpp:255
static exprt simplified_expr(exprt expr)
Definition: interval.cpp:986
bool contains_zero() const
Definition: interval.cpp:1870
constant_interval_exprt handle_constant_unary_expression(const irep_idt &op) const
SET OF ARITHMETIC OPERATORS.
Definition: interval.cpp:938
constant_interval_exprt modulo(const constant_interval_exprt &o) const
Definition: interval.cpp:154
static exprt get_max(const exprt &a, const exprt &b)
Definition: interval.cpp:959
bool has_no_lower_bound() const
Definition: interval.cpp:1210
static exprt get_min(const exprt &a, const exprt &b)
Definition: interval.cpp:964
static bool is_max(const constant_interval_exprt &a)
Definition: interval.cpp:1824
static void generate_expression(const exprt &lhs, const exprt &rhs, const irep_idt &operation, std::vector< exprt > &collection)
Definition: interval.cpp:571
constant_interval_exprt eval(const irep_idt &unary_operator) const
Definition: interval.cpp:792
tvt is_definitely_true() const
Definition: interval.cpp:218
bool is_unsigned() const
Definition: interval.cpp:1185
min_exprt min() const
Definition: interval.cpp:1021
max_exprt max() const
Definition: interval.cpp:1026
static bool is_min(const constant_interval_exprt &a)
Definition: interval.cpp:1819
static exprt generate_modulo_expression(const exprt &lhs, const exprt &rhs)
Definition: interval.cpp:738
tvt logical_xor(const constant_interval_exprt &o) const
Definition: interval.cpp:274
const exprt & get_lower() const
Definition: interval.cpp:29
static void append_multiply_expression_min(const exprt &min, const exprt &other, std::vector< exprt > &collection)
Appends interval bounds that could arise from MIN * other.
Definition: interval.cpp:663
constant_interval_exprt right_shift(const constant_interval_exprt &o) const
Definition: interval.cpp:319
tvt logical_and(const constant_interval_exprt &o) const
Definition: interval.cpp:266
static void append_multiply_expression_max(const exprt &expr, std::vector< exprt > &collection)
Appends interval bounds that could arise from MAX * expr.
Definition: interval.cpp:638
constant_interval_exprt bitwise_and(const constant_interval_exprt &o) const
Definition: interval.cpp:357
constant_interval_exprt top() const
Definition: interval.cpp:1052
static bool contains_extreme(const exprt expr)
Definition: interval.cpp:1829
constant_interval_exprt unary_minus() const
Definition: interval.cpp:44
constant_exprt zero() const
Definition: interval.cpp:1016
tvt less_than(const constant_interval_exprt &o) const
Definition: interval.cpp:377
static exprt abs(const exprt &expr)
Definition: interval.cpp:1299
constant_interval_exprt bitwise_not() const
Definition: interval.cpp:367
constant_interval_exprt divide(const constant_interval_exprt &o) const
Definition: interval.cpp:137
static constant_interval_exprt simplified_interval(exprt &l, exprt &r)
Definition: interval.cpp:981
constant_interval_exprt handle_constant_binary_expression(const constant_interval_exprt &other, const irep_idt &) const
Definition: interval.cpp:950
tvt logical_not() const
Definition: interval.cpp:284
const exprt & get_upper() const
Definition: interval.cpp:34
tvt equal(const constant_interval_exprt &o) const
Definition: interval.cpp:432
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
bool is_one() const
Return whether the expression is a constant representing 1.
Definition: expr.cpp:114
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:33
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:42
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:64
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:26
typet & type()
Return the type of the expression.
Definition: expr.h:82
The Boolean constant false.
Definition: std_expr.h:2865
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:45
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
+∞ upper bound for intervals
Definition: interval.h:18
-∞ upper bound for intervals
Definition: interval.h:31
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
Definition: std_expr.h:1135
Binary multiplication Associativity is not specified.
Definition: std_expr.h:1019
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
The NIL expression.
Definition: std_expr.h:2874
The plus expression Associativity is not specified.
Definition: std_expr.h:914
A base class for shift and rotate operators.
The symbol table.
Definition: symbol_table.h:14
The Boolean constant true.
Definition: std_expr.h:2856
Definition: threeval.h:20
bool is_false() const
Definition: threeval.h:26
bool is_true() const
Definition: threeval.h:25
static tvt unknown()
Definition: threeval.h:33
Semantic type conversion.
Definition: std_expr.h:1920
The type of an expression, extends irept.
Definition: type.h:29
Generic base class for unary expressions.
Definition: std_expr.h:281
The unary minus expression.
Definition: std_expr.h:390
#define forall_operands(it, expr)
Definition: expr.h:18
const constant_interval_exprt operator/(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1552
bool operator<=(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1510
const constant_interval_exprt operator%(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1566
const constant_interval_exprt operator>>(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1606
bool operator==(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1524
bool operator<(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1496
std::ostream & operator<<(std::ostream &out, const constant_interval_exprt &i)
Definition: interval.cpp:1442
const constant_interval_exprt operator&(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1573
bool operator>(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1503
const constant_interval_exprt operator+(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1538
bool operator!=(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1531
const constant_interval_exprt operator-(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1545
const constant_interval_exprt operator*(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1559
const constant_interval_exprt operator^(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1587
const constant_interval_exprt operator|(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1580
bool operator>=(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
Definition: interval.cpp:1517
const constant_interval_exprt operator!(const constant_interval_exprt &lhs)
Definition: interval.cpp:1594
static int8_t r
Definition: irep_hash.h:60
exprt simplify_expr(exprt src, const namespacet &ns)
BigInt mp_integer
Definition: smt_terms.h:12
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
#define POSTCONDITION(CONDITION)
Definition: invariant.h:479
API to expression classes.
Author: Diffblue Ltd.