2 ** Splint - annotation-assisted static program checker
3 ** Copyright (C) 1994-2001 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 lclint: lclint-request@cs.virginia.edu
21 ** To report a bug: lclint-bug@cs.virginia.edu
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 "lclintMacros.nf"
38 # include "cgrammar.h"
39 # include "cgrammar_tokens.h"
41 # include "exprChecks.h"
42 # include "exprNodeSList.h"
44 # include "exprDataQuite.i"
46 /*@access constraint, exprNode @*/
48 /*@access constraintExpr @*/
50 static bool isInc (/*@observer@*/ constraintExpr c) /*@*/
53 llassert(constraintExpr_isDefined(c) );
54 if (c->kind == binaryexpr )
56 constraintExprBinaryOpKind binOP;
57 constraintExpr t1, t2;
58 t1 = constraintExprData_binaryExprGetExpr1 (c->data);
59 t2 = constraintExprData_binaryExprGetExpr2 (c->data);
61 binOP = constraintExprData_binaryExprGetOp (c->data);
62 if (binOP == BINARYOP_PLUS)
63 if (constraintExpr_isLit (t2) && constraintExpr_getValue (t2) == 1 )
72 /* look for constraints like cexrp = cexrp + 1 */
73 static bool incVar (/*@notnull@*/ constraint c) /*@*/
80 if (! isInc (c->expr ) )
83 llassert (constraintExpr_isDefined(c->expr) );
84 llassert (c->expr->kind == binaryexpr);
86 t1 = constraintExprData_binaryExprGetExpr1 (c->expr->data);
87 if (constraintExpr_similar (c->lexpr, t1) )
92 /*@noaccess constraintExpr @*/
95 static bool increments (/*@observer@*/ constraint c,
96 /*@observer@*/ constraintExpr var)
98 llassert(constraint_isDefined(c) );
100 if (constraint_isUndefined(c) )
105 llassert (incVar (c));
106 if (constraintExpr_similar (c->lexpr, var) )
112 static bool canGetForTimes (/*@notnull@*/ exprNode forPred, /*@notnull@*/ exprNode forBody)
115 exprNode init, test, inc, t1, t2;
118 llassert(exprNode_isDefined (forPred) );
119 llassert(exprNode_isDefined (forBody) );
121 init = exprData_getTripleInit (forPred->edata);
122 test = exprData_getTripleTest (forPred->edata);
123 inc = exprData_getTripleInc (forPred->edata);
125 llassert(exprNode_isDefined(test) );
127 if (exprNode_isUndefined(test) )
132 llassert(exprNode_isDefined(inc) );
134 if (exprNode_isUndefined(inc) )
139 if (test->kind != XPR_PREOP)
142 tok = (exprData_getUopTok (test->edata));
143 if (!lltok_isMult (tok) )
148 /* should check preop too */
149 if (inc->kind != XPR_POSTOP)
154 tok = (exprData_getUopTok (inc->edata));
155 if (lltok_isInc_Op (tok) )
157 t1 = exprData_getUopNode (test->edata);
158 t2 = exprData_getUopNode (inc->edata);
159 llassert(exprNode_isDefined(t2) && exprNode_isDefined(t2) );
161 if (exprNode_isUndefined(t1) || exprNode_isUndefined(t2) )
166 if (sRef_sameName (t1->sref, t2->sref) )
174 static /*@only@*/ constraintList getLessThanConstraints (/*@observer@*/ constraintList c)
178 ret = constraintList_makeNew();
179 constraintList_elements (c, el)
181 llassert(constraint_isDefined(el));
182 if ( constraint_isUndefined(el) )
185 if (el->ar == LT || el->ar == LTE)
188 temp = constraint_copy(el);
190 ret = constraintList_add (ret, temp);
193 end_constraintList_elements;
198 static /*@only@*/ constraintList getIncConstraints (/*@observer@*/ constraintList c)
202 ret = constraintList_makeNew();
203 constraintList_elements (c, el)
205 llassert (constraint_isDefined (el));
210 temp = constraint_copy(el);
211 ret = constraintList_add (ret, temp);
214 end_constraintList_elements;
219 static /*@only@*/ constraintExpr getForTimes (/*@notnull@*/ exprNode forPred, /*@notnull@*/ exprNode forBody)
222 exprNode init, test, inc, t1, t2;
223 constraintList ltCon;
224 constraintList incCon;
229 init = exprData_getTripleInit (forPred->edata);
230 test = exprData_getTripleTest (forPred->edata);
231 inc = exprData_getTripleInc (forPred->edata);
233 llassert(exprNode_isDefined(test) );
234 llassert(exprNode_isDefined(inc) );
236 ltCon = getLessThanConstraints (test->trueEnsuresConstraints);
237 incCon = getIncConstraints (inc->ensuresConstraints);
239 DPRINTF(( message ("getForTimes: ltCon: %s from %s", constraintList_print(ltCon), constraintList_print(test->trueEnsuresConstraints) ) ));
241 DPRINTF(( message ("getForTimes: incCon: %s from %s", constraintList_print(incCon), constraintList_print(inc->ensuresConstraints) ) ));
243 constraintList_elements (ltCon, el)
245 constraintList_elements(incCon, el2)
247 if ( increments(el2, el->lexpr) )
249 DPRINTF(( message ("getForTimes: %s increments %s", constraint_print(el2), constraint_print(el) ) ));
250 ret = constraintExpr_copy (el->expr);
251 constraintList_free(ltCon);
252 constraintList_free(incCon);
257 DPRINTF(( message ("getForTimes: %s doesn't increment %s", constraint_print(el2), constraint_print(el) ) ));
259 end_constraintList_elements;
262 end_constraintList_elements;
264 constraintList_free(ltCon);
265 constraintList_free(incCon);
267 DPRINTF (( message ("getForTimes: %s %s resorting to ugly hack", exprNode_unparse(forPred), exprNode_unparse(forBody) ) ));
268 if (! canGetForTimes (forPred, forBody) )
274 if (test->kind != XPR_PREOP)
277 tok = (exprData_getUopTok (test->edata));
278 if (!lltok_isMult (tok) )
283 /* should check preop too */
284 if (inc->kind != XPR_POSTOP)
289 tok = (exprData_getUopTok (inc->edata));
290 if (lltok_isInc_Op (tok) )
292 t1 = exprData_getUopNode (test->edata);
293 t2 = exprData_getUopNode (inc->edata);
294 if (sRef_sameName (t1->sref, t2->sref) )
296 return (constraintExpr_makeMaxSetExpr (t1) );
303 /*@access constraintExpr @*/
305 static /*@only@*/ constraintExpr constraintExpr_searchAndAdd (/*@only@*/ constraintExpr c, /*@observer@*/ constraintExpr find, /*@observer@*/ constraintExpr add)
307 constraintExprKind kind;
310 DPRINTF(( message ("Doing constraintExpr_searchAndAdd %s %s %s ",
311 constraintExpr_unparse(c), constraintExpr_unparse(find), constraintExpr_unparse(add) ) ) );
313 if ( constraintExpr_similar (c, find) )
316 constraintExpr newExpr;
320 cPrint = constraintExpr_unparse(c);
323 newExpr = constraintExpr_makeAddExpr (c, constraintExpr_copy(add) );
325 DPRINTF((message ("Replacing %q with %q",
326 cPrint, constraintExpr_unparse(newExpr)
338 temp = constraintExprData_unaryExprGetExpr (c->data);
339 temp = constraintExpr_searchAndAdd (constraintExpr_copy(temp), find, add);
340 c->data = constraintExprData_unaryExprSetExpr (c->data, temp);
344 temp = constraintExprData_binaryExprGetExpr1 (c->data);
345 temp = constraintExpr_searchAndAdd (constraintExpr_copy(temp), find, add);
346 c->data = constraintExprData_binaryExprSetExpr1 (c->data, temp);
348 temp = constraintExprData_binaryExprGetExpr2 (c->data);
349 temp = constraintExpr_searchAndAdd (constraintExpr_copy(temp), find, add);
350 c->data = constraintExprData_binaryExprSetExpr2 (c->data, temp);
359 /*@noaccess constraintExpr @*/
361 static constraint constraint_searchAndAdd (/*@returned@*/ constraint c, /*@observer@*/ constraintExpr find, /*@observer@*/ constraintExpr add)
364 llassert (constraint_search (c, find) );
365 DPRINTF(( message ("Doing constraint_searchAndAdd %s %s %s ",
366 constraint_print(c), constraintExpr_unparse(find), constraintExpr_unparse(add) ) ) );
368 c->lexpr = constraintExpr_searchAndAdd (c->lexpr, find, add);
369 c->expr = constraintExpr_searchAndAdd (c->expr, find, add);
371 c = constraint_simplify (c);
372 c = constraint_simplify (c);
378 static constraintList constraintList_searchAndAdd (/*@returned@*/ constraintList list,
379 /*@observer@*/ constraintExpr find, /*@observer@*/ constraintExpr add)
381 constraintList newConstraints;
384 newConstraints = constraintList_makeNew();
386 constraintList_elements (list, el)
388 if (constraint_search (el, find) )
391 newExpr = constraint_copy (el);
393 newExpr = constraint_searchAndAdd (newExpr, find, add);
394 DPRINTF (( (message ("Adding constraint %s ", constraint_print (newExpr)) ) ));
395 newConstraints = constraintList_add (newConstraints, newExpr);
399 end_constraintList_elements;
401 ret = constraintList_addListFree (list, newConstraints);
405 static void doAdjust(/*@unused@*/ exprNode e, /*@unused@*/ exprNode forPred, /*@observer@*/ exprNode forBody, /*@observer@*/ constraintExpr iterations)
408 constraintList_elements (forBody->ensuresConstraints, el)
410 /* look for var = var + 1 */
413 DPRINTF((message ("Found inc variable constraint : %s", constraint_print (el) ) ));
414 forBody->requiresConstraints = constraintList_searchAndAdd(forBody->requiresConstraints, el->lexpr, iterations);
417 end_constraintList_elements;
420 void exprNode_forLoopHeuristics( exprNode e, exprNode forPred, exprNode forBody)
422 exprNode init, test, inc;
424 constraintExpr iterations;
426 init = exprData_getTripleInit (forPred->edata);
427 test = exprData_getTripleTest (forPred->edata);
428 inc = exprData_getTripleInc (forPred->edata);
430 if (exprNode_isError (test) || exprNode_isError (inc) )
433 iterations = getForTimes (forPred, forBody );
435 if (constraintExpr_isDefined (iterations) )
437 doAdjust ( e, forPred, forBody, iterations);
438 constraintExpr_free(iterations);
445 /* DPRINTF (("Can't get for time ")); */
448 /* if (exprNode_isError(init) ) */
453 /* if (init->kind == XPR_ASSIGN) */
455 /* t1 = exprData_getOpA (init->edata); */
456 /* t2 = exprData_getOpB (init->edata); */
458 /* if (! (t1->kind == XPR_VAR) ) */
464 /* if (test->kind == XPR_FETCH) */
466 /* t3 = exprData_getPairA (test->edata); */
467 /* t4 = exprData_getPairB (test->edata); */
469 /* if (sRef_sameName(t1->sref, t4->sref) ) */
471 /* DPRINTF((message ("Found a for loop matching heuristic:%s", exprNode_unparse (forPred) ) )); */
472 /* con = constraint_makeEnsureLteMaxRead(t1, t3); */
473 /* forPred->ensuresConstraints = constraintList_add(forPred->ensuresConstraints, con); */
477 /* DPRINTF((message ("Didn't Find a for loop matching heuristic:%s %s and %s differ", exprNode_unparse (forPred), exprNode_unparse(t1), exprNode_unparse(t3) ) )); */