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
, int *mixed
)
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
);
165 if (mixed
&& !is_merged(s
) && !istrue
&& !isfalse
)
169 add_pool(true_stack
, s
->pool
);
172 add_pool(false_stack
, s
->pool
);
175 static int pool_in_pools(struct stree
*pool
,
176 const struct stree_stack
*pools
)
180 FOR_EACH_PTR(pools
, tmp
) {
185 } END_FOR_EACH_PTR(tmp
);
189 static int is_checked(struct state_list
*checked
, struct sm_state
*sm
)
191 struct sm_state
*tmp
;
193 FOR_EACH_PTR(checked
, tmp
) {
196 } END_FOR_EACH_PTR(tmp
);
202 * Example code: if (foo == 99) {
204 * Say 'foo' is a merged state that has many possible values. It is the combination
205 * of merges. separate_pools() iterates through the pools recursively and calls
206 * do_compare() for each time 'foo' was set.
208 static void separate_pools(struct sm_state
*sm
, int comparison
, struct range_list
*rl
,
209 struct stree_stack
**true_stack
,
210 struct stree_stack
**false_stack
,
211 struct state_list
**checked
, int *mixed
)
213 int free_checked
= 0;
214 struct state_list
*checked_states
= NULL
;
220 Sometimes the implications are just too big to deal with
221 so we bail. Theoretically, bailing out here can cause more false
222 positives but won't hide actual bugs.
224 if (sm
->nr_children
> 4000) {
225 if (option_debug
|| option_debug_implied
) {
226 static char buf
[1028];
227 snprintf(buf
, sizeof(buf
), "debug: separate_pools: nr_children over 4000 (%d). (%s %s)",
228 sm
->nr_children
, sm
->name
, show_state(sm
->state
));
229 implied_debug_msg
= buf
;
234 if (checked
== NULL
) {
235 checked
= &checked_states
;
238 if (is_checked(*checked
, sm
))
240 add_ptr_list(checked
, sm
);
242 do_compare(sm
, comparison
, rl
, true_stack
, false_stack
, mixed
);
244 separate_pools(sm
->left
, comparison
, rl
, true_stack
, false_stack
, checked
, mixed
);
245 separate_pools(sm
->right
, comparison
, rl
, true_stack
, false_stack
, checked
, mixed
);
250 struct sm_state
*filter_pools(struct sm_state
*sm
,
251 const struct stree_stack
*remove_stack
,
252 const struct stree_stack
*keep_stack
,
255 struct sm_state
*ret
= NULL
;
256 struct sm_state
*left
;
257 struct sm_state
*right
;
263 if (sm
->nr_children
> 4000) {
264 if (option_debug
|| option_debug_implied
) {
265 static char buf
[1028];
266 snprintf(buf
, sizeof(buf
), "debug: %s: nr_children over 4000 (%d). (%s %s)",
267 __func__
, sm
->nr_children
, sm
->name
, show_state(sm
->state
));
268 implied_debug_msg
= buf
;
273 if (pool_in_pools(sm
->pool
, remove_stack
)) {
274 DIMPLIED("removed %s from %d [stree %d]\n", show_sm(sm
), sm
->line
, get_stree_id(sm
->pool
));
279 if (!is_merged(sm
) || pool_in_pools(sm
->pool
, keep_stack
)) {
280 DIMPLIED("kept %s from %d [stree %d]\n", show_sm(sm
), sm
->line
, get_stree_id(sm
->pool
));
284 DIMPLIED("checking %s from %d (%d) [stree %d] left = %s [stree %d] right = %s [stree %d]\n",
285 show_sm(sm
), sm
->line
, sm
->nr_children
, get_stree_id(sm
->pool
),
286 sm
->left
? show_sm(sm
->left
) : "<none>", sm
->left
? get_stree_id(sm
->left
->pool
) : -1,
287 sm
->right
? show_sm(sm
->right
) : "<none>", sm
->right
? get_stree_id(sm
->right
->pool
) : -1);
288 left
= filter_pools(sm
->left
, remove_stack
, keep_stack
, &removed
);
289 right
= filter_pools(sm
->right
, remove_stack
, keep_stack
, &removed
);
291 DIMPLIED("kept %s from %d [stree %d]\n", show_sm(sm
), sm
->line
, get_stree_id(sm
->pool
));
295 if (!left
&& !right
) {
296 DIMPLIED("removed %s from %d <none> [stree %d]\n", show_sm(sm
), sm
->line
, get_stree_id(sm
->pool
));
301 ret
= clone_sm(right
);
306 ret
= clone_sm(left
);
311 ret
= merge_sm_states(left
, right
);
314 ret
->pool
= sm
->pool
;
317 DIMPLIED("partial %s => ", show_sm(sm
));
318 DIMPLIED("%s from %d [stree %d]\n", show_sm(ret
), sm
->line
, get_stree_id(sm
->pool
));
322 static int highest_stree_id(struct sm_state
*sm
)
327 if (!sm
->left
&& !sm
->right
)
331 left
= get_stree_id(sm
->left
->pool
);
333 right
= get_stree_id(sm
->right
->pool
);
340 static struct stree
*filter_stack(struct sm_state
*gate_sm
,
341 struct stree
*pre_stree
,
342 const struct stree_stack
*remove_stack
,
343 const struct stree_stack
*keep_stack
)
345 struct stree
*ret
= NULL
;
346 struct sm_state
*tmp
;
347 struct sm_state
*filtered_sm
;
353 FOR_EACH_SM(pre_stree
, tmp
) {
356 if (highest_stree_id(tmp
) < highest_stree_id(gate_sm
)) {
357 DIMPLIED("skipping %s. set before. %d vs %d\n",
358 tmp
->name
, highest_stree_id(tmp
),
359 highest_stree_id(gate_sm
));
363 filtered_sm
= filter_pools(tmp
, remove_stack
, keep_stack
, &modified
);
364 if (filtered_sm
&& modified
) {
365 /* the assignments here are for borrowed implications */
366 filtered_sm
->name
= tmp
->name
;
367 filtered_sm
->sym
= tmp
->sym
;
368 avl_insert(&ret
, filtered_sm
);
373 } END_FOR_EACH_SM(tmp
);
377 static void separate_and_filter(struct sm_state
*sm
, int comparison
, struct range_list
*rl
,
378 struct stree
*pre_stree
,
379 struct stree
**true_states
,
380 struct stree
**false_states
,
383 struct stree_stack
*true_stack
= NULL
;
384 struct stree_stack
*false_stack
= NULL
;
385 struct timeval time_before
;
386 struct timeval time_after
;
388 gettimeofday(&time_before
, NULL
);
393 if (!is_merged(sm
)) {
394 DIMPLIED("%d '%s' is not merged.\n", get_lineno(), sm
->name
);
398 if (option_debug_implied
|| option_debug
) {
399 sm_msg("checking implications: (%s %s %s)",
400 sm
->name
, show_special(comparison
), show_rl(rl
));
403 separate_pools(sm
, comparison
, rl
, &true_stack
, &false_stack
, NULL
, mixed
);
405 DIMPLIED("filtering true stack.\n");
406 *true_states
= filter_stack(sm
, pre_stree
, false_stack
, true_stack
);
407 DIMPLIED("filtering false stack.\n");
408 *false_states
= filter_stack(sm
, pre_stree
, true_stack
, false_stack
);
409 free_stree_stack(&true_stack
);
410 free_stree_stack(&false_stack
);
411 if (option_debug_implied
|| option_debug
) {
412 printf("These are the implied states for the true path:\n");
413 __print_stree(*true_states
);
414 printf("These are the implied states for the false path:\n");
415 __print_stree(*false_states
);
418 gettimeofday(&time_after
, NULL
);
419 if (time_after
.tv_sec
- time_before
.tv_sec
> 7)
420 __bail_on_rest_of_function
= 1;
423 static struct expression
*get_left_most_expr(struct expression
*expr
)
425 expr
= strip_expr(expr
);
426 if (expr
->type
== EXPR_ASSIGNMENT
)
427 return get_left_most_expr(expr
->left
);
431 static int is_merged_expr(struct expression
*expr
)
436 if (get_value(expr
, &dummy
))
438 sm
= get_sm_state_expr(SMATCH_EXTRA
, expr
);
446 static void delete_equiv_stree(struct stree
**stree
, const char *name
, struct symbol
*sym
)
448 struct smatch_state
*state
;
449 struct relation
*rel
;
451 state
= get_state(SMATCH_EXTRA
, name
, sym
);
452 if (!estate_related(state
)) {
453 delete_state_stree(stree
, SMATCH_EXTRA
, name
, sym
);
457 FOR_EACH_PTR(estate_related(state
), rel
) {
458 delete_state_stree(stree
, SMATCH_EXTRA
, rel
->name
, rel
->sym
);
459 } END_FOR_EACH_PTR(rel
);
462 static int handle_comparison(struct expression
*expr
,
463 struct stree
**implied_true
,
464 struct stree
**implied_false
)
466 struct sm_state
*sm
= NULL
;
467 struct range_list
*rl
= NULL
;
468 struct expression
*left
;
469 struct expression
*right
;
471 int comparison
= expr
->op
;
474 left
= get_left_most_expr(expr
->left
);
475 right
= get_left_most_expr(expr
->right
);
477 if (is_merged_expr(left
)) {
478 sm
= get_sm_state_expr(SMATCH_EXTRA
, left
);
479 get_implied_rl(right
, &rl
);
480 } else if (is_merged_expr(right
)) {
481 sm
= get_sm_state_expr(SMATCH_EXTRA
, right
);
482 get_implied_rl(left
, &rl
);
483 comparison
= flip_comparison(comparison
);
491 type
= get_type(expr
);
494 if (type_positive_bits(rl_type(rl
)) > type_positive_bits(type
))
496 if (type_positive_bits(type
) < 31)
498 rl
= cast_rl(type
, rl
);
500 separate_and_filter(sm
, comparison
, rl
, __get_cur_stree(), implied_true
, implied_false
, &mixed
);
503 delete_equiv_stree(implied_true
, sm
->name
, sm
->sym
);
504 delete_equiv_stree(implied_false
, sm
->name
, sm
->sym
);
510 static int handle_zero_comparison(struct expression
*expr
,
511 struct stree
**implied_true
,
512 struct stree
**implied_false
)
520 if (expr
->type
== EXPR_POSTOP
)
521 expr
= strip_expr(expr
->unop
);
523 if (expr
->type
== EXPR_ASSIGNMENT
) {
524 /* most of the time ->pools will be empty here because we
525 just set the state, but if have assigned a conditional
526 function there are implications. */
530 name
= expr_to_var_sym(expr
, &sym
);
533 sm
= get_sm_state(SMATCH_EXTRA
, name
, sym
);
537 separate_and_filter(sm
, SPECIAL_NOTEQUAL
, tmp_range_list(estate_type(sm
->state
), 0), __get_cur_stree(), implied_true
, implied_false
, &mixed
);
539 delete_equiv_stree(implied_true
, name
, sym
);
540 delete_equiv_stree(implied_false
, name
, sym
);
548 static int handled_by_implied_hook(struct expression
*expr
,
549 struct stree
**implied_true
,
550 struct stree
**implied_false
)
552 struct stree_stack
*true_stack
= NULL
;
553 struct stree_stack
*false_stack
= NULL
;
554 struct stree
*pre_stree
;
557 sm
= comparison_implication_hook(expr
, &true_stack
, &false_stack
);
561 pre_stree
= clone_stree(__get_cur_stree());
563 *implied_true
= filter_stack(sm
, pre_stree
, false_stack
, true_stack
);
564 *implied_false
= filter_stack(sm
, pre_stree
, true_stack
, false_stack
);
566 free_stree(&pre_stree
);
567 free_stree_stack(&true_stack
);
568 free_stree_stack(&false_stack
);
573 static int handled_by_extra_states(struct expression
*expr
,
574 struct stree
**implied_true
,
575 struct stree
**implied_false
)
577 if (expr
->type
== EXPR_COMPARE
)
578 return handle_comparison(expr
, implied_true
, implied_false
);
580 return handle_zero_comparison(expr
, implied_true
, implied_false
);
584 static int handled_by_stored_conditions(struct expression
*expr
,
585 struct stree
**implied_true
,
586 struct stree
**implied_false
)
588 struct stree_stack
*true_stack
= NULL
;
589 struct stree_stack
*false_stack
= NULL
;
590 struct stree
*pre_stree
;
593 sm
= stored_condition_implication_hook(expr
, &true_stack
, &false_stack
);
597 pre_stree
= clone_stree(__get_cur_stree());
599 *implied_true
= filter_stack(sm
, pre_stree
, false_stack
, true_stack
);
600 *implied_false
= filter_stack(sm
, pre_stree
, true_stack
, false_stack
);
602 free_stree(&pre_stree
);
603 free_stree_stack(&true_stack
);
604 free_stree_stack(&false_stack
);
609 static int found_implications
;
610 static void get_tf_states(struct expression
*expr
,
611 struct stree
**implied_true
,
612 struct stree
**implied_false
)
614 if (handled_by_implied_hook(expr
, implied_true
, implied_false
))
617 if (handled_by_extra_states(expr
, implied_true
, implied_false
))
620 if (handled_by_stored_conditions(expr
, implied_true
, implied_false
))
625 found_implications
= 1;
628 static struct stree
*saved_implied_true
;
629 static struct stree
*saved_implied_false
;
631 static void save_implications_hook(struct expression
*expr
)
633 get_tf_states(expr
, &saved_implied_true
, &saved_implied_false
);
636 static void set_implied_states(struct expression
*expr
)
640 FOR_EACH_SM(saved_implied_true
, sm
) {
641 __set_true_false_sm(sm
, NULL
);
642 } END_FOR_EACH_SM(sm
);
643 free_stree(&saved_implied_true
);
645 FOR_EACH_SM(saved_implied_false
, sm
) {
646 __set_true_false_sm(NULL
, sm
);
647 } END_FOR_EACH_SM(sm
);
648 free_stree(&saved_implied_false
);
651 void param_limit_implications(struct expression
*expr
, int param
, char *key
, char *value
)
653 struct expression
*arg
;
654 struct symbol
*compare_type
;
658 struct sm_state
*tmp
;
659 struct stree
*implied_true
= NULL
;
660 struct stree
*implied_false
= NULL
;
661 struct range_list
*orig
, *limit
, *rl
;
663 while (expr
->type
== EXPR_ASSIGNMENT
)
664 expr
= strip_expr(expr
->right
);
665 if (expr
->type
!= EXPR_CALL
)
668 arg
= get_argument_from_call_expr(expr
->args
, param
);
672 name
= get_variable_from_key(arg
, key
, &sym
);
676 sm
= get_sm_state(SMATCH_EXTRA
, name
, sym
);
677 if (!sm
|| !sm
->merged
)
680 if (strcmp(key
, "$") == 0)
681 compare_type
= get_arg_type(expr
->fn
, param
);
683 compare_type
= get_member_type_from_key(arg
, key
);
685 orig
= estate_rl(sm
->state
);
686 orig
= cast_rl(compare_type
, orig
);
688 call_results_to_rl(expr
, compare_type
, value
, &limit
);
689 rl
= rl_intersection(orig
, limit
);
691 separate_and_filter(sm
, SPECIAL_EQUAL
, rl
, __get_cur_stree(), &implied_true
, &implied_false
, NULL
);
693 FOR_EACH_SM(implied_true
, tmp
) {
694 __set_sm_fake_stree(tmp
);
695 } END_FOR_EACH_SM(tmp
);
697 free_stree(&implied_true
);
698 free_stree(&implied_false
);
703 struct stree
*__implied_case_stree(struct expression
*switch_expr
,
704 struct range_list
*rl
,
705 struct range_list_stack
**remaining_cases
,
706 struct stree
**raw_stree
)
711 struct stree
*true_states
= NULL
;
712 struct stree
*false_states
= NULL
;
713 struct stree
*extra_states
;
714 struct stree
*ret
= clone_stree(*raw_stree
);
716 name
= expr_to_var_sym(switch_expr
, &sym
);
721 filter_top_rl(remaining_cases
, rl
);
723 rl
= clone_rl(top_rl(*remaining_cases
));
725 sm
= get_sm_state_stree(*raw_stree
, SMATCH_EXTRA
, name
, sym
);
727 separate_and_filter(sm
, SPECIAL_EQUAL
, rl
, *raw_stree
, &true_states
, &false_states
, NULL
);
729 __push_fake_cur_stree();
731 set_extra_nomod(name
, sym
, alloc_estate_rl(rl
));
732 extra_states
= __pop_fake_cur_stree();
733 overwrite_stree(extra_states
, &true_states
);
734 overwrite_stree(true_states
, &ret
);
735 free_stree(&extra_states
);
736 free_stree(&true_states
);
737 free_stree(&false_states
);
743 static void match_end_func(struct symbol
*sym
)
747 implied_debug_msg
= NULL
;
750 static int sm_state_in_slist(struct sm_state
*sm
, struct state_list
*slist
)
752 struct sm_state
*tmp
;
754 FOR_EACH_PTR(slist
, tmp
) {
757 } END_FOR_EACH_PTR(tmp
);
762 * The situation is we have a SMATCH_EXTRA state and we want to break it into
763 * each of the ->possible states and find the implications of each. The caller
764 * has to use __push_fake_cur_stree() to preserve the correct states so they
765 * can be restored later.
767 void overwrite_states_using_pool(struct sm_state
*sm
)
769 struct sm_state
*old
;
770 struct sm_state
*new;
775 FOR_EACH_SM(sm
->pool
, old
) {
776 new = get_sm_state(old
->owner
, old
->name
, old
->sym
);
777 if (!new) /* the variable went out of scope */
779 if (sm_state_in_slist(old
, new->possible
))
780 set_state(old
->owner
, old
->name
, old
->sym
, old
->state
);
781 } END_FOR_EACH_SM(old
);
784 int assume(struct expression
*expr
)
786 int orig_final_pass
= final_pass
;
789 __push_fake_cur_stree();
790 found_implications
= 0;
791 __split_whole_condition(expr
);
792 final_pass
= orig_final_pass
;
794 if (!found_implications
) {
795 __discard_false_states();
796 __free_fake_cur_stree();
803 void end_assume(void)
805 __discard_false_states();
806 __free_fake_cur_stree();
809 void __extra_match_condition(struct expression
*expr
);
810 void __comparison_match_condition(struct expression
*expr
);
811 void __stored_condition(struct expression
*expr
);
812 void register_implications(int id
)
814 add_hook(&save_implications_hook
, CONDITION_HOOK
);
815 add_hook(&__extra_match_condition
, CONDITION_HOOK
);
816 add_hook(&set_implied_states
, CONDITION_HOOK
);
817 add_hook(&__comparison_match_condition
, CONDITION_HOOK
);
818 add_hook(&__stored_condition
, CONDITION_HOOK
);
819 add_hook(&match_end_func
, END_FUNC_HOOK
);