[clang][dataflow] Store flow condition constraints in a single `FlowConditionConstraints` map.

[wyt]

Summary

A flow condition is represented with an atomic boolean token, and it is bound to a set of constraints: (FC <=> C1 ^ C2 ^ ...). \
This was internally represented as (FC v !C1 v !C2 v ...) ^ (C1 v !FC) ^ (C2 v !FC) ^ ... and tracked by 2 maps:

• FlowConditionFirstConjunct stores the first conjunct (FC v !C1 v !C2 v ...)
• FlowConditionRemainingConjuncts stores the remaining conjuncts (C1 v !FC) ^ (C2 v !FC) ^ ...

This patch simplifies the tracking of the constraints by using a single FlowConditionConstraints map which stores (C1 ^ C2 ^ ...), eliminating the use of two maps.

[sgatev]

clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp

138–150

142–144

[xazax.hun]

I found a small nit inline, otherwise looks good.

clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp

76

Do you actually need a second lookup? Couldn't you use Res.first to update the corresponding value?

[wyt]

Address comments.

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

 
 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;
+      llvm::DenseSet<AtomicBoolValue *> &VisitedTokens);
 
   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
llvm::DenseMap<std::pair<BoolValue *, BoolValue *>, DisjunctionValue *>
       DisjunctionVals;
   llvm::DenseMap<BoolValue *, NegationValue *> NegationVals;
 
   // Flow conditions are tracked symbolically: each unique flow condition is
   // associated with a fresh symbolic variable (token), bound to the clause that
   // defines the flow condition. Conceptually, each binding corresponds to an
   // "iff" of the form `FC <=> (C1 ^ C2 ^ ...)` where `FC` is a flow condition
   // token (an atomic boolean) and `Ci`s are the set of constraints in the flow
-  // flow condition clause. Internally, we do not record the formula directly as
-  // an "iff". Instead, a flow condition clause is encoded as conjuncts of the
-  // form `(FC v !C1 v !C2 v ...) ^ (C1 v !FC) ^ (C2 v !FC) ^ ...`. The first
-  // conjuct is stored in the `FlowConditionFirstConjuncts` map and the set of
-  // remaining conjuncts are stored in the `FlowConditionRemainingConjuncts`
-  // map, both keyed by the token of the flow condition.
+  // flow condition clause. The set of constraints (C1 ^ C2 ^ ...) are stored in
+  // the `FlowConditionConstraints` map, keyed by the token of the flow
+  // condition.
   //
   // Flow conditions depend on other flow conditions if they are created using
   // `forkFlowCondition` or `joinFlowConditions`. The graph of flow condition
   // dependencies is stored in the `FlowConditionDeps` map.
   llvm::DenseMap<AtomicBoolValue *, llvm::DenseSet<AtomicBoolValue *>>
       FlowConditionDeps;
-  llvm::DenseMap<AtomicBoolValue *, BoolValue *> FlowConditionFirstConjuncts;
-  llvm::DenseMap<AtomicBoolValue *, llvm::DenseSet<BoolValue *>>
-      FlowConditionRemainingConjuncts;
+  llvm::DenseMap<AtomicBoolValue *, BoolValue *> FlowConditionConstraints;
 };
 
 } // namespace dataflow
 } // namespace clang
 
 #endif // LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_DATAFLOWANALYSISCONTEXT_H

clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp

 BoolValue &DataflowAnalysisContext::getOrCreateNegationValue(BoolValue &Val) {
   auto Res = NegationVals.try_emplace(&Val, nullptr);
   if (Res.second)
     Res.first->second = &takeOwnership(std::make_unique<NegationValue>(Val));
   return *Res.first->second;
 }
 
 AtomicBoolValue &DataflowAnalysisContext::makeFlowConditionToken() {
-  AtomicBoolValue &Token = createAtomicBoolValue();
-  FlowConditionRemainingConjuncts[&Token] = {};
-  FlowConditionFirstConjuncts[&Token] = &Token;
-  return Token;
+  return createAtomicBoolValue();
 }
 
 void DataflowAnalysisContext::addFlowConditionConstraint(
     AtomicBoolValue &Token, BoolValue &Constraint) {
-  FlowConditionRemainingConjuncts[&Token].insert(&getOrCreateDisjunctionValue(
-      Constraint, getOrCreateNegationValue(Token)));
-  FlowConditionFirstConjuncts[&Token] =
-      &getOrCreateDisjunctionValue(*FlowConditionFirstConjuncts[&Token],
-                                   getOrCreateNegationValue(Constraint));
+  auto Res = FlowConditionConstraints.try_emplace(&Token, &Constraint);
+  if (!Res.second) {
+    Res.first->second =
+        &getOrCreateConjunctionValue(*Res.first->second, Constraint);
+  }
 }
 
 AtomicBoolValue &
 DataflowAnalysisContext::forkFlowCondition(AtomicBoolValue &Token) {
   auto &ForkToken = makeFlowConditionToken();
   FlowConditionDeps[&ForkToken].insert(&Token);
   addFlowConditionConstraint(ForkToken, Token);
   return ForkToken;
bool DataflowAnalysisContext::flowConditionIsTautology(AtomicBoolValue &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 {
+    llvm::DenseSet<AtomicBoolValue *> &VisitedTokens) {
   auto Res = VisitedTokens.insert(&Token);
   if (!Res.second)
     return;
 
-  auto FirstConjunctIT = FlowConditionFirstConjuncts.find(&Token);
-  if (FirstConjunctIT != FlowConditionFirstConjuncts.end())
-    Constraints.insert(FirstConjunctIT->second);
-  auto RemainingConjunctsIT = FlowConditionRemainingConjuncts.find(&Token);
-  if (RemainingConjunctsIT != FlowConditionRemainingConjuncts.end())
-    Constraints.insert(RemainingConjunctsIT->second.begin(),
-                       RemainingConjunctsIT->second.end());
+  auto ConstraintsIT = FlowConditionConstraints.find(&Token);
+  if (ConstraintsIT == FlowConditionConstraints.end()) {
+    Constraints.insert(&Token);
+  } else {
+    // Bind flow condition token via `iff` to its set of constraints:
+    // FC <=> (C1 ^ C2 ^ ...), where Ci are constraints
+    Constraints.insert(&getOrCreateConjunctionValue(
+        getOrCreateDisjunctionValue(
+            Token, getOrCreateNegationValue(*ConstraintsIT->second)),
+        getOrCreateDisjunctionValue(getOrCreateNegationValue(Token),
+                                    *ConstraintsIT->second)));
+  }
 
   auto DepsIT = FlowConditionDeps.find(&Token);
   if (DepsIT != FlowConditionDeps.end()) {
-    for (AtomicBoolValue *DepToken : DepsIT->second)
+    for (AtomicBoolValue *DepToken : DepsIT->second) {
       addTransitiveFlowConditionConstraints(*DepToken, Constraints,
                                             VisitedTokens);
     }
   }
+}
 
 } // namespace dataflow
 } // namespace clang
 
 using namespace clang;
 
 const Expr &clang::dataflow::ignoreCFGOmittedNodes(const Expr &E) {
   const Expr *Current = &E;