[PATCH] D124395: [clang][dataflow] Optimize flow condition representation

[Yitzhak Mandelbaum via Phabricator via cfe-commits]

ymandel accepted this revision.
ymandel added a comment.
This revision is now accepted and ready to land.

Nice work. On the surface, this adds complexity to the system and so should be justified in terms of performance improvements. However, having read through the patch, I think it overall reduces the complexity, since both environment join and boolean-value join have been radically simplified.  So, I'm fine with the patch as is, even without performance measurement. That said, I'm not against such measurement -- just saying it's not blocking. :)

If you agree, you may want to reword the description of the patch to focuse on the design improvements rather than (exclusively) the optimization aspect.



================
Comment at: clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h:49
-  /// Returns the SAT solver instance that is available in this context.
-  Solver &getSolver() const { return *S; }
-
----------------
nit: Maybe mention this removal in the patch description.


================
Comment at: clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h:152
 
+  /// Returns a fresh flow condition token.
+  AtomicBoolValue &makeFlowConditionToken();
----------------
I think it would be helpful to expand here with a brief explanation of the role of flow condition tokens.


================
Comment at: clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h:155
+
+  /// Adds `Constraint` to the flow condition indentified by `Token`.
+  void addFlowConditionConstraint(AtomicBoolValue &Token,
----------------



================
Comment at: clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h:209
+
+  // Flow conditions are represented as `FC <=> (C1 ^ C2 ^ ...)` clauses where
+  // `FC` is a flow condition token (an atomic boolean) and `Ci`s are a set of
----------------
Is the idea that this is an encoding of the `<=>`? If so, maybe use "encoded" in the internal description, as in "Internally, a flow condition clause is encoded as ..."? 

Or, a bigger change:

Flow conditions are tracked symbolically: each unique flow condition is associated with a fresh symbolic variable, bound to the clause that defines the flow condition.  Conceptually, each binding corresponds to an "iff" over the form `FC <=> (C1 ^ C2 ^ ...)`, where `FC` is a flow condition token (an atomic boolean) and `Ci`s are the set of constraints that define the flow condition. However, we do not record the formula directly as an `iff`. Instead, internally, a flow condition clause is ...


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D124395/new/

https://reviews.llvm.org/D124395