smatch_implied.c

   1 /*
   2  * Copyright (C) 2008 Dan Carpenter.
   3  *
   4  * This program is free software; you can redistribute it and/or
   5  * modify it under the terms of the GNU General Public License
   6  * as published by the Free Software Foundation; either version 2
   7  * of the License, or (at your option) any later version.
   8  *
   9  * This program is distributed in the hope that it will be useful,
  10  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  11  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  12  * GNU General Public License for more details.
  13  *
  14  * You should have received a copy of the GNU General Public License
  15  * along with this program; if not, see http://www.gnu.org/copyleft/gpl.txt
  16  */
  17
  18 /*
  19  * Imagine we have this code:
  20  * foo = 1;
  21  * if (bar)
  22  *         foo = 99;
  23  * else
  24  *         frob();
  25  *                   //  <-- point #1
  26  * if (foo == 99)    //  <-- point #2
  27  *         bar->baz; //  <-- point #3
  28  *
  29  *
  30  * At point #3 bar is non null and can be dereferenced.
  31  *
  32  * It's smatch_implied.c which sets bar to non null at point #2.
  33  *
  34  * At point #1 merge_slist() stores the list of states from both
  35  * the true and false paths.  On the true path foo == 99 and on
  36  * the false path foo == 1.  merge_slist() sets their pool
  37  * list to show the other states which were there when foo == 99.
  38  *
  39  * When it comes to the if (foo == 99) the smatch implied hook
  40  * looks for all the pools where foo was not 99.  It makes a list
  41  * of those.
  42  *
  43  * Then for bar (and all the other states) it says, ok bar is a
  44  * merged state that came from these previous states.  We'll
  45  * chop out all the states where it came from a pool where
  46  * foo != 99 and merge it all back together.
  47  *
  48  * That is the implied state of bar.
  49  *
  50  * merge_slist() sets up ->pool.  An sm_state only has one ->pool and
  51  *    that is the pool where it was first set.  The my pool gets set when
  52  *    code paths merge.  States that have been set since the last merge do
  53  *    not have a ->pool.
  54  * merge_sm_state() sets ->left and ->right.  (These are the states which were
  55  *    merged to form the current state.)
  56  * a pool:  a pool is an slist that has been merged with another slist.
  57  */
  58
  59 #include <sys/time.h>
  60 #include <time.h>
  61 #include "smatch.h"
  62 #include "smatch_slist.h"
  63 #include "smatch_extra.h"
  64
  65 char *implied_debug_msg;
  66 #define DIMPLIED(msg...) do { if (option_debug_implied) printf(msg); } while (0)
  67
  68 int option_debug_implied = 0;
  69
  70 /*
  71  * tmp_range_list():
  72  * It messes things up to free range list allocations.  This helper fuction
  73  * lets us reuse memory instead of doing new allocations.
  74  */
  75 static struct range_list *tmp_range_list(struct symbol *type, long long num)
  76 {
  77         static struct range_list *my_list = NULL;
  78         static struct data_range *my_range;
  79
  80         __free_ptr_list((struct ptr_list **)&my_list);
  81         my_range = alloc_range(ll_to_sval(num), ll_to_sval(num));
  82         add_ptr_list(&my_list, my_range);
  83         return my_list;
  84 }
  85
  86 static void print_debug_tf(struct sm_state *sm, int istrue, int isfalse)
  87 {
  88         if (!option_debug_implied && !option_debug)
  89                 return;
  90
  91         if (istrue && isfalse) {
  92                 printf("'%s = %s' from %d does not exist.\n", sm->name,
  93                         show_state(sm->state), sm->line);
  94         } else if (istrue) {
  95                 printf("'%s = %s' from %d is true. [stree %d]\n", sm->name, show_state(sm->state),
  96                         sm->line, get_stree_id(sm->pool));
  97         } else if (isfalse) {
  98                 printf("'%s = %s' from %d is false. [stree %d]\n", sm->name, show_state(sm->state),
  99                         sm->line, get_stree_id(sm->pool));
 100         } else {
 101                 printf("'%s = %s' from %d could be true or false. [stree %d]\n", sm->name,
 102                         show_state(sm->state), sm->line, get_stree_id(sm->pool));
 103         }
 104 }
 105
 106 /*
 107  * add_pool() adds a slist to *pools. If the slist has already been
 108  * added earlier then it doesn't get added a second time.
 109  */
 110 void add_pool(struct stree_stack **pools, struct stree *new)
 111 {
 112         struct stree *tmp;
 113
 114         FOR_EACH_PTR(*pools, tmp) {
 115                 if (tmp < new)
 116                         continue;
 117                 else if (tmp == new) {
 118                         return;
 119                 } else {
 120                         INSERT_CURRENT(new, tmp);
 121                         return;
 122                 }
 123         } END_FOR_EACH_PTR(tmp);
 124         add_ptr_list(pools, new);
 125 }
 126
 127 /*
 128  * If 'foo' == 99 add it that pool to the true pools.  If it's false, add it to
 129  * the false pools.  If we're not sure, then we don't add it to either.
 130  */
 131 static void do_compare(struct sm_state *sm, int comparison, struct range_list *rl,
 132                         struct stree_stack **true_stack,
 133                         struct stree_stack **false_stack)
 134 {
 135         struct sm_state *s;
 136         int istrue;
 137         int isfalse;
 138         struct range_list *var_rl;
 139
 140         if (!sm->pool)
 141                 return;
 142
 143         if (is_implied(sm)) {
 144                 s = get_sm_state_stree(sm->pool,
 145                                 sm->owner, sm->name,
 146                                 sm->sym);
 147         } else {
 148                 s = sm;
 149         }
 150
 151         if (!s) {
 152                 if (option_debug_implied || option_debug)
 153                         sm_msg("%s from %d, has borrowed implications.",
 154                                 sm->name, sm->line);
 155                 return;
 156         }
 157
 158         var_rl = cast_rl(rl_type(rl), estate_rl(s->state));
 159
 160         istrue = !possibly_false_rl(var_rl, comparison, rl);
 161         isfalse = !possibly_true_rl(var_rl, comparison, rl);
 162
 163         print_debug_tf(s, istrue, isfalse);
 164
 165         if (istrue)
 166                 add_pool(true_stack, s->pool);
 167
 168         if (isfalse)
 169                 add_pool(false_stack, s->pool);
 170 }
 171
 172 static int pool_in_pools(struct stree *pool,
 173                          const struct stree_stack *pools)
 174 {
 175         struct stree *tmp;
 176
 177         FOR_EACH_PTR(pools, tmp) {
 178                 if (tmp == pool)
 179                         return 1;
 180                 if (tmp > pool)
 181                         return 0;
 182         } END_FOR_EACH_PTR(tmp);
 183         return 0;
 184 }
 185
 186 static int is_checked(struct state_list *checked, struct sm_state *sm)
 187 {
 188         struct sm_state *tmp;
 189
 190         FOR_EACH_PTR(checked, tmp) {
 191                 if (tmp == sm)
 192                         return 1;
 193         } END_FOR_EACH_PTR(tmp);
 194         return 0;
 195 }
 196
 197 /*
 198  * separate_pools():
 199  * Example code:  if (foo == 99) {
 200  *
 201  * Say 'foo' is a merged state that has many possible values.  It is the combination
 202  * of merges.  separate_pools() iterates through the pools recursively and calls
 203  * do_compare() for each time 'foo' was set.
 204  */
 205 static void separate_pools(struct sm_state *sm, int comparison, struct range_list *rl,
 206                         struct stree_stack **true_stack,
 207                         struct stree_stack **false_stack,
 208                         struct state_list **checked)
 209 {
 210         int free_checked = 0;
 211         struct state_list *checked_states = NULL;
 212
 213         if (!sm)
 214                 return;
 215
 216         /*
 217            Sometimes the implications are just too big to deal with
 218            so we bail.  Theoretically, bailing out here can cause more false
 219            positives but won't hide actual bugs.
 220         */
 221         if (sm->nr_children > 4000) {
 222                 if (option_debug || option_debug_implied) {
 223                         static char buf[1028];
 224                         snprintf(buf, sizeof(buf), "debug: separate_pools: nr_children over 4000 (%d). (%s %s)",
 225                                  sm->nr_children, sm->name, show_state(sm->state));
 226                         implied_debug_msg = buf;
 227                 }
 228                 return;
 229         }
 230
 231         if (checked == NULL) {
 232                 checked = &checked_states;
 233                 free_checked = 1;
 234         }
 235         if (is_checked(*checked, sm))
 236                 return;
 237         add_ptr_list(checked, sm);
 238
 239         do_compare(sm, comparison, rl, true_stack, false_stack);
 240
 241         separate_pools(sm->left, comparison, rl, true_stack, false_stack, checked);
 242         separate_pools(sm->right, comparison, rl, true_stack, false_stack, checked);
 243         if (free_checked)
 244                 free_slist(checked);
 245 }
 246
 247 struct sm_state *filter_pools(struct sm_state *sm,
 248                               const struct stree_stack *remove_stack,
 249                               const struct stree_stack *keep_stack,
 250                               int *modified)
 251 {
 252         struct sm_state *ret = NULL;
 253         struct sm_state *left;
 254         struct sm_state *right;
 255         int removed = 0;
 256
 257         if (!sm)
 258                 return NULL;
 259
 260         if (sm->nr_children > 4000) {
 261                 if (option_debug || option_debug_implied) {
 262                         static char buf[1028];
 263                         snprintf(buf, sizeof(buf), "debug: %s: nr_children over 4000 (%d). (%s %s)",
 264                                  __func__, sm->nr_children, sm->name, show_state(sm->state));
 265                         implied_debug_msg = buf;
 266                 }
 267                 return NULL;
 268         }
 269
 270         if (pool_in_pools(sm->pool, remove_stack)) {
 271                 DIMPLIED("removed %s from %d [stree %d]\n", show_sm(sm), sm->line, get_stree_id(sm->pool));
 272                 *modified = 1;
 273                 return NULL;
 274         }
 275
 276         if (!is_merged(sm) || pool_in_pools(sm->pool, keep_stack)) {
 277                 DIMPLIED("kept %s from %d [stree %d]\n", show_sm(sm), sm->line, get_stree_id(sm->pool));
 278                 return sm;
 279         }
 280
 281         DIMPLIED("checking %s from %d (%d) [stree %d] left = %s [stree %d] right = %s [stree %d]\n",
 282                  show_sm(sm), sm->line, sm->nr_children, get_stree_id(sm->pool),
 283                  sm->left ? show_sm(sm->left) : "<none>", sm->left ? get_stree_id(sm->left->pool) : -1,
 284                  sm->right ? show_sm(sm->right) : "<none>", sm->right ? get_stree_id(sm->right->pool) : -1);
 285         left = filter_pools(sm->left, remove_stack, keep_stack, &removed);
 286         right = filter_pools(sm->right, remove_stack, keep_stack, &removed);
 287         if (!removed) {
 288                 DIMPLIED("kept %s from %d [stree %d]\n", show_sm(sm), sm->line, get_stree_id(sm->pool));
 289                 return sm;
 290         }
 291         *modified = 1;
 292         if (!left && !right) {
 293                 DIMPLIED("removed %s from %d <none> [stree %d]\n", show_sm(sm), sm->line, get_stree_id(sm->pool));
 294                 return NULL;
 295         }
 296
 297         if (!left) {
 298                 ret = clone_sm(right);
 299                 ret->merged = 1;
 300                 ret->right = right;
 301                 ret->left = NULL;
 302         } else if (!right) {
 303                 ret = clone_sm(left);
 304                 ret->merged = 1;
 305                 ret->left = left;
 306                 ret->right = NULL;
 307         } else {
 308                 ret = merge_sm_states(left, right);
 309         }
 310
 311         ret->pool = sm->pool;
 312
 313         ret->implied = 1;
 314         DIMPLIED("partial %s => ", show_sm(sm));
 315         DIMPLIED("%s from %d [stree %d]\n", show_sm(ret), sm->line, get_stree_id(sm->pool));
 316         return ret;
 317 }
 318
 319 static int highest_stree_id(struct sm_state *sm)
 320 {
 321         int left = 0;
 322         int right = 0;
 323
 324         if (!sm->left && !sm->right)
 325                 return 0;
 326
 327         if (sm->left)
 328                 left = get_stree_id(sm->left->pool);
 329         if (sm->right)
 330                 right = get_stree_id(sm->right->pool);
 331
 332         if (right > left)
 333                 return right;
 334         return left;
 335 }
 336
 337 static struct stree *filter_stack(struct sm_state *gate_sm,
 338                                        struct stree *pre_stree,
 339                                        const struct stree_stack *remove_stack,
 340                                        const struct stree_stack *keep_stack)
 341 {
 342         struct stree *ret = NULL;
 343         struct sm_state *tmp;
 344         struct sm_state *filtered_sm;
 345         int modified;
 346
 347         if (!remove_stack)
 348                 return NULL;
 349
 350         FOR_EACH_SM(pre_stree, tmp) {
 351                 if (!tmp->merged)
 352                         continue;
 353                 if (highest_stree_id(tmp) < highest_stree_id(gate_sm)) {
 354                         DIMPLIED("skipping %s.  set before.  %d vs %d\n",
 355                                         tmp->name, highest_stree_id(tmp),
 356                                         highest_stree_id(gate_sm));
 357                         continue;
 358                 }
 359                 modified = 0;
 360                 filtered_sm = filter_pools(tmp, remove_stack, keep_stack, &modified);
 361                 if (filtered_sm && modified) {
 362                         /* the assignments here are for borrowed implications */
 363                         filtered_sm->name = tmp->name;
 364                         filtered_sm->sym = tmp->sym;
 365                         avl_insert(&ret, filtered_sm);
 366                         if (out_of_memory())
 367                                 return NULL;
 368
 369                 }
 370         } END_FOR_EACH_SM(tmp);
 371         return ret;
 372 }
 373
 374 static void separate_and_filter(struct sm_state *sm, int comparison, struct range_list *rl,
 375                 struct stree *pre_stree,
 376                 struct stree **true_states,
 377                 struct stree **false_states)
 378 {
 379         struct stree_stack *true_stack = NULL;
 380         struct stree_stack *false_stack = NULL;
 381         struct timeval time_before;
 382         struct timeval time_after;
 383
 384         gettimeofday(&time_before, NULL);
 385
 386         if (!is_merged(sm)) {
 387                 DIMPLIED("%d '%s' is not merged.\n", get_lineno(), sm->name);
 388                 return;
 389         }
 390
 391         if (option_debug_implied || option_debug) {
 392                 sm_msg("checking implications: (%s %s %s)",
 393                        sm->name, show_special(comparison), show_rl(rl));
 394         }
 395
 396         separate_pools(sm, comparison, rl, &true_stack, &false_stack, NULL);
 397
 398         DIMPLIED("filtering true stack.\n");
 399         *true_states = filter_stack(sm, pre_stree, false_stack, true_stack);
 400         DIMPLIED("filtering false stack.\n");
 401         *false_states = filter_stack(sm, pre_stree, true_stack, false_stack);
 402         free_stree_stack(&true_stack);
 403         free_stree_stack(&false_stack);
 404         if (option_debug_implied || option_debug) {
 405                 printf("These are the implied states for the true path:\n");
 406                 __print_stree(*true_states);
 407                 printf("These are the implied states for the false path:\n");
 408                 __print_stree(*false_states);
 409         }
 410
 411         gettimeofday(&time_after, NULL);
 412         if (time_after.tv_sec - time_before.tv_sec > 7)
 413                 __bail_on_rest_of_function = 1;
 414 }
 415
 416 static struct expression *get_left_most_expr(struct expression *expr)
 417 {
 418         expr = strip_expr(expr);
 419         if (expr->type == EXPR_ASSIGNMENT)
 420                 return get_left_most_expr(expr->left);
 421         return expr;
 422 }
 423
 424 static int is_merged_expr(struct expression  *expr)
 425 {
 426         struct sm_state *sm;
 427         sval_t dummy;
 428
 429         if (get_value(expr, &dummy))
 430                 return 0;
 431         sm = get_sm_state_expr(SMATCH_EXTRA, expr);
 432         if (!sm)
 433                 return 0;
 434         if (is_merged(sm))
 435                 return 1;
 436         return 0;
 437 }
 438
 439 static void delete_equiv_stree(struct stree **stree, const char *name, struct symbol *sym)
 440 {
 441         struct smatch_state *state;
 442         struct relation *rel;
 443
 444         state = get_state(SMATCH_EXTRA, name, sym);
 445         if (!estate_related(state)) {
 446                 delete_state_stree(stree, SMATCH_EXTRA, name, sym);
 447                 return;
 448         }
 449
 450         FOR_EACH_PTR(estate_related(state), rel) {
 451                 delete_state_stree(stree, SMATCH_EXTRA, rel->name, rel->sym);
 452         } END_FOR_EACH_PTR(rel);
 453 }
 454
 455 static int handle_comparison(struct expression *expr,
 456                               struct stree **implied_true,
 457                               struct stree **implied_false)
 458 {
 459         struct sm_state *sm = NULL;
 460         struct range_list *rl = NULL;
 461         struct expression *left;
 462         struct expression *right;
 463         struct symbol *type;
 464         int comparison = expr->op;
 465
 466         left = get_left_most_expr(expr->left);
 467         right = get_left_most_expr(expr->right);
 468
 469         if (is_merged_expr(left)) {
 470                 sm = get_sm_state_expr(SMATCH_EXTRA, left);
 471                 get_implied_rl(right, &rl);
 472         } else if (is_merged_expr(right)) {
 473                 sm = get_sm_state_expr(SMATCH_EXTRA, right);
 474                 get_implied_rl(left, &rl);
 475                 comparison = flip_comparison(comparison);
 476         }
 477
 478         if (!rl || !sm) {
 479                 free_rl(&rl);
 480                 return 0;
 481         }
 482
 483         type = get_type(expr);
 484         if (!type)
 485                 return 0;
 486         if (type_positive_bits(rl_type(rl)) > type_positive_bits(type))
 487                 type = rl_type(rl);
 488         if (type_positive_bits(type) < 31)
 489                 type = &int_ctype;
 490         rl = cast_rl(type, rl);
 491
 492         separate_and_filter(sm, comparison, rl, __get_cur_stree(), implied_true, implied_false);
 493         free_rl(&rl);
 494         delete_equiv_stree(implied_true, sm->name, sm->sym);
 495         delete_equiv_stree(implied_false, sm->name, sm->sym);
 496
 497         return 1;
 498 }
 499
 500 static int handle_zero_comparison(struct expression *expr,
 501                                 struct stree **implied_true,
 502                                 struct stree **implied_false)
 503 {
 504         struct symbol *sym;
 505         char *name;
 506         struct sm_state *sm;
 507         int ret = 0;
 508
 509         if (expr->type == EXPR_POSTOP)
 510                 expr = strip_expr(expr->unop);
 511
 512         if (expr->type == EXPR_ASSIGNMENT) {
 513                 /* most of the time ->pools will be empty here because we
 514                    just set the state, but if have assigned a conditional
 515                    function there are implications. */
 516                 expr = expr->left;
 517         }
 518
 519         name = expr_to_var_sym(expr, &sym);
 520         if (!name || !sym)
 521                 goto free;
 522         sm = get_sm_state(SMATCH_EXTRA, name, sym);
 523         if (!sm)
 524                 goto free;
 525
 526         separate_and_filter(sm, SPECIAL_NOTEQUAL, tmp_range_list(estate_type(sm->state), 0), __get_cur_stree(), implied_true, implied_false);
 527         delete_equiv_stree(implied_true, name, sym);
 528         delete_equiv_stree(implied_false, name, sym);
 529         ret = 1;
 530 free:
 531         free_string(name);
 532         return ret;
 533 }
 534
 535 static int handled_by_implied_hook(struct expression *expr,
 536                                    struct stree **implied_true,
 537                                    struct stree **implied_false)
 538 {
 539         struct stree_stack *true_stack = NULL;
 540         struct stree_stack *false_stack = NULL;
 541         struct stree *pre_stree;
 542         struct sm_state *sm;
 543
 544         sm = comparison_implication_hook(expr, &true_stack, &false_stack);
 545         if (!sm)
 546                 return 0;
 547
 548         pre_stree = clone_stree(__get_cur_stree());
 549
 550         *implied_true = filter_stack(sm, pre_stree, false_stack, true_stack);
 551         *implied_false = filter_stack(sm, pre_stree, true_stack, false_stack);
 552
 553         free_stree(&pre_stree);
 554         free_stree_stack(&true_stack);
 555         free_stree_stack(&false_stack);
 556
 557         return 1;
 558 }
 559
 560 static int handled_by_extra_states(struct expression *expr,
 561                                    struct stree **implied_true,
 562                                    struct stree **implied_false)
 563 {
 564         if (expr->type == EXPR_COMPARE)
 565                 return handle_comparison(expr, implied_true, implied_false);
 566         else
 567                 return handle_zero_comparison(expr, implied_true, implied_false);
 568
 569 }
 570
 571 static int handled_by_stored_conditions(struct expression *expr,
 572                                         struct stree **implied_true,
 573                                         struct stree **implied_false)
 574 {
 575         struct stree_stack *true_stack = NULL;
 576         struct stree_stack *false_stack = NULL;
 577         struct stree *pre_stree;
 578         struct sm_state *sm;
 579
 580         sm = stored_condition_implication_hook(expr, &true_stack, &false_stack);
 581         if (!sm)
 582                 return 0;
 583
 584         pre_stree = clone_stree(__get_cur_stree());
 585
 586         *implied_true = filter_stack(sm, pre_stree, false_stack, true_stack);
 587         *implied_false = filter_stack(sm, pre_stree, true_stack, false_stack);
 588
 589         free_stree(&pre_stree);
 590         free_stree_stack(&true_stack);
 591         free_stree_stack(&false_stack);
 592
 593         return 1;
 594 }
 595
 596 static int found_implications;
 597 static void get_tf_states(struct expression *expr,
 598                           struct stree **implied_true,
 599                           struct stree **implied_false)
 600 {
 601         if (handled_by_implied_hook(expr, implied_true, implied_false))
 602                 goto found;
 603
 604         if (handled_by_extra_states(expr, implied_true, implied_false))
 605                 goto found;
 606
 607         if (handled_by_stored_conditions(expr, implied_true, implied_false))
 608                 goto found;
 609
 610         return;
 611 found:
 612         found_implications = 1;
 613 }
 614
 615 static struct stree *saved_implied_true;
 616 static struct stree *saved_implied_false;
 617
 618 static void save_implications_hook(struct expression *expr)
 619 {
 620         get_tf_states(expr, &saved_implied_true, &saved_implied_false);
 621 }
 622
 623 static void set_implied_states(struct expression *expr)
 624 {
 625         struct sm_state *sm;
 626
 627         FOR_EACH_SM(saved_implied_true, sm) {
 628                 __set_true_false_sm(sm, NULL);
 629         } END_FOR_EACH_SM(sm);
 630         free_stree(&saved_implied_true);
 631
 632         FOR_EACH_SM(saved_implied_false, sm) {
 633                 __set_true_false_sm(NULL, sm);
 634         } END_FOR_EACH_SM(sm);
 635         free_stree(&saved_implied_false);
 636 }
 637
 638 void param_limit_implications(struct expression *expr, int param, char *key, char *value)
 639 {
 640         struct expression *arg;
 641         struct symbol *compare_type;
 642         char *name;
 643         struct symbol *sym;
 644         struct sm_state *sm;
 645         struct sm_state *tmp;
 646         struct stree *implied_true = NULL;
 647         struct stree *implied_false = NULL;
 648         struct range_list *orig, *limit, *rl;
 649
 650         while (expr->type == EXPR_ASSIGNMENT)
 651                 expr = strip_expr(expr->right);
 652         if (expr->type != EXPR_CALL)
 653                 return;
 654
 655         arg = get_argument_from_call_expr(expr->args, param);
 656         if (!arg)
 657                 return;
 658
 659         name = get_variable_from_key(arg, key, &sym);
 660         if (!name || !sym)
 661                 goto free;
 662
 663         sm = get_sm_state(SMATCH_EXTRA, name, sym);
 664         if (!sm || !sm->merged)
 665                 goto free;
 666
 667         if (strcmp(key, "$") == 0)
 668                 compare_type = get_arg_type(expr->fn, param);
 669         else
 670                 compare_type = get_member_type_from_key(arg, key);
 671
 672         orig = estate_rl(sm->state);
 673         orig = cast_rl(compare_type, orig);
 674
 675         call_results_to_rl(expr, compare_type, value, &limit);
 676         rl = rl_intersection(orig, limit);
 677
 678         separate_and_filter(sm, SPECIAL_EQUAL, rl, __get_cur_stree(), &implied_true, &implied_false);
 679
 680         FOR_EACH_SM(implied_true, tmp) {
 681                 __set_sm_fake_stree(tmp);
 682         } END_FOR_EACH_SM(tmp);
 683
 684         free_stree(&implied_true);
 685         free_stree(&implied_false);
 686 free:
 687         free_string(name);
 688 }
 689
 690 struct range_list *__get_implied_values(struct expression *switch_expr)
 691 {
 692         char *name;
 693         struct symbol *sym;
 694         struct smatch_state *state;
 695         struct range_list *ret = NULL;
 696
 697         name = expr_to_var_sym(switch_expr, &sym);
 698         if (!name || !sym)
 699                 goto free;
 700         state = get_state(SMATCH_EXTRA, name, sym);
 701         if (!state)
 702                 goto free;
 703         ret = clone_rl(estate_rl(state));
 704 free:
 705         free_string(name);
 706         if (!ret) {
 707                 struct symbol *type;
 708
 709                 type = get_type(switch_expr);
 710                 ret = alloc_rl(sval_type_min(type), sval_type_max(type));
 711         }
 712         return ret;
 713 }
 714
 715 struct stree *__implied_case_stree(struct expression *switch_expr,
 716                                         struct expression *case_expr,
 717                                         struct expression *case_to,
 718                                         struct range_list_stack **remaining_cases,
 719                                         struct stree **raw_stree)
 720 {
 721         char *name = NULL;
 722         struct symbol *sym;
 723         struct sm_state *sm;
 724         struct stree *true_states = NULL;
 725         struct stree *false_states = NULL;
 726         struct stree *extra_states = NULL;
 727         struct stree *ret = clone_stree(*raw_stree);
 728         sval_t start, end;
 729         struct range_list *rl = NULL;
 730
 731         name = expr_to_var_sym(switch_expr, &sym);
 732         if (!name || !sym)
 733                 goto free;
 734         sm = get_sm_state_stree(*raw_stree, SMATCH_EXTRA, name, sym);
 735
 736         if (get_value(case_to, &end) && get_value(case_expr, &start)) {
 737                 filter_top_rl(remaining_cases, start, end);
 738                 add_range(&rl, start, end);
 739         } else if (get_value(case_expr, &start)) {
 740                 filter_top_rl(remaining_cases, start, start);
 741                 add_range(&rl, start, start);
 742         } else {
 743                 rl = clone_rl(top_rl(*remaining_cases));
 744         }
 745
 746         if (sm)
 747                 separate_and_filter(sm, SPECIAL_EQUAL, rl, *raw_stree, &true_states, &false_states);
 748
 749         __push_fake_cur_stree();
 750         __unnullify_path();
 751         set_extra_nomod(name, sym, alloc_estate_rl(rl));
 752         extra_states = __pop_fake_cur_stree();
 753         overwrite_stree(extra_states, &true_states);
 754         overwrite_stree(true_states, &ret);
 755         free_stree(&extra_states);
 756         free_stree(&true_states);
 757         free_stree(&false_states);
 758 free:
 759         free_string(name);
 760         return ret;
 761 }
 762
 763 static void match_end_func(struct symbol *sym)
 764 {
 765         if (__inline_fn)
 766                 return;
 767         implied_debug_msg = NULL;
 768 }
 769
 770 static int sm_state_in_slist(struct sm_state *sm, struct state_list *slist)
 771 {
 772         struct sm_state *tmp;
 773
 774         FOR_EACH_PTR(slist, tmp) {
 775                 if (tmp == sm)
 776                         return 1;
 777         } END_FOR_EACH_PTR(tmp);
 778         return 0;
 779 }
 780
 781 /*
 782  * The situation is we have a SMATCH_EXTRA state and we want to break it into
 783  * each of the ->possible states and find the implications of each.  The caller
 784  * has to use __push_fake_cur_stree() to preserve the correct states so they
 785  * can be restored later.
 786  */
 787 void overwrite_states_using_pool(struct sm_state *sm)
 788 {
 789         struct sm_state *old;
 790         struct sm_state *new;
 791
 792         if (!sm->pool)
 793                 return;
 794
 795         FOR_EACH_SM(sm->pool, old) {
 796                 new = get_sm_state(old->owner, old->name, old->sym);
 797                 if (!new)  /* the variable went out of scope */
 798                         continue;
 799                 if (sm_state_in_slist(old, new->possible))
 800                         set_state(old->owner, old->name, old->sym, old->state);
 801         } END_FOR_EACH_SM(old);
 802 }
 803
 804 int assume(struct expression *expr)
 805 {
 806         int orig_final_pass = final_pass;
 807
 808         final_pass = 0;
 809         __push_fake_cur_stree();
 810         found_implications = 0;
 811         __split_whole_condition(expr);
 812         final_pass = orig_final_pass;
 813
 814         if (!found_implications) {
 815                 __discard_false_states();
 816                 __free_fake_cur_stree();
 817                 return 0;
 818         }
 819
 820         return 1;
 821 }
 822
 823 void end_assume(void)
 824 {
 825         __discard_false_states();
 826         __free_fake_cur_stree();
 827 }
 828
 829 void __extra_match_condition(struct expression *expr);
 830 void __comparison_match_condition(struct expression *expr);
 831 void __stored_condition(struct expression *expr);
 832 void register_implications(int id)
 833 {
 834         add_hook(&save_implications_hook, CONDITION_HOOK);
 835         add_hook(&set_implied_states, CONDITION_HOOK);
 836         add_hook(&__extra_match_condition, CONDITION_HOOK);
 837         add_hook(&__comparison_match_condition, CONDITION_HOOK);
 838         add_hook(&__stored_condition, CONDITION_HOOK);
 839         add_hook(&match_end_func, END_FUNC_HOOK);
 840 }