[clang] 0646e36 - [Analyzer][solver] Fix crashes during symbol simplification
Gabor Marton via cfe-commits
cfe-commits at lists.llvm.org
Fri Jun 25 02:50:04 PDT 2021
Author: Gabor Marton
Date: 2021-06-25T11:49:26+02:00
New Revision: 0646e3625499b08a3ac9efd48396f3b463a19139
URL: https://github.com/llvm/llvm-project/commit/0646e3625499b08a3ac9efd48396f3b463a19139
DIFF: https://github.com/llvm/llvm-project/commit/0646e3625499b08a3ac9efd48396f3b463a19139.diff
LOG: [Analyzer][solver] Fix crashes during symbol simplification
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.
Differential Revision: https://reviews.llvm.org/D104844
Added:
clang/test/Analysis/solver-sym-simplification-no-crash.c
clang/test/Analysis/solver-sym-simplification-with-proper-range-type.c
Modified:
clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
Removed:
################################################################################
diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
index a4957c697c0ae..bf00fd98a4616 100644
--- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
+++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
@@ -384,6 +384,11 @@ class RangedConstraintManager : public SimpleConstraintManager {
static void computeAdjustment(SymbolRef &Sym, llvm::APSInt &Adjustment);
};
+/// Try to simplify a given symbolic expression's associated value based on the
+/// constraints in State. This is needed because the Environment bindings are
+/// not getting updated when a new constraint is added to the State.
+SymbolRef simplify(ProgramStateRef State, SymbolRef Sym);
+
} // namespace ento
} // namespace clang
diff --git a/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp b/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
index ac7767f0d3c4d..6d17bcb8b87f0 100644
--- a/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ b/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -1384,12 +1384,6 @@ RangeSet SymbolicRangeInferrer::VisitBinaryOperator<BO_Rem>(Range LHS,
// Constraint manager implementation details
//===----------------------------------------------------------------------===//
-static SymbolRef simplify(ProgramStateRef State, SymbolRef Sym) {
- SValBuilder &SVB = State->getStateManager().getSValBuilder();
- SVal SimplifiedVal = SVB.simplifySVal(State, SVB.makeSymbolVal(Sym));
- return SimplifiedVal.getAsSymbol();
-}
-
class RangeConstraintManager : public RangedConstraintManager {
public:
RangeConstraintManager(ExprEngine *EE, SValBuilder &SVB)
@@ -1503,9 +1497,6 @@ class RangeConstraintManager : public RangedConstraintManager {
// 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,
@@ -1962,7 +1953,7 @@ LLVM_NODISCARD ProgramStateRef EquivalenceClass::simplify(
SValBuilder &SVB, RangeSet::Factory &F, ProgramStateRef State) {
SymbolSet ClassMembers = getClassMembers(State);
for (const SymbolRef &MemberSym : ClassMembers) {
- SymbolRef SimplifiedMemberSym = ::simplify(State, MemberSym);
+ SymbolRef SimplifiedMemberSym = ento::simplify(State, MemberSym);
if (SimplifiedMemberSym && MemberSym != SimplifiedMemberSym) {
EquivalenceClass ClassOfSimplifiedSym =
EquivalenceClass::find(State, SimplifiedMemberSym);
@@ -2288,7 +2279,6 @@ RangeConstraintManager::assumeSymNE(ProgramStateRef St, SymbolRef Sym,
return St;
llvm::APSInt Point = AdjustmentType.convert(Int) - Adjustment;
-
RangeSet New = getRange(St, Sym);
New = F.deletePoint(New, Point);
diff --git a/clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp b/clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
index 1b8945fb66af0..d227c025fb203 100644
--- a/clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
+++ b/clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
@@ -23,12 +23,14 @@ RangedConstraintManager::~RangedConstraintManager() {}
ProgramStateRef RangedConstraintManager::assumeSym(ProgramStateRef State,
SymbolRef Sym,
bool Assumption) {
+ Sym = simplify(State, Sym);
+
// Handle SymbolData.
- if (isa<SymbolData>(Sym)) {
+ if (isa<SymbolData>(Sym))
return assumeSymUnsupported(State, Sym, Assumption);
- // Handle symbolic expression.
- } else if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(Sym)) {
+ // Handle symbolic expression.
+ if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(Sym)) {
// We can only simplify expressions whose RHS is an integer.
BinaryOperator::Opcode op = SIE->getOpcode();
@@ -93,6 +95,9 @@ ProgramStateRef RangedConstraintManager::assumeSym(ProgramStateRef State,
ProgramStateRef RangedConstraintManager::assumeSymInclusiveRange(
ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
const llvm::APSInt &To, bool InRange) {
+
+ Sym = simplify(State, Sym);
+
// Get the type used for calculating wraparound.
BasicValueFactory &BVF = getBasicVals();
APSIntType WraparoundType = BVF.getAPSIntType(Sym->getType());
@@ -121,6 +126,8 @@ ProgramStateRef RangedConstraintManager::assumeSymInclusiveRange(
ProgramStateRef
RangedConstraintManager::assumeSymUnsupported(ProgramStateRef State,
SymbolRef Sym, bool Assumption) {
+ Sym = simplify(State, Sym);
+
BasicValueFactory &BVF = getBasicVals();
QualType T = Sym->getType();
@@ -219,5 +226,13 @@ void RangedConstraintManager::computeAdjustment(SymbolRef &Sym,
}
}
+SymbolRef simplify(ProgramStateRef State, SymbolRef Sym) {
+ SValBuilder &SVB = State->getStateManager().getSValBuilder();
+ SVal SimplifiedVal = SVB.simplifySVal(State, SVB.makeSymbolVal(Sym));
+ if (SymbolRef SimplifiedSym = SimplifiedVal.getAsSymbol())
+ return SimplifiedSym;
+ return Sym;
+}
+
} // end of namespace ento
} // end of namespace clang
diff --git a/clang/test/Analysis/solver-sym-simplification-no-crash.c b/clang/test/Analysis/solver-sym-simplification-no-crash.c
new file mode 100644
index 0000000000000..f90fad07f0c30
--- /dev/null
+++ b/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);
+ }
+}
diff --git a/clang/test/Analysis/solver-sym-simplification-with-proper-range-type.c b/clang/test/Analysis/solver-sym-simplification-with-proper-range-type.c
new file mode 100644
index 0000000000000..248742e96b6b4
--- /dev/null
+++ b/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}}
+ }
+}
More information about the cfe-commits
mailing list