/*
-** LCLint - annotation-assisted static program checker
-** Copyright (C) 1994-2001 University of Virginia,
+** Splint - annotation-assisted static program checker
+** Copyright (C) 1994-2003 University of Virginia,
** Massachusetts Institute of Technology
**
** This program is free software; you can redistribute it and/or modify it
** the Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston,
** MA 02111-1307, USA.
**
-** For information on lclint: lclint-request@cs.virginia.edu
-** To report a bug: lclint-bug@cs.virginia.edu
-** For more information: http://lclint.cs.virginia.edu
+** For information on splint: info@splint.org
+** To report a bug: splint-bug@splint.org
+** For more information: http://www.splint.org
*/
/*
/* #define DEBUGPRINT 1 */
# include <ctype.h> /* for isdigit */
-# include "lclintMacros.nf"
+# include "splintMacros.nf"
# include "basic.h"
# include "cgrammar.h"
# include "cgrammar_tokens.h"
# include "exprChecks.h"
# include "exprNodeSList.h"
-# include "exprDataQuite.i"
+/* this file was created to split the loop heuristics functionality out of constraintGeneration.c and constraint.c*/
+/*We need to access the internal representation of constraint
+ see above for an explanation.
+*/
-/*@access constraint, exprNode @*/
+/*@access constraint @*/
-/*@access constraintExpr @*/
+static bool isInc (/*@observer@*/ constraintExpr p_c) /*@*/;
+static bool incVar (/*@notnull@*/ constraint p_c) /*@*/;
-static bool isInc (/*@observer@*/ constraintExpr c) /*@*/
+
+static bool increments (/*@observer@*/ constraint c,
+ /*@observer@*/ constraintExpr var)
{
-
- llassert(constraintExpr_isDefined(c) );
- if (c->kind == binaryexpr )
- {
- constraintExprBinaryOpKind binOP;
- constraintExpr t1, t2;
- t1 = constraintExprData_binaryExprGetExpr1 (c->data);
- t2 = constraintExprData_binaryExprGetExpr2 (c->data);
+ llassert (constraint_isDefined (c) );
- binOP = constraintExprData_binaryExprGetOp (c->data);
- if (binOP == BINARYOP_PLUS)
- if (constraintExpr_isLit (t2) && constraintExpr_getValue (t2) == 1 )
- {
- return TRUE;
- }
+ if (constraint_isUndefined (c) )
+ {
+ return FALSE;
}
- return FALSE;
+ llassert (incVar (c));
+ if (constraintExpr_similar (c->lexpr, var) )
+ return TRUE;
+ else
+ return FALSE;
}
-/* look for constraints like cexrp = cexrp + 1 */
-static bool incVar (/*@notnull@*/ constraint c) /*@*/
+static /*@only@*/ constraintList getLessThanConstraints (/*@observer@*/ constraintList c)
{
- constraintExpr t1;
- if (c->ar != EQ)
- {
- return FALSE;
- }
- if (! isInc (c->expr ) )
- return FALSE;
+ constraintList ret;
- llassert (constraintExpr_isDefined(c->expr) );
- llassert (c->expr->kind == binaryexpr);
+ ret = constraintList_makeNew ();
+ constraintList_elements (c, el)
+ {
+ llassert (constraint_isDefined (el));
+ if ( constraint_isUndefined (el) )
+ continue;
+
+ if (el->ar == LT || el->ar == LTE)
+ {
+ constraint temp;
+ temp = constraint_copy (el);
- t1 = constraintExprData_binaryExprGetExpr1 (c->expr->data);
- if (constraintExpr_similar (c->lexpr, t1) )
- return TRUE;
+ ret = constraintList_add (ret, temp);
+ }
+ }
+ end_constraintList_elements;
- return FALSE;
+ return ret;
}
-/*@noaccess constraintExpr @*/
-
-static bool increments (/*@observer@*/ constraint c,
- /*@observer@*/ constraintExpr var)
+static /*@only@*/ constraintList getIncConstraints (/*@observer@*/ constraintList c)
{
- llassert(constraint_isDefined(c) );
+ constraintList ret;
- if (constraint_isUndefined(c) )
+ ret = constraintList_makeNew ();
+ constraintList_elements (c, el)
{
- return FALSE;
- }
+ llassert (constraint_isDefined (el));
- llassert (incVar (c));
- if (constraintExpr_similar (c->lexpr, var) )
- return TRUE;
- else
- return FALSE;
+ if (incVar (el) )
+ {
+ constraint temp;
+ temp = constraint_copy (el);
+ ret = constraintList_add (ret, temp);
+ }
+ }
+ end_constraintList_elements;
+
+ return ret;
}
+/*@access exprNode@*/
static bool canGetForTimes (/*@notnull@*/ exprNode forPred, /*@notnull@*/ exprNode forBody)
{
exprNode init, test, inc, t1, t2;
lltok tok;
- llassert(exprNode_isDefined (forPred) );
- llassert(exprNode_isDefined (forBody) );
+ llassert (exprNode_isDefined (forPred) );
+ llassert (exprNode_isDefined (forBody) );
init = exprData_getTripleInit (forPred->edata);
test = exprData_getTripleTest (forPred->edata);
inc = exprData_getTripleInc (forPred->edata);
- llassert(exprNode_isDefined(test) );
+ llassert (exprNode_isDefined (test) );
- if (exprNode_isUndefined(test) )
+ if (exprNode_isUndefined (test) )
{
return FALSE;
}
- llassert(exprNode_isDefined(inc) );
+ llassert (exprNode_isDefined (inc) );
- if (exprNode_isUndefined(inc) )
+ if (exprNode_isUndefined (inc) )
{
return FALSE;
}
}
tok = (exprData_getUopTok (inc->edata));
- if (lltok_isInc_Op (tok) )
+ if (lltok_isIncOp (tok) )
{
t1 = exprData_getUopNode (test->edata);
t2 = exprData_getUopNode (inc->edata);
- llassert(exprNode_isDefined(t2) && exprNode_isDefined(t2) );
+ llassert (exprNode_isDefined (t2) && exprNode_isDefined (t2) );
- if (exprNode_isUndefined(t1) || exprNode_isUndefined(t2) )
+ if (exprNode_isUndefined (t1) || exprNode_isUndefined (t2) )
{
return FALSE;
}
}
return FALSE;
}
+/*@noaccess exprNode@*/
-static /*@only@*/ constraintList getLessThanConstraints (/*@observer@*/ constraintList c)
-{
- constraintList ret;
-
- ret = constraintList_makeNew();
- constraintList_elements (c, el)
- {
- llassert(constraint_isDefined(el));
- if ( constraint_isUndefined(el) )
- continue;
-
- if (el->ar == LT || el->ar == LTE)
- {
- constraint temp;
- temp = constraint_copy(el);
-
- ret = constraintList_add (ret, temp);
- }
- }
- end_constraintList_elements;
-
- return ret;
-}
-
-static /*@only@*/ constraintList getIncConstraints (/*@observer@*/ constraintList c)
-{
- constraintList ret;
-
- ret = constraintList_makeNew();
- constraintList_elements (c, el)
- {
- llassert (constraint_isDefined (el));
-
- if (incVar (el) )
- {
- constraint temp;
- temp = constraint_copy(el);
- ret = constraintList_add (ret, temp);
- }
- }
- end_constraintList_elements;
-
- return ret;
-}
+/*@access exprNode@*/
static /*@only@*/ constraintExpr getForTimes (/*@notnull@*/ exprNode forPred, /*@notnull@*/ exprNode forBody)
{
test = exprData_getTripleTest (forPred->edata);
inc = exprData_getTripleInc (forPred->edata);
- llassert(exprNode_isDefined(test) );
- llassert(exprNode_isDefined(inc) );
+ llassert (exprNode_isDefined (test) );
+ llassert (exprNode_isDefined (inc) );
ltCon = getLessThanConstraints (test->trueEnsuresConstraints);
incCon = getIncConstraints (inc->ensuresConstraints);
- DPRINTF(( message ("getForTimes: ltCon: %s from %s", constraintList_print(ltCon), constraintList_print(test->trueEnsuresConstraints) ) ));
+ DPRINTF (( message ("getForTimes: ltCon: %s from %s", constraintList_unparse (ltCon), constraintList_unparse (test->trueEnsuresConstraints) ) ));
- DPRINTF(( message ("getForTimes: incCon: %s from %s", constraintList_print(incCon), constraintList_print(inc->ensuresConstraints) ) ));
+ DPRINTF (( message ("getForTimes: incCon: %s from %s", constraintList_unparse (incCon), constraintList_unparse (inc->ensuresConstraints) ) ));
constraintList_elements (ltCon, el)
{
- constraintList_elements(incCon, el2)
+ constraintList_elements (incCon, el2)
{
- if ( increments(el2, el->lexpr) )
+ llassert(constraint_isDefined (el ) );
+
+ if ( (constraint_isDefined (el ) ) && ( increments (el2, el->lexpr) ) )
{
- DPRINTF(( message ("getForTimes: %s increments %s", constraint_print(el2), constraint_print(el) ) ));
+ DPRINTF (( message ("getForTimes: %s increments %s", constraint_print (el2), constraint_print (el) ) ));
ret = constraintExpr_copy (el->expr);
- constraintList_free(ltCon);
- constraintList_free(incCon);
+ constraintList_free (ltCon);
+ constraintList_free (incCon);
return ret;
}
else
- DPRINTF(( message ("getForTimes: %s doesn't increment %s", constraint_print(el2), constraint_print(el) ) ));
+ {
+ ;
+ DPRINTF (( message ("getForTimes: %s doesn't increment %s", constraint_print (el2), constraint_print (el) ) ));
+ }
}
end_constraintList_elements;
}
end_constraintList_elements;
- constraintList_free(ltCon);
- constraintList_free(incCon);
+ constraintList_free (ltCon);
+ constraintList_free (incCon);
- DPRINTF (( message ("getForTimes: %s %s resorting to ugly hack", exprNode_unparse(forPred), exprNode_unparse(forBody) ) ));
+ DPRINTF (( message ("getForTimes: %s %s resorting to ugly hack", exprNode_unparse (forPred), exprNode_unparse (forBody) ) ));
if (! canGetForTimes (forPred, forBody) )
{
return NULL;
}
tok = (exprData_getUopTok (inc->edata));
- if (lltok_isInc_Op (tok) )
+ if (lltok_isIncOp (tok) )
{
t1 = exprData_getUopNode (test->edata);
t2 = exprData_getUopNode (inc->edata);
+
+ llassert(exprNode_isDefined(t1) && exprNode_isDefined(t2) );
if (sRef_sameName (t1->sref, t2->sref) )
{
return (constraintExpr_makeMaxSetExpr (t1) );
}
}
- llassert( FALSE);
+ llassert ( FALSE);
BADEXIT;
}
+/*@noaccess exprNode@*/
/*@access constraintExpr @*/
constraintExprKind kind;
constraintExpr temp;
- DPRINTF(( message ("Doing constraintExpr_searchAndAdd %s %s %s ",
- constraintExpr_unparse(c), constraintExpr_unparse(find), constraintExpr_unparse(add) ) ) );
+
+ llassert (constraintExpr_isDefined (c) );
+
+ DPRINTF (( message ("Doing constraintExpr_searchAndAdd %s %s %s ",
+ constraintExpr_unparse (c), constraintExpr_unparse (find), constraintExpr_unparse (add) ) ) );
if ( constraintExpr_similar (c, find) )
{
cstring cPrint;
- cPrint = constraintExpr_unparse(c);
+ cPrint = constraintExpr_unparse (c);
- newExpr = constraintExpr_makeAddExpr (c, constraintExpr_copy(add) );
+ newExpr = constraintExpr_makeAddExpr (c, constraintExpr_copy (add) );
- DPRINTF((message ("Replacing %q with %q",
- cPrint, constraintExpr_unparse(newExpr)
+ DPRINTF ((message ("Replacing %q with %q",
+ cPrint, constraintExpr_unparse (newExpr)
)));
return newExpr;
}
break;
case unaryExpr:
temp = constraintExprData_unaryExprGetExpr (c->data);
- temp = constraintExpr_searchAndAdd (constraintExpr_copy(temp), find, add);
+ temp = constraintExpr_searchAndAdd (constraintExpr_copy (temp), find, add);
c->data = constraintExprData_unaryExprSetExpr (c->data, temp);
break;
case binaryexpr:
temp = constraintExprData_binaryExprGetExpr1 (c->data);
- temp = constraintExpr_searchAndAdd (constraintExpr_copy(temp), find, add);
+ temp = constraintExpr_searchAndAdd (constraintExpr_copy (temp), find, add);
c->data = constraintExprData_binaryExprSetExpr1 (c->data, temp);
temp = constraintExprData_binaryExprGetExpr2 (c->data);
- temp = constraintExpr_searchAndAdd (constraintExpr_copy(temp), find, add);
+ temp = constraintExpr_searchAndAdd (constraintExpr_copy (temp), find, add);
c->data = constraintExprData_binaryExprSetExpr2 (c->data, temp);
break;
default:
- llassert(FALSE);
+ llassert (FALSE);
}
return c;
static constraint constraint_searchAndAdd (/*@returned@*/ constraint c, /*@observer@*/ constraintExpr find, /*@observer@*/ constraintExpr add)
{
-
+
+
+ llassert (constraint_isDefined (c) );
+
llassert (constraint_search (c, find) );
- DPRINTF(( message ("Doing constraint_searchAndAdd %s %s %s ",
- constraint_print(c), constraintExpr_unparse(find), constraintExpr_unparse(add) ) ) );
+ DPRINTF (( message ("Doing constraint_searchAndAdd %s %s %s ",
+ constraint_print (c), constraintExpr_unparse (find), constraintExpr_unparse (add) ) ) );
c->lexpr = constraintExpr_searchAndAdd (c->lexpr, find, add);
c->expr = constraintExpr_searchAndAdd (c->expr, find, add);
constraintList newConstraints;
constraintList ret;
- newConstraints = constraintList_makeNew();
+ newConstraints = constraintList_makeNew ();
constraintList_elements (list, el)
{
return ret;
}
-static void doAdjust(/*@unused@*/ exprNode e, /*@unused@*/ exprNode forPred, /*@observer@*/ exprNode forBody, /*@observer@*/ constraintExpr iterations)
+/*@access exprNode@*/
+static void doAdjust (/*@unused@*/ exprNode e, /*@unused@*/ exprNode forPred, /*@observer@*/ exprNode forBody, /*@observer@*/ constraintExpr iterations)
{
-
+
+ llassert (exprNode_isDefined (forBody) );
+
constraintList_elements (forBody->ensuresConstraints, el)
{
/* look for var = var + 1 */
- if (incVar(el) )
+ if (constraint_isDefined (el) && incVar (el) )
{
- DPRINTF((message ("Found inc variable constraint : %s", constraint_print (el) ) ));
- forBody->requiresConstraints = constraintList_searchAndAdd(forBody->requiresConstraints, el->lexpr, iterations);
+ DPRINTF ((message ("Found inc variable constraint : %s", constraint_print (el) ) ));
+ forBody->requiresConstraints = constraintList_searchAndAdd (forBody->requiresConstraints, el->lexpr, iterations);
}
}
end_constraintList_elements;
}
-void exprNode_forLoopHeuristics( exprNode e, exprNode forPred, exprNode forBody)
+
+/*@access exprNode@*/
+
+
+static void forLoopHeuristicsImpl ( exprNode e, exprNode forPred, /*@observer@*/ exprNode forBody)
{
exprNode init, test, inc;
constraintExpr iterations;
-
+
+ llassert (exprNode_isDefined(forPred) );
+ llassert (exprNode_isDefined(forBody) );
+
init = exprData_getTripleInit (forPred->edata);
test = exprData_getTripleTest (forPred->edata);
inc = exprData_getTripleInc (forPred->edata);
if (constraintExpr_isDefined (iterations) )
{
doAdjust ( e, forPred, forBody, iterations);
- constraintExpr_free(iterations);
+ constraintExpr_free (iterations);
}
}
+/*@noaccess exprNode@*/
+
+void exprNode_forLoopHeuristics ( exprNode e, exprNode forPred, exprNode forBody)
+{
+ forLoopHeuristicsImpl (e, forPred, forBody);
+}
+
+ /*@access constraintExpr @*/
+
+static bool isInc (/*@observer@*/ constraintExpr c) /*@*/
+{
+
+ llassert (constraintExpr_isDefined (c) );
+ if (c->kind == binaryexpr )
+ {
+ constraintExprBinaryOpKind binOP;
+ constraintExpr t1, t2;
+ t1 = constraintExprData_binaryExprGetExpr1 (c->data);
+ t2 = constraintExprData_binaryExprGetExpr2 (c->data);
+
+ binOP = constraintExprData_binaryExprGetOp (c->data);
+ if (binOP == BINARYOP_PLUS)
+ if (constraintExpr_isLit (t2) && constraintExpr_getValue (t2) == 1 )
+ {
+ return TRUE;
+ }
+ }
+
+ return FALSE;
+}
+ /*@noaccess constraintExpr @*/
+
+ /*@access constraintExpr @*/
+/* look for constraints like cexrp = cexrp + 1 */
+static bool incVar (/*@notnull@*/ constraint c) /*@*/
+{
+ constraintExpr t1;
+ if (c->ar != EQ)
+ {
+ return FALSE;
+ }
+ if (! isInc (c->expr ) )
+ return FALSE;
+
+ llassert (constraintExpr_isDefined (c->expr) );
+ llassert (c->expr->kind == binaryexpr);
+
+ t1 = constraintExprData_binaryExprGetExpr1 (c->expr->data);
+ if (constraintExpr_similar (c->lexpr, t1) )
+ return TRUE;
+
+ return FALSE;
+}
+/*@noaccess constraintExpr @*/
+
+
/* else */
/* DPRINTF (("Can't get for time ")); */
/* } */
-/* if (exprNode_isError(init) ) */
+/* if (exprNode_isError (init) ) */
/* { */
/* return; */
/* } */
/* t3 = exprData_getPairA (test->edata); */
/* t4 = exprData_getPairB (test->edata); */
-/* if (sRef_sameName(t1->sref, t4->sref) ) */
+/* if (sRef_sameName (t1->sref, t4->sref) ) */
/* { */
-/* DPRINTF((message ("Found a for loop matching heuristic:%s", exprNode_unparse (forPred) ) )); */
-/* con = constraint_makeEnsureLteMaxRead(t1, t3); */
-/* forPred->ensuresConstraints = constraintList_add(forPred->ensuresConstraints, con); */
+/* DPRINTF ((message ("Found a for loop matching heuristic:%s", exprNode_unparse (forPred) ) )); */
+/* con = constraint_makeEnsureLteMaxRead (t1, t3); */
+/* forPred->ensuresConstraints = constraintList_add (forPred->ensuresConstraints, con); */
/* } */
/* else */
/* { */
-/* DPRINTF((message ("Didn't Find a for loop matching heuristic:%s %s and %s differ", exprNode_unparse (forPred), exprNode_unparse(t1), exprNode_unparse(t3) ) )); */
+/* DPRINTF ((message ("Didn't Find a for loop matching heuristic:%s %s and %s differ", exprNode_unparse (forPred), exprNode_unparse (t1), exprNode_unparse (t3) ) )); */
/* } */
/* return; */
/* } */
andersk / splint.git / blobdiff