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.
61 #include "smatch_slist.h"
62 #include "smatch_extra.h"
64 char *implied_debug_msg
;
66 bool implications_off
;
70 #define full_debug implied_debug
71 #define DIMPLIED(msg...) do { if (full_debug) printf(msg); } while (0)
73 bool debug_implied(void)
75 return option_debug
|| implied_debug
|| full_debug
;
80 * It messes things up to free range list allocations. This helper fuction
81 * lets us reuse memory instead of doing new allocations.
83 static struct range_list
*tmp_range_list(struct symbol
*type
, long long num
)
85 static struct range_list
*my_list
= NULL
;
86 static struct data_range
*my_range
;
88 __free_ptr_list((struct ptr_list
**)&my_list
);
89 my_range
= alloc_range(ll_to_sval(num
), ll_to_sval(num
));
90 add_ptr_list(&my_list
, my_range
);
94 static const char *show_comparison(int op
)
96 if (op
== PARAM_LIMIT
)
98 return show_special(op
);
101 static void print_debug_tf(struct sm_state
*sm
, int istrue
, int isfalse
)
103 if (!full_debug
&& !option_debug
&& !implied_debug
)
106 if (istrue
&& isfalse
) {
107 printf("%s: %d: does not exist.\n", show_sm(sm
), sm
->line
);
109 printf("'%s = %s' from %d is true. %s[stree %d]\n", sm
->name
, show_state(sm
->state
),
110 sm
->line
, sm
->merged
? "[merged]" : "[leaf]",
111 get_stree_id(sm
->pool
));
112 } else if (isfalse
) {
113 printf("'%s = %s' from %d is false. %s[stree %d]\n", sm
->name
, show_state(sm
->state
),
115 sm
->merged
? "[merged]" : "[leaf]",
116 get_stree_id(sm
->pool
));
118 printf("'%s = %s' from %d could be true or false. %s[stree %d]\n", sm
->name
,
119 show_state(sm
->state
), sm
->line
,
120 sm
->merged
? "[merged]" : "[leaf]",
121 get_stree_id(sm
->pool
));
125 void split_comparison_helper(struct range_list
*left_orig
, int op
, struct range_list
*right_orig
,
126 struct range_list
**left_true_rl
, struct range_list
**left_false_rl
)
128 if (op
== PARAM_LIMIT
) {
129 *left_true_rl
= rl_intersection(left_orig
, right_orig
);
130 *left_false_rl
= rl_filter(left_orig
, right_orig
);
134 split_comparison_rl(left_orig
, op
, right_orig
, left_true_rl
, left_false_rl
, NULL
, NULL
);
137 static int create_fake_history(struct sm_state
*sm
, int comparison
, struct range_list
*rl
)
139 struct range_list
*orig_rl
;
140 struct range_list
*true_rl
, *false_rl
;
141 struct stree
*true_stree
, *false_stree
;
142 struct sm_state
*true_sm
, *false_sm
;
145 if (is_merged(sm
) || sm
->left
|| sm
->right
)
147 if (!rl_to_sval(rl
, &sval
))
149 if (!estate_rl(sm
->state
))
152 orig_rl
= cast_rl(rl_type(rl
), estate_rl(sm
->state
));
153 split_comparison_helper(orig_rl
, comparison
, rl
, &true_rl
, &false_rl
);
155 true_rl
= rl_truncate_cast(estate_type(sm
->state
), true_rl
);
156 false_rl
= rl_truncate_cast(estate_type(sm
->state
), false_rl
);
157 if (is_whole_rl(true_rl
) || is_whole_rl(false_rl
) ||
158 !true_rl
|| !false_rl
||
159 rl_equiv(orig_rl
, true_rl
) || rl_equiv(orig_rl
, false_rl
) ||
160 rl_equiv(estate_rl(sm
->state
), true_rl
) || rl_equiv(estate_rl(sm
->state
), false_rl
))
163 if (rl_intersection(true_rl
, false_rl
)) {
165 * Normally these won't intersect, but one exception is when
166 * we're dealing with mtags. We have a long list of mtags and
167 * then negate the list. Now it's over the limit for mtag list
168 * length and we squash it down to 4096-ptr_max. So then it's
169 * possible for the true and false rl to overlap.
175 sm_msg("fake_history: %s vs %s. %s %s %s. --> T: %s F: %s",
176 sm
->name
, show_rl(rl
), sm
->state
->name
, show_comparison(comparison
), show_rl(rl
),
177 show_rl(true_rl
), show_rl(false_rl
));
179 true_sm
= clone_sm(sm
);
180 false_sm
= clone_sm(sm
);
182 true_sm
->state
= clone_partial_estate(sm
->state
, true_rl
);
183 free_slist(&true_sm
->possible
);
184 add_possible_sm(true_sm
, true_sm
);
185 false_sm
->state
= clone_partial_estate(sm
->state
, false_rl
);
186 free_slist(&false_sm
->possible
);
187 add_possible_sm(false_sm
, false_sm
);
189 true_stree
= clone_stree(sm
->pool
);
190 false_stree
= clone_stree(sm
->pool
);
192 overwrite_sm_state_stree(&true_stree
, true_sm
);
193 overwrite_sm_state_stree(&false_stree
, false_sm
);
195 true_sm
->pool
= true_stree
;
196 false_sm
->pool
= false_stree
;
200 sm
->right
= false_sm
;
206 * add_pool() adds a slist to *pools. If the slist has already been
207 * added earlier then it doesn't get added a second time.
209 void add_pool(struct state_list
**pools
, struct sm_state
*new)
211 struct sm_state
*tmp
;
213 FOR_EACH_PTR(*pools
, tmp
) {
214 if (tmp
->pool
< new->pool
)
216 else if (tmp
->pool
== new->pool
) {
219 INSERT_CURRENT(new, tmp
);
222 } END_FOR_EACH_PTR(tmp
);
223 add_ptr_list(pools
, new);
226 static int pool_in_pools(struct stree
*pool
,
227 const struct state_list
*slist
)
229 struct sm_state
*tmp
;
231 FOR_EACH_PTR(slist
, tmp
) {
234 if (tmp
->pool
== pool
)
236 } END_FOR_EACH_PTR(tmp
);
240 static int remove_pool(struct state_list
**pools
, struct stree
*remove
)
242 struct sm_state
*tmp
;
245 FOR_EACH_PTR(*pools
, tmp
) {
246 if (tmp
->pool
== remove
) {
247 DELETE_CURRENT_PTR(tmp
);
250 } END_FOR_EACH_PTR(tmp
);
255 static bool possibly_true_helper(struct range_list
*var_rl
, int comparison
, struct range_list
*rl
)
257 if (comparison
== PARAM_LIMIT
) {
258 struct range_list
*intersect
;
260 intersect
= rl_intersection(var_rl
, rl
);
265 return possibly_true_rl(var_rl
, comparison
, rl
);
268 static bool possibly_false_helper(struct range_list
*var_rl
, int comparison
, struct range_list
*rl
)
270 if (comparison
== PARAM_LIMIT
) {
271 struct range_list
*intersect
;
273 intersect
= rl_intersection(var_rl
, rl
);
274 /* if it's not equiv then it's possibly false */
275 return !rl_equiv(var_rl
, intersect
);
277 return possibly_false_rl(var_rl
, comparison
, rl
);
281 * If 'foo' == 99 add it that pool to the true pools. If it's false, add it to
282 * the false pools. If we're not sure, then we don't add it to either.
284 static void do_compare(struct sm_state
*sm
, int comparison
, struct range_list
*rl
,
285 struct state_list
**true_stack
,
286 struct state_list
**maybe_stack
,
287 struct state_list
**false_stack
,
288 int *mixed
, struct sm_state
*gate_sm
)
292 struct range_list
*var_rl
;
297 var_rl
= cast_rl(rl_type(rl
), estate_rl(sm
->state
));
299 istrue
= !possibly_false_helper(var_rl
, comparison
, rl
);
300 isfalse
= !possibly_true_helper(var_rl
, comparison
, rl
);
302 print_debug_tf(sm
, istrue
, isfalse
);
304 /* give up if we have borrowed implications (smatch_equiv.c) */
305 if (sm
->sym
!= gate_sm
->sym
||
306 strcmp(sm
->name
, gate_sm
->name
) != 0) {
311 if (mixed
&& !*mixed
&& !is_merged(sm
) && !istrue
&& !isfalse
) {
312 if (!create_fake_history(sm
, comparison
, rl
))
317 add_pool(true_stack
, sm
);
319 add_pool(false_stack
, sm
);
321 add_pool(maybe_stack
, sm
);
324 static int is_checked(struct state_list
*checked
, struct sm_state
*sm
)
326 struct sm_state
*tmp
;
328 FOR_EACH_PTR(checked
, tmp
) {
331 } END_FOR_EACH_PTR(tmp
);
337 * Example code: if (foo == 99) {
339 * Say 'foo' is a merged state that has many possible values. It is the combination
340 * of merges. separate_pools() iterates through the pools recursively and calls
341 * do_compare() for each time 'foo' was set.
343 static void __separate_pools(struct sm_state
*sm
, int comparison
, struct range_list
*rl
,
344 struct state_list
**true_stack
,
345 struct state_list
**maybe_stack
,
346 struct state_list
**false_stack
,
347 struct state_list
**checked
, int *mixed
, struct sm_state
*gate_sm
,
348 struct timeval
*start_time
)
350 int free_checked
= 0;
351 struct state_list
*checked_states
= NULL
;
352 struct timeval now
, diff
;
357 gettimeofday(&now
, NULL
);
358 timersub(&now
, start_time
, &diff
);
359 if (diff
.tv_sec
>= 1) {
361 sm_msg("debug: %s: implications taking too long. (%s %s %s)",
362 __func__
, sm
->state
->name
, show_comparison(comparison
), show_rl(rl
));
368 if (checked
== NULL
) {
369 checked
= &checked_states
;
372 if (is_checked(*checked
, sm
))
374 add_ptr_list(checked
, sm
);
376 do_compare(sm
, comparison
, rl
, true_stack
, maybe_stack
, false_stack
, mixed
, gate_sm
);
378 __separate_pools(sm
->left
, comparison
, rl
, true_stack
, maybe_stack
, false_stack
, checked
, mixed
, gate_sm
, start_time
);
379 __separate_pools(sm
->right
, comparison
, rl
, true_stack
, maybe_stack
, false_stack
, checked
, mixed
, gate_sm
, start_time
);
384 static void separate_pools(struct sm_state
*sm
, int comparison
, struct range_list
*rl
,
385 struct state_list
**true_stack
,
386 struct state_list
**false_stack
,
387 struct state_list
**checked
, int *mixed
)
389 struct state_list
*maybe_stack
= NULL
;
390 struct sm_state
*tmp
;
391 struct timeval start_time
;
394 gettimeofday(&start_time
, NULL
);
395 __separate_pools(sm
, comparison
, rl
, true_stack
, &maybe_stack
, false_stack
, checked
, mixed
, sm
, &start_time
);
400 FOR_EACH_PTR(*true_stack
, sm
) {
401 sm_msg("TRUE %s [stree %d %p]", show_sm(sm
), get_stree_id(sm
->pool
), sm
->pool
);
402 } END_FOR_EACH_PTR(sm
);
404 FOR_EACH_PTR(maybe_stack
, sm
) {
405 sm_msg("MAYBE %s %s[stree %d %p]",
406 show_sm(sm
), sm
->merged
? "(merged) ": "", get_stree_id(sm
->pool
), sm
->pool
);
407 } END_FOR_EACH_PTR(sm
);
409 FOR_EACH_PTR(*false_stack
, sm
) {
410 sm_msg("FALSE %s [stree %d %p]", show_sm(sm
), get_stree_id(sm
->pool
), sm
->pool
);
411 } END_FOR_EACH_PTR(sm
);
413 /* if it's a maybe then remove it */
414 FOR_EACH_PTR(maybe_stack
, tmp
) {
415 remove_pool(false_stack
, tmp
->pool
);
416 remove_pool(true_stack
, tmp
->pool
);
417 } END_FOR_EACH_PTR(tmp
);
419 /* if it's both true and false remove it from both */
420 FOR_EACH_PTR(*true_stack
, tmp
) {
421 if (remove_pool(false_stack
, tmp
->pool
))
422 DELETE_CURRENT_PTR(tmp
);
423 } END_FOR_EACH_PTR(tmp
);
426 static int sm_in_keep_leafs(struct sm_state
*sm
, const struct state_list
*keep_gates
)
428 struct sm_state
*tmp
, *old
;
430 FOR_EACH_PTR(keep_gates
, tmp
) {
433 old
= get_sm_state_stree(tmp
->pool
, sm
->owner
, sm
->name
, sm
->sym
);
438 } END_FOR_EACH_PTR(tmp
);
442 static int going_too_slow(void)
444 static void *printed
;
446 if (out_of_memory()) {
447 implications_off
= true;
451 if (time_parsing_function() < 60) {
452 implications_off
= false;
456 if (!__inline_fn
&& printed
!= cur_func_sym
) {
457 sm_perror("turning off implications after 60 seconds");
458 printed
= cur_func_sym
;
460 implications_off
= true;
464 static char *sm_state_info(struct sm_state
*sm
)
466 static char buf
[512];
469 n
+= snprintf(buf
+ n
, sizeof(buf
) - n
, "[stree %d line %d] ",
470 get_stree_id(sm
->pool
), sm
->line
);
471 if (n
>= sizeof(buf
))
473 n
+= snprintf(buf
+ n
, sizeof(buf
) - n
, "%s ", show_sm(sm
));
474 if (n
>= sizeof(buf
))
476 n
+= snprintf(buf
+ n
, sizeof(buf
) - n
, "left = %s [stree %d] ",
477 sm
->left
? sm
->left
->state
->name
: "<none>",
478 sm
->left
? get_stree_id(sm
->left
->pool
) : -1);
479 if (n
>= sizeof(buf
))
481 n
+= snprintf(buf
+ n
, sizeof(buf
) - n
, "right = %s [stree %d]",
482 sm
->right
? sm
->right
->state
->name
: "<none>",
483 sm
->right
? get_stree_id(sm
->right
->pool
) : -1);
488 * NOTE: If a state is in both the keep stack and the remove stack then that is
489 * a bug. Only add states which are definitely true or definitely false. If
490 * you have a leaf state that could be both true and false, then create a fake
491 * split history where one side is true and one side is false. Otherwise, if
492 * you can't do that, then don't add it to either list.
494 #define RECURSE_LIMIT 300
495 struct sm_state
*filter_pools(struct sm_state
*sm
,
496 const struct state_list
*remove_stack
,
497 const struct state_list
*keep_stack
,
498 int *modified
, int *recurse_cnt
,
499 struct timeval
*start
, int *skip
, int *bail
)
501 struct sm_state
*ret
= NULL
;
502 struct sm_state
*left
;
503 struct sm_state
*right
;
505 struct timeval now
, diff
;
511 gettimeofday(&now
, NULL
);
512 timersub(&now
, start
, &diff
);
513 if (diff
.tv_sec
>= 3) {
514 DIMPLIED("%s: implications taking too long: %s\n", __func__
, sm_state_info(sm
));
518 if ((*recurse_cnt
)++ > RECURSE_LIMIT
) {
519 DIMPLIED("%s: recursed too far: %s\n", __func__
, sm_state_info(sm
));
524 if (pool_in_pools(sm
->pool
, remove_stack
)) {
525 DIMPLIED("%s: remove: %s\n", __func__
, sm_state_info(sm
));
530 if (!is_merged(sm
) || pool_in_pools(sm
->pool
, keep_stack
) || sm_in_keep_leafs(sm
, keep_stack
)) {
531 DIMPLIED("%s: keep %s (%s, %s, %s): %s\n", __func__
, sm
->state
->name
,
532 is_merged(sm
) ? "merged" : "not merged",
533 pool_in_pools(sm
->pool
, keep_stack
) ? "in keep pools" : "not in keep pools",
534 sm_in_keep_leafs(sm
, keep_stack
) ? "reachable keep leaf" : "no keep leaf",
539 left
= filter_pools(sm
->left
, remove_stack
, keep_stack
, &removed
, recurse_cnt
, start
, skip
, bail
);
540 right
= filter_pools(sm
->right
, remove_stack
, keep_stack
, &removed
, recurse_cnt
, start
, skip
, bail
);
544 DIMPLIED("%s: kept all: %s\n", __func__
, sm_state_info(sm
));
548 if (!left
&& !right
) {
549 DIMPLIED("%s: removed all: %s\n", __func__
, sm_state_info(sm
));
554 ret
= clone_sm(right
);
559 ret
= clone_sm(left
);
564 if (left
->sym
!= sm
->sym
|| strcmp(left
->name
, sm
->name
) != 0) {
565 left
= clone_sm(left
);
567 left
->name
= sm
->name
;
569 if (right
->sym
!= sm
->sym
|| strcmp(right
->name
, sm
->name
) != 0) {
570 right
= clone_sm(right
);
571 right
->sym
= sm
->sym
;
572 right
->name
= sm
->name
;
574 ret
= merge_sm_states(left
, right
);
577 ret
->pool
= sm
->pool
;
579 DIMPLIED("%s: partial: %s\n", __func__
, sm_state_info(sm
));
583 static struct stree
*filter_stack(struct sm_state
*gate_sm
,
584 struct stree
*pre_stree
,
585 const struct state_list
*remove_stack
,
586 const struct state_list
*keep_stack
)
588 struct stree
*ret
= NULL
;
589 struct sm_state
*tmp
;
590 struct sm_state
*filtered_sm
;
593 struct timeval start
;
600 gettimeofday(&start
, NULL
);
601 FOR_EACH_SM(pre_stree
, tmp
) {
602 if (!tmp
->merged
|| sm_in_keep_leafs(tmp
, keep_stack
))
607 filtered_sm
= filter_pools(tmp
, remove_stack
, keep_stack
, &modified
, &recurse_cnt
, &start
, &skip
, &bail
);
608 if (going_too_slow())
611 return ret
; /* Return the implications we figured out before time ran out. */
614 if (skip
|| !filtered_sm
|| !modified
)
616 /* the assignments here are for borrowed implications */
617 filtered_sm
->name
= tmp
->name
;
618 filtered_sm
->sym
= tmp
->sym
;
619 avl_insert(&ret
, filtered_sm
);
620 } END_FOR_EACH_SM(tmp
);
624 static void separate_and_filter(struct sm_state
*sm
, int comparison
, struct range_list
*rl
,
625 struct stree
*pre_stree
,
626 struct stree
**true_states
,
627 struct stree
**false_states
,
630 struct state_list
*true_stack
= NULL
;
631 struct state_list
*false_stack
= NULL
;
632 struct timeval time_before
;
633 struct timeval time_after
;
636 gettimeofday(&time_before
, NULL
);
638 DIMPLIED("checking implications: (%s (%s) %s %s)\n",
639 sm
->name
, sm
->state
->name
, show_comparison(comparison
), show_rl(rl
));
641 if (!is_merged(sm
)) {
642 DIMPLIED("%d '%s' from line %d is not merged.\n", get_lineno(), sm
->name
, sm
->line
);
646 separate_pools(sm
, comparison
, rl
, &true_stack
, &false_stack
, NULL
, mixed
);
651 FOR_EACH_PTR(true_stack
, sm
) {
652 sm_msg("TRUE POOL: %p", sm
->pool
);
653 } END_FOR_EACH_PTR(sm
);
655 FOR_EACH_PTR(false_stack
, sm
) {
656 sm_msg("FALSE POOL: %p", sm
->pool
);
657 } END_FOR_EACH_PTR(sm
);
660 DIMPLIED("filtering true stack.\n");
661 *true_states
= filter_stack(sm
, pre_stree
, false_stack
, true_stack
);
662 DIMPLIED("filtering false stack.\n");
663 *false_states
= filter_stack(sm
, pre_stree
, true_stack
, false_stack
);
664 free_slist(&true_stack
);
665 free_slist(&false_stack
);
667 gettimeofday(&time_after
, NULL
);
668 sec
= time_after
.tv_sec
- time_before
.tv_sec
;
670 sm_perror("Function too hairy. Ignoring implications after %d seconds.", sec
);
673 static struct expression
*get_last_expr(struct statement
*stmt
)
675 struct statement
*last
;
677 last
= last_ptr_list((struct ptr_list
*)stmt
->stmts
);
678 if (last
->type
== STMT_EXPRESSION
)
679 return last
->expression
;
681 if (last
->type
== STMT_LABEL
) {
682 if (last
->label_statement
&&
683 last
->label_statement
->type
== STMT_EXPRESSION
)
684 return last
->label_statement
->expression
;
690 static struct expression
*get_left_most_expr(struct expression
*expr
)
692 struct statement
*compound
;
694 compound
= get_expression_statement(expr
);
696 return get_last_expr(compound
);
698 expr
= strip_parens(expr
);
699 if (expr
->type
== EXPR_ASSIGNMENT
)
700 return get_left_most_expr(expr
->left
);
704 static int is_merged_expr(struct expression
*expr
)
709 if (get_value(expr
, &dummy
))
711 sm
= get_sm_state_expr(SMATCH_EXTRA
, expr
);
719 static void delete_gate_sm_equiv(struct stree
**stree
, const char *name
, struct symbol
*sym
)
721 struct smatch_state
*state
;
722 struct relation
*rel
;
724 state
= get_state(SMATCH_EXTRA
, name
, sym
);
727 FOR_EACH_PTR(estate_related(state
), rel
) {
728 delete_state_stree(stree
, SMATCH_EXTRA
, rel
->name
, rel
->sym
);
729 } END_FOR_EACH_PTR(rel
);
732 static void delete_gate_sm(struct stree
**stree
, const char *name
, struct symbol
*sym
)
734 delete_state_stree(stree
, SMATCH_EXTRA
, name
, sym
);
737 static int handle_comparison(struct expression
*expr
,
738 struct stree
**implied_true
,
739 struct stree
**implied_false
)
741 struct sm_state
*sm
= NULL
;
742 struct range_list
*rl
= NULL
;
743 struct expression
*left
;
744 struct expression
*right
;
746 int comparison
= expr
->op
;
749 left
= get_left_most_expr(expr
->left
);
750 right
= get_left_most_expr(expr
->right
);
752 if (is_merged_expr(left
)) {
753 sm
= get_sm_state_expr(SMATCH_EXTRA
, left
);
754 get_implied_rl(right
, &rl
);
755 } else if (is_merged_expr(right
)) {
756 sm
= get_sm_state_expr(SMATCH_EXTRA
, right
);
757 get_implied_rl(left
, &rl
);
758 comparison
= flip_comparison(comparison
);
764 type
= get_type(expr
);
767 if (type_positive_bits(rl_type(rl
)) > type_positive_bits(type
))
769 if (type_positive_bits(type
) < 31)
771 rl
= cast_rl(type
, rl
);
773 separate_and_filter(sm
, comparison
, rl
, __get_cur_stree(), implied_true
, implied_false
, &mixed
);
775 delete_gate_sm_equiv(implied_true
, sm
->name
, sm
->sym
);
776 delete_gate_sm_equiv(implied_false
, sm
->name
, sm
->sym
);
778 delete_gate_sm(implied_true
, sm
->name
, sm
->sym
);
779 delete_gate_sm(implied_false
, sm
->name
, sm
->sym
);
785 static int handle_zero_comparison(struct expression
*expr
,
786 struct stree
**implied_true
,
787 struct stree
**implied_false
)
795 if (expr
->type
== EXPR_POSTOP
)
796 expr
= strip_expr(expr
->unop
);
798 if (expr
->type
== EXPR_ASSIGNMENT
) {
799 /* most of the time ->pools will be empty here because we
800 just set the state, but if have assigned a conditional
801 function there are implications. */
805 name
= expr_to_var_sym(expr
, &sym
);
808 sm
= get_sm_state(SMATCH_EXTRA
, name
, sym
);
809 if (!sm
|| !sm
->merged
)
812 separate_and_filter(sm
, SPECIAL_NOTEQUAL
, tmp_range_list(estate_type(sm
->state
), 0), __get_cur_stree(), implied_true
, implied_false
, &mixed
);
813 delete_gate_sm_equiv(implied_true
, sm
->name
, sm
->sym
);
814 delete_gate_sm_equiv(implied_false
, sm
->name
, sm
->sym
);
816 delete_gate_sm(implied_true
, sm
->name
, sm
->sym
);
817 delete_gate_sm(implied_false
, sm
->name
, sm
->sym
);
826 static int handled_by_comparison_hook(struct expression
*expr
,
827 struct stree
**implied_true
,
828 struct stree
**implied_false
)
830 struct sm_state
*sm
, *true_sm
, *false_sm
;
831 struct state_list
*true_stack
= NULL
;
832 struct state_list
*false_stack
= NULL
;
833 struct stree
*pre_stree
;
835 sm
= comparison_implication_hook(expr
, &true_stack
, &false_stack
);
839 pre_stree
= clone_stree(__get_cur_stree());
841 *implied_true
= filter_stack(sm
, pre_stree
, false_stack
, true_stack
);
842 *implied_false
= filter_stack(sm
, pre_stree
, true_stack
, false_stack
);
844 true_sm
= get_sm_state_stree(*implied_true
, sm
->owner
, sm
->name
, sm
->sym
);
845 false_sm
= get_sm_state_stree(*implied_false
, sm
->owner
, sm
->name
, sm
->sym
);
846 if (true_sm
&& strcmp(true_sm
->state
->name
, "unknown") == 0)
847 delete_state_stree(implied_true
, sm
->owner
, sm
->name
, sm
->sym
);
848 if (false_sm
&& strcmp(false_sm
->state
->name
, "unknown") == 0)
849 delete_state_stree(implied_false
, sm
->owner
, sm
->name
, sm
->sym
);
851 free_stree(&pre_stree
);
852 free_slist(&true_stack
);
853 free_slist(&false_stack
);
858 static int handled_by_extra_states(struct expression
*expr
,
859 struct stree
**implied_true
,
860 struct stree
**implied_false
)
864 /* If the expression is known then it has no implications. */
865 if (get_implied_value(expr
, &sval
))
868 if (expr
->type
== EXPR_COMPARE
)
869 return handle_comparison(expr
, implied_true
, implied_false
);
871 return handle_zero_comparison(expr
, implied_true
, implied_false
);
874 static int handled_by_parsed_conditions(struct expression
*expr
,
875 struct stree
**implied_true
,
876 struct stree
**implied_false
)
878 struct state_list
*true_stack
= NULL
;
879 struct state_list
*false_stack
= NULL
;
880 struct stree
*pre_stree
;
883 sm
= parsed_condition_implication_hook(expr
, &true_stack
, &false_stack
);
887 pre_stree
= clone_stree(__get_cur_stree());
889 *implied_true
= filter_stack(sm
, pre_stree
, false_stack
, true_stack
);
890 *implied_false
= filter_stack(sm
, pre_stree
, true_stack
, false_stack
);
892 free_stree(&pre_stree
);
893 free_slist(&true_stack
);
894 free_slist(&false_stack
);
899 static int handled_by_stored_conditions(struct expression
*expr
,
900 struct stree
**implied_true
,
901 struct stree
**implied_false
)
903 struct state_list
*true_stack
= NULL
;
904 struct state_list
*false_stack
= NULL
;
905 struct stree
*pre_stree
;
908 sm
= stored_condition_implication_hook(expr
, &true_stack
, &false_stack
);
912 pre_stree
= clone_stree(__get_cur_stree());
914 *implied_true
= filter_stack(sm
, pre_stree
, false_stack
, true_stack
);
915 *implied_false
= filter_stack(sm
, pre_stree
, true_stack
, false_stack
);
917 free_stree(&pre_stree
);
918 free_slist(&true_stack
);
919 free_slist(&false_stack
);
924 static struct stree
*saved_implied_true
;
925 static struct stree
*saved_implied_false
;
926 static struct stree
*extra_saved_implied_true
;
927 static struct stree
*extra_saved_implied_false
;
929 static void separate_implication_states(struct stree
**implied_true
,
930 struct stree
**implied_false
,
935 /* We process these states later to preserve the implications. */
936 FOR_EACH_SM(*implied_true
, sm
) {
937 if (sm
->owner
== owner
)
938 overwrite_sm_state_stree(&extra_saved_implied_true
, sm
);
939 } END_FOR_EACH_SM(sm
);
940 FOR_EACH_SM(extra_saved_implied_true
, sm
) {
941 delete_state_stree(implied_true
, sm
->owner
, sm
->name
, sm
->sym
);
942 } END_FOR_EACH_SM(sm
);
944 FOR_EACH_SM(*implied_false
, sm
) {
945 if (sm
->owner
== owner
)
946 overwrite_sm_state_stree(&extra_saved_implied_false
, sm
);
947 } END_FOR_EACH_SM(sm
);
948 FOR_EACH_SM(extra_saved_implied_false
, sm
) {
949 delete_state_stree(implied_false
, sm
->owner
, sm
->name
, sm
->sym
);
950 } END_FOR_EACH_SM(sm
);
953 static void get_tf_states(struct expression
*expr
,
954 struct stree
**implied_true
,
955 struct stree
**implied_false
)
957 if (handled_by_parsed_conditions(expr
, implied_true
, implied_false
))
960 if (handled_by_comparison_hook(expr
, implied_true
, implied_false
)) {
961 separate_implication_states(implied_true
, implied_false
, comparison_id
);
965 if (handled_by_extra_states(expr
, implied_true
, implied_false
)) {
966 separate_implication_states(implied_true
, implied_false
, SMATCH_EXTRA
);
970 if (handled_by_stored_conditions(expr
, implied_true
, implied_false
))
974 static void save_implications_hook(struct expression
*expr
)
976 if (going_too_slow())
978 get_tf_states(expr
, &saved_implied_true
, &saved_implied_false
);
981 static void set_implied_states(struct expression
*expr
)
985 if ((full_debug
|| implied_debug
) &&
986 (expr
|| saved_implied_true
|| saved_implied_false
)) {
989 name
= expr_to_str(expr
);
990 printf("These are the implied states for the true path: (%s)\n", name
);
991 __print_stree(saved_implied_true
);
992 printf("These are the implied states for the false path: (%s)\n", name
);
993 __print_stree(saved_implied_false
);
997 FOR_EACH_SM(saved_implied_true
, sm
) {
998 __set_true_false_sm(sm
, NULL
);
999 } END_FOR_EACH_SM(sm
);
1000 free_stree(&saved_implied_true
);
1002 FOR_EACH_SM(saved_implied_false
, sm
) {
1003 __set_true_false_sm(NULL
, sm
);
1004 } END_FOR_EACH_SM(sm
);
1005 free_stree(&saved_implied_false
);
1008 static void set_extra_implied_states(struct expression
*expr
)
1010 saved_implied_true
= extra_saved_implied_true
;
1011 saved_implied_false
= extra_saved_implied_false
;
1012 extra_saved_implied_true
= NULL
;
1013 extra_saved_implied_false
= NULL
;
1014 set_implied_states(NULL
);
1017 void param_limit_implications(struct expression
*expr
, int param
, char *key
, char *value
, struct stree
**implied
)
1019 struct expression
*orig_expr
, *arg
;
1020 struct symbol
*compare_type
;
1023 struct sm_state
*sm
;
1024 struct sm_state
*tmp
;
1025 struct stree
*implied_true
= NULL
;
1026 struct stree
*implied_false
= NULL
;
1027 struct range_list
*orig
, *limit
;
1028 char *left_name
= NULL
;
1029 struct symbol
*left_sym
= NULL
;
1032 if (time_parsing_function() > 40)
1036 while (expr
->type
== EXPR_ASSIGNMENT
)
1037 expr
= strip_expr(expr
->right
);
1038 if (expr
->type
!= EXPR_CALL
)
1041 arg
= get_argument_from_call_expr(expr
->args
, param
);
1045 arg
= strip_parens(arg
);
1046 while (arg
->type
== EXPR_ASSIGNMENT
&& arg
->op
== '=')
1047 arg
= strip_parens(arg
->left
);
1049 name
= get_variable_from_key(arg
, key
, &sym
);
1053 sm
= get_sm_state(SMATCH_EXTRA
, name
, sym
);
1054 if (!sm
|| !sm
->merged
)
1057 if (strcmp(key
, "$") == 0)
1058 compare_type
= get_arg_type(expr
->fn
, param
);
1060 compare_type
= get_member_type_from_key(arg
, key
);
1062 orig
= estate_rl(sm
->state
);
1063 orig
= cast_rl(compare_type
, orig
);
1065 call_results_to_rl(expr
, compare_type
, value
, &limit
);
1067 separate_and_filter(sm
, PARAM_LIMIT
, limit
, __get_cur_stree(), &implied_true
, &implied_false
, &mixed
);
1069 if (orig_expr
->type
== EXPR_ASSIGNMENT
)
1070 left_name
= expr_to_var_sym(orig_expr
->left
, &left_sym
);
1072 FOR_EACH_SM(implied_true
, tmp
) {
1074 * What we're trying to do here is preserve the sm state so that
1075 * smatch extra doesn't create a new sm state when it parses the
1078 if (!mixed
&& tmp
->sym
== sym
&&
1079 strcmp(tmp
->name
, name
) == 0 &&
1080 (!left_name
|| strcmp(left_name
, name
) != 0)) {
1081 overwrite_sm_state_stree(implied
, tmp
);
1085 // TODO why can't this just be __set_sm()? Or alternatively,
1086 // why is this not written to the "implied" stree?
1087 __set_sm_fake_stree(tmp
);
1088 } END_FOR_EACH_SM(tmp
);
1090 free_stree(&implied_true
);
1091 free_stree(&implied_false
);
1096 struct stree
*__implied_case_stree(struct expression
*switch_expr
,
1097 struct range_list
*rl
,
1098 struct range_list_stack
**remaining_cases
,
1099 struct stree
**raw_stree
)
1103 struct var_sym_list
*vsl
;
1104 struct sm_state
*sm
;
1105 struct stree
*true_states
= NULL
;
1106 struct stree
*false_states
= NULL
;
1107 struct stree
*extra_states
;
1108 struct stree
*ret
= clone_stree(*raw_stree
);
1110 name
= expr_to_chunk_sym_vsl(switch_expr
, &sym
, &vsl
);
1113 filter_top_rl(remaining_cases
, rl
);
1115 rl
= clone_rl(top_rl(*remaining_cases
));
1118 sm
= get_sm_state_stree(*raw_stree
, SMATCH_EXTRA
, name
, sym
);
1120 separate_and_filter(sm
, SPECIAL_EQUAL
, rl
, *raw_stree
, &true_states
, &false_states
, NULL
);
1123 __push_fake_cur_stree();
1126 set_extra_nomod_vsl(name
, sym
, vsl
, NULL
, alloc_estate_rl(rl
));
1127 __pass_case_to_client(switch_expr
, rl
);
1128 extra_states
= __pop_fake_cur_stree();
1129 overwrite_stree(extra_states
, &true_states
);
1130 overwrite_stree(true_states
, &ret
);
1131 free_stree(&extra_states
);
1132 free_stree(&true_states
);
1133 free_stree(&false_states
);
1139 static void match_end_func(struct symbol
*sym
)
1143 implied_debug_msg
= NULL
;
1146 static void get_tf_stacks_from_pool(struct sm_state
*gate_sm
,
1147 struct sm_state
*pool_sm
,
1148 struct state_list
**true_stack
,
1149 struct state_list
**false_stack
)
1151 struct sm_state
*tmp
;
1152 int possibly_true
= 0;
1157 if (strcmp(gate_sm
->state
->name
, pool_sm
->state
->name
) == 0) {
1158 add_ptr_list(true_stack
, pool_sm
);
1162 FOR_EACH_PTR(gate_sm
->possible
, tmp
) {
1163 if (strcmp(tmp
->state
->name
, pool_sm
->state
->name
) == 0) {
1167 } END_FOR_EACH_PTR(tmp
);
1169 if (!possibly_true
) {
1170 add_ptr_list(false_stack
, gate_sm
);
1174 get_tf_stacks_from_pool(gate_sm
->left
, pool_sm
, true_stack
, false_stack
);
1175 get_tf_stacks_from_pool(gate_sm
->right
, pool_sm
, true_stack
, false_stack
);
1179 * The situation is we have a SMATCH_EXTRA state and we want to break it into
1180 * each of the ->possible states and find the implications of each. The caller
1181 * has to use __push_fake_cur_stree() to preserve the correct states so they
1182 * can be restored later.
1184 void overwrite_states_using_pool(struct sm_state
*gate_sm
, struct sm_state
*pool_sm
)
1186 struct state_list
*true_stack
= NULL
;
1187 struct state_list
*false_stack
= NULL
;
1188 struct stree
*pre_stree
;
1189 struct stree
*implied_true
;
1190 struct sm_state
*tmp
;
1195 get_tf_stacks_from_pool(gate_sm
, pool_sm
, &true_stack
, &false_stack
);
1197 pre_stree
= clone_stree(__get_cur_stree());
1199 implied_true
= filter_stack(gate_sm
, pre_stree
, false_stack
, true_stack
);
1201 free_stree(&pre_stree
);
1202 free_slist(&true_stack
);
1203 free_slist(&false_stack
);
1205 FOR_EACH_SM(implied_true
, tmp
) {
1206 set_state(tmp
->owner
, tmp
->name
, tmp
->sym
, tmp
->state
);
1207 } END_FOR_EACH_SM(tmp
);
1209 free_stree(&implied_true
);
1212 int assume(struct expression
*expr
)
1214 int orig_final_pass
= final_pass
;
1218 __push_fake_cur_stree();
1219 __split_whole_condition(expr
);
1220 final_pass
= orig_final_pass
;
1226 void end_assume(void)
1228 __discard_false_states();
1229 __free_fake_cur_stree();
1232 int impossible_assumption(struct expression
*left
, int op
, sval_t sval
)
1234 struct expression
*value
;
1235 struct expression
*comparison
;
1238 value
= value_expr(sval
.value
);
1239 comparison
= compare_expression(left
, op
, value
);
1241 if (!assume(comparison
))
1243 ret
= is_impossible_path();
1249 void __extra_match_condition(struct expression
*expr
);
1250 void __comparison_match_condition(struct expression
*expr
);
1251 void __stored_condition(struct expression
*expr
);
1252 void register_implications(int id
)
1254 add_hook(&save_implications_hook
, CONDITION_HOOK
);
1255 add_hook(&set_implied_states
, CONDITION_HOOK
);
1256 add_hook(&__extra_match_condition
, CONDITION_HOOK
);
1257 add_hook(&__comparison_match_condition
, CONDITION_HOOK
);
1258 add_hook(&set_extra_implied_states
, CONDITION_HOOK
);
1259 add_hook(&__stored_condition
, CONDITION_HOOK
);
1260 add_hook(&match_end_func
, END_FUNC_HOOK
);