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
);
325 * NOTE: If a state is in both the keep stack and the remove stack then it is
326 * removed. If that happens it means you have a bug. Only add states which are
327 * definitely true or definitely false. If you have a leaf state that could be
328 * both true and false, then create a fake split history where one side is true
329 * and one side is false. Otherwise, if you can't do that, then don't add it to
330 * either list, and it will be treated as true.
332 struct sm_state
*filter_pools(struct sm_state
*sm
,
333 const struct state_list
*remove_stack
,
334 const struct state_list
*keep_stack
,
337 struct sm_state
*ret
= NULL
;
338 struct sm_state
*left
;
339 struct sm_state
*right
;
345 if (sm
->nr_children
> 4000) {
346 if (option_debug
|| option_debug_implied
) {
347 static char buf
[1028];
348 snprintf(buf
, sizeof(buf
), "debug: %s: nr_children over 4000 (%d). (%s %s)",
349 __func__
, sm
->nr_children
, sm
->name
, show_state(sm
->state
));
350 implied_debug_msg
= buf
;
355 if (pool_in_pools(sm
->pool
, remove_stack
)) {
356 DIMPLIED("removed %s from %d [stree %d]\n", show_sm(sm
), sm
->line
, get_stree_id(sm
->pool
));
361 if (!is_merged(sm
) || pool_in_pools(sm
->pool
, keep_stack
)) {
362 DIMPLIED("kept %s from %d [stree %d]\n", show_sm(sm
), sm
->line
, get_stree_id(sm
->pool
));
366 DIMPLIED("checking %s from %d (%d) [stree %d] left = %s [stree %d] right = %s [stree %d]\n",
367 show_sm(sm
), sm
->line
, sm
->nr_children
, get_stree_id(sm
->pool
),
368 sm
->left
? show_sm(sm
->left
) : "<none>", sm
->left
? get_stree_id(sm
->left
->pool
) : -1,
369 sm
->right
? show_sm(sm
->right
) : "<none>", sm
->right
? get_stree_id(sm
->right
->pool
) : -1);
370 left
= filter_pools(sm
->left
, remove_stack
, keep_stack
, &removed
);
371 right
= filter_pools(sm
->right
, remove_stack
, keep_stack
, &removed
);
373 DIMPLIED("kept %s from %d [stree %d]\n", show_sm(sm
), sm
->line
, get_stree_id(sm
->pool
));
377 if (!left
&& !right
) {
378 DIMPLIED("removed %s from %d <none> [stree %d]\n", show_sm(sm
), sm
->line
, get_stree_id(sm
->pool
));
383 ret
= clone_sm(right
);
388 ret
= clone_sm(left
);
393 ret
= merge_sm_states(left
, right
);
396 ret
->pool
= sm
->pool
;
399 DIMPLIED("partial %s => ", show_sm(sm
));
400 DIMPLIED("%s from %d [stree %d]\n", show_sm(ret
), sm
->line
, get_stree_id(sm
->pool
));
404 static int sm_in_keep_leafs(struct sm_state
*sm
, const struct state_list
*keep_gates
)
406 struct sm_state
*tmp
, *old
;
408 FOR_EACH_PTR(keep_gates
, tmp
) {
411 old
= get_sm_state_stree(tmp
->pool
, sm
->owner
, sm
->name
, sm
->sym
);
414 } END_FOR_EACH_PTR(tmp
);
418 static struct stree
*filter_stack(struct sm_state
*gate_sm
,
419 struct stree
*pre_stree
,
420 const struct state_list
*remove_stack
,
421 const struct state_list
*keep_stack
)
423 struct stree
*ret
= NULL
;
424 struct sm_state
*tmp
;
425 struct sm_state
*filtered_sm
;
431 FOR_EACH_SM(pre_stree
, tmp
) {
434 if (sm_in_keep_leafs(tmp
, keep_stack
))
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_last_expr(struct statement
*stmt
)
496 struct statement
*last
;
498 last
= last_ptr_list((struct ptr_list
*)stmt
->stmts
);
499 if (last
->type
== STMT_EXPRESSION
)
500 return last
->expression
;
502 if (last
->type
== STMT_LABEL
) {
503 if (last
->label_statement
&&
504 last
->label_statement
->type
== STMT_EXPRESSION
)
505 return last
->label_statement
->expression
;
511 static struct expression
*get_left_most_expr(struct expression
*expr
)
513 struct statement
*compound
;
515 compound
= get_expression_statement(expr
);
517 return get_last_expr(compound
);
519 expr
= strip_parens(expr
);
520 if (expr
->type
== EXPR_ASSIGNMENT
)
521 return get_left_most_expr(expr
->left
);
525 static int is_merged_expr(struct expression
*expr
)
530 if (get_value(expr
, &dummy
))
532 sm
= get_sm_state_expr(SMATCH_EXTRA
, expr
);
540 static void delete_gate_sm_equiv(struct stree
**stree
, const char *name
, struct symbol
*sym
)
542 struct smatch_state
*state
;
543 struct relation
*rel
;
545 state
= get_state(SMATCH_EXTRA
, name
, sym
);
548 FOR_EACH_PTR(estate_related(state
), rel
) {
549 delete_state_stree(stree
, SMATCH_EXTRA
, rel
->name
, rel
->sym
);
550 } END_FOR_EACH_PTR(rel
);
553 static void delete_gate_sm(struct stree
**stree
, const char *name
, struct symbol
*sym
)
555 delete_state_stree(stree
, SMATCH_EXTRA
, name
, sym
);
558 static int handle_comparison(struct expression
*expr
,
559 struct stree
**implied_true
,
560 struct stree
**implied_false
)
562 struct sm_state
*sm
= NULL
;
563 struct range_list
*rl
= NULL
;
564 struct expression
*left
;
565 struct expression
*right
;
567 int comparison
= expr
->op
;
570 left
= get_left_most_expr(expr
->left
);
571 right
= get_left_most_expr(expr
->right
);
573 if (is_merged_expr(left
)) {
574 sm
= get_sm_state_expr(SMATCH_EXTRA
, left
);
575 get_implied_rl(right
, &rl
);
576 } else if (is_merged_expr(right
)) {
577 sm
= get_sm_state_expr(SMATCH_EXTRA
, right
);
578 get_implied_rl(left
, &rl
);
579 comparison
= flip_comparison(comparison
);
587 type
= get_type(expr
);
590 if (type_positive_bits(rl_type(rl
)) > type_positive_bits(type
))
592 if (type_positive_bits(type
) < 31)
594 rl
= cast_rl(type
, rl
);
596 separate_and_filter(sm
, comparison
, rl
, __get_cur_stree(), implied_true
, implied_false
, &mixed
);
599 delete_gate_sm_equiv(implied_true
, sm
->name
, sm
->sym
);
600 delete_gate_sm_equiv(implied_false
, sm
->name
, sm
->sym
);
602 delete_gate_sm(implied_true
, sm
->name
, sm
->sym
);
603 delete_gate_sm(implied_false
, sm
->name
, sm
->sym
);
609 static int handle_zero_comparison(struct expression
*expr
,
610 struct stree
**implied_true
,
611 struct stree
**implied_false
)
619 if (expr
->type
== EXPR_POSTOP
)
620 expr
= strip_expr(expr
->unop
);
622 if (expr
->type
== EXPR_ASSIGNMENT
) {
623 /* most of the time ->pools will be empty here because we
624 just set the state, but if have assigned a conditional
625 function there are implications. */
629 name
= expr_to_var_sym(expr
, &sym
);
632 sm
= get_sm_state(SMATCH_EXTRA
, name
, sym
);
636 separate_and_filter(sm
, SPECIAL_NOTEQUAL
, tmp_range_list(estate_type(sm
->state
), 0), __get_cur_stree(), implied_true
, implied_false
, &mixed
);
637 delete_gate_sm_equiv(implied_true
, sm
->name
, sm
->sym
);
638 delete_gate_sm_equiv(implied_false
, sm
->name
, sm
->sym
);
640 delete_gate_sm(implied_true
, sm
->name
, sm
->sym
);
641 delete_gate_sm(implied_false
, sm
->name
, sm
->sym
);
650 static int handled_by_implied_hook(struct expression
*expr
,
651 struct stree
**implied_true
,
652 struct stree
**implied_false
)
654 struct state_list
*true_stack
= NULL
;
655 struct state_list
*false_stack
= NULL
;
656 struct stree
*pre_stree
;
659 sm
= comparison_implication_hook(expr
, &true_stack
, &false_stack
);
663 pre_stree
= clone_stree(__get_cur_stree());
665 *implied_true
= filter_stack(sm
, pre_stree
, false_stack
, true_stack
);
666 *implied_false
= filter_stack(sm
, pre_stree
, true_stack
, false_stack
);
668 free_stree(&pre_stree
);
669 free_slist(&true_stack
);
670 free_slist(&false_stack
);
675 static int handled_by_extra_states(struct expression
*expr
,
676 struct stree
**implied_true
,
677 struct stree
**implied_false
)
679 if (expr
->type
== EXPR_COMPARE
)
680 return handle_comparison(expr
, implied_true
, implied_false
);
682 return handle_zero_comparison(expr
, implied_true
, implied_false
);
685 static int handled_by_stored_conditions(struct expression
*expr
,
686 struct stree
**implied_true
,
687 struct stree
**implied_false
)
689 struct state_list
*true_stack
= NULL
;
690 struct state_list
*false_stack
= NULL
;
691 struct stree
*pre_stree
;
694 sm
= stored_condition_implication_hook(expr
, &true_stack
, &false_stack
);
698 pre_stree
= clone_stree(__get_cur_stree());
700 *implied_true
= filter_stack(sm
, pre_stree
, false_stack
, true_stack
);
701 *implied_false
= filter_stack(sm
, pre_stree
, true_stack
, false_stack
);
703 free_stree(&pre_stree
);
704 free_slist(&true_stack
);
705 free_slist(&false_stack
);
710 static int found_implications
;
711 static struct stree
*saved_implied_true
;
712 static struct stree
*saved_implied_false
;
713 static struct stree
*extra_saved_implied_true
;
714 static struct stree
*extra_saved_implied_false
;
716 static void get_tf_states(struct expression
*expr
,
717 struct stree
**implied_true
,
718 struct stree
**implied_false
)
720 if (handled_by_implied_hook(expr
, implied_true
, implied_false
))
723 if (handled_by_extra_states(expr
, implied_true
, implied_false
)) {
724 /* We process these later. */
725 extra_saved_implied_true
= *implied_true
;
726 extra_saved_implied_false
= *implied_false
;
727 *implied_true
= NULL
;
728 *implied_false
= NULL
;
732 if (handled_by_stored_conditions(expr
, implied_true
, implied_false
))
737 found_implications
= 1;
740 static void save_implications_hook(struct expression
*expr
)
742 get_tf_states(expr
, &saved_implied_true
, &saved_implied_false
);
745 static void set_implied_states(struct expression
*expr
)
749 FOR_EACH_SM(saved_implied_true
, sm
) {
750 __set_true_false_sm(sm
, NULL
);
751 } END_FOR_EACH_SM(sm
);
752 free_stree(&saved_implied_true
);
754 FOR_EACH_SM(saved_implied_false
, sm
) {
755 __set_true_false_sm(NULL
, sm
);
756 } END_FOR_EACH_SM(sm
);
757 free_stree(&saved_implied_false
);
760 static void set_extra_implied_states(struct expression
*expr
)
762 saved_implied_true
= extra_saved_implied_true
;
763 saved_implied_false
= extra_saved_implied_false
;
764 extra_saved_implied_true
= NULL
;
765 extra_saved_implied_false
= NULL
;
766 set_implied_states(NULL
);
769 void param_limit_implications(struct expression
*expr
, int param
, char *key
, char *value
)
771 struct expression
*arg
;
772 struct symbol
*compare_type
;
776 struct sm_state
*tmp
;
777 struct stree
*implied_true
= NULL
;
778 struct stree
*implied_false
= NULL
;
779 struct range_list
*orig
, *limit
, *rl
;
781 while (expr
->type
== EXPR_ASSIGNMENT
)
782 expr
= strip_expr(expr
->right
);
783 if (expr
->type
!= EXPR_CALL
)
786 arg
= get_argument_from_call_expr(expr
->args
, param
);
790 name
= get_variable_from_key(arg
, key
, &sym
);
794 sm
= get_sm_state(SMATCH_EXTRA
, name
, sym
);
795 if (!sm
|| !sm
->merged
)
798 if (strcmp(key
, "$") == 0)
799 compare_type
= get_arg_type(expr
->fn
, param
);
801 compare_type
= get_member_type_from_key(arg
, key
);
803 orig
= estate_rl(sm
->state
);
804 orig
= cast_rl(compare_type
, orig
);
806 call_results_to_rl(expr
, compare_type
, value
, &limit
);
807 rl
= rl_intersection(orig
, limit
);
809 separate_and_filter(sm
, SPECIAL_EQUAL
, rl
, __get_cur_stree(), &implied_true
, &implied_false
, NULL
);
811 FOR_EACH_SM(implied_true
, tmp
) {
812 __set_sm_fake_stree(tmp
);
813 } END_FOR_EACH_SM(tmp
);
815 free_stree(&implied_true
);
816 free_stree(&implied_false
);
821 struct stree
*__implied_case_stree(struct expression
*switch_expr
,
822 struct range_list
*rl
,
823 struct range_list_stack
**remaining_cases
,
824 struct stree
**raw_stree
)
828 struct var_sym_list
*vsl
;
830 struct stree
*true_states
= NULL
;
831 struct stree
*false_states
= NULL
;
832 struct stree
*extra_states
;
833 struct stree
*ret
= clone_stree(*raw_stree
);
835 name
= expr_to_chunk_sym_vsl(switch_expr
, &sym
, &vsl
);
840 filter_top_rl(remaining_cases
, rl
);
842 rl
= clone_rl(top_rl(*remaining_cases
));
844 sm
= get_sm_state_stree(*raw_stree
, SMATCH_EXTRA
, name
, sym
);
846 separate_and_filter(sm
, SPECIAL_EQUAL
, rl
, *raw_stree
, &true_states
, &false_states
, NULL
);
848 __push_fake_cur_stree();
850 set_extra_nomod_vsl(name
, sym
, vsl
, alloc_estate_rl(rl
));
851 __pass_case_to_client(switch_expr
, rl
);
852 extra_states
= __pop_fake_cur_stree();
853 overwrite_stree(extra_states
, &true_states
);
854 overwrite_stree(true_states
, &ret
);
855 free_stree(&extra_states
);
856 free_stree(&true_states
);
857 free_stree(&false_states
);
863 static void match_end_func(struct symbol
*sym
)
867 implied_debug_msg
= NULL
;
870 static int sm_state_in_slist(struct sm_state
*sm
, struct state_list
*slist
)
872 struct sm_state
*tmp
;
874 FOR_EACH_PTR(slist
, tmp
) {
877 } END_FOR_EACH_PTR(tmp
);
881 static void get_tf_stacks_from_pool(struct sm_state
*gate_sm
,
882 struct sm_state
*pool_sm
,
883 struct state_list
**true_stack
,
884 struct state_list
**false_stack
)
886 struct sm_state
*tmp
;
887 int possibly_true
= 0;
892 if (strcmp(gate_sm
->state
->name
, pool_sm
->state
->name
) == 0) {
893 add_ptr_list(true_stack
, pool_sm
);
897 FOR_EACH_PTR(gate_sm
->possible
, tmp
) {
898 if (strcmp(tmp
->state
->name
, pool_sm
->state
->name
) == 0) {
902 } END_FOR_EACH_PTR(tmp
);
904 if (!possibly_true
) {
905 add_ptr_list(false_stack
, gate_sm
);
909 get_tf_stacks_from_pool(gate_sm
->left
, pool_sm
, true_stack
, false_stack
);
910 get_tf_stacks_from_pool(gate_sm
->right
, pool_sm
, true_stack
, false_stack
);
914 * The situation is we have a SMATCH_EXTRA state and we want to break it into
915 * each of the ->possible states and find the implications of each. The caller
916 * has to use __push_fake_cur_stree() to preserve the correct states so they
917 * can be restored later.
919 void overwrite_states_using_pool(struct sm_state
*gate_sm
, struct sm_state
*pool_sm
)
921 struct state_list
*true_stack
= NULL
;
922 struct state_list
*false_stack
= NULL
;
923 struct stree
*pre_stree
;
924 struct stree
*implied_true
;
925 struct sm_state
*tmp
;
930 get_tf_stacks_from_pool(gate_sm
, pool_sm
, &true_stack
, &false_stack
);
932 pre_stree
= clone_stree(__get_cur_stree());
934 implied_true
= filter_stack(gate_sm
, pre_stree
, false_stack
, true_stack
);
936 free_stree(&pre_stree
);
937 free_slist(&true_stack
);
938 free_slist(&false_stack
);
940 FOR_EACH_SM(implied_true
, tmp
) {
941 set_state(tmp
->owner
, tmp
->name
, tmp
->sym
, tmp
->state
);
942 } END_FOR_EACH_SM(tmp
);
944 free_stree(&implied_true
);
947 int assume(struct expression
*expr
)
949 int orig_final_pass
= final_pass
;
952 __push_fake_cur_stree();
953 found_implications
= 0;
954 __split_whole_condition(expr
);
955 final_pass
= orig_final_pass
;
957 if (!found_implications
) {
958 __discard_false_states();
959 __free_fake_cur_stree();
966 void end_assume(void)
968 __discard_false_states();
969 __free_fake_cur_stree();
972 void __extra_match_condition(struct expression
*expr
);
973 void __comparison_match_condition(struct expression
*expr
);
974 void __stored_condition(struct expression
*expr
);
975 void register_implications(int id
)
977 add_hook(&save_implications_hook
, CONDITION_HOOK
);
978 add_hook(&set_implied_states
, CONDITION_HOOK
);
979 add_hook(&__extra_match_condition
, CONDITION_HOOK
);
980 add_hook(&set_extra_implied_states
, CONDITION_HOOK
);
981 add_hook(&__comparison_match_condition
, CONDITION_HOOK
);
982 add_hook(&__stored_condition
, CONDITION_HOOK
);
983 add_hook(&match_end_func
, END_FUNC_HOOK
);