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(); }); +} _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits