[clang][dataflow] Add Environment::allows().
#70046
Merged
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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.
llvmbot
added
clang
|
@llvm/pr-subscribers-clang-analysis @llvm/pr-subscribers-clang Author: None (martinboehme) ChangesThis allows querying whether, given the flow condition, a certain formula still This can be checked today, but only with a double negation, i.e. to check For consistency, this patch also renames Full diff: https://github.com/llvm/llvm-project/pull/70046.diff 5 Files Affected:
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) {
|
|
LGTM |
sgatev
reviewed
Oct 24, 2023
| 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 |
There was a problem hiding this comment.
Missing "if" - "Returns false the flow"
| @@ -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` | |||
There was a problem hiding this comment.
Missing dot at the end of the sentence.
| /// | ||
| /// 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 |
There was a problem hiding this comment.
Extra space at the end of `allows() `.
Xazax-hun
approved these changes
Oct 24, 2023
|
CI failures look unrelated |
sgatev
approved these changes
Oct 25, 2023
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
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 thishard to reason about, and it would be nicer to have a way of directly checking
this.
For consistency, this patch also renames
flowConditionImplies()toproves();the old name is kept around for compatibility but deprecated.