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) 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 = %s' from %d does not exist.\n", sm
->name
,
93 show_state(sm
->state
), sm
->line
);
95 printf("'%s = %s' from %d is true. [stree %d]\n", sm
->name
, show_state(sm
->state
),
96 sm
->line
, get_stree_id(sm
->pool
));
98 printf("'%s = %s' from %d is false. [stree %d]\n", sm
->name
, show_state(sm
->state
),
99 sm
->line
, get_stree_id(sm
->pool
));
101 printf("'%s = %s' from %d could be true or false. [stree %d]\n", sm
->name
,
102 show_state(sm
->state
), sm
->line
, get_stree_id(sm
->pool
));
107 * add_pool() adds a slist to *pools. If the slist has already been
108 * added earlier then it doesn't get added a second time.
110 void add_pool(struct stree_stack
**pools
, struct stree
*new)
114 FOR_EACH_PTR(*pools
, tmp
) {
117 else if (tmp
== new) {
120 INSERT_CURRENT(new, tmp
);
123 } END_FOR_EACH_PTR(tmp
);
124 add_ptr_list(pools
, new);
128 * If 'foo' == 99 add it that pool to the true pools. If it's false, add it to
129 * the false pools. If we're not sure, then we don't add it to either.
131 static void do_compare(struct sm_state
*sm
, int comparison
, struct range_list
*rl
,
132 struct stree_stack
**true_stack
,
133 struct stree_stack
**false_stack
)
138 struct range_list
*var_rl
;
143 if (is_implied(sm
)) {
144 s
= get_sm_state_stree(sm
->pool
,
152 if (option_debug_implied
|| option_debug
)
153 sm_msg("%s from %d, has borrowed implications.",
158 var_rl
= cast_rl(rl_type(rl
), estate_rl(s
->state
));
160 istrue
= !possibly_false_rl(var_rl
, comparison
, rl
);
161 isfalse
= !possibly_true_rl(var_rl
, comparison
, rl
);
163 print_debug_tf(s
, istrue
, isfalse
);
166 add_pool(true_stack
, s
->pool
);
169 add_pool(false_stack
, s
->pool
);
172 static int pool_in_pools(struct stree
*pool
,
173 const struct stree_stack
*pools
)
177 FOR_EACH_PTR(pools
, tmp
) {
182 } END_FOR_EACH_PTR(tmp
);
186 static int is_checked(struct state_list
*checked
, struct sm_state
*sm
)
188 struct sm_state
*tmp
;
190 FOR_EACH_PTR(checked
, tmp
) {
193 } END_FOR_EACH_PTR(tmp
);
199 * Example code: if (foo == 99) {
201 * Say 'foo' is a merged state that has many possible values. It is the combination
202 * of merges. separate_pools() iterates through the pools recursively and calls
203 * do_compare() for each time 'foo' was set.
205 static void separate_pools(struct sm_state
*sm
, int comparison
, struct range_list
*rl
,
206 struct stree_stack
**true_stack
,
207 struct stree_stack
**false_stack
,
208 struct state_list
**checked
)
210 int free_checked
= 0;
211 struct state_list
*checked_states
= NULL
;
217 Sometimes the implications are just too big to deal with
218 so we bail. Theoretically, bailing out here can cause more false
219 positives but won't hide actual bugs.
221 if (sm
->nr_children
> 4000) {
222 if (option_debug
|| option_debug_implied
) {
223 static char buf
[1028];
224 snprintf(buf
, sizeof(buf
), "debug: separate_pools: nr_children over 4000 (%d). (%s %s)",
225 sm
->nr_children
, sm
->name
, show_state(sm
->state
));
226 implied_debug_msg
= buf
;
231 if (checked
== NULL
) {
232 checked
= &checked_states
;
235 if (is_checked(*checked
, sm
))
237 add_ptr_list(checked
, sm
);
239 do_compare(sm
, comparison
, rl
, true_stack
, false_stack
);
241 separate_pools(sm
->left
, comparison
, rl
, true_stack
, false_stack
, checked
);
242 separate_pools(sm
->right
, comparison
, rl
, true_stack
, false_stack
, checked
);
247 struct sm_state
*filter_pools(struct sm_state
*sm
,
248 const struct stree_stack
*remove_stack
,
249 const struct stree_stack
*keep_stack
,
252 struct sm_state
*ret
= NULL
;
253 struct sm_state
*left
;
254 struct sm_state
*right
;
260 if (sm
->nr_children
> 4000) {
261 if (option_debug
|| option_debug_implied
) {
262 static char buf
[1028];
263 snprintf(buf
, sizeof(buf
), "debug: %s: nr_children over 4000 (%d). (%s %s)",
264 __func__
, sm
->nr_children
, sm
->name
, show_state(sm
->state
));
265 implied_debug_msg
= buf
;
270 if (pool_in_pools(sm
->pool
, remove_stack
)) {
271 DIMPLIED("removed %s from %d [stree %d]\n", show_sm(sm
), sm
->line
, get_stree_id(sm
->pool
));
276 if (!is_merged(sm
) || pool_in_pools(sm
->pool
, keep_stack
)) {
277 DIMPLIED("kept %s from %d [stree %d]\n", show_sm(sm
), sm
->line
, get_stree_id(sm
->pool
));
281 DIMPLIED("checking %s from %d (%d) [stree %d] left = %s [stree %d] right = %s [stree %d]\n",
282 show_sm(sm
), sm
->line
, sm
->nr_children
, get_stree_id(sm
->pool
),
283 sm
->left
? show_sm(sm
->left
) : "<none>", sm
->left
? get_stree_id(sm
->left
->pool
) : -1,
284 sm
->right
? show_sm(sm
->right
) : "<none>", sm
->right
? get_stree_id(sm
->right
->pool
) : -1);
285 left
= filter_pools(sm
->left
, remove_stack
, keep_stack
, &removed
);
286 right
= filter_pools(sm
->right
, remove_stack
, keep_stack
, &removed
);
288 DIMPLIED("kept %s from %d [stree %d]\n", show_sm(sm
), sm
->line
, get_stree_id(sm
->pool
));
292 if (!left
&& !right
) {
293 DIMPLIED("removed %s from %d <none> [stree %d]\n", show_sm(sm
), sm
->line
, get_stree_id(sm
->pool
));
298 ret
= clone_sm(right
);
303 ret
= clone_sm(left
);
308 ret
= merge_sm_states(left
, right
);
311 ret
->pool
= sm
->pool
;
314 DIMPLIED("partial %s => ", show_sm(sm
));
315 DIMPLIED("%s from %d [stree %d]\n", show_sm(ret
), sm
->line
, get_stree_id(sm
->pool
));
319 static int highest_stree_id(struct sm_state
*sm
)
324 if (!sm
->left
&& !sm
->right
)
328 left
= get_stree_id(sm
->left
->pool
);
330 right
= get_stree_id(sm
->right
->pool
);
337 static struct stree
*filter_stack(struct sm_state
*gate_sm
,
338 struct stree
*pre_stree
,
339 const struct stree_stack
*remove_stack
,
340 const struct stree_stack
*keep_stack
)
342 struct stree
*ret
= NULL
;
343 struct sm_state
*tmp
;
344 struct sm_state
*filtered_sm
;
350 FOR_EACH_SM(pre_stree
, tmp
) {
353 if (highest_stree_id(tmp
) < highest_stree_id(gate_sm
)) {
354 DIMPLIED("skipping %s. set before. %d vs %d\n",
355 tmp
->name
, highest_stree_id(tmp
),
356 highest_stree_id(gate_sm
));
360 filtered_sm
= filter_pools(tmp
, remove_stack
, keep_stack
, &modified
);
361 if (filtered_sm
&& modified
) {
362 /* the assignments here are for borrowed implications */
363 filtered_sm
->name
= tmp
->name
;
364 filtered_sm
->sym
= tmp
->sym
;
365 avl_insert(&ret
, filtered_sm
);
370 } END_FOR_EACH_SM(tmp
);
374 static void separate_and_filter(struct sm_state
*sm
, int comparison
, struct range_list
*rl
,
375 struct stree
*pre_stree
,
376 struct stree
**true_states
,
377 struct stree
**false_states
)
379 struct stree_stack
*true_stack
= NULL
;
380 struct stree_stack
*false_stack
= NULL
;
381 struct timeval time_before
;
382 struct timeval time_after
;
384 gettimeofday(&time_before
, NULL
);
386 if (!is_merged(sm
)) {
387 DIMPLIED("%d '%s' is not merged.\n", get_lineno(), sm
->name
);
391 if (option_debug_implied
|| option_debug
) {
392 sm_msg("checking implications: (%s %s %s)",
393 sm
->name
, show_special(comparison
), show_rl(rl
));
396 separate_pools(sm
, comparison
, rl
, &true_stack
, &false_stack
, NULL
);
398 DIMPLIED("filtering true stack.\n");
399 *true_states
= filter_stack(sm
, pre_stree
, false_stack
, true_stack
);
400 DIMPLIED("filtering false stack.\n");
401 *false_states
= filter_stack(sm
, pre_stree
, true_stack
, false_stack
);
402 free_stree_stack(&true_stack
);
403 free_stree_stack(&false_stack
);
404 if (option_debug_implied
|| option_debug
) {
405 printf("These are the implied states for the true path:\n");
406 __print_stree(*true_states
);
407 printf("These are the implied states for the false path:\n");
408 __print_stree(*false_states
);
411 gettimeofday(&time_after
, NULL
);
412 if (time_after
.tv_sec
- time_before
.tv_sec
> 7)
413 __bail_on_rest_of_function
= 1;
416 static struct expression
*get_left_most_expr(struct expression
*expr
)
418 expr
= strip_expr(expr
);
419 if (expr
->type
== EXPR_ASSIGNMENT
)
420 return get_left_most_expr(expr
->left
);
424 static int is_merged_expr(struct expression
*expr
)
429 if (get_value(expr
, &dummy
))
431 sm
= get_sm_state_expr(SMATCH_EXTRA
, expr
);
439 static void delete_equiv_stree(struct stree
**stree
, const char *name
, struct symbol
*sym
)
441 struct smatch_state
*state
;
442 struct relation
*rel
;
444 state
= get_state(SMATCH_EXTRA
, name
, sym
);
445 if (!estate_related(state
)) {
446 delete_state_stree(stree
, SMATCH_EXTRA
, name
, sym
);
450 FOR_EACH_PTR(estate_related(state
), rel
) {
451 delete_state_stree(stree
, SMATCH_EXTRA
, rel
->name
, rel
->sym
);
452 } END_FOR_EACH_PTR(rel
);
455 static int handle_comparison(struct expression
*expr
,
456 struct stree
**implied_true
,
457 struct stree
**implied_false
)
459 struct sm_state
*sm
= NULL
;
460 struct range_list
*rl
= NULL
;
461 struct expression
*left
;
462 struct expression
*right
;
464 int comparison
= expr
->op
;
466 left
= get_left_most_expr(expr
->left
);
467 right
= get_left_most_expr(expr
->right
);
469 if (is_merged_expr(left
)) {
470 sm
= get_sm_state_expr(SMATCH_EXTRA
, left
);
471 get_implied_rl(right
, &rl
);
472 } else if (is_merged_expr(right
)) {
473 sm
= get_sm_state_expr(SMATCH_EXTRA
, right
);
474 get_implied_rl(left
, &rl
);
475 comparison
= flip_comparison(comparison
);
483 type
= get_type(expr
);
486 if (type_positive_bits(rl_type(rl
)) > type_positive_bits(type
))
488 if (type_positive_bits(type
) < 31)
490 rl
= cast_rl(type
, rl
);
492 separate_and_filter(sm
, comparison
, rl
, __get_cur_stree(), implied_true
, implied_false
);
494 delete_equiv_stree(implied_true
, sm
->name
, sm
->sym
);
495 delete_equiv_stree(implied_false
, sm
->name
, sm
->sym
);
500 static int handle_zero_comparison(struct expression
*expr
,
501 struct stree
**implied_true
,
502 struct stree
**implied_false
)
509 if (expr
->type
== EXPR_POSTOP
)
510 expr
= strip_expr(expr
->unop
);
512 if (expr
->type
== EXPR_ASSIGNMENT
) {
513 /* most of the time ->pools will be empty here because we
514 just set the state, but if have assigned a conditional
515 function there are implications. */
519 name
= expr_to_var_sym(expr
, &sym
);
522 sm
= get_sm_state(SMATCH_EXTRA
, name
, sym
);
526 separate_and_filter(sm
, SPECIAL_NOTEQUAL
, tmp_range_list(estate_type(sm
->state
), 0), __get_cur_stree(), implied_true
, implied_false
);
527 delete_equiv_stree(implied_true
, name
, sym
);
528 delete_equiv_stree(implied_false
, name
, sym
);
535 static int handled_by_implied_hook(struct expression
*expr
,
536 struct stree
**implied_true
,
537 struct stree
**implied_false
)
539 struct stree_stack
*true_stack
= NULL
;
540 struct stree_stack
*false_stack
= NULL
;
541 struct stree
*pre_stree
;
544 sm
= comparison_implication_hook(expr
, &true_stack
, &false_stack
);
548 pre_stree
= clone_stree(__get_cur_stree());
550 *implied_true
= filter_stack(sm
, pre_stree
, false_stack
, true_stack
);
551 *implied_false
= filter_stack(sm
, pre_stree
, true_stack
, false_stack
);
553 free_stree(&pre_stree
);
554 free_stree_stack(&true_stack
);
555 free_stree_stack(&false_stack
);
560 static int handled_by_extra_states(struct expression
*expr
,
561 struct stree
**implied_true
,
562 struct stree
**implied_false
)
564 if (expr
->type
== EXPR_COMPARE
)
565 return handle_comparison(expr
, implied_true
, implied_false
);
567 return handle_zero_comparison(expr
, implied_true
, implied_false
);
571 static int handled_by_stored_conditions(struct expression
*expr
,
572 struct stree
**implied_true
,
573 struct stree
**implied_false
)
575 struct stree_stack
*true_stack
= NULL
;
576 struct stree_stack
*false_stack
= NULL
;
577 struct stree
*pre_stree
;
580 sm
= stored_condition_implication_hook(expr
, &true_stack
, &false_stack
);
584 pre_stree
= clone_stree(__get_cur_stree());
586 *implied_true
= filter_stack(sm
, pre_stree
, false_stack
, true_stack
);
587 *implied_false
= filter_stack(sm
, pre_stree
, true_stack
, false_stack
);
589 free_stree(&pre_stree
);
590 free_stree_stack(&true_stack
);
591 free_stree_stack(&false_stack
);
596 static int found_implications
;
597 static void get_tf_states(struct expression
*expr
,
598 struct stree
**implied_true
,
599 struct stree
**implied_false
)
601 if (handled_by_implied_hook(expr
, implied_true
, implied_false
))
604 if (handled_by_extra_states(expr
, implied_true
, implied_false
))
607 if (handled_by_stored_conditions(expr
, implied_true
, implied_false
))
612 found_implications
= 1;
615 static struct stree
*saved_implied_true
;
616 static struct stree
*saved_implied_false
;
618 static void save_implications_hook(struct expression
*expr
)
620 get_tf_states(expr
, &saved_implied_true
, &saved_implied_false
);
623 static void set_implied_states(struct expression
*expr
)
627 FOR_EACH_SM(saved_implied_true
, sm
) {
628 __set_true_false_sm(sm
, NULL
);
629 } END_FOR_EACH_SM(sm
);
630 free_stree(&saved_implied_true
);
632 FOR_EACH_SM(saved_implied_false
, sm
) {
633 __set_true_false_sm(NULL
, sm
);
634 } END_FOR_EACH_SM(sm
);
635 free_stree(&saved_implied_false
);
638 void param_limit_implications(struct expression
*expr
, int param
, char *key
, char *value
)
640 struct expression
*arg
;
641 struct symbol
*compare_type
;
645 struct sm_state
*tmp
;
646 struct stree
*implied_true
= NULL
;
647 struct stree
*implied_false
= NULL
;
648 struct range_list
*orig
, *limit
, *rl
;
650 while (expr
->type
== EXPR_ASSIGNMENT
)
651 expr
= strip_expr(expr
->right
);
652 if (expr
->type
!= EXPR_CALL
)
655 arg
= get_argument_from_call_expr(expr
->args
, param
);
659 name
= get_variable_from_key(arg
, key
, &sym
);
663 sm
= get_sm_state(SMATCH_EXTRA
, name
, sym
);
664 if (!sm
|| !sm
->merged
)
667 if (strcmp(key
, "$") == 0)
668 compare_type
= get_arg_type(expr
->fn
, param
);
670 compare_type
= get_member_type_from_key(arg
, key
);
672 orig
= estate_rl(sm
->state
);
673 orig
= cast_rl(compare_type
, orig
);
675 call_results_to_rl(expr
, compare_type
, value
, &limit
);
676 rl
= rl_intersection(orig
, limit
);
678 separate_and_filter(sm
, SPECIAL_EQUAL
, rl
, __get_cur_stree(), &implied_true
, &implied_false
);
680 FOR_EACH_SM(implied_true
, tmp
) {
681 __set_sm_fake_stree(tmp
);
682 } END_FOR_EACH_SM(tmp
);
684 free_stree(&implied_true
);
685 free_stree(&implied_false
);
690 struct range_list
*__get_implied_values(struct expression
*switch_expr
)
694 struct smatch_state
*state
;
695 struct range_list
*ret
= NULL
;
697 name
= expr_to_var_sym(switch_expr
, &sym
);
700 state
= get_state(SMATCH_EXTRA
, name
, sym
);
703 ret
= clone_rl(estate_rl(state
));
709 type
= get_type(switch_expr
);
710 ret
= alloc_rl(sval_type_min(type
), sval_type_max(type
));
715 struct stree
*__implied_case_stree(struct expression
*switch_expr
,
716 struct expression
*case_expr
,
717 struct expression
*case_to
,
718 struct range_list_stack
**remaining_cases
,
719 struct stree
**raw_stree
)
724 struct stree
*true_states
= NULL
;
725 struct stree
*false_states
= NULL
;
726 struct stree
*extra_states
= NULL
;
727 struct stree
*ret
= clone_stree(*raw_stree
);
729 struct range_list
*rl
= NULL
;
731 name
= expr_to_var_sym(switch_expr
, &sym
);
734 sm
= get_sm_state_stree(*raw_stree
, SMATCH_EXTRA
, name
, sym
);
736 if (get_value(case_to
, &end
) && get_value(case_expr
, &start
)) {
737 filter_top_rl(remaining_cases
, start
, end
);
738 add_range(&rl
, start
, end
);
739 } else if (get_value(case_expr
, &start
)) {
740 filter_top_rl(remaining_cases
, start
, start
);
741 add_range(&rl
, start
, start
);
743 rl
= clone_rl(top_rl(*remaining_cases
));
747 separate_and_filter(sm
, SPECIAL_EQUAL
, rl
, *raw_stree
, &true_states
, &false_states
);
749 __push_fake_cur_stree();
751 set_extra_nomod(name
, sym
, alloc_estate_rl(rl
));
752 extra_states
= __pop_fake_cur_stree();
753 overwrite_stree(extra_states
, &true_states
);
754 overwrite_stree(true_states
, &ret
);
755 free_stree(&extra_states
);
756 free_stree(&true_states
);
757 free_stree(&false_states
);
763 static void match_end_func(struct symbol
*sym
)
767 implied_debug_msg
= NULL
;
770 static int sm_state_in_slist(struct sm_state
*sm
, struct state_list
*slist
)
772 struct sm_state
*tmp
;
774 FOR_EACH_PTR(slist
, tmp
) {
777 } END_FOR_EACH_PTR(tmp
);
782 * The situation is we have a SMATCH_EXTRA state and we want to break it into
783 * each of the ->possible states and find the implications of each. The caller
784 * has to use __push_fake_cur_stree() to preserve the correct states so they
785 * can be restored later.
787 void overwrite_states_using_pool(struct sm_state
*sm
)
789 struct sm_state
*old
;
790 struct sm_state
*new;
795 FOR_EACH_SM(sm
->pool
, old
) {
796 new = get_sm_state(old
->owner
, old
->name
, old
->sym
);
797 if (!new) /* the variable went out of scope */
799 if (sm_state_in_slist(old
, new->possible
))
800 set_state(old
->owner
, old
->name
, old
->sym
, old
->state
);
801 } END_FOR_EACH_SM(old
);
804 int assume(struct expression
*expr
)
806 int orig_final_pass
= final_pass
;
809 __push_fake_cur_stree();
810 found_implications
= 0;
811 __split_whole_condition(expr
);
812 final_pass
= orig_final_pass
;
814 if (!found_implications
) {
815 __discard_false_states();
816 __free_fake_cur_stree();
823 void end_assume(void)
825 __discard_false_states();
826 __free_fake_cur_stree();
829 void __extra_match_condition(struct expression
*expr
);
830 void __comparison_match_condition(struct expression
*expr
);
831 void __stored_condition(struct expression
*expr
);
832 void register_implications(int id
)
834 add_hook(&save_implications_hook
, CONDITION_HOOK
);
835 add_hook(&set_implied_states
, CONDITION_HOOK
);
836 add_hook(&__extra_match_condition
, CONDITION_HOOK
);
837 add_hook(&__comparison_match_condition
, CONDITION_HOOK
);
838 add_hook(&__stored_condition
, CONDITION_HOOK
);
839 add_hook(&match_end_func
, END_FUNC_HOOK
);