[clang] d1f5954 - [clang][dataflow] Add `Environment::allows()`. (#70046)
via cfe-commits
cfe-commits at lists.llvm.org
Wed Oct 25 07:02:26 PDT 2023
Author: martinboehme
Date: 2023-10-25T16:02:22+02:00
New Revision: d1f59544cf31488d84a2daff0020af2f8e366ed8
URL: https://github.com/llvm/llvm-project/commit/d1f59544cf31488d84a2daff0020af2f8e366ed8
DIFF: https://github.com/llvm/llvm-project/commit/d1f59544cf31488d84a2daff0020af2f8e366ed8.diff
LOG: [clang][dataflow] Add `Environment::allows()`. (#70046)
This allows querying whether, given the flow condition, a certain
formula still
has a solution (though it is not necessarily implied by the flow
condition, as
`flowConditionImplies()` would check).
This can be checked today, but only with a double negation, i.e. to
check
whether, given the flow condition, a formula F has a solution, you can
check
`!Env.flowConditionImplies(Arena.makeNot(F))`. The double negation makes
this
hard to reason about, and it would be nicer to have a way of directly
checking
this.
For consistency, this patch also renames `flowConditionImplies()` to
`proves()`;
the old name is kept around for compatibility but deprecated.
Added:
Modified:
clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
clang/unittests/Analysis/FlowSensitive/DataflowEnvironmentTest.cpp
Removed:
################################################################################
diff --git a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
index a792c3f911b1dd0..c1aa8484817a9d9 100644
--- a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
+++ b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
@@ -129,9 +129,17 @@ class DataflowAnalysisContext {
/// token.
Atom joinFlowConditions(Atom FirstToken, Atom SecondToken);
- /// Returns true if and only if the constraints of the flow condition
- /// identified by `Token` imply that `Val` is true.
- bool flowConditionImplies(Atom Token, const Formula &);
+ /// Returns true if the constraints of the flow condition identified by
+ /// `Token` imply that `F` is true.
+ /// Returns false if the flow condition does not imply `F` or if the solver
+ /// times out.
+ bool flowConditionImplies(Atom Token, const Formula &F);
+
+ /// Returns true if the constraints of the flow condition identified by
+ /// `Token` still allow `F` to be true.
+ /// Returns false if the flow condition implies that `F` is false or if the
+ /// solver times out.
+ bool flowConditionAllows(Atom Token, const Formula &F);
/// Returns true if `Val1` is equivalent to `Val2`.
/// Note: This function doesn't take into account constraints on `Val1` and
@@ -184,6 +192,12 @@ class DataflowAnalysisContext {
addTransitiveFlowConditionConstraints(Atom Token,
llvm::SetVector<const Formula *> &Out);
+ /// Returns true if the solver is able to prove that there is a satisfying
+ /// assignment for `Constraints`.
+ bool isSatisfiable(llvm::SetVector<const Formula *> Constraints) {
+ return querySolver(std::move(Constraints)).getStatus() ==
+ Solver::Result::Status::Satisfiable;
+ }
/// Returns true if the solver is able to prove that there is no satisfying
/// assignment for `Constraints`
diff --git a/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h b/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
index 33e9f0fba02bc77..963197b728f4273 100644
--- a/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
+++ b/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
@@ -542,12 +542,29 @@ class Environment {
Atom getFlowConditionToken() const { return FlowConditionToken; }
/// Record a fact that must be true if this point in the program is reached.
- void addToFlowCondition(const Formula &);
+ void assume(const Formula &);
+
+ /// Deprecated synonym for `assume()`.
+ void addToFlowCondition(const Formula &F) { assume(F); }
/// Returns true if the formula is always true when this point is reached.
- /// Returns false if the formula may be false, or if the flow condition isn't
- /// sufficiently precise to prove that it is true.
- bool flowConditionImplies(const Formula &) const;
+ /// Returns false if the formula may be false (or the flow condition isn't
+ /// sufficiently precise to prove that it is true) or if the solver times out.
+ ///
+ /// Note that there is an asymmetry between this function and `allows()` in
+ /// that they both return false if the solver times out. The assumption is
+ /// that if `proves()` or `allows()` returns true, this will result in a
+ /// diagnostic, and we want to bias towards false negatives in the case where
+ /// the solver times out.
+ bool proves(const Formula &) const;
+
+ /// Returns true if the formula may be true when this point is reached.
+ /// Returns false if the formula is always false when this point is reached
+ /// (or the flow condition is overly constraining) or if the solver times out.
+ bool allows(const Formula &) const;
+
+ /// Deprecated synonym for `proves()`.
+ bool flowConditionImplies(const Formula &F) const { return proves(F); }
/// Returns the `DeclContext` of the block being analysed, if any. Otherwise,
/// returns null.
diff --git a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
index 6a1feb229d47b61..40de6cdf3a69e28 100644
--- a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
+++ b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
@@ -145,19 +145,28 @@ Solver::Result DataflowAnalysisContext::querySolver(
}
bool DataflowAnalysisContext::flowConditionImplies(Atom Token,
- const Formula &Val) {
+ const Formula &F) {
// Returns true if and only if truth assignment of the flow condition implies
- // that `Val` is also true. We prove whether or not this property holds by
+ // that `F` is also true. We prove whether or not this property holds by
// reducing the problem to satisfiability checking. In other words, we attempt
- // to show that assuming `Val` is false makes the constraints induced by the
+ // to show that assuming `F` is false makes the constraints induced by the
// flow condition unsatisfiable.
llvm::SetVector<const Formula *> Constraints;
Constraints.insert(&arena().makeAtomRef(Token));
- Constraints.insert(&arena().makeNot(Val));
+ Constraints.insert(&arena().makeNot(F));
addTransitiveFlowConditionConstraints(Token, Constraints);
return isUnsatisfiable(std::move(Constraints));
}
+bool DataflowAnalysisContext::flowConditionAllows(Atom Token,
+ const Formula &F) {
+ llvm::SetVector<const Formula *> Constraints;
+ Constraints.insert(&arena().makeAtomRef(Token));
+ Constraints.insert(&F);
+ addTransitiveFlowConditionConstraints(Token, Constraints);
+ return isSatisfiable(std::move(Constraints));
+}
+
bool DataflowAnalysisContext::equivalentFormulas(const Formula &Val1,
const Formula &Val2) {
llvm::SetVector<const Formula *> Constraints;
diff --git a/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp b/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
index 00e56ce51c530b3..cf1e9eb7b1fd7f2 100644
--- a/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
+++ b/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
@@ -929,12 +929,16 @@ StorageLocation &Environment::createObjectInternal(const ValueDecl *D,
return Loc;
}
-void Environment::addToFlowCondition(const Formula &Val) {
- DACtx->addFlowConditionConstraint(FlowConditionToken, Val);
+void Environment::assume(const Formula &F) {
+ DACtx->addFlowConditionConstraint(FlowConditionToken, F);
}
-bool Environment::flowConditionImplies(const Formula &Val) const {
- return DACtx->flowConditionImplies(FlowConditionToken, Val);
+bool Environment::proves(const Formula &F) const {
+ return DACtx->flowConditionImplies(FlowConditionToken, F);
+}
+
+bool Environment::allows(const Formula &F) const {
+ return DACtx->flowConditionAllows(FlowConditionToken, F);
}
void Environment::dump(raw_ostream &OS) const {
diff --git a/clang/unittests/Analysis/FlowSensitive/DataflowEnvironmentTest.cpp b/clang/unittests/Analysis/FlowSensitive/DataflowEnvironmentTest.cpp
index ad40c0b082d302e..751e86770d5e6dc 100644
--- a/clang/unittests/Analysis/FlowSensitive/DataflowEnvironmentTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/DataflowEnvironmentTest.cpp
@@ -39,17 +39,22 @@ TEST_F(EnvironmentTest, FlowCondition) {
Environment Env(DAContext);
auto &A = Env.arena();
- EXPECT_TRUE(Env.flowConditionImplies(A.makeLiteral(true)));
- EXPECT_FALSE(Env.flowConditionImplies(A.makeLiteral(false)));
+ EXPECT_TRUE(Env.proves(A.makeLiteral(true)));
+ EXPECT_TRUE(Env.allows(A.makeLiteral(true)));
+ EXPECT_FALSE(Env.proves(A.makeLiteral(false)));
+ EXPECT_FALSE(Env.allows(A.makeLiteral(false)));
auto &X = A.makeAtomRef(A.makeAtom());
- EXPECT_FALSE(Env.flowConditionImplies(X));
+ EXPECT_FALSE(Env.proves(X));
+ EXPECT_TRUE(Env.allows(X));
- Env.addToFlowCondition(X);
- EXPECT_TRUE(Env.flowConditionImplies(X));
+ Env.assume(X);
+ EXPECT_TRUE(Env.proves(X));
+ EXPECT_TRUE(Env.allows(X));
auto &NotX = A.makeNot(X);
- EXPECT_FALSE(Env.flowConditionImplies(NotX));
+ EXPECT_FALSE(Env.proves(NotX));
+ EXPECT_FALSE(Env.allows(NotX));
}
TEST_F(EnvironmentTest, CreateValueRecursiveType) {
More information about the cfe-commits
mailing list