manas created this revision.
Herald added subscribers: steakhal, ASDenysPetrov, martong, dkrupp, donat.nagy,
Szelethus, mikhail.ramalho, a.sidorin, szepet, baloghadamsoftware, xazax.hun.
manas requested review of this revision.
Herald added a project: clang.
Herald added a subscriber: cfe-commits.
With this patch, the solver can infer results for not equal to operator
over Ranges as well. This also fixes the issue of comparison between
different types, by first converting the RangeSets to resulting type,
which then can be used for comparisons.
Repository:
rG LLVM Github Monorepo
https://reviews.llvm.org/D114758
Files:
clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
clang/test/Analysis/constant-folding.c
Index: clang/test/Analysis/constant-folding.c
===================================================================
--- clang/test/Analysis/constant-folding.c
+++ clang/test/Analysis/constant-folding.c
@@ -281,3 +281,55 @@
clang_analyzer_eval((b % a) < x + 10); // expected-warning{{TRUE}}
}
}
+
+void testDisequalityRules(unsigned int u1, unsigned int u2, int s1, int s2) {
+ // Checks when ranges are not overlapping
+ if (u1 <= 10 && u2 >= 20) {
+ // u1: [0,10], u2: [20,UINT_MAX]
+ clang_analyzer_eval((u1 != u2) != 0); // expected-warning{{TRUE}}
+ }
+
+ if (s1 <= INT_MIN + 10 && s2 >= INT_MAX - 10) {
+ // s1: [INT_MIN,INT_MIN + 10], s2: [INT_MAX - 10,INT_MAX]
+ clang_analyzer_eval((s1 != s2) == 0); // expected-warning{{FALSE}}
+ }
+
+ // Checks when ranges are completely overlapping and have more than one point
+ if (u1 >= 20 && u1 <= 50 && u2 >= 20 && u2 <= 50) {
+ // u1: [20,50], u2: [20,50]
+ clang_analyzer_eval((u1 != u2) != 0); // expected-warning{{UNKNOWN}}
+ }
+
+ if (s1 >= -20 && s1 <= 20 && s2 >= -20 && s2 <= 20) {
+ // s1: [-20,20], s2: [-20,20]
+ clang_analyzer_eval((s1 != s2) != 0); // expected-warning{{UNKNOWN}}
+ }
+
+ // Checks when ranges are partially overlapping
+ if (u1 >= 100 && u1 <= 200 && u2 >= 150 && u2 <= 300) {
+ // u1: [100,200], u2: [150,300]
+ clang_analyzer_eval((u1 != u2) != 0); // expected-warning{{UNKNOWN}}
+ }
+
+ if (s1 >= -80 && s1 <= -50 && s2 >= -100 && s2 <= -75) {
+ // s1: [-80,-50], s2: [-100,-75]
+ clang_analyzer_eval((s1 != s2) == 0); // expected-warning{{UNKNOWN}}
+ }
+
+ // Checks for ranges which are subset of one-another
+ if (u1 >= 500 && u1 <= 1000 && u2 >= 750 && u2 <= 1000) {
+ // u1: [500,1000], u2: [750,1000]
+ clang_analyzer_eval((u1 != u2) == 0); // expected-warning{{UNKNOWN}}
+ }
+
+ if (s1 >= -1000 && s1 <= -500 && s2 <= -500 && s2 >= -750) {
+ // s1: [-1000,-500], s2: [-500,-750]
+ clang_analyzer_eval((s1 != s2) == 0); // expected-warning{{UNKNOWN}}
+ }
+
+ // Checks for comparison between different types
+ if (u1 <= 255 && s1 <= 0) {
+ // u1: [0, 255], s1: [INT_MIN, 0]
+ clang_analyzer_eval((u1 != s1) == 0); // expected-warning{{UNKNOWN}}
+ }
+}
Index: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
===================================================================
--- clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -20,8 +20,8 @@
#include "llvm/ADT/FoldingSet.h"
#include "llvm/ADT/ImmutableSet.h"
#include "llvm/ADT/STLExtras.h"
-#include "llvm/ADT/StringExtras.h"
#include "llvm/ADT/SmallSet.h"
+#include "llvm/ADT/StringExtras.h"
#include "llvm/Support/Compiler.h"
#include "llvm/Support/raw_ostream.h"
#include <algorithm>
@@ -960,18 +960,7 @@
}
RangeSet VisitBinaryOperator(RangeSet LHS, BinaryOperator::Opcode Op,
- RangeSet RHS, QualType T) {
- switch (Op) {
- case BO_Or:
- return VisitBinaryOperator<BO_Or>(LHS, RHS, T);
- case BO_And:
- return VisitBinaryOperator<BO_And>(LHS, RHS, T);
- case BO_Rem:
- return VisitBinaryOperator<BO_Rem>(LHS, RHS, T);
- default:
- return infer(T);
- }
- }
+ RangeSet RHS, QualType T);
//===----------------------------------------------------------------------===//
// Ranges and operators
@@ -1236,6 +1225,67 @@
// Range-based reasoning about symbolic operations
//===----------------------------------------------------------------------===//
+template <>
+RangeSet SymbolicRangeInferrer::VisitBinaryOperator<BO_NE>(RangeSet LHS,
+ RangeSet RHS,
+ QualType T) {
+
+ // We must check for empty RangeSets. This gets done via VisitBinaryOperator
+ // for other operators, but BO_NE is handled specifically.
+ if (LHS.isEmpty() || RHS.isEmpty()) {
+ return RangeFactory.getEmptySet();
+ }
+
+ APSIntType ResultType = ValueFactory.getAPSIntType(T);
+
+ RangeSet ConvertedLHS = RangeFactory.getEmptySet();
+ RangeSet ConvertedRHS = RangeFactory.getEmptySet();
+
+ // Convert each Range inside the RangeSet to given type. This will make it
+ // possible to have comparisons between different APSInts.
+ for (auto LRange : LHS) {
+ auto ConvertedLRange = convert(LRange, ResultType);
+
+ // If any of the converted Range is not bounded within the limits of the
+ // type, then we must not compare the APSInt values. Hence, we have no
+ // option other than to infer results via type.
+ if (!ConvertedLRange) {
+ return infer(T);
+ }
+
+ ConvertedLHS = RangeFactory.add(ConvertedLHS, ConvertedLRange.getValue());
+ }
+
+ for (auto RRange : RHS) {
+ auto ConvertedRRange = convert(RRange, ResultType);
+
+ if (!ConvertedRRange) {
+ return infer(T);
+ }
+
+ ConvertedRHS = RangeFactory.add(ConvertedRHS, ConvertedRRange.getValue());
+ }
+
+ // When both the Ranges are non-overlapping then all possible pairs of (x, y)
+ // in ConvertedLHS, ConvertedRHS respectively, will satisfy expression
+ // (x != y).
+ if ((ConvertedLHS.getMaxValue() < ConvertedRHS.getMinValue()) ||
+ (ConvertedLHS.getMinValue() > ConvertedRHS.getMaxValue())) {
+ return getTrueRange(T);
+ }
+
+ // If both Ranges contain only one Point which is equal, then the expression
+ // will always return true.
+ if ((ConvertedLHS.getMinValue() == ConvertedRHS.getMaxValue()) &&
+ (ConvertedLHS.getMaxValue() == ConvertedRHS.getMaxValue()) &&
+ (ConvertedLHS.getMinValue() == ConvertedRHS.getMinValue())) {
+ return getFalseRange(T);
+ }
+
+ // In all other cases, the resulting range cannot be deduced.
+ return infer(T);
+}
+
template <>
RangeSet SymbolicRangeInferrer::VisitBinaryOperator<BO_Or>(Range LHS, Range RHS,
QualType T) {
@@ -1396,6 +1446,23 @@
return {RangeFactory, ValueFactory.getValue(Min), ValueFactory.getValue(Max)};
}
+RangeSet SymbolicRangeInferrer::VisitBinaryOperator(RangeSet LHS,
+ BinaryOperator::Opcode Op,
+ RangeSet RHS, QualType T) {
+ switch (Op) {
+ case BO_NE:
+ return VisitBinaryOperator<BO_NE>(LHS, RHS, T);
+ case BO_Or:
+ return VisitBinaryOperator<BO_Or>(LHS, RHS, T);
+ case BO_And:
+ return VisitBinaryOperator<BO_And>(LHS, RHS, T);
+ case BO_Rem:
+ return VisitBinaryOperator<BO_Rem>(LHS, RHS, T);
+ default:
+ return infer(T);
+ }
+}
+
//===----------------------------------------------------------------------===//
// Constraint manager implementation details
//===----------------------------------------------------------------------===//
@@ -1724,7 +1791,6 @@
RangeSet::Factory &RangeFactory;
};
-
bool ConstraintAssignor::assignSymExprToConst(const SymExpr *Sym,
const llvm::APSInt &Constraint) {
llvm::SmallSet<EquivalenceClass, 4> SimplifiedClasses;
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
