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/expr_util.h>
10#include <util/floatbv_expr.h>
12#include <util/pointer_expr.h>
14#include <util/range.h>
15#include <util/std_expr.h>
17
23
24#include <algorithm>
25#include <functional>
26#include <numeric>
27#include <stack>
28
38using sub_expression_mapt = std::unordered_map<exprt, smt_termt, irep_hash>;
39
52template <typename factoryt>
54 const multi_ary_exprt &expr,
55 const sub_expression_mapt &converted,
56 const factoryt &factory)
57{
58 PRECONDITION(expr.operands().size() >= 2);
59 const auto operand_terms =
60 make_range(expr.operands()).map([&](const exprt &expr) {
61 return converted.at(expr);
62 });
63 return std::accumulate(
64 ++operand_terms.begin(),
65 operand_terms.end(),
66 *operand_terms.begin(),
67 factory);
68}
69
74template <typename target_typet>
75static bool operands_are_of_type(const exprt &expr)
76{
77 return std::all_of(
78 expr.operands().cbegin(), expr.operands().cend(), [](const exprt &operand) {
79 return can_cast_type<target_typet>(operand.type());
80 });
81}
82
84{
85 return smt_bool_sortt{};
86}
87
92
99
101{
102 if(const auto bool_type = type_try_dynamic_cast<bool_typet>(type))
103 {
104 return convert_type_to_smt_sort(*bool_type);
105 }
106 if(const auto bitvector_type = type_try_dynamic_cast<bitvector_typet>(type))
107 {
108 return convert_type_to_smt_sort(*bitvector_type);
109 }
110 if(const auto array_type = type_try_dynamic_cast<array_typet>(type))
111 {
112 return convert_type_to_smt_sort(*array_type);
113 }
114 UNIMPLEMENTED_FEATURE("Generation of SMT formula for type: " + type.pretty());
115}
116
118{
119 return smt_identifier_termt{symbol_expr.get_identifier(),
120 convert_type_to_smt_sort(symbol_expr.type())};
121}
122
124 const nondet_symbol_exprt &nondet_symbol,
125 const sub_expression_mapt &converted)
126{
127 // A nondet_symbol is a reference to an unconstrained function. This function
128 // will already have been added as a dependency.
130 nondet_symbol.get_identifier(),
131 convert_type_to_smt_sort(nondet_symbol.type())};
132}
133
135static smt_termt make_not_zero(const smt_termt &input, const typet &source_type)
136{
137 if(input.get_sort().cast<smt_bool_sortt>())
138 return input;
139 if(const auto bit_vector_sort = input.get_sort().cast<smt_bit_vector_sortt>())
140 {
142 input, smt_bit_vector_constant_termt{0, *bit_vector_sort});
143 }
145}
146
149 const smt_termt &from_term,
150 const typet &from_type,
151 const bitvector_typet &to_type)
152{
153 const std::size_t c_bool_width = to_type.get_width();
155 make_not_zero(from_term, from_type),
156 smt_bit_vector_constant_termt{1, c_bool_width},
157 smt_bit_vector_constant_termt{0, c_bool_width});
158}
159
160static std::function<std::function<smt_termt(smt_termt)>(std::size_t)>
173
175 const smt_termt &from_term,
177 const bitvector_typet &to_type)
178{
180 {
182 "Generation of SMT formula for type cast to fixed-point bitvector "
183 "type: " +
184 to_type.pretty());
185 }
187 {
189 "Generation of SMT formula for type cast to floating-point bitvector "
190 "type: " +
191 to_type.pretty());
192 }
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)
196 return from_term;
197 if(to_width < from_width)
198 return smt_bit_vector_theoryt::extract(to_width - 1, 0)(from_term);
199 const std::size_t extension_size = to_width - from_width;
200 return extension_for_type(from_type)(extension_size)(from_term);
201}
202
205{
209 std::optional<smt_termt> result;
210
218
219 void visit(const smt_bool_sortt &) override
220 {
223 }
224
225 void visit(const smt_bit_vector_sortt &) override
226 {
227 if(const auto bitvector = type_try_dynamic_cast<bitvector_typet>(from_type))
229 else
231 "Generation of SMT formula for type cast to bit vector from type: " +
232 from_type.pretty());
233 }
234
235 void visit(const smt_array_sortt &) override
236 {
238 "Generation of SMT formula for type cast to bit vector from type: " +
239 from_type.pretty());
240 }
241};
242
244 const smt_termt &from_term,
245 const typet &from_type,
246 const bitvector_typet &to_type)
247{
249 from_term, from_type, to_type};
250 from_term.get_sort().accept(converter);
251 POSTCONDITION(converter.result);
252 return *converter.result;
253}
254
256 const typecast_exprt &cast,
257 const sub_expression_mapt &converted)
258{
259 const auto &from_term = converted.at(cast.op());
260 const typet &from_type = cast.op().type();
261 const typet &to_type = cast.type();
262 if(const auto bool_type = type_try_dynamic_cast<bool_typet>(to_type))
263 return make_not_zero(from_term, cast.op().type());
264 if(const auto c_bool_type = type_try_dynamic_cast<c_bool_typet>(to_type))
265 return convert_c_bool_cast(from_term, from_type, *c_bool_type);
266 if(const auto bit_vector = type_try_dynamic_cast<bitvector_typet>(to_type))
267 return convert_bit_vector_cast(from_term, from_type, *bit_vector);
269 "Generation of SMT formula for type cast expression: " + cast.pretty());
270}
271
273 const floatbv_typecast_exprt &float_cast,
274 const sub_expression_mapt &converted)
275{
277 "Generation of SMT formula for floating point type cast expression: " +
278 float_cast.pretty());
279}
280
282 const struct_exprt &struct_construction,
283 const sub_expression_mapt &converted)
284{
286 "Generation of SMT formula for struct construction expression: " +
287 struct_construction.pretty());
288}
289
291 const union_exprt &union_construction,
292 const sub_expression_mapt &converted)
293{
295 "Generation of SMT formula for union construction expression: " +
296 union_construction.pretty());
297}
298
300{
302 std::optional<smt_termt> result;
303
305 : member_input{input}
306 {
307 }
308
309 void visit(const smt_bool_sortt &) override
310 {
312 }
313
314 void visit(const smt_bit_vector_sortt &bit_vector_sort) override
315 {
316 const auto &width = bit_vector_sort.bit_width();
317 // We get the value using a non-signed interpretation, as smt bit vector
318 // terms do not carry signedness.
319 const auto value = bvrep2integer(member_input.get_value(), width, false);
320 result = smt_bit_vector_constant_termt{value, bit_vector_sort};
321 }
322
323 void visit(const smt_array_sortt &array_sort) override
324 {
326 "Conversion of array SMT literal " + array_sort.pretty());
327 }
328};
329
330static smt_termt convert_expr_to_smt(const constant_exprt &constant_literal)
331{
332 if(is_null_pointer(constant_literal))
333 {
334 const size_t bit_width =
335 type_checked_cast<pointer_typet>(constant_literal.type()).get_width();
336 // An address of 0 encodes an object identifier of 0 for the NULL object
337 // and an offset of 0 into the object.
338 const auto address = 0;
339 return smt_bit_vector_constant_termt{address, bit_width};
340 }
341 if(constant_literal.type() == integer_typet{})
342 {
343 // This is converting integer constants into bit vectors for use with
344 // bit vector based smt logics. As bit vector widths are not specified for
345 // non bit vector types, this chooses a width based on the minimum needed
346 // to hold the integer constant value.
347 const auto value = numeric_cast_v<mp_integer>(constant_literal);
348 return smt_bit_vector_constant_termt{value, address_bits(value + 1)};
349 }
350 const auto sort = convert_type_to_smt_sort(constant_literal.type());
351 sort_based_literal_convertert converter(constant_literal);
352 sort.accept(converter);
353 return *converter.result;
354}
355
357 const concatenation_exprt &concatenation,
358 const sub_expression_mapt &converted)
359{
361 {
363 concatenation, converted, smt_bit_vector_theoryt::concat);
364 }
366 "Generation of SMT formula for concatenation expression: " +
367 concatenation.pretty());
368}
369
371 const bitand_exprt &bitwise_and_expr,
372 const sub_expression_mapt &converted)
373{
374 if(operands_are_of_type<bitvector_typet>(bitwise_and_expr))
375 {
377 bitwise_and_expr, converted, smt_bit_vector_theoryt::make_and);
378 }
379 else
380 {
382 "Generation of SMT formula for bitwise and expression: " +
383 bitwise_and_expr.pretty());
384 }
385}
386
388 const bitor_exprt &bitwise_or_expr,
389 const sub_expression_mapt &converted)
390{
391 if(operands_are_of_type<bitvector_typet>(bitwise_or_expr))
392 {
394 bitwise_or_expr, converted, smt_bit_vector_theoryt::make_or);
395 }
396 else
397 {
399 "Generation of SMT formula for bitwise or expression: " +
400 bitwise_or_expr.pretty());
401 }
402}
403
406 const sub_expression_mapt &converted)
407{
409 {
412 }
413 else
414 {
416 "Generation of SMT formula for bitwise xor expression: " +
417 bitwise_xor.pretty());
418 }
419}
420
422 const bitnot_exprt &bitwise_not,
423 const sub_expression_mapt &converted)
424{
425 if(can_cast_type<bitvector_typet>(bitwise_not.op().type()))
426 {
427 return smt_bit_vector_theoryt::make_not(converted.at(bitwise_not.op()));
428 }
429 else
430 {
432 "Generation of SMT formula for bitnot_exprt: " + bitwise_not.pretty());
433 }
434}
435
437 const unary_minus_exprt &unary_minus,
438 const sub_expression_mapt &converted)
439{
441 {
442 return smt_bit_vector_theoryt::negate(converted.at(unary_minus.op()));
443 }
444 else
445 {
447 "Generation of SMT formula for unary minus expression: " +
448 unary_minus.pretty());
449 }
450}
451
453 const unary_plus_exprt &unary_plus,
454 const sub_expression_mapt &converted)
455{
457 "Generation of SMT formula for unary plus expression: " +
458 unary_plus.pretty());
459}
460
462 const sign_exprt &is_negative,
463 const sub_expression_mapt &converted)
464{
466 "Generation of SMT formula for \"is negative\" expression: " +
467 is_negative.pretty());
468}
469
471 const if_exprt &if_expression,
472 const sub_expression_mapt &converted)
473{
475 converted.at(if_expression.cond()),
476 converted.at(if_expression.true_case()),
477 converted.at(if_expression.false_case()));
478}
479
481 const and_exprt &and_expression,
482 const sub_expression_mapt &converted)
483{
485 and_expression, converted, smt_core_theoryt::make_and);
486}
487
489 const or_exprt &or_expression,
490 const sub_expression_mapt &converted)
491{
493 or_expression, converted, smt_core_theoryt::make_or);
494}
495
497 const xor_exprt &xor_expression,
498 const sub_expression_mapt &converted)
499{
501 xor_expression, converted, smt_core_theoryt::make_xor);
502}
503
505 const implies_exprt &implies,
506 const sub_expression_mapt &converted)
507{
509 converted.at(implies.op0()), converted.at(implies.op1()));
510}
511
513 const not_exprt &logical_not,
514 const sub_expression_mapt &converted)
515{
516 return smt_core_theoryt::make_not(converted.at(logical_not.op()));
517}
518
520 const equal_exprt &equal,
521 const sub_expression_mapt &converted)
522{
524 converted.at(equal.op0()), converted.at(equal.op1()));
525}
526
528 const notequal_exprt &not_equal,
529 const sub_expression_mapt &converted)
530{
532 converted.at(not_equal.op0()), converted.at(not_equal.op1()));
533}
534
536 const ieee_float_equal_exprt &float_equal,
537 const sub_expression_mapt &converted)
538{
540 "Generation of SMT formula for floating point equality expression: " +
541 float_equal.pretty());
542}
543
545 const ieee_float_notequal_exprt &float_not_equal,
546 const sub_expression_mapt &converted)
547{
549 "Generation of SMT formula for floating point not equal expression: " +
550 float_not_equal.pretty());
551}
552
553template <typename unsigned_factory_typet, typename signed_factory_typet>
555 const binary_relation_exprt &binary_relation,
556 const unsigned_factory_typet &unsigned_factory,
557 const signed_factory_typet &signed_factory,
558 const sub_expression_mapt &converted)
559{
560 PRECONDITION(binary_relation.lhs().type() == binary_relation.rhs().type());
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();
564 if(can_cast_type<pointer_typet>(operand_type))
565 {
566 // The code here is operating under the assumption that the comparison
567 // operands have types for which the comparison makes sense.
568
569 // We already know this is the case given that we have followed
570 // the if statement branch, but including the same check here
571 // for consistency (it's cheap).
572 const auto lhs_type_is_pointer =
573 can_cast_type<pointer_typet>(binary_relation.lhs().type());
574 const auto rhs_type_is_pointer =
575 can_cast_type<pointer_typet>(binary_relation.rhs().type());
576 INVARIANT(
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);
580 }
581 else if(lhs.get_sort().cast<smt_bit_vector_sortt>())
582 {
583 if(can_cast_type<unsignedbv_typet>(operand_type))
584 return unsigned_factory(lhs, rhs);
585 if(can_cast_type<signedbv_typet>(operand_type))
586 return signed_factory(lhs, rhs);
587 }
588
590 "Generation of SMT formula for relational expression: " +
591 binary_relation.pretty());
592}
593
594static std::optional<smt_termt> try_relational_conversion(
595 const exprt &expr,
596 const sub_expression_mapt &converted)
597{
599 {
604 converted);
605 }
606 if(
607 const auto greater_than_or_equal =
609 {
611 *greater_than_or_equal,
614 converted);
615 }
617 {
619 *less_than,
622 converted);
623 }
624 if(
625 const auto less_than_or_equal =
627 {
629 *less_than_or_equal,
632 converted);
633 }
634 return {};
635}
636
638 const plus_exprt &plus,
639 const sub_expression_mapt &converted,
640 const type_size_mapt &pointer_sizes)
641{
642 if(std::all_of(
643 plus.operands().cbegin(), plus.operands().cend(), [](exprt operand) {
644 return can_cast_type<integer_bitvector_typet>(operand.type());
645 }))
646 {
648 plus, converted, smt_bit_vector_theoryt::add);
649 }
650 else if(can_cast_type<pointer_typet>(plus.type()))
651 {
652 INVARIANT(
653 plus.operands().size() == 2,
654 "We are only handling a binary version of plus when it has a pointer "
655 "operand");
656
657 exprt pointer;
658 exprt scalar;
659 for(auto &operand : plus.operands())
660 {
662 {
663 pointer = operand;
664 }
665 else
666 {
667 scalar = operand;
668 }
669 }
670
671 // We need to ensure that we follow this code path only if the expression
672 // our assumptions about the structure of the addition expression hold.
673 INVARIANT(
675 "An addition expression with both operands being pointers when they are "
676 "not dereferenced is malformed");
677
680 const auto base_type = pointer_type.base_type();
681 const auto pointer_size = pointer_sizes.at(base_type);
682
684 converted.at(pointer),
685 smt_bit_vector_theoryt::multiply(converted.at(scalar), pointer_size));
686 }
687 else
688 {
690 "Generation of SMT formula for plus expression: " + plus.pretty());
691 }
692}
693
695 const minus_exprt &minus,
696 const sub_expression_mapt &converted,
697 const type_size_mapt &pointer_sizes)
698{
699 const bool both_operands_bitvector =
702
703 const bool lhs_is_pointer = can_cast_type<pointer_typet>(minus.lhs().type());
704 const bool rhs_is_pointer = can_cast_type<pointer_typet>(minus.rhs().type());
705
706 const bool both_operands_pointers = lhs_is_pointer && rhs_is_pointer;
707
708 // We don't really handle this - we just compute this to fall
709 // into an if-else branch that gives proper error handling information.
710 const bool one_operand_pointer = lhs_is_pointer || rhs_is_pointer;
711
712 if(both_operands_bitvector)
713 {
715 converted.at(minus.lhs()), converted.at(minus.rhs()));
716 }
717 else if(both_operands_pointers)
718 {
719 const auto lhs_base_type = to_pointer_type(minus.lhs().type()).base_type();
720 const auto rhs_base_type = to_pointer_type(minus.rhs().type()).base_type();
721 INVARIANT(
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));
728 }
729 else if(one_operand_pointer)
730 {
731 // It's semantically void to have an expression `3 - a` where `a`
732 // is a pointer.
733 INVARIANT(
734 lhs_is_pointer,
735 "minus expressions of pointer and integer expect lhs to be the pointer");
736 const auto lhs_base_type = to_pointer_type(minus.lhs().type()).base_type();
737
739 converted.at(minus.lhs()),
741 converted.at(minus.rhs()), pointer_sizes.at(lhs_base_type)));
742 }
743 else
744 {
746 "Generation of SMT formula for minus expression: " + minus.pretty());
747 }
748}
749
751 const div_exprt &divide,
752 const sub_expression_mapt &converted)
753{
754 const smt_termt &lhs = converted.at(divide.lhs());
755 const smt_termt &rhs = converted.at(divide.rhs());
756
757 const bool both_operands_bitvector =
760
761 const bool both_operands_unsigned =
764
765 if(both_operands_bitvector)
766 {
767 if(both_operands_unsigned)
768 {
770 }
771 else
772 {
774 }
775 }
776 else
777 {
779 "Generation of SMT formula for divide expression: " + divide.pretty());
780 }
781}
782
784 const ieee_float_op_exprt &float_operation,
785 const sub_expression_mapt &converted)
786{
787 // This case includes the floating point plus, minus, division and
788 // multiplication operations.
790 "Generation of SMT formula for floating point operation expression: " +
791 float_operation.pretty());
792}
793
795 const mod_exprt &truncation_modulo,
796 const sub_expression_mapt &converted)
797{
798 const smt_termt &lhs = converted.at(truncation_modulo.lhs());
799 const smt_termt &rhs = converted.at(truncation_modulo.rhs());
800
801 const bool both_operands_bitvector =
802 can_cast_type<integer_bitvector_typet>(truncation_modulo.lhs().type()) &&
803 can_cast_type<integer_bitvector_typet>(truncation_modulo.rhs().type());
804
805 const bool both_operands_unsigned =
806 can_cast_type<unsignedbv_typet>(truncation_modulo.lhs().type()) &&
807 can_cast_type<unsignedbv_typet>(truncation_modulo.rhs().type());
808
809 if(both_operands_bitvector)
810 {
811 if(both_operands_unsigned)
812 {
814 }
815 else
816 {
818 }
819 }
820 else
821 {
823 "Generation of SMT formula for remainder (modulus) expression: " +
824 truncation_modulo.pretty());
825 }
826}
827
829 const euclidean_mod_exprt &euclidean_modulo,
830 const sub_expression_mapt &converted)
831{
833 "Generation of SMT formula for euclidean modulo expression: " +
834 euclidean_modulo.pretty());
835}
836
838 const mult_exprt &multiply,
839 const sub_expression_mapt &converted)
840{
841 if(std::all_of(
842 multiply.operands().cbegin(),
843 multiply.operands().cend(),
844 [](exprt operand) {
845 return can_cast_type<integer_bitvector_typet>(operand.type());
846 }))
847 {
849 multiply, converted, smt_bit_vector_theoryt::multiply);
850 }
851 else
852 {
854 "Generation of SMT formula for multiply expression: " +
855 multiply.pretty());
856 }
857}
858
867 const address_of_exprt &address_of,
868 const sub_expression_mapt &converted,
869 const smt_object_mapt &object_map)
870{
871 const auto type = type_try_dynamic_cast<pointer_typet>(address_of.type());
872 INVARIANT(
873 type, "Result of the address_of operator should have pointer type.");
874 const auto base = find_object_base_expression(address_of);
875 const auto object = object_map.find(base);
876 INVARIANT(
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;
880 const std::size_t object_bits = config.bv_encoding.object_bits;
881 const std::size_t max_objects = std::size_t(1) << object_bits;
882 if(object_id >= max_objects)
883 {
885 "too many addressed objects: maximum number of objects is set to 2^n=" +
886 std::to_string(max_objects) + " (with n=" + std::to_string(object_bits) +
887 "); " +
888 "use the `--object-bits n` option to increase the maximum number"};
889 }
890 const smt_termt object_bit_vector =
891 smt_bit_vector_constant_termt{object_id, object_bits};
892 INVARIANT(
893 type->get_width() > object_bits,
894 "Pointer should be wider than object_bits in order to allow for offset "
895 "encoding.");
896 const size_t offset_bits = type->get_width() - object_bits;
897 if(
898 const auto symbol =
900 {
901 const smt_bit_vector_constant_termt offset{0, offset_bits};
902 return smt_bit_vector_theoryt::concat(object_bit_vector, offset);
903 }
905 "Generation of SMT formula for address of expression: " +
906 address_of.pretty());
907}
908
910 const array_of_exprt &array_of,
911 const sub_expression_mapt &converted)
912{
913 // This function is unreachable as the `array_of_exprt` nodes are already
914 // fully converted by the incremental decision procedure functions
915 // (smt2_incremental_decision_proceduret::define_array_function).
917}
918
920 const array_comprehension_exprt &array_comprehension,
921 const sub_expression_mapt &converted)
922{
924 "Generation of SMT formula for array comprehension expression: " +
925 array_comprehension.pretty());
926}
927
929 const index_exprt &index_of,
930 const sub_expression_mapt &converted)
931{
932 const smt_termt &array = converted.at(index_of.array());
933 const smt_termt &index = converted.at(index_of.index());
934 return smt_array_theoryt::select(array, index);
935}
936
937template <typename factoryt, typename shiftt>
939 const factoryt &factory,
940 const shiftt &shift,
941 const sub_expression_mapt &converted)
942{
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 =
946 first_operand.get_sort().cast<smt_bit_vector_sortt>();
947 const auto second_bit_vector_sort =
948 second_operand.get_sort().cast<smt_bit_vector_sortt>();
949 INVARIANT(
950 first_bit_vector_sort && second_bit_vector_sort,
951 "Shift expressions are expected to have bit vector operands.");
952 INVARIANT(
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)
958 {
959 return factory(
960 first_operand,
961 extension_for_type(shift.op1().type())(first_width - second_width)(
962 second_operand));
963 }
964 else if(first_width < second_width)
965 {
966 const auto result = factory(
967 extension_for_type(shift.op0().type())(second_width - first_width)(
968 first_operand),
969 second_operand);
970 return smt_bit_vector_theoryt::extract(first_width - 1, 0)(result);
971 }
972 else
973 {
974 return factory(first_operand, second_operand);
975 }
976}
977
979 const shift_exprt &shift,
980 const sub_expression_mapt &converted)
981{
982 // TODO: Dispatch for rotation expressions. A `shift_exprt` can be a rotation.
983 if(const auto left_shift = expr_try_dynamic_cast<shl_exprt>(shift))
984 {
986 smt_bit_vector_theoryt::shift_left, *left_shift, converted);
987 }
988 if(const auto right_logical_shift = expr_try_dynamic_cast<lshr_exprt>(shift))
989 {
992 *right_logical_shift,
993 converted);
994 }
995 if(const auto right_arith_shift = expr_try_dynamic_cast<ashr_exprt>(shift))
996 {
999 *right_arith_shift,
1000 converted);
1001 }
1003 "Generation of SMT formula for shift expression: " + shift.pretty());
1004}
1005
1007 const with_exprt &with,
1008 const sub_expression_mapt &converted)
1009{
1010 smt_termt array = converted.at(with.old());
1011 for(auto it = ++with.operands().begin(); it != with.operands().end(); it += 2)
1012 {
1013 const smt_termt &index_term = converted.at(it[0]);
1014 const smt_termt &value_term = converted.at(it[1]);
1015 array = smt_array_theoryt::store(array, index_term, value_term);
1016 }
1017 return array;
1018}
1019
1021 const with_exprt &with,
1022 const sub_expression_mapt &converted)
1023{
1025 return convert_array_update_to_smt(with, converted);
1026 // 'with' expression is also used to update struct fields, but for now we do
1027 // not support them, so we fail.
1029 "Generation of SMT formula for with expression: " + with.pretty());
1030}
1031
1033 const update_exprt &update,
1034 const sub_expression_mapt &converted)
1035{
1037 "Generation of SMT formula for update expression: " + update.pretty());
1038}
1039
1041 const member_exprt &member_extraction,
1042 const sub_expression_mapt &converted)
1043{
1045 "Generation of SMT formula for member extraction expression: " +
1046 member_extraction.pretty());
1047}
1048
1050 const is_dynamic_object_exprt &is_dynamic_object,
1051 const sub_expression_mapt &converted,
1052 const smt_is_dynamic_objectt::make_applicationt &apply_is_dynamic_object)
1053{
1054 const smt_termt &pointer = converted.at(is_dynamic_object.address());
1055 const auto pointer_sort = pointer.get_sort().cast<smt_bit_vector_sortt>();
1056 INVARIANT(
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(
1060 std::vector<smt_termt>{smt_bit_vector_theoryt::extract(
1061 pointer_width - 1,
1062 pointer_width - config.bv_encoding.object_bits)(pointer)});
1063}
1064
1066 const is_invalid_pointer_exprt &is_invalid_pointer,
1067 const smt_object_mapt &object_map,
1068 const sub_expression_mapt &converted)
1069{
1070 const exprt &pointer_expr(to_unary_expr(is_invalid_pointer).op());
1073 INVARIANT(pointer_type, "Pointer object should have a bitvector-based type.");
1074 const std::size_t object_bits = config.bv_encoding.object_bits;
1075 const std::size_t width = pointer_type->get_width();
1076 INVARIANT(
1077 width >= object_bits,
1078 "Width should be at least as big as the number of object bits.");
1079
1080 const auto extract_op = smt_bit_vector_theoryt::extract(
1081 width - 1, width - object_bits)(converted.at(pointer_expr));
1082
1083 const auto &invalid_pointer = object_map.at(make_invalid_pointer_expr());
1084
1085 const smt_termt invalid_pointer_address = smt_bit_vector_constant_termt(
1086 invalid_pointer.unique_id, config.bv_encoding.object_bits);
1087
1088 return smt_core_theoryt::equal(invalid_pointer_address, extract_op);
1089}
1090
1092 const string_constantt &string_constant,
1093 const sub_expression_mapt &converted)
1094{
1096 "Generation of SMT formula for string constant expression: " +
1097 string_constant.pretty());
1098}
1099
1101 const extractbit_exprt &extract_bit,
1102 const sub_expression_mapt &converted)
1103{
1105 "Generation of SMT formula for extract bit expression: " +
1106 extract_bit.pretty());
1107}
1108
1110 const extractbits_exprt &extract_bits,
1111 const sub_expression_mapt &converted)
1112{
1113 const smt_termt &from = converted.at(extract_bits.src());
1114 const auto bit_vector_sort =
1116 INVARIANT(
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());
1119 if(index_value)
1121 *index_value + bit_vector_sort->bit_width() - 1, *index_value)(from);
1123 "Generation of SMT formula for extract bits expression: " +
1124 extract_bits.pretty());
1125}
1126
1128 const replication_exprt &replication,
1129 const sub_expression_mapt &converted)
1130{
1132 "Generation of SMT formula for bit vector replication expression: " +
1133 replication.pretty());
1134}
1135
1137 const byte_extract_exprt &byte_extraction,
1138 const sub_expression_mapt &converted)
1139{
1141 "Generation of SMT formula for byte extract expression: " +
1142 byte_extraction.pretty());
1143}
1144
1146 const byte_update_exprt &byte_update,
1147 const sub_expression_mapt &converted)
1148{
1150 "Generation of SMT formula for byte update expression: " +
1151 byte_update.pretty());
1152}
1153
1155 const abs_exprt &absolute_value_of,
1156 const sub_expression_mapt &converted)
1157{
1159 "Generation of SMT formula for absolute value of expression: " +
1160 absolute_value_of.pretty());
1161}
1162
1164 const isnan_exprt &is_nan_expr,
1165 const sub_expression_mapt &converted)
1166{
1168 "Generation of SMT formula for is not a number expression: " +
1169 is_nan_expr.pretty());
1170}
1171
1173 const isfinite_exprt &is_finite_expr,
1174 const sub_expression_mapt &converted)
1175{
1177 "Generation of SMT formula for is finite expression: " +
1178 is_finite_expr.pretty());
1179}
1180
1182 const isinf_exprt &is_infinite_expr,
1183 const sub_expression_mapt &converted)
1184{
1186 "Generation of SMT formula for is infinite expression: " +
1187 is_infinite_expr.pretty());
1188}
1189
1191 const isnormal_exprt &is_normal_expr,
1192 const sub_expression_mapt &converted)
1193{
1195 "Generation of SMT formula for is infinite expression: " +
1196 is_normal_expr.pretty());
1197}
1198
1203{
1204 const auto bit_vector_sort = input.get_sort().cast<smt_bit_vector_sortt>();
1205 INVARIANT(
1206 bit_vector_sort,
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;
1209 const auto extract_most_significant_bit = smt_bit_vector_theoryt::extract(
1210 most_significant_bit_index, most_significant_bit_index);
1212 extract_most_significant_bit(input), smt_bit_vector_constant_termt{1, 1});
1213}
1214
1216 const plus_overflow_exprt &plus_overflow,
1217 const sub_expression_mapt &converted)
1218{
1219 const smt_termt &left = converted.at(plus_overflow.lhs());
1220 const smt_termt &right = converted.at(plus_overflow.rhs());
1222 {
1223 const auto add_carry_bit = smt_bit_vector_theoryt::zero_extend(1);
1225 smt_bit_vector_theoryt::add(add_carry_bit(left), add_carry_bit(right)));
1226 }
1227 if(operands_are_of_type<signedbv_typet>(plus_overflow))
1228 {
1229 // Overflow has occurred if the operands have the same sign and adding them
1230 // gives a result of the opposite sign.
1231 const smt_termt msb_left = most_significant_bit_is_set(left);
1232 const smt_termt msb_right = most_significant_bit_is_set(right);
1234 smt_core_theoryt::equal(msb_left, msb_right),
1236 msb_left,
1238 }
1240 "Generation of SMT formula for plus overflow expression: " +
1241 plus_overflow.pretty());
1242}
1243
1245 const minus_overflow_exprt &minus_overflow,
1246 const sub_expression_mapt &converted)
1247{
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))
1251 {
1253 }
1254 if(operands_are_of_type<signedbv_typet>(minus_overflow))
1255 {
1256 // Overflow has occurred if the operands have the opposing signs and
1257 // subtracting them gives a result having the same signedness as the
1258 // right-hand operand. For example the following would be overflow for cases
1259 // for 8 bit wide bit vectors -
1260 // -128 - 1 == 127
1261 // 127 - (-1) == -128
1262 const smt_termt msb_left = most_significant_bit_is_set(left);
1263 const smt_termt msb_right = most_significant_bit_is_set(right);
1265 smt_core_theoryt::distinct(msb_left, msb_right),
1267 msb_right,
1269 smt_bit_vector_theoryt::subtract(left, right))));
1270 }
1272 "Generation of SMT formula for minus overflow expression: " +
1273 minus_overflow.pretty());
1274}
1275
1277 const mult_overflow_exprt &mult_overflow,
1278 const sub_expression_mapt &converted)
1279{
1280 PRECONDITION(mult_overflow.lhs().type() == mult_overflow.rhs().type());
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());
1284 if(
1285 const auto unsigned_type =
1287 {
1288 const std::size_t width = unsigned_type->get_width();
1289 const auto extend = smt_bit_vector_theoryt::zero_extend(width);
1291 smt_bit_vector_theoryt::multiply(extend(left), extend(right)),
1292 smt_bit_vector_constant_termt{power(2, width), width * 2});
1293 }
1294 if(
1295 const auto signed_type =
1297 {
1298 const smt_termt msb_left = most_significant_bit_is_set(left);
1299 const smt_termt msb_right = most_significant_bit_is_set(right);
1300 const std::size_t width = signed_type->get_width();
1301 const auto extend = smt_bit_vector_theoryt::sign_extend(width);
1302 const auto multiplication =
1303 smt_bit_vector_theoryt::multiply(extend(left), extend(right));
1305 multiplication,
1306 smt_bit_vector_constant_termt{power(2, width - 1), width * 2});
1307 const auto too_small = smt_bit_vector_theoryt::signed_less_than(
1308 multiplication,
1310 smt_bit_vector_constant_termt{power(2, width - 1), width * 2}));
1312 smt_core_theoryt::equal(msb_left, msb_right), too_large, too_small);
1313 }
1315 "Generation of SMT formula for multiply overflow expression: " +
1316 mult_overflow.pretty());
1317}
1318
1321 const sub_expression_mapt &converted)
1322{
1323 const auto type =
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();
1328 const std::size_t object_bits = config.bv_encoding.object_bits;
1329 INVARIANT(
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;
1333 const auto extract_op = smt_bit_vector_theoryt::extract(
1334 width - 1, width - object_bits)(converted_expr);
1335 if(ext > 0)
1336 {
1337 return smt_bit_vector_theoryt::zero_extend(ext)(extract_op);
1338 }
1339 return extract_op;
1340}
1341
1344 const sub_expression_mapt &converted)
1345{
1346 const auto type =
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();
1351 std::size_t offset_bits = width - config.bv_encoding.object_bits;
1352 if(offset_bits > width)
1353 offset_bits = width;
1354 const auto extract_op =
1355 smt_bit_vector_theoryt::extract(offset_bits - 1, 0)(converted_expr);
1356 if(width > offset_bits)
1357 {
1358 return smt_bit_vector_theoryt::sign_extend(width - offset_bits)(extract_op);
1359 }
1360 return extract_op;
1361}
1362
1364 const shl_overflow_exprt &shl_overflow,
1365 const sub_expression_mapt &converted)
1366{
1368 "Generation of SMT formula for shift left overflow expression: " +
1369 shl_overflow.pretty());
1370}
1371
1373 const array_exprt &array_construction,
1374 const sub_expression_mapt &converted)
1375{
1376 // This function is unreachable as the `array_exprt` nodes are already fully
1377 // converted by the incremental decision procedure functions
1378 // (smt2_incremental_decision_proceduret::define_array_function).
1380}
1381
1383 const literal_exprt &literal,
1384 const sub_expression_mapt &converted)
1385{
1387 "Generation of SMT formula for literal expression: " + literal.pretty());
1388}
1389
1391 const forall_exprt &for_all,
1392 const sub_expression_mapt &converted)
1393{
1395 "Generation of SMT formula for for all expression: " + for_all.pretty());
1396}
1397
1399 const exists_exprt &exists,
1400 const sub_expression_mapt &converted)
1401{
1403 "Generation of SMT formula for exists expression: " + exists.pretty());
1404}
1405
1407 const vector_exprt &vector,
1408 const sub_expression_mapt &converted)
1409{
1411 "Generation of SMT formula for vector expression: " + vector.pretty());
1412}
1413
1416 const sub_expression_mapt &converted,
1417 const smt_object_sizet::make_applicationt &call_object_size)
1418{
1419 const smt_termt &pointer = converted.at(object_size.pointer());
1420 const auto pointer_sort = pointer.get_sort().cast<smt_bit_vector_sortt>();
1421 INVARIANT(
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(
1425 std::vector<smt_termt>{smt_bit_vector_theoryt::extract(
1426 pointer_width - 1,
1427 pointer_width - config.bv_encoding.object_bits)(pointer)});
1428}
1429
1430static smt_termt
1432{
1434 "Generation of SMT formula for let expression: " + let.pretty());
1435}
1436
1438 const bswap_exprt &byte_swap,
1439 const sub_expression_mapt &converted)
1440{
1442 "Generation of SMT formula for byte swap expression: " +
1443 byte_swap.pretty());
1444}
1445
1447 const popcount_exprt &population_count,
1448 const sub_expression_mapt &converted)
1449{
1451 "Generation of SMT formula for population count expression: " +
1452 population_count.pretty());
1453}
1454
1456 const count_leading_zeros_exprt &count_leading_zeros,
1457 const sub_expression_mapt &converted)
1458{
1460 "Generation of SMT formula for count leading zeros expression: " +
1461 count_leading_zeros.pretty());
1462}
1463
1465 const count_trailing_zeros_exprt &count_trailing_zeros,
1466 const sub_expression_mapt &converted)
1467{
1469 "Generation of SMT formula for count trailing zeros expression: " +
1470 count_trailing_zeros.pretty());
1471}
1472
1474 const prophecy_r_or_w_ok_exprt &prophecy_r_or_w_ok,
1475 const sub_expression_mapt &converted)
1476{
1478 "prophecy_r_or_w_ok expression should have been lowered by the decision "
1479 "procedure before conversion to smt terms");
1480}
1481
1483 const prophecy_pointer_in_range_exprt &prophecy_pointer_in_range,
1484 const sub_expression_mapt &converted)
1485{
1487 "prophecy_pointer_in_range expression should have been lowered by the "
1488 "decision procedure before conversion to smt terms");
1489}
1490
1492 const exprt &expr,
1493 const sub_expression_mapt &converted,
1494 const smt_object_mapt &object_map,
1495 const type_size_mapt &pointer_sizes,
1496 const smt_object_sizet::make_applicationt &call_object_size,
1497 const smt_is_dynamic_objectt::make_applicationt &apply_is_dynamic_object)
1498{
1499 if(const auto symbol = expr_try_dynamic_cast<symbol_exprt>(expr))
1500 {
1501 return convert_expr_to_smt(*symbol);
1502 }
1503 if(const auto nondet = expr_try_dynamic_cast<nondet_symbol_exprt>(expr))
1504 {
1505 return convert_expr_to_smt(*nondet, converted);
1506 }
1507 if(const auto cast = expr_try_dynamic_cast<typecast_exprt>(expr))
1508 {
1509 return convert_expr_to_smt(*cast, converted);
1510 }
1511 if(
1512 const auto float_cast = expr_try_dynamic_cast<floatbv_typecast_exprt>(expr))
1513 {
1514 return convert_expr_to_smt(*float_cast, converted);
1515 }
1516 if(const auto struct_construction = expr_try_dynamic_cast<struct_exprt>(expr))
1517 {
1518 return convert_expr_to_smt(*struct_construction, converted);
1519 }
1520 if(const auto union_construction = expr_try_dynamic_cast<union_exprt>(expr))
1521 {
1522 return convert_expr_to_smt(*union_construction, converted);
1523 }
1524 if(const auto constant_literal = expr_try_dynamic_cast<constant_exprt>(expr))
1525 {
1526 return convert_expr_to_smt(*constant_literal);
1527 }
1528 if(
1529 const auto concatenation = expr_try_dynamic_cast<concatenation_exprt>(expr))
1530 {
1531 return convert_expr_to_smt(*concatenation, converted);
1532 }
1533 if(const auto bitwise_and_expr = expr_try_dynamic_cast<bitand_exprt>(expr))
1534 {
1535 return convert_expr_to_smt(*bitwise_and_expr, converted);
1536 }
1537 if(const auto bitwise_or_expr = expr_try_dynamic_cast<bitor_exprt>(expr))
1538 {
1539 return convert_expr_to_smt(*bitwise_or_expr, converted);
1540 }
1542 {
1543 return convert_expr_to_smt(*bitwise_xor, converted);
1544 }
1545 if(const auto bitwise_not = expr_try_dynamic_cast<bitnot_exprt>(expr))
1546 {
1547 return convert_expr_to_smt(*bitwise_not, converted);
1548 }
1549 if(const auto unary_minus = expr_try_dynamic_cast<unary_minus_exprt>(expr))
1550 {
1551 return convert_expr_to_smt(*unary_minus, converted);
1552 }
1553 if(const auto unary_plus = expr_try_dynamic_cast<unary_plus_exprt>(expr))
1554 {
1555 return convert_expr_to_smt(*unary_plus, converted);
1556 }
1557 if(const auto is_negative = expr_try_dynamic_cast<sign_exprt>(expr))
1558 {
1559 return convert_expr_to_smt(*is_negative, converted);
1560 }
1561 if(const auto if_expression = expr_try_dynamic_cast<if_exprt>(expr))
1562 {
1563 return convert_expr_to_smt(*if_expression, converted);
1564 }
1565 if(const auto and_expression = expr_try_dynamic_cast<and_exprt>(expr))
1566 {
1567 return convert_expr_to_smt(*and_expression, converted);
1568 }
1569 if(const auto or_expression = expr_try_dynamic_cast<or_exprt>(expr))
1570 {
1571 return convert_expr_to_smt(*or_expression, converted);
1572 }
1573 if(const auto xor_expression = expr_try_dynamic_cast<xor_exprt>(expr))
1574 {
1575 return convert_expr_to_smt(*xor_expression, converted);
1576 }
1577 if(const auto implies = expr_try_dynamic_cast<implies_exprt>(expr))
1578 {
1579 return convert_expr_to_smt(*implies, converted);
1580 }
1581 if(const auto logical_not = expr_try_dynamic_cast<not_exprt>(expr))
1582 {
1583 return convert_expr_to_smt(*logical_not, converted);
1584 }
1585 if(const auto equal = expr_try_dynamic_cast<equal_exprt>(expr))
1586 {
1587 return convert_expr_to_smt(*equal, converted);
1588 }
1589 if(const auto not_equal = expr_try_dynamic_cast<notequal_exprt>(expr))
1590 {
1591 return convert_expr_to_smt(*not_equal, converted);
1592 }
1593 if(
1594 const auto float_equal =
1596 {
1597 return convert_expr_to_smt(*float_equal, converted);
1598 }
1599 if(
1600 const auto float_not_equal =
1602 {
1603 return convert_expr_to_smt(*float_not_equal, converted);
1604 }
1605 if(
1606 const auto converted_relational =
1607 try_relational_conversion(expr, converted))
1608 {
1609 return *converted_relational;
1610 }
1611 if(const auto plus = expr_try_dynamic_cast<plus_exprt>(expr))
1612 {
1613 return convert_expr_to_smt(*plus, converted, pointer_sizes);
1614 }
1615 if(const auto minus = expr_try_dynamic_cast<minus_exprt>(expr))
1616 {
1617 return convert_expr_to_smt(*minus, converted, pointer_sizes);
1618 }
1619 if(const auto divide = expr_try_dynamic_cast<div_exprt>(expr))
1620 {
1621 return convert_expr_to_smt(*divide, converted);
1622 }
1623 if(
1624 const auto float_operation =
1626 {
1627 return convert_expr_to_smt(*float_operation, converted);
1628 }
1629 if(const auto truncation_modulo = expr_try_dynamic_cast<mod_exprt>(expr))
1630 {
1631 return convert_expr_to_smt(*truncation_modulo, converted);
1632 }
1633 if(
1634 const auto euclidean_modulo =
1636 {
1637 return convert_expr_to_smt(*euclidean_modulo, converted);
1638 }
1639 if(const auto multiply = expr_try_dynamic_cast<mult_exprt>(expr))
1640 {
1641 return convert_expr_to_smt(*multiply, converted);
1642 }
1643#if 0
1644 else if(expr.id() == ID_floatbv_rem)
1645 {
1646 convert_floatbv_rem(to_binary_expr(expr));
1647 }
1648#endif
1649 if(const auto address_of = expr_try_dynamic_cast<address_of_exprt>(expr))
1650 {
1651 return convert_expr_to_smt(*address_of, converted, object_map);
1652 }
1653 if(const auto array_of = expr_try_dynamic_cast<array_of_exprt>(expr))
1654 {
1655 return convert_expr_to_smt(*array_of, converted);
1656 }
1657 if(
1658 const auto array_comprehension =
1660 {
1661 return convert_expr_to_smt(*array_comprehension, converted);
1662 }
1663 if(const auto index = expr_try_dynamic_cast<index_exprt>(expr))
1664 {
1665 return convert_expr_to_smt(*index, converted);
1666 }
1667 if(const auto shift = expr_try_dynamic_cast<shift_exprt>(expr))
1668 {
1669 return convert_expr_to_smt(*shift, converted);
1670 }
1671 if(const auto with = expr_try_dynamic_cast<with_exprt>(expr))
1672 {
1673 return convert_expr_to_smt(*with, converted);
1674 }
1675 if(const auto update = expr_try_dynamic_cast<update_exprt>(expr))
1676 {
1677 return convert_expr_to_smt(*update, converted);
1678 }
1679 if(const auto member_extraction = expr_try_dynamic_cast<member_exprt>(expr))
1680 {
1681 return convert_expr_to_smt(*member_extraction, converted);
1682 }
1683 else if(
1684 const auto pointer_offset =
1686 {
1687 return convert_expr_to_smt(*pointer_offset, converted);
1688 }
1689 else if(
1690 const auto pointer_object =
1692 {
1693 return convert_expr_to_smt(*pointer_object, converted);
1694 }
1695 if(
1696 const auto is_dynamic_object =
1698 {
1699 return convert_expr_to_smt(
1700 *is_dynamic_object, converted, apply_is_dynamic_object);
1701 }
1702 if(
1703 const auto is_invalid_pointer =
1705 {
1706 return convert_expr_to_smt(*is_invalid_pointer, object_map, converted);
1707 }
1708 if(const auto string_constant = expr_try_dynamic_cast<string_constantt>(expr))
1709 {
1710 return convert_expr_to_smt(*string_constant, converted);
1711 }
1712 if(const auto extract_bit = expr_try_dynamic_cast<extractbit_exprt>(expr))
1713 {
1714 return convert_expr_to_smt(*extract_bit, converted);
1715 }
1716 if(const auto extract_bits = expr_try_dynamic_cast<extractbits_exprt>(expr))
1717 {
1718 return convert_expr_to_smt(*extract_bits, converted);
1719 }
1720 if(const auto replication = expr_try_dynamic_cast<replication_exprt>(expr))
1721 {
1722 return convert_expr_to_smt(*replication, converted);
1723 }
1724 if(
1725 const auto byte_extraction =
1727 {
1728 return convert_expr_to_smt(*byte_extraction, converted);
1729 }
1730 if(const auto byte_update = expr_try_dynamic_cast<byte_update_exprt>(expr))
1731 {
1732 return convert_expr_to_smt(*byte_update, converted);
1733 }
1734 if(const auto absolute_value_of = expr_try_dynamic_cast<abs_exprt>(expr))
1735 {
1736 return convert_expr_to_smt(*absolute_value_of, converted);
1737 }
1738 if(const auto is_nan_expr = expr_try_dynamic_cast<isnan_exprt>(expr))
1739 {
1740 return convert_expr_to_smt(*is_nan_expr, converted);
1741 }
1742 if(const auto is_finite_expr = expr_try_dynamic_cast<isfinite_exprt>(expr))
1743 {
1744 return convert_expr_to_smt(*is_finite_expr, converted);
1745 }
1746 if(const auto is_infinite_expr = expr_try_dynamic_cast<isinf_exprt>(expr))
1747 {
1748 return convert_expr_to_smt(*is_infinite_expr, converted);
1749 }
1750 if(const auto is_normal_expr = expr_try_dynamic_cast<isnormal_exprt>(expr))
1751 {
1752 return convert_expr_to_smt(*is_normal_expr, converted);
1753 }
1754 if(
1755 const auto plus_overflow = expr_try_dynamic_cast<plus_overflow_exprt>(expr))
1756 {
1757 return convert_expr_to_smt(*plus_overflow, converted);
1758 }
1759 if(
1760 const auto minus_overflow =
1762 {
1763 return convert_expr_to_smt(*minus_overflow, converted);
1764 }
1765 if(
1766 const auto mult_overflow = expr_try_dynamic_cast<mult_overflow_exprt>(expr))
1767 {
1768 return convert_expr_to_smt(*mult_overflow, converted);
1769 }
1770 if(const auto shl_overflow = expr_try_dynamic_cast<shl_overflow_exprt>(expr))
1771 {
1772 return convert_expr_to_smt(*shl_overflow, converted);
1773 }
1774 if(const auto array_construction = expr_try_dynamic_cast<array_exprt>(expr))
1775 {
1776 return convert_expr_to_smt(*array_construction, converted);
1777 }
1778 if(const auto literal = expr_try_dynamic_cast<literal_exprt>(expr))
1779 {
1780 return convert_expr_to_smt(*literal, converted);
1781 }
1782 if(const auto for_all = expr_try_dynamic_cast<forall_exprt>(expr))
1783 {
1784 return convert_expr_to_smt(*for_all, converted);
1785 }
1786 if(const auto exists = expr_try_dynamic_cast<exists_exprt>(expr))
1787 {
1788 return convert_expr_to_smt(*exists, converted);
1789 }
1790 if(const auto vector = expr_try_dynamic_cast<vector_exprt>(expr))
1791 {
1792 return convert_expr_to_smt(*vector, converted);
1793 }
1795 {
1796 return convert_expr_to_smt(*object_size, converted, call_object_size);
1797 }
1798 if(const auto let = expr_try_dynamic_cast<let_exprt>(expr))
1799 {
1800 return convert_expr_to_smt(*let, converted);
1801 }
1802 INVARIANT(
1803 expr.id() != ID_constraint_select_one,
1804 "constraint_select_one is not expected in smt conversion: " +
1805 expr.pretty());
1806 if(const auto byte_swap = expr_try_dynamic_cast<bswap_exprt>(expr))
1807 {
1808 return convert_expr_to_smt(*byte_swap, converted);
1809 }
1810 if(const auto population_count = expr_try_dynamic_cast<popcount_exprt>(expr))
1811 {
1812 return convert_expr_to_smt(*population_count, converted);
1813 }
1814 if(
1815 const auto count_leading_zeros =
1817 {
1818 return convert_expr_to_smt(*count_leading_zeros, converted);
1819 }
1820 if(
1821 const auto count_trailing_zeros =
1823 {
1824 return convert_expr_to_smt(*count_trailing_zeros, converted);
1825 }
1826 if(
1827 const auto prophecy_r_or_w_ok =
1829 {
1830 return convert_expr_to_smt(*prophecy_r_or_w_ok, converted);
1831 }
1832 if(
1833 const auto prophecy_pointer_in_range =
1835 {
1836 return convert_expr_to_smt(*prophecy_pointer_in_range, converted);
1837 }
1838
1840 "Generation of SMT formula for unknown kind of expression: " +
1841 expr.pretty());
1842}
1843
1844#ifndef CPROVER_INVARIANT_DO_NOT_CHECK
1845template <typename functiont>
1858
1859template <typename functiont>
1861{
1862 return at_scope_exitt<functiont>(exit_function);
1863}
1864#endif
1865
1867{
1868 expr.visit_pre([](exprt &expr) {
1869 const auto address_of_expr = expr_try_dynamic_cast<address_of_exprt>(expr);
1870 if(!address_of_expr)
1871 return;
1872 const auto array_index_expr =
1873 expr_try_dynamic_cast<index_exprt>(address_of_expr->object());
1874 if(!array_index_expr)
1875 return;
1876 expr = plus_exprt{
1878 array_index_expr->array(),
1879 type_checked_cast<pointer_typet>(address_of_expr->type())},
1880 array_index_expr->index()};
1881 });
1882 return expr;
1883}
1884
1889 const exprt &_expr,
1890 std::function<bool(const exprt &)> filter,
1891 std::function<void(const exprt &)> visitor)
1892{
1893 struct stack_entryt
1894 {
1895 const exprt *e;
1896 bool operands_pushed;
1897 explicit stack_entryt(const exprt *_e) : e(_e), operands_pushed(false)
1898 {
1899 }
1900 };
1901
1902 std::stack<stack_entryt> stack;
1903
1904 stack.emplace(&_expr);
1905
1906 while(!stack.empty())
1907 {
1908 auto &top = stack.top();
1909 if(top.operands_pushed)
1910 {
1911 visitor(*top.e);
1912 stack.pop();
1913 }
1914 else
1915 {
1916 // do modification of 'top' before pushing in case 'top' isn't stable
1917 top.operands_pushed = true;
1918 if(filter(*top.e))
1919 for(auto &op : top.e->operands())
1920 stack.emplace(&op);
1921 }
1922 }
1923}
1924
1926 const exprt &expr,
1927 const smt_object_mapt &object_map,
1928 const type_size_mapt &pointer_sizes,
1930 const smt_is_dynamic_objectt::make_applicationt &is_dynamic_object)
1931{
1932#ifndef CPROVER_INVARIANT_DO_NOT_CHECK
1933 static bool in_conversion = false;
1934 INVARIANT(
1935 !in_conversion,
1936 "Conversion of expr to smt should be non-recursive. "
1937 "Re-entrance found in conversion of " +
1938 expr.pretty(1, 0));
1939 in_conversion = true;
1940 const auto end_conversion = at_scope_exit([&]() { in_conversion = false; });
1941#endif
1942 sub_expression_mapt sub_expression_map;
1943 const auto lowered_expr = lower_address_of_array_index(expr);
1945 lowered_expr,
1946 [](const exprt &expr) {
1947 // Code values inside "address of" expressions do not need to be converted
1948 // as the "address of" conversion only depends on the object identifier.
1949 // Avoiding the conversion side steps a need to convert arbitrary code to
1950 // SMT terms.
1951 const auto address_of = expr_try_dynamic_cast<address_of_exprt>(expr);
1952 if(!address_of)
1953 return true;
1954 return !can_cast_type<code_typet>(address_of->object().type());
1955 },
1956 [&](const exprt &expr) {
1957 const auto find_result = sub_expression_map.find(expr);
1958 if(find_result != sub_expression_map.cend())
1959 return;
1961 expr,
1962 sub_expression_map,
1963 object_map,
1964 pointer_sizes,
1966 is_dynamic_object);
1967 sub_expression_map.emplace_hint(find_result, expr, std::move(term));
1968 });
1969 return std::move(sub_expression_map.at(lowered_expr));
1970}
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< signedbv_typet >(const typet &type)
Check whether a reference to a typet is a signedbv_typet.
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_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.
bool can_cast_type< unsignedbv_typet >(const typet &type)
Check whether a reference to a typet is a unsignedbv_typet.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_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:2120
Expression to define a mapping from an argument (index) to elements.
Definition std_expr.h:3405
Array constructor from list of elements.
Definition std_expr.h:1616
Array constructor from single element.
Definition std_expr.h:1553
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:33
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:920
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.
struct configt::bv_encodingt bv_encoding
A constant literal expression.
Definition std_expr.h:2987
const irep_idt & get_value() const
Definition std_expr.h:2995
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:1152
Equality.
Definition std_expr.h:1361
Boute's Euclidean definition of Modulo – to match SMT-LIB2.
Definition std_expr.h:1291
An exists expression.
Base class for all expressions.
Definition expr.h:56
bool is_true() const
Return whether the expression is a constant representing true.
Definition expr.cpp:27
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:2370
exprt & cond()
Definition std_expr.h:2387
exprt & false_case()
Definition std_expr.h:2407
exprt & true_case()
Definition std_expr.h:2397
Boolean implication.
Definition std_expr.h:2183
Array index operator.
Definition std_expr.h:1465
exprt & index()
Definition std_expr.h:1505
exprt & array()
Definition std_expr.h:1495
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:3196
Extract member of struct or union.
Definition std_expr.h:2841
Binary minus.
Definition std_expr.h:1061
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
Definition std_expr.h:1223
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:2327
Disequality.
Definition std_expr.h:1420
Expression for finding the size (in bytes) of the object a pointer points to.
Boolean OR.
Definition std_expr.h:2228
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:1872
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:2068
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:1765
Operator to update elements in structs and arrays.
Definition std_expr.h:2655
Vector constructor from list of elements.
Definition std_expr.h:1729
Operator to update elements in structs and arrays.
Definition std_expr.h:2471
exprt & old()
Definition std_expr.h:2481
Boolean XOR.
Definition std_expr.h:2291
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
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
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)
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< array_typet >(const typet &type)
Check whether a reference to a typet is a array_typet.
Definition std_types.h:875
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
bool can_cast_type< bitvector_typet >(const typet &type)
Check whether a reference to a typet is a bitvector_typet.
Definition std_types.h:943
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)
std::size_t object_bits
Definition config.h:355
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