[clang] [clang][dataflow] Add `Environment::allows()`. (PR #70046)
via cfe-commits
cfe-commits at lists.llvm.org
Tue Oct 24 07:14:20 PDT 2023
https://github.com/martinboehme created https://github.com/llvm/llvm-project/pull/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.
>From 8d1119c97581fe5bf9d44330ce2a58b2be18e8b7 Mon Sep 17 00:00:00 2001
From: Martin Braenne <mboehme at google.com>
Date: Tue, 24 Oct 2023 14:13:44 +0000
Subject: [PATCH] [clang][dataflow] Add `Environment::allows()`.
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.
---
.../FlowSensitive/DataflowAnalysisContext.h | 20 ++++++++++++---
.../FlowSensitive/DataflowEnvironment.h | 25 ++++++++++++++++---
.../FlowSensitive/DataflowAnalysisContext.cpp | 17 ++++++++++---
.../FlowSensitive/DataflowEnvironment.cpp | 12 ++++++---
.../FlowSensitive/DataflowEnvironmentTest.cpp | 17 ++++++++-----
5 files changed, 70 insertions(+), 21 deletions(-)
diff --git a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
index a792c3f911b1dd0..3ae5ac3cf501e39 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 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 9ac2cb90ccc4d4a..a815a3f2d263d70 100644
--- a/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
+++ b/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
@@ -546,12 +546,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 01c6cc69e2b9fac..461dce5c98cd363 100644
--- a/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
+++ b/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
@@ -947,12 +947,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