[clang][dataflow] Add flowConditionIsTautology function

[li.zhe.hua]

Summary

Provide a way for users to check if a flow condition is
unconditionally true.

[ymandel]

The code looks good, but what is the intended application?

[li.zhe.hua]

This allows me to query when an expression is always encountered/executed. Alternatively, if I have a set of interesting expressions, I can note the flow condition at every expression, compute the disjunction of the set of flow conditions, and determine if execution will always encounter an interesting expression.

[xazax.hun]

The code looks good to me too. I was also wondering what sort of check will need this info.

[sgatev]

clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h

176–177

clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp

144

151

I don't think this is doing what the comment above it says. We probably shouldn't add flow conditions directly as constraints because this isn't tracking flow condition dependencies. I suggest removing this case and keeping the one with FC5.

154

Again, I suggest removing this case. The one with FC6 should suffice.

[li.zhe.hua]

I'm playing around with a tool to take raw pointers and add a non-null annotation or convert them to references, for code that is assumed to be correct. So in this case, "interesting expression" is anything that would be UB if the pointer was null, e.g. dereferencing the pointer.

[li.zhe.hua]

Address reviewer comments.

[li.zhe.hua]

Ah, good catch regarding the flow condition deps not being tracked. Thanks for the review!

clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h

public:
   /// token.
   AtomicBoolValue &joinFlowConditions(AtomicBoolValue &FirstToken,
                                       AtomicBoolValue &SecondToken);
 
   /// Returns true if and only if the constraints of the flow condition
   /// identified by `Token` imply that `Val` is true.
   bool flowConditionImplies(AtomicBoolValue &Token, BoolValue &Val);
 
+  /// Returns true if and only if the constraints of the flow condition
+  /// identified by `Token` are always true.
+  bool flowConditionIsTautology(AtomicBoolValue &Token);
+
 private:
   /// Adds all constraints of the flow condition identified by `Token` and all
   /// of its transitive dependencies to `Constraints`. `VisitedTokens` is used
   /// to track tokens of flow conditions that were already visited by recursive
   /// calls.
   void addTransitiveFlowConditionConstraints(
       AtomicBoolValue &Token, llvm::DenseSet<BoolValue *> &Constraints,
       llvm::DenseSet<AtomicBoolValue *> &VisitedTokens) const;

clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp

llvm::DenseSet<BoolValue *> Constraints = {
       &getOrCreateNegationValue(getBoolLiteralValue(false)),
       &getOrCreateNegationValue(Val),
   };
   llvm::DenseSet<AtomicBoolValue *> VisitedTokens;
   addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens);
   return S->solve(std::move(Constraints)) == Solver::Result::Unsatisfiable;
 }
 
+bool DataflowAnalysisContext::flowConditionIsTautology(AtomicBoolValue &Token) {
+  // Returns true if and only if we cannot prove that the flow condition can
+  // ever be false.
+  llvm::DenseSet<BoolValue *> Constraints = {
+      &getBoolLiteralValue(true),
+      &getOrCreateNegationValue(getBoolLiteralValue(false)),
+      &getOrCreateNegationValue(Token),
+  };
+  llvm::DenseSet<AtomicBoolValue *> VisitedTokens;
+  addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens);
+  return S->solve(std::move(Constraints)) == Solver::Result::Unsatisfiable;
+}
+
 void DataflowAnalysisContext::addTransitiveFlowConditionConstraints(
     AtomicBoolValue &Token, llvm::DenseSet<BoolValue *> &Constraints,
     llvm::DenseSet<AtomicBoolValue *> &VisitedTokens) const {
   auto Res = VisitedTokens.insert(&Token);
   if (!Res.second)
     return;
 
   auto FirstConjunctIT = FlowConditionFirstConjuncts.find(&Token);

clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp

TEST_F(DataflowAnalysisContextTest, JoinFlowConditions) {
   Context.addFlowConditionConstraint(FC2, C3);
 
   auto &FC3 = Context.joinFlowConditions(FC1, FC2);
   EXPECT_FALSE(Context.flowConditionImplies(FC3, C1));
   EXPECT_FALSE(Context.flowConditionImplies(FC3, C2));
   EXPECT_TRUE(Context.flowConditionImplies(FC3, C3));
 }
 
+TEST_F(DataflowAnalysisContextTest, FlowConditionTautologies) {
+  // Fresh flow condition with empty/no constraints is always true.
+  auto &FC1 = Context.makeFlowConditionToken();
+  EXPECT_TRUE(Context.flowConditionIsTautology(FC1));
+
+  // Literal `true` is always true.
+  auto &FC2 = Context.makeFlowConditionToken();
+  Context.addFlowConditionConstraint(FC2, Context.getBoolLiteralValue(true));
+  EXPECT_TRUE(Context.flowConditionIsTautology(FC2));
+
+  // Literal `false` is never true.
+  auto &FC3 = Context.makeFlowConditionToken();
+  Context.addFlowConditionConstraint(FC3, Context.getBoolLiteralValue(false));
+  EXPECT_FALSE(Context.flowConditionIsTautology(FC3));
+
+  // We can't prove that an arbitrary bool A is always true...
+  auto &C1 = Context.createAtomicBoolValue();
+  auto &FC4 = Context.makeFlowConditionToken();
+  Context.addFlowConditionConstraint(FC4, C1);
+  EXPECT_FALSE(Context.flowConditionIsTautology(FC4));
+
+  // ... but we can prove A || !A is true.
+  auto &FC5 = Context.makeFlowConditionToken();
+  Context.addFlowConditionConstraint(
+      FC5, Context.getOrCreateDisjunctionValue(
+               C1, Context.getOrCreateNegationValue(C1)));
+  EXPECT_TRUE(Context.flowConditionIsTautology(FC5));
+}
+
 } // namespace