[PATCH] D112621: [analyzer][solver] Introduce reasoning for not equal to operator

[Gabor Marton via Phabricator via cfe-commits]

martong added a comment.

In D112621#3660256 <https://reviews.llvm.org/D112621#3660256>, @manas wrote:

> Considering @ASDenysPetrov 's example of `LHS = [1, 2] U [8, 9]` and `RHS = [5, 6]`, I constructed a test case as following:
>
> `(((u1 >= 1 && u1 <= 2) || (u1 >= 8 && u1 <= 9)) && u2 >= 5 && u2 <= 6)`
>
> but I can see that the analyzer is bifurcating paths at the OR operator. Essentially, there are two diverged paths:
>
> 1. `1 <= u1 && u1 <= 2 && 5 <= u2 && u2 <= 6`
>
> 2. `8 <= u1 && u1 <= 9 && 5 <= u2 && u2 <= 6`
>
> Separately, they hit `VisitBinaryOperator<BO_NE>` and in both cases, we get `TRUE` for `(u1 != u2)`.
>
> Is there any other way to formulate the expression so that it constructs `LHS = [1, 2] U [8, 9]` and doesn't bifurcate?

@manas, constrain into `[8, 9]` first and then pop out each intermediate element. This should work:

  void clang_analyzer_eval(bool);
  
  template <typename T>
  void clang_analyzer_value(T x);
  
  extern void abort() __attribute__((__noreturn__));
  #define assert(expr) ((expr) ? (void)(0) : abort())
  
  void testDisequalityRules(unsigned int u1, unsigned int u2, unsigned int u3,
                            int s1, int s2, int s3, unsigned char uch,
                            signed char sch, short ssh, unsigned short ush) {
      assert(1 <= u1 && u1 <= 9);
      assert(u1 != 3);
      assert(u1 != 4);
      assert(u1 != 5);
      assert(u1 != 6);
      assert(u1 != 7);
      clang_analyzer_value(u1);      // expected-warning{{32u:{ [1, 2], [8, 9] }}}
      assert(5 <= u2 && u2 <= 6);
      clang_analyzer_value(u2);      // expected-warning{{32u:{ [5, 6] }}}
  
      clang_analyzer_eval(u1 != u2); // expected-warning{{TRUE}}
  }


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D112621