[clang] [clang][dataflow] Add `Environment::allows()`. (PR #70046)

via cfe-commits cfe-commits at lists.llvm.org
Tue Oct 24 23:33:45 PDT 2023


https://github.com/martinboehme updated https://github.com/llvm/llvm-project/pull/70046

>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 1/2] [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) {

>From 0bd3a4ec7024019d1c69059fd28ed07470afe3b7 Mon Sep 17 00:00:00 2001
From: Martin Braenne <mboehme at google.com>
Date: Wed, 25 Oct 2023 06:33:05 +0000
Subject: [PATCH 2/2] fixup! [clang][dataflow] Add `Environment::allows()`.

---
 .../clang/Analysis/FlowSensitive/DataflowAnalysisContext.h  | 6 +++---
 .../clang/Analysis/FlowSensitive/DataflowEnvironment.h      | 2 +-
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
index 3ae5ac3cf501e39..c1aa8484817a9d9 100644
--- a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
+++ b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
@@ -131,8 +131,8 @@ class DataflowAnalysisContext {
 
   /// 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.
+  /// 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
@@ -193,7 +193,7 @@ class DataflowAnalysisContext {
                                         llvm::SetVector<const Formula *> &Out);
 
   /// Returns true if the solver is able to prove that there is a satisfying
-  /// assignment for `Constraints`
+  /// assignment for `Constraints`.
   bool isSatisfiable(llvm::SetVector<const Formula *> Constraints) {
     return querySolver(std::move(Constraints)).getStatus() ==
            Solver::Result::Status::Satisfiable;
diff --git a/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h b/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
index a815a3f2d263d70..809a5dc7ba21421 100644
--- a/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
+++ b/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
@@ -557,7 +557,7 @@ class Environment {
   ///
   /// 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
+  /// 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;



More information about the cfe-commits mailing list