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

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

steakhal updated this revision to Diff 286318.
steakhal marked 4 inline comments as done.
steakhal retitled this revision from "[analyzer][RFC] Handle pointer difference of ElementRegion and SymbolicRegion" to "[analyzer] Handle pointer difference of ElementRegion and SymbolicRegion".
steakhal edited the summary of this revision.
steakhal added a comment.

- Refined documentation comments as noted.
- Added tests.
- Removed the complicated `ByteOffsetOfElement` lambda.
- Rename revision.

---

Before this patch, only these reported `Unknown` instead of the currently expected value.
Besides that all tests passed as-is on master:

  clang_analyzer_dump_int(p - p0);       // expected-warning {{0 S32b}}
  clang_analyzer_dump_int(p - p1);       // expected-warning {{-1 S32b}}
  clang_analyzer_dump_int(p - pn);       // expected-warning-re {{0 - (reg_${{[0-9]+}}<int n>)}}
  clang_analyzer_dump_int((p + 1) - p);  // expected-warning {{1 S32b}}
  
  // Swapped operands:
  clang_analyzer_dump_int(p0 - p);       // expected-warning {{0 S32b}}
  clang_analyzer_dump_int(p1 - p);       // expected-warning {{1 S32b}}
  clang_analyzer_dump_int(pn - p);       // expected-warning-re {{reg_${{[0-9]+}}<int n>}}
  clang_analyzer_dump_int(p - (p + 1));  // expected-warning {{-1 S32b}}



---

Further notes:
Element{X, n, Ty1} and Element{X, m, Ty2} should compare equal if and only if the `n * sizeof(Ty1)` equals to `n * sizeof(Ty2)`.
However, previously it did not take the size of the types into account (there is the corresponding FIXIT).
I'm not fixing this either for now.

The analyzer returns `Unknown` for this call:
clang_analyzer_dump_int((p + 1) - q);
However, IMO it should hold the expression 'p+1+q' instead - regardless of `p` alias (or not) the same memory region of `p`
There is a FIXME in the testcode for this.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D84736

Files:
  clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
  clang/test/Analysis/pointer-arithmetic.c

-------------- next part --------------
A non-text attachment was scrubbed...
Name: D84736.286318.patch
Type: text/x-patch
Size: 11167 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20200818/615e5d60/attachment-0001.bin>