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 * 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
)) {
264 add_pool(true_stack
, sm
);
266 add_pool(false_stack
, sm
);
268 add_pool(maybe_stack
, sm
);
272 static int is_checked(struct state_list
*checked
, struct sm_state
*sm
)
274 struct sm_state
*tmp
;
276 FOR_EACH_PTR(checked
, tmp
) {
279 } END_FOR_EACH_PTR(tmp
);
285 * Example code: if (foo == 99) {
287 * Say 'foo' is a merged state that has many possible values. It is the combination
288 * of merges. separate_pools() iterates through the pools recursively and calls
289 * do_compare() for each time 'foo' was set.
291 static void __separate_pools(struct sm_state
*sm
, int comparison
, struct range_list
*rl
,
292 struct state_list
**true_stack
,
293 struct state_list
**maybe_stack
,
294 struct state_list
**false_stack
,
295 struct state_list
**checked
, int *mixed
, struct sm_state
*gate_sm
)
297 int free_checked
= 0;
298 struct state_list
*checked_states
= NULL
;
304 * If it looks like this is going to take too long as-is, then don't
305 * create even more fake history.
307 if (mixed
&& sm
->nr_children
> 100)
311 Sometimes the implications are just too big to deal with
312 so we bail. Theoretically, bailing out here can cause more false
313 positives but won't hide actual bugs.
315 if (sm
->nr_children
> 4000) {
316 if (option_debug
|| option_debug_implied
) {
317 static char buf
[1028];
318 snprintf(buf
, sizeof(buf
), "debug: %s: nr_children over 4000 (%d). (%s %s)",
319 __func__
, sm
->nr_children
, sm
->name
, show_state(sm
->state
));
320 implied_debug_msg
= buf
;
325 if (checked
== NULL
) {
326 checked
= &checked_states
;
329 if (is_checked(*checked
, sm
))
331 add_ptr_list(checked
, sm
);
333 do_compare(sm
, comparison
, rl
, true_stack
, maybe_stack
, false_stack
, mixed
, gate_sm
);
335 __separate_pools(sm
->left
, comparison
, rl
, true_stack
, maybe_stack
, false_stack
, checked
, mixed
, gate_sm
);
336 __separate_pools(sm
->right
, comparison
, rl
, true_stack
, maybe_stack
, false_stack
, checked
, mixed
, gate_sm
);
341 static void separate_pools(struct sm_state
*sm
, int comparison
, struct range_list
*rl
,
342 struct state_list
**true_stack
,
343 struct state_list
**false_stack
,
344 struct state_list
**checked
, int *mixed
)
346 struct state_list
*maybe_stack
= NULL
;
347 struct sm_state
*tmp
;
349 __separate_pools(sm
, comparison
, rl
, true_stack
, &maybe_stack
, false_stack
, checked
, mixed
, sm
);
354 FOR_EACH_PTR(*true_stack
, sm
) {
355 sm_msg("TRUE %s [stree %d]", show_sm(sm
), get_stree_id(sm
->pool
));
356 } END_FOR_EACH_PTR(sm
);
358 FOR_EACH_PTR(maybe_stack
, sm
) {
359 sm_msg("MAYBE %s [stree %d]", show_sm(sm
), get_stree_id(sm
->pool
));
360 } END_FOR_EACH_PTR(sm
);
362 FOR_EACH_PTR(*false_stack
, sm
) {
363 sm_msg("FALSE %s [stree %d]", show_sm(sm
), get_stree_id(sm
->pool
));
364 } END_FOR_EACH_PTR(sm
);
366 /* if it's a maybe then remove it from the false stack */
367 FOR_EACH_PTR(maybe_stack
, tmp
) {
368 remove_pool(false_stack
, tmp
->pool
);
369 } END_FOR_EACH_PTR(tmp
);
371 /* and the true stack */
372 FOR_EACH_PTR(maybe_stack
, tmp
) {
373 remove_pool(true_stack
, tmp
->pool
);
374 } END_FOR_EACH_PTR(tmp
);
376 /* if it's both true and false remove it from both */
377 FOR_EACH_PTR(*true_stack
, tmp
) {
378 if (remove_pool(false_stack
, tmp
->pool
))
379 DELETE_CURRENT_PTR(tmp
);
380 } END_FOR_EACH_PTR(tmp
);
383 static int sm_in_keep_leafs(struct sm_state
*sm
, const struct state_list
*keep_gates
)
385 struct sm_state
*tmp
, *old
;
387 FOR_EACH_PTR(keep_gates
, tmp
) {
390 old
= get_sm_state_stree(tmp
->pool
, sm
->owner
, sm
->name
, sm
->sym
);
395 } END_FOR_EACH_PTR(tmp
);
400 * NOTE: If a state is in both the keep stack and the remove stack then it is
401 * removed. If that happens it means you have a bug. Only add states which are
402 * definitely true or definitely false. If you have a leaf state that could be
403 * both true and false, then create a fake split history where one side is true
404 * and one side is false. Otherwise, if you can't do that, then don't add it to
405 * either list, and it will be treated as true.
407 struct sm_state
*filter_pools(struct sm_state
*sm
,
408 const struct state_list
*remove_stack
,
409 const struct state_list
*keep_stack
,
412 struct sm_state
*ret
= NULL
;
413 struct sm_state
*left
;
414 struct sm_state
*right
;
420 if (sm
->nr_children
> 4000) {
421 if (option_debug
|| option_debug_implied
) {
422 static char buf
[1028];
423 snprintf(buf
, sizeof(buf
), "debug: %s: nr_children over 4000 (%d). (%s %s)",
424 __func__
, sm
->nr_children
, sm
->name
, show_state(sm
->state
));
425 implied_debug_msg
= buf
;
430 if (pool_in_pools(sm
->pool
, remove_stack
)) {
431 DIMPLIED("removed [stree %d] %s from %d\n", get_stree_id(sm
->pool
), show_sm(sm
), sm
->line
);
436 if (!is_merged(sm
) || pool_in_pools(sm
->pool
, keep_stack
) || sm_in_keep_leafs(sm
, keep_stack
)) {
437 DIMPLIED("kept [stree %d] %s from %d. %s. %s. %s.\n", get_stree_id(sm
->pool
), show_sm(sm
), sm
->line
,
438 is_merged(sm
) ? "merged" : "not merged",
439 pool_in_pools(sm
->pool
, keep_stack
) ? "not in keep pools" : "in keep pools",
440 sm_in_keep_leafs(sm
, keep_stack
) ? "reachable keep leaf" : "no keep leaf");
444 DIMPLIED("checking [stree %d] %s from %d (%d) left = %s [stree %d] right = %s [stree %d]\n",
445 get_stree_id(sm
->pool
),
446 show_sm(sm
), sm
->line
, sm
->nr_children
,
447 sm
->left
? sm
->left
->state
->name
: "<none>", sm
->left
? get_stree_id(sm
->left
->pool
) : -1,
448 sm
->right
? sm
->right
->state
->name
: "<none>", sm
->right
? get_stree_id(sm
->right
->pool
) : -1);
449 left
= filter_pools(sm
->left
, remove_stack
, keep_stack
, &removed
);
450 right
= filter_pools(sm
->right
, remove_stack
, keep_stack
, &removed
);
452 DIMPLIED("kept [stree %d] %s from %d\n", get_stree_id(sm
->pool
), show_sm(sm
), sm
->line
);
456 if (!left
&& !right
) {
457 DIMPLIED("removed [stree %d] %s from %d <none>\n", get_stree_id(sm
->pool
), show_sm(sm
), sm
->line
);
462 ret
= clone_sm(right
);
467 ret
= clone_sm(left
);
472 ret
= merge_sm_states(left
, right
);
475 ret
->pool
= sm
->pool
;
477 DIMPLIED("partial %s => ", show_sm(sm
));
478 DIMPLIED("%s from %d [stree %d]\n", show_sm(ret
), sm
->line
, get_stree_id(sm
->pool
));
482 static struct stree
*filter_stack(struct sm_state
*gate_sm
,
483 struct stree
*pre_stree
,
484 const struct state_list
*remove_stack
,
485 const struct state_list
*keep_stack
)
487 struct stree
*ret
= NULL
;
488 struct sm_state
*tmp
;
489 struct sm_state
*filtered_sm
;
495 FOR_EACH_SM(pre_stree
, tmp
) {
497 sm_msg("%s: %s", __func__
, show_sm(tmp
));
500 if (sm_in_keep_leafs(tmp
, keep_stack
))
503 filtered_sm
= filter_pools(tmp
, remove_stack
, keep_stack
, &modified
);
504 if (!filtered_sm
|| !modified
)
506 /* the assignments here are for borrowed implications */
507 filtered_sm
->name
= tmp
->name
;
508 filtered_sm
->sym
= tmp
->sym
;
509 avl_insert(&ret
, filtered_sm
);
513 } END_FOR_EACH_SM(tmp
);
517 static void separate_and_filter(struct sm_state
*sm
, int comparison
, struct range_list
*rl
,
518 struct stree
*pre_stree
,
519 struct stree
**true_states
,
520 struct stree
**false_states
,
523 struct state_list
*true_stack
= NULL
;
524 struct state_list
*false_stack
= NULL
;
525 struct timeval time_before
;
526 struct timeval time_after
;
528 gettimeofday(&time_before
, NULL
);
530 if (!is_merged(sm
)) {
531 DIMPLIED("%d '%s' is not merged.\n", get_lineno(), sm
->name
);
535 if (option_debug_implied
|| option_debug
) {
536 sm_msg("checking implications: (%s %s %s)",
537 sm
->name
, show_special(comparison
), show_rl(rl
));
540 separate_pools(sm
, comparison
, rl
, &true_stack
, &false_stack
, NULL
, mixed
);
542 DIMPLIED("filtering true stack.\n");
543 *true_states
= filter_stack(sm
, pre_stree
, false_stack
, true_stack
);
544 DIMPLIED("filtering false stack.\n");
545 *false_states
= filter_stack(sm
, pre_stree
, true_stack
, false_stack
);
546 free_slist(&true_stack
);
547 free_slist(&false_stack
);
548 if (option_debug_implied
|| option_debug
) {
549 printf("These are the implied states for the true path:\n");
550 __print_stree(*true_states
);
551 printf("These are the implied states for the false path:\n");
552 __print_stree(*false_states
);
555 gettimeofday(&time_after
, NULL
);
556 if (time_after
.tv_sec
- time_before
.tv_sec
> 20) {
557 sm
->nr_children
= 4000;
558 sm_msg("Function too hairy. Giving up.");
562 static struct expression
*get_last_expr(struct statement
*stmt
)
564 struct statement
*last
;
566 last
= last_ptr_list((struct ptr_list
*)stmt
->stmts
);
567 if (last
->type
== STMT_EXPRESSION
)
568 return last
->expression
;
570 if (last
->type
== STMT_LABEL
) {
571 if (last
->label_statement
&&
572 last
->label_statement
->type
== STMT_EXPRESSION
)
573 return last
->label_statement
->expression
;
579 static struct expression
*get_left_most_expr(struct expression
*expr
)
581 struct statement
*compound
;
583 compound
= get_expression_statement(expr
);
585 return get_last_expr(compound
);
587 expr
= strip_parens(expr
);
588 if (expr
->type
== EXPR_ASSIGNMENT
)
589 return get_left_most_expr(expr
->left
);
593 static int is_merged_expr(struct expression
*expr
)
598 if (get_value(expr
, &dummy
))
600 sm
= get_sm_state_expr(SMATCH_EXTRA
, expr
);
608 static void delete_gate_sm_equiv(struct stree
**stree
, const char *name
, struct symbol
*sym
)
610 struct smatch_state
*state
;
611 struct relation
*rel
;
613 state
= get_state(SMATCH_EXTRA
, name
, sym
);
616 FOR_EACH_PTR(estate_related(state
), rel
) {
617 delete_state_stree(stree
, SMATCH_EXTRA
, rel
->name
, rel
->sym
);
618 } END_FOR_EACH_PTR(rel
);
621 static void delete_gate_sm(struct stree
**stree
, const char *name
, struct symbol
*sym
)
623 delete_state_stree(stree
, SMATCH_EXTRA
, name
, sym
);
626 static int handle_comparison(struct expression
*expr
,
627 struct stree
**implied_true
,
628 struct stree
**implied_false
)
630 struct sm_state
*sm
= NULL
;
631 struct range_list
*rl
= NULL
;
632 struct expression
*left
;
633 struct expression
*right
;
635 int comparison
= expr
->op
;
638 left
= get_left_most_expr(expr
->left
);
639 right
= get_left_most_expr(expr
->right
);
641 if (is_merged_expr(left
)) {
642 sm
= get_sm_state_expr(SMATCH_EXTRA
, left
);
643 get_implied_rl(right
, &rl
);
644 } else if (is_merged_expr(right
)) {
645 sm
= get_sm_state_expr(SMATCH_EXTRA
, right
);
646 get_implied_rl(left
, &rl
);
647 comparison
= flip_comparison(comparison
);
655 type
= get_type(expr
);
658 if (type_positive_bits(rl_type(rl
)) > type_positive_bits(type
))
660 if (type_positive_bits(type
) < 31)
662 rl
= cast_rl(type
, rl
);
664 separate_and_filter(sm
, comparison
, rl
, __get_cur_stree(), implied_true
, implied_false
, &mixed
);
667 delete_gate_sm_equiv(implied_true
, sm
->name
, sm
->sym
);
668 delete_gate_sm_equiv(implied_false
, sm
->name
, sm
->sym
);
670 delete_gate_sm(implied_true
, sm
->name
, sm
->sym
);
671 delete_gate_sm(implied_false
, sm
->name
, sm
->sym
);
677 static int handle_zero_comparison(struct expression
*expr
,
678 struct stree
**implied_true
,
679 struct stree
**implied_false
)
687 if (expr
->type
== EXPR_POSTOP
)
688 expr
= strip_expr(expr
->unop
);
690 if (expr
->type
== EXPR_ASSIGNMENT
) {
691 /* most of the time ->pools will be empty here because we
692 just set the state, but if have assigned a conditional
693 function there are implications. */
697 name
= expr_to_var_sym(expr
, &sym
);
700 sm
= get_sm_state(SMATCH_EXTRA
, name
, sym
);
704 separate_and_filter(sm
, SPECIAL_NOTEQUAL
, tmp_range_list(estate_type(sm
->state
), 0), __get_cur_stree(), implied_true
, implied_false
, &mixed
);
705 delete_gate_sm_equiv(implied_true
, sm
->name
, sm
->sym
);
706 delete_gate_sm_equiv(implied_false
, sm
->name
, sm
->sym
);
708 delete_gate_sm(implied_true
, sm
->name
, sm
->sym
);
709 delete_gate_sm(implied_false
, sm
->name
, sm
->sym
);
718 static int handled_by_implied_hook(struct expression
*expr
,
719 struct stree
**implied_true
,
720 struct stree
**implied_false
)
722 struct state_list
*true_stack
= NULL
;
723 struct state_list
*false_stack
= NULL
;
724 struct stree
*pre_stree
;
727 sm
= comparison_implication_hook(expr
, &true_stack
, &false_stack
);
731 pre_stree
= clone_stree(__get_cur_stree());
733 *implied_true
= filter_stack(sm
, pre_stree
, false_stack
, true_stack
);
734 *implied_false
= filter_stack(sm
, pre_stree
, true_stack
, false_stack
);
736 free_stree(&pre_stree
);
737 free_slist(&true_stack
);
738 free_slist(&false_stack
);
743 static int handled_by_extra_states(struct expression
*expr
,
744 struct stree
**implied_true
,
745 struct stree
**implied_false
)
747 if (expr
->type
== EXPR_COMPARE
)
748 return handle_comparison(expr
, implied_true
, implied_false
);
750 return handle_zero_comparison(expr
, implied_true
, implied_false
);
753 static int handled_by_stored_conditions(struct expression
*expr
,
754 struct stree
**implied_true
,
755 struct stree
**implied_false
)
757 struct state_list
*true_stack
= NULL
;
758 struct state_list
*false_stack
= NULL
;
759 struct stree
*pre_stree
;
762 sm
= stored_condition_implication_hook(expr
, &true_stack
, &false_stack
);
766 pre_stree
= clone_stree(__get_cur_stree());
768 *implied_true
= filter_stack(sm
, pre_stree
, false_stack
, true_stack
);
769 *implied_false
= filter_stack(sm
, pre_stree
, true_stack
, false_stack
);
771 free_stree(&pre_stree
);
772 free_slist(&true_stack
);
773 free_slist(&false_stack
);
778 static int found_implications
;
779 static struct stree
*saved_implied_true
;
780 static struct stree
*saved_implied_false
;
781 static struct stree
*extra_saved_implied_true
;
782 static struct stree
*extra_saved_implied_false
;
784 static void get_tf_states(struct expression
*expr
,
785 struct stree
**implied_true
,
786 struct stree
**implied_false
)
788 if (handled_by_implied_hook(expr
, implied_true
, implied_false
))
791 if (handled_by_extra_states(expr
, implied_true
, implied_false
)) {
792 /* We process these later. */
793 extra_saved_implied_true
= *implied_true
;
794 extra_saved_implied_false
= *implied_false
;
795 *implied_true
= NULL
;
796 *implied_false
= NULL
;
800 if (handled_by_stored_conditions(expr
, implied_true
, implied_false
))
805 found_implications
= 1;
808 static void save_implications_hook(struct expression
*expr
)
810 get_tf_states(expr
, &saved_implied_true
, &saved_implied_false
);
813 static void set_implied_states(struct expression
*expr
)
817 FOR_EACH_SM(saved_implied_true
, sm
) {
818 __set_true_false_sm(sm
, NULL
);
819 } END_FOR_EACH_SM(sm
);
820 free_stree(&saved_implied_true
);
822 FOR_EACH_SM(saved_implied_false
, sm
) {
823 __set_true_false_sm(NULL
, sm
);
824 } END_FOR_EACH_SM(sm
);
825 free_stree(&saved_implied_false
);
828 static void set_extra_implied_states(struct expression
*expr
)
830 saved_implied_true
= extra_saved_implied_true
;
831 saved_implied_false
= extra_saved_implied_false
;
832 extra_saved_implied_true
= NULL
;
833 extra_saved_implied_false
= NULL
;
834 set_implied_states(NULL
);
837 void param_limit_implications(struct expression
*expr
, int param
, char *key
, char *value
)
839 struct expression
*arg
;
840 struct symbol
*compare_type
;
844 struct sm_state
*tmp
;
845 struct stree
*implied_true
= NULL
;
846 struct stree
*implied_false
= NULL
;
847 struct range_list
*orig
, *limit
, *rl
;
849 while (expr
->type
== EXPR_ASSIGNMENT
)
850 expr
= strip_expr(expr
->right
);
851 if (expr
->type
!= EXPR_CALL
)
854 arg
= get_argument_from_call_expr(expr
->args
, param
);
858 name
= get_variable_from_key(arg
, key
, &sym
);
862 sm
= get_sm_state(SMATCH_EXTRA
, name
, sym
);
863 if (!sm
|| !sm
->merged
)
866 if (strcmp(key
, "$") == 0)
867 compare_type
= get_arg_type(expr
->fn
, param
);
869 compare_type
= get_member_type_from_key(arg
, key
);
871 orig
= estate_rl(sm
->state
);
872 orig
= cast_rl(compare_type
, orig
);
874 call_results_to_rl(expr
, compare_type
, value
, &limit
);
875 rl
= rl_intersection(orig
, limit
);
877 separate_and_filter(sm
, SPECIAL_EQUAL
, rl
, __get_cur_stree(), &implied_true
, &implied_false
, NULL
);
879 FOR_EACH_SM(implied_true
, tmp
) {
880 __set_sm_fake_stree(tmp
);
881 } END_FOR_EACH_SM(tmp
);
883 free_stree(&implied_true
);
884 free_stree(&implied_false
);
889 struct stree
*__implied_case_stree(struct expression
*switch_expr
,
890 struct range_list
*rl
,
891 struct range_list_stack
**remaining_cases
,
892 struct stree
**raw_stree
)
896 struct var_sym_list
*vsl
;
898 struct stree
*true_states
= NULL
;
899 struct stree
*false_states
= NULL
;
900 struct stree
*extra_states
;
901 struct stree
*ret
= clone_stree(*raw_stree
);
903 name
= expr_to_chunk_sym_vsl(switch_expr
, &sym
, &vsl
);
906 filter_top_rl(remaining_cases
, rl
);
908 rl
= clone_rl(top_rl(*remaining_cases
));
911 sm
= get_sm_state_stree(*raw_stree
, SMATCH_EXTRA
, name
, sym
);
913 separate_and_filter(sm
, SPECIAL_EQUAL
, rl
, *raw_stree
, &true_states
, &false_states
, NULL
);
916 __push_fake_cur_stree();
919 set_extra_nomod_vsl(name
, sym
, vsl
, alloc_estate_rl(rl
));
920 __pass_case_to_client(switch_expr
, rl
);
921 extra_states
= __pop_fake_cur_stree();
922 overwrite_stree(extra_states
, &true_states
);
923 overwrite_stree(true_states
, &ret
);
924 free_stree(&extra_states
);
925 free_stree(&true_states
);
926 free_stree(&false_states
);
932 static void match_end_func(struct symbol
*sym
)
936 implied_debug_msg
= NULL
;
939 static void get_tf_stacks_from_pool(struct sm_state
*gate_sm
,
940 struct sm_state
*pool_sm
,
941 struct state_list
**true_stack
,
942 struct state_list
**false_stack
)
944 struct sm_state
*tmp
;
945 int possibly_true
= 0;
950 if (strcmp(gate_sm
->state
->name
, pool_sm
->state
->name
) == 0) {
951 add_ptr_list(true_stack
, pool_sm
);
955 FOR_EACH_PTR(gate_sm
->possible
, tmp
) {
956 if (strcmp(tmp
->state
->name
, pool_sm
->state
->name
) == 0) {
960 } END_FOR_EACH_PTR(tmp
);
962 if (!possibly_true
) {
963 add_ptr_list(false_stack
, gate_sm
);
967 get_tf_stacks_from_pool(gate_sm
->left
, pool_sm
, true_stack
, false_stack
);
968 get_tf_stacks_from_pool(gate_sm
->right
, pool_sm
, true_stack
, false_stack
);
972 * The situation is we have a SMATCH_EXTRA state and we want to break it into
973 * each of the ->possible states and find the implications of each. The caller
974 * has to use __push_fake_cur_stree() to preserve the correct states so they
975 * can be restored later.
977 void overwrite_states_using_pool(struct sm_state
*gate_sm
, struct sm_state
*pool_sm
)
979 struct state_list
*true_stack
= NULL
;
980 struct state_list
*false_stack
= NULL
;
981 struct stree
*pre_stree
;
982 struct stree
*implied_true
;
983 struct sm_state
*tmp
;
988 get_tf_stacks_from_pool(gate_sm
, pool_sm
, &true_stack
, &false_stack
);
990 pre_stree
= clone_stree(__get_cur_stree());
992 implied_true
= filter_stack(gate_sm
, pre_stree
, false_stack
, true_stack
);
994 free_stree(&pre_stree
);
995 free_slist(&true_stack
);
996 free_slist(&false_stack
);
998 FOR_EACH_SM(implied_true
, tmp
) {
999 set_state(tmp
->owner
, tmp
->name
, tmp
->sym
, tmp
->state
);
1000 } END_FOR_EACH_SM(tmp
);
1002 free_stree(&implied_true
);
1005 int assume(struct expression
*expr
)
1007 int orig_final_pass
= final_pass
;
1010 __push_fake_cur_stree();
1011 found_implications
= 0;
1012 __split_whole_condition(expr
);
1013 final_pass
= orig_final_pass
;
1015 if (!found_implications
) {
1016 __discard_false_states();
1017 __free_fake_cur_stree();
1024 void end_assume(void)
1026 __discard_false_states();
1027 __free_fake_cur_stree();
1030 void __extra_match_condition(struct expression
*expr
);
1031 void __comparison_match_condition(struct expression
*expr
);
1032 void __stored_condition(struct expression
*expr
);
1033 void register_implications(int id
)
1035 add_hook(&save_implications_hook
, CONDITION_HOOK
);
1036 add_hook(&set_implied_states
, CONDITION_HOOK
);
1037 add_hook(&__extra_match_condition
, CONDITION_HOOK
);
1038 add_hook(&set_extra_implied_states
, CONDITION_HOOK
);
1039 add_hook(&__comparison_match_condition
, CONDITION_HOOK
);
1040 add_hook(&__stored_condition
, CONDITION_HOOK
);
1041 add_hook(&match_end_func
, END_FUNC_HOOK
);