Index: test/Analysis/std-c-library-functions.c
===================================================================
--- test/Analysis/std-c-library-functions.c
+++ test/Analysis/std-c-library-functions.c
@@ -57,8 +57,7 @@
size_t y = fread(buf, sizeof(int), 10, fp);
clang_analyzer_eval(y <= 10); // expected-warning{{TRUE}}
size_t z = fwrite(buf, sizeof(int), y, fp);
- // FIXME: should be TRUE once symbol-symbol constraint support is improved.
- clang_analyzer_eval(z <= y); // expected-warning{{UNKNOWN}}
+ clang_analyzer_eval(z <= y); // expected-warning{{TRUE}}
}
ssize_t getline(char **, size_t *, FILE *);
Index: test/Analysis/range_casts.c
===================================================================
--- test/Analysis/range_casts.c
+++ test/Analysis/range_casts.c
@@ -67,7 +67,7 @@
{
unsigned index = -1;
if (index < foo) index = foo;
- if (index - 1 == 0) // Was not reached prior fix.
+ if (index - 1 == 0)
clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
else
clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
@@ -87,7 +87,7 @@
{
unsigned index = -1;
if (index < foo) index = foo;
- if (index - 1L == 0L) // Was not reached prior fix.
+ if (index - 1L == 0L)
clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
else
clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
@@ -117,7 +117,7 @@
{
unsigned index = -1;
if (index < foo) index = foo;
- if (index - 1UL == 0L) // Was not reached prior fix.
+ if (index - 1UL == 0L)
clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
else
clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
Index: test/Analysis/plist-macros.cpp
===================================================================
--- test/Analysis/plist-macros.cpp
+++ test/Analysis/plist-macros.cpp
@@ -1,7 +1,7 @@
// RUN: %clang_analyze_cc1 -analyzer-checker=core,unix -analyzer-eagerly-assume -verify %s
-// RUN: %clang_analyze_cc1 -analyzer-checker=core,unix -analyzer-eagerly-assume -analyzer-output=plist-multi-file -analyzer-config path-diagnostics-alternate=ture %s -o %t.plist
+// RUN: %clang_analyze_cc1 -analyzer-checker=core,unix -analyzer-eagerly-assume -analyzer-output=plist-multi-file -analyzer-config path-diagnostics-alternate=true %s -o %t.plist
// RUN: FileCheck --input-file=%t.plist %s
-
+// REQUIRES: !z3
typedef __typeof(sizeof(int)) size_t;
void *malloc(size_t);
@@ -11,13 +11,13 @@
y++;
y--;
mallocmemory
- y++;
+ y++;
y++;
delete x; // expected-warning {{Memory allocated by malloc() should be deallocated by free(), not 'delete'}}
}
void macroIsFirstInFunction(int y) {
- mallocmemory
+ mallocmemory
y++; // expected-warning {{Potential leak of memory pointed to by 'x'}}
}
@@ -39,7 +39,7 @@
return *p; // expected-warning {{Dereference of null pointer}}
}
-#define macroWithArg(mp) mp==0
+#define macroWithArg(mp) mp==0
int macroWithArgInExpression(int *p, int y) {;
y++;
if (macroWithArg(p))
@@ -85,6 +85,7 @@
void test2(int *p) {
CALL_FN(p);
}
+
// CHECK: diagnostics
// CHECK-NEXT:
// CHECK-NEXT:
@@ -636,6 +637,69 @@
// CHECK-NEXT: end
// CHECK-NEXT:
// CHECK-NEXT:
+// CHECK-NEXT: line36
+// CHECK-NEXT: col7
+// CHECK-NEXT: file0
+// CHECK-NEXT:
+// CHECK-NEXT:
+// CHECK-NEXT: line36
+// CHECK-NEXT: col7
+// CHECK-NEXT: file0
+// CHECK-NEXT:
+// CHECK-NEXT:
+// CHECK-NEXT:
+// CHECK-NEXT:
+// CHECK-NEXT:
+// CHECK-NEXT:
+// CHECK-NEXT: kindevent
+// CHECK-NEXT: location
+// CHECK-NEXT:
+// CHECK-NEXT: line36
+// CHECK-NEXT: col7
+// CHECK-NEXT: file0
+// CHECK-NEXT:
+// CHECK-NEXT: ranges
+// CHECK-NEXT:
+// CHECK-NEXT:
+// CHECK-NEXT:
+// CHECK-NEXT: line36
+// CHECK-NEXT: col7
+// CHECK-NEXT: file0
+// CHECK-NEXT:
+// CHECK-NEXT:
+// CHECK-NEXT: line36
+// CHECK-NEXT: col25
+// CHECK-NEXT: file0
+// CHECK-NEXT:
+// CHECK-NEXT:
+// CHECK-NEXT:
+// CHECK-NEXT: depth0
+// CHECK-NEXT: extended_message
+// CHECK-NEXT: Assuming the condition is true
+// CHECK-NEXT: message
+// CHECK-NEXT: Assuming the condition is true
+// CHECK-NEXT:
+// CHECK-NEXT:
+// CHECK-NEXT: kindcontrol
+// CHECK-NEXT: edges
+// CHECK-NEXT:
+// CHECK-NEXT:
+// CHECK-NEXT: start
+// CHECK-NEXT:
+// CHECK-NEXT:
+// CHECK-NEXT: line36
+// CHECK-NEXT: col7
+// CHECK-NEXT: file0
+// CHECK-NEXT:
+// CHECK-NEXT:
+// CHECK-NEXT: line36
+// CHECK-NEXT: col7
+// CHECK-NEXT: file0
+// CHECK-NEXT:
+// CHECK-NEXT:
+// CHECK-NEXT: end
+// CHECK-NEXT:
+// CHECK-NEXT:
// CHECK-NEXT: line37
// CHECK-NEXT: col5
// CHECK-NEXT: file0
Index: test/Analysis/plist-macros-z3.cpp
===================================================================
--- test/Analysis/plist-macros-z3.cpp
+++ test/Analysis/plist-macros-z3.cpp
@@ -1,7 +1,7 @@
// RUN: %clang_analyze_cc1 -analyzer-checker=core,unix -analyzer-eagerly-assume -verify %s
-// RUN: %clang_analyze_cc1 -analyzer-checker=core,unix -analyzer-eagerly-assume -analyzer-output=plist-multi-file -analyzer-config path-diagnostics-alternate=ture %s -o %t.plist
+// RUN: %clang_analyze_cc1 -analyzer-checker=core,unix -analyzer-eagerly-assume -analyzer-output=plist-multi-file -analyzer-config path-diagnostics-alternate=true %s -o %t.plist
// RUN: FileCheck --input-file=%t.plist %s
-
+// REQUIRES: z3
typedef __typeof(sizeof(int)) size_t;
void *malloc(size_t);
@@ -11,13 +11,13 @@
y++;
y--;
mallocmemory
- y++;
+ y++;
y++;
delete x; // expected-warning {{Memory allocated by malloc() should be deallocated by free(), not 'delete'}}
}
void macroIsFirstInFunction(int y) {
- mallocmemory
+ mallocmemory
y++; // expected-warning {{Potential leak of memory pointed to by 'x'}}
}
@@ -39,7 +39,7 @@
return *p; // expected-warning {{Dereference of null pointer}}
}
-#define macroWithArg(mp) mp==0
+#define macroWithArg(mp) mp==0
int macroWithArgInExpression(int *p, int y) {;
y++;
if (macroWithArg(p))
@@ -85,6 +85,7 @@
void test2(int *p) {
CALL_FN(p);
}
+
// CHECK: diagnostics
// CHECK-NEXT:
// CHECK-NEXT:
Index: test/Analysis/loop-unrolling.cpp
===================================================================
--- test/Analysis/loop-unrolling.cpp
+++ test/Analysis/loop-unrolling.cpp
@@ -252,7 +252,11 @@
int nested_inlined_no_unroll1() {
int k;
for (int i = 0; i < 9; i++) {
+#ifdef ANALYZER_CM_Z3
+ clang_analyzer_numTimesReached(); // expected-warning {{13}}
+#else
clang_analyzer_numTimesReached(); // expected-warning {{15}}
+#endif
k = simple_unknown_bound_loop(); // reevaluation without inlining, splits the state as well
}
int a = 22 / k; // no-warning
Index: test/Analysis/explain-svals.cpp
===================================================================
--- test/Analysis/explain-svals.cpp
+++ test/Analysis/explain-svals.cpp
@@ -69,7 +69,7 @@
static int stat;
clang_analyzer_explain(x + 1); // expected-warning-re{{{{^\(argument 'x'\) \+ 1$}}}}
clang_analyzer_explain(1 + y); // expected-warning-re{{{{^\(argument 'y'\) \+ 1$}}}}
- clang_analyzer_explain(x + y); // expected-warning-re{{{{^unknown value$}}}}
+ clang_analyzer_explain(x + y); // expected-warning-re{{{{^\(argument 'x'\) \+ \(argument 'y'\)$}}}}
clang_analyzer_explain(z); // expected-warning-re{{{{^undefined value$}}}}
clang_analyzer_explain(&z); // expected-warning-re{{{{^pointer to local variable 'z'$}}}}
clang_analyzer_explain(stat); // expected-warning-re{{{{^signed 32-bit integer '0'$}}}}
Index: test/Analysis/conditional-path-notes.c
===================================================================
--- test/Analysis/conditional-path-notes.c
+++ test/Analysis/conditional-path-notes.c
@@ -77,7 +77,8 @@
void testNonDiagnosableBranchArithmetic(int a, int b) {
if (a - b) {
- // expected-note@-1 {{Taking true branch}}
+ // expected-note@-1 {{Assuming the condition is true}}
+ // expected-note@-2 {{Taking true branch}}
*(volatile int *)0 = 1; // expected-warning{{Dereference of null pointer}}
// expected-note@-1 {{Dereference of null pointer}}
}
@@ -1573,12 +1574,75 @@
// CHECK-NEXT: end
// CHECK-NEXT:
// CHECK-NEXT:
-// CHECK-NEXT: line81
+// CHECK-NEXT: line79
+// CHECK-NEXT: col7
+// CHECK-NEXT: file0
+// CHECK-NEXT:
+// CHECK-NEXT:
+// CHECK-NEXT: line79
+// CHECK-NEXT: col7
+// CHECK-NEXT: file0
+// CHECK-NEXT:
+// CHECK-NEXT:
+// CHECK-NEXT:
+// CHECK-NEXT:
+// CHECK-NEXT:
+// CHECK-NEXT:
+// CHECK-NEXT: kindevent
+// CHECK-NEXT: location
+// CHECK-NEXT:
+// CHECK-NEXT: line79
+// CHECK-NEXT: col7
+// CHECK-NEXT: file0
+// CHECK-NEXT:
+// CHECK-NEXT: ranges
+// CHECK-NEXT:
+// CHECK-NEXT:
+// CHECK-NEXT:
+// CHECK-NEXT: line79
+// CHECK-NEXT: col7
+// CHECK-NEXT: file0
+// CHECK-NEXT:
+// CHECK-NEXT:
+// CHECK-NEXT: line79
+// CHECK-NEXT: col11
+// CHECK-NEXT: file0
+// CHECK-NEXT:
+// CHECK-NEXT:
+// CHECK-NEXT:
+// CHECK-NEXT: depth0
+// CHECK-NEXT: extended_message
+// CHECK-NEXT: Assuming the condition is true
+// CHECK-NEXT: message
+// CHECK-NEXT: Assuming the condition is true
+// CHECK-NEXT:
+// CHECK-NEXT:
+// CHECK-NEXT: kindcontrol
+// CHECK-NEXT: edges
+// CHECK-NEXT:
+// CHECK-NEXT:
+// CHECK-NEXT: start
+// CHECK-NEXT:
+// CHECK-NEXT:
+// CHECK-NEXT: line79
+// CHECK-NEXT: col7
+// CHECK-NEXT: file0
+// CHECK-NEXT:
+// CHECK-NEXT:
+// CHECK-NEXT: line79
+// CHECK-NEXT: col7
+// CHECK-NEXT: file0
+// CHECK-NEXT:
+// CHECK-NEXT:
+// CHECK-NEXT: end
+// CHECK-NEXT:
+// CHECK-NEXT:
+// CHECK-NEXT: line82
// CHECK-NEXT: col5
// CHECK-NEXT: file0
// CHECK-NEXT:
// CHECK-NEXT:
-// CHECK-NEXT: line81
+// CHECK-NEXT: line82
// CHECK-NEXT: col5
// CHECK-NEXT: file0
// CHECK-NEXT:
@@ -1594,25 +1658,25 @@
// CHECK-NEXT: start
// CHECK-NEXT:
// CHECK-NEXT:
-// CHECK-NEXT: line81
+// CHECK-NEXT: line82
// CHECK-NEXT: col5
// CHECK-NEXT: file0
// CHECK-NEXT:
// CHECK-NEXT:
-// CHECK-NEXT: line81
+// CHECK-NEXT: line82
// CHECK-NEXT: col5
// CHECK-NEXT: file0
// CHECK-NEXT:
// CHECK-NEXT:
// CHECK-NEXT: end
// CHECK-NEXT:
// CHECK-NEXT:
-// CHECK-NEXT: line81
+// CHECK-NEXT: line82
// CHECK-NEXT: col24
// CHECK-NEXT: file0
// CHECK-NEXT:
// CHECK-NEXT:
-// CHECK-NEXT: line81
+// CHECK-NEXT: line82
// CHECK-NEXT: col24
// CHECK-NEXT: file0
// CHECK-NEXT:
@@ -1624,20 +1688,20 @@
// CHECK-NEXT: kindevent
// CHECK-NEXT: location
// CHECK-NEXT:
-// CHECK-NEXT: line81
+// CHECK-NEXT: line82
// CHECK-NEXT: col24
// CHECK-NEXT: file0
// CHECK-NEXT:
// CHECK-NEXT: ranges
// CHECK-NEXT:
// CHECK-NEXT:
// CHECK-NEXT:
-// CHECK-NEXT: line81
+// CHECK-NEXT: line82
// CHECK-NEXT: col5
// CHECK-NEXT: file0
// CHECK-NEXT:
// CHECK-NEXT:
-// CHECK-NEXT: line81
+// CHECK-NEXT: line82
// CHECK-NEXT: col26
// CHECK-NEXT: file0
// CHECK-NEXT:
@@ -1658,10 +1722,10 @@
// CHECK-NEXT: issue_hash_content_of_line_in_contextf56671e5f67c73abef619b56f7c29fa4
// CHECK-NEXT: issue_context_kindfunction
// CHECK-NEXT: issue_contexttestNonDiagnosableBranchArithmetic
-// CHECK-NEXT: issue_hash_function_offset3
+// CHECK-NEXT: issue_hash_function_offset4
// CHECK-NEXT: location
// CHECK-NEXT:
-// CHECK-NEXT: line81
+// CHECK-NEXT: line82
// CHECK-NEXT: col24
// CHECK-NEXT: file0
// CHECK-NEXT:
Index: test/Analysis/bool-assignment.c
===================================================================
--- test/Analysis/bool-assignment.c
+++ test/Analysis/bool-assignment.c
@@ -43,15 +43,11 @@
return;
}
if (y > 200 && y < 250) {
-#ifdef ANALYZER_CM_Z3
BOOL x = y; // expected-warning {{Assignment of a non-Boolean value}}
-#else
- BOOL x = y; // no-warning
-#endif
return;
}
if (y >= 127 && y < 150) {
- BOOL x = y; // expected-warning{{Assignment of a non-Boolean value}}
+ BOOL x = y; // expected-warning {{Assignment of a non-Boolean value}}
return;
}
if (y > 1) {
Index: test/Analysis/bitwise-ops.c
===================================================================
--- test/Analysis/bitwise-ops.c
+++ test/Analysis/bitwise-ops.c
@@ -7,10 +7,9 @@
// Sanity check
CHECK(x); // expected-warning{{TRUE}}
CHECK(x & 1); // expected-warning{{TRUE}}
-
- // False positives due to SValBuilder giving up on certain kinds of exprs.
- CHECK(1 - x); // expected-warning{{UNKNOWN}}
- CHECK(x & y); // expected-warning{{UNKNOWN}}
+
+ CHECK(1 - x); // expected-warning{{TRUE}}
+ CHECK(x & y); // expected-warning{{TRUE}}
}
int testConstantShifts_PR18073(int which) {
@@ -29,4 +28,4 @@
default:
return 0;
}
-}
\ No newline at end of file
+}
Index: test/Analysis/analyzer_test.py
===================================================================
--- test/Analysis/analyzer_test.py
+++ test/Analysis/analyzer_test.py
@@ -1,3 +1,4 @@
+import copy
import lit.formats
import lit.TestRunner
@@ -8,18 +9,21 @@
results = []
# Parse any test requirements ('REQUIRES: ')
- saved_test = test
+ saved_test = copy.deepcopy(test)
lit.TestRunner.parseIntegratedTestScript(test)
+ # If the test does not require z3, drop it from the available features
+ # to satisfy tests that explicitly require !z3
if 'z3' not in test.requires:
+ test.config.available_features.discard('z3')
results.append(self.executeWithAnalyzeSubstitution(
- saved_test, litConfig, '-analyzer-constraints=range'))
+ test, litConfig, '-analyzer-constraints=range'))
- if results[-1].code == lit.Test.FAIL:
+ if results[-1].code != lit.Test.PASS:
return results[-1]
# If z3 backend available, add an additional run line for it
- if test.config.clang_staticanalyzer_z3 == '1':
+ if test.config.clang_staticanalyzer_z3 == '1' and '!z3' not in test.requires:
results.append(self.executeWithAnalyzeSubstitution(
saved_test, litConfig, '-analyzer-constraints=z3 -DANALYZER_CM_Z3'))
Index: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
===================================================================
--- lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
+++ lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
@@ -987,6 +987,10 @@
// TODO: Refactor to put elsewhere
QualType getAPSIntType(const llvm::APSInt &Int) const;
+ // Fix the input APSInt if it is has a bitwidth of 1, and set the type.
+ const llvm::APSInt &fixAPSInt(const llvm::APSInt &Int, llvm::APSInt &NewInt,
+ QualType *Ty = nullptr) const;
+
// Perform implicit type conversion on binary symbolic expressions.
// May modify all input parameters.
// TODO: Refactor to use built-in conversion functions
@@ -1037,28 +1041,29 @@
QualType RetTy;
// The expression may be casted, so we cannot call getZ3DataExpr() directly
Z3Expr Exp = getZ3Expr(Sym, &RetTy);
-
- assert((getAPSIntType(From) == getAPSIntType(To)) &&
- "Range values have different types!");
- QualType RTy = getAPSIntType(From);
- bool isSignedTy = RetTy->isSignedIntegerOrEnumerationType();
- Z3Expr FromExp = Z3Expr::fromAPSInt(From);
- Z3Expr ToExp = Z3Expr::fromAPSInt(To);
+ QualType LTy;
+ llvm::APSInt NewFromInt;
+ Z3Expr FromExp = Z3Expr::fromAPSInt(fixAPSInt(From, NewFromInt, <y));
// Construct single (in)equality
if (From == To)
return assumeZ3Expr(State, Sym,
getZ3BinExpr(Exp, RetTy, InRange ? BO_EQ : BO_NE,
- FromExp, RTy, nullptr));
+ FromExp, LTy, nullptr));
+ QualType RTy;
+ llvm::APSInt NewToInt;
+ Z3Expr ToExp = Z3Expr::fromAPSInt(fixAPSInt(To, NewToInt, &RTy));
+ assert(LTy == RTy && "Range values have different types!");
// Construct two (in)equalities, and a logical and/or
Z3Expr LHS =
- getZ3BinExpr(Exp, RetTy, InRange ? BO_GE : BO_LT, FromExp, RTy, nullptr);
+ getZ3BinExpr(Exp, RetTy, InRange ? BO_GE : BO_LT, FromExp, LTy, nullptr);
Z3Expr RHS =
getZ3BinExpr(Exp, RetTy, InRange ? BO_LE : BO_GT, ToExp, RTy, nullptr);
return assumeZ3Expr(
State, Sym,
- Z3Expr::fromBinOp(LHS, InRange ? BO_LAnd : BO_LOr, RHS, isSignedTy));
+ Z3Expr::fromBinOp(LHS, InRange ? BO_LAnd : BO_LOr, RHS,
+ RetTy->isSignedIntegerOrEnumerationType()));
}
ProgramStateRef Z3ConstraintManager::assumeSymUnsupported(ProgramStateRef State,
@@ -1145,8 +1150,8 @@
const llvm::APSInt *Z3ConstraintManager::getSymVal(ProgramStateRef State,
SymbolRef Sym) const {
- BasicValueFactory &BV = getBasicVals();
- ASTContext &Ctx = BV.getContext();
+ BasicValueFactory &BVF = getBasicVals();
+ ASTContext &Ctx = BVF.getContext();
if (const SymbolData *SD = dyn_cast(Sym)) {
QualType Ty = Sym->getType();
@@ -1180,7 +1185,7 @@
return nullptr;
// This is the only solution, store it
- return &BV.getValue(Value);
+ return &BVF.getValue(Value);
} else if (const SymbolCast *SC = dyn_cast(Sym)) {
SymbolRef CastSym = SC->getOperand();
QualType CastTy = SC->getType();
@@ -1191,7 +1196,7 @@
const llvm::APSInt *Value;
if (!(Value = getSymVal(State, CastSym)))
return nullptr;
- return &BV.Convert(SC->getType(), *Value);
+ return &BVF.Convert(SC->getType(), *Value);
} else if (const BinarySymExpr *BSE = dyn_cast(Sym)) {
const llvm::APSInt *LHS, *RHS;
if (const SymIntExpr *SIE = dyn_cast(BSE)) {
@@ -1215,7 +1220,7 @@
QualType LTy = getAPSIntType(*LHS), RTy = getAPSIntType(*RHS);
doIntTypeConversion(
ConvertedLHS, LTy, ConvertedRHS, RTy);
- return BV.evalAPSInt(BSE->getOpcode(), ConvertedLHS, ConvertedRHS);
+ return BVF.evalAPSInt(BSE->getOpcode(), ConvertedLHS, ConvertedRHS);
}
llvm_unreachable("Unsupported expression to get symbol value!");
@@ -1342,13 +1347,13 @@
BinaryOperator::Opcode Op = BSE->getOpcode();
if (const SymIntExpr *SIE = dyn_cast(BSE)) {
- RTy = getAPSIntType(SIE->getRHS());
+ llvm::APSInt NewRInt;
Z3Expr LHS = getZ3SymExpr(SIE->getLHS(), <y, hasComparison);
- Z3Expr RHS = Z3Expr::fromAPSInt(SIE->getRHS());
+ Z3Expr RHS = Z3Expr::fromAPSInt(fixAPSInt(SIE->getRHS(), NewRInt, &RTy));
return getZ3BinExpr(LHS, LTy, Op, RHS, RTy, RetTy);
} else if (const IntSymExpr *ISE = dyn_cast(BSE)) {
- LTy = getAPSIntType(ISE->getLHS());
- Z3Expr LHS = Z3Expr::fromAPSInt(ISE->getLHS());
+ llvm::APSInt NewLInt;
+ Z3Expr LHS = Z3Expr::fromAPSInt(fixAPSInt(ISE->getLHS(), NewLInt, <y));
Z3Expr RHS = getZ3SymExpr(ISE->getRHS(), &RTy, hasComparison);
return getZ3BinExpr(LHS, LTy, Op, RHS, RTy, RetTy);
} else if (const SymSymExpr *SSM = dyn_cast(BSE)) {
@@ -1402,10 +1407,30 @@
return Ctx.getIntTypeForBitwidth(Int.getBitWidth(), Int.isSigned());
}
+const llvm::APSInt &Z3ConstraintManager::fixAPSInt(const llvm::APSInt &Int,
+ llvm::APSInt &NewInt,
+ QualType *Ty) const {
+ // FIXME: This should be a cast from a 1-bit integer type to a boolean type,
+ // but the former is not available in Clang. Instead, extend the APSInt
+ // directly.
+ if (Int.getBitWidth() == 1 && getAPSIntType(Int).isNull()) {
+ ASTContext &Ctx = getBasicVals().getContext();
+ NewInt = Int.extend(Ctx.getTypeSize(Ctx.BoolTy));
+ if (Ty)
+ *Ty = getAPSIntType(NewInt);
+ return NewInt;
+ }
+
+ if (Ty)
+ *Ty = getAPSIntType(Int);
+ return Int;
+}
+
void Z3ConstraintManager::doTypeConversion(Z3Expr &LHS, Z3Expr &RHS,
QualType <y, QualType &RTy) const {
ASTContext &Ctx = getBasicVals().getContext();
+ assert(!LTy.isNull() && !RTy.isNull() && "Input type is null!");
// Perform type conversion
if (LTy->isIntegralOrEnumerationType() &&
RTy->isIntegralOrEnumerationType()) {
@@ -1468,10 +1493,10 @@
void Z3ConstraintManager::doIntTypeConversion(T &LHS, QualType <y, T &RHS,
QualType &RTy) const {
ASTContext &Ctx = getBasicVals().getContext();
-
uint64_t LBitWidth = Ctx.getTypeSize(LTy);
uint64_t RBitWidth = Ctx.getTypeSize(RTy);
+ assert(!LTy.isNull() && !RTy.isNull() && "Input type is null!");
// Always perform integer promotion before checking type equality.
// Otherwise, e.g. (bool) a + (bool) b could trigger a backend assertion
if (LTy->isPromotableIntegerType()) {
@@ -1612,7 +1637,9 @@
#if CLANG_ANALYZER_WITH_Z3
return llvm::make_unique(Eng, StMgr.getSValBuilder());
#else
- llvm::report_fatal_error("Clang was not compiled with Z3 support!", false);
+ llvm::report_fatal_error("Clang was not compiled with Z3 support, rebuild "
+ "with -DCLANG_ANALYZER_BUILD_Z3=ON",
+ false);
return nullptr;
#endif
}
Index: lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
===================================================================
--- lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
+++ lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
@@ -12,9 +12,12 @@
//===----------------------------------------------------------------------===//
#include "clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h"
+#include "clang/StaticAnalyzer/Core/AnalyzerOptions.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/AnalysisManager.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/SValVisitor.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/SubEngine.h"
using namespace clang;
using namespace ento;
@@ -677,14 +680,18 @@
// If one of the operands is a symbol and the other is a constant,
// build an expression for use by the constraint manager.
if (SymbolRef rSym = rhs.getAsLocSymbol()) {
- // We can only build expressions with symbols on the left,
- // so we need a reversible operator.
- if (!BinaryOperator::isComparisonOp(op))
- return UnknownVal();
-
const llvm::APSInt &lVal = lhs.castAs().getValue();
- op = BinaryOperator::reverseComparisonOp(op);
- return makeNonLoc(rSym, op, lVal, resultTy);
+
+ if (BinaryOperator::isCommutativeOp(op))
+ return makeNonLoc(rSym, op, lVal, resultTy);
+
+ if (BinaryOperator::isComparisonOp(op)) {
+ BinaryOperator::Opcode NewOp = BinaryOperator::reverseComparisonOp(op);
+ return makeNonLoc(rSym, NewOp, lVal, resultTy);
+ }
+
+ // Prefer expressions with symbols on the left
+ return makeNonLoc(lVal, op, rSym, resultTy);
}
// If both operands are constants, just perform the operation.
@@ -1002,7 +1009,8 @@
if (SymbolRef Sym = V.getAsSymbol())
return state->getConstraintManager().getSymVal(state, Sym);
- // FIXME: Add support for SymExprs.
+ // FIXME: Add support for SymExprs in RangeConstraintManager.
+
return nullptr;
}
@@ -1014,22 +1022,30 @@
class Simplifier : public FullSValVisitor {
ProgramStateRef State;
SValBuilder &SVB;
+ AnalyzerOptions &Opts;
public:
Simplifier(ProgramStateRef State)
- : State(State), SVB(State->getStateManager().getSValBuilder()) {}
+ : State(State), SVB(State->getStateManager().getSValBuilder()),
+ Opts(State->getStateManager()
+ .getOwningEngine()
+ ->getAnalysisManager()
+ .options) {}
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);
- return Loc::isLocType(S->getType()) ? (SVal)SVB.makeLoc(S)
+ return Loc::isLocType(S->getType()) ? (SVal)SVB.makeLoc(S)
: nonloc::SymbolVal(S);
}
- // TODO: Support SymbolCast. Support IntSymExpr when/if we actually
- // start producing them.
+ SVal VisitIntSymExpr(const IntSymExpr *S) {
+ SVal RHS = Visit(S->getRHS());
+ SVal LHS = SVB.makeIntVal(S->getLHS());
+ return SVB.evalBinOp(State, S->getOpcode(), LHS, RHS, S->getType());
+ }
SVal VisitSymIntExpr(const SymIntExpr *S) {
SVal LHS = Visit(S->getLHS());
@@ -1054,6 +1070,11 @@
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());
+ }
+
SVal VisitSymSymExpr(const SymSymExpr *S) {
SVal LHS = Visit(S->getLHS());
SVal RHS = Visit(S->getRHS());
@@ -1067,7 +1088,11 @@
SVal VisitNonLocSymbolVal(nonloc::SymbolVal V) {
// Simplification is much more costly than computing complexity.
// For high complexity, it may be not worth it.
- if (V.getSymbol()->computeComplexity() > 100)
+ // Use a lower bound to avoid recursive blowup, e.g. on PR24184.cpp
+
+ // FIXME: Complexity monotonically decreases in child recursive calls,
+ // avoid calling this repeatedly
+ if (V.getSymbol()->computeComplexity() > Opts.getMaxSimplifyComplexity())
return V;
return Visit(V.getSymbol());
}
Index: lib/StaticAnalyzer/Core/SValBuilder.cpp
===================================================================
--- lib/StaticAnalyzer/Core/SValBuilder.cpp
+++ lib/StaticAnalyzer/Core/SValBuilder.cpp
@@ -15,10 +15,13 @@
#include "clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h"
#include "clang/AST/DeclCXX.h"
#include "clang/AST/ExprCXX.h"
+#include "clang/StaticAnalyzer/Core/AnalyzerOptions.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/AnalysisManager.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/BasicValueFactory.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/MemRegion.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/SVals.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/SubEngine.h"
using namespace clang;
using namespace ento;
@@ -100,7 +103,7 @@
if (T->isNullPtrType())
return makeZeroVal(T);
-
+
if (!SymbolManager::canSymbolicate(T))
return UnknownVal();
@@ -354,17 +357,17 @@
BinaryOperator::Opcode Op,
NonLoc LHS, NonLoc RHS,
QualType ResultTy) {
- if (!State->isTainted(RHS) && !State->isTainted(LHS))
- return UnknownVal();
-
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 = 10000; // 100000 28X
+
+ AnalyzerOptions &Opts =
+ StateMgr.getOwningEngine()->getAnalysisManager().options;
+ const unsigned MaxComp = Opts.getMaxTaintComplexity(); // 100000 28X
if (symLHS && symRHS &&
- (symLHS->computeComplexity() + symRHS->computeComplexity()) < MaxComp)
+ (symLHS->computeComplexity() + symRHS->computeComplexity()) < MaxComp)
return makeNonLoc(symLHS, Op, symRHS, ResultTy);
if (symLHS && symLHS->computeComplexity() < MaxComp)
@@ -378,7 +381,6 @@
return UnknownVal();
}
-
SVal SValBuilder::evalBinOp(ProgramStateRef state, BinaryOperator::Opcode op,
SVal lhs, SVal rhs, QualType type) {
Index: lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
===================================================================
--- lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
+++ lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
@@ -130,8 +130,9 @@
// "exp comparison_op expr" to false.)
if (Int == 0 && (Op == BO_EQ || Op == BO_NE)) {
if (const BinarySymExpr *SE = dyn_cast(Sym))
- if (BinaryOperator::isComparisonOp(SE->getOpcode()))
+ if (BinaryOperator::isComparisonOp(SE->getOpcode())) {
return assumeSym(State, Sym, (Op == BO_NE ? true : false));
+ }
}
// Get the type used for calculating wraparound.
Index: lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
===================================================================
--- lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -370,42 +370,57 @@
bool RangeConstraintManager::canReasonAbout(SVal X) const {
Optional SymVal = X.getAs();
- if (SymVal && SymVal->isExpression()) {
- const SymExpr *SE = SymVal->getSymbol();
-
- if (const SymIntExpr *SIE = dyn_cast(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:
+ if (!SymVal)
+ return true;
+
+ const SymExpr *SE = SymVal->getSymbol();
+ do {
+ if (isa(SE)) {
+ return true;
+ }
+
+ if (const BinarySymExpr *BSE = dyn_cast(SE)) {
+ BinaryOperator::Opcode Op = BSE->getOpcode();
+
+ if (isa(BSE)) {
return false;
- // All other cases.
- default:
+ }
+
+ if (const SymIntExpr *SIE = dyn_cast(BSE)) {
+ if (BinaryOperator::isMultiplicativeOp(Op) ||
+ BinaryOperator::isShiftOp(Op) || BinaryOperator::isBitwiseOp(Op)) {
+ // We don't reason yet about bitwise-constraints on symbolic values.
+ // We don't reason yet about arithmetic constraints on symbolic values
+ return false;
+ }
+
+ // The simplification case of RangedConstraintManager::assumeSymRel()
+ if (isa(SIE->getLHS()) &&
+ BinaryOperator::isEqualityOp(Op) && SIE->getRHS() == 0 &&
+ BinaryOperator::isComparisonOp(
+ cast(SIE->getLHS())->getOpcode())) {
+ SE = SIE->getLHS();
+ continue;
+ }
+
return true;
}
- }
- if (const SymSymExpr *SSE = dyn_cast(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;
+ if (const SymSymExpr *SSE = dyn_cast(BSE)) {
+ if (!BinaryOperator::isComparisonOp(Op) ||
+ !Loc::isLocType(SSE->getLHS()->getType()) ||
+ !Loc::isLocType(SSE->getRHS()->getType())) {
+ // We handle Loc <> Loc comparisons, but not (yet) NonLoc <> NonLoc.
+ return false;
}
+
+ return canReasonAbout(nonloc::SymbolVal(SSE->getLHS())) &&
+ canReasonAbout(nonloc::SymbolVal(SSE->getRHS()));
}
}
return false;
- }
+ } while (SE);
return true;
}
Index: lib/StaticAnalyzer/Core/AnalyzerOptions.cpp
===================================================================
--- lib/StaticAnalyzer/Core/AnalyzerOptions.cpp
+++ lib/StaticAnalyzer/Core/AnalyzerOptions.cpp
@@ -324,6 +324,18 @@
return GraphTrimInterval.getValue();
}
+unsigned AnalyzerOptions::getMaxSimplifyComplexity() {
+ if (!MaxSimplifyComplexity.hasValue())
+ MaxSimplifyComplexity = getOptionAsInteger("max-simplify-complexity", 10);
+ return MaxSimplifyComplexity.getValue();
+}
+
+unsigned AnalyzerOptions::getMaxTaintComplexity() {
+ if (!MaxTaintComplexity.hasValue())
+ MaxTaintComplexity = getOptionAsInteger("max-taint-complexity", 10000);
+ return MaxTaintComplexity.getValue();
+}
+
unsigned AnalyzerOptions::getMaxTimesInlineLarge() {
if (!MaxTimesInlineLarge.hasValue())
MaxTimesInlineLarge = getOptionAsInteger("max-times-inline-large", 32);
Index: include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
===================================================================
--- include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
+++ include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
@@ -85,7 +85,7 @@
// does not. Is there a good equivalent there?
assert(assume(State, Cond, false) && "System is over constrained.");
#endif
- return ProgramStatePair((ProgramStateRef)nullptr, State);
+ return ProgramStatePair((ProgramStateRef) nullptr, State);
}
ProgramStateRef StFalse = assume(State, Cond, false);
Index: include/clang/StaticAnalyzer/Core/AnalyzerOptions.h
===================================================================
--- include/clang/StaticAnalyzer/Core/AnalyzerOptions.h
+++ include/clang/StaticAnalyzer/Core/AnalyzerOptions.h
@@ -263,6 +263,12 @@
/// \sa getGraphTrimInterval
Optional GraphTrimInterval;
+ /// \sa getMaxSimplifyComplexity
+ Optional MaxSimplifyComplexity;
+
+ /// \sa getMaxTaintComplexity
+ Optional MaxTaintComplexity;
+
/// \sa getMaxTimesInlineLarge
Optional MaxTimesInlineLarge;
@@ -546,6 +552,18 @@
/// node reclamation, set the option to "0".
unsigned getGraphTrimInterval();
+ /// Returns the maximum complexity of symbolic constraint to generate
+ /// when taint analysis checkers are enabled (10000 by default).
+ ///
+ /// This is controlled by "-analyzer-config max-simplify-complexity" option.
+ unsigned getMaxSimplifyComplexity();
+
+ /// Returns the maximum complexity of symbolic constraints to simplify
+ /// through recursive evaluation (10 by default).
+ ///
+ /// This is controlled by "-analyzer-config max-taint-complexity" option.
+ unsigned getMaxTaintComplexity();
+
/// Returns the maximum times a large function could be inlined.
///
/// This is controlled by the 'max-times-inline-large' config option.
Index: include/clang/StaticAnalyzer/Checkers/SValExplainer.h
===================================================================
--- include/clang/StaticAnalyzer/Checkers/SValExplainer.h
+++ include/clang/StaticAnalyzer/Checkers/SValExplainer.h
@@ -125,17 +125,25 @@
return OS.str();
}
- // TODO: IntSymExpr doesn't appear in practice.
- // Add the relevant code once it does.
+ std::string VisitIntSymExpr(const IntSymExpr *S) {
+ std::string Str;
+ llvm::raw_string_ostream OS(Str);
+ OS << S->getLHS()
+ << std::string(BinaryOperator::getOpcodeStr(S->getOpcode())) << " "
+ << "(" << Visit(S->getRHS()) << ") ";
+ return OS.str();
+ }
std::string VisitSymSymExpr(const SymSymExpr *S) {
return "(" + Visit(S->getLHS()) + ") " +
std::string(BinaryOperator::getOpcodeStr(S->getOpcode())) +
" (" + Visit(S->getRHS()) + ")";
}
- // TODO: SymbolCast doesn't appear in practice.
- // Add the relevant code once it does.
+ std::string VisitSymbolCast(const SymbolCast *S) {
+ return "cast of type '" + S->getType().getAsString() + "' of " +
+ Visit(S->getOperand());
+ }
std::string VisitSymbolicRegion(const SymbolicRegion *R) {
// Explain 'this' object here.
Index: include/clang/Config/config.h.cmake
===================================================================
--- include/clang/Config/config.h.cmake
+++ include/clang/Config/config.h.cmake
@@ -38,7 +38,7 @@
/* Define if we have libxml2 */
#cmakedefine CLANG_HAVE_LIBXML ${CLANG_HAVE_LIBXML}
-/* Define if we have z3 and want to build it */
+/* Define if we have z3 and want to build with it */
#cmakedefine CLANG_ANALYZER_WITH_Z3 ${CLANG_ANALYZER_WITH_Z3}
/* Define if we have sys/resource.h (rlimits) */
Index: include/clang/AST/Expr.h
===================================================================
--- include/clang/AST/Expr.h
+++ include/clang/AST/Expr.h
@@ -875,7 +875,7 @@
: Expr(OpaqueValueExprClass, T, VK, OK,
T->isDependentType() ||
(SourceExpr && SourceExpr->isTypeDependent()),
- T->isDependentType() ||
+ T->isDependentType() ||
(SourceExpr && SourceExpr->isValueDependent()),
T->isInstantiationDependentType() ||
(SourceExpr && SourceExpr->isInstantiationDependent()),
@@ -3103,6 +3103,13 @@
}
bool isAssignmentOp() const { return isAssignmentOp(getOpcode()); }
+ static bool isCommutativeOp(Opcode Opc) {
+ return Opc == BO_Mul || Opc == BO_Add || (Opc >= BO_EQ && Opc <= BO_Or);
+ }
+ bool isCommutativeOp() const {
+ return isCommutativeOp(getOpcode());
+ }
+
static bool isCompoundAssignmentOp(Opcode Opc) {
return Opc > BO_Assign && Opc <= BO_OrAssign;
}
@@ -5229,7 +5236,7 @@
SourceLocation getLocStart() const LLVM_READONLY { return SourceLocation(); }
SourceLocation getLocEnd() const LLVM_READONLY { return SourceLocation(); }
-
+
static bool classof(const Stmt *T) {
return T->getStmtClass() == TypoExprClass;
}