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