[PATCH] D110357: [Analyzer] Extend ConstraintAssignor to handle remainder op

[Balázs Benics via Phabricator via cfe-commits]

steakhal added inline comments.


================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1619
+      return true;
+    const SymExpr *LHS = Sym->getLHS();
+    const llvm::APSInt &Zero =
----------------



================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1623
+    if (Constraint.containsZero())
+      State = RCM.assumeSymEQ(State, LHS, Zero, Zero);
+    else
----------------
In case the `Constraint` //might be// zero, why do you constrain `LHS` so that it **must be** zero?
I could not come up with a concrete example, but I hope you got my concern.
We either have a logic flaw or we lack an assertion here stating this hidden assumption about `Constraints`.


================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1626-1628
+    if (!State)
+      return false;
+    return true;
----------------



================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1603-1604
 
+  template <typename SymT>
+  bool handleRem(const SymT *Sym, RangeSet Constraint) {
+    // a % b != 0 implies that a != 0.
----------------
martong wrote:
> ASDenysPetrov wrote:
> > steakhal wrote:
> > > Why is this not a `const` member function?
> > IMO it's better to rename the function `handleRemainderOp`.
> > 
> > Add a function description in comments above. 
> > E.g. Handle expressions like: `a % b == 0`. ... Returns `true` when //bla-bla//, otherwise returns `false`.
> > Why is this not a const member function?
> Because `RCM.assumeSymNE` is not `const`.
> 
> > IMO it's better to rename the function handleRemainderOp.
> I agree, changed it.
>> Why is this not a const member function?
> Because RCM.assumeSymNE is not const.
I don't think it's an excuse: https://godbolt.org/z/nEcsozheq

---

Aside from that, I would clarify that it will try to apply the following *two* assumptions:
`a % b == 0 implies that a == 0.`
`a % b != 0 implies that a != 0.`
Now the comment only highlights the latter.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D110357