Author: mramalho Date: Thu Jul 26 04:17:13 2018 New Revision: 338020 URL: http://llvm.org/viewvc/llvm-project?rev=338020&view=rev Log: [analyzer] Fixed method to get APSInt model
Summary: This patch replaces the current method of getting an `APSInt` from Z3's model by calling generic API method `getBitvector` instead of `Z3_get_numeral_uint64`. By calling `getBitvector`, there's no need to handle bitvectors with bit width == 128 separately. And, as a bonus, clang now compiles correctly with Z3 4.7.1. Reviewers: NoQ, george.karpenkov Reviewed By: george.karpenkov Subscribers: xazax.hun, szepet, a.sidorin Differential Revision: https://reviews.llvm.org/D49818 Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h?rev=338020&r1=338019&r2=338020&view=diff ============================================================================== --- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h (original) +++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h Thu Jul 26 04:17:13 2018 @@ -931,7 +931,8 @@ public: virtual SMTExprRef getFloatRoundingMode() = 0; // If the a model is available, returns the value of a given bitvector symbol - virtual const llvm::APSInt getBitvector(const SMTExprRef &Exp) = 0; + virtual llvm::APSInt getBitvector(const SMTExprRef &Exp, unsigned BitWidth, + bool isUnsigned) = 0; // If the a model is available, returns the value of a given boolean symbol virtual bool getBoolean(const SMTExprRef &Exp) = 0; Modified: cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp?rev=338020&r1=338019&r2=338020&view=diff ============================================================================== --- cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp (original) +++ cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Thu Jul 26 04:17:13 2018 @@ -734,10 +734,11 @@ public: toZ3Sort(*Sort).Sort))); } - const llvm::APSInt getBitvector(const SMTExprRef &Exp) override { - // FIXME: this returns a string and the bitWidth is overridden - return llvm::APSInt( - Z3_get_numeral_string(Context.Context, toZ3Expr(*Exp).AST)); + llvm::APSInt getBitvector(const SMTExprRef &Exp, unsigned BitWidth, + bool isUnsigned) override { + return llvm::APSInt(llvm::APInt( + BitWidth, Z3_get_numeral_string(Context.Context, toZ3Expr(*Exp).AST), + 10)); } bool getBoolean(const SMTExprRef &Exp) override { @@ -814,26 +815,20 @@ public: return false; } - uint64_t Value[2]; - // Force cast because Z3 defines __uint64 to be a unsigned long long - // type, which isn't compatible with a unsigned long type, even if they - // are the same size. - Z3_get_numeral_uint64(Context.Context, toZ3Expr(*AST).AST, - reinterpret_cast<__uint64 *>(&Value[0])); - if (Sort->getBitvectorSortSize() <= 64) { - Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), Value[0]), - Int.isUnsigned()); - } else if (Sort->getBitvectorSortSize() == 128) { - SMTExprRef ASTHigh = mkBVExtract(127, 64, AST); - Z3_get_numeral_uint64(Context.Context, toZ3Expr(*AST).AST, - reinterpret_cast<__uint64 *>(&Value[1])); - Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), Value), - Int.isUnsigned()); - } else { - assert(false && "Bitwidth not supported!"); - return false; + // FIXME: This function is also used to retrieve floating-point values, + // which can be 16, 32, 64 or 128 bits long. Bitvectors can be anything + // between 1 and 64 bits long, which is the reason we have this weird + // guard. In the future, we need proper calls in the backend to retrieve + // floating-points and its special values (NaN, +/-infinity, +/-zero), + // then we can drop this weird condition. + if (Sort->getBitvectorSortSize() <= 64 || + Sort->getBitvectorSortSize() == 128) { + Int = getBitvector(AST, Int.getBitWidth(), Int.isUnsigned()); + return true; } - return true; + + assert(false && "Bitwidth not supported!"); + return false; } if (Sort->isBooleanSort()) { _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
