cprover
Loading...
Searching...
No Matches
convert_expr_to_smt.cpp
Go to the documentation of this file.
1// Author: Diffblue Ltd.
2#include <util/arith_tools.h>
5#include <util/c_types.h>
6#include <util/config.h>
7#include <util/expr.h>
8#include <util/expr_cast.h>
9#include <util/floatbv_expr.h>
11#include <util/pointer_expr.h>
13#include <util/range.h>
14#include <util/std_expr.h>
16
22
23#include <algorithm>
24#include <functional>
25#include <numeric>
26#include <stack>
27
37using sub_expression_mapt = std::unordered_map<exprt, smt_termt, irep_hash>;
38
51template <typename factoryt>
53 const multi_ary_exprt &expr,
54 const sub_expression_mapt &converted,
55 const factoryt &factory)
56{
57 PRECONDITION(expr.operands().size() >= 2);
58 const auto operand_terms =
59 make_range(expr.operands()).map([&](const exprt &expr) {
60 return converted.at(expr);
61 });
62 return std::accumulate(
63 ++operand_terms.begin(),
64 operand_terms.end(),
65 *operand_terms.begin(),
66 factory);
67}
68
73template <typename target_typet>
74static bool operands_are_of_type(const exprt &expr)
75{
76 return std::all_of(
77 expr.operands().cbegin(), expr.operands().cend(), [](const exprt &operand) {
78 return can_cast_type<target_typet>(operand.type());
79 });
80}
81
83{
84 return smt_bool_sortt{};
85}
86
91
98
100{
101 if(const auto bool_type = type_try_dynamic_cast<bool_typet>(type))
102 {
103 return convert_type_to_smt_sort(*bool_type);
104 }
105 if(const auto bitvector_type = type_try_dynamic_cast<bitvector_typet>(type))
106 {
107 return convert_type_to_smt_sort(*bitvector_type);
108 }
109 if(const auto array_type = type_try_dynamic_cast<array_typet>(type))
110 {
111 return convert_type_to_smt_sort(*array_type);
112 }
113 UNIMPLEMENTED_FEATURE("Generation of SMT formula for type: " + type.pretty());
114}
115
117{
118 return smt_identifier_termt{symbol_expr.get_identifier(),
119 convert_type_to_smt_sort(symbol_expr.type())};
120}
121
123 const nondet_symbol_exprt &nondet_symbol,
124 const sub_expression_mapt &converted)
125{
126 // A nondet_symbol is a reference to an unconstrained function. This function
127 // will already have been added as a dependency.
129 nondet_symbol.get_identifier(),
130 convert_type_to_smt_sort(nondet_symbol.type())};
131}
132
134static smt_termt make_not_zero(const smt_termt &input, const typet &source_type)
135{
136 if(input.get_sort().cast<smt_bool_sortt>())
137 return input;
138 if(const auto bit_vector_sort = input.get_sort().cast<smt_bit_vector_sortt>())
139 {
141 input, smt_bit_vector_constant_termt{0, *bit_vector_sort});
142 }
144}
145
148 const smt_termt &from_term,
149 const typet &from_type,
150 const bitvector_typet &to_type)
151{
152 const std::size_t c_bool_width = to_type.get_width();
154 make_not_zero(from_term, from_type),
155 smt_bit_vector_constant_termt{1, c_bool_width},
156 smt_bit_vector_constant_termt{0, c_bool_width});
157}
158
159static std::function<std::function<smt_termt(smt_termt)>(std::size_t)>
172
174 const smt_termt &from_term,
176 const bitvector_typet &to_type)
177{
179 {
181 "Generation of SMT formula for type cast to fixed-point bitvector "
182 "type: " +
183 to_type.pretty());
184 }
186 {
188 "Generation of SMT formula for type cast to floating-point bitvector "
189 "type: " +
190 to_type.pretty());
191 }
192 const std::size_t from_width = from_type.get_width();
193 const std::size_t to_width = to_type.get_width();
194 if(to_width == from_width)
195 return from_term;
196 if(to_width < from_width)
197 return smt_bit_vector_theoryt::extract(to_width - 1, 0)(from_term);
198 const std::size_t extension_size = to_width - from_width;
199 return extension_for_type(from_type)(extension_size)(from_term);
200}
201
204{
208 std::optional<smt_termt> result;
209
217
218 void visit(const smt_bool_sortt &) override
219 {
221 from_term, from_type, c_bool_typet{to_type.get_width()});
222 }
223
224 void visit(const smt_bit_vector_sortt &) override
225 {
226 if(const auto bitvector = type_try_dynamic_cast<bitvector_typet>(from_type))
228 else
230 "Generation of SMT formula for type cast to bit vector from type: " +
231 from_type.pretty());
232 }
233
234 void visit(const smt_array_sortt &) override
235 {
237 "Generation of SMT formula for type cast to bit vector from type: " +
238 from_type.pretty());
239 }
240};
241
243 const smt_termt &from_term,
244 const typet &from_type,
245 const bitvector_typet &to_type)
246{
248 from_term, from_type, to_type};
249 from_term.get_sort().accept(converter);
250 POSTCONDITION(converter.result);
251 return *converter.result;
252}
253
255 const typecast_exprt &cast,
256 const sub_expression_mapt &converted)
257{
258 const auto &from_term = converted.at(cast.op());
259 const typet &from_type = cast.op().type();
260 const typet &to_type = cast.type();
262 return make_not_zero(from_term, cast.op().type());
263 if(const auto c_bool_type = type_try_dynamic_cast<c_bool_typet>(to_type))
264 return convert_c_bool_cast(from_term, from_type, *c_bool_type);
265 if(const auto bit_vector = type_try_dynamic_cast<bitvector_typet>(to_type))
266 return convert_bit_vector_cast(from_term, from_type, *bit_vector);
268 "Generation of SMT formula for type cast expression: " + cast.pretty());
269}
270
272 const floatbv_typecast_exprt &float_cast,
273 const sub_expression_mapt &converted)
274{
276 "Generation of SMT formula for floating point type cast expression: " +
277 float_cast.pretty());
278}
279
281 const struct_exprt &struct_construction,
282 const sub_expression_mapt &converted)
283{
285 "Generation of SMT formula for struct construction expression: " +
286 struct_construction.pretty());
287}
288
290 const union_exprt &union_construction,
291 const sub_expression_mapt &converted)
292{
294 "Generation of SMT formula for union construction expression: " +
295 union_construction.pretty());
296}
297
299{
301 std::optional<smt_termt> result;
302
304 : member_input{input}
305 {
306 }
307
308 void visit(const smt_bool_sortt &) override
309 {
311 }
312
313 void visit(const smt_bit_vector_sortt &bit_vector_sort) override
314 {
315 const auto &width = bit_vector_sort.bit_width();
316 // We get the value using a non-signed interpretation, as smt bit vector
317 // terms do not carry signedness.
318 const auto value = bvrep2integer(member_input.get_value(), width, false);
319 result = smt_bit_vector_constant_termt{value, bit_vector_sort};
320 }
321
322 void visit(const smt_array_sortt &array_sort) override
323 {
325 "Conversion of array SMT literal " + array_sort.pretty());
326 }
327};
328
329static smt_termt convert_expr_to_smt(const constant_exprt &constant_literal)
330{
331 if(constant_literal.is_null_pointer())
332 {
333 const size_t bit_width =
334 type_checked_cast<pointer_typet>(constant_literal.type()).get_width();
335 // An address of 0 encodes an object identifier of 0 for the NULL object
336 // and an offset of 0 into the object.
337 const auto address = 0;
338 return smt_bit_vector_constant_termt{address, bit_width};
339 }
340 if(constant_literal.type() == integer_typet{})
341 {
342 // This is converting integer constants into bit vectors for use with
343 // bit vector based smt logics. As bit vector widths are not specified for
344 // non bit vector types, this chooses a width based on the minimum needed
345 // to hold the integer constant value.
346 const auto value = numeric_cast_v<mp_integer>(constant_literal);
347 return smt_bit_vector_constant_termt{value, address_bits(value + 1)};
348 }
349 const auto sort = convert_type_to_smt_sort(constant_literal.type());
350 sort_based_literal_convertert converter(constant_literal);
351 sort.accept(converter);
352 return *converter.result;
353}
354
356 const concatenation_exprt &concatenation,
357 const sub_expression_mapt &converted)
358{
360 {
362 concatenation, converted, smt_bit_vector_theoryt::concat);
363 }
365 "Generation of SMT formula for concatenation expression: " +
366 concatenation.pretty());
367}
368
370 const bitand_exprt &bitwise_and_expr,
371 const sub_expression_mapt &converted)
372{
373 if(operands_are_of_type<bitvector_typet>(bitwise_and_expr))
374 {
376 bitwise_and_expr, converted, smt_bit_vector_theoryt::make_and);
377 }
378 else
379 {
381 "Generation of SMT formula for bitwise and expression: " +
382 bitwise_and_expr.pretty());
383 }
384}
385
387 const bitor_exprt &bitwise_or_expr,
388 const sub_expression_mapt &converted)
389{
390 if(operands_are_of_type<bitvector_typet>(bitwise_or_expr))
391 {
393 bitwise_or_expr, converted, smt_bit_vector_theoryt::make_or);
394 }
395 else
396 {
398 "Generation of SMT formula for bitwise or expression: " +
399 bitwise_or_expr.pretty());
400 }
401}
402
405 const sub_expression_mapt &converted)
406{
408 {
411 }
412 else
413 {
415 "Generation of SMT formula for bitwise xor expression: " +
416 bitwise_xor.pretty());
417 }
418}
419
421 const bitnot_exprt &bitwise_not,
422 const sub_expression_mapt &converted)
423{
424 if(can_cast_type<bitvector_typet>(bitwise_not.op().type()))
425 {
426 return smt_bit_vector_theoryt::make_not(converted.at(bitwise_not.op()));
427 }
428 else
429 {
431 "Generation of SMT formula for bitnot_exprt: " + bitwise_not.pretty());
432 }
433}
434
436 const unary_minus_exprt &unary_minus,
437 const sub_expression_mapt &converted)
438{
440 {
441 return smt_bit_vector_theoryt::negate(converted.at(unary_minus.op()));
442 }
443 else
444 {
446 "Generation of SMT formula for unary minus expression: " +
447 unary_minus.pretty());
448 }
449}
450
452 const unary_plus_exprt &unary_plus,
453 const sub_expression_mapt &converted)
454{
456 "Generation of SMT formula for unary plus expression: " +
457 unary_plus.pretty());
458}
459
461 const sign_exprt &is_negative,
462 const sub_expression_mapt &converted)
463{
465 "Generation of SMT formula for \"is negative\" expression: " +
466 is_negative.pretty());
467}
468
470 const if_exprt &if_expression,
471 const sub_expression_mapt &converted)
472{
474 converted.at(if_expression.cond()),
475 converted.at(if_expression.true_case()),
476 converted.at(if_expression.false_case()));
477}
478
480 const and_exprt &and_expression,
481 const sub_expression_mapt &converted)
482{
484 and_expression, converted, smt_core_theoryt::make_and);
485}
486
488 const or_exprt &or_expression,
489 const sub_expression_mapt &converted)
490{
492 or_expression, converted, smt_core_theoryt::make_or);
493}
494
496 const xor_exprt &xor_expression,
497 const sub_expression_mapt &converted)
498{
500 xor_expression, converted, smt_core_theoryt::make_xor);
501}
502
504 const implies_exprt &implies,
505 const sub_expression_mapt &converted)
506{
508 converted.at(implies.op0()), converted.at(implies.op1()));
509}
510
512 const not_exprt &logical_not,
513 const sub_expression_mapt &converted)
514{
515 return smt_core_theoryt::make_not(converted.at(logical_not.op()));
516}
517
519 const equal_exprt &equal,
520 const sub_expression_mapt &converted)
521{
523 converted.at(equal.op0()), converted.at(equal.op1()));
524}
525
527 const notequal_exprt &not_equal,
528 const sub_expression_mapt &converted)
529{
531 converted.at(not_equal.op0()), converted.at(not_equal.op1()));
532}
533
535 const ieee_float_equal_exprt &float_equal,
536 const sub_expression_mapt &converted)
537{
539 "Generation of SMT formula for floating point equality expression: " +
540 float_equal.pretty());
541}
542
544 const ieee_float_notequal_exprt &float_not_equal,
545 const sub_expression_mapt &converted)
546{
548 "Generation of SMT formula for floating point not equal expression: " +
549 float_not_equal.pretty());
550}
551
552template <typename unsigned_factory_typet, typename signed_factory_typet>
554 const binary_relation_exprt &binary_relation,
555 const unsigned_factory_typet &unsigned_factory,
556 const signed_factory_typet &signed_factory,
557 const sub_expression_mapt &converted)
558{
559 PRECONDITION(binary_relation.lhs().type() == binary_relation.rhs().type());
560 const auto &lhs = converted.at(binary_relation.lhs());
561 const auto &rhs = converted.at(binary_relation.rhs());
562 const typet operand_type = binary_relation.lhs().type();
563 if(can_cast_type<pointer_typet>(operand_type))
564 {
565 // The code here is operating under the assumption that the comparison
566 // operands have types for which the comparison makes sense.
567
568 // We already know this is the case given that we have followed
569 // the if statement branch, but including the same check here
570 // for consistency (it's cheap).
571 const auto lhs_type_is_pointer =
572 can_cast_type<pointer_typet>(binary_relation.lhs().type());
573 const auto rhs_type_is_pointer =
574 can_cast_type<pointer_typet>(binary_relation.rhs().type());
575 INVARIANT(
576 lhs_type_is_pointer && rhs_type_is_pointer,
577 "pointer comparison requires that both operand types are pointers.");
578 return unsigned_factory(lhs, rhs);
579 }
580 else if(lhs.get_sort().cast<smt_bit_vector_sortt>())
581 {
582 if(can_cast_type<unsignedbv_typet>(operand_type))
583 return unsigned_factory(lhs, rhs);
584 if(can_cast_type<signedbv_typet>(operand_type))
585 return signed_factory(lhs, rhs);
586 }
587
589 "Generation of SMT formula for relational expression: " +
590 binary_relation.pretty());
591}
592
593static std::optional<smt_termt> try_relational_conversion(
594 const exprt &expr,
595 const sub_expression_mapt &converted)
596{
598 {
603 converted);
604 }
605 if(
606 const auto greater_than_or_equal =
608 {
610 *greater_than_or_equal,
613 converted);
614 }
616 {
618 *less_than,
621 converted);
622 }
623 if(
624 const auto less_than_or_equal =
626 {
628 *less_than_or_equal,
631 converted);
632 }
633 return {};
634}
635
637 const plus_exprt &plus,
638 const sub_expression_mapt &converted,
639 const type_size_mapt &pointer_sizes)
640{
641 if(std::all_of(
642 plus.operands().cbegin(), plus.operands().cend(), [](exprt operand) {
643 return can_cast_type<integer_bitvector_typet>(operand.type());
644 }))
645 {
647 plus, converted, smt_bit_vector_theoryt::add);
648 }
649 else if(can_cast_type<pointer_typet>(plus.type()))
650 {
651 INVARIANT(
652 plus.operands().size() == 2,
653 "We are only handling a binary version of plus when it has a pointer "
654 "operand");
655
656 exprt pointer;
657 exprt scalar;
658 for(auto &operand : plus.operands())
659 {
661 {
662 pointer = operand;
663 }
664 else
665 {
666 scalar = operand;
667 }
668 }
669
670 // We need to ensure that we follow this code path only if the expression
671 // our assumptions about the structure of the addition expression hold.
672 INVARIANT(
674 "An addition expression with both operands being pointers when they are "
675 "not dereferenced is malformed");
676
679 const auto base_type = pointer_type.base_type();
680 const auto pointer_size = pointer_sizes.at(base_type);
681
683 converted.at(pointer),
684 smt_bit_vector_theoryt::multiply(converted.at(scalar), pointer_size));
685 }
686 else
687 {
689 "Generation of SMT formula for plus expression: " + plus.pretty());
690 }
691}
692
694 const minus_exprt &minus,
695 const sub_expression_mapt &converted,
696 const type_size_mapt &pointer_sizes)
697{
698 const bool both_operands_bitvector =
701
702 const bool lhs_is_pointer = can_cast_type<pointer_typet>(minus.lhs().type());
703 const bool rhs_is_pointer = can_cast_type<pointer_typet>(minus.rhs().type());
704
705 const bool both_operands_pointers = lhs_is_pointer && rhs_is_pointer;
706
707 // We don't really handle this - we just compute this to fall
708 // into an if-else branch that gives proper error handling information.
709 const bool one_operand_pointer = lhs_is_pointer || rhs_is_pointer;
710
711 if(both_operands_bitvector)
712 {
714 converted.at(minus.lhs()), converted.at(minus.rhs()));
715 }
716 else if(both_operands_pointers)
717 {
718 const auto lhs_base_type = to_pointer_type(minus.lhs().type()).base_type();
719 const auto rhs_base_type = to_pointer_type(minus.rhs().type()).base_type();
720 INVARIANT(
721 lhs_base_type == rhs_base_type,
722 "only pointers of the same object type can be subtracted.");
725 converted.at(minus.lhs()), converted.at(minus.rhs())),
726 pointer_sizes.at(lhs_base_type));
727 }
728 else if(one_operand_pointer)
729 {
730 // It's semantically void to have an expression `3 - a` where `a`
731 // is a pointer.
732 INVARIANT(
733 lhs_is_pointer,
734 "minus expressions of pointer and integer expect lhs to be the pointer");
735 const auto lhs_base_type = to_pointer_type(minus.lhs().type()).base_type();
736
738 converted.at(minus.lhs()),
740 converted.at(minus.rhs()), pointer_sizes.at(lhs_base_type)));
741 }
742 else
743 {
745 "Generation of SMT formula for minus expression: " + minus.pretty());
746 }
747}
748
750 const div_exprt &divide,
751 const sub_expression_mapt &converted)
752{
753 const smt_termt &lhs = converted.at(divide.lhs());
754 const smt_termt &rhs = converted.at(divide.rhs());
755
756 const bool both_operands_bitvector =
759
760 const bool both_operands_unsigned =
763
764 if(both_operands_bitvector)
765 {
766 if(both_operands_unsigned)
767 {
769 }
770 else
771 {
773 }
774 }
775 else
776 {
778 "Generation of SMT formula for divide expression: " + divide.pretty());
779 }
780}
781
783 const ieee_float_op_exprt &float_operation,
784 const sub_expression_mapt &converted)
785{
786 // This case includes the floating point plus, minus, division and
787 // multiplication operations.
789 "Generation of SMT formula for floating point operation expression: " +
790 float_operation.pretty());
791}
792
794 const mod_exprt &truncation_modulo,
795 const sub_expression_mapt &converted)
796{
797 const smt_termt &lhs = converted.at(truncation_modulo.lhs());
798 const smt_termt &rhs = converted.at(truncation_modulo.rhs());
799
800 const bool both_operands_bitvector =
801 can_cast_type<integer_bitvector_typet>(truncation_modulo.lhs().type()) &&
802 can_cast_type<integer_bitvector_typet>(truncation_modulo.rhs().type());
803
804 const bool both_operands_unsigned =
805 can_cast_type<unsignedbv_typet>(truncation_modulo.lhs().type()) &&
806 can_cast_type<unsignedbv_typet>(truncation_modulo.rhs().type());
807
808 if(both_operands_bitvector)
809 {
810 if(both_operands_unsigned)
811 {
813 }
814 else
815 {
817 }
818 }
819 else
820 {
822 "Generation of SMT formula for remainder (modulus) expression: " +
823 truncation_modulo.pretty());
824 }
825}
826
828 const euclidean_mod_exprt &euclidean_modulo,
829 const sub_expression_mapt &converted)
830{
832 "Generation of SMT formula for euclidean modulo expression: " +
833 euclidean_modulo.pretty());
834}
835
837 const mult_exprt &multiply,
838 const sub_expression_mapt &converted)
839{
840 if(std::all_of(
841 multiply.operands().cbegin(),
842 multiply.operands().cend(),
843 [](exprt operand) {
844 return can_cast_type<integer_bitvector_typet>(operand.type());
845 }))
846 {
848 multiply, converted, smt_bit_vector_theoryt::multiply);
849 }
850 else
851 {
853 "Generation of SMT formula for multiply expression: " +
854 multiply.pretty());
855 }
856}
857
866 const address_of_exprt &address_of,
867 const sub_expression_mapt &converted,
868 const smt_object_mapt &object_map)
869{
870 const auto type = type_try_dynamic_cast<pointer_typet>(address_of.type());
871 INVARIANT(
872 type, "Result of the address_of operator should have pointer type.");
873 const auto base = find_object_base_expression(address_of);
874 const auto object = object_map.find(base);
875 INVARIANT(
876 object != object_map.end(),
877 "Objects should be tracked before converting their address to SMT terms");
878 const std::size_t object_id = object->second.unique_id;
879 const std::size_t object_bits = config.bv_encoding.object_bits;
880 const std::size_t max_objects = std::size_t(1) << object_bits;
881 if(object_id >= max_objects)
882 {
884 "too many addressed objects: maximum number of objects is set to 2^n=" +
885 std::to_string(max_objects) + " (with n=" + std::to_string(object_bits) +
886 "); " +
887 "use the `--object-bits n` option to increase the maximum number"};
888 }
889 const smt_termt object_bit_vector =
890 smt_bit_vector_constant_termt{object_id, object_bits};
891 INVARIANT(
892 type->get_width() > object_bits,
893 "Pointer should be wider than object_bits in order to allow for offset "
894 "encoding.");
895 const size_t offset_bits = type->get_width() - object_bits;
897 {
898 const smt_bit_vector_constant_termt offset{0, offset_bits};
899 return smt_bit_vector_theoryt::concat(object_bit_vector, offset);
900 }
902 "Generation of SMT formula for address of expression: " +
903 address_of.pretty());
904}
905
907 const array_of_exprt &array_of,
908 const sub_expression_mapt &converted)
909{
910 // This function is unreachable as the `array_of_exprt` nodes are already
911 // fully converted by the incremental decision procedure functions
912 // (smt2_incremental_decision_proceduret::define_array_function).
914}
915
917 const array_comprehension_exprt &array_comprehension,
918 const sub_expression_mapt &converted)
919{
921 "Generation of SMT formula for array comprehension expression: " +
922 array_comprehension.pretty());
923}
924
926 const index_exprt &index_of,
927 const sub_expression_mapt &converted)
928{
929 const smt_termt &array = converted.at(index_of.array());
930 const smt_termt &index = converted.at(index_of.index());
931 return smt_array_theoryt::select(array, index);
932}
933
934template <typename factoryt, typename shiftt>
936 const factoryt &factory,
937 const shiftt &shift,
938 const sub_expression_mapt &converted)
939{
940 const smt_termt &first_operand = converted.at(shift.op0());
941 const smt_termt &second_operand = converted.at(shift.op1());
942 const auto first_bit_vector_sort =
943 first_operand.get_sort().cast<smt_bit_vector_sortt>();
944 const auto second_bit_vector_sort =
945 second_operand.get_sort().cast<smt_bit_vector_sortt>();
946 INVARIANT(
947 first_bit_vector_sort && second_bit_vector_sort,
948 "Shift expressions are expected to have bit vector operands.");
949 INVARIANT(
950 shift.type() == shift.op0().type(),
951 "Shift expression type must be equals to first operand type.");
952 const std::size_t first_width = first_bit_vector_sort->bit_width();
953 const std::size_t second_width = second_bit_vector_sort->bit_width();
954 if(first_width > second_width)
955 {
956 return factory(
957 first_operand,
958 extension_for_type(shift.op1().type())(first_width - second_width)(
959 second_operand));
960 }
961 else if(first_width < second_width)
962 {
963 const auto result = factory(
964 extension_for_type(shift.op0().type())(second_width - first_width)(
965 first_operand),
966 second_operand);
967 return smt_bit_vector_theoryt::extract(first_width - 1, 0)(result);
968 }
969 else
970 {
971 return factory(first_operand, second_operand);
972 }
973}
974
976 const shift_exprt &shift,
977 const sub_expression_mapt &converted)
978{
979 // TODO: Dispatch for rotation expressions. A `shift_exprt` can be a rotation.
980 if(const auto left_shift = expr_try_dynamic_cast<shl_exprt>(shift))
981 {
983 smt_bit_vector_theoryt::shift_left, *left_shift, converted);
984 }
985 if(const auto right_logical_shift = expr_try_dynamic_cast<lshr_exprt>(shift))
986 {
989 *right_logical_shift,
990 converted);
991 }
992 if(const auto right_arith_shift = expr_try_dynamic_cast<ashr_exprt>(shift))
993 {
996 *right_arith_shift,
997 converted);
998 }
1000 "Generation of SMT formula for shift expression: " + shift.pretty());
1001}
1002
1004 const with_exprt &with,
1005 const sub_expression_mapt &converted)
1006{
1007 smt_termt array = converted.at(with.old());
1008 const smt_termt &index_term = converted.at(with.where());
1009 const smt_termt &value_term = converted.at(with.new_value());
1010 array = smt_array_theoryt::store(array, index_term, value_term);
1011 return array;
1012}
1013
1015 const with_exprt &with,
1016 const sub_expression_mapt &converted)
1017{
1019 return convert_array_update_to_smt(with, converted);
1020 // 'with' expression is also used to update struct fields, but for now we do
1021 // not support them, so we fail.
1023 "Generation of SMT formula for with expression: " + with.pretty());
1024}
1025
1027 const update_exprt &update,
1028 const sub_expression_mapt &converted)
1029{
1031 "Generation of SMT formula for update expression: " + update.pretty());
1032}
1033
1035 const member_exprt &member_extraction,
1036 const sub_expression_mapt &converted)
1037{
1039 "Generation of SMT formula for member extraction expression: " +
1040 member_extraction.pretty());
1041}
1042
1044 const is_dynamic_object_exprt &is_dynamic_object,
1045 const sub_expression_mapt &converted,
1046 const smt_is_dynamic_objectt::make_applicationt &apply_is_dynamic_object)
1047{
1048 const smt_termt &pointer = converted.at(is_dynamic_object.address());
1049 const auto pointer_sort = pointer.get_sort().cast<smt_bit_vector_sortt>();
1050 INVARIANT(
1051 pointer_sort, "Pointers should be encoded as bit vector sorted terms.");
1052 const std::size_t pointer_width = pointer_sort->bit_width();
1053 return apply_is_dynamic_object(
1054 std::vector<smt_termt>{smt_bit_vector_theoryt::extract(
1055 pointer_width - 1,
1056 pointer_width - config.bv_encoding.object_bits)(pointer)});
1057}
1058
1060 const is_invalid_pointer_exprt &is_invalid_pointer,
1061 const smt_object_mapt &object_map,
1062 const sub_expression_mapt &converted)
1063{
1064 const exprt &pointer_expr(to_unary_expr(is_invalid_pointer).op());
1067 INVARIANT(pointer_type, "Pointer object should have a bitvector-based type.");
1068 const std::size_t object_bits = config.bv_encoding.object_bits;
1069 const std::size_t width = pointer_type->get_width();
1070 INVARIANT(
1071 width >= object_bits,
1072 "Width should be at least as big as the number of object bits.");
1073
1074 const auto extract_op = smt_bit_vector_theoryt::extract(
1075 width - 1, width - object_bits)(converted.at(pointer_expr));
1076
1077 const auto &invalid_pointer = object_map.at(make_invalid_pointer_expr());
1078
1079 const smt_termt invalid_pointer_address = smt_bit_vector_constant_termt(
1080 invalid_pointer.unique_id, config.bv_encoding.object_bits);
1081
1082 return smt_core_theoryt::equal(invalid_pointer_address, extract_op);
1083}
1084
1086 const string_constantt &string_constant,
1087 const sub_expression_mapt &converted)
1088{
1090 "Generation of SMT formula for string constant expression: " +
1091 string_constant.pretty());
1092}
1093
1095 const extractbit_exprt &extract_bit,
1096 const sub_expression_mapt &converted)
1097{
1099 "Generation of SMT formula for extract bit expression: " +
1100 extract_bit.pretty());
1101}
1102
1104 const extractbits_exprt &extract_bits,
1105 const sub_expression_mapt &converted)
1106{
1107 const smt_termt &from = converted.at(extract_bits.src());
1108 const auto bit_vector_sort =
1110 INVARIANT(
1111 bit_vector_sort, "Extract can only be applied to bit vector terms.");
1112 const auto index_value = numeric_cast<std::size_t>(extract_bits.index());
1113 if(index_value)
1115 *index_value + bit_vector_sort->bit_width() - 1, *index_value)(from);
1117 "Generation of SMT formula for extract bits expression: " +
1118 extract_bits.pretty());
1119}
1120
1122 const replication_exprt &replication,
1123 const sub_expression_mapt &converted)
1124{
1126 "Generation of SMT formula for bit vector replication expression: " +
1127 replication.pretty());
1128}
1129
1131 const byte_extract_exprt &byte_extraction,
1132 const sub_expression_mapt &converted)
1133{
1135 "Generation of SMT formula for byte extract expression: " +
1136 byte_extraction.pretty());
1137}
1138
1140 const byte_update_exprt &byte_update,
1141 const sub_expression_mapt &converted)
1142{
1144 "Generation of SMT formula for byte update expression: " +
1145 byte_update.pretty());
1146}
1147
1149 const abs_exprt &absolute_value_of,
1150 const sub_expression_mapt &converted)
1151{
1153 "Generation of SMT formula for absolute value of expression: " +
1154 absolute_value_of.pretty());
1155}
1156
1158 const isnan_exprt &is_nan_expr,
1159 const sub_expression_mapt &converted)
1160{
1162 "Generation of SMT formula for is not a number expression: " +
1163 is_nan_expr.pretty());
1164}
1165
1167 const isfinite_exprt &is_finite_expr,
1168 const sub_expression_mapt &converted)
1169{
1171 "Generation of SMT formula for is finite expression: " +
1172 is_finite_expr.pretty());
1173}
1174
1176 const isinf_exprt &is_infinite_expr,
1177 const sub_expression_mapt &converted)
1178{
1180 "Generation of SMT formula for is infinite expression: " +
1181 is_infinite_expr.pretty());
1182}
1183
1185 const isnormal_exprt &is_normal_expr,
1186 const sub_expression_mapt &converted)
1187{
1189 "Generation of SMT formula for is infinite expression: " +
1190 is_normal_expr.pretty());
1191}
1192
1197{
1198 const auto bit_vector_sort = input.get_sort().cast<smt_bit_vector_sortt>();
1199 INVARIANT(
1200 bit_vector_sort,
1201 "Most significant bit can only be extracted from bit vector terms.");
1202 const size_t most_significant_bit_index = bit_vector_sort->bit_width() - 1;
1203 const auto extract_most_significant_bit = smt_bit_vector_theoryt::extract(
1204 most_significant_bit_index, most_significant_bit_index);
1206 extract_most_significant_bit(input), smt_bit_vector_constant_termt{1, 1});
1207}
1208
1210 const plus_overflow_exprt &plus_overflow,
1211 const sub_expression_mapt &converted)
1212{
1213 const smt_termt &left = converted.at(plus_overflow.lhs());
1214 const smt_termt &right = converted.at(plus_overflow.rhs());
1216 {
1217 const auto add_carry_bit = smt_bit_vector_theoryt::zero_extend(1);
1219 smt_bit_vector_theoryt::add(add_carry_bit(left), add_carry_bit(right)));
1220 }
1221 if(operands_are_of_type<signedbv_typet>(plus_overflow))
1222 {
1223 // Overflow has occurred if the operands have the same sign and adding them
1224 // gives a result of the opposite sign.
1225 const smt_termt msb_left = most_significant_bit_is_set(left);
1226 const smt_termt msb_right = most_significant_bit_is_set(right);
1228 smt_core_theoryt::equal(msb_left, msb_right),
1230 msb_left,
1232 }
1234 "Generation of SMT formula for plus overflow expression: " +
1235 plus_overflow.pretty());
1236}
1237
1239 const minus_overflow_exprt &minus_overflow,
1240 const sub_expression_mapt &converted)
1241{
1242 const smt_termt &left = converted.at(minus_overflow.lhs());
1243 const smt_termt &right = converted.at(minus_overflow.rhs());
1244 if(operands_are_of_type<unsignedbv_typet>(minus_overflow))
1245 {
1247 }
1248 if(operands_are_of_type<signedbv_typet>(minus_overflow))
1249 {
1250 // Overflow has occurred if the operands have the opposing signs and
1251 // subtracting them gives a result having the same signedness as the
1252 // right-hand operand. For example the following would be overflow for cases
1253 // for 8 bit wide bit vectors -
1254 // -128 - 1 == 127
1255 // 127 - (-1) == -128
1256 const smt_termt msb_left = most_significant_bit_is_set(left);
1257 const smt_termt msb_right = most_significant_bit_is_set(right);
1259 smt_core_theoryt::distinct(msb_left, msb_right),
1261 msb_right,
1263 smt_bit_vector_theoryt::subtract(left, right))));
1264 }
1266 "Generation of SMT formula for minus overflow expression: " +
1267 minus_overflow.pretty());
1268}
1269
1271 const mult_overflow_exprt &mult_overflow,
1272 const sub_expression_mapt &converted)
1273{
1274 PRECONDITION(mult_overflow.lhs().type() == mult_overflow.rhs().type());
1275 const auto &operand_type = mult_overflow.lhs().type();
1276 const smt_termt &left = converted.at(mult_overflow.lhs());
1277 const smt_termt &right = converted.at(mult_overflow.rhs());
1278 if(
1279 const auto unsigned_type =
1281 {
1282 const std::size_t width = unsigned_type->get_width();
1283 const auto extend = smt_bit_vector_theoryt::zero_extend(width);
1285 smt_bit_vector_theoryt::multiply(extend(left), extend(right)),
1286 smt_bit_vector_constant_termt{power(2, width), width * 2});
1287 }
1288 if(
1289 const auto signed_type =
1291 {
1292 const smt_termt msb_left = most_significant_bit_is_set(left);
1293 const smt_termt msb_right = most_significant_bit_is_set(right);
1294 const std::size_t width = signed_type->get_width();
1295 const auto extend = smt_bit_vector_theoryt::sign_extend(width);
1296 const auto multiplication =
1297 smt_bit_vector_theoryt::multiply(extend(left), extend(right));
1299 multiplication,
1300 smt_bit_vector_constant_termt{power(2, width - 1), width * 2});
1301 const auto too_small = smt_bit_vector_theoryt::signed_less_than(
1302 multiplication,
1304 smt_bit_vector_constant_termt{power(2, width - 1), width * 2}));
1306 smt_core_theoryt::equal(msb_left, msb_right), too_large, too_small);
1307 }
1309 "Generation of SMT formula for multiply overflow expression: " +
1310 mult_overflow.pretty());
1311}
1312
1315 const sub_expression_mapt &converted)
1316{
1317 const auto type =
1319 INVARIANT(type, "Pointer object should have a bitvector-based type.");
1320 const auto converted_expr = converted.at(pointer_object.pointer());
1321 const std::size_t width = type->get_width();
1322 const std::size_t object_bits = config.bv_encoding.object_bits;
1323 INVARIANT(
1324 width >= object_bits,
1325 "Width should be at least as big as the number of object bits.");
1326 const std::size_t ext = width - object_bits;
1327 const auto extract_op = smt_bit_vector_theoryt::extract(
1328 width - 1, width - object_bits)(converted_expr);
1329 if(ext > 0)
1330 {
1331 return smt_bit_vector_theoryt::zero_extend(ext)(extract_op);
1332 }
1333 return extract_op;
1334}
1335
1338 const sub_expression_mapt &converted)
1339{
1340 const auto type =
1342 INVARIANT(type, "Pointer offset should have a bitvector-based type.");
1343 const auto converted_expr = converted.at(pointer_offset.pointer());
1344 const std::size_t width = type->get_width();
1345 std::size_t offset_bits = width - config.bv_encoding.object_bits;
1346 if(offset_bits > width)
1347 offset_bits = width;
1348 const auto extract_op =
1349 smt_bit_vector_theoryt::extract(offset_bits - 1, 0)(converted_expr);
1350 if(width > offset_bits)
1351 {
1352 return smt_bit_vector_theoryt::sign_extend(width - offset_bits)(extract_op);
1353 }
1354 return extract_op;
1355}
1356
1358 const shl_overflow_exprt &shl_overflow,
1359 const sub_expression_mapt &converted)
1360{
1362 "Generation of SMT formula for shift left overflow expression: " +
1363 shl_overflow.pretty());
1364}
1365
1367 const array_exprt &array_construction,
1368 const sub_expression_mapt &converted)
1369{
1370 // This function is unreachable as the `array_exprt` nodes are already fully
1371 // converted by the incremental decision procedure functions
1372 // (smt2_incremental_decision_proceduret::define_array_function).
1374}
1375
1377 const literal_exprt &literal,
1378 const sub_expression_mapt &converted)
1379{
1381 "Generation of SMT formula for literal expression: " + literal.pretty());
1382}
1383
1385 const forall_exprt &for_all,
1386 const sub_expression_mapt &converted)
1387{
1389 "Generation of SMT formula for for all expression: " + for_all.pretty());
1390}
1391
1393 const exists_exprt &exists,
1394 const sub_expression_mapt &converted)
1395{
1397 "Generation of SMT formula for exists expression: " + exists.pretty());
1398}
1399
1401 const vector_exprt &vector,
1402 const sub_expression_mapt &converted)
1403{
1405 "Generation of SMT formula for vector expression: " + vector.pretty());
1406}
1407
1410 const sub_expression_mapt &converted,
1411 const smt_object_sizet::make_applicationt &call_object_size)
1412{
1413 const smt_termt &pointer = converted.at(object_size.pointer());
1414 const auto pointer_sort = pointer.get_sort().cast<smt_bit_vector_sortt>();
1415 INVARIANT(
1416 pointer_sort, "Pointers should be encoded as bit vector sorted terms.");
1417 const std::size_t pointer_width = pointer_sort->bit_width();
1418 return call_object_size(
1419 std::vector<smt_termt>{smt_bit_vector_theoryt::extract(
1420 pointer_width - 1,
1421 pointer_width - config.bv_encoding.object_bits)(pointer)});
1422}
1423
1424static smt_termt
1426{
1428 "Generation of SMT formula for let expression: " + let.pretty());
1429}
1430
1432 const bswap_exprt &byte_swap,
1433 const sub_expression_mapt &converted)
1434{
1436 "Generation of SMT formula for byte swap expression: " +
1437 byte_swap.pretty());
1438}
1439
1441 const popcount_exprt &population_count,
1442 const sub_expression_mapt &converted)
1443{
1445 "Generation of SMT formula for population count expression: " +
1446 population_count.pretty());
1447}
1448
1450 const count_leading_zeros_exprt &count_leading_zeros,
1451 const sub_expression_mapt &converted)
1452{
1454 "Generation of SMT formula for count leading zeros expression: " +
1455 count_leading_zeros.pretty());
1456}
1457
1459 const count_trailing_zeros_exprt &count_trailing_zeros,
1460 const sub_expression_mapt &converted)
1461{
1463 "Generation of SMT formula for count trailing zeros expression: " +
1464 count_trailing_zeros.pretty());
1465}
1466
1468 const zero_extend_exprt &zero_extend,
1469 const sub_expression_mapt &converted)
1470{
1472 "zero_extend expression should have been lowered by the decision "
1473 "procedure before conversion to smt terms");
1474}
1475
1477 const prophecy_r_or_w_ok_exprt &prophecy_r_or_w_ok,
1478 const sub_expression_mapt &converted)
1479{
1481 "prophecy_r_or_w_ok expression should have been lowered by the decision "
1482 "procedure before conversion to smt terms");
1483}
1484
1486 const prophecy_pointer_in_range_exprt &prophecy_pointer_in_range,
1487 const sub_expression_mapt &converted)
1488{
1490 "prophecy_pointer_in_range expression should have been lowered by the "
1491 "decision procedure before conversion to smt terms");
1492}
1493
1495 const exprt &expr,
1496 const sub_expression_mapt &converted,
1497 const smt_object_mapt &object_map,
1498 const type_size_mapt &pointer_sizes,
1499 const smt_object_sizet::make_applicationt &call_object_size,
1500 const smt_is_dynamic_objectt::make_applicationt &apply_is_dynamic_object)
1501{
1502 if(const auto symbol = expr_try_dynamic_cast<symbol_exprt>(expr))
1503 {
1504 return convert_expr_to_smt(*symbol);
1505 }
1506 if(const auto nondet = expr_try_dynamic_cast<nondet_symbol_exprt>(expr))
1507 {
1508 return convert_expr_to_smt(*nondet, converted);
1509 }
1510 if(const auto cast = expr_try_dynamic_cast<typecast_exprt>(expr))
1511 {
1512 return convert_expr_to_smt(*cast, converted);
1513 }
1514 if(
1515 const auto float_cast = expr_try_dynamic_cast<floatbv_typecast_exprt>(expr))
1516 {
1517 return convert_expr_to_smt(*float_cast, converted);
1518 }
1519 if(const auto struct_construction = expr_try_dynamic_cast<struct_exprt>(expr))
1520 {
1521 return convert_expr_to_smt(*struct_construction, converted);
1522 }
1523 if(const auto union_construction = expr_try_dynamic_cast<union_exprt>(expr))
1524 {
1525 return convert_expr_to_smt(*union_construction, converted);
1526 }
1527 if(const auto constant_literal = expr_try_dynamic_cast<constant_exprt>(expr))
1528 {
1529 return convert_expr_to_smt(*constant_literal);
1530 }
1531 if(
1532 const auto concatenation = expr_try_dynamic_cast<concatenation_exprt>(expr))
1533 {
1534 return convert_expr_to_smt(*concatenation, converted);
1535 }
1536 if(const auto bitwise_and_expr = expr_try_dynamic_cast<bitand_exprt>(expr))
1537 {
1538 return convert_expr_to_smt(*bitwise_and_expr, converted);
1539 }
1540 if(const auto bitwise_or_expr = expr_try_dynamic_cast<bitor_exprt>(expr))
1541 {
1542 return convert_expr_to_smt(*bitwise_or_expr, converted);
1543 }
1545 {
1546 return convert_expr_to_smt(*bitwise_xor, converted);
1547 }
1548 if(const auto bitwise_not = expr_try_dynamic_cast<bitnot_exprt>(expr))
1549 {
1550 return convert_expr_to_smt(*bitwise_not, converted);
1551 }
1552 if(const auto unary_minus = expr_try_dynamic_cast<unary_minus_exprt>(expr))
1553 {
1554 return convert_expr_to_smt(*unary_minus, converted);
1555 }
1556 if(const auto unary_plus = expr_try_dynamic_cast<unary_plus_exprt>(expr))
1557 {
1558 return convert_expr_to_smt(*unary_plus, converted);
1559 }
1560 if(const auto is_negative = expr_try_dynamic_cast<sign_exprt>(expr))
1561 {
1562 return convert_expr_to_smt(*is_negative, converted);
1563 }
1564 if(const auto if_expression = expr_try_dynamic_cast<if_exprt>(expr))
1565 {
1566 return convert_expr_to_smt(*if_expression, converted);
1567 }
1568 if(const auto and_expression = expr_try_dynamic_cast<and_exprt>(expr))
1569 {
1570 return convert_expr_to_smt(*and_expression, converted);
1571 }
1572 if(const auto or_expression = expr_try_dynamic_cast<or_exprt>(expr))
1573 {
1574 return convert_expr_to_smt(*or_expression, converted);
1575 }
1576 if(const auto xor_expression = expr_try_dynamic_cast<xor_exprt>(expr))
1577 {
1578 return convert_expr_to_smt(*xor_expression, converted);
1579 }
1580 if(const auto implies = expr_try_dynamic_cast<implies_exprt>(expr))
1581 {
1582 return convert_expr_to_smt(*implies, converted);
1583 }
1584 if(const auto logical_not = expr_try_dynamic_cast<not_exprt>(expr))
1585 {
1586 return convert_expr_to_smt(*logical_not, converted);
1587 }
1588 if(const auto equal = expr_try_dynamic_cast<equal_exprt>(expr))
1589 {
1590 return convert_expr_to_smt(*equal, converted);
1591 }
1592 if(const auto not_equal = expr_try_dynamic_cast<notequal_exprt>(expr))
1593 {
1594 return convert_expr_to_smt(*not_equal, converted);
1595 }
1596 if(
1597 const auto float_equal =
1599 {
1600 return convert_expr_to_smt(*float_equal, converted);
1601 }
1602 if(
1603 const auto float_not_equal =
1605 {
1606 return convert_expr_to_smt(*float_not_equal, converted);
1607 }
1608 if(
1609 const auto converted_relational =
1610 try_relational_conversion(expr, converted))
1611 {
1612 return *converted_relational;
1613 }
1614 if(const auto plus = expr_try_dynamic_cast<plus_exprt>(expr))
1615 {
1616 return convert_expr_to_smt(*plus, converted, pointer_sizes);
1617 }
1618 if(const auto minus = expr_try_dynamic_cast<minus_exprt>(expr))
1619 {
1620 return convert_expr_to_smt(*minus, converted, pointer_sizes);
1621 }
1622 if(const auto divide = expr_try_dynamic_cast<div_exprt>(expr))
1623 {
1624 return convert_expr_to_smt(*divide, converted);
1625 }
1626 if(
1627 const auto float_operation =
1629 {
1630 return convert_expr_to_smt(*float_operation, converted);
1631 }
1632 if(const auto truncation_modulo = expr_try_dynamic_cast<mod_exprt>(expr))
1633 {
1634 return convert_expr_to_smt(*truncation_modulo, converted);
1635 }
1636 if(
1637 const auto euclidean_modulo =
1639 {
1640 return convert_expr_to_smt(*euclidean_modulo, converted);
1641 }
1642 if(const auto multiply = expr_try_dynamic_cast<mult_exprt>(expr))
1643 {
1644 return convert_expr_to_smt(*multiply, converted);
1645 }
1646#if 0
1647 else if(expr.id() == ID_floatbv_rem)
1648 {
1649 convert_floatbv_rem(to_binary_expr(expr));
1650 }
1651#endif
1652 if(const auto address_of = expr_try_dynamic_cast<address_of_exprt>(expr))
1653 {
1654 return convert_expr_to_smt(*address_of, converted, object_map);
1655 }
1656 if(const auto array_of = expr_try_dynamic_cast<array_of_exprt>(expr))
1657 {
1658 return convert_expr_to_smt(*array_of, converted);
1659 }
1660 if(
1661 const auto array_comprehension =
1663 {
1664 return convert_expr_to_smt(*array_comprehension, converted);
1665 }
1666 if(const auto index = expr_try_dynamic_cast<index_exprt>(expr))
1667 {
1668 return convert_expr_to_smt(*index, converted);
1669 }
1670 if(const auto shift = expr_try_dynamic_cast<shift_exprt>(expr))
1671 {
1672 return convert_expr_to_smt(*shift, converted);
1673 }
1674 if(const auto with = expr_try_dynamic_cast<with_exprt>(expr))
1675 {
1676 return convert_expr_to_smt(*with, converted);
1677 }
1678 if(const auto update = expr_try_dynamic_cast<update_exprt>(expr))
1679 {
1680 return convert_expr_to_smt(*update, converted);
1681 }
1682 if(const auto member_extraction = expr_try_dynamic_cast<member_exprt>(expr))
1683 {
1684 return convert_expr_to_smt(*member_extraction, converted);
1685 }
1686 else if(
1687 const auto pointer_offset =
1689 {
1690 return convert_expr_to_smt(*pointer_offset, converted);
1691 }
1692 else if(
1693 const auto pointer_object =
1695 {
1696 return convert_expr_to_smt(*pointer_object, converted);
1697 }
1698 if(
1699 const auto is_dynamic_object =
1701 {
1702 return convert_expr_to_smt(
1703 *is_dynamic_object, converted, apply_is_dynamic_object);
1704 }
1705 if(
1706 const auto is_invalid_pointer =
1708 {
1709 return convert_expr_to_smt(*is_invalid_pointer, object_map, converted);
1710 }
1711 if(const auto string_constant = expr_try_dynamic_cast<string_constantt>(expr))
1712 {
1713 return convert_expr_to_smt(*string_constant, converted);
1714 }
1715 if(const auto extract_bit = expr_try_dynamic_cast<extractbit_exprt>(expr))
1716 {
1717 return convert_expr_to_smt(*extract_bit, converted);
1718 }
1719 if(const auto extract_bits = expr_try_dynamic_cast<extractbits_exprt>(expr))
1720 {
1721 return convert_expr_to_smt(*extract_bits, converted);
1722 }
1723 if(const auto replication = expr_try_dynamic_cast<replication_exprt>(expr))
1724 {
1725 return convert_expr_to_smt(*replication, converted);
1726 }
1727 if(
1728 const auto byte_extraction =
1730 {
1731 return convert_expr_to_smt(*byte_extraction, converted);
1732 }
1733 if(const auto byte_update = expr_try_dynamic_cast<byte_update_exprt>(expr))
1734 {
1735 return convert_expr_to_smt(*byte_update, converted);
1736 }
1737 if(const auto absolute_value_of = expr_try_dynamic_cast<abs_exprt>(expr))
1738 {
1739 return convert_expr_to_smt(*absolute_value_of, converted);
1740 }
1741 if(const auto is_nan_expr = expr_try_dynamic_cast<isnan_exprt>(expr))
1742 {
1743 return convert_expr_to_smt(*is_nan_expr, converted);
1744 }
1745 if(const auto is_finite_expr = expr_try_dynamic_cast<isfinite_exprt>(expr))
1746 {
1747 return convert_expr_to_smt(*is_finite_expr, converted);
1748 }
1749 if(const auto is_infinite_expr = expr_try_dynamic_cast<isinf_exprt>(expr))
1750 {
1751 return convert_expr_to_smt(*is_infinite_expr, converted);
1752 }
1753 if(const auto is_normal_expr = expr_try_dynamic_cast<isnormal_exprt>(expr))
1754 {
1755 return convert_expr_to_smt(*is_normal_expr, converted);
1756 }
1757 if(
1758 const auto plus_overflow = expr_try_dynamic_cast<plus_overflow_exprt>(expr))
1759 {
1760 return convert_expr_to_smt(*plus_overflow, converted);
1761 }
1762 if(
1763 const auto minus_overflow =
1765 {
1766 return convert_expr_to_smt(*minus_overflow, converted);
1767 }
1768 if(
1769 const auto mult_overflow = expr_try_dynamic_cast<mult_overflow_exprt>(expr))
1770 {
1771 return convert_expr_to_smt(*mult_overflow, converted);
1772 }
1773 if(const auto shl_overflow = expr_try_dynamic_cast<shl_overflow_exprt>(expr))
1774 {
1775 return convert_expr_to_smt(*shl_overflow, converted);
1776 }
1777 if(const auto array_construction = expr_try_dynamic_cast<array_exprt>(expr))
1778 {
1779 return convert_expr_to_smt(*array_construction, converted);
1780 }
1781 if(const auto literal = expr_try_dynamic_cast<literal_exprt>(expr))
1782 {
1783 return convert_expr_to_smt(*literal, converted);
1784 }
1785 if(const auto for_all = expr_try_dynamic_cast<forall_exprt>(expr))
1786 {
1787 return convert_expr_to_smt(*for_all, converted);
1788 }
1789 if(const auto exists = expr_try_dynamic_cast<exists_exprt>(expr))
1790 {
1791 return convert_expr_to_smt(*exists, converted);
1792 }
1793 if(const auto vector = expr_try_dynamic_cast<vector_exprt>(expr))
1794 {
1795 return convert_expr_to_smt(*vector, converted);
1796 }
1798 {
1799 return convert_expr_to_smt(*object_size, converted, call_object_size);
1800 }
1801 if(const auto let = expr_try_dynamic_cast<let_exprt>(expr))
1802 {
1803 return convert_expr_to_smt(*let, converted);
1804 }
1805 INVARIANT(
1806 expr.id() != ID_constraint_select_one,
1807 "constraint_select_one is not expected in smt conversion: " +
1808 expr.pretty());
1809 if(const auto byte_swap = expr_try_dynamic_cast<bswap_exprt>(expr))
1810 {
1811 return convert_expr_to_smt(*byte_swap, converted);
1812 }
1813 if(const auto population_count = expr_try_dynamic_cast<popcount_exprt>(expr))
1814 {
1815 return convert_expr_to_smt(*population_count, converted);
1816 }
1817 if(
1818 const auto count_leading_zeros =
1820 {
1821 return convert_expr_to_smt(*count_leading_zeros, converted);
1822 }
1823 if(
1824 const auto count_trailing_zeros =
1826 {
1827 return convert_expr_to_smt(*count_trailing_zeros, converted);
1828 }
1829 if(const auto zero_extend = expr_try_dynamic_cast<zero_extend_exprt>(expr))
1830 {
1831 return convert_expr_to_smt(*zero_extend, converted);
1832 }
1833 if(
1834 const auto prophecy_r_or_w_ok =
1836 {
1837 return convert_expr_to_smt(*prophecy_r_or_w_ok, converted);
1838 }
1839 if(
1840 const auto prophecy_pointer_in_range =
1842 {
1843 return convert_expr_to_smt(*prophecy_pointer_in_range, converted);
1844 }
1845
1847 "Generation of SMT formula for unknown kind of expression: " +
1848 expr.pretty());
1849}
1850
1851#ifndef CPROVER_INVARIANT_DO_NOT_CHECK
1852template <typename functiont>
1865
1866template <typename functiont>
1868{
1869 return at_scope_exitt<functiont>(exit_function);
1870}
1871#endif
1872
1874{
1875 expr.visit_pre([](exprt &expr) {
1876 const auto address_of_expr = expr_try_dynamic_cast<address_of_exprt>(expr);
1877 if(!address_of_expr)
1878 return;
1879 const auto array_index_expr =
1880 expr_try_dynamic_cast<index_exprt>(address_of_expr->object());
1881 if(!array_index_expr)
1882 return;
1883 expr = plus_exprt{
1885 array_index_expr->array(),
1886 type_checked_cast<pointer_typet>(address_of_expr->type())},
1887 array_index_expr->index()};
1888 });
1889 return expr;
1890}
1891
1896 const exprt &_expr,
1897 std::function<bool(const exprt &)> filter,
1898 std::function<void(const exprt &)> visitor)
1899{
1900 struct stack_entryt
1901 {
1902 const exprt *e;
1903 bool operands_pushed;
1904 explicit stack_entryt(const exprt *_e) : e(_e), operands_pushed(false)
1905 {
1906 }
1907 };
1908
1909 std::stack<stack_entryt> stack;
1910
1911 stack.emplace(&_expr);
1912
1913 while(!stack.empty())
1914 {
1915 auto &top = stack.top();
1916 if(top.operands_pushed)
1917 {
1918 visitor(*top.e);
1919 stack.pop();
1920 }
1921 else
1922 {
1923 // do modification of 'top' before pushing in case 'top' isn't stable
1924 top.operands_pushed = true;
1925 if(filter(*top.e))
1926 for(auto &op : top.e->operands())
1927 stack.emplace(&op);
1928 }
1929 }
1930}
1931
1933 const exprt &expr,
1934 const smt_object_mapt &object_map,
1935 const type_size_mapt &pointer_sizes,
1937 const smt_is_dynamic_objectt::make_applicationt &is_dynamic_object)
1938{
1939#ifndef CPROVER_INVARIANT_DO_NOT_CHECK
1940 static bool in_conversion = false;
1941 INVARIANT(
1942 !in_conversion,
1943 "Conversion of expr to smt should be non-recursive. "
1944 "Re-entrance found in conversion of " +
1945 expr.pretty(1, 0));
1946 in_conversion = true;
1947 const auto end_conversion = at_scope_exit([&]() { in_conversion = false; });
1948#endif
1949 sub_expression_mapt sub_expression_map;
1950 const auto lowered_expr = lower_address_of_array_index(expr);
1952 lowered_expr,
1953 [](const exprt &expr) {
1954 // Code values inside "address of" expressions do not need to be converted
1955 // as the "address of" conversion only depends on the object identifier.
1956 // Avoiding the conversion side steps a need to convert arbitrary code to
1957 // SMT terms.
1958 const auto address_of = expr_try_dynamic_cast<address_of_exprt>(expr);
1959 if(!address_of)
1960 return true;
1961 return !can_cast_type<code_typet>(address_of->object().type());
1962 },
1963 [&](const exprt &expr) {
1964 const auto find_result = sub_expression_map.find(expr);
1965 if(find_result != sub_expression_map.cend())
1966 return;
1968 expr,
1969 sub_expression_map,
1970 object_map,
1971 pointer_sizes,
1973 is_dynamic_object);
1974 sub_expression_map.emplace_hint(find_result, expr, std::move(term));
1975 });
1976 return std::move(sub_expression_map.at(lowered_expr));
1977}
configt config
Definition config.cpp:25
mp_integer bvrep2integer(const irep_idt &src, std::size_t width, bool is_signed)
convert a bit-vector representation (possibly signed) to integer
std::size_t address_bits(const mp_integer &size)
ceil(log2(size))
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
Target numeric_cast_v(const mp_integer &arg)
Convert an mp_integer to integral type Target An invariant will fail if the conversion is not possibl...
std::optional< Target > numeric_cast(const exprt &arg)
Converts an expression to any integral type.
API to expression classes for bitvectors.
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< 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)
Definition c_types.cpp:235
typet c_bool_type()
Definition c_types.cpp:100
Absolute value.
Definition std_expr.h:442
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...
Boolean AND.
Definition std_expr.h:2125
Expression to define a mapping from an argument (index) to elements.
Definition std_expr.h:3544
Array constructor from list of elements.
Definition std_expr.h:1621
Array constructor from single element.
Definition std_expr.h:1558
Arrays with given size.
Definition std_types.h:807
typet index_type() const
The type of the index expressions into any instance of this type.
Definition std_types.cpp:34
const typet & element_type() const
The type of the elements of the array.
Definition std_types.h:827
exprt & lhs()
Definition std_expr.h:668
exprt & rhs()
Definition std_expr.h:678
exprt & op0()
Definition expr.h:133
exprt & op1()
Definition expr.h:136
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:762
Bit-wise AND.
Bit-wise negation of bit-vectors.
Bit-wise OR.
Base class of fixed-width bit-vector types.
Definition std_types.h:909
std::size_t get_width() const
Definition std_types.h:925
Bit-wise XOR.
The Boolean type.
Definition std_types.h:36
The byte swap expression.
Expression of type type extracted from some object op starting at position offset (given in number of...
Expression corresponding to op() where the bytes starting at position offset (given in number of byte...
The C/C++ Booleans.
Definition c_types.h:97
Concatenation of bit-vector operands.
A constant literal expression.
Definition std_expr.h:3118
bool is_null_pointer() const
Returns true if expr has a pointer type and a value NULL; it also returns true when expr has value ze...
Definition std_expr.cpp:25
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...
Division.
Definition std_expr.h:1157
Equality.
Definition std_expr.h:1366
Boute's Euclidean definition of Modulo – to match SMT-LIB2.
Definition std_expr.h:1296
An exists expression.
Base class for all expressions.
Definition expr.h:56
void visit_pre(std::function< void(exprt &)>)
Definition expr.cpp:227
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.
Extracts a sub-range of a bit-vector operand.
Semantic type conversion from/to floating-point formats.
A forall expression.
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.
Definition std_expr.h:2502
exprt & cond()
Definition std_expr.h:2519
exprt & false_case()
Definition std_expr.h:2539
exprt & true_case()
Definition std_expr.h:2529
Boolean implication.
Definition std_expr.h:2230
Array index operator.
Definition std_expr.h:1470
exprt & index()
Definition std_expr.h:1510
exprt & array()
Definition std_expr.h:1500
Unbounded, signed integers (mathematical integers, not bitvectors)
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition irep.cpp:482
const irep_idt & id() const
Definition irep.h:388
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.
A let expression.
Definition std_expr.h:3332
Extract member of struct or union.
Definition std_expr.h:2972
Binary minus.
Definition std_expr.h:1061
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
Definition std_expr.h:1228
Binary multiplication Associativity is not specified.
Definition std_expr.h:1107
A base class for multi-ary expressions Associativity is not specified.
Definition std_expr.h:912
Expression to hold a nondeterministic choice.
Definition std_expr.h:292
const irep_idt & get_identifier() const
Definition std_expr.h:320
Boolean negation.
Definition std_expr.h:2459
Disequality.
Definition std_expr.h:1425
Expression for finding the size (in bytes) of the object a pointer points to.
Boolean OR.
Definition std_expr.h:2275
The plus expression Associativity is not specified.
Definition std_expr.h:1002
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.
Bit-vector replication.
A base class for shift and rotate operators.
Sign of an expression Predicate is true if _op is negative, false otherwise.
Definition std_expr.h:596
static const smt_function_application_termt::factoryt< storet > store
static const smt_function_application_termt::factoryt< selectt > select
std::size_t bit_width() const
Definition smt_sorts.cpp:62
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.
Definition smt_terms.h:93
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition irep.cpp:482
const sub_classt * cast() const &
void accept(smt_sort_const_downcast_visitort &) const
Definition smt_sorts.cpp:97
const smt_sortt & get_sort() const
Definition smt_terms.cpp:36
Struct constructor from list of elements.
Definition std_expr.h:1877
Expression to hold a symbol (variable)
Definition std_expr.h:131
const irep_idt & get_identifier() const
Definition std_expr.h:160
Semantic type conversion.
Definition std_expr.h:2073
The type of an expression, extends irept.
Definition type.h:29
const exprt & op() const
Definition std_expr.h:391
The unary minus expression.
Definition std_expr.h:484
The unary plus expression.
Definition std_expr.h:531
Union constructor from single element.
Definition std_expr.h:1770
Operator to update elements in structs and arrays.
Definition std_expr.h:2783
Vector constructor from list of elements.
Definition std_expr.h:1734
Operator to update elements in structs and arrays.
Definition std_expr.h:2603
exprt & new_value()
Definition std_expr.h:2633
exprt & where()
Definition std_expr.h:2623
exprt & old()
Definition std_expr.h:2613
Boolean XOR.
Definition std_expr.h:2375
zero extension The operand is converted to the given type by either a) truncating if the new type is ...
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 std::optional< smt_termt > try_relational_conversion(const exprt &expr, const sub_expression_mapt &converted)
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::function< std::function< smt_termt(smt_termt)>(std::size_t)> extension_for_type(const typet &type)
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)
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.
at_scope_exitt< functiont > at_scope_exit(functiont exit_function)
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.
auto type_checked_cast(TType &base) -> typename detail::expr_dynamic_cast_return_typet< T, TType >::type
Cast a reference to a generic typet to a specific derived class and checks that the type could be con...
Definition expr_cast.h:242
auto type_try_dynamic_cast(TType &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TType >::type
Try to cast a reference to a generic typet to a specific derived class.
Definition expr_cast.h:135
bool can_cast_type(const typet &base)
Check whether a reference to a generic typet is of a specific derived class.
auto expr_try_dynamic_cast(TExpr &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TExpr >::type
Try to cast a reference to a generic exprt to a specific derived class.
Definition expr_cast.h:81
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)
Definition miniBDD.cpp:556
mp_integer bitwise_xor(const mp_integer &a, const mp_integer &b)
bitwise 'xor' of two nonnegative integers
Definition mp_arith.cpp:239
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)
Definition range.h:522
#define UNIMPLEMENTED_FEATURE(FEATURE)
Definition invariant.h:549
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
#define UNHANDLED_CASE
Definition invariant.h:559
#define POSTCONDITION(CONDITION)
Definition invariant.h:479
#define UNREACHABLE_BECAUSE(REASON)
Definition invariant.h:526
API to expression classes.
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition std_expr.h:715
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition std_expr.h:426
bool can_cast_type< code_typet >(const typet &type)
Check whether a reference to a typet is a code_typet.
Definition std_types.h:775
binary_relation_exprt less_than(exprt lhs, exprt rhs)
Definition string_expr.h:49
binary_relation_exprt greater_than(exprt lhs, exprt rhs)
Definition string_expr.h:26
at_scope_exitt(functiont exit_function)
smt_function_application_termt::factoryt< smt_command_functiont > make_applicationt
Function which makes applications of the smt function.
smt_function_application_termt::factoryt< smt_command_functiont > make_applicationt
Function which makes applications of the smt function.
void visit(const smt_array_sortt &) override
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
void visit(const smt_bit_vector_sortt &) override
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
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