Print this page
new smatch

Split Close
Expand all
Collapse all
          --- old/usr/src/tools/smatch/src/smatch_comparison.c
          +++ new/usr/src/tools/smatch/src/smatch_comparison.c
↓ open down ↓ 49 lines elided ↑ open up ↑
  50   50          struct var_sym *vs;
  51   51  
  52   52          if (!vsl)
  53   53                  return NULL;
  54   54          if (ptr_list_size((struct ptr_list *)vsl) != 1)
  55   55                  return NULL;
  56   56          vs = first_ptr_list((struct ptr_list *)vsl);
  57   57          return vs->sym;
  58   58  }
  59   59  
       60 +static const char *show_comparison(int comparison)
       61 +{
       62 +        if (comparison == IMPOSSIBLE_COMPARISON)
       63 +                return "impossible";
       64 +        if (comparison == UNKNOWN_COMPARISON)
       65 +                return "unknown";
       66 +        return show_special(comparison);
       67 +}
       68 +
  60   69  struct smatch_state *alloc_compare_state(
  61   70                  struct expression *left,
  62   71                  const char *left_var, struct var_sym_list *left_vsl,
  63   72                  int comparison,
  64   73                  struct expression *right,
  65   74                  const char *right_var, struct var_sym_list *right_vsl)
  66   75  {
  67   76          struct smatch_state *state;
  68   77          struct compare_data *data;
  69   78  
  70   79          state = __alloc_smatch_state(0);
  71      -        state->name = alloc_sname(show_special(comparison));
       80 +        state->name = alloc_sname(show_comparison(comparison));
  72   81          data = __alloc_compare_data(0);
  73   82          data->left = left;
  74   83          data->left_var = alloc_sname(left_var);
  75   84          data->left_vsl = clone_var_sym_list(left_vsl);
  76   85          data->comparison = comparison;
  77   86          data->right = right;
  78   87          data->right_var = alloc_sname(right_var);
  79   88          data->right_vsl = clone_var_sym_list(right_vsl);
  80   89          state->data = data;
  81   90          return state;
  82   91  }
  83   92  
  84   93  int state_to_comparison(struct smatch_state *state)
  85   94  {
  86   95          if (!state || !state->data)
  87      -                return 0;
       96 +                return UNKNOWN_COMPARISON;
  88   97          return ((struct compare_data *)state->data)->comparison;
  89   98  }
  90   99  
  91  100  /*
  92  101   * flip_comparison() reverses the op left and right.  So "x >= y" becomes "y <= x".
  93  102   */
  94  103  int flip_comparison(int op)
  95  104  {
  96  105          switch (op) {
  97      -        case 0:
  98      -                return 0;
      106 +        case UNKNOWN_COMPARISON:
      107 +                return UNKNOWN_COMPARISON;
  99  108          case '<':
 100  109                  return '>';
 101  110          case SPECIAL_UNSIGNED_LT:
 102  111                  return SPECIAL_UNSIGNED_GT;
 103  112          case SPECIAL_LTE:
 104  113                  return SPECIAL_GTE;
 105  114          case SPECIAL_UNSIGNED_LTE:
 106  115                  return SPECIAL_UNSIGNED_GTE;
 107  116          case SPECIAL_EQUAL:
 108  117                  return SPECIAL_EQUAL;
 109  118          case SPECIAL_NOTEQUAL:
 110  119                  return SPECIAL_NOTEQUAL;
 111  120          case SPECIAL_GTE:
 112  121                  return SPECIAL_LTE;
 113  122          case SPECIAL_UNSIGNED_GTE:
 114  123                  return SPECIAL_UNSIGNED_LTE;
 115  124          case '>':
 116  125                  return '<';
 117  126          case SPECIAL_UNSIGNED_GT:
 118  127                  return SPECIAL_UNSIGNED_LT;
      128 +        case IMPOSSIBLE_COMPARISON:
      129 +                return UNKNOWN_COMPARISON;
 119  130          default:
 120  131                  sm_perror("unhandled comparison %d", op);
 121  132                  return op;
 122  133          }
 123  134  }
 124  135  
 125  136  int negate_comparison(int op)
 126  137  {
 127  138          switch (op) {
 128      -        case 0:
 129      -                return 0;
      139 +        case UNKNOWN_COMPARISON:
      140 +                return UNKNOWN_COMPARISON;
 130  141          case '<':
 131  142                  return SPECIAL_GTE;
 132  143          case SPECIAL_UNSIGNED_LT:
 133  144                  return SPECIAL_UNSIGNED_GTE;
 134  145          case SPECIAL_LTE:
 135  146                  return '>';
 136  147          case SPECIAL_UNSIGNED_LTE:
 137  148                  return SPECIAL_UNSIGNED_GT;
 138  149          case SPECIAL_EQUAL:
 139  150                  return SPECIAL_NOTEQUAL;
 140  151          case SPECIAL_NOTEQUAL:
 141  152                  return SPECIAL_EQUAL;
 142  153          case SPECIAL_GTE:
 143  154                  return '<';
 144  155          case SPECIAL_UNSIGNED_GTE:
 145  156                  return SPECIAL_UNSIGNED_LT;
 146  157          case '>':
 147  158                  return SPECIAL_LTE;
 148  159          case SPECIAL_UNSIGNED_GT:
 149  160                  return SPECIAL_UNSIGNED_LTE;
      161 +        case IMPOSSIBLE_COMPARISON:
      162 +                return UNKNOWN_COMPARISON;
 150  163          default:
 151  164                  sm_perror("unhandled comparison %d", op);
 152  165                  return op;
 153  166          }
 154  167  }
 155  168  
 156  169  static int rl_comparison(struct range_list *left_rl, struct range_list *right_rl)
 157  170  {
 158  171          sval_t left_min, left_max, right_min, right_max;
 159  172          struct symbol *type = &int_ctype;
 160  173  
 161  174          if (!left_rl || !right_rl)
 162      -                return 0;
      175 +                return UNKNOWN_COMPARISON;
 163  176  
 164  177          if (type_positive_bits(rl_type(left_rl)) > type_positive_bits(type))
 165  178                  type = rl_type(left_rl);
 166  179          if (type_positive_bits(rl_type(right_rl)) > type_positive_bits(type))
 167  180                  type = rl_type(right_rl);
 168  181  
 169  182          left_rl = cast_rl(type, left_rl);
 170  183          right_rl = cast_rl(type, right_rl);
 171  184  
 172  185          left_min = rl_min(left_rl);
↓ open down ↓ 8 lines elided ↑ open up ↑
 181  194  
 182  195          if (sval_cmp(left_max, right_min) < 0)
 183  196                  return '<';
 184  197          if (sval_cmp(left_max, right_min) == 0)
 185  198                  return SPECIAL_LTE;
 186  199          if (sval_cmp(left_min, right_max) > 0)
 187  200                  return '>';
 188  201          if (sval_cmp(left_min, right_max) == 0)
 189  202                  return SPECIAL_GTE;
 190  203  
 191      -        return 0;
      204 +        return UNKNOWN_COMPARISON;
 192  205  }
 193  206  
 194  207  static int comparison_from_extra(struct expression *a, struct expression *b)
 195  208  {
 196  209          struct range_list *left, *right;
 197  210  
 198  211          if (!get_implied_rl(a, &left))
 199      -                return 0;
      212 +                return UNKNOWN_COMPARISON;
 200  213          if (!get_implied_rl(b, &right))
 201      -                return 0;
      214 +                return UNKNOWN_COMPARISON;
 202  215  
 203  216          return rl_comparison(left, right);
 204  217  }
 205  218  
 206  219  static struct range_list *get_orig_rl(struct var_sym_list *vsl)
 207  220  {
 208  221          struct symbol *sym;
 209  222          struct smatch_state *state;
 210  223  
 211  224          if (!vsl)
↓ open down ↓ 2 lines elided ↑ open up ↑
 214  227          if (!sym || !sym->ident)
 215  228                  return NULL;
 216  229          state = get_orig_estate(sym->ident->name, sym);
 217  230          return estate_rl(state);
 218  231  }
 219  232  
 220  233  static struct smatch_state *unmatched_comparison(struct sm_state *sm)
 221  234  {
 222  235          struct compare_data *data = sm->state->data;
 223  236          struct range_list *left_rl, *right_rl;
 224      -        int op;
      237 +        int op = UNKNOWN_COMPARISON;
 225  238  
 226  239          if (!data)
 227  240                  return &undefined;
 228  241  
      242 +        if (is_impossible_path()) {
      243 +                op = IMPOSSIBLE_COMPARISON;
      244 +                goto alloc;
      245 +        }
      246 +
 229  247          if (strstr(data->left_var, " orig"))
 230  248                  left_rl = get_orig_rl(data->left_vsl);
 231  249          else if (!get_implied_rl_var_sym(data->left_var, vsl_to_sym(data->left_vsl), &left_rl))
 232      -                return &undefined;
      250 +                goto alloc;
 233  251  
 234  252          if (strstr(data->right_var, " orig"))
 235  253                  right_rl = get_orig_rl(data->right_vsl);
 236  254          else if (!get_implied_rl_var_sym(data->right_var, vsl_to_sym(data->right_vsl), &right_rl))
 237      -                return &undefined;
      255 +                goto alloc;
 238  256  
 239  257          op = rl_comparison(left_rl, right_rl);
 240      -        if (op)
 241      -                return alloc_compare_state(
 242      -                                data->left, data->left_var, data->left_vsl,
 243      -                                op,
 244      -                                data->right, data->right_var, data->right_vsl);
 245  258  
 246      -        return &undefined;
      259 +alloc:
      260 +        return alloc_compare_state(data->left, data->left_var, data->left_vsl,
      261 +                                   op,
      262 +                                   data->right, data->right_var, data->right_vsl);
 247  263  }
 248  264  
 249  265  /* remove_unsigned_from_comparison() is obviously a hack. */
 250  266  int remove_unsigned_from_comparison(int op)
 251  267  {
 252  268          switch (op) {
 253  269          case SPECIAL_UNSIGNED_LT:
 254  270                  return '<';
 255  271          case SPECIAL_UNSIGNED_LTE:
 256  272                  return SPECIAL_LTE;
↓ open down ↓ 7 lines elided ↑ open up ↑
 264  280  }
 265  281  
 266  282  /*
 267  283   * This is for when you merge states "a < b" and "a == b", the result is that
 268  284   * we can say for sure, "a <= b" after the merge.
 269  285   */
 270  286  int merge_comparisons(int one, int two)
 271  287  {
 272  288          int LT, EQ, GT;
 273  289  
 274      -        if (!one || !two)
 275      -                return 0;
      290 +        if (one == UNKNOWN_COMPARISON || two == UNKNOWN_COMPARISON)
      291 +                return UNKNOWN_COMPARISON;
 276  292  
      293 +        if (one == IMPOSSIBLE_COMPARISON)
      294 +                return two;
      295 +        if (two == IMPOSSIBLE_COMPARISON)
      296 +                return one;
      297 +
 277  298          one = remove_unsigned_from_comparison(one);
 278  299          two = remove_unsigned_from_comparison(two);
 279  300  
 280  301          if (one == two)
 281  302                  return one;
 282  303  
 283  304          LT = EQ = GT = 0;
 284  305  
 285  306          switch (one) {
 286  307          case '<':
↓ open down ↓ 27 lines elided ↑ open up ↑
 314  335                  break;
 315  336          case SPECIAL_GTE:
 316  337                  GT = 1;
 317  338                  EQ = 1;
 318  339                  break;
 319  340          case '>':
 320  341                  GT = 1;
 321  342          }
 322  343  
 323  344          if (LT && EQ && GT)
 324      -                return 0;
      345 +                return UNKNOWN_COMPARISON;
 325  346          if (LT && EQ)
 326  347                  return SPECIAL_LTE;
 327  348          if (LT && GT)
 328  349                  return SPECIAL_NOTEQUAL;
 329  350          if (LT)
 330  351                  return '<';
 331  352          if (EQ && GT)
 332  353                  return SPECIAL_GTE;
 333  354          if (GT)
 334  355                  return '>';
 335      -        return 0;
      356 +        return UNKNOWN_COMPARISON;
 336  357  }
 337  358  
 338  359  /*
 339      - * This is for if you have "a < b" and "b <= c".  Or in other words,
 340      - * "a < b <= c".  You would call this like get_combined_comparison('<', '<=').
      360 + * This is for if you have "a < b" and "b <= c" and you want to see how "a
      361 + * compares to c".  You would call this like get_combined_comparison('<', '<=').
 341  362   * The return comparison would be '<'.
 342      - *
 343      - * This function is different from merge_comparisons(), for example:
 344      - * merge_comparison('<', '==') returns '<='
 345      - * get_combined_comparison('<', '==') returns '<'
 346  363   */
 347  364  int combine_comparisons(int left_compare, int right_compare)
 348  365  {
 349  366          int LT, EQ, GT;
 350  367  
 351  368          left_compare = remove_unsigned_from_comparison(left_compare);
 352  369          right_compare = remove_unsigned_from_comparison(right_compare);
 353  370  
 354  371          LT = EQ = GT = 0;
 355  372  
↓ open down ↓ 37 lines elided ↑ open up ↑
 393  410                  if (EQ == 2)
 394  411                          return SPECIAL_LTE;
 395  412                  return '<';
 396  413          }
 397  414  
 398  415          if (GT == 2) {
 399  416                  if (EQ == 2)
 400  417                          return SPECIAL_GTE;
 401  418                  return '>';
 402  419          }
 403      -        return 0;
      420 +        return UNKNOWN_COMPARISON;
 404  421  }
 405  422  
 406      -int filter_comparison(int orig, int op)
      423 +/*
      424 + * This is mostly used when you know from extra state that a <= b but you
      425 + * know from comparisons that a != b so then if take the intersection then
      426 + * we know that a < b.  The name is taken from the fact that the intersection
      427 + * of < and <= is <.
      428 + */
      429 +int comparison_intersection(int left_compare, int right_compare)
 407  430  {
 408      -        if (orig == op)
 409      -                return orig;
      431 +        int LT, GT, EQ, NE, total;
 410  432  
 411      -        orig = remove_unsigned_from_comparison(orig);
 412      -        op = remove_unsigned_from_comparison(op);
      433 +        if (left_compare == IMPOSSIBLE_COMPARISON ||
      434 +            right_compare == IMPOSSIBLE_COMPARISON)
      435 +                return IMPOSSIBLE_COMPARISON;
 413  436  
 414      -        switch (orig) {
 415      -        case 0:
 416      -                return op;
      437 +        left_compare = remove_unsigned_from_comparison(left_compare);
      438 +        right_compare = remove_unsigned_from_comparison(right_compare);
      439 +
      440 +        LT = GT = EQ = NE = total = 0;
      441 +
      442 +        /* Only one side is known. */
      443 +        if (!left_compare)
      444 +                return right_compare;
      445 +        if (!right_compare)
      446 +                return left_compare;
      447 +
      448 +        switch (left_compare) {
 417  449          case '<':
 418      -                switch (op) {
 419      -                case '<':
 420      -                case SPECIAL_LTE:
 421      -                case SPECIAL_NOTEQUAL:
 422      -                        return '<';
 423      -                }
 424      -                return 0;
      450 +                LT++;
      451 +                total += 1;
      452 +                break;
 425  453          case SPECIAL_LTE:
 426      -                switch (op) {
 427      -                case '<':
 428      -                case SPECIAL_LTE:
 429      -                case SPECIAL_EQUAL:
 430      -                        return op;
 431      -                case SPECIAL_NOTEQUAL:
 432      -                        return '<';
 433      -                }
 434      -                return 0;
      454 +                LT++;
      455 +                EQ++;
      456 +                total += 2;
      457 +                break;
 435  458          case SPECIAL_EQUAL:
 436      -                switch (op) {
 437      -                case SPECIAL_LTE:
 438      -                case SPECIAL_EQUAL:
 439      -                case SPECIAL_GTE:
 440      -                case SPECIAL_UNSIGNED_LTE:
 441      -                case SPECIAL_UNSIGNED_GTE:
 442      -                        return SPECIAL_EQUAL;
 443      -                }
 444      -                return 0;
      459 +                EQ++;
      460 +                total += 1;
      461 +                break;
 445  462          case SPECIAL_NOTEQUAL:
 446      -                switch (op) {
 447      -                case '<':
 448      -                case SPECIAL_LTE:
 449      -                        return '<';
 450      -                case SPECIAL_UNSIGNED_LT:
 451      -                case SPECIAL_UNSIGNED_LTE:
 452      -                        return SPECIAL_UNSIGNED_LT;
 453      -                case SPECIAL_NOTEQUAL:
 454      -                        return op;
 455      -                case '>':
 456      -                case SPECIAL_GTE:
 457      -                        return '>';
 458      -                case SPECIAL_UNSIGNED_GT:
 459      -                case SPECIAL_UNSIGNED_GTE:
 460      -                        return SPECIAL_UNSIGNED_GT;
 461      -                }
 462      -                return 0;
      463 +                NE++;
      464 +                total += 1;
      465 +                break;
 463  466          case SPECIAL_GTE:
 464      -                switch (op) {
 465      -                case SPECIAL_LTE:
 466      -                        return SPECIAL_EQUAL;
 467      -                case '>':
 468      -                case SPECIAL_GTE:
 469      -                case SPECIAL_EQUAL:
 470      -                        return op;
 471      -                case SPECIAL_NOTEQUAL:
 472      -                        return '>';
 473      -                }
 474      -                return 0;
      467 +                GT++;
      468 +                EQ++;
      469 +                total += 2;
      470 +                break;
 475  471          case '>':
 476      -                switch (op) {
 477      -                case '>':
 478      -                case SPECIAL_GTE:
 479      -                case SPECIAL_NOTEQUAL:
 480      -                        return '>';
 481      -                }
 482      -                return 0;
 483      -        case SPECIAL_UNSIGNED_LT:
 484      -                switch (op) {
 485      -                case SPECIAL_UNSIGNED_LT:
 486      -                case SPECIAL_UNSIGNED_LTE:
 487      -                case SPECIAL_NOTEQUAL:
 488      -                        return SPECIAL_UNSIGNED_LT;
 489      -                }
 490      -                return 0;
 491      -        case SPECIAL_UNSIGNED_LTE:
 492      -                switch (op) {
 493      -                case SPECIAL_UNSIGNED_LT:
 494      -                case SPECIAL_UNSIGNED_LTE:
 495      -                case SPECIAL_EQUAL:
 496      -                        return op;
 497      -                case SPECIAL_NOTEQUAL:
 498      -                        return SPECIAL_UNSIGNED_LT;
 499      -                case SPECIAL_UNSIGNED_GTE:
 500      -                        return SPECIAL_EQUAL;
 501      -                }
 502      -                return 0;
 503      -        case SPECIAL_UNSIGNED_GTE:
 504      -                switch (op) {
 505      -                case SPECIAL_UNSIGNED_LTE:
 506      -                        return SPECIAL_EQUAL;
 507      -                case SPECIAL_NOTEQUAL:
 508      -                        return SPECIAL_UNSIGNED_GT;
 509      -                case SPECIAL_EQUAL:
 510      -                case SPECIAL_UNSIGNED_GTE:
 511      -                case SPECIAL_UNSIGNED_GT:
 512      -                        return op;
 513      -                }
 514      -                return 0;
 515      -        case SPECIAL_UNSIGNED_GT:
 516      -                switch (op) {
 517      -                case SPECIAL_UNSIGNED_GT:
 518      -                case SPECIAL_UNSIGNED_GTE:
 519      -                case SPECIAL_NOTEQUAL:
 520      -                        return SPECIAL_UNSIGNED_GT;
 521      -                }
 522      -                return 0;
      472 +                GT++;
      473 +                total += 1;
      474 +                break;
      475 +        default:
      476 +                return UNKNOWN_COMPARISON;
 523  477          }
 524      -        return 0;
      478 +
      479 +        switch (right_compare) {
      480 +        case '<':
      481 +                LT++;
      482 +                total += 1;
      483 +                break;
      484 +        case SPECIAL_LTE:
      485 +                LT++;
      486 +                EQ++;
      487 +                total += 2;
      488 +                break;
      489 +        case SPECIAL_EQUAL:
      490 +                EQ++;
      491 +                total += 1;
      492 +                break;
      493 +        case SPECIAL_NOTEQUAL:
      494 +                NE++;
      495 +                total += 1;
      496 +                break;
      497 +        case SPECIAL_GTE:
      498 +                GT++;
      499 +                EQ++;
      500 +                total += 2;
      501 +                break;
      502 +        case '>':
      503 +                GT++;
      504 +                total += 1;
      505 +                break;
      506 +        default:
      507 +                return UNKNOWN_COMPARISON;
      508 +        }
      509 +
      510 +        if (LT == 2) {
      511 +                if (EQ == 2)
      512 +                        return SPECIAL_LTE;
      513 +                return '<';
      514 +        }
      515 +
      516 +        if (GT == 2) {
      517 +                if (EQ == 2)
      518 +                        return SPECIAL_GTE;
      519 +                return '>';
      520 +        }
      521 +        if (EQ == 2)
      522 +                return SPECIAL_EQUAL;
      523 +        if (total == 2 && EQ && NE)
      524 +                return IMPOSSIBLE_COMPARISON;
      525 +        if (GT && LT)
      526 +                return IMPOSSIBLE_COMPARISON;
      527 +        if (GT && NE)
      528 +                return '>';
      529 +        if (LT && NE)
      530 +                return '<';
      531 +        if (NE == 2)
      532 +                return SPECIAL_NOTEQUAL;
      533 +        if (total == 2 && (LT || GT) && EQ)
      534 +                return IMPOSSIBLE_COMPARISON;
      535 +
      536 +        return UNKNOWN_COMPARISON;
 525  537  }
 526  538  
 527      -static void pre_merge_hook(struct sm_state *sm)
      539 +static void pre_merge_hook(struct sm_state *cur, struct sm_state *other)
 528  540  {
 529      -        struct compare_data *data = sm->state->data;
 530      -        int other;
      541 +        struct compare_data *data = cur->state->data;
      542 +        int extra, new;
      543 +        static bool in_recurse;
 531  544  
 532  545          if (!data)
 533  546                  return;
 534      -        other = get_comparison(data->left, data->right);
 535      -        if (!other)
      547 +
      548 +        if (in_recurse)
 536  549                  return;
      550 +        in_recurse = true;
      551 +        extra = comparison_from_extra(data->left, data->right);
      552 +        in_recurse = false;
      553 +        if (!extra)
      554 +                return;
      555 +        new = comparison_intersection(extra, data->comparison);
      556 +        if (new == data->comparison)
      557 +                return;
 537  558  
 538      -        set_state(compare_id, sm->name, NULL,
      559 +        set_state(compare_id, cur->name, NULL,
 539  560                    alloc_compare_state(data->left, data->left_var, data->left_vsl,
 540      -                                      other,
      561 +                                      new,
 541  562                                        data->right, data->right_var, data->right_vsl));
 542  563  }
 543  564  
 544  565  struct smatch_state *merge_compare_states(struct smatch_state *s1, struct smatch_state *s2)
 545  566  {
 546  567          struct compare_data *data = s1->data;
 547  568          int op;
 548  569  
      570 +        if (!data)
      571 +                return &undefined;
      572 +
 549  573          op = merge_comparisons(state_to_comparison(s1), state_to_comparison(s2));
 550      -        if (op)
 551      -                return alloc_compare_state(
 552      -                                data->left, data->left_var, data->left_vsl,
 553      -                                op,
 554      -                                data->right, data->right_var, data->right_vsl);
 555      -        return &undefined;
      574 +        return alloc_compare_state(
      575 +                        data->left, data->left_var, data->left_vsl,
      576 +                        op,
      577 +                        data->right, data->right_var, data->right_vsl);
 556  578  }
 557  579  
 558  580  static struct smatch_state *alloc_link_state(struct string_list *links)
 559  581  {
 560  582          struct smatch_state *state;
 561  583          static char buf[256];
 562  584          char *tmp;
 563  585          int i;
 564  586  
 565  587          state = __alloc_smatch_state(0);
↓ open down ↓ 117 lines elided ↑ open up ↑
 683  705                          break;
 684  706                  case '<':
 685  707                  case SPECIAL_UNSIGNED_LT:
 686  708                          new = alloc_compare_state(
 687  709                                          data->left, data->left_var, data->left_vsl,
 688  710                                          flip ? SPECIAL_GTE : SPECIAL_LTE,
 689  711                                          data->right, data->right_var, data->right_vsl);
 690  712                          set_state(compare_id, tmp, NULL, new);
 691  713                          break;
 692  714                  default:
 693      -                        set_state(compare_id, tmp, NULL, &undefined);
      715 +                        new = alloc_compare_state(
      716 +                                        data->left, data->left_var, data->left_vsl,
      717 +                                        UNKNOWN_COMPARISON,
      718 +                                        data->right, data->right_var, data->right_vsl);
      719 +                        set_state(compare_id, tmp, NULL, new);
 694  720                  }
 695  721          } END_FOR_EACH_PTR(tmp);
 696  722  }
 697  723  
 698  724  static void match_dec(struct sm_state *sm, bool preserve)
 699  725  {
 700  726          struct string_list *links;
 701  727          struct smatch_state *state;
 702  728          char *tmp;
 703  729  
 704  730          links = sm->state->data;
 705  731  
 706  732          FOR_EACH_PTR(links, tmp) {
      733 +                struct compare_data *data;
      734 +                struct smatch_state *new;
      735 +
 707  736                  state = get_state(compare_id, tmp, NULL);
      737 +                if (!state || !state->data)
      738 +                        continue;
 708  739  
      740 +                data = state->data;
      741 +
 709  742                  switch (state_to_comparison(state)) {
 710  743                  case SPECIAL_EQUAL:
 711  744                  case SPECIAL_LTE:
 712  745                  case SPECIAL_UNSIGNED_LTE:
 713  746                  case '<':
 714  747                  case SPECIAL_UNSIGNED_LT: {
 715      -                        struct compare_data *data = state->data;
 716      -                        struct smatch_state *new;
 717      -
 718  748                          if (preserve)
 719  749                                  break;
 720  750  
 721  751                          new = alloc_compare_state(
 722  752                                          data->left, data->left_var, data->left_vsl,
 723  753                                          '<',
 724  754                                          data->right, data->right_var, data->right_vsl);
 725  755                          set_state(compare_id, tmp, NULL, new);
 726  756                          break;
 727  757                          }
 728  758                  default:
 729      -                        set_state(compare_id, tmp, NULL, &undefined);
      759 +                        new = alloc_compare_state(
      760 +                                        data->left, data->left_var, data->left_vsl,
      761 +                                        UNKNOWN_COMPARISON,
      762 +                                        data->right, data->right_var, data->right_vsl);
      763 +                        set_state(compare_id, tmp, NULL, new);
 730  764                  }
 731  765          } END_FOR_EACH_PTR(tmp);
 732  766  }
 733  767  
 734  768  static void reset_sm(struct sm_state *sm)
 735  769  {
 736  770          struct string_list *links;
 737  771          char *tmp;
 738  772  
 739  773          links = sm->state->data;
 740  774  
 741  775          FOR_EACH_PTR(links, tmp) {
 742      -                set_state(compare_id, tmp, NULL, &undefined);
      776 +                struct smatch_state *old, *new;
      777 +
      778 +                old = get_state(compare_id, tmp, NULL);
      779 +                if (!old || !old->data) {
      780 +                        new = &undefined;
      781 +                } else {
      782 +                        struct compare_data *data = old->data;
      783 +
      784 +                        new = alloc_compare_state(
      785 +                                        data->left, data->left_var, data->left_vsl,
      786 +                                        UNKNOWN_COMPARISON,
      787 +                                        data->right, data->right_var, data->right_vsl);
      788 +                }
      789 +                set_state(compare_id, tmp, NULL, new);
 743  790          } END_FOR_EACH_PTR(tmp);
 744  791          set_state(link_id, sm->name, sm->sym, &undefined);
 745  792  }
 746  793  
 747  794  static bool match_add_sub_assign(struct sm_state *sm, struct expression *expr)
 748  795  {
 749  796          struct range_list *rl;
 750  797          sval_t zero = { .type = &int_ctype };
 751  798  
 752  799          if (!expr || expr->type != EXPR_ASSIGNMENT)
↓ open down ↓ 89 lines elided ↑ open up ↑
 842  889          if (parent->type != EXPR_COMPARE || parent->op != SPECIAL_EQUAL)
 843  890                  return;
 844  891          if (parent->left != expr)
 845  892                  return;
 846  893  
 847  894          if (!get_implied_rl(expr->unop, &left) ||
 848  895             !get_implied_rl(parent->right, &right))
 849  896                  return;
 850  897  
 851  898          op = rl_comparison(left, right);
 852      -        if (!op)
      899 +        if (op == UNKNOWN_COMPARISON)
 853  900                  return;
 854  901  
 855  902          add_comparison(expr->unop, op, parent->right);
 856  903  }
 857  904  
 858  905  static char *chunk_to_var_sym(struct expression *expr, struct symbol **sym)
 859  906  {
 860  907          expr = strip_expr(expr);
 861  908          if (!expr)
 862  909                  return NULL;
↓ open down ↓ 146 lines elided ↑ open up ↑
1009 1056                          right_comparison = flip_comparison(right_comparison);
1010 1057                  }
1011 1058                  if (have_common_var_sym(left_vsl, right_vsl))
1012 1059                          continue;
1013 1060  
1014 1061                  orig_comparison = get_orig_comparison(pre_stree, left_var, right_var);
1015 1062  
1016 1063                  true_comparison = combine_comparisons(left_comparison, right_comparison);
1017 1064                  false_comparison = combine_comparisons(left_false_comparison, right_comparison);
1018 1065  
1019      -                true_comparison = filter_comparison(orig_comparison, true_comparison);
1020      -                false_comparison = filter_comparison(orig_comparison, false_comparison);
     1066 +                true_comparison = comparison_intersection(orig_comparison, true_comparison);
     1067 +                false_comparison = comparison_intersection(orig_comparison, false_comparison);
1021 1068  
1022 1069                  if (strcmp(left_var, right_var) > 0) {
1023 1070                          struct expression *tmp_expr = left_expr;
1024 1071                          const char *tmp_var = left_var;
1025 1072                          struct var_sym_list *tmp_vsl = left_vsl;
1026 1073  
1027 1074                          left_expr = right_expr;
1028 1075                          left_var = right_var;
1029 1076                          left_vsl = right_vsl;
1030 1077                          right_expr = tmp_expr;
↓ open down ↓ 238 lines elided ↑ open up ↑
1269 1316                  left_vsl = right_vsl;
1270 1317                  left_expr = right_expr;
1271 1318                  right = tmp_name;
1272 1319                  right_vsl = tmp_vsl;
1273 1320                  right_expr = tmp_expr;
1274 1321                  op = flip_comparison(op);
1275 1322                  false_op = flip_comparison(false_op);
1276 1323          }
1277 1324  
1278 1325          orig_comparison = get_comparison(left_expr, right_expr);
1279      -        op = filter_comparison(orig_comparison, op);
1280      -        false_op = filter_comparison(orig_comparison, false_op);
     1326 +        op = comparison_intersection(orig_comparison, op);
     1327 +        false_op = comparison_intersection(orig_comparison, false_op);
1281 1328  
1282 1329          snprintf(state_name, sizeof(state_name), "%s vs %s", left, right);
1283 1330          true_state = alloc_compare_state(
1284 1331                          left_expr, left, left_vsl,
1285 1332                          op,
1286 1333                          right_expr, right, right_vsl);
1287 1334          false_state = alloc_compare_state(
1288 1335                          left_expr, left, left_vsl,
1289 1336                          false_op,
1290 1337                          right_expr, right, right_vsl);
↓ open down ↓ 36 lines elided ↑ open up ↑
1327 1374          if (left->type == EXPR_BINOP && left->op == '+') {
1328 1375                  new_left = left->left;
1329 1376                  new_right = binop_expression(right, '-', left->right);
1330 1377                  handle_comparison(new_left, expr->op, new_right, NULL, NULL);
1331 1378  
1332 1379                  new_left = left->right;
1333 1380                  new_right = binop_expression(right, '-', left->left);
1334 1381                  handle_comparison(new_left, expr->op, new_right, NULL, NULL);
1335 1382          }
1336 1383  
1337      -
1338 1384          redo = 0;
1339 1385          left = strip_parens(expr->left);
1340 1386          right = strip_parens(expr->right);
1341 1387          if (get_last_expr_from_expression_stmt(expr->left)) {
1342 1388                  left = get_last_expr_from_expression_stmt(expr->left);
1343 1389                  redo = 1;
1344 1390          }
1345 1391          if (get_last_expr_from_expression_stmt(expr->right)) {
1346 1392                  right = get_last_expr_from_expression_stmt(expr->right);
1347 1393                  redo = 1;
↓ open down ↓ 263 lines elided ↑ open up ↑
1611 1657  }
1612 1658  
1613 1659  int get_comparison_strings(const char *one, const char *two)
1614 1660  {
1615 1661          char buf[256];
1616 1662          struct smatch_state *state;
1617 1663          int invert = 0;
1618 1664          int ret = 0;
1619 1665  
1620 1666          if (!one || !two)
1621      -                return 0;
     1667 +                return UNKNOWN_COMPARISON;
1622 1668  
1623 1669          if (strcmp(one, two) == 0)
1624 1670                  return SPECIAL_EQUAL;
1625 1671  
1626 1672          if (strcmp(one, two) > 0) {
1627 1673                  const char *tmp = one;
1628 1674  
1629 1675                  one = two;
1630 1676                  two = tmp;
1631 1677                  invert = 1;
↓ open down ↓ 7 lines elided ↑ open up ↑
1639 1685          if (invert)
1640 1686                  ret = flip_comparison(ret);
1641 1687  
1642 1688          return ret;
1643 1689  }
1644 1690  
1645 1691  static int get_comparison_helper(struct expression *a, struct expression *b, bool use_extra)
1646 1692  {
1647 1693          char *one = NULL;
1648 1694          char *two = NULL;
1649      -        int ret = 0;
     1695 +        int ret = UNKNOWN_COMPARISON;
     1696 +        int extra = UNKNOWN_COMPARISON;
1650 1697  
1651      -        if (!a || !b)
1652      -                return 0;
     1698 +        if (a == UNKNOWN_COMPARISON ||
     1699 +            b == UNKNOWN_COMPARISON)
     1700 +                return UNKNOWN_COMPARISON;
1653 1701  
1654 1702          a = strip_parens(a);
1655 1703          b = strip_parens(b);
1656 1704  
1657 1705          move_plus_to_minus(&a, &b);
1658 1706  
1659 1707          one = chunk_to_var(a);
1660 1708          if (!one)
1661 1709                  goto free;
1662 1710          two = chunk_to_var(b);
↓ open down ↓ 7 lines elided ↑ open up ↑
1670 1718          if (is_plus_one(a) || is_minus_one(a)) {
1671 1719                  free_string(one);
1672 1720                  one = chunk_to_var(a->left);
1673 1721                  ret = get_comparison_strings(one, two);
1674 1722          } else if (is_plus_one(b) || is_minus_one(b)) {
1675 1723                  free_string(two);
1676 1724                  two = chunk_to_var(b->left);
1677 1725                  ret = get_comparison_strings(one, two);
1678 1726          }
1679 1727  
1680      -        if (!ret)
     1728 +        if (ret == UNKNOWN_COMPARISON)
1681 1729                  goto free;
1682 1730  
1683 1731          if ((is_plus_one(a) || is_minus_one(b)) && ret == '<')
1684 1732                  ret = SPECIAL_LTE;
1685 1733          else if ((is_minus_one(a) || is_plus_one(b)) && ret == '>')
1686 1734                  ret = SPECIAL_GTE;
1687 1735          else
1688      -                ret = 0;
     1736 +                ret = UNKNOWN_COMPARISON;
1689 1737  
1690 1738  free:
1691 1739          free_string(one);
1692 1740          free_string(two);
1693 1741  
1694      -        if (!ret && use_extra)
1695      -                return comparison_from_extra(a, b);
1696      -        return ret;
     1742 +        extra = comparison_from_extra(a, b);
     1743 +        return comparison_intersection(ret, extra);
1697 1744  }
1698 1745  
1699 1746  int get_comparison(struct expression *a, struct expression *b)
1700 1747  {
1701 1748          return get_comparison_helper(a, b, true);
1702 1749  }
1703 1750  
1704 1751  int get_comparison_no_extra(struct expression *a, struct expression *b)
1705 1752  {
1706 1753          return get_comparison_helper(a, b, false);
↓ open down ↓ 191 lines elided ↑ open up ↑
1898 1945          } END_FOR_EACH_PTR(tmp);
1899 1946  
1900 1947  done:
1901 1948          free_string(right_var);
1902 1949  }
1903 1950  
1904 1951  void __add_return_comparison(struct expression *call, const char *range)
1905 1952  {
1906 1953          struct expression *arg;
1907 1954          int comparison;
1908      -        char buf[4];
     1955 +        char buf[16];
1909 1956  
1910 1957          if (!str_to_comparison_arg(range, call, &comparison, &arg))
1911 1958                  return;
1912      -        snprintf(buf, sizeof(buf), "%s", show_special(comparison));
     1959 +        snprintf(buf, sizeof(buf), "%s", show_comparison(comparison));
1913 1960          update_links_from_call(call, comparison, arg);
1914 1961          add_comparison(call, comparison, arg);
1915 1962  }
1916 1963  
1917 1964  void __add_comparison_info(struct expression *expr, struct expression *call, const char *range)
1918 1965  {
1919 1966          copy_comparisons(expr, call);
1920 1967  }
1921 1968  
1922 1969  static char *get_mask_comparison(struct expression *expr, int ignore)
↓ open down ↓ 41 lines elided ↑ open up ↑
1964 2011  
1965 2012          i = -1;
1966 2013          FOR_EACH_PTR(cur_func_sym->ctype.base_type->arguments, param) {
1967 2014                  i++;
1968 2015                  if (i == ignore)
1969 2016                          continue;
1970 2017                  if (!param->ident)
1971 2018                          continue;
1972 2019                  snprintf(buf, sizeof(buf), "%s orig", param->ident->name);
1973 2020                  compare = get_comparison_strings(var, buf);
1974      -                if (!compare)
     2021 +                if (compare == UNKNOWN_COMPARISON ||
     2022 +                    compare == IMPOSSIBLE_COMPARISON)
1975 2023                          continue;
1976      -                if (show_special(compare)[0] != starts_with)
     2024 +                if (show_comparison(compare)[0] != starts_with)
1977 2025                          continue;
1978      -                snprintf(buf, sizeof(buf), "[%s$%d]", show_special(compare), i);
     2026 +                snprintf(buf, sizeof(buf), "[%s$%d]", show_comparison(compare), i);
1979 2027                  ret_str = alloc_sname(buf);
1980 2028                  break;
1981 2029          } END_FOR_EACH_PTR(param);
1982 2030  
1983 2031          free_string(var);
1984 2032          if (!ret_str)
1985 2033                  goto try_mask;
1986 2034  
1987 2035          return ret_str;
1988 2036  
↓ open down ↓ 10 lines elided ↑ open up ↑
1999 2047          int compare;
2000 2048          int i;
2001 2049  
2002 2050          i = -1;
2003 2051          FOR_EACH_PTR(cur_func_sym->ctype.base_type->arguments, param) {
2004 2052                  i++;
2005 2053                  if (!param->ident)
2006 2054                          continue;
2007 2055                  snprintf(buf, sizeof(buf), "%s orig", param->ident->name);
2008 2056                  compare = get_comparison_strings(name, buf);
2009      -                if (!compare)
     2057 +                if (compare == UNKNOWN_COMPARISON ||
     2058 +                    compare == IMPOSSIBLE_COMPARISON)
2010 2059                          continue;
2011      -                snprintf(buf, sizeof(buf), "[%s$%d]", show_special(compare), i);
     2060 +                snprintf(buf, sizeof(buf), "[%s$%d]", show_comparison(compare), i);
2012 2061                  return alloc_sname(buf);
2013 2062          } END_FOR_EACH_PTR(param);
2014 2063  
2015 2064          return NULL;
2016 2065  }
2017 2066  
2018 2067  char *expr_equal_to_param(struct expression *expr, int ignore)
2019 2068  {
2020 2069          return range_comparison_to_param_helper(expr, '=', ignore);
2021 2070  }
↓ open down ↓ 20 lines elided ↑ open up ↑
2042 2091          FOR_EACH_PTR(cur_func_sym->ctype.base_type->arguments, param) {
2043 2092                  i++;
2044 2093                  if (i == ignore)
2045 2094                          continue;
2046 2095                  if (!param->ident)
2047 2096                          continue;
2048 2097                  snprintf(buf, sizeof(buf), "%s orig", param->ident->name);
2049 2098                  compare = get_comparison_strings(var, buf);
2050 2099                  if (!compare)
2051 2100                          continue;
2052      -                snprintf(buf, sizeof(buf), "[%s$%d]", show_special(compare), i);
     2101 +                snprintf(buf, sizeof(buf), "[%s$%d]", show_comparison(compare), i);
2053 2102                  ret_str = alloc_sname(buf);
2054 2103                  break;
2055 2104          } END_FOR_EACH_PTR(param);
2056 2105  
2057 2106  free:
2058 2107          free_string(var);
2059 2108          return ret_str;
2060 2109  }
2061 2110  
2062 2111  char *get_printed_param_name(struct expression *call, const char *param_name, struct symbol *param_sym)
↓ open down ↓ 58 lines elided ↑ open up ↑
2121 2170                          struct var_sym_list *right_vsl;
2122 2171                          struct var_sym *right_vs;
2123 2172  
2124 2173  
2125 2174                          if (strstr(link, " orig"))
2126 2175                                  continue;
2127 2176                          sm = get_sm_state(compare_id, link, NULL);
2128 2177                          if (!sm)
2129 2178                                  continue;
2130 2179                          data = sm->state->data;
2131      -                        if (!data || !data->comparison)
     2180 +                        if (!data ||
     2181 +                            data->comparison == UNKNOWN_COMPARISON ||
     2182 +                            data->comparison == IMPOSSIBLE_COMPARISON)
2132 2183                                  continue;
2133 2184                          arg_name = expr_to_var(arg);
2134 2185                          if (!arg_name)
2135 2186                                  continue;
2136 2187  
2137 2188                          right_vsl = NULL;
2138 2189                          if (strcmp(data->left_var, arg_name) == 0) {
2139 2190                                  comparison = data->comparison;
2140 2191                                  right_name = data->right_var;
2141 2192                                  right_vsl = data->right_vsl;
↓ open down ↓ 4 lines elided ↑ open up ↑
2146 2197                          }
2147 2198                          if (!right_vsl || ptr_list_size((struct ptr_list *)right_vsl) != 1)
2148 2199                                  goto free;
2149 2200  
2150 2201                          right_vs = first_ptr_list((struct ptr_list *)right_vsl);
2151 2202                          if (strcmp(right_vs->var, right_name) != 0)
2152 2203                                  goto free;
2153 2204                          right_name = get_printed_param_name(expr, right_vs->var, right_vs->sym);
2154 2205                          if (!right_name)
2155 2206                                  goto free;
2156      -                        snprintf(info_buf, sizeof(info_buf), "%s %s", show_special(comparison), right_name);
     2207 +                        snprintf(info_buf, sizeof(info_buf), "%s %s", show_comparison(comparison), right_name);
2157 2208                          sql_insert_caller_info(expr, PARAM_COMPARE, i, "$", info_buf);
2158 2209  
2159 2210  free:
2160 2211                          free_string(arg_name);
2161 2212                  } END_FOR_EACH_PTR(link);
2162 2213          } END_FOR_EACH_PTR(arg);
2163 2214  }
2164 2215  
2165 2216  static void struct_member_callback(struct expression *call, int param, char *printed_name, struct sm_state *link_sm)
2166 2217  {
↓ open down ↓ 29 lines elided ↑ open up ↑
2196 2247                   * Both parameters link to this comparison so only
2197 2248                   * record the first one.
2198 2249                   */
2199 2250                  if (left->sym != link_sm->sym ||
2200 2251                      strcmp(left->var, link_sm->name) != 0)
2201 2252                          continue;
2202 2253  
2203 2254                  right_name = get_printed_param_name(call, right->var, right->sym);
2204 2255                  if (!right_name)
2205 2256                          continue;
2206      -                snprintf(info_buf, sizeof(info_buf), "%s %s", show_special(data->comparison), right_name);
     2257 +                snprintf(info_buf, sizeof(info_buf), "%s %s", show_comparison(data->comparison), right_name);
2207 2258                  sql_insert_caller_info(call, PARAM_COMPARE, param, printed_name, info_buf);
2208 2259          } END_FOR_EACH_PTR(link);
2209 2260  }
2210 2261  
2211 2262  static void print_return_value_comparison(int return_id, char *return_ranges, struct expression *expr)
2212 2263  {
2213 2264          char *name;
2214 2265          const char *tmp_name;
2215 2266          struct symbol *sym;
2216 2267          int param;
↓ open down ↓ 50 lines elided ↑ open up ↑
2267 2318  
2268 2319          FOR_EACH_MY_SM(link_id, __get_cur_stree(), tmp) {
2269 2320                  if (get_param_num_from_sym(tmp->sym) < 0)
2270 2321                          continue;
2271 2322                  links = tmp->state->data;
2272 2323                  FOR_EACH_PTR(links, link) {
2273 2324                          sm = get_sm_state(compare_id, link, NULL);
2274 2325                          if (!sm)
2275 2326                                  continue;
2276 2327                          data = sm->state->data;
2277      -                        if (!data || !data->comparison)
     2328 +                        if (!data ||
     2329 +                            data->comparison == UNKNOWN_COMPARISON ||
     2330 +                            data->comparison == IMPOSSIBLE_COMPARISON)
2278 2331                                  continue;
2279 2332                          if (ptr_list_size((struct ptr_list *)data->left_vsl) != 1 ||
2280 2333                              ptr_list_size((struct ptr_list *)data->right_vsl) != 1)
2281 2334                                  continue;
2282 2335                          left = first_ptr_list((struct ptr_list *)data->left_vsl);
2283 2336                          right = first_ptr_list((struct ptr_list *)data->right_vsl);
2284 2337                          if (left->sym == right->sym &&
2285 2338                              strcmp(left->var, right->var) == 0)
2286 2339                                  continue;
2287 2340                          /*
↓ open down ↓ 21 lines elided ↑ open up ↑
2309 2362                          if (!tmp_name || tmp_name[0] != '$')
2310 2363                                  continue;
2311 2364                          snprintf(right_buf, sizeof(right_buf), "$%d%s", right_param, tmp_name + 1);
2312 2365  
2313 2366                          /*
2314 2367                           * FIXME: this should reject $ type variables (as
2315 2368                           * opposed to $->foo type).  Those should come from
2316 2369                           * smatch_param_compare_limit.c.
2317 2370                           */
2318 2371  
2319      -                        snprintf(info_buf, sizeof(info_buf), "%s %s", show_special(data->comparison), right_buf);
     2372 +                        snprintf(info_buf, sizeof(info_buf), "%s %s", show_comparison(data->comparison), right_buf);
2320 2373                          sql_insert_return_states(return_id, return_ranges,
2321 2374                                          PARAM_COMPARE, left_param, left_buf, info_buf);
2322 2375                  } END_FOR_EACH_PTR(link);
2323 2376  
2324 2377          } END_FOR_EACH_SM(tmp);
2325 2378  }
2326 2379  
2327 2380  static int parse_comparison(char **value, int *op)
2328 2381  {
2329 2382  
↓ open down ↓ 156 lines elided ↑ open up ↑
2486 2539                  goto free;
2487 2540  
2488 2541          snprintf(buf, sizeof(buf), "%s vs %s", left_name, right_name);
2489 2542          state = get_state(compare_id, buf, NULL);
2490 2543          if (!state)
2491 2544                  goto free;
2492 2545          state_op = state_to_comparison(state);
2493 2546          if (!state_op)
2494 2547                  goto free;
2495 2548  
2496      -        if (!filter_comparison(remove_unsigned_from_comparison(state_op), op))
     2549 +        if (!comparison_intersection(remove_unsigned_from_comparison(state_op), op))
2497 2550                  ret = 1;
2498 2551  free:
2499 2552          free_string(left_name);
2500 2553          free_string(right_name);
2501 2554          return ret;
2502 2555  }
2503 2556  
2504 2557  int impossibly_high_comparison(struct expression *expr)
2505 2558  {
2506 2559          struct smatch_state *link_state;
↓ open down ↓ 77 lines elided ↑ open up ↑
2584 2637          inc_dec_link_id = id;
2585 2638          set_dynamic_states(inc_dec_link_id);
2586 2639          set_up_link_functions(inc_dec_id, inc_dec_link_id);
2587 2640  }
2588 2641  
2589 2642  static void filter_by_sm(struct sm_state *sm, int op,
2590 2643                         struct state_list **true_stack,
2591 2644                         struct state_list **false_stack)
2592 2645  {
2593 2646          struct compare_data *data;
2594      -        int istrue = 0;
2595      -        int isfalse = 0;
     2647 +        int is_true = 0;
     2648 +        int is_false = 0;
2596 2649  
2597 2650          if (!sm)
2598 2651                  return;
2599 2652          data = sm->state->data;
2600      -        if (!data) {
2601      -                if (sm->merged) {
2602      -                        filter_by_sm(sm->left, op, true_stack, false_stack);
2603      -                        filter_by_sm(sm->right, op, true_stack, false_stack);
2604      -                }
     2653 +        if (!data || data->comparison == UNKNOWN_COMPARISON)
     2654 +                goto split;
     2655 +        if (data->comparison == IMPOSSIBLE_COMPARISON)
2605 2656                  return;
2606      -        }
2607 2657  
2608      -        if (data->comparison &&
2609      -            data->comparison == filter_comparison(data->comparison, op))
2610      -                istrue = 1;
     2658 +        /*
     2659 +         * We want to check that "data->comparison" is totally inside "op".  So
     2660 +         * if data->comparison is < and op is <= then that's true.  Or if
     2661 +         * data->comparison is == and op is <= then that's true.  But if
     2662 +         * data->comparison is <= and op is < than that's neither true nor
     2663 +         * false.
     2664 +         */
     2665 +        if (data->comparison == comparison_intersection(data->comparison, op))
     2666 +                is_true = 1;
     2667 +        if (data->comparison == comparison_intersection(data->comparison, negate_comparison(op)))
     2668 +                is_false = 1;
2611 2669  
2612      -        if (data->comparison &&
2613      -            data->comparison == filter_comparison(data->comparison, negate_comparison(op)))
2614      -                isfalse = 1;
     2670 +        if (debug_implied()) {
     2671 +                sm_msg("%s: %s: op = '%s' negated '%s'. true_intersect = '%s' false_insersect = '%s' sm = '%s'",
     2672 +                       __func__,
     2673 +                       sm->state->name,
     2674 +                       alloc_sname(show_comparison(op)),
     2675 +                       alloc_sname(show_comparison(negate_comparison(op))),
     2676 +                       alloc_sname(show_comparison(comparison_intersection(data->comparison, op))),
     2677 +                       alloc_sname(show_comparison(comparison_intersection(data->comparison, negate_comparison(op)))),
     2678 +                       show_sm(sm));
     2679 +        }
2615 2680  
2616      -        if (istrue)
     2681 +        if (is_true)
2617 2682                  add_ptr_list(true_stack, sm);
2618      -        if (isfalse)
     2683 +        if (is_false)
2619 2684                  add_ptr_list(false_stack, sm);
2620      -
2621      -        if (sm->merged) {
2622      -                filter_by_sm(sm->left, op, true_stack, false_stack);
2623      -                filter_by_sm(sm->right, op, true_stack, false_stack);
2624      -        }
     2685 +split:
     2686 +        filter_by_sm(sm->left, op, true_stack, false_stack);
     2687 +        filter_by_sm(sm->right, op, true_stack, false_stack);
2625 2688  }
2626 2689  
2627 2690  struct sm_state *comparison_implication_hook(struct expression *expr,
2628 2691                                  struct state_list **true_stack,
2629 2692                                  struct state_list **false_stack)
2630 2693  {
2631 2694          struct sm_state *sm;
2632 2695          char *left, *right;
2633 2696          int op;
2634 2697          static char buf[256];
↓ open down ↓ 23 lines elided ↑ open up ↑
2658 2721          sm = get_sm_state(compare_id, buf, NULL);
2659 2722          if (!sm)
2660 2723                  return NULL;
2661 2724          if (!sm->merged)
2662 2725                  return NULL;
2663 2726  
2664 2727          filter_by_sm(sm, op, true_stack, false_stack);
2665 2728          if (!*true_stack && !*false_stack)
2666 2729                  return NULL;
2667 2730  
2668      -        if (option_debug)
     2731 +        if (debug_implied())
2669 2732                  sm_msg("implications from comparison: (%s)", show_sm(sm));
2670 2733  
2671 2734          return sm;
2672 2735  }
    
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX