ddcc updated this revision to Diff 99522.
ddcc added a comment.
Herald added a subscriber: eraman.
Rebase, avoid generating floating-point constraints if unsupported by
constraint manager
https://reviews.llvm.org/D28954
Files:
include/clang/StaticAnalyzer/Checkers/Checkers.td
include/clang/StaticAnalyzer/Core/PathSensitive/BasicValueFactory.h
include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h
include/clang/StaticAnalyzer/Core/PathSensitive/SVals.def
include/clang/StaticAnalyzer/Core/PathSensitive/SVals.h
include/clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h
include/clang/StaticAnalyzer/Core/PathSensitive/Symbols.def
lib/StaticAnalyzer/Checkers/BuiltinFunctionChecker.cpp
lib/StaticAnalyzer/Checkers/CMakeLists.txt
lib/StaticAnalyzer/Checkers/FloatingPointMath.cpp
lib/StaticAnalyzer/Core/BasicValueFactory.cpp
lib/StaticAnalyzer/Core/Environment.cpp
lib/StaticAnalyzer/Core/ProgramState.cpp
lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
lib/StaticAnalyzer/Core/RegionStore.cpp
lib/StaticAnalyzer/Core/SValBuilder.cpp
lib/StaticAnalyzer/Core/SVals.cpp
lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
lib/StaticAnalyzer/Core/SymbolManager.cpp
lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
test/Analysis/diagnostics/macros.cpp
test/Analysis/float-rules.c
test/Analysis/float.c
test/Analysis/inline.cpp
test/Analysis/operator-calls.cpp
Index: test/Analysis/operator-calls.cpp
===================================================================
--- test/Analysis/operator-calls.cpp
+++ test/Analysis/operator-calls.cpp
@@ -81,8 +81,8 @@
void test(int coin) {
// Force a cache-out when we try to conjure a temporary region for the operator call.
// ...then, don't crash.
- clang_analyzer_eval(+(coin ? getSmallOpaque() : getSmallOpaque())); // expected-warning{{UNKNOWN}}
- clang_analyzer_eval(+(coin ? getLargeOpaque() : getLargeOpaque())); // expected-warning{{UNKNOWN}}
+ clang_analyzer_eval(+(coin ? getSmallOpaque() : getSmallOpaque())); // expected-warning{{TRUE}}
+ clang_analyzer_eval(+(coin ? getLargeOpaque() : getLargeOpaque())); // expected-warning{{TRUE}}
}
}
Index: test/Analysis/inline.cpp
===================================================================
--- test/Analysis/inline.cpp
+++ test/Analysis/inline.cpp
@@ -285,11 +285,11 @@
}
void testFloatReference() {
- clang_analyzer_eval(defaultFloatReference(1) == -1); // expected-warning{{UNKNOWN}}
- clang_analyzer_eval(defaultFloatReference() == -42); // expected-warning{{UNKNOWN}}
+ clang_analyzer_eval(defaultFloatReference(1) == -1); // expected-warning{{TRUE}}
+ clang_analyzer_eval(defaultFloatReference() == -42); // expected-warning{{TRUE}}
- clang_analyzer_eval(defaultFloatReferenceZero(1) == -1); // expected-warning{{UNKNOWN}}
- clang_analyzer_eval(defaultFloatReferenceZero() == 0); // expected-warning{{UNKNOWN}}
+ clang_analyzer_eval(defaultFloatReferenceZero(1) == -1); // expected-warning{{TRUE}}
+ clang_analyzer_eval(defaultFloatReferenceZero() == 0); // expected-warning{{TRUE}}
}
char defaultString(const char *s = "abc") {
Index: test/Analysis/float.c
===================================================================
--- /dev/null
+++ test/Analysis/float.c
@@ -0,0 +1,83 @@
+// RUN: %clang_analyze_cc1 -analyzer-checker=core.builtin,debug.ExprInspection -verify %s
+// REQUIRES: z3
+
+void clang_analyzer_eval(int);
+
+void float1() {
+ float z1 = 0.0, z2 = -0.0;
+ clang_analyzer_eval(z1 == z2); // expected-warning{{TRUE}}
+}
+
+void float2(float a, float b) {
+ clang_analyzer_eval(a == b); // expected-warning{{UNKNOWN}}
+ clang_analyzer_eval(a != b); // expected-warning{{UNKNOWN}}
+}
+
+void float3(float a, float b) {
+ if (__builtin_isnan(a) || __builtin_isnan(b) || a < b) {
+ clang_analyzer_eval(a > b); // expected-warning{{FALSE}}
+ clang_analyzer_eval(a == b); // expected-warning{{FALSE}}
+ return;
+ }
+ clang_analyzer_eval(a >= b); // expected-warning{{TRUE}}
+ clang_analyzer_eval(a == b); // expected-warning{{UNKNOWN}}
+}
+
+void float4(float a) {
+ if (__builtin_isnan(a) || a < 0.0f)
+ return;
+ clang_analyzer_eval(a >= 0.0Q); // expected-warning{{TRUE}}
+ clang_analyzer_eval(a >= 0.0F); // expected-warning{{TRUE}}
+ clang_analyzer_eval(a >= 0.0); // expected-warning{{TRUE}}
+ clang_analyzer_eval(a >= 0); // expected-warning{{TRUE}}
+}
+
+void float5() {
+ double value = 1.0;
+ double pinf = __builtin_inf();
+ double ninf = -__builtin_inf();
+ double nan = __builtin_nan("");
+
+ /* NaN */
+ clang_analyzer_eval(__builtin_isnan(value)); // expected-warning{{FALSE}}
+ clang_analyzer_eval(__builtin_isnan(nan)); // expected-warning{{TRUE}}
+
+ clang_analyzer_eval(__builtin_isnan(0.0 / 0.0)); // expected-warning{{TRUE}}
+ clang_analyzer_eval(__builtin_isnan(pinf / ninf)); // expected-warning{{TRUE}}
+ clang_analyzer_eval(__builtin_isnan(pinf / pinf)); // expected-warning{{TRUE}}
+ clang_analyzer_eval(__builtin_isnan(ninf / pinf)); // expected-warning{{TRUE}}
+ clang_analyzer_eval(__builtin_isnan(ninf / ninf)); // expected-warning{{TRUE}}
+
+ clang_analyzer_eval(__builtin_isnan(0.0 * ninf)); // expected-warning{{TRUE}}
+ clang_analyzer_eval(__builtin_isnan(0.0 * pinf)); // expected-warning{{TRUE}}
+ clang_analyzer_eval(__builtin_isnan(ninf * 0.0)); // expected-warning{{TRUE}}
+ clang_analyzer_eval(__builtin_isnan(pinf * 0.0)); // expected-warning{{TRUE}}
+
+ clang_analyzer_eval(__builtin_isnan(nan + value)); // expected-warning{{TRUE}}
+ clang_analyzer_eval(__builtin_isnan(value - nan)); // expected-warning{{TRUE}}
+ clang_analyzer_eval(__builtin_isnan(nan * value)); // expected-warning{{TRUE}}
+ clang_analyzer_eval(__builtin_isnan(value / nan)); // expected-warning{{TRUE}}
+
+ /* Infinity */
+ clang_analyzer_eval(__builtin_isinf(value)); // expected-warning{{FALSE}}
+ clang_analyzer_eval(__builtin_isinf(pinf)); // expected-warning{{TRUE}}
+ clang_analyzer_eval(__builtin_isinf(ninf)); // expected-warning{{TRUE}}
+ clang_analyzer_eval(1.0 / pinf == 0.0); // expected-warning{{TRUE}}
+ clang_analyzer_eval(1.0 / ninf == 0.0); // expected-warning{{TRUE}}
+
+ /* Zero */
+ clang_analyzer_eval(0.0 == -0.0); // expected-warning{{TRUE}}
+}
+
+void mixed() {
+ clang_analyzer_eval(0.0 * 0 == 0.0); // expected-warning{{TRUE}}
+ clang_analyzer_eval(1.0 * 0 == 0.0); // expected-warning{{TRUE}}
+ clang_analyzer_eval(1.0 * 1 == 1.0); // expected-warning{{TRUE}}
+ clang_analyzer_eval((5 * 5) * 1.0 == 25); // expected-warning{{TRUE}}
+}
+
+void nan1(double a) {
+ if (a == a)
+ return;
+ clang_analyzer_eval(__builtin_isnan(a)); // expected-warning{{TRUE}}
+}
Index: test/Analysis/float-rules.c
===================================================================
--- /dev/null
+++ test/Analysis/float-rules.c
@@ -0,0 +1,107 @@
+// RUN: %clang_analyze_cc1 -analyzer-checker=core.builtin,alpha.core.FPMath,debug.ExprInspection -verify %s
+// REQUIRES: z3
+
+double acos(double x);
+double asin(double x);
+double acosh(double x);
+double atanh(double x);
+double log(double x);
+double log2(double x);
+double log10(double x);
+double log1p(double x);
+double logb(double x);
+double sqrt(double x);
+double fmod(double x, double y);
+double remainder(double x, double y);
+
+double domain1() {
+ double nan = __builtin_nan("");
+ double z = 0.0;
+
+ // -1 <= x <= 1
+ z = acos(-5.0); // expected-warning{{Argument value is out of valid domain for function call}}
+ z = acos(5.0); // expected-warning{{Argument value is out of valid domain for function call}}
+ z = acos(0.0); // no-warning
+ z = acos(nan); // no-warning
+ z = asin(-5.0); // expected-warning{{Argument value is out of valid domain for function call}}
+ z = asin(5.0); // expected-warning{{Argument value is out of valid domain for function call}}
+ z = asin(0.0); // no-warning
+ z = asin(nan); // no-warning
+
+ // x >= 1
+ z = acosh(-5.0); // expected-warning{{Argument value is out of valid domain for function call}}
+ z = acosh(-1.0); // expected-warning{{Argument value is out of valid domain for function call}}
+ z = acosh(0.0); // expected-warning{{Argument value is out of valid domain for function call}}
+ z = acosh(1.0); // no-warning
+ z = acosh(nan); // no-warning
+
+ // -1 < x < 1
+ z = atanh(-1.0); // expected-warning{{Argument value is out of valid domain for function call}}
+ z = atanh(1.0); // expected-warning{{Argument value is out of valid domain for function call}}
+ z = atanh(0.0); // no-warning
+ z = atanh(nan); // no-warning
+
+ // x >= 0
+ z = log(-1.0); // expected-warning{{Argument value is out of valid domain for function call}}
+ z = log(-0.5); // expected-warning{{Argument value is out of valid domain for function call}}
+ z = log(0.0); // no-warning
+ z = log(nan); // no-warning
+ z = log2(-1.0); // expected-warning{{Argument value is out of valid domain for function call}}
+ z = log2(-0.5); // expected-warning{{Argument value is out of valid domain for function call}}
+ z = log2(0.0); // no-warning
+ z = log2(nan); // no-warning
+ z = log10(-1.0); // expected-warning{{Argument value is out of valid domain for function call}}
+ z = log10(-0.5); // expected-warning{{Argument value is out of valid domain for function call}}
+ z = log10(0.0); // no-warning
+ z = log10(nan); // no-warning
+ z = sqrt(-1.0); // expected-warning{{Argument value is out of valid domain for function call}}
+ z = sqrt(-0.5); // expected-warning{{Argument value is out of valid domain for function call}}
+ z = sqrt(0.0); // no-warning
+ z = sqrt(nan); // no-warning
+
+ // x >= -1
+ z = log1p(-5.0); // expected-warning{{Argument value is out of valid domain for function call}}
+ z = log1p(-1.0); // no-warning
+ z = log1p(0.0); // no-warning
+ z = log1p(nan); // no-warning
+
+ // x != 0
+ z = logb(0.0); // expected-warning{{Argument value is out of valid domain for function call}}
+ z = logb(-1.0); // no-warning
+ z = logb(1.0); // no-warning
+ z = logb(nan); // no-warning
+
+ return z;
+}
+
+double domain2(double x) {
+ double nan = __builtin_nan("");
+ double z = 0.0;
+
+ // y != 0
+ z = fmod(x, 0.0); // expected-warning{{Argument value is out of valid domain for function call}}
+ z = fmod(x, 1.0); // no-warning
+ z = fmod(x, -1.0); // no-warning
+ z = fmod(x, nan); // no-warning
+ z = remainder(x, 0.0); // expected-warning{{Argument value is out of valid domain for function call}}
+ z = remainder(x, 1.0); // no-warning
+ z = remainder(x, -1.0); // no-warning
+ z = remainder(x, nan); // no-warning
+
+ return z;
+}
+
+double domain3(double x) {
+ double z = 0.0;
+
+ if (__builtin_isnan(x) || x < 0)
+ return z;
+
+ z = acosh(x); // expected-warning{{Argument value is out of valid domain for function call}}
+ z = asin(x); // expected-warning{{Argument value is out of valid domain for function call}}
+ z = logb(x); // expected-warning{{Argument value is out of valid domain for function call}}
+ z = log1p(x); // no-warning
+ z = log(x); // no-warning
+
+ return z;
+}
Index: test/Analysis/diagnostics/macros.cpp
===================================================================
--- test/Analysis/diagnostics/macros.cpp
+++ test/Analysis/diagnostics/macros.cpp
@@ -30,8 +30,12 @@
// There are no path notes on the comparison to float types.
void testDoubleMacro(double d) {
+#ifdef ANALYZER_CM_Z3
+ if (d == DBL_MAX) { // expected-note {{Assuming 'd' is equal to DBL_MAX}}
+ // expected-note@-1 {{Taking true branch}}
+#else
if (d == DBL_MAX) { // expected-note {{Taking true branch}}
-
+#endif
char *p = NULL; // expected-note {{'p' initialized to a null pointer value}}
*p = 7; // expected-warning {{Dereference of null pointer (loaded from variable 'p')}}
// expected-note@-1 {{Dereference of null pointer (loaded from variable 'p')}}
Index: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
===================================================================
--- lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
+++ lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
@@ -904,11 +904,16 @@
bool canReasonAbout(SVal X) const override;
+ bool canReasonAboutFloat() const override;
+
ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym) override;
const llvm::APSInt *getSymVal(ProgramStateRef State,
SymbolRef Sym) const override;
+ const llvm::APFloat *getSymFloatVal(ProgramStateRef State,
+ SymbolRef Sym) const override;
+
ProgramStateRef removeDeadBindings(ProgramStateRef St,
SymbolReaper &SymReaper) override;
@@ -983,6 +988,10 @@
// Helper functions.
//===------------------------------------------------------------------===//
+ // Recover the QualType of an APFloat.
+ // TODO: Refactor to put elsewhere
+ QualType getAPFloatType(const llvm::APFloat &Float) const;
+
// Recover the QualType of an APSInt.
// TODO: Refactor to put elsewhere
QualType getAPSIntType(const llvm::APSInt &Int) const;
@@ -1008,6 +1017,11 @@
void doFloatTypeConversion(T &LHS, QualType <y, T &RHS,
QualType &RTy) const;
+ // Callback function for doCast parameter on APFloat type.
+ static llvm::APFloat castAPFloat(const llvm::APFloat &V, QualType ToTy,
+ uint64_t ToWidth, QualType FromTy,
+ uint64_t FromWidth);
+
// Callback function for doCast parameter on APSInt type.
static llvm::APSInt castAPSInt(const llvm::APSInt &V, QualType ToTy,
uint64_t ToWidth, QualType FromTy,
@@ -1106,6 +1120,10 @@
Sym = SIE->getLHS();
} else if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) {
Sym = ISE->getRHS();
+ } else if (const SymFloatExpr *SFE = dyn_cast<SymFloatExpr>(BSE)) {
+ Sym = SFE->getLHS();
+ } else if (const FloatSymExpr *FSE = dyn_cast<FloatSymExpr>(BSE)) {
+ Sym = FSE->getRHS();
} else if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {
return canReasonAbout(nonloc::SymbolVal(SSM->getLHS())) &&
canReasonAbout(nonloc::SymbolVal(SSM->getRHS()));
@@ -1120,6 +1138,10 @@
return true;
}
+bool Z3ConstraintManager::canReasonAboutFloat() const {
+ return true;
+}
+
ConditionTruthVal Z3ConstraintManager::checkNull(ProgramStateRef State,
SymbolRef Sym) {
QualType RetTy;
@@ -1151,6 +1173,8 @@
return ConditionTruthVal();
}
+// TODO: Merge implementation of getSymVal() and getSymFloatVal() into one
+// templated function, to avoid weird corner cases when casting back and forth
const llvm::APSInt *Z3ConstraintManager::getSymVal(ProgramStateRef State,
SymbolRef Sym) const {
BasicValueFactory &BV = getBasicVals();
@@ -1196,11 +1220,45 @@
if (CastTy->isVoidType())
return nullptr;
- const llvm::APSInt *Value;
- if (!(Value = getSymVal(State, CastSym)))
- return nullptr;
- return &BV.Convert(SC->getType(), *Value);
+ // Call the other getSym*Val() function depending on expression type
+ if (CastSym->getType()->isRealFloatingType()) {
+ const llvm::APFloat *Float = getSymFloatVal(State, CastSym);
+ assert(!CastTy->isRealFloatingType());
+ llvm::APSInt Int(Ctx.getTypeSize(CastTy),
+ !CastTy->isSignedIntegerOrEnumerationType());
+ if (!Float || !BasicValueFactory::Convert(Int, *Float))
+ return nullptr;
+ return &BV.getValue(Int);
+ } else {
+ const llvm::APSInt *Value;
+ if (!(Value = getSymVal(State, CastSym)))
+ return nullptr;
+ return &BV.Convert(CastTy, *Value);
+ }
} else if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
+ // Floating-point comparisons produce an integral result
+ if ((isa<FloatSymExpr>(BSE) || isa<SymFloatExpr>(BSE)) &&
+ BinaryOperator::isComparisonOp(BSE->getOpcode())) {
+ const llvm::APFloat *LHS, *RHS;
+ if (const FloatSymExpr *FSE = dyn_cast<FloatSymExpr>(BSE)) {
+ LHS = &FSE->getLHS();
+ RHS = getSymFloatVal(State, FSE->getRHS());
+ } else if (const SymFloatExpr *SFE = dyn_cast<SymFloatExpr>(BSE)) {
+ LHS = getSymFloatVal(State, SFE->getLHS());
+ RHS = &SFE->getRHS();
+ }
+
+ if (!LHS || !RHS)
+ return nullptr;
+
+ llvm::APFloat ConvertedLHS = *LHS, ConvertedRHS = *RHS;
+ QualType LTy = getAPFloatType(*LHS), RTy = getAPFloatType(*RHS);
+ doFloatTypeConversion<llvm::APFloat, Z3ConstraintManager::castAPFloat>(
+ ConvertedLHS, LTy, ConvertedRHS, RTy);
+ return BV.evalAPFloatComparison(BSE->getOpcode(), ConvertedLHS,
+ ConvertedRHS);
+ }
+
const llvm::APSInt *LHS, *RHS;
if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
LHS = getSymVal(State, SIE->getLHS());
@@ -1229,6 +1287,92 @@
llvm_unreachable("Unsupported expression to get symbol value!");
}
+const llvm::APFloat *Z3ConstraintManager::getSymFloatVal(ProgramStateRef State,
+ SymbolRef Sym) const {
+ BasicValueFactory &BV = getBasicVals();
+ ASTContext &Ctx = BV.getContext();
+
+ if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) {
+ QualType Ty = Sym->getType();
+ assert(Ty->isRealFloatingType());
+ llvm::APFloat Value(Ctx.getFloatTypeSemantics(Ty));
+
+ Z3Expr Exp = getZ3DataExpr(SD->getSymbolID(), Ty);
+
+ Solver.reset();
+ Solver.addStateConstraints(State);
+
+ // Constraints are unsatisfiable
+ if (Solver.check() != Z3_L_TRUE)
+ return nullptr;
+
+ Z3Model Model = Solver.getModel();
+ // Model does not assign interpretation
+ if (!Model.getInterpretation(Exp, Value))
+ return nullptr;
+
+ // A value has been obtained, check if it is the only value
+ Z3Expr NotExp =
+ Z3Expr::fromFloatBinOp(Exp, BO_NE, Z3Expr::fromAPFloat(Value));
+
+ Solver.addConstraint(NotExp);
+ if (Solver.check() == Z3_L_TRUE)
+ return nullptr;
+
+ // This is the only solution, store it
+ return &BV.getValue(Value);
+ } else if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) {
+ SymbolRef CastSym = SC->getOperand();
+ QualType CastTy = SC->getType();
+ // Skip the void type
+ if (CastTy->isVoidType())
+ return nullptr;
+
+ // Call the other getSym*Val() function depending on expression type
+ if (!CastSym->getType()->isRealFloatingType()) {
+ const llvm::APSInt *Int = getSymVal(State, CastSym);
+ assert(CastTy->isRealFloatingType());
+ llvm::APFloat Float(Ctx.getFloatTypeSemantics(CastTy));
+ if (!Int || !BasicValueFactory::Convert(Float, *Int))
+ return nullptr;
+ return &BV.getValue(Float);
+ } else {
+ const llvm::APFloat *Value;
+ if (!(Value = getSymFloatVal(State, CastSym)))
+ return nullptr;
+ return &BV.Convert(CastTy, *Value);
+ }
+ } else if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
+ const llvm::APFloat *LHS, *RHS;
+ if (const SymFloatExpr *SIE = dyn_cast<SymFloatExpr>(BSE)) {
+ LHS = getSymFloatVal(State, SIE->getLHS());
+ RHS = &SIE->getRHS();
+ } else if (const FloatSymExpr *ISE = dyn_cast<FloatSymExpr>(BSE)) {
+ LHS = &ISE->getLHS();
+ RHS = getSymFloatVal(State, ISE->getRHS());
+ } else if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {
+ // Early termination to avoid expensive call
+ LHS = getSymFloatVal(State, SSM->getLHS());
+ RHS = LHS ? getSymFloatVal(State, SSM->getRHS()) : nullptr;
+ } else {
+ llvm_unreachable("Unsupported binary expression to get symbol value!");
+ }
+
+ if (!LHS || !RHS)
+ return nullptr;
+
+ llvm::APFloat ConvertedLHS = *LHS, ConvertedRHS = *RHS;
+ QualType LTy = getAPFloatType(*LHS), RTy = getAPFloatType(*RHS);
+ doFloatTypeConversion<llvm::APFloat, Z3ConstraintManager::castAPFloat>(
+ ConvertedLHS, LTy, ConvertedRHS, RTy);
+ return BV.evalAPFloat(BSE->getOpcode(), ConvertedLHS, ConvertedRHS);
+ } else {
+ llvm_unreachable("Unsupported expression to get symbol value!");
+ }
+
+ return nullptr;
+}
+
ProgramStateRef
Z3ConstraintManager::removeDeadBindings(ProgramStateRef State,
SymbolReaper &SymReaper) {
@@ -1359,6 +1503,16 @@
Z3Expr LHS = Z3Expr::fromAPSInt(ISE->getLHS());
Z3Expr RHS = getZ3SymExpr(ISE->getRHS(), &RTy, hasComparison);
return getZ3BinExpr(LHS, LTy, Op, RHS, RTy, RetTy);
+ } else if (const SymFloatExpr *SFE = dyn_cast<SymFloatExpr>(BSE)) {
+ RTy = getAPFloatType(SFE->getRHS());
+ Z3Expr LHS = getZ3SymExpr(SFE->getLHS(), <y, hasComparison);
+ Z3Expr RHS = Z3Expr::fromAPFloat(SFE->getRHS());
+ return getZ3BinExpr(LHS, LTy, Op, RHS, RTy, RetTy);
+ } else if (const FloatSymExpr *FSE = dyn_cast<FloatSymExpr>(BSE)) {
+ LTy = getAPFloatType(FSE->getLHS());
+ Z3Expr LHS = Z3Expr::fromAPFloat(FSE->getLHS());
+ Z3Expr RHS = getZ3SymExpr(FSE->getRHS(), &RTy, hasComparison);
+ return getZ3BinExpr(LHS, LTy, Op, RHS, RTy, RetTy);
} else if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {
Z3Expr LHS = getZ3SymExpr(SSM->getLHS(), <y, hasComparison);
Z3Expr RHS = getZ3SymExpr(SSM->getRHS(), &RTy, hasComparison);
@@ -1405,6 +1559,12 @@
// Helper functions.
//===------------------------------------------------------------------===//
+QualType Z3ConstraintManager::getAPFloatType(const llvm::APFloat &Float) const {
+ ASTContext &Ctx = getBasicVals().getContext();
+ return Ctx.getRealTypeForBitwidth(
+ llvm::APFloat::getSizeInBits(Float.getSemantics()));
+}
+
QualType Z3ConstraintManager::getAPSIntType(const llvm::APSInt &Int) const {
ASTContext &Ctx = getBasicVals().getContext();
return Ctx.getIntTypeForBitwidth(Int.getBitWidth(), Int.isSigned());
@@ -1579,16 +1739,34 @@
// Note: Safe to skip updating bitwidth because this must terminate
int order = Ctx.getFloatingTypeOrder(LTy, RTy);
if (order > 0) {
- RHS = Z3Expr::fromCast(RHS, LTy, LBitWidth, RTy, RBitWidth);
+ RHS = (*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);
RTy = LTy;
} else if (order == 0) {
- LHS = Z3Expr::fromCast(LHS, RTy, RBitWidth, LTy, LBitWidth);
+ LHS = (*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth);
LTy = RTy;
} else {
llvm_unreachable("Unsupported floating-point type cast!");
}
}
+llvm::APFloat Z3ConstraintManager::castAPFloat(const llvm::APFloat &V,
+ QualType ToTy, uint64_t ToWidth,
+ QualType FromTy,
+ uint64_t FromWidth) {
+ bool lossOfPrecision;
+ llvm::APFloat To = V;
+#ifndef NDEBUG
+ llvm::APFloat::opStatus Status =
+ To.convert(Z3Expr::getFloatSemantics(ToWidth),
+ llvm::APFloat::rmNearestTiesToEven, &lossOfPrecision);
+#else
+ To.convert(Z3Expr::getFloatSemantics(ToWidth),
+ llvm::APFloat::rmNearestTiesToEven, &lossOfPrecision);
+#endif
+ assert(!(Status & (llvm::APFloat::opOverflow | llvm::APFloat::opInvalidOp)));
+ return To;
+}
+
llvm::APSInt Z3ConstraintManager::castAPSInt(const llvm::APSInt &V,
QualType ToTy, uint64_t ToWidth,
QualType FromTy,
Index: lib/StaticAnalyzer/Core/SymbolManager.cpp
===================================================================
--- lib/StaticAnalyzer/Core/SymbolManager.cpp
+++ lib/StaticAnalyzer/Core/SymbolManager.cpp
@@ -48,6 +48,29 @@
os << ')';
}
+void SymFloatExpr::dumpToStream(raw_ostream &os) const {
+ SmallString<24> Chars;
+ getRHS().toString(Chars, 0, 0);
+
+ os << '(';
+ getLHS()->dumpToStream(os);
+ os << ") "
+ << BinaryOperator::getOpcodeStr(getOpcode()) << ' '
+ << Chars;
+}
+
+void FloatSymExpr::dumpToStream(raw_ostream &os) const {
+ SmallString<24> Chars;
+ getLHS().toString(Chars, 0, 0);
+
+ os << Chars
+ << ' '
+ << BinaryOperator::getOpcodeStr(getOpcode())
+ << " (";
+ getRHS()->dumpToStream(os);
+ os << ')';
+}
+
void SymSymExpr::dumpToStream(raw_ostream &os) const {
os << '(';
getLHS()->dumpToStream(os);
@@ -131,6 +154,12 @@
case SymExpr::IntSymExprKind:
itr.push_back(cast<IntSymExpr>(SE)->getRHS());
return;
+ case SymExpr::SymFloatExprKind:
+ itr.push_back(cast<SymFloatExpr>(SE)->getLHS());
+ return;
+ case SymExpr::FloatSymExprKind:
+ itr.push_back(cast<FloatSymExpr>(SE)->getRHS());
+ return;
case SymExpr::SymSymExprKind: {
const SymSymExpr *x = cast<SymSymExpr>(SE);
itr.push_back(x->getLHS());
@@ -288,6 +317,42 @@
return cast<IntSymExpr>(data);
}
+const SymFloatExpr *SymbolManager::getSymFloatExpr(const SymExpr *lhs,
+ BinaryOperator::Opcode op,
+ const llvm::APFloat& v,
+ QualType t) {
+ llvm::FoldingSetNodeID ID;
+ SymFloatExpr::Profile(ID, lhs, op, v, t);
+ void *InsertPos;
+ SymExpr *data = DataSet.FindNodeOrInsertPos(ID, InsertPos);
+
+ if (!data) {
+ data = (SymFloatExpr*) BPAlloc.Allocate<SymFloatExpr>();
+ new (data) SymFloatExpr(lhs, op, v, t);
+ DataSet.InsertNode(data, InsertPos);
+ }
+
+ return cast<SymFloatExpr>(data);
+}
+
+const FloatSymExpr *SymbolManager::getFloatSymExpr(const llvm::APFloat& lhs,
+ BinaryOperator::Opcode op,
+ const SymExpr *rhs,
+ QualType t) {
+ llvm::FoldingSetNodeID ID;
+ FloatSymExpr::Profile(ID, lhs, op, rhs, t);
+ void *InsertPos;
+ SymExpr *data = DataSet.FindNodeOrInsertPos(ID, InsertPos);
+
+ if (!data) {
+ data = (FloatSymExpr*) BPAlloc.Allocate<FloatSymExpr>();
+ new (data) FloatSymExpr(lhs, op, rhs, t);
+ DataSet.InsertNode(data, InsertPos);
+ }
+
+ return cast<FloatSymExpr>(data);
+}
+
const SymSymExpr *SymbolManager::getSymSymExpr(const SymExpr *lhs,
BinaryOperator::Opcode op,
const SymExpr *rhs,
@@ -340,6 +405,9 @@
if (T->isIntegralOrEnumerationType())
return true;
+ if (T->isRealFloatingType())
+ return true;
+
if (T->isRecordType() && !T->isUnionType())
return true;
@@ -484,6 +552,12 @@
case SymExpr::IntSymExprKind:
KnownLive = isLive(cast<IntSymExpr>(sym)->getRHS());
break;
+ case SymExpr::SymFloatExprKind:
+ KnownLive = isLive(cast<SymFloatExpr>(sym)->getLHS());
+ break;
+ case SymExpr::FloatSymExprKind:
+ KnownLive = isLive(cast<FloatSymExpr>(sym)->getRHS());
+ break;
case SymExpr::SymSymExprKind:
KnownLive = isLive(cast<SymSymExpr>(sym)->getLHS()) &&
isLive(cast<SymSymExpr>(sym)->getRHS());
Index: lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
===================================================================
--- lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
+++ lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
@@ -42,15 +42,23 @@
Loc lhs, NonLoc rhs, QualType resultTy) override;
/// getKnownValue - evaluates a given SVal. If the SVal has only one possible
- /// (integer) value, that value is returned. Otherwise, returns NULL.
+ /// integer value, that value is returned. Otherwise, returns NULL.
const llvm::APSInt *getKnownValue(ProgramStateRef state, SVal V) override;
+ /// Evaluates a given SVal. If the SVal has only one possible float value,
+ /// that value is returned. Otherwise, returns NULL.
+ const llvm::APFloat *getKnownFloatValue(ProgramStateRef state,
+ SVal val) override;
+
/// Recursively descends into symbolic expressions and replaces symbols
/// with their known values (in the sense of the getKnownValue() method).
SVal simplifySVal(ProgramStateRef State, SVal V) override;
SVal MakeSymIntVal(const SymExpr *LHS, BinaryOperator::Opcode op,
const llvm::APSInt &RHS, QualType resultTy);
+
+ SVal MakeSymFloatVal(const SymExpr *LHS, BinaryOperator::Opcode op,
+ const llvm::APFloat &RHS, QualType resultTy);
};
} // end anonymous namespace
@@ -67,7 +75,7 @@
SVal SimpleSValBuilder::dispatchCast(SVal Val, QualType CastTy) {
assert(Val.getAs<Loc>() || Val.getAs<NonLoc>());
return Val.getAs<Loc>() ? evalCastFromLoc(Val.castAs<Loc>(), CastTy)
- : evalCastFromNonLoc(Val.castAs<NonLoc>(), CastTy);
+ : evalCastFromNonLoc(Val.castAs<NonLoc>(), CastTy);
}
SVal SimpleSValBuilder::evalCastFromNonLoc(NonLoc val, QualType castTy) {
@@ -97,36 +105,84 @@
// 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 (haveSameType(T, castTy))
return val;
if (!isLocType)
return makeNonLoc(se, T, castTy);
return UnknownVal();
}
- // If value is a non-integer constant, produce unknown.
- if (!val.getAs<nonloc::ConcreteInt>())
+ // If value is an unsupported constant, produce unknown.
+ if (!val.getAs<nonloc::ConcreteInt>() && !val.getAs<nonloc::ConcreteFloat>())
return UnknownVal();
// Handle casts to a boolean type.
if (castTy->isBooleanType()) {
- bool b = val.castAs<nonloc::ConcreteInt>().getValue().getBoolValue();
- return makeTruthVal(b, castTy);
+ if (Optional<nonloc::ConcreteInt> CI = val.getAs<nonloc::ConcreteInt>())
+ return makeTruthVal(CI->getValue().getBoolValue(), castTy);
+ if (Optional<nonloc::ConcreteFloat> CF = val.getAs<nonloc::ConcreteFloat>())
+ return makeTruthVal(!CF->getValue().isZero(), castTy);
}
- // Only handle casts from integers to integers - if val is an integer constant
- // being cast to a non-integer type, produce unknown.
- if (!isLocType && !castTy->isIntegralOrEnumerationType())
- return UnknownVal();
+ // Handle casts from integer
+ if (Optional<nonloc::ConcreteInt> CI = val.getAs<nonloc::ConcreteInt>()) {
+ if (castTy->isRealFloatingType()) {
+ if (isLocType)
+ return UnknownVal();
- llvm::APSInt i = val.castAs<nonloc::ConcreteInt>().getValue();
- BasicVals.getAPSIntType(castTy).apply(i);
+ llvm::APFloat Value(Context.getFloatTypeSemantics(castTy));
+ // Cannot be represented in destination type, this is undefined behavior
+ if (!BasicValueFactory::Convert(Value, CI->getValue()))
+ return UndefinedVal();
+ return makeFloatVal(Value);
+ }
- if (isLocType)
- return makeIntLocVal(i);
- else
- return makeIntVal(i);
+ // Only handle casts from integers to integers - if val is an integer
+ // constant being cast to a non-integer type, produce unknown.
+ if (!isLocType && !castTy->isIntegralOrEnumerationType())
+ return UnknownVal();
+
+ llvm::APSInt Value = CI->getValue();
+ BasicVals.getAPSIntType(castTy).apply(Value);
+ if (isLocType)
+ return makeIntLocVal(Value);
+ return makeIntVal(Value);
+ }
+
+ // Handle casts from real floating-point
+ if (Optional<nonloc::ConcreteFloat> CF = val.getAs<nonloc::ConcreteFloat>()) {
+ bool lossOfPrecision;
+
+ if (castTy->isIntegralOrEnumerationType()) {
+ llvm::APSInt Value(Context.getTypeSize(castTy),
+ !castTy->isSignedIntegerOrEnumerationType());
+ // Cannot be represented in destination type, this is undefined behavior
+ if (!BasicValueFactory::Convert(Value, CF->getValue()))
+ return UndefinedVal();
+ if (isLocType)
+ return makeIntLocVal(Value);
+ return makeIntVal(Value);
+ }
+
+ if (castTy->isRealFloatingType()) {
+ if (isLocType)
+ return UnknownVal();
+
+ llvm::APFloat Value = CF->getValue();
+ llvm::APFloat::opStatus Status =
+ Value.convert(Context.getFloatTypeSemantics(castTy),
+ llvm::APFloat::rmNearestTiesToEven, &lossOfPrecision);
+ // Cannot be represented in destination type, this is undefined behavior
+ if (Status & (llvm::APFloat::opOverflow | llvm::APFloat::opInvalidOp))
+ return UndefinedVal();
+ return makeFloatVal(Value);
+ }
+
+ return UnknownVal();
+ }
+
+ return UnknownVal();
}
SVal SimpleSValBuilder::evalCastFromLoc(Loc val, QualType castTy) {
@@ -196,6 +252,8 @@
switch (val.getSubKind()) {
case nonloc::ConcreteIntKind:
return val.castAs<nonloc::ConcreteInt>().evalMinus(*this);
+ case nonloc::ConcreteFloatKind:
+ return val.castAs<nonloc::ConcreteFloat>().evalMinus(*this);
default:
return UnknownVal();
}
@@ -215,9 +273,9 @@
//===----------------------------------------------------------------------===//
SVal SimpleSValBuilder::MakeSymIntVal(const SymExpr *LHS,
- BinaryOperator::Opcode op,
- const llvm::APSInt &RHS,
- QualType resultTy) {
+ BinaryOperator::Opcode op,
+ const llvm::APSInt &RHS,
+ QualType resultTy) {
bool isIdempotent = false;
// Check for a few special cases with known reductions first.
@@ -309,15 +367,31 @@
return makeNonLoc(LHS, op, *ConvertedRHS, resultTy);
}
+SVal SimpleSValBuilder::MakeSymFloatVal(const SymExpr *LHS,
+ BinaryOperator::Opcode op,
+ const llvm::APFloat &RHS,
+ QualType resultTy) {
+ ConstraintManager &CM = getStateManager().getConstraintManager();
+ if (!CM.canReasonAboutFloat())
+ return UnknownVal();
+
+ if (RHS.isNaN())
+ return makeTruthVal(op == BO_NE, resultTy);
+
+ const llvm::APFloat *ConvertedRHS = &RHS;
+ return makeNonLoc(LHS, op, *ConvertedRHS, resultTy);
+}
+
SVal SimpleSValBuilder::evalBinOpNN(ProgramStateRef state,
BinaryOperator::Opcode op,
NonLoc lhs, NonLoc rhs,
QualType resultTy) {
NonLoc InputLHS = lhs;
NonLoc InputRHS = rhs;
// Handle trivial case where left-side and right-side are the same.
- if (lhs == rhs)
+ // Skip floating-point operations, which are not commutative.
+ if (lhs == rhs && !lhs.isFloat())
switch (op) {
default:
break;
@@ -448,6 +522,29 @@
return makeSymExprValNN(state, op, InputLHS, InputRHS, resultTy);
}
}
+ case nonloc::ConcreteFloatKind: {
+ llvm::APFloat LHSValue = lhs.castAs<nonloc::ConcreteFloat>().getValue();
+
+ // If we're dealing with two known constants, just perform the operation.
+ if (const llvm::APFloat *KnownRHSValue = getKnownFloatValue(state, rhs)) {
+ llvm::APFloat RHSValue = *KnownRHSValue;
+
+ if (BinaryOperator::isComparisonOp(op)) {
+ const llvm::APSInt *V =
+ BasicVals.evalAPFloatComparison(op, LHSValue, RHSValue);
+ if (V)
+ return nonloc::ConcreteInt(*V);
+ return UnknownVal();
+ }
+
+ const llvm::APFloat *V = BasicVals.evalAPFloat(op, LHSValue, RHSValue);
+ if (V)
+ return nonloc::ConcreteFloat(*V);
+ return UnknownVal();
+ }
+
+ return makeSymExprValNN(state, op, InputLHS, InputRHS, resultTy);
+ }
case nonloc::SymbolValKind: {
// We only handle LHS as simple symbols or SymIntExprs.
SymbolRef Sym = lhs.castAs<nonloc::SymbolVal>().getSymbol();
@@ -550,8 +647,13 @@
}
// Is the RHS a constant?
- if (const llvm::APSInt *RHSValue = getKnownValue(state, rhs))
- return MakeSymIntVal(Sym, op, *RHSValue, resultTy);
+ if (rhs.isFloat()) {
+ if (const llvm::APFloat *RHSValue = getKnownFloatValue(state, rhs))
+ return MakeSymFloatVal(Sym, op, *RHSValue, resultTy);
+ } else {
+ if (const llvm::APSInt *RHSValue = getKnownValue(state, rhs))
+ return MakeSymIntVal(Sym, op, *RHSValue, resultTy);
+ }
// Give up -- this is not a symbolic expression we can handle.
return makeSymExprValNN(state, op, InputLHS, InputRHS, resultTy);
@@ -987,6 +1089,8 @@
if (V.isUnknownOrUndef())
return nullptr;
+ assert(!V.isFloat());
+
if (Optional<loc::ConcreteInt> X = V.getAs<loc::ConcreteInt>())
return &X->getValue();
@@ -1003,6 +1107,26 @@
return nullptr;
}
+const llvm::APFloat *
+SimpleSValBuilder::getKnownFloatValue(ProgramStateRef state, SVal V) {
+ if (V.isUnknownOrUndef())
+ return nullptr;
+
+ assert(V.isFloat());
+
+ if (Optional<nonloc::ConcreteFloat> X = V.getAs<nonloc::ConcreteFloat>())
+ return &X->getValue();
+
+ if (SymbolRef Sym = V.getAsSymbol())
+ return state->getConstraintManager().getSymFloatVal(state, Sym);
+
+ if (Optional<NonLoc> NV = V.getAs<NonLoc>())
+ if (SymbolRef Sym = NV->getAsSymExpr())
+ return state->getConstraintManager().getSymFloatVal(state, Sym);
+
+ return nullptr;
+}
+
SVal SimpleSValBuilder::simplifySVal(ProgramStateRef State, SVal V) {
// For now, this function tries to constant-fold symbols inside a
// nonloc::SymbolVal, and does nothing else. More simplifications should
@@ -1017,10 +1141,19 @@
: State(State), SVB(State->getStateManager().getSValBuilder()) {}
SVal VisitSymbolData(const SymbolData *S) {
- if (const llvm::APSInt *I =
- SVB.getKnownValue(State, nonloc::SymbolVal(S)))
- return Loc::isLocType(S->getType()) ? (SVal)SVB.makeIntLocVal(*I)
- : (SVal)SVB.makeIntVal(*I);
+ if (!S->getType()->isRealFloatingType()) {
+ const llvm::APSInt *I =
+ SVB.getKnownValue(State, nonloc::SymbolVal(S));
+ if (I)
+ return Loc::isLocType(S->getType()) ? (SVal)SVB.makeIntLocVal(*I)
+ : (SVal)SVB.makeIntVal(*I);
+ } else {
+ const llvm::APFloat *F =
+ SVB.getKnownFloatValue(State, nonloc::SymbolVal(S));
+ assert(!Loc::isLocType(S->getType()));
+ if (F)
+ return (SVal)SVB.makeFloatVal(*F);
+ }
return nonloc::SymbolVal(S);
}
@@ -1053,6 +1186,18 @@
return SVB.evalBinOp(State, S->getOpcode(), LHS, RHS, S->getType());
}
+ SVal VisitSymFloatExpr(const SymFloatExpr *S) {
+ SVal LHS = Visit(S->getLHS());
+ SVal RHS = SVB.makeFloatVal(S->getRHS());
+ return SVB.evalBinOp(State, S->getOpcode(), LHS, RHS, S->getType());
+ }
+
+ SVal VisitFloatSymExpr(const FloatSymExpr *S) {
+ SVal RHS = Visit(S->getRHS());
+ SVal LHS = SVB.makeFloatVal(S->getLHS());
+ return SVB.evalBinOp(State, S->getOpcode(), LHS, RHS, S->getType());
+ }
+
SVal VisitSymbolCast(const SymbolCast *S) {
SVal V = Visit(S->getOperand());
return SVB.evalCast(V, S->getType(), S->getOperand()->getType());
Index: lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
===================================================================
--- lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
+++ lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
@@ -53,9 +53,6 @@
ProgramStateRef SimpleConstraintManager::assumeAux(ProgramStateRef State,
NonLoc Cond,
bool Assumption) {
-
- // We cannot reason about SymSymExprs, and can only reason about some
- // SymIntExprs.
if (!canReasonAbout(Cond)) {
// Just add the constraint to the expression without trying to simplify.
SymbolRef Sym = Cond.getAsSymExpr();
@@ -74,6 +71,12 @@
return assumeSym(State, Sym, Assumption);
}
+ case nonloc::ConcreteFloatKind: {
+ bool b = !Cond.castAs<nonloc::ConcreteFloat>().getValue().isZero();
+ bool isFeasible = b ? Assumption : !Assumption;
+ return isFeasible ? State : nullptr;
+ }
+
case nonloc::ConcreteIntKind: {
bool b = Cond.castAs<nonloc::ConcreteInt>().getValue() != 0;
bool isFeasible = b ? Assumption : !Assumption;
@@ -117,7 +120,32 @@
if (SymbolRef Sym = Value.getAsSymbol())
return assumeSymInclusiveRange(State, Sym, From, To, InRange);
return State;
- } // end switch
+ }
+
+ case nonloc::ConcreteFloatKind: {
+ BasicValueFactory &BVF = getBasicVals();
+
+ const llvm::APFloat &FloatVal =
+ Value.castAs<nonloc::ConcreteFloat>().getValue();
+ llvm::APFloat FromF(FloatVal.getSemantics(), llvm::APFloat::uninitialized);
+ llvm::APFloat ToF(FloatVal.getSemantics(), llvm::APFloat::uninitialized);
+#ifndef NDEBUG
+ assert(BVF.Convert(FromF, From) && "Integer failed to convert to float!");
+ assert(BVF.Convert(ToF, To) && "Integer failed to convert to float!");
+#else
+ BVF.Convert(FromF, From);
+ BVF.Convert(ToF, To);
+#endif
+ llvm::APFloat::cmpResult CompareFrom = FloatVal.compare(FromF);
+ llvm::APFloat::cmpResult CompareTo = FloatVal.compare(ToF);
+
+ bool IsInRange = (CompareFrom == llvm::APFloat::cmpGreaterThan ||
+ CompareFrom == llvm::APFloat::cmpEqual) &&
+ (CompareTo == llvm::APFloat::cmpLessThan ||
+ CompareTo == llvm::APFloat::cmpEqual);
+ bool isFeasible = (IsInRange == InRange);
+ return isFeasible ? State : nullptr;
+ }
case nonloc::ConcreteIntKind: {
const llvm::APSInt &IntVal = Value.castAs<nonloc::ConcreteInt>().getValue();
Index: lib/StaticAnalyzer/Core/SVals.cpp
===================================================================
--- lib/StaticAnalyzer/Core/SVals.cpp
+++ lib/StaticAnalyzer/Core/SVals.cpp
@@ -19,6 +19,7 @@
#include "clang/AST/DeclCXX.h"
using namespace clang;
using namespace ento;
+using llvm::APFloat;
using llvm::APSInt;
//===----------------------------------------------------------------------===//
@@ -204,8 +205,16 @@
// Useful predicates.
//===----------------------------------------------------------------------===//
+bool SVal::isFloat() const {
+ if (Optional<nonloc::SymbolVal> SV = getAs<nonloc::SymbolVal>()) {
+ return SV->getSymbol()->getType()->isRealFloatingType();
+ }
+ return getAs<nonloc::ConcreteFloat>().hasValue();
+}
+
bool SVal::isConstant() const {
- return getAs<nonloc::ConcreteInt>() || getAs<loc::ConcreteInt>();
+ return getAs<nonloc::ConcreteInt>() || getAs<loc::ConcreteInt>() ||
+ getAs<nonloc::ConcreteFloat>();
}
bool SVal::isConstant(int I) const {
@@ -216,7 +225,15 @@
return false;
}
+bool SVal::isConstant(APFloat &V) const {
+ if (Optional<nonloc::ConcreteFloat> NF = getAs<nonloc::ConcreteFloat>())
+ return NF->getValue().compare(V) == llvm::APFloat::cmpEqual;
+ return false;
+}
+
bool SVal::isZeroConstant() const {
+ if (Optional<nonloc::ConcreteFloat> NF = getAs<nonloc::ConcreteFloat>())
+ return NF->getValue().isPosZero() || NF->getValue().isNegZero();
return isConstant(0);
}
@@ -247,6 +264,31 @@
return svalBuilder.makeIntVal(-getValue());
}
+nonloc::ConcreteFloat
+nonloc::ConcreteFloat::evalMinus(SValBuilder &svalBuilder) const {
+ llvm::APFloat Value = getValue();
+ Value.changeSign();
+ return svalBuilder.makeFloatVal(Value);
+}
+
+SVal nonloc::ConcreteFloat::evalBinOp(SValBuilder &svalBuilder,
+ BinaryOperator::Opcode Op,
+ const nonloc::ConcreteFloat& R) const {
+ if (BinaryOperator::isComparisonOp(Op)) {
+ const llvm::APSInt *V = svalBuilder.getBasicValueFactory().evalAPFloatComparison(
+ Op, getValue(), R.getValue());
+ if (V)
+ return nonloc::ConcreteInt(*V);
+ return UnknownVal();
+ }
+
+ const llvm::APFloat *V = svalBuilder.getBasicValueFactory().evalAPFloat(
+ Op, getValue(), R.getValue());
+ if (V)
+ return nonloc::ConcreteFloat(*V);
+ return UnknownVal();
+}
+
//===----------------------------------------------------------------------===//
// Transfer function dispatch for Locs.
//===----------------------------------------------------------------------===//
@@ -300,6 +342,17 @@
<< C.getValue().getBitWidth() << 'b';
break;
}
+ case nonloc::ConcreteFloatKind: {
+ const nonloc::ConcreteFloat& C = castAs<nonloc::ConcreteFloat>();
+ SmallString<24> Chars;
+
+ C.getValue().toString(Chars, 0, 0);
+ os << Chars
+ << ' '
+ << llvm::APFloat::semanticsSizeInBits(C.getValue().getSemantics())
+ << 'b';
+ break;
+ }
case nonloc::SymbolValKind: {
os << castAs<nonloc::SymbolVal>().getSymbol();
break;
Index: lib/StaticAnalyzer/Core/SValBuilder.cpp
===================================================================
--- lib/StaticAnalyzer/Core/SValBuilder.cpp
+++ lib/StaticAnalyzer/Core/SValBuilder.cpp
@@ -40,12 +40,15 @@
type->isAnyComplexType())
return makeCompoundVal(type, BasicVals.getEmptySValList());
- // FIXME: Handle floats.
+ if (type->isRealFloatingType())
+ return makeFloatVal(0, type);
+
+ // FIXME: Handle structs.
return UnknownVal();
}
NonLoc SValBuilder::makeNonLoc(const SymExpr *lhs, BinaryOperator::Opcode op,
- const llvm::APSInt& rhs, QualType type) {
+ const llvm::APSInt& rhs, QualType type) {
// The Environment ensures we always get a persistent APSInt in
// BasicValueFactory, so we don't need to get the APSInt from
// BasicValueFactory again.
@@ -63,6 +66,24 @@
}
NonLoc SValBuilder::makeNonLoc(const SymExpr *lhs, BinaryOperator::Opcode op,
+ const llvm::APFloat& rhs, QualType type) {
+ // The Environment ensures we always get a persistent APSInt in
+ // BasicValueFactory, so we don't need to get the APSInt from
+ // BasicValueFactory again.
+ assert(lhs);
+ assert(!Loc::isLocType(type));
+ return nonloc::SymbolVal(SymMgr.getSymFloatExpr(lhs, op, rhs, type));
+}
+
+NonLoc SValBuilder::makeNonLoc(const llvm::APFloat& lhs,
+ BinaryOperator::Opcode op, const SymExpr *rhs,
+ QualType type) {
+ assert(rhs);
+ assert(!Loc::isLocType(type));
+ return nonloc::SymbolVal(SymMgr.getFloatSymExpr(lhs, op, rhs, type));
+}
+
+NonLoc SValBuilder::makeNonLoc(const SymExpr *lhs, BinaryOperator::Opcode op,
const SymExpr *rhs, QualType type) {
assert(lhs && rhs);
assert(!Loc::isLocType(type));
@@ -304,6 +325,9 @@
case Stmt::IntegerLiteralClass:
return makeIntVal(cast<IntegerLiteral>(E));
+ case Stmt::FloatingLiteralClass:
+ return makeFloatVal(cast<FloatingLiteral>(E));
+
case Stmt::ObjCBoolLiteralExprClass:
return makeBoolVal(cast<ObjCBoolLiteralExpr>(E));
@@ -316,7 +340,8 @@
default:
break;
case CK_ArrayToPointerDecay:
- case CK_BitCast: {
+ case CK_BitCast:
+ case CK_IntegralToFloating: {
const Expr *SE = CE->getSubExpr();
Optional<SVal> Val = getConstantVal(SE);
if (!Val)
@@ -353,23 +378,41 @@
BinaryOperator::Opcode Op,
NonLoc LHS, NonLoc RHS,
QualType ResultTy) {
+ ConstraintManager &CM = getStateManager().getConstraintManager();
+
const SymExpr *symLHS = LHS.getAsSymExpr();
const SymExpr *symRHS = RHS.getAsSymExpr();
// TODO: When the Max Complexity is reached, we should conjure a symbol
// instead of generating an Unknown value and propagate the taint info to it.
const unsigned MaxComp = 1000; // 10000 28X
+ // If constraint manager doesn't support floating-point expressions, skip
+ // generating those constraints.
if (symLHS && symRHS &&
- (symLHS->computeComplexity() + symRHS->computeComplexity()) < MaxComp)
+ (symLHS->computeComplexity() + symRHS->computeComplexity()) < MaxComp) {
+ if (!CM.canReasonAboutFloat() &&
+ (symLHS->getType()->isFloatingType() || symRHS->getType()->isFloatingType()))
+ return UnknownVal();
return makeNonLoc(symLHS, Op, symRHS, ResultTy);
+ }
- if (symLHS && symLHS->computeComplexity() < MaxComp)
+ if (symLHS && symLHS->computeComplexity() < MaxComp) {
if (Optional<nonloc::ConcreteInt> rInt = RHS.getAs<nonloc::ConcreteInt>())
return makeNonLoc(symLHS, Op, rInt->getValue(), ResultTy);
+ if (Optional<nonloc::ConcreteFloat> rFloat = RHS.getAs<nonloc::ConcreteFloat>()) {
+ if (CM.canReasonAboutFloat())
+ return makeNonLoc(symLHS, Op, rFloat->getValue(), ResultTy);
+ }
+ }
- if (symRHS && symRHS->computeComplexity() < MaxComp)
+ if (symRHS && symRHS->computeComplexity() < MaxComp) {
if (Optional<nonloc::ConcreteInt> lInt = LHS.getAs<nonloc::ConcreteInt>())
return makeNonLoc(lInt->getValue(), Op, symRHS, ResultTy);
+ if (Optional<nonloc::ConcreteFloat> lFloat = LHS.getAs<nonloc::ConcreteFloat>()) {
+ if (CM.canReasonAboutFloat())
+ return makeNonLoc(lFloat->getValue(), Op, symRHS, ResultTy);
+ }
+ }
return UnknownVal();
}
Index: lib/StaticAnalyzer/Core/RegionStore.cpp
===================================================================
--- lib/StaticAnalyzer/Core/RegionStore.cpp
+++ lib/StaticAnalyzer/Core/RegionStore.cpp
@@ -2038,7 +2038,7 @@
if (Loc::isLocType(T))
V = svalBuilder.makeNull();
- else if (T->isIntegralOrEnumerationType())
+ else if (T->isIntegralOrEnumerationType() || T->isRealFloatingType())
V = svalBuilder.makeZeroVal(T);
else if (T->isStructureOrClassType() || T->isArrayType()) {
// Set the default value to a zero constant when it is a structure
Index: lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
===================================================================
--- lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
+++ lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
@@ -39,7 +39,6 @@
return assumeSymRel(State, SIE->getLHS(), op, SIE->getRHS());
}
-
} else if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(Sym)) {
// Translate "a != b" to "(b - a) != 0".
// We invert the order of the operands as a heuristic for how loop
Index: lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
===================================================================
--- lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -293,6 +293,8 @@
bool canReasonAbout(SVal X) const override;
+ bool canReasonAboutFloat() const override;
+
ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym) override;
const llvm::APSInt *getSymVal(ProgramStateRef State,
@@ -370,46 +372,50 @@
bool RangeConstraintManager::canReasonAbout(SVal X) const {
Optional<nonloc::SymbolVal> SymVal = X.getAs<nonloc::SymbolVal>();
- if (SymVal && SymVal->isExpression()) {
- const SymExpr *SE = SymVal->getSymbol();
-
- if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(SE)) {
- switch (SIE->getOpcode()) {
- // We don't reason yet about bitwise-constraints on symbolic values.
- case BO_And:
- case BO_Or:
- case BO_Xor:
- return false;
- // We don't reason yet about these arithmetic constraints on
- // symbolic values.
- case BO_Mul:
- case BO_Div:
- case BO_Rem:
- case BO_Shl:
- case BO_Shr:
- return false;
- // All other cases.
- default:
- return true;
- }
- }
-
- if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(SE)) {
- if (BinaryOperator::isComparisonOp(SSE->getOpcode())) {
- // We handle Loc <> Loc comparisons, but not (yet) NonLoc <> NonLoc.
- if (Loc::isLocType(SSE->getLHS()->getType())) {
- assert(Loc::isLocType(SSE->getRHS()->getType()));
+ if (SymVal) {
+ if (SymVal->getSymbol()->getType()->isFloatingType()) {
+ return false;
+ } else if (const SymExpr *SE = SymVal->getSymbol()) {
+ if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(SE)) {
+ switch (SIE->getOpcode()) {
+ // We don't reason yet about bitwise-constraints on symbolic values.
+ case BO_And:
+ case BO_Or:
+ case BO_Xor:
+ return false;
+ // We don't reason yet about these arithmetic constraints on
+ // symbolic values.
+ case BO_Mul:
+ case BO_Div:
+ case BO_Rem:
+ case BO_Shl:
+ case BO_Shr:
+ return false;
+ // All other cases.
+ default:
return true;
}
+ } else if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(SE)) {
+ if (BinaryOperator::isComparisonOp(SSE->getOpcode())) {
+ // We handle Loc <> Loc comparisons, but not (yet) NonLoc <> NonLoc.
+ if (Loc::isLocType(SSE->getLHS()->getType())) {
+ assert(Loc::isLocType(SSE->getRHS()->getType()));
+ return true;
+ }
+ }
}
- }
- return false;
+ return false;
+ }
}
return true;
}
+bool RangeConstraintManager::canReasonAboutFloat() const {
+ return false;
+}
+
ConditionTruthVal RangeConstraintManager::checkNull(ProgramStateRef State,
SymbolRef Sym) {
const RangeSet *Ranges = State->get<ConstraintRange>(Sym);
Index: lib/StaticAnalyzer/Core/ProgramState.cpp
===================================================================
--- lib/StaticAnalyzer/Core/ProgramState.cpp
+++ lib/StaticAnalyzer/Core/ProgramState.cpp
@@ -262,29 +262,39 @@
// about).
if (!T.isNull()) {
if (SymbolRef sym = V.getAsSymbol()) {
- if (const llvm::APSInt *Int = getStateManager()
- .getConstraintManager()
- .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.
- //
- // This shows up in the following:
- //
- // char foo();
- // unsigned x = foo();
- // if (x == 54)
- // ...
- //
- // 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 (V.getAs<Loc>())
- return loc::ConcreteInt(NewV);
- else
- return nonloc::ConcreteInt(NewV);
+ ConstraintManager &CM = getStateManager().getConstraintManager();
+
+ if (sym->getType()->isRealFloatingType()) {
+ if (const llvm::APFloat *Float = CM.getSymFloatVal(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.
+ //
+ // This shows up in the following:
+ //
+ // char foo();
+ // unsigned x = foo();
+ // if (x == 54)
+ // ...
+ //
+ // 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::APFloat &NewV = getBasicVals().Convert(T, *Float);
+
+ assert(!V.getAs<Loc>() && "Loc::ConcreteFloat not supported!");
+ return nonloc::ConcreteFloat(NewV);
+ }
+ } else {
+ if (const llvm::APSInt *Int = CM.getSymVal(this, sym)) {
+ // FIXME: Likewise
+ const llvm::APSInt &NewV = getBasicVals().Convert(T, *Int);
+
+ if (V.getAs<Loc>())
+ return loc::ConcreteInt(NewV);
+ else
+ return nonloc::ConcreteInt(NewV);
+ }
}
}
}
Index: lib/StaticAnalyzer/Core/Environment.cpp
===================================================================
--- lib/StaticAnalyzer/Core/Environment.cpp
+++ lib/StaticAnalyzer/Core/Environment.cpp
@@ -86,6 +86,7 @@
case Stmt::CXXScalarValueInitExprClass:
case Stmt::ImplicitValueInitExprClass:
case Stmt::IntegerLiteralClass:
+ case Stmt::FloatingLiteralClass:
case Stmt::ObjCBoolLiteralExprClass:
case Stmt::CXXNullPtrLiteralExprClass:
case Stmt::ObjCStringLiteralClass:
Index: lib/StaticAnalyzer/Core/BasicValueFactory.cpp
===================================================================
--- lib/StaticAnalyzer/Core/BasicValueFactory.cpp
+++ lib/StaticAnalyzer/Core/BasicValueFactory.cpp
@@ -72,6 +72,9 @@
for (APSIntSetTy::iterator I=APSIntSet.begin(), E=APSIntSet.end(); I!=E; ++I)
I->getValue().~APSInt();
+ for (APFloatSetTy::iterator I=APFloatSet.begin(), E=APFloatSet.end(); I!=E; ++I)
+ I->getValue().~APFloat();
+
delete (PersistentSValsTy*) PersistentSVals;
delete (PersistentSValPairsTy*) PersistentSValPairs;
}
@@ -111,6 +114,28 @@
return getValue(getAPSIntType(T).getValue(X));
}
+const llvm::APFloat &BasicValueFactory::getValue(const llvm::APFloat& X) {
+ llvm::FoldingSetNodeID ID;
+ void *InsertPos;
+ typedef llvm::FoldingSetNodeWrapper<llvm::APFloat> FoldNodeTy;
+
+ X.Profile(ID);
+ FoldNodeTy* P = APFloatSet.FindNodeOrInsertPos(ID, InsertPos);
+
+ if (!P) {
+ P = (FoldNodeTy*) BPAlloc.Allocate<FoldNodeTy>();
+ new (P) FoldNodeTy(X);
+ APFloatSet.InsertNode(P, InsertPos);
+ }
+
+ return *P;
+}
+
+const llvm::APFloat &BasicValueFactory::getValue(int64_t X,
+ const llvm::fltSemantics &S) {
+ return Convert(llvm::APSInt::get(X), S);
+}
+
const CompoundValData*
BasicValueFactory::getCompoundValData(QualType T,
llvm::ImmutableList<SVal> Vals) {
@@ -286,6 +311,90 @@
}
}
+const llvm::APFloat*
+BasicValueFactory::evalAPFloat(BinaryOperator::Opcode Op,
+ const llvm::APFloat& V1, const llvm::APFloat& V2) {
+ llvm::APFloat NewV = V1;
+ llvm::APFloat::opStatus Status = llvm::APFloat::opOK;
+
+ switch (Op) {
+ default:
+ assert (false && "Invalid Opcode.");
+
+ case BO_Mul:
+ Status = NewV.multiply(V2, llvm::APFloat::rmNearestTiesToEven);
+ if (Status & llvm::APFloat::opOK)
+ return &getValue(NewV);
+ break;
+
+ case BO_Div:
+ // Divide by zero
+ if (V1.isFinite() && V2.isInfinity())
+ NewV = llvm::APFloat::getZero(V1.getSemantics());
+ else
+ Status = NewV.divide(V2, llvm::APFloat::rmNearestTiesToEven);
+ if (Status & llvm::APFloat::opOK)
+ return &getValue(NewV);
+ break;
+
+ case BO_Rem:
+ Status = NewV.remainder(V2);
+ if (Status & llvm::APFloat::opOK)
+ return &getValue(NewV);
+ break;
+
+ case BO_Add:
+ Status = NewV.add(V2, llvm::APFloat::rmNearestTiesToEven);
+ if (Status & llvm::APFloat::opOK)
+ return &getValue(NewV);
+ break;
+
+ case BO_Sub:
+ Status = NewV.subtract(V2, llvm::APFloat::rmNearestTiesToEven);
+ if (Status & llvm::APFloat::opOK)
+ return &getValue(NewV);
+ break;
+ }
+
+ // TODO: Fix sign of special results
+ if (Status & llvm::APFloat::opOverflow)
+ return &getValue(llvm::APFloat::getInf(NewV.getSemantics()));
+ else if (Status & llvm::APFloat::opDivByZero)
+ return &getValue(llvm::APFloat::getInf(NewV.getSemantics()));
+ else if (Status & llvm::APFloat::opInvalidOp)
+ return &getValue(llvm::APFloat::getSNaN(NewV.getSemantics()));
+ return &getValue(NewV);
+}
+
+const llvm::APSInt*
+BasicValueFactory::evalAPFloatComparison(BinaryOperator::Opcode Op,
+ const llvm::APFloat& V1, const llvm::APFloat& V2) {
+ llvm::APFloat::cmpResult R = V1.compare(V2);
+ switch (Op) {
+ default:
+ assert (false && "Invalid Opcode.");
+
+ case BO_LT:
+ return &getTruthValue(R == llvm::APFloat::cmpLessThan);
+
+ case BO_GT:
+ return &getTruthValue(R == llvm::APFloat::cmpGreaterThan);
+
+ case BO_LE:
+ return &getTruthValue(R == llvm::APFloat::cmpLessThan ||
+ R == llvm::APFloat::cmpEqual);
+
+ case BO_GE:
+ return &getTruthValue(R == llvm::APFloat::cmpGreaterThan ||
+ R == llvm::APFloat::cmpEqual);
+
+ case BO_EQ:
+ return &getTruthValue(R == llvm::APFloat::cmpEqual);
+
+ case BO_NE:
+ return &getTruthValue(R != llvm::APFloat::cmpEqual);
+ }
+}
const std::pair<SVal, uintptr_t>&
BasicValueFactory::getPersistentSValWithData(const SVal& V, uintptr_t Data) {
Index: lib/StaticAnalyzer/Checkers/FloatingPointMath.cpp
===================================================================
--- /dev/null
+++ lib/StaticAnalyzer/Checkers/FloatingPointMath.cpp
@@ -0,0 +1,342 @@
+//=== FloatingPointMathChecker.cpp --------------------------------*- C++
+//-*-===//
+//
+// The LLVM Compiler Infrastructure
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+//
+// This checker evaluates calls to floating-point math functions for domain
+// errors.
+//
+//===----------------------------------------------------------------------===//
+
+#include "ClangSACheckers.h"
+#include "clang/Basic/Builtins.h"
+#include "clang/StaticAnalyzer/Core/BugReporter/BugType.h"
+#include "clang/StaticAnalyzer/Core/Checker.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/CallEvent.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/CheckerContext.h"
+
+using namespace clang;
+using namespace ento;
+
+namespace {
+class FloatingPointMathChecker : public Checker<check::PreCall> {
+ mutable std::unique_ptr<BuiltinBug> BT;
+
+ void reportError(ProgramStateRef State, CheckerContext &C) const;
+
+ void inline handleAssumption(ProgramStateRef T, ProgramStateRef F,
+ ProgramStateRef State, CheckerContext &C) const;
+
+public:
+ void checkPreCall(const CallEvent &Call, CheckerContext &C) const;
+};
+
+} // end anonymous namespace
+
+void FloatingPointMathChecker::reportError(ProgramStateRef State,
+ CheckerContext &C) const {
+ if (ExplodedNode *N = C.generateNonFatalErrorNode(State)) {
+ if (!BT)
+ BT.reset(new BuiltinBug(this, "Domain/range error"));
+ C.emitReport(llvm::make_unique<BugReport>(
+ *BT, "Argument value is out of valid domain for function call", N));
+ }
+}
+
+void FloatingPointMathChecker::handleAssumption(ProgramStateRef T,
+ ProgramStateRef F,
+ ProgramStateRef State,
+ CheckerContext &C) const {
+ if (F) {
+ reportError(State, C);
+
+ if (!T)
+ C.addTransition(F);
+ }
+
+ if (!F && T)
+ C.addTransition(T);
+}
+
+void FloatingPointMathChecker::checkPreCall(const CallEvent &Call,
+ CheckerContext &C) const {
+ ProgramStateRef State = C.getState();
+ const Decl *D = Call.getDecl();
+ if (!D)
+ return;
+ const FunctionDecl *FD = dyn_cast<FunctionDecl>(D);
+ if (!FD)
+ return;
+
+ ConstraintManager &CM = C.getConstraintManager();
+ SValBuilder &SVB = C.getSValBuilder();
+ BasicValueFactory &BVF = SVB.getBasicValueFactory();
+ ASTContext &Ctx = SVB.getContext();
+ QualType Int32Ty = Ctx.getIntTypeForBitwidth(32, true);
+
+ switch (FD->getBuiltinID()) {
+ default:
+ return;
+
+ // acos(x): -1 <= x <= 1
+ case Builtin::BIacos:
+ case Builtin::BIacosf:
+ case Builtin::BIacosl:
+ case Builtin::BIasin:
+ case Builtin::BIasinf:
+ case Builtin::BIasinl:
+ case Builtin::BI__builtin_acos:
+ case Builtin::BI__builtin_acosf:
+ case Builtin::BI__builtin_acosl:
+ case Builtin::BI__builtin_asin:
+ case Builtin::BI__builtin_asinf:
+ case Builtin::BI__builtin_asinl: {
+ assert(Call.getNumArgs() == 1);
+ SVal V = Call.getArgSVal(0);
+ llvm::APSInt From = BVF.getValue(-1, Int32Ty);
+ llvm::APSInt To = BVF.getValue(1, Int32Ty);
+
+ // Skip if known to be NaN, otherwise assume to be not NaN
+ SVal notNaN = SVB.evalBinOp(State, BO_EQ, V, V, SVB.getConditionType());
+ if (notNaN.isUnknown() || notNaN.isZeroConstant()) {
+ return;
+ }
+
+ ProgramStateRef StIR, StOR;
+ // This relies on the constraint manager promoting from APSInt to APFloat
+ // because the type of V is floating-point.
+ std::tie(StIR, StOR) =
+ CM.assumeInclusiveRangeDual(State, V.castAs<NonLoc>(), From, To);
+ return handleAssumption(StIR, StOR, State, C);
+ }
+
+ // acosh(x): x >= 1
+ case Builtin::BIacosh:
+ case Builtin::BIacoshf:
+ case Builtin::BIacoshl:
+ case Builtin::BI__builtin_acosh:
+ case Builtin::BI__builtin_acoshf:
+ case Builtin::BI__builtin_acoshl: {
+ assert(Call.getNumArgs() == 1);
+ SVal V = Call.getArgSVal(0);
+ llvm::APFloat From = BVF.getValue(
+ 1, Ctx.getFloatTypeSemantics(Call.getArgExpr(0)->getType()));
+ DefinedOrUnknownSVal SV = SVB.makeFloatVal(From);
+
+ SVal notNaN = SVB.evalBinOp(State, BO_EQ, V, V, SVB.getConditionType());
+ if (notNaN.isUnknown() || notNaN.isZeroConstant()) {
+ return;
+ }
+
+ SVal isGE = SVB.evalBinOp(State, BO_GE, V, SV, SVB.getConditionType());
+ if (isGE.isZeroConstant())
+ return reportError(State, C);
+
+ ProgramStateRef StT, StF;
+ std::tie(StT, StF) = CM.assumeDual(State, isGE.castAs<DefinedSVal>());
+ return handleAssumption(StT, StF, State, C);
+ }
+
+ // atanh(x): -1 < x < 1
+ case Builtin::BIatanh:
+ case Builtin::BIatanhf:
+ case Builtin::BIatanhl:
+ case Builtin::BI__builtin_atanh:
+ case Builtin::BI__builtin_atanhf:
+ case Builtin::BI__builtin_atanhl: {
+ assert(Call.getNumArgs() == 1);
+ SVal V = Call.getArgSVal(0);
+ llvm::APFloat From = BVF.getValue(
+ -1, Ctx.getFloatTypeSemantics(Call.getArgExpr(0)->getType()));
+ llvm::APFloat To = BVF.getValue(
+ 1, Ctx.getFloatTypeSemantics(Call.getArgExpr(0)->getType()));
+
+ SVal notNaN = SVB.evalBinOp(State, BO_EQ, V, V, SVB.getConditionType());
+ if (notNaN.isUnknown() || notNaN.isZeroConstant()) {
+ return;
+ }
+
+ DefinedOrUnknownSVal SFrom = SVB.makeFloatVal(From);
+ SVal isGT = SVB.evalBinOp(State, BO_GT, V, SFrom, SVB.getConditionType());
+ if (isGT.isZeroConstant())
+ return reportError(State, C);
+
+ DefinedOrUnknownSVal STo = SVB.makeFloatVal(To);
+ SVal isLT = SVB.evalBinOp(State, BO_LT, V, STo, SVB.getConditionType());
+ if (isGT.isConstant(1) && isLT.isZeroConstant())
+ return reportError(State, C);
+
+ // TODO: FIXME
+ // This should be BO_LAnd, but logical operations are handled much earlier
+ // during ExplodedGraph generation. However, since both sides are
+ // Boolean/Int1Ty, we can use bitwise and.
+ // If/when this is fixed, also remove the explicit short-circuits above.
+ SVal isIR =
+ SVB.evalBinOp(State, BO_And, isGT, isLT, SVB.getConditionType());
+ if (isIR.isZeroConstant())
+ return reportError(State, C);
+
+ ProgramStateRef StIR, StOR;
+ std::tie(StIR, StOR) = CM.assumeDual(State, isIR.castAs<DefinedSVal>());
+ return handleAssumption(StIR, StOR, State, C);
+ }
+
+ // log(x): x >= 0
+ case Builtin::BIlog:
+ case Builtin::BIlogf:
+ case Builtin::BIlogl:
+ case Builtin::BIlog2:
+ case Builtin::BIlog2f:
+ case Builtin::BIlog2l:
+ case Builtin::BIlog10:
+ case Builtin::BIlog10f:
+ case Builtin::BIlog10l:
+ case Builtin::BIsqrt:
+ case Builtin::BIsqrtf:
+ case Builtin::BIsqrtl:
+ case Builtin::BI__builtin_log:
+ case Builtin::BI__builtin_logf:
+ case Builtin::BI__builtin_logl:
+ case Builtin::BI__builtin_log2:
+ case Builtin::BI__builtin_log2f:
+ case Builtin::BI__builtin_log2l:
+ case Builtin::BI__builtin_log10:
+ case Builtin::BI__builtin_log10f:
+ case Builtin::BI__builtin_log10l:
+ case Builtin::BI__builtin_sqrt:
+ case Builtin::BI__builtin_sqrtf:
+ case Builtin::BI__builtin_sqrtl: {
+ assert(Call.getNumArgs() == 1);
+ SVal V = Call.getArgSVal(0);
+ llvm::APFloat From = BVF.getValue(
+ 0, Ctx.getFloatTypeSemantics(Call.getArgExpr(0)->getType()));
+ DefinedOrUnknownSVal SV = SVB.makeFloatVal(From);
+
+ SVal notNaN = SVB.evalBinOp(State, BO_EQ, V, V, SVB.getConditionType());
+ if (notNaN.isUnknown() || notNaN.isZeroConstant()) {
+ return;
+ }
+
+ SVal isGE = SVB.evalBinOp(State, BO_GE, V, SV, SVB.getConditionType());
+ if (isGE.isZeroConstant())
+ return reportError(State, C);
+
+ ProgramStateRef StT, StF;
+ std::tie(StT, StF) = CM.assumeDual(State, isGE.castAs<DefinedSVal>());
+ return handleAssumption(StT, StF, State, C);
+ }
+
+ // log1p(x): x >= -1
+ case Builtin::BIlog1p:
+ case Builtin::BIlog1pf:
+ case Builtin::BIlog1pl:
+ case Builtin::BI__builtin_log1p:
+ case Builtin::BI__builtin_log1pf:
+ case Builtin::BI__builtin_log1pl: {
+ assert(Call.getNumArgs() == 1);
+ SVal V = Call.getArgSVal(0);
+ llvm::APFloat From = BVF.getValue(
+ -1, Ctx.getFloatTypeSemantics(Call.getArgExpr(0)->getType()));
+ DefinedOrUnknownSVal SV = SVB.makeFloatVal(From);
+
+ SVal notNaN = SVB.evalBinOp(State, BO_EQ, V, V, SVB.getConditionType());
+ if (notNaN.isUnknown() || notNaN.isZeroConstant()) {
+ return;
+ }
+
+ SVal isGE = SVB.evalBinOp(State, BO_GE, V, SV, SVB.getConditionType());
+ if (isGE.isZeroConstant())
+ return reportError(State, C);
+
+ ProgramStateRef StT, StF;
+ std::tie(StT, StF) = CM.assumeDual(State, isGE.castAs<DefinedSVal>());
+ return handleAssumption(StT, StF, State, C);
+ }
+
+ // logb(x): x != 0
+ case Builtin::BIlogb:
+ case Builtin::BIlogbf:
+ case Builtin::BIlogbl:
+ case Builtin::BI__builtin_logb:
+ case Builtin::BI__builtin_logbf:
+ case Builtin::BI__builtin_logbl: {
+ assert(Call.getNumArgs() == 1);
+ SVal V = Call.getArgSVal(0);
+ llvm::APFloat From = BVF.getValue(
+ 0, Ctx.getFloatTypeSemantics(Call.getArgExpr(0)->getType()));
+ DefinedOrUnknownSVal SV = SVB.makeFloatVal(From);
+
+ SVal isNE = SVB.evalBinOp(State, BO_NE, V, SV, SVB.getConditionType());
+ if (isNE.isZeroConstant())
+ return reportError(State, C);
+
+ ProgramStateRef StT, StF;
+ std::tie(StT, StF) = CM.assumeDual(State, isNE.castAs<DefinedSVal>());
+ return handleAssumption(StT, StF, State, C);
+ }
+
+ // TODO:
+ // pow(x, y) : x > 0 || (x == 0 && y > 0) || (x < 0 && (int) y)
+ // case Builtin::BIpow:
+ // case Builtin::BIpowf:
+ // case Builtin::BIpowl:
+ // case Builtin::BI__builtin_pow:
+ // case Builtin::BI__builtin_powf:
+ // case Builtin::BI__builtin_powl:
+
+ // TODO:
+ // lgamma(x) : x != 0 && !(x < 0 && (int) x)
+ // case Builtin::BIlgamma:
+ // case Builtin::BIlgammaf:
+ // case Builtin::BIlgammal:
+ // case Builtin::BItgamma:
+ // case Builtin::BItgammaf:
+ // case Builtin::BItgammal:
+ // case Builtin::BI__builtin_lgamma:
+ // case Builtin::BI__builtin_lgammaf:
+ // case Builtin::BI__builtin_lgammal:
+ // case Builtin::BI__builtin_tgamma:
+ // case Builtin::BI__builtin_tgammaf:
+ // case Builtin::BI__builtin_tgammal:
+
+ // fmod(x,y) : y != 0
+ case Builtin::BIfmod:
+ case Builtin::BIfmodf:
+ case Builtin::BIfmodl:
+ case Builtin::BIremainder:
+ case Builtin::BIremainderf:
+ case Builtin::BIremainderl:
+ case Builtin::BI__builtin_fmod:
+ case Builtin::BI__builtin_fmodf:
+ case Builtin::BI__builtin_fmodl:
+ case Builtin::BI__builtin_remainder:
+ case Builtin::BI__builtin_remainderf:
+ case Builtin::BI__builtin_remainderl:
+ case Builtin::BI__builtin_remquo:
+ case Builtin::BI__builtin_remquof:
+ case Builtin::BI__builtin_remquol: {
+ assert(Call.getNumArgs() >= 2);
+ SVal V = Call.getArgSVal(1);
+ llvm::APFloat From = BVF.getValue(
+ 0, Ctx.getFloatTypeSemantics(Call.getArgExpr(1)->getType()));
+ DefinedOrUnknownSVal SV = SVB.makeFloatVal(From);
+
+ SVal isNE = SVB.evalBinOp(State, BO_NE, V, SV, SVB.getConditionType());
+ if (isNE.isZeroConstant())
+ return reportError(State, C);
+
+ ProgramStateRef StT, StF;
+ std::tie(StT, StF) = CM.assumeDual(State, isNE.castAs<DefinedSVal>());
+ return handleAssumption(StT, StF, State, C);
+ }
+ }
+}
+
+void ento::registerFloatingPointMathChecker(CheckerManager &mgr) {
+ mgr.registerChecker<FloatingPointMathChecker>();
+}
Index: lib/StaticAnalyzer/Checkers/CMakeLists.txt
===================================================================
--- lib/StaticAnalyzer/Checkers/CMakeLists.txt
+++ lib/StaticAnalyzer/Checkers/CMakeLists.txt
@@ -36,6 +36,7 @@
DynamicTypeChecker.cpp
ExprInspectionChecker.cpp
FixedAddressChecker.cpp
+ FloatingPointMath.cpp
GenericTaintChecker.cpp
GTestChecker.cpp
IdenticalExprChecker.cpp
Index: lib/StaticAnalyzer/Checkers/BuiltinFunctionChecker.cpp
===================================================================
--- lib/StaticAnalyzer/Checkers/BuiltinFunctionChecker.cpp
+++ lib/StaticAnalyzer/Checkers/BuiltinFunctionChecker.cpp
@@ -41,6 +41,80 @@
default:
return false;
+ case Builtin::BI__builtin_inf:
+ case Builtin::BI__builtin_inff:
+ case Builtin::BI__builtin_infl: {
+ SValBuilder &SVB = C.getSValBuilder();
+ ASTContext &Ctx = SVB.getContext();
+ llvm::APFloat Inf = llvm::APFloat::getInf(
+ Ctx.getFloatTypeSemantics(FD->getReturnType()));
+ SVal V = SVB.makeFloatVal(Inf);
+ C.addTransition(state->BindExpr(CE, LCtx, V));
+ return true;
+ }
+
+ // TODO: Model the string argument as well
+ case Builtin::BI__builtin_nan:
+ case Builtin::BI__builtin_nanf:
+ case Builtin::BI__builtin_nanl: {
+ SValBuilder &SVB = C.getSValBuilder();
+ ASTContext &Ctx = SVB.getContext();
+ llvm::APFloat NaN = llvm::APFloat::getQNaN(
+ Ctx.getFloatTypeSemantics(FD->getReturnType()));
+ SVal V = SVB.makeFloatVal(NaN);
+ C.addTransition(state->BindExpr(CE, LCtx, V));
+ return true;
+ }
+
+ case Builtin::BI__builtin_isinf: {
+ SValBuilder &SVB = C.getSValBuilder();
+ ASTContext &Ctx = SVB.getContext();
+ assert(CE->arg_begin() + 1 == CE->arg_end());
+ DefinedOrUnknownSVal V =
+ state->getSVal(*(CE->arg_begin()), LCtx).castAs<DefinedOrUnknownSVal>();
+
+ llvm::APFloat PInf = llvm::APFloat::getInf(
+ Ctx.getFloatTypeSemantics((*(CE->arg_begin()))->getType()), false);
+ DefinedOrUnknownSVal SPInf = SVB.makeFloatVal(PInf);
+ DefinedOrUnknownSVal isPInf = SVB.evalEQ(state, V, SPInf);
+ if (isPInf.isConstant(1)) {
+ C.addTransition(state->BindExpr(CE, LCtx, isPInf));
+ return true;
+ }
+
+ llvm::APFloat NInf = llvm::APFloat::getInf(
+ Ctx.getFloatTypeSemantics((*(CE->arg_begin()))->getType()), true);
+ DefinedOrUnknownSVal SNInf = SVB.makeFloatVal(NInf);
+ DefinedOrUnknownSVal isNInf = SVB.evalEQ(state, V, SNInf);
+ if (isPInf.isZeroConstant() && isNInf.isConstant(1)) {
+ C.addTransition(state->BindExpr(CE, LCtx, isNInf));
+ return true;
+ }
+
+ // TODO: FIXME
+ // This should be BO_LOr for (V == -\inf) || (V == \inf), but logical
+ // operations are handled much earlier during ExplodedGraph generation.
+ // However, since both sides are Boolean/Int1Ty, we can use bitwise or.
+ // If/when this is fixed, also remove the explicit short-circuits above.
+ SVal isInf = SVB.evalBinOp(state, BO_Or, isPInf, isNInf,
+ SVB.getConditionType());
+ C.addTransition(state->BindExpr(CE, LCtx, isInf));
+ return true;
+ }
+
+ // TODO: FIXME
+ // IEEE-754 changes evaluation of direct comparison to NaN, which makes it
+ // difficult to express NaN constraints for the symbolic executor.
+ // As a workaround, express this as V != V, for which only NaN satisfies.
+ case Builtin::BI__builtin_isnan: {
+ SValBuilder &SVB = C.getSValBuilder();
+ assert(CE->arg_begin() + 1 == CE->arg_end());
+ SVal V = state->getSVal(*(CE->arg_begin()), LCtx);
+ SVal isNaN = SVB.evalBinOp(state, BO_NE, V, V, SVB.getConditionType());
+ C.addTransition(state->BindExpr(CE, LCtx, isNaN));
+ return true;
+ }
+
case Builtin::BI__builtin_unpredictable:
case Builtin::BI__builtin_expect:
case Builtin::BI__builtin_assume_aligned:
Index: include/clang/StaticAnalyzer/Core/PathSensitive/Symbols.def
===================================================================
--- include/clang/StaticAnalyzer/Core/PathSensitive/Symbols.def
+++ include/clang/StaticAnalyzer/Core/PathSensitive/Symbols.def
@@ -37,6 +37,8 @@
ABSTRACT_SYMBOL(BinarySymExpr, SymExpr)
SYMBOL(IntSymExpr, BinarySymExpr)
SYMBOL(SymIntExpr, BinarySymExpr)
+ SYMBOL(FloatSymExpr, BinarySymExpr)
+ SYMBOL(SymFloatExpr, BinarySymExpr)
SYMBOL(SymSymExpr, BinarySymExpr)
SYMBOL_RANGE(BINARYSYMEXPRS, IntSymExprKind, SymSymExprKind)
Index: include/clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h
===================================================================
--- include/clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h
+++ include/clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h
@@ -391,6 +391,77 @@
}
};
+
+/// \brief Represents a symbolic expression like 'x' + 3.0.
+class SymFloatExpr : public BinarySymExpr {
+ const SymExpr *LHS;
+ const llvm::APFloat& RHS;
+
+public:
+ SymFloatExpr(const SymExpr *lhs, BinaryOperator::Opcode op,
+ const llvm::APFloat& rhs, QualType t)
+ : BinarySymExpr(SymFloatExprKind, op, t), LHS(lhs), RHS(rhs) {}
+
+ void dumpToStream(raw_ostream &os) const override;
+
+ const SymExpr *getLHS() const { return LHS; }
+ const llvm::APFloat &getRHS() const { return RHS; }
+
+ static void Profile(llvm::FoldingSetNodeID& ID, const SymExpr *lhs,
+ BinaryOperator::Opcode op, const llvm::APFloat& rhs,
+ QualType t) {
+ ID.AddInteger((unsigned) SymFloatExprKind);
+ ID.AddPointer(lhs);
+ ID.AddInteger(op);
+ ID.AddPointer(&rhs);
+ ID.Add(t);
+ }
+
+ void Profile(llvm::FoldingSetNodeID& ID) override {
+ Profile(ID, LHS, getOpcode(), RHS, getType());
+ }
+
+ // Implement isa<T> support.
+ static inline bool classof(const SymExpr *SE) {
+ return SE->getKind() == SymFloatExprKind;
+ }
+};
+
+/// \brief Represents a symbolic expression like 3.0 - 'x'.
+class FloatSymExpr : public BinarySymExpr {
+ const llvm::APFloat& LHS;
+ const SymExpr *RHS;
+
+public:
+ FloatSymExpr(const llvm::APFloat& lhs, BinaryOperator::Opcode op,
+ const SymExpr *rhs, QualType t)
+ : BinarySymExpr(FloatSymExprKind, op, t), LHS(lhs), RHS(rhs) {}
+
+ void dumpToStream(raw_ostream &os) const override;
+
+ const SymExpr *getRHS() const { return RHS; }
+ const llvm::APFloat &getLHS() const { return LHS; }
+
+ static void Profile(llvm::FoldingSetNodeID& ID, const llvm::APFloat& lhs,
+ BinaryOperator::Opcode op, const SymExpr *rhs,
+ QualType t) {
+ ID.AddInteger((unsigned) FloatSymExprKind);
+ ID.AddPointer(&lhs);
+ ID.AddInteger(op);
+ ID.AddPointer(rhs);
+ ID.Add(t);
+ }
+
+ void Profile(llvm::FoldingSetNodeID& ID) override {
+ Profile(ID, LHS, getOpcode(), RHS, getType());
+ }
+
+ // Implement isa<T> support.
+ static inline bool classof(const SymExpr *SE) {
+ return SE->getKind() == FloatSymExprKind;
+ }
+};
+
/// \brief Represents a symbolic expression like 'x' + 'y'.
class SymSymExpr : public BinarySymExpr {
const SymExpr *LHS;
@@ -497,6 +568,20 @@
BinaryOperator::Opcode op,
const SymExpr *rhs, QualType t);
+ const SymFloatExpr *getSymFloatExpr(const SymExpr *lhs,
+ BinaryOperator::Opcode op,
+ const llvm::APFloat& rhs, QualType t);
+
+ const SymFloatExpr *getSymFloatExpr(const SymExpr &lhs,
+ BinaryOperator::Opcode op,
+ const llvm::APFloat& rhs, QualType t) {
+ return getSymFloatExpr(&lhs, op, rhs, t);
+ }
+
+ const FloatSymExpr *getFloatSymExpr(const llvm::APFloat& lhs,
+ BinaryOperator::Opcode op,
+ const SymExpr *rhs, QualType t);
+
const SymSymExpr *getSymSymExpr(const SymExpr *lhs, BinaryOperator::Opcode op,
const SymExpr *rhs, QualType t);
Index: include/clang/StaticAnalyzer/Core/PathSensitive/SVals.h
===================================================================
--- include/clang/StaticAnalyzer/Core/PathSensitive/SVals.h
+++ include/clang/StaticAnalyzer/Core/PathSensitive/SVals.h
@@ -141,10 +141,14 @@
return getRawKind() > UnknownValKind;
}
+ bool isFloat() const;
+
bool isConstant() const;
bool isConstant(int I) const;
+ bool isConstant(llvm::APFloat &V) const;
+
bool isZeroConstant() const;
/// hasConjuredSymbol - If this SVal wraps a conjured symbol, return true;
@@ -193,7 +197,7 @@
return SymExpr::symbol_iterator();
}
- SymExpr::symbol_iterator symbol_end() const {
+ SymExpr::symbol_iterator symbol_end() const {
return SymExpr::symbol_end();
}
};
@@ -216,26 +220,26 @@
// tautologically false.
bool isUndef() const = delete;
bool isValid() const = delete;
-
+
protected:
DefinedOrUnknownSVal() {}
explicit DefinedOrUnknownSVal(const void *d, bool isLoc, unsigned ValKind)
: SVal(d, isLoc, ValKind) {}
-
+
explicit DefinedOrUnknownSVal(BaseKind k, void *D = nullptr)
: SVal(k, D) {}
-
+
private:
friend class SVal;
static bool isKind(const SVal& V) {
return !V.isUndef();
}
};
-
+
class UnknownVal : public DefinedOrUnknownSVal {
public:
explicit UnknownVal() : DefinedOrUnknownSVal(UnknownValKind) {}
-
+
private:
friend class SVal;
static bool isKind(const SVal &V) {
@@ -305,7 +309,7 @@
void dumpToStream(raw_ostream &Out) const;
static inline bool isLocType(QualType T) {
- return T->isAnyPointerType() || T->isBlockPointerType() ||
+ return T->isAnyPointerType() || T->isBlockPointerType() ||
T->isReferenceType() || T->isNullPtrType();
}
@@ -378,6 +382,34 @@
}
};
+/// \brief Value representing floating-point constant.
+class ConcreteFloat : public NonLoc {
+public:
+ explicit ConcreteFloat(const llvm::APFloat& V) : NonLoc(ConcreteFloatKind, &V) {}
+
+ const llvm::APFloat& getValue() const {
+ return *static_cast<const llvm::APFloat*>(Data);
+ }
+
+ // Transfer functions for binary/unary operations on ConcreteFloats.
+ SVal evalBinOp(SValBuilder &svalBuilder, BinaryOperator::Opcode Op,
+ const ConcreteFloat& R) const;
+
+ ConcreteFloat evalMinus(SValBuilder &svalBuilder) const;
+
+private:
+ friend class SVal;
+ ConcreteFloat() {}
+ static bool isKind(const SVal& V) {
+ return V.getBaseKind() == NonLocKind &&
+ V.getSubKind() == ConcreteFloatKind;
+ }
+
+ static bool isKind(const NonLoc& V) {
+ return V.getSubKind() == ConcreteFloatKind;
+ }
+};
+
class LocAsInteger : public NonLoc {
friend class ento::SValBuilder;
Index: include/clang/StaticAnalyzer/Core/PathSensitive/SVals.def
===================================================================
--- include/clang/StaticAnalyzer/Core/PathSensitive/SVals.def
+++ include/clang/StaticAnalyzer/Core/PathSensitive/SVals.def
@@ -63,6 +63,7 @@
ABSTRACT_SVAL_WITH_KIND(NonLoc, DefinedSVal)
NONLOC_SVAL(CompoundVal, NonLoc)
NONLOC_SVAL(ConcreteInt, NonLoc)
+ NONLOC_SVAL(ConcreteFloat, NonLoc)
NONLOC_SVAL(LazyCompoundVal, NonLoc)
NONLOC_SVAL(LocAsInteger, NonLoc)
NONLOC_SVAL(SymbolVal, NonLoc)
Index: include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h
===================================================================
--- include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h
+++ include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h
@@ -33,7 +33,7 @@
virtual void anchor();
protected:
ASTContext &Context;
-
+
/// Manager of APSInt values.
BasicValueFactory BasicVals;
@@ -47,7 +47,7 @@
/// The scalar type to use for array indices.
const QualType ArrayIndexTy;
-
+
/// The width of the scalar type used for array indices.
const unsigned ArrayIndexWidth;
@@ -109,34 +109,38 @@
virtual SVal evalBinOpLN(ProgramStateRef state, BinaryOperator::Opcode op,
Loc lhs, NonLoc rhs, QualType resultTy) = 0;
- /// Evaluates a given SVal. If the SVal has only one possible (integer) value,
+ /// Evaluates a given SVal. If the SVal has only one possible integer value,
/// that value is returned. Otherwise, returns NULL.
virtual const llvm::APSInt *getKnownValue(ProgramStateRef state, SVal val) = 0;
+ /// Evaluates a given SVal. If the SVal has only one possible float value,
+ /// that value is returned. Otherwise, returns NULL.
+ virtual const llvm::APFloat *getKnownFloatValue(ProgramStateRef state, SVal val) = 0;
+
/// Simplify symbolic expressions within a given SVal. Return an SVal
/// that represents the same value, but is hopefully easier to work with
/// than the original SVal.
virtual SVal simplifySVal(ProgramStateRef State, SVal Val) = 0;
-
+
/// Constructs a symbolic expression for two non-location values.
SVal makeSymExprValNN(ProgramStateRef state, BinaryOperator::Opcode op,
NonLoc lhs, NonLoc rhs, QualType resultTy);
SVal evalBinOp(ProgramStateRef state, BinaryOperator::Opcode op,
SVal lhs, SVal rhs, QualType type);
-
+
DefinedOrUnknownSVal evalEQ(ProgramStateRef state, DefinedOrUnknownSVal lhs,
DefinedOrUnknownSVal rhs);
ASTContext &getContext() { return Context; }
const ASTContext &getContext() const { return Context; }
ProgramStateManager &getStateManager() { return StateMgr; }
-
+
QualType getConditionType() const {
return Context.getLangOpts().CPlusPlus ? Context.BoolTy : Context.IntTy;
}
-
+
QualType getArrayIndexType() const {
return ArrayIndexTy;
}
@@ -188,7 +192,7 @@
const LocationContext *LCtx,
QualType type,
unsigned count);
-
+
DefinedOrUnknownSVal conjureSymbolVal(const Stmt *stmt,
const LocationContext *LCtx,
QualType type,
@@ -212,7 +216,7 @@
DefinedSVal getMemberPointer(const DeclaratorDecl *DD);
DefinedSVal getFunctionPointer(const FunctionDecl *func);
-
+
DefinedSVal getBlockPointer(const BlockDecl *block, CanQualType locTy,
const LocationContext *locContext,
unsigned blockCount);
@@ -227,7 +231,7 @@
return nonloc::CompoundVal(BasicVals.getCompoundValData(type, vals));
}
- NonLoc makeLazyCompoundVal(const StoreRef &store,
+ NonLoc makeLazyCompoundVal(const StoreRef &store,
const TypedValueRegion *region) {
return nonloc::LazyCompoundVal(
BasicVals.getLazyCompoundValData(store, region));
@@ -295,13 +299,33 @@
return nonloc::LocAsInteger(BasicVals.getPersistentSValWithData(loc, bits));
}
+ nonloc::ConcreteFloat makeFloatVal(const FloatingLiteral *F) {
+ return nonloc::ConcreteFloat(BasicVals.getValue(F->getValue()));
+ }
+
+ nonloc::ConcreteFloat makeFloatVal(const llvm::APFloat &F) {
+ return nonloc::ConcreteFloat(BasicVals.getValue(F));
+ }
+
+ DefinedSVal makeFloatVal(uint64_t V, QualType T) {
+ assert(!Loc::isLocType(T));
+ return nonloc::ConcreteFloat(BasicVals.getValue(V,
+ Context.getFloatTypeSemantics(T)));
+ }
+
NonLoc makeNonLoc(const SymExpr *lhs, BinaryOperator::Opcode op,
const llvm::APSInt& rhs, QualType type);
NonLoc makeNonLoc(const llvm::APSInt& rhs, BinaryOperator::Opcode op,
const SymExpr *lhs, QualType type);
NonLoc makeNonLoc(const SymExpr *lhs, BinaryOperator::Opcode op,
+ const llvm::APFloat& rhs, QualType type);
+
+ NonLoc makeNonLoc(const llvm::APFloat& lhs, BinaryOperator::Opcode op,
+ const SymExpr *rhs, QualType type);
+
+ NonLoc makeNonLoc(const SymExpr *lhs, BinaryOperator::Opcode op,
const SymExpr *rhs, QualType type);
/// \brief Create a NonLoc value for cast.
Index: include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
===================================================================
--- include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
+++ include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
@@ -139,6 +139,16 @@
return nullptr;
}
+ /// \brief If a symbol is perfectly constrained to a constant, attempt
+ /// to return the concrete value.
+ ///
+ /// Note that a ConstraintManager is not obligated to return a concretized
+ /// value for a symbol, even if it is perfectly constrained.
+ virtual const llvm::APFloat* getSymFloatVal(ProgramStateRef state,
+ SymbolRef sym) const {
+ return nullptr;
+ }
+
/// Scan all symbols referenced by the constraints. If the symbol is not
/// alive, remove it.
virtual ProgramStateRef removeDeadBindings(ProgramStateRef state,
@@ -159,6 +169,11 @@
return checkNull(State, Sym);
}
+ /// canReasonAbout - Not all ConstraintManagers can reason about floating-
+ /// point values. Instead of first instantiating a floating-point SVal to
+ /// query whether it is supported, use this to ask directly.
+ virtual bool canReasonAboutFloat() 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: include/clang/StaticAnalyzer/Core/PathSensitive/BasicValueFactory.h
===================================================================
--- include/clang/StaticAnalyzer/Core/PathSensitive/BasicValueFactory.h
+++ include/clang/StaticAnalyzer/Core/PathSensitive/BasicValueFactory.h
@@ -89,11 +89,14 @@
class BasicValueFactory {
typedef llvm::FoldingSet<llvm::FoldingSetNodeWrapper<llvm::APSInt> >
APSIntSetTy;
+ typedef llvm::FoldingSet<llvm::FoldingSetNodeWrapper<llvm::APFloat> >
+ APFloatSetTy;
ASTContext &Ctx;
llvm::BumpPtrAllocator& BPAlloc;
APSIntSetTy APSIntSet;
+ APFloatSetTy APFloatSet;
void * PersistentSVals;
void * PersistentSValPairs;
@@ -121,6 +124,9 @@
const llvm::APSInt& getValue(const llvm::APInt& X, bool isUnsigned);
const llvm::APSInt& getValue(uint64_t X, QualType T);
+ const llvm::APFloat &getValue(const llvm::APFloat& X);
+ const llvm::APFloat &getValue(int64_t X, const llvm::fltSemantics &S);
+
/// Returns the type of the APSInt used to store values of the given QualType.
APSIntType getAPSIntType(QualType T) const {
assert(T->isIntegralOrEnumerationType() || Loc::isLocType(T));
@@ -138,15 +144,63 @@
return getValue(TargetType.convert(From));
}
-
+
const llvm::APSInt &Convert(QualType T, const llvm::APSInt &From) {
APSIntType TargetType = getAPSIntType(T);
if (TargetType == APSIntType(From))
return From;
-
+
return getValue(TargetType.convert(From));
}
+ const llvm::APFloat &Convert(const llvm::APSInt &From,
+ const llvm::fltSemantics &S) {
+ llvm::APFloat To(S, llvm::APFloat::uninitialized);
+ assert(Convert(To, From) && "Failed to convert integer to floating-point!");
+ return getValue(To);
+ }
+
+ const llvm::APFloat &Convert(QualType T, const llvm::APFloat &From) {
+ bool lossOfPrecision;
+ llvm::APFloat To = From;
+#ifndef NDEBUG
+ llvm::APFloat::opStatus Status = To.convert(Ctx.getFloatTypeSemantics(T),
+ llvm::APFloat::rmNearestTiesToEven, &lossOfPrecision);
+#else
+ To.convert(Ctx.getFloatTypeSemantics(T),
+ llvm::APFloat::rmNearestTiesToEven, &lossOfPrecision);
+#endif
+ assert(!(Status & (llvm::APFloat::opOverflow | llvm::APFloat::opInvalidOp)));
+ return getValue(To);
+ }
+
+ /// Fills an existing APFloat with the floating-point representation of an
+ /// APSInt. Returns true if the conversion is successful.
+ static bool Convert(llvm::APFloat &Float, const llvm::APSInt &Int) {
+ llvm::APFloat::opStatus Status = Float.convertFromAPInt(
+ Int, Int.isSigned(), llvm::APFloat::rmNearestTiesToEven);
+ // Cannot be represented in destination type, this is undefined behavior
+ if (llvm::APFloat::opOverflow & Status ||
+ llvm::APFloat::opInvalidOp & Status)
+ return false;
+
+ return true;
+ }
+
+ /// Fills an existing APSInt with the integer representation of an
+ /// APFloat. Returns true if the conversion is successful.
+ static bool Convert(llvm::APSInt &Int, const llvm::APFloat &Float) {
+ bool isExact;
+ llvm::APFloat::opStatus Status = Float.convertToInteger(
+ Int, llvm::APFloat::rmNearestTiesToEven, &isExact);
+ // Cannot be represented in destination type, this is undefined behavior
+ if (llvm::APFloat::opOverflow & Status ||
+ llvm::APFloat::opInvalidOp & Status)
+ return false;
+
+ return true;
+ }
+
const llvm::APSInt& getIntValue(uint64_t X, bool isUnsigned) {
QualType T = isUnsigned ? Ctx.UnsignedIntTy : Ctx.IntTy;
return getValue(X, T);
@@ -229,8 +283,16 @@
const nonloc::PointerToMember &PTM);
const llvm::APSInt* evalAPSInt(BinaryOperator::Opcode Op,
- const llvm::APSInt& V1,
- const llvm::APSInt& V2);
+ const llvm::APSInt& V1,
+ const llvm::APSInt& V2);
+
+ const llvm::APFloat* evalAPFloat(BinaryOperator::Opcode Op,
+ const llvm::APFloat& V1,
+ const llvm::APFloat& V2);
+
+ const llvm::APSInt* evalAPFloatComparison(BinaryOperator::Opcode Op,
+ const llvm::APFloat& V1,
+ const llvm::APFloat& V2);
const std::pair<SVal, uintptr_t>&
getPersistentSValWithData(const SVal& V, uintptr_t Data);
Index: include/clang/StaticAnalyzer/Checkers/Checkers.td
===================================================================
--- include/clang/StaticAnalyzer/Checkers/Checkers.td
+++ include/clang/StaticAnalyzer/Checkers/Checkers.td
@@ -147,6 +147,10 @@
HelpText<"Loss of sign/precision in implicit conversions">,
DescFile<"ConversionChecker.cpp">;
+def FloatingPointMathChecker : Checker<"FPMath">,
+ HelpText<"Check for domain errors in floating-point math functions">,
+ DescFile<"FloatingPointMath.cpp">;
+
def IdenticalExprChecker : Checker<"IdenticalExpr">,
HelpText<"Warn about unintended use of identical expressions in operators">,
DescFile<"IdenticalExprChecker.cpp">;
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
