martong updated this revision to Diff 430611.
martong added a comment.
- Split into two patches, this first patch will be just the no-brainer
copy-paste from assumeDual implementaton.
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D125892/new/
https://reviews.llvm.org/D125892
Files:
clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
clang/include/clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h
clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
clang/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
Index: clang/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
===================================================================
--- clang/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
+++ clang/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
@@ -91,7 +91,7 @@
} // end switch
}
-ProgramStateRef SimpleConstraintManager::assumeInclusiveRange(
+ProgramStateRef SimpleConstraintManager::assumeInclusiveRangeInternal(
ProgramStateRef State, NonLoc Value, const llvm::APSInt &From,
const llvm::APSInt &To, bool InRange) {
Index: clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
===================================================================
--- clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
+++ clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
@@ -71,8 +71,49 @@
return ProgramStatePair(StTrue, StFalse);
}
+ConstraintManager::ProgramStatePair
+ConstraintManager::assumeInclusiveRangeDual(ProgramStateRef State, NonLoc Value,
+ const llvm::APSInt &From,
+ const llvm::APSInt &To) {
+ ProgramStateRef StInRange =
+ assumeInclusiveRangeInternal(State, Value, From, To, true);
+ if (!StInRange) {
+ ProgramStateRef StOutOfRange =
+ assumeInclusiveRangeInternal(State, Value, From, To, false);
+ if (LLVM_UNLIKELY(!StOutOfRange)) { // both infeasible
+ ProgramStateRef StInfeasible = State->cloneAsPosteriorlyOverconstrained();
+ assert(StInfeasible->isPosteriorlyOverconstrained());
+ // Checkers might rely on the API contract that both returned states
+ // cannot be null. Thus, we return StInfeasible for both branches because
+ // it might happen that a Checker uncoditionally uses one of them if the
+ // other is a nullptr. This may also happen with the non-dual and
+ // adjacent `assume(true)` and `assume(false)` calls. By implementing
+ // assume in therms of assumeDual, we can keep our API contract there as
+ // well.
+ return ProgramStatePair(StInfeasible, StInfeasible);
+ }
+ }
+
+ ProgramStateRef StOutOfRange =
+ assumeInclusiveRangeInternal(State, Value, From, To, false);
+ if (!StOutOfRange) {
+ return ProgramStatePair(StInRange, nullptr);
+ }
+
+ return ProgramStatePair(StInRange, StOutOfRange);
+}
+
ProgramStateRef ConstraintManager::assume(ProgramStateRef State,
DefinedSVal Cond, bool Assumption) {
ConstraintManager::ProgramStatePair R = assumeDual(State, Cond);
return Assumption ? R.first : R.second;
}
+
+ProgramStateRef
+ConstraintManager::assumeInclusiveRange(ProgramStateRef State, NonLoc Value,
+ const llvm::APSInt &From,
+ const llvm::APSInt &To, bool InBound) {
+ ConstraintManager::ProgramStatePair R =
+ assumeInclusiveRangeDual(State, Value, From, To);
+ return InBound ? R.first : R.second;
+}
Index: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h
===================================================================
--- clang/include/clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h
+++ clang/include/clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h
@@ -39,10 +39,11 @@
ProgramStateRef assumeInternal(ProgramStateRef State, DefinedSVal Cond,
bool Assumption) override;
- ProgramStateRef assumeInclusiveRange(ProgramStateRef State, NonLoc Value,
- const llvm::APSInt &From,
- const llvm::APSInt &To,
- bool InRange) override;
+ ProgramStateRef assumeInclusiveRangeInternal(ProgramStateRef State,
+ NonLoc Value,
+ const llvm::APSInt &From,
+ const llvm::APSInt &To,
+ bool InRange) override;
protected:
//===------------------------------------------------------------------===//
Index: clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
===================================================================
--- clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
+++ clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
@@ -94,35 +94,18 @@
/// not perfectly precise and this may happen very rarely.)
ProgramStatePair assumeDual(ProgramStateRef State, DefinedSVal Cond);
- virtual ProgramStateRef assumeInclusiveRange(ProgramStateRef State,
- NonLoc Value,
- const llvm::APSInt &From,
- const llvm::APSInt &To,
- bool InBound) = 0;
-
- virtual ProgramStatePair assumeInclusiveRangeDual(ProgramStateRef State,
- NonLoc Value,
- const llvm::APSInt &From,
- const llvm::APSInt &To) {
- ProgramStateRef StInRange =
- assumeInclusiveRange(State, Value, From, To, true);
-
- // If StTrue is infeasible, asserting the falseness of Cond is unnecessary
- // because the existing constraints already establish this.
- if (!StInRange)
- return ProgramStatePair((ProgramStateRef)nullptr, State);
-
- ProgramStateRef StOutOfRange =
- assumeInclusiveRange(State, Value, From, To, false);
- if (!StOutOfRange) {
- // We are careful to return the original state, /not/ StTrue,
- // because we want to avoid having callers generate a new node
- // in the ExplodedGraph.
- return ProgramStatePair(State, (ProgramStateRef)nullptr);
- }
-
- return ProgramStatePair(StInRange, StOutOfRange);
- }
+ ProgramStateRef assumeInclusiveRange(ProgramStateRef State, NonLoc Value,
+ const llvm::APSInt &From,
+ const llvm::APSInt &To, bool InBound);
+
+ /// Returns a pair of states (StInRange, StOutOfRange) where the given value
+ /// is assumed to be in the range or out of the range, respectively.
+ /// (Note that these two states might be equal if the parent state turns out
+ /// to be infeasible. This may happen if the underlying constraint solver is
+ /// not perfectly precise and this may happen very rarely.)
+ ProgramStatePair assumeInclusiveRangeDual(ProgramStateRef State, NonLoc Value,
+ const llvm::APSInt &From,
+ const llvm::APSInt &To);
/// If a symbol is perfectly constrained to a constant, attempt
/// to return the concrete value.
@@ -163,6 +146,12 @@
virtual ProgramStateRef assumeInternal(ProgramStateRef state,
DefinedSVal Cond, bool Assumption) = 0;
+ virtual ProgramStateRef assumeInclusiveRangeInternal(ProgramStateRef State,
+ NonLoc Value,
+ const llvm::APSInt &From,
+ const llvm::APSInt &To,
+ bool InBound) = 0;
+
/// canReasonAbout - Not all ConstraintManagers can accurately reason about
/// all SVal values. This method returns true if the ConstraintManager can
/// reasonably handle a given SVal value. This is typically queried by
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
