forked from OSchip/llvm-project
[analyzer][solver] Prevent infeasible states (PR49490)
This patch fixes the situation when our knowledge of disequalities can help us figuring out that some assumption is infeasible, but the solver still produces a state with inconsistent constraints. Additionally, this patch adds a couple of assertions to catch this type of problems easier. Differential Revision: https://reviews.llvm.org/D98341
This commit is contained in:
parent
f50aef745c
commit
6dc1523508
|
@ -19,6 +19,8 @@
|
|||
#include "clang/StaticAnalyzer/Core/PathSensitive/SValVisitor.h"
|
||||
#include "llvm/ADT/FoldingSet.h"
|
||||
#include "llvm/ADT/ImmutableSet.h"
|
||||
#include "llvm/ADT/STLExtras.h"
|
||||
#include "llvm/Support/Compiler.h"
|
||||
#include "llvm/Support/raw_ostream.h"
|
||||
|
||||
using namespace clang;
|
||||
|
@ -1395,12 +1397,23 @@ private:
|
|||
return EquivalenceClass::merge(getBasicVals(), F, State, LHS, RHS);
|
||||
}
|
||||
|
||||
LLVM_NODISCARD inline ProgramStateRef setConstraint(ProgramStateRef State,
|
||||
EquivalenceClass Class,
|
||||
RangeSet Constraint) {
|
||||
LLVM_NODISCARD LLVM_ATTRIBUTE_UNUSED static bool
|
||||
areFeasible(ConstraintRangeTy Constraints) {
|
||||
return llvm::none_of(
|
||||
Constraints,
|
||||
[](const std::pair<EquivalenceClass, RangeSet> &ClassConstraint) {
|
||||
return ClassConstraint.second.isEmpty();
|
||||
});
|
||||
}
|
||||
|
||||
LLVM_NODISCARD ProgramStateRef setConstraint(ProgramStateRef State,
|
||||
EquivalenceClass Class,
|
||||
RangeSet Constraint) {
|
||||
ConstraintRangeTy Constraints = State->get<ConstraintRange>();
|
||||
ConstraintRangeTy::Factory &CF = State->get_context<ConstraintRange>();
|
||||
|
||||
assert(!Constraint.isEmpty() && "New constraint should not be empty");
|
||||
|
||||
// Add new constraint.
|
||||
Constraints = CF.add(Constraints, Class, Constraint);
|
||||
|
||||
|
@ -1413,9 +1426,18 @@ private:
|
|||
for (EquivalenceClass DisequalClass : Class.getDisequalClasses(State)) {
|
||||
RangeSet UpdatedConstraint =
|
||||
getRange(State, DisequalClass).Delete(getBasicVals(), F, *Point);
|
||||
|
||||
// If we end up with at least one of the disequal classes to be
|
||||
// constrainted with an empty range-set, the state is infeasible.
|
||||
if (UpdatedConstraint.isEmpty())
|
||||
return nullptr;
|
||||
|
||||
Constraints = CF.add(Constraints, DisequalClass, UpdatedConstraint);
|
||||
}
|
||||
|
||||
assert(areFeasible(Constraints) && "Constraint manager shouldn't produce "
|
||||
"a state with infeasible constraints");
|
||||
|
||||
return State->set<ConstraintRange>(Constraints);
|
||||
}
|
||||
|
||||
|
|
|
@ -0,0 +1,30 @@
|
|||
// RUN: %clang_analyze_cc1 -w -analyzer-checker=core -verify %s
|
||||
|
||||
// expected-no-diagnostics
|
||||
|
||||
struct toggle {
|
||||
bool value;
|
||||
};
|
||||
|
||||
toggle global_toggle;
|
||||
toggle get_global_toggle() { return global_toggle; }
|
||||
|
||||
int oob_access();
|
||||
|
||||
bool compare(toggle one, bool other) {
|
||||
if (one.value != other)
|
||||
return true;
|
||||
|
||||
if (one.value)
|
||||
oob_access();
|
||||
return true;
|
||||
}
|
||||
|
||||
bool coin();
|
||||
|
||||
void bar() {
|
||||
bool left = coin();
|
||||
bool right = coin();
|
||||
for (;;)
|
||||
compare(get_global_toggle(), left) && compare(get_global_toggle(), right);
|
||||
}
|
Loading…
Reference in New Issue