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:
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};
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:
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:
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);
282 return ret;
283}
284
287{
288 shift_exprt &ret = static_cast<shift_exprt &>(expr);
290 return ret;
291}
292
294class shl_exprt : public shift_exprt
295{
296public:
298 : shift_exprt(std::move(_src), ID_shl, std::move(_distance))
299 {
300 }
301
302 shl_exprt(exprt _src, const std::size_t _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);
325 return ret;
326}
327
330{
331 PRECONDITION(expr.id() == ID_shl);
332 shl_exprt &ret = static_cast<shl_exprt &>(expr);
334 return ret;
335}
336
339{
340public:
345
346 ashr_exprt(exprt _src, const std::size_t _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:
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:
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);
434 return ret;
435}
436
439{
440 PRECONDITION(expr.id() == ID_extractbit);
441 extractbit_exprt &ret = static_cast<extractbit_exprt &>(expr);
443 return ret;
444}
445
448{
449public:
458 std::move(_type),
459 {std::move(_src), std::move(_upper), std::move(_lower)})
460 {
461 }
462
464 exprt _src,
465 const std::size_t _upper,
466 const std::size_t _lower,
467 typet _type);
468
470 {
471 return op0();
472 }
473
475 {
476 return op1();
477 }
478
480 {
481 return op2();
482 }
483
484 const exprt &src() const
485 {
486 return op0();
487 }
488
489 const exprt &upper() const
490 {
491 return op1();
492 }
493
494 const exprt &lower() const
495 {
496 return op2();
497 }
498};
499
500template <>
502{
503 return base.id() == ID_extractbits;
504}
505
506inline void validate_expr(const extractbits_exprt &value)
507{
508 validate_operands(value, 3, "Extract bits must have three operands");
509}
510
518{
519 PRECONDITION(expr.id() == ID_extractbits);
520 const extractbits_exprt &ret = static_cast<const extractbits_exprt &>(expr);
522 return ret;
523}
524
527{
528 PRECONDITION(expr.id() == ID_extractbits);
529 extractbits_exprt &ret = static_cast<extractbits_exprt &>(expr);
531 return ret;
532}
533
536{
537public:
539 : binary_exprt(
540 std::move(_times),
542 std::move(_src),
543 std::move(_type))
544 {
545 }
546
548 {
549 return static_cast<constant_exprt &>(op0());
550 }
551
552 const constant_exprt &times() const
553 {
554 return static_cast<const constant_exprt &>(op0());
555 }
556
558 {
559 return op1();
560 }
561
562 const exprt &op() const
563 {
564 return op1();
565 }
566};
567
568template <>
570{
571 return base.id() == ID_replication;
572}
573
574inline void validate_expr(const replication_exprt &value)
575{
576 validate_operands(value, 2, "Bit-wise replication must have two operands");
577}
578
586{
587 PRECONDITION(expr.id() == ID_replication);
588 const replication_exprt &ret = static_cast<const replication_exprt &>(expr);
590 return ret;
591}
592
595{
596 PRECONDITION(expr.id() == ID_replication);
597 replication_exprt &ret = static_cast<replication_exprt &>(expr);
599 return ret;
600}
601
608{
609public:
614
618 {std::move(_op0), std::move(_op1)},
619 std::move(_type))
620 {
621 }
622};
623
624template <>
626{
627 return base.id() == ID_concatenation;
628}
629
637{
639 return static_cast<const concatenation_exprt &>(expr);
640}
641
644{
646 return static_cast<concatenation_exprt &>(expr);
647}
648
651{
652public:
654 : unary_exprt(ID_popcount, std::move(_op), std::move(_type))
655 {
656 }
657
658 explicit popcount_exprt(const exprt &_op)
660 {
661 }
662
665 exprt lower() const;
666};
667
668template <>
669inline bool can_cast_expr<popcount_exprt>(const exprt &base)
670{
671 return base.id() == ID_popcount;
672}
673
674inline void validate_expr(const popcount_exprt &value)
675{
676 validate_operands(value, 1, "popcount must have one operand");
677}
678
685inline const popcount_exprt &to_popcount_expr(const exprt &expr)
686{
687 PRECONDITION(expr.id() == ID_popcount);
688 const popcount_exprt &ret = static_cast<const popcount_exprt &>(expr);
690 return ret;
691}
692
695{
696 PRECONDITION(expr.id() == ID_popcount);
697 popcount_exprt &ret = static_cast<popcount_exprt &>(expr);
699 return ret;
700}
701
705{
706public:
708 : binary_predicate_exprt(std::move(_lhs), make_id(kind), std::move(_rhs))
709 {
710 INVARIANT(
711 valid_id(id()),
712 "The kind used to construct binary_overflow_exprt should be in the set "
713 "of expected valid kinds.");
714 }
715
716 static void check(
717 const exprt &expr,
719 {
720 binary_exprt::check(expr, vm);
721
722 if(expr.id() != ID_overflow_shl)
723 {
726 vm,
727 binary_expr.lhs().type() == binary_expr.rhs().type(),
728 "operand types must match");
729 }
730 }
731
732 static void validate(
733 const exprt &expr,
734 const namespacet &,
736 {
737 check(expr, vm);
738 }
739
741 static bool valid_id(const irep_idt &id)
742 {
743 return id == ID_overflow_plus || id == ID_overflow_mult ||
744 id == ID_overflow_minus || id == ID_overflow_shl;
745 }
746
747private:
748 static irep_idt make_id(const irep_idt &kind)
749 {
750 if(valid_id(kind))
751 return kind;
752 else
753 return "overflow-" + id2string(kind);
754 }
755};
756
757template <>
759{
760 return binary_overflow_exprt::valid_id(base.id());
761}
762
763inline void validate_expr(const binary_overflow_exprt &value)
764{
766 value, 2, "binary overflow expression must have two operands");
767}
768
776{
778 expr.id() == ID_overflow_plus || expr.id() == ID_overflow_mult ||
779 expr.id() == ID_overflow_minus || expr.id() == ID_overflow_shl);
781 static_cast<const binary_overflow_exprt &>(expr);
783 return ret;
784}
785
788{
790 expr.id() == ID_overflow_plus || expr.id() == ID_overflow_mult ||
791 expr.id() == ID_overflow_minus || expr.id() == ID_overflow_shl);
792 binary_overflow_exprt &ret = static_cast<binary_overflow_exprt &>(expr);
794 return ret;
795}
796
798{
799public:
804
807 exprt lower() const;
808};
809
810template <>
812{
813 return base.id() == ID_overflow_plus;
814}
815
817{
818public:
823
826 exprt lower() const;
827};
828
829template <>
831{
832 return base.id() == ID_overflow_minus;
833}
834
836{
837public:
842
845 exprt lower() const;
846};
847
848template <>
850{
851 return base.id() == ID_overflow_mult;
852}
853
862
863template <>
865{
866 return base.id() == ID_overflow_shl;
867}
868
872{
873public:
875 : unary_predicate_exprt("overflow-" + id2string(kind), std::move(_op))
876 {
877 }
878
879 static void check(
880 const exprt &expr,
882 {
883 unary_exprt::check(expr, vm);
884 }
885
886 static void validate(
887 const exprt &expr,
888 const namespacet &,
890 {
891 check(expr, vm);
892 }
893};
894
895template <>
897{
898 return base.id() == ID_overflow_unary_minus;
899}
900
901inline void validate_expr(const unary_overflow_exprt &value)
902{
904 value, 1, "unary overflow expression must have one operand");
905}
906
910{
911public:
916
917 static void check(
918 const exprt &expr,
920 {
921 unary_exprt::check(expr, vm);
922 }
923
924 static void validate(
925 const exprt &expr,
926 const namespacet &,
928 {
929 check(expr, vm);
930 }
931};
932
933template <>
935{
936 return base.id() == ID_overflow_unary_minus;
937}
938
940{
942 value, 1, "unary minus overflow expression must have one operand");
943}
944
952{
955 static_cast<const unary_overflow_exprt &>(expr);
957 return ret;
958}
959
962{
964 unary_overflow_exprt &ret = static_cast<unary_overflow_exprt &>(expr);
966 return ret;
967}
968
975{
976public:
982
987
988 bool zero_permitted() const
989 {
991 }
992
993 void zero_permitted(bool value)
994 {
995 set(ID_C_bounds_check, !value);
996 }
997
998 static void check(
999 const exprt &expr,
1001 {
1002 DATA_CHECK(
1003 vm,
1004 expr.operands().size() == 1,
1005 "unary expression must have a single operand");
1006 DATA_CHECK(
1007 vm,
1009 "operand must be of bitvector type");
1010 }
1011
1012 static void validate(
1013 const exprt &expr,
1014 const namespacet &,
1016 {
1017 check(expr, vm);
1018 }
1019
1022 exprt lower() const;
1023};
1024
1025template <>
1027{
1028 return base.id() == ID_count_leading_zeros;
1029}
1030
1032{
1033 validate_operands(value, 1, "count_leading_zeros must have one operand");
1034}
1035
1042inline const count_leading_zeros_exprt &
1044{
1047 static_cast<const count_leading_zeros_exprt &>(expr);
1049 return ret;
1050}
1051
1061
1068{
1069public:
1075
1080
1081 bool zero_permitted() const
1082 {
1083 return !get_bool(ID_C_bounds_check);
1084 }
1085
1086 void zero_permitted(bool value)
1087 {
1088 set(ID_C_bounds_check, !value);
1089 }
1090
1091 static void check(
1092 const exprt &expr,
1094 {
1095 DATA_CHECK(
1096 vm,
1097 expr.operands().size() == 1,
1098 "unary expression must have a single operand");
1099 DATA_CHECK(
1100 vm,
1102 "operand must be of bitvector type");
1103 }
1104
1105 static void validate(
1106 const exprt &expr,
1107 const namespacet &,
1109 {
1110 check(expr, vm);
1111 }
1112
1115 exprt lower() const;
1116};
1117
1118template <>
1120{
1121 return base.id() == ID_count_trailing_zeros;
1122}
1123
1125{
1126 validate_operands(value, 1, "count_trailing_zeros must have one operand");
1127}
1128
1135inline const count_trailing_zeros_exprt &
1137{
1140 static_cast<const count_trailing_zeros_exprt &>(expr);
1142 return ret;
1143}
1144
1154
1157{
1158public:
1160 : unary_exprt(ID_bitreverse, std::move(op))
1161 {
1162 }
1163
1166 exprt lower() const;
1167};
1168
1169template <>
1171{
1172 return base.id() == ID_bitreverse;
1173}
1174
1175inline void validate_expr(const bitreverse_exprt &value)
1176{
1177 validate_operands(value, 1, "Bit-wise reverse must have one operand");
1178}
1179
1187{
1188 PRECONDITION(expr.id() == ID_bitreverse);
1189 const bitreverse_exprt &ret = static_cast<const bitreverse_exprt &>(expr);
1191 return ret;
1192}
1193
1196{
1197 PRECONDITION(expr.id() == ID_bitreverse);
1198 bitreverse_exprt &ret = static_cast<bitreverse_exprt &>(expr);
1200 return ret;
1201}
1202
1205{
1206public:
1211
1213 : binary_exprt(
1214 std::move(_lhs),
1216 std::move(_rhs),
1217 std::move(_type))
1218 {
1219 }
1220};
1221
1222template <>
1224{
1225 return base.id() == ID_saturating_plus;
1226}
1227
1228inline void validate_expr(const saturating_plus_exprt &value)
1229{
1230 validate_operands(value, 2, "saturating plus must have two operands");
1231}
1232
1240{
1242 const saturating_plus_exprt &ret =
1243 static_cast<const saturating_plus_exprt &>(expr);
1245 return ret;
1246}
1247
1250{
1252 saturating_plus_exprt &ret = static_cast<saturating_plus_exprt &>(expr);
1254 return ret;
1255}
1256
1259{
1260public:
1265};
1266
1267template <>
1269{
1270 return base.id() == ID_saturating_minus;
1271}
1272
1273inline void validate_expr(const saturating_minus_exprt &value)
1274{
1275 validate_operands(value, 2, "saturating minus must have two operands");
1276}
1277
1285{
1288 static_cast<const saturating_minus_exprt &>(expr);
1290 return ret;
1291}
1292
1295{
1297 saturating_minus_exprt &ret = static_cast<saturating_minus_exprt &>(expr);
1299 return ret;
1300}
1301
1305{
1306public:
1309 make_id(kind),
1311 {{ID_value, _lhs.type()},
1312 {"overflow-" + id2string(kind), bool_typet{}}}},
1313 {_lhs, std::move(_rhs)})
1314 {
1315 INVARIANT(
1316 valid_id(id()),
1317 "The kind used to construct overflow_result_exprt should be in the set "
1318 "of expected valid kinds.");
1319 }
1320
1323 make_id(kind),
1325 {{ID_value, _op.type()},
1326 {"overflow-" + id2string(kind), bool_typet{}}}},
1327 {_op})
1328 {
1329 INVARIANT(
1330 valid_id(id()),
1331 "The kind used to construct overflow_result_exprt should be in the set "
1332 "of expected valid kinds.");
1333 }
1334
1335 // make op0 and op1 public
1336 using exprt::op0;
1337 using exprt::op1;
1338
1339 const exprt &op2() const = delete;
1340 exprt &op2() = delete;
1341 const exprt &op3() const = delete;
1342 exprt &op3() = delete;
1343
1344 static void check(
1345 const exprt &expr,
1347 {
1349 binary_exprt::check(expr, vm);
1350
1351 if(
1353 expr.id() != ID_overflow_result_shl)
1354 {
1356 DATA_CHECK(
1357 vm,
1358 binary_expr.lhs().type() == binary_expr.rhs().type(),
1359 "operand types must match");
1360 }
1361 }
1362
1363 static void validate(
1364 const exprt &expr,
1365 const namespacet &,
1367 {
1368 check(expr, vm);
1369 }
1370
1372 static bool valid_id(const irep_idt &id)
1373 {
1374 return id == ID_overflow_result_plus || id == ID_overflow_result_mult ||
1377 }
1378
1379private:
1380 static irep_idt make_id(const irep_idt &kind)
1381 {
1382 return "overflow_result-" + id2string(kind);
1383 }
1384};
1385
1386template <>
1388{
1389 return overflow_result_exprt::valid_id(base.id());
1390}
1391
1392inline void validate_expr(const overflow_result_exprt &value)
1393{
1394 if(value.id() == ID_overflow_result_unary_minus)
1395 {
1397 value, 1, "unary overflow expression must have two operands");
1398 }
1399 else
1400 {
1402 value, 2, "binary overflow expression must have two operands");
1403 }
1404}
1405
1413{
1415 const overflow_result_exprt &ret =
1416 static_cast<const overflow_result_exprt &>(expr);
1418 return ret;
1419}
1420
1429
1433{
1434public:
1436 : unary_exprt(ID_find_first_set, std::move(_op), std::move(_type))
1437 {
1438 }
1439
1442 {
1443 }
1444
1445 static void check(
1446 const exprt &expr,
1448 {
1449 DATA_CHECK(
1450 vm,
1451 expr.operands().size() == 1,
1452 "unary expression must have a single operand");
1453 DATA_CHECK(
1454 vm,
1456 "operand must be of bitvector type");
1457 }
1458
1459 static void validate(
1460 const exprt &expr,
1461 const namespacet &,
1463 {
1464 check(expr, vm);
1465 }
1466
1469 exprt lower() const;
1470};
1471
1472template <>
1474{
1475 return base.id() == ID_find_first_set;
1476}
1477
1478inline void validate_expr(const find_first_set_exprt &value)
1479{
1480 validate_operands(value, 1, "find_first_set must have one operand");
1481}
1482
1490{
1492 const find_first_set_exprt &ret =
1493 static_cast<const find_first_set_exprt &>(expr);
1495 return ret;
1496}
1497
1500{
1502 find_first_set_exprt &ret = static_cast<find_first_set_exprt &>(expr);
1504 return ret;
1505}
1506
1507#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.
bool can_cast_expr< shift_exprt >(const exprt &base)
bool can_cast_expr< bitand_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< 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 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.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
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:583
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:595
exprt & op0()
Definition expr.h:125
exprt & op1()
Definition expr.h:128
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:676
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:2942
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:39
Base class for all expressions.
Definition expr.h:336
exprt & op0()
Definition expr.h:125
exprt & op1()
Definition expr.h:128
exprt & op2()
Definition expr.h:131
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:246
exprt & op0()
Definition expr.h:125
exprt & op1()
Definition expr.h:128
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 & upper() const
extractbits_exprt(exprt _src, exprt _upper, exprt _lower, typet _type)
Extract the bits [_lower .
const exprt & lower() const
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:420
void set_size_t(const irep_idt &name, const std::size_t value)
Definition irep.cpp:86
const irep_idt & id() const
Definition irep.h:396
Logical right shift.
lshr_exprt(exprt _src, const std::size_t _distance)
lshr_exprt(exprt _src, exprt _distance)
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:857
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
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:314
const exprt & op() const
Definition std_expr.h:326
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:528
void validate_operands(const exprt &value, exprt::operandst::size_type number, const char *message, bool allow_more=false)
Definition expr_cast.h:250
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
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:660
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition std_expr.h:361
#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