]>
Commit | Line | Data |
---|---|---|
d9900876 | 1 | /* |
11db3170 | 2 | ** Splint - annotation-assisted static program checker |
c59f5181 | 3 | ** Copyright (C) 1994-2003 University of Virginia, |
d9900876 | 4 | ** Massachusetts Institute of Technology |
5 | ** | |
6 | ** This program is free software; you can redistribute it and/or modify it | |
7 | ** under the terms of the GNU General Public License as published by the | |
8 | ** Free Software Foundation; either version 2 of the License, or (at your | |
9 | ** option) any later version. | |
10 | ** | |
11 | ** This program is distributed in the hope that it will be useful, but | |
12 | ** WITHOUT ANY WARRANTY; without even the implied warranty of | |
13 | ** MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU | |
14 | ** General Public License for more details. | |
15 | ** | |
16 | ** The GNU General Public License is available from http://www.gnu.org/ or | |
17 | ** the Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, | |
18 | ** MA 02111-1307, USA. | |
19 | ** | |
155af98d | 20 | ** For information on splint: info@splint.org |
21 | ** To report a bug: splint-bug@splint.org | |
11db3170 | 22 | ** For more information: http://www.splint.org |
d9900876 | 23 | */ |
24 | ||
25 | /* | |
26 | ** loopHeuristics.c | |
27 | */ | |
28 | ||
29 | /*This file was formerly called forjunk.c C | |
30 | renamed Oct 8, 2001 - DRL | |
31 | */ | |
32 | ||
33 | /* #define DEBUGPRINT 1 */ | |
34 | ||
35 | # include <ctype.h> /* for isdigit */ | |
1b8ae690 | 36 | # include "splintMacros.nf" |
d9900876 | 37 | # include "basic.h" |
38 | # include "cgrammar.h" | |
39 | # include "cgrammar_tokens.h" | |
40 | ||
41 | # include "exprChecks.h" | |
42 | # include "exprNodeSList.h" | |
43 | ||
2e4caa51 | 44 | /* this file was created to split the loop heuristics functionality out of constraintGeneration.c and constraint.c*/ |
45 | /*We need to access the internal representation of constraint | |
46 | see above for an explanation. | |
47 | */ | |
d9900876 | 48 | |
2e4caa51 | 49 | /*@access constraint @*/ |
d9900876 | 50 | |
2e4caa51 | 51 | static bool isInc (/*@observer@*/ constraintExpr p_c) /*@*/; |
52 | static bool incVar (/*@notnull@*/ constraint p_c) /*@*/; | |
d9900876 | 53 | |
54 | ||
55 | static bool increments (/*@observer@*/ constraint c, | |
56 | /*@observer@*/ constraintExpr var) | |
57 | { | |
bb7c2085 | 58 | llassert (constraint_isDefined (c) ); |
d9900876 | 59 | |
bb7c2085 | 60 | if (constraint_isUndefined (c) ) |
d9900876 | 61 | { |
62 | return FALSE; | |
63 | } | |
64 | ||
65 | llassert (incVar (c)); | |
66 | if (constraintExpr_similar (c->lexpr, var) ) | |
67 | return TRUE; | |
68 | else | |
69 | return FALSE; | |
70 | } | |
71 | ||
2e4caa51 | 72 | static /*@only@*/ constraintList getLessThanConstraints (/*@observer@*/ constraintList c) |
73 | { | |
74 | constraintList ret; | |
75 | ||
76 | ret = constraintList_makeNew (); | |
77 | constraintList_elements (c, el) | |
78 | { | |
79 | llassert (constraint_isDefined (el)); | |
80 | if ( constraint_isUndefined (el) ) | |
81 | continue; | |
82 | ||
83 | if (el->ar == LT || el->ar == LTE) | |
84 | { | |
85 | constraint temp; | |
86 | temp = constraint_copy (el); | |
87 | ||
88 | ret = constraintList_add (ret, temp); | |
89 | } | |
90 | } | |
91 | end_constraintList_elements; | |
92 | ||
93 | return ret; | |
94 | } | |
95 | ||
96 | static /*@only@*/ constraintList getIncConstraints (/*@observer@*/ constraintList c) | |
97 | { | |
98 | constraintList ret; | |
99 | ||
100 | ret = constraintList_makeNew (); | |
101 | constraintList_elements (c, el) | |
102 | { | |
103 | llassert (constraint_isDefined (el)); | |
104 | ||
105 | if (incVar (el) ) | |
106 | { | |
107 | constraint temp; | |
108 | temp = constraint_copy (el); | |
109 | ret = constraintList_add (ret, temp); | |
110 | } | |
111 | } | |
112 | end_constraintList_elements; | |
113 | ||
114 | return ret; | |
115 | } | |
116 | ||
117 | /*@access exprNode@*/ | |
d9900876 | 118 | static bool canGetForTimes (/*@notnull@*/ exprNode forPred, /*@notnull@*/ exprNode forBody) |
119 | { | |
120 | ||
121 | exprNode init, test, inc, t1, t2; | |
122 | lltok tok; | |
123 | ||
bb7c2085 | 124 | llassert (exprNode_isDefined (forPred) ); |
125 | llassert (exprNode_isDefined (forBody) ); | |
d9900876 | 126 | |
127 | init = exprData_getTripleInit (forPred->edata); | |
128 | test = exprData_getTripleTest (forPred->edata); | |
129 | inc = exprData_getTripleInc (forPred->edata); | |
130 | ||
bb7c2085 | 131 | llassert (exprNode_isDefined (test) ); |
d9900876 | 132 | |
bb7c2085 | 133 | if (exprNode_isUndefined (test) ) |
d9900876 | 134 | { |
135 | return FALSE; | |
136 | } | |
137 | ||
bb7c2085 | 138 | llassert (exprNode_isDefined (inc) ); |
d9900876 | 139 | |
bb7c2085 | 140 | if (exprNode_isUndefined (inc) ) |
d9900876 | 141 | { |
142 | return FALSE; | |
143 | } | |
144 | ||
145 | if (test->kind != XPR_PREOP) | |
146 | return FALSE; | |
147 | ||
148 | tok = (exprData_getUopTok (test->edata)); | |
149 | if (!lltok_isMult (tok) ) | |
150 | { | |
151 | return FALSE; | |
152 | } | |
153 | ||
154 | /* should check preop too */ | |
155 | if (inc->kind != XPR_POSTOP) | |
156 | { | |
157 | return FALSE; | |
158 | } | |
159 | ||
160 | tok = (exprData_getUopTok (inc->edata)); | |
16c024b5 | 161 | if (lltok_isIncOp (tok) ) |
d9900876 | 162 | { |
163 | t1 = exprData_getUopNode (test->edata); | |
164 | t2 = exprData_getUopNode (inc->edata); | |
bb7c2085 | 165 | llassert (exprNode_isDefined (t2) && exprNode_isDefined (t2) ); |
d9900876 | 166 | |
bb7c2085 | 167 | if (exprNode_isUndefined (t1) || exprNode_isUndefined (t2) ) |
d9900876 | 168 | { |
169 | return FALSE; | |
170 | } | |
171 | ||
172 | if (sRef_sameName (t1->sref, t2->sref) ) | |
173 | { | |
174 | return TRUE; | |
175 | } | |
176 | } | |
177 | return FALSE; | |
178 | } | |
2e4caa51 | 179 | /*@noaccess exprNode@*/ |
d9900876 | 180 | |
d9900876 | 181 | |
2e4caa51 | 182 | /*@access exprNode@*/ |
d9900876 | 183 | static /*@only@*/ constraintExpr getForTimes (/*@notnull@*/ exprNode forPred, /*@notnull@*/ exprNode forBody) |
184 | { | |
185 | ||
186 | exprNode init, test, inc, t1, t2; | |
187 | constraintList ltCon; | |
188 | constraintList incCon; | |
189 | constraintExpr ret; | |
190 | ||
191 | lltok tok; | |
192 | ||
193 | init = exprData_getTripleInit (forPred->edata); | |
194 | test = exprData_getTripleTest (forPred->edata); | |
195 | inc = exprData_getTripleInc (forPred->edata); | |
196 | ||
bb7c2085 | 197 | llassert (exprNode_isDefined (test) ); |
198 | llassert (exprNode_isDefined (inc) ); | |
d9900876 | 199 | |
200 | ltCon = getLessThanConstraints (test->trueEnsuresConstraints); | |
201 | incCon = getIncConstraints (inc->ensuresConstraints); | |
202 | ||
8f58355a | 203 | DPRINTF (( message ("getForTimes: ltCon: %s from %s", constraintList_unparse (ltCon), constraintList_unparse (test->trueEnsuresConstraints) ) )); |
d9900876 | 204 | |
8f58355a | 205 | DPRINTF (( message ("getForTimes: incCon: %s from %s", constraintList_unparse (incCon), constraintList_unparse (inc->ensuresConstraints) ) )); |
d9900876 | 206 | |
207 | constraintList_elements (ltCon, el) | |
208 | { | |
bb7c2085 | 209 | constraintList_elements (incCon, el2) |
d9900876 | 210 | { |
2e4caa51 | 211 | llassert(constraint_isDefined (el ) ); |
212 | ||
213 | if ( (constraint_isDefined (el ) ) && ( increments (el2, el->lexpr) ) ) | |
d9900876 | 214 | { |
566b8b82 | 215 | DPRINTF (( message ("getForTimes: %s increments %s", constraint_printLocation (el2), constraint_printLocation (el) ) )); |
d9900876 | 216 | ret = constraintExpr_copy (el->expr); |
bb7c2085 | 217 | constraintList_free (ltCon); |
218 | constraintList_free (incCon); | |
d9900876 | 219 | return ret; |
220 | ||
221 | } | |
222 | else | |
393e573f | 223 | { |
224 | ; | |
566b8b82 | 225 | DPRINTF (( message ("getForTimes: %s doesn't increment %s", constraint_printLocation (el2), constraint_printLocation (el) ) )); |
393e573f | 226 | } |
d9900876 | 227 | } |
228 | end_constraintList_elements; | |
229 | } | |
230 | ||
231 | end_constraintList_elements; | |
232 | ||
bb7c2085 | 233 | constraintList_free (ltCon); |
234 | constraintList_free (incCon); | |
d9900876 | 235 | |
bb7c2085 | 236 | DPRINTF (( message ("getForTimes: %s %s resorting to ugly hack", exprNode_unparse (forPred), exprNode_unparse (forBody) ) )); |
d9900876 | 237 | if (! canGetForTimes (forPred, forBody) ) |
238 | { | |
239 | return NULL; | |
240 | } | |
241 | ||
242 | ||
243 | if (test->kind != XPR_PREOP) | |
244 | llassert (FALSE); | |
245 | ||
246 | tok = (exprData_getUopTok (test->edata)); | |
247 | if (!lltok_isMult (tok) ) | |
248 | { | |
249 | llassert ( FALSE ); | |
250 | } | |
251 | ||
252 | /* should check preop too */ | |
253 | if (inc->kind != XPR_POSTOP) | |
254 | { | |
255 | llassert (FALSE ); | |
256 | } | |
257 | ||
258 | tok = (exprData_getUopTok (inc->edata)); | |
16c024b5 | 259 | if (lltok_isIncOp (tok) ) |
d9900876 | 260 | { |
261 | t1 = exprData_getUopNode (test->edata); | |
262 | t2 = exprData_getUopNode (inc->edata); | |
2e4caa51 | 263 | |
264 | llassert(exprNode_isDefined(t1) && exprNode_isDefined(t2) ); | |
d9900876 | 265 | if (sRef_sameName (t1->sref, t2->sref) ) |
266 | { | |
267 | return (constraintExpr_makeMaxSetExpr (t1) ); | |
268 | } | |
269 | } | |
bb7c2085 | 270 | llassert ( FALSE); |
d9900876 | 271 | BADEXIT; |
272 | } | |
2e4caa51 | 273 | /*@noaccess exprNode@*/ |
d9900876 | 274 | |
275 | /*@access constraintExpr @*/ | |
276 | ||
277 | static /*@only@*/ constraintExpr constraintExpr_searchAndAdd (/*@only@*/ constraintExpr c, /*@observer@*/ constraintExpr find, /*@observer@*/ constraintExpr add) | |
278 | { | |
279 | constraintExprKind kind; | |
280 | constraintExpr temp; | |
281 | ||
2e4caa51 | 282 | |
283 | llassert (constraintExpr_isDefined (c) ); | |
284 | ||
bb7c2085 | 285 | DPRINTF (( message ("Doing constraintExpr_searchAndAdd %s %s %s ", |
286 | constraintExpr_unparse (c), constraintExpr_unparse (find), constraintExpr_unparse (add) ) ) ); | |
d9900876 | 287 | |
288 | if ( constraintExpr_similar (c, find) ) | |
289 | { | |
290 | ||
291 | constraintExpr newExpr; | |
292 | ||
293 | cstring cPrint; | |
294 | ||
bb7c2085 | 295 | cPrint = constraintExpr_unparse (c); |
d9900876 | 296 | |
297 | ||
bb7c2085 | 298 | newExpr = constraintExpr_makeAddExpr (c, constraintExpr_copy (add) ); |
d9900876 | 299 | |
bb7c2085 | 300 | DPRINTF ((message ("Replacing %q with %q", |
301 | cPrint, constraintExpr_unparse (newExpr) | |
d9900876 | 302 | ))); |
303 | return newExpr; | |
304 | } | |
305 | ||
306 | kind = c->kind; | |
307 | ||
308 | switch (kind) | |
309 | { | |
310 | case term: | |
311 | break; | |
312 | case unaryExpr: | |
313 | temp = constraintExprData_unaryExprGetExpr (c->data); | |
bb7c2085 | 314 | temp = constraintExpr_searchAndAdd (constraintExpr_copy (temp), find, add); |
d9900876 | 315 | c->data = constraintExprData_unaryExprSetExpr (c->data, temp); |
316 | break; | |
317 | case binaryexpr: | |
318 | ||
319 | temp = constraintExprData_binaryExprGetExpr1 (c->data); | |
bb7c2085 | 320 | temp = constraintExpr_searchAndAdd (constraintExpr_copy (temp), find, add); |
d9900876 | 321 | c->data = constraintExprData_binaryExprSetExpr1 (c->data, temp); |
322 | ||
323 | temp = constraintExprData_binaryExprGetExpr2 (c->data); | |
bb7c2085 | 324 | temp = constraintExpr_searchAndAdd (constraintExpr_copy (temp), find, add); |
d9900876 | 325 | c->data = constraintExprData_binaryExprSetExpr2 (c->data, temp); |
326 | break; | |
327 | default: | |
bb7c2085 | 328 | llassert (FALSE); |
d9900876 | 329 | } |
330 | return c; | |
331 | ||
332 | } | |
333 | ||
334 | /*@noaccess constraintExpr @*/ | |
335 | ||
336 | static constraint constraint_searchAndAdd (/*@returned@*/ constraint c, /*@observer@*/ constraintExpr find, /*@observer@*/ constraintExpr add) | |
337 | { | |
2e4caa51 | 338 | |
339 | ||
340 | llassert (constraint_isDefined (c) ); | |
341 | ||
d9900876 | 342 | llassert (constraint_search (c, find) ); |
bb7c2085 | 343 | DPRINTF (( message ("Doing constraint_searchAndAdd %s %s %s ", |
566b8b82 | 344 | constraint_printLocation (c), constraintExpr_unparse (find), constraintExpr_unparse (add) ) ) ); |
d9900876 | 345 | |
346 | c->lexpr = constraintExpr_searchAndAdd (c->lexpr, find, add); | |
347 | c->expr = constraintExpr_searchAndAdd (c->expr, find, add); | |
348 | ||
349 | c = constraint_simplify (c); | |
350 | c = constraint_simplify (c); | |
351 | ||
352 | return c; | |
353 | ||
354 | } | |
355 | ||
356 | static constraintList constraintList_searchAndAdd (/*@returned@*/ constraintList list, | |
357 | /*@observer@*/ constraintExpr find, /*@observer@*/ constraintExpr add) | |
358 | { | |
359 | constraintList newConstraints; | |
360 | constraintList ret; | |
361 | ||
bb7c2085 | 362 | newConstraints = constraintList_makeNew (); |
d9900876 | 363 | |
364 | constraintList_elements (list, el) | |
365 | { | |
366 | if (constraint_search (el, find) ) | |
367 | { | |
368 | constraint newExpr; | |
369 | newExpr = constraint_copy (el); | |
370 | ||
371 | newExpr = constraint_searchAndAdd (newExpr, find, add); | |
566b8b82 | 372 | DPRINTF (( (message ("Adding constraint %s ", constraint_printLocation (newExpr)) ) )); |
d9900876 | 373 | newConstraints = constraintList_add (newConstraints, newExpr); |
374 | } | |
375 | ||
376 | } | |
377 | end_constraintList_elements; | |
378 | ||
379 | ret = constraintList_addListFree (list, newConstraints); | |
380 | return ret; | |
381 | } | |
382 | ||
2e4caa51 | 383 | /*@access exprNode@*/ |
bb7c2085 | 384 | static void doAdjust (/*@unused@*/ exprNode e, /*@unused@*/ exprNode forPred, /*@observer@*/ exprNode forBody, /*@observer@*/ constraintExpr iterations) |
d9900876 | 385 | { |
2e4caa51 | 386 | |
387 | llassert (exprNode_isDefined (forBody) ); | |
388 | ||
d9900876 | 389 | constraintList_elements (forBody->ensuresConstraints, el) |
390 | { | |
391 | /* look for var = var + 1 */ | |
2e4caa51 | 392 | if (constraint_isDefined (el) && incVar (el) ) |
d9900876 | 393 | { |
566b8b82 | 394 | DPRINTF ((message ("Found inc variable constraint : %s", constraint_printLocation (el) ) )); |
bb7c2085 | 395 | forBody->requiresConstraints = constraintList_searchAndAdd (forBody->requiresConstraints, el->lexpr, iterations); |
d9900876 | 396 | } |
397 | } | |
398 | end_constraintList_elements; | |
399 | } | |
400 | ||
2e4caa51 | 401 | |
402 | /*@access exprNode@*/ | |
403 | ||
404 | ||
405 | static void forLoopHeuristicsImpl ( exprNode e, exprNode forPred, /*@observer@*/ exprNode forBody) | |
d9900876 | 406 | { |
407 | exprNode init, test, inc; | |
408 | ||
409 | constraintExpr iterations; | |
2e4caa51 | 410 | |
411 | llassert (exprNode_isDefined(forPred) ); | |
412 | llassert (exprNode_isDefined(forBody) ); | |
413 | ||
d9900876 | 414 | init = exprData_getTripleInit (forPred->edata); |
415 | test = exprData_getTripleTest (forPred->edata); | |
416 | inc = exprData_getTripleInc (forPred->edata); | |
417 | ||
418 | if (exprNode_isError (test) || exprNode_isError (inc) ) | |
419 | return; | |
420 | ||
421 | iterations = getForTimes (forPred, forBody ); | |
422 | ||
423 | if (constraintExpr_isDefined (iterations) ) | |
424 | { | |
425 | doAdjust ( e, forPred, forBody, iterations); | |
bb7c2085 | 426 | constraintExpr_free (iterations); |
d9900876 | 427 | } |
428 | } | |
2e4caa51 | 429 | /*@noaccess exprNode@*/ |
430 | ||
431 | void exprNode_forLoopHeuristics ( exprNode e, exprNode forPred, exprNode forBody) | |
432 | { | |
433 | forLoopHeuristicsImpl (e, forPred, forBody); | |
434 | } | |
435 | ||
436 | /*@access constraintExpr @*/ | |
437 | ||
438 | static bool isInc (/*@observer@*/ constraintExpr c) /*@*/ | |
439 | { | |
440 | ||
441 | llassert (constraintExpr_isDefined (c) ); | |
442 | if (c->kind == binaryexpr ) | |
443 | { | |
444 | constraintExprBinaryOpKind binOP; | |
445 | constraintExpr t1, t2; | |
446 | t1 = constraintExprData_binaryExprGetExpr1 (c->data); | |
447 | t2 = constraintExprData_binaryExprGetExpr2 (c->data); | |
448 | ||
449 | binOP = constraintExprData_binaryExprGetOp (c->data); | |
450 | if (binOP == BINARYOP_PLUS) | |
451 | if (constraintExpr_isLit (t2) && constraintExpr_getValue (t2) == 1 ) | |
452 | { | |
453 | return TRUE; | |
454 | } | |
455 | } | |
456 | ||
457 | return FALSE; | |
458 | } | |
459 | /*@noaccess constraintExpr @*/ | |
460 | ||
461 | /*@access constraintExpr @*/ | |
462 | /* look for constraints like cexrp = cexrp + 1 */ | |
463 | static bool incVar (/*@notnull@*/ constraint c) /*@*/ | |
464 | { | |
465 | constraintExpr t1; | |
466 | if (c->ar != EQ) | |
467 | { | |
468 | return FALSE; | |
469 | } | |
470 | if (! isInc (c->expr ) ) | |
471 | return FALSE; | |
472 | ||
473 | llassert (constraintExpr_isDefined (c->expr) ); | |
474 | llassert (c->expr->kind == binaryexpr); | |
475 | ||
476 | t1 = constraintExprData_binaryExprGetExpr1 (c->expr->data); | |
477 | if (constraintExpr_similar (c->lexpr, t1) ) | |
478 | return TRUE; | |
479 | ||
480 | return FALSE; | |
481 | } | |
482 | /*@noaccess constraintExpr @*/ | |
483 | ||
484 | ||
d9900876 | 485 | |
486 | ||
487 | /* else */ | |
488 | /* { */ | |
489 | /* DPRINTF (("Can't get for time ")); */ | |
490 | /* } */ | |
491 | ||
bb7c2085 | 492 | /* if (exprNode_isError (init) ) */ |
d9900876 | 493 | /* { */ |
494 | /* return; */ | |
495 | /* } */ | |
496 | ||
497 | /* if (init->kind == XPR_ASSIGN) */ | |
498 | /* { */ | |
499 | /* t1 = exprData_getOpA (init->edata); */ | |
500 | /* t2 = exprData_getOpB (init->edata); */ | |
501 | ||
502 | /* if (! (t1->kind == XPR_VAR) ) */ | |
503 | /* return; */ | |
504 | /* } */ | |
505 | /* else */ | |
506 | /* return; */ | |
507 | ||
508 | /* if (test->kind == XPR_FETCH) */ | |
509 | /* { */ | |
510 | /* t3 = exprData_getPairA (test->edata); */ | |
511 | /* t4 = exprData_getPairB (test->edata); */ | |
512 | ||
bb7c2085 | 513 | /* if (sRef_sameName (t1->sref, t4->sref) ) */ |
d9900876 | 514 | /* { */ |
bb7c2085 | 515 | /* DPRINTF ((message ("Found a for loop matching heuristic:%s", exprNode_unparse (forPred) ) )); */ |
516 | /* con = constraint_makeEnsureLteMaxRead (t1, t3); */ | |
517 | /* forPred->ensuresConstraints = constraintList_add (forPred->ensuresConstraints, con); */ | |
d9900876 | 518 | /* } */ |
519 | /* else */ | |
520 | /* { */ | |
bb7c2085 | 521 | /* DPRINTF ((message ("Didn't Find a for loop matching heuristic:%s %s and %s differ", exprNode_unparse (forPred), exprNode_unparse (t1), exprNode_unparse (t3) ) )); */ |
d9900876 | 522 | /* } */ |
523 | /* return; */ | |
524 | /* } */ |