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  * Copyright 2019 Joyent, Inc.
  18  */
  19 
  20 /*
  21  * Imagine we have this code:
  22  * foo = 1;
  23  * if (bar)
  24  *         foo = 99;
  25  * else
  26  *         frob();
  27  *                   //  <-- point #1
  28  * if (foo == 99)    //  <-- point #2
  29  *         bar->baz; //  <-- point #3
  30  *
  31  *
  32  * At point #3 bar is non null and can be dereferenced.
  33  *
  34  * It's smatch_implied.c which sets bar to non null at point #2.
  35  *
  36  * At point #1 merge_slist() stores the list of states from both
  37  * the true and false paths.  On the true path foo == 99 and on
  38  * the false path foo == 1.  merge_slist() sets their pool
  39  * list to show the other states which were there when foo == 99.
  40  *
  41  * When it comes to the if (foo == 99) the smatch implied hook
  42  * looks for all the pools where foo was not 99.  It makes a list
  43  * of those.
  44  *
  45  * Then for bar (and all the other states) it says, ok bar is a
  46  * merged state that came from these previous states.  We'll
  47  * chop out all the states where it came from a pool where
  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 <time.h>
  62 #include "smatch.h"
  63 #include "smatch_slist.h"
  64 #include "smatch_extra.h"
  65 
  66 char *implied_debug_msg;
  67 
  68 bool implications_off;
  69 
  70 #define implied_debug 0
  71 #define DIMPLIED(msg...) do { if (implied_debug) printf(msg); } while (0)
  72 
  73 bool debug_implied(void)
  74 {
  75         if (option_debug)
  76                 return true;
  77         return implied_debug;
  78 }
  79 
  80 /*
  81  * tmp_range_list():
  82  * It messes things up to free range list allocations.  This helper fuction
  83  * lets us reuse memory instead of doing new allocations.
  84  */
  85 static struct range_list *tmp_range_list(struct symbol *type, long long num)
  86 {
  87         static struct range_list *my_list = NULL;
  88         static struct data_range *my_range;
  89 
  90         __free_ptr_list((struct ptr_list **)&my_list);
  91         my_range = alloc_range(ll_to_sval(num), ll_to_sval(num));
  92         add_ptr_list(&my_list, my_range);
  93         return my_list;
  94 }
  95 
  96 static const char *show_comparison(int op)
  97 {
  98         if (op == PARAM_LIMIT)
  99                 return "<lim>";
 100         return show_special(op);
 101 }
 102 
 103 static void print_debug_tf(struct sm_state *sm, int istrue, int isfalse)
 104 {
 105         if (!implied_debug && !option_debug)
 106                 return;
 107 
 108         if (istrue && isfalse) {
 109                 printf("%s: %d: does not exist.\n", show_sm(sm), sm->line);
 110         } else if (istrue) {
 111                 printf("'%s = %s' from %d is true. %s[stree %d]\n", sm->name, show_state(sm->state),
 112                         sm->line, sm->merged ? "[merged]" : "[leaf]",
 113                         get_stree_id(sm->pool));
 114         } else if (isfalse) {
 115                 printf("'%s = %s' from %d is false. %s[stree %d]\n", sm->name, show_state(sm->state),
 116                         sm->line,
 117                         sm->merged ? "[merged]" : "[leaf]",
 118                         get_stree_id(sm->pool));
 119         } else {
 120                 printf("'%s = %s' from %d could be true or false. %s[stree %d]\n", sm->name,
 121                         show_state(sm->state), sm->line,
 122                         sm->merged ? "[merged]" : "[leaf]",
 123                         get_stree_id(sm->pool));
 124         }
 125 }
 126 
 127 void split_comparison_helper(struct range_list *left_orig, int op, struct range_list *right_orig,
 128                 struct range_list **left_true_rl, struct range_list **left_false_rl)
 129 {
 130         if (op == PARAM_LIMIT) {
 131                 *left_true_rl = rl_intersection(left_orig, right_orig);
 132                 *left_false_rl = rl_filter(left_orig, right_orig);
 133                 return;
 134         }
 135 
 136         split_comparison_rl(left_orig, op, right_orig, left_true_rl, left_false_rl, NULL, NULL);
 137 }
 138 
 139 static int create_fake_history(struct sm_state *sm, int comparison, struct range_list *rl)
 140 {
 141         struct range_list *orig_rl;
 142         struct range_list *true_rl, *false_rl;
 143         struct stree *true_stree, *false_stree;
 144         struct sm_state *true_sm, *false_sm;
 145         sval_t sval;
 146 
 147         if (is_merged(sm) || sm->left || sm->right)
 148                 return 0;
 149         if (!rl_to_sval(rl, &sval))
 150                 return 0;
 151         if (!estate_rl(sm->state))
 152                 return 0;
 153 
 154         orig_rl = cast_rl(rl_type(rl), estate_rl(sm->state));
 155         split_comparison_helper(orig_rl, comparison, rl, &true_rl, &false_rl);
 156 
 157         true_rl = rl_truncate_cast(estate_type(sm->state), true_rl);
 158         false_rl = rl_truncate_cast(estate_type(sm->state), false_rl);
 159         if (is_whole_rl(true_rl) || is_whole_rl(false_rl) ||
 160             !true_rl || !false_rl ||
 161             rl_equiv(orig_rl, true_rl) || rl_equiv(orig_rl, false_rl) ||
 162             rl_equiv(estate_rl(sm->state), true_rl) || rl_equiv(estate_rl(sm->state), false_rl))
 163                 return 0;
 164 
 165         if (rl_intersection(true_rl, false_rl)) {
 166                 /*
 167                  * Normally these won't intersect, but one exception is when
 168                  * we're dealing with mtags.  We have a long list of mtags and
 169                  * then negate the list.  Now it's over the limit for mtag list
 170                  * length and we squash it down to 4096-ptr_max.  So then it's
 171                  * possible for the true and false rl to overlap.
 172                  */
 173                 return 0;
 174         }
 175 
 176         if (implied_debug)
 177                 sm_msg("fake_history: %s vs %s.  %s %s %s. --> T: %s F: %s",
 178                        sm->name, show_rl(rl), sm->state->name, show_comparison(comparison), show_rl(rl),
 179                        show_rl(true_rl), show_rl(false_rl));
 180 
 181         true_sm = clone_sm(sm);
 182         false_sm = clone_sm(sm);
 183 
 184         true_sm->state = clone_partial_estate(sm->state, true_rl);
 185         free_slist(&true_sm->possible);
 186         add_possible_sm(true_sm, true_sm);
 187         false_sm->state = clone_partial_estate(sm->state, false_rl);
 188         free_slist(&false_sm->possible);
 189         add_possible_sm(false_sm, false_sm);
 190 
 191         true_stree = clone_stree(sm->pool);
 192         false_stree = clone_stree(sm->pool);
 193 
 194         overwrite_sm_state_stree(&true_stree, true_sm);
 195         overwrite_sm_state_stree(&false_stree, false_sm);
 196 
 197         true_sm->pool = true_stree;
 198         false_sm->pool = false_stree;
 199 
 200         sm->merged = 1;
 201         sm->left = true_sm;
 202         sm->right = false_sm;
 203 
 204         return 1;
 205 }
 206 
 207 /*
 208  * add_pool() adds a slist to *pools. If the slist has already been
 209  * added earlier then it doesn't get added a second time.
 210  */
 211 void add_pool(struct state_list **pools, struct sm_state *new)
 212 {
 213         struct sm_state *tmp;
 214 
 215         FOR_EACH_PTR(*pools, tmp) {
 216                 if (tmp->pool < new->pool)
 217                         continue;
 218                 else if (tmp->pool == new->pool) {
 219                         return;
 220                 } else {
 221                         INSERT_CURRENT(new, tmp);
 222                         return;
 223                 }
 224         } END_FOR_EACH_PTR(tmp);
 225         add_ptr_list(pools, new);
 226 }
 227 
 228 static int pool_in_pools(struct stree *pool,
 229                          const struct state_list *slist)
 230 {
 231         struct sm_state *tmp;
 232 
 233         FOR_EACH_PTR(slist, tmp) {
 234                 if (!tmp->pool)
 235                         continue;
 236                 if (tmp->pool == pool)
 237                         return 1;
 238         } END_FOR_EACH_PTR(tmp);
 239         return 0;
 240 }
 241 
 242 static int remove_pool(struct state_list **pools, struct stree *remove)
 243 {
 244         struct sm_state *tmp;
 245         int ret = 0;
 246 
 247         FOR_EACH_PTR(*pools, tmp) {
 248                 if (tmp->pool == remove) {
 249                         DELETE_CURRENT_PTR(tmp);
 250                         ret = 1;
 251                 }
 252         } END_FOR_EACH_PTR(tmp);
 253 
 254         return ret;
 255 }
 256 
 257 static bool possibly_true_helper(struct range_list *var_rl, int comparison, struct range_list *rl)
 258 {
 259         if (comparison == PARAM_LIMIT) {
 260                 struct range_list *intersect;
 261 
 262                 intersect = rl_intersection(var_rl, rl);
 263                 if (intersect)
 264                         return true;
 265                 return false;
 266         }
 267         return possibly_true_rl(var_rl, comparison, rl);
 268 }
 269 
 270 static bool possibly_false_helper(struct range_list *var_rl, int comparison, struct range_list *rl)
 271 {
 272         if (comparison == PARAM_LIMIT) {
 273                 struct range_list *intersect;
 274 
 275                 intersect = rl_intersection(var_rl, rl);
 276                 if (!rl_equiv(var_rl, intersect))
 277                         return true;
 278                 return false;
 279         }
 280         return possibly_false_rl(var_rl, comparison, rl);
 281 }
 282 
 283 /*
 284  * If 'foo' == 99 add it that pool to the true pools.  If it's false, add it to
 285  * the false pools.  If we're not sure, then we don't add it to either.
 286  */
 287 static void do_compare(struct sm_state *sm, int comparison, struct range_list *rl,
 288                         struct state_list **true_stack,
 289                         struct state_list **maybe_stack,
 290                         struct state_list **false_stack,
 291                         int *mixed, struct sm_state *gate_sm)
 292 {
 293         int istrue;
 294         int isfalse;
 295         struct range_list *var_rl;
 296 
 297         if (!sm->pool)
 298                 return;
 299 
 300         var_rl = cast_rl(rl_type(rl), estate_rl(sm->state));
 301 
 302         istrue = !possibly_false_helper(var_rl, comparison, rl);
 303         isfalse = !possibly_true_helper(var_rl, comparison, rl);
 304 
 305         print_debug_tf(sm, istrue, isfalse);
 306 
 307         /* give up if we have borrowed implications (smatch_equiv.c) */
 308         if (sm->sym != gate_sm->sym ||
 309             strcmp(sm->name, gate_sm->name) != 0) {
 310                 if (mixed)
 311                         *mixed = 1;
 312         }
 313 
 314         if (mixed && !*mixed && !is_merged(sm) && !istrue && !isfalse) {
 315                 if (!create_fake_history(sm, comparison, rl))
 316                         *mixed = 1;
 317         }
 318 
 319         if (istrue)
 320                 add_pool(true_stack, sm);
 321         else if (isfalse)
 322                 add_pool(false_stack, sm);
 323         else
 324                 add_pool(maybe_stack, sm);
 325 }
 326 
 327 static int is_checked(struct state_list *checked, struct sm_state *sm)
 328 {
 329         struct sm_state *tmp;
 330 
 331         FOR_EACH_PTR(checked, tmp) {
 332                 if (tmp == sm)
 333                         return 1;
 334         } END_FOR_EACH_PTR(tmp);
 335         return 0;
 336 }
 337 
 338 /*
 339  * separate_pools():
 340  * Example code:  if (foo == 99) {
 341  *
 342  * Say 'foo' is a merged state that has many possible values.  It is the combination
 343  * of merges.  separate_pools() iterates through the pools recursively and calls
 344  * do_compare() for each time 'foo' was set.
 345  */
 346 static void __separate_pools(struct sm_state *sm, int comparison, struct range_list *rl,
 347                         struct state_list **true_stack,
 348                         struct state_list **maybe_stack,
 349                         struct state_list **false_stack,
 350                         struct state_list **checked, int *mixed, struct sm_state *gate_sm,
 351                         struct timeval *start_time)
 352 {
 353         int free_checked = 0;
 354         struct state_list *checked_states = NULL;
 355         struct timeval now, diff;
 356 
 357         if (!sm)
 358                 return;
 359 
 360         gettimeofday(&now, NULL);
 361         timersub(&now, start_time, &diff);
 362         if (diff.tv_sec >= 1) {
 363                 if (implied_debug) {
 364                         sm_msg("debug: %s: implications taking too long.  (%s %s %s)",
 365                                __func__, sm->state->name, show_comparison(comparison), show_rl(rl));
 366                 }
 367                 if (mixed)
 368                         *mixed = 1;
 369         }
 370 
 371         if (checked == NULL) {
 372                 checked = &checked_states;
 373                 free_checked = 1;
 374         }
 375         if (is_checked(*checked, sm))
 376                 return;
 377         add_ptr_list(checked, sm);
 378 
 379         do_compare(sm, comparison, rl, true_stack, maybe_stack, false_stack, mixed, gate_sm);
 380 
 381         __separate_pools(sm->left, comparison, rl, true_stack, maybe_stack, false_stack, checked, mixed, gate_sm, start_time);
 382         __separate_pools(sm->right, comparison, rl, true_stack, maybe_stack, false_stack, checked, mixed, gate_sm, start_time);
 383         if (free_checked)
 384                 free_slist(checked);
 385 }
 386 
 387 static void separate_pools(struct sm_state *sm, int comparison, struct range_list *rl,
 388                         struct state_list **true_stack,
 389                         struct state_list **false_stack,
 390                         struct state_list **checked, int *mixed)
 391 {
 392         struct state_list *maybe_stack = NULL;
 393         struct sm_state *tmp;
 394         struct timeval start_time;
 395 
 396 
 397         gettimeofday(&start_time, NULL);
 398         __separate_pools(sm, comparison, rl, true_stack, &maybe_stack, false_stack, checked, mixed, sm, &start_time);
 399 
 400         if (implied_debug) {
 401                 struct sm_state *sm;
 402 
 403                 FOR_EACH_PTR(*true_stack, sm) {
 404                         sm_msg("TRUE %s [stree %d]", show_sm(sm), get_stree_id(sm->pool));
 405                 } END_FOR_EACH_PTR(sm);
 406 
 407                 FOR_EACH_PTR(maybe_stack, sm) {
 408                         sm_msg("MAYBE %s %s[stree %d]",
 409                                show_sm(sm), sm->merged ? "(merged) ": "", get_stree_id(sm->pool));
 410                 } END_FOR_EACH_PTR(sm);
 411 
 412                 FOR_EACH_PTR(*false_stack, sm) {
 413                         sm_msg("FALSE %s [stree %d]", show_sm(sm), get_stree_id(sm->pool));
 414                 } END_FOR_EACH_PTR(sm);
 415         }
 416         /* if it's a maybe then remove it */
 417         FOR_EACH_PTR(maybe_stack, tmp) {
 418                 remove_pool(false_stack, tmp->pool);
 419                 remove_pool(true_stack, tmp->pool);
 420         } END_FOR_EACH_PTR(tmp);
 421 
 422         /* if it's both true and false remove it from both */
 423         FOR_EACH_PTR(*true_stack, tmp) {
 424                 if (remove_pool(false_stack, tmp->pool))
 425                         DELETE_CURRENT_PTR(tmp);
 426         } END_FOR_EACH_PTR(tmp);
 427 }
 428 
 429 static int sm_in_keep_leafs(struct sm_state *sm, const struct state_list *keep_gates)
 430 {
 431         struct sm_state *tmp, *old;
 432 
 433         FOR_EACH_PTR(keep_gates, tmp) {
 434                 if (is_merged(tmp))
 435                         continue;
 436                 old = get_sm_state_stree(tmp->pool, sm->owner, sm->name, sm->sym);
 437                 if (!old)
 438                         continue;
 439                 if (old == sm)
 440                         return 1;
 441         } END_FOR_EACH_PTR(tmp);
 442         return 0;
 443 }
 444 
 445 static int going_too_slow(void)
 446 {
 447         static void *printed;
 448 
 449         if (out_of_memory()) {
 450                 implications_off = true;
 451                 return 1;
 452         }
 453 
 454         if (!option_timeout || time_parsing_function() < option_timeout) {
 455                 implications_off = false;
 456                 return 0;
 457         }
 458 
 459         if (!__inline_fn && printed != cur_func_sym) {
 460                 if (!is_skipped_function())
 461                         sm_perror("turning off implications after %d seconds", option_timeout);
 462                 printed = cur_func_sym;
 463         }
 464         implications_off = true;
 465         return 1;
 466 }
 467 
 468 static char *sm_state_info(struct sm_state *sm)
 469 {
 470         static char buf[512];
 471         int n = 0;
 472 
 473         n += snprintf(buf + n, sizeof(buf) - n, "[stree %d line %d] ",
 474                       get_stree_id(sm->pool),  sm->line);
 475         if (n >= sizeof(buf))
 476                 return buf;
 477         n += snprintf(buf + n, sizeof(buf) - n, "%s ", show_sm(sm));
 478         if (n >= sizeof(buf))
 479                 return buf;
 480         n += snprintf(buf + n, sizeof(buf) - n, "left = %s [stree %d] ",
 481                       sm->left ? sm->left->state->name : "<none>",
 482                       sm->left ? get_stree_id(sm->left->pool) : -1);
 483         if (n >= sizeof(buf))
 484                 return buf;
 485         n += snprintf(buf + n, sizeof(buf) - n, "right = %s [stree %d]",
 486                       sm->right ? sm->right->state->name : "<none>",
 487                       sm->right ? get_stree_id(sm->right->pool) : -1);
 488         return buf;
 489 }
 490 
 491 /*
 492  * NOTE: If a state is in both the keep stack and the remove stack then that is
 493  * a bug.  Only add states which are definitely true or definitely false.  If
 494  * you have a leaf state that could be both true and false, then create a fake
 495  * split history where one side is true and one side is false.  Otherwise, if
 496  * you can't do that, then don't add it to either list.
 497  */
 498 #define RECURSE_LIMIT 300
 499 struct sm_state *filter_pools(struct sm_state *sm,
 500                               const struct state_list *remove_stack,
 501                               const struct state_list *keep_stack,
 502                               int *modified, int *recurse_cnt,
 503                               struct timeval *start, int *skip, int *bail)
 504 {
 505         struct sm_state *ret = NULL;
 506         struct sm_state *left;
 507         struct sm_state *right;
 508         int removed = 0;
 509         struct timeval now, diff;
 510 
 511         if (!sm)
 512                 return NULL;
 513         if (*bail)
 514                 return NULL;
 515         gettimeofday(&now, NULL);
 516         timersub(&now, start, &diff);
 517         if (diff.tv_sec >= 3) {
 518                 DIMPLIED("%s: implications taking too long: %s\n", __func__, sm_state_info(sm));
 519                 *bail = 1;
 520                 return NULL;
 521         }
 522         if ((*recurse_cnt)++ > RECURSE_LIMIT) {
 523                 DIMPLIED("%s: recursed too far:  %s\n", __func__, sm_state_info(sm));
 524                 *skip = 1;
 525                 return NULL;
 526         }
 527 
 528         if (pool_in_pools(sm->pool, remove_stack)) {
 529                 DIMPLIED("%s: remove: %s\n", __func__, sm_state_info(sm));
 530                 *modified = 1;
 531                 return NULL;
 532         }
 533 
 534         if (!is_merged(sm) || pool_in_pools(sm->pool, keep_stack) || sm_in_keep_leafs(sm, keep_stack)) {
 535                 DIMPLIED("%s: keep %s (%s, %s, %s): %s\n", __func__, sm->state->name,
 536                         is_merged(sm) ? "merged" : "not merged",
 537                         pool_in_pools(sm->pool, keep_stack) ? "not in keep pools" : "in keep pools",
 538                         sm_in_keep_leafs(sm, keep_stack) ? "reachable keep leaf" : "no keep leaf",
 539                         sm_state_info(sm));
 540                 return sm;
 541         }
 542 
 543         left = filter_pools(sm->left, remove_stack, keep_stack, &removed, recurse_cnt, start, skip, bail);
 544         right = filter_pools(sm->right, remove_stack, keep_stack, &removed, recurse_cnt, start, skip, bail);
 545         if (*bail || *skip)
 546                 return NULL;
 547         if (!removed) {
 548                 DIMPLIED("%s: kept all: %s\n", __func__, sm_state_info(sm));
 549                 return sm;
 550         }
 551         *modified = 1;
 552         if (!left && !right) {
 553                 DIMPLIED("%s: removed all: %s\n", __func__, sm_state_info(sm));
 554                 return NULL;
 555         }
 556 
 557         if (!left) {
 558                 ret = clone_sm(right);
 559                 ret->merged = 1;
 560                 ret->right = right;
 561                 ret->left = NULL;
 562         } else if (!right) {
 563                 ret = clone_sm(left);
 564                 ret->merged = 1;
 565                 ret->left = left;
 566                 ret->right = NULL;
 567         } else {
 568                 if (left->sym != sm->sym || strcmp(left->name, sm->name) != 0) {
 569                         left = clone_sm(left);
 570                         left->sym = sm->sym;
 571                         left->name = sm->name;
 572                 }
 573                 if (right->sym != sm->sym || strcmp(right->name, sm->name) != 0) {
 574                         right = clone_sm(right);
 575                         right->sym = sm->sym;
 576                         right->name = sm->name;
 577                 }
 578                 ret = merge_sm_states(left, right);
 579         }
 580 
 581         ret->pool = sm->pool;
 582 
 583         DIMPLIED("%s: partial: %s\n", __func__, sm_state_info(sm));
 584         return ret;
 585 }
 586 
 587 static struct stree *filter_stack(struct sm_state *gate_sm,
 588                                   struct stree *pre_stree,
 589                                   const struct state_list *remove_stack,
 590                                   const struct state_list *keep_stack)
 591 {
 592         struct stree *ret = NULL;
 593         struct sm_state *tmp;
 594         struct sm_state *filtered_sm;
 595         int modified;
 596         int recurse_cnt;
 597         struct timeval start;
 598         int skip;
 599         int bail = 0;
 600 
 601         if (!remove_stack)
 602                 return NULL;
 603 
 604         gettimeofday(&start, NULL);
 605         FOR_EACH_SM(pre_stree, tmp) {
 606                 if (!tmp->merged || sm_in_keep_leafs(tmp, keep_stack))
 607                         continue;
 608                 modified = 0;
 609                 recurse_cnt = 0;
 610                 skip = 0;
 611                 filtered_sm = filter_pools(tmp, remove_stack, keep_stack, &modified, &recurse_cnt, &start, &skip, &bail);
 612                 if (going_too_slow())
 613                         return NULL;
 614                 if (bail)
 615                         return ret;  /* Return the implications we figured out before time ran out. */
 616 
 617 
 618                 if (skip || !filtered_sm || !modified)
 619                         continue;
 620                 /* the assignments here are for borrowed implications */
 621                 filtered_sm->name = tmp->name;
 622                 filtered_sm->sym = tmp->sym;
 623                 avl_insert(&ret, filtered_sm);
 624         } END_FOR_EACH_SM(tmp);
 625         return ret;
 626 }
 627 
 628 static void separate_and_filter(struct sm_state *sm, int comparison, struct range_list *rl,
 629                 struct stree *pre_stree,
 630                 struct stree **true_states,
 631                 struct stree **false_states,
 632                 int *mixed)
 633 {
 634         struct state_list *true_stack = NULL;
 635         struct state_list *false_stack = NULL;
 636         struct timeval time_before;
 637         struct timeval time_after;
 638         int sec;
 639 
 640         gettimeofday(&time_before, NULL);
 641 
 642         DIMPLIED("checking implications: (%s (%s) %s %s)\n",
 643                  sm->name, sm->state->name, show_comparison(comparison), show_rl(rl));
 644 
 645         if (!is_merged(sm)) {
 646                 DIMPLIED("%d '%s' from line %d is not merged.\n", get_lineno(), sm->name, sm->line);
 647                 return;
 648         }
 649 
 650         separate_pools(sm, comparison, rl, &true_stack, &false_stack, NULL, mixed);
 651 
 652         DIMPLIED("filtering true stack.\n");
 653         *true_states = filter_stack(sm, pre_stree, false_stack, true_stack);
 654         DIMPLIED("filtering false stack.\n");
 655         *false_states = filter_stack(sm, pre_stree, true_stack, false_stack);
 656         free_slist(&true_stack);
 657         free_slist(&false_stack);
 658 
 659         gettimeofday(&time_after, NULL);
 660         sec = time_after.tv_sec - time_before.tv_sec;
 661         if (option_timeout && sec > option_timeout) {
 662                 sm_perror("Function too hairy.  Ignoring implications after %d seconds.", sec);
 663         }
 664 }
 665 
 666 static struct expression *get_last_expr(struct statement *stmt)
 667 {
 668         struct statement *last;
 669 
 670         last = last_ptr_list((struct ptr_list *)stmt->stmts);
 671         if (last->type == STMT_EXPRESSION)
 672                 return last->expression;
 673 
 674         if (last->type == STMT_LABEL) {
 675                 if (last->label_statement &&
 676                     last->label_statement->type == STMT_EXPRESSION)
 677                         return last->label_statement->expression;
 678         }
 679 
 680         return NULL;
 681 }
 682 
 683 static struct expression *get_left_most_expr(struct expression *expr)
 684 {
 685         struct statement *compound;
 686 
 687         compound = get_expression_statement(expr);
 688         if (compound)
 689                 return get_last_expr(compound);
 690 
 691         expr = strip_parens(expr);
 692         if (expr->type == EXPR_ASSIGNMENT)
 693                 return get_left_most_expr(expr->left);
 694         return expr;
 695 }
 696 
 697 static int is_merged_expr(struct expression  *expr)
 698 {
 699         struct sm_state *sm;
 700         sval_t dummy;
 701 
 702         if (get_value(expr, &dummy))
 703                 return 0;
 704         sm = get_sm_state_expr(SMATCH_EXTRA, expr);
 705         if (!sm)
 706                 return 0;
 707         if (is_merged(sm))
 708                 return 1;
 709         return 0;
 710 }
 711 
 712 static void delete_gate_sm_equiv(struct stree **stree, const char *name, struct symbol *sym)
 713 {
 714         struct smatch_state *state;
 715         struct relation *rel;
 716 
 717         state = get_state(SMATCH_EXTRA, name, sym);
 718         if (!state)
 719                 return;
 720         FOR_EACH_PTR(estate_related(state), rel) {
 721                 delete_state_stree(stree, SMATCH_EXTRA, rel->name, rel->sym);
 722         } END_FOR_EACH_PTR(rel);
 723 }
 724 
 725 static void delete_gate_sm(struct stree **stree, const char *name, struct symbol *sym)
 726 {
 727         delete_state_stree(stree, SMATCH_EXTRA, name, sym);
 728 }
 729 
 730 static int handle_comparison(struct expression *expr,
 731                               struct stree **implied_true,
 732                               struct stree **implied_false)
 733 {
 734         struct sm_state *sm = NULL;
 735         struct range_list *rl = NULL;
 736         struct expression *left;
 737         struct expression *right;
 738         struct symbol *type;
 739         int comparison = expr->op;
 740         int mixed = 0;
 741 
 742         left = get_left_most_expr(expr->left);
 743         right = get_left_most_expr(expr->right);
 744 
 745         if (is_merged_expr(left)) {
 746                 sm = get_sm_state_expr(SMATCH_EXTRA, left);
 747                 get_implied_rl(right, &rl);
 748         } else if (is_merged_expr(right)) {
 749                 sm = get_sm_state_expr(SMATCH_EXTRA, right);
 750                 get_implied_rl(left, &rl);
 751                 comparison = flip_comparison(comparison);
 752         }
 753 
 754         if (!rl || !sm)
 755                 return 0;
 756 
 757         type = get_type(expr);
 758         if (!type)
 759                 return 0;
 760         if (type_positive_bits(rl_type(rl)) > type_positive_bits(type))
 761                 type = rl_type(rl);
 762         if (type_positive_bits(type) < 31)
 763                 type = &int_ctype;
 764         rl = cast_rl(type, rl);
 765 
 766         separate_and_filter(sm, comparison, rl, __get_cur_stree(), implied_true, implied_false, &mixed);
 767 
 768         delete_gate_sm_equiv(implied_true, sm->name, sm->sym);
 769         delete_gate_sm_equiv(implied_false, sm->name, sm->sym);
 770         if (mixed) {
 771                 delete_gate_sm(implied_true, sm->name, sm->sym);
 772                 delete_gate_sm(implied_false, sm->name, sm->sym);
 773         }
 774 
 775         return 1;
 776 }
 777 
 778 static int handle_zero_comparison(struct expression *expr,
 779                                 struct stree **implied_true,
 780                                 struct stree **implied_false)
 781 {
 782         struct symbol *sym;
 783         char *name;
 784         struct sm_state *sm;
 785         int mixed = 0;
 786         int ret = 0;
 787 
 788         if (expr->type == EXPR_POSTOP)
 789                 expr = strip_expr(expr->unop);
 790 
 791         if (expr->type == EXPR_ASSIGNMENT) {
 792                 /* most of the time ->pools will be empty here because we
 793                    just set the state, but if have assigned a conditional
 794                    function there are implications. */
 795                 expr = expr->left;
 796         }
 797 
 798         name = expr_to_var_sym(expr, &sym);
 799         if (!name || !sym)
 800                 goto free;
 801         sm = get_sm_state(SMATCH_EXTRA, name, sym);
 802         if (!sm || !sm->merged)
 803                 goto free;
 804 
 805         separate_and_filter(sm, SPECIAL_NOTEQUAL, tmp_range_list(estate_type(sm->state), 0), __get_cur_stree(), implied_true, implied_false, &mixed);
 806         delete_gate_sm_equiv(implied_true, sm->name, sm->sym);
 807         delete_gate_sm_equiv(implied_false, sm->name, sm->sym);
 808         if (mixed) {
 809                 delete_gate_sm(implied_true, sm->name, sm->sym);
 810                 delete_gate_sm(implied_false, sm->name, sm->sym);
 811         }
 812 
 813         ret = 1;
 814 free:
 815         free_string(name);
 816         return ret;
 817 }
 818 
 819 static int handled_by_comparison_hook(struct expression *expr,
 820                                       struct stree **implied_true,
 821                                       struct stree **implied_false)
 822 {
 823         struct sm_state *sm, *true_sm, *false_sm;
 824         struct state_list *true_stack = NULL;
 825         struct state_list *false_stack = NULL;
 826         struct stree *pre_stree;
 827 
 828         sm = comparison_implication_hook(expr, &true_stack, &false_stack);
 829         if (!sm)
 830                 return 0;
 831 
 832         pre_stree = clone_stree(__get_cur_stree());
 833 
 834         *implied_true = filter_stack(sm, pre_stree, false_stack, true_stack);
 835         *implied_false = filter_stack(sm, pre_stree, true_stack, false_stack);
 836 
 837         true_sm = get_sm_state_stree(*implied_true, sm->owner, sm->name, sm->sym);
 838         false_sm = get_sm_state_stree(*implied_false, sm->owner, sm->name, sm->sym);
 839         if (true_sm && strcmp(true_sm->state->name, "unknown") == 0)
 840                 delete_state_stree(implied_true, sm->owner, sm->name, sm->sym);
 841         if (false_sm && strcmp(false_sm->state->name, "unknown") == 0)
 842                 delete_state_stree(implied_false, sm->owner, sm->name, sm->sym);
 843 
 844         free_stree(&pre_stree);
 845         free_slist(&true_stack);
 846         free_slist(&false_stack);
 847 
 848         return 1;
 849 }
 850 
 851 static int handled_by_extra_states(struct expression *expr,
 852                                    struct stree **implied_true,
 853                                    struct stree **implied_false)
 854 {
 855         sval_t sval;
 856 
 857         /* If the expression is known then it has no implications.  */
 858         if (get_implied_value(expr, &sval))
 859                 return true;
 860 
 861         if (expr->type == EXPR_COMPARE)
 862                 return handle_comparison(expr, implied_true, implied_false);
 863         else
 864                 return handle_zero_comparison(expr, implied_true, implied_false);
 865 }
 866 
 867 static int handled_by_parsed_conditions(struct expression *expr,
 868                                         struct stree **implied_true,
 869                                         struct stree **implied_false)
 870 {
 871         struct state_list *true_stack = NULL;
 872         struct state_list *false_stack = NULL;
 873         struct stree *pre_stree;
 874         struct sm_state *sm;
 875 
 876         sm = parsed_condition_implication_hook(expr, &true_stack, &false_stack);
 877         if (!sm)
 878                 return 0;
 879 
 880         pre_stree = clone_stree(__get_cur_stree());
 881 
 882         *implied_true = filter_stack(sm, pre_stree, false_stack, true_stack);
 883         *implied_false = filter_stack(sm, pre_stree, true_stack, false_stack);
 884 
 885         free_stree(&pre_stree);
 886         free_slist(&true_stack);
 887         free_slist(&false_stack);
 888 
 889         return 1;
 890 }
 891 
 892 static int handled_by_stored_conditions(struct expression *expr,
 893                                         struct stree **implied_true,
 894                                         struct stree **implied_false)
 895 {
 896         struct state_list *true_stack = NULL;
 897         struct state_list *false_stack = NULL;
 898         struct stree *pre_stree;
 899         struct sm_state *sm;
 900 
 901         sm = stored_condition_implication_hook(expr, &true_stack, &false_stack);
 902         if (!sm)
 903                 return 0;
 904 
 905         pre_stree = clone_stree(__get_cur_stree());
 906 
 907         *implied_true = filter_stack(sm, pre_stree, false_stack, true_stack);
 908         *implied_false = filter_stack(sm, pre_stree, true_stack, false_stack);
 909 
 910         free_stree(&pre_stree);
 911         free_slist(&true_stack);
 912         free_slist(&false_stack);
 913 
 914         return 1;
 915 }
 916 
 917 static struct stree *saved_implied_true;
 918 static struct stree *saved_implied_false;
 919 static struct stree *extra_saved_implied_true;
 920 static struct stree *extra_saved_implied_false;
 921 
 922 static void separate_implication_states(struct stree **implied_true,
 923                                          struct stree **implied_false,
 924                                          int owner)
 925 {
 926         struct sm_state *sm;
 927 
 928         /* We process these states later to preserve the implications. */
 929         FOR_EACH_SM(*implied_true, sm) {
 930                 if (sm->owner == owner)
 931                         overwrite_sm_state_stree(&extra_saved_implied_true, sm);
 932         } END_FOR_EACH_SM(sm);
 933         FOR_EACH_SM(extra_saved_implied_true, sm) {
 934                 delete_state_stree(implied_true, sm->owner, sm->name, sm->sym);
 935         } END_FOR_EACH_SM(sm);
 936 
 937         FOR_EACH_SM(*implied_false, sm) {
 938                 if (sm->owner == owner)
 939                         overwrite_sm_state_stree(&extra_saved_implied_false, sm);
 940         } END_FOR_EACH_SM(sm);
 941         FOR_EACH_SM(extra_saved_implied_false, sm) {
 942                 delete_state_stree(implied_false, sm->owner, sm->name, sm->sym);
 943         } END_FOR_EACH_SM(sm);
 944 }
 945 
 946 static void get_tf_states(struct expression *expr,
 947                           struct stree **implied_true,
 948                           struct stree **implied_false)
 949 {
 950         if (handled_by_parsed_conditions(expr, implied_true, implied_false))
 951                 return;
 952 
 953         if (handled_by_comparison_hook(expr, implied_true, implied_false)) {
 954                 separate_implication_states(implied_true, implied_false, comparison_id);
 955                 return;
 956         }
 957 
 958         if (handled_by_extra_states(expr, implied_true, implied_false)) {
 959                 separate_implication_states(implied_true, implied_false, SMATCH_EXTRA);
 960                 return;
 961         }
 962 
 963         if (handled_by_stored_conditions(expr, implied_true, implied_false))
 964                 return;
 965 }
 966 
 967 static void save_implications_hook(struct expression *expr)
 968 {
 969         if (going_too_slow())
 970                 return;
 971         get_tf_states(expr, &saved_implied_true, &saved_implied_false);
 972 }
 973 
 974 static void set_implied_states(struct expression *expr)
 975 {
 976         struct sm_state *sm;
 977 
 978         if (implied_debug &&
 979             (expr || saved_implied_true || saved_implied_false)) {
 980                 char *name;
 981 
 982                 name = expr_to_str(expr);
 983                 printf("These are the implied states for the true path: (%s)\n", name);
 984                 __print_stree(saved_implied_true);
 985                 printf("These are the implied states for the false path: (%s)\n", name);
 986                 __print_stree(saved_implied_false);
 987                 free_string(name);
 988         }
 989 
 990         FOR_EACH_SM(saved_implied_true, sm) {
 991                 __set_true_false_sm(sm, NULL);
 992         } END_FOR_EACH_SM(sm);
 993         free_stree(&saved_implied_true);
 994 
 995         FOR_EACH_SM(saved_implied_false, sm) {
 996                 __set_true_false_sm(NULL, sm);
 997         } END_FOR_EACH_SM(sm);
 998         free_stree(&saved_implied_false);
 999 }
1000 
1001 static void set_extra_implied_states(struct expression *expr)
1002 {
1003         saved_implied_true = extra_saved_implied_true;
1004         saved_implied_false = extra_saved_implied_false;
1005         extra_saved_implied_true = NULL;
1006         extra_saved_implied_false = NULL;
1007         set_implied_states(NULL);
1008 }
1009 
1010 void param_limit_implications(struct expression *expr, int param, char *key, char *value, struct stree **implied)
1011 {
1012         struct expression *orig_expr, *arg;
1013         struct symbol *compare_type;
1014         char *name;
1015         struct symbol *sym;
1016         struct sm_state *sm;
1017         struct sm_state *tmp;
1018         struct stree *implied_true = NULL;
1019         struct stree *implied_false = NULL;
1020         struct range_list *orig, *limit;
1021         char *left_name = NULL;
1022         struct symbol *left_sym = NULL;
1023         int mixed = 0;
1024 
1025         if (time_parsing_function() > 40)
1026                 return;
1027 
1028         orig_expr = expr;
1029         while (expr->type == EXPR_ASSIGNMENT)
1030                 expr = strip_expr(expr->right);
1031         if (expr->type != EXPR_CALL)
1032                 return;
1033 
1034         arg = get_argument_from_call_expr(expr->args, param);
1035         if (!arg)
1036                 return;
1037 
1038         arg = strip_parens(arg);
1039         while (arg->type == EXPR_ASSIGNMENT && arg->op == '=')
1040                 arg = strip_parens(arg->left);
1041 
1042         name = get_variable_from_key(arg, key, &sym);
1043         if (!name || !sym)
1044                 goto free;
1045 
1046         sm = get_sm_state(SMATCH_EXTRA, name, sym);
1047         if (!sm || !sm->merged)
1048                 goto free;
1049 
1050         if (strcmp(key, "$") == 0)
1051                 compare_type = get_arg_type(expr->fn, param);
1052         else
1053                 compare_type = get_member_type_from_key(arg, key);
1054 
1055         orig = estate_rl(sm->state);
1056         orig = cast_rl(compare_type, orig);
1057 
1058         call_results_to_rl(expr, compare_type, value, &limit);
1059 
1060         separate_and_filter(sm, PARAM_LIMIT, limit, __get_cur_stree(), &implied_true, &implied_false, &mixed);
1061 
1062         if (orig_expr->type == EXPR_ASSIGNMENT)
1063                 left_name = expr_to_var_sym(orig_expr->left, &left_sym);
1064 
1065         FOR_EACH_SM(implied_true, tmp) {
1066                 /*
1067                  * What we're trying to do here is preserve the sm state so that
1068                  * smatch extra doesn't create a new sm state when it parses the
1069                  * PARAM_LIMIT.
1070                  */
1071                 if (!mixed && tmp->sym == sym &&
1072                     strcmp(tmp->name, name) == 0 &&
1073                     (!left_name || strcmp(left_name, name) != 0)) {
1074                         overwrite_sm_state_stree(implied, tmp);
1075                         continue;
1076                 }
1077 
1078                 // TODO why can't this just be __set_sm()?
1079                 __set_sm_fake_stree(tmp);
1080         } END_FOR_EACH_SM(tmp);
1081 
1082         free_stree(&implied_true);
1083         free_stree(&implied_false);
1084 free:
1085         free_string(name);
1086 }
1087 
1088 struct stree *__implied_case_stree(struct expression *switch_expr,
1089                                    struct range_list *rl,
1090                                    struct range_list_stack **remaining_cases,
1091                                    struct stree **raw_stree)
1092 {
1093         char *name;
1094         struct symbol *sym;
1095         struct var_sym_list *vsl;
1096         struct sm_state *sm;
1097         struct stree *true_states = NULL;
1098         struct stree *false_states = NULL;
1099         struct stree *extra_states;
1100         struct stree *ret = clone_stree(*raw_stree);
1101 
1102         name = expr_to_chunk_sym_vsl(switch_expr, &sym, &vsl);
1103 
1104         if (rl)
1105                 filter_top_rl(remaining_cases, rl);
1106         else
1107                 rl = clone_rl(top_rl(*remaining_cases));
1108 
1109         if (name) {
1110                 sm = get_sm_state_stree(*raw_stree, SMATCH_EXTRA, name, sym);
1111                 if (sm)
1112                         separate_and_filter(sm, SPECIAL_EQUAL, rl, *raw_stree, &true_states, &false_states, NULL);
1113         }
1114 
1115         __push_fake_cur_stree();
1116         __unnullify_path();
1117         if (name)
1118                 set_extra_nomod_vsl(name, sym, vsl, NULL, alloc_estate_rl(rl));
1119         __pass_case_to_client(switch_expr, rl);
1120         extra_states = __pop_fake_cur_stree();
1121         overwrite_stree(extra_states, &true_states);
1122         overwrite_stree(true_states, &ret);
1123         free_stree(&extra_states);
1124         free_stree(&true_states);
1125         free_stree(&false_states);
1126 
1127         free_string(name);
1128         return ret;
1129 }
1130 
1131 static void match_end_func(struct symbol *sym)
1132 {
1133         if (__inline_fn)
1134                 return;
1135         implied_debug_msg = NULL;
1136 }
1137 
1138 static void get_tf_stacks_from_pool(struct sm_state *gate_sm,
1139                                     struct sm_state *pool_sm,
1140                                     struct state_list **true_stack,
1141                                     struct state_list **false_stack)
1142 {
1143         struct sm_state *tmp;
1144         int possibly_true = 0;
1145 
1146         if (!gate_sm)
1147                 return;
1148 
1149         if (strcmp(gate_sm->state->name, pool_sm->state->name) == 0) {
1150                 add_ptr_list(true_stack, pool_sm);
1151                 return;
1152         }
1153 
1154         FOR_EACH_PTR(gate_sm->possible, tmp) {
1155                 if (strcmp(tmp->state->name, pool_sm->state->name) == 0) {
1156                         possibly_true = 1;
1157                         break;
1158                 }
1159         } END_FOR_EACH_PTR(tmp);
1160 
1161         if (!possibly_true) {
1162                 add_ptr_list(false_stack, gate_sm);
1163                 return;
1164         }
1165 
1166         get_tf_stacks_from_pool(gate_sm->left, pool_sm, true_stack, false_stack);
1167         get_tf_stacks_from_pool(gate_sm->right, pool_sm, true_stack, false_stack);
1168 }
1169 
1170 /*
1171  * The situation is we have a SMATCH_EXTRA state and we want to break it into
1172  * each of the ->possible states and find the implications of each.  The caller
1173  * has to use __push_fake_cur_stree() to preserve the correct states so they
1174  * can be restored later.
1175  */
1176 void overwrite_states_using_pool(struct sm_state *gate_sm, struct sm_state *pool_sm)
1177 {
1178         struct state_list *true_stack = NULL;
1179         struct state_list *false_stack = NULL;
1180         struct stree *pre_stree;
1181         struct stree *implied_true;
1182         struct sm_state *tmp;
1183 
1184         if (!pool_sm->pool)
1185                 return;
1186 
1187         get_tf_stacks_from_pool(gate_sm, pool_sm, &true_stack, &false_stack);
1188 
1189         pre_stree = clone_stree(__get_cur_stree());
1190 
1191         implied_true = filter_stack(gate_sm, pre_stree, false_stack, true_stack);
1192 
1193         free_stree(&pre_stree);
1194         free_slist(&true_stack);
1195         free_slist(&false_stack);
1196 
1197         FOR_EACH_SM(implied_true, tmp) {
1198                 set_state(tmp->owner, tmp->name, tmp->sym, tmp->state);
1199         } END_FOR_EACH_SM(tmp);
1200 
1201         free_stree(&implied_true);
1202 }
1203 
1204 int assume(struct expression *expr)
1205 {
1206         int orig_final_pass = final_pass;
1207 
1208         in_fake_env++;
1209         final_pass = 0;
1210         __push_fake_cur_stree();
1211         __split_whole_condition(expr);
1212         final_pass = orig_final_pass;
1213         in_fake_env--;
1214 
1215         return 1;
1216 }
1217 
1218 void end_assume(void)
1219 {
1220         __discard_false_states();
1221         __free_fake_cur_stree();
1222 }
1223 
1224 int impossible_assumption(struct expression *left, int op, sval_t sval)
1225 {
1226         struct expression *value;
1227         struct expression *comparison;
1228         int ret;
1229 
1230         value = value_expr(sval.value);
1231         comparison = compare_expression(left, op, value);
1232 
1233         if (!assume(comparison))
1234                 return 0;
1235         ret = is_impossible_path();
1236         end_assume();
1237 
1238         return ret;
1239 }
1240 
1241 void __extra_match_condition(struct expression *expr);
1242 void __comparison_match_condition(struct expression *expr);
1243 void __stored_condition(struct expression *expr);
1244 void register_implications(int id)
1245 {
1246         add_hook(&save_implications_hook, CONDITION_HOOK);
1247         add_hook(&set_implied_states, CONDITION_HOOK);
1248         add_hook(&__extra_match_condition, CONDITION_HOOK);
1249         add_hook(&__comparison_match_condition, CONDITION_HOOK);
1250         add_hook(&set_extra_implied_states, CONDITION_HOOK);
1251         add_hook(&__stored_condition, CONDITION_HOOK);
1252         add_hook(&match_end_func, END_FUNC_HOOK);
1253 }