Index: clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h =================================================================== --- clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h +++ clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h @@ -174,6 +174,11 @@ return checkNull(State, Sym); } + /// canReasonAboutSymbolicExtTrunc - Not all ConstraintManagers can reason + /// symbolic extension and truncation. Used this to ask directly when + /// building SVals. + virtual bool canReasonAboutSymbolicExtTrunc() const = 0; + protected: /// A flag to indicate that clients should be notified of assumptions. /// By default this is the case, but sometimes this needs to be restricted Index: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h =================================================================== --- clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h +++ clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h @@ -288,6 +288,10 @@ llvm_unreachable("Unsupported expression to reason about!"); } + bool canReasonAboutSymbolicExtTrunc() const override { + return Solver->isExtTruncSupported(); + } + /// Dumps SMT formula LLVM_DUMP_METHOD void dump() const { Solver->dump(); } Index: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h =================================================================== --- clang/include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h +++ clang/include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h @@ -90,16 +90,8 @@ virtual ~SValBuilder() = default; - bool haveSameType(const SymExpr *Sym1, const SymExpr *Sym2) { - return haveSameType(Sym1->getType(), Sym2->getType()); - } - bool haveSameType(QualType Ty1, QualType Ty2) { - // FIXME: Remove the second disjunct when we support symbolic - // truncation/extension. - return (Context.getCanonicalType(Ty1) == Context.getCanonicalType(Ty2) || - (Ty1->isIntegralOrEnumerationType() && - Ty2->isIntegralOrEnumerationType())); + return (Context.getCanonicalType(Ty1) == Context.getCanonicalType(Ty2)); } SVal evalCast(SVal val, QualType castTy, QualType originalType); Index: clang/lib/StaticAnalyzer/Core/ProgramState.cpp =================================================================== --- clang/lib/StaticAnalyzer/Core/ProgramState.cpp +++ clang/lib/StaticAnalyzer/Core/ProgramState.cpp @@ -267,12 +267,12 @@ // to the type of T, which is not always the case (e.g. for void). if (!T.isNull() && (T->isIntegralOrEnumerationType() || Loc::isLocType(T))) { if (SymbolRef sym = V.getAsSymbol()) { - if (const llvm::APSInt *Int = getStateManager() - .getConstraintManager() - .getSymVal(this, sym)) { + ConstraintManager &CM = getStateManager().getConstraintManager(); + + if (const llvm::APSInt *Int = CM.getSymVal(this, sym)) { // FIXME: Because we don't correctly model (yet) sign-extension // and truncation of symbolic values, we need to convert - // the integer value to the correct signedness and bitwidth. + // the integer value to the correct signedness and // // This shows up in the following: // @@ -284,12 +284,13 @@ // The symbolic value stored to 'x' is actually the conjured // symbol for the call to foo(); the type of that symbol is 'char', // not unsigned. - const llvm::APSInt &NewV = getBasicVals().Convert(T, *Int); + if (!CM.canReasonAboutSymbolicExtTrunc()) + Int = &getBasicVals().Convert(T, *Int); if (V.getAs()) - return loc::ConcreteInt(NewV); + return loc::ConcreteInt(*Int); else - return nonloc::ConcreteInt(NewV); + return nonloc::ConcreteInt(*Int); } } } Index: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp =================================================================== --- clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp +++ clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp @@ -254,6 +254,8 @@ bool canReasonAbout(SVal X) const override; + bool canReasonAboutSymbolicExtTrunc() const override; + ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym) override; const llvm::APSInt *getSymVal(ProgramStateRef State, @@ -379,6 +381,10 @@ return true; } +bool RangeConstraintManager::canReasonAboutSymbolicExtTrunc() const { + return false; +} + ConditionTruthVal RangeConstraintManager::checkNull(ProgramStateRef State, SymbolRef Sym) { const RangeSet *Ranges = State->get(Sym); Index: clang/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp =================================================================== --- clang/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp +++ clang/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp @@ -120,7 +120,8 @@ case nonloc::ConcreteIntKind: { const llvm::APSInt &IntVal = Value.castAs().getValue(); - bool IsInRange = IntVal >= From && IntVal <= To; + bool IsInRange = llvm::APSInt::compareValues(IntVal, From) != -1 && + llvm::APSInt::compareValues(IntVal, To) != 1; bool isFeasible = (IsInRange == InRange); return isFeasible ? State : nullptr; } Index: clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp =================================================================== --- clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp +++ clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp @@ -72,6 +72,8 @@ } SVal SimpleSValBuilder::evalCastFromNonLoc(NonLoc val, QualType castTy) { + ConstraintManager &CM = getStateManager().getConstraintManager(); + bool isLocType = Loc::isLocType(castTy); if (val.getAs()) return val; @@ -79,28 +81,37 @@ if (Optional LI = val.getAs()) { if (isLocType) return LI->getLoc(); + // FIXME: Correctly support promotions/truncations. - unsigned castSize = Context.getIntWidth(castTy); - if (castSize == LI->getNumBits()) + unsigned castSize = Context.getTypeSize(castTy); + if (!CM.canReasonAboutSymbolicExtTrunc() && castSize == LI->getNumBits()) return val; + return makeLocAsInteger(LI->getLoc(), castSize); } if (const SymExpr *se = val.getAsSymbolicExpression()) { QualType T = Context.getCanonicalType(se->getType()); - // If types are the same or both are integers, ignore the cast. + // If types are the same, ignore the cast. + if (haveSameType(T, castTy)) + return val; + + // If types are both integers, ignore the cast. // FIXME: Remove this hack when we support symbolic truncation/extension. // HACK: If both castTy and T are integers, ignore the cast. This is // not a permanent solution. Eventually we want to precisely handle // extension/truncation of symbolic integers. This prevents us from losing // precision when we assign 'x = y' and 'y' is symbolic and x and y are // different integer types. - if (haveSameType(T, castTy)) + if (!CM.canReasonAboutSymbolicExtTrunc() && + (T->isIntegralOrEnumerationType() && + castTy->isIntegralOrEnumerationType())) return val; - if (!isLocType) - return makeNonLoc(se, T, castTy); - return UnknownVal(); + if (isLocType) + return UnknownVal(); + + return makeNonLoc(se, T, castTy); } // If value is a non-integer constant, produce unknown. Index: clang/lib/StaticAnalyzer/Core/Store.cpp =================================================================== --- clang/lib/StaticAnalyzer/Core/Store.cpp +++ clang/lib/StaticAnalyzer/Core/Store.cpp @@ -532,7 +532,9 @@ elementType, Offset, cast(ElemR->getSuperRegion()), Ctx)); } - const llvm::APSInt& OffI = Offset.castAs().getValue(); + // FIXME: This isn't quite correct, but avoids casting the Offset symbol + llvm::APSInt OffI = APSIntType(BaseIdxI).convert( + Offset.castAs().getValue()); assert(BaseIdxI.isSigned()); // Compute the new index. Index: llvm/include/llvm/Support/SMTAPI.h =================================================================== --- llvm/include/llvm/Support/SMTAPI.h +++ llvm/include/llvm/Support/SMTAPI.h @@ -433,6 +433,9 @@ /// Checks if the solver supports floating-points. virtual bool isFPSupported() = 0; + /// Checks if the solver supports extension/truncation. + virtual bool isExtTruncSupported() = 0; + virtual void print(raw_ostream &OS) const = 0; }; Index: llvm/lib/Support/Z3Solver.cpp =================================================================== --- llvm/lib/Support/Z3Solver.cpp +++ llvm/lib/Support/Z3Solver.cpp @@ -872,6 +872,8 @@ bool isFPSupported() override { return true; } + bool isExtTruncSupported() override { return true; } + /// Reset the solver and remove all constraints. void reset() override { Z3_solver_reset(Context.Context, Solver); }