From: Mikhail R. Gadelha Date: Tue, 17 Jul 2018 17:40:34 +0000 (+0000) Subject: [analyzer] Fix Z3 backend after D48205 X-Git-Tag: llvmorg-7.0.0-rc1~1223 X-Git-Url: http://review.tizen.org/git/?a=commitdiff_plain;h=81943b805b41f921fe97acbb2db2592ee05e76da;p=platform%2Fupstream%2Fllvm.git [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 llvm-svn: 337304 --- diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h index db6b8c0..d64b90e 100644 --- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h +++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h @@ -75,6 +75,7 @@ protected: // Internal implementation. //===------------------------------------------------------------------===// + SValBuilder &getSValBuilder() const { return SVB; } BasicValueFactory &getBasicVals() const { return SVB.getBasicValueFactory(); } SymbolManager &getSymbolManager() const { return SVB.getSymbolManager(); } diff --git a/clang/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp b/clang/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp index 721e177..66a6cf5 100644 --- a/clang/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp +++ b/clang/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp @@ -1077,40 +1077,39 @@ bool Z3ConstraintManager::canReasonAbout(SVal X) const { 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; + // 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; + // 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(Sym)) { - break; - } else if (const SymbolCast *SC = dyn_cast(Sym)) { - Sym = SC->getOperand(); - } else if (const BinarySymExpr *BSE = dyn_cast(Sym)) { - if (const SymIntExpr *SIE = dyn_cast(BSE)) { - Sym = SIE->getLHS(); - } else if (const IntSymExpr *ISE = dyn_cast(BSE)) { - Sym = ISE->getRHS(); - } else if (const SymSymExpr *SSM = dyn_cast(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); + if (isa(Sym)) + return true; + + SValBuilder &SVB = getSValBuilder(); + + if (const SymbolCast *SC = dyn_cast(Sym)) + return canReasonAbout(SVB.makeSymbolVal(SC->getOperand())); + + if (const BinarySymExpr *BSE = dyn_cast(Sym)) { + if (const SymIntExpr *SIE = dyn_cast(BSE)) + return canReasonAbout(SVB.makeSymbolVal(SIE->getLHS())); + + if (const IntSymExpr *ISE = dyn_cast(BSE)) + return canReasonAbout(SVB.makeSymbolVal(ISE->getRHS())); + + if (const SymSymExpr *SSE = dyn_cast(BSE)) + return canReasonAbout(SVB.makeSymbolVal(SSE->getLHS())) && + canReasonAbout(SVB.makeSymbolVal(SSE->getRHS())); + } - return true; + llvm_unreachable("Unsupported expression to reason about!"); } ConditionTruthVal Z3ConstraintManager::checkNull(ProgramStateRef State,