X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/65f973be66947763bda2a1453692079800650d38..288cbc5cbbbb68f1c95fd491c667d34e162f7863:/src/constraintResolve.c diff --git a/src/constraintResolve.c b/src/constraintResolve.c index 5eb743a..9cbc788 100644 --- a/src/constraintResolve.c +++ b/src/constraintResolve.c @@ -1,6 +1,6 @@ /* -** LCLint - annotation-assisted static program checker -** Copyright (C) 1994-2001 University of Virginia, +** Splint - annotation-assisted static program checker +** Copyright (C) 1994-2002 University of Virginia, ** Massachusetts Institute of Technology ** ** This program is free software; you can redistribute it and/or modify it @@ -17,9 +17,9 @@ ** 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 */ /* @@ -30,7 +30,7 @@ /* #define DEBUGPRINT 1 */ # include /* for isdigit */ -# include "lclintMacros.nf" +# include "splintMacros.nf" # include "basic.h" # include "cgrammar.h" # include "cgrammar_tokens.h" @@ -39,7 +39,13 @@ # include "exprNodeSList.h" -/*@access constraint, exprNode @*/ +/*@access constraint, exprNode @*/ /*!!! NO! Don't do this so recklessly - design your code more carefully so you don't need to! */ + +/*@-nullderef@*/ /* !!! DRL needs to fix this code! */ +/*@-nullstate@*/ /* !!! DRL needs to fix this code! */ +/*@-nullpass@*/ /* !!! DRL needs to fix this code! */ +/*@-temptrans@*/ /* !!! DRL needs to fix this code! */ + static constraint inequalitySubstitute (/*@returned@*/ constraint p_c, constraintList p_p); @@ -125,6 +131,13 @@ static /*@only@*/ constraintList reflectChangesEnsuresFree1 (/*@only@*/ constrai DPRINTF((message ("constraintList_mergeRequires: merging %s and %s ", constraintList_print (list1), constraintList_print(list2) ) ) ); + if (context_getFlag (FLG_REDUNDANTCONSTRAINTS) ) + { + ret = constraintList_copy(list1); + ret = constraintList_addList(ret, list2); + return ret; + } + /* get constraints in list1 not satified by list2 */ temp = constraintList_reflectChanges(list1, list2); DPRINTF((message ("constraintList_mergeRequires: temp = %s", constraintList_print(temp) ) ) ); @@ -146,9 +159,9 @@ void exprNode_mergeResolve (exprNode parent, exprNode child1, exprNode child2) { constraintList temp, temp2; - DPRINTF( (message ("magically merging constraint into parent:%s for", exprNode_unparse (parent) )) ); + DPRINTF((message ("magically merging constraint into parent:%s for", exprNode_unparse (parent) )) ); - DPRINTF( (message (" children: %s and %s", exprNode_unparse (child1), exprNode_unparse(child2) ) ) ); + DPRINTF((message (" children: %s and %s", exprNode_unparse (child1), exprNode_unparse(child2) ) ) ); if (exprNode_isError (child1) || exprNode_isError(child2) ) { @@ -176,7 +189,7 @@ void exprNode_mergeResolve (exprNode parent, exprNode child1, exprNode child2) llassert(!exprNode_isError (child1) && ! exprNode_isError(child2) ); - DPRINTF( (message ("Child constraints are %s %s and %s %s", + DPRINTF((message ("Child constraints are %s %s and %s %s", constraintList_print (child1->requiresConstraints), constraintList_print (child1->ensuresConstraints), constraintList_print (child2->requiresConstraints), @@ -199,7 +212,7 @@ void exprNode_mergeResolve (exprNode parent, exprNode child1, exprNode child2) parent->requiresConstraints = temp2; - DPRINTF( (message ("Parent requires constraints are %s ", + DPRINTF((message ("Parent requires constraints are %s ", constraintList_print (parent->requiresConstraints) ) ) ); @@ -209,7 +222,7 @@ void exprNode_mergeResolve (exprNode parent, exprNode child1, exprNode child2) child2->ensuresConstraints); - DPRINTF( (message ("Parent constraints are %s and %s ", + DPRINTF((message ("Parent constraints are %s and %s ", constraintList_print (parent->requiresConstraints), constraintList_print (parent->ensuresConstraints) ) ) ); @@ -235,7 +248,7 @@ void exprNode_mergeResolve (exprNode parent, exprNode child1, exprNode child2) } else { - DPRINTF ( (message ("Subsuming %s", constraint_print (el) ) ) ); + DPRINTF ((message ("Subsuming %s", constraint_print (el) ) ) ); } } end_constraintList_elements; @@ -432,7 +445,7 @@ static /*@only@*/ constraint doResolve (/*@only@*/ constraint c, constraintList } constraint_free(c); - *resolved = TRUE; + /*drl bee: pbr*/ *resolved = TRUE; return NULL; } @@ -447,7 +460,7 @@ static /*@only@*/ constraint doResolveOr (/*@observer@*/ /*@temp@*/ constraint c - *resolved = FALSE; + /*drl bee: pbr*/ *resolved = FALSE; ret = constraint_copy(c); @@ -481,7 +494,7 @@ static /*@only@*/ constraint doResolveOr (/*@observer@*/ /*@temp@*/ constraint c curr = doResolve (curr, post1, resolved); - if (*resolved) + /*drl bee: pbr*/ if (*resolved) { /* curr is null so we don't try to free it*/ llassert(curr == NULL); @@ -547,7 +560,7 @@ static /*@only@*/ constraintList reflectChangesEnsures (/*@observer@*/ constrain } else { - DPRINTF ( (message ("Resolved away %s ", constraint_print(el) ) ) ); + DPRINTF ((message ("Resolved away %s ", constraint_print(el) ) ) ); } } end_constraintList_elements; @@ -575,7 +588,7 @@ static bool constraint_conflict (constraint c1, constraint c2) if (c1->ar == EQ) if (c1->ar == c2->ar) { - DPRINTF ( (message ("%s conflicts with %s ", constraint_print (c1), constraint_print(c2) ) ) ); + DPRINTF ((message ("%s conflicts with %s ", constraint_print (c1), constraint_print(c2) ) ) ); return TRUE; } } @@ -598,7 +611,7 @@ static bool constraint_conflict (constraint c1, constraint c2) if (constraintTerm_isExprNode(term) ) { - DPRINTF ( (message ("%s conflicts with %s ", constraint_print (c1), constraint_print(c2) ) ) ); + DPRINTF ((message ("%s conflicts with %s ", constraint_print (c1), constraint_print(c2) ) ) ); return TRUE; } } @@ -606,11 +619,11 @@ static bool constraint_conflict (constraint c1, constraint c2) if (constraint_tooDeep(c1) || constraint_tooDeep(c2) ) { - DPRINTF ( (message ("%s conflicts with %s (constraint is too deep", constraint_print (c1), constraint_print(c2) ) ) ); + DPRINTF ((message ("%s conflicts with %s (constraint is too deep", constraint_print (c1), constraint_print(c2) ) ) ); return TRUE; } - DPRINTF ( (message ("%s doesn't conflict with %s ", constraint_print (c1), constraint_print(c2) ) ) ); + DPRINTF ((message ("%s doesn't conflict with %s ", constraint_print (c1), constraint_print(c2) ) ) ); return FALSE; @@ -692,13 +705,13 @@ bool constraintList_resolve (/*@temp@*/ /*@observer@*/ constraint c, /*@temp@*/ { if ( satifies (c, el) ) { - DPRINTF ( (message ("\n%s Satifies %s\n ", constraint_print(el), constraint_print(c) ) ) ); + DPRINTF ((message ("\n%s Satifies %s\n ", constraint_print(el), constraint_print(c) ) ) ); return TRUE; } - DPRINTF ( (message ("\n%s does not satify %s\n ", constraint_print(el), constraint_print(c) ) ) ); + DPRINTF ((message ("\n%s does not satify %s\n ", constraint_print(el), constraint_print(c) ) ) ); } end_constraintList_elements; - DPRINTF ( (message ("no constraints satify %s", constraint_print(c) ) )); + DPRINTF ((message ("no constraints satify %s", constraint_print(c) ) )); return FALSE; } @@ -708,7 +721,7 @@ static bool arithType_canResolve (arithType ar1, arithType ar2) { case GTE: case GT: - if ( (ar2 == GT) || (ar2 == GTE) || (ar2 == EQ) ) + if ((ar2 == GT) || (ar2 == GTE) || (ar2 == EQ) ) { return TRUE; } @@ -721,7 +734,7 @@ static bool arithType_canResolve (arithType ar1, arithType ar2) case LT: case LTE: - if ( (ar2 == LT) || (ar2 == LTE) || (ar2 == EQ) ) + if ((ar2 == LT) || (ar2 == LTE) || (ar2 == EQ) ) return TRUE; break; default: @@ -730,6 +743,126 @@ static bool arithType_canResolve (arithType ar1, arithType ar2) return FALSE; } +/*checks for the case expr2 == sizeof buf1 and buf1 is a fixed array*/ +static bool sizeofBufComp(constraintExpr buf1, constraintExpr expr2) +{ + constraintTerm ct; + exprNode e, t; + sRef s1, s2; + /*@access constraintExpr@*/ + + if ((expr2->kind != term) && (buf1->kind != term) ) + return FALSE; + + + ct = constraintExprData_termGetTerm(expr2->data); + + if (!constraintTerm_isExprNode(ct) ) + return FALSE; + + e = constraintTerm_getExprNode(ct); + + if (e->kind != XPR_SIZEOF) + return FALSE; + + t = exprData_getSingle (e->edata); + s1 = exprNode_getSref (t); + + s2 = constraintTerm_getsRef(constraintExprData_termGetTerm(buf1->data) ); + + /*@i223@*/ /*this may be the wronge thing to test for */ + if (sRef_similarRelaxed(s1, s2) || sRef_sameName (s1, s2) ) + { + /*@i22*/ /* get rid of this test of now */ + /* if (ctype_isFixedArray (sRef_getType (s2) ) ) */ + return TRUE; + } + return FALSE; +} + +/* look for the special case of + maxSet(buf) >= sizeof(buf) - 1 +*/ + +/*@i223@*/ /*need to add some type checking */ +static bool sizeOfMaxSet( /*@observer@*/ /*@temp@*/ constraint c) +{ + constraintExpr l, r, buf1, buf2, con; + + DPRINTF(( message("sizeOfMaxSet: checking %s ", constraint_print(c) ) + )); + + l = c->lexpr; + r = c->expr; + + if (!((c->ar == EQ) || (c->ar == GTE) || (c->ar == LTE) ) ) + return FALSE; + + /*check if the constraintExpr is MaxSet(buf) */ + if (l->kind == unaryExpr) + { + if (constraintExprData_unaryExprGetOp(l->data) == MAXSET) + { + buf1 = constraintExprData_unaryExprGetExpr(l->data); + } + else + return FALSE; + } + else + return FALSE; + + + if (r->kind != binaryexpr) + return FALSE; + + buf2 = constraintExprData_binaryExprGetExpr1(r->data); + con = constraintExprData_binaryExprGetExpr2(r->data); + + if (constraintExprData_binaryExprGetOp(r->data) == BINARYOP_MINUS) + { + if (constraintExpr_canGetValue(con) ) + { + long i; + + i = constraintExpr_getValue(con); + if (i != 1) + { + return FALSE; + } + } + else + return FALSE; + } + + if (constraintExprData_binaryExprGetOp(r->data) == BINARYOP_PLUS) + { + if (constraintExpr_canGetValue(con) ) + { + long i; + + i = constraintExpr_getValue(con); + if (i != -1) + { + return FALSE; + } + } + else + return FALSE; + } + + if (sizeofBufComp(buf1, buf2)) + { + return TRUE; + } + else + { + return FALSE; + } + + +} +/*@noaccess constraintExpr@*/ + /* We look for constraint which are tautologies */ bool constraint_isAlwaysTrue (/*@observer@*/ /*@temp@*/ constraint c) @@ -742,7 +875,10 @@ bool constraint_isAlwaysTrue (/*@observer@*/ /*@temp@*/ constraint c) r = c->expr; DPRINTF(( message("constraint_IsAlwaysTrue:examining %s", constraint_print(c) ) )); - + + if (sizeOfMaxSet(c) ) + return TRUE; + if (constraintExpr_canGetValue(l) && constraintExpr_canGetValue(r) ) { int cmp; @@ -874,7 +1010,7 @@ static bool rangeCheck (arithType ar1, /*@observer@*/ constraintExpr expr1, arit return TRUE; } } - DPRINTF( ("Can't Get value")); + DPRINTF(("Can't Get value")); constraintExpr_free(e1); constraintExpr_free(e2); @@ -928,7 +1064,7 @@ static bool rangeCheck (arithType ar1, /*@observer@*/ constraintExpr expr1, arit constraintExpr_free(e1); constraintExpr_free(e2); - DPRINTF( ("Can't Get value")); + DPRINTF(("Can't Get value")); return FALSE; } @@ -967,7 +1103,7 @@ static constraint constraint_adjust (/*@returned@*/ constraint substitute, /*@ob { fileloc loc1, loc2, loc3; - DPRINTF ( (message("Start adjust on %s and %s", constraint_print(substitute), + DPRINTF ((message("Start adjust on %s and %s", constraint_print(substitute), constraint_print(old)) )); @@ -980,7 +1116,7 @@ static constraint constraint_adjust (/*@returned@*/ constraint substitute, /*@ob if (fileloc_closer (loc1, loc3, loc2)) { constraintExpr temp; - DPRINTF ( (message("Doing adjust on %s", constraint_print(substitute) ) + DPRINTF ((message("Doing adjust on %s", constraint_print(substitute) ) )); temp = substitute->lexpr; substitute->lexpr = substitute->expr; @@ -1010,7 +1146,7 @@ constraint inequalitySubstitute (/*@returned@*/ constraint c, constraintList p constraintList_elements (p, el) { - if ( (el->ar == LT ) ) + if ((el->ar == LT ) ) /* if (!constraint_conflict (c, el) ) */ /*@i523 explain this! */ { constraintExpr temp2; @@ -1062,7 +1198,7 @@ static constraint inequalitySubstituteStrong (/*@returned@*/ constraint c, con { DPRINTF (( message ("inequalitySubstituteStrong examining substituting %s on %s", constraint_print(el), constraint_print(c) ) )); - if ( (el->ar == LT ) || (el->ar == LTE ) ) + if ((el->ar == LT ) || (el->ar == LTE ) ) /* if (!constraint_conflict (c, el) ) */ /*@i523@*/ { constraintExpr temp2; @@ -1078,7 +1214,7 @@ static constraint inequalitySubstituteStrong (/*@returned@*/ constraint c, con )); temp2 = constraintExpr_copy (el->expr); constraintExpr_free(c->expr); - if ( (el->ar == LTE ) ) + if ((el->ar == LTE ) ) { c->expr = temp2; } @@ -1114,7 +1250,7 @@ static constraint inequalitySubstituteUnsound (/*@returned@*/ constraint c, co constraintList_elements (p, el) { DPRINTF (( message ("inequalitySubstituteUnsound examining substituting %s on %s", constraint_print(el), constraint_print(c) ) )); - if ( ( el->ar == LTE) || (el->ar == LT) ) + if (( el->ar == LTE) || (el->ar == LT) ) /* if (!constraint_conflict (c, el) ) */ /*@i532@*/ { constraintExpr temp2; @@ -1209,9 +1345,9 @@ return ret; static constraint constraint_solve (/*@returned@*/ constraint c) { - DPRINTF( (message ("Solving %s\n", constraint_print(c) ) ) ); + DPRINTF((message ("Solving %s\n", constraint_print(c) ) ) ); c->expr = constraintExpr_solveBinaryExpr (c->lexpr, c->expr); - DPRINTF( (message ("Solved and got %s\n", constraint_print(c) ) ) ); + DPRINTF((message ("Solved and got %s\n", constraint_print(c) ) ) ); return c; }