ddcc updated this revision to Diff 106883.
ddcc added a comment.
Fix typo
https://reviews.llvm.org/D35450
Files:
include/clang/AST/Expr.h
include/clang/Config/config.h.cmake
include/clang/StaticAnalyzer/Checkers/SValExplainer.h
include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
lib/StaticAnalyzer/Core/SValBuilder.cpp
lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
test/Analysis/analyzer_test.py
test/Analysis/bitwise-ops.c
test/Analysis/bool-assignment.c
test/Analysis/conditional-path-notes.c
test/Analysis/explain-svals.cpp
test/Analysis/plist-macros-z3.cpp
test/Analysis/plist-macros.cpp
test/Analysis/range_casts.c
test/Analysis/std-c-library-functions.c
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,8 +67,8 @@
{
unsigned index = -1;
if (index < foo) index = foo;
- if (index - 1 == 0) // Was not reached prior fix.
- clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+ if (index - 1 == 0)
+ clang_analyzer_warnIfReached(); // no-warning
else
clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
}
@@ -87,8 +87,8 @@
{
unsigned index = -1;
if (index < foo) index = foo;
- if (index - 1L == 0L) // Was not reached prior fix.
- clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+ if (index - 1L == 0L)
+ clang_analyzer_warnIfReached(); // no-warning
else
clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
}
@@ -117,8 +117,8 @@
{
unsigned index = -1;
if (index < foo) index = foo;
- if (index - 1UL == 0L) // Was not reached prior fix.
- clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+ if (index - 1UL == 0L)
+ clang_analyzer_warnIfReached(); // no-warning
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: <key>diagnostics</key>
// CHECK-NEXT: <array>
// CHECK-NEXT: <dict>
@@ -636,6 +637,69 @@
// CHECK-NEXT: <key>end</key>
// CHECK-NEXT: <array>
// CHECK-NEXT: <dict>
+// CHECK-NEXT: <key>line</key><integer>36</integer>
+// CHECK-NEXT: <key>col</key><integer>7</integer>
+// CHECK-NEXT: <key>file</key><integer>0</integer>
+// CHECK-NEXT: </dict>
+// CHECK-NEXT: <dict>
+// CHECK-NEXT: <key>line</key><integer>36</integer>
+// CHECK-NEXT: <key>col</key><integer>7</integer>
+// CHECK-NEXT: <key>file</key><integer>0</integer>
+// CHECK-NEXT: </dict>
+// CHECK-NEXT: </array>
+// CHECK-NEXT: </dict>
+// CHECK-NEXT: </array>
+// CHECK-NEXT: </dict>
+// CHECK-NEXT: <dict>
+// CHECK-NEXT: <key>kind</key><string>event</string>
+// CHECK-NEXT: <key>location</key>
+// CHECK-NEXT: <dict>
+// CHECK-NEXT: <key>line</key><integer>36</integer>
+// CHECK-NEXT: <key>col</key><integer>7</integer>
+// CHECK-NEXT: <key>file</key><integer>0</integer>
+// CHECK-NEXT: </dict>
+// CHECK-NEXT: <key>ranges</key>
+// CHECK-NEXT: <array>
+// CHECK-NEXT: <array>
+// CHECK-NEXT: <dict>
+// CHECK-NEXT: <key>line</key><integer>36</integer>
+// CHECK-NEXT: <key>col</key><integer>7</integer>
+// CHECK-NEXT: <key>file</key><integer>0</integer>
+// CHECK-NEXT: </dict>
+// CHECK-NEXT: <dict>
+// CHECK-NEXT: <key>line</key><integer>36</integer>
+// CHECK-NEXT: <key>col</key><integer>25</integer>
+// CHECK-NEXT: <key>file</key><integer>0</integer>
+// CHECK-NEXT: </dict>
+// CHECK-NEXT: </array>
+// CHECK-NEXT: </array>
+// CHECK-NEXT: <key>depth</key><integer>0</integer>
+// CHECK-NEXT: <key>extended_message</key>
+// CHECK-NEXT: <string>Assuming the condition is true</string>
+// CHECK-NEXT: <key>message</key>
+// CHECK-NEXT: <string>Assuming the condition is true</string>
+// CHECK-NEXT: </dict>
+// CHECK-NEXT: <dict>
+// CHECK-NEXT: <key>kind</key><string>control</string>
+// CHECK-NEXT: <key>edges</key>
+// CHECK-NEXT: <array>
+// CHECK-NEXT: <dict>
+// CHECK-NEXT: <key>start</key>
+// CHECK-NEXT: <array>
+// CHECK-NEXT: <dict>
+// CHECK-NEXT: <key>line</key><integer>36</integer>
+// CHECK-NEXT: <key>col</key><integer>7</integer>
+// CHECK-NEXT: <key>file</key><integer>0</integer>
+// CHECK-NEXT: </dict>
+// CHECK-NEXT: <dict>
+// CHECK-NEXT: <key>line</key><integer>36</integer>
+// CHECK-NEXT: <key>col</key><integer>7</integer>
+// CHECK-NEXT: <key>file</key><integer>0</integer>
+// CHECK-NEXT: </dict>
+// CHECK-NEXT: </array>
+// CHECK-NEXT: <key>end</key>
+// CHECK-NEXT: <array>
+// CHECK-NEXT: <dict>
// CHECK-NEXT: <key>line</key><integer>37</integer>
// CHECK-NEXT: <key>col</key><integer>5</integer>
// CHECK-NEXT: <key>file</key><integer>0</integer>
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: <key>diagnostics</key>
// CHECK-NEXT: <array>
// CHECK-NEXT: <dict>
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: <key>end</key>
// CHECK-NEXT: <array>
// CHECK-NEXT: <dict>
-// CHECK-NEXT: <key>line</key><integer>81</integer>
+// CHECK-NEXT: <key>line</key><integer>79</integer>
+// CHECK-NEXT: <key>col</key><integer>7</integer>
+// CHECK-NEXT: <key>file</key><integer>0</integer>
+// CHECK-NEXT: </dict>
+// CHECK-NEXT: <dict>
+// CHECK-NEXT: <key>line</key><integer>79</integer>
+// CHECK-NEXT: <key>col</key><integer>7</integer>
+// CHECK-NEXT: <key>file</key><integer>0</integer>
+// CHECK-NEXT: </dict>
+// CHECK-NEXT: </array>
+// CHECK-NEXT: </dict>
+// CHECK-NEXT: </array>
+// CHECK-NEXT: </dict>
+// CHECK-NEXT: <dict>
+// CHECK-NEXT: <key>kind</key><string>event</string>
+// CHECK-NEXT: <key>location</key>
+// CHECK-NEXT: <dict>
+// CHECK-NEXT: <key>line</key><integer>79</integer>
+// CHECK-NEXT: <key>col</key><integer>7</integer>
+// CHECK-NEXT: <key>file</key><integer>0</integer>
+// CHECK-NEXT: </dict>
+// CHECK-NEXT: <key>ranges</key>
+// CHECK-NEXT: <array>
+// CHECK-NEXT: <array>
+// CHECK-NEXT: <dict>
+// CHECK-NEXT: <key>line</key><integer>79</integer>
+// CHECK-NEXT: <key>col</key><integer>7</integer>
+// CHECK-NEXT: <key>file</key><integer>0</integer>
+// CHECK-NEXT: </dict>
+// CHECK-NEXT: <dict>
+// CHECK-NEXT: <key>line</key><integer>79</integer>
+// CHECK-NEXT: <key>col</key><integer>11</integer>
+// CHECK-NEXT: <key>file</key><integer>0</integer>
+// CHECK-NEXT: </dict>
+// CHECK-NEXT: </array>
+// CHECK-NEXT: </array>
+// CHECK-NEXT: <key>depth</key><integer>0</integer>
+// CHECK-NEXT: <key>extended_message</key>
+// CHECK-NEXT: <string>Assuming the condition is true</string>
+// CHECK-NEXT: <key>message</key>
+// CHECK-NEXT: <string>Assuming the condition is true</string>
+// CHECK-NEXT: </dict>
+// CHECK-NEXT: <dict>
+// CHECK-NEXT: <key>kind</key><string>control</string>
+// CHECK-NEXT: <key>edges</key>
+// CHECK-NEXT: <array>
+// CHECK-NEXT: <dict>
+// CHECK-NEXT: <key>start</key>
+// CHECK-NEXT: <array>
+// CHECK-NEXT: <dict>
+// CHECK-NEXT: <key>line</key><integer>79</integer>
+// CHECK-NEXT: <key>col</key><integer>7</integer>
+// CHECK-NEXT: <key>file</key><integer>0</integer>
+// CHECK-NEXT: </dict>
+// CHECK-NEXT: <dict>
+// CHECK-NEXT: <key>line</key><integer>79</integer>
+// CHECK-NEXT: <key>col</key><integer>7</integer>
+// CHECK-NEXT: <key>file</key><integer>0</integer>
+// CHECK-NEXT: </dict>
+// CHECK-NEXT: </array>
+// CHECK-NEXT: <key>end</key>
+// CHECK-NEXT: <array>
+// CHECK-NEXT: <dict>
+// CHECK-NEXT: <key>line</key><integer>82</integer>
// CHECK-NEXT: <key>col</key><integer>5</integer>
// CHECK-NEXT: <key>file</key><integer>0</integer>
// CHECK-NEXT: </dict>
// CHECK-NEXT: <dict>
-// CHECK-NEXT: <key>line</key><integer>81</integer>
+// CHECK-NEXT: <key>line</key><integer>82</integer>
// CHECK-NEXT: <key>col</key><integer>5</integer>
// CHECK-NEXT: <key>file</key><integer>0</integer>
// CHECK-NEXT: </dict>
@@ -1594,25 +1658,25 @@
// CHECK-NEXT: <key>start</key>
// CHECK-NEXT: <array>
// CHECK-NEXT: <dict>
-// CHECK-NEXT: <key>line</key><integer>81</integer>
+// CHECK-NEXT: <key>line</key><integer>82</integer>
// CHECK-NEXT: <key>col</key><integer>5</integer>
// CHECK-NEXT: <key>file</key><integer>0</integer>
// CHECK-NEXT: </dict>
// CHECK-NEXT: <dict>
-// CHECK-NEXT: <key>line</key><integer>81</integer>
+// CHECK-NEXT: <key>line</key><integer>82</integer>
// CHECK-NEXT: <key>col</key><integer>5</integer>
// CHECK-NEXT: <key>file</key><integer>0</integer>
// CHECK-NEXT: </dict>
// CHECK-NEXT: </array>
// CHECK-NEXT: <key>end</key>
// CHECK-NEXT: <array>
// CHECK-NEXT: <dict>
-// CHECK-NEXT: <key>line</key><integer>81</integer>
+// CHECK-NEXT: <key>line</key><integer>82</integer>
// CHECK-NEXT: <key>col</key><integer>24</integer>
// CHECK-NEXT: <key>file</key><integer>0</integer>
// CHECK-NEXT: </dict>
// CHECK-NEXT: <dict>
-// CHECK-NEXT: <key>line</key><integer>81</integer>
+// CHECK-NEXT: <key>line</key><integer>82</integer>
// CHECK-NEXT: <key>col</key><integer>24</integer>
// CHECK-NEXT: <key>file</key><integer>0</integer>
// CHECK-NEXT: </dict>
@@ -1624,20 +1688,20 @@
// CHECK-NEXT: <key>kind</key><string>event</string>
// CHECK-NEXT: <key>location</key>
// CHECK-NEXT: <dict>
-// CHECK-NEXT: <key>line</key><integer>81</integer>
+// CHECK-NEXT: <key>line</key><integer>82</integer>
// CHECK-NEXT: <key>col</key><integer>24</integer>
// CHECK-NEXT: <key>file</key><integer>0</integer>
// CHECK-NEXT: </dict>
// CHECK-NEXT: <key>ranges</key>
// CHECK-NEXT: <array>
// CHECK-NEXT: <array>
// CHECK-NEXT: <dict>
-// CHECK-NEXT: <key>line</key><integer>81</integer>
+// CHECK-NEXT: <key>line</key><integer>82</integer>
// CHECK-NEXT: <key>col</key><integer>5</integer>
// CHECK-NEXT: <key>file</key><integer>0</integer>
// CHECK-NEXT: </dict>
// CHECK-NEXT: <dict>
-// CHECK-NEXT: <key>line</key><integer>81</integer>
+// CHECK-NEXT: <key>line</key><integer>82</integer>
// CHECK-NEXT: <key>col</key><integer>26</integer>
// CHECK-NEXT: <key>file</key><integer>0</integer>
// CHECK-NEXT: </dict>
@@ -1658,10 +1722,10 @@
// CHECK-NEXT: <key>issue_hash_content_of_line_in_context</key><string>f56671e5f67c73abef619b56f7c29fa4</string>
// CHECK-NEXT: <key>issue_context_kind</key><string>function</string>
// CHECK-NEXT: <key>issue_context</key><string>testNonDiagnosableBranchArithmetic</string>
-// CHECK-NEXT: <key>issue_hash_function_offset</key><string>3</string>
+// CHECK-NEXT: <key>issue_hash_function_offset</key><string>4</string>
// CHECK-NEXT: <key>location</key>
// CHECK-NEXT: <dict>
-// CHECK-NEXT: <key>line</key><integer>81</integer>
+// CHECK-NEXT: <key>line</key><integer>82</integer>
// CHECK-NEXT: <key>col</key><integer>24</integer>
// CHECK-NEXT: <key>file</key><integer>0</integer>
// CHECK-NEXT: </dict>
Index: test/Analysis/bool-assignment.c
===================================================================
--- test/Analysis/bool-assignment.c
+++ test/Analysis/bool-assignment.c
@@ -43,11 +43,7 @@
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) {
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<SymbolData>(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<SymbolCast>(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<BinarySymExpr>(Sym)) {
const llvm::APSInt *LHS, *RHS;
if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
@@ -1215,7 +1220,7 @@
QualType LTy = getAPSIntType(*LHS), RTy = getAPSIntType(*RHS);
doIntTypeConversion<llvm::APSInt, Z3ConstraintManager::castAPSInt>(
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<SymIntExpr>(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<IntSymExpr>(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<SymSymExpr>(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<Z3ConstraintManager>(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
@@ -669,14 +669,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<loc::ConcreteInt>().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.
@@ -994,7 +998,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;
}
@@ -1019,8 +1024,11 @@
return 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());
@@ -1045,6 +1053,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());
@@ -1058,7 +1071,8 @@
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
+ if (V.getSymbol()->computeComplexity() > 10)
return V;
return Visit(V.getSymbol());
}
Index: lib/StaticAnalyzer/Core/SValBuilder.cpp
===================================================================
--- lib/StaticAnalyzer/Core/SValBuilder.cpp
+++ lib/StaticAnalyzer/Core/SValBuilder.cpp
@@ -100,7 +100,7 @@
if (T->isNullPtrType())
return makeZeroVal(T);
-
+
if (!SymbolManager::canSymbolicate(T))
return UnknownVal();
@@ -354,17 +354,14 @@
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
if (symLHS && symRHS &&
- (symLHS->computeComplexity() + symRHS->computeComplexity()) < MaxComp)
+ (symLHS->computeComplexity() + symRHS->computeComplexity()) < MaxComp)
return makeNonLoc(symLHS, Op, symRHS, ResultTy);
if (symLHS && symLHS->computeComplexity() < MaxComp)
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<BinarySymExpr>(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,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:
+ if (!SymVal)
+ return true;
+
+ const SymExpr *SE = SymVal->getSymbol();
+ do {
+ if (isa<SymbolData>(SE)) {
+ return true;
+ } else if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(SE)) {
+ BinaryOperator::Opcode Op = BSE->getOpcode();
+
+ if (isa<IntSymExpr>(BSE)) {
return false;
- // All other cases.
- default:
- return true;
- }
- }
+ } else if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(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<BinarySymExpr>(SIE->getLHS()) &&
+ BinaryOperator::isEqualityOp(Op) && SIE->getRHS() == 0 &&
+ BinaryOperator::isComparisonOp(
+ cast<BinarySymExpr>(SIE->getLHS())->getOpcode())) {
+ SE = SIE->getLHS();
+ continue;
+ }
- 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 true;
+ } else if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(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: include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
===================================================================
--- include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
+++ include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
@@ -83,9 +83,10 @@
// builds.
// FIXME: __OPTIMIZE__ is a GNU extension that Clang implements but MSVC
// does not. Is there a good equivalent there?
- assert(assume(State, Cond, false) && "System is over constrained.");
+ if (canReasonAbout(Cond))
+ 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/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
@@ -874,7 +874,7 @@
: Expr(OpaqueValueExprClass, T, VK, OK,
T->isDependentType() ||
(SourceExpr && SourceExpr->isTypeDependent()),
- T->isDependentType() ||
+ T->isDependentType() ||
(SourceExpr && SourceExpr->isValueDependent()),
T->isInstantiationDependentType() ||
(SourceExpr && SourceExpr->isInstantiationDependent()),
@@ -3092,6 +3092,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;
}
@@ -5184,7 +5191,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;
}
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
