replica
/
hanchenye-llvm-project
2
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

[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

llvm-svn: 338020
This commit is contained in:
Mikhail R. Gadelha 2018-07-26 11:17:13 +00:00
parent 4a612d4bf2
commit 127093129a
2 changed files with 20 additions and 24 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h
View File

@ -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;

39
clang/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
View File

@ -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,27 +815,21 @@ 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 {
// 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;
}
assert(false && "Bitwidth not supported!");
return false;
}
return true;
}
if (Sort->isBooleanSort()) {
if (useSemantics && Int.getBitWidth() < 1) {