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 */
367 FOR_EACH_PTR(maybe_stack
, tmp
) {
368 remove_pool(false_stack
, tmp
->pool
);
369 remove_pool(true_stack
, tmp
->pool
);
370 } END_FOR_EACH_PTR(tmp
);
372 /* if it's both true and false remove it from both */
373 FOR_EACH_PTR(*true_stack
, tmp
) {
374 if (remove_pool(false_stack
, tmp
->pool
))
375 DELETE_CURRENT_PTR(tmp
);
376 } END_FOR_EACH_PTR(tmp
);
379 static int sm_in_keep_leafs(struct sm_state
*sm
, const struct state_list
*keep_gates
)
381 struct sm_state
*tmp
, *old
;
383 FOR_EACH_PTR(keep_gates
, tmp
) {
386 old
= get_sm_state_stree(tmp
->pool
, sm
->owner
, sm
->name
, sm
->sym
);
391 } END_FOR_EACH_PTR(tmp
);
396 * NOTE: If a state is in both the keep stack and the remove stack then it is
397 * removed. If that happens it means you have a bug. Only add states which are
398 * definitely true or definitely false. If you have a leaf state that could be
399 * both true and false, then create a fake split history where one side is true
400 * and one side is false. Otherwise, if you can't do that, then don't add it to
401 * either list, and it will be treated as true.
403 struct sm_state
*filter_pools(struct sm_state
*sm
,
404 const struct state_list
*remove_stack
,
405 const struct state_list
*keep_stack
,
408 struct sm_state
*ret
= NULL
;
409 struct sm_state
*left
;
410 struct sm_state
*right
;
416 if (sm
->nr_children
> 4000) {
417 if (option_debug
|| option_debug_implied
) {
418 static char buf
[1028];
419 snprintf(buf
, sizeof(buf
), "debug: %s: nr_children over 4000 (%d). (%s %s)",
420 __func__
, sm
->nr_children
, sm
->name
, show_state(sm
->state
));
421 implied_debug_msg
= buf
;
426 if (pool_in_pools(sm
->pool
, remove_stack
)) {
427 DIMPLIED("removed [stree %d] %s from %d\n", get_stree_id(sm
->pool
), show_sm(sm
), sm
->line
);
432 if (!is_merged(sm
) || pool_in_pools(sm
->pool
, keep_stack
) || sm_in_keep_leafs(sm
, keep_stack
)) {
433 DIMPLIED("kept [stree %d] %s from %d. %s. %s. %s.\n", get_stree_id(sm
->pool
), show_sm(sm
), sm
->line
,
434 is_merged(sm
) ? "merged" : "not merged",
435 pool_in_pools(sm
->pool
, keep_stack
) ? "not in keep pools" : "in keep pools",
436 sm_in_keep_leafs(sm
, keep_stack
) ? "reachable keep leaf" : "no keep leaf");
440 DIMPLIED("checking [stree %d] %s from %d (%d) left = %s [stree %d] right = %s [stree %d]\n",
441 get_stree_id(sm
->pool
),
442 show_sm(sm
), sm
->line
, sm
->nr_children
,
443 sm
->left
? sm
->left
->state
->name
: "<none>", sm
->left
? get_stree_id(sm
->left
->pool
) : -1,
444 sm
->right
? sm
->right
->state
->name
: "<none>", sm
->right
? get_stree_id(sm
->right
->pool
) : -1);
445 left
= filter_pools(sm
->left
, remove_stack
, keep_stack
, &removed
);
446 right
= filter_pools(sm
->right
, remove_stack
, keep_stack
, &removed
);
448 DIMPLIED("kept [stree %d] %s from %d\n", get_stree_id(sm
->pool
), show_sm(sm
), sm
->line
);
452 if (!left
&& !right
) {
453 DIMPLIED("removed [stree %d] %s from %d <none>\n", get_stree_id(sm
->pool
), show_sm(sm
), sm
->line
);
458 ret
= clone_sm(right
);
463 ret
= clone_sm(left
);
468 if (left
->sym
!= sm
->sym
|| strcmp(left
->name
, sm
->name
) != 0) {
469 left
= clone_sm(left
);
471 left
->name
= sm
->name
;
473 if (right
->sym
!= sm
->sym
|| strcmp(right
->name
, sm
->name
) != 0) {
474 right
= clone_sm(right
);
475 right
->sym
= sm
->sym
;
476 right
->name
= sm
->name
;
478 ret
= merge_sm_states(left
, right
);
481 ret
->pool
= sm
->pool
;
483 DIMPLIED("partial %s => ", show_sm(sm
));
484 DIMPLIED("%s from %d [stree %d]\n", show_sm(ret
), sm
->line
, get_stree_id(sm
->pool
));
488 static struct stree
*filter_stack(struct sm_state
*gate_sm
,
489 struct stree
*pre_stree
,
490 const struct state_list
*remove_stack
,
491 const struct state_list
*keep_stack
)
493 struct stree
*ret
= NULL
;
494 struct sm_state
*tmp
;
495 struct sm_state
*filtered_sm
;
501 FOR_EACH_SM(pre_stree
, tmp
) {
503 sm_msg("%s: %s", __func__
, show_sm(tmp
));
506 if (sm_in_keep_leafs(tmp
, keep_stack
))
509 filtered_sm
= filter_pools(tmp
, remove_stack
, keep_stack
, &modified
);
510 if (!filtered_sm
|| !modified
)
512 /* the assignments here are for borrowed implications */
513 filtered_sm
->name
= tmp
->name
;
514 filtered_sm
->sym
= tmp
->sym
;
515 avl_insert(&ret
, filtered_sm
);
519 } END_FOR_EACH_SM(tmp
);
523 static void separate_and_filter(struct sm_state
*sm
, int comparison
, struct range_list
*rl
,
524 struct stree
*pre_stree
,
525 struct stree
**true_states
,
526 struct stree
**false_states
,
529 struct state_list
*true_stack
= NULL
;
530 struct state_list
*false_stack
= NULL
;
531 struct timeval time_before
;
532 struct timeval time_after
;
535 gettimeofday(&time_before
, NULL
);
537 if (!is_merged(sm
)) {
538 DIMPLIED("%d '%s' is not merged.\n", get_lineno(), sm
->name
);
542 if (option_debug_implied
|| option_debug
) {
543 sm_msg("checking implications: (%s %s %s)",
544 sm
->name
, show_special(comparison
), show_rl(rl
));
547 separate_pools(sm
, comparison
, rl
, &true_stack
, &false_stack
, NULL
, mixed
);
549 DIMPLIED("filtering true stack.\n");
550 *true_states
= filter_stack(sm
, pre_stree
, false_stack
, true_stack
);
551 DIMPLIED("filtering false stack.\n");
552 *false_states
= filter_stack(sm
, pre_stree
, true_stack
, false_stack
);
553 free_slist(&true_stack
);
554 free_slist(&false_stack
);
555 if (option_debug_implied
|| option_debug
) {
556 printf("These are the implied states for the true path: (%s %s %s)\n",
557 sm
->name
, show_special(comparison
), show_rl(rl
));
558 __print_stree(*true_states
);
559 printf("These are the implied states for the false path: (%s %s %s)\n",
560 sm
->name
, show_special(comparison
), show_rl(rl
));
561 __print_stree(*false_states
);
564 gettimeofday(&time_after
, NULL
);
565 sec
= time_after
.tv_sec
- time_before
.tv_sec
;
567 sm
->nr_children
= 4000;
568 sm_msg("Function too hairy. Ignoring implications after %d seconds.", sec
);
572 static struct expression
*get_last_expr(struct statement
*stmt
)
574 struct statement
*last
;
576 last
= last_ptr_list((struct ptr_list
*)stmt
->stmts
);
577 if (last
->type
== STMT_EXPRESSION
)
578 return last
->expression
;
580 if (last
->type
== STMT_LABEL
) {
581 if (last
->label_statement
&&
582 last
->label_statement
->type
== STMT_EXPRESSION
)
583 return last
->label_statement
->expression
;
589 static struct expression
*get_left_most_expr(struct expression
*expr
)
591 struct statement
*compound
;
593 compound
= get_expression_statement(expr
);
595 return get_last_expr(compound
);
597 expr
= strip_parens(expr
);
598 if (expr
->type
== EXPR_ASSIGNMENT
)
599 return get_left_most_expr(expr
->left
);
603 static int is_merged_expr(struct expression
*expr
)
608 if (get_value(expr
, &dummy
))
610 sm
= get_sm_state_expr(SMATCH_EXTRA
, expr
);
618 static void delete_gate_sm_equiv(struct stree
**stree
, const char *name
, struct symbol
*sym
)
620 struct smatch_state
*state
;
621 struct relation
*rel
;
623 state
= get_state(SMATCH_EXTRA
, name
, sym
);
626 FOR_EACH_PTR(estate_related(state
), rel
) {
627 delete_state_stree(stree
, SMATCH_EXTRA
, rel
->name
, rel
->sym
);
628 } END_FOR_EACH_PTR(rel
);
631 static void delete_gate_sm(struct stree
**stree
, const char *name
, struct symbol
*sym
)
633 delete_state_stree(stree
, SMATCH_EXTRA
, name
, sym
);
636 static int handle_comparison(struct expression
*expr
,
637 struct stree
**implied_true
,
638 struct stree
**implied_false
)
640 struct sm_state
*sm
= NULL
;
641 struct range_list
*rl
= NULL
;
642 struct expression
*left
;
643 struct expression
*right
;
645 int comparison
= expr
->op
;
648 left
= get_left_most_expr(expr
->left
);
649 right
= get_left_most_expr(expr
->right
);
651 if (is_merged_expr(left
)) {
652 sm
= get_sm_state_expr(SMATCH_EXTRA
, left
);
653 get_implied_rl(right
, &rl
);
654 } else if (is_merged_expr(right
)) {
655 sm
= get_sm_state_expr(SMATCH_EXTRA
, right
);
656 get_implied_rl(left
, &rl
);
657 comparison
= flip_comparison(comparison
);
665 type
= get_type(expr
);
668 if (type_positive_bits(rl_type(rl
)) > type_positive_bits(type
))
670 if (type_positive_bits(type
) < 31)
672 rl
= cast_rl(type
, rl
);
674 separate_and_filter(sm
, comparison
, rl
, __get_cur_stree(), implied_true
, implied_false
, &mixed
);
677 delete_gate_sm_equiv(implied_true
, sm
->name
, sm
->sym
);
678 delete_gate_sm_equiv(implied_false
, sm
->name
, sm
->sym
);
680 delete_gate_sm(implied_true
, sm
->name
, sm
->sym
);
681 delete_gate_sm(implied_false
, sm
->name
, sm
->sym
);
687 static int handle_zero_comparison(struct expression
*expr
,
688 struct stree
**implied_true
,
689 struct stree
**implied_false
)
697 if (expr
->type
== EXPR_POSTOP
)
698 expr
= strip_expr(expr
->unop
);
700 if (expr
->type
== EXPR_ASSIGNMENT
) {
701 /* most of the time ->pools will be empty here because we
702 just set the state, but if have assigned a conditional
703 function there are implications. */
707 name
= expr_to_var_sym(expr
, &sym
);
710 sm
= get_sm_state(SMATCH_EXTRA
, name
, sym
);
714 separate_and_filter(sm
, SPECIAL_NOTEQUAL
, tmp_range_list(estate_type(sm
->state
), 0), __get_cur_stree(), implied_true
, implied_false
, &mixed
);
715 delete_gate_sm_equiv(implied_true
, sm
->name
, sm
->sym
);
716 delete_gate_sm_equiv(implied_false
, sm
->name
, sm
->sym
);
718 delete_gate_sm(implied_true
, sm
->name
, sm
->sym
);
719 delete_gate_sm(implied_false
, sm
->name
, sm
->sym
);
728 static int handled_by_comparison_hook(struct expression
*expr
,
729 struct stree
**implied_true
,
730 struct stree
**implied_false
)
732 struct state_list
*true_stack
= NULL
;
733 struct state_list
*false_stack
= NULL
;
734 struct stree
*pre_stree
;
737 sm
= comparison_implication_hook(expr
, &true_stack
, &false_stack
);
741 pre_stree
= clone_stree(__get_cur_stree());
743 *implied_true
= filter_stack(sm
, pre_stree
, false_stack
, true_stack
);
744 *implied_false
= filter_stack(sm
, pre_stree
, true_stack
, false_stack
);
746 free_stree(&pre_stree
);
747 free_slist(&true_stack
);
748 free_slist(&false_stack
);
753 static int handled_by_extra_states(struct expression
*expr
,
754 struct stree
**implied_true
,
755 struct stree
**implied_false
)
757 if (expr
->type
== EXPR_COMPARE
)
758 return handle_comparison(expr
, implied_true
, implied_false
);
760 return handle_zero_comparison(expr
, implied_true
, implied_false
);
763 static int handled_by_stored_conditions(struct expression
*expr
,
764 struct stree
**implied_true
,
765 struct stree
**implied_false
)
767 struct state_list
*true_stack
= NULL
;
768 struct state_list
*false_stack
= NULL
;
769 struct stree
*pre_stree
;
772 sm
= stored_condition_implication_hook(expr
, &true_stack
, &false_stack
);
776 pre_stree
= clone_stree(__get_cur_stree());
778 *implied_true
= filter_stack(sm
, pre_stree
, false_stack
, true_stack
);
779 *implied_false
= filter_stack(sm
, pre_stree
, true_stack
, false_stack
);
781 free_stree(&pre_stree
);
782 free_slist(&true_stack
);
783 free_slist(&false_stack
);
788 static int found_implications
;
789 static struct stree
*saved_implied_true
;
790 static struct stree
*saved_implied_false
;
791 static struct stree
*extra_saved_implied_true
;
792 static struct stree
*extra_saved_implied_false
;
794 static void separate_extra_states(struct stree
**implied_true
,
795 struct stree
**implied_false
)
799 /* We process extra states later to preserve the implications. */
800 FOR_EACH_SM(*implied_true
, sm
) {
801 if (sm
->owner
== SMATCH_EXTRA
)
802 overwrite_sm_state_stree(&extra_saved_implied_true
, sm
);
803 } END_FOR_EACH_SM(sm
);
804 FOR_EACH_SM(extra_saved_implied_true
, sm
) {
805 delete_state_stree(implied_true
, sm
->owner
, sm
->name
, sm
->sym
);
806 } END_FOR_EACH_SM(sm
);
808 FOR_EACH_SM(*implied_false
, sm
) {
809 if (sm
->owner
== SMATCH_EXTRA
)
810 overwrite_sm_state_stree(&extra_saved_implied_false
, sm
);
811 } END_FOR_EACH_SM(sm
);
812 FOR_EACH_SM(extra_saved_implied_false
, sm
) {
813 delete_state_stree(implied_false
, sm
->owner
, sm
->name
, sm
->sym
);
814 } END_FOR_EACH_SM(sm
);
817 static void get_tf_states(struct expression
*expr
,
818 struct stree
**implied_true
,
819 struct stree
**implied_false
)
821 if (handled_by_comparison_hook(expr
, implied_true
, implied_false
))
824 if (handled_by_extra_states(expr
, implied_true
, implied_false
)) {
825 separate_extra_states(implied_true
, implied_false
);
829 if (handled_by_stored_conditions(expr
, implied_true
, implied_false
))
834 found_implications
= 1;
837 static void save_implications_hook(struct expression
*expr
)
839 if (time_parsing_function() > 60)
841 get_tf_states(expr
, &saved_implied_true
, &saved_implied_false
);
844 static void set_implied_states(struct expression
*expr
)
848 FOR_EACH_SM(saved_implied_true
, sm
) {
849 __set_true_false_sm(sm
, NULL
);
850 } END_FOR_EACH_SM(sm
);
851 free_stree(&saved_implied_true
);
853 FOR_EACH_SM(saved_implied_false
, sm
) {
854 __set_true_false_sm(NULL
, sm
);
855 } END_FOR_EACH_SM(sm
);
856 free_stree(&saved_implied_false
);
859 static void set_extra_implied_states(struct expression
*expr
)
861 saved_implied_true
= extra_saved_implied_true
;
862 saved_implied_false
= extra_saved_implied_false
;
863 extra_saved_implied_true
= NULL
;
864 extra_saved_implied_false
= NULL
;
865 set_implied_states(NULL
);
868 void param_limit_implications(struct expression
*expr
, int param
, char *key
, char *value
)
870 struct expression
*arg
;
871 struct symbol
*compare_type
;
875 struct sm_state
*tmp
;
876 struct stree
*implied_true
= NULL
;
877 struct stree
*implied_false
= NULL
;
878 struct range_list
*orig
, *limit
;
880 while (expr
->type
== EXPR_ASSIGNMENT
)
881 expr
= strip_expr(expr
->right
);
882 if (expr
->type
!= EXPR_CALL
)
885 arg
= get_argument_from_call_expr(expr
->args
, param
);
889 name
= get_variable_from_key(arg
, key
, &sym
);
893 sm
= get_sm_state(SMATCH_EXTRA
, name
, sym
);
894 if (!sm
|| !sm
->merged
)
897 if (strcmp(key
, "$") == 0)
898 compare_type
= get_arg_type(expr
->fn
, param
);
900 compare_type
= get_member_type_from_key(arg
, key
);
902 orig
= estate_rl(sm
->state
);
903 orig
= cast_rl(compare_type
, orig
);
905 call_results_to_rl(expr
, compare_type
, value
, &limit
);
907 separate_and_filter(sm
, SPECIAL_EQUAL
, limit
, __get_cur_stree(), &implied_true
, &implied_false
, NULL
);
909 FOR_EACH_SM(implied_true
, tmp
) {
910 __set_sm_fake_stree(tmp
);
911 } END_FOR_EACH_SM(tmp
);
913 free_stree(&implied_true
);
914 free_stree(&implied_false
);
919 struct stree
*__implied_case_stree(struct expression
*switch_expr
,
920 struct range_list
*rl
,
921 struct range_list_stack
**remaining_cases
,
922 struct stree
**raw_stree
)
926 struct var_sym_list
*vsl
;
928 struct stree
*true_states
= NULL
;
929 struct stree
*false_states
= NULL
;
930 struct stree
*extra_states
;
931 struct stree
*ret
= clone_stree(*raw_stree
);
933 name
= expr_to_chunk_sym_vsl(switch_expr
, &sym
, &vsl
);
936 filter_top_rl(remaining_cases
, rl
);
938 rl
= clone_rl(top_rl(*remaining_cases
));
941 sm
= get_sm_state_stree(*raw_stree
, SMATCH_EXTRA
, name
, sym
);
943 separate_and_filter(sm
, SPECIAL_EQUAL
, rl
, *raw_stree
, &true_states
, &false_states
, NULL
);
946 __push_fake_cur_stree();
949 set_extra_nomod_vsl(name
, sym
, vsl
, NULL
, alloc_estate_rl(rl
));
950 __pass_case_to_client(switch_expr
, rl
);
951 extra_states
= __pop_fake_cur_stree();
952 overwrite_stree(extra_states
, &true_states
);
953 overwrite_stree(true_states
, &ret
);
954 free_stree(&extra_states
);
955 free_stree(&true_states
);
956 free_stree(&false_states
);
962 static void match_end_func(struct symbol
*sym
)
966 implied_debug_msg
= NULL
;
969 static void get_tf_stacks_from_pool(struct sm_state
*gate_sm
,
970 struct sm_state
*pool_sm
,
971 struct state_list
**true_stack
,
972 struct state_list
**false_stack
)
974 struct sm_state
*tmp
;
975 int possibly_true
= 0;
980 if (strcmp(gate_sm
->state
->name
, pool_sm
->state
->name
) == 0) {
981 add_ptr_list(true_stack
, pool_sm
);
985 FOR_EACH_PTR(gate_sm
->possible
, tmp
) {
986 if (strcmp(tmp
->state
->name
, pool_sm
->state
->name
) == 0) {
990 } END_FOR_EACH_PTR(tmp
);
992 if (!possibly_true
) {
993 add_ptr_list(false_stack
, gate_sm
);
997 get_tf_stacks_from_pool(gate_sm
->left
, pool_sm
, true_stack
, false_stack
);
998 get_tf_stacks_from_pool(gate_sm
->right
, pool_sm
, true_stack
, false_stack
);
1002 * The situation is we have a SMATCH_EXTRA state and we want to break it into
1003 * each of the ->possible states and find the implications of each. The caller
1004 * has to use __push_fake_cur_stree() to preserve the correct states so they
1005 * can be restored later.
1007 void overwrite_states_using_pool(struct sm_state
*gate_sm
, struct sm_state
*pool_sm
)
1009 struct state_list
*true_stack
= NULL
;
1010 struct state_list
*false_stack
= NULL
;
1011 struct stree
*pre_stree
;
1012 struct stree
*implied_true
;
1013 struct sm_state
*tmp
;
1018 get_tf_stacks_from_pool(gate_sm
, pool_sm
, &true_stack
, &false_stack
);
1020 pre_stree
= clone_stree(__get_cur_stree());
1022 implied_true
= filter_stack(gate_sm
, pre_stree
, false_stack
, true_stack
);
1024 free_stree(&pre_stree
);
1025 free_slist(&true_stack
);
1026 free_slist(&false_stack
);
1028 FOR_EACH_SM(implied_true
, tmp
) {
1029 set_state(tmp
->owner
, tmp
->name
, tmp
->sym
, tmp
->state
);
1030 } END_FOR_EACH_SM(tmp
);
1032 free_stree(&implied_true
);
1035 int assume(struct expression
*expr
)
1037 int orig_final_pass
= final_pass
;
1040 __push_fake_cur_stree();
1041 found_implications
= 0;
1042 __split_whole_condition(expr
);
1043 final_pass
= orig_final_pass
;
1045 if (!found_implications
) {
1046 __discard_false_states();
1047 __free_fake_cur_stree();
1054 void end_assume(void)
1056 __discard_false_states();
1057 __free_fake_cur_stree();
1060 void __extra_match_condition(struct expression
*expr
);
1061 void __comparison_match_condition(struct expression
*expr
);
1062 void __stored_condition(struct expression
*expr
);
1063 void register_implications(int id
)
1065 add_hook(&save_implications_hook
, CONDITION_HOOK
);
1066 add_hook(&set_implied_states
, CONDITION_HOOK
);
1067 add_hook(&__extra_match_condition
, CONDITION_HOOK
);
1068 add_hook(&set_extra_implied_states
, CONDITION_HOOK
);
1069 add_hook(&__comparison_match_condition
, CONDITION_HOOK
);
1070 add_hook(&__stored_condition
, CONDITION_HOOK
);
1071 add_hook(&match_end_func
, END_FUNC_HOOK
);