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

[Gabor Marton via Phabricator via cfe-commits]

martong marked 5 inline comments as done.
martong added inline comments.


================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1619
+      return true;
+    const SymExpr *LHS = Sym->getLHS();
+    const llvm::APSInt &Zero =
----------------
ASDenysPetrov wrote:
> steakhal wrote:
> > 
> Since `SymbolRef` actually is already `const`. (`using SymbolRef = const SymExpr *;`)
Fair enough.


================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1623
+    if (Constraint.containsZero())
+      State = RCM.assumeSymEQ(State, LHS, Zero, Zero);
+    else
----------------
steakhal wrote:
> 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`.
Ahh, very good catch, sharp eyes! This mistake slipped in when I extended the original logic with `a % b == 0 implies that a == 0`. Fixed it.


================
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.
----------------
steakhal wrote:
> 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.
> >> 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
Yeah you're right. It has nothing to do with the non-constness of `RCM.assumeSymNE`, my bad. The problem is that we try to assign a new state to the member non-const `State` and assignment is non-const:
```
No viable overloaded '='
/home/egbomrt/WORK/llvm4/git/llvm-project/llvm/include/llvm/ADT/IntrusiveRefCntPtr.h:188:23:
note: candidate function not viable: 'this' argument has type 'const clang::ento::ProgramStateRef' (aka 'const IntrusiveRefCntPtr<const clang::ento::ProgramState>'), but method is not marked const
```

> ---
> 
> 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.
Ok, I've added those comments.




================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1609-1612
+      const SymExpr *LHS = Sym->getLHS();
+      const llvm::APSInt &Zero =
+          Builder.getBasicValueFactory().getValue(0, LHS->getType());
+      State = RCM->assumeSymNE(State, LHS, Zero, Zero);
----------------
ASDenysPetrov wrote:
> martong wrote:
> > steakhal wrote:
> > > ASDenysPetrov wrote:
> > > > Maybe make some more complex assumptions to cover complex **LHS's**?
> > > Oh nice.
> > `State->assume` goes through many higher level abstractions and finally calls `assumeSymNE`, so I think calling that would be a pessimization in this case.
> I agree, but then you lose an internal simplification of LHS symbol.
Well, I cannot come up any disadvantages of  using`State->assume` other than some performance constraints. On the other hand, that could simplify the implementation by eliminating the need for `RCM`. I'll give it a try and perhaps will update the patch accordingly.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D110357