struct_assignment: add copy_from_user()
[smatch.git] / smatch_implied.c
blobe67491b2110e40c193a38ab646ba8f78e2e1ef12
1 /*
2 * Copyright (C) 2008 Dan Carpenter.
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.
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.
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
19 * Imagine we have this code:
20 * foo = 1;
21 * if (bar)
22 * foo = 99;
23 * else
24 * frob();
25 * // <-- point #1
26 * if (foo == 99) // <-- point #2
27 * bar->baz; // <-- point #3
30 * At point #3 bar is non null and can be dereferenced.
32 * It's smatch_implied.c which sets bar to non null at point #2.
34 * At point #1 merge_slist() stores the list of states from both
35 * the true and false paths. On the true path foo == 99 and on
36 * the false path foo == 1. merge_slist() sets their pool
37 * list to show the other states which were there when foo == 99.
39 * When it comes to the if (foo == 99) the smatch implied hook
40 * looks for all the pools where foo was not 99. It makes a list
41 * of those.
43 * Then for bar (and all the other states) it says, ok bar is a
44 * merged state that came from these previous states. We'll
45 * chop out all the states where it came from a pool where
46 * foo != 99 and merge it all back together.
48 * That is the implied state of bar.
50 * merge_slist() sets up ->pool. An sm_state only has one ->pool and
51 * that is the pool where it was first set. The my pool gets set when
52 * code paths merge. States that have been set since the last merge do
53 * not have a ->pool.
54 * merge_sm_state() sets ->left and ->right. (These are the states which were
55 * merged to form the current state.)
56 * a pool: a pool is an slist that has been merged with another slist.
59 #include <time.h>
60 #include "smatch.h"
61 #include "smatch_slist.h"
62 #include "smatch_extra.h"
64 char *implied_debug_msg;
66 bool implications_off;
68 bool implied_debug;
70 #define full_debug 0
71 #define DIMPLIED(msg...) do { if (full_debug) printf(msg); } while (0)
73 bool debug_implied(void)
75 return option_debug || implied_debug || full_debug;
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.
83 static struct range_list *tmp_range_list(struct symbol *type, long long num)
85 static struct range_list *my_list = NULL;
86 static struct data_range *my_range;
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;
94 static const char *show_comparison(int op)
96 if (op == PARAM_LIMIT)
97 return "<lim>";
98 return show_special(op);
101 static void print_debug_tf(struct sm_state *sm, int istrue, int isfalse)
103 if (!full_debug && !option_debug)
104 return;
106 if (istrue && isfalse) {
107 printf("%s: %d: does not exist.\n", show_sm(sm), sm->line);
108 } else if (istrue) {
109 printf("'%s = %s' from %d is true. %s[stree %d]\n", sm->name, show_state(sm->state),
110 sm->line, sm->merged ? "[merged]" : "[leaf]",
111 get_stree_id(sm->pool));
112 } else if (isfalse) {
113 printf("'%s = %s' from %d is false. %s[stree %d]\n", sm->name, show_state(sm->state),
114 sm->line,
115 sm->merged ? "[merged]" : "[leaf]",
116 get_stree_id(sm->pool));
117 } else {
118 printf("'%s = %s' from %d could be true or false. %s[stree %d]\n", sm->name,
119 show_state(sm->state), sm->line,
120 sm->merged ? "[merged]" : "[leaf]",
121 get_stree_id(sm->pool));
125 void split_comparison_helper(struct range_list *left_orig, int op, struct range_list *right_orig,
126 struct range_list **left_true_rl, struct range_list **left_false_rl)
128 if (op == PARAM_LIMIT) {
129 *left_true_rl = rl_intersection(left_orig, right_orig);
130 *left_false_rl = rl_filter(left_orig, right_orig);
131 return;
134 split_comparison_rl(left_orig, op, right_orig, left_true_rl, left_false_rl, NULL, NULL);
137 static int create_fake_history(struct sm_state *sm, int comparison, struct range_list *rl)
139 struct range_list *orig_rl;
140 struct range_list *true_rl, *false_rl;
141 struct stree *true_stree, *false_stree;
142 struct sm_state *true_sm, *false_sm;
143 sval_t sval;
145 if (is_merged(sm) || sm->left || sm->right)
146 return 0;
147 if (comparison != PARAM_LIMIT && !rl_to_sval(rl, &sval))
148 return 0;
149 if (!estate_rl(sm->state))
150 return 0;
152 orig_rl = cast_rl(rl_type(rl), estate_rl(sm->state));
153 split_comparison_helper(orig_rl, comparison, rl, &true_rl, &false_rl);
155 true_rl = rl_truncate_cast(estate_type(sm->state), true_rl);
156 false_rl = rl_truncate_cast(estate_type(sm->state), false_rl);
157 if (is_whole_rl(true_rl) || is_whole_rl(false_rl) ||
158 !true_rl || !false_rl ||
159 rl_equiv(orig_rl, true_rl) || rl_equiv(orig_rl, false_rl) ||
160 rl_equiv(estate_rl(sm->state), true_rl) || rl_equiv(estate_rl(sm->state), false_rl))
161 return 0;
163 if (rl_intersection(true_rl, false_rl)) {
165 * Normally these won't intersect, but one exception is when
166 * we're dealing with mtags. We have a long list of mtags and
167 * then negate the list. Now it's over the limit for mtag list
168 * length and we squash it down to 4096-ptr_max. So then it's
169 * possible for the true and false rl to overlap.
171 return 0;
174 if (full_debug)
175 sm_msg("fake_history: %s vs %s. %s %s %s. --> T: %s F: %s",
176 sm->name, show_rl(rl), sm->state->name, show_comparison(comparison), show_rl(rl),
177 show_rl(true_rl), show_rl(false_rl));
179 true_sm = clone_sm(sm);
180 false_sm = clone_sm(sm);
182 true_sm->state = clone_partial_estate(sm->state, true_rl);
183 free_slist(&true_sm->possible);
184 add_possible_sm(true_sm, true_sm);
185 false_sm->state = clone_partial_estate(sm->state, false_rl);
186 free_slist(&false_sm->possible);
187 add_possible_sm(false_sm, false_sm);
189 true_stree = clone_stree(sm->pool);
190 false_stree = clone_stree(sm->pool);
192 overwrite_sm_state_stree(&true_stree, true_sm);
193 overwrite_sm_state_stree(&false_stree, false_sm);
195 true_sm->pool = true_stree;
196 false_sm->pool = false_stree;
198 sm->leaf = 1;
199 sm->merged = 1;
200 sm->left = true_sm;
201 sm->right = false_sm;
203 return 1;
207 * add_pool() adds a slist to *pools. If the slist has already been
208 * added earlier then it doesn't get added a second time.
210 void add_pool(struct state_list **pools, struct sm_state *new)
212 struct sm_state *tmp;
214 FOR_EACH_PTR(*pools, tmp) {
215 if (tmp->pool < new->pool)
216 continue;
217 else if (tmp->pool == new->pool) {
218 return;
219 } else {
220 INSERT_CURRENT(new, tmp);
221 return;
223 } END_FOR_EACH_PTR(tmp);
224 add_ptr_list(pools, new);
227 static int pool_in_pools(struct stree *pool,
228 const struct state_list *slist)
230 struct sm_state *tmp;
232 FOR_EACH_PTR(slist, tmp) {
233 if (!tmp->pool)
234 continue;
235 if (tmp->pool == pool)
236 return 1;
237 } END_FOR_EACH_PTR(tmp);
238 return 0;
241 static int remove_pool(struct state_list **pools, struct stree *remove)
243 struct sm_state *tmp;
244 int ret = 0;
246 FOR_EACH_PTR(*pools, tmp) {
247 if (tmp->pool == remove) {
248 DELETE_CURRENT_PTR(tmp);
249 ret = 1;
251 } END_FOR_EACH_PTR(tmp);
253 return ret;
256 static bool possibly_true_helper(struct range_list *var_rl, int comparison, struct range_list *rl)
258 if (comparison == PARAM_LIMIT) {
259 struct range_list *intersect;
261 intersect = rl_intersection(var_rl, rl);
262 if (intersect)
263 return true;
264 return false;
266 return possibly_true_rl(var_rl, comparison, rl);
269 static bool possibly_false_helper(struct range_list *var_rl, int comparison, struct range_list *rl)
271 if (comparison == PARAM_LIMIT) {
272 struct range_list *intersect;
274 intersect = rl_intersection(var_rl, rl);
275 /* if it's not equiv then it's possibly false */
276 return !rl_equiv(var_rl, intersect);
278 return possibly_false_rl(var_rl, comparison, rl);
282 * If 'foo' == 99 add it that pool to the true pools. If it's false, add it to
283 * the false pools. If we're not sure, then we don't add it to either.
285 static void do_compare(struct sm_state *sm, int comparison, struct range_list *rl,
286 struct state_list **true_stack,
287 struct state_list **maybe_stack,
288 struct state_list **false_stack,
289 int *mixed, struct sm_state *gate_sm)
291 int istrue;
292 int isfalse;
293 struct range_list *var_rl;
295 if (!sm->pool)
296 return;
298 var_rl = cast_rl(rl_type(rl), estate_rl(sm->state));
300 istrue = !possibly_false_helper(var_rl, comparison, rl);
301 isfalse = !possibly_true_helper(var_rl, comparison, rl);
303 print_debug_tf(sm, istrue, isfalse);
305 /* give up if we have borrowed implications (smatch_equiv.c) */
306 if (sm->sym != gate_sm->sym ||
307 strcmp(sm->name, gate_sm->name) != 0) {
308 if (mixed)
309 *mixed = 1;
312 if (mixed && !*mixed && !is_merged(sm) && !istrue && !isfalse) {
313 if (!create_fake_history(sm, comparison, rl))
314 *mixed = 1;
317 if (istrue)
318 add_pool(true_stack, sm);
319 else if (isfalse)
320 add_pool(false_stack, sm);
321 else
322 add_pool(maybe_stack, sm);
325 static int is_checked(struct state_list *checked, struct sm_state *sm)
327 struct sm_state *tmp;
329 FOR_EACH_PTR(checked, tmp) {
330 if (tmp == sm)
331 return 1;
332 } END_FOR_EACH_PTR(tmp);
333 return 0;
337 * separate_pools():
338 * Example code: if (foo == 99) {
340 * Say 'foo' is a merged state that has many possible values. It is the combination
341 * of merges. separate_pools() iterates through the pools recursively and calls
342 * do_compare() for each time 'foo' was set.
344 static void __separate_pools(struct sm_state *sm, int comparison, struct range_list *rl,
345 struct state_list **true_stack,
346 struct state_list **maybe_stack,
347 struct state_list **false_stack,
348 struct state_list **checked, int *mixed, struct sm_state *gate_sm,
349 struct timeval *start_time)
351 int free_checked = 0;
352 struct state_list *checked_states = NULL;
353 struct timeval now, diff;
355 if (!sm)
356 return;
358 gettimeofday(&now, NULL);
359 timersub(&now, start_time, &diff);
360 if (diff.tv_sec >= 1) {
361 if (full_debug) {
362 sm_msg("debug: %s: implications taking too long. (%s %s %s)",
363 __func__, sm->state->name, show_comparison(comparison), show_rl(rl));
365 if (mixed)
366 *mixed = 1;
369 if (checked == NULL) {
370 checked = &checked_states;
371 free_checked = 1;
373 if (is_checked(*checked, sm))
374 return;
375 add_ptr_list(checked, sm);
377 do_compare(sm, comparison, rl, true_stack, maybe_stack, false_stack, mixed, gate_sm);
379 __separate_pools(sm->left, comparison, rl, true_stack, maybe_stack, false_stack, checked, mixed, gate_sm, start_time);
380 __separate_pools(sm->right, comparison, rl, true_stack, maybe_stack, false_stack, checked, mixed, gate_sm, start_time);
381 if (free_checked)
382 free_slist(checked);
385 static void separate_pools(struct sm_state *sm, int comparison, struct range_list *rl,
386 struct state_list **true_stack,
387 struct state_list **false_stack,
388 struct state_list **checked, int *mixed)
390 struct state_list *maybe_stack = NULL;
391 struct sm_state *tmp;
392 struct timeval start_time;
395 gettimeofday(&start_time, NULL);
396 __separate_pools(sm, comparison, rl, true_stack, &maybe_stack, false_stack, checked, mixed, sm, &start_time);
398 if (full_debug) {
399 struct sm_state *sm;
401 FOR_EACH_PTR(*true_stack, sm) {
402 sm_msg("TRUE %s [stree %d %p]", show_sm(sm), get_stree_id(sm->pool), sm->pool);
403 } END_FOR_EACH_PTR(sm);
405 FOR_EACH_PTR(maybe_stack, sm) {
406 sm_msg("MAYBE %s %s[stree %d %p]",
407 show_sm(sm), sm->merged ? "(merged) ": "", get_stree_id(sm->pool), sm->pool);
408 } END_FOR_EACH_PTR(sm);
410 FOR_EACH_PTR(*false_stack, sm) {
411 sm_msg("FALSE %s [stree %d %p]", show_sm(sm), get_stree_id(sm->pool), sm->pool);
412 } END_FOR_EACH_PTR(sm);
414 /* if it's a maybe then remove it */
415 FOR_EACH_PTR(maybe_stack, tmp) {
416 remove_pool(false_stack, tmp->pool);
417 remove_pool(true_stack, tmp->pool);
418 } END_FOR_EACH_PTR(tmp);
420 /* if it's both true and false remove it from both */
421 FOR_EACH_PTR(*true_stack, tmp) {
422 if (remove_pool(false_stack, tmp->pool))
423 DELETE_CURRENT_PTR(tmp);
424 } END_FOR_EACH_PTR(tmp);
427 static int sm_in_keep_leafs(struct sm_state *sm, const struct state_list *keep_gates)
429 struct sm_state *tmp, *old;
431 FOR_EACH_PTR(keep_gates, tmp) {
432 if (is_merged(tmp))
433 continue;
434 old = get_sm_state_stree(tmp->pool, sm->owner, sm->name, sm->sym);
435 if (!old)
436 continue;
437 if (old == sm)
438 return 1;
439 } END_FOR_EACH_PTR(tmp);
440 return 0;
443 static int going_too_slow(void)
445 static void *printed;
447 if (out_of_memory()) {
448 implications_off = true;
449 return 1;
452 if (time_parsing_function() < 60) {
453 implications_off = false;
454 return 0;
457 if (!__inline_fn && printed != cur_func_sym) {
458 sm_perror("turning off implications after 60 seconds");
459 printed = cur_func_sym;
461 implications_off = true;
462 return 1;
465 static char *sm_state_info(struct sm_state *sm)
467 static char buf[512];
468 int n = 0;
470 n += snprintf(buf + n, sizeof(buf) - n, "[stree %d line %d] ",
471 get_stree_id(sm->pool), sm->line);
472 if (n >= sizeof(buf))
473 return buf;
474 n += snprintf(buf + n, sizeof(buf) - n, "%s ", show_sm(sm));
475 if (n >= sizeof(buf))
476 return buf;
477 n += snprintf(buf + n, sizeof(buf) - n, "left = %s [stree %d] ",
478 sm->left ? sm->left->state->name : "<none>",
479 sm->left ? get_stree_id(sm->left->pool) : -1);
480 if (n >= sizeof(buf))
481 return buf;
482 n += snprintf(buf + n, sizeof(buf) - n, "right = %s [stree %d]",
483 sm->right ? sm->right->state->name : "<none>",
484 sm->right ? get_stree_id(sm->right->pool) : -1);
485 return buf;
489 * NOTE: If a state is in both the keep stack and the remove stack then that is
490 * a bug. Only add states which are definitely true or definitely false. If
491 * you have a leaf state that could be both true and false, then create a fake
492 * split history where one side is true and one side is false. Otherwise, if
493 * you can't do that, then don't add it to either list.
495 #define RECURSE_LIMIT 300
496 struct sm_state *filter_pools(struct sm_state *sm,
497 const struct state_list *remove_stack,
498 const struct state_list *keep_stack,
499 int *modified, int *recurse_cnt,
500 struct timeval *start, int *skip, int *bail)
502 struct sm_state *ret = NULL;
503 struct sm_state *left;
504 struct sm_state *right;
505 int removed = 0;
506 struct timeval now, diff;
508 if (!sm)
509 return NULL;
510 if (*bail)
511 return NULL;
512 gettimeofday(&now, NULL);
513 timersub(&now, start, &diff);
514 if (diff.tv_sec >= 3) {
515 DIMPLIED("%s: implications taking too long: %s\n", __func__, sm_state_info(sm));
516 *bail = 1;
517 return NULL;
519 if ((*recurse_cnt)++ > RECURSE_LIMIT) {
520 DIMPLIED("%s: recursed too far: %s\n", __func__, sm_state_info(sm));
521 *skip = 1;
522 return NULL;
525 if (pool_in_pools(sm->pool, remove_stack)) {
526 DIMPLIED("%s: remove: %s\n", __func__, sm_state_info(sm));
527 *modified = 1;
528 return NULL;
531 if (!is_merged(sm) || pool_in_pools(sm->pool, keep_stack) || sm_in_keep_leafs(sm, keep_stack)) {
532 DIMPLIED("%s: keep %s (%s, %s, %s): %s\n", __func__, sm->state->name,
533 is_merged(sm) ? "merged" : "not merged",
534 pool_in_pools(sm->pool, keep_stack) ? "in keep pools" : "not in keep pools",
535 sm_in_keep_leafs(sm, keep_stack) ? "reachable keep leaf" : "no keep leaf",
536 sm_state_info(sm));
537 return sm;
540 left = filter_pools(sm->left, remove_stack, keep_stack, &removed, recurse_cnt, start, skip, bail);
541 right = filter_pools(sm->right, remove_stack, keep_stack, &removed, recurse_cnt, start, skip, bail);
542 if (*bail || *skip)
543 return NULL;
544 if (!removed) {
545 DIMPLIED("%s: kept all: %s\n", __func__, sm_state_info(sm));
546 return sm;
548 *modified = 1;
549 if (!left && !right) {
550 DIMPLIED("%s: removed all: %s\n", __func__, sm_state_info(sm));
551 return NULL;
554 if (!left) {
555 ret = clone_sm(right);
556 ret->merged = 1;
557 ret->right = right;
558 ret->left = NULL;
559 } else if (!right) {
560 ret = clone_sm(left);
561 ret->merged = 1;
562 ret->left = left;
563 ret->right = NULL;
564 } else {
565 if (left->sym != sm->sym || strcmp(left->name, sm->name) != 0) {
566 left = clone_sm(left);
567 left->sym = sm->sym;
568 left->name = sm->name;
570 if (right->sym != sm->sym || strcmp(right->name, sm->name) != 0) {
571 right = clone_sm(right);
572 right->sym = sm->sym;
573 right->name = sm->name;
575 ret = merge_sm_states(left, right);
578 ret->pool = sm->pool;
580 DIMPLIED("%s: partial: %s\n", __func__, sm_state_info(sm));
581 return ret;
584 static struct stree *filter_stack(struct sm_state *gate_sm,
585 struct stree *pre_stree,
586 const struct state_list *remove_stack,
587 const struct state_list *keep_stack)
589 struct stree *ret = NULL;
590 struct sm_state *tmp;
591 struct sm_state *filtered_sm;
592 int modified;
593 int recurse_cnt;
594 struct timeval start;
595 int skip;
596 int bail = 0;
598 if (!remove_stack)
599 return NULL;
601 gettimeofday(&start, NULL);
602 FOR_EACH_SM(pre_stree, tmp) {
603 if (!tmp->merged || sm_in_keep_leafs(tmp, keep_stack))
604 continue;
605 modified = 0;
606 recurse_cnt = 0;
607 skip = 0;
608 filtered_sm = filter_pools(tmp, remove_stack, keep_stack, &modified, &recurse_cnt, &start, &skip, &bail);
609 if (going_too_slow())
610 return NULL;
611 if (bail)
612 return ret; /* Return the implications we figured out before time ran out. */
615 if (skip || !filtered_sm || !modified)
616 continue;
617 /* the assignments here are for borrowed implications */
618 filtered_sm->name = tmp->name;
619 filtered_sm->sym = tmp->sym;
620 avl_insert(&ret, filtered_sm);
621 } END_FOR_EACH_SM(tmp);
622 return ret;
625 static void separate_and_filter(struct sm_state *sm, int comparison, struct range_list *rl,
626 struct stree *pre_stree,
627 struct stree **true_states,
628 struct stree **false_states,
629 int *mixed)
631 struct state_list *true_stack = NULL;
632 struct state_list *false_stack = NULL;
633 struct timeval time_before;
634 struct timeval time_after;
635 int sec;
637 gettimeofday(&time_before, NULL);
639 DIMPLIED("checking implications: (%s (%s) %s %s)\n",
640 sm->name, sm->state->name, show_comparison(comparison), show_rl(rl));
642 if (!is_merged(sm)) {
643 DIMPLIED("%d '%s' from line %d is not merged.\n", get_lineno(), sm->name, sm->line);
644 return;
647 separate_pools(sm, comparison, rl, &true_stack, &false_stack, NULL, mixed);
649 if (full_debug) {
650 struct sm_state *sm;
652 FOR_EACH_PTR(true_stack, sm) {
653 sm_msg("TRUE POOL: %p", sm->pool);
654 } END_FOR_EACH_PTR(sm);
656 FOR_EACH_PTR(false_stack, sm) {
657 sm_msg("FALSE POOL: %p", sm->pool);
658 } END_FOR_EACH_PTR(sm);
661 DIMPLIED("filtering true stack.\n");
662 *true_states = filter_stack(sm, pre_stree, false_stack, true_stack);
663 DIMPLIED("filtering false stack.\n");
664 *false_states = filter_stack(sm, pre_stree, true_stack, false_stack);
665 free_slist(&true_stack);
666 free_slist(&false_stack);
668 gettimeofday(&time_after, NULL);
669 sec = time_after.tv_sec - time_before.tv_sec;
670 if (sec > 20)
671 sm_perror("Function too hairy. Ignoring implications after %d seconds.", sec);
674 static struct expression *get_last_expr(struct statement *stmt)
676 struct statement *last;
678 last = last_ptr_list((struct ptr_list *)stmt->stmts);
679 if (last->type == STMT_EXPRESSION)
680 return last->expression;
682 if (last->type == STMT_LABEL) {
683 if (last->label_statement &&
684 last->label_statement->type == STMT_EXPRESSION)
685 return last->label_statement->expression;
688 return NULL;
691 static struct expression *get_left_most_expr(struct expression *expr)
693 struct statement *compound;
694 struct expression *fake;
696 compound = get_expression_statement(expr);
697 if (compound)
698 return get_last_expr(compound);
700 expr = strip_parens(expr);
701 if (expr->type == EXPR_ASSIGNMENT)
702 return get_left_most_expr(expr->left);
703 fake = expr_get_fake_parent_expr(expr);
704 if (fake && fake->type == EXPR_ASSIGNMENT)
705 return fake->left;
706 return expr;
709 static int is_merged_expr(struct expression *expr)
711 struct sm_state *sm;
712 sval_t dummy;
714 if (get_value(expr, &dummy))
715 return 0;
716 sm = get_sm_state_expr(SMATCH_EXTRA, expr);
717 if (!sm)
718 return 0;
719 if (is_merged(sm))
720 return 1;
721 return 0;
724 static void delete_gate_sm_equiv(struct stree **stree, const char *name, struct symbol *sym)
726 struct smatch_state *state;
727 struct relation *rel;
729 state = get_state(SMATCH_EXTRA, name, sym);
730 if (!state)
731 return;
732 FOR_EACH_PTR(estate_related(state), rel) {
733 delete_state_stree(stree, SMATCH_EXTRA, rel->name, rel->sym);
734 } END_FOR_EACH_PTR(rel);
737 static void delete_gate_sm(struct stree **stree, const char *name, struct symbol *sym)
739 delete_state_stree(stree, SMATCH_EXTRA, name, sym);
742 static int handle_comparison(struct expression *expr,
743 struct stree **implied_true,
744 struct stree **implied_false)
746 struct sm_state *sm = NULL;
747 struct range_list *rl = NULL;
748 struct expression *left;
749 struct expression *right;
750 struct symbol *type;
751 int comparison = expr->op;
752 int mixed = 0;
754 left = get_left_most_expr(expr->left);
755 right = get_left_most_expr(expr->right);
757 if (is_merged_expr(left)) {
758 sm = get_sm_state_expr(SMATCH_EXTRA, left);
759 get_implied_rl(right, &rl);
760 } else if (is_merged_expr(right)) {
761 sm = get_sm_state_expr(SMATCH_EXTRA, right);
762 get_implied_rl(left, &rl);
763 comparison = flip_comparison(comparison);
766 if (!rl || !sm)
767 return 0;
769 type = get_type(expr);
770 if (!type)
771 return 0;
772 if (type_positive_bits(rl_type(rl)) > type_positive_bits(type))
773 type = rl_type(rl);
774 if (type_positive_bits(type) < 31)
775 type = &int_ctype;
776 rl = cast_rl(type, rl);
778 separate_and_filter(sm, comparison, rl, __get_cur_stree(), implied_true, implied_false, &mixed);
780 delete_gate_sm_equiv(implied_true, sm->name, sm->sym);
781 delete_gate_sm_equiv(implied_false, sm->name, sm->sym);
782 if (mixed) {
783 delete_gate_sm(implied_true, sm->name, sm->sym);
784 delete_gate_sm(implied_false, sm->name, sm->sym);
787 return 1;
790 static int handle_zero_comparison(struct expression *expr,
791 struct stree **implied_true,
792 struct stree **implied_false)
794 struct symbol *sym;
795 char *name;
796 struct sm_state *sm;
797 int mixed = 0;
798 int ret = 0;
800 if (expr->type == EXPR_POSTOP)
801 expr = strip_expr(expr->unop);
803 if (expr->type == EXPR_ASSIGNMENT) {
804 /* most of the time ->pools will be empty here because we
805 just set the state, but if have assigned a conditional
806 function there are implications. */
807 expr = expr->left;
810 name = expr_to_var_sym(expr, &sym);
811 if (!name || !sym)
812 goto free;
813 sm = get_sm_state(SMATCH_EXTRA, name, sym);
814 if (!sm || !sm->merged)
815 goto free;
817 separate_and_filter(sm, SPECIAL_NOTEQUAL, tmp_range_list(estate_type(sm->state), 0), __get_cur_stree(), implied_true, implied_false, &mixed);
818 delete_gate_sm_equiv(implied_true, sm->name, sm->sym);
819 delete_gate_sm_equiv(implied_false, sm->name, sm->sym);
820 if (mixed) {
821 delete_gate_sm(implied_true, sm->name, sm->sym);
822 delete_gate_sm(implied_false, sm->name, sm->sym);
825 ret = 1;
826 free:
827 free_string(name);
828 return ret;
831 static int handled_by_comparison_hook(struct expression *expr,
832 struct stree **implied_true,
833 struct stree **implied_false)
835 struct sm_state *sm, *true_sm, *false_sm;
836 struct state_list *true_stack = NULL;
837 struct state_list *false_stack = NULL;
838 struct stree *pre_stree;
840 sm = comparison_implication_hook(expr, &true_stack, &false_stack);
841 if (!sm)
842 return 0;
844 pre_stree = clone_stree(__get_cur_stree());
846 *implied_true = filter_stack(sm, pre_stree, false_stack, true_stack);
847 *implied_false = filter_stack(sm, pre_stree, true_stack, false_stack);
849 true_sm = get_sm_state_stree(*implied_true, sm->owner, sm->name, sm->sym);
850 false_sm = get_sm_state_stree(*implied_false, sm->owner, sm->name, sm->sym);
851 if (true_sm && strcmp(true_sm->state->name, "unknown") == 0)
852 delete_state_stree(implied_true, sm->owner, sm->name, sm->sym);
853 if (false_sm && strcmp(false_sm->state->name, "unknown") == 0)
854 delete_state_stree(implied_false, sm->owner, sm->name, sm->sym);
856 free_stree(&pre_stree);
857 free_slist(&true_stack);
858 free_slist(&false_stack);
860 return 1;
863 static int handled_by_extra_states(struct expression *expr,
864 struct stree **implied_true,
865 struct stree **implied_false)
867 sval_t sval;
869 /* If the expression is known then it has no implications. */
870 if (get_implied_value(expr, &sval))
871 return true;
873 if (expr->type == EXPR_COMPARE)
874 return handle_comparison(expr, implied_true, implied_false);
875 else
876 return handle_zero_comparison(expr, implied_true, implied_false);
879 static int handled_by_parsed_conditions(struct expression *expr,
880 struct stree **implied_true,
881 struct stree **implied_false)
883 struct state_list *true_stack = NULL;
884 struct state_list *false_stack = NULL;
885 struct stree *pre_stree;
886 struct sm_state *sm;
888 sm = parsed_condition_implication_hook(expr, &true_stack, &false_stack);
889 if (!sm)
890 return 0;
892 pre_stree = clone_stree(__get_cur_stree());
894 *implied_true = filter_stack(sm, pre_stree, false_stack, true_stack);
895 *implied_false = filter_stack(sm, pre_stree, true_stack, false_stack);
897 free_stree(&pre_stree);
898 free_slist(&true_stack);
899 free_slist(&false_stack);
901 return 1;
904 static int handled_by_stored_conditions(struct expression *expr,
905 struct stree **implied_true,
906 struct stree **implied_false)
908 struct state_list *true_stack = NULL;
909 struct state_list *false_stack = NULL;
910 struct stree *pre_stree;
911 struct sm_state *sm;
913 sm = stored_condition_implication_hook(expr, &true_stack, &false_stack);
914 if (!sm)
915 return 0;
917 pre_stree = clone_stree(__get_cur_stree());
919 *implied_true = filter_stack(sm, pre_stree, false_stack, true_stack);
920 *implied_false = filter_stack(sm, pre_stree, true_stack, false_stack);
922 free_stree(&pre_stree);
923 free_slist(&true_stack);
924 free_slist(&false_stack);
926 return 1;
929 static struct stree *saved_implied_true;
930 static struct stree *saved_implied_false;
931 static struct stree *extra_saved_implied_true;
932 static struct stree *extra_saved_implied_false;
934 static void separate_implication_states(struct stree **implied_true,
935 struct stree **implied_false,
936 int owner)
938 struct sm_state *sm;
940 /* We process these states later to preserve the implications. */
941 FOR_EACH_SM(*implied_true, sm) {
942 if (sm->owner == owner)
943 overwrite_sm_state_stree(&extra_saved_implied_true, sm);
944 } END_FOR_EACH_SM(sm);
945 FOR_EACH_SM(extra_saved_implied_true, sm) {
946 delete_state_stree(implied_true, sm->owner, sm->name, sm->sym);
947 } END_FOR_EACH_SM(sm);
949 FOR_EACH_SM(*implied_false, sm) {
950 if (sm->owner == owner)
951 overwrite_sm_state_stree(&extra_saved_implied_false, sm);
952 } END_FOR_EACH_SM(sm);
953 FOR_EACH_SM(extra_saved_implied_false, sm) {
954 delete_state_stree(implied_false, sm->owner, sm->name, sm->sym);
955 } END_FOR_EACH_SM(sm);
958 static void get_tf_states(struct expression *expr,
959 struct stree **implied_true,
960 struct stree **implied_false)
962 while (expr->type == EXPR_ASSIGNMENT && expr->op == '=')
963 expr = strip_parens(expr->left);
965 if (handled_by_parsed_conditions(expr, implied_true, implied_false))
966 return;
968 if (handled_by_comparison_hook(expr, implied_true, implied_false)) {
969 separate_implication_states(implied_true, implied_false, comparison_id);
970 return;
973 if (handled_by_extra_states(expr, implied_true, implied_false)) {
974 separate_implication_states(implied_true, implied_false, SMATCH_EXTRA);
975 return;
978 if (handled_by_stored_conditions(expr, implied_true, implied_false))
979 return;
982 static void save_implications_hook(struct expression *expr)
984 if (going_too_slow())
985 return;
986 get_tf_states(expr, &saved_implied_true, &saved_implied_false);
989 static void set_implied_states(struct expression *expr)
991 struct sm_state *sm;
993 if ((full_debug || implied_debug) &&
994 (expr || saved_implied_true || saved_implied_false)) {
995 char *name;
997 name = expr_to_str(expr);
998 printf("These are the implied states for the true path: (%s)\n", name);
999 __print_stree(saved_implied_true);
1000 printf("These are the implied states for the false path: (%s)\n", name);
1001 __print_stree(saved_implied_false);
1002 free_string(name);
1005 FOR_EACH_SM(saved_implied_true, sm) {
1006 __set_true_false_sm(sm, NULL);
1007 } END_FOR_EACH_SM(sm);
1008 free_stree(&saved_implied_true);
1010 FOR_EACH_SM(saved_implied_false, sm) {
1011 __set_true_false_sm(NULL, sm);
1012 } END_FOR_EACH_SM(sm);
1013 free_stree(&saved_implied_false);
1016 static void set_extra_implied_states(struct expression *expr)
1018 saved_implied_true = extra_saved_implied_true;
1019 saved_implied_false = extra_saved_implied_false;
1020 extra_saved_implied_true = NULL;
1021 extra_saved_implied_false = NULL;
1022 set_implied_states(NULL);
1025 void param_limit_implications(struct expression *expr, int param, char *key, char *value, struct stree **implied)
1027 struct expression *orig_expr, *arg;
1028 struct symbol *compare_type;
1029 char *name;
1030 struct symbol *sym;
1031 struct sm_state *sm;
1032 struct sm_state *tmp;
1033 struct stree *implied_true = NULL;
1034 struct stree *implied_false = NULL;
1035 struct range_list *orig, *limit;
1036 char *left_name = NULL;
1037 struct symbol *left_sym = NULL;
1038 int mixed = 0;
1040 if (time_parsing_function() > 40)
1041 return;
1043 orig_expr = expr;
1044 while (expr->type == EXPR_ASSIGNMENT)
1045 expr = strip_expr(expr->right);
1046 if (expr->type != EXPR_CALL)
1047 return;
1049 arg = get_argument_from_call_expr(expr->args, param);
1050 if (!arg)
1051 return;
1053 arg = strip_parens(arg);
1054 while (arg->type == EXPR_ASSIGNMENT && arg->op == '=')
1055 arg = strip_parens(arg->left);
1057 name = get_variable_from_key(arg, key, &sym);
1058 if (!name || !sym)
1059 goto free;
1061 sm = get_sm_state(SMATCH_EXTRA, name, sym);
1062 if (!sm || !sm->merged)
1063 goto free;
1065 if (strcmp(key, "$") == 0)
1066 compare_type = get_arg_type(expr->fn, param);
1067 else
1068 compare_type = get_member_type_from_key(arg, key);
1070 orig = estate_rl(sm->state);
1071 orig = cast_rl(compare_type, orig);
1073 call_results_to_rl(expr, compare_type, value, &limit);
1075 separate_and_filter(sm, PARAM_LIMIT, limit, __get_cur_stree(), &implied_true, &implied_false, &mixed);
1077 if (orig_expr->type == EXPR_ASSIGNMENT)
1078 left_name = expr_to_var_sym(orig_expr->left, &left_sym);
1080 FOR_EACH_SM(implied_true, tmp) {
1082 if (implied_debug)
1083 sm_msg("param_implication: param='%s' limit='%s' sm='%s'", name, show_rl(limit), show_sm(tmp));
1086 * What we're trying to do here is preserve the sm state so that
1087 * smatch extra doesn't create a new sm state when it parses the
1088 * PARAM_LIMIT.
1090 if (!mixed && tmp->sym == sym &&
1091 strcmp(tmp->name, name) == 0 &&
1092 (!left_name || strcmp(left_name, name) != 0)) {
1093 overwrite_sm_state_stree(implied, tmp);
1094 continue;
1097 __set_sm(tmp);
1098 } END_FOR_EACH_SM(tmp);
1100 free_stree(&implied_true);
1101 free_stree(&implied_false);
1102 free:
1103 free_string(name);
1106 struct stree *__implied_case_stree(struct expression *switch_expr,
1107 struct range_list *rl,
1108 struct range_list_stack **remaining_cases,
1109 struct stree **raw_stree)
1111 char *name;
1112 struct symbol *sym;
1113 struct var_sym_list *vsl;
1114 struct sm_state *sm;
1115 struct stree *true_states = NULL;
1116 struct stree *false_states = NULL;
1117 struct stree *extra_states;
1118 struct stree *ret = clone_stree(*raw_stree);
1120 name = expr_to_chunk_sym_vsl(switch_expr, &sym, &vsl);
1122 if (rl)
1123 filter_top_rl(remaining_cases, rl);
1124 else
1125 rl = clone_rl(top_rl(*remaining_cases));
1127 if (name) {
1128 sm = get_sm_state_stree(*raw_stree, SMATCH_EXTRA, name, sym);
1129 if (sm)
1130 separate_and_filter(sm, SPECIAL_EQUAL, rl, *raw_stree, &true_states, &false_states, NULL);
1133 __push_fake_cur_stree();
1134 __unnullify_path();
1135 if (name)
1136 set_extra_nomod_vsl(name, sym, vsl, NULL, alloc_estate_rl(rl));
1137 __pass_case_to_client(switch_expr, rl);
1138 extra_states = __pop_fake_cur_stree();
1139 overwrite_stree(extra_states, &true_states);
1140 overwrite_stree(true_states, &ret);
1141 free_stree(&extra_states);
1142 free_stree(&true_states);
1143 free_stree(&false_states);
1145 free_string(name);
1146 return ret;
1149 static void match_end_func(struct symbol *sym)
1151 if (__inline_fn)
1152 return;
1153 implied_debug_msg = NULL;
1156 static void get_tf_stacks_from_pool(struct sm_state *gate_sm,
1157 struct sm_state *pool_sm,
1158 struct state_list **true_stack,
1159 struct state_list **false_stack)
1161 struct sm_state *tmp;
1162 int possibly_true = 0;
1164 if (!gate_sm)
1165 return;
1167 if (strcmp(gate_sm->state->name, pool_sm->state->name) == 0) {
1168 add_ptr_list(true_stack, pool_sm);
1169 return;
1172 FOR_EACH_PTR(gate_sm->possible, tmp) {
1173 if (strcmp(tmp->state->name, pool_sm->state->name) == 0) {
1174 possibly_true = 1;
1175 break;
1177 } END_FOR_EACH_PTR(tmp);
1179 if (!possibly_true) {
1180 add_ptr_list(false_stack, gate_sm);
1181 return;
1184 get_tf_stacks_from_pool(gate_sm->left, pool_sm, true_stack, false_stack);
1185 get_tf_stacks_from_pool(gate_sm->right, pool_sm, true_stack, false_stack);
1189 * The situation is we have a SMATCH_EXTRA state and we want to break it into
1190 * each of the ->possible states and find the implications of each. The caller
1191 * has to use __push_fake_cur_stree() to preserve the correct states so they
1192 * can be restored later.
1194 void overwrite_states_using_pool(struct sm_state *gate_sm, struct sm_state *pool_sm)
1196 struct state_list *true_stack = NULL;
1197 struct state_list *false_stack = NULL;
1198 struct stree *pre_stree;
1199 struct stree *implied_true;
1200 struct sm_state *tmp;
1202 if (!pool_sm->pool)
1203 return;
1205 get_tf_stacks_from_pool(gate_sm, pool_sm, &true_stack, &false_stack);
1207 pre_stree = clone_stree(__get_cur_stree());
1209 implied_true = filter_stack(gate_sm, pre_stree, false_stack, true_stack);
1211 free_stree(&pre_stree);
1212 free_slist(&true_stack);
1213 free_slist(&false_stack);
1215 FOR_EACH_SM(implied_true, tmp) {
1216 __set_sm(tmp);
1217 } END_FOR_EACH_SM(tmp);
1219 free_stree(&implied_true);
1222 int assume(struct expression *expr)
1224 int orig_final_pass = final_pass;
1226 in_fake_env++;
1227 final_pass = 0;
1228 __push_fake_cur_stree();
1229 __split_whole_condition(expr);
1230 final_pass = orig_final_pass;
1231 in_fake_env--;
1233 return 1;
1236 void end_assume(void)
1238 __discard_false_states();
1239 __free_fake_cur_stree();
1242 int impossible_assumption(struct expression *left, int op, sval_t sval)
1244 struct expression *value;
1245 struct expression *comparison;
1246 int ret;
1248 value = value_expr(sval.value);
1249 comparison = compare_expression(left, op, value);
1251 if (!assume(comparison))
1252 return 0;
1253 ret = is_impossible_path();
1254 end_assume();
1256 return ret;
1259 void __extra_match_condition(struct expression *expr);
1260 void __comparison_match_condition(struct expression *expr);
1261 void __stored_condition(struct expression *expr);
1262 void register_implications(int id)
1264 add_hook(&save_implications_hook, CONDITION_HOOK);
1265 add_hook(&set_implied_states, CONDITION_HOOK);
1266 add_hook(&__extra_match_condition, CONDITION_HOOK);
1267 add_hook(&__comparison_match_condition, CONDITION_HOOK);
1268 add_hook(&set_extra_implied_states, CONDITION_HOOK);
1269 add_hook(&__stored_condition, CONDITION_HOOK);
1270 add_hook(&match_end_func, END_FUNC_HOOK);