cprover
Loading...
Searching...
No Matches
convert_expr_to_smt.cpp
Go to the documentation of this file.
1// Author: Diffblue Ltd.
2
4
8#include <util/arith_tools.h>
10#include <util/byte_operators.h>
11#include <util/expr.h>
12#include <util/expr_cast.h>
13#include <util/floatbv_expr.h>
15#include <util/pointer_expr.h>
17#include <util/range.h>
18#include <util/std_expr.h>
20
21#include <functional>
22#include <numeric>
23
25{
26 return smt_bool_sortt{};
27}
28
33
35{
36 if(const auto bool_type = type_try_dynamic_cast<bool_typet>(type))
37 {
39 }
41 {
43 }
44 UNIMPLEMENTED_FEATURE("Generation of SMT formula for type: " + type.pretty());
45}
46
47static smt_termt convert_expr_to_smt(const symbol_exprt &symbol_expr)
48{
49 return smt_identifier_termt{symbol_expr.get_identifier(),
50 convert_type_to_smt_sort(symbol_expr.type())};
51}
52
54{
56 "Generation of SMT formula for nondet symbol expression: " +
57 nondet_symbol.pretty());
58}
59
61{
63 "Generation of SMT formula for type cast expression: " + cast.pretty());
64}
65
67{
69 "Generation of SMT formula for floating point type cast expression: " +
70 float_cast.pretty());
71}
72
74{
76 "Generation of SMT formula for struct construction expression: " +
77 struct_construction.pretty());
78}
79
81{
83 "Generation of SMT formula for union construction expression: " +
84 union_construction.pretty());
85}
86
88{
91
93 : member_input{input}
94 {
95 }
96
97 void visit(const smt_bool_sortt &) override
98 {
100 }
101
103 {
104 const auto &width = bit_vector_sort.bit_width();
105 // We get the value using a non-signed interpretation, as smt bit vector
106 // terms do not carry signedness.
107 const auto value = bvrep2integer(member_input.get_value(), width, false);
109 }
110};
111
113{
114 const auto sort = convert_type_to_smt_sort(constant_literal.type());
116 sort.accept(converter);
117 return *converter.result;
118}
119
121{
123 "Generation of SMT formula for concatenation expression: " +
124 concatenation.pretty());
125}
126
128{
130 "Generation of SMT formula for bitwise and expression: " +
131 bitwise_and_expr.pretty());
132}
133
135{
137 "Generation of SMT formula for bitwise or expression: " +
138 bitwise_or_expr.pretty());
139}
140
142{
144 "Generation of SMT formula for bitwise xor expression: " +
145 bitwise_xor.pretty());
146}
147
149{
151 "Generation of SMT formula for bitwise not expression: " +
152 bitwise_not.pretty());
153}
154
156{
157 const bool operand_is_bitvector =
160 {
162 convert_expr_to_smt(unary_minus.op()));
163 }
164 else
165 {
167 "Generation of SMT formula for unary minus expression: " +
168 unary_minus.pretty());
169 }
170}
171
173{
175 "Generation of SMT formula for unary plus expression: " +
176 unary_plus.pretty());
177}
178
179static smt_termt convert_expr_to_smt(const sign_exprt &is_negative)
180{
182 "Generation of SMT formula for \"is negative\" expression: " +
183 is_negative.pretty());
184}
185
193
205template <typename factoryt>
207 const multi_ary_exprt &expr,
208 const factoryt &factory)
209{
210 PRECONDITION(expr.operands().size() >= 2);
211 const auto operand_terms =
212 make_range(expr.operands()).map([](const exprt &expr) {
213 return convert_expr_to_smt(expr);
214 });
215 return std::accumulate(
216 ++operand_terms.begin(),
217 operand_terms.end(),
218 *operand_terms.begin(),
219 factory);
220}
221
227
233
239
241{
243 convert_expr_to_smt(implies.op0()), convert_expr_to_smt(implies.op1()));
244}
245
246static smt_termt convert_expr_to_smt(const not_exprt &logical_not)
247{
249}
250
252{
255}
256
258{
260 convert_expr_to_smt(not_equal.op0()), convert_expr_to_smt(not_equal.op1()));
261}
262
264{
266 "Generation of SMT formula for floating point equality expression: " +
267 float_equal.pretty());
268}
269
270static smt_termt
272{
274 "Generation of SMT formula for floating point not equal expression: " +
275 float_not_equal.pretty());
276}
277
278template <typename unsigned_factory_typet, typename signed_factory_typet>
283{
284 PRECONDITION(binary_relation.lhs().type() == binary_relation.rhs().type());
285 const auto lhs = convert_expr_to_smt(binary_relation.lhs());
286 const auto rhs = convert_expr_to_smt(binary_relation.rhs());
287 const typet operand_type = binary_relation.lhs().type();
288 if(lhs.get_sort().cast<smt_bit_vector_sortt>())
289 {
291 return unsigned_factory(lhs, rhs);
293 return signed_factory(lhs, rhs);
294 }
296 "Generation of SMT formula for relational expression: " +
297 binary_relation.pretty());
298}
299
336
338{
339 if(std::all_of(
340 plus.operands().cbegin(), plus.operands().cend(), [](exprt operand) {
341 return can_cast_type<integer_bitvector_typet>(operand.type());
342 }))
343 {
346 }
347 else
348 {
350 "Generation of SMT formula for plus expression: " + plus.pretty());
351 }
352}
353
355{
356 const bool both_operands_bitvector =
359
361 {
364 }
365 else
366 {
368 "Generation of SMT formula for minus expression: " + minus.pretty());
369 }
370}
371
373{
374 const bool both_operands_bitvector =
377
378 const bool both_operands_unsigned =
381
383 {
385 {
387 convert_expr_to_smt(divide.lhs()), convert_expr_to_smt(divide.rhs()));
388 }
389 else
390 {
392 convert_expr_to_smt(divide.lhs()), convert_expr_to_smt(divide.rhs()));
393 }
394 }
395 else
396 {
398 "Generation of SMT formula for divide expression: " + divide.pretty());
399 }
400}
401
403{
404 // This case includes the floating point plus, minus, division and
405 // multiplication operations.
407 "Generation of SMT formula for floating point operation expression: " +
408 float_operation.pretty());
409}
410
412{
413 const bool both_operands_bitvector =
416
417 const bool both_operands_unsigned =
420
422 {
424 {
428 }
429 else
430 {
434 }
435 }
436 else
437 {
439 "Generation of SMT formula for remainder (modulus) expression: " +
440 truncation_modulo.pretty());
441 }
442}
443
444static smt_termt
446{
448 "Generation of SMT formula for euclidean modulo expression: " +
449 euclidean_modulo.pretty());
450}
451
453{
454 if(std::all_of(
455 multiply.operands().cbegin(),
456 multiply.operands().cend(),
457 [](exprt operand) {
458 return can_cast_type<integer_bitvector_typet>(operand.type());
459 }))
460 {
463 }
464 else
465 {
467 "Generation of SMT formula for multiply expression: " +
468 multiply.pretty());
469 }
470}
471
473{
475 "Generation of SMT formula for address of expression: " +
476 address_of.pretty());
477}
478
480{
482 "Generation of SMT formula for array of expression: " + array_of.pretty());
483}
484
485static smt_termt
487{
489 "Generation of SMT formula for array comprehension expression: " +
490 array_comprehension.pretty());
491}
492
494{
496 "Generation of SMT formula for index expression: " + index.pretty());
497}
498
500{
501 // TODO: split into functions for separate types of shift including rotate.
503 "Generation of SMT formula for shift expression: " + shift.pretty());
504}
505
507{
509 "Generation of SMT formula for with expression: " + with.pretty());
510}
511
513{
515 "Generation of SMT formula for update expression: " + update.pretty());
516}
517
519{
521 "Generation of SMT formula for member extraction expression: " +
522 member_extraction.pretty());
523}
524
525static smt_termt
527{
529 "Generation of SMT formula for is dynamic object expression: " +
530 is_dynamic_object.pretty());
531}
532
533static smt_termt
535{
537 "Generation of SMT formula for is invalid pointer expression: " +
538 is_invalid_pointer.pretty());
539}
540
542{
544 "Generation of SMT formula for is invalid pointer expression: " +
545 is_invalid_pointer.pretty());
546}
547
549{
551 "Generation of SMT formula for extract bit expression: " +
552 extract_bit.pretty());
553}
554
556{
558 "Generation of SMT formula for extract bits expression: " +
559 extract_bits.pretty());
560}
561
563{
565 "Generation of SMT formula for bit vector replication expression: " +
566 replication.pretty());
567}
568
570{
572 "Generation of SMT formula for byte extract expression: " +
573 byte_extraction.pretty());
574}
575
577{
579 "Generation of SMT formula for byte update expression: " +
580 byte_update.pretty());
581}
582
584{
586 "Generation of SMT formula for absolute value of expression: " +
587 absolute_value_of.pretty());
588}
589
591{
593 "Generation of SMT formula for is not a number expression: " +
594 is_nan_expr.pretty());
595}
596
598{
600 "Generation of SMT formula for is finite expression: " +
601 is_finite_expr.pretty());
602}
603
605{
607 "Generation of SMT formula for is infinite expression: " +
608 is_infinite_expr.pretty());
609}
610
612{
614 "Generation of SMT formula for is infinite expression: " +
615 is_normal_expr.pretty());
616}
617
619{
621 "Generation of SMT formula for array construction expression: " +
622 array_construction.pretty());
623}
624
626{
628 "Generation of SMT formula for literal expression: " + literal.pretty());
629}
630
632{
634 "Generation of SMT formula for for all expression: " + for_all.pretty());
635}
636
638{
640 "Generation of SMT formula for exists expression: " + exists.pretty());
641}
642
644{
646 "Generation of SMT formula for vector expression: " + vector.pretty());
647}
648
650{
652 "Generation of SMT formula for byte swap expression: " +
653 byte_swap.pretty());
654}
655
657{
659 "Generation of SMT formula for population count expression: " +
660 population_count.pretty());
661}
662
663static smt_termt
665{
667 "Generation of SMT formula for count leading zeros expression: " +
668 count_leading_zeros.pretty());
669}
670
671static smt_termt
673{
675 "Generation of SMT formula for byte swap expression: " +
676 count_trailing_zeros.pretty());
677}
678
680{
681 if(const auto symbol = expr_try_dynamic_cast<symbol_exprt>(expr))
682 {
683 return convert_expr_to_smt(*symbol);
684 }
686 {
688 }
689 if(const auto cast = expr_try_dynamic_cast<typecast_exprt>(expr))
690 {
691 return convert_expr_to_smt(*cast);
692 }
693 if(
695 {
697 }
699 {
701 }
703 {
705 }
707 {
709 }
710 if(
712 {
714 }
716 {
718 }
720 {
722 }
724 {
726 }
727 if(const auto bitwise_not = expr_try_dynamic_cast<bitnot_exprt>(expr))
728 {
729 return convert_expr_to_smt(*bitwise_not);
730 }
731 if(const auto unary_minus = expr_try_dynamic_cast<unary_minus_exprt>(expr))
732 {
733 return convert_expr_to_smt(*unary_minus);
734 }
735 if(const auto unary_plus = expr_try_dynamic_cast<unary_plus_exprt>(expr))
736 {
737 return convert_expr_to_smt(*unary_plus);
738 }
739 if(const auto is_negative = expr_try_dynamic_cast<sign_exprt>(expr))
740 {
741 return convert_expr_to_smt(*is_negative);
742 }
744 {
746 }
748 {
750 }
752 {
754 }
756 {
758 }
759 if(const auto implies = expr_try_dynamic_cast<implies_exprt>(expr))
760 {
761 return convert_expr_to_smt(*implies);
762 }
763 if(const auto logical_not = expr_try_dynamic_cast<not_exprt>(expr))
764 {
765 return convert_expr_to_smt(*logical_not);
766 }
767 if(const auto equal = expr_try_dynamic_cast<equal_exprt>(expr))
768 {
769 return convert_expr_to_smt(*equal);
770 }
771 if(const auto not_equal = expr_try_dynamic_cast<notequal_exprt>(expr))
772 {
773 return convert_expr_to_smt(*not_equal);
774 }
775 if(
776 const auto float_equal =
778 {
780 }
781 if(
782 const auto float_not_equal =
784 {
786 }
788 {
789 return *converted_relational;
790 }
791 if(const auto plus = expr_try_dynamic_cast<plus_exprt>(expr))
792 {
793 return convert_expr_to_smt(*plus);
794 }
795 if(const auto minus = expr_try_dynamic_cast<minus_exprt>(expr))
796 {
797 return convert_expr_to_smt(*minus);
798 }
799 if(const auto divide = expr_try_dynamic_cast<div_exprt>(expr))
800 {
801 return convert_expr_to_smt(*divide);
802 }
803 if(
804 const auto float_operation =
806 {
808 }
810 {
812 }
813 if(
814 const auto euclidean_modulo =
816 {
818 }
819 if(const auto multiply = expr_try_dynamic_cast<mult_exprt>(expr))
820 {
821 return convert_expr_to_smt(*multiply);
822 }
823#if 0
824 else if(expr.id() == ID_floatbv_rem)
825 {
826 convert_floatbv_rem(to_binary_expr(expr));
827 }
828#endif
830 {
832 }
834 {
836 }
837 if(
838 const auto array_comprehension =
840 {
842 }
843 if(const auto index = expr_try_dynamic_cast<index_exprt>(expr))
844 {
845 return convert_expr_to_smt(*index);
846 }
847 if(const auto shift = expr_try_dynamic_cast<shift_exprt>(expr))
848 {
849 return convert_expr_to_smt(*shift);
850 }
851 if(const auto with = expr_try_dynamic_cast<with_exprt>(expr))
852 {
853 return convert_expr_to_smt(*with);
854 }
855 if(const auto update = expr_try_dynamic_cast<update_exprt>(expr))
856 {
857 return convert_expr_to_smt(*update);
858 }
860 {
862 }
863#if 0
864 else if(expr.id()==ID_pointer_offset)
865 {
866 }
867 else if(expr.id()==ID_pointer_object)
868 {
869 }
870#endif
871 if(
872 const auto is_dynamic_object =
874 {
875 return convert_expr_to_smt(*is_dynamic_object);
876 }
877 if(
878 const auto is_invalid_pointer =
880 {
882 }
884 {
886 }
888 {
890 }
892 {
894 }
896 {
898 }
899 if(
900 const auto byte_extraction =
902 {
904 }
906 {
908 }
910 {
912 }
914 {
916 }
918 {
920 }
922 {
924 }
926 {
928 }
930 {
932 }
933 if(const auto literal = expr_try_dynamic_cast<literal_exprt>(expr))
934 {
936 }
937 if(const auto for_all = expr_try_dynamic_cast<forall_exprt>(expr))
938 {
940 }
941 if(const auto exists = expr_try_dynamic_cast<exists_exprt>(expr))
942 {
944 }
945 if(const auto vector = expr_try_dynamic_cast<vector_exprt>(expr))
946 {
947 return convert_expr_to_smt(*vector);
948 }
949#if 0
950 else if(expr.id()==ID_object_size)
951 {
952 out << "|" << object_sizes[expr] << "|";
953 }
954#endif
955 if(const auto let = expr_try_dynamic_cast<let_exprt>(expr))
956 {
957 return convert_expr_to_smt(*let);
958 }
959 INVARIANT(
961 "constraint_select_one is not expected in smt conversion: " +
962 expr.pretty());
963 if(const auto byte_swap = expr_try_dynamic_cast<bswap_exprt>(expr))
964 {
966 }
968 {
970 }
971 if(
972 const auto count_leading_zeros =
974 {
976 }
977 if(
978 const auto count_trailing_zeros =
980 {
982 }
983
985 "Generation of SMT formula for unknown kind of expression: " +
986 expr.pretty());
987}
mp_integer bvrep2integer(const irep_idt &src, std::size_t width, bool is_signed)
convert a bit-vector representation (possibly signed) to integer
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.
Absolute value.
Definition std_expr.h:346
Operator to return the address of an object.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
Boolean AND.
Definition std_expr.h:1974
Expression to define a mapping from an argument (index) to elements.
Definition std_expr.h:3182
Array constructor from list of elements.
Definition std_expr.h:1476
Array constructor from single element.
Definition std_expr.h:1411
exprt & lhs()
Definition std_expr.h:580
exprt & rhs()
Definition std_expr.h:590
exprt & op0()
Definition expr.h:99
exprt & op1()
Definition expr.h:102
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:674
Bit-wise AND.
Bit-wise negation of bit-vectors.
Bit-wise OR.
Base class of fixed-width bit-vector types.
Definition std_types.h:853
std::size_t get_width() const
Definition std_types.h:864
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...
Concatenation of bit-vector operands.
A constant literal expression.
Definition std_expr.h:2807
const irep_idt & get_value() const
Definition std_expr.h:2815
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:1064
Equality.
Definition std_expr.h:1225
Boute's Euclidean definition of Modulo – to match SMT-LIB2.
Definition std_expr.h:1179
An exists expression.
Base class for all expressions.
Definition expr.h:54
bool is_true() const
Return whether the expression is a constant representing true.
Definition expr.cpp:33
typet & type()
Return the type of the expression.
Definition expr.h:82
operandst & operands()
Definition expr.h:92
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:2226
Boolean implication.
Definition std_expr.h:2037
Array index operator.
Definition std_expr.h:1328
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition irep.cpp:495
const irep_idt & id() const
Definition irep.h:396
Evaluates to true if the operand is a pointer to a dynamic object.
Evaluates to true if the operand is finite.
Evaluates to true if the operand is infinite.
Evaluates to true if the operand is NaN.
Evaluates to true if the operand is a normal number.
Extract member of struct or union.
Definition std_expr.h:2667
Binary minus.
Definition std_expr.h:973
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
Definition std_expr.h:1135
Binary multiplication Associativity is not specified.
Definition std_expr.h:1019
A base class for multi-ary expressions Associativity is not specified.
Definition std_expr.h:824
Expression to hold a nondeterministic choice.
Definition std_expr.h:209
Boolean negation.
Definition std_expr.h:2181
Disequality.
Definition std_expr.h:1283
Boolean OR.
Definition std_expr.h:2082
The plus expression Associativity is not specified.
Definition std_expr.h:914
The popcount (counting the number of bits set to 1) expression.
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:506
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< 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< multiplyt > multiply
static const smt_function_application_termt::factoryt< signed_less_thant > signed_less_than
static const smt_function_application_termt::factoryt< signed_greater_thant > signed_greater_than
static const smt_function_application_termt::factoryt< negatet > negate
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< distinctt > distinct
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:81
Struct constructor from list of elements.
Definition std_expr.h:1722
Expression to hold a symbol (variable)
Definition std_expr.h:80
const irep_idt & get_identifier() const
Definition std_expr.h:109
Semantic type conversion.
Definition std_expr.h:1920
The type of an expression, extends irept.
Definition type.h:29
const exprt & op() const
Definition std_expr.h:293
The unary minus expression.
Definition std_expr.h:390
The unary plus expression.
Definition std_expr.h:439
Union constructor from single element.
Definition std_expr.h:1611
Operator to update elements in structs and arrays.
Definition std_expr.h:2496
Vector constructor from list of elements.
Definition std_expr.h:1575
Operator to update elements in structs and arrays.
Definition std_expr.h:2312
Boolean XOR.
Definition std_expr.h:2145
static optionalt< smt_termt > try_relational_conversion(const exprt &expr)
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)
static smt_termt convert_multiary_operator_to_terms(const multi_ary_exprt &expr, const factoryt &factory)
Converts operator expressions with 2 or more operands to terms expressed as binary operator applicati...
static smt_sortt convert_type_to_smt_sort(const bool_typet &type)
static smt_termt convert_expr_to_smt(const symbol_exprt &symbol_expr)
Templated functions to cast to specific exprt-derived classes.
API to expression classes for floating-point arithmetic.
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
API to expression classes for Pointers.
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:524
#define UNIMPLEMENTED_FEATURE(FEATURE)
Definition invariant.h:517
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
API to expression classes.
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition std_expr.h:627
binary_relation_exprt less_than(exprt lhs, exprt rhs)
Definition string_expr.h:48
binary_relation_exprt greater_than(exprt lhs, exprt rhs)
Definition string_expr.h:25
void visit(const smt_bit_vector_sortt &bit_vector_sort) override
const constant_exprt & member_input
void visit(const smt_bool_sortt &) override
sort_based_literal_convertert(const constant_exprt &input)