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