[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.

Author: martinboehme

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`

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.

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;

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 {

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) {