db: introduce the --db-file=/path/to/smatch_db.sqlite option
[smatch.git] / smatch_implied.c
blobfc86de2b3cffceb4f123868574df3b451dbc8bed
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 <sys/time.h>
60 #include <time.h>
61 #include "smatch.h"
62 #include "smatch_slist.h"
63 #include "smatch_extra.h"
65 char *implied_debug_msg;
66 #define DIMPLIED(msg...) do { if (option_debug_implied || option_debug) printf(msg); } while (0)
68 int option_debug_implied = 0;
71 * tmp_range_list():
72 * It messes things up to free range list allocations. This helper fuction
73 * lets us reuse memory instead of doing new allocations.
75 static struct range_list *tmp_range_list(struct symbol *type, long long num)
77 static struct range_list *my_list = NULL;
78 static struct data_range *my_range;
80 __free_ptr_list((struct ptr_list **)&my_list);
81 my_range = alloc_range(ll_to_sval(num), ll_to_sval(num));
82 add_ptr_list(&my_list, my_range);
83 return my_list;
86 static void print_debug_tf(struct sm_state *sm, int istrue, int isfalse)
88 if (!option_debug_implied && !option_debug)
89 return;
91 if (istrue && isfalse) {
92 printf("%s: %d: does not exist.\n", show_sm(sm), sm->line);
93 } else if (istrue) {
94 printf("'%s = %s' from %d is true. %s[stree %d]\n", sm->name, show_state(sm->state),
95 sm->line, sm->merged ? "[merged]" : "[leaf]",
96 get_stree_id(sm->pool));
97 } else if (isfalse) {
98 printf("'%s = %s' from %d is false. %s[stree %d]\n", sm->name, show_state(sm->state),
99 sm->line,
100 sm->merged ? "[merged]" : "[leaf]",
101 get_stree_id(sm->pool));
102 } else {
103 printf("'%s = %s' from %d could be true or false. %s[stree %d]\n", sm->name,
104 show_state(sm->state), sm->line,
105 sm->merged ? "[merged]" : "[leaf]",
106 get_stree_id(sm->pool));
110 static int create_fake_history(struct sm_state *sm, int comparison, struct range_list *rl)
112 struct range_list *orig_rl;
113 struct range_list *true_rl, *false_rl;
114 struct stree *true_stree, *false_stree;
115 struct sm_state *true_sm, *false_sm;
116 sval_t sval;
118 if (is_merged(sm) || sm->left || sm->right)
119 return 0;
120 if (!rl_to_sval(rl, &sval))
121 return 0;
122 if (!estate_rl(sm->state))
123 return 0;
125 orig_rl = cast_rl(rl_type(rl), estate_rl(sm->state));
126 split_comparison_rl(orig_rl, comparison, rl, &true_rl, &false_rl, NULL, NULL);
128 true_rl = rl_truncate_cast(estate_type(sm->state), true_rl);
129 false_rl = rl_truncate_cast(estate_type(sm->state), false_rl);
130 if (is_whole_rl(true_rl) || is_whole_rl(false_rl) ||
131 !true_rl || !false_rl ||
132 rl_equiv(orig_rl, true_rl) || rl_equiv(orig_rl, false_rl) ||
133 rl_equiv(estate_rl(sm->state), true_rl) || rl_equiv(estate_rl(sm->state), false_rl))
134 return 0;
136 if (rl_intersection(true_rl, false_rl)) {
137 sm_msg("internal error parsing (%s (%s) %s %s)",
138 sm->name, sm->state->name, show_special(comparison), show_rl(rl));
139 sm_msg("true_rl = %s false_rl = %s intersection = %s",
140 show_rl(true_rl), show_rl(false_rl), show_rl(rl_intersection(true_rl, false_rl)));
141 return 0;
144 if (option_debug)
145 sm_msg("fake_history: %s vs %s. %s %s %s. --> T: %s F: %s",
146 sm->name, show_rl(rl), sm->state->name, show_special(comparison), show_rl(rl),
147 show_rl(true_rl), show_rl(false_rl));
149 true_sm = clone_sm(sm);
150 false_sm = clone_sm(sm);
152 true_sm->state = alloc_estate_rl(cast_rl(estate_type(sm->state), true_rl));
153 free_slist(&true_sm->possible);
154 add_possible_sm(true_sm, true_sm);
155 false_sm->state = alloc_estate_rl(cast_rl(estate_type(sm->state), false_rl));
156 free_slist(&false_sm->possible);
157 add_possible_sm(false_sm, false_sm);
159 true_stree = clone_stree(sm->pool);
160 false_stree = clone_stree(sm->pool);
162 overwrite_sm_state_stree(&true_stree, true_sm);
163 overwrite_sm_state_stree(&false_stree, false_sm);
165 true_sm->pool = true_stree;
166 false_sm->pool = false_stree;
168 sm->merged = 1;
169 sm->left = true_sm;
170 sm->right = false_sm;
172 return 1;
176 * add_pool() adds a slist to *pools. If the slist has already been
177 * added earlier then it doesn't get added a second time.
179 void add_pool(struct state_list **pools, struct sm_state *new)
181 struct sm_state *tmp;
183 FOR_EACH_PTR(*pools, tmp) {
184 if (tmp->pool < new->pool)
185 continue;
186 else if (tmp->pool == new->pool) {
187 return;
188 } else {
189 INSERT_CURRENT(new, tmp);
190 return;
192 } END_FOR_EACH_PTR(tmp);
193 add_ptr_list(pools, new);
196 static int pool_in_pools(struct stree *pool,
197 const struct state_list *slist)
199 struct sm_state *tmp;
201 FOR_EACH_PTR(slist, tmp) {
202 if (!tmp->pool)
203 continue;
204 if (tmp->pool == pool)
205 return 1;
206 } END_FOR_EACH_PTR(tmp);
207 return 0;
210 static int remove_pool(struct state_list **pools, struct stree *remove)
212 struct sm_state *tmp;
213 int ret = 0;
215 FOR_EACH_PTR(*pools, tmp) {
216 if (tmp->pool == remove) {
217 DELETE_CURRENT_PTR(tmp);
218 ret = 1;
220 } END_FOR_EACH_PTR(tmp);
222 return ret;
226 * If 'foo' == 99 add it that pool to the true pools. If it's false, add it to
227 * the false pools. If we're not sure, then we don't add it to either.
229 static void do_compare(struct sm_state *sm, int comparison, struct range_list *rl,
230 struct state_list **true_stack,
231 struct state_list **maybe_stack,
232 struct state_list **false_stack,
233 int *mixed, struct sm_state *gate_sm)
235 int istrue;
236 int isfalse;
237 struct range_list *var_rl;
239 if (!sm->pool)
240 return;
242 var_rl = cast_rl(rl_type(rl), estate_rl(sm->state));
244 istrue = !possibly_false_rl(var_rl, comparison, rl);
245 isfalse = !possibly_true_rl(var_rl, comparison, rl);
247 print_debug_tf(sm, istrue, isfalse);
249 /* give up if we have borrowed implications (smatch_equiv.c) */
250 if (sm->sym != gate_sm->sym ||
251 strcmp(sm->name, gate_sm->name) != 0) {
252 if (mixed)
253 *mixed = 1;
256 if (mixed && !*mixed && !is_merged(sm) && !istrue && !isfalse) {
257 if (!create_fake_history(sm, comparison, rl)) {
258 if (mixed)
259 *mixed = 1;
263 if (istrue)
264 add_pool(true_stack, sm);
265 else if (isfalse)
266 add_pool(false_stack, sm);
267 else
268 add_pool(maybe_stack, sm);
272 static int is_checked(struct state_list *checked, struct sm_state *sm)
274 struct sm_state *tmp;
276 FOR_EACH_PTR(checked, tmp) {
277 if (tmp == sm)
278 return 1;
279 } END_FOR_EACH_PTR(tmp);
280 return 0;
284 * separate_pools():
285 * Example code: if (foo == 99) {
287 * Say 'foo' is a merged state that has many possible values. It is the combination
288 * of merges. separate_pools() iterates through the pools recursively and calls
289 * do_compare() for each time 'foo' was set.
291 static void __separate_pools(struct sm_state *sm, int comparison, struct range_list *rl,
292 struct state_list **true_stack,
293 struct state_list **maybe_stack,
294 struct state_list **false_stack,
295 struct state_list **checked, int *mixed, struct sm_state *gate_sm)
297 int free_checked = 0;
298 struct state_list *checked_states = NULL;
300 if (!sm)
301 return;
304 * If it looks like this is going to take too long as-is, then don't
305 * create even more fake history.
307 if (mixed && sm->nr_children > 100)
308 *mixed = 1;
311 Sometimes the implications are just too big to deal with
312 so we bail. Theoretically, bailing out here can cause more false
313 positives but won't hide actual bugs.
315 if (sm->nr_children > 4000) {
316 if (option_debug || option_debug_implied) {
317 static char buf[1028];
318 snprintf(buf, sizeof(buf), "debug: %s: nr_children over 4000 (%d). (%s %s)",
319 __func__, sm->nr_children, sm->name, show_state(sm->state));
320 implied_debug_msg = buf;
322 return;
325 if (checked == NULL) {
326 checked = &checked_states;
327 free_checked = 1;
329 if (is_checked(*checked, sm))
330 return;
331 add_ptr_list(checked, sm);
333 do_compare(sm, comparison, rl, true_stack, maybe_stack, false_stack, mixed, gate_sm);
335 __separate_pools(sm->left, comparison, rl, true_stack, maybe_stack, false_stack, checked, mixed, gate_sm);
336 __separate_pools(sm->right, comparison, rl, true_stack, maybe_stack, false_stack, checked, mixed, gate_sm);
337 if (free_checked)
338 free_slist(checked);
341 static void separate_pools(struct sm_state *sm, int comparison, struct range_list *rl,
342 struct state_list **true_stack,
343 struct state_list **false_stack,
344 struct state_list **checked, int *mixed)
346 struct state_list *maybe_stack = NULL;
347 struct sm_state *tmp;
349 __separate_pools(sm, comparison, rl, true_stack, &maybe_stack, false_stack, checked, mixed, sm);
351 if (option_debug) {
352 struct sm_state *sm;
354 FOR_EACH_PTR(*true_stack, sm) {
355 sm_msg("TRUE %s [stree %d]", show_sm(sm), get_stree_id(sm->pool));
356 } END_FOR_EACH_PTR(sm);
358 FOR_EACH_PTR(maybe_stack, sm) {
359 sm_msg("MAYBE %s [stree %d]", show_sm(sm), get_stree_id(sm->pool));
360 } END_FOR_EACH_PTR(sm);
362 FOR_EACH_PTR(*false_stack, sm) {
363 sm_msg("FALSE %s [stree %d]", show_sm(sm), get_stree_id(sm->pool));
364 } END_FOR_EACH_PTR(sm);
366 /* if it's a maybe then remove it */
367 FOR_EACH_PTR(maybe_stack, tmp) {
368 remove_pool(false_stack, tmp->pool);
369 remove_pool(true_stack, tmp->pool);
370 } END_FOR_EACH_PTR(tmp);
372 /* if it's both true and false remove it from both */
373 FOR_EACH_PTR(*true_stack, tmp) {
374 if (remove_pool(false_stack, tmp->pool))
375 DELETE_CURRENT_PTR(tmp);
376 } END_FOR_EACH_PTR(tmp);
379 static int sm_in_keep_leafs(struct sm_state *sm, const struct state_list *keep_gates)
381 struct sm_state *tmp, *old;
383 FOR_EACH_PTR(keep_gates, tmp) {
384 if (is_merged(tmp))
385 continue;
386 old = get_sm_state_stree(tmp->pool, sm->owner, sm->name, sm->sym);
387 if (!old)
388 continue;
389 if (old == sm)
390 return 1;
391 } END_FOR_EACH_PTR(tmp);
392 return 0;
395 static int taking_too_long(void)
397 static void *printed;
399 if (out_of_memory())
400 return 1;
402 if (time_parsing_function() < 60)
403 return 0;
405 if (!__inline_fn && printed != cur_func_sym) {
406 sm_msg("internal: turning off implications after 60 seconds");
407 printed = cur_func_sym;
409 return 1;
413 * NOTE: If a state is in both the keep stack and the remove stack then that is
414 * a bug. Only add states which are definitely true or definitely false. If
415 * you have a leaf state that could be both true and false, then create a fake
416 * split history where one side is true and one side is false. Otherwise, if
417 * you can't do that, then don't add it to either list.
419 struct sm_state *filter_pools(struct sm_state *sm,
420 const struct state_list *remove_stack,
421 const struct state_list *keep_stack,
422 int *modified, int *recurse_cnt,
423 struct timeval *start)
425 struct sm_state *ret = NULL;
426 struct sm_state *left;
427 struct sm_state *right;
428 int removed = 0;
429 struct timeval now;
431 if (!sm)
432 return NULL;
433 if (sm->skip_implications)
434 return sm;
435 if (taking_too_long())
436 return sm;
438 gettimeofday(&now, NULL);
439 if ((*recurse_cnt)++ > 1000 || now.tv_sec - start->tv_sec > 5) {
440 if (local_debug || option_debug_implied) {
441 static char buf[1028];
442 snprintf(buf, sizeof(buf), "debug: %s: nr_children over 4000 (%d). (%s %s)",
443 __func__, sm->nr_children, sm->name, show_state(sm->state));
444 implied_debug_msg = buf;
446 sm->skip_implications = 1;
447 return sm;
450 if (pool_in_pools(sm->pool, remove_stack)) {
451 DIMPLIED("removed [stree %d] %s from %d\n", get_stree_id(sm->pool), show_sm(sm), sm->line);
452 *modified = 1;
453 return NULL;
456 if (!is_merged(sm) || pool_in_pools(sm->pool, keep_stack) || sm_in_keep_leafs(sm, keep_stack)) {
457 DIMPLIED("kept [stree %d] %s from %d. %s. %s. %s.\n", get_stree_id(sm->pool), show_sm(sm), sm->line,
458 is_merged(sm) ? "merged" : "not merged",
459 pool_in_pools(sm->pool, keep_stack) ? "not in keep pools" : "in keep pools",
460 sm_in_keep_leafs(sm, keep_stack) ? "reachable keep leaf" : "no keep leaf");
461 return sm;
464 DIMPLIED("checking [stree %d] %s from %d (%d) left = %s [stree %d] right = %s [stree %d]\n",
465 get_stree_id(sm->pool),
466 show_sm(sm), sm->line, sm->nr_children,
467 sm->left ? sm->left->state->name : "<none>", sm->left ? get_stree_id(sm->left->pool) : -1,
468 sm->right ? sm->right->state->name : "<none>", sm->right ? get_stree_id(sm->right->pool) : -1);
469 left = filter_pools(sm->left, remove_stack, keep_stack, &removed, recurse_cnt, start);
470 right = filter_pools(sm->right, remove_stack, keep_stack, &removed, recurse_cnt, start);
471 if (!removed) {
472 DIMPLIED("kept [stree %d] %s from %d\n", get_stree_id(sm->pool), show_sm(sm), sm->line);
473 return sm;
475 *modified = 1;
476 if (!left && !right) {
477 DIMPLIED("removed [stree %d] %s from %d <none>\n", get_stree_id(sm->pool), show_sm(sm), sm->line);
478 return NULL;
481 if (!left) {
482 ret = clone_sm(right);
483 ret->merged = 1;
484 ret->right = right;
485 ret->left = NULL;
486 } else if (!right) {
487 ret = clone_sm(left);
488 ret->merged = 1;
489 ret->left = left;
490 ret->right = NULL;
491 } else {
492 if (left->sym != sm->sym || strcmp(left->name, sm->name) != 0) {
493 left = clone_sm(left);
494 left->sym = sm->sym;
495 left->name = sm->name;
497 if (right->sym != sm->sym || strcmp(right->name, sm->name) != 0) {
498 right = clone_sm(right);
499 right->sym = sm->sym;
500 right->name = sm->name;
502 ret = merge_sm_states(left, right);
505 ret->pool = sm->pool;
507 DIMPLIED("partial %s => ", show_sm(sm));
508 DIMPLIED("%s from %d [stree %d]\n", show_sm(ret), sm->line, get_stree_id(sm->pool));
509 return ret;
512 static struct stree *filter_stack(struct sm_state *gate_sm,
513 struct stree *pre_stree,
514 const struct state_list *remove_stack,
515 const struct state_list *keep_stack)
517 struct stree *ret = NULL;
518 struct sm_state *tmp;
519 struct sm_state *filtered_sm;
520 int modified;
521 int recurse_cnt;
522 struct timeval start;
524 if (!remove_stack)
525 return NULL;
527 if (taking_too_long())
528 return NULL;
530 FOR_EACH_SM(pre_stree, tmp) {
531 if (option_debug)
532 sm_msg("%s: %s", __func__, show_sm(tmp));
533 if (!tmp->merged)
534 continue;
535 if (sm_in_keep_leafs(tmp, keep_stack))
536 continue;
537 modified = 0;
538 recurse_cnt = 0;
539 gettimeofday(&start, NULL);
540 filtered_sm = filter_pools(tmp, remove_stack, keep_stack, &modified, &recurse_cnt, &start);
541 if (!filtered_sm || !modified)
542 continue;
543 /* the assignments here are for borrowed implications */
544 filtered_sm->name = tmp->name;
545 filtered_sm->sym = tmp->sym;
546 avl_insert(&ret, filtered_sm);
547 if (out_of_memory() || taking_too_long())
548 return NULL;
550 } END_FOR_EACH_SM(tmp);
551 return ret;
554 static void separate_and_filter(struct sm_state *sm, int comparison, struct range_list *rl,
555 struct stree *pre_stree,
556 struct stree **true_states,
557 struct stree **false_states,
558 int *mixed)
560 struct state_list *true_stack = NULL;
561 struct state_list *false_stack = NULL;
562 struct timeval time_before;
563 struct timeval time_after;
564 int sec;
566 gettimeofday(&time_before, NULL);
568 if (!is_merged(sm)) {
569 DIMPLIED("%d '%s' is not merged.\n", get_lineno(), sm->name);
570 return;
573 if (option_debug_implied || option_debug) {
574 sm_msg("checking implications: (%s %s %s)",
575 sm->name, show_special(comparison), show_rl(rl));
578 separate_pools(sm, comparison, rl, &true_stack, &false_stack, NULL, mixed);
580 DIMPLIED("filtering true stack.\n");
581 *true_states = filter_stack(sm, pre_stree, false_stack, true_stack);
582 DIMPLIED("filtering false stack.\n");
583 *false_states = filter_stack(sm, pre_stree, true_stack, false_stack);
584 free_slist(&true_stack);
585 free_slist(&false_stack);
586 if (option_debug_implied || option_debug) {
587 printf("These are the implied states for the true path: (%s %s %s)\n",
588 sm->name, show_special(comparison), show_rl(rl));
589 __print_stree(*true_states);
590 printf("These are the implied states for the false path: (%s %s %s)\n",
591 sm->name, show_special(comparison), show_rl(rl));
592 __print_stree(*false_states);
595 gettimeofday(&time_after, NULL);
596 sec = time_after.tv_sec - time_before.tv_sec;
597 if (sec > 20) {
598 sm->nr_children = 4000;
599 sm_msg("Function too hairy. Ignoring implications after %d seconds.", sec);
603 static struct expression *get_last_expr(struct statement *stmt)
605 struct statement *last;
607 last = last_ptr_list((struct ptr_list *)stmt->stmts);
608 if (last->type == STMT_EXPRESSION)
609 return last->expression;
611 if (last->type == STMT_LABEL) {
612 if (last->label_statement &&
613 last->label_statement->type == STMT_EXPRESSION)
614 return last->label_statement->expression;
617 return NULL;
620 static struct expression *get_left_most_expr(struct expression *expr)
622 struct statement *compound;
624 compound = get_expression_statement(expr);
625 if (compound)
626 return get_last_expr(compound);
628 expr = strip_parens(expr);
629 if (expr->type == EXPR_ASSIGNMENT)
630 return get_left_most_expr(expr->left);
631 return expr;
634 static int is_merged_expr(struct expression *expr)
636 struct sm_state *sm;
637 sval_t dummy;
639 if (get_value(expr, &dummy))
640 return 0;
641 sm = get_sm_state_expr(SMATCH_EXTRA, expr);
642 if (!sm)
643 return 0;
644 if (is_merged(sm))
645 return 1;
646 return 0;
649 static void delete_gate_sm_equiv(struct stree **stree, const char *name, struct symbol *sym)
651 struct smatch_state *state;
652 struct relation *rel;
654 state = get_state(SMATCH_EXTRA, name, sym);
655 if (!state)
656 return;
657 FOR_EACH_PTR(estate_related(state), rel) {
658 delete_state_stree(stree, SMATCH_EXTRA, rel->name, rel->sym);
659 } END_FOR_EACH_PTR(rel);
662 static void delete_gate_sm(struct stree **stree, const char *name, struct symbol *sym)
664 delete_state_stree(stree, SMATCH_EXTRA, name, sym);
667 static int handle_comparison(struct expression *expr,
668 struct stree **implied_true,
669 struct stree **implied_false)
671 struct sm_state *sm = NULL;
672 struct range_list *rl = NULL;
673 struct expression *left;
674 struct expression *right;
675 struct symbol *type;
676 int comparison = expr->op;
677 int mixed = 0;
679 left = get_left_most_expr(expr->left);
680 right = get_left_most_expr(expr->right);
682 if (is_merged_expr(left)) {
683 sm = get_sm_state_expr(SMATCH_EXTRA, left);
684 get_implied_rl(right, &rl);
685 } else if (is_merged_expr(right)) {
686 sm = get_sm_state_expr(SMATCH_EXTRA, right);
687 get_implied_rl(left, &rl);
688 comparison = flip_comparison(comparison);
691 if (!rl || !sm)
692 return 0;
694 type = get_type(expr);
695 if (!type)
696 return 0;
697 if (type_positive_bits(rl_type(rl)) > type_positive_bits(type))
698 type = rl_type(rl);
699 if (type_positive_bits(type) < 31)
700 type = &int_ctype;
701 rl = cast_rl(type, rl);
703 separate_and_filter(sm, comparison, rl, __get_cur_stree(), implied_true, implied_false, &mixed);
705 delete_gate_sm_equiv(implied_true, sm->name, sm->sym);
706 delete_gate_sm_equiv(implied_false, sm->name, sm->sym);
707 if (mixed) {
708 delete_gate_sm(implied_true, sm->name, sm->sym);
709 delete_gate_sm(implied_false, sm->name, sm->sym);
712 return 1;
715 static int handle_zero_comparison(struct expression *expr,
716 struct stree **implied_true,
717 struct stree **implied_false)
719 struct symbol *sym;
720 char *name;
721 struct sm_state *sm;
722 int mixed = 0;
723 int ret = 0;
725 if (expr->type == EXPR_POSTOP)
726 expr = strip_expr(expr->unop);
728 if (expr->type == EXPR_ASSIGNMENT) {
729 /* most of the time ->pools will be empty here because we
730 just set the state, but if have assigned a conditional
731 function there are implications. */
732 expr = expr->left;
735 name = expr_to_var_sym(expr, &sym);
736 if (!name || !sym)
737 goto free;
738 sm = get_sm_state(SMATCH_EXTRA, name, sym);
739 if (!sm)
740 goto free;
742 separate_and_filter(sm, SPECIAL_NOTEQUAL, tmp_range_list(estate_type(sm->state), 0), __get_cur_stree(), implied_true, implied_false, &mixed);
743 delete_gate_sm_equiv(implied_true, sm->name, sm->sym);
744 delete_gate_sm_equiv(implied_false, sm->name, sm->sym);
745 if (mixed) {
746 delete_gate_sm(implied_true, sm->name, sm->sym);
747 delete_gate_sm(implied_false, sm->name, sm->sym);
750 ret = 1;
751 free:
752 free_string(name);
753 return ret;
756 static int handled_by_comparison_hook(struct expression *expr,
757 struct stree **implied_true,
758 struct stree **implied_false)
760 struct state_list *true_stack = NULL;
761 struct state_list *false_stack = NULL;
762 struct stree *pre_stree;
763 struct sm_state *sm;
765 sm = comparison_implication_hook(expr, &true_stack, &false_stack);
766 if (!sm)
767 return 0;
769 pre_stree = clone_stree(__get_cur_stree());
771 *implied_true = filter_stack(sm, pre_stree, false_stack, true_stack);
772 *implied_false = filter_stack(sm, pre_stree, true_stack, false_stack);
774 free_stree(&pre_stree);
775 free_slist(&true_stack);
776 free_slist(&false_stack);
778 return 1;
781 static int handled_by_extra_states(struct expression *expr,
782 struct stree **implied_true,
783 struct stree **implied_false)
785 if (expr->type == EXPR_COMPARE)
786 return handle_comparison(expr, implied_true, implied_false);
787 else
788 return handle_zero_comparison(expr, implied_true, implied_false);
791 static int handled_by_stored_conditions(struct expression *expr,
792 struct stree **implied_true,
793 struct stree **implied_false)
795 struct state_list *true_stack = NULL;
796 struct state_list *false_stack = NULL;
797 struct stree *pre_stree;
798 struct sm_state *sm;
800 sm = stored_condition_implication_hook(expr, &true_stack, &false_stack);
801 if (!sm)
802 return 0;
804 pre_stree = clone_stree(__get_cur_stree());
806 *implied_true = filter_stack(sm, pre_stree, false_stack, true_stack);
807 *implied_false = filter_stack(sm, pre_stree, true_stack, false_stack);
809 free_stree(&pre_stree);
810 free_slist(&true_stack);
811 free_slist(&false_stack);
813 return 1;
816 static int found_implications;
817 static struct stree *saved_implied_true;
818 static struct stree *saved_implied_false;
819 static struct stree *extra_saved_implied_true;
820 static struct stree *extra_saved_implied_false;
822 static void separate_extra_states(struct stree **implied_true,
823 struct stree **implied_false)
825 struct sm_state *sm;
827 /* We process extra states later to preserve the implications. */
828 FOR_EACH_SM(*implied_true, sm) {
829 if (sm->owner == SMATCH_EXTRA)
830 overwrite_sm_state_stree(&extra_saved_implied_true, sm);
831 } END_FOR_EACH_SM(sm);
832 FOR_EACH_SM(extra_saved_implied_true, sm) {
833 delete_state_stree(implied_true, sm->owner, sm->name, sm->sym);
834 } END_FOR_EACH_SM(sm);
836 FOR_EACH_SM(*implied_false, sm) {
837 if (sm->owner == SMATCH_EXTRA)
838 overwrite_sm_state_stree(&extra_saved_implied_false, sm);
839 } END_FOR_EACH_SM(sm);
840 FOR_EACH_SM(extra_saved_implied_false, sm) {
841 delete_state_stree(implied_false, sm->owner, sm->name, sm->sym);
842 } END_FOR_EACH_SM(sm);
845 static void get_tf_states(struct expression *expr,
846 struct stree **implied_true,
847 struct stree **implied_false)
849 if (handled_by_comparison_hook(expr, implied_true, implied_false))
850 goto found;
852 if (handled_by_extra_states(expr, implied_true, implied_false)) {
853 separate_extra_states(implied_true, implied_false);
854 goto found;
857 if (handled_by_stored_conditions(expr, implied_true, implied_false))
858 goto found;
860 return;
861 found:
862 found_implications = 1;
865 static void save_implications_hook(struct expression *expr)
867 if (taking_too_long())
868 return;
869 get_tf_states(expr, &saved_implied_true, &saved_implied_false);
872 static void set_implied_states(struct expression *expr)
874 struct sm_state *sm;
876 FOR_EACH_SM(saved_implied_true, sm) {
877 __set_true_false_sm(sm, NULL);
878 } END_FOR_EACH_SM(sm);
879 free_stree(&saved_implied_true);
881 FOR_EACH_SM(saved_implied_false, sm) {
882 __set_true_false_sm(NULL, sm);
883 } END_FOR_EACH_SM(sm);
884 free_stree(&saved_implied_false);
887 static void set_extra_implied_states(struct expression *expr)
889 saved_implied_true = extra_saved_implied_true;
890 saved_implied_false = extra_saved_implied_false;
891 extra_saved_implied_true = NULL;
892 extra_saved_implied_false = NULL;
893 set_implied_states(NULL);
896 void param_limit_implications(struct expression *expr, int param, char *key, char *value)
898 struct expression *arg;
899 struct symbol *compare_type;
900 char *name;
901 struct symbol *sym;
902 struct sm_state *sm;
903 struct sm_state *tmp;
904 struct stree *implied_true = NULL;
905 struct stree *implied_false = NULL;
906 struct range_list *orig, *limit;
908 while (expr->type == EXPR_ASSIGNMENT)
909 expr = strip_expr(expr->right);
910 if (expr->type != EXPR_CALL)
911 return;
913 arg = get_argument_from_call_expr(expr->args, param);
914 if (!arg)
915 return;
917 arg = strip_parens(arg);
918 while (arg->type == EXPR_ASSIGNMENT && arg->op == '=')
919 arg = strip_parens(arg->left);
921 name = get_variable_from_key(arg, key, &sym);
922 if (!name || !sym)
923 goto free;
925 sm = get_sm_state(SMATCH_EXTRA, name, sym);
926 if (!sm || !sm->merged)
927 goto free;
929 if (strcmp(key, "$") == 0)
930 compare_type = get_arg_type(expr->fn, param);
931 else
932 compare_type = get_member_type_from_key(arg, key);
934 orig = estate_rl(sm->state);
935 orig = cast_rl(compare_type, orig);
937 call_results_to_rl(expr, compare_type, value, &limit);
939 separate_and_filter(sm, SPECIAL_EQUAL, limit, __get_cur_stree(), &implied_true, &implied_false, NULL);
941 FOR_EACH_SM(implied_true, tmp) {
942 __set_sm_fake_stree(tmp);
943 } END_FOR_EACH_SM(tmp);
945 free_stree(&implied_true);
946 free_stree(&implied_false);
947 free:
948 free_string(name);
951 struct stree *__implied_case_stree(struct expression *switch_expr,
952 struct range_list *rl,
953 struct range_list_stack **remaining_cases,
954 struct stree **raw_stree)
956 char *name;
957 struct symbol *sym;
958 struct var_sym_list *vsl;
959 struct sm_state *sm;
960 struct stree *true_states = NULL;
961 struct stree *false_states = NULL;
962 struct stree *extra_states;
963 struct stree *ret = clone_stree(*raw_stree);
965 name = expr_to_chunk_sym_vsl(switch_expr, &sym, &vsl);
967 if (rl)
968 filter_top_rl(remaining_cases, rl);
969 else
970 rl = clone_rl(top_rl(*remaining_cases));
972 if (name) {
973 sm = get_sm_state_stree(*raw_stree, SMATCH_EXTRA, name, sym);
974 if (sm)
975 separate_and_filter(sm, SPECIAL_EQUAL, rl, *raw_stree, &true_states, &false_states, NULL);
978 __push_fake_cur_stree();
979 __unnullify_path();
980 if (name)
981 set_extra_nomod_vsl(name, sym, vsl, NULL, alloc_estate_rl(rl));
982 __pass_case_to_client(switch_expr, rl);
983 extra_states = __pop_fake_cur_stree();
984 overwrite_stree(extra_states, &true_states);
985 overwrite_stree(true_states, &ret);
986 free_stree(&extra_states);
987 free_stree(&true_states);
988 free_stree(&false_states);
990 free_string(name);
991 return ret;
994 static void match_end_func(struct symbol *sym)
996 if (__inline_fn)
997 return;
998 implied_debug_msg = NULL;
1001 static void get_tf_stacks_from_pool(struct sm_state *gate_sm,
1002 struct sm_state *pool_sm,
1003 struct state_list **true_stack,
1004 struct state_list **false_stack)
1006 struct sm_state *tmp;
1007 int possibly_true = 0;
1009 if (!gate_sm)
1010 return;
1012 if (strcmp(gate_sm->state->name, pool_sm->state->name) == 0) {
1013 add_ptr_list(true_stack, pool_sm);
1014 return;
1017 FOR_EACH_PTR(gate_sm->possible, tmp) {
1018 if (strcmp(tmp->state->name, pool_sm->state->name) == 0) {
1019 possibly_true = 1;
1020 break;
1022 } END_FOR_EACH_PTR(tmp);
1024 if (!possibly_true) {
1025 add_ptr_list(false_stack, gate_sm);
1026 return;
1029 get_tf_stacks_from_pool(gate_sm->left, pool_sm, true_stack, false_stack);
1030 get_tf_stacks_from_pool(gate_sm->right, pool_sm, true_stack, false_stack);
1034 * The situation is we have a SMATCH_EXTRA state and we want to break it into
1035 * each of the ->possible states and find the implications of each. The caller
1036 * has to use __push_fake_cur_stree() to preserve the correct states so they
1037 * can be restored later.
1039 void overwrite_states_using_pool(struct sm_state *gate_sm, struct sm_state *pool_sm)
1041 struct state_list *true_stack = NULL;
1042 struct state_list *false_stack = NULL;
1043 struct stree *pre_stree;
1044 struct stree *implied_true;
1045 struct sm_state *tmp;
1047 if (!pool_sm->pool)
1048 return;
1050 get_tf_stacks_from_pool(gate_sm, pool_sm, &true_stack, &false_stack);
1052 pre_stree = clone_stree(__get_cur_stree());
1054 implied_true = filter_stack(gate_sm, pre_stree, false_stack, true_stack);
1056 free_stree(&pre_stree);
1057 free_slist(&true_stack);
1058 free_slist(&false_stack);
1060 FOR_EACH_SM(implied_true, tmp) {
1061 set_state(tmp->owner, tmp->name, tmp->sym, tmp->state);
1062 } END_FOR_EACH_SM(tmp);
1064 free_stree(&implied_true);
1067 int assume(struct expression *expr)
1069 int orig_final_pass = final_pass;
1071 in_fake_env++;
1072 final_pass = 0;
1073 __push_fake_cur_stree();
1074 found_implications = 0;
1075 __split_whole_condition(expr);
1076 final_pass = orig_final_pass;
1077 in_fake_env--;
1079 return 1;
1082 void end_assume(void)
1084 __discard_false_states();
1085 __free_fake_cur_stree();
1088 int impossible_assumption(struct expression *left, int op, sval_t sval)
1090 struct expression *value;
1091 struct expression *comparison;
1092 int ret;
1094 value = value_expr(sval.value);
1095 comparison = compare_expression(left, op, value);
1097 if (!assume(comparison))
1098 return 0;
1099 ret = is_impossible_path();
1100 end_assume();
1102 return ret;
1105 void __extra_match_condition(struct expression *expr);
1106 void __comparison_match_condition(struct expression *expr);
1107 void __stored_condition(struct expression *expr);
1108 void register_implications(int id)
1110 add_hook(&save_implications_hook, CONDITION_HOOK);
1111 add_hook(&set_implied_states, CONDITION_HOOK);
1112 add_hook(&__extra_match_condition, CONDITION_HOOK);
1113 add_hook(&set_extra_implied_states, CONDITION_HOOK);
1114 add_hook(&__comparison_match_condition, CONDITION_HOOK);
1115 add_hook(&__stored_condition, CONDITION_HOOK);
1116 add_hook(&match_end_func, END_FUNC_HOOK);