ASDenysPetrov updated this revision to Diff 261556.
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D78933/new/
https://reviews.llvm.org/D78933
Files:
clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
clang/test/Analysis/constraint_manager_conditions.cpp
Index: clang/test/Analysis/constraint_manager_conditions.cpp
===================================================================
--- /dev/null
+++ clang/test/Analysis/constraint_manager_conditions.cpp
@@ -0,0 +1,183 @@
+// RUN: %clang_analyze_cc1 -analyzer-checker=debug.ExprInspection -verify %s
+
+void clang_analyzer_eval(int);
+
+void comparison_lt(int x, int y) {
+ if (x < y) {
+ clang_analyzer_eval(x < y); // expected-warning{{TRUE}}
+ clang_analyzer_eval(y > x); // expected-warning{{TRUE}}
+ clang_analyzer_eval(x > y); // expected-warning{{FALSE}}
+ clang_analyzer_eval(y < x); // expected-warning{{FALSE}}
+ clang_analyzer_eval(x <= y); // expected-warning{{TRUE}}
+ clang_analyzer_eval(y >= x); // expected-warning{{TRUE}}
+ clang_analyzer_eval(x >= y); // expected-warning{{FALSE}}
+ clang_analyzer_eval(y <= x); // expected-warning{{FALSE}}
+ clang_analyzer_eval(x == y); // expected-warning{{FALSE}}
+ clang_analyzer_eval(y == x); // expected-warning{{FALSE}}
+ clang_analyzer_eval(x != y); // expected-warning{{TRUE}}
+ clang_analyzer_eval(y != x); // expected-warning{{TRUE}}
+ } else {
+ clang_analyzer_eval(x < y); // expected-warning{{FALSE}}
+ clang_analyzer_eval(y > x); // expected-warning{{FALSE}}
+ clang_analyzer_eval(x > y); // expected-warning{{TRUE}} expected-warning{{FALSE}}
+ clang_analyzer_eval(y < x); // expected-warning{{TRUE}} expected-warning{{FALSE}}
+ clang_analyzer_eval(x <= y); // expected-warning{{TRUE}} expected-warning{{FALSE}}
+ clang_analyzer_eval(y >= x); // expected-warning{{TRUE}} expected-warning{{FALSE}}
+ clang_analyzer_eval(x >= y); // expected-warning{{TRUE}}
+ clang_analyzer_eval(y <= x); // expected-warning{{TRUE}}
+ clang_analyzer_eval(x == y); // expected-warning{{TRUE}} expected-warning{{FALSE}}
+ clang_analyzer_eval(y == x); // expected-warning{{TRUE}} expected-warning{{FALSE}}
+ clang_analyzer_eval(x != y); // expected-warning{{TRUE}} expected-warning{{FALSE}}
+ clang_analyzer_eval(y != x); // expected-warning{{TRUE}} expected-warning{{FALSE}}
+ }
+}
+
+void comparison_gt(int x, int y) {
+ if (x > y) {
+ clang_analyzer_eval(x < y); // expected-warning{{FALSE}}
+ clang_analyzer_eval(y > x); // expected-warning{{FALSE}}
+ clang_analyzer_eval(x > y); // expected-warning{{TRUE}}
+ clang_analyzer_eval(y < x); // expected-warning{{TRUE}}
+ clang_analyzer_eval(x <= y); // expected-warning{{FALSE}}
+ clang_analyzer_eval(y >= x); // expected-warning{{FALSE}}
+ clang_analyzer_eval(x >= y); // expected-warning{{TRUE}}
+ clang_analyzer_eval(y <= x); // expected-warning{{TRUE}}
+ clang_analyzer_eval(x == y); // expected-warning{{FALSE}}
+ clang_analyzer_eval(y == x); // expected-warning{{FALSE}}
+ clang_analyzer_eval(x != y); // expected-warning{{TRUE}}
+ clang_analyzer_eval(y != x); // expected-warning{{TRUE}}
+ } else {
+ clang_analyzer_eval(x < y); // expected-warning{{TRUE}} expected-warning{{FALSE}}
+ clang_analyzer_eval(y > x); // expected-warning{{TRUE}} expected-warning{{FALSE}}
+ clang_analyzer_eval(x > y); // expected-warning{{FALSE}}
+ clang_analyzer_eval(y < x); // expected-warning{{FALSE}}
+ clang_analyzer_eval(x <= y); // expected-warning{{TRUE}}
+ clang_analyzer_eval(y >= x); // expected-warning{{TRUE}}
+ clang_analyzer_eval(x >= y); // expected-warning{{TRUE}} expected-warning{{FALSE}}
+ clang_analyzer_eval(y <= x); // expected-warning{{TRUE}} expected-warning{{FALSE}}
+ clang_analyzer_eval(x == y); // expected-warning{{TRUE}} expected-warning{{FALSE}}
+ clang_analyzer_eval(y == x); // expected-warning{{TRUE}} expected-warning{{FALSE}}
+ clang_analyzer_eval(x != y); // expected-warning{{TRUE}} expected-warning{{FALSE}}
+ clang_analyzer_eval(y != x); // expected-warning{{TRUE}} expected-warning{{FALSE}}
+ }
+}
+
+void comparison_le(int x, int y) {
+ if (x <= y) {
+ clang_analyzer_eval(x < y); // expected-warning{{TRUE}} expected-warning{{FALSE}}
+ clang_analyzer_eval(y > x); // expected-warning{{TRUE}} expected-warning{{FALSE}}
+ clang_analyzer_eval(x > y); // expected-warning{{FALSE}}
+ clang_analyzer_eval(y < x); // expected-warning{{FALSE}}
+ clang_analyzer_eval(x <= y); // expected-warning{{TRUE}}
+ clang_analyzer_eval(y >= x); // expected-warning{{TRUE}}
+ clang_analyzer_eval(x >= y); // expected-warning{{TRUE}} expected-warning{{FALSE}}
+ clang_analyzer_eval(y <= x); // expected-warning{{TRUE}} expected-warning{{FALSE}}
+ clang_analyzer_eval(x == y); // expected-warning{{TRUE}} expected-warning{{FALSE}}
+ clang_analyzer_eval(y == x); // expected-warning{{TRUE}} expected-warning{{FALSE}}
+ clang_analyzer_eval(x != y); // expected-warning{{TRUE}} expected-warning{{FALSE}}
+ clang_analyzer_eval(y != x); // expected-warning{{TRUE}} expected-warning{{FALSE}}
+ } else {
+ clang_analyzer_eval(x < y); // expected-warning{{FALSE}}
+ clang_analyzer_eval(y > x); // expected-warning{{FALSE}}
+ clang_analyzer_eval(x > y); // expected-warning{{TRUE}}
+ clang_analyzer_eval(y < x); // expected-warning{{TRUE}}
+ clang_analyzer_eval(x <= y); // expected-warning{{FALSE}}
+ clang_analyzer_eval(y >= x); // expected-warning{{FALSE}}
+ clang_analyzer_eval(x >= y); // expected-warning{{TRUE}}
+ clang_analyzer_eval(y <= x); // expected-warning{{TRUE}}
+ clang_analyzer_eval(x == y); // expected-warning{{FALSE}}
+ clang_analyzer_eval(y == x); // expected-warning{{FALSE}}
+ clang_analyzer_eval(x != y); // expected-warning{{TRUE}}
+ clang_analyzer_eval(y != x); // expected-warning{{TRUE}}
+ }
+}
+
+void comparison_ge(int x, int y) {
+ if (x >= y) {
+ clang_analyzer_eval(x < y); // expected-warning{{FALSE}}
+ clang_analyzer_eval(y > x); // expected-warning{{FALSE}}
+ clang_analyzer_eval(x > y); // expected-warning{{TRUE}} expected-warning{{FALSE}}
+ clang_analyzer_eval(y < x); // expected-warning{{TRUE}} expected-warning{{FALSE}}
+ clang_analyzer_eval(x <= y); // expected-warning{{TRUE}} expected-warning{{FALSE}}
+ clang_analyzer_eval(y >= x); // expected-warning{{TRUE}} expected-warning{{FALSE}}
+ clang_analyzer_eval(x >= y); // expected-warning{{TRUE}}
+ clang_analyzer_eval(y <= x); // expected-warning{{TRUE}}
+ clang_analyzer_eval(x == y); // expected-warning{{TRUE}} expected-warning{{FALSE}}
+ clang_analyzer_eval(y == x); // expected-warning{{TRUE}} expected-warning{{FALSE}}
+ clang_analyzer_eval(x != y); // expected-warning{{TRUE}} expected-warning{{FALSE}}
+ clang_analyzer_eval(y != x); // expected-warning{{TRUE}} expected-warning{{FALSE}}
+ } else {
+ clang_analyzer_eval(x < y); // expected-warning{{TRUE}}
+ clang_analyzer_eval(y > x); // expected-warning{{TRUE}}
+ clang_analyzer_eval(x > y); // expected-warning{{FALSE}}
+ clang_analyzer_eval(y < x); // expected-warning{{FALSE}}
+ clang_analyzer_eval(x <= y); // expected-warning{{TRUE}}
+ clang_analyzer_eval(y >= x); // expected-warning{{TRUE}}
+ clang_analyzer_eval(x >= y); // expected-warning{{FALSE}}
+ clang_analyzer_eval(y <= x); // expected-warning{{FALSE}}
+ clang_analyzer_eval(x == y); // expected-warning{{FALSE}}
+ clang_analyzer_eval(y == x); // expected-warning{{FALSE}}
+ clang_analyzer_eval(x != y); // expected-warning{{TRUE}}
+ clang_analyzer_eval(y != x); // expected-warning{{TRUE}}
+ }
+}
+
+void comparison_eq(int x, int y) {
+ if (x == y) {
+ clang_analyzer_eval(x < y); // expected-warning{{FALSE}}
+ clang_analyzer_eval(y > x); // expected-warning{{FALSE}}
+ clang_analyzer_eval(x > y); // expected-warning{{FALSE}}
+ clang_analyzer_eval(y < x); // expected-warning{{FALSE}}
+ clang_analyzer_eval(x <= y); // expected-warning{{TRUE}}
+ clang_analyzer_eval(y >= x); // expected-warning{{TRUE}}
+ clang_analyzer_eval(x >= y); // expected-warning{{TRUE}}
+ clang_analyzer_eval(y <= x); // expected-warning{{TRUE}}
+ clang_analyzer_eval(x == y); // expected-warning{{TRUE}}
+ clang_analyzer_eval(y == x); // expected-warning{{TRUE}}
+ clang_analyzer_eval(x != y); // expected-warning{{FALSE}}
+ clang_analyzer_eval(y != x); // expected-warning{{FALSE}}
+ } else {
+ clang_analyzer_eval(x < y); // expected-warning{{TRUE}} expected-warning{{FALSE}}
+ clang_analyzer_eval(y > x); // expected-warning{{TRUE}} expected-warning{{FALSE}}
+ clang_analyzer_eval(x > y); // expected-warning{{TRUE}} expected-warning{{FALSE}}
+ clang_analyzer_eval(y < x); // expected-warning{{TRUE}} expected-warning{{FALSE}}
+ clang_analyzer_eval(x <= y); // expected-warning{{TRUE}} expected-warning{{FALSE}}
+ clang_analyzer_eval(y >= x); // expected-warning{{TRUE}} expected-warning{{FALSE}}
+ clang_analyzer_eval(x >= y); // expected-warning{{TRUE}} expected-warning{{FALSE}}
+ clang_analyzer_eval(y <= x); // expected-warning{{TRUE}} expected-warning{{FALSE}}
+ clang_analyzer_eval(x == y); // expected-warning{{FALSE}}
+ clang_analyzer_eval(y == x); // expected-warning{{FALSE}}
+ clang_analyzer_eval(x != y); // expected-warning{{TRUE}}
+ clang_analyzer_eval(y != x); // expected-warning{{TRUE}}
+ }
+}
+
+void comparison_ne(int x, int y) {
+ if (x != y) {
+ clang_analyzer_eval(x < y); // expected-warning{{TRUE}} expected-warning{{FALSE}}
+ clang_analyzer_eval(y > x); // expected-warning{{TRUE}} expected-warning{{FALSE}}
+ clang_analyzer_eval(x > y); // expected-warning{{TRUE}} expected-warning{{FALSE}}
+ clang_analyzer_eval(y < x); // expected-warning{{TRUE}} expected-warning{{FALSE}}
+ clang_analyzer_eval(x <= y); // expected-warning{{TRUE}} expected-warning{{FALSE}}
+ clang_analyzer_eval(y >= x); // expected-warning{{TRUE}} expected-warning{{FALSE}}
+ clang_analyzer_eval(x >= y); // expected-warning{{TRUE}} expected-warning{{FALSE}}
+ clang_analyzer_eval(y <= x); // expected-warning{{TRUE}} expected-warning{{FALSE}}
+ clang_analyzer_eval(x == y); // expected-warning{{FALSE}}
+ clang_analyzer_eval(y == x); // expected-warning{{FALSE}}
+ clang_analyzer_eval(x != y); // expected-warning{{TRUE}}
+ clang_analyzer_eval(y != x); // expected-warning{{TRUE}}
+ } else {
+ clang_analyzer_eval(x < y); // expected-warning{{FALSE}}
+ clang_analyzer_eval(y > x); // expected-warning{{FALSE}}
+ clang_analyzer_eval(x > y); // expected-warning{{FALSE}}
+ clang_analyzer_eval(y < x); // expected-warning{{FALSE}}
+ clang_analyzer_eval(x <= y); // expected-warning{{TRUE}}
+ clang_analyzer_eval(y >= x); // expected-warning{{TRUE}}
+ clang_analyzer_eval(x >= y); // expected-warning{{TRUE}}
+ clang_analyzer_eval(y <= x); // expected-warning{{TRUE}}
+ clang_analyzer_eval(x == y); // expected-warning{{TRUE}}
+ clang_analyzer_eval(y == x); // expected-warning{{TRUE}}
+ clang_analyzer_eval(x != y); // expected-warning{{FALSE}}
+ clang_analyzer_eval(y != x); // expected-warning{{FALSE}}
+ }
+}
\ No newline at end of file
Index: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
===================================================================
--- clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -305,8 +305,8 @@
RangeSet::Factory F;
RangeSet getRange(ProgramStateRef State, SymbolRef Sym);
- const RangeSet* getRangeForMinusSymbol(ProgramStateRef State,
- SymbolRef Sym);
+ const RangeSet *getRangeForMinusSymbol(ProgramStateRef State, SymbolRef Sym);
+ RangeSet getRangeForComparisonSymbol(ProgramStateRef State, SymbolRef Sym);
RangeSet getSymLTRange(ProgramStateRef St, SymbolRef Sym,
const llvm::APSInt &Int,
@@ -478,16 +478,23 @@
RangeSet RangeConstraintManager::getRange(ProgramStateRef State,
SymbolRef Sym) {
+ // If Sym is a comparison expression (except <=>),
+ // find any other comparisons with the same operands.
+ // See function description.
+ auto CmpRangeSet = getRangeForComparisonSymbol(State, Sym);
+ if (!CmpRangeSet.isEmpty())
+ return CmpRangeSet;
+
ConstraintRangeTy::data_type *V = State->get<ConstraintRange>(Sym);
// If Sym is a difference of symbols A - B, then maybe we have range set
// stored for B - A.
- BasicValueFactory &BV = getBasicVals();
const RangeSet *R = getRangeForMinusSymbol(State, Sym);
// If we have range set stored for both A - B and B - A then calculate the
// effective range set by intersecting the range set for A - B and the
// negated range set of B - A.
+ BasicValueFactory &BV = getBasicVals();
if (V && R)
return V->Intersect(BV, F, R->Negate(BV, F));
if (V)
@@ -538,6 +545,146 @@
return nullptr;
}
+// Returns ranges only for binary comparison operators (except <=>)
+// when left and right operands are symbolic values.
+// Finds any other comparisons with the same operands.
+// Then do logical calculations and refuse impossible branches.
+// E.g. (x < y) and (x > y) at the same time are impossible.
+// E.g. (x >= y) and (x != y) at the same time makes (x > y) true only.
+// E.g. (x == y) and (y == x) are just reversed but the same.
+// It covers all possible combinations (see CmpOpTable description).
+RangeSet
+RangeConstraintManager::getRangeForComparisonSymbol(ProgramStateRef State,
+ SymbolRef Sym) {
+ static_assert(BO_LT < BO_GT && BO_GT < BO_LE && BO_LE < BO_GE &&
+ BO_GE < BO_EQ && BO_EQ < BO_NE,
+ "This function relies on operators order. Rework it and "
+ "companions otherwise.");
+
+ enum TriState {
+ False = 0,
+ True,
+ Any,
+ };
+
+ // CmpOpTable holds states for the preceding comparison operation
+ // assuming the latter is true.
+ // E.g. assuming (x < y) is true that means (x != y) is surely true.
+ // if (x preciding_operation y) // < | != | >
+ // if (x operation y) // != | > | <
+ // tristate // True | Any | False
+ //
+ // CmpOpTable represents next:
+ // __|< |> |<=|>=|==|!=|AnyX2|
+ // < |1 |0 |* |0 |0 |* |1 |
+ // > |0 |1 |0 |* |0 |* |1 |
+ // <=|1 |0 |1 |* |1 |* |0 |
+ // >=|0 |1 |* |1 |1 |* |0 |
+ // ==|0 |0 |* |* |1 |0 |1 |
+ // !=|1 |1 |* |* |0 |1 |0 |
+ // Columns stands for a preceding operator.
+ // Rows stands for a current operator.
+ // AnyX2 means that two expressions marked as `Any` are met in code,
+ // and there is a special column for that, for example:
+ // if (x >= y)
+ // if (x != y)
+ // if (x <= y)
+ // False only
+ static constexpr size_t CmpOpCount = BO_NE - BO_LT + 1;
+ static const TriState CmpOpTable[CmpOpCount][CmpOpCount + 1] = {
+ // < > <= >= == != AnyX2
+ {True, False, Any, False, False, Any, True}, // <
+ {False, True, False, Any, False, Any, True}, // >
+ {True, False, True, Any, True, Any, False}, // <=
+ {False, True, Any, True, True, Any, False}, // >=
+ {False, False, Any, Any, True, False, True}, // ==
+ {True, True, Any, Any, False, True, False}, // !=
+ };
+
+ const RangeSet EmptyRangeSet = F.getEmptySet();
+
+ auto SSE = dyn_cast<SymSymExpr>(Sym);
+ if (!SSE)
+ return EmptyRangeSet;
+
+ auto OP = SSE->getOpcode();
+
+ // we currently do not support <=> (C++20)
+ if (!BinaryOperator::isComparisonOp(OP) || (OP == BO_Cmp))
+ return EmptyRangeSet;
+
+ auto IndexFromOp = [](BinaryOperatorKind OP) { return OP - BO_LT; };
+ auto OpFromIndex = [](size_t Index) {
+ return static_cast<BinaryOperatorKind>(Index + BO_LT);
+ };
+ auto NegateTristate = [](TriState State) {
+ return (State == False) ? True : ((State == True) ? False : Any);
+ };
+
+ auto IndexOP = IndexFromOp(OP);
+ auto LHS = SSE->getLHS();
+ auto RHS = SSE->getRHS();
+ QualType T = SSE->getType();
+ SymbolManager &SymMgr = State->getSymbolManager();
+ BasicValueFactory &BV = getBasicVals();
+ auto &Zero = BV.getValue(0, T);
+ auto &One = BV.getValue(1, T);
+ const RangeSet TrueRangeSet(F, One, One);
+ const RangeSet FalseRangeSet(F, Zero, Zero);
+ int AnyStates = 0;
+
+ for (size_t i = 0; i < CmpOpCount; ++i) {
+
+ // Let's find an expression e.g. (x < y).
+ OP = OpFromIndex(i);
+ auto SymSym = SymMgr.getSymSymExpr(LHS, OP, RHS, T);
+ const RangeSet *RangeSet = State->get<ConstraintRange>(SymSym);
+
+ // If ranges were not previously found,
+ // try to find a reversed expression (y > x).
+ if (!RangeSet) {
+ auto ROP = BinaryOperator::reverseComparisonOp(OP);
+ SymSym = SymMgr.getSymSymExpr(RHS, ROP, LHS, T);
+ RangeSet = State->get<ConstraintRange>(SymSym);
+ }
+
+ if (!RangeSet)
+ continue;
+
+ auto ConcreteValue = RangeSet->getConcreteValue();
+ assert(ConcreteValue &&
+ "RangeSet for comparison operator can only be a singleton.");
+ const bool isInFalseBranch = (*ConcreteValue == 0);
+ auto Index = i;
+
+ // If it is a false branch, we shall be guided by opposite operator,
+ // because the table is made assuming we are in the true branch.
+ // E.g. when (x <= y) is false, then (x > y) is true.
+ if (isInFalseBranch) {
+ auto NOP = BinaryOperator::negateComparisonOp(OP);
+ Index = IndexFromOp(NOP);
+ }
+
+ auto tristate = CmpOpTable[IndexOP][Index];
+
+ // If we met two any-state expressions,
+ // so current expr is also true.
+ // if (x <= y) // assume true
+ // if (x != y) // assume true
+ // if (x < y) // is also true
+ // Get a value from the last special column of the table.
+ if (tristate == Any)
+ if (++AnyStates == 2)
+ tristate = CmpOpTable[IndexOP][CmpOpCount];
+ else
+ continue;
+
+ return (tristate == True) ? TrueRangeSet : FalseRangeSet;
+ }
+
+ return EmptyRangeSet;
+}
+
//===------------------------------------------------------------------------===
// assumeSymX methods: protected interface for RangeConstraintManager.
//===------------------------------------------------------------------------===/
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
