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