clang/test/Analysis/solver-sym-simplification-adjustment.c

   1 // RUN: %clang_analyze_cc1 %s \
   2 // RUN:   -analyzer-checker=core \
   3 // RUN:   -analyzer-checker=debug.ExprInspection \
   4 // RUN:   -analyzer-config eagerly-assume=false \
   5 // RUN:   -verify
   6
   7 void clang_analyzer_warnIfReached(void);
   8 void clang_analyzer_eval(_Bool);
   9
  10 void test_simplification_adjustment_concrete_int(int b, int c) {
  11   if (b < 0 || b > 1)  // b: [0,1]
  12     return;
  13   if (c < -1 || c > 1) // c: [-1,1]
  14     return;
  15   if (c + b != 0)      // c + b == 0
  16     return;
  17   clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
  18   if (b != 1)          // b == 1  --> c + 1 == 0 --> c == -1
  19     return;
  20   clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
  21   clang_analyzer_eval(c == -1);   // expected-warning{{TRUE}}
  22
  23   // Keep the symbols and the constraints! alive.
  24   (void)(b * c);
  25   return;
  26 }
  27
  28 void test_simplification_adjustment_range(int b, int c) {
  29   if (b < 0 || b > 1)              // b: [0,1]
  30     return;
  31   if (c < -1 || c > 1)             // c: [-1,1]
  32     return;
  33   if (c + b < -1 || c + b > 0)     // c + b: [-1,0]
  34     return;
  35   clang_analyzer_warnIfReached();  // expected-warning{{REACHABLE}}
  36   if (b != 1)                      // b == 1  --> c + 1: [-1,0] --> c: [-2,-1]
  37     return;
  38                                    // c: [-2,-1] is intersected with the
  39                                    // already associated range which is [-1,1],
  40                                    // thus we get c: [-1,-1]
  41   clang_analyzer_warnIfReached();  // expected-warning{{REACHABLE}}
  42   clang_analyzer_eval(c == -1);    // expected-warning{{TRUE}}
  43
  44   // Keep the symbols and the constraints! alive.
  45   (void)(b * c);
  46   return;
  47 }
  48
  49 void test_simplification_adjustment_to_infeasible_concrete_int(int b, int c) {
  50   if (b < 0 || b > 1) // b: [0,1]
  51     return;
  52   if (c < 0 || c > 1) // c: [0,1]
  53     return;
  54   if (c + b != 0)     // c + b == 0
  55     return;
  56   clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
  57   if (b != 1) {       // b == 1  --> c + 1 == 0 --> c == -1 contradiction
  58     clang_analyzer_eval(b == 0);  // expected-warning{{TRUE}}
  59     clang_analyzer_eval(c == 0);  // expected-warning{{TRUE}}
  60     // Keep the symbols and the constraints! alive.
  61     (void)(b * c);
  62     return;
  63   }
  64   clang_analyzer_warnIfReached(); // no warning
  65
  66   // Keep the symbols and the constraints! alive.
  67   (void)(b * c);
  68   return;
  69 }
  70
  71 void test_simplification_adjustment_to_infeassible_range(int b, int c) {
  72   if (b < 0 || b > 1)              // b: [0,1]
  73     return;
  74   if (c < 0 || c > 1)              // c: [0,1]
  75     return;
  76   if (c + b < -1 || c + b > 0)     // c + b: [-1,0]
  77     return;
  78   clang_analyzer_warnIfReached();  // expected-warning{{REACHABLE}}
  79   if (b != 1)                      // b == 1  --> c + 1: [-1,0] --> c: [-2,-1] contradiction
  80     return;
  81   clang_analyzer_warnIfReached();  // no warning
  82
  83   // Keep the symbols and the constraints! alive.
  84   (void)(b * c);
  85   return;
  86 }
  87
  88 void test_simplification_adjusment_no_infinite_loop(int a, int b, int c) {
  89   if (a == b)        // a != b
  90     return;
  91   if (c != 0)        // c == 0
  92     return;
  93
  94   if (b != 0)        // b == 0
  95     return;
  96   // The above simplification of `b == 0` could result in an infinite loop
  97   // unless we detect that the State is unchanged.
  98   // The loop:
  99   // 1) Simplification of the trivial equivalence class
 100   //      "symbol": "(reg_$0<int a>) == (reg_$1<int b>)", "range": "{ [0, 0] }"
 101   //    results in
 102   //      "symbol": "(reg_$0<int a>) == 0", "range": "{ [0, 0] }" }
 103   //    which in turn creates a non-trivial equivalence class
 104   //      [ "(reg_$0<int a>) == (reg_$1<int b>)", "(reg_$0<int a>) == 0" ]
 105   // 2) We call assumeSymInclusiveRange("(reg_$0<int a>) == 0")
 106   //    and that calls **simplify** on the associated non-trivial equivalence
 107   //    class. During the simplification the State does not change, we reached
 108   //    the fixpoint.
 109
 110   (void)(a * b * c);
 111 }