Print this page
11506 smatch resync


  48  * foo != 99 and merge it all back together.
  49  *
  50  * That is the implied state of bar.
  51  *
  52  * merge_slist() sets up ->pool.  An sm_state only has one ->pool and
  53  *    that is the pool where it was first set.  The my pool gets set when
  54  *    code paths merge.  States that have been set since the last merge do
  55  *    not have a ->pool.
  56  * merge_sm_state() sets ->left and ->right.  (These are the states which were
  57  *    merged to form the current state.)
  58  * a pool:  a pool is an slist that has been merged with another slist.
  59  */
  60 
  61 #include <sys/time.h>
  62 #include <time.h>
  63 #include "smatch.h"
  64 #include "smatch_slist.h"
  65 #include "smatch_extra.h"
  66 
  67 char *implied_debug_msg;
  68 #define DIMPLIED(msg...) do { if (option_debug_implied || option_debug) printf(msg); } while (0)
  69 
  70 int option_debug_implied = 0;
  71 



  72 /*
  73  * tmp_range_list():
  74  * It messes things up to free range list allocations.  This helper fuction
  75  * lets us reuse memory instead of doing new allocations.
  76  */
  77 static struct range_list *tmp_range_list(struct symbol *type, long long num)
  78 {
  79         static struct range_list *my_list = NULL;
  80         static struct data_range *my_range;
  81 
  82         __free_ptr_list((struct ptr_list **)&my_list);
  83         my_range = alloc_range(ll_to_sval(num), ll_to_sval(num));
  84         add_ptr_list(&my_list, my_range);
  85         return my_list;
  86 }
  87 
  88 static void print_debug_tf(struct sm_state *sm, int istrue, int isfalse)
  89 {
  90         if (!option_debug_implied && !option_debug)
  91                 return;
  92 
  93         if (istrue && isfalse) {
  94                 printf("%s: %d: does not exist.\n", show_sm(sm), sm->line);
  95         } else if (istrue) {
  96                 printf("'%s = %s' from %d is true. %s[stree %d]\n", sm->name, show_state(sm->state),
  97                         sm->line, sm->merged ? "[merged]" : "[leaf]",
  98                         get_stree_id(sm->pool));
  99         } else if (isfalse) {
 100                 printf("'%s = %s' from %d is false. %s[stree %d]\n", sm->name, show_state(sm->state),
 101                         sm->line,
 102                         sm->merged ? "[merged]" : "[leaf]",
 103                         get_stree_id(sm->pool));
 104         } else {
 105                 printf("'%s = %s' from %d could be true or false. %s[stree %d]\n", sm->name,
 106                         show_state(sm->state), sm->line,
 107                         sm->merged ? "[merged]" : "[leaf]",
 108                         get_stree_id(sm->pool));
 109         }
 110 }


 126 
 127         orig_rl = cast_rl(rl_type(rl), estate_rl(sm->state));
 128         split_comparison_rl(orig_rl, comparison, rl, &true_rl, &false_rl, NULL, NULL);
 129 
 130         true_rl = rl_truncate_cast(estate_type(sm->state), true_rl);
 131         false_rl = rl_truncate_cast(estate_type(sm->state), false_rl);
 132         if (is_whole_rl(true_rl) || is_whole_rl(false_rl) ||
 133             !true_rl || !false_rl ||
 134             rl_equiv(orig_rl, true_rl) || rl_equiv(orig_rl, false_rl) ||
 135             rl_equiv(estate_rl(sm->state), true_rl) || rl_equiv(estate_rl(sm->state), false_rl))
 136                 return 0;
 137 
 138         if (rl_intersection(true_rl, false_rl)) {
 139                 sm_perror("parsing (%s (%s) %s %s)",
 140                         sm->name, sm->state->name, show_special(comparison), show_rl(rl));
 141                 sm_msg("true_rl = %s false_rl = %s intersection = %s",
 142                        show_rl(true_rl), show_rl(false_rl), show_rl(rl_intersection(true_rl, false_rl)));
 143                 return 0;
 144         }
 145 
 146         if (option_debug)
 147                 sm_info("fake_history: %s vs %s.  %s %s %s. --> T: %s F: %s",
 148                        sm->name, show_rl(rl), sm->state->name, show_special(comparison), show_rl(rl),
 149                        show_rl(true_rl), show_rl(false_rl));
 150 
 151         true_sm = clone_sm(sm);
 152         false_sm = clone_sm(sm);
 153 
 154         true_sm->state = alloc_estate_rl(cast_rl(estate_type(sm->state), true_rl));
 155         free_slist(&true_sm->possible);
 156         add_possible_sm(true_sm, true_sm);
 157         false_sm->state = alloc_estate_rl(cast_rl(estate_type(sm->state), false_rl));
 158         free_slist(&false_sm->possible);
 159         add_possible_sm(false_sm, false_sm);
 160 
 161         true_stree = clone_stree(sm->pool);
 162         false_stree = clone_stree(sm->pool);
 163 
 164         overwrite_sm_state_stree(&true_stree, true_sm);
 165         overwrite_sm_state_stree(&false_stree, false_sm);
 166 
 167         true_sm->pool = true_stree;
 168         false_sm->pool = false_stree;
 169 
 170         sm->merged = 1;
 171         sm->left = true_sm;
 172         sm->right = false_sm;
 173 
 174         return 1;
 175 }
 176 
 177 /*


 249         print_debug_tf(sm, istrue, isfalse);
 250 
 251         /* give up if we have borrowed implications (smatch_equiv.c) */
 252         if (sm->sym != gate_sm->sym ||
 253             strcmp(sm->name, gate_sm->name) != 0) {
 254                 if (mixed)
 255                         *mixed = 1;
 256         }
 257 
 258         if (mixed && !*mixed && !is_merged(sm) && !istrue && !isfalse) {
 259                 if (!create_fake_history(sm, comparison, rl))
 260                         *mixed = 1;
 261         }
 262 
 263         if (istrue)
 264                 add_pool(true_stack, sm);
 265         else if (isfalse)
 266                 add_pool(false_stack, sm);
 267         else
 268                 add_pool(maybe_stack, sm);
 269 
 270 }
 271 
 272 static int is_checked(struct state_list *checked, struct sm_state *sm)
 273 {
 274         struct sm_state *tmp;
 275 
 276         FOR_EACH_PTR(checked, tmp) {
 277                 if (tmp == sm)
 278                         return 1;
 279         } END_FOR_EACH_PTR(tmp);
 280         return 0;
 281 }
 282 
 283 /*
 284  * separate_pools():
 285  * Example code:  if (foo == 99) {
 286  *
 287  * Say 'foo' is a merged state that has many possible values.  It is the combination
 288  * of merges.  separate_pools() iterates through the pools recursively and calls
 289  * do_compare() for each time 'foo' was set.
 290  */
 291 static void __separate_pools(struct sm_state *sm, int comparison, struct range_list *rl,
 292                         struct state_list **true_stack,
 293                         struct state_list **maybe_stack,
 294                         struct state_list **false_stack,
 295                         struct state_list **checked, int *mixed, struct sm_state *gate_sm)

 296 {
 297         int free_checked = 0;
 298         struct state_list *checked_states = NULL;

 299 
 300         if (!sm)
 301                 return;
 302 
 303         /*
 304          * If it looks like this is going to take too long as-is, then don't
 305          * create even more fake history.
 306          */
 307         if (mixed && sm->nr_children > 100)


 308                 *mixed = 1;
 309 
 310         /*
 311            Sometimes the implications are just too big to deal with
 312            so we bail.  Theoretically, bailing out here can cause more false
 313            positives but won't hide actual bugs.
 314         */
 315         if (sm->nr_children > 4000) {
 316                 if (option_debug || option_debug_implied) {
 317                         static char buf[1028];
 318                         snprintf(buf, sizeof(buf), "debug: %s: nr_children over 4000 (%d). (%s %s)",
 319                                  __func__, sm->nr_children, sm->name, show_state(sm->state));
 320                         implied_debug_msg = buf;
 321                 }
 322                 return;
 323         }
 324 
 325         if (checked == NULL) {
 326                 checked = &checked_states;
 327                 free_checked = 1;
 328         }
 329         if (is_checked(*checked, sm))
 330                 return;
 331         add_ptr_list(checked, sm);
 332 
 333         do_compare(sm, comparison, rl, true_stack, maybe_stack, false_stack, mixed, gate_sm);
 334 
 335         __separate_pools(sm->left, comparison, rl, true_stack, maybe_stack, false_stack, checked, mixed, gate_sm);
 336         __separate_pools(sm->right, comparison, rl, true_stack, maybe_stack, false_stack, checked, mixed, gate_sm);
 337         if (free_checked)
 338                 free_slist(checked);
 339 }
 340 
 341 static void separate_pools(struct sm_state *sm, int comparison, struct range_list *rl,
 342                         struct state_list **true_stack,
 343                         struct state_list **false_stack,
 344                         struct state_list **checked, int *mixed)
 345 {
 346         struct state_list *maybe_stack = NULL;
 347         struct sm_state *tmp;

 348 
 349         __separate_pools(sm, comparison, rl, true_stack, &maybe_stack, false_stack, checked, mixed, sm);
 350 
 351         if (option_debug) {



 352                 struct sm_state *sm;
 353 
 354                 FOR_EACH_PTR(*true_stack, sm) {
 355                         sm_msg("TRUE %s [stree %d]", show_sm(sm), get_stree_id(sm->pool));
 356                 } END_FOR_EACH_PTR(sm);
 357 
 358                 FOR_EACH_PTR(maybe_stack, sm) {
 359                         sm_msg("MAYBE %s [stree %d]", show_sm(sm), get_stree_id(sm->pool));

 360                 } END_FOR_EACH_PTR(sm);
 361 
 362                 FOR_EACH_PTR(*false_stack, sm) {
 363                         sm_msg("FALSE %s [stree %d]", show_sm(sm), get_stree_id(sm->pool));
 364                 } END_FOR_EACH_PTR(sm);
 365         }
 366         /* if it's a maybe then remove it */
 367         FOR_EACH_PTR(maybe_stack, tmp) {
 368                 remove_pool(false_stack, tmp->pool);
 369                 remove_pool(true_stack, tmp->pool);
 370         } END_FOR_EACH_PTR(tmp);
 371 
 372         /* if it's both true and false remove it from both */
 373         FOR_EACH_PTR(*true_stack, tmp) {
 374                 if (remove_pool(false_stack, tmp->pool))
 375                         DELETE_CURRENT_PTR(tmp);
 376         } END_FOR_EACH_PTR(tmp);
 377 }
 378 
 379 static int sm_in_keep_leafs(struct sm_state *sm, const struct state_list *keep_gates)
 380 {
 381         struct sm_state *tmp, *old;
 382 
 383         FOR_EACH_PTR(keep_gates, tmp) {
 384                 if (is_merged(tmp))
 385                         continue;
 386                 old = get_sm_state_stree(tmp->pool, sm->owner, sm->name, sm->sym);
 387                 if (!old)
 388                         continue;
 389                 if (old == sm)
 390                         return 1;
 391         } END_FOR_EACH_PTR(tmp);
 392         return 0;
 393 }
 394 
 395 static int taking_too_long(void)
 396 {
 397         static void *printed;
 398 
 399         if (out_of_memory())

 400                 return 1;

 401 
 402         if (time_parsing_function() < option_timeout)

 403                 return 0;

 404 
 405         if (!__inline_fn && printed != cur_func_sym) {
 406                 if (!is_skipped_function())
 407                         sm_perror("turning off implications after 60 seconds");
 408                 printed = cur_func_sym;
 409         }

 410         return 1;
 411 }
 412 























 413 /*
 414  * NOTE: If a state is in both the keep stack and the remove stack then that is
 415  * a bug.  Only add states which are definitely true or definitely false.  If
 416  * you have a leaf state that could be both true and false, then create a fake
 417  * split history where one side is true and one side is false.  Otherwise, if
 418  * you can't do that, then don't add it to either list.
 419  */

 420 struct sm_state *filter_pools(struct sm_state *sm,
 421                               const struct state_list *remove_stack,
 422                               const struct state_list *keep_stack,
 423                               int *modified, int *recurse_cnt,
 424                               struct timeval *start)
 425 {
 426         struct sm_state *ret = NULL;
 427         struct sm_state *left;
 428         struct sm_state *right;
 429         int removed = 0;
 430         struct timeval now;
 431 
 432         if (!sm)
 433                 return NULL;
 434         if (sm->skip_implications)
 435                 return sm;
 436         if (taking_too_long())
 437                 return sm;
 438 
 439         gettimeofday(&now, NULL);
 440         if ((*recurse_cnt)++ > 1000 || now.tv_sec - start->tv_sec > 5) {
 441                 if (local_debug || option_debug_implied) {
 442                         static char buf[1028];
 443                         snprintf(buf, sizeof(buf), "debug: %s: nr_children over 4000 (%d). (%s %s)",
 444                                  __func__, sm->nr_children, sm->name, show_state(sm->state));
 445                         implied_debug_msg = buf;
 446                 }
 447                 sm->skip_implications = 1;
 448                 return sm;


 449         }
 450 
 451         if (pool_in_pools(sm->pool, remove_stack)) {
 452                 DIMPLIED("removed [stree %d] %s from %d\n", get_stree_id(sm->pool), show_sm(sm), sm->line);
 453                 *modified = 1;
 454                 return NULL;
 455         }
 456 
 457         if (!is_merged(sm) || pool_in_pools(sm->pool, keep_stack) || sm_in_keep_leafs(sm, keep_stack)) {
 458                 DIMPLIED("kept [stree %d] %s from %d. %s. %s. %s.\n", get_stree_id(sm->pool), show_sm(sm), sm->line,
 459                         is_merged(sm) ? "merged" : "not merged",
 460                         pool_in_pools(sm->pool, keep_stack) ? "not in keep pools" : "in keep pools",
 461                         sm_in_keep_leafs(sm, keep_stack) ? "reachable keep leaf" : "no keep leaf");

 462                 return sm;
 463         }
 464 
 465         DIMPLIED("checking [stree %d] %s from %d (%d) left = %s [stree %d] right = %s [stree %d]\n",
 466                  get_stree_id(sm->pool),
 467                  show_sm(sm), sm->line, sm->nr_children,
 468                  sm->left ? sm->left->state->name : "<none>", sm->left ? get_stree_id(sm->left->pool) : -1,
 469                  sm->right ? sm->right->state->name : "<none>", sm->right ? get_stree_id(sm->right->pool) : -1);
 470         left = filter_pools(sm->left, remove_stack, keep_stack, &removed, recurse_cnt, start);
 471         right = filter_pools(sm->right, remove_stack, keep_stack, &removed, recurse_cnt, start);
 472         if (!removed) {
 473                 DIMPLIED("kept [stree %d] %s from %d\n", get_stree_id(sm->pool), show_sm(sm), sm->line);
 474                 return sm;
 475         }
 476         *modified = 1;
 477         if (!left && !right) {
 478                 DIMPLIED("removed [stree %d] %s from %d <none>\n", get_stree_id(sm->pool), show_sm(sm), sm->line);
 479                 return NULL;
 480         }
 481 
 482         if (!left) {
 483                 ret = clone_sm(right);
 484                 ret->merged = 1;
 485                 ret->right = right;
 486                 ret->left = NULL;
 487         } else if (!right) {
 488                 ret = clone_sm(left);
 489                 ret->merged = 1;
 490                 ret->left = left;
 491                 ret->right = NULL;
 492         } else {
 493                 if (left->sym != sm->sym || strcmp(left->name, sm->name) != 0) {
 494                         left = clone_sm(left);
 495                         left->sym = sm->sym;
 496                         left->name = sm->name;
 497                 }
 498                 if (right->sym != sm->sym || strcmp(right->name, sm->name) != 0) {
 499                         right = clone_sm(right);
 500                         right->sym = sm->sym;
 501                         right->name = sm->name;
 502                 }
 503                 ret = merge_sm_states(left, right);
 504         }
 505 
 506         ret->pool = sm->pool;
 507 
 508         DIMPLIED("partial %s => ", show_sm(sm));
 509         DIMPLIED("%s from %d [stree %d]\n", show_sm(ret), sm->line, get_stree_id(sm->pool));
 510         return ret;
 511 }
 512 
 513 static struct stree *filter_stack(struct sm_state *gate_sm,
 514                                        struct stree *pre_stree,
 515                                        const struct state_list *remove_stack,
 516                                        const struct state_list *keep_stack)
 517 {
 518         struct stree *ret = NULL;
 519         struct sm_state *tmp;
 520         struct sm_state *filtered_sm;
 521         int modified;
 522         int recurse_cnt;
 523         struct timeval start;


 524 
 525         if (!remove_stack)
 526                 return NULL;
 527 
 528         if (taking_too_long())
 529                 return NULL;
 530 
 531         FOR_EACH_SM(pre_stree, tmp) {
 532                 if (option_debug)
 533                         sm_msg("%s: %s", __func__, show_sm(tmp));
 534                 if (!tmp->merged)
 535                         continue;
 536                 if (sm_in_keep_leafs(tmp, keep_stack))
 537                         continue;
 538                 modified = 0;
 539                 recurse_cnt = 0;
 540                 gettimeofday(&start, NULL);
 541                 filtered_sm = filter_pools(tmp, remove_stack, keep_stack, &modified, &recurse_cnt, &start);
 542                 if (!filtered_sm || !modified)






 543                         continue;
 544                 /* the assignments here are for borrowed implications */
 545                 filtered_sm->name = tmp->name;
 546                 filtered_sm->sym = tmp->sym;
 547                 avl_insert(&ret, filtered_sm);
 548                 if (out_of_memory() || taking_too_long())
 549                         return NULL;
 550 
 551         } END_FOR_EACH_SM(tmp);
 552         return ret;
 553 }
 554 
 555 static void separate_and_filter(struct sm_state *sm, int comparison, struct range_list *rl,
 556                 struct stree *pre_stree,
 557                 struct stree **true_states,
 558                 struct stree **false_states,
 559                 int *mixed)
 560 {
 561         struct state_list *true_stack = NULL;
 562         struct state_list *false_stack = NULL;
 563         struct timeval time_before;
 564         struct timeval time_after;
 565         int sec;
 566 
 567         gettimeofday(&time_before, NULL);
 568 



 569         if (!is_merged(sm)) {
 570                 DIMPLIED("%d '%s' is not merged.\n", get_lineno(), sm->name);
 571                 return;
 572         }
 573 
 574         if (option_debug_implied || option_debug) {
 575                 sm_msg("checking implications: (%s %s %s)",
 576                        sm->name, show_special(comparison), show_rl(rl));
 577         }
 578 
 579         separate_pools(sm, comparison, rl, &true_stack, &false_stack, NULL, mixed);
 580 
 581         DIMPLIED("filtering true stack.\n");
 582         *true_states = filter_stack(sm, pre_stree, false_stack, true_stack);
 583         DIMPLIED("filtering false stack.\n");
 584         *false_states = filter_stack(sm, pre_stree, true_stack, false_stack);
 585         free_slist(&true_stack);
 586         free_slist(&false_stack);
 587         if (option_debug_implied || option_debug) {
 588                 printf("These are the implied states for the true path: (%s %s %s)\n",
 589                        sm->name, show_special(comparison), show_rl(rl));
 590                 __print_stree(*true_states);
 591                 printf("These are the implied states for the false path: (%s %s %s)\n",
 592                        sm->name, show_special(comparison), show_rl(rl));
 593                 __print_stree(*false_states);
 594         }
 595 
 596         gettimeofday(&time_after, NULL);
 597         sec = time_after.tv_sec - time_before.tv_sec;
 598         if (sec > option_timeout) {
 599                 sm->nr_children = 4000;
 600                 sm_perror("Function too hairy.  Ignoring implications after %d seconds.", sec);
 601         }
 602 }
 603 
 604 static struct expression *get_last_expr(struct statement *stmt)
 605 {
 606         struct statement *last;
 607 
 608         last = last_ptr_list((struct ptr_list *)stmt->stmts);
 609         if (last->type == STMT_EXPRESSION)
 610                 return last->expression;
 611 
 612         if (last->type == STMT_LABEL) {
 613                 if (last->label_statement &&
 614                     last->label_statement->type == STMT_EXPRESSION)
 615                         return last->label_statement->expression;
 616         }
 617 
 618         return NULL;
 619 }


 797         struct state_list *false_stack = NULL;
 798         struct stree *pre_stree;
 799         struct sm_state *sm;
 800 
 801         sm = stored_condition_implication_hook(expr, &true_stack, &false_stack);
 802         if (!sm)
 803                 return 0;
 804 
 805         pre_stree = clone_stree(__get_cur_stree());
 806 
 807         *implied_true = filter_stack(sm, pre_stree, false_stack, true_stack);
 808         *implied_false = filter_stack(sm, pre_stree, true_stack, false_stack);
 809 
 810         free_stree(&pre_stree);
 811         free_slist(&true_stack);
 812         free_slist(&false_stack);
 813 
 814         return 1;
 815 }
 816 
 817 static int found_implications;
 818 static struct stree *saved_implied_true;
 819 static struct stree *saved_implied_false;
 820 static struct stree *extra_saved_implied_true;
 821 static struct stree *extra_saved_implied_false;
 822 
 823 static void separate_extra_states(struct stree **implied_true,
 824                                   struct stree **implied_false)
 825 {
 826         struct sm_state *sm;
 827 
 828         /* We process extra states later to preserve the implications. */
 829         FOR_EACH_SM(*implied_true, sm) {
 830                 if (sm->owner == SMATCH_EXTRA)
 831                         overwrite_sm_state_stree(&extra_saved_implied_true, sm);
 832         } END_FOR_EACH_SM(sm);
 833         FOR_EACH_SM(extra_saved_implied_true, sm) {
 834                 delete_state_stree(implied_true, sm->owner, sm->name, sm->sym);
 835         } END_FOR_EACH_SM(sm);
 836 
 837         FOR_EACH_SM(*implied_false, sm) {
 838                 if (sm->owner == SMATCH_EXTRA)
 839                         overwrite_sm_state_stree(&extra_saved_implied_false, sm);
 840         } END_FOR_EACH_SM(sm);
 841         FOR_EACH_SM(extra_saved_implied_false, sm) {
 842                 delete_state_stree(implied_false, sm->owner, sm->name, sm->sym);
 843         } END_FOR_EACH_SM(sm);
 844 }
 845 
 846 static void get_tf_states(struct expression *expr,
 847                           struct stree **implied_true,
 848                           struct stree **implied_false)
 849 {
 850         if (handled_by_comparison_hook(expr, implied_true, implied_false))
 851                 goto found;
 852 
 853         if (handled_by_extra_states(expr, implied_true, implied_false)) {
 854                 separate_extra_states(implied_true, implied_false);
 855                 goto found;
 856         }
 857 
 858         if (handled_by_stored_conditions(expr, implied_true, implied_false))
 859                 goto found;
 860 
 861         return;
 862 found:
 863         found_implications = 1;
 864 }
 865 
 866 static void save_implications_hook(struct expression *expr)
 867 {
 868         if (taking_too_long())
 869                 return;
 870         get_tf_states(expr, &saved_implied_true, &saved_implied_false);
 871 }
 872 
 873 static void set_implied_states(struct expression *expr)
 874 {
 875         struct sm_state *sm;
 876 
 877         FOR_EACH_SM(saved_implied_true, sm) {
 878                 __set_true_false_sm(sm, NULL);
 879         } END_FOR_EACH_SM(sm);
 880         free_stree(&saved_implied_true);
 881 
 882         FOR_EACH_SM(saved_implied_false, sm) {
 883                 __set_true_false_sm(NULL, sm);
 884         } END_FOR_EACH_SM(sm);
 885         free_stree(&saved_implied_false);
 886 }
 887 
 888 static void set_extra_implied_states(struct expression *expr)
 889 {
 890         saved_implied_true = extra_saved_implied_true;
 891         saved_implied_false = extra_saved_implied_false;
 892         extra_saved_implied_true = NULL;
 893         extra_saved_implied_false = NULL;
 894         set_implied_states(NULL);
 895 }
 896 
 897 void param_limit_implications(struct expression *expr, int param, char *key, char *value)
 898 {
 899         struct expression *arg;
 900         struct symbol *compare_type;
 901         char *name;
 902         struct symbol *sym;
 903         struct sm_state *sm;
 904         struct sm_state *tmp;
 905         struct stree *implied_true = NULL;
 906         struct stree *implied_false = NULL;
 907         struct range_list *orig, *limit;
 908 



 909         while (expr->type == EXPR_ASSIGNMENT)
 910                 expr = strip_expr(expr->right);
 911         if (expr->type != EXPR_CALL)
 912                 return;
 913 
 914         arg = get_argument_from_call_expr(expr->args, param);
 915         if (!arg)
 916                 return;
 917 
 918         arg = strip_parens(arg);
 919         while (arg->type == EXPR_ASSIGNMENT && arg->op == '=')
 920                 arg = strip_parens(arg->left);
 921 
 922         name = get_variable_from_key(arg, key, &sym);
 923         if (!name || !sym)
 924                 goto free;
 925 
 926         sm = get_sm_state(SMATCH_EXTRA, name, sym);
 927         if (!sm || !sm->merged)
 928                 goto free;


1055         implied_true = filter_stack(gate_sm, pre_stree, false_stack, true_stack);
1056 
1057         free_stree(&pre_stree);
1058         free_slist(&true_stack);
1059         free_slist(&false_stack);
1060 
1061         FOR_EACH_SM(implied_true, tmp) {
1062                 set_state(tmp->owner, tmp->name, tmp->sym, tmp->state);
1063         } END_FOR_EACH_SM(tmp);
1064 
1065         free_stree(&implied_true);
1066 }
1067 
1068 int assume(struct expression *expr)
1069 {
1070         int orig_final_pass = final_pass;
1071 
1072         in_fake_env++;
1073         final_pass = 0;
1074         __push_fake_cur_stree();
1075         found_implications = 0;
1076         __split_whole_condition(expr);
1077         final_pass = orig_final_pass;
1078         in_fake_env--;
1079 
1080         return 1;
1081 }
1082 
1083 void end_assume(void)
1084 {
1085         __discard_false_states();
1086         __free_fake_cur_stree();
1087 }
1088 
1089 int impossible_assumption(struct expression *left, int op, sval_t sval)
1090 {
1091         struct expression *value;
1092         struct expression *comparison;
1093         int ret;
1094 
1095         value = value_expr(sval.value);




  48  * foo != 99 and merge it all back together.
  49  *
  50  * That is the implied state of bar.
  51  *
  52  * merge_slist() sets up ->pool.  An sm_state only has one ->pool and
  53  *    that is the pool where it was first set.  The my pool gets set when
  54  *    code paths merge.  States that have been set since the last merge do
  55  *    not have a ->pool.
  56  * merge_sm_state() sets ->left and ->right.  (These are the states which were
  57  *    merged to form the current state.)
  58  * a pool:  a pool is an slist that has been merged with another slist.
  59  */
  60 
  61 #include <sys/time.h>
  62 #include <time.h>
  63 #include "smatch.h"
  64 #include "smatch_slist.h"
  65 #include "smatch_extra.h"
  66 
  67 char *implied_debug_msg;

  68 
  69 bool implications_off;
  70 
  71 #define implied_debug 0
  72 #define DIMPLIED(msg...) do { if (implied_debug) printf(msg); } while (0)
  73 
  74 /*
  75  * tmp_range_list():
  76  * It messes things up to free range list allocations.  This helper fuction
  77  * lets us reuse memory instead of doing new allocations.
  78  */
  79 static struct range_list *tmp_range_list(struct symbol *type, long long num)
  80 {
  81         static struct range_list *my_list = NULL;
  82         static struct data_range *my_range;
  83 
  84         __free_ptr_list((struct ptr_list **)&my_list);
  85         my_range = alloc_range(ll_to_sval(num), ll_to_sval(num));
  86         add_ptr_list(&my_list, my_range);
  87         return my_list;
  88 }
  89 
  90 static void print_debug_tf(struct sm_state *sm, int istrue, int isfalse)
  91 {
  92         if (!implied_debug && !option_debug)
  93                 return;
  94 
  95         if (istrue && isfalse) {
  96                 printf("%s: %d: does not exist.\n", show_sm(sm), sm->line);
  97         } else if (istrue) {
  98                 printf("'%s = %s' from %d is true. %s[stree %d]\n", sm->name, show_state(sm->state),
  99                         sm->line, sm->merged ? "[merged]" : "[leaf]",
 100                         get_stree_id(sm->pool));
 101         } else if (isfalse) {
 102                 printf("'%s = %s' from %d is false. %s[stree %d]\n", sm->name, show_state(sm->state),
 103                         sm->line,
 104                         sm->merged ? "[merged]" : "[leaf]",
 105                         get_stree_id(sm->pool));
 106         } else {
 107                 printf("'%s = %s' from %d could be true or false. %s[stree %d]\n", sm->name,
 108                         show_state(sm->state), sm->line,
 109                         sm->merged ? "[merged]" : "[leaf]",
 110                         get_stree_id(sm->pool));
 111         }
 112 }


 128 
 129         orig_rl = cast_rl(rl_type(rl), estate_rl(sm->state));
 130         split_comparison_rl(orig_rl, comparison, rl, &true_rl, &false_rl, NULL, NULL);
 131 
 132         true_rl = rl_truncate_cast(estate_type(sm->state), true_rl);
 133         false_rl = rl_truncate_cast(estate_type(sm->state), false_rl);
 134         if (is_whole_rl(true_rl) || is_whole_rl(false_rl) ||
 135             !true_rl || !false_rl ||
 136             rl_equiv(orig_rl, true_rl) || rl_equiv(orig_rl, false_rl) ||
 137             rl_equiv(estate_rl(sm->state), true_rl) || rl_equiv(estate_rl(sm->state), false_rl))
 138                 return 0;
 139 
 140         if (rl_intersection(true_rl, false_rl)) {
 141                 sm_perror("parsing (%s (%s) %s %s)",
 142                         sm->name, sm->state->name, show_special(comparison), show_rl(rl));
 143                 sm_msg("true_rl = %s false_rl = %s intersection = %s",
 144                        show_rl(true_rl), show_rl(false_rl), show_rl(rl_intersection(true_rl, false_rl)));
 145                 return 0;
 146         }
 147 
 148         if (implied_debug)
 149                 sm_msg("fake_history: %s vs %s.  %s %s %s. --> T: %s F: %s",
 150                        sm->name, show_rl(rl), sm->state->name, show_special(comparison), show_rl(rl),
 151                        show_rl(true_rl), show_rl(false_rl));
 152 
 153         true_sm = clone_sm(sm);
 154         false_sm = clone_sm(sm);
 155 
 156         true_sm->state = clone_partial_estate(sm->state, true_rl);
 157         free_slist(&true_sm->possible);
 158         add_possible_sm(true_sm, true_sm);
 159         false_sm->state = clone_partial_estate(sm->state, false_rl);
 160         free_slist(&false_sm->possible);
 161         add_possible_sm(false_sm, false_sm);
 162 
 163         true_stree = clone_stree(sm->pool);
 164         false_stree = clone_stree(sm->pool);
 165 
 166         overwrite_sm_state_stree(&true_stree, true_sm);
 167         overwrite_sm_state_stree(&false_stree, false_sm);
 168 
 169         true_sm->pool = true_stree;
 170         false_sm->pool = false_stree;
 171 
 172         sm->merged = 1;
 173         sm->left = true_sm;
 174         sm->right = false_sm;
 175 
 176         return 1;
 177 }
 178 
 179 /*


 251         print_debug_tf(sm, istrue, isfalse);
 252 
 253         /* give up if we have borrowed implications (smatch_equiv.c) */
 254         if (sm->sym != gate_sm->sym ||
 255             strcmp(sm->name, gate_sm->name) != 0) {
 256                 if (mixed)
 257                         *mixed = 1;
 258         }
 259 
 260         if (mixed && !*mixed && !is_merged(sm) && !istrue && !isfalse) {
 261                 if (!create_fake_history(sm, comparison, rl))
 262                         *mixed = 1;
 263         }
 264 
 265         if (istrue)
 266                 add_pool(true_stack, sm);
 267         else if (isfalse)
 268                 add_pool(false_stack, sm);
 269         else
 270                 add_pool(maybe_stack, sm);

 271 }
 272 
 273 static int is_checked(struct state_list *checked, struct sm_state *sm)
 274 {
 275         struct sm_state *tmp;
 276 
 277         FOR_EACH_PTR(checked, tmp) {
 278                 if (tmp == sm)
 279                         return 1;
 280         } END_FOR_EACH_PTR(tmp);
 281         return 0;
 282 }
 283 
 284 /*
 285  * separate_pools():
 286  * Example code:  if (foo == 99) {
 287  *
 288  * Say 'foo' is a merged state that has many possible values.  It is the combination
 289  * of merges.  separate_pools() iterates through the pools recursively and calls
 290  * do_compare() for each time 'foo' was set.
 291  */
 292 static void __separate_pools(struct sm_state *sm, int comparison, struct range_list *rl,
 293                         struct state_list **true_stack,
 294                         struct state_list **maybe_stack,
 295                         struct state_list **false_stack,
 296                         struct state_list **checked, int *mixed, struct sm_state *gate_sm,
 297                         struct timeval *start_time)
 298 {
 299         int free_checked = 0;
 300         struct state_list *checked_states = NULL;
 301         struct timeval now;
 302 
 303         if (!sm)
 304                 return;
 305 
 306         gettimeofday(&now, NULL);
 307         if (now.tv_usec - start_time->tv_usec > 1000000) {
 308                 if (implied_debug) {
 309                         sm_msg("debug: %s: implications taking too long.  (%s %s %s)",
 310                                __func__, sm->state->name, show_special(comparison), show_rl(rl));
 311                 }
 312                 if (mixed)
 313                         *mixed = 1;












 314         }


 315 
 316         if (checked == NULL) {
 317                 checked = &checked_states;
 318                 free_checked = 1;
 319         }
 320         if (is_checked(*checked, sm))
 321                 return;
 322         add_ptr_list(checked, sm);
 323 
 324         do_compare(sm, comparison, rl, true_stack, maybe_stack, false_stack, mixed, gate_sm);
 325 
 326         __separate_pools(sm->left, comparison, rl, true_stack, maybe_stack, false_stack, checked, mixed, gate_sm, start_time);
 327         __separate_pools(sm->right, comparison, rl, true_stack, maybe_stack, false_stack, checked, mixed, gate_sm, start_time);
 328         if (free_checked)
 329                 free_slist(checked);
 330 }
 331 
 332 static void separate_pools(struct sm_state *sm, int comparison, struct range_list *rl,
 333                         struct state_list **true_stack,
 334                         struct state_list **false_stack,
 335                         struct state_list **checked, int *mixed)
 336 {
 337         struct state_list *maybe_stack = NULL;
 338         struct sm_state *tmp;
 339         struct timeval start_time;
 340 

 341 
 342         gettimeofday(&start_time, NULL);
 343         __separate_pools(sm, comparison, rl, true_stack, &maybe_stack, false_stack, checked, mixed, sm, &start_time);
 344 
 345         if (implied_debug) {
 346                 struct sm_state *sm;
 347 
 348                 FOR_EACH_PTR(*true_stack, sm) {
 349                         sm_msg("TRUE %s [stree %d]", show_sm(sm), get_stree_id(sm->pool));
 350                 } END_FOR_EACH_PTR(sm);
 351 
 352                 FOR_EACH_PTR(maybe_stack, sm) {
 353                         sm_msg("MAYBE %s %s[stree %d]",
 354                                show_sm(sm), sm->merged ? "(merged) ": "", get_stree_id(sm->pool));
 355                 } END_FOR_EACH_PTR(sm);
 356 
 357                 FOR_EACH_PTR(*false_stack, sm) {
 358                         sm_msg("FALSE %s [stree %d]", show_sm(sm), get_stree_id(sm->pool));
 359                 } END_FOR_EACH_PTR(sm);
 360         }
 361         /* if it's a maybe then remove it */
 362         FOR_EACH_PTR(maybe_stack, tmp) {
 363                 remove_pool(false_stack, tmp->pool);
 364                 remove_pool(true_stack, tmp->pool);
 365         } END_FOR_EACH_PTR(tmp);
 366 
 367         /* if it's both true and false remove it from both */
 368         FOR_EACH_PTR(*true_stack, tmp) {
 369                 if (remove_pool(false_stack, tmp->pool))
 370                         DELETE_CURRENT_PTR(tmp);
 371         } END_FOR_EACH_PTR(tmp);
 372 }
 373 
 374 static int sm_in_keep_leafs(struct sm_state *sm, const struct state_list *keep_gates)
 375 {
 376         struct sm_state *tmp, *old;
 377 
 378         FOR_EACH_PTR(keep_gates, tmp) {
 379                 if (is_merged(tmp))
 380                         continue;
 381                 old = get_sm_state_stree(tmp->pool, sm->owner, sm->name, sm->sym);
 382                 if (!old)
 383                         continue;
 384                 if (old == sm)
 385                         return 1;
 386         } END_FOR_EACH_PTR(tmp);
 387         return 0;
 388 }
 389 
 390 static int going_too_slow(void)
 391 {
 392         static void *printed;
 393 
 394         if (out_of_memory()) {
 395                 implications_off = true;
 396                 return 1;
 397         }
 398 
 399         if (!option_timeout || time_parsing_function() < option_timeout) {
 400                 implications_off = false;
 401                 return 0;
 402         }
 403 
 404         if (!__inline_fn && printed != cur_func_sym) {
 405                 if (!is_skipped_function())
 406                         sm_perror("turning off implications after %d seconds", option_timeout);
 407                 printed = cur_func_sym;
 408         }
 409         implications_off = true;
 410         return 1;
 411 }
 412 
 413 static char *sm_state_info(struct sm_state *sm)
 414 {
 415         static char buf[512];
 416         int n = 0;
 417 
 418         n += snprintf(buf + n, sizeof(buf) - n, "[stree %d line %d] ",
 419                       get_stree_id(sm->pool),  sm->line);
 420         if (n >= sizeof(buf))
 421                 return buf;
 422         n += snprintf(buf + n, sizeof(buf) - n, "%s ", show_sm(sm));
 423         if (n >= sizeof(buf))
 424                 return buf;
 425         n += snprintf(buf + n, sizeof(buf) - n, "left = %s [stree %d] ",
 426                       sm->left ? sm->left->state->name : "<none>",
 427                       sm->left ? get_stree_id(sm->left->pool) : -1);
 428         if (n >= sizeof(buf))
 429                 return buf;
 430         n += snprintf(buf + n, sizeof(buf) - n, "right = %s [stree %d]",
 431                       sm->right ? sm->right->state->name : "<none>",
 432                       sm->right ? get_stree_id(sm->right->pool) : -1);
 433         return buf;
 434 }
 435 
 436 /*
 437  * NOTE: If a state is in both the keep stack and the remove stack then that is
 438  * a bug.  Only add states which are definitely true or definitely false.  If
 439  * you have a leaf state that could be both true and false, then create a fake
 440  * split history where one side is true and one side is false.  Otherwise, if
 441  * you can't do that, then don't add it to either list.
 442  */
 443 #define RECURSE_LIMIT 300
 444 struct sm_state *filter_pools(struct sm_state *sm,
 445                               const struct state_list *remove_stack,
 446                               const struct state_list *keep_stack,
 447                               int *modified, int *recurse_cnt,
 448                               struct timeval *start, int *skip, int *bail)
 449 {
 450         struct sm_state *ret = NULL;
 451         struct sm_state *left;
 452         struct sm_state *right;
 453         int removed = 0;
 454         struct timeval now;
 455 
 456         if (!sm)
 457                 return NULL;
 458         if (*bail)
 459                 return NULL;



 460         gettimeofday(&now, NULL);
 461         if (now.tv_usec - start->tv_usec > 3000000) {
 462                 DIMPLIED("%s: implications taking too long: %s\n", __func__, sm_state_info(sm));
 463                 *bail = 1;
 464                 return NULL;


 465         }
 466         if ((*recurse_cnt)++ > RECURSE_LIMIT) {
 467                 DIMPLIED("%s: recursed too far:  %s\n", __func__, sm_state_info(sm));
 468                 *skip = 1;
 469                 return NULL;
 470         }
 471 
 472         if (pool_in_pools(sm->pool, remove_stack)) {
 473                 DIMPLIED("%s: remove: %s\n", __func__, sm_state_info(sm));
 474                 *modified = 1;
 475                 return NULL;
 476         }
 477 
 478         if (!is_merged(sm) || pool_in_pools(sm->pool, keep_stack) || sm_in_keep_leafs(sm, keep_stack)) {
 479                 DIMPLIED("%s: keep %s (%s, %s, %s): %s\n", __func__, sm->state->name,
 480                         is_merged(sm) ? "merged" : "not merged",
 481                         pool_in_pools(sm->pool, keep_stack) ? "not in keep pools" : "in keep pools",
 482                         sm_in_keep_leafs(sm, keep_stack) ? "reachable keep leaf" : "no keep leaf",
 483                         sm_state_info(sm));
 484                 return sm;
 485         }
 486 
 487         left = filter_pools(sm->left, remove_stack, keep_stack, &removed, recurse_cnt, start, skip, bail);
 488         right = filter_pools(sm->right, remove_stack, keep_stack, &removed, recurse_cnt, start, skip, bail);
 489         if (*bail || *skip)
 490                 return NULL;



 491         if (!removed) {
 492                 DIMPLIED("%s: kept all: %s\n", __func__, sm_state_info(sm));
 493                 return sm;
 494         }
 495         *modified = 1;
 496         if (!left && !right) {
 497                 DIMPLIED("%s: removed all: %s\n", __func__, sm_state_info(sm));
 498                 return NULL;
 499         }
 500 
 501         if (!left) {
 502                 ret = clone_sm(right);
 503                 ret->merged = 1;
 504                 ret->right = right;
 505                 ret->left = NULL;
 506         } else if (!right) {
 507                 ret = clone_sm(left);
 508                 ret->merged = 1;
 509                 ret->left = left;
 510                 ret->right = NULL;
 511         } else {
 512                 if (left->sym != sm->sym || strcmp(left->name, sm->name) != 0) {
 513                         left = clone_sm(left);
 514                         left->sym = sm->sym;
 515                         left->name = sm->name;
 516                 }
 517                 if (right->sym != sm->sym || strcmp(right->name, sm->name) != 0) {
 518                         right = clone_sm(right);
 519                         right->sym = sm->sym;
 520                         right->name = sm->name;
 521                 }
 522                 ret = merge_sm_states(left, right);
 523         }
 524 
 525         ret->pool = sm->pool;
 526 
 527         DIMPLIED("%s: partial: %s\n", __func__, sm_state_info(sm));

 528         return ret;
 529 }
 530 
 531 static struct stree *filter_stack(struct sm_state *gate_sm,
 532                                        struct stree *pre_stree,
 533                                        const struct state_list *remove_stack,
 534                                        const struct state_list *keep_stack)
 535 {
 536         struct stree *ret = NULL;
 537         struct sm_state *tmp;
 538         struct sm_state *filtered_sm;
 539         int modified;
 540         int recurse_cnt;
 541         struct timeval start;
 542         int skip;
 543         int bail = 0;
 544 
 545         if (!remove_stack)
 546                 return NULL;
 547 
 548         gettimeofday(&start, NULL);


 549         FOR_EACH_SM(pre_stree, tmp) {
 550                 if (!tmp->merged || sm_in_keep_leafs(tmp, keep_stack))


 551                         continue;


 552                 modified = 0;
 553                 recurse_cnt = 0;
 554                 skip = 0;
 555                 filtered_sm = filter_pools(tmp, remove_stack, keep_stack, &modified, &recurse_cnt, &start, &skip, &bail);
 556                 if (going_too_slow())
 557                         return NULL;
 558                 if (bail)
 559                         return ret;  /* Return the implications we figured out before time ran out. */
 560 
 561 
 562                 if (skip || !filtered_sm || !modified)
 563                         continue;
 564                 /* the assignments here are for borrowed implications */
 565                 filtered_sm->name = tmp->name;
 566                 filtered_sm->sym = tmp->sym;
 567                 avl_insert(&ret, filtered_sm);



 568         } END_FOR_EACH_SM(tmp);
 569         return ret;
 570 }
 571 
 572 static void separate_and_filter(struct sm_state *sm, int comparison, struct range_list *rl,
 573                 struct stree *pre_stree,
 574                 struct stree **true_states,
 575                 struct stree **false_states,
 576                 int *mixed)
 577 {
 578         struct state_list *true_stack = NULL;
 579         struct state_list *false_stack = NULL;
 580         struct timeval time_before;
 581         struct timeval time_after;
 582         int sec;
 583 
 584         gettimeofday(&time_before, NULL);
 585 
 586         DIMPLIED("checking implications: (%s (%s) %s %s)\n",
 587                  sm->name, sm->state->name, show_special(comparison), show_rl(rl));
 588 
 589         if (!is_merged(sm)) {
 590                 DIMPLIED("%d '%s' from line %d is not merged.\n", get_lineno(), sm->name, sm->line);
 591                 return;
 592         }
 593 





 594         separate_pools(sm, comparison, rl, &true_stack, &false_stack, NULL, mixed);
 595 
 596         DIMPLIED("filtering true stack.\n");
 597         *true_states = filter_stack(sm, pre_stree, false_stack, true_stack);
 598         DIMPLIED("filtering false stack.\n");
 599         *false_states = filter_stack(sm, pre_stree, true_stack, false_stack);
 600         free_slist(&true_stack);
 601         free_slist(&false_stack);
 602         if (implied_debug) {
 603                 printf("These are the implied states for the true path: (%s (%s) %s %s)\n",
 604                        sm->name, sm->state->name, show_special(comparison), show_rl(rl));
 605                 __print_stree(*true_states);
 606                 printf("These are the implied states for the false path: (%s (%s) %s %s)\n",
 607                        sm->name, sm->state->name, show_special(comparison), show_rl(rl));
 608                 __print_stree(*false_states);
 609         }
 610 
 611         gettimeofday(&time_after, NULL);
 612         sec = time_after.tv_sec - time_before.tv_sec;
 613         if (option_timeout && sec > option_timeout) {

 614                 sm_perror("Function too hairy.  Ignoring implications after %d seconds.", sec);
 615         }
 616 }
 617 
 618 static struct expression *get_last_expr(struct statement *stmt)
 619 {
 620         struct statement *last;
 621 
 622         last = last_ptr_list((struct ptr_list *)stmt->stmts);
 623         if (last->type == STMT_EXPRESSION)
 624                 return last->expression;
 625 
 626         if (last->type == STMT_LABEL) {
 627                 if (last->label_statement &&
 628                     last->label_statement->type == STMT_EXPRESSION)
 629                         return last->label_statement->expression;
 630         }
 631 
 632         return NULL;
 633 }


 811         struct state_list *false_stack = NULL;
 812         struct stree *pre_stree;
 813         struct sm_state *sm;
 814 
 815         sm = stored_condition_implication_hook(expr, &true_stack, &false_stack);
 816         if (!sm)
 817                 return 0;
 818 
 819         pre_stree = clone_stree(__get_cur_stree());
 820 
 821         *implied_true = filter_stack(sm, pre_stree, false_stack, true_stack);
 822         *implied_false = filter_stack(sm, pre_stree, true_stack, false_stack);
 823 
 824         free_stree(&pre_stree);
 825         free_slist(&true_stack);
 826         free_slist(&false_stack);
 827 
 828         return 1;
 829 }
 830 

 831 static struct stree *saved_implied_true;
 832 static struct stree *saved_implied_false;
 833 static struct stree *extra_saved_implied_true;
 834 static struct stree *extra_saved_implied_false;
 835 
 836 static void separate_extra_states(struct stree **implied_true,
 837                                   struct stree **implied_false)
 838 {
 839         struct sm_state *sm;
 840 
 841         /* We process extra states later to preserve the implications. */
 842         FOR_EACH_SM(*implied_true, sm) {
 843                 if (sm->owner == SMATCH_EXTRA)
 844                         overwrite_sm_state_stree(&extra_saved_implied_true, sm);
 845         } END_FOR_EACH_SM(sm);
 846         FOR_EACH_SM(extra_saved_implied_true, sm) {
 847                 delete_state_stree(implied_true, sm->owner, sm->name, sm->sym);
 848         } END_FOR_EACH_SM(sm);
 849 
 850         FOR_EACH_SM(*implied_false, sm) {
 851                 if (sm->owner == SMATCH_EXTRA)
 852                         overwrite_sm_state_stree(&extra_saved_implied_false, sm);
 853         } END_FOR_EACH_SM(sm);
 854         FOR_EACH_SM(extra_saved_implied_false, sm) {
 855                 delete_state_stree(implied_false, sm->owner, sm->name, sm->sym);
 856         } END_FOR_EACH_SM(sm);
 857 }
 858 
 859 static void get_tf_states(struct expression *expr,
 860                           struct stree **implied_true,
 861                           struct stree **implied_false)
 862 {
 863         if (handled_by_comparison_hook(expr, implied_true, implied_false))
 864                 return;
 865 
 866         if (handled_by_extra_states(expr, implied_true, implied_false)) {
 867                 separate_extra_states(implied_true, implied_false);
 868                 return;
 869         }
 870 
 871         if (handled_by_stored_conditions(expr, implied_true, implied_false))


 872                 return;


 873 }
 874 
 875 static void save_implications_hook(struct expression *expr)
 876 {
 877         if (going_too_slow())
 878                 return;
 879         get_tf_states(expr, &saved_implied_true, &saved_implied_false);
 880 }
 881 
 882 static void set_implied_states(struct expression *expr)
 883 {
 884         struct sm_state *sm;
 885 
 886         FOR_EACH_SM(saved_implied_true, sm) {
 887                 __set_true_false_sm(sm, NULL);
 888         } END_FOR_EACH_SM(sm);
 889         free_stree(&saved_implied_true);
 890 
 891         FOR_EACH_SM(saved_implied_false, sm) {
 892                 __set_true_false_sm(NULL, sm);
 893         } END_FOR_EACH_SM(sm);
 894         free_stree(&saved_implied_false);
 895 }
 896 
 897 static void set_extra_implied_states(struct expression *expr)
 898 {
 899         saved_implied_true = extra_saved_implied_true;
 900         saved_implied_false = extra_saved_implied_false;
 901         extra_saved_implied_true = NULL;
 902         extra_saved_implied_false = NULL;
 903         set_implied_states(NULL);
 904 }
 905 
 906 void param_limit_implications(struct expression *expr, int param, char *key, char *value)
 907 {
 908         struct expression *arg;
 909         struct symbol *compare_type;
 910         char *name;
 911         struct symbol *sym;
 912         struct sm_state *sm;
 913         struct sm_state *tmp;
 914         struct stree *implied_true = NULL;
 915         struct stree *implied_false = NULL;
 916         struct range_list *orig, *limit;
 917 
 918         if (time_parsing_function() > 40)
 919                 return;
 920 
 921         while (expr->type == EXPR_ASSIGNMENT)
 922                 expr = strip_expr(expr->right);
 923         if (expr->type != EXPR_CALL)
 924                 return;
 925 
 926         arg = get_argument_from_call_expr(expr->args, param);
 927         if (!arg)
 928                 return;
 929 
 930         arg = strip_parens(arg);
 931         while (arg->type == EXPR_ASSIGNMENT && arg->op == '=')
 932                 arg = strip_parens(arg->left);
 933 
 934         name = get_variable_from_key(arg, key, &sym);
 935         if (!name || !sym)
 936                 goto free;
 937 
 938         sm = get_sm_state(SMATCH_EXTRA, name, sym);
 939         if (!sm || !sm->merged)
 940                 goto free;


1067         implied_true = filter_stack(gate_sm, pre_stree, false_stack, true_stack);
1068 
1069         free_stree(&pre_stree);
1070         free_slist(&true_stack);
1071         free_slist(&false_stack);
1072 
1073         FOR_EACH_SM(implied_true, tmp) {
1074                 set_state(tmp->owner, tmp->name, tmp->sym, tmp->state);
1075         } END_FOR_EACH_SM(tmp);
1076 
1077         free_stree(&implied_true);
1078 }
1079 
1080 int assume(struct expression *expr)
1081 {
1082         int orig_final_pass = final_pass;
1083 
1084         in_fake_env++;
1085         final_pass = 0;
1086         __push_fake_cur_stree();

1087         __split_whole_condition(expr);
1088         final_pass = orig_final_pass;
1089         in_fake_env--;
1090 
1091         return 1;
1092 }
1093 
1094 void end_assume(void)
1095 {
1096         __discard_false_states();
1097         __free_fake_cur_stree();
1098 }
1099 
1100 int impossible_assumption(struct expression *left, int op, sval_t sval)
1101 {
1102         struct expression *value;
1103         struct expression *comparison;
1104         int ret;
1105 
1106         value = value_expr(sval.value);