[PATCH] D77792: [analyzer] Extend constraint manager to be able to compare simple SymSymExprs

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

steakhal created this revision.
steakhal added reviewers: NoQ, baloghadamsoftware, Charusso, Szelethus.
Herald added subscribers: cfe-commits, ASDenysPetrov, martong, dkrupp, donat.nagy, mikhail.ramalho, a.sidorin, rnkovacs, szepet, xazax.hun, whisperity.
Herald added a project: clang.

This patch extends the constraint manager to be able to reason about trivial sym-sym comparisons.

We all know that `a < b` if the maximum value of `a` is still less than the minimum value of `b`.
This reasoning can be applied for the <,<=,>,>= relation operators.
This patch solely implements this functionality.

This patch does not address transitity like:
If `a < b` and `b < c` than `a < c`.

This patch is necessary to be able to express //hidden function preconditions//.
For example, with the `D69726` we could express the connection between the 
extent size of `src` and the size (`n`) parameter of the function.

  #define ANALYZER_ASSERT assert
  
  void my_memcpy(char *dst, char *src, int n) {
    ANALYZER_ASSERT(clang_analyzer_getExtent(src) >= n)
    ANALYZER_ASSERT(clang_analyzer_getExtent(dst) >= n)
    
    for (int i = 0; i < n; ++i) {
      // The extent of dst would be compared to the index i.
      dst[i] = src[i]; // each memory access in-bound, no-warning
    }
  }


Repository:
  rG LLVM Github Monorepo

https://reviews.llvm.org/D77792

Files:
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
  clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
  clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
  clang/test/Analysis/constraint-manager-sym-sym.c

-------------- next part --------------
A non-text attachment was scrubbed...
Name: D77792.256252.patch
Type: text/x-patch
Size: 13317 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20200409/7c18066a/attachment.bin>