martong created this revision.
martong added reviewers: vsavchenko, steakhal.
Herald added subscribers: manas, ASDenysPetrov, gamesh411, dkrupp, donat.nagy,
Szelethus, mikhail.ramalho, a.sidorin, rnkovacs, szepet, baloghadamsoftware,
xazax.hun, whisperity.
Herald added a reviewer: Szelethus.
martong requested review of this revision.
Herald added a project: clang.
Herald added a subscriber: cfe-commits.
Consider the code
void f(int a0, int b0, int c)
{
int a1 = a0 - b0;
int b1 = (unsigned)a1 + c;
if (c == 0) {
int d = 7L / b1;
}
}
At the point of divisiion by `b1` that is considered to be non-zero,
which results in a new constraint for `$a0 - $b0 + $c`. The type
of this sym is unsigned, however, the simplified sym is `$a0 -
$b0` and its type is signed. This is probably the result of the
inherent improper handling of casts. Anyway, Range assignment
for constraints use this type information. Therefore, we must
make sure that first we simplify the symbol and only then we
assign the range.
Repository:
rG LLVM Github Monorepo
https://reviews.llvm.org/D104844
Files:
clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
clang/test/Analysis/solver-sym-simplification-no-crash.c
clang/test/Analysis/solver-sym-simplification-with-proper-range-type.c
Index: clang/test/Analysis/solver-sym-simplification-with-proper-range-type.c
===================================================================
--- /dev/null
+++ clang/test/Analysis/solver-sym-simplification-with-proper-range-type.c
@@ -0,0 +1,29 @@
+// RUN: %clang_analyze_cc1 %s \
+// RUN: -analyzer-checker=core \
+// RUN: -analyzer-checker=debug.ExprInspection \
+// RUN: -verify
+
+// Here we test that the range based solver equivalency tracking mechanism
+// assigns a properly typed range to the simplified symbol.
+
+void clang_analyzer_printState();
+void clang_analyzer_eval(int);
+
+void f(int a0, int b0, int c)
+{
+ int a1 = a0 - b0;
+ int b1 = (unsigned)a1 + c;
+ if (c == 0) {
+
+ int d = 7L / b1; // ...
+ // At this point b1 is considered non-zero, which results in a new
+ // constraint for $a0 - $b0 + $c. The type of this sym is unsigned,
+ // however, the simplified sym is $a0 - $b0 and its type is signed.
+ // This is probably the result of the inherent improper handling of
+ // casts. Anyway, Range assignment for constraints use this type
+ // information. Therefore, we must make sure that first we simplify the
+ // symbol and only then we assign the range.
+
+ clang_analyzer_eval(a0 - b0 != 0); // expected-warning{{TRUE}}
+ }
+}
Index: clang/test/Analysis/solver-sym-simplification-no-crash.c
===================================================================
--- /dev/null
+++ clang/test/Analysis/solver-sym-simplification-no-crash.c
@@ -0,0 +1,26 @@
+// RUN: %clang_analyze_cc1 %s \
+// RUN: -analyzer-checker=core \
+// RUN: -analyzer-checker=debug.ExprInspection \
+// RUN: -verify
+
+// Here, we test that symbol simplification in the solver does not produce any
+// crashes.
+
+// expected-no-diagnostics
+
+static int a, b;
+static long c;
+
+static void f(int i, int j)
+{
+ (void)(j <= 0 && i ? i : j);
+}
+
+static void g(void)
+{
+ int d = a - b | (c < 0);
+ for (;;)
+ {
+ f(d ^ c, c);
+ }
+}
Index: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
===================================================================
--- clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -1519,9 +1519,6 @@
// This is an infeasible assumption.
return nullptr;
- if (SymbolRef SimplifiedSym = simplify(State, Sym))
- Sym = SimplifiedSym;
-
if (ProgramStateRef NewState = setConstraint(State, Sym, NewConstraint)) {
if (auto Equality = EqualityInfo::extract(Sym, Int, Adjustment)) {
// If the original assumption is not Sym + Adjustment !=/</> Int,
@@ -2314,6 +2311,9 @@
llvm::APSInt Point = AdjustmentType.convert(Int) - Adjustment;
+ if (SymbolRef SimplifiedSym = simplify(St, Sym))
+ Sym = SimplifiedSym;
+
RangeSet New = getRange(St, Sym);
New = F.deletePoint(New, Point);
@@ -2331,6 +2331,10 @@
// [Int-Adjustment, Int-Adjustment]
llvm::APSInt AdjInt = AdjustmentType.convert(Int) - Adjustment;
+
+ if (SymbolRef SimplifiedSym = simplify(St, Sym))
+ Sym = SimplifiedSym;
+
RangeSet New = getRange(St, Sym);
New = F.intersect(New, AdjInt);
@@ -2370,6 +2374,8 @@
RangeConstraintManager::assumeSymLT(ProgramStateRef St, SymbolRef Sym,
const llvm::APSInt &Int,
const llvm::APSInt &Adjustment) {
+ if (SymbolRef SimplifiedSym = simplify(St, Sym))
+ Sym = SimplifiedSym;
RangeSet New = getSymLTRange(St, Sym, Int, Adjustment);
return trackNE(New, St, Sym, Int, Adjustment);
}
@@ -2407,6 +2413,8 @@
RangeConstraintManager::assumeSymGT(ProgramStateRef St, SymbolRef Sym,
const llvm::APSInt &Int,
const llvm::APSInt &Adjustment) {
+ if (SymbolRef SimplifiedSym = simplify(St, Sym))
+ Sym = SimplifiedSym;
RangeSet New = getSymGTRange(St, Sym, Int, Adjustment);
return trackNE(New, St, Sym, Int, Adjustment);
}
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
