[PATCH] D126481: [analyzer] Handle SymbolCast in SValBuilder

[Gabor Marton via Phabricator via cfe-commits]

martong added a comment.

I don't see this case different to the unary expressions. Consider the unary minus for example. Let's say, the symbol `a` is constrained to `[1, 1]` and then `-a` is constrained to `[-2, -2]`. This is clearly an infeasible state and the analyzer will terminate the path. So, no further call of SValBuilder should happen from that point. That is, it is meaningless to evaluate `-(-a)` if there is a contradiction in the constraints that are assigned to the sub-symbols of the the symbol tree of `-(-a)`.
Here is a test case that demonstrates this (this passes with latest llvm/main):

  // RUN: %clang_analyze_cc1 %s \
  // RUN:   -analyzer-checker=core \
  // RUN:   -analyzer-checker=debug.ExprInspection \
  // RUN:   -analyzer-config eagerly-assume=false \
  // RUN:   -verify
  
  extern void abort() __attribute__((__noreturn__));
  #define assert(expr) ((expr) ? (void)(0) : abort())
  
  void clang_analyzer_warnIfReached();
  void clang_analyzer_eval(int);
  
  void test(int a, int b) {
    assert(-a == -1);
    assert(a == 1);
    clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
    clang_analyzer_eval(-(-a) == 1); // expected-warning{{TRUE}}
  
    assert(-b <= -2);
    assert(b == 1);
    clang_analyzer_warnIfReached(); // unreachable!, no-warning
    clang_analyzer_eval(-(-b) == 1); // no-warning
  }


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D126481