Author: mramalho
Date: Mon Jul 16 06:32:22 2018
New Revision: 337169
URL: http://llvm.org/viewvc/llvm-project?rev=337169&view=rev
Log:
[analyzer] Fix the Z3 backend always generating unsigned APSInt
Summary:
In `toAPSInt`, the Z3 backend was not checking the variable `Int`'s type and
was always generating unsigned `APSInt`s.
This was found by accident when I removed:
```
llvm::APSInt ConvertedLHS, ConvertedRHS;
QualType LTy, RTy;
std::tie(ConvertedLHS, LTy) = fixAPSInt(*LHS);
std::tie(ConvertedRHS, RTy) = fixAPSInt(*RHS);
- doIntTypePromotion<llvm::APSInt, Z3ConstraintManager::castAPSInt>(
- ConvertedLHS, LTy, ConvertedRHS, RTy);
return BVF.evalAPSInt(BSE->getOpcode(), ConvertedLHS, ConvertedRHS);
```
And the `BasicValueFactory` started to complain about different `signedness`.
Reviewers: george.karpenkov, NoQ, ddcc
Reviewed By: ddcc
Subscribers: xazax.hun, szepet, a.sidorin
Differential Revision: https://reviews.llvm.org/D49305
Modified:
cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
Modified: cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
URL:
http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp?rev=337169&r1=337168&r2=337169&view=diff
==============================================================================
--- cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp (original)
+++ cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Mon Jul 16
06:32:22 2018
@@ -681,12 +681,14 @@ public:
Z3_get_numeral_uint64(Z3Context::ZC, AST,
reinterpret_cast<__uint64 *>(&Value[0]));
if (Sort.getBitvectorSortSize() <= 64) {
- Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), Value[0]), true);
+ Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), Value[0]),
+ Int.isUnsigned());
} else if (Sort.getBitvectorSortSize() == 128) {
Z3Expr ASTHigh = Z3Expr(Z3_mk_extract(Z3Context::ZC, 127, 64, AST));
Z3_get_numeral_uint64(Z3Context::ZC, AST,
reinterpret_cast<__uint64 *>(&Value[1]));
- Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), Value), true);
+ Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), Value),
+ Int.isUnsigned());
} else {
assert(false && "Bitwidth not supported!");
return false;
@@ -702,7 +704,7 @@ public:
llvm::APInt(Int.getBitWidth(),
Z3_get_bool_value(Z3Context::ZC, AST) == Z3_L_TRUE ? 1
: 0),
- true);
+ Int.isUnsigned());
return true;
}
}
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
