CBMC
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:
22 : unary_exprt(ID_bswap, std::move(_op), std::move(_type))
23 {
25 }
26
32
33 std::size_t get_bits_per_byte() const
34 {
36 }
37
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);
68 return ret;
69}
70
73{
74 PRECONDITION(expr.id() == ID_bswap);
75 bswap_exprt &ret = static_cast<bswap_exprt &>(expr);
77 return ret;
78}
79
82{
83public:
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);
111 return ret;
112}
113
116{
117 PRECONDITION(expr.id() == ID_bitnot);
118 bitnot_exprt &ret = static_cast<bitnot_exprt &>(expr);
120 return ret;
121}
122
125{
126public:
129 {
130 }
131
133 : multi_ary_exprt(ID_bitor, std::move(_operands), std::move(_type))
134 {
135 }
136};
137
138template <>
139inline bool can_cast_expr<bitor_exprt>(const exprt &base)
140{
141 return base.id() == ID_bitor;
142}
143
150inline const bitor_exprt &to_bitor_expr(const exprt &expr)
151{
152 PRECONDITION(expr.id() == ID_bitor);
153 return static_cast<const bitor_exprt &>(expr);
154}
155
158{
159 PRECONDITION(expr.id() == ID_bitor);
160 return static_cast<bitor_exprt &>(expr);
161}
162
169{
170public:
172 : multi_ary_exprt(std::move(_op0), ID_bitnor, std::move(_op1))
173 {
174 }
175
177 : multi_ary_exprt(ID_bitnor, std::move(_operands), std::move(_type))
178 {
179 }
180};
181
182template <>
183inline bool can_cast_expr<bitnor_exprt>(const exprt &base)
184{
185 return base.id() == ID_bitnor;
186}
187
194inline const bitnor_exprt &to_bitnor_expr(const exprt &expr)
195{
196 PRECONDITION(expr.id() == ID_bitnor);
197 return static_cast<const bitnor_exprt &>(expr);
198}
199
202{
203 PRECONDITION(expr.id() == ID_bitnor);
204 return static_cast<bitnor_exprt &>(expr);
205}
206
209{
210public:
212 : multi_ary_exprt(std::move(_op0), ID_bitxor, std::move(_op1))
213 {
214 }
215
217 : multi_ary_exprt(ID_bitxor, std::move(_operands), std::move(_type))
218 {
219 }
220};
221
222template <>
223inline bool can_cast_expr<bitxor_exprt>(const exprt &base)
224{
225 return base.id() == ID_bitxor;
226}
227
234inline const bitxor_exprt &to_bitxor_expr(const exprt &expr)
235{
236 PRECONDITION(expr.id() == ID_bitxor);
237 return static_cast<const bitxor_exprt &>(expr);
238}
239
242{
243 PRECONDITION(expr.id() == ID_bitxor);
244 return static_cast<bitxor_exprt &>(expr);
245}
246
253{
254public:
259
261 : multi_ary_exprt(ID_bitxnor, std::move(_operands), std::move(_type))
262 {
263 }
264};
265
266template <>
267inline bool can_cast_expr<bitxnor_exprt>(const exprt &base)
268{
269 return base.id() == ID_bitxnor;
270}
271
278inline const bitxnor_exprt &to_bitxnor_expr(const exprt &expr)
279{
280 PRECONDITION(expr.id() == ID_bitxnor);
282 return static_cast<const bitxnor_exprt &>(expr);
283}
284
287{
288 PRECONDITION(expr.id() == ID_bitxnor);
290 return static_cast<bitxnor_exprt &>(expr);
291}
292
295{
296public:
299 {
300 }
301
303 : multi_ary_exprt(ID_bitand, std::move(_operands), std::move(_type))
304 {
305 }
306};
307
308template <>
309inline bool can_cast_expr<bitand_exprt>(const exprt &base)
310{
311 return base.id() == ID_bitand;
312}
313
320inline const bitand_exprt &to_bitand_expr(const exprt &expr)
321{
322 PRECONDITION(expr.id() == ID_bitand);
323 return static_cast<const bitand_exprt &>(expr);
324}
325
328{
329 PRECONDITION(expr.id() == ID_bitand);
330 return static_cast<bitand_exprt &>(expr);
331}
332
339{
340public:
345
347 : multi_ary_exprt(ID_bitnand, std::move(_operands), std::move(_type))
348 {
349 }
350};
351
352template <>
353inline bool can_cast_expr<bitnand_exprt>(const exprt &base)
354{
355 return base.id() == ID_bitnand;
356}
357
364inline const bitnand_exprt &to_bitnand_expr(const exprt &expr)
365{
366 PRECONDITION(expr.id() == ID_bitnand);
367 return static_cast<const bitnand_exprt &>(expr);
368}
369
372{
373 PRECONDITION(expr.id() == ID_bitnand);
374 return static_cast<bitnand_exprt &>(expr);
375}
376
379{
380public:
382 : binary_exprt(std::move(_src), _id, std::move(_distance))
383 {
384 }
385
386 shift_exprt(exprt _src, const irep_idt &_id, const std::size_t _distance);
387
389 {
390 return op0();
391 }
392
393 const exprt &op() const
394 {
395 return op0();
396 }
397
399 {
400 return op1();
401 }
402
403 const exprt &distance() const
404 {
405 return op1();
406 }
407};
408
409template <>
410inline bool can_cast_expr<shift_exprt>(const exprt &base)
411{
412 return base.id() == ID_shl || base.id() == ID_ashr || base.id() == ID_lshr ||
413 base.id() == ID_ror || base.id() == ID_rol;
414}
415
416inline void validate_expr(const shift_exprt &value)
417{
418 validate_operands(value, 2, "Shifts must have two operands");
419}
420
427inline const shift_exprt &to_shift_expr(const exprt &expr)
428{
429 const shift_exprt &ret = static_cast<const shift_exprt &>(expr);
431 return ret;
432}
433
436{
437 shift_exprt &ret = static_cast<shift_exprt &>(expr);
439 return ret;
440}
441
443class shl_exprt : public shift_exprt
444{
445public:
447 : shift_exprt(std::move(_src), ID_shl, std::move(_distance))
448 {
449 }
450
451 shl_exprt(exprt _src, const std::size_t _distance)
453 {
454 }
455};
456
457template <>
458inline bool can_cast_expr<shl_exprt>(const exprt &base)
459{
460 return base.id() == ID_shl;
461}
462
469inline const shl_exprt &to_shl_expr(const exprt &expr)
470{
471 PRECONDITION(expr.id() == ID_shl);
472 const shl_exprt &ret = static_cast<const shl_exprt &>(expr);
474 return ret;
475}
476
479{
480 PRECONDITION(expr.id() == ID_shl);
481 shl_exprt &ret = static_cast<shl_exprt &>(expr);
483 return ret;
484}
485
488{
489public:
494
495 ashr_exprt(exprt _src, const std::size_t _distance)
497 {
498 }
499};
500
501template <>
502inline bool can_cast_expr<ashr_exprt>(const exprt &base)
503{
504 return base.id() == ID_ashr;
505}
506
509{
510public:
515
516 lshr_exprt(exprt _src, const std::size_t _distance)
517 : shift_exprt(std::move(_src), ID_lshr, std::move(_distance))
518 {
519 }
520};
521
522template <>
523inline bool can_cast_expr<lshr_exprt>(const exprt &base)
524{
525 return base.id() == ID_lshr;
526}
527
530{
531public:
537
538 extractbit_exprt(exprt _src, const std::size_t _index);
539
541 {
542 return op0();
543 }
544
546 {
547 return op1();
548 }
549
550 const exprt &src() const
551 {
552 return op0();
553 }
554
555 const exprt &index() const
556 {
557 return op1();
558 }
559};
560
561template <>
563{
564 return base.id() == ID_extractbit;
565}
566
567inline void validate_expr(const extractbit_exprt &value)
568{
569 validate_operands(value, 2, "Extract bit must have two operands");
570}
571
578inline const extractbit_exprt &to_extractbit_expr(const exprt &expr)
579{
580 PRECONDITION(expr.id() == ID_extractbit);
581 const extractbit_exprt &ret = static_cast<const extractbit_exprt &>(expr);
583 return ret;
584}
585
588{
589 PRECONDITION(expr.id() == ID_extractbit);
590 extractbit_exprt &ret = static_cast<extractbit_exprt &>(expr);
592 return ret;
593}
594
597{
598public:
607 std::move(_type),
608 {std::move(_src), std::move(_index)})
609 {
610 }
611
612 extractbits_exprt(exprt _src, const std::size_t _index, typet _type);
613
615 {
616 return op0();
617 }
618
620 {
621 return op1();
622 }
623
624 const exprt &src() const
625 {
626 return op0();
627 }
628
629 const exprt &index() const
630 {
631 return op1();
632 }
633};
634
635template <>
637{
638 return base.id() == ID_extractbits;
639}
640
641inline void validate_expr(const extractbits_exprt &value)
642{
643 validate_operands(value, 2, "Extractbits must have two operands");
644}
645
653{
654 PRECONDITION(expr.id() == ID_extractbits);
655 const extractbits_exprt &ret = static_cast<const extractbits_exprt &>(expr);
657 return ret;
658}
659
662{
663 PRECONDITION(expr.id() == ID_extractbits);
664 extractbits_exprt &ret = static_cast<extractbits_exprt &>(expr);
666 return ret;
667}
668
671{
672public:
680 _src.type(),
681 {_src, std::move(_index), std::move(_new_value)})
682 {
683 PRECONDITION(new_value().type().id() == ID_bool);
684 }
685
686 update_bit_exprt(exprt _src, const std::size_t _index, exprt _new_value);
687
689 {
690 return op0();
691 }
692
694 {
695 return op1();
696 }
697
699 {
700 return op2();
701 }
702
703 const exprt &src() const
704 {
705 return op0();
706 }
707
708 const exprt &index() const
709 {
710 return op1();
711 }
712
713 const exprt &new_value() const
714 {
715 return op2();
716 }
717
718 static void check(
719 const exprt &expr,
721 {
722 validate_operands(expr, 3, "update_bit must have three operands");
723 }
724
726 exprt lower() const;
727};
728
729template <>
731{
732 return base.id() == ID_update_bit;
733}
734
741inline const update_bit_exprt &to_update_bit_expr(const exprt &expr)
742{
743 PRECONDITION(expr.id() == ID_update_bit);
745 return static_cast<const update_bit_exprt &>(expr);
746}
747
750{
751 PRECONDITION(expr.id() == ID_update_bit);
753 return static_cast<update_bit_exprt &>(expr);
754}
755
758{
759public:
767 _src.type(),
768 {_src, std::move(_index), std::move(_new_value)})
769 {
770 }
771
773
775 {
776 return op0();
777 }
778
780 {
781 return op1();
782 }
783
785 {
786 return op2();
787 }
788
789 const exprt &src() const
790 {
791 return op0();
792 }
793
794 const exprt &index() const
795 {
796 return op1();
797 }
798
799 const exprt &new_value() const
800 {
801 return op2();
802 }
803
804 static void check(
805 const exprt &expr,
807 {
808 validate_operands(expr, 3, "update_bits must have three operands");
809 }
810
812 exprt lower() const;
813};
814
815template <>
817{
818 return base.id() == ID_update_bits;
819}
820
828{
829 PRECONDITION(expr.id() == ID_update_bits);
831 return static_cast<const update_bits_exprt &>(expr);
832}
833
836{
837 PRECONDITION(expr.id() == ID_update_bits);
839 return static_cast<update_bits_exprt &>(expr);
840}
841
844{
845public:
847 : binary_exprt(
848 std::move(_times),
850 std::move(_src),
851 std::move(_type))
852 {
853 }
854
856 {
857 return static_cast<constant_exprt &>(op0());
858 }
859
860 const constant_exprt &times() const
861 {
862 return static_cast<const constant_exprt &>(op0());
863 }
864
866 {
867 return op1();
868 }
869
870 const exprt &op() const
871 {
872 return op1();
873 }
874};
875
876template <>
878{
879 return base.id() == ID_replication;
880}
881
882inline void validate_expr(const replication_exprt &value)
883{
884 validate_operands(value, 2, "Bit-wise replication must have two operands");
885}
886
894{
895 PRECONDITION(expr.id() == ID_replication);
896 const replication_exprt &ret = static_cast<const replication_exprt &>(expr);
898 return ret;
899}
900
903{
904 PRECONDITION(expr.id() == ID_replication);
905 replication_exprt &ret = static_cast<replication_exprt &>(expr);
907 return ret;
908}
909
916{
917public:
922
926 {std::move(_op0), std::move(_op1)},
927 std::move(_type))
928 {
929 }
930};
931
932template <>
934{
935 return base.id() == ID_concatenation;
936}
937
945{
947 return static_cast<const concatenation_exprt &>(expr);
948}
949
952{
954 return static_cast<concatenation_exprt &>(expr);
955}
956
959{
960public:
962 : unary_exprt(ID_popcount, std::move(_op), std::move(_type))
963 {
964 }
965
966 explicit popcount_exprt(const exprt &_op)
968 {
969 }
970
973 exprt lower() const;
974};
975
976template <>
977inline bool can_cast_expr<popcount_exprt>(const exprt &base)
978{
979 return base.id() == ID_popcount;
980}
981
982inline void validate_expr(const popcount_exprt &value)
983{
984 validate_operands(value, 1, "popcount must have one operand");
985}
986
993inline const popcount_exprt &to_popcount_expr(const exprt &expr)
994{
995 PRECONDITION(expr.id() == ID_popcount);
996 const popcount_exprt &ret = static_cast<const popcount_exprt &>(expr);
998 return ret;
999}
1000
1003{
1004 PRECONDITION(expr.id() == ID_popcount);
1005 popcount_exprt &ret = static_cast<popcount_exprt &>(expr);
1007 return ret;
1008}
1009
1013{
1014public:
1016 : binary_predicate_exprt(std::move(_lhs), make_id(kind), std::move(_rhs))
1017 {
1018 INVARIANT(
1019 valid_id(id()),
1020 "The kind used to construct binary_overflow_exprt should be in the set "
1021 "of expected valid kinds.");
1022 }
1023
1024 static void check(
1025 const exprt &expr,
1027 {
1028 binary_exprt::check(expr, vm);
1029
1030 if(expr.id() != ID_overflow_shl)
1031 {
1033 DATA_CHECK(
1034 vm,
1035 binary_expr.lhs().type() == binary_expr.rhs().type(),
1036 "operand types must match");
1037 }
1038 }
1039
1040 static void validate(
1041 const exprt &expr,
1042 const namespacet &,
1044 {
1045 check(expr, vm);
1046 }
1047
1049 static bool valid_id(const irep_idt &id)
1050 {
1051 return id == ID_overflow_plus || id == ID_overflow_mult ||
1052 id == ID_overflow_minus || id == ID_overflow_shl;
1053 }
1054
1055private:
1056 static irep_idt make_id(const irep_idt &kind)
1057 {
1058 if(valid_id(kind))
1059 return kind;
1060 else
1061 return "overflow-" + id2string(kind);
1062 }
1063};
1064
1065template <>
1067{
1068 return binary_overflow_exprt::valid_id(base.id());
1069}
1070
1071inline void validate_expr(const binary_overflow_exprt &value)
1072{
1074 value, 2, "binary overflow expression must have two operands");
1075}
1076
1084{
1086 expr.id() == ID_overflow_plus || expr.id() == ID_overflow_mult ||
1087 expr.id() == ID_overflow_minus || expr.id() == ID_overflow_shl);
1088 const binary_overflow_exprt &ret =
1089 static_cast<const binary_overflow_exprt &>(expr);
1091 return ret;
1092}
1093
1096{
1098 expr.id() == ID_overflow_plus || expr.id() == ID_overflow_mult ||
1099 expr.id() == ID_overflow_minus || expr.id() == ID_overflow_shl);
1100 binary_overflow_exprt &ret = static_cast<binary_overflow_exprt &>(expr);
1102 return ret;
1103}
1104
1106{
1107public:
1112
1115 exprt lower() const;
1116};
1117
1118template <>
1120{
1121 return base.id() == ID_overflow_plus;
1122}
1123
1125{
1126public:
1131
1134 exprt lower() const;
1135};
1136
1137template <>
1139{
1140 return base.id() == ID_overflow_minus;
1141}
1142
1144{
1145public:
1150
1153 exprt lower() const;
1154};
1155
1156template <>
1158{
1159 return base.id() == ID_overflow_mult;
1160}
1161
1163{
1164public:
1169};
1170
1171template <>
1173{
1174 return base.id() == ID_overflow_shl;
1175}
1176
1180{
1181public:
1183 : unary_predicate_exprt("overflow-" + id2string(kind), std::move(_op))
1184 {
1185 }
1186
1187 static void check(
1188 const exprt &expr,
1190 {
1191 unary_exprt::check(expr, vm);
1192 }
1193
1194 static void validate(
1195 const exprt &expr,
1196 const namespacet &,
1198 {
1199 check(expr, vm);
1200 }
1201};
1202
1203template <>
1205{
1206 return base.id() == ID_overflow_unary_minus;
1207}
1208
1209inline void validate_expr(const unary_overflow_exprt &value)
1210{
1212 value, 1, "unary overflow expression must have one operand");
1213}
1214
1218{
1219public:
1224
1225 static void check(
1226 const exprt &expr,
1228 {
1229 unary_exprt::check(expr, vm);
1230 }
1231
1232 static void validate(
1233 const exprt &expr,
1234 const namespacet &,
1236 {
1237 check(expr, vm);
1238 }
1239};
1240
1241template <>
1243{
1244 return base.id() == ID_overflow_unary_minus;
1245}
1246
1248{
1250 value, 1, "unary minus overflow expression must have one operand");
1251}
1252
1260{
1262 const unary_overflow_exprt &ret =
1263 static_cast<const unary_overflow_exprt &>(expr);
1265 return ret;
1266}
1267
1270{
1272 unary_overflow_exprt &ret = static_cast<unary_overflow_exprt &>(expr);
1274 return ret;
1275}
1276
1283{
1284public:
1290
1293 {
1294 }
1295
1296 bool zero_permitted() const
1297 {
1298 return !get_bool(ID_C_bounds_check);
1299 }
1300
1301 void zero_permitted(bool value)
1302 {
1303 set(ID_C_bounds_check, !value);
1304 }
1305
1306 static void check(
1307 const exprt &expr,
1309 {
1310 DATA_CHECK(
1311 vm,
1312 expr.operands().size() == 1,
1313 "unary expression must have a single operand");
1314 DATA_CHECK(
1315 vm,
1317 "operand must be of bitvector type");
1318 }
1319
1320 static void validate(
1321 const exprt &expr,
1322 const namespacet &,
1324 {
1325 check(expr, vm);
1326 }
1327
1330 exprt lower() const;
1331};
1332
1333template <>
1335{
1336 return base.id() == ID_count_leading_zeros;
1337}
1338
1340{
1341 validate_operands(value, 1, "count_leading_zeros must have one operand");
1342}
1343
1350inline const count_leading_zeros_exprt &
1352{
1355 static_cast<const count_leading_zeros_exprt &>(expr);
1357 return ret;
1358}
1359
1369
1376{
1377public:
1383
1388
1389 bool zero_permitted() const
1390 {
1391 return !get_bool(ID_C_bounds_check);
1392 }
1393
1394 void zero_permitted(bool value)
1395 {
1396 set(ID_C_bounds_check, !value);
1397 }
1398
1399 static void check(
1400 const exprt &expr,
1402 {
1403 DATA_CHECK(
1404 vm,
1405 expr.operands().size() == 1,
1406 "unary expression must have a single operand");
1407 DATA_CHECK(
1408 vm,
1410 "operand must be of bitvector type");
1411 }
1412
1413 static void validate(
1414 const exprt &expr,
1415 const namespacet &,
1417 {
1418 check(expr, vm);
1419 }
1420
1423 exprt lower() const;
1424};
1425
1426template <>
1428{
1429 return base.id() == ID_count_trailing_zeros;
1430}
1431
1433{
1434 validate_operands(value, 1, "count_trailing_zeros must have one operand");
1435}
1436
1443inline const count_trailing_zeros_exprt &
1445{
1448 static_cast<const count_trailing_zeros_exprt &>(expr);
1450 return ret;
1451}
1452
1462
1465{
1466public:
1468 : unary_exprt(ID_bitreverse, std::move(op))
1469 {
1470 }
1471
1474 exprt lower() const;
1475};
1476
1477template <>
1479{
1480 return base.id() == ID_bitreverse;
1481}
1482
1483inline void validate_expr(const bitreverse_exprt &value)
1484{
1485 validate_operands(value, 1, "Bit-wise reverse must have one operand");
1486}
1487
1495{
1496 PRECONDITION(expr.id() == ID_bitreverse);
1497 const bitreverse_exprt &ret = static_cast<const bitreverse_exprt &>(expr);
1499 return ret;
1500}
1501
1504{
1505 PRECONDITION(expr.id() == ID_bitreverse);
1506 bitreverse_exprt &ret = static_cast<bitreverse_exprt &>(expr);
1508 return ret;
1509}
1510
1513{
1514public:
1519
1521 : binary_exprt(
1522 std::move(_lhs),
1524 std::move(_rhs),
1525 std::move(_type))
1526 {
1527 }
1528};
1529
1530template <>
1532{
1533 return base.id() == ID_saturating_plus;
1534}
1535
1536inline void validate_expr(const saturating_plus_exprt &value)
1537{
1538 validate_operands(value, 2, "saturating plus must have two operands");
1539}
1540
1548{
1550 const saturating_plus_exprt &ret =
1551 static_cast<const saturating_plus_exprt &>(expr);
1553 return ret;
1554}
1555
1558{
1560 saturating_plus_exprt &ret = static_cast<saturating_plus_exprt &>(expr);
1562 return ret;
1563}
1564
1567{
1568public:
1573};
1574
1575template <>
1577{
1578 return base.id() == ID_saturating_minus;
1579}
1580
1581inline void validate_expr(const saturating_minus_exprt &value)
1582{
1583 validate_operands(value, 2, "saturating minus must have two operands");
1584}
1585
1593{
1596 static_cast<const saturating_minus_exprt &>(expr);
1598 return ret;
1599}
1600
1603{
1605 saturating_minus_exprt &ret = static_cast<saturating_minus_exprt &>(expr);
1607 return ret;
1608}
1609
1613{
1614public:
1617 make_id(kind),
1619 {{ID_value, _lhs.type()},
1620 {"overflow-" + id2string(kind), bool_typet{}}}},
1621 {_lhs, std::move(_rhs)})
1622 {
1623 INVARIANT(
1624 valid_id(id()),
1625 "The kind used to construct overflow_result_exprt should be in the set "
1626 "of expected valid kinds.");
1627 }
1628
1631 make_id(kind),
1633 {{ID_value, _op.type()},
1634 {"overflow-" + id2string(kind), bool_typet{}}}},
1635 {_op})
1636 {
1637 INVARIANT(
1638 valid_id(id()),
1639 "The kind used to construct overflow_result_exprt should be in the set "
1640 "of expected valid kinds.");
1641 }
1642
1643 // make op0 and op1 public
1644 using exprt::op0;
1645 using exprt::op1;
1646
1647 const exprt &op2() const = delete;
1648 exprt &op2() = delete;
1649 const exprt &op3() const = delete;
1650 exprt &op3() = delete;
1651
1652 static void check(
1653 const exprt &expr,
1655 {
1657 binary_exprt::check(expr, vm);
1658
1659 if(
1661 expr.id() != ID_overflow_result_shl)
1662 {
1664 DATA_CHECK(
1665 vm,
1666 binary_expr.lhs().type() == binary_expr.rhs().type(),
1667 "operand types must match");
1668 }
1669 }
1670
1671 static void validate(
1672 const exprt &expr,
1673 const namespacet &,
1675 {
1676 check(expr, vm);
1677 }
1678
1680 static bool valid_id(const irep_idt &id)
1681 {
1682 return id == ID_overflow_result_plus || id == ID_overflow_result_mult ||
1685 }
1686
1687private:
1688 static irep_idt make_id(const irep_idt &kind)
1689 {
1690 return "overflow_result-" + id2string(kind);
1691 }
1692};
1693
1694template <>
1696{
1697 return overflow_result_exprt::valid_id(base.id());
1698}
1699
1700inline void validate_expr(const overflow_result_exprt &value)
1701{
1702 if(value.id() == ID_overflow_result_unary_minus)
1703 {
1705 value, 1, "unary overflow expression must have two operands");
1706 }
1707 else
1708 {
1710 value, 2, "binary overflow expression must have two operands");
1711 }
1712}
1713
1721{
1723 const overflow_result_exprt &ret =
1724 static_cast<const overflow_result_exprt &>(expr);
1726 return ret;
1727}
1728
1737
1741{
1742public:
1744 : unary_exprt(ID_find_first_set, std::move(_op), std::move(_type))
1745 {
1746 }
1747
1750 {
1751 }
1752
1753 static void check(
1754 const exprt &expr,
1756 {
1757 DATA_CHECK(
1758 vm,
1759 expr.operands().size() == 1,
1760 "unary expression must have a single operand");
1761 DATA_CHECK(
1762 vm,
1764 "operand must be of bitvector type");
1765 }
1766
1767 static void validate(
1768 const exprt &expr,
1769 const namespacet &,
1771 {
1772 check(expr, vm);
1773 }
1774
1777 exprt lower() const;
1778};
1779
1780template <>
1782{
1783 return base.id() == ID_find_first_set;
1784}
1785
1786inline void validate_expr(const find_first_set_exprt &value)
1787{
1788 validate_operands(value, 1, "find_first_set must have one operand");
1789}
1790
1798{
1800 const find_first_set_exprt &ret =
1801 static_cast<const find_first_set_exprt &>(expr);
1803 return ret;
1804}
1805
1808{
1810 find_first_set_exprt &ret = static_cast<find_first_set_exprt &>(expr);
1812 return ret;
1813}
1814
1821{
1822public:
1824 : unary_exprt(ID_zero_extend, std::move(_op), std::move(_type))
1825 {
1826 }
1827
1828 // a lowering to extraction or concatenation
1829 exprt lower() const;
1830};
1831
1832template <>
1834{
1835 return base.id() == ID_zero_extend;
1836}
1837
1845{
1846 PRECONDITION(expr.id() == ID_zero_extend);
1848 return static_cast<const zero_extend_exprt &>(expr);
1849}
1850
1853{
1854 PRECONDITION(expr.id() == ID_zero_extend);
1856 return static_cast<zero_extend_exprt &>(expr);
1857}
1858
1862{
1863public:
1866 {
1867 }
1868
1870 exprt lower() const;
1871};
1872
1879inline const onehot_exprt &to_onehot_expr(const exprt &expr)
1880{
1881 PRECONDITION(expr.id() == ID_onehot);
1882 onehot_exprt::check(expr);
1883 return static_cast<const onehot_exprt &>(expr);
1884}
1885
1888{
1889 PRECONDITION(expr.id() == ID_onehot);
1890 onehot_exprt::check(expr);
1891 return static_cast<onehot_exprt &>(expr);
1892}
1893
1897{
1898public:
1901 {
1902 }
1903
1905 exprt lower() const;
1906};
1907
1914inline const onehot0_exprt &to_onehot0_expr(const exprt &expr)
1915{
1916 PRECONDITION(expr.id() == ID_onehot0);
1918 return static_cast<const onehot0_exprt &>(expr);
1919}
1920
1923{
1924 PRECONDITION(expr.id() == ID_onehot0);
1926 return static_cast<onehot0_exprt &>(expr);
1927}
1928
1929#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 onehot0_exprt & to_onehot0_expr(const exprt &expr)
Cast an exprt to a onehot0_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.
const bitnand_exprt & to_bitnand_expr(const exprt &expr)
Cast an exprt to a bitnand_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< bitnand_exprt >(const exprt &base)
bool can_cast_expr< shift_exprt >(const exprt &base)
bool can_cast_expr< bitand_exprt >(const exprt &base)
bool can_cast_expr< update_bits_exprt >(const exprt &base)
bool can_cast_expr< saturating_minus_exprt >(const exprt &base)
const extractbits_exprt & to_extractbits_expr(const exprt &expr)
Cast an exprt to an extractbits_exprt.
bool can_cast_expr< popcount_exprt >(const exprt &base)
const onehot_exprt & to_onehot_expr(const exprt &expr)
Cast an exprt to a onehot_exprt.
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.
const bitnor_exprt & to_bitnor_expr(const exprt &expr)
Cast an exprt to a bitnor_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.
bool can_cast_expr< bitnor_exprt >(const exprt &base)
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.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
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
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:650
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(exprt::operandst _operands, typet _type)
bitand_exprt(const exprt &_op0, exprt _op1)
Bit-wise NAND.
bitnand_exprt(exprt _op0, exprt _op1)
bitnand_exprt(exprt::operandst _operands, typet _type)
Bit-wise NOR.
bitnor_exprt(exprt::operandst _operands, typet _type)
bitnor_exprt(exprt _op0, exprt _op1)
Bit-wise negation of bit-vectors.
bitnot_exprt(exprt op)
Bit-wise OR.
bitor_exprt(exprt::operandst _operands, typet _type)
bitor_exprt(const exprt &_op0, exprt _op1)
Reverse the order of bits in a bit-vector.
bitreverse_exprt(exprt op)
exprt lower() const
Lower a bitreverse_exprt to arithmetic and logic expressions.
Bit-wise XNOR.
bitxnor_exprt(exprt::operandst _operands, typet _type)
bitxnor_exprt(exprt _op0, exprt _op1)
Bit-wise XOR.
bitxor_exprt(exprt::operandst _operands, typet _type)
bitxor_exprt(exprt _op0, exprt _op1)
The Boolean type.
Definition std_types.h:36
The byte swap expression.
bswap_exprt(exprt _op, std::size_t bits_per_byte)
std::size_t get_bits_per_byte() const
bswap_exprt(exprt _op, std::size_t bits_per_byte, typet _type)
void set_bits_per_byte(std::size_t bits_per_byte)
Concatenation of bit-vector operands.
concatenation_exprt(operandst _operands, typet _type)
concatenation_exprt(exprt _op0, exprt _op1, typet _type)
A constant literal expression.
Definition std_expr.h:3117
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
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
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:91
A Boolean expression returning true iff the given operand consists of exactly one '0' and '1' otherwi...
onehot0_exprt(exprt _op)
exprt lower() const
lowering to extractbit
A Boolean expression returning true iff the given operand consists of exactly one '1' and '0' otherwi...
onehot_exprt(exprt _op)
exprt lower() const
lowering to extractbit
An expression returning both the result of the arithmetic operation under wrap-around semantics as we...
exprt & 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)
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
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