Author: mramalho Date: Tue Jul 17 10:40:34 2018 New Revision: 337304 URL: http://llvm.org/viewvc/llvm-project?rev=337304&view=rev Log: [analyzer] Fix Z3 backend after D48205
Summary: An assertion was added in D48205 to catch places where a `nonloc::SymbolVal` was wrapping a `loc` object. This patch fixes that in the Z3 backend by making the `SValBuilder` object accessible from inherited instances of `SimpleConstraintManager` and calling `SVB.makeSymbolVal(foo)` instead of `nonloc::SymbolVal(foo)`. Reviewers: NoQ, george.karpenkov Reviewed By: NoQ Subscribers: xazax.hun, szepet, a.sidorin Differential Revision: https://reviews.llvm.org/D49430 Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h?rev=337304&r1=337303&r2=337304&view=diff ============================================================================== --- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h (original) +++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h Tue Jul 17 10:40:34 2018 @@ -75,6 +75,7 @@ protected: // Internal implementation. //===------------------------------------------------------------------===// + SValBuilder &getSValBuilder() const { return SVB; } BasicValueFactory &getBasicVals() const { return SVB.getBasicValueFactory(); } SymbolManager &getSymbolManager() const { return SVB.getSymbolManager(); } Modified: cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp?rev=337304&r1=337303&r2=337304&view=diff ============================================================================== --- cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp (original) +++ cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Tue Jul 17 10:40:34 2018 @@ -1077,40 +1077,39 @@ bool Z3ConstraintManager::canReasonAbout return true; const SymExpr *Sym = SymVal->getSymbol(); - do { - QualType Ty = Sym->getType(); + QualType Ty = Sym->getType(); - // Complex types are not modeled - if (Ty->isComplexType() || Ty->isComplexIntegerType()) - return false; - - // Non-IEEE 754 floating-point types are not modeled - if ((Ty->isSpecificBuiltinType(BuiltinType::LongDouble) && - (&TI.getLongDoubleFormat() == &llvm::APFloat::x87DoubleExtended() || - &TI.getLongDoubleFormat() == &llvm::APFloat::PPCDoubleDouble()))) - return false; - - if (isa<SymbolData>(Sym)) { - break; - } else if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) { - Sym = SC->getOperand(); - } else if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) { - if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) { - Sym = SIE->getLHS(); - } else if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) { - Sym = ISE->getRHS(); - } else if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) { - return canReasonAbout(nonloc::SymbolVal(SSM->getLHS())) && - canReasonAbout(nonloc::SymbolVal(SSM->getRHS())); - } else { - llvm_unreachable("Unsupported binary expression to reason about!"); - } - } else { - llvm_unreachable("Unsupported expression to reason about!"); - } - } while (Sym); + // Complex types are not modeled + if (Ty->isComplexType() || Ty->isComplexIntegerType()) + return false; + + // Non-IEEE 754 floating-point types are not modeled + if ((Ty->isSpecificBuiltinType(BuiltinType::LongDouble) && + (&TI.getLongDoubleFormat() == &llvm::APFloat::x87DoubleExtended() || + &TI.getLongDoubleFormat() == &llvm::APFloat::PPCDoubleDouble()))) + return false; - return true; + if (isa<SymbolData>(Sym)) + return true; + + SValBuilder &SVB = getSValBuilder(); + + if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) + return canReasonAbout(SVB.makeSymbolVal(SC->getOperand())); + + if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) { + if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) + return canReasonAbout(SVB.makeSymbolVal(SIE->getLHS())); + + if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) + return canReasonAbout(SVB.makeSymbolVal(ISE->getRHS())); + + if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(BSE)) + return canReasonAbout(SVB.makeSymbolVal(SSE->getLHS())) && + canReasonAbout(SVB.makeSymbolVal(SSE->getRHS())); + } + + llvm_unreachable("Unsupported expression to reason about!"); } ConditionTruthVal Z3ConstraintManager::checkNull(ProgramStateRef State, _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
