martong created this revision.
martong added reviewers: steakhal, NoQ.
Herald added subscribers: manas, ASDenysPetrov, gamesh411, dkrupp, donat.nagy,
Szelethus, mikhail.ramalho, a.sidorin, rnkovacs, szepet, baloghadamsoftware,
xazax.hun.
Herald added a reviewer: Szelethus.
Herald added a project: All.
martong requested review of this revision.
Herald added a project: clang.
Herald added a subscriber: cfe-commits.
This includes the refactoring of the common assumle*Dual logic into the
function template `assumeDualImpl`.
Repository:
rG LLVM Github Monorepo
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
@@ -42,12 +42,14 @@
return {};
}
+template <typename AssumeFunction>
ConstraintManager::ProgramStatePair
-ConstraintManager::assumeDual(ProgramStateRef State, DefinedSVal Cond) {
- ProgramStateRef StTrue = assumeInternal(State, Cond, true);
+ConstraintManager::assumeDualImpl(ProgramStateRef &State,
+ AssumeFunction &Assume) {
+ ProgramStateRef StTrue = Assume(true);
if (!StTrue) {
- ProgramStateRef StFalse = assumeInternal(State, Cond, false);
+ ProgramStateRef StFalse = Assume(false);
if (LLVM_UNLIKELY(!StFalse)) { // both infeasible
ProgramStateRef StInfeasible = State->cloneAsPosteriorlyOverconstrained();
assert(StInfeasible->isPosteriorlyOverconstrained());
@@ -63,7 +65,7 @@
return ProgramStatePair(nullptr, StFalse);
}
- ProgramStateRef StFalse = assumeInternal(State, Cond, false);
+ ProgramStateRef StFalse = Assume(false);
if (!StFalse) {
return ProgramStatePair(StTrue, nullptr);
}
@@ -71,8 +73,35 @@
return ProgramStatePair(StTrue, StFalse);
}
+ConstraintManager::ProgramStatePair
+ConstraintManager::assumeDual(ProgramStateRef State, DefinedSVal Cond) {
+ auto AssumeFun = [&](bool Assumption) {
+ return assumeInternal(State, Cond, Assumption);
+ };
+ return assumeDualImpl(State, AssumeFun);
+}
+
+ConstraintManager::ProgramStatePair
+ConstraintManager::assumeInclusiveRangeDual(ProgramStateRef State, NonLoc Value,
+ const llvm::APSInt &From,
+ const llvm::APSInt &To) {
+ auto AssumeFun = [&](bool Assumption) {
+ return assumeInclusiveRangeInternal(State, Value, From, To, Assumption);
+ };
+ return assumeDualImpl(State, AssumeFun);
+}
+
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
@@ -173,6 +162,10 @@
/// Returns whether or not a symbol is known to be null ("true"), known to be
/// non-null ("false"), or may be either ("underconstrained").
virtual ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym);
+
+ template <typename AssumeFunction>
+ ProgramStatePair assumeDualImpl(ProgramStateRef &State,
+ AssumeFunction &Assume);
};
std::unique_ptr<ConstraintManager>
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
