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 for(auto it = ++with.operands().begin(); it != with.operands().end(); it += 2)
1009 {
1010 const smt_termt &index_term = converted.at(it[0]);
1011 const smt_termt &value_term = converted.at(it[1]);
1012 array = smt_array_theoryt::store(array, index_term, value_term);
1013 }
1014 return array;
1015}
1016
1018 const with_exprt &with,
1019 const sub_expression_mapt &converted)
1020{
1022 return convert_array_update_to_smt(with, converted);
1023 // 'with' expression is also used to update struct fields, but for now we do
1024 // not support them, so we fail.
1026 "Generation of SMT formula for with expression: " + with.pretty());
1027}
1028
1030 const update_exprt &update,
1031 const sub_expression_mapt &converted)
1032{
1034 "Generation of SMT formula for update expression: " + update.pretty());
1035}
1036
1038 const member_exprt &member_extraction,
1039 const sub_expression_mapt &converted)
1040{
1042 "Generation of SMT formula for member extraction expression: " +
1043 member_extraction.pretty());
1044}
1045
1047 const is_dynamic_object_exprt &is_dynamic_object,
1048 const sub_expression_mapt &converted,
1049 const smt_is_dynamic_objectt::make_applicationt &apply_is_dynamic_object)
1050{
1051 const smt_termt &pointer = converted.at(is_dynamic_object.address());
1052 const auto pointer_sort = pointer.get_sort().cast<smt_bit_vector_sortt>();
1053 INVARIANT(
1054 pointer_sort, "Pointers should be encoded as bit vector sorted terms.");
1055 const std::size_t pointer_width = pointer_sort->bit_width();
1056 return apply_is_dynamic_object(
1057 std::vector<smt_termt>{smt_bit_vector_theoryt::extract(
1058 pointer_width - 1,
1059 pointer_width - config.bv_encoding.object_bits)(pointer)});
1060}
1061
1063 const is_invalid_pointer_exprt &is_invalid_pointer,
1064 const smt_object_mapt &object_map,
1065 const sub_expression_mapt &converted)
1066{
1067 const exprt &pointer_expr(to_unary_expr(is_invalid_pointer).op());
1070 INVARIANT(pointer_type, "Pointer object should have a bitvector-based type.");
1071 const std::size_t object_bits = config.bv_encoding.object_bits;
1072 const std::size_t width = pointer_type->get_width();
1073 INVARIANT(
1074 width >= object_bits,
1075 "Width should be at least as big as the number of object bits.");
1076
1077 const auto extract_op = smt_bit_vector_theoryt::extract(
1078 width - 1, width - object_bits)(converted.at(pointer_expr));
1079
1080 const auto &invalid_pointer = object_map.at(make_invalid_pointer_expr());
1081
1082 const smt_termt invalid_pointer_address = smt_bit_vector_constant_termt(
1083 invalid_pointer.unique_id, config.bv_encoding.object_bits);
1084
1085 return smt_core_theoryt::equal(invalid_pointer_address, extract_op);
1086}
1087
1089 const string_constantt &string_constant,
1090 const sub_expression_mapt &converted)
1091{
1093 "Generation of SMT formula for string constant expression: " +
1094 string_constant.pretty());
1095}
1096
1098 const extractbit_exprt &extract_bit,
1099 const sub_expression_mapt &converted)
1100{
1102 "Generation of SMT formula for extract bit expression: " +
1103 extract_bit.pretty());
1104}
1105
1107 const extractbits_exprt &extract_bits,
1108 const sub_expression_mapt &converted)
1109{
1110 const smt_termt &from = converted.at(extract_bits.src());
1111 const auto bit_vector_sort =
1113 INVARIANT(
1114 bit_vector_sort, "Extract can only be applied to bit vector terms.");
1115 const auto index_value = numeric_cast<std::size_t>(extract_bits.index());
1116 if(index_value)
1118 *index_value + bit_vector_sort->bit_width() - 1, *index_value)(from);
1120 "Generation of SMT formula for extract bits expression: " +
1121 extract_bits.pretty());
1122}
1123
1125 const replication_exprt &replication,
1126 const sub_expression_mapt &converted)
1127{
1129 "Generation of SMT formula for bit vector replication expression: " +
1130 replication.pretty());
1131}
1132
1134 const byte_extract_exprt &byte_extraction,
1135 const sub_expression_mapt &converted)
1136{
1138 "Generation of SMT formula for byte extract expression: " +
1139 byte_extraction.pretty());
1140}
1141
1143 const byte_update_exprt &byte_update,
1144 const sub_expression_mapt &converted)
1145{
1147 "Generation of SMT formula for byte update expression: " +
1148 byte_update.pretty());
1149}
1150
1152 const abs_exprt &absolute_value_of,
1153 const sub_expression_mapt &converted)
1154{
1156 "Generation of SMT formula for absolute value of expression: " +
1157 absolute_value_of.pretty());
1158}
1159
1161 const isnan_exprt &is_nan_expr,
1162 const sub_expression_mapt &converted)
1163{
1165 "Generation of SMT formula for is not a number expression: " +
1166 is_nan_expr.pretty());
1167}
1168
1170 const isfinite_exprt &is_finite_expr,
1171 const sub_expression_mapt &converted)
1172{
1174 "Generation of SMT formula for is finite expression: " +
1175 is_finite_expr.pretty());
1176}
1177
1179 const isinf_exprt &is_infinite_expr,
1180 const sub_expression_mapt &converted)
1181{
1183 "Generation of SMT formula for is infinite expression: " +
1184 is_infinite_expr.pretty());
1185}
1186
1188 const isnormal_exprt &is_normal_expr,
1189 const sub_expression_mapt &converted)
1190{
1192 "Generation of SMT formula for is infinite expression: " +
1193 is_normal_expr.pretty());
1194}
1195
1200{
1201 const auto bit_vector_sort = input.get_sort().cast<smt_bit_vector_sortt>();
1202 INVARIANT(
1203 bit_vector_sort,
1204 "Most significant bit can only be extracted from bit vector terms.");
1205 const size_t most_significant_bit_index = bit_vector_sort->bit_width() - 1;
1206 const auto extract_most_significant_bit = smt_bit_vector_theoryt::extract(
1207 most_significant_bit_index, most_significant_bit_index);
1209 extract_most_significant_bit(input), smt_bit_vector_constant_termt{1, 1});
1210}
1211
1213 const plus_overflow_exprt &plus_overflow,
1214 const sub_expression_mapt &converted)
1215{
1216 const smt_termt &left = converted.at(plus_overflow.lhs());
1217 const smt_termt &right = converted.at(plus_overflow.rhs());
1219 {
1220 const auto add_carry_bit = smt_bit_vector_theoryt::zero_extend(1);
1222 smt_bit_vector_theoryt::add(add_carry_bit(left), add_carry_bit(right)));
1223 }
1224 if(operands_are_of_type<signedbv_typet>(plus_overflow))
1225 {
1226 // Overflow has occurred if the operands have the same sign and adding them
1227 // gives a result of the opposite sign.
1228 const smt_termt msb_left = most_significant_bit_is_set(left);
1229 const smt_termt msb_right = most_significant_bit_is_set(right);
1231 smt_core_theoryt::equal(msb_left, msb_right),
1233 msb_left,
1235 }
1237 "Generation of SMT formula for plus overflow expression: " +
1238 plus_overflow.pretty());
1239}
1240
1242 const minus_overflow_exprt &minus_overflow,
1243 const sub_expression_mapt &converted)
1244{
1245 const smt_termt &left = converted.at(minus_overflow.lhs());
1246 const smt_termt &right = converted.at(minus_overflow.rhs());
1247 if(operands_are_of_type<unsignedbv_typet>(minus_overflow))
1248 {
1250 }
1251 if(operands_are_of_type<signedbv_typet>(minus_overflow))
1252 {
1253 // Overflow has occurred if the operands have the opposing signs and
1254 // subtracting them gives a result having the same signedness as the
1255 // right-hand operand. For example the following would be overflow for cases
1256 // for 8 bit wide bit vectors -
1257 // -128 - 1 == 127
1258 // 127 - (-1) == -128
1259 const smt_termt msb_left = most_significant_bit_is_set(left);
1260 const smt_termt msb_right = most_significant_bit_is_set(right);
1262 smt_core_theoryt::distinct(msb_left, msb_right),
1264 msb_right,
1266 smt_bit_vector_theoryt::subtract(left, right))));
1267 }
1269 "Generation of SMT formula for minus overflow expression: " +
1270 minus_overflow.pretty());
1271}
1272
1274 const mult_overflow_exprt &mult_overflow,
1275 const sub_expression_mapt &converted)
1276{
1277 PRECONDITION(mult_overflow.lhs().type() == mult_overflow.rhs().type());
1278 const auto &operand_type = mult_overflow.lhs().type();
1279 const smt_termt &left = converted.at(mult_overflow.lhs());
1280 const smt_termt &right = converted.at(mult_overflow.rhs());
1281 if(
1282 const auto unsigned_type =
1284 {
1285 const std::size_t width = unsigned_type->get_width();
1286 const auto extend = smt_bit_vector_theoryt::zero_extend(width);
1288 smt_bit_vector_theoryt::multiply(extend(left), extend(right)),
1289 smt_bit_vector_constant_termt{power(2, width), width * 2});
1290 }
1291 if(
1292 const auto signed_type =
1294 {
1295 const smt_termt msb_left = most_significant_bit_is_set(left);
1296 const smt_termt msb_right = most_significant_bit_is_set(right);
1297 const std::size_t width = signed_type->get_width();
1298 const auto extend = smt_bit_vector_theoryt::sign_extend(width);
1299 const auto multiplication =
1300 smt_bit_vector_theoryt::multiply(extend(left), extend(right));
1302 multiplication,
1303 smt_bit_vector_constant_termt{power(2, width - 1), width * 2});
1304 const auto too_small = smt_bit_vector_theoryt::signed_less_than(
1305 multiplication,
1307 smt_bit_vector_constant_termt{power(2, width - 1), width * 2}));
1309 smt_core_theoryt::equal(msb_left, msb_right), too_large, too_small);
1310 }
1312 "Generation of SMT formula for multiply overflow expression: " +
1313 mult_overflow.pretty());
1314}
1315
1318 const sub_expression_mapt &converted)
1319{
1320 const auto type =
1322 INVARIANT(type, "Pointer object should have a bitvector-based type.");
1323 const auto converted_expr = converted.at(pointer_object.pointer());
1324 const std::size_t width = type->get_width();
1325 const std::size_t object_bits = config.bv_encoding.object_bits;
1326 INVARIANT(
1327 width >= object_bits,
1328 "Width should be at least as big as the number of object bits.");
1329 const std::size_t ext = width - object_bits;
1330 const auto extract_op = smt_bit_vector_theoryt::extract(
1331 width - 1, width - object_bits)(converted_expr);
1332 if(ext > 0)
1333 {
1334 return smt_bit_vector_theoryt::zero_extend(ext)(extract_op);
1335 }
1336 return extract_op;
1337}
1338
1341 const sub_expression_mapt &converted)
1342{
1343 const auto type =
1345 INVARIANT(type, "Pointer offset should have a bitvector-based type.");
1346 const auto converted_expr = converted.at(pointer_offset.pointer());
1347 const std::size_t width = type->get_width();
1348 std::size_t offset_bits = width - config.bv_encoding.object_bits;
1349 if(offset_bits > width)
1350 offset_bits = width;
1351 const auto extract_op =
1352 smt_bit_vector_theoryt::extract(offset_bits - 1, 0)(converted_expr);
1353 if(width > offset_bits)
1354 {
1355 return smt_bit_vector_theoryt::sign_extend(width - offset_bits)(extract_op);
1356 }
1357 return extract_op;
1358}
1359
1361 const shl_overflow_exprt &shl_overflow,
1362 const sub_expression_mapt &converted)
1363{
1365 "Generation of SMT formula for shift left overflow expression: " +
1366 shl_overflow.pretty());
1367}
1368
1370 const array_exprt &array_construction,
1371 const sub_expression_mapt &converted)
1372{
1373 // This function is unreachable as the `array_exprt` nodes are already fully
1374 // converted by the incremental decision procedure functions
1375 // (smt2_incremental_decision_proceduret::define_array_function).
1377}
1378
1380 const literal_exprt &literal,
1381 const sub_expression_mapt &converted)
1382{
1384 "Generation of SMT formula for literal expression: " + literal.pretty());
1385}
1386
1388 const forall_exprt &for_all,
1389 const sub_expression_mapt &converted)
1390{
1392 "Generation of SMT formula for for all expression: " + for_all.pretty());
1393}
1394
1396 const exists_exprt &exists,
1397 const sub_expression_mapt &converted)
1398{
1400 "Generation of SMT formula for exists expression: " + exists.pretty());
1401}
1402
1404 const vector_exprt &vector,
1405 const sub_expression_mapt &converted)
1406{
1408 "Generation of SMT formula for vector expression: " + vector.pretty());
1409}
1410
1413 const sub_expression_mapt &converted,
1414 const smt_object_sizet::make_applicationt &call_object_size)
1415{
1416 const smt_termt &pointer = converted.at(object_size.pointer());
1417 const auto pointer_sort = pointer.get_sort().cast<smt_bit_vector_sortt>();
1418 INVARIANT(
1419 pointer_sort, "Pointers should be encoded as bit vector sorted terms.");
1420 const std::size_t pointer_width = pointer_sort->bit_width();
1421 return call_object_size(
1422 std::vector<smt_termt>{smt_bit_vector_theoryt::extract(
1423 pointer_width - 1,
1424 pointer_width - config.bv_encoding.object_bits)(pointer)});
1425}
1426
1427static smt_termt
1429{
1431 "Generation of SMT formula for let expression: " + let.pretty());
1432}
1433
1435 const bswap_exprt &byte_swap,
1436 const sub_expression_mapt &converted)
1437{
1439 "Generation of SMT formula for byte swap expression: " +
1440 byte_swap.pretty());
1441}
1442
1444 const popcount_exprt &population_count,
1445 const sub_expression_mapt &converted)
1446{
1448 "Generation of SMT formula for population count expression: " +
1449 population_count.pretty());
1450}
1451
1453 const count_leading_zeros_exprt &count_leading_zeros,
1454 const sub_expression_mapt &converted)
1455{
1457 "Generation of SMT formula for count leading zeros expression: " +
1458 count_leading_zeros.pretty());
1459}
1460
1462 const count_trailing_zeros_exprt &count_trailing_zeros,
1463 const sub_expression_mapt &converted)
1464{
1466 "Generation of SMT formula for count trailing zeros expression: " +
1467 count_trailing_zeros.pretty());
1468}
1469
1471 const zero_extend_exprt &zero_extend,
1472 const sub_expression_mapt &converted)
1473{
1475 "zero_extend expression should have been lowered by the decision "
1476 "procedure before conversion to smt terms");
1477}
1478
1480 const prophecy_r_or_w_ok_exprt &prophecy_r_or_w_ok,
1481 const sub_expression_mapt &converted)
1482{
1484 "prophecy_r_or_w_ok expression should have been lowered by the decision "
1485 "procedure before conversion to smt terms");
1486}
1487
1489 const prophecy_pointer_in_range_exprt &prophecy_pointer_in_range,
1490 const sub_expression_mapt &converted)
1491{
1493 "prophecy_pointer_in_range expression should have been lowered by the "
1494 "decision procedure before conversion to smt terms");
1495}
1496
1498 const exprt &expr,
1499 const sub_expression_mapt &converted,
1500 const smt_object_mapt &object_map,
1501 const type_size_mapt &pointer_sizes,
1502 const smt_object_sizet::make_applicationt &call_object_size,
1503 const smt_is_dynamic_objectt::make_applicationt &apply_is_dynamic_object)
1504{
1505 if(const auto symbol = expr_try_dynamic_cast<symbol_exprt>(expr))
1506 {
1507 return convert_expr_to_smt(*symbol);
1508 }
1509 if(const auto nondet = expr_try_dynamic_cast<nondet_symbol_exprt>(expr))
1510 {
1511 return convert_expr_to_smt(*nondet, converted);
1512 }
1513 if(const auto cast = expr_try_dynamic_cast<typecast_exprt>(expr))
1514 {
1515 return convert_expr_to_smt(*cast, converted);
1516 }
1517 if(
1518 const auto float_cast = expr_try_dynamic_cast<floatbv_typecast_exprt>(expr))
1519 {
1520 return convert_expr_to_smt(*float_cast, converted);
1521 }
1522 if(const auto struct_construction = expr_try_dynamic_cast<struct_exprt>(expr))
1523 {
1524 return convert_expr_to_smt(*struct_construction, converted);
1525 }
1526 if(const auto union_construction = expr_try_dynamic_cast<union_exprt>(expr))
1527 {
1528 return convert_expr_to_smt(*union_construction, converted);
1529 }
1530 if(const auto constant_literal = expr_try_dynamic_cast<constant_exprt>(expr))
1531 {
1532 return convert_expr_to_smt(*constant_literal);
1533 }
1534 if(
1535 const auto concatenation = expr_try_dynamic_cast<concatenation_exprt>(expr))
1536 {
1537 return convert_expr_to_smt(*concatenation, converted);
1538 }
1539 if(const auto bitwise_and_expr = expr_try_dynamic_cast<bitand_exprt>(expr))
1540 {
1541 return convert_expr_to_smt(*bitwise_and_expr, converted);
1542 }
1543 if(const auto bitwise_or_expr = expr_try_dynamic_cast<bitor_exprt>(expr))
1544 {
1545 return convert_expr_to_smt(*bitwise_or_expr, converted);
1546 }
1548 {
1549 return convert_expr_to_smt(*bitwise_xor, converted);
1550 }
1551 if(const auto bitwise_not = expr_try_dynamic_cast<bitnot_exprt>(expr))
1552 {
1553 return convert_expr_to_smt(*bitwise_not, converted);
1554 }
1555 if(const auto unary_minus = expr_try_dynamic_cast<unary_minus_exprt>(expr))
1556 {
1557 return convert_expr_to_smt(*unary_minus, converted);
1558 }
1559 if(const auto unary_plus = expr_try_dynamic_cast<unary_plus_exprt>(expr))
1560 {
1561 return convert_expr_to_smt(*unary_plus, converted);
1562 }
1563 if(const auto is_negative = expr_try_dynamic_cast<sign_exprt>(expr))
1564 {
1565 return convert_expr_to_smt(*is_negative, converted);
1566 }
1567 if(const auto if_expression = expr_try_dynamic_cast<if_exprt>(expr))
1568 {
1569 return convert_expr_to_smt(*if_expression, converted);
1570 }
1571 if(const auto and_expression = expr_try_dynamic_cast<and_exprt>(expr))
1572 {
1573 return convert_expr_to_smt(*and_expression, converted);
1574 }
1575 if(const auto or_expression = expr_try_dynamic_cast<or_exprt>(expr))
1576 {
1577 return convert_expr_to_smt(*or_expression, converted);
1578 }
1579 if(const auto xor_expression = expr_try_dynamic_cast<xor_exprt>(expr))
1580 {
1581 return convert_expr_to_smt(*xor_expression, converted);
1582 }
1583 if(const auto implies = expr_try_dynamic_cast<implies_exprt>(expr))
1584 {
1585 return convert_expr_to_smt(*implies, converted);
1586 }
1587 if(const auto logical_not = expr_try_dynamic_cast<not_exprt>(expr))
1588 {
1589 return convert_expr_to_smt(*logical_not, converted);
1590 }
1591 if(const auto equal = expr_try_dynamic_cast<equal_exprt>(expr))
1592 {
1593 return convert_expr_to_smt(*equal, converted);
1594 }
1595 if(const auto not_equal = expr_try_dynamic_cast<notequal_exprt>(expr))
1596 {
1597 return convert_expr_to_smt(*not_equal, converted);
1598 }
1599 if(
1600 const auto float_equal =
1602 {
1603 return convert_expr_to_smt(*float_equal, converted);
1604 }
1605 if(
1606 const auto float_not_equal =
1608 {
1609 return convert_expr_to_smt(*float_not_equal, converted);
1610 }
1611 if(
1612 const auto converted_relational =
1613 try_relational_conversion(expr, converted))
1614 {
1615 return *converted_relational;
1616 }
1617 if(const auto plus = expr_try_dynamic_cast<plus_exprt>(expr))
1618 {
1619 return convert_expr_to_smt(*plus, converted, pointer_sizes);
1620 }
1621 if(const auto minus = expr_try_dynamic_cast<minus_exprt>(expr))
1622 {
1623 return convert_expr_to_smt(*minus, converted, pointer_sizes);
1624 }
1625 if(const auto divide = expr_try_dynamic_cast<div_exprt>(expr))
1626 {
1627 return convert_expr_to_smt(*divide, converted);
1628 }
1629 if(
1630 const auto float_operation =
1632 {
1633 return convert_expr_to_smt(*float_operation, converted);
1634 }
1635 if(const auto truncation_modulo = expr_try_dynamic_cast<mod_exprt>(expr))
1636 {
1637 return convert_expr_to_smt(*truncation_modulo, converted);
1638 }
1639 if(
1640 const auto euclidean_modulo =
1642 {
1643 return convert_expr_to_smt(*euclidean_modulo, converted);
1644 }
1645 if(const auto multiply = expr_try_dynamic_cast<mult_exprt>(expr))
1646 {
1647 return convert_expr_to_smt(*multiply, converted);
1648 }
1649#if 0
1650 else if(expr.id() == ID_floatbv_rem)
1651 {
1652 convert_floatbv_rem(to_binary_expr(expr));
1653 }
1654#endif
1655 if(const auto address_of = expr_try_dynamic_cast<address_of_exprt>(expr))
1656 {
1657 return convert_expr_to_smt(*address_of, converted, object_map);
1658 }
1659 if(const auto array_of = expr_try_dynamic_cast<array_of_exprt>(expr))
1660 {
1661 return convert_expr_to_smt(*array_of, converted);
1662 }
1663 if(
1664 const auto array_comprehension =
1666 {
1667 return convert_expr_to_smt(*array_comprehension, converted);
1668 }
1669 if(const auto index = expr_try_dynamic_cast<index_exprt>(expr))
1670 {
1671 return convert_expr_to_smt(*index, converted);
1672 }
1673 if(const auto shift = expr_try_dynamic_cast<shift_exprt>(expr))
1674 {
1675 return convert_expr_to_smt(*shift, converted);
1676 }
1677 if(const auto with = expr_try_dynamic_cast<with_exprt>(expr))
1678 {
1679 return convert_expr_to_smt(*with, converted);
1680 }
1681 if(const auto update = expr_try_dynamic_cast<update_exprt>(expr))
1682 {
1683 return convert_expr_to_smt(*update, converted);
1684 }
1685 if(const auto member_extraction = expr_try_dynamic_cast<member_exprt>(expr))
1686 {
1687 return convert_expr_to_smt(*member_extraction, converted);
1688 }
1689 else if(
1690 const auto pointer_offset =
1692 {
1693 return convert_expr_to_smt(*pointer_offset, converted);
1694 }
1695 else if(
1696 const auto pointer_object =
1698 {
1699 return convert_expr_to_smt(*pointer_object, converted);
1700 }
1701 if(
1702 const auto is_dynamic_object =
1704 {
1705 return convert_expr_to_smt(
1706 *is_dynamic_object, converted, apply_is_dynamic_object);
1707 }
1708 if(
1709 const auto is_invalid_pointer =
1711 {
1712 return convert_expr_to_smt(*is_invalid_pointer, object_map, converted);
1713 }
1714 if(const auto string_constant = expr_try_dynamic_cast<string_constantt>(expr))
1715 {
1716 return convert_expr_to_smt(*string_constant, converted);
1717 }
1718 if(const auto extract_bit = expr_try_dynamic_cast<extractbit_exprt>(expr))
1719 {
1720 return convert_expr_to_smt(*extract_bit, converted);
1721 }
1722 if(const auto extract_bits = expr_try_dynamic_cast<extractbits_exprt>(expr))
1723 {
1724 return convert_expr_to_smt(*extract_bits, converted);
1725 }
1726 if(const auto replication = expr_try_dynamic_cast<replication_exprt>(expr))
1727 {
1728 return convert_expr_to_smt(*replication, converted);
1729 }
1730 if(
1731 const auto byte_extraction =
1733 {
1734 return convert_expr_to_smt(*byte_extraction, converted);
1735 }
1736 if(const auto byte_update = expr_try_dynamic_cast<byte_update_exprt>(expr))
1737 {
1738 return convert_expr_to_smt(*byte_update, converted);
1739 }
1740 if(const auto absolute_value_of = expr_try_dynamic_cast<abs_exprt>(expr))
1741 {
1742 return convert_expr_to_smt(*absolute_value_of, converted);
1743 }
1744 if(const auto is_nan_expr = expr_try_dynamic_cast<isnan_exprt>(expr))
1745 {
1746 return convert_expr_to_smt(*is_nan_expr, converted);
1747 }
1748 if(const auto is_finite_expr = expr_try_dynamic_cast<isfinite_exprt>(expr))
1749 {
1750 return convert_expr_to_smt(*is_finite_expr, converted);
1751 }
1752 if(const auto is_infinite_expr = expr_try_dynamic_cast<isinf_exprt>(expr))
1753 {
1754 return convert_expr_to_smt(*is_infinite_expr, converted);
1755 }
1756 if(const auto is_normal_expr = expr_try_dynamic_cast<isnormal_exprt>(expr))
1757 {
1758 return convert_expr_to_smt(*is_normal_expr, converted);
1759 }
1760 if(
1761 const auto plus_overflow = expr_try_dynamic_cast<plus_overflow_exprt>(expr))
1762 {
1763 return convert_expr_to_smt(*plus_overflow, converted);
1764 }
1765 if(
1766 const auto minus_overflow =
1768 {
1769 return convert_expr_to_smt(*minus_overflow, converted);
1770 }
1771 if(
1772 const auto mult_overflow = expr_try_dynamic_cast<mult_overflow_exprt>(expr))
1773 {
1774 return convert_expr_to_smt(*mult_overflow, converted);
1775 }
1776 if(const auto shl_overflow = expr_try_dynamic_cast<shl_overflow_exprt>(expr))
1777 {
1778 return convert_expr_to_smt(*shl_overflow, converted);
1779 }
1780 if(const auto array_construction = expr_try_dynamic_cast<array_exprt>(expr))
1781 {
1782 return convert_expr_to_smt(*array_construction, converted);
1783 }
1784 if(const auto literal = expr_try_dynamic_cast<literal_exprt>(expr))
1785 {
1786 return convert_expr_to_smt(*literal, converted);
1787 }
1788 if(const auto for_all = expr_try_dynamic_cast<forall_exprt>(expr))
1789 {
1790 return convert_expr_to_smt(*for_all, converted);
1791 }
1792 if(const auto exists = expr_try_dynamic_cast<exists_exprt>(expr))
1793 {
1794 return convert_expr_to_smt(*exists, converted);
1795 }
1796 if(const auto vector = expr_try_dynamic_cast<vector_exprt>(expr))
1797 {
1798 return convert_expr_to_smt(*vector, converted);
1799 }
1801 {
1802 return convert_expr_to_smt(*object_size, converted, call_object_size);
1803 }
1804 if(const auto let = expr_try_dynamic_cast<let_exprt>(expr))
1805 {
1806 return convert_expr_to_smt(*let, converted);
1807 }
1808 INVARIANT(
1809 expr.id() != ID_constraint_select_one,
1810 "constraint_select_one is not expected in smt conversion: " +
1811 expr.pretty());
1812 if(const auto byte_swap = expr_try_dynamic_cast<bswap_exprt>(expr))
1813 {
1814 return convert_expr_to_smt(*byte_swap, converted);
1815 }
1816 if(const auto population_count = expr_try_dynamic_cast<popcount_exprt>(expr))
1817 {
1818 return convert_expr_to_smt(*population_count, converted);
1819 }
1820 if(
1821 const auto count_leading_zeros =
1823 {
1824 return convert_expr_to_smt(*count_leading_zeros, converted);
1825 }
1826 if(
1827 const auto count_trailing_zeros =
1829 {
1830 return convert_expr_to_smt(*count_trailing_zeros, converted);
1831 }
1832 if(const auto zero_extend = expr_try_dynamic_cast<zero_extend_exprt>(expr))
1833 {
1834 return convert_expr_to_smt(*zero_extend, converted);
1835 }
1836 if(
1837 const auto prophecy_r_or_w_ok =
1839 {
1840 return convert_expr_to_smt(*prophecy_r_or_w_ok, converted);
1841 }
1842 if(
1843 const auto prophecy_pointer_in_range =
1845 {
1846 return convert_expr_to_smt(*prophecy_pointer_in_range, converted);
1847 }
1848
1850 "Generation of SMT formula for unknown kind of expression: " +
1851 expr.pretty());
1852}
1853
1854#ifndef CPROVER_INVARIANT_DO_NOT_CHECK
1855template <typename functiont>
1868
1869template <typename functiont>
1871{
1872 return at_scope_exitt<functiont>(exit_function);
1873}
1874#endif
1875
1877{
1878 expr.visit_pre([](exprt &expr) {
1879 const auto address_of_expr = expr_try_dynamic_cast<address_of_exprt>(expr);
1880 if(!address_of_expr)
1881 return;
1882 const auto array_index_expr =
1883 expr_try_dynamic_cast<index_exprt>(address_of_expr->object());
1884 if(!array_index_expr)
1885 return;
1886 expr = plus_exprt{
1888 array_index_expr->array(),
1889 type_checked_cast<pointer_typet>(address_of_expr->type())},
1890 array_index_expr->index()};
1891 });
1892 return expr;
1893}
1894
1899 const exprt &_expr,
1900 std::function<bool(const exprt &)> filter,
1901 std::function<void(const exprt &)> visitor)
1902{
1903 struct stack_entryt
1904 {
1905 const exprt *e;
1906 bool operands_pushed;
1907 explicit stack_entryt(const exprt *_e) : e(_e), operands_pushed(false)
1908 {
1909 }
1910 };
1911
1912 std::stack<stack_entryt> stack;
1913
1914 stack.emplace(&_expr);
1915
1916 while(!stack.empty())
1917 {
1918 auto &top = stack.top();
1919 if(top.operands_pushed)
1920 {
1921 visitor(*top.e);
1922 stack.pop();
1923 }
1924 else
1925 {
1926 // do modification of 'top' before pushing in case 'top' isn't stable
1927 top.operands_pushed = true;
1928 if(filter(*top.e))
1929 for(auto &op : top.e->operands())
1930 stack.emplace(&op);
1931 }
1932 }
1933}
1934
1936 const exprt &expr,
1937 const smt_object_mapt &object_map,
1938 const type_size_mapt &pointer_sizes,
1940 const smt_is_dynamic_objectt::make_applicationt &is_dynamic_object)
1941{
1942#ifndef CPROVER_INVARIANT_DO_NOT_CHECK
1943 static bool in_conversion = false;
1944 INVARIANT(
1945 !in_conversion,
1946 "Conversion of expr to smt should be non-recursive. "
1947 "Re-entrance found in conversion of " +
1948 expr.pretty(1, 0));
1949 in_conversion = true;
1950 const auto end_conversion = at_scope_exit([&]() { in_conversion = false; });
1951#endif
1952 sub_expression_mapt sub_expression_map;
1953 const auto lowered_expr = lower_address_of_array_index(expr);
1955 lowered_expr,
1956 [](const exprt &expr) {
1957 // Code values inside "address of" expressions do not need to be converted
1958 // as the "address of" conversion only depends on the object identifier.
1959 // Avoiding the conversion side steps a need to convert arbitrary code to
1960 // SMT terms.
1961 const auto address_of = expr_try_dynamic_cast<address_of_exprt>(expr);
1962 if(!address_of)
1963 return true;
1964 return !can_cast_type<code_typet>(address_of->object().type());
1965 },
1966 [&](const exprt &expr) {
1967 const auto find_result = sub_expression_map.find(expr);
1968 if(find_result != sub_expression_map.cend())
1969 return;
1971 expr,
1972 sub_expression_map,
1973 object_map,
1974 pointer_sizes,
1976 is_dynamic_object);
1977 sub_expression_map.emplace_hint(find_result, expr, std::move(term));
1978 });
1979 return std::move(sub_expression_map.at(lowered_expr));
1980}
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:3548
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:3122
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:3336
Extract member of struct or union.
Definition std_expr.h:2976
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:2787
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 & 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