[PATCH] D84736: [analyzer][RFC] Handle pointer difference of ElementRegion and SymbolicRegion

[Valeriy Savchenko via Phabricator via cfe-commits]

vsavchenko added inline comments.


================
Comment at: clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:1035-1038
+        return evalBinOpNN(state, BO_Mul, Index,
+                           makeArrayIndex(SingleElementSize.getQuantity()),
+                           ArrayIndexTy)
+            .castAs<NonLoc>();
----------------
steakhal wrote:
> vsavchenko wrote:
> > I would prefer having a comment for this line with a very simple formula of the thing we are calculating.  I think it can increase the readability of the code because when there is a call accepting a whole bunch of arguments it is never obvious and it always takes time to parse through.
> Sure, I will add something like this:
> ```
> // T buf[n];   Element{buf,2} --> 2 * sizeof(T)
> ```
Yeah, something like this would be good.  I would prefer more explicit version of it simply because `Stmt;   Smth` can be a bit confusing for notation. 


================
Comment at: clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:1041
+
+      // If both has the same memory region, and the index has a concrete value,
+      // we can evaluate equality operators.
----------------
steakhal wrote:
> vsavchenko wrote:
> > This comment is a bit deceiving IMO.  It returns a concrete value even when `HasSameMemRegions` is false, but from the comment it seems like we evaluate the operator ONLY when `HasSameMemRegions` is true.
> No, the comment is up to date.
> This lambda handles both equality and inequality operators, and this is why its called EvaluateEqualityOperators.
> 
> EQResult will be true only if the two memory regions are the same and the index is zero.
> The result of the **inequality**  is just the negated version of the result of equality.
> If both have the same and the index has a concrete value, we can evaluate equality operators.

In this setting, I assume that we talk about "if and only if", and in any case other than "//both have the same and the index has a concrete value//" we **can't** evaluate equality operators.
Also, I didn't say that it is necessarily incorrect, I said that it is deceiving because if it confused me, it can confuse other people as well.

I would prefer something more like this:

```
// For a situation, a OP b + index, where OP is equality operator, 
// we can infer the result for known `index` values.
// We are able to do this because ...
```


================
Comment at: clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:1068
+        }
+      } else if (LeftER && !RightER) {
+        NonLoc LeftIndex = ByteOffsetOfElement(LeftER);
----------------
steakhal wrote:
> vsavchenko wrote:
> > I think it's better to add comments for each case describing what is the situation we handle here in a simplified form.
> > And for each return within the case - a short comment with the reason.
> I'm not sure if it's necessary.
> I have already described these 3 cases at the beginning.
> Quote:
> ```
>     // Handle: \forall MemRegion X, \forall NonLoc n, m:
>     //  - Element{X,n} OP Element{X,m}
>     //  - Element{X,n} OP X
>     //  -            X OP Element{X,n}
>     // We don't handle here nested ElementRegions like in the this expression:
>     // Element{Element{x,3,int [10]},5,int}  ==  Element{x,35,int}
> ```
> If you still insist, I will defenately add more comments though.
In that comment, you don't say anything about `OP` and how we //handle// those.

Also I want to add that you probably want to add an arbitrary `MemRegion Y` as well because you handle not only cases when `MemRegion`s are same.


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

https://reviews.llvm.org/D84736