2 * Copyright (C) 2008 Dan Carpenter.
4 * This program is free software; you can redistribute it and/or
5 * modify it under the terms of the GNU General Public License
6 * as published by the Free Software Foundation; either version 2
7 * of the License, or (at your option) any later version.
9 * This program is distributed in the hope that it will be useful,
10 * but WITHOUT ANY WARRANTY; without even the implied warranty of
11 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
12 * GNU General Public License for more details.
14 * You should have received a copy of the GNU General Public License
15 * along with this program; if not, see http://www.gnu.org/copyleft/gpl.txt
19 * Imagine we have this code:
26 * if (foo == 99) // <-- point #2
27 * bar->baz; // <-- point #3
30 * At point #3 bar is non null and can be dereferenced.
32 * It's smatch_implied.c which sets bar to non null at point #2.
34 * At point #1 merge_slist() stores the list of states from both
35 * the true and false paths. On the true path foo == 99 and on
36 * the false path foo == 1. merge_slist() sets their pool
37 * list to show the other states which were there when foo == 99.
39 * When it comes to the if (foo == 99) the smatch implied hook
40 * looks for all the pools where foo was not 99. It makes a list
43 * Then for bar (and all the other states) it says, ok bar is a
44 * merged state that came from these previous states. We'll
45 * chop out all the states where it came from a pool where
46 * foo != 99 and merge it all back together.
48 * That is the implied state of bar.
50 * merge_slist() sets up ->pool. An sm_state only has one ->pool and
51 * that is the pool where it was first set. The my pool gets set when
52 * code paths merge. States that have been set since the last merge do
54 * merge_sm_state() sets ->left and ->right. (These are the states which were
55 * merged to form the current state.)
56 * a pool: a pool is an slist that has been merged with another slist.
62 #include "smatch_slist.h"
63 #include "smatch_extra.h"
65 char *implied_debug_msg
;
66 #define DIMPLIED(msg...) do { if (option_debug_implied || option_debug) printf(msg); } while (0)
68 int option_debug_implied
= 0;
72 * It messes things up to free range list allocations. This helper fuction
73 * lets us reuse memory instead of doing new allocations.
75 static struct range_list
*tmp_range_list(struct symbol
*type
, long long num
)
77 static struct range_list
*my_list
= NULL
;
78 static struct data_range
*my_range
;
80 __free_ptr_list((struct ptr_list
**)&my_list
);
81 my_range
= alloc_range(ll_to_sval(num
), ll_to_sval(num
));
82 add_ptr_list(&my_list
, my_range
);
86 static void print_debug_tf(struct sm_state
*sm
, int istrue
, int isfalse
)
88 if (!option_debug_implied
&& !option_debug
)
91 if (istrue
&& isfalse
) {
92 printf("%s: %d: does not exist.\n", show_sm(sm
), sm
->line
);
94 printf("'%s = %s' from %d is true. %s[stree %d]\n", sm
->name
, show_state(sm
->state
),
95 sm
->line
, sm
->merged
? "[merged]" : "[leaf]",
96 get_stree_id(sm
->pool
));
98 printf("'%s = %s' from %d is false. %s[stree %d]\n", sm
->name
, show_state(sm
->state
),
100 sm
->merged
? "[merged]" : "[leaf]",
101 get_stree_id(sm
->pool
));
103 printf("'%s = %s' from %d could be true or false. %s[stree %d]\n", sm
->name
,
104 show_state(sm
->state
), sm
->line
,
105 sm
->merged
? "[merged]" : "[leaf]",
106 get_stree_id(sm
->pool
));
110 static int create_fake_history(struct sm_state
*sm
, int comparison
, struct range_list
*rl
)
112 struct range_list
*orig_rl
;
113 struct range_list
*true_rl
, *false_rl
;
114 struct stree
*true_stree
, *false_stree
;
115 struct sm_state
*true_sm
, *false_sm
;
118 if (is_merged(sm
) || sm
->left
|| sm
->right
)
120 if (!rl_to_sval(rl
, &sval
))
122 if (!estate_rl(sm
->state
))
125 orig_rl
= cast_rl(rl_type(rl
), estate_rl(sm
->state
));
126 split_comparison_rl(orig_rl
, comparison
, rl
, &true_rl
, &false_rl
, NULL
, NULL
);
128 true_rl
= rl_truncate_cast(estate_type(sm
->state
), true_rl
);
129 false_rl
= rl_truncate_cast(estate_type(sm
->state
), false_rl
);
130 if (is_whole_rl(true_rl
) || is_whole_rl(false_rl
) ||
131 !true_rl
|| !false_rl
||
132 rl_equiv(orig_rl
, true_rl
) || rl_equiv(orig_rl
, false_rl
) ||
133 rl_equiv(estate_rl(sm
->state
), true_rl
) || rl_equiv(estate_rl(sm
->state
), false_rl
))
136 if (rl_intersection(true_rl
, false_rl
)) {
137 sm_perror("parsing (%s (%s) %s %s)",
138 sm
->name
, sm
->state
->name
, show_special(comparison
), show_rl(rl
));
139 sm_msg("true_rl = %s false_rl = %s intersection = %s",
140 show_rl(true_rl
), show_rl(false_rl
), show_rl(rl_intersection(true_rl
, false_rl
)));
145 sm_info("fake_history: %s vs %s. %s %s %s. --> T: %s F: %s",
146 sm
->name
, show_rl(rl
), sm
->state
->name
, show_special(comparison
), show_rl(rl
),
147 show_rl(true_rl
), show_rl(false_rl
));
149 true_sm
= clone_sm(sm
);
150 false_sm
= clone_sm(sm
);
152 true_sm
->state
= clone_partial_estate(sm
->state
, true_rl
);
153 free_slist(&true_sm
->possible
);
154 add_possible_sm(true_sm
, true_sm
);
155 false_sm
->state
= clone_partial_estate(sm
->state
, false_rl
);
156 free_slist(&false_sm
->possible
);
157 add_possible_sm(false_sm
, false_sm
);
159 true_stree
= clone_stree(sm
->pool
);
160 false_stree
= clone_stree(sm
->pool
);
162 overwrite_sm_state_stree(&true_stree
, true_sm
);
163 overwrite_sm_state_stree(&false_stree
, false_sm
);
165 true_sm
->pool
= true_stree
;
166 false_sm
->pool
= false_stree
;
170 sm
->right
= false_sm
;
176 * add_pool() adds a slist to *pools. If the slist has already been
177 * added earlier then it doesn't get added a second time.
179 void add_pool(struct state_list
**pools
, struct sm_state
*new)
181 struct sm_state
*tmp
;
183 FOR_EACH_PTR(*pools
, tmp
) {
184 if (tmp
->pool
< new->pool
)
186 else if (tmp
->pool
== new->pool
) {
189 INSERT_CURRENT(new, tmp
);
192 } END_FOR_EACH_PTR(tmp
);
193 add_ptr_list(pools
, new);
196 static int pool_in_pools(struct stree
*pool
,
197 const struct state_list
*slist
)
199 struct sm_state
*tmp
;
201 FOR_EACH_PTR(slist
, tmp
) {
204 if (tmp
->pool
== pool
)
206 } END_FOR_EACH_PTR(tmp
);
210 static int remove_pool(struct state_list
**pools
, struct stree
*remove
)
212 struct sm_state
*tmp
;
215 FOR_EACH_PTR(*pools
, tmp
) {
216 if (tmp
->pool
== remove
) {
217 DELETE_CURRENT_PTR(tmp
);
220 } END_FOR_EACH_PTR(tmp
);
226 * If 'foo' == 99 add it that pool to the true pools. If it's false, add it to
227 * the false pools. If we're not sure, then we don't add it to either.
229 static void do_compare(struct sm_state
*sm
, int comparison
, struct range_list
*rl
,
230 struct state_list
**true_stack
,
231 struct state_list
**maybe_stack
,
232 struct state_list
**false_stack
,
233 int *mixed
, struct sm_state
*gate_sm
)
237 struct range_list
*var_rl
;
242 var_rl
= cast_rl(rl_type(rl
), estate_rl(sm
->state
));
244 istrue
= !possibly_false_rl(var_rl
, comparison
, rl
);
245 isfalse
= !possibly_true_rl(var_rl
, comparison
, rl
);
247 print_debug_tf(sm
, istrue
, isfalse
);
249 /* give up if we have borrowed implications (smatch_equiv.c) */
250 if (sm
->sym
!= gate_sm
->sym
||
251 strcmp(sm
->name
, gate_sm
->name
) != 0) {
256 if (mixed
&& !*mixed
&& !is_merged(sm
) && !istrue
&& !isfalse
) {
257 if (!create_fake_history(sm
, comparison
, rl
))
262 add_pool(true_stack
, sm
);
264 add_pool(false_stack
, sm
);
266 add_pool(maybe_stack
, sm
);
270 static int is_checked(struct state_list
*checked
, struct sm_state
*sm
)
272 struct sm_state
*tmp
;
274 FOR_EACH_PTR(checked
, tmp
) {
277 } END_FOR_EACH_PTR(tmp
);
283 * Example code: if (foo == 99) {
285 * Say 'foo' is a merged state that has many possible values. It is the combination
286 * of merges. separate_pools() iterates through the pools recursively and calls
287 * do_compare() for each time 'foo' was set.
289 static void __separate_pools(struct sm_state
*sm
, int comparison
, struct range_list
*rl
,
290 struct state_list
**true_stack
,
291 struct state_list
**maybe_stack
,
292 struct state_list
**false_stack
,
293 struct state_list
**checked
, int *mixed
, struct sm_state
*gate_sm
)
295 int free_checked
= 0;
296 struct state_list
*checked_states
= NULL
;
302 * If it looks like this is going to take too long as-is, then don't
303 * create even more fake history.
305 if (mixed
&& sm
->nr_children
> 100)
309 Sometimes the implications are just too big to deal with
310 so we bail. Theoretically, bailing out here can cause more false
311 positives but won't hide actual bugs.
313 if (sm
->nr_children
> 4000) {
314 if (option_debug
|| option_debug_implied
) {
315 static char buf
[1028];
316 snprintf(buf
, sizeof(buf
), "debug: %s: nr_children over 4000 (%d). (%s %s)",
317 __func__
, sm
->nr_children
, sm
->name
, show_state(sm
->state
));
318 implied_debug_msg
= buf
;
323 if (checked
== NULL
) {
324 checked
= &checked_states
;
327 if (is_checked(*checked
, sm
))
329 add_ptr_list(checked
, sm
);
331 do_compare(sm
, comparison
, rl
, true_stack
, maybe_stack
, false_stack
, mixed
, gate_sm
);
333 __separate_pools(sm
->left
, comparison
, rl
, true_stack
, maybe_stack
, false_stack
, checked
, mixed
, gate_sm
);
334 __separate_pools(sm
->right
, comparison
, rl
, true_stack
, maybe_stack
, false_stack
, checked
, mixed
, gate_sm
);
339 static void separate_pools(struct sm_state
*sm
, int comparison
, struct range_list
*rl
,
340 struct state_list
**true_stack
,
341 struct state_list
**false_stack
,
342 struct state_list
**checked
, int *mixed
)
344 struct state_list
*maybe_stack
= NULL
;
345 struct sm_state
*tmp
;
347 __separate_pools(sm
, comparison
, rl
, true_stack
, &maybe_stack
, false_stack
, checked
, mixed
, sm
);
352 FOR_EACH_PTR(*true_stack
, sm
) {
353 sm_msg("TRUE %s [stree %d]", show_sm(sm
), get_stree_id(sm
->pool
));
354 } END_FOR_EACH_PTR(sm
);
356 FOR_EACH_PTR(maybe_stack
, sm
) {
357 sm_msg("MAYBE %s [stree %d]", show_sm(sm
), get_stree_id(sm
->pool
));
358 } END_FOR_EACH_PTR(sm
);
360 FOR_EACH_PTR(*false_stack
, sm
) {
361 sm_msg("FALSE %s [stree %d]", show_sm(sm
), get_stree_id(sm
->pool
));
362 } END_FOR_EACH_PTR(sm
);
364 /* if it's a maybe then remove it */
365 FOR_EACH_PTR(maybe_stack
, tmp
) {
366 remove_pool(false_stack
, tmp
->pool
);
367 remove_pool(true_stack
, tmp
->pool
);
368 } END_FOR_EACH_PTR(tmp
);
370 /* if it's both true and false remove it from both */
371 FOR_EACH_PTR(*true_stack
, tmp
) {
372 if (remove_pool(false_stack
, tmp
->pool
))
373 DELETE_CURRENT_PTR(tmp
);
374 } END_FOR_EACH_PTR(tmp
);
377 static int sm_in_keep_leafs(struct sm_state
*sm
, const struct state_list
*keep_gates
)
379 struct sm_state
*tmp
, *old
;
381 FOR_EACH_PTR(keep_gates
, tmp
) {
384 old
= get_sm_state_stree(tmp
->pool
, sm
->owner
, sm
->name
, sm
->sym
);
389 } END_FOR_EACH_PTR(tmp
);
393 static int taking_too_long(void)
395 static void *printed
;
400 if (time_parsing_function() < 60)
403 if (!__inline_fn
&& printed
!= cur_func_sym
) {
404 sm_perror("turning off implications after 60 seconds");
405 printed
= cur_func_sym
;
411 * NOTE: If a state is in both the keep stack and the remove stack then that is
412 * a bug. Only add states which are definitely true or definitely false. If
413 * you have a leaf state that could be both true and false, then create a fake
414 * split history where one side is true and one side is false. Otherwise, if
415 * you can't do that, then don't add it to either list.
417 struct sm_state
*filter_pools(struct sm_state
*sm
,
418 const struct state_list
*remove_stack
,
419 const struct state_list
*keep_stack
,
420 int *modified
, int *recurse_cnt
,
421 struct timeval
*start
, int *incomplete
)
423 struct sm_state
*ret
= NULL
;
424 struct sm_state
*left
;
425 struct sm_state
*right
;
432 DIMPLIED("checking [stree %d] %s from %d (nr_children: %d)%s%s left = %s [stree %d] right = %s [stree %d]\n",
433 get_stree_id(sm
->pool
),
434 show_sm(sm
), sm
->line
, sm
->nr_children
,
435 sm
->skip_implications
? " (skip_implications)" : "",
436 *incomplete
? " (INCOMPLETE)" : "",
437 sm
->left
? sm
->left
->state
->name
: "<none>", sm
->left
? get_stree_id(sm
->left
->pool
) : -1,
438 sm
->right
? sm
->right
->state
->name
: "<none>", sm
->right
? get_stree_id(sm
->right
->pool
) : -1);
442 if (sm
->skip_implications
)
444 if (taking_too_long())
447 gettimeofday(&now
, NULL
);
448 if ((*recurse_cnt
)++ > 1000 || now
.tv_sec
- start
->tv_sec
> 5) {
449 if (local_debug
|| option_debug_implied
) {
450 static char buf
[1028];
451 snprintf(buf
, sizeof(buf
), "debug: %s: nr_children over 4000 (%d). (%s %s)",
452 __func__
, sm
->nr_children
, sm
->name
, show_state(sm
->state
));
453 implied_debug_msg
= buf
;
455 sm
->skip_implications
= 1;
460 if (pool_in_pools(sm
->pool
, remove_stack
)) {
461 DIMPLIED("removed [stree %d] %s from %d\n", get_stree_id(sm
->pool
), show_sm(sm
), sm
->line
);
466 if (!is_merged(sm
) || pool_in_pools(sm
->pool
, keep_stack
) || sm_in_keep_leafs(sm
, keep_stack
)) {
467 DIMPLIED("kept [stree %d] %s from %d. %s. %s. %s.\n", get_stree_id(sm
->pool
), show_sm(sm
), sm
->line
,
468 is_merged(sm
) ? "merged" : "not merged",
469 pool_in_pools(sm
->pool
, keep_stack
) ? "not in keep pools" : "in keep pools",
470 sm_in_keep_leafs(sm
, keep_stack
) ? "reachable keep leaf" : "no keep leaf");
474 left
= filter_pools(sm
->left
, remove_stack
, keep_stack
, &removed
, recurse_cnt
, start
, incomplete
);
475 right
= filter_pools(sm
->right
, remove_stack
, keep_stack
, &removed
, recurse_cnt
, start
, incomplete
);
477 DIMPLIED("kept [stree %d] %s from %d\n", get_stree_id(sm
->pool
), show_sm(sm
), sm
->line
);
481 if (!left
&& !right
) {
482 DIMPLIED("removed [stree %d] %s from %d <none>\n", get_stree_id(sm
->pool
), show_sm(sm
), sm
->line
);
487 ret
= clone_sm(right
);
492 ret
= clone_sm(left
);
497 if (left
->sym
!= sm
->sym
|| strcmp(left
->name
, sm
->name
) != 0) {
498 left
= clone_sm(left
);
500 left
->name
= sm
->name
;
502 if (right
->sym
!= sm
->sym
|| strcmp(right
->name
, sm
->name
) != 0) {
503 right
= clone_sm(right
);
504 right
->sym
= sm
->sym
;
505 right
->name
= sm
->name
;
507 ret
= merge_sm_states(left
, right
);
510 ret
->pool
= sm
->pool
;
512 DIMPLIED("partial %s => ", show_sm(sm
));
513 DIMPLIED("%s from %d [stree %d]\n", show_sm(ret
), sm
->line
, get_stree_id(sm
->pool
));
517 static struct stree
*filter_stack(struct sm_state
*gate_sm
,
518 struct stree
*pre_stree
,
519 const struct state_list
*remove_stack
,
520 const struct state_list
*keep_stack
)
522 struct stree
*ret
= NULL
;
523 struct sm_state
*tmp
;
524 struct sm_state
*filtered_sm
;
527 struct timeval start
;
533 if (taking_too_long())
536 FOR_EACH_SM(pre_stree
, tmp
) {
538 sm_msg("%s: %s", __func__
, show_sm(tmp
));
541 if (sm_in_keep_leafs(tmp
, keep_stack
))
545 gettimeofday(&start
, NULL
);
547 filtered_sm
= filter_pools(tmp
, remove_stack
, keep_stack
, &modified
, &recurse_cnt
, &start
, &incomplete
);
548 if (!filtered_sm
|| !modified
|| incomplete
)
550 /* the assignments here are for borrowed implications */
551 filtered_sm
->name
= tmp
->name
;
552 filtered_sm
->sym
= tmp
->sym
;
553 avl_insert(&ret
, filtered_sm
);
554 if (out_of_memory() || taking_too_long())
557 } END_FOR_EACH_SM(tmp
);
561 static void separate_and_filter(struct sm_state
*sm
, int comparison
, struct range_list
*rl
,
562 struct stree
*pre_stree
,
563 struct stree
**true_states
,
564 struct stree
**false_states
,
567 struct state_list
*true_stack
= NULL
;
568 struct state_list
*false_stack
= NULL
;
569 struct timeval time_before
;
570 struct timeval time_after
;
573 gettimeofday(&time_before
, NULL
);
575 DIMPLIED("checking implications: (%s (%s) %s %s)\n",
576 sm
->name
, sm
->state
->name
, show_special(comparison
), show_rl(rl
));
578 if (!is_merged(sm
)) {
579 DIMPLIED("%d '%s' from line %d is not merged.\n", get_lineno(), sm
->name
, sm
->line
);
583 separate_pools(sm
, comparison
, rl
, &true_stack
, &false_stack
, NULL
, mixed
);
585 DIMPLIED("filtering true stack.\n");
586 *true_states
= filter_stack(sm
, pre_stree
, false_stack
, true_stack
);
587 DIMPLIED("filtering false stack.\n");
588 *false_states
= filter_stack(sm
, pre_stree
, true_stack
, false_stack
);
589 free_slist(&true_stack
);
590 free_slist(&false_stack
);
591 if (option_debug_implied
|| option_debug
) {
592 printf("These are the implied states for the true path: (%s %s %s)\n",
593 sm
->name
, show_special(comparison
), show_rl(rl
));
594 __print_stree(*true_states
);
595 printf("These are the implied states for the false path: (%s %s %s)\n",
596 sm
->name
, show_special(comparison
), show_rl(rl
));
597 __print_stree(*false_states
);
600 gettimeofday(&time_after
, NULL
);
601 sec
= time_after
.tv_sec
- time_before
.tv_sec
;
603 sm
->nr_children
= MAX_CHILDREN
;
604 sm_perror("Function too hairy. Ignoring implications after %d seconds.", sec
);
608 static struct expression
*get_last_expr(struct statement
*stmt
)
610 struct statement
*last
;
612 last
= last_ptr_list((struct ptr_list
*)stmt
->stmts
);
613 if (last
->type
== STMT_EXPRESSION
)
614 return last
->expression
;
616 if (last
->type
== STMT_LABEL
) {
617 if (last
->label_statement
&&
618 last
->label_statement
->type
== STMT_EXPRESSION
)
619 return last
->label_statement
->expression
;
625 static struct expression
*get_left_most_expr(struct expression
*expr
)
627 struct statement
*compound
;
629 compound
= get_expression_statement(expr
);
631 return get_last_expr(compound
);
633 expr
= strip_parens(expr
);
634 if (expr
->type
== EXPR_ASSIGNMENT
)
635 return get_left_most_expr(expr
->left
);
639 static int is_merged_expr(struct expression
*expr
)
644 if (get_value(expr
, &dummy
))
646 sm
= get_sm_state_expr(SMATCH_EXTRA
, expr
);
654 static void delete_gate_sm_equiv(struct stree
**stree
, const char *name
, struct symbol
*sym
)
656 struct smatch_state
*state
;
657 struct relation
*rel
;
659 state
= get_state(SMATCH_EXTRA
, name
, sym
);
662 FOR_EACH_PTR(estate_related(state
), rel
) {
663 delete_state_stree(stree
, SMATCH_EXTRA
, rel
->name
, rel
->sym
);
664 } END_FOR_EACH_PTR(rel
);
667 static void delete_gate_sm(struct stree
**stree
, const char *name
, struct symbol
*sym
)
669 delete_state_stree(stree
, SMATCH_EXTRA
, name
, sym
);
672 static int handle_comparison(struct expression
*expr
,
673 struct stree
**implied_true
,
674 struct stree
**implied_false
)
676 struct sm_state
*sm
= NULL
;
677 struct range_list
*rl
= NULL
;
678 struct expression
*left
;
679 struct expression
*right
;
681 int comparison
= expr
->op
;
684 left
= get_left_most_expr(expr
->left
);
685 right
= get_left_most_expr(expr
->right
);
687 if (is_merged_expr(left
)) {
688 sm
= get_sm_state_expr(SMATCH_EXTRA
, left
);
689 get_implied_rl(right
, &rl
);
690 } else if (is_merged_expr(right
)) {
691 sm
= get_sm_state_expr(SMATCH_EXTRA
, right
);
692 get_implied_rl(left
, &rl
);
693 comparison
= flip_comparison(comparison
);
699 type
= get_type(expr
);
702 if (type_positive_bits(rl_type(rl
)) > type_positive_bits(type
))
704 if (type_positive_bits(type
) < 31)
706 rl
= cast_rl(type
, rl
);
708 separate_and_filter(sm
, comparison
, rl
, __get_cur_stree(), implied_true
, implied_false
, &mixed
);
710 delete_gate_sm_equiv(implied_true
, sm
->name
, sm
->sym
);
711 delete_gate_sm_equiv(implied_false
, sm
->name
, sm
->sym
);
713 delete_gate_sm(implied_true
, sm
->name
, sm
->sym
);
714 delete_gate_sm(implied_false
, sm
->name
, sm
->sym
);
720 static int handle_zero_comparison(struct expression
*expr
,
721 struct stree
**implied_true
,
722 struct stree
**implied_false
)
730 if (expr
->type
== EXPR_POSTOP
)
731 expr
= strip_expr(expr
->unop
);
733 if (expr
->type
== EXPR_ASSIGNMENT
) {
734 /* most of the time ->pools will be empty here because we
735 just set the state, but if have assigned a conditional
736 function there are implications. */
740 name
= expr_to_var_sym(expr
, &sym
);
743 sm
= get_sm_state(SMATCH_EXTRA
, name
, sym
);
747 separate_and_filter(sm
, SPECIAL_NOTEQUAL
, tmp_range_list(estate_type(sm
->state
), 0), __get_cur_stree(), implied_true
, implied_false
, &mixed
);
748 delete_gate_sm_equiv(implied_true
, sm
->name
, sm
->sym
);
749 delete_gate_sm_equiv(implied_false
, sm
->name
, sm
->sym
);
751 delete_gate_sm(implied_true
, sm
->name
, sm
->sym
);
752 delete_gate_sm(implied_false
, sm
->name
, sm
->sym
);
761 static int handled_by_comparison_hook(struct expression
*expr
,
762 struct stree
**implied_true
,
763 struct stree
**implied_false
)
765 struct state_list
*true_stack
= NULL
;
766 struct state_list
*false_stack
= NULL
;
767 struct stree
*pre_stree
;
770 sm
= comparison_implication_hook(expr
, &true_stack
, &false_stack
);
774 pre_stree
= clone_stree(__get_cur_stree());
776 *implied_true
= filter_stack(sm
, pre_stree
, false_stack
, true_stack
);
777 *implied_false
= filter_stack(sm
, pre_stree
, true_stack
, false_stack
);
779 free_stree(&pre_stree
);
780 free_slist(&true_stack
);
781 free_slist(&false_stack
);
786 static int handled_by_extra_states(struct expression
*expr
,
787 struct stree
**implied_true
,
788 struct stree
**implied_false
)
790 if (expr
->type
== EXPR_COMPARE
)
791 return handle_comparison(expr
, implied_true
, implied_false
);
793 return handle_zero_comparison(expr
, implied_true
, implied_false
);
796 static int handled_by_stored_conditions(struct expression
*expr
,
797 struct stree
**implied_true
,
798 struct stree
**implied_false
)
800 struct state_list
*true_stack
= NULL
;
801 struct state_list
*false_stack
= NULL
;
802 struct stree
*pre_stree
;
805 sm
= stored_condition_implication_hook(expr
, &true_stack
, &false_stack
);
809 pre_stree
= clone_stree(__get_cur_stree());
811 *implied_true
= filter_stack(sm
, pre_stree
, false_stack
, true_stack
);
812 *implied_false
= filter_stack(sm
, pre_stree
, true_stack
, false_stack
);
814 free_stree(&pre_stree
);
815 free_slist(&true_stack
);
816 free_slist(&false_stack
);
821 static int found_implications
;
822 static struct stree
*saved_implied_true
;
823 static struct stree
*saved_implied_false
;
824 static struct stree
*extra_saved_implied_true
;
825 static struct stree
*extra_saved_implied_false
;
827 static void separate_extra_states(struct stree
**implied_true
,
828 struct stree
**implied_false
)
832 /* We process extra states later to preserve the implications. */
833 FOR_EACH_SM(*implied_true
, sm
) {
834 if (sm
->owner
== SMATCH_EXTRA
)
835 overwrite_sm_state_stree(&extra_saved_implied_true
, sm
);
836 } END_FOR_EACH_SM(sm
);
837 FOR_EACH_SM(extra_saved_implied_true
, sm
) {
838 delete_state_stree(implied_true
, sm
->owner
, sm
->name
, sm
->sym
);
839 } END_FOR_EACH_SM(sm
);
841 FOR_EACH_SM(*implied_false
, sm
) {
842 if (sm
->owner
== SMATCH_EXTRA
)
843 overwrite_sm_state_stree(&extra_saved_implied_false
, sm
);
844 } END_FOR_EACH_SM(sm
);
845 FOR_EACH_SM(extra_saved_implied_false
, sm
) {
846 delete_state_stree(implied_false
, sm
->owner
, sm
->name
, sm
->sym
);
847 } END_FOR_EACH_SM(sm
);
850 static void get_tf_states(struct expression
*expr
,
851 struct stree
**implied_true
,
852 struct stree
**implied_false
)
854 if (handled_by_comparison_hook(expr
, implied_true
, implied_false
))
857 if (handled_by_extra_states(expr
, implied_true
, implied_false
)) {
858 separate_extra_states(implied_true
, implied_false
);
862 if (handled_by_stored_conditions(expr
, implied_true
, implied_false
))
867 found_implications
= 1;
870 static void save_implications_hook(struct expression
*expr
)
872 if (taking_too_long())
874 get_tf_states(expr
, &saved_implied_true
, &saved_implied_false
);
877 static void set_implied_states(struct expression
*expr
)
881 FOR_EACH_SM(saved_implied_true
, sm
) {
882 __set_true_false_sm(sm
, NULL
);
883 } END_FOR_EACH_SM(sm
);
884 free_stree(&saved_implied_true
);
886 FOR_EACH_SM(saved_implied_false
, sm
) {
887 __set_true_false_sm(NULL
, sm
);
888 } END_FOR_EACH_SM(sm
);
889 free_stree(&saved_implied_false
);
892 static void set_extra_implied_states(struct expression
*expr
)
894 saved_implied_true
= extra_saved_implied_true
;
895 saved_implied_false
= extra_saved_implied_false
;
896 extra_saved_implied_true
= NULL
;
897 extra_saved_implied_false
= NULL
;
898 set_implied_states(NULL
);
901 void param_limit_implications(struct expression
*expr
, int param
, char *key
, char *value
)
903 struct expression
*arg
;
904 struct symbol
*compare_type
;
908 struct sm_state
*tmp
;
909 struct stree
*implied_true
= NULL
;
910 struct stree
*implied_false
= NULL
;
911 struct range_list
*orig
, *limit
;
913 while (expr
->type
== EXPR_ASSIGNMENT
)
914 expr
= strip_expr(expr
->right
);
915 if (expr
->type
!= EXPR_CALL
)
918 arg
= get_argument_from_call_expr(expr
->args
, param
);
922 arg
= strip_parens(arg
);
923 while (arg
->type
== EXPR_ASSIGNMENT
&& arg
->op
== '=')
924 arg
= strip_parens(arg
->left
);
926 name
= get_variable_from_key(arg
, key
, &sym
);
930 sm
= get_sm_state(SMATCH_EXTRA
, name
, sym
);
931 if (!sm
|| !sm
->merged
)
934 if (strcmp(key
, "$") == 0)
935 compare_type
= get_arg_type(expr
->fn
, param
);
937 compare_type
= get_member_type_from_key(arg
, key
);
939 orig
= estate_rl(sm
->state
);
940 orig
= cast_rl(compare_type
, orig
);
942 call_results_to_rl(expr
, compare_type
, value
, &limit
);
944 separate_and_filter(sm
, SPECIAL_EQUAL
, limit
, __get_cur_stree(), &implied_true
, &implied_false
, NULL
);
946 FOR_EACH_SM(implied_true
, tmp
) {
947 __set_sm_fake_stree(tmp
);
948 } END_FOR_EACH_SM(tmp
);
950 free_stree(&implied_true
);
951 free_stree(&implied_false
);
956 struct stree
*__implied_case_stree(struct expression
*switch_expr
,
957 struct range_list
*rl
,
958 struct range_list_stack
**remaining_cases
,
959 struct stree
**raw_stree
)
963 struct var_sym_list
*vsl
;
965 struct stree
*true_states
= NULL
;
966 struct stree
*false_states
= NULL
;
967 struct stree
*extra_states
;
968 struct stree
*ret
= clone_stree(*raw_stree
);
970 name
= expr_to_chunk_sym_vsl(switch_expr
, &sym
, &vsl
);
973 filter_top_rl(remaining_cases
, rl
);
975 rl
= clone_rl(top_rl(*remaining_cases
));
978 sm
= get_sm_state_stree(*raw_stree
, SMATCH_EXTRA
, name
, sym
);
980 separate_and_filter(sm
, SPECIAL_EQUAL
, rl
, *raw_stree
, &true_states
, &false_states
, NULL
);
983 __push_fake_cur_stree();
986 set_extra_nomod_vsl(name
, sym
, vsl
, NULL
, alloc_estate_rl(rl
));
987 __pass_case_to_client(switch_expr
, rl
);
988 extra_states
= __pop_fake_cur_stree();
989 overwrite_stree(extra_states
, &true_states
);
990 overwrite_stree(true_states
, &ret
);
991 free_stree(&extra_states
);
992 free_stree(&true_states
);
993 free_stree(&false_states
);
999 static void match_end_func(struct symbol
*sym
)
1003 implied_debug_msg
= NULL
;
1006 static void get_tf_stacks_from_pool(struct sm_state
*gate_sm
,
1007 struct sm_state
*pool_sm
,
1008 struct state_list
**true_stack
,
1009 struct state_list
**false_stack
)
1011 struct sm_state
*tmp
;
1012 int possibly_true
= 0;
1017 if (strcmp(gate_sm
->state
->name
, pool_sm
->state
->name
) == 0) {
1018 add_ptr_list(true_stack
, pool_sm
);
1022 FOR_EACH_PTR(gate_sm
->possible
, tmp
) {
1023 if (strcmp(tmp
->state
->name
, pool_sm
->state
->name
) == 0) {
1027 } END_FOR_EACH_PTR(tmp
);
1029 if (!possibly_true
) {
1030 add_ptr_list(false_stack
, gate_sm
);
1034 get_tf_stacks_from_pool(gate_sm
->left
, pool_sm
, true_stack
, false_stack
);
1035 get_tf_stacks_from_pool(gate_sm
->right
, pool_sm
, true_stack
, false_stack
);
1039 * The situation is we have a SMATCH_EXTRA state and we want to break it into
1040 * each of the ->possible states and find the implications of each. The caller
1041 * has to use __push_fake_cur_stree() to preserve the correct states so they
1042 * can be restored later.
1044 void overwrite_states_using_pool(struct sm_state
*gate_sm
, struct sm_state
*pool_sm
)
1046 struct state_list
*true_stack
= NULL
;
1047 struct state_list
*false_stack
= NULL
;
1048 struct stree
*pre_stree
;
1049 struct stree
*implied_true
;
1050 struct sm_state
*tmp
;
1055 get_tf_stacks_from_pool(gate_sm
, pool_sm
, &true_stack
, &false_stack
);
1057 pre_stree
= clone_stree(__get_cur_stree());
1059 implied_true
= filter_stack(gate_sm
, pre_stree
, false_stack
, true_stack
);
1061 free_stree(&pre_stree
);
1062 free_slist(&true_stack
);
1063 free_slist(&false_stack
);
1065 FOR_EACH_SM(implied_true
, tmp
) {
1066 set_state(tmp
->owner
, tmp
->name
, tmp
->sym
, tmp
->state
);
1067 } END_FOR_EACH_SM(tmp
);
1069 free_stree(&implied_true
);
1072 int assume(struct expression
*expr
)
1074 int orig_final_pass
= final_pass
;
1078 __push_fake_cur_stree();
1079 found_implications
= 0;
1080 __split_whole_condition(expr
);
1081 final_pass
= orig_final_pass
;
1087 void end_assume(void)
1089 __discard_false_states();
1090 __free_fake_cur_stree();
1093 int impossible_assumption(struct expression
*left
, int op
, sval_t sval
)
1095 struct expression
*value
;
1096 struct expression
*comparison
;
1099 value
= value_expr(sval
.value
);
1100 comparison
= compare_expression(left
, op
, value
);
1102 if (!assume(comparison
))
1104 ret
= is_impossible_path();
1110 void __extra_match_condition(struct expression
*expr
);
1111 void __comparison_match_condition(struct expression
*expr
);
1112 void __stored_condition(struct expression
*expr
);
1113 void register_implications(int id
)
1115 add_hook(&save_implications_hook
, CONDITION_HOOK
);
1116 add_hook(&set_implied_states
, CONDITION_HOOK
);
1117 add_hook(&__extra_match_condition
, CONDITION_HOOK
);
1118 add_hook(&set_extra_implied_states
, CONDITION_HOOK
);
1119 add_hook(&__comparison_match_condition
, CONDITION_HOOK
);
1120 add_hook(&__stored_condition
, CONDITION_HOOK
);
1121 add_hook(&match_end_func
, END_FUNC_HOOK
);