cprover
Loading...
Searching...
No Matches
bitvector_expr.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: API to expression classes for bitvectors
4
5Author: 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
19{
20public:
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
44template <>
45inline bool can_cast_expr<bswap_exprt>(const exprt &base)
46{
47 return base.id() == ID_bswap;
48}
49
50inline 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
63inline 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
82{
83public:
84 explicit bitnot_exprt(exprt op) : unary_exprt(ID_bitnot, std::move(op))
85 {
86 }
87};
88
89template <>
90inline bool can_cast_expr<bitnot_exprt>(const exprt &base)
91{
92 return base.id() == ID_bitnot;
93}
94
95inline void validate_expr(const bitnot_exprt &value)
96{
97 validate_operands(value, 1, "Bit-wise not must have one operand");
98}
99
106inline 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{
126public:
127 bitor_exprt(const exprt &_op0, exprt _op1)
128 : multi_ary_exprt(_op0, ID_bitor, std::move(_op1), _op0.type())
129 {
130 }
131};
132
133template <>
134inline bool can_cast_expr<bitor_exprt>(const exprt &base)
135{
136 return base.id() == ID_bitor;
137}
138
145inline 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{
161public:
163 : multi_ary_exprt(std::move(_op0), ID_bitxor, std::move(_op1))
164 {
165 }
166};
167
168template <>
169inline bool can_cast_expr<bitxor_exprt>(const exprt &base)
170{
171 return base.id() == ID_bitxor;
172}
173
180inline 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{
196public:
197 bitand_exprt(const exprt &_op0, exprt _op1)
198 : multi_ary_exprt(_op0, ID_bitand, std::move(_op1), _op0.type())
199 {
200 }
201};
202
203template <>
204inline bool can_cast_expr<bitand_exprt>(const exprt &base)
205{
206 return base.id() == ID_bitand;
207}
208
215inline 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
230{
231public:
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
260template <>
261inline 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
267inline void validate_expr(const shift_exprt &value)
268{
269 validate_operands(value, 2, "Shifts must have two operands");
270}
271
278inline 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
294class shl_exprt : public shift_exprt
295{
296public:
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
308template <>
309inline bool can_cast_expr<shl_exprt>(const exprt &base)
310{
311 return base.id() == ID_shl;
312}
313
320inline const shl_exprt &to_shl_expr(const exprt &expr)
321{
322 PRECONDITION(expr.id() == ID_shl);
323 const shl_exprt &ret = static_cast<const shl_exprt &>(expr);
324 validate_expr(ret);
325 return ret;
326}
327
330{
331 PRECONDITION(expr.id() == ID_shl);
332 shl_exprt &ret = static_cast<shl_exprt &>(expr);
333 validate_expr(ret);
334 return ret;
335}
336
339{
340public:
341 ashr_exprt(exprt _src, exprt _distance)
342 : shift_exprt(std::move(_src), ID_ashr, std::move(_distance))
343 {
344 }
345
346 ashr_exprt(exprt _src, const std::size_t _distance)
347 : shift_exprt(std::move(_src), ID_ashr, _distance)
348 {
349 }
350};
351
352template <>
353inline bool can_cast_expr<ashr_exprt>(const exprt &base)
354{
355 return base.id() == ID_ashr;
356}
357
360{
361public:
362 lshr_exprt(exprt _src, exprt _distance)
363 : shift_exprt(std::move(_src), ID_lshr, std::move(_distance))
364 {
365 }
366
367 lshr_exprt(exprt _src, const std::size_t _distance)
368 : shift_exprt(std::move(_src), ID_lshr, std::move(_distance))
369 {
370 }
371};
372
373template <>
374inline bool can_cast_expr<lshr_exprt>(const exprt &base)
375{
376 return base.id() == ID_lshr;
377}
378
381{
382public:
385 : binary_predicate_exprt(std::move(_src), ID_extractbit, std::move(_index))
386 {
387 }
388
389 extractbit_exprt(exprt _src, const std::size_t _index);
390
392 {
393 return op0();
394 }
395
397 {
398 return op1();
399 }
400
401 const exprt &src() const
402 {
403 return op0();
404 }
405
406 const exprt &index() const
407 {
408 return op1();
409 }
410};
411
412template <>
414{
415 return base.id() == ID_extractbit;
416}
417
418inline void validate_expr(const extractbit_exprt &value)
419{
420 validate_operands(value, 2, "Extract bit must have two operands");
421}
422
429inline const extractbit_exprt &to_extractbit_expr(const exprt &expr)
430{
431 PRECONDITION(expr.id() == ID_extractbit);
432 const extractbit_exprt &ret = static_cast<const extractbit_exprt &>(expr);
433 validate_expr(ret);
434 return ret;
435}
436
439{
440 PRECONDITION(expr.id() == ID_extractbit);
441 extractbit_exprt &ret = static_cast<extractbit_exprt &>(expr);
442 validate_expr(ret);
443 return ret;
444}
445
448{
449public:
455 extractbits_exprt(exprt _src, exprt _index, typet _type)
457 ID_extractbits,
458 std::move(_type),
459 {std::move(_src), std::move(_index)})
460 {
461 }
462
463 extractbits_exprt(exprt _src, const std::size_t _index, typet _type);
464
466 {
467 return op0();
468 }
469
471 {
472 return op1();
473 }
474
475 const exprt &src() const
476 {
477 return op0();
478 }
479
480 const exprt &index() const
481 {
482 return op1();
483 }
484};
485
486template <>
488{
489 return base.id() == ID_extractbits;
490}
491
492inline void validate_expr(const extractbits_exprt &value)
493{
494 validate_operands(value, 2, "Extractbits must have two operands");
495}
496
504{
505 PRECONDITION(expr.id() == ID_extractbits);
506 const extractbits_exprt &ret = static_cast<const extractbits_exprt &>(expr);
507 validate_expr(ret);
508 return ret;
509}
510
513{
514 PRECONDITION(expr.id() == ID_extractbits);
515 extractbits_exprt &ret = static_cast<extractbits_exprt &>(expr);
516 validate_expr(ret);
517 return ret;
518}
519
522{
523public:
528 update_bit_exprt(exprt _src, exprt _index, exprt _new_value)
530 ID_update_bit,
531 _src.type(),
532 {_src, std::move(_index), std::move(_new_value)})
533 {
534 PRECONDITION(new_value().type().id() == ID_bool);
535 }
536
537 update_bit_exprt(exprt _src, const std::size_t _index, exprt _new_value);
538
540 {
541 return op0();
542 }
543
545 {
546 return op1();
547 }
548
550 {
551 return op2();
552 }
553
554 const exprt &src() const
555 {
556 return op0();
557 }
558
559 const exprt &index() const
560 {
561 return op1();
562 }
563
564 const exprt &new_value() const
565 {
566 return op2();
567 }
568
569 static void check(
570 const exprt &expr,
572 {
573 validate_operands(expr, 3, "update_bit must have three operands");
574 }
575
577 exprt lower() const;
578};
579
580template <>
582{
583 return base.id() == ID_update_bit;
584}
585
592inline const update_bit_exprt &to_update_bit_expr(const exprt &expr)
593{
594 PRECONDITION(expr.id() == ID_update_bit);
596 return static_cast<const update_bit_exprt &>(expr);
597}
598
601{
602 PRECONDITION(expr.id() == ID_update_bit);
604 return static_cast<update_bit_exprt &>(expr);
605}
606
609{
610public:
615 update_bits_exprt(exprt _src, exprt _index, exprt _new_value)
617 ID_update_bits,
618 _src.type(),
619 {_src, std::move(_index), std::move(_new_value)})
620 {
621 }
622
623 update_bits_exprt(exprt _src, const std::size_t _index, exprt _new_value);
624
626 {
627 return op0();
628 }
629
631 {
632 return op1();
633 }
634
636 {
637 return op2();
638 }
639
640 const exprt &src() const
641 {
642 return op0();
643 }
644
645 const exprt &index() const
646 {
647 return op1();
648 }
649
650 const exprt &new_value() const
651 {
652 return op2();
653 }
654
655 static void check(
656 const exprt &expr,
658 {
659 validate_operands(expr, 3, "update_bits must have three operands");
660 }
661
663 exprt lower() const;
664};
665
666template <>
668{
669 return base.id() == ID_update_bits;
670}
671
679{
680 PRECONDITION(expr.id() == ID_update_bits);
682 return static_cast<const update_bits_exprt &>(expr);
683}
684
687{
688 PRECONDITION(expr.id() == ID_update_bits);
690 return static_cast<update_bits_exprt &>(expr);
691}
692
695{
696public:
698 : binary_exprt(
699 std::move(_times),
700 ID_replication,
701 std::move(_src),
702 std::move(_type))
703 {
704 }
705
707 {
708 return static_cast<constant_exprt &>(op0());
709 }
710
711 const constant_exprt &times() const
712 {
713 return static_cast<const constant_exprt &>(op0());
714 }
715
717 {
718 return op1();
719 }
720
721 const exprt &op() const
722 {
723 return op1();
724 }
725};
726
727template <>
729{
730 return base.id() == ID_replication;
731}
732
733inline void validate_expr(const replication_exprt &value)
734{
735 validate_operands(value, 2, "Bit-wise replication must have two operands");
736}
737
745{
746 PRECONDITION(expr.id() == ID_replication);
747 const replication_exprt &ret = static_cast<const replication_exprt &>(expr);
748 validate_expr(ret);
749 return ret;
750}
751
754{
755 PRECONDITION(expr.id() == ID_replication);
756 replication_exprt &ret = static_cast<replication_exprt &>(expr);
757 validate_expr(ret);
758 return ret;
759}
760
767{
768public:
770 : multi_ary_exprt(ID_concatenation, std::move(_operands), std::move(_type))
771 {
772 }
773
776 ID_concatenation,
777 {std::move(_op0), std::move(_op1)},
778 std::move(_type))
779 {
780 }
781};
782
783template <>
785{
786 return base.id() == ID_concatenation;
787}
788
796{
797 PRECONDITION(expr.id() == ID_concatenation);
798 return static_cast<const concatenation_exprt &>(expr);
799}
800
803{
804 PRECONDITION(expr.id() == ID_concatenation);
805 return static_cast<concatenation_exprt &>(expr);
806}
807
810{
811public:
813 : unary_exprt(ID_popcount, std::move(_op), std::move(_type))
814 {
815 }
816
817 explicit popcount_exprt(const exprt &_op)
818 : unary_exprt(ID_popcount, _op, _op.type())
819 {
820 }
821
824 exprt lower() const;
825};
826
827template <>
828inline bool can_cast_expr<popcount_exprt>(const exprt &base)
829{
830 return base.id() == ID_popcount;
831}
832
833inline void validate_expr(const popcount_exprt &value)
834{
835 validate_operands(value, 1, "popcount must have one operand");
836}
837
844inline const popcount_exprt &to_popcount_expr(const exprt &expr)
845{
846 PRECONDITION(expr.id() == ID_popcount);
847 const popcount_exprt &ret = static_cast<const popcount_exprt &>(expr);
848 validate_expr(ret);
849 return ret;
850}
851
854{
855 PRECONDITION(expr.id() == ID_popcount);
856 popcount_exprt &ret = static_cast<popcount_exprt &>(expr);
857 validate_expr(ret);
858 return ret;
859}
860
864{
865public:
866 binary_overflow_exprt(exprt _lhs, const irep_idt &kind, exprt _rhs)
867 : binary_predicate_exprt(std::move(_lhs), make_id(kind), std::move(_rhs))
868 {
869 INVARIANT(
870 valid_id(id()),
871 "The kind used to construct binary_overflow_exprt should be in the set "
872 "of expected valid kinds.");
873 }
874
875 static void check(
876 const exprt &expr,
878 {
879 binary_exprt::check(expr, vm);
880
881 if(expr.id() != ID_overflow_shl)
882 {
883 const binary_exprt &binary_expr = to_binary_expr(expr);
885 vm,
886 binary_expr.lhs().type() == binary_expr.rhs().type(),
887 "operand types must match");
888 }
889 }
890
891 static void validate(
892 const exprt &expr,
893 const namespacet &,
895 {
896 check(expr, vm);
897 }
898
900 static bool valid_id(const irep_idt &id)
901 {
902 return id == ID_overflow_plus || id == ID_overflow_mult ||
903 id == ID_overflow_minus || id == ID_overflow_shl;
904 }
905
906private:
907 static irep_idt make_id(const irep_idt &kind)
908 {
909 if(valid_id(kind))
910 return kind;
911 else
912 return "overflow-" + id2string(kind);
913 }
914};
915
916template <>
918{
919 return binary_overflow_exprt::valid_id(base.id());
920}
921
922inline void validate_expr(const binary_overflow_exprt &value)
923{
925 value, 2, "binary overflow expression must have two operands");
926}
927
935{
937 expr.id() == ID_overflow_plus || expr.id() == ID_overflow_mult ||
938 expr.id() == ID_overflow_minus || expr.id() == ID_overflow_shl);
939 const binary_overflow_exprt &ret =
940 static_cast<const binary_overflow_exprt &>(expr);
941 validate_expr(ret);
942 return ret;
943}
944
947{
949 expr.id() == ID_overflow_plus || expr.id() == ID_overflow_mult ||
950 expr.id() == ID_overflow_minus || expr.id() == ID_overflow_shl);
951 binary_overflow_exprt &ret = static_cast<binary_overflow_exprt &>(expr);
952 validate_expr(ret);
953 return ret;
954}
955
957{
958public:
960 : binary_overflow_exprt(std::move(_lhs), ID_overflow_plus, std::move(_rhs))
961 {
962 }
963
966 exprt lower() const;
967};
968
969template <>
971{
972 return base.id() == ID_overflow_plus;
973}
974
976{
977public:
979 : binary_overflow_exprt(std::move(_lhs), ID_overflow_minus, std::move(_rhs))
980 {
981 }
982
985 exprt lower() const;
986};
987
988template <>
990{
991 return base.id() == ID_overflow_minus;
992}
993
995{
996public:
998 : binary_overflow_exprt(std::move(_lhs), ID_overflow_mult, std::move(_rhs))
999 {
1000 }
1001
1004 exprt lower() const;
1005};
1006
1007template <>
1009{
1010 return base.id() == ID_overflow_mult;
1011}
1012
1014{
1015public:
1017 : binary_overflow_exprt(std::move(_lhs), ID_overflow_shl, std::move(_rhs))
1018 {
1019 }
1020};
1021
1022template <>
1024{
1025 return base.id() == ID_overflow_shl;
1026}
1027
1031{
1032public:
1034 : unary_predicate_exprt("overflow-" + id2string(kind), std::move(_op))
1035 {
1036 }
1037
1038 static void check(
1039 const exprt &expr,
1041 {
1042 unary_exprt::check(expr, vm);
1043 }
1044
1045 static void validate(
1046 const exprt &expr,
1047 const namespacet &,
1049 {
1050 check(expr, vm);
1051 }
1052};
1053
1054template <>
1056{
1057 return base.id() == ID_overflow_unary_minus;
1058}
1059
1060inline void validate_expr(const unary_overflow_exprt &value)
1061{
1063 value, 1, "unary overflow expression must have one operand");
1064}
1065
1069{
1070public:
1072 : unary_overflow_exprt(ID_unary_minus, std::move(_op))
1073 {
1074 }
1075
1076 static void check(
1077 const exprt &expr,
1079 {
1080 unary_exprt::check(expr, vm);
1081 }
1082
1083 static void validate(
1084 const exprt &expr,
1085 const namespacet &,
1087 {
1088 check(expr, vm);
1089 }
1090};
1091
1092template <>
1094{
1095 return base.id() == ID_overflow_unary_minus;
1096}
1097
1099{
1101 value, 1, "unary minus overflow expression must have one operand");
1102}
1103
1111{
1112 PRECONDITION(expr.id() == ID_overflow_unary_minus);
1113 const unary_overflow_exprt &ret =
1114 static_cast<const unary_overflow_exprt &>(expr);
1115 validate_expr(ret);
1116 return ret;
1117}
1118
1121{
1122 PRECONDITION(expr.id() == ID_overflow_unary_minus);
1123 unary_overflow_exprt &ret = static_cast<unary_overflow_exprt &>(expr);
1124 validate_expr(ret);
1125 return ret;
1126}
1127
1134{
1135public:
1136 count_leading_zeros_exprt(exprt _op, bool _zero_permitted, typet _type)
1137 : unary_exprt(ID_count_leading_zeros, std::move(_op), std::move(_type))
1138 {
1139 zero_permitted(_zero_permitted);
1140 }
1141
1143 : count_leading_zeros_exprt(_op, true, _op.type())
1144 {
1145 }
1146
1147 bool zero_permitted() const
1148 {
1149 return !get_bool(ID_C_bounds_check);
1150 }
1151
1152 void zero_permitted(bool value)
1153 {
1154 set(ID_C_bounds_check, !value);
1155 }
1156
1157 static void check(
1158 const exprt &expr,
1160 {
1161 DATA_CHECK(
1162 vm,
1163 expr.operands().size() == 1,
1164 "unary expression must have a single operand");
1165 DATA_CHECK(
1166 vm,
1168 "operand must be of bitvector type");
1169 }
1170
1171 static void validate(
1172 const exprt &expr,
1173 const namespacet &,
1175 {
1176 check(expr, vm);
1177 }
1178
1181 exprt lower() const;
1182};
1183
1184template <>
1186{
1187 return base.id() == ID_count_leading_zeros;
1188}
1189
1191{
1192 validate_operands(value, 1, "count_leading_zeros must have one operand");
1193}
1194
1201inline const count_leading_zeros_exprt &
1203{
1204 PRECONDITION(expr.id() == ID_count_leading_zeros);
1205 const count_leading_zeros_exprt &ret =
1206 static_cast<const count_leading_zeros_exprt &>(expr);
1207 validate_expr(ret);
1208 return ret;
1209}
1210
1213{
1214 PRECONDITION(expr.id() == ID_count_leading_zeros);
1216 static_cast<count_leading_zeros_exprt &>(expr);
1217 validate_expr(ret);
1218 return ret;
1219}
1220
1227{
1228public:
1229 count_trailing_zeros_exprt(exprt _op, bool _zero_permitted, typet _type)
1230 : unary_exprt(ID_count_trailing_zeros, std::move(_op), std::move(_type))
1231 {
1232 zero_permitted(_zero_permitted);
1233 }
1234
1236 : count_trailing_zeros_exprt(_op, true, _op.type())
1237 {
1238 }
1239
1240 bool zero_permitted() const
1241 {
1242 return !get_bool(ID_C_bounds_check);
1243 }
1244
1245 void zero_permitted(bool value)
1246 {
1247 set(ID_C_bounds_check, !value);
1248 }
1249
1250 static void check(
1251 const exprt &expr,
1253 {
1254 DATA_CHECK(
1255 vm,
1256 expr.operands().size() == 1,
1257 "unary expression must have a single operand");
1258 DATA_CHECK(
1259 vm,
1261 "operand must be of bitvector type");
1262 }
1263
1264 static void validate(
1265 const exprt &expr,
1266 const namespacet &,
1268 {
1269 check(expr, vm);
1270 }
1271
1274 exprt lower() const;
1275};
1276
1277template <>
1279{
1280 return base.id() == ID_count_trailing_zeros;
1281}
1282
1284{
1285 validate_operands(value, 1, "count_trailing_zeros must have one operand");
1286}
1287
1294inline const count_trailing_zeros_exprt &
1296{
1297 PRECONDITION(expr.id() == ID_count_trailing_zeros);
1298 const count_trailing_zeros_exprt &ret =
1299 static_cast<const count_trailing_zeros_exprt &>(expr);
1300 validate_expr(ret);
1301 return ret;
1302}
1303
1306{
1307 PRECONDITION(expr.id() == ID_count_trailing_zeros);
1309 static_cast<count_trailing_zeros_exprt &>(expr);
1310 validate_expr(ret);
1311 return ret;
1312}
1313
1316{
1317public:
1319 : unary_exprt(ID_bitreverse, std::move(op))
1320 {
1321 }
1322
1325 exprt lower() const;
1326};
1327
1328template <>
1330{
1331 return base.id() == ID_bitreverse;
1332}
1333
1334inline void validate_expr(const bitreverse_exprt &value)
1335{
1336 validate_operands(value, 1, "Bit-wise reverse must have one operand");
1337}
1338
1346{
1347 PRECONDITION(expr.id() == ID_bitreverse);
1348 const bitreverse_exprt &ret = static_cast<const bitreverse_exprt &>(expr);
1349 validate_expr(ret);
1350 return ret;
1351}
1352
1355{
1356 PRECONDITION(expr.id() == ID_bitreverse);
1357 bitreverse_exprt &ret = static_cast<bitreverse_exprt &>(expr);
1358 validate_expr(ret);
1359 return ret;
1360}
1361
1364{
1365public:
1367 : binary_exprt(std::move(_lhs), ID_saturating_plus, std::move(_rhs))
1368 {
1369 }
1370
1372 : binary_exprt(
1373 std::move(_lhs),
1374 ID_saturating_plus,
1375 std::move(_rhs),
1376 std::move(_type))
1377 {
1378 }
1379};
1380
1381template <>
1383{
1384 return base.id() == ID_saturating_plus;
1385}
1386
1387inline void validate_expr(const saturating_plus_exprt &value)
1388{
1389 validate_operands(value, 2, "saturating plus must have two operands");
1390}
1391
1399{
1400 PRECONDITION(expr.id() == ID_saturating_plus);
1401 const saturating_plus_exprt &ret =
1402 static_cast<const saturating_plus_exprt &>(expr);
1403 validate_expr(ret);
1404 return ret;
1405}
1406
1409{
1410 PRECONDITION(expr.id() == ID_saturating_plus);
1411 saturating_plus_exprt &ret = static_cast<saturating_plus_exprt &>(expr);
1412 validate_expr(ret);
1413 return ret;
1414}
1415
1418{
1419public:
1421 : binary_exprt(std::move(_lhs), ID_saturating_minus, std::move(_rhs))
1422 {
1423 }
1424};
1425
1426template <>
1428{
1429 return base.id() == ID_saturating_minus;
1430}
1431
1432inline void validate_expr(const saturating_minus_exprt &value)
1433{
1434 validate_operands(value, 2, "saturating minus must have two operands");
1435}
1436
1444{
1445 PRECONDITION(expr.id() == ID_saturating_minus);
1446 const saturating_minus_exprt &ret =
1447 static_cast<const saturating_minus_exprt &>(expr);
1448 validate_expr(ret);
1449 return ret;
1450}
1451
1454{
1455 PRECONDITION(expr.id() == ID_saturating_minus);
1456 saturating_minus_exprt &ret = static_cast<saturating_minus_exprt &>(expr);
1457 validate_expr(ret);
1458 return ret;
1459}
1460
1464{
1465public:
1468 make_id(kind),
1470 {{ID_value, _lhs.type()},
1471 {"overflow-" + id2string(kind), bool_typet{}}}},
1472 {_lhs, std::move(_rhs)})
1473 {
1474 INVARIANT(
1475 valid_id(id()),
1476 "The kind used to construct overflow_result_exprt should be in the set "
1477 "of expected valid kinds.");
1478 }
1479
1482 make_id(kind),
1484 {{ID_value, _op.type()},
1485 {"overflow-" + id2string(kind), bool_typet{}}}},
1486 {_op})
1487 {
1488 INVARIANT(
1489 valid_id(id()),
1490 "The kind used to construct overflow_result_exprt should be in the set "
1491 "of expected valid kinds.");
1492 }
1493
1494 // make op0 and op1 public
1495 using exprt::op0;
1496 using exprt::op1;
1497
1498 const exprt &op2() const = delete;
1499 exprt &op2() = delete;
1500 const exprt &op3() const = delete;
1501 exprt &op3() = delete;
1502
1503 static void check(
1504 const exprt &expr,
1506 {
1507 if(expr.id() != ID_overflow_result_unary_minus)
1508 binary_exprt::check(expr, vm);
1509
1510 if(
1511 expr.id() != ID_overflow_result_unary_minus &&
1512 expr.id() != ID_overflow_result_shl)
1513 {
1514 const binary_exprt &binary_expr = to_binary_expr(expr);
1515 DATA_CHECK(
1516 vm,
1517 binary_expr.lhs().type() == binary_expr.rhs().type(),
1518 "operand types must match");
1519 }
1520 }
1521
1522 static void validate(
1523 const exprt &expr,
1524 const namespacet &,
1526 {
1527 check(expr, vm);
1528 }
1529
1531 static bool valid_id(const irep_idt &id)
1532 {
1533 return id == ID_overflow_result_plus || id == ID_overflow_result_mult ||
1534 id == ID_overflow_result_minus || id == ID_overflow_result_shl ||
1535 id == ID_overflow_result_unary_minus;
1536 }
1537
1538private:
1539 static irep_idt make_id(const irep_idt &kind)
1540 {
1541 return "overflow_result-" + id2string(kind);
1542 }
1543};
1544
1545template <>
1547{
1548 return overflow_result_exprt::valid_id(base.id());
1549}
1550
1551inline void validate_expr(const overflow_result_exprt &value)
1552{
1553 if(value.id() == ID_overflow_result_unary_minus)
1554 {
1556 value, 1, "unary overflow expression must have two operands");
1557 }
1558 else
1559 {
1561 value, 2, "binary overflow expression must have two operands");
1562 }
1563}
1564
1572{
1574 const overflow_result_exprt &ret =
1575 static_cast<const overflow_result_exprt &>(expr);
1576 validate_expr(ret);
1577 return ret;
1578}
1579
1582{
1584 overflow_result_exprt &ret = static_cast<overflow_result_exprt &>(expr);
1585 validate_expr(ret);
1586 return ret;
1587}
1588
1592{
1593public:
1595 : unary_exprt(ID_find_first_set, std::move(_op), std::move(_type))
1596 {
1597 }
1598
1599 explicit find_first_set_exprt(const exprt &_op)
1600 : find_first_set_exprt(_op, _op.type())
1601 {
1602 }
1603
1604 static void check(
1605 const exprt &expr,
1607 {
1608 DATA_CHECK(
1609 vm,
1610 expr.operands().size() == 1,
1611 "unary expression must have a single operand");
1612 DATA_CHECK(
1613 vm,
1615 "operand must be of bitvector type");
1616 }
1617
1618 static void validate(
1619 const exprt &expr,
1620 const namespacet &,
1622 {
1623 check(expr, vm);
1624 }
1625
1628 exprt lower() const;
1629};
1630
1631template <>
1633{
1634 return base.id() == ID_find_first_set;
1635}
1636
1637inline void validate_expr(const find_first_set_exprt &value)
1638{
1639 validate_operands(value, 1, "find_first_set must have one operand");
1640}
1641
1649{
1650 PRECONDITION(expr.id() == ID_find_first_set);
1651 const find_first_set_exprt &ret =
1652 static_cast<const find_first_set_exprt &>(expr);
1653 validate_expr(ret);
1654 return ret;
1655}
1656
1659{
1660 PRECONDITION(expr.id() == ID_find_first_set);
1661 find_first_set_exprt &ret = static_cast<find_first_set_exprt &>(expr);
1662 validate_expr(ret);
1663 return ret;
1664}
1665
1666#endif // CPROVER_UTIL_BITVECTOR_EXPR_H
bool can_cast_expr< count_trailing_zeros_exprt >(const exprt &base)
const saturating_minus_exprt & to_saturating_minus_expr(const exprt &expr)
Cast an exprt to a saturating_minus_exprt.
const replication_exprt & to_replication_expr(const exprt &expr)
Cast an exprt to a replication_exprt.
const saturating_plus_exprt & to_saturating_plus_expr(const exprt &expr)
Cast an exprt to a saturating_plus_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)
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
bool can_cast_expr< find_first_set_exprt >(const exprt &base)
bool can_cast_expr< saturating_plus_exprt >(const exprt &base)
const shl_exprt & to_shl_expr(const exprt &expr)
Cast an exprt to a shl_exprt.
bool can_cast_expr< bitreverse_exprt >(const exprt &base)
bool can_cast_expr< count_leading_zeros_exprt >(const exprt &base)
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.
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 extractbits_exprt & to_extractbits_expr(const exprt &expr)
Cast an exprt to an extractbits_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 binary_overflow_exprt & to_binary_overflow_expr(const exprt &expr)
Cast an exprt to a binary_overflow_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 find_first_set_exprt & to_find_first_set_expr(const exprt &expr)
Cast an exprt to a find_first_set_exprt.
bool can_cast_expr< ashr_exprt >(const exprt &base)
bool can_cast_expr< shl_overflow_exprt >(const exprt &base)
const bitor_exprt & to_bitor_expr(const exprt &expr)
Cast an exprt to a bitor_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)
const update_bit_exprt & to_update_bit_expr(const exprt &expr)
Cast an exprt to an update_bit_exprt.
const bitnot_exprt & to_bitnot_expr(const exprt &expr)
Cast an exprt to a bitnot_exprt.
const unary_overflow_exprt & to_unary_overflow_expr(const exprt &expr)
Cast an exprt to a unary_overflow_exprt.
bool can_cast_expr< concatenation_exprt >(const exprt &base)
bool can_cast_expr< unary_overflow_exprt >(const exprt &base)
const overflow_result_exprt & to_overflow_result_expr(const exprt &expr)
Cast an exprt to a overflow_result_exprt.
bool can_cast_expr< lshr_exprt >(const exprt &base)
bool can_cast_expr< shl_exprt >(const exprt &base)
const bitxor_exprt & to_bitxor_expr(const exprt &expr)
Cast an exprt to a bitxor_exprt.
const bswap_exprt & to_bswap_expr(const exprt &expr)
Cast an exprt to a bswap_exprt.
bool can_cast_expr< plus_overflow_exprt >(const exprt &base)
const count_leading_zeros_exprt & to_count_leading_zeros_expr(const exprt &expr)
Cast an exprt to a count_leading_zeros_exprt.
bool can_cast_expr< bitnot_exprt >(const exprt &base)
bool can_cast_expr< binary_overflow_exprt >(const exprt &base)
const bitreverse_exprt & to_bitreverse_expr(const exprt &expr)
Cast an exprt to a bitreverse_exprt.
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast an exprt to an extractbit_exprt.
bool can_cast_expr< unary_minus_overflow_exprt >(const exprt &base)
bool can_cast_expr< extractbit_exprt >(const exprt &base)
const concatenation_exprt & to_concatenation_expr(const exprt &expr)
Cast an exprt to a concatenation_exprt.
const count_trailing_zeros_exprt & to_count_trailing_zeros_expr(const exprt &expr)
Cast an exprt to a count_trailing_zeros_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 & lhs()
Definition std_expr.h:668
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:650
exprt & rhs()
Definition std_expr.h:678
exprt & op0()
Definition expr.h:133
exprt & op1()
Definition expr.h:136
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(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 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:2987
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 & op0()
Definition expr.h:133
exprt & op1()
Definition expr.h:136
exprt & op2()
Definition expr.h:139
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
exprt & op0()
Definition expr.h:133
exprt & op1()
Definition expr.h:136
typet & type()
Return the type of the expression.
Definition expr.h:84
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 & index() const
const exprt & src() 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
An expression returning both the result of the arithmetic operation under wrap-around semantics as we...
exprt & op3()=delete
overflow_result_exprt(exprt _lhs, const irep_idt &kind, exprt _rhs)
overflow_result_exprt(exprt _op, const irep_idt &kind)
static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
exprt & op2()=delete
static bool valid_id(const irep_idt &id)
Returns true iff id is a valid identifier of an overflow_exprt.
const exprt & op2() const =delete
static irep_idt make_id(const irep_idt &kind)
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
const exprt & op3() const =delete
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()
shift_exprt(exprt _src, const irep_idt &_id, exprt _distance)
const exprt & distance() const
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 & src() const
const exprt & index() 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.
exprt lower() const
A lowering to masking, shifting, or.
const exprt & new_value() const
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
update_bit_exprt(exprt _src, const std::size_t _index, exprt _new_value)
Replaces a sub-range of a bit-vector operand.
const exprt & index() const
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
update_bits_exprt(exprt _src, exprt _index, exprt _new_value)
Replace the bits [_index .
const exprt & new_value() const
exprt lower() const
A lowering to masking, shifting, or.
const exprt & src() const
update_bits_exprt(exprt _src, const std::size_t _index, exprt _new_value)
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
STL namespace.
#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:943
#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