forked from OSchip/llvm-project
[analyzer] Return from reAssume if State is posteriorly overconstrained
Depends on D124758. That patch introduced serious regression in the run-time in some special cases. This fixes that. Differential Revision: https://reviews.llvm.org/D126406
This commit is contained in:
parent
b0ccf38b01
commit
ca3d962548
|
@ -55,6 +55,8 @@ template <typename T> struct ProgramStateTrait {
|
|||
}
|
||||
};
|
||||
|
||||
class RangeSet;
|
||||
|
||||
/// \class ProgramState
|
||||
/// ProgramState - This class encapsulates:
|
||||
///
|
||||
|
@ -79,7 +81,6 @@ private:
|
|||
friend class ExplodedGraph;
|
||||
friend class ExplodedNode;
|
||||
friend class NodeBuilder;
|
||||
friend class ConstraintManager;
|
||||
|
||||
ProgramStateManager *stateMgr;
|
||||
Environment Env; // Maps a Stmt to its current SVal.
|
||||
|
@ -113,6 +114,16 @@ private:
|
|||
// posteriorly over-constrained. These parents are handled with special care:
|
||||
// we do not allow transitions to exploded nodes with such states.
|
||||
bool PosteriorlyOverconstrained = false;
|
||||
// Make internal constraint solver entities friends so they can access the
|
||||
// overconstrained-related functions. We want to keep this API inaccessible
|
||||
// for Checkers.
|
||||
friend class ConstraintManager;
|
||||
friend ProgramStateRef reAssume(ProgramStateRef State,
|
||||
const RangeSet *Constraint, SVal TheValue);
|
||||
bool isPosteriorlyOverconstrained() const {
|
||||
return PosteriorlyOverconstrained;
|
||||
}
|
||||
ProgramStateRef cloneAsPosteriorlyOverconstrained() const;
|
||||
|
||||
unsigned refCount;
|
||||
|
||||
|
@ -122,11 +133,6 @@ private:
|
|||
|
||||
void setStore(const StoreRef &storeRef);
|
||||
|
||||
ProgramStateRef cloneAsPosteriorlyOverconstrained() const;
|
||||
bool isPosteriorlyOverconstrained() const {
|
||||
return PosteriorlyOverconstrained;
|
||||
}
|
||||
|
||||
public:
|
||||
/// This ctor is used when creating the first ProgramState object.
|
||||
ProgramState(ProgramStateManager *mgr, const Environment& env,
|
||||
|
|
|
@ -2530,10 +2530,19 @@ EquivalenceClass::removeMember(ProgramStateRef State, const SymbolRef Old) {
|
|||
return State;
|
||||
}
|
||||
|
||||
// We must declare reAssume in clang::ento, otherwise we could not declare that
|
||||
// as a friend in ProgramState. More precisely, the call of reAssume would be
|
||||
// ambiguous (one in the global namespace and an other which is declared in
|
||||
// ProgramState is in clang::ento).
|
||||
namespace clang {
|
||||
namespace ento {
|
||||
// Re-evaluate an SVal with top-level `State->assume` logic.
|
||||
LLVM_NODISCARD ProgramStateRef reAssume(ProgramStateRef State,
|
||||
const RangeSet *Constraint,
|
||||
SVal TheValue) {
|
||||
assert(State);
|
||||
if (State->isPosteriorlyOverconstrained())
|
||||
return nullptr;
|
||||
if (!Constraint)
|
||||
return State;
|
||||
|
||||
|
@ -2556,6 +2565,8 @@ LLVM_NODISCARD ProgramStateRef reAssume(ProgramStateRef State,
|
|||
return State->assumeInclusiveRange(DefinedVal, Constraint->getMinValue(),
|
||||
Constraint->getMaxValue(), true);
|
||||
}
|
||||
} // namespace ento
|
||||
} // namespace clang
|
||||
|
||||
// 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
|
||||
|
|
|
@ -0,0 +1,55 @@
|
|||
// RUN: %clang_analyze_cc1 %s \
|
||||
// RUN: -analyzer-checker=core,alpha.security.ArrayBoundV2 \
|
||||
// RUN: -analyzer-checker=debug.ExprInspection \
|
||||
// RUN: -triple x86_64-unknown-linux-gnu \
|
||||
// RUN: -verify
|
||||
|
||||
// This test is here to check if there is no significant run-time regression
|
||||
// related to the assume machinery. The analysis should finish in less than 10
|
||||
// seconds.
|
||||
|
||||
// expected-no-diagnostics
|
||||
|
||||
typedef unsigned char uint8_t;
|
||||
typedef unsigned short uint16_t;
|
||||
typedef unsigned long uint64_t;
|
||||
|
||||
int filter_slice_word(int sat_linesize, int sigma, int radius, uint64_t *sat,
|
||||
uint64_t *square_sat, int width, int height,
|
||||
int src_linesize, int dst_linesize, const uint16_t *src,
|
||||
uint16_t *dst, int jobnr, int nb_jobs) {
|
||||
const int starty = height * jobnr / nb_jobs;
|
||||
const int endy = height * (jobnr + 1) / nb_jobs;
|
||||
|
||||
for (int y = starty; y < endy; y++) {
|
||||
|
||||
int lower_y = y - radius < 0 ? 0 : y - radius;
|
||||
int higher_y = y + radius + 1 > height ? height : y + radius + 1;
|
||||
int dist_y = higher_y - lower_y;
|
||||
|
||||
for (int x = 0; x < width; x++) {
|
||||
|
||||
int lower_x = x - radius < 0 ? 0 : x - radius;
|
||||
int higher_x = x + radius + 1 > width ? width : x + radius + 1;
|
||||
int count = dist_y * (higher_x - lower_x);
|
||||
|
||||
// The below hunk caused significant regression in run-time.
|
||||
#if 1
|
||||
uint64_t sum = sat[higher_y * sat_linesize + higher_x] -
|
||||
sat[higher_y * sat_linesize + lower_x] -
|
||||
sat[lower_y * sat_linesize + higher_x] +
|
||||
sat[lower_y * sat_linesize + lower_x];
|
||||
uint64_t square_sum = square_sat[higher_y * sat_linesize + higher_x] -
|
||||
square_sat[higher_y * sat_linesize + lower_x] -
|
||||
square_sat[lower_y * sat_linesize + higher_x] +
|
||||
square_sat[lower_y * sat_linesize + lower_x];
|
||||
uint64_t mean = sum / count;
|
||||
uint64_t var = (square_sum - sum * sum / count) / count;
|
||||
dst[y * dst_linesize + x] =
|
||||
(sigma * mean + var * src[y * src_linesize + x]) / (sigma + var);
|
||||
#endif
|
||||
|
||||
}
|
||||
}
|
||||
return 0;
|
||||
}
|
Loading…
Reference in New Issue