r333704 - [analyzer] fix bug with 1-bit APSInt types in Z3ConstraintManager
Dominic Chen via cfe-commits
cfe-commits at lists.llvm.org
Thu May 31 15:23:07 PDT 2018
Author: ddcc
Date: Thu May 31 15:23:07 2018
New Revision: 333704
URL: http://llvm.org/viewvc/llvm-project?rev=333704&view=rev
Log:
[analyzer] fix bug with 1-bit APSInt types in Z3ConstraintManager
Summary: Clang does not have a corresponding QualType for a 1-bit APSInt, so use the BoolTy and extend the APSInt. Split from D35450. Fixes PR37622.
Reviewers: george.karpenkov, NoQ
Subscribers: mikhail.ramalho, xazax.hun, szepet, rnkovacs, cfe-commits, a.sidorin
Differential Revision: https://reviews.llvm.org/D47603
Added:
cfe/trunk/test/Analysis/apsint.c
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=333704&r1=333703&r2=333704&view=diff
==============================================================================
--- cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp (original)
+++ cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Thu May 31 15:23:07 2018
@@ -987,6 +987,9 @@ private:
// TODO: Refactor to put elsewhere
QualType getAPSIntType(const llvm::APSInt &Int) const;
+ // Get the QualTy for the input APSInt, and fix it if it has a bitwidth of 1.
+ std::pair<llvm::APSInt, QualType> fixAPSInt(const llvm::APSInt &Int) const;
+
// Perform implicit type conversion on binary symbolic expressions.
// May modify all input parameters.
// TODO: Refactor to use built-in conversion functions
@@ -1038,27 +1041,31 @@ ProgramStateRef Z3ConstraintManager::ass
// The expression may be casted, so we cannot call getZ3DataExpr() directly
Z3Expr Exp = getZ3Expr(Sym, &RetTy);
- assert((getAPSIntType(From) == getAPSIntType(To)) &&
- "Range values have different types!");
- QualType RTy = getAPSIntType(From);
- bool isSignedTy = RetTy->isSignedIntegerOrEnumerationType();
- Z3Expr FromExp = Z3Expr::fromAPSInt(From);
- Z3Expr ToExp = Z3Expr::fromAPSInt(To);
+ QualType FromTy;
+ llvm::APSInt NewFromInt;
+ std::tie(NewFromInt, FromTy) = fixAPSInt(From);
+ Z3Expr FromExp = Z3Expr::fromAPSInt(NewFromInt);
// Construct single (in)equality
if (From == To)
return assumeZ3Expr(State, Sym,
getZ3BinExpr(Exp, RetTy, InRange ? BO_EQ : BO_NE,
- FromExp, RTy, nullptr));
+ FromExp, FromTy, nullptr));
+ QualType ToTy;
+ llvm::APSInt NewToInt;
+ std::tie(NewToInt, ToTy) = fixAPSInt(To);
+ Z3Expr ToExp = Z3Expr::fromAPSInt(NewToInt);
+ assert(FromTy == ToTy && "Range values have different types!");
// Construct two (in)equalities, and a logical and/or
- Z3Expr LHS =
- getZ3BinExpr(Exp, RetTy, InRange ? BO_GE : BO_LT, FromExp, RTy, nullptr);
+ Z3Expr LHS = getZ3BinExpr(Exp, RetTy, InRange ? BO_GE : BO_LT, FromExp,
+ FromTy, nullptr);
Z3Expr RHS =
- getZ3BinExpr(Exp, RetTy, InRange ? BO_LE : BO_GT, ToExp, RTy, nullptr);
+ getZ3BinExpr(Exp, RetTy, InRange ? BO_LE : BO_GT, ToExp, ToTy, nullptr);
return assumeZ3Expr(
State, Sym,
- Z3Expr::fromBinOp(LHS, InRange ? BO_LAnd : BO_LOr, RHS, isSignedTy));
+ Z3Expr::fromBinOp(LHS, InRange ? BO_LAnd : BO_LOr, RHS,
+ RetTy->isSignedIntegerOrEnumerationType()));
}
ProgramStateRef Z3ConstraintManager::assumeSymUnsupported(ProgramStateRef State,
@@ -1145,8 +1152,8 @@ ConditionTruthVal Z3ConstraintManager::c
const llvm::APSInt *Z3ConstraintManager::getSymVal(ProgramStateRef State,
SymbolRef Sym) const {
- BasicValueFactory &BV = getBasicVals();
- ASTContext &Ctx = BV.getContext();
+ BasicValueFactory &BVF = getBasicVals();
+ ASTContext &Ctx = BVF.getContext();
if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) {
QualType Ty = Sym->getType();
@@ -1180,7 +1187,7 @@ const llvm::APSInt *Z3ConstraintManager:
return nullptr;
// This is the only solution, store it
- return &BV.getValue(Value);
+ return &BVF.getValue(Value);
} else if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) {
SymbolRef CastSym = SC->getOperand();
QualType CastTy = SC->getType();
@@ -1191,7 +1198,7 @@ const llvm::APSInt *Z3ConstraintManager:
const llvm::APSInt *Value;
if (!(Value = getSymVal(State, CastSym)))
return nullptr;
- return &BV.Convert(SC->getType(), *Value);
+ return &BVF.Convert(SC->getType(), *Value);
} else if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
const llvm::APSInt *LHS, *RHS;
if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
@@ -1215,7 +1222,7 @@ const llvm::APSInt *Z3ConstraintManager:
QualType LTy = getAPSIntType(*LHS), RTy = getAPSIntType(*RHS);
doIntTypeConversion<llvm::APSInt, Z3ConstraintManager::castAPSInt>(
ConvertedLHS, LTy, ConvertedRHS, RTy);
- return BV.evalAPSInt(BSE->getOpcode(), ConvertedLHS, ConvertedRHS);
+ return BVF.evalAPSInt(BSE->getOpcode(), ConvertedLHS, ConvertedRHS);
}
llvm_unreachable("Unsupported expression to get symbol value!");
@@ -1342,13 +1349,15 @@ Z3Expr Z3ConstraintManager::getZ3SymBinE
BinaryOperator::Opcode Op = BSE->getOpcode();
if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
- RTy = getAPSIntType(SIE->getRHS());
Z3Expr LHS = getZ3SymExpr(SIE->getLHS(), <y, hasComparison);
- Z3Expr RHS = Z3Expr::fromAPSInt(SIE->getRHS());
+ llvm::APSInt NewRInt;
+ std::tie(NewRInt, RTy) = fixAPSInt(SIE->getRHS());
+ Z3Expr RHS = Z3Expr::fromAPSInt(NewRInt);
return getZ3BinExpr(LHS, LTy, Op, RHS, RTy, RetTy);
} else if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) {
- LTy = getAPSIntType(ISE->getLHS());
- Z3Expr LHS = Z3Expr::fromAPSInt(ISE->getLHS());
+ llvm::APSInt NewLInt;
+ std::tie(NewLInt, LTy) = fixAPSInt(ISE->getLHS());
+ Z3Expr LHS = Z3Expr::fromAPSInt(NewLInt);
Z3Expr RHS = getZ3SymExpr(ISE->getRHS(), &RTy, hasComparison);
return getZ3BinExpr(LHS, LTy, Op, RHS, RTy, RetTy);
} else if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {
@@ -1402,10 +1411,27 @@ QualType Z3ConstraintManager::getAPSIntT
return Ctx.getIntTypeForBitwidth(Int.getBitWidth(), Int.isSigned());
}
+std::pair<llvm::APSInt, QualType>
+Z3ConstraintManager::fixAPSInt(const llvm::APSInt &Int) const {
+ llvm::APSInt NewInt;
+
+ // FIXME: This should be a cast from a 1-bit integer type to a boolean type,
+ // but the former is not available in Clang. Instead, extend the APSInt
+ // directly.
+ if (Int.getBitWidth() == 1 && getAPSIntType(Int).isNull()) {
+ ASTContext &Ctx = getBasicVals().getContext();
+ NewInt = Int.extend(Ctx.getTypeSize(Ctx.BoolTy));
+ } else
+ NewInt = Int;
+
+ return std::make_pair(NewInt, getAPSIntType(NewInt));
+}
+
void Z3ConstraintManager::doTypeConversion(Z3Expr &LHS, Z3Expr &RHS,
QualType <y, QualType &RTy) const {
ASTContext &Ctx = getBasicVals().getContext();
+ assert(!LTy.isNull() && !RTy.isNull() && "Input type is null!");
// Perform type conversion
if (LTy->isIntegralOrEnumerationType() &&
RTy->isIntegralOrEnumerationType()) {
@@ -1468,10 +1494,10 @@ template <typename T,
void Z3ConstraintManager::doIntTypeConversion(T &LHS, QualType <y, T &RHS,
QualType &RTy) const {
ASTContext &Ctx = getBasicVals().getContext();
-
uint64_t LBitWidth = Ctx.getTypeSize(LTy);
uint64_t RBitWidth = Ctx.getTypeSize(RTy);
+ assert(!LTy.isNull() && !RTy.isNull() && "Input type is null!");
// Always perform integer promotion before checking type equality.
// Otherwise, e.g. (bool) a + (bool) b could trigger a backend assertion
if (LTy->isPromotableIntegerType()) {
@@ -1612,7 +1638,9 @@ ento::CreateZ3ConstraintManager(ProgramS
#if CLANG_ANALYZER_WITH_Z3
return llvm::make_unique<Z3ConstraintManager>(Eng, StMgr.getSValBuilder());
#else
- llvm::report_fatal_error("Clang was not compiled with Z3 support!", false);
+ llvm::report_fatal_error("Clang was not compiled with Z3 support, rebuild "
+ "with -DCLANG_ANALYZER_BUILD_Z3=ON",
+ false);
return nullptr;
#endif
}
Added: cfe/trunk/test/Analysis/apsint.c
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/test/Analysis/apsint.c?rev=333704&view=auto
==============================================================================
--- cfe/trunk/test/Analysis/apsint.c (added)
+++ cfe/trunk/test/Analysis/apsint.c Thu May 31 15:23:07 2018
@@ -0,0 +1,7 @@
+// REQUIRES: z3
+// RUN: %clang_analyze_cc1 -triple x86_64-unknown-linux-gnu -analyzer-checker=core -verify %s
+// expected-no-diagnostics
+
+_Bool a() {
+ return !({ a(); });
+}
More information about the cfe-commits
mailing list