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:
198 : multi_ary_exprt(std::move(_op0), ID_bitxnor, std::move(_op1))
199 {
200 }
201};
202
203template <>
204inline bool can_cast_expr<bitxnor_exprt>(const exprt &base)
205{
206 return base.id() == ID_bitxnor;
207}
208
215inline const bitxnor_exprt &to_bitxnor_expr(const exprt &expr)
216{
217 PRECONDITION(expr.id() == ID_bitxnor);
218 return static_cast<const bitxnor_exprt &>(expr);
219}
220
223{
224 PRECONDITION(expr.id() == ID_bitxnor);
225 return static_cast<bitxnor_exprt &>(expr);
226}
227
230{
231public:
232 bitand_exprt(const exprt &_op0, exprt _op1)
233 : multi_ary_exprt(_op0, ID_bitand, std::move(_op1), _op0.type())
234 {
235 }
236};
237
238template <>
239inline bool can_cast_expr<bitand_exprt>(const exprt &base)
240{
241 return base.id() == ID_bitand;
242}
243
250inline const bitand_exprt &to_bitand_expr(const exprt &expr)
251{
252 PRECONDITION(expr.id() == ID_bitand);
253 return static_cast<const bitand_exprt &>(expr);
254}
255
258{
259 PRECONDITION(expr.id() == ID_bitand);
260 return static_cast<bitand_exprt &>(expr);
261}
262
265{
266public:
267 shift_exprt(exprt _src, const irep_idt &_id, exprt _distance)
268 : binary_exprt(std::move(_src), _id, std::move(_distance))
269 {
270 }
271
272 shift_exprt(exprt _src, const irep_idt &_id, const std::size_t _distance);
273
275 {
276 return op0();
277 }
278
279 const exprt &op() const
280 {
281 return op0();
282 }
283
285 {
286 return op1();
287 }
288
289 const exprt &distance() const
290 {
291 return op1();
292 }
293};
294
295template <>
296inline bool can_cast_expr<shift_exprt>(const exprt &base)
297{
298 return base.id() == ID_shl || base.id() == ID_ashr || base.id() == ID_lshr ||
299 base.id() == ID_ror || base.id() == ID_rol;
300}
301
302inline void validate_expr(const shift_exprt &value)
303{
304 validate_operands(value, 2, "Shifts must have two operands");
305}
306
313inline const shift_exprt &to_shift_expr(const exprt &expr)
314{
315 const shift_exprt &ret = static_cast<const shift_exprt &>(expr);
316 validate_expr(ret);
317 return ret;
318}
319
322{
323 shift_exprt &ret = static_cast<shift_exprt &>(expr);
324 validate_expr(ret);
325 return ret;
326}
327
329class shl_exprt : public shift_exprt
330{
331public:
332 shl_exprt(exprt _src, exprt _distance)
333 : shift_exprt(std::move(_src), ID_shl, std::move(_distance))
334 {
335 }
336
337 shl_exprt(exprt _src, const std::size_t _distance)
338 : shift_exprt(std::move(_src), ID_shl, _distance)
339 {
340 }
341};
342
343template <>
344inline bool can_cast_expr<shl_exprt>(const exprt &base)
345{
346 return base.id() == ID_shl;
347}
348
355inline const shl_exprt &to_shl_expr(const exprt &expr)
356{
357 PRECONDITION(expr.id() == ID_shl);
358 const shl_exprt &ret = static_cast<const shl_exprt &>(expr);
359 validate_expr(ret);
360 return ret;
361}
362
365{
366 PRECONDITION(expr.id() == ID_shl);
367 shl_exprt &ret = static_cast<shl_exprt &>(expr);
368 validate_expr(ret);
369 return ret;
370}
371
374{
375public:
376 ashr_exprt(exprt _src, exprt _distance)
377 : shift_exprt(std::move(_src), ID_ashr, std::move(_distance))
378 {
379 }
380
381 ashr_exprt(exprt _src, const std::size_t _distance)
382 : shift_exprt(std::move(_src), ID_ashr, _distance)
383 {
384 }
385};
386
387template <>
388inline bool can_cast_expr<ashr_exprt>(const exprt &base)
389{
390 return base.id() == ID_ashr;
391}
392
395{
396public:
397 lshr_exprt(exprt _src, exprt _distance)
398 : shift_exprt(std::move(_src), ID_lshr, std::move(_distance))
399 {
400 }
401
402 lshr_exprt(exprt _src, const std::size_t _distance)
403 : shift_exprt(std::move(_src), ID_lshr, std::move(_distance))
404 {
405 }
406};
407
408template <>
409inline bool can_cast_expr<lshr_exprt>(const exprt &base)
410{
411 return base.id() == ID_lshr;
412}
413
416{
417public:
420 : binary_predicate_exprt(std::move(_src), ID_extractbit, std::move(_index))
421 {
422 }
423
424 extractbit_exprt(exprt _src, const std::size_t _index);
425
427 {
428 return op0();
429 }
430
432 {
433 return op1();
434 }
435
436 const exprt &src() const
437 {
438 return op0();
439 }
440
441 const exprt &index() const
442 {
443 return op1();
444 }
445};
446
447template <>
449{
450 return base.id() == ID_extractbit;
451}
452
453inline void validate_expr(const extractbit_exprt &value)
454{
455 validate_operands(value, 2, "Extract bit must have two operands");
456}
457
464inline const extractbit_exprt &to_extractbit_expr(const exprt &expr)
465{
466 PRECONDITION(expr.id() == ID_extractbit);
467 const extractbit_exprt &ret = static_cast<const extractbit_exprt &>(expr);
468 validate_expr(ret);
469 return ret;
470}
471
474{
475 PRECONDITION(expr.id() == ID_extractbit);
476 extractbit_exprt &ret = static_cast<extractbit_exprt &>(expr);
477 validate_expr(ret);
478 return ret;
479}
480
483{
484public:
490 extractbits_exprt(exprt _src, exprt _index, typet _type)
492 ID_extractbits,
493 std::move(_type),
494 {std::move(_src), std::move(_index)})
495 {
496 }
497
498 extractbits_exprt(exprt _src, const std::size_t _index, typet _type);
499
501 {
502 return op0();
503 }
504
506 {
507 return op1();
508 }
509
510 const exprt &src() const
511 {
512 return op0();
513 }
514
515 const exprt &index() const
516 {
517 return op1();
518 }
519};
520
521template <>
523{
524 return base.id() == ID_extractbits;
525}
526
527inline void validate_expr(const extractbits_exprt &value)
528{
529 validate_operands(value, 2, "Extractbits must have two operands");
530}
531
539{
540 PRECONDITION(expr.id() == ID_extractbits);
541 const extractbits_exprt &ret = static_cast<const extractbits_exprt &>(expr);
542 validate_expr(ret);
543 return ret;
544}
545
548{
549 PRECONDITION(expr.id() == ID_extractbits);
550 extractbits_exprt &ret = static_cast<extractbits_exprt &>(expr);
551 validate_expr(ret);
552 return ret;
553}
554
557{
558public:
563 update_bit_exprt(exprt _src, exprt _index, exprt _new_value)
565 ID_update_bit,
566 _src.type(),
567 {_src, std::move(_index), std::move(_new_value)})
568 {
569 PRECONDITION(new_value().type().id() == ID_bool);
570 }
571
572 update_bit_exprt(exprt _src, const std::size_t _index, exprt _new_value);
573
575 {
576 return op0();
577 }
578
580 {
581 return op1();
582 }
583
585 {
586 return op2();
587 }
588
589 const exprt &src() const
590 {
591 return op0();
592 }
593
594 const exprt &index() const
595 {
596 return op1();
597 }
598
599 const exprt &new_value() const
600 {
601 return op2();
602 }
603
604 static void check(
605 const exprt &expr,
607 {
608 validate_operands(expr, 3, "update_bit must have three operands");
609 }
610
612 exprt lower() const;
613};
614
615template <>
617{
618 return base.id() == ID_update_bit;
619}
620
627inline const update_bit_exprt &to_update_bit_expr(const exprt &expr)
628{
629 PRECONDITION(expr.id() == ID_update_bit);
631 return static_cast<const update_bit_exprt &>(expr);
632}
633
636{
637 PRECONDITION(expr.id() == ID_update_bit);
639 return static_cast<update_bit_exprt &>(expr);
640}
641
644{
645public:
650 update_bits_exprt(exprt _src, exprt _index, exprt _new_value)
652 ID_update_bits,
653 _src.type(),
654 {_src, std::move(_index), std::move(_new_value)})
655 {
656 }
657
658 update_bits_exprt(exprt _src, const std::size_t _index, exprt _new_value);
659
661 {
662 return op0();
663 }
664
666 {
667 return op1();
668 }
669
671 {
672 return op2();
673 }
674
675 const exprt &src() const
676 {
677 return op0();
678 }
679
680 const exprt &index() const
681 {
682 return op1();
683 }
684
685 const exprt &new_value() const
686 {
687 return op2();
688 }
689
690 static void check(
691 const exprt &expr,
693 {
694 validate_operands(expr, 3, "update_bits must have three operands");
695 }
696
698 exprt lower() const;
699};
700
701template <>
703{
704 return base.id() == ID_update_bits;
705}
706
714{
715 PRECONDITION(expr.id() == ID_update_bits);
717 return static_cast<const update_bits_exprt &>(expr);
718}
719
722{
723 PRECONDITION(expr.id() == ID_update_bits);
725 return static_cast<update_bits_exprt &>(expr);
726}
727
730{
731public:
733 : binary_exprt(
734 std::move(_times),
735 ID_replication,
736 std::move(_src),
737 std::move(_type))
738 {
739 }
740
742 {
743 return static_cast<constant_exprt &>(op0());
744 }
745
746 const constant_exprt &times() const
747 {
748 return static_cast<const constant_exprt &>(op0());
749 }
750
752 {
753 return op1();
754 }
755
756 const exprt &op() const
757 {
758 return op1();
759 }
760};
761
762template <>
764{
765 return base.id() == ID_replication;
766}
767
768inline void validate_expr(const replication_exprt &value)
769{
770 validate_operands(value, 2, "Bit-wise replication must have two operands");
771}
772
780{
781 PRECONDITION(expr.id() == ID_replication);
782 const replication_exprt &ret = static_cast<const replication_exprt &>(expr);
783 validate_expr(ret);
784 return ret;
785}
786
789{
790 PRECONDITION(expr.id() == ID_replication);
791 replication_exprt &ret = static_cast<replication_exprt &>(expr);
792 validate_expr(ret);
793 return ret;
794}
795
802{
803public:
805 : multi_ary_exprt(ID_concatenation, std::move(_operands), std::move(_type))
806 {
807 }
808
811 ID_concatenation,
812 {std::move(_op0), std::move(_op1)},
813 std::move(_type))
814 {
815 }
816};
817
818template <>
820{
821 return base.id() == ID_concatenation;
822}
823
831{
832 PRECONDITION(expr.id() == ID_concatenation);
833 return static_cast<const concatenation_exprt &>(expr);
834}
835
838{
839 PRECONDITION(expr.id() == ID_concatenation);
840 return static_cast<concatenation_exprt &>(expr);
841}
842
845{
846public:
848 : unary_exprt(ID_popcount, std::move(_op), std::move(_type))
849 {
850 }
851
852 explicit popcount_exprt(const exprt &_op)
853 : unary_exprt(ID_popcount, _op, _op.type())
854 {
855 }
856
859 exprt lower() const;
860};
861
862template <>
863inline bool can_cast_expr<popcount_exprt>(const exprt &base)
864{
865 return base.id() == ID_popcount;
866}
867
868inline void validate_expr(const popcount_exprt &value)
869{
870 validate_operands(value, 1, "popcount must have one operand");
871}
872
879inline const popcount_exprt &to_popcount_expr(const exprt &expr)
880{
881 PRECONDITION(expr.id() == ID_popcount);
882 const popcount_exprt &ret = static_cast<const popcount_exprt &>(expr);
883 validate_expr(ret);
884 return ret;
885}
886
889{
890 PRECONDITION(expr.id() == ID_popcount);
891 popcount_exprt &ret = static_cast<popcount_exprt &>(expr);
892 validate_expr(ret);
893 return ret;
894}
895
899{
900public:
901 binary_overflow_exprt(exprt _lhs, const irep_idt &kind, exprt _rhs)
902 : binary_predicate_exprt(std::move(_lhs), make_id(kind), std::move(_rhs))
903 {
904 INVARIANT(
905 valid_id(id()),
906 "The kind used to construct binary_overflow_exprt should be in the set "
907 "of expected valid kinds.");
908 }
909
910 static void check(
911 const exprt &expr,
913 {
914 binary_exprt::check(expr, vm);
915
916 if(expr.id() != ID_overflow_shl)
917 {
918 const binary_exprt &binary_expr = to_binary_expr(expr);
920 vm,
921 binary_expr.lhs().type() == binary_expr.rhs().type(),
922 "operand types must match");
923 }
924 }
925
926 static void validate(
927 const exprt &expr,
928 const namespacet &,
930 {
931 check(expr, vm);
932 }
933
935 static bool valid_id(const irep_idt &id)
936 {
937 return id == ID_overflow_plus || id == ID_overflow_mult ||
938 id == ID_overflow_minus || id == ID_overflow_shl;
939 }
940
941private:
942 static irep_idt make_id(const irep_idt &kind)
943 {
944 if(valid_id(kind))
945 return kind;
946 else
947 return "overflow-" + id2string(kind);
948 }
949};
950
951template <>
953{
954 return binary_overflow_exprt::valid_id(base.id());
955}
956
957inline void validate_expr(const binary_overflow_exprt &value)
958{
960 value, 2, "binary overflow expression must have two operands");
961}
962
970{
972 expr.id() == ID_overflow_plus || expr.id() == ID_overflow_mult ||
973 expr.id() == ID_overflow_minus || expr.id() == ID_overflow_shl);
974 const binary_overflow_exprt &ret =
975 static_cast<const binary_overflow_exprt &>(expr);
976 validate_expr(ret);
977 return ret;
978}
979
982{
984 expr.id() == ID_overflow_plus || expr.id() == ID_overflow_mult ||
985 expr.id() == ID_overflow_minus || expr.id() == ID_overflow_shl);
986 binary_overflow_exprt &ret = static_cast<binary_overflow_exprt &>(expr);
987 validate_expr(ret);
988 return ret;
989}
990
992{
993public:
995 : binary_overflow_exprt(std::move(_lhs), ID_overflow_plus, std::move(_rhs))
996 {
997 }
998
1001 exprt lower() const;
1002};
1003
1004template <>
1006{
1007 return base.id() == ID_overflow_plus;
1008}
1009
1011{
1012public:
1014 : binary_overflow_exprt(std::move(_lhs), ID_overflow_minus, std::move(_rhs))
1015 {
1016 }
1017
1020 exprt lower() const;
1021};
1022
1023template <>
1025{
1026 return base.id() == ID_overflow_minus;
1027}
1028
1030{
1031public:
1033 : binary_overflow_exprt(std::move(_lhs), ID_overflow_mult, std::move(_rhs))
1034 {
1035 }
1036
1039 exprt lower() const;
1040};
1041
1042template <>
1044{
1045 return base.id() == ID_overflow_mult;
1046}
1047
1049{
1050public:
1052 : binary_overflow_exprt(std::move(_lhs), ID_overflow_shl, std::move(_rhs))
1053 {
1054 }
1055};
1056
1057template <>
1059{
1060 return base.id() == ID_overflow_shl;
1061}
1062
1066{
1067public:
1069 : unary_predicate_exprt("overflow-" + id2string(kind), std::move(_op))
1070 {
1071 }
1072
1073 static void check(
1074 const exprt &expr,
1076 {
1077 unary_exprt::check(expr, vm);
1078 }
1079
1080 static void validate(
1081 const exprt &expr,
1082 const namespacet &,
1084 {
1085 check(expr, vm);
1086 }
1087};
1088
1089template <>
1091{
1092 return base.id() == ID_overflow_unary_minus;
1093}
1094
1095inline void validate_expr(const unary_overflow_exprt &value)
1096{
1098 value, 1, "unary overflow expression must have one operand");
1099}
1100
1104{
1105public:
1107 : unary_overflow_exprt(ID_unary_minus, std::move(_op))
1108 {
1109 }
1110
1111 static void check(
1112 const exprt &expr,
1114 {
1115 unary_exprt::check(expr, vm);
1116 }
1117
1118 static void validate(
1119 const exprt &expr,
1120 const namespacet &,
1122 {
1123 check(expr, vm);
1124 }
1125};
1126
1127template <>
1129{
1130 return base.id() == ID_overflow_unary_minus;
1131}
1132
1134{
1136 value, 1, "unary minus overflow expression must have one operand");
1137}
1138
1146{
1147 PRECONDITION(expr.id() == ID_overflow_unary_minus);
1148 const unary_overflow_exprt &ret =
1149 static_cast<const unary_overflow_exprt &>(expr);
1150 validate_expr(ret);
1151 return ret;
1152}
1153
1156{
1157 PRECONDITION(expr.id() == ID_overflow_unary_minus);
1158 unary_overflow_exprt &ret = static_cast<unary_overflow_exprt &>(expr);
1159 validate_expr(ret);
1160 return ret;
1161}
1162
1169{
1170public:
1171 count_leading_zeros_exprt(exprt _op, bool _zero_permitted, typet _type)
1172 : unary_exprt(ID_count_leading_zeros, std::move(_op), std::move(_type))
1173 {
1174 zero_permitted(_zero_permitted);
1175 }
1176
1178 : count_leading_zeros_exprt(_op, true, _op.type())
1179 {
1180 }
1181
1182 bool zero_permitted() const
1183 {
1184 return !get_bool(ID_C_bounds_check);
1185 }
1186
1187 void zero_permitted(bool value)
1188 {
1189 set(ID_C_bounds_check, !value);
1190 }
1191
1192 static void check(
1193 const exprt &expr,
1195 {
1196 DATA_CHECK(
1197 vm,
1198 expr.operands().size() == 1,
1199 "unary expression must have a single operand");
1200 DATA_CHECK(
1201 vm,
1203 "operand must be of bitvector type");
1204 }
1205
1206 static void validate(
1207 const exprt &expr,
1208 const namespacet &,
1210 {
1211 check(expr, vm);
1212 }
1213
1216 exprt lower() const;
1217};
1218
1219template <>
1221{
1222 return base.id() == ID_count_leading_zeros;
1223}
1224
1226{
1227 validate_operands(value, 1, "count_leading_zeros must have one operand");
1228}
1229
1236inline const count_leading_zeros_exprt &
1238{
1239 PRECONDITION(expr.id() == ID_count_leading_zeros);
1240 const count_leading_zeros_exprt &ret =
1241 static_cast<const count_leading_zeros_exprt &>(expr);
1242 validate_expr(ret);
1243 return ret;
1244}
1245
1248{
1249 PRECONDITION(expr.id() == ID_count_leading_zeros);
1251 static_cast<count_leading_zeros_exprt &>(expr);
1252 validate_expr(ret);
1253 return ret;
1254}
1255
1262{
1263public:
1264 count_trailing_zeros_exprt(exprt _op, bool _zero_permitted, typet _type)
1265 : unary_exprt(ID_count_trailing_zeros, std::move(_op), std::move(_type))
1266 {
1267 zero_permitted(_zero_permitted);
1268 }
1269
1271 : count_trailing_zeros_exprt(_op, true, _op.type())
1272 {
1273 }
1274
1275 bool zero_permitted() const
1276 {
1277 return !get_bool(ID_C_bounds_check);
1278 }
1279
1280 void zero_permitted(bool value)
1281 {
1282 set(ID_C_bounds_check, !value);
1283 }
1284
1285 static void check(
1286 const exprt &expr,
1288 {
1289 DATA_CHECK(
1290 vm,
1291 expr.operands().size() == 1,
1292 "unary expression must have a single operand");
1293 DATA_CHECK(
1294 vm,
1296 "operand must be of bitvector type");
1297 }
1298
1299 static void validate(
1300 const exprt &expr,
1301 const namespacet &,
1303 {
1304 check(expr, vm);
1305 }
1306
1309 exprt lower() const;
1310};
1311
1312template <>
1314{
1315 return base.id() == ID_count_trailing_zeros;
1316}
1317
1319{
1320 validate_operands(value, 1, "count_trailing_zeros must have one operand");
1321}
1322
1329inline const count_trailing_zeros_exprt &
1331{
1332 PRECONDITION(expr.id() == ID_count_trailing_zeros);
1333 const count_trailing_zeros_exprt &ret =
1334 static_cast<const count_trailing_zeros_exprt &>(expr);
1335 validate_expr(ret);
1336 return ret;
1337}
1338
1341{
1342 PRECONDITION(expr.id() == ID_count_trailing_zeros);
1344 static_cast<count_trailing_zeros_exprt &>(expr);
1345 validate_expr(ret);
1346 return ret;
1347}
1348
1351{
1352public:
1354 : unary_exprt(ID_bitreverse, std::move(op))
1355 {
1356 }
1357
1360 exprt lower() const;
1361};
1362
1363template <>
1365{
1366 return base.id() == ID_bitreverse;
1367}
1368
1369inline void validate_expr(const bitreverse_exprt &value)
1370{
1371 validate_operands(value, 1, "Bit-wise reverse must have one operand");
1372}
1373
1381{
1382 PRECONDITION(expr.id() == ID_bitreverse);
1383 const bitreverse_exprt &ret = static_cast<const bitreverse_exprt &>(expr);
1384 validate_expr(ret);
1385 return ret;
1386}
1387
1390{
1391 PRECONDITION(expr.id() == ID_bitreverse);
1392 bitreverse_exprt &ret = static_cast<bitreverse_exprt &>(expr);
1393 validate_expr(ret);
1394 return ret;
1395}
1396
1399{
1400public:
1402 : binary_exprt(std::move(_lhs), ID_saturating_plus, std::move(_rhs))
1403 {
1404 }
1405
1407 : binary_exprt(
1408 std::move(_lhs),
1409 ID_saturating_plus,
1410 std::move(_rhs),
1411 std::move(_type))
1412 {
1413 }
1414};
1415
1416template <>
1418{
1419 return base.id() == ID_saturating_plus;
1420}
1421
1422inline void validate_expr(const saturating_plus_exprt &value)
1423{
1424 validate_operands(value, 2, "saturating plus must have two operands");
1425}
1426
1434{
1435 PRECONDITION(expr.id() == ID_saturating_plus);
1436 const saturating_plus_exprt &ret =
1437 static_cast<const saturating_plus_exprt &>(expr);
1438 validate_expr(ret);
1439 return ret;
1440}
1441
1444{
1445 PRECONDITION(expr.id() == ID_saturating_plus);
1446 saturating_plus_exprt &ret = static_cast<saturating_plus_exprt &>(expr);
1447 validate_expr(ret);
1448 return ret;
1449}
1450
1453{
1454public:
1456 : binary_exprt(std::move(_lhs), ID_saturating_minus, std::move(_rhs))
1457 {
1458 }
1459};
1460
1461template <>
1463{
1464 return base.id() == ID_saturating_minus;
1465}
1466
1467inline void validate_expr(const saturating_minus_exprt &value)
1468{
1469 validate_operands(value, 2, "saturating minus must have two operands");
1470}
1471
1479{
1480 PRECONDITION(expr.id() == ID_saturating_minus);
1481 const saturating_minus_exprt &ret =
1482 static_cast<const saturating_minus_exprt &>(expr);
1483 validate_expr(ret);
1484 return ret;
1485}
1486
1489{
1490 PRECONDITION(expr.id() == ID_saturating_minus);
1491 saturating_minus_exprt &ret = static_cast<saturating_minus_exprt &>(expr);
1492 validate_expr(ret);
1493 return ret;
1494}
1495
1499{
1500public:
1503 make_id(kind),
1505 {{ID_value, _lhs.type()},
1506 {"overflow-" + id2string(kind), bool_typet{}}}},
1507 {_lhs, std::move(_rhs)})
1508 {
1509 INVARIANT(
1510 valid_id(id()),
1511 "The kind used to construct overflow_result_exprt should be in the set "
1512 "of expected valid kinds.");
1513 }
1514
1517 make_id(kind),
1519 {{ID_value, _op.type()},
1520 {"overflow-" + id2string(kind), bool_typet{}}}},
1521 {_op})
1522 {
1523 INVARIANT(
1524 valid_id(id()),
1525 "The kind used to construct overflow_result_exprt should be in the set "
1526 "of expected valid kinds.");
1527 }
1528
1529 // make op0 and op1 public
1530 using exprt::op0;
1531 using exprt::op1;
1532
1533 const exprt &op2() const = delete;
1534 exprt &op2() = delete;
1535 const exprt &op3() const = delete;
1536 exprt &op3() = delete;
1537
1538 static void check(
1539 const exprt &expr,
1541 {
1542 if(expr.id() != ID_overflow_result_unary_minus)
1543 binary_exprt::check(expr, vm);
1544
1545 if(
1546 expr.id() != ID_overflow_result_unary_minus &&
1547 expr.id() != ID_overflow_result_shl)
1548 {
1549 const binary_exprt &binary_expr = to_binary_expr(expr);
1550 DATA_CHECK(
1551 vm,
1552 binary_expr.lhs().type() == binary_expr.rhs().type(),
1553 "operand types must match");
1554 }
1555 }
1556
1557 static void validate(
1558 const exprt &expr,
1559 const namespacet &,
1561 {
1562 check(expr, vm);
1563 }
1564
1566 static bool valid_id(const irep_idt &id)
1567 {
1568 return id == ID_overflow_result_plus || id == ID_overflow_result_mult ||
1569 id == ID_overflow_result_minus || id == ID_overflow_result_shl ||
1570 id == ID_overflow_result_unary_minus;
1571 }
1572
1573private:
1574 static irep_idt make_id(const irep_idt &kind)
1575 {
1576 return "overflow_result-" + id2string(kind);
1577 }
1578};
1579
1580template <>
1582{
1583 return overflow_result_exprt::valid_id(base.id());
1584}
1585
1586inline void validate_expr(const overflow_result_exprt &value)
1587{
1588 if(value.id() == ID_overflow_result_unary_minus)
1589 {
1591 value, 1, "unary overflow expression must have two operands");
1592 }
1593 else
1594 {
1596 value, 2, "binary overflow expression must have two operands");
1597 }
1598}
1599
1607{
1609 const overflow_result_exprt &ret =
1610 static_cast<const overflow_result_exprt &>(expr);
1611 validate_expr(ret);
1612 return ret;
1613}
1614
1617{
1619 overflow_result_exprt &ret = static_cast<overflow_result_exprt &>(expr);
1620 validate_expr(ret);
1621 return ret;
1622}
1623
1627{
1628public:
1630 : unary_exprt(ID_find_first_set, std::move(_op), std::move(_type))
1631 {
1632 }
1633
1634 explicit find_first_set_exprt(const exprt &_op)
1635 : find_first_set_exprt(_op, _op.type())
1636 {
1637 }
1638
1639 static void check(
1640 const exprt &expr,
1642 {
1643 DATA_CHECK(
1644 vm,
1645 expr.operands().size() == 1,
1646 "unary expression must have a single operand");
1647 DATA_CHECK(
1648 vm,
1650 "operand must be of bitvector type");
1651 }
1652
1653 static void validate(
1654 const exprt &expr,
1655 const namespacet &,
1657 {
1658 check(expr, vm);
1659 }
1660
1663 exprt lower() const;
1664};
1665
1666template <>
1668{
1669 return base.id() == ID_find_first_set;
1670}
1671
1672inline void validate_expr(const find_first_set_exprt &value)
1673{
1674 validate_operands(value, 1, "find_first_set must have one operand");
1675}
1676
1684{
1685 PRECONDITION(expr.id() == ID_find_first_set);
1686 const find_first_set_exprt &ret =
1687 static_cast<const find_first_set_exprt &>(expr);
1688 validate_expr(ret);
1689 return ret;
1690}
1691
1694{
1695 PRECONDITION(expr.id() == ID_find_first_set);
1696 find_first_set_exprt &ret = static_cast<find_first_set_exprt &>(expr);
1697 validate_expr(ret);
1698 return ret;
1699}
1700
1707{
1708public:
1710 : unary_exprt(ID_zero_extend, std::move(_op), std::move(_type))
1711 {
1712 }
1713
1714 // a lowering to extraction or concatenation
1715 exprt lower() const;
1716};
1717
1718template <>
1720{
1721 return base.id() == ID_zero_extend;
1722}
1723
1731{
1732 PRECONDITION(expr.id() == ID_zero_extend);
1734 return static_cast<const zero_extend_exprt &>(expr);
1735}
1736
1739{
1740 PRECONDITION(expr.id() == ID_zero_extend);
1742 return static_cast<zero_extend_exprt &>(expr);
1743}
1744
1745#endif // CPROVER_UTIL_BITVECTOR_EXPR_H
bool can_cast_expr< count_trailing_zeros_exprt >(const exprt &base)
const bitxnor_exprt & to_bitxnor_expr(const exprt &expr)
Cast an exprt to a bitxnor_exprt.
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< zero_extend_exprt >(const exprt &base)
bool can_cast_expr< shl_overflow_exprt >(const exprt &base)
bool can_cast_expr< bitxnor_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 zero_extend_exprt & to_zero_extend_expr(const exprt &expr)
Cast an exprt to a zero_extend_exprt.
const count_trailing_zeros_exprt & to_count_trailing_zeros_expr(const exprt &expr)
Cast an exprt to a count_trailing_zeros_exprt.
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
binary_exprt(const exprt &_lhs, const irep_idt &_id, exprt _rhs)
Definition std_expr.h:640
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)
binary_predicate_exprt(exprt _op0, const irep_idt &_id, exprt _op1)
Definition std_expr.h:733
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 XNOR.
bitxnor_exprt(exprt _op0, exprt _op1)
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:2995
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.
expr_protectedt(irep_idt _id, typet _type)
Definition expr.h:347
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()
Definition expr.h:61
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:254
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
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.
multi_ary_exprt(const irep_idt &_id, operandst _operands, typet _type)
Definition std_expr.h:914
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
unary_exprt(const irep_idt &_id, const exprt &_op)
Definition std_expr.h:363
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)
unary_predicate_exprt(const irep_idt &_id, exprt _op)
Definition std_expr.h:587
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)
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)
zero extension The operand is converted to the given type by either a) truncating if the new type is ...
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
bool can_cast_type(const typet &base)
Check whether a reference to a generic typet is of a specific derived class.
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
#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
dstringt irep_idt