[clang][dataflow] Implement functionality for flow condition variable substitution.

[wyt]

Summary

This patch introduces buildAndSubstituteFlowCondition - given a flow condition token, this function returns the expression of constraints defining the flow condition, with values substituted where specified.

As an example:
Say we have tokens FC1, FC2, FC3:

FlowConditionConstraints: {
 FC1: C1,
 FC2: C2,
 FC3: (FC1 v FC2) ^ C3,
}

buildAndSubstituteFlowCondition(FC3, /*Substitutions:*/{{C1 -> C1'}})
returns a value corresponding to (C1' v C2) ^ C3.

Note:
This function returns the flow condition expressed directly as its constraints, which differs to how we currently represent the flow condition as a token bound to a set of constraints and dependencies. Making the representation consistent may be an option to consider in the future.

Depends On D128357

[gribozavr2]

clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp

174

Could you refactor it into a free function? It does not use 'this', seems like.

236–240

It is better to put special cases (early returns) first.

clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp

235

Could you do the following: build explicitly a BoolValue that represents the expected result formula, and then ask the SAT solver to prove equivalence between the two? That would be a stronger test than merely checking one implication.

Same in the test below.

[xazax.hun]

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

209

Could you elaborate on why do we need this? Why do we care about how flow condition constraints are represented? We should use the solver to ask questions and as far as I understand the solver should work with both representations. Also this function feels like doing two things, building the flow condition from the tokens and doing substitutions. Any reason why those two are not separate functions? Is this for performance reasons?

[wyt]

Address comments - improve test clarity by comparing substituted flow condition with an expected value using equivalentBoolValues utility.

[wyt]

@xazax.hun

Could you elaborate on why do we need this?

We are currently working on a pointer nullability analysis here: https://github.com/google/crubit/tree/main/nullability_verification.
One of the things we are trying to do is to check if the flow condition is independent of a variable, done by checking if the formula regardless if the variable is substituted to true or false - requiring buildAndSubstituteFlowCondition.

Why do we care about how flow condition constraints are represented? We should use the solver to ask questions and as far as I understand the solver should work with both representations.

The first approach of representing flow conditions as an atomic boolean token, places the responsibility on the user to handle adding the constraints of the flow condition when checking with the solver.
The second approach of representing flow conditions as a direct conjunction of its constraints, has performance implications as any boolean values with the flow condition appearing in it may grow in size, and the entire conjunction of the flow condition has to be added repeatedly if the flow condition appears in multiple places.

Also this function feels like doing two things, building the flow condition from the tokens and doing substitutions. Any reason why those two are not separate functions? Is this for performance reasons?

You'd build the flow condition by passing in an empty substitutions set. Also, just building the flow condition does not see any use currently.

clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp

188

@gribozavr2

Could you refactor it into a free function? It does not use 'this', seems like.

We store and retrieve BoolVals in DataflowAnalysisContext. Example as highlighted.

[xazax.hun]

clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp

219

I think DenseMap has a constructor that accepts two iterators.

235–238

Should we move this check to the beginning to save work?

[wyt]

Address comments.

[gribozavr2]

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

209

Could you copy the example from the commit description into the doc comment?

clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp

319

Could you also add a test for negations?

[wyt]

Address comments - add example to buildAndSubstituteFlowCondition doc comment, add tests for atomic and negated flow condition.

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

public:
   AtomicBoolValue &forkFlowCondition(AtomicBoolValue &Token);
 
   /// Creates a new flow condition that represents the disjunction of the flow
   /// conditions identified by `FirstToken` and `SecondToken`, and returns its
   /// token.
   AtomicBoolValue &joinFlowConditions(AtomicBoolValue &FirstToken,
                                       AtomicBoolValue &SecondToken);
 
+  // FIXME: This function returns the flow condition expressed directly as its
+  // constraints: (C1 AND C2 AND ...). This differs from the general approach in
+  // the framework where a flow condition is represented as a token (an atomic
+  // boolean) with dependencies and constraints tracked in `FlowConditionDeps`
+  // and `FlowConditionConstraints`: (FC <=> C1 AND C2 AND ...).
+  // Consider if we should make the representation of flow condition consistent,
+  // returning an atomic boolean token with separate constraints instead.
+  //
+  /// Builds and returns the logical formula defining the flow condition
+  /// identified by `Token`. If a value in the formula is present as a key in
+  /// `Substitutions`, it will be substituted with the value it maps to.
+  BoolValue &buildAndSubstituteFlowCondition(
+      AtomicBoolValue &Token,
+      llvm::DenseMap<AtomicBoolValue *, BoolValue *> Substitutions);
+
   /// 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:
   Solver::Result querySolver(llvm::DenseSet<BoolValue *> Constraints);
 
   /// Returns true if the solver is able to prove that there is no satisfying
   /// assignment for `Constraints`
   bool checkUnsatisfiable(llvm::DenseSet<BoolValue *> Constraints) {
     return querySolver(std::move(Constraints)) == Solver::Result::Unsatisfiable;
   }
 
+  /// Returns a boolean value as a result of substituting `Val` and its sub
+  /// values based on entries in `SubstitutionsCache`. Intermediate results are
+  /// stored in `SubstitutionsCache` to avoid reprocessing values that have
+  /// already been visited.
+  BoolValue &substituteBoolValue(
+      BoolValue &Val,
+      llvm::DenseMap<BoolValue *, BoolValue *> &SubstitutionsCache);
+
+  /// Builds and returns the logical formula defining the flow condition
+  /// identified by `Token`, sub values may be substituted based on entries in
+  /// `SubstitutionsCache`. Intermediate results are stored in
+  /// `SubstitutionsCache` to avoid reprocessing values that have already been
+  /// visited.
+  BoolValue &buildAndSubstituteFlowConditionWithCache(
+      AtomicBoolValue &Token,
+      llvm::DenseMap<BoolValue *, BoolValue *> &SubstitutionsCache);
+
   std::unique_ptr<Solver> S;
 
   // Storage for the state of a program.
   std::vector<std::unique_ptr<StorageLocation>> Locs;
   std::vector<std::unique_ptr<Value>> Vals;
 
   // Maps from program declarations and statements to storage locations that are
   // assigned to them. These assignments are global (aggregated across all basic

clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp

void DataflowAnalysisContext::addTransitiveFlowConditionConstraints(
   if (DepsIT != FlowConditionDeps.end()) {
     for (AtomicBoolValue *DepToken : DepsIT->second) {
       addTransitiveFlowConditionConstraints(*DepToken, Constraints,
                                             VisitedTokens);
     }
   }
 }
 
+BoolValue &DataflowAnalysisContext::substituteBoolValue(
+    BoolValue &Val,
+    llvm::DenseMap<BoolValue *, BoolValue *> &SubstitutionsCache) {
+  auto IT = SubstitutionsCache.find(&Val);
+  if (IT != SubstitutionsCache.end()) {
+    return *IT->second;
+  }
+  BoolValue *Result;
+  switch (Val.getKind()) {
+  case Value::Kind::AtomicBool: {
+    Result = &Val;
+    break;
+  }
+  case Value::Kind::Negation: {
+    auto &Negation = *cast<NegationValue>(&Val);
+    auto &Sub = substituteBoolValue(Negation.getSubVal(), SubstitutionsCache);
+    Result = &getOrCreateNegation(Sub);
+    break;
+  }
+  case Value::Kind::Disjunction: {
+    auto &Disjunct = *cast<DisjunctionValue>(&Val);
+    auto &LeftSub =
+        substituteBoolValue(Disjunct.getLeftSubValue(), SubstitutionsCache);
+    auto &RightSub =
+        substituteBoolValue(Disjunct.getRightSubValue(), SubstitutionsCache);
+    Result = &getOrCreateDisjunction(LeftSub, RightSub);
+    break;
+  }
+  case Value::Kind::Conjunction: {
+    auto &Conjunct = *cast<ConjunctionValue>(&Val);
+    auto &LeftSub =
+        substituteBoolValue(Conjunct.getLeftSubValue(), SubstitutionsCache);
+    auto &RightSub =
+        substituteBoolValue(Conjunct.getRightSubValue(), SubstitutionsCache);
+    Result = &getOrCreateConjunction(LeftSub, RightSub);
+    break;
+  }
+  default:
+    llvm_unreachable("Unhandled Value Kind");
+  }
+  SubstitutionsCache[&Val] = Result;
+  return *Result;
+}
+
+BoolValue &DataflowAnalysisContext::buildAndSubstituteFlowCondition(
+    AtomicBoolValue &Token,
+    llvm::DenseMap<AtomicBoolValue *, BoolValue *> Substitutions) {
+  llvm::DenseMap<BoolValue *, BoolValue *> SubstitutionsCache(
+      Substitutions.begin(), Substitutions.end());
+  return buildAndSubstituteFlowConditionWithCache(Token, SubstitutionsCache);
+}
+
+BoolValue &DataflowAnalysisContext::buildAndSubstituteFlowConditionWithCache(
+    AtomicBoolValue &Token,
+    llvm::DenseMap<BoolValue *, BoolValue *> &SubstitutionsCache) {
+  auto ConstraintsIT = FlowConditionConstraints.find(&Token);
+  if (ConstraintsIT == FlowConditionConstraints.end()) {
+    return getBoolLiteralValue(true);
+  }
+  auto DepsIT = FlowConditionDeps.find(&Token);
+  if (DepsIT != FlowConditionDeps.end()) {
+    for (AtomicBoolValue *DepToken : DepsIT->second) {
+      auto &NewDep = buildAndSubstituteFlowConditionWithCache(
+          *DepToken, SubstitutionsCache);
+      SubstitutionsCache[DepToken] = &NewDep;
+    }
+  }
+  return substituteBoolValue(*ConstraintsIT->second, SubstitutionsCache);
+}
+
 } // namespace dataflow
 } // namespace clang
 
 using namespace clang;
 
 const Expr &clang::dataflow::ignoreCFGOmittedNodes(const Expr &E) {
   const Expr *Current = &E;
   if (auto *EWC = dyn_cast<ExprWithCleanups>(Current)) {

clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp

TEST_F(DataflowAnalysisContextTest, EquivBoolVals) {
 
   // !X != X
   EXPECT_FALSE(Context.equivalentBoolValues(Context.getOrCreateNegation(X), X));
   // !(!X) = X
   EXPECT_TRUE(Context.equivalentBoolValues(
       Context.getOrCreateNegation(Context.getOrCreateNegation(X)), X));
 
   // (X || X) == X
   EXPECT_TRUE(
       Context.equivalentBoolValues(Context.getOrCreateDisjunction(X, X), X));
   // (X || Y) != X
   EXPECT_FALSE(
       Context.equivalentBoolValues(Context.getOrCreateDisjunction(X, Y), X));
   // (X || True) == True
   EXPECT_TRUE(Context.equivalentBoolValues(
       Context.getOrCreateDisjunction(X, True), True));
   // (X || False) == X
EXPECT_TRUE(Context.equivalentBoolValues(
       Context.getOrCreateDisjunction(Context.getOrCreateDisjunction(X, Y), Z),
       Context.getOrCreateDisjunction(X, Context.getOrCreateDisjunction(Y, Z))));
   // ((X && Y) && Z) == (X && (Y && Z))
   EXPECT_TRUE(Context.equivalentBoolValues(
       Context.getOrCreateConjunction(Context.getOrCreateConjunction(X, Y), Z),
       Context.getOrCreateConjunction(X, Context.getOrCreateConjunction(Y, Z))));
 }
 
+TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsDisjunctiveFC) {
+  auto &X = Context.createAtomicBoolValue();
+  auto &Y = Context.createAtomicBoolValue();
+  auto &True = Context.getBoolLiteralValue(true);
+  auto &False = Context.getBoolLiteralValue(false);
+
+  // FC = X || Y
+  auto &FC = Context.makeFlowConditionToken();
+  Context.addFlowConditionConstraint(FC, Context.getOrCreateDisjunction(X, Y));
+
+  // If X is true in FC, FC = X || Y must be true
+  auto &FCWithXTrue =
+      Context.buildAndSubstituteFlowCondition(FC, {{&X, &True}});
+  EXPECT_TRUE(Context.equivalentBoolValues(FCWithXTrue, True));
+
+  // If X is false in FC, FC = X || Y is equivalent to evaluating Y
+  auto &FC1WithXFalse =
+      Context.buildAndSubstituteFlowCondition(FC, {{&X, &False}});
+  EXPECT_TRUE(Context.equivalentBoolValues(FC1WithXFalse, Y));
+}
+
+TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsConjunctiveFC) {
+  auto &X = Context.createAtomicBoolValue();
+  auto &Y = Context.createAtomicBoolValue();
+  auto &True = Context.getBoolLiteralValue(true);
+  auto &False = Context.getBoolLiteralValue(false);
+
+  // FC = X && Y
+  auto &FC = Context.makeFlowConditionToken();
+  Context.addFlowConditionConstraint(FC, Context.getOrCreateConjunction(X, Y));
+
+  // If X is true in FC, FC = X && Y is equivalent to evaluating Y
+  auto &FCWithXTrue =
+      Context.buildAndSubstituteFlowCondition(FC, {{&X, &True}});
+  EXPECT_TRUE(Context.equivalentBoolValues(FCWithXTrue, Y));
+
+  // If X is false in FC, FC = X && Y must be false
+  auto &FCWithXFalse =
+      Context.buildAndSubstituteFlowCondition(FC, {{&X, &False}});
+  EXPECT_TRUE(Context.equivalentBoolValues(FCWithXFalse, False));
+}
+
+TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsForkedFC) {
+  auto &X = Context.createAtomicBoolValue();
+  auto &Y = Context.createAtomicBoolValue();
+  auto &Z = Context.createAtomicBoolValue();
+  auto &True = Context.getBoolLiteralValue(true);
+  auto &False = Context.getBoolLiteralValue(false);
+
+  // FC = X && Y
+  auto &FC = Context.makeFlowConditionToken();
+  Context.addFlowConditionConstraint(FC, Context.getOrCreateConjunction(X, Y));
+  // ForkedFC = FC && Z = X && Y && Z
+  auto &ForkedFC = Context.forkFlowCondition(FC);
+  Context.addFlowConditionConstraint(ForkedFC, Z);
+
+  // If any of X,Y,Z is true in ForkedFC, ForkedFC = X && Y && Z is equivalent
+  // to evaluating the conjunction of the remaining values
+  auto &ForkedFCWithZTrue =
+      Context.buildAndSubstituteFlowCondition(ForkedFC, {{&Z, &True}});
+  EXPECT_TRUE(Context.equivalentBoolValues(
+      ForkedFCWithZTrue, Context.getOrCreateConjunction(X, Y)));
+  auto &ForkedFCWithYAndZTrue = Context.buildAndSubstituteFlowCondition(
+      ForkedFC, {{&Y, &True}, {&Z, &True}});
+  EXPECT_TRUE(Context.equivalentBoolValues(ForkedFCWithYAndZTrue, X));
+
+  // If any of X,Y,Z is false in ForkedFC, ForkedFC = X && Y && Z must be false
+  auto &ForkedFCWithXFalse =
+      Context.buildAndSubstituteFlowCondition(ForkedFC, {{&X, &False}});
+  auto &ForkedFCWithYFalse =
+      Context.buildAndSubstituteFlowCondition(ForkedFC, {{&Y, &False}});
+  auto &ForkedFCWithZFalse =
+      Context.buildAndSubstituteFlowCondition(ForkedFC, {{&Z, &False}});
+  EXPECT_TRUE(Context.equivalentBoolValues(ForkedFCWithXFalse, False));
+  EXPECT_TRUE(Context.equivalentBoolValues(ForkedFCWithYFalse, False));
+  EXPECT_TRUE(Context.equivalentBoolValues(ForkedFCWithZFalse, False));
+}
+
+TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsJoinedFC) {
+  auto &X = Context.createAtomicBoolValue();
+  auto &Y = Context.createAtomicBoolValue();
+  auto &Z = Context.createAtomicBoolValue();
+  auto &True = Context.getBoolLiteralValue(true);
+  auto &False = Context.getBoolLiteralValue(false);
+
+  // FC1 = X
+  auto &FC1 = Context.makeFlowConditionToken();
+  Context.addFlowConditionConstraint(FC1, X);
+  // FC2 = Y
+  auto &FC2 = Context.makeFlowConditionToken();
+  Context.addFlowConditionConstraint(FC2, Y);
+  // JoinedFC = (FC1 || FC2) && Z = (X || Y) && Z
+  auto &JoinedFC = Context.joinFlowConditions(FC1, FC2);
+  Context.addFlowConditionConstraint(JoinedFC, Z);
+
+  // If any of X, Y is true in JoinedFC, JoinedFC = (X || Y) && Z is equivalent
+  // to evaluating the remaining Z
+  auto &JoinedFCWithXTrue =
+      Context.buildAndSubstituteFlowCondition(JoinedFC, {{&X, &True}});
+  auto &JoinedFCWithYTrue =
+      Context.buildAndSubstituteFlowCondition(JoinedFC, {{&Y, &True}});
+  EXPECT_TRUE(Context.equivalentBoolValues(JoinedFCWithXTrue, Z));
+  EXPECT_TRUE(Context.equivalentBoolValues(JoinedFCWithYTrue, Z));
+
+  // If Z is true in JoinedFC, JoinedFC = (X || Y) && Z is equivalent to
+  // evaluating the remaining disjunction (X || Y)
+  auto &JoinedFCWithZTrue =
+      Context.buildAndSubstituteFlowCondition(JoinedFC, {{&Z, &True}});
+  EXPECT_TRUE(Context.equivalentBoolValues(
+      JoinedFCWithZTrue, Context.getOrCreateDisjunction(X, Y)));
+
+  // If any of X, Y is false in JoinedFC, JoinedFC = (X || Y) && Z is equivalent
+  // to evaluating the conjunction of the other value and Z
+  auto &JoinedFCWithXFalse =
+      Context.buildAndSubstituteFlowCondition(JoinedFC, {{&X, &False}});
+  auto &JoinedFCWithYFalse =
+      Context.buildAndSubstituteFlowCondition(JoinedFC, {{&Y, &False}});
+  EXPECT_TRUE(Context.equivalentBoolValues(
+      JoinedFCWithXFalse, Context.getOrCreateConjunction(Y, Z)));
+  EXPECT_TRUE(Context.equivalentBoolValues(
+      JoinedFCWithYFalse, Context.getOrCreateConjunction(X, Z)));
+
+  // If Z is false in JoinedFC, JoinedFC = (X || Y) && Z must be false
+  auto &JoinedFCWithZFalse =
+      Context.buildAndSubstituteFlowCondition(JoinedFC, {{&Z, &False}});
+  EXPECT_TRUE(Context.equivalentBoolValues(JoinedFCWithZFalse, False));
+}
+
 } // namespace