[PATCH] D153366: [dataflow] Add dedicated representation of boolean formulas

[Dmitri Gribenko via Phabricator via cfe-commits]

gribozavr2 accepted this revision.
gribozavr2 added inline comments.
This revision is now accepted and ready to land.


================
Comment at: clang/include/clang/Analysis/FlowSensitive/Formula.h:27
+///
+/// This often represents an assertion that is interesting to the analysis but
+/// cannot immediately be proven true or false. For example:
----------------



================
Comment at: clang/include/clang/Analysis/FlowSensitive/Formula.h:33
+/// We can use these variables in formulas to describe relationships we know
+/// to be true: "if the parameter was null, the program reaches this point".
+/// We also express hypotheses as formulas, and use a SAT solver to check
----------------



================
Comment at: clang/include/clang/Analysis/FlowSensitive/Formula.h:46
+/// Simple formulas such as "true" and "V1" are self-contained.
+/// Compound formulas connect other formulas, e.g. "(V1 & V2) || V3" is an 'or'
+/// formula, with pointers to its operands "(V1 & V2)" and "V3" stored as
----------------
For consistency with the printed representation of the formula.


================
Comment at: clang/include/clang/Analysis/FlowSensitive/Formula.h:69
+
+  Atom atom() const {
+    assert(kind() == AtomRef);
----------------
Should it be called getAsAtom() or castAsAtom() ? For uniformity with other names in Clang and LLVM.




================
Comment at: clang/include/clang/Analysis/FlowSensitive/Formula.h:129-130
+
+  static inline Atom getEmptyKey() { return Atom(Underlying(-1)); }
+  static inline Atom getTombstoneKey() { return Atom(Underlying(-2)); }
+  static unsigned getHashValue(const Atom &Val) {
----------------
'inline' should be unnecessary here.


================
Comment at: clang/include/clang/Analysis/FlowSensitive/Solver.h:73
   private:
-    Result(
-        enum Status SATCheckStatus,
-        std::optional<llvm::DenseMap<AtomicBoolValue *, Assignment>> Solution)
+    Result(enum Status SATCheckStatus,
+           std::optional<llvm::DenseMap<Atom, Assignment>> Solution)
----------------



================
Comment at: clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp:137
+  std::vector<const Formula *> Formulas;
+  for (const BoolValue * Constraint : Constraints)
+    Formulas.push_back(&arena().getFormula(*Constraint));
----------------



================
Comment at: clang/unittests/Analysis/FlowSensitive/SolverTest.cpp:91
+                  Pair(X->atom(), Solver::Result::Assignment::AssignedTrue),
+                  Pair(Y->atom(), Solver::Result::Assignment::AssignedFalse))));
 }
----------------
While you're refactoring this test, could you add 'using' decls for AssignedTrue and AssignedFalse at the top of the file?


================
Comment at: clang/unittests/Analysis/FlowSensitive/TestingSupport.h:479
+public:
+  // Creates a reference to a fresh atomic variable.
+  const Formula *atom() {
----------------
I'd say either "creates a fresh..." or "returns a reference to..." (although pedantically, it returns a pointer)


================
Comment at: clang/unittests/Analysis/FlowSensitive/TestingSupport.h:490
   // Creates a boolean disjunction value.
-  BoolValue *disj(BoolValue *LeftSubVal, BoolValue *RightSubVal) {
-    Vals.push_back(
-        std::make_unique<DisjunctionValue>(*LeftSubVal, *RightSubVal));
-    return Vals.back().get();
+  const Formula*disj(const Formula*LeftSubVal, const Formula*RightSubVal) {
+    return make(Formula::Or, {LeftSubVal, RightSubVal});
----------------



================
Comment at: clang/unittests/Analysis/FlowSensitive/TestingSupport.h:504
 
   // Creates a boolean biconditional value.
+  const Formula *iff(const Formula *LeftSubVal, const Formula *RightSubVal) {
----------------
Similarly, drop "value" from the rest of the comments above.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D153366