xazax.hun accepted this revision.
xazax.hun added a comment.
Overall, looks good to me. Some nits inline.
Are there plans to get a model/assignment of the variables from the solver?
That could be helpful for generating warning messages in the future :)
================
Comment at: clang/include/clang/Analysis/FlowSensitive/Solver.h:39
+
+ virtual ~Solver() {}
+
----------------
`= default`? To make this trivially destructible.
================
Comment at: clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp:159
+ /// Adds the 3-literal `L1 v L2 v L3` clause to the formula.
+ void addClause(Literal L1, Literal L2, Literal L3) {
+ // The literals are guaranteed to be distinct from properties of BoolValue
----------------
Shouldn't we make this function variadic (or taking a container) instead of
having multiple overloads?
================
Comment at: clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp:213
+ // Visit the sub-values of `Val`.
+ if (auto *C = dyn_cast<ConjunctionValue>(Val)) {
+ UnprocessedSubVals.push(&C->getLeftSubValue());
----------------
Switch on the kind instead? That way `DisjunctionValue` and `ConjunctionValue`
could be handled by the same case.
================
Comment at: clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp:241
+ for (BoolValue *Val : Vals)
+ UnprocessedSubVals.push(Val);
+ while (!UnprocessedSubVals.empty()) {
----------------
While I get that this should be empty before this loop due to the loop
condition at the previous use, but I find such code confusing. I'd prefer to
either use a separate queue or have at least an assert to remind us that this
one should be a clean container before the loop.
================
Comment at: clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp:355
+
+ LevelVars.resize(Formula.LargestVar + 1);
+
----------------
Shouldn't we call the right ctor directly in the initialization list instead of
resizing a default constructed vector?
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D120289/new/
https://reviews.llvm.org/D120289
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
