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:
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
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
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.
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;
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
);
86 static void print_debug_tf(struct sm_state
*sm
, int istrue
, int isfalse
)
88 if (!option_debug_implied
&& !option_debug
)
91 if (istrue
&& isfalse
) {
92 printf("%s: %d: does not exist.\n", show_sm(sm
), sm
->line
);
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
));
98 printf("'%s = %s' from %d is false. %s[stree %d]\n", sm
->name
, show_state(sm
->state
),
100 sm
->merged
? "[merged]" : "[leaf]",
101 get_stree_id(sm
->pool
));
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
;
118 if (is_merged(sm
) || sm
->left
|| sm
->right
)
120 if (!rl_to_sval(rl
, &sval
))
122 if (!estate_rl(sm
->state
))
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
))
136 if (rl_intersection(true_rl
, false_rl
)) {
137 sm_perror("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
)));
145 sm_info("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
= clone_partial_estate(sm
->state
, true_rl
);
153 free_slist(&true_sm
->possible
);
154 add_possible_sm(true_sm
, true_sm
);
155 false_sm
->state
= clone_partial_estate(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
;
170 sm
->right
= false_sm
;
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
)
186 else if (tmp
->pool
== new->pool
) {
189 INSERT_CURRENT(new, tmp
);
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
) {
204 if (tmp
->pool
== pool
)
206 } END_FOR_EACH_PTR(tmp
);
210 static int remove_pool(struct state_list
**pools
, struct stree
*remove
)
212 struct sm_state
*tmp
;
215 FOR_EACH_PTR(*pools
, tmp
) {
216 if (tmp
->pool
== remove
) {
217 DELETE_CURRENT_PTR(tmp
);
220 } END_FOR_EACH_PTR(tmp
);
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
)
237 struct range_list
*var_rl
;
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) {
256 if (mixed
&& !*mixed
&& !is_merged(sm
) && !istrue
&& !isfalse
) {
257 if (!create_fake_history(sm
, comparison
, rl
))
262 add_pool(true_stack
, sm
);
264 add_pool(false_stack
, sm
);
266 add_pool(maybe_stack
, sm
);
270 static int is_checked(struct state_list
*checked
, struct sm_state
*sm
)
272 struct sm_state
*tmp
;
274 FOR_EACH_PTR(checked
, tmp
) {
277 } END_FOR_EACH_PTR(tmp
);
283 * Example code: if (foo == 99) {
285 * Say 'foo' is a merged state that has many possible values. It is the combination
286 * of merges. separate_pools() iterates through the pools recursively and calls
287 * do_compare() for each time 'foo' was set.
289 static void __separate_pools(struct sm_state
*sm
, int comparison
, struct range_list
*rl
,
290 struct state_list
**true_stack
,
291 struct state_list
**maybe_stack
,
292 struct state_list
**false_stack
,
293 struct state_list
**checked
, int *mixed
, struct sm_state
*gate_sm
)
295 int free_checked
= 0;
296 struct state_list
*checked_states
= NULL
;
302 * If it looks like this is going to take too long as-is, then don't
303 * create even more fake history.
305 if (mixed
&& sm
->nr_children
> 100)
309 Sometimes the implications are just too big to deal with
310 so we bail. Theoretically, bailing out here can cause more false
311 positives but won't hide actual bugs.
313 if (sm
->nr_children
> 4000) {
314 if (option_debug
|| option_debug_implied
) {
315 static char buf
[1028];
316 snprintf(buf
, sizeof(buf
), "debug: %s: nr_children over 4000 (%d). (%s %s)",
317 __func__
, sm
->nr_children
, sm
->name
, show_state(sm
->state
));
318 implied_debug_msg
= buf
;
323 if (checked
== NULL
) {
324 checked
= &checked_states
;
327 if (is_checked(*checked
, sm
))
329 add_ptr_list(checked
, sm
);
331 do_compare(sm
, comparison
, rl
, true_stack
, maybe_stack
, false_stack
, mixed
, gate_sm
);
333 __separate_pools(sm
->left
, comparison
, rl
, true_stack
, maybe_stack
, false_stack
, checked
, mixed
, gate_sm
);
334 __separate_pools(sm
->right
, comparison
, rl
, true_stack
, maybe_stack
, false_stack
, checked
, mixed
, gate_sm
);
339 static void separate_pools(struct sm_state
*sm
, int comparison
, struct range_list
*rl
,
340 struct state_list
**true_stack
,
341 struct state_list
**false_stack
,
342 struct state_list
**checked
, int *mixed
)
344 struct state_list
*maybe_stack
= NULL
;
345 struct sm_state
*tmp
;
347 __separate_pools(sm
, comparison
, rl
, true_stack
, &maybe_stack
, false_stack
, checked
, mixed
, sm
);
352 FOR_EACH_PTR(*true_stack
, sm
) {
353 sm_msg("TRUE %s [stree %d]", show_sm(sm
), get_stree_id(sm
->pool
));
354 } END_FOR_EACH_PTR(sm
);
356 FOR_EACH_PTR(maybe_stack
, sm
) {
357 sm_msg("MAYBE %s [stree %d]", show_sm(sm
), get_stree_id(sm
->pool
));
358 } END_FOR_EACH_PTR(sm
);
360 FOR_EACH_PTR(*false_stack
, sm
) {
361 sm_msg("FALSE %s [stree %d]", show_sm(sm
), get_stree_id(sm
->pool
));
362 } END_FOR_EACH_PTR(sm
);
364 /* if it's a maybe then remove it */
365 FOR_EACH_PTR(maybe_stack
, tmp
) {
366 remove_pool(false_stack
, tmp
->pool
);
367 remove_pool(true_stack
, tmp
->pool
);
368 } END_FOR_EACH_PTR(tmp
);
370 /* if it's both true and false remove it from both */
371 FOR_EACH_PTR(*true_stack
, tmp
) {
372 if (remove_pool(false_stack
, tmp
->pool
))
373 DELETE_CURRENT_PTR(tmp
);
374 } END_FOR_EACH_PTR(tmp
);
377 static int sm_in_keep_leafs(struct sm_state
*sm
, const struct state_list
*keep_gates
)
379 struct sm_state
*tmp
, *old
;
381 FOR_EACH_PTR(keep_gates
, tmp
) {
384 old
= get_sm_state_stree(tmp
->pool
, sm
->owner
, sm
->name
, sm
->sym
);
389 } END_FOR_EACH_PTR(tmp
);
393 static int taking_too_long(void)
395 static void *printed
;
400 if (time_parsing_function() < 60)
403 if (!__inline_fn
&& printed
!= cur_func_sym
) {
404 sm_perror("turning off implications after 60 seconds");
405 printed
= cur_func_sym
;
411 * NOTE: If a state is in both the keep stack and the remove stack then that is
412 * a bug. Only add states which are definitely true or definitely false. If
413 * you have a leaf state that could be both true and false, then create a fake
414 * split history where one side is true and one side is false. Otherwise, if
415 * you can't do that, then don't add it to either list.
417 struct sm_state
*filter_pools(struct sm_state
*sm
,
418 const struct state_list
*remove_stack
,
419 const struct state_list
*keep_stack
,
420 int *modified
, int *recurse_cnt
,
421 struct timeval
*start
)
423 struct sm_state
*ret
= NULL
;
424 struct sm_state
*left
;
425 struct sm_state
*right
;
431 if (sm
->skip_implications
)
433 if (taking_too_long())
436 gettimeofday(&now
, NULL
);
437 if ((*recurse_cnt
)++ > 1000 || now
.tv_sec
- start
->tv_sec
> 5) {
438 if (local_debug
|| option_debug_implied
) {
439 static char buf
[1028];
440 snprintf(buf
, sizeof(buf
), "debug: %s: nr_children over 4000 (%d). (%s %s)",
441 __func__
, sm
->nr_children
, sm
->name
, show_state(sm
->state
));
442 implied_debug_msg
= buf
;
444 sm
->skip_implications
= 1;
448 if (pool_in_pools(sm
->pool
, remove_stack
)) {
449 DIMPLIED("removed [stree %d] %s from %d\n", get_stree_id(sm
->pool
), show_sm(sm
), sm
->line
);
454 if (!is_merged(sm
) || pool_in_pools(sm
->pool
, keep_stack
) || sm_in_keep_leafs(sm
, keep_stack
)) {
455 DIMPLIED("kept [stree %d] %s from %d. %s. %s. %s.\n", get_stree_id(sm
->pool
), show_sm(sm
), sm
->line
,
456 is_merged(sm
) ? "merged" : "not merged",
457 pool_in_pools(sm
->pool
, keep_stack
) ? "not in keep pools" : "in keep pools",
458 sm_in_keep_leafs(sm
, keep_stack
) ? "reachable keep leaf" : "no keep leaf");
462 DIMPLIED("checking [stree %d] %s from %d (%d) left = %s [stree %d] right = %s [stree %d]\n",
463 get_stree_id(sm
->pool
),
464 show_sm(sm
), sm
->line
, sm
->nr_children
,
465 sm
->left
? sm
->left
->state
->name
: "<none>", sm
->left
? get_stree_id(sm
->left
->pool
) : -1,
466 sm
->right
? sm
->right
->state
->name
: "<none>", sm
->right
? get_stree_id(sm
->right
->pool
) : -1);
467 left
= filter_pools(sm
->left
, remove_stack
, keep_stack
, &removed
, recurse_cnt
, start
);
468 right
= filter_pools(sm
->right
, remove_stack
, keep_stack
, &removed
, recurse_cnt
, start
);
470 DIMPLIED("kept [stree %d] %s from %d\n", get_stree_id(sm
->pool
), show_sm(sm
), sm
->line
);
474 if (!left
&& !right
) {
475 DIMPLIED("removed [stree %d] %s from %d <none>\n", get_stree_id(sm
->pool
), show_sm(sm
), sm
->line
);
480 ret
= clone_sm(right
);
485 ret
= clone_sm(left
);
490 if (left
->sym
!= sm
->sym
|| strcmp(left
->name
, sm
->name
) != 0) {
491 left
= clone_sm(left
);
493 left
->name
= sm
->name
;
495 if (right
->sym
!= sm
->sym
|| strcmp(right
->name
, sm
->name
) != 0) {
496 right
= clone_sm(right
);
497 right
->sym
= sm
->sym
;
498 right
->name
= sm
->name
;
500 ret
= merge_sm_states(left
, right
);
503 ret
->pool
= sm
->pool
;
505 DIMPLIED("partial %s => ", show_sm(sm
));
506 DIMPLIED("%s from %d [stree %d]\n", show_sm(ret
), sm
->line
, get_stree_id(sm
->pool
));
510 static struct stree
*filter_stack(struct sm_state
*gate_sm
,
511 struct stree
*pre_stree
,
512 const struct state_list
*remove_stack
,
513 const struct state_list
*keep_stack
)
515 struct stree
*ret
= NULL
;
516 struct sm_state
*tmp
;
517 struct sm_state
*filtered_sm
;
520 struct timeval start
;
525 if (taking_too_long())
528 FOR_EACH_SM(pre_stree
, tmp
) {
530 sm_msg("%s: %s", __func__
, show_sm(tmp
));
533 if (sm_in_keep_leafs(tmp
, keep_stack
))
537 gettimeofday(&start
, NULL
);
538 filtered_sm
= filter_pools(tmp
, remove_stack
, keep_stack
, &modified
, &recurse_cnt
, &start
);
539 if (!filtered_sm
|| !modified
)
541 /* the assignments here are for borrowed implications */
542 filtered_sm
->name
= tmp
->name
;
543 filtered_sm
->sym
= tmp
->sym
;
544 avl_insert(&ret
, filtered_sm
);
545 if (out_of_memory() || taking_too_long())
548 } END_FOR_EACH_SM(tmp
);
552 static void separate_and_filter(struct sm_state
*sm
, int comparison
, struct range_list
*rl
,
553 struct stree
*pre_stree
,
554 struct stree
**true_states
,
555 struct stree
**false_states
,
558 struct state_list
*true_stack
= NULL
;
559 struct state_list
*false_stack
= NULL
;
560 struct timeval time_before
;
561 struct timeval time_after
;
564 gettimeofday(&time_before
, NULL
);
566 DIMPLIED("checking implications: (%s (%s) %s %s)\n",
567 sm
->name
, sm
->state
->name
, show_special(comparison
), show_rl(rl
));
569 if (!is_merged(sm
)) {
570 DIMPLIED("%d '%s' from line %d is not merged.\n", get_lineno(), sm
->name
, sm
->line
);
574 separate_pools(sm
, comparison
, rl
, &true_stack
, &false_stack
, NULL
, mixed
);
576 DIMPLIED("filtering true stack.\n");
577 *true_states
= filter_stack(sm
, pre_stree
, false_stack
, true_stack
);
578 DIMPLIED("filtering false stack.\n");
579 *false_states
= filter_stack(sm
, pre_stree
, true_stack
, false_stack
);
580 free_slist(&true_stack
);
581 free_slist(&false_stack
);
582 if (option_debug_implied
|| option_debug
) {
583 printf("These are the implied states for the true path: (%s %s %s)\n",
584 sm
->name
, show_special(comparison
), show_rl(rl
));
585 __print_stree(*true_states
);
586 printf("These are the implied states for the false path: (%s %s %s)\n",
587 sm
->name
, show_special(comparison
), show_rl(rl
));
588 __print_stree(*false_states
);
591 gettimeofday(&time_after
, NULL
);
592 sec
= time_after
.tv_sec
- time_before
.tv_sec
;
594 sm
->nr_children
= 4000;
595 sm_perror("Function too hairy. Ignoring implications after %d seconds.", sec
);
599 static struct expression
*get_last_expr(struct statement
*stmt
)
601 struct statement
*last
;
603 last
= last_ptr_list((struct ptr_list
*)stmt
->stmts
);
604 if (last
->type
== STMT_EXPRESSION
)
605 return last
->expression
;
607 if (last
->type
== STMT_LABEL
) {
608 if (last
->label_statement
&&
609 last
->label_statement
->type
== STMT_EXPRESSION
)
610 return last
->label_statement
->expression
;
616 static struct expression
*get_left_most_expr(struct expression
*expr
)
618 struct statement
*compound
;
620 compound
= get_expression_statement(expr
);
622 return get_last_expr(compound
);
624 expr
= strip_parens(expr
);
625 if (expr
->type
== EXPR_ASSIGNMENT
)
626 return get_left_most_expr(expr
->left
);
630 static int is_merged_expr(struct expression
*expr
)
635 if (get_value(expr
, &dummy
))
637 sm
= get_sm_state_expr(SMATCH_EXTRA
, expr
);
645 static void delete_gate_sm_equiv(struct stree
**stree
, const char *name
, struct symbol
*sym
)
647 struct smatch_state
*state
;
648 struct relation
*rel
;
650 state
= get_state(SMATCH_EXTRA
, name
, sym
);
653 FOR_EACH_PTR(estate_related(state
), rel
) {
654 delete_state_stree(stree
, SMATCH_EXTRA
, rel
->name
, rel
->sym
);
655 } END_FOR_EACH_PTR(rel
);
658 static void delete_gate_sm(struct stree
**stree
, const char *name
, struct symbol
*sym
)
660 delete_state_stree(stree
, SMATCH_EXTRA
, name
, sym
);
663 static int handle_comparison(struct expression
*expr
,
664 struct stree
**implied_true
,
665 struct stree
**implied_false
)
667 struct sm_state
*sm
= NULL
;
668 struct range_list
*rl
= NULL
;
669 struct expression
*left
;
670 struct expression
*right
;
672 int comparison
= expr
->op
;
675 left
= get_left_most_expr(expr
->left
);
676 right
= get_left_most_expr(expr
->right
);
678 if (is_merged_expr(left
)) {
679 sm
= get_sm_state_expr(SMATCH_EXTRA
, left
);
680 get_implied_rl(right
, &rl
);
681 } else if (is_merged_expr(right
)) {
682 sm
= get_sm_state_expr(SMATCH_EXTRA
, right
);
683 get_implied_rl(left
, &rl
);
684 comparison
= flip_comparison(comparison
);
690 type
= get_type(expr
);
693 if (type_positive_bits(rl_type(rl
)) > type_positive_bits(type
))
695 if (type_positive_bits(type
) < 31)
697 rl
= cast_rl(type
, rl
);
699 separate_and_filter(sm
, comparison
, rl
, __get_cur_stree(), implied_true
, implied_false
, &mixed
);
701 delete_gate_sm_equiv(implied_true
, sm
->name
, sm
->sym
);
702 delete_gate_sm_equiv(implied_false
, sm
->name
, sm
->sym
);
704 delete_gate_sm(implied_true
, sm
->name
, sm
->sym
);
705 delete_gate_sm(implied_false
, sm
->name
, sm
->sym
);
711 static int handle_zero_comparison(struct expression
*expr
,
712 struct stree
**implied_true
,
713 struct stree
**implied_false
)
721 if (expr
->type
== EXPR_POSTOP
)
722 expr
= strip_expr(expr
->unop
);
724 if (expr
->type
== EXPR_ASSIGNMENT
) {
725 /* most of the time ->pools will be empty here because we
726 just set the state, but if have assigned a conditional
727 function there are implications. */
731 name
= expr_to_var_sym(expr
, &sym
);
734 sm
= get_sm_state(SMATCH_EXTRA
, name
, sym
);
738 separate_and_filter(sm
, SPECIAL_NOTEQUAL
, tmp_range_list(estate_type(sm
->state
), 0), __get_cur_stree(), implied_true
, implied_false
, &mixed
);
739 delete_gate_sm_equiv(implied_true
, sm
->name
, sm
->sym
);
740 delete_gate_sm_equiv(implied_false
, sm
->name
, sm
->sym
);
742 delete_gate_sm(implied_true
, sm
->name
, sm
->sym
);
743 delete_gate_sm(implied_false
, sm
->name
, sm
->sym
);
752 static int handled_by_comparison_hook(struct expression
*expr
,
753 struct stree
**implied_true
,
754 struct stree
**implied_false
)
756 struct state_list
*true_stack
= NULL
;
757 struct state_list
*false_stack
= NULL
;
758 struct stree
*pre_stree
;
761 sm
= comparison_implication_hook(expr
, &true_stack
, &false_stack
);
765 pre_stree
= clone_stree(__get_cur_stree());
767 *implied_true
= filter_stack(sm
, pre_stree
, false_stack
, true_stack
);
768 *implied_false
= filter_stack(sm
, pre_stree
, true_stack
, false_stack
);
770 free_stree(&pre_stree
);
771 free_slist(&true_stack
);
772 free_slist(&false_stack
);
777 static int handled_by_extra_states(struct expression
*expr
,
778 struct stree
**implied_true
,
779 struct stree
**implied_false
)
781 if (expr
->type
== EXPR_COMPARE
)
782 return handle_comparison(expr
, implied_true
, implied_false
);
784 return handle_zero_comparison(expr
, implied_true
, implied_false
);
787 static int handled_by_stored_conditions(struct expression
*expr
,
788 struct stree
**implied_true
,
789 struct stree
**implied_false
)
791 struct state_list
*true_stack
= NULL
;
792 struct state_list
*false_stack
= NULL
;
793 struct stree
*pre_stree
;
796 sm
= stored_condition_implication_hook(expr
, &true_stack
, &false_stack
);
800 pre_stree
= clone_stree(__get_cur_stree());
802 *implied_true
= filter_stack(sm
, pre_stree
, false_stack
, true_stack
);
803 *implied_false
= filter_stack(sm
, pre_stree
, true_stack
, false_stack
);
805 free_stree(&pre_stree
);
806 free_slist(&true_stack
);
807 free_slist(&false_stack
);
812 static int found_implications
;
813 static struct stree
*saved_implied_true
;
814 static struct stree
*saved_implied_false
;
815 static struct stree
*extra_saved_implied_true
;
816 static struct stree
*extra_saved_implied_false
;
818 static void separate_extra_states(struct stree
**implied_true
,
819 struct stree
**implied_false
)
823 /* We process extra states later to preserve the implications. */
824 FOR_EACH_SM(*implied_true
, sm
) {
825 if (sm
->owner
== SMATCH_EXTRA
)
826 overwrite_sm_state_stree(&extra_saved_implied_true
, sm
);
827 } END_FOR_EACH_SM(sm
);
828 FOR_EACH_SM(extra_saved_implied_true
, sm
) {
829 delete_state_stree(implied_true
, sm
->owner
, sm
->name
, sm
->sym
);
830 } END_FOR_EACH_SM(sm
);
832 FOR_EACH_SM(*implied_false
, sm
) {
833 if (sm
->owner
== SMATCH_EXTRA
)
834 overwrite_sm_state_stree(&extra_saved_implied_false
, sm
);
835 } END_FOR_EACH_SM(sm
);
836 FOR_EACH_SM(extra_saved_implied_false
, sm
) {
837 delete_state_stree(implied_false
, sm
->owner
, sm
->name
, sm
->sym
);
838 } END_FOR_EACH_SM(sm
);
841 static void get_tf_states(struct expression
*expr
,
842 struct stree
**implied_true
,
843 struct stree
**implied_false
)
845 if (handled_by_comparison_hook(expr
, implied_true
, implied_false
))
848 if (handled_by_extra_states(expr
, implied_true
, implied_false
)) {
849 separate_extra_states(implied_true
, implied_false
);
853 if (handled_by_stored_conditions(expr
, implied_true
, implied_false
))
858 found_implications
= 1;
861 static void save_implications_hook(struct expression
*expr
)
863 if (taking_too_long())
865 get_tf_states(expr
, &saved_implied_true
, &saved_implied_false
);
868 static void set_implied_states(struct expression
*expr
)
872 FOR_EACH_SM(saved_implied_true
, sm
) {
873 __set_true_false_sm(sm
, NULL
);
874 } END_FOR_EACH_SM(sm
);
875 free_stree(&saved_implied_true
);
877 FOR_EACH_SM(saved_implied_false
, sm
) {
878 __set_true_false_sm(NULL
, sm
);
879 } END_FOR_EACH_SM(sm
);
880 free_stree(&saved_implied_false
);
883 static void set_extra_implied_states(struct expression
*expr
)
885 saved_implied_true
= extra_saved_implied_true
;
886 saved_implied_false
= extra_saved_implied_false
;
887 extra_saved_implied_true
= NULL
;
888 extra_saved_implied_false
= NULL
;
889 set_implied_states(NULL
);
892 void param_limit_implications(struct expression
*expr
, int param
, char *key
, char *value
)
894 struct expression
*arg
;
895 struct symbol
*compare_type
;
899 struct sm_state
*tmp
;
900 struct stree
*implied_true
= NULL
;
901 struct stree
*implied_false
= NULL
;
902 struct range_list
*orig
, *limit
;
904 while (expr
->type
== EXPR_ASSIGNMENT
)
905 expr
= strip_expr(expr
->right
);
906 if (expr
->type
!= EXPR_CALL
)
909 arg
= get_argument_from_call_expr(expr
->args
, param
);
913 arg
= strip_parens(arg
);
914 while (arg
->type
== EXPR_ASSIGNMENT
&& arg
->op
== '=')
915 arg
= strip_parens(arg
->left
);
917 name
= get_variable_from_key(arg
, key
, &sym
);
921 sm
= get_sm_state(SMATCH_EXTRA
, name
, sym
);
922 if (!sm
|| !sm
->merged
)
925 if (strcmp(key
, "$") == 0)
926 compare_type
= get_arg_type(expr
->fn
, param
);
928 compare_type
= get_member_type_from_key(arg
, key
);
930 orig
= estate_rl(sm
->state
);
931 orig
= cast_rl(compare_type
, orig
);
933 call_results_to_rl(expr
, compare_type
, value
, &limit
);
935 separate_and_filter(sm
, SPECIAL_EQUAL
, limit
, __get_cur_stree(), &implied_true
, &implied_false
, NULL
);
937 FOR_EACH_SM(implied_true
, tmp
) {
938 __set_sm_fake_stree(tmp
);
939 } END_FOR_EACH_SM(tmp
);
941 free_stree(&implied_true
);
942 free_stree(&implied_false
);
947 struct stree
*__implied_case_stree(struct expression
*switch_expr
,
948 struct range_list
*rl
,
949 struct range_list_stack
**remaining_cases
,
950 struct stree
**raw_stree
)
954 struct var_sym_list
*vsl
;
956 struct stree
*true_states
= NULL
;
957 struct stree
*false_states
= NULL
;
958 struct stree
*extra_states
;
959 struct stree
*ret
= clone_stree(*raw_stree
);
961 name
= expr_to_chunk_sym_vsl(switch_expr
, &sym
, &vsl
);
964 filter_top_rl(remaining_cases
, rl
);
966 rl
= clone_rl(top_rl(*remaining_cases
));
969 sm
= get_sm_state_stree(*raw_stree
, SMATCH_EXTRA
, name
, sym
);
971 separate_and_filter(sm
, SPECIAL_EQUAL
, rl
, *raw_stree
, &true_states
, &false_states
, NULL
);
974 __push_fake_cur_stree();
977 set_extra_nomod_vsl(name
, sym
, vsl
, NULL
, alloc_estate_rl(rl
));
978 __pass_case_to_client(switch_expr
, rl
);
979 extra_states
= __pop_fake_cur_stree();
980 overwrite_stree(extra_states
, &true_states
);
981 overwrite_stree(true_states
, &ret
);
982 free_stree(&extra_states
);
983 free_stree(&true_states
);
984 free_stree(&false_states
);
990 static void match_end_func(struct symbol
*sym
)
994 implied_debug_msg
= NULL
;
997 static void get_tf_stacks_from_pool(struct sm_state
*gate_sm
,
998 struct sm_state
*pool_sm
,
999 struct state_list
**true_stack
,
1000 struct state_list
**false_stack
)
1002 struct sm_state
*tmp
;
1003 int possibly_true
= 0;
1008 if (strcmp(gate_sm
->state
->name
, pool_sm
->state
->name
) == 0) {
1009 add_ptr_list(true_stack
, pool_sm
);
1013 FOR_EACH_PTR(gate_sm
->possible
, tmp
) {
1014 if (strcmp(tmp
->state
->name
, pool_sm
->state
->name
) == 0) {
1018 } END_FOR_EACH_PTR(tmp
);
1020 if (!possibly_true
) {
1021 add_ptr_list(false_stack
, gate_sm
);
1025 get_tf_stacks_from_pool(gate_sm
->left
, pool_sm
, true_stack
, false_stack
);
1026 get_tf_stacks_from_pool(gate_sm
->right
, pool_sm
, true_stack
, false_stack
);
1030 * The situation is we have a SMATCH_EXTRA state and we want to break it into
1031 * each of the ->possible states and find the implications of each. The caller
1032 * has to use __push_fake_cur_stree() to preserve the correct states so they
1033 * can be restored later.
1035 void overwrite_states_using_pool(struct sm_state
*gate_sm
, struct sm_state
*pool_sm
)
1037 struct state_list
*true_stack
= NULL
;
1038 struct state_list
*false_stack
= NULL
;
1039 struct stree
*pre_stree
;
1040 struct stree
*implied_true
;
1041 struct sm_state
*tmp
;
1046 get_tf_stacks_from_pool(gate_sm
, pool_sm
, &true_stack
, &false_stack
);
1048 pre_stree
= clone_stree(__get_cur_stree());
1050 implied_true
= filter_stack(gate_sm
, pre_stree
, false_stack
, true_stack
);
1052 free_stree(&pre_stree
);
1053 free_slist(&true_stack
);
1054 free_slist(&false_stack
);
1056 FOR_EACH_SM(implied_true
, tmp
) {
1057 set_state(tmp
->owner
, tmp
->name
, tmp
->sym
, tmp
->state
);
1058 } END_FOR_EACH_SM(tmp
);
1060 free_stree(&implied_true
);
1063 int assume(struct expression
*expr
)
1065 int orig_final_pass
= final_pass
;
1069 __push_fake_cur_stree();
1070 found_implications
= 0;
1071 __split_whole_condition(expr
);
1072 final_pass
= orig_final_pass
;
1078 void end_assume(void)
1080 __discard_false_states();
1081 __free_fake_cur_stree();
1084 int impossible_assumption(struct expression
*left
, int op
, sval_t sval
)
1086 struct expression
*value
;
1087 struct expression
*comparison
;
1090 value
= value_expr(sval
.value
);
1091 comparison
= compare_expression(left
, op
, value
);
1093 if (!assume(comparison
))
1095 ret
= is_impossible_path();
1101 void __extra_match_condition(struct expression
*expr
);
1102 void __comparison_match_condition(struct expression
*expr
);
1103 void __stored_condition(struct expression
*expr
);
1104 void register_implications(int id
)
1106 add_hook(&save_implications_hook
, CONDITION_HOOK
);
1107 add_hook(&set_implied_states
, CONDITION_HOOK
);
1108 add_hook(&__extra_match_condition
, CONDITION_HOOK
);
1109 add_hook(&set_extra_implied_states
, CONDITION_HOOK
);
1110 add_hook(&__comparison_match_condition
, CONDITION_HOOK
);
1111 add_hook(&__stored_condition
, CONDITION_HOOK
);
1112 add_hook(&match_end_func
, END_FUNC_HOOK
);