martong updated this revision to Diff 350898.
martong added a comment.
- Simplify the symbol before eq tracking as well
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D103314/new/
https://reviews.llvm.org/D103314
Files:
clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
clang/test/Analysis/find-binop-constraints.cpp
Index: clang/test/Analysis/find-binop-constraints.cpp
===================================================================
--- /dev/null
+++ clang/test/Analysis/find-binop-constraints.cpp
@@ -0,0 +1,163 @@
+// RUN: %clang_analyze_cc1 %s \
+// RUN: -analyzer-checker=core \
+// RUN: -analyzer-checker=debug.ExprInspection \
+// RUN: -analyzer-config eagerly-assume=false \
+// RUN: -verify
+
+void clang_analyzer_eval(bool);
+void clang_analyzer_warnIfReached();
+
+int test_legacy_behavior(int x, int y) {
+ if (y != 0)
+ return 0;
+ if (x + y != 0)
+ return 0;
+ clang_analyzer_eval(x + y == 0); // expected-warning{{TRUE}}
+ clang_analyzer_eval(y == 0); // expected-warning{{TRUE}}
+ return y / (x + y); // expected-warning{{Division by zero}}
+}
+
+int test_rhs_further_constrained(int x, int y) {
+ if (x + y != 0)
+ return 0;
+ if (y != 0)
+ return 0;
+ clang_analyzer_eval(x + y == 0); // expected-warning{{TRUE}}
+ clang_analyzer_eval(y == 0); // expected-warning{{TRUE}}
+ return 0;
+}
+
+int test_lhs_further_constrained(int x, int y) {
+ if (x + y != 0)
+ return 0;
+ if (x != 0)
+ return 0;
+ clang_analyzer_eval(x + y == 0); // expected-warning{{TRUE}}
+ clang_analyzer_eval(x == 0); // expected-warning{{TRUE}}
+ return 0;
+}
+
+int test_lhs_and_rhs_further_constrained(int x, int y) {
+ if (x % y != 1)
+ return 0;
+ if (x != 1)
+ return 0;
+ if (y != 2)
+ return 0;
+ clang_analyzer_eval(x % y == 1); // expected-warning{{TRUE}}
+ clang_analyzer_eval(y == 2); // expected-warning{{TRUE}}
+ return 0;
+}
+
+int test_commutativity(int x, int y) {
+ if (x + y != 0)
+ return 0;
+ if (y != 0)
+ return 0;
+ clang_analyzer_eval(y + x == 0); // expected-warning{{TRUE}}
+ clang_analyzer_eval(y == 0); // expected-warning{{TRUE}}
+ return 0;
+}
+
+int test_binop_when_height_is_2_r(int a, int x, int y, int z) {
+ switch (a) {
+ case 1: {
+ if (x + y + z != 0)
+ return 0;
+ if (z != 0)
+ return 0;
+ clang_analyzer_eval(x + y + z == 0); // expected-warning{{TRUE}}
+ clang_analyzer_eval(z == 0); // expected-warning{{TRUE}}
+ break;
+ }
+ case 2: {
+ if (x + y + z != 0)
+ return 0;
+ if (y != 0)
+ return 0;
+ clang_analyzer_eval(x + y + z == 0); // expected-warning{{TRUE}}
+ clang_analyzer_eval(y == 0); // expected-warning{{TRUE}}
+ break;
+ }
+ case 3: {
+ if (x + y + z != 0)
+ return 0;
+ if (x != 0)
+ return 0;
+ clang_analyzer_eval(x + y + z == 0); // expected-warning{{TRUE}}
+ clang_analyzer_eval(x == 0); // expected-warning{{TRUE}}
+ break;
+ }
+ case 4: {
+ if (x + y + z != 0)
+ return 0;
+ if (x + y != 0)
+ return 0;
+ clang_analyzer_eval(x + y + z == 0); // expected-warning{{TRUE}}
+ clang_analyzer_eval(x + y == 0); // expected-warning{{TRUE}}
+ break;
+ }
+ case 5: {
+ if (z != 0)
+ return 0;
+ if (x + y + z != 0)
+ return 0;
+ clang_analyzer_eval(x + y + z == 0); // expected-warning{{TRUE}}
+ if (y != 0)
+ return 0;
+ clang_analyzer_eval(y == 0); // expected-warning{{TRUE}}
+ clang_analyzer_eval(z == 0); // expected-warning{{TRUE}}
+ clang_analyzer_eval(x + y + z == 0); // expected-warning{{TRUE}}
+ break;
+ }
+
+ }
+ return 0;
+}
+
+void test_equivalence_classes_are_updated(int a, int b, int c, int d) {
+ if (a + b != c)
+ return;
+ if (a != d)
+ return;
+ if (b != 0)
+ return;
+ clang_analyzer_eval(c == d); // expected-warning{{TRUE}}
+ // Keep the symbols and the constraints! alive.
+ (void)(a * b * c * d);
+ return;
+}
+
+void test_contradiction(int a, int b, int c, int d) {
+ if (a + b != c)
+ return;
+ if (a == c)
+ return;
+ clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+
+ // Bring in the contradiction.
+ if (b != 0)
+ return;
+ clang_analyzer_warnIfReached(); // no-warning, i.e. UNREACHABLE
+ // Keep the symbols and the constraints! alive.
+ (void)(a * b * c * d);
+ return;
+}
+
+void test_deferred_contradiction(int e0, int b0, int b1) {
+
+ int e1 = e0 - b0; // e1 is bound to (reg_$0<int e0>) - (reg_$1<int b0>)
+ (void)(b0 == 2);
+
+ int e2 = e1 - b1;
+ if (e2 > 0) { // b1 != e1
+ clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+ // Here, e1 is still bound to (reg_$0<int e0>) - (reg_$1<int b0>) but we
+ // should be able to simplify it to (reg_$0<int e0>) - 2 and thus realize
+ // the contradiction.
+ if (b1 == e1) {
+ clang_analyzer_warnIfReached(); // no-warning, i.e. UNREACHABLE
+ (void)(b0 * b1 * e0 * e1 * e2);
+ }
+ }
+}
Index: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
===================================================================
--- clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -20,6 +20,7 @@
#include "llvm/ADT/FoldingSet.h"
#include "llvm/ADT/ImmutableSet.h"
#include "llvm/ADT/STLExtras.h"
+#include "llvm/ADT/SmallSet.h"
#include "llvm/Support/Compiler.h"
#include "llvm/Support/raw_ostream.h"
#include <algorithm>
@@ -581,9 +582,20 @@
LLVM_NODISCARD inline ClassSet
getDisequalClasses(DisequalityMapTy Map, ClassSet::Factory &Factory) const;
+ LLVM_NODISCARD static inline Optional<bool> areEqual(ProgramStateRef State,
+ EquivalenceClass First,
+ EquivalenceClass Second);
LLVM_NODISCARD static inline Optional<bool>
areEqual(ProgramStateRef State, SymbolRef First, SymbolRef Second);
+ LLVM_NODISCARD inline Optional<bool> isEqualTo(ProgramStateRef State,
+ EquivalenceClass Other) const;
+
+ /// Iterate over all symbols and try to simplify them.
+ LLVM_NODISCARD ProgramStateRef simplify(SValBuilder &SVB,
+ RangeSet::Factory &F,
+ ProgramStateRef State);
+
/// Check equivalence data for consistency.
LLVM_NODISCARD LLVM_ATTRIBUTE_UNUSED static bool
isClassDataConsistent(ProgramStateRef State);
@@ -1374,6 +1386,12 @@
// 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)
@@ -1487,6 +1505,9 @@
// 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,
@@ -1553,9 +1574,47 @@
return State->set<ConstraintRange>(Constraints);
}
+ // Associate a constraint to a symbolic expression. First, we set the
+ // constraint in the State, then we try to simplify existing symbolic
+ // expressions based on the newly set constraint.
LLVM_NODISCARD inline ProgramStateRef
setConstraint(ProgramStateRef State, SymbolRef Sym, RangeSet Constraint) {
- return setConstraint(State, EquivalenceClass::find(State, Sym), Constraint);
+ assert(State);
+
+ State = setConstraint(State, EquivalenceClass::find(State, Sym), Constraint);
+ if (!State)
+ return nullptr;
+
+ // We have a chance to simplify existing symbolic values if the new
+ // constraint is a constant.
+ if (!Constraint.getConcreteValue())
+ return State;
+
+ llvm::SmallSet<EquivalenceClass, 4> SimplifiedClasses;
+ // Iterate over all equivalence classes and try to simplify them.
+ ClassMembersTy Members = State->get<ClassMembers>();
+ for (std::pair<EquivalenceClass, SymbolSet> ClassToSymbolSet : Members) {
+ EquivalenceClass Class = ClassToSymbolSet.first;
+ State = Class.simplify(getSValBuilder(), F, State);
+ if (!State)
+ return nullptr;
+ SimplifiedClasses.insert(Class);
+ }
+
+ // Trivial equivalence classes (those that have only one symbol member) are
+ // not stored in the State. Thus, we must skim through the constraints as
+ // well. And we try to simplify symbols in the constraints.
+ ConstraintRangeTy Constraints = State->get<ConstraintRange>();
+ for (std::pair<EquivalenceClass, RangeSet> ClassConstraint : Constraints) {
+ EquivalenceClass Class = ClassConstraint.first;
+ if (SimplifiedClasses.count(Class)) // Already simplified.
+ continue;
+ State = Class.simplify(getSValBuilder(), F, State);
+ if (!State)
+ return nullptr;
+ }
+
+ return State;
}
};
@@ -1591,6 +1650,8 @@
inline EquivalenceClass EquivalenceClass::find(ProgramStateRef State,
SymbolRef Sym) {
+ assert(State && "State should not be null");
+ assert(Sym && "Symbol should not be null");
// We store far from all Symbol -> Class mappings
if (const EquivalenceClass *NontrivialClass = State->get<ClassMap>(Sym))
return *NontrivialClass;
@@ -1722,6 +1783,10 @@
// 4. Update disequality relations
ClassSet DisequalToOther = Other.getDisequalClasses(DisequalityInfo, CF);
+ // We are about to merge two classes but they are already known to be
+ // non-equal. This is a contradiction.
+ if (DisequalToOther.contains(*this))
+ return nullptr;
if (!DisequalToOther.isEmpty()) {
ClassSet DisequalToThis = getDisequalClasses(DisequalityInfo, CF);
DisequalityInfo = DF.remove(DisequalityInfo, Other);
@@ -1868,9 +1933,13 @@
inline Optional<bool> EquivalenceClass::areEqual(ProgramStateRef State,
SymbolRef FirstSym,
SymbolRef SecondSym) {
- EquivalenceClass First = find(State, FirstSym);
- EquivalenceClass Second = find(State, SecondSym);
+ return EquivalenceClass::areEqual(State, find(State, FirstSym),
+ find(State, SecondSym));
+}
+inline Optional<bool> EquivalenceClass::areEqual(ProgramStateRef State,
+ EquivalenceClass First,
+ EquivalenceClass Second) {
// The same equivalence class => symbols are equal.
if (First == Second)
return true;
@@ -1885,6 +1954,47 @@
return llvm::None;
}
+LLVM_NODISCARD inline Optional<bool>
+EquivalenceClass::isEqualTo(ProgramStateRef State,
+ EquivalenceClass Other) const {
+ return EquivalenceClass::areEqual(State, *this, Other);
+}
+
+// Iterate over all symbols and try to simplify them. Once a symbol is
+// simplified then we check if we can merge the simplified symbol's equivalence
+// class to the this class. This way, we simplify not just the symbols but the
+// classes as well: we strive to keep the number of the classes to be the
+// absolute minimum.
+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);
+ if (SimplifiedMemberSym && MemberSym != SimplifiedMemberSym) {
+ EquivalenceClass ClassOfSimplifiedSym =
+ EquivalenceClass::find(State, SimplifiedMemberSym);
+ Optional<bool> KnownClassEquality =
+ isEqualTo(State, ClassOfSimplifiedSym);
+ if (KnownClassEquality) {
+ // The classes are already equal, there is no need to merge.
+ if (*KnownClassEquality == true)
+ continue;
+ // We are about to add the newly simplified symbol to this equivalence
+ // class, but they are known to be non-equal. This is a contradiction.
+ if (*KnownClassEquality == false)
+ return nullptr;
+ }
+ // The simplified symbol should be the member of the original Class,
+ // however, it might be in another existing class at the moment. We
+ // have to merge these classes.
+ State = merge(SVB.getBasicValueFactory(), F, State, ClassOfSimplifiedSym);
+ if (!State)
+ return nullptr;
+ }
+ }
+ return State;
+}
+
inline ClassSet EquivalenceClass::getDisequalClasses(ProgramStateRef State,
SymbolRef Sym) {
return find(State, Sym).getDisequalClasses(State);
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
@@ -256,7 +256,7 @@
/// by FoldingSet.
void Profile(llvm::FoldingSetNodeID &ID) const { Profile(ID, *this); }
- /// getConcreteValue - If a symbol is contrained to equal a specific integer
+ /// getConcreteValue - If a symbol is constrained to equal a specific integer
/// constant then this method returns that value. Otherwise, it returns
/// NULL.
const llvm::APSInt *getConcreteValue() const {
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
