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_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 [stree %d] %s from %d\n", get_stree_id(sm
->pool
), show_sm(sm
), sm
->line
);
361 if (!is_merged(sm
) || pool_in_pools(sm
->pool
, keep_stack
)) {
362 DIMPLIED("kept [stree %d] %s from %d\n", get_stree_id(sm
->pool
), show_sm(sm
), sm
->line
);
366 DIMPLIED("checking [stree %d] %s from %d (%d) left = %s [stree %d] right = %s [stree %d]\n",
367 get_stree_id(sm
->pool
),
368 show_sm(sm
), sm
->line
, sm
->nr_children
,
369 sm
->left
? sm
->left
->state
->name
: "<none>", sm
->left
? get_stree_id(sm
->left
->pool
) : -1,
370 sm
->right
? sm
->right
->state
->name
: "<none>", sm
->right
? get_stree_id(sm
->right
->pool
) : -1);
371 left
= filter_pools(sm
->left
, remove_stack
, keep_stack
, &removed
);
372 right
= filter_pools(sm
->right
, remove_stack
, keep_stack
, &removed
);
374 DIMPLIED("kept [stree %d] %s from %d\n", get_stree_id(sm
->pool
), show_sm(sm
), sm
->line
);
378 if (!left
&& !right
) {
379 DIMPLIED("removed [stree %d] %s from %d <none>\n", get_stree_id(sm
->pool
), show_sm(sm
), sm
->line
);
384 ret
= clone_sm(right
);
389 ret
= clone_sm(left
);
394 ret
= merge_sm_states(left
, right
);
397 ret
->pool
= sm
->pool
;
400 DIMPLIED("partial %s => ", show_sm(sm
));
401 DIMPLIED("%s from %d [stree %d]\n", show_sm(ret
), sm
->line
, get_stree_id(sm
->pool
));
405 static int sm_in_keep_leafs(struct sm_state
*sm
, const struct state_list
*keep_gates
)
407 struct sm_state
*tmp
, *old
;
409 FOR_EACH_PTR(keep_gates
, tmp
) {
412 old
= get_sm_state_stree(tmp
->pool
, sm
->owner
, sm
->name
, sm
->sym
);
415 } END_FOR_EACH_PTR(tmp
);
419 static struct stree
*filter_stack(struct sm_state
*gate_sm
,
420 struct stree
*pre_stree
,
421 const struct state_list
*remove_stack
,
422 const struct state_list
*keep_stack
)
424 struct stree
*ret
= NULL
;
425 struct sm_state
*tmp
;
426 struct sm_state
*filtered_sm
;
432 FOR_EACH_SM(pre_stree
, tmp
) {
434 sm_msg("%s: %s", __func__
, show_sm(tmp
));
437 if (sm_in_keep_leafs(tmp
, keep_stack
))
440 filtered_sm
= filter_pools(tmp
, remove_stack
, keep_stack
, &modified
);
441 if (filtered_sm
&& modified
) {
442 /* the assignments here are for borrowed implications */
443 filtered_sm
->name
= tmp
->name
;
444 filtered_sm
->sym
= tmp
->sym
;
445 avl_insert(&ret
, filtered_sm
);
450 } END_FOR_EACH_SM(tmp
);
454 static void separate_and_filter(struct sm_state
*sm
, int comparison
, struct range_list
*rl
,
455 struct stree
*pre_stree
,
456 struct stree
**true_states
,
457 struct stree
**false_states
,
460 struct state_list
*true_stack
= NULL
;
461 struct state_list
*false_stack
= NULL
;
462 struct timeval time_before
;
463 struct timeval time_after
;
465 gettimeofday(&time_before
, NULL
);
467 if (!is_merged(sm
)) {
468 DIMPLIED("%d '%s' is not merged.\n", get_lineno(), sm
->name
);
472 if (option_debug_implied
|| option_debug
) {
473 sm_msg("checking implications: (%s %s %s)",
474 sm
->name
, show_special(comparison
), show_rl(rl
));
477 separate_pools(sm
, comparison
, rl
, &true_stack
, &false_stack
, NULL
, mixed
);
479 DIMPLIED("filtering true stack.\n");
480 *true_states
= filter_stack(sm
, pre_stree
, false_stack
, true_stack
);
481 DIMPLIED("filtering false stack.\n");
482 *false_states
= filter_stack(sm
, pre_stree
, true_stack
, false_stack
);
483 free_slist(&true_stack
);
484 free_slist(&false_stack
);
485 if (option_debug_implied
|| option_debug
) {
486 printf("These are the implied states for the true path:\n");
487 __print_stree(*true_states
);
488 printf("These are the implied states for the false path:\n");
489 __print_stree(*false_states
);
492 gettimeofday(&time_after
, NULL
);
493 if (time_after
.tv_sec
- time_before
.tv_sec
> 20) {
494 sm
->nr_children
= 4000;
495 sm_msg("Function too hairy. Giving up.");
499 static struct expression
*get_last_expr(struct statement
*stmt
)
501 struct statement
*last
;
503 last
= last_ptr_list((struct ptr_list
*)stmt
->stmts
);
504 if (last
->type
== STMT_EXPRESSION
)
505 return last
->expression
;
507 if (last
->type
== STMT_LABEL
) {
508 if (last
->label_statement
&&
509 last
->label_statement
->type
== STMT_EXPRESSION
)
510 return last
->label_statement
->expression
;
516 static struct expression
*get_left_most_expr(struct expression
*expr
)
518 struct statement
*compound
;
520 compound
= get_expression_statement(expr
);
522 return get_last_expr(compound
);
524 expr
= strip_parens(expr
);
525 if (expr
->type
== EXPR_ASSIGNMENT
)
526 return get_left_most_expr(expr
->left
);
530 static int is_merged_expr(struct expression
*expr
)
535 if (get_value(expr
, &dummy
))
537 sm
= get_sm_state_expr(SMATCH_EXTRA
, expr
);
545 static void delete_gate_sm_equiv(struct stree
**stree
, const char *name
, struct symbol
*sym
)
547 struct smatch_state
*state
;
548 struct relation
*rel
;
550 state
= get_state(SMATCH_EXTRA
, name
, sym
);
553 FOR_EACH_PTR(estate_related(state
), rel
) {
554 delete_state_stree(stree
, SMATCH_EXTRA
, rel
->name
, rel
->sym
);
555 } END_FOR_EACH_PTR(rel
);
558 static void delete_gate_sm(struct stree
**stree
, const char *name
, struct symbol
*sym
)
560 delete_state_stree(stree
, SMATCH_EXTRA
, name
, sym
);
563 static int handle_comparison(struct expression
*expr
,
564 struct stree
**implied_true
,
565 struct stree
**implied_false
)
567 struct sm_state
*sm
= NULL
;
568 struct range_list
*rl
= NULL
;
569 struct expression
*left
;
570 struct expression
*right
;
572 int comparison
= expr
->op
;
575 left
= get_left_most_expr(expr
->left
);
576 right
= get_left_most_expr(expr
->right
);
578 if (is_merged_expr(left
)) {
579 sm
= get_sm_state_expr(SMATCH_EXTRA
, left
);
580 get_implied_rl(right
, &rl
);
581 } else if (is_merged_expr(right
)) {
582 sm
= get_sm_state_expr(SMATCH_EXTRA
, right
);
583 get_implied_rl(left
, &rl
);
584 comparison
= flip_comparison(comparison
);
592 type
= get_type(expr
);
595 if (type_positive_bits(rl_type(rl
)) > type_positive_bits(type
))
597 if (type_positive_bits(type
) < 31)
599 rl
= cast_rl(type
, rl
);
601 separate_and_filter(sm
, comparison
, rl
, __get_cur_stree(), implied_true
, implied_false
, &mixed
);
604 delete_gate_sm_equiv(implied_true
, sm
->name
, sm
->sym
);
605 delete_gate_sm_equiv(implied_false
, sm
->name
, sm
->sym
);
607 delete_gate_sm(implied_true
, sm
->name
, sm
->sym
);
608 delete_gate_sm(implied_false
, sm
->name
, sm
->sym
);
614 static int handle_zero_comparison(struct expression
*expr
,
615 struct stree
**implied_true
,
616 struct stree
**implied_false
)
624 if (expr
->type
== EXPR_POSTOP
)
625 expr
= strip_expr(expr
->unop
);
627 if (expr
->type
== EXPR_ASSIGNMENT
) {
628 /* most of the time ->pools will be empty here because we
629 just set the state, but if have assigned a conditional
630 function there are implications. */
634 name
= expr_to_var_sym(expr
, &sym
);
637 sm
= get_sm_state(SMATCH_EXTRA
, name
, sym
);
641 separate_and_filter(sm
, SPECIAL_NOTEQUAL
, tmp_range_list(estate_type(sm
->state
), 0), __get_cur_stree(), implied_true
, implied_false
, &mixed
);
642 delete_gate_sm_equiv(implied_true
, sm
->name
, sm
->sym
);
643 delete_gate_sm_equiv(implied_false
, sm
->name
, sm
->sym
);
645 delete_gate_sm(implied_true
, sm
->name
, sm
->sym
);
646 delete_gate_sm(implied_false
, sm
->name
, sm
->sym
);
655 static int handled_by_implied_hook(struct expression
*expr
,
656 struct stree
**implied_true
,
657 struct stree
**implied_false
)
659 struct state_list
*true_stack
= NULL
;
660 struct state_list
*false_stack
= NULL
;
661 struct stree
*pre_stree
;
664 sm
= comparison_implication_hook(expr
, &true_stack
, &false_stack
);
668 pre_stree
= clone_stree(__get_cur_stree());
670 *implied_true
= filter_stack(sm
, pre_stree
, false_stack
, true_stack
);
671 *implied_false
= filter_stack(sm
, pre_stree
, true_stack
, false_stack
);
673 free_stree(&pre_stree
);
674 free_slist(&true_stack
);
675 free_slist(&false_stack
);
680 static int handled_by_extra_states(struct expression
*expr
,
681 struct stree
**implied_true
,
682 struct stree
**implied_false
)
684 if (expr
->type
== EXPR_COMPARE
)
685 return handle_comparison(expr
, implied_true
, implied_false
);
687 return handle_zero_comparison(expr
, implied_true
, implied_false
);
690 static int handled_by_stored_conditions(struct expression
*expr
,
691 struct stree
**implied_true
,
692 struct stree
**implied_false
)
694 struct state_list
*true_stack
= NULL
;
695 struct state_list
*false_stack
= NULL
;
696 struct stree
*pre_stree
;
699 sm
= stored_condition_implication_hook(expr
, &true_stack
, &false_stack
);
703 pre_stree
= clone_stree(__get_cur_stree());
705 *implied_true
= filter_stack(sm
, pre_stree
, false_stack
, true_stack
);
706 *implied_false
= filter_stack(sm
, pre_stree
, true_stack
, false_stack
);
708 free_stree(&pre_stree
);
709 free_slist(&true_stack
);
710 free_slist(&false_stack
);
715 static int found_implications
;
716 static struct stree
*saved_implied_true
;
717 static struct stree
*saved_implied_false
;
718 static struct stree
*extra_saved_implied_true
;
719 static struct stree
*extra_saved_implied_false
;
721 static void get_tf_states(struct expression
*expr
,
722 struct stree
**implied_true
,
723 struct stree
**implied_false
)
725 if (handled_by_implied_hook(expr
, implied_true
, implied_false
))
728 if (handled_by_extra_states(expr
, implied_true
, implied_false
)) {
729 /* We process these later. */
730 extra_saved_implied_true
= *implied_true
;
731 extra_saved_implied_false
= *implied_false
;
732 *implied_true
= NULL
;
733 *implied_false
= NULL
;
737 if (handled_by_stored_conditions(expr
, implied_true
, implied_false
))
742 found_implications
= 1;
745 static void save_implications_hook(struct expression
*expr
)
747 get_tf_states(expr
, &saved_implied_true
, &saved_implied_false
);
750 static void set_implied_states(struct expression
*expr
)
754 FOR_EACH_SM(saved_implied_true
, sm
) {
755 __set_true_false_sm(sm
, NULL
);
756 } END_FOR_EACH_SM(sm
);
757 free_stree(&saved_implied_true
);
759 FOR_EACH_SM(saved_implied_false
, sm
) {
760 __set_true_false_sm(NULL
, sm
);
761 } END_FOR_EACH_SM(sm
);
762 free_stree(&saved_implied_false
);
765 static void set_extra_implied_states(struct expression
*expr
)
767 saved_implied_true
= extra_saved_implied_true
;
768 saved_implied_false
= extra_saved_implied_false
;
769 extra_saved_implied_true
= NULL
;
770 extra_saved_implied_false
= NULL
;
771 set_implied_states(NULL
);
774 void param_limit_implications(struct expression
*expr
, int param
, char *key
, char *value
)
776 struct expression
*arg
;
777 struct symbol
*compare_type
;
781 struct sm_state
*tmp
;
782 struct stree
*implied_true
= NULL
;
783 struct stree
*implied_false
= NULL
;
784 struct range_list
*orig
, *limit
, *rl
;
786 while (expr
->type
== EXPR_ASSIGNMENT
)
787 expr
= strip_expr(expr
->right
);
788 if (expr
->type
!= EXPR_CALL
)
791 arg
= get_argument_from_call_expr(expr
->args
, param
);
795 name
= get_variable_from_key(arg
, key
, &sym
);
799 sm
= get_sm_state(SMATCH_EXTRA
, name
, sym
);
800 if (!sm
|| !sm
->merged
)
803 if (strcmp(key
, "$") == 0)
804 compare_type
= get_arg_type(expr
->fn
, param
);
806 compare_type
= get_member_type_from_key(arg
, key
);
808 orig
= estate_rl(sm
->state
);
809 orig
= cast_rl(compare_type
, orig
);
811 call_results_to_rl(expr
, compare_type
, value
, &limit
);
812 rl
= rl_intersection(orig
, limit
);
814 separate_and_filter(sm
, SPECIAL_EQUAL
, rl
, __get_cur_stree(), &implied_true
, &implied_false
, NULL
);
816 FOR_EACH_SM(implied_true
, tmp
) {
817 __set_sm_fake_stree(tmp
);
818 } END_FOR_EACH_SM(tmp
);
820 free_stree(&implied_true
);
821 free_stree(&implied_false
);
826 struct stree
*__implied_case_stree(struct expression
*switch_expr
,
827 struct range_list
*rl
,
828 struct range_list_stack
**remaining_cases
,
829 struct stree
**raw_stree
)
833 struct var_sym_list
*vsl
;
835 struct stree
*true_states
= NULL
;
836 struct stree
*false_states
= NULL
;
837 struct stree
*extra_states
;
838 struct stree
*ret
= clone_stree(*raw_stree
);
840 name
= expr_to_chunk_sym_vsl(switch_expr
, &sym
, &vsl
);
845 filter_top_rl(remaining_cases
, rl
);
847 rl
= clone_rl(top_rl(*remaining_cases
));
849 sm
= get_sm_state_stree(*raw_stree
, SMATCH_EXTRA
, name
, sym
);
851 separate_and_filter(sm
, SPECIAL_EQUAL
, rl
, *raw_stree
, &true_states
, &false_states
, NULL
);
853 __push_fake_cur_stree();
855 set_extra_nomod_vsl(name
, sym
, vsl
, alloc_estate_rl(rl
));
856 __pass_case_to_client(switch_expr
, rl
);
857 extra_states
= __pop_fake_cur_stree();
858 overwrite_stree(extra_states
, &true_states
);
859 overwrite_stree(true_states
, &ret
);
860 free_stree(&extra_states
);
861 free_stree(&true_states
);
862 free_stree(&false_states
);
868 static void match_end_func(struct symbol
*sym
)
872 implied_debug_msg
= NULL
;
875 static void get_tf_stacks_from_pool(struct sm_state
*gate_sm
,
876 struct sm_state
*pool_sm
,
877 struct state_list
**true_stack
,
878 struct state_list
**false_stack
)
880 struct sm_state
*tmp
;
881 int possibly_true
= 0;
886 if (strcmp(gate_sm
->state
->name
, pool_sm
->state
->name
) == 0) {
887 add_ptr_list(true_stack
, pool_sm
);
891 FOR_EACH_PTR(gate_sm
->possible
, tmp
) {
892 if (strcmp(tmp
->state
->name
, pool_sm
->state
->name
) == 0) {
896 } END_FOR_EACH_PTR(tmp
);
898 if (!possibly_true
) {
899 add_ptr_list(false_stack
, gate_sm
);
903 get_tf_stacks_from_pool(gate_sm
->left
, pool_sm
, true_stack
, false_stack
);
904 get_tf_stacks_from_pool(gate_sm
->right
, pool_sm
, true_stack
, false_stack
);
908 * The situation is we have a SMATCH_EXTRA state and we want to break it into
909 * each of the ->possible states and find the implications of each. The caller
910 * has to use __push_fake_cur_stree() to preserve the correct states so they
911 * can be restored later.
913 void overwrite_states_using_pool(struct sm_state
*gate_sm
, struct sm_state
*pool_sm
)
915 struct state_list
*true_stack
= NULL
;
916 struct state_list
*false_stack
= NULL
;
917 struct stree
*pre_stree
;
918 struct stree
*implied_true
;
919 struct sm_state
*tmp
;
924 get_tf_stacks_from_pool(gate_sm
, pool_sm
, &true_stack
, &false_stack
);
926 pre_stree
= clone_stree(__get_cur_stree());
928 implied_true
= filter_stack(gate_sm
, pre_stree
, false_stack
, true_stack
);
930 free_stree(&pre_stree
);
931 free_slist(&true_stack
);
932 free_slist(&false_stack
);
934 FOR_EACH_SM(implied_true
, tmp
) {
935 set_state(tmp
->owner
, tmp
->name
, tmp
->sym
, tmp
->state
);
936 } END_FOR_EACH_SM(tmp
);
938 free_stree(&implied_true
);
941 int assume(struct expression
*expr
)
943 int orig_final_pass
= final_pass
;
946 __push_fake_cur_stree();
947 found_implications
= 0;
948 __split_whole_condition(expr
);
949 final_pass
= orig_final_pass
;
951 if (!found_implications
) {
952 __discard_false_states();
953 __free_fake_cur_stree();
960 void end_assume(void)
962 __discard_false_states();
963 __free_fake_cur_stree();
966 void __extra_match_condition(struct expression
*expr
);
967 void __comparison_match_condition(struct expression
*expr
);
968 void __stored_condition(struct expression
*expr
);
969 void register_implications(int id
)
971 add_hook(&save_implications_hook
, CONDITION_HOOK
);
972 add_hook(&set_implied_states
, CONDITION_HOOK
);
973 add_hook(&__extra_match_condition
, CONDITION_HOOK
);
974 add_hook(&set_extra_implied_states
, CONDITION_HOOK
);
975 add_hook(&__comparison_match_condition
, CONDITION_HOOK
);
976 add_hook(&__stored_condition
, CONDITION_HOOK
);
977 add_hook(&match_end_func
, END_FUNC_HOOK
);