1 //== Z3ConstraintManager.cpp --------------------------------*- C++ -*--==//
3 // The LLVM Compiler Infrastructure
5 // This file is distributed under the University of Illinois Open Source
6 // License. See LICENSE.TXT for details.
8 //===----------------------------------------------------------------------===//
10 #include "clang/Basic/TargetInfo.h"
11 #include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h"
12 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
13 #include "clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h"
15 #include "clang/Config/config.h"
17 using namespace clang;
20 #if CLANG_ANALYZER_WITH_Z3
24 // Forward declarations
27 class ConstraintZ3 {};
28 } // end anonymous namespace
30 typedef llvm::ImmutableSet<std::pair<SymbolRef, Z3Expr>> ConstraintZ3Ty;
32 // Expansion of REGISTER_TRAIT_WITH_PROGRAMSTATE(ConstraintZ3, Z3SetPair)
36 struct ProgramStateTrait<ConstraintZ3>
37 : public ProgramStatePartialTrait<ConstraintZ3Ty> {
38 static void *GDMIndex() {
43 } // end namespace ento
44 } // end namespace clang
49 friend class Z3Context;
54 Z3Config() : Config(Z3_mk_config()) {
55 // Enable model finding
56 Z3_set_param_value(Config, "model", "true");
57 // Disable proof generation
58 Z3_set_param_value(Config, "proof", "false");
59 // Set timeout to 15000ms = 15s
60 Z3_set_param_value(Config, "timeout", "15000");
63 ~Z3Config() { Z3_del_config(Config); }
64 }; // end class Z3Config
72 Z3Context() : ZC_P(Z3_mk_context_rc(Z3Config().Config)) { ZC = ZC_P; }
79 }; // end class Z3Context
86 Z3Sort() : Sort(nullptr) {}
87 Z3Sort(Z3_sort ZS) : Sort(ZS) {
88 Z3_inc_ref(Z3Context::ZC, reinterpret_cast<Z3_ast>(Sort));
92 /// Override implicit copy constructor for correct reference counting.
93 Z3Sort(const Z3Sort &Copy) : Sort(Copy.Sort) {
94 Z3_inc_ref(Z3Context::ZC, reinterpret_cast<Z3_ast>(Sort));
97 /// Provide move constructor
98 Z3Sort(Z3Sort &&Move) : Sort(nullptr) { *this = std::move(Move); }
100 /// Provide move assignment constructor
101 Z3Sort &operator=(Z3Sort &&Move) {
104 Z3_dec_ref(Z3Context::ZC, reinterpret_cast<Z3_ast>(Sort));
113 Z3_dec_ref(Z3Context::ZC, reinterpret_cast<Z3_ast>(Sort));
116 // Return a boolean sort.
117 static Z3Sort getBoolSort() { return Z3Sort(Z3_mk_bool_sort(Z3Context::ZC)); }
119 // Return an appropriate bitvector sort for the given bitwidth.
120 static Z3Sort getBitvectorSort(unsigned BitWidth) {
121 return Z3Sort(Z3_mk_bv_sort(Z3Context::ZC, BitWidth));
124 // Return an appropriate floating-point sort for the given bitwidth.
125 static Z3Sort getFloatSort(unsigned BitWidth) {
130 llvm_unreachable("Unsupported floating-point bitwidth!");
133 Sort = Z3_mk_fpa_sort_16(Z3Context::ZC);
136 Sort = Z3_mk_fpa_sort_32(Z3Context::ZC);
139 Sort = Z3_mk_fpa_sort_64(Z3Context::ZC);
142 Sort = Z3_mk_fpa_sort_128(Z3Context::ZC);
148 // Return an appropriate sort for the given AST.
149 static Z3Sort getSort(Z3_ast AST) {
150 return Z3Sort(Z3_get_sort(Z3Context::ZC, AST));
153 Z3_sort_kind getSortKind() const {
154 return Z3_get_sort_kind(Z3Context::ZC, Sort);
157 unsigned getBitvectorSortSize() const {
158 assert(getSortKind() == Z3_BV_SORT && "Not a bitvector sort!");
159 return Z3_get_bv_sort_size(Z3Context::ZC, Sort);
162 unsigned getFloatSortSize() const {
163 assert(getSortKind() == Z3_FLOATING_POINT_SORT &&
164 "Not a floating-point sort!");
165 return Z3_fpa_get_ebits(Z3Context::ZC, Sort) +
166 Z3_fpa_get_sbits(Z3Context::ZC, Sort);
169 bool operator==(const Z3Sort &Other) const {
170 return Z3_is_eq_sort(Z3Context::ZC, Sort, Other.Sort);
173 Z3Sort &operator=(const Z3Sort &Move) {
174 Z3_inc_ref(Z3Context::ZC, reinterpret_cast<Z3_ast>(Move.Sort));
175 Z3_dec_ref(Z3Context::ZC, reinterpret_cast<Z3_ast>(Sort));
180 void print(raw_ostream &OS) const {
181 OS << Z3_sort_to_string(Z3Context::ZC, Sort);
184 LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
185 }; // end class Z3Sort
188 friend class Z3Model;
189 friend class Z3Solver;
193 Z3Expr(Z3_ast ZA) : AST(ZA) { Z3_inc_ref(Z3Context::ZC, AST); }
195 // Return an appropriate floating-point rounding mode.
196 static Z3Expr getFloatRoundingMode() {
197 // TODO: Don't assume nearest ties to even rounding mode
198 return Z3Expr(Z3_mk_fpa_rne(Z3Context::ZC));
201 // Determine whether two float semantics are equivalent
202 static bool areEquivalent(const llvm::fltSemantics &LHS,
203 const llvm::fltSemantics &RHS) {
204 return (llvm::APFloat::semanticsPrecision(LHS) ==
205 llvm::APFloat::semanticsPrecision(RHS)) &&
206 (llvm::APFloat::semanticsMinExponent(LHS) ==
207 llvm::APFloat::semanticsMinExponent(RHS)) &&
208 (llvm::APFloat::semanticsMaxExponent(LHS) ==
209 llvm::APFloat::semanticsMaxExponent(RHS)) &&
210 (llvm::APFloat::semanticsSizeInBits(LHS) ==
211 llvm::APFloat::semanticsSizeInBits(RHS));
215 /// Override implicit copy constructor for correct reference counting.
216 Z3Expr(const Z3Expr &Copy) : AST(Copy.AST) { Z3_inc_ref(Z3Context::ZC, AST); }
218 /// Provide move constructor
219 Z3Expr(Z3Expr &&Move) : AST(nullptr) { *this = std::move(Move); }
221 /// Provide move assignment constructor
222 Z3Expr &operator=(Z3Expr &&Move) {
225 Z3_dec_ref(Z3Context::ZC, AST);
234 Z3_dec_ref(Z3Context::ZC, AST);
237 /// Get the corresponding IEEE floating-point type for a given bitwidth.
238 static const llvm::fltSemantics &getFloatSemantics(unsigned BitWidth) {
241 llvm_unreachable("Unsupported floating-point semantics!");
244 return llvm::APFloat::IEEEhalf();
246 return llvm::APFloat::IEEEsingle();
248 return llvm::APFloat::IEEEdouble();
250 return llvm::APFloat::IEEEquad();
254 /// Construct a Z3Expr from a unary operator, given a Z3_context.
255 static Z3Expr fromUnOp(const UnaryOperator::Opcode Op, const Z3Expr &Exp) {
260 llvm_unreachable("Unimplemented opcode");
264 AST = Z3_mk_bvneg(Z3Context::ZC, Exp.AST);
268 AST = Z3_mk_bvnot(Z3Context::ZC, Exp.AST);
272 AST = Z3_mk_not(Z3Context::ZC, Exp.AST);
279 /// Construct a Z3Expr from a floating-point unary operator, given a
281 static Z3Expr fromFloatUnOp(const UnaryOperator::Opcode Op,
287 llvm_unreachable("Unimplemented opcode");
291 AST = Z3_mk_fpa_neg(Z3Context::ZC, Exp.AST);
295 return Z3Expr::fromUnOp(Op, Exp);
301 /// Construct a Z3Expr from a n-ary binary operator.
302 static Z3Expr fromNBinOp(const BinaryOperator::Opcode Op,
303 const std::vector<Z3_ast> &ASTs) {
308 llvm_unreachable("Unimplemented opcode");
312 AST = Z3_mk_and(Z3Context::ZC, ASTs.size(), ASTs.data());
316 AST = Z3_mk_or(Z3Context::ZC, ASTs.size(), ASTs.data());
323 /// Construct a Z3Expr from a binary operator, given a Z3_context.
324 static Z3Expr fromBinOp(const Z3Expr &LHS, const BinaryOperator::Opcode Op,
325 const Z3Expr &RHS, bool isSigned) {
328 assert(Z3Sort::getSort(LHS.AST) == Z3Sort::getSort(RHS.AST) &&
329 "AST's must have the same sort!");
333 llvm_unreachable("Unimplemented opcode");
336 // Multiplicative operators
338 AST = Z3_mk_bvmul(Z3Context::ZC, LHS.AST, RHS.AST);
341 AST = isSigned ? Z3_mk_bvsdiv(Z3Context::ZC, LHS.AST, RHS.AST)
342 : Z3_mk_bvudiv(Z3Context::ZC, LHS.AST, RHS.AST);
345 AST = isSigned ? Z3_mk_bvsrem(Z3Context::ZC, LHS.AST, RHS.AST)
346 : Z3_mk_bvurem(Z3Context::ZC, LHS.AST, RHS.AST);
349 // Additive operators
351 AST = Z3_mk_bvadd(Z3Context::ZC, LHS.AST, RHS.AST);
354 AST = Z3_mk_bvsub(Z3Context::ZC, LHS.AST, RHS.AST);
357 // Bitwise shift operators
359 AST = Z3_mk_bvshl(Z3Context::ZC, LHS.AST, RHS.AST);
362 AST = isSigned ? Z3_mk_bvashr(Z3Context::ZC, LHS.AST, RHS.AST)
363 : Z3_mk_bvlshr(Z3Context::ZC, LHS.AST, RHS.AST);
366 // Relational operators
368 AST = isSigned ? Z3_mk_bvslt(Z3Context::ZC, LHS.AST, RHS.AST)
369 : Z3_mk_bvult(Z3Context::ZC, LHS.AST, RHS.AST);
372 AST = isSigned ? Z3_mk_bvsgt(Z3Context::ZC, LHS.AST, RHS.AST)
373 : Z3_mk_bvugt(Z3Context::ZC, LHS.AST, RHS.AST);
376 AST = isSigned ? Z3_mk_bvsle(Z3Context::ZC, LHS.AST, RHS.AST)
377 : Z3_mk_bvule(Z3Context::ZC, LHS.AST, RHS.AST);
380 AST = isSigned ? Z3_mk_bvsge(Z3Context::ZC, LHS.AST, RHS.AST)
381 : Z3_mk_bvuge(Z3Context::ZC, LHS.AST, RHS.AST);
384 // Equality operators
386 AST = Z3_mk_eq(Z3Context::ZC, LHS.AST, RHS.AST);
389 return Z3Expr::fromUnOp(UO_LNot,
390 Z3Expr::fromBinOp(LHS, BO_EQ, RHS, isSigned));
395 AST = Z3_mk_bvand(Z3Context::ZC, LHS.AST, RHS.AST);
398 AST = Z3_mk_bvxor(Z3Context::ZC, LHS.AST, RHS.AST);
401 AST = Z3_mk_bvor(Z3Context::ZC, LHS.AST, RHS.AST);
407 std::vector<Z3_ast> Args = {LHS.AST, RHS.AST};
408 return Z3Expr::fromNBinOp(Op, Args);
415 /// Construct a Z3Expr from a special floating-point binary operator, given
417 static Z3Expr fromFloatSpecialBinOp(const Z3Expr &LHS,
418 const BinaryOperator::Opcode Op,
419 const llvm::APFloat::fltCategory &RHS) {
424 llvm_unreachable("Unimplemented opcode");
427 // Equality operators
430 case llvm::APFloat::fcInfinity:
431 AST = Z3_mk_fpa_is_infinite(Z3Context::ZC, LHS.AST);
433 case llvm::APFloat::fcNaN:
434 AST = Z3_mk_fpa_is_nan(Z3Context::ZC, LHS.AST);
436 case llvm::APFloat::fcNormal:
437 AST = Z3_mk_fpa_is_normal(Z3Context::ZC, LHS.AST);
439 case llvm::APFloat::fcZero:
440 AST = Z3_mk_fpa_is_zero(Z3Context::ZC, LHS.AST);
445 return Z3Expr::fromFloatUnOp(
446 UO_LNot, Z3Expr::fromFloatSpecialBinOp(LHS, BO_EQ, RHS));
453 /// Construct a Z3Expr from a floating-point binary operator, given a
455 static Z3Expr fromFloatBinOp(const Z3Expr &LHS,
456 const BinaryOperator::Opcode Op,
460 assert(Z3Sort::getSort(LHS.AST) == Z3Sort::getSort(RHS.AST) &&
461 "AST's must have the same sort!");
465 llvm_unreachable("Unimplemented opcode");
468 // Multiplicative operators
470 Z3Expr RoundingMode = Z3Expr::getFloatRoundingMode();
471 AST = Z3_mk_fpa_mul(Z3Context::ZC, RoundingMode.AST, LHS.AST, RHS.AST);
475 Z3Expr RoundingMode = Z3Expr::getFloatRoundingMode();
476 AST = Z3_mk_fpa_div(Z3Context::ZC, RoundingMode.AST, LHS.AST, RHS.AST);
480 AST = Z3_mk_fpa_rem(Z3Context::ZC, LHS.AST, RHS.AST);
483 // Additive operators
485 Z3Expr RoundingMode = Z3Expr::getFloatRoundingMode();
486 AST = Z3_mk_fpa_add(Z3Context::ZC, RoundingMode.AST, LHS.AST, RHS.AST);
490 Z3Expr RoundingMode = Z3Expr::getFloatRoundingMode();
491 AST = Z3_mk_fpa_sub(Z3Context::ZC, RoundingMode.AST, LHS.AST, RHS.AST);
495 // Relational operators
497 AST = Z3_mk_fpa_lt(Z3Context::ZC, LHS.AST, RHS.AST);
500 AST = Z3_mk_fpa_gt(Z3Context::ZC, LHS.AST, RHS.AST);
503 AST = Z3_mk_fpa_leq(Z3Context::ZC, LHS.AST, RHS.AST);
506 AST = Z3_mk_fpa_geq(Z3Context::ZC, LHS.AST, RHS.AST);
509 // Equality operators
511 AST = Z3_mk_fpa_eq(Z3Context::ZC, LHS.AST, RHS.AST);
514 return Z3Expr::fromFloatUnOp(UO_LNot,
515 Z3Expr::fromFloatBinOp(LHS, BO_EQ, RHS));
521 return Z3Expr::fromBinOp(LHS, Op, RHS, false);
527 /// Construct a Z3Expr from a SymbolData, given a Z3_context.
528 static Z3Expr fromData(const SymbolID ID, bool isBool, bool isFloat,
530 llvm::Twine Name = "$" + llvm::Twine(ID);
534 Sort = Z3Sort::getBoolSort();
536 Sort = Z3Sort::getFloatSort(BitWidth);
538 Sort = Z3Sort::getBitvectorSort(BitWidth);
540 Z3_symbol Symbol = Z3_mk_string_symbol(Z3Context::ZC, Name.str().c_str());
541 Z3_ast AST = Z3_mk_const(Z3Context::ZC, Symbol, Sort.Sort);
545 /// Construct a Z3Expr from a SymbolCast, given a Z3_context.
546 static Z3Expr fromCast(const Z3Expr &Exp, QualType ToTy, uint64_t ToBitWidth,
547 QualType FromTy, uint64_t FromBitWidth) {
550 if ((FromTy->isIntegralOrEnumerationType() &&
551 ToTy->isIntegralOrEnumerationType()) ||
552 (FromTy->isAnyPointerType() ^ ToTy->isAnyPointerType()) ||
553 (FromTy->isBlockPointerType() ^ ToTy->isBlockPointerType()) ||
554 (FromTy->isReferenceType() ^ ToTy->isReferenceType())) {
555 // Special case: Z3 boolean type is distinct from bitvector type, so
556 // must use if-then-else expression instead of direct cast
557 if (FromTy->isBooleanType()) {
558 assert(ToBitWidth > 0 && "BitWidth must be positive!");
559 Z3Expr Zero = Z3Expr::fromInt("0", ToBitWidth);
560 Z3Expr One = Z3Expr::fromInt("1", ToBitWidth);
561 AST = Z3_mk_ite(Z3Context::ZC, Exp.AST, One.AST, Zero.AST);
562 } else if (ToBitWidth > FromBitWidth) {
563 AST = FromTy->isSignedIntegerOrEnumerationType()
564 ? Z3_mk_sign_ext(Z3Context::ZC, ToBitWidth - FromBitWidth,
566 : Z3_mk_zero_ext(Z3Context::ZC, ToBitWidth - FromBitWidth,
568 } else if (ToBitWidth < FromBitWidth) {
569 AST = Z3_mk_extract(Z3Context::ZC, ToBitWidth - 1, 0, Exp.AST);
571 // Both are bitvectors with the same width, ignore the type cast
574 } else if (FromTy->isRealFloatingType() && ToTy->isRealFloatingType()) {
575 if (ToBitWidth != FromBitWidth) {
576 Z3Expr RoundingMode = Z3Expr::getFloatRoundingMode();
577 Z3Sort Sort = Z3Sort::getFloatSort(ToBitWidth);
578 AST = Z3_mk_fpa_to_fp_float(Z3Context::ZC, RoundingMode.AST, Exp.AST,
583 } else if (FromTy->isIntegralOrEnumerationType() &&
584 ToTy->isRealFloatingType()) {
585 Z3Expr RoundingMode = Z3Expr::getFloatRoundingMode();
586 Z3Sort Sort = Z3Sort::getFloatSort(ToBitWidth);
587 AST = FromTy->isSignedIntegerOrEnumerationType()
588 ? Z3_mk_fpa_to_fp_signed(Z3Context::ZC, RoundingMode.AST,
590 : Z3_mk_fpa_to_fp_unsigned(Z3Context::ZC, RoundingMode.AST,
592 } else if (FromTy->isRealFloatingType() &&
593 ToTy->isIntegralOrEnumerationType()) {
594 Z3Expr RoundingMode = Z3Expr::getFloatRoundingMode();
595 AST = ToTy->isSignedIntegerOrEnumerationType()
596 ? Z3_mk_fpa_to_sbv(Z3Context::ZC, RoundingMode.AST, Exp.AST,
598 : Z3_mk_fpa_to_ubv(Z3Context::ZC, RoundingMode.AST, Exp.AST,
601 llvm_unreachable("Unsupported explicit type cast!");
607 /// Construct a Z3Expr from a boolean, given a Z3_context.
608 static Z3Expr fromBoolean(const bool Bool) {
609 Z3_ast AST = Bool ? Z3_mk_true(Z3Context::ZC) : Z3_mk_false(Z3Context::ZC);
613 /// Construct a Z3Expr from a finite APFloat, given a Z3_context.
614 static Z3Expr fromAPFloat(const llvm::APFloat &Float) {
616 Z3Sort Sort = Z3Sort::getFloatSort(
617 llvm::APFloat::semanticsSizeInBits(Float.getSemantics()));
619 llvm::APSInt Int = llvm::APSInt(Float.bitcastToAPInt(), true);
620 Z3Expr Z3Int = Z3Expr::fromAPSInt(Int);
621 AST = Z3_mk_fpa_to_fp_bv(Z3Context::ZC, Z3Int.AST, Sort.Sort);
626 /// Construct a Z3Expr from an APSInt, given a Z3_context.
627 static Z3Expr fromAPSInt(const llvm::APSInt &Int) {
628 Z3Sort Sort = Z3Sort::getBitvectorSort(Int.getBitWidth());
630 Z3_mk_numeral(Z3Context::ZC, Int.toString(10).c_str(), Sort.Sort);
634 /// Construct a Z3Expr from an integer, given a Z3_context.
635 static Z3Expr fromInt(const char *Int, uint64_t BitWidth) {
636 Z3Sort Sort = Z3Sort::getBitvectorSort(BitWidth);
637 Z3_ast AST = Z3_mk_numeral(Z3Context::ZC, Int, Sort.Sort);
641 /// Construct an APFloat from a Z3Expr, given the AST representation
642 static bool toAPFloat(const Z3Sort &Sort, const Z3_ast &AST,
643 llvm::APFloat &Float, bool useSemantics = true) {
644 assert(Sort.getSortKind() == Z3_FLOATING_POINT_SORT &&
645 "Unsupported sort to floating-point!");
647 llvm::APSInt Int(Sort.getFloatSortSize(), true);
648 const llvm::fltSemantics &Semantics =
649 Z3Expr::getFloatSemantics(Sort.getFloatSortSize());
650 Z3Sort BVSort = Z3Sort::getBitvectorSort(Sort.getFloatSortSize());
651 if (!Z3Expr::toAPSInt(BVSort, AST, Int, true)) {
656 !Z3Expr::areEquivalent(Float.getSemantics(), Semantics)) {
657 assert(false && "Floating-point types don't match!");
661 Float = llvm::APFloat(Semantics, Int);
665 /// Construct an APSInt from a Z3Expr, given the AST representation
666 static bool toAPSInt(const Z3Sort &Sort, const Z3_ast &AST, llvm::APSInt &Int,
667 bool useSemantics = true) {
668 switch (Sort.getSortKind()) {
670 llvm_unreachable("Unsupported sort to integer!");
672 if (useSemantics && Int.getBitWidth() != Sort.getBitvectorSortSize()) {
673 assert(false && "Bitvector types don't match!");
678 // Force cast because Z3 defines __uint64 to be a unsigned long long
679 // type, which isn't compatible with a unsigned long type, even if they
680 // are the same size.
681 Z3_get_numeral_uint64(Z3Context::ZC, AST,
682 reinterpret_cast<__uint64 *>(&Value[0]));
683 if (Sort.getBitvectorSortSize() <= 64) {
684 Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), Value[0]), true);
685 } else if (Sort.getBitvectorSortSize() == 128) {
686 Z3Expr ASTHigh = Z3Expr(Z3_mk_extract(Z3Context::ZC, 127, 64, AST));
687 Z3_get_numeral_uint64(Z3Context::ZC, AST,
688 reinterpret_cast<__uint64 *>(&Value[1]));
689 Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), Value), true);
691 assert(false && "Bitwidth not supported!");
697 if (useSemantics && Int.getBitWidth() < 1) {
698 assert(false && "Boolean type doesn't match!");
702 llvm::APInt(Int.getBitWidth(),
703 Z3_get_bool_value(Z3Context::ZC, AST) == Z3_L_TRUE ? 1
710 void Profile(llvm::FoldingSetNodeID &ID) const {
711 ID.AddInteger(Z3_get_ast_hash(Z3Context::ZC, AST));
714 bool operator<(const Z3Expr &Other) const {
715 llvm::FoldingSetNodeID ID1, ID2;
721 /// Comparison of AST equality, not model equivalence.
722 bool operator==(const Z3Expr &Other) const {
723 assert(Z3_is_eq_sort(Z3Context::ZC, Z3_get_sort(Z3Context::ZC, AST),
724 Z3_get_sort(Z3Context::ZC, Other.AST)) &&
725 "AST's must have the same sort");
726 return Z3_is_eq_ast(Z3Context::ZC, AST, Other.AST);
729 /// Override implicit move constructor for correct reference counting.
730 Z3Expr &operator=(const Z3Expr &Move) {
731 Z3_inc_ref(Z3Context::ZC, Move.AST);
732 Z3_dec_ref(Z3Context::ZC, AST);
737 void print(raw_ostream &OS) const {
738 OS << Z3_ast_to_string(Z3Context::ZC, AST);
741 LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
742 }; // end class Z3Expr
748 Z3Model(Z3_model ZM) : Model(ZM) { Z3_model_inc_ref(Z3Context::ZC, Model); }
750 /// Override implicit copy constructor for correct reference counting.
751 Z3Model(const Z3Model &Copy) : Model(Copy.Model) {
752 Z3_model_inc_ref(Z3Context::ZC, Model);
755 /// Provide move constructor
756 Z3Model(Z3Model &&Move) : Model(nullptr) { *this = std::move(Move); }
758 /// Provide move assignment constructor
759 Z3Model &operator=(Z3Model &&Move) {
762 Z3_model_dec_ref(Z3Context::ZC, Model);
764 Move.Model = nullptr;
771 Z3_model_dec_ref(Z3Context::ZC, Model);
774 /// Given an expression, extract the value of this operand in the model.
775 bool getInterpretation(const Z3Expr &Exp, llvm::APSInt &Int) const {
777 Z3_get_app_decl(Z3Context::ZC, Z3_to_app(Z3Context::ZC, Exp.AST));
778 if (Z3_model_has_interp(Z3Context::ZC, Model, Func) != Z3_L_TRUE)
781 Z3_ast Assign = Z3_model_get_const_interp(Z3Context::ZC, Model, Func);
782 Z3Sort Sort = Z3Sort::getSort(Assign);
783 return Z3Expr::toAPSInt(Sort, Assign, Int, true);
786 /// Given an expression, extract the value of this operand in the model.
787 bool getInterpretation(const Z3Expr &Exp, llvm::APFloat &Float) const {
789 Z3_get_app_decl(Z3Context::ZC, Z3_to_app(Z3Context::ZC, Exp.AST));
790 if (Z3_model_has_interp(Z3Context::ZC, Model, Func) != Z3_L_TRUE)
793 Z3_ast Assign = Z3_model_get_const_interp(Z3Context::ZC, Model, Func);
794 Z3Sort Sort = Z3Sort::getSort(Assign);
795 return Z3Expr::toAPFloat(Sort, Assign, Float, true);
798 void print(raw_ostream &OS) const {
799 OS << Z3_model_to_string(Z3Context::ZC, Model);
802 LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
803 }; // end class Z3Model
806 friend class Z3ConstraintManager;
810 Z3Solver(Z3_solver ZS) : Solver(ZS) {
811 Z3_solver_inc_ref(Z3Context::ZC, Solver);
815 /// Override implicit copy constructor for correct reference counting.
816 Z3Solver(const Z3Solver &Copy) : Solver(Copy.Solver) {
817 Z3_solver_inc_ref(Z3Context::ZC, Solver);
820 /// Provide move constructor
821 Z3Solver(Z3Solver &&Move) : Solver(nullptr) { *this = std::move(Move); }
823 /// Provide move assignment constructor
824 Z3Solver &operator=(Z3Solver &&Move) {
827 Z3_solver_dec_ref(Z3Context::ZC, Solver);
828 Solver = Move.Solver;
829 Move.Solver = nullptr;
836 Z3_solver_dec_ref(Z3Context::ZC, Solver);
839 /// Given a constraint, add it to the solver
840 void addConstraint(const Z3Expr &Exp) {
841 Z3_solver_assert(Z3Context::ZC, Solver, Exp.AST);
844 /// Given a program state, construct the logical conjunction and add it to
846 void addStateConstraints(ProgramStateRef State) {
847 // TODO: Don't add all the constraints, only the relevant ones
848 ConstraintZ3Ty CZ = State->get<ConstraintZ3>();
849 ConstraintZ3Ty::iterator I = CZ.begin(), IE = CZ.end();
851 // Construct the logical AND of all the constraints
853 std::vector<Z3_ast> ASTs;
856 ASTs.push_back(I++->second.AST);
858 Z3Expr Conj = Z3Expr::fromNBinOp(BO_LAnd, ASTs);
863 /// Check if the constraints are satisfiable
864 Z3_lbool check() { return Z3_solver_check(Z3Context::ZC, Solver); }
866 /// Push the current solver state
867 void push() { return Z3_solver_push(Z3Context::ZC, Solver); }
869 /// Pop the previous solver state
870 void pop(unsigned NumStates = 1) {
871 assert(Z3_solver_get_num_scopes(Z3Context::ZC, Solver) >= NumStates);
872 return Z3_solver_pop(Z3Context::ZC, Solver, NumStates);
875 /// Get a model from the solver. Caller should check the model is
878 return Z3Model(Z3_solver_get_model(Z3Context::ZC, Solver));
881 /// Reset the solver and remove all constraints.
882 void reset() { Z3_solver_reset(Z3Context::ZC, Solver); }
883 }; // end class Z3Solver
885 void Z3ErrorHandler(Z3_context Context, Z3_error_code Error) {
886 llvm::report_fatal_error("Z3 error: " +
887 llvm::Twine(Z3_get_error_msg_ex(Context, Error)));
890 class Z3ConstraintManager : public SimpleConstraintManager {
892 mutable Z3Solver Solver;
895 Z3ConstraintManager(SubEngine *SE, SValBuilder &SB)
896 : SimpleConstraintManager(SE, SB),
897 Solver(Z3_mk_simple_solver(Z3Context::ZC)) {
898 Z3_set_error_handler(Z3Context::ZC, Z3ErrorHandler);
901 //===------------------------------------------------------------------===//
902 // Implementation for interface from ConstraintManager.
903 //===------------------------------------------------------------------===//
905 bool canReasonAbout(SVal X) const override;
907 ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym) override;
909 const llvm::APSInt *getSymVal(ProgramStateRef State,
910 SymbolRef Sym) const override;
912 ProgramStateRef removeDeadBindings(ProgramStateRef St,
913 SymbolReaper &SymReaper) override;
915 void print(ProgramStateRef St, raw_ostream &Out, const char *nl,
916 const char *sep) override;
918 //===------------------------------------------------------------------===//
919 // Implementation for interface from SimpleConstraintManager.
920 //===------------------------------------------------------------------===//
922 ProgramStateRef assumeSym(ProgramStateRef state, SymbolRef Sym,
923 bool Assumption) override;
925 ProgramStateRef assumeSymInclusiveRange(ProgramStateRef State, SymbolRef Sym,
926 const llvm::APSInt &From,
927 const llvm::APSInt &To,
928 bool InRange) override;
930 ProgramStateRef assumeSymUnsupported(ProgramStateRef State, SymbolRef Sym,
931 bool Assumption) override;
934 //===------------------------------------------------------------------===//
935 // Internal implementation.
936 //===------------------------------------------------------------------===//
938 // Check whether a new model is satisfiable, and update the program state.
939 ProgramStateRef assumeZ3Expr(ProgramStateRef State, SymbolRef Sym,
942 // Generate and check a Z3 model, using the given constraint.
943 Z3_lbool checkZ3Model(ProgramStateRef State, const Z3Expr &Exp) const;
945 // Generate a Z3Expr that represents the given symbolic expression.
946 // Sets the hasComparison parameter if the expression has a comparison
948 // Sets the RetTy parameter to the final return type after promotions and
950 Z3Expr getZ3Expr(SymbolRef Sym, QualType *RetTy = nullptr,
951 bool *hasComparison = nullptr) const;
953 // Generate a Z3Expr that takes the logical not of an expression.
954 Z3Expr getZ3NotExpr(const Z3Expr &Exp) const;
956 // Generate a Z3Expr that compares the expression to zero.
957 Z3Expr getZ3ZeroExpr(const Z3Expr &Exp, QualType RetTy,
958 bool Assumption) const;
960 // Recursive implementation to unpack and generate symbolic expression.
961 // Sets the hasComparison and RetTy parameters. See getZ3Expr().
962 Z3Expr getZ3SymExpr(SymbolRef Sym, QualType *RetTy,
963 bool *hasComparison) const;
965 // Wrapper to generate Z3Expr from SymbolData.
966 Z3Expr getZ3DataExpr(const SymbolID ID, QualType Ty) const;
968 // Wrapper to generate Z3Expr from SymbolCast.
969 Z3Expr getZ3CastExpr(const Z3Expr &Exp, QualType FromTy, QualType Ty) const;
971 // Wrapper to generate Z3Expr from BinarySymExpr.
972 // Sets the hasComparison and RetTy parameters. See getZ3Expr().
973 Z3Expr getZ3SymBinExpr(const BinarySymExpr *BSE, bool *hasComparison,
974 QualType *RetTy) const;
976 // Wrapper to generate Z3Expr from unpacked binary symbolic expression.
977 // Sets the RetTy parameter. See getZ3Expr().
978 Z3Expr getZ3BinExpr(const Z3Expr &LHS, QualType LTy,
979 BinaryOperator::Opcode Op, const Z3Expr &RHS,
980 QualType RTy, QualType *RetTy) const;
982 //===------------------------------------------------------------------===//
984 //===------------------------------------------------------------------===//
986 // Recover the QualType of an APSInt.
987 // TODO: Refactor to put elsewhere
988 QualType getAPSIntType(const llvm::APSInt &Int) const;
990 // Perform implicit type conversion on binary symbolic expressions.
991 // May modify all input parameters.
992 // TODO: Refactor to use built-in conversion functions
993 void doTypeConversion(Z3Expr &LHS, Z3Expr &RHS, QualType <y,
994 QualType &RTy) const;
996 // Perform implicit integer type conversion.
997 // May modify all input parameters.
998 // TODO: Refactor to use Sema::handleIntegerConversion()
999 template <typename T,
1000 T(doCast)(const T &, QualType, uint64_t, QualType, uint64_t)>
1001 void doIntTypeConversion(T &LHS, QualType <y, T &RHS, QualType &RTy) const;
1003 // Perform implicit floating-point type conversion.
1004 // May modify all input parameters.
1005 // TODO: Refactor to use Sema::handleFloatConversion()
1006 template <typename T,
1007 T(doCast)(const T &, QualType, uint64_t, QualType, uint64_t)>
1008 void doFloatTypeConversion(T &LHS, QualType <y, T &RHS,
1009 QualType &RTy) const;
1011 // Callback function for doCast parameter on APSInt type.
1012 static llvm::APSInt castAPSInt(const llvm::APSInt &V, QualType ToTy,
1013 uint64_t ToWidth, QualType FromTy,
1014 uint64_t FromWidth);
1015 }; // end class Z3ConstraintManager
1017 Z3_context Z3Context::ZC;
1019 } // end anonymous namespace
1021 ProgramStateRef Z3ConstraintManager::assumeSym(ProgramStateRef State,
1022 SymbolRef Sym, bool Assumption) {
1026 Z3Expr Exp = getZ3Expr(Sym, &RetTy, &hasComparison);
1027 // Create zero comparison for implicit boolean cast, with reversed assumption
1028 if (!hasComparison && !RetTy->isBooleanType())
1029 return assumeZ3Expr(State, Sym, getZ3ZeroExpr(Exp, RetTy, !Assumption));
1031 return assumeZ3Expr(State, Sym, Assumption ? Exp : getZ3NotExpr(Exp));
1034 ProgramStateRef Z3ConstraintManager::assumeSymInclusiveRange(
1035 ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
1036 const llvm::APSInt &To, bool InRange) {
1038 // The expression may be casted, so we cannot call getZ3DataExpr() directly
1039 Z3Expr Exp = getZ3Expr(Sym, &RetTy);
1041 assert((getAPSIntType(From) == getAPSIntType(To)) &&
1042 "Range values have different types!");
1043 QualType RTy = getAPSIntType(From);
1044 bool isSignedTy = RetTy->isSignedIntegerOrEnumerationType();
1045 Z3Expr FromExp = Z3Expr::fromAPSInt(From);
1046 Z3Expr ToExp = Z3Expr::fromAPSInt(To);
1048 // Construct single (in)equality
1050 return assumeZ3Expr(State, Sym,
1051 getZ3BinExpr(Exp, RetTy, InRange ? BO_EQ : BO_NE,
1052 FromExp, RTy, nullptr));
1054 // Construct two (in)equalities, and a logical and/or
1056 getZ3BinExpr(Exp, RetTy, InRange ? BO_GE : BO_LT, FromExp, RTy, nullptr);
1058 getZ3BinExpr(Exp, RetTy, InRange ? BO_LE : BO_GT, ToExp, RTy, nullptr);
1059 return assumeZ3Expr(
1061 Z3Expr::fromBinOp(LHS, InRange ? BO_LAnd : BO_LOr, RHS, isSignedTy));
1064 ProgramStateRef Z3ConstraintManager::assumeSymUnsupported(ProgramStateRef State,
1067 // Skip anything that is unsupported
1071 bool Z3ConstraintManager::canReasonAbout(SVal X) const {
1072 const TargetInfo &TI = getBasicVals().getContext().getTargetInfo();
1074 Optional<nonloc::SymbolVal> SymVal = X.getAs<nonloc::SymbolVal>();
1078 const SymExpr *Sym = SymVal->getSymbol();
1080 QualType Ty = Sym->getType();
1082 // Complex types are not modeled
1083 if (Ty->isComplexType() || Ty->isComplexIntegerType())
1086 // Non-IEEE 754 floating-point types are not modeled
1087 if ((Ty->isSpecificBuiltinType(BuiltinType::LongDouble) &&
1088 (&TI.getLongDoubleFormat() == &llvm::APFloat::x87DoubleExtended() ||
1089 &TI.getLongDoubleFormat() == &llvm::APFloat::PPCDoubleDouble())))
1092 if (isa<SymbolData>(Sym)) {
1094 } else if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) {
1095 Sym = SC->getOperand();
1096 } else if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
1097 if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
1098 Sym = SIE->getLHS();
1099 } else if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) {
1100 Sym = ISE->getRHS();
1101 } else if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {
1102 return canReasonAbout(nonloc::SymbolVal(SSM->getLHS())) &&
1103 canReasonAbout(nonloc::SymbolVal(SSM->getRHS()));
1105 llvm_unreachable("Unsupported binary expression to reason about!");
1108 llvm_unreachable("Unsupported expression to reason about!");
1115 ConditionTruthVal Z3ConstraintManager::checkNull(ProgramStateRef State,
1118 // The expression may be casted, so we cannot call getZ3DataExpr() directly
1119 Z3Expr VarExp = getZ3Expr(Sym, &RetTy);
1120 Z3Expr Exp = getZ3ZeroExpr(VarExp, RetTy, true);
1121 // Negate the constraint
1122 Z3Expr NotExp = getZ3ZeroExpr(VarExp, RetTy, false);
1125 Solver.addStateConstraints(State);
1128 Solver.addConstraint(Exp);
1129 Z3_lbool isSat = Solver.check();
1132 Solver.addConstraint(NotExp);
1133 Z3_lbool isNotSat = Solver.check();
1135 // Zero is the only possible solution
1136 if (isSat == Z3_L_TRUE && isNotSat == Z3_L_FALSE)
1138 // Zero is not a solution
1139 else if (isSat == Z3_L_FALSE && isNotSat == Z3_L_TRUE)
1142 // Zero may be a solution
1143 return ConditionTruthVal();
1146 const llvm::APSInt *Z3ConstraintManager::getSymVal(ProgramStateRef State,
1147 SymbolRef Sym) const {
1148 BasicValueFactory &BV = getBasicVals();
1149 ASTContext &Ctx = BV.getContext();
1151 if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) {
1152 QualType Ty = Sym->getType();
1153 assert(!Ty->isRealFloatingType());
1154 llvm::APSInt Value(Ctx.getTypeSize(Ty),
1155 !Ty->isSignedIntegerOrEnumerationType());
1157 Z3Expr Exp = getZ3DataExpr(SD->getSymbolID(), Ty);
1160 Solver.addStateConstraints(State);
1162 // Constraints are unsatisfiable
1163 if (Solver.check() != Z3_L_TRUE)
1166 Z3Model Model = Solver.getModel();
1167 // Model does not assign interpretation
1168 if (!Model.getInterpretation(Exp, Value))
1171 // A value has been obtained, check if it is the only value
1172 Z3Expr NotExp = Z3Expr::fromBinOp(
1174 Ty->isBooleanType() ? Z3Expr::fromBoolean(Value.getBoolValue())
1175 : Z3Expr::fromAPSInt(Value),
1178 Solver.addConstraint(NotExp);
1179 if (Solver.check() == Z3_L_TRUE)
1182 // This is the only solution, store it
1183 return &BV.getValue(Value);
1184 } else if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) {
1185 SymbolRef CastSym = SC->getOperand();
1186 QualType CastTy = SC->getType();
1187 // Skip the void type
1188 if (CastTy->isVoidType())
1191 const llvm::APSInt *Value;
1192 if (!(Value = getSymVal(State, CastSym)))
1194 return &BV.Convert(SC->getType(), *Value);
1195 } else if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
1196 const llvm::APSInt *LHS, *RHS;
1197 if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
1198 LHS = getSymVal(State, SIE->getLHS());
1199 RHS = &SIE->getRHS();
1200 } else if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) {
1201 LHS = &ISE->getLHS();
1202 RHS = getSymVal(State, ISE->getRHS());
1203 } else if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {
1204 // Early termination to avoid expensive call
1205 LHS = getSymVal(State, SSM->getLHS());
1206 RHS = LHS ? getSymVal(State, SSM->getRHS()) : nullptr;
1208 llvm_unreachable("Unsupported binary expression to get symbol value!");
1214 llvm::APSInt ConvertedLHS = *LHS, ConvertedRHS = *RHS;
1215 QualType LTy = getAPSIntType(*LHS), RTy = getAPSIntType(*RHS);
1216 doIntTypeConversion<llvm::APSInt, Z3ConstraintManager::castAPSInt>(
1217 ConvertedLHS, LTy, ConvertedRHS, RTy);
1218 return BV.evalAPSInt(BSE->getOpcode(), ConvertedLHS, ConvertedRHS);
1221 llvm_unreachable("Unsupported expression to get symbol value!");
1225 Z3ConstraintManager::removeDeadBindings(ProgramStateRef State,
1226 SymbolReaper &SymReaper) {
1227 ConstraintZ3Ty CZ = State->get<ConstraintZ3>();
1228 ConstraintZ3Ty::Factory &CZFactory = State->get_context<ConstraintZ3>();
1230 for (ConstraintZ3Ty::iterator I = CZ.begin(), E = CZ.end(); I != E; ++I) {
1231 if (SymReaper.maybeDead(I->first))
1232 CZ = CZFactory.remove(CZ, *I);
1235 return State->set<ConstraintZ3>(CZ);
1238 //===------------------------------------------------------------------===//
1239 // Internal implementation.
1240 //===------------------------------------------------------------------===//
1242 ProgramStateRef Z3ConstraintManager::assumeZ3Expr(ProgramStateRef State,
1244 const Z3Expr &Exp) {
1245 // Check the model, avoid simplifying AST to save time
1246 if (checkZ3Model(State, Exp) == Z3_L_TRUE)
1247 return State->add<ConstraintZ3>(std::make_pair(Sym, Exp));
1252 Z3_lbool Z3ConstraintManager::checkZ3Model(ProgramStateRef State,
1253 const Z3Expr &Exp) const {
1255 Solver.addConstraint(Exp);
1256 Solver.addStateConstraints(State);
1257 return Solver.check();
1260 Z3Expr Z3ConstraintManager::getZ3Expr(SymbolRef Sym, QualType *RetTy,
1261 bool *hasComparison) const {
1262 if (hasComparison) {
1263 *hasComparison = false;
1266 return getZ3SymExpr(Sym, RetTy, hasComparison);
1269 Z3Expr Z3ConstraintManager::getZ3NotExpr(const Z3Expr &Exp) const {
1270 return Z3Expr::fromUnOp(UO_LNot, Exp);
1273 Z3Expr Z3ConstraintManager::getZ3ZeroExpr(const Z3Expr &Exp, QualType Ty,
1274 bool Assumption) const {
1275 ASTContext &Ctx = getBasicVals().getContext();
1276 if (Ty->isRealFloatingType()) {
1277 llvm::APFloat Zero = llvm::APFloat::getZero(Ctx.getFloatTypeSemantics(Ty));
1278 return Z3Expr::fromFloatBinOp(Exp, Assumption ? BO_EQ : BO_NE,
1279 Z3Expr::fromAPFloat(Zero));
1280 } else if (Ty->isIntegralOrEnumerationType() || Ty->isAnyPointerType() ||
1281 Ty->isBlockPointerType() || Ty->isReferenceType()) {
1282 bool isSigned = Ty->isSignedIntegerOrEnumerationType();
1283 // Skip explicit comparison for boolean types
1284 if (Ty->isBooleanType())
1285 return Assumption ? getZ3NotExpr(Exp) : Exp;
1286 return Z3Expr::fromBinOp(Exp, Assumption ? BO_EQ : BO_NE,
1287 Z3Expr::fromInt("0", Ctx.getTypeSize(Ty)),
1291 llvm_unreachable("Unsupported type for zero value!");
1294 Z3Expr Z3ConstraintManager::getZ3SymExpr(SymbolRef Sym, QualType *RetTy,
1295 bool *hasComparison) const {
1296 if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) {
1298 *RetTy = Sym->getType();
1300 return getZ3DataExpr(SD->getSymbolID(), Sym->getType());
1301 } else if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) {
1303 *RetTy = Sym->getType();
1306 Z3Expr Exp = getZ3SymExpr(SC->getOperand(), &FromTy, hasComparison);
1307 // Casting an expression with a comparison invalidates it. Note that this
1308 // must occur after the recursive call above.
1309 // e.g. (signed char) (x > 0)
1311 *hasComparison = false;
1312 return getZ3CastExpr(Exp, FromTy, Sym->getType());
1313 } else if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
1314 Z3Expr Exp = getZ3SymBinExpr(BSE, hasComparison, RetTy);
1315 // Set the hasComparison parameter, in post-order traversal order.
1317 *hasComparison = BinaryOperator::isComparisonOp(BSE->getOpcode());
1321 llvm_unreachable("Unsupported SymbolRef type!");
1324 Z3Expr Z3ConstraintManager::getZ3DataExpr(const SymbolID ID,
1325 QualType Ty) const {
1326 ASTContext &Ctx = getBasicVals().getContext();
1327 return Z3Expr::fromData(ID, Ty->isBooleanType(), Ty->isRealFloatingType(),
1328 Ctx.getTypeSize(Ty));
1331 Z3Expr Z3ConstraintManager::getZ3CastExpr(const Z3Expr &Exp, QualType FromTy,
1332 QualType ToTy) const {
1333 ASTContext &Ctx = getBasicVals().getContext();
1334 return Z3Expr::fromCast(Exp, ToTy, Ctx.getTypeSize(ToTy), FromTy,
1335 Ctx.getTypeSize(FromTy));
1338 Z3Expr Z3ConstraintManager::getZ3SymBinExpr(const BinarySymExpr *BSE,
1339 bool *hasComparison,
1340 QualType *RetTy) const {
1342 BinaryOperator::Opcode Op = BSE->getOpcode();
1344 if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
1345 RTy = getAPSIntType(SIE->getRHS());
1346 Z3Expr LHS = getZ3SymExpr(SIE->getLHS(), <y, hasComparison);
1347 Z3Expr RHS = Z3Expr::fromAPSInt(SIE->getRHS());
1348 return getZ3BinExpr(LHS, LTy, Op, RHS, RTy, RetTy);
1349 } else if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) {
1350 LTy = getAPSIntType(ISE->getLHS());
1351 Z3Expr LHS = Z3Expr::fromAPSInt(ISE->getLHS());
1352 Z3Expr RHS = getZ3SymExpr(ISE->getRHS(), &RTy, hasComparison);
1353 return getZ3BinExpr(LHS, LTy, Op, RHS, RTy, RetTy);
1354 } else if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {
1355 Z3Expr LHS = getZ3SymExpr(SSM->getLHS(), <y, hasComparison);
1356 Z3Expr RHS = getZ3SymExpr(SSM->getRHS(), &RTy, hasComparison);
1357 return getZ3BinExpr(LHS, LTy, Op, RHS, RTy, RetTy);
1359 llvm_unreachable("Unsupported BinarySymExpr type!");
1363 Z3Expr Z3ConstraintManager::getZ3BinExpr(const Z3Expr &LHS, QualType LTy,
1364 BinaryOperator::Opcode Op,
1365 const Z3Expr &RHS, QualType RTy,
1366 QualType *RetTy) const {
1367 Z3Expr NewLHS = LHS;
1368 Z3Expr NewRHS = RHS;
1369 doTypeConversion(NewLHS, NewRHS, LTy, RTy);
1370 // Update the return type parameter if the output type has changed.
1372 // A boolean result can be represented as an integer type in C/C++, but at
1373 // this point we only care about the Z3 type. Set it as a boolean type to
1374 // avoid subsequent Z3 errors.
1375 if (BinaryOperator::isComparisonOp(Op) || BinaryOperator::isLogicalOp(Op)) {
1376 ASTContext &Ctx = getBasicVals().getContext();
1377 *RetTy = Ctx.BoolTy;
1382 // If the two operands are pointers and the operation is a subtraction, the
1383 // result is of type ptrdiff_t, which is signed
1384 if (LTy->isAnyPointerType() && LTy == RTy && Op == BO_Sub) {
1385 ASTContext &Ctx = getBasicVals().getContext();
1386 *RetTy = Ctx.getIntTypeForBitwidth(Ctx.getTypeSize(LTy), true);
1390 return LTy->isRealFloatingType()
1391 ? Z3Expr::fromFloatBinOp(NewLHS, Op, NewRHS)
1392 : Z3Expr::fromBinOp(NewLHS, Op, NewRHS,
1393 LTy->isSignedIntegerOrEnumerationType());
1396 //===------------------------------------------------------------------===//
1397 // Helper functions.
1398 //===------------------------------------------------------------------===//
1400 QualType Z3ConstraintManager::getAPSIntType(const llvm::APSInt &Int) const {
1401 ASTContext &Ctx = getBasicVals().getContext();
1402 return Ctx.getIntTypeForBitwidth(Int.getBitWidth(), Int.isSigned());
1405 void Z3ConstraintManager::doTypeConversion(Z3Expr &LHS, Z3Expr &RHS,
1406 QualType <y, QualType &RTy) const {
1407 ASTContext &Ctx = getBasicVals().getContext();
1409 // Perform type conversion
1410 if (LTy->isIntegralOrEnumerationType() &&
1411 RTy->isIntegralOrEnumerationType()) {
1412 if (LTy->isArithmeticType() && RTy->isArithmeticType())
1413 return doIntTypeConversion<Z3Expr, Z3Expr::fromCast>(LHS, LTy, RHS, RTy);
1414 } else if (LTy->isRealFloatingType() || RTy->isRealFloatingType()) {
1415 return doFloatTypeConversion<Z3Expr, Z3Expr::fromCast>(LHS, LTy, RHS, RTy);
1416 } else if ((LTy->isAnyPointerType() || RTy->isAnyPointerType()) ||
1417 (LTy->isBlockPointerType() || RTy->isBlockPointerType()) ||
1418 (LTy->isReferenceType() || RTy->isReferenceType())) {
1419 // TODO: Refactor to Sema::FindCompositePointerType(), and
1420 // Sema::CheckCompareOperands().
1422 uint64_t LBitWidth = Ctx.getTypeSize(LTy);
1423 uint64_t RBitWidth = Ctx.getTypeSize(RTy);
1425 // Cast the non-pointer type to the pointer type.
1426 // TODO: Be more strict about this.
1427 if ((LTy->isAnyPointerType() ^ RTy->isAnyPointerType()) ||
1428 (LTy->isBlockPointerType() ^ RTy->isBlockPointerType()) ||
1429 (LTy->isReferenceType() ^ RTy->isReferenceType())) {
1430 if (LTy->isNullPtrType() || LTy->isBlockPointerType() ||
1431 LTy->isReferenceType()) {
1432 LHS = Z3Expr::fromCast(LHS, RTy, RBitWidth, LTy, LBitWidth);
1435 RHS = Z3Expr::fromCast(RHS, LTy, LBitWidth, RTy, RBitWidth);
1440 // Cast the void pointer type to the non-void pointer type.
1441 // For void types, this assumes that the casted value is equal to the value
1442 // of the original pointer, and does not account for alignment requirements.
1443 if (LTy->isVoidPointerType() ^ RTy->isVoidPointerType()) {
1444 assert((Ctx.getTypeSize(LTy) == Ctx.getTypeSize(RTy)) &&
1445 "Pointer types have different bitwidths!");
1446 if (RTy->isVoidPointerType())
1456 // Fallback: for the solver, assume that these types don't really matter
1457 if ((LTy.getCanonicalType() == RTy.getCanonicalType()) ||
1458 (LTy->isObjCObjectPointerType() && RTy->isObjCObjectPointerType())) {
1463 // TODO: Refine behavior for invalid type casts
1466 template <typename T,
1467 T(doCast)(const T &, QualType, uint64_t, QualType, uint64_t)>
1468 void Z3ConstraintManager::doIntTypeConversion(T &LHS, QualType <y, T &RHS,
1469 QualType &RTy) const {
1470 ASTContext &Ctx = getBasicVals().getContext();
1472 uint64_t LBitWidth = Ctx.getTypeSize(LTy);
1473 uint64_t RBitWidth = Ctx.getTypeSize(RTy);
1475 // Always perform integer promotion before checking type equality.
1476 // Otherwise, e.g. (bool) a + (bool) b could trigger a backend assertion
1477 if (LTy->isPromotableIntegerType()) {
1478 QualType NewTy = Ctx.getPromotedIntegerType(LTy);
1479 uint64_t NewBitWidth = Ctx.getTypeSize(NewTy);
1480 LHS = (*doCast)(LHS, NewTy, NewBitWidth, LTy, LBitWidth);
1482 LBitWidth = NewBitWidth;
1484 if (RTy->isPromotableIntegerType()) {
1485 QualType NewTy = Ctx.getPromotedIntegerType(RTy);
1486 uint64_t NewBitWidth = Ctx.getTypeSize(NewTy);
1487 RHS = (*doCast)(RHS, NewTy, NewBitWidth, RTy, RBitWidth);
1489 RBitWidth = NewBitWidth;
1495 // Perform integer type conversion
1496 // Note: Safe to skip updating bitwidth because this must terminate
1497 bool isLSignedTy = LTy->isSignedIntegerOrEnumerationType();
1498 bool isRSignedTy = RTy->isSignedIntegerOrEnumerationType();
1500 int order = Ctx.getIntegerTypeOrder(LTy, RTy);
1501 if (isLSignedTy == isRSignedTy) {
1502 // Same signedness; use the higher-ranked type
1504 RHS = (*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);
1507 LHS = (*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth);
1510 } else if (order != (isLSignedTy ? 1 : -1)) {
1511 // The unsigned type has greater than or equal rank to the
1512 // signed type, so use the unsigned type
1514 RHS = (*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);
1517 LHS = (*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth);
1520 } else if (LBitWidth != RBitWidth) {
1521 // The two types are different widths; if we are here, that
1522 // means the signed type is larger than the unsigned type, so
1523 // use the signed type.
1525 RHS = (*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);
1528 LHS = (*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth);
1532 // The signed type is higher-ranked than the unsigned type,
1533 // but isn't actually any bigger (like unsigned int and long
1534 // on most 32-bit systems). Use the unsigned type corresponding
1535 // to the signed type.
1536 QualType NewTy = Ctx.getCorrespondingUnsignedType(isLSignedTy ? LTy : RTy);
1537 RHS = (*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);
1539 LHS = (*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth);
1544 template <typename T,
1545 T(doCast)(const T &, QualType, uint64_t, QualType, uint64_t)>
1546 void Z3ConstraintManager::doFloatTypeConversion(T &LHS, QualType <y, T &RHS,
1547 QualType &RTy) const {
1548 ASTContext &Ctx = getBasicVals().getContext();
1550 uint64_t LBitWidth = Ctx.getTypeSize(LTy);
1551 uint64_t RBitWidth = Ctx.getTypeSize(RTy);
1553 // Perform float-point type promotion
1554 if (!LTy->isRealFloatingType()) {
1555 LHS = (*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth);
1557 LBitWidth = RBitWidth;
1559 if (!RTy->isRealFloatingType()) {
1560 RHS = (*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);
1562 RBitWidth = LBitWidth;
1568 // If we have two real floating types, convert the smaller operand to the
1570 // Note: Safe to skip updating bitwidth because this must terminate
1571 int order = Ctx.getFloatingTypeOrder(LTy, RTy);
1573 RHS = Z3Expr::fromCast(RHS, LTy, LBitWidth, RTy, RBitWidth);
1575 } else if (order == 0) {
1576 LHS = Z3Expr::fromCast(LHS, RTy, RBitWidth, LTy, LBitWidth);
1579 llvm_unreachable("Unsupported floating-point type cast!");
1583 llvm::APSInt Z3ConstraintManager::castAPSInt(const llvm::APSInt &V,
1584 QualType ToTy, uint64_t ToWidth,
1586 uint64_t FromWidth) {
1587 APSIntType TargetType(ToWidth, !ToTy->isSignedIntegerOrEnumerationType());
1588 return TargetType.convert(V);
1591 //==------------------------------------------------------------------------==/
1593 //==------------------------------------------------------------------------==/
1595 void Z3ConstraintManager::print(ProgramStateRef St, raw_ostream &OS,
1596 const char *nl, const char *sep) {
1598 ConstraintZ3Ty CZ = St->get<ConstraintZ3>();
1600 OS << nl << sep << "Constraints:";
1601 for (ConstraintZ3Ty::iterator I = CZ.begin(), E = CZ.end(); I != E; ++I) {
1602 OS << nl << ' ' << I->first << " : ";
1603 I->second.print(OS);
1610 std::unique_ptr<ConstraintManager>
1611 ento::CreateZ3ConstraintManager(ProgramStateManager &StMgr, SubEngine *Eng) {
1612 #if CLANG_ANALYZER_WITH_Z3
1613 return llvm::make_unique<Z3ConstraintManager>(Eng, StMgr.getSValBuilder());
1615 llvm::report_fatal_error("Clang was not compiled with Z3 support!", false);