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
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
