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