Print this page
12166 resync smatch to 0.6.1-rc1-il-3
| Split |
Close |
| Expand all |
| Collapse all |
--- old/usr/src/tools/smatch/src/smatch_implied.c
+++ new/usr/src/tools/smatch/src/smatch_implied.c
1 1 /*
2 2 * Copyright (C) 2008 Dan Carpenter.
3 3 *
4 4 * This program is free software; you can redistribute it and/or
5 5 * modify it under the terms of the GNU General Public License
6 6 * as published by the Free Software Foundation; either version 2
7 7 * of the License, or (at your option) any later version.
8 8 *
9 9 * This program is distributed in the hope that it will be useful,
10 10 * but WITHOUT ANY WARRANTY; without even the implied warranty of
11 11 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
12 12 * GNU General Public License for more details.
13 13 *
14 14 * You should have received a copy of the GNU General Public License
15 15 * along with this program; if not, see http://www.gnu.org/copyleft/gpl.txt
16 16 *
17 17 * Copyright 2019 Joyent, Inc.
18 18 */
19 19
20 20 /*
21 21 * Imagine we have this code:
22 22 * foo = 1;
23 23 * if (bar)
24 24 * foo = 99;
25 25 * else
26 26 * frob();
27 27 * // <-- point #1
28 28 * if (foo == 99) // <-- point #2
29 29 * bar->baz; // <-- point #3
30 30 *
31 31 *
32 32 * At point #3 bar is non null and can be dereferenced.
33 33 *
34 34 * It's smatch_implied.c which sets bar to non null at point #2.
35 35 *
36 36 * At point #1 merge_slist() stores the list of states from both
37 37 * the true and false paths. On the true path foo == 99 and on
38 38 * the false path foo == 1. merge_slist() sets their pool
39 39 * list to show the other states which were there when foo == 99.
40 40 *
41 41 * When it comes to the if (foo == 99) the smatch implied hook
42 42 * looks for all the pools where foo was not 99. It makes a list
43 43 * of those.
44 44 *
45 45 * Then for bar (and all the other states) it says, ok bar is a
46 46 * merged state that came from these previous states. We'll
47 47 * chop out all the states where it came from a pool where
48 48 * foo != 99 and merge it all back together.
49 49 *
50 50 * That is the implied state of bar.
51 51 *
52 52 * merge_slist() sets up ->pool. An sm_state only has one ->pool and
53 53 * that is the pool where it was first set. The my pool gets set when
54 54 * code paths merge. States that have been set since the last merge do
55 55 * not have a ->pool.
56 56 * merge_sm_state() sets ->left and ->right. (These are the states which were
57 57 * merged to form the current state.)
58 58 * a pool: a pool is an slist that has been merged with another slist.
59 59 */
60 60
61 61 #include <time.h>
62 62 #include "smatch.h"
63 63 #include "smatch_slist.h"
64 64 #include "smatch_extra.h"
65 65
66 66 char *implied_debug_msg;
67 67
68 68 bool implications_off;
69 69
70 70 #define implied_debug 0
71 71 #define DIMPLIED(msg...) do { if (implied_debug) printf(msg); } while (0)
72 72
73 73 bool debug_implied(void)
74 74 {
75 75 return implied_debug;
76 76 }
77 77
78 78 /*
79 79 * tmp_range_list():
80 80 * It messes things up to free range list allocations. This helper fuction
81 81 * lets us reuse memory instead of doing new allocations.
82 82 */
83 83 static struct range_list *tmp_range_list(struct symbol *type, long long num)
84 84 {
85 85 static struct range_list *my_list = NULL;
86 86 static struct data_range *my_range;
87 87
88 88 __free_ptr_list((struct ptr_list **)&my_list);
89 89 my_range = alloc_range(ll_to_sval(num), ll_to_sval(num));
90 90 add_ptr_list(&my_list, my_range);
91 91 return my_list;
92 92 }
93 93
94 94 static void print_debug_tf(struct sm_state *sm, int istrue, int isfalse)
95 95 {
96 96 if (!implied_debug && !option_debug)
97 97 return;
98 98
99 99 if (istrue && isfalse) {
100 100 printf("%s: %d: does not exist.\n", show_sm(sm), sm->line);
101 101 } else if (istrue) {
102 102 printf("'%s = %s' from %d is true. %s[stree %d]\n", sm->name, show_state(sm->state),
103 103 sm->line, sm->merged ? "[merged]" : "[leaf]",
104 104 get_stree_id(sm->pool));
105 105 } else if (isfalse) {
106 106 printf("'%s = %s' from %d is false. %s[stree %d]\n", sm->name, show_state(sm->state),
107 107 sm->line,
108 108 sm->merged ? "[merged]" : "[leaf]",
109 109 get_stree_id(sm->pool));
110 110 } else {
111 111 printf("'%s = %s' from %d could be true or false. %s[stree %d]\n", sm->name,
112 112 show_state(sm->state), sm->line,
113 113 sm->merged ? "[merged]" : "[leaf]",
114 114 get_stree_id(sm->pool));
115 115 }
116 116 }
117 117
118 118 static int create_fake_history(struct sm_state *sm, int comparison, struct range_list *rl)
119 119 {
120 120 struct range_list *orig_rl;
121 121 struct range_list *true_rl, *false_rl;
122 122 struct stree *true_stree, *false_stree;
123 123 struct sm_state *true_sm, *false_sm;
124 124 sval_t sval;
125 125
126 126 if (is_merged(sm) || sm->left || sm->right)
127 127 return 0;
128 128 if (!rl_to_sval(rl, &sval))
129 129 return 0;
130 130 if (!estate_rl(sm->state))
131 131 return 0;
132 132
133 133 orig_rl = cast_rl(rl_type(rl), estate_rl(sm->state));
134 134 split_comparison_rl(orig_rl, comparison, rl, &true_rl, &false_rl, NULL, NULL);
|
↓ open down ↓ |
134 lines elided |
↑ open up ↑ |
135 135
136 136 true_rl = rl_truncate_cast(estate_type(sm->state), true_rl);
137 137 false_rl = rl_truncate_cast(estate_type(sm->state), false_rl);
138 138 if (is_whole_rl(true_rl) || is_whole_rl(false_rl) ||
139 139 !true_rl || !false_rl ||
140 140 rl_equiv(orig_rl, true_rl) || rl_equiv(orig_rl, false_rl) ||
141 141 rl_equiv(estate_rl(sm->state), true_rl) || rl_equiv(estate_rl(sm->state), false_rl))
142 142 return 0;
143 143
144 144 if (rl_intersection(true_rl, false_rl)) {
145 - sm_perror("parsing (%s (%s) %s %s)",
146 - sm->name, sm->state->name, show_special(comparison), show_rl(rl));
147 - sm_msg("true_rl = %s false_rl = %s intersection = %s",
148 - show_rl(true_rl), show_rl(false_rl), show_rl(rl_intersection(true_rl, false_rl)));
145 + /*
146 + * Normally these won't intersect, but one exception is when
147 + * we're dealing with mtags. We have a long list of mtags and
148 + * then negate the list. Now it's over the limit for mtag list
149 + * length and we squash it down to 4096-ptr_max. So then it's
150 + * possible for the true and false rl to overlap.
151 + */
149 152 return 0;
150 153 }
151 154
152 155 if (implied_debug)
153 156 sm_msg("fake_history: %s vs %s. %s %s %s. --> T: %s F: %s",
154 157 sm->name, show_rl(rl), sm->state->name, show_special(comparison), show_rl(rl),
155 158 show_rl(true_rl), show_rl(false_rl));
156 159
157 160 true_sm = clone_sm(sm);
158 161 false_sm = clone_sm(sm);
159 162
160 163 true_sm->state = clone_partial_estate(sm->state, true_rl);
161 164 free_slist(&true_sm->possible);
162 165 add_possible_sm(true_sm, true_sm);
163 166 false_sm->state = clone_partial_estate(sm->state, false_rl);
164 167 free_slist(&false_sm->possible);
165 168 add_possible_sm(false_sm, false_sm);
166 169
167 170 true_stree = clone_stree(sm->pool);
168 171 false_stree = clone_stree(sm->pool);
169 172
170 173 overwrite_sm_state_stree(&true_stree, true_sm);
171 174 overwrite_sm_state_stree(&false_stree, false_sm);
172 175
173 176 true_sm->pool = true_stree;
174 177 false_sm->pool = false_stree;
175 178
176 179 sm->merged = 1;
177 180 sm->left = true_sm;
178 181 sm->right = false_sm;
179 182
180 183 return 1;
181 184 }
182 185
183 186 /*
184 187 * add_pool() adds a slist to *pools. If the slist has already been
185 188 * added earlier then it doesn't get added a second time.
186 189 */
187 190 void add_pool(struct state_list **pools, struct sm_state *new)
188 191 {
189 192 struct sm_state *tmp;
190 193
191 194 FOR_EACH_PTR(*pools, tmp) {
192 195 if (tmp->pool < new->pool)
193 196 continue;
194 197 else if (tmp->pool == new->pool) {
195 198 return;
196 199 } else {
197 200 INSERT_CURRENT(new, tmp);
198 201 return;
199 202 }
200 203 } END_FOR_EACH_PTR(tmp);
201 204 add_ptr_list(pools, new);
202 205 }
203 206
204 207 static int pool_in_pools(struct stree *pool,
205 208 const struct state_list *slist)
206 209 {
207 210 struct sm_state *tmp;
208 211
209 212 FOR_EACH_PTR(slist, tmp) {
210 213 if (!tmp->pool)
211 214 continue;
212 215 if (tmp->pool == pool)
213 216 return 1;
214 217 } END_FOR_EACH_PTR(tmp);
215 218 return 0;
216 219 }
217 220
218 221 static int remove_pool(struct state_list **pools, struct stree *remove)
219 222 {
220 223 struct sm_state *tmp;
221 224 int ret = 0;
222 225
223 226 FOR_EACH_PTR(*pools, tmp) {
224 227 if (tmp->pool == remove) {
225 228 DELETE_CURRENT_PTR(tmp);
226 229 ret = 1;
227 230 }
228 231 } END_FOR_EACH_PTR(tmp);
229 232
230 233 return ret;
231 234 }
232 235
233 236 /*
234 237 * If 'foo' == 99 add it that pool to the true pools. If it's false, add it to
235 238 * the false pools. If we're not sure, then we don't add it to either.
236 239 */
237 240 static void do_compare(struct sm_state *sm, int comparison, struct range_list *rl,
238 241 struct state_list **true_stack,
239 242 struct state_list **maybe_stack,
240 243 struct state_list **false_stack,
241 244 int *mixed, struct sm_state *gate_sm)
242 245 {
243 246 int istrue;
244 247 int isfalse;
245 248 struct range_list *var_rl;
246 249
247 250 if (!sm->pool)
248 251 return;
249 252
250 253 var_rl = cast_rl(rl_type(rl), estate_rl(sm->state));
251 254
252 255 istrue = !possibly_false_rl(var_rl, comparison, rl);
253 256 isfalse = !possibly_true_rl(var_rl, comparison, rl);
254 257
255 258 print_debug_tf(sm, istrue, isfalse);
256 259
257 260 /* give up if we have borrowed implications (smatch_equiv.c) */
258 261 if (sm->sym != gate_sm->sym ||
259 262 strcmp(sm->name, gate_sm->name) != 0) {
260 263 if (mixed)
261 264 *mixed = 1;
262 265 }
263 266
264 267 if (mixed && !*mixed && !is_merged(sm) && !istrue && !isfalse) {
265 268 if (!create_fake_history(sm, comparison, rl))
266 269 *mixed = 1;
267 270 }
268 271
269 272 if (istrue)
270 273 add_pool(true_stack, sm);
271 274 else if (isfalse)
272 275 add_pool(false_stack, sm);
273 276 else
274 277 add_pool(maybe_stack, sm);
275 278 }
276 279
277 280 static int is_checked(struct state_list *checked, struct sm_state *sm)
278 281 {
279 282 struct sm_state *tmp;
280 283
281 284 FOR_EACH_PTR(checked, tmp) {
282 285 if (tmp == sm)
283 286 return 1;
284 287 } END_FOR_EACH_PTR(tmp);
285 288 return 0;
286 289 }
287 290
288 291 /*
289 292 * separate_pools():
290 293 * Example code: if (foo == 99) {
291 294 *
292 295 * Say 'foo' is a merged state that has many possible values. It is the combination
293 296 * of merges. separate_pools() iterates through the pools recursively and calls
294 297 * do_compare() for each time 'foo' was set.
295 298 */
296 299 static void __separate_pools(struct sm_state *sm, int comparison, struct range_list *rl,
297 300 struct state_list **true_stack,
298 301 struct state_list **maybe_stack,
299 302 struct state_list **false_stack,
300 303 struct state_list **checked, int *mixed, struct sm_state *gate_sm,
301 304 struct timeval *start_time)
302 305 {
303 306 int free_checked = 0;
304 307 struct state_list *checked_states = NULL;
305 308 struct timeval now, diff;
306 309
307 310 if (!sm)
308 311 return;
309 312
310 313 gettimeofday(&now, NULL);
311 314 timersub(&now, start_time, &diff);
312 315 if (diff.tv_sec >= 1) {
313 316 if (implied_debug) {
314 317 sm_msg("debug: %s: implications taking too long. (%s %s %s)",
315 318 __func__, sm->state->name, show_special(comparison), show_rl(rl));
316 319 }
317 320 if (mixed)
318 321 *mixed = 1;
319 322 }
320 323
321 324 if (checked == NULL) {
322 325 checked = &checked_states;
323 326 free_checked = 1;
324 327 }
325 328 if (is_checked(*checked, sm))
326 329 return;
327 330 add_ptr_list(checked, sm);
328 331
329 332 do_compare(sm, comparison, rl, true_stack, maybe_stack, false_stack, mixed, gate_sm);
330 333
331 334 __separate_pools(sm->left, comparison, rl, true_stack, maybe_stack, false_stack, checked, mixed, gate_sm, start_time);
332 335 __separate_pools(sm->right, comparison, rl, true_stack, maybe_stack, false_stack, checked, mixed, gate_sm, start_time);
333 336 if (free_checked)
334 337 free_slist(checked);
335 338 }
336 339
337 340 static void separate_pools(struct sm_state *sm, int comparison, struct range_list *rl,
338 341 struct state_list **true_stack,
339 342 struct state_list **false_stack,
340 343 struct state_list **checked, int *mixed)
341 344 {
342 345 struct state_list *maybe_stack = NULL;
343 346 struct sm_state *tmp;
344 347 struct timeval start_time;
345 348
346 349
347 350 gettimeofday(&start_time, NULL);
348 351 __separate_pools(sm, comparison, rl, true_stack, &maybe_stack, false_stack, checked, mixed, sm, &start_time);
349 352
350 353 if (implied_debug) {
351 354 struct sm_state *sm;
352 355
353 356 FOR_EACH_PTR(*true_stack, sm) {
354 357 sm_msg("TRUE %s [stree %d]", show_sm(sm), get_stree_id(sm->pool));
355 358 } END_FOR_EACH_PTR(sm);
356 359
357 360 FOR_EACH_PTR(maybe_stack, sm) {
358 361 sm_msg("MAYBE %s %s[stree %d]",
359 362 show_sm(sm), sm->merged ? "(merged) ": "", get_stree_id(sm->pool));
360 363 } END_FOR_EACH_PTR(sm);
361 364
362 365 FOR_EACH_PTR(*false_stack, sm) {
363 366 sm_msg("FALSE %s [stree %d]", show_sm(sm), get_stree_id(sm->pool));
364 367 } END_FOR_EACH_PTR(sm);
365 368 }
366 369 /* if it's a maybe then remove it */
367 370 FOR_EACH_PTR(maybe_stack, tmp) {
368 371 remove_pool(false_stack, tmp->pool);
369 372 remove_pool(true_stack, tmp->pool);
370 373 } END_FOR_EACH_PTR(tmp);
371 374
372 375 /* if it's both true and false remove it from both */
373 376 FOR_EACH_PTR(*true_stack, tmp) {
374 377 if (remove_pool(false_stack, tmp->pool))
375 378 DELETE_CURRENT_PTR(tmp);
376 379 } END_FOR_EACH_PTR(tmp);
377 380 }
378 381
379 382 static int sm_in_keep_leafs(struct sm_state *sm, const struct state_list *keep_gates)
380 383 {
381 384 struct sm_state *tmp, *old;
382 385
383 386 FOR_EACH_PTR(keep_gates, tmp) {
384 387 if (is_merged(tmp))
385 388 continue;
386 389 old = get_sm_state_stree(tmp->pool, sm->owner, sm->name, sm->sym);
387 390 if (!old)
388 391 continue;
389 392 if (old == sm)
390 393 return 1;
391 394 } END_FOR_EACH_PTR(tmp);
392 395 return 0;
393 396 }
394 397
395 398 static int going_too_slow(void)
396 399 {
397 400 static void *printed;
398 401
399 402 if (out_of_memory()) {
400 403 implications_off = true;
401 404 return 1;
402 405 }
403 406
404 407 if (!option_timeout || time_parsing_function() < option_timeout) {
405 408 implications_off = false;
406 409 return 0;
407 410 }
408 411
409 412 if (!__inline_fn && printed != cur_func_sym) {
410 413 if (!is_skipped_function())
411 414 sm_perror("turning off implications after %d seconds", option_timeout);
412 415 printed = cur_func_sym;
413 416 }
414 417 implications_off = true;
415 418 return 1;
416 419 }
417 420
418 421 static char *sm_state_info(struct sm_state *sm)
419 422 {
420 423 static char buf[512];
421 424 int n = 0;
422 425
423 426 n += snprintf(buf + n, sizeof(buf) - n, "[stree %d line %d] ",
424 427 get_stree_id(sm->pool), sm->line);
425 428 if (n >= sizeof(buf))
426 429 return buf;
427 430 n += snprintf(buf + n, sizeof(buf) - n, "%s ", show_sm(sm));
428 431 if (n >= sizeof(buf))
429 432 return buf;
430 433 n += snprintf(buf + n, sizeof(buf) - n, "left = %s [stree %d] ",
431 434 sm->left ? sm->left->state->name : "<none>",
432 435 sm->left ? get_stree_id(sm->left->pool) : -1);
433 436 if (n >= sizeof(buf))
434 437 return buf;
435 438 n += snprintf(buf + n, sizeof(buf) - n, "right = %s [stree %d]",
436 439 sm->right ? sm->right->state->name : "<none>",
437 440 sm->right ? get_stree_id(sm->right->pool) : -1);
438 441 return buf;
439 442 }
440 443
441 444 /*
442 445 * NOTE: If a state is in both the keep stack and the remove stack then that is
443 446 * a bug. Only add states which are definitely true or definitely false. If
444 447 * you have a leaf state that could be both true and false, then create a fake
445 448 * split history where one side is true and one side is false. Otherwise, if
446 449 * you can't do that, then don't add it to either list.
447 450 */
448 451 #define RECURSE_LIMIT 300
449 452 struct sm_state *filter_pools(struct sm_state *sm,
450 453 const struct state_list *remove_stack,
451 454 const struct state_list *keep_stack,
452 455 int *modified, int *recurse_cnt,
453 456 struct timeval *start, int *skip, int *bail)
454 457 {
455 458 struct sm_state *ret = NULL;
456 459 struct sm_state *left;
457 460 struct sm_state *right;
458 461 int removed = 0;
459 462 struct timeval now, diff;
460 463
461 464 if (!sm)
462 465 return NULL;
463 466 if (*bail)
464 467 return NULL;
465 468 gettimeofday(&now, NULL);
466 469 timersub(&now, start, &diff);
467 470 if (diff.tv_sec >= 3) {
468 471 DIMPLIED("%s: implications taking too long: %s\n", __func__, sm_state_info(sm));
469 472 *bail = 1;
470 473 return NULL;
471 474 }
472 475 if ((*recurse_cnt)++ > RECURSE_LIMIT) {
473 476 DIMPLIED("%s: recursed too far: %s\n", __func__, sm_state_info(sm));
474 477 *skip = 1;
475 478 return NULL;
476 479 }
477 480
478 481 if (pool_in_pools(sm->pool, remove_stack)) {
479 482 DIMPLIED("%s: remove: %s\n", __func__, sm_state_info(sm));
480 483 *modified = 1;
481 484 return NULL;
482 485 }
483 486
484 487 if (!is_merged(sm) || pool_in_pools(sm->pool, keep_stack) || sm_in_keep_leafs(sm, keep_stack)) {
485 488 DIMPLIED("%s: keep %s (%s, %s, %s): %s\n", __func__, sm->state->name,
486 489 is_merged(sm) ? "merged" : "not merged",
487 490 pool_in_pools(sm->pool, keep_stack) ? "not in keep pools" : "in keep pools",
488 491 sm_in_keep_leafs(sm, keep_stack) ? "reachable keep leaf" : "no keep leaf",
489 492 sm_state_info(sm));
490 493 return sm;
491 494 }
492 495
493 496 left = filter_pools(sm->left, remove_stack, keep_stack, &removed, recurse_cnt, start, skip, bail);
494 497 right = filter_pools(sm->right, remove_stack, keep_stack, &removed, recurse_cnt, start, skip, bail);
495 498 if (*bail || *skip)
496 499 return NULL;
497 500 if (!removed) {
498 501 DIMPLIED("%s: kept all: %s\n", __func__, sm_state_info(sm));
499 502 return sm;
500 503 }
501 504 *modified = 1;
502 505 if (!left && !right) {
503 506 DIMPLIED("%s: removed all: %s\n", __func__, sm_state_info(sm));
504 507 return NULL;
505 508 }
506 509
507 510 if (!left) {
508 511 ret = clone_sm(right);
509 512 ret->merged = 1;
510 513 ret->right = right;
511 514 ret->left = NULL;
512 515 } else if (!right) {
513 516 ret = clone_sm(left);
514 517 ret->merged = 1;
515 518 ret->left = left;
516 519 ret->right = NULL;
517 520 } else {
518 521 if (left->sym != sm->sym || strcmp(left->name, sm->name) != 0) {
519 522 left = clone_sm(left);
520 523 left->sym = sm->sym;
521 524 left->name = sm->name;
522 525 }
523 526 if (right->sym != sm->sym || strcmp(right->name, sm->name) != 0) {
524 527 right = clone_sm(right);
525 528 right->sym = sm->sym;
526 529 right->name = sm->name;
527 530 }
528 531 ret = merge_sm_states(left, right);
529 532 }
530 533
531 534 ret->pool = sm->pool;
532 535
533 536 DIMPLIED("%s: partial: %s\n", __func__, sm_state_info(sm));
534 537 return ret;
535 538 }
536 539
537 540 static struct stree *filter_stack(struct sm_state *gate_sm,
538 541 struct stree *pre_stree,
539 542 const struct state_list *remove_stack,
540 543 const struct state_list *keep_stack)
541 544 {
542 545 struct stree *ret = NULL;
543 546 struct sm_state *tmp;
544 547 struct sm_state *filtered_sm;
545 548 int modified;
546 549 int recurse_cnt;
547 550 struct timeval start;
548 551 int skip;
549 552 int bail = 0;
550 553
551 554 if (!remove_stack)
552 555 return NULL;
553 556
554 557 gettimeofday(&start, NULL);
555 558 FOR_EACH_SM(pre_stree, tmp) {
556 559 if (!tmp->merged || sm_in_keep_leafs(tmp, keep_stack))
557 560 continue;
558 561 modified = 0;
559 562 recurse_cnt = 0;
560 563 skip = 0;
561 564 filtered_sm = filter_pools(tmp, remove_stack, keep_stack, &modified, &recurse_cnt, &start, &skip, &bail);
562 565 if (going_too_slow())
563 566 return NULL;
564 567 if (bail)
565 568 return ret; /* Return the implications we figured out before time ran out. */
566 569
567 570
568 571 if (skip || !filtered_sm || !modified)
569 572 continue;
570 573 /* the assignments here are for borrowed implications */
571 574 filtered_sm->name = tmp->name;
572 575 filtered_sm->sym = tmp->sym;
573 576 avl_insert(&ret, filtered_sm);
574 577 } END_FOR_EACH_SM(tmp);
575 578 return ret;
576 579 }
577 580
578 581 static void separate_and_filter(struct sm_state *sm, int comparison, struct range_list *rl,
579 582 struct stree *pre_stree,
580 583 struct stree **true_states,
581 584 struct stree **false_states,
582 585 int *mixed)
583 586 {
584 587 struct state_list *true_stack = NULL;
585 588 struct state_list *false_stack = NULL;
586 589 struct timeval time_before;
587 590 struct timeval time_after;
588 591 int sec;
589 592
590 593 gettimeofday(&time_before, NULL);
591 594
592 595 DIMPLIED("checking implications: (%s (%s) %s %s)\n",
593 596 sm->name, sm->state->name, show_special(comparison), show_rl(rl));
594 597
595 598 if (!is_merged(sm)) {
596 599 DIMPLIED("%d '%s' from line %d is not merged.\n", get_lineno(), sm->name, sm->line);
597 600 return;
598 601 }
599 602
600 603 separate_pools(sm, comparison, rl, &true_stack, &false_stack, NULL, mixed);
601 604
602 605 DIMPLIED("filtering true stack.\n");
603 606 *true_states = filter_stack(sm, pre_stree, false_stack, true_stack);
604 607 DIMPLIED("filtering false stack.\n");
605 608 *false_states = filter_stack(sm, pre_stree, true_stack, false_stack);
606 609 free_slist(&true_stack);
607 610 free_slist(&false_stack);
608 611
609 612 gettimeofday(&time_after, NULL);
610 613 sec = time_after.tv_sec - time_before.tv_sec;
611 614 if (option_timeout && sec > option_timeout) {
612 615 sm_perror("Function too hairy. Ignoring implications after %d seconds.", sec);
613 616 }
614 617 }
615 618
616 619 static struct expression *get_last_expr(struct statement *stmt)
617 620 {
618 621 struct statement *last;
619 622
620 623 last = last_ptr_list((struct ptr_list *)stmt->stmts);
621 624 if (last->type == STMT_EXPRESSION)
622 625 return last->expression;
623 626
624 627 if (last->type == STMT_LABEL) {
625 628 if (last->label_statement &&
626 629 last->label_statement->type == STMT_EXPRESSION)
627 630 return last->label_statement->expression;
628 631 }
629 632
630 633 return NULL;
631 634 }
632 635
633 636 static struct expression *get_left_most_expr(struct expression *expr)
634 637 {
635 638 struct statement *compound;
636 639
637 640 compound = get_expression_statement(expr);
638 641 if (compound)
639 642 return get_last_expr(compound);
640 643
641 644 expr = strip_parens(expr);
642 645 if (expr->type == EXPR_ASSIGNMENT)
643 646 return get_left_most_expr(expr->left);
644 647 return expr;
645 648 }
646 649
647 650 static int is_merged_expr(struct expression *expr)
648 651 {
649 652 struct sm_state *sm;
650 653 sval_t dummy;
651 654
652 655 if (get_value(expr, &dummy))
653 656 return 0;
654 657 sm = get_sm_state_expr(SMATCH_EXTRA, expr);
655 658 if (!sm)
656 659 return 0;
657 660 if (is_merged(sm))
658 661 return 1;
659 662 return 0;
660 663 }
661 664
662 665 static void delete_gate_sm_equiv(struct stree **stree, const char *name, struct symbol *sym)
663 666 {
664 667 struct smatch_state *state;
665 668 struct relation *rel;
666 669
667 670 state = get_state(SMATCH_EXTRA, name, sym);
668 671 if (!state)
669 672 return;
670 673 FOR_EACH_PTR(estate_related(state), rel) {
671 674 delete_state_stree(stree, SMATCH_EXTRA, rel->name, rel->sym);
672 675 } END_FOR_EACH_PTR(rel);
673 676 }
674 677
675 678 static void delete_gate_sm(struct stree **stree, const char *name, struct symbol *sym)
676 679 {
677 680 delete_state_stree(stree, SMATCH_EXTRA, name, sym);
678 681 }
679 682
680 683 static int handle_comparison(struct expression *expr,
681 684 struct stree **implied_true,
682 685 struct stree **implied_false)
683 686 {
684 687 struct sm_state *sm = NULL;
685 688 struct range_list *rl = NULL;
686 689 struct expression *left;
687 690 struct expression *right;
688 691 struct symbol *type;
689 692 int comparison = expr->op;
690 693 int mixed = 0;
691 694
692 695 left = get_left_most_expr(expr->left);
693 696 right = get_left_most_expr(expr->right);
694 697
695 698 if (is_merged_expr(left)) {
696 699 sm = get_sm_state_expr(SMATCH_EXTRA, left);
697 700 get_implied_rl(right, &rl);
698 701 } else if (is_merged_expr(right)) {
699 702 sm = get_sm_state_expr(SMATCH_EXTRA, right);
700 703 get_implied_rl(left, &rl);
701 704 comparison = flip_comparison(comparison);
702 705 }
703 706
704 707 if (!rl || !sm)
705 708 return 0;
706 709
707 710 type = get_type(expr);
708 711 if (!type)
709 712 return 0;
710 713 if (type_positive_bits(rl_type(rl)) > type_positive_bits(type))
711 714 type = rl_type(rl);
712 715 if (type_positive_bits(type) < 31)
713 716 type = &int_ctype;
714 717 rl = cast_rl(type, rl);
715 718
716 719 separate_and_filter(sm, comparison, rl, __get_cur_stree(), implied_true, implied_false, &mixed);
717 720
718 721 delete_gate_sm_equiv(implied_true, sm->name, sm->sym);
719 722 delete_gate_sm_equiv(implied_false, sm->name, sm->sym);
720 723 if (mixed) {
721 724 delete_gate_sm(implied_true, sm->name, sm->sym);
722 725 delete_gate_sm(implied_false, sm->name, sm->sym);
723 726 }
724 727
725 728 return 1;
726 729 }
727 730
728 731 static int handle_zero_comparison(struct expression *expr,
729 732 struct stree **implied_true,
730 733 struct stree **implied_false)
731 734 {
732 735 struct symbol *sym;
733 736 char *name;
734 737 struct sm_state *sm;
735 738 int mixed = 0;
736 739 int ret = 0;
737 740
738 741 if (expr->type == EXPR_POSTOP)
739 742 expr = strip_expr(expr->unop);
740 743
741 744 if (expr->type == EXPR_ASSIGNMENT) {
742 745 /* most of the time ->pools will be empty here because we
743 746 just set the state, but if have assigned a conditional
744 747 function there are implications. */
745 748 expr = expr->left;
746 749 }
747 750
748 751 name = expr_to_var_sym(expr, &sym);
749 752 if (!name || !sym)
750 753 goto free;
751 754 sm = get_sm_state(SMATCH_EXTRA, name, sym);
752 755 if (!sm)
753 756 goto free;
754 757
755 758 separate_and_filter(sm, SPECIAL_NOTEQUAL, tmp_range_list(estate_type(sm->state), 0), __get_cur_stree(), implied_true, implied_false, &mixed);
756 759 delete_gate_sm_equiv(implied_true, sm->name, sm->sym);
757 760 delete_gate_sm_equiv(implied_false, sm->name, sm->sym);
758 761 if (mixed) {
759 762 delete_gate_sm(implied_true, sm->name, sm->sym);
760 763 delete_gate_sm(implied_false, sm->name, sm->sym);
761 764 }
762 765
763 766 ret = 1;
764 767 free:
765 768 free_string(name);
766 769 return ret;
767 770 }
768 771
769 772 static int handled_by_comparison_hook(struct expression *expr,
770 773 struct stree **implied_true,
771 774 struct stree **implied_false)
772 775 {
773 776 struct state_list *true_stack = NULL;
774 777 struct state_list *false_stack = NULL;
775 778 struct stree *pre_stree;
776 779 struct sm_state *sm;
777 780
778 781 sm = comparison_implication_hook(expr, &true_stack, &false_stack);
779 782 if (!sm)
780 783 return 0;
781 784
782 785 pre_stree = clone_stree(__get_cur_stree());
783 786
784 787 *implied_true = filter_stack(sm, pre_stree, false_stack, true_stack);
785 788 *implied_false = filter_stack(sm, pre_stree, true_stack, false_stack);
786 789
787 790 free_stree(&pre_stree);
788 791 free_slist(&true_stack);
789 792 free_slist(&false_stack);
790 793
791 794 return 1;
792 795 }
793 796
794 797 static int handled_by_extra_states(struct expression *expr,
795 798 struct stree **implied_true,
796 799 struct stree **implied_false)
797 800 {
798 801 sval_t sval;
799 802
|
↓ open down ↓ |
641 lines elided |
↑ open up ↑ |
800 803 /* If the expression is known then it has no implications. */
801 804 if (get_implied_value(expr, &sval))
802 805 return true;
803 806
804 807 if (expr->type == EXPR_COMPARE)
805 808 return handle_comparison(expr, implied_true, implied_false);
806 809 else
807 810 return handle_zero_comparison(expr, implied_true, implied_false);
808 811 }
809 812
813 +static int handled_by_parsed_conditions(struct expression *expr,
814 + struct stree **implied_true,
815 + struct stree **implied_false)
816 +{
817 + struct state_list *true_stack = NULL;
818 + struct state_list *false_stack = NULL;
819 + struct stree *pre_stree;
820 + struct sm_state *sm;
821 +
822 + sm = parsed_condition_implication_hook(expr, &true_stack, &false_stack);
823 + if (!sm)
824 + return 0;
825 +
826 + pre_stree = clone_stree(__get_cur_stree());
827 +
828 + *implied_true = filter_stack(sm, pre_stree, false_stack, true_stack);
829 + *implied_false = filter_stack(sm, pre_stree, true_stack, false_stack);
830 +
831 + free_stree(&pre_stree);
832 + free_slist(&true_stack);
833 + free_slist(&false_stack);
834 +
835 + return 1;
836 +}
837 +
810 838 static int handled_by_stored_conditions(struct expression *expr,
811 839 struct stree **implied_true,
812 840 struct stree **implied_false)
813 841 {
814 842 struct state_list *true_stack = NULL;
815 843 struct state_list *false_stack = NULL;
816 844 struct stree *pre_stree;
817 845 struct sm_state *sm;
818 846
819 847 sm = stored_condition_implication_hook(expr, &true_stack, &false_stack);
820 848 if (!sm)
821 849 return 0;
822 850
823 851 pre_stree = clone_stree(__get_cur_stree());
824 852
825 853 *implied_true = filter_stack(sm, pre_stree, false_stack, true_stack);
826 854 *implied_false = filter_stack(sm, pre_stree, true_stack, false_stack);
827 855
828 856 free_stree(&pre_stree);
829 857 free_slist(&true_stack);
|
↓ open down ↓ |
10 lines elided |
↑ open up ↑ |
830 858 free_slist(&false_stack);
831 859
832 860 return 1;
833 861 }
834 862
835 863 static struct stree *saved_implied_true;
836 864 static struct stree *saved_implied_false;
837 865 static struct stree *extra_saved_implied_true;
838 866 static struct stree *extra_saved_implied_false;
839 867
840 -static void separate_extra_states(struct stree **implied_true,
841 - struct stree **implied_false)
868 +static void separate_implication_states(struct stree **implied_true,
869 + struct stree **implied_false,
870 + int owner)
842 871 {
843 872 struct sm_state *sm;
844 873
845 - /* We process extra states later to preserve the implications. */
874 + /* We process these states later to preserve the implications. */
846 875 FOR_EACH_SM(*implied_true, sm) {
847 - if (sm->owner == SMATCH_EXTRA)
876 + if (sm->owner == owner)
848 877 overwrite_sm_state_stree(&extra_saved_implied_true, sm);
849 878 } END_FOR_EACH_SM(sm);
850 879 FOR_EACH_SM(extra_saved_implied_true, sm) {
851 880 delete_state_stree(implied_true, sm->owner, sm->name, sm->sym);
852 881 } END_FOR_EACH_SM(sm);
853 882
854 883 FOR_EACH_SM(*implied_false, sm) {
855 - if (sm->owner == SMATCH_EXTRA)
884 + if (sm->owner == owner)
856 885 overwrite_sm_state_stree(&extra_saved_implied_false, sm);
857 886 } END_FOR_EACH_SM(sm);
858 887 FOR_EACH_SM(extra_saved_implied_false, sm) {
859 888 delete_state_stree(implied_false, sm->owner, sm->name, sm->sym);
860 889 } END_FOR_EACH_SM(sm);
861 890 }
862 891
863 892 static void get_tf_states(struct expression *expr,
864 893 struct stree **implied_true,
865 894 struct stree **implied_false)
866 895 {
867 - if (handled_by_comparison_hook(expr, implied_true, implied_false))
896 + if (handled_by_parsed_conditions(expr, implied_true, implied_false))
868 897 return;
869 898
899 + if (handled_by_comparison_hook(expr, implied_true, implied_false)) {
900 + separate_implication_states(implied_true, implied_false, comparison_id);
901 + return;
902 + }
903 +
870 904 if (handled_by_extra_states(expr, implied_true, implied_false)) {
871 - separate_extra_states(implied_true, implied_false);
905 + separate_implication_states(implied_true, implied_false, SMATCH_EXTRA);
872 906 return;
873 907 }
874 908
875 909 if (handled_by_stored_conditions(expr, implied_true, implied_false))
876 910 return;
877 911 }
878 912
879 913 static void save_implications_hook(struct expression *expr)
880 914 {
881 915 if (going_too_slow())
882 916 return;
883 917 get_tf_states(expr, &saved_implied_true, &saved_implied_false);
884 918 }
885 919
886 920 static void set_implied_states(struct expression *expr)
887 921 {
888 922 struct sm_state *sm;
889 923
890 924 if (implied_debug &&
891 925 (expr || saved_implied_true || saved_implied_false)) {
892 926 char *name;
893 927
894 928 name = expr_to_str(expr);
895 929 printf("These are the implied states for the true path: (%s)\n", name);
896 930 __print_stree(saved_implied_true);
897 931 printf("These are the implied states for the false path: (%s)\n", name);
898 932 __print_stree(saved_implied_false);
899 933 free_string(name);
900 934 }
901 935
902 936 FOR_EACH_SM(saved_implied_true, sm) {
903 937 __set_true_false_sm(sm, NULL);
904 938 } END_FOR_EACH_SM(sm);
905 939 free_stree(&saved_implied_true);
906 940
907 941 FOR_EACH_SM(saved_implied_false, sm) {
908 942 __set_true_false_sm(NULL, sm);
909 943 } END_FOR_EACH_SM(sm);
910 944 free_stree(&saved_implied_false);
911 945 }
912 946
913 947 static void set_extra_implied_states(struct expression *expr)
914 948 {
915 949 saved_implied_true = extra_saved_implied_true;
916 950 saved_implied_false = extra_saved_implied_false;
917 951 extra_saved_implied_true = NULL;
918 952 extra_saved_implied_false = NULL;
919 953 set_implied_states(NULL);
920 954 }
921 955
922 956 void param_limit_implications(struct expression *expr, int param, char *key, char *value)
923 957 {
924 958 struct expression *arg;
925 959 struct symbol *compare_type;
926 960 char *name;
927 961 struct symbol *sym;
928 962 struct sm_state *sm;
929 963 struct sm_state *tmp;
930 964 struct stree *implied_true = NULL;
931 965 struct stree *implied_false = NULL;
932 966 struct range_list *orig, *limit;
933 967
934 968 if (time_parsing_function() > 40)
935 969 return;
936 970
937 971 while (expr->type == EXPR_ASSIGNMENT)
938 972 expr = strip_expr(expr->right);
939 973 if (expr->type != EXPR_CALL)
940 974 return;
941 975
942 976 arg = get_argument_from_call_expr(expr->args, param);
943 977 if (!arg)
944 978 return;
945 979
946 980 arg = strip_parens(arg);
947 981 while (arg->type == EXPR_ASSIGNMENT && arg->op == '=')
948 982 arg = strip_parens(arg->left);
949 983
950 984 name = get_variable_from_key(arg, key, &sym);
951 985 if (!name || !sym)
952 986 goto free;
953 987
954 988 sm = get_sm_state(SMATCH_EXTRA, name, sym);
955 989 if (!sm || !sm->merged)
956 990 goto free;
957 991
958 992 if (strcmp(key, "$") == 0)
959 993 compare_type = get_arg_type(expr->fn, param);
960 994 else
961 995 compare_type = get_member_type_from_key(arg, key);
962 996
963 997 orig = estate_rl(sm->state);
964 998 orig = cast_rl(compare_type, orig);
965 999
966 1000 call_results_to_rl(expr, compare_type, value, &limit);
967 1001
968 1002 separate_and_filter(sm, SPECIAL_EQUAL, limit, __get_cur_stree(), &implied_true, &implied_false, NULL);
969 1003
970 1004 FOR_EACH_SM(implied_true, tmp) {
971 1005 __set_sm_fake_stree(tmp);
972 1006 } END_FOR_EACH_SM(tmp);
973 1007
974 1008 free_stree(&implied_true);
975 1009 free_stree(&implied_false);
976 1010 free:
977 1011 free_string(name);
978 1012 }
979 1013
980 1014 struct stree *__implied_case_stree(struct expression *switch_expr,
981 1015 struct range_list *rl,
982 1016 struct range_list_stack **remaining_cases,
983 1017 struct stree **raw_stree)
984 1018 {
985 1019 char *name;
986 1020 struct symbol *sym;
987 1021 struct var_sym_list *vsl;
988 1022 struct sm_state *sm;
989 1023 struct stree *true_states = NULL;
990 1024 struct stree *false_states = NULL;
991 1025 struct stree *extra_states;
992 1026 struct stree *ret = clone_stree(*raw_stree);
993 1027
994 1028 name = expr_to_chunk_sym_vsl(switch_expr, &sym, &vsl);
995 1029
996 1030 if (rl)
997 1031 filter_top_rl(remaining_cases, rl);
998 1032 else
999 1033 rl = clone_rl(top_rl(*remaining_cases));
1000 1034
1001 1035 if (name) {
1002 1036 sm = get_sm_state_stree(*raw_stree, SMATCH_EXTRA, name, sym);
1003 1037 if (sm)
1004 1038 separate_and_filter(sm, SPECIAL_EQUAL, rl, *raw_stree, &true_states, &false_states, NULL);
1005 1039 }
1006 1040
1007 1041 __push_fake_cur_stree();
1008 1042 __unnullify_path();
1009 1043 if (name)
1010 1044 set_extra_nomod_vsl(name, sym, vsl, NULL, alloc_estate_rl(rl));
1011 1045 __pass_case_to_client(switch_expr, rl);
1012 1046 extra_states = __pop_fake_cur_stree();
1013 1047 overwrite_stree(extra_states, &true_states);
1014 1048 overwrite_stree(true_states, &ret);
1015 1049 free_stree(&extra_states);
1016 1050 free_stree(&true_states);
1017 1051 free_stree(&false_states);
1018 1052
1019 1053 free_string(name);
1020 1054 return ret;
1021 1055 }
1022 1056
1023 1057 static void match_end_func(struct symbol *sym)
1024 1058 {
1025 1059 if (__inline_fn)
1026 1060 return;
1027 1061 implied_debug_msg = NULL;
1028 1062 }
1029 1063
1030 1064 static void get_tf_stacks_from_pool(struct sm_state *gate_sm,
1031 1065 struct sm_state *pool_sm,
1032 1066 struct state_list **true_stack,
1033 1067 struct state_list **false_stack)
1034 1068 {
1035 1069 struct sm_state *tmp;
1036 1070 int possibly_true = 0;
1037 1071
1038 1072 if (!gate_sm)
1039 1073 return;
1040 1074
1041 1075 if (strcmp(gate_sm->state->name, pool_sm->state->name) == 0) {
1042 1076 add_ptr_list(true_stack, pool_sm);
1043 1077 return;
1044 1078 }
1045 1079
1046 1080 FOR_EACH_PTR(gate_sm->possible, tmp) {
1047 1081 if (strcmp(tmp->state->name, pool_sm->state->name) == 0) {
1048 1082 possibly_true = 1;
1049 1083 break;
1050 1084 }
1051 1085 } END_FOR_EACH_PTR(tmp);
1052 1086
1053 1087 if (!possibly_true) {
1054 1088 add_ptr_list(false_stack, gate_sm);
1055 1089 return;
1056 1090 }
1057 1091
1058 1092 get_tf_stacks_from_pool(gate_sm->left, pool_sm, true_stack, false_stack);
1059 1093 get_tf_stacks_from_pool(gate_sm->right, pool_sm, true_stack, false_stack);
1060 1094 }
1061 1095
1062 1096 /*
1063 1097 * The situation is we have a SMATCH_EXTRA state and we want to break it into
1064 1098 * each of the ->possible states and find the implications of each. The caller
1065 1099 * has to use __push_fake_cur_stree() to preserve the correct states so they
1066 1100 * can be restored later.
1067 1101 */
1068 1102 void overwrite_states_using_pool(struct sm_state *gate_sm, struct sm_state *pool_sm)
1069 1103 {
1070 1104 struct state_list *true_stack = NULL;
1071 1105 struct state_list *false_stack = NULL;
1072 1106 struct stree *pre_stree;
1073 1107 struct stree *implied_true;
1074 1108 struct sm_state *tmp;
1075 1109
1076 1110 if (!pool_sm->pool)
1077 1111 return;
1078 1112
1079 1113 get_tf_stacks_from_pool(gate_sm, pool_sm, &true_stack, &false_stack);
1080 1114
1081 1115 pre_stree = clone_stree(__get_cur_stree());
1082 1116
1083 1117 implied_true = filter_stack(gate_sm, pre_stree, false_stack, true_stack);
1084 1118
1085 1119 free_stree(&pre_stree);
1086 1120 free_slist(&true_stack);
1087 1121 free_slist(&false_stack);
1088 1122
1089 1123 FOR_EACH_SM(implied_true, tmp) {
1090 1124 set_state(tmp->owner, tmp->name, tmp->sym, tmp->state);
1091 1125 } END_FOR_EACH_SM(tmp);
1092 1126
1093 1127 free_stree(&implied_true);
1094 1128 }
1095 1129
1096 1130 int assume(struct expression *expr)
1097 1131 {
1098 1132 int orig_final_pass = final_pass;
1099 1133
1100 1134 in_fake_env++;
1101 1135 final_pass = 0;
1102 1136 __push_fake_cur_stree();
1103 1137 __split_whole_condition(expr);
1104 1138 final_pass = orig_final_pass;
1105 1139 in_fake_env--;
1106 1140
1107 1141 return 1;
1108 1142 }
1109 1143
1110 1144 void end_assume(void)
1111 1145 {
1112 1146 __discard_false_states();
1113 1147 __free_fake_cur_stree();
1114 1148 }
1115 1149
1116 1150 int impossible_assumption(struct expression *left, int op, sval_t sval)
1117 1151 {
1118 1152 struct expression *value;
1119 1153 struct expression *comparison;
1120 1154 int ret;
1121 1155
1122 1156 value = value_expr(sval.value);
1123 1157 comparison = compare_expression(left, op, value);
1124 1158
1125 1159 if (!assume(comparison))
1126 1160 return 0;
1127 1161 ret = is_impossible_path();
1128 1162 end_assume();
1129 1163
1130 1164 return ret;
|
↓ open down ↓ |
249 lines elided |
↑ open up ↑ |
1131 1165 }
1132 1166
1133 1167 void __extra_match_condition(struct expression *expr);
1134 1168 void __comparison_match_condition(struct expression *expr);
1135 1169 void __stored_condition(struct expression *expr);
1136 1170 void register_implications(int id)
1137 1171 {
1138 1172 add_hook(&save_implications_hook, CONDITION_HOOK);
1139 1173 add_hook(&set_implied_states, CONDITION_HOOK);
1140 1174 add_hook(&__extra_match_condition, CONDITION_HOOK);
1141 - add_hook(&set_extra_implied_states, CONDITION_HOOK);
1142 1175 add_hook(&__comparison_match_condition, CONDITION_HOOK);
1176 + add_hook(&set_extra_implied_states, CONDITION_HOOK);
1143 1177 add_hook(&__stored_condition, CONDITION_HOOK);
1144 1178 add_hook(&match_end_func, END_FUNC_HOOK);
1145 1179 }
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX