martong updated this revision to Diff 354274.
martong added a comment.
- Use simplify from RangedConstraintManager
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D104844/new/
https://reviews.llvm.org/D104844
Files:
clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
clang/lib/StaticAnalyzer/Core/RangedConstraintManager.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/RangedConstraintManager.cpp
===================================================================
--- clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
+++ clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
@@ -23,12 +23,14 @@
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::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::assumeSymUnsupported(ProgramStateRef State,
SymbolRef Sym, bool Assumption) {
+ Sym = simplify(State, Sym);
+
BasicValueFactory &BVF = getBasicVals();
QualType T = Sym->getType();
@@ -219,5 +226,13 @@
}
}
+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
Index: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
===================================================================
--- clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -1389,12 +1389,6 @@
// 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)
@@ -1519,9 +1513,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,
@@ -1987,7 +1978,7 @@
SValBuilder &SVB, RangeSet::Factory &F, ProgramStateRef State) {
SymbolSet ClassMembers = getClassMembers(State);
for (const SymbolRef &MemberSym : ClassMembers) {
- SymbolRef SimplifiedMemberSym = ::simplify(State, MemberSym);
+ SymbolRef SimplifiedMemberSym = ::clang::ento::simplify(State, MemberSym);
if (SimplifiedMemberSym && MemberSym != SimplifiedMemberSym) {
EquivalenceClass ClassOfSimplifiedSym =
EquivalenceClass::find(State, SimplifiedMemberSym);
@@ -2313,7 +2304,6 @@
return St;
llvm::APSInt Point = AdjustmentType.convert(Int) - Adjustment;
-
RangeSet New = getRange(St, Sym);
New = F.deletePoint(New, Point);
Index: clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
===================================================================
--- clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
+++ clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
@@ -384,6 +384,11 @@
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
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
