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
;
67 #define implied_debug 0
68 #define DIMPLIED(msg...) do { if (implied_debug) printf(msg); } while (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 (!implied_debug
&& !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_msg("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
);
269 static int is_checked(struct state_list
*checked
, struct sm_state
*sm
)
271 struct sm_state
*tmp
;
273 FOR_EACH_PTR(checked
, tmp
) {
276 } END_FOR_EACH_PTR(tmp
);
282 * Example code: if (foo == 99) {
284 * Say 'foo' is a merged state that has many possible values. It is the combination
285 * of merges. separate_pools() iterates through the pools recursively and calls
286 * do_compare() for each time 'foo' was set.
288 static void __separate_pools(struct sm_state
*sm
, int comparison
, struct range_list
*rl
,
289 struct state_list
**true_stack
,
290 struct state_list
**maybe_stack
,
291 struct state_list
**false_stack
,
292 struct state_list
**checked
, int *mixed
, struct sm_state
*gate_sm
,
293 struct timeval
*start_time
)
295 int free_checked
= 0;
296 struct state_list
*checked_states
= NULL
;
302 gettimeofday(&now
, NULL
);
303 if (now
.tv_usec
- start_time
->tv_usec
> 1000000) {
305 sm_msg("debug: %s: implications taking too long. (%s %s %s)",
306 __func__
, sm
->state
->name
, show_special(comparison
), show_rl(rl
));
312 if (checked
== NULL
) {
313 checked
= &checked_states
;
316 if (is_checked(*checked
, sm
))
318 add_ptr_list(checked
, sm
);
320 do_compare(sm
, comparison
, rl
, true_stack
, maybe_stack
, false_stack
, mixed
, gate_sm
);
322 __separate_pools(sm
->left
, comparison
, rl
, true_stack
, maybe_stack
, false_stack
, checked
, mixed
, gate_sm
, start_time
);
323 __separate_pools(sm
->right
, comparison
, rl
, true_stack
, maybe_stack
, false_stack
, checked
, mixed
, gate_sm
, start_time
);
328 static void separate_pools(struct sm_state
*sm
, int comparison
, struct range_list
*rl
,
329 struct state_list
**true_stack
,
330 struct state_list
**false_stack
,
331 struct state_list
**checked
, int *mixed
)
333 struct state_list
*maybe_stack
= NULL
;
334 struct sm_state
*tmp
;
335 struct timeval start_time
;
338 gettimeofday(&start_time
, NULL
);
339 __separate_pools(sm
, comparison
, rl
, true_stack
, &maybe_stack
, false_stack
, checked
, mixed
, sm
, &start_time
);
344 FOR_EACH_PTR(*true_stack
, sm
) {
345 sm_msg("TRUE %s [stree %d]", show_sm(sm
), get_stree_id(sm
->pool
));
346 } END_FOR_EACH_PTR(sm
);
348 FOR_EACH_PTR(maybe_stack
, sm
) {
349 sm_msg("MAYBE %s %s[stree %d]",
350 show_sm(sm
), sm
->merged
? "(merged) ": "", get_stree_id(sm
->pool
));
351 } END_FOR_EACH_PTR(sm
);
353 FOR_EACH_PTR(*false_stack
, sm
) {
354 sm_msg("FALSE %s [stree %d]", show_sm(sm
), get_stree_id(sm
->pool
));
355 } END_FOR_EACH_PTR(sm
);
357 /* if it's a maybe then remove it */
358 FOR_EACH_PTR(maybe_stack
, tmp
) {
359 remove_pool(false_stack
, tmp
->pool
);
360 remove_pool(true_stack
, tmp
->pool
);
361 } END_FOR_EACH_PTR(tmp
);
363 /* if it's both true and false remove it from both */
364 FOR_EACH_PTR(*true_stack
, tmp
) {
365 if (remove_pool(false_stack
, tmp
->pool
))
366 DELETE_CURRENT_PTR(tmp
);
367 } END_FOR_EACH_PTR(tmp
);
370 static int sm_in_keep_leafs(struct sm_state
*sm
, const struct state_list
*keep_gates
)
372 struct sm_state
*tmp
, *old
;
374 FOR_EACH_PTR(keep_gates
, tmp
) {
377 old
= get_sm_state_stree(tmp
->pool
, sm
->owner
, sm
->name
, sm
->sym
);
382 } END_FOR_EACH_PTR(tmp
);
386 static int taking_too_long(void)
388 static void *printed
;
393 if (time_parsing_function() < 60)
396 if (!__inline_fn
&& printed
!= cur_func_sym
) {
397 sm_perror("turning off implications after 60 seconds");
398 printed
= cur_func_sym
;
404 * NOTE: If a state is in both the keep stack and the remove stack then that is
405 * a bug. Only add states which are definitely true or definitely false. If
406 * you have a leaf state that could be both true and false, then create a fake
407 * split history where one side is true and one side is false. Otherwise, if
408 * you can't do that, then don't add it to either list.
410 #define RECURSE_LIMIT 300
411 struct sm_state
*filter_pools(struct sm_state
*sm
,
412 const struct state_list
*remove_stack
,
413 const struct state_list
*keep_stack
,
414 int *modified
, int *recurse_cnt
,
415 struct timeval
*start
, int *skip
, int *bail
)
417 struct sm_state
*ret
= NULL
;
418 struct sm_state
*left
;
419 struct sm_state
*right
;
426 DIMPLIED("checking [stree %d] %s from %d left = %s [stree %d] right = %s [stree %d]\n",
427 get_stree_id(sm
->pool
),
428 show_sm(sm
), sm
->line
,
429 sm
->left
? sm
->left
->state
->name
: "<none>", sm
->left
? get_stree_id(sm
->left
->pool
) : -1,
430 sm
->right
? sm
->right
->state
->name
: "<none>", sm
->right
? get_stree_id(sm
->right
->pool
) : -1);
433 gettimeofday(&now
, NULL
);
434 if (now
.tv_usec
- start
->tv_usec
> 3000000) {
438 if ((*recurse_cnt
)++ > RECURSE_LIMIT
) {
443 if (pool_in_pools(sm
->pool
, remove_stack
)) {
444 DIMPLIED("removed [stree %d] %s from %d\n", get_stree_id(sm
->pool
), show_sm(sm
), sm
->line
);
449 if (!is_merged(sm
) || pool_in_pools(sm
->pool
, keep_stack
) || sm_in_keep_leafs(sm
, keep_stack
)) {
450 DIMPLIED("kept [stree %d] %s from %d. %s. %s. %s.\n", get_stree_id(sm
->pool
), show_sm(sm
), sm
->line
,
451 is_merged(sm
) ? "merged" : "not merged",
452 pool_in_pools(sm
->pool
, keep_stack
) ? "not in keep pools" : "in keep pools",
453 sm_in_keep_leafs(sm
, keep_stack
) ? "reachable keep leaf" : "no keep leaf");
457 left
= filter_pools(sm
->left
, remove_stack
, keep_stack
, &removed
, recurse_cnt
, start
, skip
, bail
);
458 right
= filter_pools(sm
->right
, remove_stack
, keep_stack
, &removed
, recurse_cnt
, start
, skip
, bail
);
462 DIMPLIED("kept [stree %d] %s from %d\n", get_stree_id(sm
->pool
), show_sm(sm
), sm
->line
);
466 if (!left
&& !right
) {
467 DIMPLIED("removed [stree %d] %s from %d <none>\n", get_stree_id(sm
->pool
), show_sm(sm
), sm
->line
);
472 ret
= clone_sm(right
);
477 ret
= clone_sm(left
);
482 if (left
->sym
!= sm
->sym
|| strcmp(left
->name
, sm
->name
) != 0) {
483 left
= clone_sm(left
);
485 left
->name
= sm
->name
;
487 if (right
->sym
!= sm
->sym
|| strcmp(right
->name
, sm
->name
) != 0) {
488 right
= clone_sm(right
);
489 right
->sym
= sm
->sym
;
490 right
->name
= sm
->name
;
492 ret
= merge_sm_states(left
, right
);
495 ret
->pool
= sm
->pool
;
497 DIMPLIED("partial %s => ", show_sm(sm
));
498 DIMPLIED("%s from %d [stree %d]\n", show_sm(ret
), sm
->line
, get_stree_id(sm
->pool
));
502 static struct stree
*filter_stack(struct sm_state
*gate_sm
,
503 struct stree
*pre_stree
,
504 const struct state_list
*remove_stack
,
505 const struct state_list
*keep_stack
)
507 struct stree
*ret
= NULL
;
508 struct sm_state
*tmp
;
509 struct sm_state
*filtered_sm
;
512 struct timeval start
;
519 gettimeofday(&start
, NULL
);
520 FOR_EACH_SM(pre_stree
, tmp
) {
521 if (!tmp
->merged
|| sm_in_keep_leafs(tmp
, keep_stack
))
526 filtered_sm
= filter_pools(tmp
, remove_stack
, keep_stack
, &modified
, &recurse_cnt
, &start
, &skip
, &bail
);
527 if (taking_too_long())
530 return ret
; /* Return the implications we figured out before time ran out. */
533 if (skip
|| !filtered_sm
|| !modified
)
535 /* the assignments here are for borrowed implications */
536 filtered_sm
->name
= tmp
->name
;
537 filtered_sm
->sym
= tmp
->sym
;
538 avl_insert(&ret
, filtered_sm
);
539 } END_FOR_EACH_SM(tmp
);
543 static void separate_and_filter(struct sm_state
*sm
, int comparison
, struct range_list
*rl
,
544 struct stree
*pre_stree
,
545 struct stree
**true_states
,
546 struct stree
**false_states
,
549 struct state_list
*true_stack
= NULL
;
550 struct state_list
*false_stack
= NULL
;
551 struct timeval time_before
;
552 struct timeval time_after
;
555 gettimeofday(&time_before
, NULL
);
557 DIMPLIED("checking implications: (%s (%s) %s %s)\n",
558 sm
->name
, sm
->state
->name
, show_special(comparison
), show_rl(rl
));
560 if (!is_merged(sm
)) {
561 DIMPLIED("%d '%s' from line %d is not merged.\n", get_lineno(), sm
->name
, sm
->line
);
565 separate_pools(sm
, comparison
, rl
, &true_stack
, &false_stack
, NULL
, mixed
);
567 DIMPLIED("filtering true stack.\n");
568 *true_states
= filter_stack(sm
, pre_stree
, false_stack
, true_stack
);
569 DIMPLIED("filtering false stack.\n");
570 *false_states
= filter_stack(sm
, pre_stree
, true_stack
, false_stack
);
571 free_slist(&true_stack
);
572 free_slist(&false_stack
);
574 printf("These are the implied states for the true path: (%s %s %s)\n",
575 sm
->name
, show_special(comparison
), show_rl(rl
));
576 __print_stree(*true_states
);
577 printf("These are the implied states for the false path: (%s %s %s)\n",
578 sm
->name
, show_special(comparison
), show_rl(rl
));
579 __print_stree(*false_states
);
582 gettimeofday(&time_after
, NULL
);
583 sec
= time_after
.tv_sec
- time_before
.tv_sec
;
585 sm_perror("Function too hairy. Ignoring implications after %d seconds.", sec
);
588 static struct expression
*get_last_expr(struct statement
*stmt
)
590 struct statement
*last
;
592 last
= last_ptr_list((struct ptr_list
*)stmt
->stmts
);
593 if (last
->type
== STMT_EXPRESSION
)
594 return last
->expression
;
596 if (last
->type
== STMT_LABEL
) {
597 if (last
->label_statement
&&
598 last
->label_statement
->type
== STMT_EXPRESSION
)
599 return last
->label_statement
->expression
;
605 static struct expression
*get_left_most_expr(struct expression
*expr
)
607 struct statement
*compound
;
609 compound
= get_expression_statement(expr
);
611 return get_last_expr(compound
);
613 expr
= strip_parens(expr
);
614 if (expr
->type
== EXPR_ASSIGNMENT
)
615 return get_left_most_expr(expr
->left
);
619 static int is_merged_expr(struct expression
*expr
)
624 if (get_value(expr
, &dummy
))
626 sm
= get_sm_state_expr(SMATCH_EXTRA
, expr
);
634 static void delete_gate_sm_equiv(struct stree
**stree
, const char *name
, struct symbol
*sym
)
636 struct smatch_state
*state
;
637 struct relation
*rel
;
639 state
= get_state(SMATCH_EXTRA
, name
, sym
);
642 FOR_EACH_PTR(estate_related(state
), rel
) {
643 delete_state_stree(stree
, SMATCH_EXTRA
, rel
->name
, rel
->sym
);
644 } END_FOR_EACH_PTR(rel
);
647 static void delete_gate_sm(struct stree
**stree
, const char *name
, struct symbol
*sym
)
649 delete_state_stree(stree
, SMATCH_EXTRA
, name
, sym
);
652 static int handle_comparison(struct expression
*expr
,
653 struct stree
**implied_true
,
654 struct stree
**implied_false
)
656 struct sm_state
*sm
= NULL
;
657 struct range_list
*rl
= NULL
;
658 struct expression
*left
;
659 struct expression
*right
;
661 int comparison
= expr
->op
;
664 left
= get_left_most_expr(expr
->left
);
665 right
= get_left_most_expr(expr
->right
);
667 if (is_merged_expr(left
)) {
668 sm
= get_sm_state_expr(SMATCH_EXTRA
, left
);
669 get_implied_rl(right
, &rl
);
670 } else if (is_merged_expr(right
)) {
671 sm
= get_sm_state_expr(SMATCH_EXTRA
, right
);
672 get_implied_rl(left
, &rl
);
673 comparison
= flip_comparison(comparison
);
679 type
= get_type(expr
);
682 if (type_positive_bits(rl_type(rl
)) > type_positive_bits(type
))
684 if (type_positive_bits(type
) < 31)
686 rl
= cast_rl(type
, rl
);
688 separate_and_filter(sm
, comparison
, rl
, __get_cur_stree(), implied_true
, implied_false
, &mixed
);
690 delete_gate_sm_equiv(implied_true
, sm
->name
, sm
->sym
);
691 delete_gate_sm_equiv(implied_false
, sm
->name
, sm
->sym
);
693 delete_gate_sm(implied_true
, sm
->name
, sm
->sym
);
694 delete_gate_sm(implied_false
, sm
->name
, sm
->sym
);
700 static int handle_zero_comparison(struct expression
*expr
,
701 struct stree
**implied_true
,
702 struct stree
**implied_false
)
710 if (expr
->type
== EXPR_POSTOP
)
711 expr
= strip_expr(expr
->unop
);
713 if (expr
->type
== EXPR_ASSIGNMENT
) {
714 /* most of the time ->pools will be empty here because we
715 just set the state, but if have assigned a conditional
716 function there are implications. */
720 name
= expr_to_var_sym(expr
, &sym
);
723 sm
= get_sm_state(SMATCH_EXTRA
, name
, sym
);
727 separate_and_filter(sm
, SPECIAL_NOTEQUAL
, tmp_range_list(estate_type(sm
->state
), 0), __get_cur_stree(), implied_true
, implied_false
, &mixed
);
728 delete_gate_sm_equiv(implied_true
, sm
->name
, sm
->sym
);
729 delete_gate_sm_equiv(implied_false
, sm
->name
, sm
->sym
);
731 delete_gate_sm(implied_true
, sm
->name
, sm
->sym
);
732 delete_gate_sm(implied_false
, sm
->name
, sm
->sym
);
741 static int handled_by_comparison_hook(struct expression
*expr
,
742 struct stree
**implied_true
,
743 struct stree
**implied_false
)
745 struct state_list
*true_stack
= NULL
;
746 struct state_list
*false_stack
= NULL
;
747 struct stree
*pre_stree
;
750 sm
= comparison_implication_hook(expr
, &true_stack
, &false_stack
);
754 pre_stree
= clone_stree(__get_cur_stree());
756 *implied_true
= filter_stack(sm
, pre_stree
, false_stack
, true_stack
);
757 *implied_false
= filter_stack(sm
, pre_stree
, true_stack
, false_stack
);
759 free_stree(&pre_stree
);
760 free_slist(&true_stack
);
761 free_slist(&false_stack
);
766 static int handled_by_extra_states(struct expression
*expr
,
767 struct stree
**implied_true
,
768 struct stree
**implied_false
)
770 if (expr
->type
== EXPR_COMPARE
)
771 return handle_comparison(expr
, implied_true
, implied_false
);
773 return handle_zero_comparison(expr
, implied_true
, implied_false
);
776 static int handled_by_stored_conditions(struct expression
*expr
,
777 struct stree
**implied_true
,
778 struct stree
**implied_false
)
780 struct state_list
*true_stack
= NULL
;
781 struct state_list
*false_stack
= NULL
;
782 struct stree
*pre_stree
;
785 sm
= stored_condition_implication_hook(expr
, &true_stack
, &false_stack
);
789 pre_stree
= clone_stree(__get_cur_stree());
791 *implied_true
= filter_stack(sm
, pre_stree
, false_stack
, true_stack
);
792 *implied_false
= filter_stack(sm
, pre_stree
, true_stack
, false_stack
);
794 free_stree(&pre_stree
);
795 free_slist(&true_stack
);
796 free_slist(&false_stack
);
801 static struct stree
*saved_implied_true
;
802 static struct stree
*saved_implied_false
;
803 static struct stree
*extra_saved_implied_true
;
804 static struct stree
*extra_saved_implied_false
;
806 static void separate_extra_states(struct stree
**implied_true
,
807 struct stree
**implied_false
)
811 /* We process extra states later to preserve the implications. */
812 FOR_EACH_SM(*implied_true
, sm
) {
813 if (sm
->owner
== SMATCH_EXTRA
)
814 overwrite_sm_state_stree(&extra_saved_implied_true
, sm
);
815 } END_FOR_EACH_SM(sm
);
816 FOR_EACH_SM(extra_saved_implied_true
, sm
) {
817 delete_state_stree(implied_true
, sm
->owner
, sm
->name
, sm
->sym
);
818 } END_FOR_EACH_SM(sm
);
820 FOR_EACH_SM(*implied_false
, sm
) {
821 if (sm
->owner
== SMATCH_EXTRA
)
822 overwrite_sm_state_stree(&extra_saved_implied_false
, sm
);
823 } END_FOR_EACH_SM(sm
);
824 FOR_EACH_SM(extra_saved_implied_false
, sm
) {
825 delete_state_stree(implied_false
, sm
->owner
, sm
->name
, sm
->sym
);
826 } END_FOR_EACH_SM(sm
);
829 static void get_tf_states(struct expression
*expr
,
830 struct stree
**implied_true
,
831 struct stree
**implied_false
)
833 if (handled_by_comparison_hook(expr
, implied_true
, implied_false
))
836 if (handled_by_extra_states(expr
, implied_true
, implied_false
)) {
837 separate_extra_states(implied_true
, implied_false
);
841 if (handled_by_stored_conditions(expr
, implied_true
, implied_false
))
845 static void save_implications_hook(struct expression
*expr
)
847 if (taking_too_long())
849 get_tf_states(expr
, &saved_implied_true
, &saved_implied_false
);
852 static void set_implied_states(struct expression
*expr
)
856 FOR_EACH_SM(saved_implied_true
, sm
) {
857 __set_true_false_sm(sm
, NULL
);
858 } END_FOR_EACH_SM(sm
);
859 free_stree(&saved_implied_true
);
861 FOR_EACH_SM(saved_implied_false
, sm
) {
862 __set_true_false_sm(NULL
, sm
);
863 } END_FOR_EACH_SM(sm
);
864 free_stree(&saved_implied_false
);
867 static void set_extra_implied_states(struct expression
*expr
)
869 saved_implied_true
= extra_saved_implied_true
;
870 saved_implied_false
= extra_saved_implied_false
;
871 extra_saved_implied_true
= NULL
;
872 extra_saved_implied_false
= NULL
;
873 set_implied_states(NULL
);
876 void param_limit_implications(struct expression
*expr
, int param
, char *key
, char *value
)
878 struct expression
*arg
;
879 struct symbol
*compare_type
;
883 struct sm_state
*tmp
;
884 struct stree
*implied_true
= NULL
;
885 struct stree
*implied_false
= NULL
;
886 struct range_list
*orig
, *limit
;
888 if (time_parsing_function() > 40)
891 while (expr
->type
== EXPR_ASSIGNMENT
)
892 expr
= strip_expr(expr
->right
);
893 if (expr
->type
!= EXPR_CALL
)
896 arg
= get_argument_from_call_expr(expr
->args
, param
);
900 arg
= strip_parens(arg
);
901 while (arg
->type
== EXPR_ASSIGNMENT
&& arg
->op
== '=')
902 arg
= strip_parens(arg
->left
);
904 name
= get_variable_from_key(arg
, key
, &sym
);
908 sm
= get_sm_state(SMATCH_EXTRA
, name
, sym
);
909 if (!sm
|| !sm
->merged
)
912 if (strcmp(key
, "$") == 0)
913 compare_type
= get_arg_type(expr
->fn
, param
);
915 compare_type
= get_member_type_from_key(arg
, key
);
917 orig
= estate_rl(sm
->state
);
918 orig
= cast_rl(compare_type
, orig
);
920 call_results_to_rl(expr
, compare_type
, value
, &limit
);
922 separate_and_filter(sm
, SPECIAL_EQUAL
, limit
, __get_cur_stree(), &implied_true
, &implied_false
, NULL
);
924 FOR_EACH_SM(implied_true
, tmp
) {
925 __set_sm_fake_stree(tmp
);
926 } END_FOR_EACH_SM(tmp
);
928 free_stree(&implied_true
);
929 free_stree(&implied_false
);
934 struct stree
*__implied_case_stree(struct expression
*switch_expr
,
935 struct range_list
*rl
,
936 struct range_list_stack
**remaining_cases
,
937 struct stree
**raw_stree
)
941 struct var_sym_list
*vsl
;
943 struct stree
*true_states
= NULL
;
944 struct stree
*false_states
= NULL
;
945 struct stree
*extra_states
;
946 struct stree
*ret
= clone_stree(*raw_stree
);
948 name
= expr_to_chunk_sym_vsl(switch_expr
, &sym
, &vsl
);
951 filter_top_rl(remaining_cases
, rl
);
953 rl
= clone_rl(top_rl(*remaining_cases
));
956 sm
= get_sm_state_stree(*raw_stree
, SMATCH_EXTRA
, name
, sym
);
958 separate_and_filter(sm
, SPECIAL_EQUAL
, rl
, *raw_stree
, &true_states
, &false_states
, NULL
);
961 __push_fake_cur_stree();
964 set_extra_nomod_vsl(name
, sym
, vsl
, NULL
, alloc_estate_rl(rl
));
965 __pass_case_to_client(switch_expr
, rl
);
966 extra_states
= __pop_fake_cur_stree();
967 overwrite_stree(extra_states
, &true_states
);
968 overwrite_stree(true_states
, &ret
);
969 free_stree(&extra_states
);
970 free_stree(&true_states
);
971 free_stree(&false_states
);
977 static void match_end_func(struct symbol
*sym
)
981 implied_debug_msg
= NULL
;
984 static void get_tf_stacks_from_pool(struct sm_state
*gate_sm
,
985 struct sm_state
*pool_sm
,
986 struct state_list
**true_stack
,
987 struct state_list
**false_stack
)
989 struct sm_state
*tmp
;
990 int possibly_true
= 0;
995 if (strcmp(gate_sm
->state
->name
, pool_sm
->state
->name
) == 0) {
996 add_ptr_list(true_stack
, pool_sm
);
1000 FOR_EACH_PTR(gate_sm
->possible
, tmp
) {
1001 if (strcmp(tmp
->state
->name
, pool_sm
->state
->name
) == 0) {
1005 } END_FOR_EACH_PTR(tmp
);
1007 if (!possibly_true
) {
1008 add_ptr_list(false_stack
, gate_sm
);
1012 get_tf_stacks_from_pool(gate_sm
->left
, pool_sm
, true_stack
, false_stack
);
1013 get_tf_stacks_from_pool(gate_sm
->right
, pool_sm
, true_stack
, false_stack
);
1017 * The situation is we have a SMATCH_EXTRA state and we want to break it into
1018 * each of the ->possible states and find the implications of each. The caller
1019 * has to use __push_fake_cur_stree() to preserve the correct states so they
1020 * can be restored later.
1022 void overwrite_states_using_pool(struct sm_state
*gate_sm
, struct sm_state
*pool_sm
)
1024 struct state_list
*true_stack
= NULL
;
1025 struct state_list
*false_stack
= NULL
;
1026 struct stree
*pre_stree
;
1027 struct stree
*implied_true
;
1028 struct sm_state
*tmp
;
1033 get_tf_stacks_from_pool(gate_sm
, pool_sm
, &true_stack
, &false_stack
);
1035 pre_stree
= clone_stree(__get_cur_stree());
1037 implied_true
= filter_stack(gate_sm
, pre_stree
, false_stack
, true_stack
);
1039 free_stree(&pre_stree
);
1040 free_slist(&true_stack
);
1041 free_slist(&false_stack
);
1043 FOR_EACH_SM(implied_true
, tmp
) {
1044 set_state(tmp
->owner
, tmp
->name
, tmp
->sym
, tmp
->state
);
1045 } END_FOR_EACH_SM(tmp
);
1047 free_stree(&implied_true
);
1050 int assume(struct expression
*expr
)
1052 int orig_final_pass
= final_pass
;
1056 __push_fake_cur_stree();
1057 __split_whole_condition(expr
);
1058 final_pass
= orig_final_pass
;
1064 void end_assume(void)
1066 __discard_false_states();
1067 __free_fake_cur_stree();
1070 int impossible_assumption(struct expression
*left
, int op
, sval_t sval
)
1072 struct expression
*value
;
1073 struct expression
*comparison
;
1076 value
= value_expr(sval
.value
);
1077 comparison
= compare_expression(left
, op
, value
);
1079 if (!assume(comparison
))
1081 ret
= is_impossible_path();
1087 void __extra_match_condition(struct expression
*expr
);
1088 void __comparison_match_condition(struct expression
*expr
);
1089 void __stored_condition(struct expression
*expr
);
1090 void register_implications(int id
)
1092 add_hook(&save_implications_hook
, CONDITION_HOOK
);
1093 add_hook(&set_implied_states
, CONDITION_HOOK
);
1094 add_hook(&__extra_match_condition
, CONDITION_HOOK
);
1095 add_hook(&set_extra_implied_states
, CONDITION_HOOK
);
1096 add_hook(&__comparison_match_condition
, CONDITION_HOOK
);
1097 add_hook(&__stored_condition
, CONDITION_HOOK
);
1098 add_hook(&match_end_func
, END_FUNC_HOOK
);