CBMC
bitvector_expr.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: API to expression classes for bitvectors
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #ifndef CPROVER_UTIL_BITVECTOR_EXPR_H
10 #define CPROVER_UTIL_BITVECTOR_EXPR_H
11 
14 
15 #include "std_expr.h"
16 
18 class bswap_exprt : public unary_exprt
19 {
20 public:
21  bswap_exprt(exprt _op, std::size_t bits_per_byte, typet _type)
22  : unary_exprt(ID_bswap, std::move(_op), std::move(_type))
23  {
24  set_bits_per_byte(bits_per_byte);
25  }
26 
27  bswap_exprt(exprt _op, std::size_t bits_per_byte)
28  : unary_exprt(ID_bswap, std::move(_op))
29  {
30  set_bits_per_byte(bits_per_byte);
31  }
32 
33  std::size_t get_bits_per_byte() const
34  {
35  return get_size_t(ID_bits_per_byte);
36  }
37 
38  void set_bits_per_byte(std::size_t bits_per_byte)
39  {
40  set_size_t(ID_bits_per_byte, bits_per_byte);
41  }
42 };
43 
44 template <>
45 inline bool can_cast_expr<bswap_exprt>(const exprt &base)
46 {
47  return base.id() == ID_bswap;
48 }
49 
50 inline void validate_expr(const bswap_exprt &value)
51 {
52  validate_operands(value, 1, "bswap must have one operand");
54  value.op().type() == value.type(), "bswap type must match operand type");
55 }
56 
63 inline const bswap_exprt &to_bswap_expr(const exprt &expr)
64 {
65  PRECONDITION(expr.id() == ID_bswap);
66  const bswap_exprt &ret = static_cast<const bswap_exprt &>(expr);
67  validate_expr(ret);
68  return ret;
69 }
70 
73 {
74  PRECONDITION(expr.id() == ID_bswap);
75  bswap_exprt &ret = static_cast<bswap_exprt &>(expr);
76  validate_expr(ret);
77  return ret;
78 }
79 
81 class bitnot_exprt : public unary_exprt
82 {
83 public:
84  explicit bitnot_exprt(exprt op) : unary_exprt(ID_bitnot, std::move(op))
85  {
86  }
87 };
88 
89 template <>
90 inline bool can_cast_expr<bitnot_exprt>(const exprt &base)
91 {
92  return base.id() == ID_bitnot;
93 }
94 
95 inline void validate_expr(const bitnot_exprt &value)
96 {
97  validate_operands(value, 1, "Bit-wise not must have one operand");
98 }
99 
106 inline const bitnot_exprt &to_bitnot_expr(const exprt &expr)
107 {
108  PRECONDITION(expr.id() == ID_bitnot);
109  const bitnot_exprt &ret = static_cast<const bitnot_exprt &>(expr);
110  validate_expr(ret);
111  return ret;
112 }
113 
116 {
117  PRECONDITION(expr.id() == ID_bitnot);
118  bitnot_exprt &ret = static_cast<bitnot_exprt &>(expr);
119  validate_expr(ret);
120  return ret;
121 }
122 
125 {
126 public:
127  bitor_exprt(const exprt &_op0, exprt _op1)
128  : multi_ary_exprt(_op0, ID_bitor, std::move(_op1), _op0.type())
129  {
130  }
131 
133  : multi_ary_exprt(ID_bitor, std::move(_operands), std::move(_type))
134  {
135  }
136 };
137 
138 template <>
139 inline bool can_cast_expr<bitor_exprt>(const exprt &base)
140 {
141  return base.id() == ID_bitor;
142 }
143 
150 inline const bitor_exprt &to_bitor_expr(const exprt &expr)
151 {
152  PRECONDITION(expr.id() == ID_bitor);
153  return static_cast<const bitor_exprt &>(expr);
154 }
155 
158 {
159  PRECONDITION(expr.id() == ID_bitor);
160  return static_cast<bitor_exprt &>(expr);
161 }
162 
165 {
166 public:
168  : multi_ary_exprt(std::move(_op0), ID_bitxor, std::move(_op1))
169  {
170  }
171 
173  : multi_ary_exprt(ID_bitxor, std::move(_operands), std::move(_type))
174  {
175  }
176 };
177 
178 template <>
179 inline bool can_cast_expr<bitxor_exprt>(const exprt &base)
180 {
181  return base.id() == ID_bitxor;
182 }
183 
190 inline const bitxor_exprt &to_bitxor_expr(const exprt &expr)
191 {
192  PRECONDITION(expr.id() == ID_bitxor);
193  return static_cast<const bitxor_exprt &>(expr);
194 }
195 
198 {
199  PRECONDITION(expr.id() == ID_bitxor);
200  return static_cast<bitxor_exprt &>(expr);
201 }
202 
205 {
206 public:
208  : multi_ary_exprt(std::move(_op0), ID_bitxnor, std::move(_op1))
209  {
210  }
211 };
212 
213 template <>
214 inline bool can_cast_expr<bitxnor_exprt>(const exprt &base)
215 {
216  return base.id() == ID_bitxnor;
217 }
218 
225 inline const bitxnor_exprt &to_bitxnor_expr(const exprt &expr)
226 {
227  PRECONDITION(expr.id() == ID_bitxnor);
228  return static_cast<const bitxnor_exprt &>(expr);
229 }
230 
233 {
234  PRECONDITION(expr.id() == ID_bitxnor);
235  return static_cast<bitxnor_exprt &>(expr);
236 }
237 
240 {
241 public:
242  bitand_exprt(const exprt &_op0, exprt _op1)
243  : multi_ary_exprt(_op0, ID_bitand, std::move(_op1), _op0.type())
244  {
245  }
246 
248  : multi_ary_exprt(ID_bitand, std::move(_operands), std::move(_type))
249  {
250  }
251 };
252 
253 template <>
254 inline bool can_cast_expr<bitand_exprt>(const exprt &base)
255 {
256  return base.id() == ID_bitand;
257 }
258 
265 inline const bitand_exprt &to_bitand_expr(const exprt &expr)
266 {
267  PRECONDITION(expr.id() == ID_bitand);
268  return static_cast<const bitand_exprt &>(expr);
269 }
270 
273 {
274  PRECONDITION(expr.id() == ID_bitand);
275  return static_cast<bitand_exprt &>(expr);
276 }
277 
279 class shift_exprt : public binary_exprt
280 {
281 public:
282  shift_exprt(exprt _src, const irep_idt &_id, exprt _distance)
283  : binary_exprt(std::move(_src), _id, std::move(_distance))
284  {
285  }
286 
287  shift_exprt(exprt _src, const irep_idt &_id, const std::size_t _distance);
288 
290  {
291  return op0();
292  }
293 
294  const exprt &op() const
295  {
296  return op0();
297  }
298 
300  {
301  return op1();
302  }
303 
304  const exprt &distance() const
305  {
306  return op1();
307  }
308 };
309 
310 template <>
311 inline bool can_cast_expr<shift_exprt>(const exprt &base)
312 {
313  return base.id() == ID_shl || base.id() == ID_ashr || base.id() == ID_lshr ||
314  base.id() == ID_ror || base.id() == ID_rol;
315 }
316 
317 inline void validate_expr(const shift_exprt &value)
318 {
319  validate_operands(value, 2, "Shifts must have two operands");
320 }
321 
328 inline const shift_exprt &to_shift_expr(const exprt &expr)
329 {
330  const shift_exprt &ret = static_cast<const shift_exprt &>(expr);
331  validate_expr(ret);
332  return ret;
333 }
334 
337 {
338  shift_exprt &ret = static_cast<shift_exprt &>(expr);
339  validate_expr(ret);
340  return ret;
341 }
342 
344 class shl_exprt : public shift_exprt
345 {
346 public:
347  shl_exprt(exprt _src, exprt _distance)
348  : shift_exprt(std::move(_src), ID_shl, std::move(_distance))
349  {
350  }
351 
352  shl_exprt(exprt _src, const std::size_t _distance)
353  : shift_exprt(std::move(_src), ID_shl, _distance)
354  {
355  }
356 };
357 
358 template <>
359 inline bool can_cast_expr<shl_exprt>(const exprt &base)
360 {
361  return base.id() == ID_shl;
362 }
363 
370 inline const shl_exprt &to_shl_expr(const exprt &expr)
371 {
372  PRECONDITION(expr.id() == ID_shl);
373  const shl_exprt &ret = static_cast<const shl_exprt &>(expr);
374  validate_expr(ret);
375  return ret;
376 }
377 
380 {
381  PRECONDITION(expr.id() == ID_shl);
382  shl_exprt &ret = static_cast<shl_exprt &>(expr);
383  validate_expr(ret);
384  return ret;
385 }
386 
388 class ashr_exprt : public shift_exprt
389 {
390 public:
391  ashr_exprt(exprt _src, exprt _distance)
392  : shift_exprt(std::move(_src), ID_ashr, std::move(_distance))
393  {
394  }
395 
396  ashr_exprt(exprt _src, const std::size_t _distance)
397  : shift_exprt(std::move(_src), ID_ashr, _distance)
398  {
399  }
400 };
401 
402 template <>
403 inline bool can_cast_expr<ashr_exprt>(const exprt &base)
404 {
405  return base.id() == ID_ashr;
406 }
407 
409 class lshr_exprt : public shift_exprt
410 {
411 public:
412  lshr_exprt(exprt _src, exprt _distance)
413  : shift_exprt(std::move(_src), ID_lshr, std::move(_distance))
414  {
415  }
416 
417  lshr_exprt(exprt _src, const std::size_t _distance)
418  : shift_exprt(std::move(_src), ID_lshr, std::move(_distance))
419  {
420  }
421 };
422 
423 template <>
424 inline bool can_cast_expr<lshr_exprt>(const exprt &base)
425 {
426  return base.id() == ID_lshr;
427 }
428 
431 {
432 public:
435  : binary_predicate_exprt(std::move(_src), ID_extractbit, std::move(_index))
436  {
437  }
438 
439  extractbit_exprt(exprt _src, const std::size_t _index);
440 
442  {
443  return op0();
444  }
445 
447  {
448  return op1();
449  }
450 
451  const exprt &src() const
452  {
453  return op0();
454  }
455 
456  const exprt &index() const
457  {
458  return op1();
459  }
460 };
461 
462 template <>
463 inline bool can_cast_expr<extractbit_exprt>(const exprt &base)
464 {
465  return base.id() == ID_extractbit;
466 }
467 
468 inline void validate_expr(const extractbit_exprt &value)
469 {
470  validate_operands(value, 2, "Extract bit must have two operands");
471 }
472 
479 inline const extractbit_exprt &to_extractbit_expr(const exprt &expr)
480 {
481  PRECONDITION(expr.id() == ID_extractbit);
482  const extractbit_exprt &ret = static_cast<const extractbit_exprt &>(expr);
483  validate_expr(ret);
484  return ret;
485 }
486 
489 {
490  PRECONDITION(expr.id() == ID_extractbit);
491  extractbit_exprt &ret = static_cast<extractbit_exprt &>(expr);
492  validate_expr(ret);
493  return ret;
494 }
495 
498 {
499 public:
505  extractbits_exprt(exprt _src, exprt _index, typet _type)
506  : expr_protectedt(
507  ID_extractbits,
508  std::move(_type),
509  {std::move(_src), std::move(_index)})
510  {
511  }
512 
513  extractbits_exprt(exprt _src, const std::size_t _index, typet _type);
514 
516  {
517  return op0();
518  }
519 
521  {
522  return op1();
523  }
524 
525  const exprt &src() const
526  {
527  return op0();
528  }
529 
530  const exprt &index() const
531  {
532  return op1();
533  }
534 };
535 
536 template <>
537 inline bool can_cast_expr<extractbits_exprt>(const exprt &base)
538 {
539  return base.id() == ID_extractbits;
540 }
541 
542 inline void validate_expr(const extractbits_exprt &value)
543 {
544  validate_operands(value, 2, "Extractbits must have two operands");
545 }
546 
553 inline const extractbits_exprt &to_extractbits_expr(const exprt &expr)
554 {
555  PRECONDITION(expr.id() == ID_extractbits);
556  const extractbits_exprt &ret = static_cast<const extractbits_exprt &>(expr);
557  validate_expr(ret);
558  return ret;
559 }
560 
563 {
564  PRECONDITION(expr.id() == ID_extractbits);
565  extractbits_exprt &ret = static_cast<extractbits_exprt &>(expr);
566  validate_expr(ret);
567  return ret;
568 }
569 
572 {
573 public:
578  update_bit_exprt(exprt _src, exprt _index, exprt _new_value)
579  : expr_protectedt(
580  ID_update_bit,
581  _src.type(),
582  {_src, std::move(_index), std::move(_new_value)})
583  {
584  PRECONDITION(new_value().type().id() == ID_bool);
585  }
586 
587  update_bit_exprt(exprt _src, const std::size_t _index, exprt _new_value);
588 
590  {
591  return op0();
592  }
593 
595  {
596  return op1();
597  }
598 
600  {
601  return op2();
602  }
603 
604  const exprt &src() const
605  {
606  return op0();
607  }
608 
609  const exprt &index() const
610  {
611  return op1();
612  }
613 
614  const exprt &new_value() const
615  {
616  return op2();
617  }
618 
619  static void check(
620  const exprt &expr,
622  {
623  validate_operands(expr, 3, "update_bit must have three operands");
624  }
625 
627  exprt lower() const;
628 };
629 
630 template <>
631 inline bool can_cast_expr<update_bit_exprt>(const exprt &base)
632 {
633  return base.id() == ID_update_bit;
634 }
635 
642 inline const update_bit_exprt &to_update_bit_expr(const exprt &expr)
643 {
644  PRECONDITION(expr.id() == ID_update_bit);
646  return static_cast<const update_bit_exprt &>(expr);
647 }
648 
651 {
652  PRECONDITION(expr.id() == ID_update_bit);
654  return static_cast<update_bit_exprt &>(expr);
655 }
656 
659 {
660 public:
665  update_bits_exprt(exprt _src, exprt _index, exprt _new_value)
666  : expr_protectedt(
667  ID_update_bits,
668  _src.type(),
669  {_src, std::move(_index), std::move(_new_value)})
670  {
671  }
672 
673  update_bits_exprt(exprt _src, const std::size_t _index, exprt _new_value);
674 
676  {
677  return op0();
678  }
679 
681  {
682  return op1();
683  }
684 
686  {
687  return op2();
688  }
689 
690  const exprt &src() const
691  {
692  return op0();
693  }
694 
695  const exprt &index() const
696  {
697  return op1();
698  }
699 
700  const exprt &new_value() const
701  {
702  return op2();
703  }
704 
705  static void check(
706  const exprt &expr,
708  {
709  validate_operands(expr, 3, "update_bits must have three operands");
710  }
711 
713  exprt lower() const;
714 };
715 
716 template <>
717 inline bool can_cast_expr<update_bits_exprt>(const exprt &base)
718 {
719  return base.id() == ID_update_bits;
720 }
721 
728 inline const update_bits_exprt &to_update_bits_expr(const exprt &expr)
729 {
730  PRECONDITION(expr.id() == ID_update_bits);
732  return static_cast<const update_bits_exprt &>(expr);
733 }
734 
737 {
738  PRECONDITION(expr.id() == ID_update_bits);
740  return static_cast<update_bits_exprt &>(expr);
741 }
742 
745 {
746 public:
748  : binary_exprt(
749  std::move(_times),
750  ID_replication,
751  std::move(_src),
752  std::move(_type))
753  {
754  }
755 
757  {
758  return static_cast<constant_exprt &>(op0());
759  }
760 
761  const constant_exprt &times() const
762  {
763  return static_cast<const constant_exprt &>(op0());
764  }
765 
767  {
768  return op1();
769  }
770 
771  const exprt &op() const
772  {
773  return op1();
774  }
775 };
776 
777 template <>
778 inline bool can_cast_expr<replication_exprt>(const exprt &base)
779 {
780  return base.id() == ID_replication;
781 }
782 
783 inline void validate_expr(const replication_exprt &value)
784 {
785  validate_operands(value, 2, "Bit-wise replication must have two operands");
786 }
787 
794 inline const replication_exprt &to_replication_expr(const exprt &expr)
795 {
796  PRECONDITION(expr.id() == ID_replication);
797  const replication_exprt &ret = static_cast<const replication_exprt &>(expr);
798  validate_expr(ret);
799  return ret;
800 }
801 
804 {
805  PRECONDITION(expr.id() == ID_replication);
806  replication_exprt &ret = static_cast<replication_exprt &>(expr);
807  validate_expr(ret);
808  return ret;
809 }
810 
817 {
818 public:
820  : multi_ary_exprt(ID_concatenation, std::move(_operands), std::move(_type))
821  {
822  }
823 
825  : multi_ary_exprt(
826  ID_concatenation,
827  {std::move(_op0), std::move(_op1)},
828  std::move(_type))
829  {
830  }
831 };
832 
833 template <>
835 {
836  return base.id() == ID_concatenation;
837 }
838 
846 {
847  PRECONDITION(expr.id() == ID_concatenation);
848  return static_cast<const concatenation_exprt &>(expr);
849 }
850 
853 {
854  PRECONDITION(expr.id() == ID_concatenation);
855  return static_cast<concatenation_exprt &>(expr);
856 }
857 
860 {
861 public:
863  : unary_exprt(ID_popcount, std::move(_op), std::move(_type))
864  {
865  }
866 
867  explicit popcount_exprt(const exprt &_op)
868  : unary_exprt(ID_popcount, _op, _op.type())
869  {
870  }
871 
874  exprt lower() const;
875 };
876 
877 template <>
878 inline bool can_cast_expr<popcount_exprt>(const exprt &base)
879 {
880  return base.id() == ID_popcount;
881 }
882 
883 inline void validate_expr(const popcount_exprt &value)
884 {
885  validate_operands(value, 1, "popcount must have one operand");
886 }
887 
894 inline const popcount_exprt &to_popcount_expr(const exprt &expr)
895 {
896  PRECONDITION(expr.id() == ID_popcount);
897  const popcount_exprt &ret = static_cast<const popcount_exprt &>(expr);
898  validate_expr(ret);
899  return ret;
900 }
901 
904 {
905  PRECONDITION(expr.id() == ID_popcount);
906  popcount_exprt &ret = static_cast<popcount_exprt &>(expr);
907  validate_expr(ret);
908  return ret;
909 }
910 
914 {
915 public:
916  binary_overflow_exprt(exprt _lhs, const irep_idt &kind, exprt _rhs)
917  : binary_predicate_exprt(std::move(_lhs), make_id(kind), std::move(_rhs))
918  {
919  INVARIANT(
920  valid_id(id()),
921  "The kind used to construct binary_overflow_exprt should be in the set "
922  "of expected valid kinds.");
923  }
924 
925  static void check(
926  const exprt &expr,
928  {
929  binary_exprt::check(expr, vm);
930 
931  if(expr.id() != ID_overflow_shl)
932  {
933  const binary_exprt &binary_expr = to_binary_expr(expr);
934  DATA_CHECK(
935  vm,
936  binary_expr.lhs().type() == binary_expr.rhs().type(),
937  "operand types must match");
938  }
939  }
940 
941  static void validate(
942  const exprt &expr,
943  const namespacet &,
945  {
946  check(expr, vm);
947  }
948 
950  static bool valid_id(const irep_idt &id)
951  {
952  return id == ID_overflow_plus || id == ID_overflow_mult ||
953  id == ID_overflow_minus || id == ID_overflow_shl;
954  }
955 
956 private:
957  static irep_idt make_id(const irep_idt &kind)
958  {
959  if(valid_id(kind))
960  return kind;
961  else
962  return "overflow-" + id2string(kind);
963  }
964 };
965 
966 template <>
968 {
969  return binary_overflow_exprt::valid_id(base.id());
970 }
971 
972 inline void validate_expr(const binary_overflow_exprt &value)
973 {
975  value, 2, "binary overflow expression must have two operands");
976 }
977 
985 {
986  PRECONDITION(
987  expr.id() == ID_overflow_plus || expr.id() == ID_overflow_mult ||
988  expr.id() == ID_overflow_minus || expr.id() == ID_overflow_shl);
989  const binary_overflow_exprt &ret =
990  static_cast<const binary_overflow_exprt &>(expr);
991  validate_expr(ret);
992  return ret;
993 }
994 
997 {
998  PRECONDITION(
999  expr.id() == ID_overflow_plus || expr.id() == ID_overflow_mult ||
1000  expr.id() == ID_overflow_minus || expr.id() == ID_overflow_shl);
1001  binary_overflow_exprt &ret = static_cast<binary_overflow_exprt &>(expr);
1002  validate_expr(ret);
1003  return ret;
1004 }
1005 
1007 {
1008 public:
1010  : binary_overflow_exprt(std::move(_lhs), ID_overflow_plus, std::move(_rhs))
1011  {
1012  }
1013 
1016  exprt lower() const;
1017 };
1018 
1019 template <>
1021 {
1022  return base.id() == ID_overflow_plus;
1023 }
1024 
1026 {
1027 public:
1029  : binary_overflow_exprt(std::move(_lhs), ID_overflow_minus, std::move(_rhs))
1030  {
1031  }
1032 
1035  exprt lower() const;
1036 };
1037 
1038 template <>
1040 {
1041  return base.id() == ID_overflow_minus;
1042 }
1043 
1045 {
1046 public:
1048  : binary_overflow_exprt(std::move(_lhs), ID_overflow_mult, std::move(_rhs))
1049  {
1050  }
1051 
1054  exprt lower() const;
1055 };
1056 
1057 template <>
1059 {
1060  return base.id() == ID_overflow_mult;
1061 }
1062 
1064 {
1065 public:
1067  : binary_overflow_exprt(std::move(_lhs), ID_overflow_shl, std::move(_rhs))
1068  {
1069  }
1070 };
1071 
1072 template <>
1074 {
1075  return base.id() == ID_overflow_shl;
1076 }
1077 
1081 {
1082 public:
1084  : unary_predicate_exprt("overflow-" + id2string(kind), std::move(_op))
1085  {
1086  }
1087 
1088  static void check(
1089  const exprt &expr,
1091  {
1092  unary_exprt::check(expr, vm);
1093  }
1094 
1095  static void validate(
1096  const exprt &expr,
1097  const namespacet &,
1099  {
1100  check(expr, vm);
1101  }
1102 };
1103 
1104 template <>
1106 {
1107  return base.id() == ID_overflow_unary_minus;
1108 }
1109 
1110 inline void validate_expr(const unary_overflow_exprt &value)
1111 {
1113  value, 1, "unary overflow expression must have one operand");
1114 }
1115 
1119 {
1120 public:
1122  : unary_overflow_exprt(ID_unary_minus, std::move(_op))
1123  {
1124  }
1125 
1126  static void check(
1127  const exprt &expr,
1129  {
1130  unary_exprt::check(expr, vm);
1131  }
1132 
1133  static void validate(
1134  const exprt &expr,
1135  const namespacet &,
1137  {
1138  check(expr, vm);
1139  }
1140 };
1141 
1142 template <>
1144 {
1145  return base.id() == ID_overflow_unary_minus;
1146 }
1147 
1149 {
1151  value, 1, "unary minus overflow expression must have one operand");
1152 }
1153 
1161 {
1162  PRECONDITION(expr.id() == ID_overflow_unary_minus);
1163  const unary_overflow_exprt &ret =
1164  static_cast<const unary_overflow_exprt &>(expr);
1165  validate_expr(ret);
1166  return ret;
1167 }
1168 
1171 {
1172  PRECONDITION(expr.id() == ID_overflow_unary_minus);
1173  unary_overflow_exprt &ret = static_cast<unary_overflow_exprt &>(expr);
1174  validate_expr(ret);
1175  return ret;
1176 }
1177 
1184 {
1185 public:
1186  count_leading_zeros_exprt(exprt _op, bool _zero_permitted, typet _type)
1187  : unary_exprt(ID_count_leading_zeros, std::move(_op), std::move(_type))
1188  {
1189  zero_permitted(_zero_permitted);
1190  }
1191 
1192  explicit count_leading_zeros_exprt(const exprt &_op)
1193  : count_leading_zeros_exprt(_op, true, _op.type())
1194  {
1195  }
1196 
1197  bool zero_permitted() const
1198  {
1199  return !get_bool(ID_C_bounds_check);
1200  }
1201 
1202  void zero_permitted(bool value)
1203  {
1204  set(ID_C_bounds_check, !value);
1205  }
1206 
1207  static void check(
1208  const exprt &expr,
1210  {
1211  DATA_CHECK(
1212  vm,
1213  expr.operands().size() == 1,
1214  "unary expression must have a single operand");
1215  DATA_CHECK(
1216  vm,
1218  "operand must be of bitvector type");
1219  }
1220 
1221  static void validate(
1222  const exprt &expr,
1223  const namespacet &,
1225  {
1226  check(expr, vm);
1227  }
1228 
1231  exprt lower() const;
1232 };
1233 
1234 template <>
1236 {
1237  return base.id() == ID_count_leading_zeros;
1238 }
1239 
1240 inline void validate_expr(const count_leading_zeros_exprt &value)
1241 {
1242  validate_operands(value, 1, "count_leading_zeros must have one operand");
1243 }
1244 
1251 inline const count_leading_zeros_exprt &
1253 {
1254  PRECONDITION(expr.id() == ID_count_leading_zeros);
1255  const count_leading_zeros_exprt &ret =
1256  static_cast<const count_leading_zeros_exprt &>(expr);
1257  validate_expr(ret);
1258  return ret;
1259 }
1260 
1263 {
1264  PRECONDITION(expr.id() == ID_count_leading_zeros);
1266  static_cast<count_leading_zeros_exprt &>(expr);
1267  validate_expr(ret);
1268  return ret;
1269 }
1270 
1277 {
1278 public:
1279  count_trailing_zeros_exprt(exprt _op, bool _zero_permitted, typet _type)
1280  : unary_exprt(ID_count_trailing_zeros, std::move(_op), std::move(_type))
1281  {
1282  zero_permitted(_zero_permitted);
1283  }
1284 
1285  explicit count_trailing_zeros_exprt(const exprt &_op)
1286  : count_trailing_zeros_exprt(_op, true, _op.type())
1287  {
1288  }
1289 
1290  bool zero_permitted() const
1291  {
1292  return !get_bool(ID_C_bounds_check);
1293  }
1294 
1295  void zero_permitted(bool value)
1296  {
1297  set(ID_C_bounds_check, !value);
1298  }
1299 
1300  static void check(
1301  const exprt &expr,
1303  {
1304  DATA_CHECK(
1305  vm,
1306  expr.operands().size() == 1,
1307  "unary expression must have a single operand");
1308  DATA_CHECK(
1309  vm,
1311  "operand must be of bitvector type");
1312  }
1313 
1314  static void validate(
1315  const exprt &expr,
1316  const namespacet &,
1318  {
1319  check(expr, vm);
1320  }
1321 
1324  exprt lower() const;
1325 };
1326 
1327 template <>
1329 {
1330  return base.id() == ID_count_trailing_zeros;
1331 }
1332 
1334 {
1335  validate_operands(value, 1, "count_trailing_zeros must have one operand");
1336 }
1337 
1344 inline const count_trailing_zeros_exprt &
1346 {
1347  PRECONDITION(expr.id() == ID_count_trailing_zeros);
1348  const count_trailing_zeros_exprt &ret =
1349  static_cast<const count_trailing_zeros_exprt &>(expr);
1350  validate_expr(ret);
1351  return ret;
1352 }
1353 
1356 {
1357  PRECONDITION(expr.id() == ID_count_trailing_zeros);
1359  static_cast<count_trailing_zeros_exprt &>(expr);
1360  validate_expr(ret);
1361  return ret;
1362 }
1363 
1366 {
1367 public:
1369  : unary_exprt(ID_bitreverse, std::move(op))
1370  {
1371  }
1372 
1375  exprt lower() const;
1376 };
1377 
1378 template <>
1379 inline bool can_cast_expr<bitreverse_exprt>(const exprt &base)
1380 {
1381  return base.id() == ID_bitreverse;
1382 }
1383 
1384 inline void validate_expr(const bitreverse_exprt &value)
1385 {
1386  validate_operands(value, 1, "Bit-wise reverse must have one operand");
1387 }
1388 
1395 inline const bitreverse_exprt &to_bitreverse_expr(const exprt &expr)
1396 {
1397  PRECONDITION(expr.id() == ID_bitreverse);
1398  const bitreverse_exprt &ret = static_cast<const bitreverse_exprt &>(expr);
1399  validate_expr(ret);
1400  return ret;
1401 }
1402 
1405 {
1406  PRECONDITION(expr.id() == ID_bitreverse);
1407  bitreverse_exprt &ret = static_cast<bitreverse_exprt &>(expr);
1408  validate_expr(ret);
1409  return ret;
1410 }
1411 
1414 {
1415 public:
1417  : binary_exprt(std::move(_lhs), ID_saturating_plus, std::move(_rhs))
1418  {
1419  }
1420 
1422  : binary_exprt(
1423  std::move(_lhs),
1424  ID_saturating_plus,
1425  std::move(_rhs),
1426  std::move(_type))
1427  {
1428  }
1429 };
1430 
1431 template <>
1433 {
1434  return base.id() == ID_saturating_plus;
1435 }
1436 
1437 inline void validate_expr(const saturating_plus_exprt &value)
1438 {
1439  validate_operands(value, 2, "saturating plus must have two operands");
1440 }
1441 
1449 {
1450  PRECONDITION(expr.id() == ID_saturating_plus);
1451  const saturating_plus_exprt &ret =
1452  static_cast<const saturating_plus_exprt &>(expr);
1453  validate_expr(ret);
1454  return ret;
1455 }
1456 
1459 {
1460  PRECONDITION(expr.id() == ID_saturating_plus);
1461  saturating_plus_exprt &ret = static_cast<saturating_plus_exprt &>(expr);
1462  validate_expr(ret);
1463  return ret;
1464 }
1465 
1468 {
1469 public:
1471  : binary_exprt(std::move(_lhs), ID_saturating_minus, std::move(_rhs))
1472  {
1473  }
1474 };
1475 
1476 template <>
1478 {
1479  return base.id() == ID_saturating_minus;
1480 }
1481 
1482 inline void validate_expr(const saturating_minus_exprt &value)
1483 {
1484  validate_operands(value, 2, "saturating minus must have two operands");
1485 }
1486 
1494 {
1495  PRECONDITION(expr.id() == ID_saturating_minus);
1496  const saturating_minus_exprt &ret =
1497  static_cast<const saturating_minus_exprt &>(expr);
1498  validate_expr(ret);
1499  return ret;
1500 }
1501 
1504 {
1505  PRECONDITION(expr.id() == ID_saturating_minus);
1506  saturating_minus_exprt &ret = static_cast<saturating_minus_exprt &>(expr);
1507  validate_expr(ret);
1508  return ret;
1509 }
1510 
1514 {
1515 public:
1516  overflow_result_exprt(exprt _lhs, const irep_idt &kind, exprt _rhs)
1517  : expr_protectedt(
1518  make_id(kind),
1519  struct_typet{
1520  {{ID_value, _lhs.type()},
1521  {"overflow-" + id2string(kind), bool_typet{}}}},
1522  {_lhs, std::move(_rhs)})
1523  {
1524  INVARIANT(
1525  valid_id(id()),
1526  "The kind used to construct overflow_result_exprt should be in the set "
1527  "of expected valid kinds.");
1528  }
1529 
1531  : expr_protectedt(
1532  make_id(kind),
1533  struct_typet{
1534  {{ID_value, _op.type()},
1535  {"overflow-" + id2string(kind), bool_typet{}}}},
1536  {_op})
1537  {
1538  INVARIANT(
1539  valid_id(id()),
1540  "The kind used to construct overflow_result_exprt should be in the set "
1541  "of expected valid kinds.");
1542  }
1543 
1544  // make op0 and op1 public
1545  using exprt::op0;
1546  using exprt::op1;
1547 
1548  const exprt &op2() const = delete;
1549  exprt &op2() = delete;
1550  const exprt &op3() const = delete;
1551  exprt &op3() = delete;
1552 
1553  static void check(
1554  const exprt &expr,
1556  {
1557  if(expr.id() != ID_overflow_result_unary_minus)
1558  binary_exprt::check(expr, vm);
1559 
1560  if(
1561  expr.id() != ID_overflow_result_unary_minus &&
1562  expr.id() != ID_overflow_result_shl)
1563  {
1564  const binary_exprt &binary_expr = to_binary_expr(expr);
1565  DATA_CHECK(
1566  vm,
1567  binary_expr.lhs().type() == binary_expr.rhs().type(),
1568  "operand types must match");
1569  }
1570  }
1571 
1572  static void validate(
1573  const exprt &expr,
1574  const namespacet &,
1576  {
1577  check(expr, vm);
1578  }
1579 
1581  static bool valid_id(const irep_idt &id)
1582  {
1583  return id == ID_overflow_result_plus || id == ID_overflow_result_mult ||
1584  id == ID_overflow_result_minus || id == ID_overflow_result_shl ||
1585  id == ID_overflow_result_unary_minus;
1586  }
1587 
1588 private:
1589  static irep_idt make_id(const irep_idt &kind)
1590  {
1591  return "overflow_result-" + id2string(kind);
1592  }
1593 };
1594 
1595 template <>
1597 {
1598  return overflow_result_exprt::valid_id(base.id());
1599 }
1600 
1601 inline void validate_expr(const overflow_result_exprt &value)
1602 {
1603  if(value.id() == ID_overflow_result_unary_minus)
1604  {
1606  value, 1, "unary overflow expression must have two operands");
1607  }
1608  else
1609  {
1611  value, 2, "binary overflow expression must have two operands");
1612  }
1613 }
1614 
1622 {
1624  const overflow_result_exprt &ret =
1625  static_cast<const overflow_result_exprt &>(expr);
1626  validate_expr(ret);
1627  return ret;
1628 }
1629 
1632 {
1634  overflow_result_exprt &ret = static_cast<overflow_result_exprt &>(expr);
1635  validate_expr(ret);
1636  return ret;
1637 }
1638 
1642 {
1643 public:
1645  : unary_exprt(ID_find_first_set, std::move(_op), std::move(_type))
1646  {
1647  }
1648 
1649  explicit find_first_set_exprt(const exprt &_op)
1650  : find_first_set_exprt(_op, _op.type())
1651  {
1652  }
1653 
1654  static void check(
1655  const exprt &expr,
1657  {
1658  DATA_CHECK(
1659  vm,
1660  expr.operands().size() == 1,
1661  "unary expression must have a single operand");
1662  DATA_CHECK(
1663  vm,
1665  "operand must be of bitvector type");
1666  }
1667 
1668  static void validate(
1669  const exprt &expr,
1670  const namespacet &,
1672  {
1673  check(expr, vm);
1674  }
1675 
1678  exprt lower() const;
1679 };
1680 
1681 template <>
1683 {
1684  return base.id() == ID_find_first_set;
1685 }
1686 
1687 inline void validate_expr(const find_first_set_exprt &value)
1688 {
1689  validate_operands(value, 1, "find_first_set must have one operand");
1690 }
1691 
1699 {
1700  PRECONDITION(expr.id() == ID_find_first_set);
1701  const find_first_set_exprt &ret =
1702  static_cast<const find_first_set_exprt &>(expr);
1703  validate_expr(ret);
1704  return ret;
1705 }
1706 
1709 {
1710  PRECONDITION(expr.id() == ID_find_first_set);
1711  find_first_set_exprt &ret = static_cast<find_first_set_exprt &>(expr);
1712  validate_expr(ret);
1713  return ret;
1714 }
1715 
1722 {
1723 public:
1725  : unary_exprt(ID_zero_extend, std::move(_op), std::move(_type))
1726  {
1727  }
1728 
1729  // a lowering to extraction or concatenation
1730  exprt lower() const;
1731 };
1732 
1733 template <>
1734 inline bool can_cast_expr<zero_extend_exprt>(const exprt &base)
1735 {
1736  return base.id() == ID_zero_extend;
1737 }
1738 
1745 inline const zero_extend_exprt &to_zero_extend_expr(const exprt &expr)
1746 {
1747  PRECONDITION(expr.id() == ID_zero_extend);
1749  return static_cast<const zero_extend_exprt &>(expr);
1750 }
1751 
1754 {
1755  PRECONDITION(expr.id() == ID_zero_extend);
1757  return static_cast<zero_extend_exprt &>(expr);
1758 }
1759 
1763 {
1764 public:
1765  explicit onehot_exprt(exprt _op)
1766  : unary_predicate_exprt(ID_onehot, std::move(_op))
1767  {
1768  }
1769 
1771  exprt lower() const;
1772 };
1773 
1780 inline const onehot_exprt &to_onehot_expr(const exprt &expr)
1781 {
1782  PRECONDITION(expr.id() == ID_onehot);
1783  onehot_exprt::check(expr);
1784  return static_cast<const onehot_exprt &>(expr);
1785 }
1786 
1789 {
1790  PRECONDITION(expr.id() == ID_onehot);
1791  onehot_exprt::check(expr);
1792  return static_cast<onehot_exprt &>(expr);
1793 }
1794 
1798 {
1799 public:
1800  explicit onehot0_exprt(exprt _op)
1801  : unary_predicate_exprt(ID_onehot0, std::move(_op))
1802  {
1803  }
1804 
1806  exprt lower() const;
1807 };
1808 
1815 inline const onehot0_exprt &to_onehot0_expr(const exprt &expr)
1816 {
1817  PRECONDITION(expr.id() == ID_onehot0);
1818  onehot0_exprt::check(expr);
1819  return static_cast<const onehot0_exprt &>(expr);
1820 }
1821 
1824 {
1825  PRECONDITION(expr.id() == ID_onehot0);
1826  onehot0_exprt::check(expr);
1827  return static_cast<onehot0_exprt &>(expr);
1828 }
1829 
1830 #endif // CPROVER_UTIL_BITVECTOR_EXPR_H
const update_bit_exprt & to_update_bit_expr(const exprt &expr)
Cast an exprt to an update_bit_exprt.
bool can_cast_expr< count_trailing_zeros_exprt >(const exprt &base)
const onehot_exprt & to_onehot_expr(const exprt &expr)
Cast an exprt to a onehot_exprt.
bool can_cast_expr< mult_overflow_exprt >(const exprt &base)
bool can_cast_expr< replication_exprt >(const exprt &base)
bool can_cast_expr< bswap_exprt >(const exprt &base)
bool can_cast_expr< find_first_set_exprt >(const exprt &base)
bool can_cast_expr< saturating_plus_exprt >(const exprt &base)
bool can_cast_expr< bitreverse_exprt >(const exprt &base)
bool can_cast_expr< count_leading_zeros_exprt >(const exprt &base)
bool can_cast_expr< shift_exprt >(const exprt &base)
bool can_cast_expr< bitand_exprt >(const exprt &base)
bool can_cast_expr< update_bits_exprt >(const exprt &base)
bool can_cast_expr< saturating_minus_exprt >(const exprt &base)
const overflow_result_exprt & to_overflow_result_expr(const exprt &expr)
Cast an exprt to a overflow_result_exprt.
const binary_overflow_exprt & to_binary_overflow_expr(const exprt &expr)
Cast an exprt to a binary_overflow_exprt.
bool can_cast_expr< popcount_exprt >(const exprt &base)
bool can_cast_expr< extractbits_exprt >(const exprt &base)
const onehot0_exprt & to_onehot0_expr(const exprt &expr)
Cast an exprt to a onehot0_exprt.
bool can_cast_expr< bitxor_exprt >(const exprt &base)
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
bool can_cast_expr< bitor_exprt >(const exprt &base)
bool can_cast_expr< update_bit_exprt >(const exprt &base)
bool can_cast_expr< minus_overflow_exprt >(const exprt &base)
void validate_expr(const bswap_exprt &value)
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast an exprt to an extractbit_exprt.
bool can_cast_expr< ashr_exprt >(const exprt &base)
bool can_cast_expr< zero_extend_exprt >(const exprt &base)
const extractbits_exprt & to_extractbits_expr(const exprt &expr)
Cast an exprt to an extractbits_exprt.
const unary_overflow_exprt & to_unary_overflow_expr(const exprt &expr)
Cast an exprt to a unary_overflow_exprt.
bool can_cast_expr< shl_overflow_exprt >(const exprt &base)
bool can_cast_expr< bitxnor_exprt >(const exprt &base)
const saturating_plus_exprt & to_saturating_plus_expr(const exprt &expr)
Cast an exprt to a saturating_plus_exprt.
const bitxor_exprt & to_bitxor_expr(const exprt &expr)
Cast an exprt to a bitxor_exprt.
const bitand_exprt & to_bitand_expr(const exprt &expr)
Cast an exprt to a bitand_exprt.
bool can_cast_expr< overflow_result_exprt >(const exprt &base)
bool can_cast_expr< concatenation_exprt >(const exprt &base)
const find_first_set_exprt & to_find_first_set_expr(const exprt &expr)
Cast an exprt to a find_first_set_exprt.
const bitreverse_exprt & to_bitreverse_expr(const exprt &expr)
Cast an exprt to a bitreverse_exprt.
const zero_extend_exprt & to_zero_extend_expr(const exprt &expr)
Cast an exprt to a zero_extend_exprt.
bool can_cast_expr< unary_overflow_exprt >(const exprt &base)
const count_trailing_zeros_exprt & to_count_trailing_zeros_expr(const exprt &expr)
Cast an exprt to a count_trailing_zeros_exprt.
bool can_cast_expr< lshr_exprt >(const exprt &base)
bool can_cast_expr< shl_exprt >(const exprt &base)
bool can_cast_expr< plus_overflow_exprt >(const exprt &base)
const bitnot_exprt & to_bitnot_expr(const exprt &expr)
Cast an exprt to a bitnot_exprt.
bool can_cast_expr< bitnot_exprt >(const exprt &base)
const saturating_minus_exprt & to_saturating_minus_expr(const exprt &expr)
Cast an exprt to a saturating_minus_exprt.
bool can_cast_expr< binary_overflow_exprt >(const exprt &base)
const replication_exprt & to_replication_expr(const exprt &expr)
Cast an exprt to a replication_exprt.
const concatenation_exprt & to_concatenation_expr(const exprt &expr)
Cast an exprt to a concatenation_exprt.
bool can_cast_expr< unary_minus_overflow_exprt >(const exprt &base)
bool can_cast_expr< extractbit_exprt >(const exprt &base)
const bitor_exprt & to_bitor_expr(const exprt &expr)
Cast an exprt to a bitor_exprt.
const bswap_exprt & to_bswap_expr(const exprt &expr)
Cast an exprt to a bswap_exprt.
const shl_exprt & to_shl_expr(const exprt &expr)
Cast an exprt to a shl_exprt.
const count_leading_zeros_exprt & to_count_leading_zeros_expr(const exprt &expr)
Cast an exprt to a count_leading_zeros_exprt.
const popcount_exprt & to_popcount_expr(const exprt &expr)
Cast an exprt to a popcount_exprt.
const update_bits_exprt & to_update_bits_expr(const exprt &expr)
Cast an exprt to an update_bits_exprt.
const bitxnor_exprt & to_bitxnor_expr(const exprt &expr)
Cast an exprt to a bitxnor_exprt.
Arithmetic right shift.
ashr_exprt(exprt _src, exprt _distance)
ashr_exprt(exprt _src, const std::size_t _distance)
A base class for binary expressions.
Definition: std_expr.h:638
exprt & op1()
Definition: expr.h:136
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:650
exprt & lhs()
Definition: std_expr.h:668
exprt & op0()
Definition: expr.h:133
exprt & rhs()
Definition: std_expr.h:678
A Boolean expression returning true, iff operation kind would result in an overflow when applied to o...
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
static bool valid_id(const irep_idt &id)
Returns true iff id is a valid identifier of a binary_overflow_exprt.
static irep_idt make_id(const irep_idt &kind)
binary_overflow_exprt(exprt _lhs, const irep_idt &kind, exprt _rhs)
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition: std_expr.h:731
Bit-wise AND.
bitand_exprt(exprt::operandst _operands, typet _type)
bitand_exprt(const exprt &_op0, exprt _op1)
Bit-wise negation of bit-vectors.
bitnot_exprt(exprt op)
Bit-wise OR.
bitor_exprt(exprt::operandst _operands, typet _type)
bitor_exprt(const exprt &_op0, exprt _op1)
Reverse the order of bits in a bit-vector.
bitreverse_exprt(exprt op)
exprt lower() const
Lower a bitreverse_exprt to arithmetic and logic expressions.
Bit-wise XNOR.
bitxnor_exprt(exprt _op0, exprt _op1)
Bit-wise XOR.
bitxor_exprt(exprt::operandst _operands, typet _type)
bitxor_exprt(exprt _op0, exprt _op1)
The Boolean type.
Definition: std_types.h:36
The byte swap expression.
bswap_exprt(exprt _op, std::size_t bits_per_byte)
std::size_t get_bits_per_byte() const
bswap_exprt(exprt _op, std::size_t bits_per_byte, typet _type)
void set_bits_per_byte(std::size_t bits_per_byte)
Concatenation of bit-vector operands.
concatenation_exprt(operandst _operands, typet _type)
concatenation_exprt(exprt _op0, exprt _op1, typet _type)
A constant literal expression.
Definition: std_expr.h:3000
The count leading zeros (counting the number of zero bits starting from the most-significant bit) exp...
static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
void zero_permitted(bool value)
exprt lower() const
Lower a count_leading_zeros_exprt to arithmetic and logic expressions.
count_leading_zeros_exprt(const exprt &_op)
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
count_leading_zeros_exprt(exprt _op, bool _zero_permitted, typet _type)
The count trailing zeros (counting the number of zero bits starting from the least-significant bit) e...
count_trailing_zeros_exprt(const exprt &_op)
count_trailing_zeros_exprt(exprt _op, bool _zero_permitted, typet _type)
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
void zero_permitted(bool value)
exprt lower() const
Lower a count_trailing_zeros_exprt to arithmetic and logic expressions.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
Base class for all expressions.
Definition: expr.h:344
exprt & op1()
Definition: expr.h:136
exprt & op2()
Definition: expr.h:139
exprt & op0()
Definition: expr.h:133
Base class for all expressions.
Definition: expr.h:56
std::vector< exprt > operandst
Definition: expr.h:58
exprt & op1()
Definition: expr.h:136
typet & type()
Return the type of the expression.
Definition: expr.h:84
exprt & op0()
Definition: expr.h:133
operandst & operands()
Definition: expr.h:94
Extracts a single bit of a bit-vector operand.
extractbit_exprt(exprt _src, exprt _index)
Extract the _index-th least significant bit from _src.
const exprt & src() const
const exprt & index() const
Extracts a sub-range of a bit-vector operand.
const exprt & index() const
extractbits_exprt(exprt _src, exprt _index, typet _type)
Extract the bits [_index .
const exprt & src() const
Returns one plus the index of the least-significant one bit, or zero if the operand is zero.
find_first_set_exprt(exprt _op, typet _type)
static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
exprt lower() const
Lower a find_first_set_exprt to arithmetic and logic expressions.
find_first_set_exprt(const exprt &_op)
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
bool get_bool(const irep_idt &name) const
Definition: irep.cpp:57
std::size_t get_size_t(const irep_idt &name) const
Definition: irep.cpp:67
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:412
void set_size_t(const irep_idt &name, const std::size_t value)
Definition: irep.cpp:82
const irep_idt & id() const
Definition: irep.h:388
Logical right shift.
lshr_exprt(exprt _src, const std::size_t _distance)
lshr_exprt(exprt _src, exprt _distance)
minus_overflow_exprt(exprt _lhs, exprt _rhs)
exprt lower() const
Lower a minus_overflow_exprt to arithmetic and logic expressions.
mult_overflow_exprt(exprt _lhs, exprt _rhs)
exprt lower() const
Lower a mult_overflow_exprt to arithmetic and logic expressions.
A base class for multi-ary expressions Associativity is not specified.
Definition: std_expr.h:912
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
A Boolean expression returning true iff the given operand consists of exactly one '0' and '1' otherwi...
onehot0_exprt(exprt _op)
exprt lower() const
lowering to extractbit
A Boolean expression returning true iff the given operand consists of exactly one '1' and '0' otherwi...
onehot_exprt(exprt _op)
exprt lower() const
lowering to extractbit
An expression returning both the result of the arithmetic operation under wrap-around semantics as we...
exprt & op2()=delete
const exprt & op3() const =delete
overflow_result_exprt(exprt _lhs, const irep_idt &kind, exprt _rhs)
exprt & op3()=delete
overflow_result_exprt(exprt _op, const irep_idt &kind)
const exprt & op2() const =delete
static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
static bool valid_id(const irep_idt &id)
Returns true iff id is a valid identifier of an overflow_exprt.
static irep_idt make_id(const irep_idt &kind)
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
plus_overflow_exprt(exprt _lhs, exprt _rhs)
exprt lower() const
Lower a plus_overflow_exprt to arithmetic and logic expressions.
The popcount (counting the number of bits set to 1) expression.
exprt lower() const
Lower a popcount_exprt to arithmetic and logic expressions.
popcount_exprt(exprt _op, typet _type)
popcount_exprt(const exprt &_op)
Bit-vector replication.
const exprt & op() const
const constant_exprt & times() const
constant_exprt & times()
replication_exprt(constant_exprt _times, exprt _src, typet _type)
Saturating subtraction expression.
saturating_minus_exprt(exprt _lhs, exprt _rhs)
The saturating plus expression.
saturating_plus_exprt(exprt _lhs, exprt _rhs, typet _type)
saturating_plus_exprt(exprt _lhs, exprt _rhs)
A base class for shift and rotate operators.
exprt & distance()
exprt & op()
const exprt & distance() const
shift_exprt(exprt _src, const irep_idt &_id, exprt _distance)
const exprt & op() const
Left shift.
shl_exprt(exprt _src, const std::size_t _distance)
shl_exprt(exprt _src, exprt _distance)
shl_overflow_exprt(exprt _lhs, exprt _rhs)
Structure type, corresponds to C style structs.
Definition: std_types.h:231
The type of an expression, extends irept.
Definition: type.h:29
Generic base class for unary expressions.
Definition: std_expr.h:361
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:373
const exprt & op() const
Definition: std_expr.h:391
A Boolean expression returning true, iff negation would result in an overflow when applied to the (si...
static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
A Boolean expression returning true, iff operation kind would result in an overflow when applied to t...
static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
unary_overflow_exprt(const irep_idt &kind, exprt _op)
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly one argu...
Definition: std_expr.h:585
Replaces a sub-range of a bit-vector operand.
const exprt & new_value() const
update_bit_exprt(exprt _src, exprt _index, exprt _new_value)
Replaces the bit [_index] from _src to produce a result of the same type as _src.
const exprt & src() const
exprt lower() const
A lowering to masking, shifting, or.
const exprt & index() const
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Replaces a sub-range of a bit-vector operand.
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
const exprt & src() const
const exprt & index() const
update_bits_exprt(exprt _src, exprt _index, exprt _new_value)
Replace the bits [_index .
exprt lower() const
A lowering to masking, shifting, or.
update_bits_exprt(exprt _src, const std::size_t _index, exprt _new_value)
const exprt & new_value() const
zero extension The operand is converted to the given type by either a) truncating if the new type is ...
exprt lower() const
zero_extend_exprt(exprt _op, typet _type)
void validate_operands(const exprt &value, exprt::operandst::size_type number, const char *message, bool allow_more=false)
Definition: expr_cast.h:250
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:534
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
API to expression classes.
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:715
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:426
bool can_cast_type< bitvector_typet >(const typet &type)
Check whether a reference to a typet is a bitvector_typet.
Definition: std_types.h:952
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...
Definition: validate.h:22
validation_modet