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