[PATCH] D124758: [analyzer] Implement assume in terms of assumeDual

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

steakhal added a comment.

This commit introduced a serious runtime regression on this code:

  #define DEMONSTRATE_HANG
  
  typedef unsigned char uint8_t;
  typedef unsigned short uint16_t;
  typedef unsigned long uint64_t;
  
  void clang_analyzer_numTimesReached(void);
  
  int filter_slice_word(int sat_linesize, int sigma, int radius, uint64_t *sat,
                        uint64_t *square_sat, int width, int height,
                        int src_linesize, int dst_linesize, const uint16_t *src,
                        uint16_t *dst, int jobnr, int nb_jobs) {
    const int starty = height * jobnr / nb_jobs;
    const int endy = height * (jobnr + 1) / nb_jobs;
  
    clang_analyzer_numTimesReached(); // 1 times
    for (int y = starty; y < endy; y++) {
      clang_analyzer_numTimesReached(); // 285 times
  
      int lower_y = y - radius < 0 ? 0 : y - radius;
      int higher_y = y + radius + 1 > height ? height : y + radius + 1;
      int dist_y = higher_y - lower_y;
      clang_analyzer_numTimesReached(); // 1128 times
  
      for (int x = 0; x < width; x++) {
        clang_analyzer_numTimesReached(); // 560 times
        
        int lower_x = x - radius < 0 ? 0 : x - radius;
        int higher_x = x + radius + 1 > width ? width : x + radius + 1;
        int count = dist_y * (higher_x - lower_x);
  #ifdef DEMONSTRATE_HANG
        uint64_t sum = sat[higher_y * sat_linesize + higher_x] -
                       sat[higher_y * sat_linesize + lower_x] -
                       sat[lower_y * sat_linesize + higher_x] +
                       sat[lower_y * sat_linesize + lower_x];
        uint64_t square_sum = square_sat[higher_y * sat_linesize + higher_x] -
                              square_sat[higher_y * sat_linesize + lower_x] -
                              square_sat[lower_y * sat_linesize + higher_x] +
                              square_sat[lower_y * sat_linesize + lower_x];
        uint64_t mean = sum / count;
        uint64_t var = (square_sum - sum * sum / count) / count;
        dst[y * dst_linesize + x] =
            (sigma * mean + var * src[y * src_linesize + x]) / (sigma + var);
  #endif
      }
    }
    return 0;
  }

  /build/release/bin/clang --analyze -Xclang -analyzer-checker=core,alpha.security.ArrayBoundV2,debug.ExprInspection test.c

Prior to this commit, the analysis of this code took about 2.6 seconds on my machine (release build with shared libs)
After this commit, it takes more than 67 minutes, and most of the time is spent in the constraint solver doing simplification I think.

Be reminded of the `ArrayBoundV2` checker which will try to express the symbolic atom of the indexer expression:
`0 <= (x + 3) < extent` => `-3 <= x < extent - 3` (this is more complex in the wild, it's for demonstration now).
So, it will create new and new states during this process, while gathering constraints to make the indexing well-formed.

However, the nested loops and the eager bifurcation over the `<` and `>` operators cause a significant path explosion, and on each one of them, we do this complex equality system reorganization, aggregating constraints, thus causing constraint system simplifications down the line.
I'm not sure how to tackle this problem ATM.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D124758