52 template <
typename factoryt>
56 const factoryt &factory)
59 const auto operand_terms =
61 return converted.at(expr);
63 return std::accumulate(
64 ++operand_terms.begin(),
66 *operand_terms.begin(),
74 template <
typename target_typet>
79 return can_cast_type<target_typet>(operand.type());
102 if(
const auto bool_type = type_try_dynamic_cast<bool_typet>(type))
106 if(
const auto bitvector_type = type_try_dynamic_cast<bitvector_typet>(type))
110 if(
const auto array_type = type_try_dynamic_cast<array_typet>(type))
153 const std::size_t c_bool_width = to_type.
get_width();
160 static std::function<std::function<smt_termt(smt_termt)>(std::size_t)>
179 if(
const auto to_fixedbv_type = type_try_dynamic_cast<fixedbv_typet>(to_type))
182 "Generation of SMT formula for type cast to fixed-point bitvector "
186 if(
const auto to_floatbv_type = type_try_dynamic_cast<floatbv_typet>(to_type))
189 "Generation of SMT formula for type cast to floating-point bitvector "
193 const std::size_t from_width =
from_type.get_width();
194 const std::size_t to_width = to_type.
get_width();
195 if(to_width == from_width)
197 if(to_width < from_width)
199 const std::size_t extension_size = to_width - from_width;
227 if(
const auto bitvector = type_try_dynamic_cast<bitvector_typet>(
from_type))
231 "Generation of SMT formula for type cast to bit vector from type: " +
238 "Generation of SMT formula for type cast to bit vector from type: " +
252 return *converter.result;
259 const auto &from_term = converted.at(cast.
op());
262 if(
const auto bool_type = type_try_dynamic_cast<bool_typet>(to_type))
264 if(
const auto c_bool_type = type_try_dynamic_cast<c_bool_typet>(to_type))
266 if(
const auto bit_vector = type_try_dynamic_cast<bitvector_typet>(to_type))
269 "Generation of SMT formula for type cast expression: " + cast.
pretty());
277 "Generation of SMT formula for floating point type cast expression: " +
286 "Generation of SMT formula for struct construction expression: " +
287 struct_construction.
pretty());
295 "Generation of SMT formula for union construction expression: " +
296 union_construction.
pretty());
316 const auto &width = bit_vector_sort.
bit_width();
326 "Conversion of array SMT literal " + array_sort.
pretty());
334 const size_t bit_width =
335 type_checked_cast<pointer_typet>(constant_literal.
type()).get_width();
338 const auto address = 0;
347 const auto value = numeric_cast_v<mp_integer>(constant_literal);
352 sort.accept(converter);
360 if(operands_are_of_type<bitvector_typet>(concatenation))
366 "Generation of SMT formula for concatenation expression: " +
374 if(operands_are_of_type<bitvector_typet>(bitwise_and_expr))
382 "Generation of SMT formula for bitwise and expression: " +
383 bitwise_and_expr.
pretty());
391 if(operands_are_of_type<bitvector_typet>(bitwise_or_expr))
399 "Generation of SMT formula for bitwise or expression: " +
400 bitwise_or_expr.
pretty());
408 if(operands_are_of_type<bitvector_typet>(
bitwise_xor))
416 "Generation of SMT formula for bitwise xor expression: " +
432 "Generation of SMT formula for bitnot_exprt: " + bitwise_not.
pretty());
447 "Generation of SMT formula for unary minus expression: " +
457 "Generation of SMT formula for unary plus expression: " +
466 "Generation of SMT formula for \"is negative\" expression: " +
475 converted.at(if_expression.
cond()),
509 converted.at(implies.
op0()), converted.at(implies.
op1()));
524 converted.at(equal.
op0()), converted.at(equal.
op1()));
532 converted.at(not_equal.
op0()), converted.at(not_equal.
op1()));
540 "Generation of SMT formula for floating point equality expression: " +
549 "Generation of SMT formula for floating point not equal expression: " +
550 float_not_equal.
pretty());
553 template <
typename unsigned_factory_typet,
typename signed_factory_typet>
556 const unsigned_factory_typet &unsigned_factory,
557 const signed_factory_typet &signed_factory,
561 const auto &lhs = converted.at(binary_relation.
lhs());
562 const auto &rhs = converted.at(binary_relation.
rhs());
563 const typet operand_type = binary_relation.
lhs().
type();
572 const auto lhs_type_is_pointer =
574 const auto rhs_type_is_pointer =
577 lhs_type_is_pointer && rhs_type_is_pointer,
578 "pointer comparison requires that both operand types are pointers.");
579 return unsigned_factory(lhs, rhs);
584 return unsigned_factory(lhs, rhs);
586 return signed_factory(lhs, rhs);
590 "Generation of SMT formula for relational expression: " +
591 binary_relation.
pretty());
598 if(
const auto greater_than = expr_try_dynamic_cast<greater_than_exprt>(expr))
607 const auto greater_than_or_equal =
608 expr_try_dynamic_cast<greater_than_or_equal_exprt>(expr))
611 *greater_than_or_equal,
616 if(
const auto less_than = expr_try_dynamic_cast<less_than_exprt>(expr))
625 const auto less_than_or_equal =
626 expr_try_dynamic_cast<less_than_or_equal_exprt>(expr))
644 return can_cast_type<integer_bitvector_typet>(operand.type());
654 "We are only handling a binary version of plus when it has a pointer "
659 for(
auto &operand : plus.
operands())
675 "An addition expression with both operands being pointers when they are "
676 "not dereferenced is malformed");
679 *type_try_dynamic_cast<pointer_typet>(pointer.
type());
681 const auto pointer_size = pointer_sizes.at(base_type);
684 converted.at(pointer),
690 "Generation of SMT formula for plus expression: " + plus.
pretty());
699 const bool both_operands_bitvector =
706 const bool both_operands_pointers = lhs_is_pointer && rhs_is_pointer;
710 const bool one_operand_pointer = lhs_is_pointer || rhs_is_pointer;
712 if(both_operands_bitvector)
715 converted.at(minus.
lhs()), converted.at(minus.
rhs()));
717 else if(both_operands_pointers)
722 lhs_base_type == rhs_base_type,
723 "only pointers of the same object type can be subtracted.");
726 converted.at(minus.
lhs()), converted.at(minus.
rhs())),
727 pointer_sizes.at(lhs_base_type));
729 else if(one_operand_pointer)
735 "minus expressions of pointer and integer expect lhs to be the pointer");
739 converted.at(minus.
lhs()),
741 converted.at(minus.
rhs()), pointer_sizes.at(lhs_base_type)));
746 "Generation of SMT formula for minus expression: " + minus.
pretty());
757 const bool both_operands_bitvector =
761 const bool both_operands_unsigned =
765 if(both_operands_bitvector)
767 if(both_operands_unsigned)
779 "Generation of SMT formula for divide expression: " + divide.
pretty());
790 "Generation of SMT formula for floating point operation expression: " +
791 float_operation.
pretty());
798 const smt_termt &lhs = converted.at(truncation_modulo.
lhs());
799 const smt_termt &rhs = converted.at(truncation_modulo.
rhs());
801 const bool both_operands_bitvector =
805 const bool both_operands_unsigned =
809 if(both_operands_bitvector)
811 if(both_operands_unsigned)
823 "Generation of SMT formula for remainder (modulus) expression: " +
824 truncation_modulo.
pretty());
833 "Generation of SMT formula for euclidean modulo expression: " +
834 euclidean_modulo.
pretty());
845 return can_cast_type<integer_bitvector_typet>(operand.type());
854 "Generation of SMT formula for multiply expression: " +
871 const auto type = type_try_dynamic_cast<pointer_typet>(address_of.
type());
873 type,
"Result of the address_of operator should have pointer type.");
875 const auto object = object_map.find(base);
877 object != object_map.end(),
878 "Objects should be tracked before converting their address to SMT terms");
879 const std::size_t object_id =
object->second.unique_id;
881 const std::size_t max_objects = std::size_t(1) << object_bits;
882 if(object_id >= max_objects)
885 "too many addressed objects: maximum number of objects is set to 2^n=" +
888 "use the `--object-bits n` option to increase the maximum number"};
893 type->get_width() > object_bits,
894 "Pointer should be wider than object_bits in order to allow for offset "
896 const size_t offset_bits = type->get_width() - object_bits;
899 expr_try_dynamic_cast<symbol_exprt>(address_of.
object()))
905 "Generation of SMT formula for address of expression: " +
924 "Generation of SMT formula for array comprehension expression: " +
925 array_comprehension.
pretty());
937 template <
typename factoryt,
typename shiftt>
939 const factoryt &factory,
943 const smt_termt &first_operand = converted.at(shift.op0());
944 const smt_termt &second_operand = converted.at(shift.op1());
945 const auto first_bit_vector_sort =
947 const auto second_bit_vector_sort =
950 first_bit_vector_sort && second_bit_vector_sort,
951 "Shift expressions are expected to have bit vector operands.");
953 shift.type() == shift.op0().type(),
954 "Shift expression type must be equals to first operand type.");
955 const std::size_t first_width = first_bit_vector_sort->bit_width();
956 const std::size_t second_width = second_bit_vector_sort->
bit_width();
957 if(first_width > second_width)
964 else if(first_width < second_width)
966 const auto result = factory(
974 return factory(first_operand, second_operand);
983 if(
const auto left_shift = expr_try_dynamic_cast<shl_exprt>(shift))
988 if(
const auto right_logical_shift = expr_try_dynamic_cast<lshr_exprt>(shift))
992 *right_logical_shift,
995 if(
const auto right_arith_shift = expr_try_dynamic_cast<ashr_exprt>(shift))
1003 "Generation of SMT formula for shift expression: " + shift.
pretty());
1011 for(
auto it = ++with.
operands().begin(); it != with.
operands().end(); it += 2)
1013 const smt_termt &index_term = converted.at(it[0]);
1014 const smt_termt &value_term = converted.at(it[1]);
1029 "Generation of SMT formula for with expression: " + with.
pretty());
1037 "Generation of SMT formula for update expression: " + update.
pretty());
1045 "Generation of SMT formula for member extraction expression: " +
1046 member_extraction.
pretty());
1057 pointer_sort,
"Pointers should be encoded as bit vector sorted terms.");
1058 const std::size_t pointer_width = pointer_sort->bit_width();
1059 return apply_is_dynamic_object(
1072 type_try_dynamic_cast<bitvector_typet>(pointer_expr.
type());
1077 width >= object_bits,
1078 "Width should be at least as big as the number of object bits.");
1081 width - 1, width - object_bits)(converted.at(pointer_expr));
1096 "Generation of SMT formula for string constant expression: " +
1097 string_constant.
pretty());
1105 "Generation of SMT formula for extract bit expression: " +
1113 const smt_termt &from = converted.at(extract_bits.
src());
1114 const auto bit_vector_sort =
1117 bit_vector_sort,
"Extract can only be applied to bit vector terms.");
1118 const auto index_value = numeric_cast<std::size_t>(extract_bits.
index());
1121 *index_value + bit_vector_sort->bit_width() - 1, *index_value)(from);
1123 "Generation of SMT formula for extract bits expression: " +
1132 "Generation of SMT formula for bit vector replication expression: " +
1141 "Generation of SMT formula for byte extract expression: " +
1142 byte_extraction.
pretty());
1150 "Generation of SMT formula for byte update expression: " +
1159 "Generation of SMT formula for absolute value of expression: " +
1160 absolute_value_of.
pretty());
1168 "Generation of SMT formula for is not a number expression: " +
1177 "Generation of SMT formula for is finite expression: " +
1178 is_finite_expr.
pretty());
1186 "Generation of SMT formula for is infinite expression: " +
1187 is_infinite_expr.
pretty());
1195 "Generation of SMT formula for is infinite expression: " +
1196 is_normal_expr.
pretty());
1207 "Most significant bit can only be extracted from bit vector terms.");
1208 const size_t most_significant_bit_index = bit_vector_sort->bit_width() - 1;
1210 most_significant_bit_index, most_significant_bit_index);
1219 const smt_termt &left = converted.at(plus_overflow.
lhs());
1220 const smt_termt &right = converted.at(plus_overflow.
rhs());
1221 if(operands_are_of_type<unsignedbv_typet>(plus_overflow))
1227 if(operands_are_of_type<signedbv_typet>(plus_overflow))
1240 "Generation of SMT formula for plus overflow expression: " +
1248 const smt_termt &left = converted.at(minus_overflow.
lhs());
1249 const smt_termt &right = converted.at(minus_overflow.
rhs());
1250 if(operands_are_of_type<unsignedbv_typet>(minus_overflow))
1254 if(operands_are_of_type<signedbv_typet>(minus_overflow))
1272 "Generation of SMT formula for minus overflow expression: " +
1273 minus_overflow.
pretty());
1281 const auto &operand_type = mult_overflow.
lhs().
type();
1282 const smt_termt &left = converted.at(mult_overflow.
lhs());
1283 const smt_termt &right = converted.at(mult_overflow.
rhs());
1285 const auto unsigned_type =
1286 type_try_dynamic_cast<unsignedbv_typet>(operand_type))
1288 const std::size_t width = unsigned_type->get_width();
1295 const auto signed_type =
1296 type_try_dynamic_cast<signedbv_typet>(operand_type))
1300 const std::size_t width = signed_type->get_width();
1302 const auto multiplication =
1315 "Generation of SMT formula for multiply overflow expression: " +
1325 INVARIANT(type,
"Pointer object should have a bitvector-based type.");
1326 const auto converted_expr = converted.at(
pointer_object.pointer());
1327 const std::size_t width = type->get_width();
1330 width >= object_bits,
1331 "Width should be at least as big as the number of object bits.");
1332 const std::size_t ext = width - object_bits;
1334 width - 1, width - object_bits)(converted_expr);
1348 INVARIANT(type,
"Pointer offset should have a bitvector-based type.");
1349 const auto converted_expr = converted.at(
pointer_offset.pointer());
1350 const std::size_t width = type->get_width();
1352 if(offset_bits > width)
1353 offset_bits = width;
1354 const auto extract_op =
1356 if(width > offset_bits)
1368 "Generation of SMT formula for shift left overflow expression: " +
1387 "Generation of SMT formula for literal expression: " + literal.
pretty());
1395 "Generation of SMT formula for for all expression: " + for_all.
pretty());
1403 "Generation of SMT formula for exists expression: " +
exists.pretty());
1411 "Generation of SMT formula for vector expression: " + vector.
pretty());
1422 pointer_sort,
"Pointers should be encoded as bit vector sorted terms.");
1423 const std::size_t pointer_width = pointer_sort->bit_width();
1424 return call_object_size(
1434 "Generation of SMT formula for let expression: " + let.
pretty());
1442 "Generation of SMT formula for byte swap expression: " +
1451 "Generation of SMT formula for population count expression: " +
1452 population_count.
pretty());
1460 "Generation of SMT formula for count leading zeros expression: " +
1461 count_leading_zeros.
pretty());
1469 "Generation of SMT formula for count trailing zeros expression: " +
1470 count_trailing_zeros.
pretty());
1478 "prophecy_r_or_w_ok expression should have been lowered by the decision "
1479 "procedure before conversion to smt terms");
1487 "prophecy_pointer_in_range expression should have been lowered by the "
1488 "decision procedure before conversion to smt terms");
1499 if(
const auto symbol = expr_try_dynamic_cast<symbol_exprt>(expr))
1503 if(
const auto nondet = expr_try_dynamic_cast<nondet_symbol_exprt>(expr))
1507 if(
const auto cast = expr_try_dynamic_cast<typecast_exprt>(expr))
1512 const auto float_cast = expr_try_dynamic_cast<floatbv_typecast_exprt>(expr))
1516 if(
const auto struct_construction = expr_try_dynamic_cast<struct_exprt>(expr))
1520 if(
const auto union_construction = expr_try_dynamic_cast<union_exprt>(expr))
1524 if(
const auto constant_literal = expr_try_dynamic_cast<constant_exprt>(expr))
1529 const auto concatenation = expr_try_dynamic_cast<concatenation_exprt>(expr))
1533 if(
const auto bitwise_and_expr = expr_try_dynamic_cast<bitand_exprt>(expr))
1537 if(
const auto bitwise_or_expr = expr_try_dynamic_cast<bitor_exprt>(expr))
1541 if(
const auto bitwise_xor = expr_try_dynamic_cast<bitxor_exprt>(expr))
1545 if(
const auto bitwise_not = expr_try_dynamic_cast<bitnot_exprt>(expr))
1549 if(
const auto unary_minus = expr_try_dynamic_cast<unary_minus_exprt>(expr))
1553 if(
const auto unary_plus = expr_try_dynamic_cast<unary_plus_exprt>(expr))
1557 if(
const auto is_negative = expr_try_dynamic_cast<sign_exprt>(expr))
1561 if(
const auto if_expression = expr_try_dynamic_cast<if_exprt>(expr))
1565 if(
const auto and_expression = expr_try_dynamic_cast<and_exprt>(expr))
1569 if(
const auto or_expression = expr_try_dynamic_cast<or_exprt>(expr))
1573 if(
const auto xor_expression = expr_try_dynamic_cast<xor_exprt>(expr))
1577 if(
const auto implies = expr_try_dynamic_cast<implies_exprt>(expr))
1581 if(
const auto logical_not = expr_try_dynamic_cast<not_exprt>(expr))
1585 if(
const auto equal = expr_try_dynamic_cast<equal_exprt>(expr))
1589 if(
const auto not_equal = expr_try_dynamic_cast<notequal_exprt>(expr))
1594 const auto float_equal =
1595 expr_try_dynamic_cast<ieee_float_equal_exprt>(expr))
1600 const auto float_not_equal =
1601 expr_try_dynamic_cast<ieee_float_notequal_exprt>(expr))
1606 const auto converted_relational =
1609 return *converted_relational;
1611 if(
const auto plus = expr_try_dynamic_cast<plus_exprt>(expr))
1615 if(
const auto minus = expr_try_dynamic_cast<minus_exprt>(expr))
1619 if(
const auto divide = expr_try_dynamic_cast<div_exprt>(expr))
1624 const auto float_operation =
1625 expr_try_dynamic_cast<ieee_float_op_exprt>(expr))
1629 if(
const auto truncation_modulo = expr_try_dynamic_cast<mod_exprt>(expr))
1634 const auto euclidean_modulo =
1635 expr_try_dynamic_cast<euclidean_mod_exprt>(expr))
1639 if(
const auto multiply = expr_try_dynamic_cast<mult_exprt>(expr))
1644 else if(expr.
id() == ID_floatbv_rem)
1649 if(
const auto address_of = expr_try_dynamic_cast<address_of_exprt>(expr))
1653 if(
const auto array_of = expr_try_dynamic_cast<array_of_exprt>(expr))
1658 const auto array_comprehension =
1659 expr_try_dynamic_cast<array_comprehension_exprt>(expr))
1663 if(
const auto index = expr_try_dynamic_cast<index_exprt>(expr))
1667 if(
const auto shift = expr_try_dynamic_cast<shift_exprt>(expr))
1671 if(
const auto with = expr_try_dynamic_cast<with_exprt>(expr))
1675 if(
const auto update = expr_try_dynamic_cast<update_exprt>(expr))
1679 if(
const auto member_extraction = expr_try_dynamic_cast<member_exprt>(expr))
1685 expr_try_dynamic_cast<pointer_offset_exprt>(expr))
1691 expr_try_dynamic_cast<pointer_object_exprt>(expr))
1696 const auto is_dynamic_object =
1697 expr_try_dynamic_cast<is_dynamic_object_exprt>(expr))
1700 *is_dynamic_object, converted, apply_is_dynamic_object);
1703 const auto is_invalid_pointer =
1704 expr_try_dynamic_cast<is_invalid_pointer_exprt>(expr))
1708 if(
const auto string_constant = expr_try_dynamic_cast<string_constantt>(expr))
1712 if(
const auto extract_bit = expr_try_dynamic_cast<extractbit_exprt>(expr))
1716 if(
const auto extract_bits = expr_try_dynamic_cast<extractbits_exprt>(expr))
1720 if(
const auto replication = expr_try_dynamic_cast<replication_exprt>(expr))
1725 const auto byte_extraction =
1726 expr_try_dynamic_cast<byte_extract_exprt>(expr))
1730 if(
const auto byte_update = expr_try_dynamic_cast<byte_update_exprt>(expr))
1734 if(
const auto absolute_value_of = expr_try_dynamic_cast<abs_exprt>(expr))
1738 if(
const auto is_nan_expr = expr_try_dynamic_cast<isnan_exprt>(expr))
1742 if(
const auto is_finite_expr = expr_try_dynamic_cast<isfinite_exprt>(expr))
1746 if(
const auto is_infinite_expr = expr_try_dynamic_cast<isinf_exprt>(expr))
1750 if(
const auto is_normal_expr = expr_try_dynamic_cast<isnormal_exprt>(expr))
1755 const auto plus_overflow = expr_try_dynamic_cast<plus_overflow_exprt>(expr))
1760 const auto minus_overflow =
1761 expr_try_dynamic_cast<minus_overflow_exprt>(expr))
1766 const auto mult_overflow = expr_try_dynamic_cast<mult_overflow_exprt>(expr))
1770 if(
const auto shl_overflow = expr_try_dynamic_cast<shl_overflow_exprt>(expr))
1774 if(
const auto array_construction = expr_try_dynamic_cast<array_exprt>(expr))
1778 if(
const auto literal = expr_try_dynamic_cast<literal_exprt>(expr))
1782 if(
const auto for_all = expr_try_dynamic_cast<forall_exprt>(expr))
1786 if(
const auto exists = expr_try_dynamic_cast<exists_exprt>(expr))
1790 if(
const auto vector = expr_try_dynamic_cast<vector_exprt>(expr))
1794 if(
const auto object_size = expr_try_dynamic_cast<object_size_exprt>(expr))
1798 if(
const auto let = expr_try_dynamic_cast<let_exprt>(expr))
1803 expr.
id() != ID_constraint_select_one,
1804 "constraint_select_one is not expected in smt conversion: " +
1806 if(
const auto byte_swap = expr_try_dynamic_cast<bswap_exprt>(expr))
1810 if(
const auto population_count = expr_try_dynamic_cast<popcount_exprt>(expr))
1815 const auto count_leading_zeros =
1816 expr_try_dynamic_cast<count_leading_zeros_exprt>(expr))
1821 const auto count_trailing_zeros =
1822 expr_try_dynamic_cast<count_trailing_zeros_exprt>(expr))
1827 const auto prophecy_r_or_w_ok =
1828 expr_try_dynamic_cast<prophecy_r_or_w_ok_exprt>(expr))
1833 const auto prophecy_pointer_in_range =
1834 expr_try_dynamic_cast<prophecy_pointer_in_range_exprt>(expr))
1840 "Generation of SMT formula for unknown kind of expression: " +
1844 #ifndef CPROVER_INVARIANT_DO_NOT_CHECK
1845 template <
typename functiont>
1859 template <
typename functiont>
1869 const auto address_of_expr = expr_try_dynamic_cast<address_of_exprt>(expr);
1870 if(!address_of_expr)
1872 const auto array_index_expr =
1873 expr_try_dynamic_cast<index_exprt>(address_of_expr->object());
1874 if(!array_index_expr)
1878 array_index_expr->array(),
1879 type_checked_cast<pointer_typet>(address_of_expr->type())},
1880 array_index_expr->index()};
1890 std::function<
bool(
const exprt &)> filter,
1891 std::function<
void(
const exprt &)> visitor)
1896 bool operands_pushed;
1897 explicit stack_entryt(
const exprt *_e) : e(_e), operands_pushed(
false)
1902 std::stack<stack_entryt> stack;
1904 stack.emplace(&_expr);
1906 while(!stack.empty())
1908 auto &top = stack.top();
1909 if(top.operands_pushed)
1917 top.operands_pushed =
true;
1919 for(
auto &op : top.e->operands())
1932 #ifndef CPROVER_INVARIANT_DO_NOT_CHECK
1933 static bool in_conversion =
false;
1936 "Conversion of expr to smt should be non-recursive. "
1937 "Re-entrance found in conversion of " +
1939 in_conversion =
true;
1940 const auto end_conversion =
at_scope_exit([&]() { in_conversion =
false; });
1946 [](
const exprt &expr) {
1951 const auto address_of = expr_try_dynamic_cast<address_of_exprt>(expr);
1956 [&](
const exprt &expr) {
1957 const auto find_result = sub_expression_map.find(expr);
1958 if(find_result != sub_expression_map.cend())
1967 sub_expression_map.emplace_hint(find_result, expr, std::move(term));
1969 return std::move(sub_expression_map.at(lowered_expr));
API to expression classes for bitvectors.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
bool can_cast_type< signedbv_typet >(const typet &type)
Check whether a reference to a typet is a signedbv_typet.
bool can_cast_type< integer_bitvector_typet >(const typet &type)
Check whether a reference to a typet is an integer_bitvector_typet.
bool can_cast_type< bv_typet >(const typet &type)
Check whether a reference to a typet is a bv_typet.
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
bool can_cast_type< unsignedbv_typet >(const typet &type)
Check whether a reference to a typet is a unsignedbv_typet.
Expression classes for byte-level operators.
pointer_typet pointer_type(const typet &subtype)
Operator to return the address of an object.
Thrown when an unexpected error occurs during the analysis (e.g., when the SAT solver returns an erro...
Expression to define a mapping from an argument (index) to elements.
Array constructor from list of elements.
Array constructor from single element.
typet index_type() const
The type of the index expressions into any instance of this type.
const typet & element_type() const
The type of the elements of the array.
A base class for relations, i.e., binary predicates whose two operands have the same type.
Bit-wise negation of bit-vectors.
Base class of fixed-width bit-vector types.
std::size_t get_width() const
The byte swap expression.
Expression corresponding to op() where the bytes starting at position offset (given in number of byte...
Concatenation of bit-vector operands.
struct configt::bv_encodingt bv_encoding
A constant literal expression.
const irep_idt & get_value() const
The count leading zeros (counting the number of zero bits starting from the most-significant bit) exp...
The count trailing zeros (counting the number of zero bits starting from the least-significant bit) e...
Boute's Euclidean definition of Modulo – to match SMT-LIB2.
Base class for all expressions.
bool is_true() const
Return whether the expression is a constant representing true.
void visit_pre(std::function< void(exprt &)>)
typet & type()
Return the type of the expression.
Semantic type conversion from/to floating-point formats.
IEEE-floating-point equality.
IEEE floating-point disequality.
IEEE floating-point operations These have two data operands (op0 and op1) and one rounding mode (op2)...
The trinary if-then-else operator.
Unbounded, signed integers (mathematical integers, not bitvectors)
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
const irep_idt & id() const
Evaluates to true if the operand is a pointer to a dynamic object.
Evaluates to true if the operand is finite.
Evaluates to true if the operand is infinite.
Evaluates to true if the operand is NaN.
Evaluates to true if the operand is a normal number.
Extract member of struct or union.
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
Binary multiplication Associativity is not specified.
A base class for multi-ary expressions Associativity is not specified.
Expression to hold a nondeterministic choice.
const irep_idt & get_identifier() const
Expression for finding the size (in bytes) of the object a pointer points to.
The plus expression Associativity is not specified.
A numerical identifier for the object a pointer points to.
The offset (in bytes) of a pointer relative to the object.
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
const typet & base_type() const
The type of the data what we point to.
The popcount (counting the number of bits set to 1) expression.
pointer_in_range (see pointer_in_range_exprt) with prophecy expressions to encode whether a pointer r...
A base class for a predicate that indicates that an address range is ok to read or write or both.
A base class for shift and rotate operators.
Sign of an expression Predicate is true if _op is negative, false otherwise.
static const smt_function_application_termt::factoryt< storet > store
static const smt_function_application_termt::factoryt< selectt > select
std::size_t bit_width() const
static const smt_function_application_termt::factoryt< ort > make_or
static const smt_function_application_termt::factoryt< unsigned_less_than_or_equalt > unsigned_less_than_or_equal
static const smt_function_application_termt::factoryt< signed_less_than_or_equalt > signed_less_than_or_equal
static const smt_function_application_termt::factoryt< addt > add
static const smt_function_application_termt::factoryt< arithmetic_shift_rightt > arithmetic_shift_right
static const smt_function_application_termt::factoryt< signed_greater_than_or_equalt > signed_greater_than_or_equal
static const smt_function_application_termt::factoryt< unsigned_greater_thant > unsigned_greater_than
static const smt_function_application_termt::factoryt< unsigned_remaindert > unsigned_remainder
static const smt_function_application_termt::factoryt< unsigned_greater_than_or_equalt > unsigned_greater_than_or_equal
static const smt_function_application_termt::factoryt< xort > make_xor
static const smt_function_application_termt::factoryt< nott > make_not
static const smt_function_application_termt::factoryt< shift_leftt > shift_left
static const smt_function_application_termt::factoryt< multiplyt > multiply
static smt_function_application_termt::factoryt< sign_extendt > sign_extend(std::size_t i)
static const smt_function_application_termt::factoryt< signed_less_thant > signed_less_than
static smt_function_application_termt::factoryt< zero_extendt > zero_extend(std::size_t i)
static smt_function_application_termt::factoryt< extractt > extract(std::size_t i, std::size_t j)
Makes a factory for extract function applications.
static const smt_function_application_termt::factoryt< signed_greater_thant > signed_greater_than
static const smt_function_application_termt::factoryt< logical_shift_rightt > logical_shift_right
static const smt_function_application_termt::factoryt< negatet > negate
Arithmetic negation in two's complement.
static const smt_function_application_termt::factoryt< concatt > concat
static const smt_function_application_termt::factoryt< unsigned_dividet > unsigned_divide
static const smt_function_application_termt::factoryt< unsigned_less_thant > unsigned_less_than
static const smt_function_application_termt::factoryt< signed_dividet > signed_divide
static const smt_function_application_termt::factoryt< signed_remaindert > signed_remainder
static const smt_function_application_termt::factoryt< subtractt > subtract
static const smt_function_application_termt::factoryt< andt > make_and
static const smt_function_application_termt::factoryt< distinctt > distinct
Makes applications of the function which returns true iff its two arguments are not identical.
static const smt_function_application_termt::factoryt< if_then_elset > if_then_else
static const smt_function_application_termt::factoryt< impliest > implies
static const smt_function_application_termt::factoryt< ort > make_or
static const smt_function_application_termt::factoryt< equalt > equal
static const smt_function_application_termt::factoryt< andt > make_and
static const smt_function_application_termt::factoryt< xort > make_xor
static const smt_function_application_termt::factoryt< nott > make_not
Stores identifiers in unescaped and unquoted form.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
const sub_classt * cast() const &
void accept(smt_sort_const_downcast_visitort &) const
const smt_sortt & get_sort() const
Struct constructor from list of elements.
Expression to hold a symbol (variable)
const irep_idt & get_identifier() const
Semantic type conversion.
The type of an expression, extends irept.
The unary minus expression.
The unary plus expression.
Union constructor from single element.
Operator to update elements in structs and arrays.
Vector constructor from list of elements.
Operator to update elements in structs and arrays.
static std::function< std::function< smt_termt(smt_termt)>std::size_t)> extension_for_type(const typet &type)
void filtered_visit_post(const exprt &_expr, std::function< bool(const exprt &)> filter, std::function< void(const exprt &)> visitor)
Post order traversal where the children of a node are only visited if applying the filter function to...
exprt lower_address_of_array_index(exprt expr)
Lower the address_of(array[idx]) sub expressions in expr to idx + address_of(array),...
static smt_termt convert_bit_vector_cast(const smt_termt &from_term, const typet &from_type, const bitvector_typet &to_type)
static smt_termt most_significant_bit_is_set(const smt_termt &input)
Constructs a term which is true if the most significant bit of input is set.
static smt_termt convert_array_update_to_smt(const with_exprt &with, const sub_expression_mapt &converted)
static smt_termt make_bitvector_resize_cast(const smt_termt &from_term, const bitvector_typet &from_type, const bitvector_typet &to_type)
static std::optional< smt_termt > try_relational_conversion(const exprt &expr, const sub_expression_mapt &converted)
static smt_termt convert_multiary_operator_to_terms(const multi_ary_exprt &expr, const sub_expression_mapt &converted, const factoryt &factory)
Converts operator expressions with 2 or more operands to terms expressed as binary operator applicati...
std::unordered_map< exprt, smt_termt, irep_hash > sub_expression_mapt
Post order visitation is used in order to construct the the smt terms bottom upwards without using re...
static smt_termt make_not_zero(const smt_termt &input, const typet &source_type)
Makes a term which is true if input is not 0 / false.
static smt_termt convert_relational_to_smt(const binary_relation_exprt &binary_relation, const unsigned_factory_typet &unsigned_factory, const signed_factory_typet &signed_factory, const sub_expression_mapt &converted)
static smt_termt dispatch_expr_to_smt_conversion(const exprt &expr, const sub_expression_mapt &converted, const smt_object_mapt &object_map, const type_size_mapt &pointer_sizes, const smt_object_sizet::make_applicationt &call_object_size, const smt_is_dynamic_objectt::make_applicationt &apply_is_dynamic_object)
static smt_termt convert_to_smt_shift(const factoryt &factory, const shiftt &shift, const sub_expression_mapt &converted)
static smt_sortt convert_type_to_smt_sort(const bool_typet &type)
at_scope_exitt< functiont > at_scope_exit(functiont exit_function)
static smt_termt convert_c_bool_cast(const smt_termt &from_term, const typet &from_type, const bitvector_typet &to_type)
Returns a cast to C bool expressed in smt terms.
static bool operands_are_of_type(const exprt &expr)
Ensures that all operands of the argument expression have related types.
static smt_termt convert_expr_to_smt(const symbol_exprt &symbol_expr)
Templated functions to cast to specific exprt-derived classes.
bool is_null_pointer(const constant_exprt &expr)
Returns true if expr has a pointer type and a value NULL; it also returns true when expr has value ze...
Deprecated expression utility functions.
API to expression classes for floating-point arithmetic.
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
API to expression classes for 'mathematical' expressions.
mini_bddt exists(const mini_bddt &u, const unsigned var)
mp_integer bitwise_xor(const mp_integer &a, const mp_integer &b)
bitwise 'xor' of two nonnegative integers
exprt make_invalid_pointer_expr()
Create the invalid pointer constant.
exprt find_object_base_expression(const address_of_exprt &address_of)
The model of addresses we use consists of a unique object identifier and an offset.
std::unordered_map< exprt, decision_procedure_objectt, irep_hash > smt_object_mapt
Mapping from an object's base expression to the set of information about it which we track.
API to expression classes for Pointers.
bool can_cast_type< pointer_typet >(const typet &type)
Check whether a reference to a typet is a pointer_typet.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
exprt pointer_offset(const exprt &pointer)
exprt object_size(const exprt &pointer)
exprt pointer_object(const exprt &p)
Various predicates over pointers in programs.
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< iteratort > make_range(iteratort begin, iteratort end)
#define UNIMPLEMENTED_FEATURE(FEATURE)
#define UNREACHABLE
This should be used to mark dead code.
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
#define POSTCONDITION(CONDITION)
#define UNREACHABLE_BECAUSE(REASON)
API to expression classes.
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
bool can_cast_type< array_typet >(const typet &type)
Check whether a reference to a typet is a array_typet.
bool can_cast_type< code_typet >(const typet &type)
Check whether a reference to a typet is a code_typet.
bool can_cast_type< bitvector_typet >(const typet &type)
Check whether a reference to a typet is a bitvector_typet.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
binary_relation_exprt less_than(exprt lhs, exprt rhs)
binary_relation_exprt greater_than(exprt lhs, exprt rhs)
at_scope_exitt(functiont exit_function)
void visit(const smt_array_sortt &) override
const smt_termt & from_term
sort_based_cast_to_bit_vector_convertert(const smt_termt &from_term, const typet &from_type, const bitvector_typet &to_type)
void visit(const smt_bool_sortt &) override
const bitvector_typet & to_type
void visit(const smt_bit_vector_sortt &) override
std::optional< smt_termt > result
void visit(const smt_array_sortt &array_sort) override
void visit(const smt_bit_vector_sortt &bit_vector_sort) override
std::optional< smt_termt > result
const constant_exprt & member_input
void visit(const smt_bool_sortt &) override
sort_based_literal_convertert(const constant_exprt &input)
std::unordered_map< typet, smt_termt, irep_hash > type_size_mapt