2 * Copyright (C) 2008 Dan Carpenter.
4 * This program is free software; you can redistribute it and/or
5 * modify it under the terms of the GNU General Public License
6 * as published by the Free Software Foundation; either version 2
7 * of the License, or (at your option) any later version.
9 * This program is distributed in the hope that it will be useful,
10 * but WITHOUT ANY WARRANTY; without even the implied warranty of
11 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
12 * GNU General Public License for more details.
14 * You should have received a copy of the GNU General Public License
15 * along with this program; if not, see http://www.gnu.org/copyleft/gpl.txt
19 * Imagine we have this code:
26 * if (foo == 99) // <-- point #2
27 * bar->baz; // <-- point #3
30 * At point #3 bar is non null and can be dereferenced.
32 * It's smatch_implied.c which sets bar to non null at point #2.
34 * At point #1 merge_slist() stores the list of states from both
35 * the true and false paths. On the true path foo == 99 and on
36 * the false path foo == 1. merge_slist() sets their pool
37 * list to show the other states which were there when foo == 99.
39 * When it comes to the if (foo == 99) the smatch implied hook
40 * looks for all the pools where foo was not 99. It makes a list
43 * Then for bar (and all the other states) it says, ok bar is a
44 * merged state that came from these previous states. We'll
45 * chop out all the states where it came from a pool where
46 * foo != 99 and merge it all back together.
48 * That is the implied state of bar.
50 * merge_slist() sets up ->pool. An sm_state only has one ->pool and
51 * that is the pool where it was first set. The my pool gets set when
52 * code paths merge. States that have been set since the last merge do
54 * merge_sm_state() sets ->left and ->right. (These are the states which were
55 * merged to form the current state.)
56 * a pool: a pool is an slist that has been merged with another slist.
62 #include "smatch_slist.h"
63 #include "smatch_extra.h"
65 char *implied_debug_msg
;
66 #define DIMPLIED(msg...) do { if (option_debug_implied) printf(msg); } while (0)
68 int option_debug_implied
= 0;
72 * It messes things up to free range list allocations. This helper fuction
73 * lets us reuse memory instead of doing new allocations.
75 static struct range_list
*tmp_range_list(struct symbol
*type
, long long num
)
77 static struct range_list
*my_list
= NULL
;
78 static struct data_range
*my_range
;
80 __free_ptr_list((struct ptr_list
**)&my_list
);
81 my_range
= alloc_range(ll_to_sval(num
), ll_to_sval(num
));
82 add_ptr_list(&my_list
, my_range
);
86 static void print_debug_tf(struct sm_state
*sm
, int istrue
, int isfalse
)
88 if (!option_debug_implied
&& !option_debug
)
91 if (istrue
&& isfalse
) {
92 printf("%s: %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_msg("internal error 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
= alloc_estate_rl(cast_rl(estate_type(sm
->state
), true_rl
));
153 free_slist(&true_sm
->possible
);
154 add_possible_sm(true_sm
, true_sm
);
155 false_sm
->state
= alloc_estate_rl(cast_rl(estate_type(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 * If 'foo' == 99 add it that pool to the true pools. If it's false, add it to
177 * the false pools. If we're not sure, then we don't add it to either.
179 static void do_compare(struct sm_state
*sm
, int comparison
, struct range_list
*rl
,
180 struct state_list
**true_stack
,
181 struct state_list
**false_stack
, int *mixed
, struct sm_state
*gate_sm
)
186 struct range_list
*var_rl
;
191 if (is_implied(sm
)) {
192 s
= get_sm_state_stree(sm
->pool
,
200 if (option_debug_implied
|| option_debug
)
201 sm_msg("%s from %d, has borrowed implications.",
206 var_rl
= cast_rl(rl_type(rl
), estate_rl(s
->state
));
208 istrue
= !possibly_false_rl(var_rl
, comparison
, rl
);
209 isfalse
= !possibly_true_rl(var_rl
, comparison
, rl
);
211 print_debug_tf(s
, istrue
, isfalse
);
213 /* give up if we have borrowed implications (smatch_equiv.c) */
214 if (sm
->sym
!= gate_sm
->sym
||
215 strcmp(sm
->name
, gate_sm
->name
) != 0) {
220 if (mixed
&& !*mixed
&& !is_merged(sm
) && !istrue
&& !isfalse
) {
221 if (!create_fake_history(sm
, comparison
, rl
)) {
228 add_ptr_list(true_stack
, s
);
231 add_ptr_list(false_stack
, s
);
234 static int pool_in_pools(struct stree
*pool
,
235 const struct state_list
*slist
)
237 struct sm_state
*tmp
;
239 FOR_EACH_PTR(slist
, tmp
) {
242 if (tmp
->pool
== pool
)
244 } END_FOR_EACH_PTR(tmp
);
248 static int is_checked(struct state_list
*checked
, struct sm_state
*sm
)
250 struct sm_state
*tmp
;
252 FOR_EACH_PTR(checked
, tmp
) {
255 } END_FOR_EACH_PTR(tmp
);
261 * Example code: if (foo == 99) {
263 * Say 'foo' is a merged state that has many possible values. It is the combination
264 * of merges. separate_pools() iterates through the pools recursively and calls
265 * do_compare() for each time 'foo' was set.
267 static void __separate_pools(struct sm_state
*sm
, int comparison
, struct range_list
*rl
,
268 struct state_list
**true_stack
,
269 struct state_list
**false_stack
,
270 struct state_list
**checked
, int *mixed
, struct sm_state
*gate_sm
)
272 int free_checked
= 0;
273 struct state_list
*checked_states
= NULL
;
279 * If it looks like this is going to take too long as-is, then don't
280 * create even more fake history.
282 if (mixed
&& sm
->nr_children
> 100)
286 Sometimes the implications are just too big to deal with
287 so we bail. Theoretically, bailing out here can cause more false
288 positives but won't hide actual bugs.
290 if (sm
->nr_children
> 4000) {
291 if (option_debug
|| option_debug_implied
) {
292 static char buf
[1028];
293 snprintf(buf
, sizeof(buf
), "debug: %s: nr_children over 4000 (%d). (%s %s)",
294 __func__
, sm
->nr_children
, sm
->name
, show_state(sm
->state
));
295 implied_debug_msg
= buf
;
300 if (checked
== NULL
) {
301 checked
= &checked_states
;
304 if (is_checked(*checked
, sm
))
306 add_ptr_list(checked
, sm
);
308 do_compare(sm
, comparison
, rl
, true_stack
, false_stack
, mixed
, gate_sm
);
310 __separate_pools(sm
->left
, comparison
, rl
, true_stack
, false_stack
, checked
, mixed
, gate_sm
);
311 __separate_pools(sm
->right
, comparison
, rl
, true_stack
, false_stack
, checked
, mixed
, gate_sm
);
316 static void separate_pools(struct sm_state
*sm
, int comparison
, struct range_list
*rl
,
317 struct state_list
**true_stack
,
318 struct state_list
**false_stack
,
319 struct state_list
**checked
, int *mixed
)
321 __separate_pools(sm
, comparison
, rl
, true_stack
, false_stack
, checked
, mixed
, sm
);
324 struct sm_state
*filter_pools(struct sm_state
*sm
,
325 const struct state_list
*remove_stack
,
326 const struct state_list
*keep_stack
,
329 struct sm_state
*ret
= NULL
;
330 struct sm_state
*left
;
331 struct sm_state
*right
;
337 if (sm
->nr_children
> 4000) {
338 if (option_debug
|| option_debug_implied
) {
339 static char buf
[1028];
340 snprintf(buf
, sizeof(buf
), "debug: %s: nr_children over 4000 (%d). (%s %s)",
341 __func__
, sm
->nr_children
, sm
->name
, show_state(sm
->state
));
342 implied_debug_msg
= buf
;
347 if (pool_in_pools(sm
->pool
, remove_stack
)) {
348 DIMPLIED("removed %s from %d [stree %d]\n", show_sm(sm
), sm
->line
, get_stree_id(sm
->pool
));
353 if (!is_merged(sm
) || pool_in_pools(sm
->pool
, keep_stack
)) {
354 DIMPLIED("kept %s from %d [stree %d]\n", show_sm(sm
), sm
->line
, get_stree_id(sm
->pool
));
358 DIMPLIED("checking %s from %d (%d) [stree %d] left = %s [stree %d] right = %s [stree %d]\n",
359 show_sm(sm
), sm
->line
, sm
->nr_children
, get_stree_id(sm
->pool
),
360 sm
->left
? show_sm(sm
->left
) : "<none>", sm
->left
? get_stree_id(sm
->left
->pool
) : -1,
361 sm
->right
? show_sm(sm
->right
) : "<none>", sm
->right
? get_stree_id(sm
->right
->pool
) : -1);
362 left
= filter_pools(sm
->left
, remove_stack
, keep_stack
, &removed
);
363 right
= filter_pools(sm
->right
, remove_stack
, keep_stack
, &removed
);
365 DIMPLIED("kept %s from %d [stree %d]\n", show_sm(sm
), sm
->line
, get_stree_id(sm
->pool
));
369 if (!left
&& !right
) {
370 DIMPLIED("removed %s from %d <none> [stree %d]\n", show_sm(sm
), sm
->line
, get_stree_id(sm
->pool
));
375 ret
= clone_sm(right
);
380 ret
= clone_sm(left
);
385 ret
= merge_sm_states(left
, right
);
388 ret
->pool
= sm
->pool
;
391 DIMPLIED("partial %s => ", show_sm(sm
));
392 DIMPLIED("%s from %d [stree %d]\n", show_sm(ret
), sm
->line
, get_stree_id(sm
->pool
));
396 static int highest_stree_id(struct sm_state
*sm
)
401 if (!sm
->left
&& !sm
->right
)
405 left
= get_stree_id(sm
->left
->pool
);
407 right
= get_stree_id(sm
->right
->pool
);
414 static struct stree
*filter_stack(struct sm_state
*gate_sm
,
415 struct stree
*pre_stree
,
416 const struct state_list
*remove_stack
,
417 const struct state_list
*keep_stack
)
419 struct stree
*ret
= NULL
;
420 struct sm_state
*tmp
;
421 struct sm_state
*filtered_sm
;
427 FOR_EACH_SM(pre_stree
, tmp
) {
430 if (highest_stree_id(tmp
) < highest_stree_id(gate_sm
)) {
431 DIMPLIED("skipping %s. set before. %d vs %d\n",
432 tmp
->name
, highest_stree_id(tmp
),
433 highest_stree_id(gate_sm
));
437 filtered_sm
= filter_pools(tmp
, remove_stack
, keep_stack
, &modified
);
438 if (filtered_sm
&& modified
) {
439 /* the assignments here are for borrowed implications */
440 filtered_sm
->name
= tmp
->name
;
441 filtered_sm
->sym
= tmp
->sym
;
442 avl_insert(&ret
, filtered_sm
);
447 } END_FOR_EACH_SM(tmp
);
451 static void separate_and_filter(struct sm_state
*sm
, int comparison
, struct range_list
*rl
,
452 struct stree
*pre_stree
,
453 struct stree
**true_states
,
454 struct stree
**false_states
,
457 struct state_list
*true_stack
= NULL
;
458 struct state_list
*false_stack
= NULL
;
459 struct timeval time_before
;
460 struct timeval time_after
;
462 gettimeofday(&time_before
, NULL
);
464 if (!is_merged(sm
)) {
465 DIMPLIED("%d '%s' is not merged.\n", get_lineno(), sm
->name
);
469 if (option_debug_implied
|| option_debug
) {
470 sm_msg("checking implications: (%s %s %s)",
471 sm
->name
, show_special(comparison
), show_rl(rl
));
474 separate_pools(sm
, comparison
, rl
, &true_stack
, &false_stack
, NULL
, mixed
);
476 DIMPLIED("filtering true stack.\n");
477 *true_states
= filter_stack(sm
, pre_stree
, false_stack
, true_stack
);
478 DIMPLIED("filtering false stack.\n");
479 *false_states
= filter_stack(sm
, pre_stree
, true_stack
, false_stack
);
480 free_slist(&true_stack
);
481 free_slist(&false_stack
);
482 if (option_debug_implied
|| option_debug
) {
483 printf("These are the implied states for the true path:\n");
484 __print_stree(*true_states
);
485 printf("These are the implied states for the false path:\n");
486 __print_stree(*false_states
);
489 gettimeofday(&time_after
, NULL
);
490 if (time_after
.tv_sec
- time_before
.tv_sec
> 7)
491 __bail_on_rest_of_function
= 1;
494 static struct expression
*get_left_most_expr(struct expression
*expr
)
496 expr
= strip_parens(expr
);
497 if (expr
->type
== EXPR_ASSIGNMENT
)
498 return get_left_most_expr(expr
->left
);
502 static int is_merged_expr(struct expression
*expr
)
507 if (get_value(expr
, &dummy
))
509 sm
= get_sm_state_expr(SMATCH_EXTRA
, expr
);
517 static void delete_gate_sm_equiv(struct stree
**stree
, const char *name
, struct symbol
*sym
)
519 struct smatch_state
*state
;
520 struct relation
*rel
;
522 state
= get_state(SMATCH_EXTRA
, name
, sym
);
525 FOR_EACH_PTR(estate_related(state
), rel
) {
526 delete_state_stree(stree
, SMATCH_EXTRA
, rel
->name
, rel
->sym
);
527 } END_FOR_EACH_PTR(rel
);
530 static void delete_gate_sm(struct stree
**stree
, const char *name
, struct symbol
*sym
)
532 delete_state_stree(stree
, SMATCH_EXTRA
, name
, sym
);
535 static int handle_comparison(struct expression
*expr
,
536 struct stree
**implied_true
,
537 struct stree
**implied_false
)
539 struct sm_state
*sm
= NULL
;
540 struct range_list
*rl
= NULL
;
541 struct expression
*left
;
542 struct expression
*right
;
544 int comparison
= expr
->op
;
547 left
= get_left_most_expr(expr
->left
);
548 right
= get_left_most_expr(expr
->right
);
550 if (is_merged_expr(left
)) {
551 sm
= get_sm_state_expr(SMATCH_EXTRA
, left
);
552 get_implied_rl(right
, &rl
);
553 } else if (is_merged_expr(right
)) {
554 sm
= get_sm_state_expr(SMATCH_EXTRA
, right
);
555 get_implied_rl(left
, &rl
);
556 comparison
= flip_comparison(comparison
);
564 type
= get_type(expr
);
567 if (type_positive_bits(rl_type(rl
)) > type_positive_bits(type
))
569 if (type_positive_bits(type
) < 31)
571 rl
= cast_rl(type
, rl
);
573 separate_and_filter(sm
, comparison
, rl
, __get_cur_stree(), implied_true
, implied_false
, &mixed
);
576 delete_gate_sm_equiv(implied_true
, sm
->name
, sm
->sym
);
577 delete_gate_sm_equiv(implied_false
, sm
->name
, sm
->sym
);
579 delete_gate_sm(implied_true
, sm
->name
, sm
->sym
);
580 delete_gate_sm(implied_false
, sm
->name
, sm
->sym
);
586 static int handle_zero_comparison(struct expression
*expr
,
587 struct stree
**implied_true
,
588 struct stree
**implied_false
)
596 if (expr
->type
== EXPR_POSTOP
)
597 expr
= strip_expr(expr
->unop
);
599 if (expr
->type
== EXPR_ASSIGNMENT
) {
600 /* most of the time ->pools will be empty here because we
601 just set the state, but if have assigned a conditional
602 function there are implications. */
606 name
= expr_to_var_sym(expr
, &sym
);
609 sm
= get_sm_state(SMATCH_EXTRA
, name
, sym
);
613 separate_and_filter(sm
, SPECIAL_NOTEQUAL
, tmp_range_list(estate_type(sm
->state
), 0), __get_cur_stree(), implied_true
, implied_false
, &mixed
);
614 delete_gate_sm_equiv(implied_true
, sm
->name
, sm
->sym
);
615 delete_gate_sm_equiv(implied_false
, sm
->name
, sm
->sym
);
617 delete_gate_sm(implied_true
, sm
->name
, sm
->sym
);
618 delete_gate_sm(implied_false
, sm
->name
, sm
->sym
);
627 static int handled_by_implied_hook(struct expression
*expr
,
628 struct stree
**implied_true
,
629 struct stree
**implied_false
)
631 struct state_list
*true_stack
= NULL
;
632 struct state_list
*false_stack
= NULL
;
633 struct stree
*pre_stree
;
636 sm
= comparison_implication_hook(expr
, &true_stack
, &false_stack
);
640 pre_stree
= clone_stree(__get_cur_stree());
642 *implied_true
= filter_stack(sm
, pre_stree
, false_stack
, true_stack
);
643 *implied_false
= filter_stack(sm
, pre_stree
, true_stack
, false_stack
);
645 free_stree(&pre_stree
);
646 free_slist(&true_stack
);
647 free_slist(&false_stack
);
652 static int handled_by_extra_states(struct expression
*expr
,
653 struct stree
**implied_true
,
654 struct stree
**implied_false
)
656 if (expr
->type
== EXPR_COMPARE
)
657 return handle_comparison(expr
, implied_true
, implied_false
);
659 return handle_zero_comparison(expr
, implied_true
, implied_false
);
662 static int handled_by_stored_conditions(struct expression
*expr
,
663 struct stree
**implied_true
,
664 struct stree
**implied_false
)
666 struct state_list
*true_stack
= NULL
;
667 struct state_list
*false_stack
= NULL
;
668 struct stree
*pre_stree
;
671 sm
= stored_condition_implication_hook(expr
, &true_stack
, &false_stack
);
675 pre_stree
= clone_stree(__get_cur_stree());
677 *implied_true
= filter_stack(sm
, pre_stree
, false_stack
, true_stack
);
678 *implied_false
= filter_stack(sm
, pre_stree
, true_stack
, false_stack
);
680 free_stree(&pre_stree
);
681 free_slist(&true_stack
);
682 free_slist(&false_stack
);
687 static int found_implications
;
688 static struct stree
*saved_implied_true
;
689 static struct stree
*saved_implied_false
;
690 static struct stree
*extra_saved_implied_true
;
691 static struct stree
*extra_saved_implied_false
;
693 static void get_tf_states(struct expression
*expr
,
694 struct stree
**implied_true
,
695 struct stree
**implied_false
)
697 if (handled_by_implied_hook(expr
, implied_true
, implied_false
))
700 if (handled_by_extra_states(expr
, implied_true
, implied_false
)) {
701 /* We process these later. */
702 extra_saved_implied_true
= *implied_true
;
703 extra_saved_implied_false
= *implied_false
;
704 *implied_true
= NULL
;
705 *implied_false
= NULL
;
709 if (handled_by_stored_conditions(expr
, implied_true
, implied_false
))
714 found_implications
= 1;
717 static void save_implications_hook(struct expression
*expr
)
719 get_tf_states(expr
, &saved_implied_true
, &saved_implied_false
);
722 static void set_implied_states(struct expression
*expr
)
726 FOR_EACH_SM(saved_implied_true
, sm
) {
727 __set_true_false_sm(sm
, NULL
);
728 } END_FOR_EACH_SM(sm
);
729 free_stree(&saved_implied_true
);
731 FOR_EACH_SM(saved_implied_false
, sm
) {
732 __set_true_false_sm(NULL
, sm
);
733 } END_FOR_EACH_SM(sm
);
734 free_stree(&saved_implied_false
);
737 static void set_extra_implied_states(struct expression
*expr
)
739 saved_implied_true
= extra_saved_implied_true
;
740 saved_implied_false
= extra_saved_implied_false
;
741 extra_saved_implied_true
= NULL
;
742 extra_saved_implied_false
= NULL
;
743 set_implied_states(NULL
);
746 void param_limit_implications(struct expression
*expr
, int param
, char *key
, char *value
)
748 struct expression
*arg
;
749 struct symbol
*compare_type
;
753 struct sm_state
*tmp
;
754 struct stree
*implied_true
= NULL
;
755 struct stree
*implied_false
= NULL
;
756 struct range_list
*orig
, *limit
, *rl
;
758 while (expr
->type
== EXPR_ASSIGNMENT
)
759 expr
= strip_expr(expr
->right
);
760 if (expr
->type
!= EXPR_CALL
)
763 arg
= get_argument_from_call_expr(expr
->args
, param
);
767 name
= get_variable_from_key(arg
, key
, &sym
);
771 sm
= get_sm_state(SMATCH_EXTRA
, name
, sym
);
772 if (!sm
|| !sm
->merged
)
775 if (strcmp(key
, "$") == 0)
776 compare_type
= get_arg_type(expr
->fn
, param
);
778 compare_type
= get_member_type_from_key(arg
, key
);
780 orig
= estate_rl(sm
->state
);
781 orig
= cast_rl(compare_type
, orig
);
783 call_results_to_rl(expr
, compare_type
, value
, &limit
);
784 rl
= rl_intersection(orig
, limit
);
786 separate_and_filter(sm
, SPECIAL_EQUAL
, rl
, __get_cur_stree(), &implied_true
, &implied_false
, NULL
);
788 FOR_EACH_SM(implied_true
, tmp
) {
789 __set_sm_fake_stree(tmp
);
790 } END_FOR_EACH_SM(tmp
);
792 free_stree(&implied_true
);
793 free_stree(&implied_false
);
798 struct stree
*__implied_case_stree(struct expression
*switch_expr
,
799 struct range_list
*rl
,
800 struct range_list_stack
**remaining_cases
,
801 struct stree
**raw_stree
)
806 struct stree
*true_states
= NULL
;
807 struct stree
*false_states
= NULL
;
808 struct stree
*extra_states
;
809 struct stree
*ret
= clone_stree(*raw_stree
);
811 name
= expr_to_var_sym(switch_expr
, &sym
);
816 filter_top_rl(remaining_cases
, rl
);
818 rl
= clone_rl(top_rl(*remaining_cases
));
820 sm
= get_sm_state_stree(*raw_stree
, SMATCH_EXTRA
, name
, sym
);
822 separate_and_filter(sm
, SPECIAL_EQUAL
, rl
, *raw_stree
, &true_states
, &false_states
, NULL
);
824 __push_fake_cur_stree();
826 set_extra_nomod(name
, sym
, alloc_estate_rl(rl
));
827 extra_states
= __pop_fake_cur_stree();
828 overwrite_stree(extra_states
, &true_states
);
829 overwrite_stree(true_states
, &ret
);
830 free_stree(&extra_states
);
831 free_stree(&true_states
);
832 free_stree(&false_states
);
838 static void match_end_func(struct symbol
*sym
)
842 implied_debug_msg
= NULL
;
845 static int sm_state_in_slist(struct sm_state
*sm
, struct state_list
*slist
)
847 struct sm_state
*tmp
;
849 FOR_EACH_PTR(slist
, tmp
) {
852 } END_FOR_EACH_PTR(tmp
);
857 * The situation is we have a SMATCH_EXTRA state and we want to break it into
858 * each of the ->possible states and find the implications of each. The caller
859 * has to use __push_fake_cur_stree() to preserve the correct states so they
860 * can be restored later.
862 void overwrite_states_using_pool(struct sm_state
*sm
)
864 struct sm_state
*old
;
865 struct sm_state
*new;
870 FOR_EACH_SM(sm
->pool
, old
) {
871 new = get_sm_state(old
->owner
, old
->name
, old
->sym
);
872 if (!new) /* the variable went out of scope */
874 if (sm_state_in_slist(old
, new->possible
))
875 set_state(old
->owner
, old
->name
, old
->sym
, old
->state
);
876 } END_FOR_EACH_SM(old
);
879 int assume(struct expression
*expr
)
881 int orig_final_pass
= final_pass
;
884 __push_fake_cur_stree();
885 found_implications
= 0;
886 __split_whole_condition(expr
);
887 final_pass
= orig_final_pass
;
889 if (!found_implications
) {
890 __discard_false_states();
891 __free_fake_cur_stree();
898 void end_assume(void)
900 __discard_false_states();
901 __free_fake_cur_stree();
904 void __extra_match_condition(struct expression
*expr
);
905 void __comparison_match_condition(struct expression
*expr
);
906 void __stored_condition(struct expression
*expr
);
907 void register_implications(int id
)
909 add_hook(&save_implications_hook
, CONDITION_HOOK
);
910 add_hook(&set_implied_states
, CONDITION_HOOK
);
911 add_hook(&__extra_match_condition
, CONDITION_HOOK
);
912 add_hook(&set_extra_implied_states
, CONDITION_HOOK
);
913 add_hook(&__comparison_match_condition
, CONDITION_HOOK
);
914 add_hook(&__stored_condition
, CONDITION_HOOK
);
915 add_hook(&match_end_func
, END_FUNC_HOOK
);