[PATCH] D77062: [analyzer] Added check for unacceptable equality operation between Loc and NonLoc types

Sat Apr 11 18:08:39 PDT 2020

Szelethus added a comment.

In D77062#1959286 <https://reviews.llvm.org/D77062#1959286>, @ASDenysPetrov wrote:

> @Szelethus , @NoQ please, look at my solution. I'm not sure if it is correct, but it actually passes all the tests and throw off the issue.

Sorry for the late answer, I've been kinda busy with other things! And thank you for attending to these bugs! I admit, this isn't really within the realms of my expertise, but nevertheless, here are my two cents.

I think what what be great to see here (and this seems to be the thing @NoQ is fishing for) is not to change an if branch and avoid running into the crash, but rather find out why `assumeZero` was ever called with a `nonloc` value, which shouldn't really happen. We're treating the symptom, not curing the illness, if you will. The `SVal` (if its `DefinedSVal`) is supposed to be always `MemRegionVal` here, is that right? Maybe if we tried to add an assert here, that could help nail where the actual issue is coming from. It's probably in `evalStrcpyCommon`, judging from the bug report you linked in your summary.

================
Comment at: clang/lib/StaticAnalyzer/Checkers/CStringChecker.cpp:272-274
   Optional<DefinedSVal> val = V.getAs<DefinedSVal>();
-  if (!val)
-    return std::pair<ProgramStateRef , ProgramStateRef >(state, state);
+  if (val && !V.getAs<nonloc::LazyCompoundVal>()) {
+     // return pair shall be {null, non-null} so reorder states
----------------

>>Why are we getting a compound value here? 
> We are getting **nonloc::SymbolVal** here, not a compound value. SA thinks that double-dereference of the first agrument applies to unsigned char* *, instead of char* * * (look at the test sample).

So, in other words the condition seems to be this:
```lang=cpp
if (V.getAs<DefinedSVall>(&& !V.getAs<nonloc::LazyCompoundVal>())
```

But `nonloc::SymbolVal` is a subclass of `DefinedSVal` (and is not a `nonloc::LazyCompoundVal`), so we're definitely running into the assume call, isn't that right?
https://clang.llvm.org/doxygen/classclang_1_1ento_1_1SVal.html

What really seems to be the problem solver here is that you changed the assumption from `x == 0` (creating a state where this expression is false, and one where it isn't) into `x` (whether `x` is true or not).

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

https://reviews.llvm.org/D77062