48 * foo != 99 and merge it all back together.
49 *
50 * That is the implied state of bar.
51 *
52 * merge_slist() sets up ->pool. An sm_state only has one ->pool and
53 * that is the pool where it was first set. The my pool gets set when
54 * code paths merge. States that have been set since the last merge do
55 * not have a ->pool.
56 * merge_sm_state() sets ->left and ->right. (These are the states which were
57 * merged to form the current state.)
58 * a pool: a pool is an slist that has been merged with another slist.
59 */
60
61 #include <sys/time.h>
62 #include <time.h>
63 #include "smatch.h"
64 #include "smatch_slist.h"
65 #include "smatch_extra.h"
66
67 char *implied_debug_msg;
68 #define DIMPLIED(msg...) do { if (option_debug_implied || option_debug) printf(msg); } while (0)
69
70 int option_debug_implied = 0;
71
72 /*
73 * tmp_range_list():
74 * It messes things up to free range list allocations. This helper fuction
75 * lets us reuse memory instead of doing new allocations.
76 */
77 static struct range_list *tmp_range_list(struct symbol *type, long long num)
78 {
79 static struct range_list *my_list = NULL;
80 static struct data_range *my_range;
81
82 __free_ptr_list((struct ptr_list **)&my_list);
83 my_range = alloc_range(ll_to_sval(num), ll_to_sval(num));
84 add_ptr_list(&my_list, my_range);
85 return my_list;
86 }
87
88 static void print_debug_tf(struct sm_state *sm, int istrue, int isfalse)
89 {
90 if (!option_debug_implied && !option_debug)
91 return;
92
93 if (istrue && isfalse) {
94 printf("%s: %d: does not exist.\n", show_sm(sm), sm->line);
95 } else if (istrue) {
96 printf("'%s = %s' from %d is true. %s[stree %d]\n", sm->name, show_state(sm->state),
97 sm->line, sm->merged ? "[merged]" : "[leaf]",
98 get_stree_id(sm->pool));
99 } else if (isfalse) {
100 printf("'%s = %s' from %d is false. %s[stree %d]\n", sm->name, show_state(sm->state),
101 sm->line,
102 sm->merged ? "[merged]" : "[leaf]",
103 get_stree_id(sm->pool));
104 } else {
105 printf("'%s = %s' from %d could be true or false. %s[stree %d]\n", sm->name,
106 show_state(sm->state), sm->line,
107 sm->merged ? "[merged]" : "[leaf]",
108 get_stree_id(sm->pool));
109 }
110 }
126
127 orig_rl = cast_rl(rl_type(rl), estate_rl(sm->state));
128 split_comparison_rl(orig_rl, comparison, rl, &true_rl, &false_rl, NULL, NULL);
129
130 true_rl = rl_truncate_cast(estate_type(sm->state), true_rl);
131 false_rl = rl_truncate_cast(estate_type(sm->state), false_rl);
132 if (is_whole_rl(true_rl) || is_whole_rl(false_rl) ||
133 !true_rl || !false_rl ||
134 rl_equiv(orig_rl, true_rl) || rl_equiv(orig_rl, false_rl) ||
135 rl_equiv(estate_rl(sm->state), true_rl) || rl_equiv(estate_rl(sm->state), false_rl))
136 return 0;
137
138 if (rl_intersection(true_rl, false_rl)) {
139 sm_perror("parsing (%s (%s) %s %s)",
140 sm->name, sm->state->name, show_special(comparison), show_rl(rl));
141 sm_msg("true_rl = %s false_rl = %s intersection = %s",
142 show_rl(true_rl), show_rl(false_rl), show_rl(rl_intersection(true_rl, false_rl)));
143 return 0;
144 }
145
146 if (option_debug)
147 sm_info("fake_history: %s vs %s. %s %s %s. --> T: %s F: %s",
148 sm->name, show_rl(rl), sm->state->name, show_special(comparison), show_rl(rl),
149 show_rl(true_rl), show_rl(false_rl));
150
151 true_sm = clone_sm(sm);
152 false_sm = clone_sm(sm);
153
154 true_sm->state = alloc_estate_rl(cast_rl(estate_type(sm->state), true_rl));
155 free_slist(&true_sm->possible);
156 add_possible_sm(true_sm, true_sm);
157 false_sm->state = alloc_estate_rl(cast_rl(estate_type(sm->state), false_rl));
158 free_slist(&false_sm->possible);
159 add_possible_sm(false_sm, false_sm);
160
161 true_stree = clone_stree(sm->pool);
162 false_stree = clone_stree(sm->pool);
163
164 overwrite_sm_state_stree(&true_stree, true_sm);
165 overwrite_sm_state_stree(&false_stree, false_sm);
166
167 true_sm->pool = true_stree;
168 false_sm->pool = false_stree;
169
170 sm->merged = 1;
171 sm->left = true_sm;
172 sm->right = false_sm;
173
174 return 1;
175 }
176
177 /*
249 print_debug_tf(sm, istrue, isfalse);
250
251 /* give up if we have borrowed implications (smatch_equiv.c) */
252 if (sm->sym != gate_sm->sym ||
253 strcmp(sm->name, gate_sm->name) != 0) {
254 if (mixed)
255 *mixed = 1;
256 }
257
258 if (mixed && !*mixed && !is_merged(sm) && !istrue && !isfalse) {
259 if (!create_fake_history(sm, comparison, rl))
260 *mixed = 1;
261 }
262
263 if (istrue)
264 add_pool(true_stack, sm);
265 else if (isfalse)
266 add_pool(false_stack, sm);
267 else
268 add_pool(maybe_stack, sm);
269
270 }
271
272 static int is_checked(struct state_list *checked, struct sm_state *sm)
273 {
274 struct sm_state *tmp;
275
276 FOR_EACH_PTR(checked, tmp) {
277 if (tmp == sm)
278 return 1;
279 } END_FOR_EACH_PTR(tmp);
280 return 0;
281 }
282
283 /*
284 * separate_pools():
285 * Example code: if (foo == 99) {
286 *
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.
290 */
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)
296 {
297 int free_checked = 0;
298 struct state_list *checked_states = NULL;
299
300 if (!sm)
301 return;
302
303 /*
304 * If it looks like this is going to take too long as-is, then don't
305 * create even more fake history.
306 */
307 if (mixed && sm->nr_children > 100)
308 *mixed = 1;
309
310 /*
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.
314 */
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;
321 }
322 return;
323 }
324
325 if (checked == NULL) {
326 checked = &checked_states;
327 free_checked = 1;
328 }
329 if (is_checked(*checked, sm))
330 return;
331 add_ptr_list(checked, sm);
332
333 do_compare(sm, comparison, rl, true_stack, maybe_stack, false_stack, mixed, gate_sm);
334
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);
337 if (free_checked)
338 free_slist(checked);
339 }
340
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)
345 {
346 struct state_list *maybe_stack = NULL;
347 struct sm_state *tmp;
348
349 __separate_pools(sm, comparison, rl, true_stack, &maybe_stack, false_stack, checked, mixed, sm);
350
351 if (option_debug) {
352 struct sm_state *sm;
353
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);
357
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);
361
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);
365 }
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);
371
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);
377 }
378
379 static int sm_in_keep_leafs(struct sm_state *sm, const struct state_list *keep_gates)
380 {
381 struct sm_state *tmp, *old;
382
383 FOR_EACH_PTR(keep_gates, tmp) {
384 if (is_merged(tmp))
385 continue;
386 old = get_sm_state_stree(tmp->pool, sm->owner, sm->name, sm->sym);
387 if (!old)
388 continue;
389 if (old == sm)
390 return 1;
391 } END_FOR_EACH_PTR(tmp);
392 return 0;
393 }
394
395 static int taking_too_long(void)
396 {
397 static void *printed;
398
399 if (out_of_memory())
400 return 1;
401
402 if (time_parsing_function() < option_timeout)
403 return 0;
404
405 if (!__inline_fn && printed != cur_func_sym) {
406 if (!is_skipped_function())
407 sm_perror("turning off implications after 60 seconds");
408 printed = cur_func_sym;
409 }
410 return 1;
411 }
412
413 /*
414 * NOTE: If a state is in both the keep stack and the remove stack then that is
415 * a bug. Only add states which are definitely true or definitely false. If
416 * you have a leaf state that could be both true and false, then create a fake
417 * split history where one side is true and one side is false. Otherwise, if
418 * you can't do that, then don't add it to either list.
419 */
420 struct sm_state *filter_pools(struct sm_state *sm,
421 const struct state_list *remove_stack,
422 const struct state_list *keep_stack,
423 int *modified, int *recurse_cnt,
424 struct timeval *start)
425 {
426 struct sm_state *ret = NULL;
427 struct sm_state *left;
428 struct sm_state *right;
429 int removed = 0;
430 struct timeval now;
431
432 if (!sm)
433 return NULL;
434 if (sm->skip_implications)
435 return sm;
436 if (taking_too_long())
437 return sm;
438
439 gettimeofday(&now, NULL);
440 if ((*recurse_cnt)++ > 1000 || now.tv_sec - start->tv_sec > 5) {
441 if (local_debug || option_debug_implied) {
442 static char buf[1028];
443 snprintf(buf, sizeof(buf), "debug: %s: nr_children over 4000 (%d). (%s %s)",
444 __func__, sm->nr_children, sm->name, show_state(sm->state));
445 implied_debug_msg = buf;
446 }
447 sm->skip_implications = 1;
448 return sm;
449 }
450
451 if (pool_in_pools(sm->pool, remove_stack)) {
452 DIMPLIED("removed [stree %d] %s from %d\n", get_stree_id(sm->pool), show_sm(sm), sm->line);
453 *modified = 1;
454 return NULL;
455 }
456
457 if (!is_merged(sm) || pool_in_pools(sm->pool, keep_stack) || sm_in_keep_leafs(sm, keep_stack)) {
458 DIMPLIED("kept [stree %d] %s from %d. %s. %s. %s.\n", get_stree_id(sm->pool), show_sm(sm), sm->line,
459 is_merged(sm) ? "merged" : "not merged",
460 pool_in_pools(sm->pool, keep_stack) ? "not in keep pools" : "in keep pools",
461 sm_in_keep_leafs(sm, keep_stack) ? "reachable keep leaf" : "no keep leaf");
462 return sm;
463 }
464
465 DIMPLIED("checking [stree %d] %s from %d (%d) left = %s [stree %d] right = %s [stree %d]\n",
466 get_stree_id(sm->pool),
467 show_sm(sm), sm->line, sm->nr_children,
468 sm->left ? sm->left->state->name : "<none>", sm->left ? get_stree_id(sm->left->pool) : -1,
469 sm->right ? sm->right->state->name : "<none>", sm->right ? get_stree_id(sm->right->pool) : -1);
470 left = filter_pools(sm->left, remove_stack, keep_stack, &removed, recurse_cnt, start);
471 right = filter_pools(sm->right, remove_stack, keep_stack, &removed, recurse_cnt, start);
472 if (!removed) {
473 DIMPLIED("kept [stree %d] %s from %d\n", get_stree_id(sm->pool), show_sm(sm), sm->line);
474 return sm;
475 }
476 *modified = 1;
477 if (!left && !right) {
478 DIMPLIED("removed [stree %d] %s from %d <none>\n", get_stree_id(sm->pool), show_sm(sm), sm->line);
479 return NULL;
480 }
481
482 if (!left) {
483 ret = clone_sm(right);
484 ret->merged = 1;
485 ret->right = right;
486 ret->left = NULL;
487 } else if (!right) {
488 ret = clone_sm(left);
489 ret->merged = 1;
490 ret->left = left;
491 ret->right = NULL;
492 } else {
493 if (left->sym != sm->sym || strcmp(left->name, sm->name) != 0) {
494 left = clone_sm(left);
495 left->sym = sm->sym;
496 left->name = sm->name;
497 }
498 if (right->sym != sm->sym || strcmp(right->name, sm->name) != 0) {
499 right = clone_sm(right);
500 right->sym = sm->sym;
501 right->name = sm->name;
502 }
503 ret = merge_sm_states(left, right);
504 }
505
506 ret->pool = sm->pool;
507
508 DIMPLIED("partial %s => ", show_sm(sm));
509 DIMPLIED("%s from %d [stree %d]\n", show_sm(ret), sm->line, get_stree_id(sm->pool));
510 return ret;
511 }
512
513 static struct stree *filter_stack(struct sm_state *gate_sm,
514 struct stree *pre_stree,
515 const struct state_list *remove_stack,
516 const struct state_list *keep_stack)
517 {
518 struct stree *ret = NULL;
519 struct sm_state *tmp;
520 struct sm_state *filtered_sm;
521 int modified;
522 int recurse_cnt;
523 struct timeval start;
524
525 if (!remove_stack)
526 return NULL;
527
528 if (taking_too_long())
529 return NULL;
530
531 FOR_EACH_SM(pre_stree, tmp) {
532 if (option_debug)
533 sm_msg("%s: %s", __func__, show_sm(tmp));
534 if (!tmp->merged)
535 continue;
536 if (sm_in_keep_leafs(tmp, keep_stack))
537 continue;
538 modified = 0;
539 recurse_cnt = 0;
540 gettimeofday(&start, NULL);
541 filtered_sm = filter_pools(tmp, remove_stack, keep_stack, &modified, &recurse_cnt, &start);
542 if (!filtered_sm || !modified)
543 continue;
544 /* the assignments here are for borrowed implications */
545 filtered_sm->name = tmp->name;
546 filtered_sm->sym = tmp->sym;
547 avl_insert(&ret, filtered_sm);
548 if (out_of_memory() || taking_too_long())
549 return NULL;
550
551 } END_FOR_EACH_SM(tmp);
552 return ret;
553 }
554
555 static void separate_and_filter(struct sm_state *sm, int comparison, struct range_list *rl,
556 struct stree *pre_stree,
557 struct stree **true_states,
558 struct stree **false_states,
559 int *mixed)
560 {
561 struct state_list *true_stack = NULL;
562 struct state_list *false_stack = NULL;
563 struct timeval time_before;
564 struct timeval time_after;
565 int sec;
566
567 gettimeofday(&time_before, NULL);
568
569 if (!is_merged(sm)) {
570 DIMPLIED("%d '%s' is not merged.\n", get_lineno(), sm->name);
571 return;
572 }
573
574 if (option_debug_implied || option_debug) {
575 sm_msg("checking implications: (%s %s %s)",
576 sm->name, show_special(comparison), show_rl(rl));
577 }
578
579 separate_pools(sm, comparison, rl, &true_stack, &false_stack, NULL, mixed);
580
581 DIMPLIED("filtering true stack.\n");
582 *true_states = filter_stack(sm, pre_stree, false_stack, true_stack);
583 DIMPLIED("filtering false stack.\n");
584 *false_states = filter_stack(sm, pre_stree, true_stack, false_stack);
585 free_slist(&true_stack);
586 free_slist(&false_stack);
587 if (option_debug_implied || option_debug) {
588 printf("These are the implied states for the true path: (%s %s %s)\n",
589 sm->name, show_special(comparison), show_rl(rl));
590 __print_stree(*true_states);
591 printf("These are the implied states for the false path: (%s %s %s)\n",
592 sm->name, show_special(comparison), show_rl(rl));
593 __print_stree(*false_states);
594 }
595
596 gettimeofday(&time_after, NULL);
597 sec = time_after.tv_sec - time_before.tv_sec;
598 if (sec > option_timeout) {
599 sm->nr_children = 4000;
600 sm_perror("Function too hairy. Ignoring implications after %d seconds.", sec);
601 }
602 }
603
604 static struct expression *get_last_expr(struct statement *stmt)
605 {
606 struct statement *last;
607
608 last = last_ptr_list((struct ptr_list *)stmt->stmts);
609 if (last->type == STMT_EXPRESSION)
610 return last->expression;
611
612 if (last->type == STMT_LABEL) {
613 if (last->label_statement &&
614 last->label_statement->type == STMT_EXPRESSION)
615 return last->label_statement->expression;
616 }
617
618 return NULL;
619 }
797 struct state_list *false_stack = NULL;
798 struct stree *pre_stree;
799 struct sm_state *sm;
800
801 sm = stored_condition_implication_hook(expr, &true_stack, &false_stack);
802 if (!sm)
803 return 0;
804
805 pre_stree = clone_stree(__get_cur_stree());
806
807 *implied_true = filter_stack(sm, pre_stree, false_stack, true_stack);
808 *implied_false = filter_stack(sm, pre_stree, true_stack, false_stack);
809
810 free_stree(&pre_stree);
811 free_slist(&true_stack);
812 free_slist(&false_stack);
813
814 return 1;
815 }
816
817 static int found_implications;
818 static struct stree *saved_implied_true;
819 static struct stree *saved_implied_false;
820 static struct stree *extra_saved_implied_true;
821 static struct stree *extra_saved_implied_false;
822
823 static void separate_extra_states(struct stree **implied_true,
824 struct stree **implied_false)
825 {
826 struct sm_state *sm;
827
828 /* We process extra states later to preserve the implications. */
829 FOR_EACH_SM(*implied_true, sm) {
830 if (sm->owner == SMATCH_EXTRA)
831 overwrite_sm_state_stree(&extra_saved_implied_true, sm);
832 } END_FOR_EACH_SM(sm);
833 FOR_EACH_SM(extra_saved_implied_true, sm) {
834 delete_state_stree(implied_true, sm->owner, sm->name, sm->sym);
835 } END_FOR_EACH_SM(sm);
836
837 FOR_EACH_SM(*implied_false, sm) {
838 if (sm->owner == SMATCH_EXTRA)
839 overwrite_sm_state_stree(&extra_saved_implied_false, sm);
840 } END_FOR_EACH_SM(sm);
841 FOR_EACH_SM(extra_saved_implied_false, sm) {
842 delete_state_stree(implied_false, sm->owner, sm->name, sm->sym);
843 } END_FOR_EACH_SM(sm);
844 }
845
846 static void get_tf_states(struct expression *expr,
847 struct stree **implied_true,
848 struct stree **implied_false)
849 {
850 if (handled_by_comparison_hook(expr, implied_true, implied_false))
851 goto found;
852
853 if (handled_by_extra_states(expr, implied_true, implied_false)) {
854 separate_extra_states(implied_true, implied_false);
855 goto found;
856 }
857
858 if (handled_by_stored_conditions(expr, implied_true, implied_false))
859 goto found;
860
861 return;
862 found:
863 found_implications = 1;
864 }
865
866 static void save_implications_hook(struct expression *expr)
867 {
868 if (taking_too_long())
869 return;
870 get_tf_states(expr, &saved_implied_true, &saved_implied_false);
871 }
872
873 static void set_implied_states(struct expression *expr)
874 {
875 struct sm_state *sm;
876
877 FOR_EACH_SM(saved_implied_true, sm) {
878 __set_true_false_sm(sm, NULL);
879 } END_FOR_EACH_SM(sm);
880 free_stree(&saved_implied_true);
881
882 FOR_EACH_SM(saved_implied_false, sm) {
883 __set_true_false_sm(NULL, sm);
884 } END_FOR_EACH_SM(sm);
885 free_stree(&saved_implied_false);
886 }
887
888 static void set_extra_implied_states(struct expression *expr)
889 {
890 saved_implied_true = extra_saved_implied_true;
891 saved_implied_false = extra_saved_implied_false;
892 extra_saved_implied_true = NULL;
893 extra_saved_implied_false = NULL;
894 set_implied_states(NULL);
895 }
896
897 void param_limit_implications(struct expression *expr, int param, char *key, char *value)
898 {
899 struct expression *arg;
900 struct symbol *compare_type;
901 char *name;
902 struct symbol *sym;
903 struct sm_state *sm;
904 struct sm_state *tmp;
905 struct stree *implied_true = NULL;
906 struct stree *implied_false = NULL;
907 struct range_list *orig, *limit;
908
909 while (expr->type == EXPR_ASSIGNMENT)
910 expr = strip_expr(expr->right);
911 if (expr->type != EXPR_CALL)
912 return;
913
914 arg = get_argument_from_call_expr(expr->args, param);
915 if (!arg)
916 return;
917
918 arg = strip_parens(arg);
919 while (arg->type == EXPR_ASSIGNMENT && arg->op == '=')
920 arg = strip_parens(arg->left);
921
922 name = get_variable_from_key(arg, key, &sym);
923 if (!name || !sym)
924 goto free;
925
926 sm = get_sm_state(SMATCH_EXTRA, name, sym);
927 if (!sm || !sm->merged)
928 goto free;
1055 implied_true = filter_stack(gate_sm, pre_stree, false_stack, true_stack);
1056
1057 free_stree(&pre_stree);
1058 free_slist(&true_stack);
1059 free_slist(&false_stack);
1060
1061 FOR_EACH_SM(implied_true, tmp) {
1062 set_state(tmp->owner, tmp->name, tmp->sym, tmp->state);
1063 } END_FOR_EACH_SM(tmp);
1064
1065 free_stree(&implied_true);
1066 }
1067
1068 int assume(struct expression *expr)
1069 {
1070 int orig_final_pass = final_pass;
1071
1072 in_fake_env++;
1073 final_pass = 0;
1074 __push_fake_cur_stree();
1075 found_implications = 0;
1076 __split_whole_condition(expr);
1077 final_pass = orig_final_pass;
1078 in_fake_env--;
1079
1080 return 1;
1081 }
1082
1083 void end_assume(void)
1084 {
1085 __discard_false_states();
1086 __free_fake_cur_stree();
1087 }
1088
1089 int impossible_assumption(struct expression *left, int op, sval_t sval)
1090 {
1091 struct expression *value;
1092 struct expression *comparison;
1093 int ret;
1094
1095 value = value_expr(sval.value);
|
48 * foo != 99 and merge it all back together.
49 *
50 * That is the implied state of bar.
51 *
52 * merge_slist() sets up ->pool. An sm_state only has one ->pool and
53 * that is the pool where it was first set. The my pool gets set when
54 * code paths merge. States that have been set since the last merge do
55 * not have a ->pool.
56 * merge_sm_state() sets ->left and ->right. (These are the states which were
57 * merged to form the current state.)
58 * a pool: a pool is an slist that has been merged with another slist.
59 */
60
61 #include <sys/time.h>
62 #include <time.h>
63 #include "smatch.h"
64 #include "smatch_slist.h"
65 #include "smatch_extra.h"
66
67 char *implied_debug_msg;
68
69 bool implications_off;
70
71 #define implied_debug 0
72 #define DIMPLIED(msg...) do { if (implied_debug) printf(msg); } while (0)
73
74 /*
75 * tmp_range_list():
76 * It messes things up to free range list allocations. This helper fuction
77 * lets us reuse memory instead of doing new allocations.
78 */
79 static struct range_list *tmp_range_list(struct symbol *type, long long num)
80 {
81 static struct range_list *my_list = NULL;
82 static struct data_range *my_range;
83
84 __free_ptr_list((struct ptr_list **)&my_list);
85 my_range = alloc_range(ll_to_sval(num), ll_to_sval(num));
86 add_ptr_list(&my_list, my_range);
87 return my_list;
88 }
89
90 static void print_debug_tf(struct sm_state *sm, int istrue, int isfalse)
91 {
92 if (!implied_debug && !option_debug)
93 return;
94
95 if (istrue && isfalse) {
96 printf("%s: %d: does not exist.\n", show_sm(sm), sm->line);
97 } else if (istrue) {
98 printf("'%s = %s' from %d is true. %s[stree %d]\n", sm->name, show_state(sm->state),
99 sm->line, sm->merged ? "[merged]" : "[leaf]",
100 get_stree_id(sm->pool));
101 } else if (isfalse) {
102 printf("'%s = %s' from %d is false. %s[stree %d]\n", sm->name, show_state(sm->state),
103 sm->line,
104 sm->merged ? "[merged]" : "[leaf]",
105 get_stree_id(sm->pool));
106 } else {
107 printf("'%s = %s' from %d could be true or false. %s[stree %d]\n", sm->name,
108 show_state(sm->state), sm->line,
109 sm->merged ? "[merged]" : "[leaf]",
110 get_stree_id(sm->pool));
111 }
112 }
128
129 orig_rl = cast_rl(rl_type(rl), estate_rl(sm->state));
130 split_comparison_rl(orig_rl, comparison, rl, &true_rl, &false_rl, NULL, NULL);
131
132 true_rl = rl_truncate_cast(estate_type(sm->state), true_rl);
133 false_rl = rl_truncate_cast(estate_type(sm->state), false_rl);
134 if (is_whole_rl(true_rl) || is_whole_rl(false_rl) ||
135 !true_rl || !false_rl ||
136 rl_equiv(orig_rl, true_rl) || rl_equiv(orig_rl, false_rl) ||
137 rl_equiv(estate_rl(sm->state), true_rl) || rl_equiv(estate_rl(sm->state), false_rl))
138 return 0;
139
140 if (rl_intersection(true_rl, false_rl)) {
141 sm_perror("parsing (%s (%s) %s %s)",
142 sm->name, sm->state->name, show_special(comparison), show_rl(rl));
143 sm_msg("true_rl = %s false_rl = %s intersection = %s",
144 show_rl(true_rl), show_rl(false_rl), show_rl(rl_intersection(true_rl, false_rl)));
145 return 0;
146 }
147
148 if (implied_debug)
149 sm_msg("fake_history: %s vs %s. %s %s %s. --> T: %s F: %s",
150 sm->name, show_rl(rl), sm->state->name, show_special(comparison), show_rl(rl),
151 show_rl(true_rl), show_rl(false_rl));
152
153 true_sm = clone_sm(sm);
154 false_sm = clone_sm(sm);
155
156 true_sm->state = clone_partial_estate(sm->state, true_rl);
157 free_slist(&true_sm->possible);
158 add_possible_sm(true_sm, true_sm);
159 false_sm->state = clone_partial_estate(sm->state, false_rl);
160 free_slist(&false_sm->possible);
161 add_possible_sm(false_sm, false_sm);
162
163 true_stree = clone_stree(sm->pool);
164 false_stree = clone_stree(sm->pool);
165
166 overwrite_sm_state_stree(&true_stree, true_sm);
167 overwrite_sm_state_stree(&false_stree, false_sm);
168
169 true_sm->pool = true_stree;
170 false_sm->pool = false_stree;
171
172 sm->merged = 1;
173 sm->left = true_sm;
174 sm->right = false_sm;
175
176 return 1;
177 }
178
179 /*
251 print_debug_tf(sm, istrue, isfalse);
252
253 /* give up if we have borrowed implications (smatch_equiv.c) */
254 if (sm->sym != gate_sm->sym ||
255 strcmp(sm->name, gate_sm->name) != 0) {
256 if (mixed)
257 *mixed = 1;
258 }
259
260 if (mixed && !*mixed && !is_merged(sm) && !istrue && !isfalse) {
261 if (!create_fake_history(sm, comparison, rl))
262 *mixed = 1;
263 }
264
265 if (istrue)
266 add_pool(true_stack, sm);
267 else if (isfalse)
268 add_pool(false_stack, sm);
269 else
270 add_pool(maybe_stack, sm);
271 }
272
273 static int is_checked(struct state_list *checked, struct sm_state *sm)
274 {
275 struct sm_state *tmp;
276
277 FOR_EACH_PTR(checked, tmp) {
278 if (tmp == sm)
279 return 1;
280 } END_FOR_EACH_PTR(tmp);
281 return 0;
282 }
283
284 /*
285 * separate_pools():
286 * Example code: if (foo == 99) {
287 *
288 * Say 'foo' is a merged state that has many possible values. It is the combination
289 * of merges. separate_pools() iterates through the pools recursively and calls
290 * do_compare() for each time 'foo' was set.
291 */
292 static void __separate_pools(struct sm_state *sm, int comparison, struct range_list *rl,
293 struct state_list **true_stack,
294 struct state_list **maybe_stack,
295 struct state_list **false_stack,
296 struct state_list **checked, int *mixed, struct sm_state *gate_sm,
297 struct timeval *start_time)
298 {
299 int free_checked = 0;
300 struct state_list *checked_states = NULL;
301 struct timeval now;
302
303 if (!sm)
304 return;
305
306 gettimeofday(&now, NULL);
307 if (now.tv_usec - start_time->tv_usec > 1000000) {
308 if (implied_debug) {
309 sm_msg("debug: %s: implications taking too long. (%s %s %s)",
310 __func__, sm->state->name, show_special(comparison), show_rl(rl));
311 }
312 if (mixed)
313 *mixed = 1;
314 }
315
316 if (checked == NULL) {
317 checked = &checked_states;
318 free_checked = 1;
319 }
320 if (is_checked(*checked, sm))
321 return;
322 add_ptr_list(checked, sm);
323
324 do_compare(sm, comparison, rl, true_stack, maybe_stack, false_stack, mixed, gate_sm);
325
326 __separate_pools(sm->left, comparison, rl, true_stack, maybe_stack, false_stack, checked, mixed, gate_sm, start_time);
327 __separate_pools(sm->right, comparison, rl, true_stack, maybe_stack, false_stack, checked, mixed, gate_sm, start_time);
328 if (free_checked)
329 free_slist(checked);
330 }
331
332 static void separate_pools(struct sm_state *sm, int comparison, struct range_list *rl,
333 struct state_list **true_stack,
334 struct state_list **false_stack,
335 struct state_list **checked, int *mixed)
336 {
337 struct state_list *maybe_stack = NULL;
338 struct sm_state *tmp;
339 struct timeval start_time;
340
341
342 gettimeofday(&start_time, NULL);
343 __separate_pools(sm, comparison, rl, true_stack, &maybe_stack, false_stack, checked, mixed, sm, &start_time);
344
345 if (implied_debug) {
346 struct sm_state *sm;
347
348 FOR_EACH_PTR(*true_stack, sm) {
349 sm_msg("TRUE %s [stree %d]", show_sm(sm), get_stree_id(sm->pool));
350 } END_FOR_EACH_PTR(sm);
351
352 FOR_EACH_PTR(maybe_stack, sm) {
353 sm_msg("MAYBE %s %s[stree %d]",
354 show_sm(sm), sm->merged ? "(merged) ": "", get_stree_id(sm->pool));
355 } END_FOR_EACH_PTR(sm);
356
357 FOR_EACH_PTR(*false_stack, sm) {
358 sm_msg("FALSE %s [stree %d]", show_sm(sm), get_stree_id(sm->pool));
359 } END_FOR_EACH_PTR(sm);
360 }
361 /* if it's a maybe then remove it */
362 FOR_EACH_PTR(maybe_stack, tmp) {
363 remove_pool(false_stack, tmp->pool);
364 remove_pool(true_stack, tmp->pool);
365 } END_FOR_EACH_PTR(tmp);
366
367 /* if it's both true and false remove it from both */
368 FOR_EACH_PTR(*true_stack, tmp) {
369 if (remove_pool(false_stack, tmp->pool))
370 DELETE_CURRENT_PTR(tmp);
371 } END_FOR_EACH_PTR(tmp);
372 }
373
374 static int sm_in_keep_leafs(struct sm_state *sm, const struct state_list *keep_gates)
375 {
376 struct sm_state *tmp, *old;
377
378 FOR_EACH_PTR(keep_gates, tmp) {
379 if (is_merged(tmp))
380 continue;
381 old = get_sm_state_stree(tmp->pool, sm->owner, sm->name, sm->sym);
382 if (!old)
383 continue;
384 if (old == sm)
385 return 1;
386 } END_FOR_EACH_PTR(tmp);
387 return 0;
388 }
389
390 static int going_too_slow(void)
391 {
392 static void *printed;
393
394 if (out_of_memory()) {
395 implications_off = true;
396 return 1;
397 }
398
399 if (!option_timeout || time_parsing_function() < option_timeout) {
400 implications_off = false;
401 return 0;
402 }
403
404 if (!__inline_fn && printed != cur_func_sym) {
405 if (!is_skipped_function())
406 sm_perror("turning off implications after %d seconds", option_timeout);
407 printed = cur_func_sym;
408 }
409 implications_off = true;
410 return 1;
411 }
412
413 static char *sm_state_info(struct sm_state *sm)
414 {
415 static char buf[512];
416 int n = 0;
417
418 n += snprintf(buf + n, sizeof(buf) - n, "[stree %d line %d] ",
419 get_stree_id(sm->pool), sm->line);
420 if (n >= sizeof(buf))
421 return buf;
422 n += snprintf(buf + n, sizeof(buf) - n, "%s ", show_sm(sm));
423 if (n >= sizeof(buf))
424 return buf;
425 n += snprintf(buf + n, sizeof(buf) - n, "left = %s [stree %d] ",
426 sm->left ? sm->left->state->name : "<none>",
427 sm->left ? get_stree_id(sm->left->pool) : -1);
428 if (n >= sizeof(buf))
429 return buf;
430 n += snprintf(buf + n, sizeof(buf) - n, "right = %s [stree %d]",
431 sm->right ? sm->right->state->name : "<none>",
432 sm->right ? get_stree_id(sm->right->pool) : -1);
433 return buf;
434 }
435
436 /*
437 * NOTE: If a state is in both the keep stack and the remove stack then that is
438 * a bug. Only add states which are definitely true or definitely false. If
439 * you have a leaf state that could be both true and false, then create a fake
440 * split history where one side is true and one side is false. Otherwise, if
441 * you can't do that, then don't add it to either list.
442 */
443 #define RECURSE_LIMIT 300
444 struct sm_state *filter_pools(struct sm_state *sm,
445 const struct state_list *remove_stack,
446 const struct state_list *keep_stack,
447 int *modified, int *recurse_cnt,
448 struct timeval *start, int *skip, int *bail)
449 {
450 struct sm_state *ret = NULL;
451 struct sm_state *left;
452 struct sm_state *right;
453 int removed = 0;
454 struct timeval now;
455
456 if (!sm)
457 return NULL;
458 if (*bail)
459 return NULL;
460 gettimeofday(&now, NULL);
461 if (now.tv_usec - start->tv_usec > 3000000) {
462 DIMPLIED("%s: implications taking too long: %s\n", __func__, sm_state_info(sm));
463 *bail = 1;
464 return NULL;
465 }
466 if ((*recurse_cnt)++ > RECURSE_LIMIT) {
467 DIMPLIED("%s: recursed too far: %s\n", __func__, sm_state_info(sm));
468 *skip = 1;
469 return NULL;
470 }
471
472 if (pool_in_pools(sm->pool, remove_stack)) {
473 DIMPLIED("%s: remove: %s\n", __func__, sm_state_info(sm));
474 *modified = 1;
475 return NULL;
476 }
477
478 if (!is_merged(sm) || pool_in_pools(sm->pool, keep_stack) || sm_in_keep_leafs(sm, keep_stack)) {
479 DIMPLIED("%s: keep %s (%s, %s, %s): %s\n", __func__, sm->state->name,
480 is_merged(sm) ? "merged" : "not merged",
481 pool_in_pools(sm->pool, keep_stack) ? "not in keep pools" : "in keep pools",
482 sm_in_keep_leafs(sm, keep_stack) ? "reachable keep leaf" : "no keep leaf",
483 sm_state_info(sm));
484 return sm;
485 }
486
487 left = filter_pools(sm->left, remove_stack, keep_stack, &removed, recurse_cnt, start, skip, bail);
488 right = filter_pools(sm->right, remove_stack, keep_stack, &removed, recurse_cnt, start, skip, bail);
489 if (*bail || *skip)
490 return NULL;
491 if (!removed) {
492 DIMPLIED("%s: kept all: %s\n", __func__, sm_state_info(sm));
493 return sm;
494 }
495 *modified = 1;
496 if (!left && !right) {
497 DIMPLIED("%s: removed all: %s\n", __func__, sm_state_info(sm));
498 return NULL;
499 }
500
501 if (!left) {
502 ret = clone_sm(right);
503 ret->merged = 1;
504 ret->right = right;
505 ret->left = NULL;
506 } else if (!right) {
507 ret = clone_sm(left);
508 ret->merged = 1;
509 ret->left = left;
510 ret->right = NULL;
511 } else {
512 if (left->sym != sm->sym || strcmp(left->name, sm->name) != 0) {
513 left = clone_sm(left);
514 left->sym = sm->sym;
515 left->name = sm->name;
516 }
517 if (right->sym != sm->sym || strcmp(right->name, sm->name) != 0) {
518 right = clone_sm(right);
519 right->sym = sm->sym;
520 right->name = sm->name;
521 }
522 ret = merge_sm_states(left, right);
523 }
524
525 ret->pool = sm->pool;
526
527 DIMPLIED("%s: partial: %s\n", __func__, sm_state_info(sm));
528 return ret;
529 }
530
531 static struct stree *filter_stack(struct sm_state *gate_sm,
532 struct stree *pre_stree,
533 const struct state_list *remove_stack,
534 const struct state_list *keep_stack)
535 {
536 struct stree *ret = NULL;
537 struct sm_state *tmp;
538 struct sm_state *filtered_sm;
539 int modified;
540 int recurse_cnt;
541 struct timeval start;
542 int skip;
543 int bail = 0;
544
545 if (!remove_stack)
546 return NULL;
547
548 gettimeofday(&start, NULL);
549 FOR_EACH_SM(pre_stree, tmp) {
550 if (!tmp->merged || sm_in_keep_leafs(tmp, keep_stack))
551 continue;
552 modified = 0;
553 recurse_cnt = 0;
554 skip = 0;
555 filtered_sm = filter_pools(tmp, remove_stack, keep_stack, &modified, &recurse_cnt, &start, &skip, &bail);
556 if (going_too_slow())
557 return NULL;
558 if (bail)
559 return ret; /* Return the implications we figured out before time ran out. */
560
561
562 if (skip || !filtered_sm || !modified)
563 continue;
564 /* the assignments here are for borrowed implications */
565 filtered_sm->name = tmp->name;
566 filtered_sm->sym = tmp->sym;
567 avl_insert(&ret, filtered_sm);
568 } END_FOR_EACH_SM(tmp);
569 return ret;
570 }
571
572 static void separate_and_filter(struct sm_state *sm, int comparison, struct range_list *rl,
573 struct stree *pre_stree,
574 struct stree **true_states,
575 struct stree **false_states,
576 int *mixed)
577 {
578 struct state_list *true_stack = NULL;
579 struct state_list *false_stack = NULL;
580 struct timeval time_before;
581 struct timeval time_after;
582 int sec;
583
584 gettimeofday(&time_before, NULL);
585
586 DIMPLIED("checking implications: (%s (%s) %s %s)\n",
587 sm->name, sm->state->name, show_special(comparison), show_rl(rl));
588
589 if (!is_merged(sm)) {
590 DIMPLIED("%d '%s' from line %d is not merged.\n", get_lineno(), sm->name, sm->line);
591 return;
592 }
593
594 separate_pools(sm, comparison, rl, &true_stack, &false_stack, NULL, mixed);
595
596 DIMPLIED("filtering true stack.\n");
597 *true_states = filter_stack(sm, pre_stree, false_stack, true_stack);
598 DIMPLIED("filtering false stack.\n");
599 *false_states = filter_stack(sm, pre_stree, true_stack, false_stack);
600 free_slist(&true_stack);
601 free_slist(&false_stack);
602 if (implied_debug) {
603 printf("These are the implied states for the true path: (%s (%s) %s %s)\n",
604 sm->name, sm->state->name, show_special(comparison), show_rl(rl));
605 __print_stree(*true_states);
606 printf("These are the implied states for the false path: (%s (%s) %s %s)\n",
607 sm->name, sm->state->name, show_special(comparison), show_rl(rl));
608 __print_stree(*false_states);
609 }
610
611 gettimeofday(&time_after, NULL);
612 sec = time_after.tv_sec - time_before.tv_sec;
613 if (option_timeout && sec > option_timeout) {
614 sm_perror("Function too hairy. Ignoring implications after %d seconds.", sec);
615 }
616 }
617
618 static struct expression *get_last_expr(struct statement *stmt)
619 {
620 struct statement *last;
621
622 last = last_ptr_list((struct ptr_list *)stmt->stmts);
623 if (last->type == STMT_EXPRESSION)
624 return last->expression;
625
626 if (last->type == STMT_LABEL) {
627 if (last->label_statement &&
628 last->label_statement->type == STMT_EXPRESSION)
629 return last->label_statement->expression;
630 }
631
632 return NULL;
633 }
811 struct state_list *false_stack = NULL;
812 struct stree *pre_stree;
813 struct sm_state *sm;
814
815 sm = stored_condition_implication_hook(expr, &true_stack, &false_stack);
816 if (!sm)
817 return 0;
818
819 pre_stree = clone_stree(__get_cur_stree());
820
821 *implied_true = filter_stack(sm, pre_stree, false_stack, true_stack);
822 *implied_false = filter_stack(sm, pre_stree, true_stack, false_stack);
823
824 free_stree(&pre_stree);
825 free_slist(&true_stack);
826 free_slist(&false_stack);
827
828 return 1;
829 }
830
831 static struct stree *saved_implied_true;
832 static struct stree *saved_implied_false;
833 static struct stree *extra_saved_implied_true;
834 static struct stree *extra_saved_implied_false;
835
836 static void separate_extra_states(struct stree **implied_true,
837 struct stree **implied_false)
838 {
839 struct sm_state *sm;
840
841 /* We process extra states later to preserve the implications. */
842 FOR_EACH_SM(*implied_true, sm) {
843 if (sm->owner == SMATCH_EXTRA)
844 overwrite_sm_state_stree(&extra_saved_implied_true, sm);
845 } END_FOR_EACH_SM(sm);
846 FOR_EACH_SM(extra_saved_implied_true, sm) {
847 delete_state_stree(implied_true, sm->owner, sm->name, sm->sym);
848 } END_FOR_EACH_SM(sm);
849
850 FOR_EACH_SM(*implied_false, sm) {
851 if (sm->owner == SMATCH_EXTRA)
852 overwrite_sm_state_stree(&extra_saved_implied_false, sm);
853 } END_FOR_EACH_SM(sm);
854 FOR_EACH_SM(extra_saved_implied_false, sm) {
855 delete_state_stree(implied_false, sm->owner, sm->name, sm->sym);
856 } END_FOR_EACH_SM(sm);
857 }
858
859 static void get_tf_states(struct expression *expr,
860 struct stree **implied_true,
861 struct stree **implied_false)
862 {
863 if (handled_by_comparison_hook(expr, implied_true, implied_false))
864 return;
865
866 if (handled_by_extra_states(expr, implied_true, implied_false)) {
867 separate_extra_states(implied_true, implied_false);
868 return;
869 }
870
871 if (handled_by_stored_conditions(expr, implied_true, implied_false))
872 return;
873 }
874
875 static void save_implications_hook(struct expression *expr)
876 {
877 if (going_too_slow())
878 return;
879 get_tf_states(expr, &saved_implied_true, &saved_implied_false);
880 }
881
882 static void set_implied_states(struct expression *expr)
883 {
884 struct sm_state *sm;
885
886 FOR_EACH_SM(saved_implied_true, sm) {
887 __set_true_false_sm(sm, NULL);
888 } END_FOR_EACH_SM(sm);
889 free_stree(&saved_implied_true);
890
891 FOR_EACH_SM(saved_implied_false, sm) {
892 __set_true_false_sm(NULL, sm);
893 } END_FOR_EACH_SM(sm);
894 free_stree(&saved_implied_false);
895 }
896
897 static void set_extra_implied_states(struct expression *expr)
898 {
899 saved_implied_true = extra_saved_implied_true;
900 saved_implied_false = extra_saved_implied_false;
901 extra_saved_implied_true = NULL;
902 extra_saved_implied_false = NULL;
903 set_implied_states(NULL);
904 }
905
906 void param_limit_implications(struct expression *expr, int param, char *key, char *value)
907 {
908 struct expression *arg;
909 struct symbol *compare_type;
910 char *name;
911 struct symbol *sym;
912 struct sm_state *sm;
913 struct sm_state *tmp;
914 struct stree *implied_true = NULL;
915 struct stree *implied_false = NULL;
916 struct range_list *orig, *limit;
917
918 if (time_parsing_function() > 40)
919 return;
920
921 while (expr->type == EXPR_ASSIGNMENT)
922 expr = strip_expr(expr->right);
923 if (expr->type != EXPR_CALL)
924 return;
925
926 arg = get_argument_from_call_expr(expr->args, param);
927 if (!arg)
928 return;
929
930 arg = strip_parens(arg);
931 while (arg->type == EXPR_ASSIGNMENT && arg->op == '=')
932 arg = strip_parens(arg->left);
933
934 name = get_variable_from_key(arg, key, &sym);
935 if (!name || !sym)
936 goto free;
937
938 sm = get_sm_state(SMATCH_EXTRA, name, sym);
939 if (!sm || !sm->merged)
940 goto free;
1067 implied_true = filter_stack(gate_sm, pre_stree, false_stack, true_stack);
1068
1069 free_stree(&pre_stree);
1070 free_slist(&true_stack);
1071 free_slist(&false_stack);
1072
1073 FOR_EACH_SM(implied_true, tmp) {
1074 set_state(tmp->owner, tmp->name, tmp->sym, tmp->state);
1075 } END_FOR_EACH_SM(tmp);
1076
1077 free_stree(&implied_true);
1078 }
1079
1080 int assume(struct expression *expr)
1081 {
1082 int orig_final_pass = final_pass;
1083
1084 in_fake_env++;
1085 final_pass = 0;
1086 __push_fake_cur_stree();
1087 __split_whole_condition(expr);
1088 final_pass = orig_final_pass;
1089 in_fake_env--;
1090
1091 return 1;
1092 }
1093
1094 void end_assume(void)
1095 {
1096 __discard_false_states();
1097 __free_fake_cur_stree();
1098 }
1099
1100 int impossible_assumption(struct expression *left, int op, sval_t sval)
1101 {
1102 struct expression *value;
1103 struct expression *comparison;
1104 int ret;
1105
1106 value = value_expr(sval.value);
|