cprover
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 };
132 
133 template <>
134 inline bool can_cast_expr<bitor_exprt>(const exprt &base)
135 {
136  return base.id() == ID_bitor;
137 }
138 
145 inline const bitor_exprt &to_bitor_expr(const exprt &expr)
146 {
147  PRECONDITION(expr.id() == ID_bitor);
148  return static_cast<const bitor_exprt &>(expr);
149 }
150 
153 {
154  PRECONDITION(expr.id() == ID_bitor);
155  return static_cast<bitor_exprt &>(expr);
156 }
157 
160 {
161 public:
163  : multi_ary_exprt(std::move(_op0), ID_bitxor, std::move(_op1))
164  {
165  }
166 };
167 
168 template <>
169 inline bool can_cast_expr<bitxor_exprt>(const exprt &base)
170 {
171  return base.id() == ID_bitxor;
172 }
173 
180 inline const bitxor_exprt &to_bitxor_expr(const exprt &expr)
181 {
182  PRECONDITION(expr.id() == ID_bitxor);
183  return static_cast<const bitxor_exprt &>(expr);
184 }
185 
188 {
189  PRECONDITION(expr.id() == ID_bitxor);
190  return static_cast<bitxor_exprt &>(expr);
191 }
192 
195 {
196 public:
197  bitand_exprt(const exprt &_op0, exprt _op1)
198  : multi_ary_exprt(_op0, ID_bitand, std::move(_op1), _op0.type())
199  {
200  }
201 };
202 
203 template <>
204 inline bool can_cast_expr<bitand_exprt>(const exprt &base)
205 {
206  return base.id() == ID_bitand;
207 }
208 
215 inline const bitand_exprt &to_bitand_expr(const exprt &expr)
216 {
217  PRECONDITION(expr.id() == ID_bitand);
218  return static_cast<const bitand_exprt &>(expr);
219 }
220 
223 {
224  PRECONDITION(expr.id() == ID_bitand);
225  return static_cast<bitand_exprt &>(expr);
226 }
227 
229 class shift_exprt : public binary_exprt
230 {
231 public:
232  shift_exprt(exprt _src, const irep_idt &_id, exprt _distance)
233  : binary_exprt(std::move(_src), _id, std::move(_distance))
234  {
235  }
236 
237  shift_exprt(exprt _src, const irep_idt &_id, const std::size_t _distance);
238 
240  {
241  return op0();
242  }
243 
244  const exprt &op() const
245  {
246  return op0();
247  }
248 
250  {
251  return op1();
252  }
253 
254  const exprt &distance() const
255  {
256  return op1();
257  }
258 };
259 
260 template <>
261 inline bool can_cast_expr<shift_exprt>(const exprt &base)
262 {
263  return base.id() == ID_shl || base.id() == ID_ashr || base.id() == ID_lshr ||
264  base.id() == ID_ror || base.id() == ID_rol;
265 }
266 
267 inline void validate_expr(const shift_exprt &value)
268 {
269  validate_operands(value, 2, "Shifts must have two operands");
270 }
271 
278 inline const shift_exprt &to_shift_expr(const exprt &expr)
279 {
280  const shift_exprt &ret = static_cast<const shift_exprt &>(expr);
281  validate_expr(ret);
282  return ret;
283 }
284 
287 {
288  shift_exprt &ret = static_cast<shift_exprt &>(expr);
289  validate_expr(ret);
290  return ret;
291 }
292 
294 class shl_exprt : public shift_exprt
295 {
296 public:
297  shl_exprt(exprt _src, exprt _distance)
298  : shift_exprt(std::move(_src), ID_shl, std::move(_distance))
299  {
300  }
301 
302  shl_exprt(exprt _src, const std::size_t _distance)
303  : shift_exprt(std::move(_src), ID_shl, _distance)
304  {
305  }
306 };
307 
314 inline const shl_exprt &to_shl_expr(const exprt &expr)
315 {
316  PRECONDITION(expr.id() == ID_shl);
317  const shl_exprt &ret = static_cast<const shl_exprt &>(expr);
318  validate_expr(ret);
319  return ret;
320 }
321 
324 {
325  PRECONDITION(expr.id() == ID_shl);
326  shl_exprt &ret = static_cast<shl_exprt &>(expr);
327  validate_expr(ret);
328  return ret;
329 }
330 
332 class ashr_exprt : public shift_exprt
333 {
334 public:
335  ashr_exprt(exprt _src, exprt _distance)
336  : shift_exprt(std::move(_src), ID_ashr, std::move(_distance))
337  {
338  }
339 
340  ashr_exprt(exprt _src, const std::size_t _distance)
341  : shift_exprt(std::move(_src), ID_ashr, _distance)
342  {
343  }
344 };
345 
347 class lshr_exprt : public shift_exprt
348 {
349 public:
350  lshr_exprt(exprt _src, exprt _distance)
351  : shift_exprt(std::move(_src), ID_lshr, std::move(_distance))
352  {
353  }
354 
355  lshr_exprt(exprt _src, const std::size_t _distance)
356  : shift_exprt(std::move(_src), ID_lshr, std::move(_distance))
357  {
358  }
359 };
360 
363 {
364 public:
367  : binary_predicate_exprt(std::move(_src), ID_extractbit, std::move(_index))
368  {
369  }
370 
371  extractbit_exprt(exprt _src, const std::size_t _index);
372 
374  {
375  return op0();
376  }
377 
379  {
380  return op1();
381  }
382 
383  const exprt &src() const
384  {
385  return op0();
386  }
387 
388  const exprt &index() const
389  {
390  return op1();
391  }
392 };
393 
394 template <>
395 inline bool can_cast_expr<extractbit_exprt>(const exprt &base)
396 {
397  return base.id() == ID_extractbit;
398 }
399 
400 inline void validate_expr(const extractbit_exprt &value)
401 {
402  validate_operands(value, 2, "Extract bit must have two operands");
403 }
404 
411 inline const extractbit_exprt &to_extractbit_expr(const exprt &expr)
412 {
413  PRECONDITION(expr.id() == ID_extractbit);
414  const extractbit_exprt &ret = static_cast<const extractbit_exprt &>(expr);
415  validate_expr(ret);
416  return ret;
417 }
418 
421 {
422  PRECONDITION(expr.id() == ID_extractbit);
423  extractbit_exprt &ret = static_cast<extractbit_exprt &>(expr);
424  validate_expr(ret);
425  return ret;
426 }
427 
430 {
431 public:
437  extractbits_exprt(exprt _src, exprt _upper, exprt _lower, typet _type)
438  : expr_protectedt(
439  ID_extractbits,
440  std::move(_type),
441  {std::move(_src), std::move(_upper), std::move(_lower)})
442  {
443  }
444 
446  exprt _src,
447  const std::size_t _upper,
448  const std::size_t _lower,
449  typet _type);
450 
452  {
453  return op0();
454  }
455 
457  {
458  return op1();
459  }
460 
462  {
463  return op2();
464  }
465 
466  const exprt &src() const
467  {
468  return op0();
469  }
470 
471  const exprt &upper() const
472  {
473  return op1();
474  }
475 
476  const exprt &lower() const
477  {
478  return op2();
479  }
480 };
481 
482 template <>
483 inline bool can_cast_expr<extractbits_exprt>(const exprt &base)
484 {
485  return base.id() == ID_extractbits;
486 }
487 
488 inline void validate_expr(const extractbits_exprt &value)
489 {
490  validate_operands(value, 3, "Extract bits must have three operands");
491 }
492 
499 inline const extractbits_exprt &to_extractbits_expr(const exprt &expr)
500 {
501  PRECONDITION(expr.id() == ID_extractbits);
502  const extractbits_exprt &ret = static_cast<const extractbits_exprt &>(expr);
503  validate_expr(ret);
504  return ret;
505 }
506 
509 {
510  PRECONDITION(expr.id() == ID_extractbits);
511  extractbits_exprt &ret = static_cast<extractbits_exprt &>(expr);
512  validate_expr(ret);
513  return ret;
514 }
515 
518 {
519 public:
521  : binary_exprt(
522  std::move(_times),
523  ID_replication,
524  std::move(_src),
525  std::move(_type))
526  {
527  }
528 
530  {
531  return static_cast<constant_exprt &>(op0());
532  }
533 
534  const constant_exprt &times() const
535  {
536  return static_cast<const constant_exprt &>(op0());
537  }
538 
540  {
541  return op1();
542  }
543 
544  const exprt &op() const
545  {
546  return op1();
547  }
548 };
549 
550 template <>
551 inline bool can_cast_expr<replication_exprt>(const exprt &base)
552 {
553  return base.id() == ID_replication;
554 }
555 
556 inline void validate_expr(const replication_exprt &value)
557 {
558  validate_operands(value, 2, "Bit-wise replication must have two operands");
559 }
560 
567 inline const replication_exprt &to_replication_expr(const exprt &expr)
568 {
569  PRECONDITION(expr.id() == ID_replication);
570  const replication_exprt &ret = static_cast<const replication_exprt &>(expr);
571  validate_expr(ret);
572  return ret;
573 }
574 
577 {
578  PRECONDITION(expr.id() == ID_replication);
579  replication_exprt &ret = static_cast<replication_exprt &>(expr);
580  validate_expr(ret);
581  return ret;
582 }
583 
590 {
591 public:
593  : multi_ary_exprt(ID_concatenation, std::move(_operands), std::move(_type))
594  {
595  }
596 
598  : multi_ary_exprt(
599  ID_concatenation,
600  {std::move(_op0), std::move(_op1)},
601  std::move(_type))
602  {
603  }
604 };
605 
606 template <>
608 {
609  return base.id() == ID_concatenation;
610 }
611 
619 {
620  PRECONDITION(expr.id() == ID_concatenation);
621  return static_cast<const concatenation_exprt &>(expr);
622 }
623 
626 {
627  PRECONDITION(expr.id() == ID_concatenation);
628  return static_cast<concatenation_exprt &>(expr);
629 }
630 
633 {
634 public:
636  : unary_exprt(ID_popcount, std::move(_op), std::move(_type))
637  {
638  }
639 
640  explicit popcount_exprt(const exprt &_op)
641  : unary_exprt(ID_popcount, _op, _op.type())
642  {
643  }
644 
647  exprt lower() const;
648 };
649 
650 template <>
651 inline bool can_cast_expr<popcount_exprt>(const exprt &base)
652 {
653  return base.id() == ID_popcount;
654 }
655 
656 inline void validate_expr(const popcount_exprt &value)
657 {
658  validate_operands(value, 1, "popcount must have one operand");
659 }
660 
667 inline const popcount_exprt &to_popcount_expr(const exprt &expr)
668 {
669  PRECONDITION(expr.id() == ID_popcount);
670  const popcount_exprt &ret = static_cast<const popcount_exprt &>(expr);
671  validate_expr(ret);
672  return ret;
673 }
674 
677 {
678  PRECONDITION(expr.id() == ID_popcount);
679  popcount_exprt &ret = static_cast<popcount_exprt &>(expr);
680  validate_expr(ret);
681  return ret;
682 }
683 
687 {
688 public:
689  binary_overflow_exprt(exprt _lhs, const irep_idt &kind, exprt _rhs)
691  std::move(_lhs),
692  "overflow-" + id2string(kind),
693  std::move(_rhs))
694  {
695  }
696 
697  static void check(
698  const exprt &expr,
700  {
701  binary_exprt::check(expr, vm);
702 
703  if(expr.id() != ID_overflow_shl)
704  {
705  const binary_exprt &binary_expr = to_binary_expr(expr);
706  DATA_CHECK(
707  vm,
708  binary_expr.lhs().type() == binary_expr.rhs().type(),
709  "operand types must match");
710  }
711  }
712 
713  static void validate(
714  const exprt &expr,
715  const namespacet &,
717  {
718  check(expr, vm);
719  }
720 };
721 
722 template <>
724 {
725  return base.id() == ID_overflow_plus || base.id() == ID_overflow_mult ||
726  base.id() == ID_overflow_minus || base.id() == ID_overflow_shl;
727 }
728 
729 inline void validate_expr(const binary_overflow_exprt &value)
730 {
732  value, 2, "binary overflow expression must have two operands");
733 }
734 
742 {
743  PRECONDITION(
744  expr.id() == ID_overflow_plus || expr.id() == ID_overflow_mult ||
745  expr.id() == ID_overflow_minus || expr.id() == ID_overflow_shl);
746  const binary_overflow_exprt &ret =
747  static_cast<const binary_overflow_exprt &>(expr);
748  validate_expr(ret);
749  return ret;
750 }
751 
754 {
755  PRECONDITION(
756  expr.id() == ID_overflow_plus || expr.id() == ID_overflow_mult ||
757  expr.id() == ID_overflow_minus || expr.id() == ID_overflow_shl);
758  binary_overflow_exprt &ret = static_cast<binary_overflow_exprt &>(expr);
759  validate_expr(ret);
760  return ret;
761 }
762 
766 {
767 public:
769  : unary_predicate_exprt("overflow-" + id2string(kind), std::move(_op))
770  {
771  }
772 
773  static void check(
774  const exprt &expr,
776  {
777  unary_exprt::check(expr, vm);
778  }
779 
780  static void validate(
781  const exprt &expr,
782  const namespacet &,
784  {
785  check(expr, vm);
786  }
787 };
788 
789 template <>
791 {
792  return base.id() == ID_overflow_unary_minus;
793 }
794 
795 inline void validate_expr(const unary_overflow_exprt &value)
796 {
798  value, 1, "unary overflow expression must have one operand");
799 }
800 
808 {
809  PRECONDITION(expr.id() == ID_overflow_unary_minus);
810  const unary_overflow_exprt &ret =
811  static_cast<const unary_overflow_exprt &>(expr);
812  validate_expr(ret);
813  return ret;
814 }
815 
818 {
819  PRECONDITION(expr.id() == ID_overflow_unary_minus);
820  unary_overflow_exprt &ret = static_cast<unary_overflow_exprt &>(expr);
821  validate_expr(ret);
822  return ret;
823 }
824 
831 {
832 public:
833  count_leading_zeros_exprt(exprt _op, bool _zero_permitted, typet _type)
834  : unary_exprt(ID_count_leading_zeros, std::move(_op), std::move(_type))
835  {
836  zero_permitted(_zero_permitted);
837  }
838 
839  explicit count_leading_zeros_exprt(const exprt &_op)
840  : count_leading_zeros_exprt(_op, true, _op.type())
841  {
842  }
843 
844  bool zero_permitted() const
845  {
846  return !get_bool(ID_C_bounds_check);
847  }
848 
849  void zero_permitted(bool value)
850  {
851  set(ID_C_bounds_check, !value);
852  }
853 
854  static void check(
855  const exprt &expr,
857  {
858  DATA_CHECK(
859  vm,
860  expr.operands().size() == 1,
861  "unary expression must have a single operand");
862  DATA_CHECK(
863  vm,
865  "operand must be of bitvector type");
866  }
867 
868  static void validate(
869  const exprt &expr,
870  const namespacet &,
872  {
873  check(expr, vm);
874  }
875 
878  exprt lower() const;
879 };
880 
881 template <>
883 {
884  return base.id() == ID_count_leading_zeros;
885 }
886 
887 inline void validate_expr(const count_leading_zeros_exprt &value)
888 {
889  validate_operands(value, 1, "count_leading_zeros must have one operand");
890 }
891 
898 inline const count_leading_zeros_exprt &
900 {
901  PRECONDITION(expr.id() == ID_count_leading_zeros);
902  const count_leading_zeros_exprt &ret =
903  static_cast<const count_leading_zeros_exprt &>(expr);
904  validate_expr(ret);
905  return ret;
906 }
907 
910 {
911  PRECONDITION(expr.id() == ID_count_leading_zeros);
913  static_cast<count_leading_zeros_exprt &>(expr);
914  validate_expr(ret);
915  return ret;
916 }
917 
924 {
925 public:
926  count_trailing_zeros_exprt(exprt _op, bool _zero_permitted, typet _type)
927  : unary_exprt(ID_count_trailing_zeros, std::move(_op), std::move(_type))
928  {
929  zero_permitted(_zero_permitted);
930  }
931 
932  explicit count_trailing_zeros_exprt(const exprt &_op)
933  : count_trailing_zeros_exprt(_op, true, _op.type())
934  {
935  }
936 
937  bool zero_permitted() const
938  {
939  return !get_bool(ID_C_bounds_check);
940  }
941 
942  void zero_permitted(bool value)
943  {
944  set(ID_C_bounds_check, !value);
945  }
946 
947  static void check(
948  const exprt &expr,
950  {
951  DATA_CHECK(
952  vm,
953  expr.operands().size() == 1,
954  "unary expression must have a single operand");
955  DATA_CHECK(
956  vm,
958  "operand must be of bitvector type");
959  }
960 
961  static void validate(
962  const exprt &expr,
963  const namespacet &,
965  {
966  check(expr, vm);
967  }
968 
971  exprt lower() const;
972 };
973 
974 template <>
976 {
977  return base.id() == ID_count_trailing_zeros;
978 }
979 
980 inline void validate_expr(const count_trailing_zeros_exprt &value)
981 {
982  validate_operands(value, 1, "count_trailing_zeros must have one operand");
983 }
984 
991 inline const count_trailing_zeros_exprt &
993 {
994  PRECONDITION(expr.id() == ID_count_trailing_zeros);
995  const count_trailing_zeros_exprt &ret =
996  static_cast<const count_trailing_zeros_exprt &>(expr);
997  validate_expr(ret);
998  return ret;
999 }
1000 
1003 {
1004  PRECONDITION(expr.id() == ID_count_trailing_zeros);
1006  static_cast<count_trailing_zeros_exprt &>(expr);
1007  validate_expr(ret);
1008  return ret;
1009 }
1010 
1013 {
1014 public:
1016  : unary_exprt(ID_bitreverse, std::move(op))
1017  {
1018  }
1019 
1022  exprt lower() const;
1023 };
1024 
1025 template <>
1026 inline bool can_cast_expr<bitreverse_exprt>(const exprt &base)
1027 {
1028  return base.id() == ID_bitreverse;
1029 }
1030 
1031 inline void validate_expr(const bitreverse_exprt &value)
1032 {
1033  validate_operands(value, 1, "Bit-wise reverse must have one operand");
1034 }
1035 
1042 inline const bitreverse_exprt &to_bitreverse_expr(const exprt &expr)
1043 {
1044  PRECONDITION(expr.id() == ID_bitreverse);
1045  const bitreverse_exprt &ret = static_cast<const bitreverse_exprt &>(expr);
1046  validate_expr(ret);
1047  return ret;
1048 }
1049 
1052 {
1053  PRECONDITION(expr.id() == ID_bitreverse);
1054  bitreverse_exprt &ret = static_cast<bitreverse_exprt &>(expr);
1055  validate_expr(ret);
1056  return ret;
1057 }
1058 
1059 #endif // CPROVER_UTIL_BITVECTOR_EXPR_H
bool can_cast_expr< count_trailing_zeros_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< 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)
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)
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)
void validate_expr(const bswap_exprt &value)
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast an exprt to an extractbit_exprt.
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.
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< concatenation_exprt >(const exprt &base)
const bitreverse_exprt & to_bitreverse_expr(const exprt &expr)
Cast an exprt to a bitreverse_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.
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)
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< 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.
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:550
exprt & op1()
Definition: expr.h:102
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:562
exprt & lhs()
Definition: std_expr.h:580
exprt & op0()
Definition: expr.h:99
exprt & rhs()
Definition: std_expr.h:590
A Boolean expression returning true, iff operation kind would result in an overflow when applied to o...
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)
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:643
Bit-wise AND.
bitand_exprt(const exprt &_op0, exprt _op1)
Bit-wise negation of bit-vectors.
bitnot_exprt(exprt op)
Bit-wise OR.
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 XOR.
bitxor_exprt(exprt _op0, exprt _op1)
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:2807
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:37
Base class for all expressions.
Definition: expr.h:343
exprt & op1()
Definition: expr.h:102
exprt & op2()
Definition: expr.h:105
exprt & op0()
Definition: expr.h:99
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
static void check(const exprt &, const validation_modet)
Check that the expression is well-formed (shallow checks only, i.e., subexpressions and its type are ...
Definition: expr.h:253
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
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 & lower() const
const exprt & upper() const
extractbits_exprt(exprt _src, exprt _upper, exprt _lower, typet _type)
Extract the bits [_lower .
const exprt & src() const
bool get_bool(const irep_idt &name) const
Definition: irep.cpp:58
std::size_t get_size_t(const irep_idt &name) const
Definition: irep.cpp:68
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:420
void set_size_t(const irep_idt &name, const std::size_t value)
Definition: irep.cpp:87
const irep_idt & id() const
Definition: irep.h:396
Logical right shift.
lshr_exprt(exprt _src, const std::size_t _distance)
lshr_exprt(exprt _src, exprt _distance)
A base class for multi-ary expressions Associativity is not specified.
Definition: std_expr.h:824
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
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)
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)
The type of an expression, extends irept.
Definition: type.h:29
Generic base class for unary expressions.
Definition: std_expr.h:281
const exprt & op() const
Definition: std_expr.h:293
A Boolean expression returning true, iff operation kind would result in an overflow when applied to t...
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:495
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:47
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
API to expression classes.
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:627
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:328
bool can_cast_type< bitvector_typet >(const typet &type)
Check whether a reference to a typet is a bitvector_typet.
Definition: std_types.h:887
#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