2 ** Splint - annotation-assisted static program checker
3 ** Copyright (C) 1994-2003 University of Virginia,
4 ** Massachusetts Institute of Technology
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.
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.
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.
20 ** For information on splint: info@splint.org
21 ** To report a bug: splint-bug@splint.org
22 ** For more information: http://www.splint.org
29 /*This file was formerly called forjunk.c C
30 renamed Oct 8, 2001 - DRL
33 /* #define DEBUGPRINT 1 */
35 # include <ctype.h> /* for isdigit */
36 # include "splintMacros.nf"
38 # include "cgrammar.h"
39 # include "cgrammar_tokens.h"
41 # include "exprChecks.h"
42 # include "exprNodeSList.h"
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.
49 /*@access constraint @*/
51 static bool isInc (/*@observer@*/ constraintExpr p_c) /*@*/;
52 static bool incVar (/*@notnull@*/ constraint p_c) /*@*/;
55 static bool increments (/*@observer@*/ constraint c,
56 /*@observer@*/ constraintExpr var)
58 llassert (constraint_isDefined (c) );
60 if (constraint_isUndefined (c) )
65 llassert (incVar (c));
66 if (constraintExpr_similar (c->lexpr, var) )
72 static /*@only@*/ constraintList getLessThanConstraints (/*@observer@*/ constraintList c)
76 ret = constraintList_makeNew ();
77 constraintList_elements (c, el)
79 llassert (constraint_isDefined (el));
80 if ( constraint_isUndefined (el) )
83 if (el->ar == LT || el->ar == LTE)
86 temp = constraint_copy (el);
88 ret = constraintList_add (ret, temp);
91 end_constraintList_elements;
96 static /*@only@*/ constraintList getIncConstraints (/*@observer@*/ constraintList c)
100 ret = constraintList_makeNew ();
101 constraintList_elements (c, el)
103 llassert (constraint_isDefined (el));
108 temp = constraint_copy (el);
109 ret = constraintList_add (ret, temp);
112 end_constraintList_elements;
117 /*@access exprNode@*/
118 static bool canGetForTimes (/*@notnull@*/ exprNode forPred, /*@notnull@*/ exprNode forBody)
121 exprNode init, test, inc, t1, t2;
124 llassert (exprNode_isDefined (forPred) );
125 llassert (exprNode_isDefined (forBody) );
127 init = exprData_getTripleInit (forPred->edata);
128 test = exprData_getTripleTest (forPred->edata);
129 inc = exprData_getTripleInc (forPred->edata);
131 llassert (exprNode_isDefined (test) );
133 if (exprNode_isUndefined (test) )
138 llassert (exprNode_isDefined (inc) );
140 if (exprNode_isUndefined (inc) )
145 if (test->kind != XPR_PREOP)
148 tok = (exprData_getUopTok (test->edata));
149 if (!lltok_isMult (tok) )
154 /* should check preop too */
155 if (inc->kind != XPR_POSTOP)
160 tok = (exprData_getUopTok (inc->edata));
161 if (lltok_isIncOp (tok) )
163 t1 = exprData_getUopNode (test->edata);
164 t2 = exprData_getUopNode (inc->edata);
165 llassert (exprNode_isDefined (t2) && exprNode_isDefined (t2) );
167 if (exprNode_isUndefined (t1) || exprNode_isUndefined (t2) )
172 if (sRef_sameName (t1->sref, t2->sref) )
179 /*@noaccess exprNode@*/
182 /*@access exprNode@*/
183 static /*@only@*/ constraintExpr getForTimes (/*@notnull@*/ exprNode forPred, /*@notnull@*/ exprNode forBody)
186 exprNode init, test, inc, t1, t2;
187 constraintList ltCon;
188 constraintList incCon;
193 init = exprData_getTripleInit (forPred->edata);
194 test = exprData_getTripleTest (forPred->edata);
195 inc = exprData_getTripleInc (forPred->edata);
197 llassert (exprNode_isDefined (test) );
198 llassert (exprNode_isDefined (inc) );
200 ltCon = getLessThanConstraints (test->trueEnsuresConstraints);
201 incCon = getIncConstraints (inc->ensuresConstraints);
203 DPRINTF (( message ("getForTimes: ltCon: %s from %s", constraintList_print (ltCon), constraintList_print (test->trueEnsuresConstraints) ) ));
205 DPRINTF (( message ("getForTimes: incCon: %s from %s", constraintList_print (incCon), constraintList_print (inc->ensuresConstraints) ) ));
207 constraintList_elements (ltCon, el)
209 constraintList_elements (incCon, el2)
211 llassert(constraint_isDefined (el ) );
213 if ( (constraint_isDefined (el ) ) && ( increments (el2, el->lexpr) ) )
215 DPRINTF (( message ("getForTimes: %s increments %s", constraint_print (el2), constraint_print (el) ) ));
216 ret = constraintExpr_copy (el->expr);
217 constraintList_free (ltCon);
218 constraintList_free (incCon);
225 DPRINTF (( message ("getForTimes: %s doesn't increment %s", constraint_print (el2), constraint_print (el) ) ));
228 end_constraintList_elements;
231 end_constraintList_elements;
233 constraintList_free (ltCon);
234 constraintList_free (incCon);
236 DPRINTF (( message ("getForTimes: %s %s resorting to ugly hack", exprNode_unparse (forPred), exprNode_unparse (forBody) ) ));
237 if (! canGetForTimes (forPred, forBody) )
243 if (test->kind != XPR_PREOP)
246 tok = (exprData_getUopTok (test->edata));
247 if (!lltok_isMult (tok) )
252 /* should check preop too */
253 if (inc->kind != XPR_POSTOP)
258 tok = (exprData_getUopTok (inc->edata));
259 if (lltok_isIncOp (tok) )
261 t1 = exprData_getUopNode (test->edata);
262 t2 = exprData_getUopNode (inc->edata);
264 llassert(exprNode_isDefined(t1) && exprNode_isDefined(t2) );
265 if (sRef_sameName (t1->sref, t2->sref) )
267 return (constraintExpr_makeMaxSetExpr (t1) );
273 /*@noaccess exprNode@*/
275 /*@access constraintExpr @*/
277 static /*@only@*/ constraintExpr constraintExpr_searchAndAdd (/*@only@*/ constraintExpr c, /*@observer@*/ constraintExpr find, /*@observer@*/ constraintExpr add)
279 constraintExprKind kind;
283 llassert (constraintExpr_isDefined (c) );
285 DPRINTF (( message ("Doing constraintExpr_searchAndAdd %s %s %s ",
286 constraintExpr_unparse (c), constraintExpr_unparse (find), constraintExpr_unparse (add) ) ) );
288 if ( constraintExpr_similar (c, find) )
291 constraintExpr newExpr;
295 cPrint = constraintExpr_unparse (c);
298 newExpr = constraintExpr_makeAddExpr (c, constraintExpr_copy (add) );
300 DPRINTF ((message ("Replacing %q with %q",
301 cPrint, constraintExpr_unparse (newExpr)
313 temp = constraintExprData_unaryExprGetExpr (c->data);
314 temp = constraintExpr_searchAndAdd (constraintExpr_copy (temp), find, add);
315 c->data = constraintExprData_unaryExprSetExpr (c->data, temp);
319 temp = constraintExprData_binaryExprGetExpr1 (c->data);
320 temp = constraintExpr_searchAndAdd (constraintExpr_copy (temp), find, add);
321 c->data = constraintExprData_binaryExprSetExpr1 (c->data, temp);
323 temp = constraintExprData_binaryExprGetExpr2 (c->data);
324 temp = constraintExpr_searchAndAdd (constraintExpr_copy (temp), find, add);
325 c->data = constraintExprData_binaryExprSetExpr2 (c->data, temp);
334 /*@noaccess constraintExpr @*/
336 static constraint constraint_searchAndAdd (/*@returned@*/ constraint c, /*@observer@*/ constraintExpr find, /*@observer@*/ constraintExpr add)
340 llassert (constraint_isDefined (c) );
342 llassert (constraint_search (c, find) );
343 DPRINTF (( message ("Doing constraint_searchAndAdd %s %s %s ",
344 constraint_print (c), constraintExpr_unparse (find), constraintExpr_unparse (add) ) ) );
346 c->lexpr = constraintExpr_searchAndAdd (c->lexpr, find, add);
347 c->expr = constraintExpr_searchAndAdd (c->expr, find, add);
349 c = constraint_simplify (c);
350 c = constraint_simplify (c);
356 static constraintList constraintList_searchAndAdd (/*@returned@*/ constraintList list,
357 /*@observer@*/ constraintExpr find, /*@observer@*/ constraintExpr add)
359 constraintList newConstraints;
362 newConstraints = constraintList_makeNew ();
364 constraintList_elements (list, el)
366 if (constraint_search (el, find) )
369 newExpr = constraint_copy (el);
371 newExpr = constraint_searchAndAdd (newExpr, find, add);
372 DPRINTF (( (message ("Adding constraint %s ", constraint_print (newExpr)) ) ));
373 newConstraints = constraintList_add (newConstraints, newExpr);
377 end_constraintList_elements;
379 ret = constraintList_addListFree (list, newConstraints);
383 /*@access exprNode@*/
384 static void doAdjust (/*@unused@*/ exprNode e, /*@unused@*/ exprNode forPred, /*@observer@*/ exprNode forBody, /*@observer@*/ constraintExpr iterations)
387 llassert (exprNode_isDefined (forBody) );
389 constraintList_elements (forBody->ensuresConstraints, el)
391 /* look for var = var + 1 */
392 if (constraint_isDefined (el) && incVar (el) )
394 DPRINTF ((message ("Found inc variable constraint : %s", constraint_print (el) ) ));
395 forBody->requiresConstraints = constraintList_searchAndAdd (forBody->requiresConstraints, el->lexpr, iterations);
398 end_constraintList_elements;
402 /*@access exprNode@*/
405 static void forLoopHeuristicsImpl ( exprNode e, exprNode forPred, /*@observer@*/ exprNode forBody)
407 exprNode init, test, inc;
409 constraintExpr iterations;
411 llassert (exprNode_isDefined(forPred) );
412 llassert (exprNode_isDefined(forBody) );
414 init = exprData_getTripleInit (forPred->edata);
415 test = exprData_getTripleTest (forPred->edata);
416 inc = exprData_getTripleInc (forPred->edata);
418 if (exprNode_isError (test) || exprNode_isError (inc) )
421 iterations = getForTimes (forPred, forBody );
423 if (constraintExpr_isDefined (iterations) )
425 doAdjust ( e, forPred, forBody, iterations);
426 constraintExpr_free (iterations);
429 /*@noaccess exprNode@*/
431 void exprNode_forLoopHeuristics ( exprNode e, exprNode forPred, exprNode forBody)
433 forLoopHeuristicsImpl (e, forPred, forBody);
436 /*@access constraintExpr @*/
438 static bool isInc (/*@observer@*/ constraintExpr c) /*@*/
441 llassert (constraintExpr_isDefined (c) );
442 if (c->kind == binaryexpr )
444 constraintExprBinaryOpKind binOP;
445 constraintExpr t1, t2;
446 t1 = constraintExprData_binaryExprGetExpr1 (c->data);
447 t2 = constraintExprData_binaryExprGetExpr2 (c->data);
449 binOP = constraintExprData_binaryExprGetOp (c->data);
450 if (binOP == BINARYOP_PLUS)
451 if (constraintExpr_isLit (t2) && constraintExpr_getValue (t2) == 1 )
459 /*@noaccess constraintExpr @*/
461 /*@access constraintExpr @*/
462 /* look for constraints like cexrp = cexrp + 1 */
463 static bool incVar (/*@notnull@*/ constraint c) /*@*/
470 if (! isInc (c->expr ) )
473 llassert (constraintExpr_isDefined (c->expr) );
474 llassert (c->expr->kind == binaryexpr);
476 t1 = constraintExprData_binaryExprGetExpr1 (c->expr->data);
477 if (constraintExpr_similar (c->lexpr, t1) )
482 /*@noaccess constraintExpr @*/
489 /* DPRINTF (("Can't get for time ")); */
492 /* if (exprNode_isError (init) ) */
497 /* if (init->kind == XPR_ASSIGN) */
499 /* t1 = exprData_getOpA (init->edata); */
500 /* t2 = exprData_getOpB (init->edata); */
502 /* if (! (t1->kind == XPR_VAR) ) */
508 /* if (test->kind == XPR_FETCH) */
510 /* t3 = exprData_getPairA (test->edata); */
511 /* t4 = exprData_getPairB (test->edata); */
513 /* if (sRef_sameName (t1->sref, t4->sref) ) */
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); */
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) ) )); */