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

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

steakhal planned changes to this revision.
steakhal marked an inline comment as done.
steakhal 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>();
----------------
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)
```


================
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.
----------------
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.


================
Comment at: clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:1068
+        }
+      } else if (LeftER && !RightER) {
+        NonLoc LeftIndex = ByteOffsetOfElement(LeftER);
----------------
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.


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

https://reviews.llvm.org/D84736