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 (comparison
!= PARAM_LIMIT
&& !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
;
201 sm
->right
= false_sm
;
207 * add_pool() adds a slist to *pools. If the slist has already been
208 * added earlier then it doesn't get added a second time.
210 void add_pool(struct state_list
**pools
, struct sm_state
*new)
212 struct sm_state
*tmp
;
214 FOR_EACH_PTR(*pools
, tmp
) {
215 if (tmp
->pool
< new->pool
)
217 else if (tmp
->pool
== new->pool
) {
220 INSERT_CURRENT(new, tmp
);
223 } END_FOR_EACH_PTR(tmp
);
224 add_ptr_list(pools
, new);
227 static int pool_in_pools(struct stree
*pool
,
228 const struct state_list
*slist
)
230 struct sm_state
*tmp
;
232 FOR_EACH_PTR(slist
, tmp
) {
235 if (tmp
->pool
== pool
)
237 } END_FOR_EACH_PTR(tmp
);
241 static int remove_pool(struct state_list
**pools
, struct stree
*remove
)
243 struct sm_state
*tmp
;
246 FOR_EACH_PTR(*pools
, tmp
) {
247 if (tmp
->pool
== remove
) {
248 DELETE_CURRENT_PTR(tmp
);
251 } END_FOR_EACH_PTR(tmp
);
256 static bool possibly_true_helper(struct range_list
*var_rl
, int comparison
, struct range_list
*rl
)
258 if (comparison
== PARAM_LIMIT
) {
259 struct range_list
*intersect
;
261 intersect
= rl_intersection(var_rl
, rl
);
266 return possibly_true_rl(var_rl
, comparison
, rl
);
269 static bool possibly_false_helper(struct range_list
*var_rl
, int comparison
, struct range_list
*rl
)
271 if (comparison
== PARAM_LIMIT
) {
272 struct range_list
*intersect
;
274 intersect
= rl_intersection(var_rl
, rl
);
275 /* if it's not equiv then it's possibly false */
276 return !rl_equiv(var_rl
, intersect
);
278 return possibly_false_rl(var_rl
, comparison
, rl
);
282 * If 'foo' == 99 add it that pool to the true pools. If it's false, add it to
283 * the false pools. If we're not sure, then we don't add it to either.
285 static void do_compare(struct sm_state
*sm
, int comparison
, struct range_list
*rl
,
286 struct state_list
**true_stack
,
287 struct state_list
**maybe_stack
,
288 struct state_list
**false_stack
,
289 int *mixed
, struct sm_state
*gate_sm
)
293 struct range_list
*var_rl
;
298 var_rl
= cast_rl(rl_type(rl
), estate_rl(sm
->state
));
300 istrue
= !possibly_false_helper(var_rl
, comparison
, rl
);
301 isfalse
= !possibly_true_helper(var_rl
, comparison
, rl
);
303 print_debug_tf(sm
, istrue
, isfalse
);
305 /* give up if we have borrowed implications (smatch_equiv.c) */
306 if (sm
->sym
!= gate_sm
->sym
||
307 strcmp(sm
->name
, gate_sm
->name
) != 0) {
312 if (mixed
&& !*mixed
&& !is_merged(sm
) && !istrue
&& !isfalse
) {
313 if (!create_fake_history(sm
, comparison
, rl
))
318 add_pool(true_stack
, sm
);
320 add_pool(false_stack
, sm
);
322 add_pool(maybe_stack
, sm
);
325 static int is_checked(struct state_list
*checked
, struct sm_state
*sm
)
327 struct sm_state
*tmp
;
329 FOR_EACH_PTR(checked
, tmp
) {
332 } END_FOR_EACH_PTR(tmp
);
338 * Example code: if (foo == 99) {
340 * Say 'foo' is a merged state that has many possible values. It is the combination
341 * of merges. separate_pools() iterates through the pools recursively and calls
342 * do_compare() for each time 'foo' was set.
344 static void __separate_pools(struct sm_state
*sm
, int comparison
, struct range_list
*rl
,
345 struct state_list
**true_stack
,
346 struct state_list
**maybe_stack
,
347 struct state_list
**false_stack
,
348 struct state_list
**checked
, int *mixed
, struct sm_state
*gate_sm
,
349 struct timeval
*start_time
)
351 int free_checked
= 0;
352 struct state_list
*checked_states
= NULL
;
353 struct timeval now
, diff
;
358 gettimeofday(&now
, NULL
);
359 timersub(&now
, start_time
, &diff
);
360 if (diff
.tv_sec
>= 1) {
362 sm_msg("debug: %s: implications taking too long. (%s %s %s)",
363 __func__
, sm
->state
->name
, show_comparison(comparison
), show_rl(rl
));
369 if (checked
== NULL
) {
370 checked
= &checked_states
;
373 if (is_checked(*checked
, sm
))
375 add_ptr_list(checked
, sm
);
377 do_compare(sm
, comparison
, rl
, true_stack
, maybe_stack
, false_stack
, mixed
, gate_sm
);
379 __separate_pools(sm
->left
, comparison
, rl
, true_stack
, maybe_stack
, false_stack
, checked
, mixed
, gate_sm
, start_time
);
380 __separate_pools(sm
->right
, comparison
, rl
, true_stack
, maybe_stack
, false_stack
, checked
, mixed
, gate_sm
, start_time
);
385 static void separate_pools(struct sm_state
*sm
, int comparison
, struct range_list
*rl
,
386 struct state_list
**true_stack
,
387 struct state_list
**false_stack
,
388 struct state_list
**checked
, int *mixed
)
390 struct state_list
*maybe_stack
= NULL
;
391 struct sm_state
*tmp
;
392 struct timeval start_time
;
395 gettimeofday(&start_time
, NULL
);
396 __separate_pools(sm
, comparison
, rl
, true_stack
, &maybe_stack
, false_stack
, checked
, mixed
, sm
, &start_time
);
401 FOR_EACH_PTR(*true_stack
, sm
) {
402 sm_msg("TRUE %s [stree %d %p]", show_sm(sm
), get_stree_id(sm
->pool
), sm
->pool
);
403 } END_FOR_EACH_PTR(sm
);
405 FOR_EACH_PTR(maybe_stack
, sm
) {
406 sm_msg("MAYBE %s %s[stree %d %p]",
407 show_sm(sm
), sm
->merged
? "(merged) ": "", get_stree_id(sm
->pool
), sm
->pool
);
408 } END_FOR_EACH_PTR(sm
);
410 FOR_EACH_PTR(*false_stack
, sm
) {
411 sm_msg("FALSE %s [stree %d %p]", show_sm(sm
), get_stree_id(sm
->pool
), sm
->pool
);
412 } END_FOR_EACH_PTR(sm
);
414 /* if it's a maybe then remove it */
415 FOR_EACH_PTR(maybe_stack
, tmp
) {
416 remove_pool(false_stack
, tmp
->pool
);
417 remove_pool(true_stack
, tmp
->pool
);
418 } END_FOR_EACH_PTR(tmp
);
420 /* if it's both true and false remove it from both */
421 FOR_EACH_PTR(*true_stack
, tmp
) {
422 if (remove_pool(false_stack
, tmp
->pool
))
423 DELETE_CURRENT_PTR(tmp
);
424 } END_FOR_EACH_PTR(tmp
);
427 static int sm_in_keep_leafs(struct sm_state
*sm
, const struct state_list
*keep_gates
)
429 struct sm_state
*tmp
, *old
;
431 FOR_EACH_PTR(keep_gates
, tmp
) {
434 old
= get_sm_state_stree(tmp
->pool
, sm
->owner
, sm
->name
, sm
->sym
);
439 } END_FOR_EACH_PTR(tmp
);
443 static int going_too_slow(void)
445 static void *printed
;
447 if (out_of_memory()) {
448 implications_off
= true;
452 if (time_parsing_function() < 60) {
453 implications_off
= false;
457 if (!__inline_fn
&& printed
!= cur_func_sym
) {
458 sm_perror("turning off implications after 60 seconds");
459 printed
= cur_func_sym
;
461 implications_off
= true;
465 static char *sm_state_info(struct sm_state
*sm
)
467 static char buf
[512];
470 n
+= snprintf(buf
+ n
, sizeof(buf
) - n
, "[stree %d line %d] ",
471 get_stree_id(sm
->pool
), sm
->line
);
472 if (n
>= sizeof(buf
))
474 n
+= snprintf(buf
+ n
, sizeof(buf
) - n
, "%s ", show_sm(sm
));
475 if (n
>= sizeof(buf
))
477 n
+= snprintf(buf
+ n
, sizeof(buf
) - n
, "left = %s [stree %d] ",
478 sm
->left
? sm
->left
->state
->name
: "<none>",
479 sm
->left
? get_stree_id(sm
->left
->pool
) : -1);
480 if (n
>= sizeof(buf
))
482 n
+= snprintf(buf
+ n
, sizeof(buf
) - n
, "right = %s [stree %d]",
483 sm
->right
? sm
->right
->state
->name
: "<none>",
484 sm
->right
? get_stree_id(sm
->right
->pool
) : -1);
489 * NOTE: If a state is in both the keep stack and the remove stack then that is
490 * a bug. Only add states which are definitely true or definitely false. If
491 * you have a leaf state that could be both true and false, then create a fake
492 * split history where one side is true and one side is false. Otherwise, if
493 * you can't do that, then don't add it to either list.
495 #define RECURSE_LIMIT 300
496 struct sm_state
*filter_pools(struct sm_state
*sm
,
497 const struct state_list
*remove_stack
,
498 const struct state_list
*keep_stack
,
499 int *modified
, int *recurse_cnt
,
500 struct timeval
*start
, int *skip
, int *bail
)
502 struct sm_state
*ret
= NULL
;
503 struct sm_state
*left
;
504 struct sm_state
*right
;
506 struct timeval now
, diff
;
512 gettimeofday(&now
, NULL
);
513 timersub(&now
, start
, &diff
);
514 if (diff
.tv_sec
>= 3) {
515 DIMPLIED("%s: implications taking too long: %s\n", __func__
, sm_state_info(sm
));
519 if ((*recurse_cnt
)++ > RECURSE_LIMIT
) {
520 DIMPLIED("%s: recursed too far: %s\n", __func__
, sm_state_info(sm
));
525 if (pool_in_pools(sm
->pool
, remove_stack
)) {
526 DIMPLIED("%s: remove: %s\n", __func__
, sm_state_info(sm
));
531 if (!is_merged(sm
) || pool_in_pools(sm
->pool
, keep_stack
) || sm_in_keep_leafs(sm
, keep_stack
)) {
532 DIMPLIED("%s: keep %s (%s, %s, %s): %s\n", __func__
, sm
->state
->name
,
533 is_merged(sm
) ? "merged" : "not merged",
534 pool_in_pools(sm
->pool
, keep_stack
) ? "in keep pools" : "not in keep pools",
535 sm_in_keep_leafs(sm
, keep_stack
) ? "reachable keep leaf" : "no keep leaf",
540 left
= filter_pools(sm
->left
, remove_stack
, keep_stack
, &removed
, recurse_cnt
, start
, skip
, bail
);
541 right
= filter_pools(sm
->right
, remove_stack
, keep_stack
, &removed
, recurse_cnt
, start
, skip
, bail
);
545 DIMPLIED("%s: kept all: %s\n", __func__
, sm_state_info(sm
));
549 if (!left
&& !right
) {
550 DIMPLIED("%s: removed all: %s\n", __func__
, sm_state_info(sm
));
555 ret
= clone_sm(right
);
560 ret
= clone_sm(left
);
565 if (left
->sym
!= sm
->sym
|| strcmp(left
->name
, sm
->name
) != 0) {
566 left
= clone_sm(left
);
568 left
->name
= sm
->name
;
570 if (right
->sym
!= sm
->sym
|| strcmp(right
->name
, sm
->name
) != 0) {
571 right
= clone_sm(right
);
572 right
->sym
= sm
->sym
;
573 right
->name
= sm
->name
;
575 ret
= merge_sm_states(left
, right
);
578 ret
->pool
= sm
->pool
;
580 DIMPLIED("%s: partial: %s\n", __func__
, sm_state_info(sm
));
584 static struct stree
*filter_stack(struct sm_state
*gate_sm
,
585 struct stree
*pre_stree
,
586 const struct state_list
*remove_stack
,
587 const struct state_list
*keep_stack
)
589 struct stree
*ret
= NULL
;
590 struct sm_state
*tmp
;
591 struct sm_state
*filtered_sm
;
594 struct timeval start
;
601 gettimeofday(&start
, NULL
);
602 FOR_EACH_SM(pre_stree
, tmp
) {
603 if (!tmp
->merged
|| sm_in_keep_leafs(tmp
, keep_stack
))
608 filtered_sm
= filter_pools(tmp
, remove_stack
, keep_stack
, &modified
, &recurse_cnt
, &start
, &skip
, &bail
);
609 if (going_too_slow())
612 return ret
; /* Return the implications we figured out before time ran out. */
615 if (skip
|| !filtered_sm
|| !modified
)
617 /* the assignments here are for borrowed implications */
618 filtered_sm
->name
= tmp
->name
;
619 filtered_sm
->sym
= tmp
->sym
;
620 avl_insert(&ret
, filtered_sm
);
621 } END_FOR_EACH_SM(tmp
);
625 static void separate_and_filter(struct sm_state
*sm
, int comparison
, struct range_list
*rl
,
626 struct stree
*pre_stree
,
627 struct stree
**true_states
,
628 struct stree
**false_states
,
631 struct state_list
*true_stack
= NULL
;
632 struct state_list
*false_stack
= NULL
;
633 struct timeval time_before
;
634 struct timeval time_after
;
637 gettimeofday(&time_before
, NULL
);
639 DIMPLIED("checking implications: (%s (%s) %s %s)\n",
640 sm
->name
, sm
->state
->name
, show_comparison(comparison
), show_rl(rl
));
642 if (!is_merged(sm
)) {
643 DIMPLIED("%d '%s' from line %d is not merged.\n", get_lineno(), sm
->name
, sm
->line
);
647 separate_pools(sm
, comparison
, rl
, &true_stack
, &false_stack
, NULL
, mixed
);
652 FOR_EACH_PTR(true_stack
, sm
) {
653 sm_msg("TRUE POOL: %p", sm
->pool
);
654 } END_FOR_EACH_PTR(sm
);
656 FOR_EACH_PTR(false_stack
, sm
) {
657 sm_msg("FALSE POOL: %p", sm
->pool
);
658 } END_FOR_EACH_PTR(sm
);
661 DIMPLIED("filtering true stack.\n");
662 *true_states
= filter_stack(sm
, pre_stree
, false_stack
, true_stack
);
663 DIMPLIED("filtering false stack.\n");
664 *false_states
= filter_stack(sm
, pre_stree
, true_stack
, false_stack
);
665 free_slist(&true_stack
);
666 free_slist(&false_stack
);
668 gettimeofday(&time_after
, NULL
);
669 sec
= time_after
.tv_sec
- time_before
.tv_sec
;
671 sm_perror("Function too hairy. Ignoring implications after %d seconds.", sec
);
674 static struct expression
*get_last_expr(struct statement
*stmt
)
676 struct statement
*last
;
678 last
= last_ptr_list((struct ptr_list
*)stmt
->stmts
);
679 if (last
->type
== STMT_EXPRESSION
)
680 return last
->expression
;
682 if (last
->type
== STMT_LABEL
) {
683 if (last
->label_statement
&&
684 last
->label_statement
->type
== STMT_EXPRESSION
)
685 return last
->label_statement
->expression
;
691 static struct expression
*get_left_most_expr(struct expression
*expr
)
693 struct statement
*compound
;
695 compound
= get_expression_statement(expr
);
697 return get_last_expr(compound
);
699 expr
= strip_parens(expr
);
700 if (expr
->type
== EXPR_ASSIGNMENT
)
701 return get_left_most_expr(expr
->left
);
705 static int is_merged_expr(struct expression
*expr
)
710 if (get_value(expr
, &dummy
))
712 sm
= get_sm_state_expr(SMATCH_EXTRA
, expr
);
720 static void delete_gate_sm_equiv(struct stree
**stree
, const char *name
, struct symbol
*sym
)
722 struct smatch_state
*state
;
723 struct relation
*rel
;
725 state
= get_state(SMATCH_EXTRA
, name
, sym
);
728 FOR_EACH_PTR(estate_related(state
), rel
) {
729 delete_state_stree(stree
, SMATCH_EXTRA
, rel
->name
, rel
->sym
);
730 } END_FOR_EACH_PTR(rel
);
733 static void delete_gate_sm(struct stree
**stree
, const char *name
, struct symbol
*sym
)
735 delete_state_stree(stree
, SMATCH_EXTRA
, name
, sym
);
738 static int handle_comparison(struct expression
*expr
,
739 struct stree
**implied_true
,
740 struct stree
**implied_false
)
742 struct sm_state
*sm
= NULL
;
743 struct range_list
*rl
= NULL
;
744 struct expression
*left
;
745 struct expression
*right
;
747 int comparison
= expr
->op
;
750 left
= get_left_most_expr(expr
->left
);
751 right
= get_left_most_expr(expr
->right
);
753 if (is_merged_expr(left
)) {
754 sm
= get_sm_state_expr(SMATCH_EXTRA
, left
);
755 get_implied_rl(right
, &rl
);
756 } else if (is_merged_expr(right
)) {
757 sm
= get_sm_state_expr(SMATCH_EXTRA
, right
);
758 get_implied_rl(left
, &rl
);
759 comparison
= flip_comparison(comparison
);
765 type
= get_type(expr
);
768 if (type_positive_bits(rl_type(rl
)) > type_positive_bits(type
))
770 if (type_positive_bits(type
) < 31)
772 rl
= cast_rl(type
, rl
);
774 separate_and_filter(sm
, comparison
, rl
, __get_cur_stree(), implied_true
, implied_false
, &mixed
);
776 delete_gate_sm_equiv(implied_true
, sm
->name
, sm
->sym
);
777 delete_gate_sm_equiv(implied_false
, sm
->name
, sm
->sym
);
779 delete_gate_sm(implied_true
, sm
->name
, sm
->sym
);
780 delete_gate_sm(implied_false
, sm
->name
, sm
->sym
);
786 static int handle_zero_comparison(struct expression
*expr
,
787 struct stree
**implied_true
,
788 struct stree
**implied_false
)
796 if (expr
->type
== EXPR_POSTOP
)
797 expr
= strip_expr(expr
->unop
);
799 if (expr
->type
== EXPR_ASSIGNMENT
) {
800 /* most of the time ->pools will be empty here because we
801 just set the state, but if have assigned a conditional
802 function there are implications. */
806 name
= expr_to_var_sym(expr
, &sym
);
809 sm
= get_sm_state(SMATCH_EXTRA
, name
, sym
);
810 if (!sm
|| !sm
->merged
)
813 separate_and_filter(sm
, SPECIAL_NOTEQUAL
, tmp_range_list(estate_type(sm
->state
), 0), __get_cur_stree(), implied_true
, implied_false
, &mixed
);
814 delete_gate_sm_equiv(implied_true
, sm
->name
, sm
->sym
);
815 delete_gate_sm_equiv(implied_false
, sm
->name
, sm
->sym
);
817 delete_gate_sm(implied_true
, sm
->name
, sm
->sym
);
818 delete_gate_sm(implied_false
, sm
->name
, sm
->sym
);
827 static int handled_by_comparison_hook(struct expression
*expr
,
828 struct stree
**implied_true
,
829 struct stree
**implied_false
)
831 struct sm_state
*sm
, *true_sm
, *false_sm
;
832 struct state_list
*true_stack
= NULL
;
833 struct state_list
*false_stack
= NULL
;
834 struct stree
*pre_stree
;
836 sm
= comparison_implication_hook(expr
, &true_stack
, &false_stack
);
840 pre_stree
= clone_stree(__get_cur_stree());
842 *implied_true
= filter_stack(sm
, pre_stree
, false_stack
, true_stack
);
843 *implied_false
= filter_stack(sm
, pre_stree
, true_stack
, false_stack
);
845 true_sm
= get_sm_state_stree(*implied_true
, sm
->owner
, sm
->name
, sm
->sym
);
846 false_sm
= get_sm_state_stree(*implied_false
, sm
->owner
, sm
->name
, sm
->sym
);
847 if (true_sm
&& strcmp(true_sm
->state
->name
, "unknown") == 0)
848 delete_state_stree(implied_true
, sm
->owner
, sm
->name
, sm
->sym
);
849 if (false_sm
&& strcmp(false_sm
->state
->name
, "unknown") == 0)
850 delete_state_stree(implied_false
, sm
->owner
, sm
->name
, sm
->sym
);
852 free_stree(&pre_stree
);
853 free_slist(&true_stack
);
854 free_slist(&false_stack
);
859 static int handled_by_extra_states(struct expression
*expr
,
860 struct stree
**implied_true
,
861 struct stree
**implied_false
)
865 /* If the expression is known then it has no implications. */
866 if (get_implied_value(expr
, &sval
))
869 if (expr
->type
== EXPR_COMPARE
)
870 return handle_comparison(expr
, implied_true
, implied_false
);
872 return handle_zero_comparison(expr
, implied_true
, implied_false
);
875 static int handled_by_parsed_conditions(struct expression
*expr
,
876 struct stree
**implied_true
,
877 struct stree
**implied_false
)
879 struct state_list
*true_stack
= NULL
;
880 struct state_list
*false_stack
= NULL
;
881 struct stree
*pre_stree
;
884 sm
= parsed_condition_implication_hook(expr
, &true_stack
, &false_stack
);
888 pre_stree
= clone_stree(__get_cur_stree());
890 *implied_true
= filter_stack(sm
, pre_stree
, false_stack
, true_stack
);
891 *implied_false
= filter_stack(sm
, pre_stree
, true_stack
, false_stack
);
893 free_stree(&pre_stree
);
894 free_slist(&true_stack
);
895 free_slist(&false_stack
);
900 static int handled_by_stored_conditions(struct expression
*expr
,
901 struct stree
**implied_true
,
902 struct stree
**implied_false
)
904 struct state_list
*true_stack
= NULL
;
905 struct state_list
*false_stack
= NULL
;
906 struct stree
*pre_stree
;
909 sm
= stored_condition_implication_hook(expr
, &true_stack
, &false_stack
);
913 pre_stree
= clone_stree(__get_cur_stree());
915 *implied_true
= filter_stack(sm
, pre_stree
, false_stack
, true_stack
);
916 *implied_false
= filter_stack(sm
, pre_stree
, true_stack
, false_stack
);
918 free_stree(&pre_stree
);
919 free_slist(&true_stack
);
920 free_slist(&false_stack
);
925 static struct stree
*saved_implied_true
;
926 static struct stree
*saved_implied_false
;
927 static struct stree
*extra_saved_implied_true
;
928 static struct stree
*extra_saved_implied_false
;
930 static void separate_implication_states(struct stree
**implied_true
,
931 struct stree
**implied_false
,
936 /* We process these states later to preserve the implications. */
937 FOR_EACH_SM(*implied_true
, sm
) {
938 if (sm
->owner
== owner
)
939 overwrite_sm_state_stree(&extra_saved_implied_true
, sm
);
940 } END_FOR_EACH_SM(sm
);
941 FOR_EACH_SM(extra_saved_implied_true
, sm
) {
942 delete_state_stree(implied_true
, sm
->owner
, sm
->name
, sm
->sym
);
943 } END_FOR_EACH_SM(sm
);
945 FOR_EACH_SM(*implied_false
, sm
) {
946 if (sm
->owner
== owner
)
947 overwrite_sm_state_stree(&extra_saved_implied_false
, sm
);
948 } END_FOR_EACH_SM(sm
);
949 FOR_EACH_SM(extra_saved_implied_false
, sm
) {
950 delete_state_stree(implied_false
, sm
->owner
, sm
->name
, sm
->sym
);
951 } END_FOR_EACH_SM(sm
);
954 static void get_tf_states(struct expression
*expr
,
955 struct stree
**implied_true
,
956 struct stree
**implied_false
)
958 if (handled_by_parsed_conditions(expr
, implied_true
, implied_false
))
961 if (handled_by_comparison_hook(expr
, implied_true
, implied_false
)) {
962 separate_implication_states(implied_true
, implied_false
, comparison_id
);
966 if (handled_by_extra_states(expr
, implied_true
, implied_false
)) {
967 separate_implication_states(implied_true
, implied_false
, SMATCH_EXTRA
);
971 if (handled_by_stored_conditions(expr
, implied_true
, implied_false
))
975 static void save_implications_hook(struct expression
*expr
)
977 if (going_too_slow())
979 get_tf_states(expr
, &saved_implied_true
, &saved_implied_false
);
982 static void set_implied_states(struct expression
*expr
)
986 if ((full_debug
|| implied_debug
) &&
987 (expr
|| saved_implied_true
|| saved_implied_false
)) {
990 name
= expr_to_str(expr
);
991 printf("These are the implied states for the true path: (%s)\n", name
);
992 __print_stree(saved_implied_true
);
993 printf("These are the implied states for the false path: (%s)\n", name
);
994 __print_stree(saved_implied_false
);
998 FOR_EACH_SM(saved_implied_true
, sm
) {
999 __set_true_false_sm(sm
, NULL
);
1000 } END_FOR_EACH_SM(sm
);
1001 free_stree(&saved_implied_true
);
1003 FOR_EACH_SM(saved_implied_false
, sm
) {
1004 __set_true_false_sm(NULL
, sm
);
1005 } END_FOR_EACH_SM(sm
);
1006 free_stree(&saved_implied_false
);
1009 static void set_extra_implied_states(struct expression
*expr
)
1011 saved_implied_true
= extra_saved_implied_true
;
1012 saved_implied_false
= extra_saved_implied_false
;
1013 extra_saved_implied_true
= NULL
;
1014 extra_saved_implied_false
= NULL
;
1015 set_implied_states(NULL
);
1018 void param_limit_implications(struct expression
*expr
, int param
, char *key
, char *value
, struct stree
**implied
)
1020 struct expression
*orig_expr
, *arg
;
1021 struct symbol
*compare_type
;
1024 struct sm_state
*sm
;
1025 struct sm_state
*tmp
;
1026 struct stree
*implied_true
= NULL
;
1027 struct stree
*implied_false
= NULL
;
1028 struct range_list
*orig
, *limit
;
1029 char *left_name
= NULL
;
1030 struct symbol
*left_sym
= NULL
;
1033 if (time_parsing_function() > 40)
1037 while (expr
->type
== EXPR_ASSIGNMENT
)
1038 expr
= strip_expr(expr
->right
);
1039 if (expr
->type
!= EXPR_CALL
)
1042 arg
= get_argument_from_call_expr(expr
->args
, param
);
1046 arg
= strip_parens(arg
);
1047 while (arg
->type
== EXPR_ASSIGNMENT
&& arg
->op
== '=')
1048 arg
= strip_parens(arg
->left
);
1050 name
= get_variable_from_key(arg
, key
, &sym
);
1054 sm
= get_sm_state(SMATCH_EXTRA
, name
, sym
);
1055 if (!sm
|| !sm
->merged
)
1058 if (strcmp(key
, "$") == 0)
1059 compare_type
= get_arg_type(expr
->fn
, param
);
1061 compare_type
= get_member_type_from_key(arg
, key
);
1063 orig
= estate_rl(sm
->state
);
1064 orig
= cast_rl(compare_type
, orig
);
1066 call_results_to_rl(expr
, compare_type
, value
, &limit
);
1068 separate_and_filter(sm
, PARAM_LIMIT
, limit
, __get_cur_stree(), &implied_true
, &implied_false
, &mixed
);
1070 if (orig_expr
->type
== EXPR_ASSIGNMENT
)
1071 left_name
= expr_to_var_sym(orig_expr
->left
, &left_sym
);
1073 FOR_EACH_SM(implied_true
, tmp
) {
1075 * What we're trying to do here is preserve the sm state so that
1076 * smatch extra doesn't create a new sm state when it parses the
1079 if (!mixed
&& tmp
->sym
== sym
&&
1080 strcmp(tmp
->name
, name
) == 0 &&
1081 (!left_name
|| strcmp(left_name
, name
) != 0)) {
1082 overwrite_sm_state_stree(implied
, tmp
);
1087 } END_FOR_EACH_SM(tmp
);
1089 free_stree(&implied_true
);
1090 free_stree(&implied_false
);
1095 struct stree
*__implied_case_stree(struct expression
*switch_expr
,
1096 struct range_list
*rl
,
1097 struct range_list_stack
**remaining_cases
,
1098 struct stree
**raw_stree
)
1102 struct var_sym_list
*vsl
;
1103 struct sm_state
*sm
;
1104 struct stree
*true_states
= NULL
;
1105 struct stree
*false_states
= NULL
;
1106 struct stree
*extra_states
;
1107 struct stree
*ret
= clone_stree(*raw_stree
);
1109 name
= expr_to_chunk_sym_vsl(switch_expr
, &sym
, &vsl
);
1112 filter_top_rl(remaining_cases
, rl
);
1114 rl
= clone_rl(top_rl(*remaining_cases
));
1117 sm
= get_sm_state_stree(*raw_stree
, SMATCH_EXTRA
, name
, sym
);
1119 separate_and_filter(sm
, SPECIAL_EQUAL
, rl
, *raw_stree
, &true_states
, &false_states
, NULL
);
1122 __push_fake_cur_stree();
1125 set_extra_nomod_vsl(name
, sym
, vsl
, NULL
, alloc_estate_rl(rl
));
1126 __pass_case_to_client(switch_expr
, rl
);
1127 extra_states
= __pop_fake_cur_stree();
1128 overwrite_stree(extra_states
, &true_states
);
1129 overwrite_stree(true_states
, &ret
);
1130 free_stree(&extra_states
);
1131 free_stree(&true_states
);
1132 free_stree(&false_states
);
1138 static void match_end_func(struct symbol
*sym
)
1142 implied_debug_msg
= NULL
;
1145 static void get_tf_stacks_from_pool(struct sm_state
*gate_sm
,
1146 struct sm_state
*pool_sm
,
1147 struct state_list
**true_stack
,
1148 struct state_list
**false_stack
)
1150 struct sm_state
*tmp
;
1151 int possibly_true
= 0;
1156 if (strcmp(gate_sm
->state
->name
, pool_sm
->state
->name
) == 0) {
1157 add_ptr_list(true_stack
, pool_sm
);
1161 FOR_EACH_PTR(gate_sm
->possible
, tmp
) {
1162 if (strcmp(tmp
->state
->name
, pool_sm
->state
->name
) == 0) {
1166 } END_FOR_EACH_PTR(tmp
);
1168 if (!possibly_true
) {
1169 add_ptr_list(false_stack
, gate_sm
);
1173 get_tf_stacks_from_pool(gate_sm
->left
, pool_sm
, true_stack
, false_stack
);
1174 get_tf_stacks_from_pool(gate_sm
->right
, pool_sm
, true_stack
, false_stack
);
1178 * The situation is we have a SMATCH_EXTRA state and we want to break it into
1179 * each of the ->possible states and find the implications of each. The caller
1180 * has to use __push_fake_cur_stree() to preserve the correct states so they
1181 * can be restored later.
1183 void overwrite_states_using_pool(struct sm_state
*gate_sm
, struct sm_state
*pool_sm
)
1185 struct state_list
*true_stack
= NULL
;
1186 struct state_list
*false_stack
= NULL
;
1187 struct stree
*pre_stree
;
1188 struct stree
*implied_true
;
1189 struct sm_state
*tmp
;
1194 get_tf_stacks_from_pool(gate_sm
, pool_sm
, &true_stack
, &false_stack
);
1196 pre_stree
= clone_stree(__get_cur_stree());
1198 implied_true
= filter_stack(gate_sm
, pre_stree
, false_stack
, true_stack
);
1200 free_stree(&pre_stree
);
1201 free_slist(&true_stack
);
1202 free_slist(&false_stack
);
1204 FOR_EACH_SM(implied_true
, tmp
) {
1206 } END_FOR_EACH_SM(tmp
);
1208 free_stree(&implied_true
);
1211 int assume(struct expression
*expr
)
1213 int orig_final_pass
= final_pass
;
1217 __push_fake_cur_stree();
1218 __split_whole_condition(expr
);
1219 final_pass
= orig_final_pass
;
1225 void end_assume(void)
1227 __discard_false_states();
1228 __free_fake_cur_stree();
1231 int impossible_assumption(struct expression
*left
, int op
, sval_t sval
)
1233 struct expression
*value
;
1234 struct expression
*comparison
;
1237 value
= value_expr(sval
.value
);
1238 comparison
= compare_expression(left
, op
, value
);
1240 if (!assume(comparison
))
1242 ret
= is_impossible_path();
1248 void __extra_match_condition(struct expression
*expr
);
1249 void __comparison_match_condition(struct expression
*expr
);
1250 void __stored_condition(struct expression
*expr
);
1251 void register_implications(int id
)
1253 add_hook(&save_implications_hook
, CONDITION_HOOK
);
1254 add_hook(&set_implied_states
, CONDITION_HOOK
);
1255 add_hook(&__extra_match_condition
, CONDITION_HOOK
);
1256 add_hook(&__comparison_match_condition
, CONDITION_HOOK
);
1257 add_hook(&set_extra_implied_states
, CONDITION_HOOK
);
1258 add_hook(&__stored_condition
, CONDITION_HOOK
);
1259 add_hook(&match_end_func
, END_FUNC_HOOK
);