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

[Dmitri Gribenko via cfe-commits]

Author: Wei Yi Tee
Date: 2022-06-24T21:52:16+02:00
New Revision: fb88ea62602c90f8f7c80560fd6a14f1c8c6d520

URL: https://github.com/llvm/llvm-project/commit/fb88ea62602c90f8f7c80560fd6a14f1c8c6d520
DIFF: https://github.com/llvm/llvm-project/commit/fb88ea62602c90f8f7c80560fd6a14f1c8c6d520.diff

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

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.

Reviewed By: gribozavr2, sgatev, xazax.hun

Differential Revision: https://reviews.llvm.org/D128357

Added: 
    

Modified: 
    clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
    clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp

Removed: 
    


################################################################################
diff  --git a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
index e2820fcb55655..48d0eedc49dde 100644
--- a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
+++ b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
@@ -198,7 +198,7 @@ class DataflowAnalysisContext {
   /// calls.
   void addTransitiveFlowConditionConstraints(
       AtomicBoolValue &Token, llvm::DenseSet<BoolValue *> &Constraints,
-      llvm::DenseSet<AtomicBoolValue *> &VisitedTokens) const;
+      llvm::DenseSet<AtomicBoolValue *> &VisitedTokens);
 
   std::unique_ptr<Solver> S;
 
@@ -232,21 +232,16 @@ class DataflowAnalysisContext {
   // 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

diff  --git a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
index 81e37e6e6905a..ffd552b1fdc72 100644
--- a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
+++ b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
@@ -66,19 +66,16 @@ BoolValue &DataflowAnalysisContext::getOrCreateNegationValue(BoolValue &Val) {
 }
 
 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 &
@@ -133,24 +130,30 @@ bool DataflowAnalysisContext::flowConditionIsTautology(AtomicBoolValue &Token) {
 
 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);
+    }
   }
 }