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