]>
Commit | Line | Data |
---|---|---|
d9900876 | 1 | /* |
11db3170 | 2 | ** Splint - annotation-assisted static program checker |
77d37419 | 3 | ** Copyright (C) 1994-2002 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 | ||
44 | # include "exprDataQuite.i" | |
45 | ||
393e573f | 46 | /*@access constraint, exprNode @*/ /* !!! NO! */ |
d9900876 | 47 | |
393e573f | 48 | /*@access constraintExpr @*/ /* !!! NO! */ |
49 | ||
50 | /*@-nullderef@*/ /* !!! DRL needs to fix this code! */ | |
51 | /*@-nullstate@*/ /* !!! DRL needs to fix this code! */ | |
52 | /*@-nullpass@*/ /* !!! DRL needs to fix this code! */ | |
53 | /*@-temptrans@*/ /* !!! DRL needs to fix this code! */ | |
d9900876 | 54 | |
55 | static bool isInc (/*@observer@*/ constraintExpr c) /*@*/ | |
56 | { | |
57 | ||
bb7c2085 | 58 | llassert (constraintExpr_isDefined (c) ); |
d9900876 | 59 | if (c->kind == binaryexpr ) |
60 | { | |
61 | constraintExprBinaryOpKind binOP; | |
62 | constraintExpr t1, t2; | |
63 | t1 = constraintExprData_binaryExprGetExpr1 (c->data); | |
64 | t2 = constraintExprData_binaryExprGetExpr2 (c->data); | |
65 | ||
66 | binOP = constraintExprData_binaryExprGetOp (c->data); | |
67 | if (binOP == BINARYOP_PLUS) | |
68 | if (constraintExpr_isLit (t2) && constraintExpr_getValue (t2) == 1 ) | |
69 | { | |
70 | return TRUE; | |
71 | } | |
72 | } | |
73 | ||
74 | return FALSE; | |
75 | } | |
76 | ||
77 | /* look for constraints like cexrp = cexrp + 1 */ | |
78 | static bool incVar (/*@notnull@*/ constraint c) /*@*/ | |
79 | { | |
80 | constraintExpr t1; | |
81 | if (c->ar != EQ) | |
82 | { | |
83 | return FALSE; | |
84 | } | |
85 | if (! isInc (c->expr ) ) | |
86 | return FALSE; | |
87 | ||
bb7c2085 | 88 | llassert (constraintExpr_isDefined (c->expr) ); |
d9900876 | 89 | llassert (c->expr->kind == binaryexpr); |
90 | ||
91 | t1 = constraintExprData_binaryExprGetExpr1 (c->expr->data); | |
92 | if (constraintExpr_similar (c->lexpr, t1) ) | |
93 | return TRUE; | |
94 | ||
95 | return FALSE; | |
96 | } | |
97 | /*@noaccess constraintExpr @*/ | |
98 | ||
99 | ||
100 | static bool increments (/*@observer@*/ constraint c, | |
101 | /*@observer@*/ constraintExpr var) | |
102 | { | |
bb7c2085 | 103 | llassert (constraint_isDefined (c) ); |
d9900876 | 104 | |
bb7c2085 | 105 | if (constraint_isUndefined (c) ) |
d9900876 | 106 | { |
107 | return FALSE; | |
108 | } | |
109 | ||
110 | llassert (incVar (c)); | |
111 | if (constraintExpr_similar (c->lexpr, var) ) | |
112 | return TRUE; | |
113 | else | |
114 | return FALSE; | |
115 | } | |
116 | ||
117 | static bool canGetForTimes (/*@notnull@*/ exprNode forPred, /*@notnull@*/ exprNode forBody) | |
118 | { | |
119 | ||
120 | exprNode init, test, inc, t1, t2; | |
121 | lltok tok; | |
122 | ||
bb7c2085 | 123 | llassert (exprNode_isDefined (forPred) ); |
124 | llassert (exprNode_isDefined (forBody) ); | |
d9900876 | 125 | |
126 | init = exprData_getTripleInit (forPred->edata); | |
127 | test = exprData_getTripleTest (forPred->edata); | |
128 | inc = exprData_getTripleInc (forPred->edata); | |
129 | ||
bb7c2085 | 130 | llassert (exprNode_isDefined (test) ); |
d9900876 | 131 | |
bb7c2085 | 132 | if (exprNode_isUndefined (test) ) |
d9900876 | 133 | { |
134 | return FALSE; | |
135 | } | |
136 | ||
bb7c2085 | 137 | llassert (exprNode_isDefined (inc) ); |
d9900876 | 138 | |
bb7c2085 | 139 | if (exprNode_isUndefined (inc) ) |
d9900876 | 140 | { |
141 | return FALSE; | |
142 | } | |
143 | ||
144 | if (test->kind != XPR_PREOP) | |
145 | return FALSE; | |
146 | ||
147 | tok = (exprData_getUopTok (test->edata)); | |
148 | if (!lltok_isMult (tok) ) | |
149 | { | |
150 | return FALSE; | |
151 | } | |
152 | ||
153 | /* should check preop too */ | |
154 | if (inc->kind != XPR_POSTOP) | |
155 | { | |
156 | return FALSE; | |
157 | } | |
158 | ||
159 | tok = (exprData_getUopTok (inc->edata)); | |
160 | if (lltok_isInc_Op (tok) ) | |
161 | { | |
162 | t1 = exprData_getUopNode (test->edata); | |
163 | t2 = exprData_getUopNode (inc->edata); | |
bb7c2085 | 164 | llassert (exprNode_isDefined (t2) && exprNode_isDefined (t2) ); |
d9900876 | 165 | |
bb7c2085 | 166 | if (exprNode_isUndefined (t1) || exprNode_isUndefined (t2) ) |
d9900876 | 167 | { |
168 | return FALSE; | |
169 | } | |
170 | ||
171 | if (sRef_sameName (t1->sref, t2->sref) ) | |
172 | { | |
173 | return TRUE; | |
174 | } | |
175 | } | |
176 | return FALSE; | |
177 | } | |
178 | ||
179 | static /*@only@*/ constraintList getLessThanConstraints (/*@observer@*/ constraintList c) | |
180 | { | |
181 | constraintList ret; | |
182 | ||
bb7c2085 | 183 | ret = constraintList_makeNew (); |
d9900876 | 184 | constraintList_elements (c, el) |
185 | { | |
bb7c2085 | 186 | llassert (constraint_isDefined (el)); |
187 | if ( constraint_isUndefined (el) ) | |
d9900876 | 188 | continue; |
189 | ||
190 | if (el->ar == LT || el->ar == LTE) | |
191 | { | |
192 | constraint temp; | |
bb7c2085 | 193 | temp = constraint_copy (el); |
d9900876 | 194 | |
195 | ret = constraintList_add (ret, temp); | |
196 | } | |
197 | } | |
198 | end_constraintList_elements; | |
199 | ||
200 | return ret; | |
201 | } | |
202 | ||
203 | static /*@only@*/ constraintList getIncConstraints (/*@observer@*/ constraintList c) | |
204 | { | |
205 | constraintList ret; | |
206 | ||
bb7c2085 | 207 | ret = constraintList_makeNew (); |
d9900876 | 208 | constraintList_elements (c, el) |
209 | { | |
210 | llassert (constraint_isDefined (el)); | |
211 | ||
212 | if (incVar (el) ) | |
213 | { | |
214 | constraint temp; | |
bb7c2085 | 215 | temp = constraint_copy (el); |
d9900876 | 216 | ret = constraintList_add (ret, temp); |
217 | } | |
218 | } | |
219 | end_constraintList_elements; | |
220 | ||
221 | return ret; | |
222 | } | |
223 | ||
224 | static /*@only@*/ constraintExpr getForTimes (/*@notnull@*/ exprNode forPred, /*@notnull@*/ exprNode forBody) | |
225 | { | |
226 | ||
227 | exprNode init, test, inc, t1, t2; | |
228 | constraintList ltCon; | |
229 | constraintList incCon; | |
230 | constraintExpr ret; | |
231 | ||
232 | lltok tok; | |
233 | ||
234 | init = exprData_getTripleInit (forPred->edata); | |
235 | test = exprData_getTripleTest (forPred->edata); | |
236 | inc = exprData_getTripleInc (forPred->edata); | |
237 | ||
bb7c2085 | 238 | llassert (exprNode_isDefined (test) ); |
239 | llassert (exprNode_isDefined (inc) ); | |
d9900876 | 240 | |
241 | ltCon = getLessThanConstraints (test->trueEnsuresConstraints); | |
242 | incCon = getIncConstraints (inc->ensuresConstraints); | |
243 | ||
bb7c2085 | 244 | DPRINTF (( message ("getForTimes: ltCon: %s from %s", constraintList_print (ltCon), constraintList_print (test->trueEnsuresConstraints) ) )); |
d9900876 | 245 | |
bb7c2085 | 246 | DPRINTF (( message ("getForTimes: incCon: %s from %s", constraintList_print (incCon), constraintList_print (inc->ensuresConstraints) ) )); |
d9900876 | 247 | |
248 | constraintList_elements (ltCon, el) | |
249 | { | |
bb7c2085 | 250 | constraintList_elements (incCon, el2) |
d9900876 | 251 | { |
bb7c2085 | 252 | if ( increments (el2, el->lexpr) ) |
d9900876 | 253 | { |
bb7c2085 | 254 | DPRINTF (( message ("getForTimes: %s increments %s", constraint_print (el2), constraint_print (el) ) )); |
d9900876 | 255 | ret = constraintExpr_copy (el->expr); |
bb7c2085 | 256 | constraintList_free (ltCon); |
257 | constraintList_free (incCon); | |
d9900876 | 258 | return ret; |
259 | ||
260 | } | |
261 | else | |
393e573f | 262 | { |
263 | ; | |
264 | DPRINTF (( message ("getForTimes: %s doesn't increment %s", constraint_print (el2), constraint_print (el) ) )); | |
265 | } | |
d9900876 | 266 | } |
267 | end_constraintList_elements; | |
268 | } | |
269 | ||
270 | end_constraintList_elements; | |
271 | ||
bb7c2085 | 272 | constraintList_free (ltCon); |
273 | constraintList_free (incCon); | |
d9900876 | 274 | |
bb7c2085 | 275 | DPRINTF (( message ("getForTimes: %s %s resorting to ugly hack", exprNode_unparse (forPred), exprNode_unparse (forBody) ) )); |
d9900876 | 276 | if (! canGetForTimes (forPred, forBody) ) |
277 | { | |
278 | return NULL; | |
279 | } | |
280 | ||
281 | ||
282 | if (test->kind != XPR_PREOP) | |
283 | llassert (FALSE); | |
284 | ||
285 | tok = (exprData_getUopTok (test->edata)); | |
286 | if (!lltok_isMult (tok) ) | |
287 | { | |
288 | llassert ( FALSE ); | |
289 | } | |
290 | ||
291 | /* should check preop too */ | |
292 | if (inc->kind != XPR_POSTOP) | |
293 | { | |
294 | llassert (FALSE ); | |
295 | } | |
296 | ||
297 | tok = (exprData_getUopTok (inc->edata)); | |
298 | if (lltok_isInc_Op (tok) ) | |
299 | { | |
300 | t1 = exprData_getUopNode (test->edata); | |
301 | t2 = exprData_getUopNode (inc->edata); | |
302 | if (sRef_sameName (t1->sref, t2->sref) ) | |
303 | { | |
304 | return (constraintExpr_makeMaxSetExpr (t1) ); | |
305 | } | |
306 | } | |
bb7c2085 | 307 | llassert ( FALSE); |
d9900876 | 308 | BADEXIT; |
309 | } | |
310 | ||
311 | /*@access constraintExpr @*/ | |
312 | ||
313 | static /*@only@*/ constraintExpr constraintExpr_searchAndAdd (/*@only@*/ constraintExpr c, /*@observer@*/ constraintExpr find, /*@observer@*/ constraintExpr add) | |
314 | { | |
315 | constraintExprKind kind; | |
316 | constraintExpr temp; | |
317 | ||
bb7c2085 | 318 | DPRINTF (( message ("Doing constraintExpr_searchAndAdd %s %s %s ", |
319 | constraintExpr_unparse (c), constraintExpr_unparse (find), constraintExpr_unparse (add) ) ) ); | |
d9900876 | 320 | |
321 | if ( constraintExpr_similar (c, find) ) | |
322 | { | |
323 | ||
324 | constraintExpr newExpr; | |
325 | ||
326 | cstring cPrint; | |
327 | ||
bb7c2085 | 328 | cPrint = constraintExpr_unparse (c); |
d9900876 | 329 | |
330 | ||
bb7c2085 | 331 | newExpr = constraintExpr_makeAddExpr (c, constraintExpr_copy (add) ); |
d9900876 | 332 | |
bb7c2085 | 333 | DPRINTF ((message ("Replacing %q with %q", |
334 | cPrint, constraintExpr_unparse (newExpr) | |
d9900876 | 335 | ))); |
336 | return newExpr; | |
337 | } | |
338 | ||
339 | kind = c->kind; | |
340 | ||
341 | switch (kind) | |
342 | { | |
343 | case term: | |
344 | break; | |
345 | case unaryExpr: | |
346 | temp = constraintExprData_unaryExprGetExpr (c->data); | |
bb7c2085 | 347 | temp = constraintExpr_searchAndAdd (constraintExpr_copy (temp), find, add); |
d9900876 | 348 | c->data = constraintExprData_unaryExprSetExpr (c->data, temp); |
349 | break; | |
350 | case binaryexpr: | |
351 | ||
352 | temp = constraintExprData_binaryExprGetExpr1 (c->data); | |
bb7c2085 | 353 | temp = constraintExpr_searchAndAdd (constraintExpr_copy (temp), find, add); |
d9900876 | 354 | c->data = constraintExprData_binaryExprSetExpr1 (c->data, temp); |
355 | ||
356 | temp = constraintExprData_binaryExprGetExpr2 (c->data); | |
bb7c2085 | 357 | temp = constraintExpr_searchAndAdd (constraintExpr_copy (temp), find, add); |
d9900876 | 358 | c->data = constraintExprData_binaryExprSetExpr2 (c->data, temp); |
359 | break; | |
360 | default: | |
bb7c2085 | 361 | llassert (FALSE); |
d9900876 | 362 | } |
363 | return c; | |
364 | ||
365 | } | |
366 | ||
367 | /*@noaccess constraintExpr @*/ | |
368 | ||
369 | static constraint constraint_searchAndAdd (/*@returned@*/ constraint c, /*@observer@*/ constraintExpr find, /*@observer@*/ constraintExpr add) | |
370 | { | |
371 | ||
372 | llassert (constraint_search (c, find) ); | |
bb7c2085 | 373 | DPRINTF (( message ("Doing constraint_searchAndAdd %s %s %s ", |
374 | constraint_print (c), constraintExpr_unparse (find), constraintExpr_unparse (add) ) ) ); | |
d9900876 | 375 | |
376 | c->lexpr = constraintExpr_searchAndAdd (c->lexpr, find, add); | |
377 | c->expr = constraintExpr_searchAndAdd (c->expr, find, add); | |
378 | ||
379 | c = constraint_simplify (c); | |
380 | c = constraint_simplify (c); | |
381 | ||
382 | return c; | |
383 | ||
384 | } | |
385 | ||
386 | static constraintList constraintList_searchAndAdd (/*@returned@*/ constraintList list, | |
387 | /*@observer@*/ constraintExpr find, /*@observer@*/ constraintExpr add) | |
388 | { | |
389 | constraintList newConstraints; | |
390 | constraintList ret; | |
391 | ||
bb7c2085 | 392 | newConstraints = constraintList_makeNew (); |
d9900876 | 393 | |
394 | constraintList_elements (list, el) | |
395 | { | |
396 | if (constraint_search (el, find) ) | |
397 | { | |
398 | constraint newExpr; | |
399 | newExpr = constraint_copy (el); | |
400 | ||
401 | newExpr = constraint_searchAndAdd (newExpr, find, add); | |
402 | DPRINTF (( (message ("Adding constraint %s ", constraint_print (newExpr)) ) )); | |
403 | newConstraints = constraintList_add (newConstraints, newExpr); | |
404 | } | |
405 | ||
406 | } | |
407 | end_constraintList_elements; | |
408 | ||
409 | ret = constraintList_addListFree (list, newConstraints); | |
410 | return ret; | |
411 | } | |
412 | ||
bb7c2085 | 413 | static void doAdjust (/*@unused@*/ exprNode e, /*@unused@*/ exprNode forPred, /*@observer@*/ exprNode forBody, /*@observer@*/ constraintExpr iterations) |
d9900876 | 414 | { |
415 | ||
416 | constraintList_elements (forBody->ensuresConstraints, el) | |
417 | { | |
418 | /* look for var = var + 1 */ | |
bb7c2085 | 419 | if (incVar (el) ) |
d9900876 | 420 | { |
bb7c2085 | 421 | DPRINTF ((message ("Found inc variable constraint : %s", constraint_print (el) ) )); |
422 | forBody->requiresConstraints = constraintList_searchAndAdd (forBody->requiresConstraints, el->lexpr, iterations); | |
d9900876 | 423 | } |
424 | } | |
425 | end_constraintList_elements; | |
426 | } | |
427 | ||
bb7c2085 | 428 | void exprNode_forLoopHeuristics ( exprNode e, exprNode forPred, exprNode forBody) |
d9900876 | 429 | { |
430 | exprNode init, test, inc; | |
431 | ||
432 | constraintExpr iterations; | |
433 | ||
434 | init = exprData_getTripleInit (forPred->edata); | |
435 | test = exprData_getTripleTest (forPred->edata); | |
436 | inc = exprData_getTripleInc (forPred->edata); | |
437 | ||
438 | if (exprNode_isError (test) || exprNode_isError (inc) ) | |
439 | return; | |
440 | ||
441 | iterations = getForTimes (forPred, forBody ); | |
442 | ||
443 | if (constraintExpr_isDefined (iterations) ) | |
444 | { | |
445 | doAdjust ( e, forPred, forBody, iterations); | |
bb7c2085 | 446 | constraintExpr_free (iterations); |
d9900876 | 447 | } |
448 | } | |
449 | ||
450 | ||
451 | /* else */ | |
452 | /* { */ | |
453 | /* DPRINTF (("Can't get for time ")); */ | |
454 | /* } */ | |
455 | ||
bb7c2085 | 456 | /* if (exprNode_isError (init) ) */ |
d9900876 | 457 | /* { */ |
458 | /* return; */ | |
459 | /* } */ | |
460 | ||
461 | /* if (init->kind == XPR_ASSIGN) */ | |
462 | /* { */ | |
463 | /* t1 = exprData_getOpA (init->edata); */ | |
464 | /* t2 = exprData_getOpB (init->edata); */ | |
465 | ||
466 | /* if (! (t1->kind == XPR_VAR) ) */ | |
467 | /* return; */ | |
468 | /* } */ | |
469 | /* else */ | |
470 | /* return; */ | |
471 | ||
472 | /* if (test->kind == XPR_FETCH) */ | |
473 | /* { */ | |
474 | /* t3 = exprData_getPairA (test->edata); */ | |
475 | /* t4 = exprData_getPairB (test->edata); */ | |
476 | ||
bb7c2085 | 477 | /* if (sRef_sameName (t1->sref, t4->sref) ) */ |
d9900876 | 478 | /* { */ |
bb7c2085 | 479 | /* DPRINTF ((message ("Found a for loop matching heuristic:%s", exprNode_unparse (forPred) ) )); */ |
480 | /* con = constraint_makeEnsureLteMaxRead (t1, t3); */ | |
481 | /* forPred->ensuresConstraints = constraintList_add (forPred->ensuresConstraints, con); */ | |
d9900876 | 482 | /* } */ |
483 | /* else */ | |
484 | /* { */ | |
bb7c2085 | 485 | /* 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 | 486 | /* } */ |
487 | /* return; */ | |
488 | /* } */ |