diff --git a/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp b/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp --- a/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp +++ b/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 @@ -955,18 +955,7 @@ } RangeSet VisitBinaryOperator(RangeSet LHS, BinaryOperator::Opcode Op, - RangeSet RHS, QualType T) { - switch (Op) { - case BO_Or: - return VisitBinaryOperator(LHS, RHS, T); - case BO_And: - return VisitBinaryOperator(LHS, RHS, T); - case BO_Rem: - return VisitBinaryOperator(LHS, RHS, T); - default: - return infer(T); - } - } + RangeSet RHS, QualType T); //===----------------------------------------------------------------------===// // Ranges and operators @@ -1231,6 +1220,29 @@ // Range-based reasoning about symbolic operations //===----------------------------------------------------------------------===// +template <> +RangeSet SymbolicRangeInferrer::VisitBinaryOperator(RangeSet LHS, + RangeSet RHS, + QualType T) { + // When both the RangeSets are non-overlapping then all possible pairs of + // (x, y) in LHS, RHS respectively, will satisfy expression (x != y). + if ((LHS.getMaxValue() < RHS.getMinValue()) || + (LHS.getMinValue() > RHS.getMaxValue())) { + return getTrueRange(T); + } + + // If both RangeSets contain only one Point which is equal then the + // expression will always return true. + if ((LHS.getMinValue() == RHS.getMaxValue()) && + (LHS.getMaxValue() == RHS.getMaxValue()) && + (LHS.getMinValue() == RHS.getMinValue())) { + return getFalseRange(T); + } + + // In all other cases, the resulting range cannot be deduced. + return infer(T); +} + template <> RangeSet SymbolicRangeInferrer::VisitBinaryOperator(Range LHS, Range RHS, QualType T) { @@ -1391,6 +1403,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(LHS, RHS, T); + case BO_Or: + return VisitBinaryOperator(LHS, RHS, T); + case BO_And: + return VisitBinaryOperator(LHS, RHS, T); + case BO_Rem: + return VisitBinaryOperator(LHS, RHS, T); + default: + return infer(T); + } +} + //===----------------------------------------------------------------------===// // Constraint manager implementation details //===----------------------------------------------------------------------===// diff --git a/clang/test/Analysis/constant-folding.c b/clang/test/Analysis/constant-folding.c --- a/clang/test/Analysis/constant-folding.c +++ b/clang/test/Analysis/constant-folding.c @@ -281,3 +281,49 @@ 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}} + } +}