[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 added a comment.

Thank you all for the comments.

In D84736#2179828 <https://reviews.llvm.org/D84736#2179828>, @NoQ wrote:

> I think the overall idea is correct.

So I will keep going in this direction, you can expect the more complex version of this.
I plan to reuse this revision.

So we can formalize this logic like this: 
//for all// `MemReg`, and `Y`: `&Element{MemReg,Y,char} - &MemReg` => `Y`



================
Comment at: clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:1059-1060
+        return UnknownVal();
+      if (Optional<NonLoc> LeftIndex = MaybeNonLocIndexOfElementRegion(LeftER))
+        return LeftIndex.getValue();
+      return UnknownVal();
----------------
NoQ wrote:
> You'll have to multiply by the size of a single element - it's an index, not an offset.
Nice catch.


================
Comment at: clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:1067-1069
+        llvm_unreachable(
+            "TODO: return the negated value of RightIndex - figure out how :D\n"
+            "Maybe a unary minus operator would do the job.");
----------------
NoQ wrote:
> Yeah, sounds like we'll have to stick to `UnknownVal` for now when `RightIndex` is symbolic. You can easily compute unary minus for a concrete index though, and that'll probably be your most important case anyway.
I managed to get around this by turning the unary minus into a binary substitution from zero (using `ArrayIndexTy` type).
Although I should have improved the `SimpleSValBuilder::minus` function to handle other svals besides concrete ints instead.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D84736