// RUN: %clang_analyze_cc1 %s \
// RUN:   -analyzer-checker=core \
// RUN:   -analyzer-checker=debug.ExprInspection \
// RUN:   -analyzer-config eagerly-assume=false \
// RUN:   -verify

void clang_analyzer_eval(bool);
void clang_analyzer_warnIfReached();

int test_legacy_behavior(int x, int y) {
  if (y != 0)
    return 0;
  if (x + y != 0)
    return 0;
  clang_analyzer_eval(x + y == 0); // expected-warning{{TRUE}}
  clang_analyzer_eval(y == 0);     // expected-warning{{TRUE}}
  return y / (x + y);              // expected-warning{{Division by zero}}
}

int test_rhs_further_constrained(int x, int y) {
  if (x + y != 0)
    return 0;
  if (y != 0)
    return 0;
  clang_analyzer_eval(x + y == 0); // expected-warning{{TRUE}}
  clang_analyzer_eval(y == 0);     // expected-warning{{TRUE}}
  return 0;
}

int test_lhs_further_constrained(int x, int y) {
  if (x + y != 0)
    return 0;
  if (x != 0)
    return 0;
  clang_analyzer_eval(x + y == 0); // expected-warning{{TRUE}}
  clang_analyzer_eval(x == 0);     // expected-warning{{TRUE}}
  return 0;
}

int test_lhs_and_rhs_further_constrained(int x, int y) {
  if (x % y != 1)
    return 0;
  if (x != 1)
    return 0;
  if (y != 2)
    return 0;
  clang_analyzer_eval(x % y == 1); // expected-warning{{TRUE}}
  clang_analyzer_eval(y == 2);     // expected-warning{{TRUE}}
  return 0;
}

int test_commutativity(int x, int y) {
  if (x + y != 0)
    return 0;
  if (y != 0)
    return 0;
  clang_analyzer_eval(y + x == 0); // expected-warning{{TRUE}}
  clang_analyzer_eval(y == 0);     // expected-warning{{TRUE}}
  return 0;
}

int test_binop_when_height_is_2_r(int a, int x, int y, int z) {
  switch (a) {
  case 1: {
    if (x + y + z != 0)
      return 0;
    if (z != 0)
      return 0;
    clang_analyzer_eval(x + y + z == 0); // expected-warning{{TRUE}}
    clang_analyzer_eval(z == 0);         // expected-warning{{TRUE}}
    break;
  }
  case 2: {
    if (x + y + z != 0)
      return 0;
    if (y != 0)
      return 0;
    clang_analyzer_eval(x + y + z == 0); // expected-warning{{TRUE}}
    clang_analyzer_eval(y == 0);         // expected-warning{{TRUE}}
    break;
  }
  case 3: {
    if (x + y + z != 0)
      return 0;
    if (x != 0)
      return 0;
    clang_analyzer_eval(x + y + z == 0); // expected-warning{{TRUE}}
    clang_analyzer_eval(x == 0);         // expected-warning{{TRUE}}
    break;
  }
  case 4: {
    if (x + y + z != 0)
      return 0;
    if (x + y != 0)
      return 0;
    clang_analyzer_eval(x + y + z == 0); // expected-warning{{TRUE}}
    clang_analyzer_eval(x + y == 0);     // expected-warning{{TRUE}}
    break;
  }
  case 5: {
    if (z != 0)
      return 0;
    if (x + y + z != 0)
      return 0;
    clang_analyzer_eval(x + y + z == 0); // expected-warning{{TRUE}}
    if (y != 0)
      return 0;
    clang_analyzer_eval(y == 0);         // expected-warning{{TRUE}}
    clang_analyzer_eval(z == 0);         // expected-warning{{TRUE}}
    clang_analyzer_eval(x + y + z == 0); // expected-warning{{TRUE}}
    break;
  }

  }
  return 0;
}

void test_equivalence_classes_are_updated(int a, int b, int c, int d) {
  if (a + b != c)
    return;
  if (a != d)
    return;
  if (b != 0)
    return;
  clang_analyzer_eval(c == d); // expected-warning{{TRUE}}
  // Keep the symbols and the constraints! alive.
  (void)(a * b * c * d);
  return;
}

void test_contradiction(int a, int b, int c, int d) {
  if (a + b != c)
    return;
  if (a == c)
    return;
  clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}

  // Bring in the contradiction.
  if (b != 0)
    return;
  clang_analyzer_warnIfReached(); // no-warning, i.e. UNREACHABLE
  // Keep the symbols and the constraints! alive.
  (void)(a * b * c * d);
  return;
}

void test_deferred_contradiction(int e0, int b0, int b1) {

  int e1 = e0 - b0; // e1 is bound to (reg_$0<int e0>) - (reg_$1<int b0>)
  (void)(b0 == 2);  // bifurcate

  int e2 = e1 - b1;
  if (e2 > 0) { // b1 != e1
    clang_analyzer_warnIfReached();   // expected-warning{{REACHABLE}}
    // Here, e1 is still bound to (reg_$0<int e0>) - (reg_$1<int b0>) but we
    // should be able to simplify it to (reg_$0<int e0>) - 2 and thus realize
    // the contradiction.
    if (b1 == e1) {
      clang_analyzer_warnIfReached(); // no-warning, i.e. UNREACHABLE
      (void)(b0 * b1 * e0 * e1 * e2);
    }
  }
}