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

[Denys Petrov via Phabricator via cfe-commits]

ASDenysPetrov added inline comments.


================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1618-1627
+    const SymbolRef LHS = Sym->getLHS();
+    const llvm::APSInt &Zero =
+        Builder.getBasicValueFactory().getValue(0, Sym->getType());
+    // a % b != 0 implies that a != 0.
+    if (!Constraint.containsZero()) {
+      State = RCM.assumeSymNE(State, LHS, Zero, Zero);
+      if (!State)
----------------
Let me suggest possible changes.


================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1619-1620
+    const SymbolRef LHS = Sym->getLHS();
+    const llvm::APSInt &Zero =
+        Builder.getBasicValueFactory().getValue(0, Sym->getType());
+    // a % b != 0 implies that a != 0.
----------------
Howerver, put this line inside //if-body// below, since `Zero` isn't needed wherever else.


================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1618-1627
+    const SymbolRef LHS = Sym->getLHS();
+    const llvm::APSInt &Zero =
+        Builder.getBasicValueFactory().getValue(0, Sym->getType());
+    // a % b != 0 implies that a != 0.
+    if (!Constraint.containsZero()) {
+      State = RCM.assumeSymNE(State, LHS, Zero, Zero);
+      if (!State)
----------------
martong wrote:
> ASDenysPetrov wrote:
> > How about using the family of `ProgramState::isNonNull` or `ProgramState::isNull` or `RangeConstraintManager::checkNull` functoins for this stuff?
> I've been checking this and turend out that `ProgramState::isNull` does not modify the State (this is aligned with being a `const` member function). So, these functions do not "assume" anything, they can be used only to query some property of an SVal (or Symbol) from the State.
> 
> However, this comment and your other previous comment made me to do further investigations towards exploiting the "assume" machinery better. The result is a new child patch, where we can handle "adjustments" as well.
But I don't see you use the modified `State` in any way. Why it's important for you to change the `State`?




Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D110357